Remove generality for COFE/CMRA maps.

modures/fin_maps.v

-Require Export modures.cmra.
-Require Import prelude.pmap prelude.natmap prelude.gmap modures.option.
+Require Export modures.cmra prelude.gmap.
+Require Import modures.option.
+Local Obligation Tactic := idtac.
 
 Section map.
-Context `{FinMap K M}.
+Context `{Countable K}.
 
 (* COFE *)
-Global Instance map_dist `{Dist A} : Dist (M A) := λ n m1 m2,
+Global Instance map_dist `{Dist A} : Dist (gmap K A) := λ n m1 m2,
   ∀ i, m1 !! i ={n}= m2 !! i.
-Program Definition map_chain `{Dist A} (c : chain (M A))
+Program Definition map_chain `{Dist A} (c : chain (gmap K A))
   (k : K) : chain (option A) := {| chain_car n := c n !! k |}.
 Next Obligation. by intros A ? c k n i ?; apply (chain_cauchy c). Qed.
-Global Instance map_compl `{Cofe A} : Compl (M A) := λ c,
+Global Instance map_compl `{Cofe A} : Compl (gmap K A) := λ c,
   map_imap (λ i _, compl (map_chain c i)) (c 1).
-Global Instance map_cofe `{Cofe A} : Cofe (M A).
+Global Instance map_cofe `{Cofe A} : Cofe (gmap K A).
 Proof.
   split.
   * intros m1 m2; split.
@@ -30,33 +31,33 @@ Proof.
     by rewrite conv_compl; simpl; apply reflexive_eq.
 Qed.
 Global Instance lookup_ne `{Dist A} n k :
-  Proper (dist n ==> dist n) (lookup k : M A → option A).
+  Proper (dist n ==> dist n) (lookup k : gmap K A → option A).
 Proof. by intros m1 m2. Qed.
 Global Instance insert_ne `{Dist A} (i : K) n :
-  Proper (dist n ==> dist n ==> dist n) (insert (M:=M A) i).
+  Proper (dist n ==> dist n ==> dist n) (insert (M:=gmap K A) i).
 Proof.
   intros x y ? m m' ? j; destruct (decide (i = j)); simplify_map_equality;
     [by constructor|by apply lookup_ne].
 Qed.
 Global Instance delete_ne `{Dist A} (i : K) n :
-  Proper (dist n ==> dist n) (delete (M:=M A) i).
+  Proper (dist n ==> dist n) (delete (M:=gmap K A) i).
 Proof.
   intros m m' ? j; destruct (decide (i = j)); simplify_map_equality;
     [by constructor|by apply lookup_ne].
 Qed.
-Global Instance map_empty_timeless `{Dist A, Equiv A} : Timeless (∅ : M A).
+Global Instance map_empty_timeless `{Dist A, Equiv A} : 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 `{Cofe A} (m : M A) i :
+Global Instance map_lookup_timeless `{Cofe A} (m : gmap K A) i :
   Timeless m → Timeless (m !! i).
 Proof.
   intros ? [x|] Hx; [|by symmetry; apply (timeless _)].
   rewrite (timeless m (<[i:=x]>m)), lookup_insert; auto.
   by symmetry in Hx; inversion Hx; cofe_subst; rewrite insert_id.
 Qed.
-Global Instance map_ra_insert_timeless `{Cofe A} (m : M A) i x :
+Global Instance map_ra_insert_timeless `{Cofe A} (m : gmap K A) i x :
   Timeless x → Timeless m → Timeless (<[i:=x]>m).
 Proof.
   intros ?? m' Hm j; destruct (decide (i = j)); simplify_map_equality.
@@ -64,11 +65,12 @@ Proof.
   by apply (timeless _); rewrite <-Hm, lookup_insert_ne by done.
 Qed.
 Global Instance map_ra_singleton_timeless `{Cofe A} (i : K) (x : A) :
