coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jonathan Leivent <jonikelee AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] proof uninformativeness vs. proof irrelevance
- Date: Sat, 23 Apr 2016 23:48:56 -0400
- Authentication-results: mail3-smtp-sop.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-qk0-f177.google.com
- Ironport-phdr: 9a23:ketSBhS1DeGEbY6q7E7c821godpsv+yvbD5Q0YIujvd0So/mwa64YBWN2/xhgRfzUJnB7Loc0qyN4/CmBjZLu8ze+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq82VPF8D3mDiKZpJbzyI7izp/vEMhoVjLqtjgjDomVBvP9ps+GVzOFiIlAz97MrjtLRq8iBXpu5zv5UYCfayLOwESulTCy1jOGQo7uXqswPCRE2B/CgySGITxzhPBQHZ7Bj8FrP8szX3sPY1jCudO8z1QLQ5VByt6q5qTFnjjyJRZG1xy33elsEl1PETmxmmvREqm4M=
On 04/23/2016 10:39 PM, Gabriel Scherer wrote:
f is injective iff (f p = f q) implies (p = q). This is compatible with
proof-irrelevance. In particular, all functions whose domain is in a
proof-irrelevant Prop are injective.
But, proof irrelevance is not compatible with injectivity of a Prop-typed function with non-Prop-typed args. Which is why Coq doesn't define Prop constructors to be injective. Unfortunately, I need a single Prop constructor with a single Set-typed arg to be injective (via an axiom), but would otherwise like some aspects of proof irrelevance. But, thanks to this discussion, I'm convinced this attempt isn't going to work.
Thanks,
-- Jonathan.
On Sat, Apr 23, 2016 at 10:10 PM, Jonathan Leivent
<jonikelee AT gmail.com>
wrote:
Sigh... there's got to be a version that "works" - that captures Coq's
uninformative Prop concept, yet is weaker than proof irrelevance. Is it
enough to restrict T to bool? :
Definition proof_uninformativeness := forall (P : Prop)(f : P -> bool)(p1
p2 : P), f p1 = f p2.
What I'm trying to do is to work in a context where proof irrelevance is
inconsistent (because I need injectivity of some props), yet one can still
have its benefits. So, I would like to keep proofs relevant to other
proofs, but not to non-Prop types somehow...
-- Jonathan
- Re: [Coq-Club] proof uninformativeness vs. proof irrelevance, (continued)
- Re: [Coq-Club] proof uninformativeness vs. proof irrelevance, Abhishek Anand, 04/24/2016
- Re: [Coq-Club] proof uninformativeness vs. proof irrelevance, Jonathan Leivent, 04/24/2016
- Re: [Coq-Club] proof uninformativeness vs. proof irrelevance, Abhishek Anand, 04/24/2016
- Re: [Coq-Club] proof uninformativeness vs. proof irrelevance, Jonathan Leivent, 04/24/2016
- Re: [Coq-Club] proof uninformativeness vs. proof irrelevance, Abhishek Anand, 04/24/2016
- Re: [Coq-Club] proof uninformativeness vs. proof irrelevance, Jonathan Leivent, 04/24/2016
- Re: [Coq-Club] proof uninformativeness vs. proof irrelevance, Jason Gross, 04/24/2016
- Re: [Coq-Club] proof uninformativeness vs. proof irrelevance, Abhishek Anand, 04/24/2016
- Re: [Coq-Club] proof uninformativeness vs. proof irrelevance, Jason Gross, 04/24/2016
- Re: [Coq-Club] proof uninformativeness vs. proof irrelevance, Abhishek Anand, 04/24/2016
- Re: [Coq-Club] proof uninformativeness vs. proof irrelevance, Jonathan Leivent, 04/24/2016
- Re: [Coq-Club] proof uninformativeness vs. proof irrelevance, Abhishek Anand, 04/24/2016
- Re: [Coq-Club] proof uninformativeness vs. proof irrelevance, Jonathan Leivent, 04/24/2016
Archive powered by MHonArc 2.6.18.