proposition: Lemma map_fold_comm_acc_strong {A B} (R : relation B) `{!PreOrder R} (f : K → A → B → B) (g : B → B) (x : B) (m : M A) : (∀ j z, Proper (R ==> R) (f j z)) → Proper (R ==> R) g → (∀ 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))) → (∀ j z y, m !! j = Some z → R (f j z (g y)) (g (f j z y))) → R (map_fold f (g x) m) (g (map_fold f x m)).
proof: Proof. intros ? ? Hf Hg. apply (map_fold_ind (λ z m, (∀ 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))) → (∀ j z y, m !! j = Some z → R (f j z (g y)) (g (f j z y))) → R (map_fold f (g x) m) (g z))); [by rewrite map_fold_empty| |apply Hf|apply Hg]. intros i x' m' r Hx' IH Hfm' Hgm'. rewrite map_fold_insert by (apply _ || done). rewrite <-Hgm' by (by rewrite lookup_insert). f_equiv. apply IH. - intros j1 j2 z1 z2 y Hjs Hl1 Hl2. apply Hfm'; [done|rewrite lookup_insert_Some; naive_solver..]. - intros j z y Hj. apply Hgm'. rewrite lookup_insert_ne by naive_solver. done. Qed.
imports: Coq(Permutation) stdpp(options)