diff options
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 30 |
2 files changed, 25 insertions, 7 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index d8bd318..38d15bc 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -251,6 +251,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - in `polydiv.v`, new lemma `dvdpNl`. +- in `seq.v`, new definition `rot_add` and new lemmas `rot_minn`, `leq_rot_add`, `rot_addC`, `rot_rot_add`. + ### Changed - in ssrbool.v, use `Reserved Notation` for `[rel _ _ : _ | _]` to avoid warnings with coq-8.12 diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 7cdc422..1e9e1c9 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -1854,17 +1854,33 @@ 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). +Lemma rot_minn n s : rot n s = rot (minn n (size s)) s. +Proof. +by case: (leqP n (size s)) => // /leqW ?; rewrite rot_size rot_oversize. +Qed. + +Definition rot_add s n m (k := size s) (p := minn m k + minn n k) := + locked (if p <= k then p else p - k). + +Lemma leq_rot_add n m s : rot_add s n m <= size s. Proof. -case: (ltnP (size s) m) => Hm. - by rewrite !(@rot_oversize T m) ?size_rot 1?ltnW. -case: (ltnP (size s) n) => Hn. - by rewrite !(@rot_oversize T n) ?size_rot 1?ltnW. -by rewrite !rot_add_mod 1?addnC. +by unlock rot_add; case: ifP; rewrite // leq_subLR leq_add // geq_minr. Qed. +Lemma rot_addC n m s : rot_add s n m = rot_add s m n. +Proof. by unlock rot_add; rewrite ![minn n _ + _]addnC. Qed. + +Lemma rot_rot_add n m s : rot m (rot n s) = rot (rot_add s n m) s. +Proof. +unlock rot_add. +by rewrite (rot_minn n) (rot_minn m) rot_add_mod ?size_rot ?geq_minr. +Qed. + +Lemma rot_rot m n s : rot m (rot n s) = rot n (rot m s). +Proof. by rewrite rot_rot_add rot_addC -rot_rot_add. Qed. + Lemma rot_rotr m n s : rot m (rotr n s) = rotr n (rot m s). -Proof. by rewrite {2}/rotr size_rot rot_rot. Qed. +Proof. by rewrite [RHS]/rotr size_rot rot_rot. Qed. Lemma rotr_rotr m n s : rotr m (rotr n s) = rotr n (rotr m s). Proof. by rewrite /rotr !size_rot rot_rot. Qed. |