Group Theory

lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala

@@ -103,6 +103,10 @@ object KernelHelpers {
   extension (t: Term) {
     infix def ===(u: Term): Formula = PredicateFormula(equality, Seq(t, u))
     infix def ＝(u: Term): Formula = PredicateFormula(equality, Seq(t, u))
+
+    infix def !==(u: Term): Formula = !(t === u)
+
+    infix def ≠(u: Term): Formula = !(t === u)
   }
 
   /* Conversions */

src/main/scala/lisa/automation/kernel/CommonTactics.scala

@@ -8,8 +8,13 @@ import lisa.prooflib.BasicStepTactic.*
 import lisa.prooflib.ProofTacticLib.{_, given}
 import lisa.prooflib.SimpleDeducedSteps.*
 import lisa.prooflib.*
+import lisa.utils.FOLPrinter
 import lisa.utils.KernelHelpers.{_, given}
 
+import scala.collection.immutable.Queue
+import scala.collection.mutable.{Map => MutableMap}
+import scala.collection.mutable.{Set => MutableSet}
+
 object CommonTactics {
 
   /**
@@ -57,6 +62,7 @@ object CommonTactics {
         proof.InvalidProofTactic("Could not infer correct right pivots.")
       } else {
         val gammaPrime = uniquenessSeq.left.filter(f => !isSame(f, phi) && !isSame(f, substPhi))
+        val deltaPrime = uniquenessSeq.right.filter(f => !isSame(f, (x === y)) && !isSame(f, (y === x)))
 
         TacticSubproof {
           // There's got to be a better way of importing have/thenHave/assume methods
@@ -72,13 +78,13 @@ object CommonTactics {
             lib.assume(f)
           }
 
-          val backward = lib.have(phi |- (substPhi ==> (x === y))) by Restate.from(uniqueness)
+          val backward = lib.have(phi |- (deltaPrime + (substPhi ==> (x === y)))) by Restate.from(uniqueness)
 
-          lib.have(phi |- ((x === y) <=> substPhi)) by RightIff(forward, backward)
-          lib.thenHave(phi |- ∀(y, (x === y) <=> substPhi)) by RightForall
-          lib.thenHave(phi |- ∃(x, ∀(y, (x === y) <=> substPhi))) by RightExists
-          lib.thenHave(∃(x, phi) |- ∃(x, ∀(y, (x === y) <=> substPhi))) by LeftExists
-          lib.thenHave(∃(x, phi) |- ∃!(x, phi)) by RightExistsOne
+          lib.have(phi |- (deltaPrime + ((x === y) <=> substPhi))) by RightIff(forward, backward)
+          lib.thenHave(phi |- (deltaPrime + ∀(y, (x === y) <=> substPhi))) by RightForall
+          lib.thenHave(phi |- (deltaPrime + ∃(x, ∀(y, (x === y) <=> substPhi)))) by RightExists
+          lib.thenHave(∃(x, phi) |- (deltaPrime + ∃(x, ∀(y, (x === y) <=> substPhi)))) by LeftExists
+          lib.thenHave(∃(x, phi) |- (deltaPrime + ∃!(x, phi))) by RightExistsOne
 
           lib.have(bot) by Cut(existence, lib.lastStep)
         }
@@ -231,10 +237,11 @@ object CommonTactics {
                     FOL.ConnectorFormula(FOL.Implies, Seq(a, f)),
                     FOL.ConnectorFormula(FOL.Implies, Seq(b, g))
                   )
-                ) if isSame(FOL.Neg(a), b) =>
+                ) if isSame(FOL.Neg(a), b) => {
               if (isSame(a, phi)) FOL.LambdaTermFormula(Seq(y), f)
               else if (isSame(b, phi)) FOL.LambdaTermFormula(Seq(y), g)
               else return proof.InvalidProofTactic("Condition of definition is not satisfied.")
+            }
 
             case _ => return proof.InvalidProofTactic("Definition is not conditional.")
           }
@@ -250,11 +257,192 @@ object CommonTactics {
             lib.thenHave((f(xs) === f(xs)) <=> P(Seq(f(xs)))) by InstFunSchema(Map(y -> f(xs)))
             lib.thenHave(P(Seq(f(xs)))) by Restate
             lib.thenHave(phi ==> Q(Seq(f(xs)))) by Tautology
-            lib.thenHave(phi |- Q(Seq(f(xs)))) by Restate
+            lib.thenHave(bot) by Restate
           }
 
         case _ => proof.InvalidProofTactic("Could not get definition of function.")
       }
     }
   }
+
+  /**
+   * <pre>
+   * Γ |- a(0) === a(1)   Γ' |- a(2) === a(3) ...
+   * --------------------------------------------
+   * Γ, Γ', ... |- a(i) === a(j)
+   * </pre>
+   * Proves any equality induced transitively by the equalities of the premises.
+   *
+   * Internally, we construct an undirected graph, where sides of an equality are represented by vertices, and
+   * an edge between two terms `a` and `b` means that some premise proves `a === b` (or equivalently `b === a`).
+   * We also keep the premise from which the equality stems as a label of the edge to construct the final antecedent of
+   * the bottom sequent.
+   *
+   * We can see that an equality `a === b` is provable from the premises if and only if `a` is reachable from `b`.
+   * We thus run Breadth-First Search (BFS) on the graph starting from `a` to find the smallest solution (in terms of
+   * sequent calculus steps), if any.
+   */
+  object Equalities extends ProofTactic {
+    def apply(using lib: Library, proof: lib.Proof)(equalities: proof.Fact*)(bot: Sequent): proof.ProofTacticJudgement = {
+      // Construct the graph as an adjacency list for O(1) equality checks
+      val graph = MutableMap[FOL.Term, List[FOL.Term]]()
+      val premises = MutableMap[(FOL.Term, FOL.Term), proof.Fact]()
+
+      // Use a variable to avoid non-local returns
+      // This is because the below loop is rewritten using maps and filters under the hood
+      var error: Option[proof.InvalidProofTactic] = None
+      for (premise <- equalities; f <- proof.getSequent(premise).right) {
+        f match {
+          case FOL.PredicateFormula(FOL.`equality`, Seq(x: FOL.Term, y: FOL.Term)) =>
+            if (error.isEmpty) {
+              // In case of conflicts, it would be too costly in the general case to find which premise is appropriate
+              // We simply throw an error to indicate that something is wrong with the premises
+              if (premises.contains((x, y)) && premises((x, y)) != premise) {
+                // TODO Indicate which premises lead to the error
+                error = Some(proof.InvalidProofTactic(s"Equality ${FOLPrinter.prettyTerm(x)} === ${FOLPrinter.prettyTerm(y)} was proven in two different premises."))
+              } else {
+                graph(x) = y :: graph.getOrElse(x, Nil)
+                graph(y) = x :: graph.getOrElse(y, Nil)
+                premises += ((x, y) -> premise)
+                premises += ((y, x) -> premise)
+              }
+            }
+          case _ =>
+            if (error.isEmpty) {
+              error = Some(proof.InvalidProofTactic("Right-hand side of premises should only contain equalities."))
+            }
+        }
+      }
+
+      if (error.nonEmpty) {
+        return error.get
+      }
+
+      if (bot.right.size != 1) {
+        return proof.InvalidProofTactic(s"Right-hand side of bottom sequent expected exactly 1 formula, got ${bot.right.size}")
+      }
+
+      bot.right.head match {
+        case FOL.PredicateFormula(FOL.`equality`, Seq(x: FOL.Term, y: FOL.Term)) =>
+          // Optimization in the trivial case x === x
+          if (isSameTerm(x, y)) {
+            return TacticSubproof {
+              lib.have(x === y) by RightRefl
+              if (bot.left.nonEmpty) {
+                lib.thenHave(bot) by Weakening
+              }
+            }
+          }
+
+          // Run BFS on the graph
+          var Q = Queue[FOL.Term](x)
+          val explored = MutableSet[FOL.Term](x)
+          val parent = MutableMap[FOL.Term, FOL.Term]()
+          while (Q.nonEmpty) {
+            val (v, newQ) = Q.dequeue
+            Q = newQ
+            if (v == y) {
+              lazy val traversal: LazyList[FOL.Term] = y #:: traversal.map(parent)
+              val path = (traversal.tail.takeWhile(_ != x) :+ x).toList // Path from y (excluded) to x (included)
+
+              def getEqTerms(using lib: Library, proof: lib.Proof)(eq: proof.Fact): (FOL.Term, FOL.Term) =
+                proof.getSequent(eq).right.head match {
+                  case FOL.PredicateFormula(`equality`, Seq(a, b)) => (a, b)
+                  case _ => throw IllegalArgumentException("Not an equality.")
+                }
+
+              def order(using lib: Library, proof: lib.Proof)(eq: proof.Fact, first: FOL.Term, second: FOL.Term): proof.Fact = {
+                val seq = proof.getSequent(eq)
+                seq.right.head match {
+                  case FOL.PredicateFormula(`equality`, Seq(`first`, `second`)) => eq
+                  case FOL.PredicateFormula(`equality`, Seq(`second`, `first`)) => {
+                    val u = variable
+                    lib.have(first === first) by RightRefl
+                    lib.thenHave(second === first |- first === second) by RightSubstEq(List((second, first)), lambda(u, first === u))
+                    lib.have(seq.left |- first === second) by Cut(eq, lib.lastStep)
+                  }
+                  case _ => throw IllegalArgumentException("First or last is not present in the given equality.")
+                }
+              }
+
+              return TacticSubproof { (innerProof: proof.InnerProof) ?=>
+                val initialStep = order(premises(y -> path.head), path.head, y)
+                val u = variable
+
+                path
+                  .zip(path.tail)
+                  .foldLeft(initialStep)((leftEq, vars) => {
+                    val leftSeq = innerProof.getSequent(leftEq)
+                    val (a, b) = vars
+                    val premiseEq = premises(vars)
+                    val premiseSeq = proof.getSequent(premiseEq)
+
+                    // Apply equality transitivity on (a === y) /\ (a === b) to get (b === y)
+                    // TODO Watch for issue #161, as assumptions will break this step
+                    lib.have((leftSeq.left + premiseSeq.right.head) |- b === y) by RightSubstEq(
+                      List(getEqTerms(premiseEq)),
+                      lambda(u, u === y)
+                    )(leftEq)
+                    val seq = (leftSeq.left ++ premiseSeq.left) |- b === y
+                    val eq = lib.have(seq) by Cut(premiseEq, lib.lastStep)
+
+                    eq
+                  })
+              }
+            }
+
+            for (w <- graph(v) if !explored.contains(w)) {
+              explored += w
+              parent(w) = v
+              Q = Q.enqueue(w)
+            }
+          }
+          proof.InvalidProofTactic("Equality is not provable from the premises.")
+
+        case _ => proof.InvalidProofTactic("Right-hand side of bottom sequent should be of the form x === y.")
+      }
+    }
+  }
+
+  /**
+   * <pre>
+   * Γ, φ |- Δ, Σ   Γ, ¬φ |- Δ, Σ'
+   * -----------------------------
+   * Γ |- Δ
+   * </pre>
+   *
+   * TODO: Extending the tactic to more general pivots
+   */
+  object Cases extends ProofTactic {
+    def withParameters(using lib: Library, proof: lib.Proof, om: OutputManager)(phi: Formula)(pos: proof.Fact, neg: proof.Fact)(bot: Sequent): proof.ProofTacticJudgement = {
+      val seqPos = proof.getSequent(pos)
+      val seqNeg = proof.getSequent(neg)
+
+      if (
+        !(contains(seqPos.left, phi) && contains(seqNeg.left, !phi) && !contains(seqNeg.left, phi)) &&
+        !(contains(seqPos.left, !phi) && contains(seqNeg.left, phi) && !contains(seqNeg.left, !phi))
+      ) {
+        proof.InvalidProofTactic("The given sequent do not contain φ or ¬φ.")
+      } else {
+        val gamma = bot.left
+        TacticSubproof {
+          val excludedMiddle = lib.have(phi \/ !phi) by Tautology
+          val toCut = lib.have((gamma + (phi \/ !phi)) |- bot.right) by LeftOr(pos, neg)
+
+          lib.have(bot) by Cut(excludedMiddle, toCut)
+        }
+      }
+    }
+
+    def apply(using lib: Library, proof: lib.Proof, om: OutputManager)(pos: proof.Fact, neg: proof.Fact)(bot: Sequent): proof.ProofTacticJudgement = {
+      val seqPos = proof.getSequent(pos)
+      val pivot = seqPos.left -- bot.left
+
+      if (pivot.size != 1) {
+        proof.InvalidProofTactic("Could not infer correct formula φ.")
+      } else {
+        Cases.withParameters(pivot.head)(pos, neg)(bot)
+      }
+    }
+  }
 }

src/main/scala/lisa/mathematics/FirstOrderLogic.scala

@@ -1,5 +1,6 @@
 package lisa.mathematics
 
+import lisa.automation.kernel.CommonTactics.Cases
 import lisa.automation.kernel.OLPropositionalSolver.Tautology
 import lisa.automation.kernel.SimplePropositionalSolver.*
 import lisa.automation.kernel.SimpleSimplifier.*
@@ -70,6 +71,46 @@ object FirstOrderLogic extends lisa.Main {
     thenHave(thesis) by Restate
   }
 
+  /**
+   * Theorem -- If `P` and `Q` are equivalent, then `∃(x, P(x))` implies `∃(x, Q(x))`.
+   */
+  val substitutionInExistenceQuantifier = Theorem(
+    (∃(x, P(x)), ∀(y, P(y) <=> Q(y))) |- ∃(x, Q(x))
+  ) {
+    have(P(x) |- P(x)) by Hypothesis
+    val substitution = thenHave((P(x), P(x) <=> Q(x)) |- Q(x)) by RightSubstIff(List((P(x), Q(x))), lambda(p, p))
+
+    have(∀(y, P(y) <=> Q(y)) |- ∀(y, P(y) <=> Q(y))) by Hypothesis
+    val equiv = thenHave(∀(y, P(y) <=> Q(y)) |- P(x) <=> Q(x)) by InstantiateForall(x)
+
+    have((P(x), ∀(y, P(y) <=> Q(y))) |- Q(x)) by Cut(equiv, substitution)
+    thenHave((P(x), ∀(y, P(y) <=> Q(y))) |- ∃(x, Q(x))) by RightExists
+    thenHave(thesis) by LeftExists
+  }
+
+  /**
+   * Theorem -- If `P` and `Q` are equivalent, then `∃!(x, P(x))` implies `∃!(x, Q(x))`.
+   */
+  val substitutionInUniquenessQuantifier = Theorem(
+    (∃!(x, P(x)), ∀(y, P(y) <=> Q(y))) |- ∃!(x, Q(x))
+  ) {
+    have((x === y) <=> P(y) |- (x === y) <=> P(y)) by Hypothesis
+    thenHave(∀(y, (x === y) <=> P(y)) |- (x === y) <=> P(y)) by LeftForall
+    val substitution = thenHave((∀(y, (x === y) <=> P(y)), P(y) <=> Q(y)) |- (x === y) <=> Q(y)) by RightSubstIff(
+      List((P(y), Q(y))),
+      lambda(p, (x === y) <=> p)
+    )
+
+    have(∀(y, P(y) <=> Q(y)) |- ∀(y, P(y) <=> Q(y))) by Hypothesis
+    val equiv = thenHave(∀(y, P(y) <=> Q(y)) |- P(y) <=> Q(y)) by InstantiateForall(y)
+
+    have((∀(y, (x === y) <=> P(y)), ∀(y, P(y) <=> Q(y))) |- (x === y) <=> Q(y)) by Cut(equiv, substitution)
+    thenHave((∀(y, (x === y) <=> P(y)), ∀(y, P(y) <=> Q(y))) |- ∀(y, (x === y) <=> Q(y))) by RightForall
+    thenHave((∀(y, (x === y) <=> P(y)), ∀(y, P(y) <=> Q(y))) |- ∃(x, ∀(y, (x === y) <=> Q(y)))) by RightExists
+    thenHave((∃(x, ∀(y, (x === y) <=> P(y))), ∀(y, P(y) <=> Q(y))) |- ∃(x, ∀(y, (x === y) <=> Q(y)))) by LeftExists
+    thenHave(thesis) by Restate
+  }
+
   /**
    * Theorem --- Equality relation is transitive.
    */
@@ -354,4 +395,42 @@ object FirstOrderLogic extends lisa.Main {
     thenHave(thesis) by Restate
   }
 
+  /**
+   * Theorem --- Unique existential quantifier distributes fully with a closed formula.
+   */
+  val uniqueExistentialConjunctionWithClosedFormula = Theorem(
+    existsOne(x, P(x) /\ p()) <=> (existsOne(x, P(x)) /\ p())
+  ) {
+    val pos = have(p() |- existsOne(x, P(x) /\ p()) <=> (existsOne(x, P(x)) /\ p())) subproof {
+      have(p() |- (P(x) /\ p()) <=> P(x)) by Tautology
+      thenHave(p() |- forall(x, (P(x) /\ p()) <=> P(x))) by RightForall
+
+      have(p() |- existsOne(x, P(x) /\ p()) <=> (existsOne(x, P(x)))) by Cut(
+        lastStep,
+        uniqueExistentialEquivalenceDistribution of (
+          P -> lambda(x, P(x) /\ p()),
+          Q -> lambda(x, P(x))
+        )
+      )
+      thenHave(thesis) by Tautology
+    }
+
+    val neg = have(!p() |- existsOne(x, P(x) /\ p()) <=> (existsOne(x, P(x)) /\ p())) subproof {
+      have((!p(), (x === x) <=> (P(x) /\ p())) |- p()) by Tautology
+      thenHave((!p(), forall(y, (x === y) <=> (P(y) /\ p()))) |- p()) by LeftForall
+      thenHave((!p(), exists(x, forall(y, (x === y) <=> (P(y) /\ p())))) |- p()) by LeftExists
+      thenHave((!p(), existsOne(x, P(x) /\ p())) |- p()) by LeftExistsOne
+      thenHave((!p(), existsOne(x, P(x) /\ p())) |- ()) by LeftNot
+      thenHave((!p(), existsOne(x, P(x) /\ p())) |- existsOne(x, P(x)) /\ p()) by Weakening
+      val forward = thenHave(!p() |- existsOne(x, P(x) /\ p()) ==> (existsOne(x, P(x)) /\ p())) by Restate
+
+      have((!p(), existsOne(x, P(x)) /\ p()) |- ()) by Tautology
+      thenHave((!p(), existsOne(x, P(x)) /\ p()) |- existsOne(x, P(x) /\ p())) by Weakening
+      val backward = thenHave(!p() |- existsOne(x, P(x)) /\ p() ==> existsOne(x, P(x) /\ p())) by Restate
+
+      have(thesis) by RightIff(forward, backward)
+    }
+
+    have(thesis) by Cases(pos, neg)
+  }
 }