diff options
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 4 | ||||
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 9 |
2 files changed, 9 insertions, 4 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index ecf539a..c635497 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -272,6 +272,10 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - in `seq.v` new lemmas `eqseq_pivot`, `eqseq_pivot_uniql`, `eqseq_pivot_uniqr`, `mask_rcons, `rev_mask`, `subseq_rev`, `subseq_cat2l`, `subseq_cat2r`, `subseq_rot`, and +- in `seq.v` new lemmas `index_pivot`, `take_pivot`, `rev_pivot`, + `eqseq_pivot2l`, `eqseq_pivot2r`, `eqseq_pivotl`, `eqseq_pivotr` + `uniq_eqseq_pivotl`, `uniq_eqseq_pivotr`, `mask_rcons, `rev_mask`, + `subseq_rev`, `subseq_cat2l`, `subseq_cat2r`, `subseq_rot`, and `uniq_subseq_pivot`. ### Changed diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 16f17c3..a85ff76 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -1395,12 +1395,13 @@ Proof. by move=> x; rewrite -[s in RHS](cat_take_drop n0) !mem_cat /= orbC. Qed. Lemma eqseq_rot s1 s2 : (rot n0 s1 == rot n0 s2) = (s1 == s2). Proof. exact/inj_eq/rot_inj. Qed. +(* lemmas about the pivot pattern [_ ++ _ :: _] *) -Lemma index_pivot x s1 s2 (s := s1 ++ x :: s2) : x \notin s1 -> +Lemma index_pivot x s1 s2 (s := s1 ++ x :: s2) : x \notin s1 -> index x s = size s1. Proof. by rewrite index_cat/= eqxx addn0; case: ifPn. Qed. -Lemma take_pivot x s2 s1 (s := s1 ++ x :: s2) : x \notin s1 -> +Lemma take_pivot x s2 s1 (s := s1 ++ x :: s2) : x \notin s1 -> take (index x s) s = s1. Proof. by move=> /index_pivot->; rewrite take_size_cat. Qed. @@ -1419,7 +1420,7 @@ Lemma eqseq_pivot2r x s1 s2 s3 s4 : x \notin s2 -> x \notin s4 -> (s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4). Proof. move=> xNs2 xNs4; rewrite -(can_eq revK) !rev_pivot. -by rewrite eqseq_pivot2l ?mem_rev// !(can_eq revK) andbC. +by rewrite eqseq_pivot2l ?mem_rev // !(can_eq revK) andbC. Qed. Lemma eqseq_pivotl x s1 s2 s3 s4 : x \notin s1 -> x \notin s2 -> @@ -2394,7 +2395,7 @@ Proof. move => uniq_s sub_s'_s; have uniq_s' := subseq_uniq sub_s'_s uniq_s. have/eqP {sub_s'_s uniq_s} := subseq_uniqP _ uniq_s sub_s'_s. rewrite !filter_cat /= mem_cat inE eqxx orbT /=. -rewrite eqseq_pivot_uniql // => /andP [/eqP -> /eqP ->]. +rewrite uniq_eqseq_pivotl // => /andP [/eqP -> /eqP ->]. by rewrite !filter_subseq. Qed. |