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 end. Lemma one_is_not_zero : ~ isZero 1. simpl. intro H. destruct H. Qed. Lemma zero_is_zero : isZero 0. simpl. exact I. Qed. (* 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. Qed.
Play this proof step-by-step to discover the “lie”, that resides in the rewriting step.