Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification


Chronological Thread 
  • From: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification
  • Date: Thu, 8 Jun 2017 15:24:21 +0200

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




Archive powered by MHonArc 2.6.18.

Top of Page