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

Question

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:

1. le_n which takes any natural number and constructs a proof of le n n.
2. 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?

Answer 1

The problem is that the induction or elim tactic forgets about the fact that in le n 0, the second argument is 0. Two cases are possible, either the proof of le n 0 is le_n or the proof is le_S. In fact, the second case is not possible because 0 <> S n but the tactic won't know that.

inversion is closer to destruct that to induction in that it will not give you any induction hypothesis. It will look at all the constructors of the proposition you gave it, and see which ones could lead to it. And this times, it's smart and sees that le_S only applies if you have 0 <> S n and discards it.

A way to do it by hand is to simply force Coq to remember that the second argument is 0.

Lemma tricky : forall n, le n 0 -> n = 0.
Proof.
  assert (h : forall n m, m = 0 -> le n m -> n = 0).
  { intros n m e h.
    induction h.
    - assumption.
    - discriminate.
  }
  intros n hyp.
  eapply h.
  - reflexivity.
  - assumption.
Qed.

As you can see, I generalise the lemma by adding an equality. The discriminate tactic allows you conclude a goal from an absurd hypothesis such as 0 = S n.

Answer 2

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.

Answer 3

A short proof using SSReflect can be designed, following Théo's approach while swapping the two hypotheses of h:

Lemma tricky n (len0 : le n 0) : n = 0.
Proof.
  have h m : le n m -> m = 0 -> n = 0 by elim. 
  exact: (h 0).
Qed.    

Answer 4

When you destruct the assumption n <= 0, Coq forgets that the right hand value was 0 and asks you to prove the second step for an arbitrary value m.

So, you must remember that the value was actually 0. Then you will have enough information to get the contradictory assumption "S m = 0" in the second case.

Goal forall n, n <= 0 -> n = 0.
  remember 0 as m. 
  destruct 1. 
  - reflexivity.
  - pose proof (I : match S m with S _ => True | 0 => False end) as HF.
    rewrite Heqm in HF.
    apply False_ind, HF.
Qed.