coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "David de Villiers" <davidc1 AT ananzi.co.za>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club]proven false
- Date: Tue, 19 Dec 2006 20:40:29 +0200
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hi,
I have been searching for a way to prove a statement false.
In the CoqArt book, p118 is the following unsatisfactory
example:
Hypothesis ff:False.
Lemma ex1: 220=284.
Proof.
apply False_ind.
exact ff.
Qed.
It is unsatisfactory because I tried the following and
noticed the identicality.
Lemma ex1: 220=220.
Proof.
apply False_ind.
exact ff.
Qed.
My idea runs as follows:
Prove that:
True XOR X, and you have proven X false.
For XOR I use the following logically equivalent
formulation:
(True /\ ~X) \/ (X /\ ~True).
The result:
Theorem no_eq: (True /\ ~(7=11)) \/ ((7=11) /\ False).
Proof.
auto.
Qed.
Any other ideas?
Ciao.
David.
It's holiday season again! Time for family and fun! For a cheap and efficient
way to keep in touch this festive season send sms's from your Ananzi mail
account to anywhere in the world from just 40c!
http://www.swiftsms.co.za/swiftT/track.asp?e=*em*&cid=113&u=8&tid=1424
- [Coq-Club]proven false, David de Villiers
- Re: [Coq-Club]proven false, Arnaud Spiwack
- Re: [Coq-Club]proven false, Pierre Castéran
Archive powered by MhonArc 2.6.16.