Library FSetAVL

This module implements sets using AVL trees. It follows the implementation from Ocaml's standard library.




Require FSetInterface.

Require FSetList.

Require ZArith.

Import Z_scope.

Open Scope Z_scope.

Notation "[]" := (nil ?) (at level 1).

Notation "a :: l" := (cons a l) (at level 1, l at next level).

Set Ground Depth 3.

Module Make [X : OrderedType] <: Sdep with Module E := X.

  Module E := X.

  Module ME := MoreOrderedType X.

  Definition elt := X.t.

Trees

Inductive tree : Set := | Leaf : tree | Node : tree -> X.t -> tree -> Z -> tree.

The fourth field of Node is the height of the tree

Occurrence in a tree

Inductive In_tree [x:elt] : tree -> Prop := | IsRoot : (l,r:tree)(h:Z)(y:elt) (X.eq x y) -> (In_tree x (Node l y r h)) | InLeft : (l,r:tree)(h:Z)(y:elt) (In_tree x l) -> (In_tree x (Node l y r h)) | InRight : (l,r:tree)(h:Z)(y:elt) (In_tree x r) -> (In_tree x (Node l y r h)).

Hint In_tree := Constructors In_tree.

In_tree is compatible with X.eq

Lemma eq_In_tree: (s:tree)(x,y:elt)(E.eq x y) -> (In_tree x s) -> (In_tree y s).

In_tree is height-insensitive

Lemma In_height : (h,h':Z)(x,y:elt)(l,r:tree) (In_tree y (Node l x r h)) -> (In_tree y (Node l x r h')). Hints Resolve In_height.

Binary search trees

lt_tree x s: all elements in s are smaller than x (resp. greater for gt_tree)

Definition lt_tree [x:elt; s:tree] := (y:elt)(In_tree y s) -> (X.lt y x). Definition gt_tree [x:elt; s:tree] := (y:elt)(In_tree y s) -> (X.lt x y).

Hints Unfold lt_tree gt_tree.

Results about lt_tree and gt_tree

Lemma lt_leaf : (x:elt)(lt_tree x Leaf).

Lemma gt_leaf : (x:elt)(gt_tree x Leaf).

Lemma lt_tree_node : (x,y:elt)(l,r:tree)(h:Z) (lt_tree x l) -> (lt_tree x r) -> (X.lt y x) -> (lt_tree x (Node l y r h)).

Lemma gt_tree_node : (x,y:elt)(l,r:tree)(h:Z) (gt_tree x l) -> (gt_tree x r) -> (E.lt x y) -> (gt_tree x (Node l y r h)).

Hints Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node.

Lemma lt_node_lt : (x,y:elt)(l,r:tree)(h:Z) (lt_tree x (Node l y r h)) -> (E.lt y x).

Lemma gt_node_gt : (x,y:elt)(l,r:tree)(h:Z) (gt_tree x (Node l y r h)) -> (E.lt x y).

Lemma lt_left : (x,y:elt)(l,r:tree)(h:Z) (lt_tree x (Node l y r h)) -> (lt_tree x l).

Lemma lt_right : (x,y:elt)(l,r:tree)(h:Z) (lt_tree x (Node l y r h)) -> (lt_tree x r).

Lemma gt_left : (x,y:elt)(l,r:tree)(h:Z) (gt_tree x (Node l y r h)) -> (gt_tree x l).

Lemma gt_right : (x,y:elt)(l,r:tree)(h:Z) (gt_tree x (Node l y r h)) -> (gt_tree x r).

Hints Resolve lt_node_lt gt_node_gt lt_left lt_right gt_left gt_right.

Lemma lt_tree_not_in : (x:elt)(t:tree)(lt_tree x t) -> ~(In_tree x t).

Lemma lt_tree_trans : (x,y:elt)(X.lt x y) -> (t:tree)(lt_tree x t) -> (lt_tree y t).

Lemma gt_tree_not_in : (x:elt)(t:tree)(gt_tree x t) -> ~(In_tree x t).

Lemma gt_tree_trans : (x,y:elt)(X.lt y x) -> (t:tree)(gt_tree x t) -> (gt_tree y t).

Hints Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans.

bst t : t is a binary search tree

Inductive bst : tree -> Prop := | BSLeaf : (bst Leaf) | BSNode : (x:elt)(l,r:tree)(h:Z) (bst l) -> (bst r) -> (lt_tree x l) -> (gt_tree x r) -> (bst (Node l x r h)).

Hint bst := Constructors bst.

Results about bst
Lemma bst_left : (x:elt)(l,r:tree)(h:Z) (bst (Node l x r h)) -> (bst l).

Lemma bst_right : (x:elt)(l,r:tree)(h:Z) (bst (Node l x r h)) -> (bst r).

Implicits bst_left. Implicits bst_right. Hints Resolve bst_left bst_right.

