Merge pull request #646 from pi8027/rename-eq_sorted

Rename `eq_sorted` lemmas to `sorted_eq` and generalize `sort_le_id`

5 files changed, 38 insertions, 24 deletions

diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v
index e8293ae..0ece733 100644
--- a/mathcomp/ssreflect/bigop.v
+++ b/mathcomp/ssreflect/bigop.v
@@ -990,7 +990,7 @@ Lemma big_nat_widen m n1 n2 (P : pred nat) F :
       = \big[op/idx]_(m <= i < n2 | P i && (i < n1)) F i.
 Proof.
 move=> len12; symmetry; rewrite -big_filter filter_predI big_filter.
-have [ltn_trans eq_by_mem] := (ltn_trans, eq_sorted_irr ltn_trans ltnn).
+have [ltn_trans eq_by_mem] := (ltn_trans, irr_sorted_eq ltn_trans ltnn).
 congr bigop; apply: eq_by_mem; rewrite ?sorted_filter ?iota_ltn_sorted // => i.
 rewrite mem_filter !mem_index_iota andbCA andbA andb_idr => // /andP[_].
 by move/leq_trans->.
diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v
index 836c323..cd3ec87 100644
--- a/mathcomp/ssreflect/binomial.v
+++ b/mathcomp/ssreflect/binomial.v
@@ -468,7 +468,7 @@ have ft_m: #|f_t t| = m.
   rewrite cardsE (card_uniqP _) ?size_tuple // -(map_inj_uniq val_inj).
   exact: (sorted_uniq ltn_trans ltnn).
 rewrite ft_m eqxx -val_eqE val_fA // -(inj_eq (inj_map val_inj)) /=.
-apply/eqP/(eq_sorted_irr ltn_trans ltnn) => // y.
+apply/eqP/(irr_sorted_eq ltn_trans ltnn) => // y.
 by apply/mapP/mapP=> [] [x t_x ->]; exists x; rewrite // mem_enum inE in t_x *.
 Qed.
 
diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v
index da4d59d..1546a55 100644
--- a/mathcomp/ssreflect/order.v
+++ b/mathcomp/ssreflect/order.v
@@ -2741,7 +2741,7 @@ Proof. by rewrite andbC lt_le_asym. Qed.
 
 Definition lte_anti := (=^~ eq_le, lt_asym, lt_le_asym, le_lt_asym).
 
-Lemma lt_sorted_uniq_le s : sorted lt s = uniq s && sorted le s.
+Lemma lt_sorted_uniq_le s : sorted <%O s = uniq s && sorted <=%O s.
 Proof.
 case: s => //= n s; elim: s n => //= m s IHs n.
 rewrite inE lt_neqAle negb_or IHs -!andbA.
@@ -2750,12 +2750,15 @@ rewrite andbF; apply/and5P=> [[ne_nm lenm _ _ le_ms]]; case/negP: ne_nm.
 by rewrite eq_le lenm /=; apply: (allP (order_path_min le_trans le_ms)).
 Qed.
 
-Lemma eq_sorted_lt s1 s2 : sorted lt s1 -> sorted lt s2 -> s1 =i s2 -> s1 = s2.
-Proof. by apply: eq_sorted_irr => //; apply: lt_trans. Qed.
+Lemma lt_sorted_eq s1 s2 : sorted <%O s1 -> sorted <%O s2 -> s1 =i s2 -> s1 = s2.
+Proof. by apply: irr_sorted_eq => //; apply: lt_trans. Qed.
 
-Lemma eq_sorted_le s1 s2 : sorted le s1 -> sorted le s2 ->
-  perm_eq s1 s2 -> s1 = s2.
-Proof. by apply: eq_sorted; [apply: le_trans|apply: le_anti]. Qed.
+Lemma le_sorted_eq s1 s2 :
+  sorted <=%O s1 -> sorted <=%O s2 -> perm_eq s1 s2 -> s1 = s2.
+Proof. exact/sorted_eq/le_anti/le_trans. Qed.
+
+Lemma sort_le_id s : sorted <=%O s -> sort <=%O s = s.
+Proof. exact/sorted_sort/le_trans. Qed.
 
 Lemma comparable_leNgt x y : x >=< y -> (x <= y) = ~~ (y < x).
 Proof.
@@ -3419,6 +3422,13 @@ Proof. exact: anti_mono_in. Qed.
 
 End POrderMonotonyTheory.
 
