CoqExtraction/Letouzey/2/2.1

#2.1 The difficulties in the removal of logical parts

A potential danger induced by removal of logical parts is that this removal can modify the evaluation order. Let us take for example a function of type $\forall x:A,(Px)\to B\backslash forall\; x\; :\; A,\; (P~\; x)\; \backslash to\; B$, with $AA$ and $BB$ being informative types, and $PP$ a logical property. Our function $ff$ thus awaits an informative argument and $xx$ and a proof that this argument satisfies the pre-condition $PxP\; ~x$. If one also has a term $tt$ of type $AA$ and a proof $pp$ of type $(Pt)(P\; ~t)$, one can then form the two well-typed Coq terms $(ft)(f~t)$ and $(ftp)(f~t~p)$. On the Coq level, these two terms have appreciably different nature. For example, the evaluation of $(ft)(f\; ~t)$ will probably be quickly blocked by the lack of the second argument $pp$, whereas $(ftp)(f~t~p)$ is a total application which can normally be reduced towards a value of type $BB$ (when for example these terms $ff$, $tt$ and $pp$ are closed).