From 4f19acdf4e13fcb4afba82a460d1eb0765096ff8 Mon Sep 17 00:00:00 2001
From: Katja Goltsova <katja.goltsova@protonmail.com>
Date: Sun, 17 Jul 2022 00:50:48 +0200
Subject: [PATCH 1/2] Add tests for formula and set removals from sequents
---
.../scala/lisa/utils/SequentUtilsTest.scala | 56 +++++++++++++++++++
1 file changed, 56 insertions(+)
create mode 100644 lisa-utils/src/test/scala/lisa/utils/SequentUtilsTest.scala
diff --git a/lisa-utils/src/test/scala/lisa/utils/SequentUtilsTest.scala b/lisa-utils/src/test/scala/lisa/utils/SequentUtilsTest.scala
new file mode 100644
index 00000000..846b131b
--- /dev/null
+++ b/lisa-utils/src/test/scala/lisa/utils/SequentUtilsTest.scala
@@ -0,0 +1,56 @@
+package lisa.utils
+
+import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.SequentCalculus.Sequent
+import lisa.kernel.proof.SequentCalculus.isSameSequent
+import lisa.test.ProofCheckerSuite
+import lisa.utils.Helpers.*
+
+import scala.collection.immutable.Set
+
+class SequentUtilsTest extends ProofCheckerSuite {
+ val simpleSequent: Sequent = s === t |- s === t
+ val sequent: Sequent = Set(s === t, t === u) |- Set(s === t, s === u)
+ val emptySequent: Sequent = () |- ()
+
+ test("left remove formula") {
+ val leftFormula = simpleSequent.left.head
+ // plain removal
+ assert((simpleSequent -< leftFormula) === (() |- simpleSequent.right))
+ // isSame removal
+ val sameFormula = leftFormula /\ (s === s)
+ assert(!(sameFormula == leftFormula))
+ assert(isSame(leftFormula, sameFormula))
+ assert((simpleSequent -< sameFormula) === (simpleSequent -< leftFormula))
+ }
+
+ test("right remove formula") {
+ val rightFormula = simpleSequent.right.head
+ // plain removal
+ assert((simpleSequent -> rightFormula) === (simpleSequent.left |- ()))
+ // isSame removal
+ val sameFormula = rightFormula /\ (s === s)
+ assert(!(sameFormula == rightFormula))
+ assert(isSame(rightFormula, sameFormula))
+ assert((simpleSequent -> sameFormula) === (simpleSequent -> rightFormula))
+ }
+
+ test("left remove set") {
+ assert(sequent --< sequent === (() |- sequent.right))
+ val sameLeft = Sequent(sequent.left.map(_ /\ (u === u)), sequent.right)
+ assert((sequent --< sameLeft) === (() |- sequent.right))
+ }
+
+ test("right remove set") {
+ assert((sequent --> sequent) === (sequent.left |- ()))
+ val sameRight = Sequent(sequent.left, sequent.right.map(_ /\ (u === u)))
+ assert(!(sequent.right === sameRight))
+ assert(isSameSet(sequent.right, sameRight.right))
+ assert(sequent --> sameRight === (sequent.left |- ()))
+ }
+
+ test("sequent remove sequent") {
+ val equivalentSequent = Set((s === t) /\ (s === s), t === u) |- Set(s === t, (s === u) /\ (u === u))
+ assert(sequent -- equivalentSequent === emptySequent)
+ }
+}
--
GitLab
From da641136a2f0767e39a073669f44d2a70f3e454c Mon Sep 17 00:00:00 2001
From: Katja Goltsova <katja.goltsova@protonmail.com>
Date: Mon, 18 Jul 2022 10:08:08 +0200
Subject: [PATCH 2/2] When removing a formula from a sequent, account for
isSame formulas
First try removing the exact formula, if that fails, remove all isSame formulas.
This increases the runtime of the removal operation to O(n).
---
.../src/main/scala/lisa/utils/KernelHelpers.scala | 14 +++++++++-----
1 file changed, 9 insertions(+), 5 deletions(-)
diff --git a/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala b/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
index e372a02e..94f5fb0e 100644
--- a/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
@@ -98,17 +98,21 @@ trait KernelHelpers {
val emptySeq: Sequent = Sequent(Set.empty, Set.empty)
+ private def removeFormula(s: Set[Formula], f: Formula): Set[Formula] = {
+ if (s.contains(f)) s - f else s.filterNot(isSame(_, f))
+ }
+
extension (s: Sequent) {
infix def +<(f: Formula): Sequent = s.copy(left = s.left + f)
- infix def -<(f: Formula): Sequent = s.copy(left = s.left - f)
+ infix def -<(f: Formula): Sequent = s.copy(left = removeFormula(s.left, f))
infix def +>(f: Formula): Sequent = s.copy(right = s.right + f)
- infix def ->(f: Formula): Sequent = s.copy(right = s.right - f)
+ infix def ->(f: Formula): Sequent = s.copy(right = removeFormula(s.right, f))
infix def ++<(s1: Sequent): Sequent = s.copy(left = s.left ++ s1.left)
- infix def --<(s1: Sequent): Sequent = s.copy(left = s.left -- s1.left)
+ infix def --<(s1: Sequent): Sequent = s.copy(left = s1.left.foldLeft(s.left)(removeFormula))
infix def ++>(s1: Sequent): Sequent = s.copy(right = s.right ++ s1.right)
- infix def -->(s1: Sequent): Sequent = s.copy(right = s.right -- s1.right)
+ infix def -->(s1: Sequent): Sequent = s.copy(right = s1.right.foldLeft(s.right)(removeFormula))
infix def ++(s1: Sequent): Sequent = s.copy(left = s.left ++ s1.left, right = s.right ++ s1.right)
- infix def --(s1: Sequent): Sequent = s.copy(left = s.left -- s1.left, right = s.right -- s1.right)
+ infix def --(s1: Sequent): Sequent = s.copy(left = s1.left.foldLeft(s.left)(removeFormula), right = s1.right.foldLeft(s.right)(removeFormula))
}
/**
--
GitLab