Small corrections to Lisa manual

refman/kernel.tex

@@ -614,7 +614,7 @@ \subsection{Proofs}
 \end{figure}
 
 In the Lisa kernel, proof steps are organised linearly, in a list, to form actual proofs. Each proof step refers to its premises using numbers, which indicate the place of the premise in the proof.
-a proof step can also be refered to by multiple subsequent proof steps, so that proofs are actually directed acyclic graphs (DAG) rather than trees. For the proof to be the linearization of a rooted DAG, the proof steps must only refer to numbers smaller than their own in the proof. Indeed, using topological sorting, it is always possible to order the nodes of a directed acyclic graph such that for any node, its predecessors appear earlier in the list.
+a proof step can also be referred to by multiple subsequent proof steps, so that proofs are actually directed acyclic graphs (DAG) rather than trees. For the proof to be the linearization of a rooted DAG, the proof steps must only refer to numbers smaller than their own in the proof. Indeed, using topological sorting, it is always possible to order the nodes of a directed acyclic graph such that for any node, its predecessors appear earlier in the list.
 \autoref{fig:exampleProofLinear} shows the proof of Pierce's Law as linearized in Lisa's kernel.
 %
 \begin{figure}[ht]
@@ -682,7 +682,7 @@ \subsection{Proofs}
   \centering
   \begin{lstlisting}[language=scala, showspaces=false]
 val PierceLawProof = SCProof(IndexedSeq(
-    Hypothesis(φ |- φ,   φ),
+    Hypothesis( φ |- φ,   φ),
     Weakening( φ |- ( φ, ψ ), 0),
     RightImplies(() |- ( φ, φ ==> ψ ), 1,   φ, ψ)
     LeftImplies(( φ ==> ψ ) ==> φ |- φ, 2, 0,   φ ==> ψ, φ),
@@ -811,7 +811,7 @@ \subsection{Definitions}
   Theorem(
     name: String,
     proposition: Sequent
-    )
+  )
 
           \end{lstlisting}
           \\ %\hline
@@ -821,7 +821,7 @@ \subsection{Definitions}
   Axiom(
     name: String,
     ax: Formula
-    )
+  )
 
           \end{lstlisting}
           \\ %\hline
@@ -831,7 +831,7 @@ \subsection{Definitions}
   PredicateDefinition(
     label: ConstantAtomicLabel,
     expression: LambdaTermFormula
-    )
+  )
 
           \end{lstlisting}
           \\ %\hline
@@ -842,7 +842,7 @@ \subsection{Definitions}
     label: ConstantFunctionLabel,
     out: VariableLabel,
     expression: LambdaTermFormula
-    )
+  )
 
           \end{lstlisting}
           \\ %\hline
@@ -867,7 +867,7 @@ \subsection{Definitions}
     statement: Sequent,
     proof: SCProof,
     justs: Seq[Justification]
-    )
+  )
           \end{lstlisting}
           \\ %\hline
 
@@ -876,7 +876,7 @@ \subsection{Definitions}
   addAxiom(
     name: String,
     f: Formula
-    )
+  )
           \end{lstlisting}
           \\ %\hline
 
@@ -885,7 +885,7 @@ \subsection{Definitions}
   makePredicateDefinition(
     label: ConstantAtomicLabel,
     expression: LambdaTermFormula
-    )
+  )
           \end{lstlisting}
           \\ %\hline
 
@@ -897,7 +897,7 @@ \subsection{Definitions}
     label: ConstantFunctionLabel,
     out: VariableLabel,
     expression: LambdaTermFormula
-    )
+  )
           \end{lstlisting}
           \\ %\hline
         \end{tabular}
@@ -1106,7 +1106,7 @@ \subsection{How to write helpers}
   given Conversion[TermLabel, Term] = (t: Term) => Term(t, Seq())
 \end{lstlisting}
 %
