summaryrefslogtreecommitdiff
path: root/theories/FSets/FMapFullAVL.v
blob: 57cbbcc4ce0ec32aa45aec62dc27e93835e7a915 (plain)
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
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823

(***********************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
(*   \VV/  *************************************************************)
(*    //   *      This file is distributed under the terms of the      *)
(*         *       GNU Lesser General Public License Version 2.1       *)
(***********************************************************************)

(* Finite map library.  *)

(* $Id: FMapFullAVL.v 10748 2008-04-03 18:28:26Z letouzey $ *)

(** * FMapFullAVL
   
   This file contains some complements to [FMapAVL].

   - Functor [AvlProofs] proves that trees of [FMapAVL] are not only 
   binary search trees, but moreover well-balanced ones. This is done
   by proving that all operations preserve the balancing.
  
   - We then pack the previous elements in a [IntMake] functor 
   similar to the one of [FMapAVL], but richer.

   - In final [IntMake_ord] functor, the [compare] function is 
   different from the one in [FMapAVL]: this non-structural 
   version is closer to the original Ocaml code.

*)

Require Import Recdef FMapInterface FMapList ZArith Int FMapAVL.

Set Implicit Arguments.
Unset Strict Implicit.

Module AvlProofs (Import I:Int)(X: OrderedType).
Module Import Raw := Raw I X.
Module Import II:=MoreInt(I).
Import Raw.Proofs.
Open Local Scope pair_scope.
Open Local Scope Int_scope.

Section Elt.
Variable elt : Type.
Implicit Types m r : t elt.

(** * AVL trees *)

(** [avl s] : [s] is a properly balanced AVL tree,
    i.e. for any node the heights of the two children
    differ by at most 2 *)

Inductive avl : t elt -> Prop :=
  | RBLeaf : avl (Leaf _)
  | RBNode : forall x e l r h, 
      avl l ->
      avl r ->
      -(2) <= height l - height r <= 2 ->
      h = max (height l) (height r) + 1 -> 
      avl (Node l x e r h).


(** * Automation and dedicated tactics about [avl]. *)

Hint Constructors avl.

Lemma height_non_negative : forall (s : t elt), avl s -> 
 height s >= 0.
Proof.
 induction s; simpl; intros; auto with zarith.
 inv avl; intuition; omega_max.
Qed.

Ltac avl_nn_hyp H := 
     let nz := fresh "nz" in assert (nz := height_non_negative H).

Ltac avl_nn h := 
  let t := type of h in 
  match type of t with 
   | Prop => avl_nn_hyp h
   | _ => match goal with H : avl h |- _ => avl_nn_hyp H end
  end.

(* Repeat the previous tactic. 
   Drawback: need to clear the [avl _] hyps ... Thank you Ltac *)

Ltac avl_nns :=
  match goal with 
     | H:avl _ |- _ => avl_nn_hyp H; clear H; avl_nns
     | _ => idtac
  end.


(** * Basic results about [avl], [height] *)

Lemma avl_node : forall x e l r, avl l -> avl r ->
 -(2) <= height l - height r <= 2 ->
 avl (Node l x e r (max (height l) (height r) + 1)).
Proof.
  intros; auto.
Qed.
Hint Resolve avl_node.

(** Results about [height] *)

Lemma height_0 : forall l, avl l -> height l = 0 -> 
 l = Leaf _.
Proof.
 destruct 1; intuition; simpl in *.
 avl_nns; simpl in *; elimtype False; omega_max.
Qed.


(** * Empty map *)

Lemma empty_avl : avl (empty elt).
Proof. 
 unfold empty; auto.
Qed.


(** * Helper functions *)

Lemma create_avl : 
 forall l x e r, avl l -> avl r ->  -(2) <= height l - height r <= 2 -> 
 avl (create l x e r).
Proof.
 unfold create; auto.
Qed.

Lemma create_height : 
 forall l x e r, avl l -> avl r ->  -(2) <= height l - height r <= 2 -> 
 height (create l x e r) = max (height l) (height r) + 1.
Proof.
 unfold create; intros; auto.
Qed.

Lemma bal_avl : forall l x e r, avl l -> avl r -> 
 -(3) <= height l - height r <= 3 -> avl (bal l x e r).
Proof.
 intros l x e r; functional induction (bal l x e r); intros; clearf;
 inv avl; simpl in *; 
 match goal with |- avl (assert_false _ _ _ _) => avl_nns
  | _ => repeat apply create_avl; simpl in *; auto
 end; omega_max.
Qed.

Lemma bal_height_1 : forall l x e r, avl l -> avl r -> 
 -(3) <= height l - height r <= 3 ->
 0 <= height (bal l x e r) - max (height l) (height r) <= 1.
Proof.
 intros l x e r; functional induction (bal l x e r); intros; clearf;
 inv avl; avl_nns; simpl in *; omega_max.
Qed.

Lemma bal_height_2 : 
 forall l x e r, avl l -> avl r -> -(2) <= height l - height r <= 2 -> 
 height (bal l x e r) == max (height l) (height r) +1.
Proof.
 intros l x e r; functional induction (bal l x e r); intros; clearf;
 inv avl; avl_nns; simpl in *; omega_max.
Qed.

Ltac omega_bal := match goal with 
  | H:avl ?l, H':avl ?r |- context [ bal ?l ?x ?e ?r ] => 
     generalize (bal_height_1 x e H H') (bal_height_2 x e H H'); 
     omega_max
  end.

(** * Insertion *)

Lemma add_avl_1 :  forall m x e, avl m -> 
 avl (add x e m) /\ 0 <= height (add x e m) - height m <= 1.
Proof. 
 intros m x e; functional induction (add x e m); intros; inv avl; simpl in *.
 intuition; try constructor; simpl; auto; try omega_max.
 (* LT *)
 destruct IHt; auto.
 split.
 apply bal_avl; auto; omega_max.
 omega_bal.
 (* EQ *)
 intuition; omega_max.
 (* GT *)
 destruct IHt; auto.
 split.
 apply bal_avl; auto; omega_max.
 omega_bal.
Qed.

Lemma add_avl : forall m x e, avl m -> avl (add x e m).
Proof.
 intros; generalize (add_avl_1 x e H); intuition.
Qed.
Hint Resolve add_avl.

(** * Extraction of minimum binding *)

Lemma remove_min_avl_1 : forall l x e r h, avl (Node l x e r h) -> 
 avl (remove_min l x e r)#1 /\ 
 0 <= height (Node l x e r h) - height (remove_min l x e r)#1 <= 1.
Proof.
 intros l x e r; functional induction (remove_min l x e r); simpl in *; intros.
 inv avl; simpl in *; split; auto.
 avl_nns; omega_max.
 inversion_clear H.
 rewrite e0 in IHp;simpl in IHp;destruct (IHp _x); auto.
 split; simpl in *.
 apply bal_avl; auto; omega_max.
 omega_bal.
Qed.

Lemma remove_min_avl : forall l x e r h, avl (Node l x e r h) -> 
    avl (remove_min l x e r)#1. 
Proof.
 intros; generalize (remove_min_avl_1 H); intuition.
Qed.

(** * Merging two trees *)

Lemma merge_avl_1 : forall m1 m2, avl m1 -> avl m2 -> 
 -(2) <= height m1 - height m2 <= 2 -> 
 avl (merge m1 m2) /\ 
 0<= height (merge m1 m2) - max (height m1) (height m2) <=1.
Proof.
 intros m1 m2; functional induction (merge m1 m2); intros; 
 try factornode _x _x0 _x1 _x2 _x3 as m1.
 simpl; split; auto; avl_nns; omega_max.
 simpl; split; auto; avl_nns; omega_max.
 generalize (remove_min_avl_1 H0).
 rewrite e1; destruct 1.
 split.
 apply bal_avl; auto.
 omega_max.
 omega_bal.
Qed.

Lemma merge_avl : forall m1 m2, avl m1 -> avl m2 -> 
  -(2) <= height m1 - height m2 <= 2 -> avl (merge m1 m2).
Proof. 
 intros; generalize (merge_avl_1 H H0 H1); intuition.
Qed.


(** * Deletion *)

Lemma remove_avl_1 : forall m x, avl m -> 
 avl (remove x m) /\ 0 <= height m - height (remove x m) <= 1.
Proof.
 intros m x; functional induction (remove x m); intros.
 split; auto; omega_max.
 (* LT *)
 inv avl.
 destruct (IHt H0).
 split. 
 apply bal_avl; auto.
 omega_max.
 omega_bal.
 (* EQ *)
 inv avl. 
 generalize (merge_avl_1 H0 H1 H2).
 intuition omega_max.
 (* GT *)
 inv avl.
 destruct (IHt H1).
 split. 
 apply bal_avl; auto.
 omega_max.
 omega_bal.
Qed.

Lemma remove_avl : forall m x, avl m -> avl (remove x m).
Proof. 
 intros; generalize (remove_avl_1 x H); intuition.
Qed.
Hint Resolve remove_avl.


(** * Join *)

Lemma join_avl_1 : forall l x d r, avl l -> avl r -> 
 avl (join l x d r) /\
 0<= height (join l x d r) - max (height l) (height r) <= 1.
Proof.
 join_tac.

 split; simpl; auto.
 destruct (add_avl_1 x d H0).
 avl_nns; omega_max.
 set (l:=Node ll lx ld lr lh) in *.
 split; auto.
 destruct (add_avl_1 x d H).
 simpl (height (Leaf elt)).
 avl_nns; omega_max.

 inversion_clear H.
 assert (height (Node rl rx rd rr rh) = rh); auto.
 set (r := Node rl rx rd rr rh) in *; clearbody r.
 destruct (Hlr x d r H2 H0); clear Hrl Hlr.
 set (j := join lr x d r) in *; clearbody j.
 simpl.
 assert (-(3) <= height ll - height j <= 3) by omega_max.
 split.
 apply bal_avl; auto.
 omega_bal.

 inversion_clear H0.
 assert (height (Node ll lx ld lr lh) = lh); auto.
 set (l := Node ll lx ld lr lh) in *; clearbody l.
 destruct (Hrl H H1); clear Hrl Hlr.
 set (j := join l x d rl) in *; clearbody j.
 simpl.
 assert (-(3) <= height j - height rr <= 3) by omega_max.
 split.
 apply bal_avl; auto.
 omega_bal.

 clear Hrl Hlr.
 assert (height (Node ll lx ld lr lh) = lh); auto.
 assert (height (Node rl rx rd rr rh) = rh); auto.
 set (l := Node ll lx ld lr lh) in *; clearbody l.
 set (r := Node rl rx rd rr rh) in *; clearbody r.
 assert (-(2) <= height l - height r <= 2) by omega_max.
 split.
 apply create_avl; auto.
 rewrite create_height; auto; omega_max.
Qed.

Lemma join_avl : forall l x d r, avl l -> avl r -> avl (join l x d r).
Proof.
 intros; destruct (join_avl_1 x d H H0); auto.
Qed.
Hint Resolve join_avl.

(** concat *)

Lemma concat_avl : forall m1 m2, avl m1 -> avl m2 -> avl (concat m1 m2).
Proof.
 intros m1 m2; functional induction (concat m1 m2); auto.
 intros; apply join_avl; auto.
 generalize (remove_min_avl H0); rewrite e1; simpl; auto.
Qed.
Hint Resolve concat_avl.

(** split *)

Lemma split_avl : forall m x, avl m -> 
  avl (split x m)#l /\ avl (split x m)#r.
Proof. 
 intros m x; functional induction (split x m); simpl; auto.
 rewrite e1 in IHt;simpl in IHt;inversion_clear 1; intuition.
 simpl; inversion_clear 1; auto.
 rewrite e1 in IHt;simpl in IHt;inversion_clear 1; intuition.
Qed.

End Elt.
Hint Constructors avl.

Section Map. 
Variable elt elt' : Type.
Variable f : elt -> elt'. 

Lemma map_height : forall m, height (map f m) = height m.
Proof. 
destruct m; simpl; auto.
Qed.

Lemma map_avl : forall m, avl m -> avl (map f m).
Proof.
induction m; simpl; auto.
inversion_clear 1; constructor; auto; do 2 rewrite map_height; auto.
Qed.

End Map.

Section Mapi.
Variable elt elt' : Type.
Variable f : key -> elt -> elt'. 

Lemma mapi_height : forall m, height (mapi f m) = height m.
Proof. 
destruct m; simpl; auto.
Qed.

Lemma mapi_avl : forall m, avl m -> avl (mapi f m).
Proof.
induction m; simpl; auto.
inversion_clear 1; constructor; auto; do 2 rewrite mapi_height; auto.
Qed.

End Mapi.

Section Map_option. 
Variable elt elt' : Type.
Variable f : key -> elt -> option elt'.

Lemma map_option_avl : forall m, avl m -> avl (map_option f m).
Proof.
induction m; simpl; auto; intros.
inv avl; destruct (f k e); auto using join_avl, concat_avl.
Qed.

End Map_option.

Section Map2_opt.
Variable elt elt' elt'' : Type.
Variable f : key -> elt -> option elt' -> option elt''.
Variable mapl : t elt -> t elt''.
Variable mapr : t elt' -> t elt''.
Hypothesis mapl_avl : forall m, avl m -> avl (mapl m).
Hypothesis mapr_avl : forall m', avl m' -> avl (mapr m').

Notation map2_opt := (map2_opt f mapl mapr).

Lemma map2_opt_avl : forall m1 m2, avl m1 -> avl m2 -> 
 avl (map2_opt m1 m2).
Proof.
intros m1 m2; functional induction (map2_opt m1 m2); auto; 
factornode _x0 _x1 _x2 _x3 _x4 as r2; intros; 
destruct (split_avl x1 H0); rewrite e1 in *; simpl in *; inv avl; 
auto using join_avl, concat_avl.
Qed.

End Map2_opt.

Section Map2.
Variable elt elt' elt'' : Type.
Variable f : option elt -> option elt' -> option elt''.

Lemma map2_avl : forall m1 m2, avl m1 -> avl m2 -> avl (map2 f m1 m2).
Proof.
unfold map2; auto using map2_opt_avl, map_option_avl.
Qed.

End Map2.
End AvlProofs.

(** * Encapsulation

   We can implement [S] with balanced binary search trees. 
   When compared to [FMapAVL], we maintain here two invariants
   (bst and avl) instead of only bst, which is enough for fulfilling
   the FMap interface.
*) 

Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.

 Module E := X.
 Module Import AvlProofs := AvlProofs I X.
 Import Raw.
 Import Raw.Proofs.

 Record bbst (elt:Type) := 
  Bbst {this :> tree elt; is_bst : bst this; is_avl: avl this}.
 
 Definition t := bbst.
 Definition key := E.t.
 
 Section Elt.
 Variable elt elt' elt'': Type.

 Implicit Types m : t elt.
 Implicit Types x y : key. 
 Implicit Types e : elt. 

 Definition empty : t elt := Bbst (empty_bst elt) (empty_avl elt).
 Definition is_empty m : bool := is_empty m.(this).
 Definition add x e m : t elt := 
  Bbst (add_bst x e m.(is_bst)) (add_avl x e m.(is_avl)).
 Definition remove x m : t elt := 
  Bbst (remove_bst x m.(is_bst)) (remove_avl x m.(is_avl)).
 Definition mem x m : bool := mem x m.(this).
 Definition find x m : option elt := find x m.(this).
 Definition map f m : t elt' := 
  Bbst (map_bst f m.(is_bst)) (map_avl f m.(is_avl)).
 Definition mapi (f:key->elt->elt') m : t elt' := 
  Bbst (mapi_bst f m.(is_bst)) (mapi_avl f m.(is_avl)).
 Definition map2 f m (m':t elt') : t elt'' := 
  Bbst (map2_bst f m.(is_bst) m'.(is_bst)) (map2_avl f m.(is_avl) m'.(is_avl)).
 Definition elements m : list (key*elt) := elements m.(this).
 Definition cardinal m := cardinal m.(this).
 Definition fold (A:Type) (f:key->elt->A->A) m i := fold (A:=A) f m.(this) i.
 Definition equal cmp m m' : bool := equal cmp m.(this) m'.(this).

 Definition MapsTo x e m : Prop := MapsTo x e m.(this).
 Definition In x m : Prop := In0 x m.(this).
 Definition Empty m : Prop := Empty m.(this).

 Definition eq_key : (key*elt) -> (key*elt) -> Prop := @PX.eqk elt.
 Definition eq_key_elt : (key*elt) -> (key*elt) -> Prop := @PX.eqke elt.
 Definition lt_key : (key*elt) -> (key*elt) -> Prop := @PX.ltk elt.

 Lemma MapsTo_1 : forall m x y e, E.eq x y -> MapsTo x e m -> MapsTo y e m.
 Proof. intros m; exact (@MapsTo_1 _ m.(this)). Qed.
 
 Lemma mem_1 : forall m x, In x m -> mem x m = true.
 Proof.
 unfold In, mem; intros m x; rewrite In_alt; simpl; apply mem_1; auto.
 apply m.(is_bst).
 Qed.
 
 Lemma mem_2 : forall m x, mem x m = true -> In x m. 
 Proof.
 unfold In, mem; intros m x; rewrite In_alt; simpl; apply mem_2; auto.
 Qed.

 Lemma empty_1 : Empty empty.
 Proof. exact (@empty_1 elt). Qed.

 Lemma is_empty_1 : forall m, Empty m -> is_empty m = true.
 Proof. intros m; exact (@is_empty_1 _ m.(this)). Qed.
 Lemma is_empty_2 : forall m, is_empty m = true -> Empty m.
 Proof. intros m; exact (@is_empty_2 _ m.(this)). Qed.

 Lemma add_1 : forall m x y e, E.eq x y -> MapsTo y e (add x e m).
 Proof. intros m x y e; exact (@add_1 elt _ x y e). Qed.
 Lemma add_2 : forall m x y e e', ~ E.eq x y -> MapsTo y e m -> MapsTo y e (add x e' m).
 Proof. intros m x y e e'; exact (@add_2 elt _ x y e e'). Qed.
 Lemma add_3 : forall m x y e e', ~ E.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m.
 Proof. intros m x y e e'; exact (@add_3 elt _ x y e e'). Qed.

 Lemma remove_1 : forall m x y, E.eq x y -> ~ In y (remove x m).
 Proof.
 unfold In, remove; intros m x y; rewrite In_alt; simpl; apply remove_1; auto.
 apply m.(is_bst).
 Qed.
 Lemma remove_2 : forall m x y e, ~ E.eq x y -> MapsTo y e m -> MapsTo y e (remove x m).
 Proof. intros m x y e; exact (@remove_2 elt _ x y e m.(is_bst)). Qed.
 Lemma remove_3 : forall m x y e, MapsTo y e (remove x m) -> MapsTo y e m.
 Proof. intros m x y e; exact (@remove_3 elt _ x y e m.(is_bst)). Qed.


 Lemma find_1 : forall m x e, MapsTo x e m -> find x m = Some e. 
 Proof. intros m x e; exact (@find_1 elt _ x e m.(is_bst)). Qed.
 Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m.
 Proof. intros m; exact (@find_2 elt m.(this)). Qed.

 Lemma fold_1 : forall m (A : Type) (i : A) (f : key -> elt -> A -> A),
        fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
 Proof. intros m; exact (@fold_1 elt m.(this) m.(is_bst)). Qed.

 Lemma elements_1 : forall m x e,       
   MapsTo x e m -> InA eq_key_elt (x,e) (elements m).
 Proof.
 intros; unfold elements, MapsTo, eq_key_elt; rewrite elements_mapsto; auto.
 Qed.

 Lemma elements_2 : forall m x e,   
   InA eq_key_elt (x,e) (elements m) -> MapsTo x e m.
 Proof.
 intros; unfold elements, MapsTo, eq_key_elt; rewrite <- elements_mapsto; auto.
 Qed.

 Lemma elements_3 : forall m, sort lt_key (elements m).  
 Proof. intros m; exact (@elements_sort elt m.(this) m.(is_bst)). Qed.

 Lemma elements_3w : forall m, NoDupA eq_key (elements m).  
 Proof. intros m; exact (@elements_nodup elt m.(this) m.(is_bst)). Qed.

 Lemma cardinal_1 : forall m, cardinal m = length (elements m).
 Proof. intro m; exact (@elements_cardinal elt m.(this)). Qed.

 Definition Equal m m' := forall y, find y m = find y m'.
 Definition Equiv (eq_elt:elt->elt->Prop) m m' := 
   (forall k, In k m <-> In k m') /\ 
   (forall k e e', MapsTo k e m -> MapsTo k e' m' -> eq_elt e e').
 Definition Equivb cmp := Equiv (Cmp cmp).

 Lemma Equivb_Equivb : forall cmp m m', 
  Equivb cmp m m' <-> Raw.Proofs.Equivb cmp m m'.
 Proof. 
 intros; unfold Equivb, Equiv, Raw.Proofs.Equivb, In; intuition.
 generalize (H0 k); do 2 rewrite In_alt; intuition.
 generalize (H0 k); do 2 rewrite In_alt; intuition.
 generalize (H0 k); do 2 rewrite <- In_alt; intuition.
 generalize (H0 k); do 2 rewrite <- In_alt; intuition.
 Qed.

 Lemma equal_1 : forall m m' cmp, 
   Equivb cmp m m' -> equal cmp m m' = true. 
 Proof. 
 unfold equal; intros (m,b,a) (m',b',a') cmp; rewrite Equivb_Equivb; 
  intros; simpl in *; rewrite equal_Equivb; auto.
 Qed. 

 Lemma equal_2 : forall m m' cmp, 
   equal cmp m m' = true -> Equivb cmp m m'.
 Proof. 
 unfold equal; intros (m,b,a) (m',b',a') cmp; rewrite Equivb_Equivb; 
  intros; simpl in *; rewrite <-equal_Equivb; auto.
 Qed.

 End Elt.

 Lemma map_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)(f:elt->elt'), 
        MapsTo x e m -> MapsTo x (f e) (map f m).
 Proof. intros elt elt' m x e f; exact (@map_1 elt elt' f m.(this) x e). Qed.

 Lemma map_2 : forall (elt elt':Type)(m:t elt)(x:key)(f:elt->elt'), In x (map f m) -> In x m.
 Proof.
 intros elt elt' m x f; do 2 unfold In in *; do 2 rewrite In_alt; simpl.
 apply map_2; auto.
 Qed. 

 Lemma mapi_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)
        (f:key->elt->elt'), MapsTo x e m -> 
        exists y, E.eq y x /\ MapsTo x (f y e) (mapi f m).
 Proof. intros elt elt' m x e f; exact (@mapi_1 elt elt' f m.(this) x e). Qed.
 Lemma mapi_2 : forall (elt elt':Type)(m: t elt)(x:key)
        (f:key->elt->elt'), In x (mapi f m) -> In x m.
 Proof.
 intros elt elt' m x f; unfold In in *; do 2 rewrite In_alt; simpl; apply mapi_2; auto.
 Qed.

 Lemma map2_1 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt')
    (x:key)(f:option elt->option elt'->option elt''), 
    In x m \/ In x m' -> 
    find x (map2 f m m') = f (find x m) (find x m'). 
 Proof. 
 unfold find, map2, In; intros elt elt' elt'' m m' x f.
 do 2 rewrite In_alt; intros; simpl; apply map2_1; auto.
 apply m.(is_bst).
 apply m'.(is_bst).
 Qed.

 Lemma map2_2 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt')
     (x:key)(f:option elt->option elt'->option elt''), 
     In x (map2 f m m') -> In x m \/ In x m'.
 Proof. 
 unfold In, map2; intros elt elt' elt'' m m' x f.
 do 3 rewrite In_alt; intros; simpl in *; eapply map2_2; eauto.
 apply m.(is_bst).
 apply m'.(is_bst).
 Qed.

End IntMake.


Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: 
    Sord with Module Data := D 
            with Module MapS.E := X.

  Module Data := D.
  Module Import MapS := IntMake(I)(X). 
  Import AvlProofs.
  Import Raw.Proofs.
  Module Import MD := OrderedTypeFacts(D).
  Module LO := FMapList.Make_ord(X)(D).

  Definition t := MapS.t D.t. 

  Definition cmp e e' := 
   match D.compare e e' with EQ _ => true | _ => false end.

  Definition elements (m:t) := 
    LO.MapS.Build_slist (Raw.Proofs.elements_sort m.(is_bst)).

  (** * As comparison function, we propose here a non-structural 
    version faithful to the code of Ocaml's Map library, instead of 
    the structural version of FMapAVL *)

  Fixpoint cardinal_e (e:Raw.enumeration D.t) := 
    match e with 
     | Raw.End => 0%nat
     | Raw.More _ _ r e => S (Raw.cardinal r + cardinal_e e)
    end.

  Lemma cons_cardinal_e : forall m e, 
   cardinal_e (Raw.cons m e) = (Raw.cardinal m + cardinal_e e)%nat.
  Proof.
   induction m; simpl; intros; auto.
   rewrite IHm1; simpl; rewrite <- plus_n_Sm; auto with arith.
  Qed.

  Definition cardinal_e_2 ee := 
   (cardinal_e (fst ee) + cardinal_e (snd ee))%nat.

  Function compare_aux (ee:Raw.enumeration D.t * Raw.enumeration D.t) 
   { measure cardinal_e_2 ee } : comparison := 
  match ee with 
  | (Raw.End, Raw.End) => Eq
  | (Raw.End, Raw.More _ _ _ _) => Lt
  | (Raw.More _ _ _ _, Raw.End) => Gt
  | (Raw.More x1 d1 r1 e1, Raw.More x2 d2 r2 e2) =>
      match X.compare x1 x2 with
      | EQ _ => match D.compare d1 d2 with 
                | EQ _ => compare_aux (Raw.cons r1 e1, Raw.cons r2 e2)
                | LT _ => Lt
                | GT _ => Gt
                end
      | LT _ => Lt
      | GT _ => Gt
      end
  end.
  Proof.
  intros; unfold cardinal_e_2; simpl; 
  abstract (do 2 rewrite cons_cardinal_e; romega with * ).
  Defined.
  
  Definition Cmp c :=
   match c with
    | Eq => LO.eq_list
    | Lt => LO.lt_list
    | Gt => (fun l1 l2 => LO.lt_list l2 l1)
   end.

  Lemma cons_Cmp : forall c x1 x2 d1 d2 l1 l2, 
   X.eq x1 x2 -> D.eq d1 d2 ->
   Cmp c l1 l2 -> Cmp c ((x1,d1)::l1) ((x2,d2)::l2).
  Proof.
   destruct c; simpl; intros; MX.elim_comp; auto.
  Qed.
  Hint Resolve cons_Cmp.

  Lemma compare_aux_Cmp : forall e, 
   Cmp (compare_aux e) (flatten_e (fst e)) (flatten_e (snd e)).
  Proof.
  intros e; functional induction (compare_aux e); simpl in *; 
   auto; intros; try clear e0; try clear e3; try MX.elim_comp; auto.
  rewrite 2 cons_1 in IHc; auto.
  Qed.

  Lemma compare_Cmp : forall m1 m2, 
    Cmp (compare_aux (Raw.cons m1 (Raw.End _), Raw.cons m2 (Raw.End _))) 
     (Raw.elements m1) (Raw.elements m2).
  Proof.
  intros. 
  assert (H1:=cons_1 m1 (Raw.End _)).
  assert (H2:=cons_1 m2 (Raw.End _)).
  simpl in *; rewrite <- app_nil_end in *; rewrite <-H1,<-H2.
  apply (@compare_aux_Cmp (Raw.cons m1 (Raw.End _), 
                           Raw.cons m2 (Raw.End _))).
  Qed.

  Definition eq (m1 m2 : t) := LO.eq_list (Raw.elements m1) (Raw.elements m2).
  Definition lt (m1 m2 : t) := LO.lt_list (Raw.elements m1) (Raw.elements m2).

  Definition compare (s s':t) : Compare lt eq s s'.
  Proof.
   intros (s,b,a) (s',b',a').
   generalize (compare_Cmp s s').
   destruct compare_aux; intros; [apply EQ|apply LT|apply GT]; red; auto.
  Defined.

    
  (* Proofs about [eq] and [lt] *)

  Definition selements (m1 : t) := 
   LO.MapS.Build_slist (elements_sort m1.(is_bst)).

  Definition seq (m1 m2 : t) := LO.eq (selements m1) (selements m2).
  Definition slt (m1 m2 : t) := LO.lt (selements m1) (selements m2).

  Lemma eq_seq : forall m1 m2, eq m1 m2 <-> seq m1 m2.
  Proof.
   unfold eq, seq, selements, elements, LO.eq; intuition.
  Qed.

  Lemma lt_slt : forall m1 m2, lt m1 m2 <-> slt m1 m2.
  Proof.
   unfold lt, slt, selements, elements, LO.lt; intuition.
  Qed.

  Lemma eq_1 : forall (m m' : t), MapS.Equivb cmp m m' -> eq m m'.
  Proof.
  intros m m'.
  rewrite eq_seq; unfold seq.
  rewrite Equivb_Equivb.
  rewrite Equivb_elements.
  auto using LO.eq_1.
  Qed.

  Lemma eq_2 : forall m m', eq m m' -> MapS.Equivb cmp m m'.
  Proof.
  intros m m'.
  rewrite eq_seq; unfold seq.
  rewrite Equivb_Equivb.
  rewrite Equivb_elements.
  intros.
  generalize (LO.eq_2 H).
  auto.
  Qed.

  Lemma eq_refl : forall m : t, eq m m.
  Proof. 
  intros; rewrite eq_seq; unfold seq; intros; apply LO.eq_refl.
  Qed.

  Lemma eq_sym : forall m1 m2 : t, eq m1 m2 -> eq m2 m1.
  Proof.
  intros m1 m2; rewrite 2 eq_seq; unfold seq; intros; apply LO.eq_sym; auto.
  Qed.

  Lemma eq_trans : forall m1 m2 m3 : t, eq m1 m2 -> eq m2 m3 -> eq m1 m3.
  Proof.
  intros m1 m2 M3; rewrite 3 eq_seq; unfold seq.
   intros; eapply LO.eq_trans; eauto.
  Qed.

  Lemma lt_trans : forall m1 m2 m3 : t, lt m1 m2 -> lt m2 m3 -> lt m1 m3.
  Proof.
  intros m1 m2 m3; rewrite 3 lt_slt; unfold slt;  
   intros; eapply LO.lt_trans; eauto.
  Qed.

  Lemma lt_not_eq : forall m1 m2 : t, lt m1 m2 -> ~ eq m1 m2.
  Proof.
  intros m1 m2; rewrite lt_slt, eq_seq; unfold slt, seq; 
   intros; apply LO.lt_not_eq; auto.
  Qed.

End IntMake_ord.

(* For concrete use inside Coq, we propose an instantiation of [Int] by [Z]. *)

Module Make (X: OrderedType) <: S with Module E := X
 :=IntMake(Z_as_Int)(X).

Module Make_ord (X: OrderedType)(D: OrderedType) 
 <: Sord with Module Data := D 
            with Module MapS.E := X
 :=IntMake_ord(Z_as_Int)(X)(D).