From a389ce1bcd0182654cdf99756824c11cd76ee7a2 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 9 May 2022 09:58:59 +0200
Subject: [PATCH] make dom D parameter implicit and adjust Dom Mode

---
 tests/fin_maps.v       |   4 +-
 tests/gmap.ref         |   2 +-
 tests/gmap.v           |   4 +-
 theories/base.v        |  10 ++-
 theories/fin_map_dom.v | 180 ++++++++++++++++++++---------------------
 theories/gmap.v        |   4 +-
 theories/gmultiset.v   |   4 +-
 7 files changed, 105 insertions(+), 103 deletions(-)

diff --git a/tests/fin_maps.v b/tests/fin_maps.v
index b81d06ae..2c5d5a81 100644
--- a/tests/fin_maps.v
+++ b/tests/fin_maps.v
@@ -16,9 +16,9 @@ Section map_dom.
   Context `{FinMapDom K M D}.
 
   Lemma set_solver_dom_subseteq {A} (i j : K) (x y : A) :
-    {[i; j]} ⊆ dom D (<[i:=x]> (<[j:=y]> (∅ : M A))).
+    {[i; j]} ⊆ dom (<[i:=x]> (<[j:=y]> (∅ : M A))).
   Proof. set_solver. Qed.
 
-  Lemma set_solver_dom_disjoint {A} (X : D) : dom D (∅ : M A) ## X.
+  Lemma set_solver_dom_disjoint {A} (X : D) : dom (∅ : M A) ## X.
   Proof. set_solver. Qed.
 End map_dom.
diff --git a/tests/gmap.ref b/tests/gmap.ref
index 8b1fa98f..b2c05bf2 100644
--- a/tests/gmap.ref
+++ b/tests/gmap.ref
@@ -29,7 +29,7 @@ Failed to progress.
 1 goal
   
   ============================
-  1 ∈ dom (gset nat) (<[1:=2]> ∅)
+  1 ∈ dom (<[1:=2]> ∅)
 The command has indeed failed with message:
 Failed to progress.
 The command has indeed failed with message:
diff --git a/tests/gmap.v b/tests/gmap.v
index 987c0fe6..3eb98b06 100644
--- a/tests/gmap.v
+++ b/tests/gmap.v
@@ -22,7 +22,7 @@ Proof.
   Show.
 Abort.
 
-Goal 1 ∈ dom (M := gmap nat nat) (gset nat) (<[ 1 := 2 ]> ∅).
+Goal 1 ∈ dom (M := gmap nat nat) (<[ 1 := 2 ]> ∅).
 Proof.
   Fail progress simpl.
   Fail progress cbn.
@@ -70,7 +70,7 @@ Proof.
 Qed.
 
 Lemma should_not_unfold (m1 m2 : gmap nat nat) k x :
-  dom (gset nat) m1 = dom (gset nat) m2 →
+  dom m1 = dom m2 →
   <[k:=x]> m1 = <[k:=x]> m2 →
   True.
 Proof.
diff --git a/theories/base.v b/theories/base.v
index 77abf35f..59118414 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -1303,13 +1303,15 @@ Global Hint Mode PartialAlter - - ! : typeclass_instances.
 Global Instance: Params (@partial_alter) 4 := {}.
 Global Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
 
-(** The function [dom C m] should yield the domain of [m]. That is a finite
-set of type [C] that contains the keys that are a member of [m]. *)
+(** The function [dom m] should yield the domain of [m]. That is a finite
+set of type [C] that contains the keys that are a member of [m].
+[C] is an output of the typeclass, i.e., there can be only one instance per map
+type [M]. *)
 Class Dom (M C : Type) := dom: M → C.
-Global Hint Mode Dom ! ! : typeclass_instances.
+Global Hint Mode Dom ! - : typeclass_instances.
 Global Instance: Params (@dom) 3 := {}.
 Global Arguments dom : clear implicits.
-Global Arguments dom {_} _ {_} !_ / : simpl nomatch, assert.
+Global Arguments dom {_ _ _} !_ / : simpl nomatch, assert.
 
 (** The function [merge f m1 m2] should merge the maps [m1] and [m2] by
 constructing a new map whose value at key [k] is [f (m1 !! k) (m2 !! k)].*)
diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index 4d9d66ef..f2be1b2a 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -14,40 +14,40 @@ Class FinMapDom K M D `{∀ A, Dom (M A) D, FMap M,
     Union D, Intersection D, Difference D} := {
   finmap_dom_map :> FinMap K M;
   finmap_dom_set :> Set_ K D;
-  elem_of_dom {A} (m : M A) i : i ∈ dom D m ↔ is_Some (m !! i)
+  elem_of_dom {A} (m : M A) i : i ∈ dom m ↔ is_Some (m !! i)
 }.
 
 Section fin_map_dom.
 Context `{FinMapDom K M D}.
 
 Lemma lookup_lookup_total_dom `{!Inhabited A} (m : M A) i :
