From e2620d368a61c54508fe611f57a50cfac4178965 Mon Sep 17 00:00:00 2001 From: Sankalp Gambhir Date: Mon, 3 Jul 2023 10:48:44 +0200 Subject: [PATCH] Allow instantiate to weaken sequents --- .../src/main/scala/lisa/prooflib/SimpleDeducedSteps.scala | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lisa-utils/src/main/scala/lisa/prooflib/SimpleDeducedSteps.scala b/lisa-utils/src/main/scala/lisa/prooflib/SimpleDeducedSteps.scala index 97129853..65ae99ef 100644 --- a/lisa-utils/src/main/scala/lisa/prooflib/SimpleDeducedSteps.scala +++ b/lisa-utils/src/main/scala/lisa/prooflib/SimpleDeducedSteps.scala @@ -118,8 +118,8 @@ object SimpleDeducedSteps { res._3 match { case proof.InvalidProofTactic(_) => res._3 case proof.ValidProofTactic(_, _) => { - if (SC.isSameSequent(res._1.conclusion, bot)) - proof.ValidProofTactic(Seq(SC.SCSubproof(res._1.withNewSteps(IndexedSeq(SC.Restate(bot, res._1.length - 1))), Seq(-1))), Seq(premise)) + if (SC.isImplyingSequent(res._1.conclusion, bot)) + proof.ValidProofTactic(Seq(SC.SCSubproof(res._1.withNewSteps(IndexedSeq(SC.Weakening(bot, res._1.length - 1))), Seq(-1))), Seq(premise)) else proof.InvalidProofTactic(s"InstantiateForall proved \n\t${FOLParser.printSequent(res._1.conclusion)}\ninstead of input sequent\n\t${FOLParser.printSequent(bot)}") }