Backport from stablesort #1097
Backport from stablesort #1097
Conversation
ef41c7a to
6061c29
Compare
mathcomp/ssreflect/seq.v
Outdated
| Lemma eq_allrel_l {T : eqType} {S} (r : T -> S -> bool) (s1 s1' : seq T) s2 : | ||
| s1 =i s1' -> allrel r s1 s2 = allrel r s1' s2. | ||
| Proof. by move=> eqs1; apply: eq_all_r. Qed. | ||
|
|
||
| Lemma eq_allrel_r {T} {S : eqType} (r : T -> S -> bool) s1 (s2 s2' : seq S) : | ||
| s2 =i s2' -> allrel r s1 s2 = allrel r s1 s2'. | ||
| Proof. by rewrite ![allrel _ s1 _]allrelC; apply: eq_allrel_l. Qed. | ||
|
|
||
| Lemma eq_allrel2 {T S : eqType} (r : T -> S -> bool) | ||
| (s1 s1' : seq T) (s2 s2' : seq S) : | ||
| s1 =i s1' -> s2 =i s2' -> allrel r s1 s2 = allrel r s1' s2'. | ||
| Proof. by move=> /eq_allrel_l -> /eq_allrel_r ->. Qed. |
There was a problem hiding this comment.
I'm not so sure if these names are coherent with the following lemma:
Lemma eq_allrel {T S : Type} (r r' : T -> S -> bool) :
r =2 r' -> allrel r =2 allrel r'.There was a problem hiding this comment.
We have been using the suffix 2 for operations that apply to the both sides of a relation, like:
Lemma lteN2 x y : (- x < - y) = (y < x).I am wondering whether eq_allrel should be eq2_allrel and
eq_allrel2 be eq_allrel because in that case eq_allrel_r/l
would seem more natural to me.
allrel_rev2 seems ok to me (somehow, a shortcut for allrel_revrev).
I would have found allrelrev2 ok but one may find it a bit disgracious.
I also have the following proposal:
allrel_revr could be allrelsrev
and allrel_revl could be allrelrevs (positional notations with "s" to mark the position of a string, I have a tendency to prefer that over l/r suffixes but like the above I wouldn't argue too long with somebody thinking it is ugly).
There was a problem hiding this comment.
Names like allrelsrev and allrelrevs work only when rev is replaced with one capital character IMO.
There was a problem hiding this comment.
I am wondering whether eq_allrel should be eq2_allrel
A grep on "eq2_" returns nothing but an old thing that was renamed in the changelog, so likely not a consensual choice.
There was a problem hiding this comment.
We could have a suffix _mem (because the hypothesis is using =i) but I think it's good enough as it is.
We'd like to release a 2.1 tomorrow and it would be nice that this lands in it, so I'm ratherfor merging as it is.
There was a problem hiding this comment.
I am wondering whether eq_allrel should be eq2_allrel and
eq_allrel2 be eq_allrel because in that case eq_allrel_r/l
would seem more natural to me.
By the way, it looks like _r and _l are often used in the Coq standard library
but much less in MathComp. Don't you want to remove the _?
There was a problem hiding this comment.
(We are planning to release today by the way ^_^.)
There was a problem hiding this comment.
What about eq_allrel2 -> eq_allrel_mem2 (we "apply" mem on the left and on the right of the rel)?
There was a problem hiding this comment.
(which then calls for the renaming eq_allrel_l -> eq_allrel_meml)
6061c29 to
b9430c4
Compare
Motivation for this change
Backport from this file: https://github.com/pi8027/stablesort/blob/565499cbef5884e219e8af6048083651ef0f43cf/theories/mathcomp_ext.v
Things done/to do
CHANGELOG_UNRELEASED.md[ ] added corresponding documentation in the headersCompatibility with MathComp 1.X
TODO: MC-1 portto make sure someone ports this PR tothe
mathcomp-1branch or I already opened an issue or PR (please cross reference).Automatic note to reviewers
Read this Checklist and put a milestone if possible.