proposition: Theorem lb_step_failure_pt_mapped_simulation_1_non_silent : forall net net' failed failed' lb tr, tot_map_label lb <> label_silent -> @lb_step_failure _ labeled_multi_fst (failed, net) lb (failed', net') tr -> @lb_step_failure _ labeled_multi_snd (List.map tot_map_name failed, pt_map_net net) (tot_map_label lb) (List.map tot_map_name failed', pt_map_net net') (filterMap pt_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_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 => //=. - destruct (pt_map_packet p) eqn:?; last first. destruct p. simpl in *. break_match => //. have H_q := @pt_lb_net_handlers_none _ _ _ _ _ _ _ _ multi_map_lb_congr pDst pSrc _ (nwState net pDst) Heqo0. rewrite /tot_mapped_lb_net_handlers_label in H_q. repeat break_let. by tuple_inversion. have H_eq_n: tot_map_name (pDst p) = pDst p0. destruct p. simpl in *. break_match => //. by find_injection. rewrite H_eq_n. apply (@LabeledStepFailure_deliver _ _ _ _ _ _ (filterMap pt_map_packet xs) (filterMap pt_map_packet ys) (filterMap pt_map_output out) (pt_map_data d) (filterMap (@pt_map_name_msg _ _ _ _ _ msg_map) l)). * rewrite /pt_map_net /=. find_rewrite. by rewrite filterMap_app /= Heqo. * rewrite -H_eq_n. exact: not_in_failed_not_in. * rewrite /pt_map_net /= -{2}H_eq_n tot_map_name_inv_inverse. destruct p, p0. simpl in *. break_match => //. find_injection. clean. have H_q := @pt_net_handlers_some _ _ _ _ _ _ _ multi_map_congr pDst pSrc pBody (nwState net pDst) _ Heqo0. 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 _ _ _ _ _ _ _ _ _ Heqo0 Heqp1. rewrite /tot_mapped_lb_net_handlers_label in H_q'. repeat break_let. break_and. by repeat tuple_inversion. * rewrite /pt_map_net /= 2!filterMap_app. by rewrite (filterMap_pt_map_packet_map_eq_some _ _ Heqo) (pt_map_update_eq_some _ _ _ Heqo). - case H_i: pt_map_input => [inp'|]; last first. have H_q := @pt_lb_input_handlers_none _ _ _ _ _ _ _ _ multi_map_lb_congr h _ (nwState net h) H_i. rewrite /tot_mapped_lb_input_handlers_label /= in H_q. repeat break_let. by tuple_inversion. apply (@LabeledStepFailure_input _ _ _ _ _ _ _ _ (pt_map_data d) (filterMap (@pt_map_name_msg _ _ _ _ _ msg_map) l)). * exact: not_in_failed_not_in. * have H_q := @pt_input_handlers_some _ _ _ _ _ _ _ multi_map_congr h _ (nwState 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. break_and. unfold tot_mapped_lb_input_handlers_label in *. repeat break_let. repeat tuple_inversion. by rewrite /pt_map_net /= tot_map_name_inv_inverse. * rewrite /pt_map_net /=. rewrite filterMap_app filterMap_pt_map_packet_map_eq. by rewrite -(@pt_map_update_eq _ _ _ _ _ _ name_map_bijective). Qed.
imports: Verdi(Verdi LabeledNet) Verdi(TotalMapSimulations PartialMapSimulations) Verdi(TotalMapExecutionSimulations) InfSeqExt(infseq map exteq) Coq(FunctionalExtensionality) Verdi(Ssrexport) Coq(ssrbool)