Allow InstantiateForall to weaken sequents (#169)

epfl-lara · Jul 3, 2023 · 93bbf67 · 93bbf67
1 parent 1ee6175
commit 93bbf67
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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)}")
           }