Lemma bst_height : (h,h':Z)(x:elt)(l,r:tree) (bst (Node l x r h)) -> (bst (Node l x r h')). Hints Resolve bst_height.

Key fact about binary search trees: rotations preserve the bst property

Lemma rotate_left : (x,y:elt)(a,b,c:tree)(h1,h2,h3,h4:Z) (bst (Node a x (Node b y c h2) h1)) -> (bst (Node (Node a x b h4) y c h3)).

Lemma rotate_right : (x,y:elt)(a,b,c:tree)(h1,h2,h3,h4:Z) (bst (Node (Node a x b h4) y c h3)) -> (bst (Node a x (Node b y c h2) h1)).

Hints Resolve rotate_left rotate_right.

AVL trees

avl s : s is a properly balanced AVL tree, i.e. for any node the heights of the two children differ by at most 2

Definition height : tree -> Z := [s:tree]Cases s of | Leaf => 0 | (Node _ _ _ h) => h end.

Definition max [x,y:Z] : Z := if (Z_lt_ge_dec x y) then [_]y else [_]x.

Instead of writing h = 1 + (max (height l) (height r)) we prefer the following relation height_of_node l r h to ease the use of Omega

Definition height_of_node [l,r:tree; h:Z] := ((height l) >= (height r) /\ h = (height l) + 1) \/ ((height r) >= (height l) /\ h = (height r) + 1).

Inductive avl : tree -> Prop := | RBLeaf : (avl Leaf) | RBNode : (x:elt)(l,r:tree)(h:Z) (avl l) -> (avl r) -> `-2 <= (height l) - (height r) <= 2` -> (height_of_node l r h) -> (avl (Node l x r h)).

Hint avl := Constructors avl.

Results about avl

Lemma avl_left : (x:elt)(l,r:tree)(h:Z) (avl (Node l x r h)) -> (avl l).

Lemma avl_right : (x:elt)(l,r:tree)(h:Z) (avl (Node l x r h)) -> (avl l).

Implicits avl_left. Implicits avl_right. Hints Resolve avl_left avl_right.

Tactic Definition MaxCase x y := Unfold max; Case (Z_lt_ge_dec x y); Simpl.

Lemma avl_node: (x:elt)(l,r:tree) (avl l) -> (avl r) -> `-2 <= (height l) - (height r) <= 2` -> (avl (Node l x r ((max (height l) (height r)) + 1))). Hints Resolve avl_node.

The AVL tactic

Lemma height_non_negative : (s:tree)(avl s) -> (height s) >= 0. Lemma height_equation : (l,r:tree)(x:elt)(h:Z) (avl (Node l x r h)) -> `-2 <= (height l) - (height r) <= 2` /\ (((height l) >= (height r) /\ h = (height l) + 1) \/ ((height r) >= (height l) /\ h = (height r) + 1)).

Implicits height_non_negative. Implicits height_equation.

If h is a proof of avl (Node l x r h), then tactic AVL h is adding all information about h to the context
Tactic Definition AVL h := (Generalize (height_non_negative h); Try Simpl); (Try Generalize (height_equation h)); Intros.

Sets as AVL trees

A set is implement as a record t, containing a tree, a proof that it is a binary search tree and a proof that it is a properly balanced AVL tree

Record t_ : Set := t_intro { the_tree :> tree; is_bst : (bst the_tree); is_avl : (avl the_tree) }. Definition t := t_.

Projections

Lemma t_is_bst : (s:t)(bst s). Hints Resolve t_is_bst.

Lemma t_is_avl : (s:t)(avl s). Hints Resolve t_is_avl.

Logical appartness

Definition In : elt -> t -> Prop := [x:elt][s:t](In_tree x s).

Definition Equal := [s,s'](a:elt)(In a s)<->(In a s'). Definition Subset := [s,s'](a:elt)(In a s)->(In a s'). Definition Add := [x:elt;s,s':t](y:elt)(In y s') <-> ((E.eq y x)\/(In y s)). Definition Empty := [s](a:elt)~(In a s). Definition For_all := [P:elt->Prop; s:t](x:elt)(In x s)->(P x). Definition Exists := [P:elt->Prop; s:t](EX x:elt | (In x s)/\(P x)).

Lemma eq_In: (s:t)(x,y:elt)(E.eq x y) -> (In x s) -> (In y s).

Hints Resolve eq_In.

Empty set

Definition t_empty : t.

Definition empty : { s:t | (x:elt)~(In x s) }.

Emptyness test

Definition is_empty : (s:t){ Empty s }+{ ~(Empty s) }.

Appartness

The mem function is deciding appartness. It exploits the bst property to achieve logarithmic complexity.

Definition mem : (x:elt) (s:t) { (In x s) } + { ~(In x s) }.

Singleton set

Definition singleton_tree [x:elt] := (Node Leaf x Leaf 1).

