Reorganize (#191)

Reorganize and clean up files: Remove old unussed files, move the root project to lisa-sets, change lisa.mathematics to lisa.maths, some more.

.gitignore

@@ -16,3 +16,6 @@ target
 
 silex/*
 scallion/*
+
+# caching of theorems
+cache

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")

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 {
 

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
 

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.

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
+    }
+  }
+
+}

src/main/scala/lisa/settheory/SetTheoryZAxioms.scala → 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))
+
+  }
 
 }

src/main/scala/lisa/automation/kernel/CommonTactics.scala → 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.*

lisa-utils/src/main/scala/lisa/prooflib/Substitution.scala → 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