Coq alternative mechanisms of proving that a function terminates

Question

I wrote a proof for this question, but it's long and kind of terrible, see Appendix A.

There is one specific thing that I want to focus on and that is the induction step in make_double_induction.

Program Fixpoint make_double_induction
  P
  (H0 : P 0 0)
  (Hn : forall n, P 0 n -> P 0 (S n))
  (Hm : forall m, P m 0 -> P (S m) 0)
  (Hmn : forall m n, P m n -> P (S m) (S n))
  (m : nat)
  (n : nat) : P m n :=
match (m, n) with
| (O, _) => make_double_induction_lemma P H0 Hn Hm Hmn n
| (S m, O) => Hm m (make_double_induction _ _ _ _ _ _ _)
| (S m, S n) => Hmn m n (make_double_induction _ _ _ _ _ _ _)
end.

In order to convince Rocq that this function terminates, I broke out the case that counts down on the second argument and put it in a lemma that was also structurally inductive. (The lemma takes a bunch of unnecessary arguments but that is neither here nor there).

Anyway, there are various ways of proving to another human that the version of make_double_induction with the lemma unfolded terminates, such as nothing that it always counts down on m + n.

I am curious if there's a way of writing this function in a way that will be accepted by the Coq termination checker without hiding make_double_induction_lemma

Appendix A

Lemma leibniz : forall {T} {U} (a : T) b (f : T -> U), a = b -> f a = f b.
Proof.
  intros T U a b f H.
  now rewrite H.
Defined.

Lemma pair_extensionality : forall {T} {U} (a : T) (b : U) c d, (a, b) = (c, d) <-> (a = c /\ b = d).
Proof.
  intros T U a b c d.
  intuition.
  - pose proof @leibniz _ _ (a, b) (c, d) fst as I.
    now specialize (I H).
  - pose proof @leibniz _ _ (a, b) (c, d) snd as I.
    now specialize (I H).
  - rewrite H0.
    now rewrite H1.
Defined.

Lemma debiconditional : forall {A} {B} (x : A <-> B), (A -> B).
Proof. intuition. Defined.

Program Fixpoint make_double_induction_lemma
  P
  (H0 : P 0 0)
  (Hn : forall n, P 0 n -> P 0 (S n))
  (Hm : forall m, P m 0 -> P (S m) 0)
  (Hmn : forall m n, P m n -> P (S m) (S n))
  (n : nat) : P 0 n :=
match n with
| O => _
| S n => Hn n (make_double_induction_lemma _ _ _ _ _ n)
end.
Next Obligation. intros. refine H0. Defined.
Next Obligation. intros. refine H0. Defined.
Next Obligation. intros. refine (Hn n1 X). Defined.
Next Obligation. intros. refine (Hm m X). Defined.
Next Obligation. intros. refine (Hmn m n1 X). Defined.

Program Fixpoint make_double_induction
  P
  (H0 : P 0 0)
  (Hn : forall n, P 0 n -> P 0 (S n))
  (Hm : forall m, P m 0 -> P (S m) 0)
  (Hmn : forall m n, P m n -> P (S m) (S n))
  (m : nat)
  (n : nat) : P m n :=
match (m, n) with
| (O, _) => make_double_induction_lemma P H0 Hn Hm Hmn n
| (S m, O) => Hm m (make_double_induction _ _ _ _ _ _ _)
| (S m, S n) => Hmn m n (make_double_induction _ _ _ _ _ _ _)
end.
Next Obligation.
  intros.
  unfold filtered_var in *.
  pose proof (debiconditional (pair_extensionality 0 wildcard' m n)) as H.
  specialize (H Heq_anonymous).
  now destruct H.
Defined.
Next Obligation. intros. easy. Defined.
Next Obligation. intros. refine (Hn n0 X). Defined.
Next Obligation. intros. refine (Hm m1 X). Defined.
Next Obligation. intros. refine (Hmn m1 n0 X). Defined.
Next Obligation.
  intros.
  unfold filtered_var in Heq_anonymous.
  pose proof (debiconditional (pair_extensionality (S m) 0 m0 n)).
  specialize (H Heq_anonymous).
  now destruct H.
Defined.
Next Obligation.
  intros.
  unfold filtered_var in Heq_anonymous.
  pose proof (debiconditional (pair_extensionality (S m) 0 m0 n)).
  specialize (H Heq_anonymous).
  now destruct H.
Defined.
Next Obligation. intros. easy. Defined.
Next Obligation. intros. refine (Hn n1 X). Defined.
Next Obligation. intros. refine (Hm m1 X). Defined.
Next Obligation. intros. refine (Hmn m1 n1 X). Defined.
Next Obligation.
  intros.
  unfold filtered_var in Heq_anonymous.
  pose proof (debiconditional (pair_extensionality (S m) (S n) m0 n0)).
  specialize (H Heq_anonymous).
  now destruct H.
Defined.
Next Obligation.
  intros.
  unfold filtered_var in Heq_anonymous.
  pose proof (debiconditional (pair_extensionality (S m) (S n) m0 n0)).
  specialize (H Heq_anonymous).
  now destruct H.
Defined.
```

Answer 1

You may use Program Fixpoint's {measure} feature, where you provide a function of the argument that decreases at each recursive call:

Require Import Program Lia.

Program Fixpoint make_double_induction
  P
  (H0 : P 0 0)
  (Hn : forall n, P 0 n -> P 0 (S n))
  (Hm : forall m, P m 0 -> P (S m) 0)
  (Hmn : forall m n, P m n -> P (S m) (S n))
  (m : nat)
  (n : nat)
  { measure (m+n) }:
  P m n :=
  match (m, n) with
  | (O, O) => H0
  | (S m, O) => Hm m (make_double_induction P H0 Hn Hm Hmn m O)
  | (O, S n) => Hn n (make_double_induction P H0 Hn Hm Hmn O n)
  | (S m, S n) => Hmn m n (make_double_induction P H0 Hn Hm Hmn m n)
  end.
Next Obligation. lia. Qed.

Answer 2

You can also use the package Equations (comes with the Coq Platform) for these kinds of things, that often works better and comes with powerful feature like function elimination

From Equations Require Import Equations.
Require Import Lia.

Section Foo.

  Context
  (P : nat -> nat -> Type)
  (H0 : P 0 0)
  (Hn : forall n, P 0 n -> P 0 (S n))
  (Hm : forall m, P m 0 -> P (S m) 0)
  (Hmn : forall m n, P m n -> P (S m) (S n)).

Equations? make_double_induction (m : nat) (n : nat) : P m n by wf (n + m) lt :=
  | O, O   := H0
  | S m, O := Hm m (make_double_induction m O)
  | O, S n := Hn n (make_double_induction O n)
  | S m, S n := Hmn m n (make_double_induction m n).
Proof.
  lia.
Qed.

Equations make_double_induction' (m : nat) (n : nat) : P m n by wf (n,m) (lexprod _ _ lt lt) :=
  | O, O   := H0
  | S m, O := Hm m (make_double_induction' m O)
  | O, S n := Hn n (make_double_induction' O n)
  | S m, S n := Hmn m n (make_double_induction' m n).


End Foo.

C.f. the repo and the documentation. Note that bugs mentioned in the documentation have been fixed in the 8.20 version. (Coq platform is currently 19.2)