diff --git a/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala b/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
index 4a6d0501d35c86330cb1d08f377fdbcaf6bb640c..722d2c1f45cb72a48c0acee966888fc6e279657c 100644
--- a/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
+++ b/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
@@ -14,11 +14,17 @@ class EquivalenceCheckerTests extends AnyFunSuite {
private val verbose = false // Turn this on to print all tested couples
def checkEquivalence(left: Formula, right: Formula): Unit = {
- assert(isSame(left, right), s"Couldn't prove the equivalence between ${Printer.prettyFormula(left)} and ${Printer.prettyFormula(right)}\nLeft tree: ${left}\nRight tree: ${right}")
+ assert(
+ isSame(left, right),
+ s"Couldn't prove the equivalence between ${Printer.prettyFormula(left)} and ${Printer.prettyFormula(right)}\nLeft tree: ${left}\nRight tree: ${right}"
+ )
}
def checkNonEquivalence(left: Formula, right: Formula): Unit = {
- assert(!isSame(left, right), s"Expected the checker to not be able to show equivalence between ${Printer.prettyFormula(left)} and ${Printer.prettyFormula(right)}\nLeft tree: ${left}\nRight tree: ${right}")
+ assert(
+ !isSame(left, right),
+ s"Expected the checker to not be able to show equivalence between ${Printer.prettyFormula(left)} and ${Printer.prettyFormula(right)}\nLeft tree: ${left}\nRight tree: ${right}"
+ )
}
def nameGenerator(): () => String = {
@@ -59,10 +65,10 @@ class EquivalenceCheckerTests extends AnyFunSuite {
def generate(p: Double): Formula = {
val q = random.nextDouble()
- if(q >= p) {
+ if (q >= p) {
// Leaf
val name =
- if(connectors.isEmpty || random.nextDouble() <= 0.75) { // TODO adapt
+ if (connectors.isEmpty || random.nextDouble() <= 0.75) { // TODO adapt
// New name
val id = nextConnectorName()
connectors += id
@@ -75,16 +81,16 @@ class EquivalenceCheckerTests extends AnyFunSuite {
} else {
// Branch
val nextP = p * c
- if(random.nextDouble() < 0.9) {
+ if (random.nextDouble() < 0.9) {
// Connector
val binaries = Seq(and, or, iff, implies)
- if(random.nextInt(binaries.size + 1) > 0) {
+ if (random.nextInt(binaries.size + 1) > 0) {
// Binary
val binary = binaries(random.nextInt(binaries.size))
val (l, r) = {
val p1 = nextP * nextP
val (f1, f2) = (generate(p1), generate(p1))
- if(random.nextBoolean()) (f1, f2) else (f2, f1)
+ if (random.nextBoolean()) (f1, f2) else (f2, f1)
}
(binary(l, r))
} else {
@@ -112,16 +118,16 @@ class EquivalenceCheckerTests extends AnyFunSuite {
val cases = generatorToTestcases(generator())(random)
cases.foreach { (left, right) =>
// For completeness we also test symmetry
- if(equivalent) {
+ if (equivalent) {
checkEquivalence(left, right)
checkEquivalence(right, left)
- if(verbose) {
+ if (verbose) {
println(s"${Printer.prettyFormula(left)} <==> ${Printer.prettyFormula(right)}")
}
} else {
checkNonEquivalence(left, right)
checkNonEquivalence(right, left)
- if(verbose) {
+ if (verbose) {
println(s"${Printer.prettyFormula(left)} <!=> ${Printer.prettyFormula(right)}")
}
}
@@ -129,7 +135,7 @@ class EquivalenceCheckerTests extends AnyFunSuite {
}
def testWithRepeat(generator: () => () => Formula, n: Int): Unit = {
- for(i <- 0 until n) {
+ for (i <- 0 until n) {
testWith(generator)
}
}
@@ -156,7 +162,7 @@ class EquivalenceCheckerTests extends AnyFunSuite {
def testcases(f: (Formula, Formula, Formula, Formula) => Random => Seq[(Formula, Formula)], equivalent: Boolean): Unit =
testcasesAny(generator => r => f(generator(), generator(), generator(), generator())(r), equivalent)
- def repeatApply[T](n: Int)(f: T => T)(initial: T): T = if(n > 0) repeatApply(n - 1)(f)(f(initial)) else initial
+ def repeatApply[T](n: Int)(f: T => T)(initial: T): T = if (n > 0) repeatApply(n - 1)(f)(f(initial)) else initial
def commutativeShuffle(iterations: Int)(random: Random)(f: Formula): Formula = {
def transform(f: Formula): Formula = f match {
case PredicateFormula(label, args) => f
@@ -175,13 +181,13 @@ class EquivalenceCheckerTests extends AnyFunSuite {
case PredicateFormula(label, args) => f
// Simple for now, assume binary operations
case ConnectorFormula(label1 @ (And | Or), Seq(ConnectorFormula(label2, Seq(a1, a2)), a3)) if label1 == label2 =>
- if(random.nextBoolean()) {
+ if (random.nextBoolean()) {
ConnectorFormula(label1, Seq(a1, ConnectorFormula(label2, Seq(a2, a3))))
} else {
f
}
case ConnectorFormula(label1 @ (And | Or), Seq(a1, ConnectorFormula(label2, Seq(a2, a3)))) if label1 == label2 =>
- if(random.nextBoolean()) {
+ if (random.nextBoolean()) {
ConnectorFormula(label1, Seq(ConnectorFormula(label2, Seq(a1, a2)), a3))
} else {
f
@@ -193,12 +199,13 @@ class EquivalenceCheckerTests extends AnyFunSuite {
}
def addDoubleNegations(p: Double)(random: Random)(f: Formula): Formula = {
def transform(f: Formula): Formula =
- if(random.nextDouble() < p) neg(neg(transform(f)))
- else f match {
- case _: PredicateFormula => f
- case ConnectorFormula(label, args) => ConnectorFormula(label, args.map(transform))
- case BinderFormula(label, bound, inner) => BinderFormula(label, bound, transform(inner))
- }
+ if (random.nextDouble() < p) neg(neg(transform(f)))
+ else
+ f match {
+ case _: PredicateFormula => f
+ case ConnectorFormula(label, args) => ConnectorFormula(label, args.map(transform))
+ case BinderFormula(label, bound, inner) => BinderFormula(label, bound, transform(inner))
+ }
transform(f)
}
def addDeMorgans(p: Double)(random: Random)(f: Formula): Formula = {
@@ -222,81 +229,136 @@ class EquivalenceCheckerTests extends AnyFunSuite {
}
test("Commutativity (root with equal leaves)") {
- testcases((a, b) => _ => Seq(
- and(a, b) -> and(b, a),
- or(a, b) -> or(b, a),
- iff(a, b) -> iff(b, a),
- ), equivalent = true)
+ testcases(
+ (a, b) =>
+ _ =>
+ Seq(
+ and(a, b) -> and(b, a),
+ or(a, b) -> or(b, a),
+ iff(a, b) -> iff(b, a)
+ ),
+ equivalent = true
+ )
}
test("Associativity (root with equal leaves)") {
- testcases((a, b, c, d) => _ => Seq(
- and(and(a, b), c) -> and(a, and(b, c)),
- or(or(a, b), c) -> or(a, or(b, c)),
- ), equivalent = true)
+ testcases(
+ (a, b, c, d) =>
+ _ =>
+ Seq(
+ and(and(a, b), c) -> and(a, and(b, c)),
+ or(or(a, b), c) -> or(a, or(b, c))
+ ),
+ equivalent = true
+ )
}
test("Commutativity (general)") {
- testcases((a, b) => random => Seq(
- a -> commutativeShuffle(15)(random)(a)
- ), equivalent = true)
+ testcases(
+ (a, b) =>
+ random =>
+ Seq(
+ a -> commutativeShuffle(15)(random)(a)
+ ),
+ equivalent = true
+ )
}
test("Associativity (general)") {
- testcases((a, b) => random => Seq(
- a -> associativeShuffle(15)(random)(a)
- ), equivalent = true)
+ testcases(
+ (a, b) =>
+ random =>
+ Seq(
+ a -> associativeShuffle(15)(random)(a)
+ ),
+ equivalent = true
+ )
}
test("Commutativity and associativity (general)") {
- testcases((a, b) => random => Seq(
- a -> repeatApply(15)(commutativeShuffle(1)(random).andThen(associativeShuffle(1)(random)))(a)
- ), equivalent = true)
+ testcases(
+ (a, b) =>
+ random =>
+ Seq(
+ a -> repeatApply(15)(commutativeShuffle(1)(random).andThen(associativeShuffle(1)(random)))(a)
+ ),
+ equivalent = true
+ )
}
test("Double negation (root with equal leaf)") {
- testcases(a => _ => Seq(
- a -> neg(neg(a)),
- neg(a) -> neg(neg(neg(a))),
- a -> neg(neg(neg(neg(a)))),
- ), equivalent = true)
+ testcases(
+ a =>
+ _ =>
+ Seq(
+ a -> neg(neg(a)),
+ neg(a) -> neg(neg(neg(a))),
+ a -> neg(neg(neg(neg(a))))
+ ),
+ equivalent = true
+ )
}
test("Double negation (general)") {
val p = 0.25
- testcases(a => random => Seq(
- addDoubleNegations(p)(random)(a) -> addDoubleNegations(p)(random)(a),
- ), equivalent = true)
+ testcases(
+ a =>
+ random =>
+ Seq(
+ addDoubleNegations(p)(random)(a) -> addDoubleNegations(p)(random)(a)
+ ),
+ equivalent = true
+ )
}
test("De Morgan's law (root)") {
- testcases((a, b) => random => Seq(
- and(a, b) -> neg(or(neg(a), neg(b))),
- or(a, b) -> neg(and(neg(a), neg(b))),
- ), equivalent = true)
+ testcases(
+ (a, b) =>
+ random =>
+ Seq(
+ and(a, b) -> neg(or(neg(a), neg(b))),
+ or(a, b) -> neg(and(neg(a), neg(b)))
+ ),
+ equivalent = true
+ )
}
test("De Morgan's law (general)") {
val p = 0.25
- testcases(a => random => Seq(
- addDeMorgans(p)(random)(a) -> addDeMorgans(p)(random)(a)
- ), equivalent = true)
+ testcases(
+ a =>
+ random =>
+ Seq(
+ addDeMorgans(p)(random)(a) -> addDeMorgans(p)(random)(a)
+ ),
+ equivalent = true
+ )
}
test("Allowed tautologies") {
- testcases((a, b, c) => random => Seq(
- or(a, neg(a)) -> or(neg(a), neg(neg(a))),
- and(a, neg(a)) -> and(neg(a), neg(neg(a))),
- ), equivalent = true)
+ testcases(
+ (a, b, c) =>
+ random =>
+ Seq(
+ or(a, neg(a)) -> or(neg(a), neg(neg(a))),
+ and(a, neg(a)) -> and(neg(a), neg(neg(a)))
+ ),
+ equivalent = true
+ )
}
test("Absorption") {
- testcases((a, b, c) => random => Seq(
- and(a, a) -> a,
- or(a, a) -> a,
- //or(or(a, neg(a)), c) -> c,
- //and(and(a, neg(a)), c) -> and(a, neg(a)),
- ), equivalent = true)
+ testcases(
+ (a, b, c) =>
+ random =>
+ Seq(
+ and(a, a) -> a,
+ or(a, a) -> a
+ // or(or(a, neg(a)), c) -> c,
+ // and(and(a, neg(a)), c) -> and(a, neg(a)),
+ ),
+ equivalent = true
+ )
}
test("All allowed transformations") {
@@ -304,20 +366,25 @@ class EquivalenceCheckerTests extends AnyFunSuite {
r => commutativeShuffle(1)(r) _,
r => associativeShuffle(1)(r) _,
r => addDoubleNegations(0.02)(r) _,
- r => addDeMorgans(0.05)(r) _,
+ r => addDeMorgans(0.05)(r) _
)
def randomTransformations(random: Random)(f: Formula): Formula = {
val n = random.nextInt(50)
Seq.fill(n)(transformations(random.nextInt(transformations.size))).foldLeft(f)((acc, e) => e(random)(acc))
}
- testcases(a => random => Seq(
- randomTransformations(random)(a) -> randomTransformations(random)(a)
- ), equivalent = true)
+ testcases(
+ a =>
+ random =>
+ Seq(
+ randomTransformations(random)(a) -> randomTransformations(random)(a)
+ ),
+ equivalent = true
+ )
}
// Negative
-/*
+ /*
test("Negative by construction") {
val x = PredicateFormula(ConstantPredicateLabel("$", 0), Seq.empty) // Globally free
testcases((a, b) => random => Seq(
@@ -328,5 +395,4 @@ class EquivalenceCheckerTests extends AnyFunSuite {
), equivalent = false)
}*/
-
}
diff --git a/src/test/scala/lisa/kernel/FolTests.scala b/src/test/scala/lisa/kernel/FolTests.scala
index 70ae8ea2502c808468a7b060682388a4385ac71d..27a3eede291b31d6faff676c6b7c6ff04baff8a1 100644
--- a/src/test/scala/lisa/kernel/FolTests.scala
+++ b/src/test/scala/lisa/kernel/FolTests.scala
@@ -25,30 +25,30 @@ class FolTests extends AnyFunSuite {
if (maxDepth <= 1) {
val r = gen.between(0, 3)
if (r == 0) {
- val name = "" + ('a' to 'e') (gen.between(0, 5))
+ val name = "" + ('a' to 'e')(gen.between(0, 5))
FunctionTerm(ConstantFunctionLabel(name, 0), List())
- }
- else {
- val name = "" + ('v' to 'z') (gen.between(0, 5))
+ } else {
+ val name = "" + ('v' to 'z')(gen.between(0, 5))
VariableTerm(VariableLabel(name))
}
} else {
val r = gen.between(0, 8)
- val name = "" + ('f' to 'j') (gen.between(0, 5))
+ val name = "" + ('f' to 'j')(gen.between(0, 5))
if (r == 0) {
- val name = "" + ('a' to 'e') (gen.between(0, 5))
+ val name = "" + ('a' to 'e')(gen.between(0, 5))
FunctionTerm(ConstantFunctionLabel(name, 0), List())
- }
- else if (r == 1) {
- val name = "" + ('v' to 'z') (gen.between(0, 5))
+ } else if (r == 1) {
+ val name = "" + ('v' to 'z')(gen.between(0, 5))
VariableTerm(VariableLabel(name))
}
if (r <= 3) FunctionTerm(ConstantFunctionLabel(name, 1), Seq(termGenerator(maxDepth - 1, gen)))
else if (r <= 5) FunctionTerm(ConstantFunctionLabel(name, 2), Seq(termGenerator(maxDepth - 1, gen), termGenerator(maxDepth - 1, gen)))
- else if (r == 6) FunctionTerm(ConstantFunctionLabel(name, 3),
- Seq(termGenerator(maxDepth - 1, gen), termGenerator(maxDepth - 1, gen), termGenerator(maxDepth - 1, gen)))
- else FunctionTerm(ConstantFunctionLabel(name, 4),
- Seq(termGenerator(maxDepth - 1, gen), termGenerator(maxDepth - 1, gen), termGenerator(maxDepth - 1, gen), termGenerator(maxDepth - 1, gen)))
+ else if (r == 6) FunctionTerm(ConstantFunctionLabel(name, 3), Seq(termGenerator(maxDepth - 1, gen), termGenerator(maxDepth - 1, gen), termGenerator(maxDepth - 1, gen)))
+ else
+ FunctionTerm(
+ ConstantFunctionLabel(name, 4),
+ Seq(termGenerator(maxDepth - 1, gen), termGenerator(maxDepth - 1, gen), termGenerator(maxDepth - 1, gen), termGenerator(maxDepth - 1, gen))
+ )
}
}
@@ -57,42 +57,34 @@ class FolTests extends AnyFunSuite {
if (maxDepth <= 2 || (gen.nextBoolean() && gen.nextBoolean())) {
val r = gen.between(0, 7)
if (r <= 1) {
- val name = "" + ('A' to 'E') (gen.between(0, 5))
+ val name = "" + ('A' to 'E')(gen.between(0, 5))
PredicateFormula(ConstantPredicateLabel(name, 0), Seq())
- }
-
- else if (r <= 3) {
- val name = "" + ('A' to 'E') (gen.between(0, 5))
+ } else if (r <= 3) {
+ val name = "" + ('A' to 'E')(gen.between(0, 5))
PredicateFormula(ConstantPredicateLabel(name, 1), Seq(termGenerator(maxDepth - 1, gen)))
- }
-
- else if (r <= 5) {
+ } else if (r <= 5) {
val s = gen.between(0, 3)
if (s == 0) PredicateFormula(equality, Seq(termGenerator(maxDepth - 1, gen), termGenerator(maxDepth - 1, gen)))
else {
- val name = "" + ('A' to 'E') (gen.between(0, 5))
+ val name = "" + ('A' to 'E')(gen.between(0, 5))
PredicateFormula(ConstantPredicateLabel(name, 2), Seq(termGenerator(maxDepth - 1, gen), termGenerator(maxDepth - 1, gen)))
}
- }
- else {
- val name = "" + ('A' to 'E') (gen.between(0, 5))
- PredicateFormula(ConstantPredicateLabel(name, 3),
- Seq(termGenerator(maxDepth - 1, gen), termGenerator(maxDepth - 1, gen), termGenerator(maxDepth - 1, gen)))
+ } else {
+ val name = "" + ('A' to 'E')(gen.between(0, 5))
+ PredicateFormula(ConstantPredicateLabel(name, 3), Seq(termGenerator(maxDepth - 1, gen), termGenerator(maxDepth - 1, gen), termGenerator(maxDepth - 1, gen)))
}
- }
- else {
+ } else {
val r = gen.between(0, 7)
if (r <= 1) neg(formulaGenerator(maxDepth - 1, gen))
else if (r == 2) and(formulaGenerator(maxDepth - 1, gen), formulaGenerator(maxDepth - 1, gen))
else if (r == 3) or(formulaGenerator(maxDepth - 1, gen), formulaGenerator(maxDepth - 1, gen))
- else if (r == 4) implies(formulaGenerator(maxDepth - 1, gen),formulaGenerator(maxDepth - 1, gen))
+ else if (r == 4) implies(formulaGenerator(maxDepth - 1, gen), formulaGenerator(maxDepth - 1, gen))
else if (r == 5) {
val f = formulaGenerator(maxDepth - 1, gen)
val l = f.freeVariables.toSeq ++ Seq(x)
forall(l(gen.between(0, l.size)), f)
- }
- else {
+ } else {
val f = formulaGenerator(maxDepth - 1, gen)
val l = f.freeVariables.toSeq ++ Seq(x)
exists(l(gen.between(0, l.size)), f)
@@ -117,10 +109,9 @@ class FolTests extends AnyFunSuite {
(0 to 50).foreach(_ => formulaGenerator(10))
}
-
test("Fresh variables should be fresh") {
val y1 = VariableLabel(freshId(equ(VariableTerm(x), VariableTerm(x)).freeVariables.map(_.name), x.name))
assert(!isSame(x, y1))
}
-}
\ No newline at end of file
+}
diff --git a/src/test/scala/lisa/kernel/IncorrectProofsTests.scala b/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
index 14f1de7881d7060c4954d37973aaa9899ead8967..9259274b6e5edeaf0fc0fd9f6b297d811c70824a 100644
--- a/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
+++ b/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
@@ -26,7 +26,6 @@ class IncorrectProofsTests extends ProofCheckerSuite {
val emptySetAxiom = lisa.settheory.AxiomaticSetTheory.emptySetAxiom
val pairAxiom = lisa.settheory.AxiomaticSetTheory.pairAxiom
-
val incorrectProofs: Seq[SCProof] = List(
SCProof(
Hypothesis(emptySeq +< (x === x) +> (x === x), x === x),
@@ -40,22 +39,22 @@ class IncorrectProofsTests extends ProofCheckerSuite {
RightRefl(emptySeq +> f, x === x),
RightRefl(emptySeq +> (x === x), f),
// Correct proof would be: x=y |- x=y \ x=y,x=z |- z=y
-
+
SCProof(
Hypothesis(emptySeq +< (x === y) +> (x === y), x === y),
- RightSubstEq(emptySeq +< (x === y) +< (x === z) +> (z === y), 0, List((x, z)), LambdaTermFormula(Seq(yl), x === y)) // wrong variable replaced
+ RightSubstEq(emptySeq +< (x === y) +< (x === z) +> (z === y), 0, List((x, z)), LambdaTermFormula(Seq(yl), x === y)) // wrong variable replaced
),
SCProof(
Hypothesis(emptySeq +< (x === y) +> (x === y), x === y),
- RightSubstEq(emptySeq +< (x === y) +> (z === y), 0, List((x, z)), LambdaTermFormula(Seq(xl), x === y)) // missing hypothesis
+ RightSubstEq(emptySeq +< (x === y) +> (z === y), 0, List((x, z)), LambdaTermFormula(Seq(xl), x === y)) // missing hypothesis
),
SCProof(
Hypothesis(emptySeq +< (x === y) +> (x === y), x === y),
- RightSubstEq(emptySeq +< (x === y) +< (x === z) +> (z === y), 0, List((x, z)), LambdaTermFormula(Seq(xl), x === z)) // replacement mismatch
+ RightSubstEq(emptySeq +< (x === y) +< (x === z) +> (z === y), 0, List((x, z)), LambdaTermFormula(Seq(xl), x === z)) // replacement mismatch
),
SCProof(
Hypothesis(emptySeq +< (x === y) +> (x === y), x === y),
- LeftSubstEq(emptySeq +< (z === y) +< (x === z) +> (x === y), 0, List((x, z)), LambdaTermFormula(Seq(yl), x === y))
+ LeftSubstEq(emptySeq +< (z === y) +< (x === z) +> (x === y), 0, List((x, z)), LambdaTermFormula(Seq(yl), x === y))
),
SCProof(
Hypothesis(emptySeq +< (f <=> g) +> (f <=> g), f <=> g),
@@ -88,7 +87,6 @@ class IncorrectProofsTests extends ProofCheckerSuite {
Hypothesis(emptySeq +< f +> f, f),
RightOr(emptySeq +< f +> (f \/ g) +> g, 0, f, g) // supplemental right g
)
-
)
incorrectProofs.foreach(checkIncorrectProof)
diff --git a/src/test/scala/lisa/kernel/ProofTests.scala b/src/test/scala/lisa/kernel/ProofTests.scala
index b26dbe442a7d7330a925517fa944b88545c34e75..665f95754322cdbba1a9b75a8641453856986206 100644
--- a/src/test/scala/lisa/kernel/ProofTests.scala
+++ b/src/test/scala/lisa/kernel/ProofTests.scala
@@ -11,8 +11,7 @@ import lisa.kernel.proof.{SCProof, SCProofChecker}
import scala.util.Random
-
-class ProofTests extends AnyFunSuite {
+class ProofTests extends AnyFunSuite {
val predicateVerifier = SCProofChecker.checkSCProof
private val x = VariableLabel("x")
@@ -23,11 +22,10 @@ class ProofTests extends AnyFunSuite {
private val fp = ConstantPredicateLabel("F", 1)
val sT = SchematicFunctionLabel("t", 0)
-
test("Verification of Pierce law") {
- val s0 = Hypothesis( a |- a, a)
- val s1 = Weakening(a |- Set(a,b), 0)
- val s2 = RightImplies(() |- Set(a,a==>b), 1, a, b)
+ val s0 = Hypothesis(a |- a, a)
+ val s1 = Weakening(a |- Set(a, b), 0)
+ val s2 = RightImplies(() |- Set(a, a ==> b), 1, a, b)
val s3 = LeftImplies((a ==> b) ==> a |- a, 2, 0, a ==> b, a)
val s4 = RightImplies(() |- (a ==> b) ==> a ==> a, 3, (a ==> b) ==> a, a)
val ppl: SCProof = SCProof(IndexedSeq(s0, s1, s2, s3, s4))
@@ -35,7 +33,7 @@ class ProofTests extends AnyFunSuite {
}
test("Verification of substitution") {
- val t0 = Hypothesis(fp(x)|-fp(x), fp(x))
+ val t0 = Hypothesis(fp(x) |- fp(x), fp(x))
val t1 = RightSubstEq(Set(fp(x), x === y) |- fp(y), 0, List((x, y)), LambdaTermFormula(Seq(sT), fp(sT())))
val pr = new SCProof(IndexedSeq(t0, t1))
assert(predicateVerifier(pr).isValid)
diff --git a/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala b/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala
index da4387b54eb92e7452256d97e784074ab2039b4f..5786462d0495fa3aeb214878b01718d01bc6bbfa 100644
--- a/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala
+++ b/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala
@@ -13,45 +13,67 @@ import lisa.kernel.proof.SequentCalculus.*
class ElementsOfSetTheoryTests extends ProofCheckerSuite {
-
test("Verification of the proof of symmetry of the pair") {
checkProof(proofUnorderedPairSymmetry, emptySeq +> forall(vl, forall(ul, pair(u, v) === pair(v, u))))
}
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(u, v)) ==>
- (((VariableTerm(v) === t) /\ (VariableTerm(u) === s)) \/ ((VariableTerm(s) === v) /\ (VariableTerm(t) === u)))))))
+ checkProof(
+ proofUnorderedPairDeconstruction,
+ emptySeq +>
+ forall(
+ sl,
+ forall(
+ tl,
+ forall(
+ ul,
+ forall(
+ vl,
+ (pair(s, t) === pair(u, v)) ==>
+ (((VariableTerm(v) === t) /\ (VariableTerm(u) === s)) \/ ((VariableTerm(s) === v) /\ (VariableTerm(t) === u)))
+ )
+ )
+ )
+ )
)
}
// forall x, y. (x in {y, y}) <=> (x = y)
val singletonSetEqualityProof: SCProof = {
- val t0 = SCSubproof({
- val t0 = Rewrite(()|-pairAxiom, -1)
- 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 )
+ val t0 = SCSubproof(
+ {
+ val t0 = Rewrite(() |- pairAxiom, -1)
+ 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({
- val t0 = Hypothesis(Sequent(Set(f), Set(f)), f)
- val t1 = RightOr(Sequent(Set(f), Set(f \/ f)), 0, f, f)
- val t2 = LeftOr(Sequent(Set(f \/ f), Set(f)), Seq(0, 0), Seq(f, f))
- val t3 = RightImplies(Sequent(Set(), Set(f ==> (f \/ f))), 1, f, f \/ f)
- 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))
- }, display=false)
+ def selfIffOr(f: Formula): SCSubproof = SCSubproof(
+ {
+ val t0 = Hypothesis(Sequent(Set(f), Set(f)), f)
+ val t1 = RightOr(Sequent(Set(f), Set(f \/ f)), 0, f, f)
+ val t2 = LeftOr(Sequent(Set(f \/ f), Set(f)), Seq(0, 0), Seq(f, f))
+ val t3 = RightImplies(Sequent(Set(), Set(f ==> (f \/ f))), 1, f, f \/ f)
+ 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))
+ },
+ 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(u, pair(v, v)))), 0,
- List(((v === u) \/ (v === u), v === u)),
- LambdaFormulaFormula(Seq(h), in(u, pair(v, v)) <=> PredicateFormula(h, Seq.empty)))
+ val t2 = RightSubstIff(
+ Sequent(Set((xy \/ xy) <=> xy), Set(xy <=> in(u, pair(v, v)))),
+ 0,
+ List(((v === u) \/ (v === u), v === u)),
+ LambdaFormulaFormula(Seq(h), in(u, pair(v, v)) <=> PredicateFormula(h, Seq.empty))
+ )
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), IndexedSeq(() |- pairAxiom))
@@ -63,6 +85,4 @@ class ElementsOfSetTheoryTests extends ProofCheckerSuite {
checkProof(singletonSetEqualityProof, emptySeq +> forall(u, forall(v, (u === v) <=> in(u, pair(v, v)))))
}
-
-
}
diff --git a/src/test/scala/lisa/proven/SimpleProverTests.scala b/src/test/scala/lisa/proven/SimpleProverTests.scala
index 3538752262928c4d671eb135a12f51ef2ec1242c..8f56fe7be3442b98d4195b0360b9025894c4e15f 100644
--- a/src/test/scala/lisa/proven/SimpleProverTests.scala
+++ b/src/test/scala/lisa/proven/SimpleProverTests.scala
@@ -11,10 +11,9 @@ import tptp.ProblemGatherer.getPRPproblems
import tptp.KernelParser.*
import proven.tactics.SimplePropositionalSolver as SPS
-
class SimpleProverTests extends AnyFunSuite {
- /*
+ /*
test("Simple propositional logic proofs") {
val problems = getPRPproblems.take(1)
problems.foreach( pr => {
@@ -29,5 +28,5 @@ class SimpleProverTests extends AnyFunSuite {
})
}
- */
+ */
}
diff --git a/src/test/scala/test/ProofCheckerSuite.scala b/src/test/scala/test/ProofCheckerSuite.scala
index 57872adb26d740736a40539c375e261b6ab4c817..d91d1fd9a1761af03d847ed93fea4ca7c4448c2d 100644
--- a/src/test/scala/test/ProofCheckerSuite.scala
+++ b/src/test/scala/test/ProofCheckerSuite.scala
@@ -12,8 +12,26 @@ import lisa.KernelHelpers.given_Conversion_Boolean_List_String_Option
abstract class ProofCheckerSuite extends AnyFunSuite {
import lisa.kernel.fol.FOL.*
- protected val (xl, yl, zl, wl, xpl, ypl, zpl, wpl) = (SchematicFunctionLabel("x", 0), SchematicFunctionLabel("y", 0), SchematicFunctionLabel("z", 0), SchematicFunctionLabel("w", 0), SchematicFunctionLabel("x'", 0), SchematicFunctionLabel("y'", 0), SchematicFunctionLabel("z'", 0), SchematicFunctionLabel("w'", 0))
- protected val (x, y, z, w, xp, yp, zp, wp) = (FunctionTerm(xl, Seq.empty), FunctionTerm(yl, Seq.empty), FunctionTerm(zl, Seq.empty), FunctionTerm(wl, Seq.empty), FunctionTerm(xpl, Seq.empty), FunctionTerm(ypl, Seq.empty), FunctionTerm(zpl, Seq.empty), FunctionTerm(wpl, Seq.empty))
+ protected val (xl, yl, zl, wl, xpl, ypl, zpl, wpl) = (
+ SchematicFunctionLabel("x", 0),
+ SchematicFunctionLabel("y", 0),
+ SchematicFunctionLabel("z", 0),
+ SchematicFunctionLabel("w", 0),
+ SchematicFunctionLabel("x'", 0),
+ SchematicFunctionLabel("y'", 0),
+ SchematicFunctionLabel("z'", 0),
+ SchematicFunctionLabel("w'", 0)
+ )
+ protected val (x, y, z, w, xp, yp, zp, wp) = (
+ FunctionTerm(xl, Seq.empty),
+ FunctionTerm(yl, Seq.empty),
+ FunctionTerm(zl, Seq.empty),
+ FunctionTerm(wl, Seq.empty),
+ FunctionTerm(xpl, Seq.empty),
+ FunctionTerm(ypl, Seq.empty),
+ FunctionTerm(zpl, Seq.empty),
+ FunctionTerm(wpl, Seq.empty)
+ )
protected val (sl, tl, ul, vl) = (VariableLabel("s"), VariableLabel("t"), VariableLabel("u"), VariableLabel("v"))
protected val (s, t, u, v) = (VariableTerm(sl), VariableTerm(tl), VariableTerm(ul), VariableTerm(vl))
@@ -27,11 +45,14 @@ abstract class ProofCheckerSuite extends AnyFunSuite {
def checkProof(proof: SCProof, expected: Sequent): Unit = {
val judgement = checkSCProof(proof)
- assert(judgement.isValid, "\n"+Printer.prettySCProof(proof, judgement))
+ assert(judgement.isValid, "\n" + Printer.prettySCProof(proof, judgement))
assert(isSameSequent(proof.conclusion, expected), s"(${Printer.prettySequent(proof.conclusion)} did not equal ${Printer.prettySequent(expected)})")
}
def checkIncorrectProof(incorrectProof: SCProof): Unit = {
- assert(!checkSCProof(incorrectProof).isValid, s"(incorrect proof with conclusion '${Printer.prettySequent(incorrectProof.conclusion)}' was accepted by the proof checker)\nSequent: ${incorrectProof.conclusion}")
+ assert(
+ !checkSCProof(incorrectProof).isValid,
+ s"(incorrect proof with conclusion '${Printer.prettySequent(incorrectProof.conclusion)}' was accepted by the proof checker)\nSequent: ${incorrectProof.conclusion}"
+ )
}
}