Merge branch 'main' into require-arity

Reference Manual/lisa.tex

@@ -56,8 +56,7 @@ escapeinside={(*@}{@*)}
 \begin{document}
 \maketitle
 \chapter*{Introduction}
-This document aims to give a complete documentation on LISA. Tentatively, every chapter and section will explain a part or concept of LISA, and explains both its implementation and its theoretical foundations.
-\cite{DBLP:conf/tacas/GuilloudK22}
+This document aims to give a complete documentation on LISA. Tentatively, every chapter and section will explain a part or concept of LISA, and explains both its implementation and its theoretical foundations \cite{DBLP:conf/tacas/GuilloudK22}.
 
 \input{part1.tex}
 

Reference Manual/part2.tex

@@ -8,7 +8,7 @@
 An extension by definition is the formal way of introducing new symbols in a mathematical theory.
 Theories can be extended into new ones by adding new symbols and new axioms to it. We're interested in a special kind of extension, called \textit{conservative extension}.
 \begin{defin}[Conservative Extension]
-A theory $\mathcal{T}_2$ is a conservative extension over a theory $\mathcal{T}_1$ if:
+A theory $\mathcal{T}_2$ is a conservative extension of a theory $\mathcal{T}_1$ if:
 \begin{itemize}
 	\item $\mathcal{T}_1 \subset \mathcal{T}_2$
 	\item For any formula $\phi$ in the language of $\mathcal{T}_1$, if $\mathcal{T}_2 \vdash 		\phi$ then $\mathcal{T}_1 \vdash \phi$
@@ -29,7 +29,7 @@ Moreover, in that case we require that
 $$
 \exists ! y. \phi_{y, x_1,...,x_k}
 $$
-is a theorem of $\mathcal{T}_1$
+is a theorem of $\mathcal{T}_1$.
 \end{itemize}
 \end{itemize}
 \end{defin}
@@ -38,7 +38,7 @@ We also say that a theory $\mathcal{T}_k$ is an extension by definition of a the
 
 For function definition, it is common in logic textbooks to only require the existence of $y$ and not its uniqueness. The axiom one would then obtain would only be $\phi[f(x_1,...,x_n)/y]$ This also leads to conservative extension, but it turns out not to be enough in the presence of axiom schemas (axioms containing schematic symbols).
 \begin{lemma}
-In ZF, an extension by definition without uniqueness doesn't necessarily yields a conservative extension if the use of the new symbol is allowed in axiom schemas.
+In ZF, an extension by definition without uniqueness doesn't necessarily yield a conservative extension if the use of the new symbol is allowed in axiom schemas.
 \end{lemma}
 \begin{proof}
 In ZF, consider the formula $\phi_c := \forall x. \exists y. (x \neq \emptyset) \implies y \in x$ expressing that nonempty sets contain an element, which is provable in ZFC.
@@ -54,8 +54,8 @@ For the definition with uniqueness, there is a stronger result than only conserv
 \begin{defin}
 A theory $\mathcal{T}_2$ is a fully conservative extension over a theory $\mathcal{T}_1$ if:
 \begin{itemize}
-\item It is conservative
-\item For any formula $\phi_2$ with free variables $x_1, ..., x_k$ in the language of $\mathcal{T}_2$, there exists a formula $\phi_1$ in the language of $\mathcal{T}_1$ with free variables among $x_1, ..., x_k$ such that
+\item it is conservative, and
+\item for any formula $\phi_2$ with free variables $x_1, ..., x_k$ in the language of $\mathcal{T}_2$, there exists a formula $\phi_1$ in the language of $\mathcal{T}_1$ with free variables among $x_1, ..., x_k$ such that
 $$\mathcal{T}_2 \vdash \forall x_1...x_k. (\phi_1 \leftrightarrow \phi_2)$$
 \end{itemize}
 \end{defin}
@@ -64,7 +64,7 @@ An extension by definition with uniqueness is fully conservative.
 \end{thm}
 The proof is done by induction on the height of the formula and isn't difficult, but fairly tedious.
 \begin{thm}
