proposition: Theorem step_ordered_dynamic_failure_pt_ext_mapped_simulation_1 : forall net net' failed failed' tr, NoDup (odnwNodes net) -> @step_ordered_dynamic_failure _ _ overlay_fst new_msg_fst fail_msg_fst (failed, net) (failed', net') tr -> (exists tr', @step_ordered_dynamic_failure _ _ overlay_snd new_msg_snd fail_msg_snd (map tot_map_name failed, pt_ext_map_odnet net) (map tot_map_name failed', pt_ext_map_odnet net') tr') \/ (pt_ext_map_odnet net' = pt_ext_map_odnet net /\ failed = failed').
proof: Proof. Proof using overlay_map_congr new_msg_map_congr name_map_bijective multi_map_congr fail_msg_map_congr. move => net net' failed failed' tr H_nd H_step. invcs H_step. - left. rewrite /pt_ext_map_odnet. exists []. apply (@StepOrderedDynamicFailure_start _ _ _ _ _ _ _ _ (tot_map_name h)) => /=; first exact: not_in_failed_not_in. set p1 := fun _ _ => _. set p2 := collate_ls _ _ _ _ _. set s1 := fun _ => _. set s2 := update _ _ _ _. have H_eq_s: s1 = s2. rewrite /s1 /s2 /update {s1 s2}. apply functional_extensionality => n. rewrite -pt_ext_init_handlers_eq. break_match_goal. break_if; break_if; try by congruence. - by repeat find_rewrite; repeat find_rewrite_lem tot_map_name_inv_inverse. - by find_reverse_rewrite; find_rewrite_lem tot_map_name_inverse_inv. - by find_rewrite. break_if; break_if; (try by congruence); last by find_rewrite. by repeat find_rewrite; repeat find_rewrite_lem tot_map_name_inv_inverse. rewrite H_eq_s /s2 {s1 s2 H_eq_s}. have H_eq_p: p1 = p2. rewrite /p1 /p2 {p1 p2}. rewrite (collate_ls_pt_map_eq _ _ _ _ pt_new_msg_fst_snd) /=. rewrite collate_pt_map_eq. set f1 := fun _ _ => _. set c1 := collate _ _ _ _. set c2 := collate _ _ _ _. set f'1 := map tot_map_name _. set f'2 := filter_rel _ (tot_map_name h) _. have H_c: c1 = c2. rewrite /c1 /c2 {c1 c2}. apply: NoDup_Permutation_collate_eq; last first. rewrite /pt_map_name_msg. apply: pt_nodup_perm_map_map_pair_perm => //. by rewrite pt_new_msg_fst_snd. rewrite /pt_map_name_msg /=. apply: NoDup_map_snd_fst => //. apply (@nodup_pt_map _ _ _ _ _ _ _ msg_new); first exact: in_map2snd_snd. apply: NoDup_map2snd. exact: NoDup_remove_all. move => nm nm' H_in H_in'. apply (@pt_map_in_snd _ _ _ _ _ _ _ msg_new _ _ _ _ pt_new_msg_fst_snd) in H_in. apply (@pt_map_in_snd _ _ _ _ _ _ _ msg_new _ _ _ _ pt_new_msg_fst_snd) in H_in'. by rewrite H_in H_in'. rewrite H_c {H_c}. suff H_suff: f'1 = f'2 by rewrite H_suff. rewrite /f'1 /f'2. elim (odnwNodes net) => /=; first by rewrite 2!remove_all_nil. move => n ns. set mn := tot_map_name n. set mns := map _ ns. set mfailed' := map _ failed'. move => IH. have H_cn := remove_all_cons name_eq_dec failed' n ns. have H_cn' := remove_all_cons name_eq_dec mfailed' mn mns. unfold mn, mns, mfailed' in *. repeat break_or_hyp; repeat break_and; repeat find_rewrite => //=. * by find_apply_lem_hyp not_in_failed_not_in. * by find_apply_lem_hyp in_failed_in. * case: adjacent_to_dec => H_dec; case adjacent_to_dec => H_dec' => //=. + by rewrite IH. + by find_apply_lem_hyp tot_adjacent_to_fst_snd. + by find_apply_lem_hyp tot_adjacent_to_fst_snd. by rewrite H_eq_p. - destruct (pt_map_msg m) eqn:?. left. destruct (net_handlers (tot_map_name to) (tot_map_name from) m0 (pt_ext_map_data d to)) eqn:?. destruct p as [out' d'']. exists (map2fst (tot_map_name to) (map inr out')). rewrite /pt_ext_map_onet /=. apply (@StepOrderedDynamicFailure_deliver _ _ _ _ _ _ _ _ _ m0 (filterMap pt_map_msg ms) out' (pt_ext_map_data d to) (pt_ext_map_data d' to) (filterMap pt_map_name_msg l) (tot_map_name from) (tot_map_name to)) => //=. * exact: not_in_failed_not_in. * exact: in_failed_in. * by rewrite /= tot_map_name_inv_inverse /= H5. * rewrite /= 2!tot_map_name_inv_inverse /=. find_rewrite. by rewrite /= Heqo. * 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. * rewrite /= /pt_ext_map_odnet /=. set u1 := fun _ => match _ with | _ => _ end. set u2 := update _ _ _ _. rewrite collate_pt_map_update2_eq. suff H_suff: u1 = u2 by rewrite H_suff. rewrite /u1 /u2 /update /=. apply functional_extensionality => n. repeat break_if; try by congruence. rewrite -(tot_map_name_inverse_inv n) in n0. by rewrite e in n0. find_rewrite. by find_rewrite_lem tot_map_name_inv_inverse. right. split => //. have [H_eq_d H_ms] := pt_ext_net_handlers_none _ _ _ _ Heqo H7. rewrite /pt_ext_map_odnet /= collate_pt_map_update2_eq H_ms /=. set nwP1 := update2 _ _ _ _ _. set nwS1 := fun _ => match _ with _ => _ end. set nwP2 := fun _ _ => _. set nwS2 := fun _ => _. have H_eq_s: nwS1 = nwS2. rewrite /nwS1 /nwS2 {nwS1 nwS2}. apply functional_extensionality => n. rewrite /update /=. break_if => //. find_rewrite. rewrite H5. by congruence. have H_eq_p: nwP1 = nwP2. rewrite /nwP1 /nwP2 /=. apply functional_extensionality => src. apply functional_extensionality => dst. rewrite /update2 /=. break_if => //. break_and. by rewrite -H -H0 2!tot_map_name_inv_inverse H6 /= Heqo. by rewrite H_eq_s H_eq_p. - destruct (pt_ext_map_input inp h d) eqn:?. left. destruct (input_handlers (tot_map_name h) i (pt_ext_map_data d h)) eqn:?. destruct p as [out' d'']. exists ((tot_map_name h, inl i) :: map2fst (tot_map_name h) (map inr out')). apply (@StepOrderedDynamicFailure_input _ _ _ _ _ (tot_map_name h) _ _ _ _ out' i (pt_ext_map_data d h) (pt_ext_map_data d' h) (filterMap pt_map_name_msg l)) => //=. * exact: not_in_failed_not_in. * exact: in_failed_in. * by rewrite /pt_ext_map_odnet /= tot_map_name_inv_inverse H5. * have H_q := @pt_ext_input_handlers_some _ _ _ _ _ _ _ multi_map_congr h inp d _ _ _ _ Heqo Heqp. rewrite /pt_ext_mapped_input_handlers /= in H_q. find_rewrite. by repeat tuple_inversion. * rewrite /= /pt_ext_map_odnet /= collate_pt_map_eq. set u1 := fun _ => match _ with | _ => _ end. set u2 := update _ _ _ _. suff H_suff: u1 = u2 by rewrite H_suff. rewrite /u1 /u2 /update /=. apply functional_extensionality => n. repeat break_if; try by congruence. rewrite -(tot_map_name_inverse_inv n) in n0. by rewrite e in n0. find_rewrite. by find_rewrite_lem tot_map_name_inv_inverse. right. rewrite /= /pt_ext_map_odnet /=. have [H_d H_l] := pt_ext_input_handlers_none h inp d Heqo H6. split => //=. rewrite collate_pt_map_eq H_l /=. set nwS1 := fun n : name => match _ with | _ => _ end. set nwS2 := fun n : name => match _ with | _ => _ end. have H_eq_n: nwS1 = nwS2. rewrite /nwS1 /nwS2 /=. apply functional_extensionality => n. rewrite /update /=. break_if => //. by repeat find_rewrite. by rewrite H_eq_n. - left. rewrite /pt_ext_map_odnet /=. 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. exact: NoDup_remove_all. 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: StepOrderedDynamicFailure_fail => //. * exact: not_in_failed_not_in. * exact: in_failed_in. * rewrite /=. rewrite /l collate_pt_map_eq. have H_pm := pt_nodup_perm_map_map_pair_perm _ h failed H_nd (Permutation_refl (map tot_map_name (odnwNodes net))) pt_fail_msg_fst_snd. have H_pm' := H_pm _ _ _ _ name_map_bijective _ _ overlay_map_congr _ _ fail_msg_map_congr. have H_eq := NoDup_Permutation_collate_eq _ _ _ _ _ _ _ H_nd' H_pm'. by rewrite H_eq. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Verdi(TotalMapSimulations PartialMapSimulations) Coq(FunctionalExtensionality Sumbool) Coq(Sorting.Permutation) Verdi(Ssrexport)