Library Coq.MSets.MSetAVL
MSetAVL : Implementation of MSetInterface via AVL trees
This module implements finite 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: heights 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 MSet interface. As a consequence,
balancing results are not part of this file anymore, they can
now be found in
MSetFullAVL.
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
MSetFullAVL. The structural variants compute faster in Coq,
whereas the other variants produce nicer and/or (slightly) faster
code after extraction.
Generic trees instantiated with integer height
We reuse a generic definition of trees where the information
parameter is a
Int.t. Functions like mem or fold are also
provided by this generic functor.
Helper functions
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 h l x r. 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.
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).
Fixpoint split x s :
triple :=
match s with
|
Leaf =>
<< Leaf, false, Leaf >>
|
Node _ l y r =>
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.
Union
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
MSetFullAVL.
MakeRaw
Functor of pure functions + a posteriori proofs of invariant
preservation
Generic definition of binary-search-trees and proofs of
specifications for generic functions such as mem or fold.
Automation and dedicated tactics
Local Hint Immediate MX.eq_sym :
core.
Local Hint Unfold In lt_tree gt_tree Ok :
core.
Local Hint Constructors InT bst :
core.
Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans ok :
core.
Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node :
core.
Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans :
core.
Local Hint Resolve elements_spec2 :
core.
Tactic Notation "factornode"
ident(
s) :=
try clear s;
match goal with
| |-
context [
Node ?
l ?
x ?
r ?
h] =>
set (
s:=
Node l x r h)
in *;
clearbody s;
clear l x r h
|
_ :
context [
Node ?
l ?
x ?
r ?
h] |-
_ =>
set (
s:=
Node l x r h)
in *;
clearbody s;
clear l x r h
end.
Inductions principles for some of the set operators
Functional Scheme bal_ind := Induction for bal Sort Prop.
Functional Scheme remove_min_ind := Induction for remove_min Sort Prop.
Functional Scheme merge_ind := Induction for merge Sort Prop.
Functional Scheme concat_ind := Induction for concat Sort Prop.
Functional Scheme inter_ind := Induction for inter Sort Prop.
Functional Scheme diff_ind := Induction for diff Sort Prop.
Functional Scheme union_ind := Induction for union Sort Prop.
Notations and helper lemma about pairs and triples
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.
Notation "t #l" := (
t_left t) (
at level 9,
format "t '#l'") :
pair_scope.
Notation "t #b" := (
t_in t) (
at level 9,
format "t '#b'") :
pair_scope.
Notation "t #r" := (
t_right t) (
at level 9,
format "t '#r'") :
pair_scope.
Local Open Scope pair_scope.
Join
Function/Functional Scheme can't deal with internal fix.
Let's do its job by hand:
Extraction of minimum element
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
MSetFullAVL if you need more than just the MSet interface.