Fix congruence issues (some statements where missing assumptions that were silently added).

Author: SimonGuilloud

lisa-sets/src/main/scala/lisa/Tests.scala

@@ -30,17 +30,24 @@ object Congruence extends ProofTactic with ProofSequentTactic with ProofFactSequ
     val botWithAssumptions = bot.left ++ newAssumptions.map(_._1) |- bot.right
     var seq = botWithAssumptions
 
-    TacticSubproof {
+    TacticSubproof { iProof ?=>
       import lib.*
 
       have(botWithAssumptions) by this
-      for ((assumption, f) <- newAssumptions.reverse) {
+      //println(s"Bot with assumptions: $botWithAssumptions")
+      for ((assumption, f) <- newAssumptions) {
+        //println(s"eliminating premise ${f.statement}")
         val assumsOfPrem = f.statement.left
         if lastStep.statement.left.contains(assumption) then
-          val seq = (lastStep.statement.left - assumption) ++ assumsOfPrem |- lastStep.statement.right
+          val assumptionWeWantToGet = (lastStep.statement.left - assumption)
+          val seq = assumptionWeWantToGet ++ assumsOfPrem |- lastStep.statement.right
           have(seq) by Cut(f, lastStep)
+          //println(s"seq after cutting with the premise: $seq")
           assumsOfPrem.foldLeft(lastStep) { (step, a) =>
-            if !bot.left.exists(botAssumption => isSame(a, botAssumption)) then
+            if !assumptionWeWantToGet.exists(acceptableAssum => isSame(a, acceptableAssum)) then
+              this((step.statement.left - a) |- a) match
+                case r: iProof.ValidProofTactic => r.validate
+                case iProof.InvalidProofTactic(e) => return proof.InvalidProofTactic(s"Failed to prove $a from ${step.statement.left - a} while eliminating premise ${f.statement}: $e")
               val aProof = have((step.statement.left - a) |- a) by this //TODO: catch errors
               have(step.statement -<< a) by Cut(aProof, step)
             else step

lisa-sets/src/main/scala/lisa/automation/Congruence.scala

@@ -296,6 +296,25 @@ object CartesianProduct extends lisa.Main {
     )
   }
 
+  val R = variable[Ind]
+  val CongTest = Theorem(
+    (A × B) ∪ (C × D) ⊆ R
+  ) {
+    val left = have((A × B) ⊆ R) by Sorry
+    val right = have((C × D) ⊆ R) by Sorry
+    val s1 = Union.idempotence of (x := R)
+    val s2 = Union.monotonic of (x := (A × B), y := (C × D), a := R, b := R)
+
+    have(s1.statement) by Restate.from(s1)
+    have(s2.statement) by Restate.from(s2)
+
+    have(thesis) by Congruence.from(
+      s1,
+      s2,
+      left,
+      right
+    )
+  }
   /**
    * Theorem --- The union of two Cartesian products `A × B` and `C × D` is a subset
    * of the Cartesian product of the unions.
@@ -315,10 +334,15 @@ object CartesianProduct extends lisa.Main {
       Union.rightSubset of (x := A, y := C),
       Union.rightSubset of (x := B, y := D)
     )
+    val s1 = Union.idempotence of (x := RHS)
+    val s2 = Union.monotonic of (x := (A × B), y := (C × D), a := RHS, b := RHS)
+
+    have(s1.statement) by Restate.from(s1)
+    have(s2.statement) by Restate.from(s2)
 
     have(thesis) by Congruence.from(
-      Union.monotonic of (x := (A × B), y := (C × D), a := RHS, b := RHS),
-      Union.idempotence of (x := RHS),
+      s1,
+      s2,
       left,
       right
     )

lisa-sets/src/main/scala/lisa/maths/SetTheory/Base/CartesianProduct.scala

@@ -344,8 +344,8 @@ object BasicTheorems extends lisa.Main {
 
       // 6. g(fst(z)) = snd(z)
       val step6 = have(g(fst(z)) === snd(z)) by Congruence.from(
-        step4,
-        step5
+        step5,
+        step4
       )
 
       // 7. fst(z) ∈ dom(g)

lisa-sets/src/main/scala/lisa/maths/SetTheory/Functions/BasicTheorems.scala

@@ -145,10 +145,10 @@ object WellOrderedRecursion extends lisa.Main {
       }
 
       // By definition of G1(x) and G2(x), this means that G1(x) === G2(x)
-      have(minimal(x)(D)(<) |- G1(x) === G2(x)) by Congruence.from(
-        lastStep,
+      have((x ∈ A, minimal(x)(D)(<)) |- G1(x) === G2(x)) by Congruence.from(
         `G1(x)`,
-        `G2(x)`
+        `G2(x)`,
+        lastStep
       )
 
       // Contradiction since x ∈ D implies G1(x) ≠ G2(x)
@@ -349,7 +349,7 @@ object WellOrderedRecursion extends lisa.Main {
       }
 
       // By definition of f(x) and g(x), this means that f(x) === g(x)
-      have(minimal(x)(D)(<) |- f(x) === g(x)) by Congruence.from(
+      have((x ∈ dom(f), x ∈ dom(g), minimal(x)(D)(<)) |- f(x) === g(x)) by Congruence.from(
         lastStep,
         `f(x)`,
         `g(x)`
@@ -739,7 +739,7 @@ object WellOrderedRecursion extends lisa.Main {
         thenHave(y ∈ initialSegment(x)(A)(<) |- dom(G_(y)) ∈ D) by Substitute(`d ∈ D` of (d := dom(G_(y))))
 
       val `==>` = have(⋃(D) ⊆ initialSegment(x)(A)(<)) subproof {
-        have((y ∈ A, y < x, G_(y) === f, dom(f) === d) |- d ⊆ initialSegment(x)(A)(<)) by Congruence.from(
+        have((y ∈ initialSegment(x)(A)(<), y ∈ A, y < x, G_(y) === f, dom(f) === d) |- d ⊆ initialSegment(x)(A)(<)) by Congruence.from(
           InitialSegment.monotonic of (x := y, y := x),
           `dom(G_y)`
         )
@@ -811,7 +811,7 @@ object WellOrderedRecursion extends lisa.Main {
     have(y ∈ initialSegment(x)(A)(<) |- G_x(y) === F(y)(G_x ↾ initialSegment(y)(A)(<))) subproof {
       assume(y ∈ initialSegment(x)(A)(<))
 
-      val `y ∈ dom(G_z)` = have(y ∈ initialSegment(z)(A)(<) |- y ∈ dom(G_(z))) by Congruence.from(`dom(G_y)` of (y := z))
+      val `y ∈ dom(G_z)` = have((z ∈ initialSegment(x)(A)(<), y ∈ initialSegment(z)(A)(<)) |- y ∈ dom(G_(z))) by Congruence.from(`dom(G_y)` of (y := z))
 
       /**
        * We show that if `y < z` then `G_z(y) = F(y, G_x ↾ A_<y)`.

lisa-sets/src/main/scala/lisa/maths/SetTheory/Order/WellOrders/WellOrderedRecursion.scala

@@ -43,7 +43,7 @@ object TransfiniteRecursion extends lisa.Main {
     )
 
     // It remains to replace `initialSegment(β, α, <)` with `β` under the binders.
-    have(G(β) === F(β)(G ↾ initialSegment(β)(α)(membershipRelation(α))) |- (G(β) === F(β)(G ↾ β))) by Congruence.from(Ordinal.ordinalInitialSegment)
+    have((G(β) === F(β)(G ↾ initialSegment(β)(α)(membershipRelation(α))), β ∈ α) |- (G(β) === F(β)(G ↾ β))) by Congruence.from(Ordinal.ordinalInitialSegment)
     thenHave(β ∈ α ==> (G(β) === F(β)(G ↾ initialSegment(β)(α)(membershipRelation(α)))) |- β ∈ α ==> (G(β) === F(β)(G ↾ β))) by Tautology
     thenHave(∀(β, β ∈ α ==> (G(β) === F(β)(G ↾ initialSegment(β)(α)(membershipRelation(α))))) |- β ∈ α ==> (G(β) === F(β)(G ↾ β))) by LeftForall
     thenHave(∀(β, β ∈ α ==> (G(β) === F(β)(G ↾ initialSegment(β)(α)(membershipRelation(α))))) |- ∀(β, β ∈ α ==> (G(β) === F(β)(G ↾ β)))) by RightForall