Proof checker fix (#183)

* super condensed propositional tableau with eqChecker data

* work on princess

* Start working on princess-lisa

* Continued work on princess integration

* more tinkering

* trying some tableau implementation

* continue work on ATP

* Mostly working, problem with test 14 (with functions).

* test 14 does pass (make variables names unique)

* improvements on Tableau

* Proof production is completely correct!

* pruning implemented

* Tableau integreated as a tactic. Working on all theorems of the Quantifiers file, except for those with equality

* integrating tests

* Integrated tests

* clean some files

* scalafix, scalafmt

* fix unsoundness in Cut, LeftOr, RightAnd and RightIff proof checking. Correct Tableau prover accordingly.

* Adapt cut proof checking

* Adapt LeftOr proof checking

* Adapt RightAnd proof checking

* Adapting RightIff proof checking and better reporting

* scalafmt

* scalafix, scalafmt

---------

Co-authored-by: Sankalp Gambhir <[email protected]>

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))
   }
 
   /**

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.")

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))
     }

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)
       )