small improvements.

epfl-lara · Nov 3, 2024 · f624c6a · f624c6a
1 parent b92ae33
commit f624c6a
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 3 deletions.
diff --git a/lisa-sets2/src/main/scala/lisa/automation/Substitution.scala b/lisa-sets2/src/main/scala/lisa/automation/Substitution.scala
@@ -230,6 +230,13 @@ object Substitution:
 
   end Apply
 
+  object Unfold extends ProofTactic:
+    def apply(using lib: Library, proof: lib.Proof)(definition: Definition)(premise: proof.Fact): proof.ProofTacticJudgement =
+      ???
+
+
+  end Unfold
+
   // object applySubst extends ProofTactic {
 
   //   private def condflat[T](s: Seq[(T, Boolean)]): (Seq[T], Boolean) = (s.map(_._1), s.exists(_._2))

diff --git a/lisa-sets2/src/main/scala/lisa/maths/Tests.scala b/lisa-sets2/src/main/scala/lisa/maths/Tests.scala
@@ -14,13 +14,15 @@ object Tests extends lisa.Main {
   val z = variable[Term]
   val P = variable[Term >>: Formula]
 
-  //val ppp = ProofParser.reconstructProof(new File("goeland/testSubst.p"))(using ProofParser.mapAtom, ProofParser.mapTerm, ProofParser.mapVariable)
+  val ppp = ProofParser.reconstructProof(new File("goeland/testEgg.p"))(using ProofParser.mapAtom, ProofParser.mapTerm, ProofParser.mapVariable)
 
-  //checkProof(ppp)
+  checkProof(ppp)
 
 
 
+  /*
   val buveurs = Theorem(exists(x, P(x) ==> forall(y, P(y)))) {
     have(thesis) by Goeland // ("goeland/Example.buveurs2_sol")
   }
+    */
 }
diff --git a/lisa-utils/src/main/scala/lisa/utils/tptp/ProofParser.scala b/lisa-utils/src/main/scala/lisa/utils/tptp/ProofParser.scala
@@ -545,7 +545,8 @@ object ProofParser {
               case K.equality(s, t) => (s, t)
               case _ => throw new Exception(s"Expected an existential quantification, but got $f")
             }
-            Some((K.RightSubstEq(convertToKernel(sequent), numbermap(t1), Seq((s, t)), (Seq(x), fl)), name)) 
+            Some((K.RightSubstEq(convertToKernel(sequent), numbermap(t1), Seq((s, t)), (Seq(x), fl)), name))
+
           case _ => None
         }
     }