related_work.tex

\chapter{Related Work}
\label{ch:relatedwork}

Theorem provers have developed different techniques for developing the algebraic hierarchy. We discuss them in Section~\ref{sec:relwork:hierarchy}. In~\ref{sec:relwork:automation} we present the current support for automation provided by theorem provers. 
A language with strong reflection mechanisms can be extended to support the generative approach we discuss here. We discuss reflection mechanisms in theorem provers in Section~\ref{sec:relwork:reflectionTPs}. 
%We discuss theory and proof development automation in Section~\ref{sec:relwork:genDefs} and the efforts to export definitions and proofs between systems in Section~\ref{sec:relwork:exporting}.  

\section{Formalizing the algebraic hierarchy}
\label{sec:relwork:hierarchy}
The algebraic hierarchy is a main part of the libraries of theorem provers. Several efforts has been dedicated to organize them in a way that reflects their mathematical structure. 

Many formalizations depends on the unification algorithm to figure out the connections between the different theories in the hierarchy. 
The simplest way is to use inclusions to describe inheritance between two structures. This is used in~\cite{Geuvers2002} where algebraic structures are presented as dependent records and user provided coercions are used to guide the unification algorithm. The hierarchy developed using this approach has been used to prove the fundamental theorem of algebra. As has been noted by the authors, this technique does not support multiple inheritance, so there is no way to describe that a ring is both a monoid and an abelian group. 
%Multiple inheritance is important to capture the structure of mathematics. 
%Various techniques have been developed to incorporate multiple inheritance. 
Canonical structures~\cite{canonical2013} is a mechanism for programming the type inference, originally introduced to handle overloading of symbols. It has been used to enable multiple inheritance in the development of the mathematical components library~\cite{mathCompBook2020} which has been used in the proof of the odd order (Feit-Thompson) theorem~\cite{gonthier2013oddOrderTheorem}. 
% Canonical mul_monoid := Monoid.Law mulrA mul1r mulr1. 
Another approach to building the algebraic hierarchy in Coq is using packed classes~\cite{Gonthier2009} which mainly solves the problem of multiple inheritance. This approach has been extended in~\cite{cohen2020hierarchy} and~\cite{sakaguchi2020validating} to overcome the complexity of using it to build and maintain the hierarchy. \cite{cohen2020hierarchy} creates an ELPI~\cite{elpi,elpiForCoq} plugin to Coq introducing a language for building the algebraic hierarchy whose expressions are elaborated into packed classes. One of the merits of this language is that the hierarchy can change without breaking users' code, i.e. it makes it possible to add new structures and connections between them, while keeping the older ones. \cite{sakaguchi2020validating} provides invariants and algorithms to validate the structure of the library.  
Type classes has been used to build the algebraic hierarchy in Coq and Lean. In Coq~\cite{spitters2011type}, type class $A$ extends type class $B$ by having $B$ become a field of $A$. The unification algorithm is guided by using \verb|:>| symbol instead of \verb|:| when declaring the type. Multiple inheritance is therefore possible. Lean~\cite{lean2019}, on the other hand, provide an \verb|extends| operation through which one can state all the predecessors of a class. Lean also provide \verb|attributes| that enables describing other ways in which structure connect to each other. For example, the \verb|to_additive| attribute describes that one class is the additive version of another.

Depending on unification to infer connections between theories restricts the ways in which they can be connected. 
%These different techniques restrict the morphisms between theories to the identity. Even in the case of a rename, it is performed first and then the inclusion happens. In some cases it is not clear whether there is actually a rename morphisms between the two versions of the theory or not. 
Therefore, some systems allow general morphisms, as explained in Section~\ref{sec:background:morphisms}, which are capable of describing more complex relations between theories. Many specification systems~\cite{Goguen1980, CoFI:2004:CASL-RM, Smith99, duran2007maude} allow user provided general morphisms. They mostly refer to them as \emph{views}. It is common for these systems to provide combinators to build new theories by reusing older ones. In the theorem proving world, Isabelle provides locale interpretations~\cite{localeIntepretations2006}, IMPS provides theory interpretations~\cite{farmer1993imps}, and MMT provides morphisms~\cite{rabe2013scalable}. Neither IMPS nor MMT provides combinators, which makes it hard to build libraries of hundreds of theories, as the library developer needs to provide all theories and morphisms manually. Isabelle provide locale expressions~\cite{ballarin2003locales}, which are combinators to build locales and locale intepretations. However its \lstmath{combine} operator is based on same-name-same-thing principle, which has limitations that we discussed in Section~\ref{sec:thry_graph_in_action}. 

