Update report (2022-06-22)

CITATION.cff

@@ -4,7 +4,7 @@ authors:
 - family-names: "Cassayre"
   given-names: "Florian"
   orcid: "https://orcid.org/0000-0001-5784-8051"
-title: "A front-end for LISA"
+title: "A front-end for the LISA proof assistant"
 version: 1.0.0
 doi: 10.5281/zenodo.6645113
 date-released: 2022-06-24

README.md

@@ -9,7 +9,7 @@
 This repository hosts the work related to my Master Project (PDM) at [LARA](https://lara.epfl.ch/w/).
 This includes source code, writeup and any other significant resource related to the project.
 
-Project title: ***A Proof System for LISA***
+Project title: ***A front-end for the LISA proof assistant***
 
 Dates: **21.02.2022** to **24.06.2022**
 

thesis/report/abstract.tex

@@ -11,10 +11,10 @@
 \begin{abstractpage}
 \begin{i18nabstract}{english}
   % Don't forget to update the translation if you make any changes here!
-  We propose a front-end framework for the novel proof assistant LISA. The two systems are based on Gentzen's sequent calculus with first-order logic and are implemented in the Scala programming language. Our framework supports different proof styles and provides a declarative language for tactics. The usage of tactics is facilitated thanks to a parameter inference system. The proofs written in our framework can then be translated into the trusted kernel for verification. We demonstrate that our framework simplifies the process of writing formal proofs for LISA, and that it is suitable for an interactive use. We also introduce other relevant components for LISA such as a strongly typed programming interface, a two-way parser and printer, and a proof simplifier.
+  We propose a front-end framework for the novel proof assistant LISA. The two systems are based on Gentzen's sequent calculus with first-order logic and are implemented in the Scala programming language. Our framework supports different proof styles and provides a declarative language for tactics. The usage of tactics is facilitated thanks to a parameter inference system. The proofs written in our framework can be translated into the trusted kernel for verification. We demonstrate that our framework simplifies the process of writing formal proofs for LISA, and that it is suitable for an interactive usage. We also introduce other relevant components for LISA such as a strongly typed programming interface, a two-way parser and printer, and a proof simplifier.
 \end{i18nabstract}
 
 \begin{i18nabstract}{french}
-  Nous proposons un cadriciel pour le nouvel assistant de preuve LISA. Les deux systèmes sont basés sur le calcul des séquents de Gentzen en utilisant la logique du premier ordre, et sont implémentés dans le langage de programmation Scala. Notre système prend en charge différents styles de preuve et apporte un langage déclaratif pour les tactiques. L'utilisation des tactiques est facilitée grâce à un système d'inférence des paramètres. Les preuves écrites dans ce cadre peuvent ensuite être traduites vers le noyau de confiance pour y être vérifiées. Nous montrons que notre cadre permet de simplifier le processus d'écriture de démonstrations formelles pour LISA, et qu'il est adapté à une utilisation interactive. Nous présentons d'autres composantes clés pour LISA, telles qu'une interface de programmation fortement typée, un analyseur syntactique ains qu'un système d'impression élégante, et un simplificateur de preuves.
+  Nous proposons un cadriciel pour le nouvel assistant de preuve LISA. Les deux systèmes sont basés sur le calcul des séquents de Gentzen en utilisant la logique du premier ordre, et sont implémentés dans le langage de programmation Scala. Notre système prend en charge différents styles de preuve et apporte un langage déclaratif pour les tactiques. L'utilisation des tactiques est facilitée par un système d'inférence des paramètres. Les preuves écrites dans ce cadre peuvent ensuite être traduites vers le noyau de confiance pour y être vérifiées. Nous montrons que notre cadre permet de simplifier le processus d'écriture de démonstrations formelles pour LISA, et qu'il est adapté à une utilisation interactive. Nous présentons d'autres composantes clés pour LISA, telles qu'une interface de programmation fortement typée, un analyseur syntactique ains qu'un système d'impression élégante, et un simplificateur de preuves.
 \end{i18nabstract}
 \end{abstractpage}

thesis/report/bibliography.bib

@@ -227,3 +227,10 @@ @book{Appel1989
   year={1989},
   publisher={American Mathematical Soc.}
 }
+
+@phdthesis{Ayers2021,
+  title={A Tool for Producing Verified, Explainable Proofs},
+  author={Ayers, Edward},
+  year={2021},
+  school={University of Cambridge}
+}

thesis/report/chapters/1-introduction.tex

@@ -1,18 +1,16 @@
 \section{Introduction}
 \label{sec:introduction}
 
-A proof assistant is a piece of software that can assist a user in writing a particular type of proofs, one that can be verified by a machine. Proofs following this format are desirable because it suffices to show that the verification procedure is sound to automatically and irrefutably judge them. Computer-assisted theorem proving can also leverage the computational capabilities offered by machines, one of the most famous example being the proof of the \textit{four-color conjecture} \cite{Appel1989}. However, the greatest strength of proof assistants might also be their greatest weakness: they are often complex systems, which correctness is difficult to demonstrate and therefore are prone to bugs in their implementation.
+A proof assistant is a piece of software that can assist a human user in writing a particular type of proofs, one that can be verified by a machine. Proofs following this format are desirable because it suffices to show that the verification procedure is sound to automatically and irrefutably judge any of them. Computer-assisted theorem proving can also leverage the computational capabilities offered by machines, one of the most famous example being the proof of the \textit{four-color conjecture} \cite{Appel1989}. However, the greatest strength of proof assistants might also be their greatest weakness: they are often complex systems, whose correctness is difficult to demonstrate and therefore are prone to bugs in their implementation. They also suffer from a lack of understandability, both in terms of the underlying theories used and of the proofs produced, which results in a low adoption rate by mathematicians \cite{Ayers2021}.
 
-In this thesis we describe the design process of a front-end for the modern proof assistant LISA. Our main focus is to preserve the same soundness standards as the existing framework while making it more expressive and introducing an interactive component.
-
-The supporting source code for this project is published at the following address:
+In this thesis we describe the design process of a front-end for the modern proof assistant LISA. Our main focus is to preserve the same soundness standards as the existing framework while making it more expressive and interactive. The supporting source code for this project is published at the following address:
 \begin{center}
 \href{http://github.com/FlorianCassayre/master-project}{\textbf{github.com/FlorianCassayre/master-project}}\footnote{The current release is identified by commit: \code{c3499c2729730a7f807efb8676a92dcb6f8a3f8f}}
 \end{center}
 
 \subsection{LISA}
 
-LISA\footnote{\textbf{L}ISA \textbf{I}s \textbf{S}ets \textbf{A}utomated} is an ongoing project conducted at the lab for automated reasoning and analysis (LARA), EPFL. It is a library built on top of sequent calculus and set theory that enables the formalization of mathematical proofs \cite{Guilloud2022-2}.
+LISA\footnote{\textbf{L}ISA \textbf{I}s \textbf{S}ets \textbf{A}utomated} is an ongoing project conducted at the Lab for Automated Reasoning and Analysis (LARA), EPFL. It is a library built on top of sequent calculus and set theory that enables the formalization of mathematical proofs \cite{Guilloud2022-2}.
 
 \begin{figure}[H]
   $$
@@ -38,17 +36,17 @@ \subsection{LISA}
   \infer2[Right $\Leftrightarrow$]{\vdash \neg{?a} \lor {?b} \Leftrightarrow {?a} \Rightarrow {?b}}
   \end{prooftree}
   $$
-  \caption[Proof tree (1)]{An example of a proof in sequent calculus. Here it proves the tautology $\neg{?a}\lor{?b}\Leftrightarrow{?a}\Rightarrow{?b}$. The question mark indicates a schema, essentially a variable such that the statement holds true for any value. The inference used at every step is indicated.}
+  \caption[Proof tree (1)]{An example of a proof in sequent calculus. This proof demonstrates the tautology $\neg{?a}\lor{?b}\Leftrightarrow{?a}\Rightarrow{?b}$. The question mark indicates a schema, namely a variable that can later be instantiated. The inference rule used at every step is indicated on the right.}
   \label{fig:simple-lisa-proof-graph}
 \end{figure}
 
 \begin{figure}[H]
   \centering
   \input{figures/proof-mini.lisa}
-  \caption[Proof in LISA]{A representation of the proof of \autoref{fig:simple-lisa-proof-graph} in LISA. Each step is assigned an index, import are represented with negative indices. The indentation corresponds to the level of the proof: subproofs are indented further down. The second column states what rule is used, along with the premises it relies upon. The third column is the conclusion of that step. The last column contains parameters to disambiguate the application of the rule.}
+  \caption[Proof in LISA]{A representation of the proof of \autoref{fig:simple-lisa-proof-graph} in LISA. Each step is assigned an index, and import are represented with negative indices. Scoping within the proof is possible and determined by the indentation level: subproofs are indented further down. The second column states what rule is used, along with the premises it uses. The third column is the conclusion of that step. The last column contains parameters to disambiguate the application of the rule.}
   \label{fig:simple-lisa-proof}
 \end{figure}
 
-A proof in this system is a directed acyclic graph of proof steps. Each such step corresponds to the application of an inference rule, and is characterized by its conclusion expressed as a sequent, and some premises. A sequent is a pair of sets of formulas, noted $\phi_1, \phi_2, ..., \phi_n \vdash \psi_1, \psi_2, ..., \psi_m$ or $\Gamma \vdash \Delta$, and can be interpreted in conventional logic as a conjunction of premises implying a disjunction of conclusions. That said, the actual semantic is controlled by the inference rules provided by the system. Proofs can optionally have ``imports'', sequents that can be used as premises, and proofs may also be nested for organization purposes. Figures \ref{fig:simple-lisa-proof-graph} and \ref{fig:simple-lisa-proof} showcase a formal proof in LISA along with its linear representation. Notice that a directed acyclic graph can always be represented in a linear fashion, but not necessarily as a tree (without having to inline leaves).
+A proof in this system is a directed acyclic graph of proof steps. Each such step corresponds to the application of an inference rule, and is characterized by its conclusion expressed as a sequent, and some premises. A sequent is a pair of sets of formulas, noted $\phi_1, \phi_2, ..., \phi_n \vdash \psi_1, \psi_2, ..., \psi_m$ or $\Gamma \vdash \Delta$, and can be interpreted in conventional logic as a conjunction of premises implying a disjunction of conclusions. That said, the actual semantic is controlled by the inference rules provided by the system. Proofs can optionally have ``imports'', sequents that can be used as premises, and proofs may also be nested for organization purposes. Figures \ref{fig:simple-lisa-proof-graph} and \ref{fig:simple-lisa-proof} showcase a formal proof in LISA. Notice that a directed acyclic graph can always be represented in a linear fashion, but not necessarily as a tree (unless we duplicate forward edges).
 
 Currently LISA only exists as a Scala library, therefore the proofs are described using Scala code. For further technical details about LISA, we refer the reader to the official manual \cite{Guilloud2022-2}.

thesis/report/chapters/2-background.tex

@@ -1,18 +1,18 @@
 \section{Background}
 \label{sec:background}
 
-Attempts at formalizing logic and mathematics are numerous, and one can observe that successful systems are often the result of an iterative process \cite{Paulson2019, Harrison2014, Asperti2007}. In this section we describe the history of proof assistants, and we present my past contributions to the field.
+Attempts at formalizing logic and mathematics are numerous, and one can observe that successful systems are often the result of an iterative process \cite{Paulson2019, Harrison2014, Asperti2007}. In this section we describe the history of proof assistants, and we present our past contributions to the field.
 
 \subsection{Overview}
 
-Historically, proof assistants focused mainly on automating the process of demonstrating assertions rather than providing tools to assist the user in doing so; which is objectively a simpler task \cite{Harrison2014}. It is only later that designs have leaned towards user-centered systems with ideas such as the Edinburgh LCF, and subsequent work on metalogic and tactics \cite{Milner1984}. Usability gradually improved, as progress was made in the areas of higher-order logic, type systems and unification \cite{Paulson2019}. The proof assistants that are currently available vary in designs, however different systems often share a set of similar features. Coq and Isabelle/HOL are two examples of widely adopted systems that have a vast repertoire of proven theorems \cite{Yushkovskiy2018}. Both support forward and backward reasoning, and are expressive enough to write procedures such as tactics. Their main differences boil down to the underlying theory and the implementation of their kernel \cite{Barras1999, Wenzel2021}. Coq is based on the calculus of constructions, while Isabelle/HOL relies on higher-order logic.
+Historically, proof assistants consisted mainly on automating the process of demonstrating assertions rather than providing tools to assist the user in doing so; which is objectively a simpler task \cite{Harrison2014}. It is only later that designs have leaned towards user-centered systems with ideas such as the Edinburgh LCF, and subsequent work on metalogic and tactics \cite{Milner1984}. Usability gradually improved, as progress was made in the areas of higher-order logic, type systems and unification \cite{Paulson2019}. The proof assistants that are currently available vary in designs, however different systems often share a set of similar features. Coq and Isabelle/HOL are two examples of widely adopted systems that have a vast repertoire of proven theorems \cite{Yushkovskiy2018}. Both support forward and backward reasoning, and are expressive enough to write procedures such as tactics. Their main differences boil down to the underlying theory and the implementation of their verifier \cite{Barras1999, Wenzel2021}: Coq is based on the calculus of constructions, while Isabelle/HOL relies on higher-order logic.
 
-\subsection{LCF-like framework}
+\subsection{LCF-style framework}
 
-In 2020 I worked on designing a LCF-like framework in Scala that used the Von Neumann-Bernays-Gödel set theory (NBG) as a foundation \cite{Cassayre2020} and attempted to formalize the proofs displayed in a logic textbook \cite{Mendelson2015}. This project allowed me to explore different areas in theorem proving such as the representation of proofs and tableaux solving strategies. One of the particularity of that framework was that formulas and more generally theorems were strongly typed. In the lines of the Curry-Howard Correspondence, this meant that the soundness could be enforced by the type checker alone. Naturally this feature gets in the way when working with higher-order rules (e.g. induction) and automated strategies (e.g. tableaux). It also demonstrated that the LCF style restricted the expressiveness of proofs, and that to provide more flexibility an extra layer would be needed.
+In 2020 I worked on designing a LCF-style framework in Scala that used the Von Neumann-Bernays-Gödel set theory (NBG) as a foundation \cite{Cassayre2020} and attempted to formalize the proofs displayed in a logic textbook \cite{Mendelson2015}. This project allowed me to explore different areas of formal methods and theorem proving such as the representation of proofs and tableaux solving strategies. One of the particularities of that framework was that formulas---and more generally theorems were strongly typed. In the lines of the Curry-Howard Correspondence, this meant that soundness could be enforced by the type checker alone. Unavoidably, this feature gets in the way when working with higher-order rules (e.g. induction) and automated strategies (e.g. tableaux). It also demonstrated that the raw LCF-style restricted the expressiveness of proofs, and that to provide more flexibility an extra layer would be needed.
 
 LISA uses the Zermelo-Fraenkel set theory (ZF, and more specifically ZFC) instead of NBG. Both axiomatizations are similar, the main difference being that NBG makes the distinction between sets and proper classes. NBG has been (independently) proven to be a conservative extension of ZFC, meaning that neither is stronger than the other. Furthermore, LISA uses sequent calculus in its deductive system, while that framework had formulas as first-class citizens.
 
 \subsection{LISA}
 
-Before starting this thesis I contributed to the design of LISA late 2021, notably by maintaining the codebase, reviewing and testing the proof checker, and exploring the design of third-party tools for LISA. This LISA project then ramified itself into several sub-projects, including this very thesis. The topic of projects lead by other persons include: formalization of other theories such as Peano's arithmetic, proof space exploration using deep learning methods, and interoperability with other tools, for example Stainless \cite{Kuncak2021}. During the period of the thesis I continued to occasionally work on LISA as it continued its maturation process. Some components and ideas designed in this front-end framework were integrated in LISA, and eventually the full framework strives to become a module of LISA.
+Late 2021 before starting working on this thesis, I contributed to the design of LISA, notably by maintaining the codebase, reviewing and testing the proof checker, and exploring the design of third-party tools for LISA. This LISA project then ramified itself into several sub-projects, including this very thesis. The topic of projects lead by other persons include: formalization of other theories such as Peano's arithmetic, proof space exploration using deep learning methods, translation of natural language sentences into formal statements, and interoperability with other tools, for example Stainless \cite{Kuncak2021}. During the period of the thesis I continued to occasionally work on LISA as it proceeded further in its maturation process. Some components and ideas designed in this front-end framework were integrated in LISA. Eventually we are aiming to integrate the full framework proposed in this thesis as a module of LISA.