diff options
Diffstat (limited to 'mathcomp/ssreflect')
| -rw-r--r-- | mathcomp/ssreflect/bigop.v | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/binomial.v | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/order.v | 29 | ||||
| -rw-r--r-- | mathcomp/ssreflect/path.v | 19 | ||||
| -rw-r--r-- | mathcomp/ssreflect/prime.v | 10 | ||||
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 99 |
6 files changed, 118 insertions, 43 deletions
diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index e8293ae..0ece733 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -990,7 +990,7 @@ Lemma big_nat_widen m n1 n2 (P : pred nat) F : = \big[op/idx]_(m <= i < n2 | P i && (i < n1)) F i. Proof. move=> len12; symmetry; rewrite -big_filter filter_predI big_filter. -have [ltn_trans eq_by_mem] := (ltn_trans, eq_sorted_irr ltn_trans ltnn). +have [ltn_trans eq_by_mem] := (ltn_trans, irr_sorted_eq ltn_trans ltnn). congr bigop; apply: eq_by_mem; rewrite ?sorted_filter ?iota_ltn_sorted // => i. rewrite mem_filter !mem_index_iota andbCA andbA andb_idr => // /andP[_]. by move/leq_trans->. diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v index 836c323..cd3ec87 100644 --- a/mathcomp/ssreflect/binomial.v +++ b/mathcomp/ssreflect/binomial.v @@ -468,7 +468,7 @@ have ft_m: #|f_t t| = m. rewrite cardsE (card_uniqP _) ?size_tuple // -(map_inj_uniq val_inj). exact: (sorted_uniq ltn_trans ltnn). rewrite ft_m eqxx -val_eqE val_fA // -(inj_eq (inj_map val_inj)) /=. -apply/eqP/(eq_sorted_irr ltn_trans ltnn) => // y. +apply/eqP/(irr_sorted_eq ltn_trans ltnn) => // y. by apply/mapP/mapP=> [] [x t_x ->]; exists x; rewrite // mem_enum inE in t_x *. Qed. diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v index da4d59d..1546a55 100644 --- a/mathcomp/ssreflect/order.v +++ b/mathcomp/ssreflect/order.v @@ -2741,7 +2741,7 @@ Proof. by rewrite andbC lt_le_asym. Qed. Definition lte_anti := (=^~ eq_le, lt_asym, lt_le_asym, le_lt_asym). -Lemma lt_sorted_uniq_le s : sorted lt s = uniq s && sorted le s. +Lemma lt_sorted_uniq_le s : sorted <%O s = uniq s && sorted <=%O s. Proof. case: s => //= n s; elim: s n => //= m s IHs n. rewrite inE lt_neqAle negb_or IHs -!andbA. @@ -2750,12 +2750,15 @@ rewrite andbF; apply/and5P=> [[ne_nm lenm _ _ le_ms]]; case/negP: ne_nm. by rewrite eq_le lenm /=; apply: (allP (order_path_min le_trans le_ms)). Qed. -Lemma eq_sorted_lt s1 s2 : sorted lt s1 -> sorted lt s2 -> s1 =i s2 -> s1 = s2. -Proof. by apply: eq_sorted_irr => //; apply: lt_trans. Qed. +Lemma lt_sorted_eq s1 s2 : sorted <%O s1 -> sorted <%O s2 -> s1 =i s2 -> s1 = s2. +Proof. by apply: irr_sorted_eq => //; apply: lt_trans. Qed. -Lemma eq_sorted_le s1 s2 : sorted le s1 -> sorted le s2 -> - perm_eq s1 s2 -> s1 = s2. -Proof. by apply: eq_sorted; [apply: le_trans|apply: le_anti]. Qed. +Lemma le_sorted_eq s1 s2 : + sorted <=%O s1 -> sorted <=%O s2 -> perm_eq s1 s2 -> s1 = s2. +Proof. exact/sorted_eq/le_anti/le_trans. Qed. + +Lemma sort_le_id s : sorted <=%O s -> sort <=%O s = s. +Proof. exact/sorted_sort/le_trans. Qed. Lemma comparable_leNgt x y : x >=< y -> (x <= y) = ~~ (y < x). Proof. @@ -3419,6 +3422,13 @@ Proof. exact: anti_mono_in. Qed. End POrderMonotonyTheory. +Notation "@ 'eq_sorted_lt'" := (deprecate eq_sorted_lt lt_sorted_eq) + (at level 10, only parsing) : fun_scope. +Notation "@ 'eq_sorted_le'" := (deprecate eq_sorted_le le_sorted_eq) + (at level 10, only parsing) : fun_scope. +Notation eq_sorted_lt := (@eq_sorted_lt _ _ _ _) (only parsing). +Notation eq_sorted_le := (@eq_sorted_le _ _ _ _) (only parsing). + End POrderTheory. Hint Resolve lexx le_refl ltxx lt_irreflexive ltW lt_eqF : core. @@ -3728,14 +3738,9 @@ Lemma sort_le_sorted s : sorted <=%O (sort <=%O s). Proof. exact: sort_sorted. Qed. Hint Resolve sort_le_sorted : core. -Lemma sort_lt_sorted s : sorted lt (sort le s) = uniq s. +Lemma sort_lt_sorted s : sorted <%O (sort <=%O s) = uniq s. Proof. by rewrite lt_sorted_uniq_le sort_uniq sort_le_sorted andbT. Qed. -Lemma sort_le_id s : sorted le s -> sort le s = s. -Proof. -by move=> ss; apply: eq_sorted_le; rewrite ?sort_le_sorted // perm_sort. -Qed. - Lemma leNgt x y : (x <= y) = ~~ (y < x). Proof. exact: comparable_leNgt. Qed. Lemma ltNge x y : (x < y) = ~~ (y <= x). Proof. exact: comparable_ltNge. Qed. diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index 1f675a6..93521d7 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -804,7 +804,7 @@ rewrite (IHs (path_sorted s_ord)) andbT; apply/negP=> s_x. by case/allPn: (order_path_min leT_tr s_ord); exists x; rewrite // leT_irr. Qed. -Lemma eq_sorted : antisymmetric leT -> +Lemma sorted_eq : antisymmetric leT -> forall s1 s2, sorted s1 -> sorted s2 -> perm_eq s1 s2 -> s1 = s2. Proof. move=> leT_asym; elim=> [|x1 s1 IHs1] s2 //= ord_s1 ord_s2 eq_s12. @@ -819,13 +819,13 @@ case/predU1P=> [eq_x12 | s1_x2]; first by case ne_x12. by rewrite (allP (order_path_min _ ord_s1)). Qed. -Lemma eq_sorted_irr : irreflexive leT -> +Lemma irr_sorted_eq : irreflexive leT -> forall s1 s2, sorted s1 -> sorted s2 -> s1 =i s2 -> s1 = s2. Proof. move=> leT_irr s1 s2 s1_sort s2_sort eq_s12. have: antisymmetric leT. by move=> m n /andP[? ltnm]; case/idP: (leT_irr m); apply: leT_tr ltnm. -by move/eq_sorted; apply=> //; apply: uniq_perm => //; apply: sorted_uniq. +by move/sorted_eq; apply=> //; apply: uniq_perm => //; apply: sorted_uniq. Qed. End Transitive. @@ -867,7 +867,7 @@ Lemma perm_sortP : Proof. move=> leT_total leT_tr leT_asym s1 s2. apply: (iffP idP) => eq12; last by rewrite -perm_sort eq12 perm_sort. -apply: eq_sorted; rewrite ?sort_sorted //. +apply: sorted_eq; rewrite ?sort_sorted //. by rewrite perm_sort (permPl eq12) -perm_sort. Qed. @@ -1038,7 +1038,7 @@ Lemma filter_sort p s : filter p (sort leT s) = sort leT (filter p s). Proof. case Ds: s => // [x s1]; rewrite -{s1}Ds. rewrite -(mkseq_nth x s) !(filter_map, sort_map). -congr map; apply/(@eq_sorted_irr _ (le_lex x s)) => //. +congr map; apply/(@irr_sorted_eq _ (le_lex x s)) => //. - by move=> ?; rewrite /= ltnn implybF andbN. - exact/sorted_filter/sort_stable/iota_ltn_sorted/ltn_trans. - exact/sort_stable/sorted_filter/iota_ltn_sorted/ltn_trans/ltn_trans. @@ -1461,3 +1461,12 @@ by rewrite ?nth_index ?[_ \in gtn _]index_mem //; apply. Qed. End Monotonicity. + +Notation "@ 'eq_sorted'" := + (deprecate eq_sorted sorted_eq) (at level 10, only parsing) : fun_scope. +Notation "@ 'eq_sorted_irr'" := (deprecate eq_sorted_irr irr_sorted_eq) + (at level 10, only parsing) : fun_scope. +Notation eq_sorted := + (fun le_tr le_asym => @eq_sorted _ _ le_tr le_asym _ _) (only parsing). +Notation eq_sorted_irr := + (fun le_tr le_irr => @eq_sorted_irr _ _ le_tr le_irr _ _) (only parsing). diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v index 8e94ef6..389b1c2 100644 --- a/mathcomp/ssreflect/prime.v +++ b/mathcomp/ssreflect/prime.v @@ -454,7 +454,7 @@ Qed. Lemma eq_primes m n : (primes m =i primes n) <-> (primes m = primes n). Proof. split=> [eqpr| -> //]. -by apply: (eq_sorted_irr ltn_trans ltnn); rewrite ?sorted_primes. +by apply: (irr_sorted_eq ltn_trans ltnn); rewrite ?sorted_primes. Qed. Lemma primes_uniq n : uniq (primes n). @@ -565,7 +565,7 @@ Qed. Lemma primes_prime p : prime p -> primes p = [::p]. Proof. -move=> pr_p; apply: (eq_sorted_irr ltn_trans ltnn) => // [|q]. +move=> pr_p; apply: (irr_sorted_eq ltn_trans ltnn) => // [|q]. exact: sorted_primes. rewrite mem_seq1 mem_primes prime_gt0 //=. by apply/andP/idP=> [[pr_q q_p] | /eqP-> //]; rewrite -dvdn_prime2. @@ -862,7 +862,7 @@ Proof. by move=> eq_pi n; rewrite 3!inE /= eq_pi. Qed. Lemma eq_piP m n : \pi(m) =i \pi(n) <-> \pi(m) = \pi(n). Proof. -rewrite /pi_of; have eqs := eq_sorted_irr ltn_trans ltnn. +rewrite /pi_of; have eqs := irr_sorted_eq ltn_trans ltnn. by split=> [|-> //] /(eqs _ _ (sorted_primes m) (sorted_primes n)) ->. Qed. @@ -954,7 +954,7 @@ Proof. by rewrite ltn_neqAle part_gt0 andbT eq_sym p_part_eq1 negbK. Qed. Lemma primes_part pi n : primes n`_pi = filter (mem pi) (primes n). Proof. have ltnT := ltn_trans; have [->|n_gt0] := posnP n; first by rewrite partn0. -apply: (eq_sorted_irr ltnT ltnn); rewrite ?(sorted_primes, sorted_filter) //. +apply: (irr_sorted_eq ltnT ltnn); rewrite ?(sorted_primes, sorted_filter) //. move=> p; rewrite mem_filter /= !mem_primes n_gt0 part_gt0 /=. apply/andP/and3P=> [[p_pr] | [pi_p p_pr dv_p_n]]. rewrite /partn; apply big_ind => [|n1 n2 IHn1 IHn2|q pi_q]. @@ -970,7 +970,7 @@ Qed. Lemma filter_pi_of n m : n < m -> filter \pi(n) (index_iota 0 m) = primes n. Proof. -move=> lt_n_m; have ltnT := ltn_trans; apply: (eq_sorted_irr ltnT ltnn). +move=> lt_n_m; have ltnT := ltn_trans; apply: (irr_sorted_eq ltnT ltnn). - by rewrite sorted_filter // iota_ltn_sorted. - exact: sorted_primes. move=> p; rewrite mem_filter mem_index_iota /= mem_primes; case: and3P => //. diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index bb462a3..9747171 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -1271,6 +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_countP x s1 s2 : uniq s1 -> + reflect (x \in s1 -> x \in s2) (count_mem x s1 <= count_mem x s2). +Proof. +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 _ _)). @@ -1395,6 +1406,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 +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_nth x) ?index_mem ?nth_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'. @@ -2203,16 +2215,19 @@ 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). -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. -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 +2257,18 @@ 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 [/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 []//= := boolP (x \in s). +by case: eqP => // <- /count_memPn->. +Qed. + End Rem. Section Map. @@ -2347,8 +2374,18 @@ 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. + +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). + +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 +2394,33 @@ elim: m s => [|[] m ih] [|x s] //=. - by case: ifP => [/mem_mask -> // | _ /andP [] _ /ih]. 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 _ /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 *. + 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); 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 s, subseq s s2 & perm_eq s1 s. +Proof. +rewrite count_maskP; split=> [[m _]|[_/subseqP[m sm ->]]]; last by exists m. +by exists (mask m s2); rewrite ?mask_subseq. +Qed. + +End MiscMask. + Section FilterSubseq. Variable T : eqType. @@ -2403,15 +2467,12 @@ 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 x : {homo rem x : s1 s2 / @subseq T s1 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). +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->//. +by have [->|_] := eqVneq x x2; [apply: rem_subseq|apply: subseq_cons]. Qed. End FilterSubseq. |