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 | 398 | ||||
| -rw-r--r-- | mathcomp/ssreflect/prime.v | 10 | ||||
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 289 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 8 |
7 files changed, 535 insertions, 203 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 0965b14..93521d7 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -137,55 +137,247 @@ Qed. Lemma rotr_cycle p : cycle (rotr n0 p) = cycle p. Proof. by rewrite -rot_cycle rotrK. Qed. +Definition sorted s := if s is x :: s' then path x s' else true. + +Lemma path_sorted x s : path x s -> sorted s. +Proof. by case: s => //= y s /andP[]. Qed. + +Lemma path_min_sorted x s : all (e x) s -> path x s = sorted s. +Proof. by case: s => //= y s /andP [->]. Qed. + End Path. -Lemma eq_path e e' : e =2 e' -> path e =2 path e'. -Proof. by move=> ee' x p; elim: p x => //= y p IHp x; rewrite ee' IHp. Qed. +Section SubPath_in. -Lemma eq_cycle e e' : e =2 e' -> cycle e =1 cycle e'. -Proof. by move=> ee' [|x p] //=; apply: eq_path. Qed. +Variable (P : {pred T}) (e e' : rel T). +Hypothesis (ee' : {in P &, subrel e e'}). -Lemma sub_path e e' : subrel e e' -> forall x p, path e x p -> path e' x p. -Proof. by move=> ee' x p; elim: p x => //= y p IHp x /andP[/ee'-> /IHp]. Qed. +Lemma sub_path_in x s : all P (x :: s) -> path e x s -> path e' x s. +Proof. +by elim: s x => //= y s ihs x /and3P [? ? ?] /andP [/ee' -> //]; apply/ihs/andP. +Qed. -Lemma rev_path e x p : - path e (last x p) (rev (belast x p)) = path (fun z => e^~ z) x p. +Lemma sub_cycle_in s : all P s -> cycle e s -> cycle e' s. Proof. -elim: p x => //= y p IHp x; rewrite rev_cons rcons_path -{}IHp andbC. -by rewrite -(last_cons x) -rev_rcons -lastI rev_cons last_rcons. +case: s => //= x s /andP [Px Ps]. +by apply: sub_path_in; rewrite /= all_rcons Px. +Qed. + +Lemma sub_sorted_in s : all P s -> sorted e s -> sorted e' s. +Proof. by case: s => //; apply: sub_path_in. Qed. + +End SubPath_in. + +Section EqPath_in. + +Variable (P : {pred T}) (e e' : rel T). +Hypothesis (ee' : {in P &, e =2 e'}). + +Let e_e' : {in P &, subrel e e'}. Proof. by move=> ? ? ? ?; rewrite ee'. Qed. +Let e'_e : {in P &, subrel e' e}. Proof. by move=> ? ? ? ?; rewrite ee'. Qed. + +Lemma eq_path_in x s : all P (x :: s) -> path e x s = path e' x s. +Proof. by move=> Pxs; apply/idP/idP; apply: sub_path_in Pxs. Qed. + +Lemma eq_cycle_in s : all P s -> cycle e s = cycle e' s. +Proof. by move=> Ps; apply/idP/idP; apply: sub_cycle_in Ps. Qed. + +End EqPath_in. + +Section SubPath. + +Variables e e' : rel T. + +Lemma sub_path : subrel e e' -> forall x p, path e x p -> path e' x p. +Proof. by move=> ? ? ?; apply/sub_path_in/all_predT; apply: in2W. Qed. + +Lemma sub_cycle : subrel e e' -> subpred (cycle e) (cycle e'). +Proof. by move=> ee' [] // ? ?; apply: sub_path. Qed. + +Lemma sub_sorted : subrel e e' -> subpred (sorted e) (sorted e'). +Proof. by move=> ee' [] //=; apply: sub_path. Qed. + +Lemma eq_path : e =2 e' -> path e =2 path e'. +Proof. by move=> ? ? ?; apply/eq_path_in/all_predT; apply: in2W. Qed. + +Lemma eq_cycle : e =2 e' -> cycle e =1 cycle e'. +Proof. by move=> ee' [] // ? ?; apply: eq_path. Qed. + +End SubPath. + +Section Transitive_in. + +Variables (P : {pred T}) (leT : rel T). +Hypothesis leT_tr : {in P & &, transitive leT}. + +Lemma path_mask_in x m s : + all P (x :: s) -> path leT x s -> path leT x (mask m s). +Proof. +elim: m s x => [|[] m ih] [|y s] x //=. + by case/and3P=> ? ? ? /andP [-> /ih ->] //; apply/andP. +case/andP=> Px Pys /andP [xy ys]; case/andP: (Pys) => Py Ps. +case: (mask _ _) (all_mask m Ps) (ih s y Pys ys) => //=. +by move=> z t /andP [Pz Pt] /andP [] /(leT_tr Py Px Pz xy) ->. Qed. +Lemma path_filter_in x a s : + all P (x :: s) -> path leT x s -> path leT x (filter a s). +Proof. by move=> Pxs; rewrite filter_mask; exact: path_mask_in. Qed. + +Lemma sorted_mask_in m s : all P s -> sorted leT s -> sorted leT (mask m s). +Proof. +elim: m s => [|[] m ih] [|x s] //= Pxs; first exact: path_mask_in. +by move/path_sorted/ih; apply; case/andP: Pxs. +Qed. + +Lemma sorted_filter_in a s : all P s -> sorted leT s -> sorted leT (filter a s). +Proof. rewrite filter_mask; exact: sorted_mask_in. Qed. + +End Transitive_in. + +Section Transitive. + +Variable (leT : rel T). +Hypothesis leT_tr : transitive leT. + +Let leT_tr' : {in predT & &, transitive leT}. Proof. exact: in3W. Qed. + +Lemma path_mask x m s : path leT x s -> path leT x (mask m s). +Proof. exact/path_mask_in/all_predT. Qed. + +Lemma path_filter x a s : path leT x s -> path leT x (filter a s). +Proof. by rewrite filter_mask; exact: path_mask. Qed. + +Lemma sorted_mask m s : sorted leT s -> sorted leT (mask m s). +Proof. exact/sorted_mask_in/all_predT. Qed. + +Lemma sorted_filter a s : sorted leT s -> sorted leT (filter a s). +Proof. rewrite filter_mask; exact: sorted_mask. Qed. + +End Transitive. + End Paths. +Arguments pathP {T e x p}. +Arguments path_sorted {T e x s}. +Arguments path_min_sorted {T e x s}. +Arguments path_mask_in {T P leT} leT_tr {x m s}. +Arguments path_filter_in {T P leT} leT_tr {x a s}. +Arguments sorted_mask_in {T P leT} leT_tr {m s}. +Arguments sorted_filter_in {T P leT} leT_tr {a s}. +Arguments path_mask {T leT} leT_tr {x} m {s}. +Arguments path_filter {T leT} leT_tr {x} a {s}. +Arguments sorted_mask {T leT} leT_tr m {s}. +Arguments sorted_filter {T leT} leT_tr a {s}. + Lemma cycle_catC (T : Type) (e : rel T) (p q : seq T) : cycle e (p ++ q) = cycle e (q ++ p). Proof. by rewrite -rot_size_cat rot_cycle. Qed. -Arguments pathP {T e x p}. +Section RevPath. + +Variables (T : Type) (e : rel T). + +Lemma rev_path x p : + path e (last x p) (rev (belast x p)) = path (fun z => e^~ z) x p. +Proof. +elim: p x => //= y p IHp x; rewrite rev_cons rcons_path -{}IHp andbC. +by rewrite -(last_cons x) -rev_rcons -lastI rev_cons last_rcons. +Qed. + +Lemma rev_cycle p : cycle e (rev p) = cycle (fun z => e^~ z) p. +Proof. +case: p => //= x p; rewrite -rev_path last_rcons belast_rcons rev_cons. +by rewrite -[in LHS]cats1 cycle_catC. +Qed. + +Lemma rev_sorted p : sorted e (rev p) = sorted (fun z => e^~ z) p. +Proof. by case: p => //= x p; rewrite -rev_path lastI rev_rcons. Qed. + +End RevPath. Section HomoPath. -Variables (T T' : Type) (f : T -> T') (leT : rel T) (leT' : rel T'). +Variables (T T' : Type) (P : {pred T}) (f : T -> T') (e : rel T) (e' : rel T'). -Lemma path_map x s : path leT' (f x) (map f s) = path (relpre f leT') x s. +Lemma path_map x s : path e' (f x) (map f s) = path (relpre f e') x s. Proof. by elim: s x => //= y s <-. Qed. -Lemma homo_path x s : {homo f : x y / leT x y >-> leT' x y} -> - path leT x s -> path leT' (f x) (map f s). -Proof. by move=> f_homo xs; rewrite path_map (sub_path _ xs). Qed. +Lemma cycle_map s : cycle e' (map f s) = cycle (relpre f e') s. +Proof. by case: s => //= ? ?; rewrite -map_rcons path_map. Qed. + +Lemma sorted_map s : sorted e' (map f s) = sorted (relpre f e') s. +Proof. by case: s; last apply: path_map. Qed. + +Lemma homo_path_in x s : {in P &, {homo f : x y / e x y >-> e' x y}} -> + all P (x :: s) -> path e x s -> path e' (f x) (map f s). +Proof. by move=> f_mono; rewrite path_map; apply: sub_path_in. Qed. + +Lemma homo_cycle_in s : {in P &, {homo f : x y / e x y >-> e' x y}} -> + all P s -> cycle e s -> cycle e' (map f s). +Proof. by move=> f_mono; rewrite cycle_map; apply: sub_cycle_in. Qed. + +Lemma homo_sorted_in s : {in P &, {homo f : x y / e x y >-> e' x y}} -> + all P s -> sorted e s -> sorted e' (map f s). +Proof. by move=> f_mono; rewrite sorted_map; apply: sub_sorted_in. Qed. + +Lemma mono_path_in x s : {in P &, {mono f : x y / e x y >-> e' x y}} -> + all P (x :: s) -> path e' (f x) (map f s) = path e x s. +Proof. by move=> f_mono; rewrite path_map; apply: eq_path_in. Qed. + +Lemma mono_cycle_in s : {in P &, {mono f : x y / e x y >-> e' x y}} -> + all P s -> cycle e' (map f s) = cycle e s. +Proof. by move=> f_mono; rewrite cycle_map; apply: eq_cycle_in. Qed. -Lemma mono_path x s : {mono f : x y / leT x y >-> leT' x y} -> - path leT' (f x) (map f s) = path leT x s. +Lemma mono_sorted_in s : {in P &, {mono f : x y / e x y >-> e' x y}} -> + all P s -> sorted e' (map f s) = sorted e s. +Proof. by case: s => // x s; apply: mono_path_in. Qed. + +Lemma homo_path x s : {homo f : x y / e x y >-> e' x y} -> + path e x s -> path e' (f x) (map f s). +Proof. by move=> f_homo; rewrite path_map; apply: sub_path. Qed. + +Lemma homo_cycle : {homo f : x y / e x y >-> e' x y} -> + {homo map f : s / cycle e s >-> cycle e' s}. +Proof. by move=> f_homo s hs; rewrite cycle_map (sub_cycle _ hs). Qed. + +Lemma homo_sorted : {homo f : x y / e x y >-> e' x y} -> + {homo map f : s / sorted e s >-> sorted e' s}. +Proof. by move/homo_path => ? []. Qed. + +Lemma mono_path x s : {mono f : x y / e x y >-> e' x y} -> + path e' (f x) (map f s) = path e x s. Proof. by move=> f_mon; rewrite path_map; apply: eq_path. Qed. +Lemma mono_cycle : {mono f : x y / e x y >-> e' x y} -> + {mono map f : s / cycle e s >-> cycle e' s}. +Proof. by move=> ? ?; rewrite cycle_map; apply: eq_cycle. Qed. + +Lemma mono_sorted : {mono f : x y / e x y >-> e' x y} -> + {mono map f : s / sorted e s >-> sorted e' s}. +Proof. by move=> f_mon [] //= x s; apply: mono_path. Qed. + End HomoPath. -Arguments homo_path {T T' f leT leT' x s}. -Arguments mono_path {T T' f leT leT' x s}. +Arguments path_map {T T' f e'}. +Arguments cycle_map {T T' f e'}. +Arguments sorted_map {T T' f e'}. +Arguments homo_path_in {T T' P f e e' x s}. +Arguments homo_cycle_in {T T' P f e e' s}. +Arguments homo_sorted_in {T T' P f e e' s}. +Arguments mono_path_in {T T' P f e e' x s}. +Arguments mono_cycle_in {T T' P f e e' s}. +Arguments mono_sorted_in {T T' P f e e' s}. +Arguments homo_path {T T' f e e' x s}. +Arguments homo_cycle {T T' f e e'}. +Arguments homo_sorted {T T' f e e'}. +Arguments mono_path {T T' f e e' x s}. +Arguments mono_cycle {T T' f e e'}. +Arguments mono_sorted {T T' f e e'}. Section EqPath. -Variables (n0 : nat) (T : eqType) (x0_cycle : T) (e : rel T). +Variables (n0 : nat) (T : eqType) (e : rel T). Implicit Type p : seq T. Variant split x : seq T -> seq T -> seq T -> Type := @@ -405,40 +597,15 @@ Qed. End EqPath. -Section EqHomoPath. - -Variables (T : eqType) (T' : Type) (f : T -> T') (leT : rel T) (leT' : rel T'). - -Lemma sub_path_in (e e' : rel T) x s : {in x :: s &, subrel e e'} -> - path e x s -> path e' x s. -Proof. -elim: s x => //= y s IHs x ee' /andP[/ee'->//=]; rewrite ?(eqxx,in_cons,orbT)//. -by apply: IHs => z t zys tys; apply: ee'; rewrite in_cons (zys, tys) orbT. -Qed. - -Lemma eq_path_in (e e' : rel T) x s : {in x :: s &, e =2 e'} -> - path e x s = path e' x s. -Proof. by move=> ee'; apply/idP/idP => /sub_path_in->// y z /ee' P/P->. Qed. - -Lemma homo_path_in x s : {in x :: s &, {homo f : x y / leT x y >-> leT' x y}} -> - path leT x s -> path leT' (f x) (map f s). -Proof. by move=> f_homo xs; rewrite path_map (sub_path_in _ xs). Qed. - -Lemma mono_path_in x s : {in x :: s &, {mono f : x y / leT x y >-> leT' x y}} -> - path leT' (f x) (map f s) = path leT x s. -Proof. by move=> f_mono; rewrite path_map; apply: eq_path_in. Qed. - -End EqHomoPath. - -Arguments homo_path_in {T T' f leT leT' x s}. -Arguments mono_path_in {T T' f leT leT' x s}. - (* Ordered paths and sorting. *) Section SortSeq. Variables (T : Type) (leT : rel T). +Local Notation path := (path leT). +Local Notation sorted := (sorted leT). + Fixpoint merge s1 := if s1 is x1 :: s1' then let fix merge_s1 s2 := @@ -482,15 +649,9 @@ rewrite /sort; move: [::] {2}_.+1 (ltnSn (size s)./2) => ss n. by elim: n => // n IHn in ss s *; case: s => [|x [|y s]] //= /IHn->. Qed. -Definition sorted s := if s is x :: s' then path leT x s' else true. - -Lemma path_sorted x s : path leT x s -> sorted s. -Proof. by case: s => //= y s /andP[]. Qed. - Hypothesis leT_total : total leT. -Lemma merge_path x s1 s2 : - path leT x s1 -> path leT x s2 -> path leT x (merge s1 s2). +Lemma merge_path x s1 s2 : path x s1 -> path x s2 -> path x (merge s1 s2). Proof. elim: s1 s2 x => //= x1 s1 IHs1. elim=> //= x2 s2 IHs2 x /andP[le_x_x1 ord_s1] /andP[le_x_x2 ord_s2]. @@ -517,9 +678,6 @@ elim: s [::] => /= [|x s ihs] ss allss. [rewrite /= ht | apply/ihss/merge_sorted]. Qed. -Lemma path_min_sorted x s : all (leT x) s -> path leT x s = sorted s. -Proof. by case: s => //= y s /andP [->]. Qed. - Lemma size_merge s1 s2 : size (merge s1 s2) = size (s1 ++ s2). Proof. rewrite size_cat; elim: s1 s2 => // x s1 IH1. @@ -527,7 +685,7 @@ elim=> //= [|y s2 IH2]; first by rewrite addn0. by case: leT; rewrite /= ?IH1 ?IH2 !addnS. Qed. -Lemma order_path_min x s : transitive leT -> path leT x s -> all (leT x) s. +Lemma order_path_min x s : transitive leT -> path x s -> all (leT x) s. Proof. move=> leT_tr; elim: s => //= y [//|z s] ihs /andP[xy yz]; rewrite xy {}ihs//. by move: yz => /= /andP [/(leT_tr _ _ _ xy) ->]. @@ -535,7 +693,7 @@ Qed. Hypothesis leT_tr : transitive leT. -Lemma path_sortedE x s : path leT x s = all (leT x) s && sorted s. +Lemma path_sortedE x s : path x s = all (leT x) s && sorted s. Proof. apply/idP/idP => [xs|/andP[/path_min_sorted<-//]]. by rewrite order_path_min//; apply: path_sorted xs. @@ -567,46 +725,25 @@ rewrite -{1 3}[s]/(catss [::] ++ s) sortE; elim: s [::] => /= [|x s ihs] ss. by elim: (catss ss) h_sorted => //= ? ? ih /path_sorted. Qed. -Lemma path_mask x m s : path leT x s -> path leT x (mask m s). -Proof. -elim: m s x => [|[] m ih] [|y s] x //=; first by case/andP=> -> /ih. -by case/andP => xy /ih; case: (mask _ _) => //= ? ? /andP [] /(leT_tr xy) ->. -Qed. - -Lemma path_filter x a s : path leT x s -> path leT x (filter a s). -Proof. by rewrite filter_mask; exact: path_mask. Qed. - -Lemma sorted_mask m s : sorted s -> sorted (mask m s). -Proof. -by elim: m s => [|[] m ih] [|x s] //=; [apply/path_mask | move/path_sorted/ih]. -Qed. - -Lemma sorted_filter a s : sorted s -> sorted (filter a s). -Proof. rewrite filter_mask; exact: sorted_mask. Qed. - End SortSeq. -Arguments path_sorted {T leT x s}. -Arguments order_path_min {T leT x s}. -Arguments path_min_sorted {T leT x s}. Arguments merge {T} relT !s1 !s2 : rename. +Arguments merge_path {T leT} leT_total {x s1 s2}. +Arguments merge_sorted {T leT} leT_total {s1 s2}. +Arguments sort_sorted {T leT} leT_total s. +Arguments order_path_min {T leT x s}. +Arguments path_sortedE {T leT} leT_tr x s. +Arguments sorted_merge {T leT} leT_tr {s t}. +Arguments sorted_sort {T leT} leT_tr {s}. Section SortMap. Variables (T T' : Type) (f : T' -> T). Section Monotonicity. -Variables (leT' : rel T') (leT : rel T). - -Lemma homo_sorted : {homo f : x y / leT' x y >-> leT x y} -> - {homo map f : s / sorted leT' s >-> sorted leT s}. -Proof. by move=> /homo_path f_path [|//= x s]. Qed. -Section Strict. +Variables (leT' : rel T') (leT : rel T). Hypothesis f_mono : {mono f : x y / leT' x y >-> leT x y}. -Lemma mono_sorted : {mono map f : s / sorted leT' s >-> sorted leT s}. -Proof. by case=> //= x s; rewrite (mono_path f_mono). Qed. - Lemma map_merge : {morph map f : s1 s2 / merge leT' s1 s2 >-> merge leT s1 s2}. Proof. elim=> //= x s1 IHs1; elim => [|y s2 IHs2] //=; rewrite f_mono. @@ -622,59 +759,39 @@ rewrite ihs -/(map f [:: x]); congr sort_rec1. by elim: ss [:: x] => {x s ihs} [|[|x s] ss ihss] //= ?; rewrite ihss map_merge. Qed. -End Strict. End Monotonicity. -Variable (leT : rel T). -Local Notation leTf := (relpre f leT). +Variable leT : rel T. -Lemma merge_map s1 s2 : merge leT (map f s1) (map f s2) = - map f (merge leTf s1 s2). +Lemma merge_map s1 s2 : + merge leT (map f s1) (map f s2) = map f (merge (relpre f leT) s1 s2). Proof. exact/esym/map_merge. Qed. -Lemma sort_map s : sort leT (map f s) = map f (sort leTf s). +Lemma sort_map s : sort leT (map f s) = map f (sort (relpre f leT) s). Proof. exact/esym/map_sort. Qed. -Lemma sorted_map s : sorted leT (map f s) = sorted leTf s. -Proof. exact: mono_sorted. Qed. - -Lemma sub_sorted (leT' : rel T) : - subrel leT leT' -> forall s, sorted leT s -> sorted leT' s. -Proof. by move=> leTT'; case => //; apply: sub_path. Qed. - End SortMap. -Arguments homo_sorted {T T' f leT' leT}. -Arguments mono_sorted {T T' f leT' leT}. Arguments map_merge {T T' f leT' leT}. Arguments map_sort {T T' f leT' leT}. Arguments merge_map {T T' f leT}. Arguments sort_map {T T' f leT}. -Arguments sorted_map {T T' f leT}. - -Lemma rev_sorted (T : Type) (leT : rel T) s : - sorted leT (rev s) = sorted (fun y x => leT x y) s. -Proof. by case: s => //= x p; rewrite -rev_path lastI rev_rcons. Qed. Section EqSortSeq. Variable T : eqType. Variable leT : rel T. -Lemma sub_sorted_in (leT' : rel T) (s : seq T) : - {in s &, subrel leT leT'} -> sorted leT s -> sorted leT' s. -Proof. by case: s => //; apply: sub_path_in. Qed. - +Local Notation path := (path leT). +Local Notation sorted := (sorted leT). Local Notation merge := (merge leT). Local Notation sort := (sort leT). -Local Notation sorted := (sorted leT). Section Transitive. Hypothesis leT_tr : transitive leT. -Lemma subseq_order_path x s1 s2 : - subseq s1 s2 -> path leT x s2 -> path leT x s1. +Lemma subseq_order_path x s1 s2 : subseq s1 s2 -> path x s2 -> path x s1. Proof. by case/subseqP => m _ ->; apply/path_mask. Qed. Lemma subseq_sorted s1 s2 : subseq s1 s2 -> sorted s2 -> sorted s1. @@ -687,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. @@ -702,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. @@ -750,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. @@ -771,23 +888,6 @@ case: s => [|x s] //; have [s1 pp qq] := perm_iota_sort leT x (x :: s). by rewrite qq size_map (perm_size pp) size_iota. Qed. -Section EqHomoSortSeq. - -Variables (T : eqType) (T' : Type) (f : T -> T') (leT : rel T) (leT' : rel T'). - -Lemma homo_sorted_in s : {in s &, {homo f : x y / leT x y >-> leT' x y}} -> - sorted leT s -> sorted leT' (map f s). -Proof. by case: s => //= x s /homo_path_in. Qed. - -Lemma mono_sorted_in s : {in s &, {mono f : x y / leT x y >-> leT' x y}} -> - sorted leT' (map f s) = sorted leT s. -Proof. by case: s => // x s /mono_path_in /= ->. Qed. - -End EqHomoSortSeq. - -Arguments homo_sorted_in {T T' f leT leT'}. -Arguments mono_sorted_in {T T' f leT leT'}. - Lemma ltn_sorted_uniq_leq s : sorted ltn s = uniq s && sorted leq s. Proof. case: s => //= n s; elim: s n => //= m s IHs n. @@ -905,7 +1005,8 @@ Lemma sort_stable s : Proof. move=> sorted_s; case Ds: s => // [x s1]; rewrite -{s1}Ds. rewrite -(mkseq_nth x s) sort_map. -apply/(homo_sorted_in (f := nth x s)): (sort_iota_stable x s (size s)). +move: (sort_iota_stable x s (size s)). +apply/(homo_sorted_in (f := nth x s) _ (allss _)). move=> /= y z; rewrite !mem_sort !mem_iota !leq0n add0n /= => y_le_s z_le_s. case/andP => -> /= /implyP yz; apply/implyP => /yz {yz} y_le_z. elim: s y z sorted_s y_le_z y_le_s z_le_s => // y s ih [|n] [|m] //=; @@ -937,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. @@ -1339,8 +1440,7 @@ Qed. Lemma ltn_index (s : seq T) : sorted r s -> {in s &, forall x y, index x s < index y s -> r x y}. Proof. -case: s => [//|x0 s'] r_sorted x y xs ys. -move=> /(@sorted_lt_nth x0 (x0 :: s')). +case: s => // x0 s' r_sorted x y xs ys /(@sorted_lt_nth x0 (x0 :: s')). by rewrite ?nth_index ?[_ \in gtn _]index_mem //; apply. Qed. @@ -1350,15 +1450,23 @@ Lemma sorted_le_nth x0 (s : seq T) : sorted r s -> {in [pred n | n < size s] &, {homo nth x0 s : i j / i <= j >-> r i j}}. Proof. move=> s_sorted x y xs ys. -by rewrite leq_eqVlt=> /orP[/eqP->//|/sorted_lt_nth]; apply. +by rewrite leq_eqVlt=> /predU1P[->//|]; apply: sorted_lt_nth. Qed. Lemma leq_index (s : seq T) : sorted r s -> {in s &, forall x y, index x s <= index y s -> r x y}. Proof. -case: s => [//|x0 s'] r_sorted x y xs ys. -move=> /(@sorted_le_nth x0 (x0 :: s')). +case: s => // x0 s' r_sorted x y xs ys /(@sorted_le_nth x0 (x0 :: s')). 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 1e9e1c9..9747171 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -1119,6 +1119,8 @@ Proof. by rewrite -all_predC; apply: allP. Qed. Lemma allPn a s : reflect (exists2 x, x \in s & ~~ a x) (~~ all a s). Proof. by rewrite -has_predC; apply: hasP. Qed. +Lemma allss s : all (mem s) s. Proof. exact/allP. Qed. + Lemma mem_filter a x s : (x \in filter a s) = a x && (x \in s). Proof. rewrite andbC; elim: s => //= y s IHs. @@ -1269,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 _ _)). @@ -1393,6 +1406,60 @@ 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 -> + 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. 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). +Proof. +by rewrite uniq_catC/= mem_cat => /andP[/norP[? ?] _]; rewrite eqseq_pivotl. +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//; case: eqVneq => /=. Qed. + End EqSeq. Section RotIndex. @@ -1401,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'. @@ -1472,7 +1537,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). @@ -1623,6 +1688,10 @@ Proof. by apply/permPl; rewrite -!catA perm_cat2l perm_catC. Qed. Lemma perm_catCA s1 s2 s3 : perm_eql (s1 ++ s2 ++ s3) (s2 ++ s1 ++ s3). Proof. by apply/permPl; rewrite !catA perm_cat2r perm_catC. Qed. +Lemma perm_catACA s1 s2 s3 s4 : + perm_eql ((s1 ++ s2) ++ (s3 ++ s4)) ((s1 ++ s3) ++ (s2 ++ s4)). +Proof. by apply/permPl; rewrite perm_catAC !catA perm_catAC. Qed. + Lemma perm_rcons x s : perm_eql (rcons s x) (x :: s). Proof. by move=> /= s2; rewrite -cats1 perm_catC. Qed. @@ -1920,14 +1989,24 @@ 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. + Lemma has_mask_cons a b m x s : has a (mask (b :: m) (x :: s)) = b && a x || has a (mask m s). 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. -elim: m s => [|b m IHm] [|x s] //; rewrite has_mask_cons /= andbC. -by case: (a x) => //= /IHm. +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 -> @@ -2102,6 +2181,27 @@ 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. +by case/subseqP => m size_m ->; rewrite rev_mask // mask_subseq. +Qed. + +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 : 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. +by rewrite (leq_trans (count_size _ _))// size_take; case: ltnP. +Qed. + End Subseq. Prenex Implicits subseq. @@ -2115,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. @@ -2154,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. @@ -2259,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. @@ -2269,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. @@ -2294,6 +2446,18 @@ 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 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. + 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 ->]. +by rewrite !filter_subseq. +Qed. + Lemma perm_to_subseq s1 s2 : subseq s1 s2 -> {s3 | perm_eq s2 (s1 ++ s3)}. Proof. @@ -2303,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. @@ -3063,16 +3224,45 @@ Lemma size_allpairs_dep f s t : size [seq f x y | x <- s, y <- t x] = sumn [seq size (t x) | x <- s]. Proof. by elim: s => //= x s IHs; rewrite size_cat size_map IHs. Qed. +Lemma allpairs0l f t : [seq f x y | x <- [::], y <- t x] = [::]. +Proof. by []. Qed. + +Lemma allpairs0r f s : [seq f x y | x <- s, y <- [::]] = [::]. +Proof. by elim: s. Qed. + +Lemma allpairs1l f x t : + [seq f x y | x <- [:: x], y <- t x] = [seq f x y | y <- t x]. +Proof. exact: cats0. Qed. + +Lemma allpairs1r f s y : + [seq f x y | x <- s, y <- [:: y x]] = [seq f x (y x) | x <- s]. +Proof. exact: flatten_map1. Qed. + +Lemma allpairs_cons f x s t : + [seq f x y | x <- x :: s, y <- t x] = + [seq f x y | y <- t x] ++ [seq f x y | x <- s, y <- t x]. +Proof. by []. Qed. + Lemma eq_allpairs (f1 f2 : forall x, T x -> R) s t : (forall x, f1 x =1 f2 x) -> [seq f1 x y | x <- s, y <- t x] = [seq f2 x y | x <- s, y <- t x]. -Proof. by move=> eq_f; rewrite (eq_map (fun x => eq_map (eq_f x) (t x))). Qed. +Proof. by move=> eq_f; rewrite (eq_map (fun x => eq_map (eq_f x) (t x))). Qed. + +Lemma eq_allpairsr (f : forall x, T x -> R) s t1 t2 : (forall x, t1 x = t2 x) -> + [seq f x y | x <- s, y <- t1 x] = [seq f x y | x <- s, y <- t2 x]. +(* From Coq 8.10 Proof. by move=> eq_t; under eq_map do rewrite eq_t. Qed. *) +Proof. by move=> eq_t; congr flatten; apply: eq_map => x; rewrite eq_t. Qed. Lemma allpairs_cat f s1 s2 t : [seq f x y | x <- s1 ++ s2, y <- t x] = [seq f x y | x <- s1, y <- t x] ++ [seq f x y | x <- s2, y <- t x]. Proof. by rewrite map_cat flatten_cat. Qed. +Lemma allpairs_rcons f x s t : + [seq f x y | x <- rcons s x, y <- t x] = + [seq f x y | x <- s, y <- t x] ++ [seq f x y | y <- t x]. +Proof. by rewrite -cats1 allpairs_cat allpairs1l. Qed. + Lemma allpairs_mapl f (g : S' -> S) s t : [seq f x y | x <- map g s, y <- t x] = [seq f (g x) y | x <- s, y <- t (g x)]. Proof. by rewrite -map_comp. Qed. @@ -3165,21 +3355,44 @@ Section MemAllPairs. Variables (S : Type) (T : S -> Type) (R : eqType). Implicit Types (f : forall x, T x -> R) (s : seq S). -Lemma allpairs_catr f s t1 t2 : - [seq f x y | x <- s, y <- t1 x ++ t2 x] =i - [seq f x y | x <- s, y <- t1 x] ++ [seq f x y | x <- s, y <- t2 x]. +Lemma perm_allpairs_catr f s t1 t2 : + perm_eql [seq f x y | x <- s, y <- t1 x ++ t2 x] + ([seq f x y | x <- s, y <- t1 x] ++ [seq f x y | x <- s, y <- t2 x]). +Proof. +apply/permPl; rewrite perm_sym; elim: s => //= x s ihs. +by rewrite perm_catACA perm_cat ?map_cat. +Qed. + +Lemma mem_allpairs_catr f s y0 t : + [seq f x y | x <- s, y <- y0 x ++ t x] =i + [seq f x y | x <- s, y <- y0 x] ++ [seq f x y | x <- s, y <- t x]. +Proof. exact/perm_mem/permPl/perm_allpairs_catr. Qed. + +Lemma perm_allpairs_consr f s y0 t : + perm_eql [seq f x y | x <- s, y <- y0 x :: t x] + ([seq f x (y0 x) | x <- s] ++ [seq f x y | x <- s, y <- t x]). Proof. -move=> z; rewrite mem_cat; elim: s => //= x s ih. -by rewrite map_cat !mem_cat ih !orbA; congr orb; rewrite orbAC. +by apply/permPl; rewrite (perm_allpairs_catr _ _ (fun=> [:: _])) allpairs1r. Qed. -Lemma allpairs_consr f s t1 t2 : - [seq f x y | x <- s, y <- t1 x :: t2 x] =i - [seq f x (t1 x) | x <- s] ++ [seq f x y | x <- s, y <- t2 x]. +Lemma mem_allpairs_consr f s t y0 : + [seq f x y | x <- s, y <- y0 x :: t x] =i + [seq f x (y0 x) | x <- s] ++ [seq f x y | x <- s, y <- t x]. +Proof. exact/perm_mem/permPl/perm_allpairs_consr. Qed. + +Lemma allpairs_rconsr f s y0 t : + perm_eql [seq f x y | x <- s, y <- rcons (t x) (y0 x)] + ([seq f x y | x <- s, y <- t x] ++ [seq f x (y0 x) | x <- s]). Proof. -by move=> z; rewrite (allpairs_catr f s (fun x => [:: t1 x])) /= flatten_map1. +apply/permPl; rewrite -(eq_allpairsr _ _ (fun=> cats1 _ _)). +by rewrite perm_allpairs_catr allpairs1r. Qed. +Lemma mem_allpairs_rconsr f s t y0 : + [seq f x y | x <- s, y <- rcons (t x) (y0 x)] =i + ([seq f x y | x <- s, y <- t x] ++ [seq f x (y0 x) | x <- s]). +Proof. exact/perm_mem/permPl/allpairs_rconsr. Qed. + End MemAllPairs. Lemma all_allpairsP @@ -3596,6 +3809,14 @@ Notation uniq_perm_eq := (deprecate uniq_perm_eq uniq_perm _ _ _) Notation perm_eq_iotaP := (deprecate perm_eq_iotaP perm_iotaP) (only parsing). Notation perm_undup_count := (deprecate perm_undup_count perm_count_undup _ _) (only parsing). - -Notation iota_add := (deprecate iota_add iotaD) (only parsing). +(* TODO: restore when Coq 8.10 is no longer supported *) +(* #[deprecated(since="mathcomp 1.13.0", note="Use iotaD instead.")] *) +Notation iota_add := iotaD (only parsing). Notation iota_addl := (deprecate iota_addl iotaDl) (only parsing). + +Notation allpairs_catr := + (deprecate allpairs_catr mem_allpairs_catr _ _ _) (only parsing). +Notation allpairs_consr := + (deprecate allpairs_consr mem_allpairs_consr _ _ _) (only parsing). +Notation perm_allpairs_rconsr := + (deprecate perm_allpairs_rconsr allpairs_rconsr _ _ _) (only parsing). diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index 568f8b0..0a2fbcd 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -2030,15 +2030,13 @@ Notation "@ 'decr_inj_in'" := (deprecate decr_inj_in decn_inj_in) (at level 10, only parsing) : fun_scope. Notation decr_inj_in := (@decr_inj_in _ _) (only parsing). +Notation "@ 'iter_add'" := + (deprecate iter_add iterD) (at level 10, only parsing) : fun_scope. Notation "@ 'odd_opp'" := (deprecate odd_opp oddN) (at level 10, only parsing) : fun_scope. Notation "@ 'sqrn_sub'" := (deprecate sqrn_sub sqrnB) (at level 10, only parsing) : fun_scope. - -(* TODO: restore when Coq 8.10 is no longer supported *) -(* #[deprecated(since="mathcomp 1.13.0", note="Use iterD instead.")] *) -Notation iter_add := iterD (only parsing). - +Notation iter_add := (@iterD _) (only parsing). Notation maxn_mulr := (deprecate maxn_mulr maxnMr) (only parsing). Notation maxn_mull := (deprecate maxn_mull maxnMl) (only parsing). Notation minn_mulr := (deprecate minn_mulr minnMr) (only parsing). |