diff options
Diffstat (limited to 'mathcomp/ssreflect/seq.v')
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index e1e0ad4..6ffbd34 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -2996,10 +2996,21 @@ Lemma all2E s t : all2 s t = (size s == size t) && all [pred xy | r xy.1 xy.2] (zip s t). Proof. by elim: s t => [|x s IHs] [|y t] //=; rewrite IHs andbCA. Qed. +Lemma zip_map I f g (s : seq I) : + zip (map f s) (map g s) = [seq (f i, g i) | i <- s]. +Proof. by elim: s => //= i s ->. Qed. + End Zip. Prenex Implicits zip unzip1 unzip2 all2. +Lemma eqseq_all (T : eqType) (s t : seq T) : (s == t) = all2 eq_op s t. +Proof. by elim: s t => [|x s +] [|y t]//= => <-. Qed. + +Lemma eq_map_all I (T : eqType) (f g : I -> T) (s : seq I) : + (map f s == map g s) = all [pred xy | xy.1 == xy.2] [seq (f i, g i) | i <- s]. +Proof. by rewrite eqseq_all all2E !size_map eqxx zip_map. Qed. + Section Flatten. Variable T : Type. |