The Coq mailing list

[Georgi Guninski <guninski AT guninski.com>]

On Sun, Jun 12, 2011 at 10:32:52AM -0400, Randy Pollack wrote:
> 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
> --

Dear Pollack,

It is my understanding that the current implementation of Coq coercions 
allows arbitrary redefinition of constants (as in jokes).

Are the current Coq coercions justified by theory, if yes, by what theory?

On unrelated note, why should i believe [coqchk] doesn't reject valid code?

Is there an independent implementation of coqchk?

On Coq-club bugs pop up often, it is easy to fix a counter example in coqchk, 
but what about false positives where coqchk rejects valid code?

{FYI i have a coq fork where coqtop is happy but coqchk gives errors on 
counterintuitive statements...}