switching long suffixes to short suffixes

.gitlab-ci.yml

@@ -174,7 +174,6 @@ ci-fourcolor-dev:
   variables:
     COQ_VERSION: "dev"
 
-
 # The Odd Order Theorem
 .ci-odd-order:
   extends: .ci

CHANGELOG_UNRELEASED.md

@@ -164,6 +164,12 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 - The following naming inconsistencies have been fixed in `ssrnat.v`:
   + `homo_inj_lt(_in)` -> `inj_homo_ltn(in)`
   + `(inc|dec)r(_in)` -> `(inc|dev)n(_in)`
+- switching long suffixes to short suffixes
+  + `odd_add` -> `oddD`
+  + `odd_sub` -> `oddB`
+  + `take_addn` -> `takeD`
+  + `rot_addn` -> `rotD`
+  + `nseq_addn` -> `nseqD`
 
 ### Removed
 

mathcomp/algebra/matrix.v

@@ -2395,7 +2395,7 @@ rewrite (reindex (lift_perm i0 j0)); last first.
   by rewrite lift_perm_lift -si0 permE ulsfK.
 rewrite /cofactor big_distrr /=.
 apply: eq_big => [s | s _]; first by rewrite lift_perm_id eqxx.
-rewrite -signr_odd mulrA -signr_addb odd_add -odd_lift_perm; congr (_ * _).
+rewrite -signr_odd mulrA -signr_addb oddD -odd_lift_perm; congr (_ * _).
 case: (pickP 'I_n) => [k0 _ | n0]; last first.
   by rewrite !big1 // => [j /unlift_some[i] | i _]; have:= n0 i.
 rewrite (reindex (lift i0)).

mathcomp/algebra/mxpoly.v

@@ -469,7 +469,7 @@ rewrite big_ord_recr big_ord_recl/= big1 ?add0r //=; last first.
 rewrite !mxE ?subnn -horner_coef0 /= hornerMXaddC.
 rewrite !(eqxx, mulr0, add0r, addr0, subr0, rmorphN, opprK)/=.
 rewrite mulrC /cofactor; congr (_ * 'X + _).
-  rewrite /cofactor -signr_odd odd_add addbb mul1r; congr (\det _).
+  rewrite /cofactor -signr_odd oddD addbb mul1r; congr (\det _).
   apply/matrixP => i j; rewrite !mxE -val_eqE coefD coefMX coefC.
   by rewrite /= /bump /= !add1n !eqSS addr0.
 rewrite /cofactor [X in \det X](_ : _ = D _).

mathcomp/fingroup/perm.v

@@ -452,8 +452,8 @@ Qed.
 
 Lemma odd_mul_tperm x y s : odd_perm (tperm x y * s) = (x != y) (+) odd_perm s.
 Proof.
-rewrite addbC -addbA -[~~ _]oddb -odd_add -ncycles_mul_tperm.
-by rewrite odd_add odd_double addbF.
+rewrite addbC -addbA -[~~ _]oddb -oddD -ncycles_mul_tperm.
+by rewrite oddD odd_double addbF.
 Qed.
 
 Lemma odd_tperm x y : odd_perm (tperm x y) = (x != y).
@@ -490,7 +490,7 @@ Lemma odd_permM : {morph odd_perm : s1 s2 / s1 * s2 >-> s1 (+) s2}.
 Proof.
 move=> s1 s2; case: (prod_tpermP s1) => ts1 ->{s1} dts1.
 case: (prod_tpermP s2) => ts2 ->{s2} dts2.
-by rewrite -big_cat !odd_perm_prod ?all_cat ?dts1 // size_cat odd_add.
+by rewrite -big_cat !odd_perm_prod ?all_cat ?dts1 // size_cat oddD.
 Qed.
 
 Lemma odd_permV s : odd_perm s^-1 = odd_perm s.

mathcomp/ssreflect/div.v

@@ -329,7 +329,7 @@ Proof. by rewrite [in RHS](divn_eq m 2) modn2 muln2 addnC half_bit_double. Qed.
 
 Lemma odd_mod m d : odd d = false -> odd (m %% d) = odd m.
 Proof.
-by move=> d_even; rewrite [in RHS](divn_eq m d) odd_add odd_mul d_even andbF.
+by move=> d_even; rewrite [in RHS](divn_eq m d) oddD odd_mul d_even andbF.
 Qed.
 
 Lemma modnXm m n a : (a %% n) ^ m = a ^ m %[mod n].

mathcomp/ssreflect/seq.v

@@ -282,7 +282,7 @@ Lemma cat_cons x s1 s2 : (x :: s1) ++ s2 = x :: s1 ++ s2. Proof. by []. Qed.
 Lemma cat_nseq n x s : nseq n x ++ s = ncons n x s.
 Proof. by elim: n => //= n ->. Qed.
 
-Lemma nseq_addn n1 n2 x :
+Lemma nseqD n1 n2 x :
   nseq (n1 + n2) x = nseq n1 x ++ nseq n2 x.
 Proof. by rewrite cat_nseq /nseq /ncons iter_add. Qed.
 
@@ -772,7 +772,7 @@ Qed.
 Lemma take_drop i j s : take i (drop j s) = drop j (take (i + j) s).
 Proof. by rewrite addnC; elim: s i j => // x s IHs [|i] [|j] /=. Qed.
 
-Lemma take_addn i j s : take (i + j) s = take i s ++ take j (drop i s).
+Lemma takeD i j s : take (i + j) s = take i s ++ take j (drop i s).
 Proof.
 elim: i j s => [|i IHi] [|j] [|a s] //; first by rewrite take0 addn0 cats0.
 by rewrite addSn /= IHi.
@@ -788,12 +788,12 @@ by case: s => [|a s]//; rewrite /= ltnS.
 Qed.
 
 Lemma take_nseq i j x : i <= j -> take i (nseq j x) = nseq i x.
-Proof. by move=>/subnKC <-; rewrite nseq_addn take_size_cat // size_nseq. Qed.
+Proof. by move=>/subnKC <-; rewrite nseqD take_size_cat // size_nseq. Qed.
 
 Lemma drop_nseq i j x : drop i (nseq j x) = nseq (j - i) x.
 Proof.
 case: (leqP i j) => [/subnKC {1}<-|/ltnW j_le_i].
-  by rewrite nseq_addn drop_size_cat // size_nseq.
+  by rewrite nseqD drop_size_cat // size_nseq.
 by rewrite drop_oversize ?size_nseq // (eqP j_le_i).
 Qed.
 
@@ -890,7 +890,7 @@ Lemma all_rev a s : all a (rev s) = all a s.
 Proof. by rewrite !all_count count_rev size_rev. Qed.
 
 Lemma rev_nseq n x : rev (nseq n x) = nseq n x.
-Proof. by elim: n => // n IHn; rewrite -{1}(addn1 n) nseq_addn rev_cat IHn. Qed.
+Proof. by elim: n => // n IHn; rewrite -[in LHS]addn1 nseqD rev_cat IHn. Qed.
 
 End Sequences.
 
@@ -1784,21 +1784,21 @@ Section RotCompLemmas.
 Variable T : Type.
 Implicit Type s : seq T.
 
-Lemma rot_addn m n s : m + n <= size s -> rot (m + n) s = rot m (rot n s).
+Lemma rotD m n s : m + n <= size s -> rot (m + n) s = rot m (rot n s).
 Proof.
 move=> sz_s; rewrite {1}/rot -[take _ s](cat_take_drop n).
 rewrite 5!(catA, =^~ rot_size_cat) !cat_take_drop.
 by rewrite size_drop !size_takel ?leq_addl ?addnK.
 Qed.
 
 Lemma rotS n s : n < size s -> rot n.+1 s = rot 1 (rot n s).
-Proof. exact: (@rot_addn 1). Qed.
+Proof. exact: (@rotD 1). Qed.
 
 Lemma rot_add_mod m n s : n <= size s -> m <= size s ->
   rot m (rot n s) = rot (if m + n <= size s then m + n else m + n - size s) s.
 Proof.
-move=> Hn Hm; case: leqP => [/rot_addn // | /ltnW Hmn]; symmetry.
-by rewrite -{2}(rotK n s) /rotr -rot_addn size_rot addnBA ?subnK ?addnK.
+move=> Hn Hm; case: leqP => [/rotD // | /ltnW Hmn]; symmetry.
+by rewrite -{2}(rotK n s) /rotr -rotD size_rot addnBA ?subnK ?addnK.
 Qed.
 
 Lemma rot_rot m n s : rot m (rot n s) = rot n (rot m s).
@@ -3340,7 +3340,7 @@ have take'x t i: i <= index x t -> i <= size t /\ x \notin take i t.
 pose xrot t i := rot i (x :: t); pose xrotV t := index x (rev (rot 1 t)).
 have xrotK t: {in le_x t, cancel (xrot t) xrotV}.
   move=> i; rewrite mem_iota addn1 /xrotV => /take'x[le_i_t ti'x].
-  rewrite -rot_addn ?rev_cat //= rev_cons cat_rcons index_cat mem_rev size_rev.
+  rewrite -rotD ?rev_cat //= rev_cons cat_rcons index_cat mem_rev size_rev.
   by rewrite ifN // size_takel //= eqxx addn0.
 apply/uniq_perm=> [||t]; first exact: permutations_uniq.
   apply/allpairs_uniq_dep=> [|t _|]; rewrite ?permutations_uniq ?iota_uniq //.
@@ -3426,6 +3426,9 @@ Notation "[ '<->' P0 ; P1 ; .. ; Pn ]" :=
 Ltac tfae := do !apply: AllIffConj.
 
 (* Temporary backward compatibility. *)
+Notation take_addn := (deprecate take_addn takeD _) (only parsing).
+Notation rot_addn := (deprecate rot_addn rotD _) (only parsing).
+Notation nseq_addn := (deprecate nseq_addn nseqD _) (only parsing).
 Notation perm_eq_rev := (deprecate perm_eq_rev perm_rev _)
   (only parsing).
 Notation perm_eq_flatten := (deprecate perm_eq_flatten perm_flatten _ _ _)

mathcomp/ssreflect/ssrnat.v

@@ -1245,19 +1245,19 @@ Fixpoint odd n := if n is n'.+1 then ~~ odd n' else false.
 
 Lemma oddb (b : bool) : odd b = b. Proof. by case: b. Qed.
 
-Lemma odd_add m n : odd (m + n) = odd m (+) odd n.
+Lemma oddD m n : odd (m + n) = odd m (+) odd n.
 Proof. by elim: m => [|m IHn] //=; rewrite -addTb IHn addbA addTb. Qed.
 
-Lemma odd_sub m n : n <= m -> odd (m - n) = odd m (+) odd n.
+Lemma oddB m n : n <= m -> odd (m - n) = odd m (+) odd n.
 Proof.
-by move=> le_nm; apply: (@canRL bool) (addbK _) _; rewrite -odd_add subnK.
+by move=> le_nm; apply: (@canRL bool) (addbK _) _; rewrite -oddD subnK.
 Qed.
 
 Lemma odd_opp i m : odd m = false -> i <= m -> odd (m - i) = odd i.
-Proof. by move=> oddm le_im; rewrite (odd_sub (le_im)) oddm. Qed.
+Proof. by move=> oddm le_im; rewrite (oddB (le_im)) oddm. Qed.
 
 Lemma odd_mul m n : odd (m * n) = odd m && odd n.
-Proof. by elim: m => //= m IHm; rewrite odd_add -addTb andb_addl -IHm. Qed.
+Proof. by elim: m => //= m IHm; rewrite oddD -addTb andb_addl -IHm. Qed.
 
 Lemma odd_exp m n : odd (m ^ n) = (n == 0) || odd m.
 Proof. by elim: n => // n IHn; rewrite expnS odd_mul {}IHn orbC; case odd. Qed.
@@ -1304,7 +1304,7 @@ Lemma leq_Sdouble m n : (m.*2 <= n.*2.+1) = (m <= n).
 Proof. by rewrite leqNgt ltn_Sdouble -leqNgt. Qed.
 
 Lemma odd_double n : odd n.*2 = false.
-Proof. by rewrite -addnn odd_add addbb. Qed.
+Proof. by rewrite -addnn oddD addbb. Qed.
 
 Lemma double_gt0 n : (0 < n.*2) = (0 < n).
 Proof. by case: n. Qed.
@@ -1918,3 +1918,7 @@ Lemma ltngtP m n : compare_nat m n (n == m) (m == n) (n <= m)
 Proof. by case: ltngtP; constructor. Qed.
 
 End mc_1_10.
+
+(* Temporary backward compatibility. *)
+Notation odd_add := (deprecate odd_add oddD _) (only parsing).
+Notation odd_sub := (deprecate odd_sub oddB _) (only parsing).