From f372c5c1530963f73148bf1231ac7b45e0e0e5cf Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 29 Mar 2016 12:41:55 +0200
Subject: [PATCH] Rename algebra/fin_maps.v -> algebra/gmap.v

Also remove some superfluous map_ prefixes.
---
 _CoqProject                     |   2 +-
 algebra/{fin_maps.v => gmap.v}  | 190 ++++++++++++++++----------------
 heap_lang/lib/heap.v            |  16 +--
 program_logic/ghost_ownership.v |  20 ++--
 program_logic/global_functor.v  |   4 +-
 program_logic/ownership.v       |   2 +-
 program_logic/resources.v       |   6 +-
 program_logic/wsat.v            |   2 +-
 8 files changed, 119 insertions(+), 123 deletions(-)
 rename algebra/{fin_maps.v => gmap.v} (66%)

diff --git a/_CoqProject b/_CoqProject
index 11ce70ea2..6c8d1e3ca 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -41,7 +41,7 @@ algebra/cmra_big_op.v
 algebra/cmra_tactics.v
 algebra/sts.v
 algebra/auth.v
-algebra/fin_maps.v
+algebra/gmap.v
 algebra/cofe.v
 algebra/base.v
 algebra/dra.v
diff --git a/algebra/fin_maps.v b/algebra/gmap.v
similarity index 66%
rename from algebra/fin_maps.v
rename to algebra/gmap.v
index 52ef68d60..1adec3526 100644
--- a/algebra/fin_maps.v
+++ b/algebra/gmap.v
@@ -6,14 +6,14 @@ Section cofe.
 Context `{Countable K} {A : cofeT}.
 Implicit Types m : gmap K A.
 
-Instance map_dist : Dist (gmap K A) := Î» n m1 m2,
+Instance gmap_dist : Dist (gmap K A) := Î» n m1 m2,
   âˆ€ i, m1 !! i â‰¡{n}â‰¡ m2 !! i.
-Program Definition map_chain (c : chain (gmap K A))
+Program Definition gmap_chain (c : chain (gmap K A))
   (k : K) : chain (option A) := {| chain_car n := c n !! k |}.
 Next Obligation. by intros c k n i ?; apply (chain_cauchy c). Qed.
-Instance map_compl : Compl (gmap K A) := Î» c,
-  map_imap (Î» i _, compl (map_chain c i)) (c 0).
-Definition map_cofe_mixin : CofeMixin (gmap K A).
+Instance gmap_compl : Compl (gmap K A) := Î» c,
+  map_imap (Î» i _, compl (gmap_chain c i)) (c 0).
+Definition gmap_cofe_mixin : CofeMixin (gmap K A).
 Proof.
   split.
   - intros m1 m2; split.
@@ -24,15 +24,15 @@ Proof.
     + by intros m1 m2 ? k.
     + by intros m1 m2 m3 ?? k; trans (m2 !! k).
   - by intros n m1 m2 ? k; apply dist_S.
-  - intros n c k; rewrite /compl /map_compl lookup_imap.
+  - intros n c k; rewrite /compl /gmap_compl lookup_imap.
     feed inversion (Î» H, chain_cauchy c 0 n H k); simpl; auto with lia.
     by rewrite conv_compl /=; apply reflexive_eq.
 Qed.
-Canonical Structure mapC : cofeT := CofeT map_cofe_mixin.
-Global Instance map_discrete : Discrete A â†’ Discrete mapC.
+Canonical Structure gmapC : cofeT := CofeT gmap_cofe_mixin.
+Global Instance gmap_discrete : Discrete A â†’ Discrete gmapC.
 Proof. intros ? m m' ? i. by apply (timeless _). Qed.
 (* why doesn't this go automatic? *)
-Global Instance mapC_leibniz: LeibnizEquiv A â†’ LeibnizEquiv mapC.
+Global Instance gmapC_leibniz: LeibnizEquiv A â†’ LeibnizEquiv gmapC.
 Proof. intros; change (LeibnizEquiv (gmap K A)); apply _. Qed.
 
 Global Instance lookup_ne n k :
@@ -62,47 +62,47 @@ Proof.
     [by constructor|by apply lookup_ne].
 Qed.
 
-Instance map_empty_timeless : Timeless (âˆ… : gmap K A).
+Instance gmap_empty_timeless : Timeless (âˆ… : gmap K A).
 Proof.
   intros m Hm i; specialize (Hm i); rewrite lookup_empty in Hm |- *.
   inversion_clear Hm; constructor.
 Qed.
-Global Instance map_lookup_timeless m i : Timeless m â†’ Timeless (m !! i).
+Global Instance gmap_lookup_timeless m i : Timeless m â†’ Timeless (m !! i).
 Proof.
   intros ? [x|] Hx; [|by symmetry; apply: timeless].
   assert (m â‰¡{0}â‰¡ <[i:=x]> m)
     by (by symmetry in Hx; inversion Hx; cofe_subst; rewrite insert_id).
   by rewrite (timeless m (<[i:=x]>m)) // lookup_insert.
 Qed.
-Global Instance map_insert_timeless m i x :
+Global Instance gmap_insert_timeless m i x :
   Timeless x â†’ Timeless m â†’ Timeless (<[i:=x]>m).
 Proof.
   intros ?? m' Hm j; destruct (decide (i = j)); simplify_map_eq.
   { by apply: timeless; rewrite -Hm lookup_insert. }
   by apply: timeless; rewrite -Hm lookup_insert_ne.
 Qed.
-Global Instance map_singleton_timeless i x :
+Global Instance gmap_singleton_timeless i x :
   Timeless x â†’ Timeless ({[ i := x ]} : gmap K A) := _.
 End cofe.
 
-Arguments mapC _ {_ _} _.
+Arguments gmapC _ {_ _} _.
 
 (* CMRA *)
 Section cmra.
 Context `{Countable K} {A : cmraT}.
 Implicit Types m : gmap K A.
 
