From 572ed12432d034ea55fb9080855f907513dc5565 Mon Sep 17 00:00:00 2001
From: Sankalp Gambhir <sankalp.gambhir47@gmail.com>
Date: Tue, 1 Nov 2022 14:07:34 +0100
Subject: [PATCH 1/6] Proof checking at higher abstraction level - Left
propositional rules
---
.../lisa/utils/tactics/BasicStepTactic.scala | 315 ++++++++++++++----
1 file changed, 241 insertions(+), 74 deletions(-)
diff --git a/lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala b/lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala
index 9c02f590..59f81b59 100644
--- a/lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala
@@ -12,13 +12,34 @@ 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)
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ val intersectedPivot = bot.left.intersect(bot.right)
+
+ if (!intersectedPivot.isEmpty)
+ SC.Hypothesis(bot, intersectedPivot.head)
+ else
+ ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ "A formula for input to hypothesis could not be inferred from left and right side of sequent."
+ )
+ }
}
case object Rewrite extends ProofStepWithoutBotNorPrem(1) {
- def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
- SC.Rewrite(bot, premises(0))
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ if (premises.length != 1)
+ ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ s"One premise expected, ${premises.length} received."
+ )
+ else if (SC.isSameSequent(bot, currentProof.getSequent(premises(0))))
+ SC.Rewrite(bot, premises(0))
+ else
+ ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ "The premise and the conclusion are not trivially equivalent."
+ )
+ }
}
/**
@@ -29,30 +50,54 @@ object BasicStepTactic {
* </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)
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val leftSequent = currentProof.getSequent(premises(0))
+ lazy val rightSequent = currentProof.getSequent(premises(1))
+
+ if (premises.length != 2)
+ invalid(s"Two premises expected, ${premises.length} received.")
+ else if (!contains(leftSequent.right, phi))
+ invalid("Right-hand side of first premise does not contain φ as claimed.")
+ else if (!contains(rightSequent.left, phi))
+ invalid("Left-hand side of second premise does not contain φ as claimed.")
+ else if (!isSameSet(bot.left, leftSequent.left ++ rightSequent.left.filterNot(isSame(_, phi))))
+ invalid("Left-hand side of conclusion + φ is not the union of the left-hand sides of the premises.")
+ else if (!isSameSet(bot.right, leftSequent.right.filterNot(isSame(_, phi)) ++ rightSequent.right))
+ invalid("Right-hand side of conclusion + φ is not the union of the right-hand sides of the premises.")
+ else
+ 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)
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val leftSequent = currentProof.getSequent(premises(0))
+ lazy val rightSequent = currentProof.getSequent(premises(1))
+ lazy 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.")
+ if (premises.length != 2)
+ invalid(s"Two premises expected, ${premises.length} received.")
+ else if (!cutSet.isEmpty)
+ if (cutSet.tail.isEmpty)
+ Cut(cutSet.head).asSCProof(bot, premises, currentProof)
+ else
+ invalid("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)
+ Cut(intersectedCutSet.head).asSCProof(bot, premises, currentProof)
else
- ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- "A consistent cut pivot cannot be inferred from the premises. Possibly a missing or extraneous clause."
- )
+ invalid("A consistent cut pivot cannot be inferred from the premises. Possibly a missing or extraneous clause.")
}
}
@@ -76,33 +121,57 @@ object BasicStepTactic {
* </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)
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val premiseSequent = currentProof.getSequent(premises(0))
+ lazy val phiAndPsi = ConnectorFormula(And, Seq(phi, psi))
+
+ if (premises.length != 1)
+ invalid(s"One premise expected, ${premises.length} received.")
+ else if (!isSameSet(bot.right, premiseSequent.right))
+ invalid("Right-hand sides of the premise and the conclusion must be the same.")
+ else if (
+ !isSameSet(bot.left + phi, premiseSequent.left + phiAndPsi) &&
+ !isSameSet(bot.left + psi, premiseSequent.left + phiAndPsi) &&
+ !isSameSet(bot.left + phi + psi, premiseSequent.left + phiAndPsi)
+ )
+ invalid("Left-hand side of conclusion + φ∧ψ must be same as left-hand side of premise + either φ, ψ or both.")
+ else
+ 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)
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val premiseSequent = currentProof.getSequent(premises(0))
+ lazy val pivot = bot.left.diff(premiseSequent.left)
+
+ if (premises.length != 1)
+ invalid(s"One premise expected, ${premises.length} received.")
+ else 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)
+ LeftAnd(phi, psi).asSCProof(bot, premises, currentProof)
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.")
+ LeftAnd(psi, phi).asSCProof(bot, premises, currentProof)
+ case _ => invalid("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."
- )
+ // try a rewrite, if it works, go ahead with it, otherwise malformed
+ if (SC.isSameSequent(premiseSequent, bot))
+ Rewrite.asSCProof(bot, premises, currentProof)
+ else
+ invalid("Left-hand side of conclusion + φ∧ψ must be same as left-hand side of premise + either φ, ψ or both.")
}
}
@@ -125,24 +194,44 @@ object BasicStepTactic {
*/
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)
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val premiseSequents = premises.map(currentProof.getSequent(_))
+ lazy val disjunction = ConnectorFormula(Or, disjuncts)
+
+
+ if (premises.length == 0)
+ invalid(s"Premises expected, ${premises.length} received.")
+ else if (!isSameSet(bot.right, premiseSequents.map(_.right).reduce(_ union _)))
+ invalid("Right-hand side of conclusion is not the union of the right-hand sides of the premises.")
+ else if (!isSameSet(disjuncts.foldLeft(bot.left)(_ + _), premiseSequents.map(_.left).reduce(_ union _) + disjunction))
+ invalid("Left-hand side of conclusion + disjuncts is not the same as the union of the left-hand sides of the premises + φ∨ψ.")
+ else
+ 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)))
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val premiseSequents = premises.map(currentProof.getSequent(_))
+ lazy val pivots = premiseSequents.map(_.left.diff(bot.left))
+
+ if (premises.length == 0)
+ invalid(s"Premises expected, ${premises.length} received.")
+ else if (pivots.exists(_.isEmpty))
+ Weakening.asSCProof(bot, Seq(premises(pivots.indexWhere(_.isEmpty))), currentProof)
else if (pivots.forall(_.tail.isEmpty))
- SC.LeftOr(bot, premises, pivots.map(_.head))
+ LeftOr(pivots.map(_.head)).asSCProof(bot, premises, currentProof)
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 + φ∨ψ."
- )
+ invalid("Left-hand side of conclusion + disjuncts is not the same as the union of the left-hand sides of the premises + φ∨ψ.")
}
}
@@ -164,23 +253,48 @@ object BasicStepTactic {
* </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)
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val leftSequent = currentProof.getSequent(premises(0))
+ lazy val rightSequent = currentProof.getSequent(premises(1))
+ lazy val implication = ConnectorFormula(Implies, Seq(phi, psi))
+
+
+ if (premises.length != 2)
+ invalid(s"Two premises expected, ${premises.length} received.")
+ else if (!isSameSet(bot.right + phi, leftSequent.right union rightSequent.right))
+ invalid("Right-hand side of conclusion + φ must be identical to union of right-hand sides of premises.")
+ else if (!isSameSet(bot.left + psi, leftSequent.left union rightSequent.left + implication))
+ invalid("Left-hand side of conclusion + ψ must be identical to union of left-hand sides of premises + φ→ψ.")
+ else
+ 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)
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val leftSequent = currentProof.getSequent(premises(0))
+ lazy val rightSequent = currentProof.getSequent(premises(1))
+ lazy val pivotLeft = leftSequent.right.diff(bot.right)
lazy val pivotRight = rightSequent.left.diff(bot.left)
- if (pivotLeft.isEmpty)
- SC.Weakening(bot, premises(0))
+ if (premises.length != 2)
+ invalid(s"Two premises expected, ${premises.length} received.")
+ else if (pivotLeft.isEmpty)
+ Weakening.asSCProof(bot, premises, currentProof)
else if (pivotRight.isEmpty)
- SC.Weakening(bot, premises(1))
+ Weakening.asSCProof(bot, premises, currentProof)
else if (pivotLeft.tail.isEmpty && pivotRight.tail.isEmpty)
- SC.LeftImplies(bot, premises(0), premises(1), pivotLeft.head, pivotRight.head)
+ LeftImplies(pivotLeft.head, pivotRight.head).asSCProof(bot, premises, currentProof)
else
ProofStepJudgement.InvalidProofStep(
this.asProofStepWithoutBot(premises).asProofStep(bot),
@@ -207,21 +321,51 @@ object BasicStepTactic {
* </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)
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val premiseSequent = currentProof.getSequent(premises(0))
+ lazy val implication = ConnectorFormula(Iff, Seq(phi, psi))
+ lazy val impLeft = ConnectorFormula(Implies, Seq(phi, psi))
+ lazy val impRight = ConnectorFormula(Implies, Seq(psi, phi))
+
+
+ if (premises.length != 1)
+ invalid(s"One premise expected, ${premises.length} received.")
+ else if (!isSameSet(bot.right, premiseSequent.right))
+ invalid("Right-hand sides of premise and conclusion must be the same.")
+ else if (
+ !isSameSet(bot.left + impLeft, premiseSequent.left + implication) &&
+ !isSameSet(bot.left + impRight, premiseSequent.left + implication) &&
+ !isSameSet(bot.left + impLeft + impRight, premiseSequent.left + implication)
+ )
+ invalid("Left-hand side of conclusion + φ↔ψ must be same as left-hand side of premise + either φ→ψ, ψ→φ or both.")
+ else
+ 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))
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val premiseSequent = currentProof.getSequent(premises(0))
+ lazy val pivot = premiseSequent.left.diff(bot.left)
+
+ if (premises.length != 1)
+ invalid(s"One premise expected, ${premises.length} received.")
+ else if (pivot.isEmpty)
+ Weakening.asSCProof(bot, premises, currentProof)
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 ConnectorFormula(Implies, Seq(phi, psi)) => LeftIff(phi, psi).asSCProof(bot, premises, currentProof)
+ case _ => invalid("Could not infer a pivot implication from premise.")
}
}
}
@@ -244,21 +388,44 @@ object BasicStepTactic {
* </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)
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val premiseSequent = currentProof.getSequent(premises(0))
+ lazy val negation = ConnectorFormula(Neg, Seq(phi))
+
+ if (premises.length != 1)
+ invalid(s"One premise expected, ${premises.length} received.")
+ else if (!isSameSet(bot.right + phi, premiseSequent.right))
+ invalid("Right-hand side of conclusion + φ must be the same as right-hand side of premise.")
+ else if (!isSameSet(bot.left, premiseSequent.left + negation))
+ invalid("Left-hand side of conclusion must be the same as left-hand side of premise + ¬φ.")
+ else
+ 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))
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val premiseSequent = currentProof.getSequent(premises(0))
+ lazy val pivot = premiseSequent.right.diff(bot.right)
+
+ if (premises.length != 1)
+ invalid(s"One premise expected, ${premises.length} received.")
+ else if (pivot.isEmpty)
+ Weakening.asSCProof(bot, premises, currentProof)
else if (pivot.tail.isEmpty)
- SC.LeftNot(bot, premises(0), pivot.head)
+ LeftNot(pivot.head).asSCProof(bot, premises, currentProof)
else
- ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Right-hand side of conclusion + φ must be the same as right-hand side of premise.")
+ invalid("Right-hand side of conclusion + φ must be the same as right-hand side of premise.")
}
}
--
GitLab
From cf2107b186c98c514bc0ce5c0ed03b448df47a07 Mon Sep 17 00:00:00 2001
From: Sankalp Gambhir <sankalp.gambhir47@gmail.com>
Date: Tue, 1 Nov 2022 18:24:22 +0100
Subject: [PATCH 2/6] Left rules - proof checking during construction
---
.../lisa/utils/tactics/BasicStepTactic.scala | 210 ++++++++++++------
1 file changed, 144 insertions(+), 66 deletions(-)
diff --git a/lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala b/lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala
index 59f81b59..97340316 100644
--- a/lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala
@@ -13,32 +13,35 @@ object BasicStepTactic {
case object Hypothesis extends ProofStepWithoutBotNorPrem(0) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
- val intersectedPivot = bot.left.intersect(bot.right)
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
- if (!intersectedPivot.isEmpty)
- SC.Hypothesis(bot, intersectedPivot.head)
+ lazy val intersectedPivot = bot.left.intersect(bot.right)
+
+ if (premises.length != 0)
+ invalid(s"No premises expected, ${premises.length} received.")
+ else if (intersectedPivot.isEmpty)
+ invalid("A formula for input to hypothesis could not be inferred from left and right side of sequent.")
else
- ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- "A formula for input to hypothesis could not be inferred from left and right side of sequent."
- )
+ SC.Hypothesis(bot, intersectedPivot.head)
}
}
case object Rewrite extends ProofStepWithoutBotNorPrem(1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
if (premises.length != 1)
- ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- s"One premise expected, ${premises.length} received."
- )
- else if (SC.isSameSequent(bot, currentProof.getSequent(premises(0))))
- SC.Rewrite(bot, premises(0))
+ invalid(s"One premise expected, ${premises.length} received.")
+ else if (!SC.isSameSequent(bot, currentProof.getSequent(premises(0))))
+ invalid("The premise and the conclusion are not trivially equivalent.")
else
- ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- "The premise and the conclusion are not trivially equivalent."
- )
+ SC.Rewrite(bot, premises(0))
}
}
@@ -139,7 +142,7 @@ object BasicStepTactic {
!isSameSet(bot.left + psi, premiseSequent.left + phiAndPsi) &&
!isSameSet(bot.left + phi + psi, premiseSequent.left + phiAndPsi)
)
- invalid("Left-hand side of conclusion + φ∧ψ must be same as left-hand side of premise + either φ, ψ or both.")
+ invalid("Left-hand side of premise + φ∧ψ must be same as left-hand side of conclusion + either φ, ψ or both.")
else
SC.LeftAnd(bot, premises(0), phi, psi)
}
@@ -171,7 +174,7 @@ object BasicStepTactic {
if (SC.isSameSequent(premiseSequent, bot))
Rewrite.asSCProof(bot, premises, currentProof)
else
- invalid("Left-hand side of conclusion + φ∧ψ must be same as left-hand side of premise + either φ, ψ or both.")
+ invalid("Left-hand side of premise + φ∧ψ must be same as left-hand side of conclusion + either φ, ψ or both.")
}
}
@@ -213,7 +216,7 @@ object BasicStepTactic {
SC.LeftOr(bot, premises, disjuncts)
}
}
- case class LeftOrWithoutFormula() extends ProofStepWithoutBotNorPrem(-1) {
+ case object LeftOrWithoutFormula extends ProofStepWithoutBotNorPrem(-1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
this.asProofStepWithoutBot(premises).asProofStep(bot),
@@ -238,7 +241,7 @@ object BasicStepTactic {
case object LeftOr extends ProofStepWithoutBotNorPrem(-1) {
// default construction:
// def apply(disjuncts: Seq[Formula]) = new LeftOr(disjuncts)
- def apply() = new LeftOrWithoutFormula()
+ def apply() = LeftOrWithoutFormula
// usage without an argument list
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
@@ -296,10 +299,7 @@ object BasicStepTactic {
else if (pivotLeft.tail.isEmpty && pivotRight.tail.isEmpty)
LeftImplies(pivotLeft.head, pivotRight.head).asSCProof(bot, premises, currentProof)
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."
- )
+ invalid("Could not infer an implication as a pivot from the premises and conclusion, possible extraneous formulae in premises.")
}
}
@@ -342,13 +342,13 @@ object BasicStepTactic {
!isSameSet(bot.left + impRight, premiseSequent.left + implication) &&
!isSameSet(bot.left + impLeft + impRight, premiseSequent.left + implication)
)
- invalid("Left-hand side of conclusion + φ↔ψ must be same as left-hand side of premise + either φ→ψ, ψ→φ or both.")
+ invalid("Left-hand side of premise + φ↔ψ must be same as left-hand side of conclusion + either φ→ψ, ψ→φ or both.")
else
SC.LeftIff(bot, premises(0), phi, psi)
}
}
- case class LeftIffWithoutFormula() extends ProofStepWithoutBotNorPrem(1) {
+ case object LeftIffWithoutFormula extends ProofStepWithoutBotNorPrem(1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
this.asProofStepWithoutBot(premises).asProofStep(bot),
@@ -373,7 +373,7 @@ object BasicStepTactic {
case object LeftIff extends ProofStepWithoutBotNorPrem(1) {
// default construction:
// def apply(phi: Formula, psi: Formula) = new LeftIff(phi, psi)
- def apply() = new LeftIffWithoutFormula()
+ def apply() = LeftIffWithoutFormula
// usage without an argument list
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
@@ -408,7 +408,7 @@ object BasicStepTactic {
}
}
- case class LeftNotWithoutFormula() extends ProofStepWithoutBotNorPrem(1) {
+ case object LeftNotWithoutFormula extends ProofStepWithoutBotNorPrem(1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
this.asProofStepWithoutBot(premises).asProofStep(bot),
@@ -433,7 +433,7 @@ object BasicStepTactic {
case object LeftNot extends ProofStepWithoutBotNorPrem(1) {
// default construction:
// def apply(phi: Formula) = new LeftNot(phi)
- def apply() = new LeftNotWithoutFormula()
+ def apply() = LeftNotWithoutFormula
// usage without an argument list
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
@@ -449,25 +449,49 @@ object BasicStepTactic {
* </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)
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val premiseSequent = currentProof.getSequent(premises(0))
+ lazy val quantified = BinderFormula(Forall, x, phi)
+ lazy val instantiated = substituteVariables(phi, Map(x -> t))
+
+ if (premises.length != 1)
+ invalid(s"One premise expected, ${premises.length} received.")
+ else if (!isSameSet(bot.right, premiseSequent.right))
+ invalid("Right-hand side of conclusion must be the same as right-hand side of premise")
+ else if (!isSameSet(bot.left + instantiated, premiseSequent.left + quantified))
+ invalid("Left-hand side of conclusion + φ[t/x] must be the same as left-hand side of premise + ∀x. φ")
+ else
+ 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)
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val premiseSequent = currentProof.getSequent(premises(0))
+ lazy val pivot = bot.left.diff(premiseSequent.left)
lazy val instantiatedPivot = premiseSequent.left.diff(bot.left)
- if (!pivot.isEmpty)
+ if (premises.length != 1)
+ invalid(s"One premise expected, ${premises.length} received.")
+ else 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.")
+ case BinderFormula(Forall, x, phi) => LeftForall(phi, x, t).asSCProof(bot, premises, currentProof)
+ case _ => invalid("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))
+ invalid("Left-hand side of conclusion + φ[t/x] must be the same as left-hand side of premise + ∀x. φ.")
+ else if (instantiatedPivot.isEmpty) Weakening.asSCProof(bot, premises, currentProof)
else if (instantiatedPivot.tail.isEmpty) {
// go through conclusion to find a matching quantified formula
@@ -480,10 +504,12 @@ object BasicStepTactic {
)
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.")
+ case Some(BinderFormula(Forall, x, phi)) => LeftForall(phi, x, t).asSCProof(bot, premises, currentProof)
+ case _ => invalid("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
+ invalid("Left-hand side of conclusion + φ[t/x] must be the same as left-hand side of premise + ∀x. φ.")
}
}
@@ -510,18 +536,43 @@ object BasicStepTactic {
* </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)
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val premiseSequent = currentProof.getSequent(premises(0))
+ lazy val quantified = BinderFormula(Exists, x, phi)
+
+ if (premises.length != 1)
+ invalid(s"One premise expected, ${premises.length} received.")
+ else if ((bot.left union bot.right).exists(_.freeVariables.contains(x)))
+ invalid("The variable x must not be free in the resulting sequent.")
+ else if (!isSameSet(bot.right, premiseSequent.right))
+ invalid("Right-hand side of conclusion must be the same as right-hand side of premise")
+ else if (!isSameSet(bot.left + phi, premiseSequent.left + quantified))
+ invalid("Left-hand side of conclusion + φ must be the same as left-hand side of premise + ∃x. φ")
+ else
+ SC.LeftExists(bot, premises(0), phi, x)
+ }
}
- case class LeftExistsWithoutFormula() extends ProofStepWithoutBotNorPrem(1) {
+ case object 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)
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val premiseSequent = currentProof.getSequent(premises(0))
+ lazy 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))
+ if (premises.length != 1)
+ invalid(s"One premise expected, ${premises.length} received.")
+ else if (pivot.isEmpty)
+ if (instantiatedPivot.isEmpty) Rewrite.asSCProof(bot, premises, currentProof)
else if (instantiatedPivot.tail.isEmpty) {
val in: Formula = instantiatedPivot.head
val quantifiedPhi: Option[Formula] = bot.left.find(f =>
@@ -532,24 +583,26 @@ object BasicStepTactic {
)
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.")
+ case Some(BinderFormula(Exists, x, phi)) => LeftExists(phi, x).asSCProof(bot, premises, currentProof)
+ case _ => invalid("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
+ invalid("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.")
+ case BinderFormula(Exists, x, phi) => LeftExists(phi, x).asSCProof(bot, premises, currentProof)
+ case _ => invalid("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. φ.")
+ invalid("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()
+ def apply() = LeftExistsWithoutFormula
// usage without an argument list
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
@@ -564,34 +617,59 @@ object BasicStepTactic {
* </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)
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val premiseSequent = currentProof.getSequent(premises(0))
+ lazy val y = VariableLabel(freshId(phi.freeVariables.map(_.id) + x.id, "y"))
+ lazy val instantiated = BinderFormula(Exists, y, BinderFormula(Forall, x, ConnectorFormula(Iff, List(PredicateFormula(equality, List(VariableTerm(x), VariableTerm(y))), phi))))
+ lazy val quantified = BinderFormula(ExistsOne, x, phi)
+
+ if (premises.length != 1)
+ invalid(s"One premise expected, ${premises.length} received.")
+ else if (!isSameSet(bot.right, premiseSequent.right))
+ invalid("Right-hand side of conclusion must be the same as right-hand side of premise.")
+ else if (!isSameSet(bot.left + instantiated, premiseSequent.left + quantified))
+ invalid("Left-hand side of conclusion + ∃y.∀x. (x=y) ↔ φ must be the same as left-hand side of premise + ∃!x. φ.")
+ else
+ 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)
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val premiseSequent = currentProof.getSequent(premises(0))
+ lazy val pivot = bot.left.diff(premiseSequent.left)
lazy val instantiatedPivot = premiseSequent.left.diff(bot.left)
- if (pivot.isEmpty)
+ if (premises.length != 1)
+ invalid(s"One premise expected, ${premises.length} received.")
+ else if (pivot.isEmpty)
if (instantiatedPivot.isEmpty)
- SC.Rewrite(bot, premises(0))
+ Rewrite.asSCProof(bot, premises, currentProof)
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 BinderFormula(Exists, _, BinderFormula(Forall, x, ConnectorFormula(Iff, Seq(_, phi)))) => LeftExistsOne(phi, x).asSCProof(bot, premises, currentProof)
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. φ.")
+ invalid("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.")
+ case _ => invalid("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. φ.")
+ invalid("Left-hand side of conclusion + φ must be the same as left-hand side of premise + ∃x. φ.")
}
}
--
GitLab
From da82badb27160493519f60866556bd1ca51dc94d Mon Sep 17 00:00:00 2001
From: Sankalp Gambhir <sankalp.gambhir47@gmail.com>
Date: Tue, 1 Nov 2022 20:22:51 +0100
Subject: [PATCH 3/6] Right prop and reflixivity rules, documentation
---
.../lisa/utils/tactics/BasicStepTactic.scala | 572 +++++++++++++-----
1 file changed, 423 insertions(+), 149 deletions(-)
diff --git a/lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala b/lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala
index 97340316..c1702bef 100644
--- a/lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala
@@ -136,13 +136,13 @@ object BasicStepTactic {
if (premises.length != 1)
invalid(s"One premise expected, ${premises.length} received.")
else if (!isSameSet(bot.right, premiseSequent.right))
- invalid("Right-hand sides of the premise and the conclusion must be the same.")
+ invalid("Right-hand side of the conclusion is not the same as the right-hand side of the premise.")
else if (
!isSameSet(bot.left + phi, premiseSequent.left + phiAndPsi) &&
!isSameSet(bot.left + psi, premiseSequent.left + phiAndPsi) &&
!isSameSet(bot.left + phi + psi, premiseSequent.left + phiAndPsi)
)
- invalid("Left-hand side of premise + φ∧ψ must be same as left-hand side of conclusion + either φ, ψ or both.")
+ invalid("Left-hand side of premise + φ∧ψ is not the same as left-hand side of conclusion + either φ, ψ or both.")
else
SC.LeftAnd(bot, premises(0), phi, psi)
}
@@ -174,7 +174,7 @@ object BasicStepTactic {
if (SC.isSameSequent(premiseSequent, bot))
Rewrite.asSCProof(bot, premises, currentProof)
else
- invalid("Left-hand side of premise + φ∧ψ must be same as left-hand side of conclusion + either φ, ψ or both.")
+ invalid("Left-hand side of premise + φ∧ψ is not the same as left-hand side of conclusion + either φ, ψ or both.")
}
}
@@ -270,9 +270,9 @@ object BasicStepTactic {
if (premises.length != 2)
invalid(s"Two premises expected, ${premises.length} received.")
else if (!isSameSet(bot.right + phi, leftSequent.right union rightSequent.right))
- invalid("Right-hand side of conclusion + φ must be identical to union of right-hand sides of premises.")
+ invalid("Right-hand side of conclusion + φ is not the union of right-hand sides of premises.")
else if (!isSameSet(bot.left + psi, leftSequent.left union rightSequent.left + implication))
- invalid("Left-hand side of conclusion + ψ must be identical to union of left-hand sides of premises + φ→ψ.")
+ invalid("Left-hand side of conclusion + ψ is not the union of left-hand sides of premises + φ→ψ.")
else
SC.LeftImplies(bot, premises(0), premises(1), phi, psi)
}
@@ -336,13 +336,13 @@ object BasicStepTactic {
if (premises.length != 1)
invalid(s"One premise expected, ${premises.length} received.")
else if (!isSameSet(bot.right, premiseSequent.right))
- invalid("Right-hand sides of premise and conclusion must be the same.")
+ invalid("Right-hand side of premise is not the same as right-hand side of conclusion.")
else if (
!isSameSet(bot.left + impLeft, premiseSequent.left + implication) &&
!isSameSet(bot.left + impRight, premiseSequent.left + implication) &&
!isSameSet(bot.left + impLeft + impRight, premiseSequent.left + implication)
)
- invalid("Left-hand side of premise + φ↔ψ must be same as left-hand side of conclusion + either φ→ψ, ψ→φ or both.")
+ invalid("Left-hand side of premise + φ↔ψ is not the same as left-hand side of conclusion + either φ→ψ, ψ→φ or both.")
else
SC.LeftIff(bot, premises(0), phi, psi)
}
@@ -400,9 +400,9 @@ object BasicStepTactic {
if (premises.length != 1)
invalid(s"One premise expected, ${premises.length} received.")
else if (!isSameSet(bot.right + phi, premiseSequent.right))
- invalid("Right-hand side of conclusion + φ must be the same as right-hand side of premise.")
+ invalid("Right-hand side of conclusion + φ is not the same as right-hand side of premise.")
else if (!isSameSet(bot.left, premiseSequent.left + negation))
- invalid("Left-hand side of conclusion must be the same as left-hand side of premise + ¬φ.")
+ invalid("Left-hand side of conclusion is not the same as left-hand side of premise + ¬φ.")
else
SC.LeftNot(bot, premises(0), phi)
}
@@ -425,7 +425,7 @@ object BasicStepTactic {
else if (pivot.tail.isEmpty)
LeftNot(pivot.head).asSCProof(bot, premises, currentProof)
else
- invalid("Right-hand side of conclusion + φ must be the same as right-hand side of premise.")
+ invalid("Right-hand side of conclusion + φ is not the same as right-hand side of premise.")
}
}
@@ -462,9 +462,9 @@ object BasicStepTactic {
if (premises.length != 1)
invalid(s"One premise expected, ${premises.length} received.")
else if (!isSameSet(bot.right, premiseSequent.right))
- invalid("Right-hand side of conclusion must be the same as right-hand side of premise")
+ invalid("Right-hand side of conclusion is not the same as right-hand side of premise")
else if (!isSameSet(bot.left + instantiated, premiseSequent.left + quantified))
- invalid("Left-hand side of conclusion + φ[t/x] must be the same as left-hand side of premise + ∀x. φ")
+ invalid("Left-hand side of conclusion + φ[t/x] is not the same as left-hand side of premise + ∀x. φ")
else
SC.LeftForall(bot, premises(0), phi, x, t)
}
@@ -490,7 +490,7 @@ object BasicStepTactic {
case _ => invalid("Could not infer a universally quantified pivot from premise and conclusion.")
}
else
- invalid("Left-hand side of conclusion + φ[t/x] must be the same as left-hand side of premise + ∀x. φ.")
+ invalid("Left-hand side of conclusion + φ[t/x] is not the same as left-hand side of premise + ∀x. φ.")
else if (instantiatedPivot.isEmpty) Weakening.asSCProof(bot, premises, currentProof)
else if (instantiatedPivot.tail.isEmpty) {
// go through conclusion to find a matching quantified formula
@@ -509,7 +509,7 @@ object BasicStepTactic {
}
}
else
- invalid("Left-hand side of conclusion + φ[t/x] must be the same as left-hand side of premise + ∀x. φ.")
+ invalid("Left-hand side of conclusion + φ[t/x] is not the same as left-hand side of premise + ∀x. φ.")
}
}
@@ -550,9 +550,9 @@ object BasicStepTactic {
else if ((bot.left union bot.right).exists(_.freeVariables.contains(x)))
invalid("The variable x must not be free in the resulting sequent.")
else if (!isSameSet(bot.right, premiseSequent.right))
- invalid("Right-hand side of conclusion must be the same as right-hand side of premise")
+ invalid("Right-hand side of conclusion is not the same as right-hand side of premise")
else if (!isSameSet(bot.left + phi, premiseSequent.left + quantified))
- invalid("Left-hand side of conclusion + φ must be the same as left-hand side of premise + ∃x. φ")
+ invalid("Left-hand side of conclusion + φ is not the same as left-hand side of premise + ∃x. φ")
else
SC.LeftExists(bot, premises(0), phi, x)
}
@@ -588,14 +588,14 @@ object BasicStepTactic {
}
}
else
- invalid("Left-hand side of conclusion + φ must be the same as left-hand side of premise + ∃x. φ.")
+ invalid("Left-hand side of conclusion + φ is not the same as left-hand side of premise + ∃x. φ.")
else if (pivot.tail.isEmpty)
pivot.head match {
case BinderFormula(Exists, x, phi) => LeftExists(phi, x).asSCProof(bot, premises, currentProof)
case _ => invalid("Could not infer an existentially quantified pivot from premise and conclusion.")
}
else
- invalid("Left-hand side of conclusion + φ must be the same as left-hand side of premise + ∃x. φ.")
+ invalid("Left-hand side of conclusion + φ is not the same as left-hand side of premise + ∃x. φ.")
}
}
@@ -631,15 +631,15 @@ object BasicStepTactic {
if (premises.length != 1)
invalid(s"One premise expected, ${premises.length} received.")
else if (!isSameSet(bot.right, premiseSequent.right))
- invalid("Right-hand side of conclusion must be the same as right-hand side of premise.")
+ invalid("Right-hand side of conclusion is not the same as right-hand side of premise.")
else if (!isSameSet(bot.left + instantiated, premiseSequent.left + quantified))
- invalid("Left-hand side of conclusion + ∃y.∀x. (x=y) ↔ φ must be the same as left-hand side of premise + ∃!x. φ.")
+ invalid("Left-hand side of conclusion + ∃y.∀x. (x=y) ↔ φ is not the same as left-hand side of premise + ∃!x. φ.")
else
SC.LeftExistsOne(bot, premises(0), phi, x)
}
}
- case class LeftExistsOneWithoutFormula() extends ProofStepWithoutBotNorPrem(1) {
+ case object LeftExistsOneWithoutFormula extends ProofStepWithoutBotNorPrem(1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
this.asProofStepWithoutBot(premises).asProofStep(bot),
@@ -662,21 +662,21 @@ object BasicStepTactic {
case _ => ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Could not infer an existentially quantified pivot from premise and conclusion.")
}
} else
- invalid("Left-hand side of conclusion + φ must be the same as left-hand side of premise + ∃x. φ.")
+ invalid("Left-hand side of conclusion + φ is not 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 _ => invalid("Could not infer an existentially quantified pivot from premise and conclusion.")
}
else
- invalid("Left-hand side of conclusion + φ must be the same as left-hand side of premise + ∃x. φ.")
+ invalid("Left-hand side of conclusion + φ is not 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()
+ def apply() = LeftExistsOneWithoutFormula
// usage without an argument list
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
@@ -691,25 +691,45 @@ object BasicStepTactic {
* Γ, Σ |- φ∧ψ∧..., Π, Δ
* </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 class RightAnd(conjuncts: Seq[Formula]) extends ProofStepWithoutBotNorPrem(-1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val premiseSequents = premises.map(currentProof.getSequent(_))
+ lazy val conjunction = ConnectorFormula(And, conjuncts)
+
+ if (premises.length == 0)
+ invalid(s"Premises expected, ${premises.length} received.")
+ else if (!isSameSet(bot.left, premiseSequents.map(_.left).reduce(_ union _)))
+ invalid("Left-hand side of conclusion is not the union of the left-hand sides of the premises.")
+ else if (!isSameSet(conjuncts.foldLeft(bot.right)(_ + _), premiseSequents.map(_.right).reduce(_ union _) + conjunction))
+ invalid("Right-hand side of conclusion + conjuncts is not the same as the union of the right-hand sides of the premises + φ∧ψ....")
+ else
+ SC.RightAnd(bot, premises, conjuncts)
+ }
}
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))
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val premiseSequents = premises.map(currentProof.getSequent(_))
+ lazy val pivots = premiseSequents.map(_.right.diff(bot.right))
- if (pivots.exists(_.isEmpty))
- SC.Weakening(bot, premises(pivots.indexWhere(_.isEmpty)))
+ if (premises.length == 0)
+ invalid(s"Premises expected, ${premises.length} received.")
+ else if (pivots.exists(_.isEmpty))
+ Weakening.asSCProof(bot, Seq(premises(pivots.indexWhere(_.isEmpty))), currentProof)
else if (pivots.forall(_.tail.isEmpty))
- SC.RightAnd(bot, premises, pivots.map(_.head))
+ RightAnd(pivots.map(_.head)).asSCProof(bot, premises, currentProof)
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 +φ∧ψ."
- )
+ invalid("Right-hand side of conclusion + φ + ψ is not the same as the union of the right-hand sides of the premises +φ∧ψ.")
}
}
@@ -731,40 +751,64 @@ object BasicStepTactic {
* </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)
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val premiseSequent = currentProof.getSequent(premises(0))
+ lazy val phiAndPsi = ConnectorFormula(Or, Seq(phi, psi))
+
+ if (premises.length != 1)
+ invalid(s"One premise expected, ${premises.length} received.")
+ else if (!isSameSet(bot.left, premiseSequent.left))
+ invalid("Left-hand side of the premise is not the same as the left-hand side of the conclusion.")
+ else if (
+ !isSameSet(bot.right + phi, premiseSequent.right + phiAndPsi) &&
+ !isSameSet(bot.right + psi, premiseSequent.right + phiAndPsi) &&
+ !isSameSet(bot.right + phi + psi, premiseSequent.right + phiAndPsi)
+ )
+ invalid("Right-hand side of premise + φ∧ψ is not the same as right-hand side of conclusion + either φ, ψ or both.")
+ else
+ SC.RightOr(bot, premises(0), phi, psi)
+ }
}
- case class RightOrWithoutFormula() extends ProofStepWithoutBotNorPrem(1) {
+ case object 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)
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val premiseSequent = currentProof.getSequent(premises(0))
+ lazy val pivot = bot.right.diff(premiseSequent.right)
- if (!pivot.isEmpty && pivot.tail.isEmpty)
+ if (premises.length != 1)
+ invalid(s"One premise expected, ${premises.length} received.")
+ else 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)
+ RightOr(phi, psi).asSCProof(bot, premises, currentProof)
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.")
+ RightOr(psi, phi).asSCProof(bot, premises, currentProof)
+ case _ => invalid("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))
+ Rewrite.asSCProof(bot, premises, currentProof)
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."
- )
+ invalid("Right-hand side of conclusion + φ∧ψ is not the 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()
+ def apply() = RightOrWithoutFormula
// usage without an argument list
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
@@ -779,30 +823,53 @@ object BasicStepTactic {
* </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)
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val premiseSequent = currentProof.getSequent(premises(0))
+ lazy val implication = ConnectorFormula(Implies, Seq(phi, psi))
+
+ if (premises.length != 1)
+ invalid(s"One premise expected, ${premises.length} received.")
+ else if (!isSameSet(bot.left + phi, premiseSequent.left))
+ invalid("Left-hand side of conclusion + φ is not the same as left-hand side of premise.")
+ else if (!isSameSet(bot.right + psi, premiseSequent.right + implication))
+ invalid("Right-hand side of conclusion + ψ is not the same as right-hand side of premise + φ→ψ.")
+ else
+ SC.RightImplies(bot, premises(0), phi, psi)
+ }
}
- case class RightImpliesWithoutFormula() extends ProofStepWithoutBotNorPrem(1) {
+ case object 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)
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val premiseSequent = currentProof.getSequent(premises(0))
+ lazy val leftPivot = premiseSequent.left.diff(bot.left)
+ lazy val rightPivot = premiseSequent.right.diff(bot.right)
- if (
+ if (premises.length != 1)
+ invalid(s"One premise expected, ${premises.length} received.")
+ else if (
!leftPivot.isEmpty && leftPivot.tail.isEmpty &&
!rightPivot.isEmpty && rightPivot.tail.isEmpty
)
- SC.RightImplies(bot, premises(0), leftPivot.head, rightPivot.head)
+ RightImplies(leftPivot.head, rightPivot.head).asSCProof(bot, premises, currentProof)
else
- ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Right-hand side of conclusion + ψ must be same as right-hand side of premise + φ→ψ.")
+ invalid("Right-hand side of conclusion + ψ is not the 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()
+ def apply() = RightImpliesWithoutFormula
// usage without an argument list
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
@@ -817,34 +884,57 @@ object BasicStepTactic {
* </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)
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val leftSequent = currentProof.getSequent(premises(0))
+ lazy val rightSequent = currentProof.getSequent(premises(1))
+ lazy val implication = ConnectorFormula(Iff, Seq(phi, psi))
+ lazy val impLeft = ConnectorFormula(Implies, Seq(phi, psi))
+ lazy val impRight = ConnectorFormula(Implies, Seq(psi, phi))
+
+ if (premises.length != 2)
+ invalid(s"Two premises expected, ${premises.length} received.")
+ else if (!isSameSet(bot.left, leftSequent.left union rightSequent.left))
+ invalid("Left-hand side of conclusion is not the union of the left-hand sides of the premises.")
+ else if (!isSameSet(bot.right + impLeft + impRight, leftSequent.right union rightSequent.right + implication))
+ invalid("Right-hand side of conclusion + φ→ψ + ψ→φ is not the same as the union of the right-hand sides of the premises + φ↔ψ.")
+ else
+ SC.RightIff(bot, premises(0), premises(1), phi, psi)
+ }
}
- case class RightIffWithoutFormula() extends ProofStepWithoutBotNorPrem(2) {
+ case object 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)
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
- if (pivot.isEmpty)
- SC.Weakening(bot, premises(0))
+ lazy val premiseSequent = currentProof.getSequent(premises(0))
+ lazy val pivot = premiseSequent.right.diff(bot.right)
+
+ if (premises.length != 2)
+ invalid(s"Two premises expected, ${premises.length} received.")
+ else if (pivot.isEmpty)
+ Weakening.asSCProof(bot, Seq(premises(0)), currentProof)
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.")
+ case ConnectorFormula(Implies, Seq(phi, psi)) => RightIff(phi, psi).asSCProof(bot, premises, currentProof)
+ case _ => invalid("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 φ↔ψ."
- )
+ invalid("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()
+ def apply() = RightIffWithoutFormula
// usage without an argument list
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
@@ -853,27 +943,50 @@ object BasicStepTactic {
/**
* <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)
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val premiseSequent = currentProof.getSequent(premises(0))
+ lazy val negation = ConnectorFormula(Neg, Seq(phi))
+
+ if (premises.length != 1)
+ invalid(s"One premise expected, ${premises.length} received.")
+ else if (!isSameSet(bot.left + phi, premiseSequent.left))
+ invalid("Left-hand side of conclusion + φ must be the same as left-hand side of premise.")
+ else if (!isSameSet(bot.right, premiseSequent.right + negation))
+ invalid("Right-hand side of conclusion must be the same as right-hand side of premise + ¬φ.")
+ else
+ SC.RightNot(bot, premises(0), phi)
+ }
}
- case class RightNotWithoutFormula() extends ProofStepWithoutBotNorPrem(1) {
+ case object 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)
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
- if (pivot.isEmpty)
- SC.Weakening(bot, premises(0))
+ lazy val premiseSequent = currentProof.getSequent(premises(0))
+ lazy val pivot = premiseSequent.left.diff(bot.left)
+
+ if (premises.length != 1)
+ invalid(s"One premise expected, ${premises.length} received.")
+ else if (pivot.isEmpty)
+ Weakening.asSCProof(bot, Seq(premises(0)), currentProof)
else if (pivot.tail.isEmpty)
- SC.RightNot(bot, premises(0), pivot.head)
+ RightNot(pivot.head).asSCProof(bot, premises, currentProof)
else
- ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Left-hand side of conclusion + φ must be the same as left-hand side of premise.")
+ invalid("Left-hand side of conclusion + φ must be the same as left-hand side of premise.")
}
}
@@ -881,7 +994,7 @@ object BasicStepTactic {
case object RightNot extends ProofStepWithoutBotNorPrem(1) {
// default construction:
// def apply(phi: Formula) = new RightNot(phi)
- def apply() = new RightNotWithoutFormula()
+ def apply() = RightNotWithoutFormula
// usage without an argument list
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
@@ -896,18 +1009,43 @@ object BasicStepTactic {
* </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)
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val premiseSequent = currentProof.getSequent(premises(0))
+ lazy val quantified = BinderFormula(Forall, x, phi)
+
+ if (premises.length != 1)
+ invalid(s"One premise expected, ${premises.length} received.")
+ else if ((bot.left union bot.right).exists(_.freeVariables.contains(x)))
+ invalid("The variable x is free in the resulting sequent.")
+ else if (!isSameSet(bot.left, premiseSequent.left))
+ invalid("Left-hand side of conclusion is not the same as left-hand side of premise.")
+ else if (!isSameSet(bot.right + phi, premiseSequent.right + quantified))
+ invalid("Right-hand side of conclusion + φ is not the same as right-hand side of premise + ∀x. φ.")
+ else
+ SC.RightForall(bot, premises(0), phi, x)
+ }
}
- case class RightForallWithoutFormula() extends ProofStepWithoutBotNorPrem(1) {
+ case object 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)
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val premiseSequent = currentProof.getSequent(premises(0))
+ lazy 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))
+ if (premises.length != 1)
+ invalid(s"One premise expected, ${premises.length} received.")
+ else if (pivot.isEmpty)
+ if (instantiatedPivot.isEmpty) Rewrite.asSCProof(bot, Seq(premises(0)), currentProof)
else if (instantiatedPivot.tail.isEmpty) {
val in: Formula = instantiatedPivot.head
val quantifiedPhi: Option[Formula] = bot.right.find(f =>
@@ -918,24 +1056,24 @@ object BasicStepTactic {
)
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.")
+ case Some(BinderFormula(Forall, x, phi)) => RightForall(phi, x).asSCProof(bot, premises, currentProof)
+ case _ => invalid("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 invalid("Right-hand side of conclusion + φ is not 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.")
+ case BinderFormula(Forall, x, phi) => RightForall(phi, x).asSCProof(bot, premises, currentProof)
+ case _ => invalid("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. φ.")
+ invalid("Right-hand side of conclusion + φ is not 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()
+ def apply() = RightForallWithoutFormula
// usage without an argument list
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
@@ -948,32 +1086,52 @@ object BasicStepTactic {
* -------------------
* Γ |- ∃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)
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val premiseSequent = currentProof.getSequent(premises(0))
+ lazy val quantified = BinderFormula(Exists, x, phi)
+ lazy val instantiated = substituteVariables(phi, Map(x -> t))
+
+ if (premises.length != 1)
+ invalid(s"One premise expected, ${premises.length} received.")
+ else if (!isSameSet(bot.left, premiseSequent.left))
+ invalid("Left-hand side of conclusion is not the same as left-hand side of premise")
+ else if (!isSameSet(bot.right + instantiated, premiseSequent.right + quantified))
+ invalid("Right-hand side of conclusion + φ[t/x] is not the same as right-hand side of premise + ∃x. φ")
+ else
+ 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)
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val premiseSequent = currentProof.getSequent(premises(0))
+ lazy val pivot = bot.right.diff(premiseSequent.right)
lazy val instantiatedPivot = premiseSequent.right.diff(bot.right)
- if (!pivot.isEmpty)
+ if (premises.length != 1)
+ invalid(s"One premise expected, ${premises.length} received.")
+ else 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.")
+ case BinderFormula(Exists, x, phi) => RightExists(phi, x, t).asSCProof(bot, premises, currentProof)
+ case _ => invalid("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))
+ invalid("Right-hand side of conclusion + φ[t/x] is not the same as right-hand side of premise + ∀x. φ.")
+ else if (instantiatedPivot.isEmpty) Weakening.asSCProof(bot, premises, currentProof)
else if (instantiatedPivot.tail.isEmpty) {
// go through conclusion to find a matching quantified formula
@@ -986,14 +1144,11 @@ object BasicStepTactic {
)
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.")
+ case Some(BinderFormula(Exists, x, phi)) => RightExists(phi, x, t).asSCProof(bot, premises, currentProof)
+ case _ => invalid("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. φ."
- )
+ invalid("Right-hand side of conclusion + φ[t/x] is not the same as right-hand side of premise + ∀x. φ.")
}
}
@@ -1019,41 +1174,66 @@ object BasicStepTactic {
* </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)
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val premiseSequent = currentProof.getSequent(premises(0))
+ lazy val y = VariableLabel(freshId(phi.freeVariables.map(_.id) + x.id, "y"))
+ lazy val instantiated = BinderFormula(Exists, y, BinderFormula(Forall, x, ConnectorFormula(Iff, List(PredicateFormula(equality, List(VariableTerm(x), VariableTerm(y))), phi))))
+ lazy val quantified = BinderFormula(ExistsOne, x, phi)
+
+ if (premises.length != 1)
+ invalid(s"One premise expected, ${premises.length} received.")
+ else if (!isSameSet(bot.left, premiseSequent.left))
+ invalid("Left-hand side of conclusion is not the same as left-hand side of premise.")
+ else if (!isSameSet(bot.right + instantiated, premiseSequent.right + quantified))
+ invalid("Right-hand side of conclusion + ∃y.∀x. (x=y) ↔ φ is not the same as right-hand side of premise + ∃!x. φ.")
+ else
+ SC.RightExistsOne(bot, premises(0), phi, x)
+ }
}
- case class RightExistsOneWithoutFormula() extends ProofStepWithoutBotNorPrem(1) {
+ case object 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)
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val premiseSequent = currentProof.getSequent(premises(0))
+ lazy val pivot = bot.right.diff(premiseSequent.right)
lazy val instantiatedPivot = premiseSequent.right.diff(bot.right)
- if (pivot.isEmpty)
+ if (premises.length != 1)
+ invalid(s"One premise expected, ${premises.length} received.")
+ else if (pivot.isEmpty)
if (instantiatedPivot.isEmpty)
- SC.Rewrite(bot, premises(0))
+ Rewrite.asSCProof(bot, premises, currentProof)
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.")
+ case BinderFormula(Exists, _, BinderFormula(Forall, x, ConnectorFormula(Iff, Seq(_, phi)))) => RightExistsOne(phi, x).asSCProof(bot, premises, currentProof)
+ case _ => invalid("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. φ.")
+ invalid("Right-hand side of conclusion + φ is not 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.")
+ case BinderFormula(ExistsOne, x, phi) => RightExistsOne(phi, x).asSCProof(bot, premises, currentProof)
+ case _ => invalid("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. φ.")
+ invalid("Right-hand side of conclusion + φ is not 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()
+ def apply() = RightExistsOneWithoutFormula
// usage without an argument list
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
@@ -1069,8 +1249,23 @@ object BasicStepTactic {
* </pre>
*/
case object Weakening extends ProofStepWithoutBotNorPrem(1) {
- def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
- SC.Weakening(bot, premises(0))
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val premiseSequent = currentProof.getSequent(premises(0))
+
+ if (premises.length != 1)
+ invalid(s"One premise expected, ${premises.length} received.")
+ else if (!isSubset(premiseSequent.left, bot.left))
+ invalid("Left-hand side of conclusion is not the same as left-hand side of premise.")
+ else if (!isSubset(premiseSequent.right, bot.right))
+ invalid("Left-hand side of premise is not a subset of left-hand side of conclusion.")
+ else
+ SC.Weakening(bot, premises(0))
+ }
}
// Equality Rules
@@ -1081,20 +1276,56 @@ object BasicStepTactic {
* Γ |- Δ
* </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 LeftRefl(phi: Formula) extends ProofStepWithoutBotNorPrem(1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val premiseSequent = currentProof.getSequent(premises(0))
+
+ if (premises.length != 1)
+ invalid(s"One premise expected, ${premises.length} received.")
+ else if (!isSameSet(bot.left + phi, premiseSequent.left))
+ invalid("Left-hand sides of the conclusion + φ is not the same as left-hand side of the premise.")
+ else if (!isSameSet(bot.right, premiseSequent.right))
+ invalid("Right-hand side of the premise is not the same as the right-hand side of the conclusion.")
+ else
+ phi match {
+ case PredicateFormula(`equality`, Seq(left, right)) =>
+ if (isSame(left, right))
+ SC.LeftRefl(bot, premises(0), phi)
+ else
+ invalid("φ is not an instance of reflexivity.")
+ case _ => invalid("φ is not an equality.")
+ }
+ }
}
- case class LeftReflWithoutFormula() extends ProofStepWithoutBotNorPrem(1) {
- def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
- SC.Rewrite(bot, premises(0))
+ case object LeftReflWithoutFormula extends ProofStepWithoutBotNorPrem(1) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val premiseSequent = currentProof.getSequent(premises(0))
+ lazy val pivot = premiseSequent.left.diff(bot.left)
+
+ if (premises.length != 1)
+ invalid(s"One premise expected, ${premises.length} received.")
+ else if(!pivot.isEmpty && pivot.tail.isEmpty)
+ LeftRefl(pivot.head).asSCProof(bot, premises, currentProof)
+ else
+ invalid("Could not infer an equality as pivot from premise and conclusion.")
+ }
}
case object LeftRefl extends ProofStepWithoutBotNorPrem(1) {
// default construction:
// def apply(fa: Formula) = new LeftRefl(fa)
- def apply() = new LeftReflWithoutFormula()
+ def apply() = LeftReflWithoutFormula
// usage without an argument list
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
@@ -1108,20 +1339,63 @@ object BasicStepTactic {
* |- 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 RightRefl(phi: Formula) extends ProofStepWithoutBotNorPrem(0) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ if (premises.length != 0)
+ invalid(s"No premises expected, ${premises.length} received.")
+ else if (!contains(bot.right, phi))
+ invalid("Right-hand side of conclusion does not contain φ.")
+ else
+ phi match {
+ case PredicateFormula(`equality`, Seq(left, right)) =>
+ if (isSame(left, right))
+ SC.RightRefl(bot, phi)
+ else
+ invalid("φ is not an instance of reflexivity.")
+ case _ => invalid("φ is not an equality.")
+ }
+ }
}
- case class RightReflWithoutFormula() extends ProofStepWithoutBotNorPrem(0) {
- def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
- SC.RewriteTrue(bot)
+ case object RightReflWithoutFormula extends ProofStepWithoutBotNorPrem(0) {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ if (premises.length != 0)
+ invalid(s"No premises expected, ${premises.length} received.")
+ else if(bot.right.isEmpty)
+ invalid("Right-hand side of conclusion does not contain an instance of reflexivity.")
+ else {
+ // go through conclusion to see if you can find an reflexive formula
+ val pivot: Option[Formula] = bot.right.find(f =>
+ f match {
+ case PredicateFormula(`equality`, Seq(l, r)) => isSame(l, r)
+ case _ => false
+ }
+ )
+
+ pivot match {
+ case Some(phi) => RightRefl(phi).asSCProof(bot, premises, currentProof)
+ case _ => invalid("Could not infer an equality as pivot from conclusion.")
+ }
+
+ }
+
+ }
}
case object RightRefl extends ProofStepWithoutBotNorPrem(0) {
// default construction:
// def apply(fa: Formula) = new RightRefl(fa)
- def apply() = new RightReflWithoutFormula()
+ def apply() = RightReflWithoutFormula
// usage without an argument list
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
--
GitLab
From 9b873594e1c8a59095b46c056223dc8e0ebf9023 Mon Sep 17 00:00:00 2001
From: Sankalp Gambhir <sankalp.gambhir47@gmail.com>
Date: Wed, 2 Nov 2022 12:44:01 +0100
Subject: [PATCH 4/6] Proof checking for substitution rules
---
.../lisa/utils/tactics/BasicStepTactic.scala | 104 ++++++++++++++++--
1 file changed, 96 insertions(+), 8 deletions(-)
diff --git a/lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala b/lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala
index c1702bef..9fd096e3 100644
--- a/lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala
@@ -1410,8 +1410,30 @@ object BasicStepTactic {
* </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)
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val premiseSequent = currentProof.getSequent(premises(0))
+ lazy val (s_es, t_es) = equals.unzip
+ lazy val phi_s = lambdaPhi(s_es)
+ lazy val phi_t = lambdaPhi(t_es)
+ lazy val equalities = equals map { case (s, t) => PredicateFormula(equality, Seq(s, t)) }
+
+ if (premises.length != 1)
+ invalid(s"One premise expected, ${premises.length} received.")
+ else if (!isSameSet(bot.right, premiseSequent.right))
+ invalid("Right-hand side of the premise is not the same as the right-hand side of the conclusion.")
+ else if (
+ !isSameSet(bot.left + phi_s, premiseSequent.left ++ equalities + phi_t) &&
+ !isSameSet(bot.left + phi_t, premiseSequent.left ++ equalities + phi_s)
+ )
+ invalid("Left-hand side of the conclusion + φ(s_) is not the same as left-hand side of the premise + (s=t)_ + φ(t_) (or with s_ and t_ swapped).")
+ else
+ SC.LeftSubstEq(bot, premises(0), equals, lambdaPhi)
+ }
}
/**
@@ -1422,8 +1444,30 @@ object BasicStepTactic {
* </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)
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val premiseSequent = currentProof.getSequent(premises(0))
+ lazy val (s_es, t_es) = equals.unzip
+ lazy val phi_s = lambdaPhi(s_es)
+ lazy val phi_t = lambdaPhi(t_es)
+ lazy val equalities = equals map { case (s, t) => PredicateFormula(equality, Seq(s, t)) }
+
+ if (premises.length != 1)
+ invalid(s"One premise expected, ${premises.length} received.")
+ else if (!isSameSet(bot.left, premiseSequent.left ++ equalities))
+ invalid("Left-hand side of the conclusion is not the same as the left-hand side of the premise + (s=t)_.")
+ else if (
+ !isSameSet(bot.left + phi_s, premiseSequent.left + phi_t) &&
+ !isSameSet(bot.left + phi_t, premiseSequent.left + phi_s)
+ )
+ invalid("Right-hand side of the conclusion + φ(s_) is not the same as right-hand side of the premise + φ(t_) (or with s_ and t_ swapped).")
+ else
+ SC.RightSubstEq(bot, premises(0), equals, lambdaPhi)
+ }
}
/**
@@ -1434,8 +1478,30 @@ object BasicStepTactic {
* </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)
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val premiseSequent = currentProof.getSequent(premises(0))
+ lazy val (psi_es, tau_es) = equals.unzip
+ lazy val phi_psi = lambdaPhi(psi_es)
+ lazy val phi_tau = lambdaPhi(tau_es)
+ lazy val implications = equals map { case (s, t) => ConnectorFormula(Iff, Seq(s, t)) }
+
+ if (premises.length != 1)
+ invalid(s"One premise expected, ${premises.length} received.")
+ else if (!isSameSet(bot.right, premiseSequent.right))
+ invalid("Right-hand side of the premise is not the same as the right-hand side of the conclusion.")
+ else if (
+ !isSameSet(bot.left + phi_psi, premiseSequent.left ++ implications + phi_tau) &&
+ !isSameSet(bot.left + phi_tau, premiseSequent.left ++ implications + phi_psi)
+ )
+ invalid("Left-hand side of the conclusion + φ(ψ_) is not the same as left-hand side of the premise + (ψ ↔ τ)_ + φ(τ_) (or with ψ_ and τ_ swapped).")
+ else
+ SC.LeftSubstIff(bot, premises(0), equals, lambdaPhi)
+ }
}
/**
@@ -1446,8 +1512,30 @@ object BasicStepTactic {
* </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)
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val premiseSequent = currentProof.getSequent(premises(0))
+ lazy val (psi_es, tau_es) = equals.unzip
+ lazy val phi_psi = lambdaPhi(psi_es)
+ lazy val phi_tau = lambdaPhi(tau_es)
+ lazy val implications = equals map { case (s, t) => ConnectorFormula(Iff, Seq(s, t)) }
+
+ if (premises.length != 1)
+ invalid(s"One premise expected, ${premises.length} received.")
+ else if (!isSameSet(bot.left, premiseSequent.left ++ implications))
+ invalid("Left-hand side of the conclusion is not the same as the left-hand side of the premise + (ψ ↔ τ)_.")
+ else if (
+ !isSameSet(bot.left + phi_psi, premiseSequent.left + phi_tau) &&
+ !isSameSet(bot.left + phi_tau, premiseSequent.left + phi_psi)
+ )
+ invalid("Right-hand side of the conclusion + φ(ψ_) is not the same as right-hand side of the premise + φ(τ_) (or with ψ_ and τ_ swapped).")
+ else
+ SC.RightSubstIff(bot, premises(0), equals, lambdaPhi)
+ }
}
/**
--
GitLab
From 3295ca673bfb88f481f0b89f34169662bef802cf Mon Sep 17 00:00:00 2001
From: Sankalp Gambhir <sankalp.gambhir47@gmail.com>
Date: Wed, 2 Nov 2022 15:08:23 +0100
Subject: [PATCH 5/6] Checking for abstracted instantiation steps
---
.../lisa/utils/tactics/BasicStepTactic.scala | 66 +++++++++++++++----
1 file changed, 54 insertions(+), 12 deletions(-)
diff --git a/lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala b/lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala
index 9fd096e3..b66cea87 100644
--- a/lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala
@@ -961,16 +961,16 @@ object BasicStepTactic {
if (premises.length != 1)
invalid(s"One premise expected, ${premises.length} received.")
else if (!isSameSet(bot.left + phi, premiseSequent.left))
- invalid("Left-hand side of conclusion + φ must be the same as left-hand side of premise.")
+ invalid("Left-hand side of conclusion + φ is not the same as left-hand side of premise.")
else if (!isSameSet(bot.right, premiseSequent.right + negation))
- invalid("Right-hand side of conclusion must be the same as right-hand side of premise + ¬φ.")
+ invalid("Right-hand side of conclusion is not the same as right-hand side of premise + ¬φ.")
else
SC.RightNot(bot, premises(0), phi)
}
}
case object RightNotWithoutFormula extends ProofStepWithoutBotNorPrem(1) {
- def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
this.asProofStepWithoutBot(premises).asProofStep(bot),
msg
@@ -986,7 +986,7 @@ object BasicStepTactic {
else if (pivot.tail.isEmpty)
RightNot(pivot.head).asSCProof(bot, premises, currentProof)
else
- invalid("Left-hand side of conclusion + φ must be the same as left-hand side of premise.")
+ invalid("Left-hand side of conclusion + φ is not the same as left-hand side of premise.")
}
}
@@ -1546,8 +1546,23 @@ object BasicStepTactic {
* </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)
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val premiseSequent = currentProof.getSequent(premises(0))
+
+ if (premises.length != 1)
+ invalid(s"One premise expected, ${premises.length} received.")
+ else if (!isSameSet(bot.left, premiseSequent.left.map(instantiateTermSchemas(_, insts))))
+ invalid("Left-hand side of premise instantiated with the map 'insts' is not the same as left-hand side of conclusion.")
+ else if (!isSameSet(bot.right, premiseSequent.right.map(instantiateTermSchemas(_, insts))))
+ invalid("Right-hand side of premise instantiated with the map 'insts' is not the same as right-hand side of conclusion.")
+ else
+ SC.InstFunSchema(bot, premises(0), insts)
+ }
}
/**
@@ -1558,16 +1573,43 @@ object BasicStepTactic {
* </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)
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
+ lazy val premiseSequent = currentProof.getSequent(premises(0))
+
+ if (premises.length != 1)
+ invalid(s"One premise expected, ${premises.length} received.")
+ else if (!isSameSet(bot.left, premiseSequent.left.map(instantiatePredicateSchemas(_, insts))))
+ invalid("Left-hand side of premise instantiated with the map 'insts' is not the same as left-hand side of conclusion.")
+ else if (!isSameSet(bot.right, premiseSequent.right.map(instantiatePredicateSchemas(_, insts))))
+ invalid("Right-hand side of premise instantiated with the map 'insts' is not the same as right-hand side of conclusion.")
+ else
+ 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)
- }
+ def asSCProof(currentProof: Library#Proof): ProofStepJudgement = {
+ def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+ this,
+ msg
+ )
+
+ lazy val premiseSequents = premises.map(currentProof.getSequent(_))
+ lazy val invalidPremise = premises.zipWithIndex.find( (no, p) => !SC.isSameSequent(premiseSequents(no), sp.imports(p)))
+
+ if (premises.length != sp.imports.length)
+ invalid(s"Subproof expected ${sp.imports.length} premises, ${premises.length} received.")
+ else if (!invalidPremise.isEmpty)
+ invalid(s"Premise number ${invalidPremise.get._1} (refering to step ${invalidPremise.get}) is not the same as import number ${invalidPremise.get._1} of the subproof.")
+ else
+ SC.SCSubproof(sp, premises)
+ }
}
}
--
GitLab
From 5149ae2a85d688bba20f2d26e6370c22e2232e32 Mon Sep 17 00:00:00 2001
From: Sankalp Gambhir <sankalp.gambhir47@gmail.com>
Date: Wed, 2 Nov 2022 15:10:56 +0100
Subject: [PATCH 6/6] scalafmt
---
.../lisa/utils/tactics/BasicStepTactic.scala | 396 +++++++++---------
1 file changed, 192 insertions(+), 204 deletions(-)
diff --git a/lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala b/lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala
index b66cea87..23e9e616 100644
--- a/lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala
@@ -14,9 +14,9 @@ object BasicStepTactic {
case object Hypothesis extends ProofStepWithoutBotNorPrem(0) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val intersectedPivot = bot.left.intersect(bot.right)
@@ -32,10 +32,10 @@ object BasicStepTactic {
case object Rewrite extends ProofStepWithoutBotNorPrem(1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
-
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
if (premises.length != 1)
invalid(s"One premise expected, ${premises.length} received.")
else if (!SC.isSameSequent(bot, currentProof.getSequent(premises(0))))
@@ -55,9 +55,9 @@ object BasicStepTactic {
case class Cut(phi: Formula) extends ProofStepWithoutBotNorPrem(2) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val leftSequent = currentProof.getSequent(premises(0))
lazy val rightSequent = currentProof.getSequent(premises(1))
@@ -80,9 +80,9 @@ object BasicStepTactic {
case object CutWithoutFormula extends ProofStepWithoutBotNorPrem(2) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val leftSequent = currentProof.getSequent(premises(0))
lazy val rightSequent = currentProof.getSequent(premises(1))
@@ -126,9 +126,9 @@ object BasicStepTactic {
case class LeftAnd(phi: Formula, psi: Formula) extends ProofStepWithoutBotNorPrem(1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val premiseSequent = currentProof.getSequent(premises(0))
lazy val phiAndPsi = ConnectorFormula(And, Seq(phi, psi))
@@ -151,10 +151,10 @@ object BasicStepTactic {
case object LeftAndWithoutFormula extends ProofStepWithoutBotNorPrem(1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
-
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
+
lazy val premiseSequent = currentProof.getSequent(premises(0))
lazy val pivot = bot.left.diff(premiseSequent.left)
@@ -170,11 +170,11 @@ object BasicStepTactic {
case _ => invalid("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))
- Rewrite.asSCProof(bot, premises, currentProof)
- else
- invalid("Left-hand side of premise + φ∧ψ is not the same as left-hand side of conclusion + either φ, ψ or both.")
+ // try a rewrite, if it works, go ahead with it, otherwise malformed
+ if (SC.isSameSequent(premiseSequent, bot))
+ Rewrite.asSCProof(bot, premises, currentProof)
+ else
+ invalid("Left-hand side of premise + φ∧ψ is not the same as left-hand side of conclusion + either φ, ψ or both.")
}
}
@@ -198,13 +198,12 @@ object BasicStepTactic {
case class LeftOr(disjuncts: Seq[Formula]) extends ProofStepWithoutBotNorPrem(-1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val premiseSequents = premises.map(currentProof.getSequent(_))
lazy val disjunction = ConnectorFormula(Or, disjuncts)
-
if (premises.length == 0)
invalid(s"Premises expected, ${premises.length} received.")
@@ -219,9 +218,9 @@ object BasicStepTactic {
case object LeftOrWithoutFormula extends ProofStepWithoutBotNorPrem(-1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val premiseSequents = premises.map(currentProof.getSequent(_))
lazy val pivots = premiseSequents.map(_.left.diff(bot.left))
@@ -258,14 +257,13 @@ object BasicStepTactic {
case class LeftImplies(phi: Formula, psi: Formula) extends ProofStepWithoutBotNorPrem(2) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val leftSequent = currentProof.getSequent(premises(0))
lazy val rightSequent = currentProof.getSequent(premises(1))
lazy val implication = ConnectorFormula(Implies, Seq(phi, psi))
-
if (premises.length != 2)
invalid(s"Two premises expected, ${premises.length} received.")
@@ -281,9 +279,9 @@ object BasicStepTactic {
case object LeftImpliesWithoutFormula extends ProofStepWithoutBotNorPrem(2) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val leftSequent = currentProof.getSequent(premises(0))
lazy val rightSequent = currentProof.getSequent(premises(1))
@@ -323,25 +321,24 @@ object BasicStepTactic {
case class LeftIff(phi: Formula, psi: Formula) extends ProofStepWithoutBotNorPrem(1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val premiseSequent = currentProof.getSequent(premises(0))
lazy val implication = ConnectorFormula(Iff, Seq(phi, psi))
lazy val impLeft = ConnectorFormula(Implies, Seq(phi, psi))
lazy val impRight = ConnectorFormula(Implies, Seq(psi, phi))
-
if (premises.length != 1)
invalid(s"One premise expected, ${premises.length} received.")
else if (!isSameSet(bot.right, premiseSequent.right))
invalid("Right-hand side of premise is not the same as right-hand side of conclusion.")
else if (
- !isSameSet(bot.left + impLeft, premiseSequent.left + implication) &&
- !isSameSet(bot.left + impRight, premiseSequent.left + implication) &&
- !isSameSet(bot.left + impLeft + impRight, premiseSequent.left + implication)
- )
+ !isSameSet(bot.left + impLeft, premiseSequent.left + implication) &&
+ !isSameSet(bot.left + impRight, premiseSequent.left + implication) &&
+ !isSameSet(bot.left + impLeft + impRight, premiseSequent.left + implication)
+ )
invalid("Left-hand side of premise + φ↔ψ is not the same as left-hand side of conclusion + either φ→ψ, ψ→φ or both.")
else
SC.LeftIff(bot, premises(0), phi, psi)
@@ -351,9 +348,9 @@ object BasicStepTactic {
case object LeftIffWithoutFormula extends ProofStepWithoutBotNorPrem(1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val premiseSequent = currentProof.getSequent(premises(0))
lazy val pivot = premiseSequent.left.diff(bot.left)
@@ -390,13 +387,13 @@ object BasicStepTactic {
case class LeftNot(phi: Formula) extends ProofStepWithoutBotNorPrem(1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val premiseSequent = currentProof.getSequent(premises(0))
lazy val negation = ConnectorFormula(Neg, Seq(phi))
-
+
if (premises.length != 1)
invalid(s"One premise expected, ${premises.length} received.")
else if (!isSameSet(bot.right + phi, premiseSequent.right))
@@ -411,9 +408,9 @@ object BasicStepTactic {
case object LeftNotWithoutFormula extends ProofStepWithoutBotNorPrem(1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val premiseSequent = currentProof.getSequent(premises(0))
lazy val pivot = premiseSequent.right.diff(bot.right)
@@ -451,14 +448,14 @@ object BasicStepTactic {
case class LeftForall(phi: Formula, x: VariableLabel, t: Term) extends ProofStepWithoutBotNorPrem(1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val premiseSequent = currentProof.getSequent(premises(0))
lazy val quantified = BinderFormula(Forall, x, phi)
lazy val instantiated = substituteVariables(phi, Map(x -> t))
-
+
if (premises.length != 1)
invalid(s"One premise expected, ${premises.length} received.")
else if (!isSameSet(bot.right, premiseSequent.right))
@@ -473,16 +470,15 @@ object BasicStepTactic {
case class LeftForallWithoutFormula(t: Term) extends ProofStepWithoutBotNorPrem(1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val premiseSequent = currentProof.getSequent(premises(0))
lazy val pivot = bot.left.diff(premiseSequent.left)
lazy val instantiatedPivot = premiseSequent.left.diff(bot.left)
- if (premises.length != 1)
- invalid(s"One premise expected, ${premises.length} received.")
+ if (premises.length != 1) invalid(s"One premise expected, ${premises.length} received.")
else if (!pivot.isEmpty)
if (pivot.tail.isEmpty)
pivot.head match {
@@ -507,9 +503,7 @@ object BasicStepTactic {
case Some(BinderFormula(Forall, x, phi)) => LeftForall(phi, x, t).asSCProof(bot, premises, currentProof)
case _ => invalid("Could not infer a universally quantified pivot from premise and conclusion.")
}
- }
- else
- invalid("Left-hand side of conclusion + φ[t/x] is not the same as left-hand side of premise + ∀x. φ.")
+ } else invalid("Left-hand side of conclusion + φ[t/x] is not the same as left-hand side of premise + ∀x. φ.")
}
}
@@ -538,13 +532,13 @@ object BasicStepTactic {
case class LeftExists(phi: Formula, x: VariableLabel) extends ProofStepWithoutBotNorPrem(1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val premiseSequent = currentProof.getSequent(premises(0))
lazy val quantified = BinderFormula(Exists, x, phi)
-
+
if (premises.length != 1)
invalid(s"One premise expected, ${premises.length} received.")
else if ((bot.left union bot.right).exists(_.freeVariables.contains(x)))
@@ -561,9 +555,9 @@ object BasicStepTactic {
case object LeftExistsWithoutFormula extends ProofStepWithoutBotNorPrem(1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val premiseSequent = currentProof.getSequent(premises(0))
lazy val pivot = bot.left.diff(premiseSequent.left)
@@ -586,9 +580,7 @@ object BasicStepTactic {
case Some(BinderFormula(Exists, x, phi)) => LeftExists(phi, x).asSCProof(bot, premises, currentProof)
case _ => invalid("Could not infer an existensially quantified pivot from premise and conclusion.")
}
- }
- else
- invalid("Left-hand side of conclusion + φ is not the same as left-hand side of premise + ∃x. φ.")
+ } else invalid("Left-hand side of conclusion + φ is not the same as left-hand side of premise + ∃x. φ.")
else if (pivot.tail.isEmpty)
pivot.head match {
case BinderFormula(Exists, x, phi) => LeftExists(phi, x).asSCProof(bot, premises, currentProof)
@@ -619,9 +611,9 @@ object BasicStepTactic {
case class LeftExistsOne(phi: Formula, x: VariableLabel) extends ProofStepWithoutBotNorPrem(1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val premiseSequent = currentProof.getSequent(premises(0))
lazy val y = VariableLabel(freshId(phi.freeVariables.map(_.id) + x.id, "y"))
@@ -642,9 +634,9 @@ object BasicStepTactic {
case object LeftExistsOneWithoutFormula extends ProofStepWithoutBotNorPrem(1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val premiseSequent = currentProof.getSequent(premises(0))
lazy val pivot = bot.left.diff(premiseSequent.left)
@@ -694,9 +686,9 @@ object BasicStepTactic {
case class RightAnd(conjuncts: Seq[Formula]) extends ProofStepWithoutBotNorPrem(-1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val premiseSequents = premises.map(currentProof.getSequent(_))
lazy val conjunction = ConnectorFormula(And, conjuncts)
@@ -714,9 +706,9 @@ object BasicStepTactic {
case object RightAndWithoutFormula extends ProofStepWithoutBotNorPrem(-1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val premiseSequents = premises.map(currentProof.getSequent(_))
lazy val pivots = premiseSequents.map(_.right.diff(bot.right))
@@ -753,9 +745,9 @@ object BasicStepTactic {
case class RightOr(phi: Formula, psi: Formula) extends ProofStepWithoutBotNorPrem(1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val premiseSequent = currentProof.getSequent(premises(0))
lazy val phiAndPsi = ConnectorFormula(Or, Seq(phi, psi))
@@ -778,9 +770,9 @@ object BasicStepTactic {
case object RightOrWithoutFormula extends ProofStepWithoutBotNorPrem(1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val premiseSequent = currentProof.getSequent(premises(0))
lazy val pivot = bot.right.diff(premiseSequent.right)
@@ -825,13 +817,13 @@ object BasicStepTactic {
case class RightImplies(phi: Formula, psi: Formula) extends ProofStepWithoutBotNorPrem(1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val premiseSequent = currentProof.getSequent(premises(0))
lazy val implication = ConnectorFormula(Implies, Seq(phi, psi))
-
+
if (premises.length != 1)
invalid(s"One premise expected, ${premises.length} received.")
else if (!isSameSet(bot.left + phi, premiseSequent.left))
@@ -846,9 +838,9 @@ object BasicStepTactic {
case object RightImpliesWithoutFormula extends ProofStepWithoutBotNorPrem(1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val premiseSequent = currentProof.getSequent(premises(0))
lazy val leftPivot = premiseSequent.left.diff(bot.left)
@@ -886,16 +878,16 @@ object BasicStepTactic {
case class RightIff(phi: Formula, psi: Formula) extends ProofStepWithoutBotNorPrem(2) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val leftSequent = currentProof.getSequent(premises(0))
lazy val rightSequent = currentProof.getSequent(premises(1))
lazy val implication = ConnectorFormula(Iff, Seq(phi, psi))
lazy val impLeft = ConnectorFormula(Implies, Seq(phi, psi))
lazy val impRight = ConnectorFormula(Implies, Seq(psi, phi))
-
+
if (premises.length != 2)
invalid(s"Two premises expected, ${premises.length} received.")
else if (!isSameSet(bot.left, leftSequent.left union rightSequent.left))
@@ -910,9 +902,9 @@ object BasicStepTactic {
case object RightIffWithoutFormula extends ProofStepWithoutBotNorPrem(2) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val premiseSequent = currentProof.getSequent(premises(0))
lazy val pivot = premiseSequent.right.diff(bot.right)
@@ -951,13 +943,13 @@ object BasicStepTactic {
case class RightNot(phi: Formula) extends ProofStepWithoutBotNorPrem(1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val premiseSequent = currentProof.getSequent(premises(0))
lazy val negation = ConnectorFormula(Neg, Seq(phi))
-
+
if (premises.length != 1)
invalid(s"One premise expected, ${premises.length} received.")
else if (!isSameSet(bot.left + phi, premiseSequent.left))
@@ -970,11 +962,11 @@ object BasicStepTactic {
}
case object RightNotWithoutFormula extends ProofStepWithoutBotNorPrem(1) {
- def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+ def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val premiseSequent = currentProof.getSequent(premises(0))
lazy val pivot = premiseSequent.left.diff(bot.left)
@@ -1011,13 +1003,13 @@ object BasicStepTactic {
case class RightForall(phi: Formula, x: VariableLabel) extends ProofStepWithoutBotNorPrem(1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val premiseSequent = currentProof.getSequent(premises(0))
lazy val quantified = BinderFormula(Forall, x, phi)
-
+
if (premises.length != 1)
invalid(s"One premise expected, ${premises.length} received.")
else if ((bot.left union bot.right).exists(_.freeVariables.contains(x)))
@@ -1034,9 +1026,9 @@ object BasicStepTactic {
case object RightForallWithoutFormula extends ProofStepWithoutBotNorPrem(1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val premiseSequent = currentProof.getSequent(premises(0))
lazy val pivot = bot.right.diff(premiseSequent.right)
@@ -1091,14 +1083,14 @@ object BasicStepTactic {
case class RightExists(phi: Formula, x: VariableLabel, t: Term) extends ProofStepWithoutBotNorPrem(1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val premiseSequent = currentProof.getSequent(premises(0))
lazy val quantified = BinderFormula(Exists, x, phi)
lazy val instantiated = substituteVariables(phi, Map(x -> t))
-
+
if (premises.length != 1)
invalid(s"One premise expected, ${premises.length} received.")
else if (!isSameSet(bot.left, premiseSequent.left))
@@ -1113,16 +1105,15 @@ object BasicStepTactic {
case class RightExistsWithoutFormula(t: Term) extends ProofStepWithoutBotNorPrem(1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val premiseSequent = currentProof.getSequent(premises(0))
lazy val pivot = bot.right.diff(premiseSequent.right)
lazy val instantiatedPivot = premiseSequent.right.diff(bot.right)
- if (premises.length != 1)
- invalid(s"One premise expected, ${premises.length} received.")
+ if (premises.length != 1) invalid(s"One premise expected, ${premises.length} received.")
else if (!pivot.isEmpty)
if (pivot.tail.isEmpty)
pivot.head match {
@@ -1147,8 +1138,7 @@ object BasicStepTactic {
case Some(BinderFormula(Exists, x, phi)) => RightExists(phi, x, t).asSCProof(bot, premises, currentProof)
case _ => invalid("Could not infer an existentially quantified pivot from premise and conclusion.")
}
- } else
- invalid("Right-hand side of conclusion + φ[t/x] is not the same as right-hand side of premise + ∀x. φ.")
+ } else invalid("Right-hand side of conclusion + φ[t/x] is not the same as right-hand side of premise + ∀x. φ.")
}
}
@@ -1176,9 +1166,9 @@ object BasicStepTactic {
case class RightExistsOne(phi: Formula, x: VariableLabel) extends ProofStepWithoutBotNorPrem(1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val premiseSequent = currentProof.getSequent(premises(0))
lazy val y = VariableLabel(freshId(phi.freeVariables.map(_.id) + x.id, "y"))
@@ -1199,9 +1189,9 @@ object BasicStepTactic {
case object RightExistsOneWithoutFormula extends ProofStepWithoutBotNorPrem(1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val premiseSequent = currentProof.getSequent(premises(0))
lazy val pivot = bot.right.diff(premiseSequent.right)
@@ -1251,9 +1241,9 @@ object BasicStepTactic {
case object Weakening extends ProofStepWithoutBotNorPrem(1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val premiseSequent = currentProof.getSequent(premises(0))
@@ -1279,9 +1269,9 @@ object BasicStepTactic {
case class LeftRefl(phi: Formula) extends ProofStepWithoutBotNorPrem(1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val premiseSequent = currentProof.getSequent(premises(0))
@@ -1293,10 +1283,10 @@ object BasicStepTactic {
invalid("Right-hand side of the premise is not the same as the right-hand side of the conclusion.")
else
phi match {
- case PredicateFormula(`equality`, Seq(left, right)) =>
- if (isSame(left, right))
+ case PredicateFormula(`equality`, Seq(left, right)) =>
+ if (isSame(left, right))
SC.LeftRefl(bot, premises(0), phi)
- else
+ else
invalid("φ is not an instance of reflexivity.")
case _ => invalid("φ is not an equality.")
}
@@ -1306,16 +1296,16 @@ object BasicStepTactic {
case object LeftReflWithoutFormula extends ProofStepWithoutBotNorPrem(1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val premiseSequent = currentProof.getSequent(premises(0))
lazy val pivot = premiseSequent.left.diff(bot.left)
if (premises.length != 1)
invalid(s"One premise expected, ${premises.length} received.")
- else if(!pivot.isEmpty && pivot.tail.isEmpty)
+ else if (!pivot.isEmpty && pivot.tail.isEmpty)
LeftRefl(pivot.head).asSCProof(bot, premises, currentProof)
else
invalid("Could not infer an equality as pivot from premise and conclusion.")
@@ -1342,9 +1332,9 @@ object BasicStepTactic {
case class RightRefl(phi: Formula) extends ProofStepWithoutBotNorPrem(0) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
if (premises.length != 0)
invalid(s"No premises expected, ${premises.length} received.")
@@ -1352,10 +1342,10 @@ object BasicStepTactic {
invalid("Right-hand side of conclusion does not contain φ.")
else
phi match {
- case PredicateFormula(`equality`, Seq(left, right)) =>
- if (isSame(left, right))
+ case PredicateFormula(`equality`, Seq(left, right)) =>
+ if (isSame(left, right))
SC.RightRefl(bot, phi)
- else
+ else
invalid("φ is not an instance of reflexivity.")
case _ => invalid("φ is not an equality.")
}
@@ -1365,14 +1355,12 @@ object BasicStepTactic {
case object RightReflWithoutFormula extends ProofStepWithoutBotNorPrem(0) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
- if (premises.length != 0)
- invalid(s"No premises expected, ${premises.length} received.")
- else if(bot.right.isEmpty)
- invalid("Right-hand side of conclusion does not contain an instance of reflexivity.")
+ if (premises.length != 0) invalid(s"No premises expected, ${premises.length} received.")
+ else if (bot.right.isEmpty) invalid("Right-hand side of conclusion does not contain an instance of reflexivity.")
else {
// go through conclusion to see if you can find an reflexive formula
val pivot: Option[Formula] = bot.right.find(f =>
@@ -1386,7 +1374,7 @@ object BasicStepTactic {
case Some(phi) => RightRefl(phi).asSCProof(bot, premises, currentProof)
case _ => invalid("Could not infer an equality as pivot from conclusion.")
}
-
+
}
}
@@ -1412,9 +1400,9 @@ object BasicStepTactic {
case class LeftSubstEq(equals: List[(Term, Term)], lambdaPhi: LambdaTermFormula) extends ProofStepWithoutBotNorPrem(1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val premiseSequent = currentProof.getSequent(premises(0))
lazy val (s_es, t_es) = equals.unzip
@@ -1427,9 +1415,9 @@ object BasicStepTactic {
else if (!isSameSet(bot.right, premiseSequent.right))
invalid("Right-hand side of the premise is not the same as the right-hand side of the conclusion.")
else if (
- !isSameSet(bot.left + phi_s, premiseSequent.left ++ equalities + phi_t) &&
- !isSameSet(bot.left + phi_t, premiseSequent.left ++ equalities + phi_s)
- )
+ !isSameSet(bot.left + phi_s, premiseSequent.left ++ equalities + phi_t) &&
+ !isSameSet(bot.left + phi_t, premiseSequent.left ++ equalities + phi_s)
+ )
invalid("Left-hand side of the conclusion + φ(s_) is not the same as left-hand side of the premise + (s=t)_ + φ(t_) (or with s_ and t_ swapped).")
else
SC.LeftSubstEq(bot, premises(0), equals, lambdaPhi)
@@ -1446,9 +1434,9 @@ object BasicStepTactic {
case class RightSubstEq(equals: List[(Term, Term)], lambdaPhi: LambdaTermFormula) extends ProofStepWithoutBotNorPrem(1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val premiseSequent = currentProof.getSequent(premises(0))
lazy val (s_es, t_es) = equals.unzip
@@ -1461,9 +1449,9 @@ object BasicStepTactic {
else if (!isSameSet(bot.left, premiseSequent.left ++ equalities))
invalid("Left-hand side of the conclusion is not the same as the left-hand side of the premise + (s=t)_.")
else if (
- !isSameSet(bot.left + phi_s, premiseSequent.left + phi_t) &&
- !isSameSet(bot.left + phi_t, premiseSequent.left + phi_s)
- )
+ !isSameSet(bot.left + phi_s, premiseSequent.left + phi_t) &&
+ !isSameSet(bot.left + phi_t, premiseSequent.left + phi_s)
+ )
invalid("Right-hand side of the conclusion + φ(s_) is not the same as right-hand side of the premise + φ(t_) (or with s_ and t_ swapped).")
else
SC.RightSubstEq(bot, premises(0), equals, lambdaPhi)
@@ -1480,9 +1468,9 @@ object BasicStepTactic {
case class LeftSubstIff(equals: List[(Formula, Formula)], lambdaPhi: LambdaFormulaFormula) extends ProofStepWithoutBotNorPrem(1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val premiseSequent = currentProof.getSequent(premises(0))
lazy val (psi_es, tau_es) = equals.unzip
@@ -1495,9 +1483,9 @@ object BasicStepTactic {
else if (!isSameSet(bot.right, premiseSequent.right))
invalid("Right-hand side of the premise is not the same as the right-hand side of the conclusion.")
else if (
- !isSameSet(bot.left + phi_psi, premiseSequent.left ++ implications + phi_tau) &&
- !isSameSet(bot.left + phi_tau, premiseSequent.left ++ implications + phi_psi)
- )
+ !isSameSet(bot.left + phi_psi, premiseSequent.left ++ implications + phi_tau) &&
+ !isSameSet(bot.left + phi_tau, premiseSequent.left ++ implications + phi_psi)
+ )
invalid("Left-hand side of the conclusion + φ(ψ_) is not the same as left-hand side of the premise + (ψ ↔ τ)_ + φ(τ_) (or with ψ_ and τ_ swapped).")
else
SC.LeftSubstIff(bot, premises(0), equals, lambdaPhi)
@@ -1514,9 +1502,9 @@ object BasicStepTactic {
case class RightSubstIff(equals: List[(Formula, Formula)], lambdaPhi: LambdaFormulaFormula) extends ProofStepWithoutBotNorPrem(1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val premiseSequent = currentProof.getSequent(premises(0))
lazy val (psi_es, tau_es) = equals.unzip
@@ -1529,9 +1517,9 @@ object BasicStepTactic {
else if (!isSameSet(bot.left, premiseSequent.left ++ implications))
invalid("Left-hand side of the conclusion is not the same as the left-hand side of the premise + (ψ ↔ τ)_.")
else if (
- !isSameSet(bot.left + phi_psi, premiseSequent.left + phi_tau) &&
- !isSameSet(bot.left + phi_tau, premiseSequent.left + phi_psi)
- )
+ !isSameSet(bot.left + phi_psi, premiseSequent.left + phi_tau) &&
+ !isSameSet(bot.left + phi_tau, premiseSequent.left + phi_psi)
+ )
invalid("Right-hand side of the conclusion + φ(ψ_) is not the same as right-hand side of the premise + φ(τ_) (or with ψ_ and τ_ swapped).")
else
SC.RightSubstIff(bot, premises(0), equals, lambdaPhi)
@@ -1548,9 +1536,9 @@ object BasicStepTactic {
case class InstFunSchema(insts: Map[SchematicTermLabel, LambdaTermTerm]) extends ProofStepWithoutBotNorPrem(1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val premiseSequent = currentProof.getSequent(premises(0))
@@ -1575,9 +1563,9 @@ object BasicStepTactic {
case class InstPredSchema(insts: Map[SchematicVarOrPredLabel, LambdaTermFormula]) extends ProofStepWithoutBotNorPrem(1) {
def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this.asProofStepWithoutBot(premises).asProofStep(bot),
- msg
- )
+ this.asProofStepWithoutBot(premises).asProofStep(bot),
+ msg
+ )
lazy val premiseSequent = currentProof.getSequent(premises(0))
@@ -1596,12 +1584,12 @@ object BasicStepTactic {
case class SCSubproof(sp: SCProof, premises: Seq[Int] = Seq.empty, display: Boolean = true) extends ProofStep {
def asSCProof(currentProof: Library#Proof): ProofStepJudgement = {
def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
- this,
- msg
- )
+ this,
+ msg
+ )
lazy val premiseSequents = premises.map(currentProof.getSequent(_))
- lazy val invalidPremise = premises.zipWithIndex.find( (no, p) => !SC.isSameSequent(premiseSequents(no), sp.imports(p)))
+ lazy val invalidPremise = premises.zipWithIndex.find((no, p) => !SC.isSameSequent(premiseSequents(no), sp.imports(p)))
if (premises.length != sp.imports.length)
invalid(s"Subproof expected ${sp.imports.length} premises, ${premises.length} received.")
--
GitLab