The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

Hello,

I had only a brief look at your example, so I may be repeating something
that was said previously. Sorry if that's the case.

One key thing to note is that the kernel calls [whd_betaiotazeta], which
does only a weak head reduction. In particular, it won't reduce the
branches of the match in your example, whereas it will reduce the head
let-ins.

Hope it helps.

Maxime.

On 11/03/2017 03:39 PM, Joachim Breitner wrote:
> Hi,
> 
> Am Freitag, den 03.11.2017, 15:01 +0100 schrieb William J. Bowman:
>> The Coq termination checker normalizes the body of a recursive
>> function *before* checking that it terminates. The typing rule is
>> something like:
>>
>>   Γ,f:A ⊢ e : A
>>   Γ,f:A ⊢  v = eval(e)
>>   terminates(v)
>>   -------------
>>   Γ ⊢ (fix f:A.e) : A
> 
> I dug into the source code and found this:
> 
>     (* Check if [def] is a guarded fixpoint body with decreasing arg.
>        given [recpos], the decreasing arguments of each mutually defined
>        fixpoint. *)
>     let check_one_fix renv recpos trees def =
>       let nfi = Array.length recpos in
> 
>       (* Checks if [t] only make valid recursive calls *)
>       let rec check_rec_call renv stack t =
>         (* if [t] does not make recursive calls, it is guarded: *)
>         if noccur_with_meta renv.rel_min nfi t then ()
>         else
>           let (f,l) = decompose_app (whd_betaiotazeta t) in
> 
>     (*               Interesting bit ↑ *)
> 
> From this I conclude that your `eval(e)` in the typing rule is actually
> ßɩζ-reduction.
> 
> Now ζ means “contraction of local definitions”, so that explains why it
> works with a locally bound list_C'.
> And the lack of δ (unfolding of transparent constants) explains why it
> would not work with the globally defined list_C.
> 
> And indeed,
> 
>   Eval cbv beta iota zeta in fun a C => (P (list_C C)).
> 
> does not reduce to list_P.
> 
> 
> But this does not explain everything, and I’d like to get a better
> understanding what precisly is happening:
> 
> Without δ, why does it unfold `list_P` and `existsb` to see that the
> recursion on the list is nicely structural? And why do tree_P1 and
> tree_P2 still work even when I specify Opaque list_P.?
> 
> 
> 
> And I expect the answer to be no… but is there any way to make the
> termination checker reduce with delta on?
> 
> Thanks,
> Joachim
> 
>