coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
-- Abhishek
http://www.cs.cornell.edu/~aa755/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
- [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, Arnaud Spiwack, 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, 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.