The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

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?

It may be possible using clever use of applications as well, as we're equating all terms of forall X, P X as well. We might try to be clever, with some impredicative encoding maybe. But I doubt I can make that work, maybe someone smarter than me (though I must confess I'd be really surprised if it was the case).

 

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.

Well, you seem to be missing Hugo's point here. By the lemma above, f1 (Acc R x) p1 p2 and f2 (Acc R x) p1 p2 are convertible. Hence any two proofs of Acc R x are convertible, hence full proof-irrelevance.



Back to the main discussion, I personally dislike singleton elimination for eq and acc. They allow opaque term to sneak in my computations without the typechecker detecting it. It's very painful when this sort of things happen, in my experience. That said, there is an alternative solution to proof irrelevance it's Bruno Barras & Bruno Bernardo's CIC* kind of ideas: instead of using the type Prop to mean "I'm irrelevant to all computation" (we could call it server-side irrelevance), specifying in a term's type what it will consider as computationally relevant or irrelevant (client-side irrelevance).

I'm kind of keen for the client-side version of things. But truth be told, usually both are needed/useful. I'm still unclear on what it would cost to go that way though.