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
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
|
Require Import
Coq.MSets.MSetInterface Coq.MSets.MSetFacts Coq.MSets.MSetProperties
MathClasses.implementations.list MathClasses.implementations.list_finite_set MathClasses.theory.finite_sets
MathClasses.interfaces.finite_sets MathClasses.interfaces.orders MathClasses.interfaces.abstract_algebra.
Import ListNotations.
Module MSet_FSet (E : DecidableType) (Import set : WSetsOn E).
Module facts := WFactsOn E set.
Module props := WPropertiesOn E set.
#[global]
Instance mset: SetType elt := t.
#[global]
Instance mset_in: SetContains elt := In.
#[global]
Instance mset_car_eq: Equiv elt := E.eq.
#[global]
Instance mset_eq: SetEquiv elt := Equal.
#[global]
Instance mset_le: SetLe elt := Subset.
#[global]
Instance mset_singleton: SetSingleton elt := singleton.
#[global]
Instance mset_empty: EmptySet elt := empty.
#[global]
Instance mset_join: SetJoin elt := union.
#[global]
Instance mset_meet: SetMeet elt := inter.
#[global]
Instance mset_difference: SetDifference elt := diff.
#[global]
Instance mset_car_dec: ∀ x y : elt, Decision (x = y) := E.eq_dec.
#[global]
Instance mset_dec: ∀ x y : t, Decision (x = y) := eq_dec.
Local Instance: Setoid elt.
Proof. split; try apply _. Qed.
Local Instance: BoundedJoinSemiLattice mset.
Proof.
Local Opaque Equal.
repeat (split; try apply _); repeat intro.
symmetry. now apply props.union_assoc.
now apply props.empty_union_1, empty_spec.
now apply props.empty_union_2, empty_spec.
now apply props.union_sym.
apply props.union_subset_equal, props.subset_refl.
Local Transparent Equal.
Qed.
Local Instance: Setoid_Morphism singleton.
Proof. split; try apply _. Qed.
Definition to_listset (X : @set_type _ mset) : @set_type _ (listset elt)
:= props.to_list X↾elements_spec2w X.
#[global]
Instance from_listset: Inverse to_listset := λ l, props.of_list (`l).
Local Instance: Setoid_Morphism to_listset.
Proof.
split; try apply _. intros X Y E x.
change (InA E.eq x (props.to_list X) ↔ InA E.eq x (props.to_list Y)).
now rewrite <-!props.of_list_1, 2!props.of_list_3, E.
Qed.
#[global]
Instance: Bijective to_listset.
Proof.
split; split; try apply _.
intros X Y E x. rewrite <-!elements_spec1. now apply E.
intros ?? E. rewrite <-E. now rapply props.of_list_2.
Qed.
#[global]
Instance: BoundedJoinSemiLattice_Morphism to_listset.
Proof.
split; try apply _; split; try apply _.
split; try apply _. intros X Y z.
setoid_rewrite listset_in_join.
repeat setoid_rewrite elements_spec1.
apply union_spec.
intros z. compute. rewrite props.elements_empty. tauto.
Qed.
#[global]
Instance mset_extend: FSetExtend elt := iso_is_fset_extend id to_listset.
Local Instance: FSet elt.
Proof.
apply (iso_is_fset id to_listset).
intros x y E z.
change (InA E.eq z (elements (singleton x)) ↔ InA E.eq z [y]).
now rewrite elements_spec1, singleton_spec, E, InA_singleton.
Qed.
#[global]
Instance: FullFSet elt.
Proof.
split; try apply _. split.
apply lattices.alt_Build_JoinSemiLatticeOrder.
intros X Y. split; intros E.
now apply props.union_subset_equal.
rewrite <-E. now apply props.union_subset_1.
intros x X. split; intros E.
transitivity (add x empty).
now apply props.subset_equal, props.singleton_equal_add.
apply props.subset_add_3. auto. now apply props.subset_empty.
apply props.union_subset_equal in E. rewrite <-E.
now apply facts.union_2, singleton_spec.
now apply inter_spec.
now apply diff_spec.
Qed.
End MSet_FSet.
|
