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

Added section on Matita

1 edited


  • Papers/jar-cerco-2017/introduction.tex

    r3618 r3619  
    14% Introduction
    25%   Problem being solved, background, etc.
    273276\subsection{Introduction to Matita}
    275 The theorem prover used to implement and verify the prototype compiler is
    276 Matita~\cite{matita}.
    278 Matita, like Coq, is based on the Calculus of (Co)Inductive Constructions. Its
    279 main features are:
     278Matita is a theorem prover based on a variant of the Calculus of Coinductive Constructions~\cite{asperti:user:2007}.
     279The 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.
     281Matita's syntax is similar to the syntaxes of mainstream functional programming languages such as OCaml or Standard ML.
     282The type theory that Matita implements is broadly akin to that of Coq~\cite{coq:2004} and Agda~\cite{bove:brief:2009}.
     283Nevertheless, 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:
    282         \item A bidirectional type inference algorithm, which combines usage of
    283         inferred and expected types. The type inference algorithm also uses a hints
    284         system that helps with unification;
    285         \item A disambiguation system that allows for notation overloading by having
    286         the parser and typechecker cooperate closely.
     286Non-recursive functions and definitions are introduced via the \texttt{definition} keyword.
     287Recursive functions are introduced with \texttt{let rec}.
     288Mutually recursive functions are separated via the \texttt{and} keyword.
     289Matita's termination checker ensures that all recursive functions are terminating before being admitted to maintain soundness of the system's logic.
     291Matita has an infinite hierarchy of type universes.
     292A single impredicative universe of types, \texttt{Prop}, exists at the base of this hierarchy.
     293An infinite series of predicative universes, \texttt{Type[0]} : \texttt{Type[1]} : \texttt{Type[2]}, and so on and so forth, sits atop \texttt{Prop}.
     294Matita, unlike Coq or Agda, implements no form of typical ambiguity or universe polymorphism, with explicit concrete universe levels being preferred instead.
     296Matita's type theory plays host to a rich and expressive higher-order logic.
     297Constants \texttt{True} and \texttt{False} represent truth and falsity in \texttt{Prop} respectively.
     298Two inductive families in \texttt{Prop} encode conjunction and disjunction---$\mathtt{P \wedge Q}$ and $\mathtt{P \vee Q}$ respectively.
     300As 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).
     301We 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.
     302We use $\langle M,N \rangle$ for the pairing of $M$ and $N$.
     304Inductive and coinductive families are introduced via the \texttt{inductive} and \texttt{coinductive} keywords respectively, with named constructor declarations separated by a bar.
     305Mutually inductive data family declarations are separated via \texttt{with}.
     306In the following declaration:
     308inductive I ($P_1$ : $\tau_1$) $\ldots$ ($P_n$ : $\tau_n$) : $\phi_1 \rightarrow \ldots \rightarrow \phi_m \rightarrow \phi$ := $\ldots$
     310We 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}.
     311Matita's positivity checker ensures that constructors have strictly-positive types before admitting an inductive family to maintain soundness of the system's logic.
     313Records are introduced with the \texttt{record} keyword.
     314A Matita record
     316record R : Type[0] := { F1 : nat }.
     318may be thought of as syntactic sugar for a single-constructor inductive data type of the same name:
     320inductive R : Type[0] :=
     321  | mk_R : nat -> R.
     323A record field's type may depend on fields declared earlier in the record.
     325Records may be decomposed with projections.
     326Projections, one for each of field of a record, are registered in the global context.
     327In 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.
     329Record fields may also be marked as coercions.
     330In the following example
     332record S : Type[1] :=
     334  Carrier :> Type[0];
     335  op : Carrier -> Carrier -> Carrier
     338the 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.
     339Field coercions facilitate the informal but common mathematical practice of intentionally confusing a structure with its underlying carrier set.
     341Terms may be freely omitted, allowing the user to write down partial types and terms.
     342A question mark, \texttt{?}, denotes a single term that has been omitted by the user.
     343Some omitted terms can be deduced by Matita's refinement system.
     344Other, 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.
     345Three consecutive dots, \texttt{$\ldots$}, denote multiple terms or types that have been omitted.
     347Data may be decomposed by pattern matching with a \texttt{match} expression.
     348We may fully annotate a \texttt{match} expression with its return type.
     349This is especially useful when working with indexed families of types or with invariants, expressed as types, on functions.
     350In the following
     352match t return $\lam{x}x = 0 \rightarrow bool$ with
     353[ 0    $\Rightarrow$ $\lam{prf_1}P_1$
     354| S m $\Rightarrow$ $\lam{prf_2}P_2$
     355] (refl $\ldots$ t)
     357the \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}.
     358In 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.
     359The entire term, with \texttt{match} expression applied to \texttt{refl $\ldots$ t}, has type \texttt{bool}.
     361Matita features a liberal system of coercions (distinct from the previously mentioned record field coercions).
     362It 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$.
     363The coercion opens a proof obligation that asks the user to prove that $P$ holds for $x$.
     364When 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.
     365For instance, to apply a coercion to force $\lam{x}M : A \rightarrow B$ to
     366have 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$.
     367This 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.
     368In this way, Matita supports the `Russell' proof methodology developed by Sozeau in~\cite{sozeau:subset:2007}, in a lightweight but tightly-integrated manner.
     370Throughout, for reasons of clarity, conciseness, and readability, we may choose to simplify or omit parts of Matita code.
     371We will always ensure that these omissions do not mislead the reader.
    289373\subsection{Map of the paper}
    305389some of the case studies we have performed to validate it.
    307 Finally, in section~\ref{sect:conclusions} we present conclusions, as well as
     391Finally, in section~\ref{sect.conclusions} we present conclusions, as well as
    308392related and future work.
Note: See TracChangeset for help on using the changeset viewer.