proposition: Theorem step_async_pt_ext_mapped_simulation_1 : forall net net' tr, @step_async _ multi_fst net net' tr -> (exists tr, @step_async _ multi_snd (pt_ext_map_net net) (pt_ext_map_net net') tr) \/ pt_ext_map_net net' = pt_ext_map_net net.
proof: Proof. Proof using name_map_bijective multi_map_congr. move => net net' tr. case => {net net' tr}. - move => net net' p ms ms' out d l H_eq H_hnd H_eq'. destruct (pt_map_packet p) eqn:?. left. rewrite H_eq' /= /pt_ext_map_net /=. have H_eq_dst: tot_map_name (pDst p) = pDst p0. case: p H_eq H_hnd H_eq' Heqo => /= src dst m H_eq H_hnd H_eq'. case (pt_map_msg m) => //= m' H_m. by inversion H_m. destruct (net_handlers (pDst p0) (pSrc p0) (pBody p0) (pt_ext_map_data (nwState net (pDst p)) (pDst p))) eqn:?. destruct p1 as [out' d']. exists [(pDst p0, inr out')]. apply @StepAsync_deliver with (xs := filterMap pt_map_packet ms) (ys := filterMap pt_map_packet ms') (d := pt_ext_map_data d (pDst p)) (l := filterMap pt_map_name_msg l). * rewrite /= H_eq filterMap_app /=. case H_p: (pt_map_packet _) => [p1|]; last by rewrite H_p in Heqo. by rewrite H_p in Heqo; injection Heqo => H_eq_p; rewrite H_eq_p. * rewrite /=. rewrite -{2}H_eq_dst tot_map_name_inv_inverse. case: p H_eq H_hnd H_eq' Heqo H_eq_dst Heqp1 => /= src dst mg H_eq H_hnd H_eq'. case H_m: (pt_map_msg mg) => [mg'|] //. case: p0 H_eq' => src' dst' m0 H_eq' H_eq_p. inversion H_eq_p; subst. move => H_eq_dst H_eq_n {H_eq_p H_eq_dst}. simpl in *. have H_q := @pt_ext_net_handlers_some _ _ _ _ _ _ _ multi_map_congr dst src mg (nwState net dst) _ _ _ _ H_m H_eq_n. rewrite /pt_ext_mapped_net_handlers in H_q. rewrite H_hnd in H_q. find_inversion. by rewrite tot_map_name_inv_inverse. * rewrite /= /pt_ext_map_net /= 2!filterMap_app. rewrite (filterMap_pt_map_packet_map_eq_some _ _ Heqo). by rewrite (pt_ext_map_update_eq_some _ _ _ Heqo). right. rewrite H_eq' /= {H_eq'}. rewrite /pt_ext_map_net /=. case: p H_eq H_hnd Heqo => /= src dst m H_eq H_hnd. case H_m: (pt_map_msg _) => [m'|] // H_eq' {H_eq'}. rewrite 2!filterMap_app H_eq filterMap_app /=. case H_m': (pt_map_msg _) => [m'|]; first by rewrite H_m' in H_m. have [H_d H_l] := pt_ext_net_handlers_none _ _ _ _ H_m H_hnd. rewrite (filterMap_pt_map_name_msg_empty_eq _ dst H_l) /=. set nwS1 := fun _ => _. set nwS2 := fun _ => _. have H_eq_s: nwS1 = nwS2. rewrite /nwS1 /nwS2 /=. apply functional_extensionality => n. rewrite /update /=. case: name_eq_dec => H_dec //. by rewrite H_dec H_d. by rewrite H_eq_s. - move => h net net' out inp d l H_hnd H_eq. destruct (pt_ext_map_input inp h (nwState net h)) eqn:?. left. destruct (input_handlers (tot_map_name h) i (pt_ext_map_data (nwState net h) h)) eqn:?. destruct p as [out' d']. exists [(tot_map_name h, inl i); (tot_map_name h, inr out')]. apply (@StepAsync_input _ _ _ _ _ _ _ (pt_ext_map_data d h) (filterMap pt_map_name_msg l)). rewrite /=. have H_q := @pt_ext_input_handlers_some _ _ _ _ _ _ _ multi_map_congr h inp (nwState net h) _ _ _ _ Heqo Heqp. rewrite /pt_ext_mapped_input_handlers /= in H_q. rewrite H_hnd in H_q. find_inversion. by rewrite tot_map_name_inv_inverse. rewrite /= H_eq /= /pt_ext_map_net /= filterMap_app filterMap_pt_map_packet_map_eq. by rewrite -pt_ext_map_update_eq. right. rewrite H_eq /pt_ext_map_net /=. have [H_d H_l] := pt_ext_input_handlers_none _ _ _ Heqo H_hnd. rewrite filterMap_app. rewrite (filterMap_pt_map_name_msg_empty_eq _ h H_l) /=. set nwS1 := fun _ => _. set nwS2 := fun _ => _. have H_eq_s: nwS1 = nwS2. rewrite /nwS1 /nwS2 /=. apply functional_extensionality => n. rewrite /update /=. case: name_eq_dec => H_dec //. by rewrite H_dec H_d. by rewrite H_eq_s. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Verdi(TotalMapSimulations PartialMapSimulations) Coq(FunctionalExtensionality Sumbool) Coq(Sorting.Permutation) Verdi(Ssrexport)