Prove all sorry holes in the library.

Author: SimonGuilloud

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

@@ -296,25 +296,6 @@ 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.

lisa-sets/src/main/scala/lisa/maths/SetTheory/Functions/Operations/Restriction.scala

@@ -86,12 +86,40 @@ object Restriction extends lisa.Main {
     val `x ∈ dom(f)` = thenHave(x ∈ dom(f) <=> ∃(z ∈ f, fst(z) === x)) by Substitute(dom.definition of (R := f))
 
     have(∀(z, z ∈ (f ↾ A) <=> (z ∈ f) /\ (fst(z) ∈ A))) by RightForall(membership)
-    have(x ∈ dom(f ↾ A) <=> ∃(z ∈ f, fst(z) ∈ A /\ (fst(z) === x))) by Tableau.from(
+    val eq1 = have(x ∈ dom(f ↾ A) <=> ∃(z ∈ f, fst(z) ∈ A /\ (fst(z) === x))) by Tableau.from(
       lastStep,
       `x ∈ dom(f)` of (f := f ↾ A)
     )
 
-    sorry
+    // Forward: ∃(z ∈ f, fst(z) ∈ A ∧ fst(z) = x) |- x ∈ dom(f) ∩ A
+    have(fst(z) ∈ A |- fst(z) ∈ A) by Hypothesis
+    val xInA = thenHave((fst(z) ∈ A, fst(z) === x) |- x ∈ A) by Congruence
+
+    have((z ∈ f, fst(z) === x) |- z ∈ f /\ (fst(z) === x)) by Restate
+    thenHave((z ∈ f, fst(z) === x) |- ∃(z, z ∈ f /\ (fst(z) === x))) by RightExists
+    val xInDomF = thenHave((z ∈ f, fst(z) === x) |- x ∈ dom(f)) by Tautology.fromLastStep(`x ∈ dom(f)`)
+
+    have(z ∈ f /\ (fst(z) ∈ A) /\ (fst(z) === x) |- x ∈ dom(f) /\ (x ∈ A)) by Tautology.from(xInA, xInDomF)
+    thenHave(∃(z, z ∈ f /\ (fst(z) ∈ A) /\ (fst(z) === x)) |- x ∈ dom(f) /\ (x ∈ A)) by LeftExists
+    val fwd = thenHave(x ∈ dom(f ↾ A) ==> x ∈ (dom(f) ∩ A)) by Tautology.fromLastStep(
+      eq1, Intersection.membership of (z := x, x := dom(f), y := A)
+    )
+
+    // Backward: x ∈ dom(f) ∩ A |- ∃(z ∈ f, fst(z) ∈ A ∧ fst(z) = x)
+    have(x ∈ A |- x ∈ A) by Hypothesis
+    val fstInA = thenHave((x ∈ A, fst(z) === x) |- fst(z) ∈ A) by Congruence
+
+    have((z ∈ f, fst(z) === x, fst(z) ∈ A) |- z ∈ f /\ (fst(z) ∈ A) /\ (fst(z) === x)) by Restate
+    thenHave((z ∈ f, fst(z) === x, x ∈ A) |- z ∈ f /\ (fst(z) ∈ A) /\ (fst(z) === x)) by Tautology.fromLastStep(fstInA)
+    thenHave((z ∈ f, fst(z) === x, x ∈ A) |- ∃(z, z ∈ f /\ (fst(z) ∈ A) /\ (fst(z) === x))) by RightExists
+    thenHave((z ∈ f /\ (fst(z) === x), x ∈ A) |- ∃(z, z ∈ f /\ (fst(z) ∈ A) /\ (fst(z) === x))) by Restate
+    thenHave((∃(z, z ∈ f /\ (fst(z) === x)), x ∈ A) |- ∃(z, z ∈ f /\ (fst(z) ∈ A) /\ (fst(z) === x))) by LeftExists
+    val bwd = thenHave(x ∈ (dom(f) ∩ A) ==> x ∈ dom(f ↾ A)) by Tautology.fromLastStep(
+      eq1, `x ∈ dom(f)`, Intersection.membership of (z := x, x := dom(f), y := A)
+    )
+
+    have(x ∈ dom(f ↾ A) <=> x ∈ (dom(f) ∩ A)) by Tautology.from(fwd, bwd)
+    thenHave(thesis) by Extensionality
   }
 
   /**
@@ -161,19 +189,166 @@ object Restriction extends lisa.Main {
   val subsetIsRestriction = Theorem(
     (function(f), g ⊆ f) |- (g === f ↾ dom(g))
   ) {
-    sorry
+    assume(function(f))
+    assume(g ⊆ f)
+
+    val gIsFunc = have(function(g)) by Restate.from(BasicTheorems.subset)
+
+    // Forward: z ∈ g → z ∈ f↾dom(g)
+    val fwd = have(z ∈ g |- z ∈ (f ↾ dom(g))) subproof {
+      assume(z ∈ g)
+      val zInF = have(z ∈ f) by Tautology.from(Subset.membership of (x := g, y := f, z := z))
+      have(fst(z) ∈ { fst(z) | z ∈ g }) by Tautology.from(Replacement.map of (x := z, A := g, F := fst))
+      val fstInDomG = thenHave(fst(z) ∈ dom(g)) by Substitute(dom.definition of (R := g))
+      have(thesis) by Tautology.from(membership of (A := dom(g)), zInF, fstInDomG)
+    }
+
+    // Backward: z ∈ f↾dom(g) → z ∈ g
+    val bwd = have(z ∈ (f ↾ dom(g)) |- z ∈ g) subproof {
+      assume(z ∈ (f ↾ dom(g)))
+      val zInF = have(z ∈ f) by Tautology.from(membership of (A := dom(g)))
+      val fstInDomG = have(fst(z) ∈ dom(g)) by Tautology.from(membership of (A := dom(g)))
+
+      // z = (fst(z), snd(z)) since f is a function
+      val zIsPair = have(z === (fst(z), snd(z))) by Tautology.from(BasicTheorems.inversion, zInF)
+      val pairInF = have((fst(z), snd(z)) ∈ f) by Congruence.from(zInF, zIsPair)
+      val fstInDomF = have(fst(z) ∈ dom(f)) by Tautology.from(BasicTheorems.domainMembership of (x := fst(z), y := snd(z)), pairInF)
+
+      // f(fst(z)) = snd(z)
+      val fApp = have(f(fst(z)) === snd(z)) by Tautology.from(
+        BasicTheorems.appDefinition of (x := fst(z), y := snd(z)), fstInDomF, pairInF
+      )
+
+      // g(fst(z)) is defined and (fst(z), g(fst(z))) ∈ g
+      val gAppInG = have((fst(z), g(fst(z))) ∈ g) by Tautology.from(
+        BasicTheorems.appDefinition of (f := g, x := fst(z), y := g(fst(z))), gIsFunc, fstInDomG
+      )
+
+      // (fst(z), g(fst(z))) ∈ f since g ⊆ f
+      val gAppInF = have((fst(z), g(fst(z))) ∈ f) by Tautology.from(
+        Subset.membership of (x := g, y := f, z := (fst(z), g(fst(z)))), gAppInG
+      )
+
+      // f(fst(z)) = g(fst(z))
+      val fEqG = have(f(fst(z)) === g(fst(z))) by Tautology.from(
+        BasicTheorems.appDefinition of (x := fst(z), y := g(fst(z))), fstInDomF, gAppInF
+      )
+
+      // snd(z) = g(fst(z)), so (fst(z), snd(z)) ∈ g
+      val sndEq = have(snd(z) === g(fst(z))) by Congruence.from(fApp, fEqG)
+      have((fst(z), snd(z)) ∈ g) by Congruence.from(gAppInG, sndEq)
+      thenHave(thesis) by Substitute(zIsPair)
+    }
+
+    have(z ∈ g <=> z ∈ (f ↾ dom(g))) by Tautology.from(fwd, bwd)
+    thenHave(thesis) by Extensionality
   }
 
   /**
-   * Theorem --- If `f` and `g` agree on `A`, then `f↾A = g↾A`.
+   * Theorem --- If `f` and `g` agree on `A`, and `A ⊆ dom(f)` and `A ⊆ dom(g)`, then `f↾A = g↾A`.
    */
   val extensionality = Theorem(
-    (function(f), function(g), ∀(x ∈ A, f(x) === g(x))) |- (f ↾ A) === (g ↾ A)
+    (function(f), function(g), A ⊆ dom(f), A ⊆ dom(g), ∀(x ∈ A, f(x) === g(x))) |- (f ↾ A) === (g ↾ A)
   ) {
     assume(function(f))
     assume(function(g))
+    assume(A ⊆ dom(f))
+    assume(A ⊆ dom(g))
     assume(∀(x ∈ A, f(x) === g(x)))
 
-    sorry
+    // Forward: z ∈ (f ↾ A) → z ∈ (g ↾ A)
+    val fwd = have(z ∈ (f ↾ A) |- z ∈ (g ↾ A)) subproof {
+      assume(z ∈ (f ↾ A))
+
+      val zInF = have(z ∈ f) by Tautology.from(membership)
+      val fstInA = have(fst(z) ∈ A) by Tautology.from(membership)
+
+      // z = (fst(z), snd(z)) since function(f) and z ∈ f
+      val zIsPair = have(z === (fst(z), snd(z))) by Tautology.from(BasicTheorems.inversion, zInF)
+      val pairInF = have((fst(z), snd(z)) ∈ f) by Congruence.from(zInF, zIsPair)
+
+      // fst(z) ∈ dom(f)
+      val fstInDomF = have(fst(z) ∈ dom(f)) by Tautology.from(
+        BasicTheorems.domainMembership of (x := fst(z), y := snd(z)), pairInF
+      )
+
+      // f(fst(z)) = snd(z)
+      val fApp = have(f(fst(z)) === snd(z)) by Tautology.from(
+        BasicTheorems.appDefinition of (x := fst(z), y := snd(z)), fstInDomF, pairInF
+      )
+
+      // fst(z) ∈ dom(g) from A ⊆ dom(g)
+      val fstInDomG = have(fst(z) ∈ dom(g)) by Tautology.from(
+        Subset.membership of (x := A, y := dom(g), z := fst(z)), fstInA
+      )
+
+      // f(fst(z)) = g(fst(z))
+      have(∀(x ∈ A, f(x) === g(x))) by Hypothesis
+      thenHave(fst(z) ∈ A ==> (f(fst(z)) === g(fst(z)))) by InstantiateForall(fst(z))
+      val fEqG = thenHave(f(fst(z)) === g(fst(z))) by Tautology.fromLastStep(fstInA)
+
+      // snd(z) = g(fst(z))
+      val sndEq = have(snd(z) === g(fst(z))) by Congruence.from(fApp, fEqG)
+
+      // (fst(z), g(fst(z))) ∈ g
+      val gAppInG = have((fst(z), g(fst(z))) ∈ g) by Tautology.from(
+        BasicTheorems.appDefinition of (f := g, x := fst(z), y := g(fst(z))), fstInDomG
+      )
+
+      // (fst(z), snd(z)) ∈ g
+      have((fst(z), snd(z)) ∈ g) by Congruence.from(gAppInG, sndEq)
+      // z ∈ g
+      thenHave(z ∈ g) by Substitute(zIsPair)
+
+      have(thesis) by Tautology.from(lastStep, fstInA, membership of (f := g))
+    }
+
+    // Backward: z ∈ (g ↾ A) → z ∈ (f ↾ A) (symmetric)
+    val bwd = have(z ∈ (g ↾ A) |- z ∈ (f ↾ A)) subproof {
+      assume(z ∈ (g ↾ A))
+
+      val zInG = have(z ∈ g) by Tautology.from(membership of (f := g))
+      val fstInA = have(fst(z) ∈ A) by Tautology.from(membership of (f := g))
+
+      val zIsPair = have(z === (fst(z), snd(z))) by Tautology.from(BasicTheorems.inversion of (f := g), zInG)
+      val pairInG = have((fst(z), snd(z)) ∈ g) by Congruence.from(zInG, zIsPair)
+
+      val fstInDomG = have(fst(z) ∈ dom(g)) by Tautology.from(
+        BasicTheorems.domainMembership of (f := g, x := fst(z), y := snd(z)), pairInG
+      )
+
+      // g(fst(z)) = snd(z)
+      val gApp = have(g(fst(z)) === snd(z)) by Tautology.from(
+        BasicTheorems.appDefinition of (f := g, x := fst(z), y := snd(z)), fstInDomG, pairInG
+      )
+
+      // fst(z) ∈ dom(f) from A ⊆ dom(f)
+      val fstInDomF = have(fst(z) ∈ dom(f)) by Tautology.from(
+        Subset.membership of (x := A, y := dom(f), z := fst(z)), fstInA
+      )
+
+      // f(fst(z)) = g(fst(z))
+      have(∀(x ∈ A, f(x) === g(x))) by Hypothesis
+      thenHave(fst(z) ∈ A ==> (f(fst(z)) === g(fst(z)))) by InstantiateForall(fst(z))
+      val fEqG = thenHave(f(fst(z)) === g(fst(z))) by Tautology.fromLastStep(fstInA)
+
+      // snd(z) = f(fst(z))
+      val sndEq = have(snd(z) === f(fst(z))) by Congruence.from(gApp, fEqG)
+
+      // (fst(z), f(fst(z))) ∈ f
+      val fAppInF = have((fst(z), f(fst(z))) ∈ f) by Tautology.from(
+        BasicTheorems.appDefinition of (x := fst(z), y := f(fst(z))), fstInDomF
+      )
+
+      // (fst(z), snd(z)) ∈ f
+      have((fst(z), snd(z)) ∈ f) by Congruence.from(fAppInF, sndEq)
+      // z ∈ f
+      thenHave(z ∈ f) by Substitute(zIsPair)
+
+      have(thesis) by Tautology.from(lastStep, fstInA, membership)
+    }
+
+    have(z ∈ (f ↾ A) <=> z ∈ (g ↾ A)) by Tautology.from(fwd, bwd)
+    thenHave(thesis) by Extensionality
   }
 }