-  i ∈ dom D m → m !! i = Some (m !!! i).
+  i ∈ dom m → m !! i = Some (m !!! i).
 Proof. rewrite elem_of_dom. apply lookup_lookup_total. Qed.
 
 Lemma dom_imap_subseteq {A B} (f: K → A → option B) (m: M A) :
-  dom D (map_imap f m) ⊆ dom D m.
+  dom (map_imap f m) ⊆ dom m.
 Proof.
   intros k. rewrite 2!elem_of_dom, map_lookup_imap.
   destruct 1 as [?[?[Eq _]]%bind_Some]. by eexists.
 Qed.
-Lemma dom_imap {A B} (f: K → A → option B) (m: M A) X :
+Lemma dom_imap {A B} (f : K → A → option B) (m : M A) (X : D) :
   (∀ i, i ∈ X ↔ ∃ x, m !! i = Some x ∧ is_Some (f i x)) →
-  dom D (map_imap f m) ≡ X.
+  dom (map_imap f m) ≡ X.
 Proof.
   intros HX k. rewrite elem_of_dom, HX, map_lookup_imap.
   unfold is_Some. setoid_rewrite bind_Some. naive_solver.
 Qed.
 
-Lemma elem_of_dom_2 {A} (m : M A) i x : m !! i = Some x → i ∈ dom D m.
+Lemma elem_of_dom_2 {A} (m : M A) i x : m !! i = Some x → i ∈ dom m.
 Proof. rewrite elem_of_dom; eauto. Qed.
-Lemma not_elem_of_dom {A} (m : M A) i : i ∉ dom D m ↔ m !! i = None.
+Lemma not_elem_of_dom {A} (m : M A) i : i ∉ dom m ↔ m !! i = None.
 Proof. by rewrite elem_of_dom, eq_None_not_Some. Qed.
-Lemma subseteq_dom {A} (m1 m2 : M A) : m1 ⊆ m2 → dom D m1 ⊆ dom D m2.
+Lemma subseteq_dom {A} (m1 m2 : M A) : m1 ⊆ m2 → dom m1 ⊆ dom m2.
 Proof.
   rewrite map_subseteq_spec.
   intros ??. rewrite !elem_of_dom. inversion 1; eauto.
 Qed.
-Lemma subset_dom {A} (m1 m2 : M A) : m1 ⊂ m2 → dom D m1 ⊂ dom D m2.
+Lemma subset_dom {A} (m1 m2 : M A) : m1 ⊂ m2 → dom m1 ⊂ dom m2.
 Proof.
   intros [Hss1 Hss2]; split; [by apply subseteq_dom |].
   contradict Hss2. rewrite map_subseteq_spec. intros i x Hi.
@@ -55,110 +55,110 @@ Proof.
   destruct Hss2; eauto. by simplify_map_eq.
 Qed.
 
-Lemma dom_filter {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) X :
+Lemma dom_filter {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) (X : D) :
   (∀ i, i ∈ X ↔ ∃ x, m !! i = Some x ∧ P (i, x)) →
-  dom D (filter P m) ≡ X.
+  dom (filter P m) ≡ X.
 Proof.
   intros HX i. rewrite elem_of_dom, HX.
   unfold is_Some. by setoid_rewrite map_filter_lookup_Some.
 Qed.
 Lemma dom_filter_subseteq {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A):
-  dom D (filter P m) ⊆ dom D m.
+  dom (filter P m) ⊆ dom m.
 Proof. apply subseteq_dom, map_filter_subseteq. Qed.
 
-Lemma dom_empty {A} : dom D (@empty (M A) _) ≡ ∅.
+Lemma dom_empty {A} : dom (@empty (M A) _) ≡@{D} ∅.
 Proof.
   intros x. rewrite elem_of_dom, lookup_empty, <-not_eq_None_Some. set_solver.
 Qed.
-Lemma dom_empty_iff {A} (m : M A) : dom D m ≡ ∅ ↔ m = ∅.
+Lemma dom_empty_iff {A} (m : M A) : dom m ≡@{D} ∅ ↔ m = ∅.
 Proof.
   split; [|intros ->; by rewrite dom_empty].
   intros E. apply map_empty. intros. apply not_elem_of_dom.
   rewrite E. set_solver.
 Qed.
