Commit 2cf0cd35 authored by Robbert Krebbers's avatar Robbert Krebbers

Merge branch 'robbert/set_rename' into 'master'

Consistently use `set_` prefix.

Closes #24

See merge request !45
parents 22d4a0cd e823cff6
Pipeline #14844 failed with stage
in 6 minutes and 6 seconds
......@@ -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,28 @@ 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.
Note that we cannot use the name [Set] since that is a reserved keyword. Hence
we use [Set_]. *)
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 +1164,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 +1175,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 +1197,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.
......@@ -126,26 +126,26 @@ Lemma coPset_intersection_wf t1 t2 :
Proof. revert t2; induction t1 as [[]|[]]; intros [[]|[] ??]; simpl; eauto. Qed.
Lemma coPset_opp_wf t : coPset_wf (coPset_opp_raw t).
Proof. induction t as [[]|[]]; simpl; eauto. Qed.
Lemma elem_to_Pset_singleton p q : e_of p (coPset_singleton_raw q) p = q.
Lemma coPset_elem_of_singleton p q : e_of p (coPset_singleton_raw q) p = q.
Proof.
split; [|by intros <-; induction p; simpl; rewrite ?coPset_elem_of_node].
by revert q; induction p; intros [?|?|]; simpl;
rewrite ?coPset_elem_of_node; intros; f_equal/=; auto.
Qed.
Lemma elem_to_Pset_union t1 t2 p : e_of p (t1 t2) = e_of p t1 || e_of p t2.
Lemma coPset_elem_of_union t1 t2 p : e_of p (t1 t2) = e_of p t1 || e_of p t2.
Proof.
by revert t2 p; induction t1 as [[]|[]]; intros [[]|[] ??] [?|?|]; simpl;
rewrite ?coPset_elem_of_node; simpl;
rewrite ?orb_true_l, ?orb_false_l, ?orb_true_r, ?orb_false_r.
Qed.
Lemma elem_to_Pset_intersection t1 t2 p :
Lemma coPset_elem_of_intersection t1 t2 p :
e_of p (t1 t2) = e_of p t1 && e_of p t2.
Proof.
by revert t2 p; induction t1 as [[]|[]]; intros [[]|[] ??] [?|?|]; simpl;
rewrite ?coPset_elem_of_node; simpl;
rewrite ?andb_true_l, ?andb_false_l, ?andb_true_r, ?andb_false_r.
Qed.
Lemma elem_to_Pset_opp t p : e_of p (coPset_opp_raw t) = negb (e_of p t).
Lemma coPset_elem_of_opp t p : e_of p (coPset_opp_raw t) = negb (e_of p t).
Proof.
by revert p; induction t as [[]|[]]; intros [?|?|]; simpl;
rewrite ?coPset_elem_of_node; simpl.
......@@ -169,18 +169,18 @@ 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 ??.
- intros p q. apply elem_to_Pset_singleton.
- intros p q. apply coPset_elem_of_singleton.
- intros [t] [t'] p; unfold elem_of, coPset_elem_of, coPset_union; simpl.
by rewrite elem_to_Pset_union, orb_True.
by rewrite coPset_elem_of_union, orb_True.
- intros [t] [t'] p; unfold elem_of,coPset_elem_of,coPset_intersection; simpl.
by rewrite elem_to_Pset_intersection, andb_True.
by rewrite coPset_elem_of_intersection, andb_True.
- intros [t] [t'] p; unfold elem_of, coPset_elem_of, coPset_difference; simpl.
by rewrite elem_to_Pset_intersection,
elem_to_Pset_opp, andb_True, negb_True.
by rewrite coPset_elem_of_intersection,
coPset_elem_of_opp, andb_True, negb_True.
Qed.
Instance coPset_leibniz : LeibnizEquiv coPset.
......@@ -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.
......@@ -271,88 +271,88 @@ Proof.
Qed.
(** * Conversion to psets *)
Fixpoint to_Pset_raw (t : coPset_raw) : Pmap_raw () :=
Fixpoint coPset_to_Pset_raw (t : coPset_raw) : Pmap_raw () :=
match t with
| coPLeaf _ => PLeaf
| coPNode false l r => PNode' None (to_Pset_raw l) (to_Pset_raw r)
| coPNode true l r => PNode (Some ()) (to_Pset_raw l) (to_Pset_raw r)
| coPNode false l r => PNode' None (coPset_to_Pset_raw l) (coPset_to_Pset_raw r)
| coPNode true l r => PNode (Some ()) (coPset_to_Pset_raw l) (coPset_to_Pset_raw r)
end.
Lemma to_Pset_wf t : coPset_wf t Pmap_wf (to_Pset_raw t).
Lemma coPset_to_Pset_wf t : coPset_wf t Pmap_wf (coPset_to_Pset_raw t).
Proof. induction t as [|[]]; simpl; eauto using PNode_wf. Qed.
Definition to_Pset (X : coPset) : Pset :=
let (t,Ht) := X in Mapset (PMap (to_Pset_raw t) (to_Pset_wf _ Ht)).
Lemma elem_of_to_Pset X i : set_finite X i to_Pset X i X.
Definition coPset_to_Pset (X : coPset) : Pset :=
let (t,Ht) := X in Mapset (PMap (coPset_to_Pset_raw t) (coPset_to_Pset_wf _ Ht)).
Lemma elem_of_coPset_to_Pset X i : set_finite X i coPset_to_Pset X i X.
Proof.
rewrite coPset_finite_spec; destruct X as [t Ht].
change (coPset_finite t to_Pset_raw t !! i = Some () e_of i t).
change (coPset_finite t coPset_to_Pset_raw t !! i = Some () e_of i t).
clear Ht; revert i; induction t as [[]|[] l IHl r IHr]; intros [i|i|];
simpl; rewrite ?andb_True, ?PNode_lookup; naive_solver.
Qed.
(** * Conversion from psets *)
Fixpoint of_Pset_raw (t : Pmap_raw ()) : coPset_raw :=
Fixpoint Pset_to_coPset_raw (t : Pmap_raw ()) : coPset_raw :=
match t with
| PLeaf => coPLeaf false
| PNode None l r => coPNode false (of_Pset_raw l) (of_Pset_raw r)
| PNode (Some _) l r => coPNode true (of_Pset_raw l) (of_Pset_raw r)
| PNode None l r => coPNode false (Pset_to_coPset_raw l) (Pset_to_coPset_raw r)
| PNode (Some _) l r => coPNode true (Pset_to_coPset_raw l) (Pset_to_coPset_raw r)
end.
Lemma of_Pset_wf t : Pmap_wf t coPset_wf (of_Pset_raw t).
Lemma Pset_to_coPset_wf t : Pmap_wf t coPset_wf (Pset_to_coPset_raw t).
Proof.
induction t as [|[] l IHl r IHr]; simpl; rewrite ?andb_True; auto.
- intros [??]; destruct l as [|[]], r as [|[]]; simpl in *; auto.
- destruct l as [|[]], r as [|[]]; simpl in *; rewrite ?andb_true_r;
rewrite ?andb_True; rewrite ?andb_True in IHl, IHr; intuition.
Qed.
Lemma elem_of_of_Pset_raw i t : e_of i (of_Pset_raw t) t !! i = Some ().
Lemma elem_of_Pset_to_coPset_raw i t : e_of i (Pset_to_coPset_raw t) t !! i = Some ().
Proof. by revert i; induction t as [|[[]|]]; intros []; simpl; auto; split. Qed.
Lemma of_Pset_raw_finite t : coPset_finite (of_Pset_raw t).
Lemma Pset_to_coPset_raw_finite t : coPset_finite (Pset_to_coPset_raw t).
Proof. induction t as [|[[]|]]; simpl; rewrite ?andb_True; auto. Qed.
Definition of_Pset (X : Pset) : coPset :=
let 'Mapset (PMap t Ht) := X in of_Pset_raw t of_Pset_wf _ Ht.
Lemma elem_of_of_Pset X i : i of_Pset X i X.
Proof. destruct X as [[t ?]]; apply elem_of_of_Pset_raw. Qed.
Lemma of_Pset_finite X : set_finite (of_Pset X).
Definition Pset_to_coPset (X : Pset) : coPset :=
let 'Mapset (PMap t Ht) := X in Pset_to_coPset_raw t Pset_to_coPset_wf _ Ht.
Lemma elem_of_Pset_to_coPset X i : i Pset_to_coPset X i X.
Proof. destruct X as [[t ?]]; apply elem_of_Pset_to_coPset_raw. Qed.
Lemma Pset_to_coPset_finite X : set_finite (Pset_to_coPset X).
Proof.
apply coPset_finite_spec; destruct X as [[t ?]]; apply of_Pset_raw_finite.
apply coPset_finite_spec; destruct X as [[t ?]]; apply Pset_to_coPset_raw_finite.
Qed.
(** * Conversion to and from gsets of positives *)
Lemma to_gset_wf (m : Pmap ()) : gmap_wf (K:=positive) m.
Lemma coPset_to_gset_wf (m : Pmap ()) : gmap_wf (K:=positive) m.
Proof. done. Qed.
Definition to_gset (X : coPset) : gset positive :=
let 'Mapset m := to_Pset X in
Mapset (GMap m (bool_decide_pack _ (to_gset_wf m))).
Definition coPset_to_gset (X : coPset) : gset positive :=
let 'Mapset m := coPset_to_Pset X in
Mapset (GMap m (bool_decide_pack _ (coPset_to_gset_wf m))).
Definition of_gset (X : gset positive) : coPset :=
let 'Mapset (GMap (PMap t Ht) _) := X in of_Pset_raw t of_Pset_wf _ Ht.
Definition gset_to_coPset (X : gset positive) : coPset :=
let 'Mapset (GMap (PMap t Ht) _) := X in Pset_to_coPset_raw t Pset_to_coPset_wf _ Ht.
Lemma elem_of_to_gset X i : set_finite X i to_gset X i X.
Lemma elem_of_coPset_to_gset X i : set_finite X i coPset_to_gset X i X.
Proof.
intros ?. rewrite <-elem_of_to_Pset by done.
unfold to_gset. by destruct (to_Pset X).
intros ?. rewrite <-elem_of_coPset_to_Pset by done.
unfold coPset_to_gset. by destruct (coPset_to_Pset X).
Qed.
Lemma elem_of_of_gset X i : i of_gset X i X.
Proof. destruct X as [[[t ?]]]; apply elem_of_of_Pset_raw. Qed.
Lemma of_gset_finite X : set_finite (of_gset X).
Lemma elem_of_gset_to_coPset X i : i gset_to_coPset X i X.
Proof. destruct X as [[[t ?]]]; apply elem_of_Pset_to_coPset_raw. Qed.
Lemma gset_to_coPset_finite X : set_finite (gset_to_coPset X).
Proof.
apply coPset_finite_spec; destruct X as [[[t ?]]]; apply of_Pset_raw_finite.
apply coPset_finite_spec; destruct X as [[[t ?]]]; apply Pset_to_coPset_raw_finite.
Qed.
(** * Domain of finite maps *)
Instance Pmap_dom_coPset {A} : Dom (Pmap A) coPset := λ m, of_Pset (dom _ m).
Instance Pmap_dom_coPset {A} : Dom (Pmap A) coPset := λ m, Pset_to_coPset (dom _ m).
Instance Pmap_dom_coPset_spec: FinMapDom positive Pmap coPset.
Proof.
split; try apply _; intros A m i; unfold dom, Pmap_dom_coPset.
by rewrite elem_of_of_Pset, elem_of_dom.
by rewrite elem_of_Pset_to_coPset, elem_of_dom.
Qed.
Instance gmap_dom_coPset {A} : Dom (gmap positive A) coPset := λ m,
of_gset (dom _ m).
gset_to_coPset (dom _ m).
Instance gmap_dom_coPset_spec: FinMapDom positive (gmap positive) coPset.
Proof.
split; try apply _; intros A m i; unfold dom, gmap_dom_coPset.
by rewrite elem_of_of_gset, elem_of_dom.
by rewrite elem_of_gset_to_coPset, elem_of_dom.
Qed.
(** * Suffix sets *)
......@@ -405,7 +405,7 @@ Definition coPset_r (X : coPset) : coPset :=
Lemma coPset_lr_disjoint X : coPset_l X coPset_r X = .
Proof.
apply elem_of_equiv_empty_L; intros p; apply Is_true_false.
destruct X as [t Ht]; simpl; clear Ht; rewrite elem_to_Pset_intersection.
destruct X as [t Ht]; simpl; clear Ht; rewrite coPset_elem_of_intersection.
revert p; induction t as [[]|[]]; intros [?|?|]; simpl;
rewrite ?coPset_elem_of_node; simpl;
rewrite ?orb_true_l, ?orb_false_l, ?orb_true_r, ?orb_false_r; auto.
......@@ -413,7 +413,7 @@ Qed.
Lemma coPset_lr_union X : coPset_l X coPset_r X = X.
Proof.
apply elem_of_equiv_L; intros p; apply eq_bool_prop_elim.
destruct X as [t Ht]; simpl; clear Ht; rewrite elem_to_Pset_union.
destruct X as [t Ht]; simpl; clear Ht; rewrite coPset_elem_of_union.
revert p; induction t as [[]|[]]; intros [?|?|]; simpl;
rewrite ?coPset_elem_of_node; simpl;
rewrite ?orb_true_l, ?orb_false_l, ?orb_true_r, ?orb_false_r; 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.