Changeset 3619 for Papers/jarcerco2017/introduction.tex
 Timestamp:
 Mar 6, 2017, 4:02:43 PM (3 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/jarcerco2017/introduction.tex
r3618 r3619 1 \newcommand{\All}[1]{\forall{#1}.\;} 2 \newcommand{\lam}[1]{\lambda{#1}.\;} 3 1 4 % Introduction 2 5 % Problem being solved, background, etc. … … 273 276 \subsection{Introduction to Matita} 274 277 275 The theorem prover used to implement and verify the prototype compiler is 276 Matita~\cite{matita}. 277 278 Matita , like Coq, is based on the Calculus of (Co)Inductive Constructions. Its279 main features are: 280 278 Matita is a theorem prover based on a variant of the Calculus of Coinductive Constructions~\cite{asperti:user:2007}. 279 The system features a full spectrum of dependent types and (co)inductive families, a system of coercions, a tacticdriven proof construction engine~\cite{sacerdoticoen:tinycals:2007}, and paramodulation based automation~\cite{asperti:higherorder:2007}, all of which we exploit in the formalisation described herein. 280 281 Matita's syntax is similar to the syntaxes of mainstream functional programming languages such as OCaml or Standard ML. 282 The type theory that Matita implements is broadly akin to that of Coq~\cite{coq:2004} and Agda~\cite{bove:brief:2009}. 283 Nevertheless, we provide a brief explanation of the main syntactic and typetheoretic features of Matita that will be needed to follow the body of the paper: 281 284 \begin{itemize} 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. 285 \item 286 Nonrecursive functions and definitions are introduced via the \texttt{definition} keyword. 287 Recursive functions are introduced with \texttt{let rec}. 288 Mutually recursive functions are separated via the \texttt{and} keyword. 289 Matita's termination checker ensures that all recursive functions are terminating before being admitted to maintain soundness of the system's logic. 290 \item 291 Matita has an infinite hierarchy of type universes. 292 A single impredicative universe of types, \texttt{Prop}, exists at the base of this hierarchy. 293 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}. 294 Matita, unlike Coq or Agda, implements no form of typical ambiguity or universe polymorphism, with explicit concrete universe levels being preferred instead. 295 \item 296 Matita's type theory plays host to a rich and expressive higherorder logic. 297 Constants \texttt{True} and \texttt{False} represent truth and falsity in \texttt{Prop} respectively. 298 Two inductive families in \texttt{Prop} encode conjunction and disjunction$\mathtt{P \wedge Q}$ and $\mathtt{P \vee Q}$ respectively. 299 300 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). 301 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. 302 We use $\langle M,N \rangle$ for the pairing of $M$ and $N$. 303 \item 304 Inductive and coinductive families are introduced via the \texttt{inductive} and \texttt{coinductive} keywords respectively, with named constructor declarations separated by a bar. 305 Mutually inductive data family declarations are separated via \texttt{with}. 306 In the following declaration: 307 \begin{lstlisting}[language=Grafite] 308 inductive I ($P_1$ : $\tau_1$) $\ldots$ ($P_n$ : $\tau_n$) : $\phi_1 \rightarrow \ldots \rightarrow \phi_m \rightarrow \phi$ := $\ldots$ 309 \end{lstlisting} 310 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}. 311 Matita's positivity checker ensures that constructors have strictlypositive types before admitting an inductive family to maintain soundness of the system's logic. 312 \item 313 Records are introduced with the \texttt{record} keyword. 314 A Matita record 315 \begin{lstlisting}[language=Grafite] 316 record R : Type[0] := { F1 : nat }. 317 \end{lstlisting} 318 may be thought of as syntactic sugar for a singleconstructor inductive data type of the same name: 319 \begin{lstlisting}[language=Grafite] 320 inductive R : Type[0] := 321  mk_R : nat > R. 322 \end{lstlisting} 323 A record field's type may depend on fields declared earlier in the record. 324 325 Records may be decomposed with projections. 326 Projections, one for each of field of a record, are registered in the global context. 327 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. 328 329 Record fields may also be marked as coercions. 330 In the following example 331 \begin{lstlisting}[language=Grafite] 332 record S : Type[1] := 333 { 334 Carrier :> Type[0]; 335 op : Carrier > Carrier > Carrier 336 } 337 \end{lstlisting} 338 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. 339 Field coercions facilitate the informal but common mathematical practice of intentionally confusing a structure with its underlying carrier set. 340 \item 341 Terms may be freely omitted, allowing the user to write down partial types and terms. 342 A question mark, \texttt{?}, denotes a single term that has been omitted by the user. 343 Some omitted terms can be deduced by Matita's refinement system. 344 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. 345 Three consecutive dots, \texttt{$\ldots$}, denote multiple terms or types that have been omitted. 346 \item 347 Data may be decomposed by pattern matching with a \texttt{match} expression. 348 We may fully annotate a \texttt{match} expression with its return type. 349 This is especially useful when working with indexed families of types or with invariants, expressed as types, on functions. 350 In the following 351 \begin{lstlisting}[language=Grafite] 352 match 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) 356 \end{lstlisting} 357 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}. 358 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. 359 The entire term, with \texttt{match} expression applied to \texttt{refl $\ldots$ t}, has type \texttt{bool}. 360 \item 361 Matita features a liberal system of coercions (distinct from the previously mentioned record field coercions). 362 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$. 363 The coercion opens a proof obligation that asks the user to prove that $P$ holds for $x$. 364 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 subterms. 365 For instance, to apply a coercion to force $\lam{x}M : A \rightarrow B$ to 366 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$. 367 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. 368 In this way, Matita supports the `Russell' proof methodology developed by Sozeau in~\cite{sozeau:subset:2007}, in a lightweight but tightlyintegrated manner. 287 369 \end{itemize} 370 Throughout, for reasons of clarity, conciseness, and readability, we may choose to simplify or omit parts of Matita code. 371 We will always ensure that these omissions do not mislead the reader. 288 372 289 373 \subsection{Map of the paper} … … 305 389 some of the case studies we have performed to validate it. 306 390 307 Finally, in section~\ref{sect :conclusions} we present conclusions, as well as391 Finally, in section~\ref{sect.conclusions} we present conclusions, as well as 308 392 related and future work.
Note: See TracChangeset
for help on using the changeset viewer.