Library Coq.FSets.FSetFullAVL




FSetFullAVL



This file contains some complements to FSetAVL.

  • Functor AvlProofs proves that trees of FSetAVL are not only binary search trees, but moreover well-balanced ones. This is done by proving that all operations preserve the balancing.


  • Functor OcamlOps contains variants of union, subset, compare and equal that are faithful to the original ocaml codes, while the versions in FSetAVL have been adapted to perform only structural recursive code.


  • Finally, we pack the previous elements in a Make functor similar to the one of FSetAVL, but richer.

Require Import Recdef FSetInterface FSetList ZArith Int FSetAVL.


Module AvlProofs (Import I:Int)(X:OrderedType).
Module Import Raw := Raw I X.
Import Raw.Proofs.
Module Import II := MoreInt I.
Open Local Scope pair_scope.
Open Local Scope Int_scope.

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

Inductive avl : tree -> Prop :=
  | RBLeaf : avl Leaf
  | RBNode : forall x l r h, avl l -> avl r ->
      -(2) <= height l - height r <= 2 ->
      h = max (height l) (height r) + 1 ->
      avl (Node l x r h).

Automation and dedicated tactics


Hint Constructors avl.

A tactic for cleaning hypothesis after use of functional induction.

Ltac clearf :=
 match goal with
  | H : (@Logic.eq (Compare _ _ _ _) _ _) |- _ => clear H; clearf
  | H : (@Logic.eq (sumbool _ _) _ _) |- _ => clear H; clearf
  | _ => idtac
 end.

Tactics about avl

Lemma height_non_negative : forall s : tree, avl s -> height s >= 0.
Implicit Arguments height_non_negative.

When H:avl r, typing avl_nn H or avl_nn r adds height r>=0

Ltac avl_nn_hyp H :=
     let nz := fresh "nz" in assert (nz := height_non_negative H).

Ltac avl_nn h :=
  let t := type of h in
  match type of t with
   | Prop => avl_nn_hyp h
   | _ => match goal with H : avl h |- _ => avl_nn_hyp H end
  end.


Ltac avl_nns :=
  match goal with
     | H:avl _ |- _ => avl_nn_hyp H; clear H; avl_nns
     | _ => idtac
  end.

Results about height

Lemma height_0 : forall s, avl s -> height s = 0 -> s = Leaf.

Results about avl


Lemma avl_node :
 forall x l r, avl l -> avl r ->
 -(2) <= height l - height r <= 2 ->
 avl (Node l x r (max (height l) (height r) + 1)).
Hint Resolve avl_node.

empty

Lemma empty_avl : avl empty.

singleton

Lemma singleton_avl : forall x : elt, avl (singleton x).

create

Lemma create_avl :
 forall l x r, avl l -> avl r -> -(2) <= height l - height r <= 2 ->
 avl (create l x r).

Lemma create_height :
 forall l x r, avl l -> avl r -> -(2) <= height l - height r <= 2 ->
 height (create l x r) = max (height l) (height r) + 1.

bal

Lemma bal_avl : forall l x r, avl l -> avl r ->
 -(3) <= height l - height r <= 3 -> avl (bal l x r).

Lemma bal_height_1 : forall l x r, avl l -> avl r ->
 -(3) <= height l - height r <= 3 ->
 0 <= height (bal l x r) - max (height l) (height r) <= 1.

Lemma bal_height_2 :
 forall l x r, avl l -> avl r -> -(2) <= height l - height r <= 2 ->
 height (bal l x r) == max (height l) (height r) +1.

Ltac omega_bal := match goal with
  | H:avl ?l, H':avl ?r |- context [ bal ?l ?x ?r ] =>
     generalize (bal_height_1 x H H') (bal_height_2 x H H');
     omega_max
  end.

add

Lemma add_avl_1 : forall s x, avl s ->
 avl (add x s) /\ 0 <= height (add x s) - height s <= 1.

