The Coq mailing list

[Pierre Casteran <casteran AT labri.fr>]

GANGCHEN5 AT aol.com
 wrote:
> Hello,
>
> Given an inductive definition:
>
> Inductive A : Set := a : A | b : A | c : A.
>
> I want to prove that each pair of two constructors are
> different. Here is a proof following the method proposed in the book CoqArt:
>
> Lemma ineq : ~a=b.
> Proof.
> Unfold not; Intros H; Change ([o:A]Cases o of a => True | _ => False end 
> b);Rewrite <- H; Trivial.
> Qed.
>
> Question:
> Are there simpler or general proofs for this problem ?
>
> With the above method, each lemma ~x=y needs a slightly different proof.
>
>
> Thanks.
>
> gang chen

It's better to use the "discriminate" tactic.

Lemma ineq : a <> b.
Proof.
  Unfold not ; Discriminate 1.
Qed.

Then all lemmas have the same proof.

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