Structural recursion on two arguments

Question

I have tried to make a function in Coq which has a pretty complex termination argument. To make it easier, I am able to write the function so that it has a natural number as first argument, so that either the number or the argument after it is structurally smaller.

When trying the nested fix approach to recursion on two arguments, Coq complains that a proof argument that contains the semantics of the decreasing number is not an inductive type.

I could probably do well-founded recursion manually, but I would like to use Program Fixpoint or Equations. With Program Fixpoint I get a very ugly version of the well-foundedness proof. Below is a minimal code example that demonstrates the ugliness.

Require Import Program.

Inductive tuple_lt : (nat * nat) -> (nat * nat) -> Prop :=
  fst_lt : forall a b c d, a < c -> tuple_lt (a, b) (c, d).

Program Fixpoint f (a : nat) (b : nat) {measure (a, b) tuple_lt} :=
  match a with
  | 0 => 0
  | S n => f n b
  end.

Next Obligation.b, n: nat
f: forall a b0 : nat,
tuple_lt (a, b0) (S n, b) -> nat
tuple_lt (n, b) (S n, b)
  apply fst_lt.b, n: nat
f: forall a b0 : nat,
tuple_lt (a, b0) (S n, b) -> nat
n < S n auto.
Qed.

Next Obligation.well_founded
  (MR tuple_lt
     (fun recarg : {_ : nat & nat} =>
      (projT1 recarg, projT2 recarg)))
  unfold well_founded.forall a : {_ : nat & nat},
Acc
  (MR tuple_lt
     (fun recarg : {_ : nat & nat} =>
      (projT1 recarg, projT2 recarg))) a unfold MR.forall a : {_ : nat & nat},
Acc
  (fun x y : {_ : nat & nat} =>
   tuple_lt (projT1 x, projT2 x) (projT1 y, projT2 y))
  a

The obligation looks like this:

1 subgoal

  ============================
  forall a : {_ : nat & nat},
  Acc
    (fun x y : {_ : nat & nat} =>
     tuple_lt (projT1 x, projT2 x)
       (projT1 y, projT2 y)) a

Can I somehow transform a proof of Acc tuple_lt into that ugly proof or avoid generating it?

Is there a proof in the standard library for structural recursion on two arguments?

How do I even write a manual WF proof using Equations? The manual does not mention that.

Answer

In simple cases like this one, you shouldn't have to unfold definitions such as well_founded and MR, but rather use appropriate lemmas.

To deal with MR, you can use lemma measure_wf in Program.Wf.

To prove the well-foundedness of tuple_lt, you can rely on lemmas showing the well-foundedness of a relation based on the well-foundedness of another relation. Here, we can use well_founded_lt_compat. In other cases, you may find other lemmas useful, such as wf_inverse_image, well_founded_ltof or well_founded_gtof.

The proof of the well-foundedness of tuple_lt becomes simple.

Lemma tuple_lt_wf : well_founded tuple_lt.well_founded tuple_lt
Proof.well_founded tuple_lt
  apply well_founded_lt_compat with fst.forall x y : nat * nat, tuple_lt x y -> fst x < fst y
  intros ? ? []; assumption.
Defined.

And so does the proof of the second obligation.

Next Obligation.well_founded
  (MR tuple_lt
     (fun recarg : {_ : nat & nat} =>
      (projT1 recarg, projT2 recarg)))
  apply measure_wf.well_founded tuple_lt apply tuple_lt_wf.
Defined.

(Note that in both cases, you should end the proofs with Defined instead of Qed, if you want your function defined by Program Fixpoint to compute inside Coq (otherwise it gets stuck on opaque proofs); it seems that you can end the proof of the first obligation with Qed, though).

You could also use the following simpler definition for tuple_lt:

Definition tuple_lt (p1 p2 : nat * nat) := fst p1 < fst p2.

In that case, the proof of well-foundedness is trivial.

Lemma tuple_lt_wf : well_founded tuple_lt.well_founded tuple_lt
Proof.well_founded tuple_lt
  apply well_founded_ltof.
Defined.