diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/algebra/matrix.v | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/mxpoly.v | 2 | ||||
| -rw-r--r-- | mathcomp/fingroup/perm.v | 6 | ||||
| -rw-r--r-- | mathcomp/ssreflect/div.v | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 23 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 16 |
6 files changed, 29 insertions, 22 deletions
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index f49473f..21730c3 100644 --- a/mathcomp/algebra/matrix.v +++ b/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)). diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v index 4c97dfc..a8cf94b 100644 --- a/mathcomp/algebra/mxpoly.v +++ b/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 _). diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v index eb5e028..aff97b0 100644 --- a/mathcomp/fingroup/perm.v +++ b/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. diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v index b366055..9047a44 100644 --- a/mathcomp/ssreflect/div.v +++ b/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]. diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 6dc739e..dca4136 100644 --- a/mathcomp/ssreflect/seq.v +++ b/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,7 +1784,7 @@ 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. @@ -1792,13 +1792,13 @@ 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 _ _ _) diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index fb6a030..c2f2c52 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/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). |