Is it possible to prove `forall n: nat, le n 0 -> n = 0.` in Coq without using inversion?

In the official coq tutorial they define the following inductive definition of less than or equal to:

Inductive le (n : nat) : nat -> Prop :=
          | le_n : le n n
          | le_S : forall m : nat, le n m -> le n (S m).

My understanding of this is that it is defining two type constructors:

le_n which takes any natural number and constructs a proof of le n n.
le_S which takes any natural number m, a proof of le n m and constructs a proof of le n (S m)

So far so good. However, they then proceed to introduce the following lemma and proof

Lemma tricky : forall n:nat, le n 0 -> n = 0.
Proof.
  intros n0 H.
  inversion H.
  trivial.
Qed.

The 'inversion' step is where I am getting confused. I understand that there is no way to construct le n 0 unless n is equal to 0, since 0 has no successor, but I am not sure at how the inversion tactic figures this out.

To try and understand what it was doing better, I attempted to prove this lemma without using the inversion tactic. However, all of my attempts so far (i.e. using elim on n0, and on H, trying to use the fact that forall n : nat, 0 <> S n., etc.) have failed.

Although my 'Computer science' brain is completely fine with this reasoning, my 'mathematician brain' is having a little bit of trouble accepting this, since there is no hypothesis that this is the only way to construct an inhabitant of le. This made me think that perhaps using the inversion tactic was the only way to do this.

Is it possible to prove this lemma without the inversion tactic? If so, how can it be done?

Solution

It is possible to prove this lemma without inversion: the important point is to do induction (elimination) on the appropriate goal.

First note that when you apply elim on a hypothesis of type le n 0, what's happening underneath is that Coq will apply the elimination principle associated with le. Here that elimination principle is called le_ind and you can query its type:

forall (n : nat) (P : nat -> Prop),
       P n ->
       (forall m : nat, n <= m -> P m -> P (S m)) ->
       forall n0 : nat, n <= n0 -> P n0

This might be a bit intimidating but the important point is that in order to prove a goal P n0 out of an hypothesis n <= n0 you need to consider two cases, one for each constructor of le.

So how does that help with your issue ? With an hypothesis n <= 0, this means that your goal should be of the shape P(n0) with n0 := 0. Now considering that you want to prove n = 0, what should be the shape of P ? You could try to take the simplest solution P(n0) := n = 0 (and that's actually what Coq is doing if you call directly elim H in your code) but you are then unable to prove any of your two cases. The problem is that with this choice of P(n0) := n = 0 you are forgetting about the value of n0 so you cannot use that it is equal to 0. The solution to that problem is exactly to remember that n0 is 0, that is to set P(n0) := n0 = 0 -> n = 0.

How do we do that in practice ? Here is one solution:

Goal forall n, le n 0 -> n = 0.
Proof.
  intros n H.
  remember 0 as q eqn: Hq. (* change all the 0s to a new variable q and add the equation Hq : q = 0 *)
  revert Hq. (* now the goal is of the shape q = 0 -> n = 0 and H : le n q *)
  elim H.
  - intros; reflexivity. (* proves n = n *)
  - intros; discriminate. (* discriminates S m = 0 *)
Qed.

All this work of generalizing 0 is actually what inversion is trying to do for you.

Note that the predicate P that I propose is not the only possible solution. Another interesting solution is based on match (the keyword is small-scale inversions) with P(n0) := match n0 with 0 => n = 0 | S _ => True end. Also, tactics are always producing bare gallina terms in the end, so you can always (at least theoretically) write a term that proves the same thing as any tactic. Here's an example using Coq's powerful albeit verbose pattern-matching:

Definition pf : forall n, le n 0 -> n = 0 :=
  fun n H =>
    match H
          in le _ q
          return match q return Prop with
                 | 0 => n = q
                 | S _ => True
                 end
    with
    | le_n _ => match n with 0 => eq_refl | S _ => I end
    | le_S _ _ _ => I
    end.

EDIT: Simplifying the tactic script using the remember tactic. The original proposition was reimplementing remember by hand:

set (q := 0). (* change all the 0s in the goal into q and add it as hypothesis *)
  intro H.
  generalize (eq_refl : q = 0). (* introduce q = 0 *)
  revert H.
  generalize q ; clear q.  (* generalizes q *)
  (* Now the goal is of the shape
     forall q : nat, n <= q -> q = 0 -> n = q
     and we can apply elim *)
  intros q H ; elim H.