The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

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
>