-  Timeless x → Timeless ({[ i, x ]} : M A) := _.
+  Timeless x → Timeless ({[ i, x ]} : gmap K A) := _.
 Instance map_fmap_ne `{Dist A, Dist B} (f : A → B) n :
-  Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (fmap (M:=M) f).
+  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.
-Definition mapC (A : cofeT) : cofeT := CofeT (M A).
+Canonical Structure mapC (A : cofeT) : cofeT := CofeT (gmap K A).
 Definition mapC_map {A B} (f: A -n> B) : mapC A -n> mapC B :=
   CofeMor (fmap f : mapC A → mapC B).
 Global Instance mapC_map_ne {A B} n :
@@ -79,19 +81,19 @@ Proof.
 Qed.
 
 (* CMRA *)
-Global Instance map_op `{Op A} : Op (M A) := merge op.
-Global Instance map_unit `{Unit A} : Unit (M A) := fmap unit.
-Global Instance map_valid `{Valid A} : Valid (M A) := λ m, ∀ i, ✓ (m !! i).
-Global Instance map_validN `{ValidN A} : ValidN (M A) := λ n m,
+Global Instance map_op `{Op A} : Op (gmap K A) := merge op.
+Global Instance map_unit `{Unit A} : Unit (gmap K A) := fmap unit.
+Global Instance map_valid `{Valid A} : Valid (gmap K A) := λ m, ∀ i, ✓ (m !! i).
+Global Instance map_validN `{ValidN A} : ValidN (gmap K A) := λ n m,
   ∀ i, ✓{n} (m!!i).
-Global Instance map_minus `{Minus A} : Minus (M A) := merge minus.
+Global Instance map_minus `{Minus A} : Minus (gmap K A) := merge minus.
 Lemma lookup_op `{Op A} m1 m2 i : (m1 ⋅ m2) !! i = m1 !! i ⋅ m2 !! i.
 Proof. by apply lookup_merge. Qed.
 Lemma lookup_minus `{Minus A} m1 m2 i : (m1 ⩪ m2) !! i = m1 !! i ⩪ m2 !! i.
 Proof. by apply lookup_merge. Qed.
 Lemma lookup_unit `{Unit A} m i : unit m !! i = unit (m !! i).
 Proof. by apply lookup_fmap. Qed.
-Lemma map_included_spec `{CMRA A} (m1 m2 : M A) :
+Lemma map_included_spec `{CMRA A} (m1 m2 : gmap K A) :
   m1 ≼ m2 ↔ ∀ i, m1 !! i ≼ m2 !! i.
 Proof.
   split.
@@ -99,7 +101,7 @@ Proof.
   * intros Hm; exists (m2 ⩪ m1); intros i.
     by rewrite lookup_op, lookup_minus, ra_op_minus.
 Qed.
-Lemma map_includedN_spec `{CMRA A} (m1 m2 : M A) n :
+Lemma map_includedN_spec `{CMRA A} (m1 m2 : gmap K A) n :
   m1 ≼{n} m2 ↔ ∀ i, m1 !! i ≼{n} m2 !! i.
 Proof.
   split.
@@ -107,7 +109,7 @@ Proof.
   * intros Hm; exists (m2 ⩪ m1); intros i.
     by rewrite lookup_op, lookup_minus, cmra_op_minus.
 Qed.
-Global Instance map_cmra `{CMRA A} : CMRA (M A).
+Global Instance map_cmra `{CMRA A} : CMRA (gmap K A).
 Proof.
   split.
   * apply _.
@@ -131,13 +133,13 @@ Proof.
   * intros x y n; rewrite map_includedN_spec; intros ? i.
     by rewrite lookup_op, lookup_minus, cmra_op_minus by done.
 Qed.
-Global Instance map_ra_empty `{RA A} : RAIdentity (M A).
+Global Instance map_ra_empty `{RA A} : RAIdentity (gmap K A).
 Proof.
   split.
   * by intros ?; rewrite lookup_empty.
   * by intros m i; simpl; rewrite lookup_op, lookup_empty; destruct (m !! i).
 Qed.
-Global Instance map_cmra_extend `{CMRA A, !CMRAExtend A} : CMRAExtend (M A).
+Global Instance map_cmra_extend `{CMRA A, !CMRAExtend A} : CMRAExtend (gmap K A).
 Proof.
   intros n m m1 m2 Hm Hm12.
   assert (∀ i, m !! i ={n}= m1 !! i ⋅ m2 !! i) as Hm12'
@@ -156,9 +158,10 @@ Proof.
     by destruct (m1 !! i), (m2 !! i); inversion_clear Hm12''.
 Qed.
 Global Instance map_empty_valid_timeless `{Valid A, ValidN A} :
-  ValidTimeless (∅ : M A).
+  ValidTimeless (∅ : gmap K A).
 Proof. by intros ??; rewrite lookup_empty. Qed.
-Global Instance map_ra_insert_valid_timeless `{Valid A,ValidN A} (m: M A) i x:
+Global Instance map_ra_insert_valid_timeless `{Valid A, ValidN A}
+    (m : gmap K A) i x:
   ValidTimeless x → ValidTimeless m → m !! i = None →
   ValidTimeless (<[i:=x]>m).
 Proof.
@@ -169,20 +172,20 @@ Proof.
   by specialize (Hm j); simplify_map_equality.
 Qed.
 Global Instance map_ra_singleton_valid_timeless `{Valid A, ValidN A} (i : K) x :
-  ValidTimeless x → ValidTimeless ({[ i, x ]} : M A).
+  ValidTimeless x → ValidTimeless ({[ i, x ]} : gmap K A).
 Proof.
   intros ?; apply (map_ra_insert_valid_timeless _ _ _ _ _); simpl.
   by rewrite lookup_empty.
 Qed.
-Lemma map_insert_valid `{ValidN A} (m : M A) n i x :
+Lemma map_insert_valid `{ValidN A} (m : gmap K A) n i x :
   ✓{n} x → ✓{n} m → ✓{n} (<[i:=x]>m).
 Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_equality. Qed.
