Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] help with excluded middle at point vs. all

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] help with excluded middle at point vs. all


Chronological Thread 
  • 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






Archive powered by MHonArc 2.6.18.

Top of Page