theories/fin_maps.v

@@ -1975,14 +1975,14 @@ Section map_seq.
     - by rewrite IH, Nat.add_succ_r, !insert_union_singleton_l, (assoc_L _).
   Qed.
 
-  Lemma map_seq_cons_disjoint start xs x :
+  Lemma map_seq_cons_disjoint start xs :
     map_seq (M:=M A) (S start) xs !! start = None.
   Proof. rewrite lookup_map_seq_None. lia. Qed.
   Lemma map_seq_cons start xs x :
     map_seq start (x :: xs) =@{M A} <[start:=x]> (map_seq (S start) xs).
   Proof. done. Qed.
 
-  Lemma map_seq_snoc_disjoint start xs x :
+  Lemma map_seq_snoc_disjoint start xs :
     map_seq (M:=M A) start xs !! (start+length xs) = None.
   Proof. rewrite lookup_map_seq_None. lia. Qed.
   Lemma map_seq_snoc start xs x :

theories/gmap.v

@@ -213,54 +213,77 @@ Section curry_uncurry.
 End curry_uncurry.
 
 (** * Finite sets *)
-Notation gset K := (mapset (gmap K)).
-Instance gset_dom `{Countable K} {A} : Dom (gmap K A) (gset K) := mapset_dom.
-Instance gset_dom_spec `{Countable K} :
-  FinMapDom K (gmap K) (gset K) := mapset_dom_spec.
+Definition gset K `{Countable K} := mapset (gmap K).
 
-Definition gset_to_propset `{Countable A} (X : gset A) : propset A :=
-  {[ x | x ∈ X ]}.
-Lemma elem_of_gset_to_propset `{Countable A} (X : gset A) x : x ∈ gset_to_propset X ↔ x ∈ X.
-Proof. done. Qed.
+Section gset.
+  Context `{Countable K}.
+  Global Instance gset_elem_of: ElemOf K (gset K) := _.
+  Global Instance gset_empty : Empty (gset K) := _.
+  Global Instance gset_singleton : Singleton K (gset K) := _.
+  Global Instance gset_union: Union (gset K) := _.
+  Global Instance gset_intersection: Intersection (gset K) := _.
+  Global Instance gset_difference: Difference (gset K) := _.
+  Global Instance gset_elements: Elements K (gset K) := _.
+  Global Instance gset_leibniz : LeibnizEquiv (gset K) := _.
+  Global Instance gset_semi_set : SemiSet K (gset K) | 1 := _.
+  Global Instance gset_set : Set_ K (gset K) | 1 := _.
+  Global Instance gset_fin_set : FinSet K (gset K) := _.
+  Global Instance gset_eq_dec : EqDecision (gset K) := _.
+  Global Instance gset_countable : Countable (gset K) := _.
+  Global Instance gset_equiv_dec : RelDecision (≡@{gset K}) | 1 := _.
+  Global Instance gset_elem_of_dec : RelDecision (∈@{gset K}) | 1 := _.
+  Global Instance gset_disjoint_dec : RelDecision (##@{gset K}) := _.
+  Global Instance gset_subseteq_dec : RelDecision (⊆@{gset K}) := _.
+  Global Instance gset_dom {A} : Dom (gmap K A) (gset K) := mapset_dom.
+  Global Instance gset_dom_spec : FinMapDom K (gmap K) (gset K) := mapset_dom_spec.
 
-Definition gset_to_gmap `{Countable K} {A} (x : A) (X : gset K) : gmap K A :=
-  (λ _, x) <$> mapset_car X.
+  Definition gset_to_propset (X : gset K) : propset K :=
+    {[ x | x ∈ X ]}.
+  Lemma elem_of_gset_to_propset (X : gset K) x : x ∈ gset_to_propset X ↔ x ∈ X.
+  Proof. done. Qed.
 
-Lemma lookup_gset_to_gmap `{Countable K} {A} (x : A) (X : gset K) i :
-  gset_to_gmap x X !! i = guard (i ∈ X); Some x.
-Proof.
-  destruct X as [X]; unfold gset_to_gmap, elem_of, mapset_elem_of; simpl.
-  rewrite lookup_fmap.
-  case_option_guard; destruct (X !! i) as [[]|]; naive_solver.
-Qed.
-Lemma lookup_gset_to_gmap_Some `{Countable K} {A} (x : A) (X : gset K) i y :
-  gset_to_gmap x X !! i = Some y ↔ i ∈ X ∧ x = y.
-Proof. rewrite lookup_gset_to_gmap. simplify_option_eq; naive_solver. Qed.
-Lemma lookup_gset_to_gmap_None `{Countable K} {A} (x : A) (X : gset K) i :
-  gset_to_gmap x X !! i = None ↔ i ∉ X.
-Proof. rewrite lookup_gset_to_gmap. simplify_option_eq; naive_solver. Qed.
+  Definition gset_to_gmap {A} (x : A) (X : gset K) : gmap K A :=
+    (λ _, x) <$> mapset_car X.
 
-Lemma gset_to_gmap_empty `{Countable K} {A} (x : A) : gset_to_gmap x ∅ = ∅.
-Proof. apply fmap_empty. Qed.
-Lemma gset_to_gmap_union_singleton `{Countable K} {A} (x : A) i Y :
-  gset_to_gmap x ({[ i ]} ∪ Y) = <[i:=x]>(gset_to_gmap x Y).
-Proof.
-  apply map_eq; intros j; apply option_eq; intros y.
-  rewrite lookup_insert_Some, !lookup_gset_to_gmap_Some, elem_of_union,
-    elem_of_singleton; destruct (decide (i = j)); intuition.
-Qed.
+  Lemma lookup_gset_to_gmap {A} (x : A) (X : gset K) i :
+    gset_to_gmap x X !! i = guard (i ∈ X); Some x.
+  Proof.
+    destruct X as [X].
+    unfold gset_to_gmap, gset_elem_of, elem_of, mapset_elem_of; simpl.
+    rewrite lookup_fmap.
+    case_option_guard; destruct (X !! i) as [[]|]; naive_solver.
+  Qed.
+  Lemma lookup_gset_to_gmap_Some {A} (x : A) (X : gset K) i y :
+    gset_to_gmap x X !! i = Some y ↔ i ∈ X ∧ x = y.
+  Proof. rewrite lookup_gset_to_gmap. simplify_option_eq; naive_solver. Qed.
+  Lemma lookup_gset_to_gmap_None {A} (x : A) (X : gset K) i :
+    gset_to_gmap x X !! i = None ↔ i ∉ X.
+  Proof. rewrite lookup_gset_to_gmap. simplify_option_eq; naive_solver. Qed.
 
-Lemma fmap_gset_to_gmap `{Countable K} {A B} (f : A → B) (X : gset K) (x : A) :
-  f <$> gset_to_gmap x X = gset_to_gmap (f x) X.
-Proof.
-  apply map_eq; intros j. rewrite lookup_fmap, !lookup_gset_to_gmap.
-  by simplify_option_eq.
-Qed.
-Lemma gset_to_gmap_dom `{Countable K} {A B} (m : gmap K A) (y : B) :
-  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:?.
-  - by rewrite option_guard_True by (rewrite elem_of_dom; eauto).
-  - by rewrite option_guard_False by (rewrite not_elem_of_dom; eauto).
-Qed.
+  Lemma gset_to_gmap_empty {A} (x : A) : gset_to_gmap x ∅ = ∅.
+  Proof. apply fmap_empty. Qed.
+  Lemma gset_to_gmap_union_singleton {A} (x : A) i Y :
+    gset_to_gmap x ({[ i ]} ∪ Y) = <[i:=x]>(gset_to_gmap x Y).
+  Proof.
+    apply map_eq; intros j; apply option_eq; intros y.
+    rewrite lookup_insert_Some, !lookup_gset_to_gmap_Some, elem_of_union,
+      elem_of_singleton; destruct (decide (i = j)); intuition.
+  Qed.
+
+  Lemma fmap_gset_to_gmap {A B} (f : A → B) (X : gset K) (x : A) :
+    f <$> gset_to_gmap x X = gset_to_gmap (f x) X.
+  Proof.
+    apply map_eq; intros j. rewrite lookup_fmap, !lookup_gset_to_gmap.
+    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.
+  Proof.
+    apply map_eq; intros j. rewrite lookup_fmap, lookup_gset_to_gmap.
+    destruct (m !! j) as [x|] eqn:?.
+    - by rewrite option_guard_True by (rewrite elem_of_dom; eauto).
+    - by rewrite option_guard_False by (rewrite not_elem_of_dom; eauto).
+  Qed.
+End gset.
+
+Typeclasses Opaque gset.

theories/mapset.v

@@ -76,7 +76,7 @@ Section deciders.
     match X1, X2 with Mapset m1, Mapset m2 => cast_if (decide (m1 = m2)) end);
     abstract congruence.
   Defined.
-  Program Instance mapset_countable `{Countable (M ())} : Countable (mapset M) :=
+  Global Program Instance mapset_countable `{Countable (M ())} : Countable (mapset M) :=
     inj_countable mapset_car (Some ∘ Mapset) _.
   Next Obligation. by intros ? ? []. Qed.
   Global Instance mapset_equiv_dec : RelDecision (≡@{mapset M}) | 1.