Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] proof uninformativeness vs. proof irrelevance

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] proof uninformativeness vs. proof irrelevance


Chronological Thread 
  • From: Jason Gross <jasongross9 AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] proof uninformativeness vs. proof irrelevance
  • Date: Sun, 24 Apr 2016 14:25:36 +0000
  • Authentication-results: mail2-smtp-roc.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-oi0-f42.google.com
  • Ironport-phdr: 9a23:9fbe/h9cje//Z/9uRHKM819IXTAuvvDOBiVQ1KB90OwcTK2v8tzYMVDF4r011RmSDdWdtK4P0rCempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXsq3G/pQQfBg/4fVIsYL+lSsiN04/ujaibwN76XUZhvHKFe7R8LRG7/036l/I9ps9cEJs30QbDuXBSeu5blitCLFOXmAvgtI/rpMYwu3cYh/V0/MlZFK7+Yq4QTLpCDT1gPXpmytfssEzhRBCI4DMzSGINiVIcAQHe6xf1RJDqqXrSue902S3cNsrzG+NnEQ++5rtmHUe7wBwMMCQ0pTna

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




Archive powered by MHonArc 2.6.18.

Top of Page