From a18a03452a84e1f54716ce20accca4e16715e382 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Thu, 19 Nov 2020 18:12:26 +0900 Subject: Add `_in` lemmas for `sort` --- mathcomp/ssreflect/path.v | 100 ++++++++++++++++++++++++++++++++++++++++++++++ mathcomp/ssreflect/seq.v | 6 +++ 2 files changed, 106 insertions(+) (limited to 'mathcomp') diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index fa66807..2d2182b 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -879,6 +879,31 @@ Arguments map_sort {T T' f leT' leT}. Arguments merge_map {T T' f leT}. Arguments sort_map {T T' f leT}. +Section SortSeq_in. + +Variables (T : Type) (P : {pred T}) (leT : rel T). + +Hypothesis leT_total : {in P &, total leT}. + +Lemma sort_sorted_in s : all P s -> sorted leT (sort leT s). +Proof. +move=> /all_sigP [{}s <-]; rewrite sort_map sorted_map. +by apply: sort_sorted; move=> [x Px] [y Py]; apply: leT_total. +Qed. + +Hypothesis leT_tr : {in P & &, transitive leT}. + +Lemma sorted_sort_in s : all P s -> sorted leT s -> sort leT s = s. +Proof. +move=> /all_sigP [{}s <-]; rewrite sort_map sorted_map. +by move=> /sorted_sort -> // [x Px] [y Py] [z Pz]; apply: leT_tr. +Qed. + +End SortSeq_in. + +Arguments sort_sorted_in {T P leT} leT_total {s}. +Arguments sorted_sort_in {T P leT} leT_tr {s}. + Section EqSortSeq. Variables (T : eqType) (leT : rel T). @@ -1069,6 +1094,26 @@ apply/(@irr_sorted_eq _ lt_lex); rewrite /lt_lex /leN //=. - by move=> ?; rewrite !(mem_filter, mem_sort). Qed. +Lemma sort_stable_in T (P : {pred T}) (leT leT' : rel T) : + {in P &, total leT} -> {in P & &, transitive leT'} -> + forall s : seq T, all P s -> sorted leT' s -> + sorted [rel x y | leT x y && (leT y x ==> leT' x y)] (sort leT s). +Proof. +move=> leT_total leT_tr _ /all_sigP [s <-]; rewrite sort_map !sorted_map. +apply: sort_stable; first by move=> [x Px] [y Py]; apply: leT_total. +by move=> [x Px] [y Py] [z Pz]; apply: leT_tr. +Qed. + +Lemma filter_sort_in T (P : {pred T}) (leT : rel T) : + {in P &, total leT} -> {in P & &, transitive leT} -> + forall p s, all P s -> filter p (sort leT s) = sort leT (filter p s). +Proof. +move=> leT_total leT_tr p _ /all_sigP [s <-]. +rewrite !(sort_map, filter_map) filter_sort //. + by move=> [x Px] [y Py]; apply: leT_total. +by move=> [x Px] [y Py] [z Pz]; apply: leT_tr. +Qed. + Section Stability_mask. Variables (T : Type) (leT : rel T). @@ -1091,6 +1136,30 @@ Proof. by move/(sorted_sort leT_tr) <-; exact: mask_sort. Qed. End Stability_mask. +Section Stability_mask_in. + +Variables (T : Type) (P : {pred T}) (leT : rel T). +Hypothesis leT_total : {in P &, total leT}. +Hypothesis leT_tr : {in P & &, transitive leT}. + +Lemma mask_sort_in s m : + all P s -> {m_s : bitseq | mask m_s (sort leT s) = sort leT (mask m s)}. +Proof. +move=> /all_sigP [{}s <-]; case: (mask_sort (leT := relpre sval leT) _ _ s m). +- by move=> [x Px] [y Py]; apply: leT_total. +- by move=> [x Px] [y Py] [z Pz]; apply: leT_tr. +- by move=> m' m'E; exists m'; rewrite -map_mask !sort_map -map_mask m'E. +Qed. + +Lemma sorted_mask_sort_in s m : + all P s -> sorted leT (mask m s) -> {m_s | mask m_s (sort leT s) = mask m s}. +Proof. +move=> ? /(sorted_sort_in leT_tr _) <-; last exact: all_mask. +exact: mask_sort_in. +Qed. + +End Stability_mask_in. + Section Stability_subseq. Variables (T : eqType) (leT : rel T). @@ -1114,6 +1183,37 @@ Qed. End Stability_subseq. +Section Stability_subseq_in. + +Variables (T : eqType) (leT : rel T). + +Lemma subseq_sort_in t s : + {in s &, total leT} -> {in s & &, transitive leT} -> + subseq t s -> subseq (sort leT t) (sort leT s). +Proof. +move=> leT_total leT_tr /subseqP [m _ ->]. +have [m' <-] := mask_sort_in leT_total leT_tr m (allss _). +exact: mask_subseq. +Qed. + +Lemma sorted_subseq_sort_in t s : + {in s &, total leT} -> {in s & &, transitive leT} -> + subseq t s -> sorted leT t -> subseq t (sort leT s). +Proof. +move=> ? leT_tr ? /(sorted_sort_in leT_tr) <-; last exact/allP/mem_subseq. +exact: subseq_sort_in. +Qed. + +Lemma mem2_sort_in s : + {in s &, total leT} -> {in s & &, transitive leT} -> + forall x y, leT x y -> mem2 s x y -> mem2 (sort leT s) x y. +Proof. +move=> leT_total leT_tr x y lexy; rewrite !mem2E. +by move/subseq_sort_in; case: (_ == _); rewrite /sort /= ?lexy; apply. +Qed. + +End Stability_subseq_in. + (* Function trajectories. *) Notation fpath f := (path (coerced_frel f)). diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index a0a0548..fab3fa9 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -2385,6 +2385,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 all_sigP T a (s : seq T) : all a s -> {s' : seq (sig a) | map sval s' = s}. +Proof. +elim: s => /= [_|x s ihs /andP [ax /ihs [s' <-]]]; first by exists [::]. +by exists (exist a x ax :: s'). +Qed. + Section MiscMask. Lemma leq_count_mask T (P : {pred T}) m s : count P (mask m s) <= count P s. -- cgit v1.2.3 From a0f3506f41b038d8a9935afa1e587b1ac10f7fe4 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Thu, 19 Nov 2020 18:03:36 +0100 Subject: factoring out in_sig --- mathcomp/ssreflect/path.v | 35 ++++++++++++++++------------------- mathcomp/ssreflect/seq.v | 4 ++-- mathcomp/ssreflect/ssrbool.v | 42 ++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 60 insertions(+), 21 deletions(-) (limited to 'mathcomp') diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index 2d2182b..f4ecfbb 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -882,21 +882,20 @@ Arguments sort_map {T T' f leT}. Section SortSeq_in. Variables (T : Type) (P : {pred T}) (leT : rel T). +Notation le_sT := (relpre (val : sig P -> _) leT). Hypothesis leT_total : {in P &, total leT}. +Let le_sT_total : total le_sT := in2_sig leT_total. Lemma sort_sorted_in s : all P s -> sorted leT (sort leT s). -Proof. -move=> /all_sigP [{}s <-]; rewrite sort_map sorted_map. -by apply: sort_sorted; move=> [x Px] [y Py]; apply: leT_total. -Qed. +Proof. by move=> /all_sigP[? ->]; rewrite sort_map sorted_map sort_sorted. Qed. Hypothesis leT_tr : {in P & &, transitive leT}. +Let le_sT_tr : transitive le_sT := in3_sig leT_tr. Lemma sorted_sort_in s : all P s -> sorted leT s -> sort leT s = s. Proof. -move=> /all_sigP [{}s <-]; rewrite sort_map sorted_map. -by move=> /sorted_sort -> // [x Px] [y Py] [z Pz]; apply: leT_tr. +by move=> /all_sigP [{}s ->]; rewrite sort_map sorted_map => /sorted_sort->. Qed. End SortSeq_in. @@ -1099,19 +1098,16 @@ Lemma sort_stable_in T (P : {pred T}) (leT leT' : rel T) : forall s : seq T, all P s -> sorted leT' s -> sorted [rel x y | leT x y && (leT y x ==> leT' x y)] (sort leT s). Proof. -move=> leT_total leT_tr _ /all_sigP [s <-]; rewrite sort_map !sorted_map. -apply: sort_stable; first by move=> [x Px] [y Py]; apply: leT_total. -by move=> [x Px] [y Py] [z Pz]; apply: leT_tr. +move=> /in2_sig leT_total /in3_sig leT_tr _ /all_sigP[s ->]. +by rewrite sort_map !sorted_map; apply: sort_stable. Qed. Lemma filter_sort_in T (P : {pred T}) (leT : rel T) : {in P &, total leT} -> {in P & &, transitive leT} -> forall p s, all P s -> filter p (sort leT s) = sort leT (filter p s). Proof. -move=> leT_total leT_tr p _ /all_sigP [s <-]. -rewrite !(sort_map, filter_map) filter_sort //. - by move=> [x Px] [y Py]; apply: leT_total. -by move=> [x Px] [y Py] [z Pz]; apply: leT_tr. +move=> /in2_sig leT_total /in3_sig leT_tr p _ /all_sigP[s ->]. +by rewrite !(sort_map, filter_map) filter_sort. Qed. Section Stability_mask. @@ -1142,20 +1138,21 @@ Variables (T : Type) (P : {pred T}) (leT : rel T). Hypothesis leT_total : {in P &, total leT}. Hypothesis leT_tr : {in P & &, transitive leT}. +Notation le_sT := (relpre (val : sig P -> _) leT). +Let le_sT_total : total le_sT := in2_sig leT_total. +Let le_sT_tr : transitive le_sT := in3_sig leT_tr. + Lemma mask_sort_in s m : all P s -> {m_s : bitseq | mask m_s (sort leT s) = sort leT (mask m s)}. Proof. -move=> /all_sigP [{}s <-]; case: (mask_sort (leT := relpre sval leT) _ _ s m). -- by move=> [x Px] [y Py]; apply: leT_total. -- by move=> [x Px] [y Py] [z Pz]; apply: leT_tr. -- by move=> m' m'E; exists m'; rewrite -map_mask !sort_map -map_mask m'E. +move=> /all_sigP [{}s ->]; case: (mask_sort (leT := le_sT) _ _ s m) => //. +by move=> m' m'E; exists m'; rewrite -map_mask !sort_map -map_mask m'E. Qed. Lemma sorted_mask_sort_in s m : all P s -> sorted leT (mask m s) -> {m_s | mask m_s (sort leT s) = mask m s}. Proof. -move=> ? /(sorted_sort_in leT_tr _) <-; last exact: all_mask. -exact: mask_sort_in. +move=> ? /(sorted_sort_in leT_tr _) <-; [exact: mask_sort_in | exact: all_mask]. Qed. End Stability_mask_in. diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index fab3fa9..999ec0a 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -2385,9 +2385,9 @@ 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 all_sigP T a (s : seq T) : all a s -> {s' : seq (sig a) | map sval s' = s}. +Lemma all_sigP T a (s : seq T) : all a s -> {s' : seq (sig a) | s = map sval s'}. Proof. -elim: s => /= [_|x s ihs /andP [ax /ihs [s' <-]]]; first by exists [::]. +elim: s => /= [_|x s ihs /andP [ax /ihs [s' ->]]]; first by exists [::]. by exists (exist a x ax :: s'). Qed. diff --git a/mathcomp/ssreflect/ssrbool.v b/mathcomp/ssreflect/ssrbool.v index 48f0262..1864b53 100644 --- a/mathcomp/ssreflect/ssrbool.v +++ b/mathcomp/ssreflect/ssrbool.v @@ -349,3 +349,45 @@ Proof. by case: b => // /(_ isT). Qed. Lemma contra_notF P b : (b -> P) -> ~ P -> b = false. Proof. by case: b => // /(_ isT). Qed. End Contra. + +(******************) +(* v8.14 addtions *) +(******************) + +Section in_sig. +Local Notation "{ 'all1' P }" := (forall x, P x : Prop) (at level 0). +Local Notation "{ 'all2' P }" := (forall x y, P x y : Prop) (at level 0). +Local Notation "{ 'all3' P }" := (forall x y z, P x y z : Prop) (at level 0). + +Variables T1 T2 T3 : Type. +Variables (D1 : {pred T1}) (D2 : {pred T2}) (D3 : {pred T3}). +Variable P1 : T1 -> Prop. +Variable P11 : T1 -> T2 -> Prop. +Variable P111 : T1 -> T2 -> T3 -> Prop. +Variable P2 : T1 -> T1 -> Prop. +Variable P3 : T1 -> T1 -> T1 -> Prop. + +Lemma in1_sig : {in D1, {all1 P1}} -> forall x : sig D1, P1 (sval x). +Proof. by move=> DP [x Dx]; have := DP _ Dx. Qed. + +Lemma in11_sig : {in D1 & D2, {all2 P11}} -> + forall (x : sig D1) (y : sig D2), P11 (sval x) (sval y). +Proof. by move=> DP [x Dx] [y Dy]; have := DP _ _ Dx Dy. Qed. + +Lemma in111_sig : {in D1 & D2 & D3, {all3 P111}} -> + forall (x : sig D1) (y : sig D2) (z : sig D3), P111 (sval x) (sval y) (sval z). +Proof. by move=> DP [x Dx] [y Dy] [z Dz]; have := DP _ _ _ Dx Dy Dz. Qed. + +Lemma in2_sig : {in D1 &, {all2 P2}} -> forall x y : sig D1, P2 (sval x) (sval y). +Proof. by move=> DP [x Dx] [y Dy]; have := DP _ _ Dx Dy. Qed. + +Lemma in3_sig : {in D1 & &, {all3 P3}} -> + forall x y z : sig D1, P3 (sval x) (sval y) (sval z). +Proof. by move=> DP [x Dx] [y Dy] [z Dz]; have := DP _ _ _ Dx Dy Dz. Qed. + +End in_sig. +Arguments in1_sig {T1 D1 P1}. +Arguments in11_sig {T1 T2 D1 D2 P11}. +Arguments in111_sig {T1 T2 T3 D1 D2 D3 P111}. +Arguments in2_sig {T1 D1 P2}. +Arguments in3_sig {T1 D1 P3}. -- cgit v1.2.3 From c42c0678c5de1db9f3e747a7e3b553242719d82c Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Fri, 20 Nov 2020 11:19:29 +0900 Subject: `in11(1)_sig` subsumes `in(2|3)_sig` --- mathcomp/ssreflect/path.v | 4 ++-- mathcomp/ssreflect/ssrbool.v | 35 ++++++++++++++++------------------- 2 files changed, 18 insertions(+), 21 deletions(-) (limited to 'mathcomp') diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index f4ecfbb..d99dedf 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -882,7 +882,7 @@ Arguments sort_map {T T' f leT}. Section SortSeq_in. Variables (T : Type) (P : {pred T}) (leT : rel T). -Notation le_sT := (relpre (val : sig P -> _) leT). +Let le_sT := relpre (val : sig P -> _) leT. Hypothesis leT_total : {in P &, total leT}. Let le_sT_total : total le_sT := in2_sig leT_total. @@ -1138,7 +1138,7 @@ Variables (T : Type) (P : {pred T}) (leT : rel T). Hypothesis leT_total : {in P &, total leT}. Hypothesis leT_tr : {in P & &, transitive leT}. -Notation le_sT := (relpre (val : sig P -> _) leT). +Let le_sT := relpre (val : sig P -> _) leT. Let le_sT_total : total le_sT := in2_sig leT_total. Let le_sT_tr : transitive le_sT := in3_sig leT_tr. diff --git a/mathcomp/ssreflect/ssrbool.v b/mathcomp/ssreflect/ssrbool.v index 1864b53..49be7b0 100644 --- a/mathcomp/ssreflect/ssrbool.v +++ b/mathcomp/ssreflect/ssrbool.v @@ -102,6 +102,10 @@ Arguments mono_sym_in {aT rT} [aR rR f aD]. Arguments homo_sym_in11 {aT rT} [aR rR f aD aD']. Arguments mono_sym_in11 {aT rT} [aR rR f aD aD']. +(******************) +(* v8.14 addtions *) +(******************) + Section LocalGlobal. Local Notation "{ 'all1' P }" := (forall x, P x : Prop) (at level 0). @@ -209,6 +213,10 @@ Arguments in_on1S {T1 T2} D2 {f Q1}. Arguments in_on1lS {T1 T2 T3} D2 {f h Q1l}. Arguments in_on2S {T1 T2} D2 {f Q2}. +(******************) +(* v8.13 addtions *) +(******************) + Section CancelOn. Variables (aT rT : predArgType) (aD : {pred aT}) (rD : {pred rT}). @@ -362,32 +370,21 @@ Local Notation "{ 'all3' P }" := (forall x y z, P x y z : Prop) (at level 0). Variables T1 T2 T3 : Type. Variables (D1 : {pred T1}) (D2 : {pred T2}) (D3 : {pred T3}). Variable P1 : T1 -> Prop. -Variable P11 : T1 -> T2 -> Prop. -Variable P111 : T1 -> T2 -> T3 -> Prop. -Variable P2 : T1 -> T1 -> Prop. -Variable P3 : T1 -> T1 -> T1 -> Prop. +Variable P2 : T1 -> T2 -> Prop. +Variable P3 : T1 -> T2 -> T3 -> Prop. Lemma in1_sig : {in D1, {all1 P1}} -> forall x : sig D1, P1 (sval x). Proof. by move=> DP [x Dx]; have := DP _ Dx. Qed. -Lemma in11_sig : {in D1 & D2, {all2 P11}} -> - forall (x : sig D1) (y : sig D2), P11 (sval x) (sval y). -Proof. by move=> DP [x Dx] [y Dy]; have := DP _ _ Dx Dy. Qed. - -Lemma in111_sig : {in D1 & D2 & D3, {all3 P111}} -> - forall (x : sig D1) (y : sig D2) (z : sig D3), P111 (sval x) (sval y) (sval z). -Proof. by move=> DP [x Dx] [y Dy] [z Dz]; have := DP _ _ _ Dx Dy Dz. Qed. - -Lemma in2_sig : {in D1 &, {all2 P2}} -> forall x y : sig D1, P2 (sval x) (sval y). +Lemma in2_sig : {in D1 & D2, {all2 P2}} -> + forall (x : sig D1) (y : sig D2), P2 (sval x) (sval y). Proof. by move=> DP [x Dx] [y Dy]; have := DP _ _ Dx Dy. Qed. -Lemma in3_sig : {in D1 & &, {all3 P3}} -> - forall x y z : sig D1, P3 (sval x) (sval y) (sval z). +Lemma in3_sig : {in D1 & D2 & D3, {all3 P3}} -> + forall (x : sig D1) (y : sig D2) (z : sig D3), P3 (sval x) (sval y) (sval z). Proof. by move=> DP [x Dx] [y Dy] [z Dz]; have := DP _ _ _ Dx Dy Dz. Qed. End in_sig. Arguments in1_sig {T1 D1 P1}. -Arguments in11_sig {T1 T2 D1 D2 P11}. -Arguments in111_sig {T1 T2 T3 D1 D2 D3 P111}. -Arguments in2_sig {T1 D1 P2}. -Arguments in3_sig {T1 D1 P3}. +Arguments in2_sig {T1 T2 D1 D2 P2}. +Arguments in3_sig {T1 T2 T3 D1 D2 D3 P3}. -- cgit v1.2.3 From 95cbf3b00c2d3709b2db9cff16c321012ff4fe62 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Sun, 22 Nov 2020 18:15:03 +0900 Subject: Add more `_in` lemmas and CHANGELOG entries --- mathcomp/ssreflect/path.v | 153 +++++++++++++++++++++++++++++++++++++++------- mathcomp/ssreflect/seq.v | 10 +++ 2 files changed, 142 insertions(+), 21 deletions(-) (limited to 'mathcomp') diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index d99dedf..df71460 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -208,6 +208,15 @@ End SubPath. Section Transitive_in. Variables (P : {pred T}) (leT : rel T). + +Lemma order_path_min_in x s : + {in P & &, transitive leT} -> all P (x :: s) -> path leT x s -> all (leT x) s. +Proof. +move=> leT_tr; elim: s => //= y s ihs /and3P [Px Py Ps] /andP [xy ys]. +rewrite xy {}ihs ?Px //=; case: s Ps ys => //= z s /andP [Pz Ps] /andP [yz ->]. +by rewrite (leT_tr _ _ _ Py Px Pz). +Qed. + Hypothesis leT_tr : {in P & &, transitive leT}. Lemma path_mask_in x m s : @@ -233,6 +242,31 @@ 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. +Lemma path_sorted_inE x s : + all P (x :: s) -> path leT x s = all (leT x) s && sorted leT s. +Proof. +move=> Pxs; apply/idP/idP => [xs|/andP[/path_min_sorted<-//]]. +by rewrite (order_path_min_in leT_tr) //; apply: path_sorted xs. +Qed. + +Lemma sorted_ltn_nth_in x0 s : all P s -> sorted leT s -> + {in [pred n | n < size s] &, {homo nth x0 s : i j / i < j >-> leT i j}}. +Proof. +elim: s => // x s ihs Pxs path_xs [|i] [|j] //=; rewrite -!topredE /= !ltnS. +- by move=> _ js _; apply/all_nthP/js/order_path_min_in. +- by apply/ihs/path_sorted/path_xs; case/andP: Pxs. +Qed. + +Hypothesis leT_refl : {in P, reflexive leT}. + +Lemma sorted_leq_nth_in x0 s : all P s -> sorted leT s -> + {in [pred n | n < size s] &, {homo nth x0 s : i j / i <= j >-> leT i j}}. +Proof. +move=> Ps s_sorted x y xs ys; rewrite leq_eqVlt=> /predU1P[->|]. + exact/leT_refl/all_nthP. +exact: sorted_ltn_nth_in. +Qed. + End Transitive_in. Section Transitive. @@ -241,8 +275,7 @@ Variable (leT : rel T). Lemma order_path_min x s : transitive leT -> path leT 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) ->]. +by move=> leT_tr; apply/order_path_min_in/all_predT => //; apply: in3W. Qed. Hypothesis leT_tr : transitive leT. @@ -262,27 +295,17 @@ Lemma sorted_filter a s : sorted leT s -> sorted leT (filter a s). Proof. exact/sorted_filter_in/all_predT. Qed. Lemma path_sortedE x s : path leT x s = all (leT x) s && sorted leT s. -Proof. -apply/idP/idP => [xs|/andP[/path_min_sorted<-//]]. -by rewrite order_path_min//; apply: path_sorted xs. -Qed. +Proof. exact/path_sorted_inE/all_predT. Qed. Lemma sorted_ltn_nth x0 s : sorted leT s -> {in [pred n | n < size s] &, {homo nth x0 s : i j / i < j >-> leT i j}}. -Proof. -elim: s => //= x s ihs path_xs [|i] [|j] //=; rewrite -!topredE /= !ltnS. -- by move=> _ js _; apply/all_nthP/js/order_path_min. -- exact/ihs/path_sorted/path_xs. -Qed. +Proof. exact/sorted_ltn_nth_in/all_predT. Qed. Hypothesis leT_refl : reflexive leT. Lemma sorted_leq_nth x0 s : sorted leT s -> {in [pred n | n < size s] &, {homo nth x0 s : i j / i <= j >-> leT i j}}. -Proof. -move=> s_sorted x y xs ys. -by rewrite leq_eqVlt=> /predU1P[->//|]; apply: sorted_ltn_nth. -Qed. +Proof. exact/sorted_leq_nth_in/all_predT. Qed. End Transitive. @@ -291,10 +314,14 @@ End Paths. Arguments pathP {T e x p}. Arguments path_sorted {T e x s}. Arguments path_min_sorted {T e x s}. +Arguments order_path_min_in {T P leT 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_sorted_inE {T P leT} leT_tr {x s}. +Arguments sorted_ltn_nth_in {T P leT} leT_tr x0 {s}. +Arguments sorted_leq_nth_in {T P leT} leT_tr leT_refl x0 {s}. Arguments order_path_min {T leT x s}. Arguments path_mask {T leT} leT_tr {x} m {s}. Arguments path_filter {T leT} leT_tr {x} a {s}. @@ -417,13 +444,38 @@ Implicit Type s : seq T. Local Notation path := (path leT). Local Notation sorted := (sorted leT). +Lemma subseq_path_in x s1 s2 : + {in x :: s2 & &, transitive leT} -> subseq s1 s2 -> path x s2 -> path x s1. +Proof. by move=> tr /subseqP [m _ ->]; apply/(path_mask_in tr). Qed. + +Lemma subseq_sorted_in s1 s2 : + {in s2 & &, transitive leT} -> subseq s1 s2 -> sorted s2 -> sorted s1. +Proof. by move=> tr /subseqP [m _ ->]; apply/(sorted_mask_in tr). Qed. + +Lemma sorted_ltn_index_in s : {in s & &, transitive leT} -> sorted s -> + {in s &, forall x y, index x s < index y s -> leT x y}. +Proof. +case: s => // x0 s' leT_tr s_sorted x y xs ys. +move/(sorted_ltn_nth_in leT_tr x0 (allss (_ :: _)) s_sorted). +by rewrite ?nth_index ?[_ \in gtn _]index_mem //; apply. +Qed. + +Lemma sorted_leq_index_in s : + {in s & &, transitive leT} -> {in s, reflexive leT} -> sorted s -> + {in s &, forall x y, index x s <= index y s -> leT x y}. +Proof. +case: s => // x0 s' leT_tr leT_refl s_sorted x y xs ys. +move/(sorted_leq_nth_in leT_tr leT_refl x0 (allss (_ :: _)) s_sorted). +by rewrite ?nth_index ?[_ \in gtn _]index_mem //; apply. +Qed. + Hypothesis leT_tr : transitive leT. Lemma subseq_path x s1 s2 : subseq s1 s2 -> path x s2 -> path x s1. -Proof. by case/subseqP => m _ ->; apply/path_mask. Qed. +Proof. by apply: subseq_path_in; apply: in3W. Qed. Lemma subseq_sorted s1 s2 : subseq s1 s2 -> sorted s2 -> sorted s1. -Proof. by case/subseqP => m _ ->; apply/sorted_mask. Qed. +Proof. by apply: subseq_sorted_in; apply: in3W. Qed. Lemma sorted_uniq : irreflexive leT -> forall s, sorted s -> uniq s. Proof. @@ -475,9 +527,48 @@ Qed. End EqSorted. +Arguments sorted_ltn_index_in {T leT s} leT_tr s_sorted. +Arguments sorted_leq_index_in {T leT s} leT_tr leT_refl s_sorted. Arguments sorted_ltn_index {T leT} leT_tr {s}. Arguments sorted_leq_index {T leT} leT_tr leT_refl {s}. +Section EqSorted_in. + +Variables (T : eqType) (leT : rel T). +Implicit Type s : seq T. + +Lemma sorted_uniq_in s : + {in s & &, transitive leT} -> {in s, irreflexive leT} -> + sorted leT s -> uniq s. +Proof. +move=> /in3_sig leT_tr /in1_sig leT_irr; case/all_sigP: (allss s) => s' ->. +by rewrite sorted_map (map_inj_uniq val_inj); exact: sorted_uniq. +Qed. + +Lemma sorted_eq_in s1 s2 : + {in s1 & &, transitive leT} -> {in s1 &, antisymmetric leT} -> + sorted leT s1 -> sorted leT s2 -> perm_eq s1 s2 -> s1 = s2. +Proof. +move=> /in3_sig leT_tr /in2_sig leT_asym + + perm_s12; move: (perm_s12). +case/all_sigP: (allss s1) => s1' ->; move: (allss s1). +rewrite (perm_all _ perm_s12) => /all_sigP [s2' ->] /(perm_map_inj val_inj). +rewrite !sorted_map => {}perm_s12 s1_sorted s2_sorted; congr map. +by apply: sorted_eq s1_sorted s2_sorted perm_s12 => // ? ? /leT_asym /val_inj. +Qed. + +Lemma irr_sorted_eq_in s1 s2 : + {in s1 & &, transitive leT} -> {in s1, irreflexive leT} -> + sorted leT s1 -> sorted leT s2 -> s1 =i s2 -> s1 = s2. +Proof. +move=> /in3_sig leT_tr /in1_sig leT_irr + + eq_s12; move: (eq_s12). +case/all_sigP: (allss s1) => s1' ->; move: (allss s1). +rewrite (eq_all_r eq_s12) => /all_sigP [s2' ->]. +rewrite !sorted_map => {}eq_s12 s1_sorted s2_sorted; congr map. +by apply: (irr_sorted_eq leT_tr) => // x; rewrite -!(mem_map val_inj). +Qed. + +End EqSorted_in. + Section EqPath. Variables (n0 : nat) (T : eqType) (e : rel T). @@ -937,14 +1028,26 @@ Proof. by apply: perm_mem; rewrite perm_sort. Qed. Lemma sort_uniq s : uniq (sort leT s) = uniq s. Proof. by apply: perm_uniq; rewrite perm_sort. Qed. +Lemma perm_sort_inP s1 s2 : + {in s1 &, total leT} -> {in s1 & &, transitive leT} -> + {in s1 &, antisymmetric leT} -> + reflect (sort leT s1 = sort leT s2) (perm_eq s1 s2). +Proof. +move=> leT_total leT_tr leT_asym. +apply: (iffP idP) => eq12; last by rewrite -perm_sort eq12 perm_sort. +apply: sorted_eq_in. +- by move=> ? ? ?; rewrite !mem_sort; apply: leT_tr. +- by move=> ? ?; rewrite !mem_sort; apply: leT_asym. +- by apply/(sort_sorted_in leT_total). +- by apply/(sort_sorted_in leT_total); rewrite -(perm_all _ eq12). +- by rewrite perm_sort (permPl eq12) -perm_sort. +Qed. + Lemma perm_sortP : total leT -> transitive leT -> antisymmetric leT -> forall s1 s2, reflect (sort leT s1 = sort leT s2) (perm_eq s1 s2). Proof. -move=> leT_total leT_tr leT_asym s1 s2. -apply: (iffP idP) => eq12; last by rewrite -perm_sort eq12 perm_sort. -apply: (sorted_eq leT_tr leT_asym); rewrite ?sort_sorted //. -by rewrite perm_sort (permPl eq12) -perm_sort. +by move=> *; apply: perm_sort_inP; [apply: in2W | apply: in3W | apply: in2W]. Qed. End EqSortSeq. @@ -958,6 +1061,14 @@ exists (sort (relpre (nth x0 s) leT) (iota 0 (size s))). by rewrite -[X in sort leT X](mkseq_nth x0) sort_map. Qed. +Lemma all_sort (T : Type) (P : {pred T}) (leT : rel T) s : + all P (sort leT s) = all P s. +Proof. +case: s => // x s; move: (x :: s) => {}s. +rewrite -(mkseq_nth x s) sort_map !all_map. +by apply: perm_all; rewrite perm_sort. +Qed. + Lemma size_sort (T : Type) (leT : rel T) s : size (sort leT s) = size s. Proof. case: s => [|x s] //; have [s1 pp qq] := perm_iota_sort leT x (x :: s). diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 999ec0a..48a59ee 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -1500,6 +1500,16 @@ Arguments count_memPn {T x s}. Arguments uniqPn {T} x0 {s}. Arguments uniqP {T} x0 {s}. +(* Since both `all (mem s) s` and `all (pred_of_seq s) s` may appear in *) +(* goals, the following hint has to be declared using the `Hint Extern` *) +(* command. Additionally, `mem` and `pred_of_seq` in the above terms do not *) +(* reduce to each other; thus, stating `allss` in the form of one of them *) +(* makes `apply: allss` failing for the other case. Since both `mem` and *) +(* `pred_of_seq` reduce to `mem_seq`, the following explicit type annotation *) +(* for `allss` makes it work for both cases. *) +Hint Extern 0 (is_true (all _ _)) => + apply: (allss : forall T s, all (mem_seq s) s) : core. + Section NthTheory. Lemma nthP (T : eqType) (s : seq T) x x0 : -- cgit v1.2.3 From 84d3168ae3436acec2df0b6f83e85ae7c5310ce1 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Mon, 23 Nov 2020 20:26:32 +0900 Subject: Apply suggestions from code review Co-authored-by: Cyril Cohen --- mathcomp/ssreflect/path.v | 53 +++++++++++++++++++++++------------------------ 1 file changed, 26 insertions(+), 27 deletions(-) (limited to 'mathcomp') diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index df71460..269be3e 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -253,8 +253,8 @@ Lemma sorted_ltn_nth_in x0 s : all P s -> sorted leT s -> {in [pred n | n < size s] &, {homo nth x0 s : i j / i < j >-> leT i j}}. Proof. elim: s => // x s ihs Pxs path_xs [|i] [|j] //=; rewrite -!topredE /= !ltnS. -- by move=> _ js _; apply/all_nthP/js/order_path_min_in. -- by apply/ihs/path_sorted/path_xs; case/andP: Pxs. + by move=> _ js _; apply/all_nthP/js/order_path_min_in. +by apply/ihs/path_sorted/path_xs; case/andP: Pxs. Qed. Hypothesis leT_refl : {in P, reflexive leT}. @@ -549,21 +549,20 @@ Lemma sorted_eq_in s1 s2 : {in s1 & &, transitive leT} -> {in s1 &, antisymmetric leT} -> sorted leT s1 -> sorted leT s2 -> perm_eq s1 s2 -> s1 = s2. Proof. -move=> /in3_sig leT_tr /in2_sig leT_asym + + perm_s12; move: (perm_s12). -case/all_sigP: (allss s1) => s1' ->; move: (allss s1). -rewrite (perm_all _ perm_s12) => /all_sigP [s2' ->] /(perm_map_inj val_inj). -rewrite !sorted_map => {}perm_s12 s1_sorted s2_sorted; congr map. -by apply: sorted_eq s1_sorted s2_sorted perm_s12 => // ? ? /leT_asym /val_inj. +move=> /in3_sig leT_tr /in2_sig/(_ _ _ _)/val_inj leT_anti ss1 ss2 s1s2. +move: ss1 ss2 (s1s2); have /all_sigP[s1' ->] := allss s1. +have /all_sigP[{s1s2}s2 ->] : all (mem s1) s2 by rewrite -(perm_all _ s1s2). +by rewrite !sorted_map => ss1' ss2 /(perm_map_inj val_inj)/(sorted_eq leT_tr)->. Qed. Lemma irr_sorted_eq_in s1 s2 : {in s1 & &, transitive leT} -> {in s1, irreflexive leT} -> sorted leT s1 -> sorted leT s2 -> s1 =i s2 -> s1 = s2. Proof. -move=> /in3_sig leT_tr /in1_sig leT_irr + + eq_s12; move: (eq_s12). -case/all_sigP: (allss s1) => s1' ->; move: (allss s1). -rewrite (eq_all_r eq_s12) => /all_sigP [s2' ->]. -rewrite !sorted_map => {}eq_s12 s1_sorted s2_sorted; congr map. +move=> /in3_sig leT_tr /in1_sig leT_irr ss1 ss2 s1s2; move: ss1 ss2 (s1s2). +have /all_sigP[s1' ->] := allss s1. +have /all_sigP[s2' ->] : all (mem s1) s2 by rewrite -(eq_all_r s1s2). +rewrite !sorted_map => ss1' ss2' {}s1s2; congr map. by apply: (irr_sorted_eq leT_tr) => // x; rewrite -!(mem_map val_inj). Qed. @@ -1028,30 +1027,30 @@ Proof. by apply: perm_mem; rewrite perm_sort. Qed. Lemma sort_uniq s : uniq (sort leT s) = uniq s. Proof. by apply: perm_uniq; rewrite perm_sort. Qed. -Lemma perm_sort_inP s1 s2 : - {in s1 &, total leT} -> {in s1 & &, transitive leT} -> - {in s1 &, antisymmetric leT} -> - reflect (sort leT s1 = sort leT s2) (perm_eq s1 s2). -Proof. -move=> leT_total leT_tr leT_asym. -apply: (iffP idP) => eq12; last by rewrite -perm_sort eq12 perm_sort. -apply: sorted_eq_in. -- by move=> ? ? ?; rewrite !mem_sort; apply: leT_tr. -- by move=> ? ?; rewrite !mem_sort; apply: leT_asym. -- by apply/(sort_sorted_in leT_total). -- by apply/(sort_sorted_in leT_total); rewrite -(perm_all _ eq12). -- by rewrite perm_sort (permPl eq12) -perm_sort. -Qed. - Lemma perm_sortP : total leT -> transitive leT -> antisymmetric leT -> forall s1 s2, reflect (sort leT s1 = sort leT s2) (perm_eq s1 s2). Proof. -by move=> *; apply: perm_sort_inP; [apply: in2W | apply: in3W | apply: in2W]. +move=> leT_total leT_tr leT_asym s1 s2. +apply: (iffP idP) => eq12; last by rewrite -perm_sort eq12 perm_sort. +apply: (sorted_eq leT_tr leT_asym); rewrite ?sort_sorted //. +by rewrite perm_sort (permPl eq12) -perm_sort. Qed. End EqSortSeq. +Lemma perm_sort_inP (T : eqType) (leT : rel T) (s1 s2 : seq T) : + {in s1 &, total leT} -> {in s1 & &, transitive leT} -> + {in s1 &, antisymmetric leT} -> + reflect (sort leT s1 = sort leT s2) (perm_eq s1 s2). +Proof. +move=> /in2_sig leT_total /in3_sig leT_tr /in2_sig/(_ _ _ _)/val_inj leT_asym. +apply: (iffP idP) => s1s2; last by rewrite -(perm_sort leT) s1s2 perm_sort. +move: (s1s2); have /all_sigP[s1' ->] := allss s1. +have /all_sigP[{s1s2}s2 ->] : all (mem s1) s2 by rewrite -(perm_all _ s1s2). +by rewrite !sort_map => /(perm_map_inj val_inj) /(perm_sortP leT_total)->. +Qed. + Lemma perm_iota_sort (T : Type) (leT : rel T) x0 s : {i_s : seq nat | perm_eq i_s (iota 0 (size s)) & sort leT s = map (nth x0 s) i_s}. -- cgit v1.2.3 From ac30dae7377f9762ceba1c5553f0542831a0bb5c Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Mon, 23 Nov 2020 22:41:17 +0100 Subject: Using [dup] in path --- mathcomp/ssreflect/path.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'mathcomp') diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index 269be3e..5a9de74 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -549,8 +549,8 @@ Lemma sorted_eq_in s1 s2 : {in s1 & &, transitive leT} -> {in s1 &, antisymmetric leT} -> sorted leT s1 -> sorted leT s2 -> perm_eq s1 s2 -> s1 = s2. Proof. -move=> /in3_sig leT_tr /in2_sig/(_ _ _ _)/val_inj leT_anti ss1 ss2 s1s2. -move: ss1 ss2 (s1s2); have /all_sigP[s1' ->] := allss s1. +move=> /in3_sig leT_tr /in2_sig/(_ _ _ _)/val_inj leT_anti + + /[dup] s1s2. +have /all_sigP[s1' ->] := allss s1. have /all_sigP[{s1s2}s2 ->] : all (mem s1) s2 by rewrite -(perm_all _ s1s2). by rewrite !sorted_map => ss1' ss2 /(perm_map_inj val_inj)/(sorted_eq leT_tr)->. Qed. @@ -559,7 +559,7 @@ Lemma irr_sorted_eq_in s1 s2 : {in s1 & &, transitive leT} -> {in s1, irreflexive leT} -> sorted leT s1 -> sorted leT s2 -> s1 =i s2 -> s1 = s2. Proof. -move=> /in3_sig leT_tr /in1_sig leT_irr ss1 ss2 s1s2; move: ss1 ss2 (s1s2). +move=> /in3_sig leT_tr /in1_sig leT_irr + + /[dup] s1s2. have /all_sigP[s1' ->] := allss s1. have /all_sigP[s2' ->] : all (mem s1) s2 by rewrite -(eq_all_r s1s2). rewrite !sorted_map => ss1' ss2' {}s1s2; congr map. -- cgit v1.2.3