From 9bc96e0d82346cdd62e769332c2adfb3a12dc6b7 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Sat, 10 Oct 2020 19:09:09 +0200 Subject: Adding some theory for `rem` and generalizing `subset_maskP` - Added helper lemmas about `rem`: `rem_cons` (to control unfolding), `remE`, `count_rem`, `count_mem_rem`, and `subseq_mem`. (New lemma `drop_index` briges the gap between `cat_take_drop` and `remE`). - `subset_maskP`, which was not released yet is generalized with hypothesis `(forall x, count_mem x s1 <= count_mem x s2)`, instead of `uniq s1` and `{subset s1 <= s2}`, the previous behaviour can be restored with helper lemma `leq_uniq_count` - Its trivial consequence `subset_subseqP` has been added too. --- CHANGELOG_UNRELEASED.md | 4 ++- mathcomp/ssreflect/seq.v | 87 ++++++++++++++++++++++++++++++++++++++---------- 2 files changed, 73 insertions(+), 18 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 46ba30d..073464c 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -228,7 +228,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). `commCmx`. The common arguments of these lemmas `R` and `n` are maximal implicits. - - in `seq.v`, added `in_mask`, `cons_subseq`, `undup_subseq`, `subset_maskP`. + - in `seq.v`, added `in_mask`, `cons_subseq`, `undup_subseq`, + `subset_maskP`, `subset_subseqP`, `count_rem`, `count_mem_rem`, + `rem_cons`, `remE`, `subseq_rem` and `leq_count_uniq`. - in `fintype.v`, added `mask_enum_ord`. - in `bigop.v`, added `big_mask_tuple` and `big_mask`. - in `mxalgebra.v`, new notation `stablemx V f` asserting that `f` diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index bb462a3..956a83e 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -1271,6 +1271,13 @@ elim: s => //= y s IHs /andP[/negbTE s'y /IHs-> {IHs}]. by rewrite in_cons; case: (eqVneq y x) => // <-; rewrite s'y. Qed. +Lemma leq_uniq_count s1 s2 : uniq s1 -> {subset s1 <= s2} -> + (forall x, count_mem x s1 <= count_mem x s2). +Proof. +move=> s1_uniq s1_s2 x; rewrite count_uniq_mem//. +by case: (boolP (_ \in _)) => // /s1_s2/count_memPn/eqP; rewrite -lt0n. +Qed. + Lemma filter_pred1_uniq s x : uniq s -> x \in s -> filter (pred1 x) s = [:: x]. Proof. move=> uniq_s s_x; rewrite (all_pred1P _ _ (filter_all _ _)). @@ -1395,6 +1402,9 @@ 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 drop_index s (n := index x0 s) : x0 \in s -> drop n s = x0 :: drop n.+1 s. +Proof. by move=> xs; rewrite (drop_nth x0) ?index_mem ?nth_index. Qed. + (* lemmas about the pivot pattern [_ ++ _ :: _] *) Lemma index_pivot x s1 s2 (s := s1 ++ x :: s2) : x \notin s1 -> @@ -1454,9 +1464,7 @@ Implicit Types x y z : T. Lemma rot_index s x (i := index x s) : x \in s -> rot i s = x :: (drop i.+1 s ++ take i s). -Proof. -by move=> x_s; rewrite /rot (drop_nth x) ?index_mem ?nth_index// cat_cons. -Qed. +Proof. by move=> x_s; rewrite /rot drop_index ?cat_cons. Qed. Variant rot_to_spec s x := RotToSpec i s' of rot i s = x :: s'. @@ -2203,16 +2211,21 @@ Variables (T : eqType) (x : T). Fixpoint rem s := if s is y :: t then (if y == x then t else y :: rem t) else s. +Lemma rem_cons y s : rem (y :: s) = if y == x then s else y :: rem s. +Proof. by []. Qed. + +Lemma remE s : rem s = take (index x s) s ++ drop (index x s).+1 s. +Proof. by elim: s => //= y s ->; case: eqVneq; rewrite ?drop0. Qed. + Lemma rem_id s : x \notin s -> rem s = s. Proof. -by elim: s => //= y s IHs /norP[neq_yx /IHs->]; rewrite eq_sym (negbTE neq_yx). +by move=> xNs; rewrite remE memNindex ?drop_oversize ?take_oversize ?cats0. Qed. Lemma perm_to_rem s : x \in s -> perm_eq s (x :: rem s). Proof. -elim: s => // y s IHs; rewrite inE /= eq_sym perm_sym. -case: eqP => [-> // | _ /IHs]. -by rewrite (perm_catCA [:: x] [:: y]) perm_cons perm_sym. +move=> xs; rewrite remE -[X in perm_eq X](cat_take_drop (index x s)). +by rewrite drop_index// -cat1s perm_catCA cat1s. Qed. Lemma size_rem s : x \in s -> size (rem s) = (size s).-1. @@ -2242,6 +2255,19 @@ Proof. by move/rem_filter=> -> y; rewrite mem_filter. Qed. Lemma mem_rem_uniqF s : uniq s -> x \in rem s = false. Proof. by move/mem_rem_uniq->; rewrite inE eqxx. Qed. +Lemma count_rem P s : count P (rem s) = count P s - (x \in s) && P x. +Proof. +have [xs|xNs]/= := boolP (x \in s); last by rewrite subn0 rem_id//. +rewrite -[s in RHS](cat_take_drop (index x s)) drop_index// remE !count_cat/=. +by rewrite addnCA addKn. +Qed. + +Lemma count_mem_rem y s : count_mem y (rem s) = count_mem y s - (x == y). +Proof. +rewrite count_rem/=; have [->|] := eqVneq y x; last by rewrite andbF subn0. +by have [|/count_memPn->] := boolP (x \in _). +Qed. + End Rem. Section Map. @@ -2347,8 +2373,12 @@ Notation "[ 'seq' E : R | i : T <- s & C ]" := Lemma filter_mask T a (s : seq T) : filter a s = mask (map a s) s. Proof. by elim: s => //= x s <-; case: (a x). Qed. -Lemma mask_filter (T : eqType) (s : seq T) (m : bitseq) : - uniq s -> mask m s = [seq i <- s | i \in mask m s]. +Section MiscMask. + +Variable (T : eqType). +Implicit Types (s : seq T) (m : bitseq). + +Lemma mask_filter s m : uniq s -> mask m s = [seq i <- s | i \in mask m s]. Proof. elim: m s => [|[] m ih] [|x s] //=. - by move=> _; elim: s. @@ -2357,6 +2387,29 @@ elim: m s => [|[] m ih] [|x s] //=. - by case: ifP => [/mem_mask -> // | _ /andP [] _ /ih]. Qed. +Lemma subset_maskP s1 s2 : (forall x, count_mem x s1 <= count_mem x s2) -> + exists2 m : bitseq, size m = size s2 & perm_eq s1 (mask m s2). +Proof. +move=> s1_le; suff [m mP]: exists m, perm_eq s1 (mask m s2). + by have [m' sm' eqm] := resize_mask m s2; exists m'; rewrite -?eqm. +elim: s2 => [|x s2 IHs]//= in s1 s1_le *. + by exists [::]; apply/allP => x _/=; rewrite eqn_leq s1_le. +have [xs1|xNs1] := boolP (x \in s1). + have [y|m s1s2] := IHs (rem x s1); first by rewrite count_mem_rem leq_subLR. + by exists (true :: m); rewrite (permPl (perm_to_rem xs1)) perm_cons. +have [y|m s1s2] := IHs s1; last by exists (false :: m). +have [<-|xNy] := eqVneq x y; first by rewrite (count_memPn xNs1). +by have := s1_le y; rewrite (negPf xNy). +Qed. + +Lemma subset_subseqP s1 s2 : (forall x, count_mem x s1 <= count_mem x s2) -> + exists2 t, subseq t s2 & perm_eq s1 t. +Proof. +by move=> /subset_maskP[m]; exists (mask m s2); rewrite ?mask_subseq. +Qed. + +End MiscMask. + Section FilterSubseq. Variable T : eqType. @@ -2403,15 +2456,15 @@ case: eqP => [-> | _] /IHs[s3 perm_s2] {IHs}. by exists (rcons s3 y); rewrite -cat_cons -perm_rcons -!cats1 catA perm_cat2r. Qed. -Lemma subset_maskP s1 s2 : uniq s1 -> {subset s1 <= s2} -> - exists2 m : seq bool, size m = size s2 & perm_eq s1 (mask m s2). +Lemma subseq_rem s1 s2 x : subseq s1 s2 -> subseq (rem x s1) (rem x s2). Proof. -move=> s1_uniq sub_s1_s2; pose s1' := [seq x <- undup s2 | x \in s1]. -have /subseqP[m sm s1'_eq] : subseq s1' s2. - by apply: subseq_trans (undup_subseq _); apply: filter_subseq. -exists m; rewrite // -s1'_eq; apply: uniq_perm => // [|x]. - by rewrite filter_uniq ?undup_uniq. -by rewrite mem_filter mem_undup; have [/sub_s1_s2|] := boolP (x \in s1). +elim: s2 x s1 => [|x2 s2 IHs1] x [|x1 s1]//=; first by rewrite sub0seq. +have [->|Nx12] := eqVneq x1 x2; first by case: eqP => //= _ /IHs1; rewrite eqxx. +have [->|Nx1] := eqVneq x x1. + rewrite eq_sym (negPf Nx12) => /(IHs1 x1). + by rewrite rem_cons eqxx => /subseq_trans->//; apply: subseq_cons. +move=> /(IHs1 x); rewrite rem_cons eq_sym (negPf Nx1) => /subseq_trans->//. +by have [->|Nx2] := eqVneq x x2; [apply: rem_subseq|apply: subseq_cons]. Qed. End FilterSubseq. -- cgit v1.2.3 From 74eb80a663cb1e45147a67dfa8c190547ee850e2 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Sun, 8 Nov 2020 00:25:59 +0100 Subject: Shorter proofs and suggestions by Kazuhiko Co-authored-by: Kazuhiko Sakaguchi --- CHANGELOG_UNRELEASED.md | 4 ++-- mathcomp/ssreflect/seq.v | 33 ++++++++++++++------------------- 2 files changed, 16 insertions(+), 21 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 073464c..c4abdf3 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -228,8 +228,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). `commCmx`. The common arguments of these lemmas `R` and `n` are maximal implicits. - - in `seq.v`, added `in_mask`, `cons_subseq`, `undup_subseq`, - `subset_maskP`, `subset_subseqP`, `count_rem`, `count_mem_rem`, + - in `seq.v`, added `drop_index`, `in_mask`, `cons_subseq`, `undup_subseq`, + `count_maskP`, `count_subseqP`, `count_rem`, `count_mem_rem`, `rem_cons`, `remE`, `subseq_rem` and `leq_count_uniq`. - in `fintype.v`, added `mask_enum_ord`. - in `bigop.v`, added `big_mask_tuple` and `big_mask`. diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 956a83e..aaeec2b 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -2219,7 +2219,7 @@ Proof. by elim: s => //= y s ->; case: eqVneq; rewrite ?drop0. Qed. Lemma rem_id s : x \notin s -> rem s = s. Proof. -by move=> xNs; rewrite remE memNindex ?drop_oversize ?take_oversize ?cats0. +by move=> xNs; rewrite remE memNindex ?take_size ?drop_oversize ?cats0. Qed. Lemma perm_to_rem s : x \in s -> perm_eq s (x :: rem s). @@ -2257,7 +2257,7 @@ Proof. by move/mem_rem_uniq->; rewrite inE eqxx. Qed. Lemma count_rem P s : count P (rem s) = count P s - (x \in s) && P x. Proof. -have [xs|xNs]/= := boolP (x \in s); last by rewrite subn0 rem_id//. +have [xs|xNs]/= := boolP (x \in s); last by rewrite subn0 rem_id. rewrite -[s in RHS](cat_take_drop (index x s)) drop_index// remE !count_cat/=. by rewrite addnCA addKn. Qed. @@ -2387,25 +2387,23 @@ elim: m s => [|[] m ih] [|x s] //=. - by case: ifP => [/mem_mask -> // | _ /andP [] _ /ih]. Qed. -Lemma subset_maskP s1 s2 : (forall x, count_mem x s1 <= count_mem x s2) -> +Lemma count_maskP s1 s2 : (forall x, count_mem x s1 <= count_mem x s2) -> exists2 m : bitseq, size m = size s2 & perm_eq s1 (mask m s2). Proof. move=> s1_le; suff [m mP]: exists m, perm_eq s1 (mask m s2). by have [m' sm' eqm] := resize_mask m s2; exists m'; rewrite -?eqm. elim: s2 => [|x s2 IHs]//= in s1 s1_le *. by exists [::]; apply/allP => x _/=; rewrite eqn_leq s1_le. -have [xs1|xNs1] := boolP (x \in s1). - have [y|m s1s2] := IHs (rem x s1); first by rewrite count_mem_rem leq_subLR. - by exists (true :: m); rewrite (permPl (perm_to_rem xs1)) perm_cons. -have [y|m s1s2] := IHs s1; last by exists (false :: m). -have [<-|xNy] := eqVneq x y; first by rewrite (count_memPn xNs1). -by have := s1_le y; rewrite (negPf xNy). +have [y|m s1s2] := IHs (rem x s1); first by rewrite count_mem_rem leq_subLR. +exists ((x \in s1) :: m); case: (boolP (x \in s1)). + by move/perm_to_rem/permPl->; rewrite perm_cons. +by rewrite -(permPr s1s2); move/rem_id->. Qed. -Lemma subset_subseqP s1 s2 : (forall x, count_mem x s1 <= count_mem x s2) -> +Lemma count_subseqP s1 s2 : (forall x, count_mem x s1 <= count_mem x s2) -> exists2 t, subseq t s2 & perm_eq s1 t. Proof. -by move=> /subset_maskP[m]; exists (mask m s2); rewrite ?mask_subseq. +by move=> /count_maskP[m]; exists (mask m s2); rewrite ?mask_subseq. Qed. End MiscMask. @@ -2456,15 +2454,12 @@ case: eqP => [-> | _] /IHs[s3 perm_s2] {IHs}. by exists (rcons s3 y); rewrite -cat_cons -perm_rcons -!cats1 catA perm_cat2r. Qed. -Lemma subseq_rem s1 s2 x : subseq s1 s2 -> subseq (rem x s1) (rem x s2). +Lemma subseq_rem x : {homo rem x : s1 s2 / @subseq T s1 s2}. Proof. -elim: s2 x s1 => [|x2 s2 IHs1] x [|x1 s1]//=; first by rewrite sub0seq. -have [->|Nx12] := eqVneq x1 x2; first by case: eqP => //= _ /IHs1; rewrite eqxx. -have [->|Nx1] := eqVneq x x1. - rewrite eq_sym (negPf Nx12) => /(IHs1 x1). - by rewrite rem_cons eqxx => /subseq_trans->//; apply: subseq_cons. -move=> /(IHs1 x); rewrite rem_cons eq_sym (negPf Nx1) => /subseq_trans->//. -by have [->|Nx2] := eqVneq x x2; [apply: rem_subseq|apply: subseq_cons]. +move=> s1 s2; elim: s2 s1 => [|x2 s2 IHs2] [|x1 s1]; rewrite ?sub0seq //=. +have [->|_] := eqVneq x1 x2; first by case: eqP => //= _ /IHs2; rewrite eqxx. +move/IHs2/subseq_trans=> -> //. +have [->|_] := eqVneq x x2; [apply: rem_subseq|apply: subseq_cons]. Qed. End FilterSubseq. -- cgit v1.2.3 From 94dd02febd112669b6a1543695df2eea5291dcde Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Mon, 9 Nov 2020 01:36:53 +0100 Subject: Equivalences instead of implications for `count_maskP` and `count_subseqP` --- CHANGELOG_UNRELEASED.md | 3 ++- mathcomp/ssreflect/seq.v | 36 +++++++++++++++++++++++++----------- 2 files changed, 27 insertions(+), 12 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index c4abdf3..6d4985b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -228,7 +228,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). `commCmx`. The common arguments of these lemmas `R` and `n` are maximal implicits. - - in `seq.v`, added `drop_index`, `in_mask`, `cons_subseq`, `undup_subseq`, + - in `seq.v`, added `drop_index`, `in_mask`, `cons_subseq`, + `undup_subseq`, `leq_count_mask`, `leq_count_subseq`, `count_maskP`, `count_subseqP`, `count_rem`, `count_mem_rem`, `rem_cons`, `remE`, `subseq_rem` and `leq_count_uniq`. - in `fintype.v`, added `mask_enum_ord`. diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index aaeec2b..14a7c26 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -2387,23 +2387,37 @@ elim: m s => [|[] m ih] [|x s] //=. - by case: ifP => [/mem_mask -> // | _ /andP [] _ /ih]. Qed. -Lemma count_maskP s1 s2 : (forall x, count_mem x s1 <= count_mem x s2) -> - exists2 m : bitseq, size m = size s2 & perm_eq s1 (mask m s2). +Lemma leq_count_mask P m s : count P (mask m s) <= count P s. Proof. -move=> s1_le; suff [m mP]: exists m, perm_eq s1 (mask m s2). +by elim: s m => [|x s IHs] [|[] m]//=; + rewrite ?leq_add2l (leq_trans (IHs _)) ?leq_addl. +Qed. + +Lemma leq_count_subseq P s1 s2 : subseq s1 s2 -> count P s1 <= count P s2. +Proof. by move=> /subseqP[m _ ->]; rewrite leq_count_mask. Qed. + +Lemma count_maskP s1 s2 : + (forall x, count_mem x s1 <= count_mem x s2) <-> + exists2 m : bitseq, size m = size s2 & perm_eq s1 (mask m s2). +Proof. +split=> [s1_le|[m _ /allP/(_ _ _)/eqP s1ms2 x]]; last first. + have [xs1|/count_memPn->//] := boolP (x \in s1). + by rewrite s1ms2 ?mem_cat ?xs1// leq_count_mask. +suff [m mP]: exists m, perm_eq s1 (mask m s2). by have [m' sm' eqm] := resize_mask m s2; exists m'; rewrite -?eqm. elim: s2 => [|x s2 IHs]//= in s1 s1_le *. by exists [::]; apply/allP => x _/=; rewrite eqn_leq s1_le. have [y|m s1s2] := IHs (rem x s1); first by rewrite count_mem_rem leq_subLR. -exists ((x \in s1) :: m); case: (boolP (x \in s1)). - by move/perm_to_rem/permPl->; rewrite perm_cons. -by rewrite -(permPr s1s2); move/rem_id->. +exists ((x \in s1) :: m); have [|/rem_id<-//] := boolP (x \in s1). +by move/perm_to_rem/permPl->; rewrite perm_cons. Qed. -Lemma count_subseqP s1 s2 : (forall x, count_mem x s1 <= count_mem x s2) -> - exists2 t, subseq t s2 & perm_eq s1 t. +Lemma count_subseqP s1 s2 : + (forall x, count_mem x s1 <= count_mem x s2) <-> + exists2 s, subseq s s2 & perm_eq s1 s. Proof. -by move=> /count_maskP[m]; exists (mask m s2); rewrite ?mask_subseq. +rewrite count_maskP; split=> [[m _]|[_/subseqP[m sm ->]]]; last by exists m. +by exists (mask m s2); rewrite ?mask_subseq. Qed. End MiscMask. @@ -2458,8 +2472,8 @@ Lemma subseq_rem x : {homo rem x : s1 s2 / @subseq T s1 s2}. Proof. move=> s1 s2; elim: s2 s1 => [|x2 s2 IHs2] [|x1 s1]; rewrite ?sub0seq //=. have [->|_] := eqVneq x1 x2; first by case: eqP => //= _ /IHs2; rewrite eqxx. -move/IHs2/subseq_trans=> -> //. -have [->|_] := eqVneq x x2; [apply: rem_subseq|apply: subseq_cons]. +move=> /IHs2/subseq_trans->//. +by have [->|_] := eqVneq x x2; [apply: rem_subseq|apply: subseq_cons]. Qed. End FilterSubseq. -- cgit v1.2.3 From e0d5c492d95b6833879a920430833fdaa2d7b621 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 11 Nov 2020 23:07:35 +0100 Subject: Apply suggestions from Kazuhiko Co-authored-by: Kazuhiko Sakaguchi --- CHANGELOG_UNRELEASED.md | 3 ++- mathcomp/ssreflect/seq.v | 43 +++++++++++++++++++++---------------------- 2 files changed, 23 insertions(+), 23 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 6d4985b..d7c3306 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -231,7 +231,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - in `seq.v`, added `drop_index`, `in_mask`, `cons_subseq`, `undup_subseq`, `leq_count_mask`, `leq_count_subseq`, `count_maskP`, `count_subseqP`, `count_rem`, `count_mem_rem`, - `rem_cons`, `remE`, `subseq_rem` and `leq_count_uniq`. + `rem_cons`, `remE`, `subseq_rem`, `leq_uniq_countP`, and + `leq_uniq_count`. - in `fintype.v`, added `mask_enum_ord`. - in `bigop.v`, added `big_mask_tuple` and `big_mask`. - in `mxalgebra.v`, new notation `stablemx V f` asserting that `f` diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 14a7c26..9747171 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -1271,13 +1271,17 @@ elim: s => //= y s IHs /andP[/negbTE s'y /IHs-> {IHs}]. by rewrite in_cons; case: (eqVneq y x) => // <-; rewrite s'y. Qed. -Lemma leq_uniq_count s1 s2 : uniq s1 -> {subset s1 <= s2} -> - (forall x, count_mem x s1 <= count_mem x s2). +Lemma leq_uniq_countP x s1 s2 : uniq s1 -> + reflect (x \in s1 -> x \in s2) (count_mem x s1 <= count_mem x s2). Proof. -move=> s1_uniq s1_s2 x; rewrite count_uniq_mem//. -by case: (boolP (_ \in _)) => // /s1_s2/count_memPn/eqP; rewrite -lt0n. +move/count_uniq_mem->; case: (boolP (_ \in _)) => //= _; last by constructor. +by rewrite -has_pred1 has_count; apply: (iffP idP) => //; apply. Qed. +Lemma leq_uniq_count s1 s2 : uniq s1 -> {subset s1 <= s2} -> + (forall x, count_mem x s1 <= count_mem x s2). +Proof. by move=> s1_uniq s1_s2 x; apply/leq_uniq_countP/s1_s2. Qed. + Lemma filter_pred1_uniq s x : uniq s -> x \in s -> filter (pred1 x) s = [:: x]. Proof. move=> uniq_s s_x; rewrite (all_pred1P _ _ (filter_all _ _)). @@ -1464,7 +1468,7 @@ Implicit Types x y z : T. Lemma rot_index s x (i := index x s) : x \in s -> rot i s = x :: (drop i.+1 s ++ take i s). -Proof. by move=> x_s; rewrite /rot drop_index ?cat_cons. Qed. +Proof. by move=> x_s; rewrite /rot drop_index. Qed. Variant rot_to_spec s x := RotToSpec i s' of rot i s = x :: s'. @@ -2218,9 +2222,7 @@ Lemma remE s : rem s = take (index x s) s ++ drop (index x s).+1 s. Proof. by elim: s => //= y s ->; case: eqVneq; rewrite ?drop0. Qed. Lemma rem_id s : x \notin s -> rem s = s. -Proof. -by move=> xNs; rewrite remE memNindex ?take_size ?drop_oversize ?cats0. -Qed. +Proof. by elim: s => //= y s IHs /norP[neq_yx /IHs->]; case: eqVneq neq_yx. Qed. Lemma perm_to_rem s : x \in s -> perm_eq s (x :: rem s). Proof. @@ -2257,15 +2259,14 @@ Proof. by move/mem_rem_uniq->; rewrite inE eqxx. Qed. Lemma count_rem P s : count P (rem s) = count P s - (x \in s) && P x. Proof. -have [xs|xNs]/= := boolP (x \in s); last by rewrite subn0 rem_id. -rewrite -[s in RHS](cat_take_drop (index x s)) drop_index// remE !count_cat/=. -by rewrite addnCA addKn. +have [/perm_to_rem/permP->|xNs]/= := boolP (x \in s); first by rewrite addKn. +by rewrite subn0 rem_id. Qed. Lemma count_mem_rem y s : count_mem y (rem s) = count_mem y s - (x == y). Proof. -rewrite count_rem/=; have [->|] := eqVneq y x; last by rewrite andbF subn0. -by have [|/count_memPn->] := boolP (x \in _). +rewrite count_rem; have []//= := boolP (x \in s). +by case: eqP => // <- /count_memPn->. Qed. End Rem. @@ -2375,6 +2376,12 @@ Proof. by elim: s => //= x s <-; case: (a x). Qed. Section MiscMask. +Lemma leq_count_mask T (P : {pred T}) m s : count P (mask m s) <= count P s. +Proof. +by elim: s m => [|x s IHs] [|[] m]//=; + rewrite ?leq_add2l (leq_trans (IHs _)) ?leq_addl. +Qed. + Variable (T : eqType). Implicit Types (s : seq T) (m : bitseq). @@ -2387,12 +2394,6 @@ elim: m s => [|[] m ih] [|x s] //=. - by case: ifP => [/mem_mask -> // | _ /andP [] _ /ih]. Qed. -Lemma leq_count_mask P m s : count P (mask m s) <= count P s. -Proof. -by elim: s m => [|x s IHs] [|[] m]//=; - rewrite ?leq_add2l (leq_trans (IHs _)) ?leq_addl. -Qed. - Lemma leq_count_subseq P s1 s2 : subseq s1 s2 -> count P s1 <= count P s2. Proof. by move=> /subseqP[m _ ->]; rewrite leq_count_mask. Qed. @@ -2400,9 +2401,7 @@ Lemma count_maskP s1 s2 : (forall x, count_mem x s1 <= count_mem x s2) <-> exists2 m : bitseq, size m = size s2 & perm_eq s1 (mask m s2). Proof. -split=> [s1_le|[m _ /allP/(_ _ _)/eqP s1ms2 x]]; last first. - have [xs1|/count_memPn->//] := boolP (x \in s1). - by rewrite s1ms2 ?mem_cat ?xs1// leq_count_mask. +split=> [s1_le|[m _ /permP s1ms2 x]]; last by rewrite s1ms2 leq_count_mask. suff [m mP]: exists m, perm_eq s1 (mask m s2). by have [m' sm' eqm] := resize_mask m s2; exists m'; rewrite -?eqm. elim: s2 => [|x s2 IHs]//= in s1 s1_le *. -- cgit v1.2.3