%The approach introduced in~\cite{carette2018building} supports general morphisms, via the \lstmath{mixin} combinator. Our implementation does not support them. It still allows describing names-to-names mappings, via \lstmath{rename}, which makes it more powerful than the ones that only support identity morphisms. 


%, packed classes are suggested to solve the multiple inheritance and the packaging problems\ednote{check the pakaging one}. They are used to define the algebraic hierarchy as part of the proof for Thompson-Feit theorem. Despite this improvement, packed classes need Both~\cite{cohen2020hierarchy} and~\cite{sakaguchi2020validating} criticize packed classes for the complexity of using them to build a hierarchy, as well as the complexity of maintaining a hierarchy build with them. 

%Canonical structures are used to build the algebraic hierarchy as part of the odd order theorem proof~\cite{canonical2013}. The approach is to provide unification hints for the type inference algorithms that makes it build the connection between abstract theories, or between abstract theories and their instances. 

%In~\cite{Gonthier2009} an algebraic hierarchy is developed as part of the project to formalize the proof of the Thompson-Feit theorem. Unsatisfied with telescopes and canonical structures, the author suggests packed classes to solve the problems of multiple inheritance and the coercion chain problem. The work is criticised by \cite{cohen2020hierarchy} for being complex, needs to be a coq expert to use it, and for not being robust to small changes in the hierarchy like decomposing a structure into two simpler ones. \cite{cohen2020hierarchy} builds on packed classes by providing an ELPI plugin to coq to build and maintain the algebraic hierarchy called hierarchy builder $\mathcal{HB}$. The declarations of algebraic structures written in $\mathcal{HB}$ is then elaborated into packed classes. Also~\cite{sakaguchi2020validating} also says that using packed classes needs expertize in Coq and its hard maintenance. 

%Another algebraic hierarchy is developed in~\cite{Geuvers2002} as part of the proof for the fundamental theorem of algebra. This hierarchy favors the use of dependent records, depending on coercions to guide the unification algorithm of Coq to infer connections between structures. 
%The inferred connections are mostly inclusions, what MMT would call implicit morphisms. Using only dependent records, the paper admits it is not possible to represent multiple inheritance, like the case that a ring has two monoids, one additive and one multiplicative. 

%In~\cite{spitters2011type}, type classes are used to represent algebraic structures. Inheritance is described as record fields, so a semiring would have two fields for monoids to describe that it contains two monoids. A special symbol $:>$ is used to guide the instance resolution algorithm, building the hierarchy. 

% --- lean --> type classes 

%The lean mathematical library is described in~\cite{lean2019}. The library focuses on classical mathematics, with an algebra library containing $2794$ declarations. The library uses type classes to capture the structure of mathematics. By providing type class constraints, the diamond structure can be presented. The choices for bundling is similar to ours, the carrier is a parameter to the type class, all other declarations are bundles. For morphisms, the source and target are arguments, with all other declarations being bundled, mainly to provide a better descriptive definition of composition. 

