proposition: Theorem step_async_pt_mapped_simulation_1 : forall net net' tr, @step_async _ multi_fst net net' tr -> @step_async _ multi_snd (pt_map_net net) (pt_map_net net') (filterMap pt_map_trace_occ tr) \/ (pt_map_net net' = pt_map_net net /\ filterMap trace_non_empty_out (filterMap pt_map_trace_occ tr) = []).
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'. rewrite /=. case H_m: (pt_map_packet p) => [p'|]. have ->: tot_map_name (pDst p) = pDst p'. case: p H_eq H_hnd H_eq' H_m => /= src dst m H_eq H_hnd H_eq'. case (pt_map_msg m) => //= m' H_m. by inversion H_m. left. rewrite H_eq' /=. apply (@StepAsync_deliver _ _ _ _ _ (filterMap pt_map_packet ms) (filterMap pt_map_packet ms') (filterMap pt_map_output out) (pt_map_data d) (filterMap pt_map_name_msg l)). * rewrite /= H_eq filterMap_app /=. case H_p: (pt_map_packet _) => [p0|]. rewrite H_p in H_m. by injection H_m => H_eq_p; rewrite H_eq_p. by rewrite H_p in H_m. * rewrite /=. case: p H_eq H_hnd H_eq' H_m => /= src dst m H_eq H_hnd H_eq'. case H_m: (pt_map_msg m) => [m'|] //. case: p' H_eq' => src' dst' m0 H_eq' H_eq_p. inversion H_eq_p; subst. rewrite /= {H_eq_p}. have H_q := pt_net_handlers_some dst src m (nwState net dst) H_m. rewrite /pt_mapped_net_handlers in H_q. rewrite H_hnd in H_q. rewrite H_q. by rewrite tot_map_name_inv_inverse. * rewrite /= /pt_map_net /= 2!filterMap_app. by rewrite (filterMap_pt_map_packet_map_eq_some _ _ H_m) (pt_map_update_eq_some _ _ _ H_m). right. split. * rewrite H_eq' {H_eq'}. rewrite /pt_map_net /=. case: p H_eq H_hnd H_m => /= src dst m H_eq H_hnd. case H_m: (pt_map_msg _) => [m'|] // 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 H_o]] := pt_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_eq'}. case: p H_eq H_hnd H_m => /= src dst m H_eq H_hnd. case H_m: (pt_map_msg _) => [m'|] // H_eq'. have [H_d [H_l H_o]] := pt_net_handlers_none _ _ _ _ H_m H_hnd. by rewrite H_o. - move => h net net' out inp d l H_hnd H_eq. rewrite /=. case H_i: (pt_map_input inp) => [inp'|]. left. apply (@StepAsync_input _ _ _ _ _ _ _ (pt_map_data d) (filterMap pt_map_name_msg l)). rewrite /=. have H_q := pt_input_handlers_some h inp (nwState net h) H_i. rewrite /pt_mapped_input_handlers /= in H_q. rewrite H_hnd in H_q. rewrite H_q. by rewrite tot_map_name_inv_inverse. rewrite /= H_eq /= /pt_map_net /=. rewrite -filterMap_pt_map_packet_map_eq filterMap_app. by rewrite -pt_map_update_eq. right. split. * rewrite H_eq /pt_map_net /=. have [H_d [H_l H_o]] := pt_input_handlers_none _ _ _ H_i 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. * rewrite /=. have [H_d [H_l H_o]] := pt_input_handlers_none _ _ _ H_i H_hnd. by rewrite H_o. Qed.
imports: Verdi(Verdi DynamicNetLemmas TotalMapSimulations) Coq(FunctionalExtensionality) Coq(Sumbool Sorting.Permutation) Verdi(DynamicNetLemmas) Verdi(Ssrexport)