Forked from
Iris / stdpp
1784 commits behind the upstream repository.
-
Robbert Krebbers authored
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") ```
Robbert Krebbers authoredGet 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") ```
listset_nodup.v 2.52 KiB
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements finite as unordered lists without duplicates.
Although this implementation is slow, it is very useful as decidable equality
is the only constraint on the carrier set. *)
From stdpp Require Export sets list.
Set Default Proof Using "Type".
Record listset_nodup A := ListsetNoDup {
listset_nodup_car : list A; listset_nodup_prf : NoDup listset_nodup_car
}.
Arguments ListsetNoDup {_} _ _ : assert.
Arguments listset_nodup_car {_} _ : assert.
Arguments listset_nodup_prf {_} _ : assert.
Section list_set.
Context `{EqDecision A}.
Notation C := (listset_nodup A).
Instance listset_nodup_elem_of: ElemOf A C := λ x l, x ∈ listset_nodup_car l.
Instance listset_nodup_empty: Empty C := ListsetNoDup [] (@NoDup_nil_2 _).
Instance listset_nodup_singleton: Singleton A C := λ x,
ListsetNoDup [x] (NoDup_singleton x).
Instance listset_nodup_union: Union C := λ l k,
let (l',Hl) := l in let (k',Hk) := k
in ListsetNoDup _ (NoDup_list_union _ _ Hl Hk).
Instance listset_nodup_intersection: Intersection C := λ l k,
let (l',Hl) := l in let (k',Hk) := k
in ListsetNoDup _ (NoDup_list_intersection _ k' Hl).
Instance listset_nodup_difference: Difference C := λ l k,
let (l',Hl) := l in let (k',Hk) := k
in ListsetNoDup _ (NoDup_list_difference _ k' Hl).
Instance: Set_ A C.
Proof.
split; [split | | ].
- by apply not_elem_of_nil.
- by apply elem_of_list_singleton.
- intros [??] [??] ?. apply elem_of_list_union.
- intros [??] [??] ?. apply elem_of_list_intersection.
- intros [??] [??] ?. apply elem_of_list_difference.
Qed.
Global Instance listset_nodup_elems: Elements A C := listset_nodup_car.
Global Instance: FinSet A C.
Proof. split. apply _. done. by intros [??]. Qed.
End list_set.
Hint Extern 1 (ElemOf _ (listset_nodup _)) =>
eapply @listset_nodup_elem_of : typeclass_instances.
Hint Extern 1 (Empty (listset_nodup _)) =>
eapply @listset_nodup_empty : typeclass_instances.
Hint Extern 1 (Singleton _ (listset_nodup _)) =>
eapply @listset_nodup_singleton : typeclass_instances.
Hint Extern 1 (Union (listset_nodup _)) =>
eapply @listset_nodup_union : typeclass_instances.
Hint Extern 1 (Intersection (listset_nodup _)) =>
eapply @listset_nodup_intersection : typeclass_instances.
Hint Extern 1 (Difference (listset_nodup _)) =>
eapply @listset_nodup_difference : typeclass_instances.
Hint Extern 1 (Elements _ (listset_nodup _)) =>
eapply @listset_nodup_elems : typeclass_instances.