\begin{comment}
% --- Mizar --> attributed types 
\cite{Grabowski2020} agrees with us that current formalizations of the algebraic hierarchy are not general enough to serve multiple projects, and that they are usually created with specific formalization in mind. It presents the mizar approach to building the algebraic hierarchy in a way that captures their mathematical structure and facilitates the transfer of results between them. In mizar, a signature is defined as a structure. An example taken from~\cite{schwarzweller2007mizar} 
\begin{lstlisting}
definition 
struct (ZeroStr) LoopStr
(# carrier -> set,
add -> BinOp of the carrier,
Zero -> Element of the carrier #);
end;
\end{lstlisting}
Multiple inheritance between structures (signatures) is possible. \cite{Grabowski2020} gives the signature of rings and fields as follows 
\begin{lstlisting}
definition struct (addLoopStr, multLoopStr_0) doubleLoopStr
(# carrier -> set,
addF -> BinOp of the carrier,
multF -> BinOp of the carrier,
OneF -> Element of the carrier, 
ZeroF -> Element of the carrier
#);
end;
\end{lstlisting}
It is not clear how this inheritance works, as all declarations are repeated in the body of the struct. 
Axioms (properties) are added as attributes, as follows~\cite{schwarzweller2007mizar}
\begin{lstlisting}[mathescape]
definition 
let L be non empty LoopStr;
attr L is add-associative means
for x,y,z being Element of L holds (x + y) + z = x + (y + z);
$\cdots$
end;  
\end{lstlisting}
An algebraic structure is defined as an existential registration 
\begin{lstlisting}
definition 
mode Group is add-associative right_zeroed right_complementable
(non empty LoopStr);
end;
\end{lstlisting} 
\end{comment}

\section{Automation in Theorem Provers}
\label{sec:relwork:automation}

%\subsection{Generating Definitions}
%\label{sec:relwork:genDefs}
\paragraph{Automatic Generation of Information}
Although universal algebra constructions have been formalized in type theory~\cite{capretta99, Gunther2018Agda}, we did not encounter any big efforts to automate the generations of its constructions, like we do in this work. In this section we discuss the limited efforts for generating information that we encountered in the literature. 

Coq generates the induction principle for inductive types. Equality functions can also be generated using \verb|Scheme Equality| command. Coq's approach for generating them is criticized in~\cite{coqDeriveEquality2019}. In the cases when the inductive type uses a container, the generated principle does not require that the predicate holds for elements of the container. Equality cannot be generated in these cases. 
~\cite{coqDeriveEquality2019} presents a Coq-ELPI plugin that generates equality tests and proofs for inductive types. In~\cite{coqDeriveSubterm2020}, MetaCoq is used to define equality and subterm relations.
\cite{inversPrincp1996Coq} suggests the inversion principle can also be generated for inductive types.
%\ednote{also talk about the report: Adding support for induction in Dedukti} 

%checked, not very relevant\ednote{check this paper: A Certified Multi-prover Verification Condition Generator}
A common form of automation in theorem provers is using hammers for proving lemmas. The idea is to search a library for premises that are useful to prove the given lemma and construct the proof accordingly. It is reported that hammers can automatically find proofs for $40\%$ of the Mizar library and close results in HOL systems~\cite{blanchette2016hammering}. The hammer technique is extended to Coq in~\cite{czajka2018hammer}. 

\paragraph{Automatic Exporting between Theorem Provers}
%\subsection{Translation / Exporting Between Systems}
%\label{sec:relwork:exporting}
Several translations between libraries of formal proofs has been done~\cite{impsToOmdoc2018, mizarToIsabelle2018, iancu2013mizar}. In~\cite{kaliszyk2019DeclProofTerms}, declarative proof outlines are exported from Mizar to Isabelle/Isar. 
The work in~\cite{Muller2017alignment} share our motivation of contributing to building large libraries of mathematics. The idea is to provide concept alignment between different theorem provers. We can see this approach useful as we expand our exporter to support different systems with different underlying foundations.  

Code generation from theorem provers into one or more programming languages has also been discussed in the literature. Both Coq~\cite{CoqCodegen2003, cruz2003program} and Isabelle~\cite{IsabelleCodegen2010} provides code extraction mechanisms from their theories and proofs into functional programs. 

Logipedia~\cite{Dowek2019LogipediaAM} exports proofs written in the logical framework Dedukti to multiple theorem provers. The supported targets are Coq, Lean, Matita, OpenTheory, HOL-Light, and PVS. 
Lem~\cite{lem2014} exports specifications to a programming language (OCaml), multiple theorem provers (Coq, HOL4, Isabelle/HOL), Latex and HTML. 

Another interesting work is the interface between Lean, a theorem prover, and Mathematica, a computer algebra system~\cite{Lewis_2017} which allows exchange of information between the two systems in both directions.  

%Automating Test Case Generation from Z Specifications with Isabelle
%\url{file:///Users/Yasmine/Downloads/Helke1997_Chapter_AutomatingTestCaseGenerationFr.pdf}

%A Proof Strategy Language and Proof Script Generation for Isabelle/HOL: 
%\url{https://link.springer.com/chapter/10.1007/978-3-319-63046-5_32}

\paragraph{Automation in Programming Languages (PL)}
Eliminating boilerplate is a main field of research in the PL community, either by providing abstractions that eliminates the need for the boilerplate code as in the scrap your boilerplate approach~\cite{syb2003Jones} or by generating this boilerplate for the users.  

We have already mentioned deriving and its extensions~\cite{loeh2010genericDeriving, loeh2018derivingVia}, and lenses~\cite{lensesLib}. Those techniques are pervasively used in Haskell projects.
OCaml provides the PPX preprocessor that manipulates the OCaml AST corresponding to an input program~\cite{ocaml2019ppx}. One form in which PPX transforms OCaml programs is using derivers that allow writing a deriving definition as in Haskell. 
Macros, which are provided by multiple programming languages can also be seen as a form of code generation with one application being removing boilerplate. The work in~\cite{macros2001msp} presents a typed macro system that can be used to develop domain specific languages. 


\section{Reflection Mechanisms in Theorem Provers}
\label{sec:relwork:reflectionTPs}

%\todo{A meta programming framwork for formal verification (automation in lean)}
%\todo{Agda reflection mechanism: check related work in~\cite{brady2016reflection}}
%\todo{Coq Ltac, Mtac, MetaCoq, SSReflect} 

Both Idris~\cite{brady2016reflection} and Lean~\cite{lean2017metaprogramming} provides meta programming facilities that are very similar.
In case of Idris, the meta programming API provides tactics to query and manipulate proof states in the core language TT. Lean uses the same philosophy, but instead of a core language, the tactics are based on C++ procedures. 
In both cases, declarations in the environment can be queried and the environment can be extended by adding new definitions. 
This makes them convenient to generating definitions as we do in this work. Despite that, we find that all discussions and examples are dedicated to constructing proof terms. The realization that they can be used to provide definitions does not seem dominant, with the exception of using Idris reflection to provide instances of Idris type classes \lstmath{Eq} and \lstmath{Show}. 
Another problem is that the generated definitions are part of the environment, but are not reflected back in the language of Idris or Lean. This makes it hard to consider them part of a library. 

Agda also has a reflection mechanism~\cite{van2012reflection}. A serious limitation is that the only top level declaration that can be generated are functions~\cite{agdaReflection}. 
Coq's Mtac is a meta language for constructing tactics that generate proof terms. MetaCoq~\cite{templateCoq2018} is a more general way for supporting meta programming in Coq by reflecting its kernel. Similar to Idris and Lean, the meta programming facilities in Coq has not been applied to the problem of eliminating boilerplate, although it's been hinted at as a possible application area in~\cite{templateCoq2018}. 

%Idris uses a tactic-based elaborator to compile Idris high level language into a core language, which is then type-checked. The elaborator keeps a proof state.  
%elaboration reflection~\cite{brady2016reflection} extends the tactic language by providing tactics that to manipulate or query the proof state. Using these tactics it is possible to write Idris code that instructs the elaborator to generate code in the core language. Functions and datatypes can also be generated and added to the environment. 

%The Lean supports meta programming by exposing an API for the procedures implemented in C++. Metaprogramming in Lean~\cite{lean2017metaprogramming} is performed by writing a tactic script that manipulates the tactic state to produce expressions. and elaboration is similar to Idris in the sense that 
\begin{comment}
Coq allows user-defined tactics using OCaml or Ltac (a high-level language for defining tactics). Both can generate ill-typed expressions. 
Mtac performs code generation within the M monad. they all provide tactics that produces proof terms. 
Template coq~\cite{templateCoq2018} has a more general approach that reflects the syntax of the calculus of inductive constructions as implemented by Coq. It still does not concern itself with generating definitions for managing boilerplate. 

- coq proofs ultimately compile to proof terms on the language of the type theory 
- tactics provide support to developing proof terms by applying tactics 
- 
\end{comment}



\begin{comment}
Data type generic programming (DGP) \cite{Gibbons2007DGP} abstracts over the details of data types and focus on representing its structure. There are different approaches to DGP, surveyed in \cite{hinze2007comparing}. One approach is to map a data type to a structure representation type, that only represents information about the structure. For example a type  $\alpha :+: \beta$ represents the structure of a data type with two data constructors. This approach is followed by generic Haskell \cite{Hinze2003GenericHs} and PolyP \cite{Jansson1997PolyP}. 
Another approach uses reflection, as in DrIFT \cite{winstanley1997type} and template Haskell \cite{Norell2004TemplateHs}. DrIFT extracts type declarations and directives to fire rules that generate code at compile time. Template Haskell allows meta programming within Haskell by providing access to the abstract syntax. This way, the structure of data types can be analyzed on the meta-level, and code can be generated according to that structure.\ednote{Q: this paragraph is taken from the proposal, which has not been published anywhere, do I need to rephrase it?}  
\todo{Prototyping Generic Programming in Template {H}askell}

https://kowainik.github.io/posts/deriving

https://typeclasses.com/ghc/stock-deriving-extensions
\end{comment}