The Coq mailing list

[Joachim Breitner <mail AT joachim-breitner.de>]

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


-- 
Joachim Breitner
  
mail AT joachim-breitner.de
  http://www.joachim-breitner.de/

Attachment: signature.asc
Description: This is a digitally signed message part