coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jonathan Leivent <jonikelee AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: [Coq-Club] help with excluded middle at point vs. all
- Date: Sun, 3 Jul 2016 15:56:16 -0400
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f178.google.com
- Ironport-phdr: 9a23:FiYUkRAUPBdxX+cf48GPUyQJP3N1i/DPJgcQr6AfoPdwSP79r8bcNUDSrc9gkEXOFd2CrakV06yM6uu5BTRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWM5DIfUi/yKRBybrysXNWD14Ltjqvrp8WbSj4LrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGx48sgs/M9YUKj8Y79wDfkBVGxnYCgJ45jAsgCLZg+S7DNIWWIP1xFMHgLt7RfgX563vDGs5cRn3yzPH8rwRKw0UDLqy6pqVhLulG9TNTk/8WLajsF9pK1eqROl4Rd4xtiHM8muKPNic/aFLpshTm1bU5MUDnQZDw==
I hit another constructive goal that is messing with my classical logic encumbered brain - a form of excluded middle at a point vs. overall:
A : Type
P : A -> Prop
emp : forall a : A, P a \/ ~ P a
============================
(forall a : A, P a) \/ ~ (forall a : A, P a)
I would think this is not provable in Coq in general, but it is certainly true for many A and P. What properties of A and/or P make this true? I would think it is true for example on any type A such that one can enumerate the elements somehow - such as nat, or maybe any inductive type. But, I don't even see how to prove it if A is nat for arbitrary P. It's trivial to prove if A is bool for arbitrary P, and probably so for any other finite type.
How does one go about such proofs when A is not finite - what other hypotheses about A and/or P are needed to make headway?
-- Jonathan
- [Coq-Club] help with excluded middle at point vs. all, Jonathan Leivent, 07/03/2016
- Re: [Coq-Club] help with excluded middle at point vs. all, Vilhelm Sjoberg, 07/03/2016
- Re: [Coq-Club] help with excluded middle at point vs. all, Arnaud Spiwack, 07/03/2016
- Re: [Coq-Club] help with excluded middle at point vs. all, Hugo Carvalho, 07/14/2016
- Re: [Coq-Club] help with excluded middle at point vs. all, Arnaud Spiwack, 07/14/2016
- Re: [Coq-Club] help with excluded middle at point vs. all, Hugo Carvalho, 07/15/2016
- Re: [Coq-Club] help with excluded middle at point vs. all, Arnaud Spiwack, 07/14/2016
- Re: [Coq-Club] help with excluded middle at point vs. all, Hugo Carvalho, 07/14/2016
- Re: [Coq-Club] help with excluded middle at point vs. all, Clément Pit--Claudel, 07/03/2016
- Re: [Coq-Club] help with excluded middle at point vs. all, Clément Pit--Claudel, 07/03/2016
- Re: [Coq-Club] help with excluded middle at point vs. all, Abhishek Anand, 07/03/2016
- Re: [Coq-Club] help with excluded middle at point vs. all, Jonathan Leivent, 07/03/2016
Archive powered by MHonArc 2.6.18.