Lemma singleton_bst : (x:elt)(bst (singleton_tree x)).

Lemma singleton_avl : (x:elt)(avl (singleton_tree x)).

Definition singleton : (x:elt){ s:t | (y:elt)(In y s) <-> (E.eq x y)}.

Helper functions

create l x r creates a node, assuming l and r to be balanced and |height l - height r| <= 2.

Definition create : (l:tree)(x:elt)(r:tree) (bst l) -> (avl l) -> (bst r) -> (avl r) -> (lt_tree x l) -> (gt_tree x r) -> `-2 <= (height l) - (height r) <= 2` -> { s:tree | (bst s) /\ (avl s) /\ (height_of_node l r (height s)) /\ (y:elt)(In_tree y s) <-> ((X.eq y x) \/ (In_tree y l) \/ (In_tree y r)) }.

bal l x r acts as create, but performs one step of rebalancing if necessary, i.e. assumes |height l - height r| <= 3.

Definition bal : (l:tree)(x:elt)(r:tree) (bst l) -> (avl l) -> (bst r) -> (avl r) -> (lt_tree x l) -> (gt_tree x r) -> `-3 <= (height l) - (height r) <= 3` -> { s:tree | (bst s) /\ (avl s) /\ (((height_of_node l r (height s)) \/ (height_of_node l r ((height s) + 1))) /\ (`-2 <= (height l) - (height r) <= 2` -> (height_of_node l r (height s)))) /\ (y:elt)(In_tree y s) <-> ((X.eq y x) \/ (In_tree y l) \/ (In_tree y r)) }.

Insertion

