From b353b5a9009e1fbbc3a5727fc8287171f546e0b4 Mon Sep 17 00:00:00 2001
From: Katja Goltsova <katja.goltsova@protonmail.com>
Date: Wed, 12 Oct 2022 15:40:24 +0200
Subject: [PATCH] Test that creating a theorem with an incorrect statement
fails
---
.../lisa/utils/TheoriesHelpersTest.scala | 27 +++++++++++++++++++
1 file changed, 27 insertions(+)
create mode 100644 lisa-utils/src/test/scala/lisa/utils/TheoriesHelpersTest.scala
diff --git a/lisa-utils/src/test/scala/lisa/utils/TheoriesHelpersTest.scala b/lisa-utils/src/test/scala/lisa/utils/TheoriesHelpersTest.scala
new file mode 100644
index 00000000..5b6dd309
--- /dev/null
+++ b/lisa-utils/src/test/scala/lisa/utils/TheoriesHelpersTest.scala
@@ -0,0 +1,27 @@
+package lisa.utils
+
+import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.RunningTheoryJudgement.InvalidJustification
+import lisa.kernel.proof.SCProof
+import lisa.kernel.proof.SequentCalculus.Hypothesis
+import lisa.test.TestTheory
+import lisa.utils.Helpers.*
+import org.scalatest.funsuite.AnyFunSuite
+
+class TheoriesHelpersTest extends AnyFunSuite {
+ export TestTheory.*
+
+ test("theorem with incorrect statement") {
+ val (s0, s1) = (ConstantFunctionLabel("0", 0), ConstantFunctionLabel("1", 0))
+ runningTestTheory.addSymbol(s0)
+ runningTestTheory.addSymbol(s1)
+ val (c0, c1) = (s0(), s1())
+ val judgement = runningTestTheory.theorem("False theorem", "1 = 0", SCProof(Hypothesis((c0 === c1) |- (c0 === c1), c0 === c1)), Seq())
+ assert(!judgement.isValid)
+ assert(judgement == InvalidJustification("The proof does not prove the claimed statement", None))
+
+ // same theorem but with correct statement
+ assert(runningTestTheory.theorem("True theorem", "1 = 0 |- 1 = 0", SCProof(Hypothesis((c0 === c1) |- (c0 === c1), c0 === c1)), Seq()).isValid)
+ }
+
+}
--
GitLab