proposition: Lemma map_fold_foldr {A B} (R : relation B) `{!PreOrder R} (l : list (K * A)) (f : K → A → B → B) (b : B) m : (∀ j z, Proper (R ==> R) (f j z)) → (∀ j1 j2 z1 z2 y, j1 ≠ j2 → m !! j1 = Some z1 → m !! j2 = Some z2 → R (f j1 z1 (f j2 z2 y)) (f j2 z2 (f j1 z1 y))) → map_to_list m ≡ₚ l → R (map_fold f b m) (foldr (uncurry f) b l).
proof: Proof. intros Hf_proper. revert l. apply (map_fold_ind (λ r m, ∀ l, (∀ j1 j2 z1 z2 y, j1 ≠ j2 → m !! j1 = Some z1 → m !! j2 = Some z2 → R (f j1 z1 (f j2 z2 y)) (f j2 z2 (f j1 z1 y))) → map_to_list m ≡ₚ l → R r (foldr (uncurry f) b l))); clear m. { intros [|x l] _; simpl; [done|]. by rewrite map_to_list_empty, Permutation_nil_l. } intros i x m r ? IH l Hf Hl. rewrite map_to_list_insert in Hl by done. etrans; [|apply (foldr_permutation R), Hl]; simpl. - f_equiv. apply IH; [|done]. intros j1 j2 z1 z2 y ???. apply Hf; [done|rewrite lookup_insert_Some; naive_solver..]. - intros []; apply _. - intros j1 [k1 y1] j2 [k2 y2] c Hj Hj1 Hj2. apply Hf. + intros ->. eapply Hj, (NoDup_lookup ((i,x) :: map_to_list m).*1). * csimpl. apply NoDup_cons_2, NoDup_fst_map_to_list. intros ([??]&?&?%elem_of_map_to_list)%elem_of_list_fmap; naive_solver. * by rewrite list_lookup_fmap, Hj1. * by rewrite list_lookup_fmap, Hj2. + apply elem_of_map_to_list. rewrite map_to_list_insert by done. by eapply elem_of_list_lookup_2. + apply elem_of_map_to_list. rewrite map_to_list_insert by done. by eapply elem_of_list_lookup_2. Qed.
imports: Coq(Permutation) stdpp(options)