Adding abstract topology to LISA

build.sbt

@@ -1,4 +1,4 @@
-ThisBuild / version      := "0.7"
+ThisBuild / version := "0.7"
 ThisBuild / homepage := Some(url("https://github.com/epfl-lara/lisa"))
 ThisBuild / startYear := Some(2021)
 ThisBuild / organization := "ch.epfl.lara"
@@ -7,10 +7,10 @@ ThisBuild / organizationHomepage := Some(url("https://lara.epfl.ch"))
 ThisBuild / licenses := Seq("Apache-2.0" -> url("https://www.apache.org/licenses/LICENSE-2.0.html"))
 ThisBuild / versionScheme := Some("semver-spec")
 ThisBuild / scalacOptions ++= Seq(
-      "-feature",
-      "-deprecation",
-      "-unchecked",
-    )
+  "-feature",
+  "-deprecation",
+  "-unchecked"
+)
 ThisBuild / javacOptions ++= Seq("-encoding", "UTF-8")
 ThisBuild / semanticdbEnabled := true
 ThisBuild / semanticdbVersion := scalafixSemanticdb.revision
@@ -19,7 +19,6 @@ val scala2 = "2.13.8"
 val scala3 = "3.5.1"
 val commonSettings = Seq(
   crossScalaVersions := Seq(scala3),
-
   run / fork := true
 )
 
