2
(***********************************************************************)
3
(* v * The Coq Proof Assistant / The Coq Development Team *)
4
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
5
(* \VV/ *************************************************************)
6
(* // * This file is distributed under the terms of the *)
7
(* * GNU Lesser General Public License Version 2.1 *)
8
(***********************************************************************)
10
(* Finite map library. *)
12
(* $Id: FMapFullAVL.v 10748 2008-04-03 18:28:26Z letouzey $ *)
16
This file contains some complements to [FMapAVL].
18
- Functor [AvlProofs] proves that trees of [FMapAVL] are not only
19
binary search trees, but moreover well-balanced ones. This is done
20
by proving that all operations preserve the balancing.
22
- We then pack the previous elements in a [IntMake] functor
23
similar to the one of [FMapAVL], but richer.
25
- In final [IntMake_ord] functor, the [compare] function is
26
different from the one in [FMapAVL]: this non-structural
27
version is closer to the original Ocaml code.
31
Require Import Recdef FMapInterface FMapList ZArith Int FMapAVL.
33
Set Implicit Arguments.
34
Unset Strict Implicit.
36
Module AvlProofs (Import I:Int)(X: OrderedType).
37
Module Import Raw := Raw I X.
38
Module Import II:=MoreInt(I).
40
Open Local Scope pair_scope.
41
Open Local Scope Int_scope.
45
Implicit Types m r : t elt.
49
(** [avl s] : [s] is a properly balanced AVL tree,
50
i.e. for any node the heights of the two children
51
differ by at most 2 *)
53
Inductive avl : t elt -> Prop :=
54
| RBLeaf : avl (Leaf _)
55
| RBNode : forall x e l r h,
58
-(2) <= height l - height r <= 2 ->
59
h = max (height l) (height r) + 1 ->
63
(** * Automation and dedicated tactics about [avl]. *)
65
Hint Constructors avl.
67
Lemma height_non_negative : forall (s : t elt), avl s ->
70
induction s; simpl; intros; auto with zarith.
71
inv avl; intuition; omega_max.
75
let nz := fresh "nz" in assert (nz := height_non_negative H).
80
| Prop => avl_nn_hyp h
81
| _ => match goal with H : avl h |- _ => avl_nn_hyp H end
84
(* Repeat the previous tactic.
85
Drawback: need to clear the [avl _] hyps ... Thank you Ltac *)
89
| H:avl _ |- _ => avl_nn_hyp H; clear H; avl_nns
94
(** * Basic results about [avl], [height] *)
96
Lemma avl_node : forall x e l r, avl l -> avl r ->
97
-(2) <= height l - height r <= 2 ->
98
avl (Node l x e r (max (height l) (height r) + 1)).
102
Hint Resolve avl_node.
104
(** Results about [height] *)
106
Lemma height_0 : forall l, avl l -> height l = 0 ->
109
destruct 1; intuition; simpl in *.
110
avl_nns; simpl in *; elimtype False; omega_max.
116
Lemma empty_avl : avl (empty elt).
122
(** * Helper functions *)
125
forall l x e r, avl l -> avl r -> -(2) <= height l - height r <= 2 ->
126
avl (create l x e r).
131
Lemma create_height :
132
forall l x e r, avl l -> avl r -> -(2) <= height l - height r <= 2 ->
133
height (create l x e r) = max (height l) (height r) + 1.
135
unfold create; intros; auto.
138
Lemma bal_avl : forall l x e r, avl l -> avl r ->
139
-(3) <= height l - height r <= 3 -> avl (bal l x e r).
141
intros l x e r; functional induction (bal l x e r); intros; clearf;
143
match goal with |- avl (assert_false _ _ _ _) => avl_nns
144
| _ => repeat apply create_avl; simpl in *; auto
148
Lemma bal_height_1 : forall l x e r, avl l -> avl r ->
149
-(3) <= height l - height r <= 3 ->
150
0 <= height (bal l x e r) - max (height l) (height r) <= 1.
152
intros l x e r; functional induction (bal l x e r); intros; clearf;
153
inv avl; avl_nns; simpl in *; omega_max.
157
forall l x e r, avl l -> avl r -> -(2) <= height l - height r <= 2 ->
158
height (bal l x e r) == max (height l) (height r) +1.
160
intros l x e r; functional induction (bal l x e r); intros; clearf;
161
inv avl; avl_nns; simpl in *; omega_max.
164
Ltac omega_bal := match goal with
165
| H:avl ?l, H':avl ?r |- context [ bal ?l ?x ?e ?r ] =>
166
generalize (bal_height_1 x e H H') (bal_height_2 x e H H');
172
Lemma add_avl_1 : forall m x e, avl m ->
173
avl (add x e m) /\ 0 <= height (add x e m) - height m <= 1.
175
intros m x e; functional induction (add x e m); intros; inv avl; simpl in *.
176
intuition; try constructor; simpl; auto; try omega_max.
180
apply bal_avl; auto; omega_max.
183
intuition; omega_max.
187
apply bal_avl; auto; omega_max.
191
Lemma add_avl : forall m x e, avl m -> avl (add x e m).
193
intros; generalize (add_avl_1 x e H); intuition.
195
Hint Resolve add_avl.
197
(** * Extraction of minimum binding *)
199
Lemma remove_min_avl_1 : forall l x e r h, avl (Node l x e r h) ->
200
avl (remove_min l x e r)#1 /\
201
0 <= height (Node l x e r h) - height (remove_min l x e r)#1 <= 1.
203
intros l x e r; functional induction (remove_min l x e r); simpl in *; intros.
204
inv avl; simpl in *; split; auto.
207
rewrite e0 in IHp;simpl in IHp;destruct (IHp _x); auto.
209
apply bal_avl; auto; omega_max.
213
Lemma remove_min_avl : forall l x e r h, avl (Node l x e r h) ->
214
avl (remove_min l x e r)#1.
216
intros; generalize (remove_min_avl_1 H); intuition.
219
(** * Merging two trees *)
221
Lemma merge_avl_1 : forall m1 m2, avl m1 -> avl m2 ->
222
-(2) <= height m1 - height m2 <= 2 ->
224
0<= height (merge m1 m2) - max (height m1) (height m2) <=1.
226
intros m1 m2; functional induction (merge m1 m2); intros;
227
try factornode _x _x0 _x1 _x2 _x3 as m1.
228
simpl; split; auto; avl_nns; omega_max.
229
simpl; split; auto; avl_nns; omega_max.
230
generalize (remove_min_avl_1 H0).
231
rewrite e1; destruct 1.
238
Lemma merge_avl : forall m1 m2, avl m1 -> avl m2 ->
239
-(2) <= height m1 - height m2 <= 2 -> avl (merge m1 m2).
241
intros; generalize (merge_avl_1 H H0 H1); intuition.
247
Lemma remove_avl_1 : forall m x, avl m ->
248
avl (remove x m) /\ 0 <= height m - height (remove x m) <= 1.
250
intros m x; functional induction (remove x m); intros.
251
split; auto; omega_max.
261
generalize (merge_avl_1 H0 H1 H2).
272
Lemma remove_avl : forall m x, avl m -> avl (remove x m).
274
intros; generalize (remove_avl_1 x H); intuition.
276
Hint Resolve remove_avl.
281
Lemma join_avl_1 : forall l x d r, avl l -> avl r ->
282
avl (join l x d r) /\
283
0<= height (join l x d r) - max (height l) (height r) <= 1.
288
destruct (add_avl_1 x d H0).
290
set (l:=Node ll lx ld lr lh) in *.
292
destruct (add_avl_1 x d H).
293
simpl (height (Leaf elt)).
297
assert (height (Node rl rx rd rr rh) = rh); auto.
298
set (r := Node rl rx rd rr rh) in *; clearbody r.
299
destruct (Hlr x d r H2 H0); clear Hrl Hlr.
300
set (j := join lr x d r) in *; clearbody j.
302
assert (-(3) <= height ll - height j <= 3) by omega_max.
308
assert (height (Node ll lx ld lr lh) = lh); auto.
309
set (l := Node ll lx ld lr lh) in *; clearbody l.
310
destruct (Hrl H H1); clear Hrl Hlr.
311
set (j := join l x d rl) in *; clearbody j.
313
assert (-(3) <= height j - height rr <= 3) by omega_max.
319
assert (height (Node ll lx ld lr lh) = lh); auto.
320
assert (height (Node rl rx rd rr rh) = rh); auto.
321
set (l := Node ll lx ld lr lh) in *; clearbody l.
322
set (r := Node rl rx rd rr rh) in *; clearbody r.
323
assert (-(2) <= height l - height r <= 2) by omega_max.
325
apply create_avl; auto.
326
rewrite create_height; auto; omega_max.
329
Lemma join_avl : forall l x d r, avl l -> avl r -> avl (join l x d r).
331
intros; destruct (join_avl_1 x d H H0); auto.
333
Hint Resolve join_avl.
337
Lemma concat_avl : forall m1 m2, avl m1 -> avl m2 -> avl (concat m1 m2).
339
intros m1 m2; functional induction (concat m1 m2); auto.
340
intros; apply join_avl; auto.
341
generalize (remove_min_avl H0); rewrite e1; simpl; auto.
343
Hint Resolve concat_avl.
347
Lemma split_avl : forall m x, avl m ->
348
avl (split x m)#l /\ avl (split x m)#r.
350
intros m x; functional induction (split x m); simpl; auto.
351
rewrite e1 in IHt;simpl in IHt;inversion_clear 1; intuition.
352
simpl; inversion_clear 1; auto.
353
rewrite e1 in IHt;simpl in IHt;inversion_clear 1; intuition.
357
Hint Constructors avl.
360
Variable elt elt' : Type.
361
Variable f : elt -> elt'.
363
Lemma map_height : forall m, height (map f m) = height m.
365
destruct m; simpl; auto.
368
Lemma map_avl : forall m, avl m -> avl (map f m).
370
induction m; simpl; auto.
371
inversion_clear 1; constructor; auto; do 2 rewrite map_height; auto.
377
Variable elt elt' : Type.
378
Variable f : key -> elt -> elt'.
380
Lemma mapi_height : forall m, height (mapi f m) = height m.
382
destruct m; simpl; auto.
385
Lemma mapi_avl : forall m, avl m -> avl (mapi f m).
387
induction m; simpl; auto.
388
inversion_clear 1; constructor; auto; do 2 rewrite mapi_height; auto.
394
Variable elt elt' : Type.
395
Variable f : key -> elt -> option elt'.
397
Lemma map_option_avl : forall m, avl m -> avl (map_option f m).
399
induction m; simpl; auto; intros.
400
inv avl; destruct (f k e); auto using join_avl, concat_avl.
406
Variable elt elt' elt'' : Type.
407
Variable f : key -> elt -> option elt' -> option elt''.
408
Variable mapl : t elt -> t elt''.
409
Variable mapr : t elt' -> t elt''.
410
Hypothesis mapl_avl : forall m, avl m -> avl (mapl m).
411
Hypothesis mapr_avl : forall m', avl m' -> avl (mapr m').
413
Notation map2_opt := (map2_opt f mapl mapr).
415
Lemma map2_opt_avl : forall m1 m2, avl m1 -> avl m2 ->
416
avl (map2_opt m1 m2).
418
intros m1 m2; functional induction (map2_opt m1 m2); auto;
419
factornode _x0 _x1 _x2 _x3 _x4 as r2; intros;
420
destruct (split_avl x1 H0); rewrite e1 in *; simpl in *; inv avl;
421
auto using join_avl, concat_avl.
427
Variable elt elt' elt'' : Type.
428
Variable f : option elt -> option elt' -> option elt''.
430
Lemma map2_avl : forall m1 m2, avl m1 -> avl m2 -> avl (map2 f m1 m2).
432
unfold map2; auto using map2_opt_avl, map_option_avl.
440
We can implement [S] with balanced binary search trees.
441
When compared to [FMapAVL], we maintain here two invariants
442
(bst and avl) instead of only bst, which is enough for fulfilling
446
Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
449
Module Import AvlProofs := AvlProofs I X.
453
Record bbst (elt:Type) :=
454
Bbst {this :> tree elt; is_bst : bst this; is_avl: avl this}.
456
Definition t := bbst.
457
Definition key := E.t.
460
Variable elt elt' elt'': Type.
462
Implicit Types m : t elt.
463
Implicit Types x y : key.
464
Implicit Types e : elt.
466
Definition empty : t elt := Bbst (empty_bst elt) (empty_avl elt).
467
Definition is_empty m : bool := is_empty m.(this).
468
Definition add x e m : t elt :=
469
Bbst (add_bst x e m.(is_bst)) (add_avl x e m.(is_avl)).
470
Definition remove x m : t elt :=
471
Bbst (remove_bst x m.(is_bst)) (remove_avl x m.(is_avl)).
472
Definition mem x m : bool := mem x m.(this).
473
Definition find x m : option elt := find x m.(this).
474
Definition map f m : t elt' :=
475
Bbst (map_bst f m.(is_bst)) (map_avl f m.(is_avl)).
476
Definition mapi (f:key->elt->elt') m : t elt' :=
477
Bbst (mapi_bst f m.(is_bst)) (mapi_avl f m.(is_avl)).
478
Definition map2 f m (m':t elt') : t elt'' :=
479
Bbst (map2_bst f m.(is_bst) m'.(is_bst)) (map2_avl f m.(is_avl) m'.(is_avl)).
480
Definition elements m : list (key*elt) := elements m.(this).
481
Definition cardinal m := cardinal m.(this).
482
Definition fold (A:Type) (f:key->elt->A->A) m i := fold (A:=A) f m.(this) i.
483
Definition equal cmp m m' : bool := equal cmp m.(this) m'.(this).
485
Definition MapsTo x e m : Prop := MapsTo x e m.(this).
486
Definition In x m : Prop := In0 x m.(this).
487
Definition Empty m : Prop := Empty m.(this).
489
Definition eq_key : (key*elt) -> (key*elt) -> Prop := @PX.eqk elt.
490
Definition eq_key_elt : (key*elt) -> (key*elt) -> Prop := @PX.eqke elt.
491
Definition lt_key : (key*elt) -> (key*elt) -> Prop := @PX.ltk elt.
493
Lemma MapsTo_1 : forall m x y e, E.eq x y -> MapsTo x e m -> MapsTo y e m.
494
Proof. intros m; exact (@MapsTo_1 _ m.(this)). Qed.
496
Lemma mem_1 : forall m x, In x m -> mem x m = true.
498
unfold In, mem; intros m x; rewrite In_alt; simpl; apply mem_1; auto.
502
Lemma mem_2 : forall m x, mem x m = true -> In x m.
504
unfold In, mem; intros m x; rewrite In_alt; simpl; apply mem_2; auto.
507
Lemma empty_1 : Empty empty.
508
Proof. exact (@empty_1 elt). Qed.
510
Lemma is_empty_1 : forall m, Empty m -> is_empty m = true.
511
Proof. intros m; exact (@is_empty_1 _ m.(this)). Qed.
512
Lemma is_empty_2 : forall m, is_empty m = true -> Empty m.
513
Proof. intros m; exact (@is_empty_2 _ m.(this)). Qed.
515
Lemma add_1 : forall m x y e, E.eq x y -> MapsTo y e (add x e m).
516
Proof. intros m x y e; exact (@add_1 elt _ x y e). Qed.
517
Lemma add_2 : forall m x y e e', ~ E.eq x y -> MapsTo y e m -> MapsTo y e (add x e' m).
518
Proof. intros m x y e e'; exact (@add_2 elt _ x y e e'). Qed.
519
Lemma add_3 : forall m x y e e', ~ E.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m.
520
Proof. intros m x y e e'; exact (@add_3 elt _ x y e e'). Qed.
522
Lemma remove_1 : forall m x y, E.eq x y -> ~ In y (remove x m).
524
unfold In, remove; intros m x y; rewrite In_alt; simpl; apply remove_1; auto.
527
Lemma remove_2 : forall m x y e, ~ E.eq x y -> MapsTo y e m -> MapsTo y e (remove x m).
528
Proof. intros m x y e; exact (@remove_2 elt _ x y e m.(is_bst)). Qed.
529
Lemma remove_3 : forall m x y e, MapsTo y e (remove x m) -> MapsTo y e m.
530
Proof. intros m x y e; exact (@remove_3 elt _ x y e m.(is_bst)). Qed.
533
Lemma find_1 : forall m x e, MapsTo x e m -> find x m = Some e.
534
Proof. intros m x e; exact (@find_1 elt _ x e m.(is_bst)). Qed.
535
Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m.
536
Proof. intros m; exact (@find_2 elt m.(this)). Qed.
538
Lemma fold_1 : forall m (A : Type) (i : A) (f : key -> elt -> A -> A),
539
fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
540
Proof. intros m; exact (@fold_1 elt m.(this) m.(is_bst)). Qed.
542
Lemma elements_1 : forall m x e,
543
MapsTo x e m -> InA eq_key_elt (x,e) (elements m).
545
intros; unfold elements, MapsTo, eq_key_elt; rewrite elements_mapsto; auto.
548
Lemma elements_2 : forall m x e,
549
InA eq_key_elt (x,e) (elements m) -> MapsTo x e m.
551
intros; unfold elements, MapsTo, eq_key_elt; rewrite <- elements_mapsto; auto.
554
Lemma elements_3 : forall m, sort lt_key (elements m).
555
Proof. intros m; exact (@elements_sort elt m.(this) m.(is_bst)). Qed.
557
Lemma elements_3w : forall m, NoDupA eq_key (elements m).
558
Proof. intros m; exact (@elements_nodup elt m.(this) m.(is_bst)). Qed.
560
Lemma cardinal_1 : forall m, cardinal m = length (elements m).
561
Proof. intro m; exact (@elements_cardinal elt m.(this)). Qed.
563
Definition Equal m m' := forall y, find y m = find y m'.
564
Definition Equiv (eq_elt:elt->elt->Prop) m m' :=
565
(forall k, In k m <-> In k m') /\
566
(forall k e e', MapsTo k e m -> MapsTo k e' m' -> eq_elt e e').
567
Definition Equivb cmp := Equiv (Cmp cmp).
569
Lemma Equivb_Equivb : forall cmp m m',
570
Equivb cmp m m' <-> Raw.Proofs.Equivb cmp m m'.
572
intros; unfold Equivb, Equiv, Raw.Proofs.Equivb, In; intuition.
573
generalize (H0 k); do 2 rewrite In_alt; intuition.
574
generalize (H0 k); do 2 rewrite In_alt; intuition.
575
generalize (H0 k); do 2 rewrite <- In_alt; intuition.
576
generalize (H0 k); do 2 rewrite <- In_alt; intuition.
579
Lemma equal_1 : forall m m' cmp,
580
Equivb cmp m m' -> equal cmp m m' = true.
582
unfold equal; intros (m,b,a) (m',b',a') cmp; rewrite Equivb_Equivb;
583
intros; simpl in *; rewrite equal_Equivb; auto.
586
Lemma equal_2 : forall m m' cmp,
587
equal cmp m m' = true -> Equivb cmp m m'.
589
unfold equal; intros (m,b,a) (m',b',a') cmp; rewrite Equivb_Equivb;
590
intros; simpl in *; rewrite <-equal_Equivb; auto.
595
Lemma map_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)(f:elt->elt'),
596
MapsTo x e m -> MapsTo x (f e) (map f m).
597
Proof. intros elt elt' m x e f; exact (@map_1 elt elt' f m.(this) x e). Qed.
599
Lemma map_2 : forall (elt elt':Type)(m:t elt)(x:key)(f:elt->elt'), In x (map f m) -> In x m.
601
intros elt elt' m x f; do 2 unfold In in *; do 2 rewrite In_alt; simpl.
605
Lemma mapi_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)
606
(f:key->elt->elt'), MapsTo x e m ->
607
exists y, E.eq y x /\ MapsTo x (f y e) (mapi f m).
608
Proof. intros elt elt' m x e f; exact (@mapi_1 elt elt' f m.(this) x e). Qed.
609
Lemma mapi_2 : forall (elt elt':Type)(m: t elt)(x:key)
610
(f:key->elt->elt'), In x (mapi f m) -> In x m.
612
intros elt elt' m x f; unfold In in *; do 2 rewrite In_alt; simpl; apply mapi_2; auto.
615
Lemma map2_1 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt')
616
(x:key)(f:option elt->option elt'->option elt''),
618
find x (map2 f m m') = f (find x m) (find x m').
620
unfold find, map2, In; intros elt elt' elt'' m m' x f.
621
do 2 rewrite In_alt; intros; simpl; apply map2_1; auto.
626
Lemma map2_2 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt')
627
(x:key)(f:option elt->option elt'->option elt''),
628
In x (map2 f m m') -> In x m \/ In x m'.
630
unfold In, map2; intros elt elt' elt'' m m' x f.
631
do 3 rewrite In_alt; intros; simpl in *; eapply map2_2; eauto.
639
Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
640
Sord with Module Data := D
641
with Module MapS.E := X.
644
Module Import MapS := IntMake(I)(X).
647
Module Import MD := OrderedTypeFacts(D).
648
Module LO := FMapList.Make_ord(X)(D).
650
Definition t := MapS.t D.t.
652
Definition cmp e e' :=
653
match D.compare e e' with EQ _ => true | _ => false end.
655
Definition elements (m:t) :=
656
LO.MapS.Build_slist (Raw.Proofs.elements_sort m.(is_bst)).
658
(** * As comparison function, we propose here a non-structural
659
version faithful to the code of Ocaml's Map library, instead of
660
the structural version of FMapAVL *)
662
Fixpoint cardinal_e (e:Raw.enumeration D.t) :=
665
| Raw.More _ _ r e => S (Raw.cardinal r + cardinal_e e)
668
Lemma cons_cardinal_e : forall m e,
669
cardinal_e (Raw.cons m e) = (Raw.cardinal m + cardinal_e e)%nat.
671
induction m; simpl; intros; auto.
672
rewrite IHm1; simpl; rewrite <- plus_n_Sm; auto with arith.
675
Definition cardinal_e_2 ee :=
676
(cardinal_e (fst ee) + cardinal_e (snd ee))%nat.
678
Function compare_aux (ee:Raw.enumeration D.t * Raw.enumeration D.t)
679
{ measure cardinal_e_2 ee } : comparison :=
681
| (Raw.End, Raw.End) => Eq
682
| (Raw.End, Raw.More _ _ _ _) => Lt
683
| (Raw.More _ _ _ _, Raw.End) => Gt
684
| (Raw.More x1 d1 r1 e1, Raw.More x2 d2 r2 e2) =>
685
match X.compare x1 x2 with
686
| EQ _ => match D.compare d1 d2 with
687
| EQ _ => compare_aux (Raw.cons r1 e1, Raw.cons r2 e2)
696
intros; unfold cardinal_e_2; simpl;
697
abstract (do 2 rewrite cons_cardinal_e; romega with * ).
704
| Gt => (fun l1 l2 => LO.lt_list l2 l1)
707
Lemma cons_Cmp : forall c x1 x2 d1 d2 l1 l2,
708
X.eq x1 x2 -> D.eq d1 d2 ->
709
Cmp c l1 l2 -> Cmp c ((x1,d1)::l1) ((x2,d2)::l2).
711
destruct c; simpl; intros; MX.elim_comp; auto.
713
Hint Resolve cons_Cmp.
715
Lemma compare_aux_Cmp : forall e,
716
Cmp (compare_aux e) (flatten_e (fst e)) (flatten_e (snd e)).
718
intros e; functional induction (compare_aux e); simpl in *;
719
auto; intros; try clear e0; try clear e3; try MX.elim_comp; auto.
720
rewrite 2 cons_1 in IHc; auto.
723
Lemma compare_Cmp : forall m1 m2,
724
Cmp (compare_aux (Raw.cons m1 (Raw.End _), Raw.cons m2 (Raw.End _)))
725
(Raw.elements m1) (Raw.elements m2).
728
assert (H1:=cons_1 m1 (Raw.End _)).
729
assert (H2:=cons_1 m2 (Raw.End _)).
730
simpl in *; rewrite <- app_nil_end in *; rewrite <-H1,<-H2.
731
apply (@compare_aux_Cmp (Raw.cons m1 (Raw.End _),
732
Raw.cons m2 (Raw.End _))).
735
Definition eq (m1 m2 : t) := LO.eq_list (Raw.elements m1) (Raw.elements m2).
736
Definition lt (m1 m2 : t) := LO.lt_list (Raw.elements m1) (Raw.elements m2).
738
Definition compare (s s':t) : Compare lt eq s s'.
740
intros (s,b,a) (s',b',a').
741
generalize (compare_Cmp s s').
742
destruct compare_aux; intros; [apply EQ|apply LT|apply GT]; red; auto.
746
(* Proofs about [eq] and [lt] *)
748
Definition selements (m1 : t) :=
749
LO.MapS.Build_slist (elements_sort m1.(is_bst)).
751
Definition seq (m1 m2 : t) := LO.eq (selements m1) (selements m2).
752
Definition slt (m1 m2 : t) := LO.lt (selements m1) (selements m2).
754
Lemma eq_seq : forall m1 m2, eq m1 m2 <-> seq m1 m2.
756
unfold eq, seq, selements, elements, LO.eq; intuition.
759
Lemma lt_slt : forall m1 m2, lt m1 m2 <-> slt m1 m2.
761
unfold lt, slt, selements, elements, LO.lt; intuition.
764
Lemma eq_1 : forall (m m' : t), MapS.Equivb cmp m m' -> eq m m'.
767
rewrite eq_seq; unfold seq.
768
rewrite Equivb_Equivb.
769
rewrite Equivb_elements.
773
Lemma eq_2 : forall m m', eq m m' -> MapS.Equivb cmp m m'.
776
rewrite eq_seq; unfold seq.
777
rewrite Equivb_Equivb.
778
rewrite Equivb_elements.
780
generalize (LO.eq_2 H).
784
Lemma eq_refl : forall m : t, eq m m.
786
intros; rewrite eq_seq; unfold seq; intros; apply LO.eq_refl.
789
Lemma eq_sym : forall m1 m2 : t, eq m1 m2 -> eq m2 m1.
791
intros m1 m2; rewrite 2 eq_seq; unfold seq; intros; apply LO.eq_sym; auto.
794
Lemma eq_trans : forall m1 m2 m3 : t, eq m1 m2 -> eq m2 m3 -> eq m1 m3.
796
intros m1 m2 M3; rewrite 3 eq_seq; unfold seq.
797
intros; eapply LO.eq_trans; eauto.
800
Lemma lt_trans : forall m1 m2 m3 : t, lt m1 m2 -> lt m2 m3 -> lt m1 m3.
802
intros m1 m2 m3; rewrite 3 lt_slt; unfold slt;
803
intros; eapply LO.lt_trans; eauto.
806
Lemma lt_not_eq : forall m1 m2 : t, lt m1 m2 -> ~ eq m1 m2.
808
intros m1 m2; rewrite lt_slt, eq_seq; unfold slt, seq;
809
intros; apply LO.lt_not_eq; auto.
814
(* For concrete use inside Coq, we propose an instantiation of [Int] by [Z]. *)
816
Module Make (X: OrderedType) <: S with Module E := X
817
:=IntMake(Z_as_Int)(X).
819
Module Make_ord (X: OrderedType)(D: OrderedType)
820
<: Sord with Module Data := D
821
with Module MapS.E := X
822
:=IntMake_ord(Z_as_Int)(X)(D).
added
removed
theories/FSets/FMapFullAVL.v