Lemma add_avl : forall s x, avl s -> avl (add x s).
Hint Resolve add_avl.

join

Lemma join_avl_1 : forall l x r, avl l -> avl r -> avl (join l x r) /\
 0<= height (join l x r) - max (height l) (height r) <= 1.

Lemma join_avl : forall l x r, avl l -> avl r -> avl (join l x r).
Hint Resolve join_avl.

remove_min

Lemma remove_min_avl_1 : forall l x r h, avl (Node l x r h) ->
 avl (remove_min l x r)#1 /\
 0 <= height (Node l x r h) - height (remove_min l x r)#1 <= 1.

Lemma remove_min_avl : forall l x r h, avl (Node l x r h) ->
    avl (remove_min l x r)#1.

merge

Lemma merge_avl_1 : forall s1 s2, avl s1 -> avl s2 ->
 -(2) <= height s1 - height s2 <= 2 ->
 avl (merge s1 s2) /\
 0<= height (merge s1 s2) - max (height s1) (height s2) <=1.

Lemma merge_avl : forall s1 s2, avl s1 -> avl s2 ->
  -(2) <= height s1 - height s2 <= 2 -> avl (merge s1 s2).

remove

Lemma remove_avl_1 : forall s x, avl s ->
 avl (remove x s) /\ 0 <= height s - height (remove x s) <= 1.

Lemma remove_avl : forall s x, avl s -> avl (remove x s).
Hint Resolve remove_avl.

concat

Lemma concat_avl : forall s1 s2, avl s1 -> avl s2 -> avl (concat s1 s2).
Hint Resolve concat_avl.

split

Lemma split_avl : forall s x, avl s ->
  avl (split x s)#l /\ avl (split x s)#r.

inter

Lemma inter_avl : forall s1 s2, avl s1 -> avl s2 -> avl (inter s1 s2).

diff

Lemma diff_avl : forall s1 s2, avl s1 -> avl s2 -> avl (diff s1 s2).

union

Lemma union_avl : forall s1 s2, avl s1 -> avl s2 -> avl (union s1 s2).

filter

Lemma filter_acc_avl : forall f s acc, avl s -> avl acc ->
 avl (filter_acc f acc s).
Hint Resolve filter_acc_avl.

Lemma filter_avl : forall f s, avl s -> avl (filter f s).

partition

Lemma partition_acc_avl_1 : forall f s acc, avl s ->
 avl acc#1 -> avl (partition_acc f acc s)#1.

Lemma partition_acc_avl_2 : forall f s acc, avl s ->
 avl acc#2 -> avl (partition_acc f acc s)#2.

Lemma partition_avl_1 : forall f s, avl s -> avl (partition f s)#1.

Lemma partition_avl_2 : forall f s, avl s -> avl (partition f s)#2.

End AvlProofs.

Module OcamlOps (Import I:Int)(X:OrderedType).
Module Import AvlProofs := AvlProofs I X.
Import Raw.
Import Raw.Proofs.
Import II.
Open Local Scope pair_scope.
Open Local Scope nat_scope.

Properties of cardinal

Lemma bal_cardinal : forall l x r,
 cardinal (bal l x r) = S (cardinal l + cardinal r).

Lemma add_cardinal : forall x s,
 cardinal (add x s) <= S (cardinal s).

Lemma join_cardinal : forall l x r,
 cardinal (join l x r) <= S (cardinal l + cardinal r).

