proposition: Theorem step_failure_pt_mapped_simulation_1 : forall net net' failed failed' tr, @step_failure _ _ fail_fst (failed, net) (failed', net') tr -> @step_failure _ _ fail_snd (map tot_map_name failed, pt_map_net net) (map tot_map_name failed', pt_map_net net') (filterMap pt_map_trace_occ tr) \/ (pt_map_net net' = pt_map_net net /\ failed = failed' /\ filterMap trace_non_empty_out (filterMap pt_map_trace_occ tr) = []).
proof: Proof. Proof using name_map_bijective multi_map_congr fail_map_congr. move => net net' failed failed' tr H_step. invcs H_step. - rewrite /=. case H_m: (pt_map_packet p) => [p'|]. destruct p, p'. simpl in *. move: H_m. case H_m: pt_map_msg => [m|] //. move => H_eq. find_inversion. left. rewrite /pt_map_net /= H3 filterMap_app /= H_m /= 2!filterMap_app {H3}. set p' := {| pSrc := _ ; pDst := _ ; pBody := _ |}. have ->: tot_map_name pDst = Net.pDst p' by []. apply (@StepFailure_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 l)) => //=. * exact: not_in_failed_not_in. * rewrite /= -(pt_net_handlers_some _ _ _ _ H_m) /pt_mapped_net_handlers /= tot_map_name_inv_inverse. repeat break_let. by find_inversion. * pose p := {| pSrc := pSrc ; pDst := pDst ; pBody := pBody |}. have H_p: pt_map_packet p = Some p'. rewrite /pt_map_packet. break_match. rewrite /p in Heqp0. find_inversion. by rewrite H_m. by rewrite (filterMap_pt_map_packet_map_eq_some _ _ H_p) (pt_map_update_eq_some _ _ _ H_p). right. rewrite /pt_map_net /=. destruct p. simpl in *. move: H_m. case H_m: pt_map_msg => [m|] //. move => H_eq. have H_m' := @pt_net_handlers_none _ _ _ _ _ name_map msg_map multi_map_congr _ _ _ _ _ _ _ H_m H6. break_and. rewrite H3 3!filterMap_app H1. rewrite (filterMap_pt_map_name_msg_empty_eq _ pDst H0) /= H_m. set nwS1 := fun _ => _. set nwS2 := fun _ => _. have H_eq_s: nwS1 = nwS2. rewrite /nwS1 /nwS2 /=. apply functional_extensionality => n. rewrite /update /=. case: (name_eq_dec _ _) => H_dec //. by rewrite H_dec. by rewrite H_eq_s. - rewrite /= /pt_map_net /=. case H_i: pt_map_input => [inp'|]. left. apply (@StepFailure_input _ _ _ _ _ _ _ _ _ (pt_map_data d) (filterMap pt_map_name_msg l)). * exact: not_in_failed_not_in. * rewrite /= -(pt_input_handlers_some _ _ _ H_i) /pt_mapped_input_handlers /= tot_map_name_inv_inverse. repeat break_let. by tuple_inversion. * rewrite /= -filterMap_pt_map_packet_map_eq -filterMap_app. by rewrite pt_map_update_eq. right. rewrite /=. have [H_d [H_l H_o]] := pt_input_handlers_none _ _ _ H_i H5. rewrite H_o. split => //. rewrite filterMap_app. rewrite (filterMap_pt_map_name_msg_empty_eq _ h H_l) /=. set nwS1 := fun _ => _. set nwS2 := fun _ => _. have H_eq_s: nwS1 = nwS2. rewrite /nwS1 /nwS2 /=. apply functional_extensionality => n. rewrite /update /=. case: (name_eq_dec _ _) => H_dec //. by rewrite H_dec H_d. by rewrite H_eq_s. - case H_m: (pt_map_packet p) => [p'|]. left. destruct p, p'. simpl in *. move: H_m. case H_m: pt_map_msg => [m|] //. move => H_eq. find_inversion. rewrite /pt_map_net /=. find_rewrite. rewrite filterMap_app /= H_m filterMap_app. move: H4. set p := {| pSrc := _ ; pDst := _ ; pBody := _ |}. move => H_eq. set p' := {| pSrc := _ ; pDst := _ ; pBody := _ |}. exact: (@StepFailure_drop _ _ _ _ _ _ p' (filterMap pt_map_packet xs) (filterMap pt_map_packet ys)). right. split => //. rewrite /pt_map_net /=. find_rewrite. by rewrite 2!filterMap_app /= H_m. - rewrite /pt_map_net /=. find_rewrite. case H_p: pt_map_packet => [p'|]; last by right. left. rewrite filterMap_app /= H_p. exact: (@StepFailure_dup _ _ _ _ _ _ p' (filterMap pt_map_packet xs) (filterMap pt_map_packet ys)). - left. exact: StepFailure_fail. - rewrite remove_tot_map_eq /=. left. rewrite {2}/pt_map_net /=. eapply (@StepFailure_reboot _ _ _ (tot_map_name h)) => //; first exact: in_failed_in. by rewrite pt_map_update_eq /pt_map_net pt_reboot_eq /= tot_map_name_inv_inverse. Qed.
imports: Verdi(Verdi DynamicNetLemmas TotalMapSimulations) Coq(FunctionalExtensionality) Coq(Sumbool Sorting.Permutation) Verdi(DynamicNetLemmas) Verdi(Ssrexport)