Library Coq.FSets.FSetAVL
This module implements sets using AVL trees.
It follows the implementation from Ocaml's standard library,
All operations given here expect and produce well-balanced trees
(in the ocaml sense: heigths of subtrees shouldn't differ by more
than 2), and hence has low complexities (e.g. add is logarithmic
in the size of the set). But proving these balancing preservations
is in fact not necessary for ensuring correct operational behavior
and hence fulfilling the FSet interface. As a consequence,
balancing results are not part of this file anymore, they can
now be found in FSetFullAVL.
Four operations (union, subset, compare and equal) have
been slightly adapted in order to have only structural recursive
calls. The precise ocaml versions of these operations have also
been formalized (thanks to Function+measure), see ocaml_union,
ocaml_subset, ocaml_compare and ocaml_equal in
FSetFullAVL. The structural variants compute faster in Coq,
whereas the other variants produce nicer and/or (slightly) faster
code after extraction.
Notations and helper lemma about pairs
Notation "s #1" := (
fst s) (
at level 9,
format "s '#1'") :
pair_scope.
Notation "s #2" := (
snd s) (
at level 9,
format "s '#2'") :
pair_scope.
Raw
Functor of pure functions + a posteriori proofs of invariant
preservation
Module Raw (
Import I:Int)(X:OrderedType).
Open Local Scope pair_scope.
Open Local Scope lazy_bool_scope.
Open Local Scope Int_scope.
Definition elt :=
X.t.
Trees
The fourth field of
Node is the height of the tree
Basic functions on trees: height and cardinal
The mem function is deciding appartness. It exploits the
binary search tree invariant to achieve logarithmic complexity.
create l x r creates a node, assuming l and r
to be balanced and |height l - height r| <= 2.
bal l x r acts as create, but performs one step of
rebalancing if necessary, i.e. assumes |height l - height r| <= 3.
Join
Same as
bal but does not assume anything regarding heights
of
l and
r.
Extraction of minimum element
Morally,
remove_min is to be applied to a non-empty tree
t = Node l x r h. Since we can't deal here with
assert false
for
t=Leaf, we pre-unpack
t (and forget about
h).
Merging two trees
merge t1 t2 builds the union of
t1 and
t2 assuming all elements
of
t1 to be smaller than all elements of
t2, and
|height t1 - height t2| <= 2.
Definition merge s1 s2 :=
match s1,s2
with
|
Leaf,
_ =>
s2
|
_,
Leaf =>
s1
|
_,
Node l2 x2 r2 h2 =>
let (
s2',m) :=
remove_min l2 x2 r2 in bal s1 m s2'
end.
Concatenation
Same as
merge but does not assume anything about heights.
Splitting
split x s returns a triple
(l, present, r) where
- l is the set of elements of s that are < x
- r is the set of elements of s that are > x
- present is true if and only if s contains x.
Record triple :=
mktriple {
t_left:t;
t_in:bool;
t_right:t }.
Notation "<< l , b , r >>" := (
mktriple l b r) (
at level 9).
Notation "t #l" := (
t_left t) (
at level 9,
format "t '#l'").
Notation "t #b" := (
t_in t) (
at level 9,
format "t '#b'").
Notation "t #r" := (
t_right t) (
at level 9,
format "t '#r'").
Fixpoint split x s :
triple :=
match s with
|
Leaf => <<
Leaf,
false,
Leaf >>
|
Node l y r h =>
match X.compare x y with
|
LT _ =>
let (
ll,b,rl) :=
split x l in <<
ll,
b,
join rl y r >>
|
EQ _ => <<
l,
true,
r >>
|
GT _ =>
let (
rl,b,rr) :=
split x r in <<
join l y rl,
b,
rr >>
end
end.
In ocaml, heights of s1 and s2 are compared each time in order
to recursively perform the split on the smaller set.
Unfortunately, this leads to a non-structural algorithm. The
following code is a simplification of the ocaml version: no
comparison of heights. It might be slightly slower, but
experimentally all the tests I've made in ocaml have shown this
potential slowdown to be non-significant. Anyway, the exact code
of ocaml has also been formalized thanks to Function+measure, see
ocaml_union in FSetFullAVL.
elements_tree_aux acc t catenates the elements of t in infix
order to the list acc
then elements is an instanciation with an empty acc
Fixpoint fold (
A :
Type) (
f :
elt ->
A ->
A)(
s :
tree) :
A ->
A :=
fun a =>
match s with
|
Leaf =>
a
|
Node l x r _ =>
fold f r (
f x (
fold f l a))
end.
Implicit Arguments fold [
A].
In ocaml, recursive calls are made on "half-trees" such as
(Node l1 x1 Leaf _) and (Node Leaf x1 r1 _). Instead of these
non-structural calls, we propose here two specialized functions for
these situations. This version should be almost as efficient as
the one of ocaml (closures as arguments may slow things a bit),
it is simply less compact. The exact ocaml version has also been
formalized (thanks to Function+measure), see ocaml_subset in
FSetFullAVL.
A new comparison algorithm suggested by Xavier Leroy
Transformation in C.P.S. suggested by Benjamin Grégoire.
The original ocaml code (with non-structural recursive calls)
has also been formalized (thanks to Function+measure), see
ocaml_compare in
FSetFullAVL. The following code with
continuations computes dramatically faster in Coq, and
should be almost as efficient after extraction.
Enumeration of the elements of a tree
cons t e adds the elements of tree t on the head of
enumeration e.
One step of comparison of elements
Comparison of left tree, middle element, then right tree
Initial continuation
The complete comparison
lt_tree x s: all elements in s are smaller than x
(resp. greater for gt_tree)
bst t : t is a binary search tree
Definition Equal s s' :=
forall a :
elt,
In a s <->
In a s'.
Definition Subset s s' :=
forall a :
elt,
In a s ->
In a s'.
Definition Empty s :=
forall a :
elt, ~
In a s.
Definition For_all (
P :
elt ->
Prop)
s :=
forall x,
In x s ->
P x.
Definition Exists (
P :
elt ->
Prop)
s :=
exists x,
In x s /\
P x.
Correctness proofs, isolated in a sub-module
Automation and dedicated tactics
Hint Constructors In bst.
Hint Unfold lt_tree gt_tree.
Tactic Notation "factornode"
ident(
l)
ident(
x)
ident(
r)
ident(
h)
"as"
ident(
s) :=
set (
s:=Node
l x r h)
in *;
clearbody s;
clear l x r h.
A tactic to repeat inversion_clear on all hyps of the
form (f (Node _ _ _ _))
Ltac inv f :=
match goal with
|
H:f
Leaf |-
_ =>
inversion_clear H;
inv f
|
H:f
_ Leaf |-
_ =>
inversion_clear H;
inv f
|
H:f (
Node _ _ _ _) |-
_ =>
inversion_clear H;
inv f
|
H:f
_ (
Node _ _ _ _) |-
_ =>
inversion_clear H;
inv f
|
_ =>
idtac
end.
Ltac intuition_in :=
repeat progress (
intuition;
inv In).
Helper tactic concerning order of elements.
Ltac order :=
match goal with
|
U:
lt_tree _ ?s,
V:
In _ ?s |-
_ =>
generalize (
U _ V);
clear U;
order
|
U:
gt_tree _ ?s,
V:
In _ ?s |-
_ =>
generalize (
U _ V);
clear U;
order
|
_ =>
MX.order
end.
Basic results about In, lt_tree, gt_tree, height
In is compatible with X.eq
Results about lt_tree and gt_tree
Lemma lt_leaf :
forall x :
elt,
lt_tree x Leaf.
Lemma gt_leaf :
forall x :
elt,
gt_tree x Leaf.
Lemma lt_tree_node :
forall (
x y :
elt) (
l r :
tree) (
h :
int),
lt_tree x l ->
lt_tree x r ->
X.lt y x ->
lt_tree x (
Node l y r h).
Lemma gt_tree_node :
forall (
x y :
elt) (
l r :
tree) (
h :
int),
gt_tree x l ->
gt_tree x r ->
X.lt x y ->
gt_tree x (
Node l y r h).
Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node.
Lemma lt_tree_not_in :
forall (
x :
elt) (
t :
tree),
lt_tree x t -> ~
In x t.
Lemma lt_tree_trans :
forall x y,
X.lt x y ->
forall t,
lt_tree x t ->
lt_tree y t.
Lemma gt_tree_not_in :
forall (
x :
elt) (
t :
tree),
gt_tree x t -> ~
In x t.
Lemma gt_tree_trans :
forall x y,
X.lt y x ->
forall t,
gt_tree x t ->
gt_tree y t.
Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans.
Ltac join_tac :=
intro l;
induction l as [|
ll _ lx lr Hlr lh];
[ |
intros x r;
induction r as [|
rl Hrl rx rr _ rh];
unfold join;
[ |
destruct (
gt_le_dec lh (
rh+2));
[
match goal with |-
context b [
bal ?a ?b ?c] =>
replace (
bal a b c)
with (
bal ll lx (
join lr x (
Node rl rx rr rh))); [ |
auto]
end
|
destruct (
gt_le_dec rh (
lh+2));
[
match goal with |-
context b [
bal ?a ?b ?c] =>
replace (
bal a b c)
with (
bal (
join (
Node ll lx lr lh)
x rl)
rx rr); [ |
auto]
end
| ] ] ] ];
intros.
Lemma join_in :
forall l x r y,
In y (
join l x r) <->
X.eq y x \/
In y l \/
In y r.
Lemma join_bst :
forall l x r,
bst l ->
bst r ->
lt_tree x l ->
gt_tree x r ->
bst (
join l x r).
Hint Resolve join_bst.
Extraction of minimum element
Lemma elements_aux_in :
forall s acc x,
InA X.eq x (
elements_aux acc s) <->
In x s \/
InA X.eq x acc.
Lemma elements_in :
forall s x,
InA X.eq x (
elements s) <->
In x s.
Lemma elements_aux_sort :
forall s acc,
bst s ->
sort X.lt acc ->
(
forall x y :
elt,
InA X.eq x acc ->
In y s ->
X.lt y x) ->
sort X.lt (
elements_aux acc s).
Lemma elements_sort :
forall s :
tree,
bst s ->
sort X.lt (
elements s).
Hint Resolve elements_sort.
Lemma elements_nodup :
forall s :
tree,
bst s ->
NoDupA X.eq (
elements s).
Lemma elements_aux_cardinal :
forall s acc, (
length acc +
cardinal s)%nat =
length (
elements_aux acc s).
Lemma elements_cardinal :
forall s :
tree,
cardinal s =
length (
elements s).
Lemma elements_app :
forall s acc,
elements_aux acc s =
elements s ++
acc.
Lemma elements_node :
forall l x r h acc,
elements l ++
x ::
elements r ++
acc =
elements (
Node l x r h) ++
acc.
Lemma partition_acc_in_1 :
forall s acc,
compat_bool X.eq f ->
forall x :
elt,
In x (
partition_acc f acc s)#1 <->
In x acc#1 \/
In x s /\
f x =
true.
Lemma partition_acc_in_2 :
forall s acc,
compat_bool X.eq f ->
forall x :
elt,
In x (
partition_acc f acc s)#2 <->
In x acc#2 \/
In x s /\
f x =
false.
Lemma partition_in_1 :
forall s,
compat_bool X.eq f ->
forall x :
elt,
In x (
partition f s)#1 <->
In x s /\
f x =
true.
Lemma partition_in_2 :
forall s,
compat_bool X.eq f ->
forall x :
elt,
In x (
partition f s)#2 <->
In x s /\
f x =
false.
Lemma partition_acc_bst_1 :
forall s acc,
bst s ->
bst acc#1 ->
bst (
partition_acc f acc s)#1.
Lemma partition_acc_bst_2 :
forall s acc,
bst s ->
bst acc#2 ->
bst (
partition_acc f acc s)#2.
Lemma partition_bst_1 :
forall s,
bst s ->
bst (
partition f s)#1.
Lemma partition_bst_2 :
forall s,
bst s ->
bst (
partition f s)#2.
Relations eq and lt over trees
A new comparison algorithm suggested by Xavier Leroy
flatten_e e returns the list of elements of e i.e. the list
of elements actually compared
Correctness of this comparison
Encapsulation
Now, in order to really provide a functor implementing
S, we
need to encapsulate everything into a type of binary search trees.
They also happen to be well-balanced, but this has no influence
on the correctness of operations, so we won't state this here,
see
FSetFullAVL if you need more than just the FSet interface.