The Coq mailing list

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

Le 18 mars 2014 à 02:10, Geoff Hulette 
<ghulette AT gmail.com>
 a écrit :

> Is there an easy way to convince Coq to accept the following recursion?
Yes but it implies to know about the gory detail of the guard condition…

if something is a parameter (identical for all recursive calls) put it as so :
Definition sum_to (f : nat -> nat): nat -> nat :=
fix aux i :=
  match i with
  | O => f O
  | S i' => f i + (aux i')
  end.

This is not enough : O when i is O and when i is a sub term is not a sub term 
… but i (that is equal to O) is so :
Definition sum_to (f : nat -> nat): nat -> nat :=
fix aux i :=
  match i with
  | O => f i
  | S i' => f i + (aux i')
  end.
is the sum_to definition that will make problem works !

> Parameter G : nat -> nat.
> 
> Fixpoint problem (t : nat) : nat :=
>   match t with
>   | O => G O
>   | S t' => sum_to t' (fun t_i => G (problem t_i))
>   end.

All the best,
Pierre B.