The Coq mailing list

[Donald Sebastian Leung <donaldsebleung AT gmail.com>]

I think you might be confusing the following two propositions:

- It is not the case that P -> Q for any a, b (ex : ~ (forall (a b : A), P -> Q))

- For any given pair of values a, b, P -> Q is decidedly false (ex : forall (a b : A), ~(P -> Q))

The informal proof you gave would work for the former example while you are asking for a proof of the latter example.

~ Donald

Kumar, Ashish <azk640 AT psu.edu> 於 2020年9月19日 週六 上午9:44寫道：

Suppose I have a theorem of the form:
Theorem ex: forall (a b: A), ~(P -> Q).
(where A has type 'Type' defined earlier, and a and b are used in the propositions P and Q.)

How do I go about proving this?
I realize that an informal proof for this would involve me showing there exists some value a and b, where P holds but Q does not hold i.e. informally, I would be proving the lemma ex2: exists (a b: A), P /\ ~Q. How can I prove ex2 from ex1 in Coq??

With regards,
Ashsih