diff --git a/lisa-examples/src/main/scala/Example.scala b/lisa-examples/src/main/scala/Example.scala
index 9010e489fdc450cb6d91e86488f540561eba1867..5254519235f1c444d464fe8707a42fb4f587fd80 100644
--- a/lisa-examples/src/main/scala/Example.scala
+++ b/lisa-examples/src/main/scala/Example.scala
@@ -15,10 +15,9 @@ object Example extends lisa.Main {
val step1 = have(P(x) ==> P(f(x))) by InstantiateForall
val step2 = have(P(f(x)) ==> P(f(f(x)))) by InstantiateForall
have(thesis) by Tautology.from(step1, step2)
- }
-
+ }
- //Example of set theoretic development
+ // Example of set theoretic development
/**
* Theorem --- The empty set is a subset of every set.
@@ -41,7 +40,7 @@ object Example extends lisa.Main {
val setWithElementNonEmpty = Theorem(
(y ∈ x) |- x =/= ∅
) {
- have ((x === ∅) |- !(y ∈ x)) by Substitute(x === ∅)(emptySetAxiom of (x := y))
+ have((x === ∅) |- !(y ∈ x)) by Substitute(x === ∅)(emptySetAxiom of (x := y))
}
/**
diff --git a/lisa-kernel/src/main/scala/lisa/kernel/proof/SCProofChecker.scala b/lisa-kernel/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
index 684c794a699db11c0009d9fcdf70f612d11bb0c0..08ea38d49097d97b98bf24b4c714e69523b60432 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
@@ -60,8 +60,8 @@ object SCProofChecker {
* Γ, Σ |- Δ, Π
*/
case Cut(b, t1, t2, phi) =>
- if (isSameSet(b.left + phi, ref(t1).left union ref(t2).left))
- if (isSameSet(b.right + phi, ref(t2).right union ref(t1).right))
+ if (isSameSet(b.left + phi, ref(t1).left union ref(t2).left) && (!contains(ref(t1).left, phi) || contains(b.left, phi)))
+ if (isSameSet(b.right + phi, ref(t2).right union ref(t1).right) && (!contains(ref(t2).right, phi) || contains(b.right, phi)))
if (contains(ref(t2).left, phi))
if (contains(ref(t1).right, phi))
SCValidProof(SCProof(step))
@@ -95,7 +95,11 @@ object SCProofChecker {
case LeftOr(b, t, disjuncts) =>
if (isSameSet(b.right, t.map(ref(_).right).fold(Set.empty)(_ union _))) {
val phiOrPsi = ConnectorFormula(Or, disjuncts)
- if (isSameSet(disjuncts.foldLeft(b.left)(_ + _), t.map(ref(_).left).fold(Set.empty)(_ union _) + phiOrPsi))
+ if (
+ t.zip(disjuncts).forall { case (s, phi) => isSubset(ref(s).left, b.left + phi) } &&
+ isSubset(b.left, t.map(ref(_).left).fold(Set.empty)(_ union _) + phiOrPsi)
+ )
+
SCValidProof(SCProof(step))
else SCInvalidProof(SCProof(step), 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(SCProof(step), Nil, s"Right-hand side of conclusion is not the union of the right-hand sides of the premises.")
@@ -192,7 +196,11 @@ object SCProofChecker {
case RightAnd(b, t, cunjuncts) =>
val phiAndPsi = ConnectorFormula(And, cunjuncts)
if (isSameSet(b.left, t.map(ref(_).left).fold(Set.empty)(_ union _)))
- if (isSameSet(cunjuncts.foldLeft(b.right)(_ + _), t.map(ref(_).right).fold(Set.empty)(_ union _) + phiAndPsi))
+ if (
+ t.zip(cunjuncts).forall { case (s, phi) => isSubset(ref(s).right, b.right + phi) } &&
+ isSubset(b.right, t.map(ref(_).right).fold(Set.empty)(_ union _) + phiAndPsi)
+ //isSameSet(cunjuncts.foldLeft(b.right)(_ + _), t.map(ref(_).right).fold(Set.empty)(_ union _) + phiAndPsi)
+ )
SCValidProof(SCProof(step))
else SCInvalidProof(SCProof(step), Nil, s"Right-hand side of conclusion + φ + ψ is not the same as the union of the right-hand sides of the premises φ∧ψ.")
else SCInvalidProof(SCProof(step), Nil, s"Left-hand side of conclusion is not the union of the left-hand sides of the premises.")
@@ -225,16 +233,20 @@ object SCProofChecker {
else SCInvalidProof(SCProof(step), Nil, "Right-hand side of conclusion + ψ must be same as right-hand side of premise + φ⇒ψ.")
else SCInvalidProof(SCProof(step), Nil, "Left-hand side of conclusion + psi must be same as left-hand side of premise.")
/*
- * Γ |- a⇒ψ, Δ Σ |- ψ⇒φ, Π
+ * Γ |- φ⇒ψ, Δ Σ |- ψ⇒φ, Π
* ----------------------------
- * Γ, Σ |- φ⇔b, Π, Δ
+ * Γ, Σ |- φ⇔ψ, Π, Δ
*/
case RightIff(b, t1, t2, phi, psi) =>
val phiImpPsi = ConnectorFormula(Implies, Seq(phi, psi))
val psiImpPhi = ConnectorFormula(Implies, Seq(psi, phi))
val phiIffPsi = ConnectorFormula(Iff, Seq(phi, psi))
if (isSameSet(b.left, ref(t1).left union ref(t2).left))
- if (isSameSet(b.right + phiImpPsi + psiImpPhi, ref(t1).right union ref(t2).right + phiIffPsi))
+ if (
+ isSubset(ref(t1).right, b.right + phiImpPsi) &&
+ isSubset(ref(t2).right, b.right + psiImpPhi) &&
+ isSubset(b.right, ref(t1).right union ref(t2).right + phiIffPsi)
+ )
SCValidProof(SCProof(step))
else SCInvalidProof(SCProof(step), 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(SCProof(step), Nil, s"Left-hand side of conclusion is not the union of the left-hand sides of the premises.")
diff --git a/lisa-utils/src/main/scala/lisa/prooflib/BasicStepTactic.scala b/lisa-utils/src/main/scala/lisa/prooflib/BasicStepTactic.scala
index 7e47d5ee673f7bd867b8a388727e3efc959780f2..8d066ea2a4a14a14549ddbe1209e7b08b53ec433 100644
--- a/lisa-utils/src/main/scala/lisa/prooflib/BasicStepTactic.scala
+++ b/lisa-utils/src/main/scala/lisa/prooflib/BasicStepTactic.scala
@@ -68,9 +68,9 @@ object BasicStepTactic {
proof.InvalidProofTactic("Right-hand side of first premise does not contain φ as claimed.")
else if (!K.contains(rightSequent.left, phiK))
proof.InvalidProofTactic("Left-hand side of second premise does not contain φ as claimed.")
- else if (!K.isSameSet(botK.left + phiK, leftSequent.left ++ rightSequent.left))
+ else if (!K.isSameSet(botK.left + phiK, leftSequent.left ++ rightSequent.left) || (leftSequent.left.contains(phiK) && !botK.left.contains(phiK)))
proof.InvalidProofTactic("Left-hand side of conclusion + φ is not the union of the left-hand sides of the premises.")
- else if (!K.isSameSet(botK.right + phiK, leftSequent.right ++ rightSequent.right))
+ else if (!K.isSameSet(botK.right + phiK, leftSequent.right ++ rightSequent.right) || (rightSequent.right.contains(phiK) && !botK.right.contains(phiK)))
proof.InvalidProofTactic("Right-hand side of conclusion + φ is not the union of the right-hand sides of the premises.")
else
proof.ValidProofTactic(bot, Seq(K.Cut(botK, -1, -2, phiK)), Seq(prem1, prem2))
@@ -166,7 +166,10 @@ object BasicStepTactic {
proof.InvalidProofTactic(s"Premises and disjuncts expected to be equal in number, but ${premises.length} premises and ${disjuncts.length} disjuncts received.")
else if (!K.isSameSet(botK.right, premiseSequents.map(_.right).reduce(_ union _)))
proof.InvalidProofTactic("Right-hand side of conclusion is not the union of the right-hand sides of the premises.")
- else if (!K.isSameSet(disjunctsK.foldLeft(botK.left)(_ + _), premiseSequents.map(_.left).reduce(_ union _) + disjunction))
+ else if (
+ premiseSequents.zip(disjunctsK).forall((sequent, disjunct) => K.isSubset(sequent.left, botK.left + disjunct)) // \forall i. premise_i.left \subset bot.left + phi_i
+ && !K.isSubset(botK.left, premiseSequents.map(_.left).reduce(_ union _) + disjunction) // bot.left \subseteq \bigcup premise_i.left
+ )
proof.InvalidProofTactic("Left-hand side of conclusion + disjuncts is not the same as the union of the left-hand sides of the premises + φ∨ψ.")
else
proof.ValidProofTactic(bot, Seq(K.LeftOr(botK, Range(-1, -premises.length - 1, -1), disjunctsK)), premises.toSeq)
@@ -561,7 +564,10 @@ object BasicStepTactic {
proof.InvalidProofTactic(s"Premises and conjuncts expected to be equal in number, but ${premises.length} premises and ${conjuncts.length} conjuncts received.")
else if (!K.isSameSet(botK.left, premiseSequents.map(_.left).reduce(_ union _)))
proof.InvalidProofTactic("Left-hand side of conclusion is not the union of the left-hand sides of the premises.")
- else if (!K.isSameSet(conjunctsK.foldLeft(botK.right)(_ + _), premiseSequents.map(_.right).reduce(_ union _) + conjunction))
+ else if (
+ premiseSequents.zip(conjunctsK).forall((sequent, conjunct) => K.isSubset(sequent.right, botK.right + conjunct)) // \forall i. premise_i.right \subset bot.right + phi_i
+ && !K.isSubset(botK.right, premiseSequents.map(_.right).reduce(_ union _) + conjunction) // bot.right \subseteq \bigcup premise_i.right
+ )
proof.InvalidProofTactic("Right-hand side of conclusion + conjuncts is not the same as the union of the right-hand sides of the premises + φ∧ψ....")
else
proof.ValidProofTactic(bot, Seq(K.RightAnd(botK, Range(-1, -premises.length - 1, -1), conjunctsK)), premises)
@@ -692,8 +698,21 @@ object BasicStepTactic {
if (!K.isSameSet(botK.left, leftSequent.left union rightSequent.left))
proof.InvalidProofTactic("Left-hand side of conclusion is not the union of the left-hand sides of the premises.")
- else if (!K.isSameSet(botK.right + impLeft + impRight, leftSequent.right union rightSequent.right + implication))
- proof.InvalidProofTactic("Right-hand side of conclusion + φ⇒ψ + ψ⇒φ is not the same as the union of the right-hand sides of the premises + φ⇔ψ.")
+ else if (!K.isSubset(leftSequent.right, botK.right + impLeft))
+ proof.InvalidProofTactic(
+ "Conclusion is missing the following formulas from the left premise: " + (leftSequent.right -- botK.right).map(f => s"[${FOLPrinter.prettyFormula(f)}]").reduce(_ ++ ", " ++ _)
+ )
+ else if (!K.isSubset(rightSequent.right, botK.right + impRight))
+ proof.InvalidProofTactic(
+ "Conclusion is missing the following formulas from the right premise: " + (rightSequent.right -- botK.right).map(f => s"[${FOLPrinter.prettyFormula(f)}]").reduce(_ ++ ", " ++ _)
+ )
+ else if (!K.isSubset(botK.right, leftSequent.right union rightSequent.right + implication))
+ proof.InvalidProofTactic(
+ "Conclusion has extraneous formulas apart from premises and implication: " ++ (botK.right
+ .removedAll(leftSequent.right union rightSequent.right + implication))
+ .map(f => s"[${FOLPrinter.prettyFormula(f)}]")
+ .reduce(_ ++ ", " ++ _)
+ )
else
proof.ValidProofTactic(bot, Seq(K.RightIff(botK, -1, -2, phiK, psiK)), Seq(prem1, prem2))
}
diff --git a/src/main/scala/lisa/automation/Tableau.scala b/src/main/scala/lisa/automation/Tableau.scala
index e5877d7344d7fa63333f79ea3d46d9fd2fddb76d..55a0dae91faab2db8567b0f25159934bb90b3341 100644
--- a/src/main/scala/lisa/automation/Tableau.scala
+++ b/src/main/scala/lisa/automation/Tableau.scala
@@ -363,7 +363,7 @@ object Tableau extends ProofTactic with ProofSequentTactic with ProofFactSequent
)
proof.map(proo =>
if needed == true then
- val sequent = ((proo.flatMap(_.bot.left).toSet -- list.map(_._2)) |- ()) +<< branch.beta.head
+ val sequent = ((proo.reverse.zip(list).flatMap((proof, bf) => proof.bot.left - bf._2).toSet + branch.beta.head) |- ())
(LeftOr(sequent, treversed.reverse, branch.beta.head.args) :: proo, treversed.size)
else (proo, proo.size - 1)
)