coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, (continued)
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, raffaello . giulietti, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Beta Ziliani, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, raffaello . giulietti, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Abhishek Anand, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Morrisett, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Beta Ziliani, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Dominique Larchey-Wendling, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Beta Ziliani, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, raffaello . giulietti, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Dominique Larchey-Wendling, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, raffaello . giulietti, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, raffaello . giulietti, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Pierre-Marie Pédrot, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Maxime Dénès, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Maxime Dénès, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Maxime Dénès, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Beta Ziliani, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, raffaello . giulietti, 06/08/2017
Archive powered by MHonArc 2.6.18.