Library FSets.FSetFullAVL



FSetFullAVL : 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.
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 FSetList0 ZArith Int FSetAVL0 ROmega.

Set Implicit Arguments.
Unset Strict Implicit.

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.

Ltac omega_max := i2z_refl; romega with Z.

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 : ∀ 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 : ∀ s : tree, avl s → height s ≥ 0.
Proof.
 induction s; simpl; intros; auto with zarith.
 inv avl; intuition; omega_max.
Qed.
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 : ∀ s, avl s → height s = 0 → s = Leaf.
Proof.
 destruct 1; intuition; simpl in ×.
 avl_nns; simpl in *; exfalso; omega_max.
Qed.

Results about avl


Lemma avl_node :
 ∀ x l r, avl l → avl r →
 -(2) ≤ height l - height r ≤ 2 →
 avl (Node l x r (max (height l) (height r) + 1)).
Proof.
  intros; auto.
Qed.
Hint Resolve avl_node.

empty

Lemma empty_avl : avl empty.
Proof.
 auto.
Qed.

singleton

Lemma singleton_avl : ∀ x : elt, avl (singleton x).
Proof.
 unfold singleton; intro.
 constructor; auto; try red; simpl; omega_max.
Qed.

create

Lemma create_avl :
 ∀ l x r, avl l → avl r → -(2) ≤ height l - height r ≤ 2 →
 avl (create l x r).
Proof.
 unfold create; auto.
Qed.

Lemma create_height :
 ∀ l x r, avl l → avl r → -(2) ≤ height l - height r ≤ 2 →
 height (create l x r) = max (height l) (height r) + 1.
Proof.
 unfold create; auto.
Qed.

bal

Lemma bal_avl : ∀ l x r, avl l → avl r →
 -(3) ≤ height l - height r ≤ 3 → avl (bal l x r).
Proof.
 intros l x r; functional induction bal l x r; intros; clearf;
 inv avl; simpl in *;
 match goal with |- avl (assert_false _ _ _) ⇒ avl_nns
  | _ ⇒ repeat apply create_avl; simpl in *; auto
 end; omega_max.
Qed.

Lemma bal_height_1 : ∀ 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.
Proof.
 intros l x r; functional induction bal l x r; intros; clearf;
 inv avl; avl_nns; simpl in *; omega_max.
Qed.

Lemma bal_height_2 :
 ∀ l x r, avl l → avl r → -(2) ≤ height l - height r ≤ 2 →
 height (bal l x r) == max (height l) (height r) +1.
Proof.
 intros l x r; functional induction bal l x r; intros; clearf;
 inv avl; simpl in *; omega_max.
Qed.

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 : ∀ s x, avl s →
 avl (add x s) ∧ 0 ≤ height (add x s) - height s ≤ 1.
Proof.
 intros s x; functional induction (add x s); subst;intros; inv avl; simpl in ×.
 intuition; try constructor; simpl; auto; try omega_max.
 destruct IHt; auto.
 split.
 apply bal_avl; auto; omega_max.
 omega_bal.
 intuition; omega_max.
 destruct IHt; auto.
 split.
 apply bal_avl; auto; omega_max.
 omega_bal.
Qed.

Lemma add_avl : ∀ s x, avl s → avl (add x s).
Proof.
 intros; destruct (add_avl_1 x H); auto.
Qed.
Hint Resolve add_avl.

join

Lemma join_avl_1 : ∀ l x r, avl l → avl r → avl (join l x r) ∧
 0≤ height (join l x r) - max (height l) (height r) ≤ 1.