-Instance map_op : Op (gmap K A) := merge op.
-Instance map_core : Core (gmap K A) := fmap core.
-Instance map_valid : Valid (gmap K A) := Î» m, âˆ€ i, âœ“ (m !! i).
-Instance map_validN : ValidN (gmap K A) := Î» n m, âˆ€ i, âœ“{n} (m !! i).
+Instance gmap_op : Op (gmap K A) := merge op.
+Instance gmap_core : Core (gmap K A) := fmap core.
+Instance gmap_valid : Valid (gmap K A) := Î» m, âˆ€ i, âœ“ (m !! i).
+Instance gmap_validN : ValidN (gmap K A) := Î» n m, âˆ€ i, âœ“{n} (m !! i).
 
 Lemma lookup_op m1 m2 i : (m1 â‹… m2) !! i = m1 !! i â‹… m2 !! i.
 Proof. by apply lookup_merge. Qed.
 Lemma lookup_core m i : core m !! i = core (m !! i).
 Proof. by apply lookup_fmap. Qed.
 
-Lemma map_included_spec (m1 m2 : gmap K A) : m1 â‰¼ m2 â†” âˆ€ i, m1 !! i â‰¼ m2 !! i.
+Lemma gmap_included_spec (m1 m2 : gmap K A) : m1 â‰¼ m2 â†” âˆ€ i, m1 !! i â‰¼ m2 !! i.
 Proof.
   split; [by intros [m Hm] i; exists (m !! i); rewrite -lookup_op Hm|].
   revert m2. induction m1 as [|i x m Hi IH] using map_ind=> m2 Hm.
@@ -118,7 +118,7 @@ Proof.
       lookup_insert_ne // lookup_partial_alter_ne.
 Qed.
 
-Definition map_cmra_mixin : CMRAMixin (gmap K A).
+Definition gmap_cmra_mixin : CMRAMixin (gmap K A).
 Proof.
   split.
   - by intros n m1 m2 m3 Hm i; rewrite !lookup_op (Hm i).
@@ -132,7 +132,7 @@ Proof.
   - by intros m1 m2 i; rewrite !lookup_op comm.
   - by intros m i; rewrite lookup_op !lookup_core cmra_core_l.
   - by intros m i; rewrite !lookup_core cmra_core_idemp.
-  - intros x y; rewrite !map_included_spec; intros Hm i.
+  - intros x y; rewrite !gmap_included_spec; intros Hm i.
     by rewrite !lookup_core; apply cmra_core_preserving.
   - intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i).
     by rewrite -lookup_op.
@@ -152,25 +152,25 @@ Proof.
       pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''.
       by symmetry; apply option_op_positive_dist_r with (m1 !! i).
 Qed.
-Canonical Structure mapR : cmraT := CMRAT map_cofe_mixin map_cmra_mixin.
-Global Instance map_cmra_unit : CMRAUnit mapR.
+Canonical Structure gmapR : cmraT := CMRAT gmap_cofe_mixin gmap_cmra_mixin.
+Global Instance gmap_cmra_unit : CMRAUnit gmapR.
 Proof.
   split.
   - by intros i; rewrite lookup_empty.
   - by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _).
-  - apply map_empty_timeless.
+  - apply gmap_empty_timeless.
 Qed.
-Global Instance map_cmra_discrete : CMRADiscrete A â†’ CMRADiscrete mapR.
+Global Instance gmap_cmra_discrete : CMRADiscrete A â†’ CMRADiscrete gmapR.
 Proof. split; [apply _|]. intros m ? i. by apply: cmra_discrete_valid. Qed.
 
 (** Internalized properties *)
-Lemma map_equivI {M} m1 m2 : (m1 â‰¡ m2) âŠ£âŠ¢ (âˆ€ i, m1 !! i â‰¡ m2 !! i : uPred M).
+Lemma gmap_equivI {M} m1 m2 : (m1 â‰¡ m2) âŠ£âŠ¢ (âˆ€ i, m1 !! i â‰¡ m2 !! i : uPred M).
 Proof. by uPred.unseal. Qed.
-Lemma map_validI {M} m : (âœ“ m) âŠ£âŠ¢ (âˆ€ i, âœ“ (m !! i) : uPred M).
+Lemma gmap_validI {M} m : (âœ“ m) âŠ£âŠ¢ (âˆ€ i, âœ“ (m !! i) : uPred M).
 Proof. by uPred.unseal. Qed.
 End cmra.
 
