Extract definitions/theorems of functions, add Sigma and Pi

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

@@ -58,8 +58,6 @@ object CommonTactics {
         val gammaPrime = uniquenessSeq.left.filter(f => !F.isSame(f, phi) && !F.isSame(f, substPhi))
 
         TacticSubproof {
-          val x = variable
-          val y = variable
           // There's got to be a better way of importing have/thenHave/assume methods
           // but I did not find one
 

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

@@ -1,20 +1,28 @@
 package lisa.automation.settheory
 
 import lisa.SetTheoryLibrary.{_, given}
+import lisa.automation.Tautology
 import lisa.fol.FOL.{_, given}
 import lisa.kernel.proof.SequentCalculus as SCunique
+import lisa.maths.Quantifiers
 import lisa.maths.settheory.SetTheory
 import lisa.prooflib.BasicStepTactic.*
 import lisa.prooflib.Library
 import lisa.prooflib.ProofTacticLib.{_, given}
+import lisa.prooflib.SimpleDeducedSteps.Restate
 import lisa.prooflib.*
 import lisa.utils.Printer
+import lisa.utils.unification.UnificationUtils.FormulaSubstitution
+import lisa.utils.unification.UnificationUtils.TermSubstitution
+import lisa.utils.unification.UnificationUtils.matchFormula
 
 object SetTheoryTactics {
   // var defs
   private val x = variable
   private val y = variable
   private val z = variable
+  private val h = formulaVariable
+  private val P = predicate[1]
   private val schemPred = predicate[1]
 
   /**
@@ -35,7 +43,7 @@ object SetTheoryTactics {
    * @example
    * Generates a subproof for the unique existence of the set `{t ∈ x | t ∈ y}`:
    * {{{
-   *    have(() |- existsOne(z, forall(t, in(t, z) <=> (in(t, x) /\ in(t, y))))) by uniqueComprehension(x, lambda(Seq(t, x), in(t, y)))
+   *    have(() |- existsOne(z, forall(t, in(t, z) <=> (in(t, x) /\ in(t, y))))) by UniqueComprehension(x, lambda(Seq(t, x), in(t, y)))
    * }}}
    * See [[setIntersection]] or [[relationDomain]] for more usage.
    */
@@ -81,6 +89,112 @@ object SetTheoryTactics {
       // safely check, unwrap, and return the proof judgement
       unwrapTactic(sp)("Subproof for unique comprehension failed.")
     }
-  }
 
+    /**
+     * Similarly to [[UniqueComprehension]], generates a unique existence proof
+     * but for a set comprehension that is not over some other set `x`. To do so,
+     * A proof that the predicate `P(t)` implies membership to the set `x` must be
+     * given. This then asserts the unique existence of the set `{t | P(t)}`. Useful
+     * when a definition includes a redundant membership condition.
+     *
+     *    `P(t) ==> t ∈ x ⊢ ∃! z. ∀ t. t ∈ z ⇔ P(t)`
+     *
+     * @param originalSet the set to apply comprehension on
+     * @param separationPredicate the predicate to use for comprehension `(Term =>
+     * Term => Boolean)`
+     * @param predicateImpliesInOriginalSet proof of the form `P(t) ==> t ∈ originalSet`
+     * @return subproof for unique existence of the set defined by inputs
+     *
+     * @example
+     * Generates a subproof for the unique existence of the set `{t | ∃x. x ∈ a ∧ t = {x}}`:
+     * {{{
+     *    val implicationProof = have(exists(x, in(x, a) /\ (t === singleton(x))) ==> in(t, union(cartesianProduct(a, a)))) subproof {
+     *      // ...
+     *    }
+     *    have(() |- existsOne(z, forall(t, in(t, z) <=> exists(x, in(x, a) /\ (t === singleton(x)))))) by UniqueComprehension.fromOriginalSet(
+     *      union(cartesianProduct(a, a)),
+     *      lambda(t, exists(x, in(x, a) /\ (t === singleton(x)))),
+     *      implicationProof
+     *    )
+     * }}}
+     * See [[UniqueComprehension]] for more usage.
+     */
+    def fromOriginalSet(using
+        proof: Proof,
+        line: sourcecode.Line,
+        file: sourcecode.File,
+        om: OutputManager
+    )(originalSet: Term, separationPredicate: LambdaTF[1], predicateImpliesInOriginalSet: proof.Fact)( // TODO dotty forgets that Term <:< LisaObject[Term]
+        bot: Sequent
+    ): proof.ProofTacticJudgement = {
+      require(separationPredicate.bounds.length == 1)
+      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)
+      val t1 = Variable(freshId(takenIDs, x.id))
+      val t2 = Variable(freshId(takenIDs, y.id))
+
+      val separationCondition = separationPredicate(t2)
+      val targetDef = ∀(t2, in(t2, t1) <=> separationCondition)
+      val comprehension = ∀(t2, in(t2, t1) <=> in(t2, originalSet) /\ separationCondition)
+
+      // prepare predicateImpliesInOriginalSet for usage in a proof: rename variables
+      val predicateImpliesInOriginalSetForm = separationCondition ==> in(t2, originalSet)
+      val predicateImpliesInOriginalSetReady = matchFormula(
+        separationCondition ==> in(t2, originalSet),
+        predicateImpliesInOriginalSet.statement.right.head
+      ) match
+        case None =>
+          return proof.InvalidProofTactic(s"Unable to unify `predicateImpliesInOriginalSet` with the expected form: ${predicateImpliesInOriginalSetForm}")
+        case Some((formulaSubst, termSubst)) =>
+          predicateImpliesInOriginalSet
+            .of(formulaSubst.map((k, v) => SubstPair(k, v)).toSeq*)
+            .of(termSubst.map((k, v) => SubstPair(k, v)).toSeq*)
+
+      val sp = TacticSubproof {
+        // get uniqueness with the redundant original set membership
+        val uniq = have(∃!(t1, comprehension)) by UniqueComprehension(
+          originalSet,
+          lambda(t2, separationCondition)
+        )
+
+        // show that existence of the definition with the original set membership implies the
+        // existence of the definition without the original set membership
+        val transform = have(
+          ∃(t1, comprehension) |- ∃(t1, targetDef)
+        ) subproof {
+          // derive equivalence between t ∈ x /\ P(t) and P(t) from `predicateImpliesInOriginalSet`
+          val lhs = have(separationCondition ==> (in(t2, originalSet) /\ separationCondition)) by Tautology.from(predicateImpliesInOriginalSetReady)
+          val rhs = have(separationCondition /\ in(t2, originalSet) ==> separationCondition) by Restate
+          val subst = have(separationCondition <=> (in(t2, originalSet) /\ separationCondition)) by RightIff(lhs, rhs)
+
+          // subtitute and introduce quantifiers
+          have((in(t2, t1) <=> (in(t2, originalSet) /\ separationCondition)) |- in(t2, t1) <=> (in(t2, originalSet) /\ separationCondition)) by Hypothesis
+          val cutRhs = thenHave(
+            (in(t2, t1) <=> (in(t2, originalSet) /\ separationCondition), separationCondition <=> (in(t2, originalSet) /\ separationCondition)) |- in(t2, t1) <=> (separationCondition)
+          ) by RightSubstIff.withParametersSimple(List((separationCondition, in(t2, originalSet) /\ separationCondition)), lambda(h, in(t2, t1) <=> h))
+          have((in(t2, t1) <=> (in(t2, originalSet) /\ separationCondition)) |- in(t2, t1) <=> (separationCondition)) by Cut(subst, cutRhs)
+          thenHave(∀(t2, in(t2, t1) <=> (in(t2, originalSet) /\ separationCondition)) |- in(t2, t1) <=> (separationCondition)) by LeftForall
+          thenHave(∀(t2, in(t2, t1) <=> (in(t2, originalSet) /\ separationCondition)) |- ∀(t2, in(t2, t1) <=> (separationCondition))) by RightForall
+          thenHave(∀(t2, in(t2, t1) <=> (in(t2, originalSet) /\ separationCondition)) |- ∃(t1, ∀(t2, in(t2, t1) <=> (separationCondition)))) by RightExists
+          thenHave(thesis) by LeftExists
+        }
+
+        val cutL = have(
+          ∃!(t1, comprehension) |- ∃(t1, comprehension)
+        ) by Restate.from(Quantifiers.existsOneImpliesExists of (P -> lambda(t1, comprehension)))
+        val cutR = have(∃(t1, targetDef) |- ∃!(t1, targetDef)) by Restate.from(
+          SetTheory.uniqueByExtension of (schemPred -> lambda(t2, separationCondition))
+        )
+
+        val trL = have(∃!(t1, comprehension) |- ∃(t1, targetDef)) by Cut(cutL, transform)
+        val trR = have(∃!(t1, comprehension) |- ∃!(t1, targetDef)) by Cut(trL, cutR)
+        have(∃!(t1, targetDef)) by Cut.withParameters(∃!(t1, comprehension))(uniq, trR)
+      }
+
+      // safely check, unwrap, and return the proof judgement
+      unwrapTactic(sp)("Subproof for unique comprehension failed.")
+    }
+  }
 }

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

@@ -2,7 +2,7 @@ package lisa.maths.settheory
 
 import lisa.SetTheoryLibrary
 import lisa.SetTheoryLibrary.*
-import lisa.maths.settheory.SetTheory.functional
+import lisa.maths.settheory.functions.functional
 import lisa.prooflib.BasicStepTactic.RightForall
 import lisa.prooflib.BasicStepTactic.TacticSubproof
 import lisa.prooflib.SimpleDeducedSteps.*