diff --git a/src/main/scala/lisa/kernel/proof/SCProofChecker.scala b/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
index bb475952dff29893a69c8f56eb2d8b72469f5868..372699abbe43d3a6f84c9d4e505cfc843ca599d2 100644
--- a/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
+++ b/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
@@ -1,7 +1,8 @@
package lisa.kernel.proof
-import lisa.kernel.fol.FOL._
-import lisa.kernel.proof.SequentCalculus._
+import lisa.kernel.Printer
+import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.SequentCalculus.*
object SCProofChecker {
@@ -27,9 +28,9 @@ object SCProofChecker {
val r: (Boolean, List[Int], String) =
if (false_premise.nonEmpty)
- return (false, Nil, "A step can't refer to a step with a higher or equal number as a premise.")
+ return (false, Nil, s"Step no $no can't refer to higher number ${false_premise.get} as a premise.")
if (false_premise2.nonEmpty)
- return (false, Nil, "A step can't refer to a step with a lower number than minus the number of imports.")
+ return (false, Nil, s"A step can't refer to step ${false_premise2.get}, imports only contains ${importsSize.get} elements.")
else step match {
/*
* Γ |- Δ
@@ -57,8 +58,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 (ref(t2).left.contains(phi))
- if (ref(t1).right.contains(phi))
+ if (contains(ref(t2).left, phi))
+ if (contains(ref(t1).right, phi))
(true, Nil, "")
else (false, Nil, s"Right-hand side of first premise does not contain φ as claimed.")
else (false, Nil, s"Left-hand side of second premise does not contain φ as claimed.")
@@ -322,7 +323,7 @@ object SCProofChecker {
phi match {
case PredicateFormula(`equality`, Seq(left, right)) =>
if (isSame(left, right))
- if (b.right.contains(phi))
+ if (contains(b.right, phi))
(true, Nil, "")
else (false, Nil, s"Right-Hand side of conclusion does not contain φ")
else (false, Nil, s"φ is not an instance of reflexivity.")
diff --git a/src/main/scala/proven/ElementsOfSetTheory.scala b/src/main/scala/proven/ElementsOfSetTheory.scala
index a1bf44ded463ff24e926edbab8169cf12ee40eae..532affc320fa833ab89d643aa76a76450ef347ed 100644
--- a/src/main/scala/proven/ElementsOfSetTheory.scala
+++ b/src/main/scala/proven/ElementsOfSetTheory.scala
@@ -2,11 +2,13 @@ package proven
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.SequentCalculus.*
import lisa.KernelHelpers.{*, given}
+import lisa.kernel.Printer
import proven.tactics.ProofTactics.*
import proven.tactics.Destructors.*
import lisa.settheory.AxiomaticSetTheory.*
+
import scala.collection.immutable.SortedSet
-import lisa.kernel.proof.SCProof
+import lisa.kernel.proof.{SCProof, SCProofChecker}
import scala.collection.immutable
@@ -64,25 +66,25 @@ object ElementsOfSetTheory {
val pxy = pair(x, y)
val pxy1 = pair(x1, y1)
val zexy = (z === x) \/ (z === y)
- val p0 = SCSubproof {
+ val p0 = SCSubproof({
val p0 = SCSubproof({
val zf = in(z, pxy)
val p1_0 = hypothesis(zf)
val p1_1 = RightImplies(emptySeq +> (zf ==> zf), 0, zf, zf)
val p1_2 = RightIff(emptySeq +> (zf <=> zf), 1, 1, zf, zf) // |- (z in {x,y} <=> z in {x,y})
val p1_3 = RightSubstEq(emptySeq +< (pxy === pxy1) +> (zf <=> in(z, pxy1)), 2, pxy, pxy1, zf <=> in(z, g()), g)
- SCProof(p1_0, p1_1, p1_2, p1_3)
- }, display = false) // ({x,y}={x',y'}) |- ((z∈{x,y})↔(z∈{x',y'}))
+ SCProof(IndexedSeq(p1_0, p1_1, p1_2, p1_3), IndexedSeq(()|-pairAxiom))
+ }, Seq(-1), display = true) // ({x,y}={x',y'}) |- ((z∈{x,y})↔(z∈{x',y'}))
val p1 = SCSubproof({
val p1_0 = Rewrite(()|-pairAxiom, -1) // |- ∀∀∀((z$1∈{x$3,y$2})↔((x$3=z$1)∨(y$2=z$1)))
val p1_1 = instantiateForall(SCProof(IndexedSeq(p1_0), IndexedSeq(()|-pairAxiom)), x, y, z)
p1_1
- }, display = false) // |- (z in {x,y}) <=> (z=x \/ z=y)
+ }, Seq(-1), display = true) // |- (z in {x,y}) <=> (z=x \/ z=y)
val p2 = SCSubproof({
val p2_0 = Rewrite(()|-pairAxiom, -1) // |- ∀∀∀((z$1∈{x$3,y$2})↔((x$3=z$1)∨(y$2=z$1)))
val p2_1 = instantiateForall(SCProof(IndexedSeq(p2_0), IndexedSeq(()|-pairAxiom)), x1, y1, z)
p2_1
- }, display = false) // |- (z in {x',y'}) <=> (z=x' \/ z=y')
+ }, Seq(-1), display = true) // |- (z in {x',y'}) <=> (z=x' \/ z=y')
val p3 = RightSubstEq(
emptySeq +< (pxy === pxy1) +> (in(z, pxy1) <=> ((z === x) \/ (z === y))), 1, pxy, pxy1, in(z, g()) <=> ((z === x) \/ (z === y)), g
) // ({x,y}={x',y'}) |- ((z∈{x',y'})↔((z=x)∨(z=y)))
@@ -95,8 +97,8 @@ object ElementsOfSetTheory {
h
) // ((z∈{x',y'})↔((x'=z)∨(y'=z))), ({x,y}={x',y'}) |- (((z=x)∨(z=y))↔((z=x')∨(z=y')))
val p5 = Cut(emptySeq ++< p3.bot ++> p4.bot, 2, 4, p2.bot.right.head)
- SCProof(p0, p1, p2, p3, p4, p5)
- } // ({x,y}={x',y'}) |- (((z=x)∨(z=y))↔((z=x')∨(z=y')))
+ SCProof(IndexedSeq(p0, p1, p2, p3, p4, p5), IndexedSeq(()|-pairAxiom))
+ }, Seq(-1)) // ({x,y}={x',y'}) |- (((z=x)∨(z=y))↔((z=x')∨(z=y')))
val p1 = SCSubproof(
SCProof(byCase(x === x1)(
@@ -181,9 +183,9 @@ object ElementsOfSetTheory {
val rd0_1_1 = instantiateForall(SCProof(IndexedSeq(pd0_1_0), IndexedSeq(pd0_m1.bot)), x1) // ({x,y}={x',y'}) |- (x'=x \/ x'=y) <=> (x'=x' \/ x'=y')
rd0_1_1
}, IndexedSeq(-1)) // ({x,y}={x',y'}) |- (x'=x \/ x'=y) <=> (x'=x' \/ x'=y')
- val rd0_2 = byEquiv(pd0_1.bot.right.head, pd0_0.bot.right.head)(pd0_1, pd0_0)
- val pd0_3 = SCSubproof(SCProof(rd0_2.steps, IndexedSeq(pd0_m1.bot)), IndexedSeq(-1)) // ({x,y}={x',y'}) |- (x=x' \/ y=x')
- destructRightOr(SCProof(IndexedSeq(pd0_0, pd0_1, pd0_3), IndexedSeq(pd0_m1.bot)), x === x1, y === x1) // ({x,y}={x',y'}) |- x=x', y=x'
+ val pd0_2 = RightSubstIff(pd0_1.bot.right |- ((x1===x) \/ (x1===y)), 0,(x1===x) \/ (x1===y), (x1===x1) \/ (x1===y1),SchematicPredicateLabel("h", 0)(), SchematicPredicateLabel("h", 0) ) // (x'=x \/ x'=y) <=> (x'=x' \/ x'=y') |- (x'=x \/ x'=y)
+ val pd0_3 = Cut(pd0_1.bot.left |- pd0_2.bot.right, 1,2, pd0_1.bot.right.head) // ({x,y}={x',y'}) |- (x=x' \/ y=x')
+ destructRightOr(SCProof(IndexedSeq(pd0_0, pd0_1, pd0_2, pd0_3), IndexedSeq(pd0_m1.bot)), x === x1, y === x1) // ({x,y}={x',y'}) |- x=x', y=x'
}, IndexedSeq(-1)) // ({x,y}={x',y'}) |- x=x', y=x' --
val pd1 = SCSubproof({
val pd1_m1 = pdm1
@@ -213,7 +215,7 @@ object ElementsOfSetTheory {
) // ({x,y}={x',y'}) |- (x=x' /\ y=y')\/(x=y' /\ y=x')
val p2 = RightImplies(emptySeq +> (p1.bot.left.head ==> p1.bot.right.head), 1, p1.bot.left.head, p1.bot.right.head) // |- ({x,y}={x',y'}) ==> (x=x' /\ y=y')\/(x=y' /\ y=x')
- generalizeToForall(SCProof(p0, p1, p2), x, y, x1, y1)
+ generalizeToForall(SCProof(IndexedSeq(p0, p1, p2), IndexedSeq(()|-pairAxiom)), x, y, x1, y1)
} // |- ∀∀∀∀(({x$4,y$3}={x'$2,y'$1})⇒(((y'$1=y$3)∧(x'$2=x$4))∨((x$4=y'$1)∧(y$3=x'$2))))
diff --git a/src/main/scala/proven/tactics/Destructors.scala b/src/main/scala/proven/tactics/Destructors.scala
index 12c080e88a76dbc8b29650611122900c1e9ca9ea..9bec6109136a16befdc89f2278ef76cc0c44a78f 100644
--- a/src/main/scala/proven/tactics/Destructors.scala
+++ b/src/main/scala/proven/tactics/Destructors.scala
@@ -8,11 +8,12 @@ import lisa.kernel.proof.SCProof
object Destructors {
def destructRightOr(p: SCProof, a: Formula, b: Formula): SCProof = {
- require(contains(p.conclusion.right, a \/ b))
+ val mat = p.conclusion.right.find(f => isSame(f, a \/ b))
+ require(mat.nonEmpty)
val p0 = hypothesis(a)
val p1 = hypothesis(b)
val p2 = LeftOr(emptySeq +< (a \/ b) +> a +> b, Seq(p.length, p.length + 1), Seq(a, b))
- val p3 = Cut(p.conclusion -> (a \/ b) +> a +> b, p.length - 1, p.length + 2, a \/ b)
+ val p3 = Cut(p.conclusion -> mat.get +> a +> b, p.length - 1, p.length + 2, a \/ b)
p withNewSteps IndexedSeq(p0, p1, p2, p3)
}
def destructRightAnd(p: SCProof, f: Formula, g: Formula): SCProof = {
diff --git a/src/main/scala/proven/tactics/ProofTactics.scala b/src/main/scala/proven/tactics/ProofTactics.scala
index 85c576fc716c2b8d25dcabfb14bb22f54eb81590..d7d087186f71eb88c570d1867910f595e36e56ae 100644
--- a/src/main/scala/proven/tactics/ProofTactics.scala
+++ b/src/main/scala/proven/tactics/ProofTactics.scala
@@ -81,7 +81,6 @@ object ProofTactics {
val fo = forall(x, prev._2)
(prev._1 appended RightForall(emptySeq +> fo, prev._3, prev._2, x), fo, prev._3 + 1)
})
- //val p6 = MakeFunctionDefinition(fdef._1.size - 1, f, args, x, x === t)
SCProof(fdef._1 )
}
// p1 is a proof of psi given phi, p2 is a proof of psi given !phi
diff --git a/src/test/scala/lisa/kernel/FolTests.scala b/src/test/scala/lisa/kernel/FolTests.scala
index c5f3b6f3de7543c1f47ddf7a4fe628919259232e..70ae8ea2502c808468a7b060682388a4385ac71d 100644
--- a/src/test/scala/lisa/kernel/FolTests.scala
+++ b/src/test/scala/lisa/kernel/FolTests.scala
@@ -120,7 +120,7 @@ class FolTests extends AnyFunSuite {
test("Fresh variables should be fresh") {
val y1 = VariableLabel(freshId(equ(VariableTerm(x), VariableTerm(x)).freeVariables.map(_.name), x.name))
- //println(x1, y1)
+
assert(!isSame(x, y1))
}
}
\ No newline at end of file
diff --git a/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala b/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala
index efdbd45fa6a0d46617264e4882f3eaaa7b6b95f0..413c19c457c0175e9a637499a1d8360ada471d70 100644
--- a/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala
+++ b/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala
@@ -5,13 +5,14 @@ import lisa.settheory.AxiomaticSetTheory.*
import test.ProofCheckerSuite
import proven.tactics.ProofTactics
import lisa.kernel.proof.SCProof
+import proven.ElementsOfSetTheory.*
+import lisa.kernel.proof.SequentCalculus.Sequent
+import lisa.kernel.fol.FOL.*
+import lisa.KernelHelpers.{*, given}
+import lisa.kernel.proof.SequentCalculus.*
class ElementsOfSetTheoryTests extends ProofCheckerSuite {
- import proven.ElementsOfSetTheory.*
- import lisa.kernel.proof.SequentCalculus.Sequent
- import lisa.kernel.fol.FOL.*
- import lisa.KernelHelpers.{*, given}
- import lisa.kernel.proof.SequentCalculus.*
+
test("Verification of the proof of symmetry of the pair") {
checkProof(proofUnorderedPairSymmetry, emptySeq +> forall(vl, forall(ul, pair(u, v) === pair(v, u))))
@@ -20,7 +21,7 @@ class ElementsOfSetTheoryTests extends ProofCheckerSuite {
test("Verification of the proof of deconstruction of the unordered pair") {
checkProof(proofUnorderedPairDeconstruction, emptySeq +>
forall(sl, forall(tl, forall(ul, forall(vl,
- (pair(s, t) === pair(xp, v)) ==>
+ (pair(s, t) === pair(u, v)) ==>
(((VariableTerm(v) === t) /\ (VariableTerm(u) === s)) \/ ((VariableTerm(s) === v) /\ (VariableTerm(t) === u)))))))
)
}
@@ -29,11 +30,11 @@ class ElementsOfSetTheoryTests extends ProofCheckerSuite {
val singletonSetEqualityProof: SCProof = {
val t0 = SCSubproof({
val t0 = Rewrite(()|-pairAxiom, -1)
- val p0 = ProofTactics.instantiateForall(SCProof(IndexedSeq(t0), IndexedSeq(()|-pairAxiom)), t0.bot.right.head, y)
- val p1 = ProofTactics.instantiateForall(p0, p0.conclusion.right.head, y)
- val p2:SCProof = ProofTactics.instantiateForall(p1, p1.conclusion.right.head, x)
+ val p0 = ProofTactics.instantiateForall(SCProof(IndexedSeq(t0), IndexedSeq(()|-pairAxiom)), t0.bot.right.head, v)
+ val p1 = ProofTactics.instantiateForall(p0, p0.conclusion.right.head, v)
+ val p2:SCProof = ProofTactics.instantiateForall(p1, p1.conclusion.right.head, u)
p2
- } )
+ }, IndexedSeq(-1), display=false )
// |- f <=> (f \/ f)
def selfIffOr(f: Formula): SCSubproof = SCSubproof({
@@ -44,33 +45,26 @@ class ElementsOfSetTheoryTests extends ProofCheckerSuite {
val t4 = RightImplies(Sequent(Set(), Set((f \/ f) ==> f)), 2, f \/ f, f)
val t5 = RightIff(Sequent(Set(), Set(f <=> (f \/ f))), 3, 4, f, f \/ f)
SCProof(IndexedSeq(t0, t1, t2, t3, t4, t5))
- })
-
- val t1 = selfIffOr(y === x)
-
- val xy = x === x
+ }, display=false)
+ val t1 = selfIffOr(u === v)
+ val xy = u === v
val h = SchematicPredicateLabel("h", 0)
- val t2 = RightSubstIff(Sequent(Set((xy \/ xy) <=> xy), Set(xy <=> in(x, pair(y, y)))), 0,
- (y === x) \/ (y === x),
- y === x,
- in(x, pair(y, y)) <=> PredicateFormula(h, Seq.empty),
+ val t2 = RightSubstIff(Sequent(Set((xy \/ xy) <=> xy), Set(xy <=> in(u, pair(v, v)))), 0,
+ (v === u) \/ (v === u),
+ v === u,
+ in(u, pair(v, v)) <=> PredicateFormula(h, Seq.empty),
h)
- val t3 = Cut(Sequent(Set(), Set(xy <=> in(x, pair(y, y)))), 1, 2, (xy \/ xy) <=> xy)
+ val t3 = Cut(Sequent(Set(), Set(xy <=> in(u, pair(v, v)))), 1, 2, (xy \/ xy) <=> xy)
- val p0 = SCProof(IndexedSeq(t0, t1, t2, t3))
+ val p0 = SCProof(IndexedSeq(t0, t1, t2, t3), IndexedSeq(() |- pairAxiom))
- ProofTactics.generalizeToForall(ProofTactics.generalizeToForall(p0, ul), vl)
+ ProofTactics.generalizeToForall(ProofTactics.generalizeToForall(p0, vl), ul)
}
test("Singleton set equality") {
- checkProof(singletonSetEqualityProof, emptySeq +> forall(vl, forall(ul, (u === v) <=> in(u, pair(v, v)))))
+ checkProof(singletonSetEqualityProof, emptySeq +> forall(u, forall(v, (u === v) <=> in(u, pair(v, v)))))
}
- val proofSingletonDefinition: SCProof = ProofTactics.simpleFunctionDefinition(singleton, pair(u, u), Seq(ul))
-
- test("Verify singleton set definition") {
- checkProof(proofSingletonDefinition)
- }
}