From 453f367400325495e2b75972736988927f126c04 Mon Sep 17 00:00:00 2001
From: Katja Goltsova <katja.goltsova@protonmail.com>
Date: Fri, 5 Aug 2022 14:24:30 +0200
Subject: [PATCH] Introduce PeanoArithmetics, PeanoArithmeticsLibrary, Peano
PeanoArithmetics contains the definitions and axioms of Peano arithmetics,
PeanoArithmeticsLibrary gives access to lisa.utils.Library with runningPeanoTheory,
Peano contains proofs of the theory. This separation follows the same structure
as set theory.
---
.../lisa/proven/PeanoArithmeticsLibrary.scala | 5 +++
.../scala/lisa/proven/mathematics/Peano.scala | 40 ++++---------------
.../proven/mathematics/PeanoArithmetics.scala | 39 ++++++++++++++++++
3 files changed, 52 insertions(+), 32 deletions(-)
create mode 100644 src/main/scala/lisa/proven/PeanoArithmeticsLibrary.scala
create mode 100644 src/main/scala/lisa/proven/mathematics/PeanoArithmetics.scala
diff --git a/src/main/scala/lisa/proven/PeanoArithmeticsLibrary.scala b/src/main/scala/lisa/proven/PeanoArithmeticsLibrary.scala
new file mode 100644
index 00000000..236926c7
--- /dev/null
+++ b/src/main/scala/lisa/proven/PeanoArithmeticsLibrary.scala
@@ -0,0 +1,5 @@
+package lisa.proven
+
+object PeanoArithmeticsLibrary extends lisa.utils.Library(lisa.proven.mathematics.PeanoArithmetics.runningPeanoTheory) {
+ export lisa.proven.mathematics.PeanoArithmetics.*
+}
diff --git a/src/main/scala/lisa/proven/mathematics/Peano.scala b/src/main/scala/lisa/proven/mathematics/Peano.scala
index 2b6139dd..48081a19 100644
--- a/src/main/scala/lisa/proven/mathematics/Peano.scala
+++ b/src/main/scala/lisa/proven/mathematics/Peano.scala
@@ -3,38 +3,14 @@ package lisa.proven.mathematics
import lisa.utils.Helpers.{given, *}
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.utils.Helpers.{_, given}
+import lisa.utils.Library
object Peano {
- type Axiom = Formula
- final val (x, y) =
- (VariableLabel("x"), VariableLabel("y"))
-
- 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 = SchematicPredicateLabel("?p", 1)
-
- final val ax1ZeroSuccessor: Axiom = forall(x, !(s(x) === zero))
- final val ax2Injectivity: Axiom = forall(x, forall(y, (s(x) === s(y)) ==> (x === y)))
- final val ax3neutral: Axiom = forall(x, plus(x, zero) === x)
- final val ax4plus: Axiom = forall(x, forall(y, plus(x, s(y)) === s(plus(x, y))))
- final val ax5: Axiom = forall(x, times(x, zero) === zero)
- final val ax6: Axiom = forall(x, forall(y, times(x, s(y)) === plus(times(x, y), x)))
- final val ax7induction: Axiom = (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, Axiom)] = Set(
- ("A1", ax1ZeroSuccessor),
- ("A2", ax2Injectivity),
- ("A3", ax3neutral),
- ("A4", ax4plus),
- ("A5", ax5),
- ("A6", ax6),
- ("Induction", ax7induction)
- )
- peanoAxioms.foreach(a => runningPeanoTheory.addAxiom(a._1, a._2))
+ export lisa.proven.PeanoArithmeticsLibrary.{*, given}
+ given output: (String => Unit) = println
}
diff --git a/src/main/scala/lisa/proven/mathematics/PeanoArithmetics.scala b/src/main/scala/lisa/proven/mathematics/PeanoArithmetics.scala
new file mode 100644
index 00000000..62801b59
--- /dev/null
+++ b/src/main/scala/lisa/proven/mathematics/PeanoArithmetics.scala
@@ -0,0 +1,39 @@
+package lisa.proven.mathematics
+
+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))
+}
--
GitLab