Proof.
 join_tac.

 split; simpl; auto.
 destruct (add_avl_1 x H0).
 avl_nns; omega_max.
 set (l:=Node ll lx lr lh) in ×.
 split; auto.
 destruct (add_avl_1 x H).
 simpl (height Leaf).
 avl_nns; omega_max.

 inversion_clear H.
 assert (height (Node rl rx rr rh) = rh); auto.
 set (r := Node rl rx rr rh) in *; clearbody r.
 destruct (Hlr x r H2 H0); clear Hrl Hlr.
 set (j := join lr x r) in *; clearbody j.
 simpl.
 assert (-(3) ≤ height ll - height j ≤ 3) by omega_max.
 split.
 apply bal_avl; auto.
 omega_bal.

 inversion_clear H0.
 assert (height (Node ll lx lr lh) = lh); auto.
 set (l' := Node ll lx lr lh) in *; clearbody l'.
 destruct (Hrl H H1); clear Hrl Hlr.
 set (j := join l' x rl) in *; clearbody j.
 simpl.
 assert (-(3) ≤ height j - height rr ≤ 3) by omega_max.
 split.
 apply bal_avl; auto.
 omega_bal.

 clear Hrl Hlr.
 assert (height (Node ll lx lr lh) = lh); auto.
 assert (height (Node rl rx rr rh) = rh); auto.
 set (l' := Node ll lx lr lh) in *; clearbody l'.
 set (r := Node rl rx rr rh) in *; clearbody r.
 assert (-(2) ≤ height l' - height r ≤ 2) by omega_max.
 split.
 apply create_avl; auto.
 rewrite create_height; auto; omega_max.
Qed.

Lemma join_avl : ∀ l x r, avl l → avl r → avl (join l x r).
Proof.
 intros; destruct (join_avl_1 x H H0); auto.
Qed.
Hint Resolve join_avl.

remove_min

Lemma remove_min_avl_1 : ∀ 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.
Proof.
 intros l x r; functional induction (remove_min l x r); subst;simpl in *; intros.
 inv avl; simpl in *; split; auto.
 avl_nns; omega_max.
 inversion_clear H.
 rewrite e0 in IHp;simpl in IHp;destruct (IHp _x); auto.
 split; simpl in ×.
 apply bal_avl; auto; omega_max.
 omega_bal.
Qed.

Lemma remove_min_avl : ∀ l x r h, avl (Node l x r h) →
    avl (remove_min l x r)#1.
Proof.
 intros; destruct (remove_min_avl_1 H); auto.
Qed.

merge

Lemma merge_avl_1 : ∀ 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.
Proof.
 intros s1 s2; functional induction (merge s1 s2); intros;
 try factornode _x _x0 _x1 _x2 as s1.
 simpl; split; auto; avl_nns; omega_max.
 simpl; split; auto; avl_nns; simpl in *; omega_max.
 generalize (remove_min_avl_1 H0).
 rewrite e1; destruct 1.
 split.
 apply bal_avl; auto.
 simpl; omega_max.
 simpl in *; omega_bal.
Qed.

Lemma merge_avl : ∀ s1 s2, avl s1 → avl s2 →
  -(2) ≤ height s1 - height s2 ≤ 2 → avl (merge s1 s2).
Proof.
 intros; destruct (merge_avl_1 H H0 H1); auto.
Qed.

remove

Lemma remove_avl_1 : ∀ s x, avl s →
 avl (remove x s) ∧ 0 ≤ height s - height (remove x s) ≤ 1.
Proof.
 intros s x; functional induction (remove x s); intros.
 intuition; omega_max.
 inv avl.
 destruct (IHt H0).
 split.
 apply bal_avl; auto.
 omega_max.
 omega_bal.
 inv avl.
 generalize (merge_avl_1 H0 H1 H2).
 intuition omega_max.
 inv avl.
 destruct (IHt H1).
 split.
 apply bal_avl; auto.
 omega_max.
 omega_bal.
Qed.

Lemma remove_avl : ∀ s x, avl s → avl (remove x s).
Proof.
 intros; destruct (remove_avl_1 x H); auto.
Qed.
Hint Resolve remove_avl.

concat

Lemma concat_avl : ∀ s1 s2, avl s1 → avl s2 → avl (concat s1 s2).
Proof.
 intros s1 s2; functional induction (concat s1 s2); auto.
 intros; apply join_avl; auto.
 generalize (remove_min_avl H0); rewrite e1; simpl; auto.
Qed.
Hint Resolve concat_avl.

split

Lemma split_avl : ∀ s x, avl s →
  avl (split x s)#l ∧ avl (split x s)#r.
Proof.
 intros s x; functional induction (split x s); simpl; auto.
 rewrite e1 in IHt;simpl in IHt;inversion_clear 1; intuition.
 simpl; inversion_clear 1; auto.
 rewrite e1 in IHt;simpl in IHt;inversion_clear 1; intuition.
Qed.

inter

Lemma inter_avl : ∀ s1 s2, avl s1 → avl s2 → avl (inter s1 s2).
Proof.
 intros s1 s2; functional induction inter s1 s2; auto; intros A1 A2;
 generalize (split_avl x1 A2); rewrite e1; simpl; destruct 1;
 inv avl; auto.
Qed.

diff

Lemma diff_avl : ∀ s1 s2, avl s1 → avl s2 → avl (diff s1 s2).
Proof.
 intros s1 s2; functional induction diff s1 s2; auto; intros A1 A2;
 generalize (split_avl x1 A2); rewrite e1; simpl; destruct 1;
 inv avl; auto.
Qed.

union

Lemma union_avl : ∀ s1 s2, avl s1 → avl s2 → avl (union s1 s2).
Proof.
 intros s1 s2; functional induction union s1 s2; auto; intros A1 A2;
 generalize (split_avl x1 A2); rewrite e1; simpl; destruct 1;
 inv avl; auto.
Qed.

filter

Lemma filter_acc_avl : ∀ f s acc, avl s → avl acc →
 avl (filter_acc f acc s).
Proof.
 induction s; simpl; auto.
 intros.
 inv avl.
 destruct (f t); auto.
Qed.
Hint Resolve filter_acc_avl.

Lemma filter_avl : ∀ f s, avl s → avl (filter f s).
Proof.
 unfold filter; intros; apply filter_acc_avl; auto.
Qed.

partition

Lemma partition_acc_avl_1 : ∀ f s acc, avl s →
 avl acc#1 → avl (partition_acc f acc s)#1.
Proof.
 induction s; simpl; auto.
 destruct acc as [acct accf]; simpl in ×.
 intros.
 inv avl.
 apply IHs2; auto.
 apply IHs1; auto.
 destruct (f t); simpl; auto.
Qed.

Lemma partition_acc_avl_2 : ∀ f s acc, avl s →
 avl acc#2 → avl (partition_acc f acc s)#2.
Proof.
 induction s; simpl; auto.
 destruct acc as [acct accf]; simpl in ×.
 intros.
 inv avl.
 apply IHs2; auto.
 apply IHs1; auto.
 destruct (f t); simpl; auto.
Qed.

Lemma partition_avl_1 : ∀ f s, avl s → avl (partition f s)#1.
Proof.
 unfold partition; intros; apply partition_acc_avl_1; auto.
Qed.

Lemma partition_avl_2 : ∀ f s, avl s → avl (partition f s)#2.
Proof.
 unfold partition; intros; apply partition_acc_avl_2; auto.
Qed.

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 : ∀ l x r,
 cardinal (bal l x r) = S (cardinal l + cardinal r).
Proof.
 intros l x r; functional induction bal l x r; intros; clearf;
 simpl; auto with arith; romega with ×.
Qed.

Lemma add_cardinal : ∀ x s,
 cardinal (add x s) ≤ S (cardinal s).
Proof.
 intros; functional induction add x s; simpl; auto with arith;
 rewrite bal_cardinal; romega with ×.
Qed.

Lemma join_cardinal : ∀ l x r,
 cardinal (join l x r) ≤ S (cardinal l + cardinal r).
Proof.
 join_tac; auto with arith.
 simpl; apply add_cardinal.
 simpl; destruct X.compare; simpl; auto with arith.
 generalize (bal_cardinal (add x ll) lx lr) (add_cardinal x ll);
  romega with ×.
 generalize (bal_cardinal ll lx (add x lr)) (add_cardinal x lr);
  romega with ×.
 generalize (bal_cardinal ll lx (join lr x (Node rl rx rr rh)))
  (Hlr x (Node rl rx rr rh)); simpl; romega with ×.
 simpl S in *; generalize (bal_cardinal (join (Node ll lx lr lh) x rl) rx rr).
 romega with ×.
Qed.

Lemma split_cardinal_1 : ∀ x s,
 (cardinal (split x s)#l ≤ cardinal s)%nat.
Proof.
 intros x s; functional induction split x s; simpl; auto.
 rewrite e1 in IHt; simpl in ×.
 romega with ×.
 romega with ×.
 rewrite e1 in IHt; simpl in ×.
 generalize (@join_cardinal l y rl); romega with ×.
Qed.

Lemma split_cardinal_2 : ∀ x s,
 (cardinal (split x s)#r ≤ cardinal s)%nat.
Proof.
 intros x s; functional induction split x s; simpl; auto.
 rewrite e1 in IHt; simpl in ×.
 generalize (@join_cardinal rl y r); romega with ×.
 romega with ×.
 rewrite e1 in IHt; simpl in *; romega with ×.
Qed.

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.

Function ocaml_union (s : t × t) { measure cardinal2 s } : t :=
 match s with
  | (Leaf, Leaf) ⇒ s#2
  | (Leaf, Node _ _ _ _) ⇒ s#2
  | (Node _ _ _ _, Leaf) ⇒ s#1
  | (Node l1 x1 r1 h1, Node l2 x2 r2 h2) ⇒
        if ge_lt_dec h1 h2 then
          if eq_dec h2 1%I then add x2 s#1 else
          let (l2',_,r2') := split x1 s#2 in
             join (ocaml_union (l1,l2')) x1 (ocaml_union (r1,r2'))
        else
          if eq_dec h1 1%I then add x1 s#2 else
          let (l1',_,r1') := split x2 s#1 in
             join (ocaml_union (l1',l2)) x2 (ocaml_union (r1',r2))
 end.
Proof.
abstract ocaml_union_tac.
abstract ocaml_union_tac.
abstract ocaml_union_tac.
abstract ocaml_union_tac.
Defined.

Lemma ocaml_union_in : ∀ 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).
Proof.
 intros s; functional induction ocaml_union s; intros y B1 A1 B2 A2;
  simpl fst in *; simpl snd in *; try clear e0 e1.
 intuition_in.
 intuition_in.
 intuition_in.
 inv avl.
 rewrite (height_0 H); [ | avl_nn l2; omega_max].
 rewrite (height_0 H0); [ | avl_nn r2; omega_max].
 rewrite add_in; intuition_in.
 generalize
  (split_avl x1 A2) (split_bst x1 B2)
  (split_in_1 x1 y B2) (split_in_2 x1 y B2).
 rewrite e2; simpl.
 destruct 1; destruct 1; inv avl; inv bst.
 rewrite join_in, IHt, IHt0; auto.
 do 2 (intro Eq; rewrite Eq; clear Eq).
 case (X.compare y x1); intuition_in.
 inv avl.
 rewrite (height_0 H3); [ | avl_nn l1; omega_max].
 rewrite (height_0 H4); [ | avl_nn r1; omega_max].
 rewrite add_in; auto; intuition_in.
 generalize
  (split_avl x2 A1) (split_bst x2 B1)
  (split_in_1 x2 y B1) (split_in_2 x2 y B1).
 rewrite e2; simpl.
 destruct 1; destruct 1; inv avl; inv bst.
 rewrite join_in, IHt, IHt0; auto.
 do 2 (intro Eq; rewrite Eq; clear Eq).
 case (X.compare y x2); intuition_in.
Qed.

Lemma ocaml_union_bst : ∀ s,
 bst s#1 → avl s#1 → bst s#2 → avl s#2 → bst (ocaml_union s).
Proof.
 intros s; functional induction ocaml_union s; intros B1 A1 B2 A2;
  simpl fst in *; simpl snd in *; try clear e0 e1;
  try apply add_bst; auto.
 clear _x _x0; factornode l2 x2 r2 h2 as s2.
 generalize (split_avl x1 A2) (split_bst x1 B2)
  (@split_in_1 s2 x1)(@split_in_2 s2 x1).
 rewrite e2; simpl.
 destruct 1; destruct 1; intros.
 inv bst; inv avl.
 apply join_bst; auto.
 intro y; rewrite ocaml_union_in, H3; intuition_in.
 intro y; rewrite ocaml_union_in, H4; intuition_in.
 clear _x _x0; factornode l1 x1 r1 h1 as s1.
 generalize (split_avl x2 A1) (split_bst x2 B1)
  (@split_in_1 s1 x2)(@split_in_2 s1 x2).
 rewrite e2; simpl.
 destruct 1; destruct 1; intros.
 inv bst; inv avl.
 apply join_bst; auto.
 intro y; rewrite ocaml_union_in, H3; intuition_in.
 intro y; rewrite ocaml_union_in, H4; intuition_in.
Qed.

Lemma ocaml_union_avl : ∀ s,
 avl s#1 → avl s#2 → avl (ocaml_union s).
Proof.
 intros s; functional induction ocaml_union s;
  simpl fst in *; simpl snd in *; auto.
 intros A1 A2; generalize (split_avl x1 A2); rewrite e2; simpl.
 inv avl; destruct 1; auto.
 intros A1 A2; generalize (split_avl x2 A1); rewrite e2; simpl.
 inv avl; destruct 1; auto.
Qed.

Lemma ocaml_union_alt : ∀ s, bst s#1 → avl s#1 → bst s#2 → avl s#2 →
 Equal (ocaml_union s) (union s#1 s#2).
Proof.
 red; intros; rewrite ocaml_union_in, union_in; simpl; intuition.
Qed.

ocaml_subset, a subset faithful to the original ocaml code


Function ocaml_subset (s:t×t) { measure cardinal2 s } : bool :=
 match s with
  | (Leaf, _) ⇒ true
  | (Node _ _ _ _, Leaf) ⇒ false
  | (Node l1 x1 r1 h1, Node l2 x2 r2 h2) ⇒
     match X.compare x1 x2 with
      | EQ _ ⇒ ocaml_subset (l1,l2) && ocaml_subset (r1,r2)
      | LT _ ⇒ ocaml_subset (Node l1 x1 Leaf 0%I, l2) && ocaml_subset (r1,s#2)
      | GT _ ⇒ ocaml_subset (Node Leaf x1 r1 0%I, r2) && ocaml_subset (l1,s#2)
     end
 end.

Proof.
 intros; unfold cardinal2; simpl; abstract romega with ×.
 intros; unfold cardinal2; simpl; abstract romega with ×.
 intros; unfold cardinal2; simpl; abstract romega with ×.
 intros; unfold cardinal2; simpl; abstract romega with ×.
 intros; unfold cardinal2; simpl; abstract romega with ×.
 intros; unfold cardinal2; simpl; abstract romega with ×.
Defined.

Lemma ocaml_subset_12 : ∀ s,
 bst s#1 → bst s#2 →
 (ocaml_subset s = true ↔ Subset s#1 s#2).
Proof.
 intros s; functional induction ocaml_subset s; simpl;
  intros B1 B2; try clear e0.
 intuition.
 red; auto; inversion 1.
 split; intros; try discriminate.
 assert (H': In _x0 Leaf) by auto; inversion H'.
 simpl in *; inv bst.
 rewrite andb_true_iff, IHb, IHb0; auto; clear IHb IHb0.
 unfold Subset; intuition_in.
 assert (X.eq a x2) by order; intuition_in.
 assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
 assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
 simpl in *; inv bst.
 rewrite andb_true_iff, IHb, IHb0; auto; clear IHb IHb0.
 unfold Subset; intuition_in.
 assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
 assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
 simpl in *; inv bst.
 rewrite andb_true_iff, IHb, IHb0; auto; clear IHb IHb0.
 unfold Subset; intuition_in.
 assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
 assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
Qed.

Lemma ocaml_subset_alt : ∀ s, bst s#1 → bst s#2 →
 ocaml_subset s = subset s#1 s#2.
Proof.
 intros.
 generalize (ocaml_subset_12 H H0); rewrite <-subset_12 by auto.
 destruct ocaml_subset; destruct subset; intuition.
Qed.

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 : ∀ s e,
 cardinal_e (cons s e) = cardinal s + cardinal_e e.
Proof.
 induction s; simpl; intros; auto.
 rewrite IHs1; simpl; rewrite <- plus_n_Sm; auto with arith.
Qed.

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

Function ocaml_compare_aux
 (e:enumeration×enumeration) { measure cardinal_e_2 e } : comparison :=
 match e with
 | (End,End) ⇒ Eq
 | (End,More _ _ _) ⇒ Lt
 | (More _ _ _, End) ⇒ Gt
 | (More x1 r1 e1, More x2 r2 e2) ⇒
       match X.compare x1 x2 with
        | EQ _ ⇒ ocaml_compare_aux (cons r1 e1, cons r2 e2)
        | LT _ ⇒ Lt
        | GT _ ⇒ Gt
       end
 end.

Proof.
intros; unfold cardinal_e_2; simpl;
abstract (do 2 rewrite cons_cardinal_e; romega with *).
Defined.

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

Lemma ocaml_compare_aux_Cmp : ∀ e,
 Cmp (ocaml_compare_aux e) (flatten_e e#1) (flatten_e e#2).
Proof.
 intros e; functional induction ocaml_compare_aux e; simpl; intros;
  auto; try discriminate.
 apply L.eq_refl.
 simpl in ×.
 apply cons_Cmp; auto.
 rewrite <- 2 cons_1; auto.
Qed.

Lemma ocaml_compare_Cmp : ∀ s1 s2,
 Cmp (ocaml_compare s1 s2) (elements s1) (elements s2).
Proof.
 unfold ocaml_compare; intros.
 assert (H1:=cons_1 s1 End).
 assert (H2:=cons_1 s2 End).
 simpl in *; rewrite <- app_nil_end in *; rewrite <-H1,<-H2.
 apply (@ocaml_compare_aux_Cmp (cons s1 End, cons s2 End)).
Qed.

Import Proofs.
Lemma ocaml_compare_alt : ∀ s1 s2, bst s1 → bst s2 →
 ocaml_compare s1 s2 = compare s1 s2.
Proof.
 intros s1 s2 B1 B2.
 generalize (ocaml_compare_Cmp s1 s2)(compare_Cmp s1 s2).
 unfold Cmp.
 destruct ocaml_compare; destruct compare; auto; intros; exfalso.
 elim (lt_not_eq B1 B2 H0); auto.
 elim (lt_not_eq B2 B1 H0); auto.
  apply eq_sym; auto.
 elim (lt_not_eq B1 B2 H); auto.
  elim (lt_not_eq B1 B1).
  red; eapply L.lt_trans; eauto.
  apply eq_refl.
 elim (lt_not_eq B2 B1 H); auto.
  apply eq_sym; auto.
 elim (lt_not_eq B1 B2 H0); auto.
  elim (lt_not_eq B1 B1).
  red; eapply L.lt_trans; eauto.
  apply eq_refl.
Qed.

Equality test


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

Lemma ocaml_equal_1 : ∀ s1 s2, bst s1 → bst s2 →
 Equal s1 s2 → ocaml_equal s1 s2 = true.
Proof.
unfold ocaml_equal; intros s1 s2 B1 B2 E.
generalize (ocaml_compare_Cmp s1 s2).
destruct (ocaml_compare s1 s2); auto; intros.
elim (lt_not_eq B1 B2 H E); auto.
elim (lt_not_eq B2 B1 H (eq_sym E)); auto.
Qed.

Lemma ocaml_equal_2 : ∀ s1 s2,
 ocaml_equal s1 s2 = true → Equal s1 s2.
Proof.
unfold ocaml_equal; intros s1 s2 E.
generalize (ocaml_compare_Cmp s1 s2);
 destruct ocaml_compare; auto; discriminate.
Qed.

Lemma ocaml_equal_alt : ∀ s1 s2, bst s1 → bst s2 →
 ocaml_equal s1 s2 = equal s1 s2.
Proof.
intros; unfold ocaml_equal, equal; rewrite ocaml_compare_alt; auto.
Qed.

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 := ∀ a : elt, In a s ↔ In a s'.
 Definition Subset (s s':t) : Prop := ∀ a : elt, In a s → In a s'.
 Definition Empty (s:t) : Prop := ∀ a : elt, ¬ In a s.
 Definition For_all (P : elt → Prop) (s:t) : Prop := ∀ x, In x s → P x.
 Definition Exists (P : elt → Prop) (s:t) : Prop := ∃ x, In x s ∧ P x.

 Lemma In_1 : ∀ (s:t)(x y:elt), E.eq x y → In x s → In y s.
 Proof. intro s; exact (@In_1 s). Qed.

 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'.
 Proof.
  destruct s as (s,b,a), s' as (s',b',a').
  generalize (compare_Cmp s s').
  destruct Raw.compare; intros; [apply EQ|apply LT|apply GT]; red; auto.
  change (Raw.Equal s s'); auto.
 Defined.

 Definition ocaml_compare (s s':t) : Compare lt eq s s'.
 Proof.
  destruct s as (s,b,a), s' as (s',b',a').
  generalize (ocaml_compare_Cmp s s').
  destruct ocaml_compare; intros; [apply EQ|apply LT|apply GT]; red; auto.
  change (Raw.Equal s s'); auto.
 Defined.

 Definition eq_dec (s s':t) : { eq s s' } + { ¬ eq s s' }.
 Proof.
  destruct s as (s,b,a), s' as (s',b',a'); unfold eq; simpl.
  case_eq (Raw.equal s s'); intro H; [left|right].
  apply equal_2; auto.
  intro H'; rewrite equal_1 in H; auto; discriminate.
 Defined.

 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.
 Proof. exact (mem_1 (is_bst s)). Qed.
 Lemma mem_2 : mem x s = true → In x s.
 Proof. exact (@mem_2 s x). Qed.

 Lemma equal_1 : Equal s s' → equal s s' = true.
 Proof. exact (equal_1 (is_bst s) (is_bst s')). Qed.
 Lemma equal_2 : equal s s' = true → Equal s s'.
 Proof. exact (@equal_2 s s'). Qed.

 Lemma ocaml_equal_alt : ocaml_equal s s' = equal s s'.
 Proof.
  destruct s; destruct s'; unfold ocaml_equal, equal; simpl.
  apply ocaml_equal_alt; auto.
 Qed.

 Lemma ocaml_equal_1 : Equal s s' → ocaml_equal s s' = true.
 Proof. exact (ocaml_equal_1 (is_bst s) (is_bst s')). Qed.
 Lemma ocaml_equal_2 : ocaml_equal s s' = true → Equal s s'.
 Proof. exact (@ocaml_equal_2 s s'). Qed.

 Ltac wrap t H := unfold t, In; simpl; rewrite H; auto; intuition.

 Lemma subset_1 : Subset s s' → subset s s' = true.
 Proof. wrap subset subset_12. Qed.
 Lemma subset_2 : subset s s' = true → Subset s s'.
 Proof. wrap subset subset_12. Qed.

 Lemma ocaml_subset_alt : ocaml_subset s s' = subset s s'.
 Proof.
  destruct s; destruct s'; unfold ocaml_subset, subset; simpl.
  rewrite ocaml_subset_alt; auto.
 Qed.

 Lemma ocaml_subset_1 : Subset s s' → ocaml_subset s s' = true.
 Proof. wrap ocaml_subset ocaml_subset_12; simpl; auto. Qed.
 Lemma ocaml_subset_2 : ocaml_subset s s' = true → Subset s s'.
 Proof. wrap ocaml_subset ocaml_subset_12; simpl; auto. Qed.

 Lemma empty_1 : Empty empty.
 Proof. exact empty_1. Qed.

 Lemma is_empty_1 : Empty s → is_empty s = true.
 Proof. exact (@is_empty_1 s). Qed.
 Lemma is_empty_2 : is_empty s = true → Empty s.
 Proof. exact (@is_empty_2 s). Qed.

 Lemma add_1 : E.eq x y → In y (add x s).
 Proof. wrap add add_in. Qed.
 Lemma add_2 : In y s → In y (add x s).
 Proof. wrap add add_in. Qed.
 Lemma add_3 : ¬ E.eq x y → In y (add x s) → In y s.
 Proof. wrap add add_in. elim H; auto. Qed.

 Lemma remove_1 : E.eq x y → ¬ In y (remove x s).
 Proof. wrap remove remove_in. Qed.
 Lemma remove_2 : ¬ E.eq x y → In y s → In y (remove x s).
 Proof. wrap remove remove_in. Qed.
 Lemma remove_3 : In y (remove x s) → In y s.
 Proof. wrap remove remove_in. Qed.

 Lemma singleton_1 : In y (singleton x) → E.eq x y.
 Proof. exact (@singleton_1 x y). Qed.
 Lemma singleton_2 : E.eq x y → In y (singleton x).
 Proof. exact (@singleton_2 x y). Qed.

 Lemma union_1 : In x (union s s') → In x s ∨ In x s'.
 Proof. wrap union union_in. Qed.
 Lemma union_2 : In x s → In x (union s s').
 Proof. wrap union union_in. Qed.
 Lemma union_3 : In x s' → In x (union s s').
 Proof. wrap union union_in. Qed.

 Lemma ocaml_union_alt : Equal (ocaml_union s s') (union s s').
 Proof.
  unfold ocaml_union, union, Equal, In.
  destruct s as (s0,b,a); destruct s' as (s0',b',a'); simpl.
  exact (@ocaml_union_alt (s0,s0') b a b' a').
 Qed.

 Lemma ocaml_union_1 : In x (ocaml_union s s') → In x s ∨ In x s'.
 Proof. wrap ocaml_union ocaml_union_in; simpl; auto. Qed.
 Lemma ocaml_union_2 : In x s → In x (ocaml_union s s').
 Proof. wrap ocaml_union ocaml_union_in; simpl; auto. Qed.
 Lemma ocaml_union_3 : In x s' → In x (ocaml_union s s').
 Proof. wrap ocaml_union ocaml_union_in; simpl; auto. Qed.

 Lemma inter_1 : In x (inter s s') → In x s.
 Proof. wrap inter inter_in. Qed.
 Lemma inter_2 : In x (inter s s') → In x s'.
 Proof. wrap inter inter_in. Qed.
 Lemma inter_3 : In x s → In x s' → In x (inter s s').
 Proof. wrap inter inter_in. Qed.

 Lemma diff_1 : In x (diff s s') → In x s.
 Proof. wrap diff diff_in. Qed.
 Lemma diff_2 : In x (diff s s') → ¬ In x s'.
 Proof. wrap diff diff_in. Qed.
 Lemma diff_3 : In x s → ¬ In x s' → In x (diff s s').
 Proof. wrap diff diff_in. Qed.

 Lemma fold_1 : ∀ (A : Type) (i : A) (f : elt → A → A),
      fold f s i = fold_left (fun a e ⇒ f e a) (elements s) i.
 Proof.
 unfold fold, elements; intros; apply fold_1; auto.
 Qed.

 Lemma cardinal_1 : cardinal s = length (elements s).
 Proof.
 unfold cardinal, elements; intros; apply elements_cardinal; auto.
 Qed.

 Section Filter.
 Variable f : elt → bool.

 Lemma filter_1 : compat_bool E.eq f → In x (filter f s) → In x s.
 Proof. intro. wrap filter filter_in. Qed.
 Lemma filter_2 : compat_bool E.eq f → In x (filter f s) → f x = true.
 Proof. intro. wrap filter filter_in. Qed.
 Lemma filter_3 : compat_bool E.eq f → In x s → f x = true → In x (filter f s).
 Proof. intro. wrap filter filter_in. Qed.

 Lemma for_all_1 : compat_bool E.eq f → For_all (fun x ⇒ f x = true) s → for_all f s = true.
 Proof. exact (@for_all_1 f s). Qed.
 Lemma for_all_2 : compat_bool E.eq f → for_all f s = true → For_all (fun x ⇒ f x = true) s.
 Proof. exact (@for_all_2 f s). Qed.

 Lemma exists_1 : compat_bool E.eq f → Exists (fun x ⇒ f x = true) s → exists_ f s = true.
 Proof. exact (@exists_1 f s). Qed.
 Lemma exists_2 : compat_bool E.eq f → exists_ f s = true → Exists (fun x ⇒ f x = true) s.
 Proof. exact (@exists_2 f s). Qed.

 Lemma partition_1 : compat_bool E.eq f →
  Equal (fst (partition f s)) (filter f s).
 Proof.
 unfold partition, filter, Equal, In; simpl ;intros H a.
 rewrite partition_in_1, filter_in; intuition.
 Qed.

 Lemma partition_2 : compat_bool E.eq f →
  Equal (snd (partition f s)) (filter (fun x ⇒ negb (f x)) s).
 Proof.
 unfold partition, filter, Equal, In; simpl ;intros H a.
 rewrite partition_in_2, filter_in; intuition.
 rewrite H2; auto.
 destruct (f a); auto.
 repeat red; intros; f_equal.
 rewrite (H _ _ H0); auto.
 Qed.

 End Filter.

 Lemma elements_1 : In x s → InA E.eq x (elements s).
 Proof. wrap elements elements_in. Qed.
 Lemma elements_2 : InA E.eq x (elements s) → In x s.
 Proof. wrap elements elements_in. Qed.
 Lemma elements_3 : sort E.lt (elements s).
 Proof. exact (elements_sort (is_bst s)). Qed.
 Lemma elements_3w : NoDupA E.eq (elements s).
 Proof. exact (elements_nodup (is_bst s)). Qed.

 Lemma min_elt_1 : min_elt s = Some x → In x s.
 Proof. exact (@min_elt_1 s x). Qed.
 Lemma min_elt_2 : min_elt s = Some x → In y s → ¬ E.lt y x.
 Proof. exact (@min_elt_2 s x y (is_bst s)). Qed.
 Lemma min_elt_3 : min_elt s = None → Empty s.
 Proof. exact (@min_elt_3 s). Qed.

 Lemma max_elt_1 : max_elt s = Some x → In x s.
 Proof. exact (@max_elt_1 s x). Qed.
 Lemma max_elt_2 : max_elt s = Some x → In y s → ¬ E.lt x y.
 Proof. exact (@max_elt_2 s x y (is_bst s)). Qed.
 Lemma max_elt_3 : max_elt s = None → Empty s.
 Proof. exact (@max_elt_3 s). Qed.

 Lemma choose_1 : choose s = Some x → In x s.
 Proof. exact (@choose_1 s x). Qed.
 Lemma choose_2 : choose s = None → Empty s.
 Proof. exact (@choose_2 s). Qed.
 Lemma choose_3 : choose s = Some x → choose s' = Some y →
  Equal s s' → E.eq x y.
 Proof. exact (@choose_3 _ _ (is_bst s) (is_bst s') x y). Qed.

 Lemma eq_refl : eq s s.
 Proof. exact (eq_refl s). Qed.
 Lemma eq_sym : eq s s' → eq s' s.
 Proof. exact (@eq_sym s s'). Qed.
 Lemma eq_trans : eq s s' → eq s' s'' → eq s s''.
 Proof. exact (@eq_trans s s' s''). Qed.

 Lemma lt_trans : lt s s' → lt s' s'' → lt s s''.
 Proof. exact (@lt_trans s s' s''). Qed.
 Lemma lt_not_eq : lt s s' → ¬eq s s'.
 Proof. exact (@lt_not_eq _ _ (is_bst s) (is_bst s')). Qed.

 End Specs.
End IntMake.


Module Make (X: OrderedType) <: S with Module E := X
 :=IntMake(Z_as_Int)(X).