From 6e355f4d64a3c14d9a4fe527aa7bce9a012d906c Mon Sep 17 00:00:00 2001
From: Katja Goltsova <katja.goltsova@protonmail.com>
Date: Wed, 17 Aug 2022 18:09:08 +0200
Subject: [PATCH] Prove in Peano that x+Sy = Sx+y
---
.../scala/lisa/proven/mathematics/Peano.scala | 146 +++++++++++++++++-
1 file changed, 145 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/lisa/proven/mathematics/Peano.scala b/src/main/scala/lisa/proven/mathematics/Peano.scala
index 12275ae0..06fcae02 100644
--- a/src/main/scala/lisa/proven/mathematics/Peano.scala
+++ b/src/main/scala/lisa/proven/mathematics/Peano.scala
@@ -4,8 +4,8 @@ import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.RunningTheory
import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SequentCalculus.*
-import lisa.proven.tactics.ProofTactics.*
import lisa.proven.PeanoArithmeticsLibrary
+import lisa.proven.tactics.ProofTactics.*
import lisa.utils.Helpers.{_, given}
import lisa.utils.Library
@@ -19,6 +19,19 @@ object Peano {
def main(args: Array[String]): Unit = {}
/////////////////////////////////////////////////////////////////////
+ def instantiateForallAxiom(ax: Axiom, t: Term): SCProof = {
+ val formula = ax.ax
+ require(formula.isInstanceOf[BinderFormula] && formula.asInstanceOf[BinderFormula].label == Forall)
+ val forall = ax.ax.asInstanceOf[BinderFormula]
+ instantiateForall(SCProof(IndexedSeq(), IndexedSeq(ax)))
+ val tempVar = VariableLabel(freshId(formula.freeVariables.map(_.id), "x"))
+ val instantiated = instantiateBinder(forall, t)
+ val p1 = Hypothesis(instantiated |- instantiated, instantiated)
+ val p2 = LeftForall(formula |- instantiated, 0, instantiateBinder(forall, tempVar), tempVar, t)
+ val p3 = Cut(() |- instantiated, -1, 1, formula)
+ Proof(IndexedSeq(p1, p2, p3), IndexedSeq(ax))
+ }
+
THEOREM("x + 0 = 0 + x") of "∀x. plus(x, zero) === plus(zero, x)" PROOF {
val refl0: SCProofStep = RightRefl(() |- s(x) === s(x), s(x) === s(x))
val subst1 = RightSubstEq((x === plus(zero, x)) |- s(x) === s(plus(zero, x)), 0, (x, plus(zero, x)) :: Nil, LambdaTermFormula(Seq(y), s(x) === s(y)))
@@ -127,4 +140,135 @@ object Peano {
)
} using (ax"ax4plusSuccessor", ax"ax3neutral", ax"ax7induction")
show
+
+ THEOREM("switch successor") of "∀y. ∀x. plus(x, s(y)) === plus(s(x), y)" PROOF {
+ //////////////////////////////////// Base: x + S0 = Sx + 0 ///////////////////////////////////////////////
+ val base0 = {
+ // x + 0 = x
+ val xEqXPlusZero0 = SCSubproof(instantiateForallAxiom(ax"ax3neutral", x), IndexedSeq(-1))
+ // Sx + 0 = Sx
+ val succXEqSuccXPlusZero1 = SCSubproof(instantiateForallAxiom(ax"ax3neutral", s(x)), IndexedSeq(-1))
+ // x + S0 = S(x + 0)
+ val xPlusSuccZero2 = SCSubproof(instantiateForall(instantiateForallAxiom(ax"ax4plusSuccessor", x), zero), IndexedSeq(-2))
+
+ // ------------------- x + 0 = x, Sx + 0 = Sx, x + S0 = S(x + 0) |- Sx + 0 = x + S0 ---------------------
+ val succX3 = RightRefl(() |- s(x) === s(x), s(x) === s(x))
+ val substEq4 = RightSubstEq(
+ Set(s(x) === plus(s(x), zero), x === plus(x, zero)) |- plus(s(x), zero) === s(plus(x, zero)),
+ 3,
+ (s(x), plus(s(x), zero)) :: (VariableTerm(x), plus(x, zero)) :: Nil,
+ LambdaTermFormula(Seq(y, z), y === s(z))
+ )
+ val substEq5 = RightSubstEq(
+ Set(s(x) === plus(s(x), zero), x === plus(x, zero), s(plus(x, zero)) === plus(x, s(zero))) |- plus(s(x), zero) === plus(x, s(zero)),
+ 4,
+ (s(plus(x, zero)), plus(x, s(zero))) :: Nil,
+ LambdaTermFormula(Seq(z), plus(s(x), zero) === z)
+ )
+ // -------------------------------------------------------------------------------------------------------
+ val cut6 = Cut(Set(s(x) === plus(s(x), zero), x === plus(x, zero)) |- plus(s(x), zero) === plus(x, s(zero)), 2, 5, s(plus(x, zero)) === plus(x, s(zero)))
+ val cut7 = Cut(x === plus(x, zero) |- plus(s(x), zero) === plus(x, s(zero)), 1, 6, s(x) === plus(s(x), zero))
+ val cut8 = Cut(() |- plus(s(x), zero) === plus(x, s(zero)), 0, 7, x === plus(x, zero))
+ SCSubproof(
+ SCProof(
+ IndexedSeq(xEqXPlusZero0, succXEqSuccXPlusZero1, xPlusSuccZero2, succX3, substEq4, substEq5, cut6, cut7, cut8),
+ IndexedSeq(ax"ax3neutral", ax"ax4plusSuccessor")
+ ),
+ IndexedSeq(-1, -2)
+ )
+ }
+
+ val (x1, y1, z1) =
+ (VariableLabel("x1"), VariableLabel("y1"), VariableLabel("z1"))
+
+ /////////////// Induction step: ∀y. (x + Sy === Sx + y) ==> (x + SSy === Sx + Sy) ////////////////////
+ val inductionStep1 = {
+ // x + SSy = S(x + Sy)
+ val moveSuccessor0 = SCSubproof(instantiateForall(instantiateForallAxiom(ax"ax4plusSuccessor", x), s(y)), IndexedSeq(-2))
+
+ // Sx + Sy = S(Sx + y)
+ val moveSuccessor1 = SCSubproof(instantiateForall(instantiateForallAxiom(ax"ax4plusSuccessor", s(x)), y), IndexedSeq(-2))
+
+ // ----------- x + SSy = S(x + Sy), x + Sy = Sx + y, S(Sx + y) = Sx + Sy |- x + SSy = Sx + Sy ------------
+ val middleEq2 = RightRefl(() |- s(plus(x, s(y))) === s(plus(x, s(y))), s(plus(x, s(y))) === s(plus(x, s(y))))
+ val substEq3 =
+ RightSubstEq(
+ Set(plus(x, s(y)) === plus(s(x), y)) |- s(plus(x, s(y))) === s(plus(s(x), y)),
+ 2,
+ (plus(x, s(y)), plus(s(x), y)) :: Nil,
+ LambdaTermFormula(Seq(z1), s(plus(x, s(y))) === s(z1))
+ )
+ val substEq4 =
+ RightSubstEq(
+ Set(plus(x, s(y)) === plus(s(x), y), plus(x, s(s(y))) === s(plus(x, s(y)))) |- plus(x, s(s(y))) === s(plus(s(x), y)),
+ 3,
+ (plus(x, s(s(y))), s(plus(x, s(y)))) :: Nil,
+ LambdaTermFormula(Seq(z1), z1 === s(plus(s(x), y)))
+ )
+ val substEq5 =
+ RightSubstEq(
+ Set(plus(x, s(s(y))) === s(plus(x, s(y))), plus(x, s(y)) === plus(s(x), y), s(plus(s(x), y)) === plus(s(x), s(y))) |- plus(x, s(s(y))) === plus(s(x), s(y)),
+ 4,
+ (s(plus(s(x), y)), plus(s(x), s(y))) :: Nil,
+ LambdaTermFormula(Seq(z1), plus(x, s(s(y))) === z1)
+ )
+ // -------------------------------------------------------------------------------------------------------
+ val cut6 = Cut(Set(plus(x, s(y)) === plus(s(x), y), s(plus(s(x), y)) === plus(s(x), s(y))) |- plus(x, s(s(y))) === plus(s(x), s(y)), 0, 5, plus(x, s(s(y))) === s(plus(x, s(y))))
+ val cut7 = Cut(plus(x, s(y)) === plus(s(x), y) |- plus(x, s(s(y))) === plus(s(x), s(y)), 1, 6, s(plus(s(x), y)) === plus(s(x), s(y)))
+ val implies8 = RightImplies(() |- (plus(x, s(y)) === plus(s(x), y)) ==> (plus(x, s(s(y))) === plus(s(x), s(y))), 7, plus(x, s(y)) === plus(s(x), y), plus(x, s(s(y))) === plus(s(x), s(y)))
+ val forall9 = RightForall(
+ () |- forall(y, (plus(x, s(y)) === plus(s(x), y)) ==> (plus(x, s(s(y))) === plus(s(x), s(y)))),
+ 8,
+ (plus(x, s(y)) === plus(s(x), y)) ==> (plus(x, s(s(y))) === plus(s(x), s(y))),
+ y
+ )
+ SCSubproof(
+ SCProof(
+ IndexedSeq(moveSuccessor0, moveSuccessor1, middleEq2, substEq3, substEq4, substEq5, cut6, cut7, implies8, forall9),
+ IndexedSeq(ax"ax3neutral", ax"ax4plusSuccessor")
+ ),
+ IndexedSeq(-1, -2)
+ )
+ }
+
+ val inductionOnY2 = Rewrite(() |- (sPhi(zero) /\ forall(y, sPhi(y) ==> sPhi(s(y)))) ==> forall(y, sPhi(y)), -3)
+ val inductionInstance3 = InstPredSchema(
+ () |-
+ ((plus(s(x), zero) === plus(x, s(zero))) /\
+ forall(y, (plus(x, s(y)) === plus(s(x), y)) ==> (plus(x, s(s(y))) === plus(s(x), s(y))))) ==>
+ forall(y, plus(x, s(y)) === plus(s(x), y)),
+ 2,
+ Map(sPhi -> LambdaTermFormula(Seq(y), plus(x, s(y)) === plus(s(x), y)))
+ )
+ val inductionPremise4 = RightAnd(
+ () |- (plus(x, s(zero)) === plus(s(x), zero)) /\
+ forall(y, (plus(x, s(y)) === plus(s(x), y)) ==> (plus(x, s(s(y))) === plus(s(x), s(y)))),
+ Seq(0, 1),
+ Seq(plus(x, s(zero)) === plus(s(x), zero), forall(y, (plus(x, s(y)) === plus(s(x), y)) ==> (plus(x, s(s(y))) === plus(s(x), s(y)))))
+ )
+ val conclusion5 = hypothesis(forall(y, plus(x, s(y)) === plus(s(x), y)))
+ val inductionInstanceOnTheLeft6 = LeftImplies(
+ ((plus(s(x), zero) === plus(x, s(zero))) /\
+ forall(y, (plus(x, s(y)) === plus(s(x), y)) ==> (plus(x, s(s(y))) === plus(s(x), s(y))))) ==>
+ forall(y, plus(x, s(y)) === plus(s(x), y))
+ |- forall(y, plus(x, s(y)) === plus(s(x), y)),
+ 4,
+ 5,
+ (plus(x, s(zero)) === plus(s(x), zero)) /\ forall(y, (plus(x, s(y)) === plus(s(x), y)) ==> (plus(x, s(s(y))) === plus(s(x), s(y)))),
+ forall(y, plus(x, s(y)) === plus(s(x), y))
+ )
+ val inductionResult7 = Cut(
+ () |- forall(y, plus(x, s(y)) === plus(s(x), y)),
+ 3,
+ 6,
+ ((plus(x, s(zero)) === plus(s(x), zero)) /\ forall(y, (plus(x, s(y)) === plus(s(x), y)) ==> (plus(x, s(s(y))) === plus(s(x), s(y))))) ==> forall(y, plus(x, s(y)) === plus(s(x), y))
+ )
+ val addForall8 = RightForall(() |- forall(x, forall(y, plus(x, s(y)) === plus(s(x), y))), 7, forall(y, plus(x, s(y)) === plus(s(x), y)), x)
+ val proof: SCProof = Proof(
+ IndexedSeq(base0, inductionStep1, inductionOnY2, inductionInstance3, inductionPremise4, conclusion5, inductionInstanceOnTheLeft6, inductionResult7, addForall8),
+ IndexedSeq(ax"ax3neutral", ax"ax4plusSuccessor", ax"ax7induction")
+ )
+ proof
+ } using (ax"ax3neutral", ax"ax4plusSuccessor", ax"ax7induction")
+ show
}
--
GitLab