-Arguments mapR _ {_ _} _.
+Arguments gmapR _ {_ _} _.
 
 Section properties.
 Context `{Countable K} {A : cmraT}.
@@ -178,23 +178,23 @@ Implicit Types m : gmap K A.
 Implicit Types i : K.
 Implicit Types a : A.
 
-Lemma map_lookup_validN n m i x : âœ“{n} m â†’ m !! i â‰¡{n}â‰¡ Some x â†’ âœ“{n} x.
+Lemma lookup_validN n m i x : âœ“{n} m â†’ m !! i â‰¡{n}â‰¡ Some x â†’ âœ“{n} x.
 Proof. by move=> /(_ i) Hm Hi; move:Hm; rewrite Hi. Qed.
-Lemma map_lookup_valid m i x : âœ“ m â†’ m !! i â‰¡ Some x â†’ âœ“ x.
+Lemma lookup_valid m i x : âœ“ m â†’ m !! i â‰¡ Some x â†’ âœ“ x.
 Proof. move=> Hm Hi. move:(Hm i). by rewrite Hi. Qed.
-Lemma map_insert_validN n m i x : âœ“{n} x â†’ âœ“{n} m â†’ âœ“{n} <[i:=x]>m.
+Lemma insert_validN n m i x : âœ“{n} x â†’ âœ“{n} m â†’ âœ“{n} <[i:=x]>m.
 Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_eq. Qed.
-Lemma map_insert_valid m i x : âœ“ x â†’ âœ“ m â†’ âœ“ <[i:=x]>m.
+Lemma insert_valid m i x : âœ“ x â†’ âœ“ m â†’ âœ“ <[i:=x]>m.
 Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_eq. Qed.
-Lemma map_singleton_validN n i x : âœ“{n} ({[ i := x ]} : gmap K A) â†” âœ“{n} x.
+Lemma singleton_validN n i x : âœ“{n} ({[ i := x ]} : gmap K A) â†” âœ“{n} x.
 Proof.
-  split; [|by intros; apply map_insert_validN, cmra_unit_validN].
+  split; [|by intros; apply insert_validN, cmra_unit_validN].
   by move=>/(_ i); simplify_map_eq.
 Qed.
-Lemma map_singleton_valid i x : âœ“ ({[ i := x ]} : gmap K A) â†” âœ“ x.
-Proof. rewrite !cmra_valid_validN. by setoid_rewrite map_singleton_validN. Qed.
+Lemma singleton_valid i x : âœ“ ({[ i := x ]} : gmap K A) â†” âœ“ x.
+Proof. rewrite !cmra_valid_validN. by setoid_rewrite singleton_validN. Qed.
 
-Lemma map_insert_singleton_opN n m i x :
+Lemma insert_singleton_opN n m i x :
   m !! i = None âˆ¨ m !! i â‰¡{n}â‰¡ Some (core x) â†’ <[i:=x]> m â‰¡{n}â‰¡ {[ i := x ]} â‹… m.
 Proof.
   intros Hi j; destruct (decide (i = j)) as [->|];
@@ -202,24 +202,22 @@ Proof.
   rewrite lookup_op lookup_insert lookup_singleton.
   by destruct Hi as [->| ->]; constructor; rewrite ?cmra_core_r.
 Qed.
-Lemma map_insert_singleton_op m i x :
+Lemma insert_singleton_op m i x :
   m !! i = None âˆ¨ m !! i â‰¡ Some (core x) â†’ <[i:=x]> m â‰¡ {[ i := x ]} â‹… m.
-Proof.
-  rewrite !equiv_dist; naive_solver eauto using map_insert_singleton_opN.
-Qed.
+Proof. rewrite !equiv_dist; naive_solver eauto using insert_singleton_opN. Qed.
 
-Lemma map_core_singleton (i : K) (x : A) :
+Lemma core_singleton (i : K) (x : A) :
   core ({[ i := x ]} : gmap K A) = {[ i := core x ]}.
 Proof. apply map_fmap_singleton. Qed.
-Lemma map_op_singleton (i : K) (x y : A) :
+Lemma op_singleton (i : K) (x y : A) :
   {[ i := x ]} â‹… {[ i := y ]} = ({[ i := x â‹… y ]} : gmap K A).
 Proof. by apply (merge_singleton _ _ _ x y). Qed.
 
-Global Instance map_persistent m : (âˆ€ x : A, Persistent x) â†’ Persistent m.
+Global Instance gmap_persistent m : (âˆ€ x : A, Persistent x) â†’ Persistent m.
 Proof. intros ? i. by rewrite lookup_core persistent. Qed.
-Global Instance map_singleton_persistent i (x : A) :
+Global Instance gmap_singleton_persistent i (x : A) :
   Persistent x â†’ Persistent {[ i := x ]}.
-Proof. intros. by rewrite /Persistent map_core_singleton persistent. Qed.
+Proof. intros. by rewrite /Persistent core_singleton persistent. Qed.
 
 Lemma singleton_includedN n m i x :
   {[ i := x ]} â‰¼{n} m â†” âˆƒ y, m !! i â‰¡{n}â‰¡ Some y âˆ§ x â‰¼{n} y.
@@ -234,14 +232,14 @@ Proof.
     + rewrite Hi lookup_op lookup_singleton lookup_insert. by constructor.
     + by rewrite lookup_op lookup_singleton_ne // lookup_insert_ne // left_id.
 Qed.
-Lemma map_dom_op m1 m2 : dom (gset K) (m1 â‹… m2) â‰¡ dom _ m1 âˆª dom _ m2.
+Lemma dom_op m1 m2 : dom (gset K) (m1 â‹… m2) â‰¡ dom _ m1 âˆª dom _ m2.
 Proof.
   apply elem_of_equiv; intros i; rewrite elem_of_union !elem_of_dom.
   unfold is_Some; setoid_rewrite lookup_op.
   destruct (m1 !! i), (m2 !! i); naive_solver.
 Qed.
 
-Lemma map_insert_updateP (P : A â†’ Prop) (Q : gmap K A â†’ Prop) m i x :
+Lemma insert_updateP (P : A â†’ Prop) (Q : gmap K A â†’ Prop) m i x :
   x ~~>: P â†’ (âˆ€ y, P y â†’ Q (<[i:=y]>m)) â†’ <[i:=x]>m ~~>: Q.
 Proof.
   intros Hx%option_updateP' HP n mf Hm.
@@ -251,24 +249,22 @@ Proof.
   intros j; move: (Hm j)=>{Hm}; rewrite !lookup_op=>Hm.
   destruct (decide (i = j)); simplify_map_eq/=; auto.
 Qed.
-Lemma map_insert_updateP' (P : A â†’ Prop) m i x :
+Lemma insert_updateP' (P : A â†’ Prop) m i x :
   x ~~>: P â†’ <[i:=x]>m ~~>: Î» m', âˆƒ y, m' = <[i:=y]>m âˆ§ P y.
-Proof. eauto using map_insert_updateP. Qed.
-Lemma map_insert_update m i x y : x ~~> y â†’ <[i:=x]>m ~~> <[i:=y]>m.
-Proof.
-  rewrite !cmra_update_updateP; eauto using map_insert_updateP with subst.
-Qed.
+Proof. eauto using insert_updateP. Qed.
+Lemma insert_update m i x y : x ~~> y â†’ <[i:=x]>m ~~> <[i:=y]>m.
+Proof. rewrite !cmra_update_updateP; eauto using insert_updateP with subst. Qed.
 
-Lemma map_singleton_updateP (P : A â†’ Prop) (Q : gmap K A â†’ Prop) i x :
+Lemma singleton_updateP (P : A â†’ Prop) (Q : gmap K A â†’ Prop) i x :
   x ~~>: P â†’ (âˆ€ y, P y â†’ Q {[ i := y ]}) â†’ {[ i := x ]} ~~>: Q.
-Proof. apply map_insert_updateP. Qed.
-Lemma map_singleton_updateP' (P : A â†’ Prop) i x :
+Proof. apply insert_updateP. Qed.
+Lemma singleton_updateP' (P : A â†’ Prop) i x :
   x ~~>: P â†’ {[ i := x ]} ~~>: Î» m, âˆƒ y, m = {[ i := y ]} âˆ§ P y.
-Proof. apply map_insert_updateP'. Qed.
-Lemma map_singleton_update i (x y : A) : x ~~> y â†’ {[ i := x ]} ~~> {[ i := y ]}.
-Proof. apply map_insert_update. Qed.
+Proof. apply insert_updateP'. Qed.
+Lemma singleton_update i (x y : A) : x ~~> y â†’ {[ i := x ]} ~~> {[ i := y ]}.
+Proof. apply insert_update. Qed.
 
-Lemma map_singleton_updateP_empty `{Empty A, !CMRAUnit A}
+Lemma singleton_updateP_empty `{Empty A, !CMRAUnit A}
     (P : A â†’ Prop) (Q : gmap K A â†’ Prop) i :
   âˆ… ~~>: P â†’ (âˆ€ y, P y â†’ Q {[ i := y ]}) â†’ âˆ… ~~>: Q.
 Proof.
@@ -283,34 +279,34 @@ Proof.
     by rewrite right_id.
   - move:(Hg i'). by rewrite !lookup_op lookup_singleton_ne // !left_id.
 Qed.
-Lemma map_singleton_updateP_empty' `{Empty A, !CMRAUnit A} (P: A â†’ Prop) i :
+Lemma singleton_updateP_empty' `{Empty A, !CMRAUnit A} (P: A â†’ Prop) i :
   âˆ… ~~>: P â†’ âˆ… ~~>: Î» m, âˆƒ y, m = {[ i := y ]} âˆ§ P y.
