diff --git a/prelude/gmap.v b/prelude/gmap.v index 88fa0ac29f01096271b5a25aaee5877755870be5..77a83e6c23a16b2e25e7f60cbc54eb6b2e0dc480 100644 --- a/prelude/gmap.v +++ b/prelude/gmap.v @@ -3,7 +3,7 @@ (** This file implements finite maps and finite sets with keys of any countable type. The implementation is based on [Pmap]s, radix-2 search trees. *) From prelude Require Export countable fin_maps fin_map_dom. -From prelude Require Import pmap mapset. +From prelude Require Import pmap mapset sets. (** * The data structure *) (** We pack a [Pmap] together with a proof that ensures that all keys correspond @@ -118,6 +118,10 @@ 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 of_gset `{Countable A} (X : gset A) : set A := mkSet (λ x, x ∈ X). +Lemma elem_of_of_gset `{Countable A} (X : gset A) x : x ∈ of_gset X ↔ x ∈ X. +Proof. done. Qed. + (** * Fresh elements *) (* This is pretty ad-hoc and just for the case of [gset positive]. We need a notion of countable non-finite types to generalize this. *)