The Coq mailing list

["William J. Bowman" <wjb AT williamjbowman.com>]

I agree with Tej that the problems in your code appear to result from scope 
and type classes, but I want to point out something about the termination 
checker some find surprising.

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

That is, we type check the body `e` of a recursive function, then evaluate 
`e` to a normal form `v` (with the recursive name `f` still free, so the body 
can’t diverge during type checking), then check that `v` is terminating.

The let bindings in your recursive functions can thus be inlined during 
evaluation, before checking termination (although, I don’t *think* this is 
causing your problem). If this is surprising, you may enjoy the fact that you 
can exploit this behavior to write the following well-typed expression:

  Eval cbv in ((fix f (x : nat) := let n := (f x) in 0) 0).  

—
William J. Bowman

> On Nov 3, 2017, at 2:27 PM, Joachim Breitner 
> <mail AT joachim-breitner.de>
>  wrote:
> 
> Hi,
> 
> 
> 
> I am stumbling about behavior of Coq’s termination checker that I
> cannot explain to myself. Consider:
> 
> Require Import Coq.Lists.List.
> 
> Class C a := {  P : a -> bool }.
> 
> Definition list_P {a} `{C a} : list a -> bool := existsb P.
> 
> Instance list_C  {a} `{C a} : C (list a) := { P := list_P }.
> 
> (* Note that *)
> Eval cbn in       fun a C => (@P (list a) (@list_C a C)).
> (* evaluates to:  fun a C  => list_P *)
> 
> Inductive tree a := Node : a -> list (tree a) -> tree a.
> 
> (* Works *)
> Fixpoint tree_P1 {a} `{C a} (t : tree a) : bool :=
>    let tree_C := Build_C _ tree_P1 in
>    let list_C := Build_C _ list_P in (* Question 1: Why is this line needed 
> *)
>    match t with Node _ x ts => orb (P x) (P ts) end.
> 
> Instance tree_C  {a} `{C a} : C (tree a) := { P := tree_P1 }.
> 
> (* Works too *)
> Fixpoint tree_P2 {a} `{C a} (t : tree a) : bool :=
>    let tree_C := Build_C _ tree_P2 in
>    match t with Node _ x ts => orb (P x) (list_P ts) end.
> 
> (* Does not work. Why not? *)
> Fixpoint tree_P3 {a} `{C a} (t : tree a) : bool :=
>    let tree_C := Build_C _ tree_P3 in
>    match t with Node _ x ts => orb (P x) (@P _ (@list_C _ tree_C) ts) end.
> 
> (* And hence, this (identical?) code does not work *)
> Fixpoint tree_P4 {a} `{C a} (t : tree a) : bool :=
>    let tree_C := Build_C _ tree_P4 in
>    match t with Node _ x ts => orb (P x) (P ts) end.
> 
> The first and second example show that, when trying to understand
> whether a fixpoint is terminating, Coq is able to resolve record
> accessors, basically evaluating what we wrote in tree_P1 to what we
> wrote in tree_P2.
> 
> But this seems to only work if the record is built locally (let tree_C
> :=…), not if it is defined using Definition.
> 
> But Fixpoint can look through other definitions just fine, e.g. through
> list_P. So what is special about records, and can I make Coq accept
> tree_P3 and tree_P4?
> 
> 
> Thanks,
> Joachim
> 
> 
> -- 
> Joachim Breitner
>  
> mail AT joachim-breitner.de
>  http://www.joachim-breitner.de/