Definition add_tree : (x:elt)(s:tree)(bst s) -> (avl s) -> { s':tree | (bst s') /\ (avl s') /\ 0 <= (height s')-(height s) <= 1 /\ ((y:elt)(In_tree y s') <-> ((E.eq y x)\/(In_tree y s))) }.

Definition add : (x:elt) (s:t) { s':t | (Add x s s') }.

Join

Same as bal but does not assumme anything regarding heights of l and r. Code is
let rec join l v r = match (l, r) with (Empty, _) -> add v r | (_, Empty) -> add v l | (Node(ll, lv, lr, lh), Node(rl, rv, rr, rh)) -> if lh > rh + 2 then bal ll lv (join lr v r) else if rh > lh + 2 then bal (join l v rl) rv rr else create l v r

Definition join : (l:tree)(x:elt)(r:tree) (bst l) -> (avl l) -> (bst r) -> (avl r) -> (lt_tree x l) -> (gt_tree x r) -> { s:tree | (bst s) /\ (avl s) /\ ((height_of_node l r (height s)) \/ (height_of_node l r ((height s)+1))) /\ ((y:elt)(In_tree y s) <-> ((X.eq y x) \/ (In_tree y l) \/ (In_tree y r))) }.

Extraction of minimum and maximum element

Definition remove_min : (s:tree)(bst s) -> (avl s) -> ~s=Leaf -> { r : tree * elt | let (s',m) = r in (bst s') /\ (avl s') /\ ((height s') = (height s) \/ (height s')=(height s)-1) /\ ((y:elt)(In_tree y s') -> (E.lt m y)) /\ ((y:elt)(In_tree y s) <-> (E.eq y m) \/ (In_tree y s')) }.

Definition remove_max : (s:tree)(bst s) -> (avl s) -> ~s=Leaf -> { r : tree * elt | let (s',m) = r in (bst s') /\ (avl s') /\ ((height s') = (height s) \/ (height s')=(height s)-1) /\ ((y:elt)(In_tree y s') -> (E.lt y m)) /\ ((y:elt)(In_tree y s) <-> (E.eq y m) \/ (In_tree y s')) }.

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. Code is
let merge t1 t2 = match (t1, t2) with (Empty, t) -> t | (t, Empty) -> t | (_, _) -> let (m,t'2) = remove_min t2 in bal t1 m t'2

Definition merge : (s1,s2:tree)(bst s1) -> (avl s1) -> (bst s2) -> (avl s2) -> ((y1,y2:elt)(In_tree y1 s1) -> (In_tree y2 s2) -> (X.lt y1 y2)) -> `-2 <= (height s1) - (height s2) <= 2` -> { s:tree | (bst s) /\ (avl s) /\ ((height_of_node s1 s2 (height s)) \/ (height_of_node s1 s2 ((height s)+1))) /\ ((y:elt)(In_tree y s) <-> ((In_tree y s1) \/ (In_tree y s2))) }.

Variant where we remove from the biggest subtree

Definition merge_bis : (s1,s2:tree)(bst s1) -> (avl s1) -> (bst s2) -> (avl s2) -> ((y1,y2:elt)(In_tree y1 s1) -> (In_tree y2 s2) -> (X.lt y1 y2)) -> `-2 <= (height s1) - (height s2) <= 2` -> { s:tree | (bst s) /\ (avl s) /\ ((height_of_node s1 s2 (height s)) \/ (height_of_node s1 s2 ((height s)+1))) /\ ((y:elt)(In_tree y s) <-> ((In_tree y s1) \/ (In_tree y s2))) }.

Deletion

Definition remove_tree : (x:elt)(s:tree)(bst s) -> (avl s) -> { s':tree | (bst s') /\ (avl s') /\ ((height s') = (height s) \/ (height s') = (height s) - 1) /\ ((y:elt)(In_tree y s') <-> (~(E.eq y x) /\ (In_tree y s))) }.

Definition remove : (x:elt)(s:t) { s':t | (y:elt)(In y s') <-> (~(E.eq y x) /\ (In y s))}.

Minimum element

Definition min_elt : (s:t){ x:elt | (In x s) /\ (For_all [y]~(E.lt y x) s) } + { Empty s }.

Maximum element

Definition max_elt : (s:t){ x:elt | (In x s) /\ (For_all [y]~(E.lt x y) s) } + { Empty s }.

Any element

Definition choose : (s:t) { x:elt | (In x s)} + { Empty s }.

Concatenation

Same as merge but does not assume anything about heights. Code is
let concat t1 t2 = match (t1, t2) with (Empty, t) -> t | (t, Empty) -> t | (_, _) -> join t1 (min_elt t2) (remove_min_elt t2)

Definition concat : (s1,s2:tree)(bst s1) -> (avl s1) -> (bst s2) -> (avl s2) -> ((y1,y2:elt)(In_tree y1 s1) -> (In_tree y2 s2) -> (X.lt y1 y2)) -> { s:tree | (bst s) /\ (avl s) /\ ((y:elt)(In_tree y s) <-> ((In_tree y s1) \/ (In_tree y s2))) }.

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.

let rec split x = function Empty -> (Empty, false, Empty) | Node(l, v, r, _) -> let c = Ord.compare x v in if c = 0 then (l, true, r) else if c < 0 then let (ll, pres, rl) = split x l in (ll, pres, join rl v r) else let (lr, pres, rr) = split x r in (join l v lr, pres, rr)

Definition split : (x:elt)(s:tree)(bst s) -> (avl s) -> { res:tree*bool*tree | let (l,res') = res in let (b,r) = res' in (bst l) /\ (avl l) /\ (bst r) /\ (avl r) /\ ((y:elt)(In_tree y l) <-> ((In_tree y s) /\ (X.lt y x))) /\ ((y:elt)(In_tree y r) <-> ((In_tree y s) /\ (X.lt x y))) /\ (b=true <-> (In_tree x s)) }.

Intersection

let rec inter s1 s2 = match (s1, s2) with (Empty, t2) -> Empty | (t1, Empty) -> Empty | (Node(l1, v1, r1, _), t2) -> match split v1 t2 with (l2, false, r2) -> concat (inter l1 l2) (inter r1 r2) | (l2, true, r2) -> join (inter l1 l2) v1 (inter r1 r2)

Definition inter : (s1,s2:t) { s':t | (x:elt)(In x s') <-> ((In x s1)/\(In x s2))}.

Difference

let rec diff s1 s2 = match (s1, s2) with (Empty, t2) -> Empty | (t1, Empty) -> t1 | (Node(l1, v1, r1, _), t2) -> match split v1 t2 with (l2, false, r2) -> join (diff l1 l2) v1 (diff r1 r2) | (l2, true, r2) -> concat (diff l1 l2) (diff r1 r2)

Definition diff : (s1,s2:t) { s':t | (x:elt)(In x s') <-> ((In x s1) /\ ~(In x s2))}.

Elements

elements_tree_aux acc t catenates the elements of t in infix order to the list acc

Fixpoint elements_tree_aux [acc:(list X.t); t:tree] : (list X.t) := Cases t of | Leaf => acc | (Node l x r _) => (elements_tree_aux (x :: (elements_tree_aux acc r)) l) end.

then elements_tree is an instanciation with an empty acc

Definition elements_tree := (elements_tree_aux []).

Lemma elements_tree_aux_acc_1 : (s:tree)(acc:(list elt)) (x:elt)(InList E.eq x acc)->(InList E.eq x (elements_tree_aux acc s)). Hints Resolve elements_tree_aux_acc_1.

Lemma elements_tree_aux_1 : (s:tree)(acc:(list elt)) (x:elt)(In_tree x s)->(InList E.eq x (elements_tree_aux acc s)).

Lemma elements_tree_1 : (s:tree) (x:elt)(In_tree x s)->(InList E.eq x (elements_tree s)). Hints Resolve elements_tree_1.

Lemma elements_tree_aux_acc_2 : (s:tree)(acc:(list elt)) (x:elt)(InList E.eq x (elements_tree_aux acc s)) -> (InList E.eq x acc) \/ (In_tree x s). Hints Resolve elements_tree_aux_acc_2.

Lemma elements_tree_2 : (s:tree) (x:elt)(InList E.eq x (elements_tree s)) -> (In_tree x s). Hints Resolve elements_tree_2.

Lemma elements_tree_aux_sort : (s:tree)(bst s) -> (acc:(list elt)) (sort E.lt acc) -> ((x:elt)(InList E.eq x acc) -> (y:elt)(In_tree y s) -> (E.lt y x)) -> (sort E.lt (elements_tree_aux acc s)).

Lemma elements_tree_sort : (s:tree)(bst s) -> (sort E.lt (elements_tree s)). Hints Resolve elements_tree_sort.

Definition elements : (s:t){ l:(list elt) | (sort E.lt l) /\ (x:elt)(In x s)<->(InList E.eq x l)}.

Cardinal

Fixpoint cardinal_tree [s:tree] : nat := Cases s of | Leaf => O | (Node l _ r _) => (S (plus (cardinal_tree l) (cardinal_tree r))) end.

Lemma cardinal_elements_1 : (s:tree)(acc:(list X.t)) (plus (length acc) (cardinal_tree s)) = (length (elements_tree_aux acc s)).

Lemma cardinal_elements_2 : (s:tree)(cardinal_tree s)=(length (elements_tree s)).

Definition cardinal : (s:t) { r : nat | (EX l:(list elt) | (Unique E.eq l) /\ ((x:elt)(In x s)<->(InList E.eq x l)) /\ r = (length l)) }.

Induction over cardinals

Lemma sorted_subset_cardinal : (l',l:(list X.t))(sort X.lt l) -> (sort X.lt l') -> ((x:elt)(InList X.eq x l) -> (InList X.eq x l')) -> (le (length l) (length l')).

Lemma cardinal_subset : (a,b:tree)(bst a) -> (bst b) -> ((y:elt)(In_tree y a) -> (In_tree y b)) -> (le (cardinal_tree a) (cardinal_tree b)).

Lemma cardinal_left : (l,r:tree)(x:elt)(h:Z) (lt (cardinal_tree l) (cardinal_tree (Node l x r h))).

Lemma cardinal_right : (l,r:tree)(x:elt)(h:Z) (lt (cardinal_tree r) (cardinal_tree (Node l x r h))).

Lemma cardinal_rec2 : (P:tree->tree->Set) ((x,x':tree) ((y,y':tree)(lt (plus (cardinal_tree y) (cardinal_tree y')) (plus (cardinal_tree x) (cardinal_tree x'))) ->(P y y')) -> (P x x')) -> (x,x':tree)(P x x').

Lemma height_0 : (s:tree)(avl s) -> (height s)=0 -> (x:elt)~(In_tree x s). Implicits height_0.

Union

union s1 s2 does an induction over the sum of the cardinals of s1 and s2. Code is
let rec union s1 s2 = match (s1, s2) with (Empty, t2) -> t2 | (t1, Empty) -> t1 | (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) -> if h1 >= h2 then if h2 = 1 then add v2 s1 else begin let (l2, _, r2) = split v1 s2 in join (union l1 l2) v1 (union r1 r2) end else if h1 = 1 then add v1 s2 else begin let (l1, _, r1) = split v2 s1 in join (union l1 l2) v2 (union r1 r2) end

Definition union : (s1,s2:t) { s':t | (x:elt)(In x s') <-> ((In x s1)\/(In x s2))}.

Filter

let filter p s = let rec filt accu = function | Empty -> accu | Node(l, v, r, _) -> filt (filt (if p v then add v accu else accu) l) r in filt Empty s

Definition filter_acc : (P:elt->Prop)(Pdec:(x:elt){P x}+{~(P x)}) (s,acc:tree)(bst s) -> (avl s) -> (bst acc) -> (avl acc) -> { s':tree | (bst s') /\ (avl s') /\ ((compat_P E.eq P) -> (x:elt)(In_tree x s') <-> ((In_tree x acc) \/ ((In_tree x s)/\(P x)))) }.