+Notation "@ 'eq_sorted_lt'" := (deprecate eq_sorted_lt lt_sorted_eq)
+  (at level 10, only parsing) : fun_scope.
+Notation "@ 'eq_sorted_le'" := (deprecate eq_sorted_le le_sorted_eq)
+  (at level 10, only parsing) : fun_scope.
+Notation eq_sorted_lt := (@eq_sorted_lt _ _ _ _) (only parsing).
+Notation eq_sorted_le := (@eq_sorted_le _ _ _ _) (only parsing).
+
 End POrderTheory.
 
 Hint Resolve lexx le_refl ltxx lt_irreflexive ltW lt_eqF : core.
@@ -3728,14 +3738,9 @@ Lemma sort_le_sorted s : sorted <=%O (sort <=%O s).
 Proof. exact: sort_sorted. Qed.
 Hint Resolve sort_le_sorted : core.
 
-Lemma sort_lt_sorted s : sorted lt (sort le s) = uniq s.
+Lemma sort_lt_sorted s : sorted <%O (sort <=%O s) = uniq s.
 Proof. by rewrite lt_sorted_uniq_le sort_uniq sort_le_sorted andbT. Qed.
 
-Lemma sort_le_id s : sorted le s -> sort le s = s.
-Proof.
-by move=> ss; apply: eq_sorted_le; rewrite ?sort_le_sorted // perm_sort.
-Qed.
-
 Lemma leNgt x y : (x <= y) = ~~ (y < x). Proof. exact: comparable_leNgt. Qed.
 
 Lemma ltNge x y : (x < y) = ~~ (y <= x). Proof. exact: comparable_ltNge. Qed.
diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v
index 1f675a6..93521d7 100644
--- a/mathcomp/ssreflect/path.v
+++ b/mathcomp/ssreflect/path.v
@@ -804,7 +804,7 @@ rewrite (IHs (path_sorted s_ord)) andbT; apply/negP=> s_x.
 by case/allPn: (order_path_min leT_tr s_ord); exists x; rewrite // leT_irr.
 Qed.
 
-Lemma eq_sorted : antisymmetric leT ->
+Lemma sorted_eq : antisymmetric leT ->
   forall s1 s2, sorted s1 -> sorted s2 -> perm_eq s1 s2 -> s1 = s2.
 Proof.
 move=> leT_asym; elim=> [|x1 s1 IHs1] s2 //= ord_s1 ord_s2 eq_s12.
@@ -819,13 +819,13 @@ case/predU1P=> [eq_x12 | s1_x2]; first by case ne_x12.
 by rewrite (allP (order_path_min _ ord_s1)).
 Qed.
 
-Lemma eq_sorted_irr : irreflexive leT ->
+Lemma irr_sorted_eq : irreflexive leT ->
   forall s1 s2, sorted s1 -> sorted s2 -> s1 =i s2 -> s1 = s2.
 Proof.
 move=> leT_irr s1 s2 s1_sort s2_sort eq_s12.
 have: antisymmetric leT.
   by move=> m n /andP[? ltnm]; case/idP: (leT_irr m); apply: leT_tr ltnm.
-by move/eq_sorted; apply=> //; apply: uniq_perm => //; apply: sorted_uniq.
+by move/sorted_eq; apply=> //; apply: uniq_perm => //; apply: sorted_uniq.
 Qed.
 
 End Transitive.
@@ -867,7 +867,7 @@ Lemma perm_sortP :
 Proof.
 move=> leT_total leT_tr leT_asym s1 s2.
 apply: (iffP idP) => eq12; last by rewrite -perm_sort eq12 perm_sort.
-apply: eq_sorted; rewrite ?sort_sorted //.
+apply: sorted_eq; rewrite ?sort_sorted //.
 by rewrite perm_sort (permPl eq12) -perm_sort.
 Qed.
 
@@ -1038,7 +1038,7 @@ Lemma filter_sort p s : filter p (sort leT s) = sort leT (filter p s).
 Proof.
 case Ds: s => // [x s1]; rewrite -{s1}Ds.
 rewrite -(mkseq_nth x s) !(filter_map, sort_map).
