Prove that big_sepM and fmap commute.

algebra/upred_big_op.v

@@ -154,19 +154,6 @@ Section gmap.
     m !! i = None →
     ([★ map] k↦y ∈ <[i:=x]> m, Φ k y) ⊣⊢ (Φ i x ★ [★ map] k↦y ∈ m, Φ k y).
   Proof. intros ?; by rewrite /uPred_big_sepM map_to_list_insert. Qed.
-  Lemma big_sepM_fn_insert (Ψ : K → A → uPred M → uPred M) (Φ : K → uPred M) m i x P :
-    m !! i = None →
-       ([★ map] k↦y ∈ <[i:=x]> m, Ψ k y (<[i:=P]> Φ k))
-    ⊣⊢ (Ψ i x P ★ [★ map] k↦y ∈ m, Ψ k y (Φ k)).
-  Proof.
-    intros. rewrite big_sepM_insert // fn_lookup_insert.
-    apply sep_proper, big_sepM_proper; auto=> k y ??.
-    by rewrite fn_lookup_insert_ne; last set_solver.
-  Qed.
-  Lemma big_sepM_fn_insert' (Φ : K → uPred M) m i x P :
-    m !! i = None →
-    ([★ map] k↦y ∈ <[i:=x]> m, <[i:=P]> Φ k) ⊣⊢ (P ★ [★ map] k↦y ∈ m, Φ k).
-  Proof. apply (big_sepM_fn_insert (λ _ _, id)). Qed.
 
   Lemma big_sepM_delete Φ (m : gmap K A) i x :
     m !! i = Some x →
@@ -182,6 +169,35 @@ Section gmap.
     by rewrite big_sepM_empty right_id.
   Qed.
 
+  Lemma big_sepM_fmap {B} (f : A → B) (Φ : K → B → uPred M) m :
+    ([★ map] k↦y ∈ f <$> m, Φ k y) ⊣⊢ ([★ map] k↦y ∈ m, Φ k (f y)).
+  Proof.
+    rewrite /uPred_big_sepM map_to_list_fmap -list_fmap_compose.
+    f_equiv; apply reflexive_eq, list_fmap_ext. by intros []. done.
+  Qed.
+
+  Lemma big_sepM_insert_override (Φ : K → uPred M) (m : gmap K A) i x :
+    m !! i = Some x →
+    ([★ map] k↦_ ∈ <[i:=x]> m, Φ k) ⊣⊢ ([★ map] k↦_ ∈ m, Φ k).
+  Proof.
+    intros. rewrite -insert_delete big_sepM_insert ?lookup_delete //.
+    by rewrite -big_sepM_delete.
+  Qed.
+
+  Lemma big_sepM_fn_insert (Ψ : K → A → uPred M → uPred M) (Φ : K → uPred M) m i x P :
+    m !! i = None →
+       ([★ map] k↦y ∈ <[i:=x]> m, Ψ k y (<[i:=P]> Φ k))
+    ⊣⊢ (Ψ i x P ★ [★ map] k↦y ∈ m, Ψ k y (Φ k)).
+  Proof.
+    intros. rewrite big_sepM_insert // fn_lookup_insert.
+    apply sep_proper, big_sepM_proper; auto=> k y ??.
+    by rewrite fn_lookup_insert_ne; last set_solver.
+  Qed.
+  Lemma big_sepM_fn_insert' (Φ : K → uPred M) m i x P :
+    m !! i = None →
+    ([★ map] k↦y ∈ <[i:=x]> m, <[i:=P]> Φ k) ⊣⊢ (P ★ [★ map] k↦y ∈ m, Φ k).
+  Proof. apply (big_sepM_fn_insert (λ _ _, id)). Qed.
+
   Lemma big_sepM_sepM Φ Ψ m :
        ([★ map] k↦x ∈ m, Φ k x ★ Ψ k x)
     ⊣⊢ (([★ map] k↦x ∈ m, Φ k x) ★ ([★ map] k↦x ∈ m, Ψ k x)).
@@ -190,6 +206,7 @@ Section gmap.
     induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?right_id //.
     by rewrite IH -!assoc (assoc _ (Ψ _ _)) [(Ψ _ _ ★ _)%I]comm -!assoc.
   Qed.
+
   Lemma big_sepM_later Φ m :
     (▷ [★ map] k↦x ∈ m, Φ k x) ⊣⊢ ([★ map] k↦x ∈ m, ▷ Φ k x).
   Proof.

prelude/fin_maps.v

@@ -647,6 +647,19 @@ Proof.
   intros. rewrite <-(map_of_to_list m1).
   auto using map_of_list_proper, NoDup_fst_map_to_list.
 Qed.
+
+Lemma map_of_list_nil {A} : map_of_list (@nil (K * A)) = ∅.
+Proof. done. Qed.
+Lemma map_of_list_cons {A} (l : list (K * A)) i x :
+  map_of_list ((i, x) :: l) = <[i:=x]>(map_of_list l).
+Proof. done. Qed.
+Lemma map_of_list_fmap {A B} (f : A → B) l :
+  map_of_list (prod_map id f <$> l) = f <$> map_of_list l.
+Proof.
+  induction l as [|[i x] l IH]; csimpl; rewrite ?fmap_empty; auto.
+  rewrite <-map_of_list_cons; simpl. by rewrite IH, <-fmap_insert.
+Qed.
+
 Lemma map_to_list_empty {A} : map_to_list ∅ = @nil (K * A).
 Proof.
   apply elem_of_nil_inv. intros [i x].
@@ -668,11 +681,16 @@ Proof.
   intros; apply NoDup_contains; auto using NoDup_map_to_list.
   intros [i x]. rewrite !elem_of_map_to_list; eauto using lookup_weaken.
 Qed.
-Lemma map_of_list_nil {A} : map_of_list (@nil (K * A)) = ∅.
-Proof. done. Qed.
-Lemma map_of_list_cons {A} (l : list (K * A)) i x :
-  map_of_list ((i, x) :: l) = <[i:=x]>(map_of_list l).
-Proof. done. Qed.
+Lemma map_to_list_fmap {A B} (f : A → B) m :
+  map_to_list (f <$> m) ≡ₚ prod_map id f <$> map_to_list m.
+Proof.
+  assert (NoDup ((prod_map id f <$> map_to_list m).*1)).
+  { erewrite <-list_fmap_compose, (list_fmap_ext _ fst) by done.
+    apply NoDup_fst_map_to_list. }
+  rewrite <-(map_of_to_list m) at 1.
+  by rewrite <-map_of_list_fmap, map_to_of_list.
+Qed.
+
 Lemma map_to_list_empty_inv_alt {A}  (m : M A) : map_to_list m ≡ₚ [] → m = ∅.
 Proof. rewrite <-map_to_list_empty. apply map_to_list_inj. Qed.
 Lemma map_to_list_empty_inv {A} (m : M A) : map_to_list m = [] → m = ∅.
@@ -687,6 +705,7 @@ Proof.
   rewrite Hperm, map_to_list_insert, map_to_of_list;
     auto using not_elem_of_map_of_list_1.
 Qed.
+
 Lemma map_choose {A} (m : M A) : m ≠ ∅ → ∃ i x, m !! i = Some x.
 Proof.
   intros Hemp. destruct (map_to_list m) as [|[i x] l] eqn:Hm.