-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathfmsetlist_Type.v
246 lines (192 loc) · 7.48 KB
/
fmsetlist_Type.v
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
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
(** Finite Multiset over Lists
We define an axiomatization of finite multisets through their relation with lists.
Equality is required to be Coq equality.
Permutation are with output in [Type].
An implementation of the axioms is provided by sorted lists
for every type equiped with a Boolean-valued total order relation. *)
From Coq Require Import Bool List CMorphisms.
From OLlibs Require Import BOrders Permutation_Type_more.
Set Implicit Arguments.
Set Default Proof Using "Type".
(** * Axiomatization *)
(** A finite multiset with elements in [A] is a type [M]
related with [list A] as follows: *)
Class FinMultiset M A := {
empty : M;
add : A -> M -> M;
elts : M -> list A;
elts_empty : elts empty = @nil A;
elts_add : forall a m, Permutation_Type (elts (add a m)) (a :: elts m);
elts_retract : forall m, fold_right add empty (elts m) = m;
perm_eq : forall l1 l2, Permutation_Type l1 l2 ->
fold_right add empty l1 = fold_right add empty l2 }.
(** [Mst] and [Elt] define a finite multiset construction over a type [K]
if for any [A] in [K], [Mst A] is a finite multiset with elements [Elt A]. *)
Definition FMConstructor K Mst Elt := forall A : K, FinMultiset (Mst A) (Elt A).
(** * Constructions and properties over finite multisets *)
Section FMSet2List.
Variable M A : Type.
Variable fm : FinMultiset M A.
Definition list2fm l := fold_right add empty l.
#[export] Instance list2fm_perm : Proper (@Permutation_Type A ==> eq) list2fm
:= perm_eq.
Lemma list2fm_retract m : list2fm (elts m) = m.
Proof. apply elts_retract. Qed.
Lemma list2fm_nil : list2fm nil = empty.
Proof. reflexivity. Qed.
Lemma list2fm_elt l1 l2 a :
list2fm (l1 ++ a :: l2) = add a (list2fm (l1 ++ l2)).
Proof.
symmetry.
change (add a (list2fm (l1 ++ l2)))
with (list2fm (a :: l1 ++ l2)).
apply perm_eq, Permutation_Type_middle.
Qed.
Lemma list2fm_cons l a : list2fm (a :: l) = add a (list2fm l).
Proof. now rewrite <- (app_nil_l (a :: l)), list2fm_elt. Qed.
Lemma elts_perm l : Permutation_Type (elts (list2fm l)) l.
Proof.
induction l as [|a l IHl] ; simpl.
- now rewrite elts_empty.
- transitivity (a :: elts (list2fm l)).
+ apply elts_add.
+ now apply Permutation_Type_cons.
Qed.
#[export] Instance elts_perm' : Proper (eq ==> @Permutation_Type A) elts.
Proof. now intros m1 m2 Heq ; subst. Qed.
Lemma elts_eq_nil m : elts m = nil -> m = empty.
Proof.
intros Heq.
now assert (Hr := elts_retract m); rewrite Heq in Hr; simpl in Hr; subst.
Qed.
Lemma add_swap m a b : add a (add b m) = add b (add a m).
Proof.
rewrite <- list2fm_retract.
rewrite <- list2fm_retract at 1.
apply list2fm_perm.
etransitivity ; [ apply elts_add | ].
etransitivity ; [ apply Permutation_Type_cons ;
[ reflexivity | apply elts_add ] | ].
symmetry.
etransitivity ; [ apply elts_add | ].
etransitivity ; [ apply Permutation_Type_cons ;
[ reflexivity | apply elts_add ] | ].
apply Permutation_Type_swap.
Qed.
Definition sum m1 m2 := list2fm (elts m1 ++ elts m2).
Lemma elts_sum m1 m2 :
Permutation_Type (elts (sum m1 m2)) (elts m1 ++ elts m2).
Proof. apply elts_perm. Qed.
Lemma sum_empty_left m : sum empty m = m.
Proof. unfold sum; rewrite elts_empty; apply elts_retract. Qed.
Lemma sum_empty_right m : sum m empty = m.
Proof. unfold sum; rewrite elts_empty, app_nil_r; apply elts_retract. Qed.
Lemma sum_comm m1 m2 : sum m1 m2 = sum m2 m1.
Proof. apply list2fm_perm, Permutation_Type_app_comm. Qed.
Lemma sum_ass m1 m2 m3 : sum (sum m1 m2) m3 = sum m1 (sum m2 m3).
Proof.
unfold sum; apply perm_eq.
transitivity ((elts m1 ++ elts m2) ++ elts m3).
- apply Permutation_Type_app_tail, elts_perm.
- rewrite <- app_assoc; symmetry.
apply Permutation_Type_app_head, elts_perm.
Qed.
Lemma list2fm_app l1 l2 : list2fm (l1 ++ l2) = sum (list2fm l1) (list2fm l2).
Proof.
unfold sum; apply perm_eq.
transitivity (elts (list2fm l1) ++ l2); symmetry.
- apply Permutation_Type_app_tail, elts_perm.
- apply Permutation_Type_app_head, elts_perm.
Qed.
End FMSet2List.
Arguments list2fm {_ _ _} _.
Arguments sum {_ _ _} _ _.
Section Fmmap.
Variable M A N B : Type.
Variable fm : FinMultiset M A.
Variable fm' : FinMultiset N B.
Variable f : A -> B.
Definition fmmap (m : M) := list2fm (map f (elts m)).
Lemma list2fm_map l : list2fm (map f l) = fmmap (list2fm l).
Proof. symmetry; apply perm_eq, Permutation_Type_map, elts_perm. Qed.
Lemma elts_fmmap m : Permutation_Type (elts (fmmap m)) (map f (elts m)).
Proof.
rewrite <- (elts_retract m).
remember (elts m) as l eqn:Heql; clear m Heql; induction l; simpl.
- unfold fmmap; rewrite elts_empty; simpl.
now rewrite elts_empty.
- apply elts_perm.
Qed.
End Fmmap.
Arguments fmmap {_ _ _ _ _ _} _ _.
Section Induction.
Variable M A : Type.
Variable fm : FinMultiset M A.
Lemma fm_rect (P : M -> Type) :
P empty -> (forall a m, P m -> P (add a m)) -> forall m, P m.
Proof.
intros He Ha m.
remember (elts m) as l eqn:Heql.
apply Permutation_Type_refl' in Heql; unfold id in Heql.
revert m Heql; induction l as [|a l IHl]; intros m Heql.
- apply Permutation_Type_nil in Heql.
now apply elts_eq_nil in Heql; subst.
- assert (Hr := elts_retract m).
symmetry in Heql; rewrite (perm_eq Heql) in Hr; simpl in Hr; subst.
apply Ha, IHl.
symmetry.
change (fold_right add empty l) with (list2fm l).
apply elts_perm.
Defined.
Lemma fm_ind (P : M -> Prop) :
P empty -> (forall a m, P m -> P (add a m)) -> forall m, P m.
Proof. intros; apply fm_rect; assumption. Defined.
Lemma fm_rec (P : M -> Set) :
P empty -> (forall a m, P m -> P (add a m)) -> forall m, P m.
Proof. intros; apply fm_rect; assumption. Defined.
End Induction.
(** * Notations *)
Module FMSetNotations.
Infix ":::" := add (at level 60, right associativity).
Infix "+++" := sum (right associativity, at level 60).
Notation " [[ ]] " := empty.
Notation " [[ x ]] " := (add x empty).
Notation " [[ x ; .. ; y ]] " := (add x .. (add y empty) ..).
End FMSetNotations.
(** ** Sorted lists as finite multisets
Sorted lists provide a finite multisets construction for [BOrder]. *)
Definition fmslist_empty B : SortedList B := exist _ (nil) eq_refl.
Lemma fmslist_add B : @car B -> SortedList B -> SortedList B.
Proof.
intros a m.
exists (insert a (proj1_sig m)).
apply (insert_sorted a m); reflexivity.
Defined.
Lemma insert_add B (a : @car B) l :
proj1_sig (fmslist_add a l) = insert a (proj1_sig l).
Proof. reflexivity. Qed.
Theorem FMConstr_slist : FMConstructor SortedList (@car).
Proof.
intros A.
split with (@fmslist_empty A) (@fmslist_add A) (fun m => proj1_sig m); auto.
- intros a [l Hsort].
revert Hsort; induction l as [|a' l IHl]; simpl; intros Hsort; auto.
destruct (leb a a'); auto.
change (a :: a' :: l) with ((a :: nil) ++ a' :: l).
apply Permutation_Type_cons_app.
apply is_sorted_tail in Hsort.
apply (IHl Hsort).
- intros [l Hsort].
revert Hsort; induction l as [|a l IHl]; intros Hsort.
+ now apply sortedlist_equality.
+ destruct l as [|a' l]; apply sortedlist_equality; simpl; auto.
apply andb_true_iff in Hsort as [Ha Hsort].
assert (H' := IHl Hsort).
apply (f_equal (fun m => proj1_sig m)) in H'.
simpl in H'; rewrite H'; simpl.
destruct (leb a a'); [ reflexivity | discriminate Ha ].
- intros l1 l2 HP; induction HP as [| ? ? ? ? IHP | | ? ? ? ? IHP ]; simpl; auto.
+ now rewrite IHP.
+ apply sortedlist_equality, insert_insert.
+ now rewrite IHP.
Defined.