-Proof. eauto using map_singleton_updateP_empty. Qed.
+Proof. eauto using singleton_updateP_empty. Qed.
 
 Section freshness.
 Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
-Lemma map_updateP_alloc_strong (Q : gmap K A â†’ Prop) (I : gset K) m x :
+Lemma updateP_alloc_strong (Q : gmap K A â†’ Prop) (I : gset K) m x :
   âœ“ x â†’ (âˆ€ i, m !! i = None â†’ i âˆ‰ I â†’ Q (<[i:=x]>m)) â†’ m ~~>: Q.
 Proof.
   intros ? HQ n mf Hm. set (i := fresh (I âˆª dom (gset K) (m â‹… mf))).
   assert (i âˆ‰ I âˆ§ i âˆ‰ dom (gset K) m âˆ§ i âˆ‰ dom (gset K) mf) as [?[??]].
-  { rewrite -not_elem_of_union -map_dom_op -not_elem_of_union; apply is_fresh. }
+  { rewrite -not_elem_of_union -dom_op -not_elem_of_union; apply is_fresh. }
   exists (<[i:=x]>m); split.
   { by apply HQ; last done; apply not_elem_of_dom. }
-  rewrite map_insert_singleton_opN; last by left; apply not_elem_of_dom.
-  rewrite -assoc -map_insert_singleton_opN;
-    last by left; apply not_elem_of_dom; rewrite map_dom_op not_elem_of_union.
-  by apply map_insert_validN; [apply cmra_valid_validN|].
+  rewrite insert_singleton_opN; last by left; apply not_elem_of_dom.
+  rewrite -assoc -insert_singleton_opN;
+    last by left; apply not_elem_of_dom; rewrite dom_op not_elem_of_union.
+  by apply insert_validN; [apply cmra_valid_validN|].
 Qed.
