The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

>> (1) Is there a theoretical reason it shouldn't? 

No
>> Something I'm just not seeing?

Well yes, but it is normal that you don't see it :-)

All arguments of constructors are NOT admissible subterms, polymorphic 
arguments of a constructors must not be !
See the example

Inductive I : Type := C: (forall (P : Type), P->P) -> I.

Definition Paradox : False :=
(fix ni (i :I):False := match i with | C f => ni (f i) end)
(C (fun (P :Type) (x :P)  => x)).

to understand why !

Coq registers "admissible for recursive calls" arguments of a constructor at 
definition time. Consequently, as the first argument of cons in 

Inductive list (A : Type) : Type := nil : list A | cons : A -> list A -> list 
A.

has an unknown type "A". it will never be OK to use it (or one of its 
subterm) as a subterm of the recursive argument ! (Yes, Coq should make the 
check at usage time. Everything would be fine and your trouble as the one of 
every Coq user before you would be solved)

There is sometime a work-around. In "match x with | cons a _ => ... | _ => 
... end", if 'x' is the recursive argument, we have just seen why sadly 'a' 
will never be recognize as a subterm but if 'x' is a subterm already then 'a' 
will be one.

As a consequence, inner fixpoints (has the fold hidden in Robbert solution) 
sometime saves you … (the argument of inner is a subterm)

Pierre B.

Le 5 oct. 2013 à 15:57, Robbert Krebbers 
<mailinglists AT robbertkrebbers.nl>
 a écrit :

> On 10/05/2013 03:51 PM, Michiel Helvensteijn wrote:
>> (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.
> The following alternative definition does through:
> 
> Fixpoint my_sum' (l: NatTree) : nat :=
>  match l with
>  | leaf n => n
>  | inner l => fold_right plus 0 (map my_sum' l)
>  end.
> Definition my_sum (l : list NatTree) : nat :=
>  fold_right plus 0 (map my_sum' l).