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.
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.
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.
Definition height (s : tree) : int :=
match s with
| Leaf => 0
| Node _ _ _ h => h
end.
Fixpoint cardinal (s : tree) : nat :=
match s with
| Leaf => 0%nat
| Node l _ r _ => S (cardinal l + cardinal r)
end.
The mem function is deciding appartness. It exploits the
binary search tree invariant to achieve logarithmic complexity.
Fixpoint mem x s :=
match s with
| Leaf => false
| Node l y r _ => match X.compare x y with
| LT _ => mem x l
| EQ _ => true
| GT _ => mem x r
end
end.
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.
Definition assert_false := create.
Definition bal l x r :=
let hl := height l in
let hr := height r in
if gt_le_dec hl (hr+2) then
match l with
| Leaf => assert_false l x r
| Node ll lx lr _ =>
if ge_lt_dec (height ll) (height lr) then
create ll lx (create lr x r)
else
match lr with
| Leaf => assert_false l x r
| Node lrl lrx lrr _ =>
create (create ll lx lrl) lrx (create lrr x r)
end
end
else
if gt_le_dec hr (hl+2) then
match r with
| Leaf => assert_false l x r
| Node rl rx rr _ =>
if ge_lt_dec (height rr) (height rl) then
create (create l x rl) rx rr
else
match rl with
| Leaf => assert_false l x r
| Node rll rlx rlr _ =>
create (create l x rll) rlx (create rlr rx rr)
end
end
else
create l x r.
Fixpoint add x s := match s with
| Leaf => Node Leaf x Leaf 1
| Node l y r h =>
match X.compare x y with
| LT _ => bal (add x l) y r
| EQ _ => Node l y r h
| GT _ => bal l y (add x r)
end
end.
Fixpoint join l : elt -> t -> t :=
match l with
| Leaf => add
| Node ll lx lr lh => fun x =>
fix join_aux (r:t) : t := match r with
| Leaf => add x l
| Node rl rx rr rh =>
if gt_le_dec lh (rh+2) then bal ll lx (join lr x r)
else if gt_le_dec rh (lh+2) then bal (join_aux rl) rx rr
else create l x r
end
end.
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).
Fixpoint remove_min l x r : t*elt :=
match l with
| Leaf => (r,x)
| Node ll lx lr lh =>
let (l',m) := remove_min ll lx lr in (bal l' x r, m)
end.
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.
Fixpoint remove x s := match s with
| Leaf => Leaf
| Node l y r h =>
match X.compare x y with
| LT _ => bal (remove x l) y r
| EQ _ => merge l r
| GT _ => bal l y (remove x r)
end
end.
Fixpoint min_elt s := match s with
| Leaf => None
| Node Leaf y _ _ => Some y
| Node l _ _ _ => min_elt l
end.
Fixpoint max_elt s := match s with
| Leaf => None
| Node _ y Leaf _ => Some y
| Node _ _ r _ => max_elt r
end.
Definition concat s1 s2 :=
match s1, s2 with
| Leaf, _ => s2
| _, Leaf => s1
| _, Node l2 x2 r2 _ =>
let (s2',m) := remove_min l2 x2 r2 in
join s1 m s2'
end.
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.
Fixpoint inter s1 s2 := match s1, s2 with
| Leaf, _ => Leaf
| _, Leaf => Leaf
| Node l1 x1 r1 h1, _ =>
let (l2',pres,r2') := split x1 s2 in
if pres then join (inter l1 l2') x1 (inter r1 r2')
else concat (inter l1 l2') (inter r1 r2')
end.
Fixpoint diff s1 s2 := match s1, s2 with
| Leaf, _ => Leaf
| _, Leaf => s1
| Node l1 x1 r1 h1, _ =>
let (l2',pres,r2') := split x1 s2 in
if pres then concat (diff l1 l2') (diff r1 r2')
else join (diff l1 l2') x1 (diff r1 r2')
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.
Fixpoint union s1 s2 :=
match s1, s2 with
| Leaf, _ => s2
| _, Leaf => s1
| Node l1 x1 r1 h1, _ =>
let (l2',_,r2') := split x1 s2 in
join (union l1 l2') x1 (union r1 r2')
end.
elements_tree_aux acc t catenates the elements of t in infix
order to the list acc
Fixpoint elements_aux (acc : list X.t) (t : tree) : list X.t :=
match t with
| Leaf => acc
| Node l x r _ => elements_aux (x :: elements_aux acc r) l
end.
then elements is an instanciation with an empty acc
Fixpoint filter_acc (f:elt->bool) acc s := match s with
| Leaf => acc
| Node l x r h =>
filter_acc f (filter_acc f (if f x then add x acc else acc) l) r
end.
Definition filter f := filter_acc f Leaf.
Fixpoint partition_acc (f:elt->bool)(acc : t*t)(s : t) : t*t :=
match s with
| Leaf => acc
| Node l x r _ =>
let (acct,accf) := acc in
partition_acc f
(partition_acc f
(if f x then (add x acct, accf) else (acct, add x accf)) l) r
end.
Definition partition f := partition_acc f (Leaf,Leaf).
Fixpoint for_all (f:elt->bool) s := match s with
| Leaf => true
| Node l x r _ => f x &&& for_all f l &&& for_all f r
end.
Fixpoint exists_ (f:elt->bool) s := match s with
| Leaf => false
| Node l x r _ => f x ||| exists_ f l ||| exists_ f r
end.
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.
Fixpoint subsetl (subset_l1:t->bool) x1 s2 : bool :=
match s2 with
| Leaf => false
| Node l2 x2 r2 h2 =>
match X.compare x1 x2 with
| EQ _ => subset_l1 l2
| LT _ => subsetl subset_l1 x1 l2
| GT _ => mem x1 r2 &&& subset_l1 s2
end
end.
Fixpoint subsetr (subset_r1:t->bool) x1 s2 : bool :=
match s2 with
| Leaf => false
| Node l2 x2 r2 h2 =>
match X.compare x1 x2 with
| EQ _ => subset_r1 r2
| LT _ => mem x1 l2 &&& subset_r1 s2
| GT _ => subsetr subset_r1 x1 r2
end
end.
Fixpoint subset s1 s2 : bool := match s1, s2 with
| Leaf, _ => true
| Node _ _ _ _, Leaf => false
| Node l1 x1 r1 h1, Node l2 x2 r2 h2 =>
match X.compare x1 x2 with
| EQ _ => subset l1 l2 &&& subset r1 r2
| LT _ => subsetl (subset l1) x1 l2 &&& subset r1 s2
| GT _ => subsetr (subset r1) x1 r2 &&& subset l1 s2
end
end.
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.
Fixpoint cons s e : enumeration :=
match s with
| Leaf => e
| Node l x r h => cons l (More x r e)
end.
One step of comparison of elements
Definition compare_more x1 (cont:enumeration->comparison) e2 :=
match e2 with
| End => Gt
| More x2 r2 e2 =>
match X.compare x1 x2 with
| EQ _ => cont (cons r2 e2)
| LT _ => Lt
| GT _ => Gt
end
end.
Comparison of left tree, middle element, then right tree
Fixpoint compare_cont s1 (cont:enumeration->comparison) e2 :=
match s1 with
| Leaf => cont e2
| Node l1 x1 r1 _ =>
compare_cont l1 (compare_more x1 (compare_cont r1 cont)) e2
end.
Initial continuation
The complete comparison
Inductive In (x : elt) : tree -> Prop :=
| IsRoot : forall l r h y, X.eq x y -> In x (Node l y r h)
| InLeft : forall l r h y, In x l -> In x (Node l y r h)
| InRight : forall l r h y, In x r -> In x (Node l y r h).
lt_tree x s: all elements in s are smaller than x
(resp. greater for gt_tree)
Definition lt_tree x s := forall y, In y s -> X.lt y x.
Definition gt_tree x s := forall y, In y s -> X.lt x y.
bst t : t is a binary search tree
Inductive bst : tree -> Prop :=
| BSLeaf : bst Leaf
| BSNode : forall x l r h, bst l -> bst r ->
lt_tree x l -> gt_tree x r -> bst (Node l x r h).
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.
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.
In is compatible with X.eq
Lemma In_1 :
forall s x y, X.eq x y -> In x s -> In y s.
Hint Immediate In_1.
Lemma In_node_iff :
forall l x r h y,
In y (Node l x r h) <-> In y l \/ X.eq y x \/ In y r.
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.
Lemma is_empty_1 : forall s, Empty s -> is_empty s = true.
Lemma is_empty_2 : forall s, is_empty s = true -> Empty s.
Lemma mem_1 : forall s x, bst s -> In x s -> mem x s = true.
Lemma mem_2 : forall s x, mem x s = true -> In x s.
Lemma singleton_1 : forall x y, In y (singleton x) -> X.eq x y.
Lemma singleton_2 : forall x y, X.eq x y -> In y (singleton x).
Lemma singleton_bst : forall x : elt, bst (singleton x).
Lemma create_in :
forall l x r y, In y (create l x r) <-> X.eq y x \/ In y l \/ In y r.
Lemma create_bst :
forall l x r, bst l -> bst r -> lt_tree x l -> gt_tree x r ->
bst (create l x r).
Hint Resolve create_bst.
Lemma bal_in : forall l x r y,
In y (bal l x r) <-> X.eq y x \/ In y l \/ In y r.
Lemma bal_bst : forall l x r, bst l -> bst r ->
lt_tree x l -> gt_tree x r -> bst (bal l x r).
Hint Resolve bal_bst.
Lemma add_in : forall s x y,
In y (add x s) <-> X.eq y x \/ In y s.
Lemma add_bst : forall s x, bst s -> bst (add x s).
Hint Resolve add_bst.
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.
Lemma remove_min_in : forall l x r h y,
In y (Node l x r h) <->
X.eq y (remove_min l x r)#2 \/ In y (remove_min l x r)#1.
Lemma remove_min_bst : forall l x r h,
bst (Node l x r h) -> bst (remove_min l x r)#1.
Lemma remove_min_gt_tree : forall l x r h,
bst (Node l x r h) ->
gt_tree (remove_min l x r)#2 (remove_min l x r)#1.
Hint Resolve remove_min_bst remove_min_gt_tree.
Lemma merge_in : forall s1 s2 y,
In y (merge s1 s2) <-> In y s1 \/ In y s2.
Lemma merge_bst : forall s1 s2, bst s1 -> bst s2 ->
(forall y1 y2 : elt, In y1 s1 -> In y2 s2 -> X.lt y1 y2) ->
bst (merge s1 s2).
Hint Resolve merge_bst.
Lemma remove_in : forall s x y, bst s ->
(In y (remove x s) <-> ~ X.eq y x /\ In y s).
Lemma remove_bst : forall s x, bst s -> bst (remove x s).
Hint Resolve remove_bst.
Lemma min_elt_1 : forall s x, min_elt s = Some x -> In x s.
Lemma min_elt_2 : forall s x y, bst s ->
min_elt s = Some x -> In y s -> ~ X.lt y x.
Lemma min_elt_3 : forall s, min_elt s = None -> Empty s.
Lemma max_elt_1 : forall s x, max_elt s = Some x -> In x s.
Lemma max_elt_2 : forall s x y, bst s ->
max_elt s = Some x -> In y s -> ~ X.lt x y.
Lemma max_elt_3 : forall s, max_elt s = None -> Empty s.
Lemma choose_1 : forall s x, choose s = Some x -> In x s.
Lemma choose_2 : forall s, choose s = None -> Empty s.
Lemma choose_3 : forall s s', bst s -> bst s' ->
forall x x', choose s = Some x -> choose s' = Some x' ->
Equal s s' -> X.eq x x'.
Lemma concat_in : forall s1 s2 y,
In y (concat s1 s2) <-> In y s1 \/ In y s2.
Lemma concat_bst : forall s1 s2, bst s1 -> bst s2 ->
(forall y1 y2 : elt, In y1 s1 -> In y2 s2 -> X.lt y1 y2) ->
bst (concat s1 s2).
Hint Resolve concat_bst.
Lemma split_in_1 : forall s x y, bst s ->
(In y (split x s)#l <-> In y s /\ X.lt y x).
Lemma split_in_2 : forall s x y, bst s ->
(In y (split x s)#r <-> In y s /\ X.lt x y).
Lemma split_in_3 : forall s x, bst s ->
((split x s)#b = true <-> In x s).
Lemma split_bst : forall s x, bst s ->
bst (split x s)#l /\ bst (split x s)#r.
Lemma inter_bst_in : forall s1 s2, bst s1 -> bst s2 ->
bst (inter s1 s2) /\ (forall y, In y (inter s1 s2) <-> In y s1 /\ In y s2).
Lemma inter_in : forall s1 s2 y, bst s1 -> bst s2 ->
(In y (inter s1 s2) <-> In y s1 /\ In y s2).
Lemma inter_bst : forall s1 s2, bst s1 -> bst s2 -> bst (inter s1 s2).
Lemma diff_bst_in : forall s1 s2, bst s1 -> bst s2 ->
bst (diff s1 s2) /\ (forall y, In y (diff s1 s2) <-> In y s1 /\ ~In y s2).
Lemma diff_in : forall s1 s2 y, bst s1 -> bst s2 ->
(In y (diff s1 s2) <-> In y s1 /\ ~In y s2).
Lemma diff_bst : forall s1 s2, bst s1 -> bst s2 -> bst (diff s1 s2).
Lemma union_in : forall s1 s2 y, bst s1 -> bst s2 ->
(In y (union s1 s2) <-> In y s1 \/ In y s2).
Lemma union_bst : forall s1 s2, bst s1 -> bst s2 ->
bst (union s1 s2).
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.
Section F.
Variable f : elt -> bool.
Lemma filter_acc_in : forall s acc,
compat_bool X.eq f -> forall x : elt,
In x (filter_acc f acc s) <-> In x acc \/ In x s /\ f x = true.
Lemma filter_acc_bst : forall s acc, bst s -> bst acc ->
bst (filter_acc f acc s).
Lemma filter_in : forall s,
compat_bool X.eq f -> forall x : elt,
In x (filter f s) <-> In x s /\ f x = true.
Lemma filter_bst : forall s, bst s -> bst (filter f s).
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.
Lemma for_all_1 : forall s, compat_bool X.eq f ->
For_all (fun x => f x = true) s -> for_all f s = true.
Lemma for_all_2 : forall s, compat_bool X.eq f ->
for_all f s = true -> For_all (fun x => f x = true) s.
Lemma exists_1 : forall s, compat_bool X.eq f ->
Exists (fun x => f x = true) s -> exists_ f s = true.
Lemma exists_2 : forall s, compat_bool X.eq f ->
exists_ f s = true -> Exists (fun x => f x = true) s.
End F.
Definition fold' (A : Type) (f : elt -> A -> A)(s : tree) :=
L.fold f (elements s).
Implicit Arguments fold' [A].
Lemma fold_equiv_aux :
forall (A : Type) (s : tree) (f : elt -> A -> A) (a : A) (acc : list elt),
L.fold f (elements_aux acc s) a = L.fold f acc (fold f s a).
Lemma fold_equiv :
forall (A : Type) (s : tree) (f : elt -> A -> A) (a : A),
fold f s a = fold' f s a.
Lemma fold_1 :
forall (s:t)(Hs:bst s)(A : Type)(f : elt -> A -> A)(i : A),
fold f s i = fold_left (fun a e => f e a) (elements s) i.
Lemma subsetl_12 : forall subset_l1 l1 x1 h1 s2,
bst (Node l1 x1 Leaf h1) -> bst s2 ->
(forall s, bst s -> (subset_l1 s = true <-> Subset l1 s)) ->
(subsetl subset_l1 x1 s2 = true <-> Subset (Node l1 x1 Leaf h1) s2 ).
Lemma subsetr_12 : forall subset_r1 r1 x1 h1 s2,
bst (Node Leaf x1 r1 h1) -> bst s2 ->
(forall s, bst s -> (subset_r1 s = true <-> Subset r1 s)) ->
(subsetr subset_r1 x1 s2 = true <-> Subset (Node Leaf x1 r1 h1) s2).
Lemma subset_12 : forall s1 s2, bst s1 -> bst s2 ->
(subset s1 s2 = true <-> Subset s1 s2).
Definition eq := Equal.
Definition lt (s1 s2 : t) : Prop := L.lt (elements s1) (elements s2).
Lemma eq_refl : forall s : t, Equal s s.
Lemma eq_sym : forall s s' : t, Equal s s' -> Equal s' s.
Lemma eq_trans : forall s s' s'' : t,
Equal s s' -> Equal s' s'' -> Equal s s''.
Lemma eq_L_eq :
forall s s' : t, Equal s s' -> L.eq (elements s) (elements s').
Lemma L_eq_eq :
forall s s' : t, L.eq (elements s) (elements s') -> Equal s s'.
Hint Resolve eq_L_eq L_eq_eq.
Definition lt_trans (s s' s'' : t) (h : lt s s')
(h' : lt s' s'') : lt s s'' := L.lt_trans h h'.
Lemma lt_not_eq : forall s s' : t,
bst s -> bst s' -> lt s s' -> ~ Equal s s'.
Lemma L_eq_cons :
forall (l1 l2 : list elt) (x y : elt),
X.eq x y -> L.eq l1 l2 -> L.eq (x :: l1) (y :: l2).
Hint Resolve L_eq_cons.
flatten_e e returns the list of elements of e i.e. the list
of elements actually compared
Fixpoint flatten_e (e : enumeration) : list elt := match e with
| End => nil
| More x t r => x :: elements t ++ flatten_e r
end.
Lemma flatten_e_elements :
forall l x r h e,
elements l ++ flatten_e (More x r e) = elements (Node l x r h) ++ flatten_e e.
Lemma cons_1 : forall s e,
flatten_e (cons s e) = elements s ++ flatten_e e.
Correctness of this comparison
Definition Cmp c :=
match c with
| Eq => L.eq
| Lt => L.lt
| Gt => (fun l1 l2 => L.lt l2 l1)
end.
Lemma cons_Cmp : forall c x1 x2 l1 l2, X.eq x1 x2 ->
Cmp c l1 l2 -> Cmp c (x1::l1) (x2::l2).
Hint Resolve cons_Cmp.
Lemma compare_end_Cmp :
forall e2, Cmp (compare_end e2) nil (flatten_e e2).
Lemma compare_more_Cmp : forall x1 cont x2 r2 e2 l,
Cmp (cont (cons r2 e2)) l (elements r2 ++ flatten_e e2) ->
Cmp (compare_more x1 cont (More x2 r2 e2)) (x1::l)
(flatten_e (More x2 r2 e2)).
Lemma compare_cont_Cmp : forall s1 cont e2 l,
(forall e, Cmp (cont e) l (flatten_e e)) ->
Cmp (compare_cont s1 cont e2) (elements s1 ++ l) (flatten_e e2).
Lemma compare_Cmp : forall s1 s2,
Cmp (compare s1 s2) (elements s1) (elements s2).
Lemma equal_1 : forall s1 s2, bst s1 -> bst s2 ->
Equal s1 s2 -> equal s1 s2 = true.
Lemma equal_2 : forall s1 s2,
equal s1 s2 = true -> Equal s1 s2.
End Proofs.
End Raw.
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.
Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
Module E := X.
Module Raw := Raw I X.
Import Raw.Proofs.
Record bst := Bst {this :> Raw.t; is_bst : Raw.bst this}.
Definition t := bst.
Definition elt := E.t.
Definition In (x : elt) (s : t) := Raw.In x s.
Definition Equal (s s':t) := forall a : elt, In a s <-> In a s'.
Definition Subset (s s':t) := forall a : elt, In a s -> In a s'.
Definition Empty (s:t) := forall a : elt, ~ In a s.
Definition For_all (P : elt -> Prop) (s:t) := forall x, In x s -> P x.
Definition Exists (P : elt -> Prop) (s:t) := exists x, In x s /\ P x.
Lemma In_1 : forall (s:t)(x y:elt), E.eq x y -> In x s -> In y s.
Definition mem (x:elt)(s:t) : bool := Raw.mem x s.
Definition empty : t := Bst empty_bst.
Definition is_empty (s:t) : bool := Raw.is_empty s.
Definition singleton (x:elt) : t := Bst (singleton_bst x).
Definition add (x:elt)(s:t) : t := Bst (add_bst x (is_bst s)).
Definition remove (x:elt)(s:t) : t := Bst (remove_bst x (is_bst s)).
Definition inter (s s':t) : t := Bst (inter_bst (is_bst s) (is_bst s')).
Definition union (s s':t) : t := Bst (union_bst (is_bst s) (is_bst s')).
Definition diff (s s':t) : t := Bst (diff_bst (is_bst s) (is_bst s')).
Definition elements (s:t) : list elt := Raw.elements s.
Definition min_elt (s:t) : option elt := Raw.min_elt s.
Definition max_elt (s:t) : option elt := Raw.max_elt s.
Definition choose (s:t) : option elt := Raw.choose s.
Definition fold (B : Type) (f : elt -> B -> B) (s:t) : B -> B := Raw.fold f s.
Definition cardinal (s:t) : nat := Raw.cardinal s.
Definition filter (f : elt -> bool) (s:t) : t :=
Bst (filter_bst f (is_bst s)).
Definition for_all (f : elt -> bool) (s:t) : bool := Raw.for_all f s.
Definition exists_ (f : elt -> bool) (s:t) : bool := Raw.exists_ f s.
Definition partition (f : elt -> bool) (s:t) : t * t :=
let p := Raw.partition f s in
(@Bst (fst p) (partition_bst_1 f (is_bst s)),
@Bst (snd p) (partition_bst_2 f (is_bst s))).
Definition equal (s s':t) : bool := Raw.equal s s'.
Definition subset (s s':t) : bool := Raw.subset s s'.
Definition eq (s s':t) : Prop := Raw.Equal s s'.
Definition lt (s s':t) : Prop := Raw.Proofs.lt s s'.
Definition compare (s s':t) : Compare lt eq s s'.
Definition eq_dec (s s':t) : { eq s s' } + { ~ eq s s' }.
Section Specs.
Variable s s' s'': t.
Variable x y : elt.
Hint Resolve is_bst.
Lemma mem_1 : In x s -> mem x s = true.
Lemma mem_2 : mem x s = true -> In x s.
Lemma equal_1 : Equal s s' -> equal s s' = true.
Lemma equal_2 : equal s s' = true -> Equal s s'.
Ltac wrap t H := unfold t, In; simpl; rewrite H; auto; intuition.
Lemma subset_1 : Subset s s' -> subset s s' = true.
Lemma subset_2 : subset s s' = true -> Subset s s'.
Lemma empty_1 : Empty empty.
Lemma is_empty_1 : Empty s -> is_empty s = true.
Lemma is_empty_2 : is_empty s = true -> Empty s.
Lemma add_1 : E.eq x y -> In y (add x s).
Lemma add_2 : In y s -> In y (add x s).
Lemma add_3 : ~ E.eq x y -> In y (add x s) -> In y s.
Lemma remove_1 : E.eq x y -> ~ In y (remove x s).
Lemma remove_2 : ~ E.eq x y -> In y s -> In y (remove x s).
Lemma remove_3 : In y (remove x s) -> In y s.
Lemma singleton_1 : In y (singleton x) -> E.eq x y.
Lemma singleton_2 : E.eq x y -> In y (singleton x).
Lemma union_1 : In x (union s s') -> In x s \/ In x s'.
Lemma union_2 : In x s -> In x (union s s').
Lemma union_3 : In x s' -> In x (union s s').
Lemma inter_1 : In x (inter s s') -> In x s.
Lemma inter_2 : In x (inter s s') -> In x s'.
Lemma inter_3 : In x s -> In x s' -> In x (inter s s').
Lemma diff_1 : In x (diff s s') -> In x s.
Lemma diff_2 : In x (diff s s') -> ~ In x s'.
Lemma diff_3 : In x s -> ~ In x s' -> In x (diff s s').
Lemma fold_1 : forall (A : Type) (i : A) (f : elt -> A -> A),
fold f s i = fold_left (fun a e => f e a) (elements s) i.
Lemma cardinal_1 : cardinal s = length (elements s).
Section Filter.
Variable f : elt -> bool.
Lemma filter_1 : compat_bool E.eq f -> In x (filter f s) -> In x s.
Lemma filter_2 : compat_bool E.eq f -> In x (filter f s) -> f x = true.
Lemma filter_3 : compat_bool E.eq f -> In x s -> f x = true -> In x (filter f s).
Lemma for_all_1 : compat_bool E.eq f -> For_all (fun x => f x = true) s -> for_all f s = true.
Lemma for_all_2 : compat_bool E.eq f -> for_all f s = true -> For_all (fun x => f x = true) s.
Lemma exists_1 : compat_bool E.eq f -> Exists (fun x => f x = true) s -> exists_ f s = true.
Lemma exists_2 : compat_bool E.eq f -> exists_ f s = true -> Exists (fun x => f x = true) s.
Lemma partition_1 : compat_bool E.eq f ->
Equal (fst (partition f s)) (filter f s).
Lemma partition_2 : compat_bool E.eq f ->
Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
End Filter.
Lemma elements_1 : In x s -> InA E.eq x (elements s).
Lemma elements_2 : InA E.eq x (elements s) -> In x s.
Lemma elements_3 : sort E.lt (elements s).
Lemma elements_3w : NoDupA E.eq (elements s).
Lemma min_elt_1 : min_elt s = Some x -> In x s.
Lemma min_elt_2 : min_elt s = Some x -> In y s -> ~ E.lt y x.
Lemma min_elt_3 : min_elt s = None -> Empty s.
Lemma max_elt_1 : max_elt s = Some x -> In x s.
Lemma max_elt_2 : max_elt s = Some x -> In y s -> ~ E.lt x y.
Lemma max_elt_3 : max_elt s = None -> Empty s.
Lemma choose_1 : choose s = Some x -> In x s.
Lemma choose_2 : choose s = None -> Empty s.
Lemma choose_3 : choose s = Some x -> choose s' = Some y ->
Equal s s' -> E.eq x y.
Lemma eq_refl : eq s s.
Lemma eq_sym : eq s s' -> eq s' s.
Lemma eq_trans : eq s s' -> eq s' s'' -> eq s s''.
Lemma lt_trans : lt s s' -> lt s' s'' -> lt s s''.
Lemma lt_not_eq : lt s s' -> ~eq s s'.
End Specs.
End IntMake.
Module Make (X: OrderedType) <: S with Module E := X
:=IntMake(Z_as_Int)(X).