diff options
Diffstat (limited to 'theories/FSets/FMapAVL.v')
| -rw-r--r-- | theories/FSets/FMapAVL.v | 2058 |
1 files changed, 2058 insertions, 0 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v new file mode 100644 index 00000000..425528ee --- /dev/null +++ b/theories/FSets/FMapAVL.v @@ -0,0 +1,2058 @@ + +(***********************************************************************) +(* 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 map library. *) + +(* $Id: FMapAVL.v 8899 2006-06-06 11:09:43Z jforest $ *) + +(** This module implements map using AVL trees. + It follows the implementation from Ocaml's standard library. *) + +Require Import FSetInterface. +Require Import FMapInterface. +Require Import FMapList. + +Require Import ZArith. +Require Import Int. + +Set Firstorder Depth 3. +Set Implicit Arguments. +Unset Strict Implicit. + + +Module Raw (I:Int)(X: OrderedType). +Import I. +Module II:=MoreInt(I). +Import II. +Open Scope Int_scope. + +Module E := X. +Module MX := OrderedTypeFacts X. +Module PX := KeyOrderedType X. +Module L := FMapList.Raw X. +Import MX. +Import PX. + +Definition key := X.t. + +(** * Trees *) + +Section Elt. + +Variable elt : Set. + +(* Now in KeyOrderedType: +Definition eqk (p p':key*elt) := X.eq (fst p) (fst p'). +Definition eqke (p p':key*elt) := + X.eq (fst p) (fst p') /\ (snd p) = (snd p'). +Definition ltk (p p':key*elt) := X.lt (fst p) (fst p'). +*) + +Notation eqk := (eqk (elt:= elt)). +Notation eqke := (eqke (elt:= elt)). +Notation ltk := (ltk (elt:= elt)). + +Inductive tree : Set := + | Leaf : tree + | Node : tree -> key -> elt -> tree -> int -> tree. + +Notation t := tree. + +(** The Sixth field of [Node] is the height of the tree *) + +(** * Occurrence in a tree *) + +Inductive MapsTo (x : key)(e : elt) : tree -> Prop := + | MapsRoot : forall l r h y, + X.eq x y -> MapsTo x e (Node l y e r h) + | MapsLeft : forall l r h y e', + MapsTo x e l -> MapsTo x e (Node l y e' r h) + | MapsRight : forall l r h y e', + MapsTo x e r -> MapsTo x e (Node l y e' r h). + +Inductive In (x : key) : tree -> Prop := + | InRoot : forall l r h y e, + X.eq x y -> In x (Node l y e r h) + | InLeft : forall l r h y e', + In x l -> In x (Node l y e' r h) + | InRight : forall l r h y e', + In x r -> In x (Node l y e' r h). + +Definition In0 (k:key)(m:t) : Prop := exists e:elt, MapsTo k e m. + +(** * Binary search trees *) + +(** [lt_tree x s]: all elements in [s] are smaller than [x] + (resp. greater for [gt_tree]) *) + +Definition lt_tree x s := forall y:key, In y s -> X.lt y x. +Definition gt_tree x s := forall y:key, In y s -> X.lt x y. + +(** [bst t] : [t] is a binary search tree *) + +Inductive bst : tree -> Prop := + | BSLeaf : bst Leaf + | BSNode : forall x e l r h, + bst l -> bst r -> lt_tree x l -> gt_tree x r -> bst (Node l x e r h). + +(** * 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 (s : tree) : int := + match s with + | Leaf => 0 + | Node _ _ _ _ h => h + end. + +Inductive avl : tree -> Prop := + | RBLeaf : avl Leaf + | RBNode : forall x e l r h, + avl l -> + avl r -> + -(2) <= height l - height r <= 2 -> + h = max (height l) (height r) + 1 -> + avl (Node l x e r h). + +(* We should end this section before the big proofs that follows, + otherwise the discharge takes a lot of time. *) +End Elt. + +(** Some helpful hints and tactics. *) + +Notation t := tree. +Hint Constructors tree. +Hint Constructors MapsTo. +Hint Constructors In. +Hint Constructors bst. +Hint Constructors avl. +Hint Unfold lt_tree gt_tree. + +Ltac inv f := + match goal with + | H:f (Leaf _) |- _ => inversion_clear H; inv f + | H:f _ (Leaf _) |- _ => inversion_clear H; inv f + | H:f _ _ (Leaf _) |- _ => inversion_clear H; inv f + | H:f _ _ _ (Leaf _) |- _ => inversion_clear H; inv f + | H:f (Node _ _ _ _ _) |- _ => inversion_clear H; inv f + | H:f _ (Node _ _ _ _ _) |- _ => inversion_clear H; inv f + | H:f _ _ (Node _ _ _ _ _) |- _ => inversion_clear H; inv f + | H:f _ _ _ (Node _ _ _ _ _) |- _ => inversion_clear H; inv f + | _ => idtac + end. + +Ltac safe_inv f := match goal with + | H:f (Node _ _ _ _ _) |- _ => + generalize H; inversion_clear H; safe_inv f + | H:f _ (Node _ _ _ _ _) |- _ => + generalize H; inversion_clear H; safe_inv f + | _ => intros + end. + +Ltac inv_all f := + match goal with + | H: f _ |- _ => inversion_clear H; inv f + | H: f _ _ |- _ => inversion_clear H; inv f + | H: f _ _ _ |- _ => inversion_clear H; inv f + | H: f _ _ _ _ |- _ => inversion_clear H; inv f + | _ => idtac + end. + +Ltac order := match goal with + | H: lt_tree ?x ?s, H1: In ?y ?s |- _ => generalize (H _ H1); clear H; order + | H: gt_tree ?x ?s, H1: In ?y ?s |- _ => generalize (H _ H1); clear H; order + | _ => MX.order +end. + +Ltac intuition_in := repeat progress (intuition; inv In; inv MapsTo). +Ltac firstorder_in := repeat progress (firstorder; inv In; inv MapsTo). + +Lemma height_non_negative : forall elt (s : t elt), avl s -> height s >= 0. +Proof. + induction s; simpl; intros; auto with zarith. + inv avl; intuition; omega_max. +Qed. + +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. + + +(** Facts about [MapsTo] and [In]. *) + +Lemma MapsTo_In : forall elt k e (m:t elt), MapsTo k e m -> In k m. +Proof. + induction 1; auto. +Qed. +Hint Resolve MapsTo_In. + +Lemma In_MapsTo : forall elt k (m:t elt), In k m -> exists e, MapsTo k e m. +Proof. + induction 1; try destruct IHIn as (e,He); exists e; auto. +Qed. + +Lemma In_alt : forall elt k (m:t elt), In0 k m <-> In k m. +Proof. + split. + intros (e,H); eauto. + unfold In0; apply In_MapsTo; auto. +Qed. + +Lemma MapsTo_1 : + forall elt (m:t elt) x y e, X.eq x y -> MapsTo x e m -> MapsTo y e m. +Proof. + induction m; simpl; intuition_in; eauto. +Qed. +Hint Immediate MapsTo_1. + +Lemma In_1 : + forall elt (m:t elt) x y, X.eq x y -> In x m -> In y m. +Proof. + intros elt m x y; induction m; simpl; intuition_in; eauto. +Qed. + + +(** Results about [lt_tree] and [gt_tree] *) + +Lemma lt_leaf : forall elt x, lt_tree x (Leaf elt). +Proof. + unfold lt_tree in |- *; intros; intuition_in. +Qed. + +Lemma gt_leaf : forall elt x, gt_tree x (Leaf elt). +Proof. + unfold gt_tree in |- *; intros; intuition_in. +Qed. + +Lemma lt_tree_node : forall elt x y (l:t elt) r e h, + lt_tree x l -> lt_tree x r -> X.lt y x -> lt_tree x (Node l y e r h). +Proof. + unfold lt_tree in *; firstorder_in; order. +Qed. + +Lemma gt_tree_node : forall elt x y (l:t elt) r e h, + gt_tree x l -> gt_tree x r -> X.lt x y -> gt_tree x (Node l y e r h). +Proof. + unfold gt_tree in *; firstorder_in; order. +Qed. + +Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node. + +Lemma lt_left : forall elt x y (l: t elt) r e h, + lt_tree x (Node l y e r h) -> lt_tree x l. +Proof. + intuition_in. +Qed. + +Lemma lt_right : forall elt x y (l:t elt) r e h, + lt_tree x (Node l y e r h) -> lt_tree x r. +Proof. + intuition_in. +Qed. + +Lemma gt_left : forall elt x y (l:t elt) r e h, + gt_tree x (Node l y e r h) -> gt_tree x l. +Proof. + intuition_in. +Qed. + +Lemma gt_right : forall elt x y (l:t elt) r e h, + gt_tree x (Node l y e r h) -> gt_tree x r. +Proof. + intuition_in. +Qed. + +Hint Resolve lt_left lt_right gt_left gt_right. + +Lemma lt_tree_not_in : + forall elt x (t : t elt), lt_tree x t -> ~ In x t. +Proof. + intros; intro; generalize (H _ H0); order. +Qed. + +Lemma lt_tree_trans : + forall elt x y, X.lt x y -> forall (t:t elt), lt_tree x t -> lt_tree y t. +Proof. + firstorder eauto. +Qed. + +Lemma gt_tree_not_in : + forall elt x (t : t elt), gt_tree x t -> ~ In x t. +Proof. + intros; intro; generalize (H _ H0); order. +Qed. + +Lemma gt_tree_trans : + forall elt x y, X.lt y x -> forall (t:t elt), gt_tree x t -> gt_tree y t. +Proof. + firstorder eauto. +Qed. + +Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans. + +(** Results about [avl] *) + +Lemma avl_node : forall elt x e (l:t elt) r, + avl l -> + avl r -> + -(2) <= height l - height r <= 2 -> + avl (Node l x e r (max (height l) (height r) + 1)). +Proof. + intros; auto. +Qed. +Hint Resolve avl_node. + +(** * Helper functions *) + +(** [create l x r] creates a node, assuming [l] and [r] + to be balanced and [|height l - height r| <= 2]. *) + +Definition create elt (l:t elt) x e r := + Node l x e r (max (height l) (height r) + 1). + +Lemma create_bst : + forall elt (l:t elt) x e r, bst l -> bst r -> lt_tree x l -> gt_tree x r -> + bst (create l x e r). +Proof. + unfold create; auto. +Qed. +Hint Resolve create_bst. + +Lemma create_avl : + forall elt (l:t elt) x e r, avl l -> avl r -> -(2) <= height l - height r <= 2 -> + avl (create l x e r). +Proof. + unfold create; auto. +Qed. + +Lemma create_height : + forall elt (l:t elt) x e r, avl l -> avl r -> -(2) <= height l - height r <= 2 -> + height (create l x e r) = max (height l) (height r) + 1. +Proof. + unfold create; intros; auto. +Qed. + +Lemma create_in : + forall elt (l:t elt) x e r y, In y (create l x e r) <-> X.eq y x \/ In y l \/ In y r. +Proof. + unfold create; split; [ inversion_clear 1 | ]; intuition. +Qed. + +(** trick for emulating [assert false] in Coq *) + +Notation assert_false := Leaf. + +(** [bal l x e r] acts as [create], but performs one step of + rebalancing if necessary, i.e. assumes [|height l - height r| <= 3]. *) + +Definition bal elt (l: tree elt) x e r := + let hl := height l in + let hr := height r in + if gt_le_dec hl (hr+2) then + match l with + | Leaf => assert_false _ + | Node ll lx le lr _ => + if ge_lt_dec (height ll) (height lr) then + create ll lx le (create lr x e r) + else + match lr with + | Leaf => assert_false _ + | Node lrl lrx lre lrr _ => + create (create ll lx le lrl) lrx lre (create lrr x e r) + end + end + else + if gt_le_dec hr (hl+2) then + match r with + | Leaf => assert_false _ + | Node rl rx re rr _ => + if ge_lt_dec (height rr) (height rl) then + create (create l x e rl) rx re rr + else + match rl with + | Leaf => assert_false _ + | Node rll rlx rle rlr _ => + create (create l x e rll) rlx rle (create rlr rx re rr) + end + end + else + create l x e r. + +Ltac bal_tac := + intros elt l x e r; + unfold bal; + destruct (gt_le_dec (height l) (height r + 2)); + [ destruct l as [ |ll lx le lr lh]; + [ | destruct (ge_lt_dec (height ll) (height lr)); + [ | destruct lr ] ] + | destruct (gt_le_dec (height r) (height l + 2)); + [ destruct r as [ |rl rx re rr rh]; + [ | destruct (ge_lt_dec (height rr) (height rl)); + [ | destruct rl ] ] + | ] ]; intros. + +Ltac bal_tac_imp := match goal with + | |- context [ assert_false ] => + inv avl; avl_nns; simpl in *; false_omega + | _ => idtac +end. + +Lemma bal_bst : forall elt (l:t elt) x e r, bst l -> bst r -> + lt_tree x l -> gt_tree x r -> bst (bal l x e r). +Proof. + bal_tac; + inv bst; repeat apply create_bst; auto; unfold create; + apply lt_tree_node || apply gt_tree_node; auto; + eapply lt_tree_trans || eapply gt_tree_trans || eauto; eauto. +Qed. + +Lemma bal_avl : forall elt (l:t elt) x e r, avl l -> avl r -> + -(3) <= height l - height r <= 3 -> avl (bal l x e r). +Proof. + bal_tac; inv avl; repeat apply create_avl; simpl in *; auto; omega_max. +Qed. + +Lemma bal_height_1 : forall elt (l:t elt) x e r, avl l -> avl r -> + -(3) <= height l - height r <= 3 -> + 0 <= height (bal l x e r) - max (height l) (height r) <= 1. +Proof. + bal_tac; inv avl; avl_nns; simpl in *; omega_max. +Qed. + +Lemma bal_height_2 : + forall elt (l:t elt) x e r, avl l -> avl r -> -(2) <= height l - height r <= 2 -> + height (bal l x e r) == max (height l) (height r) +1. +Proof. + bal_tac; inv avl; simpl in *; omega_max. +Qed. + +Lemma bal_in : forall elt (l:t elt) x e r y, avl l -> avl r -> + (In y (bal l x e r) <-> X.eq y x \/ In y l \/ In y r). +Proof. + bal_tac; bal_tac_imp; repeat rewrite create_in; intuition_in. +Qed. + +Lemma bal_mapsto : forall elt (l:t elt) x e r y e', avl l -> avl r -> + (MapsTo y e' (bal l x e r) <-> MapsTo y e' (create l x e r)). +Proof. + bal_tac; bal_tac_imp; unfold create; intuition_in. +Qed. + +Ltac omega_bal := match goal with + | H:avl ?l, H':avl ?r |- context [ bal ?l ?x ?e ?r ] => + generalize (bal_height_1 x e H H') (bal_height_2 x e H H'); + omega_max + end. + +(** * Insertion *) + +Function add (elt:Set)(x:key)(e:elt)(s:t elt) { struct s } : t elt := match s with + | Leaf => Node (Leaf _) x e (Leaf _) 1 + | Node l y e' r h => + match X.compare x y with + | LT _ => bal (add x e l) y e' r + | EQ _ => Node l y e r h + | GT _ => bal l y e' (add x e r) + end + end. + +Lemma add_avl_1 : forall elt (m:t elt) x e, avl m -> + avl (add x e m) /\ 0 <= height (add x e m) - height m <= 1. +Proof. + intros elt m x e; functional induction (add x e m); 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 elt (m:t elt) x e, avl m -> avl (add x e m). +Proof. + intros; generalize (add_avl_1 x e H); intuition. +Qed. +Hint Resolve add_avl. + +Lemma add_in : forall elt (m:t elt) x y e, avl m -> + (In y (add x e m) <-> X.eq y x \/ In y m). +Proof. + intros elt m x y e; functional induction (add x e m); auto; intros. + intuition_in. + (* LT *) + inv avl. + rewrite bal_in; auto. + rewrite (IHt H1); intuition_in. + (* EQ *) + inv avl. + firstorder_in. + eapply In_1; eauto. + (* GT *) + inv avl. + rewrite bal_in; auto. + rewrite (IHt H2); intuition_in. +Qed. + +Lemma add_bst : forall elt (m:t elt) x e, bst m -> avl m -> bst (add x e m). +Proof. + intros elt m x e; functional induction (add x e m); + intros; inv bst; inv avl; auto; apply bal_bst; auto. + (* lt_tree -> lt_tree (add ...) *) + red; red in H4. + intros. + rewrite (add_in x y0 e H) in H1. + intuition. + eauto. + (* gt_tree -> gt_tree (add ...) *) + red; red in H5. + intros. + rewrite (add_in x y0 e H6) in H1. + intuition. + apply lt_eq with x; auto. +Qed. + +Lemma add_1 : forall elt (m:t elt) x y e, avl m -> X.eq x y -> MapsTo y e (add x e m). +Proof. + intros elt m x y e; functional induction (add x e m); + intros; inv bst; inv avl; try rewrite bal_mapsto; unfold create; eauto. +Qed. + +Lemma add_2 : forall elt (m:t elt) x y e e', avl m -> ~X.eq x y -> + MapsTo y e m -> MapsTo y e (add x e' m). +Proof. + intros elt m x y e e'; induction m; simpl; auto. + destruct (X.compare x k); + intros; inv bst; inv avl; try rewrite bal_mapsto; unfold create; auto; + inv MapsTo; auto; order. +Qed. + +Lemma add_3 : forall elt (m:t elt) x y e e', avl m -> ~X.eq x y -> + MapsTo y e (add x e' m) -> MapsTo y e m. +Proof. + intros elt m x y e e'; induction m; simpl; auto. + intros; inv avl; inv MapsTo; auto; order. + destruct (X.compare x k); intro; inv avl; + try rewrite bal_mapsto; auto; unfold create; intros; inv MapsTo; auto; + order. +Qed. + + +(** * Extraction of minimum binding + + morally, [remove_min] is to be applied to a non-empty tree + [t = Node l x e r h]. Since we can't deal here with [assert false] + for [t=Leaf], we pre-unpack [t] (and forget about [h]). +*) + +Function remove_min (elt:Set)(l:t elt)(x:key)(e:elt)(r:t elt) { struct l } : t elt*(key*elt) := + match l with + | Leaf => (r,(x,e)) + | Node ll lx le lr lh => let (l',m) := (remove_min ll lx le lr : t elt*(key*elt)) in (bal l' x e r, m) + end. + +Lemma remove_min_avl_1 : forall elt (l:t elt) x e r h, avl (Node l x e r h) -> + avl (fst (remove_min l x e r)) /\ + 0 <= height (Node l x e r h) - height (fst (remove_min l x e r)) <= 1. +Proof. + intros elt l x e r; functional induction (remove_min l x e r); simpl in *; intros. + inv avl; simpl in *; split; auto. + avl_nns; omega_max. + (* l = Node *) + inversion_clear H. + destruct (IHp lh); auto. + split; simpl in *. + rewrite_all H0. simpl in *. + apply bal_avl; subst;auto; omega_max. + rewrite_all H0;simpl in *;omega_bal. +Qed. + +Lemma remove_min_avl : forall elt (l:t elt) x e r h, avl (Node l x e r h) -> + avl (fst (remove_min l x e r)). +Proof. + intros; generalize (remove_min_avl_1 H); intuition. +Qed. + +Lemma remove_min_in : forall elt (l:t elt) x e r h y, avl (Node l x e r h) -> + (In y (Node l x e r h) <-> + X.eq y (fst (snd (remove_min l x e r))) \/ In y (fst (remove_min l x e r))). +Proof. + intros elt l x e r; functional induction (remove_min l x e r); simpl in *; intros. + intuition_in. + (* l = Node *) + inversion_clear H. + generalize (remove_min_avl H1). + + rewrite_all H0; simpl; intros. + rewrite bal_in; auto. + generalize (IHp lh y H1). + intuition. + inversion_clear H8; intuition. +Qed. + +Lemma remove_min_mapsto : forall elt (l:t elt) x e r h y e', avl (Node l x e r h) -> + (MapsTo y e' (Node l x e r h) <-> + ((X.eq y (fst (snd (remove_min l x e r))) /\ e' = (snd (snd (remove_min l x e r)))) + \/ MapsTo y e' (fst (remove_min l x e r)))). +Proof. + intros elt l x e r; functional induction (remove_min l x e r); simpl in *; intros. + intuition_in; subst; auto. + (* l = Node *) + inversion_clear H. + generalize (remove_min_avl H1). + rewrite_all H0; simpl; intros. + rewrite bal_mapsto; auto; unfold create. + simpl in *;destruct (IHp lh y e'). + auto. + intuition. + inversion_clear H3; intuition. + inversion_clear H10; intuition. +Qed. + +Lemma remove_min_bst : forall elt (l:t elt) x e r h, + bst (Node l x e r h) -> avl (Node l x e r h) -> bst (fst (remove_min l x e r)). +Proof. + intros elt l x e r; functional induction (remove_min l x e r); simpl in *; intros. + inv bst; auto. + inversion_clear H; inversion_clear H1. + apply bal_bst; auto. + rewrite_all H0;simpl in *;firstorder. + intro; intros. + generalize (remove_min_in y H). + rewrite_all H0; simpl in *. + destruct 1. + apply H4; intuition. +Qed. + +Lemma remove_min_gt_tree : forall elt (l:t elt) x e r h, + bst (Node l x e r h) -> avl (Node l x e r h) -> + gt_tree (fst (snd (remove_min l x e r))) (fst (remove_min l x e r)). +Proof. + intros elt l x e r; functional induction (remove_min l x e r); simpl in *; intros. + inv bst; auto. + inversion_clear H; inversion_clear H1. + intro; intro. + rewrite_all H0;simpl in *. + generalize (IHp lh H2 H); clear H7 H8 IHp. + generalize (remove_min_avl H). + generalize (remove_min_in (fst m) H). + rewrite H0; simpl; intros. + rewrite (bal_in x e y H8 H6) in H1. + destruct H7. + firstorder. + apply lt_eq with x; auto. + apply X.lt_trans with x; auto. +Qed. + +(** * 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]. +*) + +Function merge (elt:Set) (s1 s2 : t elt) : tree elt := match s1,s2 with + | Leaf, _ => s2 + | _, Leaf => s1 + | _, Node l2 x2 e2 r2 h2 => + match remove_min l2 x2 e2 r2 with + (s2',(x,e)) => bal s1 x e s2' + end +end. + +Lemma merge_avl_1 : forall elt (s1 s2:t elt), 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 elt s1 s2; functional induction (merge s1 s2); simpl in *; intros. + split; auto; avl_nns; omega_max. + destruct s1;try contradiction;clear H1. + split; auto; avl_nns; simpl in *; omega_max. + destruct s1;try contradiction;clear H1. + generalize (remove_min_avl_1 H0). + rewrite H2; simpl;destruct 1. + split. + apply bal_avl; auto. + simpl; omega_max. + omega_bal. +Qed. + +Lemma merge_avl : forall elt (s1 s2:t elt), avl s1 -> avl s2 -> + -(2) <= height s1 - height s2 <= 2 -> avl (merge s1 s2). +Proof. + intros; generalize (merge_avl_1 H H0 H1); intuition. +Qed. + +Lemma merge_in : forall elt (s1 s2:t elt) y, bst s1 -> avl s1 -> bst s2 -> avl s2 -> + (In y (merge s1 s2) <-> In y s1 \/ In y s2). +Proof. + intros elt s1 s2; functional induction (merge s1 s2);intros. + intuition_in. + intuition_in. + destruct s1;try contradiction;clear H1. +(* rewrite H_eq_2; rewrite H_eq_2 in H_eq_1; clear H_eq_2. *) + replace s2' with (fst (remove_min l2 x2 e2 r2)); [|rewrite H2; auto]. + rewrite bal_in; auto. + generalize (remove_min_avl H4); rewrite H2; simpl; auto. + generalize (remove_min_in y H4); rewrite H2; simpl; intro. + rewrite H1; intuition. +Qed. + +Lemma merge_mapsto : forall elt (s1 s2:t elt) y e, bst s1 -> avl s1 -> bst s2 -> avl s2 -> + (MapsTo y e (merge s1 s2) <-> MapsTo y e s1 \/ MapsTo y e s2). +Proof. + intros elt s1 s2; functional induction (@merge elt s1 s2); intros. + intuition_in. + intuition_in. + destruct s1;try contradiction;clear H1. + replace s2' with (fst (remove_min l2 x2 e2 r2)); [|rewrite H2; auto]. + rewrite bal_mapsto; auto; unfold create. + generalize (remove_min_avl H4); rewrite H2; simpl; auto. + generalize (remove_min_mapsto y e0 H4); rewrite H2; simpl; intro. + rewrite H1; intuition (try subst; auto). + inversion_clear H1; intuition. +Qed. + +Lemma merge_bst : forall elt (s1 s2:t elt), bst s1 -> avl s1 -> bst s2 -> avl s2 -> + (forall y1 y2 : key, In y1 s1 -> In y2 s2 -> X.lt y1 y2) -> + bst (merge s1 s2). +Proof. + intros elt s1 s2; functional induction (@merge elt s1 s2); intros; auto. + + apply bal_bst; auto. + destruct s1;try contradiction. + generalize (remove_min_bst H3); rewrite H2; simpl in *; auto. + destruct s1;try contradiction. + intro; intro. + apply H5; auto. + generalize (remove_min_in x H4); rewrite H2; simpl; intuition. + destruct s1;try contradiction. + generalize (remove_min_gt_tree H3); rewrite H2; simpl; auto. +Qed. + +(** * Deletion *) + +Function remove (elt:Set)(x:key)(s:t elt) { struct s } : t elt := match s with + | Leaf => Leaf _ + | Node l y e r h => + match X.compare x y with + | LT _ => bal (remove x l) y e r + | EQ _ => merge l r + | GT _ => bal l y e (remove x r) + end + end. + +Lemma remove_avl_1 : forall elt (s:t elt) x, avl s -> + avl (remove x s) /\ 0 <= height s - height (remove x s) <= 1. +Proof. + intros elt s x; functional induction (@remove elt x s); intros. + split; auto; omega_max. + (* LT *) + inv avl. + destruct (IHt H1). + split. + apply bal_avl; auto. + omega_max. + omega_bal. + (* EQ *) + inv avl. + generalize (merge_avl_1 H1 H2 H3). + intuition omega_max. + (* GT *) + inv avl. + destruct (IHt H2). + split. + apply bal_avl; auto. + omega_max. + omega_bal. +Qed. + +Lemma remove_avl : forall elt (s:t elt) x, avl s -> avl (remove x s). +Proof. + intros; generalize (remove_avl_1 x H); intuition. +Qed. +Hint Resolve remove_avl. + +Lemma remove_in : forall elt (s:t elt) x y, bst s -> avl s -> + (In y (remove x s) <-> ~ X.eq y x /\ In y s). +Proof. + intros elt s x; functional induction (@remove elt x s); simpl; intros. + intuition_in. + (* LT *) + inv avl; inv bst; clear H0. + rewrite bal_in; auto. + generalize (IHt y0 H1); intuition; [ order | order | intuition_in ]. + (* EQ *) + inv avl; inv bst; clear H0. + rewrite merge_in; intuition; [ order | order | intuition_in ]. + elim H9; eauto. + (* GT *) + inv avl; inv bst; clear H0. + rewrite bal_in; auto. + generalize (IHt y0 H6); intuition; [ order | order | intuition_in ]. +Qed. + +Lemma remove_bst : forall elt (s:t elt) x, bst s -> avl s -> bst (remove x s). +Proof. + intros elt s x; functional induction (@remove elt x s); simpl; intros. + auto. + (* LT *) + inv avl; inv bst. + apply bal_bst; auto. + intro; intro. + rewrite (remove_in x y0 H1) in H; auto. + destruct H; eauto. + (* EQ *) + inv avl; inv bst. + apply merge_bst; eauto. + (* GT *) + inv avl; inv bst. + apply bal_bst; auto. + intro; intro. + rewrite (remove_in x y0 H6) in H; auto. + destruct H; eauto. +Qed. + +Lemma remove_1 : forall elt (m:t elt) x y, bst m -> avl m -> X.eq x y -> ~ In y (remove x m). +Proof. + intros; rewrite remove_in; intuition. +Qed. + +Lemma remove_2 : forall elt (m:t elt) x y e, bst m -> avl m -> ~X.eq x y -> + MapsTo y e m -> MapsTo y e (remove x m). +Proof. + intros elt m x y e; induction m; simpl; auto. + destruct (X.compare x k); + intros; inv bst; inv avl; try rewrite bal_mapsto; unfold create; auto; + try solve [inv MapsTo; auto]. + rewrite merge_mapsto; auto. + inv MapsTo; auto; order. +Qed. + +Lemma remove_3 : forall elt (m:t elt) x y e, bst m -> avl m -> + MapsTo y e (remove x m) -> MapsTo y e m. +Proof. + intros elt m x y e; induction m; simpl; auto. + destruct (X.compare x k); intros Bs Av; inv avl; inv bst; + try rewrite bal_mapsto; auto; unfold create. + intros; inv MapsTo; auto. + rewrite merge_mapsto; intuition. + intros; inv MapsTo; auto. +Qed. + +Section Elt2. + +Variable elt:Set. + +Notation eqk := (eqk (elt:= elt)). +Notation eqke := (eqke (elt:= elt)). +Notation ltk := (ltk (elt:= elt)). + +(** * Empty map *) + +Definition Empty m := forall (a : key)(e:elt) , ~ MapsTo a e m. + +Definition empty := (Leaf elt). + +Lemma empty_bst : bst empty. +Proof. + unfold empty; auto. +Qed. + +Lemma empty_avl : avl empty. +Proof. + unfold empty; auto. +Qed. + +Lemma empty_1 : Empty empty. +Proof. + unfold empty, Empty; intuition_in. +Qed. + +(** * Emptyness test *) + +Definition is_empty (s:t elt) := match s with Leaf => true | _ => false end. + +Lemma is_empty_1 : forall s, Empty s -> is_empty s = true. +Proof. + destruct s as [|r x e l h]; simpl; auto. + intro H; elim (H x e); auto. +Qed. + +Lemma is_empty_2 : forall s, is_empty s = true -> Empty s. +Proof. + destruct s; simpl; intros; try discriminate; red; intuition_in. +Qed. + +(** * Appartness *) + +(** The [mem] function is deciding appartness. It exploits the [bst] property + to achieve logarithmic complexity. *) + +Function mem (x:key)(m:t elt) { struct m } : bool := + match m with + | Leaf => false + | Node l y e r _ => match X.compare x y with + | LT _ => mem x l + | EQ _ => true + | GT _ => mem x r + end + end. +Implicit Arguments mem. + +Lemma mem_1 : forall s x, bst s -> In x s -> mem x s = true. +Proof. + intros s x. + functional induction (mem x s); inversion_clear 1; auto. + intuition_in. + intuition_in; firstorder; absurd (X.lt x y); eauto. + intuition_in; firstorder; absurd (X.lt y x); eauto. +Qed. + +Lemma mem_2 : forall s x, mem x s = true -> In x s. +Proof. + intros s x. + functional induction (mem x s); firstorder; intros; try discriminate. +Qed. + +Function find (x:key)(m:t elt) { struct m } : option elt := + match m with + | Leaf => None + | Node l y e r _ => match X.compare x y with + | LT _ => find x l + | EQ _ => Some e + | GT _ => find x r + end + end. + +Lemma find_1 : forall m x e, bst m -> MapsTo x e m -> find x m = Some e. +Proof. + intros m x e. + functional induction (find x m); inversion_clear 1; auto. + intuition_in. + intuition_in; firstorder; absurd (X.lt x y); eauto. + intuition_in; auto. + absurd (X.lt x y); eauto. + absurd (X.lt y x); eauto. + intuition_in; firstorder; absurd (X.lt y x); eauto. +Qed. + +Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m. +Proof. + intros m x. + functional induction (find x m); subst;firstorder; intros; try discriminate. + inversion H; subst; auto. +Qed. + +(** An all-in-one spec for [add] used later in the naive [map2] *) + +Lemma add_spec : forall m x y e , bst m -> avl m -> + find x (add y e m) = if eq_dec x y then Some e else find x m. +Proof. +intros. +destruct (eq_dec x y). +apply find_1. +apply add_bst; auto. +eapply MapsTo_1 with y; eauto. +apply add_1; auto. +case_eq (find x m); intros. +apply find_1. +apply add_bst; auto. +apply add_2; auto. +apply find_2; auto. +case_eq (find x (add y e m)); auto; intros. +rewrite <- H1; symmetry. +apply find_1; auto. +eapply add_3; eauto. +apply find_2; eauto. +Qed. + +(** * Elements *) + +(** [elements_tree_aux acc t] catenates the elements of [t] in infix + order to the list [acc] *) + +Fixpoint elements_aux (acc : list (key*elt)) (t : t elt) {struct t} : list (key*elt) := + match t with + | Leaf => acc + | Node l x e r _ => elements_aux ((x,e) :: elements_aux acc r) l + end. + +(** then [elements] is an instanciation with an empty [acc] *) + +Definition elements := elements_aux nil. + +Lemma elements_aux_mapsto : forall s acc x e, + InA eqke (x,e) (elements_aux acc s) <-> MapsTo x e s \/ InA eqke (x,e) acc. +Proof. + induction s as [ | l Hl x e r Hr h ]; simpl; auto. + intuition. + inversion H0. + intros. + rewrite Hl. + destruct (Hr acc x0 e0); clear Hl Hr. + intuition; inversion_clear H3; intuition. + destruct H0; simpl in *; subst; intuition. +Qed. + +Lemma elements_mapsto : forall s x e, InA eqke (x,e) (elements s) <-> MapsTo x e s. +Proof. + intros; generalize (elements_aux_mapsto s nil x e); intuition. + inversion_clear H0. +Qed. + +Lemma elements_in : forall s x, L.PX.In x (elements s) <-> In x s. +Proof. + intros. + unfold L.PX.In. + rewrite <- In_alt; unfold In0. + firstorder. + exists x0. + rewrite <- elements_mapsto; auto. + exists x0. + unfold L.PX.MapsTo; rewrite elements_mapsto; auto. +Qed. + +Lemma elements_aux_sort : forall s acc, bst s -> sort ltk acc -> + (forall x e y, InA eqke (x,e) acc -> In y s -> X.lt y x) -> + sort ltk (elements_aux acc s). +Proof. + induction s as [ | l Hl y e r Hr h]; simpl; intuition. + inv bst. + apply Hl; auto. + constructor. + apply Hr; eauto. + apply (InA_InfA (eqke_refl (elt:=elt))); intros (y',e') H6. + destruct (elements_aux_mapsto r acc y' e'); intuition. + red; simpl; eauto. + red; simpl; eauto. + intros. + inversion_clear H. + destruct H7; simpl in *. + order. + destruct (elements_aux_mapsto r acc x e0); intuition eauto. +Qed. + +Lemma elements_sort : forall s : t elt, bst s -> sort ltk (elements s). +Proof. + intros; unfold elements; apply elements_aux_sort; auto. + intros; inversion H0. +Qed. +Hint Resolve elements_sort. + + +(** * Fold *) + +Fixpoint fold (A : Set) (f : key -> elt -> A -> A)(s : t elt) {struct s} : A -> A := + fun a => match s with + | Leaf => a + | Node l x e r _ => fold f r (f x e (fold f l a)) + end. + +Definition fold' (A : Set) (f : key -> elt -> A -> A)(s : t elt) := + L.fold f (elements s). + +Lemma fold_equiv_aux : + forall (A : Set) (s : t elt) (f : key -> elt -> A -> A) (a : A) acc, + L.fold f (elements_aux acc s) a = L.fold f acc (fold f s a). +Proof. + simple induction s. + simpl in |- *; intuition. + simpl in |- *; intros. + rewrite H. + simpl. + apply H0. +Qed. + +Lemma fold_equiv : + forall (A : Set) (s : t elt) (f : key -> elt -> A -> A) (a : A), + fold f s a = fold' f s a. +Proof. + unfold fold', elements in |- *. + simple induction s; simpl in |- *; auto; intros. + rewrite fold_equiv_aux. + rewrite H0. + simpl in |- *; auto. +Qed. + +Lemma fold_1 : + forall (s:t elt)(Hs:bst s)(A : Set)(i:A)(f : key -> elt -> A -> A), + fold f s i = fold_left (fun a p => f (fst p) (snd p) a) (elements s) i. +Proof. + intros. + rewrite fold_equiv. + unfold fold'. + rewrite L.fold_1. + unfold L.elements; auto. +Qed. + +(** * Comparison *) + +Definition Equal (cmp:elt->elt->bool) m m' := + (forall k, In k m <-> In k m') /\ + (forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true). + +(** ** Enumeration of the elements of a tree *) + +Inductive enumeration : Set := + | End : enumeration + | More : key -> elt -> t elt -> enumeration -> enumeration. + +(** [flatten_e e] returns the list of elements of [e] i.e. the list + of elements actually compared *) + +Fixpoint flatten_e (e : enumeration) : list (key*elt) := match e with + | End => nil + | More x e t r => (x,e) :: elements t ++ flatten_e r + end. + +(** [sorted_e e] expresses that elements in the enumeration [e] are + sorted, and that all trees in [e] are binary search trees. *) + +Inductive In_e (p:key*elt) : enumeration -> Prop := + | InEHd1 : + forall (y : key)(d:elt) (s : t elt) (e : enumeration), + eqke p (y,d) -> In_e p (More y d s e) + | InEHd2 : + forall (y : key) (d:elt) (s : t elt) (e : enumeration), + MapsTo (fst p) (snd p) s -> In_e p (More y d s e) + | InETl : + forall (y : key) (d:elt) (s : t elt) (e : enumeration), + In_e p e -> In_e p (More y d s e). + +Hint Constructors In_e. + +Inductive sorted_e : enumeration -> Prop := + | SortedEEnd : sorted_e End + | SortedEMore : + forall (x : key) (d:elt) (s : t elt) (e : enumeration), + bst s -> + (gt_tree x s) -> + sorted_e e -> + (forall p, In_e p e -> ltk (x,d) p) -> + (forall p, + MapsTo (fst p) (snd p) s -> forall q, In_e q e -> ltk p q) -> + sorted_e (More x d s e). + +Hint Constructors sorted_e. + +Lemma in_flatten_e : + forall p e, InA eqke p (flatten_e e) -> In_e p e. +Proof. + simple induction e; simpl in |- *; intuition. + inversion_clear H. + inversion_clear H0; auto. + elim (InA_app H1); auto. + destruct (elements_mapsto t a b); auto. +Qed. + +Lemma sorted_flatten_e : + forall e : enumeration, sorted_e e -> sort ltk (flatten_e e). +Proof. + simple induction e; simpl in |- *; intuition. + apply cons_sort. + apply (SortA_app (eqke_refl (elt:=elt))); inversion_clear H0; auto. + intros; apply H5; auto. + rewrite <- elements_mapsto; auto; destruct x; auto. + apply in_flatten_e; auto. + inversion_clear H0. + apply In_InfA; intros. + intros; elim (in_app_or _ _ _ H0); intuition. + generalize (In_InA (eqke_refl (elt:=elt)) H6). + destruct y; rewrite elements_mapsto; eauto. + apply H4; apply in_flatten_e; auto. + apply In_InA; auto. +Qed. + +Lemma elements_app : + forall s acc, elements_aux acc s = elements s ++ acc. +Proof. + simple induction s; simpl in |- *; intuition. + rewrite H0. + rewrite H. + unfold elements; simpl. + do 2 rewrite H. + rewrite H0. + repeat rewrite <- app_nil_end. + repeat rewrite app_ass; auto. +Qed. + +Lemma compare_flatten_1 : + forall t1 t2 x e z l, + elements t1 ++ (x,e) :: elements t2 ++ l = + elements (Node t1 x e t2 z) ++ l. +Proof. + simpl in |- *; unfold elements in |- *; simpl in |- *; intuition. + repeat rewrite elements_app. + repeat rewrite <- app_nil_end. + repeat rewrite app_ass; auto. +Qed. + +(** key lemma for correctness *) + +Lemma flatten_e_elements : + forall l r x d z e, + elements l ++ flatten_e (More x d r e) = + elements (Node l x d r z) ++ flatten_e e. +Proof. + intros; simpl. + apply compare_flatten_1. +Qed. + +Open Scope Z_scope. + +(** termination of [compare_aux] *) + +Fixpoint measure_e_t (s : t elt) : Z := match s with + | Leaf => 0 + | Node l _ _ r _ => 1 + measure_e_t l + measure_e_t r + end. + +Fixpoint measure_e (e : enumeration) : Z := match e with + | End => 0 + | More _ _ s r => 1 + measure_e_t s + measure_e r + end. + +Ltac Measure_e_t := unfold measure_e_t in |- *; fold measure_e_t in |- *. +Ltac Measure_e := unfold measure_e in |- *; fold measure_e in |- *. + +Lemma measure_e_t_0 : forall s : t elt, measure_e_t s >= 0. +Proof. + simple induction s. + simpl in |- *; omega. + intros. + Measure_e_t; omega. +Qed. + +Ltac Measure_e_t_0 s := generalize (@measure_e_t_0 s); intro. + +Lemma measure_e_0 : forall e : enumeration, measure_e e >= 0. +Proof. + simple induction e. + simpl in |- *; omega. + intros. + Measure_e; Measure_e_t_0 t; omega. +Qed. + +Ltac Measure_e_0 e := generalize (@measure_e_0 e); intro. + +(** Induction principle over the sum of the measures for two lists *) + +Definition compare_rec2 : + forall P : enumeration -> enumeration -> Set, + (forall x x' : enumeration, + (forall y y' : enumeration, + measure_e y + measure_e y' < measure_e x + measure_e x' -> P y y') -> + P x x') -> + forall x x' : enumeration, P x x'. +Proof. + intros P H x x'. + apply well_founded_induction_type_2 + with (R := fun yy' xx' : enumeration * enumeration => + measure_e (fst yy') + measure_e (snd yy') < + measure_e (fst xx') + measure_e (snd xx')); auto. + apply Wf_nat.well_founded_lt_compat + with (f := fun xx' : enumeration * enumeration => + Zabs_nat (measure_e (fst xx') + measure_e (snd xx'))). + intros; apply Zabs.Zabs_nat_lt. + Measure_e_0 (fst x0); Measure_e_0 (snd x0); Measure_e_0 (fst y); + Measure_e_0 (snd y); intros; omega. +Qed. + +(** [cons t e] adds the elements of tree [t] on the head of + enumeration [e]. Code: + +let rec cons s e = match s with + | Empty -> e + | Node(l, k, d, r, _) -> cons l (More(k, d, r, e)) +*) + +Definition cons : forall s e, bst s -> sorted_e e -> + (forall x y, MapsTo (fst x) (snd x) s -> In_e y e -> ltk x y) -> + { r : enumeration + | sorted_e r /\ + measure_e r = measure_e_t s + measure_e e /\ + flatten_e r = elements s ++ flatten_e e + }. +Proof. + simple induction s; intuition. + (* s = Leaf *) + exists e; intuition. + (* s = Node t k e t0 z *) + clear H0. + case (H (More k e t0 e0)); clear H; intuition. + inv bst; auto. + constructor; inversion_clear H1; auto. + inversion_clear H0; inv bst; intuition. + destruct y; red; red in H4; simpl in *; intuition. + apply lt_eq with k; eauto. + destruct y; red; simpl in *; intuition. + apply X.lt_trans with k; eauto. + exists x; intuition. + generalize H4; Measure_e; intros; Measure_e_t; omega. + rewrite H5. + apply flatten_e_elements. +Qed. + +Definition equal_aux : + forall (cmp: elt -> elt -> bool)(e1 e2:enumeration), + sorted_e e1 -> sorted_e e2 -> + { L.Equal cmp (flatten_e e1) (flatten_e e2) } + + { ~ L.Equal cmp (flatten_e e1) (flatten_e e2) }. +Proof. + intros cmp e1 e2; pattern e1, e2 in |- *; apply compare_rec2. + simple destruct x; simple destruct x'; intuition. + (* x = x' = End *) + left; unfold L.Equal in |- *; intuition. + inversion H2. + (* x = End x' = More *) + right; simpl in |- *; auto. + destruct 1. + destruct (H2 k). + destruct H5; auto. + exists e; auto. + inversion H5. + (* x = More x' = End *) + right; simpl in |- *; auto. + destruct 1. + destruct (H2 k). + destruct H4; auto. + exists e; auto. + inversion H4. + (* x = More k e t e0, x' = More k0 e3 t0 e4 *) + case (X.compare k k0); intro. + (* k < k0 *) + right. + destruct 1. + clear H3 H. + assert (L.PX.In k (flatten_e (More k0 e3 t0 e4))). + destruct (H2 k). + apply H; simpl; exists e; auto. + destruct H. + generalize (Sort_In_cons_2 (sorted_flatten_e H1) (InA_eqke_eqk H)). + compute. + intuition order. + (* k = k0 *) + case_eq (cmp e e3). + intros EQ. + destruct (@cons t e0) as [c1 (H2,(H3,H4))]; try inversion_clear H0; auto. + destruct (@cons t0 e4) as [c2 (H5,(H6,H7))]; try inversion_clear H1; auto. + destruct (H c1 c2); clear H; intuition. + Measure_e; omega. + left. + rewrite H4 in e6; rewrite H7 in e6. + simpl; rewrite <- L.equal_cons; auto. + apply (sorted_flatten_e H0). + apply (sorted_flatten_e H1). + right. + simpl; rewrite <- L.equal_cons; auto. + apply (sorted_flatten_e H0). + apply (sorted_flatten_e H1). + swap f. + rewrite H4; rewrite H7; auto. + right. + destruct 1. + rewrite (H4 k) in H2; try discriminate; simpl; auto. + (* k > k0 *) + right. + destruct 1. + clear H3 H. + assert (L.PX.In k0 (flatten_e (More k e t e0))). + destruct (H2 k0). + apply H3; simpl; exists e3; auto. + destruct H. + generalize (Sort_In_cons_2 (sorted_flatten_e H0) (InA_eqke_eqk H)). + compute. + intuition order. +Qed. + +Lemma Equal_elements : forall cmp s s', + Equal cmp s s' <-> L.Equal cmp (elements s) (elements s'). +Proof. +unfold Equal, L.Equal; split; split; intros. +do 2 rewrite elements_in; firstorder. +destruct H. +apply (H2 k); rewrite <- elements_mapsto; auto. +do 2 rewrite <- elements_in; firstorder. +destruct H. +apply (H2 k); unfold L.PX.MapsTo; rewrite elements_mapsto; auto. +Qed. + +Definition equal : forall cmp s s', bst s -> bst s' -> + {Equal cmp s s'} + {~ Equal cmp s s'}. +Proof. + intros cmp s1 s2 s1_bst s2_bst; simpl. + destruct (@cons s1 End); auto. + inversion_clear 2. + destruct (@cons s2 End); auto. + inversion_clear 2. + simpl in a; rewrite <- app_nil_end in a. + simpl in a0; rewrite <- app_nil_end in a0. + destruct (@equal_aux cmp x x0); intuition. + left. + rewrite H4 in e; rewrite H5 in e. + rewrite Equal_elements; auto. + right. + swap n. + rewrite H4; rewrite H5. + rewrite <- Equal_elements; auto. +Qed. + +End Elt2. + +Section Elts. + +Variable elt elt' elt'' : Set. + +Section Map. +Variable f : elt -> elt'. + +Fixpoint map (m:t elt) {struct m} : t elt' := + match m with + | Leaf => Leaf _ + | Node l v d r h => Node (map l) v (f d) (map r) h + end. + +Lemma map_height : forall m, height (map m) = height m. +Proof. +destruct m; simpl; auto. +Qed. + +Lemma map_avl : forall m, avl m -> avl (map m). +Proof. +induction m; simpl; auto. +inversion_clear 1; constructor; auto; do 2 rewrite map_height; auto. +Qed. + +Lemma map_1 : forall (m: tree elt)(x:key)(e:elt), + MapsTo x e m -> MapsTo x (f e) (map m). +Proof. +induction m; simpl; inversion_clear 1; auto. +Qed. + +Lemma map_2 : forall (m: t elt)(x:key), + In x (map m) -> In x m. +Proof. +induction m; simpl; inversion_clear 1; auto. +Qed. + +Lemma map_bst : forall m, bst m -> bst (map m). +Proof. +induction m; simpl; auto. +inversion_clear 1; constructor; auto. +red; intros; apply H2; apply map_2; auto. +red; intros; apply H3; apply map_2; auto. +Qed. + +End Map. +Section Mapi. +Variable f : key -> elt -> elt'. + +Fixpoint mapi (m:t elt) {struct m} : t elt' := + match m with + | Leaf => Leaf _ + | Node l v d r h => Node (mapi l) v (f v d) (mapi r) h + end. + +Lemma mapi_height : forall m, height (mapi m) = height m. +Proof. +destruct m; simpl; auto. +Qed. + +Lemma mapi_avl : forall m, avl m -> avl (mapi m). +Proof. +induction m; simpl; auto. +inversion_clear 1; constructor; auto; do 2 rewrite mapi_height; auto. +Qed. + +Lemma mapi_1 : forall (m: tree elt)(x:key)(e:elt), + MapsTo x e m -> exists y, X.eq y x /\ MapsTo x (f y e) (mapi m). +Proof. +induction m; simpl; inversion_clear 1; auto. +exists k; auto. +destruct (IHm1 _ _ H0). +exists x0; intuition. +destruct (IHm2 _ _ H0). +exists x0; intuition. +Qed. + +Lemma mapi_2 : forall (m: t elt)(x:key), + In x (mapi m) -> In x m. +Proof. +induction m; simpl; inversion_clear 1; auto. +Qed. + +Lemma mapi_bst : forall m, bst m -> bst (mapi m). +Proof. +induction m; simpl; auto. +inversion_clear 1; constructor; auto. +red; intros; apply H2; apply mapi_2; auto. +red; intros; apply H3; apply mapi_2; auto. +Qed. + +End Mapi. + +Section Map2. +Variable f : option elt -> option elt' -> option elt''. + +(* Not exactly pretty nor perfect, but should suffice as a first naive implem. + Anyway, map2 isn't in Ocaml... +*) + +Definition anti_elements (l:list (key*elt'')) := L.fold (@add _) l (empty _). + +Definition map2 (m:t elt)(m':t elt') : t elt'' := + anti_elements (L.map2 f (elements m) (elements m')). + +Lemma anti_elements_avl_aux : forall (l:list (key*elt''))(m:t elt''), + avl m -> avl (L.fold (@add _) l m). +Proof. +unfold anti_elements; induction l. +simpl; auto. +simpl; destruct a; intros. +apply IHl. +apply add_avl; auto. +Qed. + +Lemma anti_elements_avl : forall l, avl (anti_elements l). +Proof. +unfold anti_elements, empty; intros; apply anti_elements_avl_aux; auto. +Qed. + +Lemma anti_elements_bst_aux : forall (l:list (key*elt''))(m:t elt''), + bst m -> avl m -> bst (L.fold (@add _) l m). +Proof. +induction l. +simpl; auto. +simpl; destruct a; intros. +apply IHl. +apply add_bst; auto. +apply add_avl; auto. +Qed. + +Lemma anti_elements_bst : forall l, bst (anti_elements l). +Proof. +unfold anti_elements, empty; intros; apply anti_elements_bst_aux; auto. +Qed. + +Lemma anti_elements_mapsto_aux : forall (l:list (key*elt'')) m k e, + bst m -> avl m -> NoDupA (eqk (elt:=elt'')) l -> + (forall x, L.PX.In x l -> In x m -> False) -> + (MapsTo k e (L.fold (@add _) l m) <-> L.PX.MapsTo k e l \/ MapsTo k e m). +Proof. +induction l. +simpl; auto. +intuition. +inversion H4. +simpl; destruct a; intros. +rewrite IHl; clear IHl. +apply add_bst; auto. +apply add_avl; auto. +inversion H1; auto. +intros. +inversion_clear H1. +assert (~X.eq x k). + swap H5. + destruct H3. + apply InA_eqA with (x,x0); eauto. +apply (H2 x). +destruct H3; exists x0; auto. +revert H4; do 2 rewrite <- In_alt; destruct 1; exists x0; auto. +eapply add_3; eauto. +intuition. +assert (find k0 (add k e m) = Some e0). + apply find_1; auto. + apply add_bst; auto. +clear H4. +rewrite add_spec in H3; auto. +destruct (eq_dec k0 k). +inversion_clear H3; subst; auto. +right; apply find_2; auto. +inversion_clear H4; auto. +compute in H3; destruct H3. +subst; right; apply add_1; auto. +inversion_clear H1. +destruct (eq_dec k0 k). +destruct (H2 k); eauto. +right; apply add_2; auto. +Qed. + +Lemma anti_elements_mapsto : forall l k e, NoDupA (eqk (elt:=elt'')) l -> + (MapsTo k e (anti_elements l) <-> L.PX.MapsTo k e l). +Proof. +intros. +unfold anti_elements. +rewrite anti_elements_mapsto_aux; auto; unfold empty; auto. +inversion 2. +intuition. +inversion H1. +Qed. + +Lemma map2_avl : forall (m: t elt)(m': t elt'), avl (map2 m m'). +Proof. +unfold map2; intros; apply anti_elements_avl; auto. +Qed. + +Lemma map2_bst : forall (m: t elt)(m': t elt'), bst (map2 m m'). +Proof. +unfold map2; intros; apply anti_elements_bst; auto. +Qed. + +Lemma find_elements : forall (elt:Set)(m: t elt) x, bst m -> + L.find x (elements m) = find x m. +Proof. +intros. +case_eq (find x m); intros. +apply L.find_1. +apply elements_sort; auto. +red; rewrite elements_mapsto. +apply find_2; auto. +case_eq (L.find x (elements m)); auto; intros. +rewrite <- H0; symmetry. +apply find_1; auto. +rewrite <- elements_mapsto. +apply L.find_2; auto. +Qed. + +Lemma find_anti_elements : forall (l: list (key*elt'')) x, sort (@ltk _) l -> + find x (anti_elements l) = L.find x l. +Proof. +intros. +case_eq (L.find x l); intros. +apply find_1. +apply anti_elements_bst; auto. +rewrite anti_elements_mapsto. +apply L.PX.Sort_NoDupA; auto. +apply L.find_2; auto. +case_eq (find x (anti_elements l)); auto; intros. +rewrite <- H0; symmetry. +apply L.find_1; auto. +rewrite <- anti_elements_mapsto. +apply L.PX.Sort_NoDupA; auto. +apply find_2; auto. +Qed. + +Lemma map2_1 : forall (m: t elt)(m': t elt')(x:key), bst m -> bst m' -> + In x m \/ In x m' -> find x (map2 m m') = f (find x m) (find x m'). +Proof. +unfold map2; intros. +rewrite find_anti_elements; auto. +rewrite <- find_elements; auto. +rewrite <- find_elements; auto. +apply L.map2_1; auto. +apply elements_sort; auto. +apply elements_sort; auto. +do 2 rewrite elements_in; auto. +apply L.map2_sorted; auto. +apply elements_sort; auto. +apply elements_sort; auto. +Qed. + +Lemma map2_2 : forall (m: t elt)(m': t elt')(x:key), bst m -> bst m' -> + In x (map2 m m') -> In x m \/ In x m'. +Proof. +unfold map2; intros. +do 2 rewrite <- elements_in. +apply L.map2_2 with (f:=f); auto. +apply elements_sort; auto. +apply elements_sort; auto. +revert H1. +rewrite <- In_alt. +destruct 1. +exists x0. +rewrite <- anti_elements_mapsto; auto. +apply L.PX.Sort_NoDupA; auto. +apply L.map2_sorted; auto. +apply elements_sort; auto. +apply elements_sort; auto. +Qed. + +End Map2. +End Elts. +End Raw. + +(** * Encapsulation + + Now, in order to really provide a functor implementing [S], we + need to encapsulate everything into a type of balanced binary search trees. *) + +Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. + + Module E := X. + Module Raw := Raw I X. + + Record bbst (elt:Set) : Set := + Bbst {this :> Raw.tree elt; is_bst : Raw.bst this; is_avl: Raw.avl this}. + + Definition t := bbst. + Definition key := E.t. + + Section Elt. + Variable elt elt' elt'': Set. + + Implicit Types m : t elt. + Implicit Types x y : key. + Implicit Types e : elt. + + Definition empty : t elt := Bbst (Raw.empty_bst elt) (Raw.empty_avl elt). + Definition is_empty m : bool := Raw.is_empty m.(this). + Definition add x e m : t elt := + Bbst (Raw.add_bst x e m.(is_bst) m.(is_avl)) (Raw.add_avl x e m.(is_avl)). + Definition remove x m : t elt := + Bbst (Raw.remove_bst x m.(is_bst) m.(is_avl)) (Raw.remove_avl x m.(is_avl)). + Definition mem x m : bool := Raw.mem x m.(this). + Definition find x m : option elt := Raw.find x m.(this). + Definition map f m : t elt' := + Bbst (Raw.map_bst f m.(is_bst)) (Raw.map_avl f m.(is_avl)). + Definition mapi (f:key->elt->elt') m : t elt' := + Bbst (Raw.mapi_bst f m.(is_bst)) (Raw.mapi_avl f m.(is_avl)). + Definition map2 f m (m':t elt') : t elt'' := + Bbst (Raw.map2_bst f m m') (Raw.map2_avl f m m'). + Definition elements m : list (key*elt) := Raw.elements m.(this). + Definition fold (A:Set) (f:key->elt->A->A) m i := Raw.fold (A:=A) f m.(this) i. + Definition equal cmp m m' : bool := + if (Raw.equal cmp m.(is_bst) m'.(is_bst)) then true else false. + + Definition MapsTo x e m : Prop := Raw.MapsTo x e m.(this). + Definition In x m : Prop := Raw.In0 x m.(this). + Definition Empty m : Prop := Raw.Empty m.(this). + + Definition eq_key : (key*elt) -> (key*elt) -> Prop := @Raw.PX.eqk elt. + Definition eq_key_elt : (key*elt) -> (key*elt) -> Prop := @Raw.PX.eqke elt. + Definition lt_key : (key*elt) -> (key*elt) -> Prop := @Raw.PX.ltk elt. + + Lemma MapsTo_1 : forall m x y e, E.eq x y -> MapsTo x e m -> MapsTo y e m. + Proof. intros m; exact (@Raw.MapsTo_1 _ m.(this)). Qed. + + Lemma mem_1 : forall m x, In x m -> mem x m = true. + Proof. + unfold In, mem; intros m x; rewrite Raw.In_alt; simpl; apply Raw.mem_1; auto. + apply m.(is_bst). + Qed. + + Lemma mem_2 : forall m x, mem x m = true -> In x m. + Proof. + unfold In, mem; intros m x; rewrite Raw.In_alt; simpl; apply Raw.mem_2; auto. + Qed. + + Lemma empty_1 : Empty empty. + Proof. exact (@Raw.empty_1 elt). Qed. + + Lemma is_empty_1 : forall m, Empty m -> is_empty m = true. + Proof. intros m; exact (@Raw.is_empty_1 _ m.(this)). Qed. + Lemma is_empty_2 : forall m, is_empty m = true -> Empty m. + Proof. intros m; exact (@Raw.is_empty_2 _ m.(this)). Qed. + + Lemma add_1 : forall m x y e, E.eq x y -> MapsTo y e (add x e m). + Proof. intros m x y e; exact (@Raw.add_1 elt _ x y e m.(is_avl)). Qed. + Lemma add_2 : forall m x y e e', ~ E.eq x y -> MapsTo y e m -> MapsTo y e (add x e' m). + Proof. intros m x y e e'; exact (@Raw.add_2 elt _ x y e e' m.(is_avl)). Qed. + Lemma add_3 : forall m x y e e', ~ E.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m. + Proof. intros m x y e e'; exact (@Raw.add_3 elt _ x y e e' m.(is_avl)). Qed. + + Lemma remove_1 : forall m x y, E.eq x y -> ~ In y (remove x m). + Proof. + unfold In, remove; intros m x y; rewrite Raw.In_alt; simpl; apply Raw.remove_1; auto. + apply m.(is_bst). + apply m.(is_avl). + Qed. + Lemma remove_2 : forall m x y e, ~ E.eq x y -> MapsTo y e m -> MapsTo y e (remove x m). + Proof. intros m x y e; exact (@Raw.remove_2 elt _ x y e m.(is_bst) m.(is_avl)). Qed. + Lemma remove_3 : forall m x y e, MapsTo y e (remove x m) -> MapsTo y e m. + Proof. intros m x y e; exact (@Raw.remove_3 elt _ x y e m.(is_bst) m.(is_avl)). Qed. + + + Lemma find_1 : forall m x e, MapsTo x e m -> find x m = Some e. + Proof. intros m x e; exact (@Raw.find_1 elt _ x e m.(is_bst)). Qed. + Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m. + Proof. intros m; exact (@Raw.find_2 elt m.(this)). Qed. + + Lemma fold_1 : forall m (A : Set) (i : A) (f : key -> elt -> A -> A), + fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i. + Proof. intros m; exact (@Raw.fold_1 elt m.(this) m.(is_bst)). Qed. + + Lemma elements_1 : forall m x e, + MapsTo x e m -> InA eq_key_elt (x,e) (elements m). + Proof. + intros; unfold elements, MapsTo, eq_key_elt; rewrite Raw.elements_mapsto; auto. + Qed. + + Lemma elements_2 : forall m x e, + InA eq_key_elt (x,e) (elements m) -> MapsTo x e m. + Proof. + intros; unfold elements, MapsTo, eq_key_elt; rewrite <- Raw.elements_mapsto; auto. + Qed. + + Lemma elements_3 : forall m, sort lt_key (elements m). + Proof. intros m; exact (@Raw.elements_sort elt m.(this) m.(is_bst)). Qed. + + Definition Equal cmp m m' := + (forall k, In k m <-> In k m') /\ + (forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true). + + Lemma Equal_Equal : forall cmp m m', Equal cmp m m' <-> Raw.Equal cmp m m'. + Proof. + intros; unfold Equal, Raw.Equal, In; intuition. + generalize (H0 k); do 2 rewrite Raw.In_alt; intuition. + generalize (H0 k); do 2 rewrite Raw.In_alt; intuition. + generalize (H0 k); do 2 rewrite <- Raw.In_alt; intuition. + generalize (H0 k); do 2 rewrite <- Raw.In_alt; intuition. + Qed. + + Lemma equal_1 : forall m m' cmp, + Equal cmp m m' -> equal cmp m m' = true. + Proof. + unfold equal; intros m m' cmp; rewrite Equal_Equal. + destruct (@Raw.equal _ cmp m m'); auto. + Qed. + + Lemma equal_2 : forall m m' cmp, + equal cmp m m' = true -> Equal cmp m m'. + Proof. + unfold equal; intros; rewrite Equal_Equal. + destruct (@Raw.equal _ cmp m m'); auto; try discriminate. + Qed. + + End Elt. + + Lemma map_1 : forall (elt elt':Set)(m: t elt)(x:key)(e:elt)(f:elt->elt'), + MapsTo x e m -> MapsTo x (f e) (map f m). + Proof. intros elt elt' m x e f; exact (@Raw.map_1 elt elt' f m.(this) x e). Qed. + + Lemma map_2 : forall (elt elt':Set)(m:t elt)(x:key)(f:elt->elt'), In x (map f m) -> In x m. + Proof. + intros elt elt' m x f; do 2 unfold In in *; do 2 rewrite Raw.In_alt; simpl. + apply Raw.map_2; auto. + Qed. + + Lemma mapi_1 : forall (elt elt':Set)(m: t elt)(x:key)(e:elt) + (f:key->elt->elt'), MapsTo x e m -> + exists y, E.eq y x /\ MapsTo x (f y e) (mapi f m). + Proof. intros elt elt' m x e f; exact (@Raw.mapi_1 elt elt' f m.(this) x e). Qed. + Lemma mapi_2 : forall (elt elt':Set)(m: t elt)(x:key) + (f:key->elt->elt'), In x (mapi f m) -> In x m. + Proof. + intros elt elt' m x f; unfold In in *; do 2 rewrite Raw.In_alt; simpl; apply Raw.mapi_2; auto. + Qed. + + Lemma map2_1 : forall (elt elt' elt'':Set)(m: t elt)(m': t elt') + (x:key)(f:option elt->option elt'->option elt''), + In x m \/ In x m' -> + find x (map2 f m m') = f (find x m) (find x m'). + Proof. + unfold find, map2, In; intros elt elt' elt'' m m' x f. + do 2 rewrite Raw.In_alt; intros; simpl; apply Raw.map2_1; auto. + apply m.(is_bst). + apply m'.(is_bst). + Qed. + + Lemma map2_2 : forall (elt elt' elt'':Set)(m: t elt)(m': t elt') + (x:key)(f:option elt->option elt'->option elt''), + In x (map2 f m m') -> In x m \/ In x m'. + Proof. + unfold In, map2; intros elt elt' elt'' m m' x f. + do 3 rewrite Raw.In_alt; intros; simpl in *; eapply Raw.map2_2; eauto. + apply m.(is_bst). + apply m'.(is_bst). + Qed. + +End IntMake. + + +Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: + Sord with Module Data := D + with Module MapS.E := X. + + Module Data := D. + Module MapS := IntMake(I)(X). + Import MapS. + + Module MD := OrderedTypeFacts(D). + Import MD. + + Module LO := FMapList.Make_ord(X)(D). + + Definition t := MapS.t D.t. + + Definition cmp e e' := match D.compare e e' with EQ _ => true | _ => false end. + + Definition elements (m:t) := + LO.MapS.Build_slist (Raw.elements_sort m.(is_bst)). + + Definition eq : t -> t -> Prop := + fun m1 m2 => LO.eq (elements m1) (elements m2). + + Definition lt : t -> t -> Prop := + fun m1 m2 => LO.lt (elements m1) (elements m2). + + Lemma eq_1 : forall m m', Equal cmp m m' -> eq m m'. + Proof. + intros m m'. + unfold eq. + rewrite Equal_Equal. + rewrite Raw.Equal_elements. + intros. + apply LO.eq_1. + auto. + Qed. + + Lemma eq_2 : forall m m', eq m m' -> Equal cmp m m'. + Proof. + intros m m'. + unfold eq. + rewrite Equal_Equal. + rewrite Raw.Equal_elements. + intros. + generalize (LO.eq_2 H). + auto. + Qed. + + Lemma eq_refl : forall m : t, eq m m. + Proof. + unfold eq; intros; apply LO.eq_refl. + Qed. + + Lemma eq_sym : forall m1 m2 : t, eq m1 m2 -> eq m2 m1. + Proof. + unfold eq; intros; apply LO.eq_sym; auto. + Qed. + + Lemma eq_trans : forall m1 m2 m3 : t, eq m1 m2 -> eq m2 m3 -> eq m1 m3. + Proof. + unfold eq; intros; eapply LO.eq_trans; eauto. + Qed. + + Lemma lt_trans : forall m1 m2 m3 : t, lt m1 m2 -> lt m2 m3 -> lt m1 m3. + Proof. + unfold lt; intros; eapply LO.lt_trans; eauto. + Qed. + + Lemma lt_not_eq : forall m1 m2 : t, lt m1 m2 -> ~ eq m1 m2. + Proof. + unfold lt, eq; intros; apply LO.lt_not_eq; auto. + Qed. + + Import Raw. + + Definition flatten_slist (e:enumeration D.t)(He:sorted_e e) := + LO.MapS.Build_slist (sorted_flatten_e He). + + Open Scope Z_scope. + + Definition compare_aux : + forall (e1 e2:enumeration D.t)(He1:sorted_e e1)(He2: sorted_e e2), + Compare LO.lt LO.eq (flatten_slist He1) (flatten_slist He2). + Proof. + intros e1 e2; pattern e1, e2 in |- *; apply compare_rec2. + simple destruct x; simple destruct x'; intuition. + (* x = x' = End *) + constructor 2. + compute; auto. + (* x = End x' = More *) + constructor 1. + compute; auto. + (* x = More x' = End *) + constructor 3. + compute; auto. + (* x = More k t0 t1 e, x' = More k0 t2 t3 e0 *) + case (X.compare k k0); intro. + (* k < k0 *) + constructor 1. + compute; MX.elim_comp; auto. + (* k = k0 *) + destruct (D.compare t t1). + constructor 1. + compute; MX.elim_comp; auto. + destruct (@cons _ t0 e) as [c1 (H2,(H3,H4))]; try inversion_clear He1; auto. + destruct (@cons _ t2 e0) as [c2 (H5,(H6,H7))]; try inversion_clear He2; auto. + assert (measure_e c1 + measure_e c2 < + measure_e (More k t t0 e) + + measure_e (More k0 t1 t2 e0)). + unfold measure_e in *; fold measure_e in *; omega. + destruct (H c1 c2 H0 H2 H5); clear H. + constructor 1. + unfold flatten_slist, LO.lt in *; simpl; simpl in l. + MX.elim_comp. + right; split; auto. + rewrite <- H7; rewrite <- H4; auto. + constructor 2. + unfold flatten_slist, LO.eq in *; simpl; simpl in e5. + MX.elim_comp. + split; auto. + rewrite <- H7; rewrite <- H4; auto. + constructor 3. + unfold flatten_slist, LO.lt in *; simpl; simpl in l. + MX.elim_comp. + right; split; auto. + rewrite <- H7; rewrite <- H4; auto. + constructor 3. + compute; MX.elim_comp; auto. + (* k > k0 *) + constructor 3. + compute; MX.elim_comp; auto. + Qed. + + Definition compare : forall m1 m2, Compare lt eq m1 m2. + Proof. + intros (m1,m1_bst,m1_avl) (m2,m2_bst,m2_avl); simpl. + destruct (@cons _ m1 (End _)) as [x1 (H1,H11)]; auto. + apply SortedEEnd. + inversion_clear 2. + destruct (@cons _ m2 (End _)) as [x2 (H2,H22)]; auto. + apply SortedEEnd. + inversion_clear 2. + simpl in H11; rewrite <- app_nil_end in H11. + simpl in H22; rewrite <- app_nil_end in H22. + destruct (compare_aux H1 H2); intuition. + constructor 1. + unfold lt, LO.lt, IntMake_ord.elements, flatten_slist in *; simpl in *. + rewrite <- H0; rewrite <- H4; auto. + constructor 2. + unfold eq, LO.eq, IntMake_ord.elements, flatten_slist in *; simpl in *. + rewrite <- H0; rewrite <- H4; auto. + constructor 3. + unfold lt, LO.lt, IntMake_ord.elements, flatten_slist in *; simpl in *. + rewrite <- H0; rewrite <- H4; auto. + Qed. + +End IntMake_ord. + +(* 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). + +Module Make_ord (X: OrderedType)(D: OrderedType) + <: Sord with Module Data := D + with Module MapS.E := X + :=IntMake_ord(Z_as_Int)(X)(D). |