The Coq mailing list

[Jean-Yves Vion-Dury <jean-yves.vion-dury AT inrialpes.fr>]

Goal ~(a=b) /\ ~(a=c) /\ ~(b=c).

> Repeat Split;Discriminate



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
>

--

Jean-Yves Vion-Dury   Research Scientist	Xerox Research Centre Europe
INRIA (sabbatical) 655 avenue de l'Europe, 38334 Montbonnot (FRANCE) Jean-Yves.Vion-Dury AT inrialpes.fr	from France:   0 4 76 61 53 83 from abroad: +33 4 76 61 53 83
you may have a look at the Circus Transformation Language?	www.alphaAve.com