coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] RE: Coq-club digest, Vol 1 #201 - 1 msg

From: "TAVERNIER Bertrand" <bertrand.tavernier AT criltechnology.com>
To: <coq-club AT pauillac.inria.fr>
Cc: <GANGCHEN5 AT aol.com>
Subject: [Coq-Club] RE: Coq-club digest, Vol 1 #201 - 1 msg
Date: Mon, 22 Sep 2003 10:07:04 +0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hello,

Just try using "Discriminate" for that kind of goal

Sincerly,

~Bertrand Tavernier

-----Message d'origine-----
De :
coq-club-request AT pauillac.inria.fr
[mailto:coq-club-request AT pauillac.inria.fr]
Envoy� : samedi 20 septembre 2003 12:01
� :
coq-club AT pauillac.inria.fr
Objet : Coq-club digest, Vol 1 #201 - 1 msg

Send Coq-club mailing list submissions to

coq-club AT pauillac.inria.fr

To subscribe or unsubscribe via the World Wide Web, visit
 http://pauillac.inria.fr/mailman/listinfo/coq-club
or, via email, send a message with subject or body 'help' to

coq-club-request AT pauillac.inria.fr

You can reach the person managing the list at

coq-club-admin AT pauillac.inria.fr

When replying, please edit your Subject line so it is more specific
than "Re: Contents of Coq-club digest..."

Today's Topics:

 1. How to prove two constructors are different
(GANGCHEN5 AT aol.com)

--__--__--

Message: 1
From:
GANGCHEN5 AT aol.com
Date: Fri, 19 Sep 2003 15:28:59 EDT
To:
coq-club AT pauillac.inria.fr
Subject: [Coq-Club] How to prove two constructors are different

--part1_125.25b6d868.2c9cb2fb_boundary
Content-Type: text/plain; charset="US-ASCII"
Content-Transfer-Encoding: 7bit

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

--part1_125.25b6d868.2c9cb2fb_boundary
Content-Type: text/html; charset="US-ASCII"
Content-Transfer-Encoding: quoted-printable

<HTML><BODY BGCOLOR=3D"#ffffff">Hello, 
 
Given an inductive definition: 
 
Inductive A : Set :=3D 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=3Db. 
Proof. 
Unfold not; Intros H; Change ([o:A]Cases o of a =3D> True | _ =3D> Fal=
se end b);Rewrite <- H; Trivial. 
Qed. 
 
Question: 
Are there simpler or general proofs for this problem ? 
 
With the above method, each lemma ~x=3Dy needs a slightly different proof.<B=
R>
 
 
Thanks. 
 
gang chen 
</HTML>
--part1_125.25b6d868.2c9cb2fb_boundary--

--__--__--

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

End of Coq-club Digest

[Coq-Club] RE: Coq-club digest, Vol 1 #201 - 1 msg, TAVERNIER Bertrand