From cf545d8fa39b8f544e827ab5d96ba8a85bb23866 Mon Sep 17 00:00:00 2001
From: Katja Goltsova <katja.goltsova@protonmail.com>
Date: Fri, 1 Jul 2022 13:53:13 +0200
Subject: [PATCH] Add a test theory to facilitate writing proof assistant tests
---
.../src/test/scala/lisa/test/TestTheory.scala | 3 ++
.../scala/lisa/test/TestTheoryAxioms.scala | 31 +++++++++++++++++++
.../scala/lisa/test/TestTheoryLibrary.scala | 5 +++
3 files changed, 39 insertions(+)
create mode 100644 lisa-utils/src/test/scala/lisa/test/TestTheory.scala
create mode 100644 lisa-utils/src/test/scala/lisa/test/TestTheoryAxioms.scala
create mode 100644 lisa-utils/src/test/scala/lisa/test/TestTheoryLibrary.scala
diff --git a/lisa-utils/src/test/scala/lisa/test/TestTheory.scala b/lisa-utils/src/test/scala/lisa/test/TestTheory.scala
new file mode 100644
index 00000000..caf62e80
--- /dev/null
+++ b/lisa-utils/src/test/scala/lisa/test/TestTheory.scala
@@ -0,0 +1,3 @@
+package lisa.test
+
+object TestTheory extends TestTheoryAxioms {}
diff --git a/lisa-utils/src/test/scala/lisa/test/TestTheoryAxioms.scala b/lisa-utils/src/test/scala/lisa/test/TestTheoryAxioms.scala
new file mode 100644
index 00000000..151fdbb1
--- /dev/null
+++ b/lisa-utils/src/test/scala/lisa/test/TestTheoryAxioms.scala
@@ -0,0 +1,31 @@
+package lisa.test
+
+import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.RunningTheory
+import lisa.utils.Helpers.{_, given}
+
+trait TestTheoryAxioms {
+ final val p1 = ConstantPredicateLabel("p1", 1)
+ final val p2 = ConstantPredicateLabel("p2", 1)
+ final val f1 = ConstantFunctionLabel("f1", 1)
+ final val fixedElement = ConstantFunctionLabel("fixed_element", 0)
+ final val anotherFixed = ConstantFunctionLabel("another_element", 0)
+
+ val runningTestTheory = new RunningTheory()
+ runningTestTheory.addSymbol(p1)
+ runningTestTheory.addSymbol(p2)
+ runningTestTheory.addSymbol(f1)
+ runningTestTheory.addSymbol(fixedElement)
+ runningTestTheory.addSymbol(anotherFixed)
+
+ private final val x = VariableLabel("x")
+ final val p1_implies_p2: Formula = forall(x, p1(x) ==> p2(x))
+ final val ax2 = p1(fixedElement())
+ final val same_fixed = fixedElement() === anotherFixed()
+ final val fixed_point = forall(x, (f1(x) === fixedElement()) <=> (x === fixedElement()))
+
+ assert(runningTestTheory.addAxiom("p1_implies_p2", p1_implies_p2), "p1_implies_p2")
+ assert(runningTestTheory.addAxiom("A2", ax2), "ax2")
+ assert(runningTestTheory.addAxiom("same_fixed", same_fixed), "same fixed")
+ assert(runningTestTheory.addAxiom("fixed_point", fixed_point), "fixed point")
+}
diff --git a/lisa-utils/src/test/scala/lisa/test/TestTheoryLibrary.scala b/lisa-utils/src/test/scala/lisa/test/TestTheoryLibrary.scala
new file mode 100644
index 00000000..24315915
--- /dev/null
+++ b/lisa-utils/src/test/scala/lisa/test/TestTheoryLibrary.scala
@@ -0,0 +1,5 @@
+package lisa.test
+
+object TestTheoryLibrary extends lisa.utils.Library(TestTheory.runningTestTheory) {
+ export TestTheory.*
+}
--
GitLab