1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
|
(** 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.
From stdpp Require Import options.
Record listset_nodup A := ListsetNoDup {
listset_nodup_car : list A; listset_nodup_prf : NoDup listset_nodup_car
}.
Global Arguments ListsetNoDup {_} _ _ : assert.
Global Arguments listset_nodup_car {_} _ : assert.
Global Arguments listset_nodup_prf {_} _ : assert.
Section list_set.
Context `{EqDecision A}.
Notation C := (listset_nodup A).
Global Instance listset_nodup_elem_of: ElemOf A C := λ x l, x ∈ listset_nodup_car l.
Global Instance listset_nodup_empty: Empty C := ListsetNoDup [] (@NoDup_nil_2 _).
Global Instance listset_nodup_singleton: Singleton A C := λ x,
ListsetNoDup [x] (NoDup_singleton x).
Global Instance listset_nodup_union: Union C :=
λ '(ListsetNoDup l Hl) '(ListsetNoDup k Hk),
ListsetNoDup _ (NoDup_list_union _ _ Hl Hk).
Global Instance listset_nodup_intersection: Intersection C :=
λ '(ListsetNoDup l Hl) '(ListsetNoDup k Hk),
ListsetNoDup _ (NoDup_list_intersection _ k Hl).
Global Instance listset_nodup_difference: Difference C :=
λ '(ListsetNoDup l Hl) '(ListsetNoDup k Hk),
ListsetNoDup _ (NoDup_list_difference _ k Hl).
Local Instance listset_nodup_set: 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 listset_nodup_fin_set: FinSet A C.
Proof. split; [apply _|done|]. by intros [??]. Qed.
End list_set.
|
