Changeset 3519 for Papers


Ignore:
Timestamp:
Nov 18, 2014, 4:11:49 PM (4 years ago)
Author:
mulligan
Message:

little more added about matita. finished introduction to matita

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

Legend:

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

    r3518 r3519  
    1919  pages = {125--142},
    2020  doi = {http://dx.doi.org/10.1016/j.entcs.2006.09.026},
     21  year = {2007}
     22}
     23
     24@incollection
     25{ sozeau:subset:2007,
     26  author = {Matthieu Sozeau},
     27  title = {Subset Coercions in {Coq}},
     28  booktitle = {Types for Proofs and Programs},
     29  volume = {4502},
     30  series = {Lecture Notes in Computer Science},
     31  doi = {10.1007/978-3-540-74464-1_16},
     32  pages = {237--252},
    2133  year = {2007}
    2234}
  • Papers/jar-assembler-2014/boender-jar-2014.tex

    r3518 r3519  
    138138The entire term, with \texttt{match} expression applied to \texttt{refl $\ldots$ t}, has type \texttt{bool}.
    139139\item
    140 Matita features a liberal system of uniform coercions (distinct from the previously mentioned record field coercions).
    141 \todo{dpm: more about coercions}
     140Matita features a liberal system of coercions (distinct from the previously mentioned record field coercions).
     141It 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$ (here $\langle \_,\_ \rangle$ is Matita's sugared syntax for pairs).
     142The coercion opens a proof obligation that asks the user to prove that $P$ holds for $x$.
     143When 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 sub-terms.
     144For instance, to apply a coercion to force $\lam{x}M : A \rightarrow B$ to
     145have 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$.
     146This 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.
     147In this way, Matita supports the `Russell' proof methodology developed by Sozeau in~\cite{sozeau:subset:2007}, in a lightweight but tightly-integrated manner.
    142148\end{itemize}
    143149Throughout, for reasons of clarity, conciseness, and readability, we may choose to simplify or omit parts of Matita code.
Note: See TracChangeset for help on using the changeset viewer.