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: Sun, 24 Apr 2016 10:12:39 -0400
- Authentication-results: mail2-smtp-roc.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-qg0-f42.google.com
- Ironport-phdr: 9a23:1K8NJR8IJH9NWv9uRHKM819IXTAuvvDOBiVQ1KB90OMcTK2v8tzYMVDF4r011RmSDdWdtK4P07SempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXsq3G/pQQfBg/4fVIsYL+lSsiN04/viaibwN76XUZhvHKFe7R8LRG7/036l/I9ps9cEJs30QbDuXBSeu5blitCLFOXmAvgtI/rpMYwu3cYh/V0/MlZFK7+Yq4QTLpCDT1gPXpmytfssEzhSg2G+nsVVC0ynxtWDg7ZpEX4WZHwsSb+u+dV1yyTPMmwRrcxD2fxp5x3QQPl3X9UfwUy93va35R9
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
- [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, darktenaibre, 04/24/2016
- 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, darktenaibre, 04/24/2016
- Re: [Coq-Club] proof uninformativeness vs. proof irrelevance, Gabriel Scherer, 04/24/2016
- 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
Archive powered by MHonArc 2.6.18.