From 7bef434688cea376694fbde648f31867d04d8d88 Mon Sep 17 00:00:00 2001 From: Christian Doczkal Date: Thu, 1 Oct 2020 18:06:03 +0200 Subject: lemmas on subseq and rot --- mathcomp/ssreflect/seq.v | 53 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 53 insertions(+) (limited to 'mathcomp') diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index ed0b998..91085be 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -1395,6 +1395,17 @@ 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. +Lemma eqseq_pivot s1 s2 s3 s4 x : + uniq (s3 ++ x :: s4) -> s1 ++ x :: s2 == s3 ++ x :: s4 = (s1 == s3) && (s2 == s4). +Proof. +move=> uniq34; apply/idP/idP => [E|/andP [/eqP-> /eqP->] //]. +suff S : size s1 = size s3 by rewrite eqseq_cat // eqseq_cons eqxx in E. +gen have I,I1 : s3 s4 uniq34 {E} / size s3 = index x (s3 ++ x :: s4). + rewrite index_cat index_head addn0 ifN //. + by apply: contraTN uniq34 => x_s3; rewrite cat_uniq /= x_s3 /= andbF. +by rewrite I1 -(eqP E) -I // (eqP E). +Qed. + End EqSeq. Section RotIndex. @@ -1936,6 +1947,13 @@ Proof. by case: b. Qed. Lemma has_mask a m s : has a (mask m s) -> has a s. Proof. by apply/contraTT; rewrite -!all_predC; apply: all_mask. Qed. +Lemma rev_mask m s : size m = size s -> rev (mask m s) = mask (rev m) (rev s). +Proof. +move: m s; apply: seq_ind2 => //= b x m s ? IH. +rewrite fun_if !rev_cons -!cats1 IH // mask_cat ?size_rev //. +by case: b => //=; rewrite cats0. +Qed. + Lemma mask_rot m s : size m = size s -> mask (rot n0 m) (rot n0 s) = rot (count id (take n0 m)) (mask m s). Proof. @@ -2108,6 +2126,31 @@ elim: s => //= x s; case: (_ \in _); last by rewrite eqxx. by case: (undup s) => //= y u; case: (_ == _) => //=; apply: cons_subseq. Qed. +Lemma subseq_rev s1 s2 : subseq (rev s1) (rev s2) = subseq s1 s2. +Proof. +wlog suff W : s1 s2 / subseq s1 s2 -> subseq (rev s1) (rev s2). + by apply/idP/idP => /W //; rewrite !revK. +move/subseqP => [m size_m mask_m]; apply/subseqP. +by exists (rev m); rewrite ?size_rev // -rev_mask // -mask_m. +Qed. + +Lemma subseq_cat2l (s s1 s2 : seq T) : + subseq (s ++ s1) (s ++ s2) = subseq s1 s2. +Proof. by elim: s => // x s IHs; rewrite !cat_cons /= eqxx. Qed. + +Lemma subseq_cat2r (s s1 s2 : seq T) : + subseq (s1 ++ s) (s2 ++ s) = subseq s1 s2. +Proof. by rewrite -subseq_rev !rev_cat subseq_cat2l subseq_rev. Qed. + +Lemma subseq_rot p s n : + subseq p s -> exists2 k, k <= n & subseq (rot k p) (rot n s). +Proof. +move => /subseqP [m size_m ->]. +exists (count id (take n m)); last by rewrite -mask_rot // mask_subseq. +apply: leq_trans (count_size _ _) _; rewrite size_take. +by case: (ltnP n (size m)). +Qed. + End Subseq. Prenex Implicits subseq. @@ -2300,6 +2343,16 @@ rewrite uniq_perm ?filter_uniq ?(subseq_uniq ss12) // => x. by rewrite mem_filter; apply: andb_idr; apply: (mem_subseq ss12). Qed. +Lemma subseq_pivot (s1 s2 s3 s4 : seq T) x (s := s3 ++ x :: s4) : + uniq s -> subseq (s1 ++ x :: s2) s -> subseq s1 s3 /\ subseq s2 s4. +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 /= => E. +move: (E); rewrite eqseq_pivot -?(eqP E) // => /andP [/eqP -> /eqP ->]. +by rewrite !filter_subseq. +Qed. + Lemma perm_to_subseq s1 s2 : subseq s1 s2 -> {s3 | perm_eq s2 (s1 ++ s3)}. Proof. -- cgit v1.2.3 From 188ffa169aeaf83fe111753380699f0f20915ce9 Mon Sep 17 00:00:00 2001 From: Christian Doczkal Date: Wed, 4 Nov 2020 20:32:09 +0100 Subject: suggestions from Cyril --- mathcomp/ssreflect/seq.v | 46 ++++++++++++++++++++++++++++++++-------------- 1 file changed, 32 insertions(+), 14 deletions(-) (limited to 'mathcomp') diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 91085be..72acafe 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -1395,15 +1395,30 @@ 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. -Lemma eqseq_pivot s1 s2 s3 s4 x : - uniq (s3 ++ x :: s4) -> s1 ++ x :: s2 == s3 ++ x :: s4 = (s1 == s3) && (s2 == s4). + +Lemma eqseq_pivot x s1 s2 s3 s4 : x \notin s1 -> x \notin s3 -> + s1 ++ x :: s2 == s3 ++ x :: s4 = (s1 == s3) && (s2 == s4). Proof. -move=> uniq34; apply/idP/idP => [E|/andP [/eqP-> /eqP->] //]. +move=> xNs1 xNs3; apply/idP/idP => [E|/andP [/eqP-> /eqP->] //]. suff S : size s1 = size s3 by rewrite eqseq_cat // eqseq_cons eqxx in E. -gen have I,I1 : s3 s4 uniq34 {E} / size s3 = index x (s3 ++ x :: s4). - rewrite index_cat index_head addn0 ifN //. - by apply: contraTN uniq34 => x_s3; rewrite cat_uniq /= x_s3 /= andbF. -by rewrite I1 -(eqP E) -I // (eqP E). +gen have I,I1 : s1 s2 xNs1 {E} / size s1 = index x (s1 ++ x :: s2). + by rewrite index_cat (negPf xNs1) index_head addn0. +by rewrite I1 (eqP E) -I. +Qed. + +Lemma eqseq_pivot_uniqr x s1 s2 s3 s4 (s := s3 ++ x :: s4) : + uniq s -> s1 ++ x :: s2 == s = (s1 == s3) && (s2 == s4). +Proof. +move=> /= uniq_s; apply/idP/idP => [/eqP E|/andP [/eqP-> /eqP->] //=]. +have N1 p1 p2 : uniq (p1 ++ x :: p2) -> x \notin p1. + by rewrite cat_uniq /=; case (_ \in p1); rewrite //= andbF. +by rewrite -(@eqseq_pivot x) ?E // ?(N1 s3 s4) // (N1 s1 s2) ?E. +Qed. + +Lemma eqseq_pivot_uniql x s1 s2 s3 s4 (s := s1 ++ x :: s2) : + uniq s -> s == s3 ++ x :: s4 = (s1 == s3) && (s2 == s4). +Proof. +by move=> ?; rewrite eq_sym eqseq_pivot_uniqr// [_ == s1]eq_sym [_ == s2]eq_sym. Qed. End EqSeq. @@ -1485,7 +1500,7 @@ Definition bitseq := seq bool. Canonical bitseq_eqType := Eval hnf in [eqType of bitseq]. Canonical bitseq_predType := Eval hnf in [predType of bitseq]. -(* Generalized versions of splitP (from path.v): split_find_nth and split_find *) +(* Generalizations of splitP (from path.v): split_find_nth and split_find *) Section FindNth. Variables (T : Type). Implicit Types (x : T) (p : pred T) (s : seq T). @@ -1937,6 +1952,10 @@ Lemma mask_cat m1 m2 s1 s2 : size m1 = size s1 -> mask (m1 ++ m2) (s1 ++ s2) = mask m1 s1 ++ mask m2 s2. Proof. by move: m1 s1; apply: seq_ind2 => // -[] m1 x1 s1 /= _ ->. Qed. +Lemma mask_rcons b m x s : size m = size s -> + mask (rcons m b) (rcons s x) = mask m s ++ nseq b x. +Proof. by move=> ms; rewrite -!cats1 mask_cat//; case: b. Qed. + Lemma all_mask a m s : all a s -> all a (mask m s). Proof. by elim: s m => [|x s IHs] [|[] m]//= /andP[ax /IHs->]; rewrite ?ax. Qed. @@ -1949,9 +1968,8 @@ Proof. by apply/contraTT; rewrite -!all_predC; apply: all_mask. Qed. Lemma rev_mask m s : size m = size s -> rev (mask m s) = mask (rev m) (rev s). Proof. -move: m s; apply: seq_ind2 => //= b x m s ? IH. -rewrite fun_if !rev_cons -!cats1 IH // mask_cat ?size_rev //. -by case: b => //=; rewrite cats0. +move: m s; apply: seq_ind2 => //= b x m s eq_size_sm IH. +by case: b; rewrite !rev_cons mask_rcons ?IH ?size_rev// (cats1, cats0). Qed. Lemma mask_rot m s : size m = size s -> @@ -2343,13 +2361,13 @@ rewrite uniq_perm ?filter_uniq ?(subseq_uniq ss12) // => x. by rewrite mem_filter; apply: andb_idr; apply: (mem_subseq ss12). Qed. -Lemma subseq_pivot (s1 s2 s3 s4 : seq T) x (s := s3 ++ x :: s4) : +Lemma uniq_subseq_pivot (s1 s2 s3 s4 : seq T) x (s := s3 ++ x :: s4) : uniq s -> subseq (s1 ++ x :: s2) s -> subseq s1 s3 /\ subseq s2 s4. 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 /= => E. -move: (E); rewrite eqseq_pivot -?(eqP E) // => /andP [/eqP -> /eqP ->]. +rewrite !filter_cat /= mem_cat inE eqxx orbT /=. +rewrite eqseq_pivot_uniql // => /andP [/eqP -> /eqP ->]. by rewrite !filter_subseq. Qed. -- cgit v1.2.3 From cde6e5af0d272081884f3dc1813ebbbabc0198c3 Mon Sep 17 00:00:00 2001 From: Christian Doczkal Date: Fri, 6 Nov 2020 20:09:52 +0100 Subject: Apply suggestions from code review Co-authored-by: Cyril Cohen --- mathcomp/ssreflect/seq.v | 63 ++++++++++++++++++++++++++++++++++-------------- 1 file changed, 45 insertions(+), 18 deletions(-) (limited to 'mathcomp') diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 72acafe..16f17c3 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -1396,29 +1396,57 @@ Lemma eqseq_rot s1 s2 : (rot n0 s1 == rot n0 s2) = (s1 == s2). Proof. exact/inj_eq/rot_inj. Qed. -Lemma eqseq_pivot x s1 s2 s3 s4 : x \notin s1 -> x \notin s3 -> - s1 ++ x :: s2 == s3 ++ x :: s4 = (s1 == s3) && (s2 == s4). +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 -> + take (index x s) s = s1. +Proof. by move=> /index_pivot->; rewrite take_size_cat. Qed. + +Lemma rev_pivot x s1 s2 : rev (s1 ++ x :: s2) = rev s2 ++ x :: rev s1. +Proof. by rewrite rev_cat rev_cons cat_rcons. Qed. + +Lemma eqseq_pivot2l x s1 s2 s3 s4 : x \notin s1 -> x \notin s3 -> + (s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4). +Proof. +move=> xNs1 xNs3; apply/idP/idP => [E|/andP[/eqP-> /eqP->]//]. +suff S : size s1 = size s3 by rewrite eqseq_cat// eqseq_cons eqxx in E. +by rewrite -(index_pivot s2 xNs1) (eqP E) index_pivot. +Qed. + +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. +Qed. + +Lemma eqseq_pivotl x s1 s2 s3 s4 : x \notin s1 -> x \notin s2 -> + (s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4). +Proof. +move=> xNs1 xNs2; apply/idP/idP => [E|/andP[/eqP-> /eqP->]//]. +rewrite -(@eqseq_pivot2l x)//; have /eqP/(congr1 (count_mem x)) := E. +rewrite !count_cat/= eqxx !addnS (count_memPn _ _ xNs1) (count_memPn _ _ xNs2). +by move=> -[/esym/eqP]; rewrite addn_eq0 => /andP[/eqP/count_memPn]. +Qed. + +Lemma eqseq_pivotr x s1 s2 s3 s4 : x \notin s3 -> x \notin s4 -> + (s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4). Proof. -move=> xNs1 xNs3; apply/idP/idP => [E|/andP [/eqP-> /eqP->] //]. -suff S : size s1 = size s3 by rewrite eqseq_cat // eqseq_cons eqxx in E. -gen have I,I1 : s1 s2 xNs1 {E} / size s1 = index x (s1 ++ x :: s2). - by rewrite index_cat (negPf xNs1) index_head addn0. -by rewrite I1 (eqP E) -I. +by move=> *; rewrite eq_sym eqseq_pivotl// [s3 == _]eq_sym [s4 == _]eq_sym. Qed. -Lemma eqseq_pivot_uniqr x s1 s2 s3 s4 (s := s3 ++ x :: s4) : - uniq s -> s1 ++ x :: s2 == s = (s1 == s3) && (s2 == s4). +Lemma uniq_eqseq_pivotl x s1 s2 s3 s4 : uniq (s1 ++ x :: s2) -> + (s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4). Proof. -move=> /= uniq_s; apply/idP/idP => [/eqP E|/andP [/eqP-> /eqP->] //=]. -have N1 p1 p2 : uniq (p1 ++ x :: p2) -> x \notin p1. - by rewrite cat_uniq /=; case (_ \in p1); rewrite //= andbF. -by rewrite -(@eqseq_pivot x) ?E // ?(N1 s3 s4) // (N1 s1 s2) ?E. +by rewrite uniq_catC/= mem_cat => /andP[/norP[? ?] _]; rewrite eqseq_pivotl. Qed. -Lemma eqseq_pivot_uniql x s1 s2 s3 s4 (s := s1 ++ x :: s2) : - uniq s -> s == s3 ++ x :: s4 = (s1 == s3) && (s2 == s4). +Lemma uniq_eqseq_pivotr x s1 s2 s3 s4 : uniq (s3 ++ x :: s4) -> + (s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4). Proof. -by move=> ?; rewrite eq_sym eqseq_pivot_uniqr// [_ == s1]eq_sym [_ == s2]eq_sym. +by move=> ?; rewrite eq_sym uniq_eqseq_pivotl// [s3 == _]eq_sym [s4 == _]eq_sym. Qed. End EqSeq. @@ -2165,8 +2193,7 @@ Lemma subseq_rot p s n : Proof. move => /subseqP [m size_m ->]. exists (count id (take n m)); last by rewrite -mask_rot // mask_subseq. -apply: leq_trans (count_size _ _) _; rewrite size_take. -by case: (ltnP n (size m)). +by rewrite (leq_trans (count_size _ _))// size_take; case: ltnP. Qed. End Subseq. -- cgit v1.2.3 From 2acb66dcb2d8e571b3edfecf70099893187a169f Mon Sep 17 00:00:00 2001 From: Christian Doczkal Date: Fri, 6 Nov 2020 20:41:52 +0100 Subject: fixup after feedback from Cyril --- mathcomp/ssreflect/seq.v | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'mathcomp') 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. -- cgit v1.2.3 From cd8f803281d5e62fb474192605f1de455c21bc4b Mon Sep 17 00:00:00 2001 From: Christian Doczkal Date: Mon, 9 Nov 2020 11:36:33 +0100 Subject: Apply suggestions from code review Co-authored-by: Cyril Cohen Co-authored-by: Kazuhiko Sakaguchi --- mathcomp/ssreflect/seq.v | 17 +++++------------ 1 file changed, 5 insertions(+), 12 deletions(-) (limited to 'mathcomp') diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index a85ff76..57866a4 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -1434,9 +1434,7 @@ Qed. Lemma eqseq_pivotr x s1 s2 s3 s4 : x \notin s3 -> x \notin s4 -> (s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4). -Proof. -by move=> *; rewrite eq_sym eqseq_pivotl// [s3 == _]eq_sym [s4 == _]eq_sym. -Qed. +Proof. by move=> *; rewrite eq_sym eqseq_pivotl//; case: eqVneq => /=. Qed. Lemma uniq_eqseq_pivotl x s1 s2 s3 s4 : uniq (s1 ++ x :: s2) -> (s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4). @@ -1446,9 +1444,7 @@ Qed. Lemma uniq_eqseq_pivotr x s1 s2 s3 s4 : uniq (s3 ++ x :: s4) -> (s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4). -Proof. -by move=> ?; rewrite eq_sym uniq_eqseq_pivotl// [s3 == _]eq_sym [s4 == _]eq_sym. -Qed. +Proof. by move=> ?; rewrite eq_sym uniq_eqseq_pivotl//; case: eqVneq => /=. Qed. End EqSeq. @@ -2177,16 +2173,13 @@ Lemma subseq_rev s1 s2 : subseq (rev s1) (rev s2) = subseq s1 s2. Proof. wlog suff W : s1 s2 / subseq s1 s2 -> subseq (rev s1) (rev s2). by apply/idP/idP => /W //; rewrite !revK. -move/subseqP => [m size_m mask_m]; apply/subseqP. -by exists (rev m); rewrite ?size_rev // -rev_mask // -mask_m. +by case/subseqP => m size_m ->; rewrite rev_mask // mask_subseq. Qed. -Lemma subseq_cat2l (s s1 s2 : seq T) : - subseq (s ++ s1) (s ++ s2) = subseq s1 s2. +Lemma subseq_cat2l s s1 s2 : subseq (s ++ s1) (s ++ s2) = subseq s1 s2. Proof. by elim: s => // x s IHs; rewrite !cat_cons /= eqxx. Qed. -Lemma subseq_cat2r (s s1 s2 : seq T) : - subseq (s1 ++ s) (s2 ++ s) = subseq s1 s2. +Lemma subseq_cat2r s s1 s2 : subseq (s1 ++ s) (s2 ++ s) = subseq s1 s2. Proof. by rewrite -subseq_rev !rev_cat subseq_cat2l subseq_rev. Qed. Lemma subseq_rot p s n : -- cgit v1.2.3 From 85aee7ba9a19dceccc49c16b3d9eb295c60de774 Mon Sep 17 00:00:00 2001 From: Christian Doczkal Date: Wed, 11 Nov 2020 18:06:31 +0100 Subject: turn uniq_subseq_pivot into equality --- mathcomp/ssreflect/seq.v | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'mathcomp') diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 57866a4..99405ec 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -2185,7 +2185,7 @@ Proof. by rewrite -subseq_rev !rev_cat subseq_cat2l subseq_rev. Qed. Lemma subseq_rot p s n : subseq p s -> exists2 k, k <= n & subseq (rot k p) (rot n s). Proof. -move => /subseqP [m size_m ->]. +move=> /subseqP[m size_m ->]. exists (count id (take n m)); last by rewrite -mask_rot // mask_subseq. by rewrite (leq_trans (count_size _ _))// size_take; case: ltnP. Qed. @@ -2383,9 +2383,11 @@ by rewrite mem_filter; apply: andb_idr; apply: (mem_subseq ss12). Qed. Lemma uniq_subseq_pivot (s1 s2 s3 s4 : seq T) x (s := s3 ++ x :: s4) : - uniq s -> subseq (s1 ++ x :: s2) s -> subseq s1 s3 /\ subseq s2 s4. + uniq s -> subseq (s1 ++ x :: s2) s = (subseq s1 s3 && subseq s2 s4). Proof. -move => uniq_s sub_s'_s; have uniq_s' := subseq_uniq sub_s'_s uniq_s. +move=> uniq_s; apply/idP/idP => [sub_s'_s|/andP[? ?]]; last first. + by rewrite cat_subseq //= eqxx. +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 uniq_eqseq_pivotl // => /andP [/eqP -> /eqP ->]. -- cgit v1.2.3 From b408b52bcb89468c7d61c4c56c2e7c02d8f458a8 Mon Sep 17 00:00:00 2001 From: Christian Doczkal Date: Wed, 11 Nov 2020 20:32:54 +0100 Subject: make pivot the first argument in uniq_subseq_pivot Co-authored-by: Cyril Cohen --- mathcomp/ssreflect/seq.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'mathcomp') diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 99405ec..a9ddb5e 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -2382,10 +2382,10 @@ rewrite uniq_perm ?filter_uniq ?(subseq_uniq ss12) // => x. by rewrite mem_filter; apply: andb_idr; apply: (mem_subseq ss12). Qed. -Lemma uniq_subseq_pivot (s1 s2 s3 s4 : seq T) x (s := s3 ++ x :: s4) : +Lemma uniq_subseq_pivot x (s1 s2 s3 s4 : seq T) (s := s3 ++ x :: s4) : uniq s -> subseq (s1 ++ x :: s2) s = (subseq s1 s3 && subseq s2 s4). Proof. -move=> uniq_s; apply/idP/idP => [sub_s'_s|/andP[? ?]]; last first. +move=> uniq_s; apply/idP/idP => [sub_s'_s|/andP[? ?]]; last first. by rewrite cat_subseq //= eqxx. have uniq_s' := subseq_uniq sub_s'_s uniq_s. have/eqP {sub_s'_s uniq_s} := subseq_uniqP _ uniq_s sub_s'_s. -- cgit v1.2.3