Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
    < Chronological >      < Thread >
  • From: "Kumar, Ashish" <azk640 AT psu.edu>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Showing proof of type ~(P -> Q)?
  • Date: Sat, 19 Sep 2020 02:39:14 +0000
  • Accept-language: en-US
  • Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=psu.edu; dmarc=pass action=none header.from=psu.edu; dkim=pass header.d=psu.edu; arc=none
  • Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=axPQ6wTWrsWtzPoPm4C4mfCPhqpW+OhhB8vKVng7hRw=; b=kFeVgYzQ4snT7lctjRYhXTkzuQjSCebHzxkn57iCNqKUQ6RpbGDnWXS82AXhiW0oQ3hloOpHSQZ27Y/aLGAd549qmi6CRpo7YUWs9ZCtAgAvBa6sA6rcB+0EuNkV+Qh2fTXI+8OKEmM3G6xreDHTboHIcbojkMIt64jVJJXuuqzNB4eD1YT04U1vILqv60bpQmyTj/zxZ6y9SsnmBgbY5LOLalxhe80D+Y8pZa+mI95at/VPaS7+qDP7rhuyVtnrGkyiOjj0pMN9a5G4AxJqK1SbNdYJSjRzfxGDhJQnyAG7GOsxjhmB0N/p/D8qVpYgxMlVzzkZEXcV4Rk5Fb51AA==
  • Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=Q6En5ACnczDsI2ckoGOIHU2i+CrfCv2hC1tddMUWGZmn7fO/qZ9Wzb6yxeamO1g3rKal33X+Lx7Ag8GaMgexUmeDPfdj57qABLHo8d+YZYKyFCc7YehbpZ6Wqg/WnnrT80Lf0rKFGzRX3f2jNrG7sfqjlD3/f74vcwuKEy7lyuJwNHEPVSA8J3tjaCTywmLk4JWU2MMwNjh3YjagfPUKWsFa0iehnaBMqO/K+kbXmE49sBoGcb3hSoa+XjneoKMTpEV+/baULhQqigdFngOJ+5cKoQB2izGsM1wMM9nZNmND3Fkd5l8KKaBL15dBgcEKWT3Ie21CMGZVOuNNTmUvHA==
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=azk640 AT psu.edu; spf=Pass smtp.mailfrom=azk640 AT psu.edu; spf=Pass smtp.helo=postmaster AT NAM12-BN8-obe.outbound.protection.outlook.com
  • Ironport-phdr: 9a23:Eo4H9RLLFxbvRCf6+NmcpTZWNBhigK39O0sv0rFitYgfLvvxwZ3uMQTl6Ol3ixeRBMOHsq0C07Wd7fioGTRZp8rY7jZaKN0EfiRGoP1epxYnDs+BBB+zB9/RRAt+Iv5/UkR49WqwK0lfFZW2TVTTpnqv8WxaQU2nZkJ6KevvB4Hdkdm82fys9J3PeQVIgye2ba9vIBmsogjdq8sbjZF+JqszxRfEo2dEcPlSyW90OF6fhRnx6tqx8ZJ57yhcp/ct/NNcXKvneKg1UaZWByk8PWAv483ruxjDTQ+R6XYZT24bjBlGDRXb4R/jRpv+vTf0ueR72CmBIM35Vqs0Vii476dqUxDnliEKPCMk/W7Ni8xwiKVboA+9pxF63oXZbp2ZOOZ4c6jAe94RWGhPUdtLVyFZAo2ycZYBD/YPM+hboYnypVoOogexCgS3Huzj1iNEi2Xq0aEmyessFxzN0gw6H9IJtXTZtNv5OqIPUeCw1qbI1y3PZO5K1Dfm6IjIcwshofGCUbltdsfe00guFwDEg1iftYDoJCuV1v8Qs2SB8eVvSP+vhnchpgpsrTeh2t0ihZPVhoIJ1F/E7yN5zZ41KNClVEJ2YcCpHZ9QuS2ENYZ7QcEvT31otis617ALu5+2cSYJxZknxxDSa+KLfpSK7x/nVuucPzN1inx7db6igRu57EuuyvXkW8S7zFpGtDdJnsXOu3wXyRDe5MqKRuFg8ku9xTqDzx3f5v1LLEwum6fWKIQtz7EumpYJsEnPAzf6lFv3gaOKeEgp//Wk5/j8bbjno5KQKZN4hwL7P6kunsGyBOE1PhUTU2Wd5O+yzqfs/VfjT7VPlvA2krfWsJTdJckDvqC0Hwhb3ps95xqmEjqoyNcVkWAALF1eZh2LlY/pO0zSIP/jCve/nlKsnypxy/DeJL3hBYnNIWbfn7f9fLZ97EhcxBA0zdBC+5JUDrYBIPXwWkPrqNPYCRo5PxS1w+bhFtp9ypsTVG2TDqODLa/erV2F6vgxL+SCZoIZoivxJ+Q56/L2iH82g14dfa2n3ZsNb3C4G+xrLF+YYHrvg9oMHnsGsxEmTOzxlV2OSyBcaGuvX64k/DE0FJqmDZvfRoCqmLGOwCC7HoRPam9aDlCMDGznep6fW/YMbSKSOtVuniYFVbinUY8h1AuhuBX0y7p9faLo/XhSvpX6kdNx+uf7lBco9DUyAd7XmzWGSHgxlWcVTRc32rp+qApz0AHQ/7J/hqkSNsFW7ukNGi4hNZ/Hz6YyX9ngWVydJv+RU0vgT9m7V2JiBuktysMDNh4uU+6piQrOinLzUu0l0oeTDZlxyZrymn34JsJz0XHDhfs5lERgT8dSZzT/2vxPsjPLDouMqH230r6wfPVOxDXQsmqP0DjW5RwKYEtLSazAGEsnSA7WoND+uhyQaZaLUO5iGC0RjMmIJ+1Nd8HjikhASLH7ItPCbmmtmmC2QxGV2reLa4mscGIYjnzQ
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

Archive powered by MHonArc 2.6.19+.

Top of Page