diff options
Diffstat (limited to 'theories/FSets/FSetFullAVL.v')
| -rw-r--r-- | theories/FSets/FSetFullAVL.v | 1125 |
1 files changed, 1125 insertions, 0 deletions
diff --git a/theories/FSets/FSetFullAVL.v b/theories/FSets/FSetFullAVL.v new file mode 100644 index 00000000..1fc109f3 --- /dev/null +++ b/theories/FSets/FSetFullAVL.v @@ -0,0 +1,1125 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* Finite sets library. + * Authors: Pierre Letouzey and Jean-Christophe Filliâtre + * Institution: LRI, CNRS UMR 8623 - Université Paris Sud + * 91405 Orsay, France *) + +(* $Id: FSetFullAVL.v 10739 2008-04-01 14:45:20Z herbelin $ *) + +(** * 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. + +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. + +(** * 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. +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. + +(* Repeat the previous tactic. + Drawback: need to clear the [avl _] hyps ... Thank you Ltac *) + +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. +Proof. + destruct 1; intuition; simpl in *. + avl_nns; simpl in *; elimtype False; omega_max. +Qed. + +(** * 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)). +Proof. + intros; auto. +Qed. +Hint Resolve avl_node. + + +(** empty *) + +Lemma empty_avl : avl empty. +Proof. + auto. +Qed. + +(** singleton *) + +Lemma singleton_avl : forall x : elt, avl (singleton x). +Proof. + unfold singleton; intro. + constructor; auto; try red; simpl; omega_max. +Qed. + +(** create *) + +Lemma create_avl : + forall 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 : + 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. +Proof. + unfold create; auto. +Qed. + +(** bal *) + +Lemma bal_avl : forall 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 : 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. +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 : + 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. +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 : forall 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. + (* LT *) + destruct IHt; auto. + split. + apply bal_avl; auto; omega_max. + omega_bal. + (* EQ *) + intuition; omega_max. + (* GT *) + destruct IHt; auto. + split. + apply bal_avl; auto; omega_max. + omega_bal. +Qed. + +Lemma add_avl : forall 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 : 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. +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 : forall 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 : 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. +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 : forall 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 : 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. +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 : forall 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 : forall 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. + (* LT *) + inv avl. + destruct (IHt H0). + split. + apply bal_avl; auto. + omega_max. + omega_bal. + (* EQ *) + inv avl. + generalize (merge_avl_1 H0 H1 H2). + intuition omega_max. + (* GT *) + inv avl. + destruct (IHt H1). + split. + apply bal_avl; auto. + omega_max. + omega_bal. +Qed. + +Lemma remove_avl : forall 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 : forall 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 : forall 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 : forall 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 : forall 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 : forall 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 : forall 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 : forall f s, avl s -> avl (filter f s). +Proof. + unfold filter; intros; apply filter_acc_avl; auto. +Qed. + +(** partition *) + +Lemma partition_acc_avl_1 : forall 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 : forall 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 : forall f s, avl s -> avl (partition f s)#1. +Proof. + unfold partition; intros; apply partition_acc_avl_1; auto. +Qed. + +Lemma partition_avl_2 : forall 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 : forall 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 : forall 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 : forall 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 : forall 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 : forall 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. + +Import Logic. (* Unhide eq, otherwise Function complains. *) + +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 : 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). +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. + (* add x2 s#1 *) + 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. + (* join (union (l1,l2')) x1 (union (r1,r2')) *) + 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. + (* add x1 s#2 *) + 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. + (* join (union (l1',l2)) x1 (union (r1',r2)) *) + 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 : forall 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. + (* join (union (l1,l2')) x1 (union (r1,r2')) *) + 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. + (* join (union (l1',l2)) x1 (union (r1',r2)) *) + 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 : forall 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 : forall 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 : forall 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 : forall 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 : forall 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 : forall 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 : forall 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. + +Lemma ocaml_compare_alt : forall 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; elimtype False. + 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 : forall 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 : forall 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 : forall 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 := 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. + 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. + intros (s,b,a) (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. + intros (s,b,a) (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. + + (* specs *) + 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 : forall (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. + 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. + +(* For concrete use inside Coq, we propose an instantiation of [Int] by [Z]. *) + +Module Make (X: OrderedType) <: S with Module E := X + :=IntMake(Z_as_Int)(X). + |