The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 08/06/2017 14:42, Dominique Larchey-Wendling wrote:
> I suppose that during type-checking, Coq performs some kind of reduction
> and sees that 0 * z n reduces to 0 (definition of mult) ... hence there
> is no recursive sub-call.

Indeed, it is a well-known itch of the positivity checker: it performs a
weak-head reduction on the proof term before checking for productivity.
AFAIU this is required because we do some assumptions on the normal form
of the term, and whnf is amongst them.

Note that this is not the only misfeature of the Coq kernel that
contradicts my intuition. From the top of my head, I can also mention:

1. Loss of subject reduction due to whacky coinductive types
2. Modules. We could write a whole book on that one.
3. Global graph of universes.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature