Changeset 1020

Jun 21, 2011, 12:09:33 PM (8 years ago)

More on Matita.

2 edited


  • src/ASM/CPP2011/cpp-2011.bib

    r981 r1020  
     222  author    = {Matthieu Sozeau},
     223  title     = {Subset Coercions in {C}oq},
     224  booktitle = {Types for Proofs and Programs},
     225  series    = {LNCS},
     226  year      = {2006},
     227  pages     = {237-252},
     228  VOLUME = {4502/2007},
     229  PUBLISHER = {Springer-Verlag},
     230  doi = {10.1007/978-3-540-74464-1\_16},
  • src/ASM/CPP2011/cpp-2011.tex

    r1019 r1020  
    191191In particular, in CerCo we are also interested in the completeness of the compilation process, whereas previous formalisations only focused on correctness.
    193 The rest of this paper is a detailed description of our proof.
     193The rest of this paper is a detailed description of our proof that is partly
     194still in progress.
    195196% ---------------------------------------------------------------------------- %
    210 Matita is a proof assistant based on the Calculus of (Co)inductive Constructions~\cite{asperti:user:2007}.
    211 For those familiar with Coq, Matita's syntax and mode of operation should be entirely familiar.
    212 However, we take time here to explain one of Matita's syntactic idiosyncrasies.
    213 The use of `$\mathtt{?}$' or `$\mathtt{\ldots}$' in an argument position denotes a term or terms to be inferred automatically by unification, respectively.
    214 The use of `$\mathtt{?}$' in the body of a definition, lemma or axiom denotes an incomplete term that is to be closed, by hand, using tactics.
     211Matita is a proof assistant based on a variant of the Calculus of (Co)inductive Constructions~\cite{asperti:user:2007}. In particular, it features dependent
     212types that we heavily exploit in the formalization. The syntax of the
     213statements and definitions in the paper should be self-explanatory, at least
     214to those exposed to dependent type theory. We only remark the use of
     215of `$\mathtt{?}$' or `$\mathtt{\ldots}$' for omitting single terms or
     216sequences of terms to be inferred automatically by the system, respectively.
     217Those that are not inferred are left to the user as proof obligations.
     218Pairs are denoted with angular brackets.
     220Matita features a liberal system of coercions. In particular, it is possible
     221to define a uniform coercion $\lambda x.\langle x,?\rangle$ from every type $T$ to the dependent product $\Sigma x:T.P~x$. The coercion opens a proof
     222obligation that asks the user to prove that $P$ holds for $x$. When a coercion
     223must be applied to a complex term (a lambda-abstraction, a local definition,
     224a case analysis), the system automatically propagates the coercion to the
     225sub-terms. For instance, to apply a coercion to force $\lambda x.M : A \to B$
     226to have type $\forall x:A.\Sigma y:B.P~x~y$, the system looks for a coercion from
     227$M: B$ to $\Sigma y:B.P~x~y$ in a context augmented with $x:A$. This is
     228significant when the coercion opens a proof obligation, since the user
     229will be presented with multiple, but simpler proof obligations in the right
     230context. Matita supports in this way the proof methodology developed by
     231Sozeau in~\cite{russell}, but with an implementation that is lighter than the
     232one of Coq and more integrated in the system.
    216234% ---------------------------------------------------------------------------- %
Note: See TracChangeset for help on using the changeset viewer.