From be0bb767484e20c0b27f6848094112f251211979 Mon Sep 17 00:00:00 2001
From: SimonGuilloud <sim-guilloud@bluewin.ch>
Date: Fri, 10 Jun 2022 15:07:32 +0200
Subject: [PATCH] updating the presentation of proofs and theories.

---
 .../lisa/kernel/proof/RunningTheory.scala     | 13 +++++--
 src/main/scala/proven/DSetTheory/Part1.scala  | 38 ++++++++++++++-----
 .../scala/proven/ElementsOfSetTheory.scala    | 20 ++++++++--
 src/main/scala/proven/dev/MainLibrary.scala   | 11 ++++++
 src/main/scala/proven/dev/SetTheory.scala     | 37 ++++++++++++++++++
 src/main/scala/utilities/KernelHelpers.scala  |  6 ++-
 .../scala/utilities/TheoriesHelpers.scala     | 21 ++++++++++
 7 files changed, 129 insertions(+), 17 deletions(-)
 create mode 100644 src/main/scala/proven/dev/MainLibrary.scala
 create mode 100644 src/main/scala/proven/dev/SetTheory.scala
 create mode 100644 src/main/scala/utilities/TheoriesHelpers.scala

diff --git a/src/main/scala/lisa/kernel/proof/RunningTheory.scala b/src/main/scala/lisa/kernel/proof/RunningTheory.scala
index 6364970e..49e6e1a0 100644
--- a/src/main/scala/lisa/kernel/proof/RunningTheory.scala
+++ b/src/main/scala/lisa/kernel/proof/RunningTheory.scala
@@ -74,10 +74,15 @@ class RunningTheory {
    * The proof's imports must be justified by the list of justification, and the conclusion of the theorem
    * can't contain symbols that do not belong to the theory.
    * @param justifications The list of justifications of the proof's imports.
-   * @param p The proof of the desired Theorem.
+   * @param proof The proof of the desired Theorem.
    * @return A Theorem if the proof is correct, None else
    */
-  def proofToTheorem(name: String, proof: SCProof, justifications: Seq[Justification]): RunningTheoryJudgement[this.Theorem] =
+  def makeTheorem(name: String, statement:Sequent, proof: SCProof, justifications: Seq[Justification]): RunningTheoryJudgement[this.Theorem] = {
+    if (proof.conclusion == statement) proofToTheorem(name, proof, justifications)
+    else InvalidJustification("The proof does not prove the claimed statement", None)
+  }
+
+  private def proofToTheorem(name: String, proof: SCProof, justifications: Seq[Justification]): RunningTheoryJudgement[this.Theorem] =
     if (proof.imports.forall(i => justifications.exists(j => isSameSequent(i, sequentFromJustification(j)))))
       if (belongsToTheory(proof.conclusion))
         val r = SCProofChecker.checkSCProof(proof)
@@ -85,7 +90,7 @@ class RunningTheory {
           case SCProofCheckerJudgement.SCValidProof =>
             val thm = Theorem(name, proof.conclusion)
             theorems.update(name, thm)
-            RunningTheoryJudgement.ValidJustification(thm)
+            ValidJustification(thm)
           case r @ SCProofCheckerJudgement.SCInvalidProof(path, message) =>
             InvalidJustification("The given proof is incorrect: " + message, Some(r))
         }
@@ -149,7 +154,7 @@ class RunningTheory {
                       val newDef = FunctionDefinition(label, args, out, phi)
                       definitions.update(label, Some(newDef))
                       RunningTheoryJudgement.ValidJustification(newDef)
-                    } else InvalidJustification("The proof is correct but its conclusion does not correspond to a definition for for the formula phi.", None)
+                    } else InvalidJustification("The proof is correct but its conclusion does not correspond to a definition for the formula phi.", None)
                   case _ => InvalidJustification("The conclusion of the proof must have an empty left hand side, and a single formula on the right hand side.", None)
                 }
               case r @ SCProofCheckerJudgement.SCInvalidProof(path, message) => InvalidJustification("The given proof is incorrect: " + message, Some(r))