-Lemma map_updateP_alloc (Q : gmap K A â†’ Prop) m x :
+Lemma updateP_alloc (Q : gmap K A â†’ Prop) m x :
   âœ“ x â†’ (âˆ€ i, m !! i = None â†’ Q (<[i:=x]>m)) â†’ m ~~>: Q.
-Proof. move=>??. eapply map_updateP_alloc_strong with (I:=âˆ…); by eauto. Qed.
-Lemma map_updateP_alloc_strong' m x (I : gset K) :
+Proof. move=>??. eapply updateP_alloc_strong with (I:=âˆ…); by eauto. Qed.
+Lemma updateP_alloc_strong' m x (I : gset K) :
   âœ“ x â†’ m ~~>: Î» m', âˆƒ i, i âˆ‰ I âˆ§ m' = <[i:=x]>m âˆ§ m !! i = None.
-Proof. eauto using map_updateP_alloc_strong. Qed.
-Lemma map_updateP_alloc' m x :
+Proof. eauto using updateP_alloc_strong. Qed.
+Lemma updateP_alloc' m x :
   âœ“ x â†’ m ~~>: Î» m', âˆƒ i, m' = <[i:=x]>m âˆ§ m !! i = None.
-Proof. eauto using map_updateP_alloc. Qed.
+Proof. eauto using updateP_alloc. Qed.
 End freshness.
 
 (* Allocation is a local update: Just use composition with a singleton map. *)
@@ -319,7 +315,7 @@ End freshness.
    deallocation. *)
 
 (* Applying a local update at a position we own is a local update. *)
-Global Instance map_alter_update `{!LocalUpdate Lv L} i :
+Global Instance gmap_alter_update `{!LocalUpdate Lv L} i :
   LocalUpdate (Î» m, âˆƒ x, m !! i = Some x âˆ§ Lv x) (alter L i).
 Proof.
   split; first apply _.
@@ -332,32 +328,32 @@ Qed.
 End properties.
 
 (** Functor *)
-Instance map_fmap_ne `{Countable K} {A B : cofeT} (f : A â†’ B) n :
+Instance gmap_fmap_ne `{Countable K} {A B : cofeT} (f : A â†’ B) n :
   Proper (dist n ==> dist n) f â†’ Proper (dist n ==>dist n) (fmap (M:=gmap K) f).
 Proof. by intros ? m m' Hm k; rewrite !lookup_fmap; apply option_fmap_ne. Qed.
