diff --git a/.gitignore b/.gitignore
index fa568cbdb0e80d1da85662228fb54b17815ba7e1..a784965e49d75566f0228551d1c380369cc481ca 100644
--- a/.gitignore
+++ b/.gitignore
@@ -16,3 +16,6 @@ target
silex/*
scallion/*
+
+# caching of theorems
+cache
\ No newline at end of file
diff --git a/build.sbt b/build.sbt
index a8d676f14d721174f4bf58a61d285a702c769b08..8a217a837bc141045ea76cef19341b7a42cc5a63 100644
--- a/build.sbt
+++ b/build.sbt
@@ -9,7 +9,7 @@ ThisBuild / versionScheme := Some("semver-spec")
ThisBuild / scalacOptions ++= Seq(
"-feature",
"-deprecation",
- "-unchecked"
+ "-unchecked",
)
ThisBuild / javacOptions ++= Seq("-encoding", "UTF-8")
ThisBuild / semanticdbEnabled := true
@@ -63,10 +63,7 @@ lazy val root = Project(
base = file(".")
)
.settings(commonSettings3)
- .settings(
- version := "0.1"
- )
- .dependsOn(kernel, withTests(utils)) // Everything but `examples`
+ .dependsOn(kernel, withTests(utils), withTests(sets)) // Everything but `examples`
.aggregate(utils) // To run tests on all modules
lazy val kernel = Project(
@@ -78,6 +75,13 @@ lazy val kernel = Project(
crossScalaVersions := Seq(scala3)
)
+lazy val sets = Project(
+ id = "lisa-sets",
+ base = file("lisa-sets")
+)
+ .settings(commonSettings3)
+ .dependsOn(kernel, withTests(utils))
+
lazy val utils = Project(
id = "lisa-utils",
base = file("lisa-utils")
diff --git a/lisa-examples/src/main/scala/Example.scala b/lisa-examples/src/main/scala/Example.scala
index 5254519235f1c444d464fe8707a42fb4f587fd80..17f272ab5ef77c947ff7beeb0eadc139ae1b43a7 100644
--- a/lisa-examples/src/main/scala/Example.scala
+++ b/lisa-examples/src/main/scala/Example.scala
@@ -1,4 +1,4 @@
-import lisa.prooflib.Substitution.{ApplyRules as Substitute}
+import lisa.automation.Substitution.{ApplyRules as Substitute}
object Example extends lisa.Main {
diff --git a/lisa-kernel/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
index 0965b225fe82e74a83a498df867688bcad941bfe..ee35a369898d54ab21fcb5c12c9f8823dd87d49d 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
@@ -1,6 +1,5 @@
package lisa.kernel.fol
-import java.lang
import scala.collection.mutable
import scala.math.Numeric.IntIsIntegral
diff --git a/lisa-kernel/src/main/scala/lisa/kernel/proof/RunningTheory.scala b/lisa-kernel/src/main/scala/lisa/kernel/proof/RunningTheory.scala
index 207f69ddaef6b172e2d36c16129fbadad5011d2c..b8bd954ed436b3e17281a1f335f62dea97b55fb3 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/proof/RunningTheory.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/proof/RunningTheory.scala
@@ -2,12 +2,10 @@ package lisa.kernel.proof
import lisa.kernel.fol.FOL._
import lisa.kernel.proof.RunningTheoryJudgement._
-import lisa.kernel.proof.SCProofChecker._
import lisa.kernel.proof.SequentCalculus._
import scala.collection.immutable.Set
import scala.collection.mutable.{Map => mMap}
-import scala.collection.mutable.{Set => mSet}
/**
* This class describes the theory, i.e. the context and language, in which theorems are proven.
diff --git a/lisa-sets/src/main/scala/lisa/Main.scala b/lisa-sets/src/main/scala/lisa/Main.scala
new file mode 100644
index 0000000000000000000000000000000000000000..3d21fb8f44ee9ba2550c06194b27d654c07865d4
--- /dev/null
+++ b/lisa-sets/src/main/scala/lisa/Main.scala
@@ -0,0 +1,32 @@
+package lisa
+
+import lisa.SetTheoryLibrary
+import lisa.prooflib.BasicMain
+
+/**
+ * The parent trait of all theory files containing mathematical development
+ */
+trait Main extends BasicMain {
+
+ export lisa.fol.FOL.{*, given}
+ export SetTheoryLibrary.{given, _}
+ export lisa.prooflib.BasicStepTactic.*
+ export lisa.prooflib.SimpleDeducedSteps.*
+
+ export lisa.automation.Tautology
+ export lisa.automation.Substitution
+ export lisa.automation.Tableau
+
+ knownDefs.update(emptySet, Some(emptySetAxiom))
+ knownDefs.update(unorderedPair, Some(pairAxiom))
+ knownDefs.update(union, Some(unionAxiom))
+ knownDefs.update(powerSet, Some(powerAxiom))
+ knownDefs.update(subset, Some(subsetAxiom))
+
+ extension (symbol: ConstantLabel[?]) {
+ def definition: JUSTIFICATION = {
+ getDefinition(symbol).get
+ }
+ }
+
+}
diff --git a/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala b/lisa-sets/src/main/scala/lisa/SetTheoryLibrary.scala
similarity index 55%
rename from src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
rename to lisa-sets/src/main/scala/lisa/SetTheoryLibrary.scala
index 192ff736a32165b38ac7f532830a8a56af23138e..27dec673f87586773f700f4e58f504d7e423eba8 100644
--- a/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
+++ b/lisa-sets/src/main/scala/lisa/SetTheoryLibrary.scala
@@ -1,17 +1,92 @@
-package lisa.settheory
+package lisa
import lisa.fol.FOL.{_, given}
-import lisa.utils.K
-import lisa.utils.K.makeAxiom
+import lisa.kernel.proof.RunningTheory
+import lisa.prooflib.Library
/**
- * Axioms for the Zermelo theory (Z)
+ * Specific implementation of [[utilities.Library]] for Set Theory, with a RunningTheory that is supposed to be used by the standard library.
*/
-private[settheory] trait SetTheoryZAxioms extends SetTheoryDefinitions {
+object SetTheoryLibrary extends lisa.prooflib.Library {
+
+ val theory = new RunningTheory()
+
+ // Predicates
+ /**
+ * The symbol for the set membership predicate.
+ */
+ final val in = ConstantPredicateLabel("elem", 2)
+
+ /**
+ * The symbol for the subset predicate.
+ */
+ final val subset = ConstantPredicateLabel("subsetOf", 2)
+
+ /**
+ * The symbol for the equicardinality predicate. Needed for Tarski's axiom.
+ */
+ final val sim = ConstantPredicateLabel("sameCardinality", 2) // Equicardinality
+ /**
+ * Set Theory basic predicates
+ */
+ final val predicates = Set(in, subset, sim)
+ // val choice
+
+ // Functions
+ /**
+ * The symbol for the empty set constant.
+ */
+ final val emptySet = Constant("emptySet")
+
+ /**
+ * The symbol for the unordered pair function.
+ */
+ final val unorderedPair = ConstantFunctionLabel("unorderedPair", 2)
+
+ /**
+ * The symbol for the powerset function.
+ */
+ final val powerSet = ConstantFunctionLabel("powerSet", 1)
+
+ /**
+ * The symbol for the set union function.
+ */
+ final val union = ConstantFunctionLabel("union", 1)
+
+ /**
+ * The symbol for the universe function. Defined in TG set theory.
+ */
+ final val universe = ConstantFunctionLabel("universe", 1)
+
+ /**
+ * Set Theory basic functions.
+ */
+ final val functions = Set(unorderedPair, powerSet, union, universe)
+
+ /**
+ * The kernel theory loaded with Set Theory symbols and axioms.
+ */
+ // val runningSetTheory: RunningTheory = new RunningTheory()
+ // given RunningTheory = runningSetTheory
+
+ predicates.foreach(s => addSymbol(s))
+ functions.foreach(s => addSymbol(s))
+ addSymbol(emptySet)
+
private val x = variable
private val y = variable
private val z = variable
final val φ = predicate[2]
+ private val A = variable
+ private val B = variable
+ private val P = predicate[3]
+
+ ////////////
+ // Axioms //
+ ////////////
+
+ // Z
+ ////////
/**
* Extensionality Axiom --- Two sets are equal iff they have the same
@@ -116,7 +191,38 @@ private[settheory] trait SetTheoryZAxioms extends SetTheoryDefinitions {
*/
final val foundationAxiom: AXIOM = Axiom(!(x === emptySet) ==> exists(y, in(y, x) /\ forall(z, in(z, x) ==> !in(z, y))))
- private val zAxioms: Set[(String, AXIOM)] = Set(
+ // ZF
+ /////////
+
+ /**
+ * Replacement Schema --- If a predicate `P` is 'functional' over `x`, i.e.,
+ * given `a ∈ x`, there is a unique `b` such that `P(x, a, b)`, then the
+ * 'image' of `x` in P exists and is a set. It contains exactly the `b`'s that
+ * satisfy `P` for each `a ∈ x`.
+ */
+ final val replacementSchema: AXIOM = Axiom(
+ forall(A, in(A, x) ==> existsOne(B, P(x, A, B))) ==>
+ exists(y, forall(B, in(B, y) <=> exists(A, in(A, x) /\ P(x, A, B))))
+ )
+
+ final val tarskiAxiom: AXIOM = Axiom(
+ forall(
+ x,
+ in(x, universe(x)) /\
+ forall(
+ y,
+ in(y, universe(x)) ==> (in(powerSet(y), universe(x)) /\ subset(powerSet(y), universe(x))) /\
+ forall(z, subset(z, universe(x)) ==> (sim(y, universe(x)) /\ in(y, universe(x))))
+ )
+ )
+ )
+
+ /**
+ * The set of all axioms of Tarski-Grothedick (TG) set theory.
+ *
+ * @return
+ */
+ def axioms: Set[(String, AXIOM)] = Set(
("EmptySet", emptySetAxiom),
("extensionalityAxiom", extensionalityAxiom),
("pairAxiom", pairAxiom),
@@ -125,9 +231,26 @@ private[settheory] trait SetTheoryZAxioms extends SetTheoryDefinitions {
("powerAxiom", powerAxiom),
("foundationAxiom", foundationAxiom),
("infinityAxiom", infinityAxiom),
- ("comprehensionSchema", comprehensionSchema)
+ ("comprehensionSchema", comprehensionSchema),
+ ("replacementSchema", replacementSchema),
+ ("TarskiAxiom", tarskiAxiom)
)
- override def axioms: Set[(String, AXIOM)] = super.axioms ++ zAxioms
+ /////////////
+ // Aliases //
+ /////////////
+
+ // Unicode symbols
+
+ val ∅ = emptySet
+ val ∈ = in
+
+ extension (thi: Term) {
+ def ∈(that: Term): Formula = in(thi, that)
+ def ⊆(that: Term): Formula = subset(thi, that)
+
+ def =/=(that: Term): Formula = !(===(thi, that))
+
+ }
}
diff --git a/src/main/scala/lisa/automation/kernel/CommonTactics.scala b/lisa-sets/src/main/scala/lisa/automation/CommonTactics.scala
similarity index 99%
rename from src/main/scala/lisa/automation/kernel/CommonTactics.scala
rename to lisa-sets/src/main/scala/lisa/automation/CommonTactics.scala
index 2c53f3ae55c90de3e03e8bf84f085f6bdcd3fb33..81b299ca867b5d09c74b427a4aef67ba5b49efd6 100644
--- a/src/main/scala/lisa/automation/kernel/CommonTactics.scala
+++ b/lisa-sets/src/main/scala/lisa/automation/CommonTactics.scala
@@ -1,6 +1,6 @@
package lisa.automation.kernel
-import lisa.automation.kernel.OLPropositionalSolver.Tautology
+import lisa.automation.Tautology
import lisa.fol.FOLHelpers.*
import lisa.fol.FOL as F
import lisa.prooflib.BasicStepTactic.*
diff --git a/lisa-utils/src/main/scala/lisa/prooflib/Substitution.scala b/lisa-sets/src/main/scala/lisa/automation/Substitution.scala
similarity index 99%
rename from lisa-utils/src/main/scala/lisa/prooflib/Substitution.scala
rename to lisa-sets/src/main/scala/lisa/automation/Substitution.scala
index b5e720b7b50a19a8807c6dfec096526c0e0a4d4a..31d7fad9104052e95131a0a9145e3ae2d722d86f 100644
--- a/lisa-utils/src/main/scala/lisa/prooflib/Substitution.scala
+++ b/lisa-sets/src/main/scala/lisa/automation/Substitution.scala
@@ -1,10 +1,11 @@
-package lisa.prooflib
+package lisa.automation
import lisa.fol.FOL as F
import lisa.kernel.proof.RunningTheory
import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SequentCalculus
import lisa.prooflib.BasicStepTactic.*
import lisa.prooflib.ProofTacticLib.{_, given}
+import lisa.prooflib.*
import lisa.utils.FOLPrinter
import lisa.utils.K
import lisa.utils.UserLisaException
diff --git a/src/main/scala/lisa/automation/Tableau.scala b/lisa-sets/src/main/scala/lisa/automation/Tableau.scala
similarity index 100%
rename from src/main/scala/lisa/automation/Tableau.scala
rename to lisa-sets/src/main/scala/lisa/automation/Tableau.scala
diff --git a/src/main/scala/lisa/automation/kernel/OLPropositionalSolver.scala b/lisa-sets/src/main/scala/lisa/automation/Tautology.scala
similarity index 77%
rename from src/main/scala/lisa/automation/kernel/OLPropositionalSolver.scala
rename to lisa-sets/src/main/scala/lisa/automation/Tautology.scala
index 0638854362af3130fb254343b56b5cb22ba084a9..d9bd7a2bb19ec824b1c709159b3d91b27fa1be6f 100644
--- a/src/main/scala/lisa/automation/kernel/OLPropositionalSolver.scala
+++ b/lisa-sets/src/main/scala/lisa/automation/Tautology.scala
@@ -1,65 +1,61 @@
-package lisa.automation.kernel
+package lisa.automation
+import lisa.automation.Substitution
import lisa.fol.FOL as F
import lisa.prooflib.Library
import lisa.prooflib.ProofTacticLib.*
-import lisa.prooflib.Substitution
import lisa.utils.K.{_, given}
-object OLPropositionalSolver {
+/**
+ * A tactic object dedicated to solve any propositionaly provable sequent (possibly in exponential time). Can be used with arbitrary many premises.
+ * Leverages the OL algorithm for scalafmpropositional logic.
+ */
+object Tautology extends ProofTactic with ProofSequentTactic with ProofFactSequentTactic {
/**
- * A tactic object dedicated to solve any propositionaly provable sequent (possibly in exponential time). Can be used with arbitrary many premises.
- * Leverages the OL algorithm for scalafmpropositional logic.
+ * Given a targeted conclusion sequent, try to prove it using laws of propositional logic and reflexivity and symmetry of equality.
+ *
+ * @param proof The ongoing proof object in which the step happens.
+ * @param bot The desired conclusion.
*/
- object Tautology extends ProofTactic with ProofSequentTactic with ProofFactSequentTactic {
-
- /**
- * Given a targeted conclusion sequent, try to prove it using laws of propositional logic and reflexivity and symmetry of equality.
- *
- * @param proof The ongoing proof object in which the step happens.
- * @param bot The desired conclusion.
- */
- def apply(using lib: Library, proof: lib.Proof)(bot: F.Sequent): proof.ProofTacticJudgement = {
- val botK = bot.underlying
- solveSequent(botK) match {
- case Left(value) => proof.ValidProofTactic(bot, value.steps, Seq())
- case Right((msg, seq)) => proof.InvalidProofTactic(msg)
- }
+ def apply(using lib: Library, proof: lib.Proof)(bot: F.Sequent): proof.ProofTacticJudgement = {
+ val botK = bot.underlying
+ solveSequent(botK) match {
+ case Left(value) => proof.ValidProofTactic(bot, value.steps, Seq())
+ case Right((msg, seq)) => proof.InvalidProofTactic(msg)
}
+ }
- /**
- * Given a targeted conclusion sequent, try to prove it using laws of propositional logic and reflexivity and symmetry of equality.
- * Uses the given already proven facts as assumptions to reach the desired goal.
- *
- * @param proof The ongoing proof object in which the step happens.
- * @param premise A previously proven step necessary to reach the conclusion.
- * @param bot The desired conclusion.
- */
- def apply(using lib: Library, proof: lib.Proof)(premise: proof.Fact)(bot: F.Sequent): proof.ProofTacticJudgement =
- from(using lib, proof)(Seq(premise)*)(bot)
-
- def from(using lib: Library, proof: lib.Proof)(premises: proof.Fact*)(bot: F.Sequent): proof.ProofTacticJudgement = {
- val botK = bot.underlying
- val premsFormulas: Seq[((proof.Fact, Formula), Int)] = premises.map(p => (p, sequentToFormula(proof.getSequent(p).underlying))).zipWithIndex
- val initProof = premsFormulas.map(s => Restate(() |- s._1._2, -(1 + s._2))).toList
- val sqToProve = botK ++<< (premsFormulas.map(s => s._1._2).toSet |- ())
-
- solveSequent(sqToProve) match {
- case Left(value) =>
- val subpr = SCSubproof(value)
- val stepsList = premsFormulas.foldLeft[List[SCProofStep]](List(subpr))((prev: List[SCProofStep], cur) => {
- val ((prem, form), position) = cur
- Cut(prev.head.bot -<< form, position, initProof.length + prev.length - 1, form) :: prev
- })
- val steps = (initProof ++ stepsList.reverse).toIndexedSeq
- proof.ValidProofTactic(bot, steps, premises)
- case Right((msg, seq)) =>
- proof.InvalidProofTactic(msg)
- }
+ /**
+ * Given a targeted conclusion sequent, try to prove it using laws of propositional logic and reflexivity and symmetry of equality.
+ * Uses the given already proven facts as assumptions to reach the desired goal.
+ *
+ * @param proof The ongoing proof object in which the step happens.
+ * @param premise A previously proven step necessary to reach the conclusion.
+ * @param bot The desired conclusion.
+ */
+ def apply(using lib: Library, proof: lib.Proof)(premise: proof.Fact)(bot: F.Sequent): proof.ProofTacticJudgement =
+ from(using lib, proof)(Seq(premise)*)(bot)
+
+ def from(using lib: Library, proof: lib.Proof)(premises: proof.Fact*)(bot: F.Sequent): proof.ProofTacticJudgement = {
+ val botK = bot.underlying
+ val premsFormulas: Seq[((proof.Fact, Formula), Int)] = premises.map(p => (p, sequentToFormula(proof.getSequent(p).underlying))).zipWithIndex
+ val initProof = premsFormulas.map(s => Restate(() |- s._1._2, -(1 + s._2))).toList
+ val sqToProve = botK ++<< (premsFormulas.map(s => s._1._2).toSet |- ())
+
+ solveSequent(sqToProve) match {
+ case Left(value) =>
+ val subpr = SCSubproof(value)
+ val stepsList = premsFormulas.foldLeft[List[SCProofStep]](List(subpr))((prev: List[SCProofStep], cur) => {
+ val ((prem, form), position) = cur
+ Cut(prev.head.bot -<< form, position, initProof.length + prev.length - 1, form) :: prev
+ })
+ val steps = (initProof ++ stepsList.reverse).toIndexedSeq
+ proof.ValidProofTactic(bot, steps, premises)
+ case Right((msg, seq)) =>
+ proof.InvalidProofTactic(msg)
}
-
- } // End of tactic object Tautology
+ }
/**
* This function returns a proof of the given sequent if such a proof exists using only the rules of propositional logic and reflexivity and symmetry of equality.
diff --git a/src/main/scala/lisa/automation/settheory/SetTheoryTactics.scala b/lisa-sets/src/main/scala/lisa/automation/settheory/SetTheoryTactics.scala
similarity index 91%
rename from src/main/scala/lisa/automation/settheory/SetTheoryTactics.scala
rename to lisa-sets/src/main/scala/lisa/automation/settheory/SetTheoryTactics.scala
index 3e3264e7f6e19bb5e630c2d494d1aeff696312d7..e36014f0df4a2e9baa582c4a0796250dfa99b95d 100644
--- a/src/main/scala/lisa/automation/settheory/SetTheoryTactics.scala
+++ b/lisa-sets/src/main/scala/lisa/automation/settheory/SetTheoryTactics.scala
@@ -1,18 +1,16 @@
package lisa.automation.settheory
-import lisa.automation.kernel.SimplePropositionalSolver.*
+import lisa.SetTheoryLibrary.{_, given}
+import lisa.fol.FOL.{_, given}
import lisa.kernel.proof.SequentCalculus as SC
-import lisa.mathematics.settheory.SetTheory
+import lisa.maths.settheory.SetTheory
import lisa.prooflib.BasicStepTactic.*
import lisa.prooflib.Library
import lisa.prooflib.ProofTacticLib.{_, given}
import lisa.prooflib.*
-import lisa.settheory.SetTheoryLibrary
-import lisa.utils.KernelHelpers.*
import lisa.utils.Printer
object SetTheoryTactics {
- import lisa.settheory.SetTheoryLibrary.{_, given}
// var defs
private val x = variable
private val y = variable
@@ -43,7 +41,7 @@ object SetTheoryTactics {
*/
object UniqueComprehension extends ProofTactic {
def apply(using
- proof: SetTheoryLibrary.Proof,
+ proof: Proof,
line: sourcecode.Line,
file: sourcecode.File,
om: OutputManager
@@ -51,7 +49,7 @@ object SetTheoryTactics {
bot: Sequent
): proof.ProofTacticJudgement = {
require(separationPredicate.bounds.length == 2) // separationPredicate takes two args
- given SetTheoryLibrary.type = SetTheoryLibrary
+ given lisa.SetTheoryLibrary.type = lisa.SetTheoryLibrary
// fresh variable names to avoid conflicts
val botWithAssumptions = bot ++ (proof.getAssumptions |- ())
val takenIDs = (botWithAssumptions.freeVariables ++ separationPredicate.body.freeVariables ++ originalSet.freeVariables).map(_.id)
diff --git a/src/main/scala/lisa/mathematics/fol/Quantifiers.scala b/lisa-sets/src/main/scala/lisa/maths/Quantifiers.scala
similarity index 97%
rename from src/main/scala/lisa/mathematics/fol/Quantifiers.scala
rename to lisa-sets/src/main/scala/lisa/maths/Quantifiers.scala
index 0d0a64c1339b6b8d7b3da80fdfbe68bff22d2018..67a1e6aa2bbab0796317b531360e273dc7be8bc2 100644
--- a/src/main/scala/lisa/mathematics/fol/Quantifiers.scala
+++ b/lisa-sets/src/main/scala/lisa/maths/Quantifiers.scala
@@ -1,10 +1,4 @@
-package lisa.mathematics
-package fol
-
-import lisa.automation.Tableau
-import lisa.automation.kernel.OLPropositionalSolver.Tautology
-import lisa.automation.kernel.SimplePropositionalSolver.*
-import lisa.prooflib.Substitution
+package lisa.maths
/**
* Implements theorems about first-order logic.
@@ -15,8 +9,6 @@ object Quantifiers extends lisa.Main {
private val y = variable
private val z = variable
private val a = variable
- private val b = variable
- private val c = variable
private val p = formulaVariable
private val P = predicate[1]
private val Q = predicate[1]
diff --git a/src/main/scala/lisa/mathematics/Ordinals.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/InductiveSets.scala
similarity index 92%
rename from src/main/scala/lisa/mathematics/Ordinals.scala
rename to lisa-sets/src/main/scala/lisa/maths/settheory/InductiveSets.scala
index 7298a4020992b0e8a0459b9b351b44dd45750d11..17a98e489822747f2d92ce8cc7537d6196ad9394 100644
--- a/src/main/scala/lisa/mathematics/Ordinals.scala
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/InductiveSets.scala
@@ -1,37 +1,25 @@
-package lisa.mathematics
+package lisa.maths
//import lisa.automation.settheory.SetTheoryTactics.*
-//import lisa.mathematics.fol.Quantifiers.*
-//import lisa.prooflib.Substitution
+//import lisa.maths.Quantifiers.*
+//import lisa.automation.Substitution
-import lisa.automation.kernel.OLPropositionalSolver.Tautology
-import lisa.automation.kernel.SimplePropositionalSolver.*
import lisa.automation.settheory.SetTheoryTactics.*
-import lisa.mathematics.settheory.SetTheory.*
+import lisa.maths.settheory.SetTheory.*
-object Ordinals extends lisa.Main {
+object InductiveSets extends lisa.Main {
// var defs
- private val w = variable
+ private val a = variable
private val x = variable
private val y = variable
private val z = variable
- private val h = formulaVariable
+ private val r = variable
private val t = variable
- private val a = variable
- private val b = variable
- private val c = variable
- private val d = variable
// relation and function symbols
- private val r = variable
- private val p = variable
- private val q = variable
- private val f = variable
- private val g = variable
private val P = predicate[1]
- private val Q = predicate[1]
private val schemPred = predicate[1]
/**
diff --git a/src/main/scala/lisa/mathematics/settheory/SetTheory.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/SetTheory.scala
similarity index 99%
rename from src/main/scala/lisa/mathematics/settheory/SetTheory.scala
rename to lisa-sets/src/main/scala/lisa/maths/settheory/SetTheory.scala
index b8a7973989607a75e584a5b8945eeea1a777c855..d52c226ec344474b61a6def280693b50643f0e43 100644
--- a/src/main/scala/lisa/mathematics/settheory/SetTheory.scala
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/SetTheory.scala
@@ -1,11 +1,8 @@
-package lisa.mathematics
-package settheory
+package lisa.maths.settheory
import lisa.automation.kernel.CommonTactics.Definition
-import lisa.automation.kernel.OLPropositionalSolver.Tautology
import lisa.automation.settheory.SetTheoryTactics.*
-import lisa.mathematics.fol.Quantifiers.*
-import lisa.prooflib.Substitution
+import lisa.maths.Quantifiers.*
/**
* Set Theory Library
@@ -34,7 +31,6 @@ object SetTheory extends lisa.Main {
// relation and function symbols
private val r = variable
private val p = variable
- private val q = variable
private val f = variable
private val g = variable
diff --git a/src/main/scala/lisa/mathematics/settheory/orderings/InclusionOrders.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/InclusionOrders.scala
similarity index 94%
rename from src/main/scala/lisa/mathematics/settheory/orderings/InclusionOrders.scala
rename to lisa-sets/src/main/scala/lisa/maths/settheory/orderings/InclusionOrders.scala
index 578777b5409d6e8bcc0bde99cf21306a88122e01..890d988a1aadc69e823152c933976a01743d0945 100644
--- a/src/main/scala/lisa/mathematics/settheory/orderings/InclusionOrders.scala
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/InclusionOrders.scala
@@ -1,19 +1,9 @@
-package lisa.mathematics
-package settheory
-package orderings
+package lisa.maths.settheory.orderings
-import lisa.automation.kernel.OLPropositionalSolver.Tautology
-import lisa.automation.kernel.SimplePropositionalSolver.*
import lisa.automation.settheory.SetTheoryTactics.*
-import lisa.kernel.proof.SequentCalculus as SC
-import lisa.mathematics.fol.Quantifiers.*
-import lisa.mathematics.settheory.SetTheory.*
-import lisa.mathematics.settheory.orderings.PartialOrders.*
-import lisa.prooflib.BasicStepTactic.*
-import lisa.prooflib.Library
-import lisa.prooflib.ProofTacticLib
-import lisa.prooflib.Substitution
-import lisa.utils.FOLPrinter
+import lisa.maths.Quantifiers.*
+import lisa.maths.settheory.SetTheory.*
+import lisa.maths.settheory.orderings.PartialOrders.*
object InclusionOrders extends lisa.Main {
diff --git a/src/main/scala/lisa/mathematics/settheory/orderings/Induction.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Induction.scala
similarity index 93%
rename from src/main/scala/lisa/mathematics/settheory/orderings/Induction.scala
rename to lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Induction.scala
index 3323a2987871089c033a3da94eba620d1d122f77..e57c06834cc5d2d7aab8467e51ff8f13e4f57a87 100644
--- a/src/main/scala/lisa/mathematics/settheory/orderings/Induction.scala
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Induction.scala
@@ -1,50 +1,31 @@
-package lisa.mathematics
-package settheory
-package orderings
+package lisa.maths.settheory.orderings
-import lisa.automation.kernel.OLPropositionalSolver.Tautology
-import lisa.automation.kernel.SimplePropositionalSolver.*
import lisa.automation.settheory.SetTheoryTactics.*
-import lisa.kernel.proof.SequentCalculus as SC
-import lisa.mathematics.fol.Quantifiers.*
-import lisa.mathematics.settheory.SetTheory.*
-import lisa.mathematics.settheory.orderings.InclusionOrders.*
-import lisa.mathematics.settheory.orderings.Ordinals.*
-import lisa.mathematics.settheory.orderings.PartialOrders.*
-import lisa.mathematics.settheory.orderings.Segments.*
-import lisa.mathematics.settheory.orderings.WellOrders.*
-import lisa.prooflib.BasicStepTactic.*
-import lisa.prooflib.Library
-import lisa.prooflib.ProofTacticLib
-import lisa.prooflib.Substitution
-import lisa.utils.FOLPrinter
+import lisa.maths.Quantifiers.*
+import lisa.maths.settheory.SetTheory.*
+import lisa.maths.settheory.orderings.InclusionOrders.*
+import lisa.maths.settheory.orderings.Ordinals.*
+import lisa.maths.settheory.orderings.PartialOrders.*
+import lisa.maths.settheory.orderings.Segments.*
+import lisa.maths.settheory.orderings.WellOrders.*
object Induction extends lisa.Main {
// var defs
+ private val a = variable
+ private val b = variable
+ private val p = variable
+ private val r = variable
+ private val t = variable
private val w = variable
private val x = variable
private val y = variable
private val z = variable
- private val h = formulaVariable
- private val t = variable
- private val a = variable
- private val b = variable
- private val c = variable
- private val d = variable
// relation and function symbols
- private val r = variable
- private val p = variable
- private val q = variable
- private val f = variable
- private val g = variable
- private val F = function[1]
- private val G = function[2]
private val P = predicate[1]
private val Q = predicate[1]
- private val schemPred = predicate[1]
/**
* Theorem --- Well Ordered Induction on a Subclass
diff --git a/src/main/scala/lisa/mathematics/settheory/orderings/Orderings.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Orderings.scala
similarity index 50%
rename from src/main/scala/lisa/mathematics/settheory/orderings/Orderings.scala
rename to lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Orderings.scala
index 03911abc3a540ac51eddc22c0ec4bd126d041aa9..618d1fa2614483ebf6c4b3d578d4120b65535346 100644
--- a/src/main/scala/lisa/mathematics/settheory/orderings/Orderings.scala
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Orderings.scala
@@ -1,6 +1,4 @@
-package lisa.mathematics
-package settheory
-package orderings
+package lisa.maths.settheory.orderings
object Orderings {
// export everything in this package
diff --git a/src/main/scala/lisa/mathematics/settheory/orderings/Ordinals.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Ordinals.scala
similarity index 96%
rename from src/main/scala/lisa/mathematics/settheory/orderings/Ordinals.scala
rename to lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Ordinals.scala
index 1a63add0a8bf382e5c3e3ccf01832dcd7e768d3c..5dd1ed309283907f5d2255480828b13b3dbffd57 100644
--- a/src/main/scala/lisa/mathematics/settheory/orderings/Ordinals.scala
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Ordinals.scala
@@ -1,21 +1,11 @@
-package lisa.mathematics
-package settheory
-package orderings
+package lisa.maths.settheory.orderings
-import lisa.automation.kernel.OLPropositionalSolver.Tautology
-import lisa.automation.kernel.SimplePropositionalSolver.*
import lisa.automation.settheory.SetTheoryTactics.*
-import lisa.kernel.proof.SequentCalculus as SC
-import lisa.mathematics.fol.Quantifiers.*
-import lisa.mathematics.settheory.SetTheory.*
-import lisa.mathematics.settheory.orderings.InclusionOrders.*
-import lisa.mathematics.settheory.orderings.PartialOrders.*
-import lisa.mathematics.settheory.orderings.WellOrders.*
-import lisa.prooflib.BasicStepTactic.*
-import lisa.prooflib.Library
-import lisa.prooflib.ProofTacticLib
-import lisa.prooflib.Substitution
-import lisa.utils.FOLPrinter
+import lisa.maths.Quantifiers.*
+import lisa.maths.settheory.SetTheory.*
+import lisa.maths.settheory.orderings.InclusionOrders.*
+import lisa.maths.settheory.orderings.PartialOrders.*
+import lisa.maths.settheory.orderings.WellOrders.*
object Ordinals extends lisa.Main {
diff --git a/src/main/scala/lisa/mathematics/settheory/orderings/PartialOrders.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/PartialOrders.scala
similarity index 96%
rename from src/main/scala/lisa/mathematics/settheory/orderings/PartialOrders.scala
rename to lisa-sets/src/main/scala/lisa/maths/settheory/orderings/PartialOrders.scala
index a78057478afcf791ef237bfad9acdf6789c37419..52df62f107f14dc61b1ea0143d31f20e2af3b48e 100644
--- a/src/main/scala/lisa/mathematics/settheory/orderings/PartialOrders.scala
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/PartialOrders.scala
@@ -1,18 +1,8 @@
-package lisa.mathematics
-package settheory
-package orderings
+package lisa.maths.settheory.orderings
-import lisa.automation.kernel.OLPropositionalSolver.Tautology
-import lisa.automation.kernel.SimplePropositionalSolver.*
import lisa.automation.settheory.SetTheoryTactics.*
-import lisa.kernel.proof.SequentCalculus as SC
-import lisa.mathematics.fol.Quantifiers.*
-import lisa.mathematics.settheory.SetTheory.*
-import lisa.prooflib.BasicStepTactic.*
-import lisa.prooflib.Library
-import lisa.prooflib.ProofTacticLib
-import lisa.prooflib.Substitution
-import lisa.utils.FOLPrinter
+import lisa.maths.Quantifiers.*
+import lisa.maths.settheory.SetTheory.*
object PartialOrders extends lisa.Main {
diff --git a/src/main/scala/lisa/mathematics/settheory/orderings/Recursion.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Recursion.scala
similarity index 99%
rename from src/main/scala/lisa/mathematics/settheory/orderings/Recursion.scala
rename to lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Recursion.scala
index 0335436562f643c385b6b084c2c3a27c69c39881..5308dac92fef35f0492b6221b028c6cae37ddbd5 100644
--- a/src/main/scala/lisa/mathematics/settheory/orderings/Recursion.scala
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Recursion.scala
@@ -1,24 +1,14 @@
-package lisa.mathematics
-package settheory
-package orderings
+package lisa.maths.settheory.orderings
-import lisa.automation.kernel.OLPropositionalSolver.Tautology
-import lisa.automation.kernel.SimplePropositionalSolver.*
import lisa.automation.settheory.SetTheoryTactics.*
-import lisa.kernel.proof.SequentCalculus as SC
-import lisa.mathematics.fol.Quantifiers.*
-import lisa.mathematics.settheory.SetTheory.*
-import lisa.mathematics.settheory.orderings.InclusionOrders.*
-import lisa.mathematics.settheory.orderings.Induction.*
-import lisa.mathematics.settheory.orderings.Ordinals.*
-import lisa.mathematics.settheory.orderings.PartialOrders.*
-import lisa.mathematics.settheory.orderings.Segments.*
-import lisa.mathematics.settheory.orderings.WellOrders.*
-import lisa.prooflib.BasicStepTactic.*
-import lisa.prooflib.Library
-import lisa.prooflib.ProofTacticLib
-import lisa.prooflib.Substitution
-import lisa.utils.FOLPrinter
+import lisa.maths.Quantifiers.*
+import lisa.maths.settheory.SetTheory.*
+import lisa.maths.settheory.orderings.InclusionOrders.*
+import lisa.maths.settheory.orderings.Induction.*
+import lisa.maths.settheory.orderings.Ordinals.*
+import lisa.maths.settheory.orderings.PartialOrders.*
+import lisa.maths.settheory.orderings.Segments.*
+import lisa.maths.settheory.orderings.WellOrders.*
/**
* This file is dedicated to proving the well-ordered and transfinite recursion
diff --git a/src/main/scala/lisa/mathematics/settheory/orderings/Segments.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Segments.scala
similarity index 92%
rename from src/main/scala/lisa/mathematics/settheory/orderings/Segments.scala
rename to lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Segments.scala
index ab9b2dde099e43f3988045a2d78979a2f824c363..0ecd5aae7f41f37d936900c0e1019ad25991dc71 100644
--- a/src/main/scala/lisa/mathematics/settheory/orderings/Segments.scala
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Segments.scala
@@ -1,21 +1,12 @@
-package lisa.mathematics
-package settheory
-package orderings
+package lisa.maths.settheory.orderings
-import lisa.automation.kernel.OLPropositionalSolver.Tautology
-import lisa.automation.kernel.SimplePropositionalSolver.*
import lisa.automation.settheory.SetTheoryTactics.*
-import lisa.kernel.proof.SequentCalculus as SC
-import lisa.mathematics.fol.Quantifiers.*
-import lisa.mathematics.settheory.SetTheory.*
-import lisa.mathematics.settheory.orderings.InclusionOrders.*
-import lisa.mathematics.settheory.orderings.Ordinals.*
-import lisa.mathematics.settheory.orderings.PartialOrders.*
-import lisa.mathematics.settheory.orderings.WellOrders.*
-import lisa.prooflib.BasicStepTactic.*
-import lisa.prooflib.Library
-import lisa.prooflib.ProofTacticLib
-import lisa.utils.FOLPrinter
+import lisa.maths.Quantifiers.*
+import lisa.maths.settheory.SetTheory.*
+import lisa.maths.settheory.orderings.InclusionOrders.*
+import lisa.maths.settheory.orderings.Ordinals.*
+import lisa.maths.settheory.orderings.PartialOrders.*
+import lisa.maths.settheory.orderings.WellOrders.*
object Segments extends lisa.Main {
diff --git a/src/main/scala/lisa/mathematics/settheory/orderings/WellOrders.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/WellOrders.scala
similarity index 90%
rename from src/main/scala/lisa/mathematics/settheory/orderings/WellOrders.scala
rename to lisa-sets/src/main/scala/lisa/maths/settheory/orderings/WellOrders.scala
index 3c7eecab8d489ccda251fea839f98046fff83d61..01e68326c0d5a0b03de74fd0b4f680db6aec9961 100644
--- a/src/main/scala/lisa/mathematics/settheory/orderings/WellOrders.scala
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/WellOrders.scala
@@ -1,20 +1,10 @@
-package lisa.mathematics
-package settheory
-package orderings
+package lisa.maths.settheory.orderings
-import lisa.automation.kernel.OLPropositionalSolver.Tautology
-import lisa.automation.kernel.SimplePropositionalSolver.*
import lisa.automation.settheory.SetTheoryTactics.*
-import lisa.kernel.proof.SequentCalculus as SC
-import lisa.mathematics.fol.Quantifiers.*
-import lisa.mathematics.settheory.SetTheory.*
-import lisa.mathematics.settheory.orderings.InclusionOrders.*
-import lisa.mathematics.settheory.orderings.PartialOrders.*
-import lisa.prooflib.BasicStepTactic.*
-import lisa.prooflib.Library
-import lisa.prooflib.ProofTacticLib
-import lisa.prooflib.Substitution
-import lisa.utils.FOLPrinter
+import lisa.maths.Quantifiers.*
+import lisa.maths.settheory.SetTheory.*
+import lisa.maths.settheory.orderings.InclusionOrders.*
+import lisa.maths.settheory.orderings.PartialOrders.*
object WellOrders extends lisa.Main {
diff --git a/src/test/scala/lisa/automation/TableauTest.scala b/lisa-sets/src/test/scala/lisa/automation/TableauTest.scala
similarity index 97%
rename from src/test/scala/lisa/automation/TableauTest.scala
rename to lisa-sets/src/test/scala/lisa/automation/TableauTest.scala
index 4e11402ec8396ec594bbddcd14411c7eeb3793be..70a5ae10c32d7b0c6b8b0f7f9b607ec71c49c7fe 100644
--- a/src/test/scala/lisa/automation/TableauTest.scala
+++ b/lisa-sets/src/test/scala/lisa/automation/TableauTest.scala
@@ -1,9 +1,10 @@
package lisa.test.automation
-import lisa.automation.Tableau._
+import lisa.SetTheoryLibrary.{_, given}
+import lisa.automation.Substitution.*
+import lisa.automation.Tableau.*
+import lisa.fol.FOL.*
import lisa.prooflib.Exports.*
-import lisa.prooflib.Substitution.*
-import lisa.settheory.SetTheoryLibrary.{_, given}
import lisa.utils.K.SCProofChecker.checkSCProof
import lisa.utils.parsing.FOLPrinter.prettyFormula
import lisa.utils.parsing.FOLPrinter.prettySCProof
diff --git a/src/test/scala/lisa/examples/peano_example/Peano.scala b/lisa-sets/src/test/scala/lisa/examples/peano_example/Peano.scala
similarity index 100%
rename from src/test/scala/lisa/examples/peano_example/Peano.scala
rename to lisa-sets/src/test/scala/lisa/examples/peano_example/Peano.scala
diff --git a/src/test/scala/lisa/examples/peano_example/PeanoArithmetics.scala b/lisa-sets/src/test/scala/lisa/examples/peano_example/PeanoArithmetics.scala
similarity index 100%
rename from src/test/scala/lisa/examples/peano_example/PeanoArithmetics.scala
rename to lisa-sets/src/test/scala/lisa/examples/peano_example/PeanoArithmetics.scala
diff --git a/src/test/scala/lisa/examples/peano_example/PeanoArithmeticsLibrary.scala b/lisa-sets/src/test/scala/lisa/examples/peano_example/PeanoArithmeticsLibrary.scala
similarity index 100%
rename from src/test/scala/lisa/examples/peano_example/PeanoArithmeticsLibrary.scala
rename to lisa-sets/src/test/scala/lisa/examples/peano_example/PeanoArithmeticsLibrary.scala
diff --git a/src/test/scala/lisa/proven/InitialProofsTests.scala b/lisa-sets/src/test/scala/lisa/proven/InitialProofsTests.scala
similarity index 88%
rename from src/test/scala/lisa/proven/InitialProofsTests.scala
rename to lisa-sets/src/test/scala/lisa/proven/InitialProofsTests.scala
index 7a51617ef43fc78b874b5b31f9f92016b23c1edb..9800e4fe9df4a314779c7ef0b8d57870964eb9c5 100644
--- a/src/test/scala/lisa/proven/InitialProofsTests.scala
+++ b/lisa-sets/src/test/scala/lisa/proven/InitialProofsTests.scala
@@ -4,7 +4,7 @@ import lisa.test.ProofCheckerSuite
import lisa.utils.Printer
class InitialProofsTests extends ProofCheckerSuite {
- import lisa.settheory.SetTheoryLibrary.*
+ import lisa.SetTheoryLibrary.*
/*
test("File SetTheory initialize well") {
diff --git a/src/test/scala/lisa/utilities/SerializationTest.scala b/lisa-sets/src/test/scala/lisa/utilities/SerializationTest.scala
similarity index 92%
rename from src/test/scala/lisa/utilities/SerializationTest.scala
rename to lisa-sets/src/test/scala/lisa/utilities/SerializationTest.scala
index da2ba1aa5de8d535300ba6020f8315ef9e1ee609..29826e761ba1afd7b35d42b58aa330857970b566 100644
--- a/src/test/scala/lisa/utilities/SerializationTest.scala
+++ b/lisa-sets/src/test/scala/lisa/utilities/SerializationTest.scala
@@ -1,5 +1,6 @@
package lisa.test.utils
+import lisa.automation.Tautology
import lisa.test.automation.TableauTest
import lisa.utils.K
import lisa.utils.K.getJustification
@@ -28,8 +29,8 @@ class SerializationTest extends AnyFunSuite {
def testMulti(theory: K.RunningTheory, thms: List[(String, K.SCProof, List[theory.Justification])]) = {
thmsToFile(testfile, theory, thms.map(thm => (thm._1, thm._2, thm._3.map(("test", _)))))
val thm = thmsFromFile(testfile, theory)
- File(testfile + "test.trees").delete()
- File(testfile + "test.proof").delete()
+ File(testfile + ".trees").delete()
+ File(testfile + ".proof").delete()
thm
}
@@ -54,7 +55,7 @@ class SerializationTest extends AnyFunSuite {
try {
val formula = p._2
val no = p._1
- val proof = lisa.automation.kernel.OLPropositionalSolver.solveSequent(() |- formula.underlying) match {
+ val proof = Tautology.solveSequent(() |- formula.underlying) match {
case Left(proof) => proof
case Right(_) => throw new Exception("OLPropositionalSolver failed to prove a tautology")
}
@@ -88,7 +89,7 @@ class SerializationTest extends AnyFunSuite {
try {
val formula = p._2
val no = p._1
- val proof = lisa.automation.kernel.OLPropositionalSolver.solveSequent(() |- formula.underlying) match {
+ val proof = Tautology.solveSequent(() |- formula.underlying) match {
case Left(proof) => proof
case Right(_) => throw new Exception("OLPropositionalSolver failed to prove a tautology")
}
@@ -132,7 +133,7 @@ class SerializationTest extends AnyFunSuite {
}
test("exporting a proof to a file and back should work, with imports") {
- import lisa.mathematics.settheory.SetTheory as ST
+ import lisa.maths.settheory.SetTheory as ST
val thms = List(
// ("russelsParadox", ST.russelsParadox),
("setUnionMembership", ST.setUnionMembership),
@@ -155,7 +156,7 @@ class SerializationTest extends AnyFunSuite {
}
test("exporting multiple theorems at once to a file and back should work") {
- import lisa.mathematics.settheory.SetTheory as ST
+ import lisa.maths.settheory.SetTheory as ST
val thms = List(
// ("russelsParadox", ST.russelsParadox),
("setUnionMembership", ST.setUnionMembership),
diff --git a/src/test/scala/lisa/utilities/SubstitutionTacticTest.scala b/lisa-sets/src/test/scala/lisa/utilities/SubstitutionTacticTest.scala
similarity index 97%
rename from src/test/scala/lisa/utilities/SubstitutionTacticTest.scala
rename to lisa-sets/src/test/scala/lisa/utilities/SubstitutionTacticTest.scala
index 4cfa4205259d5b9962443416c1091d32f6b94392..b69b8e4ef07359092288dc8dcd43cf9bde9cc5af 100644
--- a/src/test/scala/lisa/utilities/SubstitutionTacticTest.scala
+++ b/lisa-sets/src/test/scala/lisa/utilities/SubstitutionTacticTest.scala
@@ -1,8 +1,9 @@
-package lisa.test.utils
+package lisa.automation
+import lisa.automation.Substitution
import lisa.kernel.proof.RunningTheory
import lisa.kernel.proof.SequentCalculus as SC
-import lisa.prooflib.Substitution
+import lisa.test.ProofTacticTestLib
import lisa.utils.parsing.FOLParser.*
import lisa.utils.parsing.FOLPrinter.*
import org.scalatest.funsuite.AnyFunSuite
diff --git a/lisa-utils/src/main/scala/lisa/utils/LisaException.scala b/lisa-utils/src/main/scala/lisa/utils/LisaException.scala
index dcef0ce6b31ad1f542b028e077eccb59c445d671..6d141d3900712e69ec45f91d6dad88a99ff2928b 100644
--- a/lisa-utils/src/main/scala/lisa/utils/LisaException.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/LisaException.scala
@@ -47,6 +47,7 @@ object UserLisaException {
class InvalidProofFromFileException(errorMessage: String, file: String)(using sourcecode.Line, sourcecode.File) extends UserLisaException(errorMessage) {
def showError: String = errorMessage
}
+
class InvalidAxiomException(errorMessage: String, name: String, formula: lisa.fol.FOL.Formula, library: lisa.prooflib.Library)(using sourcecode.Line, sourcecode.File)
extends UserLisaException(errorMessage) {
def showError: String = s"The desired axiom \"$name\" contains symbol that are not part of the theory.\n" +
diff --git a/lisa-utils/src/main/scala/lisa/utils/SecondOrderMatcher.scala b/lisa-utils/src/main/scala/lisa/utils/SecondOrderMatcher.scala
deleted file mode 100644
index 91641895c646299cdcbacf2fa720d68d60fbc145..0000000000000000000000000000000000000000
--- a/lisa-utils/src/main/scala/lisa/utils/SecondOrderMatcher.scala
+++ /dev/null
@@ -1,17 +0,0 @@
-package lisa.utils
-
-import lisa.kernel.fol.FOL.*
-
-// TODO: connectors?
-
-object SecondOrderMatcher {
- case class Matching(predicates: Map[SchematicPredicateLabel, LambdaTermTerm], functions: Map[SchematicFunctionLabel, LambdaTermFormula])
-
- private case class Renaming()
-
-// def findMatching(patterns: Seq[Formula], target: Seq[Formula]): Option[Matching] = {}
-
- // TODO: error reporting?
- private def isCorrectInput(patterns: Seq[Formula], target: Seq[Formula]): Boolean = ???
-
-}
diff --git a/lisa-utils/src/main/scala/lisa/utils/Serialization.scala b/lisa-utils/src/main/scala/lisa/utils/Serialization.scala
index d89d473f7c98be058aed74279a12372e08fa8d5e..8abcd231a65c284edc30f0618e059f18abe4b75a 100644
--- a/lisa-utils/src/main/scala/lisa/utils/Serialization.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/Serialization.scala
@@ -650,8 +650,6 @@ object Serialization {
try {
Class.forName(obj + "$").getField("MODULE$").get(null)
} catch { case _ => "Not found: " + obj }
- Class.forName("lisa.settheory.SetTheoryLibrary" + "$").getField("MODULE$").get(null)
-
j(0) match
case 'a' => theory.getAxiom(name).get
case 't' =>
diff --git a/lisa-utils/src/test/scala/lisa/test/ProofCheckerSuite.scala b/lisa-utils/src/test/scala/lisa/ProofCheckerSuite.scala
similarity index 100%
rename from lisa-utils/src/test/scala/lisa/test/ProofCheckerSuite.scala
rename to lisa-utils/src/test/scala/lisa/ProofCheckerSuite.scala
diff --git a/lisa-utils/src/test/scala/lisa/test/utils/ProofTacticTestLib.scala b/lisa-utils/src/test/scala/lisa/ProofTacticTestLib.scala
similarity index 95%
rename from lisa-utils/src/test/scala/lisa/test/utils/ProofTacticTestLib.scala
rename to lisa-utils/src/test/scala/lisa/ProofTacticTestLib.scala
index 5d7ccd074dbd1c53be9350b867fabab26ba57175..ebecd9b39fd2e75575456a1f4ecb06dd75dd72f2 100644
--- a/lisa-utils/src/test/scala/lisa/test/utils/ProofTacticTestLib.scala
+++ b/lisa-utils/src/test/scala/lisa/ProofTacticTestLib.scala
@@ -1,4 +1,4 @@
-package lisa.test.utils
+package lisa.test
import lisa.kernel.proof.SequentCalculus as SC
import lisa.prooflib.BasicMain
@@ -9,7 +9,7 @@ import org.scalatest.funsuite.AnyFunSuite
import scala.collection.immutable.LazyList
-class ProofTacticTestLib extends AnyFunSuite with BasicMain {
+trait ProofTacticTestLib extends AnyFunSuite with BasicMain {
export lisa.test.TestTheoryLibrary.{_, given}
diff --git a/lisa-utils/src/test/scala/lisa/test/TestTheory.scala b/lisa-utils/src/test/scala/lisa/TestTheory.scala
similarity index 100%
rename from lisa-utils/src/test/scala/lisa/test/TestTheory.scala
rename to lisa-utils/src/test/scala/lisa/TestTheory.scala
diff --git a/lisa-utils/src/test/scala/lisa/test/TestTheoryAxioms.scala b/lisa-utils/src/test/scala/lisa/TestTheoryAxioms.scala
similarity index 100%
rename from lisa-utils/src/test/scala/lisa/test/TestTheoryAxioms.scala
rename to lisa-utils/src/test/scala/lisa/TestTheoryAxioms.scala
diff --git a/lisa-utils/src/test/scala/lisa/test/TestTheoryLibrary.scala b/lisa-utils/src/test/scala/lisa/TestTheoryLibrary.scala
similarity index 100%
rename from lisa-utils/src/test/scala/lisa/test/TestTheoryLibrary.scala
rename to lisa-utils/src/test/scala/lisa/TestTheoryLibrary.scala
diff --git a/lisa-utils/src/test/scala/lisa/kernel/SubstitutionTest.scala b/lisa-utils/src/test/scala/lisa/kernel/SubstitutionTest.scala
index 3a31f7e1fdc46d037136cdc1c7fb781fe0281aa7..8a2fa3e79209ca986aa50b47588e84a0c172875b 100644
--- a/lisa-utils/src/test/scala/lisa/kernel/SubstitutionTest.scala
+++ b/lisa-utils/src/test/scala/lisa/kernel/SubstitutionTest.scala
@@ -11,6 +11,9 @@ import lisa.utils.KernelHelpers.{_, given}
import org.scalatest.compatible.Assertion
import org.scalatest.funsuite.AnyFunSuite
+/**
+ * Extensive tests for the file lisa.kernel.Substitution
+ */
class SubstitutionTest extends AnyFunSuite {
private val x = variable
private val x1 = VariableLabel(Identifier("x", 1))
diff --git a/lisa-utils/src/test/scala/lisa/test/utils/TheoriesHelpersTest.scala b/lisa-utils/src/test/scala/lisa/kernel/TheoriesHelpersTest.scala
similarity index 90%
rename from lisa-utils/src/test/scala/lisa/test/utils/TheoriesHelpersTest.scala
rename to lisa-utils/src/test/scala/lisa/kernel/TheoriesHelpersTest.scala
index 3089836342683e2f1300bd1bb9343b6f7865df95..c74f53614d084679f5d8c565953baae62bc804bd 100644
--- a/lisa-utils/src/test/scala/lisa/test/utils/TheoriesHelpersTest.scala
+++ b/lisa-utils/src/test/scala/lisa/kernel/TheoriesHelpersTest.scala
@@ -1,4 +1,4 @@
-package lisa.test.utils
+package lisa.test.kernel
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.RunningTheoryJudgement.InvalidJustification
@@ -10,6 +10,9 @@ import lisa.utils.KernelHelpers.{_, given}
import lisa.utils.{_, given}
import org.scalatest.funsuite.AnyFunSuite
+/**
+ * Check that a simple incorrect theorem is not accepted and a single correct theorem is accepted.
+ */
class TheoriesHelpersTest extends AnyFunSuite {
export TestTheory.*
@@ -17,6 +20,7 @@ class TheoriesHelpersTest extends AnyFunSuite {
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", c1 === c0, SCProof(Hypothesis((c0 === c1) |- (c0 === c1), c0 === c1)), Seq())
assert(!judgement.isValid)
diff --git a/lisa-utils/src/test/scala/lisa/test/utils/SCProofStepFinderTests.scala b/lisa-utils/src/test/scala/lisa/test/utils/SCProofStepFinderTests.scala
deleted file mode 100644
index 3bc3061ebda23cb105dc46654350644db9cdf73b..0000000000000000000000000000000000000000
--- a/lisa-utils/src/test/scala/lisa/test/utils/SCProofStepFinderTests.scala
+++ /dev/null
@@ -1,190 +0,0 @@
-package lisa.test.utils
-
-import org.scalatest.funsuite.AnyFunSuite
-
-import scala.language.adhocExtensions
-/*
-import utilities.Helpers.*
-import utilities.Printer
-import lisa.kernel.fol.FOL.*
-import lisa.kernel.proof.*
-import lisa.kernel.proof.SequentCalculus.*
-import lisa.settheory.AxiomaticSetTheory.*
-import lisa.kernel.proof.SCProofCheckerJudgement.*
-import org.scalatest.funsuite.AnyFunSuite
-import me.cassayre.florian.masterproject.util.SCProofBuilder.{_{_, given}
-
-import util.chaining.*
-import scala.util.{Failure, Success, Try}
- */
-class SCProofStepFinderTests extends AnyFunSuite {
- /*
- test("proof steps reconstruction") {
- // These tests ensure that all the kernel proof steps can be generated
- // To achieve that, we design proofs that require these steps to be used at some point
-
- val (x, y, z) = (VariableLabel("x"), VariableLabel("y"), VariableLabel("z"))
- val theory = new RunningTheory()
- val (la, lb, lc) = (ConstantPredicateLabel("a", 0), ConstantPredicateLabel("b", 0), ConstantPredicateLabel("c", 0))
- Seq(la, lb, lc).foreach(theory.addSymbol)
- val (a, b, c) = (PredicateFormula(la, Seq.empty), PredicateFormula(lb, Seq.empty), PredicateFormula(lc, Seq.empty))
- val (ls, lt) = (ConstantFunctionLabel("s", 0), ConstantFunctionLabel("t", 0))
- Seq(ls, lt).foreach(theory.addSymbol)
- val (s, t) = (FunctionTerm(ls, Seq.empty), FunctionTerm(lt, Seq.empty))
-
- implicit class VariableLabelEq(l: VariableLabel) { // Helper due to conflicts with scalatest's `===`
- def ====(r: Term): Formula = PredicateFormula(equality, Seq(VariableTerm(l), r))
- def ====(r: VariableLabel): Formula = PredicateFormula(equality, Seq(VariableTerm(l), VariableTerm(r)))
- }
- implicit class FunctionLabelEq(l: FunctionLabel) {
- def ====(r: Term): Formula = PredicateFormula(equality, Seq(FunctionTerm(l, Seq.empty), r))
- def ====(r: FunctionLabel): Formula = PredicateFormula(equality, Seq(FunctionTerm(l, Seq.empty), FunctionTerm(r, Seq.empty)))
- }
- implicit class TermEq(l: Term) {
- def ====(r: Term): Formula = PredicateFormula(equality, Seq(l, r))
- def ====(r: FunctionLabel): Formula = PredicateFormula(equality, Seq(l, FunctionTerm(r, Seq.empty)))
- }
-
- val proofs: Seq[((String, SCProofBuilder), PartialFunction[SCProofStep, Unit])] = Seq(
- // (1.1)
- "Hypothesis" -> SCProofBuilder(
- a |- a,
- ) -> { case _: Hypothesis => () },
- "Cut" -> SCProofBuilder(
- a |- a,
- Seq(a, b) |- a by 0,
- c |- c,
- c |- Seq(b, c) by 2,
- Seq(a, c) |- Seq(a, c) by (1, 3),
- ) -> { case _: Cut => () },
- "LeftAnd" -> SCProofBuilder(
- a |- a,
- (a /\ b) |- a by 0,
- ) -> { case _: LeftAnd => () },
- "RightAnd" -> SCProofBuilder(
- a |- a,
- b |- b,
- Seq(a, b) |- (a /\ b) by (0, 1),
- ) -> { case _: RightAnd => () },
- "LeftOr" -> SCProofBuilder(
- a |- a,
- b |- b,
- Seq(a, b, a \/ b) |- Seq(a, b) by (0, 1)
- ) -> { case _: LeftOr => () },
- "RightOr" -> SCProofBuilder(
- a |- a,
- a |- (a \/ b) by 0,
- ) -> { case _: RightOr => () },
- "LeftImplies" -> SCProofBuilder(
- a |- a,
- b |- b,
- Seq(a, a ==> b) |- b by (0, 1),
- ) -> { case _: LeftImplies => () },
- "RightImplies" -> SCProofBuilder(
- a |- a,
- a |- Seq(a, a ==> a) by 0,
- ) -> { case _: RightImplies => () },
- "LeftIff" -> SCProofBuilder(
- (a ==> b) |- (a ==> b),
- (a <=> b) |- (a ==> b) by 0,
- ) -> { case _: LeftIff => () },
- "RightIff" -> SCProofBuilder(
- (a ==> b) |- (a ==> b),
- (b ==> a) |- (b ==> a),
- Seq(a ==> b, b ==> a) |- (a <=> b) by (0, 1),
- ) -> { case _: RightIff => () },
- "LeftNot" -> SCProofBuilder(
- a |- a,
- a |- Seq(a, b) by 0,
- Seq(a, !b) |- a by 1,
- ) -> { case _: LeftNot => () },
- "RightNot" -> SCProofBuilder(
- a |- a,
- Seq(a, b) |- a by 0,
- a |- Seq(a, !b) by 1,
- ) -> { case _: RightNot => () },
- "LeftForall" -> SCProofBuilder(
- (y ==== z) |- (y ==== z),
- forall(x, x ==== z) |- (y ==== z) by 0,
- ) -> { case _: LeftForall => () },
- "RightForall" -> SCProofBuilder(
- (y ==== z) |- (y ==== z),
- (y ==== z) |- forall(x, y ==== z) by 0,
- ) -> { case _: RightForall => () },
- "LeftExists" -> SCProofBuilder(
- (y ==== z) |- (y ==== z),
- exists(x, y ==== z) |- (y ==== z) by 0,
- ) -> { case _: LeftExists => () },
- "RightExists" -> SCProofBuilder(
- (y ==== z) |- (y ==== z),
- (y ==== z) |- exists(x, x ==== z) by 0,
- ) -> { case _: RightExists => () },
- "LeftExistsOne" -> SCProofBuilder(
- exists(y, forall(x, (x ==== y) <=> a)).pipe(f => f |- f),
- existsOne(x, a) |- exists(y, forall(x, (x ==== y) <=> a)) by 0,
- ) -> { case _: LeftExistsOne => () },
- "RightExistsOne" -> SCProofBuilder(
- exists(y, forall(x, (x ==== y) <=> a)).pipe(f => f |- f),
- exists(y, forall(x, (x ==== y) <=> a)) |- existsOne(x, a) by 0,
- ) -> { case _: RightExistsOne => () },
- "(Left)Weakening" -> SCProofBuilder(
- a |- a,
- Seq(a, b) |- a by 0,
- ) -> { case _: Weakening => () },
- "(Right)Weakening" -> SCProofBuilder(
- a |- a,
- a |- Seq(a, b) by 0,
- ) -> { case _: Weakening => () },
- // (1.2)
- "LeftSubstEq" -> SCProofBuilder(
- (s ==== emptySet) |- (s ==== emptySet),
- Seq(s ==== t, t ==== emptySet) |- (s ==== emptySet) by 0,
- ) -> { case _: LeftSubstEq => () },
- "RightSubstEq" -> SCProofBuilder(
- (s ==== emptySet) |- (s ==== emptySet),
- Seq(s ==== emptySet, s ==== t) |- Seq(s ==== emptySet, t ==== emptySet) by 0,
- ) -> { case _: RightSubstEq => () },
- "LeftSubstIff" -> SCProofBuilder(
- a |- a,
- Seq(b, a <=> b) |- a by 0,
- ) -> { case _: LeftSubstIff => () },
- "RightSubstIff" -> SCProofBuilder(
- a |- a,
- Seq(a, a <=> b) |- b by 0,
- ) -> { case _: RightSubstIff => () },
- "LeftRefl" -> SCProofBuilder(
- a |- a,
- Seq(a, b) |- a by 0,
- Seq(a, b, emptySet ==== emptySet) |- a by 1,
- Seq(a, b) |- a by 2,
- ) -> { case _: LeftRefl => () },
- "RightRefl" -> SCProofBuilder(
- () |- (emptySet ==== emptySet),
- ) -> { case _: RightRefl => () },
- )
-
- proofs.foreach { case ((testname, proofBuilder), partialFunction) =>
- val filter: SCProofStep => Boolean = partialFunction.lift(_).nonEmpty
- Try(proofBuilder.build) match {
- case Success(proof) =>
- SCProofChecker.checkSCProof(proof) match {
- case SCValidProof(_) => // OK
- println(testname)
- println(FOLPrinter.prettySCProof(proof))
- println()
- // Dirty, but only way to test that
- val proofWithoutLast = proof.copy(steps = proof.steps.init)
- proofBuilder.steps.last match {
- case SCImplicitProofStep(conclusion, premises, imports) =>
- val view = SCProofStepFinder.findPossibleProofSteps(proofWithoutLast, conclusion, premises)
- assert(view.exists(filter), s"The proof step finder was not able to find the step '$testname'")
- case SCExplicitProofStep(step) => assert(false)
- }
- case invalid: SCInvalidProof => throw new AssertionError(s"The reconstructed proof for '$testname' is incorrect:\n${FOLPrinter.prettySCProof(invalid)}")
- }
- case Failure(exception) => throw new AssertionError(s"Couldn't reconstruct the proof for '$testname'", exception) // Couldn't reconstruct this proof
- }
- }
- }
- */
-}
diff --git a/lisa-utils/src/test/scala/lisa/test/utils/BasicTacticTest.scala b/lisa-utils/src/test/scala/lisa/utils/BasicTacticTest.scala
similarity index 99%
rename from lisa-utils/src/test/scala/lisa/test/utils/BasicTacticTest.scala
rename to lisa-utils/src/test/scala/lisa/utils/BasicTacticTest.scala
index 48f952b9140b081323cca686b8303274b98ce5bc..e7c6520dc5fc0559c1daddd35f025c6e87b3c566 100644
--- a/lisa-utils/src/test/scala/lisa/test/utils/BasicTacticTest.scala
+++ b/lisa-utils/src/test/scala/lisa/utils/BasicTacticTest.scala
@@ -1,11 +1,11 @@
-package lisa.test.utils
+package lisa.utils
//import lisa.kernel.proof.SequentCalculus as SC
//import lisa.prooflib.BasicStepTactic.*
//import lisa.prooflib.Library
//import lisa.prooflib.ProofTacticLib
//import lisa.utils.Printer
-import lisa.test.utils.ProofTacticTestLib
+import lisa.test.ProofTacticTestLib
//import org.scalatest.funsuite.AnyFunSuite
class BasicTacticTest extends ProofTacticTestLib {
diff --git a/lisa-utils/src/test/scala/lisa/test/utils/ParserTest.scala b/lisa-utils/src/test/scala/lisa/utils/ParserTest.scala
similarity index 99%
rename from lisa-utils/src/test/scala/lisa/test/utils/ParserTest.scala
rename to lisa-utils/src/test/scala/lisa/utils/ParserTest.scala
index 441010c6615bb856040532e4239a7b382443ca62..01457e990d796e1363fbd7016bd0a45dc7923796 100644
--- a/lisa-utils/src/test/scala/lisa/test/utils/ParserTest.scala
+++ b/lisa-utils/src/test/scala/lisa/utils/ParserTest.scala
@@ -1,4 +1,4 @@
-package lisa.test.utils
+package lisa.utils
import lisa.kernel.fol.FOL._
import lisa.kernel.proof.SequentCalculus.Sequent
diff --git a/lisa-utils/src/test/scala/lisa/test/utils/PrinterTest.scala b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
similarity index 99%
rename from lisa-utils/src/test/scala/lisa/test/utils/PrinterTest.scala
rename to lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
index 521d14435abfca1819b50d052ec94c544e321891..5a776019118ac05d6b4b3f12be8c8e79dc31f5f2 100644
--- a/lisa-utils/src/test/scala/lisa/test/utils/PrinterTest.scala
+++ b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
@@ -1,4 +1,4 @@
-package lisa.test.utils
+package lisa.utils
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.SequentCalculus.Sequent
diff --git a/lisa-utils/src/test/scala/lisa/test/utils/TestUtils.scala b/lisa-utils/src/test/scala/lisa/utils/TestUtils.scala
similarity index 98%
rename from lisa-utils/src/test/scala/lisa/test/utils/TestUtils.scala
rename to lisa-utils/src/test/scala/lisa/utils/TestUtils.scala
index 076c80996b85820a085f2b35b9ab53011aba9290..daaa06674beacf01e20b13375d3e042cb566a6e8 100644
--- a/lisa-utils/src/test/scala/lisa/test/utils/TestUtils.scala
+++ b/lisa-utils/src/test/scala/lisa/utils/TestUtils.scala
@@ -1,4 +1,4 @@
-package lisa.test.utils
+package lisa.utils
import lisa.kernel.fol.FOL._
import lisa.utils.KernelHelpers._
diff --git a/lisa-utils/src/test/scala/lisa/test/utils/UnificationTest.scala b/lisa-utils/src/test/scala/lisa/utils/UnificationTest.scala
similarity index 98%
rename from lisa-utils/src/test/scala/lisa/test/utils/UnificationTest.scala
rename to lisa-utils/src/test/scala/lisa/utils/UnificationTest.scala
index 405ea777ecaa4dfc0422ddafa1f43c7bedff6af8..1910e5de8467a0fa9da7117eaea871e1d899e919 100644
--- a/lisa-utils/src/test/scala/lisa/test/utils/UnificationTest.scala
+++ b/lisa-utils/src/test/scala/lisa/utils/UnificationTest.scala
@@ -1,6 +1,6 @@
-package lisa.test.utils
+package lisa.utils
-import lisa.test.utils.ProofTacticTestLib
+import lisa.test.ProofTacticTestLib
import lisa.utils.KernelHelpers.{_, given}
import lisa.utils.*
import org.scalatest.funsuite.AnyFunSuite
diff --git a/src/main/scala/lisa/Main.scala b/src/main/scala/lisa/Main.scala
deleted file mode 100644
index 7385747af4dfbd8b986872e9cd6c8564bd911fd6..0000000000000000000000000000000000000000
--- a/src/main/scala/lisa/Main.scala
+++ /dev/null
@@ -1,68 +0,0 @@
-package lisa
-
-import lisa.prooflib.BasicMain
-import lisa.settheory.SetTheoryLibrary
-
-/**
- * The parent trait of all theory files containing mathematical development
- */
-trait Main extends BasicMain {
- export SetTheoryLibrary.{powerAxiom as _, subsetAxiom as _, emptySetAxiom as _, given, _}
- export lisa.prooflib.Exports.*
- export lisa.automation.kernel.OLPropositionalSolver.Tautology
- export lisa.prooflib.Substitution.*
-
- /**
- * Power Set Axiom --- For a set `x`, there exists a power set of `x`, denoted
- * `PP(x)` or `power(x)` which contains every subset of x.
- *
- * `|- z ∈ power(x) ⇔ z ⊆ x`
- *
- * This axiom defines [[powerSet]] as the function symbol representing this
- * set.
- */
- final val powerAxiom: SetTheoryLibrary.powerAxiom.type = SetTheoryLibrary.powerAxiom
-
- /**
- * Subset Axiom --- For sets `x` and `y`, `x` is a subset of `y` iff every
- * element of `x` is in `y`. Denoted `x ⊆ y`.
- *
- * `|- x ⊆ y ⇔ (z ∈ x ⇒ z ∈ y)`
- *
- * This axiom defines the [[subset]] symbol as this predicate.
- */
- final val subsetAxiom: SetTheoryLibrary.subsetAxiom.type = SetTheoryLibrary.subsetAxiom
-
- /**
- * Empty Set Axiom --- From the Comprehension Schema follows the existence of
- * a set containing no elements, the empty set.
- *
- * `∅ = {x ∈ X | x != x}`.
- *
- * This axiom defines [[emptySet]] as the constant symbol representing this set.
- *
- * `() |- !(x ∈ ∅)`
- */
- final val emptySetAxiom: SetTheoryLibrary.emptySetAxiom.type = SetTheoryLibrary.emptySetAxiom
-
- knownDefs.update(emptySet, Some(emptySetAxiom))
- knownDefs.update(unorderedPair, Some(pairAxiom))
- knownDefs.update(union, Some(unionAxiom))
- knownDefs.update(powerSet, Some(powerAxiom))
- knownDefs.update(subset, Some(subsetAxiom))
-
- // TODO: Refine errors and messages
- extension (symbol: ConstantLabel[?]) {
- def definition: JUSTIFICATION = {
- getDefinition(symbol).get
- /*
- symbol match {
- //case `equality` => throw new NoSuchElementException("Equality has no definition")
- /*case `top` => throw new NoSuchElementException("Top has no definition")
- case `bot` => throw new NoSuchElementException("Bot has no definition")
- case `in` => throw new NoSuchElementException("Membership has no definition")*/
- case _ => ???.asInstanceOf[JUSTIFICATION] //getDefinition(symbol).get*/
- }
- }
-
-}
diff --git a/src/main/scala/lisa/automation/kernel/SimplePropositionalSolver.scala b/src/main/scala/lisa/automation/kernel/SimplePropositionalSolver.scala
deleted file mode 100644
index 0ab0cec84dfd59ea890b941ff1a7c0738cdead22..0000000000000000000000000000000000000000
--- a/src/main/scala/lisa/automation/kernel/SimplePropositionalSolver.scala
+++ /dev/null
@@ -1,250 +0,0 @@
-package lisa.automation.kernel
-
-import lisa.kernel.fol.FOL.*
-import lisa.kernel.proof.SCProof
-import lisa.kernel.proof.SequentCalculus.*
-import lisa.prooflib.Library
-import lisa.prooflib.ProofTacticLib.*
-import lisa.utils.FOLPrinter
-import lisa.utils.KernelHelpers.{_, given}
-
-import scala.collection.mutable.Set as mSet
-
-/**
- * A simple but complete solver for propositional logic. Will not terminate for large problems
- */
-object SimplePropositionalSolver {
-
- /*
- class OrganisedFormulaSet {
- val negs: mSet[ConnectorFormula] = mSet()
- val impliess: mSet[ConnectorFormula] = mSet()
- val iffs: mSet[ConnectorFormula] = mSet()
- val ands: mSet[ConnectorFormula] = mSet()
- val ors: mSet[ConnectorFormula] = mSet()
- val others: mSet[Formula] = mSet()
-
- def updateFormula(phi: Formula, add: Boolean): Unit = (phi match {
- case phi @ ConnectorFormula(label, args) =>
- label match {
- case Neg => if (add) negs.add(phi) else negs.remove(phi)
- case Implies => if (add) impliess.add(phi) else impliess.remove(phi)
- case Iff => if (add) iffs.add(phi) else iffs.remove(phi)
- case And => if (add) ands.add(phi) else ands.remove(phi)
- case Or => if (add) ors.add(phi) else ors.remove(phi)
- case _ => if (add) others.add(phi) else others.remove(phi)
- }
- case _ => if (add) others.add(phi) else others.remove(phi)
- })
-
- def copy(): OrganisedFormulaSet = {
- val r = new OrganisedFormulaSet
- r.negs.addAll(negs)
- r.impliess.addAll(impliess)
- r.iffs.addAll(iffs)
- r.ands.addAll(ands)
- r.ors.addAll(ors)
- r.others.addAll(others)
- r
- }
- }
-
- def solveOrganisedSequent(left: OrganisedFormulaSet, right: OrganisedFormulaSet, s: Sequent, offset: Int): List[SCProofStep] = {
- if (left.negs.nonEmpty) {
- val f = left.negs.head
- val phi = f.args.head
- left.updateFormula(f, false)
- right.updateFormula(f.args.head, true)
- val proof = solveOrganisedSequent(left, right, s -<< f +>> phi, offset)
- LeftNot(s, proof.length - 1 + offset, phi) :: proof
- } else if (left.impliess.nonEmpty) {
- val f = left.impliess.head
- val phi = f.args(0)
- val psi = f.args(1)
-
- left.updateFormula(f, false) // gamma
- val rl = left.copy() // sigma
- val rr = right.copy() // pi
- right.updateFormula(phi, true) // delta
- rl.updateFormula(psi, true)
- val proof1 = solveOrganisedSequent(left, right, s -<< f +>> phi, offset)
- val proof2 = solveOrganisedSequent(rl, rr, s -<< f +<< psi, offset + proof1.size)
- LeftImplies(s, proof1.size + offset - 1, proof1.size + proof2.size + offset - 1, phi, psi) :: (proof2 ++ proof1)
- } else if (left.iffs.nonEmpty) {
- val f = left.iffs.head
- val phi = f.args(0)
- val psi = f.args(1)
- left.updateFormula(f, false)
- left.updateFormula(phi ==> psi, true)
- left.updateFormula(psi ==> phi, true)
- val proof = solveOrganisedSequent(left, right, s -<< f +<< (phi ==> psi) +<< (psi ==> phi), offset)
- LeftIff(s, proof.length - 1 + offset, phi, psi) :: proof
- } else if (left.ands.nonEmpty) {
- val f = left.ands.head
- val phi = f.args(0)
- val psi = f.args(1)
- left.updateFormula(f, false)
- left.updateFormula(phi, true)
- left.updateFormula(psi, true)
- val proof = solveOrganisedSequent(left, right, s -<< f +<< phi +<< psi, offset)
- LeftAnd(s, proof.length - 1 + offset, phi, psi) :: proof
-
- } else if (left.ors.nonEmpty) {
- val f = left.ors.head
- if (f.args.isEmpty) {
- List(RestateTrue(s))
- } else if (f.args.length == 1) {
- val phi = f.args(0)
-
- left.updateFormula(f, false) // gamma
- left.updateFormula(phi, true) // delta
- val proof1 = solveOrganisedSequent(left, right, s -<< f +<< phi, offset)
- LeftOr(s, Seq(proof1.size + offset - 1, proof1.size + offset - 1), Seq(phi)) :: (proof1)
- } else if (f.args.length == 2) {
- val phi = f.args(0)
- val psi = f.args(1)
-
- left.updateFormula(f, false) // gamma
- val rl = left.copy() // sigma
- val rr = right.copy() // pi
- left.updateFormula(phi, true) // delta
- rl.updateFormula(psi, true)
- val proof1 = solveOrganisedSequent(left, right, s -<< f +<< phi, offset)
- val proof2 = solveOrganisedSequent(rl, rr, s -<< f +<< psi, offset + proof1.size)
- LeftOr(s, Seq(proof1.size + offset - 1, proof1.size + proof2.size + offset - 1), Seq(phi, psi)) :: (proof2 ++ proof1)
- } else {
- val phis = f.args
-
- left.updateFormula(f, false) // gamma
- val pr = phis.foldLeft[(List[Int], List[SCProofStep])]((Nil, Nil))((prev, phi) => {
- val (pInts, pProof) = prev
- val (rl, rr) = (left.copy(), right.copy())
- rl.updateFormula(phi, true)
- val proof = solveOrganisedSequent(rl, rr, s -<< f +<< phi, offset + prev._2.size)
- val res = proof ++ pProof
- (pInts appended res.size + offset - 1, proof ++ pProof)
- })
- LeftOr(s, pr._1, phis) :: pr._2
- }
-
- } else if (right.negs.nonEmpty) {
- val f = right.negs.head
- val phi = f.args.head
- right.updateFormula(f, false)
- left.updateFormula(phi, true)
- val proof = solveOrganisedSequent(left, right, s ->> f +<< phi, offset)
- RightNot(s, proof.length - 1 + offset, phi) :: proof
- } else if (right.impliess.nonEmpty) {
- val f = right.impliess.head
- val phi = f.args(0)
- val psi = f.args(1)
- left.updateFormula(phi, true)
- right.updateFormula(f, false)
- right.updateFormula(psi, true)
- val proof = solveOrganisedSequent(left, right, s ->> f +<< phi +>> psi, offset)
- RightImplies(s, proof.length - 1 + offset, phi, psi) :: proof
- } else if (right.iffs.nonEmpty) {
- val f = right.iffs.head
- val phi = f.args(0)
- val psi = f.args(1)
- right.updateFormula(f, false) // gamma
- val rl = left.copy() // sigma
- val rr = right.copy() // pi
- right.updateFormula(phi ==> psi, true) // delta
- rr.updateFormula(psi ==> phi, true)
- val proof1 = solveOrganisedSequent(left, right, s ->> f +>> (phi ==> psi), offset)
- val proof2 = solveOrganisedSequent(rl, rr, s ->> f +>> (psi ==> phi), offset + proof1.size)
- RightIff(s, proof1.size + offset - 1, proof1.size + proof2.size + offset - 1, phi, psi) :: (proof2 ++ proof1)
- } else if (right.ands.nonEmpty) {
- val f = right.ands.head
- if (f.args.isEmpty) {
- List(RestateTrue(s))
- } else if (f.args.length == 1) {
- val phi = f.args(0)
-
- right.updateFormula(f, false) // gamma
- right.updateFormula(phi, true) // delta
- val proof1 = solveOrganisedSequent(left, right, s ->> f +>> phi, offset)
- RightAnd(s, Seq(proof1.size + offset - 1, proof1.size + offset - 1), Seq(phi)) :: (proof1)
- } else if (f.args.length == 2) {
- val phi = f.args(0)
- val psi = f.args(1)
-
- right.updateFormula(f, false) // gamma
-
- val rl = left.copy() // sigma
- val rr = right.copy() // pi
- right.updateFormula(phi, true) // delta
- rr.updateFormula(psi, true)
- val proof1 = solveOrganisedSequent(left, right, s ->> f +>> phi, offset)
- val proof2 = solveOrganisedSequent(rl, rr, s ->> f +>> psi, offset + proof1.size)
- RightAnd(s, Seq(proof1.size + offset - 1, proof1.size + proof2.size + offset - 1), Seq(phi, psi)) :: (proof2 ++ proof1)
- } else {
- val phis = f.args
-
- right.updateFormula(f, false) // gamma
- val pr = phis.foldLeft[(List[Int], List[SCProofStep])]((Nil, Nil))((prev, phi) => {
- val (pInts, pProof) = prev
- val (rl, rr) = (left.copy(), right.copy())
- rr.updateFormula(phi, true)
- val proof = solveOrganisedSequent(rl, rr, s ->> f +>> phi, offset + prev._2.size)
- val res = proof ++ pProof
- (pInts appended res.size + offset - 1, proof ++ pProof)
- })
- RightAnd(s, pr._1, phis) :: pr._2
- }
-
- } else if (right.ors.nonEmpty) {
- val f = right.ors.head
- val phi = f.args(0)
- val psi = f.args(1)
- right.updateFormula(f, false)
- right.updateFormula(phi, true)
- right.updateFormula(psi, true)
- val proof = solveOrganisedSequent(left, right, s ->> f +>> phi +>> psi, offset)
- RightOr(s, proof.length - 1 + offset, phi, psi) :: proof
-
- } else {
- val f = s.left.find(f => s.right.contains(f))
- List(Hypothesis(s, if (f.nonEmpty) f.get else PredicateFormula(VariableFormulaLabel("P"), Seq())))
- }
- }
-
- def solveSequent(s: Sequent): SCProof = {
- val l = new OrganisedFormulaSet
- s.left.foreach(f => l.updateFormula(f, true))
- val r = new OrganisedFormulaSet
- s.right.foreach(f => r.updateFormula(f, true))
- val r2 = solveOrganisedSequent(l, r, s, 0)
- val r3 = r2.reverse.toVector
- val r4 = SCProof(r3)
- r4
- }
-
- object Trivial extends ProofTactic with ProofSequentTactic with ProofFactSequentTactic {
-
- def apply(using lib: Library, proof: lib.Proof)(bot: Sequent): proof.ProofTacticJudgement = {
- proof.ValidProofTactic(solveSequent(bot).steps, Seq())
- }
-
- def apply(using lib: Library, proof: lib.Proof)(premise: proof.Fact)(bot: Sequent): proof.ProofTacticJudgement =
- apply2(using lib, proof)(Seq(premise)*)(bot)
-
- def apply2(using lib: Library, proof: lib.Proof)(premises: proof.Fact*)(bot: Sequent): proof.ProofTacticJudgement = {
- val steps = {
- val premsFormulas = premises.map(p => (p, sequentToFormula(proof.getSequent(p)))).zipWithIndex
- val initProof = premsFormulas.map(s => Restate(() |- s._1._2, -(1 + s._2))).toList
- val sqToProve = bot ++<< (premsFormulas.map(s => s._1._2).toSet |- ())
- val subpr = SCSubproof(solveSequent(sqToProve))
- val stepsList = premsFormulas.foldLeft[List[SCProofStep]](List(subpr))((prev: List[SCProofStep], cur) => {
- val ((prem, form), position) = cur
- Cut(prev.head.bot -<< form, position, initProof.length + prev.length - 1, form) :: prev
- })
- (initProof ++ stepsList.reverse).toIndexedSeq
- }
-
- proof.ValidProofTactic(steps, premises)
- }
- }
- */
-}
diff --git a/src/main/scala/lisa/automation/kernel/SimpleSimplifier.scala b/src/main/scala/lisa/automation/kernel/SimpleSimplifier.scala
deleted file mode 100644
index ce46e7f1d89de806dca5070b886645e14d96d8c9..0000000000000000000000000000000000000000
--- a/src/main/scala/lisa/automation/kernel/SimpleSimplifier.scala
+++ /dev/null
@@ -1,687 +0,0 @@
-package lisa.automation.kernel
-
-import lisa.fol.FOL.*
-import lisa.prooflib.BasicStepTactic
-import lisa.prooflib.ProofTacticLib.*
-import lisa.prooflib.SimpleDeducedSteps
-import lisa.utils.FOLPrinter
-import lisa.utils.K
-import lisa.utils.unification.UnificationUtils
-
-import scala.annotation.nowarn
-import scala.annotation.tailrec
-import scala.collection
-import scala.collection.immutable.Seq
-
-object SimpleSimplifier {
- /*
- private def condflat[T](s: Seq[(T, Boolean)]): (Seq[T], Boolean) = (s.map(_._1), s.exists(_._2))
-
- private def findSubterm2(t: Term, subs: Seq[(Variable, Term)]): (Term, Boolean) = {
- val eq = subs.find(s => (t == s._2))
- if (eq.nonEmpty) (eq.get._1, true)
- else {
- t match {
- case Variable(id) => (t, false)
- case Constant(id) => (t, false)
- case AppliedTerm(f, args) =>
- val induct = condflat(args.map(te => findSubterm2(te, subs)))
- if (!induct._2) (t, false)
- else (AppliedTerm(f, induct._1), true)
- }
-
- }
-
- }
-
- private def findSubterm2(f: Formula, subs: Seq[(Variable, Term)]): (Formula, Boolean) = {
- f match {
- case PredicateFormula(label, args) =>
- val induct = condflat(args.map(findSubterm2(_, subs)))
- if (!induct._2) (f, false)
- else (PredicateFormula(label, induct._1), true)
- case ConnectorFormula(label, args) =>
- val induct = condflat(args.map(findSubterm2(_, subs)))
- if (!induct._2) (f, false)
- else (ConnectorFormula(label, induct._1), true)
- case BinderFormula(label, bound, inner) =>
- val fv_in_f = subs.flatMap(e => e._2.freeSchematicLabels + e._1)
- if (!fv_in_f.contains(bound)) {
- val induct = findSubterm2(inner, subs)
- if (!induct._2) (f, false)
- else (BinderFormula(label, bound, induct._1), true)
- } else {
- val newv = Variable(freshId((f.freeSchematicLabels ++ fv_in_f).map(_.id), bound.id))
- val newInner = inner.substitute(bound := newv)
- val induct = findSubterm2(newInner, subs)
- if (!induct._2) (f, false)
- else (BinderFormula(label, newv, induct._1), true)
- }
- }
- }
-
- private def findSubformula2(f: Formula, subs: Seq[(VariableFormula, Formula)]): (Formula, Boolean) = {
- val eq = subs.find(s => isSame(f, s._2))
- if (eq.nonEmpty) (eq.get._1, true)
- else
- f match {
- case PredicateFormula(label, args) =>
- (f, false)
- case ConnectorFormula(label, args) =>
- val induct = condflat(args.map(findSubformula2(_, subs)))
- if (!induct._2) (f, false)
- else (ConnectorFormula(label, induct._1), true)
- case BinderFormula(label, bound, inner) =>
- val fv_in_f = subs.flatMap(_._2.freeSchematicLabels)
- if (!fv_in_f.contains(bound)) {
- val induct = findSubformula2(inner, subs)
- if (!induct._2) (f, false)
- else (BinderFormula(label, bound, induct._1), true)
- } else {
- val newv = Variable(freshId((f.freeSchematicLabels ++ fv_in_f).map(_.id), bound.id))
- val newInner = inner.substitute(bound := newv)
- val induct = findSubformula2(newInner, subs)
- if (!induct._2) (f, false)
- else (BinderFormula(label, newv, induct._1), true)
- }
- }
- }
- def findSubterm(t: Term, subs: Seq[(Variable, Term)]): Option[LambdaExpression[Term, Term, ?]] = {
- val vars = subs.map(_._1)
- val r = findSubterm2(t, subs)
- if (r._2) Some(lambda(vars, r._1))
- else None
- }
-
- def findSubterm(f: Formula, subs: Seq[(Variable, Term)]): Option[LambdaExpression[Term, Formula, ?]] = {
- val vars = subs.map(_._1)
- val r = findSubterm2(f, subs)
- if (r._2) Some(lambda(vars, r._1))
- else None
- }
-
- def findSubformula(f: Formula, subs: Seq[(VariableFormula, Formula)]): Option[LambdaExpression[Formula, Formula, ?]] = {
- val vars = subs.map(_._1)
- val r = findSubformula2(f, subs)
- if (r._2) Some(lambda(vars, r._1))
- else None
- }
-
- /*
- object applySubst extends ProofTactic {
- def applyLeftRight(using lib: lisa.prooflib.Library, proof: lib.Proof)
- (phi: Formula)
- (premise: proof.Fact)
- (rightLeft: Boolean = false, toLeft: Boolean = true, toRight: Boolean = true): proof.ProofTacticJudgement = {
- val originSequent = proof.getSequent(premise)
- val leftOrigin = ConnectorFormula(And, originSequent.left.toSeq)
- val rightOrigin = ConnectorFormula(Or, originSequent.right.toSeq)
-
- if (!toLeft && !toRight) return proof.InvalidProofTactic("applyLeftRight called with no substitution selected (toLeft or toRight).")
-
- phi match {
- case PredicateFormula(label, args) if label == equality =>
- val left = args(0)
- val right = args(1)
- val fv_in_phi = (originSequent.left ++ originSequent.right).flatMap(_.freeSchematicLabels).map(_.id)
- val v = Variable(nFreshId(fv_in_phi, 1).head)
- lazy val isolatedLeft = originSequent.left.filterNot(f => isSame(f, phi)).map(f => (f, findSubterm(f, IndexedSeq(v -> left))))
- lazy val isolatedRight = originSequent.right.map(f => (f, findSubterm(f, IndexedSeq(v -> left))))
- if ((!toLeft || isolatedLeft.forall(_._2.isEmpty)) && (!toRight || isolatedRight.forall(_._2.isEmpty)))
- if (rightLeft)
- return proof.InvalidProofTactic(s"There is no instance of ${FOLPrinter.prettyTerm(right)} to replace.")
- else
- applyLeftRight(equality(right, left))(premise)(true, toLeft, toRight) match {
- case proof.InvalidProofTactic(m) => return proof.InvalidProofTactic(s"There is no instance of ${FOLPrinter.prettyTerm(left)} to replace.")
- case v: proof.ValidProofTactic => return v
- }
-
- val leftForm = ConnectorFormula(And, isolatedLeft.map((f, ltf) => if (ltf.isEmpty) f else ltf.get.body).toSeq)
- val rightForm = ConnectorFormula(Or, isolatedRight.map((f, ltf) => if (ltf.isEmpty) f else ltf.get.body).toSeq)
- val newleft = if (toLeft) isolatedLeft.map((f, ltf) => if (ltf.isEmpty) f else ltf.get(Seq(right))) else originSequent.left
- val newright = if (toRight) isolatedRight.map((f, ltf) => if (ltf.isEmpty) f else ltf.get(Seq(right))) else originSequent.right
- val result1: Sequent = (ConnectorFormula(And, newleft.toSeq), phi) |- rightOrigin
- val result2: Sequent = result1.left |- ConnectorFormula(Or, newright.toSeq)
-
- var scproof: Seq[SCProofStep] = Seq(Restate(leftOrigin |- rightOrigin, -1))
- if (toLeft) scproof = scproof :+ LeftSubstEq(result1, scproof.length - 1, List(left -> right), LambdaTermFormula(Seq(v), leftForm))
- if (toRight) scproof = scproof :+ RightSubstEq(result2, scproof.length - 1, List(left -> right), LambdaTermFormula(Seq(v), rightForm))
- scproof = scproof :+ Restate(newleft + phi |- newright, scproof.length - 1)
-
- proof.ValidProofTactic(
- ???,
- scproof,
- Seq(premise)
- )
- case ConnectorFormula(label, args) if label == Iff =>
- val left = args(0)
- val right = args(1)
- val fv_in_phi = (originSequent.left ++ originSequent.right).flatMap(_.schematicFormulaLabels).map(_.id)
- val H = VariableFormula(nFreshId(fv_in_phi, 1).head)
- lazy val isolatedLeft = originSequent.left.filterNot(f => isSame(f, phi)).map(f => (f, findSubformula(f, IndexedSeq(H -> left))))
- lazy val isolatedRight = originSequent.right.map(f => (f, findSubformula(f, IndexedSeq(H -> left))))
- if ((!toLeft || isolatedLeft.forall(_._2.isEmpty)) && (!toRight || isolatedRight.forall(_._2.isEmpty)))
- if (rightLeft)
- return proof.InvalidProofTactic(s"There is no instance of ${FOLPrinter.prettyFormula(right)} to replace.")
- else
- applyLeftRight(Iff(right, left))(premise)(true, toLeft, toRight) match {
- case proof.InvalidProofTactic(m) => return proof.InvalidProofTactic(s"There is no instance of ${FOLPrinter.prettyFormula(left)} to replace.")
- case v: proof.ValidProofTactic => return v
- }
-
- val leftForm = ConnectorFormula(And, isolatedLeft.map((f, ltf) => if (ltf.isEmpty) f else ltf.get.body).toSeq)
- val rightForm = ConnectorFormula(Or, isolatedRight.map((f, ltf) => if (ltf.isEmpty) f else ltf.get.body).toSeq)
- val newleft = if (toLeft) isolatedLeft.map((f, ltf) => if (ltf.isEmpty) f else ltf.get(Seq(right))) else originSequent.left
- val newright = if (toRight) isolatedRight.map((f, ltf) => if (ltf.isEmpty) f else ltf.get(Seq(right))) else originSequent.right
- val result1: Sequent = (ConnectorFormula(And, newleft.toSeq), phi) |- rightOrigin
- val result2: Sequent = result1.left |- ConnectorFormula(Or, newright.toSeq)
-
- var scproof: Seq[SCProofStep] = Seq(Restate(leftOrigin |- rightOrigin, -1))
- if (toLeft) scproof = scproof :+ LeftSubstIff(result1, scproof.length - 1, List(left -> right), LambdaFormulaFormula(Seq(H), leftForm))
- if (toRight) scproof = scproof :+ RightSubstIff(result2, scproof.length - 1, List(left -> right), LambdaFormulaFormula(Seq(H), rightForm))
- scproof = scproof :+ Restate(newleft + phi |- newright, scproof.length - 1)
-
- proof.ValidProofTactic(
- ???,
- scproof,
- Seq(premise)
- )
- case _ => proof.InvalidProofTactic(s"Formula in applySingleSimp need to be of the form a=b or q<=>p and not ${phi.label}")
- }
-
- }
-
- @nowarn("msg=.*the type test for proof.Fact cannot be checked at runtime*")
- def apply(using
- lib: lisa.prooflib.Library,
- proof: lib.Proof,
- line: sourcecode.Line,
- file: sourcecode.File
- )(f: proof.Fact | Formula, rightLeft: Boolean = false, toLeft: Boolean = true, toRight: Boolean = true)(
- premise: proof.Fact
- ): proof.ProofTacticJudgement = {
- f match {
- case phi: Formula => applyLeftRight(phi)(premise)(rightLeft, toLeft, toRight)
- case f: proof.Fact =>
- val seq = proof.getSequent(f)
- val phi = seq.right.head
- val sp = new BasicStepTactic.SUBPROOF(using proof)(None)({
- val x = applyLeftRight(phi)(premise)(rightLeft, toLeft, toRight)
- proof.library.have(x)
- proof.library.andThen(SimpleDeducedSteps.Discharge(f))
- })
-
- BasicStepTactic.unwrapTactic(sp.judgement.asInstanceOf[proof.ProofTacticJudgement])("Subproof substitution fail.")
- }
-
- }
-
- def toLeft(using lib: lisa.prooflib.Library, proof: lib.Proof, line: sourcecode.Line, file: sourcecode.File)(f: proof.Fact | Formula, rightLeft: Boolean = false)(
- premise: proof.Fact
- ): proof.ProofTacticJudgement = apply(f, rightLeft, toLeft = true, toRight = false)(premise)
-
- def toRight(using lib: lisa.prooflib.Library, proof: lib.Proof, line: sourcecode.Line, file: sourcecode.File)(f: proof.Fact | Formula, rightLeft: Boolean = false)(
- premise: proof.Fact
- ): proof.ProofTacticJudgement = apply(f, rightLeft, toLeft = false, toRight = true)(premise)
-
- }
-
- def simplifySeq(seq: Sequent, ruleseq: IndexedSeq[PredicateFormula], rulesiff: IndexedSeq[ConnectorFormula]): SCProof = {
- /*
- val takenVarsIff = (seq.left.flatMap(_.schematicPredicateLabels) ++ seq.right.flatMap(_.schematicPredicateLabels) ++ ruleseq.flatMap(_.schematicPredicateLabels) ++ rulesiff.flatMap(_.schematicPredicateLabels)).map(_.id)
- val varsIff = nFreshId(takenVarsIff, rulesiff.length).map(VariableFormula)
- val subsIff = varsIff.zip(rulesiff.map(_.args(0)))
-
- val substs: Set[(Formula, LambdaFormulaFormula)] = seq.left.map(f => (f, findSubformula(f, subsIff)) )
- val newseq = substs.map(_._2(rulesiff.map(_.args(1)))) |- seq.right
- val step1 = ??? // LeftSubstIff(newseq, prev.length-1, )
- */
- ???
- }
-
- def simplifySequent(seq: Sequent): SCProof = {
- val (ruleseq, rulesiff, rem): (List[PredicateFormula], List[ConnectorFormula], List[Formula]) =
- seq.left.foldLeft((List[PredicateFormula](), List[ConnectorFormula](), List[Formula]()))((prev, f) => {
- f match {
- case f @ PredicateFormula(label, _) if label == equality => (f :: prev._1, prev._2, prev._3)
- case f @ ConnectorFormula(label, _) if label == iff => (prev._1, f :: prev._2, prev._3)
- case _ => prev
- }
- })
-
- ???
- }
-<<<<<<< HEAD
- */
- object Substitution2 extends ProofTactic with ProofFactSequentTactic {
- def apply(using lib: lisa.prooflib.Library, proof: lib.Proof, line: sourcecode.Line, file: sourcecode.File)(rightLeft: Boolean = false, f: lisa.prooflib.Library#Proof#InstantiatedFact | Formula)(
- premise: proof.Fact
- ): proof.ProofTacticJudgement = {
- f match {
- case phi: Formula => applySubst.applyLeftRight(phi)(premise)(rightLeft)
- case f: proof.Fact @unchecked =>
- val seq = proof.getSequent(f)
- val phi = seq.right.head
- val sp = new BasicStepTactic.SUBPROOF(using proof)(None)({
- val x = applySubst.applyLeftRight(phi)(premise)(rightLeft)
- proof.library.have(x)
- proof.library.andThen(SimpleDeducedSteps.Discharge(f))
- })
- BasicStepTactic.unwrapTactic(sp.judgement.asInstanceOf[proof.ProofTacticJudgement])("Subproof substitution fail.")
- case _ =>
- proof.InvalidProofTactic("the given fact is not valid in the current proof. (This should not compile, but a specific case of overload resolution needs to be fixed.")
- }
-
- }
- def apply(using lib: lisa.prooflib.Library, proof: lib.Proof)(premise: proof.Fact)(bot: Sequent): proof.ProofTacticJudgement = {
- lazy val premiseSequent = proof.getSequent(premise)
- val premRight = ConnectorFormula(Or, premiseSequent.right.toSeq)
- val botRight = ConnectorFormula(Or, bot.right.toSeq)
-
- val equalities = bot.left.collect { case PredicateFormula(`equality`, Seq(l, r)) =>
- (l, r)
- }
- val canReach = UnificationUtils2.canReachOneStepTermFormula(premRight, botRight, equalities.toList)
-
- if (canReach.isEmpty) {
- proof.InvalidProofTactic("Could not find a set of equalities to rewrite premise into conclusion successfully.")
- } else {
- BasicStepTactic.RightSubstEq(equalities.toList, canReach.get)(premise)(bot)
- }
- }
-
- def apply(using lib: lisa.prooflib.Library, proof: lib.Proof)(substitution: proof.Fact | Formula | RunningTheory#Justification)(premise: proof.Fact)(bot: Sequent): proof.ProofTacticJudgement = {
- lazy val premiseSequent = proof.getSequent(premise)
- val premRight = ConnectorFormula(Or, premiseSequent.right.toSeq)
- val botRight = ConnectorFormula(Or, bot.right.toSeq)
-
- val equalities = substitution match {
- case f: Formula =>
- bot.left.collect { case PredicateFormula(`equality`, Seq(l, r)) =>
- (l, r)
- }
- case j: RunningTheory#Justification =>
- proof.sequentOfFact(j.asInstanceOf[lib.theory.Justification]).right.collect { case PredicateFormula(`equality`, Seq(l, r)) =>
- (l, r)
- }
- case f: proof.Fact @unchecked =>
- proof.sequentOfFact(f).right.collect { case PredicateFormula(`equality`, Seq(l, r)) =>
- (l, r)
- }
- }
- val iffs = substitution match {
- case f: Formula =>
- f match {
- case ConnectorFormula(Iff, Seq(l, r)) =>
- List((l, r))
- case _ => List()
- }
- case j: RunningTheory#Justification =>
- proof.sequentOfFact(j.asInstanceOf[lib.theory.Justification]).right.collect { case ConnectorFormula(Iff, Seq(l, r)) =>
- (l, r)
- }
- case f: proof.Fact @unchecked =>
- proof.sequentOfFact(f).right.collect { case ConnectorFormula(Iff, Seq(l, r)) =>
- (l, r)
- }
- }
-
- val canReach = UnificationUtils2.canReachOneStepTermFormula(premRight, botRight, equalities.toList)
-
- if (canReach.isEmpty || equalities.isEmpty) {
- val canReach2 = UnificationUtils2.canReachOneStepOLFormula(premRight, botRight, iffs.toList)
- if (canReach2.isEmpty) {
- proof.InvalidProofTactic("Iffs and Equalities failed")
- } else {
- val sp = new BasicStepTactic.SUBPROOF(using proof)(None)({
- val actIffs = iffs.map((a, b) => Iff(a, b))
- val newBot = bot.copy(right = Set(ConnectorFormula(Or, bot.right.toSeq))) ++<< (actIffs |- ())
- val s1 = proof.library.have(premiseSequent.left |- ConnectorFormula(Or, premiseSequent.right.toSeq)) by SimpleDeducedSteps.Restate.from(premise)
- val x = BasicStepTactic.RightSubstIff(iffs.toList, canReach2.get)(s1)(newBot)
- proof.library.have(x)
- proof.library.thenHave(bot) by SimpleDeducedSteps.Restate.from
- substitution match {
- case f: Formula => ()
- case j: RunningTheory#Justification => proof.library.andThen(SimpleDeducedSteps.Discharge(j.asInstanceOf[lib.theory.Justification]))
- case f: proof.Fact @unchecked => proof.library.andThen(SimpleDeducedSteps.Discharge(f))
- }
- })
- BasicStepTactic.unwrapTactic(sp.judgement.asInstanceOf[proof.ProofTacticJudgement])("Subproof substitution fail.")
- }
- } else {
- val sp = new BasicStepTactic.SUBPROOF(using proof)(None)({
- val x = BasicStepTactic.RightSubstEq(equalities.toList, canReach.get)(premise)(bot)
- proof.library.have(x)
- substitution match {
- case f: Formula => ()
- case j: RunningTheory#Justification => proof.library.andThen(SimpleDeducedSteps.Discharge(j.asInstanceOf[lib.theory.Justification]))
- case f: proof.Fact @unchecked => proof.library.andThen(SimpleDeducedSteps.Discharge(f))
- }
- })
- BasicStepTactic.unwrapTactic(sp.judgement.asInstanceOf[proof.ProofTacticJudgement])("Subproof substitution fail.")
- }
- }
-
- def withExplicitRules(using lib: lisa.prooflib.Library, proof: lib.Proof)(substitutions: (proof.Fact | Formula | RunningTheory#Justification)*)(
- premise: proof.Fact
- )(bot: Sequent): proof.ProofTacticJudgement = {
- // takes a bot
- val premiseSequent: Sequent = proof.getSequent(premise)
-
- val eqspre: List[(Term, Term)] = substitutions.flatMap {
- case f: Formula =>
- f match {
- case PredicateFormula(`equality`, Seq(l, r)) => List((l, r))
- case _ => List()
- }
- case f: proof.Fact @unchecked =>
- proof.sequentOfFact(f).right.collect { case PredicateFormula(`equality`, Seq(l, r)) =>
- (l, r)
- }
- case j: RunningTheory#Justification =>
- proof.sequentOfFact(j.asInstanceOf[lib.theory.Justification]).right.collect { case PredicateFormula(`equality`, Seq(l, r)) =>
- (l, r)
- }
- }.toList
-
- val iffspre: List[(Formula, Formula)] = substitutions.flatMap {
- case f: Formula =>
- f match {
- case ConnectorFormula(Iff, Seq(l, r)) => List((l, r))
- case _ => List()
- }
- case f: proof.Fact @unchecked =>
- proof.sequentOfFact(f).right.collect { case ConnectorFormula(Iff, Seq(l, r)) =>
- (l, r)
- }
- case j: RunningTheory#Justification =>
- proof.sequentOfFact(j.asInstanceOf[lib.theory.Justification]).right.collect { case ConnectorFormula(Iff, Seq(l, r)) =>
- (l, r)
- }
- }.toList
-
- // get the original and swapped versions
- val eqs = eqspre ++ eqspre.map(_.swap)
- val iffs = iffspre ++ iffspre.map(_.swap)
-
- val filteredPrem = (premiseSequent.left filter {
- case PredicateFormula(`equality`, Seq(l, r)) if eqs.contains((l, r)) => false
- case ConnectorFormula(Iff, Seq(l, r)) if iffs.contains((l, r)) => false
- case _ => true
- }).toSeq
-
- val filteredBot = (bot.left filter {
- case PredicateFormula(`equality`, Seq(l, r)) if eqs.contains((l, r)) => false
- case ConnectorFormula(Iff, Seq(l, r)) if iffs.contains((l, r)) => false
- case _ => true
- }).toSeq
-
- lazy val rightPairs = premiseSequent.right zip premiseSequent.right.map(x => bot.right.find(y => UnificationUtils2.canReachOneStep(x, y, iffs, eqs).isDefined))
- lazy val leftPairs = filteredPrem zip filteredPrem.map(x => filteredBot.find(y => UnificationUtils2.canReachOneStep(x, y, iffs, eqs).isDefined))
-
- lazy val violatingFormulaLeft = leftPairs.find(_._2.isEmpty)
- lazy val violatingFormulaRight = rightPairs.find(_._2.isEmpty)
-
- if (violatingFormulaLeft.isDefined)
- proof.InvalidProofTactic(s"Could not rewrite LHS of premise into conclusion with given substitutions.\nViolating Formula: ${FOLPrinter.prettyFormula(violatingFormulaLeft.get._1)}")
- else if (violatingFormulaRight.isDefined)
- proof.InvalidProofTactic(s"Could not rewrite RHS of premise into conclusion with given substitutions.\nViolating Formula: ${FOLPrinter.prettyFormula(violatingFormulaRight.get._1)}")
- else {
- // actually construct proof
- try {
- val leftLambdas = leftPairs.collect { case (l, Some(r)) => UnificationUtils2.canReachOneStep(l, r, iffs, eqs).get }
- val rightLambdas = rightPairs.collect { case (l, Some(r)) => UnificationUtils2.canReachOneStep(l, r, iffs, eqs).get }
-
- val eqsForm = eqs.map { case (l, r) => PredicateFormula(`equality`, Seq(l, r)) }.toSet
- val iffsForm = iffs.map { case (l, r) => ConnectorFormula(Iff, Seq(l, r)) }.toSet
-
- val leftEqs = eqs.map(_._1).toSeq
- val rightEqs = eqs.map(_._2).toSeq
- val leftIffs = iffs.map(_._1).toSeq
- val rightIffs = iffs.map(_._2).toSeq
-
- val sp = new BasicStepTactic.SUBPROOF(using proof)(None)({
- var premiseWithSubst = premiseSequent ++<< (eqsForm |- ()) ++<< (iffsForm |- ())
- proof.library.have(premiseWithSubst) by BasicStepTactic.Weakening(premise)
-
- if (!leftLambdas.isEmpty) {
- val leftEqLambdas = leftLambdas.map(f => lambda(f._2.toSeq, substituteFormulaVariables(f._3, ((f._1: Seq[VariableFormula]) zip iffs.map(_._1)).toMap)))
-
- // substitute and set a new premise for next step
- premiseWithSubst = leftEqLambdas.foldLeft(premiseWithSubst) {
- case (prevSequent, nextLambda) => {
- val newSequent = prevSequent -<? nextLambda(leftEqs) +<< nextLambda(rightEqs)
- proof.library.thenHave(newSequent) by BasicStepTactic.LeftSubstEq(eqs, nextLambda)
-
- newSequent
- }
- }
- }
- if (!rightLambdas.isEmpty) {
- val rightEqLambdas = rightLambdas.map(f => lambda(f._2.toSeq, substituteFormulaVariables(f._3, ((f._1: Seq[VariableFormula]) zip iffs.map(_._1)).toMap)))
-
- // substitute and set a new premise for next step
- premiseWithSubst = rightEqLambdas.foldLeft(premiseWithSubst) {
- case (prevSequent, nextLambda: LambdaTermFormula) => {
- val newSequent = prevSequent ->? nextLambda(leftEqs) +>> nextLambda(rightEqs)
- proof.library.thenHave(newSequent) by BasicStepTactic.RightSubstEq(eqs, nextLambda)
-
- newSequent
- }
- }
- }
-
- if (!leftLambdas.isEmpty) {
- val leftIffLambdas = leftLambdas.map(f => lambda(f._1.toSeq, substituteVariablesInFormula(f._3, ((f._2: Seq[Variable]) zip eqs.map(_._2)).toMap)))
-
- // substitute and set a new premise for next step
- premiseWithSubst = leftIffLambdas.foldLeft(premiseWithSubst) {
- case (prevSequent, nextLambda) => {
- val newSequent = prevSequent -<? nextLambda(leftIffs) +<< nextLambda(rightIffs)
- proof.library.thenHave(newSequent) by BasicStepTactic.LeftSubstIff(iffs, nextLambda)
-
- newSequent
- }
- }
- }
- if (!rightLambdas.isEmpty) {
- val rightIffLambdas = rightLambdas.map(f => lambda(f._1.toSeq, substituteVariablesInFormula(f._3, ((f._2: Seq[Variable]) zip eqs.map(_._2)).toMap)))
-
- // substitute and set a new premise for next step
- premiseWithSubst = rightIffLambdas.foldLeft(premiseWithSubst) {
- case (prevSequent, nextLambda) => {
- val newSequent = prevSequent ->? nextLambda(leftIffs) +>> nextLambda(rightIffs)
- proof.library.thenHave(newSequent) by BasicStepTactic.RightSubstIff(iffs, nextLambda)
-
- newSequent
- }
- }
- }
-
- substitutions.foreach {
- case f: Formula =>
- case f: proof.Fact @unchecked =>
- (proof.library.andThen(SimpleDeducedSteps.Discharge(f)))
- case j: RunningTheory#Justification =>
- proof.library.andThen(SimpleDeducedSteps.Discharge(j.asInstanceOf[lib.theory.Justification]))
- }
-
- proof.library.thenHave(bot) by SimpleDeducedSteps.Restate
-
- })
-
- BasicStepTactic.unwrapTactic(sp.judgement.asInstanceOf[proof.ProofTacticJudgement])("Subproof for Substitution failed.")
- } catch case e: UnapplicableProofTactic => proof.InvalidProofTactic(s"Could not rewrite given conlusion sequent into substituted premise. You may have a typo.\n\t${e.errorMessage}")
-
- }
-
- }
-
- // def apply2(using lib: lisa.prooflib.Library, proof: lib.Proof)(substitutions: (proof.Fact | Formula | RunningTheory#Justification)*)(premise: proof.Fact)(
- // bot: Sequent
- // ): proof.ProofTacticJudgement = apply2(using lib, proof)(false, substitutions: _*)(premise)(bot)
-
- }
-
- object Simplify extends ProofTactic {
-
- def once(using lib: lisa.prooflib.Library, proof: lib.Proof)(rightLeft: Boolean = false, substitutions: (proof.Fact | Formula | RunningTheory#Justification)*)(
- premise: proof.Fact
- ): proof.ProofTacticJudgement = {
- // takes a bot
- val premiseSequent = proof.getSequent(premise)
-
- val eqspre: List[(Term, Term)] = substitutions.flatMap {
- case f: Formula =>
- f match {
- case PredicateFormula(`equality`, Seq(l, r)) => List((l, r))
- case _ => List()
- }
- case f: proof.Fact @unchecked =>
- proof.sequentOfFact(f).right.collect { case PredicateFormula(`equality`, Seq(l, r)) =>
- (l, r)
- }
- case j: RunningTheory#Justification =>
- proof.sequentOfFact(j.asInstanceOf[lib.theory.Justification]).right.collect { case PredicateFormula(`equality`, Seq(l, r)) =>
- (l, r)
- }
- }.toList
-
- val iffspre: List[(Formula, Formula)] = substitutions.flatMap {
- case f: Formula =>
- f match {
- case ConnectorFormula(Iff, Seq(l, r)) => List((l, r))
- case _ => List()
- }
- case f: proof.Fact @unchecked =>
- proof.sequentOfFact(f).right.collect { case ConnectorFormula(Iff, Seq(l, r)) =>
- (l, r)
- }
- case j: RunningTheory#Justification =>
- proof.sequentOfFact(j.asInstanceOf[lib.theory.Justification]).right.collect { case ConnectorFormula(Iff, Seq(l, r)) =>
- (l, r)
- }
- }.toList
-
- val eqs = if (rightLeft) eqspre.map(e => (e._2, e._1)) else eqspre
- val iffs = if (rightLeft) iffspre.map(i => (i._2, i._1)) else iffspre
-
- val filteredPrem = premiseSequent.left filter {
- case PredicateFormula(`equality`, Seq(l, r)) if eqs.contains((l, r)) => false
- case ConnectorFormula(Iff, Seq(l, r)) if iffs.contains((l, r)) => false
- case _ => true
- }
-
- lazy val rightLambdas = premiseSequent.right.map(UnificationUtils2.getContextOneStepFormula(_, iffs, eqs))
- lazy val leftLambdas = filteredPrem.map(UnificationUtils2.getContextOneStepFormula(_, iffs, eqs))
-
- // actually construct proof
- val eqsForm = eqs.map { case (l, r) => PredicateFormula(`equality`, Seq(l, r)) }.toSet
- val iffsForm = iffs.map { case (l, r) => ConnectorFormula(Iff, Seq(l, r)) }.toSet
-
- val leftEqs = eqs.map(_._1).toSeq
- val rightEqs = eqs.map(_._2).toSeq
- val leftIffs = iffs.map(_._1).toSeq
- val rightIffs = iffs.map(_._2).toSeq
-
- val sp = new BasicStepTactic.SUBPROOF(using proof)(None)({
- var premiseWithSubst = premiseSequent ++<< (eqsForm |- ()) ++<< (iffsForm |- ())
- proof.library.have(premiseWithSubst) by BasicStepTactic.Weakening(premise)
-
- if (!leftLambdas.isEmpty) {
- val leftEqLambdas = leftLambdas.map(f => lambda(f._2.toSeq, substituteFormulaVariables(f._3, ((f._1: Seq[VariableFormula]) zip iffs.map(_._1)).toMap)))
-
- // substitute and set a new premise for next step
- premiseWithSubst = leftEqLambdas.foldLeft(premiseWithSubst) {
- case (prevSequent, nextLambda) => {
- val newSequent = prevSequent -<< nextLambda(leftEqs) +<< nextLambda(rightEqs)
- proof.library.thenHave(newSequent) by BasicStepTactic.LeftSubstEq(eqs, nextLambda)
-
- newSequent
- }
- }
- }
- if (!rightLambdas.isEmpty) {
- val rightEqLambdas = rightLambdas.map(f => lambda(f._2.toSeq, substituteFormulaVariables(f._3, ((f._1: Seq[VariableFormula]) zip iffs.map(_._1)).toMap)))
-
- // substitute and set a new premise for next step
- premiseWithSubst = rightEqLambdas.foldLeft(premiseWithSubst) {
- case (prevSequent, nextLambda: LambdaTermFormula) => {
- val newSequent = prevSequent ->> nextLambda(leftEqs) +>> nextLambda(rightEqs)
- proof.library.thenHave(newSequent) by BasicStepTactic.RightSubstEq(eqs, nextLambda)
-
- newSequent
- }
- }
- }
-
- if (!leftLambdas.isEmpty) {
- val leftIffLambdas = leftLambdas.map(f => lambda(f._1.toSeq, substituteVariablesInTerm(f._3, ((f._2: Seq[Variable]) zip eqs.map(_._2)).toMap)))
-
- // substitute and set a new premise for next step
- premiseWithSubst = leftIffLambdas.foldLeft(premiseWithSubst) {
- case (prevSequent, nextLambda) => {
- val newSequent = prevSequent -<< nextLambda(leftIffs) +<< nextLambda(rightIffs)
- proof.library.thenHave(newSequent) by BasicStepTactic.LeftSubstIff(iffs, nextLambda)
-
- newSequent
- }
- }
- }
- if (!rightLambdas.isEmpty) {
- val rightIffLambdas = rightLambdas.map(f => lambda(f._1.toSeq, substituteVariablesInTerm(f._3, ((f._2: Seq[Variable]) zip eqs.map(_._2)).toMap)))
-
- // substitute and set a new premise for next step
- premiseWithSubst = rightIffLambdas.foldLeft(premiseWithSubst) {
- case (prevSequent, nextLambda) => {
- val newSequent = prevSequent ->> nextLambda(leftIffs) +>> nextLambda(rightIffs)
- proof.library.thenHave(newSequent) by BasicStepTactic.RightSubstIff(iffs, nextLambda)
-
- newSequent
- }
- }
- }
-
- substitutions.foreach {
- case f: Formula => ()
- case f: proof.Fact @unchecked => (proof.library.andThen(SimpleDeducedSteps.Discharge(f)))
- case j: RunningTheory#Justification => proof.library.andThen(SimpleDeducedSteps.Discharge(j.asInstanceOf[lib.theory.Justification]))
- }
-
- })
-
- if (isSameSequent(premiseSequent, sp.scproof.conclusion)) proof.InvalidProofTactic("Could not perform a substitution.")
- else BasicStepTactic.unwrapTactic(sp.judgement.asInstanceOf[proof.ProofTacticJudgement])("Subproof for Substitution failed.")
-
- }
-
- // def once(using lib: lisa.prooflib.Library, proof: lib.Proof)(substitutions: (proof.Fact | Formula | RunningTheory#Justification)*)(premise: proof.Fact): proof.ProofTacticJudgement =
- // once(using lib, proof)(false, substitutions: _*)(premise)
-
- // def exhaustive(using lib: lisa.prooflib.Library, proof: lib.Proof)(substitutions: (proof.Fact | Formula | RunningTheory#Justification)*)(premise: proof.Fact): proof.ProofTacticJudgement = star(once(using lib, proof)(substitutions))(premise)
-
- def exhaustive(using lib: lisa.prooflib.Library, proof: lib.Proof, line: sourcecode.Line, file: sourcecode.File)(
- substitutions: (proof.Fact | Formula | RunningTheory#Justification)*
- )(premise: proof.Fact): proof.ProofTacticJudgement = {
- @tailrec
- def f(using lib: lisa.prooflib.Library, proof: lib.Proof)(substitutions: (proof.Fact | Formula | RunningTheory#Justification)*)(premise: proof.Fact): Unit = {
- once(using lib, proof)(false, substitutions: _*)(premise) match {
- case v: proof.ValidProofTactic => {
- val ps = v.validate(line, file)
- f(using lib, proof)(substitutions: _*)(ps)
- }
- case _ => ()
- }
- }
- try
- BasicStepTactic.TacticSubproof {
- f(substitutions: _*)(premise)
- }
- catch case _ => proof.InvalidProofTactic("Could not perform a substitution.")
- }
-
- def apply(using lib: lisa.prooflib.Library, proof: lib.Proof)(substitutions: (proof.Fact | Formula | RunningTheory#Justification)*)(premise: proof.Fact): proof.ProofTacticJudgement =
- exhaustive(using lib, proof)(substitutions: _*)(premise)
- }
- */
-}
diff --git a/src/main/scala/lisa/settheory/AxiomaticSetTheory.scala b/src/main/scala/lisa/settheory/AxiomaticSetTheory.scala
deleted file mode 100644
index c903827da2fcc16593e4734723f594b00b765142..0000000000000000000000000000000000000000
--- a/src/main/scala/lisa/settheory/AxiomaticSetTheory.scala
+++ /dev/null
@@ -1,5 +0,0 @@
-package lisa.settheory
-
-import lisa.kernel.proof.SCProofChecker
-
-object AxiomaticSetTheory extends SetTheoryTGAxioms {}
diff --git a/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala b/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
deleted file mode 100644
index 8a8282e4cbb9971a7d6fc2e9cbc0a88dbade9968..0000000000000000000000000000000000000000
--- a/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
+++ /dev/null
@@ -1,79 +0,0 @@
-package lisa.settheory
-
-import lisa.fol.FOL.{_, given}
-import lisa.kernel.proof.RunningTheory
-import lisa.utils.K
-
-/**
- * Base trait for set theoretical axiom systems.
- * Defines the symbols used in set theory.
- */
-private[settheory] trait SetTheoryDefinitions extends lisa.prooflib.Library {
-
- val theory = new RunningTheory()
-
- def axioms: Set[(String, AXIOM)] = Set.empty
-
- // Predicates
- /**
- * The symbol for the set membership predicate.
- */
- final val in = ConstantPredicateLabel("elem", 2)
-
- /**
- * The symbol for the subset predicate.
- */
- final val subset = ConstantPredicateLabel("subsetOf", 2)
-
- /**
- * The symbol for the equicardinality predicate. Needed for Tarski's axiom.
- */
- final val sim = ConstantPredicateLabel("sameCardinality", 2) // Equicardinality
- /**
- * Set Theory basic predicates
- */
- final val predicates = Set(in, subset, sim)
- // val choice
-
- // Functions
- /**
- * The symbol for the empty set constant.
- */
- final val emptySet = Constant("emptySet")
-
- /**
- * The symbol for the unordered pair function.
- */
- final val unorderedPair = ConstantFunctionLabel("unorderedPair", 2)
-
- /**
- * The symbol for the powerset function.
- */
- final val powerSet = ConstantFunctionLabel("powerSet", 1)
-
- /**
- * The symbol for the set union function.
- */
- final val union = ConstantFunctionLabel("union", 1)
-
- /**
- * The symbol for the universe function. Defined in TG set theory.
- */
- final val universe = ConstantFunctionLabel("universe", 1)
-
- /**
- * Set Theory basic functions.
- */
- final val functions = Set(unorderedPair, powerSet, union, universe)
-
- /**
- * The kernel theory loaded with Set Theory symbols and axioms.
- */
- // val runningSetTheory: RunningTheory = new RunningTheory()
- // given RunningTheory = runningSetTheory
-
- predicates.foreach(s => addSymbol(s))
- functions.foreach(s => addSymbol(s))
- addSymbol(emptySet)
-
-}
diff --git a/src/main/scala/lisa/settheory/SetTheoryLibrary.scala b/src/main/scala/lisa/settheory/SetTheoryLibrary.scala
deleted file mode 100644
index 1829975053e3e4d302f1c04a39aa8e13a08b76b5..0000000000000000000000000000000000000000
--- a/src/main/scala/lisa/settheory/SetTheoryLibrary.scala
+++ /dev/null
@@ -1,23 +0,0 @@
-package lisa.settheory
-
-import lisa.prooflib.Library
-
-/**
- * Specific implementation of [[utilities.Library]] for Set Theory, with a RunningTheory that is supposed to be used by the standard library.
- */
-object SetTheoryLibrary extends SetTheoryTGAxioms {
- export lisa.fol.FOL.{*, given}
- // Unicode symbols
-
- val ∅ = emptySet
- val ∈ = in
-
- extension (thi: Term) {
- def ∈(that: Term): Formula = in(thi, that)
- def ⊆(that: Term): Formula = subset(thi, that)
-
- def =/=(that: Term): Formula = !(===(thi, that))
-
- }
-
-}
diff --git a/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala b/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
deleted file mode 100644
index 9f4b15a4360f643fa829cea5f562f48019f81ff9..0000000000000000000000000000000000000000
--- a/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
+++ /dev/null
@@ -1,28 +0,0 @@
-package lisa.settheory
-
-import lisa.fol.FOL.{_, given}
-import lisa.utils.K
-
-/**
- * Axioms for the Tarski-Grothendieck theory (TG)
- */
-private[settheory] trait SetTheoryTGAxioms extends SetTheoryZFAxioms {
- private val x = variable
- private val y = variable
- private val z = variable
-
- final val tarskiAxiom: AXIOM = Axiom(
- forall(
- x,
- in(x, universe(x)) /\
- forall(
- y,
- in(y, universe(x)) ==> (in(powerSet(y), universe(x)) /\ subset(powerSet(y), universe(x))) /\
- forall(z, subset(z, universe(x)) ==> (sim(y, universe(x)) /\ in(y, universe(x))))
- )
- )
- )
-
- override def axioms: Set[(String, AXIOM)] = super.axioms + (("TarskiAxiom", tarskiAxiom))
-
-}
diff --git a/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala b/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
deleted file mode 100644
index 56c314f0503ea0b7e8c619d811bfa2adef9c5e01..0000000000000000000000000000000000000000
--- a/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
+++ /dev/null
@@ -1,31 +0,0 @@
-package lisa.settheory
-
-import lisa.fol.FOL.{_, given}
-import lisa.utils.K
-import lisa.utils.K.makeAxiom
-
-/**
- * Axioms for the Zermelo-Fraenkel theory (ZF)
- */
-private[settheory] trait SetTheoryZFAxioms extends SetTheoryZAxioms {
- private val x = variable
- private val y = variable
- private val A = variable
- private val B = variable
- private val P = predicate[3]
- // private final val sPsi = SchematicPredicateLabel("P", 3)
-
- /**
- * Replacement Schema --- If a predicate `P` is 'functional' over `x`, i.e.,
- * given `a ∈ x`, there is a unique `b` such that `P(x, a, b)`, then the
- * 'image' of `x` in P exists and is a set. It contains exactly the `b`'s that
- * satisfy `P` for each `a ∈ x`.
- */
- final val replacementSchema: AXIOM = Axiom(
- forall(A, in(A, x) ==> existsOne(B, P(x, A, B))) ==>
- exists(y, forall(B, in(B, y) <=> exists(A, in(A, x) /\ P(x, A, B))))
- )
-
- override def axioms: Set[(String, AXIOM)] = super.axioms + (("replacementSchema", replacementSchema))
-
-}
diff --git a/src/test/scala/lisa/proven/SimpleProverTests.scala b/src/test/scala/lisa/proven/SimpleProverTests.scala
deleted file mode 100644
index 8e3e65c0d37bb04a98f8b97802968bb6244c5438..0000000000000000000000000000000000000000
--- a/src/test/scala/lisa/proven/SimpleProverTests.scala
+++ /dev/null
@@ -1,34 +0,0 @@
-package lisa.proven
-
-import lisa.automation.kernel.SimplePropositionalSolver as SPS
-import lisa.kernel.fol.FOL.*
-import lisa.kernel.proof.RunningTheory
-import lisa.kernel.proof.RunningTheory.PredicateLogic
-import lisa.kernel.proof.SCProofChecker
-import lisa.utils.FOLPrinter
-import lisa.utils.KernelHelpers.*
-import lisa.utils.tptp.KernelParser.*
-import lisa.utils.tptp.ProblemGatherer.getPRPproblems
-import org.scalatest.funsuite.AnyFunSuite
-
-import scala.language.adhocExtensions
-
-class SimpleProverTests extends AnyFunSuite {
-
- /*
- test("Simple propositional logic proofs") {
- val problems = getPRPproblems.take(1)
- problems.foreach( pr => {
- println("--- Problem "+pr.file)
- val sq = problemToSequent(pr)
- println(FOLPrinter.prettySequent(sq))
- val proof = SPS.solveSequent(sq)
- if (!Seq("Unsatisfiable", "Theorem", "Satisfiable").contains(pr.status)) println("Unknown status: "+pr.status+", "+pr.file)
-
- assert(SCProofChecker.checkSCProof(proof).isValid == (pr.status =="Unsatisfiable" || pr.status == "Theorem"))
-
- })
-
- }
- */
-}