Definition filter : (P:elt->Prop)(Pdec:(x:elt){P x}+{~(P x)})(s:t) { s':t | (compat_P E.eq P) -> (x:elt)(In x s') <-> ((In x s)/\(P x)) }.

Partition

let partition p s = let rec part (t, f as accu) = function | Empty -> accu | Node(l, v, r, _) -> part (part (if p v then (add v t, f) else (t, add v f)) l) r in part (Empty, Empty) s

Definition partition_acc : (P:elt->Prop)(Pdec:(x:elt){P x}+{~(P x)}) (s,acct,accf:tree) (bst s) -> (avl s) -> (bst acct) -> (avl acct) -> (bst accf) -> (avl accf) -> { partition : tree*tree | let (s1,s2) = partition in (bst s1) /\ (avl s1) /\ (bst s2) /\ (avl s2) /\ ((compat_P E.eq P) -> (x:elt)(((In_tree x s1) <-> ((In_tree x acct) \/ ((In_tree x s) /\ (P x)))) /\ (((In_tree x s2) <-> ((In_tree x accf) \/ ((In_tree x s) /\ ~(P x))))))) }.

Definition partition : (P:elt->Prop)(Pdec:(x:elt){P x}+{~(P x)})(s:t) { partition : t*t | let (s1,s2) = partition in (compat_P E.eq P) -> ((For_all P s1) /\ (For_all ([x]~(P x)) s2) /\ (x:elt)(In x s)<->((In x s1)\/(In x s2))) }.

