The Coq mailing list

[Pierre Cast�ran <pierre.casteran AT labri.fr>]

Quoting David de Villiers 
<davidc1 AT ananzi.co.za>:

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

Hello,
 The example page 118 is *NOT* about proving some contradiction, but
about using (i.e. eliminating) some contradiction for deriving any statement.

In general, this kind of argument is used within a section, as in the example
you point out. This particular example is a proof of the proposition
False -> 220=284, the proof term of which is
(fun ff:False => False_ind (220=284) ff)



> It is unsatisfactory because I tried the following and
> noticed the identicality.
>
> Lemma ex1: 220=220.
> Proof.
>   apply False_ind.
>   exact ff.
> Qed.

Ok, False -> 220=220 is also provable,

We can give a proof-term similar to the preceding one:
(fun ff:False => False_ind (220=220) ff)

But, since 220=220 is always provable, you can get another proof
which doesn't use any specific property of False.

Check (fun (p: False) => refl_equal 220).
False -> 220=220

 Notice that any proposition of the form P->220=220 is also
provable, with the proof-term (fun (p:P) => refl_equal 220)


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

Well, If you want to prove some proposition X is false, you simply
have to prove ~X  (i.e. X -> False).

But don't confound ~X (X -> False)  with False -> X,
False -> X is always provable, for any proposition X, so does not express
anything about X.



Pierre



> Ciao.
> David.
>
> --------------------------------------------------------
> 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



Pierre Castéran