From 78cfcc816ccc8ed01dfe70c36d857b8155c29b5b Mon Sep 17 00:00:00 2001
From: Florian Cassayre <florian.cassayre@gmail.com>
Date: Mon, 21 Feb 2022 08:56:55 +0100
Subject: [PATCH] Introduce the proof judgement ADT
---
src/main/scala/lisa/kernel/Printer.scala | 27 +-
.../lisa/kernel/proof/SCProofChecker.scala | 230 +++++++++---------
.../proof/SCProofCheckerJudgement.scala | 33 +++
src/test/scala/lisa/kernel/ProofTests.scala | 6 +-
.../scala/lisa/proven/SimpleProverTests.scala | 4 +-
src/test/scala/test/ProofCheckerSuite.scala | 6 +-
6 files changed, 172 insertions(+), 134 deletions(-)
create mode 100644 src/main/scala/lisa/kernel/proof/SCProofCheckerJudgement.scala
diff --git a/src/main/scala/lisa/kernel/Printer.scala b/src/main/scala/lisa/kernel/Printer.scala
index 6f27c597..cd8c20e2 100644
--- a/src/main/scala/lisa/kernel/Printer.scala
+++ b/src/main/scala/lisa/kernel/Printer.scala
@@ -1,8 +1,9 @@
package lisa.kernel
import lisa.kernel.fol.FOL.*
-import lisa.kernel.proof.SequentCalculus._
-import lisa.kernel.proof.SCProof
+import lisa.kernel.proof.SequentCalculus.*
+import lisa.kernel.proof.SCProofCheckerJudgement.*
+import lisa.kernel.proof.{SCProof, SCProofCheckerJudgement}
/**
* A set of methods to pretty-print kernel trees.
@@ -182,10 +183,11 @@ object Printer {
/**
* Returns a string representation of this proof.
* @param proof the proof
- * @param showError if set, marks that particular step in the proof (`->`) as an error
+ * @param judgement optionally provide a proof checking judgement that will mark a particular step in the proof
+ * (`->`) as an error. The proof is considered to be valid by default
* @return a string where each indented line corresponds to a step in the proof
*/
- def prettySCProof(proof: SCProof, showError: Option[(Seq[Int], String)] = None): String = {
+ def prettySCProof(proof: SCProof, judgement: SCProofCheckerJudgement = SCValidProof): String = {
def computeMaxNumbering(proof: SCProof, level: Int, result: IndexedSeq[Int]): IndexedSeq[Int] = {
val resultWithCurrent = result.updated(level, Math.max(proof.steps.size - 1, result(level)))
proof.steps.collect { case sp: SCSubproof => sp }.foldLeft(resultWithCurrent)((acc, sp) => computeMaxNumbering(sp.sp, level + 1, if(acc.size <= level + 1) acc :+ 0 else acc))
@@ -205,7 +207,10 @@ object Printer {
def prettySCProofRecursive(proof: SCProof, level: Int, tree: IndexedSeq[Int], topMostIndices: IndexedSeq[Int]): Seq[(Boolean, String, String, String)] = {
val printedImports = proof.imports.zipWithIndex.reverse.flatMap { case (imp, i) =>
val currentTree = tree :+ (-i-1)
- val showErrorForLine = showError.exists((position, reason) => currentTree.startsWith(position) && currentTree.drop(position.size).forall(_ == 0))
+ val showErrorForLine = judgement match {
+ case SCValidProof => false
+ case SCInvalidProof(position, _) => currentTree.startsWith(position) && currentTree.drop(position.size).forall(_ == 0)
+ }
val prefix = (Seq.fill(level - topMostIndices.size)(None) ++ Seq.fill(topMostIndices.size)(None) :+ Some(-i-1)) ++ Seq.fill(maxLevel - level)(None)
val prefixString = prefix.map(_.map(_.toString).getOrElse("")).zipWithIndex.map { case (v, i1) => leftPadSpaces(v, maxNumberingLengths(i1)) }.mkString(" ")
def pretty(stepName: String, topSteps: Int*): (Boolean, String, String, String) =
@@ -220,7 +225,10 @@ object Printer {
}
printedImports ++ proof.steps.zipWithIndex.flatMap { case (step, i) =>
val currentTree = tree :+ i
- val showErrorForLine = showError.exists((position, reason) => currentTree.startsWith(position) && currentTree.drop(position.size).forall(_ == 0))
+ val showErrorForLine = judgement match {
+ case SCValidProof => false
+ case SCInvalidProof(position, _) => currentTree.startsWith(position) && currentTree.drop(position.size).forall(_ == 0)
+ }
val prefix = (Seq.fill(level - topMostIndices.size)(None) ++ Seq.fill(topMostIndices.size)(None) :+ Some(i)) ++ Seq.fill(maxLevel - level)(None)
val prefixString = prefix.map(_.map(_.toString).getOrElse("")).zipWithIndex.map { case (v, i1) => leftPadSpaces(v, maxNumberingLengths(i1)) }.mkString(" ")
def pretty(stepName: String, topSteps: Int*): (Boolean, String, String, String) =
@@ -276,9 +284,12 @@ object Printer {
lines.map {
case (isMarked, indices, stepName, sequent) =>
val suffix = Seq(indices, rightPadSpaces(stepName, maxStepNameLength), sequent)
- val full = if(showError.nonEmpty) (if(isMarked) marker else leftPadSpaces("", marker.length)) +: suffix else suffix
+ val full = if(!judgement.isValid) (if(isMarked) marker else leftPadSpaces("", marker.length)) +: suffix else suffix
full.mkString(" ")
- }.mkString("\n") + (if (showError.nonEmpty) s"\nProof checker has reported error at line ${showError.get._1}: ${showError.get._2}" else "")
+ }.mkString("\n") + (judgement match {
+ case SCValidProof => ""
+ case SCInvalidProof(path, message) => s"\nProof checker has reported error at line ${path.mkString(".")}: $message"
+ })
}
}
diff --git a/src/main/scala/lisa/kernel/proof/SCProofChecker.scala b/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
index 11fd361e..6602e1ce 100644
--- a/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
+++ b/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
@@ -3,6 +3,7 @@ package lisa.kernel.proof
import lisa.kernel.Printer
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.SequentCalculus.*
+import lisa.kernel.proof.SCProofCheckerJudgement.*
object SCProofChecker {
@@ -21,16 +22,16 @@ object SCProofChecker {
* a proof's [[SCProof.getSequent]] function.
* @return
*/
- def checkSingleSCStep(no:Int, step: SCProofStep, references : Int => Sequent, importsSize: Option[Int]=None):(Boolean, List[Int], String) = {
+ def checkSingleSCStep(no:Int, step: SCProofStep, references : Int => Sequent, importsSize: Option[Int]=None): SCProofCheckerJudgement = {
val ref = references
val false_premise = step.premises.find(i => i >= no)
val false_premise2 = if (importsSize.nonEmpty) step.premises.find(i => i< -importsSize.get) else None
- val r: (Boolean, List[Int], String) =
+ val r: SCProofCheckerJudgement =
if (false_premise.nonEmpty)
- return (false, Nil, s"Step no $no can't refer to higher number ${false_premise.get} as a premise.")
- if (false_premise2.nonEmpty)
- return (false, Nil, s"A step can't refer to step ${false_premise2.get}, imports only contains ${importsSize.get} elements.")
+ SCInvalidProof(Nil, s"Step no $no can't refer to higher number ${false_premise.get} as a premise.")
+ else if (false_premise2.nonEmpty)
+ SCInvalidProof(Nil, s"A step can't refer to step ${false_premise2.get}, imports only contains ${importsSize.get} elements.")
else step match {
/*
* Γ |- Δ
@@ -38,7 +39,7 @@ object SCProofChecker {
* Γ |- Δ
*/
case Rewrite(s, t1) =>
- if (isSameSequent(s, ref(t1))) (true, Nil, "") else (false, Nil, s"The premise and the conclusion are not trivially equivalent.")
+ if (isSameSequent(s, ref(t1))) SCValidProof else SCInvalidProof(Nil, s"The premise and the conclusion are not trivially equivalent.")
/*
*
* --------------
@@ -46,10 +47,10 @@ object SCProofChecker {
*/
case Hypothesis(Sequent(left, right), phi) =>
if (contains(left, phi))
- if (contains(right, phi)) (true, Nil, "")
+ if (contains(right, phi)) SCValidProof
- else (false, Nil, s"Right-hand side does not contain formula φ")
- else (false, Nil, s"Left-hand side does not contain formula φ")
+ else SCInvalidProof(Nil, s"Right-hand side does not contain formula φ")
+ else SCInvalidProof(Nil, s"Left-hand side does not contain formula φ")
/*
* Γ |- Δ, φ φ, Σ |- Π
* ------------------------
@@ -60,11 +61,11 @@ object SCProofChecker {
if (isSameSet(b.right + phi, ref(t2).right union ref(t1).right))
if (contains(ref(t2).left, phi))
if (contains(ref(t1).right, phi))
- (true, Nil, "")
- else (false, Nil, s"Right-hand side of first premise does not contain φ as claimed.")
- else (false, Nil, s"Left-hand side of second premise does not contain φ as claimed.")
- else (false, Nil, s"Right-hand side of conclusion + φ is not the union of the right-hand sides of the premises.")
- else (false, Nil, s"Left-hand side of conclusion + φ is not the union of the left-hand sides of the premises.")
+ SCValidProof
+ else SCInvalidProof(Nil, s"Right-hand side of first premise does not contain φ as claimed.")
+ else SCInvalidProof(Nil, s"Left-hand side of second premise does not contain φ as claimed.")
+ else SCInvalidProof(Nil, s"Right-hand side of conclusion + φ is not the union of the right-hand sides of the premises.")
+ else SCInvalidProof(Nil, s"Left-hand side of conclusion + φ is not the union of the left-hand sides of the premises.")
// Left rules
/*
@@ -78,9 +79,9 @@ object SCProofChecker {
if (isSameSet(b.left + phi, ref(t1).left + phiAndPsi) ||
isSameSet(b.left + psi, ref(t1).left + phiAndPsi) ||
isSameSet(b.left + phi + psi, ref(t1).left + phiAndPsi))
- (true, Nil, "")
- else (false, Nil, "Left-hand side of conclusion + φ∧ψ must be same as left-hand side of premise + either φ, ψ or both.")
- else (false, Nil, "Right-hand sides of the premise and the conclusion must be the same.")
+ SCValidProof
+ else SCInvalidProof(Nil, "Left-hand side of conclusion + φ∧ψ must be same as left-hand side of premise + either φ, ψ or both.")
+ else SCInvalidProof(Nil, "Right-hand sides of the premise and the conclusion must be the same.")
/*
* Γ, φ |- Δ Σ, ψ |- Π
* ------------------------
@@ -90,9 +91,9 @@ object SCProofChecker {
if (isSameSet(b.right, t.map(ref(_).right).reduce(_ union _)) )
val phiOrPsi = ConnectorFormula(Or, disjuncts)
if (isSameSet(disjuncts.foldLeft(b.left)(_ + _), t.map(ref(_).left).reduce(_ union _) + phiOrPsi))
- (true, Nil, "")
- else (false, Nil, s"Left-hand side of conclusion + disjuncts is not the same as the union of the left-hand sides of the premises + φ∨ψ.")
- else (false, Nil, s"Right-hand side of conclusion is not the union of the right-hand sides of the premises.")
+ SCValidProof
+ else SCInvalidProof(Nil, s"Left-hand side of conclusion + disjuncts is not the same as the union of the left-hand sides of the premises + φ∨ψ.")
+ else SCInvalidProof(Nil, s"Right-hand side of conclusion is not the union of the right-hand sides of the premises.")
/*
* Γ |- φ, Δ Σ, ψ |- Π
* ------------------------
@@ -102,9 +103,9 @@ object SCProofChecker {
val phiImpPsi = ConnectorFormula(Implies, Seq(phi, psi))
if (isSameSet(b.right + phi, ref(t1).right union ref(t2).right))
if (isSameSet(b.left + psi, ref(t1).left union ref(t2).left + phiImpPsi))
- (true, Nil, "")
- else (false, Nil, s"Left-hand side of conclusion + ψ must be identical to union of left-hand sides of premisces + φ→ψ.")
- else (false, Nil, s"Right-hand side of conclusion + φ must be identical to union of right-hand sides of premisces.")
+ SCValidProof
+ else SCInvalidProof(Nil, s"Left-hand side of conclusion + ψ must be identical to union of left-hand sides of premisces + φ→ψ.")
+ else SCInvalidProof(Nil, s"Right-hand side of conclusion + φ must be identical to union of right-hand sides of premisces.")
/*
* Γ, φ→ψ |- Δ Γ, φ→ψ, ψ→φ |- Δ
* -------------- or ---------------
@@ -118,9 +119,9 @@ object SCProofChecker {
if (isSameSet(b.left + phiImpPsi , ref(t1).left + phiIffPsi) ||
isSameSet(b.left + psiImpPhi , ref(t1).left + phiIffPsi) ||
isSameSet(b.left + phiImpPsi + psiImpPhi , ref(t1).left + phiIffPsi))
- (true, Nil, "")
- else (false, Nil, "Left-hand side of conclusion + φ↔ψ must be same as left-hand side of premise + either φ→ψ, ψ→φ or both.")
- else (false, Nil, "Right-hand sides of premise and conclusion must be the same.")
+ SCValidProof
+ else SCInvalidProof(Nil, "Left-hand side of conclusion + φ↔ψ must be same as left-hand side of premise + either φ→ψ, ψ→φ or both.")
+ else SCInvalidProof(Nil, "Right-hand sides of premise and conclusion must be the same.")
/*
* Γ |- φ, Δ
@@ -131,9 +132,9 @@ object SCProofChecker {
val nPhi = ConnectorFormula(Neg, Seq(phi))
if (isSameSet(b.left, ref(t1).left + nPhi))
if (isSameSet(b.right + phi, ref(t1).right))
- (true, Nil, "")
- else (false, Nil, "Right-hand side of conclusion + φ must be the same as right-hand side of premise")
- else (false, Nil, "Left-hand side of conclusion must be the same as left-hand side of premise + ¬φ")
+ SCValidProof
+ else SCInvalidProof(Nil, "Right-hand side of conclusion + φ must be the same as right-hand side of premise")
+ else SCInvalidProof(Nil, "Left-hand side of conclusion must be the same as left-hand side of premise + ¬φ")
/*
* Γ, φ[t/x] |- Δ
@@ -143,9 +144,9 @@ object SCProofChecker {
case LeftForall(b, t1, phi, x, t) =>
if (isSameSet(b.right, ref(t1).right))
if (isSameSet(b.left + substituteVariable(phi, x, t), ref(t1).left + BinderFormula(Forall, x, phi)))
- (true, Nil, "")
- else (false, Nil, "Left-hand side of conclusion + φ[t/x] must be the same as left-hand side of premise + ∀x. φ")
- else (false, Nil, "Right-hand side of conclusion must be the same as right-hand side of premise")
+ SCValidProof
+ else SCInvalidProof(Nil, "Left-hand side of conclusion + φ[t/x] must be the same as left-hand side of premise + ∀x. φ")
+ else SCInvalidProof(Nil, "Right-hand side of conclusion must be the same as right-hand side of premise")
/*
* Γ, φ |- Δ
@@ -156,10 +157,10 @@ object SCProofChecker {
if (isSameSet(b.right, ref(t1).right))
if (isSameSet(b.left + phi, ref(t1).left + BinderFormula(Exists, x, phi)))
if ((b.left union b.right).forall(f => !f.freeVariables.contains(x)))
- (true, Nil, "")
- else (false, Nil, "The variable x must not be free in the resulting sequent.")
- else (false, Nil, "Left-hand side of conclusion + φ must be the same as left-hand side of premise + ∃x. φ")
- else (false, Nil, "Right-hand side of conclusion must be the same as right-hand side of premise")
+ SCValidProof
+ else SCInvalidProof(Nil, "The variable x must not be free in the resulting sequent.")
+ else SCInvalidProof(Nil, "Left-hand side of conclusion + φ must be the same as left-hand side of premise + ∃x. φ")
+ else SCInvalidProof(Nil, "Right-hand side of conclusion must be the same as right-hand side of premise")
/*
* Γ, ∃y.∀x. (x=y) ↔ φ |- Δ
@@ -171,9 +172,9 @@ object SCProofChecker {
val temp = BinderFormula(Exists, y, BinderFormula(Forall, x, ConnectorFormula(Iff, List(PredicateFormula(equality, List(VariableTerm(x), VariableTerm(y))), phi))))
if (isSameSet(b.right, ref(t1).right))
if (isSameSet(b.left + temp, ref(t1).left + BinderFormula(ExistsOne, x, phi)))
- (true, Nil, "")
- else (false, Nil, "Left-hand side of conclusion + ∃y.∀x. (x=y) ↔ φ must be the same as left-hand side of premise + ∃!x. φ")
- else (false, Nil, "Right-hand side of conclusion must be the same as right-hand side of premise")
+ SCValidProof
+ else SCInvalidProof(Nil, "Left-hand side of conclusion + ∃y.∀x. (x=y) ↔ φ must be the same as left-hand side of premise + ∃!x. φ")
+ else SCInvalidProof(Nil, "Right-hand side of conclusion must be the same as right-hand side of premise")
// Right rules
/*
@@ -185,9 +186,9 @@ object SCProofChecker {
val phiAndPsi = ConnectorFormula(And, cunjuncts)
if (isSameSet(b.left, t.map(ref(_).left).reduce(_ union _)))
if (isSameSet(cunjuncts.foldLeft(b.right)(_ + _), t.map(ref(_).right).reduce(_ union _) + phiAndPsi))
- (true, Nil, "")
- else (false, Nil, s"Right-hand side of conclusion + φ + ψ is not the same as the union of the right-hand sides of the premises φ∧ψ.")
- else (false, Nil, s"Left-hand side of conclusion is not the union of the left-hand sides of the premises.")
+ SCValidProof
+ else SCInvalidProof(Nil, s"Right-hand side of conclusion + φ + ψ is not the same as the union of the right-hand sides of the premises φ∧ψ.")
+ else SCInvalidProof(Nil, s"Left-hand side of conclusion is not the union of the left-hand sides of the premises.")
/*
* Γ |- φ, Δ Γ |- φ, ψ, Δ
* -------------- or ---------------
@@ -199,9 +200,9 @@ object SCProofChecker {
if (isSameSet(b.right + phi, ref(t1).right + phiOrPsi) ||
isSameSet(b.right + psi, ref(t1).right + phiOrPsi) ||
isSameSet(b.right + phi + psi, ref(t1).right + phiOrPsi))
- (true, Nil, "")
- else (false, Nil, "Right-hand side of conclusion + φ∧ψ must be same as right-hand side of premise + either φ, ψ or both.")
- else (false, Nil, "Left-hand sides of the premise and the conclusion must be the same.")
+ SCValidProof
+ else SCInvalidProof(Nil, "Right-hand side of conclusion + φ∧ψ must be same as right-hand side of premise + either φ, ψ or both.")
+ else SCInvalidProof(Nil, "Left-hand sides of the premise and the conclusion must be the same.")
/*
* Γ, φ |- ψ, Δ
* --------------
@@ -211,9 +212,9 @@ object SCProofChecker {
val phiImpPsi = ConnectorFormula(Implies, Seq(phi, psi))
if (isSameSet(ref(t1).left, b.left + phi))
if (isSameSet(b.right + psi, ref(t1).right + phiImpPsi))
- (true, Nil, "")
- else (false, Nil, "Right-hand side of conclusion + ψ must be same as right-hand side of premise + φ→ψ.")
- else (false, Nil, "Left-hand side of conclusion + psi must be same as left-hand side of premise.")
+ SCValidProof
+ else SCInvalidProof(Nil, "Right-hand side of conclusion + ψ must be same as right-hand side of premise + φ→ψ.")
+ else SCInvalidProof(Nil, "Left-hand side of conclusion + psi must be same as left-hand side of premise.")
/*
* Γ |- a→ψ, Δ Σ |- ψ→φ, Π
* ----------------------------
@@ -225,9 +226,9 @@ object SCProofChecker {
val phiIffPsi = ConnectorFormula(Iff, Seq(phi, psi))
if (isSameSet(b.left, ref(t1).left union ref(t2).left))
if (isSameSet(b.right + phiImpPsi + psiImpPhi, ref(t1).right union ref(t2).right + phiIffPsi))
- (true, Nil, "")
- else (false, Nil, s"Right-hand side of conclusion + a→ψ + ψ→φ is not the same as the union of the right-hand sides of the premises φ↔b.")
- else (false, Nil, s"Left-hand side of conclusion is not the union of the left-hand sides of the premises.")
+ SCValidProof
+ else SCInvalidProof(Nil, s"Right-hand side of conclusion + a→ψ + ψ→φ is not the same as the union of the right-hand sides of the premises φ↔b.")
+ else SCInvalidProof(Nil, s"Left-hand side of conclusion is not the union of the left-hand sides of the premises.")
/*
* Γ, φ |- Δ
* --------------
@@ -237,9 +238,9 @@ object SCProofChecker {
val nPhi = ConnectorFormula(Neg, Seq(phi))
if (isSameSet(b.right, ref(t1).right + nPhi))
if (isSameSet(b.left + phi, ref(t1).left))
- (true, Nil, "")
- else (false, Nil, "Left-hand side of conclusion + φ must be the same as left-hand side of premise")
- else (false, Nil, "Right-hand side of conclusion must be the same as right-hand side of premise + ¬φ")
+ SCValidProof
+ else SCInvalidProof(Nil, "Left-hand side of conclusion + φ must be the same as left-hand side of premise")
+ else SCInvalidProof(Nil, "Right-hand side of conclusion must be the same as right-hand side of premise + ¬φ")
/*
* Γ |- φ, Δ
* ------------------- if x is not free in the resulting sequent
@@ -249,10 +250,10 @@ object SCProofChecker {
if (isSameSet(b.left, ref(t1).left))
if (isSameSet(b.right + phi, ref(t1).right + BinderFormula(Forall, x ,phi)))
if ((b.left union b.right).forall(f => !f.freeVariables.contains(x)))
- (true, Nil, "")
- else (false, Nil, "The variable x must not be free in the resulting sequent.")
- else (false, Nil, "Right-hand side of conclusion + φ must be the same as right-hand side of premise + ∀x. φ")
- else (false, Nil, "Left-hand sides of conclusion and premise must be the same.")
+ SCValidProof
+ else SCInvalidProof(Nil, "The variable x must not be free in the resulting sequent.")
+ else SCInvalidProof(Nil, "Right-hand side of conclusion + φ must be the same as right-hand side of premise + ∀x. φ")
+ else SCInvalidProof(Nil, "Left-hand sides of conclusion and premise must be the same.")
/*
* Γ |- φ[t/x], Δ
* -------------------
@@ -261,9 +262,9 @@ object SCProofChecker {
case RightExists(b, t1, phi, x, t) =>
if (isSameSet(b.left, ref(t1).left))
if (isSameSet(b.right + substituteVariable(phi, x, t), ref(t1).right + BinderFormula(Exists, x ,phi)))
- (true, Nil, "")
- else (false, Nil, "Right-hand side of the conclusion + φ[t/x] must be the same as right-hand side of the premise + ∃x. φ")
- else (false, Nil, "Left-hand sides or conclusion and premise must be the same.")
+ SCValidProof
+ else SCInvalidProof(Nil, "Right-hand side of the conclusion + φ[t/x] must be the same as right-hand side of the premise + ∃x. φ")
+ else SCInvalidProof(Nil, "Left-hand sides or conclusion and premise must be the same.")
/**
* <pre>
@@ -277,9 +278,9 @@ object SCProofChecker {
val temp = BinderFormula(Exists, y, BinderFormula(Forall, x, ConnectorFormula(Iff, List(PredicateFormula(equality, List(VariableTerm(x), VariableTerm(y))), phi))))
if (isSameSet(b.left, ref(t1).left))
if (isSameSet(b.right + temp, ref(t1).right + BinderFormula(ExistsOne, x, phi)))
- (true, Nil, "")
- else (false, Nil, "Right-hand side of conclusion + ∃y.∀x. (x=y) ↔ φ must be the same as right-hand side of premise + ∃!x. φ")
- else (false, Nil, "Left-hand sides of conclusion and premise must be the same")
+ SCValidProof
+ else SCInvalidProof(Nil, "Right-hand side of conclusion + ∃y.∀x. (x=y) ↔ φ must be the same as right-hand side of premise + ∃!x. φ")
+ else SCInvalidProof(Nil, "Left-hand sides of conclusion and premise must be the same")
// Structural rules
@@ -291,9 +292,9 @@ object SCProofChecker {
case Weakening(b, t1) =>
if (isSubset(ref(t1).left, b.left))
if (isSubset(ref(t1).right, b.right))
- (true, Nil, "")
- else (false, Nil, "Right-hand side of premise must be a subset of right-hand side of conclusion")
- else (false, Nil, "Left-hand side of premise must be a subset of left-hand side of conclusion")
+ SCValidProof
+ else SCInvalidProof(Nil, "Right-hand side of premise must be a subset of right-hand side of conclusion")
+ else SCInvalidProof(Nil, "Left-hand side of premise must be a subset of left-hand side of conclusion")
// Equality Rules
/*
@@ -307,11 +308,11 @@ object SCProofChecker {
if (isSame(left, right))
if (isSameSet(b.right, ref(t1).right))
if (isSameSet(b.left + phi, ref(t1).left))
- (true, Nil, "")
- else (false, Nil, s"Left-hand sides of the conclusion + φ must be the same as left-hand side of the premise.")
- else (false, Nil, s"Right-hand sides of the premise and the conclusion aren't the same.")
- else (false, Nil, s"φ is not an instance of reflexivity.")
- case _ => (false, Nil, "φ is not an equality")
+ SCValidProof
+ else SCInvalidProof(Nil, s"Left-hand sides of the conclusion + φ must be the same as left-hand side of the premise.")
+ else SCInvalidProof(Nil, s"Right-hand sides of the premise and the conclusion aren't the same.")
+ else SCInvalidProof(Nil, s"φ is not an instance of reflexivity.")
+ case _ => SCInvalidProof(Nil, "φ is not an equality")
}
/*
@@ -324,10 +325,10 @@ object SCProofChecker {
case PredicateFormula(`equality`, Seq(left, right)) =>
if (isSame(left, right))
if (contains(b.right, phi))
- (true, Nil, "")
- else (false, Nil, s"Right-Hand side of conclusion does not contain φ")
- else (false, Nil, s"φ is not an instance of reflexivity.")
- case _ => (false, Nil, s"φ is not an equality.")
+ SCValidProof
+ else SCInvalidProof(Nil, s"Right-Hand side of conclusion does not contain φ")
+ else SCInvalidProof(Nil, s"φ is not an instance of reflexivity.")
+ case _ => SCInvalidProof(Nil, s"φ is not an equality.")
}
/*
@@ -343,10 +344,10 @@ object SCProofChecker {
if (isSameSet(b.right, ref(t1).right))
if (isSameSet(b.left + phi_t_for_f, ref(t1).left + sEqT + phi_s_for_f) ||
isSameSet(b.left + phi_s_for_f, ref(t1).left + sEqT + phi_t_for_f))
- (true, Nil, "")
- else (false, Nil, "Left-hand sides of the conclusion + φ[s/?f] must be the same as left-hand side of the premise + s=t + φ[t/?f] (or with s and t swapped).")
- else (false, Nil, "Right-hand sides of the premise and the conclusion aren't the same.")
- else (false, Nil, "Function schema ?f must have arity 0")
+ SCValidProof
+ else SCInvalidProof(Nil, "Left-hand sides of the conclusion + φ[s/?f] must be the same as left-hand side of the premise + s=t + φ[t/?f] (or with s and t swapped).")
+ else SCInvalidProof(Nil, "Right-hand sides of the premise and the conclusion aren't the same.")
+ else SCInvalidProof(Nil, "Function schema ?f must have arity 0")
/*
@@ -362,10 +363,10 @@ object SCProofChecker {
val phi_t_for_f = instantiateFunctionSchema(phi, f, t, Nil)
if (isSameSet(b.right + phi_s_for_f, ref(t1).right + phi_t_for_f) ||
isSameSet(b.right + phi_t_for_f, ref(t1).right + phi_s_for_f))
- (true, Nil, "")
- else (false, Nil, s"Right-hand side of the premise and the conclusion should be the same with each containing one of φ[s/?f] φ[t/?f], but it isn't the case." )
- else (false, Nil, "Left-hand sides of the premise + s=t must be the same as left-hand side of the premise.")
- else (false, Nil, "Function schema ?f must have arity 0.")
+ SCValidProof
+ else SCInvalidProof(Nil, s"Right-hand side of the premise and the conclusion should be the same with each containing one of φ[s/?f] φ[t/?f], but it isn't the case." )
+ else SCInvalidProof(Nil, "Left-hand sides of the premise + s=t must be the same as left-hand side of the premise.")
+ else SCInvalidProof(Nil, "Function schema ?f must have arity 0.")
/*
* Γ, φ[ψ/?q] |- Δ
* ---------------------
@@ -379,10 +380,10 @@ object SCProofChecker {
if (isSameSet(b.right, ref(t1).right))
if (isSameSet(ref(t1).left + psiIffTau + phi_tau_for_q, b.left + phi_psi_for_q) ||
isSameSet(ref(t1).left + psiIffTau + phi_psi_for_q, b.left + phi_tau_for_q))
- (true, Nil, "")
- else (false, Nil, "Left-hand sides of the conclusion + φ[ψ/?q] must be the same as left-hand side of the premise + ψ↔τ + φ[τ/?q] (or with ψ and τ swapped).")
- else (false, Nil, "Right-hand sides of the premise and the conclusion aren't the same.")
- else (false, Nil, "Predicate schema ?q must have arity 0.")
+ SCValidProof
+ else SCInvalidProof(Nil, "Left-hand sides of the conclusion + φ[ψ/?q] must be the same as left-hand side of the premise + ψ↔τ + φ[τ/?q] (or with ψ and τ swapped).")
+ else SCInvalidProof(Nil, "Right-hand sides of the premise and the conclusion aren't the same.")
+ else SCInvalidProof(Nil, "Predicate schema ?q must have arity 0.")
/*
* Γ |- φ[ψ/?p], Δ
@@ -397,10 +398,10 @@ object SCProofChecker {
if (isSameSet(ref(t1).left + psiIffTau, b.left))
if (isSameSet(b.right + phi_tau_for_q, ref(t1).right + phi_psi_for_q) ||
isSameSet(b.right + phi_psi_for_q, ref(t1).right + phi_tau_for_q))
- (true, Nil, "")
- else (false, Nil, s"Right-hand side of the premise and the conclusion should be the same with each containing one of φ[τ/?q] and φ[ψ/?q], but it isn't the case." )
- else (false, Nil, "Left-hand sides of the premise + ψ↔τ must be the same as left-hand side of the premise.")
- else (false, Nil, "Predicate schema ?q must have arity 0.")
+ SCValidProof
+ else SCInvalidProof(Nil, s"Right-hand side of the premise and the conclusion should be the same with each containing one of φ[τ/?q] and φ[ψ/?q], but it isn't the case." )
+ else SCInvalidProof(Nil, "Left-hand sides of the premise + ψ↔τ must be the same as left-hand side of the premise.")
+ else SCInvalidProof(Nil, "Predicate schema ?q must have arity 0.")
/**
* <pre>
* Γ |- Δ
@@ -412,9 +413,9 @@ object SCProofChecker {
val expected = (ref(t1).left.map(phi => instantiateFunctionSchema(phi, f, r, a)), ref(t1).right.map(phi => instantiateFunctionSchema(phi, f, r, a)))
if (isSameSet(bot.left, expected._1))
if (isSameSet(bot.right, expected._2))
- (true, Nil, "")
- else (false, Nil, "Right-hand side of premise instantiated with [?f/r(a)] must be the same as right-hand side of conclusion.")
- else (false, Nil, "Left-hand side of premise instantiated with [?f/r(a)] must be the same as left-hand side of conclusion.")
+ SCValidProof
+ else SCInvalidProof(Nil, "Right-hand side of premise instantiated with [?f/r(a)] must be the same as right-hand side of conclusion.")
+ else SCInvalidProof(Nil, "Left-hand side of premise instantiated with [?f/r(a)] must be the same as left-hand side of conclusion.")
/**
* <pre>
@@ -427,45 +428,38 @@ object SCProofChecker {
val expected = (ref(t1).left.map(phi => instantiatePredicateSchema(phi, p, psi, a)), ref(t1).right.map(phi => instantiatePredicateSchema(phi, p, psi, a)))
if (isSameSet(bot.left, expected._1))
if (isSameSet(bot.right, expected._2))
- (true, Nil, "")
- else (false, Nil, "Right-hand side of premise instantiated with [?p/ψ(a)] must be the same as right-hand side of conclusion.")
- else (false, Nil, "Left-hand side of premise instantiated with [?p/ψ(a)] must be the same as left-hand side of conclusion.")
+ SCValidProof
+ else SCInvalidProof(Nil, "Right-hand side of premise instantiated with [?p/ψ(a)] must be the same as right-hand side of conclusion.")
+ else SCInvalidProof(Nil, "Left-hand side of premise instantiated with [?p/ψ(a)] must be the same as left-hand side of conclusion.")
case SCSubproof(sp, premises, _) =>
if (premises.size == sp.imports.size){
val invalid = premises.zipWithIndex.find((no, p) => !isSameSequent(ref(no), sp.imports(p)) )
if (invalid.isEmpty){
- val r_subproof = checkSCProof(sp)
- if (r_subproof._1)
- (true, Nil, "")
- else (false, r_subproof._2, r_subproof._3)
- } else (false, Nil, s"Premise number ${invalid.get._1} (refering to step ${invalid.get}) is not the same as import number ${invalid.get._1} of the subproof.")
- } else (false, Nil, "Number of premises and imports don't match: "+premises.size+" "+sp.imports.size)
+ checkSCProof(sp)
+ } else SCInvalidProof(Nil, s"Premise number ${invalid.get._1} (refering to step ${invalid.get}) is not the same as import number ${invalid.get._1} of the subproof.")
+ } else SCInvalidProof(Nil, "Number of premises and imports don't match: "+premises.size+" "+sp.imports.size)
}
r
}
/**
- * Verifies if a given pure SequentCalculus is conditionally correct, as the imported sequents are assumed.
+ * Verifies if a given pure SequentCalculus is conditionally correct, as the imported sequents are assumed.
* If the proof is not correct, the functrion will report the faulty line and a brief explanation.
* @param proof A SC proof to check
- * @return (true, Nil, "") if the proof is correct, else (false, l, s) with l the path to the incorrect
- proof step and s an explanation.
- *
+ * @return SCValidProof if the proof is correct, else SCInvalidProof with the path to the incorrect proof step
+ * and an explanation.
*/
- def checkSCProof(proof: SCProof) : (Boolean, List[Int], String) = {
-
-
+ def checkSCProof(proof: SCProof): SCProofCheckerJudgement = {
val possibleError = proof.steps.view.zipWithIndex.map((step, no) =>
-
- val r = checkSingleSCStep(no, step, (i:Int) => proof.getSequent(i), Some(proof.imports.size))
- (r._1, no::r._2, r._3)
- ).find(p => !p._1 )
- if (possibleError.isEmpty) (true, Nil, "")
+ checkSingleSCStep(no, step, (i: Int) => proof.getSequent(i), Some(proof.imports.size)) match {
+ case SCInvalidProof(path, message) => SCInvalidProof(no +: path, message)
+ case SCValidProof => SCValidProof
+ }
+ ).find(j => !j.isValid)
+ if (possibleError.isEmpty) SCValidProof
else possibleError.get
-
-
}
}
diff --git a/src/main/scala/lisa/kernel/proof/SCProofCheckerJudgement.scala b/src/main/scala/lisa/kernel/proof/SCProofCheckerJudgement.scala
new file mode 100644
index 00000000..bf81d106
--- /dev/null
+++ b/src/main/scala/lisa/kernel/proof/SCProofCheckerJudgement.scala
@@ -0,0 +1,33 @@
+package lisa.kernel.proof
+
+/**
+ * The judgement (or verdict) of a proof checking procedure.
+ * Typically, see [[SCProofChecker.checkSingleSCStep]] and [[SCProofChecker.checkSCProof]].
+ */
+sealed abstract class SCProofCheckerJudgement {
+ import SCProofCheckerJudgement.*
+
+ /**
+ * Whether this judgement is positive -- the proof is concluded to be valid;
+ * or negative -- the proof checker couldn't certify the validity of this proof.
+ * @return An instance of either [[SCValidProof]] or [[SCInvalidProof]]
+ */
+ def isValid: Boolean = this match {
+ case SCValidProof => true
+ case _: SCInvalidProof => false
+ }
+}
+
+object SCProofCheckerJudgement {
+ /**
+ * A positive judgement.
+ */
+ case object SCValidProof extends SCProofCheckerJudgement
+
+ /**
+ * A negative judgement.
+ * @param path The path of the error, expressed as indices
+ * @param message The error message that hints about the first error encountered
+ */
+ case class SCInvalidProof(path: Seq[Int], message: String) extends SCProofCheckerJudgement
+}
diff --git a/src/test/scala/lisa/kernel/ProofTests.scala b/src/test/scala/lisa/kernel/ProofTests.scala
index d2a91582..8389948f 100644
--- a/src/test/scala/lisa/kernel/ProofTests.scala
+++ b/src/test/scala/lisa/kernel/ProofTests.scala
@@ -31,14 +31,14 @@ class ProofTests extends AnyFunSuite {
val s3 = LeftImplies((a ==> b) ==> a |- a, 2, 0, a ==> b, a)
val s4 = RightImplies(() |- (a ==> b) ==> a ==> a, 3, (a ==> b) ==> a, a)
val ppl: SCProof = SCProof(IndexedSeq(s0, s1, s2, s3, s4))
- assert(predicateVerifier(ppl)._1)
+ assert(predicateVerifier(ppl).isValid)
}
test("Verification of substitution") {
val t0 = Hypothesis(fp(x)|-fp(x), fp(x))
val t1 = RightSubstEq(Set(fp(x), x === y) |- fp(y), 0, x, y, fp(sT()), sT)
val pr = new SCProof(IndexedSeq(t0, t1))
- assert(predicateVerifier(pr)._1)
+ assert(predicateVerifier(pr).isValid)
}
test("Commutativity on a random large formula") {
@@ -58,6 +58,6 @@ class ProofTests extends AnyFunSuite {
val orig = subformulas.next().head
val swapped = subformulasSwapped.next().head
val prf = SCProof(Vector(Hypothesis(Sequent(Set(orig), Set(orig)), orig), Rewrite(Sequent(Set(orig), Set(swapped)), 0)))
- assert(predicateVerifier(prf)._1)
+ assert(predicateVerifier(prf).isValid)
}
}
diff --git a/src/test/scala/lisa/proven/SimpleProverTests.scala b/src/test/scala/lisa/proven/SimpleProverTests.scala
index 8f88cc95..5eb2269e 100644
--- a/src/test/scala/lisa/proven/SimpleProverTests.scala
+++ b/src/test/scala/lisa/proven/SimpleProverTests.scala
@@ -13,7 +13,7 @@ import proven.tactics.SimplePropositionalSolver as SPS
class SimpleProverTests extends AnyFunSuite {
-
+
test("Simple propositional logic proofs") {
val problems = getPRPproblems.take(1)
@@ -24,7 +24,7 @@ class SimpleProverTests extends AnyFunSuite {
val proof = SPS.solveSequent(sq)
if (!Seq("Unsatisfiable", "Theorem", "Satisfiable").contains(pr.status)) println("Unknown status: "+pr.status+", "+pr.file)
- assert(SCProofChecker.checkSCProof(proof)._1 == (pr.status =="Unsatisfiable" || pr.status == "Theorem"))
+ assert(SCProofChecker.checkSCProof(proof).isValid == (pr.status =="Unsatisfiable" || pr.status == "Theorem"))
})
diff --git a/src/test/scala/test/ProofCheckerSuite.scala b/src/test/scala/test/ProofCheckerSuite.scala
index df8786aa..57872adb 100644
--- a/src/test/scala/test/ProofCheckerSuite.scala
+++ b/src/test/scala/test/ProofCheckerSuite.scala
@@ -26,12 +26,12 @@ abstract class ProofCheckerSuite extends AnyFunSuite {
}
def checkProof(proof: SCProof, expected: Sequent): Unit = {
- val error = checkSCProof(proof)
- assert(error._1, "\n"+Printer.prettySCProof(proof, error))
+ val judgement = checkSCProof(proof)
+ assert(judgement.isValid, "\n"+Printer.prettySCProof(proof, judgement))
assert(isSameSequent(proof.conclusion, expected), s"(${Printer.prettySequent(proof.conclusion)} did not equal ${Printer.prettySequent(expected)})")
}
def checkIncorrectProof(incorrectProof: SCProof): Unit = {
- assert(!checkSCProof(incorrectProof)._1, s"(incorrect proof with conclusion '${Printer.prettySequent(incorrectProof.conclusion)}' was accepted by the proof checker)\nSequent: ${incorrectProof.conclusion}")
+ assert(!checkSCProof(incorrectProof).isValid, s"(incorrect proof with conclusion '${Printer.prettySequent(incorrectProof.conclusion)}' was accepted by the proof checker)\nSequent: ${incorrectProof.conclusion}")
}
}
--
GitLab