coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Showing proof of type ~(P -> Q)?

From: "River Dillon" <lists AT pitype.org>
To: <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Showing proof of type ~(P -> Q)?
Date: Fri, 18 Sep 2020 20:03:17 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=lists AT pitype.org; spf=Pass smtp.mailfrom=lists AT pitype.org; spf=None smtp.helo=postmaster AT out0.migadu.com
Ironport-phdr: 9a23:dniS1BAs6loi2NkxQsl7UyQJP3N1i/DPJgcQr6AfoPdwSPvzr8bcNUDSrc9gkEXOFd2Cra4d1KyO7Ou+ASRAuc/H7ClcNsQUFlcssoY/p0QYGsmLCEn2frbBThcRO4B8bmJj5GyxKkNPGczzNBX4q3y26iMOSF2kbVImbuv6FZTPgMupyuu854PcYxlShDq6fLh+MAi6oR/eu8ULg4ZuMLo9xxnGrnZJZ+hd2GdkKU6Okxrm6cq84Z9u/z5Mt/498sJLTLn3cbk/QbFEFjotLno75NfstRnNTAuP4mUTX2ALmRdWAAbL8Q/3UI7pviT1quRy1i+aPdbrTb8vQjSt871rSB7zhygZMTMy7XzahdZxjKJfpxKhugB/zovJa4ybKPZyYqXQds4cSGFcXMheSjZBD5uzYYQTEeQPIOZWoYf+qVQMtha+GRCsCfnzxjNUmnP736s32PkhHwHc2wwgGsoDvHrIotX0KqcdT/q1x7TGwzXCa/NW3TD96I7Gfhs8pvyMWbNwcdHNyUk0DA7FllSQqZDlPjONyOsBqW+b7/BvVe+2jWMstg5+rCS1yMg2lonJmpwaykrC9Shh3Ys7KtO1Rk50bNCkDZddtCOXOol2TM4/TW9lvCY0xqMJt5KmciYH1pQpywPfZfGGb4SF4wzuWPiQLDl2mn9odrSyjAux/0i40uDxUsa53ExUoidLiNXAq2oB2wHP5sWJTPZ2412v1iyV1w/J7+FJOUA0mrTfK54m2rMwkYcTsVjfEiPsnUX2jaCWeV859ei18ejofrLmppqEO491jAHxLLgul9S7DOk3KAQCQWaW9f6h2LH54EH1XLtHguUzkqbDsZDaIcobprS+Aw9Qyosj7xe/Dyy60NQDhnQHNFNFeA6HjojxJV7COvf4De2wg1i0ijdk2+jGPqH9ApXKNnXMjLDhfa9k50FAzAoz0MtQ6olPCrABJfLzQlX+uMbZDh8/KQy0wvzoBM9z1oMECiqzBfrNO6TL9FSM++gHIu+WZYZTtiyreNY/4Pu7x0U4h1IHNYWo2Z8QbjrwSvBnOFmCSWLtnsYZHCENpAVoH7+is0GLTTMGPyX6ZKk7/DxuUNv6X7eGfZikhfm65An+BodfPzoUElGQAG/lMYKeVKVUMX/AEopaijUBEIOZZcoh2BWp7VCozKd7dqzR+yIRuY+l399wtbWKxEMCsAdsBsHY6FmjCmR9n2cGXTgzhfotuU1h20+Ol69ijK4BGA==

Hi Ashsih,

Examining the definition of negation:

Print "~".
> not = fun A : Prop => A -> False
> : Prop -> Prop

We see that ~A is defined to be A -> False.

So to prove ~(P -> Q), we must show that (P -> Q) -> False. (You can use
`unfold not` to make this explicit.)

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

No. Unfolding the definition of negation again, we see

P -> ~Q

is equivalent to

P -> (Q -> False)

which is not equivalent to

(P -> Q) -> False

because implication is not necessarily associative.

River

[Coq-Club] Showing proof of type ~(P -> Q)?, Kumar, Ashish, 09/19/2020
- Re: [Coq-Club] Showing proof of type ~(P -> Q)?, Donald Sebastian Leung, 09/19/2020
  - Re: [Coq-Club] Showing proof of type ~(P -> Q)?, Kumar, Ashish, 09/19/2020
    - Re: [Coq-Club] Showing proof of type ~(P -> Q)?, River Dillon, 09/19/2020
    - Re: [Coq-Club] Showing proof of type ~(P -> Q)?, Daniel Kuhse, 09/19/2020