The Coq mailing list

[Michiel Helvensteijn <mhelvens AT gmail.com>]

Hi all!

It seems I'm still having trouble understanding the Coq termination
checker. I've reduced my current problem into the following minimal
example:

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 
-
Open Scope list_scope.

Inductive NatTree :=
  |  inner:  list NatTree  ->  NatTree
  |  leaf :  nat           ->  NatTree.

Fixpoint my_sum (l: list NatTree) : nat :=
  match l with
  |  (inner l'')::l'  =>  (my_sum l') + (my_sum l'')
  |  (leaf  n  )::l'  =>  (my_sum l') + n
  |  nil              =>  0
  end.
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 
-

This looks like relatively straight-forward structural recursion to
me. Nonetheless, while Coq is fine with me reducing through l' (the
list tail), it doesn't allow me to reduce through l'' (the list head).
So I have two questions:

(1) Is there a theoretical reason it shouldn't? Something I'm just not seeing?

(2) What is the recommended way of solving this? In my search I've
found some descriptions that might be related, but I'd really
appreciate a simple example.

Thanks!

-- 
www.mhelvens.net