Using dependent induction tactic to keep information while doing induction

Question

I have just run into the issue of the Coq induction discarding information about constructed terms while reading a proof from here.

The authors used something like:

remember (WHILE b DO c END) as cw eqn:Heqcw.

to rewrite a hypothesis H before the actual induction induction H. I really don't like the idea of having to introduce a trivial equality as it looks like black magic.

Some search here in SO shows that actually the remember trick is necessary. One answer here, however, points out that the new dependent induction can be used to avoid the remember trick. This is nice, but the dependent induction itself now seems a bit magical.

I have a hard time trying to understand how dependent induction works. The documentation gives an example where dependent induction is required:

Lemma le_minus : forall n : nat, n < 1 -> n = 0.
forall n : nat, n < 1 -> n = 0

I can verify how induction fails and dependent induction works in this case. But I can't use the remember trick to replicate the dependent induction result.

What I tried so far to mimic the remember trick is:

Require Import Coq.Program.Equality.

Lemma le_minus : forall n : nat, n < 1 -> n = 0.
forall n : nat, n < 1 -> n = 0
Proof.
forall n : nat, n < 1 -> n = 0
  intros n H. (* dependent induction H works*)
n: nat
H: n < 1
n = 0
  remember (n < 1) as H0.
n: nat
H0: Prop
HeqH0: H0 = (n < 1)
H: H0
n = 0 induction H.
Not an inductive product.
n: nat
H0: Prop
HeqH0: H0 = (n < 1)
H: H0
n = 0

But this doesn't work. Anyone can explain how dependent induction works here in terms of the remember-ing?

A: As indicated in the documentation, dependent induction is defined in Coq.Program.Equality. You can dig through its guts to see how it works.

Answer

You can do

Require Import Coq.Program.Equality.

Lemma le_minus : forall n : nat, n < 1 -> n = 0.
forall n : nat, n < 1 -> n = 0
Proof.
forall n : nat, n < 1 -> n = 0
  intros n H.
n: nat
H: n < 1
n = 0
  remember 1 as m in H.
n, m: nat
Heqm: m = 1
H: n < m
n = 0 induction H.
n: nat
Heqm: S n = 1
n = 0
n, m: nat
Heqm: S m = 1
H: S n <= m
IHle: m = 1 -> n = 0
n = 0
  -
n: nat
Heqm: S n = 1
n = 0 inversion Heqm.
n: nat
Heqm: S n = 1
H0: n = 0
0 = 0 reflexivity.
  -
n, m: nat
Heqm: S m = 1
H: S n <= m
IHle: m = 1 -> n = 0
n = 0 inversion Heqm.
n, m: nat
Heqm: S m = 1
H: S n <= m
IHle: m = 1 -> n = 0
H1: m = 0
n = 0 subst m.
n: nat
IHle: 0 = 1 -> n = 0
H: S n <= 0
Heqm: 1 = 1
n = 0
    inversion H.
Qed.

As stated here, the problem is that Coq cannot keep track of the shape of terms that appear in the type of the thing you are doing induction on. In other words, doing induction over the "less than" relation instructs Coq to try to prove something about a generic upper bound, as opposed to the specific one you're considering (1).

Notice that it is always possible to prove such goals without remember or dependent induction, by generalizing your result a little bit:

Lemma le_minus_aux :
  forall n m, n < m ->
              match m with
              | 1 => n = 0
              | _ => True
              end.
forall n m : nat,
n < m -> match m with
         | 1 => n = 0
         | _ => True
         end
Proof.
forall n m : nat,
n < m -> match m with
         | 1 => n = 0
         | _ => True
         end
  intros n m H.
n, m: nat
H: n < m
match m with
| 1 => n = 0
| _ => True
end destruct H.
n: nat
match n with
| 0 => n = 0
| S _ => True
end
n, m: nat
H: S n <= m
match m with
| 0 => n = 0
| S _ => True
end
  -
n: nat
match n with
| 0 => n = 0
| S _ => True
end destruct n; trivial.
  -
n, m: nat
H: S n <= m
match m with
| 0 => n = 0
| S _ => True
end destruct H; trivial.
Qed.

Lemma le_minus : forall n, n < 1 -> n = 0.
forall n : nat, n < 1 -> n = 0
Proof.
forall n : nat, n < 1 -> n = 0
  intros n H.
n: nat
H: n < 1
n = 0
  apply (le_minus_aux n 1 H).
Qed.