From ebe05d5a117f3359a0e9387a3cd356c3a314c520 Mon Sep 17 00:00:00 2001
From: Katja Goltsova <katja.goltsova@protonmail.com>
Date: Mon, 22 Aug 2022 16:37:26 +0200
Subject: [PATCH] Prove in Peano arithmetic that x+y=y+x
---
.../scala/lisa/proven/mathematics/Peano.scala | 87 ++++++++++++++++++-
1 file changed, 84 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/lisa/proven/mathematics/Peano.scala b/src/main/scala/lisa/proven/mathematics/Peano.scala
index 0f358602..491e7a9e 100644
--- a/src/main/scala/lisa/proven/mathematics/Peano.scala
+++ b/src/main/scala/lisa/proven/mathematics/Peano.scala
@@ -64,6 +64,9 @@ object Peano {
IndexedSeq(base0, step1, instance2, inductionPremise3, hypConclusion4, inductionInstanceOnTheLeft5, cutInductionInstance6)
}
+ val (y1, z1) =
+ (VariableLabel("y1"), VariableLabel("z1"))
+
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)))
@@ -182,9 +185,6 @@ object Peano {
)
}
- 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)
@@ -256,4 +256,85 @@ object Peano {
proof
} using (ax"ax3neutral", ax"ax4plusSuccessor", ax"ax7induction")
show
+
+ THEOREM("additivity of addition") of "" PROOF {
+ val base0 = SCSubproof(instantiateForallImport(thm"x + 0 = 0 + x", x), Seq(-3))
+ val inductionStep1 = {
+ val start0 = RightRefl(() |- plus(x, s(y)) === plus(x, s(y)), plus(x, s(y)) === plus(x, s(y)))
+ val applyPlusSuccAx1 =
+ RightSubstEq(plus(x, s(y)) === s(plus(x, y)) |- plus(x, s(y)) === s(plus(x, y)), 0, (plus(x, s(y)), s(plus(x, y))) :: Nil, LambdaTermFormula(Seq(z1), plus(x, s(y)) === z1))
+ val applyInductionPremise2 =
+ RightSubstEq(
+ Set(plus(x, s(y)) === s(plus(x, y)), plus(x, y) === plus(y, x)) |- plus(x, s(y)) === s(plus(y, x)),
+ 1,
+ (plus(x, y), plus(y, x)) :: Nil,
+ LambdaTermFormula(Seq(z1), plus(x, s(y)) === s(z1))
+ )
+ val applyPlusSuccAx3 =
+ RightSubstEq(
+ Set(plus(x, s(y)) === s(plus(x, y)), plus(x, y) === plus(y, x), s(plus(y, x)) === plus(y, s(x))) |- plus(x, s(y)) === plus(y, s(x)),
+ 2,
+ (s(plus(y, x)), plus(y, s(x))) :: Nil,
+ LambdaTermFormula(Seq(z1), plus(x, s(y)) === z1)
+ )
+ val applySwitchSuccessor4 =
+ RightSubstEq(
+ Set(plus(x, s(y)) === s(plus(x, y)), plus(x, y) === plus(y, x), s(plus(y, x)) === plus(y, s(x)), plus(y, s(x)) === plus(s(y), x)) |- plus(x, s(y)) === plus(s(y), x),
+ 3,
+ (plus(y, s(x)), plus(s(y), x)) :: Nil,
+ LambdaTermFormula(Seq(z1), plus(x, s(y)) === z1)
+ )
+
+ val xPlusSYInstance5 = SCSubproof(instantiateForall(instantiateForallImport(ax"ax4plusSuccessor", x), y), Seq(-1))
+ val cutXPlusSY6 = Cut(Set(plus(x, y) === plus(y, x), s(plus(y, x)) === plus(y, s(x)), plus(y, s(x)) === plus(s(y), x)) |- plus(x, s(y)) === plus(s(y), x), 5, 4, plus(x, s(y)) === s(plus(x, y)))
+ val yPlusSXInstance7 = SCSubproof(instantiateForall(instantiateForallImport(ax"ax4plusSuccessor", y), x), Seq(-1))
+ val cutYPlusSX8 = Cut(Set(plus(x, y) === plus(y, x), plus(y, s(x)) === plus(s(y), x)) |- plus(x, s(y)) === plus(s(y), x), 7, 6, s(plus(y, x)) === plus(y, s(x)))
+ val swichSuccessorInstance9 = SCSubproof(instantiateForall(instantiateForallImport(thm"switch successor", y), x), Seq(-2))
+ val cutSwitchSuccessor10 = Cut(plus(x, y) === plus(y, x) |- plus(x, s(y)) === plus(s(y), x), 9, 8, plus(y, s(x)) === plus(s(y), x))
+ val rightImplies11 = RightImplies(() |- (plus(x, y) === plus(y, x)) ==> (plus(x, s(y)) === plus(s(y), x)), 10, plus(x, y) === plus(y, x), plus(x, s(y)) === plus(s(y), x))
+ val forall12 = RightForall(() |- forall(y, (plus(x, y) === plus(y, x)) ==> (plus(x, s(y)) === plus(s(y), x))), 11, (plus(x, y) === plus(y, x)) ==> (plus(x, s(y)) === plus(s(y), x)), y)
+ SCSubproof(
+ Proof(
+ IndexedSeq(
+ start0,
+ applyPlusSuccAx1,
+ applyInductionPremise2,
+ applyPlusSuccAx3,
+ applySwitchSuccessor4,
+ xPlusSYInstance5,
+ cutXPlusSY6,
+ yPlusSXInstance7,
+ cutYPlusSX8,
+ swichSuccessorInstance9,
+ cutSwitchSuccessor10,
+ rightImplies11,
+ forall12
+ ),
+ IndexedSeq(ax"ax4plusSuccessor", thm"switch successor")
+ ),
+ IndexedSeq(-1, -4)
+ )
+ }
+
+ val inductionInstance = {
+ val inductionOnY0 = Rewrite(() |- (sPhi(zero) /\ forall(y, sPhi(y) ==> sPhi(s(y)))) ==> forall(y, sPhi(y)), -1)
+ val inductionInstance1 = InstPredSchema(
+ () |-
+ ((plus(x, zero) === plus(zero, x)) /\
+ forall(y, (plus(x, y) === plus(y, x)) ==> (plus(x, s(y)) === plus(s(y), x)))) ==>
+ forall(y, plus(x, y) === plus(y, x)),
+ 0,
+ Map(sPhi -> LambdaTermFormula(Seq(y), plus(x, y) === plus(y, x)))
+ )
+ SCSubproof(SCProof(IndexedSeq(inductionOnY0, inductionInstance1), IndexedSeq(ax"ax7induction")), Seq(-2))
+ }
+ val inductionApplication = applyInduction(base0, inductionStep1, inductionInstance)
+ val addForall = RightForall(() |- forall(x, forall(y, plus(x, y) === plus(y, x))), inductionApplication.size - 1, forall(y, plus(x, y) === plus(y, x)), x)
+ val proof: SCProof = Proof(
+ inductionApplication :+ addForall,
+ IndexedSeq(ax"ax4plusSuccessor", ax"ax7induction", thm"x + 0 = 0 + x", thm"switch successor")
+ )
+ proof
+ } using (ax"ax4plusSuccessor", ax"ax7induction", thm"x + 0 = 0 + x", thm"switch successor")
+ show
}
--
GitLab