The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hi Satrajit ,

Of course you cannot prove foo.
You can even prove its negation:

Theorem foo_false: ~(forall a b:Prop, (a->b)->(b->a)).
Proof.
 intro H;generalize (H False True).
 intro H0; apply H0;auto.
Qed.

Pierre





Le 10/02/2011 00:21, Satrajit Roy a écrit :

Also, I found an exercise in an older book (circa 1990s) which reads something like: prove that (A=>B)=>(B=>A)

I wrote :

Theorem foo: forall a b:Prop, (a->b)->(b->a).
But I cannot prove  foo.

Of course if I write:

Theorem foo':forall a b:Prop, a->(a->b)->(b->a) , it seems logical to assume a and is provable as well.
But it doesn't seem like foo and foo' equivalent, are they?

On Wed, Feb 9, 2011 at 5:51 PM, Satrajit Roy <satrajit.roy AT gmail.com> wrote:

What is the correct way to express statements like the following in the Coq environment?

for all x, exists y such that A(x, y) =>  exists y, for all x such that A(x, y) and the converse of it
--

Satrajit

--

Satrajit