The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Hi,
There is in Coq a negation primitive : ~A meaning "A is false" (or "not 
A" whichever way you prefer it said).

It is the intuitionistic negation, namely ~A is equal by definition to 
A->False. And I believe that is what you were looking for.

Exemples of use :

Goal ~42=18.
discriminate.
Qed.


Goal forall A:Prop, (A->~A)->~A.
 intros.
 intro.
 apply H; assumption.
Qed.


Arnaud Spiwack

David de Villiers a écrit :
> 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
>
> --------------------------------------------------------
> 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
>
>
>