-Lemma map_insert_op `{Op A} (m1 m2 : M A) i x :
+Lemma map_insert_op `{Op A} (m1 m2 : gmap K A) i x :
   m2 !! i = None →  <[i:=x]>(m1 ⋅ m2) = <[i:=x]>m1 ⋅ m2.
 Proof. by intros Hi; apply (insert_merge_l _); rewrite Hi. Qed.
-Definition mapRA (A : cmraT) : cmraT := CMRAT (M A).
+Canonical Structure mapRA (A : cmraT) : cmraT := CMRAT (gmap K A).
 Global Instance map_fmap_cmra_monotone `{CMRA A, CMRA B} (f : A → B)
-  `{!CMRAMonotone f} : CMRAMonotone (fmap f : M A → M B).
+  `{!CMRAMonotone f} : CMRAMonotone (fmap f : gmap K A → gmap K B).
 Proof.
   split.
   * intros m1 m2 n; rewrite !map_includedN_spec; intros Hm i.
@@ -195,47 +198,27 @@ Global Instance mapRA_map_ne {A B} n :
   Proper (dist n ==> dist n) (@mapRA_map A B) := mapC_map_ne n.
 Global Instance mapRA_map_monotone {A B : cmraT} (f : A -n> B)
   `{!CMRAMonotone f} : CMRAMonotone (mapRA_map f) := _.
-End map.
-
-Section map_dom.
-  Context `{FinMapDom K M D, Fresh K D, !FreshSpec K D}.
-  Lemma map_dom_op `{Op A} (m1 m2: M A) : dom D (m1 ⋅ m2) ≡ dom D m1 ∪ dom D 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_update_alloc `{CMRA A} (m : M A) x :
-    ✓ x → m ⇝: λ m', ∃ i, m' = <[i:=x]>m ∧ m !! i = None.
-  Proof.
-    intros ? mf n Hm. set (i := fresh (dom D (m ⋅ mf))).
-    assert (i ∉ dom D m ∧ i ∉ dom D mf) as [??].
-    { rewrite <-not_elem_of_union, <-map_dom_op; apply is_fresh. }
-    exists (<[i:=x]>m); split; [exists i; split; [done|]|].
-    * by apply not_elem_of_dom.
-    * rewrite <-map_insert_op by (by apply not_elem_of_dom).
-      by apply map_insert_valid; [apply cmra_valid_validN|].
-  Qed.
-End map_dom.
 
-Arguments mapC {_} _ {_ _ _ _ _ _ _ _ _} _.
-Arguments mapRA {_} _ {_ _ _ _ _ _ _ _ _} _.
+Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
 
-Canonical Structure natmapC := mapC natmap.
-Definition natmapC_map {A B}
-  (f : A -n> B) : natmapC A -n> natmapC B := mapC_map f.
-Canonical Structure PmapC := mapC Pmap.
-Definition PmapC_map {A B} (f : A -n> B) : PmapC A -n> PmapC B := mapC_map f.
-Canonical Structure gmapC K `{Countable K} := mapC (gmap K).
-Definition gmapC_map `{Countable K} {A B}
-  (f : A -n> B) : gmapC K A -n> gmapC K B := mapC_map f.
-
-Canonical Structure natmapRA := mapRA natmap.
-Definition natmapRA_map {A B : cmraT}
-  (f : A -n> B) : natmapRA A -n> natmapRA B := mapRA_map f.
-Canonical Structure PmapRA := mapRA Pmap.
-Definition PmapRA_map {A B : cmraT}
-  (f : A -n> B) : PmapRA A -n> PmapRA B := mapRA_map f.
-Canonical Structure gmapRA K `{Countable K} := mapRA (gmap K).
-Definition gmapRA_map `{Countable K} {A B : cmraT}
-  (f : A -n> B) : gmapRA K A -n> gmapRA K B := mapRA_map f.
+Lemma map_dom_op `{Op A} (m1 m2 : gmap K A) :
+  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_update_alloc `{CMRA A} (m : gmap K A) x :
+  ✓ x → m ⇝: λ m', ∃ i, m' = <[i:=x]>m ∧ m !! i = None.
+Proof.
+  intros ? mf n Hm. set (i := fresh (dom (gset K) (m ⋅ mf))).
+  assert (i ∉ dom (gset K) m ∧ i ∉ dom (gset K) mf) as [??].
+  { rewrite <-not_elem_of_union, <-map_dom_op; apply is_fresh. }
+  exists (<[i:=x]>m); split; [exists i; split; [done|]|].
+  * by apply not_elem_of_dom.
+  * rewrite <-map_insert_op by (by apply not_elem_of_dom).
+    by apply map_insert_valid; [apply cmra_valid_validN|].
+Qed.
+End map.
+Arguments mapC _ {_ _} _.
+Arguments mapRA _ {_ _} _.