Library probsa.util.zip
From discprob.prob Require Export indep.
Require Export Reals Psatz.
From mathcomp Require Export ssreflect ssrnat ssrbool seq eqtype fintype ssrfun.
Section Zip.
Lemma unzip1_map_nth_zip {S T : eqType} x y (s : seq S) (t : seq T) l :
size s = size t →
unzip1 [seq nth (x, y) (seq.zip s t) i | i <- l] = [seq nth x s i | i <- l].
Lemma perm_zip1 {S T : eqType} (t1 t2 : seq T) (s1 s2 : seq S):
size s1 = size t1 → size s2 = size t2 →
perm_eq (seq.zip s1 t1) (seq.zip s2 t2) → perm_eq s1 s2.
End Zip.
From prosa.util Require Import list tactics.
From probsa.util Require Export boolp min.
From probsa.rt.model Require Export task.
Lemma zip_map :
∀ {X Y Z : eqType} (fx : X → Z) (fy : Y → Z) (xs : seq X) (ys : seq Y),
zip (map fx xs) (map fy ys)
= map (fun '(x,y) ⇒ (fx x, fy y)) (zip xs ys).
Lemma zip_foldr_andb_seq_eq :
∀ {X : eqType} (xs : seq X) (ys : seq X),
size xs = size ys →
(xs == ys) = fold_right andb true [seq z.1 == z.2 | z <- zip xs ys].
Lemma pointwise_min1_zip :
∀ (xs ys : seq R),
size xs = size ys →
(∀ x y, (x,y) \in seq.zip xs ys → x ≤ y)%R →
min1 xs ≤ min1 ys.
Lemma pointwise_leq_zip_impl_in_leq :
∀ {Z : eqType} (Fx Fy : Z → R) (zs : seq Z),
(∀ z, z \in zs → Fx z ≤ Fy z) →
∀ x y,
(x, y) \in zip [seq Fx x | x <- zs] [seq Fy y | y <- zs] →
x ≤ y.
Lemma perm_eq_zippable :
∀ {T B : eqType} (xs ys : seq T) (lb : seq B),
perm_eq xs ys →
size ys = size lb →
∃ plb,
perm_eq (seq.zip xs plb) (seq.zip ys lb)
∧ size xs = size plb.
Lemma zip_map_rvar_eq :
∀ {X Y : eqType} {Ω} {μ : measure Ω} (F : X → rvar μ Y) (xs : seq X) (ys : seq Y) ω,
map (fun Xb ⇒ rvar_fun μ _ (fst Xb) ω == (snd Xb)) (zip (map F xs) ys)
= [seq Xb.1 == Xb.2 | Xb <- zip [seq F i ω | i <- xs] ys].
Lemma zip_map_pr_eq :
∀ {X Y : eqType} {Ω} {μ : measure Ω} (F : X → rvar μ Y) (xs : seq X) (ys : seq Y),
[seq pr_eq Xb.1 Xb.2 | Xb <- zip [seq F i | i <- xs] ys]
= [seq pr_eq (F Xb.1) Xb.2 | Xb <- zip [seq i | i <- xs] ys].
Require Export Reals Psatz.
From mathcomp Require Export ssreflect ssrnat ssrbool seq eqtype fintype ssrfun.
Section Zip.
Lemma unzip1_map_nth_zip {S T : eqType} x y (s : seq S) (t : seq T) l :
size s = size t →
unzip1 [seq nth (x, y) (seq.zip s t) i | i <- l] = [seq nth x s i | i <- l].
Lemma perm_zip1 {S T : eqType} (t1 t2 : seq T) (s1 s2 : seq S):
size s1 = size t1 → size s2 = size t2 →
perm_eq (seq.zip s1 t1) (seq.zip s2 t2) → perm_eq s1 s2.
End Zip.
From prosa.util Require Import list tactics.
From probsa.util Require Export boolp min.
From probsa.rt.model Require Export task.
Lemma zip_map :
∀ {X Y Z : eqType} (fx : X → Z) (fy : Y → Z) (xs : seq X) (ys : seq Y),
zip (map fx xs) (map fy ys)
= map (fun '(x,y) ⇒ (fx x, fy y)) (zip xs ys).
Lemma zip_foldr_andb_seq_eq :
∀ {X : eqType} (xs : seq X) (ys : seq X),
size xs = size ys →
(xs == ys) = fold_right andb true [seq z.1 == z.2 | z <- zip xs ys].
Lemma pointwise_min1_zip :
∀ (xs ys : seq R),
size xs = size ys →
(∀ x y, (x,y) \in seq.zip xs ys → x ≤ y)%R →
min1 xs ≤ min1 ys.
Lemma pointwise_leq_zip_impl_in_leq :
∀ {Z : eqType} (Fx Fy : Z → R) (zs : seq Z),
(∀ z, z \in zs → Fx z ≤ Fy z) →
∀ x y,
(x, y) \in zip [seq Fx x | x <- zs] [seq Fy y | y <- zs] →
x ≤ y.
Lemma perm_eq_zippable :
∀ {T B : eqType} (xs ys : seq T) (lb : seq B),
perm_eq xs ys →
size ys = size lb →
∃ plb,
perm_eq (seq.zip xs plb) (seq.zip ys lb)
∧ size xs = size plb.
Lemma zip_map_rvar_eq :
∀ {X Y : eqType} {Ω} {μ : measure Ω} (F : X → rvar μ Y) (xs : seq X) (ys : seq Y) ω,
map (fun Xb ⇒ rvar_fun μ _ (fst Xb) ω == (snd Xb)) (zip (map F xs) ys)
= [seq Xb.1 == Xb.2 | Xb <- zip [seq F i ω | i <- xs] ys].
Lemma zip_map_pr_eq :
∀ {X Y : eqType} {Ω} {μ : measure Ω} (F : X → rvar μ Y) (xs : seq X) (ys : seq Y),
[seq pr_eq Xb.1 Xb.2 | Xb <- zip [seq F i | i <- xs] ys]
= [seq pr_eq (F Xb.1) Xb.2 | Xb <- zip [seq i | i <- xs] ys].