Tidy examples

FlorianCassayre · Jun 23, 2022 · 30b0c34 · 30b0c34
1 parent 58b05eb
commit 30b0c34
Show file tree

Hide file tree

Showing 3 changed files with 14 additions and 3 deletions.
diff --git a/src/main/scala/me/cassayre/florian/masterproject/examples/frontInteractiveProof1.scala b/src/main/scala/me/cassayre/florian/masterproject/examples/frontInteractiveProof1.scala
@@ -1,5 +1,7 @@
 package me.cassayre.florian.masterproject.examples
 
+import lisa.kernel.proof.SCProofChecker
+
 import scala.util.chaining.*
 import me.cassayre.florian.masterproject.front.fol.FOL.{*, given}
 import me.cassayre.florian.masterproject.front.proof.Proof.{*, given}
@@ -56,4 +58,11 @@ import me.cassayre.florian.masterproject.front.theory.SetTheory.*
 
     p.asTheorem()
   }
+
+  println("=== Reconstruction ===")
+  println("(t0):")
+  println(KernelPrinter.prettyJudgedProof(SCProofChecker.checkSCProof(reconstructSCProofForTheorem(t0))))
+  println()
+  println("(t1):")
+  println(KernelPrinter.prettyJudgedProof(SCProofChecker.checkSCProof(reconstructSCProofForTheorem(t1))))
 }
diff --git a/src/main/scala/me/cassayre/florian/masterproject/examples/frontInteractiveProof2.scala b/src/main/scala/me/cassayre/florian/masterproject/examples/frontInteractiveProof2.scala
@@ -1,5 +1,6 @@
 package me.cassayre.florian.masterproject.examples
 
+import lisa.kernel.proof.SCProofChecker
 import me.cassayre.florian.masterproject.front.fol.FOL.{*, given}
 import me.cassayre.florian.masterproject.front.parser.FrontMacro.{*, given}
 import me.cassayre.florian.masterproject.front.printer.FrontPositionedPrinter.*
@@ -157,4 +158,7 @@ import scala.util.chaining.*
 
     asTheorem()
   }
+
+  println("=== Reconstruction ===")
+  println(KernelPrinter.prettyJudgedProof(SCProofChecker.checkSCProof(reconstructSCProofForTheorem(thmUnionAny))))
 }
diff --git a/src/main/scala/me/cassayre/florian/masterproject/examples/frontSolver.scala b/src/main/scala/me/cassayre/florian/masterproject/examples/frontSolver.scala
@@ -21,9 +21,7 @@ import scala.util.chaining.*
     val theorem: Theorem = ProofMode(sequent).tap(_(propositionalSolver)).asTheorem()
     val scProof: SCProof = reconstructSCProofForTheorem(theorem)
 
-    println(KernelPrinter.prettyProof(scProof))
-    println()
-    assert(SCProofChecker.checkSCProof(scProof).isValid)
+    println(KernelPrinter.prettyJudgedProof(SCProofChecker.checkSCProof(scProof)))
   }
 
   testSolve(sequent"?a |- ?a")