Commit 310686e9 authored by Robbert Krebbers's avatar Robbert Krebbers

Consistently use `set_` prefix.

```
sed 's/collection\_equiv/set\_equiv/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/map\_of\_set/g;
s/\bof\_list/set\_of\_list/g;
s/\bof\_option/set\_of\_option/g;
s/elem\_of\_of\_list/elem\_of\_set\_of\_list/g;
s/elem\_of\_of\_option/elem\_of\_set\_of\_option/g;
s/collection\_not\_subset\_inv/set\_not\_subset\_inv/g;
' -i $(find -name "*.v")
```
parent 005887ee
......@@ -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 (set_of_list l : Pset)), elem_of_set_of_list, 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.
......
......@@ -9,19 +9,19 @@ From stdpp Require Export orders list.
(* Higher precedence to make sure these instances are not used for other types
with an [ElemOf] instance, such as lists. *)
Instance collection_equiv `{ElemOf A C} : Equiv C | 20 := λ X Y,
Instance set_equiv `{ElemOf A C} : Equiv C | 20 := λ X Y,
x, x X x Y.
Instance collection_subseteq `{ElemOf A C} : SubsetEq C | 20 := λ X Y,
Instance set_subseteq `{ElemOf A C} : SubsetEq C | 20 := λ X Y,
x, x X x Y.
Instance collection_disjoint `{ElemOf A C} : Disjoint C | 20 := λ X Y,
Instance set_disjoint `{ElemOf A C} : Disjoint C | 20 := λ X Y,
x, x X x Y False.
Typeclasses Opaque collection_equiv collection_subseteq collection_disjoint.
Typeclasses Opaque set_equiv set_subseteq set_disjoint.
(** * Setoids *)
Section setoids_simple.
Context `{SimpleCollection A C}.
Global Instance collection_equivalence : Equivalence (@{C}).
Global Instance set_equiv_equivalence : Equivalence (@{C}).
Proof.
split.
- done.
......@@ -161,13 +161,13 @@ Section set_unfold_simple.
Global Instance set_unfold_equiv_empty_l X (P : A Prop) :
( x, SetUnfold (x X) (P x)) SetUnfold ( X) ( x, ¬P x) | 5.
Proof.
intros ?; constructor. unfold equiv, collection_equiv.
intros ?; constructor. unfold equiv, set_equiv.
pose proof (not_elem_of_empty (C:=C)); naive_solver.
Qed.
Global Instance set_unfold_equiv_empty_r (P : A Prop) X :
( x, SetUnfold (x X) (P x)) SetUnfold (X ) ( x, ¬P x) | 5.
Proof.
intros ?; constructor. unfold equiv, collection_equiv.
intros ?; constructor. unfold equiv, set_equiv.
pose proof (not_elem_of_empty (C:=C)); naive_solver.
Qed.
Global Instance set_unfold_equiv (P Q : A Prop) X :
......@@ -188,7 +188,7 @@ Section set_unfold_simple.
Global Instance set_unfold_disjoint (P Q : A Prop) X Y :
( x, SetUnfold (x X) (P x)) ( x, SetUnfold (x Y) (Q x))
SetUnfold (X ## Y) ( x, P x Q x False).
Proof. constructor. unfold disjoint, collection_disjoint. naive_solver. Qed.
Proof. constructor. unfold disjoint, set_disjoint. naive_solver. Qed.
Context `{!LeibnizEquiv C}.
Global Instance set_unfold_equiv_same_L X : SetUnfold (X = X) True | 1.
......@@ -313,14 +313,14 @@ Section simple_collection.
(** Equality *)
Lemma elem_of_equiv X Y : X Y x, x X x Y.
Proof. set_solver. Qed.
Lemma collection_equiv_spec X Y : X Y X Y Y X.
Lemma set_equiv_spec X Y : X Y X Y Y X.
Proof. set_solver. Qed.
(** Subset relation *)
Global Instance collection_subseteq_antisymm: AntiSymm () (@{C}).
Global Instance set_subseteq_antisymm: AntiSymm () (@{C}).
Proof. intros ??. set_solver. Qed.
Global Instance collection_subseteq_preorder: PreOrder (@{C}).
Global Instance set_subseteq_preorder: PreOrder (@{C}).
Proof. split. by intros ??. intros ???; set_solver. Qed.
Lemma subseteq_union X Y : X Y X Y Y.
......@@ -465,11 +465,11 @@ Section simple_collection.
Lemma elem_of_equiv_L X Y : X = Y x, x X x Y.
Proof. unfold_leibniz. apply elem_of_equiv. Qed.
Lemma collection_equiv_spec_L X Y : X = Y X Y Y X.
Proof. unfold_leibniz. apply collection_equiv_spec. Qed.
Lemma set_equiv_spec_L X Y : X = Y X Y Y X.
Proof. unfold_leibniz. apply set_equiv_spec. Qed.
(** Subset relation *)
Global Instance collection_subseteq_partialorder : PartialOrder (@{C}).
Global Instance set_subseteq_partialorder : PartialOrder (@{C}).
Proof. split. apply _. intros ??. unfold_leibniz. apply (anti_symm _). Qed.
Lemma subseteq_union_L X Y : X Y X Y = Y.
......@@ -528,9 +528,9 @@ Section simple_collection.
Section dec.
Context `{!RelDecision (@{C})}.
Lemma collection_subseteq_inv X Y : X Y X Y X Y.
Lemma set_subseteq_inv X Y : X Y X Y X Y.
Proof. destruct (decide (X Y)); [by right|left;set_solver]. Qed.
Lemma collection_not_subset_inv X Y : X Y X Y X Y.
Lemma set_not_subset_inv X Y : X Y X Y X Y.
Proof. destruct (decide (X Y)); [by right|left;set_solver]. Qed.
Lemma non_empty_union X Y : X Y X Y .
......@@ -539,10 +539,10 @@ Section simple_collection.
Proof. rewrite empty_union_list. apply (not_Forall_Exists _). Qed.
Context `{!LeibnizEquiv C}.
Lemma collection_subseteq_inv_L X Y : X Y X Y X = Y.
Proof. unfold_leibniz. apply collection_subseteq_inv. Qed.
Lemma collection_not_subset_inv_L X Y : X Y X Y X = Y.
Proof. unfold_leibniz. apply collection_not_subset_inv. Qed.
Lemma set_subseteq_inv_L X Y : X Y X Y X = Y.
Proof. unfold_leibniz. apply set_subseteq_inv. Qed.
Lemma set_not_subset_inv_L X Y : X Y X Y X = Y.
Proof. unfold_leibniz. apply set_not_subset_inv. Qed.
Lemma non_empty_union_L X Y : X Y X Y .
Proof. unfold_leibniz. apply non_empty_union. Qed.
Lemma non_empty_union_list_L Xs : Xs Exists ( ) Xs.
......@@ -748,56 +748,56 @@ End collection.
(** * Conversion of option and list *)
Definition of_option `{Singleton A C, Empty C} (mx : option A) : C :=
Definition set_of_option `{Singleton A C, Empty C} (mx : option A) : C :=
match mx with None => | Some x => {[ x ]} end.
Fixpoint of_list `{Singleton A C, Empty C, Union C} (l : list A) : C :=
match l with [] => | x :: l => {[ x ]} of_list l end.
Fixpoint set_of_list `{Singleton A C, Empty C, Union C} (l : list A) : C :=
match l with [] => | x :: l => {[ x ]} set_of_list l end.
Section of_option_list.
Section set_of_option_list.
Context `{SimpleCollection A C}.
Implicit Types l : list A.
Lemma elem_of_of_option (x : A) mx: x of_option (C:=C) mx mx = Some x.
Lemma elem_of_set_of_option (x : A) mx: x set_of_option (C:=C) mx mx = Some x.
Proof. destruct mx; set_solver. Qed.
Lemma not_elem_of_of_option (x : A) mx: x of_option (C:=C) mx mx Some x.
Proof. by rewrite elem_of_of_option. Qed.
Lemma not_elem_of_set_of_option (x : A) mx: x set_of_option (C:=C) mx mx Some x.
Proof. by rewrite elem_of_set_of_option. Qed.
Lemma elem_of_of_list (x : A) l : x of_list (C:=C) l x l.
Lemma elem_of_set_of_list (x : A) l : x set_of_list (C:=C) l x l.
Proof.
split.
- induction l; simpl; [by rewrite elem_of_empty|].
rewrite elem_of_union,elem_of_singleton; intros [->|?]; constructor; auto.
- induction 1; simpl; rewrite elem_of_union, elem_of_singleton; auto.
Qed.
Lemma not_elem_of_of_list (x : A) l : x of_list (C:=C) l x l.
Proof. by rewrite elem_of_of_list. Qed.
Lemma not_elem_of_set_of_list (x : A) l : x set_of_list (C:=C) l x l.
Proof. by rewrite elem_of_set_of_list. Qed.
Global Instance set_unfold_of_option (mx : option A) x :
SetUnfold (x of_option (C:=C) mx) (mx = Some x).
Proof. constructor; apply elem_of_of_option. Qed.
SetUnfold (x set_of_option (C:=C) mx) (mx = Some x).
Proof. constructor; apply elem_of_set_of_option. Qed.
Global Instance set_unfold_of_list (l : list A) x P :
SetUnfold (x l) P SetUnfold (x of_list (C:=C) l) P.
Proof. constructor. by rewrite elem_of_of_list, (set_unfold (x l) P). Qed.
SetUnfold (x l) P SetUnfold (x set_of_list (C:=C) l) P.
Proof. constructor. by rewrite elem_of_set_of_list, (set_unfold (x l) P). Qed.
Lemma of_list_nil : of_list [] =@{C} .
Lemma set_of_list_nil : set_of_list [] =@{C} .
Proof. done. Qed.
Lemma of_list_cons x l : of_list (x :: l) =@{C} {[ x ]} of_list l.
Lemma set_of_list_cons x l : set_of_list (x :: l) =@{C} {[ x ]} set_of_list l.
Proof. done. Qed.
Lemma of_list_app l1 l2 : of_list (l1 ++ l2) @{C} of_list l1 of_list l2.
Lemma set_of_list_app l1 l2 : set_of_list (l1 ++ l2) @{C} set_of_list l1 set_of_list l2.
Proof. set_solver. Qed.
Global Instance of_list_perm : Proper (() ==> ()) (of_list (C:=C)).
Global Instance set_of_list_perm : Proper (() ==> ()) (set_of_list (C:=C)).
Proof. induction 1; set_solver. Qed.
Context `{!LeibnizEquiv C}.
Lemma of_list_app_L l1 l2 : of_list (l1 ++ l2) =@{C} of_list l1 of_list l2.
Lemma set_of_list_app_L l1 l2 : set_of_list (l1 ++ l2) =@{C} set_of_list l1 set_of_list l2.
Proof. set_solver. Qed.
Global Instance of_list_perm_L : Proper (() ==> (=)) (of_list (C:=C)).
Global Instance set_of_list_perm_L : Proper (() ==> (=)) (set_of_list (C:=C)).
Proof. induction 1; set_solver. Qed.
End of_option_list.
End set_of_option_list.
(** * Guard *)
Global Instance collection_guard `{CollectionMonad M} : MGuard M :=
Global Instance set_guard `{CollectionMonad M} : MGuard M :=
λ P dec A x, match dec with left H => x H | _ => end.
Section collection_monad_base.
......@@ -805,7 +805,7 @@ Section collection_monad_base.
Lemma elem_of_guard `{Decision P} {A} (x : A) (X : M A) :
(x guard P; X) P x X.
Proof.
unfold mguard, collection_guard; simpl; case_match;
unfold mguard, set_guard; simpl; case_match;
rewrite ?elem_of_empty; naive_solver.
Qed.
Lemma elem_of_guard_2 `{Decision P} {A} (x : A) (X : M A) :
......@@ -949,7 +949,7 @@ Section collection_monad.
Lemma collection_bind_singleton {A B} (f : A M B) x : {[ x ]} = f f x.
Proof. set_solver. Qed.
Lemma collection_guard_True {A} `{Decision P} (X : M A) : P (guard P; X) X.
Lemma set_guard_True {A} `{Decision P} (X : M A) : P (guard P; X) X.
Proof. set_solver. Qed.
Lemma collection_fmap_compose {A B C} (f : A B) (g : B C) (X : M A) :
g f <$> X g <$> (f <$> X).
......@@ -971,7 +971,7 @@ Section collection_monad.
- revert l. induction k; set_solver by eauto.
- induction 1; set_solver.
Qed.
Lemma collection_mapM_length {A B} (f : A M B) l k :
Lemma set_mapM_length {A B} (f : A M B) l k :
l mapM f k length l = length k.
Proof. revert l; induction k; set_solver by eauto. Qed.
Lemma elem_of_mapM_fmap {A B} (f : A B) (g : B M A) l k :
......
......@@ -7,19 +7,19 @@ From stdpp Require Import relations.
From stdpp Require Export numbers collections.
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.
set_of_list (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.
set_of_list (f <$> elements X).
Typeclasses Opaque set_map.
Section fin_collection.
Context `{FinCollection A C}.
......@@ -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_set_of_list, 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).
......@@ -258,31 +258,31 @@ Section map.
Context `{Collection 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_set_of_list, 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.
......
......@@ -66,10 +66,10 @@ Definition map_of_list `{Insert K A M, Empty M} : list (K * A) → M :=
Instance map_size `{FinMapToList K A M} : Size M := λ m, length (map_to_list m).
Definition map_to_collection `{FinMapToList K A M,
Definition map_to_set `{FinMapToList K A M,
Singleton B C, Empty C, Union C} (f : K A B) (m : M) : C :=
of_list (curry f <$> map_to_list m).
Definition map_of_collection `{Elements B C, Insert K A M, Empty M}
set_of_list (curry f <$> map_to_list m).
Definition map_of_set `{Elements B C, Insert K A M, Empty M}
(f : B K * A) (X : C) : M :=
map_of_list (f <$> elements X).
......@@ -893,53 +893,53 @@ Proof. intros. unfold size, map_size. by rewrite map_to_list_fmap, fmap_length.
Section map_of_to_collection.
Context {A : Type} `{FinCollection B C}.
Lemma lookup_map_of_collection (f : B K * A) (Y : C) i x :
Lemma lookup_map_of_set (f : B K * A) (Y : C) i x :
( y y', y Y y' Y (f y).1 = (f y').1 y = y')
(map_of_collection f Y : M A) !! i = Some x y, y Y f y = (i,x).
(map_of_set f Y : M A) !! i = Some x y, y Y f y = (i,x).
Proof.
intros Hinj. assert ( x',
(i, x) f <$> elements Y (i, x') f <$> elements Y x = x').
{ intros x'. intros (y&Hx&Hy)%elem_of_list_fmap (y'&Hx'&Hy')%elem_of_list_fmap.
rewrite elem_of_elements in Hy, Hy'.
cut (y = y'); [congruence|]. apply Hinj; auto. by rewrite <-Hx, <-Hx'. }
unfold map_of_collection; rewrite <-elem_of_map_of_list' by done.
unfold map_of_set; rewrite <-elem_of_map_of_list' by done.
rewrite elem_of_list_fmap. setoid_rewrite elem_of_elements; naive_solver.
Qed.
Lemma elem_of_map_to_collection (f : K A B) (m : M A) (y : B) :
y map_to_collection (C:=C) f m i x, m !! i = Some x f i x = y.
Lemma elem_of_map_to_set (f : K A B) (m : M A) (y : B) :
y map_to_set (C:=C) f m i x, m !! i = Some x f i x = y.
Proof.
unfold map_to_collection; simpl.
rewrite elem_of_of_list, elem_of_list_fmap. split.
unfold map_to_set; simpl.
rewrite elem_of_set_of_list, elem_of_list_fmap. split.
- intros ([i x] & ? & ?%elem_of_map_to_list); eauto.
- intros (i&x&?&?). exists (i,x). by rewrite elem_of_map_to_list.
Qed.
Lemma map_to_collection_empty (f : K A B) :
map_to_collection f ( : M A) = ( : C).
Proof. unfold map_to_collection; simpl. by rewrite map_to_list_empty. Qed.
Lemma map_to_collection_insert (f : K A B)(m : M A) i x :
Lemma map_to_set_empty (f : K A B) :
map_to_set f ( : M A) = ( : C).
Proof. unfold map_to_set; simpl. by rewrite map_to_list_empty. Qed.
Lemma map_to_set_insert (f : K A B)(m : M A) i x :
m !! i = None
map_to_collection f (<[i:=x]>m) @{C} {[f i x]} map_to_collection f m.
map_to_set f (<[i:=x]>m) @{C} {[f i x]} map_to_set f m.
Proof.
intros. unfold map_to_collection; simpl. by rewrite map_to_list_insert.
intros. unfold map_to_set; simpl. by rewrite map_to_list_insert.
Qed.
Lemma map_to_collection_insert_L `{!LeibnizEquiv C} (f : K A B) (m : M A) i x :
Lemma map_to_set_insert_L `{!LeibnizEquiv C} (f : K A B) (m : M A) i x :
m !! i = None
map_to_collection f (<[i:=x]>m) =@{C} {[f i x]} map_to_collection f m.
Proof. unfold_leibniz. apply map_to_collection_insert. Qed.
map_to_set f (<[i:=x]>m) =@{C} {[f i x]} map_to_set f m.
Proof. unfold_leibniz. apply map_to_set_insert. Qed.
End map_of_to_collection.
Lemma lookup_map_of_collection_id `{FinCollection (K * A) C} (X : C) i x :
Lemma lookup_map_of_set_id `{FinCollection (K * A) C} (X : C) i x :
( i y y', (i,y) X (i,y') X y = y')
(map_of_collection id X : M A) !! i = Some x (i,x) X.
(map_of_set id X : M A) !! i = Some x (i,x) X.
Proof.
intros. etrans; [apply lookup_map_of_collection|naive_solver].
intros. etrans; [apply lookup_map_of_set|naive_solver].
intros [] [] ???; simplify_eq/=; eauto with f_equal.
Qed.
Lemma elem_of_map_to_collection_pair `{FinCollection (K * A) C} (m : M A) i x :
(i,x) map_to_collection pair m m !! i = Some x.
Proof. rewrite elem_of_map_to_collection. naive_solver. Qed.
Lemma elem_of_map_to_set_pair `{FinCollection (K * A) C} (m : M A) i x :
(i,x) map_to_set pair m m !! i = Some x.
Proof. rewrite elem_of_map_to_set. naive_solver. Qed.
(** ** Induction principles *)
Lemma map_ind {A} (P : M A Prop) :
......
......@@ -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}).