Changeset 3516 for Papers

Nov 17, 2014, 12:08:32 PM (4 years ago)

more on matita

2 edited


  • Papers/jar-assembler-2014/boender-jar-2014.bib

    r3514 r3516  
     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}
     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 = {}
    1331{ cerco:2011,
  • Papers/jar-assembler-2014/boender-jar-2014.tex

    r3515 r3516  
    19 \renewcommand{\verb}{\lstinline}
    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.
    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.
     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:
    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.
     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.
     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).
     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}.
     81Records are introduced with the \texttt{record} keyword.
     82A Matita record
     84record R : Type[0] := { F1 : nat }.
     86may be thought of as syntactic sugar for a single-constructor inductive data type of the same name:
     88inductive R : Type[0] :=
     89  | mk_R : nat -> R.
     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.
     95Record fields may be marked as coercions.
     96In the following example
     98record S : Type[1] :=
     99  {
     100    Carrier :> Type[0];
     101    op : Carrier -> Carrier -> Carrier
     102  }
     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.
     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'.
Note: See TracChangeset for help on using the changeset viewer.