From e13332becc97782eb4e7c93f310165eed456e6fb Mon Sep 17 00:00:00 2001
From: Katja Goltsova <katja.goltsova@protonmail.com>
Date: Sat, 16 Jul 2022 20:25:03 +0200
Subject: [PATCH] Add a test to make sure that the path to the first invalid
proof step is reported correctly
---
.../lisa/kernel/InvalidProofPathTests.scala | 32 +++++++++++++++++++
1 file changed, 32 insertions(+)
create mode 100644 lisa-utils/src/test/scala/lisa/kernel/InvalidProofPathTests.scala
diff --git a/lisa-utils/src/test/scala/lisa/kernel/InvalidProofPathTests.scala b/lisa-utils/src/test/scala/lisa/kernel/InvalidProofPathTests.scala
new file mode 100644
index 00000000..257f5193
--- /dev/null
+++ b/lisa-utils/src/test/scala/lisa/kernel/InvalidProofPathTests.scala
@@ -0,0 +1,32 @@
+package lisa.kernel
+
+import lisa.kernel.proof.SCProofCheckerJudgement.SCInvalidProof
+import lisa.kernel.proof.SequentCalculus.*
+import lisa.kernel.proof._
+import lisa.test.ProofCheckerSuite
+import lisa.utils.Helpers.{_, given}
+
+class InvalidProofPathTests extends ProofCheckerSuite {
+ def checkPath(invalidProof: SCProof, expectedPath: Seq[Int]): Unit = {
+ val proofCheckResult = SCProofChecker.checkSCProof(invalidProof)
+ assert(!proofCheckResult.isValid, "expected invalid proof")
+ assert(proofCheckResult.isInstanceOf[SCInvalidProof], "invalid proof but valid proof checker judgement")
+ assert(proofCheckResult.asInstanceOf[SCInvalidProof].path === expectedPath)
+ }
+
+ test("incorrect step at top level") {
+ val eq0 = RightRefl(() |- s === s, s === s)
+ val eq1 = RightRefl(() |- t === t, t === t)
+ val wrongStep2 = Weakening(s === s |- s === t, 0)
+ val wrongStep3 = RightImplies(() |- (s === s) ==> (s === t), 1, s === s, s === t)
+ checkPath(SCProof(eq0, eq1, wrongStep2, wrongStep3), Seq(2))
+ }
+
+ test("nested incorrect step") {
+ val eq0 = RightRefl(() |- s === s, s === s)
+ val wrongStep1 = Weakening(s === s |- s === t, 0)
+ val erroneousSubproof = SCSubproof(SCProof(eq0, wrongStep1))
+ val nestedSubproof = SCSubproof(SCProof(erroneousSubproof, eq0))
+ checkPath(SCProof(eq0, eq0, eq0, nestedSubproof), Seq(3, 0, 1))
+ }
+}
--
GitLab