The Coq mailing list

[Randy Pollack <rpollack AT inf.ed.ac.uk>]

The problem is that Coq coercions are informally specified and behave
somewhat unpredictably.  A formal theory of coercions, such as Luo's
Coercive subtyping (with proof theory and semantics) would eliminate
this question of the meaning of statements using coercions.  However,
the proof theory of coercions is complicated.

BTW, I guess coercions are required for large scale formal
mathematics.  For example, subtyping of algebraic structures by purely
structural means (fewer components, ...) is inadequate for real
mathematics.

Randy
--
On Sun, Jun 12, 2011 at 9:15 AM, Adam Chlipala 
<adam AT chlipala.net>
 wrote:
> Georgi Guninski wrote:
>>
>> Are lemma proved coercions considered cheating that violates Pollack
>> consistency?
>>
>
> I think the issue of coercions should be considered independently of the way
> the coercion functions are defined.
>
> I haven't read a definition of Pollack consistency.  To me, the relevant
> question is about the proper form for displaying theorem statements, so that
> we can develop high confidence that they mean what we think they mean.  I
> don't think such a form should support implicit coercions at all.  (I never
> use coercions in theorem statements.)
>
>