Subset

let rec subset s1 s2 = match (s1, s2) with Empty, _ -> true | _, Empty -> false | Node (l1, v1, r1, _), (Node (l2, v2, r2, _) as t2) -> let c = Ord.compare v1 v2 in if c = 0 then subset l1 l2 && subset r1 r2 else if c < 0 then subset (Node (l1, v1, Empty, 0)) l2 && subset r1 t2 else subset (Node (Empty, v1, r1, 0)) r2 && subset l1 t2

Definition subset : (s1,s2:t){ Subset s1 s2 } + { ~(Subset s1 s2) }.

for_all and exists

Definition for_all : (P:elt->Prop)(Pdec:(x:elt){P x}+{~(P x)})(s:t) { (compat_P E.eq P) -> (For_all P s) } + { (compat_P E.eq P) -> ~(For_all P s) }.

Definition exists : (P:elt->Prop)(Pdec:(x:elt){P x}+{~(P x)})(s:t) { (compat_P E.eq P) -> (Exists P s) } + { (compat_P E.eq P) -> ~(Exists P s) }.

Fold

Module L := Raw(E).

Fixpoint fold_tree [A:Set; f:elt->A->A; s:tree] : A -> A := Cases s of | Leaf => [a]a | (Node l x r _) => [a](fold_tree A f l (f x (fold_tree A f r a))) end. Implicits fold_tree [1].

Definition fold_tree' := [A:Set; f:elt->A->A; s:tree] (L.fold f (elements_tree s)). Implicits fold_tree' [1].

Lemma fold_tree_equiv_aux : (A:Set)(s:tree)(f:elt->A->A)(a:A; acc : (list elt)) (L.fold f (elements_tree_aux acc s) a) = (fold_tree f s (L.fold f acc a)).