diff --git a/src/main/scala/proven/DSetTheory/Part1.scala b/src/main/scala/proven/DSetTheory/Part1.scala
index 4a8b0fb2..20e8e8af 100644
--- a/src/main/scala/proven/DSetTheory/Part1.scala
+++ b/src/main/scala/proven/DSetTheory/Part1.scala
@@ -1,8 +1,8 @@
 package proven.DSetTheory
 import utilities.KernelHelpers.{_, given}
+import utilities.TheoriesHelpers.{*, given}
 import lisa.kernel.Printer
-import lisa.kernel.Printer.prettyFormula
-import lisa.kernel.Printer.prettySCProof
+import lisa.kernel.Printer.{prettyFormula, prettySCProof, prettySequent}
 import lisa.kernel.fol.FOL
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.SCProof
@@ -45,7 +45,8 @@ object Part1 {
     // val s4 = Rewrite(() |- !exists(y1, forall(x1, in(x1,y1) <=> !in(x1, x1))), 3)
     SCProof(s0, s1, s2)
   }
-  val thm_russelParadox = theory.proofToTheorem("russelParadox", russelParadox, Nil).get
+  println(prettySequent(russelParadox.conclusion))
+  val thm_russelParadox = theory.theorem("russelParadox", "∀x. (x ∈ ?y) ↔ ¬(x ∈ x) ⊢", russelParadox, Nil).get
 
   val thm4: SCProof = {
     // forall(z, exists(y, forall(x, in(x,y) <=> (in(x,y) /\ sPhi(x,z)))))
@@ -70,7 +71,8 @@ object Part1 {
     val s10 = Cut(forall(x1, in(x1, z)) |- (), 0, 9, exists(y1, forall(x1, in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1)))))
     SCProof(Vector(s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10), Vector(i1, i2))
   }