-Lemma dom_empty_inv {A} (m : M A) : dom D m ≡ ∅ → m = ∅.
+Lemma dom_empty_inv {A} (m : M A) : dom m ≡@{D} ∅ → m = ∅.
 Proof. apply dom_empty_iff. Qed.
-Lemma dom_alter {A} f (m : M A) i : dom D (alter f i m) ≡ dom D m.
+Lemma dom_alter {A} f (m : M A) i : dom (alter f i m) ≡@{D} dom m.
 Proof.
   apply set_equiv; intros j; rewrite !elem_of_dom; unfold is_Some.
   destruct (decide (i = j)); simplify_map_eq/=; eauto.
   destruct (m !! j); naive_solver.
 Qed.
-Lemma dom_insert {A} (m : M A) i x : dom D (<[i:=x]>m) ≡ {[ i ]} ∪ dom D m.
+Lemma dom_insert {A} (m : M A) i x : dom (<[i:=x]>m) ≡@{D} {[ i ]} ∪ dom m.
 Proof.
   apply set_equiv. intros j. rewrite elem_of_union, !elem_of_dom.
   unfold is_Some. setoid_rewrite lookup_insert_Some.
   destruct (decide (i = j)); set_solver.
 Qed.
 Lemma dom_insert_lookup {A} (m : M A) i x :
-  is_Some (m !! i) → dom D (<[i:=x]>m) ≡ dom D m.
+  is_Some (m !! i) → dom (<[i:=x]>m) ≡@{D} dom m.
 Proof.
-  intros Hindom. assert (i ∈ dom D m) by by apply elem_of_dom.
+  intros Hindom. assert (i ∈ dom m) by by apply elem_of_dom.
   rewrite dom_insert. set_solver.
 Qed.
-Lemma dom_insert_subseteq {A} (m : M A) i x : dom D m ⊆ dom D (<[i:=x]>m).
+Lemma dom_insert_subseteq {A} (m : M A) i x : dom m ⊆ dom (<[i:=x]>m).
 Proof. rewrite (dom_insert _). set_solver. Qed.
 Lemma dom_insert_subseteq_compat_l {A} (m : M A) i x X :
-  X ⊆ dom D m → X ⊆ dom D (<[i:=x]>m).
-Proof. intros. trans (dom D m); eauto using dom_insert_subseteq. Qed.
-Lemma dom_singleton {A} (i : K) (x : A) : dom D ({[i := x]} : M A) ≡ {[ i ]}.
+  X ⊆ dom m → X ⊆ dom (<[i:=x]>m).
+Proof. intros. trans (dom m); eauto using dom_insert_subseteq. Qed.
+Lemma dom_singleton {A} (i : K) (x : A) : dom ({[i := x]} : M A) ≡@{D} {[ i ]}.
 Proof. rewrite <-insert_empty, dom_insert, dom_empty; set_solver. Qed.
-Lemma dom_delete {A} (m : M A) i : dom D (delete i m) ≡ dom D m ∖ {[ i ]}.
+Lemma dom_delete {A} (m : M A) i : dom (delete i m) ≡@{D} dom m ∖ {[ i ]}.
 Proof.
   apply set_equiv. intros j. rewrite elem_of_difference, !elem_of_dom.
   unfold is_Some. setoid_rewrite lookup_delete_Some. set_solver.
 Qed.
 Lemma delete_partial_alter_dom {A} (m : M A) i f :
-  i ∉ dom D m → delete i (partial_alter f i m) = m.
+  i ∉ dom m → delete i (partial_alter f i m) = m.
 Proof. rewrite not_elem_of_dom. apply delete_partial_alter. Qed.
 Lemma delete_insert_dom {A} (m : M A) i x :
-  i ∉ dom D m → delete i (<[i:=x]>m) = m.
+  i ∉ dom m → delete i (<[i:=x]>m) = m.
 Proof. rewrite not_elem_of_dom. apply delete_insert. Qed.
-Lemma map_disjoint_dom {A} (m1 m2 : M A) : m1 ##ₘ m2 ↔ dom D m1 ## dom D m2.
+Lemma map_disjoint_dom {A} (m1 m2 : M A) : m1 ##ₘ m2 ↔ dom m1 ## dom m2.
 Proof.
   rewrite map_disjoint_spec, elem_of_disjoint.
   setoid_rewrite elem_of_dom. unfold is_Some. naive_solver.
 Qed.
-Lemma map_disjoint_dom_1 {A} (m1 m2 : M A) : m1 ##ₘ m2 → dom D m1 ## dom D m2.
+Lemma map_disjoint_dom_1 {A} (m1 m2 : M A) : m1 ##ₘ m2 → dom m1 ## dom m2.
 Proof. apply map_disjoint_dom. Qed.
