How to target an introduced value set with the set tactic for induction in Coq?

Question

Suppose I have a pair of two natural numbers $(a, b) \in \mathbb{N} \times \mathbb{N}$.

I define the relation $<$ below.

$(a, b) < (a', b') \;\; \text{if and only if} \;\; a + b < a' + b'$.

This relation is well-founded.

As proof, the sum $a+b$ of a pair $(a, b)$ is a natural number, so each successive pair in a strictly descending chain must have a strictly lower sum and thus the chain is finite.

I am, however, struggling to prove this fact in Coq.

The first idea I had was to use the set tactic to introduce the sum into my environment and then induct on it, but the sum s seems to vanish once I try to target it with the induct tactic.

Require Import Lia. 
 
Lemma add_2nat_induction (f : nat -> nat -> _) (base : f 0 0) 
  (ind : forall z w, (forall x y, x + y < z + w -> f x y) -> f z w) : (forall n n', f n n'). 
Proof. 
  intro n. 
  intro n'. 
  set (s := n + n'). 
  induction s. 
  - assert (n = 0). 
    + (lia || idtac). (* why does this fail? *) 
Abort.

Answer 1

I couldn't figure out any way to do it other than making an assert.

Require Import Arith.

Definition R (a b : nat * nat) := fst a + snd a < fst b + snd b.

Theorem wf_R : well_founded R.
Proof.
  assert (forall n a b, a + b = n -> Acc R (a, b)).
  - induction n as [n H] using lt_wf_ind.
    intros a b H0.
    apply Acc_intro.
    intros [x y].
    unfold R at 1.
    simpl.
    rewrite H0.
    eauto.
  - intros [x y].
    eauto.
Qed.

I guess you could use remember/revert which is functionally equivalent.

Theorem wf_R : well_founded R.
Proof.
  intros [a b].
  remember (a + b) as n.
  revert n a b Heqn.
  induction n as [n H] using lt_wf_ind.
  intros a b H0.
  apply Acc_intro.
  intros [x y].
  unfold R at 1.
  simpl.
  rewrite <-H0.
  eauto.
Qed.

Answer 2

Conceptually, when we prove something by induction on $x$, we lose any hypotheses we had on the particular value of $x$ that we wanted to apply this to.

Otherwise here is the kind of nonsensical reasoning you could do:

We prove by induction that for all $n ≥ 10$ we have $n ≥ 100$.

• For $n = 0$ we are done by contradiction with $n ≥ 10$,
• If $n ≥ 100$ then clearly $n + 1 ≥ 100$.

What is correct is to move the assumptions to what you're proving by induction. Here's how it makes the previous "proof" fail:

We prove that for all $n ≥ 10$, we have $n ≥ 100$. It suffices to prove that for all $n$, we have $n ≥ 10 ⇒n ≥ 100$.

• For $n = 0$, it is true that $n ≥ 10 ⇒ n ≥ 100$ because $n ≥ 10$ is false.
• Assume $n ≥ 10 ⇒ n ≥ 100$. Assume $n + 1 ≥ 10$ and let's prove $n + 1 ≥ 100$. ⟵ Here we are stuck (fortunately!) because we cannot deduce $n ≥ 10$ from $n + 1 ≥ 10$.

In your case, you are trying to do induction on $s$ while preserving the assumption that $s = n + n'$, which doesn't work for the same reason. Instead, what you should do is to move $n, n'$ into the goal that you prove by induction.

Additionally, what you want is induction on $<$, not structural induction on $s$, and also note that your base assumption is redundant because it is subsumed by ind.

Require Import Wf_nat.

Lemma add_2nat_induction
  (f : nat -> nat -> Type)
  (ind : forall z w, (forall x y, x + y < z + w -> f x y) -> f z w) :
  (forall n n', f n n').
Proof.
  enough (forall s n n', s = n + n' -> f n n') as H. {
    intros. apply (H (n + n')). reflexivity.
  }
  induction s as [s IH] using (well_founded_induction_type Wf_nat.lt_wf).
  intros n n' E. apply ind. intros x y Hlt.
  apply (IH (x + y)).
  - rewrite E. exact Hlt.
  - reflexivity.
Qed.

Alternatively, you can use the lemma that the inverse image of a well-founded relation by any function is well-founded, which is in the standard library. The only issue is that your function is nat -> nat -> Type and not (nat*nat) -> Type, so you have to do a bit of currying/uncurrying to actually reach the form you were looking for:

Require Import Wf_nat Wellfounded.Inverse_Image.
  
Lemma add_2nat_induction
  (f : nat -> nat -> Type)
  (ind : forall z w, (forall x y, x + y < z + w -> f x y) -> f z w) :
  (forall n n', f n n').
Proof.
  assert (wf_pairs := wf_inverse_image (nat*nat) nat lt (fun '(x, y) => x + y) Wf_nat.lt_wf).
  set (g := fun '(x, y) => f x y).
  enough (forall p, g p) as H. { intros. exact (H (n, n')). }
  induction p as [p IH] using (well_founded_induction_type wf_pairs).
  destruct p as [z w]. apply ind. intros x y. specialize (IH (x, y)). exact IH.
Qed.

Answer 3

Here is a proof that directly uses well-founded induction:

Lemma add_2nat_induction (P : nat -> nat -> Prop)
    (base : P 0 0) 
    (ind : forall z w, (forall x y, x + y < z + w -> P x y) -> P z w) :
  (forall n n', P n n'). 
Proof.
  intros n n'.
  change ((fun x => P (fst x) (snd x)) (n,n')).
  eapply (well_founded_ind (R := fun x y => (fst x) + (snd x) < (fst y) + (snd y))).
  1: apply wf_inverse_image, lt_wf.

  intros [] IH ; cbn in *.
  apply ind.
  intros.
  now apply (IH (_,_)).
Qed.

Two things to note. First, I had to be quite explicit regarding the bookkeeping happening around the pairing operation. The first change, in particular, is there to help well_founded_ind figure out the property I want to prove by induction. I don't know if there is any way to make that part nicer. Second, I used the standard library lemmas saying that 1) lt is well-founded 2) the inverse image of a well-founded relation is well-founded, so that I don't have to prove well-foundedness by hand.

Also, your base is unnecessary. Indeed, it is a consequence of the "inductive" step:

Lemma base_ind (P : nat -> nat -> Prop) :
  (forall z w, (forall x y, x + y < z + w -> P x y) -> P z w) ->
  P 0 0.
Proof.
  intros ind.
  apply ind.
  intros *.
  lia.
Qed.