-  val thm_thm4 = theory.proofToTheorem("thm4", thm4, Seq(axiom(comprehensionSchema), thm_russelParadox)).get
+  println(prettySequent(thm4.conclusion))
+  val thm_thm4 = theory.theorem("thm4", "∀x. x ∈ ?z ⊢", thm4, Seq(axiom(comprehensionSchema), thm_russelParadox)).get
 
   val thmMapFunctional: SCProof = {
     val a = VariableLabel("a")
@@ -303,7 +305,13 @@ object Part1 {
     val steps = Vector(s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, s17, s18, s19, s20, s21, s22)
     SCProof(steps, Vector(i1, i2, i3))
   }
-  val thm_thmMapFunctional = theory.proofToTheorem("thmMapFunctional", thmMapFunctional, Seq(axiom(replacementSchema), axiom(comprehensionSchema), axiom(extensionalityAxiom))).get
+  println(prettySequent(thmMapFunctional.conclusion))
+  val thm_thmMapFunctional = theory.theorem("thmMapFunctional",
+    "∀a. (a ∈ ?A) ⇒ ∃!x. ?phi(x, a) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ ?A) ∧ ?phi(x, a)",
+    thmMapFunctional,
+    Seq(axiom(replacementSchema),
+      axiom(comprehensionSchema), axiom(extensionalityAxiom))
+  ).get
 
   /**
    * ∀ b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b)    |-    ∃!X. ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b)
@@ -373,7 +381,13 @@ object Part1 {
     // by thmMapFunctional have ∀b. (b ∈ B) ⇒ ∃!x. ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b)        phi(x, b) = ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b)    s6
     // have ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b)    |-    ∃!X. ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b)   s7
   }
-  val thm_lemma1 = theory.proofToTheorem("lemma1", lemma1, Seq(thm_thmMapFunctional)).get
+  println(prettySequent(lemma1.conclusion))
+  val thm_lemma1 = theory.theorem(
+    "lemma1",
+    "∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ ?A) ∧ ?psi(x1, a, b)",
+    lemma1,
+    Seq(thm_thmMapFunctional)
+  ).get
 
   /*
     val lemma2 = SCProof({
@@ -454,7 +468,8 @@ object Part1 {
     // redGoal2 x=x1 <=> phi(x), z=F(x), x=x1   ⊢   F(x1)=z  g2.s1
     // redGoal2 x=x1 <=> phi(x), z=F(x1), x=x1   ⊢   F(x1)=z TRUE  g2.s0
   }
-  val thm_lemmaApplyFToObject = theory.proofToTheorem("lemmaApplyFToObject", lemmaApplyFToObject, Nil).get
+  println(prettySequent(lemmaApplyFToObject.conclusion))
+  val thm_lemmaApplyFToObject = theory.theorem("lemmaApplyFToObject", "∃!x. ?phi(x) ⊢ ∃!z. ∃x. (z = ?F(x)) ∧ ?phi(x)", lemmaApplyFToObject, Nil).get
 
   /**
    * ∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!z. ∃x. (z = U(x)) ∧ ∀x_0. (x_0 ∈ x) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x_0) ↔ ∃a. (a ∈ ?A) ∧ ?psi(x1, a, b)
@@ -485,7 +500,13 @@ object Part1 {
     val s2 = Cut(i1.left |- seq1.right, -1, 1, seq1.left.head)
     SCProof(Vector(s0, s1, s2), Vector(i1, i2))
   }
-  val thm_lemmaMapTwoArguments = theory.proofToTheorem("lemmaMapTwoArguments", lemmaMapTwoArguments, Seq(thm_lemma1, thm_lemmaApplyFToObject)).get
+  println(prettySequent(lemmaMapTwoArguments.conclusion))
+  val thm_lemmaMapTwoArguments = theory.theorem(
+    "lemmaMapTwoArguments",
+    "∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!z. ∃x. (z = U(x)) ∧ ∀x_0. (x_0 ∈ x) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x_0) ↔ ∃a. (a ∈ ?A) ∧ ?psi(x1, a, b)",
+    lemmaMapTwoArguments,
+    Seq(thm_lemma1, thm_lemmaApplyFToObject)
+  ).get
 
   /**
    *  ⊢ ∃!z. ∃x. (z = U(x)) ∧ ∀x_0. (x_0 ∈ x) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x_0) ↔ ∃a. (a ∈ ?A) ∧ (x1 = (a, b))
@@ -541,7 +562,6 @@ object Part1 {
     SCProof(Vector(s0, s1, s2, s3, s4, s5, s6), Vector(i1))
 
   }
-  println("cartesian")
   /*
     val thm_lemmaCartesianProduct = theory.proofToTheorem("lemmaCartesianProduct", lemmaCartesianProduct, Seq(thm_lemmaMapTwoArguments)).get
 
diff --git a/src/main/scala/proven/ElementsOfSetTheory.scala b/src/main/scala/proven/ElementsOfSetTheory.scala
index 11aaa022..e39d29e9 100644
--- a/src/main/scala/proven/ElementsOfSetTheory.scala
+++ b/src/main/scala/proven/ElementsOfSetTheory.scala
@@ -5,7 +5,9 @@ import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SCProofChecker
 import lisa.kernel.proof.SequentCalculus.*
 import utilities.KernelHelpers.{*, given}
+import utilities.TheoriesHelpers.{*, given}
 import lisa.kernel.Printer
+import lisa.kernel.Printer.*
 import proven.tactics.ProofTactics.*
 import proven.tactics.Destructors.*
 import lisa.settheory.AxiomaticSetTheory.*
@@ -74,7 +76,8 @@ object ElementsOfSetTheory {
     val fin4 = generalizeToForall(fin3, fin3.conclusion.right.head, y)
     fin4.copy(imports = imps)
   } //   |- ∀∀({x$1,y$2}={y$2,x$1})
-  val thm_proofUnorderedPairSymmetry: theory.Theorem = theory.proofToTheorem("proofUnorderedPairSymmetry", proofUnorderedPairSymmetry, Seq(axiom(extensionalityAxiom), axiom(pairAxiom))).get
+  println(prettySequent(proofUnorderedPairSymmetry.conclusion))
+  val thm_proofUnorderedPairSymmetry: theory.Theorem = theory.theorem("proofUnorderedPairSymmetry", "⊢ ∀y, x. {x, y} = {y, x}", proofUnorderedPairSymmetry, Seq(axiom(extensionalityAxiom), axiom(pairAxiom))).get
 
   val proofUnorderedPairDeconstruction: SCProof = {
     val pxy = pair(x, y)
@@ -324,8 +327,8 @@ object ElementsOfSetTheory {
     val p2 = RightImplies(emptySeq +> (p1.bot.left.head ==> p1.bot.right.head), 1, p1.bot.left.head, p1.bot.right.head) //   |- ({x,y}={x',y'}) ==> (x=x' /\ y=y')\/(x=y' /\ y=x')
     generalizeToForall(SCProof(IndexedSeq(p0, p1, p2), IndexedSeq(() |- pairAxiom)), x, y, x1, y1)
   } // |- ∀∀∀∀(({x$4,y$3}={x'$2,y'$1})⇒(((y'$1=y$3)∧(x'$2=x$4))∨((x$4=y'$1)∧(y$3=x'$2))))
-
-  val thm_proofUnorderedPairDeconstruction = theory.proofToTheorem("proofUnorderedPairDeconstruction", proofUnorderedPairDeconstruction, Seq(axiom(pairAxiom))).get
+  println(prettySequent(proofUnorderedPairDeconstruction.conclusion))
+  val thm_proofUnorderedPairDeconstruction = theory.theorem("proofUnorderedPairDeconstruction", "⊢ ∀x, y, x', y'. ({x, y} = {x', y'}) ⇒ (y' = y) ∧ (x' = x) ∨ (x = y') ∧ (y = x')", proofUnorderedPairDeconstruction, Seq(axiom(pairAxiom))).get
 
   // i2, i1, p0, p1, p2, p3
 
@@ -455,4 +458,15 @@ object ElementsOfSetTheory {
     ???
   } // |- (x,y)=(x', y')  ===>  x=x' /\ y=y'
    */
+
+  def main(args: Array[String]): Unit = {
+    def checkProof(proof: SCProof): Unit = {
+      val error = SCProofChecker.checkSCProof(proof)
+      println(prettySCProof(proof, error))
+    }
+    println("\nproofUnorderedPairSymmetry")
+    checkProof(proofUnorderedPairSymmetry)
+    println("\nproofUnorderedPairDeconstruction")
+    checkProof(proofUnorderedPairDeconstruction)
+  }
 }
