Changeset 3516 for Papers


Ignore:
Timestamp:
Nov 17, 2014, 12:08:32 PM (4 years ago)
Author:
mulligan
Message:

more on matita

Location:
Papers/jar-assembler-2014
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Papers/jar-assembler-2014/boender-jar-2014.bib

    r3514 r3516  
    1010}
    1111
     12@inproceedings
     13{ bove:brief:2009,
     14  author = {Ana Bove and Peter Dybjer and Ulf Norell},
     15  title = {A Brief Overview of {Agda} --- A Functional Language with Dependent Types},
     16  booktitle = {Theorem Proving in Higher-order Logics {(TPHOLs)}},
     17  year = {2009}
     18}
     19
     20@manual
     21{ coq:2004,
     22  title = {The {Coq} proof assistant reference manual},
     23  author =  {{The Coq development team}},
     24  organization = {{LogiCal Project}},
     25  note = {Version 8.0},
     26  year = {2004},
     27  url = {http://coq.inria.fr}
     28}
     29
    1230@misc
    1331{ cerco:2011,
  • Papers/jar-assembler-2014/boender-jar-2014.tex

    r3515 r3516  
    1414\usepackage{kpfonts}
    1515\usepackage[T1]{fontenc}
     16\usepackage[ttdefault=true]{AnonymousPro}
     17
     18\newcommand{\deffont}[1]{\textbf{#1}}
    1619
    1720\bibliographystyle{alpha}
    1821
    19 \renewcommand{\verb}{\lstinline}
     22%\renewcommand{\verb}{\lstinline}
    2023\def\lstlanguagefiles{lst-grafite.tex}
    2124\lstset{language=Grafite}
     
    5356\label{subsect.matita}
    5457
    55 Matita is a proof assistant based on a variant of the Calculus of (Co)inductive Constructions~\cite{asperti:user:2007}.
    56 It features full spectrum dependent types as well as a sophisticated system of coercions, both of which we exploit in this formalisation.
    57 
    58 Matita's syntax should be familiar for those readers acquainted with the OCaml functional programming language.
    59 Nevertheless, we provide a brief summary of the main syntactic features of Matita:
     58Matita is a theorem prover based on a variant of the Calculus of (Co-)inductive Constructions~\cite{asperti:user:2007}.
     59The system features a full spectrum of dependent types and (co-)inductive families, as well as a sophisticated system of coercions, all of which we exploit in the formalisation described in this paper.
     60
     61Matita's syntax is largely similar to the syntaxes of mainstream functional programming languages such as OCaml.
     62Nevertheless, 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:
    6063\begin{itemize}
    6164\item
    62 Non-recursive definitions are introduced with the \texttt{definition} keyword, and recursive definitions with the \texttt{let rec} keywords.
    63 \item
    64 There is extensive provision for customising syntax (through Unicode). Matita has an advanced system of overloading and resolution so that definitions and proofs look as natural as possible.
     65Non-recursive functions and definitions are introduced via the \texttt{definition} keyword, whilst recursive functions are introduced with \texttt{let rec}.
     66Mutually recursive functions are separated via the \texttt{and} keyword.
     67\item
     68Matita has an infinite hierarchy of type universes.
     69A single impredicative universe of types, \texttt{Prop}, exists at the base of this hierarchy.
     70An infinite series of predicative universes, \texttt{Type[0]} : \texttt{Type[1]} : \texttt{Type[2]}, and so on and so forth, sits atop \texttt{Prop}.
     71Matita, unlike Coq~\cite{coq:2004} or Agda~\cite{bove:brief:2009}, implements no form of typical ambiguity or universe polymorphism, with explicit concrete universe levels being preferred instead.
     72\item
     73Matita's type theory plays host to a rich and expressive higher-order logic.
     74Constant \texttt{True} and \texttt{False} represent truth and (constructive) falsity in \texttt{Prop} respectively.
     75Inductive families in \texttt{Prop} encode conjunction and disjunction---$\mathtt{P \wedge Q}$ and $\mathtt{P \vee Q}$ respectively---also.
     76As 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).
     77\item
     78Inductive families are introduced via the \texttt{inductive} keyword with named constructor declarations separated with a bar.
     79Mutually inductive data family declarations are separated via \texttt{with}.
     80\item
     81Records are introduced with the \texttt{record} keyword.
     82A Matita record
     83\begin{lstlisting}
     84record R : Type[0] := { F1 : nat }.
     85\end{lstlisting}
     86may be thought of as syntactic sugar for a single-constructor inductive data type of the same name:
     87\begin{lstlisting}
     88inductive R : Type[0] :=
     89  | mk_R : nat -> R.
     90\end{lstlisting}
     91In particular, declaration of a record \texttt{R} causes a \deffont{constructor} function \texttt{mk\_R} to be entered into the global context as a side effect.
     92\deffont{Projections}, one for each of the record's fields, are also registered in the global context.
     93In the example record above, \texttt{F1} of type $R \rightarrow nat$ is registered as a field projection.
     94
     95Record fields may be marked as coercions.
     96In the following example
     97\begin{lstlisting}
     98record S : Type[1] :=
     99  {
     100    Carrier :> Type[0];
     101    op : Carrier -> Carrier -> Carrier
     102  }
     103\end{lstlisting}
     104the field \texttt{Carrier} is declared to be a coercion with `\texttt{:>}', and the field projection \texttt{Carrier} may be omitted where it could be successfully inferred by Matita's typechecker, thus facilitating the common mathematical practice of confusing a mathematical structure with its underlying carrier set.
     105\item
     106There is provision for customising syntax (through Unicode).
     107Matita has a type-directed system of overloading and resolution so that definitions and proofs look `natural'.
    65108\end{itemize}
    66109
Note: See TracChangeset for help on using the changeset viewer.