map_reduce.v 14.2 KB
 Robbert Krebbers committed Jul 07, 2019 1 ``````From actris.channel Require Import proto_channel proofmode. `````` Robbert Krebbers committed Jul 05, 2019 2 ``````From iris.heap_lang Require Import proofmode notation. `````` Robbert Krebbers committed Jul 09, 2019 3 ``````From actris.utils Require Import llist compare contribution group. `````` jihgfee committed Jul 11, 2019 4 ``````From actris.examples Require Import map sort_fg. `````` Robbert Krebbers committed Jul 05, 2019 5 6 7 8 9 10 ``````From iris.algebra Require Import gmultiset. (** Functional version of map reduce (aka the specification) *) Definition map_reduce {A B C} `{EqDecision K} (map : A → list (K * B)) (red : K → list B → list C) : list A → list C := mbind (curry red) ∘ group ∘ mbind map. `````` Robbert Krebbers committed Jul 09, 2019 11 ``````Instance: Params (@map_reduce) 7. `````` Robbert Krebbers committed Jul 06, 2019 12 13 `````` (** Distributed version *) `````` Robbert Krebbers committed Jul 09, 2019 14 ``````Definition par_map_reduce_map : val := `````` Robbert Krebbers committed Jul 06, 2019 15 16 17 18 19 20 21 22 `````` rec: "go" "n" "cmap" "csort" "xs" := if: "n" = #0 then #() else if: recv "cmap" then (* send item to mapper *) if: lisnil "xs" then send "cmap" #false;; "go" ("n" - #1) "cmap" "csort" "xs" else send "cmap" #true;; `````` Robbert Krebbers committed Jul 08, 2019 23 24 `````` send "cmap" (lpop "xs");; "go" "n" "cmap" "csort" "xs" `````` Robbert Krebbers committed Jul 06, 2019 25 26 27 28 29 30 31 `````` else (* receive item from mapper *) let: "zs" := recv "cmap" in send_all "csort" "zs";; "go" "n" "cmap" "csort" "xs". Definition par_map_reduce_collect : val := rec: "go" "csort" "i" "ys" := `````` Robbert Krebbers committed Jul 08, 2019 32 `````` if: ~recv "csort" then NONE else `````` Robbert Krebbers committed Jul 06, 2019 33 34 `````` let: "jy" := recv "csort" in let: "j" := Fst "jy" in let: "y" := Snd "jy" in `````` Robbert Krebbers committed Jul 08, 2019 35 36 `````` if: "i" = "j" then lcons "y" "ys";; "go" "csort" "j" "ys" else SOME ("j", "y"). `````` Robbert Krebbers committed Jul 06, 2019 37 `````` `````` Robbert Krebbers committed Jul 09, 2019 38 ``````Definition par_map_reduce_reduce : val := `````` Robbert Krebbers committed Jul 06, 2019 39 `````` rec: "go" "n" "csort" "cred" "acc" "zs" := `````` Robbert Krebbers committed Jul 08, 2019 40 `````` if: "n" = #0 then #() else `````` Robbert Krebbers committed Jul 06, 2019 41 42 43 44 45 46 47 `````` if: recv "cred" then (* Send item to mapper *) match: "acc" with NONE => (* nothing left *) send "cred" #false;; "go" ("n" - #1) "csort" "cred" NONE "zs" | SOME "acc" => (* Read subsequent items with the same key *) `````` Robbert Krebbers committed Jul 08, 2019 48 `````` let: "ys" := lnil #() in lcons (Snd "acc") "ys";; `````` Robbert Krebbers committed Jul 08, 2019 49 `````` let: "new_acc" := par_map_reduce_collect "csort" (Fst "acc") "ys" in `````` Robbert Krebbers committed Jul 06, 2019 50 `````` send "cred" #true;; `````` Robbert Krebbers committed Jul 08, 2019 51 52 `````` send "cred" (Fst "acc", "ys");; "go" "n" "csort" "cred" "new_acc" "zs" `````` Robbert Krebbers committed Jul 06, 2019 53 54 55 `````` end else (* receive item from mapper *) let: "zs'" := recv "cred" in `````` Robbert Krebbers committed Jul 08, 2019 56 57 `````` lprep "zs" "zs'";; "go" "n" "csort" "cred" "acc" "zs". `````` Robbert Krebbers committed Jul 06, 2019 58 59 60 `````` Definition cmpZfst : val := λ: "x" "y", Fst "x" ≤ Fst "y". `````` Robbert Krebbers committed Jul 10, 2019 61 ``````Definition par_map_reduce : val := λ: "n" "m" "map" "red" "xs", `````` Robbert Krebbers committed Jul 09, 2019 62 `````` let: "cmap" := start_chan (λ: "c", par_map_service "n" "map" "c") in `````` Robbert Krebbers committed Jul 09, 2019 63 `````` let: "csort" := start_chan (λ: "c", sort_service_fg cmpZfst "c") in `````` Robbert Krebbers committed Jul 09, 2019 64 `````` par_map_reduce_map "n" "cmap" "csort" "xs";; `````` Robbert Krebbers committed Jul 06, 2019 65 `````` send "csort" #stop;; `````` Robbert Krebbers committed Jul 10, 2019 66 `````` let: "cred" := start_chan (λ: "c", par_map_service "m" "red" "c") in `````` Robbert Krebbers committed Jul 06, 2019 67 `````` (* We need the first sorted element in the loop to compare subsequent elements *) `````` Robbert Krebbers committed Jul 09, 2019 68 `````` if: ~recv "csort" then #() else (* Handle the empty case *) `````` Robbert Krebbers committed Jul 06, 2019 69 `````` let: "jy" := recv "csort" in `````` Robbert Krebbers committed Jul 10, 2019 70 `````` par_map_reduce_reduce "m" "csort" "cred" (SOME "jy") "xs". `````` Robbert Krebbers committed Jul 06, 2019 71 72 `````` `````` Robbert Krebbers committed Jul 05, 2019 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 ``````(** Properties about the functional version *) Section map_reduce. Context {A B C} `{EqDecision K} (map : A → list (K * B)) (red : K → list B → list C). Context `{!∀ j, Proper ((≡ₚ) ==> (≡ₚ)) (red j)}. Global Instance bind_red_perm : Proper ((≡ₚₚ) ==> (≡ₚ)) (mbind (curry red)). Proof. induction 1 as [|[i1 xs1] [i2 xs2] ixss1 ixss2 [??]|[i1 xs1] [i2 xs2] ixss|]; simplify_eq/=; try done. - repeat (done || f_equiv). - by rewrite !assoc_L (comm _ (red i2 xs2)). - by etrans. Qed. Global Instance map_reduce_perm : Proper ((≡ₚ) ==> (≡ₚ)) (map_reduce map red). Proof. intros xs1 xs2 Hxs. by rewrite /map_reduce /= Hxs. Qed. End map_reduce. (** Correctness proofs of the distributed version *) Class map_reduceG Σ A B `{Countable A, Countable B} := { `````` Robbert Krebbers committed Jul 06, 2019 92 93 `````` map_reduce_mapG :> mapG Σ A; map_reduce_reduceG :> mapG Σ (Z * list B); `````` Robbert Krebbers committed Jul 05, 2019 94 95 96 97 ``````}. Section mapper. Context `{Countable A, Countable B} {C : Type}. `````` Robbert Krebbers committed Jul 10, 2019 98 `````` Context `{!heapG Σ, !proto_chanG Σ, !map_reduceG Σ A B}. `````` Robbert Krebbers committed Jul 05, 2019 99 100 101 102 `````` Context (IA : A → val → iProp Σ) (IB : Z → B → val → iProp Σ) (IC : C → val → iProp Σ). Context (map : A → list (Z * B)) (red : Z → list B → list C). Context `{!∀ j, Proper ((≡ₚ) ==> (≡ₚ)) (red j)}. Local Open Scope nat_scope. `````` Robbert Krebbers committed Jul 06, 2019 103 `````` Implicit Types n : nat. `````` Robbert Krebbers committed Jul 05, 2019 104 105 106 107 `````` Definition IZB (iy : Z * B) (w : val) : iProp Σ := (∃ w', ⌜ w = (#iy.1, w')%V ⌝ ∧ IB iy.1 iy.2 w')%I. Definition IZBs (iys : Z * list B) (w : val) : iProp Σ := `````` Robbert Krebbers committed Jul 08, 2019 108 `````` (∃ (l : loc), ⌜ w = (#iys.1, #l)%V ⌝ ∗ llist (IB iys.1) l (iys.2))%I. `````` Robbert Krebbers committed Jul 05, 2019 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 `````` Definition RZB : relation (Z * B) := prod_relation (≤)%Z (λ _ _ : B, True). Instance RZB_dec : RelDecision RZB. Proof. solve_decision. Qed. Instance RZB_total : Total RZB. Proof. intros [i1 y1] [i2 y2]. destruct (total (≤)%Z i1 i2); [left|right]; done. Qed. Instance RZB_trans : Transitive RZB. Proof. by apply (prod_relation_trans _). Qed. Lemma RZB_cmp_spec : cmp_spec IZB RZB cmpZfst. Proof. iIntros ([i1 y1] [i2 y2] v1 v2) "!>"; iIntros (Φ) "[HI1 HI2] HΦ". iDestruct "HI1" as (w1 ->) "HI1". iDestruct "HI2" as (w2 ->) "HI2 /=". wp_lam; wp_pures. iSpecialize ("HΦ" with "[HI1 HI2]"). { iSplitL "HI1"; rewrite /IZB /=; eauto with iFrame. } repeat case_bool_decide=> //; unfold RZB, prod_relation in *; naive_solver. Qed. `````` Robbert Krebbers committed Jul 09, 2019 126 `````` Lemma par_map_reduce_map_spec n cmap csort l xs X ys : `````` Robbert Krebbers committed Jul 05, 2019 127 128 `````` (n = 0 → X = ∅ ∧ xs = []) → {{{ `````` Robbert Krebbers committed Jul 08, 2019 129 `````` llist IA l xs ∗ `````` Robbert Krebbers committed Jul 10, 2019 130 131 `````` cmap ↣ par_map_protocol IA IZB map n (X : gmultiset A) ∗ csort ↣ sort_fg_head_protocol IZB RZB ys `````` Robbert Krebbers committed Jul 05, 2019 132 `````` }}} `````` Robbert Krebbers committed Jul 09, 2019 133 `````` par_map_reduce_map #n cmap csort #l `````` Robbert Krebbers committed Jul 05, 2019 134 135 `````` {{{ ys', RET #(); ⌜ys' ≡ₚ (xs ++ elements X) ≫= map⌝ ∗ `````` Robbert Krebbers committed Jul 10, 2019 136 `````` llist IA l [] ∗ csort ↣ sort_fg_head_protocol IZB RZB (ys ++ ys') `````` Robbert Krebbers committed Jul 05, 2019 137 138 `````` }}}. Proof. `````` Robbert Krebbers committed Jul 08, 2019 139 140 `````` iIntros (Hn Φ) "(Hl & Hcmap & Hcsort) HΦ". iLöb as "IH" forall (n xs X ys Hn Φ); wp_rec; wp_pures; simpl. `````` Robbert Krebbers committed Jul 05, 2019 141 142 `````` case_bool_decide; wp_pures; simplify_eq/=. { destruct Hn as [-> ->]; first lia. `````` Robbert Krebbers committed Jul 09, 2019 143 `````` iApply ("HΦ" \$! []). rewrite right_id_L. auto with iFrame. } `````` Robbert Krebbers committed Jul 05, 2019 144 `````` destruct n as [|n]=> //=. wp_branch as %?|%_; wp_pures. `````` Robbert Krebbers committed Jul 08, 2019 145 `````` - wp_apply (lisnil_spec with "Hl"); iIntros "Hl". `````` Robbert Krebbers committed Jul 08, 2019 146 `````` destruct xs as [|x xs]; csimpl; wp_pures. `````` Robbert Krebbers committed Jul 05, 2019 147 `````` + wp_select. wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ. `````` Robbert Krebbers committed Jul 08, 2019 148 149 150 151 `````` iApply ("IH" \$! _ [] with "[%] Hl Hcmap Hcsort HΦ"); naive_solver. + wp_select. wp_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]". wp_send with "[\$HIx]". wp_apply ("IH" with "[%] Hl Hcmap Hcsort"); first done. iIntros (ys'). `````` Robbert Krebbers committed Jul 05, 2019 152 153 `````` rewrite gmultiset_elements_disj_union gmultiset_elements_singleton. rewrite assoc_L -(comm _ [x]). iApply "HΦ". `````` Robbert Krebbers committed Jul 08, 2019 154 `````` - wp_recv (x k) as (Hx) "Hk". `````` Robbert Krebbers committed Jul 09, 2019 155 `````` rewrite -(right_id END%proto _ (sort_fg_head_protocol _ _ _)). `````` Robbert Krebbers committed Jul 09, 2019 156 `````` wp_apply (send_all_spec with "[\$Hk \$Hcsort]"); iIntros "[_ Hcsort]". `````` Robbert Krebbers committed Jul 05, 2019 157 `````` rewrite right_id. `````` Robbert Krebbers committed Jul 08, 2019 158 `````` wp_apply ("IH" with "[] Hl Hcmap Hcsort"); first done. `````` Robbert Krebbers committed Jul 05, 2019 159 160 161 162 `````` iIntros (ys'). iDestruct 1 as (Hys) "Hcsort"; simplify_eq/=. rewrite -assoc_L. iApply ("HΦ" \$! (map x ++ ys') with "[\$Hcsort]"). iPureIntro. rewrite (gmultiset_disj_union_difference {[ x ]} X) -?gmultiset_elem_of_singleton_subseteq //. `````` Robbert Krebbers committed Sep 17, 2019 163 `````` rewrite (comm_L disj_union) gmultiset_elements_disj_union. `````` Robbert Krebbers committed Jul 05, 2019 164 165 166 `````` by rewrite gmultiset_elements_singleton assoc_L bind_app -Hys /= right_id_L comm. Qed. `````` Robbert Krebbers committed Jul 08, 2019 167 `````` Lemma par_map_reduce_collect_spec csort iys iys_sorted i l ys : `````` Robbert Krebbers committed Jul 05, 2019 168 169 170 171 172 173 `````` let acc := from_option (λ '(i,y,w), [(i,y)]) [] in let accv := from_option (λ '(i,y,w), SOMEV (#(i:Z),w)) NONEV in ys ≠ [] → Sorted RZB (iys_sorted ++ ((i,) <\$> ys)) → i ∉ iys_sorted.*1 → {{{ `````` Robbert Krebbers committed Jul 08, 2019 174 `````` llist (IB i) l (reverse ys) ∗ `````` Robbert Krebbers committed Jul 10, 2019 175 `````` csort ↣ sort_fg_tail_protocol IZB RZB iys (iys_sorted ++ ((i,) <\$> ys)) `````` Robbert Krebbers committed Jul 05, 2019 176 `````` }}} `````` Robbert Krebbers committed Jul 08, 2019 177 `````` par_map_reduce_collect csort #i #l `````` Robbert Krebbers committed Jul 08, 2019 178 `````` {{{ ys' miy, RET accv miy; `````` Robbert Krebbers committed Jul 05, 2019 179 180 181 `````` ⌜ Sorted RZB ((iys_sorted ++ ((i,) <\$> ys ++ ys')) ++ acc miy) ⌝ ∗ ⌜ from_option (λ '(j,_,_), i ≠ j ∧ j ∉ iys_sorted.*1) (iys_sorted ++ ((i,) <\$> ys ++ ys') ≡ₚ iys) miy ⌝ ∗ `````` Robbert Krebbers committed Jul 08, 2019 182 `````` llist (IB i) l (reverse (ys ++ ys')) ∗ `````` Robbert Krebbers committed Jul 09, 2019 183 `````` csort ↣ from_option (λ _, sort_fg_tail_protocol IZB RZB iys `````` Robbert Krebbers committed Jul 10, 2019 184 `````` ((iys_sorted ++ ((i,) <\$> ys ++ ys')) ++ acc miy)) END%proto miy ∗ `````` Robbert Krebbers committed Jul 05, 2019 185 186 187 `````` from_option (λ '(i,y,w), IB i y w) True miy }}}. Proof. `````` Robbert Krebbers committed Jul 08, 2019 188 189 `````` iIntros (acc accv Hys Hsort Hi Φ) "[Hl Hcsort] HΦ". iLöb as "IH" forall (ys Hys Hsort Hi Φ); wp_rec; wp_pures; simpl. `````` Robbert Krebbers committed Jul 05, 2019 190 `````` wp_branch as %_|%Hperm; last first; wp_pures. `````` Robbert Krebbers committed Jul 08, 2019 191 `````` { iApply ("HΦ" \$! [] None with "[Hl \$Hcsort]"); simpl. `````` Robbert Krebbers committed Jul 08, 2019 192 `````` iEval (rewrite !right_id_L); auto with iFrame. } `````` Robbert Krebbers committed Jul 08, 2019 193 `````` wp_recv ([j y] ?) as (Htl w ->) "HIy /=". wp_pures. rewrite -assoc_L. `````` Robbert Krebbers committed Jul 05, 2019 194 `````` case_bool_decide as Hij; simplify_eq/=; wp_pures. `````` Robbert Krebbers committed Jul 08, 2019 195 `````` - wp_apply (lcons_spec with "[\$Hl \$HIy]"); iIntros "Hl". `````` Robbert Krebbers committed Jul 05, 2019 196 `````` rewrite -reverse_snoc. wp_apply ("IH" \$! (ys ++ [y]) `````` Robbert Krebbers committed Jul 08, 2019 197 `````` with "[%] [%] [//] Hl [Hcsort] [HΦ]"); try iClear "IH". `````` Robbert Krebbers committed Jul 05, 2019 198 199 200 `````` + intros ?; discriminate_list. + rewrite fmap_app /= assoc_L. by apply Sorted_snoc. + by rewrite fmap_app /= assoc_L. `````` Robbert Krebbers committed Jul 08, 2019 201 202 `````` + iIntros "!>" (ys' miy). rewrite -!(assoc_L _ ys) /=. iApply "HΦ". - iApply ("HΦ" \$! [] (Some (j,y,w))). `````` Robbert Krebbers committed Jul 05, 2019 203 204 205 206 207 208 209 210 211 212 213 214 215 `````` rewrite /= !right_id_L assoc_L. iFrame. iPureIntro; split. { by apply Sorted_snoc. } split; first congruence. intros [[j' y'] [-> Hj]]%elem_of_list_fmap. destruct Hij; do 2 f_equal. destruct ys as [|y'' ys _] using rev_ind; first done. move: Htl. rewrite fmap_app assoc_L /=. inversion 1 as [|?? [? _]]; discriminate_list || simplify_list_eq. assert (RZB (j',y') (i,y'')) as [??]; last (simpl in *; lia). apply (Sorted_StronglySorted _) in Hsort. eapply elem_of_StronglySorted_app; set_solver. Qed. `````` Robbert Krebbers committed Jul 09, 2019 216 `````` Lemma par_map_reduce_reduce_spec n iys iys_sorted miy zs l Y csort cred : `````` Robbert Krebbers committed Jul 05, 2019 217 218 219 220 221 222 `````` let acc := from_option (λ '(i,y,w), [(i,y)]) [] in let accv := from_option (λ '(i,y,w), SOMEV (#(i:Z),w)) NONEV in (n = 0 → miy = None ∧ Y = ∅) → from_option (λ '(i,_,_), i ∉ iys_sorted.*1) (iys_sorted ≡ₚ iys) miy → Sorted RZB (iys_sorted ++ acc miy) → {{{ `````` Robbert Krebbers committed Jul 08, 2019 223 `````` llist IC l zs ∗ `````` Robbert Krebbers committed Jul 09, 2019 224 `````` csort ↣ from_option (λ _, sort_fg_tail_protocol IZB RZB iys `````` Robbert Krebbers committed Jul 10, 2019 225 226 `````` (iys_sorted ++ acc miy)) END%proto miy ∗ cred ↣ par_map_protocol IZBs IC (curry red) n (Y : gmultiset (Z * list B)) ∗ `````` Robbert Krebbers committed Jul 08, 2019 227 `````` from_option (λ '(i,y,w), IB i y w) True miy `````` Robbert Krebbers committed Jul 05, 2019 228 `````` }}} `````` Robbert Krebbers committed Jul 09, 2019 229 `````` par_map_reduce_reduce #n csort cred (accv miy) #l `````` Robbert Krebbers committed Jul 08, 2019 230 `````` {{{ zs', RET #(); `````` Robbert Krebbers committed Jul 05, 2019 231 `````` ⌜ (group iys_sorted ≫= curry red) ++ zs' ≡ₚ (group iys ++ elements Y) ≫= curry red ⌝ ∗ `````` Robbert Krebbers committed Jul 08, 2019 232 `````` llist IC l (zs' ++ zs) `````` Robbert Krebbers committed Jul 05, 2019 233 234 `````` }}}. Proof. `````` Robbert Krebbers committed Jul 08, 2019 235 236 `````` iIntros (acc accv Hn Hmiy Hsort Φ) "(Hl & Hcsort & Hcred & HImiy) HΦ". iLöb as "IH" forall (n iys_sorted miy zs Y Hn Hmiy Hsort Φ); wp_rec; wp_pures; simpl. `````` Robbert Krebbers committed Jul 05, 2019 237 238 `````` case_bool_decide; wp_pures; simplify_eq/=. { destruct Hn as [-> ->]; first lia. `````` Robbert Krebbers committed Jul 08, 2019 239 `````` iApply ("HΦ" \$! [] with "[\$Hl]"); iPureIntro; simpl. `````` Robbert Krebbers committed Jul 05, 2019 240 241 242 243 244 `````` by rewrite gmultiset_elements_empty !right_id_L Hmiy. } destruct n as [|n]=> //=. wp_branch as %?|%_; wp_pures. - destruct miy as [[[i y] w]|]; simplify_eq/=; wp_pures; last first. + wp_select. wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ. iApply ("IH" \$! _ _ None `````` Robbert Krebbers committed Jul 08, 2019 245 246 247 248 249 250 251 252 `````` with "[%] [%] [%] Hl Hcsort Hcred [] HΦ"); naive_solver. + wp_apply (lnil_spec (IB i) with "[//]"); iIntros (k) "Hk". wp_apply (lcons_spec with "[\$Hk \$HImiy]"); iIntros "Hk". wp_apply (par_map_reduce_collect_spec _ _ _ _ _ [_] with "[\$Hk \$Hcsort]"); try done. iIntros (ys' miy). iDestruct 1 as (? Hmiy') "(Hk & Hcsort & HImiy)"; csimpl. wp_select; wp_pures. wp_send ((i, reverse (y :: ys'))) with "[Hk]". { iExists k; simpl; auto. } `````` Robbert Krebbers committed Jul 05, 2019 253 `````` wp_pures. iApply ("IH" \$! _ (_ ++ _) miy `````` Robbert Krebbers committed Jul 08, 2019 254 `````` with "[%] [%] [//] Hl Hcsort Hcred HImiy"); first done. `````` Robbert Krebbers committed Jul 05, 2019 255 `````` { destruct miy as [[[i' y'] w']|]; set_solver +Hmiy'. } `````` Robbert Krebbers committed Jul 08, 2019 256 `````` iIntros "!>" (zs'). iDestruct 1 as (Hperm) "HIC". `````` Robbert Krebbers committed Jul 05, 2019 257 258 259 260 261 `````` iApply ("HΦ" with "[\$HIC]"); iPureIntro; move: Hperm. rewrite gmultiset_elements_disj_union gmultiset_elements_singleton. rewrite group_snoc // reverse_Permutation. rewrite !bind_app /= right_id_L -!assoc_L -(comm _ zs') !assoc_L. apply (inj (++ _)). `````` Robbert Krebbers committed Jul 08, 2019 262 `````` - wp_recv ([i ys] k) as (Hy) "Hk". `````` Robbert Krebbers committed Jul 08, 2019 263 `````` wp_apply (lprep_spec with "[\$Hl \$Hk]"); iIntros "[Hl _]". `````` Robbert Krebbers committed Jul 08, 2019 264 265 `````` wp_apply ("IH" with "[ ] [//] [//] Hl Hcsort Hcred HImiy"); first done. iIntros (zs'); iDestruct 1 as (Hzs) "HIC"; simplify_eq/=. `````` Robbert Krebbers committed Jul 05, 2019 266 267 268 `````` iApply ("HΦ" \$! (zs' ++ red i ys)). iSplit; last by rewrite -assoc_L. iPureIntro. rewrite (gmultiset_disj_union_difference {[ i,ys ]} Y) -?gmultiset_elem_of_singleton_subseteq //. `````` Robbert Krebbers committed Sep 17, 2019 269 `````` rewrite (comm_L disj_union) gmultiset_elements_disj_union. `````` Robbert Krebbers committed Jul 05, 2019 270 271 272 273 `````` rewrite gmultiset_elements_singleton assoc_L Hzs !bind_app /=. by rewrite right_id_L !assoc_L. Qed. `````` Robbert Krebbers committed Jul 10, 2019 274 275 `````` Lemma par_map_reduce_spec n m vmap vred l xs : 0 < n → 0 < m → `````` Robbert Krebbers committed Jul 06, 2019 276 277 `````` map_spec IA IZB map vmap -∗ map_spec IZBs IC (curry red) vred -∗ `````` Robbert Krebbers committed Jul 08, 2019 278 `````` {{{ llist IA l xs }}} `````` Robbert Krebbers committed Jul 10, 2019 279 `````` par_map_reduce #n #m vmap vred #l `````` Robbert Krebbers committed Jul 09, 2019 280 `````` {{{ zs, RET #(); ⌜zs ≡ₚ map_reduce map red xs⌝ ∗ llist IC l zs }}}. `````` Robbert Krebbers committed Jul 05, 2019 281 `````` Proof. `````` Robbert Krebbers committed Jul 10, 2019 282 `````` iIntros (??) "#Hmap #Hred !>"; iIntros (Φ) "Hl HΦ". wp_lam; wp_pures. `````` Robbert Krebbers committed Jul 10, 2019 283 `````` wp_apply (start_chan_proto_spec (par_map_protocol IA IZB map n ∅)); `````` Robbert Krebbers committed Jul 09, 2019 284 285 `````` iIntros (cmap) "// Hcmap". { wp_pures. wp_apply (par_map_service_spec with "Hmap Hcmap"); auto. } `````` Robbert Krebbers committed Jul 10, 2019 286 `````` wp_apply (start_chan_proto_spec (sort_fg_protocol IZB RZB <++> END)%proto); `````` Robbert Krebbers committed Jul 05, 2019 287 `````` iIntros (csort) "Hcsort". `````` Robbert Krebbers committed Jul 10, 2019 288 `````` { wp_apply (sort_service_fg_spec with "[] Hcsort"); last by auto. `````` Robbert Krebbers committed Jul 05, 2019 289 290 `````` iApply RZB_cmp_spec. } rewrite right_id. `````` Robbert Krebbers committed Jul 09, 2019 291 `````` wp_apply (par_map_reduce_map_spec with "[\$Hl \$Hcmap \$Hcsort]"); first lia. `````` Robbert Krebbers committed Jul 05, 2019 292 `````` iIntros (iys). rewrite gmultiset_elements_empty right_id_L. `````` Robbert Krebbers committed Jul 09, 2019 293 `````` iDestruct 1 as (Hiys) "[Hl Hcsort] /=". wp_select; wp_pures; simpl. `````` Robbert Krebbers committed Jul 10, 2019 294 `````` wp_apply (start_chan_proto_spec (par_map_protocol IZBs IC (curry red) m ∅)); `````` Robbert Krebbers committed Jul 09, 2019 295 296 `````` iIntros (cred) "// Hcred". { wp_pures. wp_apply (par_map_service_spec with "Hred Hcred"); auto. } `````` Robbert Krebbers committed Jul 05, 2019 297 `````` wp_branch as %_|%Hnil; last first. `````` Robbert Krebbers committed Jul 09, 2019 298 `````` { wp_pures. iApply ("HΦ" \$! [] with "[\$Hl]"); simpl. `````` Robbert Krebbers committed Jul 05, 2019 299 300 `````` by rewrite /map_reduce /= -Hiys -Hnil. } wp_recv ([i y] ?) as (_ w ->) "HIB /="; wp_pures. `````` Robbert Krebbers committed Jul 09, 2019 301 302 `````` wp_apply (par_map_reduce_reduce_spec _ _ [] (Some (i, y, w)) [] with "[\$Hl \$Hcsort \$Hcred \$HIB]"); simpl; auto; [lia|set_solver|]. `````` Robbert Krebbers committed Jul 08, 2019 303 304 305 `````` iIntros (zs). rewrite /= gmultiset_elements_empty !right_id. iDestruct 1 as (Hzs) "Hk". wp_pures. iApply ("HΦ" with "[\$Hk]"). by rewrite Hzs Hiys. `````` Robbert Krebbers committed Jul 05, 2019 306 307 `````` Qed. End mapper.``````