# Changeset 3619 for Papers/jar-cerco-2017/introduction.tex

Ignore:
Timestamp:
Mar 6, 2017, 4:02:43 PM (3 years ago)
Message:

Added section on Matita

File:
1 edited

### Legend:

Unmodified
 r3618 \newcommand{\All}[1]{\forall{#1}.\;} \newcommand{\lam}[1]{\lambda{#1}.\;} % Introduction %   Problem being solved, background, etc. \subsection{Introduction to Matita} The theorem prover used to implement and verify the prototype compiler is Matita~\cite{matita}. Matita, like Coq, is based on the Calculus of (Co)Inductive Constructions. Its main features are: Matita is a theorem prover based on a variant of the Calculus of Coinductive Constructions~\cite{asperti:user:2007}. The system features a full spectrum of dependent types and (co)inductive families, a system of coercions, a tactic-driven proof construction engine~\cite{sacerdoti-coen:tinycals:2007}, and paramodulation based automation~\cite{asperti:higher-order:2007}, all of which we exploit in the formalisation described herein. Matita's syntax is similar to the syntaxes of mainstream functional programming languages such as OCaml or Standard ML. The type theory that Matita implements is broadly akin to that of Coq~\cite{coq:2004} and Agda~\cite{bove:brief:2009}. Nevertheless, we provide a brief explanation of the main syntactic and type-theoretic features of Matita that will be needed to follow the body of the paper: \begin{itemize} \item A bidirectional type inference algorithm, which combines usage of inferred and expected types. The type inference algorithm also uses a hints system that helps with unification; \item A disambiguation system that allows for notation overloading by having the parser and typechecker cooperate closely. \item Non-recursive functions and definitions are introduced via the \texttt{definition} keyword. Recursive functions are introduced with \texttt{let rec}. Mutually recursive functions are separated via the \texttt{and} keyword. Matita's termination checker ensures that all recursive functions are terminating before being admitted to maintain soundness of the system's logic. \item Matita has an infinite hierarchy of type universes. A single impredicative universe of types, \texttt{Prop}, exists at the base of this hierarchy. An infinite series of predicative universes, \texttt{Type[0]} : \texttt{Type[1]} : \texttt{Type[2]}, and so on and so forth, sits atop \texttt{Prop}. Matita, unlike Coq or Agda, implements no form of typical ambiguity or universe polymorphism, with explicit concrete universe levels being preferred instead. \item Matita's type theory plays host to a rich and expressive higher-order logic. Constants \texttt{True} and \texttt{False} represent truth and falsity in \texttt{Prop} respectively. Two inductive families in \texttt{Prop} encode conjunction and disjunction---$\mathtt{P \wedge Q}$ and $\mathtt{P \vee Q}$ respectively. As is usual, implication and universal quantification are identified with the dependent function space ($\Pi$ types), whereas (constructive) existential quantification is encoded as a dependent sum (a $\Sigma$-type). We write $\All{x : \phi}\psi$ for the dependent function space, and abbreviate this as $\phi \rightarrow \psi$ when $x \not\in fv(\psi)$ as usual. We use $\langle M,N \rangle$ for the pairing of $M$ and $N$. \item Inductive and coinductive families are introduced via the \texttt{inductive} and \texttt{coinductive} keywords respectively, with named constructor declarations separated by a bar. Mutually inductive data family declarations are separated via \texttt{with}. In the following declaration: \begin{lstlisting}[language=Grafite] inductive I ($P_1$ : $\tau_1$) $\ldots$ ($P_n$ : $\tau_n$) : $\phi_1 \rightarrow \ldots \rightarrow \phi_m \rightarrow \phi$ := $\ldots$ \end{lstlisting} We call $P_i$ for $0 \leq i \leq n$ the \textbf{parameters} of \texttt{I} and $\phi_j$ for $0 \leq j \leq m$ the \textbf{indices} of \texttt{I}. Matita's positivity checker ensures that constructors have strictly-positive types before admitting an inductive family to maintain soundness of the system's logic. \item Records are introduced with the \texttt{record} keyword. A Matita record \begin{lstlisting}[language=Grafite] record R : Type[0] := { F1 : nat }. \end{lstlisting} may be thought of as syntactic sugar for a single-constructor inductive data type of the same name: \begin{lstlisting}[language=Grafite] inductive R : Type[0] := | mk_R : nat -> R. \end{lstlisting} A record field's type may depend on fields declared earlier in the record. Records may be decomposed with projections. Projections, one for each of field of a record, are registered in the global context. In the example record above, \texttt{F1} of type $R \rightarrow nat$ is registered as a field projection and $mk\_R$ of type $nat \rightarrow R$ is registered as a constructor. Record fields may also be marked as coercions. In the following example \begin{lstlisting}[language=Grafite] record S : Type[1] := { Carrier :> Type[0]; op : Carrier -> Carrier -> Carrier } \end{lstlisting} the field \texttt{Carrier} is declared to be a coercion with \texttt{:>}'.with the operational effect being that the field projection \texttt{Carrier} may be omitted where it could be successfully inferred by Matita. Field coercions facilitate the informal but common mathematical practice of intentionally confusing a structure with its underlying carrier set. \item Terms may be freely omitted, allowing the user to write down partial types and terms. A question mark, \texttt{?}, denotes a single term that has been omitted by the user. Some omitted terms can be deduced by Matita's refinement system. Other, more complex goals arising from omitted terms may require user input to solve, in which case a proof obligation is opened for each term that cannot be deduced automatically. Three consecutive dots, \texttt{$\ldots$}, denote multiple terms or types that have been omitted. \item Data may be decomposed by pattern matching with a \texttt{match} expression. We may fully annotate a \texttt{match} expression with its return type. This is especially useful when working with indexed families of types or with invariants, expressed as types, on functions. In the following \begin{lstlisting}[language=Grafite] match t return $\lam{x}x = 0 \rightarrow bool$ with [ 0    $\Rightarrow$ $\lam{prf_1}P_1$ | S m $\Rightarrow$ $\lam{prf_2}P_2$ ] (refl $\ldots$ t) \end{lstlisting} the \texttt{0} branch of the \texttt{match} expression returns a function from $0 = 0$ to \texttt{bool}, whereas the \texttt{S m} branch of the \texttt{match} expression returns a function from \texttt{S m = 0} to \texttt{bool}. In both cases the annotated return type $\lam{x}x = 0 \rightarrow bool$ has been specialised given new information about \texttt{t} revealed by the act of pattern matching. The entire term, with \texttt{match} expression applied to \texttt{refl $\ldots$ t}, has type \texttt{bool}. \item Matita features a liberal system of coercions (distinct from the previously mentioned record field coercions). It is possible to define a uniform coercion $\lam{x}\langle x, ?\rangle$ from every type $T$ to the dependent product $\Sigma{x : T}. P x$. The coercion opens a proof obligation that asks the user to prove that $P$ holds for $x$. When a coercion is to be applied to a complex term (for example, a $\lambda$-abstraction, a local definition, or a case analysis), the system automatically propagates the coercion to the sub-terms. For instance, to apply a coercion to force $\lam{x}M : A \rightarrow B$ to have type $\All{x : A}\Sigma{y : B}. P x y$, the system looks for a coercion from $M : B$ to $\Sigma{y : B}. P x y$ in a context augmented with $x : A$. This is significant when the coercion opens a proof obligation, as the user will be presented with multiple, but simpler proof obligations in the correct context. In this way, Matita supports the Russell' proof methodology developed by Sozeau in~\cite{sozeau:subset:2007}, in a lightweight but tightly-integrated manner. \end{itemize} Throughout, for reasons of clarity, conciseness, and readability, we may choose to simplify or omit parts of Matita code. We will always ensure that these omissions do not mislead the reader. \subsection{Map of the paper} some of the case studies we have performed to validate it. Finally, in section~\ref{sect:conclusions} we present conclusions, as well as Finally, in section~\ref{sect.conclusions} we present conclusions, as well as related and future work.