Lemma fold_tree_equiv : (A:Set)(s:tree)(f:elt->A->A; a:A) (fold_tree f s a)=(fold_tree' f s a).

Definition fold : (A:Set)(f:elt->A->A)(s:t)(i:A) { r : A | (EX l:(list elt) | (Unique E.eq l) /\ ((x:elt)(In x s)<->(InList E.eq x l)) /\ r = (fold_right f i l)) }.

Comparison

Relations eq and lt over trees

Definition eq : t -> t -> Prop := Equal.

Lemma eq_refl: (s:t)(eq s s).

Lemma eq_sym: (s,s':t)(eq s s') -> (eq s' s).

Lemma eq_trans: (s,s',s'':t)(eq s s') -> (eq s' s'') -> (eq s s'').

Lemma eq_L_eq : (s,s':t) (eq s s') -> (L.eq (elements_tree s) (elements_tree s')).

Lemma L_eq_eq : (s,s':t) (L.eq (elements_tree s) (elements_tree s')) -> (eq s s'). Hints Resolve eq_L_eq L_eq_eq.

Definition lt : t -> t -> Prop := [s1,s2:t](L.lt (elements_tree s1) (elements_tree s2)).

Definition lt_trans : (s,s',s'':t)(lt s s') -> (lt s' s'') -> (lt s s'') := [s,s',s'':t][h][h'](L.lt_trans h h').

Lemma lt_not_eq : (s,s':t)(lt s s') -> ~(eq s s').

Comparison algorithm

The code for compare s1 s2 is basically comparing elements s1 and elements s2 in lexicographic order. But it builds these lists lazily (it is doing deforestation). It uses a function compare_aux comparing two lists of trees.
We slightly modify the original code to get a simplest termination argument. The resulting code is even a bit more efficient.
let rec compare_aux l1 l2 = match (l1, l2) with ([], []) -> 0 | ([], _) -> -1 | (_, []) -> 1 | (Empty :: t1, Empty :: t2) -> compare_aux t1 t2 | (Node(Empty, v1, r1, _) :: t1, Node(Empty, v2, r2, _) :: t2) -> let c = Ord.compare v1 v2 in if c <> 0 then c else compare_aux (r1::t1) (r2::t2) | (Node(Empty, v1, r1, _) :: t1, Empty :: t2) -> compare_aux (Node(Empty, v1, r1, 0) :: t1) t2 | (Node(l1, v1, r1, _) :: t1, t2) when l1 <> Empty -> compare_aux (l1 :: Node(Empty, v1, r1, 0) :: t1) t2 | (Empty :: t1, Node(Empty, v2, r2, _) :: t2) -> compare_aux t1 (Node(Empty, v2, r2, 0) :: t2) | (t1, Node(l2, v2, r2, _) :: t2) (* when l2 <> Empty *) -> compare_aux t1 (l2 :: Node(Empty, v2, r2, 0) :: t2)

Lists of trees

flatten l returns the list of elements of l i.e. the list of elements actually compared
Fixpoint flatten [l:(list tree)] : (list elt) := Cases l of | nil => [] | (cons t r) => (app (elements_tree t) (flatten r)) end.

sorted_l l expresses that elements in the trees of l are sorted, and that all trees in l are binary search trees.

Inductive In_tree_l : elt -> (list tree) -> Prop := | InHd : (x:elt)(s:tree)(l:(list tree))(In_tree x s) -> (In_tree_l x (cons s l)) | InTl : (x:elt)(s:tree)(l:(list tree))(In_tree_l x l) -> (In_tree_l x (cons s l)).

Hint In_tree_l := Constructors In_tree_l.

Inductive sorted_l : (list tree) -> Prop := | SortedLNil : (sorted_l []) | SortedLCons : (s:tree)(l:(list tree)) (bst s) -> (sorted_l l) -> ((x:elt)(In_tree x s) -> (y:elt)(In_tree_l y l) -> (X.lt x y)) -> (sorted_l (cons s l)).

Hint sorted_l := Constructors sorted_l.

Lemma sort_app : (l1,l2:(list elt))(sort E.lt l1) -> (sort E.lt l2) -> ((x,y:elt)(InList E.eq x l1) -> (InList E.eq y l2) -> (X.lt x y)) -> (sort E.lt (app l1 l2)).

Lemma in_app : (x:elt)(l1,l2:(list elt)) (InList E.eq x (app l1 l2)) -> ((InList E.eq x l1) \/ (InList E.eq x l2)).

Lemma in_flatten : (x:elt)(l:(list tree)) (InList E.eq x (flatten l)) -> (In_tree_l x l).

Lemma sorted_flatten : (l:(list tree))(sorted_l l) -> (sort E.lt (flatten l)).

Termination of compare_aux

The measure is given by m([]) = 0, m(s :: l) = m(s) + m(l), m(Leaf) = 1, and m(Node(l,_,r,_) = 1 + 3m(l) + m(r)

Fixpoint measure_t [s:tree] : Z := Cases s of Leaf => 1 | (Node l _ r _) => 1+3*(measure_t l)+(measure_t r) end.

Fixpoint measure_l [l:(list tree)] : Z := Cases l of nil => 0 | (cons s l) => (measure_t s)+(measure_l l) end.

Tactic Definition Measure_t := Unfold measure_t; Fold measure_t. Tactic Definition Measure_l := Unfold measure_l; Fold measure_l.

Lemma measure_t_1 : (s:tree)(measure_t s) >= 1.

Tactic Definition Measure_t_1 s := Generalize (measure_t_1 s); Intro.

Lemma measure_t_3 : (l,r:tree)(x:elt)(z:Z) (measure_t (Node l x r z)) >= 3.

Tactic Definition Measure_t_3 l x r z := Generalize (measure_t_3 l x r z); Intro.

Lemma measure_l_0 : (l:(list tree))(measure_l l)>=0.

Tactic Definition Measure_l_0 l := Generalize (measure_l_0 l); Intro.

Induction principle over the sum of the measures for two lists

Definition compare_rec2 : (P:(list tree)->(list tree)->Set) ((x,x':(list tree)) ((y,y':(list tree)) (measure_l y)+(measure_l y') < (measure_l x)+(measure_l x') ->(P y y')) -> (P x x')) -> (x,x':(list tree))(P x x').

Lemmas for the correctness of compare

Lemma lt_nil_elements_tree_Node : (l,r:tree)(x:elt)(z:Z)(L.lt [] (elements_tree (Node l x r z))).

Lemma lt_app : (l1,l2,l3:(list elt)) (L.lt l1 l2) -> (L.lt l1 (app l2 l3)).

Lemma lt_app_eq : (l1,l2,l3:(list elt)) (L.lt l2 l3) -> (L.lt (app l1 l2) (app l1 l3)).

Lemma lt_eq_1 : (l1,l2,l3:(list elt)) l1=l2 -> (L.lt l1 l3) -> (L.lt l2 l3).

Lemma lt_eq_2 : (l1,l2,l3:(list elt)) l2=l3 -> (L.lt l1 l2) -> (L.lt l1 l3).

Lemma eq_eq_1 : (l1,l2,l3:(list elt)) l1=l2 -> (L.eq l1 l3) -> (L.eq l2 l3).

Lemma eq_eq_2 : (l1,l2,l3:(list elt)) l2=l3 -> (L.eq l1 l2) -> (L.eq l1 l3).

Lemma l_eq_cons : (l1,l2:(list elt))(x,y:elt) (X.eq x y) -> (L.eq l1 l2) -> (L.eq (x :: l1) (y :: l2)).

Hints Resolve lt_nil_elements_tree_Node lt_app lt_app_eq lt_eq_1 lt_eq_2 eq_eq_1 eq_eq_2 l_eq_cons.

Lemma elements_app : (s:tree)(acc:(list elt)) (elements_tree_aux acc s) = (app (elements_tree s) acc).

main lemma for correctness of compare
Lemma compare_flatten : (l,r:tree)(x:elt)(z:Z)(tl:(list tree)) (flatten ((Node l x r z) :: tl)) = (flatten (l :: ((Node Leaf x r z) :: tl))).

Hints Resolve compare_flatten.

same lemma, expressed differently
Lemma compare_flatten_1 : (t0,t2:tree)(t1:elt)(z:Z)(l:(list elt)) (app (elements_tree t0) (t1 :: (app (elements_tree t2) l))) = (app (elements_tree (Node t0 t1 t2 z)) l).

Hints Resolve compare_flatten_1.

invariant for compare l1 l2: Leaf may only occur on head of l1 and l2, and only when the other list is non-empty

Fixpoint no_leaf [l:(list tree)] : Prop := Cases l of | nil => True | (cons Leaf _) => False | (cons _ r) => (no_leaf r) end.

Inductive leaf_invariant : (list tree) -> (list tree) -> Prop := | LI_nil_l : (l:(list tree)) (no_leaf l) -> (leaf_invariant [] l) | LI_l_nil : (l:(list tree)) (no_leaf l) -> (leaf_invariant l []) | LI_leaf_leaf : (l1,l2:(list tree))(no_leaf l1) -> (no_leaf l2) -> (leaf_invariant (Leaf :: l1) (Leaf :: l2)) | LI_leaf_l : (l1,l2:(list tree))(no_leaf l1) -> (no_leaf l2) -> ~l2=[] -> (leaf_invariant (Leaf :: l1) l2) | LI_l_leaf : (l1,l2:(list tree))(no_leaf l1) -> (no_leaf l2) -> ~l1=[] -> (leaf_invariant l1 (Leaf :: l2)) | LI_l_l : (l1,l2:(list tree))(no_leaf l1) -> (no_leaf l2) -> ~l1=[] -> ~l2=[] -> (leaf_invariant l1 l2).

Hint leaf_invariant := Constructors leaf_invariant.

Lemma no_leaf_invariant : (l1,l2:(list tree)) (no_leaf l1) -> (no_leaf l2) -> (leaf_invariant l1 l2).

Hints Resolve no_leaf_invariant.

compare_aux and compare

Definition compare_aux : (l1,l2:(list tree))(sorted_l l1) -> (sorted_l l2) -> (leaf_invariant l1 l2) -> (Compare L.lt L.eq (flatten l1) (flatten l2)).

Lemma flatten_elements : (s:tree)(flatten (s::[])) = (elements_tree s).

Definition compare : (s1,s2:t)(Compare lt eq s1 s2).

Equality test

Definition equal : (s,s':t){ Equal s s' } + { ~(Equal s s') }.

Write State toto.

End Make.

Index

This page has been generated by coqdoc

Library FSetAVL

Trees

Occurrence in a tree

Binary search trees

AVL trees

Sets as AVL trees

Logical appartness

Empty set

Emptyness test

Appartness

Singleton set

Helper functions

Insertion

Join

Extraction of minimum and maximum element

Merging two trees

Deletion

Minimum element

Maximum element

Any element

Concatenation

Splitting

Intersection

Difference

Elements

Cardinal

Union

Filter

Partition

Subset

Fold

Comparison

Relations `eq` and `lt` over trees

Comparison algorithm

Lists of trees

Termination of `compare_aux`

Lemmas for the correctness of `compare`

`compare_aux` and `compare`

Equality test

Library FSetAVL

Trees

Occurrence in a tree

Binary search trees

AVL trees

Sets as AVL trees

Logical appartness

Empty set

Emptyness test

Appartness

Singleton set

Helper functions

Insertion

Join

Extraction of minimum and maximum element

Merging two trees

Deletion

Minimum element

Maximum element

Any element

Concatenation

Splitting

Intersection

Difference

Elements

Cardinal

Union

Filter

Partition

Subset

Fold

Comparison

Relations eq and lt over trees

Comparison algorithm

Lists of trees

Termination of compare_aux

Lemmas for the correctness of compare

compare_aux and compare

Equality test

Relations `eq` and `lt` over trees

Termination of `compare_aux`

Lemmas for the correctness of `compare`

`compare_aux` and `compare`