proposition: Theorem step_failure_tot_mapped_simulation_2 : forall net net' failed failed' out mnet mfailed mfailed' mout, @step_failure _ _ fail_snd (failed, net) (failed', net') out -> tot_map_net mnet = net -> map tot_map_name mfailed = failed -> map tot_map_name mfailed' = failed' -> map tot_map_trace_occ mout = out -> exists mnet', @step_failure _ _ fail_fst (mfailed, mnet) (mfailed', mnet') mout /\ tot_map_net mnet' = net'.
proof: Proof. Proof using tot_map_output_injective name_map_bijective multi_map_congr fail_map_congr. move => net net' failed failed' out mnet mfailed mfailed' mout H_step H_eq_net H_eq_f H_eq_f' H_eq_out. invcs H_step. - destruct p. rewrite /tot_map_net /=. destruct mnet. simpl in *. match goal with | H : map tot_map_packet _ = _ |- _ => have [pks1 [pks2 [H_eq_pks [H_eq_pks1 H_eq_pks2]]]] := map_eq_inv _ _ _ _ H end. case: pks2 H_eq_pks H_eq_pks2 => //= p pks2 H_eq_pks H_eq_pks2. rewrite H_eq_pks. inversion H_eq_pks2. case H_hnd': (net_handlers (Net.pDst p) (Net.pSrc p) (Net.pBody p) (nwState (Net.pDst p))) => [dout l']. case: dout H_hnd' => out' d' H_hnd'. rewrite -H_eq_pks1. exists {| nwPackets := send_packets (Net.pDst p) l' ++ pks1 ++ pks2 ; nwState := update name_eq_dec nwState (Net.pDst p) d' |}. split. * match goal with | H : _ = map tot_map_trace_occ _ |- _ => have [n' [lo [H_eq_mout [H_eq_n H_eq_lo]]]] := tot_map_trace_occ_inv _ (eq_sym H) end. rewrite H_eq_mout. have H_eq_dst: n' = Net.pDst p. rewrite -(tot_map_name_inv_inverse n') H_eq_n. destruct p. simpl in *. find_inversion. by rewrite tot_map_name_inv_inverse. rewrite H_eq_dst. match goal with | H: map tot_map_name _ = map tot_map_name _ |- _ => apply map_eq_name_eq_eq in H; rewrite H end. apply (@StepFailure_deliver _ _ _ _ _ _ _ pks1 pks2 _ d' l') => //=. rewrite -H_eq_dst => H_in. find_apply_lem_hyp in_failed_in. by find_rewrite_lem H_eq_n. suff H_suff: lo = out' by rewrite H_suff. have H_eq_hnd := @tot_net_handlers_eq _ _ _ _ _ _ _ multi_map_congr (Net.pDst p) (Net.pSrc p) (Net.pBody p) (nwState (Net.pDst p)). rewrite /tot_mapped_net_handlers /= in H_eq_hnd. repeat break_let. inversion H_hnd'. have H_eq_src: tot_map_name (Net.pSrc p) = pSrc by destruct p; simpl in *; find_inversion. rewrite H_eq_src /= {H_eq_src} in H_eq_hnd. have H_eq_body: tot_map_msg (Net.pBody p) = pBody by destruct p; simpl in *; find_inversion. rewrite H_eq_body in H_eq_hnd. match goal with | H: net_handlers _ _ _ (tot_map_data (_ (tot_map_name_inv pDst))) = _ |- _ => rewrite -H_eq_n tot_map_name_inv_inverse H_eq_dst in H ; rewrite H in H_eq_hnd end. find_inversion. find_apply_lem_hyp map_eq_inv_eq; last exact: tot_map_output_injective. by symmetry. * rewrite /= /update /=. have H_eq_dst: tot_map_name (Net.pDst p) = pDst by destruct p; simpl in *; find_inversion. have H_eq_src: tot_map_name (Net.pSrc p) = pSrc by destruct p; simpl in *; find_inversion. have H_eq_body: tot_map_msg (Net.pBody p) = pBody by destruct p; simpl in *; find_inversion. rewrite 2!map_app. have H_eq_hnd := @tot_net_handlers_eq _ _ _ _ _ _ _ multi_map_congr (Net.pDst p) (Net.pSrc p) (Net.pBody p) (nwState (Net.pDst p)). rewrite /tot_mapped_net_handlers /= in H_eq_hnd. repeat break_let. inversion H_hnd'. rewrite H_eq_dst H_eq_src H_eq_body in H_eq_hnd. simpl in *. match goal with | H: net_handlers _ _ _ (tot_map_data (_ (tot_map_name_inv pDst))) = _ |- _ => rewrite -{2}H_eq_dst tot_map_name_inv_inverse in H; rewrite H in H_eq_hnd end. find_inversion; clean. set nwP1 := map tot_map_packet _. set nwP2 := map (fun _ => _) (tot_map_name_msgs _). set nwS1 := fun _ => _. set nwS2 := fun _ => _. have H_eq_nw: nwP1 = nwP2. rewrite /nwP1 /nwP2. elim l' => //=. case => /= n' m' l0 IH. rewrite IH. by find_rewrite. rewrite -H_eq_nw /nwP1 {H_eq_nw nwP1 nwP2}. have H_eq_sw: nwS1 = nwS2. rewrite /nwS1 /nwS2. apply functional_extensionality => n'. repeat break_if => //. + find_reverse_rewrite. by find_rewrite_lem tot_map_name_inverse_inv. + find_rewrite. by find_rewrite_lem tot_map_name_inv_inverse. by rewrite H_eq_sw. - rewrite /tot_map_net /=. destruct mnet. match goal with | H: _ = map tot_map_trace_occ _ |- _ => have [h' [inp' [out' [H_eq_mout [H_eq_n [H_eq_out H_eq_inp]]]]]] := tot_map_trace_occ_in_inv _ (eq_sym H) end. have H_q := @tot_input_handlers_eq _ _ _ _ _ _ _ multi_map_congr h' inp' (nwState h'). rewrite /tot_mapped_input_handlers in H_q. repeat break_let. rewrite H_eq_n H_eq_inp in H_q. match goal with | H: input_handlers _ _ (tot_map_data (_ (tot_map_name_inv h))) = _ |- _ => rewrite -{2}H_eq_n tot_map_name_inv_inverse in H ; rewrite H in H_q end. inversion H_q. simpl in *. find_apply_lem_hyp map_eq_name_eq_eq. exists ({| nwPackets := send_packets h' l0 ++ nwPackets ; nwState := update name_eq_dec nwState h' d0 |}). split. * rewrite H_eq_mout. match goal with | H: mfailed = _ |- _ => rewrite H end. apply (@StepFailure_input _ _ _ _ _ _ _ _ _ d0 l0) => //. move => H_in. apply in_failed_in in H_in. by rewrite H_eq_n in H_in. rewrite /= Heqp. suff H_suff: l1 = out' by rewrite H_suff. match goal with | H: map tot_map_output _ = _ |- _ => rewrite -H_eq_out in H end. by find_apply_lem_hyp map_eq_inv_eq; last exact: tot_map_output_injective. * rewrite /= map_app. set nwP1 := map tot_map_packet _. set nwP2 := map (fun _ => _) (tot_map_name_msgs _). set nwS1 := fun _ => _. set nwS2 := update _ _ _ _. have H_eq_nwp: nwP1 = nwP2. rewrite /nwP1 /nwP2 {Heqp H_q nwP1 nwP2}. elim l0 => //=. case => /= n m l' IH. by rewrite H_eq_n IH. have H_eq_nws: nwS1 = nwS2. rewrite /nwS1 /nwS2. rewrite /update /=. apply functional_extensionality => n. rewrite -H_eq_n. repeat break_if => //. + match goal with | H: _ = h' , H': _ <> tot_map_name h' |- _ => rewrite -H in H' end. by find_rewrite_lem tot_map_name_inverse_inv. + match goal with | H: n = _ , H': tot_map_name_inv n <> _ |- _ => rewrite H in H' end. by find_rewrite_lem tot_map_name_inv_inverse. by rewrite H_eq_nwp H_eq_nws. - destruct mout => //. find_apply_lem_hyp map_eq_name_eq_eq. find_reverse_rewrite. match goal with | H : map tot_map_packet _ = _ |- _ => have [pks1 [pks2 [H_eq_pks [H_eq_pks1 H_eq_pks2]]]] := map_eq_inv _ _ _ _ H end. case: pks2 H_eq_pks H_eq_pks2 => //= p' pks2 H_eq_pks H_eq_pks2. inversion H_eq_pks2. rewrite -H_eq_pks1. exists {| nwPackets := pks1 ++ pks2 ; nwState := nwState mnet |}. split; first exact: (@StepFailure_drop _ _ _ _ _ _ p' pks1 pks2). by rewrite /tot_map_net /= map_app. - destruct mout => //. find_apply_lem_hyp map_eq_name_eq_eq. find_rewrite. match goal with | H : map tot_map_packet _ = _ |- _ => have [pks1 [pks2 [H_eq_pks [H_eq_pks1 H_eq_pks2]]]] := map_eq_inv _ _ _ _ H end. case: pks2 H_eq_pks H_eq_pks2 => //= p' pks2 H_eq_pks H_eq_pks2. inversion H_eq_pks2. rewrite -H_eq_pks1. exists {| nwPackets := p' :: pks1 ++ p' :: pks2 ; nwState := nwState mnet |}. split; first exact: (@StepFailure_dup _ _ _ _ _ _ p' pks1 pks2). by rewrite /tot_map_net /= map_app. - destruct mout => //. destruct mfailed' => //. simpl in *. find_inversion. find_apply_lem_hyp map_eq_name_eq_eq. find_rewrite. exists mnet => //. split => //. exact: StepFailure_fail. - destruct mout => //. find_copy_apply_lem_hyp in_split. break_exists. match goal with | H: map tot_map_name _ = _ |- _ => have [mns1 [mns2 [H_eq_mns [H_eq_mns1 H_eq_mns2]]]] := map_eq_inv _ _ _ _ H end. destruct mns2 => //. exists {| nwPackets := nwPackets mnet ; nwState := update name_eq_dec (nwState mnet) n (reboot (nwState mnet n)) |}. split. * apply (@StepFailure_reboot _ _ _ n) => //. + rewrite H_eq_mns. apply in_or_app. by right; left. + inversion H_eq_mns2. have H_eq: remove name_eq_dec h (map tot_map_name mfailed) = map tot_map_name (remove name_eq_dec n mfailed). elim mfailed => //=. move => n' l IH. repeat break_if => //. + by find_reverse_rewrite; find_apply_lem_hyp tot_map_name_injective. + by find_reverse_rewrite; find_reverse_rewrite. + by rewrite /= IH. match goal with | H: _ = remove _ _ _ |- _ => rewrite H_eq in H end. by find_apply_lem_hyp map_eq_name_eq_eq. * rewrite /tot_map_net /=. inversion H_eq_mns2. by rewrite tot_map_update_eq tot_map_name_inv_inverse tot_reboot_eq. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Coq(FunctionalExtensionality) Coq(Sorting.Permutation Sumbool) Verdi(Ssrexport)