Changeset 3519
 Timestamp:
 Nov 18, 2014, 4:11:49 PM (5 years ago)
 Location:
 Papers/jarassembler2014
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Papers/jarassembler2014/boenderjar2014.bib
r3518 r3519 19 19 pages = {125142}, 20 20 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/9783540744641_16}, 32 pages = {237252}, 21 33 year = {2007} 22 34 } 
Papers/jarassembler2014/boenderjar2014.tex
r3518 r3519 138 138 The entire term, with \texttt{match} expression applied to \texttt{refl $\ldots$ t}, has type \texttt{bool}. 139 139 \item 140 Matita features a liberal system of uniform coercions (distinct from the previously mentioned record field coercions). 141 \todo{dpm: more about coercions} 140 Matita features a liberal system of coercions (distinct from the previously mentioned record field coercions). 141 It 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). 142 The coercion opens a proof obligation that asks the user to prove that $P$ holds for $x$. 143 When 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 subterms. 144 For instance, to apply a coercion to force $\lam{x}M : A \rightarrow B$ to 145 have 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$. 146 This 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. 147 In this way, Matita supports the `Russell' proof methodology developed by Sozeau in~\cite{sozeau:subset:2007}, in a lightweight but tightlyintegrated manner. 142 148 \end{itemize} 143 149 Throughout, 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.