-Lemma map_disjoint_dom_2 {A} (m1 m2 : M A) : dom D m1 ## dom D m2 → m1 ##ₘ m2.
+Lemma map_disjoint_dom_2 {A} (m1 m2 : M A) : dom m1 ## dom m2 → m1 ##ₘ m2.
 Proof. apply map_disjoint_dom. Qed.
-Lemma dom_union {A} (m1 m2 : M A) : dom D (m1 ∪ m2) ≡ dom D m1 ∪ dom D m2.
+Lemma dom_union {A} (m1 m2 : M A) : dom (m1 ∪ m2) ≡@{D} dom m1 ∪ dom m2.
 Proof.
   apply set_equiv. intros i. rewrite elem_of_union, !elem_of_dom.
   unfold is_Some. setoid_rewrite lookup_union_Some_raw.
   destruct (m1 !! i); naive_solver.
 Qed.
-Lemma dom_intersection {A} (m1 m2: M A) : dom D (m1 ∩ m2) ≡ dom D m1 ∩ dom D m2.
+Lemma dom_intersection {A} (m1 m2: M A) : dom (m1 ∩ m2) ≡@{D} dom m1 ∩ dom m2.
 Proof.
   apply set_equiv. intros i. rewrite elem_of_intersection, !elem_of_dom.
   unfold is_Some. setoid_rewrite lookup_intersection_Some. naive_solver.
 Qed.
-Lemma dom_difference {A} (m1 m2 : M A) : dom D (m1 ∖ m2) ≡ dom D m1 ∖ dom D m2.
+Lemma dom_difference {A} (m1 m2 : M A) : dom (m1 ∖ m2) ≡@{D} dom m1 ∖ dom m2.
 Proof.
   apply set_equiv. intros i. rewrite elem_of_difference, !elem_of_dom.
   unfold is_Some. setoid_rewrite lookup_difference_Some.
   destruct (m2 !! i); naive_solver.
 Qed.
-Lemma dom_fmap {A B} (f : A → B) (m : M A) : dom D (f <$> m) ≡ dom D m.
+Lemma dom_fmap {A B} (f : A → B) (m : M A) : dom (f <$> m) ≡@{D} dom m.
 Proof.
   apply set_equiv. intros i.
   rewrite !elem_of_dom, lookup_fmap, <-!not_eq_None_Some.
   destruct (m !! i); naive_solver.
 Qed.
-Lemma dom_finite {A} (m : M A) : set_finite (dom D m).
+Lemma dom_finite {A} (m : M A) : set_finite (dom m).
 Proof.
   induction m using map_ind; rewrite ?dom_empty, ?dom_insert.
   - by apply empty_finite.
   - apply union_finite; [apply singleton_finite|done].
 Qed.
-Global Instance dom_proper `{!Equiv A} : Proper ((≡@{M A}) ==> (≡)) (dom D).
+Global Instance dom_proper `{!Equiv A} : Proper ((≡@{M A}) ==> (≡@{D})) (dom).
 Proof.
   intros m1 m2 EQm. apply set_equiv. intros i.
   rewrite !elem_of_dom, EQm. done.
 Qed.
 Lemma dom_list_to_map {A} (l : list (K * A)) :
-  dom D (list_to_map l : M A) ≡ list_to_set l.*1.
+  dom (list_to_map l : M A) ≡@{D} list_to_set l.*1.
 Proof.
   induction l as [|?? IH].
   - by rewrite dom_empty.
@@ -167,7 +167,7 @@ Qed.
 
 (** Alternative definition of [dom] in terms of [map_to_list]. *)
 Lemma dom_alt {A} (m : M A) :
-  dom D m ≡ list_to_set (map_to_list m).*1.
+  dom m ≡@{D} list_to_set (map_to_list m).*1.
 Proof.
   rewrite <-(list_to_map_to_list m) at 1.
   rewrite dom_list_to_map.
