Introduce local definitions and comprehensions (#199)

This PR introduces methods witness, t.replace, t.collect, t.map and t.filter. Update of the manual, describing how those work, along with some corrections to the statement of axioms ot match LISA's presentation. Include test cases using each, and proved some required theorems. Fix an error in the reconstruction of OL-normalized formulas used in some tactics.

CHANGES.md

@@ -1,5 +1,8 @@
 # Change List
 
+## 2023-12-19
+Introduction of local definitions, with methods `witness`, `t.replace`, `t.collect`, `t.map` and `t.filter`. Update of the manual, describing how those work, along with some corrections to the statement of axioms ot match LISA's presentation. Include test cases using each, and proved some required theorems. Fix an error in the reconstruction of OL-normalized formulas used in some tactics.
+
 ## 2023-12-06
 Re-added discovery of formulas which could not be substituted for error reporting to `Substitution.ApplyRules`
 

Reference Manual/lisa.tex

@@ -23,7 +23,7 @@
 
         \vspace{1.5cm}
 
-        \textbf{\large Version 0.2.1}
+        %\textbf{\large Version 0.2.1}
 
         \textbf{\large \today}
 

Reference Manual/macro.tex

@@ -33,10 +33,13 @@
 
 \newtheorem{axz}{}
 \renewcommand\theaxz{Z\arabic{axz}}
+\newcommand*{\axzautorefname}{Axiom}
 \newtheorem{axzf}{}
 \renewcommand\theaxzf{ZF\arabic{axzf}}
+\newcommand*{\axzfautorefname}{Axiom}
 \newtheorem{axtg}{}
 \renewcommand\theaxtg{TG\arabic{axtg}}
+\newcommand*{\axtgautorefname}{Axiom}
 
 \theoremstyle{definition}
 \newtheorem{definition}{Definition}

Reference Manual/prooflib.tex

@@ -21,7 +21,6 @@ \chapter{Developping Mathematics with Prooflib}
     have(thesis) by Tautology.from(step1, step2)
   } 
 
