proposition: Theorem lb_step_ordered_dynamic_failure_tot_mapped_simulation_1 : forall net net' failed failed' lb tr, @lb_step_ordered_dynamic_failure _ labeled_multi_fst (failed, net) lb (failed', net') tr -> @lb_step_ordered_dynamic_failure _ labeled_multi_snd (List.map tot_map_name failed, tot_map_odnet net) (tot_map_label lb) (List.map tot_map_name failed', tot_map_odnet net') (List.map tot_map_trace tr).
proof: Proof. Proof using name_map_bijective multi_map_lb_congr multi_map_congr. move => net net' failed failed' lb tr H_step. invcs H_step => //=. - rewrite /tot_map_odnet /=. apply (@LabeledStepOrderedDynamicFailure_deliver _ _ _ _ _ _ (@tot_map_msg _ _ _ _ msg_map m) (List.map (@tot_map_msg _ _ _ _ msg_map) ms) (List.map tot_map_output out) (tot_map_data d) (tot_map_data d') (@tot_map_name_msgs _ _ _ _ _ msg_map l) (@tot_map_name _ _ _ _ name_map from) (@tot_map_name _ _ _ _ name_map to)) => //=. * exact: not_in_failed_not_in. * exact: in_failed_in. * rewrite tot_map_name_inv_inverse. by find_rewrite. * rewrite 2!tot_map_name_inv_inverse. by find_rewrite. * have H_q := @tot_net_handlers_eq _ _ _ _ _ _ _ multi_map_congr to from m d. rewrite /tot_mapped_net_handlers /net_handlers /= /unlabeled_net_handlers in H_q. repeat break_let. repeat tuple_inversion. have H_q' := @tot_lb_net_handlers_eq _ _ _ _ _ _ _ _ multi_map_lb_congr _ _ _ _ _ _ _ _ Heqp1. rewrite /tot_mapped_lb_net_handlers_label in H_q'. repeat break_let. by repeat tuple_inversion. * rewrite (@collate_tot_map_update2_eq _ _ _ _ _ _ name_map_bijective). set f1 := fun _ => match _ with _ => _ end. set f2 := update _ _ _ _. have H_eq_f: f1 = f2. rewrite /f1 /f2 /update. apply functional_extensionality => dst. repeat break_if => //=; first by rewrite -e tot_map_name_inverse_inv in n. by rewrite e tot_map_name_inv_inverse in n. by rewrite H_eq_f. * by rewrite (@map_tot_map_trace_eq _ _ _ _ _ name_map). - rewrite /tot_map_odnet /=. apply (@LabeledStepOrderedDynamicFailure_input _ _ (@tot_map_name _ _ _ _ name_map h) _ _ _ _ (List.map tot_map_output out) (tot_map_input inp) (tot_map_data d) (tot_map_data d') (@tot_map_name_msgs _ _ _ _ _ msg_map l)) => //=. * exact: not_in_failed_not_in. * exact: in_failed_in. * rewrite tot_map_name_inv_inverse. by find_rewrite. * have H_q := @tot_input_handlers_eq _ _ _ _ _ _ _ multi_map_congr h inp d. rewrite /tot_mapped_input_handlers /= /unlabeled_input_handlers in H_q. repeat break_let. repeat tuple_inversion. have H_q' := @tot_lb_input_handlers_eq _ _ _ _ _ _ _ _ multi_map_lb_congr _ _ _ _ _ _ _ Heqp1. rewrite /tot_mapped_lb_input_handlers_label in H_q'. repeat break_let. by repeat tuple_inversion. * rewrite (@collate_tot_map_eq _ _ _ _ _ _ name_map_bijective). set f1 := fun _ => match _ with _ => _ end. set f2 := update _ _ _ _. have H_eq_f: f1 = f2. rewrite /f1 /f2 /update. apply functional_extensionality => n. repeat break_match; try by congruence. * by rewrite e tot_map_name_inv_inverse in n0. * by rewrite -e tot_map_name_inverse_inv in n0. * by rewrite e tot_map_name_inv_inverse in n0. by rewrite H_eq_f. * by rewrite (@map_tot_map_trace_eq _ _ _ _ _ name_map). - rewrite tot_lb_label_silent_fst_snd. exact: LabeledStepOrderedDynamicFailure_stutter. Qed.
imports: Verdi(Verdi LabeledNet TotalMapSimulations) InfSeqExt(infseq map exteq) Coq(FunctionalExtensionality) Verdi(Ssrexport)