Skip to content
Snippets Groups Projects
Commit b6073fd7 authored by Katja Goltsova's avatar Katja Goltsova
Browse files

Improve error messaging in front ProofTests

In particular, supply clues when assertions fail and split the tests into
test cases to clearly see which tests pass and which fail.
parent d31c103c
No related branches found
No related tags found
4 merge requests!62Easy tactics,!58Easy tactics,!55Front integration and various changes,!41Clarify front tests
...@@ -17,98 +17,158 @@ class ProofTests extends AnyFunSuite { ...@@ -17,98 +17,158 @@ class ProofTests extends AnyFunSuite {
val (s, t, u) = (SchematicTermLabel[0]("s"), SchematicTermLabel[0]("t"), SchematicTermLabel[0]("u")) val (s, t, u) = (SchematicTermLabel[0]("s"), SchematicTermLabel[0]("t"), SchematicTermLabel[0]("u"))
val (x, y) = (VariableLabel("x"), VariableLabel("y")) val (x, y) = (VariableLabel("x"), VariableLabel("y"))
private def checkProofs(proofs: Proof*): Unit = { private def checkProof(proof: Proof): Unit = {
val emptyEnvironment: ProofEnvironment = newEmptyEnvironment() val emptyEnvironment: ProofEnvironment = newEmptyEnvironment()
proofs.foreach { proof => val result = evaluateProof(proof)(emptyEnvironment).map(reconstructSCProof)
val result = evaluateProof(proof)(emptyEnvironment).map(reconstructSCProof) assert(result.nonEmpty, s"kernel proof was empty for $proof")
assert(result.nonEmpty) val scProof = result.get._1
val scProof = result.get._1 val judgement = SCProofChecker.checkSCProof(scProof)
val judgement = SCProofChecker.checkSCProof(scProof) assert(judgement.isValid, Printer.prettySCProof(judgement))
println(Printer.prettySCProof(judgement)) assert(scProof.imports.isEmpty, s"proof unexpectedly uses imports: ${Printer.prettySCProof(judgement)}")
println() assert(
assert(judgement.isValid) lisa.kernel.proof.SequentCalculus.isSameSequent(scProof.conclusion, proof.initialState.goals.head),
assert(scProof.imports.isEmpty) s"proof does not prove ${Printer.prettySequent(proof.initialState.goals.head)}:\nPrinter.prettySCProof(judgement)"
assert(lisa.kernel.proof.SequentCalculus.isSameSequent(scProof.conclusion, proof.initialState.goals.head)) )
}
} }
test("introduction rules") { test("hypothesis") {
checkProofs( checkProof(
Proof( Proof(
(a, b /\ c) |- (b /\ c, b) (a, b /\ c) |- (b /\ c, b)
)( )(
RuleHypothesis(RuleParameters().withIndices(0)(1)(0)) RuleHypothesis(RuleParameters().withIndices(0)(1)(0))
), )
)
}
test("left and") {
checkProof(
Proof( Proof(
(a /\ b) |- a (a /\ b) |- a
)( )(
RuleIntroductionLeftAnd(), RuleIntroductionLeftAnd(),
RuleHypothesis(RuleParameters().withIndices(0)(0)(0)) RuleHypothesis(RuleParameters().withIndices(0)(0)(0))
), )
)
}
test("right and") {
checkProof(
Proof( Proof(
(a, b) |- (a /\ b) (a, b) |- (a /\ b)
)( )(
RuleIntroductionRightAnd(RuleParameters().withIndices(0)()(0)), RuleIntroductionRightAnd(RuleParameters().withIndices(0)()(0)),
RuleHypothesis(RuleParameters().withIndices(0)(0)(0)), RuleHypothesis(RuleParameters().withIndices(0)(0)(0)),
RuleHypothesis(RuleParameters().withIndices(0)(1)(0)) RuleHypothesis(RuleParameters().withIndices(0)(1)(0))
), )
)
}
test("left or") {
checkProof(
Proof( Proof(
(a \/ b) |- (a, b) (a \/ b) |- (a, b)
)( )(
RuleIntroductionLeftOr(RuleParameters().withIndices(0)(0)()), RuleIntroductionLeftOr(RuleParameters().withIndices(0)(0)()),
RuleHypothesis(RuleParameters().withIndices(0)(0)(0)), RuleHypothesis(RuleParameters().withIndices(0)(0)(0)),
RuleHypothesis(RuleParameters().withIndices(0)(0)(1)) RuleHypothesis(RuleParameters().withIndices(0)(0)(1))
), )
)
}
test("right or") {
checkProof(
Proof( Proof(
a |- (a \/ b) a |- (a \/ b)
)( )(
RuleIntroductionRightOr(RuleParameters().withIndices(0)()(0)), RuleIntroductionRightOr(RuleParameters().withIndices(0)()(0)),
RuleHypothesis(RuleParameters().withIndices(0)(0)(0)) RuleHypothesis(RuleParameters().withIndices(0)(0)(0))
), )
)
}
test("left implies") {
checkProof(
Proof( Proof(
(a ==> b, a) |- b (a ==> b, a) |- b
)( )(
RuleIntroductionLeftImplies(RuleParameters().withIndices(0)(0)()), RuleIntroductionLeftImplies(RuleParameters().withIndices(0)(0)()),
RuleHypothesis(RuleParameters().withIndices(0)(0)(1)), RuleHypothesis(RuleParameters().withIndices(0)(0)(1)),
RuleHypothesis(RuleParameters().withIndices(0)(1)(0)) RuleHypothesis(RuleParameters().withIndices(0)(1)(0))
), )
)
}
test("right implies") {
checkProof(
Proof( Proof(
() |- (a ==> a) () |- (a ==> a)
)( )(
RuleIntroductionRightImplies(RuleParameters().withIndices(0)()(0)), RuleIntroductionRightImplies(RuleParameters().withIndices(0)()(0)),
RuleHypothesis(RuleParameters().withIndices(0)(0)(0)) RuleHypothesis(RuleParameters().withIndices(0)(0)(0))
), )
)
}
test("left iff") {
checkProof(
Proof( Proof(
(a <=> b) |- (b ==> a) (a <=> b) |- (b ==> a)
)( )(
RuleIntroductionLeftIff(RuleParameters().withIndices(0)(0)()), RuleIntroductionLeftIff(RuleParameters().withIndices(0)(0)()),
RuleHypothesis(RuleParameters().withIndices(0)(1)(0)) RuleHypothesis(RuleParameters().withIndices(0)(1)(0))
), )
)
}
test("right iff") {
checkProof(
Proof( Proof(
(a ==> b, b ==> a) |- (a <=> b) (a ==> b, b ==> a) |- (a <=> b)
)( )(
RuleIntroductionRightIff(RuleParameters().withIndices(0)()(0)), RuleIntroductionRightIff(RuleParameters().withIndices(0)()(0)),
RuleHypothesis(RuleParameters().withIndices(0)(0)(0)), RuleHypothesis(RuleParameters().withIndices(0)(0)(0)),
RuleHypothesis(RuleParameters().withIndices(0)(1)(0)) RuleHypothesis(RuleParameters().withIndices(0)(1)(0))
), )
)
}
test("left not") {
checkProof(
Proof( Proof(
(a, !a) |- b (a, !a) |- b
)( )(
RuleIntroductionLeftNot(RuleParameters().withIndices(0)(1)()), RuleIntroductionLeftNot(RuleParameters().withIndices(0)(1)()),
RuleHypothesis(RuleParameters().withIndices(0)(0)(1)) // FIXME shouldn't it be 0? RuleHypothesis(RuleParameters().withIndices(0)(0)(1)) // FIXME shouldn't it be 0?
), )
)
}
test("right not") {
checkProof(
Proof( Proof(
() |- (!a, a) () |- (!a, a)
)( )(
RuleIntroductionRightNot(RuleParameters().withIndices(0)()(0)), RuleIntroductionRightNot(RuleParameters().withIndices(0)()(0)),
RuleHypothesis(RuleParameters().withIndices(0)(0)(0)) RuleHypothesis(RuleParameters().withIndices(0)(0)(0))
), )
)
}
test("left =") {
checkProof(
Proof( Proof(
() |- (t === t) () |- (t === t)
)( )(
RuleEliminationLeftRefl(RuleParameters().withFunction(Notations.s, t)), RuleEliminationLeftRefl(RuleParameters().withFunction(Notations.s, t)),
RuleHypothesis() RuleHypothesis()
), )
)
}
test("right =") {
checkProof(
Proof( Proof(
() |- (t === t) () |- (t === t)
)( )(
...@@ -118,7 +178,7 @@ class ProofTests extends AnyFunSuite { ...@@ -118,7 +178,7 @@ class ProofTests extends AnyFunSuite {
} }
test("introduction higher order") { test("introduction higher order") {
checkProofs( checkProof(
Proof( Proof(
forall(x, u === x) |- (u === s) forall(x, u === x) |- (u === s)
)( )(
...@@ -128,7 +188,12 @@ class ProofTests extends AnyFunSuite { ...@@ -128,7 +188,12 @@ class ProofTests extends AnyFunSuite {
.withFunction(Notations.t, s) .withFunction(Notations.t, s)
), ),
RuleHypothesis() RuleHypothesis()
), )
)
}
test("right forall right or") {
checkProof(
Proof( Proof(
a |- forall(x, (u === x) \/ a) a |- forall(x, (u === x) \/ a)
)( )(
...@@ -138,7 +203,12 @@ class ProofTests extends AnyFunSuite { ...@@ -138,7 +203,12 @@ class ProofTests extends AnyFunSuite {
), ),
RuleIntroductionRightOr(), RuleIntroductionRightOr(),
RuleHypothesis() RuleHypothesis()
), )
)
}
test("left exists left and") {
checkProof(
Proof( Proof(
exists(x, (s === x) /\ a) |- a exists(x, (s === x) /\ a) |- a
)( )(
...@@ -148,7 +218,12 @@ class ProofTests extends AnyFunSuite { ...@@ -148,7 +218,12 @@ class ProofTests extends AnyFunSuite {
), ),
RuleIntroductionLeftAnd(), RuleIntroductionLeftAnd(),
RuleHypothesis() RuleHypothesis()
), )
)
}
test("right exists") {
checkProof(
Proof( Proof(
(s === t) |- exists(x, s === x) (s === t) |- exists(x, s === x)
)( )(
...@@ -158,7 +233,12 @@ class ProofTests extends AnyFunSuite { ...@@ -158,7 +233,12 @@ class ProofTests extends AnyFunSuite {
.withFunction(Notations.t, t) .withFunction(Notations.t, t)
), ),
RuleHypothesis() RuleHypothesis()
), )
)
}
test("left subst =") {
checkProof(
Proof( Proof(
(s === t, u === t) |- (u === s) (s === t, u === t) |- (u === s)
)( )(
...@@ -167,7 +247,12 @@ class ProofTests extends AnyFunSuite { ...@@ -167,7 +247,12 @@ class ProofTests extends AnyFunSuite {
.withPredicate(Notations.p, u === _) .withPredicate(Notations.p, u === _)
), ),
RuleHypothesis() RuleHypothesis()
), )
)
}
test("right subst =") {
checkProof(
Proof( Proof(
(s === t, u === s) |- (u === t) (s === t, u === s) |- (u === t)
)( )(
...@@ -176,7 +261,12 @@ class ProofTests extends AnyFunSuite { ...@@ -176,7 +261,12 @@ class ProofTests extends AnyFunSuite {
.withPredicate(Notations.p, u === _) .withPredicate(Notations.p, u === _)
), ),
RuleHypothesis() RuleHypothesis()
), )
)
}
test("left subst iff") {
checkProof(
Proof( Proof(
(a <=> b, c <=> b) |- (c <=> a) (a <=> b, c <=> b) |- (c <=> a)
)( )(
...@@ -185,7 +275,12 @@ class ProofTests extends AnyFunSuite { ...@@ -185,7 +275,12 @@ class ProofTests extends AnyFunSuite {
.withConnector(Notations.f, c <=> _) .withConnector(Notations.f, c <=> _)
), ),
RuleHypothesis() RuleHypothesis()
), )
)
}
test("right subst iff") {
checkProof(
Proof( Proof(
(a <=> b, c <=> a) |- (c <=> b) (a <=> b, c <=> a) |- (c <=> b)
)( )(
...@@ -196,12 +291,10 @@ class ProofTests extends AnyFunSuite { ...@@ -196,12 +291,10 @@ class ProofTests extends AnyFunSuite {
RuleHypothesis() RuleHypothesis()
) )
) )
// TODO remaining rules
} }
test("elimination rules") { test("elimination left subst iff") {
checkProofs( checkProof(
Proof( Proof(
(s === t) |- (t === s) (s === t) |- (t === s)
)( )(
...@@ -214,7 +307,12 @@ class ProofTests extends AnyFunSuite { ...@@ -214,7 +307,12 @@ class ProofTests extends AnyFunSuite {
RuleHypothesis(), RuleHypothesis(),
TacticalRewrite((s === t) |- (s === t)), TacticalRewrite((s === t) |- (s === t)),
RuleHypothesis() RuleHypothesis()
), )
)
}
test("elimination right subst iff") {
checkProof(
Proof( Proof(
(s === t) |- (t === s) (s === t) |- (t === s)
)( )(
...@@ -227,7 +325,12 @@ class ProofTests extends AnyFunSuite { ...@@ -227,7 +325,12 @@ class ProofTests extends AnyFunSuite {
RuleHypothesis(), RuleHypothesis(),
TacticalRewrite((s === t) |- (s === t)), TacticalRewrite((s === t) |- (s === t)),
RuleHypothesis() RuleHypothesis()
), )
)
}
test("elimination left subst =") {
checkProof(
Proof( Proof(
(s === t, t === u) |- (s === u) (s === t, t === u) |- (s === u)
)( )(
...@@ -239,7 +342,12 @@ class ProofTests extends AnyFunSuite { ...@@ -239,7 +342,12 @@ class ProofTests extends AnyFunSuite {
), ),
RuleHypothesis(), RuleHypothesis(),
RuleHypothesis() RuleHypothesis()
), )
)
}
test("elimination right subst =") {
checkProof(
Proof( Proof(
(s === t, t === u) |- (s === u) (s === t, t === u) |- (s === u)
)( )(
...@@ -279,8 +387,6 @@ class ProofTests extends AnyFunSuite { ...@@ -279,8 +387,6 @@ class ProofTests extends AnyFunSuite {
val reconstructed = reconstructSCProofForTheorem(thm3) val reconstructed = reconstructSCProofForTheorem(thm3)
println(Printer.prettySCProof(reconstructed)) assert(SCProofChecker.checkSCProof(reconstructed).isValid, Printer.prettySCProof(reconstructed))
assert(SCProofChecker.checkSCProof(reconstructed).isValid)
} }
} }
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment