The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

Some idea:
You know that all recursive calls are smaller, thus if you could define a function ρ:ℕ→ℕ→ℕ such that ∀ x, y. x>y ⇒ ρ x y = problem y, then you could get a solution to your problem, by posing "problem x = ρ (S x) x".
∀ y. ρ O y is irrelevant, so it can be set as O.
∀ x. ρ (S x) O is equal to "problem O", thus it can be set as "G O"
∀ x, y. x > y ⇒ ρ (S x) (S y) is equal to "problem (S y)", thus it should be set to "sum_to y (fun t_i => G (problem t_i))". All 't_i's will be smaller or equal to y, thus "problem t_i" can be replaced by "ρ z t_i" for any z>t_i. As all 't_i's will be smaller than or equal to y, and x>y, "problem t_i" can be replaced with "ρ x t_i". There, the call to ρ is guarded if we do a recursion on the first argument.

Thus:
Fixpoint ρ (x : nat) : nat -> nat :=
  match x with
  | O => fun _ => O
  | S x => fun y =>
           match y with
           | O => G O
           | S y => sum_to y (fun t_i => G (ρ x t_i))
           end
  end.

Definition problem (t : nat) : nat := ρ (S t) t.

could do what you wished.

2014-03-18 2:10 GMT+01:00 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

--
.../Sedrikov\...