proposition: Theorem step_failure_tot_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, tot_map_net net) (map tot_map_name failed', tot_map_net net') (map tot_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. - have ->: tot_map_name (pDst p) = pDst (tot_map_packet p) by destruct p. apply (@StepFailure_deliver _ _ _ _ _ _ _ (map tot_map_packet xs) (map tot_map_packet ys) _ (tot_map_data d) (tot_map_name_msgs l)). * rewrite /tot_map_net /=. find_rewrite. by rewrite map_app. * destruct p. exact: not_in_failed_not_in. * destruct p. simpl in *. have H_q := tot_net_handlers_eq pDst pSrc pBody (nwState net pDst). rewrite /tot_mapped_net_handlers in H_q. find_rewrite. rewrite H_q. by rewrite tot_map_name_inv_inverse. * rewrite /= -tot_map_update_packet_eq /= /tot_map_net /=. destruct p. by rewrite 2!map_app tot_map_packet_map_eq. - apply (@StepFailure_input _ _ _ _ _ _ _ _ _ (tot_map_data d) (tot_map_name_msgs l)). * exact: not_in_failed_not_in. * rewrite /=. have H_q := tot_input_handlers_eq h inp (nwState net h). rewrite /tot_mapped_input_handlers /= in H_q. find_rewrite. rewrite H_q. by rewrite tot_map_name_inv_inverse. * rewrite /= /tot_map_net /= -tot_map_update_eq. by rewrite map_app tot_map_packet_map_eq. - apply (@StepFailure_drop _ _ _ _ _ _ (tot_map_packet p) (map tot_map_packet xs) (map tot_map_packet ys)). * rewrite /tot_map_net /=. find_rewrite. by rewrite map_app. * by rewrite /tot_map_net /= map_app. - apply (@StepFailure_dup _ _ _ _ _ _ (tot_map_packet p) (map tot_map_packet xs) (map tot_map_packet ys)). * rewrite /tot_map_net /=. find_rewrite. by rewrite map_app. * by rewrite /tot_map_net /= map_app. - exact: StepFailure_fail. - eapply (@StepFailure_reboot _ _ _ (tot_map_name h)). * exact: in_failed_in. * by rewrite remove_tot_map_eq. * by rewrite /tot_map_net /= tot_map_update_eq tot_reboot_eq tot_map_name_inv_inverse. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Coq(FunctionalExtensionality) Coq(Sorting.Permutation Sumbool) Verdi(Ssrexport)