diff --git a/src/main/scala/proven/dev/MainLibrary.scala b/src/main/scala/proven/dev/MainLibrary.scala
new file mode 100644
index 00000000..dd59665a
--- /dev/null
+++ b/src/main/scala/proven/dev/MainLibrary.scala
@@ -0,0 +1,11 @@
+package proven.dev
+
+import lisa.kernel.proof.RunningTheory
+import lisa.settheory.AxiomaticSetTheory
+
+trait MainLibrary {
+
+  given RunningTheory = AxiomaticSetTheory.runningSetTheory
+  import AxiomaticSetTheory.runningSetTheory.*
+
+}
diff --git a/src/main/scala/proven/dev/SetTheory.scala b/src/main/scala/proven/dev/SetTheory.scala
new file mode 100644
index 00000000..65c9b394
--- /dev/null
+++ b/src/main/scala/proven/dev/SetTheory.scala
@@ -0,0 +1,37 @@
+package proven.dev
+
+import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.SCProof
+import lisa.kernel.proof.SequentCalculus.*
+import lisa.settheory.AxiomaticSetTheory
+import lisa.settheory.AxiomaticSetTheory.*
+import proven.DSetTheory.Part1.{russelParadox, theory}
+import utilities.KernelHelpers.{*, given}
+import utilities.TheoriesHelpers.{*, given}
+
+trait SetTheory extends MainLibrary{
+  private val x = SchematicFunctionLabel("x", 0)
+  private val y = SchematicFunctionLabel("y", 0)
+  private val z = SchematicFunctionLabel("z", 0)
+  private val x1 = VariableLabel("x")
+  private val y1 = VariableLabel("y")
+  private val z1 = VariableLabel("z")
+  private val f = SchematicFunctionLabel("f", 0)
+  private val g = SchematicFunctionLabel("g", 0)
+  private val h = SchematicPredicateLabel("h", 0)
+
+  given Conversion[SchematicFunctionLabel, Term] with
+    def apply(s: SchematicFunctionLabel): Term = s()
+
+  /**
+   */
+  val russelParadox: SCProof = {
+    val contra = (in(y, y)) <=> !(in(y, y))
+    val s0 = Hypothesis(contra |- contra, contra)
+    val s1 = LeftForall(forall(x1, in(x1, y) <=> !in(x1, x1)) |- contra, 0, in(x1, y) <=> !in(x1, x1), x1, y)
+    val s2 = Rewrite(forall(x1, in(x1, y) <=> !in(x1, x1)) |- (), 1)
+    SCProof(s0, s1, s2)
+  }
+  import AxiomaticSetTheory.runningSetTheory.*
+  theorem(AxiomaticSetTheory.runningSetTheory)("russelParadox", "∀x. (x ∈ ?y) ↔ ¬(x ∈ x) ⊢", russelParadox, Nil).get
+}
diff --git a/src/main/scala/utilities/KernelHelpers.scala b/src/main/scala/utilities/KernelHelpers.scala
index b55795ff..73650c96 100644
--- a/src/main/scala/utilities/KernelHelpers.scala
+++ b/src/main/scala/utilities/KernelHelpers.scala
@@ -1,5 +1,9 @@
 package utilities
 
