proposition: Theorem lb_step_ordered_failure_pt_mapped_simulation_1_non_silent : forall net net' failed failed' lb tr, tot_map_label lb <> label_silent -> @lb_step_ordered_failure _ labeled_multi_fst (failed, net) lb (failed', net') tr -> @lb_step_ordered_failure _ labeled_multi_snd (List.map tot_map_name failed, pt_map_onet net) (tot_map_label lb) (List.map tot_map_name failed', pt_map_onet net') (filterMap pt_map_trace_ev tr).
proof: Proof. Proof using name_map_bijective multi_map_lb_congr multi_map_congr. move => net net' failed failed' lb tr H_neq H_step. have H_neq': lb <> label_silent. rewrite -pt_lb_label_silent_fst_snd in H_neq. move => H_eq. by rewrite H_eq in H_neq. invcs H_step => //=. - rewrite {2}/pt_map_onet /=. case H_m: (@pt_map_msg _ _ _ _ msg_map m) => [m'|]; last first. have H_q := @pt_lb_net_handlers_none _ _ _ _ _ _ _ _ multi_map_lb_congr to from _ (onwState net to) H_m. rewrite /tot_mapped_lb_net_handlers_label in H_q. repeat break_let. by tuple_inversion. apply (@LabeledStepOrderedFailure_deliver _ _ _ _ _ _ m' (filterMap (@pt_map_msg _ _ _ _ msg_map) ms) (filterMap pt_map_output out) (pt_map_data d) (filterMap (@pt_map_name_msg _ _ _ _ _ msg_map) l) (@tot_map_name _ _ _ _ name_map from) (@tot_map_name _ _ _ _ name_map to)). * by rewrite /= 2!tot_map_name_inv_inverse /= H3 /= H_m. * exact: not_in_failed_not_in. * rewrite /pt_map_onet /= tot_map_name_inv_inverse. have H_q := @pt_net_handlers_some _ _ _ _ _ _ _ multi_map_congr to from m (onwState net to) _ H_m. rewrite /pt_mapped_net_handlers /net_handlers /= /unlabeled_net_handlers in H_q. repeat break_let. repeat tuple_inversion. have H_q' := @pt_lb_net_handlers_some _ _ _ _ _ _ _ _ multi_map_lb_congr _ _ _ _ _ _ _ _ _ H_m Heqp1. rewrite /tot_mapped_lb_net_handlers_label in H_q'. repeat break_let. break_and. by repeat tuple_inversion. * rewrite (@collate_pt_map_update2_eq _ _ _ _ name_map). set f1 := fun _ => pt_map_data _. set f2 := update _ _ _ _. have H_eq_f: f1 = f2. rewrite /f1 /f2. apply functional_extensionality => n. rewrite /update. break_if; break_if => //=; first 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 -filterMap_pt_map_trace_ev_outputs_eq. - rewrite {2}/pt_map_onet /=. case H_i: pt_map_input => [inp'|]; last first. have H_q := @pt_lb_input_handlers_none _ _ _ _ _ _ _ _ multi_map_lb_congr h inp (onwState net h) H_i. rewrite /tot_mapped_lb_input_handlers_label in H_q. repeat break_let. by tuple_inversion. apply (@LabeledStepOrderedFailure_input _ _ (@tot_map_name _ _ _ _ name_map h) _ _ _ _ (filterMap pt_map_output out) inp' (pt_map_data d) (filterMap (@pt_map_name_msg _ _ _ _ _ msg_map) l)). * exact: not_in_failed_not_in. * rewrite /pt_map_onet /= tot_map_name_inv_inverse. have H_q := @pt_input_handlers_some _ _ _ _ _ _ _ multi_map_congr h inp (onwState net h) _ H_i. rewrite /pt_mapped_input_handlers /input_handlers /= /unlabeled_input_handlers in H_q. repeat break_let. repeat tuple_inversion. have H_q' := @pt_lb_input_handlers_some _ _ _ _ _ _ _ _ multi_map_lb_congr _ _ _ _ _ _ _ _ H_i Heqp1. rewrite /tot_mapped_lb_input_handlers_label in H_q'. repeat break_let. break_and. by repeat tuple_inversion. * rewrite {2}/pt_map_onet /=. rewrite (@collate_pt_map_eq _ _ _ _ name_map). set f1 := fun _ => pt_map_data _. set f2 := update _ _ _ _. have H_eq_f: f1 = f2. rewrite /f1 /f2. apply functional_extensionality => n. rewrite /update. break_if; break_if => //=; first 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 -(@filterMap_pt_map_trace_ev_outputs_eq _ _ _ _ _ name_map out h). Qed.
imports: Verdi(Verdi LabeledNet) Verdi(TotalMapSimulations PartialMapSimulations) Verdi(TotalMapExecutionSimulations) InfSeqExt(infseq map exteq) Coq(FunctionalExtensionality) Verdi(Ssrexport) Coq(ssrbool)