How to prove forall n:nat, ~n<n in Coq?

Question

I've been confused for hours and I cannot figure out how to prove

forall n:nat, ~n<n

in Coq. I really need your help. Any suggestions?

Answer 1

This lemma is in the standard library:

Require Import Arith.
Lemma not_lt_refl : forall n:nat, ~n<n.
Print Hint.

Amongst the results is lt_irrefl. A more direct way of realizing that is

info auto with arith.

which proves the goal and shows how:

intro n; simple apply lt_irrefl.

Since you know where to find a proof, I'll just give a hint on how to do it from first principles (which I suppose is the point of your homework).

First, you need to prove a negation. This pretty much means you push n<n as a hypothesis and prove that you can deduce a contradiction. Then, to reason on n<n, expand it to its definition.

intros h H.
red in H.   (* or `unfold lt in H` *)

Now you need to prove that S n <= n cannot happen. To do this from first principles, you have two choices at that point: you can try to induct on n, or you can try to induct on <=. The <= predicate is defined by induction, and often in these cases you need to induct on it — that is, to reason by induction on the proof of your hypothesis. Here, though, you'll ultimately need to reason on n, to show that n cannot be an m^th successor of S n, and you can start inducting on n straight away.

After induction n, you need to prove the base case: you have the hypothesis 1 <= 0, and you need to prove that this is impossible (the goal is False). Usually, to break down an inductive hypothesis into cases, you use the induction tactic or one of its variants. This tactic constructs a fairly complex dependent case analysis on the hypothesis. One way to see what's going on is to call simple inversion, which leaves you with two subgoals: either the proof of the hypothesis 1 <= 0 uses the le_n constructor, which requires that 1 = 0, or that proof uses the le_S constructor, which requires that S m = 0. In both cases, the requirement is clearly contradictory with the definition of S, so the tactic discriminate proves the subgoal. Instead of simple inversion H, you can use inversion H, which in this particular case directly proves the goal (the impossible hypothesis case is very common, and it's baked into the full-fledged inversion tactic).

Now, we turn to the induction case, where we quickly come to the point where we would like to prove S n <= n from S (S n) <= S n. I recommend that you state this as a separate lemma (to be proved first), which can be generalized: forall n m, S n <= S m -> n <= m.

Answer 2

Require Import Arith.
auto with arith.