Commit dfec102c authored by Robbert Krebbers's avatar Robbert Krebbers

Make `gset` a `Definition` instead of `Notation`.

parent d0961b67
......@@ -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.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment