proposition: Theorem lb_step_failure_tot_mapped_simulation_1 : forall net net' failed failed' lb tr, @lb_step_failure _ labeled_multi_fst (failed, net) lb (failed', net') tr -> @lb_step_failure _ labeled_multi_snd (List.map tot_map_name failed, tot_map_net net) (tot_map_label lb) (List.map tot_map_name failed', tot_map_net net') (List.map tot_map_trace_occ 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 => //=. - have ->: tot_map_name (pDst p) = pDst (tot_map_packet p) by destruct p. apply: (@LabeledStepFailure_deliver _ _ _ _ _ _ (List.map tot_map_packet xs) (List.map tot_map_packet ys) (List.map tot_map_output out) (tot_map_data d) (@tot_map_name_msgs _ _ _ _ _ msg_map l)). * rewrite /tot_map_net /=. find_rewrite. by rewrite map_app. * destruct p. simpl in *. exact: not_in_failed_not_in. * destruct p. simpl in *. rewrite tot_map_name_inv_inverse. have H_q := @tot_net_handlers_eq _ _ _ _ _ _ _ multi_map_congr pDst pSrc pBody (nwState net pDst). 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 /tot_map_net /= 2!map_app -(@tot_map_update_packet_eq _ _ _ _ _ _ _ name_map_bijective). destruct p. by rewrite tot_map_packet_map_eq. - apply: (@LabeledStepFailure_input _ _ _ _ _ _ _ _ (tot_map_data d) (tot_map_name_msgs l)). * exact: not_in_failed_not_in. * rewrite /tot_map_net /= tot_map_name_inv_inverse. have H_q := @tot_input_handlers_eq _ _ _ _ _ _ _ multi_map_congr h inp (nwState net h). 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. * by rewrite /tot_map_net /= map_app tot_map_packet_map_eq -(@tot_map_update_eq _ _ _ _ _ _ name_map_bijective). - rewrite tot_lb_label_silent_fst_snd. exact: LabeledStepFailure_stutter. Qed.
imports: Verdi(Verdi LabeledNet TotalMapSimulations) InfSeqExt(infseq map exteq) Coq(FunctionalExtensionality) Verdi(Ssrexport)