diff --git a/README.md b/README.md
index 1010401b023d4d7feabe2944a69e4a6a92dd20ee..be8c88f42a96a9fc992840c17a614e4711ee7e42 100644
--- a/README.md
+++ b/README.md
@@ -16,3 +16,19 @@ The TPTP package contains a parser from the TPTP file format to LISA. The simple
* `sbt test` to compile and execute the test suite
* `sbt assembly` to package it as a library
* `sbt doc` to generate the Scala documentation
+
+
+#LICENSE
+ Copyright [2022] [EPFL]
+
+ Licensed under the Apache License, Version 2.0 (the "License");
+ you may not use this file except in compliance with the License.
+ You may obtain a copy of the License at
+
+ http://www.apache.org/licenses/LICENSE-2.0
+
+ Unless required by applicable law or agreed to in writing, software
+ distributed under the License is distributed on an "AS IS" BASIS,
+ WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ See the License for the specific language governing permissions and
+ limitations under the License.
diff --git a/build.sbt b/build.sbt
new file mode 100644
index 0000000000000000000000000000000000000000..ea69a270c6d5c87bc4b98982aec362d0d4a820db
--- /dev/null
+++ b/build.sbt
@@ -0,0 +1,19 @@
+name := "lisa"
+organization := "ch.epfl.lara"
+licenses := Seq("Apache-2.0" -> url("https://www.apache.org/licenses/LICENSE-2.0.html"))
+
+version := "0.1"
+
+scalaVersion := "3.0.2"
+
+scalacOptions ++= Seq("-deprecation", "-feature")
+scalacOptions ++= Seq(
+ "-language:implicitConversions"
+)
+
+
+
+libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.10" % "test"
+libraryDependencies += "io.github.leoprover" % "scala-tptp-parser_2.13" % "1.4"
+Test / parallelExecution := false
+
diff --git a/project/build.properties b/project/build.properties
new file mode 100644
index 0000000000000000000000000000000000000000..8378cad582d4344fe3358570c7950936251be224
--- /dev/null
+++ b/project/build.properties
@@ -0,0 +1 @@
+sbt.version = 1.5.7
diff --git a/project/plugins.sbt b/project/plugins.sbt
new file mode 100644
index 0000000000000000000000000000000000000000..7bc4622d2c974aee1dc6dbcd1050a6b196ba9585
--- /dev/null
+++ b/project/plugins.sbt
@@ -0,0 +1 @@
+addSbtPlugin("com.eed3si9n" % "sbt-assembly" % "1.1.0")
diff --git a/src/main/scala/Example.scala b/src/main/scala/Example.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4e59959d529ef2d50abaff8b3e7e41eb3231876f
--- /dev/null
+++ b/src/main/scala/Example.scala
@@ -0,0 +1,163 @@
+
+import lisa.KernelHelpers.{*, given}
+import lisa.kernel.Printer.*
+import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.SCProofChecker.*
+import lisa.kernel.proof.SequentCalculus.*
+import lisa.kernel.proof.{SCProof, SCProofChecker}
+import proven.tactics.SimplePropositionalSolver.solveSequent
+import tptp.KernelParser.*
+import tptp.ProblemGatherer.getPRPproblems
+
+/**
+ * Discover some of the elements of LISA to get started.
+ */
+object Example {
+ def main(args: Array[String]):Unit = {
+ //proofExample() //uncomment when exercise finished
+ solverExample()
+ tptpExample()
+ }
+
+ /**
+ * A little example of a small LISA proof with holes to fill as an exercise.
+ * All interrogation marks have to be replaced by proof steps, (sets of) formulas or integers.
+ * The last two lines don't need to be changed.
+ */
+ def proofExample(): Unit = {
+ val proof: SCProof = SCProof(Vector(
+ ???,
+ ???,
+ ?????( Set(P(x), P(f(x)), P(f(x)) ==> P(f(f(x)))) |- P(f(f(x))), 1, 0, ????, ???? ),
+ Hypothesis( Set(P(x), P(f(x)) ==> P(f(f(x)))) |- Set(P(x), P(f(f(x)))), P(x) ),
+ LeftImplies( ???? |- ????, 3, 2, ????, ???? ),
+ LeftForall( Set(????, ????, ????) |- ????, 4, ????, x, x ),
+ LeftForall( Set(????, ????) |- ????, 5, P(x) ==> P(f(x)), x, f(x) ),
+ RightImplies( forall(x, P(x) ==> P(f(x))) |- P(x) ==> P(f(f(x))), 6, P(x), P(f(f(x))) ),
+ RightForall( forall(x, P(x) ==> P(f(x))) |- forall(x, P(x) ==> P(f(f(x)))), 7, P(x) ==> P(f(f(x))), x )
+ ))
+ checkProof(proof)
+ }
+
+
+ /**
+ * An example of how to use the simple propositional solver.
+ * The solver is complete (for propositional logic) but naive and won't succede on large formulas.
+ */
+ def solverExample(): Unit = {
+ println("\n --- Pierce's Law ---")
+ checkProof(solveSequent(emptySeq +> ((A ==> B) ==> A ==> A)))
+ println("\n --- Various Tautologies ---")
+ val tests: List[Sequent] = List(
+ () |- Q \/ !Q,
+ Q /\ !Q |- (),
+ A /\ B |- A,
+ A /\ B |- Set(B, Q),
+ A |- A \/ B,
+ Set(A, Q) |- A \/ B,
+ () |- (A /\ B) ==> (A \/ C),
+ Set(A, B) |- (A \/ C) /\ B,
+ () |- ((T ==> Q) /\ (R ==> S)) ==> ((T \/ R) ==> (Q \/ S)),
+ (T ==> Q) /\ (R ==> S) /\ (!Q \/ !S) |- !T \/ !R,
+ () |- ((T /\ Q) \/ (!T /\ R)) <=> ((T ==> Q) /\ (!T ==> R))
+ )
+ println("\n --- Wrong ---")
+ tests.map(solveSequent).zipWithIndex.foreach(p => {
+ println(s"\nPropositional statement no ${p._2}")
+ checkProof(p._1)
+ })
+ }
+
+ /**
+ * An example about how to use the tptp parser. Please note that only problems and formulas expressed in the
+ * fof or cnf language of tptp are supported.
+ */
+ def tptpExample(): Unit = {
+ val axioms = List(
+ "( ~ ( ? [X] : ( big_s(X) & big_q(X) ) ) )",
+ "( ! [X] : ( big_p(X) => ( big_q(X) | big_r(X) ) ) )",
+ "( ~ ( ? [X] : big_p(X) ) => ? [Y] : big_q(Y) )",
+ "( ! [X] : ( ( big_q(X) | big_r(X) ) => big_s(X) ) )"
+ )
+ val conjecture = "( ? [X] : ( big_p(X) & big_r(X) ) )"
+ val anStatements = List(
+ "fof(pel24_1,axiom,\n ( ~ ( ? [X] :\n ( big_s(X)\n & big_q(X) ) ) )).",
+ "\nfof(pel24_2,axiom,\n ( ! [X] :\n ( big_p(X)\n => ( big_q(X)\n | big_r(X) ) ) )).",
+ "fof(pel24_3,axiom,\n ( ~ ( ? [X] : big_p(X) )\n => ? [Y] : big_q(Y) )).",
+ "fof(pel24_4,axiom,\n ( ! [X] :\n ( ( big_q(X)\n | big_r(X) )\n => big_s(X) ) )).",
+ "fof(pel24,conjecture,\n ( ? [X] :\n ( big_p(X)\n & big_r(X) ) )).",
+ )
+
+ println("\n---Individual Fetched Formulas---")
+ axioms.foreach(a => println(prettyFormula(parseToKernel(a))))
+ println(prettyFormula(parseToKernel(conjecture)))
+
+ println("\n---Annotated Formulas---")
+ anStatements.map(annotatedFormulaToKernel).foreach(printAnnotatedFormula)
+
+ println("\n---Problems---")
+
+ try {
+ val probs = getPRPproblems
+ probs.foreach(p =>
+ println("Problem: "+p.name+" ("+p.domain+") --- "+p.file)
+ )
+
+ println("Number of problems found with PRP spc: "+probs.size)
+
+ if (probs.nonEmpty) {
+ println(" - First problem as illustration:")
+ val seq = problemToSequent(probs.head)
+ printProblem(probs.head)
+ println("\n---Sequent---")
+ println(prettySequent(seq))
+ }
+ }
+ catch {
+ case error:NullPointerException => println("You can download the tptp library at http://www.tptp.org/ and put it in main/resources")
+ }
+
+
+
+ }
+
+
+
+
+
+
+
+ // Utility
+ def printAnnotatedFormula(a:AnnotatedFormula):Unit = {
+ if (a.role == "axiom") println("Given " + a.name + ": " + prettyFormula(a.formula))
+ else if (a.role == "conjecture") println("Prove " + a.name + ": " + prettyFormula(a.formula))
+ else println(a.role + " " + a.name + ": " + prettyFormula(a.formula))
+ }
+
+ def printProblem(p:Problem) : Unit = {
+ println("Problem: "+p.name+" ("+p.domain+") ---")
+ println("Status: "+p.status)
+ println("SPC: "+p.spc.mkString(", "))
+ p.formulas.foreach(printAnnotatedFormula)
+ }
+ private def checkProof(proof: SCProof): Unit = {
+ val error = SCProofChecker.checkSCProof(proof)
+ println(prettySCProof(proof, error))
+ }
+
+ val P = SchematicPredicateLabel("P", 1)
+
+ val Q = PredicateFormula(SchematicPredicateLabel("Q", 0), Seq())
+ val R = PredicateFormula(SchematicPredicateLabel("R", 0), Seq())
+ val S = PredicateFormula(SchematicPredicateLabel("S", 0), Seq())
+ val T = PredicateFormula(SchematicPredicateLabel("T", 0), Seq())
+ val A = PredicateFormula(SchematicPredicateLabel("A", 0), Seq())
+ val B = PredicateFormula(SchematicPredicateLabel("B", 0), Seq())
+ val C = PredicateFormula(SchematicPredicateLabel("C", 0), Seq())
+ val x = VariableLabel("x")
+ val f = ConstantFunctionLabel("f", 1)
+
+
+ def ???? :Formula = ???
+ def ?????(args: Any*) = ???
+}
diff --git a/src/main/scala/lisa/KernelHelpers.scala b/src/main/scala/lisa/KernelHelpers.scala
new file mode 100644
index 0000000000000000000000000000000000000000..afa8008b772cbc7fbacf9675770866a6caf86995
--- /dev/null
+++ b/src/main/scala/lisa/KernelHelpers.scala
@@ -0,0 +1,81 @@
+package lisa
+
+
+object KernelHelpers {
+
+ import lisa.kernel.proof.SequentCalculus.Sequent
+ import lisa.kernel.fol.FOL.*
+
+ // Prefix
+ def neg(f: Formula): Formula = ConnectorFormula(Neg, Seq(f))
+ def and(l: Formula, r: Formula): Formula = ConnectorFormula(And, Seq(l, r))
+ def or(l: Formula, r: Formula): Formula = ConnectorFormula(Or, Seq(l, r))
+ def implies(l: Formula, r: Formula): Formula = ConnectorFormula(Implies, Seq(l, r))
+ def iff(l: Formula, r: Formula): Formula = ConnectorFormula(Iff, Seq(l, r))
+ def forall(label: VariableLabel, body: Formula): Formula = BinderFormula(Forall, label, body)
+ def exists(label: VariableLabel, body: Formula): Formula = BinderFormula(Exists, label, body)
+ def existsOne(label: VariableLabel, body: Formula): Formula = BinderFormula(ExistsOne, label, body)
+ def equ(l: Term, r: Term): Formula = PredicateFormula(equality, Seq(l, r))
+
+ extension (label: PredicateLabel)
+ def apply(args: Term*): Formula = PredicateFormula(label, args)
+
+ extension (label: ConnectorLabel)
+ def apply(args: Formula*): Formula = ConnectorFormula(label, args)
+
+ extension (label: FunctionLabel)
+ def apply(args: Term*): Term = FunctionTerm(label, args)
+
+ extension (label: BinderLabel)
+ def apply(bound: VariableLabel, inner: Formula): Formula = BinderFormula(label, bound, inner)
+
+ // Infix
+ extension (f: Formula) {
+ def unary_! : Formula = neg(f)
+ infix def ==>(g: Formula): Formula = implies(f, g)
+ infix def <=>(g: Formula): Formula = iff(f, g)
+ infix def /\(g: Formula): Formula = and(f, g)
+ infix def \/(g: Formula): Formula = or(f, g)
+ }
+
+ extension (t: Term)
+ infix def ===(u: Term): Formula = PredicateFormula(equality, Seq(t, u))
+
+ // Other
+ given Conversion[VariableLabel, VariableTerm] = VariableTerm.apply
+ given Conversion[VariableTerm, VariableLabel] = _.label
+
+ val emptySeq = Sequent(Set.empty, Set.empty)
+
+ extension (l: Unit)
+ infix def |-(r: Iterable[Formula]): Sequent = Sequent(Set.empty, r.toSet)
+ infix def |-(r: Formula): Sequent = Sequent(Set.empty, Set(r))
+ infix def |-(r: Unit): Sequent = emptySeq
+ extension (l: Iterable[Formula])
+ infix def |-(r: Iterable[Formula]): Sequent = Sequent(l.toSet, r.toSet)
+ infix def |-(r: Formula): Sequent = Sequent(l.toSet, Set(r))
+ infix def |-(r: Unit): Sequent = Sequent(l.toSet, Set.empty)
+ extension (l: Formula)
+ infix def |-(r: Iterable[Formula]): Sequent = Sequent(Set(l), r.toSet)
+ infix def |-(r: Formula): Sequent = Sequent(Set(l), Set(r))
+ infix def |-(r: Unit): Sequent = Sequent(Set(l), Set.empty)
+
+ // given Conversion[Tuple, List[Union[_.type]]] = _.toList
+
+ given Conversion[(Boolean, List[Int], String), Option[(List[Int], String)]] = tr => if (tr._1) None else Some(tr._2, tr._3)
+
+
+
+ extension (s: Sequent) {
+ infix def +<(f: Formula): Sequent = s.copy(left = s.left + f)
+ infix def -<(f: Formula): Sequent = s.copy(left = s.left - f)
+ infix def +>(f: Formula): Sequent = s.copy(right = s.right + f)
+ infix def ->(f: Formula): Sequent = s.copy(right = s.right - f)
+ infix def ++<(s1: Sequent): Sequent = s.copy(left = s.left ++ s1.left)
+ infix def --<(s1: Sequent): Sequent = s.copy(left = s.left -- s1.left)
+ infix def ++>(s1: Sequent): Sequent = s.copy(right = s.right ++ s1.right)
+ infix def -->(s1: Sequent): Sequent = s.copy(right = s.right -- s1.right)
+ infix def ++(s1: Sequent): Sequent = s.copy(left = s.left ++ s1.left, right = s.right ++ s1.right)
+ infix def --(s1: Sequent): Sequent = s.copy(left = s.left -- s1.left, right = s.right -- s1.right)
+ }
+}
diff --git a/src/main/scala/lisa/kernel/Printer.scala b/src/main/scala/lisa/kernel/Printer.scala
new file mode 100644
index 0000000000000000000000000000000000000000..752eb43f989520fbdf1d7ece469ceee2689637cc
--- /dev/null
+++ b/src/main/scala/lisa/kernel/Printer.scala
@@ -0,0 +1,281 @@
+package lisa.kernel
+
+import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.SequentCalculus._
+import lisa.kernel.proof.SCProof
+
+/**
+ * A set of methods to pretty-print kernel trees.
+ */
+object Printer {
+
+ private def spaceSeparator(compact: Boolean): String = if(compact) "" else " "
+ private def commaSeparator(compact: Boolean, symbol: String = ","): String = s"$symbol${spaceSeparator(compact)}"
+
+ private def prettyParentheses(content: String): String = s"(${content})"
+
+ private def prettyFunction(name: String, args: Seq[String], compact: Boolean, dropParentheses: Boolean = true): String = {
+ if(dropParentheses && args.isEmpty) name else s"$name(${args.mkString(commaSeparator(compact))})"
+ }
+
+ private def prettyInfix(operator: String, left: String, right: String, compact: Boolean): String =
+ Seq(left, operator, right).mkString(spaceSeparator(compact))
+
+ // Special symbols that aren't defined in this theory
+ private val (membership, subsetOf, sameCardinality) = (
+ ConstantPredicateLabel("set_membership", 2),
+ ConstantPredicateLabel("subset_of", 2),
+ ConstantPredicateLabel("same_cardinality", 2)
+ )
+ private val (emptySet, unorderedPair, orderedPair, singleton, powerSet, unionSet) = (
+ ConstantFunctionLabel("empty_set", 0),
+ ConstantFunctionLabel("unordered_pair", 2),
+ ConstantFunctionLabel("ordered_pair", 2),
+ ConstantFunctionLabel("singleton", 1),
+ ConstantFunctionLabel("power_set", 1),
+ ConstantFunctionLabel("union", 1),
+ )
+ private val nonAtomicPredicates = Set(equality, membership, subsetOf, sameCardinality) // Predicates which require parentheses (for readability)
+
+ private def prettyFormulaInternal(formula: Formula, isRightMost: Boolean, compact: Boolean): String = formula match {
+ case PredicateFormula(label, args) => label match {
+ case `equality` => args match {
+ case Seq(l, r) => prettyInfix(label.id, prettyTerm(l), prettyTerm(r), compact)
+ case _ => throw new Exception
+ }
+ case `membership` => args match {
+ case Seq(l, r) => prettyInfix("∈", prettyTerm(l), prettyTerm(r), compact)
+ case _ => throw new Exception
+ }
+ case `subsetOf` => args match {
+ case Seq(l, r) => prettyInfix("⊆", prettyTerm(l), prettyTerm(r), compact)
+ case _ => throw new Exception
+ }
+ case `sameCardinality` => args match {
+ case Seq(l, r) => prettyInfix("~", prettyTerm(l), prettyTerm(r), compact)
+ case _ => throw new Exception
+ }
+ case _ => prettyFunction(label.id, args.map(prettyTerm(_, compact)), compact)
+ }
+ case ConnectorFormula(label, args) =>
+ (label, args) match {
+ case (Neg, Seq(arg)) =>
+ val isAtomic = arg match {
+ case PredicateFormula(label, _) => !nonAtomicPredicates.contains(label)
+ case ConnectorFormula(Neg, _) => true
+ case _ => false
+ }
+ val bodyString = prettyFormulaInternal(arg, isRightMost, compact)
+ val bodyParenthesized = if(isAtomic) bodyString else prettyParentheses(bodyString)
+ s"${label.id}${bodyParenthesized}"
+ case (binary @ (Implies | Iff | And | Or), Seq(l, r)) =>
+ val precedences: Map[ConnectorLabel, Int] = Map(
+ And -> 1,
+ Or -> 2,
+ Implies -> 3,
+ Iff -> 4,
+ )
+ val precedence = precedences(binary)
+ val isLeftParentheses = l match {
+ case _: BinderFormula => true
+ case PredicateFormula(leftLabel, _) => nonAtomicPredicates.contains(leftLabel)
+ case ConnectorFormula(leftLabel, _) => precedences.get(leftLabel).exists(_ >= precedence)
+ }
+ val isRightParentheses = r match {
+ case _: BinderFormula => !isRightMost
+ case PredicateFormula(leftLabel, _) => nonAtomicPredicates.contains(leftLabel)
+ case ConnectorFormula(rightLabel, _) => precedences.get(rightLabel).exists(_ > precedence)
+ }
+ val (leftString, rightString) = (prettyFormulaInternal(l, isLeftParentheses, compact), prettyFormulaInternal(r, isRightMost || isRightParentheses, compact))
+ val leftParenthesized = if(isLeftParentheses) prettyParentheses(leftString) else leftString
+ val rightParenthesized = if(isRightParentheses) prettyParentheses(rightString) else rightString
+ prettyInfix(label.id, leftParenthesized, rightParenthesized, compact)
+ case _ => label.id+"("+args.map(a => prettyFormulaInternal(a, isRightMost, compact)).mkString(",")+")" //throw new Exception // Invalid number of arguments, cannot print
+ }
+ case BinderFormula(label, bound, inner) =>
+ def accumulateNested(f: Formula, acc: Seq[VariableLabel]): (Seq[VariableLabel], Formula) = f match {
+ case BinderFormula(`label`, nestBound, nestInner) => accumulateNested(nestInner, nestBound +: acc)
+ case _ => (acc, f)
+ }
+ val (bounds, innerNested) = accumulateNested(inner, Seq(bound))
+ Seq(s"${label.id}${bounds.reverse.map(_.id).mkString(commaSeparator(compact))}.", prettyFormulaInternal(innerNested, true, compact)).mkString(spaceSeparator(compact))
+ }
+
+ /**
+ * Returns a string representation of this formula. See also {@link prettyTerm}.
+ * Example output:
+ * <pre>
+ * ∀x, y. (∀z. (z ∈ x) ↔ (z ∈ y)) ↔ (x = y)
+ * </pre>
+ * @param formula the formula
+ * @param compact if spaces should be omitted between separators
+ * @return the string representation of this formula
+ */
+ def prettyFormula(formula: Formula, compact: Boolean = false): String = prettyFormulaInternal(formula, true, compact)
+
+ /**
+ * Returns a string representation of this term. See also {@link prettyFormula}.
+ * Example output:
+ * <pre>
+ * f({w, (x, y)}, z)
+ * </pre>
+ * @param term the term
+ * @param compact if spaces should be omitted between separators
+ * @return the string representation of this term
+ */
+ def prettyTerm(term: Term, compact: Boolean = false): String = term match {
+ case VariableTerm(label) => label.id
+ case FunctionTerm(label, args) =>
+ label match {
+ case `emptySet` => args match {
+ case Seq() => prettyFunction("∅", Seq.empty, compact, dropParentheses = true)
+ case _ => throw new Exception
+ }
+ case `unorderedPair` => args match {
+ case Seq(l, r) => s"{${Seq(l, r).map(prettyTerm(_, compact)).mkString(commaSeparator(compact))}}"
+ case _ => throw new Exception
+ }
+ case `orderedPair` => args match {
+ case Seq(l, r) => s"(${Seq(l, r).map(prettyTerm(_, compact)).mkString(commaSeparator(compact))})"
+ case _ => throw new Exception
+ }
+ case `singleton` => args match {
+ case Seq(s) => s"{${prettyTerm(s)}}"
+ case _ => throw new Exception
+ }
+ case `powerSet` => args match {
+ case Seq(s) => prettyFunction("P", Seq(prettyTerm(s)), compact)
+ case _ => throw new Exception
+ }
+ case `unionSet` => args match {
+ case Seq(s) => prettyFunction("U", Seq(prettyTerm(s)), compact)
+ case _ => throw new Exception
+ }
+ case _ => prettyFunction(label.id, args.map(prettyTerm(_, compact)), compact)
+ }
+ }
+
+ /**
+ * Returns a string representation of this sequent.
+ * Example output:
+ * <pre>
+ * ⊢ ∀x, y. (∀z. (z ∈ x) ↔ (z ∈ y)) ↔ (x = y)
+ * </pre>
+ * @param sequent the sequent
+ * @param compact if spaces should be omitted between separators
+ * @return the string representation of this sequent
+ */
+ def prettySequent(sequent: Sequent, compact: Boolean = false): String = {
+ def prettyFormulas(set: Set[Formula]): String = set.toSeq.map(prettyFormula(_, compact)).sorted.mkString(commaSeparator(compact, ";"))
+ Seq(prettyFormulas(sequent.left), "⊢", prettyFormulas(sequent.right)).filter(_.nonEmpty).mkString(spaceSeparator(compact))
+ }
+
+ /**
+ * Returns a string representation of this proof.
+ * @param proof the proof
+ * @param showError if set, marks that particular step in the proof (`->`) as an error
+ * @return a string where each indented line corresponds to a step in the proof
+ */
+ def prettySCProof(proof: SCProof, showError: Option[(Seq[Int], String)] = None): String = {
+ def computeMaxNumbering(proof: SCProof, level: Int, result: IndexedSeq[Int]): IndexedSeq[Int] = {
+ val resultWithCurrent = result.updated(level, Math.max(proof.steps.size - 1, result(level)))
+ proof.steps.collect { case sp: SCSubproof => sp }.foldLeft(resultWithCurrent)((acc, sp) => computeMaxNumbering(sp.sp, level + 1, if(acc.size <= level + 1) acc :+ 0 else acc))
+ }
+ val maxNumbering = computeMaxNumbering(proof, 0, IndexedSeq(0)) // The maximum value for each number column
+ val maxNumberingLengths = maxNumbering.map(_.toString.length)
+ val maxLevel = maxNumbering.size - 1
+
+ def leftPadSpaces(v: Any, n: Int): String = {
+ val s = String.valueOf(v)
+ if(s.length < n) (" " * (n - s.length)) + s else s
+ }
+ def rightPadSpaces(v: Any, n: Int): String = {
+ val s = String.valueOf(v)
+ if(s.length < n) s + (" " * (n - s.length)) else s
+ }
+ def prettySCProofRecursive(proof: SCProof, level: Int, tree: IndexedSeq[Int], topMostIndices: IndexedSeq[Int]): Seq[(Boolean, String, String, String)] = {
+ val printedImports = proof.imports.zipWithIndex.reverse.flatMap { case (imp, i) =>
+ val currentTree = tree :+ (-i-1)
+ val showErrorForLine = showError.exists((position, reason) => currentTree.startsWith(position) && currentTree.drop(position.size).forall(_ == 0))
+ val prefix = (Seq.fill(level - topMostIndices.size)(None) ++ Seq.fill(topMostIndices.size)(None) :+ Some(-i-1)) ++ Seq.fill(maxLevel - level)(None)
+ val prefixString = prefix.map(_.map(_.toString).getOrElse("")).zipWithIndex.map { case (v, i1) => leftPadSpaces(v, maxNumberingLengths(i1)) }.mkString(" ")
+ def pretty(stepName: String, topSteps: Int*): (Boolean, String, String, String) =
+ (
+ showErrorForLine,
+ prefixString,
+ Seq(stepName, topSteps.mkString(commaSeparator(compact = false))).filter(_.nonEmpty).mkString(" "),
+ prettySequent(imp)
+ )
+
+ Seq(pretty("Import", 0))
+ }
+ printedImports ++ proof.steps.zipWithIndex.flatMap { case (step, i) =>
+ val currentTree = tree :+ i
+ val showErrorForLine = showError.exists((position, reason) => currentTree.startsWith(position) && currentTree.drop(position.size).forall(_ == 0))
+ val prefix = (Seq.fill(level - topMostIndices.size)(None) ++ Seq.fill(topMostIndices.size)(None) :+ Some(i)) ++ Seq.fill(maxLevel - level)(None)
+ val prefixString = prefix.map(_.map(_.toString).getOrElse("")).zipWithIndex.map { case (v, i1) => leftPadSpaces(v, maxNumberingLengths(i1)) }.mkString(" ")
+ def pretty(stepName: String, topSteps: Int*): (Boolean, String, String, String) =
+ (
+ showErrorForLine,
+ prefixString,
+ Seq(stepName, topSteps.mkString(commaSeparator(compact = false))).filter(_.nonEmpty).mkString(" "),
+ prettySequent(step.bot)
+ )
+ def prettyDefinition(stepName: String, left: String, right: String, condition: Option[String] = None): (Boolean, String, String, String) =
+ ( // This method is an alternative to print something more meaningful for definitions
+ showErrorForLine,
+ prefixString,
+ stepName,
+ Seq(Seq(left, ":=", right) ++ condition.toSeq).filter(_.nonEmpty).map(_.mkString(" ")).mkString(", ")
+ )
+ step match {
+ case sp @ SCSubproof(_, _, true) => pretty("Subproof", sp.premises*) +: prettySCProofRecursive(sp.sp, level + 1, currentTree, (if(i == 0) topMostIndices else IndexedSeq.empty) :+ i)
+ case other =>
+
+ val line = other match {
+ case Rewrite(_, t1) => pretty("Rewrite", t1)
+ case Hypothesis(_, _) => pretty("Hypo.")
+ case Cut(_, t1, t2, _) => pretty("Cut", t1, t2)
+ case LeftAnd(_, t1, _, _) => pretty("Left ∧", t1)
+ case LeftNot(_, t1, _) => pretty("Left ¬", t1)
+ case RightOr(_, t1, _, _) => pretty("Right ∨", t1)
+ case RightNot(_, t1, _) => pretty("Right ¬", t1)
+ case LeftExists(_, t1, _, _) => pretty("Left ∃", t1)
+ case LeftForall(_, t1, _, _, _) => pretty("Left ∀", t1)
+ case LeftOr(_, l, _) => pretty("Left ∨", l*)
+ case RightExists(_, t1, _, _, _) => pretty("Right ∃", t1)
+ case RightForall(_, t1, _, _) => pretty("Right ∀", t1)
+ case RightAnd(_, l,_) => pretty("Right ∧", l*)
+ case RightIff(_, t1, t2, _, _) => pretty("Right ↔", t1, t2)
+ case RightImplies(_, t1, _, _) => pretty("Right →", t1)
+ case Weakening(_, t1) => pretty("Weakening", t1)
+ case LeftImplies(_, t1, t2, _, _) => pretty("Left →", t1, t2)
+ case LeftIff(_, t1, _, _) => pretty("Left ↔", t1)
+ case LeftRefl(_, t1, _) => pretty("L. Axiom", t1)
+ case RightRefl(_, _) => pretty("R. Axiom")
+ case LeftSubstEq(_, t1, _, _, _, _) => pretty("L. SubstEq", t1)
+ case RightSubstEq(_, t1, _, _, _, _) => pretty("R. SubstEq", t1)
+ case LeftSubstIff(_, t1, _, _, _, _) => pretty("L. SubstIff", t1)
+ case RightSubstIff(_, t1, _, _, _, _) => pretty("R. SubstIff", t1)
+ case SCSubproof(_, _, false) => pretty("SCSubproof (hidden)")
+ case other => throw new Exception(s"No available method to print this proof step, consider updating Printer.scala\n$other")
+ }
+ Seq(line)
+ }
+ }
+ }
+
+
+ val marker = "->"
+
+ val lines = prettySCProofRecursive(proof, 0, IndexedSeq.empty, IndexedSeq.empty)
+ val maxStepNameLength = lines.map { case (_, _, stepName, _) => stepName.length }.maxOption.getOrElse(0)
+ lines.map {
+ case (isMarked, indices, stepName, sequent) =>
+ val suffix = Seq(indices, rightPadSpaces(stepName, maxStepNameLength), sequent)
+ val full = if(showError.nonEmpty) (if(isMarked) marker else leftPadSpaces("", marker.length)) +: suffix else suffix
+ full.mkString(" ")
+ }.mkString("\n")+(if (showError.nonEmpty) s"\nProof checker has reported error at line ${showError.get._1}: ${showError.get._2}" else "")
+ }
+
+}
diff --git a/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala b/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala
new file mode 100644
index 0000000000000000000000000000000000000000..054b4aafe16d2576cbfae65aee69bae1c523d92d
--- /dev/null
+++ b/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala
@@ -0,0 +1,28 @@
+package lisa.kernel.fol
+
+/**
+ * Definitions that are common to terms and formulas.
+ */
+private[fol] trait CommonDefinitions {
+ val MaxArity: Int = 1000000
+ /**
+ * An object with arity information for tree-like structures.
+ */
+ protected trait Arity {
+ val arity: Int
+ }
+
+ /**
+ * An labelled node for tree-like structures.
+ *
+ */
+ protected trait Label[A <: Label[A]] extends Ordered[A] {
+ val id: String
+ }
+
+ def freshId(taken: Set[String], base: String): String = {
+ var i = 0;
+ while (taken contains base + "_" + i) i += 1
+ base + "_" + i
+ }
+}
diff --git a/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala b/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a4f79c526ad5ed0fde2ed8eb2bf1dbef6c70bda7
--- /dev/null
+++ b/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
@@ -0,0 +1,335 @@
+package lisa.kernel.fol
+
+import scala.annotation.tailrec
+import scala.collection.mutable
+import scala.math.Numeric.IntIsIntegral
+
+
+/**
+ * An EquivalenceChecker is an object that allows to detect some notion of equivalence between formulas
+ * and between terms.
+ * This allows the proof checker and writer to avoid having to deal with a class of "easy" equivalence.
+ * For example, by considering "x ∨ y" as being the same formula as "y ∨ x", we can avoid frustrating errors.
+ * For soundness, this relation should always be a subrelation of the usual FOL implication.
+ * The implementation checks for Orthocomplemented Bismeilatices equivalence, plus symetry and reflexivity
+ * of equality and alpha-equivalence.
+ */
+private[fol] trait EquivalenceChecker extends FormulaDefinitions {
+ sealed abstract class SimpleFormula {
+ val size: Int
+ private[EquivalenceChecker] var normalForm: Option[NormalFormula] = None
+ }
+ case class SimplePredicate(id: PredicateLabel, args: List[Term]) extends SimpleFormula {
+ val size = 1
+ }
+ case class SNeg(child: SimpleFormula) extends SimpleFormula {
+ val size: Int = 1 + child.size
+ }
+ case class SOr(children: List[SimpleFormula]) extends SimpleFormula {
+ val size: Int = (children map (_.size)).foldLeft(1) { case (a, b) => a + b }
+ }
+ case class SForall(x: String, inner: SimpleFormula) extends SimpleFormula {
+ val size: Int = 1 + inner.size
+ }
+ case class SExists(x: String, inner: SimpleFormula) extends SimpleFormula {
+ val size: Int = 1 + inner.size
+ }
+ case class SLiteral(b: Boolean) extends SimpleFormula {
+ val size = 1
+ normalForm = Some(NLiteral(b))
+ }
+ sealed abstract class NormalFormula {
+ val code:Int
+ }
+ case class NormalPredicate(id: PredicateLabel, args: List[Term], code:Int) extends NormalFormula
+ case class NNeg(child: NormalFormula, code:Int) extends NormalFormula
+ case class NOr(children: List[NormalFormula], code:Int) extends NormalFormula
+ case class NForall(x: String, inner: NormalFormula, code:Int) extends NormalFormula
+ case class NExists(x: String, inner: NormalFormula, code:Int) extends NormalFormula
+ case class NLiteral(b: Boolean) extends NormalFormula{
+ val code:Int = if (b) 1 else 0
+ }
+
+
+ /**
+ * A class that encapsulate "runtime" information of the equivalence checker. It performs memoization for efficiency.
+ */
+ class LocalEquivalenceChecker {
+ private val unsugaredVersion = scala.collection.mutable.HashMap[Formula, SimpleFormula]()
+
+ // transform a LISA formula into a simpler, desugarised version with less symbols. Conjunction, implication, iff, existsOne are treated as alliases and translated.
+ def removeSugar(phi: Formula): SimpleFormula = unsugaredVersion.getOrElseUpdate(phi, {
+ phi match {
+ case PredicateFormula(label, args) => SimplePredicate(label, args.toList)
+ case ConnectorFormula(label, args) => label match {
+ case Neg => SNeg(removeSugar(args(0)))
+ case Implies =>
+ val l = removeSugar(args(0))
+ val r = removeSugar(args(1))
+ SOr(List(SNeg(l), r))
+ case Iff =>
+ val l = removeSugar(args(0))
+ val r = removeSugar(args(1))
+ val c1 = SNeg(SOr(List(SNeg(l), r)))
+ val c2 = SNeg(SOr(List(SNeg(r), l)))
+ SNeg(SOr(List(c1, c2)))
+ case And =>
+ SNeg(SOr(args.map(c => SNeg(removeSugar(c))).toList))
+ case Or => SOr((args map removeSugar).toList)
+ }
+ case BinderFormula(label, bound, inner) => label match {
+ case Forall => SForall(bound.id, removeSugar(inner))
+ case Exists => SExists(bound.id, removeSugar(inner))
+ case ExistsOne =>
+ val y = VariableLabel(freshId(inner.freeVariables.map(_.id), bound.id))
+ val c1 = SimplePredicate(equality, List(VariableTerm(bound), VariableTerm(y)))
+ val c2 = removeSugar(inner)
+ val c1_c2 = SOr(List(SNeg(c1), c2))
+ val c2_c1 = SOr(List(SNeg(c2), c1))
+ SExists(y.id, SForall(bound.id,
+ SNeg(SOr(List(SNeg(c1_c2), SNeg(c2_c1))))
+ ))
+ }
+ }
+ })
+
+ def toLocallyNameless(t: Term, subst: Map[VariableLabel, Int], i: Int): Term = t match {
+ case VariableTerm(label) =>
+ if (subst.contains(label)) VariableTerm(VariableLabel("x" + (i - subst(label))))
+ else VariableTerm(VariableLabel("_" + label))
+ case FunctionTerm(label, args) => FunctionTerm(label, args.map(c => toLocallyNameless(c, subst, i)))
+ }
+
+ def toLocallyNameless(phi: SimpleFormula, subst: Map[VariableLabel, Int], i: Int): SimpleFormula = phi match {
+ case SimplePredicate(id, args) => SimplePredicate(id, args.map(c => toLocallyNameless(c, subst, i)))
+ case SNeg(child) => SNeg(toLocallyNameless(child, subst, i))
+ case SOr(children) => SOr(children.map(toLocallyNameless(_, subst, i)))
+ case SForall(x, inner) => SForall("", toLocallyNameless(inner, subst + (VariableLabel(x) -> i), i + 1))
+ case SExists(x, inner) => SExists("", toLocallyNameless(inner, subst + (VariableLabel(x) -> i), i + 1))
+ case SLiteral(b) => phi
+ }
+
+ private val codesSig: mutable.HashMap[(String, Seq[Int]), Int] = mutable.HashMap()
+ codesSig.update(("zero", Nil), 0)
+ codesSig.update(("one", Nil), 1)
+
+ val codesTerms: mutable.HashMap[Term, Int] = mutable.HashMap()
+ val codesSigTerms: mutable.HashMap[(TermLabel, Seq[Int]), Int] = mutable.HashMap()
+
+ def codesOfTerm(t: Term): Int = codesTerms.getOrElseUpdate(t, t match {
+ case VariableTerm(label) =>
+ codesSigTerms.getOrElseUpdate((label, Nil), codesSigTerms.size)
+ case FunctionTerm(label, args) =>
+ val c = args map codesOfTerm
+
+ codesSigTerms.getOrElseUpdate((label, c), codesSigTerms.size)
+ })
+
+ /*
+ def hasNormaleRecComputed(sf:SimpleFormula): Boolean = sf.normalForm.nonEmpty && (sf match {
+ case SNeg(child) => hasNormaleRecComputed(child)
+ case SOr(children) => children.forall(c => hasNormaleRecComputed(c))
+ case SForall(x, inner) => hasNormaleRecComputed(inner)
+ case SExists(x, inner) => hasNormaleRecComputed(inner)
+ case _ => true
+ })
+ */
+ def checkForContradiction(children:List[(NormalFormula, Int)]): Boolean = {
+ val (negatives_temp, positives) = children.foldLeft[(List[NormalFormula], List[NormalFormula])]((Nil, Nil))(
+ (acc, ch) => acc match {
+ case (negatives, positives) => ch._1 match {
+ case NNeg(child, c) =>(child::negatives, positives)
+ case _ => (negatives, ch._1::positives)
+ }
+ }
+ )
+ val negatives = negatives_temp.sortBy(_.code)
+ var i, j = 0
+ while (i<positives.size && j<negatives.size){ //checks if there is a positive and negative nodes with same code.
+ val (c1, c2) = (positives(i).code, negatives(j).code)
+ if (c1<c2) i+=1
+ else if (c1 == c2) return true
+ else j+=1
+ }
+ var k = 0
+ val children_codes = children.map(c => c._2).toSet //check if there is a negated disjunction whose children all share a code with an uncle
+ while(k<negatives.size){
+ negatives(k) match {
+ case NOr(gdChildren, c) =>
+ if (gdChildren.forall(sf => children_codes.contains(sf.code))) return true
+ case _ => ()
+ }
+ k+=1
+ }
+ false
+ }
+
+ def updateCodesSig(sig: (String, Seq[Int])): Int = {
+ if (!codesSig.contains(sig)) codesSig.update(sig, codesSig.size)
+ codesSig(sig)
+ }
+
+
+ def OCBSLCode(phi: SimpleFormula): Int = {
+ if (phi.normalForm.nonEmpty) return phi.normalForm.get.code
+ val L = pDisj(phi, Nil)
+ val L2 = L zip (L map (_.code))
+ val L3 = L2.sortBy(_._2).distinctBy(_._2).filterNot(_._2 == 0) //actually efficient has set based implementation already
+ if (L3.isEmpty) {
+ phi.normalForm = Some(NLiteral(false))
+ } else if (L3.length == 1) {
+ phi.normalForm = Some(L3.head._1)
+ } else if (L3.exists(_._2 == 1) || checkForContradiction(L3) ) {
+ phi.normalForm = Some(NLiteral(true))
+ } else {
+ phi.normalForm = Some(NOr(L3.map(_._1), updateCodesSig(("or", L3.map(_._2)))))
+ }
+ phi.normalForm.get.code
+ }
+
+ def pDisj(phi: SimpleFormula, acc: List[NormalFormula]): List[NormalFormula] = {
+ if (phi.normalForm.nonEmpty) return pDisjNormal(phi.normalForm.get, acc)
+ val r: List[NormalFormula] = phi match {
+ case SimplePredicate(id, args) =>
+ val lab = "pred_" + id.id + "_" + id.arity
+ if (id == equality) {
+ if (codesOfTerm(args(0)) == codesOfTerm(args(1)))
+ phi.normalForm = Some(NLiteral(true))
+ else
+ phi.normalForm = Some(NormalPredicate(id, args, updateCodesSig((lab, (args map codesOfTerm).sorted))))
+ } else {
+ phi.normalForm = Some(NormalPredicate(id, args, updateCodesSig((lab, args map codesOfTerm))))
+ }
+ phi.normalForm.get :: acc
+ case SNeg(child) => pNeg(child, phi, acc)
+ case SOr(children) => children.foldLeft(acc)((p, a) => pDisj(a, p))
+ case SForall(x, inner) =>
+ val r = OCBSLCode(inner)
+ phi.normalForm = Some(NForall(x, inner.normalForm.get, updateCodesSig(("forall", List(r)))))
+ phi.normalForm.get :: acc
+ case SExists(x, inner) =>
+ val r = OCBSLCode(inner)
+ phi.normalForm = Some(NExists(x, inner.normalForm.get, updateCodesSig(("exists", List(r)))))
+ phi.normalForm.get :: acc
+ case SLiteral(true) =>
+ phi.normalForm = Some(NLiteral(true))
+ phi.normalForm.get :: acc
+ case SLiteral(false) =>
+ phi.normalForm = Some(NLiteral(false))
+ phi.normalForm.get :: acc
+ }
+ r
+ }
+
+ def pNeg(phi: SimpleFormula, parent: SimpleFormula, acc: List[NormalFormula]): List[NormalFormula] = {
+ if (phi.normalForm.nonEmpty) return pNegNormal(phi.normalForm.get, parent, acc)
+ val r:List[NormalFormula] = phi match {
+ case SimplePredicate(id, args) =>
+ val lab = "pred_" + id.id + "_" + id.arity
+ if (id == equality) {
+ if (codesOfTerm(args(0)) == codesOfTerm(args(1)))
+ phi.normalForm = Some(NLiteral(true))
+ parent.normalForm = Some(NLiteral(false))
+ else
+ phi.normalForm = Some(NormalPredicate(id, args, updateCodesSig((lab, (args map codesOfTerm).sorted))))
+ parent.normalForm = Some(NNeg(phi.normalForm.get, updateCodesSig(("neg", List(phi.normalForm.get.code)))))
+ } else {
+ phi.normalForm = Some(NormalPredicate(id, args, updateCodesSig((lab, args map codesOfTerm))))
+ parent.normalForm = Some(NNeg(phi.normalForm.get, updateCodesSig(("neg", List(phi.normalForm.get.code)))))
+ }
+ parent.normalForm.get :: acc
+ case SNeg(child) => pDisj(child, acc)
+ case SForall(x, inner) =>
+ val r = OCBSLCode(inner)
+ phi.normalForm = Some(NForall(x, inner.normalForm.get, updateCodesSig(("forall", List(r)))))
+ parent.normalForm = Some(NNeg(phi.normalForm.get, updateCodesSig(("neg", List(phi.normalForm.get.code)))))
+ parent.normalForm.get :: acc
+ case SExists(x, inner) =>
+ val r = OCBSLCode(inner)
+ phi.normalForm = Some(NExists(x, inner.normalForm.get, updateCodesSig(("exists", List(r)))))
+ parent.normalForm = Some(NNeg(phi.normalForm.get, updateCodesSig(("neg", List(phi.normalForm.get.code)))))
+ parent.normalForm.get :: acc
+ case SLiteral(true) =>
+ parent.normalForm = Some(NLiteral(false))
+ parent.normalForm.get :: acc
+ case SLiteral(false) =>
+ parent.normalForm = Some(NLiteral(true))
+ parent.normalForm.get :: acc
+ case SOr(children) =>
+ val T = children.sortBy(_.size)
+ val r1 = T.tail.foldLeft(List[NormalFormula]())((p, a) => pDisj(a, p))
+ val r2 = r1 zip (r1 map (_.code))
+ val r3 = r2.sortBy(_._2).distinctBy(_._2).filterNot(_._2 == 0)
+ if (r3.isEmpty) pNeg(T.head, parent, acc)
+ else {
+ val s1 = pDisj(T.head, r1)
+ val s2 = s1 zip (s1 map (_.code))
+ val s3 = s2.sortBy(_._2).distinctBy(_._2).filterNot(_._2 == 0)
+ if (s3.exists(_._2 == 1) || checkForContradiction(s3) ) {
+ phi.normalForm=Some(NLiteral(true))
+ parent.normalForm = Some(NLiteral(false))
+ parent.normalForm.get :: acc
+ } else if (s3.length == 1) {
+ pNegNormal(s3.head._1, parent, acc)
+ } else {
+ phi.normalForm = Some(NOr(s3.map(_._1), updateCodesSig(("or", s3.map(_._2)))))
+ parent.normalForm = Some(NNeg(phi.normalForm.get, updateCodesSig(("neg", List(phi.normalForm.get.code)))))
+ parent.normalForm.get :: acc
+ }
+ }
+ }
+ r
+ }
+ def pDisjNormal(f:NormalFormula, acc:List[NormalFormula]):List[NormalFormula] = f match {
+ case NOr(children, c) => children ++ acc
+ case p@_ => p :: acc
+ }
+ def pNegNormal(f:NormalFormula, parent: SimpleFormula, acc:List[NormalFormula]): List[NormalFormula] = f match {
+ case NNeg(child, c) =>
+ pDisjNormal(child, acc)
+ case _ =>
+ parent.normalForm = Some(NNeg(f, updateCodesSig(("neg", List(f.code)))))
+ parent.normalForm.get :: acc
+ }
+
+ def check(formula1: Formula, formula2: Formula): Boolean = {
+ getCode(formula1) == getCode(formula2)
+ }
+ def getCode(formula:Formula): Int = OCBSLCode(toLocallyNameless(removeSugar(formula), Map.empty, 0))
+
+
+ def isSame(term1: Term, term2: Term): Boolean = codesOfTerm(term1) == codesOfTerm(term2)
+
+ def isSame(formula1: Formula, formula2: Formula): Boolean = {
+ this.check(formula1, formula2)
+ }
+
+ def isSameSet(s1: Set[Formula], s2:Set[Formula]): Boolean = {
+ s1.map(this.getCode).toList.sorted == s2.map(this.getCode).toList.sorted
+ }
+
+ def isSubset(s1:Set[Formula], s2:Set[Formula]): Boolean = {
+ val codesSet1 = s1.map(this.getCode)
+ val codesSet2 = s2.map(this.getCode)
+ codesSet1.subsetOf(codesSet2)
+
+ }
+ def contains(s:Set[Formula], f:Formula): Boolean = {
+ val codesSet= s.map(this.getCode)
+ val codesFormula = this.getCode(f)
+ codesSet.contains(codesFormula)
+ }
+
+
+
+ }
+ def isSame(term1: Term, term2: Term): Boolean = (new LocalEquivalenceChecker).isSame(term1, term2)
+
+ def isSame(formula1: Formula, formula2: Formula): Boolean = (new LocalEquivalenceChecker).isSame(formula1, formula2)
+
+ def isSameSet(s1: Set[Formula], s2:Set[Formula]): Boolean = (new LocalEquivalenceChecker).isSameSet(s1, s2)
+
+ def isSubset(s1:Set[Formula], s2:Set[Formula]): Boolean = (new LocalEquivalenceChecker).isSubset(s1, s2)
+
+ def contains(s:Set[Formula], f:Formula): Boolean = (new LocalEquivalenceChecker).contains(s, f)
+}
diff --git a/src/main/scala/lisa/kernel/fol/FOL.scala b/src/main/scala/lisa/kernel/fol/FOL.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6f09ba07e254e60994196c68795ab58e8278b000
--- /dev/null
+++ b/src/main/scala/lisa/kernel/fol/FOL.scala
@@ -0,0 +1,12 @@
+package lisa.kernel.fol
+
+/**
+ * The concrete implementation of first order logic.
+ * All its content can be imported using a single statement:
+ * <pre>
+ * import lisa.fol.FOL._
+ * </pre>
+ */
+object FOL extends FormulaDefinitions with EquivalenceChecker {
+
+}
diff --git a/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala b/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
new file mode 100644
index 0000000000000000000000000000000000000000..8e1e772bde023e8c6bb5f7494a29e34e43620ce8
--- /dev/null
+++ b/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
@@ -0,0 +1,159 @@
+package lisa.kernel.fol
+
+/**
+ * Definitions of formulas; analogous to [[TermDefinitions]].
+ * Depends on [[FormulaLabelDefinitions]] and [[TermDefinitions]].
+ */
+private[fol] trait FormulaDefinitions extends FormulaLabelDefinitions with TermDefinitions {
+
+ /**
+ * The parent class of formulas.
+ * A formula is a tree whose nodes are either terms or labeled by predicates or logical connectors.
+ */
+ sealed abstract class Formula extends TreeWithLabel[FormulaLabel] {
+ def predicates: Set[ConstantPredicateLabel]
+ def functions: Set[ConstantFunctionLabel]
+ //def predicatesSchemas: Set[PredicateLabel] = predicates filter { case _: ConstantPredicateLabel => false; case _: SchematicPredicateLabel => true }
+ }
+
+ /**
+ * The formula counterpart of [[PredicateLabel]].
+ */
+ final case class PredicateFormula(label: PredicateLabel, args: Seq[Term]) extends Formula {
+ override def freeVariables: Set[VariableLabel] = args.foldLeft(Set.empty[VariableLabel])((prev, next) => prev union next.freeVariables)
+
+ override def predicates: Set[ConstantPredicateLabel] = label match {
+ case l: ConstantPredicateLabel => Set(l)
+ case l: SchematicPredicateLabel => Set()
+ }
+
+ override def functions: Set[ConstantFunctionLabel] = args.foldLeft(Set.empty[ConstantFunctionLabel])((prev, next) => prev union next.functions)
+ }
+
+
+ /**
+ * The formula counterpart of [[ConnectorLabel]].
+ */
+ final case class ConnectorFormula(label: ConnectorLabel, args: Seq[Formula]) extends Formula {
+ override def freeVariables: Set[VariableLabel] = args.foldLeft(Set.empty[VariableLabel])((prev, next) => prev union next.freeVariables)
+
+ override def predicates: Set[ConstantPredicateLabel] = args.foldLeft(Set.empty[ConstantPredicateLabel])((prev, next) => prev union next.predicates)
+
+ override def functions: Set[ConstantFunctionLabel] = args.foldLeft(Set.empty[ConstantFunctionLabel])((prev, next) => prev union next.functions)
+ }
+
+ /**
+ * The formula counterpart of [[BinderLabel]].
+ */
+ final case class BinderFormula(label: BinderLabel, bound: VariableLabel, inner: Formula) extends Formula {
+ override def freeVariables: Set[VariableLabel] = inner.freeVariables - bound
+
+ override def predicates: Set[ConstantPredicateLabel] = inner.predicates
+
+ override def functions: Set[ConstantFunctionLabel] = inner.functions
+ }
+
+ /**
+ * Performs the substitution of x by r in f. May rename bound variables of f if necessary
+ * to avoid capture of free variables in r.
+ *
+ * @param f The base formula
+ * @param x A variable, which should be free in f
+ * @param r A term that will replace x in f
+ * @return f[r/x]
+ */
+ def substituteVariable(f: Formula, x: VariableLabel, r: Term): Formula = f match {
+ case PredicateFormula(label, args) => PredicateFormula(label, args.map(substituteVariable(_, x, r)))
+ case ConnectorFormula(label, args) => ConnectorFormula(label, args.map(substituteVariable(_, x, r)))
+ case BinderFormula(label, bound, inner) =>
+ if (isSame(bound, x)) f
+ else {
+ val fv = r.freeVariables
+ if (fv.contains(bound)) {
+ val newBoundVariable = VariableLabel(freshId(fv.map(_.name), bound.name))
+ val newInner = substituteVariable(inner, bound, VariableTerm(newBoundVariable))
+ BinderFormula(label, newBoundVariable, substituteVariable(newInner, x, r))
+ }
+ else BinderFormula(label, bound, substituteVariable(inner, x, r))
+ }
+ }
+
+ def bindAll(binder: BinderLabel, vars: Seq[VariableLabel], phi:Formula): Formula =
+ vars.sortBy(_.name).foldLeft(phi)((f, v) => BinderFormula(binder, v, f))
+
+ /**
+ * Performs simultaneous substitution of multiple variables by multiple terms in a formula f.
+ *
+ * @param f The base formula
+ * @param m A map from variables to terms.
+ * @return t[m]
+ */
+ def simultaneousSubstitution(f: Formula, m: Map[VariableLabel, Term]): Formula = f match {
+ case PredicateFormula(label, args) => PredicateFormula(label, args.map(simultaneousSubstitution(_, m)))
+ case ConnectorFormula(label, args) => ConnectorFormula(label, args.map(simultaneousSubstitution(_, m)))
+ case BinderFormula(label, bound, inner) =>
+ val newSubst = m - bound
+ val fv = m.values.flatMap(_.freeVariables).toSet
+ if (fv.contains(bound)) {
+ val newBoundVariable = VariableLabel(freshId(fv.map(_.name), bound.name))
+ val newInner = substituteVariable(inner, bound, VariableTerm(newBoundVariable))
+ BinderFormula(label, newBoundVariable, simultaneousSubstitution(newInner, newSubst))
+ }
+ else BinderFormula(label, bound, simultaneousSubstitution(inner, newSubst))
+ }
+
+ /**
+ * Instantiate a schematic predicate symbol in a formula, using higher-order instantiation.
+ *
+ * @param phi The base formula
+ * @param p The symbol to replace
+ * @param psi A formula, seen as a function, that will replace p in t.
+ * @param a The "arguments" of psi when seen as a function rather than a ground formula.
+ * Those variables are replaced by the actual arguments of p.
+ * @return phi[psi(a1,..., an)/p]
+ */
+ def instantiatePredicateSchema(phi: Formula, p: SchematicPredicateLabel, psi: Formula, a: List[VariableLabel]): Formula = {
+ require(a.length == p.arity)
+ phi match {
+ case PredicateFormula(label, args) =>
+ if (isSame(label, p)) simultaneousSubstitution(psi, (a zip args).toMap)
+ else phi
+ case ConnectorFormula(label, args) => ConnectorFormula(label, args.map(instantiatePredicateSchema(_, p, psi, a)))
+ case BinderFormula(label, bound, inner) =>
+ val fv: Set[VariableLabel] = psi.freeVariables -- a
+ if (fv.contains(bound)) {
+ val newBoundVariable = VariableLabel(freshId(fv.map(_.name), bound.name))
+ val newInner = substituteVariable(inner, bound, VariableTerm(newBoundVariable))
+ BinderFormula(label, newBoundVariable, instantiatePredicateSchema(newInner, p, psi, a))
+ } else BinderFormula(label, bound, instantiatePredicateSchema(inner, p, psi, a))
+ }
+ }
+
+ /**
+ * Instantiate a schematic function symbol in a formula, using higher-order instantiation.
+ *
+ * @param phi The base formula
+ * @param f The symbol to replace
+ * @param r A term, seen as a function, that will replace f in t.
+ * @param a The "arguments" of r when seen as a function rather than a ground term.
+ * Those variables are replaced by the actual arguments of f.
+ * @return phi[r(a1,..., an)/f]
+ */
+ def instantiateFunctionSchema(phi: Formula, f: SchematicFunctionLabel, r: Term, a: List[VariableLabel]): Formula = {
+ require(a.length == f.arity)
+ phi match {
+ case PredicateFormula(label, args) => PredicateFormula(label, args.map(instantiateFunctionSchema(_, f, r, a)))
+ case ConnectorFormula(label, args) => ConnectorFormula(label, args.map(instantiateFunctionSchema(_, f, r, a)))
+ case BinderFormula(label, bound, inner) =>
+ val fv: Set[VariableLabel] = r.freeVariables -- a.toSet
+ if (fv.contains(bound)) {
+ val newBoundVariable = VariableLabel(freshId(fv.map(_.name), bound.name))
+ val newInner = substituteVariable(inner, bound, VariableTerm(newBoundVariable))
+ BinderFormula(label, newBoundVariable, instantiateFunctionSchema(newInner, f, r, a))
+ } else BinderFormula(label, bound, instantiateFunctionSchema(inner, f, r, a))
+ }
+ }
+
+ def instantiateBinder(f: BinderFormula, t: Term): Formula = substituteVariable(f.inner, f.bound, t)
+
+}
diff --git a/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala b/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
new file mode 100644
index 0000000000000000000000000000000000000000..81de8601f0bad8f71ddc954341e616a1ee9199d1
--- /dev/null
+++ b/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
@@ -0,0 +1,86 @@
+package lisa.kernel.fol
+
+/**
+ * Definitions of formula labels. Analogous to [[TermLabelDefinitions]].
+ */
+private[fol] trait FormulaLabelDefinitions extends CommonDefinitions {
+
+ /**
+ * The parent class of formula labels.
+ * It similar as with terms; they denote the Predicates and logical connector themselves, and not the terms they help forming.
+ * They label the nodes of a tree that defines a formula.
+ */
+ sealed abstract class FormulaLabel extends Label[FormulaLabel] {
+ def priority: Int = this match {
+ case _: ConstantPredicateLabel => 1
+ case _: SchematicPredicateLabel => 2
+ case _: ConnectorLabel => 3
+ case _: BinderLabel => 4
+ }
+
+ /**
+ * Compare two formula labels by type, then by arity, then by id.
+ */
+ def compare(that: FormulaLabel): Int = (this, that) match {
+ case (thi: ConstantPredicateLabel, tha: ConstantPredicateLabel) => (2 * (thi.arity compare tha.arity) + (thi.id compare tha.id)).sign
+ case (thi: SchematicPredicateLabel, tha: SchematicPredicateLabel) => (2 * (thi.arity compare tha.arity) + (thi.id compare tha.id)).sign
+ case (thi: ConnectorLabel, tha: ConnectorLabel) => thi.id compare tha.id
+ case (thi: BinderLabel, tha: BinderLabel) => thi.id compare tha.id
+ case _ => this.priority - that.priority
+ }
+ }
+
+ /**
+ * The label for a predicate, namely a function taking a fixed number of terms and returning a formula.
+ * In logical terms it is a predicate symbol.
+ */
+ sealed abstract class PredicateLabel extends FormulaLabel with Arity {
+ require(arity < MaxArity && arity >= 0)
+ }
+
+ /**
+ * A standard predicate symbol. Typical example are equality (=) and membership (∈)
+ */
+ final case class ConstantPredicateLabel(id: String, arity: Int) extends PredicateLabel
+
+ /**
+ * The equality symbol (=) for first order logic.
+ */
+ val equality: PredicateLabel = ConstantPredicateLabel("=", 2)
+
+ /**
+ * A predicate symbol that can be instantiated with any formula.
+ */
+ final case class SchematicPredicateLabel(id: String, arity: Int) extends PredicateLabel
+
+ /**
+ * The label for a connector, namely a function taking a fixed number of formulas and returning another formula.
+ */
+ sealed abstract class ConnectorLabel(val id: String, val arity: Int) extends FormulaLabel with Arity {
+ require(arity < MaxArity && arity >= -1)
+ }
+
+ case object Neg extends ConnectorLabel("¬", 1)
+
+ case object Implies extends ConnectorLabel("⇒", 2)
+
+ case object Iff extends ConnectorLabel("↔", 2)
+
+ case object And extends ConnectorLabel("∧", -1)
+
+ case object Or extends ConnectorLabel("∨", -1)
+
+ /**
+ * The label for a binder, namely an object with a body that has the ability to bind variables in it.
+ */
+ sealed abstract class BinderLabel(val id: String) extends FormulaLabel
+
+ case object Forall extends BinderLabel(id = "∀")
+
+ case object Exists extends BinderLabel(id = "∃")
+
+ case object ExistsOne extends BinderLabel(id = "∃!")
+
+ def isSame(l: FormulaLabel, r: FormulaLabel): Boolean = (l compare r) == 0
+
+}
diff --git a/src/main/scala/lisa/kernel/fol/TermDefinitions.scala b/src/main/scala/lisa/kernel/fol/TermDefinitions.scala
new file mode 100644
index 0000000000000000000000000000000000000000..03411af89036811ad6b942419ba3f739c7daccfc
--- /dev/null
+++ b/src/main/scala/lisa/kernel/fol/TermDefinitions.scala
@@ -0,0 +1,100 @@
+package lisa.kernel.fol
+
+/**
+ * Definitions of terms; depends on [[TermLabelDefinitions]].
+ */
+private[fol] trait TermDefinitions extends TermLabelDefinitions {
+
+ protected trait TreeWithLabel[A] {
+ val label: A
+
+ def freeVariables: Set[VariableLabel]
+
+ def functions: Set[ConstantFunctionLabel]
+ }
+
+
+ /**
+ * The parent classes of terms.
+ * A term is a tree with nodes labeled by functions labels or variables.
+ * The number of children of a node is restricted by the arity imposed by the label.
+ */
+ sealed abstract class Term extends TreeWithLabel[TermLabel]
+
+
+ /**
+ * A term which consists of a single variable.
+ *
+ * @param label The label of the variable.
+ */
+ final case class VariableTerm(label: VariableLabel) extends Term {
+ override def freeVariables: Set[VariableLabel] = Set(label)
+
+ override def functions: Set[ConstantFunctionLabel] = Set.empty
+ }
+
+ /**
+ * A term labelled by a function symbol. It must contain a number of children equal to the arity of the symbol
+ *
+ * @param label The label of the node
+ * @param args children of the node. The number of argument must be equal to the arity of the function.
+ */
+ final case class FunctionTerm(label: FunctionLabel, args: Seq[Term]) extends Term {
+ require(label.arity == args.size)
+
+ override def freeVariables: Set[VariableLabel] = args.foldLeft(Set.empty[VariableLabel])((prev, next) => prev union next.freeVariables)
+
+ override def functions: Set[ConstantFunctionLabel] = label match {
+ case l:ConstantFunctionLabel => args.foldLeft(Set.empty[ConstantFunctionLabel])((prev, next) => prev union next.functions) + l
+ case l:SchematicFunctionLabel => args.foldLeft(Set.empty[ConstantFunctionLabel])((prev, next) => prev union next.functions)
+ }
+
+ val arity: Int = args.size
+ }
+
+ /**
+ * Performs the substitution of x by r in t.
+ *
+ * @param t The base term
+ * @param x A variable, which should be free in t
+ * @param r A term that will replace x in t.
+ * @return t[r/x]
+ */
+ def substituteVariable(t: Term, x: VariableLabel, r: Term): Term = t match {
+ case VariableTerm(label) => if (isSame(label, x)) r else t
+ case FunctionTerm(label, args) => FunctionTerm(label, args.map(substituteVariable(_, x, r)))
+ }
+
+ /**
+ * Performs simultaneous substitution of multiple variables by multiple terms in a term t.
+ *
+ * @param t The base term
+ * @param m A map from variables to terms.
+ * @return t[m]
+ */
+ def simultaneousSubstitution(t: Term, m: Map[VariableLabel, Term]): Term = t match {
+ case VariableTerm(label) => m.getOrElse(label, t)
+ case FunctionTerm(label, args) => FunctionTerm(label, args.map(simultaneousSubstitution(_, m)))
+ }
+
+ /**
+ * instantiate a schematic function symbol in a term, using higher-order instantiation.
+ *
+ * @param t The base term
+ * @param f The symbol to replace
+ * @param r A term, seen as a function, that will replace f in t.
+ * @param a The "arguments" of r when seen as a function rather than a ground term.
+ * Those variables are replaced by the actual arguments of f.
+ * @return t[r(a1,..., an)/f]
+ */
+ def instantiateFunctionSchema(t: Term, f: SchematicFunctionLabel, r: Term, a: List[VariableLabel]): Term = {
+ require(a.length == f.arity)
+ t match {
+ case VariableTerm(label) => t
+ case FunctionTerm(label, args) =>
+ val newArgs = args.map(instantiateFunctionSchema(_, f, r, a))
+ if (isSame(label, f)) simultaneousSubstitution(r, (a zip newArgs).toMap)
+ else FunctionTerm(label, newArgs)
+ }
+ }
+}
diff --git a/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala b/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala
new file mode 100644
index 0000000000000000000000000000000000000000..288c27c1521c7c21b82c51228958b68ed19558db
--- /dev/null
+++ b/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala
@@ -0,0 +1,70 @@
+package lisa.kernel.fol
+
+/**
+ * Definitions of term labels.
+ */
+private[fol] trait TermLabelDefinitions extends CommonDefinitions {
+ /**
+ * The parent class of term labels.
+ * These are labels that can be applied to nodes that form the tree of a term.
+ * For example, Powerset is not a term itself, it's a label for a node with a single child in a tree corresponding to a term.
+ * In logical terms, those labels are essentially symbols of sme language.
+ */
+ sealed abstract class TermLabel extends Label[TermLabel] {
+ def priority: Int = this match {
+ case _: VariableLabel => 1
+ case _: ConstantFunctionLabel => 2
+ case _: SchematicFunctionLabel => 3
+ }
+
+ /**
+ * Sorts labels according to first whether the term is a variable or function, then according to arity, then to the id.
+ */
+ def compare(that: TermLabel): Int = (this, that) match {
+ case (thi: VariableLabel, tha: VariableLabel) => thi.id compare tha.id
+ case (thi: ConstantFunctionLabel, tha: ConstantFunctionLabel) => (2 * (thi.arity compare tha.arity) + (thi.id compare tha.id)).sign
+ case (thi: SchematicFunctionLabel, tha: SchematicFunctionLabel) => (2 * (thi.arity compare tha.arity) + (thi.id compare tha.id)).sign
+ case _ => this.priority - that.priority
+ }
+ }
+
+ /**
+ * The label of a term which is a variable.
+ *
+ * @param id The name of the variable, for example "x" or "y".
+ */
+ final case class VariableLabel(id: String) extends TermLabel {
+ val name: String = id
+ }
+
+ /**
+ * The label of a function-like term. Constants are functions of arity 0.
+ * There are two kinds of function symbols: Standards and schematic.
+ * Standard function symbols denote a particular function. Schematic function symbols
+ * can be instantiated with any term. This is particularly useful to express axiom schemas.
+ */
+ sealed abstract class FunctionLabel extends TermLabel with Arity {
+ require(arity >= 0 && arity < MaxArity)
+ }
+
+ /**
+ * A function symbol.
+ *
+ * @param id The name of the function symbol.
+ * @param arity The arity of the function symbol. A function symbol of arity 0 is a constant
+ */
+ final case class ConstantFunctionLabel(id: String, arity: Int) extends FunctionLabel
+
+ /**
+ * A schematic function symbol that can be substituted.
+ *
+ * @param id The name of the function symbol.
+ * @param arity The arity of the function symbol. A function symbol of arity 0 is a constant
+ */
+ final case class SchematicFunctionLabel(id: String, arity: Int) extends FunctionLabel
+
+ /**
+ * A function returning true if and only if the two symbols are considered "the same".
+ */
+ def isSame(l: TermLabel, r: TermLabel): Boolean = (l compare r) == 0
+}
diff --git a/src/main/scala/lisa/kernel/proof/RunningTheory.scala b/src/main/scala/lisa/kernel/proof/RunningTheory.scala
new file mode 100644
index 0000000000000000000000000000000000000000..49a4688bc4b56e1e5333e04320da7824ddcc0d88
--- /dev/null
+++ b/src/main/scala/lisa/kernel/proof/RunningTheory.scala
@@ -0,0 +1,276 @@
+package lisa.kernel.proof
+
+import lisa.kernel.proof.SequentCalculus.*
+import lisa.kernel.proof.SCProofChecker.*
+import lisa.kernel.fol.FOL.*
+
+import scala.collection.mutable.Map as mMap
+import scala.collection.mutable.Set as mSet
+import scala.collection.immutable.Set
+
+/**
+ * This class describes the theory, i.e. the context and language, in which theorems are proven.
+ * A theory is built from scratch by introducing axioms and symbols first, then by definitional extensions.
+ * The structure is one-way mutable: Once an axiom or definition has been introduced, it can't be removed.
+ * On the other hand, theorems proven before the theory is extended will still hold.
+ * A theorem only holds true within a specific theory.
+ * A theory is responsible to make sure that a symbol already defined or present in the language can't
+ * be redefined. If a theory needs to be extanded in two different ways, or if a theory and its extension need
+ * to coexist independently, they should be different instances of this class.
+ */
+class RunningTheory {
+ /**
+ * A Justification is either a Theorem, an Axiom or a Definition
+ */
+ sealed abstract class Justification
+ /**
+ * A theorem encapsulate a sequent and assert that this sequent has been correctly proven and may be used safely in further proofs.
+ */
+ final case class Theorem private[RunningTheory](proposition: Sequent) extends Justification
+ /**
+ * An axiom is any formula that is assumed and considered true within the theory. It can freely be used later in any proof.
+ */
+ final case class Axiom private[RunningTheory](ax: Formula) extends Justification
+
+ /**
+ * A definition can be either a PredicateDefinition or a FunctionDefinition.
+ */
+ sealed abstract class Definition extends Justification
+
+ /**
+ * Define a predicate symbol as a shortcut for a formula. Example : P(x,y) := ∃!z. (x=y+z)
+ * @param label The name and arity of the new symbol
+ * @param args The variables representing the arguments of the predicate in the formula phi.
+ * @param phi The formula defining the predicate.
+ */
+ final case class PredicateDefinition private[RunningTheory](label: ConstantPredicateLabel, args: Seq[VariableLabel], phi:Formula) extends Definition
+
+ /**
+ * Define a function symbol as the unique element that has some property. The existence and uniqueness
+ * of that elements must have been proven before obtaining such a definition. Example
+ * f(x,y) := the "z" s.t. x=y+z
+ * @param label The name and arity of the new symbol
+ * @param args The variables representing the arguments of the predicate in the formula phi.
+ * @param out The variable representing the result of the function in phi
+ * @param phi The formula defining the function.
+ */
+ final case class FunctionDefinition private[RunningTheory](label: ConstantFunctionLabel, args: Seq[VariableLabel], out: VariableLabel, phi: Formula) extends Definition
+
+
+ private[proof] val theoryAxioms : mSet[Axiom] = mSet.empty
+ private[proof] val funDefinitions: mMap[FunctionLabel, Option[FunctionDefinition]] = mMap.empty
+ private[proof] val predDefinitions: mMap[PredicateLabel, Option[PredicateDefinition]] = mMap(equality -> None)
+
+ /**
+ * Check if a label is a symbol of the theory
+ */
+ def isAcceptedFunctionLabel(label:FunctionLabel): Boolean = funDefinitions.contains(label)
+ /**
+ * Check if a label is a symbol of the theory
+ */
+ def isAcceptedPredicateLabel(label:PredicateLabel): Boolean = predDefinitions.contains(label)
+
+ /**
+ * From a given proof, if it is true in the Running theory, returns a theorem that is valid in the given theory.
+ * The proof's imports must be justified by the list of justification, and the conclusion of the theorem
+ * can't contain symbols that do not belong to the theory.
+ * @param justifications The list of justifications of the proof's imports.
+ * @param p The proof of the desired Theorem.
+ * @return A Theorem if the proof is correct, None else
+ */
+ def proofToTheorem(p: SCProof, justifications:Seq[Justification]): Option[this.Theorem] =
+ if (checkProofWithinTheory(p, justifications) && belongsToTheory(p.conclusion))
+ Some(Theorem(p.conclusion))
+ else None
+
+
+ /**
+ * Introduce a new definition of a predicate in the theory. The symbol must not already exist in the theory
+ * and the formula can't contain symbols that are not in the theory.
+ * @param label The desired label.
+ * @param args The variables representing the arguments of the predicate in the formula phi.
+ * @param phi The formula defining the predicate.
+ * @return A definition object if the parameters are correct,
+ */
+ def makePredicateDefinition(label: ConstantPredicateLabel, args: Seq[VariableLabel], phi: Formula): Option[this.PredicateDefinition] = {
+ if (belongsToTheory(phi) && !isAcceptedPredicateLabel(label)) {
+ val newDef = PredicateDefinition(label, args, phi)
+ predDefinitions.update(label, Some(newDef))
+ Some(newDef)
+ } else {
+ None
+ }
+ }
+
+ /**
+ * Introduce a new definition of a function in the theory. The symbol must not already exist in the theory
+ * and the formula can't contain symbols that are not in the theory. The existence and uniqueness of an element
+ * satisfying the definition's formula must first be proven. This is easy if the formula behaves as a shortcut,
+ * for example f(x,y) = 3x+2y
+ * but is much more general. The proof's conclusion must be of the form: |- ∀args. ∃!out. phi
+ * @param proof The proof of existence and uniqueness
+ * @param justifications The justifications of the proof.
+ * @param label The desired label.
+ * @param args The variables representing the arguments of the predicate in the formula phi.
+ * @param out The variable representing the function's result in the formula
+ * @param phi The formula defining the predicate.
+ * @return A definition object if the parameters are correct,
+ */
+ def makeFunctionDefinition(proof: SCProof, justifications:Seq[Justification], label: ConstantFunctionLabel, args: Seq[VariableLabel], out: VariableLabel, phi: Formula): Option[this.FunctionDefinition] = {
+ if (belongsToTheory(phi) && !isAcceptedFunctionLabel(label) && checkProofWithinTheory(proof, justifications)) {
+
+ proof.conclusion match{
+ case Sequent(l, r) if l.isEmpty && r.size == 1 =>
+ val subst = bindAll(ExistsOne, args, phi)
+ if (isSame(r.head, subst)){
+ val newDef = FunctionDefinition(label, args, out, phi)
+ funDefinitions.update(label, Some(newDef))
+ Some(newDef)
+ }
+ else None
+
+ case _ => None
+ }
+ } else {
+ None
+ }
+ }
+
+
+
+ /**
+ * Verify is a proof is correct withing a given Theory. It separately verifies if the proof is correct from
+ * a pure sequent calculus point of view, and if definitions and theorem imported into the proof are indeed
+ * part of the theory.
+ *
+ */
+ def checkProofWithinTheory(proof: SCProof, justifications: Seq[Justification]): Boolean = {
+
+ if (belongsToTheory(proof.conclusion)){
+ if (proof.imports.forall(i => justifications.exists( j => isSameSequent(i, sequentFromJustification(j))) ))
+ true
+ else
+ false
+ }
+ else false
+ }
+
+ private def sequentFromJustification(j:Justification): Sequent = j match {
+ case Theorem(proposition) => proposition
+ case Axiom(ax) => Sequent(Set.empty, Set(ax))
+ case PredicateDefinition(label, args, phi) =>
+ val inner = ConnectorFormula(Iff, Seq(PredicateFormula(label, args.map(VariableTerm.apply)), phi))
+ Sequent(Set(), Set(bindAll(Forall, args, inner)))
+ case FunctionDefinition(label, args, out, phi) =>
+ val inner = BinderFormula(Forall, out,
+ ConnectorFormula(Iff, Seq(
+ PredicateFormula(equality, Seq(FunctionTerm(label, args.map(VariableTerm.apply)), VariableTerm(out))),
+ phi
+ ))
+ )
+ Sequent(Set(), Set(
+ bindAll(Forall, args, inner)
+ ))
+
+ }
+
+
+
+
+ /**
+ * Verify if a given formula belongs to some language
+ * @param phi The formula to check
+ * @return Weather phi belongs to the specified language
+ */
+ def belongsToTheory(phi:Formula):Boolean = phi match {
+ case PredicateFormula(label, args) =>
+ label match {
+ case _: ConstantPredicateLabel => isAcceptedPredicateLabel(label) && args.forall(belongsToTheory)
+ case _: SchematicPredicateLabel => args.forall(belongsToTheory)
+ }
+ case ConnectorFormula(label, args) => args.forall(belongsToTheory)
+ case BinderFormula(label, bound, inner) => belongsToTheory(inner)
+ }
+
+ def makeFormulaBelongToTheory(phi:Formula) : Unit = {
+ phi.predicates.foreach(addSymbol)
+ phi.functions.foreach(addSymbol)
+ }
+ /**
+ * Verify if a given term belongs to some language
+ * @param t The term to check
+ * @return Weather t belongs to the specified language
+ */
+ def belongsToTheory(t:Term):Boolean = t match {
+ case VariableTerm(label) => true
+ case FunctionTerm(label, args) => label match {
+ case _: ConstantFunctionLabel => isAcceptedFunctionLabel(label) && args.forall(belongsToTheory(_))
+ case _: SchematicFunctionLabel => args.forall(belongsToTheory(_))
+ }
+
+ }
+ /**
+ * Verify if a given sequent belongs to some language
+ * @param s The sequent to check
+ * @return Weather s belongs to the specified language
+ */
+ def belongsToTheory(s:Sequent):Boolean =
+ s.left.forall(belongsToTheory(_)) && s.right.forall(belongsToTheory(_))
+
+
+ def makeSequentBelongToTheory(s:Sequent): Unit = {
+ s.left.foreach(makeFormulaBelongToTheory)
+ s.right.foreach(makeFormulaBelongToTheory)
+ }
+
+
+ /**
+ * Add a new axiom to the Theory. For example, if the theory contains the language and theorems
+ * of Zermelo-Fraenkel Set Theory, this function can add the axiom of choice to it.
+ * If the axiom belongs to the language of the theory, adds it and return true. Else, returns false.
+ * @param f the new axiom to be added.
+ * @return true if the axiom was added to the theory, false else.
+ */
+ def addAxiom(f:Formula):Boolean = {
+ if (belongsToTheory(f)){
+ theoryAxioms.add(Axiom(f))
+ true
+ }
+ else false
+ }
+
+ /**
+ * Add a new symbol to the theory, without providing a definition. An ad-hoc definition can be
+ * added via an axiom, typically if the desired object is not derivable in the base theory itself.
+ * For example, This function can add the empty set symbol to a theory, and then an axiom asserting
+ * the it is empty can be introduced as well.
+ */
+ def addSymbol(l:FunctionLabel):Unit = funDefinitions.update(l, None)
+ def addSymbol(l:PredicateLabel):Unit = predDefinitions.update(l, None)
+
+ /**
+ * Public accessor to the set of symbol currently in the theory's language.
+ * @return the set of symbol currently in the theory's language.
+ */
+ def language: (List[(FunctionLabel, Option[FunctionDefinition])], List[(PredicateLabel, Option[PredicateDefinition])]) = (funDefinitions.toList, predDefinitions.toList)
+ /**
+ * Public accessor to the current set of axioms of the theory
+ * @return the current set of axioms of the theory
+ */
+ def getAxioms: List[Axiom] = theoryAxioms.toList
+
+ /**
+ * Verify if a given formula is an axiom of the theory
+ * @param f the candidate axiom
+ * @return wether f is an axiom of the theory
+ */
+ def isAxiom(f:Formula): Boolean = theoryAxioms.exists(a => isSame(a.ax,f))
+
+}
+object RunningTheory {
+ /**
+ * An empty theory suitable to reason about first order logic.
+ */
+ def PredicateLogic: RunningTheory = RunningTheory()
+}
+
diff --git a/src/main/scala/lisa/kernel/proof/SCProof.scala b/src/main/scala/lisa/kernel/proof/SCProof.scala
new file mode 100644
index 0000000000000000000000000000000000000000..62573bc87c32a3a9218aa66f1f5d851b8523c471
--- /dev/null
+++ b/src/main/scala/lisa/kernel/proof/SCProof.scala
@@ -0,0 +1,98 @@
+package lisa.kernel.proof
+
+import lisa.kernel.proof.SequentCalculus._
+import lisa.kernel.proof.SCProofChecker._
+
+
+/**
+ * A SCPRoof (for Sequent Calculus Proof) is a (dependant) proof. While technically a proof is an Directed Acyclic Graph,
+ * here proofs are linearized and represented as a list of proof steps.
+ * Moreover, a proof can depend on some assumed, unproved, sequents specified in the second argument
+ * @param steps A list of Proof Steps that should form a valid proof. Each individual step should only refer to earlier
+ * proof steps as premisces.
+ * @param imports A list of assumed sequents that further steps may refer to. Imports are refered to using negative integers
+ * To refer to the first sequent of imports, use integer -1.
+ */
+case class SCProof(steps: IndexedSeq[SCProofStep], imports: IndexedSeq[Sequent] = IndexedSeq.empty) {
+ def numberedSteps: Seq[(SCProofStep, Int)] = steps.zipWithIndex
+
+ /**
+ * Fetches the <code>i</code>th step of the proof.
+ * @param i the index
+ * @return a step
+ */
+ def apply(i: Int): SCProofStep = {
+ if (i >= 0)
+ if (i >= steps.length) throw new IndexOutOfBoundsException(s"index $i is out of bounds of the steps Seq")
+ else steps(i)
+
+ else throw new IndexOutOfBoundsException(s"index $i is out of bounds of the steps Seq")
+ }
+
+ /**
+ * Get the ith sequent of the proof. If the index is positive, give the bottom sequent of proof step number i.
+ * If the index is positive, return the (-i-1)th imported sequent.
+ *
+ * @param i The reference number of a sequent in the proof
+ * @return A sequent, either imported or reached during the proof.
+ */
+ def getSequent(i:Int): Sequent = {
+ if (i >= 0)
+ if (i >= steps.length) throw new IndexOutOfBoundsException(s"index $i is out of bounds of the steps Seq")
+ else steps(i).bot
+ else
+ val i2 = -(i+1)
+ if (i2 >= imports.length) throw new IndexOutOfBoundsException(s"index $i is out of bounds of the imports Seq")
+ else imports(i2)
+
+ }
+
+ /**
+ * The length of the proof in terms of top-level steps, without including the imports.
+ */
+ def length: Int = steps.length
+
+
+ /**
+ * The total length of the proof in terms of proof-step, including steps in subproof, but excluding the imports.
+ */
+ def totalLength: Int = steps.foldLeft(0)((i, s) => i + (s match {
+ case s: SCSubproof => s.sp.totalLength + 1
+ case _ => 1
+ }))
+
+ /**
+ * The conclusion of the proof, namely the bottom sequent of the last proof step.
+ * Can be undefined if the proof is empty.
+ */
+ def conclusion: Sequent = {
+ if (steps.isEmpty) throw new NoSuchElementException("conclusion of an empty proof")
+ this(length - 1).bot
+ }
+
+ /**
+ * A helper method that creates a new proof with a new step appended at the end.
+ * @param newStep the new step to be added
+ * @return a new proof
+ */
+ def appended(newStep: SCProofStep): SCProof = copy(steps = steps appended newStep)
+
+ /**
+ * A helper method that creates a new proof with a sequence of new steps appended at the end.
+ * @param newSteps the sequence of steps to be added
+ * @return a new proof
+ */
+ def withNewSteps(newSteps: IndexedSeq[SCProofStep]): SCProof = copy(steps = steps ++ newSteps)
+}
+
+object SCProof {
+ /**
+ * Instantiates a proof from an indexed list of proof steps.
+ * @param steps the steps of the proof
+ * @return the corresponding proof
+ */
+ def apply(steps: SCProofStep*): SCProof = {
+ SCProof(steps.toIndexedSeq)
+ }
+
+}
diff --git a/src/main/scala/lisa/kernel/proof/SCProofChecker.scala b/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bb475952dff29893a69c8f56eb2d8b72469f5868
--- /dev/null
+++ b/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
@@ -0,0 +1,441 @@
+package lisa.kernel.proof
+
+import lisa.kernel.fol.FOL._
+import lisa.kernel.proof.SequentCalculus._
+
+object SCProofChecker {
+
+ private object Set {
+ def unapplySeq[T](s: Set[T]): Option[Seq[T]] = Some(s.toSeq)
+ }
+
+
+ /**
+ * This function verifies that a single SCProofStep is correctly applied. It verify that the step only refers to sequents with a lower number, and that
+ * the type and parameters of the proofstep correspond to the sequent claimed sequent.
+ *
+ * @param no The number of the given proof step. Needed to vewrify that the proof step doesn't refer to posterior sequents.
+ * @param step The proof step whose correctness needs to be checked
+ * @param references A function that associates sequents to a range of positive and negative integers that the proof step may refer to. Typically,
+ * a proof's [[SCProof.getSequent]] function.
+ * @return
+ */
+ def checkSingleSCStep(no:Int, step: SCProofStep, references : Int => Sequent, importsSize: Option[Int]=None):(Boolean, List[Int], String) = {
+ val ref = references
+ val false_premise = step.premises.find(i => i >= no)
+ val false_premise2 = if (importsSize.nonEmpty) step.premises.find(i => i< -importsSize.get) else None
+
+ val r: (Boolean, List[Int], String) =
+ if (false_premise.nonEmpty)
+ return (false, Nil, "A step can't refer to a step with a higher or equal number as a premise.")
+ if (false_premise2.nonEmpty)
+ return (false, Nil, "A step can't refer to a step with a lower number than minus the number of imports.")
+ else step match {
+ /*
+ * Γ |- Δ
+ * ------------
+ * Γ |- Δ
+ */
+ case Rewrite(s, t1) =>
+ if (isSameSequent(s, ref(t1))) (true, Nil, "") else (false, Nil, s"The premise and the conclusion are not trivially equivalent.")
+ /*
+ *
+ * --------------
+ * Γ, φ |- φ, Δ
+ */
+ case Hypothesis(Sequent(left, right), phi) =>
+ if (contains(left, phi))
+ if (contains(right, phi)) (true, Nil, "")
+
+ else (false, Nil, s"Right-hand side does not contain formula φ")
+ else (false, Nil, s"Left-hand side does not contain formula φ")
+ /*
+ * Γ |- Δ, φ φ, Σ |- Π
+ * ------------------------
+ * Γ, Σ |-Δ, Π
+ */
+ case Cut(b, t1, t2, phi) =>
+ if (isSameSet(b.left + phi, ref(t1).left union ref(t2).left))
+ if (isSameSet(b.right + phi, ref(t2).right union ref(t1).right))
+ if (ref(t2).left.contains(phi))
+ if (ref(t1).right.contains(phi))
+ (true, Nil, "")
+ else (false, Nil, s"Right-hand side of first premise does not contain φ as claimed.")
+ else (false, Nil, s"Left-hand side of second premise does not contain φ as claimed.")
+ else (false, Nil, s"Right-hand side of conclusion + φ is not the union of the right-hand sides of the premises.")
+ else (false, Nil, s"Left-hand side of conclusion + φ is not the union of the left-hand sides of the premises.")
+
+ // Left rules
+ /*
+ * Γ, φ |- Δ Γ, φ, ψ |- Δ
+ * -------------- or -------------
+ * Γ, φ∧ψ |- Δ Γ, φ∧ψ |- Δ
+ */
+ case LeftAnd(b, t1, phi, psi) =>
+ if (isSameSet(ref(t1).right, b.right))
+ val phiAndPsi = ConnectorFormula(And, Seq(phi, psi))
+ if (isSameSet(b.left + phi, ref(t1).left + phiAndPsi) ||
+ isSameSet(b.left + psi, ref(t1).left + phiAndPsi) ||
+ isSameSet(b.left + phi + psi, ref(t1).left + phiAndPsi))
+ (true, Nil, "")
+ else (false, Nil, "Left-hand side of conclusion + φ∧ψ must be same as left-hand side of premise + either φ, ψ or both.")
+ else (false, Nil, "Right-hand sides of the premise and the conclusion must be the same.")
+ /*
+ * Γ, φ |- Δ Σ, ψ |- Π
+ * ------------------------
+ * Γ, Σ, φ∨ψ |- Δ, Π
+ */
+ case LeftOr(b, t, disjuncts) =>
+ if (isSameSet(b.right, t.map(ref(_).right).reduce(_ union _)) )
+ val phiOrPsi = ConnectorFormula(Or, disjuncts)
+ if (isSameSet(disjuncts.foldLeft(b.left)(_ + _), t.map(ref(_).left).reduce(_ union _) + phiOrPsi))
+ (true, Nil, "")
+ else (false, Nil, s"Left-hand side of conclusion + disjuncts is not the same as the union of the left-hand sides of the premises + φ∨ψ.")
+ else (false, Nil, s"Right-hand side of conclusion is not the union of the right-hand sides of the premises.")
+ /*
+ * Γ |- φ, Δ Σ, ψ |- Π
+ * ------------------------
+ * Γ, Σ, φ→ψ |- Δ, Π
+ */
+ case LeftImplies(b, t1, t2, phi, psi) =>
+ val phiImpPsi = ConnectorFormula(Implies, Seq(phi, psi))
+ if (isSameSet(b.right + phi, ref(t1).right union ref(t2).right))
+ if (isSameSet(b.left + psi, ref(t1).left union ref(t2).left + phiImpPsi))
+ (true, Nil, "")
+ else (false, Nil, s"Left-hand side of conclusion + ψ must be identical to union of left-hand sides of premisces + φ→ψ.")
+ else (false, Nil, s"Right-hand side of conclusion + φ must be identical to union of right-hand sides of premisces.")
+ /*
+ * Γ, φ→ψ |- Δ Γ, φ→ψ, ψ→φ |- Δ
+ * -------------- or ---------------
+ * Γ, φ↔ψ |- Δ Γ, φ↔ψ |- Δ
+ */
+ case LeftIff(b, t1, phi, psi) =>
+ val phiImpPsi = ConnectorFormula(Implies, Seq(phi, psi))
+ val psiImpPhi = ConnectorFormula(Implies, Seq(psi, phi))
+ val phiIffPsi = ConnectorFormula(Iff, Seq(phi, psi))
+ if (isSameSet(ref(t1).right, b.right))
+ if (isSameSet(b.left + phiImpPsi , ref(t1).left + phiIffPsi) ||
+ isSameSet(b.left + psiImpPhi , ref(t1).left + phiIffPsi) ||
+ isSameSet(b.left + phiImpPsi + psiImpPhi , ref(t1).left + phiIffPsi))
+ (true, Nil, "")
+ else (false, Nil, "Left-hand side of conclusion + φ↔ψ must be same as left-hand side of premise + either φ→ψ, ψ→φ or both.")
+ else (false, Nil, "Right-hand sides of premise and conclusion must be the same.")
+
+ /*
+ * Γ |- φ, Δ
+ * --------------
+ * Γ, ¬φ |- Δ
+ */
+ case LeftNot(b, t1, phi) =>
+ val nPhi = ConnectorFormula(Neg, Seq(phi))
+ if (isSameSet(b.left, ref(t1).left + nPhi))
+ if (isSameSet(b.right + phi, ref(t1).right))
+ (true, Nil, "")
+ else (false, Nil, "Right-hand side of conclusion + φ must be the same as right-hand side of premise")
+ else (false, Nil, "Left-hand side of conclusion must be the same as left-hand side of premise + ¬φ")
+
+ /*
+ * Γ, φ[t/x] |- Δ
+ * -------------------
+ * Γ, ∀x. φ |- Δ
+ */
+ case LeftForall(b, t1, phi, x, t) =>
+ if (isSameSet(b.right, ref(t1).right))
+ if (isSameSet(b.left + substituteVariable(phi, x, t), ref(t1).left + BinderFormula(Forall, x, phi)))
+ (true, Nil, "")
+ else (false, Nil, "Left-hand side of conclusion + φ[t/x] must be the same as left-hand side of premise + ∀x. φ")
+ else (false, Nil, "Right-hand side of conclusion must be the same as right-hand side of premise")
+
+ /*
+ * Γ, φ |- Δ
+ * ------------------- if x is not free in the resulting sequent
+ * Γ, ∃x. φ|- Δ
+ */
+ case LeftExists(b, t1, phi, x) =>
+ if (isSameSet(b.right, ref(t1).right))
+ if (isSameSet(b.left + phi, ref(t1).left + BinderFormula(Exists, x, phi)))
+ if ((b.left union b.right).forall(f => !f.freeVariables.contains(x)))
+ (true, Nil, "")
+ else (false, Nil, "The variable x must not be free in the resulting sequent.")
+ else (false, Nil, "Left-hand side of conclusion + φ must be the same as left-hand side of premise + ∃x. φ")
+ else (false, Nil, "Right-hand side of conclusion must be the same as right-hand side of premise")
+
+ /*
+ * Γ, ∃y.∀x. (x=y) ↔ φ |- Δ
+ * ---------------------------- if y is not free in φ
+ * Γ, ∃!x. φ |- Δ
+ */
+ case LeftExistsOne(b, t1, phi, x) =>
+ val y = VariableLabel(freshId(phi.freeVariables.map(_.id) + x.id, "y"))
+ val temp = BinderFormula(Exists, y, BinderFormula(Forall, x, ConnectorFormula(Iff, List(PredicateFormula(equality, List(VariableTerm(x), VariableTerm(y))), phi))))
+ if (isSameSet(b.right, ref(t1).right))
+ if (isSameSet(b.left + temp, ref(t1).left + BinderFormula(ExistsOne, x, phi)))
+ (true, Nil, "")
+ else (false, Nil, "Left-hand side of conclusion + ∃y.∀x. (x=y) ↔ φ must be the same as left-hand side of premise + ∃!x. φ")
+ else (false, Nil, "Right-hand side of conclusion must be the same as right-hand side of premise")
+
+ // Right rules
+ /*
+ * Γ |- φ, Δ Σ |- ψ, Π
+ * ------------------------
+ * Γ, Σ |- φ∧ψ, Π, Δ
+ */
+ case RightAnd(b, t, cunjuncts) =>
+ val phiAndPsi = ConnectorFormula(And, cunjuncts)
+ if (isSameSet(b.left, t.map(ref(_).left).reduce(_ union _)))
+ if (isSameSet(cunjuncts.foldLeft(b.right)(_ + _), t.map(ref(_).right).reduce(_ union _) + phiAndPsi))
+ (true, Nil, "")
+ else (false, Nil, s"Right-hand side of conclusion + φ + ψ is not the same as the union of the right-hand sides of the premises φ∧ψ.")
+ else (false, Nil, s"Left-hand side of conclusion is not the union of the left-hand sides of the premises.")
+ /*
+ * Γ |- φ, Δ Γ |- φ, ψ, Δ
+ * -------------- or ---------------
+ * Γ |- φ∨ψ, Δ Γ |- φ∨ψ, Δ
+ */
+ case RightOr(b, t1, phi, psi) =>
+ val phiOrPsi = ConnectorFormula(Or, Seq(phi, psi))
+ if (isSameSet(ref(t1).left, b.left))
+ if (isSameSet(b.right + phi, ref(t1).right + phiOrPsi) ||
+ isSameSet(b.right + psi, ref(t1).right + phiOrPsi) ||
+ isSameSet(b.right + phi + psi, ref(t1).right + phiOrPsi))
+ (true, Nil, "")
+ else (false, Nil, "Right-hand side of conclusion + φ∧ψ must be same as right-hand side of premise + either φ, ψ or both.")
+ else (false, Nil, "Left-hand sides of the premise and the conclusion must be the same.")
+ /*
+ * Γ, φ |- ψ, Δ
+ * --------------
+ * Γ |- φ→ψ, Δ
+ */
+ case RightImplies(b, t1, phi, psi) =>
+ val phiImpPsi = ConnectorFormula(Implies, Seq(phi, psi))
+ if (isSameSet(ref(t1).left, b.left + phi))
+ if (isSameSet(b.right + psi, ref(t1).right + phiImpPsi))
+ (true, Nil, "")
+ else (false, Nil, "Right-hand side of conclusion + ψ must be same as right-hand side of premise + φ→ψ.")
+ else (false, Nil, "Left-hand side of conclusion + psi must be same as left-hand side of premise.")
+ /*
+ * Γ |- a→ψ, Δ Σ |- ψ→φ, Π
+ * ----------------------------
+ * Γ, Σ |- φ↔b, Π, Δ
+ */
+ case RightIff(b, t1, t2, phi, psi) =>
+ val phiImpPsi = ConnectorFormula(Implies, Seq(phi, psi))
+ val psiImpPhi = ConnectorFormula(Implies, Seq(psi, phi))
+ val phiIffPsi = ConnectorFormula(Iff, Seq(phi, psi))
+ if (isSameSet(b.left, ref(t1).left union ref(t2).left))
+ if (isSameSet(b.right + phiImpPsi + psiImpPhi, ref(t1).right union ref(t2).right + phiIffPsi))
+ (true, Nil, "")
+ else (false, Nil, s"Right-hand side of conclusion + a→ψ + ψ→φ is not the same as the union of the right-hand sides of the premises φ↔b.")
+ else (false, Nil, s"Left-hand side of conclusion is not the union of the left-hand sides of the premises.")
+ /*
+ * Γ, φ |- Δ
+ * --------------
+ * Γ |- ¬φ, Δ
+ */
+ case RightNot(b, t1, phi) =>
+ val nPhi = ConnectorFormula(Neg, Seq(phi))
+ if (isSameSet(b.right, ref(t1).right + nPhi))
+ if (isSameSet(b.left + phi, ref(t1).left))
+ (true, Nil, "")
+ else (false, Nil, "Left-hand side of conclusion + φ must be the same as left-hand side of premise")
+ else (false, Nil, "Right-hand side of conclusion must be the same as right-hand side of premise + ¬φ")
+ /*
+ * Γ |- φ, Δ
+ * ------------------- if x is not free in the resulting sequent
+ * Γ |- ∀x. φ, Δ
+ */
+ case RightForall(b, t1, phi, x) =>
+ if (isSameSet(b.left, ref(t1).left))
+ if (isSameSet(b.right + phi, ref(t1).right + BinderFormula(Forall, x ,phi)))
+ if ((b.left union b.right).forall(f => !f.freeVariables.contains(x)))
+ (true, Nil, "")
+ else (false, Nil, "The variable x must not be free in the resulting sequent.")
+ else (false, Nil, "Right-hand side of conclusion + φ must be the same as right-hand side of premise + ∀x. φ")
+ else (false, Nil, "Left-hand sides of conclusion and premise must be the same.")
+ /*
+ * Γ |- φ[t/x], Δ
+ * -------------------
+ * Γ |- ∃x. φ, Δ
+ */
+ case RightExists(b, t1, phi, x, t) =>
+ if (isSameSet(b.left, ref(t1).left))
+ if (isSameSet(b.right + substituteVariable(phi, x, t), ref(t1).right + BinderFormula(Exists, x ,phi)))
+ (true, Nil, "")
+ else (false, Nil, "Right-hand side of the conclusion + φ[t/x] must be the same as right-hand side of the premise + ∃x. φ")
+ else (false, Nil, "Left-hand sides or conclusion and premise must be the same.")
+
+ /**
+ * <pre>
+ * Γ |- ∃y.∀x. (x=y) ↔ φ, Δ
+ * ---------------------------- if y is not free in φ
+ * Γ|- ∃!x. φ, Δ
+ * </pre>
+ */
+ case RightExistsOne(b, t1, phi, x) =>
+ val y = VariableLabel(freshId(phi.freeVariables.map(_.id), "x"))
+ val temp = BinderFormula(Exists, y, BinderFormula(Forall, x, ConnectorFormula(Iff, List(PredicateFormula(equality, List(VariableTerm(x), VariableTerm(y))), phi))))
+ if (isSameSet(b.left, ref(t1).left))
+ if (isSameSet(b.right + temp, ref(t1).right + BinderFormula(ExistsOne, x, phi)))
+ (true, Nil, "")
+ else (false, Nil, "Right-hand side of conclusion + ∃y.∀x. (x=y) ↔ φ must be the same as right-hand side of premise + ∃!x. φ")
+ else (false, Nil, "Left-hand sides of conclusion and premise must be the same")
+
+
+ // Structural rules
+ /*
+ * Γ |- Δ
+ * --------------
+ * Γ, Σ |- Δ
+ */
+ case Weakening(b, t1) =>
+ if (isSubset(ref(t1).left, b.left))
+ if (isSubset(ref(t1).right, b.right))
+ (true, Nil, "")
+ else (false, Nil, "Right-hand side of premise must be a subset of right-hand side of conclusion")
+ else (false, Nil, "Left-hand side of premise must be a subset of left-hand side of conclusion")
+
+ // Equality Rules
+ /*
+ * Γ, s=s |- Δ
+ * --------------
+ * Γ |- Δ
+ */
+ case LeftRefl(b, t1, phi) =>
+ phi match {
+ case PredicateFormula(`equality`, Seq(left, right)) =>
+ if (isSame(left, right))
+ if (isSameSet(b.right, ref(t1).right))
+ if (isSameSet(b.left + phi, ref(t1).left))
+ (true, Nil, "")
+ else (false, Nil, s"Left-hand sides of the conclusion + φ must be the same as left-hand side of the premise.")
+ else (false, Nil, s"Right-hand sides of the premise and the conclusion aren't the same.")
+ else (false, Nil, s"φ is not an instance of reflexivity.")
+ case _ => (false, Nil, "φ is not an equality")
+ }
+
+ /*
+ *
+ * --------------
+ * |- s=s
+ */
+ case RightRefl(b, phi) =>
+ phi match {
+ case PredicateFormula(`equality`, Seq(left, right)) =>
+ if (isSame(left, right))
+ if (b.right.contains(phi))
+ (true, Nil, "")
+ else (false, Nil, s"Right-Hand side of conclusion does not contain φ")
+ else (false, Nil, s"φ is not an instance of reflexivity.")
+ case _ => (false, Nil, s"φ is not an equality.")
+ }
+
+ /*
+ * Γ, φ[s/?f] |- Δ
+ * ---------------------
+ * Γ, s=t, φ[t/?f] |- Δ
+ */
+ case LeftSubstEq(b, t1, s, t, phi, f) =>
+ val sEqT = PredicateFormula(equality, Seq(s, t))
+ val phi_s_for_f = instantiateFunctionSchema(phi, f, s, Nil)
+ val phi_t_for_f = instantiateFunctionSchema(phi, f, t, Nil)
+ if (f.arity == 0)
+ if (isSameSet(b.right, ref(t1).right))
+ if (isSameSet(b.left + phi_t_for_f, ref(t1).left + sEqT + phi_s_for_f) ||
+ isSameSet(b.left + phi_s_for_f, ref(t1).left + sEqT + phi_t_for_f))
+ (true, Nil, "")
+ else (false, Nil, "Left-hand sides of the conclusion + φ[s/?f] must be the same as left-hand side of the premise + s=t + φ[t/?f] (or with s and t swapped).")
+ else (false, Nil, "Right-hand sides of the premise and the conclusion aren't the same.")
+ else (false, Nil, "Function schema ?f must have arity 0")
+
+
+ /*
+ * Γ |- φ[s/?f], Δ
+ * ---------------------
+ * Γ, s=t |- φ[t/?f], Δ
+ */
+ case RightSubstEq(b, t1, s, t, phi, f) =>
+ val sEqt = PredicateFormula(equality, Seq(s, t))
+ if (f.arity == 0)
+ if (isSameSet(ref(t1).left + sEqt, b.left))
+ val phi_s_for_f = instantiateFunctionSchema(phi, f, s, Nil)
+ val phi_t_for_f = instantiateFunctionSchema(phi, f, t, Nil)
+ if (isSameSet(b.right + phi_s_for_f, ref(t1).right + phi_t_for_f) ||
+ isSameSet(b.right + phi_t_for_f, ref(t1).right + phi_s_for_f))
+ (true, Nil, "")
+ else (false, Nil, s"Right-hand side of the premise and the conclusion should be the same with each containing one of φ[s/?f] φ[t/?f], but it isn't the case." )
+ else (false, Nil, "Left-hand sides of the premise + s=t must be the same as left-hand side of the premise.")
+ else (false, Nil, "Function schema ?f must have arity 0.")
+ /*
+ * Γ, φ[ψ/?q] |- Δ
+ * ---------------------
+ * Γ, ψ↔τ, φ[τ/?q] |- Δ
+ */
+ case LeftSubstIff(b, t1, psi, tau, phi, q) =>
+ val psiIffTau = ConnectorFormula(Iff, Seq(psi, tau))
+ val phi_tau_for_q = instantiatePredicateSchema(phi, q, tau, Nil)
+ val phi_psi_for_q = instantiatePredicateSchema(phi, q, psi, Nil)
+ if (q.arity == 0)
+ if (isSameSet(b.right, ref(t1).right))
+ if (isSameSet(ref(t1).left + psiIffTau + phi_tau_for_q, b.left + phi_psi_for_q) ||
+ isSameSet(ref(t1).left + psiIffTau + phi_psi_for_q, b.left + phi_tau_for_q))
+ (true, Nil, "")
+ else (false, Nil, "Left-hand sides of the conclusion + φ[ψ/?q] must be the same as left-hand side of the premise + ψ↔τ + φ[τ/?q] (or with ψ and τ swapped).")
+ else (false, Nil, "Right-hand sides of the premise and the conclusion aren't the same.")
+ else (false, Nil, "Predicate schema ?q must have arity 0.")
+
+ /*
+ * Γ |- φ[ψ/?p], Δ
+ * ---------------------
+ * Γ, ψ↔τ |- φ[τ/?p], Δ
+ */
+ case RightSubstIff(b, t1, psi, tau, phi, q) =>
+ val psiIffTau = ConnectorFormula(Iff, Seq(psi, tau))
+ val phi_tau_for_q = instantiatePredicateSchema(phi, q, tau, Nil)
+ val phi_psi_for_q = instantiatePredicateSchema(phi, q, psi, Nil)
+ if (q.arity == 0)
+ if (isSameSet(ref(t1).left + psiIffTau, b.left))
+ if (isSameSet(b.right + phi_tau_for_q, ref(t1).right + phi_psi_for_q) ||
+ isSameSet(b.right + phi_psi_for_q, ref(t1).right + phi_tau_for_q))
+ (true, Nil, "")
+ else (false, Nil, s"Right-hand side of the premise and the conclusion should be the same with each containing one of φ[τ/?q] and φ[ψ/?q], but it isn't the case." )
+ else (false, Nil, "Left-hand sides of the premise + ψ↔τ must be the same as left-hand side of the premise.")
+ else (false, Nil, "Predicate schema ?q must have arity 0.")
+
+ case SCSubproof(sp, premises, _) =>
+ if (premises.size == sp.imports.size){
+ val invalid = premises.zipWithIndex.find((no, p) => !isSameSequent(ref(no), sp.imports(p)) )
+ if (invalid.isEmpty){
+ val r_subproof = checkSCProof(sp)
+ if (r_subproof._1)
+ (true, Nil, "")
+ else (false, r_subproof._2, "Subproof reports an error:\n"+r_subproof._3)
+ } else (false, Nil, s"Premise number ${invalid.get._1} (refering to step ${invalid.get}) is not the same as import number ${invalid.get._1} of the subproof.")
+ } else (false, Nil, "Number of premises and imports don't match: "+premises.size+" "+sp.imports.size)
+
+ }
+ r
+ }
+
+ /**
+ * Verifies if a given pure SequentCalculus is conditionally correct, as the imported sequents are assumed.
+ * If the proof is not correct, the functrion will report the faulty line and a brief explanation.
+ * @param proof A SC proof to check
+ * @return (true, Nil, "") if the proof is correct, else (false, l, s) with l the path to the incorrect
+ proof step and s an explanation.
+ *
+ */
+ def checkSCProof(proof: SCProof) : (Boolean, List[Int], String) = {
+
+
+ val possibleError = proof.steps.view.zipWithIndex.map((step, no) =>
+
+ val r = checkSingleSCStep(no, step, (i:Int) => proof.getSequent(i), Some(proof.imports.size))
+ (r._1, no::r._2, r._3)
+ ).find(p => !p._1 )
+ if (possibleError.isEmpty) (true, Nil, "")
+ else possibleError.get
+
+
+ }
+
+}
diff --git a/src/main/scala/lisa/kernel/proof/SequentCalculus.scala b/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
new file mode 100644
index 0000000000000000000000000000000000000000..cf79543367bde60c6c3ce6827dff22f56f695eaf
--- /dev/null
+++ b/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
@@ -0,0 +1,286 @@
+package lisa.kernel.proof
+
+import lisa.kernel.fol.FOL._
+import scala.collection.immutable.Set
+
+
+/**
+ * The concrete implementation of sequent calculus (with equality).
+ * This file specifies the sequents and the allowed operations on them, the deduction rules of sequent calculus.
+ * It contains typical sequent calculus rules for FOL with equality as can be found in a text book, as well as a couple more for
+ * non-elementary symbols (↔, ∃!) and rules for substituting equal terms or equivalent formulas. I also contains two structural rules,
+ * subproof and a dummy rewrite step.
+ * Further mathematical steps, such as introducing or using definitions, axioms or theorems are not part of the basic sequent calculus.
+ */
+object SequentCalculus {
+
+
+
+ /**
+ * A sequent is an object that can contain two sets of formulas, [[left]] and [[right]].
+ * The intended semantic is for the [[left]] formulas to be interpreted as a conjunction, while the [[right]] ones as a disjunction.
+ * Traditionally, sequents are represented by two lists of formulas.
+ * Since sequent calculus includes rules for permuting and weakening, it is in essence equivalent to sets.
+ * Seqs make verifying proof steps much easier, but proof construction much more verbose and proofs longer.
+ * @param left the left side of the sequent
+ * @param right the right side of the sequent
+ */
+ case class Sequent(left: Set[Formula], right: Set[Formula])
+
+ /**
+ * Simple method that transforms a sequent to a logically equivalent formula.
+ *
+ */
+ def sequentToFormula(s:Sequent): Formula = ConnectorFormula(Implies, List(ConnectorFormula(And, s.left.toSeq), ConnectorFormula(Or, s.right.toSeq)))
+ /**
+ * Checks whether two sequents are equivalent, with respect to [[isSame]].
+ * @param l the first sequent
+ * @param r the second sequent
+ * @return see [[isSame]]
+ */
+ def isSameSequent(l: Sequent, r: Sequent): Boolean = isSame(sequentToFormula(l), sequentToFormula(r))
+
+ /**
+ * The parent of all proof steps types.
+ * A proof step is a deduction rule of sequent calculus, with the sequents forming the prerequisite and conclusion.
+ * For easier linearisation of the proof, the prerequisite are represented with numbers showing the place in the proof of the sequent used.
+ */
+
+ /**
+ * The parent of all sequent calculus rules.
+ */
+ sealed trait SCProofStep {
+ val bot: Sequent
+ val premises : Seq[Int]
+ }
+
+ /**
+ * <pre>
+ * Γ |- Δ
+ * ------------
+ * Γ |- Δ
+ * </pre>
+ */
+ case class Rewrite(bot: Sequent, t1: Int) extends SCProofStep{val premises = Seq(t1)}
+ /**
+ * <pre>
+ *
+ * --------------
+ * Γ, φ |- φ, Δ
+ * </pre>
+ */
+ case class Hypothesis(bot: Sequent, phi: Formula) extends SCProofStep{val premises = Seq()}
+ /**
+ * <pre>
+ * Γ |- Δ, φ φ, Σ |- Π
+ * ------------------------
+ * Γ, Σ |-Δ, Π
+ * </pre>
+ */
+ case class Cut(bot: Sequent, t1: Int, t2: Int, phi: Formula) extends SCProofStep{val premises = Seq(t1, t2)}
+
+ // Left rules
+ /**
+ * <pre>
+ * Γ, φ |- Δ Γ, φ, ψ |- Δ
+ * -------------- or --------------
+ * Γ, φ∧ψ |- Δ Γ, φ∧ψ |- Δ
+ * </pre>
+ */
+ case class LeftAnd(bot: Sequent, t1: Int, phi: Formula, psi: Formula) extends SCProofStep{val premises = Seq(t1)}
+ /**
+ * <pre>
+ * Γ, φ |- Δ Σ, ψ |- Π ...
+ * --------------------------------
+ * Γ, Σ, φ∨ψ∨... |- Δ, Π
+ * </pre>
+ */
+ case class LeftOr(bot: Sequent, t:Seq[Int], disjuncts:Seq[Formula]) extends SCProofStep{val premises = t}
+ /**
+ * <pre>
+ * Γ |- φ, Δ Σ, ψ |- Π
+ * ------------------------
+ * Γ, Σ, φ→ψ |- Δ, Π
+ * </pre>
+ */
+ case class LeftImplies(bot: Sequent, t1: Int, t2: Int, phi: Formula, psi: Formula) extends SCProofStep{val premises = Seq(t1, t2)}
+ /**
+ * <pre>
+ * Γ, φ→ψ |- Δ Γ, φ→ψ, ψ→φ |- Δ
+ * -------------- or --------------------
+ * Γ, φ↔ψ |- Δ Γ, φ↔ψ |- Δ
+ * </pre>
+ */
+ case class LeftIff(bot: Sequent, t1: Int, phi: Formula, psi: Formula) extends SCProofStep{val premises = Seq(t1)}
+ /**
+ * <pre>
+ * Γ |- φ, Δ
+ * --------------
+ * Γ, ¬φ |- Δ
+ * </pre>
+ */
+ case class LeftNot(bot: Sequent, t1: Int, phi: Formula) extends SCProofStep{val premises = Seq(t1)}
+ /**
+ * <pre>
+ * Γ, φ[t/x] |- Δ
+ * -------------------
+ * Γ, ∀ φ |- Δ
+ *
+ * </pre>
+ */
+ case class LeftForall(bot: Sequent, t1: Int, phi: Formula, x: VariableLabel, t: Term) extends SCProofStep{val premises = Seq(t1)}
+ /**
+ * <pre>
+ * Γ, φ |- Δ
+ * ------------------- if x is not free in the resulting sequent
+ * Γ, ∃x φ|- Δ
+ *
+ * </pre>
+ */
+ case class LeftExists(bot: Sequent, t1: Int, phi: Formula, x: VariableLabel) extends SCProofStep{val premises = Seq(t1)}
+ /**
+ * <pre>
+ * Γ, ∃y.∀x. (x=y) ↔ φ |- Δ
+ * ---------------------------- if y is not free in φ
+ * Γ, ∃!x. φ |- Δ
+ * </pre>
+ */
+ case class LeftExistsOne(bot: Sequent, t1: Int, phi: Formula, x: VariableLabel) extends SCProofStep{val premises = Seq(t1)}
+
+
+ // Right rules
+ /**
+ * <pre>
+ * Γ |- φ, Δ Σ |- ψ, Π ...
+ * ------------------------------------
+ * Γ, Σ |- φ∧ψ∧..., Π, Δ
+ * </pre>
+ */
+ case class RightAnd(bot: Sequent, t:Seq[Int], cunjuncts:Seq[Formula]) extends SCProofStep{val premises = t}
+ /**
+ * <pre>
+ * Γ |- φ, Δ Γ |- φ, ψ, Δ
+ * -------------- or ---------------
+ * Γ |- φ∨ψ, Δ Γ |- φ∨ψ, Δ
+ * </pre>
+ */
+ case class RightOr(bot: Sequent, t1: Int, phi: Formula, psi: Formula) extends SCProofStep{val premises = Seq(t1)}
+ /**
+ * <pre>
+ * Γ, φ |- ψ, Δ
+ * --------------
+ * Γ |- φ→ψ, Δ
+ * </pre>
+ */
+ case class RightImplies(bot: Sequent, t1: Int, phi: Formula, psi: Formula) extends SCProofStep{val premises = Seq(t1)}
+ /**
+ * <pre>
+ * Γ |- a→ψ, Δ Σ |- ψ→φ, Π
+ * ----------------------------
+ * Γ, Σ |- φ↔ψ, Π, Δ
+ * </pre>
+ */
+ case class RightIff(bot: Sequent, t1: Int, t2: Int, phi: Formula, psi: Formula) extends SCProofStep{val premises = Seq(t1, t2)}
+ /**
+ * <pre>
+ * Γ, φ |- Δ
+ * --------------
+ * Γ |- ¬φ, Δ
+ * </pre>
+ */
+ case class RightNot(bot: Sequent, t1: Int, phi: Formula) extends SCProofStep{val premises = Seq(t1)}
+ /**
+ * <pre>
+ * Γ |- φ, Δ
+ * ------------------- if x is not free in the resulting sequent
+ * Γ |- ∀x. φ, Δ
+ * </pre>
+ */
+ case class RightForall(bot: Sequent, t1: Int, phi: Formula, x: VariableLabel) extends SCProofStep{val premises = Seq(t1)}
+ /**
+ * <pre>
+ * Γ |- φ[t/x], Δ
+ * -------------------
+ * Γ |- ∃x. φ, Δ
+ *
+ * (ln-x stands for locally nameless x)
+ * </pre>
+ */
+ case class RightExists(bot: Sequent, t1: Int, phi: Formula, x: VariableLabel, t: Term) extends SCProofStep{val premises = Seq(t1)}
+ /**
+ * <pre>
+ * Γ |- ∃y.∀x. (x=y) ↔ φ, Δ
+ * ---------------------------- if y is not free in φ
+ * Γ|- ∃!x. φ, Δ
+ * </pre>
+ */
+ case class RightExistsOne(bot: Sequent, t1: Int, phi: Formula, x: VariableLabel) extends SCProofStep{val premises = Seq(t1)}
+
+ // Structural rules
+ /**
+ * <pre>
+ * Γ |- Δ
+ * --------------
+ * Γ, Σ |- Δ, Π
+ * </pre>
+ */
+ case class Weakening(bot: Sequent, t1: Int) extends SCProofStep{val premises = Seq(t1)}
+
+
+ // Equality Rules
+ /**
+ * <pre>
+ * Γ, s=s |- Δ
+ * --------------
+ * Γ |- Δ
+ * </pre>
+ */
+ case class LeftRefl(bot: Sequent, t1: Int, fa: Formula) extends SCProofStep{val premises = Seq(t1)}
+ /**
+ * <pre>
+ *
+ * --------------
+ * |- s=s
+ * </pre>
+ */
+ case class RightRefl(bot: Sequent, fa: Formula) extends SCProofStep{val premises = Seq()}
+ /**
+ * <pre>
+ * Γ, φ[s/?f] |- Δ
+ * ---------------------
+ * Γ, s=t, φ[t/?f ] |- Δ
+ * </pre>
+ */
+ case class LeftSubstEq(bot: Sequent, t1: Int, s: Term, t: Term, phi: Formula, f: SchematicFunctionLabel) extends SCProofStep{val premises = Seq(t1)}
+ /**
+ * <pre>
+ * Γ |- φ[s/?f], Δ
+ * ---------------------
+ * Γ, s=t |- φ[t/?f], Δ
+ * </pre>
+ */
+ case class RightSubstEq(bot: Sequent, t1: Int, s: Term, t: Term, phi: Formula, f: SchematicFunctionLabel) extends SCProofStep{val premises = Seq(t1)}
+ /**
+ * <pre>
+ * Γ, φ[a/h] |- Δ
+ * ---------------------
+ * Γ, a↔b, φ[b/h] |- Δ
+ * </pre>
+ */
+ case class LeftSubstIff(bot: Sequent, t1: Int, fa: Formula, fb: Formula, phi: Formula, h: SchematicPredicateLabel) extends SCProofStep{val premises = Seq(t1)}
+ /**
+ * <pre>
+ * Γ |- φ[a/h], Δ
+ * ---------------------
+ * Γ, a↔b |- φ[b/h], Δ
+ * </pre>
+ */
+ case class RightSubstIff(bot: Sequent, t1: Int, fa: Formula, fb: Formula, phi: Formula, h: SchematicPredicateLabel) extends SCProofStep{val premises = Seq(t1)}
+
+ // Proof Organisation rules
+ case class SCSubproof(sp: SCProof, premises: Seq[Int] = Seq.empty, display:Boolean = true) extends SCProofStep {
+ // premises is a list of ints similar to t1, t2... that verifies that imports of the subproof sp are justified by previous steps.
+ val bot: Sequent = sp.conclusion
+ }
+
+}
diff --git a/src/main/scala/lisa/settheory/AxiomaticSetTheory.scala b/src/main/scala/lisa/settheory/AxiomaticSetTheory.scala
new file mode 100644
index 0000000000000000000000000000000000000000..377d64b6d8611607f7c4d1382774feb1f6c12247
--- /dev/null
+++ b/src/main/scala/lisa/settheory/AxiomaticSetTheory.scala
@@ -0,0 +1,8 @@
+package lisa.settheory
+
+import lisa.kernel.proof.SCProofChecker
+
+object AxiomaticSetTheory extends SetTheoryTGAxioms {
+
+
+}
\ No newline at end of file
diff --git a/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala b/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bf8b7bf4fe62efa8c0a0c9fe281d9e348593b34d
--- /dev/null
+++ b/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
@@ -0,0 +1,39 @@
+package lisa.settheory
+
+import lisa.kernel.fol.FOL._
+import lisa.kernel.proof.RunningTheory
+import lisa.KernelHelpers.{given, _}
+/**
+ * Base trait for set theoretical axiom systems.
+ * Defines the symbols used in set theory.
+ */
+private[settheory] trait SetTheoryDefinitions{
+ type Axiom = Formula
+ def axioms: Set[Axiom] = Set.empty
+ private[settheory] final val (x, y, z, a, b) =
+ (VariableLabel("x"), VariableLabel("y"), VariableLabel("z"), VariableLabel("A"), VariableLabel("B"))
+ private[settheory] final val sPhi = SchematicPredicateLabel("P", 2)
+ private[settheory] final val sPsi = SchematicPredicateLabel("P", 3)
+ // Predicates
+ final val in: PredicateLabel = ConstantPredicateLabel("set_membership", 2)
+ final val subset: PredicateLabel = ConstantPredicateLabel("subset_of", 2)
+ final val sim: PredicateLabel = ConstantPredicateLabel("same_cardinality", 2) // Equicardinality
+ final val predicates = Set(in, subset, sim)
+ // val application
+ // val pick
+
+ // Functions
+ final val emptySet: FunctionLabel = ConstantFunctionLabel("empty_set", 0)
+ final val pair: FunctionLabel = ConstantFunctionLabel("unordered_pair", 2)
+ final val singleton: FunctionLabel = ConstantFunctionLabel("singleton", 1)
+ final val powerSet: FunctionLabel = ConstantFunctionLabel("power_set", 1)
+ final val union: FunctionLabel = ConstantFunctionLabel("union", 1)
+ final val universe: FunctionLabel = ConstantFunctionLabel("universe", 1)
+ final val functions = Set(emptySet, pair, singleton, powerSet, union, universe)
+
+ val runningSetTheory:RunningTheory = new RunningTheory()
+ given RunningTheory = runningSetTheory
+
+ predicates.foreach(s => runningSetTheory.addSymbol(s))
+ functions.foreach(s => runningSetTheory.addSymbol(s))
+}
\ No newline at end of file
diff --git a/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala b/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c1a92a892a5097b1dac2357d11123da93acff40d
--- /dev/null
+++ b/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
@@ -0,0 +1,19 @@
+package lisa.settheory
+import lisa.kernel.fol.FOL._
+import lisa.KernelHelpers.{given, _}
+/**
+ * Axioms for the Tarski-Grothendieck theory (TG)
+ */
+private[settheory] trait SetTheoryTGAxioms extends SetTheoryZFAxioms {
+
+ final val tarskiAxiom: Axiom = forall(x, in(x, universe(x)) /\
+ forall(y, in(y, universe(x)) ==> (in(powerSet(y), universe(x)) /\ subset(powerSet(y), universe(x))) /\
+ forall(z, subset(z, universe(x)) ==> (sim(y, universe(x)) /\ in(y, universe(x))))
+ )
+ )
+
+ runningSetTheory.addAxiom(tarskiAxiom)
+
+ override def axioms: Set[Axiom] = super.axioms + tarskiAxiom
+
+}
\ No newline at end of file
diff --git a/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala b/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
new file mode 100644
index 0000000000000000000000000000000000000000..da30c8780d16dbeaf9dbf1acb94464a29aff1bc2
--- /dev/null
+++ b/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
@@ -0,0 +1,29 @@
+package lisa.settheory
+
+import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.RunningTheory
+import lisa.KernelHelpers.{given, _}
+/**
+ * Axioms for the Zermelo theory (Z)
+ */
+private[settheory] trait SetTheoryZAxioms extends SetTheoryDefinitions {
+
+ final val emptySetAxiom: Axiom = forall(x, !in(x, emptySet()))
+ final val extensionalityAxiom: Axiom = forall(x, forall(y, forall(z, in(z, x) <=> in(z, y)) <=> (x === y)))
+ final val pairAxiom: Axiom = forall(x, forall(y, forall(z, in(z, pair(x, y)) <=> (x === z) \/ (y === z))))
+ final val unionAxiom: Axiom = forall(x, forall(z, in(x, union(z)) <=> exists(y, in(x, y) /\ in(y, z))))
+ final val powerAxiom: Axiom = forall(x, forall(y, in(x, powerSet(y)) <=> subset(x, y)))
+ final val foundationAxiom: Axiom = forall(x, !(x === emptySet()) ==> exists(y, in(y, x) /\ forall(z, in(z, x) ==> !in(z, y))))
+
+
+ final val comprehensionSchema: Axiom = forall(z, exists(y, forall(x, in(x,y) <=> (in(x,y) /\ sPhi(x,z)))))
+
+ private val zAxioms: Set[Axiom] = Set(emptySetAxiom, extensionalityAxiom, pairAxiom, unionAxiom, powerAxiom, foundationAxiom)
+
+
+
+ zAxioms.foreach(a => runningSetTheory.addAxiom(a))
+
+ override def axioms: Set[Axiom] = super.axioms ++ zAxioms
+
+}
\ No newline at end of file
diff --git a/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala b/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2b77f013d58533e80f783d7dc4dd6bce6250653e
--- /dev/null
+++ b/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
@@ -0,0 +1,16 @@
+package lisa.settheory
+
+import lisa.kernel.fol.FOL._
+import lisa.KernelHelpers.{given, _}
+/**
+ * Axioms for the Zermelo-Fraenkel theory (ZF)
+ */
+private[settheory] trait SetTheoryZFAxioms extends SetTheoryZAxioms {
+
+ final val replacementSchema: Axiom = forall(a,
+ forall(x, (in(x, a)) ==> existsOne(y, sPsi(a,x,y))) ==>
+ exists(b, forall(x, in(x, a) ==> exists(y, in(y, b) /\ sPsi(a,x,y))))
+ )
+
+
+}
\ No newline at end of file
diff --git a/src/main/scala/proven/ElementsOfSetTheory.scala b/src/main/scala/proven/ElementsOfSetTheory.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a1bf44ded463ff24e926edbab8169cf12ee40eae
--- /dev/null
+++ b/src/main/scala/proven/ElementsOfSetTheory.scala
@@ -0,0 +1,346 @@
+package proven
+import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.SequentCalculus.*
+import lisa.KernelHelpers.{*, given}
+import proven.tactics.ProofTactics.*
+import proven.tactics.Destructors.*
+import lisa.settheory.AxiomaticSetTheory.*
+import scala.collection.immutable.SortedSet
+import lisa.kernel.proof.SCProof
+
+import scala.collection.immutable
+
+/**
+ * Some proofs in set theory. See it as a proof of concept.
+ */
+object ElementsOfSetTheory {
+
+ private val x = VariableLabel("x")
+ private val y = VariableLabel("y")
+ private val x1 = VariableLabel("x'")
+ private val y1 = VariableLabel("y'")
+ private val z = VariableLabel("z")
+ private val g = SchematicFunctionLabel("g", 0)
+ private val h = SchematicPredicateLabel("h", 0)
+
+ val oPair: FunctionLabel = ConstantFunctionLabel("ordered_pair", 2)
+ val oPairFirstElement: FunctionLabel = ConstantFunctionLabel("ordered_pair_first_element", 1)
+ val oPairSecondElement: FunctionLabel = ConstantFunctionLabel("ordered_pair_second_element", 1)
+
+ val proofUnorderedPairSymmetry: SCProof = {
+ val imps: IndexedSeq[Sequent] = IndexedSeq(() |- extensionalityAxiom, () |- pairAxiom)
+ val s0 = Rewrite(() |- extensionalityAxiom, -1)
+ val pairExt1 = instantiateForall(new SCProof(IndexedSeq(s0), imps), extensionalityAxiom, pair(x, y))
+ val pairExt2 = instantiateForall(pairExt1, pairExt1.conclusion.right.head, pair(y, x))
+ val t0 = Rewrite(() |- pairAxiom, -2)
+ val pairSame11 = instantiateForall(new SCProof(IndexedSeq(t0), imps), pairAxiom, x)
+ val pairSame12 = instantiateForall(pairSame11, pairSame11.conclusion.right.head, y)
+ val pairSame13 = instantiateForall(pairSame12, pairSame12.conclusion.right.head, z)
+
+ val pairSame21 = instantiateForall(new SCProof(IndexedSeq(t0), imps), pairAxiom, y)
+ val pairSame22 = instantiateForall(pairSame21, pairSame21.conclusion.right.head, x)
+ val pairSame23 = instantiateForall(pairSame22, pairSame22.conclusion.right.head, z)
+ val condsymor = ((y === z) \/ (x === z)) <=> ((x === z) \/ (y === z))
+ val pairSame24 = pairSame23 // + st1
+
+ val pr0 = SCSubproof(pairSame13, Seq(-1, -2))
+ val pr1 = SCSubproof(pairSame23, Seq(-1, -2))
+ val pr2 = RightSubstIff(Sequent(pr1.bot.right, Set(in(z, pair(x, y)) <=> in(z, pair(y, x)))), 0,
+ (x === z) \/ (y === z),
+ in(z, pair(y, x)),
+ in(z, pair(x, y)) <=> h(),
+ h)
+ val pr3 = Cut(Sequent(pr1.bot.left, pr2.bot.right), 1, 2, pr2.bot.left.head)
+ //val pr4 = LeftAxiom(Sequent(Set(), pr2.bot.right), 3, pr1.bot.left.head, "")
+ val pr4 = RightForall(Sequent(Set(), Set(forall(z, pr2.bot.right.head))), 3, pr2.bot.right.head, z)
+ val fin = SCProof(IndexedSeq(pr0, pr1, pr2, pr3, pr4), imps)
+ val fin2 = byEquiv(pairExt2.conclusion.right.head, fin.conclusion.right.head)(SCSubproof(pairExt2, Seq(-1, -2)), SCSubproof(fin, Seq(-1, -2)))
+ val fin3 = generalizeToForall(fin2, fin2.conclusion.right.head, x)
+ val fin4 = generalizeToForall(fin3, fin3.conclusion.right.head, y)
+ fin4.copy(imports = imps)
+ } // |- ∀∀({x$1,y$2}={y$2,x$1})
+
+ val proofUnorderedPairDeconstruction: SCProof = {
+ val pxy = pair(x, y)
+ val pxy1 = pair(x1, y1)
+ val zexy = (z === x) \/ (z === y)
+ val p0 = SCSubproof {
+ val p0 = SCSubproof({
+ val zf = in(z, pxy)
+ val p1_0 = hypothesis(zf)
+ val p1_1 = RightImplies(emptySeq +> (zf ==> zf), 0, zf, zf)
+ val p1_2 = RightIff(emptySeq +> (zf <=> zf), 1, 1, zf, zf) // |- (z in {x,y} <=> z in {x,y})
+ val p1_3 = RightSubstEq(emptySeq +< (pxy === pxy1) +> (zf <=> in(z, pxy1)), 2, pxy, pxy1, zf <=> in(z, g()), g)
+ SCProof(p1_0, p1_1, p1_2, p1_3)
+ }, display = false) // ({x,y}={x',y'}) |- ((z∈{x,y})↔(z∈{x',y'}))
+ val p1 = SCSubproof({
+ val p1_0 = Rewrite(()|-pairAxiom, -1) // |- ∀∀∀((z$1∈{x$3,y$2})↔((x$3=z$1)∨(y$2=z$1)))
+ val p1_1 = instantiateForall(SCProof(IndexedSeq(p1_0), IndexedSeq(()|-pairAxiom)), x, y, z)
+ p1_1
+ }, display = false) // |- (z in {x,y}) <=> (z=x \/ z=y)
+ val p2 = SCSubproof({
+ val p2_0 = Rewrite(()|-pairAxiom, -1) // |- ∀∀∀((z$1∈{x$3,y$2})↔((x$3=z$1)∨(y$2=z$1)))
+ val p2_1 = instantiateForall(SCProof(IndexedSeq(p2_0), IndexedSeq(()|-pairAxiom)), x1, y1, z)
+ p2_1
+ }, display = false) // |- (z in {x',y'}) <=> (z=x' \/ z=y')
+ val p3 = RightSubstEq(
+ emptySeq +< (pxy === pxy1) +> (in(z, pxy1) <=> ((z === x) \/ (z === y))), 1, pxy, pxy1, in(z, g()) <=> ((z === x) \/ (z === y)), g
+ ) // ({x,y}={x',y'}) |- ((z∈{x',y'})↔((z=x)∨(z=y)))
+ val p4 = RightSubstIff(
+ emptySeq +< p3.bot.left.head +< p2.bot.right.head +> (((z === x) \/ (z === y)) <=> ((z === x1) \/ (z === y1))),
+ 3,
+ (z === x1) \/ (z === y1),
+ in(z, pxy1),
+ h() <=> ((z === x) \/ (z === y)),
+ h
+ ) // ((z∈{x',y'})↔((x'=z)∨(y'=z))), ({x,y}={x',y'}) |- (((z=x)∨(z=y))↔((z=x')∨(z=y')))
+ val p5 = Cut(emptySeq ++< p3.bot ++> p4.bot, 2, 4, p2.bot.right.head)
+ SCProof(p0, p1, p2, p3, p4, p5)
+ } // ({x,y}={x',y'}) |- (((z=x)∨(z=y))↔((z=x')∨(z=y')))
+
+ val p1 = SCSubproof(
+ SCProof(byCase(x === x1)(
+ SCSubproof({
+ val pcm1 = p0
+ val pc0 = SCSubproof(SCProof(byCase(y === x)(
+ SCSubproof({
+ val pam1 = pcm1
+ val pa0 = SCSubproof({
+ val f1 = z === x
+ val pa0_m1 = pcm1 // ({x,y}={x',y'}) |- (((z=x)∨(z=y))↔((z=x')∨(z=y')))
+ val pa0_0 = SCSubproof({
+ val pa0_0_0 = hypothesis(f1)
+ val pa0_1_1 = RightOr(emptySeq +< f1 +> (f1 \/ f1), 0, f1, f1)
+ val pa0_1_2 = RightImplies(emptySeq +> (f1 ==> (f1 \/ f1)), 1, f1, f1 \/ f1)
+ val pa0_1_3 = LeftOr(emptySeq +< (f1 \/ f1) +> f1, Seq(0,0), Seq(f1, f1))
+ val pa0_1_4 = RightImplies(emptySeq +> ((f1 \/ f1) ==> f1), 3, f1 \/ f1, f1)
+ val pa0_1_5 = RightIff(emptySeq +> ((f1 \/ f1) <=> f1), 2, 4, (f1 \/ f1), f1)
+ val r = SCProof(pa0_0_0, pa0_1_1, pa0_1_2, pa0_1_3, pa0_1_4, pa0_1_5)
+ r
+ }, display = false) // |- (((z=x)∨(z=x))↔(z=x))
+ val pa0_1 = RightSubstEq(emptySeq +< (pxy === pxy1) +< (x === y) +> ((f1 \/ f1) <=> (z === x1) \/ (z === y1)), -1, x, y, (f1 \/ (z === g())) <=> ((z === x1) \/ (z === y1)), g) // ({x,y}={x',y'}) y=x|- (z=x)\/(z=x) <=> (z=x' \/ z=y')
+ val pa0_2 = RightSubstIff(emptySeq +< (pxy === pxy1) +< (x === y) +< (f1 <=> (f1 \/ f1)) +> (f1 <=> ((z === x1) \/ (z === y1))), 1, f1, f1 \/ f1, h() <=> ((z === x1) \/ (z === y1)), h)
+ val pa0_3 = Cut(emptySeq +< (pxy === pxy1) +< (x === y) +> (f1 <=> ((z === x1) \/ (z === y1))), 0, 2, f1 <=> (f1 \/ f1)) // (x=y), ({x,y}={x',y'}) |- ((z=x)↔((z=x')∨(z=y')))
+ val pa0_4 = RightForall(emptySeq +< (pxy === pxy1) +< (x === y) +> forall(z, f1 <=> ((z === x1) \/ (z === y1))), 3, f1 <=> ((z === x1) \/ (z === y1)), z)
+ val ra0_0 = instantiateForall(SCProof(IndexedSeq(pa0_0, pa0_1, pa0_2, pa0_3, pa0_4), IndexedSeq(pa0_m1.bot)), y1) // (x=y), ({x,y}={x',y'}) |- ((y'=x)↔((y'=x')∨(y'=y')))
+ ra0_0
+ }, IndexedSeq(-1)) // ({x,y}={x',y'}) y=x|- ((y'=x)↔((y'=x')∨(y'=y')))
+ val pa1 = SCSubproof({
+ val pa1_0 = RightRefl(emptySeq +> (y1 === y1), y1 === y1)
+ val pa1_1 = RightOr(emptySeq +> ((y1 === y1) \/ (y1 === x1)), 0, y1 === y1, y1 === x1)
+ SCProof(pa1_0, pa1_1)
+ }, display = false) // |- (y'=x' \/ y'=y')
+ val ra3 = byEquiv(pa0.bot.right.head, pa1.bot.right.head)(pa0, pa1) // ({x,y}={x',y'}) y=x|- ((y'=x)
+ val pal = RightSubstEq(emptySeq ++< pa0.bot +> (y1 === y), ra3.length - 1, x, y, y1 === g(), g)
+ SCProof(ra3.steps, IndexedSeq(pam1.bot)) appended pal // (x=y), ({x,y}={x',y'}) |- (y'=y)
+ }, IndexedSeq(-1)) // (x=y), ({x,y}={x',y'}) |- (y'=y)
+ ,
+ SCSubproof({
+ val pbm1 = pcm1 // ({x,y}={x',y'}) |- (((z=x)∨(z=y))↔((z=x')∨(z=y')))
+ val pb0_0 = SCSubproof({
+ val pb0_0 = RightForall(emptySeq ++< pcm1.bot +> forall(z, pcm1.bot.right.head), -1, pcm1.bot.right.head, z)
+ instantiateForall(SCProof(IndexedSeq(pb0_0), IndexedSeq(pcm1.bot)), y)
+ }, IndexedSeq(-1)) // ({x,y}={x',y'}) |- (((y=x)∨(y=y))↔((y=x')∨(y=y')))
+ val pb0_1 = SCSubproof({
+ val pa1_0 = RightRefl(emptySeq +> (y === y), y === y)
+ val pa1_1 = RightOr(emptySeq +> ((y === y) \/ (y === x)), 0, y === y, y === x)
+ SCProof(pa1_0, pa1_1)
+ }, display = false) // |- (y=x)∨(y=y)
+ val rb0 = byEquiv(pb0_0.bot.right.head, pb0_1.bot.right.head)(pb0_0, pb0_1) // ({x,y}={x',y'}) |- (y=x')∨(y=y')
+ val pb1 = RightSubstEq(emptySeq ++< rb0.conclusion +< (x === x1) +> ((y === x) \/ (y === y1)), rb0.length - 1, x, x1, (y === g()) \/ (y === y1), g)
+ val rb1 = destructRightOr(
+ rb0 appended pb1, // ({x,y}={x',y'}) , x=x'|- (y=x)∨(y=y')
+ y === x, y === y1
+ )
+ val rb2 = rb1 appended LeftNot(rb1.conclusion +< !(y === x) -> (y === x), rb1.length - 1, y === x) // (x=x'), ({x,y}={x',y'}), ¬(y=x) |- (y=y')
+ SCProof(rb2.steps, IndexedSeq(pbm1.bot))
+
+ }, IndexedSeq(-1)) // ({x,y}={x',y'}), x=x', !y=x |- y=y'
+ ).steps, IndexedSeq(pcm1.bot)), IndexedSeq(-1)) // (x=x'), ({x,y}={x',y'}) |- (y'=y)
+ val pc1 = RightRefl(emptySeq +> (x === x), x === x)
+ val pc2 = RightAnd(emptySeq ++< pc0.bot +> ((y1 === y) /\ (x === x)), Seq(0, 1), Seq(y1 === y, x === x)) // ({x,y}={x',y'}), x=x' |- (x=x /\ y=y')
+ val pc3 = RightSubstEq(emptySeq ++< pc2.bot +> ((y1 === y) /\ (x1 === x)), 2, x, x1, (y1 === y) /\ (g() === x), g) // ({x,y}={x',y'}), x=x' |- (x=x' /\ y=y')
+ val pc4 = RightOr(emptySeq ++< pc3.bot +> (pc3.bot.right.head \/ ((x === y1) /\ (y === x1))), 3, pc3.bot.right.head, (x === y1) /\ (y === x1)) // ({x,y}={x',y'}), x=x' |- (x=x' /\ y=y')\/(x=y' /\ y=x')
+ val r = SCProof(IndexedSeq(pc0, pc1, pc2, pc3, pc4), IndexedSeq(pcm1.bot))
+ r
+ }, IndexedSeq(-1)) // ({x,y}={x',y'}), x=x' |- (x=x' /\ y=y')\/(x=y' /\ y=x')
+ ,
+ SCSubproof({
+ val pdm1 = p0
+ val pd0 = SCSubproof({
+ val pd0_m1 = pdm1
+ val pd0_0 = SCSubproof {
+ val ex1x1 = x1 === x1
+ val pd0_0_0 = RightRefl(emptySeq +> ex1x1, ex1x1) // |- x'=x'
+ val pd0_0_1 = RightOr(emptySeq +> (ex1x1 \/ (x1 === y1)), 0, ex1x1, x1 === y1) // |- (x'=x' \/ x'=y')
+ SCProof(IndexedSeq(pd0_0_0, pd0_0_1))
+ } // |- (x'=x' \/ x'=y')
+ val pd0_1 = SCSubproof({
+ val pd0_1_m1 = pd0_m1 // ({x,y}={x',y'}) |- (((z=x)∨(z=y))↔((z=x')∨(z=y')))
+ val pd0_1_0 = RightForall(emptySeq ++< pd0_1_m1.bot +> forall(z, pd0_1_m1.bot.right.head), -1, pd0_1_m1.bot.right.head, z)
+ val rd0_1_1 = instantiateForall(SCProof(IndexedSeq(pd0_1_0), IndexedSeq(pd0_m1.bot)), x1) // ({x,y}={x',y'}) |- (x'=x \/ x'=y) <=> (x'=x' \/ x'=y')
+ rd0_1_1
+ }, IndexedSeq(-1)) // ({x,y}={x',y'}) |- (x'=x \/ x'=y) <=> (x'=x' \/ x'=y')
+ val rd0_2 = byEquiv(pd0_1.bot.right.head, pd0_0.bot.right.head)(pd0_1, pd0_0)
+ val pd0_3 = SCSubproof(SCProof(rd0_2.steps, IndexedSeq(pd0_m1.bot)), IndexedSeq(-1)) // ({x,y}={x',y'}) |- (x=x' \/ y=x')
+ destructRightOr(SCProof(IndexedSeq(pd0_0, pd0_1, pd0_3), IndexedSeq(pd0_m1.bot)), x === x1, y === x1) // ({x,y}={x',y'}) |- x=x', y=x'
+ }, IndexedSeq(-1)) // ({x,y}={x',y'}) |- x=x', y=x' --
+ val pd1 = SCSubproof({
+ val pd1_m1 = pdm1
+ val pd1_0 = SCSubproof {
+ val exx = x === x
+ val pd1_0_0 = RightRefl(emptySeq +> exx, exx) // |- x=x
+ val pd1_0_1 = RightOr(emptySeq +> (exx \/ (x === y)), 0, exx, x === y) // |- (x=x \/ x=y)
+ SCProof(IndexedSeq(pd1_0_0, pd1_0_1))
+ } // |- (x=x \/ x=y)
+ val pd1_1 = SCSubproof({
+ val pd1_1_m1 = pd1_m1 // ({x,y}={x',y'}) |- (((z=x)∨(z=y))↔((z=x')∨(z=y')))
+ val pd1_1_0 = RightForall(emptySeq ++< pd1_1_m1.bot +> forall(z, pd1_1_m1.bot.right.head), -1, pd1_1_m1.bot.right.head, z)
+ val rd1_1_1 = instantiateForall(SCProof(IndexedSeq(pd1_1_0), IndexedSeq(pd1_m1.bot)), x) // ({x,y}={x',y'}) |- (x=x \/ x=y) <=> (x=x' \/ x=y')
+ rd1_1_1
+ }, IndexedSeq(-1)) // // ({x,y}={x',y'}) |- (x=x \/ x=y) <=> (x=x' \/ x=y')
+ val rd1_2 = byEquiv(pd1_1.bot.right.head, pd1_0.bot.right.head)(pd1_1, pd1_0)
+ val pd1_3 = SCSubproof(SCProof(rd1_2.steps, IndexedSeq(pd1_m1.bot)), IndexedSeq(-1)) // // ({x,y}={x',y'}) |- x=x' \/ x=y'
+ destructRightOr(SCProof(IndexedSeq(pd1_0, pd1_1, pd1_3), IndexedSeq(pd1_m1.bot)), x === x1, x === y1) // ({x,y}={x',y'}) |- x=x', x=y'
+ }, IndexedSeq(-1))// ({x,y}={x',y'}) |- x=x', x=y' --
+ val pd2 = RightAnd(emptySeq ++< pd1.bot +> (x === x1) +> ((x === y1) /\ (y === x1)), Seq(0, 1), Seq(x === y1, y === x1)) // ({x,y}={x',y'}) |- x=x', (x=y' /\ y=x') ---
+ val pd3 = LeftNot(emptySeq ++< pd2.bot +< !(x === x1) +> ((x === y1) /\ (y === x1)), 2, x === x1) // ({x,y}={x',y'}), !x===x1 |- (x=y' /\ y=x')
+ val pd4 = RightOr(emptySeq ++< pd3.bot +> (pd3.bot.right.head \/ ((x === x1) /\ (y === y1))), 3, pd3.bot.right.head, (x === x1) /\ (y === y1)) // ({x,y}={x',y'}), !x===x1 |- (x=x' /\ y=y')\/(x=y' /\ y=x')
+ SCProof(IndexedSeq(pd0, pd1, pd2, pd3, pd4), IndexedSeq(pdm1.bot))
+ }, IndexedSeq(-1)) // ({x,y}={x',y'}), !x=x' |- (x=x' /\ y=y')\/(x=y' /\ y=x')
+ ).steps, IndexedSeq(p0.bot)
+ ), IndexedSeq(0)
+ ) // ({x,y}={x',y'}) |- (x=x' /\ y=y')\/(x=y' /\ y=x')
+
+ val p2 = RightImplies(emptySeq +> (p1.bot.left.head ==> p1.bot.right.head), 1, p1.bot.left.head, p1.bot.right.head) // |- ({x,y}={x',y'}) ==> (x=x' /\ y=y')\/(x=y' /\ y=x')
+ generalizeToForall(SCProof(p0, p1, p2), x, y, x1, y1)
+ } // |- ∀∀∀∀(({x$4,y$3}={x'$2,y'$1})⇒(((y'$1=y$3)∧(x'$2=x$4))∨((x$4=y'$1)∧(y$3=x'$2))))
+
+
+ // i2, i1, p0, p1, p2, p3
+
+ val orderedPairDefinition: SCProof = simpleFunctionDefinition(oPair, pair(pair(x, y), pair(x, x)), Seq(x, y))
+
+/*
+ val proofOrderedPairDeconstruction: SCProof = {
+
+ val opairxy = pair(pair(x, y), pair(x, x))
+ val opairxx = pair(pair(x, x), pair(x, x))
+ val opairxy1 = pair(pair(x1, y1), pair(x1, x1))
+ val opairxx1 = pair(pair(x1, x1), pair(x1, x1))
+ val pairxy = pair(x, y)
+ val pairxx = pair(x, x)
+ val pairxy1 = pair(x1, y1)
+ val pairxx1 = pair(x1, x1)
+
+
+ val p0 = SCSubproof(orderedPairDefinition, display = false)
+ val p1 = SCSubproof(proofUnorderedPairDeconstruction) // |- ∀∀∀∀(({x$4,y$3}={x'$2,y'$1})⇒(((y'$1=y$3)∧(x'$2=x$4))∨((x$4=y'$1)∧(y$3=x'$2))))
+
+ val p2: SCSubproof = SCSubproof(SCProof(byCase(x === y)(
+ {
+ val p2_0 = SCSubproof(SCProof({
+ val pa2_0 = SCSubproof({
+ val p2_0_0 = UseFunctionDefinition(emptySeq +> (oPair(x, y) === opairxy), oPair, Seq(x, y)) // |- (x, y) === {{x,y}, {x,x}}
+ val p2_0_1 = RightSubstEq(emptySeq +< (x === y) +> (oPair(x, y) === opairxx),
+ 0, x, y, oPair(x, y) === pair(pair(x, z), pair(x, x)), z) // (x=y) |- ((x,y)={{x,x},{x,x}})
+ val p2_0_2 = UseFunctionDefinition(emptySeq +> (oPair(x1, y1) === opairxy1), oPair, Seq(x1, y1)) // |- (x1, y1) === {{x1,y1}, {x1,x1}}
+ val p2_0_3 = RightSubstEq(emptySeq +< (oPair(x, y) === oPair(x1, y1)) +< (x === y) +> (oPair(x1, y1) === pair(pair(x, x), pair(x, x))),
+ 1, oPair(x, y), oPair(x1, y1), z === pair(pair(x, x), pair(x, x)), z) // (x=y), (x1,y1)=(x,y) |- ((x1,y1)={{x,x},{x,x}})
+ val p2_0_4 = RightSubstEq(emptySeq +< (oPair(x, y) === oPair(x1, y1)) +< (x === y) +< (opairxy1 === oPair(x1, y1)) +> (pair(pair(x, x), pair(x, x)) === pair(pair(x1, y1), pair(x1, x1))),
+ 3, opairxy1, oPair(x1, y1), z === pair(pair(x, x), pair(x, x)), z) // (x=y), (x1,y1)=(x,y), (x1,y1)={{x1,y1}, {x1,x1}} |- {{x1,y1}, {x1,x1}}={{x,x},{x,x}})
+ val p2_0_5 = Cut(emptySeq +< (oPair(x, y) === oPair(x1, y1)) +< (x === y) +> (pair(pair(x, x), pair(x, x)) === pair(pair(x1, y1), pair(x1, x1))),
+ 2, 4, opairxy1 === oPair(x1, y1))
+ SCProof(IndexedSeq(p2_0_0, p2_0_1, p2_0_2, p2_0_3, p2_0_4, p2_0_5), IndexedSeq(p0))
+ }, IndexedSeq(-1)) // ((x,y)=(x',y')), (x=y) |- ({{x,x},{x,x}}={{x',y'},{x',x'}})
+ val pa2_1 = SCSubproof({
+ instantiateForall(SCProof(IndexedSeq(), IndexedSeq(p1)), pairxx, pairxx, pairxy1, pairxx1)
+ }, IndexedSeq(-2)) // ({{x,x},{x,x}}={{x',y'},{x',x'}})⇒((({x',x'}={x,x})∧({x',y'}={x,x}))∨(({x,x}={x',x'})∧({x,x}={x',y'}))))
+ val pr2_0 = modusPonens(pa2_0.bot.right.head)(pa2_0, pa2_1) // ((x,y)=(x',y')), (x=y) |- ((({x',x'}={x,x})∧({x',y'}={x,x}))∨(({x,x}={x',x'})∧({x,x}={x',y'})))
+ val f = (pairxx === pairxx1) /\ (pairxx === pairxy1)
+ destructRightAnd(destructRightOr(pr2_0, f, f), pairxx === pairxy1, pairxx === pairxx1) // ((x,y)=(x',y')), (x=y) |- {x',y'}={x,x}
+ }.steps, IndexedSeq(p0, p1)), IndexedSeq(-1, -2)) // ((x,y)=(x',y')), (x=y) |- {x',y'}={x,x}
+ val p2_1 = SCSubproof({
+ val pr2_1_0 = instantiateForall(SCProof(IndexedSeq(), IndexedSeq(p1)), x, x, x1, y1) // (({x,x}={x',y'})⇒(((y'=x)∧(x'=x))∨((x=y')∧(x=x'))))
+ val f = (y1 === x) /\ (x1 === x)
+ val pr2_1_1 = destructRightImplies(pr2_1_0, pairxx === pairxy1, f \/ f) // (({x,x}={x',y'}) |- (((y'=x)∧(x'=x))∨((x=y')∧(x=x'))))
+ val pr2_1_2 = destructRightOr(pr2_1_1, f, f)
+ pr2_1_2
+ }, IndexedSeq(-2)) // {x',y'}={x,x}, x=y |- x=x' /\ x=y'
+ val p2_2 = Cut(emptySeq ++< p2_0.bot ++> p2_1.bot, 0, 1, p2_0.bot.right.head) // ((x,y)=(x',y')), x=y |- x=x' /\ x=y'
+ val p2_3 = RightSubstEq(emptySeq +< (oPair(x, y) === oPair(x1, y1)) +< (x === y) +> ((x === x1) /\ (y === y1)), 2, x, y, (x === x1) /\ (z === y1), z)
+
+ SCSubproof(SCProof(IndexedSeq(p2_0, p2_1, p2_2, p2_3), IndexedSeq(p0, p1)), IndexedSeq(-1, -2))
+ } // ((x,y)=(x',y')), x=y |- x=x' /\ y=y'
+ ,
+ {
+ val pa2_0: SCSubproof = SCSubproof({
+ val p2_0_0 = UseFunctionDefinition(emptySeq +> (oPair(x, y) === opairxy), oPair, Seq(x, y)) // |- (x, y) === {{x,y}, {x,x}}
+ val p2_0_1 = UseFunctionDefinition(emptySeq +> (oPair(x1, y1) === opairxy1), oPair, Seq(x1, y1)) // |- (x1, y1) === {{x1,y1}, {x1,x1}}
+ val p2_0_2 = RightSubstEq(emptySeq +< (oPair(x, y) === oPair(x1, y1)) +> (oPair(x1, y1) === pair(pair(x, y), pair(x, x))),
+ 0, oPair(x, y), oPair(x1, y1), z === pair(pair(x, y), pair(x, x)), z) // (x1,y1)=(x,y) |- ((x1,y1)={{x,y},{x,x}})
+
+ val p2_0_3 = RightSubstEq(emptySeq +< (oPair(x, y) === oPair(x1, y1)) +< (opairxy1 === oPair(x1, y1)) +> (pair(pair(x, y), pair(x, x)) === pair(pair(x1, y1), pair(x1, x1))),
+ 2, opairxy1, oPair(x1, y1), z === pair(pair(x, y), pair(x, x)), z) // (x1,y1)=(x,y), (x1,y1)={{x1,y1}, {x1,x1}} |- {{x1,y1}, {x1,x1}}={{x,y},{x,x}})
+
+ val p2_0_4 = Cut(emptySeq +< (oPair(x, y) === oPair(x1, y1)) +> (pair(pair(x, y), pair(x, x)) === pair(pair(x1, y1), pair(x1, x1))),
+ 1, 3, opairxy1 === oPair(x1, y1))
+ SCProof(IndexedSeq(p2_0_0, p2_0_1, p2_0_2, p2_0_3, p2_0_4), IndexedSeq(p0))
+ }, IndexedSeq(-1)) // ((x,y)=(x',y')) |- ({{x,y},{x,x}}={{x',y'},{x',x'}})
+ val pa2_1 = SCSubproof({
+ instantiateForall(SCProof(IndexedSeq(), IndexedSeq(p1)), pairxy, pairxx, pairxy1, pairxx1)
+ }, IndexedSeq(-2)) // ({{x,y},{x,x}}={{x',y'},{x',x'}}) => ((({x',x'}={x,y})∧({x',y'}={x,x}))∨(({x,x}={x',x'})∧({x,y}={x',y'})))
+ val pr2_0 = SCProof(modusPonens(pa2_0.bot.right.head)(pa2_0, pa2_1).steps, IndexedSeq(p0, p1)) // ((x,y)=(x',y')) |- (({x',x'}={x,y})∧({x',y'}={x,x}))∨(({x,x}={x',x'})∧({x,y}={x',y'}))
+ val (f, g) = pr2_0.conclusion.right.head match {
+ case BinaryConnectorFormula(`or`, l, r) => (l, r)
+ }
+ val pr2_1: SCProof = destructRightOr(pr2_0, f, g) // ((x,y)=(x',y')) |- (({x',x'}={x,y})∧({x',y'}={x,x})), (({x,x}={x',x'})∧({x,y}={x',y'}))
+
+ val pb2_0 = SCSubproof({
+ val prb2_0_0 = instantiateForall(SCProof(IndexedSeq(), IndexedSeq(p1)), x, y, x1, x1) // |- (({x,y}={x',x'}) ⇒ (((x'=y)∧(x'=x))∨((x=x')∧(y=x'))))
+ val f = (x1 === y) /\ (x1 === x)
+ val prb2_0_1 = destructRightImplies(prb2_0_0, pairxy === pairxx1, f \/ f) // (({x,y}={x',x'}) |- ((x'=y)∧(x'=x))∨((x=x')∧(y=x')))
+ val pb3_0_0 = SCSubproof(destructRightOr(prb2_0_1, f, f), IndexedSeq(-1)) // (({x,y}={x',x'}) |- (x'=y)∧(x'=x)
+ val pb3_0_1 = SCSubproof(destructRightAnd(SCProof(IndexedSeq(), IndexedSeq(pb3_0_0)), x1 === y, x1 === x), IndexedSeq(0)) // (({x,y}={x',x'}) |- x'=y
+ val pb3_0_2 = SCSubproof(destructRightAnd(SCProof(IndexedSeq(), IndexedSeq(pb3_0_0)), x1 === x, x1 === y), IndexedSeq(0)) // (({x,y}={x',x'}) |- x'=x
+ val pb3_0_3 = RightSubstEq(emptySeq +< (pairxy === pairxx1) +< (x1 === y) +> (y === x), 2, x1, y, z === x, z) // (({x,y}={x',x'}), x'=y |- y=x
+ val pb3_0_4 = Cut(emptySeq +< (pairxy === pairxx1) +> (y === x), 1, 3, x1 === y) // {x',x'}={x,y} |- x=y
+ SCProof(IndexedSeq(pb3_0_0, pb3_0_1, pb3_0_2, pb3_0_3, pb3_0_4), IndexedSeq(p1))
+ }, IndexedSeq(-2)) // {x',x'}={x,y} |- x=y
+ val pb2_1 = SCSubproof(destructRightAnd(pr2_1, pairxx1 === pairxy, pairxx === pairxy1), IndexedSeq(-1, -2)) // ((x,y)=(x',y')) |- (({x',x'}={x,y}), (({x,x}={x',x'})∧({x,y}={x',y'}))
+
+ val pb2_2 = Cut(pb2_1.bot -> pb2_0.bot.left.head +> (x === y), 1, 0, pb2_0.bot.left.head) // ((x,y)=(x',y')) |- x=y, (({x,x}={x',x'})∧({x,y}={x',y'}))
+ val pc2_0 = SCSubproof(SCProof(IndexedSeq(pb2_0, pb2_1, pb2_2), IndexedSeq(p0, p1)), IndexedSeq(-1, -2)) // ((x,y)=(x',y')) |- x=y, (({x,x}={x',x'})∧({x,y}={x',y'}))
+
+ val pc2_1 = SCSubproof({
+ val pc2_1_0 = SCSubproof(destructRightAnd(SCProof(IndexedSeq(), IndexedSeq(pc2_0)), pairxy === pairxy1, pairxx === pairxx1), IndexedSeq(-2)) // ((x,y)=(x',y')) |- x=y, {x,y}={x',y'}
+ val pc2_1_1 = SCSubproof(instantiateForall(SCProof(IndexedSeq(), IndexedSeq(p1)), x, y, x1, y1), IndexedSeq(-1)) // (({x,y}={x',y'})⇒(((y'=y)∧(x'=x))∨((x=y')∧(y=x'))))
+ val prc2_1_2 = modusPonens(pairxy === pairxy1)(pc2_1_0, pc2_1_1) // ((x,y)=(x',y')) |- x=y, (((y'=y)∧(x'=x))∨((x=y')∧(y=x'))))
+ val f = (y1 === y) /\ (x1 === x)
+ val g = (y1 === x) /\ (x1 === y)
+ val prc2_1_3 = destructRightOr(prc2_1_2, f, g) // ((x,y)=(x',y')) |- x=y, ((y'=x)∧(x'=y)), ((y=y')∧(x=x')))
+ val prc2_1_4 = destructRightAnd(prc2_1_3, x1 === y, y1 === x) // ((x,y)=(x',y')) |- x=y, (x'=y), ((y=y')∧(x=x')))
+ SCProof(prc2_1_4.steps, IndexedSeq(p1, pc2_0))
+ }, IndexedSeq(-2, 0)) // ((x,y)=(x',y')) |- x=y, (x'=y), ((y=y')∧(x=x')))
+ val pc2_2 = SCSubproof({
+ val pc2_2_0 = SCSubproof(destructRightAnd(SCProof(IndexedSeq(), IndexedSeq(pc2_0)), pairxx === pairxx1, pairxy === pairxy1), IndexedSeq(-2)) // ((x,y)=(x',y')) |- x=y, {x,x}={x',x'}
+ val pc2_2_1 = SCSubproof(instantiateForall(SCProof(IndexedSeq(), IndexedSeq(p1)), x, x, x1, x1), IndexedSeq(-1)) // (({x,x}={x',x'})⇒(((x'=x)∧(x'=x))∨((x=x')∧(x=x'))))
+ val prc2_2_2 = modusPonens(pairxx === pairxx1)(pc2_2_0, pc2_2_1) // ((x,y)=(x',y')) |- x=y, (((x'=x)∧(x'=x))∨((x=x')∧(x=x'))))
+ val f = (x === x1) /\ (x1 === x)
+ val prc2_2_3 = destructRightOr(prc2_2_2, f, f) // ((x,y)=(x',y')) |- x=y, ((x'=x)∧(x'=x))
+ val prc2_2_4 = destructRightAnd(prc2_2_3, x === x1, x === x1) // ((x,y)=(x',y')) |- x=y, x'=x
+ SCProof(prc2_2_4.steps, IndexedSeq(p1, pc2_0))
+ }, IndexedSeq(-2, 0)) // ((x,y)=(x',y')) |- x=y, x'=x
+
+ val pc2_3 = RightSubstEq(pc2_1.bot -> (x1 === y) +> (x === y) +< (x1 === x), 1, x, x1, z === y, z) // ((x,y)=(x',y')), x=x' |- x=y, ((y=y')∧(x=x')))
+ val pc2_4 = Cut(pc2_3.bot -< (x === x1), 2, 3, x === x1) // ((x,y)=(x',y')) |- x=y, ((y=y')∧(x=x')))
+ val pc2_5 = LeftNot(pc2_4.bot +< !(x === y) -> (x === y), 4, x === y) // ((x,y)=(x',y')), !x=y |- ((y=y')∧(x=x')))
+ SCSubproof(SCProof(IndexedSeq(pc2_0, pc2_1, pc2_2, pc2_3, pc2_4, pc2_5), IndexedSeq(p0, p1)), IndexedSeq(-1, -2))
+ } // ((x,y)=(x',y')), !x=y |- x=x' /\ y=y'
+ ).steps, IndexedSeq(p0, p1)), IndexedSeq(0, 1)) // ((x,y)=(x',y')) |- x=x' /\ y=y'
+ SCProof(p0, p1, p2)
+
+ ???
+ } // |- (x,y)=(x', y') ===> x=x' /\ y=y'
+*/
+}
diff --git a/src/main/scala/proven/tactics/Destructors.scala b/src/main/scala/proven/tactics/Destructors.scala
new file mode 100644
index 0000000000000000000000000000000000000000..12c080e88a76dbc8b29650611122900c1e9ca9ea
--- /dev/null
+++ b/src/main/scala/proven/tactics/Destructors.scala
@@ -0,0 +1,31 @@
+package proven.tactics
+
+import lisa.kernel.proof.SequentCalculus.*
+import lisa.kernel.fol.FOL.*
+import lisa.KernelHelpers.*
+import proven.tactics.ProofTactics.hypothesis
+import lisa.kernel.proof.SCProof
+
+object Destructors {
+ def destructRightOr(p: SCProof, a: Formula, b: Formula): SCProof = {
+ require(contains(p.conclusion.right, a \/ b))
+ val p0 = hypothesis(a)
+ val p1 = hypothesis(b)
+ val p2 = LeftOr(emptySeq +< (a \/ b) +> a +> b, Seq(p.length, p.length + 1), Seq(a, b))
+ val p3 = Cut(p.conclusion -> (a \/ b) +> a +> b, p.length - 1, p.length + 2, a \/ b)
+ p withNewSteps IndexedSeq(p0, p1, p2, p3)
+ }
+ def destructRightAnd(p: SCProof, f: Formula, g: Formula): SCProof = {
+ val p0 = hypothesis(f) // n
+ val p1 = LeftAnd(emptySeq +< (f /\ g) +> f, p.length, f, g) // n+1
+ val p2 = Cut(p.conclusion -> (f /\ g) +> f, p.length - 1, p.length + 1, f /\ g)
+ p withNewSteps IndexedSeq(p0, p1, p2)
+ }
+ def destructRightImplies(p: SCProof, f: Formula, g: Formula): SCProof = { // |- f=>g
+ val p0 = hypothesis(f) // f |- f
+ val p1 = hypothesis(g) // g |- g
+ val p2 = LeftImplies(emptySeq +< f +< (f ==> g) +> g, p.length, p.length + 1, f, g) // f, f=>g |- g
+ val p3 = Cut(p.conclusion -> (f ==> g) +< f +> g, p.length - 1, p.length + 2, f ==> g) // f|- g
+ p withNewSteps IndexedSeq(p0, p1, p2, p3)
+ }
+}
diff --git a/src/main/scala/proven/tactics/ProofTactics.scala b/src/main/scala/proven/tactics/ProofTactics.scala
new file mode 100644
index 0000000000000000000000000000000000000000..85c576fc716c2b8d25dcabfb14bb22f54eb81590
--- /dev/null
+++ b/src/main/scala/proven/tactics/ProofTactics.scala
@@ -0,0 +1,156 @@
+package proven.tactics
+
+import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.SequentCalculus.*
+import lisa.KernelHelpers.{*, given}
+import lisa.kernel.Printer.*
+
+import scala.collection.immutable.Set
+import lisa.kernel.proof.SCProof
+
+/**
+ * SCProof tactics are a set of strategies that help the user write proofs in a more expressive way
+ * by focusing on the final goal rather on the individual steps.
+ */
+object ProofTactics {
+
+ def hypothesis(f: Formula): SCProofStep = Hypothesis(emptySeq +< f +> f, f)
+
+ def instantiateForall(p: SCProof, phi: Formula, t: Term): SCProof = { // given a proof with a formula quantified with \forall on the right, extend the proof to the same formula with something instantiated instead.
+ require(p.conclusion.right.contains(phi))
+ phi match {
+ case b @ BinderFormula(Forall, _, _) =>
+ val c = p.conclusion
+ val tempVar = VariableLabel(freshId(b.freeVariables.map(_.id), "x"))
+ val in = instantiateBinder(b, t)
+ val p1 = Hypothesis(Sequent(Set(in), Set(in)), in)
+ val p2 = LeftForall(Sequent(Set(b), Set(in)), p.length, instantiateBinder(b, tempVar), tempVar, t)
+ val p3 = Cut(Sequent(c.left, c.right - phi + in), p.length - 1, p.length + 1, phi)
+ p withNewSteps IndexedSeq(p1, p2, p3)
+ case _ => throw new Exception("not a forall")
+ }
+ }
+ def instantiateForall(p: SCProof, phi: Formula, t: Term*): SCProof = { // given a proof with a formula quantified with \forall on the right, extend the proof to the same formula with something instantiated instead.
+ t.foldLeft((p, phi)) { case ((p, f), t1) => (instantiateForall(p, f, t1), f match {
+ case b @ BinderFormula(Forall, _, _) => instantiateBinder(b, t1)
+ case _ => throw new Exception
+ }) }._1
+ }
+ def instantiateForall(p: SCProof, t: Term): SCProof = instantiateForall(p, p.conclusion.right.head, t) // if a single formula on the right
+ def instantiateForall(p: SCProof, t: Term*): SCProof = { // given a proof with a formula quantified with \forall on the right, extend the proof to the same formula with something instantiated instead.
+ t.foldLeft(p)((p1, t1) => instantiateForall(p1, t1))
+ }
+ def generalizeToForall(p: SCProof, phi: Formula, x: VariableLabel): SCProof = {
+ require(p.conclusion.right.contains(phi))
+ val p1 = RightForall(p.conclusion -> phi +> forall(x, phi), p.length - 1, phi, x)
+ p appended p1
+ }
+ def generalizeToForall(p: SCProof, x: VariableLabel): SCProof = generalizeToForall(p, p.conclusion.right.head, x)
+ def generalizeToForall(p: SCProof, x: VariableLabel*): SCProof = { // given a proof with a formula on the right, extend the proof to the same formula with variables universally quantified.
+ x.foldRight(p)((x1, p1) => generalizeToForall(p1, x1))
+ }
+ def byEquiv(f: Formula, f1: Formula)(pEq: SCProofStep, pr1: SCProofStep): SCProof = {
+ require(pEq.bot.right.contains(f))
+ require(pr1.bot.right.contains(f1))
+ f match {
+ case ConnectorFormula(Iff, Seq(fl, fr)) =>
+ val f2 = if (isSame(f1, fl)) fr else if (isSame(f1, fr)) fl else throw new Error("not applicable")
+ val p2 = hypothesis(f1)
+ val p3 = hypothesis(f2)
+ val p4 = LeftImplies(Sequent(Set(f1, f1 ==> f2), Set(f2)), 2, 3, f1, f2)
+ val p5 = LeftIff(Sequent(Set(f1, f1 <=> f2), Set(f2)), 4, f1, f2)
+ val p6 = Cut(pEq.bot -> (f1 <=> f2) +< f1 +> f2, 0, 5, f1 <=> f2)
+ val p7 = Cut(p6.bot -< f1 ++ pr1.bot -> f1, 1, 6, f1)
+ new SCProof(IndexedSeq(pEq, pr1, p2, p3, p4, p5, p6, p7))
+ case _ => throw new Error("not applicable")
+ }
+ }
+ def simpleFunctionDefinition(f: FunctionLabel, t: Term, args: Seq[VariableLabel]): SCProof = {
+ assert(t.freeVariables subsetOf args.toSet)
+ val x = VariableLabel(freshId(t.freeVariables.map(_.id), "x"))
+ val y = VariableLabel(freshId(t.freeVariables.map(_.id)+x.id, "x"))
+ val p0 = RightRefl(emptySeq +> (t === t), t === t) // |- t===t
+ val p1 = hypothesis(y === t) // (t===y)|-(t===y)
+ val p2 = RightImplies(emptySeq +> ((t === y) ==> (t === y)), 1, t === y, t === y) // |- (t===y)==>(t===y)
+ val p3 = RightForall(emptySeq +> forall(y, (t === y) ==> (t === y)), 2, p2.bot.right.head, y) // |- ∀y (t===y)==>(t===y)
+ val p4 = RightAnd(emptySeq +> p0.bot.right.head /\ p3.bot.right.head, Seq(0, 3), Seq(p0.bot.right.head, p3.bot.right.head)) // |- t===t /\ ∀y(t===y)==>(t===y)
+ val p5 = RightExists(emptySeq +> exists(x, (x === t) /\ forall(y, (t === y) ==> (x === y))), 4,
+ (x === t) /\ forall(y, (t === y) ==> (x === y)), x, t) // |- ∃x x === t /\ ∀y(t===y)==>(x===y)
+ val definition = SCProof(IndexedSeq(p0, p1, p2, p3, p4, p5))
+ val fdef = args.foldLeft((definition.steps, p5.bot.right.head, 5))((prev, x) => {
+ val fo = forall(x, prev._2)
+ (prev._1 appended RightForall(emptySeq +> fo, prev._3, prev._2, x), fo, prev._3 + 1)
+ })
+ //val p6 = MakeFunctionDefinition(fdef._1.size - 1, f, args, x, x === t)
+ SCProof(fdef._1 )
+ }
+ // p1 is a proof of psi given phi, p2 is a proof of psi given !phi
+ def byCase(phi: Formula)(pa: SCProofStep, pb: SCProofStep): SCProof = {
+ val nphi = !phi
+ val (leftAphi, leftBnphi) = (pa.bot.left.find(isSame(_, phi)), pb.bot.left.find(isSame(_, nphi)))
+
+ require(leftAphi.nonEmpty && leftBnphi.nonEmpty)
+ val p2 = RightNot(pa.bot -< leftAphi.get +> nphi, 0, phi)
+ val p3 = Cut(pa.bot -< leftAphi.get ++ (pb.bot -< leftBnphi.get), 2, 1, nphi)
+ SCProof(IndexedSeq(pa, pb, p2, p3))
+ }
+ // pa is a proof of phi, pb is a proof of phi ==> ???
+ // |- phi ==> psi, phi===>gamma |- phi
+ // -------------------------------------
+ // |- psi, gamma
+ def modusPonens(phi: Formula)(pa: SCProofStep, pb: SCProofStep): SCProof = {
+ require(pa.bot.right.contains(phi))
+ val opsi = pb.bot.right.find {
+ case ConnectorFormula(Implies, Seq(l, _)) if isSame(l, phi) => true
+ case _ => false
+ }
+ if (opsi.isEmpty) SCProof(pa, pb)
+ else {
+ val psi = opsi.get.asInstanceOf[ConnectorFormula].args(1)
+ val p2 = hypothesis(psi)
+ val p3 = LeftImplies(emptySeq ++ (pa.bot -> phi) +< (phi ==> psi) +> psi, 0, 2, phi, psi)
+ val p4 = Cut(emptySeq ++ (pa.bot -> phi) ++< pb.bot +> psi ++> (pb.bot -> (phi ==> psi)), 1, 3, phi ==> psi)
+ SCProof(pa, pb, p2, p3, p4)
+ }
+ }
+
+ def detectSubstitution(x: VariableLabel, f: Formula, s: Formula, c: Option[Term] = None): (Option[Term], Boolean) = (f, s) match {
+ case (PredicateFormula(la1, args1), PredicateFormula(la2, args2)) if isSame(la1, la2) => {
+ args1.zip(args2).foldLeft[(Option[Term], Boolean)](c, true)((r1, a) => {
+ val r2 = detectSubstitutionT(x, a._1, a._2, r1._1)
+ (if (r1._1.isEmpty) r2._1 else r1._1, r1._2 && r2._2 && (r1._1.isEmpty || r2._1.isEmpty || isSame(r1._1.get, r2._1.get)))
+ })
+ }
+ case (ConnectorFormula(la1, args1), ConnectorFormula(la2, args2)) if isSame(la1, la2) => {
+ args1.zip(args2).foldLeft[(Option[Term], Boolean)](c, true)((r1, a) => {
+ val r2 = detectSubstitution(x, a._1, a._2, r1._1)
+ (if (r1._1.isEmpty) r2._1 else r1._1, r1._2 && r2._2 && (r1._1.isEmpty || r2._1.isEmpty || isSame(r1._1.get, r2._1.get)))
+ })
+ }
+ case (BinderFormula(la1, bound1, inner1), BinderFormula(la2, bound2, inner2)) if la1 == la2 && bound1 == bound2 => { // TODO renaming
+ detectSubstitution(x, inner1, inner2, c)
+ }
+ case _ => (c, false)
+ }
+ def detectSubstitutionT(x: VariableLabel, t: Term, s: Term, c: Option[Term] = None): (Option[Term], Boolean) = (t, s) match {
+ case (y: VariableTerm, z: Term) => {
+ if (isSame(y.label, x)) {
+ if (c.isDefined) {
+ (c, isSame(c.get, z))
+ }
+ else {
+ (Some(z), true)
+ }
+ }
+ else (c, isSame(y, z))
+ }
+ case (FunctionTerm(la1, args1), FunctionTerm(la2, args2)) if isSame(la1, la2) => {
+ args1.zip(args2).foldLeft[(Option[Term], Boolean)](c, true)((r1, a) => {
+ val r2 = detectSubstitutionT(x, a._1, a._2, r1._1)
+ (if (r1._1.isEmpty) r2._1 else r1._1, r1._2 && r2._2 && (r1._1.isEmpty || r2._1.isEmpty || isSame(r1._1.get, r2._1.get)))
+ })
+ }
+ case _ => (c, false)
+ }
+
+}
diff --git a/src/main/scala/proven/tactics/SimplePropositionalSolver.scala b/src/main/scala/proven/tactics/SimplePropositionalSolver.scala
new file mode 100644
index 0000000000000000000000000000000000000000..86f9d7fbcddfe15b35d6a1a7d38edaadc54f0475
--- /dev/null
+++ b/src/main/scala/proven/tactics/SimplePropositionalSolver.scala
@@ -0,0 +1,173 @@
+package proven.tactics
+
+import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.SequentCalculus.*
+import scala.collection.mutable.Set as mSet
+import lisa.KernelHelpers.*
+import lisa.kernel.proof.SCProof
+
+/**
+ * A simple but complete solver for propositional logic. Will not terminate for large problems
+ */
+object SimplePropositionalSolver {
+ class OrganisedFormulaSet {
+ val negs: mSet[ConnectorFormula] = mSet()
+ val impliess: mSet[ConnectorFormula] = mSet()
+ val iffs: mSet[ConnectorFormula] = mSet()
+ val ands: mSet[ConnectorFormula] = mSet()
+ val ors: mSet[ConnectorFormula] = mSet()
+ val others: mSet[Formula] = mSet()
+
+ def updateFormula(phi: Formula, add: Boolean): Unit = (phi match {
+ case phi@ConnectorFormula(label, args) =>
+ label match {
+ case Neg => if (add) negs.add(phi) else negs.remove(phi)
+ case Implies => if (add) impliess.add(phi) else impliess.remove(phi)
+ case Iff => if (add) iffs.add(phi) else iffs.remove(phi)
+ case And => if (add) ands.add(phi) else ands.remove(phi)
+ case Or => if (add) ors.add(phi) else ors.remove(phi)
+ }
+ case _ => if (add) others.add(phi) else others.remove(phi)
+ })
+
+ def copy(): OrganisedFormulaSet = {
+ val r = new OrganisedFormulaSet
+ r.negs.addAll(negs)
+ r.impliess.addAll(impliess)
+ r.iffs.addAll(iffs)
+ r.ands.addAll(ands)
+ r.ors.addAll(ors)
+ r.others.addAll(others)
+ r
+ }
+ }
+
+ def solveOrganisedSequent(left: OrganisedFormulaSet, right: OrganisedFormulaSet, s: Sequent, offset: Int): List[SCProofStep] = {
+ if (left.negs.nonEmpty) {
+ val f = left.negs.head
+ val phi = f.args.head
+ left.updateFormula(f, false)
+ right.updateFormula(f.args.head, true)
+ val proof = solveOrganisedSequent(left, right, s -< f +> phi, offset)
+ LeftNot(s, proof.length - 1 + offset, phi) :: proof
+ }
+ else if (left.impliess.nonEmpty) {
+ val f = left.impliess.head
+ val phi = f.args(0)
+ val psi = f.args(1)
+
+ left.updateFormula(f, false) //gamma
+ val rl = left.copy() //sigma
+ val rr = right.copy() //pi
+ right.updateFormula(phi, true) //delta
+ rl.updateFormula(psi, true)
+ val proof1 = solveOrganisedSequent(left, right, s -< f +> phi, offset)
+ val proof2 = solveOrganisedSequent(rl, rr, s -< f +< psi, offset + proof1.size)
+ LeftImplies(s, proof1.size + offset - 1, proof1.size + proof2.size + offset - 1, phi, psi) :: (proof2 ++ proof1)
+ }
+ else if (left.iffs.nonEmpty)
+ val f = left.iffs.head
+ val phi = f.args(0)
+ val psi = f.args(1)
+ left.updateFormula(f, false)
+ left.updateFormula(phi ==> psi, true)
+ left.updateFormula(psi ==> phi, true)
+ val proof = solveOrganisedSequent(left, right, s -< f +< (phi ==> psi) +< (psi ==> phi), offset)
+ LeftIff(s, proof.length - 1 + offset, phi, psi) :: proof
+ else if (left.ands.nonEmpty) {
+ val f = left.ands.head
+ val phi = f.args(0)
+ val psi = f.args(1)
+ left.updateFormula(f, false)
+ left.updateFormula(phi, true)
+ left.updateFormula(psi, true)
+ val proof = solveOrganisedSequent(left, right, s -< f +< phi +< psi, offset)
+ LeftAnd(s, proof.length - 1 + offset, phi, psi) :: proof
+
+ }
+ else if (left.ors.nonEmpty) {
+ val f = left.ors.head
+ val phi = f.args(0)
+ val psi = f.args(1)
+
+ left.updateFormula(f, false) //gamma
+ val rl = left.copy() //sigma
+ val rr = right.copy() //pi
+ left.updateFormula(phi, true) //delta
+ rl.updateFormula(psi, true)
+ val proof1 = solveOrganisedSequent(left, right, s -< f +< phi, offset)
+ val proof2 = solveOrganisedSequent(rl, rr, s -< f +< psi, offset + proof1.size)
+ LeftOr(s, Seq(proof1.size + offset - 1, proof1.size + proof2.size + offset - 1), Seq(phi, psi)) :: (proof2 ++ proof1)
+ }
+ else if (right.negs.nonEmpty)
+ val f = right.negs.head
+ val phi = f.args.head
+ right.updateFormula(f, false)
+ left.updateFormula(phi, true)
+ val proof = solveOrganisedSequent(left, right, s -> f +< phi, offset)
+ RightNot(s, proof.length - 1 + offset, phi) :: proof
+ else if (right.impliess.nonEmpty) {
+ val f = right.impliess.head
+ val phi = f.args(0)
+ val psi = f.args(1)
+ left.updateFormula(phi, true)
+ right.updateFormula(f, false)
+ right.updateFormula(psi, true)
+ val proof = solveOrganisedSequent(left, right, s -> f +< phi +> psi, offset)
+ RightImplies(s, proof.length - 1 + offset, phi, psi) :: proof
+ }
+ else if (right.iffs.nonEmpty)
+ val f = right.iffs.head
+ val phi = f.args(0)
+ val psi = f.args(1)
+ right.updateFormula(f, false) //gamma
+ val rl = left.copy() //sigma
+ val rr = right.copy() //pi
+ right.updateFormula(phi ==> psi, true) //delta
+ rr.updateFormula(psi ==> phi, true)
+ val proof1 = solveOrganisedSequent(left, right, s -> f +> (phi ==> psi), offset)
+ val proof2 = solveOrganisedSequent(rl, rr, s -> f +> (psi ==> phi), offset + proof1.size)
+ RightIff(s, proof1.size + offset - 1, proof1.size + proof2.size + offset - 1, phi, psi) :: (proof2 ++ proof1)
+ else if (right.ands.nonEmpty) {
+ val f = right.ands.head
+ val phi = f.args(0)
+ val psi = f.args(1)
+
+ right.updateFormula(f, false) //gamma
+ val rl = left.copy() //sigma
+ val rr = right.copy() //pi
+ right.updateFormula(phi, true) //delta
+ rr.updateFormula(psi, true)
+ val proof1 = solveOrganisedSequent(left, right, s -> f +> phi, offset)
+ val proof2 = solveOrganisedSequent(rl, rr, s -> f +> psi, offset + proof1.size)
+ RightAnd(s, Seq(proof1.size + offset - 1, proof1.size + proof2.size + offset - 1), Seq(phi, psi)) :: (proof2 ++ proof1)
+ }
+ else if (right.ors.nonEmpty) {
+ val f = right.ors.head
+ val phi = f.args(0)
+ val psi = f.args(1)
+ right.updateFormula(f, false)
+ right.updateFormula(phi, true)
+ right.updateFormula(psi, true)
+ val proof = solveOrganisedSequent(left, right, s -> f +> phi +> psi, offset)
+ RightOr(s, proof.length - 1 + offset, phi, psi) :: proof
+
+ }
+ else {
+ val f = s.left.find(f => s.right.contains(f))
+ List(Hypothesis(s, if (f.nonEmpty) f.get else PredicateFormula(SchematicPredicateLabel("P", 0), Seq())))
+ }
+ }
+
+ def solveSequent(s: Sequent): SCProof = {
+ val l = new OrganisedFormulaSet
+ s.left.foreach(f => l.updateFormula(f, true))
+ val r = new OrganisedFormulaSet
+ s.right.foreach(f => r.updateFormula(f, true))
+ val r2 = solveOrganisedSequent(l, r, s, 0)
+ val r3 = r2.reverse.toVector
+ val r4 = SCProof(r3)
+ r4
+ }
+
+}
diff --git a/src/main/scala/tptp/KernelParser.scala b/src/main/scala/tptp/KernelParser.scala
new file mode 100644
index 0000000000000000000000000000000000000000..cca3ff4fbdeccb45ce3c6e86c3f63650fd5a8bd4
--- /dev/null
+++ b/src/main/scala/tptp/KernelParser.scala
@@ -0,0 +1,238 @@
+package tptp
+
+import leo.modules.input.TPTPParser as Parser
+import Parser.TPTPParseException
+import leo.datastructures.TPTP
+import leo.datastructures.TPTP.{CNF, FOF}
+import lisa.kernel.fol.FOL as K
+import lisa.kernel.proof.SequentCalculus as SK
+import lisa.KernelHelpers.*
+
+import java.io.File
+import scala.util.matching.Regex
+
+object KernelParser {
+
+ case class AnnotatedFormula(role: String, name: String, formula: K.Formula)
+
+ case class Problem(file: String, domain: String, name: String, status: String, spc: Seq[String], formulas: Seq[AnnotatedFormula])
+
+ case class FileNotAcceptedException(msg: String, file: String) extends Exception(msg + " File: " + file)
+
+ private case class ProblemMetadata(file: String, domain: String, problem: String, status: String, spc: Seq[String])
+
+ /**
+ *
+ * @param formula A formula in the tptp language
+ * @return the corresponding LISA formula
+ */
+ def parseToKernel(formula: String): K.Formula = convertToKernel(Parser.fof(formula))
+
+ /**
+ *
+ * @param formula a tptp formula in leo parser
+ * @return the same formula in LISA
+ */
+ def convertToKernel(formula: FOF.Formula): K.Formula = {
+ formula match {
+ case FOF.AtomicFormula(f, args) => K.PredicateFormula(K.ConstantPredicateLabel(f, args.size), args map convertTermToKernel)
+ case FOF.QuantifiedFormula(quantifier, variableList, body) => quantifier match {
+ case FOF.! => variableList.foldRight(convertToKernel(body))((s, f) => K.Forall(K.VariableLabel(s), f))
+ case FOF.? => variableList.foldRight(convertToKernel(body))((s, f) => K.Exists(K.VariableLabel(s), f))
+ }
+ case FOF.UnaryFormula(connective, body) => connective match {
+ case FOF.~ => K.Neg(convertToKernel(body))
+ }
+ case FOF.BinaryFormula(connective, left, right) => connective match {
+ case FOF.<=> => convertToKernel(left) <=> convertToKernel(right)
+ case FOF.Impl => convertToKernel(left) ==> convertToKernel(right)
+ case FOF.<= => convertToKernel(right) ==> convertToKernel(left)
+ case FOF.<~> => !(convertToKernel(left) <=> convertToKernel(right))
+ case FOF.~| => !(convertToKernel(left) \/ convertToKernel(right))
+ case FOF.~& => !(convertToKernel(left) /\ convertToKernel(right))
+ case FOF.| => convertToKernel(left) \/ convertToKernel(right)
+ case FOF.& => convertToKernel(left) /\ convertToKernel(right)
+ }
+ case FOF.Equality(left, right) => K.equality(convertTermToKernel(left), convertTermToKernel(right))
+ case FOF.Inequality(left, right) => !K.equality(convertTermToKernel(left), convertTermToKernel(right))
+ }
+ }
+
+ def convertToKernel(formula: CNF.Formula): K.Formula = {
+
+ K.ConnectorFormula(K.Or, formula.map {
+ case CNF.PositiveAtomic(formula) => K.PredicateFormula(K.ConstantPredicateLabel(formula.f, formula.args.size), formula.args.map(convertTermToKernel).toList)
+ case CNF.NegativeAtomic(formula) => !K.PredicateFormula(K.ConstantPredicateLabel(formula.f, formula.args.size), formula.args.map(convertTermToKernel).toList)
+ case CNF.Equality(left, right) => K.equality(convertTermToKernel(left), convertTermToKernel(right))
+ case CNF.Inequality(left, right) => !K.equality(convertTermToKernel(left), convertTermToKernel(right))
+ })
+ }
+
+ /**
+ *
+ * @param term a tptp term in leo parser
+ * @return the same term in LISA
+ */
+ def convertTermToKernel(term: CNF.Term): K.Term = term match {
+ case CNF.AtomicTerm(f, args) => K.FunctionTerm(K.ConstantFunctionLabel(f, args.size), args map convertTermToKernel)
+ case CNF.Variable(name) => K.VariableTerm(K.VariableLabel(name))
+ case CNF.DistinctObject(name) => ???
+ }
+
+ /**
+ *
+ * @param term a tptp term in leo parser
+ * @return the same term in LISA
+ */
+ def convertTermToKernel(term: FOF.Term): K.Term = term match {
+ case FOF.AtomicTerm(f, args) =>
+ K.FunctionTerm(K.ConstantFunctionLabel(f, args.size), args map convertTermToKernel)
+ case FOF.Variable(name) => K.VariableTerm(K.VariableLabel(name))
+ case FOF.DistinctObject(name) => ???
+ case FOF.NumberTerm(value) => ???
+ }
+
+ /**
+ *
+ * @param formula an annotated tptp formula
+ * @return the corresponding LISA formula augmented with name and role.
+ */
+ def annotatedFormulaToKernel(formula: String): AnnotatedFormula = {
+ val i = Parser.annotatedFOF(formula)
+ i.formula match {
+ case FOF.Logical(formula) => AnnotatedFormula(i.role, i.name, convertToKernel(formula))
+ }
+ }
+
+ private def problemToKernel(problemFile: File, md: ProblemMetadata): Problem = {
+ val file = io.Source.fromFile(problemFile)
+ val pattern = "SPC\\s*:\\s*[A-z]{3}(_[A-z]{3})*".r
+ val g = file.getLines()
+
+ def search(): String = pattern.findFirstIn(g.next()).getOrElse(search())
+
+ val i = Parser.problem(file)
+ val sq = i.formulas map {
+ case TPTP.FOFAnnotated(name, role, formula, annotations) => formula match {
+ case FOF.Logical(formula) => AnnotatedFormula(role, name, convertToKernel(formula))
+ }
+ case TPTP.CNFAnnotated(name, role, formula, annotations) => formula match {
+ case CNF.Logical(formula) => AnnotatedFormula(role, name, convertToKernel(formula))
+ }
+ case _ => throw FileNotAcceptedException("Only FOF formulas are supported", problemFile.getPath)
+ }
+ Problem(md.file, md.domain, md.problem, md.status, md.spc, sq)
+ }
+
+ /**
+ *
+ * @param problemFile a file containning a tptp problem
+ * @return a Problem object containing the data of the tptp problem in LISA representation
+ */
+ def problemToKernel(problemFile: File): Problem = {
+ problemToKernel(problemFile, getProblemInfos(problemFile))
+ }
+
+ /**
+ *
+ * @param problemFile a path to a file containing a tptp problem
+ * @return a Problem object containing the data of the tptp problem in LISA representation
+ */
+ def problemToKernel(problemFile: String): Problem = {
+ problemToKernel(File(problemFile))
+ }
+
+ /**
+ * Given a problem consisting of many axioms and a single conjecture, create a sequent with axioms on the left
+ * and conjecture on the right.
+ *
+ * @param problem a problem, containing a list of annotated formulas from a tptp file
+ * @return a sequent with axioms of the problem on the left, and the conjecture on the right
+ */
+ def problemToSequent(problem: Problem): SK.Sequent = {
+ if (problem.spc.contains("CNF")) problem.formulas.map(_.formula) |- ()
+ else problem.formulas.foldLeft[SK.Sequent](() |- ())((s, f) =>
+ if (f._1 == "axiom") s +< f._3
+ else if (f._1 == "conjecture" && s.right.isEmpty) s +> f._3
+ else throw Exception("Can only agglomerate axioms and one conjecture into a sequents")
+ )
+ }
+
+ /**
+ * Given a folder containing folders containing problem (typical organisation of TPTP library) and a list of spc,
+ * return the same arrangement of problems in LISA syntax, filtered so that only problems with at least one
+ * spc from the "spc" argument.
+ *
+ * @param spc a list of 3-characters codes representing properties of a problem, such as FOF for First Order Logic.
+ * @param path the path to the tptp library.
+ * @return A sequence of domains, each being a sequence of problems
+ */
+ def gatherAllTPTPFormulas(spc: Seq[String], path: String): Seq[Seq[Problem]] = {
+ val d = new File(path)
+ val probfiles: Array[File] = if (d.exists) {
+ if (d.isDirectory) {
+ if (d.listFiles().isEmpty) println("empty directory")
+ d.listFiles.filter(_.isDirectory)
+
+ }
+ else throw new Exception("Specified path is not a directory.")
+ }
+ else throw new Exception("Specified path does not exist.")
+
+ probfiles.map(d => gatherFormulas(spc, d.getPath)).toSeq
+ }
+
+ def gatherFormulas(spc: Seq[String], path: String): Seq[Problem] = {
+ val d = new File(path)
+ val probfiles: Array[File] = if (d.exists) {
+ if (d.isDirectory) {
+ if (d.listFiles().isEmpty) println("empty directory")
+ d.listFiles.filter(_.isFile)
+
+ }
+ else throw new Exception("Specified path is not a directory.")
+ }
+ else throw new Exception("Specified path does not exist.")
+
+ val r = probfiles.foldRight(List.empty[Problem])((p, current) =>
+ val md = getProblemInfos(p)
+ if (md.spc.exists(spc.contains)) problemToKernel(p, md) :: current
+ else current
+ )
+ r
+ }
+
+
+ /**
+ *
+ * @param file a file containing a tptp problem
+ * @return the metadata info (file name, domain, problem, status and spc) in the file
+ */
+ private def getProblemInfos(file: File): ProblemMetadata = {
+ val pattern = "((File)|(Domain)|(Problem)|(Status)|(SPC))\\s*:.*".r
+ val s = io.Source.fromFile(file)
+ val g = s.getLines()
+ var fil: String = "?"
+ var dom: String = "?"
+ var pro: String = "?"
+ var sta: String = "?"
+ var spc: Seq[String] = Seq()
+
+ val count: Int = 0
+ while (g.hasNext && count < 5) {
+ val line = g.next()
+ val res = pattern.findFirstIn(line)
+ if (res.nonEmpty) {
+ val act = res.get
+ if (act(0) == 'F') fil = act.drop(act.indexOf(":") + 2)
+ else if (act(0) == 'D') dom = act.drop(act.indexOf(":") + 2)
+ else if (act(0) == 'P') pro = act.drop(act.indexOf(":") + 2)
+ else if (act(1) == 't') sta = act.drop(act.indexOf(":") + 2)
+ else if (act(1) == 'P') spc = act.drop(act.indexOf(":") + 2).split("_").toIndexedSeq
+ }
+ }
+ s.close()
+ ProblemMetadata(fil, dom, pro, sta, spc)
+ }
+
+}
diff --git a/src/main/scala/tptp/ProblemGatherer.scala b/src/main/scala/tptp/ProblemGatherer.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5fb3199202094ae466912200661f930d9a22891e
--- /dev/null
+++ b/src/main/scala/tptp/ProblemGatherer.scala
@@ -0,0 +1,16 @@
+package tptp
+
+import tptp.KernelParser._
+
+object ProblemGatherer {
+
+ /**
+ * The tptp library needs to be included in main/resources. It can be found at http://www.tptp.org/
+ * @return sequence of tptp problems with the PRP (propositional) tag.
+ */
+ def getPRPproblems: Seq[Problem] = {
+ val path = getClass.getResource("/TPTP/Problems/SYN/").getPath
+ gatherFormulas(Seq("PRP"), path)
+ }
+
+}
diff --git a/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala b/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
new file mode 100644
index 0000000000000000000000000000000000000000..68a5fa28e5b32e6af711482c46e7644f30b25f2a
--- /dev/null
+++ b/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
@@ -0,0 +1,332 @@
+package lisa.kernel
+
+import lisa.KernelHelpers.*
+import lisa.kernel.Printer
+import lisa.kernel.fol.FOL
+import lisa.kernel.fol.FOL.*
+import org.scalatest.funsuite.AnyFunSuite
+
+import scala.collection.MapView
+import scala.collection.mutable.{ArrayBuffer, ListBuffer}
+import scala.util.Random
+
+class EquivalenceCheckerTests extends AnyFunSuite {
+ private val verbose = false // Turn this on to print all tested couples
+
+ def checkEquivalence(left: Formula, right: Formula): Unit = {
+ assert(isSame(left, right), s"Couldn't prove the equivalence between ${Printer.prettyFormula(left)} and ${Printer.prettyFormula(right)}\nLeft tree: ${left}\nRight tree: ${right}")
+ }
+
+ def checkNonEquivalence(left: Formula, right: Formula): Unit = {
+ assert(!isSame(left, right), s"Expected the checker to not be able to show equivalence between ${Printer.prettyFormula(left)} and ${Printer.prettyFormula(right)}\nLeft tree: ${left}\nRight tree: ${right}")
+ }
+
+ def nameGenerator(): () => String = {
+ val chars = 'a' to 'z'
+ def stream: LazyList[Seq[Char]] = LazyList.from(chars.map(Seq(_))) #::: stream.flatMap(l => chars.map(_ +: l))
+ var current = stream
+ () => {
+ val id = current.head.reverse.mkString
+ current = current.tail
+ id
+ }
+ }
+ def numbersGenerator(): () => Int = {
+ var i = 1
+ () => {
+ val n = i
+ i += 1
+ n
+ }
+ }
+
+ def constantsGenerator(): () => Formula = {
+ val generator = nameGenerator()
+ () => {
+ val id = generator()
+ PredicateFormula(ConstantPredicateLabel(id, 0), Seq.empty)
+ }
+ }
+
+ def formulasGenerator(c: Double)(random: Random): () => Formula = {
+ val connectors = ArrayBuffer.empty[String]
+ val variables = ArrayBuffer.empty[String]
+ val nextConnectorName = nameGenerator()
+ val nextVariableName = {
+ val gen = numbersGenerator()
+ () => s"v${gen()}"
+ }
+ def generate(p: Double): Formula = {
+ val q = random.nextDouble()
+
+ if(q >= p) {
+ // Leaf
+ val name =
+ if(connectors.isEmpty || random.nextDouble() <= 0.75) { // TODO adapt
+ // New name
+ val id = nextConnectorName()
+ connectors += id
+ id
+ } else {
+ // Reuse existing name
+ connectors(random.nextInt(connectors.size))
+ }
+ PredicateFormula(ConstantPredicateLabel(name, 0), Seq.empty)
+ } else {
+ // Branch
+ val nextP = p * c
+ if(random.nextDouble() < 0.9) {
+ // Connector
+ val binaries = Seq(and, or, iff, implies)
+ if(random.nextInt(binaries.size + 1) > 0) {
+ // Binary
+ val binary = binaries(random.nextInt(binaries.size))
+ val (l, r) = {
+ val p1 = nextP * nextP
+ val (f1, f2) = (generate(p1), generate(p1))
+ if(random.nextBoolean()) (f1, f2) else (f2, f1)
+ }
+ (binary(l, r))
+ } else {
+ // Unary
+ neg(generate(nextP))
+ }
+ } else {
+ // Binder
+ val name = nextVariableName()
+ variables += name
+ val binderTypes: IndexedSeq[BinderLabel] = IndexedSeq(Forall, Exists, ExistsOne)
+ val binderType = binderTypes(random.nextInt(binderTypes.size))
+ BinderFormula(binderType, VariableLabel(name), generate(nextP))
+ }
+ }
+ }
+
+ () => generate(c)
+ }
+
+ def testcasesAny(generatorToTestcases: (() => Formula) => Random => Seq[(Formula, Formula)], equivalent: Boolean): Unit = {
+ val random: Random = new Random(1)
+
+ def testWith(generator: () => () => Formula): Unit = {
+ val cases = generatorToTestcases(generator())(random)
+ cases.foreach { (left, right) =>
+ // For completeness we also test symmetry
+ if(equivalent) {
+ checkEquivalence(left, right)
+ checkEquivalence(right, left)
+ if(verbose) {
+ println(s"${Printer.prettyFormula(left)} <==> ${Printer.prettyFormula(right)}")
+ }
+ } else {
+ checkNonEquivalence(left, right)
+ checkNonEquivalence(right, left)
+ if(verbose) {
+ println(s"${Printer.prettyFormula(left)} <!=> ${Printer.prettyFormula(right)}")
+ }
+ }
+ }
+ }
+
+ def testWithRepeat(generator: () => () => Formula, n: Int): Unit = {
+ for(i <- 0 until n) {
+ testWith(generator)
+ }
+ }
+
+ // 1. Constants (a, b, c, ...)
+
+ testWith(constantsGenerator)
+
+ // 2. Random formulas (small)
+
+ testWithRepeat(() => formulasGenerator(0.8)(random), 100)
+
+ // 3. Random formulas (larger)
+
+ testWithRepeat(() => formulasGenerator(0.99)(random), 100)
+ }
+
+ def testcases(f: Formula => Random => Seq[(Formula, Formula)], equivalent: Boolean): Unit =
+ testcasesAny(generator => r => f(generator())(r), equivalent)
+ def testcases(f: (Formula, Formula) => Random => Seq[(Formula, Formula)], equivalent: Boolean): Unit =
+ testcasesAny(generator => r => f(generator(), generator())(r), equivalent)
+ def testcases(f: (Formula, Formula, Formula) => Random => Seq[(Formula, Formula)], equivalent: Boolean): Unit =
+ testcasesAny(generator => r => f(generator(), generator(), generator())(r), equivalent)
+ def testcases(f: (Formula, Formula, Formula, Formula) => Random => Seq[(Formula, Formula)], equivalent: Boolean): Unit =
+ testcasesAny(generator => r => f(generator(), generator(), generator(), generator())(r), equivalent)
+
+ def repeatApply[T](n: Int)(f: T => T)(initial: T): T = if(n > 0) repeatApply(n - 1)(f)(f(initial)) else initial
+ def commutativeShuffle(iterations: Int)(random: Random)(f: Formula): Formula = {
+ def transform(f: Formula): Formula = f match {
+ case PredicateFormula(label, args) => f
+ case ConnectorFormula(label, args) =>
+ val newArgs = label match {
+ case And | Or | Iff => random.shuffle(args)
+ case _ => args
+ }
+ ConnectorFormula(label, newArgs.map(transform))
+ case BinderFormula(label, bound, inner) => BinderFormula(label, bound, transform(inner))
+ }
+ repeatApply(iterations)(transform)(f)
+ }
+ def associativeShuffle(iterations: Int)(random: Random)(f: Formula): Formula = {
+ def transform(f: Formula): Formula = f match {
+ case PredicateFormula(label, args) => f
+ // Simple for now, assume binary operations
+ case ConnectorFormula(label1 @ (And | Or), Seq(ConnectorFormula(label2, Seq(a1, a2)), a3)) if label1 == label2 =>
+ if(random.nextBoolean()) {
+ ConnectorFormula(label1, Seq(a1, ConnectorFormula(label2, Seq(a2, a3))))
+ } else {
+ f
+ }
+ case ConnectorFormula(label1 @ (And | Or), Seq(a1, ConnectorFormula(label2, Seq(a2, a3)))) if label1 == label2 =>
+ if(random.nextBoolean()) {
+ ConnectorFormula(label1, Seq(ConnectorFormula(label2, Seq(a1, a2)), a3))
+ } else {
+ f
+ }
+ case ConnectorFormula(label, args) => ConnectorFormula(label, args.map(transform))
+ case BinderFormula(label, bound, inner) => BinderFormula(label, bound, transform(inner))
+ }
+ repeatApply(iterations)(transform)(f)
+ }
+ def addDoubleNegations(p: Double)(random: Random)(f: Formula): Formula = {
+ def transform(f: Formula): Formula =
+ if(random.nextDouble() < p) neg(neg(transform(f)))
+ else f match {
+ case _: PredicateFormula => f
+ case ConnectorFormula(label, args) => ConnectorFormula(label, args.map(transform))
+ case BinderFormula(label, bound, inner) => BinderFormula(label, bound, transform(inner))
+ }
+ transform(f)
+ }
+ def addDeMorgans(p: Double)(random: Random)(f: Formula): Formula = {
+ def transform(f: Formula): Formula = f match {
+ case _: PredicateFormula => f
+ case ConnectorFormula(label, args) =>
+ val map: Map[ConnectorLabel, ConnectorLabel] = Map(And -> Or, Or -> And)
+ map.get(label) match {
+ case Some(opposite) if random.nextDouble() < p => transform(neg(ConnectorFormula(opposite, args.map(neg))))
+ case _ => ConnectorFormula(label, args.map(transform))
+ }
+ case BinderFormula(label, bound, inner) => BinderFormula(label, bound, transform(inner))
+ }
+ transform(f)
+ }
+
+ // Positive
+
+ test("Reflexivity") {
+ testcases(a => _ => Seq(a -> a), equivalent = true)
+ }
+
+ test("Commutativity (root with equal leaves)") {
+ testcases((a, b) => _ => Seq(
+ and(a, b) -> and(b, a),
+ or(a, b) -> or(b, a),
+ iff(a, b) -> iff(b, a),
+ ), equivalent = true)
+ }
+
+ test("Associativity (root with equal leaves)") {
+ testcases((a, b, c, d) => _ => Seq(
+ and(and(a, b), c) -> and(a, and(b, c)),
+ or(or(a, b), c) -> or(a, or(b, c)),
+ ), equivalent = true)
+ }
+
+ test("Commutativity (general)") {
+ testcases((a, b) => random => Seq(
+ a -> commutativeShuffle(15)(random)(a)
+ ), equivalent = true)
+ }
+
+ test("Associativity (general)") {
+ testcases((a, b) => random => Seq(
+ a -> associativeShuffle(15)(random)(a)
+ ), equivalent = true)
+ }
+
+ test("Commutativity and associativity (general)") {
+ testcases((a, b) => random => Seq(
+ a -> repeatApply(15)(commutativeShuffle(1)(random).andThen(associativeShuffle(1)(random)))(a)
+ ), equivalent = true)
+ }
+
+ test("Double negation (root with equal leaf)") {
+ testcases(a => _ => Seq(
+ a -> neg(neg(a)),
+ neg(a) -> neg(neg(neg(a))),
+ a -> neg(neg(neg(neg(a)))),
+ ), equivalent = true)
+ }
+
+ test("Double negation (general)") {
+ val p = 0.25
+ testcases(a => random => Seq(
+ addDoubleNegations(p)(random)(a) -> addDoubleNegations(p)(random)(a),
+ ), equivalent = true)
+ }
+
+ test("De Morgan's law (root)") {
+ testcases((a, b) => random => Seq(
+ and(a, b) -> neg(or(neg(a), neg(b))),
+ or(a, b) -> neg(and(neg(a), neg(b))),
+ ), equivalent = true)
+ }
+
+ test("De Morgan's law (general)") {
+ val p = 0.25
+ testcases(a => random => Seq(
+ addDeMorgans(p)(random)(a) -> addDeMorgans(p)(random)(a)
+ ), equivalent = true)
+ }
+
+ test("Allowed tautologies") {
+ testcases((a, b, c) => random => Seq(
+ or(a, neg(a)) -> or(neg(a), neg(neg(a))),
+ and(a, neg(a)) -> and(neg(a), neg(neg(a))),
+ ), equivalent = true)
+ }
+
+ test("Absorption") {
+ testcases((a, b, c) => random => Seq(
+ and(a, a) -> a,
+ or(a, a) -> a,
+ //or(or(a, neg(a)), c) -> c,
+ //and(and(a, neg(a)), c) -> and(a, neg(a)),
+ ), equivalent = true)
+ }
+
+ test("All allowed transformations") {
+ val transformations: Seq[Random => Formula => Formula] = IndexedSeq(
+ r => commutativeShuffle(1)(r) _,
+ r => associativeShuffle(1)(r) _,
+ r => addDoubleNegations(0.02)(r) _,
+ r => addDeMorgans(0.05)(r) _,
+ )
+ def randomTransformations(random: Random)(f: Formula): Formula = {
+ val n = random.nextInt(50)
+ Seq.fill(n)(transformations(random.nextInt(transformations.size))).foldLeft(f)((acc, e) => e(random)(acc))
+ }
+
+ testcases(a => random => Seq(
+ randomTransformations(random)(a) -> randomTransformations(random)(a)
+ ), equivalent = true)
+ }
+
+ // Negative
+
+ test("Negative by construction") {
+ val x = PredicateFormula(ConstantPredicateLabel("$", 0), Seq.empty) // Globally free
+ testcases((a, b) => random => Seq(
+ a -> and(a, x),
+ a -> or(a, x),
+ a -> implies(a, x),
+ a -> iff(a, x),
+ ), equivalent = false)
+ }
+
+
+}
diff --git a/src/test/scala/lisa/kernel/FolTests.scala b/src/test/scala/lisa/kernel/FolTests.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c5f3b6f3de7543c1f47ddf7a4fe628919259232e
--- /dev/null
+++ b/src/test/scala/lisa/kernel/FolTests.scala
@@ -0,0 +1,126 @@
+package lisa.kernel
+
+import lisa.KernelHelpers.{*, given}
+import lisa.kernel.Printer
+import lisa.kernel.proof.RunningTheory
+import org.scalatest.funsuite.AnyFunSuite
+import lisa.kernel.proof.SequentCalculus.*
+import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.RunningTheory.*
+import lisa.kernel.proof.{SCProof, SCProofChecker}
+
+import scala.collection.immutable.SortedSet
+import scala.util.Random
+
+class FolTests extends AnyFunSuite {
+
+ val predicateVerifier = SCProofChecker.checkSCProof
+
+ def nameGenerator(candidates: Seq[String], gen: Random = new Random(), l: Int = 1): String = {
+ if (gen.nextBoolean()) gen.nextString(1)
+ else candidates(gen.between(0, candidates.length))
+ }
+
+ def termGenerator(maxDepth: Int, gen: Random = new Random()): Term = {
+ if (maxDepth <= 1) {
+ val r = gen.between(0, 3)
+ if (r == 0) {
+ val name = "" + ('a' to 'e') (gen.between(0, 5))
+ FunctionTerm(ConstantFunctionLabel(name, 0), List())
+ }
+ else {
+ val name = "" + ('v' to 'z') (gen.between(0, 5))
+ VariableTerm(VariableLabel(name))
+ }
+ } else {
+ val r = gen.between(0, 8)
+ val name = "" + ('f' to 'j') (gen.between(0, 5))
+ if (r == 0) {
+ val name = "" + ('a' to 'e') (gen.between(0, 5))
+ FunctionTerm(ConstantFunctionLabel(name, 0), List())
+ }
+ else if (r == 1) {
+ val name = "" + ('v' to 'z') (gen.between(0, 5))
+ VariableTerm(VariableLabel(name))
+ }
+ if (r <= 3) FunctionTerm(ConstantFunctionLabel(name, 1), Seq(termGenerator(maxDepth - 1, gen)))
+ else if (r <= 5) FunctionTerm(ConstantFunctionLabel(name, 2), Seq(termGenerator(maxDepth - 1, gen), termGenerator(maxDepth - 1, gen)))
+ else if (r == 6) FunctionTerm(ConstantFunctionLabel(name, 3),
+ Seq(termGenerator(maxDepth - 1, gen), termGenerator(maxDepth - 1, gen), termGenerator(maxDepth - 1, gen)))
+ else FunctionTerm(ConstantFunctionLabel(name, 4),
+ Seq(termGenerator(maxDepth - 1, gen), termGenerator(maxDepth - 1, gen), termGenerator(maxDepth - 1, gen), termGenerator(maxDepth - 1, gen)))
+
+ }
+ }
+
+ def formulaGenerator(maxDepth: Int, gen: Random = new Random()): Formula = {
+ if (maxDepth <= 2 || (gen.nextBoolean() && gen.nextBoolean())) {
+ val r = gen.between(0, 7)
+ if (r <= 1) {
+ val name = "" + ('A' to 'E') (gen.between(0, 5))
+ PredicateFormula(ConstantPredicateLabel(name, 0), Seq())
+ }
+
+ else if (r <= 3) {
+ val name = "" + ('A' to 'E') (gen.between(0, 5))
+ PredicateFormula(ConstantPredicateLabel(name, 1), Seq(termGenerator(maxDepth - 1, gen)))
+ }
+
+ else if (r <= 5) {
+ val s = gen.between(0, 3)
+ if (s == 0) PredicateFormula(equality, Seq(termGenerator(maxDepth - 1, gen), termGenerator(maxDepth - 1, gen)))
+ else {
+ val name = "" + ('A' to 'E') (gen.between(0, 5))
+ PredicateFormula(ConstantPredicateLabel(name, 2), Seq(termGenerator(maxDepth - 1, gen), termGenerator(maxDepth - 1, gen)))
+ }
+ }
+ else {
+ val name = "" + ('A' to 'E') (gen.between(0, 5))
+ PredicateFormula(ConstantPredicateLabel(name, 3),
+ Seq(termGenerator(maxDepth - 1, gen), termGenerator(maxDepth - 1, gen), termGenerator(maxDepth - 1, gen)))
+ }
+
+ }
+ else {
+ val r = gen.between(0, 7)
+ if (r <= 1) neg(formulaGenerator(maxDepth - 1, gen))
+ else if (r == 2) and(formulaGenerator(maxDepth - 1, gen), formulaGenerator(maxDepth - 1, gen))
+ else if (r == 3) or(formulaGenerator(maxDepth - 1, gen), formulaGenerator(maxDepth - 1, gen))
+ else if (r == 4) implies(formulaGenerator(maxDepth - 1, gen),formulaGenerator(maxDepth - 1, gen))
+ else if (r == 5) {
+ val f = formulaGenerator(maxDepth - 1, gen)
+ val l = f.freeVariables.toSeq ++ Seq(x)
+ forall(l(gen.between(0, l.size)), f)
+ }
+ else {
+ val f = formulaGenerator(maxDepth - 1, gen)
+ val l = f.freeVariables.toSeq ++ Seq(x)
+ exists(l(gen.between(0, l.size)), f)
+ }
+ }
+
+ }
+
+ private val x = VariableLabel("x")
+ private val y = VariableLabel("y")
+ private val z = VariableLabel("z")
+ private val a = PredicateFormula(ConstantPredicateLabel("A", 0), Seq())
+ private val b = PredicateFormula(ConstantPredicateLabel("B", 0), Seq())
+ private val fp = ConstantPredicateLabel("F", 1)
+ private val sT = SchematicFunctionLabel("t", 0)
+
+ def test_some_random_formulas(n: Int, maxDepth: Int): Unit = {
+ (0 to n).foreach(_ => println(formulaGenerator(maxDepth)))
+ }
+
+ test("Random formulas well-constructed") {
+ (0 to 50).foreach(_ => formulaGenerator(10))
+ }
+
+
+ test("Fresh variables should be fresh") {
+ val y1 = VariableLabel(freshId(equ(VariableTerm(x), VariableTerm(x)).freeVariables.map(_.name), x.name))
+ //println(x1, y1)
+ assert(!isSame(x, y1))
+ }
+}
\ No newline at end of file
diff --git a/src/test/scala/lisa/kernel/IncorrectProofsTests.scala b/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9c7c151505387f5acb63e80589bc2266101ee380
--- /dev/null
+++ b/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
@@ -0,0 +1,97 @@
+package lisa.kernel
+
+//import lisa.settheory.AxiomaticSetTheory.{emptySet, emptySetAxiom, pair, pairAxiom, useAxiom}
+import lisa.KernelHelpers.*
+import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.SCProof
+import lisa.kernel.proof.SequentCalculus.*
+import test.ProofCheckerSuite
+
+import scala.collection.immutable.SortedSet
+import scala.language.implicitConversions
+
+class IncorrectProofsTests extends ProofCheckerSuite {
+ // These tests help to ensure that the proof checker correctly rejects incorrect proofs
+ // The cases are designed to be almost correct (but still incorrect) proofs to check various parts of the system
+
+ test("Minimal incorrect proofs") {
+ // Shorthand
+ implicit def proofStepToProof(proofStep: SCProofStep): SCProof = SCProof(proofStep)
+
+ val (fl, gl, hl) = (SchematicPredicateLabel("f", 0), SchematicPredicateLabel("g", 0), SchematicPredicateLabel("h", 0))
+ val f = PredicateFormula(fl, Seq.empty) // Some arbitrary formulas
+ val g = PredicateFormula(gl, Seq.empty)
+ val h = PredicateFormula(hl, Seq.empty)
+
+ val emptySetAxiom = lisa.settheory.AxiomaticSetTheory.emptySetAxiom
+ val pairAxiom = lisa.settheory.AxiomaticSetTheory.pairAxiom
+
+
+ val incorrectProofs: Seq[SCProof] = List(
+ SCProof(
+ Hypothesis(emptySeq +< (x === x) +> (x === x), x === x),
+ LeftRefl(emptySeq +> (x === y), 0, x === x)
+ ),
+ SCProof(
+ Hypothesis(emptySeq +< (x === y) +> (x === y), x === y),
+ LeftRefl(emptySeq +> (x === y), 0, x === y)
+ ),
+ RightRefl(emptySeq +> (x === y), x === y),
+ RightRefl(emptySeq +> f, x === x),
+ RightRefl(emptySeq +> (x === x), f),
+ // Correct proof would be: x=y |- x=y \ x=y,x=z |- z=y
+
+ SCProof(
+ Hypothesis(emptySeq +< (x === y) +> (x === y), x === y),
+ RightSubstEq(emptySeq +< (x === y) +< (x === z) +> (z === y), 0, x, z, x === y, yl) // wrong variable replaced
+ ),
+ SCProof(
+ Hypothesis(emptySeq +< (x === y) +> (x === y), x === y),
+ RightSubstEq(emptySeq +< (x === y) +> (z === y), 0, x, z, x === y, xl) // missing hypothesis
+ ),
+ SCProof(
+ Hypothesis(emptySeq +< (x === y) +> (x === y), x === y),
+ RightSubstEq(emptySeq +< (x === y) +< (x === z) +> (z === y), 0, x, z, x === z, xl) // replacement mismatch
+ ),
+ SCProof(
+ Hypothesis(emptySeq +< (x === y) +> (x === y), x === y),
+ LeftSubstEq(emptySeq +< (z === y) +< (x === z) +> (x === y), 0, x, z, x === y, yl)
+ ),
+ SCProof(
+ Hypothesis(emptySeq +< (f <=> g) +> (f <=> g), f <=> g),
+ LeftSubstIff(emptySeq +< (h <=> g) +< (f <=> h) +> (f <=> g), 0, f, h, f <=> g, gl)
+ ),
+ SCProof(
+ Hypothesis(emptySeq +< f +> f, f),
+ LeftAnd(emptySeq +< g +> f, 0, f, g)
+ ),
+ SCProof(
+ Hypothesis(emptySeq +< f +> f, f),
+ Hypothesis(emptySeq +< g +> g, g),
+ LeftImplies(emptySeq +< (g ==> f) +< f +> g, 0, 1, f, g)
+ ),
+ SCProof(
+ Hypothesis(emptySeq +< f +> f, f),
+ Hypothesis(emptySeq +< g +> g, g),
+ LeftOr(emptySeq +< (f \/ g) +< f +> g, Seq(0, 1), Seq(f, g))
+ ),
+ SCProof(
+ Hypothesis(emptySeq +< f +> f, f),
+ LeftNot(emptySeq +< f +> f, 0, f)
+ ),
+ SCProof(
+ Hypothesis(emptySeq +< f +> f, f),
+ Hypothesis(emptySeq +< g +> g, g),
+ RightAnd(emptySeq +< f +> (f /\ g), Seq(0, 1), Seq(f, g)) // missing left g
+ ),
+ SCProof(
+ Hypothesis(emptySeq +< f +> f, f),
+ RightOr(emptySeq +< f +> (f \/ g) +> g, 0, f, g) // supplemental right g
+ )
+
+ )
+
+ incorrectProofs.foreach(checkIncorrectProof)
+ }
+
+}
diff --git a/src/test/scala/lisa/kernel/PrinterTest.scala b/src/test/scala/lisa/kernel/PrinterTest.scala
new file mode 100644
index 0000000000000000000000000000000000000000..23edf5a24b16f47616809d8c9171255976e4800b
--- /dev/null
+++ b/src/test/scala/lisa/kernel/PrinterTest.scala
@@ -0,0 +1,43 @@
+package lisa.kernel
+
+import lisa.kernel.fol.FOL._
+import lisa.kernel.Printer._
+
+import org.scalatest.funsuite.AnyFunSuite
+
+class PrinterTest extends AnyFunSuite {
+
+ val (a, b, c) = (ConstantPredicateLabel("a", 0), ConstantPredicateLabel("b", 0), ConstantPredicateLabel("c", 0))
+ val (x, y, z) = (VariableLabel("x"), VariableLabel("y"), VariableLabel("z"))
+
+ given Conversion[PredicateLabel, PredicateFormula] = PredicateFormula(_, Seq.empty)
+ given Conversion[VariableLabel, VariableTerm] = VariableTerm.apply
+
+ test("Minimal parenthesization") {
+ assert(prettyFormula(ConnectorFormula(And, Seq(a, b))) == "a ∧ b")
+ assert(prettyFormula(ConnectorFormula(And, Seq(ConnectorFormula(And, Seq(a, b)), c))) == "(a ∧ b) ∧ c")
+ assert(prettyFormula(ConnectorFormula(And, Seq(a, ConnectorFormula(And, Seq(b, c))))) == "a ∧ b ∧ c")
+ assert(prettyFormula(ConnectorFormula(Or, Seq(a, ConnectorFormula(And, Seq(b, c))))) == "a ∨ b ∧ c")
+ assert(prettyFormula(ConnectorFormula(Or, Seq(ConnectorFormula(And, Seq(a, b)), c))) == "a ∧ b ∨ c")
+ assert(prettyFormula(ConnectorFormula(And, Seq(ConnectorFormula(Or, Seq(a, b)), c))) == "(a ∨ b) ∧ c")
+ assert(prettyFormula(ConnectorFormula(And, Seq(a, ConnectorFormula(Or, Seq(b, c))))) == "a ∧ (b ∨ c)")
+
+ assert(prettyFormula(ConnectorFormula(Neg, Seq(a))) == "¬a")
+ assert(prettyFormula(ConnectorFormula(Neg, Seq(ConnectorFormula(Neg, Seq(a))))) == "¬¬a")
+ assert(prettyFormula(ConnectorFormula(Neg, Seq(ConnectorFormula(Neg, Seq(ConnectorFormula(And, Seq(a, b))))))) == "¬¬(a ∧ b)")
+ assert(prettyFormula(ConnectorFormula(And, Seq(ConnectorFormula(Neg, Seq(a)), ConnectorFormula(And, Seq(ConnectorFormula(Neg, Seq(b)), ConnectorFormula(Neg, Seq(c))))))) == "¬a ∧ ¬b ∧ ¬c")
+
+ assert(prettyFormula(ConnectorFormula(And, Seq(a, PredicateFormula(equality, Seq(x, x))))) == "a ∧ (x = x)")
+
+ assert(prettyFormula(BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x)))) == "∀x. x = x")
+ assert(prettyFormula(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x)))))) == "a ∧ ∀x. x = x")
+ assert(prettyFormula(ConnectorFormula(And, Seq(BinderFormula(Forall, x, b), a))) == "(∀x. b) ∧ a")
+ assert(prettyFormula(ConnectorFormula(And, Seq(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, b))), a))) == "(a ∧ ∀x. b) ∧ a")
+ assert(prettyFormula(ConnectorFormula(Or, Seq(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, b))), a))) == "a ∧ (∀x. b) ∨ a")
+
+ assert(prettyFormula(BinderFormula(Forall, x, BinderFormula(Exists, y, BinderFormula(ExistsOne, z, a)))) == "∀x. ∃y. ∃!z. a")
+
+ assert(prettyFormula(PredicateFormula(ConstantPredicateLabel("f", 2), Seq(x, y, z))) == "f(x, y, z)")
+ }
+
+}
diff --git a/src/test/scala/lisa/kernel/ProofTests.scala b/src/test/scala/lisa/kernel/ProofTests.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d2a91582516ff99e34a851dcdef73712570788cd
--- /dev/null
+++ b/src/test/scala/lisa/kernel/ProofTests.scala
@@ -0,0 +1,63 @@
+package lisa.kernel
+
+import lisa.KernelHelpers.{*, given}
+import lisa.kernel.Printer
+import lisa.kernel.proof.RunningTheory
+import org.scalatest.funsuite.AnyFunSuite
+import lisa.kernel.proof.SequentCalculus.*
+import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.RunningTheory.*
+import lisa.kernel.proof.{SCProof, SCProofChecker}
+
+import scala.util.Random
+
+
+class ProofTests extends AnyFunSuite {
+ val predicateVerifier = SCProofChecker.checkSCProof
+
+ private val x = VariableLabel("x")
+ private val y = VariableLabel("y")
+ private val z = VariableLabel("z")
+ private val a = PredicateFormula(ConstantPredicateLabel("A", 0), Seq())
+ private val b = PredicateFormula(ConstantPredicateLabel("B", 0), Seq())
+ private val fp = ConstantPredicateLabel("F", 1)
+ val sT = SchematicFunctionLabel("t", 0)
+
+
+ test("Verification of Pierce law") {
+ val s0 = Hypothesis( a |- a, a)
+ val s1 = Weakening(a |- Set(a,b), 0)
+ val s2 = RightImplies(() |- Set(a,a==>b), 1, a, b)
+ val s3 = LeftImplies((a ==> b) ==> a |- a, 2, 0, a ==> b, a)
+ val s4 = RightImplies(() |- (a ==> b) ==> a ==> a, 3, (a ==> b) ==> a, a)
+ val ppl: SCProof = SCProof(IndexedSeq(s0, s1, s2, s3, s4))
+ assert(predicateVerifier(ppl)._1)
+ }
+
+ test("Verification of substitution") {
+ val t0 = Hypothesis(fp(x)|-fp(x), fp(x))
+ val t1 = RightSubstEq(Set(fp(x), x === y) |- fp(y), 0, x, y, fp(sT()), sT)
+ val pr = new SCProof(IndexedSeq(t0, t1))
+ assert(predicateVerifier(pr)._1)
+ }
+
+ test("Commutativity on a random large formula") {
+ val k = 9
+ val r = new Random()
+ val vars = (0 until 1 << k).map(i => PredicateFormula(ConstantPredicateLabel(s"P$i", 0), Seq()))
+
+ val pairs = vars.grouped(2)
+ val sPairs = vars.grouped(2)
+ var subformulas = pairs.map(p => or(p.head, p.last)).grouped(2)
+ var subformulasSwapped = sPairs.map(p => if (r.nextBoolean()) or(p.head, p.last) else or(p.last, p.head)).grouped(2)
+ for (i <- 1 until k) {
+ val op = if (i % 2 == 0) or _ else and _
+ subformulas = subformulas.map(sf => op(sf.head, sf.last)).grouped(2)
+ subformulasSwapped = subformulasSwapped.map(sf => if (r.nextBoolean()) op(sf.head, sf.last) else op(sf.last, sf.head)).grouped(2)
+ }
+ val orig = subformulas.next().head
+ val swapped = subformulasSwapped.next().head
+ val prf = SCProof(Vector(Hypothesis(Sequent(Set(orig), Set(orig)), orig), Rewrite(Sequent(Set(orig), Set(swapped)), 0)))
+ assert(predicateVerifier(prf)._1)
+ }
+}
diff --git a/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala b/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala
new file mode 100644
index 0000000000000000000000000000000000000000..efdbd45fa6a0d46617264e4882f3eaaa7b6b95f0
--- /dev/null
+++ b/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala
@@ -0,0 +1,76 @@
+package proven
+
+import lisa.kernel.Printer
+import lisa.settheory.AxiomaticSetTheory.*
+import test.ProofCheckerSuite
+import proven.tactics.ProofTactics
+import lisa.kernel.proof.SCProof
+
+class ElementsOfSetTheoryTests extends ProofCheckerSuite {
+ import proven.ElementsOfSetTheory.*
+ import lisa.kernel.proof.SequentCalculus.Sequent
+ import lisa.kernel.fol.FOL.*
+ import lisa.KernelHelpers.{*, given}
+ import lisa.kernel.proof.SequentCalculus.*
+
+ test("Verification of the proof of symmetry of the pair") {
+ checkProof(proofUnorderedPairSymmetry, emptySeq +> forall(vl, forall(ul, pair(u, v) === pair(v, u))))
+ }
+
+ test("Verification of the proof of deconstruction of the unordered pair") {
+ checkProof(proofUnorderedPairDeconstruction, emptySeq +>
+ forall(sl, forall(tl, forall(ul, forall(vl,
+ (pair(s, t) === pair(xp, v)) ==>
+ (((VariableTerm(v) === t) /\ (VariableTerm(u) === s)) \/ ((VariableTerm(s) === v) /\ (VariableTerm(t) === u)))))))
+ )
+ }
+
+ // forall x, y. (x in {y, y}) <=> (x = y)
+ val singletonSetEqualityProof: SCProof = {
+ val t0 = SCSubproof({
+ val t0 = Rewrite(()|-pairAxiom, -1)
+ val p0 = ProofTactics.instantiateForall(SCProof(IndexedSeq(t0), IndexedSeq(()|-pairAxiom)), t0.bot.right.head, y)
+ val p1 = ProofTactics.instantiateForall(p0, p0.conclusion.right.head, y)
+ val p2:SCProof = ProofTactics.instantiateForall(p1, p1.conclusion.right.head, x)
+ p2
+ } )
+
+ // |- f <=> (f \/ f)
+ def selfIffOr(f: Formula): SCSubproof = SCSubproof({
+ val t0 = Hypothesis(Sequent(Set(f), Set(f)), f)
+ val t1 = RightOr(Sequent(Set(f), Set(f \/ f)), 0, f, f)
+ val t2 = LeftOr(Sequent(Set(f \/ f), Set(f)), Seq(0, 0), Seq(f, f))
+ val t3 = RightImplies(Sequent(Set(), Set(f ==> (f \/ f))), 1, f, f \/ f)
+ val t4 = RightImplies(Sequent(Set(), Set((f \/ f) ==> f)), 2, f \/ f, f)
+ val t5 = RightIff(Sequent(Set(), Set(f <=> (f \/ f))), 3, 4, f, f \/ f)
+ SCProof(IndexedSeq(t0, t1, t2, t3, t4, t5))
+ })
+
+ val t1 = selfIffOr(y === x)
+
+ val xy = x === x
+ val h = SchematicPredicateLabel("h", 0)
+ val t2 = RightSubstIff(Sequent(Set((xy \/ xy) <=> xy), Set(xy <=> in(x, pair(y, y)))), 0,
+ (y === x) \/ (y === x),
+ y === x,
+ in(x, pair(y, y)) <=> PredicateFormula(h, Seq.empty),
+ h)
+ val t3 = Cut(Sequent(Set(), Set(xy <=> in(x, pair(y, y)))), 1, 2, (xy \/ xy) <=> xy)
+
+ val p0 = SCProof(IndexedSeq(t0, t1, t2, t3))
+
+ ProofTactics.generalizeToForall(ProofTactics.generalizeToForall(p0, ul), vl)
+ }
+
+ test("Singleton set equality") {
+ checkProof(singletonSetEqualityProof, emptySeq +> forall(vl, forall(ul, (u === v) <=> in(u, pair(v, v)))))
+ }
+
+ val proofSingletonDefinition: SCProof = ProofTactics.simpleFunctionDefinition(singleton, pair(u, u), Seq(ul))
+
+ test("Verify singleton set definition") {
+ checkProof(proofSingletonDefinition)
+ }
+
+
+}
diff --git a/src/test/scala/lisa/proven/SimpleProverTests.scala b/src/test/scala/lisa/proven/SimpleProverTests.scala
new file mode 100644
index 0000000000000000000000000000000000000000..8f88cc953bed2e22bcb571b011f690d4bd645244
--- /dev/null
+++ b/src/test/scala/lisa/proven/SimpleProverTests.scala
@@ -0,0 +1,32 @@
+package proven
+
+import lisa.kernel.Printer.*
+import lisa.kernel.proof.{RunningTheory, SCProofChecker}
+import lisa.kernel.fol.FOL.*
+import lisa.KernelHelpers.*
+import lisa.kernel.Printer
+import lisa.kernel.proof.RunningTheory.PredicateLogic
+import org.scalatest.funsuite.AnyFunSuite
+import tptp.ProblemGatherer.getPRPproblems
+import tptp.KernelParser.*
+import proven.tactics.SimplePropositionalSolver as SPS
+
+
+class SimpleProverTests extends AnyFunSuite {
+
+ test("Simple propositional logic proofs") {
+ val problems = getPRPproblems.take(1)
+
+ problems.foreach( pr => {
+ println("--- Problem "+pr.file)
+ val sq = problemToSequent(pr)
+ println(prettySequent(sq))
+ val proof = SPS.solveSequent(sq)
+ if (!Seq("Unsatisfiable", "Theorem", "Satisfiable").contains(pr.status)) println("Unknown status: "+pr.status+", "+pr.file)
+
+ assert(SCProofChecker.checkSCProof(proof)._1 == (pr.status =="Unsatisfiable" || pr.status == "Theorem"))
+
+ })
+
+ }
+}
diff --git a/src/test/scala/test/ProofCheckerSuite.scala b/src/test/scala/test/ProofCheckerSuite.scala
new file mode 100644
index 0000000000000000000000000000000000000000..df8786aac3c0d1722d32f116de201259402add4b
--- /dev/null
+++ b/src/test/scala/test/ProofCheckerSuite.scala
@@ -0,0 +1,37 @@
+package test
+
+import lisa.kernel.Printer
+import lisa.kernel.proof.SequentCalculus.{Sequent, isSameSequent}
+import lisa.kernel.proof.SCProofChecker._
+import lisa.settheory.AxiomaticSetTheory
+import org.scalatest.funsuite.AnyFunSuite
+import lisa.kernel.proof.SCProof
+import lisa.KernelHelpers._
+import lisa.KernelHelpers.given_Conversion_Boolean_List_String_Option
+
+abstract class ProofCheckerSuite extends AnyFunSuite {
+ import lisa.kernel.fol.FOL.*
+
+ protected val (xl, yl, zl, wl, xpl, ypl, zpl, wpl) = (SchematicFunctionLabel("x", 0), SchematicFunctionLabel("y", 0), SchematicFunctionLabel("z", 0), SchematicFunctionLabel("w", 0), SchematicFunctionLabel("x'", 0), SchematicFunctionLabel("y'", 0), SchematicFunctionLabel("z'", 0), SchematicFunctionLabel("w'", 0))
+ protected val (x, y, z, w, xp, yp, zp, wp) = (FunctionTerm(xl, Seq.empty), FunctionTerm(yl, Seq.empty), FunctionTerm(zl, Seq.empty), FunctionTerm(wl, Seq.empty), FunctionTerm(xpl, Seq.empty), FunctionTerm(ypl, Seq.empty), FunctionTerm(zpl, Seq.empty), FunctionTerm(wpl, Seq.empty))
+
+ protected val (sl, tl, ul, vl) = (VariableLabel("s"), VariableLabel("t"), VariableLabel("u"), VariableLabel("v"))
+ protected val (s, t, u, v) = (VariableTerm(sl), VariableTerm(tl), VariableTerm(ul), VariableTerm(vl))
+
+ val axioms = AxiomaticSetTheory.axioms
+ def checkProof(proof: SCProof): Unit = {
+ val error = checkSCProof(proof)
+ println(Printer.prettySCProof(proof, error))
+ println(s"\n(${proof.totalLength} proof steps in total)")
+ }
+
+ def checkProof(proof: SCProof, expected: Sequent): Unit = {
+ val error = checkSCProof(proof)
+ assert(error._1, "\n"+Printer.prettySCProof(proof, error))
+ assert(isSameSequent(proof.conclusion, expected), s"(${Printer.prettySequent(proof.conclusion)} did not equal ${Printer.prettySequent(expected)})")
+ }
+
+ def checkIncorrectProof(incorrectProof: SCProof): Unit = {
+ assert(!checkSCProof(incorrectProof)._1, s"(incorrect proof with conclusion '${Printer.prettySequent(incorrectProof.conclusion)}' was accepted by the proof checker)\nSequent: ${incorrectProof.conclusion}")
+ }
+}