coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Kumar, Ashish" <azk640 AT psu.edu>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: [Coq-Club] Showing proof of type ~(P -> Q)?
- Date: Sat, 19 Sep 2020 01:43:09 +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=GSZPrAAYzevCPjkV8WsQtg0GzG5bkgJNQXmNq5oNVRI=; b=cPiiIR1sNfnvzXiXQdvvx9M8IUP9aRbj6ckAJBkKbJmaY3zucjfKlX8+gN9IeBsv/BtHCksxn/svb6CxCdHPOXKHpcaRIEXxLlBtJvk6nCgbf4MZyg6M1zvaK40GThlOKAcNItD+OKdy2v3UFfVhfPD3B58DGD1btOgxSFtlXriDnI8l0kkjdZ6UHpJ0duZIxAF/8P3rstyI+O4c1bnuwbxl5lyGi28hYyZsw6KmPRw+5MGlcrLAPZz8/gHrzqI6woJwYjES4XB0BRPy+AUy0NHdJPhmDlAswc9u/SOuGVWJfAGiQNu9KShOTUZXGBwsYREjwund82a7wB2ykeZVBw==
- Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=g9IlKzXxOeZ9zYRkwT8V+iIxxX60qbc9+tELdUrjFJFaDN7Rp7QRlUYDPNyHwLUu/cLXEU99sqa9cB7IIjQElKvimZqIsqb/GTAucgkeDNw+5O1XZdpIzx+m9PFSsagiVkdnXiepAtBIkdLAJ7cnTg2T2ijEA1fbfmbrnSv9nY26H+Q0oCdW1M0zv6ebAZ1GtmoqAuiOSA7iLRZ3ZXW0uwvftgWGcqJ9zsn0f3Slf9lvNC9cb33QzjEo0bFDtc8pwz4DIrMPOL4ZwyYFe78L1G2PqAJiOutHQaEyo3ZXcNsHyb4ug9MZsXl0XS89hXxQTtIBX5b9g/wFmR+Hfjn8sw==
- 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 NAM10-DM6-obe.outbound.protection.outlook.com
- Ironport-phdr: 9a23:Ftg2ORXOaSu8m7kQ8aGyN7ZnZ+DV8LGtZVwlr6E/grcLSJyIuqrYbReOt8tkgFKBZ4jH8fUM07OQ7/m/HzRfqsrR+DBaKdoQDkFD0Z1X1yUbQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2agMu4zf299IPOaAtUmjW9falyLBKrpgnNq8Uam4RvJrszxxfTvndFeetayGxrKFmOmxrw+tq88IRs/ihNuv8t7dJMXbn/c68lUbFWETMqPnwv6sb2rxfDVwyP5nUdUmUSjBVFBhXO4Q/5UJnsrCb0r/Jx1yaGM8L4S7A0Qimi4LxwSBD0kicHNiU2/3/Rh8dtka9UuhOhpxh4w47JfIGYMed1c63Bcd8GQ2dKQ8BcXDFDDIyhdYsCF+oPM/hFoYnhqVUArhq+ChWjC+700DBEmmP60Lcm3+g9DA3L2hErEdIUsHTTqdX4LKkeX+WozKnN1zrDdeta0irh5YjTchAhoOqMXbJ+fcHMzkQgDQLEjlaRpIHqIz+YzfwNs3OG7+Z6S+2glnMnphh3rzOyycgilpPHiZgJylDY6yp52oA1KMW4RkN7YdOpFIVcuiCZOodoTc0vQW5mtik1xLAbuJO2eCcHxIo6yhPCavGKfYqF7g7tWuifLzp1h29pdKyhihqv90Wr1+7yVtGs3VtFsiZJiMTAumwP2hDJ7sWKROFx8lq/1TuLzwzf9/1ILE8umafVKJMt2LE9moQJvUnCAyP6gFv6ga6Kekgq/+Wk9vjrba7nq5KZKYN4lgLzP6Eul8G7BOk1NxUCU3Wd9O+hzrPs51f5T69PjvAukqnWrpTaJcMDq6ChHwJb1Zsv5wqmAzmo19oVnGALLFVedx2ZlYTpPEzOIOzjAve4nlSslipky+rePr37BZXNMmbMn6v9fbZ87E5czhA/zddC55JIDrEBJ/XzWkzruNPECR85NhS4w+fhCNpjyoMTQW2CDrODPK/PrVOF5PgjLu2CaYMPpTrxNfwo6+brjXAjmF8deaep3YEQaHC9BvlpOUSYYXntj9oODWsHpRI+TPf3iFGYTzFcemuyU7om5j4nEIKmEZvDRoe1jbOd2ye7B4RaaXxCClCRCnjlbJ6EWvcJaCKKOMBtiD0EVb67S48gzx6irgH6y6A0ZtbTr2cTsoum39xo7cXSkwsz/Hp6FY7Vh2qKViR/mn4Cbz4wxqF250JnnASty6991rZ7CNla/bcBexw6NIXchaQuAsLxBF6ZVs+SVRCrTsjwUmJ5dc4439JbOxU1IN6llB2Wh3P7UY9QrKSCAdkPyoyZ2nHwI8hnzHOXhrE6kh8rTtYdbDT61J46zBDaAsvyq2vcj7yjJPYExzOL+WuenzLX4RNoFTVoWKCAZkgxI0vbqdOluRHkZpr3UfELF1UEzsSPbKxXdtfukFNKAu/5P8jTaH6wnGH2AguUwrSLb8zhfGBPhSg=
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
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
- [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
- Re: [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
Archive powered by MHonArc 2.6.19+.