coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Gabriel Scherer <gabriel.scherer AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] proof uninformativeness vs. proof irrelevance
- Date: Sat, 23 Apr 2016 22:39:23 -0400
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gabriel.scherer AT gmail.com; spf=Pass smtp.mailfrom=gabriel.scherer AT gmail.com; spf=None smtp.helo=postmaster AT mail-ig0-f180.google.com
- Ironport-phdr: 9a23:jLjdKRKBcg/qIHB799mcpTZWNBhigK39O0sv0rFitYgULfXxwZ3uMQTl6Ol3ixeRBMOAu6IC1LCd6fmwEUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ35TxiLr5ocSDKyxzxxODIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46Fp34d6XK77Z6U1S6BDRHRjajhtpZ6jiR6WZgyWrlAYT29exhFPGk3O6Azwdpb3qCrz8ORnjnq0J8rzGJ89Uy6j4qMjcxTohT0KLXZt/2jdkM19iORAqxKsvRFl64HRaYCRcvF5e/WOLpshWWNdU5MJBGR6CYSmYt5KVrJZMA==
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.
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
On 04/23/2016 09:55 PM, Abhishek Anand wrote:
It implies proof irrelevance, as shown below.
Definition distinguished(T : Type) := exists (a b : T), a <> b.
Definition proof_uninformativeness : Prop :=
forall (P : Prop)(T : Type)(f : P -> T)(p1 p2 : P), distinguished T -> f
p1 = f p2.
Inductive InjectPT (P:Prop) : Type :=
| injectpt : P -> InjectPT P
| dummy1 : InjectPT P
| dummy2 : InjectPT P.
Lemma distinguishedInjectPT : forall P, distinguished (InjectPT P).
Proof using.
intros ?. unfold distinguished. exists (dummy1 P), (dummy2 P).
discriminate.
Qed.
Definition uninject (P:Prop) (ip: InjectPT P) : option P :=
match ip with
| injectpt _ p => Some p
| _ => None
end.
Lemma invertSome (A:Type) (a b: A) :
Some a = Some b -> a= b.
Proof using.
intros H.
inversion H.
reflexivity.
Qed.
Lemma proof_uninformativeness_implies_proof_irrelevance:
proof_uninformativeness
-> forall (P : Prop) (p q : P), p = q.
Proof using.
intros H ? ? ?.
specialize (H P (InjectPT P) (injectpt P) p q (distinguishedInjectPT P)).
apply (f_equal (uninject P)) in H.
simpl in H.
apply invertSome in H.
assumption.
Qed.
-- Abhishek
http://www.cs.cornell.edu/~aa755/
On Sat, Apr 23, 2016 at 9:00 PM, Jonathan Leivent <jonikelee AT gmail.com>
wrote:
On 04/23/2016 08:41 PM, darktenaibre wrote:
Ah, that notprop predicate prevents this stupid observation though. YouOops - my (embarrassing) mistake having Prop not be a subtype of Set. :-[
can certainly write something like (fun T => forall P : Prop, ~ (@eq Type P
T)) which will easily block the previous proof, but it's probably unusable
this way. I do not have any idea for a clever solution to this problem
though.
On 04/24/2016 02:32 AM, darktenaibre wrote:
On 04/24/2016 02:21 AM, Jonathan Leivent wrote:
Definition proof_uninformativeness := forall (P : Prop)(S : Set)(f : PHi,
-> S)(p1 p2 : P), f p1 = f p2.
If you take f:=id, isn't it just proof irrelevance ?
Lemma proof_uninformativeness_irrelevance : proof_uninformativeness ->
forall (P : Prop) (p q : P), p = q.
intros pu P; apply pu.
Qed.
So, there would need to be some usable notprop predicate.
Hmm... maybe types having at least 2 distinguished instances are
sufficient? :
Definition distinguished(T : Type) := exists (a b : T), a <> b.
Definition proof_uninformativeness := forall (P : Prop)(T : Type)(f : P ->
T)(p1 p2 : P), distinguished T -> f p1 = f p2.
Is this a suitable replacement for all interesting use cases of proof
irrelevance?
-- Jonathan
- Re: [Coq-Club] proof uninformativeness vs. proof irrelevance, (continued)
- Re: [Coq-Club] proof uninformativeness vs. proof irrelevance, darktenaibre, 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, 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, Jonathan Leivent, 04/24/2016
Archive powered by MHonArc 2.6.18.