### 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.

I’ve not heard of COG – thanks.

Nice, but a bit verbose. The solution, which is essentially from the Coq’Art book (Section 6.2.2.2), boils down to exploiting the rewriting by equality, which is way much simple when relying to computable functions constructed on site. Here is the same example in three lines without any additional lemmas (using SSReflect notation):

Lemma one_isnt_zero: 1 0.

Proof.

move=>E.

have X: if 1 == 0 then True else False by rewrite E; constructor.

exact X.

Qed.

Could be done even shorter, but I wanted to emphasise that no ‘simp’ magic and implicit assumption search is employed here.

Hi Ilya, thanks for your solution. It *is* actually shorter… but let me point out that first, contrarily to my solution, it relies on boolean equality (==), which is a “computable function constructed on site”; my two ad-hoc lemmas kind of specialize this function for my purpose; and secondly, your proof has a “cut” (the “have”), i.e. essentially an additional lemma. Would you agree with this? I was not particularly looking for concision, but for a decomposition of “discriminate” that would be understandable by beginners.

I agree that having a hypothesis ‘X’ could be lifted to a separate lemma.

I don’t quite understand the concern about relying on the boolean equality, though. In general, I try to follow the pattern that the computable functions should be written as such and ‘bool’ should be preferred to ‘Prop’ in the case of computable predicates. To me, as a beginner, it helps to avoid a lot of burden of inductive reasoning just by doing simple rewritings. This is, of course, not to be demonstrated on this example, which is already simple enough. :)

Ilya, relying on boolean equality is not a “concern”, of course. I agree 100% with you about bool vs. Prop, but as you said, it’s a design pattern, not something required to understand Coq. To teach Coq (or anything for that matter), I think it’s better to first understand the rules of the game, then repeat boring things 10 times and only then abstract from them, e.g. with a design pattern. But it’s just my style of teaching (and O. Danvy’s, which lecture is where the need for this small proof originated from).