1
(***********************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
4
(* \VV/ *************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(***********************************************************************)
9
(* Finite sets library.
10
* Authors: Pierre Letouzey and Jean-Christophe Filliâtre
11
* Institution: LRI, CNRS UMR 8623 - Université Paris Sud
12
* 91405 Orsay, France *)
14
(* $Id: FSetFullAVL.v 11699 2008-12-18 11:49:08Z letouzey $ *)
18
This file contains some complements to [FSetAVL].
20
- Functor [AvlProofs] proves that trees of [FSetAVL] are not only
21
binary search trees, but moreover well-balanced ones. This is done
22
by proving that all operations preserve the balancing.
24
- Functor [OcamlOps] contains variants of [union], [subset],
25
[compare] and [equal] that are faithful to the original ocaml codes,
26
while the versions in FSetAVL have been adapted to perform only
27
structural recursive code.
29
- Finally, we pack the previous elements in a [Make] functor
30
similar to the one of [FSetAVL], but richer.
33
Require Import Recdef FSetInterface FSetList ZArith Int FSetAVL.
35
Set Implicit Arguments.
36
Unset Strict Implicit.
38
Module AvlProofs (Import I:Int)(X:OrderedType).
39
Module Import Raw := Raw I X.
41
Module Import II := MoreInt I.
42
Open Local Scope pair_scope.
43
Open Local Scope Int_scope.
47
(** [avl s] : [s] is a properly balanced AVL tree,
48
i.e. for any node the heights of the two children
49
differ by at most 2 *)
51
Inductive avl : tree -> Prop :=
53
| RBNode : forall x l r h, avl l -> avl r ->
54
-(2) <= height l - height r <= 2 ->
55
h = max (height l) (height r) + 1 ->
58
(** * Automation and dedicated tactics *)
60
Hint Constructors avl.
62
(** A tactic for cleaning hypothesis after use of functional induction. *)
66
| H : (@Logic.eq (Compare _ _ _ _) _ _) |- _ => clear H; clearf
67
| H : (@Logic.eq (sumbool _ _) _ _) |- _ => clear H; clearf
71
(** Tactics about [avl] *)
73
Lemma height_non_negative : forall s : tree, avl s -> height s >= 0.
75
induction s; simpl; intros; auto with zarith.
76
inv avl; intuition; omega_max.
78
Implicit Arguments height_non_negative.
80
(** When [H:avl r], typing [avl_nn H] or [avl_nn r] adds [height r>=0] *)
83
let nz := fresh "nz" in assert (nz := height_non_negative H).
88
| Prop => avl_nn_hyp h
89
| _ => match goal with H : avl h |- _ => avl_nn_hyp H end
92
(* Repeat the previous tactic.
93
Drawback: need to clear the [avl _] hyps ... Thank you Ltac *)
97
| H:avl _ |- _ => avl_nn_hyp H; clear H; avl_nns
101
(** Results about [height] *)
103
Lemma height_0 : forall s, avl s -> height s = 0 -> s = Leaf.
105
destruct 1; intuition; simpl in *.
106
avl_nns; simpl in *; elimtype False; omega_max.
109
(** * Results about [avl] *)
112
forall x l r, avl l -> avl r ->
113
-(2) <= height l - height r <= 2 ->
114
avl (Node l x r (max (height l) (height r) + 1)).
118
Hint Resolve avl_node.
123
Lemma empty_avl : avl empty.
130
Lemma singleton_avl : forall x : elt, avl (singleton x).
132
unfold singleton; intro.
133
constructor; auto; try red; simpl; omega_max.
139
forall l x r, avl l -> avl r -> -(2) <= height l - height r <= 2 ->
145
Lemma create_height :
146
forall l x r, avl l -> avl r -> -(2) <= height l - height r <= 2 ->
147
height (create l x r) = max (height l) (height r) + 1.
154
Lemma bal_avl : forall l x r, avl l -> avl r ->
155
-(3) <= height l - height r <= 3 -> avl (bal l x r).
157
intros l x r; functional induction bal l x r; intros; clearf;
159
match goal with |- avl (assert_false _ _ _) => avl_nns
160
| _ => repeat apply create_avl; simpl in *; auto
164
Lemma bal_height_1 : forall l x r, avl l -> avl r ->
165
-(3) <= height l - height r <= 3 ->
166
0 <= height (bal l x r) - max (height l) (height r) <= 1.
168
intros l x r; functional induction bal l x r; intros; clearf;
169
inv avl; avl_nns; simpl in *; omega_max.
173
forall l x r, avl l -> avl r -> -(2) <= height l - height r <= 2 ->
174
height (bal l x r) == max (height l) (height r) +1.
176
intros l x r; functional induction bal l x r; intros; clearf;
177
inv avl; simpl in *; omega_max.
180
Ltac omega_bal := match goal with
181
| H:avl ?l, H':avl ?r |- context [ bal ?l ?x ?r ] =>
182
generalize (bal_height_1 x H H') (bal_height_2 x H H');
188
Lemma add_avl_1 : forall s x, avl s ->
189
avl (add x s) /\ 0 <= height (add x s) - height s <= 1.
191
intros s x; functional induction (add x s); subst;intros; inv avl; simpl in *.
192
intuition; try constructor; simpl; auto; try omega_max.
196
apply bal_avl; auto; omega_max.
199
intuition; omega_max.
203
apply bal_avl; auto; omega_max.
207
Lemma add_avl : forall s x, avl s -> avl (add x s).
209
intros; destruct (add_avl_1 x H); auto.
211
Hint Resolve add_avl.
215
Lemma join_avl_1 : forall l x r, avl l -> avl r -> avl (join l x r) /\
216
0<= height (join l x r) - max (height l) (height r) <= 1.
221
destruct (add_avl_1 x H0).
223
set (l:=Node ll lx lr lh) in *.
225
destruct (add_avl_1 x H).
230
assert (height (Node rl rx rr rh) = rh); auto.
231
set (r := Node rl rx rr rh) in *; clearbody r.
232
destruct (Hlr x r H2 H0); clear Hrl Hlr.
233
set (j := join lr x r) in *; clearbody j.
235
assert (-(3) <= height ll - height j <= 3) by omega_max.
241
assert (height (Node ll lx lr lh) = lh); auto.
242
set (l := Node ll lx lr lh) in *; clearbody l.
243
destruct (Hrl H H1); clear Hrl Hlr.
244
set (j := join l x rl) in *; clearbody j.
246
assert (-(3) <= height j - height rr <= 3) by omega_max.
252
assert (height (Node ll lx lr lh) = lh); auto.
253
assert (height (Node rl rx rr rh) = rh); auto.
254
set (l := Node ll lx lr lh) in *; clearbody l.
255
set (r := Node rl rx rr rh) in *; clearbody r.
256
assert (-(2) <= height l - height r <= 2) by omega_max.
258
apply create_avl; auto.
259
rewrite create_height; auto; omega_max.
262
Lemma join_avl : forall l x r, avl l -> avl r -> avl (join l x r).
264
intros; destruct (join_avl_1 x H H0); auto.
266
Hint Resolve join_avl.
270
Lemma remove_min_avl_1 : forall l x r h, avl (Node l x r h) ->
271
avl (remove_min l x r)#1 /\
272
0 <= height (Node l x r h) - height (remove_min l x r)#1 <= 1.
274
intros l x r; functional induction (remove_min l x r); subst;simpl in *; intros.
275
inv avl; simpl in *; split; auto.
278
rewrite e0 in IHp;simpl in IHp;destruct (IHp _x); auto.
280
apply bal_avl; auto; omega_max.
284
Lemma remove_min_avl : forall l x r h, avl (Node l x r h) ->
285
avl (remove_min l x r)#1.
287
intros; destruct (remove_min_avl_1 H); auto.
292
Lemma merge_avl_1 : forall s1 s2, avl s1 -> avl s2 ->
293
-(2) <= height s1 - height s2 <= 2 ->
295
0<= height (merge s1 s2) - max (height s1) (height s2) <=1.
297
intros s1 s2; functional induction (merge s1 s2); intros;
298
try factornode _x _x0 _x1 _x2 as s1.
299
simpl; split; auto; avl_nns; omega_max.
300
simpl; split; auto; avl_nns; simpl in *; omega_max.
301
generalize (remove_min_avl_1 H0).
302
rewrite e1; destruct 1.
306
simpl in *; omega_bal.
309
Lemma merge_avl : forall s1 s2, avl s1 -> avl s2 ->
310
-(2) <= height s1 - height s2 <= 2 -> avl (merge s1 s2).
312
intros; destruct (merge_avl_1 H H0 H1); auto.
318
Lemma remove_avl_1 : forall s x, avl s ->
319
avl (remove x s) /\ 0 <= height s - height (remove x s) <= 1.
321
intros s x; functional induction (remove x s); intros.
322
intuition; omega_max.
332
generalize (merge_avl_1 H0 H1 H2).
343
Lemma remove_avl : forall s x, avl s -> avl (remove x s).
345
intros; destruct (remove_avl_1 x H); auto.
347
Hint Resolve remove_avl.
351
Lemma concat_avl : forall s1 s2, avl s1 -> avl s2 -> avl (concat s1 s2).
353
intros s1 s2; functional induction (concat s1 s2); auto.
354
intros; apply join_avl; auto.
355
generalize (remove_min_avl H0); rewrite e1; simpl; auto.
357
Hint Resolve concat_avl.
361
Lemma split_avl : forall s x, avl s ->
362
avl (split x s)#l /\ avl (split x s)#r.
364
intros s x; functional induction (split x s); simpl; auto.
365
rewrite e1 in IHt;simpl in IHt;inversion_clear 1; intuition.
366
simpl; inversion_clear 1; auto.
367
rewrite e1 in IHt;simpl in IHt;inversion_clear 1; intuition.
372
Lemma inter_avl : forall s1 s2, avl s1 -> avl s2 -> avl (inter s1 s2).
374
intros s1 s2; functional induction inter s1 s2; auto; intros A1 A2;
375
generalize (split_avl x1 A2); rewrite e1; simpl; destruct 1;
381
Lemma diff_avl : forall s1 s2, avl s1 -> avl s2 -> avl (diff s1 s2).
383
intros s1 s2; functional induction diff s1 s2; auto; intros A1 A2;
384
generalize (split_avl x1 A2); rewrite e1; simpl; destruct 1;
390
Lemma union_avl : forall s1 s2, avl s1 -> avl s2 -> avl (union s1 s2).
392
intros s1 s2; functional induction union s1 s2; auto; intros A1 A2;
393
generalize (split_avl x1 A2); rewrite e1; simpl; destruct 1;
399
Lemma filter_acc_avl : forall f s acc, avl s -> avl acc ->
400
avl (filter_acc f acc s).
402
induction s; simpl; auto.
405
destruct (f t); auto.
407
Hint Resolve filter_acc_avl.
409
Lemma filter_avl : forall f s, avl s -> avl (filter f s).
411
unfold filter; intros; apply filter_acc_avl; auto.
416
Lemma partition_acc_avl_1 : forall f s acc, avl s ->
417
avl acc#1 -> avl (partition_acc f acc s)#1.
419
induction s; simpl; auto.
420
destruct acc as [acct accf]; simpl in *.
425
destruct (f t); simpl; auto.
428
Lemma partition_acc_avl_2 : forall f s acc, avl s ->
429
avl acc#2 -> avl (partition_acc f acc s)#2.
431
induction s; simpl; auto.
432
destruct acc as [acct accf]; simpl in *.
437
destruct (f t); simpl; auto.
440
Lemma partition_avl_1 : forall f s, avl s -> avl (partition f s)#1.
442
unfold partition; intros; apply partition_acc_avl_1; auto.
445
Lemma partition_avl_2 : forall f s, avl s -> avl (partition f s)#2.
447
unfold partition; intros; apply partition_acc_avl_2; auto.
453
Module OcamlOps (Import I:Int)(X:OrderedType).
454
Module Import AvlProofs := AvlProofs I X.
458
Open Local Scope pair_scope.
459
Open Local Scope nat_scope.
461
(** Properties of cardinal *)
463
Lemma bal_cardinal : forall l x r,
464
cardinal (bal l x r) = S (cardinal l + cardinal r).
466
intros l x r; functional induction bal l x r; intros; clearf;
467
simpl; auto with arith; romega with *.
470
Lemma add_cardinal : forall x s,
471
cardinal (add x s) <= S (cardinal s).
473
intros; functional induction add x s; simpl; auto with arith;
474
rewrite bal_cardinal; romega with *.
477
Lemma join_cardinal : forall l x r,
478
cardinal (join l x r) <= S (cardinal l + cardinal r).
480
join_tac; auto with arith.
481
simpl; apply add_cardinal.
482
simpl; destruct X.compare; simpl; auto with arith.
483
generalize (bal_cardinal (add x ll) lx lr) (add_cardinal x ll);
485
generalize (bal_cardinal ll lx (add x lr)) (add_cardinal x lr);
487
generalize (bal_cardinal ll lx (join lr x (Node rl rx rr rh)))
488
(Hlr x (Node rl rx rr rh)); simpl; romega with *.
489
simpl S in *; generalize (bal_cardinal (join (Node ll lx lr lh) x rl) rx rr).
493
Lemma split_cardinal_1 : forall x s,
494
(cardinal (split x s)#l <= cardinal s)%nat.
496
intros x s; functional induction split x s; simpl; auto.
497
rewrite e1 in IHt; simpl in *.
500
rewrite e1 in IHt; simpl in *.
501
generalize (@join_cardinal l y rl); romega with *.
504
Lemma split_cardinal_2 : forall x s,
505
(cardinal (split x s)#r <= cardinal s)%nat.
507
intros x s; functional induction split x s; simpl; auto.
508
rewrite e1 in IHt; simpl in *.
509
generalize (@join_cardinal rl y r); romega with *.
511
rewrite e1 in IHt; simpl in *; romega with *.
514
(** * [ocaml_union], an union faithful to the original ocaml code *)
516
Definition cardinal2 (s:t*t) := (cardinal s#1 + cardinal s#2)%nat.
518
Ltac ocaml_union_tac :=
519
intros; unfold cardinal2; simpl fst in *; simpl snd in *;
520
match goal with H: split ?x ?s = _ |- _ =>
521
generalize (split_cardinal_1 x s) (split_cardinal_2 x s);
522
rewrite H; simpl; romega with *
525
Import Logic. (* Unhide eq, otherwise Function complains. *)
527
Function ocaml_union (s : t * t) { measure cardinal2 s } : t :=
529
| (Leaf, Leaf) => s#2
530
| (Leaf, Node _ _ _ _) => s#2
531
| (Node _ _ _ _, Leaf) => s#1
532
| (Node l1 x1 r1 h1, Node l2 x2 r2 h2) =>
533
if ge_lt_dec h1 h2 then
534
if eq_dec h2 1%I then add x2 s#1 else
535
let (l2',_,r2') := split x1 s#2 in
536
join (ocaml_union (l1,l2')) x1 (ocaml_union (r1,r2'))
538
if eq_dec h1 1%I then add x1 s#2 else
539
let (l1',_,r1') := split x2 s#1 in
540
join (ocaml_union (l1',l2)) x2 (ocaml_union (r1',r2))
543
abstract ocaml_union_tac.
544
abstract ocaml_union_tac.
545
abstract ocaml_union_tac.
546
abstract ocaml_union_tac.
549
Lemma ocaml_union_in : forall s y,
550
bst s#1 -> avl s#1 -> bst s#2 -> avl s#2 ->
551
(In y (ocaml_union s) <-> In y s#1 \/ In y s#2).
553
intros s; functional induction ocaml_union s; intros y B1 A1 B2 A2;
554
simpl fst in *; simpl snd in *; try clear e0 e1.
560
rewrite (height_0 H); [ | avl_nn l2; omega_max].
561
rewrite (height_0 H0); [ | avl_nn r2; omega_max].
562
rewrite add_in; intuition_in.
563
(* join (union (l1,l2')) x1 (union (r1,r2')) *)
565
(split_avl x1 A2) (split_bst x1 B2)
566
(split_in_1 x1 y B2) (split_in_2 x1 y B2).
568
destruct 1; destruct 1; inv avl; inv bst.
569
rewrite join_in, IHt, IHt0; auto.
570
do 2 (intro Eq; rewrite Eq; clear Eq).
571
case (X.compare y x1); intuition_in.
574
rewrite (height_0 H3); [ | avl_nn l1; omega_max].
575
rewrite (height_0 H4); [ | avl_nn r1; omega_max].
576
rewrite add_in; auto; intuition_in.
577
(* join (union (l1',l2)) x1 (union (r1',r2)) *)
579
(split_avl x2 A1) (split_bst x2 B1)
580
(split_in_1 x2 y B1) (split_in_2 x2 y B1).
582
destruct 1; destruct 1; inv avl; inv bst.
583
rewrite join_in, IHt, IHt0; auto.
584
do 2 (intro Eq; rewrite Eq; clear Eq).
585
case (X.compare y x2); intuition_in.
588
Lemma ocaml_union_bst : forall s,
589
bst s#1 -> avl s#1 -> bst s#2 -> avl s#2 -> bst (ocaml_union s).
591
intros s; functional induction ocaml_union s; intros B1 A1 B2 A2;
592
simpl fst in *; simpl snd in *; try clear e0 e1;
593
try apply add_bst; auto.
594
(* join (union (l1,l2')) x1 (union (r1,r2')) *)
595
clear _x _x0; factornode l2 x2 r2 h2 as s2.
596
generalize (split_avl x1 A2) (split_bst x1 B2)
597
(@split_in_1 s2 x1)(@split_in_2 s2 x1).
599
destruct 1; destruct 1; intros.
601
apply join_bst; auto.
602
intro y; rewrite ocaml_union_in, H3; intuition_in.
603
intro y; rewrite ocaml_union_in, H4; intuition_in.
604
(* join (union (l1',l2)) x1 (union (r1',r2)) *)
605
clear _x _x0; factornode l1 x1 r1 h1 as s1.
606
generalize (split_avl x2 A1) (split_bst x2 B1)
607
(@split_in_1 s1 x2)(@split_in_2 s1 x2).
609
destruct 1; destruct 1; intros.
611
apply join_bst; auto.
612
intro y; rewrite ocaml_union_in, H3; intuition_in.
613
intro y; rewrite ocaml_union_in, H4; intuition_in.
616
Lemma ocaml_union_avl : forall s,
617
avl s#1 -> avl s#2 -> avl (ocaml_union s).
619
intros s; functional induction ocaml_union s;
620
simpl fst in *; simpl snd in *; auto.
621
intros A1 A2; generalize (split_avl x1 A2); rewrite e2; simpl.
622
inv avl; destruct 1; auto.
623
intros A1 A2; generalize (split_avl x2 A1); rewrite e2; simpl.
624
inv avl; destruct 1; auto.
627
Lemma ocaml_union_alt : forall s, bst s#1 -> avl s#1 -> bst s#2 -> avl s#2 ->
628
Equal (ocaml_union s) (union s#1 s#2).
630
red; intros; rewrite ocaml_union_in, union_in; simpl; intuition.
634
(** * [ocaml_subset], a subset faithful to the original ocaml code *)
636
Function ocaml_subset (s:t*t) { measure cardinal2 s } : bool :=
639
| (Node _ _ _ _, Leaf) => false
640
| (Node l1 x1 r1 h1, Node l2 x2 r2 h2) =>
641
match X.compare x1 x2 with
642
| EQ _ => ocaml_subset (l1,l2) && ocaml_subset (r1,r2)
643
| LT _ => ocaml_subset (Node l1 x1 Leaf 0%I, l2) && ocaml_subset (r1,s#2)
644
| GT _ => ocaml_subset (Node Leaf x1 r1 0%I, r2) && ocaml_subset (l1,s#2)
649
intros; unfold cardinal2; simpl; abstract romega with *.
650
intros; unfold cardinal2; simpl; abstract romega with *.
651
intros; unfold cardinal2; simpl; abstract romega with *.
652
intros; unfold cardinal2; simpl; abstract romega with *.
653
intros; unfold cardinal2; simpl; abstract romega with *.
654
intros; unfold cardinal2; simpl; abstract romega with *.
657
Lemma ocaml_subset_12 : forall s,
658
bst s#1 -> bst s#2 ->
659
(ocaml_subset s = true <-> Subset s#1 s#2).
661
intros s; functional induction ocaml_subset s; simpl;
662
intros B1 B2; try clear e0.
664
red; auto; inversion 1.
665
split; intros; try discriminate.
666
assert (H': In _x0 Leaf) by auto; inversion H'.
669
rewrite andb_true_iff, IHb, IHb0; auto; clear IHb IHb0.
670
unfold Subset; intuition_in.
671
assert (X.eq a x2) by order; intuition_in.
672
assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
673
assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
676
rewrite andb_true_iff, IHb, IHb0; auto; clear IHb IHb0.
677
unfold Subset; intuition_in.
678
assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
679
assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
682
rewrite andb_true_iff, IHb, IHb0; auto; clear IHb IHb0.
683
unfold Subset; intuition_in.
684
assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
685
assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
688
Lemma ocaml_subset_alt : forall s, bst s#1 -> bst s#2 ->
689
ocaml_subset s = subset s#1 s#2.
692
generalize (ocaml_subset_12 H H0); rewrite <-subset_12 by auto.
693
destruct ocaml_subset; destruct subset; intuition.
698
(** [ocaml_compare], a compare faithful to the original ocaml code *)
700
(** termination of [compare_aux] *)
702
Fixpoint cardinal_e e := match e with
704
| More _ s r => S (cardinal s + cardinal_e r)
707
Lemma cons_cardinal_e : forall s e,
708
cardinal_e (cons s e) = cardinal s + cardinal_e e.
710
induction s; simpl; intros; auto.
711
rewrite IHs1; simpl; rewrite <- plus_n_Sm; auto with arith.
714
Definition cardinal_e_2 e := cardinal_e e#1 + cardinal_e e#2.
716
Function ocaml_compare_aux
717
(e:enumeration*enumeration) { measure cardinal_e_2 e } : comparison :=
720
| (End,More _ _ _) => Lt
721
| (More _ _ _, End) => Gt
722
| (More x1 r1 e1, More x2 r2 e2) =>
723
match X.compare x1 x2 with
724
| EQ _ => ocaml_compare_aux (cons r1 e1, cons r2 e2)
731
intros; unfold cardinal_e_2; simpl;
732
abstract (do 2 rewrite cons_cardinal_e; romega with *).
735
Definition ocaml_compare s1 s2 :=
736
ocaml_compare_aux (cons s1 End, cons s2 End).
738
Lemma ocaml_compare_aux_Cmp : forall e,
739
Cmp (ocaml_compare_aux e) (flatten_e e#1) (flatten_e e#2).
741
intros e; functional induction ocaml_compare_aux e; simpl; intros;
742
auto; try discriminate.
745
apply cons_Cmp; auto.
746
rewrite <- 2 cons_1; auto.
749
Lemma ocaml_compare_Cmp : forall s1 s2,
750
Cmp (ocaml_compare s1 s2) (elements s1) (elements s2).
752
unfold ocaml_compare; intros.
753
assert (H1:=cons_1 s1 End).
754
assert (H2:=cons_1 s2 End).
755
simpl in *; rewrite <- app_nil_end in *; rewrite <-H1,<-H2.
756
apply (@ocaml_compare_aux_Cmp (cons s1 End, cons s2 End)).
759
Lemma ocaml_compare_alt : forall s1 s2, bst s1 -> bst s2 ->
760
ocaml_compare s1 s2 = compare s1 s2.
763
generalize (ocaml_compare_Cmp s1 s2)(compare_Cmp s1 s2).
765
destruct ocaml_compare; destruct compare; auto; intros; elimtype False.
766
elim (lt_not_eq B1 B2 H0); auto.
767
elim (lt_not_eq B2 B1 H0); auto.
769
elim (lt_not_eq B1 B2 H); auto.
770
elim (lt_not_eq B1 B1).
771
red; eapply L.lt_trans; eauto.
773
elim (lt_not_eq B2 B1 H); auto.
775
elim (lt_not_eq B1 B2 H0); auto.
776
elim (lt_not_eq B1 B1).
777
red; eapply L.lt_trans; eauto.
782
(** * Equality test *)
784
Definition ocaml_equal s1 s2 : bool :=
785
match ocaml_compare s1 s2 with
790
Lemma ocaml_equal_1 : forall s1 s2, bst s1 -> bst s2 ->
791
Equal s1 s2 -> ocaml_equal s1 s2 = true.
793
unfold ocaml_equal; intros s1 s2 B1 B2 E.
794
generalize (ocaml_compare_Cmp s1 s2).
795
destruct (ocaml_compare s1 s2); auto; intros.
796
elim (lt_not_eq B1 B2 H E); auto.
797
elim (lt_not_eq B2 B1 H (eq_sym E)); auto.
800
Lemma ocaml_equal_2 : forall s1 s2,
801
ocaml_equal s1 s2 = true -> Equal s1 s2.
803
unfold ocaml_equal; intros s1 s2 E.
804
generalize (ocaml_compare_Cmp s1 s2);
805
destruct ocaml_compare; auto; discriminate.
808
Lemma ocaml_equal_alt : forall s1 s2, bst s1 -> bst s2 ->
809
ocaml_equal s1 s2 = equal s1 s2.
811
intros; unfold ocaml_equal, equal; rewrite ocaml_compare_alt; auto.
820
We can implement [S] with balanced binary search trees.
821
When compared to [FSetAVL], we maintain here two invariants
822
(bst and avl) instead of only bst, which is enough for fulfilling
825
This encapsulation propose the non-structural variants
826
[ocaml_union], [ocaml_subset], [ocaml_compare], [ocaml_equal].
829
Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
832
Module Import OcamlOps := OcamlOps I X.
837
Record bbst := Bbst {this :> Raw.t; is_bst : bst this; is_avl : avl this}.
838
Definition t := bbst.
839
Definition elt := E.t.
841
Definition In (x : elt) (s : t) : Prop := In x s.
842
Definition Equal (s s':t) : Prop := forall a : elt, In a s <-> In a s'.
843
Definition Subset (s s':t) : Prop := forall a : elt, In a s -> In a s'.
844
Definition Empty (s:t) : Prop := forall a : elt, ~ In a s.
845
Definition For_all (P : elt -> Prop) (s:t) : Prop := forall x, In x s -> P x.
846
Definition Exists (P : elt -> Prop) (s:t) : Prop := exists x, In x s /\ P x.
848
Lemma In_1 : forall (s:t)(x y:elt), E.eq x y -> In x s -> In y s.
849
Proof. intro s; exact (@In_1 s). Qed.
851
Definition mem (x:elt)(s:t) : bool := mem x s.
853
Definition empty : t := Bbst empty_bst empty_avl.
854
Definition is_empty (s:t) : bool := is_empty s.
855
Definition singleton (x:elt) : t :=
856
Bbst (singleton_bst x) (singleton_avl x).
857
Definition add (x:elt)(s:t) : t :=
858
Bbst (add_bst x (is_bst s)) (add_avl x (is_avl s)).
859
Definition remove (x:elt)(s:t) : t :=
860
Bbst (remove_bst x (is_bst s)) (remove_avl x (is_avl s)).
861
Definition inter (s s':t) : t :=
862
Bbst (inter_bst (is_bst s) (is_bst s'))
863
(inter_avl (is_avl s) (is_avl s')).
864
Definition union (s s':t) : t :=
865
Bbst (union_bst (is_bst s) (is_bst s'))
866
(union_avl (is_avl s) (is_avl s')).
867
Definition ocaml_union (s s':t) : t :=
868
Bbst (@ocaml_union_bst (s.(this),s'.(this))
869
(is_bst s) (is_avl s) (is_bst s') (is_avl s'))
870
(@ocaml_union_avl (s.(this),s'.(this)) (is_avl s) (is_avl s')).
871
Definition diff (s s':t) : t :=
872
Bbst (diff_bst (is_bst s) (is_bst s'))
873
(diff_avl (is_avl s) (is_avl s')).
874
Definition elements (s:t) : list elt := elements s.
875
Definition min_elt (s:t) : option elt := min_elt s.
876
Definition max_elt (s:t) : option elt := max_elt s.
877
Definition choose (s:t) : option elt := choose s.
878
Definition fold (B : Type) (f : elt -> B -> B) (s:t) : B -> B := fold f s.
879
Definition cardinal (s:t) : nat := cardinal s.
880
Definition filter (f : elt -> bool) (s:t) : t :=
881
Bbst (filter_bst f (is_bst s)) (filter_avl f (is_avl s)).
882
Definition for_all (f : elt -> bool) (s:t) : bool := for_all f s.
883
Definition exists_ (f : elt -> bool) (s:t) : bool := exists_ f s.
884
Definition partition (f : elt -> bool) (s:t) : t * t :=
885
let p := partition f s in
886
(@Bbst (fst p) (partition_bst_1 f (is_bst s))
887
(partition_avl_1 f (is_avl s)),
888
@Bbst (snd p) (partition_bst_2 f (is_bst s))
889
(partition_avl_2 f (is_avl s))).
891
Definition equal (s s':t) : bool := equal s s'.
892
Definition ocaml_equal (s s':t) : bool := ocaml_equal s s'.
893
Definition subset (s s':t) : bool := subset s s'.
894
Definition ocaml_subset (s s':t) : bool :=
895
ocaml_subset (s.(this),s'.(this)).
897
Definition eq (s s':t) : Prop := Equal s s'.
898
Definition lt (s s':t) : Prop := lt s s'.
900
Definition compare (s s':t) : Compare lt eq s s'.
902
intros (s,b,a) (s',b',a').
903
generalize (compare_Cmp s s').
904
destruct Raw.compare; intros; [apply EQ|apply LT|apply GT]; red; auto.
905
change (Raw.Equal s s'); auto.
908
Definition ocaml_compare (s s':t) : Compare lt eq s s'.
910
intros (s,b,a) (s',b',a').
911
generalize (ocaml_compare_Cmp s s').
912
destruct ocaml_compare; intros; [apply EQ|apply LT|apply GT]; red; auto.
913
change (Raw.Equal s s'); auto.
916
Definition eq_dec (s s':t) : { eq s s' } + { ~ eq s s' }.
918
intros (s,b,a) (s',b',a'); unfold eq; simpl.
919
case_eq (Raw.equal s s'); intro H; [left|right].
921
intro H'; rewrite equal_1 in H; auto; discriminate.
926
Variable s s' s'': t.
929
Hint Resolve is_bst is_avl.
931
Lemma mem_1 : In x s -> mem x s = true.
932
Proof. exact (mem_1 (is_bst s)). Qed.
933
Lemma mem_2 : mem x s = true -> In x s.
934
Proof. exact (@mem_2 s x). Qed.
936
Lemma equal_1 : Equal s s' -> equal s s' = true.
937
Proof. exact (equal_1 (is_bst s) (is_bst s')). Qed.
938
Lemma equal_2 : equal s s' = true -> Equal s s'.
939
Proof. exact (@equal_2 s s'). Qed.
941
Lemma ocaml_equal_alt : ocaml_equal s s' = equal s s'.
943
destruct s; destruct s'; unfold ocaml_equal, equal; simpl.
944
apply ocaml_equal_alt; auto.
947
Lemma ocaml_equal_1 : Equal s s' -> ocaml_equal s s' = true.
948
Proof. exact (ocaml_equal_1 (is_bst s) (is_bst s')). Qed.
949
Lemma ocaml_equal_2 : ocaml_equal s s' = true -> Equal s s'.
950
Proof. exact (@ocaml_equal_2 s s'). Qed.
952
Ltac wrap t H := unfold t, In; simpl; rewrite H; auto; intuition.
954
Lemma subset_1 : Subset s s' -> subset s s' = true.
955
Proof. wrap subset subset_12. Qed.
956
Lemma subset_2 : subset s s' = true -> Subset s s'.
957
Proof. wrap subset subset_12. Qed.
959
Lemma ocaml_subset_alt : ocaml_subset s s' = subset s s'.
961
destruct s; destruct s'; unfold ocaml_subset, subset; simpl.
962
rewrite ocaml_subset_alt; auto.
965
Lemma ocaml_subset_1 : Subset s s' -> ocaml_subset s s' = true.
966
Proof. wrap ocaml_subset ocaml_subset_12; simpl; auto. Qed.
967
Lemma ocaml_subset_2 : ocaml_subset s s' = true -> Subset s s'.
968
Proof. wrap ocaml_subset ocaml_subset_12; simpl; auto. Qed.
970
Lemma empty_1 : Empty empty.
971
Proof. exact empty_1. Qed.
973
Lemma is_empty_1 : Empty s -> is_empty s = true.
974
Proof. exact (@is_empty_1 s). Qed.
975
Lemma is_empty_2 : is_empty s = true -> Empty s.
976
Proof. exact (@is_empty_2 s). Qed.
978
Lemma add_1 : E.eq x y -> In y (add x s).
979
Proof. wrap add add_in. Qed.
980
Lemma add_2 : In y s -> In y (add x s).
981
Proof. wrap add add_in. Qed.
982
Lemma add_3 : ~ E.eq x y -> In y (add x s) -> In y s.
983
Proof. wrap add add_in. elim H; auto. Qed.
985
Lemma remove_1 : E.eq x y -> ~ In y (remove x s).
986
Proof. wrap remove remove_in. Qed.
987
Lemma remove_2 : ~ E.eq x y -> In y s -> In y (remove x s).
988
Proof. wrap remove remove_in. Qed.
989
Lemma remove_3 : In y (remove x s) -> In y s.
990
Proof. wrap remove remove_in. Qed.
992
Lemma singleton_1 : In y (singleton x) -> E.eq x y.
993
Proof. exact (@singleton_1 x y). Qed.
994
Lemma singleton_2 : E.eq x y -> In y (singleton x).
995
Proof. exact (@singleton_2 x y). Qed.
997
Lemma union_1 : In x (union s s') -> In x s \/ In x s'.
998
Proof. wrap union union_in. Qed.
999
Lemma union_2 : In x s -> In x (union s s').
1000
Proof. wrap union union_in. Qed.
1001
Lemma union_3 : In x s' -> In x (union s s').
1002
Proof. wrap union union_in. Qed.
1004
Lemma ocaml_union_alt : Equal (ocaml_union s s') (union s s').
1006
unfold ocaml_union, union, Equal, In.
1007
destruct s as (s0,b,a); destruct s' as (s0',b',a'); simpl.
1008
exact (@ocaml_union_alt (s0,s0') b a b' a').
1011
Lemma ocaml_union_1 : In x (ocaml_union s s') -> In x s \/ In x s'.
1012
Proof. wrap ocaml_union ocaml_union_in; simpl; auto. Qed.
1013
Lemma ocaml_union_2 : In x s -> In x (ocaml_union s s').
1014
Proof. wrap ocaml_union ocaml_union_in; simpl; auto. Qed.
1015
Lemma ocaml_union_3 : In x s' -> In x (ocaml_union s s').
1016
Proof. wrap ocaml_union ocaml_union_in; simpl; auto. Qed.
1018
Lemma inter_1 : In x (inter s s') -> In x s.
1019
Proof. wrap inter inter_in. Qed.
1020
Lemma inter_2 : In x (inter s s') -> In x s'.
1021
Proof. wrap inter inter_in. Qed.
1022
Lemma inter_3 : In x s -> In x s' -> In x (inter s s').
1023
Proof. wrap inter inter_in. Qed.
1025
Lemma diff_1 : In x (diff s s') -> In x s.
1026
Proof. wrap diff diff_in. Qed.
1027
Lemma diff_2 : In x (diff s s') -> ~ In x s'.
1028
Proof. wrap diff diff_in. Qed.
1029
Lemma diff_3 : In x s -> ~ In x s' -> In x (diff s s').
1030
Proof. wrap diff diff_in. Qed.
1032
Lemma fold_1 : forall (A : Type) (i : A) (f : elt -> A -> A),
1033
fold f s i = fold_left (fun a e => f e a) (elements s) i.
1035
unfold fold, elements; intros; apply fold_1; auto.
1038
Lemma cardinal_1 : cardinal s = length (elements s).
1040
unfold cardinal, elements; intros; apply elements_cardinal; auto.
1044
Variable f : elt -> bool.
1046
Lemma filter_1 : compat_bool E.eq f -> In x (filter f s) -> In x s.
1047
Proof. intro. wrap filter filter_in. Qed.
1048
Lemma filter_2 : compat_bool E.eq f -> In x (filter f s) -> f x = true.
1049
Proof. intro. wrap filter filter_in. Qed.
1050
Lemma filter_3 : compat_bool E.eq f -> In x s -> f x = true -> In x (filter f s).
1051
Proof. intro. wrap filter filter_in. Qed.
1053
Lemma for_all_1 : compat_bool E.eq f -> For_all (fun x => f x = true) s -> for_all f s = true.
1054
Proof. exact (@for_all_1 f s). Qed.
1055
Lemma for_all_2 : compat_bool E.eq f -> for_all f s = true -> For_all (fun x => f x = true) s.
1056
Proof. exact (@for_all_2 f s). Qed.
1058
Lemma exists_1 : compat_bool E.eq f -> Exists (fun x => f x = true) s -> exists_ f s = true.
1059
Proof. exact (@exists_1 f s). Qed.
1060
Lemma exists_2 : compat_bool E.eq f -> exists_ f s = true -> Exists (fun x => f x = true) s.
1061
Proof. exact (@exists_2 f s). Qed.
1063
Lemma partition_1 : compat_bool E.eq f ->
1064
Equal (fst (partition f s)) (filter f s).
1066
unfold partition, filter, Equal, In; simpl ;intros H a.
1067
rewrite partition_in_1, filter_in; intuition.
1070
Lemma partition_2 : compat_bool E.eq f ->
1071
Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
1073
unfold partition, filter, Equal, In; simpl ;intros H a.
1074
rewrite partition_in_2, filter_in; intuition.
1076
destruct (f a); auto.
1077
red; intros; f_equal.
1078
rewrite (H _ _ H0); auto.
1083
Lemma elements_1 : In x s -> InA E.eq x (elements s).
1084
Proof. wrap elements elements_in. Qed.
1085
Lemma elements_2 : InA E.eq x (elements s) -> In x s.
1086
Proof. wrap elements elements_in. Qed.
1087
Lemma elements_3 : sort E.lt (elements s).
1088
Proof. exact (elements_sort (is_bst s)). Qed.
1089
Lemma elements_3w : NoDupA E.eq (elements s).
1090
Proof. exact (elements_nodup (is_bst s)). Qed.
1092
Lemma min_elt_1 : min_elt s = Some x -> In x s.
1093
Proof. exact (@min_elt_1 s x). Qed.
1094
Lemma min_elt_2 : min_elt s = Some x -> In y s -> ~ E.lt y x.
1095
Proof. exact (@min_elt_2 s x y (is_bst s)). Qed.
1096
Lemma min_elt_3 : min_elt s = None -> Empty s.
1097
Proof. exact (@min_elt_3 s). Qed.
1099
Lemma max_elt_1 : max_elt s = Some x -> In x s.
1100
Proof. exact (@max_elt_1 s x). Qed.
1101
Lemma max_elt_2 : max_elt s = Some x -> In y s -> ~ E.lt x y.
1102
Proof. exact (@max_elt_2 s x y (is_bst s)). Qed.
1103
Lemma max_elt_3 : max_elt s = None -> Empty s.
1104
Proof. exact (@max_elt_3 s). Qed.
1106
Lemma choose_1 : choose s = Some x -> In x s.
1107
Proof. exact (@choose_1 s x). Qed.
1108
Lemma choose_2 : choose s = None -> Empty s.
1109
Proof. exact (@choose_2 s). Qed.
1110
Lemma choose_3 : choose s = Some x -> choose s' = Some y ->
1111
Equal s s' -> E.eq x y.
1112
Proof. exact (@choose_3 _ _ (is_bst s) (is_bst s') x y). Qed.
1114
Lemma eq_refl : eq s s.
1115
Proof. exact (eq_refl s). Qed.
1116
Lemma eq_sym : eq s s' -> eq s' s.
1117
Proof. exact (@eq_sym s s'). Qed.
1118
Lemma eq_trans : eq s s' -> eq s' s'' -> eq s s''.
1119
Proof. exact (@eq_trans s s' s''). Qed.
1121
Lemma lt_trans : lt s s' -> lt s' s'' -> lt s s''.
1122
Proof. exact (@lt_trans s s' s''). Qed.
1123
Lemma lt_not_eq : lt s s' -> ~eq s s'.
1124
Proof. exact (@lt_not_eq _ _ (is_bst s) (is_bst s')). Qed.
1129
(* For concrete use inside Coq, we propose an instantiation of [Int] by [Z]. *)
1131
Module Make (X: OrderedType) <: S with Module E := X
1132
:=IntMake(Z_as_Int)(X).
added
removed
theories/FSets/FSetFullAVL.v