@@ -175,7 +175,7 @@ Proof.
 Qed.
 
 Lemma size_dom `{!Elements K D, !FinSet K D} {A} (m : M A) :
-  size (dom D m) = size m.
+  size (dom m) = size m.
 Proof.
   rewrite dom_alt, size_list_to_set.
   2:{ apply NoDup_fst_map_to_list. }
@@ -183,7 +183,7 @@ Proof.
 Qed.
 
 Lemma dom_singleton_inv {A} (m : M A) i :
-  dom D m ≡ {[i]} → ∃ x, m = {[i := x]}.
+  dom m ≡@{D} {[i]} → ∃ x, m = {[i := x]}.
 Proof.
   intros Hdom. assert (is_Some (m !! i)) as [x ?].
   { apply (elem_of_dom (D:=D)); set_solver. }
@@ -193,7 +193,7 @@ Proof.
 Qed.
 
 Lemma dom_map_zip_with {A B C} (f : A → B → C) (ma : M A) (mb : M B) :
-  dom D (map_zip_with f ma mb) ≡ dom D ma ∩ dom D mb.
+  dom (map_zip_with f ma mb) ≡@{D} dom ma ∩ dom mb.
 Proof.
   rewrite set_equiv. intros x.
   rewrite elem_of_intersection, !elem_of_dom, map_lookup_zip_with.
@@ -202,8 +202,8 @@ Qed.
 
 Lemma dom_union_inv `{!RelDecision (∈@{D})} {A} (m : M A) (X1 X2 : D) :
   X1 ## X2 →
-  dom D m ≡ X1 ∪ X2 →
-  ∃ m1 m2, m = m1 ∪ m2 ∧ m1 ##ₘ m2 ∧ dom D m1 ≡ X1 ∧ dom D m2 ≡ X2.
+  dom m ≡ X1 ∪ X2 →
+  ∃ m1 m2, m = m1 ∪ m2 ∧ m1 ##ₘ m2 ∧ dom m1 ≡ X1 ∧ dom m2 ≡ X2.
 Proof.
   intros.
   exists (filter (λ '(k,x), k ∈ X1) m), (filter (λ '(k,x), k ∉ X1) m).
@@ -226,7 +226,7 @@ Qed.
 
 Lemma dom_kmap `{!Elements K D, !FinSet K D, FinMapDom K2 M2 D2}
     {A} (f : K → K2) `{!Inj (=) (=) f} (m : M A) :
-  dom D2 (kmap (M2:=M2) f m) ≡ set_map f (dom D m).
+  dom (kmap (M2:=M2) f m) ≡@{D2} set_map f (dom m).
 Proof.
   apply set_equiv. intros i.
   rewrite !elem_of_dom, (lookup_kmap_is_Some _), elem_of_map.
@@ -237,128 +237,128 @@ Qed.
 common case e.g. when having a [gmap K A] where the key [K] has Leibniz equality
 (and thus also [gset K], the usual domain) but the value type [A] does not. *)
 Global Instance dom_proper_L `{!Equiv A, !LeibnizEquiv D} :
-  Proper ((≡@{M A}) ==> (=)) (dom D) | 0.
+  Proper ((≡@{M A}) ==> (=)) (dom) | 0.
 Proof. intros ???. unfold_leibniz. by apply dom_proper. Qed.
 
 Section leibniz.
   Context `{!LeibnizEquiv D}.
   Lemma dom_filter_L {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) X :
     (∀ i, i ∈ X ↔ ∃ x, m !! i = Some x ∧ P (i, x)) →
-    dom D (filter P m) = X.
+    dom (filter P m) = X.
   Proof. unfold_leibniz. apply dom_filter. Qed.
-  Lemma dom_empty_L {A} : dom D (@empty (M A) _) = ∅.
+  Lemma dom_empty_L {A} : dom (@empty (M A) _) = ∅.
   Proof. unfold_leibniz; apply dom_empty. Qed.
-  Lemma dom_empty_iff_L {A} (m : M A) : dom D m = ∅ ↔ m = ∅.
+  Lemma dom_empty_iff_L {A} (m : M A) : dom m = ∅ ↔ m = ∅.
   Proof. unfold_leibniz. apply dom_empty_iff. Qed.
-  Lemma dom_empty_inv_L {A} (m : M A) : dom D m = ∅ → m = ∅.
+  Lemma dom_empty_inv_L {A} (m : M A) : dom m = ∅ → m = ∅.
   Proof. by intros; apply dom_empty_inv; unfold_leibniz. Qed.
-  Lemma dom_alter_L {A} f (m : M A) i : dom D (alter f i m) = dom D m.
+  Lemma dom_alter_L {A} f (m : M A) i : dom (alter f i m) = dom m.
   Proof. unfold_leibniz; apply dom_alter. Qed.
-  Lemma dom_insert_L {A} (m : M A) i x : dom D (<[i:=x]>m) = {[ i ]} ∪ dom D m.
+  Lemma dom_insert_L {A} (m : M A) i x : dom (<[i:=x]>m) = {[ i ]} ∪ dom m.
   Proof. unfold_leibniz; apply dom_insert. Qed.
   Lemma dom_insert_lookup_L {A} (m : M A) i x :
