proposition: Theorem lb_step_ordered_dynamic_failure_pt_mapped_simulation_1_silent : forall net net' failed failed' lb tr, tot_map_label lb = label_silent -> @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, pt_map_odnet net) label_silent (List.map tot_map_name failed', pt_map_odnet 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_eq H_step. invcs H_step => //=. - rewrite {2}/pt_map_odnet /=. case H_m: (@pt_map_msg _ _ _ _ msg_map m) => [m'|]. have H_q := @pt_net_handlers_some _ _ _ _ _ _ _ multi_map_congr to from m d _ 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. break_and. unfold tot_mapped_lb_net_handlers_label in *. repeat break_let. by repeat tuple_inversion. have H_q := @pt_net_handlers_none _ _ _ _ _ _ _ multi_map_congr to from m d out d' l H_m. rewrite /net_handlers /= /unlabeled_net_handlers in H_q. repeat break_let. repeat tuple_inversion. concludes. break_and. have H_q' := @pt_lb_net_handlers_none _ _ _ _ _ _ _ _ multi_map_lb_congr to from _ d H_m. rewrite /tot_mapped_lb_net_handlers_label in H_q'. repeat break_let. repeat tuple_inversion. rewrite /pt_map_odnet /=. rewrite (@collate_pt_map_update2_eq _ _ _ _ name_map) /=. rewrite H0 /=. set p1 := fun _ _ => _. set p2 := update2 _ _ _ _ _. set s1 := fun _ => _. set s2 := fun _ => _. have H_eq_p: p1 = p2. rewrite /p1 /p2 /update2. apply functional_extensionality => src. apply functional_extensionality => dst. break_if => //. break_and. by rewrite -H2 -H7 2!tot_map_name_inv_inverse H6 /= H_m. have H_eq_s: s1 = s2. rewrite /s1 /s2 /update. apply functional_extensionality => n. break_if => //. by rewrite e H5 H. rewrite H_eq_p H_eq_s. split; first exact: LabeledStepOrderedDynamicFailure_stutter. rewrite (@filterMap_pt_map_trace_ev_outputs_eq _ _ _ _ _ name_map). by repeat find_rewrite. - case H_i: (pt_map_input inp) => [inp'|]. have H_q := @pt_input_handlers_some _ _ _ _ _ _ _ multi_map_congr h _ d _ 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. break_and. unfold tot_mapped_lb_input_handlers_label in *. repeat break_let. by tuple_inversion. have H_q := @pt_input_handlers_none _ _ _ _ _ _ _ multi_map_congr h _ d out d' l H_i. rewrite /input_handlers /= /unlabeled_input_handlers in H_q. repeat break_let. repeat tuple_inversion. concludes. break_and. have H_q' := @pt_lb_input_handlers_none _ _ _ _ _ _ _ _ multi_map_lb_congr h _ d H_i. rewrite /tot_mapped_lb_input_handlers_label in H_q'. repeat break_let. repeat tuple_inversion. rewrite /pt_map_odnet /=. rewrite (@collate_pt_map_eq _ _ _ _ name_map) H0 /=. set s1 := fun _ => match _ with _ => _ end. set s2 := fun _ => match _ with _ => _ end. have H_eq_s: s1 = s2. rewrite /s1 /s2. apply functional_extensionality => n. rewrite /update. by break_if; first by rewrite e H5 H. rewrite -H_eq_s /s1 {s1 s2 H_eq_s}. split; first exact: LabeledStepOrderedDynamicFailure_stutter. rewrite (@filterMap_pt_map_trace_ev_outputs_eq _ _ _ _ _ name_map). by repeat find_rewrite. - split => //; exact: LabeledStepOrderedDynamicFailure_stutter. Qed.
imports: Verdi(Verdi LabeledNet) Verdi(TotalMapSimulations PartialMapSimulations) Verdi(TotalMapExecutionSimulations) InfSeqExt(infseq map exteq) Coq(FunctionalExtensionality) Verdi(Ssrexport) Coq(ssrbool)