# Changeset 1020

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

More on Matita.

Location:
src/ASM/CPP2011
Files:
2 edited

Unmodified
Removed
• ## src/ASM/CPP2011/cpp-2011.bib

 r981 } @inproceedings{russell, author    = {Matthieu Sozeau}, title     = {Subset Coercions in {C}oq}, booktitle = {Types for Proofs and Programs}, series    = {LNCS}, year      = {2006}, pages     = {237-252}, VOLUME = {4502/2007}, PUBLISHER = {Springer-Verlag}, doi = {10.1007/978-3-540-74464-1\_16}, }
• ## src/ASM/CPP2011/cpp-2011.tex

 r1019 In particular, in CerCo we are also interested in the completeness of the compilation process, whereas previous formalisations only focused on correctness. The rest of this paper is a detailed description of our proof. The rest of this paper is a detailed description of our proof that is partly still in progress. % ---------------------------------------------------------------------------- % \label{sect.matita} Matita is a proof assistant based on the Calculus of (Co)inductive Constructions~\cite{asperti:user:2007}. For those familiar with Coq, Matita's syntax and mode of operation should be entirely familiar. However, we take time here to explain one of Matita's syntactic idiosyncrasies. The use of $\mathtt{?}$' or $\mathtt{\ldots}$' in an argument position denotes a term or terms to be inferred automatically by unification, respectively. 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. Matita is a proof assistant based on a variant of the Calculus of (Co)inductive Constructions~\cite{asperti:user:2007}. In particular, it features dependent types that we heavily exploit in the formalization. The syntax of the statements and definitions in the paper should be self-explanatory, at least to those exposed to dependent type theory. We only remark the use of of $\mathtt{?}$' or `$\mathtt{\ldots}$' for omitting single terms or sequences of terms to be inferred automatically by the system, respectively. Those that are not inferred are left to the user as proof obligations. Pairs are denoted with angular brackets. Matita features a liberal system of coercions. In particular, it is possible to 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 obligation that asks the user to prove that $P$ holds for $x$. When a coercion must be applied to a complex term (a lambda-abstraction, a local definition, a case analysis), the system automatically propagates the coercion to the sub-terms. For instance, to apply a coercion to force $\lambda x.M : A \to B$ to have type $\forall 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$. This is significant when the coercion opens a proof obligation, since the user will be presented with multiple, but simpler proof obligations in the right context. Matita supports in this way the proof methodology developed by Sozeau in~\cite{russell}, but with an implementation that is lighter than the one of Coq and more integrated in the system. % ---------------------------------------------------------------------------- %
Note: See TracChangeset for help on using the changeset viewer.