proposition: Theorem step_ordered_failure_pt_ext_mapped_simulation_1 : forall net net' failed failed' tr, @step_ordered_failure _ _ overlay_fst fail_msg_fst (failed, net) (failed', net') tr -> (exists tr', @step_ordered_failure _ _ overlay_snd fail_msg_snd (map tot_map_name failed, pt_ext_map_onet net) (map tot_map_name failed', pt_ext_map_onet net') tr') \/ pt_ext_map_onet net' = pt_ext_map_onet net /\ failed = failed'.
proof: Proof. Proof using overlay_map_congr name_map_bijective multi_map_congr fail_msg_map_congr. move => net net' failed failed' tr H_step. invcs H_step. - destruct (pt_map_msg m) eqn:?. left. destruct (net_handlers (tot_map_name to) (tot_map_name from) m0 (pt_ext_map_data (onwState net to) to)) eqn:?. destruct p as [out' d']. exists (map2fst (tot_map_name to) (map inr out')). rewrite /pt_ext_map_onet /=. apply (@StepOrderedFailure_deliver _ _ _ _ _ _ _ _ m0 (filterMap pt_map_msg ms) out' (pt_ext_map_data d to) (filterMap pt_map_name_msg l) (tot_map_name from) (tot_map_name to)) => //=. * rewrite 2!tot_map_name_inv_inverse /= H3 /=. case H_m1: (pt_map_msg _) => [m1|]; last by rewrite Heqo in H_m1. rewrite Heqo in H_m1. by inversion H_m1. * exact: not_in_failed_not_in. * rewrite /= tot_map_name_inv_inverse. have H_q := @pt_ext_net_handlers_some _ _ _ _ _ _ _ multi_map_congr _ _ _ _ _ _ _ _ Heqo Heqp. rewrite /pt_ext_mapped_net_handlers /= in H_q. by repeat break_let; repeat tuple_inversion. * by rewrite /= pt_ext_map_update_eq collate_pt_map_update2_eq. right. split => //. have [H_eq_d H_ms] := pt_ext_net_handlers_none _ _ _ _ Heqo H5. rewrite /pt_ext_map_onet /= pt_ext_map_update_eq H_eq_d collate_pt_map_update2_eq H_ms /=. set nwP1 := update2 _ _ _ _ _. set nwS1 := update _ _ _ _. set nwP2 := fun _ _ => _. set nwS2 := 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 /= 2!tot_map_name_inv_inverse H3 /=. case H_m': (pt_map_msg _) => [m'|] //. by rewrite H_m' in Heqo. by rewrite H_eq_s H_eq_p. - destruct (pt_ext_map_input inp h (onwState net h)) eqn:?. left. destruct (input_handlers (tot_map_name h) i (pt_ext_map_data (onwState net h) h)) eqn:?. destruct p as [out' d']. exists ((tot_map_name h, inl i) :: map2fst (tot_map_name h) (map inr out')). apply (@StepOrderedFailure_input _ _ _ _ (tot_map_name h) _ _ _ _ out' i (pt_ext_map_data d h) (filterMap pt_map_name_msg l)) => //=. * exact: not_in_failed_not_in. * rewrite /= tot_map_name_inv_inverse. have H_q := @pt_ext_input_handlers_some _ _ _ _ _ _ _ multi_map_congr h inp (onwState net h) _ _ _ _ Heqo Heqp. rewrite /pt_ext_mapped_input_handlers /= in H_q. by repeat break_let; repeat tuple_inversion. * by rewrite /pt_ext_map_onet /= pt_ext_map_update_eq collate_pt_map_eq. right. rewrite /= /pt_ext_map_onet /=. have [H_d H_l] := pt_ext_input_handlers_none h inp (onwState net h) Heqo H4. split => //. rewrite pt_ext_map_update_eq /= H_d. rewrite collate_pt_map_eq H_l /=. set nwS1 := update _ _ _ _. set nwS2 := fun n => pt_ext_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. - left. rewrite /pt_ext_map_onet /=. set l := map2snd _ _. have H_nd: NoDup (map (fun nm => fst nm) (filterMap pt_map_name_msg l)). rewrite /pt_map_name_msg /=. rewrite /l {l}. apply NoDup_map_snd_fst. apply (@nodup_pt_map _ _ _ _ _ _ _ msg_fail); first exact: in_map2snd_snd. apply NoDup_map2snd. apply NoDup_remove_all. exact: no_dup_nodes. move => nm nm' H_in H_in'. by rewrite (pt_map_in_snd _ _ _ _ pt_fail_msg_fst_snd H_in) (pt_map_in_snd _ _ _ _ pt_fail_msg_fst_snd H_in'). exists []. apply: StepOrderedFailure_fail => //. * exact: not_in_failed_not_in. * rewrite /=. rewrite /l collate_pt_map_eq /pt_map_name_msg. by rewrite (NoDup_Permutation_collate_eq _ _ _ _ _ _ _ H_nd (pt_map_map_pair_eq msg_fail h failed pt_fail_msg_fst_snd)). Qed.
imports: Verdi(Verdi DynamicNetLemmas) Verdi(TotalMapSimulations PartialMapSimulations) Coq(FunctionalExtensionality Sumbool) Coq(Sorting.Permutation) Verdi(Ssrexport)