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: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
  • 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 16:39:41 -0400
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw0-f182.google.com
  • Ironport-phdr: 9a23:NL7aohKMzP5KaCCp7dmcpTZWNBhigK39O0sv0rFitYgUL/jxwZ3uMQTl6Ol3ixeRBMOAuqoC0bOd6vy+EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuS9aU1Z38jrzss7ToICxwzAKnZr1zKBjk5S7wjeIxxbVYF6Aq1xHSqWFJcekFjUlhJFaUggqurpzopM0roGxsvKcq8NcFWqHndexsRrtBST8iLmod5cvxtBCFQxHZtVUGVWBDuxBIAhPF4RKyd5H4tCey4uN32CiBPcD1C7kyUDKuqaZqVBDAhyIONjp/+2bS3J8jxJlHqQ6s8kQsi7XfZ5uYYaJz

I usually turn to the halting problem to convince myself that some classical principle is not constructive.
Here is a counterexample to what you wish to prove:

In a context of an arbitrary turing machine t,
A:=nat
P := \n:nat, t does NOT halt in n or fewer steps.
eps := easily provable

If you manage to prove your lemma, I will be able to apply it to my turing machine, and normalize and visually inspect the result (or_introl vs or_intror), and thus solve the halting problem.





On Sun, Jul 3, 2016 at 3:56 PM, 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