Cut check fix (#173)

epfl-lara · Aug 14, 2023 · aa5ba1f · aa5ba1f
1 parent ed4552c
commit aa5ba1f
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 6 deletions.
diff --git a/lisa-kernel/src/main/scala/lisa/kernel/proof/SCProofChecker.scala b/lisa-kernel/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
@@ -57,11 +57,11 @@ object SCProofChecker {
           /*
            *  Γ |- Δ, φ    φ, Σ |- Π
            * ------------------------
-           *       Γ, Σ |-Δ, Π
+           *       Γ, Σ |- Δ, Π
            */
           case Cut(b, t1, t2, phi) =>
-            if (isSameSet(b.left, ref(t1).left union ref(t2).left.filterNot(isSame(_, phi))))
-              if (isSameSet(b.right, ref(t2).right union ref(t1).right.filterNot(isSame(_, 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 (contains(ref(t2).left, phi))
                   if (contains(ref(t1).right, phi))
                     SCValidProof(SCProof(step))

diff --git a/lisa-utils/src/main/scala/lisa/prooflib/BasicStepTactic.scala b/lisa-utils/src/main/scala/lisa/prooflib/BasicStepTactic.scala
@@ -56,7 +56,7 @@ object BasicStepTactic {
    * <pre>
    *  Γ |- Δ, φ    φ, Σ |- Π
    * ------------------------
-   *       Γ, Σ |-Δ, Π
+   *       Γ, Σ |- Δ, Π
    * </pre>
    */
   object Cut extends ProofTactic {
@@ -68,9 +68,9 @@ object BasicStepTactic {
         proof.InvalidProofTactic("Right-hand side of first premise does not contain φ as claimed.")
       else if (!contains(rightSequent.left, phi))
         proof.InvalidProofTactic("Left-hand side of second premise does not contain φ as claimed.")
-      else if (!isSameSet(bot.left, leftSequent.left ++ rightSequent.left.filterNot(isSame(_, phi))))
+      else if (!isSameSet(bot.left + phi, leftSequent.left ++ rightSequent.left))
         proof.InvalidProofTactic("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))
+      else if (!isSameSet(bot.right + phi, leftSequent.right ++ rightSequent.right))
         proof.InvalidProofTactic("Right-hand side of conclusion + φ is not the union of the right-hand sides of the premises.")
       else
         proof.ValidProofTactic(Seq(SC.Cut(bot, -1, -2, phi)), Seq(prem1, prem2))