Lemma split_cardinal_1 : forall x s,
 (cardinal (split x s)#l <= cardinal s)%nat.

Lemma split_cardinal_2 : forall x s,
 (cardinal (split x s)#r <= cardinal s)%nat.

ocaml_union, an union faithful to the original ocaml code


Definition cardinal2 (s:t*t) := (cardinal s#1 + cardinal s#2)%nat.

Ltac ocaml_union_tac :=
 intros; unfold cardinal2; simpl fst in *; simpl snd in *;
 match goal with H: split ?x ?s = _ |- _ =>
  generalize (split_cardinal_1 x s) (split_cardinal_2 x s);
  rewrite H; simpl; romega with *
 end.

Import Logic.


Lemma ocaml_union_in : forall s y,
 bst s#1 -> avl s#1 -> bst s#2 -> avl s#2 ->
 (In y (ocaml_union s) <-> In y s#1 \/ In y s#2).

Lemma ocaml_union_bst : forall s,
 bst s#1 -> avl s#1 -> bst s#2 -> avl s#2 -> bst (ocaml_union s).

Lemma ocaml_union_avl : forall s,
 avl s#1 -> avl s#2 -> avl (ocaml_union s).

Lemma ocaml_union_alt : forall s, bst s#1 -> avl s#1 -> bst s#2 -> avl s#2 ->
 Equal (ocaml_union s) (union s#1 s#2).

ocaml_subset, a subset faithful to the original ocaml code




Lemma ocaml_subset_12 : forall s,
 bst s#1 -> bst s#2 ->
 (ocaml_subset s = true <-> Subset s#1 s#2).

Lemma ocaml_subset_alt : forall s, bst s#1 -> bst s#2 ->
 ocaml_subset s = subset s#1 s#2.

ocaml_compare, a compare faithful to the original ocaml code

termination of compare_aux

Fixpoint cardinal_e e := match e with
  | End => 0
  | More _ s r => S (cardinal s + cardinal_e r)
 end.

Lemma cons_cardinal_e : forall s e,
 cardinal_e (cons s e) = cardinal s + cardinal_e e.

Definition cardinal_e_2 e := cardinal_e e#1 + cardinal_e e#2.



Definition ocaml_compare s1 s2 :=
 ocaml_compare_aux (cons s1 End, cons s2 End).

Lemma ocaml_compare_aux_Cmp : forall e,
 Cmp (ocaml_compare_aux e) (flatten_e e#1) (flatten_e e#2).

Lemma ocaml_compare_Cmp : forall s1 s2,
 Cmp (ocaml_compare s1 s2) (elements s1) (elements s2).

Lemma ocaml_compare_alt : forall s1 s2, bst s1 -> bst s2 ->
 ocaml_compare s1 s2 = compare s1 s2.

Equality test


Definition ocaml_equal s1 s2 : bool :=
 match ocaml_compare s1 s2 with
  | Eq => true
  | _ => false
 end.

Lemma ocaml_equal_1 : forall s1 s2, bst s1 -> bst s2 ->
 Equal s1 s2 -> ocaml_equal s1 s2 = true.

Lemma ocaml_equal_2 : forall s1 s2,
 ocaml_equal s1 s2 = true -> Equal s1 s2.

Lemma ocaml_equal_alt : forall s1 s2, bst s1 -> bst s2 ->
 ocaml_equal s1 s2 = equal s1 s2.

End OcamlOps.

Encapsulation



We can implement S with balanced binary search trees. When compared to FSetAVL, we maintain here two invariants (bst and avl) instead of only bst, which is enough for fulfilling the FSet interface.

This encapsulation propose the non-structural variants ocaml_union, ocaml_subset, ocaml_compare, ocaml_equal.

Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.

 Module E := X.
 Module Import OcamlOps := OcamlOps I X.
 Import AvlProofs.
 Import Raw.
 Import Raw.Proofs.

 Record bbst := Bbst {this :> Raw.t; is_bst : bst this; is_avl : avl this}.
 Definition t := bbst.
 Definition elt := E.t.

 Definition In (x : elt) (s : t) : Prop := In x s.
 Definition Equal (s s':t) : Prop := forall a : elt, In a s <-> In a s'.
 Definition Subset (s s':t) : Prop := forall a : elt, In a s -> In a s'.
 Definition Empty (s:t) : Prop := forall a : elt, ~ In a s.
 Definition For_all (P : elt -> Prop) (s:t) : Prop := forall x, In x s -> P x.
 Definition Exists (P : elt -> Prop) (s:t) : Prop := 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 := mem x s.

 Definition empty : t := Bbst empty_bst empty_avl.
 Definition is_empty (s:t) : bool := is_empty s.
 Definition singleton (x:elt) : t :=
   Bbst (singleton_bst x) (singleton_avl x).
 Definition add (x:elt)(s:t) : t :=
   Bbst (add_bst x (is_bst s)) (add_avl x (is_avl s)).
 Definition remove (x:elt)(s:t) : t :=
   Bbst (remove_bst x (is_bst s)) (remove_avl x (is_avl s)).
 Definition inter (s s':t) : t :=
   Bbst (inter_bst (is_bst s) (is_bst s'))
        (inter_avl (is_avl s) (is_avl s')).
 Definition union (s s':t) : t :=
   Bbst (union_bst (is_bst s) (is_bst s'))
        (union_avl (is_avl s) (is_avl s')).
 Definition ocaml_union (s s':t) : t :=
   Bbst (@ocaml_union_bst (s.(this),s'.(this))
          (is_bst s) (is_avl s) (is_bst s') (is_avl s'))
        (@ocaml_union_avl (s.(this),s'.(this)) (is_avl s) (is_avl s')).
 Definition diff (s s':t) : t :=
   Bbst (diff_bst (is_bst s) (is_bst s'))
        (diff_avl (is_avl s) (is_avl s')).
 Definition elements (s:t) : list elt := elements s.
 Definition min_elt (s:t) : option elt := min_elt s.
 Definition max_elt (s:t) : option elt := max_elt s.
 Definition choose (s:t) : option elt := choose s.
 Definition fold (B : Type) (f : elt -> B -> B) (s:t) : B -> B := fold f s.
 Definition cardinal (s:t) : nat := cardinal s.
 Definition filter (f : elt -> bool) (s:t) : t :=
   Bbst (filter_bst f (is_bst s)) (filter_avl f (is_avl s)).
 Definition for_all (f : elt -> bool) (s:t) : bool := for_all f s.
 Definition exists_ (f : elt -> bool) (s:t) : bool := exists_ f s.
 Definition partition (f : elt -> bool) (s:t) : t * t :=
   let p := partition f s in
   (@Bbst (fst p) (partition_bst_1 f (is_bst s))
                 (partition_avl_1 f (is_avl s)),
    @Bbst (snd p) (partition_bst_2 f (is_bst s))
                 (partition_avl_2 f (is_avl s))).

 Definition equal (s s':t) : bool := equal s s'.
 Definition ocaml_equal (s s':t) : bool := ocaml_equal s s'.
 Definition subset (s s':t) : bool := subset s s'.
 Definition ocaml_subset (s s':t) : bool :=
  ocaml_subset (s.(this),s'.(this)).

 Definition eq (s s':t) : Prop := Equal s s'.
 Definition lt (s s':t) : Prop := lt s s'.

 Definition compare (s s':t) : Compare lt eq s s'.

 Definition ocaml_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 is_avl.

 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'.

 Lemma ocaml_equal_alt : ocaml_equal s s' = equal s s'.

 Lemma ocaml_equal_1 : Equal s s' -> ocaml_equal s s' = true.
 Lemma ocaml_equal_2 : ocaml_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 ocaml_subset_alt : ocaml_subset s s' = subset s s'.

 Lemma ocaml_subset_1 : Subset s s' -> ocaml_subset s s' = true.
 Lemma ocaml_subset_2 : ocaml_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 ocaml_union_alt : Equal (ocaml_union s s') (union s s').

 Lemma ocaml_union_1 : In x (ocaml_union s s') -> In x s \/ In x s'.
 Lemma ocaml_union_2 : In x s -> In x (ocaml_union s s').
 Lemma ocaml_union_3 : In x s' -> In x (ocaml_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).