The Coq mailing list

[Daniel Kuhse <daniel.kuhse AT tu-dortmund.de>]

 I don't think there is generally any real way around proving the statement directly (i.e. proving that for all a b, both P and ~Q hold).

By the way, is it true that if I prove ex3: forall a b, P -> ~Q, then from ex3, I can prove ex?

Counterexample: Assume for all a b, ~P holds, then ex3 holds, but not ex since both P->~Q and P-> Q hold due to ~P

---

Daniel Kuhse

By the way, is it true that if I prove ex3: forall a b, P -> ~Q, then from ex3, I can prove ex?

By the way, is it true that if I prove ex3: forall a b, P -> ~Q, then from ex3, I can prove ex?

Am Sa., 19. Sept. 2020 um 04:39 Uhr schrieb Kumar, Ashish <azk640 AT psu.edu>:

Actually I do have to show theorem ex (i.e. theorem ex is correct).

But, your answer makes me realize that my informal proof was incorrect. Any ideas?
By the way, is it true that if I prove ex3: forall a b, P -> ~Q, then from ex3, I can prove ex?

With regards,
Ashish

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Donald Sebastian Leung <donaldsebleung AT gmail.com>
Sent: Friday, September 18, 2020 10:31 PM
To: coq-club AT inria.fr <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Showing proof of type ~(P -> Q)?

 

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