From 0de11974daaa052b0c1349531211638cd1c5b7e7 Mon Sep 17 00:00:00 2001
From: SimonGuilloud <sim-guilloud@bluewin.ch>
Date: Tue, 15 Feb 2022 18:33:13 +0100
Subject: [PATCH] Initial Commit
This is the initial alpha release of LISA 0.1. It contains a Kernel suitable to represent and manipulate First Order Logic, Proofs in Sequent Calculus and mathematical Theories.
It also contains some development of proof tactics and some early theorems of set theory, a parser for TPTP problems and other less significant features.
This release also include a test suite for those elements.
---
README.md | 16 +
build.sbt | 19 +
project/build.properties | 1 +
project/plugins.sbt | 1 +
src/main/scala/Example.scala | 163 +++++++
src/main/scala/lisa/KernelHelpers.scala | 81 ++++
src/main/scala/lisa/kernel/Printer.scala | 281 +++++++++++
.../lisa/kernel/fol/CommonDefinitions.scala | 28 ++
.../lisa/kernel/fol/EquivalenceChecker.scala | 335 +++++++++++++
src/main/scala/lisa/kernel/fol/FOL.scala | 12 +
.../lisa/kernel/fol/FormulaDefinitions.scala | 159 +++++++
.../kernel/fol/FormulaLabelDefinitions.scala | 86 ++++
.../lisa/kernel/fol/TermDefinitions.scala | 100 ++++
.../kernel/fol/TermLabelDefinitions.scala | 70 +++
.../lisa/kernel/proof/RunningTheory.scala | 276 +++++++++++
.../scala/lisa/kernel/proof/SCProof.scala | 98 ++++
.../lisa/kernel/proof/SCProofChecker.scala | 441 ++++++++++++++++++
.../lisa/kernel/proof/SequentCalculus.scala | 286 ++++++++++++
.../lisa/settheory/AxiomaticSetTheory.scala | 8 +
.../lisa/settheory/SetTheoryDefinitions.scala | 39 ++
.../lisa/settheory/SetTheoryTGAxioms.scala | 19 +
.../lisa/settheory/SetTheoryZAxioms.scala | 29 ++
.../lisa/settheory/SetTheoryZFAxioms.scala | 16 +
.../scala/proven/ElementsOfSetTheory.scala | 346 ++++++++++++++
.../scala/proven/tactics/Destructors.scala | 31 ++
.../scala/proven/tactics/ProofTactics.scala | 156 +++++++
.../tactics/SimplePropositionalSolver.scala | 173 +++++++
src/main/scala/tptp/KernelParser.scala | 238 ++++++++++
src/main/scala/tptp/ProblemGatherer.scala | 16 +
.../lisa/kernel/EquivalenceCheckerTests.scala | 332 +++++++++++++
src/test/scala/lisa/kernel/FolTests.scala | 126 +++++
.../lisa/kernel/IncorrectProofsTests.scala | 97 ++++
src/test/scala/lisa/kernel/PrinterTest.scala | 43 ++
src/test/scala/lisa/kernel/ProofTests.scala | 63 +++
.../proven/ElementsOfSetTheoryTests.scala | 76 +++
.../scala/lisa/proven/SimpleProverTests.scala | 32 ++
src/test/scala/test/ProofCheckerSuite.scala | 37 ++
37 files changed, 4330 insertions(+)
create mode 100644 build.sbt
create mode 100644 project/build.properties
create mode 100644 project/plugins.sbt
create mode 100644 src/main/scala/Example.scala
create mode 100644 src/main/scala/lisa/KernelHelpers.scala
create mode 100644 src/main/scala/lisa/kernel/Printer.scala
create mode 100644 src/main/scala/lisa/kernel/fol/CommonDefinitions.scala
create mode 100644 src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
create mode 100644 src/main/scala/lisa/kernel/fol/FOL.scala
create mode 100644 src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
create mode 100644 src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
create mode 100644 src/main/scala/lisa/kernel/fol/TermDefinitions.scala
create mode 100644 src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala
create mode 100644 src/main/scala/lisa/kernel/proof/RunningTheory.scala
create mode 100644 src/main/scala/lisa/kernel/proof/SCProof.scala
create mode 100644 src/main/scala/lisa/kernel/proof/SCProofChecker.scala
create mode 100644 src/main/scala/lisa/kernel/proof/SequentCalculus.scala
create mode 100644 src/main/scala/lisa/settheory/AxiomaticSetTheory.scala
create mode 100644 src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
create mode 100644 src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
create mode 100644 src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
create mode 100644 src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
create mode 100644 src/main/scala/proven/ElementsOfSetTheory.scala
create mode 100644 src/main/scala/proven/tactics/Destructors.scala
create mode 100644 src/main/scala/proven/tactics/ProofTactics.scala
create mode 100644 src/main/scala/proven/tactics/SimplePropositionalSolver.scala
create mode 100644 src/main/scala/tptp/KernelParser.scala
create mode 100644 src/main/scala/tptp/ProblemGatherer.scala
create mode 100644 src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
create mode 100644 src/test/scala/lisa/kernel/FolTests.scala
create mode 100644 src/test/scala/lisa/kernel/IncorrectProofsTests.scala
create mode 100644 src/test/scala/lisa/kernel/PrinterTest.scala
create mode 100644 src/test/scala/lisa/kernel/ProofTests.scala
create mode 100644 src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala
create mode 100644 src/test/scala/lisa/proven/SimpleProverTests.scala
create mode 100644 src/test/scala/test/ProofCheckerSuite.scala
diff --git a/README.md b/README.md
index 1010401b..be8c88f4 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 00000000..ea69a270
--- /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 00000000..8378cad5
--- /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 00000000..7bc4622d
--- /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 00000000..4e59959d
--- /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 00000000..afa8008b
--- /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 00000000..752eb43f
--- /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 00000000..054b4aaf
--- /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 00000000..a4f79c52
--- /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 00000000..6f09ba07
--- /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 00000000..8e1e772b
--- /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 00000000..81de8601
--- /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 00000000..03411af8
--- /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 00000000..288c27c1
--- /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 00000000..49a4688b
--- /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 00000000..62573bc8
--- /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 00000000..bb475952
--- /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 00000000..cf795433
--- /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 00000000..377d64b6
--- /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 00000000..bf8b7bf4
--- /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 00000000..c1a92a89
--- /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 00000000..da30c878
--- /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 00000000..2b77f013
--- /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 00000000..a1bf44de
--- /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 00000000..12c080e8
--- /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 00000000..85c576fc
--- /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 00000000..86f9d7fb
--- /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 00000000..cca3ff4f
--- /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 00000000..5fb31992
--- /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 00000000..68a5fa28
--- /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 00000000..c5f3b6f3
--- /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 00000000..9c7c1515
--- /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 00000000..23edf5a2
--- /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 00000000..d2a91582
--- /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 00000000..efdbd45f
--- /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 00000000..8f88cc95
--- /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 00000000..df8786aa
--- /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}")
+ }
+}
--
GitLab