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 0000000000000000000000000000000000000000..5b6dd3092c7995a4aeb16092e0faa9ed486bfe62 --- /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) + } + +}