+import lisa.kernel.proof.RunningTheoryJudgement.InvalidJustification
+import lisa.kernel.proof.{RunningTheory, RunningTheoryJudgement, SCProof}
+import lisa.kernel.proof.SequentCalculus.{Rewrite, isSameSequent}
+
 /**
  * A helper file that provides various syntactic sugars for LISA.
  * Usage:
@@ -136,5 +140,5 @@ object KernelHelpers {
   def instantiateFunctionSchemaInSequent(s: Sequent, m: Map[SchematicFunctionLabel, LambdaTermTerm]): Sequent = {
     s.left.map(phi => instantiateFunctionSchemas(phi, m)) |- s.right.map(phi => instantiateFunctionSchemas(phi, m))
   }
-
+  
 }
diff --git a/src/main/scala/utilities/TheoriesHelpers.scala b/src/main/scala/utilities/TheoriesHelpers.scala
new file mode 100644
index 00000000..3002849c
--- /dev/null
+++ b/src/main/scala/utilities/TheoriesHelpers.scala
@@ -0,0 +1,21 @@
+package utilities
+
+import lisa.kernel.proof.RunningTheoryJudgement.InvalidJustification
+import lisa.kernel.proof.{RunningTheory, RunningTheoryJudgement, SCProof}
+import lisa.kernel.proof.SequentCalculus.{Rewrite, isSameSequent}
+
+object TheoriesHelpers {
+
+  // for when the kernel will have a dedicated parser
+  extension (theory: RunningTheory)
+    def theorem(name: String, statement:String, proof: SCProof, justifications: Seq[theory.Justification]): RunningTheoryJudgement[theory.Theorem] = {
+      val expected = proof.conclusion  // parse(statement)
+      if ( expected == proof.conclusion) theory.makeTheorem(name, expected, proof, justifications)
+      else if (isSameSequent(expected, proof.conclusion)) theory.makeTheorem(name, expected, proof.appended(Rewrite(expected, proof.length-1)), justifications)
+      else InvalidJustification("The proof does not prove the claimed statement", None)
+    }
+
+
+
+
+}
-- 
GitLab