-If an extension $\mathcal{T}_2$ of a theory $\mathcal{T}_1$ with axiom schemas is fully conservative, then for any instance of the axiom schemas of an axiom schemas $\alpha$ containing a new symbol, $\Gamma \vdash \alpha$ where $\Gamma$ contains no axiom schema instantiated with new symbols.
+If an extension $\mathcal{T}_2$ of a theory $\mathcal{T}_1$ with axiom schemas is fully conservative, then for any instance of the axiom schemas containing a new symbol $\alpha$, $\Gamma \vdash \alpha$ where $\Gamma$ contains no axiom schema instantiated with new symbols.
 
 \end{thm}
 \begin{proof}

lisa-theories/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala

@@ -17,6 +17,7 @@ private[settheory] trait SetTheoryZAxioms extends SetTheoryDefinitions {
   final val extensionalityAxiom: Formula = forall(x, forall(y, forall(z, in(z, x) <=> in(z, y)) <=> (x === y)))
   final val pairAxiom: Formula = forall(x, forall(y, forall(z, in(z, pair(x, y)) <=> (x === z) \/ (y === z))))
   final val unionAxiom: Formula = forall(x, forall(z, in(x, union(z)) <=> exists(y, in(x, y) /\ in(y, z))))
+  final val subsetAxiom: Formula = forall(x, forall(y, subset(x, y) <=> forall(z, (in(z, x) ==> in(z, y)))))
   final val powerAxiom: Formula = forall(x, forall(y, in(x, powerSet(y)) <=> subset(x, y)))
   final val foundationAxiom: Formula = forall(x, !(x === emptySet()) ==> exists(y, in(y, x) /\ forall(z, in(z, x) ==> !in(z, y))))
 
@@ -27,6 +28,7 @@ private[settheory] trait SetTheoryZAxioms extends SetTheoryDefinitions {
     ("extensionalityAxiom", extensionalityAxiom),
     ("pairAxiom", pairAxiom),
     ("unionAxiom", unionAxiom),
+    ("subsetAxiom", subsetAxiom),
     ("powerAxiom", powerAxiom),
     ("foundationAxiom", foundationAxiom),
     ("comprehensionSchema", comprehensionSchema)

src/main/scala/lisa/proven/peano_example/Peano.scala

+package lisa.proven.peano_example
+
+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.utils.Helpers.{_, given}
+import lisa.utils.Library
+import lisa.utils.Printer
+
+object Peano {
+  export PeanoArithmeticsLibrary.{*, given}
+
+  /////////////////////////// OUTPUT CONTROL //////////////////////////
+  given output: (String => Unit) = println
+  given finishOutput: (Throwable => Nothing) = e => throw e
+
+  def main(args: Array[String]): Unit = {}
+  /////////////////////////////////////////////////////////////////////
+
+  def instantiateForallImport(proofImport: Sequent, t: Peano.Term): SCProof = {
+    require(proofImport.right.size == 1)
+    val formula = proofImport.right.head
+    require(formula.isInstanceOf[BinderFormula] && formula.asInstanceOf[BinderFormula].label == Forall)
+    val forall = formula.asInstanceOf[BinderFormula]
+    instantiateForall(SCProof(IndexedSeq(), IndexedSeq(proofImport)))
+    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(proofImport))
+  }
+
+  def applyInduction(baseProof: SCSubproof, inductionStepProof: SCSubproof, inductionInstance: SCProofStep): IndexedSeq[SCProofStep] = {
+    require(baseProof.bot.right.size == 1, s"baseProof should prove exactly one formula, got ${Printer.prettySequent(baseProof.bot)}")
+    require(inductionStepProof.bot.right.size == 1, s"inductionStepProof should prove exactly one formula, got ${Printer.prettySequent(inductionStepProof.bot)}")
+    require(
+      inductionInstance.bot.left.isEmpty && inductionInstance.bot.right.size == 1,
+      s"induction instance step should have nothing on the left and exactly one formula on the right, got ${Printer.prettySequent(inductionInstance.bot)}"
+    )
+    val (premise, conclusion) = (inductionInstance.bot.right.head match {
+      case ConnectorFormula(Implies, Seq(premise, conclusion)) => (premise, conclusion)
+      case _ => require(false, s"induction instance should be of the form A => B, got ${Printer.prettyFormula(inductionInstance.bot.right.head)}")
+    })
+    val baseFormula = baseProof.bot.right.head
+    val stepFormula = inductionStepProof.bot.right.head
+    require(
+      isSame(baseFormula /\ stepFormula, premise),
+      "induction instance premise should be of the form base /\\ step, got " +
+        s"premise: ${Printer.prettyFormula(premise)}, base: ${Printer.prettyFormula(baseFormula)}, step: ${Printer.prettyFormula(stepFormula)}"
+    )
+
+    val lhs: Set[Formula] = baseProof.bot.left ++ inductionStepProof.bot.left
+    val base0 = baseProof
+    val step1 = inductionStepProof
+    val instance2 = inductionInstance
+    val inductionPremise3 = RightAnd(lhs |- baseFormula /\ stepFormula, Seq(0, 1), Seq(baseFormula, stepFormula))
+    val hypConclusion4 = hypothesis(conclusion)
+    val inductionInstanceOnTheLeft5 = LeftImplies(lhs + (premise ==> conclusion) |- conclusion, 3, 4, premise, conclusion)
+    val cutInductionInstance6 = Cut(lhs |- conclusion, 2, 5, premise ==> conclusion)
+    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)))
+    val implies2 = RightImplies(() |- (x === plus(zero, x)) ==> (s(x) === s(plus(zero, x))), 1, x === plus(zero, x), s(x) === s(plus(zero, x)))
+    val transform3 = RightSubstEq(
+      (plus(zero, s(x)) === s(plus(zero, x))) |- (x === plus(zero, x)) ==> (s(x) === plus(zero, s(x))),
+      2,
+      (plus(zero, s(x)), s(plus(zero, x))) :: Nil,
+      LambdaTermFormula(Seq(y), (x === plus(zero, x)) ==> (s(x) === y))
+    )
+
+    // result: ax4plusSuccessor |- 0+Sx = S(0 + x)
+    val instanceAx4_4 = SCSubproof(
+      instantiateForall(instantiateForallImport(ax"ax4plusSuccessor", zero), x),
+      Seq(-1)
+    )
+    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(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(
+      (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(
+      instantiateForallImport(ax"ax3neutral", x),
+      Seq(-2)
+    )
+    val instancePlusZero9 = SCSubproof(
+      instantiateForallImport(ax"ax3neutral", s(x)),
+      Seq(-2)
+    )
+    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(
+      () |- (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))
+    )
+
+    val forall12 = RightForall(
+      cut11.bot.left |- forall(x, (plus(x, zero) === plus(zero, x)) ==> (plus(s(x), zero) === plus(zero, s(x)))),
+      11,
+      (plus(x, zero) === plus(zero, x)) ==> (plus(s(x), zero) === plus(zero, s(x))),
+      x
+    )
+
+    val inductionInstance: SCProofStep = InstPredSchema(
+      () |- ((plus(zero, zero) === plus(zero, zero)) /\ forall(x, (plus(x, zero) === plus(zero, x)) ==> (plus(s(x), zero) === plus(zero, s(x))))) ==> forall(
+        x,
+        plus(x, zero) === plus(zero, x)
+      ),
+      -3,
+      Map(sPhi -> LambdaTermFormula(Seq(x), plus(x, zero) === plus(zero, x)))
+    )
+
+    SCProof(
+      applyInduction(
+        SCSubproof(SCProof(RightRefl(() |- zero === zero, zero === zero))),
+        SCSubproof(
+          SCProof(
+            IndexedSeq(refl0, subst1, implies2, transform3, instanceAx4_4, cut5, transform6, leftAnd7, instancePlusZero8, instancePlusZero9, rightAnd10, cut11, forall12),
+            IndexedSeq(ax"ax4plusSuccessor", ax"ax3neutral")
+          ),
+          Seq(-1, -2)
+        ),
+        inductionInstance
+      ),
+      IndexedSeq(ax"ax4plusSuccessor", ax"ax3neutral", ax"ax7induction")
+    )
+  } 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(instantiateForallImport(ax"ax3neutral", x), IndexedSeq(-1))
+      // Sx + 0 = Sx
+      val succXEqSuccXPlusZero1 = SCSubproof(instantiateForallImport(ax"ax3neutral", s(x)), IndexedSeq(-1))
+      // x + S0 = S(x + 0)
+      val xPlusSuccZero2 = SCSubproof(instantiateForall(instantiateForallImport(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)
+      )
+    }
+
+    /////////////// Induction step: ∀y. (x + Sy === Sx + y) ==> (x + SSy === Sx + Sy) ////////////////////
+    val inductionStep1 = {
+      // x + SSy = S(x + Sy)
+      val moveSuccessor0 = SCSubproof(instantiateForall(instantiateForallImport(ax"ax4plusSuccessor", x), s(y)), IndexedSeq(-2))
+
+      // Sx + Sy = S(Sx + y)
+      val moveSuccessor1 = SCSubproof(instantiateForall(instantiateForallImport(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 inductionInstance = {
+      val inductionOnY0 = Rewrite(() |- (sPhi(zero) /\ forall(y, sPhi(y) ==> sPhi(s(y)))) ==> forall(y, sPhi(y)), -1)
+      val inductionInstance1 = 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)),
+        0,
+        Map(sPhi -> LambdaTermFormula(Seq(y), plus(x, s(y)) === plus(s(x), y)))
+      )
+      SCSubproof(SCProof(IndexedSeq(inductionOnY0, inductionInstance1), IndexedSeq(ax"ax7induction")), Seq(-3))
+    }
+    val inductionApplication = applyInduction(base0, inductionStep1, inductionInstance)
+    val addForall = RightForall(() |- forall(x, forall(y, plus(x, s(y)) === plus(s(x), y))), inductionApplication.size - 1, forall(y, plus(x, s(y)) === plus(s(x), y)), x)
+    val proof: SCProof = Proof(
+      inductionApplication :+ addForall,
+      IndexedSeq(ax"ax3neutral", ax"ax4plusSuccessor", ax"ax7induction")
+    )
+    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
+}

src/main/scala/lisa/proven/peano_example/PeanoArithmetics.scala

+package lisa.proven.peano_example
+
+import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.RunningTheory
+import lisa.utils.Helpers.{_, given}
+
+object PeanoArithmetics {
+  final val (x, y, z) =
+    (VariableLabel("x"), VariableLabel("y"), VariableLabel("z"))
+
+  final val zero: Term = ConstantFunctionLabel("0", 0)()
+  final val s = ConstantFunctionLabel("S", 1)
+  final val plus = ConstantFunctionLabel("+", 2)
+  final val times = ConstantFunctionLabel("*", 2)
+  final val sPhi: SchematicPredicateLabel = SchematicNPredicateLabel("?p", 1)
+
+  final val ax1ZeroSuccessor: Formula = forall(x, !(s(x) === zero))
+  final val ax2Injectivity: Formula = forall(x, forall(y, (s(x) === s(y)) ==> (x === y)))
+  final val ax3neutral: Formula = forall(x, plus(x, zero) === x)
+  final val ax4plusSuccessor: Formula = forall(x, forall(y, plus(x, s(y)) === s(plus(x, y))))
+  final val ax5timesZero: Formula = forall(x, times(x, zero) === zero)
+  final val ax6timesDistrib: Formula = forall(x, forall(y, times(x, s(y)) === plus(times(x, y), x)))
+  final val ax7induction: Formula = (sPhi(zero) /\ forall(x, sPhi(x) ==> sPhi(s(x)))) ==> forall(x, sPhi(x))
+
+  final val runningPeanoTheory: RunningTheory = new RunningTheory()
+  final val functions: Set[ConstantFunctionLabel] = Set(ConstantFunctionLabel("0", 0), s, plus, times)
+  functions.foreach(runningPeanoTheory.addSymbol(_))
+
+  private val peanoAxioms: Set[(String, Formula)] = Set(
+    ("ax1ZeroSuccessor", ax1ZeroSuccessor),
+    ("ax2Injectivity", ax2Injectivity),
+    ("ax3neutral", ax3neutral),
+    ("ax4plusSuccessor", ax4plusSuccessor),
+    ("ax5timesZero", ax5timesZero),
+    ("ax6timesDistrib", ax6timesDistrib),
+    ("ax7induction", ax7induction)
+  )
+  peanoAxioms.foreach(a => runningPeanoTheory.addAxiom(a._1, a._2))
+}

src/main/scala/lisa/proven/peano_example/PeanoArithmeticsLibrary.scala

+package lisa.proven.peano_example
+
+object PeanoArithmeticsLibrary extends lisa.utils.Library(lisa.proven.peano_example.PeanoArithmetics.runningPeanoTheory) {
+  export lisa.proven.peano_example.PeanoArithmetics.*
+}