Skip to Content.
Sympa Menu

coq-club - [Coq-Club]proven false

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club]proven false


chronological Thread 

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





Archive powered by MhonArc 2.6.16.

Top of Page