-Now, every time a \lstinline|TermLabel| is writen in a place where a \lstinline|Term| is expected, it will be converted implicitly.
+Now, every time a \lstinline|TermLabel| is written in a place where a \lstinline|Term| is expected, it will be converted implicitly.
 
 To learn more about Scala 3 and its capabilities, see its documentation at {\footnotesize\url{https://docs.scala-lang.org/scala3/book/introduction.html}}. 
 

refman/prooflib.tex

@@ -53,7 +53,7 @@ \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:
+The following line of reasoning 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:
@@ -80,10 +80,10 @@ \subsection{Local Definitions}
 \begin{figure}
   \begin{lstlisting}[language=lisa, frame=single]
     val existentialAxiom = Axiom(exists(x, in(x, emptySet)))
-    val falso = Theorem(⊥) {
+    val falso = Theorem( ⊥ ) {
       val c = witness(existentialAxiom)
-      have(⊥) by Tautology.from(
-            c.definition, emptySetAxiom of (x:= c))
+      have( ⊥ ) by Tautology.from(
+            c.definition, emptySetAxiom of (x := c))
     }
   \end{lstlisting}
   \caption{An example use of local definitions in Lisa}
@@ -104,7 +104,7 @@ \subsection{Instantiations with ``of''}
 \end{lstlisting}
 \lstinline|x := d| is called a substitution pair, and is equivalent to the tuple \lstinline|(x, d)|. Arbitrarily many substitution pairs can be given as argument to \lstinline|of|, and the instantiations are done simultaneously. \lstinline|ax of (x := c)| is called an \lstinline|InstantiatedFact|, whose statement is $P(c)$, and which can be used exactly like theorems, axioms and intermediate steps in the proof. Internally, Lisa produces a proof step corresponding to the instantiation using the \texttt{Inst} rule.
 
-The \lstinline|of| keyword can also instantiate universaly quantified formulas of a fact, when it contains a single formula. For example, the following code is valid:
+The \lstinline|of| keyword can also instantiate universally quantified formulas of a fact, when it contains a single formula. For example, the following code is valid:
 \begin{lstlisting}[language=lisa, frame=single]
   val ax = Axiom(∀(x, P(x)))
   val thm = Theorem(P(c) /\ P(d)) {
@@ -113,7 +113,7 @@ \subsection{Instantiations with ``of''}
 \end{lstlisting}
 Here, \lstinline|ax of c| is a fact whose proven statement is again $P(c)$. It is possible to instantiate multiple $\forall$ quantifiers at once. For example if \lstinline|ax| is an axiom of the form $\forall x, \forall y, P(x, y)$, then \lstinline|ax of (c, d)| is a fact whose proven statement is $P(c, d)$. It is also possible to combine instantiation of free symbols and quantified variables. For example, if \lstinline|ax| is an axiom of the form $\forall x, \forall y, P(x, y)$, then \lstinline|ax of (c, y, P := ===)| is a fact whose proven statement is $(c = y)$.
 
-Formally, the \lstinline|of| keyword takes as argument arbitrarily many terms and substitution pairs. If there is at least on term given as argument, the base fact must have a single universaly quantified formula on the right (an arbitrarily many formulas on the left). The number of given terms must be at most the number of leading universal quantifiers. Moreover, a substitution cannot instantiate any locked symbol (i.e. a symbol part of an assumption or definition). The ordering of substitution pairs does not matter, but the ordering of terms does. The resulting fact is obtained by firstreplacing the free symbols in the formula by the given substitution pairs, and then instantiating the quantified variables in the formula by the given terms
+Formally, the \lstinline|of| keyword takes as argument arbitrarily many terms and substitution pairs. If there is at least one term given as argument, the base fact must have a single universally quantified formula on the right (an arbitrarily many formulas on the left). The number of given terms must be at most the number of leading universal quantifiers. Moreover, a substitution cannot instantiate any locked symbol (i.e. a symbol part of an assumption or definition). The ordering of substitution pairs does not matter, but the ordering of terms does. The resulting fact is obtained by first replacing the free symbols in the formula by the given substitution pairs, and then instantiating the quantified variables in the formula by the given terms
 
 In general, for the following proof
 \begin{lstlisting}[language=lisa, frame=single]

refman/quickguide.tex

@@ -64,8 +64,8 @@ \subsection*{A Note on Special Characters}
   \begin{tabular}{c|c|c}
     Rendering         & Input            & Name     \\ \hline
     \lstinline| === | & ===              & equality \\ \hline
-    \lstinline| \/  | & \textbackslash / & and      \\ \hline
-    \lstinline| /\  | & /\textbackslash  & or       \\ \hline
+    \lstinline| \/  | & \textbackslash / & or       \\ \hline
+    \lstinline| /\  | & /\textbackslash  & and      \\ \hline
     \lstinline| ==> | & ==>              & implies  \\ \hline
     \lstinline+ |-  + &  |-              & vdash    \\ \hline
     \lstinline| ∀   | & U+2200           & forall   \\ \hline
@@ -225,7 +225,7 @@ \subsubsection*{Restate}
 \end{lstlisting}
 tries to justify \lstinline|statement| by showing it is equivalent to the previously proven \lstinline|premise|.
 
-\subsubsection*{Tautology}
+\subsubsection*{Tautology}\label{tact:Tautology}
 \lstinline|Tautology| is a propositional solver based upon restate, but complete. It is able to prove every formula inference that holds in classical propositional logic. However, in the worst case its complexity can be exponential in the size of the formula. Usage:
 
 \begin{lstlisting}[language=lisa]

refman/theory.tex

@@ -15,7 +15,7 @@ \chapter{Library Development: Set Theory}
 In a more typical mathematical introduction to Set Theory, ZF would naturally only contain the set membership symbol $\in$. Axioms defining the other symbols would then only express the existence of functions or predicates with those properties, from which we could get the same symbols using extensions by definitions.
 
 In a very traditional sense, an axiomatization is any possibly infinite semi-recursive set of axioms. Hence, in its full generality, Axioms should be any function producing possibly infinitely many formulas.
-This is however not a convenient definition. In practice, all infinite axiomatizations are schematic, meaning that they are expressable using schematic variables. Axioms \ref{axz:comprehension} (comprehension schema) and \ref{axzf:replacement} (replacement schema) are such examples of axiom schema, and motivates the use of schematic variables in Lisa.
+This is however not a convenient definition. In practice, all infinite axiomatizations are schematic, meaning that they are expressible using schematic variables. Axioms \ref{axz:comprehension} (comprehension schema) and \ref{axzf:replacement} (replacement schema) are such examples of axiom schema, and motivates the use of schematic variables in Lisa.
 
 
 
@@ -24,9 +24,9 @@ \chapter{Library Development: Set Theory}
     \begin{tabular}{l|c|l}
       {}                         & Math symbol       & Lisa Kernel             \\ \hline
       Set Membership predicate   & $\in$             & \lstinline$in(s,t)$     \\
-      Subset predicate           & $\subset$         & \lstinline$subset(s,t)$ \\
+      Subset predicate           & $\subseteq$       & \lstinline$subset(s,t)$ \\
       Empty Set constant         & $\emptyset$       & \lstinline$emptyset()$  \\
-      Unordered Pair constant    & $(\cdot, \cdot )$ & \lstinline$pair(s,t)$   \\
+      Ordered Pair constant      & $(\cdot, \cdot )$ & \lstinline$pair(s,t)$   \\
       Power Set function         & $\mathcal P$      & \lstinline$powerSet(s)$ \\
       Set Union/Flatten function & $\bigcup$         & \lstinline$union(x)$    \\
     \end{tabular}
@@ -94,7 +94,7 @@ \section{Using Comprehension and Replacement}
   \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}.
+Those are typically 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