From aa5ba1fd4e0f0525c0bf9ede66b366607961ad76 Mon Sep 17 00:00:00 2001
From: Sankalp Gambhir <sankalp.gambhir47@gmail.com>
Date: Mon, 14 Aug 2023 14:13:51 +0200
Subject: [PATCH] Cut check fix (#173)

---
 .../src/main/scala/lisa/kernel/proof/SCProofChecker.scala   | 6 +++---
 .../src/main/scala/lisa/prooflib/BasicStepTactic.scala      | 6 +++---
 2 files changed, 6 insertions(+), 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
index b15632b5..66116f85 100644
--- 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
index e60ea6e1..6c6ea28e 100644
--- 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))