diff --git a/lisa-examples/src/main/scala/Example.scala b/lisa-examples/src/main/scala/Example.scala
index d494a5222e25a1e35b95a2a19aabf47ff7ff342a..00a566cfcc080853d84838a66a405f9e73966e63 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 56981317d898906782d135b24b9458fdcdfd8f58..16af6f19d7cb4defeba3bb11b1af69c1c5d115a1 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 cfcb6846d43d5f1d85ca03192ea0d9bcc21a7c4c..5acd4867851eea3f9762662c60634ac6ae0764f1 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 9f6cfbc4858269d67a58d097cfcfeb3dbaf22bf3..a115e4c681db32b72666d9abe3c0ea9184aac51d 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 0000000000000000000000000000000000000000..612bd42ae49f7f4a3593628a69501405163a9957
--- /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 0000000000000000000000000000000000000000..57a9a4be766d81ce93e0ed641b87710c31ba36b2
--- /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 0000000000000000000000000000000000000000..99c81eb29d5cc619bccc8dbf09fb276661042314
--- /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 0000000000000000000000000000000000000000..2fa04fdd125b8cac21cdf053844f896d8a736456
--- /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 0000000000000000000000000000000000000000..5516124b4d266223183f4c9057c5867ff92bce48
--- /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 0000000000000000000000000000000000000000..832110978ae74f5ad08c5d29290c4a640d539efd
--- /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 ab43254c250ccfe7fbc06550fc8c14cea36d87a2..def2e6640e2e99a8e66fdd6ce0524bc125113f6b 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 f318e41090dcd64a142a9cc59d0343b740ea7494..f45db00fb846349ac74aa2f4feb9cbc16855f5d3 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 c02bd0c0f4fe96e3c9987d0f4d9de496655d316d..1b902db309846a3ba932a1b595eaaccc3cf2e15a 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 47642c624698b6782cfd529af4b1d6a5c9b78132..6cbc144da28866b773eb3f388346e1736c96e52e 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 f51cf3aadef181ecdf4fa27f618516fc080f5f19..4fb80659f1065ccaf6491337d1f895e99e784a4d 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()