Library Coq.MSets.MSetGenTree
MSetGenTree : sets via generic trees
This module factorizes common parts in implementations
of finite sets as AVL trees and as Red-Black trees. The nodes
of the trees defined here include an generic information
parameter, that will be the height in AVL trees and the color
in Red-Black trees. Without more details here about these
information parameters, trees here are not known to be
well-balanced, but simply binary-search-trees.
The operations we could define and prove correct here are the
one that do not build non-empty trees, but only analyze them :
- empty is_empty
- mem
- compare equal subset
- fold cardinal elements
- for_all exists
- min_elt max_elt choose
The empty set and emptyness test
Membership test
The
mem function is deciding membership. It exploits the
binary search tree invariant to achieve logarithmic complexity.
Minimal, maximal, arbitrary elements
Testing universal or existential properties.
We do not use the standard boolean operators of Coq,
but lazy ones.
Comparison of trees
The algorithm here has been suggested by Xavier Leroy,
and transformed into c.p.s. 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
MSetFullAVL. 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. This corresponds
to the "samefringe" notion in the literature.
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
Subset test
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
MSetFullAVL.
Props : correctness proofs of these generic operations
Binary search trees
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
bst is the (decidable) invariant our trees will have to satisfy.
Known facts about ordered types
Automation and dedicated tactics
Scheme tree_ind :=
Induction for tree Sort Prop.
Scheme bst_ind :=
Induction for bst Sort Prop.
Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans ok :
core.
Local Hint Immediate MX.eq_sym :
core.
Local Hint Unfold In lt_tree gt_tree :
core.
Local Hint Constructors InT bst :
core.
Local Hint Unfold Ok :
core.
Automatic treatment of Ok hypothesis
Ltac clear_inversion H :=
inversion H;
clear H;
subst.
Ltac inv_ok :=
match goal with
|
H:
Ok (
Node _ _ _ _) |-
_ =>
clear_inversion H;
inv_ok
|
H:
Ok Leaf |-
_ =>
clear H;
inv_ok
|
H:
bst ?
x |-
_ =>
change (
Ok x)
in H;
inv_ok
|
_ =>
idtac
end.
A tactic to repeat inversion_clear on all hyps of the
form (f (Node _ _ _ _))
Ltac is_tree_constr c :=
match c with
|
Leaf =>
idtac
|
Node _ _ _ _ =>
idtac
|
_ =>
fail
end.
Ltac invtree f :=
match goal with
|
H:
f ?
s |-
_ =>
is_tree_constr s;
clear_inversion H;
invtree f
|
H:
f _ ?
s |-
_ =>
is_tree_constr s;
clear_inversion H;
invtree f
|
H:
f _ _ ?
s |-
_ =>
is_tree_constr s;
clear_inversion H;
invtree f
|
_ =>
idtac
end.
Ltac inv :=
inv_ok;
invtree InT.
Ltac intuition_in :=
repeat (
intuition;
inv).
Helper tactic concerning order of elements.
Ltac order :=
match goal with
|
U:
lt_tree _ ?
s,
V:
InT _ ?
s |-
_ =>
generalize (
U _ V);
clear U;
order
|
U:
gt_tree _ ?
s,
V:
InT _ ?
s |-
_ =>
generalize (
U _ V);
clear U;
order
|
_ =>
MX.order
end.
isok is indeed a decision procedure for Ok
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) (
i :
Info.t),
lt_tree x l -> lt_tree x r -> X.lt y x -> lt_tree x (
Node i l y r).
Lemma gt_tree_node :
forall (
x y :
elt) (
l r :
tree) (
i :
Info.t),
gt_tree x l -> gt_tree x r -> X.lt x y -> gt_tree x (
Node i l y r).
Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node :
core.
Lemma lt_tree_not_in :
forall (
x :
elt) (
t :
tree),
lt_tree x t -> ~ InT 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 -> ~ InT x t.
Lemma gt_tree_trans :
forall x y,
X.lt y x -> forall t,
gt_tree x t -> gt_tree y t.
Instance lt_tree_compat :
Proper (
X.eq ==> Logic.eq ==> iff)
lt_tree.
Instance gt_tree_compat :
Proper (
X.eq ==> Logic.eq ==> iff)
gt_tree.
Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans :
core.
Ltac induct s x :=
induction s as [|
i l IHl x' r IHr];
simpl;
intros;
[|
elim_compare x x';
intros;
inv].
Ltac auto_tc :=
auto with typeclass_instances.
Ltac ok :=
inv;
change bst with Ok in *;
match goal with
| |-
Ok (
Node _ _ _ _) =>
constructor;
auto_tc;
ok
| |-
lt_tree _ (
Node _ _ _ _) =>
apply lt_tree_node;
ok
| |-
gt_tree _ (
Node _ _ _ _) =>
apply gt_tree_node;
ok
|
_ =>
eauto with typeclass_instances
end.
Minimal and maximal elements
Lemma elements_spec1' :
forall s acc x,
InA X.eq x (
elements_aux acc s)
<-> InT x s \/ InA X.eq x acc.
Lemma elements_spec1 :
forall s x,
InA X.eq x (
elements s)
<-> InT x s.
Lemma elements_spec2' :
forall s acc `{
Ok s},
sort X.lt acc ->
(forall x y :
elt,
InA X.eq x acc -> InT y s -> X.lt y x) ->
sort X.lt (
elements_aux acc s).
Lemma elements_spec2 :
forall s `(
Ok s),
sort X.lt (
elements s).
Local Hint Resolve elements_spec2 :
core.
Lemma elements_spec2w :
forall s `(
Ok 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).
Definition cardinal_spec (
s:
tree)(
Hs:
Ok s) :=
elements_cardinal s.
Lemma elements_app :
forall s acc,
elements_aux acc s = elements s ++ acc.
Lemma elements_node c l x r :
elements (
Node c l x r)
= elements l ++ x :: elements r.
Lemma rev_elements_app :
forall s acc,
rev_elements_aux acc s = rev_elements s ++ acc.
Lemma rev_elements_node c l x r :
rev_elements (
Node c l x r)
= rev_elements r ++ x :: rev_elements l.
Lemma rev_elements_rev s :
rev_elements s = rev (
elements s).
The converse of elements_spec2, used in MSetRBT
Comparison
Relations
eq and
lt over trees
Proof of the comparison algorithm
flatten_e e returns the list of elements of
e i.e. the list
of elements actually compared
Correctness of this comparison
A few results about mindepth and maxdepth