Safe tactic calls for Restate (#118)

* Add safe tactic calls to Restate * scalafix; added tests for rewrite true * Merge cleanup * scalafix
epfl-lara · Jan 30, 2023 · 892c902 · 892c902
1 parent bbb6784
commit 892c902
Show file tree

Hide file tree

Showing 3 changed files with 35 additions and 3 deletions.
diff --git a/lisa-utils/src/main/scala/lisa/prooflib/BasicStepTactic.scala b/lisa-utils/src/main/scala/lisa/prooflib/BasicStepTactic.scala
@@ -39,6 +39,15 @@ object BasicStepTactic {
     }
   }
 
+  object RewriteTrue extends ProofTactic with ParameterlessHave {
+    def apply(using proof: Library#Proof)(bot: Sequent): proof.ProofTacticJudgement = {
+      if (!SC.isSameSequent(bot, () |- PredicateFormula(top, Nil)))
+        proof.InvalidProofTactic("The desired conclusion is not a trivial tautology.")
+      else
+        proof.ValidProofTactic(Seq(SC.RewriteTrue(bot)), Seq())
+    }
+  }
+
   /**
    * <pre>
    *  Γ |- Δ, φ    φ, Σ |- Π

diff --git a/lisa-utils/src/main/scala/lisa/prooflib/SimpleDeducedSteps.scala b/lisa-utils/src/main/scala/lisa/prooflib/SimpleDeducedSteps.scala
@@ -3,10 +3,10 @@ package lisa.prooflib
 import lisa.kernel.fol.FOL
 import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SCProofChecker
-import lisa.kernel.proof.SequentCalculus.RewriteTrue
 import lisa.kernel.proof.SequentCalculus.SCProofStep
 import lisa.kernel.proof.SequentCalculus.Sequent
 import lisa.kernel.proof.SequentCalculus as SC
+import lisa.prooflib.BasicStepTactic._
 import lisa.prooflib.ProofTacticLib.{_, given}
 import lisa.prooflib.*
 import lisa.utils.FOLParser
@@ -17,13 +17,13 @@ object SimpleDeducedSteps {
 
   object Restate extends ProofTactic with ParameterlessHave with ParameterlessAndThen {
     def apply(using proof: Library#Proof)(bot: Sequent): proof.ProofTacticJudgement =
-      proof.ValidProofTactic(Seq(SC.RewriteTrue(bot)), Nil)
+      unwrapTactic(RewriteTrue(bot))("Attempted true rewrite during tactic Restate failed.")
 
     // (proof.ProofStep | proof.OutsideFact | Int)     is definitionally equal to proof.Fact, but for some reason
     // scala compiler doesn't resolve the overload with a type alias, dependant type and implicit parameter
 
     def apply(using proof: Library#Proof)(premise: proof.ProofStep | proof.OutsideFact | Int)(bot: Sequent): proof.ProofTacticJudgement =
-      proof.ValidProofTactic(Seq(SC.Rewrite(bot, -1)), Seq(premise))
+      unwrapTactic(Rewrite(premise)(bot))("Attempted rewrite during tactic Restate failed.")
 
   }
 

diff --git a/lisa-utils/src/test/scala/lisa/utils/BasicTacticTest.scala b/lisa-utils/src/test/scala/lisa/utils/BasicTacticTest.scala
@@ -21,6 +21,7 @@ class BasicTacticTest extends ProofTacticTestLib {
 
     val incorrect = List(
       ("'P('x) |- "),
+      (" |- "),
       (" |- 'P('x)"),
       (" |- 'P('x); 'Q('x)"),
       ("'Q('x) |- ")
@@ -51,6 +52,28 @@ class BasicTacticTest extends ProofTacticTestLib {
     }
   }
 
+  // rewrite true
+  test("Tactic Tests: Rewrite True") {
+    val correct = List(
+      ("'P('x); 'Q('x) |- 'P('x); 'Q('x)"),
+      ("'P('x) |- 'P('x); 'Q('x)"),
+      ("'P('x); 'Q('x) |- 'Q('x)"),
+      ("'P('x) |- 'P('x)"),
+      ("'P('x); 'Q('x) |- 'P('x); 'R('x)")
+    )
+
+    val incorrect = List(
+      ("'R('x) |- 'P('x); 'Q('x)"),
+      ("'P('x); 'S('x) |- 'Q('x)"),
+      ("'Q('x) |- 'P('x)"),
+      (" |- ")
+    )
+
+    testTacticCases(correct, incorrect) {
+      RewriteTrue(_)
+    }
+  }
+
   // cut
   test("Tactic Tests: Cut - Parameter Inference") {
     val correct = List(