The Coq mailing list

[Geoff Hulette <ghulette AT gmail.com>]

Is there an easy way to convince Coq to accept the following recursion?

Fixpoint sum_to (i : nat) (f : nat -> nat) : nat :=

  match i with

  | O => f O

  | S i' => f i + (sum_to i' f)

  end.

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.

It complains, of course, because Coq doesn't realize that t_i will always be invoked on argument structurally smaller than t. Ideally I could just use a tactic like refine and provide a proof of termination by hand, or something, but I am not quite sure what that should look like.

Any help would be greatly appreciated!

Thanks!

-geoff