Commit b7e31ce2 authored by Robbert Krebbers's avatar Robbert Krebbers

Consistently use `set` and `map` names.

Get rid of using `Collection` and favor `set` everywhere. Also, prefer conversion
functions that are called `X_to_Y`.

The following sed script performs most of the renaming, with the exception of:

- `set`, which has been renamed into `propset`. I couldn't do this rename
  using `sed` since it's too context sensitive.
- There was a spurious rename of `Vec.of_list`, which I correctly manually.
- Updating some section names and comments.

```
sed '
s/SimpleCollection/SemiSet/g;
s/FinCollection/FinSet/g;
s/CollectionMonad/MonadSet/g;
s/Collection/Set\_/g;
s/collection\_simple/set\_semi\_set/g;
s/fin\_collection/fin\_set/g;
s/collection\_monad\_simple/monad\_set\_semi\_set/g;
s/collection\_equiv/set\_equiv/g;
s/\bbset/boolset/g;
s/mkBSet/BoolSet/g;
s/mkSet/PropSet/g;
s/set\_equivalence/set\_equiv\_equivalence/g;
s/collection\_subseteq/set\_subseteq/g;
s/collection\_disjoint/set\_disjoint/g;
s/collection\_fold/set\_fold/g;
s/collection\_map/set\_map/g;
s/collection\_size/set\_size/g;
s/collection\_filter/set\_filter/g;
s/collection\_guard/set\_guard/g;
s/collection\_choose/set\_choose/g;
s/collection\_ind/set\_ind/g;
s/collection\_wf/set\_wf/g;
s/map\_to\_collection/map\_to\_set/g;
s/map\_of\_collection/set\_to\_map/g;
s/map\_of\_list/list\_to\_map/g;
s/map\_of\_to_list/list\_to\_map\_to\_list/g;
s/map\_to\_of\_list/map\_to\_list\_to\_map/g;
s/\bof\_list/list\_to\_set/g;
s/\bof\_option/option\_to\_set/g;
s/elem\_of\_of\_list/elem\_of\_list\_to\_set/g;
s/elem\_of\_of\_option/elem\_of\_option\_to\_set/g;
s/collection\_not\_subset\_inv/set\_not\_subset\_inv/g;
s/seq\_set/set\_seq/g;
s/collections/sets/g;
s/collection/set/g;
' -i $(find -name "*.v")
```
parent 22d4a0cd
......@@ -3,13 +3,13 @@ theories/base.v
theories/tactics.v
theories/option.v
theories/fin_map_dom.v
theories/bset.v
theories/boolset.v
theories/fin_maps.v
theories/fin.v
theories/vector.v
theories/pmap.v
theories/stringmap.v
theories/fin_collections.v
theories/fin_sets.v
theories/mapset.v
theories/proof_irrel.v
theories/hashset.v
......@@ -19,7 +19,7 @@ theories/orders.v
theories/natmap.v
theories/strings.v
theories/relations.v
theories/collections.v
theories/sets.v
theories/listset.v
theories/streams.v
theories/gmap.v
......@@ -32,7 +32,7 @@ theories/nmap.v
theories/zmap.v
theories/coPset.v
theories/lexico.v
theories/set.v
theories/propset.v
theories/decidable.v
theories/list.v
theories/functions.v
......
......@@ -2,7 +2,7 @@
(* This file is distributed under the terms of the BSD license. *)
(** This file collects type class interfaces, notations, and general theorems
that are used throughout the whole development. Most importantly it contains
abstract interfaces for ordered structures, collections, and various other data
abstract interfaces for ordered structures, sets, and various other data
structures. *)
From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid.
......@@ -753,9 +753,9 @@ End sig_map.
Arguments sig_map _ _ _ _ _ _ !_ / : assert.
(** * Operations on collections *)
(** * Operations on sets *)
(** We define operational type classes for the traditional operations and
relations on collections: the empty collection [∅], the union [(∪)],
relations on sets: the empty set [∅], the union [(∪)],
intersection [(∩)], and difference [(∖)], the singleton [{[_]}], the subset
[(⊆)] and element of [(∈)] relation, and disjointess [(##)]. *)
Class Empty A := empty: A.
......@@ -1053,7 +1053,7 @@ Instance: Params (@partial_alter) 4 := {}.
Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
(** The function [dom C m] should yield the domain of [m]. That is a finite
collection of type [C] that contains the keys that are a member of [m]. *)
set of type [C] that contains the keys that are a member of [m]. *)
Class Dom (M C : Type) := dom: M C.
Hint Mode Dom ! ! : typeclass_instances.
Instance: Params (@dom) 3 := {}.
......@@ -1110,23 +1110,25 @@ Notation "<[ k := a ]{ Γ }>" := (insertE Γ k a)
Arguments insertE _ _ _ _ _ _ !_ _ !_ / : simpl nomatch, assert.
(** * Axiomatization of collections *)
(** The class [SimpleCollection A C] axiomatizes a collection of type [C] with
elements of type [A]. *)
Class SimpleCollection A C `{ElemOf A C,
(** * Axiomatization of sets *)
(** The classes [SemiSet A C] and [Set_ A C] axiomatize sset of type [C] with
elements of type [A]. The first class, [SemiSet] does not include intersection
and difference. It is useful for the case of lists, where decidable equality
is needed to implement intersection and difference, but not union. *)
Class SemiSet A C `{ElemOf A C,
Empty C, Singleton A C, Union C} : Prop := {
not_elem_of_empty (x : A) : x ;
elem_of_singleton (x y : A) : x {[ y ]} x = y;
elem_of_union X Y (x : A) : x X Y x X x Y
}.
Class Collection A C `{ElemOf A C, Empty C, Singleton A C,
Class Set_ A C `{ElemOf A C, Empty C, Singleton A C,
Union C, Intersection C, Difference C} : Prop := {
collection_simple :>> SimpleCollection A C;
set_semi_set :>> SemiSet A C;
elem_of_intersection X Y (x : A) : x X Y x X x Y;
elem_of_difference X Y (x : A) : x X Y x X x Y
}.
(** We axiomative a finite collection as a collection whose elements can be
(** We axiomative a finite set as a set whose elements can be
enumerated as a list. These elements, given by the [elements] function, may be
in any order and should not contain duplicates. *)
Class Elements A C := elements: C list A.
......@@ -1159,9 +1161,9 @@ Qed.
(** Decidability of equality of the carrier set is admissible, but we add it
anyway so as to avoid cycles in type class search. *)
Class FinCollection A C `{ElemOf A C, Empty C, Singleton A C, Union C,
Class FinSet A C `{ElemOf A C, Empty C, Singleton A C, Union C,
Intersection C, Difference C, Elements A C, EqDecision A} : Prop := {
fin_collection :>> Collection A C;
fin_set_set :>> Set_ A C;
elem_of_elements X x : x elements X x X;
NoDup_elements X : NoDup (elements X)
}.
......@@ -1170,18 +1172,18 @@ Hint Mode Size ! : typeclass_instances.
Arguments size {_ _} !_ / : simpl nomatch, assert.
Instance: Params (@size) 2 := {}.
(** The class [CollectionMonad M] axiomatizes a type constructor [M] that can be
used to construct a collection [M A] with elements of type [A]. The advantage
of this class, compared to [Collection], is that it also axiomatizes the
(** The class [MonadSet M] axiomatizes a type constructor [M] that can be
used to construct a set [M A] with elements of type [A]. The advantage
of this class, compared to [Set_], is that it also axiomatizes the
the monadic operations. The disadvantage, is that not many inhabits are
possible (we will only provide an inhabitant using unordered lists without
duplicates removed). More interesting implementations typically need
decidability of equality, or a total order on the elements, which do not fit
duplicates). More interesting implementations typically need
decidable equality, or a total order on the elements, which do not fit
in a type constructor of type [Type → Type]. *)
Class CollectionMonad M `{ A, ElemOf A (M A),
Class MonadSet M `{ A, ElemOf A (M A),
A, Empty (M A), A, Singleton A (M A), A, Union (M A),
!MBind M, !MRet M, !FMap M, !MJoin M} : Prop := {
collection_monad_simple A :> SimpleCollection A (M A);
monad_set_semi_set A :> SemiSet A (M A);
elem_of_bind {A B} (f : A M B) (X : M A) (x : B) :
x X = f y, x f y y X;
elem_of_ret {A} (x y : A) : x mret y x = y;
......@@ -1192,13 +1194,13 @@ Class CollectionMonad M `{∀ A, ElemOf A (M A),
(** The function [fresh X] yields an element that is not contained in [X]. We
will later prove that [fresh] is [Proper] with respect to the induced setoid
equality on collections. *)
equality on sets. *)
Class Fresh A C := fresh: C A.
Hint Mode Fresh - ! : typeclass_instances.
Instance: Params (@fresh) 3 := {}.
Class FreshSpec A C `{ElemOf A C,
Empty C, Singleton A C, Union C, Fresh A C} : Prop := {
fresh_collection_simple :>> SimpleCollection A C;
fresh_set_semi_set :>> SemiSet A C;
fresh_proper_alt X Y : ( x, x X x Y) fresh X = fresh Y;
is_fresh (X : C) : fresh X X
}.
......
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements boolsets as functions into Prop. *)
From stdpp Require Export prelude.
Set Default Proof Using "Type".
Record boolset (A : Type) : Type := BoolSet { boolset_car : A bool }.
Arguments BoolSet {_} _ : assert.
Arguments boolset_car {_} _ _ : assert.
Instance boolset_top {A} : Top (boolset A) := BoolSet (λ _, true).
Instance boolset_empty {A} : Empty (boolset A) := BoolSet (λ _, false).
Instance boolset_singleton `{EqDecision A} : Singleton A (boolset A) := λ x,
BoolSet (λ y, bool_decide (y = x)).
Instance boolset_elem_of {A} : ElemOf A (boolset A) := λ x X, boolset_car X x.
Instance boolset_union {A} : Union (boolset A) := λ X1 X2,
BoolSet (λ x, boolset_car X1 x || boolset_car X2 x).
Instance boolset_intersection {A} : Intersection (boolset A) := λ X1 X2,
BoolSet (λ x, boolset_car X1 x && boolset_car X2 x).
Instance boolset_difference {A} : Difference (boolset A) := λ X1 X2,
BoolSet (λ x, boolset_car X1 x && negb (boolset_car X2 x)).
Instance boolset_set `{EqDecision A} : Set_ A (boolset A).
Proof.
split; [split| |].
- by intros x ?.
- by intros x y; rewrite <-(bool_decide_spec (x = y)).
- split. apply orb_prop_elim. apply orb_prop_intro.
- split. apply andb_prop_elim. apply andb_prop_intro.
- intros X Y x; unfold elem_of, boolset_elem_of; simpl.
destruct (boolset_car X x), (boolset_car Y x); simpl; tauto.
Qed.
Instance boolset_elem_of_dec {A} : RelDecision (@{boolset A}).
Proof. refine (λ x X, cast_if (decide (boolset_car X x))); done. Defined.
Typeclasses Opaque boolset_elem_of.
Global Opaque boolset_empty boolset_singleton boolset_union
boolset_intersection boolset_difference.
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements bsets as functions into Prop. *)
From stdpp Require Export prelude.
Set Default Proof Using "Type".
Record bset (A : Type) : Type := mkBSet { bset_car : A bool }.
Arguments mkBSet {_} _ : assert.
Arguments bset_car {_} _ _ : assert.
Instance bset_top {A} : Top (bset A) := mkBSet (λ _, true).
Instance bset_empty {A} : Empty (bset A) := mkBSet (λ _, false).
Instance bset_singleton `{EqDecision A} : Singleton A (bset A) := λ x,
mkBSet (λ y, bool_decide (y = x)).
Instance bset_elem_of {A} : ElemOf A (bset A) := λ x X, bset_car X x.
Instance bset_union {A} : Union (bset A) := λ X1 X2,
mkBSet (λ x, bset_car X1 x || bset_car X2 x).
Instance bset_intersection {A} : Intersection (bset A) := λ X1 X2,
mkBSet (λ x, bset_car X1 x && bset_car X2 x).
Instance bset_difference {A} : Difference (bset A) := λ X1 X2,
mkBSet (λ x, bset_car X1 x && negb (bset_car X2 x)).
Instance bset_collection `{EqDecision A} : Collection A (bset A).
Proof.
split; [split| |].
- by intros x ?.
- by intros x y; rewrite <-(bool_decide_spec (x = y)).
- split. apply orb_prop_elim. apply orb_prop_intro.
- split. apply andb_prop_elim. apply andb_prop_intro.
- intros X Y x; unfold elem_of, bset_elem_of; simpl.
destruct (bset_car X x), (bset_car Y x); simpl; tauto.
Qed.
Instance bset_elem_of_dec {A} : RelDecision (@{bset A}).
Proof. refine (λ x X, cast_if (decide (bset_car X x))); done. Defined.
Typeclasses Opaque bset_elem_of.
Global Opaque bset_empty bset_singleton bset_union
bset_intersection bset_difference.
......@@ -11,7 +11,7 @@ membership, as well as extensional equality (i.e. [X = Y ↔ ∀ x, x ∈ X ↔
Since [positive]s are bitstrings, we encode [coPset]s as trees that correspond
to the decision function that map bitstrings to bools. *)
From stdpp Require Export collections.
From stdpp Require Export sets.
From stdpp Require Import pmap gmap mapset.
Set Default Proof Using "Type".
Local Open Scope positive_scope.
......@@ -169,7 +169,7 @@ Instance coPset_difference : Difference coPset := λ X Y,
let (t1,Ht1) := X in let (t2,Ht2) := Y in
(t1 coPset_opp_raw t2) coPset_intersection_wf _ _ Ht1 (coPset_opp_wf _).
Instance coPset_collection : Collection positive coPset.
Instance coPset_set : Set_ positive coPset.
Proof.
split; [split| |].
- by intros ??.
......@@ -223,7 +223,7 @@ Proof.
unfold set_finite, elem_of at 1, coPset_elem_of; simpl; clear Ht; split.
- induction t as [b|b l IHl r IHr]; simpl.
{ destruct b; simpl; [intros [l Hl]|done].
by apply (is_fresh (of_list l : Pset)), elem_of_of_list, Hl. }
by apply (is_fresh (list_to_set l : Pset)), elem_of_list_to_set, Hl. }
intros [ll Hll]; rewrite andb_True; split.
+ apply IHl; exists (omap (maybe (~0)) ll); intros i.
rewrite elem_of_list_omap; intros; exists (i~0); auto.
......
......@@ -3,7 +3,7 @@
(** This file provides an axiomatization of the domain function of finite
maps. We provide such an axiomatization, instead of implementing the domain
function in a generic way, to allow more efficient implementations. *)
From stdpp Require Export collections fin_maps.
From stdpp Require Export sets fin_maps.
Set Default Proof Using "Type*".
Class FinMapDom K M D `{ A, Dom (M A) D, FMap M,
......@@ -12,7 +12,7 @@ Class FinMapDom K M D `{∀ A, Dom (M A) D, FMap M,
ElemOf K D, Empty D, Singleton K D,
Union D, Intersection D, Difference D} := {
finmap_dom_map :>> FinMap K M;
finmap_dom_collection :>> Collection K D;
finmap_dom_set :>> Set_ K D;
elem_of_dom {A} (m : M A) i : i dom D m is_Some (m !! i)
}.
......
This diff is collapsed.
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects definitions and theorems on finite collections. Most
(** This file collects definitions and theorems on finite sets. Most
importantly, it implements a fold and size function and some useful induction
principles on finite collections . *)
principles on finite sets . *)
From stdpp Require Import relations.
From stdpp Require Export numbers collections.
From stdpp Require Export numbers sets.
Set Default Proof Using "Type*".
Instance collection_size `{Elements A C} : Size C := length elements.
Definition collection_fold `{Elements A C} {B}
Instance set_size `{Elements A C} : Size C := length elements.
Definition set_fold `{Elements A C} {B}
(f : A B B) (b : B) : C B := foldr f b elements.
Instance collection_filter
Instance set_filter
`{Elements A C, Empty C, Singleton A C, Union C} : Filter A C := λ P _ X,
of_list (filter P (elements X)).
Typeclasses Opaque collection_filter.
list_to_set (filter P (elements X)).
Typeclasses Opaque set_filter.
Definition collection_map `{Elements A C, Singleton B D, Empty D, Union D}
Definition set_map `{Elements A C, Singleton B D, Empty D, Union D}
(f : A B) (X : C) : D :=
of_list (f <$> elements X).
Typeclasses Opaque collection_map.
list_to_set (f <$> elements X).
Typeclasses Opaque set_map.
Section fin_collection.
Context `{FinCollection A C}.
Section fin_set.
Context `{FinSet A C}.
Implicit Types X Y : C.
Lemma fin_collection_finite X : set_finite X.
Lemma fin_set_finite X : set_finite X.
Proof. by exists (elements X); intros; rewrite elem_of_elements. Qed.
Instance elem_of_dec_slow : RelDecision (@{C}) | 100.
......@@ -80,11 +80,11 @@ Proof.
Qed.
(** * The [size] operation *)
Global Instance collection_size_proper: Proper (() ==> (=)) (@size C _).
Global Instance set_size_proper: Proper (() ==> (=)) (@size C _).
Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed.
Lemma size_empty : size ( : C) = 0.
Proof. unfold size, collection_size. simpl. by rewrite elements_empty. Qed.
Proof. unfold size, set_size. simpl. by rewrite elements_empty. Qed.
Lemma size_empty_inv (X : C) : size X = 0 X .
Proof.
intros; apply equiv_empty; intros x; rewrite <-elem_of_elements.
......@@ -95,27 +95,27 @@ Proof. split. apply size_empty_inv. by intros ->; rewrite size_empty. Qed.
Lemma size_non_empty_iff (X : C) : size X 0 X .
Proof. by rewrite size_empty_iff. Qed.
Lemma collection_choose_or_empty X : ( x, x X) X .
Lemma set_choose_or_empty X : ( x, x X) X .
Proof.
destruct (elements X) as [|x l] eqn:HX; [right|left].
- apply equiv_empty; intros x. by rewrite <-elem_of_elements, HX, elem_of_nil.
- exists x. rewrite <-elem_of_elements, HX. by left.
Qed.
Lemma collection_choose X : X x, x X.
Proof. intros. by destruct (collection_choose_or_empty X). Qed.
Lemma collection_choose_L `{!LeibnizEquiv C} X : X x, x X.
Proof. unfold_leibniz. apply collection_choose. Qed.
Lemma set_choose X : X x, x X.
Proof. intros. by destruct (set_choose_or_empty X). Qed.
Lemma set_choose_L `{!LeibnizEquiv C} X : X x, x X.
Proof. unfold_leibniz. apply set_choose. Qed.
Lemma size_pos_elem_of X : 0 < size X x, x X.
Proof.
intros Hsz. destruct (collection_choose_or_empty X) as [|HX]; [done|].
intros Hsz. destruct (set_choose_or_empty X) as [|HX]; [done|].
contradict Hsz. rewrite HX, size_empty; lia.
Qed.
Lemma size_singleton (x : A) : size ({[ x ]} : C) = 1.
Proof. unfold size, collection_size. simpl. by rewrite elements_singleton. Qed.
Proof. unfold size, set_size. simpl. by rewrite elements_singleton. Qed.
Lemma size_singleton_inv X x y : size X = 1 x X y X x = y.
Proof.
unfold size, collection_size. simpl. rewrite <-!elem_of_elements.
unfold size, set_size. simpl. rewrite <-!elem_of_elements.
generalize (elements X). intros [|? l]; intro; simplify_eq/=.
rewrite (nil_length_inv l), !elem_of_list_singleton by done; congruence.
Qed.
......@@ -129,7 +129,7 @@ Qed.
Lemma size_union X Y : X ## Y size (X Y) = size X + size Y.
Proof.
intros. unfold size, collection_size. simpl. rewrite <-app_length.
intros. unfold size, set_size. simpl. rewrite <-app_length.
apply Permutation_length, NoDup_Permutation.
- apply NoDup_elements.
- apply NoDup_app; repeat split; try apply NoDup_elements.
......@@ -154,28 +154,28 @@ Proof.
Qed.
(** * Induction principles *)
Lemma collection_wf : wf (@{C}).
Lemma set_wf : wf (@{C}).
Proof. apply (wf_projected (<) size); auto using subset_size, lt_wf. Qed.
Lemma collection_ind (P : C Prop) :
Lemma set_ind (P : C Prop) :
Proper (() ==> iff) P
P ( x X, x X P X P ({[ x ]} X)) X, P X.
Proof.
intros ? Hemp Hadd. apply well_founded_induction with ().
{ apply collection_wf. }
intros X IH. destruct (collection_choose_or_empty X) as [[x ?]|HX].
{ apply set_wf. }
intros X IH. destruct (set_choose_or_empty X) as [[x ?]|HX].
- rewrite (union_difference {[ x ]} X) by set_solver.
apply Hadd. set_solver. apply IH; set_solver.
- by rewrite HX.
Qed.
Lemma collection_ind_L `{!LeibnizEquiv C} (P : C Prop) :
Lemma set_ind_L `{!LeibnizEquiv C} (P : C Prop) :
P ( x X, x X P X P ({[ x ]} X)) X, P X.
Proof. apply collection_ind. by intros ?? ->%leibniz_equiv_iff. Qed.
Proof. apply set_ind. by intros ?? ->%leibniz_equiv_iff. Qed.
(** * The [collection_fold] operation *)
Lemma collection_fold_ind {B} (P : B C Prop) (f : A B B) (b : B) :
(** * The [set_fold] operation *)
Lemma set_fold_ind {B} (P : B C Prop) (f : A B B) (b : B) :
Proper ((=) ==> () ==> iff) P
P b ( x X r, x X P r X P (f x r) ({[ x ]} X))
X, P (collection_fold f b X) X.
X, P (set_fold f b X) X.
Proof.
intros ? Hemp Hadd.
cut ( l, NoDup l X, ( x, x X x l) P (foldr f b l) X).
......@@ -188,20 +188,20 @@ Proof.
rewrite (union_difference {[ x ]} X) by set_solver.
apply Hadd. set_solver. apply IH. set_solver.
Qed.
Lemma collection_fold_proper {B} (R : relation B) `{!Equivalence R}
Lemma set_fold_proper {B} (R : relation B) `{!Equivalence R}
(f : A B B) (b : B) `{!Proper ((=) ==> R ==> R) f}
(Hf : a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
Proper (() ==> R) (collection_fold f b : C B).
Proper (() ==> R) (set_fold f b : C B).
Proof. intros ?? E. apply (foldr_permutation R f b); auto. by rewrite E. Qed.
(** * Minimal elements *)
Lemma minimal_exists R `{!Transitive R, x y, Decision (R x y)} (X : C) :
X x, x X minimal R x X.
Proof.
pattern X; apply collection_ind; clear X.
pattern X; apply set_ind; clear X.
{ by intros X X' HX; setoid_rewrite HX. }
{ done. }
intros x X ? IH Hemp. destruct (collection_choose_or_empty X) as [[z ?]|HX].
intros x X ? IH Hemp. destruct (set_choose_or_empty X) as [[z ?]|HX].
{ destruct IH as (x' & Hx' & Hmin); [set_solver|].
destruct (decide (R x x')).
- exists x; split; [set_solver|].
......@@ -222,8 +222,8 @@ Section filter.
Lemma elem_of_filter X x : x filter P X P x x X.
Proof.
unfold filter, collection_filter.
by rewrite elem_of_of_list, elem_of_list_filter, elem_of_elements.
unfold filter, set_filter.
by rewrite elem_of_list_to_set, elem_of_list_filter, elem_of_elements.
Qed.
Global Instance set_unfold_filter X Q :
SetUnfold (x X) Q SetUnfold (x filter P X) (P x Q).
......@@ -255,34 +255,34 @@ End filter.
(** * Map *)
Section map.
Context `{Collection B D}.
Context `{Set_ B D}.
Lemma elem_of_map (f : A B) (X : C) y :
y collection_map (D:=D) f X x, y = f x x X.
y set_map (D:=D) f X x, y = f x x X.
Proof.
unfold collection_map. rewrite elem_of_of_list, elem_of_list_fmap.
unfold set_map. rewrite elem_of_list_to_set, elem_of_list_fmap.
by setoid_rewrite elem_of_elements.
Qed.
Global Instance set_unfold_map (f : A B) (X : C) (P : A Prop) :
( y, SetUnfold (y X) (P y))
SetUnfold (x collection_map (D:=D) f X) ( y, x = f y P y).
SetUnfold (x set_map (D:=D) f X) ( y, x = f y P y).
Proof. constructor. rewrite elem_of_map; naive_solver. Qed.
Global Instance collection_map_proper :
Proper (pointwise_relation _ (=) ==> () ==> ()) (collection_map (C:=C) (D:=D)).
Global Instance set_map_proper :
Proper (pointwise_relation _ (=) ==> () ==> ()) (set_map (C:=C) (D:=D)).
Proof. intros f g ? X Y. set_unfold; naive_solver. Qed.
Global Instance collection_map_mono :
Proper (pointwise_relation _ (=) ==> () ==> ()) (collection_map (C:=C) (D:=D)).
Global Instance set_map_mono :
Proper (pointwise_relation _ (=) ==> () ==> ()) (set_map (C:=C) (D:=D)).
Proof. intros f g ? X Y. set_unfold; naive_solver. Qed.
Lemma elem_of_map_1 (f : A B) (X : C) (y : B) :
y collection_map (D:=D) f X x, y = f x x X.
y set_map (D:=D) f X x, y = f x x X.
Proof. set_solver. Qed.
Lemma elem_of_map_2 (f : A B) (X : C) (x : A) :
x X f x collection_map (D:=D) f X.
x X f x set_map (D:=D) f X.
Proof. set_solver. Qed.
Lemma elem_of_map_2_alt (f : A B) (X : C) (x : A) (y : B) :
x X y = f x y collection_map (D:=D) f X.
x X y = f x y set_map (D:=D) f X.
Proof. set_solver. Qed.
End map.
......@@ -321,4 +321,4 @@ Proof.
refine (cast_if (decide (Exists P (elements X))));
by rewrite set_Exists_elements.
Defined.
End fin_collection.
End fin_set.
......@@ -3,8 +3,8 @@
(** 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 stdpp Require Export countable infinite fin_maps fin_map_dom.
From stdpp Require Import pmap mapset set.
Set Default Proof Using "Type".
From stdpp Require Import pmap mapset propset.
(* Set Default Proof Using "Type". *)
(** * The data structure *)
(** We pack a [Pmap] together with a proof that ensures that all keys correspond
......@@ -116,11 +116,11 @@ Qed.
Program Instance gmap_countable
`{Countable K, Countable A} : Countable (gmap K A) := {
encode m := encode (map_to_list m : list (K * A));
decode p := map_of_list <$> decode p
decode p := list_to_map <$> decode p
}.
Next Obligation.
intros K ?? A ?? m; simpl. rewrite decode_encode; simpl.
by rewrite map_of_to_list.
by rewrite list_to_map_to_list.
Qed.
(** * Curry and uncurry *)
......@@ -218,7 +218,8 @@ 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).
Definition of_gset `{Countable A} (X : gset A) : propset A :=
{[ x | x X ]}.
Lemma elem_of_of_gset `{Countable A} (X : gset A) x : x of_gset X x X.
Proof. done. Qed.
......
......@@ -66,7 +66,7 @@ Proof.
Qed.
Global Instance gmultiset_leibniz : LeibnizEquiv (gmultiset A).
Proof. intros X Y. by rewrite gmultiset_eq. Qed.
Global Instance gmultiset_equivalence : Equivalence (@{gmultiset A}).
Global Instance gmultiset_equiv_equivalence : Equivalence (@{gmultiset A}).
Proof. constructor; repeat intro; naive_solver. Qed.
(* Multiplicity *)
......@@ -90,11 +90,11 @@ Proof.
destruct (X !! _), (Y !! _); simplify_option_eq; lia.
Qed.
(* Collection *)
(* Set_ *)
Lemma elem_of_multiplicity x X : x X 0 < multiplicity x X.
Proof. done. Qed.
Global Instance gmultiset_simple_collection : SimpleCollection A (gmultiset A).
Global Instance gmultiset_simple_set : SemiSet A (gmultiset A).
Proof.
split.
- intros x. rewrite elem_of_multiplicity, multiplicity_empty. lia.
......
......@@ -61,7 +61,7 @@ Qed.
Global Instance hashset_elements: Elements A (hashset hash) := λ m,
map_to_list (hashset_car m) = snd.
Global Instance hashset_fin_collection : FinCollection A (hashset hash).
Global Instance hashset_fin_set : FinSet A (hashset hash).
Proof.
split; [split; [split| |]| |].
- intros ? (?&?&?); simplify_map_eq/=.
......
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
From stdpp Require Export fin_collections.
From stdpp Require Export fin_sets.
From stdpp Require Import pretty relations.
(** The class [Infinite] axiomatizes types with infinitely many elements
......@@ -47,7 +47,7 @@ Since [fresh_generic] is too inefficient for all practical purposes, we seal
off its definition. That way, Coq will not accidentally unfold it during
unification or other tactics. *)
Section fresh_generic.
Context `{FinCollection A C, Infinite A, !RelDecision (@{C})}.
Context `{FinSet A C, Infinite A, !RelDecision (@{C})}.
Definition fresh_generic_body (s : C) (rec : s', s' s nat A) (n : nat) : A :=
let cand := inject n in
......@@ -57,7 +57,7 @@ Section fresh_generic.
end.
Definition fresh_generic_fix_aux :
seal (Fix collection_wf (const (nat A)) fresh_generic_body). by eexists. Qed.
seal (Fix set_wf (const (nat A)) fresh_generic_body). by eexists. Qed.
Definition fresh_generic_fix := fresh_generic_fix_aux.(unseal).
Lemma fresh_generic_fixpoint_unfold s n:
......@@ -73,7 +73,7 @@ Section fresh_generic.
i, n i < m inject i s.
Proof.
revert n.
induction s as [s IH] using (well_founded_ind collection_wf); intros n.
induction s as [s IH] using (well_founded_ind set_wf); intros n.
setoid_rewrite fresh_generic_fixpoint_unfold; unfold fresh_generic_body.
destruct decide as [Hcase|Hcase]; [|by eauto with lia].
destruct (IH _ (subset_difference_elem_of Hcase) (S n))
......
......@@ -2,7 +2,7 @@
(* This file is distributed under the terms of the BSD license. *)
(** This file implements finite set as unordered lists without duplicates
removed. This implementation forms a monad. *)
From stdpp Require Export collections list.
From stdpp Require Export sets list.
Set Default Proof Using "Type".
Record listset A := Listset { listset_car: list A }.
......@@ -19,7 +19,7 @@ Global Instance listset_union: Union (listset A) := λ l k,
let (l') := l in let (k') := k in Listset (l' ++ k').
Global Opaque listset_singleton listset_empty.
Global Instance listset_simple_collection : SimpleCollection A (listset A).
Global Instance listset_simple_set : SemiSet A (listset A).
Proof.
split.
- by apply not_elem_of_nil.
......@@ -50,7 +50,7 @@ Global Instance listset_intersection: Intersection (listset A) := λ l k,
Global Instance listset_difference: Difference (listset A) := λ l k,
let (l') := l in let (k') := k in Listset (list_difference l' k').
Instance listset_collection: Collection A (listset A).
Instance listset_set: Set_ A (listset A).
Proof.
split.
- apply _.
......@@ -59,7 +59,7 @@ Proof.
Qed.
Global Instance listset_elements: Elements A (listset A) :=
remove_dups listset_car.
Global Instance listset_fin_collection : FinCollection A (listset A).
Global Instance listset_fin_set : FinSet A (listset A).
Proof.
split.
- apply _.
......@@ -75,7 +75,7 @@ Instance listset_bind: MBind listset := λ A B f l,
let (l') := l in Listset (mbind (listset_car f) l').
Instance listset_join: MJoin listset := λ A, mbind id.