# Changeset 3519 for Papers

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

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

### Legend:

Unmodified
 r3518 The entire term, with \texttt{match} expression applied to \texttt{refl $\ldots$ t}, has type \texttt{bool}. \item Matita features a liberal system of uniform coercions (distinct from the previously mentioned record field coercions). \todo{dpm: more about coercions} Matita features a liberal system of coercions (distinct from the previously mentioned record field coercions). 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). The coercion opens a proof obligation that asks the user to prove that $P$ holds for $x$. 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 sub-terms. For instance, to apply a coercion to force $\lam{x}M : A \rightarrow B$ to 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$. 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. In this way, Matita supports the `Russell' proof methodology developed by Sozeau in~\cite{sozeau:subset:2007}, in a lightweight but tightly-integrated manner. \end{itemize} Throughout, for reasons of clarity, conciseness, and readability, we may choose to simplify or omit parts of Matita code.