Showing terminating recursion for cumsum in Coq

I want to prove that computing the cumulative sum between a and b terminates.

I use an Acc lt x term to show that the recursion decreases, like this

Require Import Omega.

Lemma L1 : forall a b, a<b -> (b-(1+a)) < (b-a).
  intros; omega. Qed.

Lemma term_lemma: forall a b, Acc lt (b-a) ->  Acc lt (b-(1+a)).
    intros;  inversion H; clear H; constructor; intros; apply H0; omega.
Defined.

Fixpoint cumsum a b (H: Acc lt (b-a)) {struct H} : nat.
refine (
    match lt_dec a b  with
    | left a_lt_b => a + cumsum (1+a) b _
    | right a_ge_b => if beq_nat a b then a else 0
    end
  ).
apply (term_lemma _ _ H).
Qed.

It clears all subgoals but it won't typecheck at the Qed statement. Coq complains:

Recursive definition of cumsum is ill-formed
Recursive call to cumsum has principal argument equal to
"term_lemma a b H" instead of a subterm of "H".

I guess I should somehow use L1 to show that the argument in the H term in the recursive call is actually smaller, but how do I do that?

Solution

Because you invert H before building something similar-ish back again by using constructor ; apply H0, you get a term_lemma with a pattern matching that's equivalent to what you'd want but confuses Coq's termination checker (You can inspect a term by using Print NAME.).

You don't need to do all of this inversion business if you remember that you already know that a < b thanks to your case analysis on lt_dec a b. By letting your lemma take an extra argument, you can now use the strict subterm of the Accessibility predicate to get your witness:

Require Import Omega.

Lemma term_lemma: forall a b, a < b -> Acc lt (b-a) ->  Acc lt (b-(1+a)).
 intros a b altb [H]; apply H; omega.
Defined.

Fixpoint cumsum a b (H: Acc lt (b-a)) {struct H} : nat.
refine (
    match lt_dec a b  with
    | left a_lt_b => a + cumsum (1+a) b _
    | right a_ge_b => if beq_nat a b then a else 0
    end
  ).
apply (term_lemma _ _ a_lt_b H).
Defined.