Skip to content

Commit

Permalink
Formatted kernel proof system to fit pages
Browse files Browse the repository at this point in the history
  • Loading branch information
@vkuncak
vkuncak committed Dec 28, 2023
1 parent 784f39f commit a2f1066
Show file tree
Hide file tree
Showing 7 changed files with 124 additions and 118 deletions.
73 changes: 41 additions & 32 deletions refman/kernel.tex
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
%\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.

Expand Down Expand Up @@ -378,7 +378,7 @@ \subsection{Sequent Calculus}
\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.

Expand All @@ -387,24 +387,20 @@ \subsection{Sequent Calculus}


\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}}
Expand Down Expand Up @@ -478,16 +474,32 @@ \subsection{Sequent Calculus}
\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}{
Expand Down Expand Up @@ -550,20 +562,17 @@ \subsection{Sequent Calculus}

\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
}
\end{tabular}
\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.
Expand Down
Binary file modified refman/lisa.pdf
View file
Binary file not shown.
68 changes: 22 additions & 46 deletions refman/lisa.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,56 +14,32 @@
\input{macro} % also imports
\input{shortcuts}

\title{Lisa Reference Manual (WIP)}
\author{Simon Guilloud\\Laboratory for Automated Reasoning and Analysis, EPFL}
\newcommand{\ourtitle}{Lisa Manual}
\newcommand{\ournames}{Simon Guilloud, Sankalp Gambhir, Viktor Kun\v{c}ak}
\title{\ourtitle}
\author{\ournames}
\date{}

\begin{document}

%\newfontfamily\titlefont{Arial}

\begin{titlepage}
\sf
%\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}
% PDF links and meta data
\usepackage{hyperref}
\makeatletter
\hypersetup{
colorlinks=true,
linkcolor=blue,
filecolor=magenta,
urlcolor=blue,
pdftitle={\@title},
pdfauthor={\@author}
}
\makeatother
\urlstyle{same}

\vspace{1.5cm}

\date{}

\end{center}

\vfill

\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}
\chapter*{Introduction}
\begin{document}
\input{titlepage.tex}

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.
% 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

Expand Down
17 changes: 2 additions & 15 deletions refman/macro.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,6 @@
\usepackage[dvipsnames]{xcolor}
\usepackage{csquotes}
\usepackage[strings]{underscore}
\usepackage{hyperref}
\usepackage{bussproofs}
\usepackage{makecell}
\usepackage{subcaption}
Expand Down Expand Up @@ -48,19 +47,6 @@
\newcommand*{\definitionautorefname}{Definition}


% URLs

\hypersetup{
colorlinks=true,
linkcolor=blue,
filecolor=magenta,
urlcolor=blue,
pdftitle={Lisa Reference Manual}
}
\urlstyle{same}



% Code fonts

%\usepackage{lstfiracode}
Expand All @@ -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{%
Expand All @@ -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}

Expand Down
48 changes: 23 additions & 25 deletions refman/quickguide.tex
View file
Original file line number Diff line number Diff line change
@@ -1,17 +1,17 @@
\chapter{Lisa Proof Starting Guide}
\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}
Expand All @@ -20,45 +20,43 @@ \section{Installation}
> 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}
"editor.fontFamily": "'Fira Code', Consolas, monospace",
"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
Expand All @@ -75,13 +73,13 @@ \subsection*{A Note on Special Characters}
\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:

Expand Down
1 change: 1 addition & 0 deletions refman/r
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
latexmk lisa.tex
35 changes: 35 additions & 0 deletions refman/titlepage.tex
View file
Original file line number Diff line number Diff line change
@@ -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}

0 comments on commit a2f1066

Please sign in to comment.