-Instance map_fmap_cmra_monotone `{Countable K} {A B : cmraT} (f : A â†’ B)
+Instance gmap_fmap_cmra_monotone `{Countable K} {A B : cmraT} (f : A â†’ B)
   `{!CMRAMonotone f} : CMRAMonotone (fmap f : gmap K A â†’ gmap K B).
 Proof.
   split; try apply _.
   - by intros n m ? i; rewrite lookup_fmap; apply (validN_preserving _).
-  - intros m1 m2; rewrite !map_included_spec=> Hm i.
+  - intros m1 m2; rewrite !gmap_included_spec=> Hm i.
     by rewrite !lookup_fmap; apply: included_preserving.
 Qed.
-Definition mapC_map `{Countable K} {A B} (f: A -n> B) : mapC K A -n> mapC K B :=
-  CofeMor (fmap f : mapC K A â†’ mapC K B).
-Instance mapC_map_ne `{Countable K} {A B} n :
-  Proper (dist n ==> dist n) (@mapC_map K _ _ A B).
+Definition gmapC_map `{Countable K} {A B} (f: A -n> B) :
+  gmapC K A -n> gmapC K B := CofeMor (fmap f : gmapC K A â†’ gmapC K B).
+Instance gmapC_map_ne `{Countable K} {A B} n :
+  Proper (dist n ==> dist n) (@gmapC_map K _ _ A B).
 Proof.
   intros f g Hf m k; rewrite /= !lookup_fmap.
   destruct (_ !! k) eqn:?; simpl; constructor; apply Hf.
 Qed.
 
-Program Definition mapCF K `{Countable K} (F : cFunctor) : cFunctor := {|
-  cFunctor_car A B := mapC K (cFunctor_car F A B);
-  cFunctor_map A1 A2 B1 B2 fg := mapC_map (cFunctor_map F fg)
+Program Definition gmapCF K `{Countable K} (F : cFunctor) : cFunctor := {|
+  cFunctor_car A B := gmapC K (cFunctor_car F A B);
+  cFunctor_map A1 A2 B1 B2 fg := gmapC_map (cFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros K ?? F A1 A2 B1 B2 n f g Hfg; apply mapC_map_ne, cFunctor_ne.
+  by intros K ?? F A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, cFunctor_ne.
 Qed.
 Next Obligation.
   intros K ?? F A B x. rewrite /= -{2}(map_fmap_id x).
@@ -367,18 +363,18 @@ Next Obligation.
   intros K ?? F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -map_fmap_compose.
   apply map_fmap_setoid_ext=>y ??; apply cFunctor_compose.
 Qed.
-Instance mapCF_contractive K `{Countable K} F :
-  cFunctorContractive F â†’ cFunctorContractive (mapCF K F).
+Instance gmapCF_contractive K `{Countable K} F :
+  cFunctorContractive F â†’ cFunctorContractive (gmapCF K F).
 Proof.
-  by intros ? A1 A2 B1 B2 n f g Hfg; apply mapC_map_ne, cFunctor_contractive.
+  by intros ? A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, cFunctor_contractive.
 Qed.
 
-Program Definition mapRF K `{Countable K} (F : rFunctor) : rFunctor := {|
-  rFunctor_car A B := mapR K (rFunctor_car F A B);
-  rFunctor_map A1 A2 B1 B2 fg := mapC_map (rFunctor_map F fg)
+Program Definition gmapRF K `{Countable K} (F : rFunctor) : rFunctor := {|
+  rFunctor_car A B := gmapR K (rFunctor_car F A B);
+  rFunctor_map A1 A2 B1 B2 fg := gmapC_map (rFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros K ?? F A1 A2 B1 B2 n f g Hfg; apply mapC_map_ne, rFunctor_ne.
+  by intros K ?? F A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, rFunctor_ne.
 Qed.
 Next Obligation.
   intros K ?? F A B x. rewrite /= -{2}(map_fmap_id x).
@@ -388,8 +384,8 @@ Next Obligation.
   intros K ?? F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -map_fmap_compose.
   apply map_fmap_setoid_ext=>y ??; apply rFunctor_compose.
 Qed.
-Instance mapRF_contractive K `{Countable K} F :
-  rFunctorContractive F â†’ rFunctorContractive (mapRF K F).
+Instance gmapRF_contractive K `{Countable K} F :
+  rFunctorContractive F â†’ rFunctorContractive (gmapRF K F).
 Proof.
-  by intros ? A1 A2 B1 B2 n f g Hfg; apply mapC_map_ne, rFunctor_contractive.
+  by intros ? A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, rFunctor_contractive.
 Qed.
diff --git a/heap_lang/lib/heap.v b/heap_lang/lib/heap.v
index fd0d90e90..88e25dac6 100644
--- a/heap_lang/lib/heap.v
+++ b/heap_lang/lib/heap.v
@@ -7,7 +7,7 @@ Import uPred.
    a finmap as their state. Or maybe even beyond "as their state", i.e. arbitrary
    predicates over finmaps instead of just ownP. *)
 
-Definition heapR : cmraT := mapR loc (fracR (dec_agreeR val)).
+Definition heapR : cmraT := gmapR loc (fracR (dec_agreeR val)).
 
 (** The CMRA we need. *)
 Class heapG Î£ := HeapG {
@@ -108,9 +108,9 @@ Section heap.
     induction Ïƒ as [|l v Ïƒ Hl IH] using map_ind.
     { rewrite big_sepM_empty; apply True_intro. }
     rewrite to_heap_insert big_sepM_insert //.
-    rewrite (map_insert_singleton_op (to_heap Ïƒ));
+    rewrite (insert_singleton_op (to_heap Ïƒ));
       last by rewrite lookup_fmap Hl; auto.
-    by rewrite auth_own_op IH. 
+    by rewrite auth_own_op IH.
   Qed.
 
   Context `{heapG Î£}.
@@ -121,16 +121,16 @@ Section heap.
 
   Lemma heap_mapsto_op_eq l q1 q2 v :
     (l â†¦{q1} v â˜… l â†¦{q2} v) âŠ£âŠ¢ (l â†¦{q1+q2} v).
-  Proof. by rewrite -auth_own_op map_op_singleton Frac_op dec_agree_idemp. Qed.
+  Proof. by rewrite -auth_own_op op_singleton Frac_op dec_agree_idemp. Qed.
 
   Lemma heap_mapsto_op l q1 q2 v1 v2 :
     (l â†¦{q1} v1 â˜… l â†¦{q2} v2) âŠ£âŠ¢ (v1 = v2 âˆ§ l â†¦{q1+q2} v1).
   Proof.
     destruct (decide (v1 = v2)) as [->|].
     { by rewrite heap_mapsto_op_eq const_equiv // left_id. }
-    rewrite -auth_own_op map_op_singleton Frac_op dec_agree_ne //.
+    rewrite -auth_own_op op_singleton Frac_op dec_agree_ne //.
     apply (anti_symm (âŠ¢)); last by apply const_elim_l.
-    rewrite auth_own_valid map_validI (forall_elim l) lookup_singleton.
+    rewrite auth_own_valid gmap_validI (forall_elim l) lookup_singleton.
     rewrite option_validI frac_validI discrete_valid. by apply const_elim_r.
   Qed.
 
@@ -160,8 +160,8 @@ Section heap.
     repeat erewrite <-exist_intro by apply _; simpl.
     rewrite -of_heap_insert left_id right_id.
     rewrite /heap_mapsto. ecancel [_ -â˜… Î¦ _]%I.
-    rewrite -(map_insert_singleton_op h); last by apply of_heap_None.
-    rewrite const_equiv; last by apply (map_insert_valid h).
+    rewrite -(insert_singleton_op h); last by apply of_heap_None.
+    rewrite const_equiv; last by apply (insert_valid h).
     by rewrite left_id -later_intro.
   Qed.
 
diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index 3955afbf0..a136bdbae 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -12,7 +12,7 @@ Typeclasses Opaque to_globalF own.
 
 (** Properties about ghost ownership *)
 Section global.
-Context `{i : inG Î› Î£ A}.
+Context `{inG Î› Î£ A}.
 Implicit Types a : A.
 
 (** * Transport empty *)
@@ -35,12 +35,12 @@ Global Instance own_proper Î³ : Proper ((â‰¡) ==> (âŠ£âŠ¢)) (own Î³) := ne_prope
 Lemma own_op Î³ a1 a2 : own Î³ (a1 â‹… a2) âŠ£âŠ¢ (own Î³ a1 â˜… own Î³ a2).
 Proof. by rewrite /own -ownG_op to_globalF_op. Qed.
 Global Instance own_mono Î³ : Proper (flip (â‰¼) ==> (âŠ¢)) (own Î³).
-Proof. move=>a b [c H]. rewrite H own_op. eauto with I. Qed.
+Proof. move=>a b [c ->]. rewrite own_op. eauto with I. Qed.
 Lemma own_valid Î³ a : own Î³ a âŠ¢ âœ“ a.
 Proof.
   rewrite /own ownG_valid /to_globalF.
   rewrite iprod_validI (forall_elim inG_id) iprod_lookup_singleton.
-  rewrite map_validI (forall_elim Î³) lookup_singleton option_validI.
+  rewrite gmap_validI (forall_elim Î³) lookup_singleton option_validI.
   (* implicit arguments differ a bit *)
   by trans (âœ“ cmra_transport inG_prf a : iPropG Î› Î£)%I; last destruct inG_prf.
 Qed.
@@ -60,8 +60,9 @@ Lemma own_alloc_strong a E (G : gset gname) :
 Proof.
   intros Ha.
   rewrite -(pvs_mono _ _ (âˆƒ m, â–  (âˆƒ Î³, Î³ âˆ‰ G âˆ§ m = to_globalF Î³ a) âˆ§ ownG m)%I).
-  - rewrite ownG_empty. eapply pvs_ownG_updateP, (iprod_singleton_updateP_empty inG_id);
-      first (eapply map_updateP_alloc_strong', cmra_transport_valid, Ha);
+  - rewrite ownG_empty.
+    eapply pvs_ownG_updateP, (iprod_singleton_updateP_empty inG_id);
+      first (eapply updateP_alloc_strong', cmra_transport_valid, Ha);
       naive_solver.
   - apply exist_elim=>m; apply const_elim_l=>-[Î³ [Hfresh ->]].
     by rewrite -(exist_intro Î³) const_equiv // left_id.
@@ -78,7 +79,7 @@ Proof.
   intros Ha.
   rewrite -(pvs_mono _ _ (âˆƒ m, â–  (âˆƒ a', m = to_globalF Î³ a' âˆ§ P a') âˆ§ ownG m)%I).
   - eapply pvs_ownG_updateP, iprod_singleton_updateP;
-      first by (eapply map_singleton_updateP', cmra_transport_updateP', Ha).
+      first by (eapply singleton_updateP', cmra_transport_updateP', Ha).
     naive_solver.
   - apply exist_elim=>m; apply const_elim_l=>-[a' [-> HP]].
     rewrite -(exist_intro a'). by apply and_intro; [apply const_intro|].
@@ -90,13 +91,12 @@ Proof.
   by apply pvs_mono, exist_elim=> a''; apply const_elim_l=> ->.
 Qed.
 
-Lemma own_empty `{Empty A, !CMRAUnit A} Î³ E :
-  True âŠ¢ (|={E}=> own Î³ âˆ…).
+Lemma own_empty `{Empty A, !CMRAUnit A} Î³ E : True âŠ¢ (|={E}=> own Î³ âˆ…).
 Proof.
   rewrite ownG_empty /own. apply pvs_ownG_update, cmra_update_updateP.
   eapply iprod_singleton_updateP_empty;
-      first by eapply map_singleton_updateP_empty', cmra_transport_updateP',
-               cmra_update_updateP, cmra_update_unit.
+    first by eapply singleton_updateP_empty', cmra_transport_updateP',
+    cmra_update_updateP, cmra_update_unit.
   naive_solver.
 Qed.
 End global.
diff --git a/program_logic/global_functor.v b/program_logic/global_functor.v
index 2e3bf775a..03219ee21 100644
--- a/program_logic/global_functor.v
+++ b/program_logic/global_functor.v
@@ -18,7 +18,7 @@ Definition gid (Î£ : gFunctors) := fin (projT1 Î£).
 Definition gname := positive.
 
 Definition globalF (Î£ : gFunctors) : iFunctor :=
-  IFunctor (iprodRF (Î» i, mapRF gname (projT2 Î£ i))).
+  IFunctor (iprodRF (Î» i, gmapRF gname (projT2 Î£ i))).
 Notation iPropG Î› Î£ := (iProp Î› (globalF Î£)).
 
 Class inG (Î› : language) (Î£ : gFunctors) (A : cmraT) := InG {
@@ -39,7 +39,7 @@ Proof. by intros a a' Ha; apply iprod_singleton_ne; rewrite Ha. Qed.
 Lemma to_globalF_op Î³ a1 a2 :
   to_globalF Î³ (a1 â‹… a2) â‰¡ to_globalF Î³ a1 â‹… to_globalF Î³ a2.
 Proof.
-  by rewrite /to_globalF iprod_op_singleton map_op_singleton cmra_transport_op.
+  by rewrite /to_globalF iprod_op_singleton op_singleton cmra_transport_op.
 Qed.
 Global Instance to_globalF_timeless Î³ m: Timeless m â†’ Timeless (to_globalF Î³ m).
 Proof. rewrite /to_globalF; apply _. Qed.
diff --git a/program_logic/ownership.v b/program_logic/ownership.v
index f89003cae..51a536405 100644
--- a/program_logic/ownership.v
+++ b/program_logic/ownership.v
@@ -65,7 +65,7 @@ Proof.
   rewrite /uPred_holds/=res_includedN/= singleton_includedN; split.
   - intros [(P'&Hi&HP) _]; rewrite Hi.
     apply Some_dist, symmetry, agree_valid_includedN; last done.
-    by apply map_lookup_validN with (wld r) i.
+    by apply lookup_validN with (wld r) i.
   - intros ?; split_and?; try apply cmra_unit_leastN; eauto.
 Qed.
 Lemma ownP_spec n r Ïƒ : âœ“{n} r â†’ (ownP Ïƒ) n r â†” pst r â‰¡ Excl Ïƒ.
diff --git a/program_logic/resources.v b/program_logic/resources.v
index 795899302..7d7714521 100644
--- a/program_logic/resources.v
+++ b/program_logic/resources.v
@@ -1,9 +1,9 @@
-From iris.algebra Require Export fin_maps agree excl.
+From iris.algebra Require Export gmap agree excl.
 From iris.algebra Require Import upred.
 From iris.program_logic Require Export language.
 
 Record res (Î› : language) (A : cofeT) (M : cmraT) := Res {
-  wld : mapR positive (agreeR A);
+  wld : gmapR positive (agreeR A);
   pst : exclR (stateC Î›);
   gst : M;
 }.
@@ -216,7 +216,7 @@ Instance resC_map_ne {Î› A A' M M'} n :
   Proper (dist n ==> dist n ==> dist n) (@resC_map Î› A A' M M').
 Proof.
   intros f g Hfg r; split; simpl; auto.
-  - by apply (mapC_map_ne _ (agreeC_map f) (agreeC_map g)), agreeC_map_ne.
+  - by apply (gmapC_map_ne _ (agreeC_map f) (agreeC_map g)), agreeC_map_ne.
 Qed.
 
 Program Definition resRF (Î› : language)
diff --git a/program_logic/wsat.v b/program_logic/wsat.v
index 7eee60b1e..70149985f 100644
--- a/program_logic/wsat.v
+++ b/program_logic/wsat.v
@@ -53,7 +53,7 @@ Proof.
   assert (P' â‰¡{S n}â‰¡ to_agree $ Next $ iProp_unfold $
                        iProp_fold $ later_car $ P' (S n)) as HPiso.
   { rewrite iProp_unfold_fold later_eta to_agree_car //.
-    apply (map_lookup_validN _ (wld (r â‹… big_opM rs)) i); rewrite ?HP'; auto. }
+    apply (lookup_validN _ (wld (r â‹… big_opM rs)) i); rewrite ?HP'; auto. }
   assert (P â‰¡{n'}â‰¡ iProp_fold (later_car (P' (S n)))) as HPP'.
   { apply (inj iProp_unfold), (inj Next), (inj to_agree).
     by rewrite -HiP -(dist_le _ _ _ _ HPiso). }
-- 
GitLab