-
   val emptySetIsASubset = Theorem(
     ∅ ⊆ x
   ) {
@@ -40,7 +39,59 @@ \chapter{Developping Mathematics with Prooflib}
 
 In this chapter, we will describe how each of these construct is made possible and how they translate to statements in the Kernel.
 
-\section*{WIP}
+\section{Richer FOL}
+
+
+
+\section{Proof Builders}
+
+\subsection{Proofs}
+
+\subsection{Facts}
+
+\subsection{Instantiations}
+
+\subsection{Local Definitions}
+\label{sec:localDefinitions}
+The following line of reasonning is standard in mathematical proofs. Suppose we have already proven the following fact:
+$$\exists x. P(x)$$
+And want to prove the property $\phi$.
+A proof of $\phi$ using the previous theorem would naturally be obtained the following way:
+\begin{quotation}
+  Since we have proven $\exists x. P(x)$, let $c$ be an arbitrary value such that $P(c)$ holds.
+  Hence we prove $\phi$, using the fact that $P(c)$: (...).
+\end{quotation}
+However, introducing a definition locally corresponding to a statement of the form
+$$\exists x. P(x)$$
+is not a built-in feature of first order logic.  This can however be simulated by introducing a fresh variable symbol $c$, that must stay fresh in the rest of the proof, and the assumption $P(c)$. The rest of the proof is then carried out under this assumption. When the proof is finished, the end statement should not contain $c$ free as it is a \textit{local} definition, and the assumption can be eliminated using the LeftExists and Cut rules. Such a $c$ is called a \textit{witness}. 
+Formally, the proof in (...) is a proof of $P(c) \vdash \phi$. This can be transformed into a proof of $\phi$ by mean of the following steps:
+\begin{center}
+  \AxiomC{$P(c) \vdash \phi$}
+  \UnaryInfC{$\exists x. P(x) \vdash  \phi$}
+  \RightLabel{\text { LeftExists}}
+  \AxiomC{$\exists x. P(x)$}
+  \RightLabel{\text { Cut}}
+  \BinaryInfC{$\phi$}
+\end{center}
+Not that for this step to be correct, $c$ must not be free in $\phi$. This correspond to the fact that $c$ is an arbitrary free symbol.
+
+This simulation is provided by LISA through the \lstinline|witness|{} method. It takes as argument a fact showing $\exists x. P(x)$, and introduce a new symbol with the desired property. For an example, see figure \ref{fig:localDefinitionExample}.
+
+\begin{figure}
+  \begin{lstlisting}[language=lisa, frame=single]
+    val existentialAxiom = Axiom(exists(x, in(x, emptySet)))
+    val falso = Theorem(⊥) {
+      val c = witness(existentialAxiom)
+      have(⊥) by Tautology.from(
+            c.definition, emptySetAxiom of (x:= c))
+    }
+  \end{lstlisting}
+  \caption{An example use of local definitions in LISA}
+  \label{fig:localDefinitionExample}
+  \end{figure}
+
+
+\section{DSL}
 
 %It is important to note that when multiple such files are developed, they all use the same underlying \lstinline|RunningTheory|{}. This makes it possible to use results proved previously by means of a simple \lstinline|import|{} statement as one would import a regular object. Similarly, one should also import as usual automation and tactics developed alongside. It is expected in the medium term that \lstinline|lisa.Main|{} will come with basic automation.
 %All imported theory objects will be run through as well, but only the result of the selected one will be printed.

Reference Manual/theory.tex

@@ -41,35 +41,84 @@ \chapter{Library Development: Set Theory}
     $\forall x. x \notin \emptyset$
   \end{axz}
   \begin{axz}[extensionality]\label{axz:extensionality}
-    $\forall x, y. (\forall z. z \in x \iff z \in y) \iff (x = y)$
+    $(\forall z. z \in x \iff z \in y) \iff (x = y)$
   \end{axz}
   \begin{axz}[subset]\label{axz:subset}
-    $\forall x, y. x\subset y \iff \forall z. z \in x \iff z \in y$
+    $x\subset y \iff \forall z. z \in x \implies z \in y$
   \end{axz}
   \begin{axz}[pair]\label{axz:pair}
-    $\forall x, y, z. (z \in (x, y)) \iff ((x \in y) \lor (y \in z))$
+    $(z \in \lbrace x, y\rbrace) \iff ((x = z) \lor (y = z))$
   \end{axz}
   \begin{axz}[union]\label{axz:union}
-    $\forall x, z. (x \in \operatorname{U}(z)) \iff (\exists y. (x \in y) \land (y \in z))$
+    $(z \in \operatorname{U}(x)) \iff (\exists y. (y \in x) \land (z \in y))$
   \end{axz}
   \begin{axz}[power]\label{axz:power}
-    $\forall x, y. (x \in \operatorname{\mathcal{P}}(y)) \iff (x \subset y)$
+    $(x \in \operatorname{\mathcal{P}}(y)) \iff (x \subset y)$
   \end{axz}
   \begin{axz}[foundation]\label{axz:foundation}
     $\forall x. (x \neq \emptyset) \implies (\exists y. (y \in x) \land (\forall z. z \in x))$
   \end{axz}
   \begin{axz}[comprehension schema]\label{axz:comprehension}
-    $\forall z, \vec{v}. \exists y. \forall x. (x \in y) \iff ((x \in z) \land \phi(x, z, \vec{v}))$
+    $\exists y. \forall x. x \in y \iff (x \in z \land \phi(x))$
+  \end{axz}
+  \begin{axz}[infinity]\label{axz:infinity}
+    $\exists x. \emptyset \in x \land (\forall y. y \in x \implies \operatorname{U}(\lbrace y, \lbrace y, y \rbrace \rbrace) \in x)$
   \end{axz}
   \caption{Axioms for Zermelo set theory.}
   \label{fig:axiomsz}
 \end{figure}
 
 \begin{figure}
   \begin{axzf}[replacement schema]\label{axzf:replacement}
-    $$\forall a. (\forall x. (x \in a) \implies !\exists y. \phi(a, \vec{v}, x, y)) \implies $$
-    $$(\exists b. \forall x. (x \in a) \implies (\exists y. (y \in b) \land \phi(a, \vec{v}, x, y)))$$
+    $$\forall x. (x \in a) \implies \forall y, z.  (\psi(x, y) \land \psi(x, y)) \implies y = z \implies $$
+    $$(\exists b. \forall y. (y \in B) \implies (\exists x. (x \in a) \land \psi(x, y)))$$
   \end{axzf}
   \caption{Axioms for Zermelo-Fraenkel set theory.}
   \label{fig:axiomszf}
 \end{figure}
+
+
+\section{Using Comprehension and Replacement}
+
+In traditional mathematics and set theory, it is standard to use \textit{set builder notations}, to denote sets built from comprehension and replacement, for example
+
+$$\lbrace -x \mid x\in \mathbb N \land \operatorname{isEven}(x) \rbrace$$
+This also naturally corresponds to \textit{comprehensions} over collections in programming languages, as in \autoref{tab:comprehensionsProgramming}.
+\begin{table}[h]
+  \begin{tabular}{l|l}
+    \textbf{Language} & \textbf{Comprehension} \\ \hline
+    Python            & \lstinline$[-x for x in range(10) if x % 2 == 0]$ \\
+    Haskell           & \lstinline$[-x | x <- [0..9], even x]$ \\
+    Scala             & \lstinline$for (x <- 0 to 9 if x % 2 == 0) yield -x$ \\
+  \end{tabular}
+  \caption{Comprehensions in various programming languages}
+  \label{tab:comprehensionsProgramming}
+\end{table}
+Those are typicaly syntactic sugar for a more verbose expression. For example in scala, \lstinline|(0 to 9).filter(x => x % 2 == 0).map(x => -x)|. However this kind of expressions is not possible in first order logic: We can't built in any way a term that contains formulas as subexpressions, as in \lstinline|filter|. So if we want to use such constructions, we need to simulate it as we did for local definitions in \autoref{sec:localDefinitions}.
+
+It turns out that the comprehension schema is a consequence of the replacement schema when the value plugged for $\psi(x, y)$ is $\phi(x) \land y = x$, i.e. when $\psi$ denotes a restriction of the diagonal relation. Hence, what follows is built only from replacement.
+Note that the replacement axiom \autoref{axzf:replacement} is conditional of the schematic symbol $\psi$ being a functional relation. It is more convenient to move this condition inside the axiom, to obtain a non-conditional equivalence. This is the approach adopted in Isabelle/ZF \cite{noelExperimentingIsabelleZF1993}. We instead can prove and use
+$$ \exists B, \forall y. y \in B \iff (\exists x. x \in A \land P(y, e) \land ∀ z. \psi(x, z) \implies z = y) $$
+Which maps elements of $A$ through the functional component of $\psi$ only. If $\psi$ is functional, those are equivalent.
+
+LISA allows to write, for an arbitrary term \lstinline|t| and lambda expression \lstinline|P: (Term, Term) \mapsto Formula|,
+\begin{center}
+  \lstinline|val c = t.replace(P)|
+\end{center}
+One can then use \lstinline|c.elim(e)| to obtain the fact 
+$e \in B \iff (\exists x. x \in A \land P(x, e) \land \forall z. \psi(x, z) \implies z = y)$. As in the case of local definitions, this statement will automatically be eliminated from the context at the end of the proof.
+
+Moreover, we most often want to map a set by a known function. In those case, LISA provides refined versions \lstinline|t.filter|, \lstinline|t.map| and \lstinline|t.collect|, which are detailed in table \ref{tab:comprehensions}. In particular, these versions already prove the functionality requirement of replacement.
+\begin{table}[h]
+  \begin{tabular}{l|l}
+    \textbf{\lstinline|val c = |} & \textbf{\lstinline|c.elim(e)|} \\ \hline
+    \lstinline|t.replace(P)| & $e \in c \iff (\exists x. x \in t \land P(x, e) \land ∀ z. P(x, z) \implies z = e)$ \\
+    \lstinline|t.collect(F, M)| & $e \in c \iff (\exists x. x \in t \land F(x) \land M(x) = e)$ \\
+    \lstinline|t.map(M)| & $e \in c \iff (\exists x. x \in t \land M(x) = e)$ \\
+    \lstinline|t.filter(F)| & $e \in c \iff e \in t \land F(e)$ \\   
+  \end{tabular}
+  \caption{Comprehensions in LISA}
+  \label{tab:comprehensions}
+\end{table}
+
+Note that each of those expressions is represented as a variable symbol in the kernel proof, and the definitions are only valid inside the current proof. They should not appear in theorem statements (in which case they should be properly introduced as defined constants).

lisa-kernel/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala

@@ -313,7 +313,7 @@ private[fol] trait EquivalenceChecker extends FormulaDefinitions {
 
     t match {
       case Term(label: VariableLabel, _) =>
-        if (subst.contains(i - label.id.no)) VariableTerm(VariableLabel(subst(i - label.id.no)))
+        if ((label.id.name == "x") && subst.contains(i - label.id.no)) VariableTerm(VariableLabel(subst(i - label.id.no)))
         else if (label.id.name.head == '$') VariableTerm(VariableLabel(Identifier(label.id.name.tail, label.id.no)))
         else {
           throw new Exception("This case should be unreachable, error")

lisa-sets/src/main/scala/lisa/SetTheoryLibrary.scala

@@ -76,10 +76,10 @@ object SetTheoryLibrary extends lisa.prooflib.Library {
   private val x = variable
   private val y = variable
   private val z = variable
-  final val φ = predicate[2]
+  final val φ = predicate[1]
   private val A = variable
   private val B = variable
-  private val P = predicate[3]
+  private val P = predicate[2]
 
   ////////////
   // Axioms //
@@ -119,7 +119,7 @@ object SetTheoryLibrary extends lisa.prooflib.Library {
    * This schema represents an infinite collection of axioms, one for each
    * formula `ϕ(x, z)`.
    */
-  final val comprehensionSchema: AXIOM = Axiom(exists(y, forall(x, in(x, y) <=> (in(x, z) /\ φ(x, z)))))
+  final val comprehensionSchema: AXIOM = Axiom(exists(y, forall(x, in(x, y) <=> (in(x, z) /\ φ(x)))))
 
   /**
    * Empty Set Axiom --- From the Comprehension Schema follows the existence of
@@ -201,8 +201,8 @@ object SetTheoryLibrary extends lisa.prooflib.Library {
    * 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))))
+    forall(x, in(x, A) ==> ∀(y, ∀(z, (P(x, y) /\ P(x, z)) ==> (y === z)))) ==>
+      exists(B, forall(y, in(y, B) <=> exists(x, in(x, A) /\ P(x, y))))
   )
 
   final val tarskiAxiom: AXIOM = Axiom(

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

@@ -143,7 +143,7 @@ object CommonTactics {
         case Some(value: lib.FunctionDefinition[?]) => value
         case _ => return proof.InvalidProofTactic("Could not get definition of function.")
       }
-      val method: (F.ConstantFunctionLabel[?], proof.Fact) => Seq[F.Term] => F.Sequent => proof.ProofTacticJudgement = 
+      val method: (F.ConstantFunctionLabel[?], proof.Fact) => Seq[F.Term] => F.Sequent => proof.ProofTacticJudgement =
         expr.f.substituteUnsafe(expr.vars.zip(xs).toMap) match {
           case F.AppliedConnector(
                 F.And,

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

@@ -2,7 +2,7 @@ package lisa.automation.settheory
 
 import lisa.SetTheoryLibrary.{_, given}
 import lisa.fol.FOL.{_, given}
-import lisa.kernel.proof.SequentCalculus as SC
+import lisa.kernel.proof.SequentCalculus as SCunique
 import lisa.maths.settheory.SetTheory
 import lisa.prooflib.BasicStepTactic.*
 import lisa.prooflib.Library
@@ -45,18 +45,18 @@ object SetTheoryTactics {
         line: sourcecode.Line,
         file: sourcecode.File,
         om: OutputManager
-    )(originalSet: Term, separationPredicate: LambdaTF[2])( // TODO dotty forgets that Term <:< LisaObject[Term]
+    )(originalSet: Term, separationPredicate: LambdaTF[1])( // TODO dotty forgets that Term <:< LisaObject[Term]
         bot: Sequent
     ): proof.ProofTacticJudgement = {
-      require(separationPredicate.bounds.length == 2) // separationPredicate takes two args
+      require(separationPredicate.bounds.length == 1) // separationPredicate takes two args
       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 prop = (in(t2, originalSet) /\ separationPredicate(t2, originalSet)) // TODO (Seq(t2, originalSet)
+      val prop = (in(t2, originalSet) /\ separationPredicate(t2)) // TODO (Seq(t2, originalSet)
       def fprop(z: Term) = forall(t2, in(t2, z) <=> prop)
 
       /**