The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le lundi 26 novembre 2012 à 07:35 +0100, Hugo Herbelin a écrit :
> 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?

I agree that "f1 (Acc R x) p1 p2" and "f2 (Acc R x) p1 p2" would be
equal. But as I said, by the time the equality of these two expressions
matters (that is, they are used as arguments of a fixpoint), their types
are no longer propositional variables. Their type is Acc R x, and as
such, they are excluded from reducing the fixpoint.

So, let me try to reformulate my question. Is there a way to break
strong normalization (or any other desirable property) by assuming proof
irrelevance yet without using match or fix? If you always need match or
fix, I am under the impression that propositional variables do not
matter since their values cannot be matched upon.

Best regards,

Guillaume