diff options
Diffstat (limited to 'mathcomp/ssreflect')
| -rw-r--r-- | mathcomp/ssreflect/path.v | 47 | ||||
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 39 |
2 files changed, 70 insertions, 16 deletions
diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index 2790aa8..bccafa8 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -167,16 +167,16 @@ Section HomoPath. Variables (T T' : Type) (f : T -> T') (leT : rel T) (leT' : rel T'). +Lemma path_map x s : path leT' (f x) (map f s) = path (relpre f leT') 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. -move=> f_homo; elim: s => //= y s IHs in x *. -by move=> /andP[le_xy path_y_s]; rewrite f_homo//= IHs. -Qed. +Proof. by move=> f_homo xs; rewrite path_map (sub_path _ xs). 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. -Proof. by move=> f_mon; elim: s => //= y s IHs in x *; rewrite f_mon IHs. Qed. +Proof. by move=> f_mon; rewrite path_map; apply: eq_path. Qed. End HomoPath. @@ -412,21 +412,24 @@ Section EqHomoPath. Variables (T : eqType) (T' : Type) (f : T -> T') (leT : rel T) (leT' : rel T'). -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). +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. -move=> f_homo; elim: s => //= y s IHs in x f_homo *; move=> /andP[x_y y_s]. -rewrite f_homo ?(in_cons, mem_head, eqxx, orbT) ?IHs//= => z t z_mem t_mem. -by apply: f_homo; rewrite in_cons ?(z_mem, t_mem, orbT). +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. -move=> f_mono; elim: s => //= y s IHs in x f_mono *. -rewrite f_mono ?(in_cons, mem_head, eqxx, orbT) ?IHs//= => z t z_mem t_mem. -by rewrite f_mono// in_cons ?(z_mem, t_mem, orbT). -Qed. +Proof. by move=> f_mono; rewrite path_map; apply: eq_path_in. Qed. End EqHomoPath. @@ -535,6 +538,12 @@ Qed. Hypothesis leT_tr : transitive leT. +Lemma path_sortedE x s : path leT 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. +Qed. + Lemma sorted_merge s t : sorted (s ++ t) -> merge s t = s ++ t. Proof. elim: s => //= x s; case: t; rewrite ?cats0 //= => y t ih hp. @@ -632,6 +641,10 @@ 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}. @@ -651,6 +664,10 @@ 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 merge := (merge leT). Local Notation sort := (sort leT). Local Notation sorted := (sorted leT). diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 65cc122..ed7c1dd 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -530,6 +530,9 @@ Proof. by elim: s => //= x s IHs; case a_x: (a x). Qed. Lemma before_find s i : i < find s -> a (nth s i) = false. Proof. by elim: s i => //= x s IHs; case: ifP => // a'x [|i] // /(IHs i). Qed. +Lemma hasNfind s : ~~ has s -> find s = size s. +Proof. by rewrite has_find; case: ltngtP (find_size s). Qed. + Lemma filter_cat s1 s2 : filter (s1 ++ s2) = filter s1 ++ filter s2. Proof. by elim: s1 => //= x s1 ->; case (a x). Qed. @@ -927,6 +930,23 @@ Proof. by move=> Pnil Pcons; elim=> [|x s IHs] [|y t] //= [eq_sz]; apply/Pcons/IHs. Qed. +Section FindSpec. +Variable (T : Type) (a : {pred T}) (s : seq T). + +Variant find_spec : bool -> nat -> Type := +| NotFound of ~~ has a s : find_spec false (size s) +| Found (i : nat) of i < size s & (forall x0, a (nth x0 s i)) & + (forall x0 j, j < i -> a (nth x0 s j) = false) : find_spec true i. + +Lemma findP : find_spec (has a s) (find a s). +Proof. +have [a_s|aNs] := boolP (has a s); last by rewrite hasNfind//; constructor. +by constructor=> [|x0|x0]; rewrite -?has_find ?nth_find//; apply: before_find. +Qed. + +End FindSpec. +Arguments findP {T}. + Section RotRcons. Variable T : Type. @@ -1302,6 +1322,9 @@ Proof. by rewrite /index find_size. Qed. Lemma index_mem x s : (index x s < size s) = (x \in s). Proof. by rewrite -has_pred1 has_find. Qed. +Lemma memNindex x s : x \notin s -> index x s = size s. +Proof. by rewrite -has_pred1 => /hasNfind. Qed. + Lemma nth_index x s : x \in s -> nth s (index x s) = x. Proof. by rewrite -has_pred1 => /(nth_find x0)/eqP. Qed. @@ -2495,6 +2518,9 @@ Variables (R : Type) (f : T2 -> R -> R) (z0 : R). Lemma foldr_cat s1 s2 : foldr f z0 (s1 ++ s2) = foldr f (foldr f z0 s2) s1. Proof. by elim: s1 => //= x s1 ->. Qed. +Lemma foldr_rcons s x : foldr f z0 (rcons s x) = foldr f (f x z0) s. +Proof. by rewrite -cats1 foldr_cat. Qed. + Lemma foldr_map s : foldr f z0 (map h s) = foldr (fun x z => f (h x) z) z0 s. Proof. by elim: s => //= x s ->. Qed. @@ -2549,6 +2575,9 @@ Proof. by rewrite -(revK (s1 ++ s2)) foldl_rev rev_cat foldr_cat -!foldl_rev !revK. Qed. +Lemma foldl_rcons z s x : foldl z (rcons s x) = f (foldl z s) x. +Proof. by rewrite -cats1 foldl_cat. Qed. + End FoldLeft. Section Scan. @@ -2579,9 +2608,17 @@ Lemma scanl_cat x s1 s2 : scanl x (s1 ++ s2) = scanl x s1 ++ scanl (foldl g x s1) s2. Proof. by elim: s1 x => //= y s1 IHs1 x; rewrite IHs1. Qed. +Lemma scanl_rcons x s1 y : + scanl x (rcons s1 y) = rcons (scanl x s1) (foldl g x (rcons s1 y)). +Proof. by rewrite -!cats1 scanl_cat foldl_cat. Qed. + +Lemma nth_cons_scanl s n : n <= size s -> + forall x, nth x1 (x :: scanl x s) n = foldl g x (take n s). +Proof. by elim: s n => [|y s IHs] [|n] Hn x //=; rewrite IHs. Qed. + Lemma nth_scanl s n : n < size s -> forall x, nth x1 (scanl x s) n = foldl g x (take n.+1 s). -Proof. by elim: s n => [|y s IHs] [|n] Hn x //=; rewrite ?take0 ?IHs. Qed. +Proof. by move=> n_lt x; rewrite -nth_cons_scanl. Qed. Lemma scanlK : (forall x, cancel (g x) (f x)) -> forall x, cancel (scanl x) (pairmap x). |