coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason Gross <jasongross9 AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] proof uninformativeness vs. proof irrelevance
- Date: Sun, 24 Apr 2016 13:14:11 -0400
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-ob0-f176.google.com
- Ironport-phdr: 9a23:TSC+mROoOjzRCfo80xwl6mtUPXoX/o7sNwtQ0KIMzox0KPj8rarrMEGX3/hxlliBBdydsKIUzbWK+Py7EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ35TxiLz5p8abSj4LrQT+SIs6FA+xowTVu5teqqpZAYF19CH0pGBVcf9d32JiKAHbtR/94sCt4MwrqHwI6Lpyv/JHBK79ZuEzSaFSRGAtNHlw78n2vzHCSxGO7z0SSDNFvABPBl3n5Qr9WN/eqCzhraIp2iCBOsv5V7cvQmWK4KJiSRuugyACYW1quFrLg9B92foI6CmqoAZyltbZ
> Axiom OrTrueTrueRelevant : (or_introl I <> or_intror I).
> Axiom UIPNatNat : forall (f:nat ->nat) (p1 p2 : f=f), p1=p2.
Yes, that's safe (or, at least, if it's unsafe, the proof of contradiction would need impredicativity, and it seems unlikely that this would interact with impredicativity in such a way); it's validated by considering the predicative subset of Coq, replacing [Prop] with [Set] (and bumping the other universe levels appropriately), and considering the model in sets.The claim I'm making is that if there are two elements of a Prop that can be distinguished in a Prop context (i.e., if you could find distinct elements were you to put the inductive in [Type] rather than [Prop]), then having distinguishable elements of [or] gives you distinguishable elements of that type. The fully general statement would probably say something about W-types in Type and W-types in Prop, and say that if you have a W-type in Type with two provably distinct elements, and you have [or_introl I <> or_intror I], then you can find two elements of the same W-type in Prop that are provably distinct.
On Sun, Apr 24, 2016 at 12:21 PM, Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:
Thanks, Jason. I understand your proof for the True \/ True case.However, I don't see a proof of the full generality of your claim.For example, for any f:nat->nat, I think proof irrelevance of f=f is not provable. However, unlike for True \/ True, I do not have any 2 elements in f=f that match can distinguish between.More formally, is it safe to simultaneously assume the following?Axiom OrTrueTrueRelevant : (or_introl I <> or_intror I).Axiom UIPNatNat : forall (f:nat ->nat) (p1 p2 : f=f), p1=p2.-- AbhishekOn Sun, Apr 24, 2016 at 10:25 AM, Jason Gross <jasongross9 AT gmail.com> wrote:Note that having *any* prop with two distinguishable elements is inconsistent with proof irrelevance for any props for which it is not already provable: when you're in a prop context, you can distinguish elements of, e.g., [or]. Since you can map two elements of, e.g., [True \/ True] to non equal things, you can't have proof irrelevance for [or].
On Sun, Apr 24, 2016, 10:13 AM Jonathan Leivent <jonikelee AT gmail.com> wrote:
On 04/24/2016 12:22 AM, Abhishek Anand wrote:
> Your proof essentially shows that Erasable_inj implies proof relevance of
> Foo, and is thus inconsistent with assuming proof irrelevance of Foo :
> (No was a Yes? Sorry if I am misunderstanding something.)
I believe that is correct.
>
> Inductive Erasable(A : Set) : Prop :=
> erasable: A -> Erasable A.
>
> Arguments erasable [A] _.
>
> Axiom Erasable_inj : forall {A : Set}{a b : A}, erasable a=erasable b ->
> a=b.
>
> Inductive Foo : Prop :=
> foo: nat -> Foo.
>
> Definition foo2erasable(f : Foo) : Erasable nat :=
> match f with
> | foo x => erasable x
> end.
>
> Lemma FooRelevant : foo 1 <> foo 2.
> Proof.
> intros H. apply f_equal with (f := foo2erasable) in H.
> simpl in H.
> apply Erasable_inj in H.
> discriminate H.
> Qed.
>
>
> Do you need to assume Erasable_inj in its full generality? or just some
> specific instances for some sets?
> If only certain instances suffice, and if there was a way to easily
> understand the implications of such instances, it may still be possible to
> safely have some instances of proof irrelevance.
> More formally, if we assume @Erasable_inj A for some set A, is there are a
> simple characterization of the Props (members of sort Prop) whose proof
> relevance become implied?
>
Unfortunately, one of the more important cases of Erasable_inj I use is
when the Set is list A for arbitrary A. That arbitrary A would seem to
imply that there is no way to restrict this proof-relevance domino effect.
Thanks for the help.
-- Jonathan
- Re: [Coq-Club] proof uninformativeness vs. proof irrelevance, (continued)
- Re: [Coq-Club] proof uninformativeness vs. proof irrelevance, Jonathan Leivent, 04/24/2016
- 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
- Re: [Coq-Club] proof uninformativeness vs. proof irrelevance, Jonathan Leivent, 04/24/2016
Archive powered by MHonArc 2.6.18.