Open anton-trunov opened 6 years ago
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'.
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...
@CohenCyril I opened a new issue for your last comment -- math-comp/math-comp#229
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?
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
.
@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...
@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
.
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: https://github.com/math-comp/math-comp/pull/230
Finally, I'm not convinced it's useful to state value irrelevance for
unit
, given thatunitE
already states thatunit
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
.
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.
Does it make sense to move
unit_irrelevance
elsewhere in Coq's part of ssreflect or mathcomp?E.g. to
ssrfun
, nearunitE
lemma, which in turn could be used to prove the fact: