Should "unit_irrelevance" fact be moved elsewhere?

[anton-trunov]

Does it make sense to move unit_irrelevance elsewhere in Coq's part of ssreflect or mathcomp?

E.g. to ssrfun, near unitE lemma, which in turn could be used to prove the fact:

Fact unit_irrelevance (x y : unit) : x = y.
Proof. by rewrite !unitE. Qed.

[anton-trunov]

I forgot to mention it, but the name unit_irrelevance is a bit confusing, as e.g. eqtype.bool_irrelevance is proof irrelevance for booleans:

Lemma bool_irrelevance (x y : bool) (E E' : x = y) : E = E'.

[CohenCyril]

I agree it is confusing, but the misnaming here would rather be bool_irrelevance since it is proof irrelevance for equalities of booleans... which by the way is subsumed by eq_irrelevance which deserves its name well...

[anton-trunov]

@CohenCyril I opened a new issue for your last comment -- math-comp/math-comp#229

[anton-trunov]

I'm almost sure there is (or at least was) a theorem like unit_irrelevance in our library (FCSL), so I think it would make sense to move it to math-comp.

What do you think?

[ggonthier]

The bool_irrelevance name refers to the well-known "Prop irrelevance" axiom, asserting that types with sort Prop have at most one inhabitant. It contains (and is most often used) the corresponding property for types that are derived from a bool expression via the is_true coercion (which is somewhat an ssreflect signature feature) - in a nutshell, specialising the second bool to true, it states irrelevance for any type of "sort" bool.

[CohenCyril]

@ggonthier I can only find references to "proof irrelevance in Prop", not "Prop-irrelevance". The latter is also confusing to me since it is indeed not Prop that is irrelevant, but only its elements...

[ggonthier]

@CohenCyril : you are correct, however that hardly justifies the proposed renaming, since the "proof" elided in the lemma name refers to inhabitants of the type, not the type itself. If the lemma names were to match the English idiom as closely as possible, they should be proof_irrelevance_for_bool and proof_irrelevance_for_decidable_eq, value_irrelevance_for_unit, and so on.
I feel this is needlessly long; the style most prevalent in MathComp is to elide terms that are not essential to the meaning of the lemma, such as the proof_, value_, and for_ in the above. Also, starting from eqtype.v onwards MathComp uses _eq in lemma names to refer to decidable equality and its boolean reflection, in addition to primitive equality, because usually it is clear from either the context or the meaning of the lemma which is meant. It's the case here, since it's well known that there is no provable proof irrelevance for the Coq primitive equality, and because clearly value irrelevance for bool would be inconsistent.
There is however one way in which bool_irrelevance should be improved: as I've hinted, it's intended as a specialisation of eq_irrelevance to proofs of (the truth of) bool propositions. I generalised the statement to also cover proofs of falsehood (which sometimes are of the form b = false) but in retrospect this was a mistake as it undermines the documentation purpose of the bool specialisation, and I'm not sure it's ever used this way.
Finally, I'm not convinced it's useful to state value irrelevance for unit, given that unitE already states that unit is contractible, which is a stronger property. If we add any thing in this area, I think it should be more generic - like contractible implies hProp, or perhaps twisted transitivity for equality x = z -> y = z -> x = y.

[CohenCyril]

I feel this is needlessly long;

I agree.

in retrospect this was a mistake as it undermines the documentation purpose of the bool specialisation, and I'm not sure it's ever used this way.

I also agree, cf: math-comp/math-comp#230

Finally, I'm not convinced it's useful to state value irrelevance for unit, given that unitE already states that unit is contractible, which is a stronger property.

I agree with you, I just stated it in order as a factory artifact, since I wanted to do a key change (in keyed display). I am quite convinced there is no other use and I planned to make it local to finmap. I am curious though about the use it may have in FCSL and whether it could be replaced by unitE.

[anton-trunov]

I am curious though about the use it may have in FCSL and whether it could be replaced by unitE.

I tried to find it but could not, it appears we removed it at some point or my memory has played a trick on me. Feel free to close the issue and sorry about the noise.