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].
Proof. by move⇒ st; elim: l ⇒ [//=|n l IH /=]; rewrite nth_zip ?IH ?st. Qed.
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.
Proof.
wlog [x y] : s1 s2 t1 t2 / (S × T)%type ⇒ [hwlog|].
case: s2 t2 ⇒ [|x s2] [|y t2] //; last exact: hwlog.
by case: s1 t1 ⇒ [|u s1] [|v t1]//= _ _ /perm_nilP.
move⇒ eq1 eq2 /(perm_iotaP (x, y))[ns nsP /(congr1 (@unzip1 _ _))].
rewrite unzip1_zip ?unzip1_map_nth_zip -?eq1// ⇒ →.
apply/(perm_iotaP x); ∃ ns; rewrite // size_zip -eq2 minnn in nsP ⇒ //.
Qed.
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).
Proof.
induction xs as [ | x xs]; move ⇒ [ | y ys] ⇒ //.
by rewrite //=; f_equal; apply IHxs.
Qed.
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].
Proof.
induction xs as [ | x xs]; first by move ⇒ [ |y ys].
move ⇒ [ |y ys]; first by done.
move ⇒ SIZE.
rewrite eqseq_cons IHxs //=.
by apply eq_add_S in SIZE.
Qed.
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.
Proof.
induction xs; first by intros [] SIZE IN; [rewrite //= /min1 //=; apply Rle_refl | done].
intros [] ⇒ //=.
intros SIZE IN; simpl in SIZE; apply eq_add_S in SIZE.
rewrite !min1_cons; apply Rle_min_compat.
{ by apply IN; rewrite in_cons eq_refl orTb. }
{ by apply IHxs ⇒ //; intros; apply IN; rewrite in_cons H orbT. }
Qed.
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.
Proof.
induction zs; first by done.
intros LE x y.
rewrite !map_cons zip_cons in_cons ⇒ /orP [/eqP EQ | IN].
{ by inversion EQ; subst x y; apply LE; rewrite in_cons eq_refl. }
{ apply: IHzs; last by apply IN.
by intros; apply LE; rewrite in_cons H orbT. }
Qed.
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.
Proof.
intros ? ? xs ys.
have [n LE] : ∃ n, (size ys ≤ n)%nat by (∃ (size ys)%nat).
move: xs ys LE; induction n.
{ intros ×.
rewrite leqn0; move⇒ /eqP ZE; apply size0nil in ZE.
subst ys; move⇒ lb /perm_nilP PERM; subst xs.
by move⇒ EQ; destruct lb; [∃ [::] | done].
}
move ⇒ xs [ | y ys].
{ move ⇒ _ lb /perm_nilP PERM; subst xs.
by move⇒ EQ; destruct lb; [∃ [::] | done].
}
move ⇒ LENT; have LEN : (size ys ≤ n)%nat; [by rewrite //= in LENT | clear LENT].
have seq_decomp :
y \in xs → xs = take (index y xs) xs ++ [::y] ++ drop (index y xs).+1 xs.
{ clear; elim: xs ⇒ [|x xs IH] /=; first by done.
case E: (x == y).
- by rewrite (eqP E) take0 drop0.
- rewrite /index /= ⇒ IN.
f_equal; move: IN; rewrite in_cons eq_sym E orFb.
by apply IH.
}
intros [ | l ylb] PERM SIZE; first by done.
have IN : y \in xs.
{ by apply perm_mem in PERM; specialize (PERM y); rewrite PERM mem_head. }
rewrite perm_sym in PERM.
have TR := @perm_trans _ xs (y :: ys) _ PERM (perm_to_rem IN).
specialize (IHn (rem (T:=T) y xs) ys LEN ylb).
feed IHn; first by rewrite perm_sym; rewrite perm_cons in TR.
feed IHn; first by inversion SIZE.
destruct IHn as [xlb [PERM2 SIZE2]].
set (i := index y xs) in ×.
∃ (take i xlb ++ [::l] ++ drop i xlb).
have SIEQ : size (take (index y xs) xs) = size (take i xlb).
{ rewrite /i !size_take index_mem IN.
destruct (index y xs < size xlb)%nat eqn:EQ ⇒ //.
move: EQ ⇒ /negP/negP; rewrite -leqNgt ⇒ GE.
apply/eqP; rewrite eqn_leq; apply/andP; split ⇒ //; clear GE.
move: (IN) ⇒ LT; rewrite -index_mem in LT.
rewrite -ltnS; apply: leq_trans; [by apply LT | clear LT].
apply perm_size in PERM; apply perm_size in PERM2.
inversion SIZE as [TE]; clear SIZE; rename TE into SIZE.
rewrite //= in PERM.
rewrite !size_zip -SIZE minnn size_rem // -PERM //= in PERM2.
by rewrite -PERM ltnS -PERM2; apply geq_minr.
}
rewrite {1}seq_decomp // !zip_cat // zip_cons; split.
{ apply: perm_trans; first by apply permEl, perm_catCA.
rewrite //= perm_cons; apply: perm_trans; last apply PERM2.
by rewrite -!zip_cat // -!remE cat_take_drop; apply perm_refl.
}
{ rewrite !size_cat //= addnA [addn _ 1%N]addnC -addnA -size_cat cat_take_drop.
rewrite size_rem // in SIZE2.
rewrite -SIZE2 addnC addn1.
by destruct xs.
}
Qed.
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].
Proof.
induction xs.
{ by intros; rewrite //= !zip_nil. }
intros [ | y ys]; first by done.
intros ω; rewrite //= IHxs //.
Qed.
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].
Proof.
induction xs.
{ by intros; rewrite //= !zip_nil. }
intros [ | t tlb]; first by done.
by rewrite //= IHxs.
Qed.
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].
Proof. by move⇒ st; elim: l ⇒ [//=|n l IH /=]; rewrite nth_zip ?IH ?st. Qed.
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.
Proof.
wlog [x y] : s1 s2 t1 t2 / (S × T)%type ⇒ [hwlog|].
case: s2 t2 ⇒ [|x s2] [|y t2] //; last exact: hwlog.
by case: s1 t1 ⇒ [|u s1] [|v t1]//= _ _ /perm_nilP.
move⇒ eq1 eq2 /(perm_iotaP (x, y))[ns nsP /(congr1 (@unzip1 _ _))].
rewrite unzip1_zip ?unzip1_map_nth_zip -?eq1// ⇒ →.
apply/(perm_iotaP x); ∃ ns; rewrite // size_zip -eq2 minnn in nsP ⇒ //.
Qed.
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).
Proof.
induction xs as [ | x xs]; move ⇒ [ | y ys] ⇒ //.
by rewrite //=; f_equal; apply IHxs.
Qed.
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].
Proof.
induction xs as [ | x xs]; first by move ⇒ [ |y ys].
move ⇒ [ |y ys]; first by done.
move ⇒ SIZE.
rewrite eqseq_cons IHxs //=.
by apply eq_add_S in SIZE.
Qed.
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.
Proof.
induction xs; first by intros [] SIZE IN; [rewrite //= /min1 //=; apply Rle_refl | done].
intros [] ⇒ //=.
intros SIZE IN; simpl in SIZE; apply eq_add_S in SIZE.
rewrite !min1_cons; apply Rle_min_compat.
{ by apply IN; rewrite in_cons eq_refl orTb. }
{ by apply IHxs ⇒ //; intros; apply IN; rewrite in_cons H orbT. }
Qed.
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.
Proof.
induction zs; first by done.
intros LE x y.
rewrite !map_cons zip_cons in_cons ⇒ /orP [/eqP EQ | IN].
{ by inversion EQ; subst x y; apply LE; rewrite in_cons eq_refl. }
{ apply: IHzs; last by apply IN.
by intros; apply LE; rewrite in_cons H orbT. }
Qed.
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.
Proof.
intros ? ? xs ys.
have [n LE] : ∃ n, (size ys ≤ n)%nat by (∃ (size ys)%nat).
move: xs ys LE; induction n.
{ intros ×.
rewrite leqn0; move⇒ /eqP ZE; apply size0nil in ZE.
subst ys; move⇒ lb /perm_nilP PERM; subst xs.
by move⇒ EQ; destruct lb; [∃ [::] | done].
}
move ⇒ xs [ | y ys].
{ move ⇒ _ lb /perm_nilP PERM; subst xs.
by move⇒ EQ; destruct lb; [∃ [::] | done].
}
move ⇒ LENT; have LEN : (size ys ≤ n)%nat; [by rewrite //= in LENT | clear LENT].
have seq_decomp :
y \in xs → xs = take (index y xs) xs ++ [::y] ++ drop (index y xs).+1 xs.
{ clear; elim: xs ⇒ [|x xs IH] /=; first by done.
case E: (x == y).
- by rewrite (eqP E) take0 drop0.
- rewrite /index /= ⇒ IN.
f_equal; move: IN; rewrite in_cons eq_sym E orFb.
by apply IH.
}
intros [ | l ylb] PERM SIZE; first by done.
have IN : y \in xs.
{ by apply perm_mem in PERM; specialize (PERM y); rewrite PERM mem_head. }
rewrite perm_sym in PERM.
have TR := @perm_trans _ xs (y :: ys) _ PERM (perm_to_rem IN).
specialize (IHn (rem (T:=T) y xs) ys LEN ylb).
feed IHn; first by rewrite perm_sym; rewrite perm_cons in TR.
feed IHn; first by inversion SIZE.
destruct IHn as [xlb [PERM2 SIZE2]].
set (i := index y xs) in ×.
∃ (take i xlb ++ [::l] ++ drop i xlb).
have SIEQ : size (take (index y xs) xs) = size (take i xlb).
{ rewrite /i !size_take index_mem IN.
destruct (index y xs < size xlb)%nat eqn:EQ ⇒ //.
move: EQ ⇒ /negP/negP; rewrite -leqNgt ⇒ GE.
apply/eqP; rewrite eqn_leq; apply/andP; split ⇒ //; clear GE.
move: (IN) ⇒ LT; rewrite -index_mem in LT.
rewrite -ltnS; apply: leq_trans; [by apply LT | clear LT].
apply perm_size in PERM; apply perm_size in PERM2.
inversion SIZE as [TE]; clear SIZE; rename TE into SIZE.
rewrite //= in PERM.
rewrite !size_zip -SIZE minnn size_rem // -PERM //= in PERM2.
by rewrite -PERM ltnS -PERM2; apply geq_minr.
}
rewrite {1}seq_decomp // !zip_cat // zip_cons; split.
{ apply: perm_trans; first by apply permEl, perm_catCA.
rewrite //= perm_cons; apply: perm_trans; last apply PERM2.
by rewrite -!zip_cat // -!remE cat_take_drop; apply perm_refl.
}
{ rewrite !size_cat //= addnA [addn _ 1%N]addnC -addnA -size_cat cat_take_drop.
rewrite size_rem // in SIZE2.
rewrite -SIZE2 addnC addn1.
by destruct xs.
}
Qed.
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].
Proof.
induction xs.
{ by intros; rewrite //= !zip_nil. }
intros [ | y ys]; first by done.
intros ω; rewrite //= IHxs //.
Qed.
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].
Proof.
induction xs.
{ by intros; rewrite //= !zip_nil. }
intros [ | t tlb]; first by done.
by rewrite //= IHxs.
Qed.