Contradiction on natural number's zero test

Question

I have a natural number that is not equal to zero. I want to prove that if it is equal to zero then it give false.

Lemma notzero : forall n, n <> 0 -> (n =? 0) = false.forall n : nat, n <> 0 -> (n =? 0) = false
Proof.forall n : nat, n <> 0 -> (n =? 0) = false
  intros n H.n: nat
H: n <> 0
(n =? 0) = false inversion H.The type of H is not inductive.
n: nat
H: n <> 0
(n =? 0) = false

Answer (larsr)

Instead of using inversion in every proof, I find that the proofs are more maintainable in the long run if you use boolean reflection. The libraries have many useful lemmas that you can use, they often are called something with "reflect", "decide", "dec" or "spec" as in specification, so you can i.e. search for lemmas related to < with Search (_ < _) "spec".

The reflection lemmas are designed to at the same time 1) destruct the boolean term in your proof context, and 2) add the corresponding Prop to your context, making it easy to then use lia, omega, etc. to finish the proof.

In your case, you can use Nat.eqb_spec (from Require Import PeanoNat.). Do

  destruct (Nat.eqb_spec n 0).n: nat
H: n <> 0
e: n = 0
true = false
n: nat
H, n0: n <> 0
false = false

It will create two branches, in one n ?= 0 is replaced with true and n = 0 is added to the context, and in the other n =? 0 is replaced with false and n <> 0 is added to the context. It is now very easy to finish of the proof, as the first goal's context contains the contradiction n = 0 and n <> 0, and the second goal is false = false. You can use the automation tactical now, so the complete proof is

  now destruct (Nat.eqb_spec n 0).

If you want to use integers Z, instead, the proof becomes now destruct (Z.eq_spec n 0).. as the Z module has many of the corresponding lemmas with matching names.

Answer (Théo Winterhalter)

Generally, you can use the fact that =? reflects equality on natural numbers (Nat.eqb_spec). Are you using the two notions of equality on purpose? Note that n <> 0 is a notation for n = 0 -> False.

Lemma notzero : forall n, n <> 0 -> (n =? 0) = false.forall n : nat, n <> 0 -> (n =? 0) = false
Proof.forall n : nat, n <> 0 -> (n =? 0) = false
  intros n h.n: nat
h: n <> 0
(n =? 0) = false destruct (Nat.eqb_spec n 0).n: nat
h: n <> 0
e: n = 0
true = false
n: nat
h, n0: n <> 0
false = false
  -n: nat
h: n <> 0
e: n = 0
true = false exfalso.n: nat
h: n <> 0
e: n = 0
False apply h.n: nat
h: n <> 0
e: n = 0
n = 0 assumption.
  -n: nat
h, n0: n <> 0
false = false reflexivity.
Qed.

There is also the possibility of simply doing an analysis on n. If it is 0 then you can use your hypothesis to conclude, and if it is some S m then your goal will be provable by reflexivity.

Lemma notzero : forall n, n <> 0 -> n =? 0 = false.forall n : nat, n <> 0 -> (n =? 0) = false
Proof.forall n : nat, n <> 0 -> (n =? 0) = false
  intros n h.n: nat
h: n <> 0
(n =? 0) = false destruct n.h: 0 <> 0
(0 =? 0) = false
n: nat
h: S n <> 0
(S n =? 0) = false
  -h: 0 <> 0
(0 =? 0) = false contradiction.
  -n: nat
h: S n <> 0
(S n =? 0) = false reflexivity.
Qed.