From 8d13de42a9ec2efa0c717f5781708dbf4eb9b5aa Mon Sep 17 00:00:00 2001
From: SimonGuilloud <simon.guilloud@bluewin.ch>
Date: Mon, 24 Oct 2022 14:21:38 +0200
Subject: [PATCH] New tactic system (#73)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
New tactic system
Proofs can now be written using dedicated tactics and deduced steps. Tactics can be developped as object from which a SCProof can be recomputed.
Management of premises and target bottom sequent is unified, but tactics can optionally take other arguments.
Tactics can be used to construct proof using a dedicated syntax and DSL. Formally, The proof is built imperatively.
This means it is possible to write code in the middle of the proof (for example to print it) and it is possible to assign proof steps.
The library keep track of the proof being written from start to finish. A proof may look like:
```
THEOREM("fixedPointDoubleApplication") of "∀'x. 'P('x) ⇒ 'P('f('x)) ⊢ 'P('x) ⇒ 'P('f('f('x)))" PROOF {
assume(forall(x, P(x) ==> P(f(x))))
val base = have( (P(x) ==> P(f(x)), P(f(x)) ==> P(f(f(x)))) |- P(x) ==> P(f(f(x)))) by Trivial
have(() |- P(x) ==> P(f(f(x)))) by SUBPROOF {
have(P(f(x)) ==> P(f(f(x))) |- P(x) ==> P(f(f(x))) ) by LeftForall(x)(base)
andThen(() |- P(x) ==> P(f(f(x)))) by LeftForall(f(x))
}
}
```
Sequent Calculus proof steps have been adapted so that they need only the minimum (often zero) explicit parameters, whcih are automatically infered.
Subproofs can also be used, and there is no need to do import management. Imports of Justifications and of proof steps of enclosing proofs are
automatically passed through the imports.
User should not use integers anymore to refer to premises, but instead provide a previous proof step or a justification directly.
On top of basic sequent calculus steps, the naive propositional solver and a tactic to instantiate forall quantifiers.
Existing proof have been translated to old sequent calculus (with every step lead by SC.) to make room for the new tactics identifiers.
---
lisa-examples/src/main/scala/Example.scala | 37 +-
.../main/scala/lisa/utils/KernelHelpers.scala | 18 +
.../src/main/scala/lisa/utils/Library.scala | 92 +-
.../scala/lisa/utils/TheoriesHelpers.scala | 20 +
.../lisa/utils/tactics/BasicStepTactic.scala | 965 ++++++++++++++++++
.../utils/tactics/ProofStepJudgement.scala | 44 +
.../lisa/utils/tactics/ProofStepLib.scala | 143 +++
.../lisa/utils/tactics/ProofsHelpers.scala | 134 +++
.../utils/tactics/SimpleDeducedSteps.scala | 438 ++++++++
.../scala/lisa/utils/tactics/WithProofs.scala | 255 +++++
.../kernel/SimplePropositionalSolver.scala | 31 +-
.../lisa/proven/mathematics/Mapping.scala | 300 +++---
.../lisa/proven/mathematics/SetTheory.scala | 236 ++---
.../lisa/proven/peano_example/Peano.scala | 149 +--
.../lisa/utilities/Transformations.scala | 8 +-
15 files changed, 2482 insertions(+), 388 deletions(-)
create mode 100644 lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala
create mode 100644 lisa-utils/src/main/scala/lisa/utils/tactics/ProofStepJudgement.scala
create mode 100644 lisa-utils/src/main/scala/lisa/utils/tactics/ProofStepLib.scala
create mode 100644 lisa-utils/src/main/scala/lisa/utils/tactics/ProofsHelpers.scala
create mode 100644 lisa-utils/src/main/scala/lisa/utils/tactics/SimpleDeducedSteps.scala
create mode 100644 lisa-utils/src/main/scala/lisa/utils/tactics/WithProofs.scala
diff --git a/lisa-examples/src/main/scala/Example.scala b/lisa-examples/src/main/scala/Example.scala
index d494a522..00a566cf 100644
--- a/lisa-examples/src/main/scala/Example.scala
+++ b/lisa-examples/src/main/scala/Example.scala
@@ -1,22 +1,25 @@
import lisa.Main
+import lisa.automation.kernel.SimplePropositionalSolver.*
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SCProofChecker
import lisa.kernel.proof.SCProofChecker.*
import lisa.kernel.proof.SequentCalculus.*
-import lisa.automation.kernel.SimplePropositionalSolver.solveSequent
import lisa.tptp.KernelParser.*
import lisa.tptp.ProblemGatherer.*
import lisa.tptp.*
+import lisa.utils.Helpers.show
import lisa.utils.Helpers.{_, given}
import lisa.utils.Printer.*
+import lisa.utils.tactics.ProofStepLib.ProofStep
/**
* Discover some of the elements of LISA to get started.
*/
object Example {
def main(args: Array[String]): Unit = {
- //proofExample() // uncomment when exercise finished
+
+ proofExample() // uncomment when exercise finished
// solverExample()
// tptpExample()
}
@@ -27,23 +30,20 @@ object Example {
* The last two lines don't need to be changed.
*/
def proofExample(): Unit = {
+
object Ex extends Main {
- THEOREM("fixedPointDoubleApplication") of "" PROOF {
- steps(
- ???,
- ???,
- ?????(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)
- )
- } using ()
- show
+ THEOREM("fixedPointDoubleApplication") of "∀'x. 'P('x) ⇒ 'P('f('x)) ⊢ 'P('x) ⇒ 'P('f('f('x)))" PROOF {
+ assume(forall(x, P(x) ==> P(f(x))))
+ val base = have((P(x) ==> P(f(x)), P(f(x)) ==> P(f(f(x)))) |- P(x) ==> P(f(f(x)))) by Trivial
+ have(() |- P(x) ==> P(f(f(x)))) by SUBPROOF {
+ have(P(f(x)) ==> P(f(f(x))) |- P(x) ==> P(f(f(x)))) by LeftForall(x)(base)
+ andThen(() |- P(x) ==> P(f(f(x)))) by LeftForall(f(x))
+ }
+ }
+ show
}
+
Ex.main(Array(""))
}
@@ -149,8 +149,11 @@ object Example {
val A = PredicateFormula(VariableFormulaLabel("A"), Seq())
val B = PredicateFormula(VariableFormulaLabel("B"), Seq())
val C = PredicateFormula(VariableFormulaLabel("C"), Seq())
+ val H = VariableFormulaLabel("H")
val x = VariableLabel("x")
- val f = ConstantFunctionLabel("f", 1)
+ val y = VariableLabel("y")
+ val z = VariableLabel("z")
+ val f = SchematicFunctionLabel("f", 1)
def ???? : Formula = ???
def ?????(args: Any*) = ???
diff --git a/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala b/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
index 56981317..16af6f19 100644
--- a/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
@@ -6,6 +6,9 @@ import lisa.kernel.proof.RunningTheoryJudgement.InvalidJustification
import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SCProofCheckerJudgement.SCInvalidProof
import lisa.kernel.proof.SequentCalculus.*
+import lisa.utils.Parser.parseFormula
+import lisa.utils.Parser.parseSequent
+import lisa.utils.Parser.parseTerm
/**
* A helper file that provides various syntactic sugars for LISA's FOL and proofs. Best imported through utilities.Helpers
@@ -181,4 +184,19 @@ trait KernelHelpers {
|(step ${judgement.path.mkString("->")}): ${judgement.message}""".stripMargin
}
+ implicit class Parsing(val sc: StringContext) {
+
+ def seq(args: Any*): Sequent = parseSequent(sc.parts.mkString(""))
+
+ def f(args: Any*): Formula = parseFormula(sc.parts.mkString(""))
+
+ def t(args: Any*): Term = parseTerm(sc.parts.mkString(""))
+
+ }
+
+ given Conversion[String, Sequent] = parseSequent(_)
+ given Conversion[String, Formula] = parseFormula(_)
+ given Conversion[String, Term] = parseTerm(_)
+ given Conversion[String, VariableLabel] = s => VariableLabel(if (s.head == '?') s.tail else s)
+
}
diff --git a/lisa-utils/src/main/scala/lisa/utils/Library.scala b/lisa-utils/src/main/scala/lisa/utils/Library.scala
index cfcb6846..5acd4867 100644
--- a/lisa-utils/src/main/scala/lisa/utils/Library.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/Library.scala
@@ -1,17 +1,25 @@
package lisa.utils
import lisa.kernel.proof.RunningTheory
+import lisa.kernel.proof.SCProofChecker
+import lisa.kernel.proof.SCProofCheckerJudgement
+import lisa.kernel.proof.SequentCalculus
+import lisa.utils.tactics.ProofStepLib.ProofStep
+
+import scala.collection.mutable.Stack as stack
/**
* A class abstracting a [[lisa.kernel.proof.RunningTheory]] providing utility functions and a convenient syntax
* to write and use Theorems and Definitions.
* @param theory The inner RunningTheory
*/
-abstract class Library(val theory: RunningTheory) {
+abstract class Library(val theory: RunningTheory) extends lisa.utils.tactics.WithProofs {
+ val library: Library = this
given RunningTheory = theory
- export lisa.kernel.fol.FOL.*
- export lisa.kernel.proof.SequentCalculus.*
- export lisa.kernel.proof.SCProof as Proof
+ export lisa.kernel.fol.FOL.{Formula, *}
+ val SC: SequentCalculus.type = lisa.kernel.proof.SequentCalculus
+ export lisa.kernel.proof.SequentCalculus.{Sequent, SCProofStep}
+ export lisa.kernel.proof.SCProof
export theory.{Justification, Theorem, Definition, Axiom, PredicateDefinition, FunctionDefinition}
export lisa.utils.Helpers.{_, given}
import lisa.kernel.proof.RunningTheoryJudgement as Judgement
@@ -23,16 +31,19 @@ abstract class Library(val theory: RunningTheory) {
private var last: Option[Justification] = None
+ val proofStack: stack[Proof] = stack()
+
/**
* A function intended for use to construct a proof:
- * <pre> Proof(steps(...), imports(...))</pre>
+ * <pre> SCProof(steps(...), imports(...))</pre>
* Must contains [[SCProofStep]]'s
*/
inline def steps(sts: SCProofStep*): IndexedSeq[SCProofStep] = sts.toIndexedSeq
+ inline def Nsteps(sts: ProofStep*): IndexedSeq[ProofStep] = sts.toIndexedSeq
/**
* A function intended for use to construct a proof:
- * <pre> Proof(steps(...), imports(...))</pre>
+ * <pre> SCProof(steps(...), imports(...))</pre>
* Must contains [[Justification]]'s, [[Formula]]'s or [[Sequent]], all of which are converted adequatly automatically.
*/
inline def imports(sqs: Sequentable*): IndexedSeq[Sequent] = sqs.map(sequantableToSequent).toIndexedSeq
@@ -42,7 +53,7 @@ abstract class Library(val theory: RunningTheory) {
/**
* An alias to create a Theorem
*/
- def makeTheorem(name: String, statement: String, proof: Proof, justifications: Seq[theory.Justification]): Judgement[theory.Theorem] =
+ def makeTheorem(name: String, statement: String, proof: SCProof, justifications: Seq[theory.Justification]): Judgement[theory.Theorem] =
theory.theorem(name, statement, proof, justifications)
/**
@@ -53,12 +64,28 @@ abstract class Library(val theory: RunningTheory) {
/**
* Syntax: <pre> THEOREM("name") of "the sequent concluding the proof" PROOF { the proof } using (assumptions) </pre>
*/
- def PROOF(proof: Proof)(using String => Unit)(using Throwable => Nothing): TheoremNameWithProof = TheoremNameWithProof(name, statement, proof)
+ def PROOF2(proof: SCProof)(using String => Unit)(using finishOutput: Throwable => Nothing): TheoremNameWithProof = TheoremNameWithProof(name, statement, proof)
/**
* Syntax: <pre> THEOREM("name") of "the sequent concluding the proof" PROOF { the proof } using (assumptions) </pre>
*/
- def PROOF(steps: IndexedSeq[SCProofStep])(using String => Unit)(using Throwable => Nothing): TheoremNameWithProof = TheoremNameWithProof(name, statement, Proof(steps))
+ def PROOF2(steps: IndexedSeq[SCProofStep])(using String => Unit)(using finishOutput: Throwable => Nothing): TheoremNameWithProof =
+ TheoremNameWithProof(name, statement, SCProof(steps))
+
+ def PROOF(computeProof: => Unit)(using String => Unit)(using finishOutput: Throwable => Nothing): theory.Theorem = {
+ require(proofStack.isEmpty) // TODO: More explicit error
+ proofStack.push(if (proofStack.isEmpty) new Proof() else new Proof(proofStack.head.getAssumptions))
+ computeProof
+ val r = TheoremNameWithProof(name, statement, proofStack.head.toSCProof)
+ val r2 = theory.theorem(r.name, r.statement, r.proof, proofStack.head.getImports.map(_.reference.asInstanceOf[theory.Justification])) match {
+ case Judgement.ValidJustification(just) =>
+ last = Some(just)
+ just
+ case wrongJudgement: Judgement.InvalidJustification[?] => wrongJudgement.showAndGet
+ }
+ proofStack.pop
+ r2
+ }
}
/**
@@ -80,7 +107,7 @@ abstract class Library(val theory: RunningTheory) {
/**
* Syntax: <pre> THEOREM("name") of "the sequent concluding the proof" PROOF { the proof } using (assumptions) </pre>
*/
- case class TheoremNameWithProof(name: String, statement: String, proof: Proof)(using String => Unit)(using Throwable => Nothing) {
+ case class TheoremNameWithProof(name: String, statement: String, proof: SCProof)(using String => Unit)(using Throwable => Nothing) {
infix def using(justifications: theory.Justification*): theory.Theorem = theory.theorem(name, statement, proof, justifications) match {
case Judgement.ValidJustification(just) =>
last = Some(just)
@@ -101,21 +128,22 @@ abstract class Library(val theory: RunningTheory) {
*/
def simpleDefinition(symbol: String, expression: LambdaTermTerm): Judgement[theory.FunctionDefinition] = {
val LambdaTermTerm(vars, body) = expression
+
val out: VariableLabel = VariableLabel(freshId((vars.map(_.id) ++ body.schematicTermLabels.map(_.id)).toSet, "y"))
- val proof: Proof = simpleFunctionDefinition(expression, out)
+ val proof: SCProof = simpleFunctionDefinition(expression, out)
theory.functionDefinition(symbol, LambdaTermFormula(vars, out === body), out, proof, Nil)
}
/**
* Allows to create a definition by existential uniqueness of a function symbol:
*/
- def complexDefinition(symbol: String, vars: Seq[VariableLabel], v: VariableLabel, f: Formula, proof: Proof, just: Seq[Justification]): Judgement[theory.FunctionDefinition] = {
+ def complexDefinition(symbol: String, vars: Seq[VariableLabel], v: VariableLabel, f: Formula, proof: SCProof, just: Seq[Justification]): Judgement[theory.FunctionDefinition] = {
theory.functionDefinition(symbol, LambdaTermFormula(vars, f), v, proof, just)
// theory.functionDefinition(symbol, LambdaTermFormula(vars, instantiateTermSchemas(f, Map(v -> LambdaTermTerm(Nil, out)))), out, proof, just)
}
/**
- * Allows to create a definition by shortcut of a function symbol:
+ * Allows to create a definition by shortcut of a predicate symbol:
*/
def simpleDefinition(symbol: String, expression: LambdaTermFormula): Judgement[theory.PredicateDefinition] =
theory.predicateDefinition(symbol, expression)
@@ -130,7 +158,7 @@ abstract class Library(val theory: RunningTheory) {
/**
* Syntax: <pre> DEFINE("symbol", arguments) as "definition" </pre>
*/
- infix def as(t: Term)(using String => Unit)(using Throwable => Nothing): ConstantFunctionLabel = {
+ infix def as(t: Term)(using String => Unit)(using finishOutput: Throwable => Nothing): ConstantFunctionLabel = {
val definition = simpleDefinition(symbol, LambdaTermTerm(vars, t)) match {
case Judgement.ValidJustification(just) =>
last = Some(just)
@@ -143,7 +171,7 @@ abstract class Library(val theory: RunningTheory) {
/**
* Syntax: <pre> DEFINE("symbol", arguments) as "definition" </pre>
*/
- infix def as(f: Formula)(using String => Unit)(using Throwable => Nothing): ConstantPredicateLabel = {
+ infix def as(f: Formula)(using String => Unit)(using finishOutput: Throwable => Nothing): ConstantPredicateLabel = {
val definition = simpleDefinition(symbol, LambdaTermFormula(vars, f)) match {
case Judgement.ValidJustification(just) =>
last = Some(just)
@@ -178,18 +206,18 @@ abstract class Library(val theory: RunningTheory) {
/**
* Syntax: <pre> DEFINE("symbol", arguments) asThe x suchThat P(x) PROOF { the proof } using (assumptions) </pre>
*/
- infix def PROOF(proof: Proof): DefinitionWithProof = DefinitionWithProof(symbol, vars, out, f, proof)
+ infix def PROOF(proof: SCProof): DefinitionWithProof = DefinitionWithProof(symbol, vars, out, f, proof)
}
/**
* Syntax: <pre> DEFINE("symbol", arguments) asThe x suchThat P(x) PROOF { the proof } using (assumptions) </pre>
*/
- case class DefinitionWithProof(symbol: String, vars: Seq[VariableLabel], out: VariableLabel, f: Formula, proof: Proof) {
+ case class DefinitionWithProof(symbol: String, vars: Seq[VariableLabel], out: VariableLabel, f: Formula, proof: SCProof) {
/**
* Syntax: <pre> DEFINE("symbol", arguments) asThe x suchThat P(x) PROOF { the proof } using (assumptions) </pre>
*/
- infix def using(justifications: theory.Justification*)(using String => Unit)(using Throwable => Nothing): ConstantFunctionLabel = {
+ infix def using(justifications: theory.Justification*)(using String => Unit)(using finishOutput: Throwable => Nothing): ConstantFunctionLabel = {
val definition = complexDefinition(symbol, vars, out, f, proof, justifications) match {
case Judgement.ValidJustification(just) =>
last = Some(just)
@@ -202,7 +230,7 @@ abstract class Library(val theory: RunningTheory) {
/**
* Syntax: <pre> DEFINE("symbol", arguments) asThe x suchThat P(x) PROOF { the proof } using (assumptions) </pre>
*/
- infix def using(u: Unit)(using String => Unit)(using Throwable => Nothing): ConstantFunctionLabel = using()
+ infix def using(u: Unit)(using String => Unit)(using finishOutput: Throwable => Nothing): ConstantFunctionLabel = using()
}
/**
@@ -213,21 +241,23 @@ abstract class Library(val theory: RunningTheory) {
/**
* For a definition of the type f(x) := term, construct the required proof ?!y. y = term.
*/
- private def simpleFunctionDefinition(expression: LambdaTermTerm, out: VariableLabel): Proof = {
+ private def simpleFunctionDefinition(expression: LambdaTermTerm, out: VariableLabel): SCProof = {
val x = out
val LambdaTermTerm(vars, body) = expression
val xeb = x === body
val y = VariableLabel(freshId(body.freeVariables.map(_.id) ++ vars.map(_.id) + out.id, "y"))
- val s0 = RightRefl(() |- body === body, body === body)
- val s1 = Rewrite(() |- (xeb) <=> (xeb), 0)
- val s2 = RightForall(() |- forall(x, (xeb) <=> (xeb)), 1, (xeb) <=> (xeb), x)
- val s3 = RightExists(() |- exists(y, forall(x, (x === y) <=> (xeb))), 2, forall(x, (x === y) <=> (xeb)), y, body)
- val s4 = Rewrite(() |- existsOne(x, xeb), 3)
+ val s0 = SC.RightRefl(() |- body === body, body === body)
+ val s1 = SC.Rewrite(() |- (xeb) <=> (xeb), 0)
+ val s2 = SC.RightForall(() |- forall(x, (xeb) <=> (xeb)), 1, (xeb) <=> (xeb), x)
+ val s3 = SC.RightExists(() |- exists(y, forall(x, (x === y) <=> (xeb))), 2, forall(x, (x === y) <=> (xeb)), y, body)
+ val s4 = SC.Rewrite(() |- existsOne(x, xeb), 3)
val v = Vector(s0, s1, s2, s3, s4)
- Proof(v)
+ SCProof(v)
}
- // Implicit conversions
+ //////////////////////////////////////////
+ // Tools for proof development //
+ //////////////////////////////////////////
given Conversion[TheoremNameWithProof, theory.Theorem] = _.using()
@@ -274,7 +304,7 @@ abstract class Library(val theory: RunningTheory) {
/**
* Prints a short representation of the last theorem or definition introduced
*/
- def show(using String => Unit): Justification = last match {
+ def show(using String => Unit)(using finishOutput: Throwable => Nothing): Justification = last match {
case Some(value) => value.show
case None => throw new NoSuchElementException("There is nothing to show: No theorem or definition has been proved yet.")
}
@@ -304,4 +334,10 @@ abstract class Library(val theory: RunningTheory) {
builder.result
}
+ def showCurrentProof()(using output: String => Unit)(using finishOutput: Throwable => Nothing) = {
+ val proof = proofStack.head.toSCProof
+ output(s" Current proof (possibly uncomplete) is:\n${Printer.prettySCProof(proof)}\n")
+
+ }
+
}
diff --git a/lisa-utils/src/main/scala/lisa/utils/TheoriesHelpers.scala b/lisa-utils/src/main/scala/lisa/utils/TheoriesHelpers.scala
index 9f6cfbc4..a115e4c6 100644
--- a/lisa-utils/src/main/scala/lisa/utils/TheoriesHelpers.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/TheoriesHelpers.scala
@@ -108,6 +108,26 @@ trait TheoriesHelpers extends KernelHelpers {
}
}
+ extension (proofJudgement: SCProofCheckerJudgement) {
+
+ /**
+ * If the SCProof is valid, show the inner proof and returns it.
+ * Otherwise, output the error leading to the invalid justification and throw an error.
+ */
+ def showAndGet(using output: String => Unit)(using finishOutput: Throwable => Nothing): SCProof = {
+ proofJudgement match {
+ case SCProofCheckerJudgement.SCValidProof(proof) =>
+ output(Printer.prettySCProof(proofJudgement))
+ proof
+ case ip @ SCProofCheckerJudgement.SCInvalidProof(proof, path, message) =>
+ output(s"$message\n${Printer.prettySCProof(proofJudgement)}")
+ finishOutput(InvalidJustificationException("", Some(ip)))
+ }
+ }
+ }
+
+ case class InvalidProofException(proofJudgement: SCProofCheckerJudgement.SCInvalidProof) extends Exception(proofJudgement.message)
+
/**
* Output a readable representation of a proof.
*/
diff --git a/lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala b/lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala
new file mode 100644
index 00000000..612bd42a
--- /dev/null
+++ b/lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala
@@ -0,0 +1,965 @@
+package lisa.utils.tactics
+
+import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.SCProof
+import lisa.kernel.proof.SequentCalculus.SCProofStep
+import lisa.kernel.proof.SequentCalculus.Sequent
+import lisa.kernel.proof.{SequentCalculus => SC}
+import lisa.utils.Library
+import lisa.utils.tactics.ProofStepLib.{_, given}
+
+object BasicStepTactic {
+
+ case object Hypothesis extends ProofStepWithoutBotNorPrem(0) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ SC.Hypothesis(bot, bot.left.intersect(bot.right).head)
+ }
+
+ case object Rewrite extends ProofStepWithoutBotNorPrem(1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ SC.Rewrite(bot, premises(0))
+ }
+
+ /**
+ * <pre>
+ * Γ |- Δ, φ φ, Σ |- Î
+ * ------------------------
+ * Γ, Σ |-Δ, Î
+ * </pre>
+ */
+ case class Cut(phi: Formula) extends ProofStepWithoutBotNorPrem(2) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ SC.Cut(bot, premises(0), premises(1), phi)
+ }
+
+ case object CutWithoutFormula extends ProofStepWithoutBotNorPrem(2) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ val leftSequent = currentProof.getSequent(premises(0))
+ val rightSequent = currentProof.getSequent(premises(1))
+ val cutSet = rightSequent.left.diff(bot.left) ++ leftSequent.right.diff(bot.right)
+ lazy val intersectedCutSet = rightSequent.left & leftSequent.right
+
+ if (!cutSet.isEmpty)
+ if (cutSet.tail.isEmpty) {
+ SC.Cut(bot, premises(0), premises(1), cutSet.head)
+ } else
+ ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Inferred cut pivot is not a singleton set.")
+ else if (!intersectedCutSet.isEmpty && intersectedCutSet.tail.isEmpty)
+ // can still find a pivot
+ SC.Cut(bot, premises(0), premises(1), intersectedCutSet.head)
+ else
+ ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ "A consistent cut pivot cannot be inferred from the premises. Possibly a missing or extraneous clause."
+ )
+ }
+ }
+
+ case object Cut extends ProofStepWithoutBotNorPrem(2) {
+ // default construction:
+ // def apply(phi: Formula) = new Cut(phi)
+ def apply() = CutWithoutFormula
+
+ // usage without an argument list
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ this().asSCProof(bot, premises, currentProof)
+
+ }
+
+ // Left rules
+ /**
+ * <pre>
+ * Γ, φ |- Δ Γ, φ, ψ |- Δ
+ * -------------- or --------------
+ * Γ, φ∧ψ |- Δ Γ, φ∧ψ |- Δ
+ * </pre>
+ */
+ case class LeftAnd(phi: Formula, psi: Formula) extends ProofStepWithoutBotNorPrem(1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ SC.LeftAnd(bot, premises(0), phi, psi)
+ }
+
+ case object LeftAndWithoutFormula extends ProofStepWithoutBotNorPrem(1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ val premiseSequent = currentProof.getSequent(premises(0))
+ val pivot = bot.left.diff(premiseSequent.left)
+
+ if (!pivot.isEmpty && pivot.tail.isEmpty)
+ pivot.head match {
+ case ConnectorFormula(And, Seq(phi, psi)) =>
+ if (premiseSequent.left.contains(phi))
+ SC.LeftAnd(bot, premises(0), phi, psi)
+ else
+ SC.LeftAnd(bot, premises(0), psi, phi)
+ case _ => ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Could not infer a conjunction as pivot from premise and conclusion.")
+ }
+ else
+ // try a rewrite, if it works, go ahead with it, otherwise malformed
+ if (SC.isSameSequent(premiseSequent, bot))
+ SC.Rewrite(bot, premises(0))
+ else
+ ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ "Left-hand side of conclusion + φ∧ψ must be same as left-hand side of premise + either φ, ψ or both."
+ )
+ }
+ }
+
+ case object LeftAnd extends ProofStepWithoutBotNorPrem(1) {
+ // default construction:
+ // def apply(phi: Formula, psi: Formula) = new LeftAnd(phi, psi)
+ def apply() = LeftAndWithoutFormula
+
+ // usage without an argument list
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ this().asSCProof(bot, premises, currentProof)
+ }
+
+ /**
+ * <pre>
+ * Γ, φ |- Δ Σ, ψ |- Π...
+ * --------------------------------
+ * Γ, Σ, φ∨ψ∨... |- Δ, Î
+ * </pre>
+ */
+ case class LeftOr(disjuncts: Seq[Formula]) extends ProofStepWithoutBotNorPrem(-1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ SC.LeftOr(bot, premises, disjuncts)
+ }
+ }
+ case class LeftOrWithoutFormula() extends ProofStepWithoutBotNorPrem(-1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ val premiseSequents = premises.map(currentProof.getSequent(_))
+ val pivots = premiseSequents.map(_.left.diff(bot.left))
+
+ if (pivots.exists(_.isEmpty))
+ SC.Weakening(bot, premises(pivots.indexWhere(_.isEmpty)))
+ else if (pivots.forall(_.tail.isEmpty))
+ SC.LeftOr(bot, premises, pivots.map(_.head))
+ else
+ // some extraneous formulae
+ ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ "Left-hand side of conclusion + disjuncts is not the same as the union of the left-hand sides of the premises + φ∨ψ."
+ )
+ }
+ }
+
+ case object LeftOr extends ProofStepWithoutBotNorPrem(-1) {
+ // default construction:
+ // def apply(disjuncts: Seq[Formula]) = new LeftOr(disjuncts)
+ def apply() = new LeftOrWithoutFormula()
+
+ // usage without an argument list
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ this().asSCProof(bot, premises, currentProof)
+ }
+
+ /**
+ * <pre>
+ * Γ |- φ, Δ Σ, ψ |- Î
+ * ------------------------
+ * Γ, Σ, φ→ψ |- Δ, Î
+ * </pre>
+ */
+ case class LeftImplies(phi: Formula, psi: Formula) extends ProofStepWithoutBotNorPrem(2) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ SC.LeftImplies(bot, premises(0), premises(1), phi, psi)
+ }
+
+ case object LeftImpliesWithoutFormula extends ProofStepWithoutBotNorPrem(2) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ val leftSequent = currentProof.getSequent(premises(0))
+ val rightSequent = currentProof.getSequent(premises(1))
+ val pivotLeft = leftSequent.right.diff(bot.right)
+ lazy val pivotRight = rightSequent.left.diff(bot.left)
+
+ if (pivotLeft.isEmpty)
+ SC.Weakening(bot, premises(0))
+ else if (pivotRight.isEmpty)
+ SC.Weakening(bot, premises(1))
+ else if (pivotLeft.tail.isEmpty && pivotRight.tail.isEmpty)
+ SC.LeftImplies(bot, premises(0), premises(1), pivotLeft.head, pivotRight.head)
+ else
+ ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ "Could not infer an implication as a pivot from the premises and conclusion, possible extraneous formulae in premises."
+ )
+ }
+ }
+
+ case object LeftImplies extends ProofStepWithoutBotNorPrem(2) {
+ // default construction:
+ // def apply(phi: Formula, psi: Formula) = new LeftImplies(phi, psi)
+ def apply() = LeftImpliesWithoutFormula
+
+ // usage without an argument list
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ this().asSCProof(bot, premises, currentProof)
+ }
+
+ /**
+ * <pre>
+ * Γ, φ→ψ |- Δ Γ, φ→ψ, ψ→φ |- Δ
+ * -------------- or --------------------
+ * Γ, φ↔ψ |- Δ Γ, φ↔ψ |- Δ
+ * </pre>
+ */
+ case class LeftIff(phi: Formula, psi: Formula) extends ProofStepWithoutBotNorPrem(1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ SC.LeftIff(bot, premises(0), phi, psi)
+ }
+
+ case class LeftIffWithoutFormula() extends ProofStepWithoutBotNorPrem(1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ val premiseSequent = currentProof.getSequent(premises(0))
+ val pivot = premiseSequent.left.diff(bot.left)
+
+ if (pivot.isEmpty)
+ SC.Weakening(bot, premises(0))
+ else
+ pivot.head match {
+ case ConnectorFormula(Implies, Seq(phi, psi)) => SC.LeftIff(bot, premises(0), phi, psi)
+ case _ => ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Could not infer a pivot implication from premise.")
+ }
+ }
+ }
+
+ case object LeftIff extends ProofStepWithoutBotNorPrem(1) {
+ // default construction:
+ // def apply(phi: Formula, psi: Formula) = new LeftIff(phi, psi)
+ def apply() = new LeftIffWithoutFormula()
+
+ // usage without an argument list
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ this().asSCProof(bot, premises, currentProof)
+ }
+
+ /**
+ * <pre>
+ * Γ |- φ, Δ
+ * --------------
+ * Γ, ¬φ |- Δ
+ * </pre>
+ */
+ case class LeftNot(phi: Formula) extends ProofStepWithoutBotNorPrem(1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ SC.LeftNot(bot, premises(0), phi)
+ }
+
+ case class LeftNotWithoutFormula() extends ProofStepWithoutBotNorPrem(1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ val premiseSequent = currentProof.getSequent(premises(0))
+ val pivot = premiseSequent.right.diff(bot.right)
+
+ if (pivot.isEmpty)
+ SC.Weakening(bot, premises(0))
+ else if (pivot.tail.isEmpty)
+ SC.LeftNot(bot, premises(0), pivot.head)
+ else
+ ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Right-hand side of conclusion + φ must be the same as right-hand side of premise.")
+
+ }
+ }
+
+ case object LeftNot extends ProofStepWithoutBotNorPrem(1) {
+ // default construction:
+ // def apply(phi: Formula) = new LeftNot(phi)
+ def apply() = new LeftNotWithoutFormula()
+
+ // usage without an argument list
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ this().asSCProof(bot, premises, currentProof)
+ }
+
+ /**
+ * <pre>
+ * Γ, φ[t/x] |- Δ
+ * -------------------
+ * Γ, ∀x. φ |- Δ
+ *
+ * </pre>
+ */
+ case class LeftForall(phi: Formula, x: VariableLabel, t: Term) extends ProofStepWithoutBotNorPrem(1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ SC.LeftForall(bot, premises(0), phi, x, t)
+ }
+
+ case class LeftForallWithoutFormula(t: Term) extends ProofStepWithoutBotNorPrem(1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ val premiseSequent = currentProof.getSequent(premises(0))
+ val pivot = bot.left.diff(premiseSequent.left)
+ lazy val instantiatedPivot = premiseSequent.left.diff(bot.left)
+
+ if (!pivot.isEmpty)
+ if (pivot.tail.isEmpty)
+ pivot.head match {
+ case BinderFormula(Forall, x, phi) => SC.LeftForall(bot, premises(0), phi, x, t)
+ case _ => ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Could not infer a universally quantified pivot from premise and conclusion.")
+ }
+ else
+ ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Left-hand side of conclusion + φ[t/x] must be the same as left-hand side of premise + ∀x. φ.")
+ else if (instantiatedPivot.isEmpty) SC.Weakening(bot, premises(0))
+ else if (instantiatedPivot.tail.isEmpty) {
+ // go through conclusion to find a matching quantified formula
+
+ val in: Formula = instantiatedPivot.head
+ val quantifiedPhi: Option[Formula] = bot.left.find(f =>
+ f match {
+ case g @ BinderFormula(Forall, _, _) => isSame(instantiateBinder(g, t), in)
+ case _ => false
+ }
+ )
+
+ quantifiedPhi match {
+ case Some(BinderFormula(Forall, x, phi)) => SC.LeftForall(bot, premises(0), phi, x, t)
+ case _ => ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Could not infer a universally quantified pivot from premise and conclusion.")
+ }
+ } else ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Left-hand side of conclusion + φ[t/x] must be the same as left-hand side of premise + ∀x. φ.")
+ }
+ }
+
+ case object LeftForall {
+ // default construction:
+ // def apply(phi: Formula, x: VariableLabel, t: Term) = new LeftForall(phi, x, t)
+ def apply(t: Term) = new LeftForallWithoutFormula(t)
+
+ // TODO: will require unification to infer input Term:
+ // def apply() = new LeftForallWithoutFormulaOrTerm()
+
+ // usage without an argument list
+ // TODO: add `extends ProofStepWithoutBotNorPrem(1)` to object when uncommenting
+ // def asSCProof(bot: Sequent, premises:Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ // this().asSCProof(bot, premises, currentProof)
+ }
+
+ /**
+ * <pre>
+ * Γ, φ |- Δ
+ * ------------------- if x is not free in the resulting sequent
+ * Γ, ∃x φ|- Δ
+ *
+ * </pre>
+ */
+ case class LeftExists(phi: Formula, x: VariableLabel) extends ProofStepWithoutBotNorPrem(1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ SC.LeftExists(bot, premises(0), phi, x)
+ }
+
+ case class LeftExistsWithoutFormula() extends ProofStepWithoutBotNorPrem(1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ val premiseSequent = currentProof.getSequent(premises(0))
+ val pivot = bot.left.diff(premiseSequent.left)
+ lazy val instantiatedPivot = premiseSequent.left.diff(bot.left)
+
+ if (pivot.isEmpty)
+ if (instantiatedPivot.isEmpty) SC.Rewrite(bot, premises(0))
+ else if (instantiatedPivot.tail.isEmpty) {
+ val in: Formula = instantiatedPivot.head
+ val quantifiedPhi: Option[Formula] = bot.left.find(f =>
+ f match {
+ case BinderFormula(Exists, _, g) => isSame(g, in)
+ case _ => false
+ }
+ )
+
+ quantifiedPhi match {
+ case Some(BinderFormula(Exists, x, phi)) => SC.LeftExists(bot, premises(0), phi, x)
+ case _ => ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Could not infer an existensially quantified pivot from premise and conclusion.")
+ }
+ } else ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Left-hand side of conclusion + φ must be the same as left-hand side of premise + ∃x. φ.")
+ else if (pivot.tail.isEmpty)
+ pivot.head match {
+ case BinderFormula(Exists, x, phi) => SC.LeftExists(bot, premises(0), phi, x)
+ case _ => ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Could not infer an existentially quantified pivot from premise and conclusion.")
+ }
+ else
+ ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Left-hand side of conclusion + φ must be the same as left-hand side of premise + ∃x. φ.")
+ }
+ }
+
+ case object LeftExists extends ProofStepWithoutBotNorPrem(1) {
+ // default construction:
+ // def apply(phi: Formula, x: VariableLabel) = new LeftExists(phi, x)
+ def apply() = new LeftExistsWithoutFormula()
+
+ // usage without an argument list
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ this().asSCProof(bot, premises, currentProof)
+ }
+
+ /**
+ * <pre>
+ * Γ, ∃y.∀x. (x=y) ↔ φ |- Δ
+ * ---------------------------- if y is not free in φ
+ * Γ, ∃!x. φ |- Δ
+ * </pre>
+ */
+ case class LeftExistsOne(phi: Formula, x: VariableLabel) extends ProofStepWithoutBotNorPrem(1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ SC.LeftExistsOne(bot, premises(0), phi, x)
+ }
+
+ case class LeftExistsOneWithoutFormula() extends ProofStepWithoutBotNorPrem(1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ val premiseSequent = currentProof.getSequent(premises(0))
+ val pivot = bot.left.diff(premiseSequent.left)
+ lazy val instantiatedPivot = premiseSequent.left.diff(bot.left)
+
+ if (pivot.isEmpty)
+ if (instantiatedPivot.isEmpty)
+ SC.Rewrite(bot, premises(0))
+ else if (instantiatedPivot.tail.isEmpty) {
+ instantiatedPivot.head match {
+ // ∃_. ∀x. _ ↔ φ == extract ==> x, phi
+ case BinderFormula(Exists, _, BinderFormula(Forall, x, ConnectorFormula(Iff, Seq(_, phi)))) => SC.LeftExistsOne(bot, premises(0), phi, x)
+ case _ => ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Could not infer an existentially quantified pivot from premise and conclusion.")
+ }
+ } else
+ ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Left-hand side of conclusion + φ must be the same as left-hand side of premise + ∃x. φ.")
+ else if (pivot.tail.isEmpty)
+ pivot.head match {
+ case BinderFormula(ExistsOne, x, phi) => SC.LeftExistsOne(bot, premises(0), phi, x)
+ case _ => ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Could not infer an existentially quantified pivot from premise and conclusion.")
+ }
+ else
+ ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Left-hand side of conclusion + φ must be the same as left-hand side of premise + ∃x. φ.")
+ }
+ }
+
+ case object LeftExistsOne extends ProofStepWithoutBotNorPrem(1) {
+ // default construction:
+ // def apply(phi: Formula, x: VariableLabel) = new LeftExistsOne(phi, x)
+ def apply() = new LeftExistsOneWithoutFormula()
+
+ // usage without an argument list
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ this().asSCProof(bot, premises, currentProof)
+ }
+
+ // Right rules
+ /**
+ * <pre>
+ * Γ |- φ, Δ Σ |- ψ, Π...
+ * ------------------------------------
+ * Γ, Σ |- φ∧ψ∧..., Π, Δ
+ * </pre>
+ */
+ case class RightAnd(cunjuncts: Seq[Formula]) extends ProofStepWithoutBotNorPrem(-1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ SC.RightAnd(bot, premises, cunjuncts)
+ }
+ case object RightAndWithoutFormula extends ProofStepWithoutBotNorPrem(-1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ val premiseSequents = premises.map(currentProof.getSequent(_))
+ val pivots = premiseSequents.map(_.right.diff(bot.right))
+
+ if (pivots.exists(_.isEmpty))
+ SC.Weakening(bot, premises(pivots.indexWhere(_.isEmpty)))
+ else if (pivots.forall(_.tail.isEmpty))
+ SC.RightAnd(bot, premises, pivots.map(_.head))
+ else
+ // some extraneous formulae
+ ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ "Right-hand side of conclusion + φ + ψ is not the same as the union of the right-hand sides of the premises +φ∧ψ."
+ )
+ }
+ }
+
+ case object RightAnd extends ProofStepWithoutBotNorPrem(-1) {
+ // default construction:
+ // def apply(conjuncts: Seq[Formula]) = new RightAnd(conjuncts)
+ def apply() = RightAndWithoutFormula
+
+ // usage without an argument list
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ this().asSCProof(bot, premises, currentProof)
+ }
+
+ /**
+ * <pre>
+ * Γ |- φ, Δ Γ |- φ, ψ, Δ
+ * -------------- or ---------------
+ * Γ |- φ∨ψ, Δ Γ |- φ∨ψ, Δ
+ * </pre>
+ */
+ case class RightOr(phi: Formula, psi: Formula) extends ProofStepWithoutBotNorPrem(1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ SC.RightOr(bot, premises(0), phi, psi)
+ }
+
+ case class RightOrWithoutFormula() extends ProofStepWithoutBotNorPrem(1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ val premiseSequent = currentProof.getSequent(premises(0))
+ val pivot = bot.right.diff(premiseSequent.right)
+
+ if (!pivot.isEmpty && pivot.tail.isEmpty)
+ pivot.head match {
+ case ConnectorFormula(Or, Seq(phi, psi)) =>
+ if (premiseSequent.left.contains(phi))
+ SC.RightOr(bot, premises(0), phi, psi)
+ else
+ SC.RightOr(bot, premises(0), psi, phi)
+ case _ => ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Could not infer a disjunction as pivot from premise and conclusion.")
+ }
+ else
+ // try a rewrite, if it works, go ahead with it, otherwise malformed
+ if (SC.isSameSequent(premiseSequent, bot))
+ SC.Rewrite(bot, premises(0))
+ else
+ ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ "Right-hand side of conclusion + φ∧ψ must be same as right-hand side of premise + either φ, ψ or both."
+ )
+ }
+ }
+
+ case object RightOr extends ProofStepWithoutBotNorPrem(1) {
+ // default construction:
+ // def apply(phi: Formula, psi: Formula) = new RightOr(phi, psi)
+ def apply() = new RightOrWithoutFormula()
+
+ // usage without an argument list
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ this().asSCProof(bot, premises, currentProof)
+ }
+
+ /**
+ * <pre>
+ * Γ, φ |- ψ, Δ
+ * --------------
+ * Γ |- φ→ψ, Δ
+ * </pre>
+ */
+ case class RightImplies(phi: Formula, psi: Formula) extends ProofStepWithoutBotNorPrem(1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ SC.RightImplies(bot, premises(0), phi, psi)
+ }
+
+ case class RightImpliesWithoutFormula() extends ProofStepWithoutBotNorPrem(1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ val premiseSequent = currentProof.getSequent(premises(0))
+ val leftPivot = premiseSequent.left.diff(bot.left)
+ val rightPivot = premiseSequent.right.diff(bot.right)
+
+ if (
+ !leftPivot.isEmpty && leftPivot.tail.isEmpty &&
+ !rightPivot.isEmpty && rightPivot.tail.isEmpty
+ )
+ SC.RightImplies(bot, premises(0), leftPivot.head, rightPivot.head)
+ else
+ ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Right-hand side of conclusion + ψ must be same as right-hand side of premise + φ→ψ.")
+ }
+ }
+
+ case object RightImplies extends ProofStepWithoutBotNorPrem(1) {
+ // default construction:
+ // def apply(phi: Formula, psi: Formula) = new RightImplies(phi, psi)
+ def apply() = new RightImpliesWithoutFormula()
+
+ // usage without an argument list
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ this().asSCProof(bot, premises, currentProof)
+ }
+
+ /**
+ * <pre>
+ * Γ |- φ→ψ, Δ Σ |- ψ→φ, Î
+ * ----------------------------
+ * Γ, Σ |- φ↔ψ, Π, Δ
+ * </pre>
+ */
+ case class RightIff(phi: Formula, psi: Formula) extends ProofStepWithoutBotNorPrem(2) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ SC.RightIff(bot, premises(0), premises(1), phi, psi)
+ }
+
+ case class RightIffWithoutFormula() extends ProofStepWithoutBotNorPrem(2) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ val premiseSequent = currentProof.getSequent(premises(0))
+ val pivot = premiseSequent.right.diff(bot.right)
+
+ if (pivot.isEmpty)
+ SC.Weakening(bot, premises(0))
+ else if (pivot.tail.isEmpty)
+ pivot.head match {
+ case ConnectorFormula(Implies, Seq(phi, psi)) => SC.RightIff(bot, premises(0), premises(1), phi, psi)
+ case _ => ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Could not infer an implication as pivot from premise and conclusion.")
+ }
+ else
+ ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ "Right-hand side of conclusion + φ→ψ + ψ→φ is not the same as the union of the right-hand sides of the premises φ↔ψ."
+ )
+ }
+ }
+
+ case object RightIff extends ProofStepWithoutBotNorPrem(2) {
+ // default construction:
+ // def apply(phi: Formula, psi: Formula) = new RightIff(phi, psi)
+ def apply() = new RightIffWithoutFormula()
+
+ // usage without an argument list
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ this().asSCProof(bot, premises, currentProof)
+ }
+
+ /**
+ * <pre>
+ * Γ, φ |- Δ
+ * --------------
+ * Γ |- ¬φ, Δ
+ * </pre>
+ */
+ case class RightNot(phi: Formula) extends ProofStepWithoutBotNorPrem(1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ SC.RightNot(bot, premises(0), phi)
+ }
+
+ case class RightNotWithoutFormula() extends ProofStepWithoutBotNorPrem(1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ val premiseSequent = currentProof.getSequent(premises(0))
+ val pivot = premiseSequent.left.diff(bot.left)
+
+ if (pivot.isEmpty)
+ SC.Weakening(bot, premises(0))
+ else if (pivot.tail.isEmpty)
+ SC.RightNot(bot, premises(0), pivot.head)
+ else
+ ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Left-hand side of conclusion + φ must be the same as left-hand side of premise.")
+
+ }
+ }
+
+ case object RightNot extends ProofStepWithoutBotNorPrem(1) {
+ // default construction:
+ // def apply(phi: Formula) = new RightNot(phi)
+ def apply() = new RightNotWithoutFormula()
+
+ // usage without an argument list
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ this().asSCProof(bot, premises, currentProof)
+ }
+
+ /**
+ * <pre>
+ * Γ |- φ, Δ
+ * ------------------- if x is not free in the resulting sequent
+ * Γ |- ∀x. φ, Δ
+ * </pre>
+ */
+ case class RightForall(phi: Formula, x: VariableLabel) extends ProofStepWithoutBotNorPrem(1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ SC.RightForall(bot, premises(0), phi, x)
+ }
+
+ case class RightForallWithoutFormula() extends ProofStepWithoutBotNorPrem(1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ val premiseSequent = currentProof.getSequent(premises(0))
+ val pivot = bot.right.diff(premiseSequent.right)
+ lazy val instantiatedPivot = premiseSequent.right.diff(bot.right)
+
+ if (pivot.isEmpty)
+ if (instantiatedPivot.isEmpty) SC.Rewrite(bot, premises(0))
+ else if (instantiatedPivot.tail.isEmpty) {
+ val in: Formula = instantiatedPivot.head
+ val quantifiedPhi: Option[Formula] = bot.right.find(f =>
+ f match {
+ case BinderFormula(Forall, _, g) => isSame(g, in)
+ case _ => false
+ }
+ )
+
+ quantifiedPhi match {
+ case Some(BinderFormula(Forall, x, phi)) => SC.RightForall(bot, premises(0), phi, x)
+ case _ => ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Could not infer a universally quantified pivot from premise and conclusion.")
+ }
+ } else ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Right-hand side of conclusion + φ must be the same as right-hand side of premise + ∃x. φ.")
+ else if (pivot.tail.isEmpty)
+ pivot.head match {
+ case BinderFormula(Forall, x, phi) => SC.RightForall(bot, premises(0), phi, x)
+ case _ => ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Could not infer a universally quantified pivot from premise and conclusion.")
+ }
+ else
+ ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Right-hand side of conclusion + φ must be the same as right-hand side of premise + ∃x. φ.")
+ }
+ }
+
+ case object RightForall extends ProofStepWithoutBotNorPrem(1) {
+ // default construction:
+ // def apply(phi: Formula, x: VariableLabel) = new RightForall(phi, x)
+ def apply() = new RightForallWithoutFormula()
+
+ // usage without an argument list
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ this().asSCProof(bot, premises, currentProof)
+ }
+
+ /**
+ * <pre>
+ * Γ |- φ[t/x], Δ
+ * -------------------
+ * Γ |- ∃x. φ, Δ
+ *
+ * (ln-x stands for locally nameless x)
+ * </pre>
+ */
+ case class RightExists(phi: Formula, x: VariableLabel, t: Term) extends ProofStepWithoutBotNorPrem(1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ SC.RightExists(bot, premises(0), phi, x, t)
+ }
+
+ case class RightExistsWithoutFormula(t: Term) extends ProofStepWithoutBotNorPrem(1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ val premiseSequent = currentProof.getSequent(premises(0))
+ val pivot = bot.right.diff(premiseSequent.right)
+ lazy val instantiatedPivot = premiseSequent.right.diff(bot.right)
+
+ if (!pivot.isEmpty)
+ if (pivot.tail.isEmpty)
+ pivot.head match {
+ case BinderFormula(Exists, x, phi) => SC.RightExists(bot, premises(0), phi, x, t)
+ case _ => ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Could not infer an existentially quantified pivot from premise and conclusion.")
+ }
+ else
+ ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ "Right-hand side of conclusion + φ[t/x] must be the same as right-hand side of premise + ∀x. φ."
+ )
+ else if (instantiatedPivot.isEmpty) SC.Weakening(bot, premises(0))
+ else if (instantiatedPivot.tail.isEmpty) {
+ // go through conclusion to find a matching quantified formula
+
+ val in: Formula = instantiatedPivot.head
+ val quantifiedPhi: Option[Formula] = bot.right.find(f =>
+ f match {
+ case g @ BinderFormula(Exists, _, _) => isSame(instantiateBinder(g, t), in)
+ case _ => false
+ }
+ )
+
+ quantifiedPhi match {
+ case Some(BinderFormula(Exists, x, phi)) => SC.RightExists(bot, premises(0), phi, x, t)
+ case _ => ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Could not infer an existentially quantified pivot from premise and conclusion.")
+ }
+ } else
+ ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ "Right-hand side of conclusion + φ[t/x] must be the same as right-hand side of premise + ∀x. φ."
+ )
+ }
+ }
+
+ case object RightExists {
+ // default construction:
+ // def apply(phi: Formula, x: VariableLabel, t: Term) = new RightExists(phi, x, t)
+ def apply(t: Term) = new RightExistsWithoutFormula(t)
+
+ // TODO: will require unification to infer input Term:
+ // def apply() = new RightExistsWithoutFormulaOrTerm()
+
+ // usage without an argument list
+ // TODO: add `extends ProofStepWithoutBotNorPrem(1)` to object when uncommenting
+ // def asSCProof(bot: Sequent, premises:Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ // this().asSCProof(bot, premises, currentProof)
+ }
+
+ /**
+ * <pre>
+ * Γ |- ∃y.∀x. (x=y) ↔ φ, Δ
+ * ---------------------------- if y is not free in φ
+ * Γ|- ∃!x. φ, Δ
+ * </pre>
+ */
+ case class RightExistsOne(phi: Formula, x: VariableLabel) extends ProofStepWithoutBotNorPrem(1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ SC.RightExistsOne(bot, premises(0), phi, x)
+ }
+
+ case class RightExistsOneWithoutFormula() extends ProofStepWithoutBotNorPrem(1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ val premiseSequent = currentProof.getSequent(premises(0))
+ val pivot = bot.right.diff(premiseSequent.right)
+ lazy val instantiatedPivot = premiseSequent.right.diff(bot.right)
+
+ if (pivot.isEmpty)
+ if (instantiatedPivot.isEmpty)
+ SC.Rewrite(bot, premises(0))
+ else if (instantiatedPivot.tail.isEmpty) {
+ instantiatedPivot.head match {
+ // ∃_. ∀x. _ ↔ φ == extract ==> x, phi
+ case BinderFormula(Exists, _, BinderFormula(Forall, x, ConnectorFormula(Iff, Seq(_, phi)))) => SC.RightExistsOne(bot, premises(0), phi, x)
+ case _ => ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Could not infer an existentially quantified pivot from premise and conclusion.")
+ }
+ } else
+ ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Right-hand side of conclusion + φ must be the same as right-hand side of premise + ∃x. φ.")
+ else if (pivot.tail.isEmpty)
+ pivot.head match {
+ case BinderFormula(ExistsOne, x, phi) => SC.RightExistsOne(bot, premises(0), phi, x)
+ case _ => ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Could not infer an existentially quantified pivot from premise and conclusion.")
+ }
+ else
+ ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Right-hand side of conclusion + φ must be the same as right-hand side of premise + ∃x. φ.")
+ }
+ }
+
+ case object RightExistsOne extends ProofStepWithoutBotNorPrem(1) {
+ // default construction:
+ // def apply(phi: Formula, x: VariableLabel) = new RightExistsOne(phi, x)
+ def apply() = new RightExistsOneWithoutFormula()
+
+ // usage without an argument list
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ this().asSCProof(bot, premises, currentProof)
+ }
+
+ // Structural rules
+ /**
+ * <pre>
+ * Γ |- Δ
+ * --------------
+ * Γ, Σ |- Δ, Î
+ * </pre>
+ */
+ case object Weakening extends ProofStepWithoutBotNorPrem(1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ SC.Weakening(bot, premises(0))
+ }
+
+ // Equality Rules
+ /**
+ * <pre>
+ * Γ, s=s |- Δ
+ * --------------
+ * Γ |- Δ
+ * </pre>
+ */
+ case class LeftRefl(fa: Formula) extends ProofStepWithoutBotNorPrem(1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ SC.LeftRefl(bot, premises(0), fa)
+ }
+
+ case class LeftReflWithoutFormula() extends ProofStepWithoutBotNorPrem(1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ SC.Rewrite(bot, premises(0))
+ }
+
+ case object LeftRefl extends ProofStepWithoutBotNorPrem(1) {
+ // default construction:
+ // def apply(fa: Formula) = new LeftRefl(fa)
+ def apply() = new LeftReflWithoutFormula()
+
+ // usage without an argument list
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ this().asSCProof(bot, premises, currentProof)
+ }
+
+ /**
+ * <pre>
+ *
+ * --------------
+ * |- s=s
+ * </pre>
+ */
+ case class RightRefl(fa: Formula) extends ProofStepWithoutBotNorPrem(0) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ SC.RightRefl(bot, fa)
+ }
+
+ case class RightReflWithoutFormula() extends ProofStepWithoutBotNorPrem(0) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ SC.RewriteTrue(bot)
+ }
+
+ case object RightRefl extends ProofStepWithoutBotNorPrem(0) {
+ // default construction:
+ // def apply(fa: Formula) = new RightRefl(fa)
+ def apply() = new RightReflWithoutFormula()
+
+ // usage without an argument list
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ this().asSCProof(bot, premises, currentProof)
+ }
+
+ /**
+ * <pre>
+ * Γ, φ(s1,...,sn) |- Δ
+ * ---------------------
+ * Γ, s1=premises(0), ..., sn=tn, φ(premises(0),...tn) |- Δ
+ * </pre>
+ */
+ case class LeftSubstEq(equals: List[(Term, Term)], lambdaPhi: LambdaTermFormula) extends ProofStepWithoutBotNorPrem(1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ SC.LeftSubstEq(bot, premises(0), equals, lambdaPhi)
+ }
+
+ /**
+ * <pre>
+ * Γ |- φ(s1,...,sn), Δ
+ * ---------------------
+ * Γ, s1=premises(0), ..., sn=tn |- φ(premises(0),...tn), Δ
+ * </pre>
+ */
+ case class RightSubstEq(equals: List[(Term, Term)], lambdaPhi: LambdaTermFormula) extends ProofStepWithoutBotNorPrem(1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ SC.RightSubstEq(bot, premises(0), equals, lambdaPhi)
+ }
+
+ /**
+ * <pre>
+ * Γ, φ(a1,...an) |- Δ
+ * ---------------------
+ * Γ, a1↔b1, ..., an↔bn, φ(b1,...bn) |- Δ
+ * </pre>
+ */
+ case class LeftSubstIff(equals: List[(Formula, Formula)], lambdaPhi: LambdaFormulaFormula) extends ProofStepWithoutBotNorPrem(1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ SC.LeftSubstIff(bot, premises(0), equals, lambdaPhi)
+ }
+
+ /**
+ * <pre>
+ * Γ |- φ(a1,...an), Δ
+ * ---------------------
+ * Γ, a1↔b1, ..., an↔bn |- φ(b1,...bn), Δ
+ * </pre>
+ */
+ case class RightSubstIff(equals: List[(Formula, Formula)], lambdaPhi: LambdaFormulaFormula) extends ProofStepWithoutBotNorPrem(1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ SC.RightSubstIff(bot, premises(0), equals, lambdaPhi)
+ }
+
+ /**
+ * <pre>
+ * Γ |- Δ
+ * --------------------------
+ * Γ[r(a)/?f] |- Δ[r(a)/?f]
+ * </pre>
+ */
+ case class InstFunSchema(insts: Map[SchematicTermLabel, LambdaTermTerm]) extends ProofStepWithoutBotNorPrem(1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ SC.InstFunSchema(bot, premises(0), insts)
+ }
+
+ /**
+ * <pre>
+ * Γ |- Δ
+ * --------------------------
+ * Γ[ψ(a)/?p] |- Δ[ψ(a)/?p]
+ * </pre>
+ */
+ case class InstPredSchema(insts: Map[SchematicVarOrPredLabel, LambdaTermFormula]) extends ProofStepWithoutBotNorPrem(1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ SC.InstPredSchema(bot, premises(0), insts)
+ }
+
+ // Proof Organisation rules
+ case class SCSubproof(sp: SCProof, premises: Seq[Int] = Seq.empty, display: Boolean = true) extends ProofStep {
+ def asSCProof(currentProof: Library#Proof): ProofStepJudgement =
+ sp match {
+ case sp: SCProof => SC.SCSubproof(sp, premises, display)
+ }
+ }
+
+}
diff --git a/lisa-utils/src/main/scala/lisa/utils/tactics/ProofStepJudgement.scala b/lisa-utils/src/main/scala/lisa/utils/tactics/ProofStepJudgement.scala
new file mode 100644
index 00000000..57a9a4be
--- /dev/null
+++ b/lisa-utils/src/main/scala/lisa/utils/tactics/ProofStepJudgement.scala
@@ -0,0 +1,44 @@
+package lisa.utils.tactics
+
+import lisa.kernel.proof.SCProofCheckerJudgement
+import lisa.kernel.proof.SequentCalculus.SCProofStep
+import lisa.utils.tactics.ProofStepLib.ProofStep
+
+/**
+ * Contains the result of a tactic computing a SCProofStep.
+ * Can be successful or unsuccessful.
+ */
+sealed abstract class ProofStepJudgement {
+ import ProofStepJudgement.*
+
+ /**
+ * Returns true if and only if the jusdgement is valid.
+ */
+ def isValid: Boolean = this match {
+ case ValidProofStep(scps) => true
+ case InvalidProofStep(ps, error) => false
+ }
+
+}
+
+object ProofStepJudgement {
+
+ /**
+ * Indicates an error in the building of a proof that was caught before the proof is passed to the logical kernel.
+ * May indicate a faulty tactic application.
+ */
+ case class EarlyProofStepException(message: String) extends Exception(message)
+
+ /**
+ * A Sequent Calculus proof step that has been correctly produced.
+ */
+ case class ValidProofStep(scps: SCProofStep) extends ProofStepJudgement
+
+ /**
+ * A proof step which led to an error when computing the corresponding Sequent Calculus proof step.
+ */
+ case class InvalidProofStep(ps: ProofStep, message: String) extends ProofStepJudgement {
+ def launch: Nothing = throw EarlyProofStepException(message)
+ }
+
+}
diff --git a/lisa-utils/src/main/scala/lisa/utils/tactics/ProofStepLib.scala b/lisa-utils/src/main/scala/lisa/utils/tactics/ProofStepLib.scala
new file mode 100644
index 00000000..99c81eb2
--- /dev/null
+++ b/lisa-utils/src/main/scala/lisa/utils/tactics/ProofStepLib.scala
@@ -0,0 +1,143 @@
+package lisa.utils.tactics
+
+import lisa.kernel.proof
+import lisa.kernel.proof.RunningTheory
+import lisa.kernel.proof.RunningTheoryJudgement
+import lisa.kernel.proof.RunningTheoryJudgement.InvalidJustification
+import lisa.kernel.proof.RunningTheoryJudgement.InvalidJustificationException
+import lisa.kernel.proof.SequentCalculus
+import lisa.kernel.proof.SequentCalculus.SCProofStep
+import lisa.kernel.proof.SequentCalculus.Sequent
+import lisa.utils.Helpers.*
+import lisa.utils.Library
+import lisa.utils.Printer
+import lisa.utils.tactics.ProofStepJudgement.*
+
+object ProofStepLib {
+
+ /**
+ * A proofstep is an object that relies on a step of premises and which can be translated into pure Sequent Calculus.
+ */
+ trait ProofStep {
+ val premises: Seq[Library#Proof#Fact]
+
+ /**
+ * Add the proofstep to the current proof of the given library.
+ */
+ def validate(l: Library)(using output: String => Unit)(using finishOutput: Throwable => Nothing): l.Proof#DoubleStep = {
+ l.proofStack.head.newDoubleStep(this)
+ }
+
+ /**
+ * An abstract function transforming the ProofStep innto a SCProofStep in pure Sequent Calculus.
+ */
+ def asSCProof(currentProof: Library#Proof): ProofStepJudgement
+
+ }
+
+ /**
+ * A proof step lacking a bottom/conclusion sequent. Once given a conclusion sequent, it can become a ProofStep.
+ */
+ trait ProofStepWithoutBot {
+ val premises: Seq[Library#Proof#Fact]
+
+ /**
+ * An abstract function transforming the ProofStepWithoutBot into a SCProofStep in pure Sequent Calculus,
+ * by being given access to a target conclusive sequent and the current state of the proof.
+ */
+ def asSCProof(bot: Sequent, currentProof: Library#Proof): ProofStepJudgement
+
+ /**
+ * Gives a targeted bottom sequent, as a partial application towards the SC transformation.
+ */
+ def asProofStep(bot: Sequent): ProofStep = new ProofStepWithBot(this, bot)
+ }
+
+ /**
+ * Intermediate datatype corresponding to a ProofStepWithoutBot once a targetted bottom sequent has been given to it.
+ */
+ class ProofStepWithBot protected[ProofStepLib] (
+ val underlying: ProofStepWithoutBot,
+ val givenBot: Sequent
+ ) extends ProofStep {
+ override val premises: Seq[Library#Proof#Fact] = underlying.premises
+ override def asSCProof(currentProof: Library#Proof): ProofStepJudgement = underlying.asSCProof(givenBot ++< (currentProof.getAssumptions |- ()), currentProof)
+ }
+
+ /**
+ * Represent a ProofStep lacking the list of its premises, for partial application.
+ */
+ trait ProofStepWithoutPrem {
+
+ /**
+ * An abstract function transforming the ProofStepWithoutPrem innto a SCProofStep in pure Sequent Calculus.
+ */
+ def asSCProof(premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement
+
+ /**
+ * Gives the premises of the ProofStep, as a partial application towards the SC transformation.
+ */
+ def asProofStep(premises: Seq[Library#Proof#Fact]): ProofStep = new ProofStepWithPrem(this, premises)
+
+ /**
+ * Alias for [[asProofStep]]
+ */
+ def by(premises: Seq[Library#Proof#Fact]): ProofStep = asProofStep(premises)
+ }
+
+ /**
+ * Intermediate datatype corresponding to a [[ProofStepWithoutPrem]] once a sequence of premises has been given to it.
+ */
+ class ProofStepWithPrem protected[ProofStepLib] (
+ val underlying: ProofStepWithoutPrem,
+ val premises: Seq[Library#Proof#Fact]
+ ) extends ProofStep {
+ override def asSCProof(currentProof: Library#Proof): ProofStepJudgement =
+ if (premises.forall(prem => currentProof.validInThisProof(prem))) {
+ underlying.asSCProof(premises.map(prem => currentProof.getSequentAndInt(prem.asInstanceOf[currentProof.Fact])._2), currentProof)
+ } else {
+ ProofStepJudgement.InvalidProofStep(this, "Illegal reference to a previous step outside of this Proof's scope.")
+ }
+ }
+
+ /**
+ * A ProofStep without premises nor targeted bottom sequent.
+ * Contains a tactic to reconstruct a partial Sequent Calculus proof if given those elements and the current proof.
+ */
+ trait ProofStepWithoutBotNorPrem[N <: Int & Singleton](val numbPrem: N) {
+
+ /**
+ * Contains a tactic to reconstruct a partial Sequent Calculus proof if given
+ * a list of premises, a targeted bottom sequent and the current proof.
+ */
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement
+ def asProofStepWithoutBot(premises: Seq[Library#Proof#Fact]): ProofStepWithoutBot =
+ new ProofStepWithoutBotWithPrem[N](this, premises)
+ def apply(premises: Library#Proof#Fact*): ProofStepWithoutBot = asProofStepWithoutBot(premises)
+ }
+
+ /**
+ * Intermediate datatype corresponding to a [[ProofStepWithoutBotNorPrem]] once a sequence of premises has been given to it.
+ */
+ class ProofStepWithoutBotWithPrem[N <: Int & Singleton] protected[ProofStepLib] (
+ val underlying: ProofStepWithoutBotNorPrem[N],
+ override val premises: Seq[Library#Proof#Fact]
+ ) extends ProofStepWithoutBot {
+ val numbPrem: N = underlying.numbPrem
+
+ /**
+ * Contains a tactic to reconstruct a partial Sequent Calculus proof if given
+ * a targeted bottom sequent and the current proof.
+ */
+ def asSCProof(bot: Sequent, currentProof: Library#Proof): ProofStepJudgement = {
+ if (premises.forall(prem => currentProof.validInThisProof(prem))) {
+ underlying.asSCProof(bot, premises.map(prem => currentProof.getSequentAndInt(prem.asInstanceOf[currentProof.Fact])._2), currentProof)
+ } else {
+ ProofStepJudgement.InvalidProofStep(asProofStep(bot), "Illegal reference to a previous step outside of this Proof's scope.")
+ }
+ }
+ }
+
+ given Conversion[SCProofStep, ProofStepJudgement] = c => ProofStepJudgement.ValidProofStep(c)
+
+}
diff --git a/lisa-utils/src/main/scala/lisa/utils/tactics/ProofsHelpers.scala b/lisa-utils/src/main/scala/lisa/utils/tactics/ProofsHelpers.scala
new file mode 100644
index 00000000..2fa04fdd
--- /dev/null
+++ b/lisa-utils/src/main/scala/lisa/utils/tactics/ProofsHelpers.scala
@@ -0,0 +1,134 @@
+package lisa.utils.tactics
+
+import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.SCProofChecker
+import lisa.kernel.proof.SequentCalculus.SCProofStep
+import lisa.kernel.proof.SequentCalculus.Sequent
+import lisa.utils.Library
+import lisa.utils.Parser.parseFormula
+import lisa.utils.Parser.parseSequent
+import lisa.utils.Parser.parseTerm
+import lisa.utils.tactics.ProofStepLib.*
+
+trait ProofsHelpers {
+ library: Library & WithProofs =>
+ given Library = library
+ export BasicStepTactic.*
+ export SimpleDeducedSteps.*
+ private def proof: Proof = proofStack.head
+
+ case class HaveSequent private[ProofsHelpers] (bot: Sequent) {
+ infix def by(just: ProofStepWithoutBot)(using String => Unit)(using finishOutput: Throwable => Nothing): library.Proof#DoubleStep = {
+ val r = just.asProofStep(bot)
+ r.validate(library)
+ }
+ }
+
+ case class AndThenSequent private[ProofsHelpers] (bot: Sequent) {
+ infix def by[N <: Int & Singleton](just: ProofStepWithoutBotNorPrem[N])(using String => Unit)(using finishOutput: Throwable => Nothing): library.Proof#DoubleStep = {
+ val r = just.asProofStepWithoutBot(Seq(proof.mostRecentStep._2)).asProofStep(bot)
+ r.validate(library)
+ }
+ }
+
+ /**
+ * Claim the given Sequent as a ProofStep, which may require a justification by a proof tactic and premises.
+ */
+ def have(res: Sequent): HaveSequent = HaveSequent(res)
+
+ /**
+ * Claim the given Sequent as a ProofStep, which may require a justification by a proof tactic and premises.
+ */
+ def have(res: String): HaveSequent = HaveSequent(parseSequent(res))
+
+ /**
+ * Claim the given known Theorem, Definition or Axiom as a Sequent.
+ */
+ def have(just: theory.Justification)(using String => Unit)(using finishOutput: Throwable => Nothing): library.Proof#DoubleStep = {
+ have(theory.sequentFromJustification(just)) by Restate(just.asInstanceOf[Library#Proof#Fact])
+ }
+
+ /* //TODO: After reviewing substitutions
+ def have(instJust: InstantiatedJustification)(using String => Unit)(using finishOutput: Throwable => Nothing): library.Proof#DoubleStep = {
+ val just = instJust.just
+ val (seq, ref) = proof.getSequentAndInt(just)
+ if (instJust.instsPred.isEmpty && instJust.instsTerm.isEmpty && instJust.instForall.isEmpty){
+ have(seq) by Restate(ref)
+ } else if (instJust.instsPred.isEmpty && instJust.instForall.isEmpty){
+ val res = (seq.left.map(phi => instantiateTermSchemas(phi, instJust.instsTerm)) |- seq.right.map(phi => instantiateTermSchemas(phi, instJust.instsTerm)))
+ have(res) by InstFunSchema(instJust.instsTerm)(ref)
+ } else if (instJust.instsTerm.isEmpty && instJust.instForall.isEmpty){
+ val res = (seq.left.map(phi => instantiatePredicateSchemas(phi, instJust.instsPred)) |- seq.right.map(phi => instantiatePredicateSchemas(phi, instJust.instsPred)))
+ have(res) by InstPredSchema(instJust.instsPred)(ref)
+ } else if(instJust.instsPred.isEmpty && instJust.instsTerm.isEmpty){
+ ???
+ } else {
+ ???
+ }
+ }
+ */
+
+ /**
+ * Claim the given Sequent as a ProofStep directly following the previously proven tactic,
+ * which may require a justification by a proof tactic.
+ */
+ def andThen(res: Sequent): AndThenSequent = AndThenSequent(res)
+
+ /**
+ * Claim the given Sequent as a ProofStep directly following the previously proven tactic,
+ * which may require a justification by a proof tactic.
+ */
+ def andThen(res: String): AndThenSequent = AndThenSequent(parseSequent(res))
+
+ /**
+ * Import the given justification (Axiom, Theorem or Definition) into the current proof.
+ */
+ def withImport(just: theory.Justification): library.Proof#ImportedFact = {
+ proofStack.head.newImportedFact(just)
+
+ }
+
+ /**
+ * Assume the given formula in all future left hand-side of claimed sequents.
+ */
+ def assume(f: Formula): Formula = {
+ proofStack.head.addAssumption(f)
+ f
+ }
+
+ /**
+ * Store the given import and use it to discharge the proof of one of its assumption at the very end.
+ */
+ def endDischarge(ji: Library#Proof#ImportedFact): Unit = {
+ val p: Proof = proof
+ if (p.validInThisProof(ji)) {
+ val p = proof
+ p.addDischarge(ji.asInstanceOf[p.ImportedFact])
+ }
+ }
+
+ given Conversion[ProofStepWithoutBotNorPrem[0], ProofStepWithoutBot] = _.asProofStepWithoutBot(Seq())
+
+ // case class InstantiatedJustification(just:theory.Justification, instsPred: Map[SchematicVarOrPredLabel, LambdaTermFormula], instsTerm: Map[SchematicTermLabel, LambdaTermTerm], instForall:Seq[Term])
+
+ /* //TODO: After reviewing the substitutions
+ extension (just: theory.Justification) {/*
+ def apply(insts: ((SchematicVarOrPredLabel, LambdaTermFormula) | (SchematicTermLabel, LambdaTermTerm) | Term)*): InstantiatedJustification = {
+ val instsPred: Map[SchematicVarOrPredLabel, LambdaTermFormula] = insts.filter(isLTT).asInstanceOf[Seq[(SchematicVarOrPredLabel, LambdaTermFormula)]].toMap
+ val instsTerm: Map[SchematicTermLabel, LambdaTermTerm] = insts.filter(isLTF).asInstanceOf[Seq[(SchematicTermLabel, LambdaTermTerm)]].toMap
+ val instsForall: Seq[Term] = insts.filter(isTerm).asInstanceOf[Seq[Term]]
+ InstantiatedJustification(just, instsPred, instsTerm, instsForall)
+ }*/
+
+ def apply(insts: (VariableLabel, Term)*): InstantiatedJustification = {
+ InstantiatedJustification(just, Map(), insts.map((x:VariableLabel, t:Term) => (x, LambdaTermTerm(Seq(), t))).toMap, Seq())
+ }
+ }
+
+ private def isTerm(x: (SchematicVarOrPredLabel, LambdaTermFormula) | (SchematicTermLabel, LambdaTermTerm) | Term):Boolean = x.isInstanceOf[Term]
+ private def isLTT(x: (SchematicVarOrPredLabel, LambdaTermFormula) | (SchematicTermLabel, LambdaTermTerm) | Term):Boolean = x.isInstanceOf[Tuple2[_, _]] && x.asInstanceOf[Tuple2[_, _]]._2.isInstanceOf[LambdaTermTerm]
+ private def isLTF(x: (SchematicVarOrPredLabel, LambdaTermFormula) | (SchematicTermLabel, LambdaTermTerm) | Term):Boolean = x.isInstanceOf[Tuple2[_, _]] && x.asInstanceOf[Tuple2[_, _]]._2.isInstanceOf[LambdaTermFormula]
+
+ */
+
+}
diff --git a/lisa-utils/src/main/scala/lisa/utils/tactics/SimpleDeducedSteps.scala b/lisa-utils/src/main/scala/lisa/utils/tactics/SimpleDeducedSteps.scala
new file mode 100644
index 00000000..5516124b
--- /dev/null
+++ b/lisa-utils/src/main/scala/lisa/utils/tactics/SimpleDeducedSteps.scala
@@ -0,0 +1,438 @@
+package lisa.utils.tactics
+
+import lisa.kernel.fol.FOL
+import lisa.kernel.proof.SCProof
+import lisa.kernel.proof.SCProofChecker
+import lisa.kernel.proof.SequentCalculus.RewriteTrue
+import lisa.kernel.proof.SequentCalculus.SCProofStep
+import lisa.kernel.proof.SequentCalculus.Sequent
+import lisa.kernel.proof.{SequentCalculus => SC}
+import lisa.utils.Helpers.{_, given}
+import lisa.utils.Library
+import lisa.utils.tactics.BasicStepTactic.SCSubproof
+import lisa.utils.tactics.ProofStepLib.{_, given}
+
+object SimpleDeducedSteps {
+
+ case object Restate extends ProofStepWithoutBot with ProofStepWithoutBotNorPrem(1) {
+ override val premises: Seq[Int] = Seq()
+ def asSCProof(bot: Sequent, currentProof: Library#Proof): ProofStepJudgement =
+ SC.RewriteTrue(bot)
+
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
+ SC.Rewrite(bot, premises(0))
+
+ }
+
+ case class FormulaDischarge(f: FOL.Formula) extends ProofStepWithoutPrem {
+ override def asSCProof(premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ val t1 = premises(0)
+ val (lastStep, t2) = currentProof.mostRecentStep
+ SC.Cut((lastStep.bot -< f) ++ (currentProof.getSequent(t1) -> f), t1, t2, f)
+ }
+ }
+
+ class SUBPROOF(computeProof: => Unit)(using String => Unit)(using finishOutput: Throwable => Nothing) extends ProofStepWithoutBot {
+ private def cp(): Unit = computeProof
+ val premises: Seq[lisa.utils.Library#Proof#Fact] = Seq()
+
+ override def asSCProof(bot: Sequent, currentProof: Library#Proof): ProofStepJudgement = {
+ val proof = currentProof.subproof(cp())
+ val scproof = proof.toSCProof
+ val check = SCProofChecker.checkSCProof(scproof)
+ if (!check.isValid) check.showAndGet
+ SC.SCSubproof(scproof, proof.getImports.map(imf => imf.reference.asInstanceOf[Int]))
+ }
+ }
+
+ case object Discharge extends ProofStepWithoutPrem {
+ override def asSCProof(premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ val s = currentProof.getSequent(premises(0))
+ if (s.right.size == 1) {
+ val f = s.right.head
+ val t1 = premises(0)
+ val (lastStep, t2) = currentProof.mostRecentStep
+ SC.Cut((lastStep.bot -< f) ++ (currentProof.getSequent(t1) -> f), t1, t2, f)
+ } else {
+ ProofStepJudgement.InvalidProofStep(this.asProofStep(premises), "When discharging this way, the target sequent must have only a single formula on the right handside.")
+ }
+ }
+ def apply(f: FOL.Formula): FormulaDischarge = FormulaDischarge(f)
+ def apply(ij: Library#Proof#Fact)(using library: Library)(using String => Unit)(using finishOutput: Throwable => Nothing): Unit = {
+ if (library.proofStack.head.validInThisProof(ij)) {
+ Discharge.asProofStep(Seq(ij)).validate(library)
+ } else {
+ val inv = ProofStepJudgement.InvalidProofStep(Discharge.asProofStep(Seq(ij)), "Illegal reference to justification from another proof in proofstep Discharge.")
+ finishOutput(inv.launch)
+ }
+ }
+ }
+
+ /**
+ * Instantiate universal quantifier
+ *
+ * The premise is a proof of φ (phi), with φ (phi) of the form ∀x.ψ
+ *
+ * t is the term to instantiate the quantifier with
+ *
+ * <pre>
+ * Γ ⊢ ∀x.ψ, Δ
+ * -------------------------
+ * Γ |- ψ[t/x], Δ
+ *
+ * </pre>
+ *
+ * Returns a subproof containing the instantiation steps
+ */
+ case class InstantiateForall(phi: FOL.Formula, t: FOL.Term) extends ProofStepWithoutPrem with ProofStepWithoutBotNorPrem(1) {
+
+ override def asSCProof(premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+
+ phi match {
+ case psi @ FOL.BinderFormula(FOL.Forall, _, _) => {
+ val in = FOL.instantiateBinder(psi, t)
+
+ this.asSCProof(currentProof.getSequent(premises(0)) -> phi +> in, premises, currentProof)
+ }
+ case _ => ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(() |- ()), "Input formula is not universally quantified")
+ }
+
+ }
+
+ override def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+
+ val premiseSequent = currentProof.getSequent(premises(0))
+
+ if (premiseSequent.right.contains(phi)) {
+ // valid derivation, construct proof
+
+ phi match {
+ case psi @ FOL.BinderFormula(FOL.Forall, _, _) => {
+
+ val tempVar = FOL.VariableLabel(FOL.freshId(psi.freeVariables.map(_.id), "x"))
+
+ // instantiate the formula with input
+ val in = FOL.instantiateBinder(psi, t)
+
+ // construct proof
+ val p0 = SC.Hypothesis(in |- in, in)
+ val p1 = SC.LeftForall(phi |- in, 0, FOL.instantiateBinder(psi, tempVar), tempVar, t)
+ val p2 = SC.Cut(bot, -1, 1, phi)
+
+ /**
+ * in = ψ[t/x]
+ *
+ * s1 = Γ ⊢ ∀x.ψ, Δ Premise
+ * bot = Γ ⊢ ψ[t/x], Δ Result
+ *
+ * p0 = ψ[t/x] ⊢ ψ[t/x] Hypothesis
+ * p1 = ∀x.ψ ⊢ ψ[t/x] LeftForall p0
+ * p2 = Γ ⊢ ψ[t/x], Δ Cut s1, p1
+ */
+
+ SC.SCSubproof(SCProof(IndexedSeq(p0, p1, p2), IndexedSeq(premiseSequent)), Seq(premises(0)))
+ }
+ case _ => ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Input formula is not universally quantified")
+ }
+ } else ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Input formula was not found in the RHS of the premise sequent.")
+ }
+ }
+
+ /**
+ * Instantiate universal quantifier, with only one formula in the RHS
+ *
+ * The premise is a proof of φ (phi), with φ (phi) of the form ∀x.ψ,
+ *
+ * Asserts φ (phi) as the sole formula in the RHS of the premise's conclusion
+ *
+ * t is the term to instantiate the quantifier with
+ *
+ * <pre>
+ * Γ ⊢ ∀x.ψ
+ * -------------------------
+ * Γ |- ψ[t/x]
+ *
+ * </pre>
+ *
+ * Returns a subproof containing the instantiation steps
+ */
+ case class InstantiateForallWithoutFormula(t: FOL.Term) extends ProofStepWithoutPrem with ProofStepWithoutBotNorPrem(1) {
+
+ override def asSCProof(premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ val premiseSequent = currentProof.getSequent(premises(0))
+
+ if (premiseSequent.right.tail.isEmpty)
+ InstantiateForall(premiseSequent.right.head, t).asSCProof(premises, currentProof)
+ else
+ ProofStepJudgement.InvalidProofStep(this.asProofStep(premises), "RHS of premise sequent is not a singleton.")
+ }
+
+ override def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ val premiseSequent = currentProof.getSequent(premises(0))
+
+ if (premiseSequent.right.tail.isEmpty) {
+ // well formed
+ InstantiateForall(premiseSequent.right.head, t).asSCProof(bot, premises, currentProof)
+ } else ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "RHS of premise sequent is not a singleton.")
+
+ }
+ }
+
+ /**
+ * Instantiate multiple universal quantifiers
+ *
+ * The premise is a proof of φ (phi), with φ (phi) of the form ∀x1, x2, ..., xn.ψ,
+ *
+ * t* are the terms to instantiate the quantifiers
+ *
+ * Asserts t*.length = n
+ *
+ * Returns a subproof containing individual instantiations as its subproof steps
+ *
+ * <pre>
+ * Γ ⊢ ∀x1, x2, ..., xn .ψ, Δ
+ * --------------------------------------------
+ * Γ |- ψ[t1/x1, t2/x2, ..., tn/xn], Δ
+ *
+ * </pre>
+ */
+ case class InstantiateForallMultiple(phi: FOL.Formula, t: FOL.Term*) extends ProofStepWithoutPrem with ProofStepWithoutBotNorPrem(1) {
+ override def asSCProof(premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+
+ val premiseSequent = currentProof.getSequent(premises(0))
+
+ if (!premiseSequent.right.contains(phi)) {
+ ProofStepJudgement.InvalidProofStep(this.asProofStep(premises), "Input formula was not found in the RHS of the premise sequent.")
+ } else {
+ val emptyProof = SCProof(IndexedSeq(), IndexedSeq(currentProof.getSequent(premises(0))))
+ val j = ProofStepJudgement.ValidProofStep(SC.Rewrite(premiseSequent, premises(0)))
+
+ // some unfortunate code reuse
+ // DoubleStep tactics cannot be composed easily at the moment
+
+ val res = t.foldLeft((emptyProof, phi, j: ProofStepJudgement)) {
+ case ((p, f, j), t) => {
+ j match {
+ case ProofStepJudgement.InvalidProofStep(_, _) => (p, f, j) // propagate error
+ case ProofStepJudgement.ValidProofStep(_) => {
+ // good state, continue instantiating
+
+ // by construction the premise is well-formed
+
+ // verify the formula structure and instantiate
+ f match {
+ case psi @ FOL.BinderFormula(FOL.Forall, _, _) => {
+
+ val tempVar = FOL.VariableLabel(FOL.freshId(psi.freeVariables.map(_.id), "x"))
+
+ // instantiate the formula with input
+ val in = FOL.instantiateBinder(psi, t)
+ val bot = p.conclusion -> f +> in
+
+ // construct proof
+ val p0 = SC.Hypothesis(in |- in, in)
+ val p1 = SC.LeftForall(f |- in, 0, FOL.instantiateBinder(psi, tempVar), tempVar, t)
+ val p2 = SC.Cut(bot, -1, 1, f)
+
+ /**
+ * in = ψ[t/x]
+ *
+ * s1 = Γ ⊢ ∀x.ψ, Δ Premise
+ * bot = Γ ⊢ ψ[t/x], Δ Result
+ *
+ * p0 = ψ[t/x] ⊢ ψ[t/x] Hypothesis
+ * p1 = ∀x.ψ ⊢ ψ[t/x] LeftForall p0
+ * p2 = Γ ⊢ ψ[t/x], Δ Cut s1, p1
+ */
+
+ val newStep = SC.SCSubproof(SCProof(IndexedSeq(p0, p1, p2), IndexedSeq(p.conclusion)), Seq(p.length - 1))
+
+ (
+ p withNewSteps IndexedSeq(newStep),
+ in,
+ j
+ )
+ }
+ case _ => {
+ (
+ p,
+ f,
+ ProofStepJudgement.InvalidProofStep(this.asProofStep(premises), "Input formula is not universally quantified")
+ )
+ }
+ }
+ }
+ }
+ }
+ }
+
+ res._3 match {
+ case ProofStepJudgement.InvalidProofStep(_, _) => res._3
+ case ProofStepJudgement.ValidProofStep(_) => SC.SCSubproof(res._1, Seq(premises(0)))
+ }
+ }
+ }
+
+ override def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ val res = this.asSCProof(premises, currentProof)
+
+ res match {
+ case ProofStepJudgement.InvalidProofStep(_, _) => res
+ case ProofStepJudgement.ValidProofStep(SC.SCSubproof(proof: SCProof, _, _)) => {
+ // check if the same sequent was obtained
+ SC.SCSubproof(
+ proof withNewSteps IndexedSeq(SC.Rewrite(bot, proof.length - 1)),
+ Seq(premises(0))
+ )
+ }
+ case _ => ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Unreachable pattern match")
+ }
+ }
+
+ }
+
+ /**
+ * Instantiate multiple universal quantifiers, with only one formula in the RHS
+ *
+ * The premise is a proof of φ (phi), with φ (phi) of the form ∀x1, x2, ..., xn.ψ,
+ *
+ * Asserts φ (phi) is the sole formula in the RHS of the conclusion of the premise
+ *
+ * t* are the terms to instantiate the quantifiers
+ *
+ * Asserts t*.length = n
+ *
+ * Returns a subproof containing individual instantiations as its subproof steps
+ *
+ * <pre>
+ * Γ ⊢ ∀x1, x2, ..., xn .ψ
+ * --------------------------------------------
+ * Γ |- ψ[t1/x1, t2/x2, ..., tn/xn]
+ *
+ * </pre>
+ */
+ case class InstantiateForallMultipleWithoutFormula(t: FOL.Term*) extends ProofStepWithoutPrem with ProofStepWithoutBotNorPrem(1) {
+ override def asSCProof(premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+
+ val prem = currentProof.getSequent(premises(0))
+
+ if (prem.right.tail.isEmpty) {
+ // well formed
+ InstantiateForall(prem.right.head, t: _*).asSCProof(premises, currentProof)
+ } else ProofStepJudgement.InvalidProofStep(this.asProofStep(premises), "RHS of premise sequent is not a singleton.")
+
+ }
+
+ override def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+
+ val prem = currentProof.getSequent(premises(0))
+
+ if (prem.right.tail.isEmpty) {
+ // well formed
+ InstantiateForall(prem.right.head, t: _*).asSCProof(bot, premises, currentProof)
+ } else ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "RHS of premise sequent is not a singleton.")
+
+ }
+
+ }
+
+ /**
+ * Overload instantiation for ease of use
+ *
+ * Generates a proof step of the relevant type
+ */
+ object InstantiateForall {
+
+ // default, automatic
+ // def apply(phi: FOL.Formula, t: FOL.Term) = InstantiateForall(phi, t)
+ def apply(t: FOL.Term) = InstantiateForallWithoutFormula(t)
+ def apply(phi: FOL.Formula, t: FOL.Term*) = InstantiateForallMultiple(phi, t: _*)
+ def apply(t: FOL.Term*) = InstantiateForallMultipleWithoutFormula(t: _*)
+ }
+
+ /**
+ * Performs a cut when the formula to be used as pivot for the cut is
+ * inside a conjunction, preserving the conjunction structure
+ *
+ * <pre>
+ *
+ * PartialCut(ϕ, ϕ ∧ ψ)(left, right) :
+ *
+ * left: Γ ⊢ ϕ ∧ ψ, Δ right: ϕ, Σ ⊢ γ1 , γ2, …, γn
+ * -----------------------------------------------------------
+ * Γ, Σ ⊢ Δ, ψ ∧ γ1, ψ ∧ γ2, … , ψ ∧ γn
+ *
+ * </pre>
+ */
+ case class PartialCut(phi: FOL.Formula, conjunction: FOL.Formula) extends ProofStepWithoutBotNorPrem(2) {
+ override def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+
+ def invalid(message: String) = ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), message)
+
+ val leftSequent = currentProof.getSequent(premises(0))
+ val rightSequent = currentProof.getSequent(premises(1))
+
+ if (leftSequent.right.contains(conjunction)) {
+
+ if (rightSequent.left.contains(phi)) {
+ // check conjunction matches with phi
+ conjunction match {
+ case FOL.ConnectorFormula(FOL.And, s: Seq[FOL.Formula]) => {
+ if (s.contains(phi)) {
+ // construct proof
+
+ val psi: Seq[FOL.Formula] = s.filterNot(_ == phi)
+ val newConclusions: Set[FOL.Formula] = rightSequent.right.map((f: FOL.Formula) => FOL.ConnectorFormula(FOL.And, f +: psi))
+
+ val Sigma: Set[FOL.Formula] = rightSequent.left - phi
+
+ val p0 = SC.Weakening(rightSequent ++< (psi |- ()), -2)
+ val p1 = SC.RewriteTrue(psi |- psi)
+
+ // TODO: can be abstracted into a RightAndAll step
+ val emptyProof = SCProof(IndexedSeq(), IndexedSeq(p0.bot, p1.bot))
+ val proofRightAndAll = rightSequent.right.foldLeft(emptyProof) { case (p, gamma) =>
+ p withNewSteps IndexedSeq(SC.RightAnd(p.conclusion -> gamma +> FOL.ConnectorFormula(FOL.And, gamma +: psi), Seq(p.length - 1, -2), gamma +: psi))
+ }
+
+ val p2 = SC.SCSubproof(proofRightAndAll, Seq(0, 1))
+ val p3 = SC.Rewrite(Sigma + conjunction |- newConclusions, 2) // sanity check and correct form
+ val p4 = SC.Cut(bot, -1, 3, conjunction)
+
+ /**
+ * newConclusions = ψ ∧ γ1, ψ ∧ γ2, … , ψ ∧ γn
+ *
+ * left = Γ ⊢ ϕ ∧ ψ, Δ Premise
+ * right = ϕ, Σ ⊢ γ1 , γ2, …, γn Premise
+ *
+ * p0 = ϕ, Σ, ψ ⊢ γ1 , γ2, …, γn Weakening on right
+ * p1 = ψ ⊢ ψ Hypothesis
+ * p2 = Subproof:
+ * 2.1 = ϕ, Σ, ψ ⊢ ψ ∧ γ1 , γ2, …, γn RightAnd on p0 and p1 with ψ ∧ γ1
+ * 2.2 = ϕ, Σ, ψ ⊢ ψ ∧ γ1 , ψ ∧ γ2, …, γn RightAnd on 2.1 and p1 ψ ∧ γ2
+ * ...
+ * 2.n = ϕ, Σ, ψ ⊢ ψ ∧ γ1, ψ ∧ γ2, …, ψ ∧ γn RightAnd on 2.(n-1) and p1 with ψ ∧ γn
+ *
+ * p3 = ϕ ∧ ψ, Σ ⊢ ψ ∧ γ1, ψ ∧ γ2, … , ψ ∧ γn Rewrite on p2 (just to have a cleaner form)
+ * p2 = Γ, Σ ⊢ Δ, ψ ∧ γ1, ψ ∧ γ2, … , ψ ∧ γn Cut on left, p1 with ϕ ∧ ψ
+ *
+ * p2 is the result
+ */
+
+ SC.SCSubproof(SCProof(IndexedSeq(p0, p1, p2, p3, p4), IndexedSeq(leftSequent, rightSequent)), premises.take(2))
+ } else {
+ invalid("Input conjunction does not contain the pivot.")
+ }
+ }
+ case _ => invalid("Input not a conjunction.")
+ }
+ } else {
+ invalid("Input pivot formula not found in right premise.")
+ }
+ } else {
+ invalid("Input conjunction not found in first premise.")
+ }
+ }
+ }
+
+}
diff --git a/lisa-utils/src/main/scala/lisa/utils/tactics/WithProofs.scala b/lisa-utils/src/main/scala/lisa/utils/tactics/WithProofs.scala
new file mode 100644
index 00000000..83211097
--- /dev/null
+++ b/lisa-utils/src/main/scala/lisa/utils/tactics/WithProofs.scala
@@ -0,0 +1,255 @@
+package lisa.utils.tactics
+
+import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.RunningTheory
+import lisa.kernel.proof.SCProof
+import lisa.kernel.proof.SequentCalculus.Sequent
+import lisa.utils.Library
+import lisa.utils.tactics.ProofStepJudgement.EarlyProofStepException
+import lisa.utils.tactics.ProofStepJudgement.InvalidProofStep
+import lisa.utils.tactics.ProofStepJudgement.ValidProofStep
+import lisa.utils.tactics.ProofStepLib.ProofStep
+
+import scala.collection.mutable.{Buffer => mBuf}
+import scala.collection.mutable.{Map => mMap}
+
+trait WithProofs extends ProofsHelpers {
+ library: Library =>
+
+ class Proof(assumpts: List[Formula] = Nil) {
+ type OutsideFact = (theory.Justification | Proof#DoubleStep)
+ // Maintaining the current state of the proof if an imperative environment //
+ private val that: Proof = this
+ private var steps: List[DoubleStep] = Nil
+ private var imports: List[ImportedFact] = Nil
+ private var assumptions: List[Formula] = assumpts
+ private var discharges: List[Fact] = Nil
+
+ private val justMap: mMap[OutsideFact, ImportedFact] = mMap()
+
+ private val parent: Option[Proof] = if (proofStack.isEmpty) None else Some(proofStack(0))
+
+ /**
+ * A step that has been added to a proof and its equivalent in pure sequent calculus.
+ */
+ case class DoubleStep private (ps: ProofStep, scps: SCProofStep, position: Int) {
+ val bot: Sequent = scps.bot
+ }
+
+ /**
+ * An import (theorem, axiom or definition) that has been added to the current proof.
+ */
+ case class ImportedFact private (of: OutsideFact, seq: Sequent, position: Int, reference: Int | theory.Justification) {}
+
+ /**
+ * The type of object which can be used as premises of proofsteps, similar to integers in pure sequent calculus.
+ */
+ type Fact = DoubleStep | OutsideFact | ImportedFact | Int
+
+ private def addStep(ds: DoubleStep): Unit = steps = ds :: steps
+ private def addImport(ji: ImportedFact): Unit = {
+ justMap.update(ji.of, ji)
+ imports = ji :: imports
+ }
+
+ // Setters //
+
+ /**
+ * @param f add the formula f as an assumption on the left handsides of all further (manually written) proofsteps in the proof.
+ */
+ def addAssumption(f: Formula): Unit = {
+ if (!assumptions.contains(f)) assumptions = f :: assumptions
+ }
+
+ /**
+ * @param ji Automatically discharge (by applying Cut rule) the given justification at the end of the proof.
+ */
+ def addDischarge(ji: Fact): Unit = {
+ if (!discharges.contains(ji)) discharges = ji :: discharges
+ }
+
+ private object DoubleStep {
+ def newDoubleStep(ps: ProofStep)(using output: String => Unit)(using finishOutput: Throwable => Nothing): DoubleStep = {
+ val judgement = ps.asSCProof(that)
+ judgement match {
+ case ValidProofStep(scps) =>
+ val ds = DoubleStep(ps, scps, steps.length)
+ addStep(ds)
+ ds
+ case InvalidProofStep(ps, message) =>
+ output(s"$message\n")
+ finishOutput(EarlyProofStepException(message))
+ }
+ }
+ }
+
+ /**
+ * Add a new proof step to the proof
+ */
+ def newDoubleStep(ps: ProofStep)(using output: String => Unit)(using finishOutput: Throwable => Nothing): DoubleStep =
+ DoubleStep.newDoubleStep(ps: ProofStep)
+
+ private object ImportedFact {
+ def newImportedFact(outFact: OutsideFact): ImportedFact = {
+ if (parent.isEmpty) {
+ outFact match {
+ case just: theory.Justification =>
+ val imf: ImportedFact = ImportedFact(outFact, theory.sequentFromJustification(just), -(imports.length + 1), just)
+ addImport(imf)
+ imf
+ case ds: Proof#DoubleStep => throw InvalidJustificationException(ds)
+ }
+ } else {
+ val (seq, ref) = parent.get.getSequentAndInt(outFact)
+ val imf: ImportedFact = ImportedFact(outFact, seq, -(imports.length + 1), ref)
+ addImport(imf)
+ imf
+ }
+ }
+ }
+
+ /**
+ * Add a new import to the proof.
+ */
+ def newImportedFact(just: theory.Justification): ImportedFact = ImportedFact.newImportedFact(just)
+
+ // Getters //
+
+ /**
+ * Favour using getSequent when applicable.
+ * @return The list of ValidatedSteps (containing a high level ProofStep and the corresponding SCProofStep).
+ */
+ def getSteps: List[DoubleStep] = steps.reverse
+
+ /**
+ * Favour using getSequent when applicable.
+ * @return The list of Imports validated in the formula, with their original justification.
+ */
+ def getImports: List[ImportedFact] = imports.reverse
+
+ /**
+ * @return The list of formulas that are assumed for the reminder of the proof.
+ */
+ def getAssumptions: List[Formula] = assumptions
+
+ /**
+ * @return The list of Formula, typically proved by outer theorems or axioms that will get discharged in the end of the proof.
+ */
+ def getDischarges: List[Fact] = discharges
+
+ /**
+ * Tell if a justification for a ProofStep (an Index, and ProofStep, a theory Justification) is usable in the current proof
+ */
+ def validInThisProof(ij: Library#Proof#Fact): Boolean = ij match {
+ case ds: library.Proof#DoubleStep => ds.isInstanceOf[this.DoubleStep] || (parent.nonEmpty && parent.get.validInThisProof(ij))
+ case ji: library.Proof#ImportedFact => ji.isInstanceOf[this.ImportedFact] || (parent.nonEmpty && parent.get.validInThisProof(ij))
+ case _: Int => true
+ case _: theory.Justification => true
+ case _ => false
+ }
+
+ /**
+ * Tell if a justification for a ProofStep (ad ProofStep, a theory Justification) is usable in the current proof
+ */
+ def validInThisProof(ji: Library#Proof#ImportedFact): Boolean = validInThisProof(ji.asInstanceOf[Library#Proof#Fact])
+
+ /**
+ * Tell if a justification for a ProofStep (ad ProofStep, a theory Justification) is usable in the current proof
+ */
+ def validInThisProof(ds: Library#Proof#DoubleStep): Boolean = validInThisProof(ds.asInstanceOf[Library#Proof#Fact])
+
+ /**
+ * Compute the final, Kernel-pure, SCProof.
+ */
+ def toSCProof(using String => Unit)(using finishOutput: Throwable => Nothing): lisa.kernel.proof.SCProof = {
+ discharges.foreach(i => Discharge(getSequentAndInt(i)._2))
+ SCProof(steps.reverse.map(_.scps).toIndexedSeq, imports.reverse.map(_.seq).toIndexedSeq)
+ }
+
+ /**
+ * Return the Sequent that a given justification proves as well as it's integer position in the steps or imports lists.
+ */
+ def getSequentAndInt(ij: Fact): (Sequent, Int) = {
+ ij match {
+ case ds: DoubleStep =>
+ (ds.bot, ds.position)
+ case ds: Proof#DoubleStep if parent.nonEmpty && parent.get.validInThisProof(ds) =>
+ val r = justMap.get(ds)
+ r match {
+ case Some(importedFact) => getSequentAndInt(importedFact)
+ case None =>
+ getSequentAndInt(ImportedFact.newImportedFact(ds))
+ }
+ case ds: Proof#DoubleStep => throw InvalidJustificationException(ds)
+ case just: theory.Justification =>
+ val r = justMap.get(just)
+ r match {
+ case Some(ji) => getSequentAndInt(ji)
+ case None =>
+ if (parent.isEmpty) getSequentAndInt(ImportedFact.newImportedFact(just))
+ else {
+ val i = parent.get.getSequentAndInt(just)
+ getSequentAndInt(ImportedFact.newImportedFact(just))
+ }
+ }
+ case ji: ImportedFact =>
+ (ji.seq, ji.position)
+ case i: Int =>
+ (
+ if (i >= 0)
+ if (i >= steps.length) throw new IndexOutOfBoundsException(s"index $i is out of bounds of the steps Seq")
+ else steps(steps.length - i - 1).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(imports.length + i).seq
+ },
+ i
+ )
+ }
+ }
+
+ /**
+ * Create a new proof with this proof as parent, execute the given code and then close the created proof (i.e. remove it from the proofstack).
+ */
+ def subproof(proofAction: => Unit): Proof = {
+ assert(proofStack.head == this, "Can only create a subproof in the latest opened Proof.")
+ val p = new Proof(getAssumptions)
+ proofStack.push(p)
+ proofAction
+ proofStack.pop
+ }
+
+ /**
+ * Return the Sequent that a given justification proves in the proof.
+ */
+ def getSequent(ij: Fact): Sequent = getSequentAndInt(ij)._1
+
+ /**
+ * @return the most recently added proofstep.
+ */
+ def mostRecentStep: (DoubleStep, Int) = (steps.head, steps.length - 1)
+
+ /**
+ * @return Current number of steps in the proof.
+ */
+ def length: Int = steps.length
+
+ /**
+ * @return a Set of symbols free in the assumption and which shouldn't be bound or instantiated.
+ */
+ def lockedSymbols: Set[SchematicLabel] = assumptions.toSet.flatMap(f => f.schematicFormulaLabels.toSet[SchematicLabel] ++ f.schematicTermLabels.toSet[SchematicLabel])
+
+ /**
+ * @return The sequent and integer position of a justification in the proof. Alias for [[getSequentAndInt]]
+ */
+ def references(ij: Fact): (Sequent, Int) = getSequentAndInt(ij)
+
+ }
+
+ /**
+ * An error indicating that a given proof step was used in a proof while it does not belong to it or its parents.
+ */
+ case class InvalidJustificationException(ds: Proof#DoubleStep) extends Exception("Reference to a step that does not belong to the current proof or on of its parents.")
+
+}
diff --git a/src/main/scala/lisa/automation/kernel/SimplePropositionalSolver.scala b/src/main/scala/lisa/automation/kernel/SimplePropositionalSolver.scala
index ab43254c..def2e664 100644
--- a/src/main/scala/lisa/automation/kernel/SimplePropositionalSolver.scala
+++ b/src/main/scala/lisa/automation/kernel/SimplePropositionalSolver.scala
@@ -3,7 +3,10 @@ package lisa.automation.kernel
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SequentCalculus.*
-import lisa.utils.Helpers.*
+import lisa.utils.Helpers.{_, given}
+import lisa.utils.Library
+import lisa.utils.tactics.ProofStepJudgement
+import lisa.utils.tactics.ProofStepLib.{_, given}
import scala.collection.mutable.Set as mSet
@@ -165,4 +168,30 @@ object SimplePropositionalSolver {
r4
}
+ case object Trivial extends ProofStepWithoutBot with ProofStepWithoutBotNorPrem(-1) {
+ override val premises: Seq[Int] = Seq()
+ def asSCProof(bot: Sequent, currentProof: Library#Proof): ProofStepJudgement = {
+ ProofStepJudgement.ValidProofStep(SCSubproof(solveSequent(bot)))
+ }
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+
+ val sp = SCSubproof(
+ {
+ val premsFormulas = premises.map(p => (p, sequentToFormula(currentProof.getSequent(p))))
+ val initProof = premsFormulas.map(s => Rewrite(() |- s._2, s._1)).toList
+ val sqToProve = bot ++< (() |- premsFormulas.map(s => s._2).toSet)
+ val subpr = SCSubproof(solveSequent(sqToProve))
+ val n = initProof.length - 1
+ val stepsList = premsFormulas.zipWithIndex.foldLeft[List[SCProofStep]](subpr :: initProof)((prev: List[SCProofStep], cur) => {
+ val ((prem, form), position) = cur
+ Cut(prev.head.bot -< form, position, prev.length - 1, form) :: prev
+ })
+ SCProof(stepsList.reverse.toIndexedSeq, premises.map(p => currentProof.getSequent(p)).toIndexedSeq)
+ },
+ premises
+ )
+ ProofStepJudgement.ValidProofStep(sp)
+ }
+ }
+
}
diff --git a/src/main/scala/lisa/proven/mathematics/Mapping.scala b/src/main/scala/lisa/proven/mathematics/Mapping.scala
index f318e410..f45db00f 100644
--- a/src/main/scala/lisa/proven/mathematics/Mapping.scala
+++ b/src/main/scala/lisa/proven/mathematics/Mapping.scala
@@ -12,7 +12,7 @@ import SetTheory.*
object Mapping extends lisa.Main {
THEOREM("functionalMapping") of
- "∀ 'a. elem('a, 'A) ⇒ (∃! 'x. 'phi('x, 'a)) ⊢ ∃! 'X. ∀ 'x. elem('x, 'X) ↔ (∃ 'a. elem('a, 'A) ∧ 'phi('x, 'a))" PROOF {
+ "∀ 'a. elem('a, 'A) ⇒ (∃! 'x. 'phi('x, 'a)) ⊢ ∃! 'X. ∀ 'x. elem('x, 'X) ↔ (∃ 'a. elem('a, 'A) ∧ 'phi('x, 'a))" PROOF2 {
val a = VariableLabel("a")
val x = VariableLabel("x")
val y = VariableLabel("y")
@@ -30,79 +30,81 @@ object Mapping extends lisa.Main {
val H = existsOne(x, phi(x, a))
val H1 = forall(a, in(a, A) ==> H)
val s0 = hypothesis(H) // () |- existsOne(x, phi(x, a)))
- val s1 = Weakening((H, in(a, A)) |- existsOne(x, phi(x, a)), 0)
- val s2 = Rewrite((H) |- in(a, A) ==> existsOne(x, phi(x, a)), 1)
- // val s3 = RightForall((H) |- forall(a, in(a, A) ==> existsOne(x, phi(x, a))), 2, in(a, A) ==> existsOne(x, phi(x, a)), a) // () |- ∀a∈A. ∃!x. phi(x, a)
+ val s1 = SC.Weakening((H, in(a, A)) |- existsOne(x, phi(x, a)), 0)
+ val s2 = SC.Rewrite((H) |- in(a, A) ==> existsOne(x, phi(x, a)), 1)
+ // val s3 = SC.RightForall((H) |- forall(a, in(a, A) ==> existsOne(x, phi(x, a))), 2, in(a, A) ==> existsOne(x, phi(x, a)), a) // () |- ∀a∈A. ∃!x. phi(x, a)
val s3 = hypothesis(H1)
val i1 = () |- replacementSchema
- val p0 = InstPredSchema(
+ val p0 = SC.InstPredSchema(
() |- instantiatePredicateSchemas(replacementSchema, Map(sPsi -> LambdaTermFormula(Seq(y, a, x), phi(x, a)))),
-1,
Map(sPsi -> LambdaTermFormula(Seq(y, a, x), phi(x, a)))
)
- val p1 = instantiateForall(Proof(steps(p0), imports(i1)), A)
- val s4 = SCSubproof(p1, Seq(-1)) //
- val s5 = Rewrite(s3.bot.right.head |- exists(B, forall(x, in(x, A) ==> exists(y, in(y, B) /\ (phi(y, x))))), 4)
- val s6 = Cut((H1) |- exists(B, forall(x, in(x, A) ==> exists(y, in(y, B) /\ (phi(y, x))))), 3, 5, s3.bot.right.head) // ⊢ ∃B. ∀x. (x ∈ A) ⇒ ∃y. (y ∈ B) ∧ (y = (x, b))
+ val p1 = instantiateForall(SCProof(steps(p0), imports(i1)), A)
+ val s4 = SC.SCSubproof(p1, Seq(-1)) //
+ val s5 = SC.Rewrite(s3.bot.right.head |- exists(B, forall(x, in(x, A) ==> exists(y, in(y, B) /\ (phi(y, x))))), 4)
+ val s6 = SC.Cut((H1) |- exists(B, forall(x, in(x, A) ==> exists(y, in(y, B) /\ (phi(y, x))))), 3, 5, s3.bot.right.head) // ⊢ ∃B. ∀x. (x ∈ A) ⇒ ∃y. (y ∈ B) ∧ (y = (x, b))
val i2 = () |- comprehensionSchema // forall(z, exists(y, forall(x, in(x,y) <=> (in(x,z) /\ sPhi(x,z)))))
- val q0 = InstPredSchema(
+ val q0 = SC.InstPredSchema(
() |- instantiatePredicateSchemas(comprehensionSchema, Map(sPhi -> LambdaTermFormula(Seq(x, z), exists(a, in(a, A) /\ phi(x, a))))),
-1,
Map(sPhi -> LambdaTermFormula(Seq(x, z), exists(a, in(a, A) /\ phi(x, a))))
)
- val q1 = instantiateForall(Proof(steps(q0), imports(i2)), B)
- val s7 = SCSubproof(q1, Seq(-2)) // ∃y. ∀x. (x ∈ y) ↔ (x ∈ B) ∧ ∃a. a ∈ A /\ x = (a, b) := exists(y, F(y) )
- Proof(steps(s0, s1, s2, s3, s4, s5, s6, s7), imports(i1, i2))
- val s8 = SCSubproof({
+ val q1 = instantiateForall(SCProof(steps(q0), imports(i2)), B)
+ val s7 = SC.SCSubproof(q1, Seq(-2)) // ∃y. ∀x. (x ∈ y) ↔ (x ∈ B) ∧ ∃a. a ∈ A /\ x = (a, b) := exists(y, F(y) )
+ SCProof(steps(s0, s1, s2, s3, s4, s5, s6, s7), imports(i1, i2))
+ val s8 = SC.SCSubproof({
val y1 = VariableLabel("y1")
val s0 = hypothesis(in(y1, B))
- val s1 = RightSubstEq((in(y1, B), x === y1) |- in(x, B), 0, List((x, y1)), LambdaTermFormula(Seq(f), in(f, B)))
- val s2 = LeftSubstIff(Set(in(y1, B), (x === y1) <=> phi(x, a), phi(x, a)) |- in(x, B), 1, List(((x === y1), phi(x, a))), LambdaFormulaFormula(Seq(h), h()))
- val s3 = LeftSubstEq(Set(y === y1, in(y1, B), (x === y) <=> phi(x, a), phi(x, a)) |- in(x, B), 2, List((y, y1)), LambdaTermFormula(Seq(f), (x === f) <=> phi(x, a)))
- val s4 = LeftSubstIff(Set((y === y1) <=> phi(y1, a), phi(y1, a), in(y1, B), (x === y) <=> phi(x, a), phi(x, a)) |- in(x, B), 3, List((phi(y1, a), y1 === y)), LambdaFormulaFormula(Seq(h), h()))
- val s5 = LeftForall(Set(forall(x, (y === x) <=> phi(x, a)), phi(y1, a), in(y1, B), (x === y) <=> phi(x, a), phi(x, a)) |- in(x, B), 4, (y === x) <=> phi(x, a), x, y1)
- val s6 = LeftForall(Set(forall(x, (y === x) <=> phi(x, a)), phi(y1, a), in(y1, B), phi(x, a)) |- in(x, B), 5, (x === y) <=> phi(x, a), x, x)
- val s7 = LeftExists(Set(exists(y, forall(x, (y === x) <=> phi(x, a))), phi(y1, a), in(y1, B), phi(x, a)) |- in(x, B), 6, forall(x, (y === x) <=> phi(x, a)), y)
- val s8 = Rewrite(Set(exists(y, forall(x, (y === x) <=> phi(x, a))), phi(y1, a) /\ in(y1, B), phi(x, a)) |- in(x, B), 7)
- val s9 = LeftExists(Set(exists(y, forall(x, (y === x) <=> phi(x, a))), exists(y1, phi(y1, a) /\ in(y1, B)), phi(x, a)) |- in(x, B), 8, phi(y1, a) /\ in(y1, B), y1)
- val s10 = Rewrite(Set(exists(y, forall(x, (y === x) <=> phi(x, a))), True ==> exists(y, phi(y, a) /\ in(y, B)), phi(x, a)) |- in(x, B), 9)
- val s11 = LeftSubstIff(
+ val s1 = SC.RightSubstEq((in(y1, B), x === y1) |- in(x, B), 0, List((x, y1)), LambdaTermFormula(Seq(f), in(f, B)))
+ val s2 = SC.LeftSubstIff(Set(in(y1, B), (x === y1) <=> phi(x, a), phi(x, a)) |- in(x, B), 1, List(((x === y1), phi(x, a))), LambdaFormulaFormula(Seq(h), h()))
+ val s3 = SC.LeftSubstEq(Set(y === y1, in(y1, B), (x === y) <=> phi(x, a), phi(x, a)) |- in(x, B), 2, List((y, y1)), LambdaTermFormula(Seq(f), (x === f) <=> phi(x, a)))
+ val s4 =
+ SC.LeftSubstIff(Set((y === y1) <=> phi(y1, a), phi(y1, a), in(y1, B), (x === y) <=> phi(x, a), phi(x, a)) |- in(x, B), 3, List((phi(y1, a), y1 === y)), LambdaFormulaFormula(Seq(h), h()))
+ val s5 = SC.LeftForall(Set(forall(x, (y === x) <=> phi(x, a)), phi(y1, a), in(y1, B), (x === y) <=> phi(x, a), phi(x, a)) |- in(x, B), 4, (y === x) <=> phi(x, a), x, y1)
+ val s6 = SC.LeftForall(Set(forall(x, (y === x) <=> phi(x, a)), phi(y1, a), in(y1, B), phi(x, a)) |- in(x, B), 5, (x === y) <=> phi(x, a), x, x)
+ val s7 = SC.LeftExists(Set(exists(y, forall(x, (y === x) <=> phi(x, a))), phi(y1, a), in(y1, B), phi(x, a)) |- in(x, B), 6, forall(x, (y === x) <=> phi(x, a)), y)
+ val s8 = SC.Rewrite(Set(exists(y, forall(x, (y === x) <=> phi(x, a))), phi(y1, a) /\ in(y1, B), phi(x, a)) |- in(x, B), 7)
+ val s9 = SC.LeftExists(Set(exists(y, forall(x, (y === x) <=> phi(x, a))), exists(y1, phi(y1, a) /\ in(y1, B)), phi(x, a)) |- in(x, B), 8, phi(y1, a) /\ in(y1, B), y1)
+ val s10 = SC.Rewrite(Set(exists(y, forall(x, (y === x) <=> phi(x, a))), True ==> exists(y, phi(y, a) /\ in(y, B)), phi(x, a)) |- in(x, B), 9)
+ val s11 = SC.LeftSubstIff(
Set(exists(y, forall(x, (y === x) <=> phi(x, a))), in(a, A) ==> exists(y, phi(y, a) /\ in(y, B)), phi(x, a), in(a, A)) |- in(x, B),
10,
List((True, in(a, A))),
LambdaFormulaFormula(Seq(h), h() ==> exists(y, phi(y, a) /\ in(y, B)))
)
- val s12 = LeftForall(
+ val s12 = SC.LeftForall(
Set(exists(y, forall(x, (y === x) <=> phi(x, a))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), phi(x, a), in(a, A)) |- in(x, B),
11,
in(a, A) ==> exists(y, phi(y, a) /\ in(y, B)),
a,
a
)
- val s13 = LeftSubstIff(
+ val s13 = SC.LeftSubstIff(
Set(in(a, A) ==> exists(y, forall(x, (y === x) <=> phi(x, a))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), phi(x, a), in(a, A)) |- in(x, B),
12,
List((True, in(a, A))),
LambdaFormulaFormula(Seq(h), h() ==> exists(y, forall(x, (y === x) <=> phi(x, a))))
)
- val s14 = LeftForall(
+ val s14 = SC.LeftForall(
Set(forall(a, in(a, A) ==> exists(y, forall(x, (y === x) <=> phi(x, a)))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), phi(x, a), in(a, A)) |- in(x, B),
13,
in(a, A) ==> exists(y, forall(x, (y === x) <=> phi(x, a))),
a,
a
)
- val s15 = Rewrite(Set(forall(a, in(a, A) ==> exists(y, forall(x, (y === x) <=> phi(x, a)))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), phi(x, a) /\ in(a, A)) |- in(x, B), 14)
- val s16 = LeftExists(
+ val s15 =
+ SC.Rewrite(Set(forall(a, in(a, A) ==> exists(y, forall(x, (y === x) <=> phi(x, a)))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), phi(x, a) /\ in(a, A)) |- in(x, B), 14)
+ val s16 = SC.LeftExists(
Set(forall(a, in(a, A) ==> exists(y, forall(x, (y === x) <=> phi(x, a)))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), exists(a, phi(x, a) /\ in(a, A))) |- in(x, B),
15,
phi(x, a) /\ in(a, A),
a
)
val truc = forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B)))
- val s17 = Rewrite(Set(forall(a, in(a, A) ==> existsOne(x, phi(x, a))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), exists(a, phi(x, a) /\ in(a, A))) |- in(x, B), 16)
- Proof(steps(s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, s17))
+ val s17 = SC.Rewrite(Set(forall(a, in(a, A) ==> existsOne(x, phi(x, a))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), exists(a, phi(x, a) /\ in(a, A))) |- in(x, B), 16)
+ SCProof(steps(s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, s17))
// goal H, ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), ∃a. a ∈ A ∧ phi(x, a) |- (x ∈ B)
// redGoal ∀a.(a ∈ A) => ∃!x. phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), ∃a. a ∈ A ∧ phi(x, a) |- (x ∈ B) s17
// redGoal ∀a.(a ∈ A) => ∃y. ∀x. (x=y) ↔ phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), ∃a. a ∈ A ∧ phi(x, a) |- (x ∈ B) s16
@@ -128,31 +130,31 @@ object Mapping extends lisa.Main {
val G = forall(a, in(a, A) ==> exists(y, in(y, B) /\ (phi(y, a))))
val F = forall(x, iff(in(x, B1), in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a)))))
- val s9 = SCSubproof({
- val p0 = instantiateForall(Proof(hypothesis(F)), x)
+ val s9 = SC.SCSubproof({
+ val p0 = instantiateForall(SCProof(hypothesis(F)), x)
val left = in(x, B1)
val right = in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a)))
- val p1 = p0.withNewSteps(Vector(Rewrite(F |- (left ==> right) /\ (right ==> left), p0.length - 1)))
+ val p1 = p0.withNewSteps(Vector(SC.Rewrite(F |- (left ==> right) /\ (right ==> left), p0.length - 1)))
val p2 = destructRightAnd(p1, (right ==> left), (left ==> right)) // F |- in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a))) => in(x, B1)
- val p3 = p2.withNewSteps(Vector(Rewrite(Set(F, in(x, B), exists(a, in(a, A) /\ (phi(x, a)))) |- in(x, B1), p2.length - 1)))
+ val p3 = p2.withNewSteps(Vector(SC.Rewrite(Set(F, in(x, B), exists(a, in(a, A) /\ (phi(x, a)))) |- in(x, B1), p2.length - 1)))
p3
}) // have F, (x ∈ B), ∃a. a ∈ A ∧ x = (a, b) |- (x ∈ B1)
- val s10 = Cut(Set(F, G, H1, exists(a, in(a, A) /\ (phi(x, a)))) |- in(x, B1), 8, 9, in(x, B)) // redGoal F, ∃a. a ∈ A ∧ x = (a, b), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ y = (a, b) |- (x ∈ B1)
- val s11 = Rewrite(Set(H1, G, F) |- exists(a, in(a, A) /\ (phi(x, a))) ==> in(x, B1), 10) // F |- ∃a. a ∈ A ∧ x = (a, b) => (x ∈ B1) --- half
- val s12 = SCSubproof({
- val p0 = instantiateForall(Proof(hypothesis(F)), x)
+ val s10 = SC.Cut(Set(F, G, H1, exists(a, in(a, A) /\ (phi(x, a)))) |- in(x, B1), 8, 9, in(x, B)) // redGoal F, ∃a. a ∈ A ∧ x = (a, b), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ y = (a, b) |- (x ∈ B1)
+ val s11 = SC.Rewrite(Set(H1, G, F) |- exists(a, in(a, A) /\ (phi(x, a))) ==> in(x, B1), 10) // F |- ∃a. a ∈ A ∧ x = (a, b) => (x ∈ B1) --- half
+ val s12 = SC.SCSubproof({
+ val p0 = instantiateForall(SCProof(hypothesis(F)), x)
val left = in(x, B1)
val right = in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a)))
- val p1 = p0.withNewSteps(Vector(Rewrite(F |- (left ==> right) /\ (right ==> left), p0.length - 1)))
+ val p1 = p0.withNewSteps(Vector(SC.Rewrite(F |- (left ==> right) /\ (right ==> left), p0.length - 1)))
val p2 = destructRightAnd(p1, (left ==> right), (right ==> left)) // F |- in(x, B1) => in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a))) =>
- val p3 = p2.withNewSteps(Vector(Rewrite(Set(F, in(x, B1)) |- exists(a, in(a, A) /\ (phi(x, a))) /\ in(x, B), p2.length - 1)))
+ val p3 = p2.withNewSteps(Vector(SC.Rewrite(Set(F, in(x, B1)) |- exists(a, in(a, A) /\ (phi(x, a))) /\ in(x, B), p2.length - 1)))
val p4 = destructRightAnd(p3, exists(a, in(a, A) /\ (phi(x, a))), in(x, B))
- val p5 = p4.withNewSteps(Vector(Rewrite(F |- in(x, B1) ==> exists(a, in(a, A) /\ (phi(x, a))), p4.length - 1)))
+ val p5 = p4.withNewSteps(Vector(SC.Rewrite(F |- in(x, B1) ==> exists(a, in(a, A) /\ (phi(x, a))), p4.length - 1)))
p5
}) // have F |- (x ∈ B1) ⇒ ∃a. a ∈ A ∧ x = (a, b) --- other half
- val s13 = RightIff((H1, G, F) |- in(x, B1) <=> exists(a, in(a, A) /\ (phi(x, a))), 11, 12, in(x, B1), exists(a, in(a, A) /\ (phi(x, a)))) // have F |- (x ∈ B1) <=> ∃a. a ∈ A ∧ x = (a, b)
+ val s13 = SC.RightIff((H1, G, F) |- in(x, B1) <=> exists(a, in(a, A) /\ (phi(x, a))), 11, 12, in(x, B1), exists(a, in(a, A) /\ (phi(x, a)))) // have F |- (x ∈ B1) <=> ∃a. a ∈ A ∧ x = (a, b)
val s14 =
- RightForall(
+ SC.RightForall(
(H1, G, F) |- forall(x, in(x, B1) <=> exists(a, in(a, A) /\ (phi(x, a)))),
13,
in(x, B1) <=> exists(a, in(a, A) /\ (phi(x, a))),
@@ -160,46 +162,49 @@ object Mapping extends lisa.Main {
) // G, F |- ∀x. (x ∈ B1) <=> ∃a. a ∈ A ∧ x = (a, b)
val i3 = () |- extensionalityAxiom
- val s15 = SCSubproof(
+ val s15 = SC.SCSubproof(
{
val i1 = s13.bot // G, F |- (x ∈ B1) <=> ∃a. a ∈ A ∧ x = (a, b)
val i2 = () |- extensionalityAxiom
- val t0 = RightSubstIff(
+ val t0 = SC.RightSubstIff(
Set(H1, G, F, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))) |- in(x, X) <=> in(x, B1),
-1,
List((in(x, X), exists(a, in(a, A) /\ (phi(x, a))))),
LambdaFormulaFormula(Seq(h), h() <=> in(x, B1))
) // redGoal2 F, (z ∈ X) <=> ∃a. a ∈ A ∧ z = (a, b) |- (z ∈ X) <=> (z ∈ B1)
- val t1 = LeftForall(
+ val t1 = SC.LeftForall(
Set(H1, G, F, forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))) |- in(x, X) <=> in(x, B1),
0,
in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))),
x,
x
) // redGoal2 F, [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] |- (z ∈ X) <=> (z ∈ B1)
- val t2 = RightForall(t1.bot.left |- forall(x, in(x, X) <=> in(x, B1)), 1, in(x, X) <=> in(x, B1), x) // redGoal2 F, [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] |- ∀z. (z ∈ X) <=> (z ∈ B1)
+ val t2 = SC.RightForall(t1.bot.left |- forall(x, in(x, X) <=> in(x, B1)), 1, in(x, X) <=> in(x, B1), x) // redGoal2 F, [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] |- ∀z. (z ∈ X) <=> (z ∈ B1)
val t3 =
- SCSubproof(instantiateForall(Proof(steps(Rewrite(() |- extensionalityAxiom, -1)), imports(() |- extensionalityAxiom)), X, B1), Vector(-2)) // (∀z. (z ∈ X) <=> (z ∈ B1)) <=> (X === B1)))
- val t4 = RightSubstIff(
+ SC.SCSubproof(
+ instantiateForall(SCProof(steps(SC.Rewrite(() |- extensionalityAxiom, -1)), imports(() |- extensionalityAxiom)), X, B1),
+ Vector(-2)
+ ) // (∀z. (z ∈ X) <=> (z ∈ B1)) <=> (X === B1)))
+ val t4 = SC.RightSubstIff(
t1.bot.left ++ t3.bot.right |- X === B1,
2,
List((X === B1, forall(z, in(z, X) <=> in(z, B1)))),
LambdaFormulaFormula(Seq(h), h())
) // redGoal2 F, [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)], (∀z. (z ∈ X) <=> (z ∈ B1)) <=> (X === B1))) |- X=B1
- val t5 = Cut(t1.bot.left |- X === B1, 3, 4, t3.bot.right.head) // redGoal2 F, [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] |- X=B1
- val t6 = Rewrite(Set(H1, G, F) |- forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))) ==> (X === B1), 5) // F |- [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] ==> X=B1
+ val t5 = SC.Cut(t1.bot.left |- X === B1, 3, 4, t3.bot.right.head) // redGoal2 F, [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] |- X=B1
+ val t6 = SC.Rewrite(Set(H1, G, F) |- forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))) ==> (X === B1), 5) // F |- [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] ==> X=B1
val i3 = s14.bot // F |- ∀x. (x ∈ B1) <=> ∃a. a ∈ A ∧ x = (a, b)
- val t7 = RightSubstEq(
+ val t7 = SC.RightSubstEq(
Set(H1, G, F, X === B1) |- forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))),
-3,
List((X, B1)),
LambdaTermFormula(Seq(f), forall(x, in(x, f) <=> exists(a, in(a, A) /\ phi(x, a))))
) // redGoal1 F, X=B1 |- [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
- val t8 = Rewrite(
+ val t8 = SC.Rewrite(
Set(H1, G, F) |- X === B1 ==> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))),
7
) // redGoal1 F |- X=B1 ==> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] -------second half with t6
- val t9 = RightIff(
+ val t9 = SC.RightIff(
Set(H1, G, F) |- (X === B1) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))),
6,
8,
@@ -207,36 +212,36 @@ object Mapping extends lisa.Main {
forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))
) // goal F |- X=B1 <=> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
- Proof(steps(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9), imports(i1, i2, i3))
+ SCProof(steps(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9), imports(i1, i2, i3))
},
Vector(13, -3, 14)
) // goal F |- X=B1 <=> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
- val s16 = RightForall(
+ val s16 = SC.RightForall(
(H1, G, F) |- forall(X, (X === B1) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))),
15,
(X === B1) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))),
X
) // goal F |- ∀X. X=B1 <=> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
- val s17 = RightExists(
+ val s17 = SC.RightExists(
(H1, G, F) |- exists(y, forall(X, (X === y) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))))),
16,
forall(X, (X === y) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))),
y,
B1
)
- val s18 = LeftExists((exists(B1, F), G, H1) |- s17.bot.right, 17, F, B1) // ∃B1. F |- ∃B1. ∀X. X=B1 <=> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
- val s19 = Rewrite(s18.bot.left |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))), 18) // ∃B1. F |- ∃!X. [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
- val s20 = Cut((G, H1) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))), 7, 19, exists(B1, F))
- val s21 = LeftExists((H1, exists(B, G)) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))), 20, G, B)
- val s22 = Cut(H1 |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ phi(x, a)))), 6, 21, exists(B, G))
+ val s18 = SC.LeftExists((exists(B1, F), G, H1) |- s17.bot.right, 17, F, B1) // ∃B1. F |- ∃B1. ∀X. X=B1 <=> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
+ val s19 = SC.Rewrite(s18.bot.left |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))), 18) // ∃B1. F |- ∃!X. [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
+ val s20 = SC.Cut((G, H1) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))), 7, 19, exists(B1, F))
+ val s21 = SC.LeftExists((H1, exists(B, G)) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))), 20, G, B)
+ val s22 = SC.Cut(H1 |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ phi(x, a)))), 6, 21, exists(B, G))
val res = steps(s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, s17, s18, s19, s20, s21, s22)
- Proof(res, imports(i1, i2, i3))
+ SCProof(res, imports(i1, i2, i3))
} using (ax"replacementSchema", ax"comprehensionSchema", ax"extensionalityAxiom")
show
THEOREM("lemmaLayeredTwoArgumentsMap") of
"∀ 'b. elem('b, 'B) ⇒ (∀ 'a. elem('a, 'A) ⇒ (∃! 'x. 'psi('x, 'a, 'b))) ⊢ " +
- "∃! 'X. ∀ 'x. elem('x, 'X) ↔ (∃ 'b. elem('b, 'B) ∧ (∀ 'x1. elem('x1, 'x) ↔ (∃ 'a. elem('a, 'A) ∧ 'psi('x1, 'a, 'b))))" PROOF {
+ "∃! 'X. ∀ 'x. elem('x, 'X) ↔ (∃ 'b. elem('b, 'B) ∧ (∀ 'x1. elem('x1, 'x) ↔ (∃ 'a. elem('a, 'A) ∧ 'psi('x1, 'a, 'b))))" PROOF2 {
val a = VariableLabel("a")
val b = VariableLabel("b")
val x = VariableLabel("x")
@@ -255,24 +260,24 @@ object Mapping extends lisa.Main {
val H1 = forall(a, in(a, A) ==> H)
val i1 = thm"functionalMapping"
val H2 = instantiatePredicateSchemas(H1, Map(phi -> LambdaTermFormula(Seq(x, a), psi(x, a, b))))
- val s0 = InstPredSchema((H2) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), -1, Map(phi -> LambdaTermFormula(Seq(x, a), psi(x, a, b))))
- val s1 = Weakening((H2, in(b, B)) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), 0)
+ val s0 = SC.InstPredSchema((H2) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), -1, Map(phi -> LambdaTermFormula(Seq(x, a), psi(x, a, b))))
+ val s1 = SC.Weakening((H2, in(b, B)) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), 0)
val s2 =
- LeftSubstIff((in(b, B) ==> H2, in(b, B)) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), 1, List((in(b, B), And())), LambdaFormulaFormula(Seq(h), h() ==> H2))
- val s3 = LeftForall((forall(b, in(b, B) ==> H2), in(b, B)) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), 2, in(b, B) ==> H2, b, b)
- val s4 = Rewrite(forall(b, in(b, B) ==> H2) |- in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), 3)
- val s5 = RightForall(
+ SC.LeftSubstIff((in(b, B) ==> H2, in(b, B)) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), 1, List((in(b, B), And())), LambdaFormulaFormula(Seq(h), h() ==> H2))
+ val s3 = SC.LeftForall((forall(b, in(b, B) ==> H2), in(b, B)) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), 2, in(b, B) ==> H2, b, b)
+ val s4 = SC.Rewrite(forall(b, in(b, B) ==> H2) |- in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), 3)
+ val s5 = SC.RightForall(
forall(b, in(b, B) ==> H2) |- forall(b, in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b))))),
4,
in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))),
b
)
- val s6 = InstFunSchema(
+ val s6 = SC.InstFunSchema(
forall(b, in(b, B) ==> existsOne(X, phi(X, b))) |- instantiateTermSchemas(i1.right.head, Map(A -> LambdaTermTerm(Nil, B))),
-1,
Map(A -> LambdaTermTerm(Nil, B))
)
- val s7 = InstPredSchema(
+ val s7 = SC.InstPredSchema(
forall(b, in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b))))) |- existsOne(
X,
forall(x, in(x, X) <=> exists(b, in(b, B) /\ forall(x1, in(x1, x) <=> exists(a, in(a, A) /\ psi(x1, a, b)))))
@@ -280,13 +285,13 @@ object Mapping extends lisa.Main {
6,
Map(phi -> LambdaTermFormula(Seq(y, b), forall(x, in(x, y) <=> exists(a, in(a, A) /\ psi(x, a, b)))))
)
- val s8 = Cut(
+ val s8 = SC.Cut(
forall(b, in(b, B) ==> H2) |- existsOne(X, forall(x, in(x, X) <=> exists(b, in(b, B) /\ forall(x1, in(x1, x) <=> exists(a, in(a, A) /\ psi(x1, a, b)))))),
5,
7,
forall(b, in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))))
)
- Proof(Vector(s0, s1, s2, s3, s4, s5, s6, s7, s8), Vector(i1))
+ SCProof(Vector(s0, s1, s2, s3, s4, s5, s6, s7, s8), Vector(i1))
// have ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s0
// have (b ∈ B), ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s1
// have (b ∈ B), (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s2
@@ -300,7 +305,7 @@ object Mapping extends lisa.Main {
show
THEOREM("applyFunctionToUniqueObject") of
- "∃! 'x. 'phi('x) ⊢ ∃! 'z. ∃ 'x. ('z = 'F('x)) ∧ 'phi('x)" PROOF {
+ "∃! 'x. 'phi('x) ⊢ ∃! 'z. ∃ 'x. ('z = 'F('x)) ∧ 'phi('x)" PROOF2 {
val x = VariableLabel("x")
val x1 = VariableLabel("x1")
val z = VariableLabel("z")
@@ -310,47 +315,48 @@ object Mapping extends lisa.Main {
val phi = SchematicPredicateLabel("phi", 1)
val g = VariableFormulaLabel("g")
- val g2 = SCSubproof({
+ val g2 = SC.SCSubproof({
val s0 = hypothesis(F(x1) === z)
- val s1 = LeftSubstEq((x === x1, F(x) === z) |- F(x1) === z, 0, List((x, x1)), LambdaTermFormula(Seq(f), F(f) === z))
- val s2 = LeftSubstIff(Set(phi(x) <=> (x === x1), phi(x), F(x) === z) |- F(x1) === z, 1, List((x === x1, phi(x))), LambdaFormulaFormula(Seq(g), g))
- val s3 = LeftForall(Set(forall(x, phi(x) <=> (x === x1)), phi(x), F(x) === z) |- F(x1) === z, 2, phi(x) <=> (x === x1), x, x)
- val s4 = Rewrite(Set(forall(x, phi(x) <=> (x === x1)), phi(x) /\ (F(x) === z)) |- F(x1) === z, 3)
- val s5 = LeftExists(Set(forall(x, phi(x) <=> (x === x1)), exists(x, phi(x) /\ (F(x) === z))) |- F(x1) === z, 4, phi(x) /\ (F(x) === z), x)
- val s6 = Rewrite(forall(x, phi(x) <=> (x === x1)) |- exists(x, phi(x) /\ (F(x) === z)) ==> (F(x1) === z), 5)
- Proof(steps(s0, s1, s2, s3, s4, s5, s6))
+ val s1 = SC.LeftSubstEq((x === x1, F(x) === z) |- F(x1) === z, 0, List((x, x1)), LambdaTermFormula(Seq(f), F(f) === z))
+ val s2 = SC.LeftSubstIff(Set(phi(x) <=> (x === x1), phi(x), F(x) === z) |- F(x1) === z, 1, List((x === x1, phi(x))), LambdaFormulaFormula(Seq(g), g))
+ val s3 = SC.LeftForall(Set(forall(x, phi(x) <=> (x === x1)), phi(x), F(x) === z) |- F(x1) === z, 2, phi(x) <=> (x === x1), x, x)
+ val s4 = SC.Rewrite(Set(forall(x, phi(x) <=> (x === x1)), phi(x) /\ (F(x) === z)) |- F(x1) === z, 3)
+ val s5 = SC.LeftExists(Set(forall(x, phi(x) <=> (x === x1)), exists(x, phi(x) /\ (F(x) === z))) |- F(x1) === z, 4, phi(x) /\ (F(x) === z), x)
+ val s6 = SC.Rewrite(forall(x, phi(x) <=> (x === x1)) |- exists(x, phi(x) /\ (F(x) === z)) ==> (F(x1) === z), 5)
+ SCProof(steps(s0, s1, s2, s3, s4, s5, s6))
}) // redGoal2 ∀x. x=x1 <=> phi(x) ⊢ ∃x. z=F(x) /\ phi(x) ==> F(x1)=z g2.s5
- val g1 = SCSubproof({
+ val g1 = SC.SCSubproof({
val s0 = hypothesis(phi(x1))
- val s1 = LeftForall(forall(x, (x === x1) <=> phi(x)) |- phi(x1), 0, (x === x1) <=> phi(x), x, x1)
+ val s1 = SC.LeftForall(forall(x, (x === x1) <=> phi(x)) |- phi(x1), 0, (x === x1) <=> phi(x), x, x1)
val s2 = hypothesis(z === F(x1))
- val s3 = RightAnd((forall(x, (x === x1) <=> phi(x)), z === F(x1)) |- (z === F(x1)) /\ phi(x1), Seq(2, 1), Seq(z === F(x1), phi(x1)))
- val s4 = RightExists((forall(x, (x === x1) <=> phi(x)), z === F(x1)) |- exists(x, (z === F(x)) /\ phi(x)), 3, (z === F(x)) /\ phi(x), x, x1)
- val s5 = Rewrite(forall(x, (x === x1) <=> phi(x)) |- z === F(x1) ==> exists(x, (z === F(x)) /\ phi(x)), 4)
- Proof(steps(s0, s1, s2, s3, s4, s5))
+ val s3 = SC.RightAnd((forall(x, (x === x1) <=> phi(x)), z === F(x1)) |- (z === F(x1)) /\ phi(x1), Seq(2, 1), Seq(z === F(x1), phi(x1)))
+ val s4 = SC.RightExists((forall(x, (x === x1) <=> phi(x)), z === F(x1)) |- exists(x, (z === F(x)) /\ phi(x)), 3, (z === F(x)) /\ phi(x), x, x1)
+ val s5 = SC.Rewrite(forall(x, (x === x1) <=> phi(x)) |- z === F(x1) ==> exists(x, (z === F(x)) /\ phi(x)), 4)
+ SCProof(steps(s0, s1, s2, s3, s4, s5))
})
val s0 = g1
val s1 = g2
- val s2 = RightIff(forall(x, (x === x1) <=> phi(x)) |- (z === F(x1)) <=> exists(x, (z === F(x)) /\ phi(x)), 0, 1, z === F(x1), exists(x, (z === F(x)) /\ phi(x)))
- val s3 = RightForall(forall(x, (x === x1) <=> phi(x)) |- forall(z, (z === F(x1)) <=> exists(x, (z === F(x)) /\ phi(x))), 2, (z === F(x1)) <=> exists(x, (z === F(x)) /\ phi(x)), z)
- val s4 = RightExists(
+ val s2 = SC.RightIff(forall(x, (x === x1) <=> phi(x)) |- (z === F(x1)) <=> exists(x, (z === F(x)) /\ phi(x)), 0, 1, z === F(x1), exists(x, (z === F(x)) /\ phi(x)))
+ val s3 = SC.RightForall(forall(x, (x === x1) <=> phi(x)) |- forall(z, (z === F(x1)) <=> exists(x, (z === F(x)) /\ phi(x))), 2, (z === F(x1)) <=> exists(x, (z === F(x)) /\ phi(x)), z)
+ val s4 = SC.RightExists(
forall(x, (x === x1) <=> phi(x)) |- exists(z1, forall(z, (z === z1) <=> exists(x, (z === F(x)) /\ phi(x)))),
3,
forall(z, (z === z1) <=> exists(x, (z === F(x)) /\ phi(x))),
z1,
F(x1)
)
- val s5 = LeftExists(exists(x1, forall(x, (x === x1) <=> phi(x))) |- exists(z1, forall(z, (z === z1) <=> exists(x, (z === F(x)) /\ phi(x)))), 4, forall(x, (x === x1) <=> phi(x)), x1)
- val s6 = Rewrite(existsOne(x, phi(x)) |- existsOne(z, exists(x, (z === F(x)) /\ phi(x))), 5) // goal ∃!x. phi(x) ⊢ ∃!z. ∃x. z=F(x) /\ phi(x)
- Proof(Vector(s0, s1, s2, s3, s4, s5, s6))
+ val s5 = SC.LeftExists(exists(x1, forall(x, (x === x1) <=> phi(x))) |- exists(z1, forall(z, (z === z1) <=> exists(x, (z === F(x)) /\ phi(x)))), 4, forall(x, (x === x1) <=> phi(x)), x1)
+ val s6 = SC.Rewrite(existsOne(x, phi(x)) |- existsOne(z, exists(x, (z === F(x)) /\ phi(x))), 5) // goal ∃!x. phi(x) ⊢ ∃!z. ∃x. z=F(x) /\ phi(x)
+ SCProof(Vector(s0, s1, s2, s3, s4, s5, s6))
} using ()
show
THEOREM("mapTwoArguments") of
"∀ 'b. elem('b, 'B) ⇒ (∀ 'a. elem('a, 'A) ⇒ (∃! 'x. 'psi('x, 'a, 'b))) ⊢ " +
- "∃! 'z. ∃ 'x. 'z = union('x) ∧ (∀ 'x_0. elem('x_0, 'x) ↔ (∃ 'b. elem('b, 'B) ∧ (∀ 'x1. elem('x1, 'x_0) ↔ (∃ 'a. elem('a, 'A) ∧ 'psi('x1, 'a, 'b)))))" PROOF {
+ "∃! 'z. ∃ 'x. 'z = union('x) ∧ (∀ 'x_0. elem('x_0, 'x) ↔ " +
+ "(∃ 'b. elem('b, 'B) ∧ (∀ 'x1. elem('x1, 'x_0) ↔ (∃ 'a. elem('a, 'A) ∧ 'psi('x1, 'a, 'b)))))" PROOF2 {
val a = VariableLabel("a")
val b = VariableLabel("b")
val x = VariableLabel("x")
@@ -366,11 +372,11 @@ object Mapping extends lisa.Main {
val i2 = thm"applyFunctionToUniqueObject"
val rPhi = forall(x, in(x, y) <=> exists(b, in(b, B) /\ forall(x1, in(x1, x) <=> exists(a, in(a, A) /\ psi(x1, a, b)))))
val seq0 = instantiatePredicateSchemaInSequent(i2, Map(phi -> LambdaTermFormula(Seq(y), rPhi)))
- val s0 = InstPredSchema(seq0, -2, Map(phi -> LambdaTermFormula(Seq(y), rPhi))) // val s0 = InstPredSchema(instantiatePredicateSchemaInSequent(i2, phi, rPhi, Seq(X)), -2, phi, rPhi, Seq(X))
+ val s0 = SC.InstPredSchema(seq0, -2, Map(phi -> LambdaTermFormula(Seq(y), rPhi))) // val s0 = SC.InstPredSchema(instantiatePredicateSchemaInSequent(i2, phi, rPhi, Seq(X)), -2, phi, rPhi, Seq(X))
val seq1 = instantiateFunctionSchemaInSequent(seq0, Map(F -> LambdaTermTerm(Seq(x), union(x))))
- val s1 = InstFunSchema(seq1, 0, Map(F -> LambdaTermTerm(Seq(x), union(x))))
- val s2 = Cut(i1.left |- seq1.right, -1, 1, seq1.left.head)
- Proof(steps(s0, s1, s2), imports(i1, i2))
+ val s1 = SC.InstFunSchema(seq1, 0, Map(F -> LambdaTermTerm(Seq(x), union(x))))
+ val s2 = SC.Cut(i1.left |- seq1.right, -1, 1, seq1.left.head)
+ SCProof(steps(s0, s1, s2), imports(i1, i2))
} using (thm"lemmaLayeredTwoArgumentsMap", thm"applyFunctionToUniqueObject")
show
@@ -378,55 +384,55 @@ object Mapping extends lisa.Main {
val B = VariableLabel("B")
private val z = VariableLabel("z")
val cartesianProduct: ConstantFunctionLabel =
- DEFINE("cartProd", A, B) asThe
- z suchThat {
- val a = VariableLabel("a")
- val b = VariableLabel("b")
- val x = VariableLabel("x")
- val x0 = VariableLabel("x0")
- val x1 = VariableLabel("x1")
- val A = VariableLabel("A")
- val B = VariableLabel("B")
- exists(x, (z === union(x)) /\ forall(x0, in(x0, x) <=> exists(b, in(b, B) /\ forall(x1, in(x1, x0) <=> exists(a, in(a, A) /\ (x1 === oPair(a, b)))))))
- } PROOF {
- def makeFunctional(t: Term): Proof = {
- val x = VariableLabel(freshId(t.freeVariables.map(_.id), "x"))
- val y = VariableLabel(freshId(t.freeVariables.map(_.id), "y"))
- val s0 = RightRefl(() |- t === t, t === t)
- val s1 = Rewrite(() |- (x === t) <=> (x === t), 0)
- val s2 = RightForall(() |- forall(x, (x === t) <=> (x === t)), 1, (x === t) <=> (x === t), x)
- val s3 = RightExists(() |- exists(y, forall(x, (x === y) <=> (x === t))), 2, forall(x, (x === y) <=> (x === t)), y, t)
- val s4 = Rewrite(() |- existsOne(x, x === t), 3)
- Proof(s0, s1, s2, s3, s4)
- }
+ DEFINE("cartProd", A, B) asThe z suchThat {
+ val a = VariableLabel("a")
+ val b = VariableLabel("b")
+ val x = VariableLabel("x")
+ val x0 = VariableLabel("x0")
+ val x1 = VariableLabel("x1")
+ val A = VariableLabel("A")
+ val B = VariableLabel("B")
+ exists(x, (z === union(x)) /\ forall(x0, in(x0, x) <=> exists(b, in(b, B) /\ forall(x1, in(x1, x0) <=> exists(a, in(a, A) /\ (x1 === oPair(a, b)))))))
+ } PROOF {
+ def makeFunctional(t: Term): SCProof = {
+ val x = VariableLabel(freshId(t.freeVariables.map(_.id), "x"))
+ val y = VariableLabel(freshId(t.freeVariables.map(_.id), "y"))
+ val s0 = SC.RightRefl(() |- t === t, t === t)
+ val s1 = SC.Rewrite(() |- (x === t) <=> (x === t), 0)
+ val s2 = SC.RightForall(() |- forall(x, (x === t) <=> (x === t)), 1, (x === t) <=> (x === t), x)
+ val s3 = SC.RightExists(() |- exists(y, forall(x, (x === y) <=> (x === t))), 2, forall(x, (x === y) <=> (x === t)), y, t)
+ val s4 = SC.Rewrite(() |- existsOne(x, x === t), 3)
+ SCProof(s0, s1, s2, s3, s4)
+ }
+
+ val a = VariableLabel("a")
+ val b = VariableLabel("b")
+ val x = VariableLabel("x")
+ val A = VariableLabel("A")
+ val B = VariableLabel("B")
+ val psi = SchematicPredicateLabel("psi", 3)
- val a = VariableLabel("a")
- val b = VariableLabel("b")
- val x = VariableLabel("x")
- val A = VariableLabel("A")
- val B = VariableLabel("B")
- val psi = SchematicPredicateLabel("psi", 3)
+ val i1 = thm"mapTwoArguments" // ∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!z. ∃x. (z = U(x)) ∧ ∀x_0. (x_0 ∈ x) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x_0) ↔ ∃a. (a ∈ ?A) ∧ ?psi(x1, a, b)
- val i1 = thm"mapTwoArguments" // ∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!z. ∃x. (z = U(x)) ∧ ∀x_0. (x_0 ∈ x) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x_0) ↔ ∃a. (a ∈ ?A) ∧ ?psi(x1, a, b)
+ val s0 = SC.SCSubproof({
+ val s0 = SC.SCSubproof(makeFunctional(oPair(a, b)))
+ val s1 = SC.Weakening((in(b, B), in(a, A)) |- s0.bot.right, 0)
+ val s2 = SC.Rewrite(in(b, B) |- in(a, A) ==> s0.bot.right.head, 1)
+ val s3 = SC.RightForall(in(b, B) |- forall(a, in(a, A) ==> s0.bot.right.head), 2, in(a, A) ==> s0.bot.right.head, a)
+ val s4 = SC.Rewrite(() |- in(b, B) ==> forall(a, in(a, A) ==> s0.bot.right.head), 3)
+ val s5 = SC.RightForall(() |- forall(b, in(b, B) ==> forall(a, in(a, A) ==> s0.bot.right.head)), 4, in(b, B) ==> forall(a, in(a, A) ==> s0.bot.right.head), b)
+ SCProof(steps(s0, s1, s2, s3, s4, s5))
+ }) // ∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. x= (a, b)
- val s0 = SCSubproof({
- val s0 = SCSubproof(makeFunctional(oPair(a, b)))
- val s1 = Weakening((in(b, B), in(a, A)) |- s0.bot.right, 0)
- val s2 = Rewrite(in(b, B) |- in(a, A) ==> s0.bot.right.head, 1)
- val s3 = RightForall(in(b, B) |- forall(a, in(a, A) ==> s0.bot.right.head), 2, in(a, A) ==> s0.bot.right.head, a)
- val s4 = Rewrite(() |- in(b, B) ==> forall(a, in(a, A) ==> s0.bot.right.head), 3)
- val s5 = RightForall(() |- forall(b, in(b, B) ==> forall(a, in(a, A) ==> s0.bot.right.head)), 4, in(b, B) ==> forall(a, in(a, A) ==> s0.bot.right.head), b)
- Proof(steps(s0, s1, s2, s3, s4, s5))
- }) // ∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. x= (a, b)
+ val s1 = SC.InstPredSchema(
+ instantiatePredicateSchemaInSequent(i1, Map(psi -> LambdaTermFormula(Seq(x, a, b), x === oPair(a, b)))),
+ -1,
+ Map(psi -> LambdaTermFormula(Seq(x, a, b), x === oPair(a, b)))
+ )
+ val s2 = SC.Cut(() |- s1.bot.right, 0, 1, s1.bot.left.head)
+ SCProof(steps(s0, s1, s2), imports(i1))
+ } using (thm"mapTwoArguments")
- val s1 = InstPredSchema(
- instantiatePredicateSchemaInSequent(i1, Map(psi -> LambdaTermFormula(Seq(x, a, b), x === oPair(a, b)))),
- -1,
- Map(psi -> LambdaTermFormula(Seq(x, a, b), x === oPair(a, b)))
- )
- val s2 = Cut(() |- s1.bot.right, 0, 1, s1.bot.left.head)
- Proof(steps(s0, s1, s2), imports(i1))
- } using (thm"mapTwoArguments")
show
}
diff --git a/src/main/scala/lisa/proven/mathematics/SetTheory.scala b/src/main/scala/lisa/proven/mathematics/SetTheory.scala
index c02bd0c0..1b902db3 100644
--- a/src/main/scala/lisa/proven/mathematics/SetTheory.scala
+++ b/src/main/scala/lisa/proven/mathematics/SetTheory.scala
@@ -4,58 +4,58 @@ import lisa.automation.kernel.Destructors.*
import lisa.automation.kernel.ProofTactics.*
/**
- * An embryo of mathematical development, containing a few example theorems and the definition of the ordered pair.
+ * An embryo of mathematical development, containing a few example theorems and the definition of the ordered unorderedPair.
*/
object SetTheory extends lisa.Main {
THEOREM("russelParadox") of "∀'x. elem('x, 'y) ↔ ¬elem('x, 'x) ⊢" PROOF {
val y = VariableLabel("y")
val x = VariableLabel("x")
- val s0 = RewriteTrue(in(y, y) <=> !in(y, y) |- ())
- val s1 = LeftForall(forall(x, in(x, y) <=> !in(x, x)) |- (), 0, in(x, y) <=> !in(x, x), x, y)
- Proof(s0, s1)
- } using ()
- thm"russelParadox".show
+
+ have(in(y, y) <=> !in(y, y) |- ()) by Restate
+ andThen(forall(x, in(x, y) <=> !in(x, x)) |- ()) by LeftForall(in(x, y) <=> !in(x, x), x, y)
+ }
+ show
THEOREM("unorderedPair_symmetry") of
- "⊢ ∀'y. ∀'x. unordered_pair('x, 'y) = unordered_pair('y, 'x)" PROOF {
+ "⊢ ∀'y. ∀'x. unordered_pair('x, 'y) = unordered_pair('y, 'x)" PROOF2 {
val x = VariableLabel("x")
val y = VariableLabel("y")
val z = VariableLabel("z")
val h = VariableFormulaLabel("h")
- val fin = SCSubproof(
+ val fin = SC.SCSubproof(
{
- val pr0 = SCSubproof(
+ val pr0 = SC.SCSubproof(
{
- val pairSame11 = instantiateForall(new Proof(steps(), imports(ax"pairAxiom")), pairAxiom, x)
+ val pairSame11 = instantiateForall(new SCProof(steps(), imports(ax"pairAxiom")), pairAxiom, x)
val pairSame12 = instantiateForall(pairSame11, pairSame11.conclusion.right.head, y)
instantiateForall(pairSame12, pairSame12.conclusion.right.head, z)
},
Seq(-1)
)
- val pr1 = SCSubproof(
+ val pr1 = SC.SCSubproof(
{
- val pairSame21 = instantiateForall(new Proof(steps(), imports(ax"pairAxiom")), pairAxiom, y)
+ val pairSame21 = instantiateForall(new SCProof(steps(), imports(ax"pairAxiom")), pairAxiom, y)
val pairSame22 = instantiateForall(pairSame21, pairSame21.conclusion.right.head, x)
instantiateForall(pairSame22, pairSame22.conclusion.right.head, z)
},
Seq(-1)
)
- val pr2 = RightSubstIff(
+ val pr2 = SC.RightSubstIff(
Sequent(pr1.bot.right, Set(in(z, unorderedPair(x, y)) <=> in(z, unorderedPair(y, x)))),
0,
List(((x === z) \/ (y === z), in(z, unorderedPair(y, x)))),
LambdaFormulaFormula(Seq(h), in(z, unorderedPair(x, y)) <=> h)
)
- val pr3 = Cut(Sequent(pr1.bot.left, pr2.bot.right), 1, 2, pr2.bot.left.head)
- val pr4 = RightForall(Sequent(Set(), Set(forall(z, pr2.bot.right.head))), 3, pr2.bot.right.head, z)
- Proof(steps(pr0, pr1, pr2, pr3, pr4), imports(ax"pairAxiom"))
+ val pr3 = SC.Cut(Sequent(pr1.bot.left, pr2.bot.right), 1, 2, pr2.bot.left.head)
+ val pr4 = SC.RightForall(Sequent(Set(), Set(forall(z, pr2.bot.right.head))), 3, pr2.bot.right.head, z)
+ SCProof(steps(pr0, pr1, pr2, pr3, pr4), imports(ax"pairAxiom"))
},
Seq(-2)
)
- val pairExt = SCSubproof(
+ val pairExt = SC.SCSubproof(
{
- val pairExt1 = instantiateForall(Proof(steps(), imports(ax"extensionalityAxiom")), ax"extensionalityAxiom", unorderedPair(x, y))
+ val pairExt1 = instantiateForall(SCProof(steps(), imports(ax"extensionalityAxiom")), ax"extensionalityAxiom", unorderedPair(x, y))
instantiateForall(pairExt1, pairExt1.conclusion.right.head, unorderedPair(y, x))
},
Seq(-1)
@@ -72,7 +72,7 @@ object SetTheory extends lisa.Main {
// This proof is old and very unoptimised
THEOREM("unorderedPair_deconstruction") of
- "⊢ ∀'x. ∀'y. ∀ 'x1. ∀ 'y1. unordered_pair('x, 'y) = unordered_pair('x1, 'y1) ⇒ 'y1 = 'y ∧ 'x1 = 'x ∨ 'x = 'y1 ∧ 'y = 'x1" PROOF {
+ "⊢ ∀'x. ∀'y. ∀ 'x1. ∀ 'y1. unordered_pair('x, 'y) = unordered_pair('x1, 'y1) ⇒ 'y1 = 'y ∧ 'x1 = 'x ∨ 'x = 'y1 ∧ 'y = 'x1" PROOF2 {
val x = VariableLabel("x")
val y = VariableLabel("y")
val x1 = VariableLabel("x'")
@@ -82,147 +82,147 @@ object SetTheory extends lisa.Main {
val h = VariableFormulaLabel("h")
val pxy = unorderedPair(x, y)
val pxy1 = unorderedPair(x1, y1)
- val p0 = SCSubproof(
+ val p0 = SC.SCSubproof(
{
- val p0 = SCSubproof(
+ val p0 = SC.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, List((pxy, pxy1)), LambdaTermFormula(Seq(g), zf <=> in(z, g)))
- Proof(IndexedSeq(p1_0, p1_1, p1_2, p1_3), IndexedSeq(() |- pairAxiom))
+ val p1_1 = SC.RightImplies(emptySeq +> (zf ==> zf), 0, zf, zf)
+ val p1_2 = SC.RightIff(emptySeq +> (zf <=> zf), 1, 1, zf, zf) // |- (z in {x,y} <=> z in {x,y})
+ val p1_3 = SC.RightSubstEq(emptySeq +< (pxy === pxy1) +> (zf <=> in(z, pxy1)), 2, List((pxy, pxy1)), LambdaTermFormula(Seq(g), zf <=> in(z, g)))
+ SCProof(IndexedSeq(p1_0, p1_1, p1_2, p1_3), IndexedSeq(() |- pairAxiom))
},
Seq(-1),
display = true
) // ({x,y}={x',y'}) |- ((z∈{x,y})↔(z∈{x',y'}))
- val p1 = SCSubproof(
+ val p1 = SC.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(Proof(IndexedSeq(p1_0), IndexedSeq(() |- pairAxiom)), x, y, z)
+ val p1_0 = SC.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
},
Seq(-1),
display = true
) // |- (z in {x,y}) <=> (z=x \/ z=y)
- val p2 = SCSubproof(
+ val p2 = SC.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(Proof(IndexedSeq(p2_0), IndexedSeq(() |- pairAxiom)), x1, y1, z)
+ val p2_0 = SC.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
},
Seq(-1)
) // |- (z in {x',y'}) <=> (z=x' \/ z=y')
- val p3 = RightSubstEq(
+ val p3 = SC.RightSubstEq(
emptySeq +< (pxy === pxy1) +> (in(z, pxy1) <=> ((z === x) \/ (z === y))),
1,
List((pxy, pxy1)),
LambdaTermFormula(Seq(g), in(z, g) <=> ((z === x) \/ (z === y)))
) // ({x,y}={x',y'}) |- ((z∈{x',y'})↔((z=x)∨(z=y)))
- val p4 = RightSubstIff(
+ val p4 = SC.RightSubstIff(
emptySeq +< p3.bot.left.head +< p2.bot.right.head +> (((z === x) \/ (z === y)) <=> ((z === x1) \/ (z === y1))),
3,
List(((z === x1) \/ (z === y1), in(z, pxy1))),
LambdaFormulaFormula(Seq(h), h <=> ((z === x) \/ (z === y)))
) // ((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)
- Proof(IndexedSeq(p0, p1, p2, p3, p4, p5), IndexedSeq(() |- pairAxiom))
+ val p5 = SC.Cut(emptySeq ++< p3.bot ++> p4.bot, 2, 4, p2.bot.right.head)
+ SCProof(IndexedSeq(p0, p1, p2, p3, p4, p5), IndexedSeq(() |- pairAxiom))
},
Seq(-1)
) // ({x,y}={x',y'}) |- (((z=x)∨(z=y))↔((z=x')∨(z=y')))
- val p1 = SCSubproof(
- Proof(
+ val p1 = SC.SCSubproof(
+ SCProof(
byCase(x === x1)(
- SCSubproof(
+ SC.SCSubproof(
{
val pcm1 = p0
- val pc0 = SCSubproof(
- Proof(
+ val pc0 = SC.SCSubproof(
+ SCProof(
byCase(y === x)(
- SCSubproof(
+ SC.SCSubproof(
{
val pam1 = pcm1
- val pa0 = SCSubproof(
+ val pa0 = SC.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 = SC.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 = Proof(pa0_0_0, pa0_1_1, pa0_1_2, pa0_1_3, pa0_1_4, pa0_1_5)
+ val pa0_1_1 = SC.RightOr(emptySeq +< f1 +> (f1 \/ f1), 0, f1, f1)
+ val pa0_1_2 = SC.RightImplies(emptySeq +> (f1 ==> (f1 \/ f1)), 1, f1, f1 \/ f1)
+ val pa0_1_3 = SC.LeftOr(emptySeq +< (f1 \/ f1) +> f1, Seq(0, 0), Seq(f1, f1))
+ val pa0_1_4 = SC.RightImplies(emptySeq +> ((f1 \/ f1) ==> f1), 3, f1 \/ f1, f1)
+ val pa0_1_5 = SC.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(
+ val pa0_1 = SC.RightSubstEq(
emptySeq +< (pxy === pxy1) +< (x === y) +> ((f1 \/ f1) <=> (z === x1) \/ (z === y1)),
-1,
List((x, y)),
LambdaTermFormula(Seq(g), (f1 \/ (z === g)) <=> ((z === x1) \/ (z === y1)))
) // ({x,y}={x',y'}) y=x|- (z=x)\/(z=x) <=> (z=x' \/ z=y')
- val pa0_2 = RightSubstIff(
+ val pa0_2 = SC.RightSubstIff(
emptySeq +< (pxy === pxy1) +< (x === y) +< (f1 <=> (f1 \/ f1)) +> (f1 <=> ((z === x1) \/ (z === y1))),
1,
List((f1, f1 \/ f1)),
LambdaFormulaFormula(Seq(h), h <=> ((z === x1) \/ (z === y1)))
)
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(Proof(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')))
+ SC.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 = SC.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 = SC.SCSubproof(
{
- val pa1_0 = RightRefl(emptySeq +> (y1 === y1), y1 === y1)
- val pa1_1 = RightOr(emptySeq +> ((y1 === y1) \/ (y1 === x1)), 0, y1 === y1, y1 === x1)
- Proof(pa1_0, pa1_1)
+ val pa1_0 = SC.RightRefl(emptySeq +> (y1 === y1), y1 === y1)
+ val pa1_1 = SC.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, List((x, y)), LambdaTermFormula(Seq(g), y1 === g))
- Proof(ra3.steps, IndexedSeq(pam1.bot)).appended(pal) // (x=y), ({x,y}={x',y'}) |- (y'=y)
+ val pal = SC.RightSubstEq(emptySeq ++< pa0.bot +> (y1 === y), ra3.length - 1, List((x, y)), LambdaTermFormula(Seq(g), y1 === 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(
+ SC.SCSubproof(
{
val pbm1 = pcm1 // ({x,y}={x',y'}) |- (((z=x)∨(z=y))↔((z=x')∨(z=y')))
- val pb0_0 = SCSubproof(
+ val pb0_0 = SC.SCSubproof(
{
- val pb0_0 = RightForall(emptySeq ++< pcm1.bot +> forall(z, pcm1.bot.right.head), -1, pcm1.bot.right.head, z)
- instantiateForall(Proof(IndexedSeq(pb0_0), IndexedSeq(pcm1.bot)), y)
+ val pb0_0 = SC.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 pb0_1 = SC.SCSubproof(
{
- val pa1_0 = RightRefl(emptySeq +> (y === y), y === y)
- val pa1_1 = RightOr(emptySeq +> ((y === y) \/ (y === x)), 0, y === y, y === x)
- Proof(pa1_0, pa1_1)
+ val pa1_0 = SC.RightRefl(emptySeq +> (y === y), y === y)
+ val pa1_1 = SC.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, List((x, x1)), LambdaTermFormula(Seq(g), (y === g) \/ (y === y1)))
+ SC.RightSubstEq(emptySeq ++< rb0.conclusion +< (x === x1) +> ((y === x) \/ (y === y1)), rb0.length - 1, List((x, x1)), LambdaTermFormula(Seq(g), (y === g) \/ (y === y1)))
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')
- Proof(rb2.steps, IndexedSeq(pbm1.bot))
+ val rb2 = rb1.appended(SC.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)
@@ -232,87 +232,87 @@ object SetTheory extends lisa.Main {
),
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 pc1 = SC.RightRefl(emptySeq +> (x === x), x === x)
+ val pc2 = SC.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, List((x, x1)), LambdaTermFormula(Seq(g), (y1 === y) /\ (g === x))) // ({x,y}={x',y'}), x=x' |- (x=x' /\ y=y')
- val pc4 = RightOr(
+ SC.RightSubstEq(emptySeq ++< pc2.bot +> ((y1 === y) /\ (x1 === x)), 2, List((x, x1)), LambdaTermFormula(Seq(g), (y1 === y) /\ (g === x))) // ({x,y}={x',y'}), x=x' |- (x=x' /\ y=y')
+ val pc4 = SC.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 = Proof(IndexedSeq(pc0, pc1, pc2, pc3, pc4), IndexedSeq(pcm1.bot))
+ 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(
+ SC.SCSubproof(
{
val pdm1 = p0
- val pd0 = SCSubproof(
+ val pd0 = SC.SCSubproof(
{
val pd0_m1 = pdm1
- val pd0_0 = SCSubproof {
+ val pd0_0 = SC.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')
- Proof(IndexedSeq(pd0_0_0, pd0_0_1))
+ val pd0_0_0 = SC.RightRefl(emptySeq +> ex1x1, ex1x1) // |- x'=x'
+ val pd0_0_1 = SC.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 = SC.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(Proof(IndexedSeq(pd0_1_0), IndexedSeq(pd0_m1.bot)), x1) // ({x,y}={x',y'}) |- (x'=x \/ x'=y) <=> (x'=x' \/ x'=y')
+ val pd0_1_0 = SC.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 pd0_2 = RightSubstIff(
+ val pd0_2 = SC.RightSubstIff(
pd0_1.bot.right |- ((x1 === x) \/ (x1 === y)),
0,
List(((x1 === x) \/ (x1 === y), (x1 === x1) \/ (x1 === y1))),
LambdaFormulaFormula(Seq(h), h)
) // (x'=x \/ x'=y) <=> (x'=x' \/ x'=y') |- (x'=x \/ x'=y)
- val pd0_3 = Cut(pd0_1.bot.left |- pd0_2.bot.right, 1, 2, pd0_1.bot.right.head) // ({x,y}={x',y'}) |- (x=x' \/ y=x')
- destructRightOr(Proof(IndexedSeq(pd0_0, pd0_1, pd0_2, pd0_3), IndexedSeq(pd0_m1.bot)), x === x1, y === x1) // ({x,y}={x',y'}) |- x=x', y=x'
+ val pd0_3 = SC.Cut(pd0_1.bot.left |- pd0_2.bot.right, 1, 2, pd0_1.bot.right.head) // ({x,y}={x',y'}) |- (x=x' \/ y=x')
+ destructRightOr(SCProof(IndexedSeq(pd0_0, pd0_1, pd0_2, 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 = SC.SCSubproof(
{
val pd1_m1 = pdm1
- val pd1_0 = SCSubproof {
+ val pd1_0 = SC.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)
- Proof(IndexedSeq(pd1_0_0, pd1_0_1))
+ val pd1_0_0 = SC.RightRefl(emptySeq +> exx, exx) // |- x=x
+ val pd1_0_1 = SC.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 = SC.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(Proof(IndexedSeq(pd1_1_0), IndexedSeq(pd1_m1.bot)), x) // ({x,y}={x',y'}) |- (x=x \/ x=y) <=> (x=x' \/ x=y')
+ val pd1_1_0 = SC.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(Proof(rd1_2.steps, IndexedSeq(pd1_m1.bot)), IndexedSeq(-1)) // // ({x,y}={x',y'}) |- x=x' \/ x=y'
- destructRightOr(Proof(IndexedSeq(pd1_0, pd1_1, pd1_3), IndexedSeq(pd1_m1.bot)), x === x1, x === y1) // ({x,y}={x',y'}) |- x=x', x=y'
+ val pd1_3 = SC.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(
+ val pd2 = SC.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 = SC.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 = SC.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')
- Proof(IndexedSeq(pd0, pd1, pd2, pd3, pd4), IndexedSeq(pdm1.bot))
+ 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')
@@ -322,12 +322,12 @@ object SetTheory extends lisa.Main {
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(Proof(IndexedSeq(p0, p1, p2), IndexedSeq(() |- pairAxiom)), x, y, x1, y1)
+ val p2 = SC.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(IndexedSeq(p0, p1, p2), IndexedSeq(() |- pairAxiom)), x, y, x1, y1)
} using ax"pairAxiom"
thm"unorderedPair_deconstruction".show
- THEOREM("noUniversalSet") of "∀'x. elem('x, 'z) ⊢ " PROOF {
+ THEOREM("noUniversalSet") of "∀'x. elem('x, 'z) ⊢ " PROOF2 {
val x = VariableLabel("x")
val y = VariableLabel("y")
val z = VariableLabel("z")
@@ -336,30 +336,30 @@ object SetTheory extends lisa.Main {
// forall(z, exists(y, forall(x, in(x,y) <=> (in(x,y) /\ sPhi(x,z)))))
val i1 = () |- comprehensionSchema
val i2 = thm"russelParadox" // forall(x1, in(x1,y) <=> !in(x1, x1)) |- ()
- val p0 = InstPredSchema(() |- forall(z, exists(y, forall(x, in(x, y) <=> (in(x, z) /\ !in(x, x))))), -1, Map(sPhi -> LambdaTermFormula(Seq(x, z), !in(x, x))))
- val s0 = SCSubproof(instantiateForall(Proof(IndexedSeq(p0), IndexedSeq(i1)), z), Seq(-1)) // exists(y1, forall(x1, in(x1,y1) <=> (in(x1,z1) /\ !in(x1, x1))))
+ val p0 = SC.InstPredSchema(() |- forall(z, exists(y, forall(x, in(x, y) <=> (in(x, z) /\ !in(x, x))))), -1, Map(sPhi -> LambdaTermFormula(Seq(x, z), !in(x, x))))
+ val s0 = SC.SCSubproof(instantiateForall(SCProof(IndexedSeq(p0), IndexedSeq(i1)), z), Seq(-1)) // exists(y1, forall(x1, in(x1,y1) <=> (in(x1,z1) /\ !in(x1, x1))))
val s1 = hypothesis(in(x, y) <=> (in(x, z) /\ !in(x, x))) // in(x,y) <=> (in(x,z) /\ in(x, x)) |- in(x,y) <=> (in(x,z) /\ in(x, x))
- val s2 = RightSubstIff(
+ val s2 = SC.RightSubstIff(
(in(x, z) <=> True, in(x, y) <=> (in(x, z) /\ !in(x, x))) |- in(x, y) <=> (True /\ !in(x, x)),
1,
List((in(x, z), And())),
LambdaFormulaFormula(Seq(h), in(x, y) <=> (h /\ !in(x, x)))
) // in(x1,y1) <=> (in(x1,z1) /\ in(x1, x1)) |- in(x,y) <=> (True /\ in(x1, x1))
- val s3 = Rewrite((in(x, z), in(x, y) <=> (in(x, z) /\ !in(x, x))) |- in(x, y) <=> !in(x, x), 2)
- val s4 = LeftForall((forall(x, in(x, z)), in(x, y) <=> (in(x, z) /\ !in(x, x))) |- in(x, y) <=> !in(x, x), 3, in(x, z), x, x)
- val s5 = LeftForall((forall(x, in(x, z)), forall(x, in(x, y) <=> (in(x, z) /\ !in(x, x)))) |- in(x, y) <=> !in(x, x), 4, in(x, y) <=> (in(x, z) /\ !in(x, x)), x, x)
- val s6 = RightForall((forall(x, in(x, z)), forall(x, in(x, y) <=> (in(x, z) /\ !in(x, x)))) |- forall(x, in(x, y) <=> !in(x, x)), 5, in(x, y) <=> !in(x, x), x)
- val s7 = InstFunSchema(forall(x, in(x, y) <=> !in(x, x)) |- (), -2, Map(y -> LambdaTermTerm(Nil, y)))
- val s8 = Cut((forall(x, in(x, z)), forall(x, in(x, y) <=> (in(x, z) /\ !in(x, x)))) |- (), 6, 7, forall(x, in(x, y) <=> !in(x, x)))
- val s9 = LeftExists((forall(x, in(x, z)), exists(y, forall(x, in(x, y) <=> (in(x, z) /\ !in(x, x))))) |- (), 8, forall(x, in(x, y) <=> (in(x, z) /\ !in(x, x))), y)
- val s10 = Cut(forall(x, in(x, z)) |- (), 0, 9, exists(y, forall(x, in(x, y) <=> (in(x, z) /\ !in(x, x)))))
- Proof(steps(s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10), imports(i1, i2))
+ val s3 = SC.Rewrite((in(x, z), in(x, y) <=> (in(x, z) /\ !in(x, x))) |- in(x, y) <=> !in(x, x), 2)
+ val s4 = SC.LeftForall((forall(x, in(x, z)), in(x, y) <=> (in(x, z) /\ !in(x, x))) |- in(x, y) <=> !in(x, x), 3, in(x, z), x, x)
+ val s5 = SC.LeftForall((forall(x, in(x, z)), forall(x, in(x, y) <=> (in(x, z) /\ !in(x, x)))) |- in(x, y) <=> !in(x, x), 4, in(x, y) <=> (in(x, z) /\ !in(x, x)), x, x)
+ val s6 = SC.RightForall((forall(x, in(x, z)), forall(x, in(x, y) <=> (in(x, z) /\ !in(x, x)))) |- forall(x, in(x, y) <=> !in(x, x)), 5, in(x, y) <=> !in(x, x), x)
+ val s7 = SC.InstFunSchema(forall(x, in(x, y) <=> !in(x, x)) |- (), -2, Map(y -> LambdaTermTerm(Nil, y)))
+ val s8 = SC.Cut((forall(x, in(x, z)), forall(x, in(x, y) <=> (in(x, z) /\ !in(x, x)))) |- (), 6, 7, forall(x, in(x, y) <=> !in(x, x)))
+ val s9 = SC.LeftExists((forall(x, in(x, z)), exists(y, forall(x, in(x, y) <=> (in(x, z) /\ !in(x, x))))) |- (), 8, forall(x, in(x, y) <=> (in(x, z) /\ !in(x, x))), y)
+ val s10 = SC.Cut(forall(x, in(x, z)) |- (), 0, 9, exists(y, forall(x, in(x, y) <=> (in(x, z) /\ !in(x, x)))))
+ SCProof(steps(s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10), imports(i1, i2))
} using (ax"comprehensionSchema", thm"russelParadox")
show
private val x = VariableLabel("x")
private val y = VariableLabel("y")
- val oPair: ConstantFunctionLabel = DEFINE("pair", x, y) as unorderedPair(unorderedPair(x, y), unorderedPair(x, x))
+ val oPair: ConstantFunctionLabel = DEFINE("", x, y) as unorderedPair(unorderedPair(x, y), unorderedPair(x, x))
show
}
diff --git a/src/main/scala/lisa/proven/peano_example/Peano.scala b/src/main/scala/lisa/proven/peano_example/Peano.scala
index 47642c62..6cbc144d 100644
--- a/src/main/scala/lisa/proven/peano_example/Peano.scala
+++ b/src/main/scala/lisa/proven/peano_example/Peano.scala
@@ -27,13 +27,13 @@ object Peano {
instantiateForall(SCProof(IndexedSeq(), IndexedSeq(proofImport)))
val tempVar = VariableLabel(freshId(formula.freeVariables.map(_.id), "x"))
val instantiated = instantiateBinder(forall, t)
- val p1 = Hypothesis(instantiated |- instantiated, instantiated)
- val p2 = LeftForall(formula |- instantiated, 0, instantiateBinder(forall, tempVar), tempVar, t)
- val p3 = Cut(() |- instantiated, -1, 1, formula)
- Proof(IndexedSeq(p1, p2, p3), IndexedSeq(proofImport))
+ val p1 = SC.Hypothesis(instantiated |- instantiated, instantiated)
+ val p2 = SC.LeftForall(formula |- instantiated, 0, instantiateBinder(forall, tempVar), tempVar, t)
+ val p3 = SC.Cut(() |- instantiated, -1, 1, formula)
+ SCProof(IndexedSeq(p1, p2, p3), IndexedSeq(proofImport))
}
- def applyInduction(baseProof: SCSubproof, inductionStepProof: SCSubproof, inductionInstance: SCProofStep): IndexedSeq[SCProofStep] = {
+ def applyInduction(baseProof: SC.SCSubproof, inductionStepProof: SC.SCSubproof, inductionInstance: SCProofStep): IndexedSeq[SCProofStep] = {
require(baseProof.bot.right.size == 1, s"baseProof should prove exactly one formula, got ${Printer.prettySequent(baseProof.bot)}")
require(inductionStepProof.bot.right.size == 1, s"inductionStepProof should prove exactly one formula, got ${Printer.prettySequent(inductionStepProof.bot)}")
require(
@@ -56,21 +56,21 @@ object Peano {
val base0 = baseProof
val step1 = inductionStepProof
val instance2 = inductionInstance
- val inductionPremise3 = RightAnd(lhs |- baseFormula /\ stepFormula, Seq(0, 1), Seq(baseFormula, stepFormula))
+ val inductionPremise3 = SC.RightAnd(lhs |- baseFormula /\ stepFormula, Seq(0, 1), Seq(baseFormula, stepFormula))
val hypConclusion4 = hypothesis(conclusion)
- val inductionInstanceOnTheLeft5 = LeftImplies(lhs + (premise ==> conclusion) |- conclusion, 3, 4, premise, conclusion)
- val cutInductionInstance6 = Cut(lhs |- conclusion, 2, 5, premise ==> conclusion)
+ val inductionInstanceOnTheLeft5 = SC.LeftImplies(lhs + (premise ==> conclusion) |- conclusion, 3, 4, premise, conclusion)
+ val cutInductionInstance6 = SC.Cut(lhs |- conclusion, 2, 5, premise ==> conclusion)
IndexedSeq(base0, step1, instance2, inductionPremise3, hypConclusion4, inductionInstanceOnTheLeft5, cutInductionInstance6)
}
val (y1, z1) =
(VariableLabel("y1"), VariableLabel("z1"))
- THEOREM("x + 0 = 0 + x") of "∀'x. +('x, 0) = +(0, 'x)" PROOF {
- val refl0: SCProofStep = RightRefl(() |- s(x) === s(x), s(x) === s(x))
- val subst1 = RightSubstEq((x === plus(zero, x)) |- s(x) === s(plus(zero, x)), 0, (x, plus(zero, x)) :: Nil, LambdaTermFormula(Seq(y), s(x) === s(y)))
- val implies2 = RightImplies(() |- (x === plus(zero, x)) ==> (s(x) === s(plus(zero, x))), 1, x === plus(zero, x), s(x) === s(plus(zero, x)))
- val transform3 = RightSubstEq(
+ THEOREM("x + 0 = 0 + x") of "∀'x. +('x, 0) = +(0, 'x)" PROOF2 {
+ val refl0: SCProofStep = SC.RightRefl(() |- s(x) === s(x), s(x) === s(x))
+ val subst1 = SC.RightSubstEq((x === plus(zero, x)) |- s(x) === s(plus(zero, x)), 0, (x, plus(zero, x)) :: Nil, LambdaTermFormula(Seq(y), s(x) === s(y)))
+ val implies2 = SC.RightImplies(() |- (x === plus(zero, x)) ==> (s(x) === s(plus(zero, x))), 1, x === plus(zero, x), s(x) === s(plus(zero, x)))
+ val transform3 = SC.RightSubstEq(
(plus(zero, s(x)) === s(plus(zero, x))) |- (x === plus(zero, x)) ==> (s(x) === plus(zero, s(x))),
2,
(plus(zero, s(x)), s(plus(zero, x))) :: Nil,
@@ -78,50 +78,50 @@ object Peano {
)
// result: ax4plusSuccessor |- 0+Sx = S(0 + x)
- val instanceAx4_4 = SCSubproof(
+ val instanceAx4_4 = SC.SCSubproof(
instantiateForall(instantiateForallImport(ax"ax4plusSuccessor", zero), x),
Seq(-1)
)
- val cut5 = Cut(() |- (x === plus(zero, x)) ==> (s(x) === plus(zero, s(x))), 4, 3, plus(zero, s(x)) === s(plus(zero, x)))
+ val cut5 = SC.Cut(() |- (x === plus(zero, x)) ==> (s(x) === plus(zero, s(x))), 4, 3, plus(zero, s(x)) === s(plus(zero, x)))
- val transform6 = RightSubstEq(
+ val transform6 = SC.RightSubstEq(
Set(plus(x, zero) === x, plus(s(x), zero) === s(x)) |- (plus(x, zero) === plus(zero, x)) ==> (plus(s(x), zero) === plus(zero, s(x))),
5,
(plus(x, zero), x) :: (plus(s(x), zero), s(x)) :: Nil,
LambdaTermFormula(Seq(y, z), (y === plus(zero, x)) ==> (z === plus(zero, s(x))))
)
- val leftAnd7 = LeftAnd(
+ val leftAnd7 = SC.LeftAnd(
(plus(x, zero) === x) /\ (plus(s(x), zero) === s(x)) |- (plus(x, zero) === plus(zero, x)) ==> (plus(s(x), zero) === plus(zero, s(x))),
6,
plus(x, zero) === x,
plus(s(x), zero) === s(x)
)
- val instancePlusZero8 = SCSubproof(
+ val instancePlusZero8 = SC.SCSubproof(
instantiateForallImport(ax"ax3neutral", x),
Seq(-2)
)
- val instancePlusZero9 = SCSubproof(
+ val instancePlusZero9 = SC.SCSubproof(
instantiateForallImport(ax"ax3neutral", s(x)),
Seq(-2)
)
- val rightAnd10 = RightAnd(() |- (plus(x, zero) === x) /\ (plus(s(x), zero) === s(x)), Seq(8, 9), Seq(plus(x, zero) === x, plus(s(x), zero) === s(x)))
+ val rightAnd10 = SC.RightAnd(() |- (plus(x, zero) === x) /\ (plus(s(x), zero) === s(x)), Seq(8, 9), Seq(plus(x, zero) === x, plus(s(x), zero) === s(x)))
- val cut11 = Cut(
+ val cut11 = SC.Cut(
() |- (plus(x, zero) === plus(zero, x)) ==> (plus(s(x), zero) === plus(zero, s(x))),
10,
7,
(plus(x, zero) === x) /\ (plus(s(x), zero) === s(x))
)
- val forall12 = RightForall(
+ val forall12 = SC.RightForall(
cut11.bot.left |- forall(x, (plus(x, zero) === plus(zero, x)) ==> (plus(s(x), zero) === plus(zero, s(x)))),
11,
(plus(x, zero) === plus(zero, x)) ==> (plus(s(x), zero) === plus(zero, s(x))),
x
)
- val inductionInstance: SCProofStep = InstPredSchema(
+ val inductionInstance: SCProofStep = SC.InstPredSchema(
() |- ((plus(zero, zero) === plus(zero, zero)) /\ forall(x, (plus(x, zero) === plus(zero, x)) ==> (plus(s(x), zero) === plus(zero, s(x))))) ==> forall(
x,
plus(x, zero) === plus(zero, x)
@@ -132,8 +132,8 @@ object Peano {
SCProof(
applyInduction(
- SCSubproof(SCProof(RightRefl(() |- zero === zero, zero === zero))),
- SCSubproof(
+ SC.SCSubproof(SCProof(SC.RightRefl(() |- zero === zero, zero === zero))),
+ SC.SCSubproof(
SCProof(
IndexedSeq(refl0, subst1, implies2, transform3, instanceAx4_4, cut5, transform6, leftAnd7, instancePlusZero8, instancePlusZero9, rightAnd10, cut11, forall12),
IndexedSeq(ax"ax4plusSuccessor", ax"ax3neutral")
@@ -147,35 +147,35 @@ object Peano {
} using (ax"ax4plusSuccessor", ax"ax3neutral", ax"ax7induction")
show
- THEOREM("switch successor") of "∀'x. ∀'y. +('x, S('y)) = +(S('x), 'y)" PROOF {
+ THEOREM("switch successor") of "∀'x. ∀'y. +('x, S('y)) = +(S('x), 'y)" PROOF2 {
//////////////////////////////////// Base: x + S0 = Sx + 0 ///////////////////////////////////////////////
val base0 = {
// x + 0 = x
- val xEqXPlusZero0 = SCSubproof(instantiateForallImport(ax"ax3neutral", x), IndexedSeq(-1))
+ val xEqXPlusZero0 = SC.SCSubproof(instantiateForallImport(ax"ax3neutral", x), IndexedSeq(-1))
// Sx + 0 = Sx
- val succXEqSuccXPlusZero1 = SCSubproof(instantiateForallImport(ax"ax3neutral", s(x)), IndexedSeq(-1))
+ val succXEqSuccXPlusZero1 = SC.SCSubproof(instantiateForallImport(ax"ax3neutral", s(x)), IndexedSeq(-1))
// x + S0 = S(x + 0)
- val xPlusSuccZero2 = SCSubproof(instantiateForall(instantiateForallImport(ax"ax4plusSuccessor", x), zero), IndexedSeq(-2))
+ val xPlusSuccZero2 = SC.SCSubproof(instantiateForall(instantiateForallImport(ax"ax4plusSuccessor", x), zero), IndexedSeq(-2))
// ------------------- x + 0 = x, Sx + 0 = Sx, x + S0 = S(x + 0) |- Sx + 0 = x + S0 ---------------------
- val succX3 = RightRefl(() |- s(x) === s(x), s(x) === s(x))
- val substEq4 = RightSubstEq(
+ val succX3 = SC.RightRefl(() |- s(x) === s(x), s(x) === s(x))
+ val substEq4 = SC.RightSubstEq(
Set(s(x) === plus(s(x), zero), x === plus(x, zero)) |- plus(s(x), zero) === s(plus(x, zero)),
3,
(s(x), plus(s(x), zero)) :: (VariableTerm(x), plus(x, zero)) :: Nil,
LambdaTermFormula(Seq(y, z), y === s(z))
)
- val substEq5 = RightSubstEq(
+ val substEq5 = SC.RightSubstEq(
Set(s(x) === plus(s(x), zero), x === plus(x, zero), s(plus(x, zero)) === plus(x, s(zero))) |- plus(s(x), zero) === plus(x, s(zero)),
4,
(s(plus(x, zero)), plus(x, s(zero))) :: Nil,
LambdaTermFormula(Seq(z), plus(s(x), zero) === z)
)
// -------------------------------------------------------------------------------------------------------
- val cut6 = Cut(Set(s(x) === plus(s(x), zero), x === plus(x, zero)) |- plus(s(x), zero) === plus(x, s(zero)), 2, 5, s(plus(x, zero)) === plus(x, s(zero)))
- val cut7 = Cut(x === plus(x, zero) |- plus(s(x), zero) === plus(x, s(zero)), 1, 6, s(x) === plus(s(x), zero))
- val cut8 = Cut(() |- plus(s(x), zero) === plus(x, s(zero)), 0, 7, x === plus(x, zero))
- SCSubproof(
+ val cut6 = SC.Cut(Set(s(x) === plus(s(x), zero), x === plus(x, zero)) |- plus(s(x), zero) === plus(x, s(zero)), 2, 5, s(plus(x, zero)) === plus(x, s(zero)))
+ val cut7 = SC.Cut(x === plus(x, zero) |- plus(s(x), zero) === plus(x, s(zero)), 1, 6, s(x) === plus(s(x), zero))
+ val cut8 = SC.Cut(() |- plus(s(x), zero) === plus(x, s(zero)), 0, 7, x === plus(x, zero))
+ SC.SCSubproof(
SCProof(
IndexedSeq(xEqXPlusZero0, succXEqSuccXPlusZero1, xPlusSuccZero2, succX3, substEq4, substEq5, cut6, cut7, cut8),
IndexedSeq(ax"ax3neutral", ax"ax4plusSuccessor")
@@ -187,45 +187,45 @@ object Peano {
/////////////// Induction step: ?y. (x + Sy === Sx + y) ==> (x + SSy === Sx + Sy) ////////////////////
val inductionStep1 = {
// x + SSy = S(x + Sy)
- val moveSuccessor0 = SCSubproof(instantiateForall(instantiateForallImport(ax"ax4plusSuccessor", x), s(y)), IndexedSeq(-2))
+ val moveSuccessor0 = SC.SCSubproof(instantiateForall(instantiateForallImport(ax"ax4plusSuccessor", x), s(y)), IndexedSeq(-2))
// Sx + Sy = S(Sx + y)
- val moveSuccessor1 = SCSubproof(instantiateForall(instantiateForallImport(ax"ax4plusSuccessor", s(x)), y), IndexedSeq(-2))
+ val moveSuccessor1 = SC.SCSubproof(instantiateForall(instantiateForallImport(ax"ax4plusSuccessor", s(x)), y), IndexedSeq(-2))
// ----------- x + SSy = S(x + Sy), x + Sy = Sx + y, S(Sx + y) = Sx + Sy |- x + SSy = Sx + Sy ------------
- val middleEq2 = RightRefl(() |- s(plus(x, s(y))) === s(plus(x, s(y))), s(plus(x, s(y))) === s(plus(x, s(y))))
+ val middleEq2 = SC.RightRefl(() |- s(plus(x, s(y))) === s(plus(x, s(y))), s(plus(x, s(y))) === s(plus(x, s(y))))
val substEq3 =
- RightSubstEq(
+ SC.RightSubstEq(
Set(plus(x, s(y)) === plus(s(x), y)) |- s(plus(x, s(y))) === s(plus(s(x), y)),
2,
(plus(x, s(y)), plus(s(x), y)) :: Nil,
LambdaTermFormula(Seq(z1), s(plus(x, s(y))) === s(z1))
)
val substEq4 =
- RightSubstEq(
+ SC.RightSubstEq(
Set(plus(x, s(y)) === plus(s(x), y), plus(x, s(s(y))) === s(plus(x, s(y)))) |- plus(x, s(s(y))) === s(plus(s(x), y)),
3,
(plus(x, s(s(y))), s(plus(x, s(y)))) :: Nil,
LambdaTermFormula(Seq(z1), z1 === s(plus(s(x), y)))
)
val substEq5 =
- RightSubstEq(
+ SC.RightSubstEq(
Set(plus(x, s(s(y))) === s(plus(x, s(y))), plus(x, s(y)) === plus(s(x), y), s(plus(s(x), y)) === plus(s(x), s(y))) |- plus(x, s(s(y))) === plus(s(x), s(y)),
4,
(s(plus(s(x), y)), plus(s(x), s(y))) :: Nil,
LambdaTermFormula(Seq(z1), plus(x, s(s(y))) === z1)
)
// -------------------------------------------------------------------------------------------------------
- val cut6 = Cut(Set(plus(x, s(y)) === plus(s(x), y), s(plus(s(x), y)) === plus(s(x), s(y))) |- plus(x, s(s(y))) === plus(s(x), s(y)), 0, 5, plus(x, s(s(y))) === s(plus(x, s(y))))
- val cut7 = Cut(plus(x, s(y)) === plus(s(x), y) |- plus(x, s(s(y))) === plus(s(x), s(y)), 1, 6, s(plus(s(x), y)) === plus(s(x), s(y)))
- val implies8 = RightImplies(() |- (plus(x, s(y)) === plus(s(x), y)) ==> (plus(x, s(s(y))) === plus(s(x), s(y))), 7, plus(x, s(y)) === plus(s(x), y), plus(x, s(s(y))) === plus(s(x), s(y)))
- val forall9 = RightForall(
+ val cut6 = SC.Cut(Set(plus(x, s(y)) === plus(s(x), y), s(plus(s(x), y)) === plus(s(x), s(y))) |- plus(x, s(s(y))) === plus(s(x), s(y)), 0, 5, plus(x, s(s(y))) === s(plus(x, s(y))))
+ val cut7 = SC.Cut(plus(x, s(y)) === plus(s(x), y) |- plus(x, s(s(y))) === plus(s(x), s(y)), 1, 6, s(plus(s(x), y)) === plus(s(x), s(y)))
+ val implies8 = SC.RightImplies(() |- (plus(x, s(y)) === plus(s(x), y)) ==> (plus(x, s(s(y))) === plus(s(x), s(y))), 7, plus(x, s(y)) === plus(s(x), y), plus(x, s(s(y))) === plus(s(x), s(y)))
+ val forall9 = SC.RightForall(
() |- forall(y, (plus(x, s(y)) === plus(s(x), y)) ==> (plus(x, s(s(y))) === plus(s(x), s(y)))),
8,
(plus(x, s(y)) === plus(s(x), y)) ==> (plus(x, s(s(y))) === plus(s(x), s(y))),
y
)
- SCSubproof(
+ SC.SCSubproof(
SCProof(
IndexedSeq(moveSuccessor0, moveSuccessor1, middleEq2, substEq3, substEq4, substEq5, cut6, cut7, implies8, forall9),
IndexedSeq(ax"ax3neutral", ax"ax4plusSuccessor")
@@ -235,8 +235,8 @@ object Peano {
}
val inductionInstance = {
- val inductionOnY0 = Rewrite(() |- (sPhi(zero) /\ forall(y, sPhi(y) ==> sPhi(s(y)))) ==> forall(y, sPhi(y)), -1)
- val inductionInstance1 = InstPredSchema(
+ val inductionOnY0 = SC.Rewrite(() |- (sPhi(zero) /\ forall(y, sPhi(y) ==> sPhi(s(y)))) ==> forall(y, sPhi(y)), -1)
+ val inductionInstance1 = SC.InstPredSchema(
() |-
((plus(s(x), zero) === plus(x, s(zero))) /\
forall(y, (plus(x, s(y)) === plus(s(x), y)) ==> (plus(x, s(s(y))) === plus(s(x), s(y))))) ==>
@@ -244,11 +244,11 @@ object Peano {
0,
Map(sPhi -> LambdaTermFormula(Seq(y), plus(x, s(y)) === plus(s(x), y)))
)
- SCSubproof(SCProof(IndexedSeq(inductionOnY0, inductionInstance1), IndexedSeq(ax"ax7induction")), Seq(-3))
+ SC.SCSubproof(SCProof(IndexedSeq(inductionOnY0, inductionInstance1), IndexedSeq(ax"ax7induction")), Seq(-3))
}
val inductionApplication = applyInduction(base0, inductionStep1, inductionInstance)
- val addForall = RightForall(() |- forall(x, forall(y, plus(x, s(y)) === plus(s(x), y))), inductionApplication.size - 1, forall(y, plus(x, s(y)) === plus(s(x), y)), x)
- val proof: SCProof = Proof(
+ val addForall = SC.RightForall(() |- forall(x, forall(y, plus(x, s(y)) === plus(s(x), y))), inductionApplication.size - 1, forall(y, plus(x, s(y)) === plus(s(x), y)), x)
+ val proof: SCProof = SCProof(
inductionApplication :+ addForall,
IndexedSeq(ax"ax3neutral", ax"ax4plusSuccessor", ax"ax7induction")
)
@@ -256,44 +256,45 @@ object Peano {
} using (ax"ax3neutral", ax"ax4plusSuccessor", ax"ax7induction")
show
- THEOREM("additivity of addition") of "∀'x. ∀'y. +('x, 'y) = +('y, 'x)" PROOF {
- val base0 = SCSubproof(instantiateForallImport(thm"x + 0 = 0 + x", x), Seq(-3))
+ THEOREM("additivity of addition") of "" PROOF2 {
+ val base0 = SC.SCSubproof(instantiateForallImport(thm"x + 0 = 0 + x", x), Seq(-3))
val inductionStep1 = {
- val start0 = RightRefl(() |- plus(x, s(y)) === plus(x, s(y)), plus(x, s(y)) === plus(x, s(y)))
+ val start0 = SC.RightRefl(() |- plus(x, s(y)) === plus(x, s(y)), plus(x, s(y)) === plus(x, s(y)))
val applyPlusSuccAx1 =
- RightSubstEq(plus(x, s(y)) === s(plus(x, y)) |- plus(x, s(y)) === s(plus(x, y)), 0, (plus(x, s(y)), s(plus(x, y))) :: Nil, LambdaTermFormula(Seq(z1), plus(x, s(y)) === z1))
+ SC.RightSubstEq(plus(x, s(y)) === s(plus(x, y)) |- plus(x, s(y)) === s(plus(x, y)), 0, (plus(x, s(y)), s(plus(x, y))) :: Nil, LambdaTermFormula(Seq(z1), plus(x, s(y)) === z1))
val applyInductionPremise2 =
- RightSubstEq(
+ SC.RightSubstEq(
Set(plus(x, s(y)) === s(plus(x, y)), plus(x, y) === plus(y, x)) |- plus(x, s(y)) === s(plus(y, x)),
1,
(plus(x, y), plus(y, x)) :: Nil,
LambdaTermFormula(Seq(z1), plus(x, s(y)) === s(z1))
)
val applyPlusSuccAx3 =
- RightSubstEq(
+ SC.RightSubstEq(
Set(plus(x, s(y)) === s(plus(x, y)), plus(x, y) === plus(y, x), s(plus(y, x)) === plus(y, s(x))) |- plus(x, s(y)) === plus(y, s(x)),
2,
(s(plus(y, x)), plus(y, s(x))) :: Nil,
LambdaTermFormula(Seq(z1), plus(x, s(y)) === z1)
)
val applySwitchSuccessor4 =
- RightSubstEq(
+ SC.RightSubstEq(
Set(plus(x, s(y)) === s(plus(x, y)), plus(x, y) === plus(y, x), s(plus(y, x)) === plus(y, s(x)), plus(y, s(x)) === plus(s(y), x)) |- plus(x, s(y)) === plus(s(y), x),
3,
(plus(y, s(x)), plus(s(y), x)) :: Nil,
LambdaTermFormula(Seq(z1), plus(x, s(y)) === z1)
)
- val xPlusSYInstance5 = SCSubproof(instantiateForall(instantiateForallImport(ax"ax4plusSuccessor", x), y), Seq(-1))
- val cutXPlusSY6 = Cut(Set(plus(x, y) === plus(y, x), s(plus(y, x)) === plus(y, s(x)), plus(y, s(x)) === plus(s(y), x)) |- plus(x, s(y)) === plus(s(y), x), 5, 4, plus(x, s(y)) === s(plus(x, y)))
- val yPlusSXInstance7 = SCSubproof(instantiateForall(instantiateForallImport(ax"ax4plusSuccessor", y), x), Seq(-1))
- val cutYPlusSX8 = Cut(Set(plus(x, y) === plus(y, x), plus(y, s(x)) === plus(s(y), x)) |- plus(x, s(y)) === plus(s(y), x), 7, 6, s(plus(y, x)) === plus(y, s(x)))
- val swichSuccessorInstance9 = SCSubproof(instantiateForall(instantiateForallImport(thm"switch successor", y), x), Seq(-2))
- val cutSwitchSuccessor10 = Cut(plus(x, y) === plus(y, x) |- plus(x, s(y)) === plus(s(y), x), 9, 8, plus(y, s(x)) === plus(s(y), x))
- val rightImplies11 = RightImplies(() |- (plus(x, y) === plus(y, x)) ==> (plus(x, s(y)) === plus(s(y), x)), 10, plus(x, y) === plus(y, x), plus(x, s(y)) === plus(s(y), x))
- val forall12 = RightForall(() |- forall(y, (plus(x, y) === plus(y, x)) ==> (plus(x, s(y)) === plus(s(y), x))), 11, (plus(x, y) === plus(y, x)) ==> (plus(x, s(y)) === plus(s(y), x)), y)
- SCSubproof(
- Proof(
+ val xPlusSYInstance5 = SC.SCSubproof(instantiateForall(instantiateForallImport(ax"ax4plusSuccessor", x), y), Seq(-1))
+ val cutXPlusSY6 =
+ SC.Cut(Set(plus(x, y) === plus(y, x), s(plus(y, x)) === plus(y, s(x)), plus(y, s(x)) === plus(s(y), x)) |- plus(x, s(y)) === plus(s(y), x), 5, 4, plus(x, s(y)) === s(plus(x, y)))
+ val yPlusSXInstance7 = SC.SCSubproof(instantiateForall(instantiateForallImport(ax"ax4plusSuccessor", y), x), Seq(-1))
+ val cutYPlusSX8 = SC.Cut(Set(plus(x, y) === plus(y, x), plus(y, s(x)) === plus(s(y), x)) |- plus(x, s(y)) === plus(s(y), x), 7, 6, s(plus(y, x)) === plus(y, s(x)))
+ val swichSuccessorInstance9 = SC.SCSubproof(instantiateForall(instantiateForallImport(thm"switch successor", y), x), Seq(-2))
+ val cutSwitchSuccessor10 = SC.Cut(plus(x, y) === plus(y, x) |- plus(x, s(y)) === plus(s(y), x), 9, 8, plus(y, s(x)) === plus(s(y), x))
+ val rightImplies11 = SC.RightImplies(() |- (plus(x, y) === plus(y, x)) ==> (plus(x, s(y)) === plus(s(y), x)), 10, plus(x, y) === plus(y, x), plus(x, s(y)) === plus(s(y), x))
+ val forall12 = SC.RightForall(() |- forall(y, (plus(x, y) === plus(y, x)) ==> (plus(x, s(y)) === plus(s(y), x))), 11, (plus(x, y) === plus(y, x)) ==> (plus(x, s(y)) === plus(s(y), x)), y)
+ SC.SCSubproof(
+ SCProof(
IndexedSeq(
start0,
applyPlusSuccAx1,
@@ -316,8 +317,8 @@ object Peano {
}
val inductionInstance = {
- val inductionOnY0 = Rewrite(() |- (sPhi(zero) /\ forall(y, sPhi(y) ==> sPhi(s(y)))) ==> forall(y, sPhi(y)), -1)
- val inductionInstance1 = InstPredSchema(
+ val inductionOnY0 = SC.Rewrite(() |- (sPhi(zero) /\ forall(y, sPhi(y) ==> sPhi(s(y)))) ==> forall(y, sPhi(y)), -1)
+ val inductionInstance1 = SC.InstPredSchema(
() |-
((plus(x, zero) === plus(zero, x)) /\
forall(y, (plus(x, y) === plus(y, x)) ==> (plus(x, s(y)) === plus(s(y), x)))) ==>
@@ -325,11 +326,11 @@ object Peano {
0,
Map(sPhi -> LambdaTermFormula(Seq(y), plus(x, y) === plus(y, x)))
)
- SCSubproof(SCProof(IndexedSeq(inductionOnY0, inductionInstance1), IndexedSeq(ax"ax7induction")), Seq(-2))
+ SC.SCSubproof(SCProof(IndexedSeq(inductionOnY0, inductionInstance1), IndexedSeq(ax"ax7induction")), Seq(-2))
}
val inductionApplication = applyInduction(base0, inductionStep1, inductionInstance)
- val addForall = RightForall(() |- forall(x, forall(y, plus(x, y) === plus(y, x))), inductionApplication.size - 1, forall(y, plus(x, y) === plus(y, x)), x)
- val proof: SCProof = Proof(
+ val addForall = SC.RightForall(() |- forall(x, forall(y, plus(x, y) === plus(y, x))), inductionApplication.size - 1, forall(y, plus(x, y) === plus(y, x)), x)
+ val proof: SCProof = SCProof(
inductionApplication :+ addForall,
IndexedSeq(ax"ax4plusSuccessor", ax"ax7induction", thm"x + 0 = 0 + x", thm"switch successor")
)
diff --git a/src/test/scala/lisa/utilities/Transformations.scala b/src/test/scala/lisa/utilities/Transformations.scala
index f51cf3aa..4fb80659 100644
--- a/src/test/scala/lisa/utilities/Transformations.scala
+++ b/src/test/scala/lisa/utilities/Transformations.scala
@@ -1,14 +1,16 @@
package lisa.utilities
import lisa.automation.kernel.Destructors.*
import lisa.automation.kernel.ProofTactics.*
-import lisa.kernel.fol.*
+import lisa.kernel.fol.FOL
+import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.SCProof
+import lisa.kernel.proof.SequentCalculus.*
import lisa.test.ProofCheckerSuite
-import lisa.utils.Helpers.given_Conversion_VariableLabel_Term
+import lisa.utils.Helpers.{_, given}
import lisa.utils.Printer
class Transformations extends ProofCheckerSuite {
- import lisa.settheory.SetTheoryLibrary.*
+ // import lisa.settheory.SetTheoryLibrary.*
test("Trasnsformation initialises well with empty proof and returns an empty proof") {
val nullSCProof = SCProof()
--
GitLab