From 2644c1779a6bab28bb06c47230505866e384d6e7 Mon Sep 17 00:00:00 2001
From: Katja Goltsova <katja.goltsova@protonmail.com>
Date: Tue, 4 Oct 2022 17:29:53 +0200
Subject: [PATCH] Parse the provided theorem statement and compare it to the
 proof conclusion

Change the statements of existing theorems accordingly: into expressions that
the parser can parse.
---
 .../src/main/scala/lisa/utils/TheoriesHelpers.scala    |  2 +-
 src/main/scala/lisa/proven/mathematics/Mapping.scala   | 10 ++++++----
 src/main/scala/lisa/proven/mathematics/SetTheory.scala |  8 ++++----
 src/main/scala/lisa/proven/peano_example/Peano.scala   |  6 +++---
 4 files changed, 14 insertions(+), 12 deletions(-)

diff --git a/lisa-utils/src/main/scala/lisa/utils/TheoriesHelpers.scala b/lisa-utils/src/main/scala/lisa/utils/TheoriesHelpers.scala
index 504c9077..9f6cfbc4 100644
--- a/lisa-utils/src/main/scala/lisa/utils/TheoriesHelpers.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/TheoriesHelpers.scala
@@ -27,7 +27,7 @@ trait TheoriesHelpers extends KernelHelpers {
      * of the theorem to have more explicit writing and for sanity check.
      */
     def theorem(name: String, statement: String, proof: SCProof, justifications: Seq[theory.Justification]): RunningTheoryJudgement[theory.Theorem] = {
-      val expected = proof.conclusion // parse(statement)
+      val expected = Parser.parseSequent(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)
diff --git a/src/main/scala/lisa/proven/mathematics/Mapping.scala b/src/main/scala/lisa/proven/mathematics/Mapping.scala
index 33715213..f318e410 100644
--- a/src/main/scala/lisa/proven/mathematics/Mapping.scala
+++ b/src/main/scala/lisa/proven/mathematics/Mapping.scala
@@ -12,7 +12,7 @@ import SetTheory.*
 object Mapping extends lisa.Main {
 
   THEOREM("functionalMapping") of
-    "∀a. (a ∈ ?A) ⇒ ∃!x. ?phi(x, a) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ ?A) ∧ ?phi(x, a)" PROOF {
+    "∀ 'a. elem('a, 'A) ⇒ (∃! 'x. 'phi('x, 'a)) ⊢ ∃! 'X. ∀ 'x. elem('x, 'X) ↔ (∃ 'a. elem('a, 'A) ∧ 'phi('x, 'a))" PROOF {
       val a = VariableLabel("a")
       val x = VariableLabel("x")
       val y = VariableLabel("y")
@@ -235,7 +235,8 @@ object Mapping extends lisa.Main {
   show
 
   THEOREM("lemmaLayeredTwoArgumentsMap") of
-    "∀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)" PROOF {
+    "∀ 'b. elem('b, 'B) ⇒ (∀ 'a. elem('a, 'A) ⇒ (∃! 'x. 'psi('x, 'a, 'b))) ⊢ " +
+    "∃! 'X. ∀ 'x. elem('x, 'X) ↔ (∃ 'b. elem('b, 'B) ∧ (∀ 'x1. elem('x1, 'x) ↔ (∃ 'a. elem('a, 'A) ∧ 'psi('x1, 'a, 'b))))" PROOF {
       val a = VariableLabel("a")
       val b = VariableLabel("b")
       val x = VariableLabel("x")
@@ -299,7 +300,7 @@ object Mapping extends lisa.Main {
   show
 
   THEOREM("applyFunctionToUniqueObject") of
-    "∃!x. ?phi(x) ⊢ ∃!z. ∃x. (z = ?F(x)) ∧ ?phi(x)" PROOF {
+    "∃! 'x. 'phi('x) ⊢ ∃! 'z. ∃ 'x. ('z = 'F('x)) ∧ 'phi('x)" PROOF {
       val x = VariableLabel("x")
       val x1 = VariableLabel("x1")
       val z = VariableLabel("z")
@@ -348,7 +349,8 @@ object Mapping extends lisa.Main {
   show
 
   THEOREM("mapTwoArguments") of
-    "∀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)" PROOF {
+    "∀ 'b. elem('b, 'B) ⇒ (∀ 'a. elem('a, 'A) ⇒ (∃! 'x. 'psi('x, 'a, 'b))) ⊢ " +
+    "∃! 'z. ∃ 'x. 'z = union('x) ∧ (∀ 'x_0. elem('x_0, 'x) ↔ (∃ 'b. elem('b, 'B) ∧ (∀ 'x1. elem('x1, 'x_0) ↔ (∃ 'a. elem('a, 'A) ∧ 'psi('x1, 'a, 'b)))))" PROOF {
       val a = VariableLabel("a")
       val b = VariableLabel("b")
       val x = VariableLabel("x")
diff --git a/src/main/scala/lisa/proven/mathematics/SetTheory.scala b/src/main/scala/lisa/proven/mathematics/SetTheory.scala
index 611c82a5..c02bd0c0 100644
--- a/src/main/scala/lisa/proven/mathematics/SetTheory.scala
+++ b/src/main/scala/lisa/proven/mathematics/SetTheory.scala
@@ -8,7 +8,7 @@ import lisa.automation.kernel.ProofTactics.*
  */
 object SetTheory extends lisa.Main {
 
-  THEOREM("russelParadox") of "∀x. (x ∈ ?y) ↔ ¬(x ∈ x) ⊢" PROOF {
+  THEOREM("russelParadox") of "∀'x. elem('x, 'y) ↔ ¬elem('x, 'x) ⊢" PROOF {
     val y = VariableLabel("y")
     val x = VariableLabel("x")
     val s0 = RewriteTrue(in(y, y) <=> !in(y, y) |- ())
@@ -18,7 +18,7 @@ object SetTheory extends lisa.Main {
   thm"russelParadox".show
 
   THEOREM("unorderedPair_symmetry") of
-    "⊢ ∀y, x. {x, y} = {y, x}" PROOF {
+    "⊢ ∀'y. ∀'x. unordered_pair('x, 'y) = unordered_pair('y, 'x)" PROOF {
       val x = VariableLabel("x")
       val y = VariableLabel("y")
       val z = VariableLabel("z")
@@ -72,7 +72,7 @@ object SetTheory extends lisa.Main {
 
   // This proof is old and very unoptimised
   THEOREM("unorderedPair_deconstruction") of
-    "⊢ ∀x, y, x', y'. ({x, y} = {x', y'}) ⇒ (y' = y) ∧ (x' = x) ∨ (x = y') ∧ (y = x')" PROOF {
+    "⊢ ∀'x. ∀'y. ∀ 'x1. ∀ 'y1. unordered_pair('x, 'y) = unordered_pair('x1, 'y1) ⇒ 'y1 = 'y ∧ 'x1 = 'x ∨ 'x = 'y1 ∧ 'y = 'x1" PROOF {
       val x = VariableLabel("x")
       val y = VariableLabel("y")
       val x1 = VariableLabel("x'")
@@ -327,7 +327,7 @@ object SetTheory extends lisa.Main {
     } using ax"pairAxiom"
   thm"unorderedPair_deconstruction".show
 
-  THEOREM("noUniversalSet") of "∀x. x ∈ ?z ⊢" PROOF {
+  THEOREM("noUniversalSet") of "∀'x. elem('x, 'z) ⊢ " PROOF {
     val x = VariableLabel("x")
     val y = VariableLabel("y")
     val z = VariableLabel("z")
diff --git a/src/main/scala/lisa/proven/peano_example/Peano.scala b/src/main/scala/lisa/proven/peano_example/Peano.scala
index 90479702..47642c62 100644
--- a/src/main/scala/lisa/proven/peano_example/Peano.scala
+++ b/src/main/scala/lisa/proven/peano_example/Peano.scala
@@ -66,7 +66,7 @@ object Peano {
   val (y1, z1) =
     (VariableLabel("y1"), VariableLabel("z1"))
 
-  THEOREM("x + 0 = 0 + x") of "?x. plus(x, zero) === plus(zero, x)" PROOF {
+  THEOREM("x + 0 = 0 + x") of "∀'x. +('x, 0) = +(0, 'x)" PROOF {
     val refl0: SCProofStep = RightRefl(() |- s(x) === s(x), s(x) === s(x))
     val subst1 = RightSubstEq((x === plus(zero, x)) |- s(x) === s(plus(zero, x)), 0, (x, plus(zero, x)) :: Nil, LambdaTermFormula(Seq(y), s(x) === s(y)))
     val implies2 = RightImplies(() |- (x === plus(zero, x)) ==> (s(x) === s(plus(zero, x))), 1, x === plus(zero, x), s(x) === s(plus(zero, x)))
@@ -147,7 +147,7 @@ object Peano {
   } using (ax"ax4plusSuccessor", ax"ax3neutral", ax"ax7induction")
   show
 
-  THEOREM("switch successor") of "?y. ?x. plus(x, s(y)) === plus(s(x), y)" PROOF {
+  THEOREM("switch successor") of "∀'x. ∀'y. +('x, S('y)) = +(S('x), 'y)" PROOF {
     //////////////////////////////////// Base: x + S0 = Sx + 0 ///////////////////////////////////////////////
     val base0 = {
       // x + 0 = x
@@ -256,7 +256,7 @@ object Peano {
   } using (ax"ax3neutral", ax"ax4plusSuccessor", ax"ax7induction")
   show
 
-  THEOREM("additivity of addition") of "" PROOF {
+  THEOREM("additivity of addition") of "∀'x. ∀'y. +('x, 'y) = +('y, 'x)" PROOF {
     val base0 = SCSubproof(instantiateForallImport(thm"x + 0 = 0 + x", x), Seq(-3))
     val inductionStep1 = {
       val start0 = RightRefl(() |- plus(x, s(y)) === plus(x, s(y)), plus(x, s(y)) === plus(x, s(y)))
-- 
GitLab