coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Hugo Herbelin <Hugo.Herbelin AT inria.fr>
- To: Guillaume Melquiond <guillaume.melquiond AT inria.fr>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Proof irrelevance
- Date: Mon, 26 Nov 2012 07:35:47 +0100
If we accept proof-irrelevance on propositional variables, then
f1 := fun (X:Prop) (x1 x2:X) => x1
and
f2 := fun (X:Prop) (x1 x2:X) => x2
are (definitionally) equal. Hence, f1 (Acc R x) p1 p2 and
f2 (Acc R x) p1 p2 are equal, whatever p1 and p2 proofs of Acc R x are.
But this would break being relevant on expressions of type Acc R x.
Or maybe I misunderstood the proposal?
Hugo
On Mon, Nov 26, 2012 at 06:52:41AM +0100, Guillaume Melquiond wrote:
> Le lundi 26 novembre 2012 à 06:10 +0100, Hugo Herbelin a écrit :
>
> > If we restrict proof-irrelevance to non-recursive-singleton (Acc) and
> > no-with-indices-singleton (eq) propositions (*), then we have to
> > forbid also propositional variables, since they may get eventually
> > substituted by one of these propositions we want to exclude.
>
> I thought I was starting to grasp what the situation is about, but
> looking at your last comment, I am not so sure anymore. It seemed to me
> that the only case that mattered when checking convertibility was
> whether surjective pairing could be applied to the argument of a
> match/fix. Thus propositional variables should have been fine, since
> their values are never matched upon. What are the other cases that could
> happen?
>
> Best regards,
>
> Guillaume
>
- [Coq-Club] Proof irrelevance, AUGER Cédric, 11/21/2012
- Re: [Coq-Club] Proof irrelevance, Andreas Abel, 11/22/2012
- Re: [Coq-Club] Proof irrelevance, AUGER Cédric, 11/22/2012
- Re: [Coq-Club] Proof irrelevance, Matthieu Sozeau, 11/23/2012
- Re: [Coq-Club] Proof irrelevance, Hugo Herbelin, 11/23/2012
- Re: [Coq-Club] Proof irrelevance, Matthieu Sozeau, 11/24/2012
- Re: [Coq-Club] Proof irrelevance, Hugo Herbelin, 11/24/2012
- Re: [Coq-Club] Proof irrelevance, Andreas Abel, 11/25/2012
- Re: [Coq-Club] Proof irrelevance, Hugo Herbelin, 11/26/2012
- Re: [Coq-Club] Proof irrelevance, Guillaume Melquiond, 11/26/2012
- Re: [Coq-Club] Proof irrelevance, Hugo Herbelin, 11/26/2012
- Re: [Coq-Club] Proof irrelevance, Guillaume Melquiond, 11/26/2012
- Re: [Coq-Club] Proof irrelevance, Arnaud Spiwack, 11/26/2012
- Re: [Coq-Club] Proof irrelevance, Guillaume Melquiond, 11/26/2012
- Re: [Coq-Club] Proof irrelevance, Arnaud Spiwack, 11/26/2012
- Re: [Coq-Club] Proof irrelevance, Hugo Herbelin, 11/24/2012
- Re: [Coq-Club] Proof irrelevance, Matthieu Sozeau, 11/24/2012
- Re: [Coq-Club] Proof irrelevance, Hugo Herbelin, 11/23/2012
- Re: [Coq-Club] Proof irrelevance, Matthieu Sozeau, 11/23/2012
- Re: [Coq-Club] Proof irrelevance, Andreas Abel, 11/26/2012
- Re: [Coq-Club] Proof irrelevance, Frederic Blanqui, 11/27/2012
- Re: [Coq-Club] Proof irrelevance, Andreas Abel, 11/27/2012
- Re: [Coq-Club] Proof irrelevance, Frédéric Blanqui, 11/27/2012
- Re: [Coq-Club] Proof irrelevance, AUGER Cédric, 11/22/2012
- Re: [Coq-Club] Proof irrelevance, Andreas Abel, 11/22/2012
Archive powered by MHonArc 2.6.18.