coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Re: How to prove two constructors are different (GANGCHEN5 AT aol.com)

From: Yves Bertot <Yves.Bertot AT sophia.inria.fr>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Re: How to prove two constructors are different (GANGCHEN5 AT aol.com)
Date: Mon, 22 Sep 2003 08:52:09 +0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

The proof term is always slightly different, but there is a specific
tactic that was designed for this very purpose: Discriminate.

Inductive A : Set := a : A | b : A | c : A.

Lemma ineq1 : ~a=b.
Proof.
Discriminate.
Qed.

Lemma ineq2 : ~b=c.
Proof.
Discriminate.
Qed.

Lemma ineq3 : ~c=a.
Proof.
Discriminate.
Qed.

[Coq-Club] Re: How to prove two constructors are different (GANGCHEN5 AT aol.com), Yves Bertot