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
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id$ i*)
Require Addr.
Require Addec.
Require Map.
Require Fset.
Require Mapaxioms.
Require Mapsubset.
Require Mapcard.
Require Mapcanon.
Require Mapc.
Require Bool.
Require Sumbool.
Require PolyList.
Require Arith.
Require Mapiter.
Require Mapfold.
Section MapLists.
Fixpoint ad_in_list [a:ad;l:(list ad)] : bool :=
Cases l of
nil => false
| (cons a' l') => (orb (ad_eq a a') (ad_in_list a l'))
end.
Fixpoint ad_list_stutters [l:(list ad)] : bool :=
Cases l of
nil => false
| (cons a l') => (orb (ad_in_list a l') (ad_list_stutters l'))
end.
Lemma ad_in_list_forms_circuit : (x:ad) (l:(list ad)) (ad_in_list x l)=true ->
{l1 : (list ad) & {l2 : (list ad) | l=(app l1 (cons x l2))}}.
Proof.
Induction l. Intro. Discriminate H.
Intros. Elim (sumbool_of_bool (ad_eq x a)). Intro H1. Simpl in H0. Split with (nil ad).
Split with l0. Rewrite (ad_eq_complete ? ? H1). Reflexivity.
Intro H2. Simpl in H0. Rewrite H2 in H0. Simpl in H0. Elim (H H0). Intros l'1 H3.
Split with (cons a l'1). Elim H3. Intros l2 H4. Split with l2. Rewrite H4. Reflexivity.
Qed.
Lemma ad_list_stutters_has_circuit : (l:(list ad)) (ad_list_stutters l)=true ->
{x:ad & {l0 : (list ad) & {l1 : (list ad) & {l2 : (list ad) |
l=(app l0 (cons x (app l1 (cons x l2))))}}}}.
Proof.
Induction l. Intro. Discriminate H.
Intros. Simpl in H0. Elim (orb_true_elim ? ? H0). Intro H1. Split with a.
Split with (nil ad). Simpl. Elim (ad_in_list_forms_circuit a l0 H1). Intros l1 H2.
Split with l1. Elim H2. Intros l2 H3. Split with l2. Rewrite H3. Reflexivity.
Intro H1. Elim (H H1). Intros x H2. Split with x. Elim H2. Intros l1 H3.
Split with (cons a l1). Elim H3. Intros l2 H4. Split with l2. Elim H4. Intros l3 H5.
Split with l3. Rewrite H5. Reflexivity.
Qed.
Fixpoint Elems [l:(list ad)] : FSet :=
Cases l of
nil => (M0 unit)
| (cons a l') => (MapPut ? (Elems l') a tt)
end.
Lemma Elems_canon : (l:(list ad)) (mapcanon ? (Elems l)).
Proof.
Induction l. Exact (M0_canon unit).
Intros. Simpl. Apply MapPut_canon. Assumption.
Qed.
Lemma Elems_app : (l,l':(list ad)) (Elems (app l l'))=(FSetUnion (Elems l) (Elems l')).
Proof.
Induction l. Trivial.
Intros. Simpl. Rewrite (MapPut_as_Merge_c unit (Elems l0)).
Rewrite (MapPut_as_Merge_c unit (Elems (app l0 l'))).
Change (FSetUnion (Elems (app l0 l')) (M1 unit a tt))
=(FSetUnion (FSetUnion (Elems l0) (M1 unit a tt)) (Elems l')).
Rewrite FSetUnion_comm_c. Rewrite (FSetUnion_comm_c (Elems l0) (M1 unit a tt)).
Rewrite FSetUnion_assoc_c. Rewrite (H l'). Reflexivity.
Apply M1_canon.
Apply Elems_canon.
Apply Elems_canon.
Apply Elems_canon.
Apply M1_canon.
Apply Elems_canon.
Apply M1_canon.
Apply Elems_canon.
Apply Elems_canon.
Qed.
Lemma Elems_rev : (l:(list ad)) (Elems (rev l))=(Elems l).
Proof.
Induction l. Trivial.
Intros. Simpl. Rewrite Elems_app. Simpl. Rewrite (MapPut_as_Merge_c unit (Elems l0)).
Rewrite H. Reflexivity.
Apply Elems_canon.
Qed.
Lemma ad_in_elems_in_list : (l:(list ad)) (a:ad) (in_FSet a (Elems l))=(ad_in_list a l).
Proof.
Induction l. Trivial.
Simpl. Unfold in_FSet. Intros. Rewrite (in_dom_put ? (Elems l0) a tt a0).
Rewrite (H a0). Reflexivity.
Qed.
Lemma ad_list_not_stutters_card : (l:(list ad)) (ad_list_stutters l)=false ->
(length l)=(MapCard ? (Elems l)).
Proof.
Induction l. Trivial.
Simpl. Intros. Rewrite MapCard_Put_2_conv. Rewrite H. Reflexivity.
Elim (orb_false_elim ? ? H0). Trivial.
Elim (sumbool_of_bool (in_FSet a (Elems l0))). Rewrite ad_in_elems_in_list.
Intro H1. Rewrite H1 in H0. Discriminate H0.
Exact (in_dom_none unit (Elems l0) a).
Qed.
Lemma ad_list_card : (l:(list ad)) (le (MapCard ? (Elems l)) (length l)).
Proof.
Induction l. Trivial.
Intros. Simpl. Apply le_trans with m:=(S (MapCard ? (Elems l0))). Apply MapCard_Put_ub.
Apply le_n_S. Assumption.
Qed.
Lemma ad_list_stutters_card : (l:(list ad)) (ad_list_stutters l)=true ->
(lt (MapCard ? (Elems l)) (length l)).
Proof.
Induction l. Intro. Discriminate H.
Intros. Simpl. Simpl in H0. Elim (orb_true_elim ? ? H0). Intro H1.
Rewrite <- (ad_in_elems_in_list l0 a) in H1. Elim (in_dom_some ? ? ? H1). Intros y H2.
Rewrite (MapCard_Put_1_conv ? ? ? ? tt H2). Apply le_lt_trans with m:=(length l0).
Apply ad_list_card.
Apply lt_n_Sn.
Intro H1. Apply le_lt_trans with m:=(S (MapCard ? (Elems l0))). Apply MapCard_Put_ub.
Apply lt_n_S. Apply H. Assumption.
Qed.
Lemma ad_list_not_stutters_card_conv : (l:(list ad)) (length l)=(MapCard ? (Elems l)) ->
(ad_list_stutters l)=false.
Proof.
Intros. Elim (sumbool_of_bool (ad_list_stutters l)). Intro H0.
Cut (lt (MapCard ? (Elems l)) (length l)). Intro. Rewrite H in H1. Elim (lt_n_n ? H1).
Exact (ad_list_stutters_card ? H0).
Trivial.
Qed.
Lemma ad_list_stutters_card_conv : (l:(list ad)) (lt (MapCard ? (Elems l)) (length l)) ->
(ad_list_stutters l)=true.
Proof.
Intros. Elim (sumbool_of_bool (ad_list_stutters l)). Trivial.
Intro H0. Rewrite (ad_list_not_stutters_card ? H0) in H. Elim (lt_n_n ? H).
Qed.
Lemma ad_in_list_l : (l,l':(list ad)) (a:ad) (ad_in_list a l)=true ->
(ad_in_list a (app l l'))=true.
Proof.
Induction l. Intros. Discriminate H.
Intros. Simpl. Simpl in H0. Elim (orb_true_elim ? ? H0). Intro H1. Rewrite H1. Reflexivity.
Intro H1. Rewrite (H l' a0 H1). Apply orb_b_true.
Qed.
Lemma ad_list_stutters_app_l : (l,l':(list ad)) (ad_list_stutters l)=true ->
(ad_list_stutters (app l l'))=true.
Proof.
Induction l. Intros. Discriminate H.
Intros. Simpl. Simpl in H0. Elim (orb_true_elim ? ? H0). Intro H1.
Rewrite (ad_in_list_l l0 l' a H1). Reflexivity.
Intro H1. Rewrite (H l' H1). Apply orb_b_true.
Qed.
Lemma ad_in_list_r : (l,l':(list ad)) (a:ad) (ad_in_list a l')=true ->
(ad_in_list a (app l l'))=true.
Proof.
Induction l. Trivial.
Intros. Simpl. Rewrite (H l' a0 H0). Apply orb_b_true.
Qed.
Lemma ad_list_stutters_app_r : (l,l':(list ad)) (ad_list_stutters l')=true ->
(ad_list_stutters (app l l'))=true.
Proof.
Induction l. Trivial.
Intros. Simpl. Rewrite (H l' H0). Apply orb_b_true.
Qed.
Lemma ad_list_stutters_app_conv_l : (l,l':(list ad)) (ad_list_stutters (app l l'))=false ->
(ad_list_stutters l)=false.
Proof.
Intros. Elim (sumbool_of_bool (ad_list_stutters l)). Intro H0.
Rewrite (ad_list_stutters_app_l l l' H0) in H. Discriminate H.
Trivial.
Qed.
Lemma ad_list_stutters_app_conv_r : (l,l':(list ad)) (ad_list_stutters (app l l'))=false ->
(ad_list_stutters l')=false.
Proof.
Intros. Elim (sumbool_of_bool (ad_list_stutters l')). Intro H0.
Rewrite (ad_list_stutters_app_r l l' H0) in H. Discriminate H.
Trivial.
Qed.
Lemma ad_in_list_app_1 : (l,l':(list ad)) (x:ad) (ad_in_list x (app l (cons x l')))=true.
Proof.
Induction l. Simpl. Intros. Rewrite (ad_eq_correct x). Reflexivity.
Intros. Simpl. Rewrite (H l' x). Apply orb_b_true.
Qed.
Lemma ad_in_list_app : (l,l':(list ad)) (x:ad)
(ad_in_list x (app l l'))=(orb (ad_in_list x l) (ad_in_list x l')).
Proof.
Induction l. Trivial.
Intros. Simpl. Rewrite <- orb_assoc. Rewrite (H l' x). Reflexivity.
Qed.
Lemma ad_in_list_rev : (l:(list ad)) (x:ad)
(ad_in_list x (rev l))=(ad_in_list x l).
Proof.
Induction l. Trivial.
Intros. Simpl. Rewrite ad_in_list_app. Rewrite (H x). Simpl. Rewrite orb_b_false.
Apply orb_sym.
Qed.
Lemma ad_list_has_circuit_stutters : (l0,l1,l2:(list ad)) (x:ad)
(ad_list_stutters (app l0 (cons x (app l1 (cons x l2)))))=true.
Proof.
Induction l0. Simpl. Intros. Rewrite (ad_in_list_app_1 l1 l2 x). Reflexivity.
Intros. Simpl. Rewrite (H l1 l2 x). Apply orb_b_true.
Qed.
Lemma ad_list_stutters_prev_l : (l,l':(list ad)) (x:ad) (ad_in_list x l)=true ->
(ad_list_stutters (app l (cons x l')))=true.
Proof.
Intros. Elim (ad_in_list_forms_circuit ? ? H). Intros l0 H0. Elim H0. Intros l1 H1.
Rewrite H1. Rewrite app_ass. Simpl. Apply ad_list_has_circuit_stutters.
Qed.
Lemma ad_list_stutters_prev_conv_l : (l,l':(list ad)) (x:ad)
(ad_list_stutters (app l (cons x l')))=false -> (ad_in_list x l)=false.
Proof.
Intros. Elim (sumbool_of_bool (ad_in_list x l)). Intro H0.
Rewrite (ad_list_stutters_prev_l l l' x H0) in H. Discriminate H.
Trivial.
Qed.
Lemma ad_list_stutters_prev_r : (l,l':(list ad)) (x:ad) (ad_in_list x l')=true ->
(ad_list_stutters (app l (cons x l')))=true.
Proof.
Intros. Elim (ad_in_list_forms_circuit ? ? H). Intros l0 H0. Elim H0. Intros l1 H1.
Rewrite H1. Apply ad_list_has_circuit_stutters.
Qed.
Lemma ad_list_stutters_prev_conv_r : (l,l':(list ad)) (x:ad)
(ad_list_stutters (app l (cons x l')))=false -> (ad_in_list x l')=false.
Proof.
Intros. Elim (sumbool_of_bool (ad_in_list x l')). Intro H0.
Rewrite (ad_list_stutters_prev_r l l' x H0) in H. Discriminate H.
Trivial.
Qed.
Lemma ad_list_Elems : (l,l':(list ad)) (MapCard ? (Elems l))=(MapCard ? (Elems l')) ->
(length l)=(length l') ->
(ad_list_stutters l)=(ad_list_stutters l').
Proof.
Intros. Elim (sumbool_of_bool (ad_list_stutters l)). Intro H1. Rewrite H1. Apply sym_eq.
Apply ad_list_stutters_card_conv. Rewrite <- H. Rewrite <- H0. Apply ad_list_stutters_card.
Assumption.
Intro H1. Rewrite H1. Apply sym_eq. Apply ad_list_not_stutters_card_conv. Rewrite <- H.
Rewrite <- H0. Apply ad_list_not_stutters_card. Assumption.
Qed.
Lemma ad_list_app_length : (l,l':(list ad)) (length (app l l'))=(plus (length l) (length l')).
Proof.
Induction l. Trivial.
Intros. Simpl. Rewrite (H l'). Reflexivity.
Qed.
Lemma ad_list_stutters_permute : (l,l':(list ad))
(ad_list_stutters (app l l'))=(ad_list_stutters (app l' l)).
Proof.
Intros. Apply ad_list_Elems. Rewrite Elems_app. Rewrite Elems_app.
Rewrite (FSetUnion_comm_c ? ? (Elems_canon l) (Elems_canon l')). Reflexivity.
Rewrite ad_list_app_length. Rewrite ad_list_app_length. Apply plus_sym.
Qed.
Lemma ad_list_rev_length : (l:(list ad)) (length (rev l))=(length l).
Proof.
Induction l. Trivial.
Intros. Simpl. Rewrite ad_list_app_length. Simpl. Rewrite H. Rewrite <- plus_Snm_nSm.
Rewrite <- plus_n_O. Reflexivity.
Qed.
Lemma ad_list_stutters_rev : (l:(list ad)) (ad_list_stutters (rev l))=(ad_list_stutters l).
Proof.
Intros. Apply ad_list_Elems. Rewrite Elems_rev. Reflexivity.
Apply ad_list_rev_length.
Qed.
Lemma ad_list_app_rev : (l,l':(list ad)) (x:ad)
(app (rev l) (cons x l'))=(app (rev (cons x l)) l').
Proof.
Induction l. Trivial.
Intros. Simpl. Rewrite (app_ass (rev l0) (cons a (nil ad)) (cons x l')). Simpl.
Rewrite (H (cons x l') a). Simpl.
Rewrite (app_ass (rev l0) (cons a (nil ad)) (cons x (nil ad))). Simpl.
Rewrite app_ass. Simpl. Rewrite app_ass. Reflexivity.
Qed.
Section ListOfDomDef.
Variable A : Set.
Definition ad_list_of_dom :=
(MapFold A (list ad) (nil ad) (!app ad) [a:ad][_:A] (cons a (nil ad))).
Lemma ad_in_list_of_dom_in_dom : (m:(Map A)) (a:ad)
(ad_in_list a (ad_list_of_dom m))=(in_dom A a m).
Proof.
Unfold ad_list_of_dom. Intros.
Rewrite (MapFold_distr_l A (list ad) (nil ad) (!app ad) bool false orb
ad [a:ad][l:(list ad)](ad_in_list a l) [c:ad](refl_equal ? ?)
ad_in_list_app [a0:ad][_:A](cons a0 (nil ad)) m a).
Simpl. Rewrite (MapFold_orb A [a0:ad][_:A](orb (ad_eq a a0) false) m).
Elim (option_sum ? (MapSweep A [a0:ad][_:A](orb (ad_eq a a0) false) m)). Intro H. Elim H.
Intro r. Elim r. Intros a0 y H0. Rewrite H0. Unfold in_dom.
Elim (orb_prop ? ? (MapSweep_semantics_1 ? ? ? ? ? H0)). Intro H1.
Rewrite (ad_eq_complete ? ? H1). Rewrite (MapSweep_semantics_2 A ? ? ? ? H0). Reflexivity.
Intro H1. Discriminate H1.
Intro H. Rewrite H. Elim (sumbool_of_bool (in_dom A a m)). Intro H0.
Elim (in_dom_some A m a H0). Intros y H1.
Elim (orb_false_elim ? ? (MapSweep_semantics_3 ? ? ? H ? ? H1)). Intro H2.
Rewrite (ad_eq_correct a) in H2. Discriminate H2.
Exact (sym_eq ? ? ?).
Qed.
Lemma Elems_of_list_of_dom :
(m:(Map A)) (eqmap unit (Elems (ad_list_of_dom m)) (MapDom A m)).
Proof.
Unfold eqmap eqm. Intros. Elim (sumbool_of_bool (in_FSet a (Elems (ad_list_of_dom m)))).
Intro H. Elim (in_dom_some ? ? ? H). Intro t. Elim t. Intro H0.
Rewrite (ad_in_elems_in_list (ad_list_of_dom m) a) in H.
Rewrite (ad_in_list_of_dom_in_dom m a) in H. Rewrite (MapDom_Dom A m a) in H.
Elim (in_dom_some ? ? ? H). Intro t'. Elim t'. Intro H1. Rewrite H1. Assumption.
Intro H. Rewrite (in_dom_none ? ? ? H).
Rewrite (ad_in_elems_in_list (ad_list_of_dom m) a) in H.
Rewrite (ad_in_list_of_dom_in_dom m a) in H. Rewrite (MapDom_Dom A m a) in H.
Rewrite (in_dom_none ? ? ? H). Reflexivity.
Qed.
Lemma Elems_of_list_of_dom_c : (m:(Map A)) (mapcanon A m) ->
(Elems (ad_list_of_dom m))=(MapDom A m).
Proof.
Intros. Apply (mapcanon_unique unit). Apply Elems_canon.
Apply MapDom_canon. Assumption.
Apply Elems_of_list_of_dom.
Qed.
Lemma ad_list_of_dom_card_1 : (m:(Map A)) (pf:ad->ad)
(length (MapFold1 A (list ad) (nil ad) (app 1!ad) [a:ad][_:A](cons a (nil ad)) pf m))=
(MapCard A m).
Proof.
Induction m; Try Trivial. Simpl. Intros. Rewrite ad_list_app_length.
Rewrite (H [a0:ad](pf (ad_double a0))). Rewrite (H0 [a0:ad](pf (ad_double_plus_un a0))).
Reflexivity.
Qed.
Lemma ad_list_of_dom_card : (m:(Map A)) (length (ad_list_of_dom m))=(MapCard A m).
Proof.
Exact [m:(Map A)](ad_list_of_dom_card_1 m [a:ad]a).
Qed.
Lemma ad_list_of_dom_not_stutters :
(m:(Map A)) (ad_list_stutters (ad_list_of_dom m))=false.
Proof.
Intro. Apply ad_list_not_stutters_card_conv. Rewrite ad_list_of_dom_card. Apply sym_eq.
Rewrite (MapCard_Dom A m). Apply MapCard_ext. Exact (Elems_of_list_of_dom m).
Qed.
End ListOfDomDef.
Lemma ad_list_of_dom_Dom_1 : (A:Set)
(m:(Map A)) (pf:ad->ad)
(MapFold1 A (list ad) (nil ad) (app 1!ad)
[a:ad][_:A](cons a (nil ad)) pf m)=
(MapFold1 unit (list ad) (nil ad) (app 1!ad)
[a:ad][_:unit](cons a (nil ad)) pf (MapDom A m)).
Proof.
Induction m; Try Trivial. Simpl. Intros. Rewrite (H [a0:ad](pf (ad_double a0))).
Rewrite (H0 [a0:ad](pf (ad_double_plus_un a0))). Reflexivity.
Qed.
Lemma ad_list_of_dom_Dom : (A:Set) (m:(Map A))
(ad_list_of_dom A m)=(ad_list_of_dom unit (MapDom A m)).
Proof.
Intros. Exact (ad_list_of_dom_Dom_1 A m [a0:ad]a0).
Qed.
End MapLists.
|
