The Coq mailing list

[Pierre Casteran <casteran AT labri.fr>]

Yong Luo wrote:
> Dear all,
>
> I am stuck in proving 1 /= 0, ie. one is not equal to zero, ~ (S O) =
> O, where 1 and 0 are Natural Numbers, nat.
>
> I can find any similar proposition in Coq's library of classical logic.
>
> Can anyone give me a hand and tell me how to prove it in Coq?
>
> Thank you.
>
> Yong
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

Hello,

 It's automatic, with the tactic discriminate:

Coq < Theorem zero_one : 1<>0.
1 subgoal

  ============================
   1 <> 0

zero_one < discriminate.
Proof completed.

zero_one < Qed.


If you want to see the proof term Coq build for you, you can print it:

Coq < Print zero_one.
zero_one =
fun H : 1 = 0 =>
let H0 :=
  eq_ind 1
    (fun ee : nat => match ee return Prop with
                     | O => False
                     | S _ => True
                     end) I 0 H in
False_ind False H0
     : 1 <> 0


Pierre

--
Pierre Casteran,
LaBRI, Universite Bordeaux-I      |
351 Cours de la Liberation        |
F-33405 TALENCE Cedex             |
France                            |
tel : (+ 33) 5 40 00 69 31
fax : (+ 33) 5 40 00 66 69
email: Pierre . Casteran @ labri .  fr  (but whithout white space)
www: http://www.labri.fr/Perso/~casteran