diff --git a/src/main/scala/dev/A.scala b/src/main/scala/dev/A.scala
deleted file mode 100644
index e9ddcd2468061333c9b6cd35398476047a1ceaca..0000000000000000000000000000000000000000
--- a/src/main/scala/dev/A.scala
+++ /dev/null
@@ -1,5 +0,0 @@
-package dev
-
-trait A extends WithMain {}
-
-object A extends A
diff --git a/src/main/scala/dev/WithMain.scala b/src/main/scala/dev/WithMain.scala
deleted file mode 100644
index 72454a97945a417a6c3f4015040c5dee6ff8037f..0000000000000000000000000000000000000000
--- a/src/main/scala/dev/WithMain.scala
+++ /dev/null
@@ -1,8 +0,0 @@
-package dev
-
-abstract class WithMain {
- def main(args: Array[String]): Unit = {
- println("Bonjour")
- }
-
-}
diff --git a/src/main/scala/lisa/kernel/proof/Judgement.scala b/src/main/scala/lisa/kernel/proof/Judgement.scala
index 56137f419ed9924e3593bc26f538c0c07ff42c2a..b0b86e27eeda5aa5d6ecba286a23f4572c32a388 100644
--- a/src/main/scala/lisa/kernel/proof/Judgement.scala
+++ b/src/main/scala/lisa/kernel/proof/Judgement.scala
@@ -39,7 +39,7 @@ object SCProofCheckerJudgement {
/**
* The judgement (or verdict) of a running theory.
*/
-sealed abstract class RunningTheoryJudgement[J <: RunningTheory#Justification] {
+sealed abstract class RunningTheoryJudgement[+J <: RunningTheory#Justification] {
import RunningTheoryJudgement.*
/**
diff --git a/src/main/scala/lisa/kernel/proof/RunningTheory.scala b/src/main/scala/lisa/kernel/proof/RunningTheory.scala
index 95280f5ec7e38aba4fc1775e5c10b5b3993a6885..9d208036c13622a87b88528806f6d579a5ebe59b 100644
--- a/src/main/scala/lisa/kernel/proof/RunningTheory.scala
+++ b/src/main/scala/lisa/kernel/proof/RunningTheory.scala
@@ -45,10 +45,9 @@ class RunningTheory {
* Define a predicate symbol as a shortcut for a formula. Example : P(x,y) := ∃!z. (x=y+z)
*
* @param label The name and arity of the new symbol
- * @param args The variables representing the arguments of the predicate in the formula phi.
- * @param phi The formula defining the predicate.
+ * @param expression The formula, depending on terms, that define the symbol.
*/
- final case class PredicateDefinition private[RunningTheory] (label: ConstantPredicateLabel, args: Seq[VariableLabel], phi: Formula) extends Definition
+ final case class PredicateDefinition private[RunningTheory] (label: ConstantPredicateLabel, expression: LambdaTermFormula) extends Definition
/**
* Define a function symbol as the unique element that has some property. The existence and uniqueness
@@ -56,11 +55,10 @@ class RunningTheory {
* f(x,y) := the "z" s.t. x=y+z
*
* @param label The name and arity of the new symbol
- * @param args The variables representing the arguments of the predicate in the formula phi.
* @param out The variable representing the result of the function in phi
- * @param phi The formula defining the function.
+ * @param expression The formula, with term parameters, defining the function.
*/
- final case class FunctionDefinition private[RunningTheory] (label: ConstantFunctionLabel, args: Seq[VariableLabel], out: VariableLabel, phi: Formula) extends Definition
+ final case class FunctionDefinition private[RunningTheory] (label: ConstantFunctionLabel, out: VariableLabel, expression: LambdaTermFormula) extends Definition
private[proof] val theoryAxioms: mMap[String, Axiom] = mMap.empty
private[proof] val theorems: mMap[String, Theorem] = mMap.empty
@@ -118,11 +116,12 @@ class RunningTheory {
* @param phi The formula defining the predicate.
* @return A definition object if the parameters are correct,
*/
- def makePredicateDefinition(label: ConstantPredicateLabel, args: Seq[VariableLabel], phi: Formula): RunningTheoryJudgement[this.PredicateDefinition] = {
- if (belongsToTheory(phi))
+ def makePredicateDefinition(label: ConstantPredicateLabel, expression:LambdaTermFormula): RunningTheoryJudgement[this.PredicateDefinition] = {
+ val LambdaTermFormula(vars, body) = expression
+ if (belongsToTheory(body))
if (isAvailable(label))
- if (phi.freeVariables.subsetOf(args.toSet) && phi.schematicFunctions.isEmpty && phi.schematicPredicates.isEmpty)
- val newDef = PredicateDefinition(label, args, phi)
+ if (body.freeVariables.isEmpty && body.schematicFunctions.subsetOf(vars.toSet) && body.schematicPredicates.isEmpty)
+ val newDef = PredicateDefinition(label, expression)
predDefinitions.update(label, Some(newDef))
knownSymbols.update(label.id, label)
RunningTheoryJudgement.ValidJustification(newDef)
@@ -150,23 +149,22 @@ class RunningTheory {
proof: SCProof,
justifications: Seq[Justification],
label: ConstantFunctionLabel,
- args: Seq[VariableLabel],
out: VariableLabel,
- phi: Formula
+ expression: LambdaTermFormula
): RunningTheoryJudgement[this.FunctionDefinition] = {
- if (belongsToTheory(phi))
+ val LambdaTermFormula(vars, body) = expression
+ if (belongsToTheory(body))
if (isAvailable(label))
- if (phi.freeVariables.subsetOf(args.toSet + out) && phi.schematicFunctions.isEmpty && phi.schematicPredicates.isEmpty)
+ if (body.freeVariables.subsetOf(Set(out)) && body.schematicFunctions.subsetOf(vars.toSet) && body.schematicPredicates.isEmpty)
if (proof.imports.forall(i => justifications.exists(j => isSameSequent(i, sequentFromJustification(j)))))
val r = SCProofChecker.checkSCProof(proof)
r match {
case SCProofCheckerJudgement.SCValidProof(_) =>
proof.conclusion match {
case Sequent(l, r) if l.isEmpty && r.size == 1 =>
- val subst = bindAll(Forall, args, BinderFormula(ExistsOne, out, phi))
- val subst2 = bindAll(Forall, args.reverse, BinderFormula(ExistsOne, out, phi))
- if (isSame(r.head, subst) || isSame(r.head, subst2)) {
- val newDef = FunctionDefinition(label, args, out, phi)
+ val subst = BinderFormula(ExistsOne, out, body)
+ if (isSame(r.head, subst)) {
+ val newDef = FunctionDefinition(label, out, expression)
funDefinitions.update(label, Some(newDef))
knownSymbols.update(label.id, label)
RunningTheoryJudgement.ValidJustification(newDef)
@@ -181,30 +179,18 @@ class RunningTheory {
else InvalidJustification("All symbols in the conclusion of the proof must belong to the theory. You need to add missing symbols to the theory.", None)
}
- private def sequentFromJustification(j: Justification): Sequent = j match {
+ def sequentFromJustification(j: Justification): Sequent = j match {
case Theorem(name, proposition) => proposition
case Axiom(name, ax) => Sequent(Set.empty, Set(ax))
- case PredicateDefinition(label, args, phi) =>
- val inner = ConnectorFormula(Iff, Seq(PredicateFormula(label, args.map(VariableTerm.apply)), phi))
- Sequent(Set(), Set(bindAll(Forall, args, inner)))
- case FunctionDefinition(label, args, out, phi) =>
- val inner = BinderFormula(
- Forall,
- out,
- ConnectorFormula(
- Iff,
- Seq(
- PredicateFormula(equality, Seq(FunctionTerm(label, args.map(VariableTerm.apply)), VariableTerm(out))),
- phi
- )
- )
- )
- Sequent(
- Set(),
- Set(
- bindAll(Forall, args, inner)
- )
- )
+ case PredicateDefinition(label, LambdaTermFormula(vars, body)) =>
+ val inner = ConnectorFormula(Iff, Seq(PredicateFormula(label, vars.map(FunctionTerm(_, Seq()))), body))
+ Sequent(Set(), Set(inner))
+ case FunctionDefinition(label, out, LambdaTermFormula(vars, body)) =>
+ val inner = BinderFormula(Forall, out, ConnectorFormula(Iff, Seq(
+ PredicateFormula(equality, Seq(FunctionTerm(label, vars.map(FunctionTerm.apply(_, Seq()))), VariableTerm(out))),
+ body
+ )))
+ Sequent(Set(), Set(inner))
}
diff --git a/src/main/scala/lisa/kernel/proof/SCProof.scala b/src/main/scala/lisa/kernel/proof/SCProof.scala
index 65c40f8de93d2ecd1c4b20719d49e506ba8afc94..244c795e40b3d054de9021ddfabfbec1bd34f7c1 100644
--- a/src/main/scala/lisa/kernel/proof/SCProof.scala
+++ b/src/main/scala/lisa/kernel/proof/SCProof.scala
@@ -65,8 +65,8 @@ case class SCProof(steps: IndexedSeq[SCProofStep], imports: IndexedSeq[Sequent]
* Can be undefined if the proof is empty.
*/
def conclusion: Sequent = {
- if (steps.isEmpty) throw new NoSuchElementException("conclusion of an empty proof")
- this(length - 1).bot
+ if (steps.isEmpty && imports.isEmpty) throw new NoSuchElementException("conclusion of an empty proof")
+ this.getSequent(length - 1)
}
/**
diff --git a/src/main/scala/proven/DSetTheory/Part1.scala b/src/main/scala/proven/DSetTheory/Part1.scala
deleted file mode 100644
index 8b69a2b4f0bd8cee213fe22b59482e6901e44ab4..0000000000000000000000000000000000000000
--- a/src/main/scala/proven/DSetTheory/Part1.scala
+++ /dev/null
@@ -1,635 +0,0 @@
-package proven.DSetTheory
-
-import lisa.kernel.fol.FOL
-import lisa.kernel.fol.FOL.*
-import lisa.kernel.proof.SCProof
-import lisa.kernel.proof.SCProofChecker
-import lisa.kernel.proof.SequentCalculus.*
-import lisa.settheory.AxiomaticSetTheory
-import lisa.settheory.AxiomaticSetTheory.*
-import proven.ElementsOfSetTheory.oPair
-import proven.ElementsOfSetTheory.orderedPairDefinition
-import proven.tactics.Destructors.*
-import proven.tactics.ProofTactics.*
-import utilities.Helpers.{_, given}
-import utilities.Printer
-import utilities.Printer.prettyFormula
-import utilities.Printer.prettySCProof
-import utilities.Printer.prettySequent
-
-import scala.collection.immutable
-import scala.collection.immutable.SortedSet
-trait Part1 {
- val theory = AxiomaticSetTheory.runningSetTheory
- def axiom(f: Formula): theory.Axiom = theory.getAxiom(f).get
-
- 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)
-
- val sPhi = SchematicPredicateLabel("P", 2)
- val sPsi = SchematicPredicateLabel("P", 3)
-
- 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)
- // val s3 = LeftExists(exists(y1, forall(x1, in(x,y) <=> !in(x, x))) |- (), 2, forall(x1, in(x,y) <=> !in(x, x)), y1)
- // val s4 = Rewrite(() |- !exists(y1, forall(x1, in(x1,y1) <=> !in(x1, x1))), 3)
- SCProof(s0, s1, s2)
- }
- 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)))))
- val i1 = () |- comprehensionSchema
- val i2 = russelParadox.conclusion // forall(x1, in(x1,y) <=> !in(x1, x1)) |- ()
- val p0: SCProofStep = InstPredSchema(() |- forall(z1, exists(y1, forall(x1, in(x1, y1) <=> (in(x1, z1) /\ !in(x1, x1))))), -1, Map(sPhi -> LambdaTermFormula(Seq(x, z), !in(x(), x()))))
- val s0 = SCSubproof(instantiateForall(SCProof(IndexedSeq(p0), IndexedSeq(i1)), z), Seq(-1)) // exists(y1, forall(x1, in(x1,y1) <=> (in(x1,z1) /\ !in(x1, x1))))
- val s1 = hypothesis(in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1))) // in(x,y) <=> (in(x,z) /\ in(x, x)) |- in(x,y) <=> (in(x,z) /\ in(x, x))
- val s2 = RightSubstIff(
- (in(x1, z) <=> And(), in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1))) |- in(x1, y1) <=> (And() /\ !in(x1, x1)),
- 1,
- List((in(x1, z), And())),
- LambdaFormulaFormula(Seq(h), in(x1, y1) <=> (h() /\ !in(x1, x1)))
- ) // in(x1,y1) <=> (in(x1,z1) /\ in(x1, x1)) |- in(x,y) <=> (And() /\ in(x1, x1))
- val s3 = Rewrite((in(x1, z), in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1))) |- in(x1, y1) <=> !in(x1, x1), 2)
- val s4 = LeftForall((forall(x1, in(x1, z)), in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1))) |- in(x1, y1) <=> !in(x1, x1), 3, in(x1, z), x1, x1)
- val s5 = LeftForall((forall(x1, in(x1, z)), forall(x1, in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1)))) |- in(x1, y1) <=> !in(x1, x1), 4, in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1)), x1, x1)
- val s6 = RightForall((forall(x1, in(x1, z)), forall(x1, in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1)))) |- forall(x1, in(x1, y1) <=> !in(x1, x1)), 5, in(x1, y1) <=> !in(x1, x1), x1)
- val s7 = InstFunSchema(forall(x1, in(x1, y1) <=> !in(x1, x1)) |- (), -2, Map(SchematicFunctionLabel("y", 0) -> LambdaTermTerm(Nil, y1)))
- val s8 = Cut((forall(x1, in(x1, z)), forall(x1, in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1)))) |- (), 6, 7, forall(x1, in(x1, y1) <=> !in(x1, x1)))
- val s9 = LeftExists((forall(x1, in(x1, z)), exists(y1, forall(x1, in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1))))) |- (), 8, forall(x1, in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1))), y1)
- 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))
- }
- 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")
- val b = VariableLabel("b")
- val x = VariableLabel("x")
- val y = VariableLabel("y")
- val z = VariableLabel("z")
- val a1 = SchematicFunctionLabel("a", 0)
- val b1 = SchematicFunctionLabel("b", 0)
- val x1 = SchematicFunctionLabel("x", 0)
- val y1 = SchematicFunctionLabel("y", 0)
- val z1 = SchematicFunctionLabel("z", 0)
- val A = SchematicFunctionLabel("A", 0)()
- val X = VariableLabel("X")
- val B = VariableLabel("B")
- val B1 = VariableLabel("B1")
- val phi = SchematicPredicateLabel("phi", 2)
- val sPhi = SchematicPredicateLabel("P", 2)
- val sPsi = SchematicPredicateLabel("P", 3)
-
- val H = existsOne(x, phi(x, a))
- val H1 = forall(a, in(a, A) ==> H)
- val s0 = hypothesis(H) // () |- existsOne(x, phi(x, a)))
- val s1 = Weakening((H, in(a, A)) |- existsOne(x, phi(x, a)), 0)
- val s2 = Rewrite((H) |- in(a, A) ==> existsOne(x, phi(x, a)), 1)
- // val s3 = RightForall((H) |- forall(a, in(a, A) ==> existsOne(x, phi(x, a))), 2, in(a, A) ==> existsOne(x, phi(x, a)), a) // () |- ∀a∈A. ∃!x. phi(x, a)
- val s3 = hypothesis(H1)
- val i1 = () |- replacementSchema
- val p0 = InstPredSchema(
- () |- instantiatePredicateSchemas(replacementSchema, Map(sPsi -> LambdaTermFormula(Seq(y1, a1, x1), phi(x1, a1)))),
- -1,
- Map(sPsi -> LambdaTermFormula(Seq(y1, a1, x1), phi(x1, a1)))
- )
- val p1 = instantiateForall(SCProof(Vector(p0), Vector(i1)), A)
- val s4 = SCSubproof(p1, Seq(-1)) //
- val s5 = Rewrite(s3.bot.right.head |- exists(B, forall(x, in(x, A) ==> exists(y, in(y, B) /\ (phi(y, x))))), 4)
- val s6 = Cut((H1) |- exists(B, forall(x, in(x, A) ==> exists(y, in(y, B) /\ (phi(y, x))))), 3, 5, s3.bot.right.head) // ⊢ ∃B. ∀x. (x ∈ A) ⇒ ∃y. (y ∈ B) ∧ (y = (x, b))
-
- val i2 = () |- comprehensionSchema // forall(z, exists(y, forall(x, in(x,y) <=> (in(x,z) /\ sPhi(x,z)))))
- val q0 = InstPredSchema(
- () |- instantiatePredicateSchemas(comprehensionSchema, Map(sPhi -> LambdaTermFormula(Seq(x1, z1), exists(a, in(a, A) /\ phi(x1, a))))),
- -1,
- Map(sPhi -> LambdaTermFormula(Seq(x1, z1), exists(a, in(a, A) /\ phi(x1, a))))
- )
- val q1 = instantiateForall(SCProof(Vector(q0), Vector(i2)), B)
- val s7 = SCSubproof(q1, Seq(-2)) // ∃y. ∀x. (x ∈ y) ↔ (x ∈ B) ∧ ∃a. a ∈ A /\ x = (a, b) := exists(y, F(y) )
- SCProof(Vector(s0, s1, s2, s3, s4, s5, s6, s7), Vector(i1, i2))
- val s8 = SCSubproof({
- val y1 = VariableLabel("y1")
- val f = SchematicFunctionLabel("f", 0)
- /*
- val s0 = hypothesis(in(y, B)) // redgoal (y ∈ B) |- (y ∈ B) TRUE
- val s1 = RightSubstEq((in(y, B), y===x) |- in(x, B), 0, x, y, in(f(), B), f)// redgoal (y ∈ B), (y = x) |- (x ∈ B)
- val s2 = LeftSubstEq((phi(x, a), in(y, B), phi(y, a)) |- in(x, B), 1, x, oPair(a,b), y===f(), f )// redGoal x = (a, b), (y ∈ B), (y = (a, b)) |- (x ∈ B)
- val s3 = Rewrite((phi(x, a), in(y, B) /\ (phi(y, a))) |- in(x, B), 2)
- val s4 = LeftExists((phi(x, a), exists(y, in(y, B) /\ (phi(y, a)))) |- in(x, B), 3, in(y, B) /\ (phi(y, a)), y)// redGoal x = (a, b), ∃y. (y ∈ B) ∧ (y = (a, b)) |- (x ∈ B)
- val s5 = Rewrite( (phi(x, a), And()==> exists(y, in(y, B) /\ (phi(y, a)))) |- in(x, B), 4) //redGoal (T) ⇒ ∃y. y ∈ B ∧ y = (a, b), x = (a, b) |- (x ∈ B)
- val s6 = LeftSubstIff(Set(phi(x, a), in(a, A)==> exists(y, in(y, B) /\ (phi(y, a))), And()<=>in(a, A)) |- in(x, B),5, And(), in(a, A), h()==> exists(y, in(y, B) /\ (phi(y, a))), h) //redGoal (a ∈ A) ⇒ ∃y. y ∈ B ∧ y = (a, b), a ∈ A <=> T, x = (a, b) |- (x ∈ B)
- val s7 = Rewrite(Set(in(a, A)==> exists(y, in(y, B) /\ (phi(y, a))), in(a, A) /\ (phi(x, a))) |- in(x, B), 6) //redGoal (a ∈ A) ⇒ ∃y. y ∈ B ∧ y = (a, b), a ∈ A ∧ x = (a, b) |- (x ∈ B)
- val s8 = LeftForall((forall(a, in(a, A)==> exists(y, in(y, B) /\ (phi(y, a)))), in(a, A) /\ (phi(x, a)))|- in(x, B), 7, in(a, A)==> exists(y, in(y, B) /\ (phi(y, a))), a, a) //redGoal ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ y = (a, b), a ∈ A ∧ x = (a, b) |- (x ∈ B)
- val s9 = LeftExists((forall(a, in(a, A)==> exists(y, in(y, B) /\ (phi(y, a)))), exists(a, in(a, A) /\ (phi(x, a))))|- in(x, B), 8, in(a, A) /\ (phi(x, a)), a) //∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ y = (a, b), ∃a. a ∈ A ∧ x = (a, b) |- (x ∈ B)
- SCProof(Vector(s0, s1, s2, s3, s4, s5, s6, s7, s8, s9))
- */
-
- val s0 = hypothesis(in(y1, B))
- val s1 = RightSubstEq((in(y1, B), x === y1) |- in(x, B), 0, List((x, y1)), LambdaTermFormula(Seq(f), in(f(), B)))
- val s2 = LeftSubstIff(Set(in(y1, B), (x === y1) <=> phi(x, a), phi(x, a)) |- in(x, B), 1, List(((x === y1), phi(x, a))), LambdaFormulaFormula(Seq(h), h()))
- val s3 = LeftSubstEq(Set(y === y1, in(y1, B), (x === y) <=> phi(x, a), phi(x, a)) |- in(x, B), 2, List((y, y1)), LambdaTermFormula(Seq(f), (x === f()) <=> phi(x, a)))
- val s4 = LeftSubstIff(Set((y === y1) <=> phi(y1, a), phi(y1, a), in(y1, B), (x === y) <=> phi(x, a), phi(x, a)) |- in(x, B), 3, List((phi(y1, a), y1 === y)), LambdaFormulaFormula(Seq(h), h()))
- val s5 = LeftForall(Set(forall(x, (y === x) <=> phi(x, a)), phi(y1, a), in(y1, B), (x === y) <=> phi(x, a), phi(x, a)) |- in(x, B), 4, (y === x) <=> phi(x, a), x, y1)
- val s6 = LeftForall(Set(forall(x, (y === x) <=> phi(x, a)), phi(y1, a), in(y1, B), phi(x, a)) |- in(x, B), 5, (x === y) <=> phi(x, a), x, x)
- val s7 = LeftExists(Set(exists(y, forall(x, (y === x) <=> phi(x, a))), phi(y1, a), in(y1, B), phi(x, a)) |- in(x, B), 6, forall(x, (y === x) <=> phi(x, a)), y)
- val s8 = Rewrite(Set(exists(y, forall(x, (y === x) <=> phi(x, a))), phi(y1, a) /\ in(y1, B), phi(x, a)) |- in(x, B), 7)
- val s9 = LeftExists(Set(exists(y, forall(x, (y === x) <=> phi(x, a))), exists(y1, phi(y1, a) /\ in(y1, B)), phi(x, a)) |- in(x, B), 8, phi(y1, a) /\ in(y1, B), y1)
- val s10 = Rewrite(Set(exists(y, forall(x, (y === x) <=> phi(x, a))), And() ==> exists(y, phi(y, a) /\ in(y, B)), phi(x, a)) |- in(x, B), 9)
- val s11 = LeftSubstIff(
- Set(exists(y, forall(x, (y === x) <=> phi(x, a))), in(a, A) ==> exists(y, phi(y, a) /\ in(y, B)), phi(x, a), in(a, A)) |- in(x, B),
- 10,
- List((And(), in(a, A))),
- LambdaFormulaFormula(Seq(h), h() ==> exists(y, phi(y, a) /\ in(y, B)))
- )
- val s12 = LeftForall(
- Set(exists(y, forall(x, (y === x) <=> phi(x, a))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), phi(x, a), in(a, A)) |- in(x, B),
- 11,
- in(a, A) ==> exists(y, phi(y, a) /\ in(y, B)),
- a,
- a
- )
- val s13 = LeftSubstIff(
- Set(in(a, A) ==> exists(y, forall(x, (y === x) <=> phi(x, a))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), phi(x, a), in(a, A)) |- in(x, B),
- 12,
- List((And(), in(a, A))),
- LambdaFormulaFormula(Seq(h), h() ==> exists(y, forall(x, (y === x) <=> phi(x, a))))
- )
- val s14 = LeftForall(
- Set(forall(a, in(a, A) ==> exists(y, forall(x, (y === x) <=> phi(x, a)))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), phi(x, a), in(a, A)) |- in(x, B),
- 13,
- in(a, A) ==> exists(y, forall(x, (y === x) <=> phi(x, a))),
- a,
- a
- )
- val s15 = Rewrite(Set(forall(a, in(a, A) ==> exists(y, forall(x, (y === x) <=> phi(x, a)))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), phi(x, a) /\ in(a, A)) |- in(x, B), 14)
- val s16 = LeftExists(
- Set(forall(a, in(a, A) ==> exists(y, forall(x, (y === x) <=> phi(x, a)))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), exists(a, phi(x, a) /\ in(a, A))) |- in(x, B),
- 15,
- phi(x, a) /\ in(a, A),
- a
- )
- val truc = forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B)))
- val s17 = Rewrite(Set(forall(a, in(a, A) ==> existsOne(x, phi(x, a))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), exists(a, phi(x, a) /\ in(a, A))) |- in(x, B), 16)
- SCProof(Vector(s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, s17))
- // goal H, ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), ∃a. a ∈ A ∧ phi(x, a) |- (x ∈ B)
- // redGoal ∀a.(a ∈ A) => ∃!x. phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), ∃a. a ∈ A ∧ phi(x, a) |- (x ∈ B) s17
- // redGoal ∀a.(a ∈ A) => ∃y. ∀x. (x=y) ↔ phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), ∃a. a ∈ A ∧ phi(x, a) |- (x ∈ B) s16
- // redGoal ∀a.(a ∈ A) => ∃y. ∀x. (x=y) ↔ phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A ∧ phi(x, a) |- (x ∈ B) s15
- // redGoal ∀a.(a ∈ A) => ∃y. ∀x. (x=y) ↔ phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A, phi(x, a) |- (x ∈ B) s14
- // redGoal (a ∈ A) => ∃y. ∀x. (x=y) ↔ phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A, phi(x, a) |- (x ∈ B) s13
- // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A, phi(x, a) |- (x ∈ B) s12
- // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A, phi(x, a) |- (x ∈ B) s11
- // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A <=> T, phi(x, a) |- (x ∈ B) s11
- // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), T ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A <=> T, phi(x, a) |- (x ∈ B) s10
- // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), ∃y1. y1 ∈ B ∧ phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s9
- // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), y1 ∈ B ∧ phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s8
- // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), y1 ∈ B, phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s7
- // redGoal ∀x. (x=y) ↔ phi(x, a), y1 ∈ B, phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s6
- // redGoal (x=y) ↔ phi(x, a), ∀x. (x=y) ↔ phi(x, a), y1 ∈ B, phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s5
- // redGoal (x=y) ↔ phi(x, a), (y1=y) ↔ phi(y1, a), y1 ∈ B, phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s4
- // redGoal (x=y) ↔ phi(x, a), (y1=y) ↔ phi(y1, a), y1 ∈ B, (y1=y), a ∈ A, phi(x, a) |- (x ∈ B) s3
- // redGoal (x=y1) ↔ phi(x, a), (y1=y) ↔ phi(y1, a), y1 ∈ B, (y1=y), a ∈ A, phi(x, a) |- (x ∈ B) s2
- // redGoal (x=y1) ↔ phi(x, a), (y1=y) ↔ phi(y1, a), y1 ∈ B, (y1=y), a ∈ A, x=y1 |- (x ∈ B) s1
- // redGoal (x=y1) ↔ phi(x, a), (y1=y) ↔ phi(y1, a), y1 ∈ B, (y1=y), a ∈ A, x=y1 |- (y1 ∈ B) s0
-
- }) // H, ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), ∃a. a ∈ A ∧ phi(x, a) |- (x ∈ B)
-
- val G = forall(a, in(a, A) ==> exists(y, in(y, B) /\ (phi(y, a))))
- val F = forall(x, iff(in(x, B1), in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a)))))
- val s9 = SCSubproof({
- val p0 = instantiateForall(SCProof(hypothesis(F)), x)
- val left = in(x, B1)
- val right = in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a)))
- val p1 = p0.withNewSteps(Vector(Rewrite(F |- (left ==> right) /\ (right ==> left), p0.length - 1)))
- val p2 = destructRightAnd(p1, (right ==> left), (left ==> right)) // F |- in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a))) => in(x, B1)
- val p3 = p2.withNewSteps(Vector(Rewrite(Set(F, in(x, B), exists(a, in(a, A) /\ (phi(x, a)))) |- in(x, B1), p2.length - 1)))
- p3
- }) // have F, (x ∈ B), ∃a. a ∈ A ∧ x = (a, b) |- (x ∈ B1)
- val s10 = Cut(Set(F, G, H1, exists(a, in(a, A) /\ (phi(x, a)))) |- in(x, B1), 8, 9, in(x, B)) // redGoal F, ∃a. a ∈ A ∧ x = (a, b), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ y = (a, b) |- (x ∈ B1)
- val s11 = Rewrite(Set(H1, G, F) |- exists(a, in(a, A) /\ (phi(x, a))) ==> in(x, B1), 10) // F |- ∃a. a ∈ A ∧ x = (a, b) => (x ∈ B1) --- half
- val s12 = SCSubproof({
- val p0 = instantiateForall(SCProof(hypothesis(F)), x)
- val left = in(x, B1)
- val right = in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a)))
- val p1 = p0.withNewSteps(Vector(Rewrite(F |- (left ==> right) /\ (right ==> left), p0.length - 1)))
- val p2 = destructRightAnd(p1, (left ==> right), (right ==> left)) // F |- in(x, B1) => in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a))) =>
- val p3 = p2.withNewSteps(Vector(Rewrite(Set(F, in(x, B1)) |- exists(a, in(a, A) /\ (phi(x, a))) /\ in(x, B), p2.length - 1)))
- val p4 = destructRightAnd(p3, exists(a, in(a, A) /\ (phi(x, a))), in(x, B))
- val p5 = p4.withNewSteps(Vector(Rewrite(F |- in(x, B1) ==> exists(a, in(a, A) /\ (phi(x, a))), p4.length - 1)))
- p5
- }) // have F |- (x ∈ B1) ⇒ ∃a. a ∈ A ∧ x = (a, b) --- other half
- val s13 = RightIff((H1, G, F) |- in(x, B1) <=> exists(a, in(a, A) /\ (phi(x, a))), 11, 12, in(x, B1), exists(a, in(a, A) /\ (phi(x, a)))) // have F |- (x ∈ B1) <=> ∃a. a ∈ A ∧ x = (a, b)
- val s14 =
- RightForall((H1, G, F) |- forall(x, in(x, B1) <=> exists(a, in(a, A) /\ (phi(x, a)))), 13, in(x, B1) <=> exists(a, in(a, A) /\ (phi(x, a))), x) // G, F |- ∀x. (x ∈ B1) <=> ∃a. a ∈ A ∧ x = (a, b)
-
- val i3 = () |- extensionalityAxiom
- val s15 = SCSubproof(
- {
- val i1 = s13.bot // G, F |- (x ∈ B1) <=> ∃a. a ∈ A ∧ x = (a, b)
- val i2 = () |- extensionalityAxiom
- val t0 = RightSubstIff(
- Set(H1, G, F, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))) |- in(x, X) <=> in(x, B1),
- -1,
- List((in(x, X), exists(a, in(a, A) /\ (phi(x, a))))),
- LambdaFormulaFormula(Seq(h), h() <=> in(x, B1))
- ) // redGoal2 F, (z ∈ X) <=> ∃a. a ∈ A ∧ z = (a, b) |- (z ∈ X) <=> (z ∈ B1)
- val t1 = LeftForall(
- Set(H1, G, F, forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))) |- in(x, X) <=> in(x, B1),
- 0,
- in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))),
- x,
- x
- ) // redGoal2 F, [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] |- (z ∈ X) <=> (z ∈ B1)
- val t2 = RightForall(t1.bot.left |- forall(x, in(x, X) <=> in(x, B1)), 1, in(x, X) <=> in(x, B1), x) // redGoal2 F, [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] |- ∀z. (z ∈ X) <=> (z ∈ B1)
- val t3 =
- SCSubproof(instantiateForall(SCProof(Vector(Rewrite(() |- extensionalityAxiom, -1)), Vector(() |- extensionalityAxiom)), X, B1), Vector(-2)) // (∀z. (z ∈ X) <=> (z ∈ B1)) <=> (X === B1)))
- val t4 = RightSubstIff(
- t1.bot.left ++ t3.bot.right |- X === B1,
- 2,
- List((X === B1, forall(z, in(z, X) <=> in(z, B1)))),
- LambdaFormulaFormula(Seq(h), h())
- ) // redGoal2 F, [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)], (∀z. (z ∈ X) <=> (z ∈ B1)) <=> (X === B1))) |- X=B1
- val t5 = Cut(t1.bot.left |- X === B1, 3, 4, t3.bot.right.head) // redGoal2 F, [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] |- X=B1
- val t6 = Rewrite(Set(H1, G, F) |- forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))) ==> (X === B1), 5) // F |- [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] ==> X=B1
- val i3 = s14.bot // F |- ∀x. (x ∈ B1) <=> ∃a. a ∈ A ∧ x = (a, b)
- val t7 = RightSubstEq(
- Set(H1, G, F, X === B1) |- forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))),
- -3,
- List((X, B1)),
- LambdaTermFormula(Seq(f), forall(x, in(x, f()) <=> exists(a, in(a, A) /\ phi(x, a))))
- ) // redGoal1 F, X=B1 |- [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
- val t8 = Rewrite(
- Set(H1, G, F) |- X === B1 ==> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))),
- 7
- ) // redGoal1 F |- X=B1 ==> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] -------second half with t6
- val t9 = RightIff(
- Set(H1, G, F) |- (X === B1) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))),
- 6,
- 8,
- X === B1,
- forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))
- ) // goal F |- X=B1 <=> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
-
- SCProof(Vector(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9), Vector(i1, i2, i3))
- },
- Vector(13, -3, 14)
- ) // goal F |- X=B1 <=> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
- val s16 = RightForall(
- (H1, G, F) |- forall(X, (X === B1) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))),
- 15,
- (X === B1) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))),
- X
- ) // goal F |- ∀X. X=B1 <=> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
- val s17 = RightExists(
- (H1, G, F) |- exists(y, forall(X, (X === y) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))))),
- 16,
- forall(X, (X === y) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))),
- y,
- B1
- )
- val s18 = LeftExists((exists(B1, F), G, H1) |- s17.bot.right, 17, F, B1) // ∃B1. F |- ∃B1. ∀X. X=B1 <=> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
- val s19 = Rewrite(s18.bot.left |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))), 18) // ∃B1. F |- ∃!X. [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
- val s20 = Cut((G, H1) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))), 7, 19, exists(B1, F))
- val s21 = LeftExists((H1, exists(B, G)) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))), 20, G, B)
- val s22 = Cut(H1 |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ phi(x, a)))), 6, 21, exists(B, G))
- 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))
- }
- 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)
- */
- val lemma1: SCProof = {
- val a = VariableLabel("a")
- val b = VariableLabel("b")
- val x = VariableLabel("x")
- val x1 = VariableLabel("x1")
- val y = VariableLabel("y")
- val z = VariableLabel("z")
- val a_ = SchematicFunctionLabel("a", 0)
- val b_ = SchematicFunctionLabel("b", 0)
- val x_ = SchematicFunctionLabel("x", 0)
- val x1_ = SchematicFunctionLabel("x1", 0)
- val y_ = SchematicFunctionLabel("y", 0)
- val z_ = SchematicFunctionLabel("z", 0)
- val A = SchematicFunctionLabel("A", 0)()
- val X = VariableLabel("X")
- val B = SchematicFunctionLabel("B", 0)()
- val B1 = VariableLabel("B1")
- val phi = SchematicPredicateLabel("phi", 2)
- val psi = SchematicPredicateLabel("psi", 3)
- val H = existsOne(x, phi(x, a))
- val H1 = forall(a, in(a, A) ==> H)
- val i1 = thmMapFunctional.conclusion
- val H2 = instantiatePredicateSchemas(H1, Map(phi -> LambdaTermFormula(Seq(x_, a_), psi(x_, a_, b))))
- val s0 = InstPredSchema((H2) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), -1, Map(phi -> LambdaTermFormula(Seq(x_, a_), psi(x_, a_, b))))
- val s1 = Weakening((H2, in(b, B)) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), 0)
- val s2 =
- LeftSubstIff((in(b, B) ==> H2, in(b, B)) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), 1, List((in(b, B), And())), LambdaFormulaFormula(Seq(h), h() ==> H2))
- val s3 = LeftForall((forall(b, in(b, B) ==> H2), in(b, B)) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), 2, in(b, B) ==> H2, b, b)
- val s4 = Rewrite(forall(b, in(b, B) ==> H2) |- in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), 3)
- val s5 = RightForall(
- forall(b, in(b, B) ==> H2) |- forall(b, in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b))))),
- 4,
- in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))),
- b
- )
- val s6 = InstFunSchema(
- forall(b, in(b, B) ==> existsOne(X, phi(X, b))) |- instantiateFunctionSchemas(i1.right.head, Map(SchematicFunctionLabel("A", 0) -> LambdaTermTerm(Nil, B))),
- -1,
- Map(SchematicFunctionLabel("A", 0) -> LambdaTermTerm(Nil, B))
- )
- val s7 = InstPredSchema(
- forall(b, in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b))))) |- existsOne(
- X,
- forall(x, in(x, X) <=> exists(b, in(b, B) /\ forall(x1, in(x1, x) <=> exists(a, in(a, A) /\ psi(x1, a, b)))))
- ),
- 6,
- Map(phi -> LambdaTermFormula(Seq(y_, b_), forall(x, in(x, y_) <=> exists(a, in(a, A) /\ psi(x, a, b_)))))
- )
- val s8 = Cut(
- forall(b, in(b, B) ==> H2) |- existsOne(X, forall(x, in(x, X) <=> exists(b, in(b, B) /\ forall(x1, in(x1, x) <=> exists(a, in(a, A) /\ psi(x1, a, b)))))),
- 5,
- 7,
- forall(b, in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))))
- )
- SCProof(Vector(s0, s1, s2, s3, s4, s5, s6, s7, s8), Vector(i1))
-
- // have ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s0
- // have (b ∈ B), ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s1
- // have (b ∈ B), (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s2
- // have (b ∈ B), ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s3
- // have ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ (b ∈ B) ⇒ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s4
- // have ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∀b. (b ∈ B) ⇒ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s5
- // 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
- }
- 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({
- // goal ∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!Z. ∃X. Z=UX /\ ∀x. (x ∈ X) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ ?A) ∧ ?psi(x1, a, b)
- // redGoal ∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃Z1. ∀Z. Z=Z1 <=> ∃X. Z=UX /\ ∀x. (x ∈ X) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ ?A) ∧ ?psi(x1, a, b)
- // redGoal ∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∀Z. Z=UX <=> ∃X. Z=UX /\ ∀x. (x ∈ X) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ ?A) ∧ ?psi(x1, a, b)
- // redGoal ∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∀Z. Z=UX <=> ∃X. Z=UX /\ ∀x. (x ∈ X) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ ?A) ∧ ?psi(x1, a, b)
- })
- */
-
- /**
- * ∃!x. ?phi(x) ⊢ ∃!z. ∃x. z=?F(x) /\ ?phi(x)
- */
- val lemmaApplyFToObject: SCProof = {
- val x = VariableLabel("x")
- val x1 = VariableLabel("x1")
- val z = VariableLabel("z")
- val z1 = VariableLabel("z1")
- val F = SchematicFunctionLabel("F", 1)
- val f = SchematicFunctionLabel("f", 0)
- val phi = SchematicPredicateLabel("phi", 1)
- val g = SchematicPredicateLabel("g", 0)
-
- val g2 = SCSubproof({
- val s0 = hypothesis(F(x1) === z)
- val s1 = LeftSubstEq((x === x1, F(x) === z) |- F(x1) === z, 0, List((x, x1)), LambdaTermFormula(Seq(f), F(f()) === z))
- val s2 = LeftSubstIff(Set(phi(x) <=> (x === x1), phi(x), F(x) === z) |- F(x1) === z, 1, List((x === x1, phi(x))), LambdaFormulaFormula(Seq(g), g()))
- val s3 = LeftForall(Set(forall(x, phi(x) <=> (x === x1)), phi(x), F(x) === z) |- F(x1) === z, 2, phi(x) <=> (x === x1), x, x)
- val s4 = Rewrite(Set(forall(x, phi(x) <=> (x === x1)), phi(x) /\ (F(x) === z)) |- F(x1) === z, 3)
- val s5 = LeftExists(Set(forall(x, phi(x) <=> (x === x1)), exists(x, phi(x) /\ (F(x) === z))) |- F(x1) === z, 4, phi(x) /\ (F(x) === z), x)
- val s6 = Rewrite(forall(x, phi(x) <=> (x === x1)) |- exists(x, phi(x) /\ (F(x) === z)) ==> (F(x1) === z), 5)
- SCProof(Vector(s0, s1, s2, s3, s4, s5, s6))
- }) // redGoal2 ∀x. x=x1 <=> phi(x) ⊢ ∃x. z=F(x) /\ phi(x) ==> F(x1)=z g2.s5
-
- val g1 = SCSubproof({
- val s0 = hypothesis(phi(x1))
- val s1 = LeftForall(forall(x, (x === x1) <=> phi(x)) |- phi(x1), 0, (x === x1) <=> phi(x), x, x1)
- val s2 = hypothesis(z === F(x1))
- val s3 = RightAnd((forall(x, (x === x1) <=> phi(x)), z === F(x1)) |- (z === F(x1)) /\ phi(x1), Seq(2, 1), Seq(z === F(x1), phi(x1)))
- val s4 = RightExists((forall(x, (x === x1) <=> phi(x)), z === F(x1)) |- exists(x, (z === F(x)) /\ phi(x)), 3, (z === F(x)) /\ phi(x), x, x1)
- val s5 = Rewrite(forall(x, (x === x1) <=> phi(x)) |- z === F(x1) ==> exists(x, (z === F(x)) /\ phi(x)), 4)
- SCProof(Vector(s0, s1, s2, s3, s4, s5))
- })
-
- val s0 = g1
- val s1 = g2
- val s2 = RightIff(forall(x, (x === x1) <=> phi(x)) |- (z === F(x1)) <=> exists(x, (z === F(x)) /\ phi(x)), 0, 1, z === F(x1), exists(x, (z === F(x)) /\ phi(x)))
- val s3 = RightForall(forall(x, (x === x1) <=> phi(x)) |- forall(z, (z === F(x1)) <=> exists(x, (z === F(x)) /\ phi(x))), 2, (z === F(x1)) <=> exists(x, (z === F(x)) /\ phi(x)), z)
- val s4 = RightExists(
- forall(x, (x === x1) <=> phi(x)) |- exists(z1, forall(z, (z === z1) <=> exists(x, (z === F(x)) /\ phi(x)))),
- 3,
- forall(z, (z === z1) <=> exists(x, (z === F(x)) /\ phi(x))),
- z1,
- F(x1)
- )
- val s5 = LeftExists(exists(x1, forall(x, (x === x1) <=> phi(x))) |- exists(z1, forall(z, (z === z1) <=> exists(x, (z === F(x)) /\ phi(x)))), 4, forall(x, (x === x1) <=> phi(x)), x1)
- val s6 = Rewrite(existsOne(x, phi(x)) |- existsOne(z, exists(x, (z === F(x)) /\ phi(x))), 5) // goal ∃!x. phi(x) ⊢ ∃!z. ∃x. z=F(x) /\ phi(x)
-
- SCProof(Vector(s0, s1, s2, s3, s4, s5, s6))
-
- // goal ∃!x. phi(x) ⊢ ∃!z. ∃x. z=F(x) /\ phi(x)
- // redGoal ∃x1. ∀X. x=x1 <=> phi(x) ⊢ ∃z1. ∀z. z1=z <=> ∃x. Z=F(x) /\ phi(x) s4, s5
- // redGoal ∀x. x=x1 <=> phi(x) ⊢ ∀z. F(x1)=z <=> ∃x. Z=F(x) /\ phi(x) s3
- // redGoal ∀x. x=x1 <=> phi(x) ⊢ F(x1)=z <=> ∃x. Z=F(x) /\ phi(x) s2
- // redGoal1 ∀x. x=x1 <=> phi(x) ⊢ F(x1)=z ==> ∃x. Z=F(x) /\ phi(x) g1.s5
- // redGoal1 ∀x. x=x1 <=> phi(x), F(x1)=z ⊢ ∃x. z=F(x) /\ phi(x) g1.s4
- // redGoal1 ∀x. x=x1 <=> phi(x), F(x1)=z ⊢ z=F(x1) /\ phi(x1) g1.s3
- // redGoal11 ∀x. x=x1 <=> phi(x), F(x1)=z ⊢ z=F(x1) TRUE g1.s2
- // redGoal12 ∀x. x=x1 <=> phi(x) ⊢ phi(x1) g1.s1
- // redGoal12 x1=x1 <=> phi(x1) ⊢ phi(x1)
- // redGoal12 phi(x1) ⊢ phi(x1) g1.s0
- // redGoal2 ∀x. x=x1 <=> phi(x) ⊢ ∃x. z=F(x) /\ phi(x) ==> F(x1)=z g2.s5
- // redGoal2 ∀x. x=x1 <=> phi(x), ∃x. z=F(x) /\ phi(x) ⊢ F(x1)=z g2.s4
- // redGoal2 ∀x. x=x1 <=> phi(x), z=F(x), phi(x) ⊢ F(x1)=z g2.s3
- // redGoal2 x=x1 <=> phi(x), z=F(x), phi(x) ⊢ F(x1)=z g2.s2
- // 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
- }
- 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)
- */
- val lemmaMapTwoArguments: SCProof = {
- val a = VariableLabel("a")
- val b = VariableLabel("b")
- val x = VariableLabel("x")
- val x1 = VariableLabel("x1")
- val a_ = SchematicFunctionLabel("a", 0)
- val b_ = SchematicFunctionLabel("b", 0)
- val x_ = SchematicFunctionLabel("x", 0)
- val y_ = SchematicFunctionLabel("y", 0)
- val F = SchematicFunctionLabel("F", 1)
- val A = SchematicFunctionLabel("A", 0)()
- val X = VariableLabel("X")
- val B = SchematicFunctionLabel("B", 0)()
- val phi = SchematicPredicateLabel("phi", 1)
- val psi = SchematicPredicateLabel("psi", 3)
-
- val i1 = lemma1.conclusion
- val i2 = lemmaApplyFToObject.conclusion
- val rPhi = forall(x, in(x, y_) <=> exists(b, in(b, B) /\ forall(x1, in(x1, x) <=> exists(a, in(a, A) /\ psi(x1, a, b)))))
- val seq0 = instantiatePredicateSchemaInSequent(i2, Map(phi -> LambdaTermFormula(Seq(y_), rPhi)))
- val s0 = InstPredSchema(seq0, -2, Map(phi -> LambdaTermFormula(Seq(y_), rPhi))) // val s0 = InstPredSchema(instantiatePredicateSchemaInSequent(i2, phi, rPhi, Seq(X)), -2, phi, rPhi, Seq(X))
- val seq1 = instantiateFunctionSchemaInSequent(seq0, Map(F -> LambdaTermTerm(Seq(x_), union(x_))))
- val s1 = InstFunSchema(seq1, 0, Map(F -> LambdaTermTerm(Seq(x_), union(x_))))
- val s2 = Cut(i1.left |- seq1.right, -1, 1, seq1.left.head)
- SCProof(Vector(s0, s1, s2), Vector(i1, i2))
- }
- 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))
- */
- val lemmaCartesianProduct: SCProof = {
- val a = VariableLabel("a")
- val b = VariableLabel("b")
- val x = VariableLabel("x")
- val a_ = SchematicFunctionLabel("a", 0)
- val b_ = SchematicFunctionLabel("b", 0)
- val x_ = SchematicFunctionLabel("x", 0)
- val x1 = VariableLabel("x1")
- val F = SchematicFunctionLabel("F", 1)
- val A = SchematicFunctionLabel("A", 0)()
- val X = VariableLabel("X")
- val B = SchematicFunctionLabel("B", 0)()
- val phi = SchematicPredicateLabel("phi", 1)
- val psi = SchematicPredicateLabel("psi", 3)
-
- val i1 =
- lemmaMapTwoArguments.conclusion // ∀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)
- val s0 = SCSubproof({
- val s0 = SCSubproof(makeFunctional(oPair(a, b)))
- val s1 = Weakening((in(b, B), in(a, A)) |- s0.bot.right, 0)
- val s2 = Rewrite(in(b, B) |- in(a, A) ==> s0.bot.right.head, 1)
- val s3 = RightForall(in(b, B) |- forall(a, in(a, A) ==> s0.bot.right.head), 2, in(a, A) ==> s0.bot.right.head, a)
- val s4 = Rewrite(() |- in(b, B) ==> forall(a, in(a, A) ==> s0.bot.right.head), 3)
- val s5 = RightForall(() |- forall(b, in(b, B) ==> forall(a, in(a, A) ==> s0.bot.right.head)), 4, in(b, B) ==> forall(a, in(a, A) ==> s0.bot.right.head), b)
- SCProof(Vector(s0, s1, s2, s3, s4, s5))
- }) // ∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. x= (a, b)
-
- val s1 = InstPredSchema(
- instantiatePredicateSchemaInSequent(i1, Map(psi -> LambdaTermFormula(Seq(x_, a_, b_), x_ === oPair(a_, b_)))),
- -1,
- Map(psi -> LambdaTermFormula(Seq(x_, a_, b_), x_ === oPair(a_, b_)))
- )
- val s2 = Cut(() |- s1.bot.right, 0, 1, s1.bot.left.head)
-
- val vA = VariableLabel("A")
- val vB = VariableLabel("B")
- val s3 = InstFunSchema(
- instantiateFunctionSchemaInSequent(s2.bot, Map(SchematicFunctionLabel("A", 0) -> LambdaTermTerm(Nil, vA))),
- 2,
- Map(SchematicFunctionLabel("A", 0) -> LambdaTermTerm(Nil, vA))
- )
- val s4 = InstFunSchema(
- instantiateFunctionSchemaInSequent(s3.bot, Map(SchematicFunctionLabel("B", 0) -> LambdaTermTerm(Nil, vA))),
- 3,
- Map(SchematicFunctionLabel("B", 0) -> LambdaTermTerm(Nil, vA))
- )
- val s5 = RightForall(() |- forall(vA, s4.bot.right.head), 4, s4.bot.right.head, vA)
- val s6 = RightForall(() |- forall(vB, s5.bot.right.head), 5, s5.bot.right.head, vB)
- SCProof(Vector(s0, s1, s2, s3, s4, s5, s6), Vector(i1))
-
- }
- /*
- val thm_lemmaCartesianProduct = theory.proofToTheorem("lemmaCartesianProduct", lemmaCartesianProduct, Seq(thm_lemmaMapTwoArguments)).get
- val vA = VariableLabel("A")
- val vB = VariableLabel("B")
- val cart_product = ConstantFunctionLabel("cart_cross", 2)
- val def_oPair = theory.makeFunctionDefinition(lemmaCartesianProduct, Seq(thm_lemmaMapTwoArguments), cart_product, Seq(vA, vB), VariableLabel("z"), innerOfDefinition(lemmaCartesianProduct.conclusion.right.head)).get
- */
-
- def innerOfDefinition(f: Formula): Formula = f match {
- case BinderFormula(Forall, bound, inner) => innerOfDefinition(inner)
- case BinderFormula(ExistsOne, bound, inner) => inner
- case _ => f
- }
-
- // def makeFunctionalReplacement(t:Term)
- def makeFunctional(t: Term): SCProof = {
- val x = VariableLabel(freshId(t.freeVariables.map(_.id), "x"))
- val y = VariableLabel(freshId(t.freeVariables.map(_.id), "y"))
- val s0 = RightRefl(() |- t === t, t === t)
- val s1 = Rewrite(() |- (x === t) <=> (x === t), 0)
- val s2 = RightForall(() |- forall(x, (x === t) <=> (x === t)), 1, (x === t) <=> (x === t), x)
- val s3 = RightExists(() |- exists(y, forall(x, (x === y) <=> (x === t))), 2, forall(x, (x === y) <=> (x === t)), y, t)
- val s4 = Rewrite(() |- existsOne(x, x === t), 3)
- SCProof(s0, s1, s2, s3, s4)
- }
-
- def main(args: Array[String]): Unit = {
-
- println("\nthmMapFunctional")
- checkProof(thmMapFunctional)
- println("\nlemma1")
- checkProof(lemma1)
- println("\nlemmaApplyFToObject")
- checkProof(lemmaApplyFToObject)
- println("\nlemmaMapTwoArguments")
- checkProof(lemmaMapTwoArguments)
- println("\nlemmaCartesianProduct")
- checkProof(lemmaCartesianProduct)
- }
-}
-
-// have union ∀x. ∀z. x ∈ Uz <=> ∃y. (x ∈ y /\ y ∈ z)
-// have x ∈ UY <=> ∃y. (x ∈ y /\ y ∈ Y)
-//
-//
-// goal ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∃a. (a ∈ A) ∧ ?psi(x, a, b)
-// redGoal ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃Y. ∀X. (Y=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∃a. (a ∈ A) ∧ ?psi(x, a, b)
-// redGoal ∀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) ⊢ ∃Y. ∀X. (UY=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∃a. (a ∈ A) ∧ ?psi(x, a, b)
-// redGoal ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b), ∃Y. ∀X. (Y=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b) ⊢ ∃Y. ∀X. (UY=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∃a. (a ∈ A) ∧ ?psi(x, a, b)
-// redGoal ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b), ∀X. (Y=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b) ⊢ ∃Y. ∀X. (UY=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∃a. (a ∈ A) ∧ ?psi(x, a, b)
-// redGoal ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b), ∀X. (Y=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b) ⊢ ∀X. (UY=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∃a. (a ∈ A) ∧ ?psi(x, a, b)
-// redGoal ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b), ∀X. (Y=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b) ⊢ (UY=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∃a. (a ∈ A) ∧ ?psi(x, a, b)
-// redGoal ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b), (Y=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b) ⊢ (UY=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∃a. (a ∈ A) ∧ ?psi(x, a, b)
-// redGoal ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b), (Y=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b), x ∈ UY <=> ∃y. (x ∈ y /\ y ∈ Y) ⊢ (UY=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∃a. (a ∈ A) ∧ ?psi(x, a, b)
-// redGoal1 ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b), (Y=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b), x ∈ UY <=> ∃y. (x ∈ y /\ y ∈ Y) ⊢ (UY=X) => ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∃a. (a ∈ A) ∧ ?psi(x, a, b)
-// redGoal1 ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b), (Y=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b), x ∈ UY <=> ∃y. (x ∈ y /\ y ∈ Y), (UY=X) ⊢ ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∃a. (a ∈ A) ∧ ?psi(x, a, b)
-// redGoal1 ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b), (Y=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b), x ∈ UY <=> ∃y. (x ∈ y /\ y ∈ Y), (UY=X) ⊢ ∀x. (x ∈ UY) ↔ ∃b. (b ∈ B) ∧ ∃a. (a ∈ A) ∧ ?psi(x, a, b)
-// redGoal1 ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b), (Y=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b), x ∈ UY <=> ∃y. (x ∈ y /\ y ∈ Y), (UY=X) ⊢ ∀x. (x ∈ UY) ↔ ∃b. (b ∈ B) ∧ ∃a. (a ∈ A) ∧ ?psi(x, a, b)
-// redGoal2 ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b), (Y=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b), x ∈ UY <=> ∃y. (x ∈ y /\ y ∈ Y) ⊢ (UY=X) <= ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∃a. (a ∈ A) ∧ ?psi(x, a, b)
diff --git a/src/main/scala/proven/ElementsOfSetTheory.scala b/src/main/scala/proven/ElementsOfSetTheory.scala
deleted file mode 100644
index e5c83222a4a9f693bd518f27ea6646a8f2e74f2f..0000000000000000000000000000000000000000
--- a/src/main/scala/proven/ElementsOfSetTheory.scala
+++ /dev/null
@@ -1,458 +0,0 @@
-package proven
-
-import lisa.kernel.fol.FOL.*
-import lisa.kernel.proof.SCProof
-import lisa.kernel.proof.SCProofChecker
-import lisa.kernel.proof.SequentCalculus.*
-import lisa.settheory.AxiomaticSetTheory
-import lisa.settheory.AxiomaticSetTheory.*
-import proven.ElementsOfSetTheory.theory
-import proven.tactics.Destructors.*
-import proven.tactics.ProofTactics.*
-import utilities.Helpers.{_, given}
-import utilities.Printer
-import utilities.Printer.*
-
-import scala.collection.immutable
-import scala.collection.immutable.SortedSet
-
-/**
- * Some proofs in set theory. See it as a proof of concept.
- */
-object ElementsOfSetTheory {
-
- val theory = AxiomaticSetTheory.runningSetTheory
- def axiom(f: Formula): theory.Axiom = theory.getAxiom(f).get
-
- private val x = VariableLabel("x")
- private val y = VariableLabel("y")
- private val x1 = VariableLabel("x'")
- private val y1 = VariableLabel("y'")
- private val z = VariableLabel("z")
- private val g = SchematicFunctionLabel("g", 0)
- private val h = SchematicPredicateLabel("h", 0)
-
- val oPair: ConstantFunctionLabel = ConstantFunctionLabel("ordered_pair", 2)
- val oPairFirstElement: ConstantFunctionLabel = ConstantFunctionLabel("ordered_pair_first_element", 1)
- val oPairSecondElement: ConstantFunctionLabel = ConstantFunctionLabel("ordered_pair_second_element", 1)
-
- val proofUnorderedPairSymmetry: SCProof = {
- val imps: IndexedSeq[Sequent] = IndexedSeq(() |- extensionalityAxiom, () |- pairAxiom)
- val s0 = Rewrite(() |- extensionalityAxiom, -1)
- val pairExt1 = instantiateForall(new SCProof(IndexedSeq(s0), imps), extensionalityAxiom, pair(x, y))
- val pairExt2 = instantiateForall(pairExt1, pairExt1.conclusion.right.head, pair(y, x))
- val t0 = Rewrite(() |- pairAxiom, -2)
- val pairSame11 = instantiateForall(new SCProof(IndexedSeq(t0), imps), pairAxiom, x)
- val pairSame12 = instantiateForall(pairSame11, pairSame11.conclusion.right.head, y)
- val pairSame13 = instantiateForall(pairSame12, pairSame12.conclusion.right.head, z)
-
- val pairSame21 = instantiateForall(new SCProof(IndexedSeq(t0), imps), pairAxiom, y)
- val pairSame22 = instantiateForall(pairSame21, pairSame21.conclusion.right.head, x)
- val pairSame23 = instantiateForall(pairSame22, pairSame22.conclusion.right.head, z)
- val condsymor = ((y === z) \/ (x === z)) <=> ((x === z) \/ (y === z))
- val pairSame24 = pairSame23 // + st1
-
- val pr0 = SCSubproof(pairSame13, Seq(-1, -2))
- val pr1 = SCSubproof(pairSame23, Seq(-1, -2))
- val pr2 = RightSubstIff(
- Sequent(pr1.bot.right, Set(in(z, pair(x, y)) <=> in(z, pair(y, x)))),
- 0,
- List(((x === z) \/ (y === z), in(z, pair(y, x)))),
- LambdaFormulaFormula(Seq(h), in(z, pair(x, y)) <=> h())
- )
- val pr3 = Cut(Sequent(pr1.bot.left, pr2.bot.right), 1, 2, pr2.bot.left.head)
- // val pr4 = LeftAxiom(Sequent(Set(), pr2.bot.right), 3, pr1.bot.left.head, "")
- val pr4 = RightForall(Sequent(Set(), Set(forall(z, pr2.bot.right.head))), 3, pr2.bot.right.head, z)
- val fin = SCProof(IndexedSeq(pr0, pr1, pr2, pr3, pr4), imps)
- val fin2 = byEquiv(pairExt2.conclusion.right.head, fin.conclusion.right.head)(SCSubproof(pairExt2, Seq(-1, -2)), SCSubproof(fin, Seq(-1, -2)))
- val fin3 = generalizeToForall(fin2, fin2.conclusion.right.head, x)
- 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.theorem("proofUnorderedPairSymmetry", "⊢ ∀y, x. {x, y} = {y, x}", proofUnorderedPairSymmetry, Seq(axiom(extensionalityAxiom), axiom(pairAxiom))).get
-
- val proofUnorderedPairDeconstruction: SCProof = {
- val pxy = pair(x, y)
- val pxy1 = pair(x1, y1)
- val zexy = (z === x) \/ (z === y)
- val p0 = SCSubproof(
- {
- val p0 = SCSubproof(
- {
- val zf = in(z, pxy)
- val p1_0 = hypothesis(zf)
- val p1_1 = RightImplies(emptySeq +> (zf ==> zf), 0, zf, zf)
- val p1_2 = RightIff(emptySeq +> (zf <=> zf), 1, 1, zf, zf) // |- (z in {x,y} <=> z in {x,y})
- val p1_3 = RightSubstEq(emptySeq +< (pxy === pxy1) +> (zf <=> in(z, pxy1)), 2, List((pxy, pxy1)), LambdaTermFormula(Seq(g), zf <=> in(z, g())))
- SCProof(IndexedSeq(p1_0, p1_1, p1_2, p1_3), IndexedSeq(() |- pairAxiom))
- },
- Seq(-1),
- display = true
- ) // ({x,y}={x',y'}) |- ((z∈{x,y})↔(z∈{x',y'}))
- val p1 = SCSubproof(
- {
- val p1_0 = Rewrite(() |- pairAxiom, -1) // |- ∀∀∀((z$1∈{x$3,y$2})↔((x$3=z$1)∨(y$2=z$1)))
- val p1_1 = instantiateForall(SCProof(IndexedSeq(p1_0), IndexedSeq(() |- pairAxiom)), x, y, z)
- p1_1
- },
- Seq(-1),
- display = true
- ) // |- (z in {x,y}) <=> (z=x \/ z=y)
- val p2 = SCSubproof(
- {
- val p2_0 = Rewrite(() |- pairAxiom, -1) // |- ∀∀∀((z$1∈{x$3,y$2})↔((x$3=z$1)∨(y$2=z$1)))
- val p2_1 = instantiateForall(SCProof(IndexedSeq(p2_0), IndexedSeq(() |- pairAxiom)), x1, y1, z)
- p2_1
- },
- Seq(-1),
- display = true
- ) // |- (z in {x',y'}) <=> (z=x' \/ z=y')
- val p3 = RightSubstEq(
- emptySeq +< (pxy === pxy1) +> (in(z, pxy1) <=> ((z === x) \/ (z === y))),
- 1,
- List((pxy, pxy1)),
- LambdaTermFormula(Seq(g), in(z, g()) <=> ((z === x) \/ (z === y)))
- ) // ({x,y}={x',y'}) |- ((z∈{x',y'})↔((z=x)∨(z=y)))
- val p4 = RightSubstIff(
- emptySeq +< p3.bot.left.head +< p2.bot.right.head +> (((z === x) \/ (z === y)) <=> ((z === x1) \/ (z === y1))),
- 3,
- List(((z === x1) \/ (z === y1), in(z, pxy1))),
- LambdaFormulaFormula(Seq(h), h() <=> ((z === x) \/ (z === y)))
- ) // ((z∈{x',y'})↔((x'=z)∨(y'=z))), ({x,y}={x',y'}) |- (((z=x)∨(z=y))↔((z=x')∨(z=y')))
- val p5 = Cut(emptySeq ++< p3.bot ++> p4.bot, 2, 4, p2.bot.right.head)
- SCProof(IndexedSeq(p0, p1, p2, p3, p4, p5), IndexedSeq(() |- pairAxiom))
- },
- Seq(-1)
- ) // ({x,y}={x',y'}) |- (((z=x)∨(z=y))↔((z=x')∨(z=y')))
-
- val p1 = SCSubproof(
- SCProof(
- byCase(x === x1)(
- SCSubproof(
- {
- val pcm1 = p0
- val pc0 = SCSubproof(
- SCProof(
- byCase(y === x)(
- SCSubproof(
- {
- val pam1 = pcm1
- val pa0 = SCSubproof(
- {
- val f1 = z === x
- val pa0_m1 = pcm1 // ({x,y}={x',y'}) |- (((z=x)∨(z=y))↔((z=x')∨(z=y')))
- val pa0_0 = SCSubproof(
- {
- val pa0_0_0 = hypothesis(f1)
- val pa0_1_1 = RightOr(emptySeq +< f1 +> (f1 \/ f1), 0, f1, f1)
- val pa0_1_2 = RightImplies(emptySeq +> (f1 ==> (f1 \/ f1)), 1, f1, f1 \/ f1)
- val pa0_1_3 = LeftOr(emptySeq +< (f1 \/ f1) +> f1, Seq(0, 0), Seq(f1, f1))
- val pa0_1_4 = RightImplies(emptySeq +> ((f1 \/ f1) ==> f1), 3, f1 \/ f1, f1)
- val pa0_1_5 = RightIff(emptySeq +> ((f1 \/ f1) <=> f1), 2, 4, (f1 \/ f1), f1)
- val r = SCProof(pa0_0_0, pa0_1_1, pa0_1_2, pa0_1_3, pa0_1_4, pa0_1_5)
- r
- },
- display = false
- ) // |- (((z=x)∨(z=x))↔(z=x))
- val pa0_1 = RightSubstEq(
- emptySeq +< (pxy === pxy1) +< (x === y) +> ((f1 \/ f1) <=> (z === x1) \/ (z === y1)),
- -1,
- List((x, y)),
- LambdaTermFormula(Seq(g), (f1 \/ (z === g())) <=> ((z === x1) \/ (z === y1)))
- ) // ({x,y}={x',y'}) y=x|- (z=x)\/(z=x) <=> (z=x' \/ z=y')
- val pa0_2 = RightSubstIff(
- emptySeq +< (pxy === pxy1) +< (x === y) +< (f1 <=> (f1 \/ f1)) +> (f1 <=> ((z === x1) \/ (z === y1))),
- 1,
- List((f1, f1 \/ f1)),
- LambdaFormulaFormula(Seq(h), h() <=> ((z === x1) \/ (z === y1)))
- )
- val pa0_3 =
- Cut(emptySeq +< (pxy === pxy1) +< (x === y) +> (f1 <=> ((z === x1) \/ (z === y1))), 0, 2, f1 <=> (f1 \/ f1)) // (x=y), ({x,y}={x',y'}) |- ((z=x)↔((z=x')∨(z=y')))
- val pa0_4 = RightForall(emptySeq +< (pxy === pxy1) +< (x === y) +> forall(z, f1 <=> ((z === x1) \/ (z === y1))), 3, f1 <=> ((z === x1) \/ (z === y1)), z)
- val ra0_0 = instantiateForall(SCProof(IndexedSeq(pa0_0, pa0_1, pa0_2, pa0_3, pa0_4), IndexedSeq(pa0_m1.bot)), y1) // (x=y), ({x,y}={x',y'}) |- ((y'=x)↔((y'=x')∨(y'=y')))
- ra0_0
- },
- IndexedSeq(-1)
- ) // ({x,y}={x',y'}) y=x|- ((y'=x)↔((y'=x')∨(y'=y')))
- val pa1 = SCSubproof(
- {
- val pa1_0 = RightRefl(emptySeq +> (y1 === y1), y1 === y1)
- val pa1_1 = RightOr(emptySeq +> ((y1 === y1) \/ (y1 === x1)), 0, y1 === y1, y1 === x1)
- SCProof(pa1_0, pa1_1)
- },
- display = false
- ) // |- (y'=x' \/ y'=y')
- val ra3 = byEquiv(pa0.bot.right.head, pa1.bot.right.head)(pa0, pa1) // ({x,y}={x',y'}) y=x|- ((y'=x)
- val pal = RightSubstEq(emptySeq ++< pa0.bot +> (y1 === y), ra3.length - 1, List((x, y)), LambdaTermFormula(Seq(g), y1 === g()))
- SCProof(ra3.steps, IndexedSeq(pam1.bot)) appended pal // (x=y), ({x,y}={x',y'}) |- (y'=y)
- },
- IndexedSeq(-1)
- ) // (x=y), ({x,y}={x',y'}) |- (y'=y)
- ,
- SCSubproof(
- {
- val pbm1 = pcm1 // ({x,y}={x',y'}) |- (((z=x)∨(z=y))↔((z=x')∨(z=y')))
- val pb0_0 = SCSubproof(
- {
- val pb0_0 = RightForall(emptySeq ++< pcm1.bot +> forall(z, pcm1.bot.right.head), -1, pcm1.bot.right.head, z)
- instantiateForall(SCProof(IndexedSeq(pb0_0), IndexedSeq(pcm1.bot)), y)
- },
- IndexedSeq(-1)
- ) // ({x,y}={x',y'}) |- (((y=x)∨(y=y))↔((y=x')∨(y=y')))
- val pb0_1 = SCSubproof(
- {
- val pa1_0 = RightRefl(emptySeq +> (y === y), y === y)
- val pa1_1 = RightOr(emptySeq +> ((y === y) \/ (y === x)), 0, y === y, y === x)
- SCProof(pa1_0, pa1_1)
- },
- display = false
- ) // |- (y=x)∨(y=y)
- val rb0 = byEquiv(pb0_0.bot.right.head, pb0_1.bot.right.head)(pb0_0, pb0_1) // ({x,y}={x',y'}) |- (y=x')∨(y=y')
- val pb1 =
- RightSubstEq(emptySeq ++< rb0.conclusion +< (x === x1) +> ((y === x) \/ (y === y1)), rb0.length - 1, List((x, x1)), LambdaTermFormula(Seq(g), (y === g()) \/ (y === y1)))
- val rb1 = destructRightOr(
- rb0 appended pb1, // ({x,y}={x',y'}) , x=x'|- (y=x)∨(y=y')
- y === x,
- y === y1
- )
- val rb2 = rb1 appended LeftNot(rb1.conclusion +< !(y === x) -> (y === x), rb1.length - 1, y === x) // (x=x'), ({x,y}={x',y'}), ¬(y=x) |- (y=y')
- SCProof(rb2.steps, IndexedSeq(pbm1.bot))
-
- },
- IndexedSeq(-1)
- ) // ({x,y}={x',y'}), x=x', !y=x |- y=y'
- ).steps,
- IndexedSeq(pcm1.bot)
- ),
- IndexedSeq(-1)
- ) // (x=x'), ({x,y}={x',y'}) |- (y'=y)
- val pc1 = RightRefl(emptySeq +> (x === x), x === x)
- val pc2 = RightAnd(emptySeq ++< pc0.bot +> ((y1 === y) /\ (x === x)), Seq(0, 1), Seq(y1 === y, x === x)) // ({x,y}={x',y'}), x=x' |- (x=x /\ y=y')
- val pc3 =
- RightSubstEq(emptySeq ++< pc2.bot +> ((y1 === y) /\ (x1 === x)), 2, List((x, x1)), LambdaTermFormula(Seq(g), (y1 === y) /\ (g() === x))) // ({x,y}={x',y'}), x=x' |- (x=x' /\ y=y')
- val pc4 = RightOr(
- emptySeq ++< pc3.bot +> (pc3.bot.right.head \/ ((x === y1) /\ (y === x1))),
- 3,
- pc3.bot.right.head,
- (x === y1) /\ (y === x1)
- ) // ({x,y}={x',y'}), x=x' |- (x=x' /\ y=y')\/(x=y' /\ y=x')
- val r = SCProof(IndexedSeq(pc0, pc1, pc2, pc3, pc4), IndexedSeq(pcm1.bot))
- r
- },
- IndexedSeq(-1)
- ) // ({x,y}={x',y'}), x=x' |- (x=x' /\ y=y')\/(x=y' /\ y=x')
- ,
- SCSubproof(
- {
- val pdm1 = p0
- val pd0 = SCSubproof(
- {
- val pd0_m1 = pdm1
- val pd0_0 = SCSubproof {
- val ex1x1 = x1 === x1
- val pd0_0_0 = RightRefl(emptySeq +> ex1x1, ex1x1) // |- x'=x'
- val pd0_0_1 = RightOr(emptySeq +> (ex1x1 \/ (x1 === y1)), 0, ex1x1, x1 === y1) // |- (x'=x' \/ x'=y')
- SCProof(IndexedSeq(pd0_0_0, pd0_0_1))
- } // |- (x'=x' \/ x'=y')
- val pd0_1 = SCSubproof(
- {
- val pd0_1_m1 = pd0_m1 // ({x,y}={x',y'}) |- (((z=x)∨(z=y))↔((z=x')∨(z=y')))
- val pd0_1_0 = RightForall(emptySeq ++< pd0_1_m1.bot +> forall(z, pd0_1_m1.bot.right.head), -1, pd0_1_m1.bot.right.head, z)
- val rd0_1_1 = instantiateForall(SCProof(IndexedSeq(pd0_1_0), IndexedSeq(pd0_m1.bot)), x1) // ({x,y}={x',y'}) |- (x'=x \/ x'=y) <=> (x'=x' \/ x'=y')
- rd0_1_1
- },
- IndexedSeq(-1)
- ) // ({x,y}={x',y'}) |- (x'=x \/ x'=y) <=> (x'=x' \/ x'=y')
- val pd0_2 = RightSubstIff(
- pd0_1.bot.right |- ((x1 === x) \/ (x1 === y)),
- 0,
- List(((x1 === x) \/ (x1 === y), (x1 === x1) \/ (x1 === y1))),
- LambdaFormulaFormula(Seq(h), h())
- ) // (x'=x \/ x'=y) <=> (x'=x' \/ x'=y') |- (x'=x \/ x'=y)
- val pd0_3 = Cut(pd0_1.bot.left |- pd0_2.bot.right, 1, 2, pd0_1.bot.right.head) // ({x,y}={x',y'}) |- (x=x' \/ y=x')
- destructRightOr(SCProof(IndexedSeq(pd0_0, pd0_1, pd0_2, pd0_3), IndexedSeq(pd0_m1.bot)), x === x1, y === x1) // ({x,y}={x',y'}) |- x=x', y=x'
- },
- IndexedSeq(-1)
- ) // ({x,y}={x',y'}) |- x=x', y=x' --
- val pd1 = SCSubproof(
- {
- val pd1_m1 = pdm1
- val pd1_0 = SCSubproof {
- val exx = x === x
- val pd1_0_0 = RightRefl(emptySeq +> exx, exx) // |- x=x
- val pd1_0_1 = RightOr(emptySeq +> (exx \/ (x === y)), 0, exx, x === y) // |- (x=x \/ x=y)
- SCProof(IndexedSeq(pd1_0_0, pd1_0_1))
- } // |- (x=x \/ x=y)
- val pd1_1 = SCSubproof(
- {
- val pd1_1_m1 = pd1_m1 // ({x,y}={x',y'}) |- (((z=x)∨(z=y))↔((z=x')∨(z=y')))
- val pd1_1_0 = RightForall(emptySeq ++< pd1_1_m1.bot +> forall(z, pd1_1_m1.bot.right.head), -1, pd1_1_m1.bot.right.head, z)
- val rd1_1_1 = instantiateForall(SCProof(IndexedSeq(pd1_1_0), IndexedSeq(pd1_m1.bot)), x) // ({x,y}={x',y'}) |- (x=x \/ x=y) <=> (x=x' \/ x=y')
- rd1_1_1
- },
- IndexedSeq(-1)
- ) // // ({x,y}={x',y'}) |- (x=x \/ x=y) <=> (x=x' \/ x=y')
- val rd1_2 = byEquiv(pd1_1.bot.right.head, pd1_0.bot.right.head)(pd1_1, pd1_0)
- val pd1_3 = SCSubproof(SCProof(rd1_2.steps, IndexedSeq(pd1_m1.bot)), IndexedSeq(-1)) // // ({x,y}={x',y'}) |- x=x' \/ x=y'
- destructRightOr(SCProof(IndexedSeq(pd1_0, pd1_1, pd1_3), IndexedSeq(pd1_m1.bot)), x === x1, x === y1) // ({x,y}={x',y'}) |- x=x', x=y'
- },
- IndexedSeq(-1)
- ) // ({x,y}={x',y'}) |- x=x', x=y' --
- val pd2 = RightAnd(emptySeq ++< pd1.bot +> (x === x1) +> ((x === y1) /\ (y === x1)), Seq(0, 1), Seq(x === y1, y === x1)) // ({x,y}={x',y'}) |- x=x', (x=y' /\ y=x') ---
- val pd3 = LeftNot(emptySeq ++< pd2.bot +< !(x === x1) +> ((x === y1) /\ (y === x1)), 2, x === x1) // ({x,y}={x',y'}), !x===x1 |- (x=y' /\ y=x')
- val pd4 = RightOr(
- emptySeq ++< pd3.bot +> (pd3.bot.right.head \/ ((x === x1) /\ (y === y1))),
- 3,
- pd3.bot.right.head,
- (x === x1) /\ (y === y1)
- ) // ({x,y}={x',y'}), !x===x1 |- (x=x' /\ y=y')\/(x=y' /\ y=x')
- SCProof(IndexedSeq(pd0, pd1, pd2, pd3, pd4), IndexedSeq(pdm1.bot))
- },
- IndexedSeq(-1)
- ) // ({x,y}={x',y'}), !x=x' |- (x=x' /\ y=y')\/(x=y' /\ y=x')
- ).steps,
- IndexedSeq(p0.bot)
- ),
- IndexedSeq(0)
- ) // ({x,y}={x',y'}) |- (x=x' /\ y=y')\/(x=y' /\ y=x')
-
- 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
- .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
-
- val orderedPairDefinition: SCProof = simpleFunctionDefinition(pair(pair(x, y), pair(x, x)), Seq(x, y))
-
- val def_oPair = theory.makeFunctionDefinition(orderedPairDefinition, Nil, oPair, Seq(x, y), x1, x1 === pair(pair(x, y), pair(x, x)))
-
- /*
- val proofOrderedPairDeconstruction: SCProof = {
- val opairxy = pair(pair(x, y), pair(x, x))
- val opairxx = pair(pair(x, x), pair(x, x))
- val opairxy1 = pair(pair(x1, y1), pair(x1, x1))
- val opairxx1 = pair(pair(x1, x1), pair(x1, x1))
- val pairxy = pair(x, y)
- val pairxx = pair(x, x)
- val pairxy1 = pair(x1, y1)
- val pairxx1 = pair(x1, x1)
- val p0 = SCSubproof(orderedPairDefinition, display = false)
- val p1 = SCSubproof(proofUnorderedPairDeconstruction) // |- ∀∀∀∀(({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 p2: SCSubproof = SCSubproof(SCProof(byCase(x === y)(
- {
- val p2_0 = SCSubproof(SCProof({
- val pa2_0 = SCSubproof({
- val p2_0_0 = UseFunctionDefinition(emptySeq +> (oPair(x, y) === opairxy), oPair, Seq(x, y)) // |- (x, y) === {{x,y}, {x,x}}
- val p2_0_1 = RightSubstEq(emptySeq +< (x === y) +> (oPair(x, y) === opairxx),
- 0, x, y, oPair(x, y) === pair(pair(x, z), pair(x, x)), z) // (x=y) |- ((x,y)={{x,x},{x,x}})
- val p2_0_2 = UseFunctionDefinition(emptySeq +> (oPair(x1, y1) === opairxy1), oPair, Seq(x1, y1)) // |- (x1, y1) === {{x1,y1}, {x1,x1}}
- val p2_0_3 = RightSubstEq(emptySeq +< (oPair(x, y) === oPair(x1, y1)) +< (x === y) +> (oPair(x1, y1) === pair(pair(x, x), pair(x, x))),
- 1, oPair(x, y), oPair(x1, y1), z === pair(pair(x, x), pair(x, x)), z) // (x=y), (x1,y1)=(x,y) |- ((x1,y1)={{x,x},{x,x}})
- val p2_0_4 = RightSubstEq(emptySeq +< (oPair(x, y) === oPair(x1, y1)) +< (x === y) +< (opairxy1 === oPair(x1, y1)) +> (pair(pair(x, x), pair(x, x)) === pair(pair(x1, y1), pair(x1, x1))),
- 3, opairxy1, oPair(x1, y1), z === pair(pair(x, x), pair(x, x)), z) // (x=y), (x1,y1)=(x,y), (x1,y1)={{x1,y1}, {x1,x1}} |- {{x1,y1}, {x1,x1}}={{x,x},{x,x}})
- val p2_0_5 = Cut(emptySeq +< (oPair(x, y) === oPair(x1, y1)) +< (x === y) +> (pair(pair(x, x), pair(x, x)) === pair(pair(x1, y1), pair(x1, x1))),
- 2, 4, opairxy1 === oPair(x1, y1))
- SCProof(IndexedSeq(p2_0_0, p2_0_1, p2_0_2, p2_0_3, p2_0_4, p2_0_5), IndexedSeq(p0))
- }, IndexedSeq(-1)) // ((x,y)=(x',y')), (x=y) |- ({{x,x},{x,x}}={{x',y'},{x',x'}})
- val pa2_1 = SCSubproof({
- instantiateForall(SCProof(IndexedSeq(), IndexedSeq(p1)), pairxx, pairxx, pairxy1, pairxx1)
- }, IndexedSeq(-2)) // ({{x,x},{x,x}}={{x',y'},{x',x'}})⇒((({x',x'}={x,x})∧({x',y'}={x,x}))∨(({x,x}={x',x'})∧({x,x}={x',y'}))))
- val pr2_0 = modusPonens(pa2_0.bot.right.head)(pa2_0, pa2_1) // ((x,y)=(x',y')), (x=y) |- ((({x',x'}={x,x})∧({x',y'}={x,x}))∨(({x,x}={x',x'})∧({x,x}={x',y'})))
- val f = (pairxx === pairxx1) /\ (pairxx === pairxy1)
- destructRightAnd(destructRightOr(pr2_0, f, f), pairxx === pairxy1, pairxx === pairxx1) // ((x,y)=(x',y')), (x=y) |- {x',y'}={x,x}
- }.steps, IndexedSeq(p0, p1)), IndexedSeq(-1, -2)) // ((x,y)=(x',y')), (x=y) |- {x',y'}={x,x}
- val p2_1 = SCSubproof({
- val pr2_1_0 = instantiateForall(SCProof(IndexedSeq(), IndexedSeq(p1)), x, x, x1, y1) // (({x,x}={x',y'})⇒(((y'=x)∧(x'=x))∨((x=y')∧(x=x'))))
- val f = (y1 === x) /\ (x1 === x)
- val pr2_1_1 = destructRightImplies(pr2_1_0, pairxx === pairxy1, f \/ f) // (({x,x}={x',y'}) |- (((y'=x)∧(x'=x))∨((x=y')∧(x=x'))))
- val pr2_1_2 = destructRightOr(pr2_1_1, f, f)
- pr2_1_2
- }, IndexedSeq(-2)) // {x',y'}={x,x}, x=y |- x=x' /\ x=y'
- val p2_2 = Cut(emptySeq ++< p2_0.bot ++> p2_1.bot, 0, 1, p2_0.bot.right.head) // ((x,y)=(x',y')), x=y |- x=x' /\ x=y'
- val p2_3 = RightSubstEq(emptySeq +< (oPair(x, y) === oPair(x1, y1)) +< (x === y) +> ((x === x1) /\ (y === y1)), 2, x, y, (x === x1) /\ (z === y1), z)
- SCSubproof(SCProof(IndexedSeq(p2_0, p2_1, p2_2, p2_3), IndexedSeq(p0, p1)), IndexedSeq(-1, -2))
- } // ((x,y)=(x',y')), x=y |- x=x' /\ y=y'
- ,
- {
- val pa2_0: SCSubproof = SCSubproof({
- val p2_0_0 = UseFunctionDefinition(emptySeq +> (oPair(x, y) === opairxy), oPair, Seq(x, y)) // |- (x, y) === {{x,y}, {x,x}}
- val p2_0_1 = UseFunctionDefinition(emptySeq +> (oPair(x1, y1) === opairxy1), oPair, Seq(x1, y1)) // |- (x1, y1) === {{x1,y1}, {x1,x1}}
- val p2_0_2 = RightSubstEq(emptySeq +< (oPair(x, y) === oPair(x1, y1)) +> (oPair(x1, y1) === pair(pair(x, y), pair(x, x))),
- 0, oPair(x, y), oPair(x1, y1), z === pair(pair(x, y), pair(x, x)), z) // (x1,y1)=(x,y) |- ((x1,y1)={{x,y},{x,x}})
- val p2_0_3 = RightSubstEq(emptySeq +< (oPair(x, y) === oPair(x1, y1)) +< (opairxy1 === oPair(x1, y1)) +> (pair(pair(x, y), pair(x, x)) === pair(pair(x1, y1), pair(x1, x1))),
- 2, opairxy1, oPair(x1, y1), z === pair(pair(x, y), pair(x, x)), z) // (x1,y1)=(x,y), (x1,y1)={{x1,y1}, {x1,x1}} |- {{x1,y1}, {x1,x1}}={{x,y},{x,x}})
- val p2_0_4 = Cut(emptySeq +< (oPair(x, y) === oPair(x1, y1)) +> (pair(pair(x, y), pair(x, x)) === pair(pair(x1, y1), pair(x1, x1))),
- 1, 3, opairxy1 === oPair(x1, y1))
- SCProof(IndexedSeq(p2_0_0, p2_0_1, p2_0_2, p2_0_3, p2_0_4), IndexedSeq(p0))
- }, IndexedSeq(-1)) // ((x,y)=(x',y')) |- ({{x,y},{x,x}}={{x',y'},{x',x'}})
- val pa2_1 = SCSubproof({
- instantiateForall(SCProof(IndexedSeq(), IndexedSeq(p1)), pairxy, pairxx, pairxy1, pairxx1)
- }, IndexedSeq(-2)) // ({{x,y},{x,x}}={{x',y'},{x',x'}}) => ((({x',x'}={x,y})∧({x',y'}={x,x}))∨(({x,x}={x',x'})∧({x,y}={x',y'})))
- val pr2_0 = SCProof(modusPonens(pa2_0.bot.right.head)(pa2_0, pa2_1).steps, IndexedSeq(p0, p1)) // ((x,y)=(x',y')) |- (({x',x'}={x,y})∧({x',y'}={x,x}))∨(({x,x}={x',x'})∧({x,y}={x',y'}))
- val (f, g) = pr2_0.conclusion.right.head match {
- case BinaryConnectorFormula(`or`, l, r) => (l, r)
- }
- val pr2_1: SCProof = destructRightOr(pr2_0, f, g) // ((x,y)=(x',y')) |- (({x',x'}={x,y})∧({x',y'}={x,x})), (({x,x}={x',x'})∧({x,y}={x',y'}))
- val pb2_0 = SCSubproof({
- val prb2_0_0 = instantiateForall(SCProof(IndexedSeq(), IndexedSeq(p1)), x, y, x1, x1) // |- (({x,y}={x',x'}) ⇒ (((x'=y)∧(x'=x))∨((x=x')∧(y=x'))))
- val f = (x1 === y) /\ (x1 === x)
- val prb2_0_1 = destructRightImplies(prb2_0_0, pairxy === pairxx1, f \/ f) // (({x,y}={x',x'}) |- ((x'=y)∧(x'=x))∨((x=x')∧(y=x')))
- val pb3_0_0 = SCSubproof(destructRightOr(prb2_0_1, f, f), IndexedSeq(-1)) // (({x,y}={x',x'}) |- (x'=y)∧(x'=x)
- val pb3_0_1 = SCSubproof(destructRightAnd(SCProof(IndexedSeq(), IndexedSeq(pb3_0_0)), x1 === y, x1 === x), IndexedSeq(0)) // (({x,y}={x',x'}) |- x'=y
- val pb3_0_2 = SCSubproof(destructRightAnd(SCProof(IndexedSeq(), IndexedSeq(pb3_0_0)), x1 === x, x1 === y), IndexedSeq(0)) // (({x,y}={x',x'}) |- x'=x
- val pb3_0_3 = RightSubstEq(emptySeq +< (pairxy === pairxx1) +< (x1 === y) +> (y === x), 2, x1, y, z === x, z) // (({x,y}={x',x'}), x'=y |- y=x
- val pb3_0_4 = Cut(emptySeq +< (pairxy === pairxx1) +> (y === x), 1, 3, x1 === y) // {x',x'}={x,y} |- x=y
- SCProof(IndexedSeq(pb3_0_0, pb3_0_1, pb3_0_2, pb3_0_3, pb3_0_4), IndexedSeq(p1))
- }, IndexedSeq(-2)) // {x',x'}={x,y} |- x=y
- val pb2_1 = SCSubproof(destructRightAnd(pr2_1, pairxx1 === pairxy, pairxx === pairxy1), IndexedSeq(-1, -2)) // ((x,y)=(x',y')) |- (({x',x'}={x,y}), (({x,x}={x',x'})∧({x,y}={x',y'}))
- val pb2_2 = Cut(pb2_1.bot -> pb2_0.bot.left.head +> (x === y), 1, 0, pb2_0.bot.left.head) // ((x,y)=(x',y')) |- x=y, (({x,x}={x',x'})∧({x,y}={x',y'}))
- val pc2_0 = SCSubproof(SCProof(IndexedSeq(pb2_0, pb2_1, pb2_2), IndexedSeq(p0, p1)), IndexedSeq(-1, -2)) // ((x,y)=(x',y')) |- x=y, (({x,x}={x',x'})∧({x,y}={x',y'}))
- val pc2_1 = SCSubproof({
- val pc2_1_0 = SCSubproof(destructRightAnd(SCProof(IndexedSeq(), IndexedSeq(pc2_0)), pairxy === pairxy1, pairxx === pairxx1), IndexedSeq(-2)) // ((x,y)=(x',y')) |- x=y, {x,y}={x',y'}
- val pc2_1_1 = SCSubproof(instantiateForall(SCProof(IndexedSeq(), IndexedSeq(p1)), x, y, x1, y1), IndexedSeq(-1)) // (({x,y}={x',y'})⇒(((y'=y)∧(x'=x))∨((x=y')∧(y=x'))))
- val prc2_1_2 = modusPonens(pairxy === pairxy1)(pc2_1_0, pc2_1_1) // ((x,y)=(x',y')) |- x=y, (((y'=y)∧(x'=x))∨((x=y')∧(y=x'))))
- val f = (y1 === y) /\ (x1 === x)
- val g = (y1 === x) /\ (x1 === y)
- val prc2_1_3 = destructRightOr(prc2_1_2, f, g) // ((x,y)=(x',y')) |- x=y, ((y'=x)∧(x'=y)), ((y=y')∧(x=x')))
- val prc2_1_4 = destructRightAnd(prc2_1_3, x1 === y, y1 === x) // ((x,y)=(x',y')) |- x=y, (x'=y), ((y=y')∧(x=x')))
- SCProof(prc2_1_4.steps, IndexedSeq(p1, pc2_0))
- }, IndexedSeq(-2, 0)) // ((x,y)=(x',y')) |- x=y, (x'=y), ((y=y')∧(x=x')))
- val pc2_2 = SCSubproof({
- val pc2_2_0 = SCSubproof(destructRightAnd(SCProof(IndexedSeq(), IndexedSeq(pc2_0)), pairxx === pairxx1, pairxy === pairxy1), IndexedSeq(-2)) // ((x,y)=(x',y')) |- x=y, {x,x}={x',x'}
- val pc2_2_1 = SCSubproof(instantiateForall(SCProof(IndexedSeq(), IndexedSeq(p1)), x, x, x1, x1), IndexedSeq(-1)) // (({x,x}={x',x'})⇒(((x'=x)∧(x'=x))∨((x=x')∧(x=x'))))
- val prc2_2_2 = modusPonens(pairxx === pairxx1)(pc2_2_0, pc2_2_1) // ((x,y)=(x',y')) |- x=y, (((x'=x)∧(x'=x))∨((x=x')∧(x=x'))))
- val f = (x === x1) /\ (x1 === x)
- val prc2_2_3 = destructRightOr(prc2_2_2, f, f) // ((x,y)=(x',y')) |- x=y, ((x'=x)∧(x'=x))
- val prc2_2_4 = destructRightAnd(prc2_2_3, x === x1, x === x1) // ((x,y)=(x',y')) |- x=y, x'=x
- SCProof(prc2_2_4.steps, IndexedSeq(p1, pc2_0))
- }, IndexedSeq(-2, 0)) // ((x,y)=(x',y')) |- x=y, x'=x
- val pc2_3 = RightSubstEq(pc2_1.bot -> (x1 === y) +> (x === y) +< (x1 === x), 1, x, x1, z === y, z) // ((x,y)=(x',y')), x=x' |- x=y, ((y=y')∧(x=x')))
- val pc2_4 = Cut(pc2_3.bot -< (x === x1), 2, 3, x === x1) // ((x,y)=(x',y')) |- x=y, ((y=y')∧(x=x')))
- val pc2_5 = LeftNot(pc2_4.bot +< !(x === y) -> (x === y), 4, x === y) // ((x,y)=(x',y')), !x=y |- ((y=y')∧(x=x')))
- SCSubproof(SCProof(IndexedSeq(pc2_0, pc2_1, pc2_2, pc2_3, pc2_4, pc2_5), IndexedSeq(p0, p1)), IndexedSeq(-1, -2))
- } // ((x,y)=(x',y')), !x=y |- x=x' /\ y=y'
- ).steps, IndexedSeq(p0, p1)), IndexedSeq(0, 1)) // ((x,y)=(x',y')) |- x=x' /\ y=y'
- SCProof(p0, p1, p2)
- ???
- } // |- (x,y)=(x', y') ===> x=x' /\ y=y'
- */
-
- def main(args: Array[String]): Unit = {
-
- println("\nproofUnorderedPairSymmetry")
- checkProof(proofUnorderedPairSymmetry)
- println("\nproofUnorderedPairDeconstruction")
- checkProof(proofUnorderedPairDeconstruction)
- }
-}
diff --git a/src/main/scala/proven/MainLibrary.scala b/src/main/scala/proven/MainLibrary.scala
index c0c1c45a5334c955c460817569ab69f6d25a7944..31951ca0cce16881aa6297851cd2c5c1eb9853af 100644
--- a/src/main/scala/proven/MainLibrary.scala
+++ b/src/main/scala/proven/MainLibrary.scala
@@ -2,11 +2,11 @@ package proven
import lisa.kernel.proof.RunningTheory
import lisa.settheory.AxiomaticSetTheory
-import lisa.settheory.SetTheoryTGAxioms
+import lisa.settheory.SetTheoryDefinitions
import utilities.Library
-abstract class MainLibrary extends Library(AxiomaticSetTheory.runningSetTheory) with SetTheoryTGAxioms {
+abstract class MainLibrary extends Library(AxiomaticSetTheory.runningSetTheory) with SetTheoryDefinitions {
import AxiomaticSetTheory.*
- override val output: String => Unit = println
+ override val realOutput: String => Unit = println
}
diff --git a/src/main/scala/proven/SetTheory.scala b/src/main/scala/proven/SetTheory.scala
index 84fae876c44e24aeb03f498eccd9ecbf2536b59f..6279f36cc8020a8eb360ea380b9b43bc43c0ce85 100644
--- a/src/main/scala/proven/SetTheory.scala
+++ b/src/main/scala/proven/SetTheory.scala
@@ -3,29 +3,791 @@ package proven
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.RunningTheory
import lisa.kernel.proof.RunningTheoryJudgement
-import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SequentCalculus.*
import lisa.settheory.AxiomaticSetTheory
import lisa.settheory.AxiomaticSetTheory.*
-import utilities.Helpers.{_, given}
+import utilities.Helpers.{*, given}
+import proven.tactics.Destructors.*
+import proven.tactics.ProofTactics.*
-trait SetTheory extends MainLibrary {
- private val x = SchematicFunctionLabel("x", 0)
- private val y = SchematicFunctionLabel("y", 0)
- private val z = SchematicFunctionLabel("z", 0)
- private val x_ = VariableLabel("x")
- private val y_ = VariableLabel("y")
- private val z_ = VariableLabel("z")
+object SetTheory extends MainLibrary {
- THEOREM("russelParadox") of ("∀x. (x ∈ ?y) ↔ ¬(x ∈ x) ⊢") PROOF {
+ THEOREM("russelParadox") of "∀x. (x ∈ ?y) ↔ ¬(x ∈ x) ⊢" PROOF {
+ val y = SchematicFunctionLabel("y", 0)
+ val x_ = VariableLabel("x")
val contra = in(y, y) <=> !in(y, y)
val s0 = Hypothesis(contra |- contra, contra)
val s1 = LeftForall(forall(x_, in(x_, y) <=> !in(x_, x_)) |- contra, 0, in(x_, y) <=> !in(x_, x_), x_, y)
val s2 = Rewrite(forall(x_, in(x_, y) <=> !in(x_, x_)) |- (), 1)
- SCProof(s0, s1, s2)
+ Proof(s0, s1, s2)
} using ()
+ thm"russelParadox".show
- thm"russelParadox".show()
-}
+ THEOREM("unorderedPair_symmetry") of
+ "⊢ ∀y, x. {x, y} = {y, x}" PROOF {
+ val x = VariableLabel("x")
+ val y = VariableLabel("y")
+ val z = VariableLabel("z")
+ val h = SchematicPredicateLabel("h", 0)
+ val fin = SCSubproof({
+ val pr0 = SCSubproof({
+ val pairSame11 = instantiateForall(new Proof(steps(), imports(ax"pairAxiom")), pairAxiom, x)
+ val pairSame12 = instantiateForall(pairSame11, pairSame11.conclusion.right.head, y)
+ instantiateForall(pairSame12, pairSame12.conclusion.right.head, z)
+ }, Seq(-1))
+ val pr1 = SCSubproof({
+ val pairSame21 = instantiateForall(new Proof(steps(), imports(ax"pairAxiom")), pairAxiom, y)
+ val pairSame22 = instantiateForall(pairSame21, pairSame21.conclusion.right.head, x)
+ instantiateForall(pairSame22, pairSame22.conclusion.right.head, z)
+ }, Seq(-1))
+ val pr2 = RightSubstIff(
+ Sequent(pr1.bot.right, Set(in(z, pair(x, y)) <=> in(z, pair(y, x)))),
+ 0,
+ List(((x === z) \/ (y === z), in(z, pair(y, x)))),
+ LambdaFormulaFormula(Seq(h), in(z, pair(x, y)) <=> h())
+ )
+ val pr3 = Cut(Sequent(pr1.bot.left, pr2.bot.right), 1, 2, pr2.bot.left.head)
+ val pr4 = RightForall(Sequent(Set(), Set(forall(z, pr2.bot.right.head))), 3, pr2.bot.right.head, z)
+ Proof(steps(pr0, pr1, pr2, pr3, pr4), imports(ax"pairAxiom"))
+ }, Seq(-2))
+ val pairExt = SCSubproof({
+ val pairExt1 = instantiateForall(Proof(steps(), imports(ax"extensionalityAxiom")), ax"extensionalityAxiom", pair(x, y))
+ instantiateForall(pairExt1, pairExt1.conclusion.right.head, pair(y, x))
+ }, Seq(-1))
+ val fin2 = byEquiv(
+ pairExt.bot.right.head,
+ fin.bot.right.head
+ )(pairExt, fin)
+ val fin3 = generalizeToForall(fin2, fin2.conclusion.right.head, x)
+ val fin4 = generalizeToForall(fin3, fin3.conclusion.right.head, y)
+ fin4.copy(imports = imports(ax"extensionalityAxiom", ax"pairAxiom"))
+ } using (ax"extensionalityAxiom", AxiomaticSetTheory.pairAxiom)
+ show
+
+ //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 {
+ val x = VariableLabel("x")
+ val y = VariableLabel("y")
+ val x1 = VariableLabel("x'")
+ val y1 = VariableLabel("y'")
+ val z = VariableLabel("z")
+ val g = SchematicFunctionLabel("g", 0)
+ val h = SchematicPredicateLabel("h", 0)
+ val pxy = pair(x, y)
+ val pxy1 = pair(x1, y1)
+ val p0 = SCSubproof(
+ {
+ val p0 = SCSubproof(
+ {
+ val zf = in(z, pxy)
+ val p1_0 = hypothesis(zf)
+ val p1_1 = RightImplies(emptySeq +> (zf ==> zf), 0, zf, zf)
+ val p1_2 = RightIff(emptySeq +> (zf <=> zf), 1, 1, zf, zf) // |- (z in {x,y} <=> z in {x,y})
+ val p1_3 = RightSubstEq(emptySeq +< (pxy === pxy1) +> (zf <=> in(z, pxy1)), 2, List((pxy, pxy1)), LambdaTermFormula(Seq(g), zf <=> in(z, g())))
+ Proof(IndexedSeq(p1_0, p1_1, p1_2, p1_3), IndexedSeq(() |- pairAxiom))
+ },
+ Seq(-1),
+ display = true
+ ) // ({x,y}={x',y'}) |- ((z∈{x,y})↔(z∈{x',y'}))
+ val p1 = SCSubproof(
+ {
+ val p1_0 = Rewrite(() |- pairAxiom, -1) // |- ∀∀∀((z$1∈{x$3,y$2})↔((x$3=z$1)∨(y$2=z$1)))
+ val p1_1 = instantiateForall(Proof(IndexedSeq(p1_0), IndexedSeq(() |- pairAxiom)), x, y, z)
+ p1_1
+ },
+ Seq(-1),
+ display = true
+ ) // |- (z in {x,y}) <=> (z=x \/ z=y)
+ val p2 = SCSubproof(
+ {
+ val p2_0 = Rewrite(() |- pairAxiom, -1) // |- ∀∀∀((z$1∈{x$3,y$2})↔((x$3=z$1)∨(y$2=z$1)))
+ val p2_1 = instantiateForall(Proof(IndexedSeq(p2_0), IndexedSeq(() |- pairAxiom)), x1, y1, z)
+ p2_1
+ },
+ Seq(-1),
+ ) // |- (z in {x',y'}) <=> (z=x' \/ z=y')
+ val p3 = RightSubstEq(
+ emptySeq +< (pxy === pxy1) +> (in(z, pxy1) <=> ((z === x) \/ (z === y))),
+ 1,
+ List((pxy, pxy1)),
+ LambdaTermFormula(Seq(g), in(z, g()) <=> ((z === x) \/ (z === y)))
+ ) // ({x,y}={x',y'}) |- ((z∈{x',y'})↔((z=x)∨(z=y)))
+ val p4 = RightSubstIff(
+ emptySeq +< p3.bot.left.head +< p2.bot.right.head +> (((z === x) \/ (z === y)) <=> ((z === x1) \/ (z === y1))),
+ 3,
+ List(((z === x1) \/ (z === y1), in(z, pxy1))),
+ LambdaFormulaFormula(Seq(h), h() <=> ((z === x) \/ (z === y)))
+ ) // ((z∈{x',y'})↔((x'=z)∨(y'=z))), ({x,y}={x',y'}) |- (((z=x)∨(z=y))↔((z=x')∨(z=y')))
+ val p5 = Cut(emptySeq ++< p3.bot ++> p4.bot, 2, 4, p2.bot.right.head)
+ Proof(IndexedSeq(p0, p1, p2, p3, p4, p5), IndexedSeq(() |- pairAxiom))
+ },
+ Seq(-1)
+ ) // ({x,y}={x',y'}) |- (((z=x)∨(z=y))↔((z=x')∨(z=y')))
+
+ val p1 = SCSubproof(
+ Proof(
+ byCase(x === x1)(
+ SCSubproof(
+ {
+ val pcm1 = p0
+ val pc0 = SCSubproof(
+ Proof(
+ byCase(y === x)(
+ SCSubproof(
+ {
+ val pam1 = pcm1
+ val pa0 = SCSubproof(
+ {
+ val f1 = z === x
+ val pa0_m1 = pcm1 // ({x,y}={x',y'}) |- (((z=x)∨(z=y))↔((z=x')∨(z=y')))
+ val pa0_0 = SCSubproof(
+ {
+ val pa0_0_0 = hypothesis(f1)
+ val pa0_1_1 = RightOr(emptySeq +< f1 +> (f1 \/ f1), 0, f1, f1)
+ val pa0_1_2 = RightImplies(emptySeq +> (f1 ==> (f1 \/ f1)), 1, f1, f1 \/ f1)
+ val pa0_1_3 = LeftOr(emptySeq +< (f1 \/ f1) +> f1, Seq(0, 0), Seq(f1, f1))
+ val pa0_1_4 = RightImplies(emptySeq +> ((f1 \/ f1) ==> f1), 3, f1 \/ f1, f1)
+ val pa0_1_5 = RightIff(emptySeq +> ((f1 \/ f1) <=> f1), 2, 4, (f1 \/ f1), f1)
+ val r = Proof(pa0_0_0, pa0_1_1, pa0_1_2, pa0_1_3, pa0_1_4, pa0_1_5)
+ r
+ },
+ display = false
+ ) // |- (((z=x)∨(z=x))↔(z=x))
+ val pa0_1 = RightSubstEq(
+ emptySeq +< (pxy === pxy1) +< (x === y) +> ((f1 \/ f1) <=> (z === x1) \/ (z === y1)),
+ -1,
+ List((x, y)),
+ LambdaTermFormula(Seq(g), (f1 \/ (z === g())) <=> ((z === x1) \/ (z === y1)))
+ ) // ({x,y}={x',y'}) y=x|- (z=x)\/(z=x) <=> (z=x' \/ z=y')
+ val pa0_2 = RightSubstIff(
+ emptySeq +< (pxy === pxy1) +< (x === y) +< (f1 <=> (f1 \/ f1)) +> (f1 <=> ((z === x1) \/ (z === y1))),
+ 1,
+ List((f1, f1 \/ f1)),
+ LambdaFormulaFormula(Seq(h), h() <=> ((z === x1) \/ (z === y1)))
+ )
+ val pa0_3 =
+ Cut(emptySeq +< (pxy === pxy1) +< (x === y) +> (f1 <=> ((z === x1) \/ (z === y1))), 0, 2, f1 <=> (f1 \/ f1)) // (x=y), ({x,y}={x',y'}) |- ((z=x)↔((z=x')∨(z=y')))
+ val pa0_4 = RightForall(emptySeq +< (pxy === pxy1) +< (x === y) +> forall(z, f1 <=> ((z === x1) \/ (z === y1))), 3, f1 <=> ((z === x1) \/ (z === y1)), z)
+ val ra0_0 = instantiateForall(Proof(IndexedSeq(pa0_0, pa0_1, pa0_2, pa0_3, pa0_4), IndexedSeq(pa0_m1.bot)), y1) // (x=y), ({x,y}={x',y'}) |- ((y'=x)↔((y'=x')∨(y'=y')))
+ ra0_0
+ },
+ IndexedSeq(-1)
+ ) // ({x,y}={x',y'}) y=x|- ((y'=x)↔((y'=x')∨(y'=y')))
+ val pa1 = SCSubproof(
+ {
+ val pa1_0 = RightRefl(emptySeq +> (y1 === y1), y1 === y1)
+ val pa1_1 = RightOr(emptySeq +> ((y1 === y1) \/ (y1 === x1)), 0, y1 === y1, y1 === x1)
+ Proof(pa1_0, pa1_1)
+ },
+ display = false
+ ) // |- (y'=x' \/ y'=y')
+ val ra3 = byEquiv(pa0.bot.right.head, pa1.bot.right.head)(pa0, pa1) // ({x,y}={x',y'}) y=x|- ((y'=x)
+ val pal = RightSubstEq(emptySeq ++< pa0.bot +> (y1 === y), ra3.length - 1, List((x, y)), LambdaTermFormula(Seq(g), y1 === g()))
+ Proof(ra3.steps, IndexedSeq(pam1.bot)).appended(pal) // (x=y), ({x,y}={x',y'}) |- (y'=y)
+ },
+ IndexedSeq(-1)
+ ) // (x=y), ({x,y}={x',y'}) |- (y'=y)
+ ,
+ SCSubproof(
+ {
+ val pbm1 = pcm1 // ({x,y}={x',y'}) |- (((z=x)∨(z=y))↔((z=x')∨(z=y')))
+ val pb0_0 = SCSubproof(
+ {
+ val pb0_0 = RightForall(emptySeq ++< pcm1.bot +> forall(z, pcm1.bot.right.head), -1, pcm1.bot.right.head, z)
+ instantiateForall(Proof(IndexedSeq(pb0_0), IndexedSeq(pcm1.bot)), y)
+ },
+ IndexedSeq(-1)
+ ) // ({x,y}={x',y'}) |- (((y=x)∨(y=y))↔((y=x')∨(y=y')))
+ val pb0_1 = SCSubproof(
+ {
+ val pa1_0 = RightRefl(emptySeq +> (y === y), y === y)
+ val pa1_1 = RightOr(emptySeq +> ((y === y) \/ (y === x)), 0, y === y, y === x)
+ Proof(pa1_0, pa1_1)
+ },
+ display = false
+ ) // |- (y=x)∨(y=y)
+ val rb0 = byEquiv(pb0_0.bot.right.head, pb0_1.bot.right.head)(pb0_0, pb0_1) // ({x,y}={x',y'}) |- (y=x')∨(y=y')
+ val pb1 =
+ RightSubstEq(emptySeq ++< rb0.conclusion +< (x === x1) +> ((y === x) \/ (y === y1)), rb0.length - 1, List((x, x1)), LambdaTermFormula(Seq(g), (y === g()) \/ (y === y1)))
+ val rb1 = destructRightOr(
+ rb0.appended(pb1), // ({x,y}={x',y'}) , x=x'|- (y=x)∨(y=y')
+ y === x,
+ y === y1
+ )
+ val rb2 = rb1.appended(LeftNot(rb1.conclusion +< !(y === x) -> (y === x), rb1.length - 1, y === x)) // (x=x'), ({x,y}={x',y'}), ¬(y=x) |- (y=y')
+ Proof(rb2.steps, IndexedSeq(pbm1.bot))
+
+ },
+ IndexedSeq(-1)
+ ) // ({x,y}={x',y'}), x=x', !y=x |- y=y'
+ ).steps,
+ IndexedSeq(pcm1.bot)
+ ),
+ IndexedSeq(-1)
+ ) // (x=x'), ({x,y}={x',y'}) |- (y'=y)
+ val pc1 = RightRefl(emptySeq +> (x === x), x === x)
+ val pc2 = RightAnd(emptySeq ++< pc0.bot +> ((y1 === y) /\ (x === x)), Seq(0, 1), Seq(y1 === y, x === x)) // ({x,y}={x',y'}), x=x' |- (x=x /\ y=y')
+ val pc3 =
+ RightSubstEq(emptySeq ++< pc2.bot +> ((y1 === y) /\ (x1 === x)), 2, List((x, x1)), LambdaTermFormula(Seq(g), (y1 === y) /\ (g() === x))) // ({x,y}={x',y'}), x=x' |- (x=x' /\ y=y')
+ val pc4 = RightOr(
+ emptySeq ++< pc3.bot +> (pc3.bot.right.head \/ ((x === y1) /\ (y === x1))),
+ 3,
+ pc3.bot.right.head,
+ (x === y1) /\ (y === x1)
+ ) // ({x,y}={x',y'}), x=x' |- (x=x' /\ y=y')\/(x=y' /\ y=x')
+ val r = Proof(IndexedSeq(pc0, pc1, pc2, pc3, pc4), IndexedSeq(pcm1.bot))
+ r
+ },
+ IndexedSeq(-1)
+ ) // ({x,y}={x',y'}), x=x' |- (x=x' /\ y=y')\/(x=y' /\ y=x')
+ ,
+ SCSubproof(
+ {
+ val pdm1 = p0
+ val pd0 = SCSubproof(
+ {
+ val pd0_m1 = pdm1
+ val pd0_0 = SCSubproof {
+ val ex1x1 = x1 === x1
+ val pd0_0_0 = RightRefl(emptySeq +> ex1x1, ex1x1) // |- x'=x'
+ val pd0_0_1 = RightOr(emptySeq +> (ex1x1 \/ (x1 === y1)), 0, ex1x1, x1 === y1) // |- (x'=x' \/ x'=y')
+ Proof(IndexedSeq(pd0_0_0, pd0_0_1))
+ } // |- (x'=x' \/ x'=y')
+ val pd0_1 = SCSubproof(
+ {
+ val pd0_1_m1 = pd0_m1 // ({x,y}={x',y'}) |- (((z=x)∨(z=y))↔((z=x')∨(z=y')))
+ val pd0_1_0 = RightForall(emptySeq ++< pd0_1_m1.bot +> forall(z, pd0_1_m1.bot.right.head), -1, pd0_1_m1.bot.right.head, z)
+ val rd0_1_1 = instantiateForall(Proof(IndexedSeq(pd0_1_0), IndexedSeq(pd0_m1.bot)), x1) // ({x,y}={x',y'}) |- (x'=x \/ x'=y) <=> (x'=x' \/ x'=y')
+ rd0_1_1
+ },
+ IndexedSeq(-1)
+ ) // ({x,y}={x',y'}) |- (x'=x \/ x'=y) <=> (x'=x' \/ x'=y')
+ val pd0_2 = RightSubstIff(
+ pd0_1.bot.right |- ((x1 === x) \/ (x1 === y)),
+ 0,
+ List(((x1 === x) \/ (x1 === y), (x1 === x1) \/ (x1 === y1))),
+ LambdaFormulaFormula(Seq(h), h())
+ ) // (x'=x \/ x'=y) <=> (x'=x' \/ x'=y') |- (x'=x \/ x'=y)
+ val pd0_3 = Cut(pd0_1.bot.left |- pd0_2.bot.right, 1, 2, pd0_1.bot.right.head) // ({x,y}={x',y'}) |- (x=x' \/ y=x')
+ destructRightOr(Proof(IndexedSeq(pd0_0, pd0_1, pd0_2, pd0_3), IndexedSeq(pd0_m1.bot)), x === x1, y === x1) // ({x,y}={x',y'}) |- x=x', y=x'
+ },
+ IndexedSeq(-1)
+ ) // ({x,y}={x',y'}) |- x=x', y=x' --
+ val pd1 = SCSubproof(
+ {
+ val pd1_m1 = pdm1
+ val pd1_0 = SCSubproof {
+ val exx = x === x
+ val pd1_0_0 = RightRefl(emptySeq +> exx, exx) // |- x=x
+ val pd1_0_1 = RightOr(emptySeq +> (exx \/ (x === y)), 0, exx, x === y) // |- (x=x \/ x=y)
+ Proof(IndexedSeq(pd1_0_0, pd1_0_1))
+ } // |- (x=x \/ x=y)
+ val pd1_1 = SCSubproof(
+ {
+ val pd1_1_m1 = pd1_m1 // ({x,y}={x',y'}) |- (((z=x)∨(z=y))↔((z=x')∨(z=y')))
+ val pd1_1_0 = RightForall(emptySeq ++< pd1_1_m1.bot +> forall(z, pd1_1_m1.bot.right.head), -1, pd1_1_m1.bot.right.head, z)
+ val rd1_1_1 = instantiateForall(Proof(IndexedSeq(pd1_1_0), IndexedSeq(pd1_m1.bot)), x) // ({x,y}={x',y'}) |- (x=x \/ x=y) <=> (x=x' \/ x=y')
+ rd1_1_1
+ },
+ IndexedSeq(-1)
+ ) // // ({x,y}={x',y'}) |- (x=x \/ x=y) <=> (x=x' \/ x=y')
+ val rd1_2 = byEquiv(pd1_1.bot.right.head, pd1_0.bot.right.head)(pd1_1, pd1_0)
+ val pd1_3 = SCSubproof(Proof(rd1_2.steps, IndexedSeq(pd1_m1.bot)), IndexedSeq(-1)) // // ({x,y}={x',y'}) |- x=x' \/ x=y'
+ destructRightOr(Proof(IndexedSeq(pd1_0, pd1_1, pd1_3), IndexedSeq(pd1_m1.bot)), x === x1, x === y1) // ({x,y}={x',y'}) |- x=x', x=y'
+ },
+ IndexedSeq(-1)
+ ) // ({x,y}={x',y'}) |- x=x', x=y' --
+ val pd2 = RightAnd(emptySeq ++< pd1.bot +> (x === x1) +> ((x === y1) /\ (y === x1)), Seq(0, 1), Seq(x === y1, y === x1)) // ({x,y}={x',y'}) |- x=x', (x=y' /\ y=x') ---
+ val pd3 = LeftNot(emptySeq ++< pd2.bot +< !(x === x1) +> ((x === y1) /\ (y === x1)), 2, x === x1) // ({x,y}={x',y'}), !x===x1 |- (x=y' /\ y=x')
+ val pd4 = RightOr(
+ emptySeq ++< pd3.bot +> (pd3.bot.right.head \/ ((x === x1) /\ (y === y1))),
+ 3,
+ pd3.bot.right.head,
+ (x === x1) /\ (y === y1)
+ ) // ({x,y}={x',y'}), !x===x1 |- (x=x' /\ y=y')\/(x=y' /\ y=x')
+ Proof(IndexedSeq(pd0, pd1, pd2, pd3, pd4), IndexedSeq(pdm1.bot))
+ },
+ IndexedSeq(-1)
+ ) // ({x,y}={x',y'}), !x=x' |- (x=x' /\ y=y')\/(x=y' /\ y=x')
+ ).steps,
+ IndexedSeq(p0.bot)
+ ),
+ IndexedSeq(0)
+ ) // ({x,y}={x',y'}) |- (x=x' /\ y=y')\/(x=y' /\ y=x')
+
+ 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(Proof(IndexedSeq(p0, p1, p2), IndexedSeq(() |- pairAxiom)), x, y, x1, y1)
+ } using ax"pairAxiom"
+ thm"unorderedPair_deconstruction".show
+
+ THEOREM("noUniversalSet") of "∀x. x ∈ ?z ⊢" PROOF {
+ val x = SchematicFunctionLabel("x", 0)
+ val z = SchematicFunctionLabel("z", 0)
+ val x1 = VariableLabel("x")
+ val y1 = VariableLabel("y")
+ val z1 = VariableLabel("z")
+ val h = SchematicPredicateLabel("h", 0)
+ val sPhi = SchematicPredicateLabel("P", 2)
+ // forall(z, exists(y, forall(x, in(x,y) <=> (in(x,y) /\ sPhi(x,z)))))
+ val i1 = () |- comprehensionSchema
+ val i2 = thm"russelParadox" // forall(x1, in(x1,y) <=> !in(x1, x1)) |- ()
+ val p0 = InstPredSchema(() |- forall(z1, exists(y1, forall(x1, in(x1, y1) <=> (in(x1, z1) /\ !in(x1, x1))))), -1, Map(sPhi -> LambdaTermFormula(Seq(x, z), !in(x(), x()))))
+ val s0 = SCSubproof(instantiateForall(Proof(IndexedSeq(p0), IndexedSeq(i1)), z), Seq(-1)) // exists(y1, forall(x1, in(x1,y1) <=> (in(x1,z1) /\ !in(x1, x1))))
+ val s1 = hypothesis(in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1))) // in(x,y) <=> (in(x,z) /\ in(x, x)) |- in(x,y) <=> (in(x,z) /\ in(x, x))
+ val s2 = RightSubstIff(
+ (in(x1, z) <=> And(), in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1))) |- in(x1, y1) <=> (And() /\ !in(x1, x1)),
+ 1,
+ List((in(x1, z), And())),
+ LambdaFormulaFormula(Seq(h), in(x1, y1) <=> (h() /\ !in(x1, x1)))
+ ) // in(x1,y1) <=> (in(x1,z1) /\ in(x1, x1)) |- in(x,y) <=> (And() /\ in(x1, x1))
+ val s3 = Rewrite((in(x1, z), in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1))) |- in(x1, y1) <=> !in(x1, x1), 2)
+ val s4 = LeftForall((forall(x1, in(x1, z)), in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1))) |- in(x1, y1) <=> !in(x1, x1), 3, in(x1, z), x1, x1)
+ val s5 = LeftForall((forall(x1, in(x1, z)), forall(x1, in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1)))) |- in(x1, y1) <=> !in(x1, x1), 4, in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1)), x1, x1)
+ val s6 = RightForall((forall(x1, in(x1, z)), forall(x1, in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1)))) |- forall(x1, in(x1, y1) <=> !in(x1, x1)), 5, in(x1, y1) <=> !in(x1, x1), x1)
+ val s7 = InstFunSchema(forall(x1, in(x1, y1) <=> !in(x1, x1)) |- (), -2, Map(SchematicFunctionLabel("y", 0) -> LambdaTermTerm(Nil, y1)))
+ val s8 = Cut((forall(x1, in(x1, z)), forall(x1, in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1)))) |- (), 6, 7, forall(x1, in(x1, y1) <=> !in(x1, x1)))
+ val s9 = LeftExists((forall(x1, in(x1, z)), exists(y1, forall(x1, in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1))))) |- (), 8, forall(x1, in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1))), y1)
+ val s10 = Cut(forall(x1, in(x1, z)) |- (), 0, 9, exists(y1, forall(x1, in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1)))))
+ Proof(steps(s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10), imports(i1, i2))
+ } using (ax"comprehensionSchema", thm"russelParadox")
+ show
+
+ private val sx = SchematicFunctionLabel("x", 0)
+ private val sy = SchematicFunctionLabel("y", 0)
+ val oPair: ConstantFunctionLabel = DEFINE("", sx, sy) as pair(pair(sx, sy), pair(sx, sx))
+ show
+
+ THEOREM("functionalMapping") of
+ "∀a. (a ∈ ?A) ⇒ ∃!x. ?phi(x, a) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ ?A) ∧ ?phi(x, a)" PROOF {
+ val a = VariableLabel("a")
+ val b = VariableLabel("b")
+ val x = VariableLabel("x")
+ val y = VariableLabel("y")
+ val z = VariableLabel("z")
+ val a1 = SchematicFunctionLabel("a", 0)
+ val b1 = SchematicFunctionLabel("b", 0)
+ val x1 = SchematicFunctionLabel("x", 0)
+ val y1 = SchematicFunctionLabel("y", 0)
+ val z1 = SchematicFunctionLabel("z", 0)
+ val f = SchematicFunctionLabel("f", 0)
+ val h = SchematicPredicateLabel("h", 0)
+ val A = SchematicFunctionLabel("A", 0)()
+ val X = VariableLabel("X")
+ val B = VariableLabel("B")
+ val B1 = VariableLabel("B1")
+ val phi = SchematicPredicateLabel("phi", 2)
+ val sPhi = SchematicPredicateLabel("P", 2)
+ val sPsi = SchematicPredicateLabel("P", 3)
+
+ val H = existsOne(x, phi(x, a))
+ val H1 = forall(a, in(a, A) ==> H)
+ val s0 = hypothesis(H) // () |- existsOne(x, phi(x, a)))
+ val s1 = Weakening((H, in(a, A)) |- existsOne(x, phi(x, a)), 0)
+ val s2 = Rewrite((H) |- in(a, A) ==> existsOne(x, phi(x, a)), 1)
+ // val s3 = RightForall((H) |- forall(a, in(a, A) ==> existsOne(x, phi(x, a))), 2, in(a, A) ==> existsOne(x, phi(x, a)), a) // () |- ∀a∈A. ∃!x. phi(x, a)
+ val s3 = hypothesis(H1)
+ val i1 = () |- replacementSchema
+ val p0 = InstPredSchema(
+ () |- instantiatePredicateSchemas(replacementSchema, Map(sPsi -> LambdaTermFormula(Seq(y1, a1, x1), phi(x1, a1)))),
+ -1,
+ Map(sPsi -> LambdaTermFormula(Seq(y1, a1, x1), phi(x1, a1)))
+ )
+ val p1 = instantiateForall(Proof(steps(p0), imports(i1)), A)
+ val s4 = SCSubproof(p1, Seq(-1)) //
+ val s5 = Rewrite(s3.bot.right.head |- exists(B, forall(x, in(x, A) ==> exists(y, in(y, B) /\ (phi(y, x))))), 4)
+ val s6 = Cut((H1) |- exists(B, forall(x, in(x, A) ==> exists(y, in(y, B) /\ (phi(y, x))))), 3, 5, s3.bot.right.head) // ⊢ ∃B. ∀x. (x ∈ A) ⇒ ∃y. (y ∈ B) ∧ (y = (x, b))
+
+ val i2 = () |- comprehensionSchema // forall(z, exists(y, forall(x, in(x,y) <=> (in(x,z) /\ sPhi(x,z)))))
+ val q0 = InstPredSchema(
+ () |- instantiatePredicateSchemas(comprehensionSchema, Map(sPhi -> LambdaTermFormula(Seq(x1, z1), exists(a, in(a, A) /\ phi(x1, a))))),
+ -1,
+ Map(sPhi -> LambdaTermFormula(Seq(x1, z1), exists(a, in(a, A) /\ phi(x1, a))))
+ )
+ val q1 = instantiateForall(Proof(steps(q0), imports(i2)), B)
+ val s7 = SCSubproof(q1, Seq(-2)) // ∃y. ∀x. (x ∈ y) ↔ (x ∈ B) ∧ ∃a. a ∈ A /\ x = (a, b) := exists(y, F(y) )
+ Proof(steps(s0, s1, s2, s3, s4, s5, s6, s7), imports(i1, i2))
+ val s8 = SCSubproof({
+ val y1 = VariableLabel("y1")
+ val f = SchematicFunctionLabel("f", 0)
+ val s0 = hypothesis(in(y1, B))
+ val s1 = RightSubstEq((in(y1, B), x === y1) |- in(x, B), 0, List((x, y1)), LambdaTermFormula(Seq(f), in(f(), B)))
+ val s2 = LeftSubstIff(Set(in(y1, B), (x === y1) <=> phi(x, a), phi(x, a)) |- in(x, B), 1, List(((x === y1), phi(x, a))), LambdaFormulaFormula(Seq(h), h()))
+ val s3 = LeftSubstEq(Set(y === y1, in(y1, B), (x === y) <=> phi(x, a), phi(x, a)) |- in(x, B), 2, List((y, y1)), LambdaTermFormula(Seq(f), (x === f()) <=> phi(x, a)))
+ val s4 = LeftSubstIff(Set((y === y1) <=> phi(y1, a), phi(y1, a), in(y1, B), (x === y) <=> phi(x, a), phi(x, a)) |- in(x, B), 3, List((phi(y1, a), y1 === y)), LambdaFormulaFormula(Seq(h), h()))
+ val s5 = LeftForall(Set(forall(x, (y === x) <=> phi(x, a)), phi(y1, a), in(y1, B), (x === y) <=> phi(x, a), phi(x, a)) |- in(x, B), 4, (y === x) <=> phi(x, a), x, y1)
+ val s6 = LeftForall(Set(forall(x, (y === x) <=> phi(x, a)), phi(y1, a), in(y1, B), phi(x, a)) |- in(x, B), 5, (x === y) <=> phi(x, a), x, x)
+ val s7 = LeftExists(Set(exists(y, forall(x, (y === x) <=> phi(x, a))), phi(y1, a), in(y1, B), phi(x, a)) |- in(x, B), 6, forall(x, (y === x) <=> phi(x, a)), y)
+ val s8 = Rewrite(Set(exists(y, forall(x, (y === x) <=> phi(x, a))), phi(y1, a) /\ in(y1, B), phi(x, a)) |- in(x, B), 7)
+ val s9 = LeftExists(Set(exists(y, forall(x, (y === x) <=> phi(x, a))), exists(y1, phi(y1, a) /\ in(y1, B)), phi(x, a)) |- in(x, B), 8, phi(y1, a) /\ in(y1, B), y1)
+ val s10 = Rewrite(Set(exists(y, forall(x, (y === x) <=> phi(x, a))), And() ==> exists(y, phi(y, a) /\ in(y, B)), phi(x, a)) |- in(x, B), 9)
+ val s11 = LeftSubstIff(
+ Set(exists(y, forall(x, (y === x) <=> phi(x, a))), in(a, A) ==> exists(y, phi(y, a) /\ in(y, B)), phi(x, a), in(a, A)) |- in(x, B),
+ 10,
+ List((And(), in(a, A))),
+ LambdaFormulaFormula(Seq(h), h() ==> exists(y, phi(y, a) /\ in(y, B)))
+ )
+ val s12 = LeftForall(
+ Set(exists(y, forall(x, (y === x) <=> phi(x, a))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), phi(x, a), in(a, A)) |- in(x, B),
+ 11,
+ in(a, A) ==> exists(y, phi(y, a) /\ in(y, B)),
+ a,
+ a
+ )
+ val s13 = LeftSubstIff(
+ Set(in(a, A) ==> exists(y, forall(x, (y === x) <=> phi(x, a))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), phi(x, a), in(a, A)) |- in(x, B),
+ 12,
+ List((And(), in(a, A))),
+ LambdaFormulaFormula(Seq(h), h() ==> exists(y, forall(x, (y === x) <=> phi(x, a))))
+ )
+ val s14 = LeftForall(
+ Set(forall(a, in(a, A) ==> exists(y, forall(x, (y === x) <=> phi(x, a)))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), phi(x, a), in(a, A)) |- in(x, B),
+ 13,
+ in(a, A) ==> exists(y, forall(x, (y === x) <=> phi(x, a))),
+ a,
+ a
+ )
+ val s15 = Rewrite(Set(forall(a, in(a, A) ==> exists(y, forall(x, (y === x) <=> phi(x, a)))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), phi(x, a) /\ in(a, A)) |- in(x, B), 14)
+ val s16 = LeftExists(
+ Set(forall(a, in(a, A) ==> exists(y, forall(x, (y === x) <=> phi(x, a)))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), exists(a, phi(x, a) /\ in(a, A))) |- in(x, B),
+ 15,
+ phi(x, a) /\ in(a, A),
+ a
+ )
+ val truc = forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B)))
+ val s17 = Rewrite(Set(forall(a, in(a, A) ==> existsOne(x, phi(x, a))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), exists(a, phi(x, a) /\ in(a, A))) |- in(x, B), 16)
+ Proof(steps(s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, s17))
+ // goal H, ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), ∃a. a ∈ A ∧ phi(x, a) |- (x ∈ B)
+ // redGoal ∀a.(a ∈ A) => ∃!x. phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), ∃a. a ∈ A ∧ phi(x, a) |- (x ∈ B) s17
+ // redGoal ∀a.(a ∈ A) => ∃y. ∀x. (x=y) ↔ phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), ∃a. a ∈ A ∧ phi(x, a) |- (x ∈ B) s16
+ // redGoal ∀a.(a ∈ A) => ∃y. ∀x. (x=y) ↔ phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A ∧ phi(x, a) |- (x ∈ B) s15
+ // redGoal ∀a.(a ∈ A) => ∃y. ∀x. (x=y) ↔ phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A, phi(x, a) |- (x ∈ B) s14
+ // redGoal (a ∈ A) => ∃y. ∀x. (x=y) ↔ phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A, phi(x, a) |- (x ∈ B) s13
+ // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A, phi(x, a) |- (x ∈ B) s12
+ // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A, phi(x, a) |- (x ∈ B) s11
+ // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A <=> T, phi(x, a) |- (x ∈ B) s11
+ // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), T ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A <=> T, phi(x, a) |- (x ∈ B) s10
+ // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), ∃y1. y1 ∈ B ∧ phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s9
+ // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), y1 ∈ B ∧ phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s8
+ // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), y1 ∈ B, phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s7
+ // redGoal ∀x. (x=y) ↔ phi(x, a), y1 ∈ B, phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s6
+ // redGoal (x=y) ↔ phi(x, a), ∀x. (x=y) ↔ phi(x, a), y1 ∈ B, phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s5
+ // redGoal (x=y) ↔ phi(x, a), (y1=y) ↔ phi(y1, a), y1 ∈ B, phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s4
+ // redGoal (x=y) ↔ phi(x, a), (y1=y) ↔ phi(y1, a), y1 ∈ B, (y1=y), a ∈ A, phi(x, a) |- (x ∈ B) s3
+ // redGoal (x=y1) ↔ phi(x, a), (y1=y) ↔ phi(y1, a), y1 ∈ B, (y1=y), a ∈ A, phi(x, a) |- (x ∈ B) s2
+ // redGoal (x=y1) ↔ phi(x, a), (y1=y) ↔ phi(y1, a), y1 ∈ B, (y1=y), a ∈ A, x=y1 |- (x ∈ B) s1
+ // redGoal (x=y1) ↔ phi(x, a), (y1=y) ↔ phi(y1, a), y1 ∈ B, (y1=y), a ∈ A, x=y1 |- (y1 ∈ B) s0
+
+ }) // H, ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), ∃a. a ∈ A ∧ phi(x, a) |- (x ∈ B)
+
+ val G = forall(a, in(a, A) ==> exists(y, in(y, B) /\ (phi(y, a))))
+ val F = forall(x, iff(in(x, B1), in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a)))))
+ val s9 = SCSubproof({
+ val p0 = instantiateForall(Proof(hypothesis(F)), x)
+ val left = in(x, B1)
+ val right = in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a)))
+ val p1 = p0.withNewSteps(Vector(Rewrite(F |- (left ==> right) /\ (right ==> left), p0.length - 1)))
+ val p2 = destructRightAnd(p1, (right ==> left), (left ==> right)) // F |- in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a))) => in(x, B1)
+ val p3 = p2.withNewSteps(Vector(Rewrite(Set(F, in(x, B), exists(a, in(a, A) /\ (phi(x, a)))) |- in(x, B1), p2.length - 1)))
+ p3
+ }) // have F, (x ∈ B), ∃a. a ∈ A ∧ x = (a, b) |- (x ∈ B1)
+ val s10 = Cut(Set(F, G, H1, exists(a, in(a, A) /\ (phi(x, a)))) |- in(x, B1), 8, 9, in(x, B)) // redGoal F, ∃a. a ∈ A ∧ x = (a, b), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ y = (a, b) |- (x ∈ B1)
+ val s11 = Rewrite(Set(H1, G, F) |- exists(a, in(a, A) /\ (phi(x, a))) ==> in(x, B1), 10) // F |- ∃a. a ∈ A ∧ x = (a, b) => (x ∈ B1) --- half
+ val s12 = SCSubproof({
+ val p0 = instantiateForall(Proof(hypothesis(F)), x)
+ val left = in(x, B1)
+ val right = in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a)))
+ val p1 = p0.withNewSteps(Vector(Rewrite(F |- (left ==> right) /\ (right ==> left), p0.length - 1)))
+ val p2 = destructRightAnd(p1, (left ==> right), (right ==> left)) // F |- in(x, B1) => in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a))) =>
+ val p3 = p2.withNewSteps(Vector(Rewrite(Set(F, in(x, B1)) |- exists(a, in(a, A) /\ (phi(x, a))) /\ in(x, B), p2.length - 1)))
+ val p4 = destructRightAnd(p3, exists(a, in(a, A) /\ (phi(x, a))), in(x, B))
+ val p5 = p4.withNewSteps(Vector(Rewrite(F |- in(x, B1) ==> exists(a, in(a, A) /\ (phi(x, a))), p4.length - 1)))
+ p5
+ }) // have F |- (x ∈ B1) ⇒ ∃a. a ∈ A ∧ x = (a, b) --- other half
+ val s13 = RightIff((H1, G, F) |- in(x, B1) <=> exists(a, in(a, A) /\ (phi(x, a))), 11, 12, in(x, B1), exists(a, in(a, A) /\ (phi(x, a)))) // have F |- (x ∈ B1) <=> ∃a. a ∈ A ∧ x = (a, b)
+ val s14 =
+ RightForall((H1, G, F) |- forall(x, in(x, B1) <=> exists(a, in(a, A) /\ (phi(x, a)))), 13, in(x, B1) <=> exists(a, in(a, A) /\ (phi(x, a))), x) // G, F |- ∀x. (x ∈ B1) <=> ∃a. a ∈ A ∧ x = (a, b)
+
+ val i3 = () |- extensionalityAxiom
+ val s15 = SCSubproof(
+ {
+ val i1 = s13.bot // G, F |- (x ∈ B1) <=> ∃a. a ∈ A ∧ x = (a, b)
+ val i2 = () |- extensionalityAxiom
+ val t0 = RightSubstIff(
+ Set(H1, G, F, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))) |- in(x, X) <=> in(x, B1),
+ -1,
+ List((in(x, X), exists(a, in(a, A) /\ (phi(x, a))))),
+ LambdaFormulaFormula(Seq(h), h() <=> in(x, B1))
+ ) // redGoal2 F, (z ∈ X) <=> ∃a. a ∈ A ∧ z = (a, b) |- (z ∈ X) <=> (z ∈ B1)
+ val t1 = LeftForall(
+ Set(H1, G, F, forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))) |- in(x, X) <=> in(x, B1),
+ 0,
+ in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))),
+ x,
+ x
+ ) // redGoal2 F, [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] |- (z ∈ X) <=> (z ∈ B1)
+ val t2 = RightForall(t1.bot.left |- forall(x, in(x, X) <=> in(x, B1)), 1, in(x, X) <=> in(x, B1), x) // redGoal2 F, [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] |- ∀z. (z ∈ X) <=> (z ∈ B1)
+ val t3 =
+ SCSubproof(instantiateForall(Proof(steps(Rewrite(() |- extensionalityAxiom, -1)), imports(() |- extensionalityAxiom)), X, B1), Vector(-2)) // (∀z. (z ∈ X) <=> (z ∈ B1)) <=> (X === B1)))
+ val t4 = RightSubstIff(
+ t1.bot.left ++ t3.bot.right |- X === B1,
+ 2,
+ List((X === B1, forall(z, in(z, X) <=> in(z, B1)))),
+ LambdaFormulaFormula(Seq(h), h())
+ ) // redGoal2 F, [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)], (∀z. (z ∈ X) <=> (z ∈ B1)) <=> (X === B1))) |- X=B1
+ val t5 = Cut(t1.bot.left |- X === B1, 3, 4, t3.bot.right.head) // redGoal2 F, [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] |- X=B1
+ val t6 = Rewrite(Set(H1, G, F) |- forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))) ==> (X === B1), 5) // F |- [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] ==> X=B1
+ val i3 = s14.bot // F |- ∀x. (x ∈ B1) <=> ∃a. a ∈ A ∧ x = (a, b)
+ val t7 = RightSubstEq(
+ Set(H1, G, F, X === B1) |- forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))),
+ -3,
+ List((X, B1)),
+ LambdaTermFormula(Seq(f), forall(x, in(x, f()) <=> exists(a, in(a, A) /\ phi(x, a))))
+ ) // redGoal1 F, X=B1 |- [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
+ val t8 = Rewrite(
+ Set(H1, G, F) |- X === B1 ==> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))),
+ 7
+ ) // redGoal1 F |- X=B1 ==> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] -------second half with t6
+ val t9 = RightIff(
+ Set(H1, G, F) |- (X === B1) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))),
+ 6,
+ 8,
+ X === B1,
+ forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))
+ ) // goal F |- X=B1 <=> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
+
+ Proof(steps(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9), imports(i1, i2, i3))
+ },
+ Vector(13, -3, 14)
+ ) // goal F |- X=B1 <=> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
+ val s16 = RightForall(
+ (H1, G, F) |- forall(X, (X === B1) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))),
+ 15,
+ (X === B1) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))),
+ X
+ ) // goal F |- ∀X. X=B1 <=> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
+ val s17 = RightExists(
+ (H1, G, F) |- exists(y, forall(X, (X === y) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))))),
+ 16,
+ forall(X, (X === y) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))),
+ y,
+ B1
+ )
+ val s18 = LeftExists((exists(B1, F), G, H1) |- s17.bot.right, 17, F, B1) // ∃B1. F |- ∃B1. ∀X. X=B1 <=> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
+ val s19 = Rewrite(s18.bot.left |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))), 18) // ∃B1. F |- ∃!X. [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
+ val s20 = Cut((G, H1) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))), 7, 19, exists(B1, F))
+ val s21 = LeftExists((H1, exists(B, G)) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))), 20, G, B)
+ val s22 = Cut(H1 |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ phi(x, a)))), 6, 21, exists(B, G))
+ val res = steps(s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, s17, s18, s19, s20, s21, s22)
+ Proof(res, imports(i1, i2, i3))
+ } using (ax"replacementSchema", ax"comprehensionSchema", ax"extensionalityAxiom")
+ 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 {
+ val a = VariableLabel("a")
+ val b = VariableLabel("b")
+ val x = VariableLabel("x")
+ val x1 = VariableLabel("x1")
+ val y = VariableLabel("y")
+ val z = VariableLabel("z")
+ val a_ = SchematicFunctionLabel("a", 0)
+ val b_ = SchematicFunctionLabel("b", 0)
+ val x_ = SchematicFunctionLabel("x", 0)
+ val x1_ = SchematicFunctionLabel("x1", 0)
+ val y_ = SchematicFunctionLabel("y", 0)
+ val z_ = SchematicFunctionLabel("z", 0)
+ val f = SchematicFunctionLabel("f", 0)
+ val h = SchematicPredicateLabel("h", 0)
+ val A = SchematicFunctionLabel("A", 0)()
+ val X = VariableLabel("X")
+ val B = SchematicFunctionLabel("B", 0)()
+ val B1 = VariableLabel("B1")
+ val phi = SchematicPredicateLabel("phi", 2)
+ val psi = SchematicPredicateLabel("psi", 3)
+ val H = existsOne(x, phi(x, a))
+ val H1 = forall(a, in(a, A) ==> H)
+ val i1 = thm"functionalMapping"
+ val H2 = instantiatePredicateSchemas(H1, Map(phi -> LambdaTermFormula(Seq(x_, a_), psi(x_, a_, b))))
+ val s0 = InstPredSchema((H2) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), -1, Map(phi -> LambdaTermFormula(Seq(x_, a_), psi(x_, a_, b))))
+ val s1 = Weakening((H2, in(b, B)) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), 0)
+ val s2 =
+ LeftSubstIff((in(b, B) ==> H2, in(b, B)) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), 1, List((in(b, B), And())), LambdaFormulaFormula(Seq(h), h() ==> H2))
+ val s3 = LeftForall((forall(b, in(b, B) ==> H2), in(b, B)) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), 2, in(b, B) ==> H2, b, b)
+ val s4 = Rewrite(forall(b, in(b, B) ==> H2) |- in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), 3)
+ val s5 = RightForall(
+ forall(b, in(b, B) ==> H2) |- forall(b, in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b))))),
+ 4,
+ in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))),
+ b
+ )
+ val s6 = InstFunSchema(
+ forall(b, in(b, B) ==> existsOne(X, phi(X, b))) |- instantiateFunctionSchemas(i1.right.head, Map(SchematicFunctionLabel("A", 0) -> LambdaTermTerm(Nil, B))),
+ -1,
+ Map(SchematicFunctionLabel("A", 0) -> LambdaTermTerm(Nil, B))
+ )
+ val s7 = InstPredSchema(
+ forall(b, in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b))))) |- existsOne(
+ X,
+ forall(x, in(x, X) <=> exists(b, in(b, B) /\ forall(x1, in(x1, x) <=> exists(a, in(a, A) /\ psi(x1, a, b)))))
+ ),
+ 6,
+ Map(phi -> LambdaTermFormula(Seq(y_, b_), forall(x, in(x, y_) <=> exists(a, in(a, A) /\ psi(x, a, b_)))))
+ )
+ val s8 = Cut(
+ forall(b, in(b, B) ==> H2) |- existsOne(X, forall(x, in(x, X) <=> exists(b, in(b, B) /\ forall(x1, in(x1, x) <=> exists(a, in(a, A) /\ psi(x1, a, b)))))),
+ 5,
+ 7,
+ forall(b, in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))))
+ )
+ Proof(Vector(s0, s1, s2, s3, s4, s5, s6, s7, s8), Vector(i1))
+ // have ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s0
+ // have (b ∈ B), ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s1
+ // have (b ∈ B), (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s2
+ // have (b ∈ B), ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s3
+ // have ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ (b ∈ B) ⇒ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s4
+ // have ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∀b. (b ∈ B) ⇒ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s5
+ // 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
-object SetTheory extends SetTheory {}
+ } using (thm"functionalMapping")
+ show
+
+ THEOREM("applyFunctionToUniqueObject") of
+ "∃!x. ?phi(x) ⊢ ∃!z. ∃x. (z = ?F(x)) ∧ ?phi(x)" PROOF {
+ val x = VariableLabel("x")
+ val x1 = VariableLabel("x1")
+ val z = VariableLabel("z")
+ val z1 = VariableLabel("z1")
+ val F = SchematicFunctionLabel("F", 1)
+ val f = SchematicFunctionLabel("f", 0)
+ val phi = SchematicPredicateLabel("phi", 1)
+ val g = SchematicPredicateLabel("g", 0)
+
+ val g2 = SCSubproof({
+ val s0 = hypothesis(F(x1) === z)
+ val s1 = LeftSubstEq((x === x1, F(x) === z) |- F(x1) === z, 0, List((x, x1)), LambdaTermFormula(Seq(f), F(f()) === z))
+ val s2 = LeftSubstIff(Set(phi(x) <=> (x === x1), phi(x), F(x) === z) |- F(x1) === z, 1, List((x === x1, phi(x))), LambdaFormulaFormula(Seq(g), g()))
+ val s3 = LeftForall(Set(forall(x, phi(x) <=> (x === x1)), phi(x), F(x) === z) |- F(x1) === z, 2, phi(x) <=> (x === x1), x, x)
+ val s4 = Rewrite(Set(forall(x, phi(x) <=> (x === x1)), phi(x) /\ (F(x) === z)) |- F(x1) === z, 3)
+ val s5 = LeftExists(Set(forall(x, phi(x) <=> (x === x1)), exists(x, phi(x) /\ (F(x) === z))) |- F(x1) === z, 4, phi(x) /\ (F(x) === z), x)
+ val s6 = Rewrite(forall(x, phi(x) <=> (x === x1)) |- exists(x, phi(x) /\ (F(x) === z)) ==> (F(x1) === z), 5)
+ Proof(steps(s0, s1, s2, s3, s4, s5, s6))
+ }) // redGoal2 ∀x. x=x1 <=> phi(x) ⊢ ∃x. z=F(x) /\ phi(x) ==> F(x1)=z g2.s5
+
+ val g1 = SCSubproof({
+ val s0 = hypothesis(phi(x1))
+ val s1 = LeftForall(forall(x, (x === x1) <=> phi(x)) |- phi(x1), 0, (x === x1) <=> phi(x), x, x1)
+ val s2 = hypothesis(z === F(x1))
+ val s3 = RightAnd((forall(x, (x === x1) <=> phi(x)), z === F(x1)) |- (z === F(x1)) /\ phi(x1), Seq(2, 1), Seq(z === F(x1), phi(x1)))
+ val s4 = RightExists((forall(x, (x === x1) <=> phi(x)), z === F(x1)) |- exists(x, (z === F(x)) /\ phi(x)), 3, (z === F(x)) /\ phi(x), x, x1)
+ val s5 = Rewrite(forall(x, (x === x1) <=> phi(x)) |- z === F(x1) ==> exists(x, (z === F(x)) /\ phi(x)), 4)
+ Proof(steps(s0, s1, s2, s3, s4, s5))
+ })
+
+ val s0 = g1
+ val s1 = g2
+ val s2 = RightIff(forall(x, (x === x1) <=> phi(x)) |- (z === F(x1)) <=> exists(x, (z === F(x)) /\ phi(x)), 0, 1, z === F(x1), exists(x, (z === F(x)) /\ phi(x)))
+ val s3 = RightForall(forall(x, (x === x1) <=> phi(x)) |- forall(z, (z === F(x1)) <=> exists(x, (z === F(x)) /\ phi(x))), 2, (z === F(x1)) <=> exists(x, (z === F(x)) /\ phi(x)), z)
+ val s4 = RightExists(
+ forall(x, (x === x1) <=> phi(x)) |- exists(z1, forall(z, (z === z1) <=> exists(x, (z === F(x)) /\ phi(x)))),
+ 3,
+ forall(z, (z === z1) <=> exists(x, (z === F(x)) /\ phi(x))),
+ z1,
+ F(x1)
+ )
+ val s5 = LeftExists(exists(x1, forall(x, (x === x1) <=> phi(x))) |- exists(z1, forall(z, (z === z1) <=> exists(x, (z === F(x)) /\ phi(x)))), 4, forall(x, (x === x1) <=> phi(x)), x1)
+ val s6 = Rewrite(existsOne(x, phi(x)) |- existsOne(z, exists(x, (z === F(x)) /\ phi(x))), 5) // goal ∃!x. phi(x) ⊢ ∃!z. ∃x. z=F(x) /\ phi(x)
+ Proof(Vector(s0, s1, s2, s3, s4, s5, s6))
+ } using ()
+ 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 {
+ val a = VariableLabel("a")
+ val b = VariableLabel("b")
+ val x = VariableLabel("x")
+ val x1 = VariableLabel("x1")
+ val x_ = SchematicFunctionLabel("x", 0)
+ val y_ = SchematicFunctionLabel("y", 0)
+ val F = SchematicFunctionLabel("F", 1)
+ val A = SchematicFunctionLabel("A", 0)()
+ val B = SchematicFunctionLabel("B", 0)()
+ val phi = SchematicPredicateLabel("phi", 1)
+ val psi = SchematicPredicateLabel("psi", 3)
+
+ val i1 = thm"lemmaLayeredTwoArgumentsMap"
+ val i2 = thm"applyFunctionToUniqueObject"
+ val rPhi = forall(x, in(x, y_) <=> exists(b, in(b, B) /\ forall(x1, in(x1, x) <=> exists(a, in(a, A) /\ psi(x1, a, b)))))
+ val seq0 = instantiatePredicateSchemaInSequent(i2, Map(phi -> LambdaTermFormula(Seq(y_), rPhi)))
+ val s0 = InstPredSchema(seq0, -2, Map(phi -> LambdaTermFormula(Seq(y_), rPhi))) // val s0 = InstPredSchema(instantiatePredicateSchemaInSequent(i2, phi, rPhi, Seq(X)), -2, phi, rPhi, Seq(X))
+ val seq1 = instantiateFunctionSchemaInSequent(seq0, Map(F -> LambdaTermTerm(Seq(x_), union(x_))))
+ val s1 = InstFunSchema(seq1, 0, Map(F -> LambdaTermTerm(Seq(x_), union(x_))))
+ val s2 = Cut(i1.left |- seq1.right, -1, 1, seq1.left.head)
+ Proof(steps(s0, s1, s2), imports(i1, i2))
+ } using (thm"lemmaLayeredTwoArgumentsMap", thm"applyFunctionToUniqueObject")
+ show
+
+
+
+ val A = SchematicFunctionLabel("A", 0)
+ val B = SchematicFunctionLabel("B", 0)
+ private val sz = SchematicFunctionLabel("z", 0)
+ val cartesianProduct: ConstantFunctionLabel =
+ DEFINE("cartProd", A, B) asThe sz suchThat {
+ val a = VariableLabel("a")
+ val b = VariableLabel("b")
+ val x = VariableLabel("x")
+ val x0 = VariableLabel("x0")
+ val x1 = VariableLabel("x1")
+ val A = SchematicFunctionLabel("A", 0)()
+ val B = SchematicFunctionLabel("B", 0)()
+ exists(x, (sz===union(x)) /\ forall(x0, in(x0, x) <=> exists(b, in(b, B) /\ forall(x1, in(x1, x0) <=> exists(a, in(a, A) /\ (x1 === oPair(a, b)))))))
+ } PROOF {
+ def makeFunctional(t: Term): Proof = {
+ val x = VariableLabel(freshId(t.freeVariables.map(_.id), "x"))
+ val y = VariableLabel(freshId(t.freeVariables.map(_.id), "y"))
+ val s0 = RightRefl(() |- t === t, t === t)
+ val s1 = Rewrite(() |- (x === t) <=> (x === t), 0)
+ val s2 = RightForall(() |- forall(x, (x === t) <=> (x === t)), 1, (x === t) <=> (x === t), x)
+ val s3 = RightExists(() |- exists(y, forall(x, (x === y) <=> (x === t))), 2, forall(x, (x === y) <=> (x === t)), y, t)
+ val s4 = Rewrite(() |- existsOne(x, x === t), 3)
+ Proof(s0, s1, s2, s3, s4)
+ }
+ val a = VariableLabel("a")
+ val b = VariableLabel("b")
+ val x = VariableLabel("x")
+ val a_ = SchematicFunctionLabel("a", 0)
+ val b_ = SchematicFunctionLabel("b", 0)
+ val x_ = SchematicFunctionLabel("x", 0)
+ val x1 = VariableLabel("x1")
+ val F = SchematicFunctionLabel("F", 1)
+ val A = SchematicFunctionLabel("A", 0)()
+ val X = VariableLabel("X")
+ val B = SchematicFunctionLabel("B", 0)()
+ val phi = SchematicPredicateLabel("phi", 1)
+ val psi = SchematicPredicateLabel("psi", 3)
+
+ val i1 = thm"mapTwoArguments" // ∀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)
+
+ val s0 = SCSubproof({
+ val s0 = SCSubproof(makeFunctional(oPair(a, b)))
+ val s1 = Weakening((in(b, B), in(a, A)) |- s0.bot.right, 0)
+ val s2 = Rewrite(in(b, B) |- in(a, A) ==> s0.bot.right.head, 1)
+ val s3 = RightForall(in(b, B) |- forall(a, in(a, A) ==> s0.bot.right.head), 2, in(a, A) ==> s0.bot.right.head, a)
+ val s4 = Rewrite(() |- in(b, B) ==> forall(a, in(a, A) ==> s0.bot.right.head), 3)
+ val s5 = RightForall(() |- forall(b, in(b, B) ==> forall(a, in(a, A) ==> s0.bot.right.head)), 4, in(b, B) ==> forall(a, in(a, A) ==> s0.bot.right.head), b)
+ Proof(steps(s0, s1, s2, s3, s4, s5))
+ }) // ∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. x= (a, b)
+
+ val s1 = InstPredSchema(
+ instantiatePredicateSchemaInSequent(i1, Map(psi -> LambdaTermFormula(Seq(x_, a_, b_), x_ === oPair(a_, b_)))),
+ -1,
+ Map(psi -> LambdaTermFormula(Seq(x_, a_, b_), x_ === oPair(a_, b_)))
+ )
+ val s2 = Cut(() |- s1.bot.right, 0, 1, s1.bot.left.head)
+ Proof(steps(s0, s1, s2), imports(i1))
+ } using (thm"mapTwoArguments")
+ show
+
+}
diff --git a/src/main/scala/proven/tactics/ProofTactics.scala b/src/main/scala/proven/tactics/ProofTactics.scala
index 5ac98af434b313e80c47228e53f150a98b4c187d..d367cf93899006d21b4565beb931ab62e74c84c2 100644
--- a/src/main/scala/proven/tactics/ProofTactics.scala
+++ b/src/main/scala/proven/tactics/ProofTactics.scala
@@ -3,7 +3,7 @@ package proven.tactics
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SequentCalculus.*
-import utilities.Helpers.{_, given}
+import utilities.Helpers.{*, given}
import utilities.Printer.*
import scala.collection.immutable.Set
@@ -71,21 +71,23 @@ object ProofTactics {
}
}
- def simpleFunctionDefinition(t: Term, args: Seq[VariableLabel]): SCProof = {
- val x = VariableLabel(freshId(t.freeVariables.map(_.id), "x"))
- val y = VariableLabel(freshId(t.freeVariables.map(_.id), "y"))
- val s0 = RightRefl(() |- t === t, t === t)
- val s1 = Rewrite(() |- (x === t) <=> (x === t), 0)
- val s2 = RightForall(() |- forall(x, (x === t) <=> (x === t)), 1, (x === t) <=> (x === t), x)
- val s3 = RightExists(() |- exists(y, forall(x, (x === y) <=> (x === t))), 2, forall(x, (x === y) <=> (x === t)), y, t)
- val s4 = Rewrite(() |- existsOne(x, x === t), 3)
- val v = Vector(s0, s1, s2, s3, s4)
+ @deprecated
+ def simpleFunctionDefinition(expression:LambdaTermTerm, out:VariableLabel): SCProof = {
+ val x = out
+ val LambdaTermTerm(vars, body) = expression
+ val xeb = x===body
+ val y = VariableLabel(freshId(body.freeVariables.map(_.id)++vars.map(_.id), "y"))
+ val s0 = RightRefl(() |- body === body, body === body)
+ val s1 = Rewrite(() |- (xeb) <=> (xeb), 0)
+ val s2 = RightForall(() |- forall(x, (xeb) <=> (xeb)), 1, (xeb) <=> (xeb), x)
+ val s3 = RightExists(() |- exists(y, forall(x, (x === y) <=> (xeb))), 2, forall(x, (x === y) <=> (xeb)), y, body)
+ val s4 = Rewrite(() |- existsOne(x, xeb), 3)
+ val v = Vector(s0, s1, s2, s3, s4)/*
val v2 = args.foldLeft((v, s4.bot.right.head, 4))((prev, x) => {
val fo = forall(x, prev._2)
(prev._1 appended RightForall(emptySeq +> fo, prev._3, prev._2, x), fo, prev._3 + 1)
- })
- SCProof(v2._1)
-
+ })*/
+ SCProof(v)
}
// p1 is a proof of psi given phi, p2 is a proof of psi given !phi
def byCase(phi: Formula)(pa: SCProofStep, pb: SCProofStep): SCProof = {
diff --git a/src/main/scala/utilities/KernelHelpers.scala b/src/main/scala/utilities/KernelHelpers.scala
index 4af7f63abadd26e5372b8b2ee49453897bd17a63..754d3f1837e57a0ede8cb5109cfabb63c48f15c0 100644
--- a/src/main/scala/utilities/KernelHelpers.scala
+++ b/src/main/scala/utilities/KernelHelpers.scala
@@ -1,9 +1,7 @@
package utilities
-import lisa.kernel.proof.RunningTheory
-import lisa.kernel.proof.RunningTheoryJudgement
+import lisa.kernel.proof.{RunningTheory, RunningTheoryJudgement, SCProof, SequentCalculus}
import lisa.kernel.proof.RunningTheoryJudgement.InvalidJustification
-import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SequentCalculus.Rewrite
import lisa.kernel.proof.SequentCalculus.isSameSequent
@@ -94,6 +92,7 @@ trait KernelHelpers {
given Conversion[(Boolean, List[Int], String), Option[(List[Int], String)]] = tr => if (tr._1) None else Some(tr._2, tr._3)
+ given Conversion[Formula, Sequent] = () |- _
/* Sequents */
val emptySeq: Sequent = Sequent(Set.empty, Set.empty)
@@ -126,7 +125,7 @@ trait KernelHelpers {
given [S]: SetConverter[S, EmptyTuple] with
override def apply(t: EmptyTuple): Set[S] = Set.empty
- given [S, H <: S, T <: Tuple, C1](using SetConverter[S, T]): SetConverter[S, H *: T] with
+ given [S, H <: S, T <: Tuple](using SetConverter[S, T]): SetConverter[S, H *: T] with
override def apply(t: H *: T): Set[S] = summon[SetConverter[S, T]].apply(t.tail) + t.head
given [S, T <: S]: SetConverter[S, T] with
diff --git a/src/main/scala/utilities/Library.scala b/src/main/scala/utilities/Library.scala
index 6f505e44bdf201127f53593be94e9f96760459f7..571807aae49c0bd4ecb992b71264d348cc5f9c44 100644
--- a/src/main/scala/utilities/Library.scala
+++ b/src/main/scala/utilities/Library.scala
@@ -1,13 +1,19 @@
package utilities
+import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.RunningTheory
import lisa.kernel.proof.RunningTheoryJudgement
import lisa.kernel.proof.SCProof
-
-import Helpers.{given, *}
+import lisa.kernel.proof.SequentCalculus.*
+import Helpers.{*, given}
+import lisa.settheory.AxiomaticSetTheory.pair
+import proven.tactics.ProofTactics.simpleFunctionDefinition
abstract class Library(val theory: RunningTheory) {
- val output: String => Unit
+ val realOutput: String => Unit
+
+ type Proof = SCProof
+ val Proof = SCProof
type Justification = theory.Justification
type Theorem = theory.Theorem
val Theorem = theory.Theorem
@@ -20,12 +26,23 @@ abstract class Library(val theory: RunningTheory) {
val FunctionDefinition = theory.FunctionDefinition
type Judgement[J <: Justification] = RunningTheoryJudgement[J]
- type Proof = SCProof
- val Proof = SCProof
- Proof.apply()
+ type Sequentable = Justification | Formula | Sequent
+
+ private var last :Option[Justification] = None
+
+ private var outString :List[String] = List()
+ private val lineBreak = "\n"
+ given output: (String => Unit) = s => outString = lineBreak :: s :: outString
+
+
+
+ inline def steps(sts:SCProofStep*):IndexedSeq[SCProofStep] = sts.toIndexedSeq
+ inline def imports(sqs:Sequentable*):IndexedSeq[Sequent] = sqs.map(sequantableToSequent).toIndexedSeq
// extension (s:String) def apply():Unit = ()
+
+ // THEOREM Syntax
def makeTheorem(name: String, statement: String, proof: SCProof, justifications: Seq[theory.Justification]): RunningTheoryJudgement[theory.Theorem] =
theory.theorem(name, statement, proof, justifications)
@@ -34,22 +51,97 @@ abstract class Library(val theory: RunningTheory) {
}
case class TheoremName(name: String) {
- def of(statement: String): TheoremNameWithStatement = TheoremNameWithStatement(name, statement)
+
+ infix def of(statement: String): TheoremNameWithStatement = TheoremNameWithStatement(name, statement)
}
def THEOREM(name: String): TheoremName = TheoremName(name)
case class TheoremNameWithProof(name: String, statement: String, proof: SCProof) {
- def using(justifications: theory.Justification*): theory.Theorem = theory.theorem(name, statement, proof, justifications) match
- case RunningTheoryJudgement.ValidJustification(just) => just
+ infix def using(justifications: theory.Justification*): theory.Theorem = theory.theorem(name, statement, proof, justifications) match
+ case RunningTheoryJudgement.ValidJustification(just) =>
+ last = Some(just)
+ just
case wrongJudgement: RunningTheoryJudgement.InvalidJustification[_] => wrongJudgement.showAndGet(output)
- def using(u: Unit): theory.Theorem = using()
+ infix def using(u: Unit): theory.Theorem = using()
+ }
+
+
+ //DEFINITION Syntax
+ def simpleDefinition(symbol:String, expression: LambdaTermTerm): RunningTheoryJudgement[theory.FunctionDefinition] =
+ val LambdaTermTerm(vars, body) = expression
+ val out:VariableLabel = VariableLabel(freshId((vars.map(_.id)++body.schematicFunctions.map(_.id)).toSet, "y"))
+ val proof:Proof = simpleFunctionDefinition(expression, out)
+ theory.functionDefinition(symbol, LambdaTermFormula(vars, out === body), out, proof, Nil)
+
+ def complexDefinition(symbol:String, vars:Seq[SchematicFunctionLabel], v:SchematicFunctionLabel, f:Formula, proof:Proof, just:Seq[Justification]): RunningTheoryJudgement[theory.FunctionDefinition] =
+ val out:VariableLabel = VariableLabel(freshId((vars.map(_.id)++f.schematicFunctions.map(_.id)).toSet, "y"))
+ theory.functionDefinition(symbol, LambdaTermFormula(vars, instantiateFunctionSchemas(f, Map(v -> LambdaTermTerm(Nil, out)))), out, proof, just)
+
+ def simpleDefinition(symbol:String, expression: LambdaTermFormula): RunningTheoryJudgement[theory.PredicateDefinition] =
+ theory.predicateDefinition(symbol, expression)
+
+ case class FunSymbolDefine(symbol:String, vars:Seq[SchematicFunctionLabel]){
+ infix def as(t:Term): ConstantFunctionLabel =
+ val definition = simpleDefinition(symbol, LambdaTermTerm(vars, t)) match
+ case RunningTheoryJudgement.ValidJustification(just) =>
+ last = Some(just)
+ just
+ case wrongJudgement: RunningTheoryJudgement.InvalidJustification[_] => wrongJudgement.showAndGet(realOutput)
+ definition.label
+ infix def as(f:Formula): ConstantPredicateLabel =
+ val definition = simpleDefinition(symbol, LambdaTermFormula(vars, f)) match
+ case RunningTheoryJudgement.ValidJustification(just) =>
+ last = Some(just)
+ just
+ case wrongJudgement: RunningTheoryJudgement.InvalidJustification[_] => wrongJudgement.showAndGet(realOutput)
+ definition.label
+
+ infix def asThe(out:SchematicFunctionLabel):DefinitionNameAndOut = DefinitionNameAndOut(symbol, vars, out)
+ }
+
+ case class DefinitionNameAndOut(symbol:String, vars:Seq[SchematicFunctionLabel], out:SchematicFunctionLabel){
+ infix def suchThat (f:Formula):DefinitionWaitingProof = DefinitionWaitingProof(symbol, vars, out, f)
+ }
+
+ case class DefinitionWaitingProof(symbol:String, vars:Seq[SchematicFunctionLabel], out:SchematicFunctionLabel, f:Formula ){
+ infix def PROOF(proof:SCProof):DefinitionWithProof = DefinitionWithProof(symbol, vars, out, f, proof)
+ }
+
+ case class DefinitionWithProof(symbol:String, vars:Seq[SchematicFunctionLabel], out:SchematicFunctionLabel, f:Formula, proof:Proof){
+ infix def using(justifications: theory.Justification*): ConstantFunctionLabel =
+ val definition = complexDefinition(symbol, vars, out, f, proof, justifications) match
+ case RunningTheoryJudgement.ValidJustification(just) =>
+ last = Some(just)
+ just
+ case wrongJudgement: RunningTheoryJudgement.InvalidJustification[_] => wrongJudgement.showAndGet(realOutput)
+ definition.label
+
+ infix def using(u: Unit): ConstantFunctionLabel = using()
+ }
+
+ //DEFINE("+", sx, sy) asThe v suchThat ... PROOF {...} using ()
+
+ def DEFINE(symbol:String, vars:SchematicFunctionLabel*): FunSymbolDefine = FunSymbolDefine(symbol, vars)
+
+ def simpleFunctionDefinition(expression:LambdaTermTerm, out:VariableLabel): SCProof = {
+ val x = out
+ val LambdaTermTerm(vars, body) = expression
+ val xeb = x===body
+ val y = VariableLabel(freshId(body.freeVariables.map(_.id)++vars.map(_.id)+out.id, "y"))
+ val s0 = RightRefl(() |- body === body, body === body)
+ val s1 = Rewrite(() |- (xeb) <=> (xeb), 0)
+ val s2 = RightForall(() |- forall(x, (xeb) <=> (xeb)), 1, (xeb) <=> (xeb), x)
+ val s3 = RightExists(() |- exists(y, forall(x, (x === y) <=> (xeb))), 2, forall(x, (x === y) <=> (xeb)), y, body)
+ val s4 = Rewrite(() |- existsOne(x, xeb), 3)
+ val v = Vector(s0, s1, s2, s3, s4)
+ SCProof(v)
}
given Conversion[TheoremNameWithProof, theory.Theorem] = _.using()
- implicit class JsonHelper(val sc: StringContext) {
+ implicit class StringToJust(val sc: StringContext) {
def thm(args: Any*): theory.Theorem = getTheorem(sc.parts.mkString(""))
@@ -73,52 +165,31 @@ abstract class Library(val theory: RunningTheory) {
case Some(value) => value
case None => throw java.util.NoSuchElementException(s"No definition for symbol \"$name\" was found.")
- given Conversion[String, theory.Justification] = name => theory.getJustification(name).get
-
- def main(args: Array[String]): Unit = { println("bonjour") }
- /*
- val a:String = "a"
- val b:String = "b"
- val c:String = "c"
- val d:String = "d"
- val e:String = "e"
- val f:String = "f"
- val g:String = "g"
- val h:String = "h"
- val i:String = "i"
- val j:String = "j"
- val k:String = "k"
- val l:String = "l"
- val m:String = "m"
- val n:String = "n"
- val o:String = "o"
- val p:String = "p"
- val q:String = "q"
- val r:String = "r"
- val s:String = "s"
- val t:String = "t"
- val u:String = "u"
- val v:String = "v"
- val w:String = "w"
- val x:String = "x"
- val y:String = "y"
- val z:String = "z"
-
- case class SchematicFLabel(s:String){
- def apply(ts:Term*): FunctionTerm = FunctionTerm(SchematicFunctionLabel(s, ts.length), ts)
- def apply(n:Int): SchematicFunctionLabel = SchematicFunctionLabel(s, n)
- }
-
- case class SchematicPLabel(s:String){
- def apply(fs:Term*): PredicateFormula = PredicateFormula(SchematicPredicateLabel(s, fs.length), fs)
- def apply(n:Int): SchematicPredicateLabel = SchematicPredicateLabel(s, n)
- }
-
- def ?(s:String) = SchematicFLabel(s)
- def &(s:String) = SchematicPLabel(s)
-
- given Conversion[String, VariableLabel] = VariableLabel(_)
- given Conversion[String, VariableTerm] = s => VariableTerm(VariableLabel(s))
-
- */
+ def show: Justification = last match
+ case Some(value) => value.show
+ case None => throw new NoSuchElementException("There is nothing to show: No theorem or definition has been proved yet.")
+ //given Conversion[String, theory.Justification] = name => theory.getJustification(name).get
+
+ private def sequantableToSequent(s:Sequentable): Sequent= s match
+ case j:Justification => theory.sequentFromJustification(j)
+ case f:Formula => () |- f
+ case s:Sequent => s
+
+ given Conversion[Sequentable, Sequent] = sequantableToSequent
+ given Conversion[theory.Axiom, Formula] = theory.sequentFromJustification(_).right.head
+ given Conversion[Formula, Axiom] = (f:Formula) => theory.getAxiom(f).get
+ given convJustSequent[C <: Iterable[Sequentable], D](using bf: scala.collection.BuildFrom[C, Sequent, D]) : Conversion[C, D] = cc => {
+ val builder = bf.newBuilder(cc)
+ cc.foreach(builder += sequantableToSequent(_))
+ builder.result
+ }
+
+ given convStrInt[C <: Iterable[String], D](using bf: scala.collection.BuildFrom[C, Int, D]) : Conversion[C, D] = cc => {
+ val builder = bf.newBuilder(cc)
+ cc.foreach(builder += _.size)
+ builder.result
+ }
+
+ def main(args: Array[String]): Unit = { realOutput(outString.reverse.mkString("")) }
+
}
diff --git a/src/main/scala/utilities/Printer.scala b/src/main/scala/utilities/Printer.scala
index d3b79263cdfcd9372dec7fa3816b017f29288898..7547ccc7d3a9d1105bf0214e8d87c3f15b5b7ac3 100644
--- a/src/main/scala/utilities/Printer.scala
+++ b/src/main/scala/utilities/Printer.scala
@@ -346,6 +346,8 @@ object Printer {
})
}
+ def prettySCProof(proof:SCProof): String = prettySCProof(SCValidProof(proof), false)
+
// def prettyTheoryJudgement((proof: SCProof, judgement: SCProofCheckerJudgement = SCValidProof, forceDisplaySubproofs: Boolean = false))
}
diff --git a/src/main/scala/utilities/TheoriesHelpers.scala b/src/main/scala/utilities/TheoriesHelpers.scala
index 0199ba734878331b2f411760864b65b99825fea9..fdab39b7e6e4558ae1d4f5cf16264b79843ed048 100644
--- a/src/main/scala/utilities/TheoriesHelpers.scala
+++ b/src/main/scala/utilities/TheoriesHelpers.scala
@@ -17,19 +17,28 @@ trait TheoriesHelpers extends KernelHelpers {
else InvalidJustification("The proof does not prove the claimed statement", None)
}
+ def functionDefinition(symbol:String, expression:LambdaTermFormula, out:VariableLabel, proof:SCProof, justifications:Seq[theory.Justification] ): RunningTheoryJudgement[theory.FunctionDefinition] = {
+ val label = ConstantFunctionLabel(symbol, expression.vars.size)
+ theory.makeFunctionDefinition(proof, justifications, label, out, expression)
+ }
+ def predicateDefinition(symbol:String, expression:LambdaTermFormula): RunningTheoryJudgement[theory.PredicateDefinition] = {
+ val label = ConstantPredicateLabel(symbol, expression.vars.size)
+ theory.makePredicateDefinition(label, expression)
+ }
+
def getJustification(name: String): Option[theory.Justification] = theory.getAxiom(name).orElse(theory.getTheorem(name)).orElse(theory.getDefinition(name))
extension (just: RunningTheory#Justification)
- def show(output: String => Unit = println): just.type = {
+ def show(implicit output: String => Unit ): just.type = {
just match
- case thm: RunningTheory#Theorem => output(s"Theorem ${thm.name} := ${Printer.prettySequent(thm.proposition)}")
- case axiom: RunningTheory#Axiom => output(s"Axiom ${axiom.name} := ${Printer.prettyFormula(axiom.ax)}")
+ case thm: RunningTheory#Theorem => output(s" Theorem ${thm.name} := ${Printer.prettySequent(thm.proposition)}\n")
+ case axiom: RunningTheory#Axiom => output(s" Axiom ${axiom.name} := ${Printer.prettyFormula(axiom.ax)}\n")
case d: RunningTheory#Definition =>
d match
case pd: RunningTheory#PredicateDefinition =>
- output(s"Definition of predicate symbol ${pd.label.id} := ${Printer.prettyFormula(pd.label(pd.args.map(VariableTerm(_))*) <=> pd.phi)}") // (label, args, phi)
+ output(s" Definition of predicate symbol ${pd.label.id} := ${Printer.prettyFormula(pd.label(pd.expression.vars.map(_())*) <=> pd.expression.body)}\n") // (label, args, phi)
case fd: RunningTheory#FunctionDefinition =>
- output(s"Definition of function symbol ${fd.label.id} := ${Printer.prettyFormula((fd.label(fd.args.map(VariableTerm(_))*) === fd.out) <=> fd.phi)})")
+ output(s" Definition of function symbol ${fd.label.id} := ${Printer.prettyFormula(( fd.out === fd.label(fd.expression.vars.map(_())*)) <=> fd.expression.body)})\n")
// output(Printer.prettySequent(thm.proposition))
// thm
just
@@ -54,4 +63,10 @@ trait TheoriesHelpers extends KernelHelpers {
val judgement = SCProofChecker.checkSCProof(proof)
output(Printer.prettySCProof(judgement))
}
+
+
+
+
+
+
}