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
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
|
(************************************************************************)
(* 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: Maplists.v 8733 2006-04-25 22:52:18Z letouzey $ i*)
Require Import BinNat.
Require Import Ndigits.
Require Import Ndec.
Require Import Map.
Require Import Fset.
Require Import Mapaxioms.
Require Import Mapsubset.
Require Import Mapcard.
Require Import Mapcanon.
Require Import Mapc.
Require Import Bool.
Require Import Sumbool.
Require Import List.
Require Import Arith.
Require Import Mapiter.
Require Import Mapfold.
Section MapLists.
Fixpoint ad_in_list (a:ad) (l:list ad) {struct l} : bool :=
match l with
| nil => false
| a' :: l' => orb (Neqb a a') (ad_in_list a l')
end.
Fixpoint ad_list_stutters (l:list ad) : bool :=
match l with
| nil => false
| a :: l' => orb (ad_in_list a l') (ad_list_stutters l')
end.
Lemma ad_in_list_forms_circuit :
forall (x:ad) (l:list ad),
ad_in_list x l = true ->
{l1 : list ad & {l2 : list ad | l = l1 ++ x :: l2}}.
Proof.
simple induction l. intro. discriminate H.
intros. elim (sumbool_of_bool (Neqb x a)). intro H1. simpl in H0. split with (nil (A:=ad)).
split with l0. rewrite (Neqb_complete _ _ H1). reflexivity.
intro H2. simpl in H0. rewrite H2 in H0. simpl in H0. elim (H H0). intros l'1 H3.
split with (a :: l'1). elim H3. intros l2 H4. split with l2. rewrite H4. reflexivity.
Qed.
Lemma ad_list_stutters_has_circuit :
forall l:list ad,
ad_list_stutters l = true ->
{x : ad &
{l0 : list ad &
{l1 : list ad & {l2 : list ad | l = l0 ++ x :: l1 ++ x :: l2}}}}.
Proof.
simple induction l. intro. discriminate H.
intros. simpl in H0. elim (orb_true_elim _ _ H0). intro H1. split with a.
split with (nil (A:=ad)). simpl in |- *. 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 (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 :=
match l with
| nil => M0 unit
| a :: l' => MapPut _ (Elems l') a tt
end.
Lemma Elems_canon : forall l:list ad, mapcanon _ (Elems l).
Proof.
simple induction l. exact (M0_canon unit).
intros. simpl in |- *. apply MapPut_canon. assumption.
Qed.
Lemma Elems_app :
forall l l':list ad, Elems (l ++ l') = FSetUnion (Elems l) (Elems l').
Proof.
simple induction l. trivial.
intros. simpl in |- *. rewrite (MapPut_as_Merge_c unit (Elems l0)).
rewrite (MapPut_as_Merge_c unit (Elems (l0 ++ l'))).
change
(FSetUnion (Elems (l0 ++ l')) (M1 unit a tt) =
FSetUnion (FSetUnion (Elems l0) (M1 unit a tt)) (Elems l'))
in |- *.
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 : forall l:list ad, Elems (rev l) = Elems l.
Proof.
simple induction l. trivial.
intros. simpl in |- *. rewrite Elems_app. simpl in |- *. rewrite (MapPut_as_Merge_c unit (Elems l0)).
rewrite H. reflexivity.
apply Elems_canon.
Qed.
Lemma ad_in_elems_in_list :
forall (l:list ad) (a:ad), in_FSet a (Elems l) = ad_in_list a l.
Proof.
simple induction l. trivial.
simpl in |- *. unfold in_FSet in |- *. intros. rewrite (in_dom_put _ (Elems l0) a tt a0).
rewrite (H a0). reflexivity.
Qed.
Lemma ad_list_not_stutters_card :
forall l:list ad,
ad_list_stutters l = false -> length l = MapCard _ (Elems l).
Proof.
simple induction l. trivial.
simpl in |- *. 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 : forall l:list ad, MapCard _ (Elems l) <= length l.
Proof.
simple induction l. trivial.
intros. simpl in |- *. apply le_trans with (m := S (MapCard _ (Elems l0))). apply MapCard_Put_ub.
apply le_n_S. assumption.
Qed.
Lemma ad_list_stutters_card :
forall l:list ad,
ad_list_stutters l = true -> MapCard _ (Elems l) < length l.
Proof.
simple induction l. intro. discriminate H.
intros. simpl in |- *. 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 :
forall 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 (MapCard _ (Elems l) < length l). intro. rewrite H in H1. elim (lt_irrefl _ H1).
exact (ad_list_stutters_card _ H0).
trivial.
Qed.
Lemma ad_list_stutters_card_conv :
forall l:list ad,
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_irrefl _ H).
Qed.
Lemma ad_in_list_l :
forall (l l':list ad) (a:ad),
ad_in_list a l = true -> ad_in_list a (l ++ l') = true.
Proof.
simple induction l. intros. discriminate H.
intros. simpl in |- *. 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 :
forall l l':list ad,
ad_list_stutters l = true -> ad_list_stutters (l ++ l') = true.
Proof.
simple induction l. intros. discriminate H.
intros. simpl in |- *. 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 :
forall (l l':list ad) (a:ad),
ad_in_list a l' = true -> ad_in_list a (l ++ l') = true.
Proof.
simple induction l. trivial.
intros. simpl in |- *. rewrite (H l' a0 H0). apply orb_b_true.
Qed.
Lemma ad_list_stutters_app_r :
forall l l':list ad,
ad_list_stutters l' = true -> ad_list_stutters (l ++ l') = true.
Proof.
simple induction l. trivial.
intros. simpl in |- *. rewrite (H l' H0). apply orb_b_true.
Qed.
Lemma ad_list_stutters_app_conv_l :
forall l l':list ad,
ad_list_stutters (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 :
forall l l':list ad,
ad_list_stutters (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 :
forall (l l':list ad) (x:ad), ad_in_list x (l ++ x :: l') = true.
Proof.
simple induction l. simpl in |- *. intros. rewrite (Neqb_correct x). reflexivity.
intros. simpl in |- *. rewrite (H l' x). apply orb_b_true.
Qed.
Lemma ad_in_list_app :
forall (l l':list ad) (x:ad),
ad_in_list x (l ++ l') = orb (ad_in_list x l) (ad_in_list x l').
Proof.
simple induction l. trivial.
intros. simpl in |- *. rewrite <- orb_assoc. rewrite (H l' x). reflexivity.
Qed.
Lemma ad_in_list_rev :
forall (l:list ad) (x:ad), ad_in_list x (rev l) = ad_in_list x l.
Proof.
simple induction l. trivial.
intros. simpl in |- *. rewrite ad_in_list_app. rewrite (H x). simpl in |- *. rewrite orb_b_false.
apply orb_comm.
Qed.
Lemma ad_list_has_circuit_stutters :
forall (l0 l1 l2:list ad) (x:ad),
ad_list_stutters (l0 ++ x :: l1 ++ x :: l2) = true.
Proof.
simple induction l0. simpl in |- *. intros. rewrite (ad_in_list_app_1 l1 l2 x). reflexivity.
intros. simpl in |- *. rewrite (H l1 l2 x). apply orb_b_true.
Qed.
Lemma ad_list_stutters_prev_l :
forall (l l':list ad) (x:ad),
ad_in_list x l = true -> ad_list_stutters (l ++ 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 in |- *. apply ad_list_has_circuit_stutters.
Qed.
Lemma ad_list_stutters_prev_conv_l :
forall (l l':list ad) (x:ad),
ad_list_stutters (l ++ 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 :
forall (l l':list ad) (x:ad),
ad_in_list x l' = true -> ad_list_stutters (l ++ 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 :
forall (l l':list ad) (x:ad),
ad_list_stutters (l ++ 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 :
forall 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 :
forall l l':list ad, length (l ++ l') = length l + length l'.
Proof.
simple induction l. trivial.
intros. simpl in |- *. rewrite (H l'). reflexivity.
Qed.
Lemma ad_list_stutters_permute :
forall l l':list ad,
ad_list_stutters (l ++ l') = ad_list_stutters (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_comm.
Qed.
Lemma ad_list_rev_length : forall l:list ad, length (rev l) = length l.
Proof.
simple induction l. trivial.
intros. simpl in |- *. rewrite ad_list_app_length. simpl in |- *. rewrite H. rewrite <- plus_Snm_nSm.
rewrite <- plus_n_O. reflexivity.
Qed.
Lemma ad_list_stutters_rev :
forall 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 :
forall (l l':list ad) (x:ad), rev l ++ x :: l' = rev (x :: l) ++ l'.
Proof.
simple induction l. trivial.
intros. simpl in |- *. rewrite (app_ass (rev l0) (a :: nil) (x :: l')). simpl in |- *.
rewrite (H (x :: l') a). simpl in |- *.
rewrite (app_ass (rev l0) (a :: nil) (x :: nil)). simpl in |- *.
rewrite app_ass. simpl in |- *. rewrite app_ass. reflexivity.
Qed.
Section ListOfDomDef.
Variable A : Set.
Definition ad_list_of_dom :=
MapFold A (list ad) nil (app (A:=ad)) (fun (a:ad) (_:A) => a :: nil).
Lemma ad_in_list_of_dom_in_dom :
forall (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 in |- *. intros.
rewrite
(MapFold_distr_l A (list ad) nil (app (A:=ad)) bool false orb ad
(fun (a:ad) (l:list ad) => ad_in_list a l) (
fun c:ad => refl_equal _) ad_in_list_app
(fun (a0:ad) (_:A) => a0 :: nil) m a).
simpl in |- *. rewrite (MapFold_orb A (fun (a0:ad) (_:A) => orb (Neqb a a0) false) m).
elim
(option_sum _
(MapSweep A (fun (a0:ad) (_:A) => orb (Neqb a a0) false) m)). intro H. elim H.
intro r. elim r. intros a0 y H0. rewrite H0. unfold in_dom in |- *.
elim (orb_prop _ _ (MapSweep_semantics_1 _ _ _ _ _ H0)). intro H1.
rewrite (Neqb_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 (Neqb_correct a) in H2. discriminate H2.
exact (sym_eq (y:=_)).
Qed.
Lemma Elems_of_list_of_dom :
forall m:Map A, eqmap unit (Elems (ad_list_of_dom m)) (MapDom A m).
Proof.
unfold eqmap, eqm in |- *. 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 :
forall 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 :
forall (m:Map A) (pf:ad -> ad),
length
(MapFold1 A (list ad) nil (app (A:=ad)) (fun (a:ad) (_:A) => a :: nil)
pf m) = MapCard A m.
Proof.
simple induction m; try trivial. simpl in |- *. intros. rewrite ad_list_app_length.
rewrite (H (fun a0:ad => pf (Ndouble a0))). rewrite (H0 (fun a0:ad => pf (Ndouble_plus_one a0))).
reflexivity.
Qed.
Lemma ad_list_of_dom_card :
forall m:Map A, length (ad_list_of_dom m) = MapCard A m.
Proof.
exact (fun m:Map A => ad_list_of_dom_card_1 m (fun a:ad => a)).
Qed.
Lemma ad_list_of_dom_not_stutters :
forall 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 :
forall (A:Set) (m:Map A) (pf:ad -> ad),
MapFold1 A (list ad) nil (app (A:=ad)) (fun (a:ad) (_:A) => a :: nil) pf
m =
MapFold1 unit (list ad) nil (app (A:=ad))
(fun (a:ad) (_:unit) => a :: nil) pf (MapDom A m).
Proof.
simple induction m; try trivial. simpl in |- *. intros. rewrite (H (fun a0:ad => pf (Ndouble a0))).
rewrite (H0 (fun a0:ad => pf (Ndouble_plus_one a0))). reflexivity.
Qed.
Lemma ad_list_of_dom_Dom :
forall (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 (fun a0:ad => a0)).
Qed.
End MapLists.
|
