proposition: Lemma pt_nodup_perm_map_map_pair_perm : forall m m' h failed ns ns', NoDup ns -> Permutation (map tot_map_name ns) ns' -> pt_map_msg m = Some m' -> Permutation (filterMap pt_map_name_msg (map2snd m (filter_rel adjacent_to_dec h (remove_all name_eq_dec failed ns)))) (map2snd m' (filter_rel adjacent_to_dec (tot_map_name h) (remove_all name_eq_dec (map tot_map_name failed) ns'))).
proof: Proof. Proof using overlay_map_congr name_map_bijective. move => m m' h failed ns ns' H_nd H_pm H_eq. apply NoDup_Permutation; last split. - apply (@nodup_pt_map m); first exact: in_map2snd_snd. apply NoDup_map2snd. exact: NoDup_remove_all. - apply NoDup_map2snd. apply NoDup_remove_all. move: H_pm. apply: NoDup_Permutation_NoDup. exact: nodup_to_map_name. - case: x => n m0 H_in. have H_eq' := pt_map_in_snd _ _ _ _ H_eq H_in. rewrite /= in H_eq'. rewrite H_eq' in H_in. rewrite H_eq' {H_eq' m0}. apply (@pt_in_tot_map_name m) in H_in => //. apply in_map_pair_adjacent_to in H_in. apply in_adjacent_exclude_in_exlude in H_in. move: H_in => [H_in H_adj]. apply in_failed_exclude in H_in. move: H_in => [H_in H_in']. have H_nin: ~ In n (map tot_map_name failed). rewrite -(tot_map_name_inverse_inv n). exact: not_in_failed_not_in. apply tot_adjacent_to_fst_snd in H_adj. rewrite tot_map_name_inverse_inv in H_adj. have H_inn: In n ns'. apply (Permutation_in n) in H_pm => //. rewrite -(tot_map_name_inverse_inv n). exact: in_failed_in. exact: in_in_adj_map_pair. exact: in_map2snd_snd. - case: x => n m0 H_in. have H_eq' := in_map2snd_snd _ _ adjacent_to adjacent_to_dec _ _ _ _ H_in. rewrite /= in H_eq'. rewrite H_eq'. rewrite H_eq' in H_in. apply in_map2snd_related_in in H_in. move: H_in => [H_adj H_in]. rewrite -(tot_map_name_inverse_inv n) in H_adj. apply tot_adjacent_to_fst_snd in H_adj. apply in_exclude_not_in_failed_map in H_in. move: H_in => [H_in_f H_in]. apply not_in_map_not_in_failed in H_in_f. have H_in_n: In (tot_map_name_inv n) ns. apply Permutation_sym in H_pm. apply (Permutation_in n) in H_pm => //. apply: tot_map_name_in. by rewrite tot_map_name_inverse_inv. apply: (@in_pt_map_map_pair m) => //; first by move => nm; apply in_map2snd_snd. apply adjacent_in_in_msg => //. exact: not_in_failed_in_exclude. Qed.
imports: Verdi(Verdi DynamicNetLemmas TotalMapSimulations) Coq(FunctionalExtensionality) Coq(Sumbool Sorting.Permutation) Verdi(DynamicNetLemmas) Verdi(Ssrexport)