proposition: Theorem step_ordered_pt_mapped_simulation_1 : forall net net' tr, @step_ordered _ multi_fst net net' tr -> @step_ordered _ multi_snd (pt_map_onet net) (pt_map_onet net') (filterMap pt_map_trace_ev tr) \/ pt_map_onet net' = pt_map_onet net /\ filterMap pt_map_trace_ev tr = [].
proof: Proof. Proof using name_map_bijective multi_map_congr. move => net net' tr. case => {net net' tr}. - move => net net' tr m ms out d l from to H_eq H_hnd H_eq' H_eq_tr. destruct (pt_map_msg m) eqn:?. left. rewrite H_eq' /= /pt_map_onet /=. apply (@StepOrdered_deliver _ _ _ _ _ m0 (filterMap pt_map_msg ms) (filterMap pt_map_output out) (pt_map_data d) (filterMap pt_map_name_msg l) (tot_map_name from) (tot_map_name to)). * rewrite /= 2!tot_map_name_inv_inverse H_eq /=. destruct (pt_map_msg _) eqn:?; last by congruence. by find_injection. * rewrite /= tot_map_name_inv_inverse. rewrite -(pt_net_handlers_some _ _ _ _ Heqo). rewrite /pt_mapped_net_handlers /=. repeat break_let. by inversion H_hnd. * by rewrite /= pt_map_update_eq collate_pt_map_update2_eq. * by rewrite H_eq_tr /= filterMap_pt_map_trace_ev_outputs_eq. right. rewrite /=. have [H_eq_d [H_ms H_out]] := pt_net_handlers_none _ _ _ _ Heqo H_hnd. rewrite H_eq_tr filterMap_pt_map_trace_ev_outputs_eq H_out /=. split => //. rewrite H_eq' /pt_map_onet /=. rewrite pt_map_update_eq /= H_eq_d. rewrite collate_pt_map_eq H_ms /=. set nwS1 := update _ _ _ _. set nwS2 := fun n => pt_map_data _. set nwP1 := fun _ _ => _. set nwP2 := fun _ _ => _. have H_eq_s: nwS1 = nwS2. rewrite /nwS1 /nwS2 {nwS1 nwS2}. apply functional_extensionality => n. rewrite /update /=. case (name_eq_dec _ _) => H_dec //. by rewrite H_dec tot_map_name_inv_inverse. have H_eq_p: nwP1 = nwP2. rewrite /nwP1 /nwP2 /=. apply functional_extensionality => src. apply functional_extensionality => dst. rewrite /update2 /=. case (sumbool_and _ _ _ _) => H_dec //. move: H_dec => [H_eq_from H_eq_to]. rewrite -H_eq_from -H_eq_to H_eq /=. case H_m': (pt_map_msg _) => [m'|] //. by rewrite H_m' in Heqo. by rewrite H_eq_s H_eq_p. - move => h net net' tr out inp d l H_hnd H_eq H_eq_tr. destruct (pt_map_input inp) eqn:?. left. apply (@StepOrdered_input _ _ (tot_map_name h) _ _ _ (filterMap pt_map_output out) i (pt_map_data d) (filterMap pt_map_name_msg l)). * rewrite /=. have H_q := pt_input_handlers_some h inp (onwState net h) Heqo. rewrite /pt_mapped_input_handlers /= in H_q. rewrite H_hnd in H_q. rewrite H_q. by rewrite tot_map_name_inv_inverse. * by rewrite H_eq /pt_map_onet /= pt_map_update_eq collate_pt_map_eq. * by rewrite H_eq_tr /= Heqo filterMap_pt_map_trace_ev_outputs_eq. right. rewrite /=. have [H_d [H_l H_o]] := pt_input_handlers_none h inp (onwState net h) Heqo H_hnd. rewrite H_eq_tr /= filterMap_pt_map_trace_ev_outputs_eq Heqo H_o /=. split => //. rewrite H_eq /= /pt_map_onet /=. rewrite pt_map_update_eq /= H_d. rewrite collate_pt_map_eq H_l /=. set nwS1 := update _ _ _ _. set nwS2 := fun n => pt_map_data _. have H_eq_n: nwS1 = nwS2. rewrite /nwS1 /nwS2 /=. apply functional_extensionality => n. rewrite /update /=. case (name_eq_dec _ _) => H_dec //. by rewrite H_dec tot_map_name_inv_inverse. by rewrite H_eq_n. Qed.
imports: Verdi(Verdi DynamicNetLemmas TotalMapSimulations) Coq(FunctionalExtensionality) Coq(Sumbool Sorting.Permutation) Verdi(DynamicNetLemmas) Verdi(Ssrexport)