-    is_Some (m !! i) → dom D (<[i:=x]>m) = dom D m.
+    is_Some (m !! i) → dom (<[i:=x]>m) = dom m.
   Proof. unfold_leibniz; apply dom_insert_lookup. Qed.
-  Lemma dom_singleton_L {A} (i : K) (x : A) : dom D ({[i := x]} : M A) = {[ i ]}.
+  Lemma dom_singleton_L {A} (i : K) (x : A) : dom ({[i := x]} : M A) = {[ i ]}.
   Proof. unfold_leibniz; apply dom_singleton. Qed.
-  Lemma dom_delete_L {A} (m : M A) i : dom D (delete i m) = dom D m ∖ {[ i ]}.
+  Lemma dom_delete_L {A} (m : M A) i : dom (delete i m) = dom m ∖ {[ i ]}.
   Proof. unfold_leibniz; apply dom_delete. Qed.
-  Lemma dom_union_L {A} (m1 m2 : M A) : dom D (m1 ∪ m2) = dom D m1 ∪ dom D m2.
+  Lemma dom_union_L {A} (m1 m2 : M A) : dom (m1 ∪ m2) = dom m1 ∪ dom m2.
   Proof. unfold_leibniz; apply dom_union. Qed.
   Lemma dom_intersection_L {A} (m1 m2 : M A) :
-    dom D (m1 ∩ m2) = dom D m1 ∩ dom D m2.
+    dom (m1 ∩ m2) = dom m1 ∩ dom m2.
   Proof. unfold_leibniz; apply dom_intersection. Qed.
-  Lemma dom_difference_L {A} (m1 m2 : M A) : dom D (m1 ∖ m2) = dom D m1 ∖ dom D m2.
+  Lemma dom_difference_L {A} (m1 m2 : M A) : dom (m1 ∖ m2) = dom m1 ∖ dom m2.
   Proof. unfold_leibniz; apply dom_difference. Qed.
-  Lemma dom_fmap_L {A B} (f : A → B) (m : M A) : dom D (f <$> m) = dom D m.
+  Lemma dom_fmap_L {A B} (f : A → B) (m : M A) : dom (f <$> m) = dom m.
   Proof. unfold_leibniz; apply dom_fmap. Qed.
   Lemma dom_imap_L {A B} (f: K → A → option B) (m: M A) X :
     (∀ i, i ∈ X ↔ ∃ x, m !! i = Some x ∧ is_Some (f i x)) →
-    dom D (map_imap f m) = X.
+    dom (map_imap f m) = X.
   Proof. unfold_leibniz; apply dom_imap. Qed.
   Lemma dom_list_to_map_L {A} (l : list (K * A)) :
-    dom D (list_to_map l : M A) = list_to_set l.*1.
+    dom (list_to_map l : M A) = list_to_set l.*1.
   Proof. unfold_leibniz. apply dom_list_to_map. Qed.
   Lemma dom_singleton_inv_L {A} (m : M A) i :
-    dom D m = {[i]} → ∃ x, m = {[i := x]}.
+    dom m = {[i]} → ∃ x, m = {[i := x]}.
   Proof. unfold_leibniz. apply dom_singleton_inv. Qed.
   Lemma dom_map_zip_with_L {A B C} (f : A → B → C) (ma : M A) (mb : M B) :
-    dom D (map_zip_with f ma mb) = dom D ma ∩ dom D mb.
+    dom (map_zip_with f ma mb) = dom ma ∩ dom mb.
   Proof. unfold_leibniz. apply dom_map_zip_with. Qed.
   Lemma dom_union_inv_L `{!RelDecision (∈@{D})} {A} (m : M A) (X1 X2 : D) :
     X1 ## X2 →
-    dom D m = X1 ∪ X2 →
-    ∃ m1 m2, m = m1 ∪ m2 ∧ m1 ##ₘ m2 ∧ dom D m1 = X1 ∧ dom D m2 = X2.
+    dom m = X1 ∪ X2 →
+    ∃ m1 m2, m = m1 ∪ m2 ∧ m1 ##ₘ m2 ∧ dom m1 = X1 ∧ dom m2 = X2.
   Proof. unfold_leibniz. apply dom_union_inv. Qed.
 End leibniz.
 
 Lemma dom_kmap_L `{!Elements K D, !FinSet K D, FinMapDom K2 M2 D2}
     `{!LeibnizEquiv D2} {A} (f : K → K2) `{!Inj (=) (=) f} (m : M A) :
-  dom D2 (kmap (M2:=M2) f m) = set_map f (dom D m).
+  dom (kmap (M2:=M2) f m) = set_map f (dom m).
 Proof. unfold_leibniz. by apply dom_kmap. Qed.
 
 (** * Set solver instances *)
