coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] help with excluded middle at point vs. all
- Date: Sun, 3 Jul 2016 22:16:36 +0200
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=arnaud.spiwack AT gmail.com; spf=Pass smtp.mailfrom=arnaud.spiwack AT gmail.com; spf=None smtp.helo=postmaster AT mail-vk0-f52.google.com
- Ironport-phdr: 9a23:DoJ9XBEf6gShyoyriT+PCZ1GYnF86YWxBRYc798ds5kLTJ75oMqwAkXT6L1XgUPTWs2DsrQf2rKQ6fmrADBeqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ3pzxjbn5osGNKyxzxxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cYk7sb+sVBSaT3ebgjBfwdVWx+cjN92Mq+nh7aBSCL+3FUBm4Ri19DBxXPxBD8RJb49CXg4LlTwi6faOTsS7kpVXyZ96Z0QRTrwHMOLCY472jcieR0jbIduBWltgByyI7SYZiIObxwZPWOLpshWWNdU5MJBGR6CYSmYt5KVrJZMA==
This is emphatically not true of the natural numbers.
It is true of the “one-point compacification” of the natural numbers (sometimes called co-natural numbers):
CoInductive CN : Type :=
| O : CN
| S : CN -> CN
In fact, for this one-point compacification of the natural number we get a slightly stronger (and, frankly, more useful):
forall P, (forall a:CN, P n \/ ~P n) -> (forall a:CN, P a) \/ exists a:CN, ~P a
Martin Escardó & Paulo Oliva have spend quite some energy studying this latter property.
This [ http://www.cs.bham.ac.uk/~mhe/papers/exhaustive.pdf ], I believe, may be a good, rather programming-oriented, starting point.
On 3 July 2016 at 21:56, Jonathan Leivent <jonikelee AT gmail.com> wrote:
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.