-congr map; apply/(@eq_sorted_irr _ (le_lex x s)) => //.
+congr map; apply/(@irr_sorted_eq _ (le_lex x s)) => //.
 - by move=> ?; rewrite /= ltnn implybF andbN.
 - exact/sorted_filter/sort_stable/iota_ltn_sorted/ltn_trans.
 - exact/sort_stable/sorted_filter/iota_ltn_sorted/ltn_trans/ltn_trans.
@@ -1461,3 +1461,12 @@ by rewrite ?nth_index ?[_ \in gtn _]index_mem //; apply.
 Qed.
 
 End Monotonicity.
+
+Notation "@ 'eq_sorted'" :=
+  (deprecate eq_sorted sorted_eq) (at level 10, only parsing) : fun_scope.
+Notation "@ 'eq_sorted_irr'" := (deprecate eq_sorted_irr irr_sorted_eq)
+  (at level 10, only parsing) : fun_scope.
+Notation eq_sorted :=
+  (fun le_tr le_asym => @eq_sorted _ _ le_tr le_asym _ _) (only parsing).
+Notation eq_sorted_irr :=
+  (fun le_tr le_irr => @eq_sorted_irr _ _ le_tr le_irr _ _) (only parsing).
diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v
index 8e94ef6..389b1c2 100644
--- a/mathcomp/ssreflect/prime.v
+++ b/mathcomp/ssreflect/prime.v
@@ -454,7 +454,7 @@ Qed.
 Lemma eq_primes m n : (primes m =i primes n) <-> (primes m = primes n).
 Proof.
 split=> [eqpr| -> //].
-by apply: (eq_sorted_irr ltn_trans ltnn); rewrite ?sorted_primes.
+by apply: (irr_sorted_eq ltn_trans ltnn); rewrite ?sorted_primes.
 Qed.
 
 Lemma primes_uniq n : uniq (primes n).
@@ -565,7 +565,7 @@ Qed.
 
 Lemma primes_prime p : prime p -> primes p = [::p].
 Proof.
-move=> pr_p; apply: (eq_sorted_irr ltn_trans ltnn) => // [|q].
+move=> pr_p; apply: (irr_sorted_eq ltn_trans ltnn) => // [|q].
   exact: sorted_primes.
 rewrite mem_seq1 mem_primes prime_gt0 //=.
 by apply/andP/idP=> [[pr_q q_p] | /eqP-> //]; rewrite -dvdn_prime2.
@@ -862,7 +862,7 @@ Proof. by move=> eq_pi n; rewrite 3!inE /= eq_pi. Qed.
 
 Lemma eq_piP m n : \pi(m) =i \pi(n) <-> \pi(m) = \pi(n).
 Proof.
-rewrite /pi_of; have eqs := eq_sorted_irr ltn_trans ltnn.
+rewrite /pi_of; have eqs := irr_sorted_eq ltn_trans ltnn.
 by split=> [|-> //] /(eqs _ _ (sorted_primes m) (sorted_primes n)) ->.
 Qed.
 
@@ -954,7 +954,7 @@ Proof. by rewrite ltn_neqAle part_gt0 andbT eq_sym p_part_eq1 negbK. Qed.
 Lemma primes_part pi n : primes n`_pi = filter (mem pi) (primes n).
 Proof.
 have ltnT := ltn_trans; have [->|n_gt0] := posnP n; first by rewrite partn0.
-apply: (eq_sorted_irr ltnT ltnn); rewrite ?(sorted_primes, sorted_filter) //.
+apply: (irr_sorted_eq ltnT ltnn); rewrite ?(sorted_primes, sorted_filter) //.
 move=> p; rewrite mem_filter /= !mem_primes n_gt0 part_gt0 /=.
 apply/andP/and3P=> [[p_pr] | [pi_p p_pr dv_p_n]].
   rewrite /partn; apply big_ind => [|n1 n2 IHn1 IHn2|q pi_q].
@@ -970,7 +970,7 @@ Qed.
 
 Lemma filter_pi_of n m : n < m -> filter \pi(n) (index_iota 0 m) = primes n.
 Proof.
-move=> lt_n_m; have ltnT := ltn_trans; apply: (eq_sorted_irr ltnT ltnn).
+move=> lt_n_m; have ltnT := ltn_trans; apply: (irr_sorted_eq ltnT ltnn).
 - by rewrite sorted_filter // iota_ltn_sorted.
 - exact: sorted_primes.
 move=> p; rewrite mem_filter mem_index_iota /= mem_primes; case: and3P => //.