Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Proof irrelevance

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Proof irrelevance


Chronological Thread 
  • 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
>



Archive powered by MHonArc 2.6.18.

Top of Page