1 ≠ 0

by Matthias Puech

Learning Coq is usually an enlightening experience. I know it first-hand, it can also be a quite frustrating one, because it seems at first to involve remembering quite a lot of arbitrarily-named tactics, that one might not fully understand the effect of. discriminate is one of them: “if you’re faced with an obvious inequality, just apply discriminate” they say. If you look at the proof term, however, it is far from trivial and involves a “trick”, a kind of “lie” that Pierre has become a specialist of. There is an intermediate step in the comprehension, that we put together with Chantal: decomposing the proof generated by discriminate. Here is a very easy proof that 1 ≠ 0, which does not require to understand neither proof terms nor return clauses in pattern-matching. Pure beginner Coq.

It goes like this (in a very pedestrian style):

Definition isZero x :=
  match x with
    | O => True
    | S _ => False

Lemma one_is_not_zero : ~ isZero 1.
  simpl. intro H. destruct H.

Lemma zero_is_zero : isZero 0.
  simpl. exact I.

(* By contradiction: suppose 1 = 0. Since 0 is null,
then so is 1. But by definition, 1 is not null, hence contradiction.  *)
Lemma zero_differs_from_one :  1 <> 0.
  intro H.
  apply one_is_not_zero.
  rewrite H.
  exact zero_is_zero.

Play this proof step-by-step to discover the “lie”, that resides in the rewriting step.

About these ads