-Global Instance set_unfold_dom_empty {A} i : SetUnfoldElemOf i (dom D (∅:M A)) False.
+Global Instance set_unfold_dom_empty {A} i : SetUnfoldElemOf i (dom (∅:M A)) False.
 Proof. constructor. by rewrite dom_empty, elem_of_empty. Qed.
 Global Instance set_unfold_dom_alter {A} f i j (m : M A) Q :
-  SetUnfoldElemOf i (dom D m) Q →
-  SetUnfoldElemOf i (dom D (alter f j m)) Q.
-Proof. constructor. by rewrite dom_alter, (set_unfold_elem_of _ (dom _ _) _). Qed.
+  SetUnfoldElemOf i (dom m) Q →
+  SetUnfoldElemOf i (dom (alter f j m)) Q.
+Proof. constructor. by rewrite dom_alter, (set_unfold_elem_of _ (dom _) _). Qed.
 Global Instance set_unfold_dom_insert {A} i j x (m : M A) Q :
-  SetUnfoldElemOf i (dom D m) Q →
-  SetUnfoldElemOf i (dom D (<[j:=x]> m)) (i = j ∨ Q).
+  SetUnfoldElemOf i (dom m) Q →
+  SetUnfoldElemOf i (dom (<[j:=x]> m)) (i = j ∨ Q).
 Proof.
   constructor. by rewrite dom_insert, elem_of_union,
-    (set_unfold_elem_of _ (dom _ _) _), elem_of_singleton.
+    (set_unfold_elem_of _ (dom _) _), elem_of_singleton.
 Qed.
 Global Instance set_unfold_dom_delete {A} i j (m : M A) Q :
-  SetUnfoldElemOf i (dom D m) Q →
-  SetUnfoldElemOf i (dom D (delete j m)) (Q ∧ i ≠ j).
+  SetUnfoldElemOf i (dom m) Q →
+  SetUnfoldElemOf i (dom (delete j m)) (Q ∧ i ≠ j).
 Proof.
   constructor. by rewrite dom_delete, elem_of_difference,
-    (set_unfold_elem_of _ (dom _ _) _), elem_of_singleton.
+    (set_unfold_elem_of _ (dom _) _), elem_of_singleton.
 Qed.
 Global Instance set_unfold_dom_singleton {A} i j x :
-  SetUnfoldElemOf i (dom D ({[ j := x ]} : M A)) (i = j).
+  SetUnfoldElemOf i (dom ({[ j := x ]} : M A)) (i = j).
 Proof. constructor. by rewrite dom_singleton, elem_of_singleton. Qed.
 Global Instance set_unfold_dom_union {A} i (m1 m2 : M A) Q1 Q2 :
-  SetUnfoldElemOf i (dom D m1) Q1 → SetUnfoldElemOf i (dom D m2) Q2 →
-  SetUnfoldElemOf i (dom D (m1 ∪ m2)) (Q1 ∨ Q2).
+  SetUnfoldElemOf i (dom m1) Q1 → SetUnfoldElemOf i (dom m2) Q2 →
+  SetUnfoldElemOf i (dom (m1 ∪ m2)) (Q1 ∨ Q2).
 Proof.
   constructor. by rewrite dom_union, elem_of_union,
-    !(set_unfold_elem_of _ (dom _ _) _).
+    !(set_unfold_elem_of _ (dom _) _).
 Qed.
 Global Instance set_unfold_dom_intersection {A} i (m1 m2 : M A) Q1 Q2 :
-  SetUnfoldElemOf i (dom D m1) Q1 → SetUnfoldElemOf i (dom D m2) Q2 →
-  SetUnfoldElemOf i (dom D (m1 ∩ m2)) (Q1 ∧ Q2).
+  SetUnfoldElemOf i (dom m1) Q1 → SetUnfoldElemOf i (dom m2) Q2 →
+  SetUnfoldElemOf i (dom (m1 ∩ m2)) (Q1 ∧ Q2).
 Proof.
   constructor. by rewrite dom_intersection, elem_of_intersection,
-    !(set_unfold_elem_of _ (dom _ _) _).
+    !(set_unfold_elem_of _ (dom _) _).
 Qed.
 Global Instance set_unfold_dom_difference {A} i (m1 m2 : M A) Q1 Q2 :
