From 152289c45144919da213d880d178b19334ecfdc4 Mon Sep 17 00:00:00 2001
From: Katja Goltsova <katja.goltsova@protonmail.com>
Date: Mon, 22 Aug 2022 13:28:06 +0200
Subject: [PATCH] Use instantiateForallAxiom in the proof of x+0=0+x to clean
up the left hand side of the proof
---
.../scala/lisa/proven/mathematics/Peano.scala | 20 +++++++++----------
1 file changed, 10 insertions(+), 10 deletions(-)
diff --git a/src/main/scala/lisa/proven/mathematics/Peano.scala b/src/main/scala/lisa/proven/mathematics/Peano.scala
index 06fcae02..b3f11f58 100644
--- a/src/main/scala/lisa/proven/mathematics/Peano.scala
+++ b/src/main/scala/lisa/proven/mathematics/Peano.scala
@@ -45,36 +45,36 @@ object Peano {
// result: ax4plusSuccessor |- 0+Sx = S(0 + x)
val instanceAx4_4 = SCSubproof(
- instantiateForall(SCProof(IndexedSeq[SCProofStep](Hypothesis(ax4plusSuccessor |- ax4plusSuccessor, ax4plusSuccessor)), IndexedSeq(() |- ax4plusSuccessor)), zero, x),
+ instantiateForall(instantiateForallAxiom(ax"ax4plusSuccessor", zero), x),
Seq(-1)
)
- val cut5 = Cut(ax4plusSuccessor |- (x === plus(zero, x)) ==> (s(x) === plus(zero, s(x))), 4, 3, plus(zero, s(x)) === s(plus(zero, x)))
+ val cut5 = Cut(() |- (x === plus(zero, x)) ==> (s(x) === plus(zero, s(x))), 4, 3, plus(zero, s(x)) === s(plus(zero, x)))
val transform6 = RightSubstEq(
- Set(ax4plusSuccessor, plus(x, zero) === x, plus(s(x), zero) === s(x)) |- (plus(x, zero) === plus(zero, x)) ==> (plus(s(x), zero) === plus(zero, s(x))),
+ Set(plus(x, zero) === x, plus(s(x), zero) === s(x)) |- (plus(x, zero) === plus(zero, x)) ==> (plus(s(x), zero) === plus(zero, s(x))),
5,
(plus(x, zero), x) :: (plus(s(x), zero), s(x)) :: Nil,
LambdaTermFormula(Seq(y, z), (y === plus(zero, x)) ==> (z === plus(zero, s(x))))
)
val leftAnd7 = LeftAnd(
- Set(ax4plusSuccessor, (plus(x, zero) === x) /\ (plus(s(x), zero) === s(x))) |- (plus(x, zero) === plus(zero, x)) ==> (plus(s(x), zero) === plus(zero, s(x))),
+ (plus(x, zero) === x) /\ (plus(s(x), zero) === s(x)) |- (plus(x, zero) === plus(zero, x)) ==> (plus(s(x), zero) === plus(zero, s(x))),
6,
plus(x, zero) === x,
plus(s(x), zero) === s(x)
)
val instancePlusZero8 = SCSubproof(
- instantiateForall(SCProof(IndexedSeq[SCProofStep](Hypothesis(ax3neutral |- ax3neutral, ax3neutral)), IndexedSeq(() |- ax3neutral)), x),
+ instantiateForallAxiom(ax"ax3neutral", x),
Seq(-2)
)
val instancePlusZero9 = SCSubproof(
- instantiateForall(SCProof(IndexedSeq[SCProofStep](Hypothesis(ax3neutral |- ax3neutral, ax3neutral)), IndexedSeq(() |- ax3neutral)), s(x)),
+ instantiateForallAxiom(ax"ax3neutral", s(x)),
Seq(-2)
)
- val rightAnd10 = RightAnd(ax3neutral |- (plus(x, zero) === x) /\ (plus(s(x), zero) === s(x)), Seq(8, 9), Seq(plus(x, zero) === x, plus(s(x), zero) === s(x)))
+ val rightAnd10 = RightAnd(() |- (plus(x, zero) === x) /\ (plus(s(x), zero) === s(x)), Seq(8, 9), Seq(plus(x, zero) === x, plus(s(x), zero) === s(x)))
val cut11 = Cut(
- Set(ax4plusSuccessor, ax3neutral) |- (plus(x, zero) === plus(zero, x)) ==> (plus(s(x), zero) === plus(zero, s(x))),
+ () |- (plus(x, zero) === plus(zero, x)) ==> (plus(s(x), zero) === plus(zero, s(x))),
10,
7,
(plus(x, zero) === x) /\ (plus(s(x), zero) === s(x))
@@ -89,7 +89,7 @@ object Peano {
val hypConclusion13 = hypothesis(forall(x, plus(x, zero) === plus(zero, x)))
val inductionLhs14 = LeftImplies(
- Set(ax4plusSuccessor, ax3neutral, forall(x, (plus(x, zero) === plus(zero, x)) ==> (plus(s(x), zero) === plus(zero, s(x)))) ==> forall(x, plus(x, zero) === plus(zero, x))) |- forall(
+ forall(x, (plus(x, zero) === plus(zero, x)) ==> (plus(s(x), zero) === plus(zero, s(x)))) ==> forall(x, plus(x, zero) === plus(zero, x)) |- forall(
x,
plus(x, zero) === plus(zero, x)
),
@@ -107,7 +107,7 @@ object Peano {
Map(sPhi -> LambdaTermFormula(Seq(x), plus(x, zero) === plus(zero, x)))
)
val commutesWithZero16 = Cut(
- Set(ax4plusSuccessor, ax3neutral) |- forall(x, plus(x, zero) === plus(zero, x)),
+ () |- forall(x, plus(x, zero) === plus(zero, x)),
15,
14,
((plus(zero, zero) === plus(zero, zero)) /\ forall(x, (plus(x, zero) === plus(zero, x)) ==> (plus(s(x), zero) === plus(zero, s(x))))) ==> forall(
--
GitLab