proposition: Lemma map_fold_insert {A B} (R : relation B) `{!PreOrder R} (f : K → A → B → B) (b : B) (i : K) (x : A) (m : M A) : (∀ j z, Proper (R ==> R) (f j z)) → (∀ j1 j2 z1 z2 y, j1 ≠ j2 → <[i:=x]> m !! j1 = Some z1 → <[i:=x]> m !! j2 = Some z2 → R (f j1 z1 (f j2 z2 y)) (f j2 z2 (f j1 z1 y))) → m !! i = None → R (map_fold f b (<[i:=x]> m)) (f i x (map_fold f b m)).
proof: Proof. intros Hf_proper Hf Hi. trans (f i x (foldr (uncurry f) b (map_to_list m))). - apply (map_fold_foldr _ ((i,x) :: map_to_list m)); [solve_proper|done|]. by rewrite map_to_list_insert by done. - f_equiv. apply (map_fold_foldr (flip R)); [solve_proper| |done]. intros j1 j2 z1 z2 y ???. apply Hf; rewrite ?lookup_insert_Some; naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)