-  SetUnfoldElemOf i (dom D m1) Q1 → SetUnfoldElemOf i (dom D m2) Q2 →
-  SetUnfoldElemOf i (dom D (m1 ∖ m2)) (Q1 ∧ ¬Q2).
+  SetUnfoldElemOf i (dom m1) Q1 → SetUnfoldElemOf i (dom m2) Q2 →
+  SetUnfoldElemOf i (dom (m1 ∖ m2)) (Q1 ∧ ¬Q2).
 Proof.
   constructor. by rewrite dom_difference, elem_of_difference,
-    !(set_unfold_elem_of _ (dom _ _) _).
+    !(set_unfold_elem_of _ (dom _) _).
 Qed.
 Global Instance set_unfold_dom_fmap {A B} (f : A → B) i (m : M A) Q :
-  SetUnfoldElemOf i (dom D m) Q →
-  SetUnfoldElemOf i (dom D (f <$> m)) Q.
-Proof. constructor. by rewrite dom_fmap, (set_unfold_elem_of _ (dom _ _) _). Qed.
+  SetUnfoldElemOf i (dom m) Q →
+  SetUnfoldElemOf i (dom (f <$> m)) Q.
+Proof. constructor. by rewrite dom_fmap, (set_unfold_elem_of _ (dom _) _). Qed.
 End fin_map_dom.
 
 Lemma dom_seq `{FinMapDom nat M D} {A} start (xs : list A) :
-  dom D (map_seq start (M:=M A) xs) ≡ set_seq start (length xs).
+  dom (map_seq start (M:=M A) xs) ≡@{D} set_seq start (length xs).
 Proof.
   revert start. induction xs as [|x xs IH]; intros start; simpl.
   - by rewrite dom_empty.
   - by rewrite dom_insert, IH.
 Qed.
 Lemma dom_seq_L `{FinMapDom nat M D, !LeibnizEquiv D} {A} start (xs : list A) :
-  dom D (map_seq (M:=M A) start xs) = set_seq start (length xs).
+  dom (map_seq (M:=M A) start xs) = set_seq start (length xs).
 Proof. unfold_leibniz. apply dom_seq. Qed.
 
 Global Instance set_unfold_dom_seq `{FinMapDom nat M D} {A} start (xs : list A) i :
-  SetUnfoldElemOf i (dom D (map_seq start (M:=M A) xs)) (start ≤ i < start + length xs).
+  SetUnfoldElemOf i (dom (map_seq start (M:=M A) xs)) (start ≤ i < start + length xs).
 Proof. constructor. by rewrite dom_seq, elem_of_set_seq. Qed.
diff --git a/theories/gmap.v b/theories/gmap.v
index 256b05e9..8630a22a 100644
--- a/theories/gmap.v
+++ b/theories/gmap.v
@@ -333,7 +333,7 @@ Section gset.
     by simplify_option_eq.
   Qed.
   Lemma gset_to_gmap_dom {A B} (m : gmap K A) (y : B) :
-    gset_to_gmap y (dom _ m) = const y <$> m.
+    gset_to_gmap y (dom m) = const y <$> m.
   Proof.
     apply map_eq; intros j. rewrite lookup_fmap, lookup_gset_to_gmap.
     destruct (m !! j) as [x|] eqn:?.
@@ -341,7 +341,7 @@ Section gset.
     - by rewrite option_guard_False by (rewrite not_elem_of_dom; eauto).
   Qed.
   Lemma dom_gset_to_gmap {A} (X : gset K) (x : A) :
-    dom _ (gset_to_gmap x X) = X.
+    dom (gset_to_gmap x X) = X.
   Proof.
     induction X as [| y X not_in IH] using set_ind_L.
     - rewrite gset_to_gmap_empty, dom_empty_L; done.
diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index 730e3061..dabfc11f 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -50,7 +50,7 @@ Section definitions.
       let z := x - y in guard (0 < z); Some (pred z)) X Y.
 
   Global Instance gmultiset_dom : Dom (gmultiset A) (gset A) := λ X,
-    let (X) := X in dom _ X.
+    let (X) := X in dom X.
 End definitions.
 
 Typeclasses Opaque gmultiset_elem_of gmultiset_subseteq.
@@ -454,7 +454,7 @@ Section more_lemmas.
       exists (x,n); split; [|by apply elem_of_map_to_list].
       apply elem_of_replicate; auto with lia.
   Qed.
-  Lemma gmultiset_elem_of_dom x X : x ∈ dom (gset A) X ↔ x ∈ X.
+  Lemma gmultiset_elem_of_dom x X : x ∈ dom X ↔ x ∈ X.
   Proof.
     unfold dom, gmultiset_dom, elem_of at 2, gmultiset_elem_of, multiplicity.
     destruct X as [X]; simpl; rewrite elem_of_dom, <-not_eq_None_Some.
-- 
GitLab