@@ -31,9 +30,8 @@ val commonSettings3 = commonSettings ++ Seq(
   scalaVersion := scala3,
   scalacOptions ++= Seq(
     "-language:implicitConversions",
-    //"-rewrite", "-source", "3.4-migration",
+    // "-rewrite", "-source", "3.4-migration",
     "-Wconf:msg=.*will never be selected.*:silent"
-
   ),
   javaOptions += "-Xmx10G",
   libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.18" % "test",
@@ -50,9 +48,9 @@ def githubProject(repo: String, commitHash: String) = RootProject(uri(s"$repo#$c
 lazy val customTstpParser = githubProject("https://github.com/SimonGuilloud/scala-tptp-parser.git", "eae9c1b7a9546f74779d77ff50fa6e8a1654cfa0")
 
 lazy val root = Project(
-    id = "lisa",
-    base = file("."),
-  )
+  id = "lisa",
+  base = file(".")
+)
   .settings(commonSettings3)
   .dependsOn(kernel, withTests(utils), withTests(sets)) // Everything but `examples`
   .aggregate(utils) // To run tests on all modules
@@ -75,17 +73,26 @@ lazy val sets = Project(
   .settings(commonSettings3)
   .dependsOn(kernel, withTests(utils))
 
+lazy val topologies = Project(
+  id = "lisa-topology",
+  base = file("lisa-topology")
+)
+  .settings(commonSettings3)
+  .dependsOn(kernel, sets, withTests(utils))
+
 lazy val utils = Project(
   id = "lisa-utils",
   base = file("lisa-utils")
 )
-  .settings(commonSettings3 ++ Seq(
-    libraryDependencies += "ch.epfl.lara" %% "scallion" % "0.6" from "https://github.com/epfl-lara/scallion/releases/download/v0.6/scallion_3-0.6.jar",
-    libraryDependencies += "ch.epfl.lara" %% "silex" % "0.6" from "https://github.com/epfl-lara/silex/releases/download/v0.6/silex_3-0.6.jar",
-  ))
+  .settings(
+    commonSettings3 ++ Seq(
+      libraryDependencies += "ch.epfl.lara" %% "scallion" % "0.6" from "https://github.com/epfl-lara/scallion/releases/download/v0.6/scallion_3-0.6.jar",
+      libraryDependencies += "ch.epfl.lara" %% "silex" % "0.6" from "https://github.com/epfl-lara/silex/releases/download/v0.6/silex_3-0.6.jar"
+    )
+  )
   .dependsOn(kernel)
   .dependsOn(customTstpParser)
-  //.settings(libraryDependencies += "io.github.leoprover" % "scala-tptp-parser_2.13" % "1.4")
+//.settings(libraryDependencies += "io.github.leoprover" % "scala-tptp-parser_2.13" % "1.4")
 
 ThisBuild / assemblyMergeStrategy := {
   case PathList("module-info.class") => MergeStrategy.discard
@@ -97,7 +104,6 @@ ThisBuild / assemblyMergeStrategy := {
     oldStrategy(x)
 }
 
-
 lazy val examples = Project(
   id = "lisa-examples",
   base = file("lisa-examples")

lisa-sets/src/main/scala/lisa/automation/Congruence.scala

@@ -1,11 +1,11 @@
 package lisa.automation
+import leo.datastructures.TPTP.CNF.AtomicFormula
 import lisa.fol.FOL.{*, given}
 import lisa.prooflib.BasicStepTactic.*
 import lisa.prooflib.ProofTacticLib.*
 import lisa.prooflib.SimpleDeducedSteps.*
 import lisa.prooflib.*
 import lisa.utils.parsing.UnreachableException
-import leo.datastructures.TPTP.CNF.AtomicFormula
 
 /**
   * This tactic tries to prove a sequent by congruence.

lisa-sets/src/main/scala/lisa/automation/settheory/SetTheoryTactics.scala

@@ -2,6 +2,7 @@ package lisa.automation.settheory
 
 import lisa.SetTheoryLibrary.{_, given}
 import lisa.automation.Tautology
+import lisa.automation.kernel.CommonTactics.ExistenceAndUniqueness
 import lisa.fol.FOL.{_, given}
 import lisa.kernel.proof.SequentCalculus as SCunique
 import lisa.maths.Quantifiers
@@ -21,8 +22,10 @@ object SetTheoryTactics {
   private val x = variable
   private val y = variable
   private val z = variable
+  private val v = variable
   private val h = formulaVariable
   private val P = predicate[1]
+  private val Q = predicate[1]
   private val schemPred = predicate[1]
 
   /**
@@ -197,4 +200,99 @@ object SetTheoryTactics {
       unwrapTactic(sp)("Subproof for unique comprehension failed.")
     }
   }
+
+  /**
+   * Defines the element that is uniquely given by the uniqueness theorem, or falls back to the error element if the
+   * assumptions of the theorem are not satisfied.
+   *
+   * This is useful in defining specific elements in groups, where their uniqueness (and existence) strongly rely
+   * on the assumption of the group structure.
+   */
+  object TheConditional {
+    def apply(using om: OutputManager)(u: Variable, f: Formula)(just: JUSTIFICATION, defaultValue: Term = ∅): The = {
+      val seq = just.statement
+
+      if (seq.left.isEmpty) {
+        The(u, f)(just)
+      } else {
+        val prem = if (seq.left.size == 1) seq.left.head else And(seq.left.toSeq)
+        val completeDef = (prem ==> f) /\ (!prem ==> (u === defaultValue))
+        val substF = completeDef.substitute(u := defaultValue)
+        val substDef = completeDef.substitute(u := v)
+
+        val completeUniquenessTheorem = Lemma(
+          ∃!(u, completeDef)
+        ) {
+          val case1 = have(prem |- ∃!(u, completeDef)) subproof {
+            // We prove the equivalence f <=> completeDef so that we can substitute it in the uniqueness quantifier
+            val equiv = have(prem |- ∀(u, f <=> completeDef)) subproof {
+              have(f |- f) by Hypothesis
+              thenHave((prem, f) |- f) by Weakening
+              val left = thenHave(f |- (prem ==> f)) by Restate
+
+              have(prem |- prem) by Hypothesis
+              thenHave((prem, !prem) |- ()) by LeftNot
+              thenHave((prem, !prem) |- (u === defaultValue)) by Weakening
+              val right = thenHave(prem |- (!prem ==> (u === defaultValue))) by Restate
+
+              have((prem, f) |- completeDef) by RightAnd(left, right)
+              val forward = thenHave(prem |- f ==> completeDef) by Restate
+
+              have(completeDef |- completeDef) by Hypothesis
+              thenHave((prem, completeDef) |- completeDef) by Weakening
+              thenHave((prem, completeDef) |- f) by Tautology
+              val backward = thenHave(prem |- completeDef ==> f) by Restate
+
+              have(prem |- f <=> completeDef) by RightIff(forward, backward)
+              thenHave(thesis) by RightForall
+            }
+
+            val substitution = have((∃!(u, f), ∀(u, f <=> completeDef)) |- ∃!(u, completeDef)) by Tautology.from(
+              Quantifiers.uniqueExistentialEquivalenceDistribution of (P := lambda(u, f), Q := lambda(u, completeDef))
+            )
+
+            val implication = have((prem, ∃!(u, f)) |- ∃!(u, completeDef)) by Cut(equiv, substitution)
+            val uniqueness = have(prem |- ∃!(u, f)) by Restate.from(just)
+            have(prem |- ∃!(u, completeDef)) by Cut(uniqueness, implication)
+          }
+
+          val case2 = have(!prem |- ∃!(u, completeDef)) subproof {
+            val existence = have(!prem |- ∃(u, completeDef)) subproof {
+              have(!prem |- !prem) by Hypothesis
+              thenHave((prem, !prem) |- ()) by LeftNot
+              thenHave((prem, !prem) |- substF) by Weakening
+              val left = thenHave(!prem |- (prem ==> substF)) by Restate
+
+              have(defaultValue === defaultValue) by RightRefl
+              thenHave(!prem |- defaultValue === defaultValue) by Weakening
+              val right = thenHave(!prem ==> (defaultValue === defaultValue)) by Restate
+
+              have(!prem |- (prem ==> substF) /\ (!prem ==> (defaultValue === defaultValue))) by RightAnd(left, right)
+              thenHave(thesis) by RightExists.withParameters(defaultValue)
+            }
+
+            val uniqueness = have((!prem, completeDef, substDef) |- (u === v)) subproof {
+              assume(!prem)
+              assume(completeDef)
+              assume(substDef)
+
+              val eq1 = have(u === defaultValue) by Tautology
+              val eq2 = have(defaultValue === v) by Tautology
+              val p = have((u === defaultValue) /\ (defaultValue === v)) by RightAnd(eq1, eq2)
+
+              val transitivity = Quantifiers.equalityTransitivity of (x -> u, y -> defaultValue, z -> v)
+              have(thesis) by Cut(p, transitivity)
+            }
+
+            have(thesis) by ExistenceAndUniqueness(completeDef)(existence, uniqueness)
+          }
+
+          have(thesis) by Tautology.from(case1, case2)
+        }
+
+        The(u, completeDef)(completeUniquenessTheorem)
+      }
+    }
+  }
+
 }

lisa-sets/src/main/scala/lisa/maths/settheory/SetTheory.scala

@@ -917,16 +917,21 @@ object SetTheory extends lisa.Main {
    */
   val setIntersection = DEF(x, y) --> The(z, ∀(t, in(t, z) <=> (in(t, x) /\ in(t, y))))(setIntersectionUniqueness)
 
-  val setIntersectionCommutativity = Theorem(
-    setIntersection(x, y) === setIntersection(y, x)
+  val setIntersectionMembership = Theorem(
+    in(t, setIntersection(x, y)) <=> (in(t, x) /\ in(t, y))
   ) {
-    sorry
+    have(forall(t, in(t, setIntersection(x, y)) <=> (in(t, x) /\ in(t, y)))) by InstantiateForall(setIntersection(x, y))(setIntersection.definition)
+    thenHave(thesis) by InstantiateForall(t)
   }
 
-  val setIntersectionMembership = Theorem(
-    in(t, setIntersection(x, y)) <=> (in(t, x) /\ in(t, y))
+  val setIntersectionCommutativity = Theorem(
+    setIntersection(x, y) === setIntersection(y, x)
   ) {
-    sorry
+    val left = have(in(t, setIntersection(x, y)) <=> (in(t, y) /\ in(t, x))) by Tautology.from(setIntersectionMembership)
+    val right = have(in(t, setIntersection(y, x)) <=> (in(t, y) /\ in(t, x))) by Tautology.from(setIntersectionMembership of (x := y, y := x))
+    have(in(t, setIntersection(x, y)) <=> in(t, setIntersection(y, x))) by Tautology.from(left, right)
+    val equalityPrepare = thenHave(forall(t, (in(t, setIntersection(x, y)) <=> in(t, setIntersection(y, x))))) by RightForall
+    have(thesis) by Tautology.from(equalityPrepare, extensionalityAxiom of (x := setIntersection(x, y), y := setIntersection(y, x)))
   }
 
   extension (x: Term) {
@@ -1030,6 +1035,11 @@ object SetTheory extends lisa.Main {
    */
   val setDifference = DEF(x, y) --> The(z, ∀(t, in(t, z) <=> (in(t, x) /\ !in(t, y))))(setDifferenceUniqueness)
 
+  val setDifferenceMembership = Theorem(in(t, setDifference(x, y)) <=> (in(t, x) /\ !in(t, y))) {
+    have(∀(t, in(t, setDifference(x, y)) <=> (in(t, x) /\ !in(t, y)))) by InstantiateForall(setDifference(x, y))(setDifference.definition)
+    thenHave(thesis) by InstantiateForall(t)
+  }
+
   /**
    * Theorem --- Intersection of a non-empty Class is a Set
    *