diff --git a/.gitignore b/.gitignore
index a784965e49d75566f0228551d1c380369cc481ca..b05d0969af134147e63d239ea3e88689adf52071 100644
--- a/.gitignore
+++ b/.gitignore
@@ -18,4 +18,7 @@ silex/*
scallion/*
# caching of theorems
-cache
\ No newline at end of file
+cache
+
+# emacs backup files
+*~
diff --git a/Reference Manual/lisa.pdf b/Reference Manual/lisa.pdf
deleted file mode 100644
index e97f7213031a3c0d2316b802cf7e2e5ec394c855..0000000000000000000000000000000000000000
Binary files a/Reference Manual/lisa.pdf and /dev/null differ
diff --git a/Reference Manual/lisa.tex b/Reference Manual/lisa.tex
deleted file mode 100644
index e08f0c4be628176d87379e76e1114159cc02ab39..0000000000000000000000000000000000000000
--- a/Reference Manual/lisa.tex
+++ /dev/null
@@ -1,67 +0,0 @@
-% !TEX program = xelatex
-\documentclass[11pt,a4paper]{book}
-
-\input{macro}
-\input{shortcuts}
-
-\title{LISA Reference Manual (WIP)}
-\author{Simon Guilloud\\Laboratory for Automated Reasoning and Analysis, EPFL}
-\date{}
-
-\begin{document}
-
-\newfontfamily\titlefont{Arial}
-
-\begin{titlepage}
-\titlefont
-%\fontfamily{\sfdefault}\selectfont
-
- \begin{center}
- \vspace*{1cm}
-
- \textbf{\Huge LISA Reference Manual}
-
- \vspace{1.5cm}
-
- %\textbf{\large Version 0.2.1}
-
- \textbf{\large \today}
-
- \vspace{1.5cm}
-
- {\Large Laboratory for Automated Reasoning and Analysis\\ EPFL, Switzerland}
-
- \vspace{1.5cm}
-
- \date{}
-
- \end{center}
- \vspace*{10em}
- \begin{flushright}\huge
- \begin{tabular}{l}
- Contributors: \hspace*{2em} \\[1em]
- Simon Guilloud\\
- Sankalp Gambhir
- \end{tabular}
- \end{flushright}
-
- \end{titlepage}
-\chapter*{Introduction}
-
-This document aims to give a complete documentation on LISA. Tentatively, every chapter and section will explain a part or concept of LISA, and explains both its implementation and its theoretical foundations.
-
-\tableofcontents
-
-\input{quickguide.tex}
-
-\input{kernel.tex}
-
-\input{prooflib.tex}
-
-\input{theory.tex}
-
-\input{theorytopics.tex}
-
-\bibliographystyle{plain}
-\bibliography{sguilloud.bib}
-\end{document}
\ No newline at end of file
diff --git a/refman/.gitignore b/refman/.gitignore
new file mode 100644
index 0000000000000000000000000000000000000000..829b57d1f46154dcfedc0254301afeacbb749767
--- /dev/null
+++ b/refman/.gitignore
@@ -0,0 +1,8 @@
+lisa.aux
+lisa.bbl
+lisa.blg
+lisa.fdb_latexmk
+lisa.fls
+lisa.log
+lisa.out
+lisa.toc
diff --git a/Reference Manual/.latexmkrc b/refman/.latexmkrc
similarity index 100%
rename from Reference Manual/.latexmkrc
rename to refman/.latexmkrc
diff --git a/refman/Makefile b/refman/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..8467b6dceeb815898b9073436737f1383403e4e2
--- /dev/null
+++ b/refman/Makefile
@@ -0,0 +1,11 @@
+# Makefile for compiling lisa.tex using latexmk
+
+# Default target
+all: lisa.pdf
+
+lisa.pdf: lisa.tex kernel.tex lisa.tex macro.tex prooflib.tex quickguide.tex shortcuts.tex theory.tex theorytopics.tex
+ latexmk lisa.tex
+
+# Clean target
+clean:
+ latexmk -c lisa.tex
diff --git a/refman/alttitlepage.tex b/refman/alttitlepage.tex
new file mode 100644
index 0000000000000000000000000000000000000000..44008337b3eeadcbc83e86953659d38fba0372cf
--- /dev/null
+++ b/refman/alttitlepage.tex
@@ -0,0 +1,39 @@
+%\newfontfamily\titlefont{Arial}
+\begin{titlepage}
+\sf
+%\fontfamily{\sfdefault}\selectfont
+
+ \begin{center}
+ \vspace*{1cm}
+
+ \textbf{\Huge \ourtitle}
+
+ \vspace{1.5cm}
+
+ {\Large \ournames}
+
+ \vspace{1.5cm}
+
+ {\Large Laboratory for Automated Reasoning and Analysis \\[1ex] EPFL, Switzerland}
+
+ \end{center}
+
+ \vfill
+
+ \begin{center}
+ \Large
+ \textbf{\large \today}
+ \end{center}
+
+ %% \begin{flushright}
+ %% \begin{minipage}{15em}
+ %% \Large
+ %% Contributors: \\[1ex]
+ %% \hspace*{3em} \begin{tabular}{l}
+ %% Simon Guilloud\\
+ %% Sankalp Gambhir
+ %% \end{tabular}
+ %% \end{minipage}
+ %% \end{flushright}
+
+ \end{titlepage}
diff --git a/Reference Manual/kernel.tex b/refman/kernel.tex
similarity index 93%
rename from Reference Manual/kernel.tex
rename to refman/kernel.tex
index 1f55e586aa5773ce472551fb945fe00982e5372c..5d5aeb1913f3785f25c0c32d901ceed471883fcf 100644
--- a/Reference Manual/kernel.tex
+++ b/refman/kernel.tex
@@ -1,17 +1,17 @@
%\part{Reference Manual}
-\chapter{LISA's trusted code: The Kernel}
+\chapter{Lisa's Trusted Kernel}
\label{chapt:kernel}
-LISA's kernel is the starting point of LISA, formalising the foundations of the whole theorem prover. It is the only trusted code base, meaning that if it is bug-free then no further erroneous code can violate the soundness property and prove invalid statements. Hence, the two main goals of the kernel are to be efficient and trustworthy.
+Lisa's kernel is the starting point of Lisa, formalising the foundations of the whole theorem prover. It is the only trusted code base, meaning that if it is bug-free then no further erroneous code can violate the soundness property and prove invalid statements. Hence, the two main goals of the kernel are to be efficient and trustworthy.
-LISA's foundations are based on very traditional (in the mathematical community) foundational theory of all mathematics: \textbf{First Order Logic}, expressed using \textbf{Sequent Calculus} (augmented with schematic symbols), with axioms of \textbf{Set Theory}.
-While the LISA library is built on top of Set Theory axioms, the kernel is actually theory-agnostic and is sound to use with any other set of axioms. Hence, we defer Set Theory to chapter~\ref{chapt:settheory}.
+Lisa's foundations are based on very traditional (in the mathematical community) foundational theory of all mathematics: \textbf{First Order Logic}, expressed using \textbf{Sequent Calculus} (augmented with schematic symbols), with axioms of \textbf{Set Theory}.
+While the Lisa library is built on top of Set Theory axioms, the kernel is actually theory-agnostic and is sound to use with any other set of axioms. Hence, we defer Set Theory to chapter~\ref{chapt:settheory}.
\section{First Order Logic}
\label{sec:FOL}
\subsection{Syntax}
\begin{definition}[Terms]
- In LISA, the set of terms $\mathcal{T}$ is defined by the following grammar:
+ In Lisa, the set of terms $\mathcal{T}$ is defined by the following grammar:
\begin{align}
\mathcal{T} := & ~\mathcal{L}_{Term}(\List[\mathcal{T}])~,
\end{align}
@@ -86,14 +86,14 @@ Schematic symbols on the other hand, are uninterpreted --- they can represent an
\mathcal{L}_{Binder} := \forall \mid \exists \mid \exists!
\end{align}
- Connectors and predicates, like terms, can exist in either constant or schematic forms. Note that connectors and predicates vary only in the type of arguments they take, so that connectors and predicates of arity 0 are essentially the same thing. Hence, LISA, does not permit connectors of arity 0 and suggests the use of predicates instead.
+ Connectors and predicates, like terms, can exist in either constant or schematic forms. Note that connectors and predicates vary only in the type of arguments they take, so that connectors and predicates of arity 0 are essentially the same thing. Hence, Lisa, does not permit connectors of arity 0 and suggests the use of predicates instead.
A contrario to schematic terms of arity 0, schematic predicates of arity 0 can't be bound, but they still play a special role sometimes, so we introduce a special notation for them
%
$$
\FormulaVar(X) \equiv \SchematicPredicateLabel(X, 0)~.
$$
%
- Moreover, in LISA, a contrario to constant predicates and term symbols, which can be freely created, there is only the following finite set of constant connector symbols in LISA:
+ Moreover, in Lisa, a contrario to constant predicates and term symbols, which can be freely created, there is only the following finite set of constant connector symbols in Lisa:
%
$$
\operatorname{Neg}(\neg, 1)\mid \operatorname{Implies}(\rightarrow, 2)\mid \operatorname{Iff}(\leftrightarrow, 2)\mid \operatorname{And}(\land, -1)\mid \operatorname{Or}(\lor, -1)~,
@@ -127,7 +127,7 @@ Schematic symbols on the other hand, are uninterpreted --- they can represent an
\leftrightarrow & := \ConstantConnectorLabel(``{\leftrightarrow}", 2) \\
c & := \SchematicConnectorLabel(``{c}", 3) \\
\end{align*}
- Note that in the case of $\ConstantConnectorLabel$, the list is exhaustive: $\neg, \land, \lor, \rightarrow$ and $\leftrightarrow$ are the only logical connectors accepted by LISA.
+ Note that in the case of $\ConstantConnectorLabel$, the list is exhaustive: $\neg, \land, \lor, \rightarrow$ and $\leftrightarrow$ are the only logical connectors accepted by Lisa.
The following are examples of Formulas:
\begin{gather*}
\True() := \True(\Nil)\\
@@ -210,7 +210,7 @@ Those expressions are a generalization of terms, and would be part of our logic
$$\lambda x y.~ t_{x,y}$$
Similarly to how variables can be substituted by terms, schematic terms labels of arity greater than 0 can be substituted by such lambda terms.
-% As the definition of such substitution is rather convoluted to describe, we prefer to show examples and redirect the reader to the source code of LISA for a technical definition. \footnote{Note that in lambda calculus, this would simply be iterated beta-reduction.}
+% As the definition of such substitution is rather convoluted to describe, we prefer to show examples and redirect the reader to the source code of Lisa for a technical definition. \footnote{Note that in lambda calculus, this would simply be iterated beta-reduction.}
The substitution is defined in a manner similar to that of variable substitution with the base case
%
\begin{equation*}
@@ -282,11 +282,11 @@ Note that in the last case, $X$ and $Y$ are $\FormulaVar$. Substitution of funct
\subsection{The Equivalence Checker}
\label{subsec:equivalencechecker}
-While proving theorems, trivial syntactical transformations such as $p\land q \equiv q\land p$ significantly increase the length of proofs, which is desirable neither to the user nor the machine. Moreover, the proof checker will very often have to check whether two formulas that appear in different sequents are the same. Hence, instead of using pure syntactical equality, LISA implements a powerful equivalence checker able to detect a class of equivalence-preserving logical transformations. For example, we would like the formulas $p\land q$ and $q\land p$ to be naturally treated as equivalent.
+While proving theorems, trivial syntactical transformations such as $p\land q \equiv q\land p$ significantly increase the length of proofs, which is desirable neither to the user nor the machine. Moreover, the proof checker will very often have to check whether two formulas that appear in different sequents are the same. Hence, instead of using pure syntactical equality, Lisa implements a powerful equivalence checker able to detect a class of equivalence-preserving logical transformations. For example, we would like the formulas $p\land q$ and $q\land p$ to be naturally treated as equivalent.
For soundness, the relation decided by the algorithm should be contained in the $\iff$ ``if and only if'' relation of first order logic. However, it is well known that this relationship is in general undecidable, and even the $\iff$ relation for propositional logic is coNP-complete. For practicality, we need a relation that is efficiently computable.
-The decision procedure implemented in LISA takes time quadratic in the size of the formula, which means that it is not significantly slower than syntactic equality.
+The decision procedure implemented in Lisa takes time quadratic in the size of the formula, which means that it is not significantly slower than syntactic equality.
It is based on an algorithm that decides the word problem for Ortholattices \cite{guilloudFormulaNormalizationsVerification2023}.
Ortholattices are a generalization of Boolean algebra where instead of the law of distributivity, the weaker absorption law (L9, \autoref{tab:ortholatticeLaws}) holds. In particular, every identity in the theory of ortholattices is also a theorem of propositional logic.
\begin{table}[bth]
@@ -321,7 +321,7 @@ We write $s\sim_\OL t$ if both $s\leq_\OL t$ and $s\geq_\OL t$ hold.
\end{theorem}
Moreover, the algorithm works with structure sharing with the same complexity, which is very relevant for example when $x \leftrightarrow y$ is expanded to $(x \land y) \lor (\neg x \land \neg y)$. It can produce a normal form in this case as well.
-LISA's Kernel contains an algorithm, called the $\FOLalg{}$ Equivalence Checker which further extends OL inequality algorithm to first order logic formulas. It first expresses the formula using de Bruijn indices, then desugars $\exists. \phi$ into $\neg \forall. \neg \phi$. It then extends the OL algorithm with the rules in \autoref{tab:Olextension}.
+Lisa's Kernel contains an algorithm, called the $\FOLalg{}$ Equivalence Checker which further extends OL inequality algorithm to first order logic formulas. It first expresses the formula using de Bruijn indices, then desugars $\exists. \phi$ into $\neg \forall. \neg \phi$. It then extends the OL algorithm with the rules in \autoref{tab:Olextension}.
\begin{table}[ht]
\centering
@@ -344,7 +344,7 @@ LISA's Kernel contains an algorithm, called the $\FOLalg{}$ Equivalence Checker
\end{table}
-In particular, the implementation in LISA also takes into account symmetry and reflexivity of equality as well as alpha-equivalence, by which we mean renaming of bound variables. It also expresses $\rightarrow$ and $\leftrightarrow$ in terms of $\lor$ and $\land$.
+In particular, the implementation in Lisa also takes into account symmetry and reflexivity of equality as well as alpha-equivalence, by which we mean renaming of bound variables. It also expresses $\rightarrow$ and $\leftrightarrow$ in terms of $\lor$ and $\land$.
A more detailed discussion of extension of ortholattices to first-order logic, proof of correctness and implementation details can be found in \cite{guilloudFormulaNormalizationsVerification2023} and \cite{guilloudLISAModernProof2023}.
@@ -354,7 +354,7 @@ A more detailed discussion of extension of ortholattices to first-order logic, p
\label{sec:proofs_lk}
\subsection{Sequent Calculus}
\label{subsec:lk}
-The deductive system used by LISA is an extended version of the classical Sequent Calculus.
+The deductive system used by Lisa is an extended version of the classical Sequent Calculus.
%
\begin{definition}
A \textbf{sequent} is a pair $(\Gamma, \Sigma)$ of (possibly empty) sets of formulas, noted:
@@ -378,7 +378,7 @@ The deductive system used by LISA is an extended version of the classical Sequen
\end{definition}
A sequent $\phi \vdash \psi$ is logically (but not conceptually) equivalent to a sequent $\vdash \phi \rightarrow \psi$. The distinction is similar to the distinction between meta-implication and inner implication in Isabelle \cite{paulsonIsabelleNext7001993}, for example. Typically, a theorem or a lemma should have its various assumptions on the left-hand side of the sequent and a single conclusion on the right. During proofs however, there may be multiple elements on the right side. \footnote{In a strict description of Sequent Calculus, this is in particular needed to have double negation elimination.}
-Sequents are manipulated in a proof using \emph{deduction rules}. A deduction rule, also called a proof step, has zero or more prerequisite sequents (which we call \emph{premises} of the rule) and one conclusion sequent. All the basic deduction rules used in LISA's kernel are shown in \autoref{fig:deduct_rules_1}.
+Sequents are manipulated in a proof using \emph{deduction rules}. A deduction rule, also called a proof step, has zero or more prerequisite sequents (which we call \emph{premises} of the rule) and one conclusion sequent. All the basic deduction rules used in Lisa's kernel are shown in \autoref{fig:deduct_rules_1} and \autoref{fig:deduct_rules_2}.
This includes first rules of propositional logic, then rules for quantifiers, then equality rules. Moreover, we include equal-for-equal and equivalent-for-equivalent substitutions. While those substitution rules are deduced steps, and hence could technically be omitted, simulating them can sometimes take a high number of steps, so they are included as base steps for efficiency.
Finally, the two rules Restate and Weakening leverage the $\FOLalg$ algorithm.
@@ -387,24 +387,20 @@ Finally, the two rules Restate and Weakening leverage the $\FOLalg$ algorithm.
\begin{figure}
- \scalebox{.8}{
+ \scalebox{.88}{
\begin{minipage}{\textwidth}
\begin{center}
\begin{tabular}{l l}
- \multicolumn{2}{c}{
- \AxiomC{}
- \RightLabel{\text { Hypothesis}}
- \UnaryInfC{$\Gamma, \phi \vdash \phi, \Delta$}
- \DisplayProof
- } \\[5ex]
-
- \multicolumn{2}{c}{
- \AxiomC{$\Gamma \vdash \phi, \Delta$}
- \AxiomC{$\Sigma, \phi \vdash \Pi$}
- \RightLabel{\text{ Cut}}
- \BinaryInfC{$\Gamma, \Sigma \vdash \Delta, \Pi$}
- \DisplayProof
- } \\[5ex]
+ \AxiomC{}
+ \RightLabel{\text { Hypothesis}}
+ \UnaryInfC{$\Gamma, \phi \vdash \phi, \Delta$}
+ \DisplayProof &
+ \AxiomC{$\Gamma \vdash \phi, \Delta$}
+ \AxiomC{$\Sigma, \phi \vdash \Pi$}
+ \RightLabel{\text{ Cut}}
+ \BinaryInfC{$\Gamma, \Sigma \vdash \Delta, \Pi$}
+ \DisplayProof
+ \\[5ex]
\AxiomC{$\Gamma, \phi, \psi \vdash \Delta$}
\RightLabel{\text { LeftAnd}}
@@ -478,16 +474,32 @@ Finally, the two rules Restate and Weakening leverage the $\FOLalg$ algorithm.
\RightLabel{\text { RightExists}}
\UnaryInfC{$\Gamma \vdash \exists \schem{x}. \phi, \Delta$}
\DisplayProof
- \\[5ex]
+ \end{tabular}
+ \end{center}
+ \end{minipage}}
+ \caption{Deduction rules allowed by Lisa's kernel (Part 1). These are typical rules for a sequent calculus for FOL. Different occurrences of the same symbols need not represent equal elements, but only elements with the same \FOLalg{} normal form.}
+ \label{fig:deduct_rules_1}
+\end{figure}
- \AxiomC{$\Gamma, \exists y \forall x. (x=y) \leftrightarrow \phi \vdash \Delta$}
- \RightLabel{\text { LeftExistsOne}}
- \UnaryInfC{$\Gamma, \exists ! x. \phi \vdash \Delta$}
- \DisplayProof &
- \AxiomC{$\Gamma \vdash \exists y \forall x. (x=y) \leftrightarrow \phi , \Delta$}
- \RightLabel{\text { RightExistsOne}}
- \UnaryInfC{$\Gamma \vdash \exists ! x. \phi, \Delta$}
- \DisplayProof
+\begin{figure}
+ \scalebox{.9}{
+ \begin{minipage}{\textwidth}
+ \begin{center}
+ \begin{tabular}{l l}
+ \multicolumn{2}{c}{
+ \AxiomC{$\Gamma, \exists y \forall x. (x=y) \leftrightarrow \phi \vdash \Delta$}
+ \RightLabel{\text { LeftExistsOne}}
+ \UnaryInfC{$\Gamma, \exists ! x. \phi \vdash \Delta$}
+ \DisplayProof
+ }
+ \\[5ex]
+
+ \multicolumn{2}{c}{
+ \AxiomC{$\Gamma \vdash \exists y \forall x. (x=y) \leftrightarrow \phi , \Delta$}
+ \RightLabel{\text { RightExistsOne}}
+ \UnaryInfC{$\Gamma \vdash \exists ! x. \phi, \Delta$}
+ \DisplayProof
+ }
\\[5ex]
\multicolumn{2}{c}{
@@ -550,7 +562,7 @@ Finally, the two rules Restate and Weakening leverage the $\FOLalg$ algorithm.
\multicolumn{2}{c}{
\AxiomC{}
- \RightLabel{\text { Sorry, admit any statement as true. Usage transitively tracked with a warning.}}
+ \RightLabel{\text { Sorry: admit a statement as axiom. Usage transitively tracked.}}
\UnaryInfC{$\Gamma \vdash \Delta$}
\DisplayProof
}
@@ -558,12 +570,9 @@ Finally, the two rules Restate and Weakening leverage the $\FOLalg$ algorithm.
\end{center}
\end{minipage}
}
- \caption{Deduction rules allowed by LISA's kernel. Different occurrences of the same symbols need not represent equal elements, but only elements with the same \FOLalg{} normal form.}
- \label{fig:deduct_rules_1}
- % \label{fig:deduct_rules_2}
+ \caption{Deduction rules allowed by Lisa's kernel (Part 2). Different occurrences of the same symbols need not represent equal elements, but only elements with the same \FOLalg{} normal form.}
+ \label{fig:deduct_rules_2}
\end{figure}
-\newpage
-
\subsection{Proofs}
A sequent calculus proof is a tree whose nodes are proof steps.
@@ -591,9 +600,9 @@ The root of the proof shows the concluding statement, and the leaves are either
\label{fig:exampleProof}
\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.
+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.
-\autoref{fig:exampleProofLinear} shows the proof of Pierce's Law as linearized in LISA's kernel.
+\autoref{fig:exampleProofLinear} shows the proof of Pierce's Law as linearized in Lisa's kernel.
%
\begin{figure}[ht]
\begin{align*}
@@ -653,7 +662,7 @@ Finally, \autoref{fig:exampleProofQuantifiers} shows a proof with quantifiers.
\label{fig:exampleProofQuantifiers}
\end{figure}
-For every proof step, LISA's kernel actually expects more than only the premises and conclusion of the rule. The proof step also contains some parameters indicating how the deduction rule is precisely applied. This makes proof checking much simpler, and hence more trustworthy. Outside the kernel, LISA includes tactic which will infer such parameters automatically (see \autoref{sec:tactics}), so that in practice the user never has to write them.
+For every proof step, Lisa's kernel actually expects more than only the premises and conclusion of the rule. The proof step also contains some parameters indicating how the deduction rule is precisely applied. This makes proof checking much simpler, and hence more trustworthy. Outside the kernel, Lisa includes tactic which will infer such parameters automatically (see \autoref{sec:tactics}), so that in practice the user never has to write them.
\autoref{fig:ExampleProofPierceScala} shows how a kernel proof is written in scala.
\begin{figure}[ht]
@@ -667,12 +676,12 @@ val PierceLawProof = SCProof(IndexedSeq(
RightImplies(() |- (( φ ==> ψ ) ==> φ) ==> φ, 3, ( φ ==> ψ ) ==> φ, φ)
), Seq.empty /* no imports */ )
\end{lstlisting}
- \caption{The proof from~\autoref{fig:exampleProof} written for LISA's kernel. The second argument (empty here) is the sequence of proof imports. The symbols \lstinline|==>| and \lstinline||-| are ligatures for ==> and |- and are syntactic sugar defined outside the kernel.}
+ \caption{The proof from~\autoref{fig:exampleProof} written for Lisa's kernel. The second argument (empty here) is the sequence of proof imports. The symbols \lstinline|==>| and \lstinline||-| are ligatures for ==> and |- and are syntactic sugar defined outside the kernel.}
\label{fig:ExampleProofPierceScala}
\end{figure}
\paragraph*{Subproofs}
-To organize proofs, LISA's kernel also defines the Subproof proof step. A Subproof is a single proof step in a large proof with arbitrarily many premises:
+To organize proofs, Lisa's kernel also defines the Subproof proof step. A Subproof is a single proof step in a large proof with arbitrarily many premises:
\begin{lstlisting}
SCSubproof(sp: SCProof, premises: Seq[Int])
\end{lstlisting}
@@ -682,7 +691,7 @@ A Subproof only has an organizational purpose and allows to more easily write ta
\subsection{Proof Checker}
\label{subsec:proofchecker}
-In LISA, a proof object by itself has no guarantee to be correct. It is possible to write a wrong proof. LISA contains a \textit{proof checking} function, which, given a proof, will verify if it is correct. To be correct, a proof must satisfy the following conditions:
+In Lisa, a proof object by itself has no guarantee to be correct. It is possible to write a wrong proof. Lisa contains a \textit{proof checking} function, which, given a proof, will verify if it is correct. To be correct, a proof must satisfy the following conditions:
\begin{enumerate}
\item No proof step must refer to itself or a posterior proof step as a premise.
\item Every proof step must be correctly constructed, with the bottom sequent correctly following from the premises by the deduction rule and its arguments.
@@ -714,18 +723,18 @@ Note that there exists a proof step, called Sorry, used to represent unimplemen
In mathematics as a discipline, theorems don't exist in isolation. They depend on some agreed upon set of axioms, definitions, and previously proven theorems. Formally, theorems are developed within theories. A theory is defined by a language, which contains the symbols allowed in the theory, and by a set of axioms, which are assumed to hold true within it.
-In LISA, a \lstinline|Theory|{} is a mutable object that starts as the pure theory of predicate logic: It has no known symbols and no axioms. Then we can introduce into it elements of Set Theory (symbols $\in$, $\emptyset$, $\bigcup$ and set theory axioms, see Chapter~\ref{chapt:settheory}) or of any other theory.
+In Lisa, a \lstinline|Theory|{} is a mutable object that starts as the pure theory of predicate logic: It has no known symbols and no axioms. Then we can introduce into it elements of Set Theory (symbols $\in$, $\emptyset$, $\bigcup$ and set theory axioms, see Chapter~\ref{chapt:settheory}) or of any other theory.
To conduct a proof inside a \lstinline|Theory|{}, using its axioms, the proof should be normally constructed and the needed axioms specified in the imports of the proof. Then, the proof can be given to the \lstinline|Theory|{} to check, along with \textit{justifications} for all imports of the proof. A justification is either an axiom, a previously proven theorem, or a definition. The \lstinline|Theory|{} object will check that every import of the proof is properly justified by a \textit{justification} in the theory, i.e. that the proof is in fact not conditional in the theory. Then, it will pass the proof to the proof checker. If the proof is correct, it will return a \lstinline|Theorem|{} encapsulating the sequent. This theorem will be allowed to be used in all further proofs as an import, exactly like an axiom. Axioms and theorems also have a name.
\subsection{Definitions}
\label{subsec:definitions}
The user can also introduce definitions in the \lstinline|Theory|{}.
-LISA's kernel allows to define two kinds of objects: Function (or Term) symbols and Predicate symbols.
+Lisa's kernel allows to define two kinds of objects: Function (or Term) symbols and Predicate symbols.
\begin{figure}
- A definition in LISA is one of those two kinds of objects: A predicate definition or a function definition.
+ A definition in Lisa is one of those two kinds of objects: A predicate definition or a function definition.
\begin{lstlisting}
PredicateDefinition(
label: ConstantAtomicLabel,
@@ -754,7 +763,7 @@ LISA's kernel allows to define two kinds of objects: Function (or Term) symbols
corresponds to \\
\hspace*{1.3em}``For any $\vec{x}$, let $f^n(\vec{x}) \textnormal{ be the unique } y \textnormal{ such that } \varphi$ holds."
- \caption{Definitions in LISA.}
+ \caption{Definitions in Lisa.}
\label{fig:definitions}
\end{figure}
@@ -963,14 +972,14 @@ getTheorem(name: String)
\fi
}
-\section{Using LISA's Kernel}
+\section{Using Lisa's Kernel}
\label{sec:kernelHelpers}
-The kernel itself is a logical core, whose main purpose is to attest correctness of mathematical developments and proofs. In particular, it is not intended to be used directly to formalise a large library, as doing so would be very verbose. It instead serves as either a foundation for LISA's user interface and automation, or as a tool to write and verify formal proofs produced by other programs.
-Nonetheless, LISA's kernel comes with a set of utilities and features and syntactic sugar that make the kernel more user-friendly.
+The kernel itself is a logical core, whose main purpose is to attest correctness of mathematical developments and proofs. In particular, it is not intended to be used directly to formalise a large library, as doing so would be very verbose. It instead serves as either a foundation for Lisa's user interface and automation, or as a tool to write and verify formal proofs produced by other programs.
+Nonetheless, Lisa's kernel comes with a set of utilities and features and syntactic sugar that make the kernel more user-friendly.
\subsection{Syntactic Sugar}
\paragraph{Aliases}
-Scala accepts most unicode symbols in identifiers, allowing LISA to define alternative representation for logical symbols
+Scala accepts most unicode symbols in identifiers, allowing Lisa to define alternative representation for logical symbols
\begin{center}
\begin{tabular}{| c | c |}
@@ -990,7 +999,7 @@ Scala accepts most unicode symbols in identifiers, allowing LISA to define alter
\end{tabular}
\end{center}
\paragraph{Identifiers}
-An identifier is a pair of a string and a number. Note that LISA kernel does not accept whitespace nor symbols among \lstinline|()[]{}_| as part of identifiers. The underscore can be used to write both the string and the integer part of an identifier at once. For example,
+An identifier is a pair of a string and a number. Note that Lisa kernel does not accept whitespace nor symbols among \lstinline|()[]{}_| as part of identifiers. The underscore can be used to write both the string and the integer part of an identifier at once. For example,
\begin{lstlisting}[language=Scala]
val x: VariableLabel("x_4")
@@ -1028,7 +1037,7 @@ The strict syntax to construct the sequent $\phi, \psi \vdash \gamma, \delta$ is
\begin{lstlisting}[language=Scala]
Sequent(Set(phi, psi), Set(phi, psi))
\end{lstlisting}
-but thanks again to extensions and implicit conversions, LISA accepts
+but thanks again to extensions and implicit conversions, Lisa accepts
\begin{lstlisting}[language=Scala]
(phi, psi) |- (phi, psi)
\end{lstlisting}
diff --git a/refman/lisa.pdf b/refman/lisa.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..485feaa4cc5206b5d66d69b6b1a9edad2fb916cf
Binary files /dev/null and b/refman/lisa.pdf differ
diff --git a/refman/lisa.tex b/refman/lisa.tex
new file mode 100644
index 0000000000000000000000000000000000000000..d78e27da4fd9770e26c436726c8c42238a34fc2d
--- /dev/null
+++ b/refman/lisa.tex
@@ -0,0 +1,58 @@
+% !TEX program = xelatex
+
+% Page size:
+\documentclass[11pt,b5paper]{book}
+ % Reduce margins whatever the original text area size was.
+ \edef\mtht{\the\textheight}
+ \edef\mtwd{\dimexpr\the\textwidth+1cm}
+ \usepackage[paperwidth=\dimexpr\mtwd+1.4cm\relax,
+ paperheight=\dimexpr\mtht+1.8cm\relax,
+ text={\mtwd,\mtht},
+ left=0.7cm,
+ top=1.3cm]{geometry}
+
+\input{macro} % also imports
+\input{shortcuts}
+
+\newcommand{\ourtitle}{Lisa Manual}
+\newcommand{\ournames}{Simon Guilloud, Sankalp Gambhir, Viktor Kun\v{c}ak}
+\title{\ourtitle}
+\author{\ournames}
+\date{}
+
+% PDF links and meta data
+\usepackage{hyperref}
+\makeatletter
+\hypersetup{
+ colorlinks=true,
+ linkcolor=blue,
+ filecolor=magenta,
+ urlcolor=blue,
+ pdftitle={\@title},
+ pdfauthor={\@author}
+}
+\makeatother
+\urlstyle{same}
+
+\begin{document}
+\input{titlepage.tex}
+
+% Uncomment once the chapter says something useful to readers as opposed to authors:
+%\chapter*{Introduction}
+%This document aims to give a complete documentation on Lisa. Tentatively, every chapter and section will explain a part or concept of Lisa, and explains both its implementation and its theoretical foundations.
+
+\tableofcontents
+
+\input{quickguide.tex}
+
+\input{kernel.tex}
+
+\input{prooflib.tex}
+
+\input{theory.tex}
+
+\input{theorytopics.tex}
+
+\bibliographystyle{plain}
+\bibliography{sguilloud.bib}
+\end{document}
diff --git a/Reference Manual/macro.tex b/refman/macro.tex
similarity index 95%
rename from Reference Manual/macro.tex
rename to refman/macro.tex
index 3f33ec6059986700233b204da47f5e377603376f..2919e649c00daa150ead14152c8fc1e3c8cbe366 100644
--- a/Reference Manual/macro.tex
+++ b/refman/macro.tex
@@ -12,7 +12,6 @@
\usepackage[dvipsnames]{xcolor}
\usepackage{csquotes}
\usepackage[strings]{underscore}
-\usepackage{hyperref}
\usepackage{bussproofs}
\usepackage{makecell}
\usepackage{subcaption}
@@ -24,6 +23,7 @@
\usepackage[T1]{fontenc}
\usepackage{newunicodechar} %To map unicode in listings to a different font than Fira Code
\renewcommand\sfdefault{ua1}
+
\sloppy % better (?) margin handling
@@ -47,20 +47,6 @@
\newcommand*{\definitionautorefname}{Definition}
-% URLs
-
-\hypersetup{
- colorlinks=true,
- linkcolor=blue,
- filecolor=magenta,
- urlcolor=blue,
- pdftitle={LISA Reference Manual},
- pdfpagemode=FullScreen,
-}
-\urlstyle{same}
-
-
-
% Code fonts
%\usepackage{lstfiracode}
@@ -79,6 +65,7 @@
% Correct lstlisting parsing of unicode character. Add unicode points at the end.
+% To add: code for \vdash
\makeatletter
\lst@InputCatcodes
\def\lst@DefEC{%
@@ -104,7 +91,7 @@
\def\verbatim@nolig@list{}
\makeatother
-\definecolor{green}{rgb}{0, 0.6, 0}
+\definecolor{green}{rgb}{0, 0.35, 0}
\definecolor{comments}{RGB}{80,0,110}
diff --git a/Reference Manual/prooflib.tex b/refman/prooflib.tex
similarity index 90%
rename from Reference Manual/prooflib.tex
rename to refman/prooflib.tex
index a025733d72edeefd36b37a4a603fd054798a5523..b338295ac7ad4dca2d9a68f5349f0c890bb557b2 100644
--- a/Reference Manual/prooflib.tex
+++ b/refman/prooflib.tex
@@ -1,9 +1,9 @@
\chapter{Developping Mathematics with Prooflib}
\label{chapt:prooflib}
-LISA's kernel offers all the necessary tools to develops proofs, but reading and writing proofs written directly in its language is cumbersome.
-To develop and maintain a library of mathematical development, LISA offers a dedicate interface and DSL to write proofs: Prooflib
-LISA provides a canonical way of writing and organizing Kernel proofs by mean of a set of utilities and a DSL made possible by some of Scala 3's features.
-\autoref{fig:theoryFileExample} is a reminder from \autoref{chapt:quickguide} of the canonical way to write a theory file in LISA.
+Lisa's kernel offers all the necessary tools to develops proofs, but reading and writing proofs written directly in its language is cumbersome.
+To develop and maintain a library of mathematical development, Lisa offers a dedicate interface and DSL to write proofs: Prooflib
+Lisa provides a canonical way of writing and organizing Kernel proofs by mean of a set of utilities and a DSL made possible by some of Scala 3's features.
+\autoref{fig:theoryFileExample} is a reminder from \autoref{chapt:quickguide} of the canonical way to write a theory file in Lisa.
\begin{figure}
\begin{lstlisting}[language=lisa, frame=single]
@@ -33,7 +33,7 @@ object MyTheoryName extends lisa.Main {
}
\end{lstlisting}
-\caption{An example of a theory file in LISA}
+\caption{An example of a theory file in Lisa}
\label{fig:theoryFileExample}
\end{figure}
@@ -75,7 +75,7 @@ Formally, the proof in (...) is a proof of $P(c) \vdash \phi$. This can be trans
\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}.
+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]
@@ -86,7 +86,7 @@ This simulation is provided by LISA through the \lstinline|witness|{} method. It
c.definition, emptySetAxiom of (x:= c))
}
\end{lstlisting}
- \caption{An example use of local definitions in LISA}
+ \caption{An example use of local definitions in Lisa}
\label{fig:localDefinitionExample}
\end{figure}
diff --git a/Reference Manual/quickguide.tex b/refman/quickguide.tex
similarity index 74%
rename from Reference Manual/quickguide.tex
rename to refman/quickguide.tex
index 97545b6de6522cc7ffd586cfb97a9eee83e1269a..503eaa4cad1f43602d60550dff572dba933fe782 100644
--- a/Reference Manual/quickguide.tex
+++ b/refman/quickguide.tex
@@ -1,17 +1,17 @@
-\chapter{Quick Guide for writing proofs in LISA}
+\chapter{Starting with Proofs in Lisa}
\label{chapt:quickguide}
-LISA is a proof assistant, i.e. a tool to help humans to write completely formal proofs of mathematical statements.
+Lisa is a proof assistant. Proof assistants support development of formal proofs of mathematical statements.
-The centerpiece of LISA (called the kernel) contains a definition of first order logic (FOL), which is a logical framework to make formal mathematical statements and proofs. This kernel is what provides correctness guarantees to the user. It only accepts a small set of formal deduction rule such as ``if $a$ is true and $b$ is true then $a\land b$ is true".
-This is in contrast with human-written proofs, which can contain a wide variety of complex or implicit arguments. Hence, if a proof is accepted as being correct by the kernel, we are guaranteed that it indeed is\footnote{Of course, it is always possible that the kernel itself has a bug in its implementation, but because it is a very small and simple program, we can build strong confidence that it is correct.}.
-LISA's kernel is described in details in \autoref{chapt:kernel}.
+The centerpiece of Lisa (called the \emph{kernel}) contains a mechanized implementation of first order logic (FOL), a logical framework to write mathematical statements and their proofs. This kernel is what provides correctness guarantees to the user. The kernel only accepts a small set of formal deduction rule such as ``if $a$ is true and $b$ is true then $a\land b$ is true''.
+This is in contrast to human-written proofs, which may contain a wide variety of complex or implicit arguments. If a proof is accepted as being correct by the kernel, it is expected to meet objective criteria for valid proofs according to the field of formal mathematical logic.\footnote{It is possible that the kernel itself has an implementation bug, but because it is a very small and simple program available in open source, we can build strong confidence that it is correct.}
+Lisa's kernel is described in more detail in \autoref{chapt:kernel}.
-However, building advanced math such as topology or probability theory only from those primitive constructions would be excessively tedious. Instead, we use them as primitive building blocs which can be combined and automatized. Beyond the correctness guarantees of the kernel, LISA's purpose is to provide tools to make writing formal proofs easier. This include automation, via decision procedure which automatically prove theorems and deductions, and layers of abstraction (helpers, domain specific language) which make the presentation of formal statements and proofs closer to the traditional, human way of writing proofs.
-This is not unlike programming languages: assembly is in theory sufficient to write any program on a computer, but high level programming languages offer many convenient features which make writing complex programs easier and which are ultimately translated into assembly.
-\autoref{chapt:prooflib} explain in details how all these layers of abstraction and automation work. The rest of the present chapter will give a quick guide on how to use LISA. If you are not familiar with first order logic, we suggest you first read an introduction to first order logic such as \url{lara.epfl.ch/w/sav08/predicate_logic_informally}.
+Writing mathematical theories (for example, group theory, combinatorics, topology, theory of computation) directly from these primitive constructions would be tedious. Instead, we use them as building blocs that can be combined and automatized. Beyond the correctness guarantees of the kernel, Lisa's purpose is to provide tools to make writing formal proofs easier. This include automation, via search procedures that automatically prove theorems, and layers of abstraction (helpers, domain specific language), which make the presentation of formal statements and proofs closer to the traditional, human way of writing proofs.
+This is similar to programming languages: machine language is sufficient to write any program on a computer, but high level programming languages offer many convenient features which make writing complex programs easier and which are ultimately translated into assembly automatically.
+\autoref{chapt:prooflib} explains how these layers of abstraction and automation work. The rest of the present chapter gives a quick guide on how to use Lisa.
\section{Installation}
-LISA requires the Scala programming language to run. You can download and install Scala following \url{www.scala-lang.org/download/}. Once this is done, clone the LISA repository:
+Lisa requires the Scala programming language to run. You can download and install Scala following the instructions at the Scala home page\footnote{\url{www.scala-lang.org/}}. Subsequently, clone the Lisa git repository:
\begin{lstlisting}[language=console]
> git clone https://github.com/epfl-lara/lisa
\end{lstlisting}
@@ -20,37 +20,36 @@ To test your installation, do
> cd lisa
> sbt
\end{lstlisting}
-SBT is a tool to run scala project and manage versions and dependencies. When it finished loading, do
+\lstinline|sbt| is a tool to run a Scala project and manage versions and dependencies. Once inside sbt, run the following commands:
\begin{lstlisting}[language=console]
> project lisa-examples
> run
\end{lstlisting}
-Wait for the LISA codebase to be compiled and then press the number corresponding to "Example". You should obtain the following result:
+Wait for the Lisa codebase to be compiled and then press the number corresponding to "Example". You should obtain the result demonstrating some example theorems proven, such as the following:
+
\noindent\begin{minipage}{\linewidth}\vspace{1em}
\begin{lstlisting}[language=console]
@*Theorem fixedPointDoubleApplication :=
- ∀'x. 'P('x) ==> 'P('f('x)) ⊢ 'P('x) ==> 'P('f('f('x)))
+ ∀'x. 'P('x) ==> 'P('f('x)) |- 'P('x) ==> 'P('f('f('x)))
- Theorem emptySetIsASubset := ⊢ subsetOf(emptySet, 'x)
+ Theorem emptySetIsASubset := |- subsetOf(emptySet, 'x)
Theorem setWithElementNonEmpty :=
- elem('y, 'x) ⊢ ¬('x = emptySet)
+ elem('y, 'x) |- ¬('x = emptySet)
- Theorem powerSetNonEmpty := ⊢ ¬(powerSet('x) = emptySet)
+ Theorem powerSetNonEmpty := |- ¬(powerSet('x) = emptySet)
*@
\end{lstlisting}
\end{minipage}
-
-
\section{Development Environment}
-To write LISA proofs, you can use any text editor or IDE. We recommend using \emph{Visual Studio Code} with the \emph{Metals} plugin.
+To write Lisa proofs, you can use any text editor or IDE. We recommend using \emph{Visual Studio Code} (henceforth VSCode) with the \emph{Metals} plugin.
\subsection*{A Note on Special Characters}
-Math is full of special character. Lisa usually admits both an ascii name and a unicode name for such symbols. By enabling ligatures, common ascii characters such as \lstinline|=|\lstinline|=|\lstinline|>| are rendered as \lstinline|==>|.
-The present document uses the font \href{https://github.com/tonsky/FiraCode}{Fira Code}. Once installed on your system, you can activate it and ligatures on VSCode the following way:
+Math often uses symbols beyond the Latin alphabet. Lisa usually admits both an English alphabet name and a unicode name for such symbols. By enabling \emph{font ligatures}, common character sequences, such as \lstinline|=|\lstinline|=|\lstinline|>| are rendered as \lstinline|==>|.
+The present document also uses the font \href{https://github.com/tonsky/FiraCode}{Fira Code}. Once installed on your system, you can activate it and ligatures on VSCode the following way:
\begin{enumerate}
- \item Press ctrl-shift-P
+ \item Press Ctrl-Shift-P
\item Search for ``Open User Settings (JSON)''
\item in the \lstinline|settings.json| file, add:
\begin{lstlisting}
@@ -58,7 +57,7 @@ The present document uses the font \href{https://github.com/tonsky/FiraCode}{Fir
"editor.fontLigatures": true,
\end{lstlisting}
\end{enumerate}
-Other symbols such as \lstinline|∀| are unicode symbols, which can be entered via their unicode code, depending on your OS\footnote{alt+numpad on windows, ctrl-shift-U+code on Linux}, or by using an extension for VS Code such as \emph{Fast Unicode Math Characters}, \emph{Insert Unicode} or \emph{Unicode Latex}.
+Other symbols such as \lstinline|∀| are Unicode symbols, which can be entered via their unicode code, depending on your OS\footnote{alt+numpad on windows, Ctrl-Shift-U+code on Linux}, or by using an extension for VS Code such as \emph{Fast Unicode Math Characters}, \emph{Insert Unicode} or \emph{Unicode Latex}.
A cheat sheet of the most common symbols and how to input them is in \autoref{tab:Unicode}.
\begin{table}
\center
@@ -75,13 +74,13 @@ A cheat sheet of the most common symbols and how to input them is in \autoref{ta
\lstinline| ⊆ | & U+2286 & subseteq \\ \hline
\lstinline| ∅ | & U+2205 & emptyset \\
\end{tabular}
- \caption{Most frequently used Unicode symbols and ligatures.}
+ \caption{Frequently used Unicode symbols and ligatures.}
\label{tab:Unicode}
\end{table}
-Note that by default, unicode characters will not be printed correctly on a Windows console. You will need to activate the corresponding charset and pick a font with support for unicode in your console's options, such as Consolas.
+Note that by default, Unicode characters may not be printed correctly on a Windows console. You will need to activate the corresponding charset and pick a font with support for unicode in your console's options, such as Consolas.
\section{Writing theory files}
-LISA provides a canonical way of writing and organizing kernel proofs by mean of a set of utilities and a DSL made possible by some of Scala 3's features.
+Lisa provides a canonical way of writing and organizing kernel proofs by mean of a set of utilities and a domain-specific language (DSL) made possible by some of Scala's features.
To prove some theorems by yourself, start by creating a file named \lstinline|MyTheoryName.scala| right next to the Example.scala file\footnote{The relative path is lisa/lisa-examples/src/main/scala}.
Then simply write:
@@ -92,11 +91,11 @@ object MyTheoryName extends lisa.Main {
}
\end{lstlisting}
\end{minipage}
-and that's it! This will give you access to all the necessary LISA features. Let see how one can use them to prove a theorem:
+and that's it! This will give you access to all the necessary Lisa features. Let see how one can use them to prove a theorem:
$$
\forall x. P(x) \implies P(f(x)) \vdash P(x) \implies P(f(f(x)))
$$
-To state the theorem, we first need to tell LISA that $x$ is a variable, $f$ is a function symbol and $P$ a predicate symbol.
+To state the theorem, we first need to tell Lisa that $x$ is a variable, $f$ is a function symbol and $P$ a predicate symbol.
\noindent\begin{minipage}{\linewidth}\vspace{1em}
\begin{lstlisting}[language=lisa, frame=single]
@@ -109,7 +108,7 @@ object MyTheoryName extends lisa.Main {
\end{lstlisting}
\end{minipage}
-where \lstinline|[1]| indicates that the symbol is of arity 1 (it takes a single argument). The symbols \lstinline|x, f, P| are scala identifiers that can be freely used in theorem statements and proofs, but they are also formal symbols of FOL in LISA's kernel.
+where \lstinline|[1]| indicates that the symbol is of arity 1 (it takes a single argument). The symbols \lstinline|x, f, P| are scala identifiers that can be freely used in theorem statements and proofs, but they are also formal symbols of FOL in Lisa's kernel.
We now can state our theorem:
\noindent\begin{minipage}{\linewidth}\vspace{1em}
@@ -148,14 +147,14 @@ object MyTheoryName extends lisa.Main {
\end{lstlisting}
\end{minipage}
First, we use the \lstinline|assume| construct in line 6.
-This tells to LISA that the assumed formula is understood as being implicitly on the left hand side of every statement in the rest of the proof.
+This tells to Lisa that the assumed formula is understood as being implicitly on the left hand side of every statement in the rest of the proof.
Then, we need to instantiate the quantified formula twice using a specialized tactic. In lines 7 and 8, we use \lstinline|have| to state that a formula or sequent is true (given the assumption inside \lstinline|assume|), and that the proof of this is produced by the tactic \lstinline|InstantiateForall|.
We'll see more about the interface of a tactic later. To be able to reuse intermediate steps at any point later, we also assign the intermediates step to a variable.
Finally, the last line says that the conclusion of the theorem itself, \lstinline|thesis|, can be proven using the tactic \lstinline|Tautology| and the two intermediate steps we reached. \lstinline|Tautology| is a tactic that is able to do reasoning with propositional connectives. It implements a complete decision procedure for propositional logic that is described in \autoref{tact:Tautology}.
-LISA is based on set theory, so you can also use set-theoretic primitives such as in the following theorem.
+Lisa is based on set theory, so you can also use set-theoretic primitives such as in the following theorem.
\noindent\begin{minipage}{\linewidth}\vspace{1em}
\begin{lstlisting}[language=lisa, frame=single]
@@ -194,7 +193,7 @@ is equivalent to
\end{lstlisting}
\end{minipage}
-LISA also allows to introduce definitions. There are essentially two kind of definitions, \emph{aliases} and definition via \emph{unique existence}.
+Lisa also allows to introduce definitions. There are essentially two kind of definitions, \emph{aliases} and definition via \emph{unique existence}.
An alias defines a constant, a function or predicate as being equal (or equivalent) to a given formula or term. For example,
\noindent\begin{minipage}{\linewidth}\vspace{1em}
@@ -283,4 +282,4 @@ If a \lstinline|subst| is a formula rather than a proven fact, then it should be
have(Q(s) /\ s===f(t)) by ???
thenHave(A, f(t) === t |- P(s) /\ s===t)
.by Substitution.ApplyRules(subst, f(t) === t)
-\end{lstlisting}
\ No newline at end of file
+\end{lstlisting}
diff --git a/refman/r b/refman/r
new file mode 100755
index 0000000000000000000000000000000000000000..35a76bb83986cc598b0544e57d9c722099f69f3e
--- /dev/null
+++ b/refman/r
@@ -0,0 +1 @@
+latexmk lisa.tex
diff --git a/Reference Manual/sguilloud.bib b/refman/sguilloud.bib
similarity index 100%
rename from Reference Manual/sguilloud.bib
rename to refman/sguilloud.bib
diff --git a/Reference Manual/shortcuts.tex b/refman/shortcuts.tex
similarity index 100%
rename from Reference Manual/shortcuts.tex
rename to refman/shortcuts.tex
diff --git a/Reference Manual/theory.tex b/refman/theory.tex
similarity index 96%
rename from Reference Manual/theory.tex
rename to refman/theory.tex
index 7dca513aa78832b9b0991564fdc2ef97d06a23c5..7eaa52d70dbb032e144bd40045d75e4b8877fe72 100644
--- a/Reference Manual/theory.tex
+++ b/refman/theory.tex
@@ -9,20 +9,20 @@ Actual mathematical functions on the other hand, are proper sets which contains
Indeed, on one hand a predicate symbol defines a truth value on all possible sets, but on the other hand it is impossible to use the symbol alone, without applying it to arguments, or to quantify over function symbol.
-LISA is based on set theory. More specifically, it is based on ZF with (still not decided) an axiom of choice, of global choice, or Tarski's universes.
+Lisa is based on set theory. More specifically, it is based on ZF with (still not decided) an axiom of choice, of global choice, or Tarski's universes.
ZF Set Theory stands for Zermelo-Fraenkel Set Theory. It contains a set of initial predicate symbols and function symbols, as shown in Figure \ref{fig:symbolszf}. It also contains the 7 axioms of Zermelo (Figure \ref{fig:axiomsz}), which are technically sufficient to formalize a large portion of mathematics, plus the axiom of replacement of Fraenkel (Figure \ref{fig:axiomszf}), which is needed to formalize more complex mathematical theories.
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 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.
\begin{figure}
\begin{center}
\begin{tabular}{l|c|l}
- {} & Math symbol & LISA Kernel \\ \hline
+ {} & Math symbol & Lisa Kernel \\ \hline
Set Membership predicate & $\in$ & \lstinline$in(s,t)$ \\
Subset predicate & $\subset$ & \lstinline$subset(s,t)$ \\
Empty Set constant & $\emptyset$ & \lstinline$emptyset()$ \\
@@ -101,14 +101,14 @@ Note that the replacement axiom \autoref{axzf:replacement} is conditional of the
$$ \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|,
+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.
+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
@@ -117,7 +117,7 @@ Moreover, we most often want to map a set by a known function. In those case, LI
\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}
+ \caption{Comprehensions in Lisa}
\label{tab:comprehensions}
\end{table}
diff --git a/Reference Manual/theorytopics.tex b/refman/theorytopics.tex
similarity index 95%
rename from Reference Manual/theorytopics.tex
rename to refman/theorytopics.tex
index e067a156c29cdfc8fe73e150d359ef0443f1b1f9..3bfc94e6e46e6174d720975635b6ebe012b3504e 100644
--- a/Reference Manual/theorytopics.tex
+++ b/refman/theorytopics.tex
@@ -1,6 +1,8 @@
\chapter{Selected Theoretical Topics}
\label{part:theory}
+Algorithms and techniques to solve and reduce formulas in propositional logic (and its generalizations) are a major field of study. They have prime relevance in SAT and SMT solving algorithms. Lisa makes use of some of them: some of the in the kernel, others as available tactics.
+
\section{Set Theory and Mathematical Logic}
\subsection{First Order Logic with Schematic Variables}
\label{sec:theoryfol}
diff --git a/refman/titlepage.tex b/refman/titlepage.tex
new file mode 100644
index 0000000000000000000000000000000000000000..bf9b865611c0778e5ef5b2b5b6a09693ca6c1c40
--- /dev/null
+++ b/refman/titlepage.tex
@@ -0,0 +1,35 @@
+%\newfontfamily\titlefont{Arial}
+\begin{titlepage}
+\sf
+%\fontfamily{\sfdefault}\selectfont
+
+ \begin{center}
+ \vspace*{1cm}
+
+ \textbf{\Huge \ourtitle}
+
+ \vspace{1.5cm}
+
+ %\textbf{\large Version 0.2.1}
+
+ \textbf{\large \today}
+
+ \vspace{1.5cm}
+
+ {\Large Laboratory for Automated Reasoning and Analysis \\ \ \\ EPFL, Switzerland}
+
+ \vspace{1.5cm}
+
+ \date{}
+
+ \end{center}
+
+ \vfill
+
+ Contributors:
+ \begin{flushright}
+ \large
+ \ournames
+ \end{flushright}
+
+ \end{titlepage}