diff options
Diffstat (limited to 'theories/FSets/FMapAVL.v')
| -rw-r--r-- | theories/FSets/FMapAVL.v | 2773 |
1 files changed, 1455 insertions, 1318 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 4807ed66..8cb1236e 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -9,35 +9,35 @@ (* Finite map library. *) -(* $Id: FMapAVL.v 9862 2007-05-25 16:57:06Z letouzey $ *) +(* $Id: FMapAVL.v 11033 2008-06-01 22:56:50Z letouzey $ *) -(** This module implements map using AVL trees. - It follows the implementation from Ocaml's standard library. *) +(** * FMapAVL *) -Require Import FSetInterface. -Require Import FMapInterface. -Require Import FMapList. +(** This module implements maps using AVL trees. + It follows the implementation from Ocaml's standard library. + + See the comments at the beginning of FSetAVL for more details. +*) -Require Import ZArith. -Require Import Int. +Require Import FMapInterface FMapList ZArith Int. -Set Firstorder Depth 3. Set Implicit Arguments. Unset Strict Implicit. +(** Notations and helper lemma about pairs *) -Module Raw (I:Int)(X: OrderedType). -Import I. -Module II:=MoreInt(I). -Import II. -Open Local Scope Int_scope. +Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope. +Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope. -Module E := X. -Module MX := OrderedTypeFacts X. -Module PX := KeyOrderedType X. -Module L := FMapList.Raw X. -Import MX. -Import PX. +(** * The Raw functor + + Functor of pure functions + separate proofs of invariant + preservation *) + +Module Raw (Import I:Int)(X: OrderedType). +Open Local Scope pair_scope. +Open Local Scope lazy_bool_scope. +Open Local Scope Int_scope. Definition key := X.t. @@ -45,30 +45,391 @@ Definition key := X.t. Section Elt. -Variable elt : Set. +Variable elt : Type. -(* 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'). -*) +(** * Trees -Notation eqk := (eqk (elt:= elt)). -Notation eqke := (eqke (elt:= elt)). -Notation ltk := (ltk (elt:= elt)). + The fifth field of [Node] is the height of the tree *) -Inductive tree : Set := +Inductive tree := | Leaf : tree | Node : tree -> key -> elt -> tree -> int -> tree. Notation t := tree. -(** The Sixth field of [Node] is the height of the tree *) +(** * Basic functions on trees: height and cardinal *) + +Definition height (m : t) : int := + match m with + | Leaf => 0 + | Node _ _ _ _ h => h + end. + +Fixpoint cardinal (m : t) : nat := + match m with + | Leaf => 0%nat + | Node l _ _ r _ => S (cardinal l + cardinal r) + end. + +(** * Empty Map *) + +Definition empty := Leaf. + +(** * Emptyness test *) + +Definition is_empty m := match m with Leaf => true | _ => false end. + +(** * Appartness *) + +(** The [mem] function is deciding appartness. It exploits the [bst] property + to achieve logarithmic complexity. *) + +Fixpoint mem x m : bool := + match m with + | Leaf => false + | Node l y _ r _ => match X.compare x y with + | LT _ => mem x l + | EQ _ => true + | GT _ => mem x r + end + end. + +Fixpoint find x m : option elt := + match m with + | Leaf => None + | Node l y d r _ => match X.compare x y with + | LT _ => find x l + | EQ _ => Some d + | GT _ => find x r + end + end. + +(** * Helper functions *) -(** * Occurrence in a tree *) +(** [create l x r] creates a node, assuming [l] and [r] + to be balanced and [|height l - height r| <= 2]. *) -Inductive MapsTo (x : key)(e : elt) : tree -> Prop := +Definition create l x e r := + Node l x e r (max (height l) (height r) + 1). + +(** [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 assert_false := create. + +Fixpoint bal l x d 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 l x d r + | Node ll lx ld lr _ => + if ge_lt_dec (height ll) (height lr) then + create ll lx ld (create lr x d r) + else + match lr with + | Leaf => assert_false l x d r + | Node lrl lrx lrd lrr _ => + create (create ll lx ld lrl) lrx lrd (create lrr x d r) + end + end + else + if gt_le_dec hr (hl+2) then + match r with + | Leaf => assert_false l x d r + | Node rl rx rd rr _ => + if ge_lt_dec (height rr) (height rl) then + create (create l x d rl) rx rd rr + else + match rl with + | Leaf => assert_false l x d r + | Node rll rlx rld rlr _ => + create (create l x d rll) rlx rld (create rlr rx rd rr) + end + end + else + create l x d r. + +(** * Insertion *) + +Fixpoint add x d m := + match m with + | Leaf => Node Leaf x d Leaf 1 + | Node l y d' r h => + match X.compare x y with + | LT _ => bal (add x d l) y d' r + | EQ _ => Node l y d r h + | GT _ => bal l y d' (add x d r) + end + end. + +(** * 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]). +*) + +Fixpoint remove_min l x d r : t*(key*elt) := + match l with + | Leaf => (r,(x,d)) + | Node ll lx ld lr lh => + let (l',m) := remove_min ll lx ld lr in + (bal l' x d r, m) + end. + +(** * 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]. +*) + +Fixpoint merge s1 s2 := match s1,s2 with + | Leaf, _ => s2 + | _, Leaf => s1 + | _, Node l2 x2 d2 r2 h2 => + match remove_min l2 x2 d2 r2 with + (s2',(x,d)) => bal s1 x d s2' + end +end. + +(** * Deletion *) + +Fixpoint remove x m := match m with + | Leaf => Leaf + | Node l y d r h => + match X.compare x y with + | LT _ => bal (remove x l) y d r + | EQ _ => merge l r + | GT _ => bal l y d (remove x r) + end + end. + +(** * join + + Same as [bal] but does not assume anything regarding heights of [l] + and [r]. +*) + +Fixpoint join l : key -> elt -> t -> t := + match l with + | Leaf => add + | Node ll lx ld lr lh => fun x d => + fix join_aux (r:t) : t := match r with + | Leaf => add x d l + | Node rl rx rd rr rh => + if gt_le_dec lh (rh+2) then bal ll lx ld (join lr x d r) + else if gt_le_dec rh (lh+2) then bal (join_aux rl) rx rd rr + else create l x d r + end + end. + +(** * Splitting + + [split x m] returns a triple [(l, o, r)] where + - [l] is the set of elements of [m] that are [< x] + - [r] is the set of elements of [m] that are [> x] + - [o] is the result of [find x m]. +*) + +Record triple := mktriple { t_left:t; t_opt:option elt; t_right:t }. +Notation "<< l , b , r >>" := (mktriple l b r) (at level 9). + +Fixpoint split x m : triple := match m with + | Leaf => << Leaf, None, Leaf >> + | Node l y d r h => + match X.compare x y with + | LT _ => let (ll,o,rl) := split x l in << ll, o, join rl y d r >> + | EQ _ => << l, Some d, r >> + | GT _ => let (rl,o,rr) := split x r in << join l y d rl, o, rr >> + end + end. + +(** * Concatenation + + Same as [merge] but does not assume anything about heights. +*) + +Definition concat m1 m2 := + match m1, m2 with + | Leaf, _ => m2 + | _ , Leaf => m1 + | _, Node l2 x2 d2 r2 _ => + let (m2',xd) := remove_min l2 x2 d2 r2 in + join m1 xd#1 xd#2 m2' + end. + +(** * 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)) m : list (key*elt) := + match m with + | Leaf => acc + | Node l x d r _ => elements_aux ((x,d) :: elements_aux acc r) l + end. + +(** then [elements] is an instanciation with an empty [acc] *) + +Definition elements := elements_aux nil. + +(** * Fold *) + +Fixpoint fold (A : Type) (f : key -> elt -> A -> A) (m : t) : A -> A := + fun a => match m with + | Leaf => a + | Node l x d r _ => fold f r (f x d (fold f l a)) + end. + +(** * Comparison *) + +Variable cmp : elt->elt->bool. + +(** ** Enumeration of the elements of a tree *) + +Inductive enumeration := + | End : enumeration + | More : key -> elt -> t -> enumeration -> enumeration. + +(** [cons m e] adds the elements of tree [m] on the head of + enumeration [e]. *) + +Fixpoint cons m e : enumeration := + match m with + | Leaf => e + | Node l x d r h => cons l (More x d r e) + end. + +(** One step of comparison of elements *) + +Definition equal_more x1 d1 (cont:enumeration->bool) e2 := + match e2 with + | End => false + | More x2 d2 r2 e2 => + match X.compare x1 x2 with + | EQ _ => cmp d1 d2 &&& cont (cons r2 e2) + | _ => false + end + end. + +(** Comparison of left tree, middle element, then right tree *) + +Fixpoint equal_cont m1 (cont:enumeration->bool) e2 := + match m1 with + | Leaf => cont e2 + | Node l1 x1 d1 r1 _ => + equal_cont l1 (equal_more x1 d1 (equal_cont r1 cont)) e2 + end. + +(** Initial continuation *) + +Definition equal_end e2 := match e2 with End => true | _ => false end. + +(** The complete comparison *) + +Definition equal m1 m2 := equal_cont m1 equal_end (cons m2 End). + +End Elt. +Notation t := tree. +Notation "<< l , b , r >>" := (mktriple l b r) (at level 9). +Notation "t #l" := (t_left t) (at level 9, format "t '#l'"). +Notation "t #o" := (t_opt t) (at level 9, format "t '#o'"). +Notation "t #r" := (t_right t) (at level 9, format "t '#r'"). + + +(** * Map *) + +Fixpoint map (elt elt' : Type)(f : elt -> elt')(m : t elt) : t elt' := + match m with + | Leaf => Leaf _ + | Node l x d r h => Node (map f l) x (f d) (map f r) h + end. + +(* * Mapi *) + +Fixpoint mapi (elt elt' : Type)(f : key -> elt -> elt')(m : t elt) : t elt' := + match m with + | Leaf => Leaf _ + | Node l x d r h => Node (mapi f l) x (f x d) (mapi f r) h + end. + +(** * Map with removal *) + +Fixpoint map_option (elt elt' : Type)(f : key -> elt -> option elt')(m : t elt) + : t elt' := + match m with + | Leaf => Leaf _ + | Node l x d r h => + match f x d with + | Some d' => join (map_option f l) x d' (map_option f r) + | None => concat (map_option f l) (map_option f r) + end + end. + +(** * Optimized map2 + + Suggestion by B. Gregoire: a [map2] function with specialized + arguments allowing to bypass some tree traversal. Instead of one + [f0] of type [key -> option elt -> option elt' -> option elt''], + we ask here for: + - [f] which is a specialisation of [f0] when first option isn't [None] + - [mapl] treats a [tree elt] with [f0] when second option is [None] + - [mapr] treats a [tree elt'] with [f0] when first option is [None] + + The idea is that [mapl] and [mapr] can be instantaneous (e.g. + the identity or some constant function). +*) + +Section Map2_opt. +Variable elt elt' elt'' : Type. +Variable f : key -> elt -> option elt' -> option elt''. +Variable mapl : t elt -> t elt''. +Variable mapr : t elt' -> t elt''. + +Fixpoint map2_opt m1 m2 := + match m1, m2 with + | Leaf, _ => mapr m2 + | _, Leaf => mapl m1 + | Node l1 x1 d1 r1 h1, _ => + let (l2',o2,r2') := split x1 m2 in + match f x1 d1 o2 with + | Some e => join (map2_opt l1 l2') x1 e (map2_opt r1 r2') + | None => concat (map2_opt l1 l2') (map2_opt r1 r2') + end + end. + +End Map2_opt. + +(** * Map2 + + The [map2] function of the Map interface can be implemented + via [map2_opt] and [map_option]. +*) + +Section Map2. +Variable elt elt' elt'' : Type. +Variable f : option elt -> option elt' -> option elt''. + +Definition map2 : t elt -> t elt' -> t elt'' := + map2_opt + (fun _ d o => f (Some d) o) + (map_option (fun _ d => f (Some d) None)) + (map_option (fun _ d' => f None (Some d'))). + +End Map2. + + + +(** * Invariants *) + +Section Invariants. +Variable elt : Type. + +(** ** Occurrence in a tree *) + +Inductive MapsTo (x : key)(e : elt) : t elt -> 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', @@ -76,7 +437,7 @@ Inductive MapsTo (x : key)(e : elt) : tree -> Prop := | 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 := +Inductive In (x : key) : t elt -> 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', @@ -84,58 +445,66 @@ Inductive In (x : key) : tree -> Prop := | 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. +Definition In0 k m := exists e:elt, MapsTo k e m. -(** * Binary search trees *) +(** ** 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. +Definition lt_tree x m := forall y, In y m -> X.lt y x. +Definition gt_tree x m := forall y, In y m -> 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). +Inductive bst : t elt -> 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 *) +End Invariants. -(** [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. +(** * Correctness proofs, isolated in a sub-module *) -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). +Module Proofs. + Module MX := OrderedTypeFacts X. + Module PX := KeyOrderedType X. + Module L := FMapList.Raw X. -(* We should end this section before the big proofs that follows, - otherwise the discharge takes a lot of time. *) -End Elt. +Functional Scheme mem_ind := Induction for mem Sort Prop. +Functional Scheme find_ind := Induction for find Sort Prop. +Functional Scheme bal_ind := Induction for bal Sort Prop. +Functional Scheme add_ind := Induction for add Sort Prop. +Functional Scheme remove_min_ind := Induction for remove_min Sort Prop. +Functional Scheme merge_ind := Induction for merge Sort Prop. +Functional Scheme remove_ind := Induction for remove Sort Prop. +Functional Scheme concat_ind := Induction for concat Sort Prop. +Functional Scheme split_ind := Induction for split Sort Prop. +Functional Scheme map_option_ind := Induction for map_option Sort Prop. +Functional Scheme map2_opt_ind := Induction for map2_opt Sort Prop. -(** Some helpful hints and tactics. *) +(** * Automation and dedicated tactics. *) -Notation t := tree. -Hint Constructors tree. -Hint Constructors MapsTo. -Hint Constructors In. -Hint Constructors bst. -Hint Constructors avl. +Hint Constructors tree MapsTo In bst. Hint Unfold lt_tree gt_tree. +Tactic Notation "factornode" ident(l) ident(x) ident(d) ident(r) ident(h) + "as" ident(s) := + set (s:=Node l x d r h) in *; clearbody s; clear l x d r h. + +(** 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. + +(** A tactic to repeat [inversion_clear] on all hyps of the + form [(f (Node ...))] *) + Ltac inv f := match goal with | H:f (Leaf _) |- _ => inversion_clear H; inv f @@ -149,14 +518,6 @@ Ltac 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 @@ -166,55 +527,54 @@ Ltac inv_all f := | _ => idtac end. +(** Helper tactic concerning order of elements. *) + 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 + | U: lt_tree _ ?s, V: In _ ?s |- _ => generalize (U _ V); clear U; order + | U: gt_tree _ ?s, V: In _ ?s |- _ => generalize (U _ V); clear U; 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 *) +(* Function/Functional Scheme can't deal with internal fix. + Let's do its job by hand: *) + +Ltac join_tac := + intros l; induction l as [| ll _ lx ld lr Hlr lh]; + [ | intros x d r; induction r as [| rl Hrl rx rd rr _ rh]; unfold join; + [ | destruct (gt_le_dec lh (rh+2)); + [ match goal with |- context [ bal ?u ?v ?w ?z ] => + replace (bal u v w z) + with (bal ll lx ld (join lr x d (Node rl rx rd rr rh))); [ | auto] + end + | destruct (gt_le_dec rh (lh+2)); + [ match goal with |- context [ bal ?u ?v ?w ?z ] => + replace (bal u v w z) + with (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr); [ | auto] + end + | ] ] ] ]; intros. -Ltac avl_nns := - match goal with - | H:avl _ |- _ => avl_nn_hyp H; clear H; avl_nns - | _ => idtac - end. +Section Elt. +Variable elt:Type. +Implicit Types m r : t elt. +(** * Basic results about [MapsTo], [In], [lt_tree], [gt_tree], [height] *) (** Facts about [MapsTo] and [In]. *) -Lemma MapsTo_In : forall elt k e (m:t elt), MapsTo k e m -> In k m. +Lemma MapsTo_In : forall k e m, 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. +Lemma In_MapsTo : forall k m, 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. +Lemma In_alt : forall k m, In0 k m <-> In k m. Proof. split. intros (e,H); eauto. @@ -222,64 +582,70 @@ Proof. Qed. Lemma MapsTo_1 : - forall elt (m:t elt) x y e, X.eq x y -> MapsTo x e m -> MapsTo y e m. + forall m 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. + forall m x y, X.eq x y -> In x m -> In y m. Proof. - intros elt m x y; induction m; simpl; intuition_in; eauto. + intros m x y; induction m; simpl; intuition_in; eauto. Qed. +Lemma In_node_iff : + forall l x e r h y, + In y (Node l x e r h) <-> In y l \/ X.eq y x \/ In y r. +Proof. + intuition_in. +Qed. (** Results about [lt_tree] and [gt_tree] *) -Lemma lt_leaf : forall elt x, lt_tree x (Leaf elt). +Lemma lt_leaf : forall 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). +Lemma gt_leaf : forall 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, +Lemma lt_tree_node : forall x y l 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. + unfold lt_tree in *; intuition_in; order. Qed. -Lemma gt_tree_node : forall elt x y (l:t elt) r e h, +Lemma gt_tree_node : forall x y l 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. + unfold gt_tree in *; intuition_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, +Lemma lt_left : forall x y l 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, +Lemma lt_right : forall x y l 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, +Lemma gt_left : forall x y l 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, +Lemma gt_right : forall x y l r e h, gt_tree x (Node l y e r h) -> gt_tree x r. Proof. intuition_in. @@ -288,731 +654,639 @@ 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. + forall x m, lt_tree x m -> ~ In x m. 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. + forall x y, X.lt x y -> forall m, lt_tree x m -> lt_tree y m. Proof. - firstorder eauto. + eauto. Qed. Lemma gt_tree_not_in : - forall elt x (t : t elt), gt_tree x t -> ~ In x t. + forall x m, gt_tree x m -> ~ In x m. 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. + forall x y, X.lt y x -> forall m, gt_tree x m -> gt_tree y m. Proof. - firstorder eauto. + eauto. Qed. Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans. -(** Results about [avl] *) +(** * Empty map *) -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)). +Definition Empty m := forall (a:key)(e:elt) , ~ MapsTo a e m. + +Lemma empty_bst : bst (empty elt). Proof. - intros; auto. + unfold empty; 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]. *) +Lemma empty_1 : Empty (empty elt). +Proof. + unfold empty, Empty; intuition_in. +Qed. -Definition create elt (l:t elt) x e r := - Node l x e r (max (height l) (height r) + 1). +(** * Emptyness test *) -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). +Lemma is_empty_1 : forall m, Empty m -> is_empty m = true. Proof. - unfold create; auto. + destruct m as [|r x e l h]; simpl; auto. + intro H; elim (H x e); 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. +Lemma is_empty_2 : forall m, is_empty m = true -> Empty m. +Proof. + destruct m; simpl; intros; try discriminate; red; intuition_in. 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. +(** * Appartness *) + +Lemma mem_1 : forall m x, bst m -> In x m -> mem x m = true. +Proof. + intros m x; functional induction (mem x m); auto; intros; clearf; + inv bst; intuition_in; order. 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. +Lemma mem_2 : forall m x, mem x m = true -> In x m. +Proof. + intros m x; functional induction (mem x m); auto; intros; discriminate. Qed. -(** trick for emulating [assert false] in Coq *) +Lemma find_1 : forall m x e, bst m -> MapsTo x e m -> find x m = Some e. +Proof. + intros m x; functional induction (find x m); auto; intros; clearf; + inv bst; intuition_in; simpl; auto; + try solve [order | absurd (X.lt x y); eauto | absurd (X.lt y x); eauto]. +Qed. -Notation assert_false := Leaf. +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; intros; clearf; + try discriminate. + constructor 2; auto. + inversion H; auto. + constructor 3; auto. +Qed. -(** [bal l x e r] acts as [create], but performs one step of - rebalancing if necessary, i.e. assumes [|height l - height r| <= 3]. *) +Lemma find_iff : forall m x e, bst m -> + (find x m = Some e <-> MapsTo x e m). +Proof. + split; auto using find_1, find_2. +Qed. -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 find_in : forall m x, find x m <> None -> In x m. +Proof. + intros. + case_eq (find x m); [intros|congruence]. + apply MapsTo_In with e; apply find_2; auto. +Qed. -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). +Lemma in_find : forall m x, bst m -> In x m -> find x m <> None. 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. + intros. + destruct (In_MapsTo H0) as (d,Hd). + rewrite (find_1 H Hd); discriminate. 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). +Lemma find_in_iff : forall m x, bst m -> + (find x m <> None <-> In x m). Proof. - bal_tac; inv avl; repeat apply create_avl; simpl in *; auto; omega_max. + split; auto using find_in, in_find. 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. +Lemma not_find_iff : forall m x, bst m -> + (find x m = None <-> ~In x m). Proof. - bal_tac; inv avl; avl_nns; simpl in *; omega_max. + split; intros. + red; intros. + elim (in_find H H1 H0). + case_eq (find x m); [ intros | auto ]. + elim H0; apply find_in; congruence. 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. +Lemma find_find : forall m m' x, + find x m = find x m' <-> + (forall d, find x m = Some d <-> find x m' = Some d). Proof. - bal_tac; inv avl; simpl in *; omega_max. + intros; destruct (find x m); destruct (find x m'); split; intros; + try split; try congruence. + rewrite H; auto. + symmetry; rewrite <- H; auto. + rewrite H; auto. 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). +Lemma find_mapsto_equiv : forall m m' x, bst m -> bst m' -> + (find x m = find x m' <-> + (forall d, MapsTo x d m <-> MapsTo x d m')). Proof. - bal_tac; bal_tac_imp; repeat rewrite create_in; intuition_in. + intros m m' x Hm Hm'. + rewrite find_find. + split; intros H d; specialize H with d. + rewrite <- 2 find_iff; auto. + rewrite 2 find_iff; auto. 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)). +Lemma find_in_equiv : forall m m' x, bst m -> bst m' -> + find x m = find x m' -> + (In x m <-> In x m'). Proof. - bal_tac; bal_tac_imp; unfold create; intuition_in. + split; intros; apply find_in; [ rewrite <- H1 | rewrite H1 ]; + apply in_find; auto. 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. +(** * Helper functions *) -(** * Insertion *) +Lemma create_bst : + forall l 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. -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 create_in : + forall l 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. -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. +Lemma bal_bst : forall l x e r, bst l -> bst r -> + lt_tree x l -> gt_tree x r -> bst (bal l x e r). +Proof. + intros l x e r; functional induction (bal l x e r); intros; clearf; + inv bst; repeat apply create_bst; auto; unfold create; try constructor; + (apply lt_tree_node || apply gt_tree_node); auto; + (eapply lt_tree_trans || eapply gt_tree_trans); eauto. Qed. +Hint Resolve bal_bst. -Lemma add_avl : forall elt (m:t elt) x e, avl m -> avl (add x e m). +Lemma bal_in : forall l x e r y, + In y (bal l x e r) <-> X.eq y x \/ In y l \/ In y r. Proof. - intros; generalize (add_avl_1 x e H); intuition. + intros l x e r; functional induction (bal l x e r); intros; clearf; + rewrite !create_in; intuition_in. 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). +Lemma bal_mapsto : forall l x e r y e', + MapsTo y e' (bal l x e r) <-> MapsTo y e' (create l x e r). 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 H0); intuition_in. - (* EQ *) - inv avl. - firstorder_in. - eapply In_1; eauto. - (* GT *) - inv avl. - rewrite bal_in; auto. - rewrite (IHt H1); intuition_in. + intros l x e r; functional induction (bal l x e r); intros; clearf; + unfold assert_false, create; 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 H0. - intuition. - eauto. - (* gt_tree -> gt_tree (add ...) *) - red; red in H4. - intros. - rewrite (add_in x y0 e H5) in H0. - intuition. - apply lt_eq with x; auto. +Lemma bal_find : forall l x e r y, + bst l -> bst r -> lt_tree x l -> gt_tree x r -> + find y (bal l x e r) = find y (create l x e r). +Proof. + intros; rewrite find_mapsto_equiv; auto; intros; apply bal_mapsto. 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). +(** * Insertion *) + +Lemma add_in : forall m x y e, + In y (add x e m) <-> X.eq y x \/ In y m. +Proof. + intros m x y e; functional induction (add x e m); auto; intros; + try (rewrite bal_in, IHt); intuition_in. + apply In_1 with x; auto. +Qed. + +Lemma add_bst : forall m x e, bst m -> bst (add x e m). +Proof. + intros m x e; functional induction (add x e m); intros; + inv bst; try apply bal_bst; auto; + intro z; rewrite add_in; intuition. + apply MX.eq_lt with x; auto. + apply MX.lt_eq with x; auto. +Qed. +Hint Resolve add_bst. + +Lemma add_1 : forall m x y e, 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. + intros m x y e; functional induction (add x e m); + intros; inv bst; 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 -> +Lemma add_2 : forall m x y e e', ~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. + intros 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; + intros; inv bst; 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 -> +Lemma add_3 : forall m x y e e', ~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; + intros m x y e e'; induction m; simpl; auto. + intros; inv MapsTo; auto; order. + destruct (X.compare x k); intro; try rewrite bal_mapsto; auto; unfold create; intros; inv MapsTo; auto; - order. + 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. +Lemma add_find : forall m x y e, bst m -> + find y (add x e m) = + match X.compare y x with EQ _ => Some e | _ => find y m end. 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 e1. simpl in *. - apply bal_avl; subst;auto; omega_max. - rewrite_all e1;simpl in *;omega_bal. + intros. + assert (~X.eq x y -> find y (add x e m) = find y m). + intros; rewrite find_mapsto_equiv; auto. + split; eauto using add_2, add_3. + destruct X.compare; try (apply H0; order). + auto using find_1, add_1. 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. +(** * Extraction of minimum binding *) -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))). +Lemma remove_min_in : forall l x e r h y, + In y (Node l x e r h) <-> + X.eq y (remove_min l x e r)#2#1 \/ In y (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. + intros 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 H0). - - rewrite_all e1; simpl; intros. - rewrite bal_in; auto. - generalize (IHp lh y H0). - intuition. - inversion_clear H7; intuition. + rewrite e0 in *; simpl; intros. + rewrite bal_in, In_node_iff, IHp; 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)))). +Lemma remove_min_mapsto : forall l x e r h y e', + MapsTo y e' (Node l x e r h) <-> + ((X.eq y (remove_min l x e r)#2#1) /\ e' = (remove_min l x e r)#2#2) + \/ MapsTo y e' (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. + intros 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 H0). - rewrite_all e1; simpl; intros. + rewrite e0 in *; simpl; intros. rewrite bal_mapsto; auto; unfold create. - simpl in *;destruct (IHp lh y e'). - auto. + simpl in *;destruct (IHp _x y e'). intuition. - inversion_clear H2; intuition. - inversion_clear H9; intuition. + inversion_clear H1; intuition. + inversion_clear H3; 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)). +Lemma remove_min_bst : forall l x e r h, + bst (Node l x e r h) -> bst (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. + intros l x e r; functional induction (remove_min l x e r); simpl in *; intros. inv bst; auto. inversion_clear H; inversion_clear H0. apply bal_bst; auto. - rewrite_all e1;simpl in *;firstorder. + rewrite e0 in *; simpl in *; apply (IHp _x); auto. intro; intros. - generalize (remove_min_in y H). - rewrite_all e1; simpl in *. + generalize (remove_min_in ll lx ld lr _x y). + rewrite e0; simpl in *. destruct 1. - apply H3; intuition. + apply H2; intuition. Qed. +Hint Resolve remove_min_bst. -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)). +Lemma remove_min_gt_tree : forall l x e r h, + bst (Node l x e r h) -> + gt_tree (remove_min l x e r)#2#1 (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. + intros l x e r; functional induction (remove_min l x e r); simpl in *; intros. inv bst; auto. - inversion_clear H; inversion_clear H0. + inversion_clear H. intro; intro. - rewrite_all e1;simpl in *. - generalize (IHp lh H1 H); clear H7 H6 IHp. - generalize (remove_min_avl H). - generalize (remove_min_in (fst m) H). - rewrite e1; simpl; intros. - rewrite (bal_in x e y H7 H5) in H0. - destruct H6. - 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 y. - split; auto; avl_nns; simpl in *; omega_max. - destruct s1;try contradiction;clear y. - generalize (remove_min_avl_1 H0). - rewrite e3; simpl;destruct 1. - split. - apply bal_avl; auto. - simpl; omega_max. - omega_bal. + rewrite e0 in *;simpl in *. + generalize (IHp _x H0). + generalize (remove_min_in ll lx ld lr _x m#1). + rewrite e0; simpl; intros. + rewrite (bal_in l' x d r y) in H. + assert (In m#1 (Node ll lx ld lr _x)) by (rewrite H4; auto); clear H4. + assert (X.lt m#1 x) by order. + decompose [or] H; order. +Qed. +Hint Resolve remove_min_gt_tree. + +Lemma remove_min_find : forall l x e r h y, + bst (Node l x e r h) -> + find y (Node l x e r h) = + match X.compare y (remove_min l x e r)#2#1 with + | LT _ => None + | EQ _ => Some (remove_min l x e r)#2#2 + | GT _ => find y (remove_min l x e r)#1 + end. +Proof. + intros. + destruct X.compare. + rewrite not_find_iff; auto. + rewrite remove_min_in; red; destruct 1 as [H'|H']; [ order | ]. + generalize (remove_min_gt_tree H H'); order. + apply find_1; auto. + rewrite remove_min_mapsto; auto. + rewrite find_mapsto_equiv; eauto; intros. + rewrite remove_min_mapsto; intuition; order. 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. +(** * Merging two trees *) -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). +Lemma merge_in : forall m1 m2 y, bst m1 -> bst m2 -> + (In y (merge m1 m2) <-> In y m1 \/ In y m2). Proof. - intros elt s1 s2; functional induction (merge s1 s2);intros. + intros m1 m2; functional induction (merge m1 m2);intros; + try factornode _x _x0 _x1 _x2 _x3 as m1. intuition_in. intuition_in. - destruct s1;try contradiction;clear y. -(* 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 e3; auto]. - rewrite bal_in; auto. - generalize (remove_min_avl H2); rewrite e3; simpl; auto. - generalize (remove_min_in y0 H2); rewrite e3; simpl; intro. - rewrite H3; intuition. + rewrite bal_in, remove_min_in, e1; simpl; 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). +Lemma merge_mapsto : forall m1 m2 y e, bst m1 -> bst m2 -> + (MapsTo y e (merge m1 m2) <-> MapsTo y e m1 \/ MapsTo y e m2). Proof. - intros elt s1 s2; functional induction (@merge elt s1 s2); intros. + intros m1 m2; functional induction (merge m1 m2); intros; + try factornode _x _x0 _x1 _x2 _x3 as m1. intuition_in. intuition_in. - destruct s1;try contradiction;clear y. - replace s2' with (fst (remove_min l2 x2 e2 r2)); [|rewrite e3; auto]. - rewrite bal_mapsto; auto; unfold create. - generalize (remove_min_avl H2); rewrite e3; simpl; auto. - generalize (remove_min_mapsto y0 e H2); rewrite e3; simpl; intro. - rewrite H3; intuition (try subst; auto). - inversion_clear H3; intuition. + rewrite bal_mapsto, remove_min_mapsto, e1; simpl; auto. + unfold create. + intuition; 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). +Lemma merge_bst : forall m1 m2, bst m1 -> bst m2 -> + (forall y1 y2 : key, In y1 m1 -> In y2 m2 -> X.lt y1 y2) -> + bst (merge m1 m2). Proof. - intros elt s1 s2; functional induction (@merge elt s1 s2); intros; auto. - + intros m1 m2; functional induction (merge m1 m2); intros; auto; + try factornode _x _x0 _x1 _x2 _x3 as m1. apply bal_bst; auto. - destruct s1;try contradiction. - generalize (remove_min_bst H1); rewrite e3; simpl in *; auto. - destruct s1;try contradiction. + generalize (remove_min_bst H0); rewrite e1; simpl in *; auto. intro; intro. - apply H3; auto. - generalize (remove_min_in x H2); rewrite e3; simpl; intuition. - destruct s1;try contradiction. - generalize (remove_min_gt_tree H1); rewrite e3; 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 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. + apply H1; auto. + generalize (remove_min_in l2 x2 d2 r2 _x4 x); rewrite e1; simpl; intuition. + generalize (remove_min_gt_tree H0); rewrite e1; simpl; auto. 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. +(** * Deletion *) -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). +Lemma remove_in : forall m x y, bst m -> + (In y (remove x m) <-> ~ X.eq y x /\ In y m). Proof. - intros elt s x; functional induction (@remove elt x s); simpl; intros. + intros m x; functional induction (remove x m); simpl; intros. intuition_in. (* LT *) - inv avl; inv bst; clear e1. + inv bst; clear e0. rewrite bal_in; auto. generalize (IHt y0 H0); intuition; [ order | order | intuition_in ]. (* EQ *) - inv avl; inv bst; clear e1. + inv bst; clear e0. rewrite merge_in; intuition; [ order | order | intuition_in ]. - elim H9; eauto. + elim H4; eauto. (* GT *) - inv avl; inv bst; clear e1. + inv bst; clear e0. rewrite bal_in; auto. - generalize (IHt y0 H5); intuition; [ order | order | intuition_in ]. + generalize (IHt y0 H1); intuition; [ order | order | intuition_in ]. Qed. -Lemma remove_bst : forall elt (s:t elt) x, bst s -> avl s -> bst (remove x s). +Lemma remove_bst : forall m x, bst m -> bst (remove x m). Proof. - intros elt s x; functional induction (@remove elt x s); simpl; intros. + intros m x; functional induction (remove x m); simpl; intros. auto. (* LT *) - inv avl; inv bst. + inv bst. apply bal_bst; auto. intro; intro. rewrite (remove_in x y0 H0) in H; auto. destruct H; eauto. (* EQ *) - inv avl; inv bst. + inv bst. apply merge_bst; eauto. (* GT *) - inv avl; inv bst. + inv bst. apply bal_bst; auto. intro; intro. - rewrite (remove_in x y0 H5) in H; auto. + rewrite (remove_in x y0 H1) 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). +Lemma remove_1 : forall m x y, bst m -> X.eq x y -> ~ In y (remove x m). Proof. intros; rewrite remove_in; intuition. -Qed. +Qed. -Lemma remove_2 : forall elt (m:t elt) x y e, bst m -> avl m -> ~X.eq x y -> +Lemma remove_2 : forall m x y e, bst 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. + intros 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; + intros; inv bst; 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 -> +Lemma remove_3 : forall m x y e, bst 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; + intros m x y e; induction m; simpl; auto. + destruct (X.compare x k); intros Bs; inv bst; try rewrite bal_mapsto; auto; unfold create. - intros; inv MapsTo; auto. + intros; inv MapsTo; auto. rewrite merge_mapsto; intuition. intros; inv MapsTo; auto. Qed. -Section Elt2. +(** * join *) -Variable elt:Set. +Lemma join_in : forall l x d r y, + In y (join l x d r) <-> X.eq y x \/ In y l \/ In y r. +Proof. + join_tac. + simpl. + rewrite add_in; intuition_in. + rewrite add_in; intuition_in. + rewrite bal_in, Hlr; clear Hlr Hrl; intuition_in. + rewrite bal_in, Hrl; clear Hlr Hrl; intuition_in. + apply create_in. +Qed. -Notation eqk := (eqk (elt:= elt)). -Notation eqke := (eqke (elt:= elt)). -Notation ltk := (ltk (elt:= elt)). +Lemma join_bst : forall l x d r, bst l -> bst r -> + lt_tree x l -> gt_tree x r -> bst (join l x d r). +Proof. + join_tac; auto; try (simpl; auto; fail); inv bst; apply bal_bst; auto; + clear Hrl Hlr z; intro; intros; rewrite join_in in *. + intuition; [ apply MX.lt_eq with x | ]; eauto. + intuition; [ apply MX.eq_lt with x | ]; eauto. +Qed. +Hint Resolve join_bst. -(** * Empty map *) +Lemma join_find : forall l x d r y, + bst l -> bst r -> lt_tree x l -> gt_tree x r -> + find y (join l x d r) = find y (create l x d r). +Proof. + join_tac; auto; inv bst; + simpl (join (Leaf elt)); + try (assert (X.lt lx x) by auto); + try (assert (X.lt x rx) by auto); + rewrite ?add_find, ?bal_find; auto. -Definition Empty m := forall (a : key)(e:elt) , ~ MapsTo a e m. + simpl; destruct X.compare; auto. + rewrite not_find_iff; auto; intro; order. -Definition empty := (Leaf elt). + simpl; repeat (destruct X.compare; auto); try (order; fail). + rewrite not_find_iff by auto; intro. + assert (X.lt y x) by auto; order. -Lemma empty_bst : bst empty. + simpl; rewrite Hlr; simpl; auto. + repeat (destruct X.compare; auto); order. + intros u Hu; rewrite join_in in Hu. + destruct Hu as [Hu|[Hu|Hu]]; try generalize (H2 _ Hu); order. + + simpl; rewrite Hrl; simpl; auto. + repeat (destruct X.compare; auto); order. + intros u Hu; rewrite join_in in Hu. + destruct Hu as [Hu|[Hu|Hu]]; order. +Qed. + +(** * split *) + +Lemma split_in_1 : forall m x, bst m -> forall y, + (In y (split x m)#l <-> In y m /\ X.lt y x). Proof. - unfold empty; auto. + intros m x; functional induction (split x m); simpl; intros; + inv bst; try clear e0. + intuition_in. + rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order. + intuition_in; order. + rewrite join_in. + rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order. Qed. -Lemma empty_avl : avl empty. +Lemma split_in_2 : forall m x, bst m -> forall y, + (In y (split x m)#r <-> In y m /\ X.lt x y). Proof. - unfold empty; auto. + intros m x; functional induction (split x m); subst; simpl; intros; + inv bst; try clear e0. + intuition_in. + rewrite join_in. + rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order. + intuition_in; order. + rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order. Qed. -Lemma empty_1 : Empty empty. +Lemma split_in_3 : forall m x, bst m -> + (split x m)#o = find x m. Proof. - unfold empty, Empty; intuition_in. + intros m x; functional induction (split x m); subst; simpl; auto; + intros; inv bst; try clear e0; + destruct X.compare; try (order;fail); rewrite <-IHt, e1; auto. Qed. -(** * Emptyness test *) - -Definition is_empty (s:t elt) := match s with Leaf => true | _ => false end. +Lemma split_bst : forall m x, bst m -> + bst (split x m)#l /\ bst (split x m)#r. +Proof. + intros m x; functional induction (split x m); subst; simpl; intros; + inv bst; try clear e0; try rewrite e1 in *; simpl in *; intuition; + apply join_bst; auto. + intros y0. + generalize (split_in_2 x H0 y0); rewrite e1; simpl; intuition. + intros y0. + generalize (split_in_1 x H1 y0); rewrite e1; simpl; intuition. +Qed. -Lemma is_empty_1 : forall s, Empty s -> is_empty s = true. +Lemma split_lt_tree : forall m x, bst m -> lt_tree x (split x m)#l. Proof. - destruct s as [|r x e l h]; simpl; auto. - intro H; elim (H x e); auto. + intros m x B y Hy; rewrite split_in_1 in Hy; intuition. Qed. -Lemma is_empty_2 : forall s, is_empty s = true -> Empty s. -Proof. - destruct s; simpl; intros; try discriminate; red; intuition_in. +Lemma split_gt_tree : forall m x, bst m -> gt_tree x (split x m)#r. +Proof. + intros m x B y Hy; rewrite split_in_2 in Hy; intuition. Qed. -(** * Appartness *) +Lemma split_find : forall m x y, bst m -> + find y m = match X.compare y x with + | LT _ => find y (split x m)#l + | EQ _ => (split x m)#o + | GT _ => find y (split x m)#r + end. +Proof. + intros m x; functional induction (split x m); subst; simpl; intros; + inv bst; try clear e0; try rewrite e1 in *; simpl in *; + [ destruct X.compare; auto | .. ]; + try match goal with E:split ?x ?t = _, B:bst ?t |- _ => + generalize (split_in_1 x B)(split_in_2 x B)(split_bst x B); + rewrite E; simpl; destruct 3 end. -(** The [mem] function is deciding appartness. It exploits the [bst] property - to achieve logarithmic complexity. *) + rewrite join_find, IHt; auto; clear IHt; simpl. + repeat (destruct X.compare; auto); order. + intro y1; rewrite H4; intuition. -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. + repeat (destruct X.compare; auto); order. -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. + rewrite join_find, IHt; auto; clear IHt; simpl. + repeat (destruct X.compare; auto); order. + intros y1; rewrite H; intuition. 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. +(** * Concatenation *) -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. +Lemma concat_in : forall m1 m2 y, + In y (concat m1 m2) <-> In y m1 \/ In y m2. +Proof. + intros m1 m2; functional induction (concat m1 m2); intros; + try factornode _x _x0 _x1 _x2 _x3 as m1. + intuition_in. 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. + rewrite join_in, remove_min_in, e1; simpl; intuition. 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. +Lemma concat_bst : forall m1 m2, bst m1 -> bst m2 -> + (forall y1 y2, In y1 m1 -> In y2 m2 -> X.lt y1 y2) -> + bst (concat m1 m2). +Proof. + intros m1 m2; functional induction (concat m1 m2); intros; auto; + try factornode _x _x0 _x1 _x2 _x3 as m1. + apply join_bst; auto. + change (bst (m2',xd)#1); rewrite <-e1; eauto. + intros y Hy. + apply H1; auto. + rewrite remove_min_in, e1; simpl; auto. + change (gt_tree (m2',xd)#2#1 (m2',xd)#1); rewrite <-e1; eauto. Qed. +Hint Resolve concat_bst. -(** * Elements *) +Lemma concat_find : forall m1 m2 y, bst m1 -> bst m2 -> + (forall y1 y2, In y1 m1 -> In y2 m2 -> X.lt y1 y2) -> + find y (concat m1 m2) = + match find y m2 with Some d => Some d | None => find y m1 end. +Proof. + intros m1 m2; functional induction (concat m1 m2); intros; auto; + try factornode _x _x0 _x1 _x2 _x3 as m1. + simpl; destruct (find y m2); auto. -(** [elements_tree_aux acc t] catenates the elements of [t] in infix - order to the list [acc] *) + generalize (remove_min_find y H0)(remove_min_in l2 x2 d2 r2 _x4) + (remove_min_bst H0)(remove_min_gt_tree H0); + rewrite e1; simpl fst; simpl snd; intros. + + inv bst. + rewrite H2, join_find; auto; clear H2. + simpl; destruct X.compare; simpl; auto. + destruct (find y m2'); auto. + symmetry; rewrite not_find_iff; auto; intro. + apply (MX.lt_not_gt l); apply H1; auto; rewrite H3; auto. -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. + intros z Hz; apply H1; auto; rewrite H3; auto. +Qed. -(** then [elements] is an instanciation with an empty [acc] *) -Definition elements := elements_aux nil. +(** * Elements *) -Lemma elements_aux_mapsto : forall s acc x e, +Notation eqk := (PX.eqk (elt:= elt)). +Notation eqke := (PX.eqke (elt:= elt)). +Notation ltk := (PX.ltk (elt:= elt)). + +Lemma elements_aux_mapsto : forall (s:t elt) 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. @@ -1025,13 +1299,13 @@ Proof. destruct H0; simpl in *; subst; intuition. Qed. -Lemma elements_mapsto : forall s x e, InA eqke (x,e) (elements s) <-> MapsTo x e s. +Lemma elements_mapsto : forall (s:t elt) 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. +Lemma elements_in : forall (s:t elt) x, L.PX.In x (elements s) <-> In x s. Proof. intros. unfold L.PX.In. @@ -1043,7 +1317,7 @@ Proof. unfold L.PX.MapsTo; rewrite elements_mapsto; auto. Qed. -Lemma elements_aux_sort : forall s acc, bst s -> sort ltk acc -> +Lemma elements_aux_sort : forall (s:t elt) 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. @@ -1052,7 +1326,7 @@ Proof. apply Hl; auto. constructor. apply Hr; eauto. - apply (InA_InfA (eqke_refl (elt:=elt))); intros (y',e') H6. + apply (InA_InfA (PX.eqke_refl (elt:=elt))); intros (y',e') H6. destruct (elements_aux_mapsto r acc y' e'); intuition. red; simpl; eauto. red; simpl; eauto. @@ -1070,20 +1344,49 @@ Proof. Qed. Hint Resolve elements_sort. +Lemma elements_nodup : forall s : t elt, bst s -> NoDupA eqk (elements s). +Proof. + intros; apply PX.Sort_NoDupA; auto. +Qed. -(** * Fold *) +Lemma elements_aux_cardinal : + forall (m:t elt) acc, (length acc + cardinal m)%nat = length (elements_aux acc m). +Proof. + simple induction m; simpl; intuition. + rewrite <- H; simpl. + rewrite <- H0; omega. +Qed. -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. +Lemma elements_cardinal : forall (m:t elt), cardinal m = length (elements m). +Proof. + exact (fun m => elements_aux_cardinal m nil). +Qed. -Definition fold' (A : Set) (f : key -> elt -> A -> A)(s : t elt) := +Lemma elements_app : + forall (s:t elt) acc, elements_aux acc s = elements s ++ acc. +Proof. + induction s; simpl; intros; auto. + rewrite IHs1, IHs2. + unfold elements; simpl. + rewrite 2 IHs1, IHs2, <- !app_nil_end, !app_ass; auto. +Qed. + +Lemma elements_node : + forall (t1 t2:t elt) x e z l, + elements t1 ++ (x,e) :: elements t2 ++ l = + elements (Node t1 x e t2 z) ++ l. +Proof. + unfold elements; simpl; intros. + rewrite !elements_app, <- !app_nil_end, !app_ass; auto. +Qed. + +(** * Fold *) + +Definition fold' (A : Type) (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, + forall (A : Type) (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. @@ -1095,7 +1398,7 @@ Proof. Qed. Lemma fold_equiv : - forall (A : Set) (s : t elt) (f : key -> elt -> A -> A) (a : A), + forall (A : Type) (s : t elt) (f : key -> elt -> A -> A) (a : A), fold f s a = fold' f s a. Proof. unfold fold', elements in |- *. @@ -1106,8 +1409,8 @@ Proof. 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. + forall (s:t elt)(Hs:bst s)(A : Type)(i:A)(f : key -> elt -> A -> A), + fold f s i = fold_left (fun a p => f p#1 p#2 a) (elements s) i. Proof. intros. rewrite fold_equiv. @@ -1118,288 +1421,93 @@ 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 *) +(** [flatten_e e] returns the list of elements of the enumeration [e] + i.e. the list of elements actually compared *) -Fixpoint flatten_e (e : enumeration) : list (key*elt) := match e with +Fixpoint flatten_e (e : enumeration elt) : 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. +Lemma flatten_e_elements : + forall (l:t elt) 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 elements_node. Qed. -Lemma sorted_flatten_e : - forall e : enumeration, sorted_e e -> sort ltk (flatten_e e). +Lemma cons_1 : forall (s:t elt) e, + flatten_e (cons s e) = elements s ++ 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. + induction s; simpl; auto; intros. + rewrite IHs1; apply flatten_e_elements; auto. Qed. -Lemma elements_app : - forall s acc, elements_aux acc s = elements s ++ acc. +(** Proof of correction for the comparison *) + +Variable cmp : elt->elt->bool. + +Definition IfEq b l1 l2 := L.equal cmp l1 l2 = b. + +Lemma cons_IfEq : forall b x1 x2 d1 d2 l1 l2, + X.eq x1 x2 -> cmp d1 d2 = true -> + IfEq b l1 l2 -> + IfEq b ((x1,d1)::l1) ((x2,d2)::l2). 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. + unfold IfEq; destruct b; simpl; intros; destruct X.compare; simpl; + try rewrite H0; auto; order. 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. +Lemma equal_end_IfEq : forall e2, + IfEq (equal_end e2) nil (flatten_e e2). Proof. - simpl in |- *; unfold elements in |- *; simpl in |- *; intuition. - repeat rewrite elements_app. - repeat rewrite <- app_nil_end. - repeat rewrite app_ass; auto. + destruct e2; red; 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. +Lemma equal_more_IfEq : + forall x1 d1 (cont:enumeration elt -> bool) x2 d2 r2 e2 l, + IfEq (cont (cons r2 e2)) l (elements r2 ++ flatten_e e2) -> + IfEq (equal_more cmp x1 d1 cont (More x2 d2 r2 e2)) ((x1,d1)::l) + (flatten_e (More x2 d2 r2 e2)). Proof. - intros; simpl. - apply compare_flatten_1. + unfold IfEq; simpl; intros; destruct X.compare; simpl; auto. + rewrite <-andb_lazy_alt; f_equal; auto. Qed. -Open Local 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. +Lemma equal_cont_IfEq : forall m1 cont e2 l, + (forall e, IfEq (cont e) l (flatten_e e)) -> + IfEq (equal_cont cmp m1 cont e2) (elements m1 ++ l) (flatten_e e2). Proof. - simple induction s. - simpl in |- *; omega. - intros. - Measure_e_t; omega. + induction m1 as [|l1 Hl1 x1 d1 r1 Hr1 h1]; simpl; intros; auto. + rewrite <- elements_node; simpl. + apply Hl1; auto. + clear e2; intros [|x2 d2 r2 e2]. + simpl; red; auto. + apply equal_more_IfEq. + rewrite <- cons_1; auto. 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. +Lemma equal_IfEq : forall (m1 m2:t elt), + IfEq (equal cmp m1 m2) (elements m1) (elements m2). Proof. - simple induction e. - simpl in |- *; omega. + intros; unfold equal. + rewrite (app_nil_end (elements m1)). + replace (elements m2) with (flatten_e (cons m2 (End _))) + by (rewrite cons_1; simpl; rewrite <-app_nil_end; auto). + apply equal_cont_IfEq. intros. - Measure_e; Measure_e_t_0 t; omega. + apply equal_end_IfEq; auto. Qed. -Ltac Measure_e_0 e := generalize (@measure_e_0 e); intro. - -(** Induction principle over the sum of the measures for two lists *) +Definition Equivb 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). -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'. +Lemma Equivb_elements : forall s s', + Equivb s s' <-> L.Equivb cmp (elements s) (elements s'). 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. +unfold Equivb, L.Equivb; split; split; intros. do 2 rewrite elements_in; firstorder. destruct H. apply (H2 k); rewrite <- elements_mapsto; auto. @@ -1408,95 +1516,46 @@ 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'}. +Lemma equal_Equivb : forall (s s': t elt), bst s -> bst s' -> + (equal cmp s s' = true <-> Equivb 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. + intros s s' B B'. + rewrite Equivb_elements, <- equal_IfEq. + split; [apply L.equal_2|apply L.equal_1]; auto. Qed. -End Elt2. - -Section Elts. - -Variable elt elt' elt'' : Set. +End Elt. Section Map. +Variable elt elt' : Type. 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). +Lemma map_1 : forall (m: t elt)(x:key)(e:elt), + MapsTo x e m -> MapsTo x (f e) (map f 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. + In x (map f m) -> In x m. Proof. induction m; simpl; inversion_clear 1; auto. Qed. -Lemma map_bst : forall m, bst m -> bst (map m). +Lemma map_bst : forall m, bst m -> bst (map f 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. +inversion_clear 1; constructor; auto; + red; auto using map_2. 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. +Section Mapi. +Variable elt elt' : Type. +Variable f : key -> elt -> elt'. 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). + MapsTo x e m -> exists y, X.eq y x /\ MapsTo x (f y e) (mapi f m). Proof. induction m; simpl; inversion_clear 1; auto. exists k; auto. @@ -1507,198 +1566,242 @@ exists x0; intuition. Qed. Lemma mapi_2 : forall (m: t elt)(x:key), - In x (mapi m) -> In x m. + In x (mapi f m) -> In x m. Proof. induction m; simpl; inversion_clear 1; auto. Qed. -Lemma mapi_bst : forall m, bst m -> bst (mapi m). +Lemma mapi_bst : forall m, bst m -> bst (mapi f 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. +inversion_clear 1; constructor; auto; + red; auto using mapi_2. 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 _). +Section Map_option. +Variable elt elt' : Type. +Variable f : key -> elt -> option elt'. +Hypothesis f_compat : forall x x' d, X.eq x x' -> f x d = f x' d. -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). +Lemma map_option_2 : forall (m:t elt)(x:key), + In x (map_option f m) -> exists d, MapsTo x d m /\ f x d <> None. Proof. -unfold anti_elements; induction l. -simpl; auto. -simpl; destruct a; intros. -apply IHl. -apply add_avl; auto. +intros m; functional induction (map_option f m); simpl; auto; intros. +inversion H. +rewrite join_in in H; destruct H as [H|[H|H]]. +exists d; split; auto; rewrite (f_compat d H), e0; discriminate. +destruct (IHt _ H) as (d0 & ? & ?); exists d0; auto. +destruct (IHt0 _ H) as (d0 & ? & ?); exists d0; auto. +rewrite concat_in in H; destruct H as [H|H]. +destruct (IHt _ H) as (d0 & ? & ?); exists d0; auto. +destruct (IHt0 _ H) as (d0 & ? & ?); exists d0; auto. Qed. -Lemma anti_elements_avl : forall l, avl (anti_elements l). +Lemma map_option_bst : forall m, bst m -> bst (map_option f m). Proof. -unfold anti_elements, empty; intros; apply anti_elements_avl_aux; auto. -Qed. +intros m; functional induction (map_option f m); simpl; auto; intros; + inv bst. +apply join_bst; auto; intros y H; + destruct (map_option_2 H) as (d0 & ? & ?); eauto using MapsTo_In. +apply concat_bst; auto; intros y y' H H'. +destruct (map_option_2 H) as (d0 & ? & ?). +destruct (map_option_2 H') as (d0' & ? & ?). +eapply X.lt_trans with x; eauto using MapsTo_In. +Qed. +Hint Resolve map_option_bst. + +Ltac nonify e := + replace e with (@None elt) by + (symmetry; rewrite not_find_iff; auto; intro; order). + +Lemma map_option_find : forall (m:t elt)(x:key), + bst m -> + find x (map_option f m) = + match (find x m) with Some d => f x d | None => None end. +Proof. +intros m; functional induction (map_option f m); simpl; auto; intros; + inv bst; rewrite join_find || rewrite concat_find; auto; simpl; + try destruct X.compare; simpl; auto. +rewrite (f_compat d e); auto. +intros y H; + destruct (map_option_2 H) as (? & ? & ?); eauto using MapsTo_In. +intros y H; + destruct (map_option_2 H) as (? & ? & ?); eauto using MapsTo_In. + +rewrite <- IHt, IHt0; auto; nonify (find x0 r); auto. +rewrite IHt, IHt0; auto; nonify (find x0 r); nonify (find x0 l); auto. +rewrite (f_compat d e); auto. +rewrite <- IHt0, IHt; auto; nonify (find x0 l); auto. + destruct (find x0 (map_option f r)); auto. + +intros y y' H H'. +destruct (map_option_2 H) as (? & ? & ?). +destruct (map_option_2 H') as (? & ? & ?). +eapply X.lt_trans with x; eauto using MapsTo_In. +Qed. + +End Map_option. + +Section Map2_opt. +Variable elt elt' elt'' : Type. +Variable f0 : key -> option elt -> option elt' -> option elt''. +Variable f : key -> elt -> option elt' -> option elt''. +Variable mapl : t elt -> t elt''. +Variable mapr : t elt' -> t elt''. +Hypothesis f0_f : forall x d o, f x d o = f0 x (Some d) o. +Hypothesis mapl_bst : forall m, bst m -> bst (mapl m). +Hypothesis mapr_bst : forall m', bst m' -> bst (mapr m'). +Hypothesis mapl_f0 : forall x m, bst m -> + find x (mapl m) = + match find x m with Some d => f0 x (Some d) None | None => None end. +Hypothesis mapr_f0 : forall x m', bst m' -> + find x (mapr m') = + match find x m' with Some d' => f0 x None (Some d') | None => None end. +Hypothesis f0_compat : forall x x' o o', X.eq x x' -> f0 x o o' = f0 x' o o'. + +Notation map2_opt := (map2_opt f mapl mapr). + +Lemma map2_opt_2 : forall m m' y, bst m -> bst m' -> + In y (map2_opt m m') -> In y m \/ In y m'. +Proof. +intros m m'; functional induction (map2_opt m m'); intros; + auto; try factornode _x0 _x1 _x2 _x3 _x4 as m2; + try (generalize (split_in_1 x1 H0 y)(split_in_2 x1 H0 y) + (split_bst x1 H0); rewrite e1; simpl; destruct 3; inv bst). + +right; apply find_in. +generalize (in_find (mapr_bst H0) H1); rewrite mapr_f0; auto. +destruct (find y m2); auto; intros; discriminate. + +factornode l1 x1 d1 r1 _x as m1. +left; apply find_in. +generalize (in_find (mapl_bst H) H1); rewrite mapl_f0; auto. +destruct (find y m1); auto; intros; discriminate. + +rewrite join_in in H1; destruct H1 as [H'|[H'|H']]; auto. +destruct (IHt1 y H6 H4 H'); intuition. +destruct (IHt0 y H7 H5 H'); intuition. + +rewrite concat_in in H1; destruct H1 as [H'|H']; auto. +destruct (IHt1 y H6 H4 H'); intuition. +destruct (IHt0 y H7 H5 H'); intuition. +Qed. + +Lemma map2_opt_bst : forall m m', bst m -> bst m' -> + bst (map2_opt m m'). +Proof. +intros m m'; functional induction (map2_opt m m'); intros; + auto; try factornode _x0 _x1 _x2 _x3 _x4 as m2; inv bst; + generalize (split_in_1 x1 H0)(split_in_2 x1 H0)(split_bst x1 H0); + rewrite e1; simpl in *; destruct 3. + +apply join_bst; auto. +intros y Hy; specialize H with y. +destruct (map2_opt_2 H1 H6 Hy); intuition. +intros y Hy; specialize H5 with y. +destruct (map2_opt_2 H2 H7 Hy); intuition. + +apply concat_bst; auto. +intros y y' Hy Hy'; specialize H with y; specialize H5 with y'. +apply X.lt_trans with x1. +destruct (map2_opt_2 H1 H6 Hy); intuition. +destruct (map2_opt_2 H2 H7 Hy'); intuition. +Qed. +Hint Resolve map2_opt_bst. + +Ltac map2_aux := + match goal with + | H : In ?x _ \/ In ?x ?m, + H' : find ?x ?m = find ?x ?m', B:bst ?m, B':bst ?m' |- _ => + destruct H; [ intuition_in; order | + rewrite <-(find_in_equiv B B' H'); auto ] + end. -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. +Ltac nonify t := + match t with (find ?y (map2_opt ?m ?m')) => + replace t with (@None elt''); + [ | symmetry; rewrite not_find_iff; auto; intro; + destruct (@map2_opt_2 m m' y); auto; order ] + end. -Lemma anti_elements_bst : forall l, bst (anti_elements l). -Proof. -unfold anti_elements, empty; intros; apply anti_elements_bst_aux; auto. -Qed. +Lemma map2_opt_1 : forall m m' y, bst m -> bst m' -> + In y m \/ In y m' -> + find y (map2_opt m m') = f0 y (find y m) (find y m'). +Proof. +intros m m'; functional induction (map2_opt m m'); intros; + auto; try factornode _x0 _x1 _x2 _x3 _x4 as m2; + try (generalize (split_in_1 x1 H0)(split_in_2 x1 H0) + (split_in_3 x1 H0)(split_bst x1 H0)(split_find x1 y H0) + (split_lt_tree (x:=x1) H0)(split_gt_tree (x:=x1) H0); + rewrite e1; simpl in *; destruct 4; intros; inv bst; + subst o2; rewrite H7, ?join_find, ?concat_find; auto). + +simpl; destruct H1; [ inversion_clear H1 | ]. +rewrite mapr_f0; auto. +generalize (in_find H0 H1); destruct (find y m2); intuition. + +factornode l1 x1 d1 r1 _x as m1. +destruct H1; [ | inversion_clear H1 ]. +rewrite mapl_f0; auto. +generalize (in_find H H1); destruct (find y m1); intuition. + +simpl; destruct X.compare; auto. +apply IHt1; auto; map2_aux. +rewrite (@f0_compat y x1), <- f0_f; auto. +apply IHt0; auto; map2_aux. +intros z Hz; destruct (@map2_opt_2 l1 l2' z); auto. +intros z Hz; destruct (@map2_opt_2 r1 r2' z); auto. + +destruct X.compare. +nonify (find y (map2_opt r1 r2')). +apply IHt1; auto; map2_aux. +nonify (find y (map2_opt r1 r2')). +nonify (find y (map2_opt l1 l2')). +rewrite (@f0_compat y x1), <- f0_f; auto. +nonify (find y (map2_opt l1 l2')). +rewrite IHt0; auto; [ | map2_aux ]. +destruct (f0 y (find y r1) (find y r2')); auto. +intros y1 y2 Hy1 Hy2; apply X.lt_trans with x1. + destruct (@map2_opt_2 l1 l2' y1); auto. + destruct (@map2_opt_2 r1 r2' y2); auto. +Qed. + +End Map2_opt. -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. +Section Map2. +Variable elt elt' elt'' : Type. +Variable f : option elt -> option elt' -> option elt''. -Lemma map2_avl : forall (m: t elt)(m': t elt'), avl (map2 m m'). +Lemma map2_bst : forall m m', bst m -> bst m' -> bst (map2 f m m'). Proof. -unfold map2; intros; apply anti_elements_avl; auto. +unfold map2; intros. +apply map2_opt_bst with (fun _ => f); auto using map_option_bst; + intros; rewrite map_option_find; auto. Qed. -Lemma map2_bst : forall (m: t elt)(m': t elt'), bst (map2 m m'). +Lemma map2_1 : forall m m' y, bst m -> bst m' -> + In y m \/ In y m' -> find y (map2 f m m') = f (find y m) (find y 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. +rewrite (map2_opt_1 (f0:=fun _ => f)); + auto using map_option_bst; intros; rewrite map_option_find; 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'. +Lemma map2_2 : forall m m' y, bst m -> bst m' -> + In y (map2 f m m') -> In y m \/ In y 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. +eapply map2_opt_2 with (f0:=fun _ => f); eauto; intros. + apply map_option_bst; auto. + apply map_option_bst; auto. + rewrite map_option_find; auto. + rewrite map_option_find; auto. Qed. End Map2. -End Elts. +End Proofs. End Raw. (** * Encapsulation @@ -1710,178 +1813,184 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. Module E := X. Module Raw := Raw I X. + Import Raw.Proofs. - Record bbst (elt:Set) : Set := - Bbst {this :> Raw.tree elt; is_bst : Raw.bst this; is_avl: Raw.avl this}. + Record bst (elt:Type) := + Bst {this :> Raw.tree elt; is_bst : Raw.bst this}. - Definition t := bbst. + Definition t := bst. Definition key := E.t. Section Elt. - Variable elt elt' elt'': Set. + Variable elt elt' elt'': Type. 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 empty : t elt := Bst (empty_bst 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 add x e m : t elt := Bst (add_bst x e m.(is_bst)). + Definition remove x m : t elt := Bst (remove_bst x m.(is_bst)). 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 map f m : t elt' := Bst (map_bst f m.(is_bst)). Definition mapi (f:key->elt->elt') m : t elt' := - Bbst (Raw.mapi_bst f m.(is_bst)) (Raw.mapi_avl f m.(is_avl)). + Bst (mapi_bst f m.(is_bst)). Definition map2 f m (m':t elt') : t elt'' := - Bbst (Raw.map2_bst f m m') (Raw.map2_avl f m m'). + Bst (map2_bst f m.(is_bst) m'.(is_bst)). 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 cardinal m := Raw.cardinal m.(this). + Definition fold (A:Type) (f:key->elt->A->A) m i := Raw.fold (A:=A) f m.(this) i. + Definition equal cmp m m' : bool := Raw.equal cmp m.(this) m'.(this). 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 Empty m : Prop := 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. + Definition eq_key : (key*elt) -> (key*elt) -> Prop := @PX.eqk elt. + Definition eq_key_elt : (key*elt) -> (key*elt) -> Prop := @PX.eqke elt. + Definition lt_key : (key*elt) -> (key*elt) -> Prop := @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. + Proof. intros m; exact (@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. + unfold In, mem; intros m x; rewrite In_alt; simpl; apply 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. + unfold In, mem; intros m x; rewrite In_alt; simpl; apply mem_2; auto. Qed. Lemma empty_1 : Empty empty. - Proof. exact (@Raw.empty_1 elt). Qed. + Proof. exact (@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. + Proof. intros m; exact (@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. + Proof. intros m; exact (@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. + Proof. intros m x y e; exact (@add_1 elt _ x y e). 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. + Proof. intros m x y e e'; exact (@add_2 elt _ x y e e'). 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. + Proof. intros m x y e e'; exact (@add_3 elt _ x y e e'). 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. + unfold In, remove; intros m x y; rewrite In_alt; simpl; apply 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. + Proof. intros m x y e; exact (@remove_2 elt _ x y e m.(is_bst)). 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. + Proof. intros m x y e; exact (@remove_3 elt _ x y e m.(is_bst)). 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. + Proof. intros m x e; exact (@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. + Proof. intros m; exact (@find_2 elt m.(this)). Qed. - Lemma fold_1 : forall m (A : Set) (i : A) (f : key -> elt -> A -> A), + Lemma fold_1 : forall m (A : Type) (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. + Proof. intros m; exact (@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. + intros; unfold elements, MapsTo, eq_key_elt; rewrite 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. + intros; unfold elements, MapsTo, eq_key_elt; rewrite <- 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. + Proof. intros m; exact (@elements_sort elt m.(this) m.(is_bst)). Qed. - Definition Equal cmp m m' := + Lemma elements_3w : forall m, NoDupA eq_key (elements m). + Proof. intros m; exact (@elements_nodup elt m.(this) m.(is_bst)). Qed. + + Lemma cardinal_1 : forall m, cardinal m = length (elements m). + Proof. intro m; exact (@elements_cardinal elt m.(this)). Qed. + + Definition Equal m m' := forall y, find y m = find y m'. + Definition Equiv (eq_elt:elt->elt->Prop) 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). + (forall k e e', MapsTo k e m -> MapsTo k e' m' -> eq_elt e e'). + Definition Equivb cmp := Equiv (Cmp cmp). - Lemma Equal_Equal : forall cmp m m', Equal cmp m m' <-> Raw.Equal cmp m m'. + Lemma Equivb_Equivb : forall cmp m m', + Equivb cmp m m' <-> Raw.Proofs.Equivb 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. + intros; unfold Equivb, Equiv, Raw.Proofs.Equivb, In; intuition. + generalize (H0 k); do 2 rewrite In_alt; intuition. + generalize (H0 k); do 2 rewrite In_alt; intuition. + generalize (H0 k); do 2 rewrite <- In_alt; intuition. + generalize (H0 k); do 2 rewrite <- In_alt; intuition. + Qed. Lemma equal_1 : forall m m' cmp, - Equal cmp m m' -> equal cmp m m' = true. + Equivb 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. + unfold equal; intros (m,b) (m',b') cmp; rewrite Equivb_Equivb; + intros; simpl in *; rewrite equal_Equivb; auto. Qed. Lemma equal_2 : forall m m' cmp, - equal cmp m m' = true -> Equal cmp m m'. + equal cmp m m' = true -> Equivb cmp m m'. Proof. - unfold equal; intros; rewrite Equal_Equal. - destruct (@Raw.equal _ cmp m m'); auto; try discriminate. - Qed. + unfold equal; intros (m,b) (m',b') cmp; rewrite Equivb_Equivb; + intros; simpl in *; rewrite <-equal_Equivb; auto. + Qed. End Elt. - Lemma map_1 : forall (elt elt':Set)(m: t elt)(x:key)(e:elt)(f:elt->elt'), + Lemma map_1 : forall (elt elt':Type)(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. + Proof. intros elt elt' m x e f; exact (@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. + Lemma map_2 : forall (elt elt':Type)(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. + intros elt elt' m x f; do 2 unfold In in *; do 2 rewrite In_alt; simpl. + apply map_2; auto. Qed. - Lemma mapi_1 : forall (elt elt':Set)(m: t elt)(x:key)(e:elt) + Lemma mapi_1 : forall (elt elt':Type)(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) + Proof. intros elt elt' m x e f; exact (@mapi_1 elt elt' f m.(this) x e). Qed. + Lemma mapi_2 : forall (elt elt':Type)(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. + intros elt elt' m x f; unfold In in *; do 2 rewrite In_alt; simpl; apply mapi_2; auto. + Qed. - Lemma map2_1 : forall (elt elt' elt'':Set)(m: t elt)(m': t elt') + Lemma map2_1 : forall (elt elt' elt'':Type)(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. + do 2 rewrite In_alt; intros; simpl; apply 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') + Lemma map2_2 : forall (elt elt' elt'':Type)(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. + do 3 rewrite In_alt; intros; simpl in *; eapply map2_2; eauto. apply m.(is_bst). apply m'.(is_bst). Qed. @@ -1891,158 +2000,185 @@ End IntMake. Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: Sord with Module Data := D - with Module MapS.E := X. + with Module MapS.E := X. Module Data := D. - Module MapS := IntMake(I)(X). - Import MapS. + Module Import MapS := IntMake(I)(X). + Module LO := FMapList.Make_ord(X)(D). + Module R := Raw. + Module P := Raw.Proofs. + + Definition t := MapS.t D.t. + + Definition cmp e e' := + match D.compare e e' with EQ _ => true | _ => false end. + + (** One step of comparison of elements *) + + Definition compare_more x1 d1 (cont:R.enumeration D.t -> comparison) e2 := + match e2 with + | R.End => Gt + | R.More x2 d2 r2 e2 => + match X.compare x1 x2 with + | EQ _ => match D.compare d1 d2 with + | EQ _ => cont (R.cons r2 e2) + | LT _ => Lt + | GT _ => Gt + end + | LT _ => Lt + | GT _ => Gt + end + end. - Module MD := OrderedTypeFacts(D). - Import MD. + (** Comparison of left tree, middle element, then right tree *) - Module LO := FMapList.Make_ord(X)(D). + Fixpoint compare_cont s1 (cont:R.enumeration D.t -> comparison) e2 := + match s1 with + | R.Leaf => cont e2 + | R.Node l1 x1 d1 r1 _ => + compare_cont l1 (compare_more x1 d1 (compare_cont r1 cont)) e2 + end. + + (** Initial continuation *) + + Definition compare_end (e2:R.enumeration D.t) := + match e2 with R.End => Eq | _ => Lt end. + + (** The complete comparison *) - Definition t := MapS.t D.t. + Definition compare_pure s1 s2 := + compare_cont s1 compare_end (R.cons s2 (Raw.End _)). - Definition cmp e e' := match D.compare e e' with EQ _ => true | _ => false end. + (** Correctness of this comparison *) - Definition elements (m:t) := - LO.MapS.Build_slist (Raw.elements_sort m.(is_bst)). + Definition Cmp c := + match c with + | Eq => LO.eq_list + | Lt => LO.lt_list + | Gt => (fun l1 l2 => LO.lt_list l2 l1) + end. + + Lemma cons_Cmp : forall c x1 x2 d1 d2 l1 l2, + X.eq x1 x2 -> D.eq d1 d2 -> + Cmp c l1 l2 -> Cmp c ((x1,d1)::l1) ((x2,d2)::l2). + Proof. + destruct c; simpl; intros; P.MX.elim_comp; auto. + Qed. + Hint Resolve cons_Cmp. + + Lemma compare_end_Cmp : + forall e2, Cmp (compare_end e2) nil (P.flatten_e e2). + Proof. + destruct e2; simpl; auto. + Qed. + + Lemma compare_more_Cmp : forall x1 d1 cont x2 d2 r2 e2 l, + Cmp (cont (R.cons r2 e2)) l (R.elements r2 ++ P.flatten_e e2) -> + Cmp (compare_more x1 d1 cont (R.More x2 d2 r2 e2)) ((x1,d1)::l) + (P.flatten_e (R.More x2 d2 r2 e2)). + Proof. + simpl; intros; destruct X.compare; simpl; + try destruct D.compare; simpl; auto; P.MX.elim_comp; auto. + Qed. + + Lemma compare_cont_Cmp : forall s1 cont e2 l, + (forall e, Cmp (cont e) l (P.flatten_e e)) -> + Cmp (compare_cont s1 cont e2) (R.elements s1 ++ l) (P.flatten_e e2). + Proof. + induction s1 as [|l1 Hl1 x1 d1 r1 Hr1 h1]; simpl; intros; auto. + rewrite <- P.elements_node; simpl. + apply Hl1; auto. clear e2. intros [|x2 d2 r2 e2]. + simpl; auto. + apply compare_more_Cmp. + rewrite <- P.cons_1; auto. + Qed. + + Lemma compare_Cmp : forall s1 s2, + Cmp (compare_pure s1 s2) (R.elements s1) (R.elements s2). + Proof. + intros; unfold compare_pure. + rewrite (app_nil_end (R.elements s1)). + replace (R.elements s2) with (P.flatten_e (R.cons s2 (R.End _))) by + (rewrite P.cons_1; simpl; rewrite <- app_nil_end; auto). + auto using compare_cont_Cmp, compare_end_Cmp. + Qed. - Definition eq : t -> t -> Prop := - fun m1 m2 => LO.eq (elements m1) (elements m2). + (** The dependent-style [compare] *) - Definition lt : t -> t -> Prop := - fun m1 m2 => LO.lt (elements m1) (elements m2). + Definition eq (m1 m2 : t) := LO.eq_list (elements m1) (elements m2). + Definition lt (m1 m2 : t) := LO.lt_list (elements m1) (elements m2). - Lemma eq_1 : forall m m', Equal cmp m m' -> eq m m'. + Definition compare (s s':t) : Compare lt eq s s'. + Proof. + intros (s,b) (s',b'). + generalize (compare_Cmp s s'). + destruct compare_pure; intros; [apply EQ|apply LT|apply GT]; red; auto. + Defined. + + (* Proofs about [eq] and [lt] *) + + Definition selements (m1 : t) := + LO.MapS.Build_slist (P.elements_sort m1.(is_bst)). + + Definition seq (m1 m2 : t) := LO.eq (selements m1) (selements m2). + Definition slt (m1 m2 : t) := LO.lt (selements m1) (selements m2). + + Lemma eq_seq : forall m1 m2, eq m1 m2 <-> seq m1 m2. + Proof. + unfold eq, seq, selements, elements, LO.eq; intuition. + Qed. + + Lemma lt_slt : forall m1 m2, lt m1 m2 <-> slt m1 m2. + Proof. + unfold lt, slt, selements, elements, LO.lt; intuition. + Qed. + + Lemma eq_1 : forall (m m' : t), Equivb 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. + rewrite eq_seq; unfold seq. + rewrite Equivb_Equivb. + rewrite P.Equivb_elements. + auto using LO.eq_1. Qed. - Lemma eq_2 : forall m m', eq m m' -> Equal cmp m m'. + Lemma eq_2 : forall m m', eq m m' -> Equivb cmp m m'. Proof. intros m m'. - unfold eq. - rewrite Equal_Equal. - rewrite Raw.Equal_elements. + rewrite eq_seq; unfold seq. + rewrite Equivb_Equivb. + rewrite P.Equivb_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. + intros; rewrite eq_seq; unfold seq; 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. + intros m1 m2; rewrite 2 eq_seq; unfold seq; 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. + intros m1 m2 M3; rewrite 3 eq_seq; unfold seq. + 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. + intros m1 m2 m3; rewrite 3 lt_slt; unfold slt; + 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 Local 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. + intros m1 m2; rewrite lt_slt, eq_seq; unfold slt, seq; + intros; apply LO.lt_not_eq; auto. Qed. End IntMake_ord. @@ -2056,3 +2192,4 @@ Module Make_ord (X: OrderedType)(D: OrderedType) <: Sord with Module Data := D with Module MapS.E := X :=IntMake_ord(Z_as_Int)(X)(D). + |