diff --git a/lisa-front/src/test/scala/lisa/front/UnificationTests.scala b/lisa-front/src/test/scala/lisa/front/UnificationTests.scala
index 5e42bb75517e149571d7f44c6ec23df781ca3971..26103982bae86ac4eb44d61a3d3445290c2c168e 100644
--- a/lisa-front/src/test/scala/lisa/front/UnificationTests.scala
+++ b/lisa-front/src/test/scala/lisa/front/UnificationTests.scala
@@ -2,11 +2,15 @@ package lisa.front
import lisa.front.fol.FOL.LabelType
import lisa.front.fol.FOL.WithArityType
-import lisa.front.{*, given}
+import lisa.front.printer.FrontPositionedPrinter
+import lisa.front.printer.FrontPrintStyle
+import lisa.front.{_, given}
+import org.scalatest.Ignore
import org.scalatest.funsuite.AnyFunSuite
import scala.language.adhocExtensions
+@Ignore
class UnificationTests extends AnyFunSuite {
val (sa, sb, sc) = (SchematicPredicateLabel[0]("a"), SchematicPredicateLabel[0]("b"), SchematicPredicateLabel[0]("c"))
@@ -21,7 +25,7 @@ class UnificationTests extends AnyFunSuite {
val (x, y, z) = (VariableLabel("x"), VariableLabel("y"), VariableLabel("z"))
- def unify(pattern: Formula, target: Formula, partial: UnificationContext = UnificationContext()): Option[(IndexedSeq[Sequent], UnificationContext)] =
+ def unify(pattern: Formula, target: Formula, partial: UnificationContext = emptyContext): Option[(IndexedSeq[Sequent], UnificationContext)] =
unifyAndResolve(
IndexedSeq(PartialSequent(IndexedSeq(pattern), IndexedSeq.empty)),
IndexedSeq(Sequent(IndexedSeq(target), IndexedSeq.empty)),
@@ -31,12 +35,20 @@ class UnificationTests extends AnyFunSuite {
)
@deprecated
- def checkUnifies(pattern: Formula, target: Formula, partial: UnificationContext = UnificationContext()): Unit = {
- assert(unify(pattern, target, partial).nonEmpty, "It did not unify")
+ def checkUnifies(pattern: Formula, target: Formula, partial: UnificationContext = emptyContext): Unit = {
+ assert(
+ unify(pattern, target, partial).nonEmpty,
+ s"Pattern ${FrontPositionedPrinter.prettyFormula(pattern, symbols = FrontPrintStyle.Unicode)} and " +
+ s"target ${FrontPositionedPrinter.prettyFormula(target, symbols = FrontPrintStyle.Unicode)} did not unify"
+ )
}
- def checkDoesNotUnify(pattern: Formula, target: Formula, partial: UnificationContext = UnificationContext()): Unit = {
- assert(unify(pattern, target, partial).isEmpty, "It did unify")
+ def checkDoesNotUnify(pattern: Formula, target: Formula, partial: UnificationContext = emptyContext): Unit = {
+ assert(
+ unify(pattern, target, partial).isEmpty,
+ s"Pattern ${FrontPositionedPrinter.prettyFormula(pattern, symbols = FrontPrintStyle.Unicode)} and " +
+ s"target ${FrontPositionedPrinter.prettyFormula(target, symbols = FrontPrintStyle.Unicode)} did unify"
+ )
}
def contextsEqual(ctx1: UnificationContext, ctx2: UnificationContext): Boolean = {
@@ -73,77 +85,172 @@ class UnificationTests extends AnyFunSuite {
normalizeContext(ctx1) == normalizeContext(ctx2)
}
- def checkUnifiesAs(pattern: Formula, target: Formula, partial: UnificationContext, ctx: UnificationContext): Unit = {
+ def checkUnifiesAs(pattern: Formula, target: Formula, partial: UnificationContext)(expected: UnificationContext): Unit = {
unify(pattern, target, partial) match {
- case Some((_, resultCtx)) => assert(contextsEqual(resultCtx, ctx), resultCtx)
- case None => throw new AssertionError("It did not unify")
+ case Some((_, resultCtx)) => assert(contextsEqual(resultCtx, expected), resultCtx)
+ case None =>
+ fail(
+ s"Pattern ${FrontPositionedPrinter.prettyFormula(pattern, symbols = FrontPrintStyle.Unicode)} and " +
+ s"target ${FrontPositionedPrinter.prettyFormula(target, symbols = FrontPrintStyle.Unicode)} did not unify"
+ )
}
}
- def checkUnifiesAs(pattern: Formula, target: Formula, ctx: UnificationContext): Unit =
- checkUnifiesAs(pattern, target, UnificationContext(), ctx)
+ def checkUnifiesAs(pattern: Formula, target: Formula)(expected: UnificationContext): Unit =
+ checkUnifiesAs(pattern, target, emptyContext)(expected)
- val U: UnificationContext = UnificationContext()
+ val emptyContext: UnificationContext = UnificationContext()
+ val emptyResult: UnificationContext = UnificationContext()
- test("unification 2") {
- checkUnifiesAs(a, a, UnificationContext())
+ test("same boolean constant") {
+ checkUnifiesAs(a, a)(emptyResult)
+ }
+ test("different boolean constants") {
checkDoesNotUnify(a, b)
+ }
+ test("boolean and schematic constants") {
checkDoesNotUnify(a, sa)
- checkUnifiesAs(a /\ b, a /\ b, U)
-
- checkUnifiesAs(sa, a, U + AssignedPredicate(sa, a))
- checkUnifiesAs(sa, sa, U + AssignedPredicate(sa, sa))
- checkUnifiesAs(sa /\ b, a /\ b, U + AssignedPredicate(sa, a))
- checkUnifiesAs(sa /\ sb, a /\ b, U + AssignedPredicate(sa, a) + AssignedPredicate(sb, b))
- checkUnifiesAs(sa /\ b, sb /\ b, U + AssignedPredicate(sa, sb))
- checkUnifiesAs(sa /\ sb, (a ==> b) /\ (c \/ a), U + AssignedPredicate(sa, a ==> b) + AssignedPredicate(sb, c \/ a))
- checkUnifiesAs(sa /\ sa, b /\ b, U + AssignedPredicate(sa, b))
- checkUnifiesAs(sa /\ sa, (a \/ b) /\ (b \/ a), U + AssignedPredicate(sa, a \/ b))
- checkDoesNotUnify(sa /\ sa, a /\ b)
-
- checkUnifiesAs(sa, a /\ b, U + AssignedPredicate(sa, b /\ a), U + AssignedPredicate(sa, b /\ a))
- checkUnifiesAs(sa, a, U + AssignedPredicate(sa, a), U + AssignedPredicate(sa, a))
- checkDoesNotUnify(sa, a, U + AssignedPredicate(sa, b))
- checkDoesNotUnify(sa, a, U + AssignedPredicate(sb, a))
+ }
+ test("boolean constant expression") {
+ checkUnifiesAs(a /\ b, a /\ b)(emptyResult)
+ }
- checkUnifiesAs(p1(t), p1(t), U)
- checkUnifiesAs(p1(st), p1(u), U + AssignedFunction(st, u))
- checkUnifiesAs(sp1(t), p1(t), U + AssignedPredicate(sp1, LambdaPredicate(x => p1(x))))
- checkUnifiesAs(sp1(t), p1(t) /\ p1(u), U + AssignedPredicate(sp1, LambdaPredicate(x => p1(x) /\ p1(u))))
+ test("schematic boolean constant") {
+ checkUnifiesAs(sa, a)(emptyResult + AssignedPredicate(sa, a))
+ }
+ test("same schematic boolean constant") {
+ checkUnifiesAs(sa, sa)(emptyResult + AssignedPredicate(sa, sa))
+ }
+ test("expression with schematic boolean constant") {
+ checkUnifiesAs(sa /\ b, a /\ b)(emptyResult + AssignedPredicate(sa, a))
+ }
+ test("expression with multiple schematic boolean constants") {
+ checkUnifiesAs(sa /\ sb, a /\ b)(emptyResult + AssignedPredicate(sa, a) + AssignedPredicate(sb, b))
+ }
+ test("matching two schematic boolean constants") {
+ checkUnifiesAs(sa /\ b, sb /\ b)(emptyResult + AssignedPredicate(sa, sb))
+ }
+ test("schematic boolean constants match expressions") {
+ checkUnifiesAs(sa /\ sb, (a ==> b) /\ (c \/ a))(emptyResult + AssignedPredicate(sa, a ==> b) + AssignedPredicate(sb, c \/ a))
+ }
+ test("schematic predicate matches same expressions") {
+ checkUnifiesAs(sa /\ sa, b /\ b)(emptyResult + AssignedPredicate(sa, b))
+ }
+ test("schematic predicate matches equivalent expressions") {
+ checkUnifiesAs(sa /\ sa, (a \/ b) /\ (b \/ a))(emptyResult + AssignedPredicate(sa, a \/ b))
+ }
+ test("schematic predicate does not match different constants") {
+ checkDoesNotUnify(sa /\ sa, a /\ b)
+ }
+ test("schematic 0-ary predicate: equivalent expression in the context") {
+ checkUnifiesAs(sa, a /\ b, emptyContext + AssignedPredicate(sa, b /\ a))(
+ emptyResult + AssignedPredicate(sa, b /\ a)
+ )
+ }
+ test("schematic 0-ary predicate with partial mapping") {
+ checkUnifiesAs(sa, a, emptyContext + AssignedPredicate(sa, a))(emptyResult + AssignedPredicate(sa, a))
+ }
+ test("schematic 0-ary predicate with contradicting partial mapping") {
+ checkDoesNotUnify(sa, a, emptyContext + AssignedPredicate(sa, b))
+ }
+ test("schematic 0-ary predicate with contradicting partial mapping 2") {
+ checkDoesNotUnify(sa, a, emptyContext + AssignedPredicate(sb, a))
+ }
- checkUnifiesAs(sg1(a), b, U + AssignedConnector(sg1, LambdaConnector(_ => b)))
+ test("same predicate") {
+ checkUnifiesAs(p1(t), p1(t))(emptyResult)
+ }
+ test("predicate of schematic variable to predicate of constant") {
+ checkUnifiesAs(p1(st), p1(u))(emptyResult + AssignedFunction(st, u))
+ }
+ test("schematic to constant predicate") {
+ checkUnifiesAs(sp1(t), p1(t))(emptyResult + AssignedPredicate(sp1, LambdaPredicate(x => p1(x))))
+ }
+ test("schematic predicate to expression") {
+ checkUnifiesAs(sp1(t), p1(t) /\ p1(u))(emptyResult + AssignedPredicate(sp1, LambdaPredicate(x => p1(x) /\ p1(u))))
+ }
+ test("schematic connector of boolean constant to boolean constant") {
+ checkUnifiesAs(sg1(a), b)(emptyResult + AssignedConnector(sg1, LambdaConnector(_ => b)))
+ }
+ test("schematic connector of schematic boolean constant does not match boolean constant") {
checkDoesNotUnify(sg1(sa), a)
- checkUnifiesAs(sg1(sa), b, U + AssignedConnector(sg1, LambdaConnector(x => x)), U + AssignedConnector(sg1, LambdaConnector(x => x)) + AssignedPredicate(sa, b))
- checkUnifiesAs(sg1(sa), b, U + AssignedPredicate(sa, b), U + AssignedPredicate(sa, b) + AssignedConnector(sg1, LambdaConnector(x => x)))
-
- checkUnifiesAs(
- sg1(sa),
- b,
- U + AssignedConnector(sg1, LambdaConnector(x => x)) + AssignedPredicate(sa, b),
- U + AssignedConnector(sg1, LambdaConnector(x => x)) + AssignedPredicate(sa, b)
+ }
+ test("schematic connector of schematic boolean constant with partial mapping of connector") {
+ checkUnifiesAs(sg1(sa), b, emptyContext + AssignedConnector(sg1, LambdaConnector(x => x)))(
+ emptyResult +
+ AssignedConnector(sg1, LambdaConnector(x => x)) + AssignedPredicate(sa, b)
+ )
+ }
+ test("schematic connector of schematic boolean constant with partial mapping of 0-ary predicate") {
+ checkUnifiesAs(sg1(sa), b, emptyContext + AssignedPredicate(sa, b))(
+ emptyResult + AssignedPredicate(sa, b) +
+ AssignedConnector(sg1, LambdaConnector(x => x))
)
- checkDoesNotUnify(sg1(sa), b, U + AssignedConnector(sg1, LambdaConnector(x => x)) + AssignedPredicate(sa, a))
- checkDoesNotUnify(sg1(sa), b, U + AssignedConnector(sg1, LambdaConnector(_ => a)) + AssignedPredicate(sa, b))
+ }
+ test("schematic connector of schematic boolean constant with partial mapping of connector and 0-ary predicate") {
+ checkUnifiesAs(sg1(sa), b, emptyContext + AssignedConnector(sg1, LambdaConnector(x => x)) + AssignedPredicate(sa, b))(
+ emptyContext + AssignedConnector(sg1, LambdaConnector(x => x)) + AssignedPredicate(sa, b)
+ )
+ }
+ test("schematic connector of schematic boolean constant with partial mapping of connector and different 0-ary predicate") {
+ checkDoesNotUnify(sg1(sa), b, emptyContext + AssignedConnector(sg1, LambdaConnector(x => x)) + AssignedPredicate(sa, a))
+ }
+ test("schematic connector of schematic boolean constant with partial mapping of 0-ary predicate and different connector") {
+ checkDoesNotUnify(sg1(sa), b, emptyContext + AssignedConnector(sg1, LambdaConnector(_ => a)) + AssignedPredicate(sa, b))
+ }
+ test("predicate of a variable") {
+ checkUnifiesAs(p1(x), p1(x))(emptyResult + (x -> x))
+ }
+ test("predicate of a variable to a predicate of a different variable") {
+ checkUnifiesAs(p1(x), p1(y))(emptyResult + (x -> y))
+ }
+ test("predicate of a variable to a predicate of a different variable with partial mapping of variables") {
+ checkUnifiesAs(p1(x), p1(y), emptyContext + (x -> y))(emptyResult + (x -> y))
+ }
+ test("predicate of a variable to a predicate of a different variable with incompatible partial mapping of variables") {
+ checkDoesNotUnify(p1(x), p1(y), emptyContext + (x -> z))
+ }
- checkUnifiesAs(exists(x, a), exists(x, a), U + (x -> x))
- checkUnifiesAs(exists(x, a), exists(y, a), U + (x -> y))
- checkUnifiesAs(exists(x, p1(x)), exists(y, p1(y)), U + (x -> y))
+ test("exists constant") {
+ checkUnifiesAs(exists(x, a), exists(x, a))(emptyResult + (x -> x))
+ }
+ test("exists constant with different bound variables") {
+ checkUnifiesAs(exists(x, a), exists(y, a))(emptyResult + (x -> y))
+ }
+ test("exists expression with different bound variables") {
+ checkUnifiesAs(exists(x, p1(x)), exists(y, p1(y)))(emptyResult + (x -> y))
+ }
+ test("exists expression of bound vs free variable") {
checkDoesNotUnify(exists(x, p1(x)), exists(y, p1(z)))
- checkUnifiesAs(p1(x), p1(x), U + (x -> x))
- checkUnifiesAs(p1(x), p1(y), U + (x -> y))
- checkUnifiesAs(p1(x), p1(y), U + (x -> y), U + (x -> y))
- checkDoesNotUnify(p1(x), p1(y), U + (x -> z))
-
- checkUnifiesAs(exists(x, sp1(x)), exists(y, p1(y) /\ a), U + (x -> y) + AssignedPredicate(sp1, LambdaPredicate(v => p1(v) /\ a)))
- checkUnifiesAs(exists(x, sa), exists(x, p1(t)), U + (x -> x) + AssignedPredicate(sa, p1(t)))
+ }
+ test("exists schematic predicate to exists expression") {
+ checkUnifiesAs(exists(x, sp1(x)), exists(y, p1(y) /\ a))(emptyResult + (x -> y) + AssignedPredicate(sp1, LambdaPredicate(v => p1(v) /\ a)))
+ }
+ test("exists schematic boolean constant to exists predicate") {
+ checkUnifiesAs(exists(x, sa), exists(x, p1(t)))(emptyResult + (x -> x) + AssignedPredicate(sa, p1(t)))
+ }
+ test("exists schematic boolean constant to exists unary predicate (does not unify)") {
checkDoesNotUnify(exists(x, sa), exists(x, p1(x)))
- checkDoesNotUnify(exists(x, sp1(x)), exists(x, p1(x)), U + (x -> x) + AssignedPredicate(sp1, LambdaPredicate(_ => p1(x))))
+ }
+ test("exists schematic unary predicate to exists unary predicate with incompatible predicate mapping") {
+ checkDoesNotUnify(exists(x, sp1(x)), exists(x, p1(x)), emptyContext + (x -> x) + AssignedPredicate(sp1, LambdaPredicate(_ => p1(x))))
+ }
+ test("exists expression: switch bound and free variable") {
+ checkUnifiesAs(exists(x, exists(y, p1(x) /\ p1(y))), exists(y, exists(x, p1(y) /\ p1(x))))(
+ emptyResult + (x -> y) + (y -> x)
+ )
+ }
- checkUnifiesAs(p1(st) /\ p1(su), p1(x) /\ p1(x), U + AssignedFunction(st, x) + AssignedFunction(su, x))
+ test("term with different schematic variables to a term with the same variable") {
+ checkUnifiesAs(p1(st) /\ p1(su), p1(x) /\ p1(x))(emptyResult + AssignedFunction(st, x) + AssignedFunction(su, x))
+ }
+ test("term with same schematic variable to a term with different variables (does not unify)") {
checkDoesNotUnify(p1(st) /\ p1(st), p1(x) /\ p1(y))
+ }
+ test("term with same schematic variable to a term with different schematic variables (does not unify)") {
checkDoesNotUnify(p1(st) /\ p1(st), p1(su) /\ p1(sv))
- checkUnifiesAs(p1(st) /\ p1(st), p1(su) /\ p1(su), U + AssignedFunction(st, su))
-
- checkUnifiesAs(exists(x, exists(y, p1(x) /\ p1(y))), exists(y, exists(x, p1(y) /\ p1(x))), U + (x -> y) + (y -> x))
+ }
+ test("rename schematic variable") {
+ checkUnifiesAs(p1(st) /\ p1(st), p1(su) /\ p1(su))(emptyResult + AssignedFunction(st, su))
}
}
diff --git a/src/test/scala/lisa/automation/ProofTests.scala b/src/test/scala/lisa/automation/ProofTests.scala
index dad762a7092af0813028523d4a001dc6cd8b34ef..4bc569ba16591ac4b3e6ac17bb15572150c37086 100644
--- a/src/test/scala/lisa/automation/ProofTests.scala
+++ b/src/test/scala/lisa/automation/ProofTests.scala
@@ -4,110 +4,171 @@ import lisa.automation.Proof2.*
import lisa.front.fol.FOL.*
import lisa.kernel.proof.SCProofChecker
import lisa.utils.Printer
+import org.scalatest.Ignore
import org.scalatest.funsuite.AnyFunSuite
import scala.language.adhocExtensions
+// Not working while the front's unifier is not repaired.
+@Ignore
class ProofTests extends AnyFunSuite {
- //Not working while the front's unifier is not repaired.
- /*
val (a, b, c) = (SchematicPredicateLabel[0]("a"), SchematicPredicateLabel[0]("b"), SchematicPredicateLabel[0]("c"))
val (s, t, u) = (SchematicTermLabel[0]("s"), SchematicTermLabel[0]("t"), SchematicTermLabel[0]("u"))
val (x, y) = (VariableLabel("x"), VariableLabel("y"))
- private def checkProofs(proofs: Proof*): Unit = {
+ private def checkProof(proof: Proof): Unit = {
val emptyEnvironment: ProofEnvironment = newEmptyEnvironment()
- proofs.foreach { proof =>
- val result = evaluateProof(proof)(emptyEnvironment).map(reconstructSCProof)
- assert(result.nonEmpty)
- val scProof = result.get._1
- val judgement = SCProofChecker.checkSCProof(scProof)
- println(Printer.prettySCProof(judgement))
- println()
- assert(judgement.isValid)
- assert(scProof.imports.isEmpty)
- assert(lisa.kernel.proof.SequentCalculus.isSameSequent(scProof.conclusion, proof.initialState.goals.head))
- }
+ val result = evaluateProof(proof)(emptyEnvironment).map(reconstructSCProof)
+ assert(result.nonEmpty, s"kernel proof was empty for $proof")
+ val scProof = result.get._1
+ val judgement = SCProofChecker.checkSCProof(scProof)
+ assert(judgement.isValid, Printer.prettySCProof(judgement))
+ assert(scProof.imports.isEmpty, s"proof unexpectedly uses imports: ${Printer.prettySCProof(judgement)}")
+ assert(
+ lisa.kernel.proof.SequentCalculus.isSameSequent(scProof.conclusion, proof.initialState.goals.head),
+ s"proof does not prove ${Printer.prettySequent(proof.initialState.goals.head)}:\nPrinter.prettySCProof(judgement)"
+ )
}
- test("introduction rules") {
- checkProofs(
+ test("hypothesis") {
+ checkProof(
Proof(
(a, b /\ c) |- (b /\ c, b)
)(
RuleHypothesis(RuleParameters().withIndices(0)(1)(0))
- ),
+ )
+ )
+
+ }
+
+ test("left and") {
+ checkProof(
Proof(
(a /\ b) |- a
)(
RuleIntroductionLeftAnd(),
RuleHypothesis(RuleParameters().withIndices(0)(0)(0))
- ),
+ )
+ )
+ }
+
+ test("right and") {
+ checkProof(
Proof(
(a, b) |- (a /\ b)
)(
RuleIntroductionRightAnd(RuleParameters().withIndices(0)()(0)),
RuleHypothesis(RuleParameters().withIndices(0)(0)(0)),
RuleHypothesis(RuleParameters().withIndices(0)(1)(0))
- ),
+ )
+ )
+ }
+
+ test("left or") {
+ checkProof(
Proof(
(a \/ b) |- (a, b)
)(
RuleIntroductionLeftOr(RuleParameters().withIndices(0)(0)()),
RuleHypothesis(RuleParameters().withIndices(0)(0)(0)),
RuleHypothesis(RuleParameters().withIndices(0)(0)(1))
- ),
+ )
+ )
+ }
+
+ test("right or") {
+ checkProof(
Proof(
a |- (a \/ b)
)(
RuleIntroductionRightOr(RuleParameters().withIndices(0)()(0)),
RuleHypothesis(RuleParameters().withIndices(0)(0)(0))
- ),
+ )
+ )
+ }
+
+ test("left implies") {
+ checkProof(
Proof(
(a ==> b, a) |- b
)(
RuleIntroductionLeftImplies(RuleParameters().withIndices(0)(0)()),
RuleHypothesis(RuleParameters().withIndices(0)(0)(1)),
RuleHypothesis(RuleParameters().withIndices(0)(1)(0))
- ),
+ )
+ )
+ }
+
+ test("right implies") {
+ checkProof(
Proof(
() |- (a ==> a)
)(
RuleIntroductionRightImplies(RuleParameters().withIndices(0)()(0)),
RuleHypothesis(RuleParameters().withIndices(0)(0)(0))
- ),
+ )
+ )
+ }
+
+ test("left iff") {
+ checkProof(
Proof(
(a <=> b) |- (b ==> a)
)(
RuleIntroductionLeftIff(RuleParameters().withIndices(0)(0)()),
RuleHypothesis(RuleParameters().withIndices(0)(1)(0))
- ),
+ )
+ )
+ }
+
+ test("right iff") {
+ checkProof(
Proof(
(a ==> b, b ==> a) |- (a <=> b)
)(
RuleIntroductionRightIff(RuleParameters().withIndices(0)()(0)),
RuleHypothesis(RuleParameters().withIndices(0)(0)(0)),
RuleHypothesis(RuleParameters().withIndices(0)(1)(0))
- ),
+ )
+ )
+ }
+
+ test("left not") {
+ checkProof(
Proof(
(a, !a) |- b
)(
RuleIntroductionLeftNot(RuleParameters().withIndices(0)(1)()),
RuleHypothesis(RuleParameters().withIndices(0)(0)(1)) // FIXME shouldn't it be 0?
- ),
+ )
+ )
+ }
+
+ test("right not") {
+ checkProof(
Proof(
() |- (!a, a)
)(
RuleIntroductionRightNot(RuleParameters().withIndices(0)()(0)),
RuleHypothesis(RuleParameters().withIndices(0)(0)(0))
- ),
+ )
+ )
+ }
+
+ test("left =") {
+ checkProof(
Proof(
() |- (t === t)
)(
RuleEliminationLeftRefl(RuleParameters().withFunction(Notations.s, t)),
RuleHypothesis()
- ),
+ )
+ )
+ }
+
+ test("right =") {
+ checkProof(
Proof(
() |- (t === t)
)(
@@ -117,7 +178,7 @@ class ProofTests extends AnyFunSuite {
}
test("introduction higher order") {
- checkProofs(
+ checkProof(
Proof(
forall(x, u === x) |- (u === s)
)(
@@ -127,7 +188,12 @@ class ProofTests extends AnyFunSuite {
.withFunction(Notations.t, s)
),
RuleHypothesis()
- ),
+ )
+ )
+ }
+
+ test("right forall right or") {
+ checkProof(
Proof(
a |- forall(x, (u === x) \/ a)
)(
@@ -137,7 +203,12 @@ class ProofTests extends AnyFunSuite {
),
RuleIntroductionRightOr(),
RuleHypothesis()
- ),
+ )
+ )
+ }
+
+ test("left exists left and") {
+ checkProof(
Proof(
exists(x, (s === x) /\ a) |- a
)(
@@ -147,7 +218,12 @@ class ProofTests extends AnyFunSuite {
),
RuleIntroductionLeftAnd(),
RuleHypothesis()
- ),
+ )
+ )
+ }
+
+ test("right exists") {
+ checkProof(
Proof(
(s === t) |- exists(x, s === x)
)(
@@ -157,7 +233,12 @@ class ProofTests extends AnyFunSuite {
.withFunction(Notations.t, t)
),
RuleHypothesis()
- ),
+ )
+ )
+ }
+
+ test("left subst =") {
+ checkProof(
Proof(
(s === t, u === t) |- (u === s)
)(
@@ -166,7 +247,12 @@ class ProofTests extends AnyFunSuite {
.withPredicate(Notations.p, u === _)
),
RuleHypothesis()
- ),
+ )
+ )
+ }
+
+ test("right subst =") {
+ checkProof(
Proof(
(s === t, u === s) |- (u === t)
)(
@@ -175,7 +261,12 @@ class ProofTests extends AnyFunSuite {
.withPredicate(Notations.p, u === _)
),
RuleHypothesis()
- ),
+ )
+ )
+ }
+
+ test("left subst iff") {
+ checkProof(
Proof(
(a <=> b, c <=> b) |- (c <=> a)
)(
@@ -184,7 +275,12 @@ class ProofTests extends AnyFunSuite {
.withConnector(Notations.f, c <=> _)
),
RuleHypothesis()
- ),
+ )
+ )
+ }
+
+ test("right subst iff") {
+ checkProof(
Proof(
(a <=> b, c <=> a) |- (c <=> b)
)(
@@ -195,12 +291,10 @@ class ProofTests extends AnyFunSuite {
RuleHypothesis()
)
)
-
- // TODO remaining rules
}
- test("elimination rules") {
- checkProofs(
+ test("elimination left subst iff") {
+ checkProof(
Proof(
(s === t) |- (t === s)
)(
@@ -213,7 +307,12 @@ class ProofTests extends AnyFunSuite {
RuleHypothesis(),
TacticalRewrite((s === t) |- (s === t)),
RuleHypothesis()
- ),
+ )
+ )
+ }
+
+ test("elimination right subst iff") {
+ checkProof(
Proof(
(s === t) |- (t === s)
)(
@@ -226,7 +325,12 @@ class ProofTests extends AnyFunSuite {
RuleHypothesis(),
TacticalRewrite((s === t) |- (s === t)),
RuleHypothesis()
- ),
+ )
+ )
+ }
+
+ test("elimination left subst =") {
+ checkProof(
Proof(
(s === t, t === u) |- (s === u)
)(
@@ -238,7 +342,12 @@ class ProofTests extends AnyFunSuite {
),
RuleHypothesis(),
RuleHypothesis()
- ),
+ )
+ )
+ }
+
+ test("elimination right subst =") {
+ checkProof(
Proof(
(s === t, t === u) |- (s === u)
)(
@@ -278,9 +387,6 @@ class ProofTests extends AnyFunSuite {
val reconstructed = reconstructSCProofForTheorem(thm3)
- println(Printer.prettySCProof(reconstructed))
-
- assert(SCProofChecker.checkSCProof(reconstructed).isValid)
+ assert(SCProofChecker.checkSCProof(reconstructed).isValid, Printer.prettySCProof(reconstructed))
}
-*/
}