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: FSetAVL.v 11699 2008-12-18 11:49:08Z letouzey $ *)
18
(** This module implements sets using AVL trees.
19
It follows the implementation from Ocaml's standard library,
21
All operations given here expect and produce well-balanced trees
22
(in the ocaml sense: heigths of subtrees shouldn't differ by more
23
than 2), and hence has low complexities (e.g. add is logarithmic
24
in the size of the set). But proving these balancing preservations
25
is in fact not necessary for ensuring correct operational behavior
26
and hence fulfilling the FSet interface. As a consequence,
27
balancing results are not part of this file anymore, they can
28
now be found in [FSetFullAVL].
30
Four operations ([union], [subset], [compare] and [equal]) have
31
been slightly adapted in order to have only structural recursive
32
calls. The precise ocaml versions of these operations have also
33
been formalized (thanks to Function+measure), see [ocaml_union],
34
[ocaml_subset], [ocaml_compare] and [ocaml_equal] in
35
[FSetFullAVL]. The structural variants compute faster in Coq,
36
whereas the other variants produce nicer and/or (slightly) faster
37
code after extraction.
40
Require Import FSetInterface FSetList ZArith Int.
42
Set Implicit Arguments.
43
Unset Strict Implicit.
45
(** Notations and helper lemma about pairs *)
47
Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope.
48
Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope.
52
Functor of pure functions + a posteriori proofs of invariant
55
Module Raw (Import I:Int)(X:OrderedType).
56
Open Local Scope pair_scope.
57
Open Local Scope lazy_bool_scope.
58
Open Local Scope Int_scope.
60
Definition elt := X.t.
64
The fourth field of [Node] is the height of the tree *)
68
| Node : tree -> X.t -> tree -> int -> tree.
72
(** * Basic functions on trees: height and cardinal *)
74
Definition height (s : tree) : int :=
80
Fixpoint cardinal (s : tree) : nat :=
83
| Node l _ r _ => S (cardinal l + cardinal r)
88
Definition empty := Leaf.
90
(** * Emptyness test *)
92
Definition is_empty s :=
93
match s with Leaf => true | _ => false end.
97
(** The [mem] function is deciding appartness. It exploits the
98
binary search tree invariant to achieve logarithmic complexity. *)
103
| Node l y r _ => match X.compare x y with
110
(** * Singleton set *)
112
Definition singleton x := Node Leaf x Leaf 1.
114
(** * Helper functions *)
116
(** [create l x r] creates a node, assuming [l] and [r]
117
to be balanced and [|height l - height r| <= 2]. *)
119
Definition create l x r :=
120
Node l x r (max (height l) (height r) + 1).
122
(** [bal l x r] acts as [create], but performs one step of
123
rebalancing if necessary, i.e. assumes [|height l - height r| <= 3]. *)
125
Definition assert_false := create.
127
Definition bal l x r :=
128
let hl := height l in
129
let hr := height r in
130
if gt_le_dec hl (hr+2) then
132
| Leaf => assert_false l x r
134
if ge_lt_dec (height ll) (height lr) then
135
create ll lx (create lr x r)
138
| Leaf => assert_false l x r
139
| Node lrl lrx lrr _ =>
140
create (create ll lx lrl) lrx (create lrr x r)
144
if gt_le_dec hr (hl+2) then
146
| Leaf => assert_false l x r
148
if ge_lt_dec (height rr) (height rl) then
149
create (create l x rl) rx rr
152
| Leaf => assert_false l x r
153
| Node rll rlx rlr _ =>
154
create (create l x rll) rlx (create rlr rx rr)
162
Fixpoint add x s := match s with
163
| Leaf => Node Leaf x Leaf 1
165
match X.compare x y with
166
| LT _ => bal (add x l) y r
167
| EQ _ => Node l y r h
168
| GT _ => bal l y (add x r)
174
Same as [bal] but does not assume anything regarding heights
178
Fixpoint join l : elt -> t -> t :=
181
| Node ll lx lr lh => fun x =>
182
fix join_aux (r:t) : t := match r with
184
| Node rl rx rr rh =>
185
if gt_le_dec lh (rh+2) then bal ll lx (join lr x r)
186
else if gt_le_dec rh (lh+2) then bal (join_aux rl) rx rr
191
(** * Extraction of minimum element
193
Morally, [remove_min] is to be applied to a non-empty tree
194
[t = Node l x r h]. Since we can't deal here with [assert false]
195
for [t=Leaf], we pre-unpack [t] (and forget about [h]).
198
Fixpoint remove_min l x r : t*elt :=
201
| Node ll lx lr lh =>
202
let (l',m) := remove_min ll lx lr in (bal l' x r, m)
205
(** * Merging two trees
207
[merge t1 t2] builds the union of [t1] and [t2] assuming all elements
208
of [t1] to be smaller than all elements of [t2], and
209
[|height t1 - height t2| <= 2].
212
Definition merge s1 s2 := match s1,s2 with
215
| _, Node l2 x2 r2 h2 =>
216
let (s2',m) := remove_min l2 x2 r2 in bal s1 m s2'
221
Fixpoint remove x s := match s with
224
match X.compare x y with
225
| LT _ => bal (remove x l) y r
227
| GT _ => bal l y (remove x r)
231
(** * Minimum element *)
233
Fixpoint min_elt s := match s with
235
| Node Leaf y _ _ => Some y
236
| Node l _ _ _ => min_elt l
239
(** * Maximum element *)
241
Fixpoint max_elt s := match s with
243
| Node _ y Leaf _ => Some y
244
| Node _ _ r _ => max_elt r
249
Definition choose := min_elt.
253
Same as [merge] but does not assume anything about heights.
256
Definition concat s1 s2 :=
260
| _, Node l2 x2 r2 _ =>
261
let (s2',m) := remove_min l2 x2 r2 in
267
[split x s] returns a triple [(l, present, r)] where
268
- [l] is the set of elements of [s] that are [< x]
269
- [r] is the set of elements of [s] that are [> x]
270
- [present] is [true] if and only if [s] contains [x].
273
Record triple := mktriple { t_left:t; t_in:bool; t_right:t }.
274
Notation "<< l , b , r >>" := (mktriple l b r) (at level 9).
275
Notation "t #l" := (t_left t) (at level 9, format "t '#l'").
276
Notation "t #b" := (t_in t) (at level 9, format "t '#b'").
277
Notation "t #r" := (t_right t) (at level 9, format "t '#r'").
279
Fixpoint split x s : triple := match s with
280
| Leaf => << Leaf, false, Leaf >>
282
match X.compare x y with
283
| LT _ => let (ll,b,rl) := split x l in << ll, b, join rl y r >>
284
| EQ _ => << l, true, r >>
285
| GT _ => let (rl,b,rr) := split x r in << join l y rl, b, rr >>
289
(** * Intersection *)
291
Fixpoint inter s1 s2 := match s1, s2 with
294
| Node l1 x1 r1 h1, _ =>
295
let (l2',pres,r2') := split x1 s2 in
296
if pres then join (inter l1 l2') x1 (inter r1 r2')
297
else concat (inter l1 l2') (inter r1 r2')
302
Fixpoint diff s1 s2 := match s1, s2 with
305
| Node l1 x1 r1 h1, _ =>
306
let (l2',pres,r2') := split x1 s2 in
307
if pres then concat (diff l1 l2') (diff r1 r2')
308
else join (diff l1 l2') x1 (diff r1 r2')
313
(** In ocaml, heights of [s1] and [s2] are compared each time in order
314
to recursively perform the split on the smaller set.
315
Unfortunately, this leads to a non-structural algorithm. The
316
following code is a simplification of the ocaml version: no
317
comparison of heights. It might be slightly slower, but
318
experimentally all the tests I've made in ocaml have shown this
319
potential slowdown to be non-significant. Anyway, the exact code
320
of ocaml has also been formalized thanks to Function+measure, see
321
[ocaml_union] in [FSetFullAVL].
324
Fixpoint union s1 s2 :=
328
| Node l1 x1 r1 h1, _ =>
329
let (l2',_,r2') := split x1 s2 in
330
join (union l1 l2') x1 (union r1 r2')
335
(** [elements_tree_aux acc t] catenates the elements of [t] in infix
336
order to the list [acc] *)
338
Fixpoint elements_aux (acc : list X.t) (t : tree) : list X.t :=
341
| Node l x r _ => elements_aux (x :: elements_aux acc r) l
344
(** then [elements] is an instanciation with an empty [acc] *)
346
Definition elements := elements_aux nil.
350
Fixpoint filter_acc (f:elt->bool) acc s := match s with
353
filter_acc f (filter_acc f (if f x then add x acc else acc) l) r
356
Definition filter f := filter_acc f Leaf.
361
Fixpoint partition_acc (f:elt->bool)(acc : t*t)(s : t) : t*t :=
365
let (acct,accf) := acc in
368
(if f x then (add x acct, accf) else (acct, add x accf)) l) r
371
Definition partition f := partition_acc f (Leaf,Leaf).
373
(** * [for_all] and [exists] *)
375
Fixpoint for_all (f:elt->bool) s := match s with
377
| Node l x r _ => f x &&& for_all f l &&& for_all f r
380
Fixpoint exists_ (f:elt->bool) s := match s with
382
| Node l x r _ => f x ||| exists_ f l ||| exists_ f r
387
Fixpoint fold (A : Type) (f : elt -> A -> A)(s : tree) : A -> A :=
388
fun a => match s with
390
| Node l x r _ => fold f r (f x (fold f l a))
392
Implicit Arguments fold [A].
397
(** In ocaml, recursive calls are made on "half-trees" such as
398
(Node l1 x1 Leaf _) and (Node Leaf x1 r1 _). Instead of these
399
non-structural calls, we propose here two specialized functions for
400
these situations. This version should be almost as efficient as
401
the one of ocaml (closures as arguments may slow things a bit),
402
it is simply less compact. The exact ocaml version has also been
403
formalized (thanks to Function+measure), see [ocaml_subset] in
407
Fixpoint subsetl (subset_l1:t->bool) x1 s2 : bool :=
410
| Node l2 x2 r2 h2 =>
411
match X.compare x1 x2 with
412
| EQ _ => subset_l1 l2
413
| LT _ => subsetl subset_l1 x1 l2
414
| GT _ => mem x1 r2 &&& subset_l1 s2
418
Fixpoint subsetr (subset_r1:t->bool) x1 s2 : bool :=
421
| Node l2 x2 r2 h2 =>
422
match X.compare x1 x2 with
423
| EQ _ => subset_r1 r2
424
| LT _ => mem x1 l2 &&& subset_r1 s2
425
| GT _ => subsetr subset_r1 x1 r2
429
Fixpoint subset s1 s2 : bool := match s1, s2 with
431
| Node _ _ _ _, Leaf => false
432
| Node l1 x1 r1 h1, Node l2 x2 r2 h2 =>
433
match X.compare x1 x2 with
434
| EQ _ => subset l1 l2 &&& subset r1 r2
435
| LT _ => subsetl (subset l1) x1 l2 &&& subset r1 s2
436
| GT _ => subsetr (subset r1) x1 r2 &&& subset l1 s2
440
(** * A new comparison algorithm suggested by Xavier Leroy
442
Transformation in C.P.S. suggested by Benjamin Grégoire.
443
The original ocaml code (with non-structural recursive calls)
444
has also been formalized (thanks to Function+measure), see
445
[ocaml_compare] in [FSetFullAVL]. The following code with
446
continuations computes dramatically faster in Coq, and
447
should be almost as efficient after extraction.
450
(** Enumeration of the elements of a tree *)
452
Inductive enumeration :=
454
| More : elt -> tree -> enumeration -> enumeration.
457
(** [cons t e] adds the elements of tree [t] on the head of
460
Fixpoint cons s e : enumeration :=
463
| Node l x r h => cons l (More x r e)
466
(** One step of comparison of elements *)
468
Definition compare_more x1 (cont:enumeration->comparison) e2 :=
472
match X.compare x1 x2 with
473
| EQ _ => cont (cons r2 e2)
479
(** Comparison of left tree, middle element, then right tree *)
481
Fixpoint compare_cont s1 (cont:enumeration->comparison) e2 :=
485
compare_cont l1 (compare_more x1 (compare_cont r1 cont)) e2
488
(** Initial continuation *)
490
Definition compare_end e2 :=
491
match e2 with End => Eq | _ => Lt end.
493
(** The complete comparison *)
495
Definition compare s1 s2 := compare_cont s1 compare_end (cons s2 End).
497
(** * Equality test *)
499
Definition equal s1 s2 : bool :=
500
match compare s1 s2 with
510
(** ** Occurrence in a tree *)
512
Inductive In (x : elt) : tree -> Prop :=
513
| IsRoot : forall l r h y, X.eq x y -> In x (Node l y r h)
514
| InLeft : forall l r h y, In x l -> In x (Node l y r h)
515
| InRight : forall l r h y, In x r -> In x (Node l y r h).
517
(** ** Binary search trees *)
519
(** [lt_tree x s]: all elements in [s] are smaller than [x]
520
(resp. greater for [gt_tree]) *)
522
Definition lt_tree x s := forall y, In y s -> X.lt y x.
523
Definition gt_tree x s := forall y, In y s -> X.lt x y.
525
(** [bst t] : [t] is a binary search tree *)
527
Inductive bst : tree -> Prop :=
529
| BSNode : forall x l r h, bst l -> bst r ->
530
lt_tree x l -> gt_tree x r -> bst (Node l x r h).
535
(** * Some shortcuts *)
537
Definition Equal s s' := forall a : elt, In a s <-> In a s'.
538
Definition Subset s s' := forall a : elt, In a s -> In a s'.
539
Definition Empty s := forall a : elt, ~ In a s.
540
Definition For_all (P : elt -> Prop) s := forall x, In x s -> P x.
541
Definition Exists (P : elt -> Prop) s := exists x, In x s /\ P x.
545
(** * Correctness proofs, isolated in a sub-module *)
548
Module MX := OrderedTypeFacts X.
549
Module L := FSetList.Raw X.
551
(** * Automation and dedicated tactics *)
553
Hint Constructors In bst.
554
Hint Unfold lt_tree gt_tree.
556
Tactic Notation "factornode" ident(l) ident(x) ident(r) ident(h)
558
set (s:=Node l x r h) in *; clearbody s; clear l x r h.
560
(** A tactic to repeat [inversion_clear] on all hyps of the
561
form [(f (Node _ _ _ _))] *)
565
| H:f Leaf |- _ => inversion_clear H; inv f
566
| H:f _ Leaf |- _ => inversion_clear H; inv f
567
| H:f (Node _ _ _ _) |- _ => inversion_clear H; inv f
568
| H:f _ (Node _ _ _ _) |- _ => inversion_clear H; inv f
572
Ltac intuition_in := repeat progress (intuition; inv In).
574
(** Helper tactic concerning order of elements. *)
576
Ltac order := match goal with
577
| U: lt_tree _ ?s, V: In _ ?s |- _ => generalize (U _ V); clear U; order
578
| U: gt_tree _ ?s, V: In _ ?s |- _ => generalize (U _ V); clear U; order
583
(** * Basic results about [In], [lt_tree], [gt_tree], [height] *)
585
(** [In] is compatible with [X.eq] *)
588
forall s x y, X.eq x y -> In x s -> In y s.
590
induction s; simpl; intuition_in; eauto.
596
In y (Node l x r h) <-> In y l \/ X.eq y x \/ In y r.
601
(** Results about [lt_tree] and [gt_tree] *)
603
Lemma lt_leaf : forall x : elt, lt_tree x Leaf.
608
Lemma gt_leaf : forall x : elt, gt_tree x Leaf.
614
forall (x y : elt) (l r : tree) (h : int),
615
lt_tree x l -> lt_tree x r -> X.lt y x -> lt_tree x (Node l y r h).
617
unfold lt_tree; intuition_in; order.
621
forall (x y : elt) (l r : tree) (h : int),
622
gt_tree x l -> gt_tree x r -> X.lt x y -> gt_tree x (Node l y r h).
624
unfold gt_tree; intuition_in; order.
627
Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node.
629
Lemma lt_tree_not_in :
630
forall (x : elt) (t : tree), lt_tree x t -> ~ In x t.
632
intros; intro; order.
635
Lemma lt_tree_trans :
636
forall x y, X.lt x y -> forall t, lt_tree x t -> lt_tree y t.
641
Lemma gt_tree_not_in :
642
forall (x : elt) (t : tree), gt_tree x t -> ~ In x t.
644
intros; intro; order.
647
Lemma gt_tree_trans :
648
forall x y, X.lt y x -> forall t, gt_tree x t -> gt_tree y t.
653
Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans.
655
(** * Inductions principles *)
657
Functional Scheme mem_ind := Induction for mem Sort Prop.
658
Functional Scheme bal_ind := Induction for bal Sort Prop.
659
Functional Scheme add_ind := Induction for add Sort Prop.
660
Functional Scheme remove_min_ind := Induction for remove_min Sort Prop.
661
Functional Scheme merge_ind := Induction for merge Sort Prop.
662
Functional Scheme remove_ind := Induction for remove Sort Prop.
663
Functional Scheme min_elt_ind := Induction for min_elt Sort Prop.
664
Functional Scheme max_elt_ind := Induction for max_elt Sort Prop.
665
Functional Scheme concat_ind := Induction for concat Sort Prop.
666
Functional Scheme split_ind := Induction for split Sort Prop.
667
Functional Scheme inter_ind := Induction for inter Sort Prop.
668
Functional Scheme diff_ind := Induction for diff Sort Prop.
669
Functional Scheme union_ind := Induction for union Sort Prop.
674
Lemma empty_1 : Empty empty.
680
Lemma empty_bst : bst empty.
685
(** * Emptyness test *)
687
Lemma is_empty_1 : forall s, Empty s -> is_empty s = true.
689
destruct s as [|r x l h]; simpl; auto.
690
intro H; elim (H x); auto.
693
Lemma is_empty_2 : forall s, is_empty s = true -> Empty s.
695
destruct s; simpl; intros; try discriminate; red; auto.
702
Lemma mem_1 : forall s x, bst s -> In x s -> mem x s = true.
704
intros s x; functional induction mem x s; auto; intros; try clear e0;
705
inv bst; intuition_in; order.
708
Lemma mem_2 : forall s x, mem x s = true -> In x s.
710
intros s x; functional induction mem x s; auto; intros; discriminate.
715
(** * Singleton set *)
717
Lemma singleton_1 : forall x y, In y (singleton x) -> X.eq x y.
719
unfold singleton; intros; inv In; order.
722
Lemma singleton_2 : forall x y, X.eq x y -> In y (singleton x).
724
unfold singleton; auto.
727
Lemma singleton_bst : forall x : elt, bst (singleton x).
729
unfold singleton; auto.
734
(** * Helper functions *)
737
forall l x r y, In y (create l x r) <-> X.eq y x \/ In y l \/ In y r.
739
unfold create; split; [ inversion_clear 1 | ]; intuition.
743
forall l x r, bst l -> bst r -> lt_tree x l -> gt_tree x r ->
748
Hint Resolve create_bst.
750
Lemma bal_in : forall l x r y,
751
In y (bal l x r) <-> X.eq y x \/ In y l \/ In y r.
753
intros l x r; functional induction bal l x r; intros; try clear e0;
754
rewrite !create_in; intuition_in.
757
Lemma bal_bst : forall l x r, bst l -> bst r ->
758
lt_tree x l -> gt_tree x r -> bst (bal l x r).
760
intros l x r; functional induction bal l x r; intros;
761
inv bst; repeat apply create_bst; auto; unfold create;
762
(apply lt_tree_node || apply gt_tree_node); auto;
763
(eapply lt_tree_trans || eapply gt_tree_trans); eauto.
765
Hint Resolve bal_bst.
771
Lemma add_in : forall s x y,
772
In y (add x s) <-> X.eq y x \/ In y s.
774
intros s x; functional induction (add x s); auto; intros;
775
try rewrite bal_in, IHt; intuition_in.
779
Lemma add_bst : forall s x, bst s -> bst (add x s).
781
intros s x; functional induction (add x s); auto; intros;
782
inv bst; apply bal_bst; auto.
783
(* lt_tree -> lt_tree (add ...) *)
789
inv bst; auto using bal_bst.
790
(* gt_tree -> gt_tree (add ...) *)
795
apply MX.lt_eq with x; auto.
797
Hint Resolve add_bst.
803
(* Function/Functional Scheme can't deal with internal fix.
804
Let's do its job by hand: *)
807
intro l; induction l as [| ll _ lx lr Hlr lh];
808
[ | intros x r; induction r as [| rl Hrl rx rr _ rh]; unfold join;
809
[ | destruct (gt_le_dec lh (rh+2));
810
[ match goal with |- context b [ bal ?a ?b ?c] =>
812
with (bal ll lx (join lr x (Node rl rx rr rh))); [ | auto]
814
| destruct (gt_le_dec rh (lh+2));
815
[ match goal with |- context b [ bal ?a ?b ?c] =>
817
with (bal (join (Node ll lx lr lh) x rl) rx rr); [ | auto]
821
Lemma join_in : forall l x r y,
822
In y (join l x r) <-> X.eq y x \/ In y l \/ In y r.
826
rewrite add_in; intuition_in.
827
rewrite add_in; intuition_in.
828
rewrite bal_in, Hlr; clear Hlr Hrl; intuition_in.
829
rewrite bal_in, Hrl; clear Hlr Hrl; intuition_in.
833
Lemma join_bst : forall l x r, bst l -> bst r ->
834
lt_tree x l -> gt_tree x r -> bst (join l x r).
836
join_tac; auto; inv bst; apply bal_bst; auto;
837
clear Hrl Hlr z; intro; intros; rewrite join_in in *.
838
intuition; [ apply MX.lt_eq with x | ]; eauto.
839
intuition; [ apply MX.eq_lt with x | ]; eauto.
841
Hint Resolve join_bst.
845
(** * Extraction of minimum element *)
847
Lemma remove_min_in : forall l x r h y,
848
In y (Node l x r h) <->
849
X.eq y (remove_min l x r)#2 \/ In y (remove_min l x r)#1.
851
intros l x r; functional induction (remove_min l x r); simpl in *; intros.
853
rewrite bal_in, In_node_iff, IHp, e0; simpl; intuition.
856
Lemma remove_min_bst : forall l x r h,
857
bst (Node l x r h) -> bst (remove_min l x r)#1.
859
intros l x r; functional induction (remove_min l x r); simpl; intros.
862
specialize IHp with (1:=H0); rewrite e0 in IHp; auto.
864
intro y; specialize (H2 y).
865
rewrite remove_min_in, e0 in H2; simpl in H2; intuition.
868
Lemma remove_min_gt_tree : forall l x r h,
869
bst (Node l x r h) ->
870
gt_tree (remove_min l x r)#2 (remove_min l x r)#1.
872
intros l x r; functional induction (remove_min l x r); simpl; intros.
875
specialize IHp with (1:=H0); rewrite e0 in IHp; simpl in IHp.
876
intro y; rewrite bal_in; intuition;
877
specialize (H2 m); rewrite remove_min_in, e0 in H2; simpl in H2;
878
[ apply MX.lt_eq with x | ]; eauto.
880
Hint Resolve remove_min_bst remove_min_gt_tree.
884
(** * Merging two trees *)
886
Lemma merge_in : forall s1 s2 y,
887
In y (merge s1 s2) <-> In y s1 \/ In y s2.
889
intros s1 s2; functional induction (merge s1 s2); intros;
890
try factornode _x _x0 _x1 _x2 as s1.
893
rewrite bal_in, remove_min_in, e1; simpl; intuition.
896
Lemma merge_bst : forall s1 s2, bst s1 -> bst s2 ->
897
(forall y1 y2 : elt, In y1 s1 -> In y2 s2 -> X.lt y1 y2) ->
900
intros s1 s2; functional induction (merge s1 s2); intros; auto;
901
try factornode _x _x0 _x1 _x2 as s1.
903
change s2' with ((s2',m)#1); rewrite <-e1; eauto.
906
rewrite remove_min_in, e1; simpl; auto.
907
change (gt_tree (s2',m)#2 (s2',m)#1); rewrite <-e1; eauto.
909
Hint Resolve merge_bst.
915
Lemma remove_in : forall s x y, bst s ->
916
(In y (remove x s) <-> ~ X.eq y x /\ In y s).
918
intros s x; functional induction (remove x s); intros; inv bst.
920
rewrite bal_in, IHt; clear e0 IHt; intuition; [order|order|intuition_in].
921
rewrite merge_in; clear e0; intuition; [order|order|intuition_in].
923
rewrite bal_in, IHt; clear e0 IHt; intuition; [order|order|intuition_in].
926
Lemma remove_bst : forall s x, bst s -> bst (remove x s).
928
intros s x; functional induction (remove x s); intros; inv bst.
932
intro z; rewrite remove_in; auto; destruct 1; eauto.
937
intro z; rewrite remove_in; auto; destruct 1; eauto.
939
Hint Resolve remove_bst.
942
(** * Minimum element *)
944
Lemma min_elt_1 : forall s x, min_elt s = Some x -> In x s.
946
intro s; functional induction (min_elt s); auto; inversion 1; auto.
949
Lemma min_elt_2 : forall s x y, bst s ->
950
min_elt s = Some x -> In y s -> ~ X.lt y x.
952
intro s; functional induction (min_elt s);
953
try rename _x1 into l1, _x2 into x1, _x3 into r1, _x4 into h1.
957
inversion_clear 1; auto.
963
assert (X.lt x y) by (apply H2; auto).
964
inversion_clear 1; auto; order.
965
assert (X.lt x1 y) by auto.
966
inversion_clear 2; auto;
967
(assert (~ X.lt x1 x) by auto); order.
970
Lemma min_elt_3 : forall s, min_elt s = None -> Empty s.
972
intro s; functional induction (min_elt s).
973
red; red; inversion 2.
976
destruct (IHo H0 _x2); auto.
981
(** * Maximum element *)
983
Lemma max_elt_1 : forall s x, max_elt s = Some x -> In x s.
985
intro s; functional induction (max_elt s); auto; inversion 1; auto.
988
Lemma max_elt_2 : forall s x y, bst s ->
989
max_elt s = Some x -> In y s -> ~ X.lt x y.
991
intro s; functional induction (max_elt s);
992
try rename _x1 into l1, _x2 into x1, _x3 into r1, _x4 into h1.
996
inversion_clear 1; auto.
999
assert (X.lt y x1) by auto.
1000
inversion_clear 2; auto;
1001
(assert (~ X.lt x x1) by auto); order.
1004
Lemma max_elt_3 : forall s, max_elt s = None -> Empty s.
1006
intro s; functional induction (max_elt s).
1009
intros H0; destruct (IHo H0 _x2); auto.
1014
(** * Any element *)
1016
Lemma choose_1 : forall s x, choose s = Some x -> In x s.
1021
Lemma choose_2 : forall s, choose s = None -> Empty s.
1026
Lemma choose_3 : forall s s', bst s -> bst s' ->
1027
forall x x', choose s = Some x -> choose s' = Some x' ->
1028
Equal s s' -> X.eq x x'.
1030
unfold choose, Equal; intros s s' Hb Hb' x x' Hx Hx' H.
1031
assert (~X.lt x x').
1032
apply min_elt_2 with s'; auto.
1033
rewrite <-H; auto using min_elt_1.
1034
assert (~X.lt x' x).
1035
apply min_elt_2 with s; auto.
1036
rewrite H; auto using min_elt_1.
1037
destruct (X.compare x x'); intuition.
1041
(** * Concatenation *)
1043
Lemma concat_in : forall s1 s2 y,
1044
In y (concat s1 s2) <-> In y s1 \/ In y s2.
1046
intros s1 s2; functional induction (concat s1 s2); intros;
1047
try factornode _x _x0 _x1 _x2 as s1.
1050
rewrite join_in, remove_min_in, e1; simpl; intuition.
1053
Lemma concat_bst : forall s1 s2, bst s1 -> bst s2 ->
1054
(forall y1 y2 : elt, In y1 s1 -> In y2 s2 -> X.lt y1 y2) ->
1057
intros s1 s2; functional induction (concat s1 s2); intros; auto;
1058
try factornode _x _x0 _x1 _x2 as s1.
1059
apply join_bst; auto.
1060
change (bst (s2',m)#1); rewrite <-e1; eauto.
1063
rewrite remove_min_in, e1; simpl; auto.
1064
change (gt_tree (s2',m)#2 (s2',m)#1); rewrite <-e1; eauto.
1066
Hint Resolve concat_bst.
1071
Lemma split_in_1 : forall s x y, bst s ->
1072
(In y (split x s)#l <-> In y s /\ X.lt y x).
1074
intros s x; functional induction (split x s); simpl; intros;
1075
inv bst; try clear e0.
1077
rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order.
1078
intuition_in; order.
1080
rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order.
1083
Lemma split_in_2 : forall s x y, bst s ->
1084
(In y (split x s)#r <-> In y s /\ X.lt x y).
1086
intros s x; functional induction (split x s); subst; simpl; intros;
1087
inv bst; try clear e0.
1090
rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order.
1091
intuition_in; order.
1092
rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order.
1095
Lemma split_in_3 : forall s x, bst s ->
1096
((split x s)#b = true <-> In x s).
1098
intros s x; functional induction (split x s); subst; simpl; intros;
1099
inv bst; try clear e0.
1100
intuition_in; try discriminate.
1101
rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order.
1103
rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order.
1106
Lemma split_bst : forall s x, bst s ->
1107
bst (split x s)#l /\ bst (split x s)#r.
1109
intros s x; functional induction (split x s); subst; simpl; intros;
1110
inv bst; try clear e0; try rewrite e1 in *; simpl in *; intuition;
1111
apply join_bst; auto.
1113
generalize (split_in_2 x y0 H0); rewrite e1; simpl; intuition.
1115
generalize (split_in_1 x y0 H1); rewrite e1; simpl; intuition.
1120
(** * Intersection *)
1122
Lemma inter_bst_in : forall s1 s2, bst s1 -> bst s2 ->
1123
bst (inter s1 s2) /\ (forall y, In y (inter s1 s2) <-> In y s1 /\ In y s2).
1125
intros s1 s2; functional induction inter s1 s2; intros B1 B2;
1126
[intuition_in|intuition_in | | ];
1127
factornode _x0 _x1 _x2 _x3 as s2;
1128
generalize (split_bst x1 B2);
1129
rewrite e1; simpl; destruct 1; inv bst;
1130
destruct IHt as (IHb1,IHi1); auto;
1131
destruct IHt0 as (IHb2,IHi2); auto;
1132
generalize (@split_in_1 s2 x1)(@split_in_2 s2 x1)
1133
(split_in_3 x1 B2)(split_bst x1 B2);
1134
rewrite e1; simpl; split; intros.
1136
apply join_bst; auto; intro y; [rewrite IHi1|rewrite IHi2]; intuition. (* In join *)
1137
rewrite join_in, IHi1, IHi2, H5, H6; intuition_in.
1138
apply In_1 with x1; auto.
1140
apply concat_bst; auto; intros y1 y2; rewrite IHi1, IHi2; intuition; order.
1142
rewrite concat_in, IHi1, IHi2, H5, H6; auto.
1143
assert (~In x1 s2) by (rewrite <- H7; auto).
1146
apply In_1 with y; auto.
1149
Lemma inter_in : forall s1 s2 y, bst s1 -> bst s2 ->
1150
(In y (inter s1 s2) <-> In y s1 /\ In y s2).
1152
intros s1 s2 y B1 B2; destruct (inter_bst_in B1 B2); auto.
1155
Lemma inter_bst : forall s1 s2, bst s1 -> bst s2 -> bst (inter s1 s2).
1157
intros s1 s2 B1 B2; destruct (inter_bst_in B1 B2); auto.
1163
Lemma diff_bst_in : forall s1 s2, bst s1 -> bst s2 ->
1164
bst (diff s1 s2) /\ (forall y, In y (diff s1 s2) <-> In y s1 /\ ~In y s2).
1166
intros s1 s2; functional induction diff s1 s2; intros B1 B2;
1167
[intuition_in|intuition_in | | ];
1168
factornode _x0 _x1 _x2 _x3 as s2;
1169
generalize (split_bst x1 B2);
1170
rewrite e1; simpl; destruct 1;
1172
destruct IHt as (IHb1,IHi1); auto;
1173
destruct IHt0 as (IHb2,IHi2); auto;
1174
generalize (@split_in_1 s2 x1)(@split_in_2 s2 x1)
1175
(split_in_3 x1 B2)(split_bst x1 B2);
1176
rewrite e1; simpl; split; intros.
1178
apply concat_bst; auto; intros y1 y2; rewrite IHi1, IHi2; intuition; order.
1180
rewrite concat_in, IHi1, IHi2, H5, H6; intuition_in.
1182
apply In_1 with x1; auto.
1184
apply join_bst; auto; intro y; [rewrite IHi1|rewrite IHi2]; intuition. (* In join *)
1185
rewrite join_in, IHi1, IHi2, H5, H6; auto.
1186
assert (~In x1 s2) by (rewrite <- H7; auto).
1189
apply In_1 with y; auto.
1192
Lemma diff_in : forall s1 s2 y, bst s1 -> bst s2 ->
1193
(In y (diff s1 s2) <-> In y s1 /\ ~In y s2).
1195
intros s1 s2 y B1 B2; destruct (diff_bst_in B1 B2); auto.
1198
Lemma diff_bst : forall s1 s2, bst s1 -> bst s2 -> bst (diff s1 s2).
1200
intros s1 s2 B1 B2; destruct (diff_bst_in B1 B2); auto.
1206
Lemma union_in : forall s1 s2 y, bst s1 -> bst s2 ->
1207
(In y (union s1 s2) <-> In y s1 \/ In y s2).
1209
intros s1 s2; functional induction union s1 s2; intros y B1 B2.
1212
factornode _x0 _x1 _x2 _x3 as s2.
1213
generalize (split_in_1 x1 y B2)(split_in_2 x1 y B2)(split_bst x1 B2).
1215
destruct 3; inv bst.
1216
rewrite join_in, IHt, IHt0, H, H0; auto.
1217
case (X.compare y x1); intuition_in.
1220
Lemma union_bst : forall s1 s2, bst s1 -> bst s2 ->
1223
intros s1 s2; functional induction union s1 s2; intros B1 B2; auto.
1224
factornode _x0 _x1 _x2 _x3 as s2.
1225
generalize (@split_in_1 s2 x1)(@split_in_2 s2 x1)(split_bst x1 B2).
1226
rewrite e1; simpl; destruct 3.
1228
apply join_bst; auto.
1229
intro y; rewrite union_in, H; intuition_in.
1230
intro y; rewrite union_in, H0; intuition_in.
1236
Lemma elements_aux_in : forall s acc x,
1237
InA X.eq x (elements_aux acc s) <-> In x s \/ InA X.eq x acc.
1239
induction s as [ | l Hl x r Hr h ]; simpl; auto.
1244
destruct (Hr acc x0); clear Hl Hr.
1245
intuition; inversion_clear H3; intuition.
1248
Lemma elements_in : forall s x, InA X.eq x (elements s) <-> In x s.
1250
intros; generalize (elements_aux_in s nil x); intuition.
1254
Lemma elements_aux_sort : forall s acc, bst s -> sort X.lt acc ->
1255
(forall x y : elt, InA X.eq x acc -> In y s -> X.lt y x) ->
1256
sort X.lt (elements_aux acc s).
1258
induction s as [ | l Hl y r Hr h]; simpl; intuition.
1263
apply MX.In_Inf; intros.
1264
destruct (elements_aux_in r acc y0); intuition.
1268
destruct (elements_aux_in r acc x); intuition eauto.
1271
Lemma elements_sort : forall s : tree, bst s -> sort X.lt (elements s).
1273
intros; unfold elements; apply elements_aux_sort; auto.
1274
intros; inversion H0.
1276
Hint Resolve elements_sort.
1278
Lemma elements_nodup : forall s : tree, bst s -> NoDupA X.eq (elements s).
1283
Lemma elements_aux_cardinal :
1284
forall s acc, (length acc + cardinal s)%nat = length (elements_aux acc s).
1286
simple induction s; simpl in |- *; intuition.
1289
rewrite <- H0; omega.
1292
Lemma elements_cardinal : forall s : tree, cardinal s = length (elements s).
1294
exact (fun s => elements_aux_cardinal s nil).
1297
Lemma elements_app :
1298
forall s acc, elements_aux acc s = elements s ++ acc.
1300
induction s; simpl; intros; auto.
1302
unfold elements; simpl.
1303
rewrite 2 IHs1, IHs2, <- !app_nil_end, !app_ass; auto.
1306
Lemma elements_node :
1308
elements l ++ x :: elements r ++ acc =
1309
elements (Node l x r h) ++ acc.
1311
unfold elements; simpl; intros; auto.
1312
rewrite !elements_app, <- !app_nil_end, !app_ass; auto.
1319
Variable f : elt -> bool.
1321
Lemma filter_acc_in : forall s acc,
1322
compat_bool X.eq f -> forall x : elt,
1323
In x (filter_acc f acc s) <-> In x acc \/ In x s /\ f x = true.
1325
induction s; simpl; intros.
1327
rewrite IHs2, IHs1 by (destruct (f t); auto).
1328
case_eq (f t); intros.
1329
rewrite (add_in); auto.
1334
rewrite (H _ _ H2) in H3.
1335
rewrite H0 in H3; discriminate.
1338
Lemma filter_acc_bst : forall s acc, bst s -> bst acc ->
1339
bst (filter_acc f acc s).
1341
induction s; simpl; auto.
1344
destruct (f t); auto.
1347
Lemma filter_in : forall s,
1348
compat_bool X.eq f -> forall x : elt,
1349
In x (filter f s) <-> In x s /\ f x = true.
1351
unfold filter; intros; rewrite filter_acc_in; intuition_in.
1354
Lemma filter_bst : forall s, bst s -> bst (filter f s).
1356
unfold filter; intros; apply filter_acc_bst; auto.
1363
Lemma partition_acc_in_1 : forall s acc,
1364
compat_bool X.eq f -> forall x : elt,
1365
In x (partition_acc f acc s)#1 <->
1366
In x acc#1 \/ In x s /\ f x = true.
1368
induction s; simpl; intros.
1370
destruct acc as [acct accf]; simpl in *.
1372
(destruct (f t); auto; apply partition_acc_avl_1; simpl; auto).
1373
rewrite IHs1 by (destruct (f t); simpl; auto).
1374
case_eq (f t); simpl; intros.
1375
rewrite (add_in); auto.
1380
rewrite (H _ _ H2) in H3.
1381
rewrite H0 in H3; discriminate.
1384
Lemma partition_acc_in_2 : forall s acc,
1385
compat_bool X.eq f -> forall x : elt,
1386
In x (partition_acc f acc s)#2 <->
1387
In x acc#2 \/ In x s /\ f x = false.
1389
induction s; simpl; intros.
1391
destruct acc as [acct accf]; simpl in *.
1393
(destruct (f t); auto; apply partition_acc_avl_2; simpl; auto).
1394
rewrite IHs1 by (destruct (f t); simpl; auto).
1395
case_eq (f t); simpl; intros.
1398
rewrite (H _ _ H2) in H3.
1399
rewrite H0 in H3; discriminate.
1400
rewrite (add_in); auto.
1406
Lemma partition_in_1 : forall s,
1407
compat_bool X.eq f -> forall x : elt,
1408
In x (partition f s)#1 <-> In x s /\ f x = true.
1410
unfold partition; intros; rewrite partition_acc_in_1;
1411
simpl in *; intuition_in.
1414
Lemma partition_in_2 : forall s,
1415
compat_bool X.eq f -> forall x : elt,
1416
In x (partition f s)#2 <-> In x s /\ f x = false.
1418
unfold partition; intros; rewrite partition_acc_in_2;
1419
simpl in *; intuition_in.
1422
Lemma partition_acc_bst_1 : forall s acc, bst s -> bst acc#1 ->
1423
bst (partition_acc f acc s)#1.
1425
induction s; simpl; auto.
1426
destruct acc as [acct accf]; simpl in *.
1429
destruct (f t); auto.
1430
apply IHs2; simpl; auto.
1431
apply IHs1; simpl; auto.
1434
Lemma partition_acc_bst_2 : forall s acc, bst s -> bst acc#2 ->
1435
bst (partition_acc f acc s)#2.
1437
induction s; simpl; auto.
1438
destruct acc as [acct accf]; simpl in *.
1441
destruct (f t); auto.
1442
apply IHs2; simpl; auto.
1443
apply IHs1; simpl; auto.
1446
Lemma partition_bst_1 : forall s, bst s -> bst (partition f s)#1.
1448
unfold partition; intros; apply partition_acc_bst_1; auto.
1451
Lemma partition_bst_2 : forall s, bst s -> bst (partition f s)#2.
1453
unfold partition; intros; apply partition_acc_bst_2; auto.
1458
(** * [for_all] and [exists] *)
1460
Lemma for_all_1 : forall s, compat_bool X.eq f ->
1461
For_all (fun x => f x = true) s -> for_all f s = true.
1463
induction s; simpl; auto.
1465
rewrite IHs1; try red; auto.
1466
rewrite IHs2; try red; auto.
1468
destruct (f t); simpl; auto.
1471
Lemma for_all_2 : forall s, compat_bool X.eq f ->
1472
for_all f s = true -> For_all (fun x => f x = true) s.
1474
induction s; simpl; auto; intros; red; intros; inv In.
1475
destruct (andb_prop _ _ H0); auto.
1476
destruct (andb_prop _ _ H1); eauto.
1478
destruct (andb_prop _ _ H0); auto.
1479
destruct (andb_prop _ _ H1); auto.
1481
destruct (andb_prop _ _ H0); auto.
1484
Lemma exists_1 : forall s, compat_bool X.eq f ->
1485
Exists (fun x => f x = true) s -> exists_ f s = true.
1487
induction s; simpl; destruct 2 as (x,(U,V)); inv In; rewrite <- ?orb_lazy_alt.
1488
rewrite (H _ _ (X.eq_sym H0)); rewrite V; auto.
1489
apply orb_true_intro; left.
1490
apply orb_true_intro; right; apply IHs1; auto; exists x; auto.
1491
apply orb_true_intro; right; apply IHs2; auto; exists x; auto.
1494
Lemma exists_2 : forall s, compat_bool X.eq f ->
1495
exists_ f s = true -> Exists (fun x => f x = true) s.
1497
induction s; simpl; intros; rewrite <- ?orb_lazy_alt in *.
1499
destruct (orb_true_elim _ _ H0) as [H1|H1].
1500
destruct (orb_true_elim _ _ H1) as [H2|H2].
1502
destruct (IHs1 H H2); auto; exists x; intuition.
1503
destruct (IHs2 H H1); auto; exists x; intuition.
1512
Definition fold' (A : Type) (f : elt -> A -> A)(s : tree) :=
1513
L.fold f (elements s).
1514
Implicit Arguments fold' [A].
1516
Lemma fold_equiv_aux :
1517
forall (A : Type) (s : tree) (f : elt -> A -> A) (a : A) (acc : list elt),
1518
L.fold f (elements_aux acc s) a = L.fold f acc (fold f s a).
1521
simpl in |- *; intuition.
1522
simpl in |- *; intros.
1529
forall (A : Type) (s : tree) (f : elt -> A -> A) (a : A),
1530
fold f s a = fold' f s a.
1532
unfold fold', elements in |- *.
1533
simple induction s; simpl in |- *; auto; intros.
1534
rewrite fold_equiv_aux.
1536
simpl in |- *; auto.
1540
forall (s:t)(Hs:bst s)(A : Type)(f : elt -> A -> A)(i : A),
1541
fold f s i = fold_left (fun a e => f e a) (elements s) i.
1547
unfold L.elements; auto.
1548
apply elements_sort; auto.
1553
Lemma subsetl_12 : forall subset_l1 l1 x1 h1 s2,
1554
bst (Node l1 x1 Leaf h1) -> bst s2 ->
1555
(forall s, bst s -> (subset_l1 s = true <-> Subset l1 s)) ->
1556
(subsetl subset_l1 x1 s2 = true <-> Subset (Node l1 x1 Leaf h1) s2 ).
1558
induction s2 as [|l2 IHl2 x2 r2 IHr2 h2]; simpl; intros.
1559
unfold Subset; intuition; try discriminate.
1560
assert (H': In x1 Leaf) by auto; inversion H'.
1562
specialize (IHl2 H H2 H1).
1563
specialize (IHr2 H H3 H1).
1567
rewrite IHl2; clear H1 IHl2 IHr2.
1568
unfold Subset. intuition_in.
1569
assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
1570
assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
1572
rewrite H1 by auto; clear H1 IHl2 IHr2.
1573
unfold Subset. intuition_in.
1574
assert (X.eq a x2) by order; intuition_in.
1575
assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
1577
rewrite <-andb_lazy_alt, andb_true_iff, H1 by auto; clear H1 IHl2 IHr2.
1578
unfold Subset. intuition_in.
1579
assert (H':=mem_2 H6); apply In_1 with x1; auto.
1581
assert (In x1 (Node l2 x2 r2 h2)) by auto; intuition_in; order.
1585
Lemma subsetr_12 : forall subset_r1 r1 x1 h1 s2,
1586
bst (Node Leaf x1 r1 h1) -> bst s2 ->
1587
(forall s, bst s -> (subset_r1 s = true <-> Subset r1 s)) ->
1588
(subsetr subset_r1 x1 s2 = true <-> Subset (Node Leaf x1 r1 h1) s2).
1590
induction s2 as [|l2 IHl2 x2 r2 IHr2 h2]; simpl; intros.
1591
unfold Subset; intuition; try discriminate.
1592
assert (H': In x1 Leaf) by auto; inversion H'.
1594
specialize (IHl2 H H2 H1).
1595
specialize (IHr2 H H3 H1).
1599
rewrite <-andb_lazy_alt, andb_true_iff, H1 by auto; clear H1 IHl2 IHr2.
1600
unfold Subset. intuition_in.
1601
assert (H':=mem_2 H1); apply In_1 with x1; auto.
1603
assert (In x1 (Node l2 x2 r2 h2)) by auto; intuition_in; order.
1605
rewrite H1 by auto; clear H1 IHl2 IHr2.
1606
unfold Subset. intuition_in.
1607
assert (X.eq a x2) by order; intuition_in.
1608
assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
1610
rewrite IHr2; clear H1 IHl2 IHr2.
1611
unfold Subset. intuition_in.
1612
assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
1613
assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
1617
Lemma subset_12 : forall s1 s2, bst s1 -> bst s2 ->
1618
(subset s1 s2 = true <-> Subset s1 s2).
1620
induction s1 as [|l1 IHl1 x1 r1 IHr1 h1]; simpl; intros.
1621
unfold Subset; intuition_in.
1622
destruct s2 as [|l2 x2 r2 h2]; simpl; intros.
1623
unfold Subset; intuition_in; try discriminate.
1624
assert (H': In x1 Leaf) by auto; inversion H'.
1628
rewrite <-andb_lazy_alt, andb_true_iff, IHr1 by auto.
1629
rewrite (@subsetl_12 (subset l1) l1 x1 h1) by auto.
1631
unfold Subset; intuition_in.
1632
assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
1633
assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
1635
rewrite <-andb_lazy_alt, andb_true_iff, IHl1, IHr1 by auto.
1637
unfold Subset; intuition_in.
1638
assert (X.eq a x2) by order; intuition_in.
1639
assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
1640
assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
1642
rewrite <-andb_lazy_alt, andb_true_iff, IHl1 by auto.
1643
rewrite (@subsetr_12 (subset r1) r1 x1 h1) by auto.
1645
unfold Subset; intuition_in.
1646
assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
1647
assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
1654
(** ** Relations [eq] and [lt] over trees *)
1656
Definition eq := Equal.
1657
Definition lt (s1 s2 : t) : Prop := L.lt (elements s1) (elements s2).
1659
Lemma eq_refl : forall s : t, Equal s s.
1661
unfold Equal; intuition.
1664
Lemma eq_sym : forall s s' : t, Equal s s' -> Equal s' s.
1666
unfold Equal; intros s s' H x; destruct (H x); split; auto.
1669
Lemma eq_trans : forall s s' s'' : t,
1670
Equal s s' -> Equal s' s'' -> Equal s s''.
1672
unfold Equal; intros s s' s'' H1 H2 x;
1673
destruct (H1 x); destruct (H2 x); split; auto.
1677
forall s s' : t, Equal s s' -> L.eq (elements s) (elements s').
1679
unfold Equal, L.eq, L.Equal; intros; do 2 rewrite elements_in; auto.
1683
forall s s' : t, L.eq (elements s) (elements s') -> Equal s s'.
1685
unfold Equal, L.eq, L.Equal; intros; do 2 rewrite <-elements_in; auto.
1687
Hint Resolve eq_L_eq L_eq_eq.
1689
Definition lt_trans (s s' s'' : t) (h : lt s s')
1690
(h' : lt s' s'') : lt s s'' := L.lt_trans h h'.
1692
Lemma lt_not_eq : forall s s' : t,
1693
bst s -> bst s' -> lt s s' -> ~ Equal s s'.
1695
unfold lt in |- *; intros; intro.
1696
apply L.lt_not_eq with (s := elements s) (s' := elements s'); auto.
1700
forall (l1 l2 : list elt) (x y : elt),
1701
X.eq x y -> L.eq l1 l2 -> L.eq (x :: l1) (y :: l2).
1703
unfold L.eq, L.Equal in |- *; intuition.
1704
inversion_clear H1; generalize (H0 a); clear H0; intuition.
1705
apply InA_eqA with x; eauto.
1706
inversion_clear H1; generalize (H0 a); clear H0; intuition.
1707
apply InA_eqA with y; eauto.
1709
Hint Resolve L_eq_cons.
1712
(** * A new comparison algorithm suggested by Xavier Leroy *)
1714
(** [flatten_e e] returns the list of elements of [e] i.e. the list
1715
of elements actually compared *)
1717
Fixpoint flatten_e (e : enumeration) : list elt := match e with
1719
| More x t r => x :: elements t ++ flatten_e r
1722
Lemma flatten_e_elements :
1724
elements l ++ flatten_e (More x r e) = elements (Node l x r h) ++ flatten_e e.
1726
intros; simpl; apply elements_node.
1729
Lemma cons_1 : forall s e,
1730
flatten_e (cons s e) = elements s ++ flatten_e e.
1732
induction s; simpl; auto; intros.
1733
rewrite IHs1; apply flatten_e_elements.
1736
(** Correctness of this comparison *)
1742
| Gt => (fun l1 l2 => L.lt l2 l1)
1745
Lemma cons_Cmp : forall c x1 x2 l1 l2, X.eq x1 x2 ->
1746
Cmp c l1 l2 -> Cmp c (x1::l1) (x2::l2).
1748
destruct c; simpl; auto.
1750
Hint Resolve cons_Cmp.
1752
Lemma compare_end_Cmp :
1753
forall e2, Cmp (compare_end e2) nil (flatten_e e2).
1755
destruct e2; simpl; auto.
1759
Lemma compare_more_Cmp : forall x1 cont x2 r2 e2 l,
1760
Cmp (cont (cons r2 e2)) l (elements r2 ++ flatten_e e2) ->
1761
Cmp (compare_more x1 cont (More x2 r2 e2)) (x1::l)
1762
(flatten_e (More x2 r2 e2)).
1764
simpl; intros; destruct X.compare; simpl; auto.
1767
Lemma compare_cont_Cmp : forall s1 cont e2 l,
1768
(forall e, Cmp (cont e) l (flatten_e e)) ->
1769
Cmp (compare_cont s1 cont e2) (elements s1 ++ l) (flatten_e e2).
1771
induction s1 as [|l1 Hl1 x1 r1 Hr1 h1]; simpl; intros; auto.
1772
rewrite <- elements_node; simpl.
1773
apply Hl1; auto. clear e2. intros [|x2 r2 e2].
1775
apply compare_more_Cmp.
1776
rewrite <- cons_1; auto.
1779
Lemma compare_Cmp : forall s1 s2,
1780
Cmp (compare s1 s2) (elements s1) (elements s2).
1782
intros; unfold compare.
1783
rewrite (app_nil_end (elements s1)).
1784
replace (elements s2) with (flatten_e (cons s2 End)) by
1785
(rewrite cons_1; simpl; rewrite <- app_nil_end; auto).
1786
apply compare_cont_Cmp; auto.
1788
apply compare_end_Cmp; auto.
1791
(** * Equality test *)
1793
Lemma equal_1 : forall s1 s2, bst s1 -> bst s2 ->
1794
Equal s1 s2 -> equal s1 s2 = true.
1796
unfold equal; intros s1 s2 B1 B2 E.
1797
generalize (compare_Cmp s1 s2).
1798
destruct (compare s1 s2); simpl in *; auto; intros.
1799
elim (lt_not_eq B1 B2 H E); auto.
1800
elim (lt_not_eq B2 B1 H (eq_sym E)); auto.
1803
Lemma equal_2 : forall s1 s2,
1804
equal s1 s2 = true -> Equal s1 s2.
1806
unfold equal; intros s1 s2 E.
1807
generalize (compare_Cmp s1 s2);
1808
destruct compare; auto; discriminate.
1819
Now, in order to really provide a functor implementing [S], we
1820
need to encapsulate everything into a type of binary search trees.
1821
They also happen to be well-balanced, but this has no influence
1822
on the correctness of operations, so we won't state this here,
1823
see [FSetFullAVL] if you need more than just the FSet interface.
1826
Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
1829
Module Raw := Raw I X.
1832
Record bst := Bst {this :> Raw.t; is_bst : Raw.bst this}.
1833
Definition t := bst.
1834
Definition elt := E.t.
1836
Definition In (x : elt) (s : t) := Raw.In x s.
1837
Definition Equal (s s':t) := forall a : elt, In a s <-> In a s'.
1838
Definition Subset (s s':t) := forall a : elt, In a s -> In a s'.
1839
Definition Empty (s:t) := forall a : elt, ~ In a s.
1840
Definition For_all (P : elt -> Prop) (s:t) := forall x, In x s -> P x.
1841
Definition Exists (P : elt -> Prop) (s:t) := exists x, In x s /\ P x.
1843
Lemma In_1 : forall (s:t)(x y:elt), E.eq x y -> In x s -> In y s.
1844
Proof. intro s; exact (@In_1 s). Qed.
1846
Definition mem (x:elt)(s:t) : bool := Raw.mem x s.
1848
Definition empty : t := Bst empty_bst.
1849
Definition is_empty (s:t) : bool := Raw.is_empty s.
1850
Definition singleton (x:elt) : t := Bst (singleton_bst x).
1851
Definition add (x:elt)(s:t) : t := Bst (add_bst x (is_bst s)).
1852
Definition remove (x:elt)(s:t) : t := Bst (remove_bst x (is_bst s)).
1853
Definition inter (s s':t) : t := Bst (inter_bst (is_bst s) (is_bst s')).
1854
Definition union (s s':t) : t := Bst (union_bst (is_bst s) (is_bst s')).
1855
Definition diff (s s':t) : t := Bst (diff_bst (is_bst s) (is_bst s')).
1856
Definition elements (s:t) : list elt := Raw.elements s.
1857
Definition min_elt (s:t) : option elt := Raw.min_elt s.
1858
Definition max_elt (s:t) : option elt := Raw.max_elt s.
1859
Definition choose (s:t) : option elt := Raw.choose s.
1860
Definition fold (B : Type) (f : elt -> B -> B) (s:t) : B -> B := Raw.fold f s.
1861
Definition cardinal (s:t) : nat := Raw.cardinal s.
1862
Definition filter (f : elt -> bool) (s:t) : t :=
1863
Bst (filter_bst f (is_bst s)).
1864
Definition for_all (f : elt -> bool) (s:t) : bool := Raw.for_all f s.
1865
Definition exists_ (f : elt -> bool) (s:t) : bool := Raw.exists_ f s.
1866
Definition partition (f : elt -> bool) (s:t) : t * t :=
1867
let p := Raw.partition f s in
1868
(@Bst (fst p) (partition_bst_1 f (is_bst s)),
1869
@Bst (snd p) (partition_bst_2 f (is_bst s))).
1871
Definition equal (s s':t) : bool := Raw.equal s s'.
1872
Definition subset (s s':t) : bool := Raw.subset s s'.
1874
Definition eq (s s':t) : Prop := Raw.Equal s s'.
1875
Definition lt (s s':t) : Prop := Raw.Proofs.lt s s'.
1877
Definition compare (s s':t) : Compare lt eq s s'.
1879
intros (s,b) (s',b').
1880
generalize (compare_Cmp s s').
1881
destruct Raw.compare; intros; [apply EQ|apply LT|apply GT]; red; auto.
1884
Definition eq_dec (s s':t) : { eq s s' } + { ~ eq s s' }.
1886
intros (s,b) (s',b'); unfold eq; simpl.
1887
case_eq (Raw.equal s s'); intro H; [left|right].
1888
apply equal_2; auto.
1889
intro H'; rewrite equal_1 in H; auto; discriminate.
1894
Variable s s' s'': t.
1897
Hint Resolve is_bst.
1899
Lemma mem_1 : In x s -> mem x s = true.
1900
Proof. exact (mem_1 (is_bst s)). Qed.
1901
Lemma mem_2 : mem x s = true -> In x s.
1902
Proof. exact (@mem_2 s x). Qed.
1904
Lemma equal_1 : Equal s s' -> equal s s' = true.
1905
Proof. exact (equal_1 (is_bst s) (is_bst s')). Qed.
1906
Lemma equal_2 : equal s s' = true -> Equal s s'.
1907
Proof. exact (@equal_2 s s'). Qed.
1909
Ltac wrap t H := unfold t, In; simpl; rewrite H; auto; intuition.
1911
Lemma subset_1 : Subset s s' -> subset s s' = true.
1912
Proof. wrap subset subset_12. Qed.
1913
Lemma subset_2 : subset s s' = true -> Subset s s'.
1914
Proof. wrap subset subset_12. Qed.
1916
Lemma empty_1 : Empty empty.
1917
Proof. exact empty_1. Qed.
1919
Lemma is_empty_1 : Empty s -> is_empty s = true.
1920
Proof. exact (@is_empty_1 s). Qed.
1921
Lemma is_empty_2 : is_empty s = true -> Empty s.
1922
Proof. exact (@is_empty_2 s). Qed.
1924
Lemma add_1 : E.eq x y -> In y (add x s).
1925
Proof. wrap add add_in. Qed.
1926
Lemma add_2 : In y s -> In y (add x s).
1927
Proof. wrap add add_in. Qed.
1928
Lemma add_3 : ~ E.eq x y -> In y (add x s) -> In y s.
1929
Proof. wrap add add_in. elim H; auto. Qed.
1931
Lemma remove_1 : E.eq x y -> ~ In y (remove x s).
1932
Proof. wrap remove remove_in. Qed.
1933
Lemma remove_2 : ~ E.eq x y -> In y s -> In y (remove x s).
1934
Proof. wrap remove remove_in. Qed.
1935
Lemma remove_3 : In y (remove x s) -> In y s.
1936
Proof. wrap remove remove_in. Qed.
1938
Lemma singleton_1 : In y (singleton x) -> E.eq x y.
1939
Proof. exact (@singleton_1 x y). Qed.
1940
Lemma singleton_2 : E.eq x y -> In y (singleton x).
1941
Proof. exact (@singleton_2 x y). Qed.
1943
Lemma union_1 : In x (union s s') -> In x s \/ In x s'.
1944
Proof. wrap union union_in. Qed.
1945
Lemma union_2 : In x s -> In x (union s s').
1946
Proof. wrap union union_in. Qed.
1947
Lemma union_3 : In x s' -> In x (union s s').
1948
Proof. wrap union union_in. Qed.
1950
Lemma inter_1 : In x (inter s s') -> In x s.
1951
Proof. wrap inter inter_in. Qed.
1952
Lemma inter_2 : In x (inter s s') -> In x s'.
1953
Proof. wrap inter inter_in. Qed.
1954
Lemma inter_3 : In x s -> In x s' -> In x (inter s s').
1955
Proof. wrap inter inter_in. Qed.
1957
Lemma diff_1 : In x (diff s s') -> In x s.
1958
Proof. wrap diff diff_in. Qed.
1959
Lemma diff_2 : In x (diff s s') -> ~ In x s'.
1960
Proof. wrap diff diff_in. Qed.
1961
Lemma diff_3 : In x s -> ~ In x s' -> In x (diff s s').
1962
Proof. wrap diff diff_in. Qed.
1964
Lemma fold_1 : forall (A : Type) (i : A) (f : elt -> A -> A),
1965
fold f s i = fold_left (fun a e => f e a) (elements s) i.
1966
Proof. unfold fold, elements; intros; apply fold_1; auto. Qed.
1968
Lemma cardinal_1 : cardinal s = length (elements s).
1970
unfold cardinal, elements; intros; apply elements_cardinal; auto.
1974
Variable f : elt -> bool.
1976
Lemma filter_1 : compat_bool E.eq f -> In x (filter f s) -> In x s.
1977
Proof. intro. wrap filter filter_in. Qed.
1978
Lemma filter_2 : compat_bool E.eq f -> In x (filter f s) -> f x = true.
1979
Proof. intro. wrap filter filter_in. Qed.
1980
Lemma filter_3 : compat_bool E.eq f -> In x s -> f x = true -> In x (filter f s).
1981
Proof. intro. wrap filter filter_in. Qed.
1983
Lemma for_all_1 : compat_bool E.eq f -> For_all (fun x => f x = true) s -> for_all f s = true.
1984
Proof. exact (@for_all_1 f s). Qed.
1985
Lemma for_all_2 : compat_bool E.eq f -> for_all f s = true -> For_all (fun x => f x = true) s.
1986
Proof. exact (@for_all_2 f s). Qed.
1988
Lemma exists_1 : compat_bool E.eq f -> Exists (fun x => f x = true) s -> exists_ f s = true.
1989
Proof. exact (@exists_1 f s). Qed.
1990
Lemma exists_2 : compat_bool E.eq f -> exists_ f s = true -> Exists (fun x => f x = true) s.
1991
Proof. exact (@exists_2 f s). Qed.
1993
Lemma partition_1 : compat_bool E.eq f ->
1994
Equal (fst (partition f s)) (filter f s).
1996
unfold partition, filter, Equal, In; simpl ;intros H a.
1997
rewrite partition_in_1, filter_in; intuition.
2000
Lemma partition_2 : compat_bool E.eq f ->
2001
Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
2003
unfold partition, filter, Equal, In; simpl ;intros H a.
2004
rewrite partition_in_2, filter_in; intuition.
2006
destruct (f a); auto.
2007
red; intros; f_equal.
2008
rewrite (H _ _ H0); auto.
2013
Lemma elements_1 : In x s -> InA E.eq x (elements s).
2014
Proof. wrap elements elements_in. Qed.
2015
Lemma elements_2 : InA E.eq x (elements s) -> In x s.
2016
Proof. wrap elements elements_in. Qed.
2017
Lemma elements_3 : sort E.lt (elements s).
2018
Proof. exact (elements_sort (is_bst s)). Qed.
2019
Lemma elements_3w : NoDupA E.eq (elements s).
2020
Proof. exact (elements_nodup (is_bst s)). Qed.
2022
Lemma min_elt_1 : min_elt s = Some x -> In x s.
2023
Proof. exact (@min_elt_1 s x). Qed.
2024
Lemma min_elt_2 : min_elt s = Some x -> In y s -> ~ E.lt y x.
2025
Proof. exact (@min_elt_2 s x y (is_bst s)). Qed.
2026
Lemma min_elt_3 : min_elt s = None -> Empty s.
2027
Proof. exact (@min_elt_3 s). Qed.
2029
Lemma max_elt_1 : max_elt s = Some x -> In x s.
2030
Proof. exact (@max_elt_1 s x). Qed.
2031
Lemma max_elt_2 : max_elt s = Some x -> In y s -> ~ E.lt x y.
2032
Proof. exact (@max_elt_2 s x y (is_bst s)). Qed.
2033
Lemma max_elt_3 : max_elt s = None -> Empty s.
2034
Proof. exact (@max_elt_3 s). Qed.
2036
Lemma choose_1 : choose s = Some x -> In x s.
2037
Proof. exact (@choose_1 s x). Qed.
2038
Lemma choose_2 : choose s = None -> Empty s.
2039
Proof. exact (@choose_2 s). Qed.
2040
Lemma choose_3 : choose s = Some x -> choose s' = Some y ->
2041
Equal s s' -> E.eq x y.
2042
Proof. exact (@choose_3 _ _ (is_bst s) (is_bst s') x y). Qed.
2044
Lemma eq_refl : eq s s.
2045
Proof. exact (eq_refl s). Qed.
2046
Lemma eq_sym : eq s s' -> eq s' s.
2047
Proof. exact (@eq_sym s s'). Qed.
2048
Lemma eq_trans : eq s s' -> eq s' s'' -> eq s s''.
2049
Proof. exact (@eq_trans s s' s''). Qed.
2051
Lemma lt_trans : lt s s' -> lt s' s'' -> lt s s''.
2052
Proof. exact (@lt_trans s s' s''). Qed.
2053
Lemma lt_not_eq : lt s s' -> ~eq s s'.
2054
Proof. exact (@lt_not_eq _ _ (is_bst s) (is_bst s')). Qed.
2059
(* For concrete use inside Coq, we propose an instantiation of [Int] by [Z]. *)
2061
Module Make (X: OrderedType) <: S with Module E := X
2062
:=IntMake(Z_as_Int)(X).
added
removed
theories/FSets/FSetAVL.v
