diff options
Diffstat (limited to 'theories/MMaps/MMapAVL.v')
| -rw-r--r-- | theories/MMaps/MMapAVL.v | 2158 |
1 files changed, 2158 insertions, 0 deletions
diff --git a/theories/MMaps/MMapAVL.v b/theories/MMaps/MMapAVL.v new file mode 100644 index 00000000..d840f1f3 --- /dev/null +++ b/theories/MMaps/MMapAVL.v @@ -0,0 +1,2158 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* Finite map library. *) + +(** * MMapAVL *) + +(** This module implements maps using AVL trees. + It follows the implementation from Ocaml's standard library. + + See the comments at the beginning of MSetAVL for more details. +*) + +Require Import Bool PeanoNat BinInt Int MMapInterface MMapList. +Require Import Orders OrdersFacts OrdersLists. + +Set Implicit Arguments. +Unset Strict Implicit. +(* For nicer extraction, we create inductive principles + only when needed *) +Local Unset Elimination Schemes. + +(** Notations and helper lemma about pairs *) + +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. + +(** * The Raw functor + + Functor of pure functions + separate proofs of invariant + preservation *) + +Module Raw (Import I:Int)(X: OrderedType). +Local Open Scope pair_scope. +Local Open Scope lazy_bool_scope. +Local Open Scope Int_scope. +Local Notation int := I.t. + +Definition key := X.t. +Hint Transparent key. + +(** * Trees *) + +Section Elt. + +Variable elt : Type. + +(** * Trees + + The fifth field of [Node] is the height of the tree *) + +Inductive tree := + | Leaf : tree + | Node : tree -> key -> elt -> tree -> int -> tree. + +Notation t := 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. + +(** * Membership *) + +(** The [mem] function is deciding membership. 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 + | Eq => true + | Lt => mem x l + | 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 + | Eq => Some d + | Lt => find x l + | Gt => find x r + end + end. + +(** * Helper functions *) + +(** [create l x r] creates a node, assuming [l] and [r] + to be balanced and [|height l - height r| <= 2]. *) + +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 (hr+2) <? hl then + match l with + | Leaf => assert_false l x d r + | Node ll lx ld lr _ => + if (height lr) <=? (height ll) 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 (hl+2) <? hr then + match r with + | Leaf => assert_false l x d r + | Node rl rx rd rr _ => + if (height rl) <=? (height rr) 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 + | Eq => Node l y d r h + | Lt => bal (add x d l) y d' r + | 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 + + [merge0 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]. +*) + +Definition merge0 s1 s2 := + match s1,s2 with + | Leaf, _ => s2 + | _, Leaf => s1 + | _, Node l2 x2 d2 r2 h2 => + let '(s2',(x,d)) := remove_min l2 x2 d2 r2 in + bal s1 x d s2' + end. + +(** * Deletion *) + +Fixpoint remove x m := match m with + | Leaf => Leaf + | Node l y d r h => + match X.compare x y with + | Eq => merge0 l r + | Lt => bal (remove x l) y d 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 rh+2 <? lh then bal ll lx ld (join lr x d r) + else if lh+2 <? rh 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. + +(** * Bindings *) + +(** [bindings_aux acc t] catenates the bindings of [t] in infix + order to the list [acc] *) + +Fixpoint bindings_aux (acc : list (key*elt)) m : list (key*elt) := + match m with + | Leaf => acc + | Node l x d r _ => bindings_aux ((x,d) :: bindings_aux acc r) l + end. + +(** then [bindings] is an instantiation with an empty [acc] *) + +Definition bindings := bindings_aux nil. + +(** * Fold *) + +Fixpoint fold {A} (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 mapo (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 (mapo f l) x d' (mapo f r) + | None => concat (mapo f l) (mapo f r) + end + end. + +(** * Generalized merge + + Suggestion by B. Gregoire: a [merge] function with specialized + arguments that allows bypassing 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 GMerge. +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 gmerge 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 (gmerge l1 l2') x1 e (gmerge r1 r2') + | None => concat (gmerge l1 l2') (gmerge r1 r2') + end + end. + +End GMerge. + +(** * Merge + + The [merge] function of the Map interface can be implemented + via [gmerge] and [mapo]. +*) + +Section Merge. +Variable elt elt' elt'' : Type. +Variable f : key -> option elt -> option elt' -> option elt''. + +Definition merge : t elt -> t elt' -> t elt'' := + gmerge + (fun k d o => f k (Some d) o) + (mapo (fun k d => f k (Some d) None)) + (mapo (fun k d' => f k None (Some d'))). + +End Merge. + + + +(** * 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', + MapsTo x e l -> MapsTo x e (Node l y e' r h) + | MapsRight : forall l r h y e', + MapsTo x e r -> MapsTo x e (Node l y e' r h). + +Inductive In (x : key) : 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', + In x l -> In x (Node l y e' r h) + | InRight : forall l r h y e', + In x r -> In x (Node l y e' r h). + +Definition In0 k m := exists e:elt, MapsTo k e m. + +(** ** Binary search trees *) + +(** [Above x m] : [x] is strictly greater than any key in [m]. + [Below x m] : [x] is strictly smaller than any key in [m]. *) + +Inductive Above (x:key) : t elt -> Prop := + | AbLeaf : Above x (Leaf _) + | AbNode l r h y e : Above x l -> X.lt y x -> Above x r -> + Above x (Node l y e r h). + +Inductive Below (x:key) : t elt -> Prop := + | BeLeaf : Below x (Leaf _) + | BeNode l r h y e : Below x l -> X.lt x y -> Below x r -> + Below x (Node l y e r h). + +Definition Apart (m1 m2 : t elt) : Prop := + forall x1 x2, In x1 m1 -> In x2 m2 -> X.lt x1 x2. + +(** Alternative statements, equivalent with [LtTree] and [GtTree] *) + +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 : t elt -> Prop := + | BSLeaf : Bst (Leaf _) + | BSNode : forall x e l r h, Bst l -> Bst r -> + Above x l -> Below x r -> Bst (Node l x e r h). + +End Invariants. + + +(** * Correctness proofs, isolated in a sub-module *) + +Module Proofs. + Module MX := OrderedTypeFacts X. + Module PX := KeyOrderedType X. + Module L := MMapList.Raw X. + +Local Infix "∈" := In (at level 70). +Local Infix "==" := X.eq (at level 70). +Local Infix "<" := X.lt (at level 70). +Local Infix "<<" := Below (at level 70). +Local Infix ">>" := Above (at level 70). +Local Infix "<<<" := Apart (at level 70). + +Scheme tree_ind := Induction for tree Sort Prop. +Scheme Bst_ind := Induction for Bst Sort Prop. +Scheme MapsTo_ind := Induction for MapsTo Sort Prop. +Scheme In_ind := Induction for In Sort Prop. +Scheme Above_ind := Induction for Above Sort Prop. +Scheme Below_ind := Induction for Below Sort Prop. + +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 merge0_ind := Induction for merge0 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 mapo_ind := Induction for mapo Sort Prop. +Functional Scheme gmerge_ind := Induction for gmerge Sort Prop. + +(** * Automation and dedicated tactics. *) + +Local Hint Constructors tree MapsTo In Bst Above Below. +Local Hint Unfold lt_tree gt_tree Apart. +Local Hint Immediate MX.eq_sym. +Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans. + +Tactic Notation "factornode" ident(s) := + try clear s; + match goal with + | |- context [Node ?l ?x ?e ?r ?h] => + set (s:=Node l x e r h) in *; clearbody s; clear l x e r h + | _ : context [Node ?l ?x ?e ?r ?h] |- _ => + set (s:=Node l x e r h) in *; clearbody s; clear l x e r h + end. + +(** A tactic for cleaning hypothesis after use of functional induction. *) + +Ltac cleanf := + match goal with + | H : X.compare _ _ = Eq |- _ => + rewrite ?H; apply MX.compare_eq in H; cleanf + | H : X.compare _ _ = Lt |- _ => + rewrite ?H; apply MX.compare_lt_iff in H; cleanf + | H : X.compare _ _ = Gt |- _ => + rewrite ?H; apply MX.compare_gt_iff in H; cleanf + | _ => 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 + | H:f _ (Leaf _) |- _ => inversion_clear H; inv f + | H:f _ _ (Leaf _) |- _ => inversion_clear H; inv f + | H:f _ _ _ (Leaf _) |- _ => inversion_clear H; inv f + | H:f (Node _ _ _ _ _) |- _ => inversion_clear H; inv f + | H:f _ (Node _ _ _ _ _) |- _ => inversion_clear H; inv f + | H:f _ _ (Node _ _ _ _ _) |- _ => inversion_clear H; inv f + | H:f _ _ _ (Node _ _ _ _ _) |- _ => inversion_clear H; inv f + | _ => idtac + end. + +Ltac inv_all f := + match goal with + | H: f _ |- _ => inversion_clear H; inv f + | H: f _ _ |- _ => inversion_clear H; inv f + | H: f _ _ _ |- _ => inversion_clear H; inv f + | H: f _ _ _ _ |- _ => inversion_clear H; inv f + | _ => idtac + end. + +Ltac intuition_in := repeat (intuition; inv In; inv MapsTo). + +(* Function/Functional Scheme can't deal with internal fix. + Let's do its job by hand: *) + +Ltac join_tac l x d r := + revert x d r; + 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 (rh+2 <? lh) eqn:LT; + [ 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 (lh+2 <? rh) eqn:LT'; + [ 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 cleansplit := + simpl; cleanf; inv Bst; + match goal with + | E:split _ _ = 〚 ?l, ?o, ?r 〛 |- _ => + change l with (〚l,o,r〛#l); rewrite <- ?E; + change o with (〚l,o,r〛#o); rewrite <- ?E; + change r with (〚l,o,r〛#r); rewrite <- ?E + | _ => idtac + end. + +(** * Basic results about [MapsTo], [In], [lt_tree], [gt_tree], [height] *) + +(** Facts about [MapsTo] and [In]. *) + +Lemma MapsTo_In {elt} k (e:elt) m : MapsTo k e m -> k ∈ m. +Proof. + induction 1; auto. +Qed. +Local Hint Resolve MapsTo_In. + +Lemma In_MapsTo {elt} k m : k ∈ m -> exists (e:elt), MapsTo k e m. +Proof. + induction 1; try destruct IHIn as (e,He); exists e; auto. +Qed. + +Lemma In_alt {elt} k (m:t elt) : In0 k m <-> k ∈ m. +Proof. + split. + intros (e,H); eauto. + unfold In0; apply In_MapsTo; auto. +Qed. + +Lemma MapsTo_1 {elt} m x y (e:elt) : + x == y -> MapsTo x e m -> MapsTo y e m. +Proof. + induction m; simpl; intuition_in; eauto. +Qed. +Hint Immediate MapsTo_1. + +Instance MapsTo_compat {elt} : + Proper (X.eq==>Logic.eq==>Logic.eq==>iff) (@MapsTo elt). +Proof. + intros x x' Hx e e' He m m' Hm. subst. + split; now apply MapsTo_1. +Qed. + +Instance In_compat {elt} : + Proper (X.eq==>Logic.eq==>iff) (@In elt). +Proof. + intros x x' H m m' <-. + induction m; simpl; intuition_in; eauto. +Qed. + +Lemma In_node_iff {elt} l x (e:elt) r h y : + y ∈ (Node l x e r h) <-> y ∈ l \/ y == x \/ y ∈ r. +Proof. + intuition_in. +Qed. + +(** Results about [Above] and [Below] *) + +Lemma above {elt} (m:t elt) x : + x >> m <-> forall y, y ∈ m -> y < x. +Proof. + split. + - induction 1; intuition_in; MX.order. + - induction m; constructor; auto. +Qed. + +Lemma below {elt} (m:t elt) x : + x << m <-> forall y, y ∈ m -> x < y. +Proof. + split. + - induction 1; intuition_in; MX.order. + - induction m; constructor; auto. +Qed. + +Lemma AboveLt {elt} (m:t elt) x y : x >> m -> y ∈ m -> y < x. +Proof. + rewrite above; intuition. +Qed. + +Lemma BelowGt {elt} (m:t elt) x y : x << m -> y ∈ m -> x < y. +Proof. + rewrite below; intuition. +Qed. + +Lemma Above_not_In {elt} (m:t elt) x : x >> m -> ~ x ∈ m. +Proof. + induction 1; intuition_in; MX.order. +Qed. + +Lemma Below_not_In {elt} (m:t elt) x : x << m -> ~ x ∈ m. +Proof. + induction 1; intuition_in; MX.order. +Qed. + +Lemma Above_trans {elt} (m:t elt) x y : x < y -> x >> m -> y >> m. +Proof. + induction 2; constructor; trivial; MX.order. +Qed. + +Lemma Below_trans {elt} (m:t elt) x y : y < x -> x << m -> y << m. +Proof. + induction 2; constructor; trivial; MX.order. +Qed. + +Local Hint Resolve + AboveLt Above_not_In Above_trans + BelowGt Below_not_In Below_trans. + +(** Helper tactic concerning order of elements. *) + +Ltac order := match goal with + | U: _ >> ?m, V: _ ∈ ?m |- _ => + generalize (AboveLt U V); clear U; order + | U: _ << ?m, V: _ ∈ ?m |- _ => + generalize (BelowGt U V); clear U; order + | U: _ >> ?m, V: MapsTo _ _ ?m |- _ => + generalize (AboveLt U (MapsTo_In V)); clear U; order + | U: _ << ?m, V: MapsTo _ _ ?m |- _ => + generalize (BelowGt U (MapsTo_In V)); clear U; order + | _ => MX.order +end. + +Lemma between {elt} (m m':t elt) x : + x >> m -> x << m' -> m <<< m'. +Proof. + intros H H' y y' Hy Hy'. order. +Qed. + +Section Elt. +Variable elt:Type. +Implicit Types m r : t elt. + +(** * Membership *) + +Lemma find_1 m x e : Bst m -> MapsTo x e m -> find x m = Some e. +Proof. + functional induction (find x m); cleanf; + intros; inv Bst; intuition_in; order. +Qed. + +Lemma find_2 m x e : find x m = Some e -> MapsTo x e m. +Proof. + functional induction (find x m); cleanf; subst; intros; auto. + - discriminate. + - injection H as ->. auto. +Qed. + +Lemma find_spec m x e : Bst m -> + (find x m = Some e <-> MapsTo x e m). +Proof. + split; auto using find_1, find_2. +Qed. + +Lemma find_in m x : find x m <> None -> x ∈ m. +Proof. + destruct (find x m) eqn:F; intros H. + - apply MapsTo_In with e. now apply find_2. + - now elim H. +Qed. + +Lemma in_find m x : Bst m -> x ∈ m -> find x m <> None. +Proof. + intros H H'. + destruct (In_MapsTo H') as (d,Hd). + now rewrite (find_1 H Hd). +Qed. + +Lemma find_in_iff m x : Bst m -> + (find x m <> None <-> x ∈ m). +Proof. + split; auto using find_in, in_find. +Qed. + +Lemma not_find_iff m x : Bst m -> + (find x m = None <-> ~ x ∈ m). +Proof. + intros H. rewrite <- find_in_iff; trivial. + destruct (find x m); split; try easy. now destruct 1. +Qed. + +Lemma eq_option_alt (o o':option elt) : + o=o' <-> (forall e, o=Some e <-> o'=Some e). +Proof. +split; intros. +- now subst. +- destruct o, o'; rewrite ?H; auto. symmetry; now apply H. +Qed. + +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. + intros m m' x Hm Hm'. rewrite eq_option_alt. + split; intros H d. now rewrite <- 2 find_spec. now rewrite 2 find_spec. +Qed. + +Lemma find_in_equiv : forall m m' x, Bst m -> Bst m' -> + find x m = find x m' -> + (x ∈ m <-> x ∈ m'). +Proof. + split; intros; apply find_in; [ rewrite <- H1 | rewrite H1 ]; + apply in_find; auto. +Qed. + +Lemma find_compat m x x' : Bst m -> X.eq x x' -> find x m = find x' m. +Proof. + intros B E. + destruct (find x' m) eqn:H. + - apply find_1; trivial. rewrite E. now apply find_2. + - rewrite not_find_iff in *; trivial. now rewrite E. +Qed. + +Lemma mem_spec m x : Bst m -> mem x m = true <-> x ∈ m. +Proof. + functional induction (mem x m); auto; intros; cleanf; + inv Bst; intuition_in; try discriminate; order. +Qed. + +(** * Empty map *) + +Lemma empty_bst : Bst (empty elt). +Proof. + constructor. +Qed. + +Lemma empty_spec x : find x (empty elt) = None. +Proof. + reflexivity. +Qed. + +(** * Emptyness test *) + +Lemma is_empty_spec m : is_empty m = true <-> forall x, find x m = None. +Proof. + destruct m as [|r x e l h]; simpl; split; try easy. + intros H. specialize (H x). now rewrite MX.compare_refl in H. +Qed. + +(** * Helper functions *) + +Lemma create_bst l x e r : + Bst l -> Bst r -> x >> l -> x << r -> Bst (create l x e r). +Proof. + unfold create; auto. +Qed. +Hint Resolve create_bst. + +Lemma create_in l x e r y : + y ∈ (create l x e r) <-> y == x \/ y ∈ l \/ y ∈ r. +Proof. + unfold create; split; [ inversion_clear 1 | ]; intuition. +Qed. + +Lemma bal_bst l x e r : Bst l -> Bst r -> + x >> l -> x << r -> Bst (bal l x e r). +Proof. + functional induction (bal l x e r); intros; cleanf; + inv Bst; inv Above; inv Below; + repeat apply create_bst; auto; unfold create; constructor; eauto. +Qed. +Hint Resolve bal_bst. + +Lemma bal_in l x e r y : + y ∈ (bal l x e r) <-> y == x \/ y ∈ l \/ y ∈ r. +Proof. + functional induction (bal l x e r); intros; cleanf; + rewrite !create_in; intuition_in. +Qed. + +Lemma bal_mapsto l x e r y e' : + MapsTo y e' (bal l x e r) <-> MapsTo y e' (create l x e r). +Proof. + functional induction (bal l x e r); intros; cleanf; + unfold assert_false, create; intuition_in. +Qed. + +Lemma bal_find l x e r y : + Bst l -> Bst r -> x >> l -> x << r -> + find y (bal l x e r) = find y (create l x e r). +Proof. + functional induction (bal l x e r); intros; cleanf; trivial; + inv Bst; inv Above; inv Below; + simpl; repeat case X.compare_spec; intuition; order. +Qed. + +(** * Insertion *) + +Lemma add_in m x y e : + y ∈ (add x e m) <-> y == x \/ y ∈ m. +Proof. + functional induction (add x e m); auto; intros; cleanf; + rewrite ?bal_in; intuition_in. setoid_replace y with x; auto. +Qed. + +Lemma add_lt m x e y : y >> m -> x < y -> y >> add x e m. +Proof. + intros. apply above. intros z. rewrite add_in. destruct 1; order. +Qed. + +Lemma add_gt m x e y : y << m -> y < x -> y << add x e m. +Proof. + intros. apply below. intros z. rewrite add_in. destruct 1; order. +Qed. + +Lemma add_bst m x e : Bst m -> Bst (add x e m). +Proof. + functional induction (add x e m); intros; cleanf; + inv Bst; try apply bal_bst; auto using add_lt, add_gt. +Qed. +Hint Resolve add_lt add_gt add_bst. + +Lemma add_spec1 m x e : Bst m -> find x (add x e m) = Some e. +Proof. + functional induction (add x e m); simpl; intros; cleanf; trivial. + - now rewrite MX.compare_refl. + - inv Bst. rewrite bal_find; auto. + simpl. case X.compare_spec; try order; auto. + - inv Bst. rewrite bal_find; auto. + simpl. case X.compare_spec; try order; auto. +Qed. + +Lemma add_spec2 m x y e : Bst m -> ~ x == y -> + find y (add x e m) = find y m. +Proof. + functional induction (add x e m); simpl; intros; cleanf; trivial. + - case X.compare_spec; trivial; order. + - case X.compare_spec; trivial; order. + - inv Bst. rewrite bal_find by auto. simpl. now rewrite IHt. + - inv Bst. rewrite bal_find by auto. simpl. now rewrite IHt. +Qed. + +Lemma add_find 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. + case X.compare_spec; intros. + - apply find_spec; auto. rewrite H0. apply find_spec; auto. + now apply add_spec1. + - apply add_spec2; trivial; order. + - apply add_spec2; trivial; order. +Qed. + +(** * Extraction of minimum binding *) + +Definition RemoveMin m res := + match m with + | Leaf _ => False + | Node l x e r h => remove_min l x e r = res + end. + +Lemma RemoveMin_step l x e r h m' p : + RemoveMin (Node l x e r h) (m',p) -> + (l = Leaf _ /\ m' = r /\ p = (x,e) \/ + exists m0, RemoveMin l (m0,p) /\ m' = bal m0 x e r). +Proof. + simpl. destruct l as [|ll lx le lr lh]; simpl. + - intros [= -> ->]. now left. + - destruct (remove_min ll lx le lr) as (l',p'). + intros [= <- <-]. right. now exists l'. +Qed. + +Lemma remove_min_mapsto m m' p : RemoveMin m (m',p) -> + forall y e, + MapsTo y e m <-> (y == p#1 /\ e = p#2) \/ MapsTo y e m'. +Proof. + revert m'. + induction m as [|l IH x d r _ h]; [destruct 1|]. + intros m' R. apply RemoveMin_step in R. + destruct R as [(->,(->,->))|[m0 (R,->)]]; intros y e; simpl. + - intuition_in. subst. now constructor. + - rewrite bal_mapsto. unfold create. specialize (IH _ R y e). + intuition_in. +Qed. + +Lemma remove_min_in m m' p : RemoveMin m (m',p) -> + forall y, y ∈ m <-> y == p#1 \/ y ∈ m'. +Proof. + revert m'. + induction m as [|l IH x e r _ h]; [destruct 1|]. + intros m' R y. apply RemoveMin_step in R. + destruct R as [(->,(->,->))|[m0 (R,->)]]. + + intuition_in. + + rewrite bal_in, In_node_iff, (IH _ R); intuition. +Qed. + +Lemma remove_min_lt m m' p : RemoveMin m (m',p) -> + forall y, y >> m -> y >> m'. +Proof. + intros R y L. apply above. intros z Hz. + apply (AboveLt L). + apply (remove_min_in R). now right. +Qed. + +Lemma remove_min_gt m m' p : RemoveMin m (m',p) -> + Bst m -> p#1 << m'. +Proof. + revert m'. + induction m as [|l IH x e r _ h]; [destruct 1|]. + intros m' R H. inv Bst. apply RemoveMin_step in R. + destruct R as [(_,(->,->))|[m0 (R,->)]]; auto. + assert (p#1 << m0) by now apply IH. + assert (In p#1 l) by (apply (remove_min_in R); now left). + apply below. intros z. rewrite bal_in. + intuition_in; order. +Qed. + +Lemma remove_min_bst m m' p : RemoveMin m (m',p) -> + Bst m -> Bst m'. +Proof. + revert m'. + induction m as [|l IH x e r _ h]; [destruct 1|]. + intros m' R H. inv Bst. apply RemoveMin_step in R. + destruct R as [(_,(->,->))|[m0 (R,->)]]; auto. + apply bal_bst; eauto using remove_min_lt. +Qed. + +Lemma remove_min_find m m' p : RemoveMin m (m',p) -> + Bst m -> + forall y, + find y m = + match X.compare y p#1 with + | Eq => Some p#2 + | Lt => None + | Gt => find y m' + end. +Proof. + revert m'. + induction m as [|l IH x e r _ h]; [destruct 1|]. + intros m' R B y. inv Bst. apply RemoveMin_step in R. + destruct R as [(->,(->,->))|[m0 (R,->)]]; auto. + assert (Bst m0) by now apply (remove_min_bst R). + assert (p#1 << m0) by now apply (remove_min_gt R). + assert (x >> m0) by now apply (remove_min_lt R). + assert (In p#1 l) by (apply (remove_min_in R); now left). + simpl in *. + rewrite (IH _ R), bal_find by trivial. clear IH. simpl. + do 2 case X.compare_spec; trivial; try order. +Qed. + +(** * Merging two trees *) + +Ltac factor_remove_min m R := match goal with + | h:int, H:remove_min ?l ?x ?e ?r = ?p |- _ => + assert (R:RemoveMin (Node l x e r h) p) by exact H; + set (m:=Node l x e r h) in *; clearbody m; clear H l x e r +end. + +Lemma merge0_in m1 m2 y : + y ∈ (merge0 m1 m2) <-> y ∈ m1 \/ y ∈ m2. +Proof. + functional induction (merge0 m1 m2); intros; try factornode m1. + - intuition_in. + - intuition_in. + - factor_remove_min l R. rewrite bal_in, (remove_min_in R). + simpl; intuition. +Qed. + +Lemma merge0_mapsto m1 m2 y e : + MapsTo y e (merge0 m1 m2) <-> MapsTo y e m1 \/ MapsTo y e m2. +Proof. + functional induction (merge0 m1 m2); intros; try factornode m1. + - intuition_in. + - intuition_in. + - factor_remove_min l R. rewrite bal_mapsto, (remove_min_mapsto R). + simpl. unfold create; intuition_in. subst. now constructor. +Qed. + +Lemma merge0_bst m1 m2 : Bst m1 -> Bst m2 -> m1 <<< m2 -> + Bst (merge0 m1 m2). +Proof. + functional induction (merge0 m1 m2); intros B1 B2 B12; trivial. + factornode m1. factor_remove_min l R. + apply bal_bst; auto. + - eapply remove_min_bst; eauto. + - apply above. intros z Hz. apply B12; trivial. + rewrite (remove_min_in R). now left. + - now apply (remove_min_gt R). +Qed. +Hint Resolve merge0_bst. + +(** * Deletion *) + +Lemma remove_in m x y : Bst m -> + (y ∈ remove x m <-> ~ y == x /\ y ∈ m). +Proof. + functional induction (remove x m); simpl; intros; cleanf; inv Bst; + rewrite ?merge0_in, ?bal_in, ?IHt; intuition_in; order. +Qed. + +Lemma remove_lt m x y : Bst m -> y >> m -> y >> remove x m. +Proof. + intros. apply above. intro. rewrite remove_in by trivial. + destruct 1; order. +Qed. + +Lemma remove_gt m x y : Bst m -> y << m -> y << remove x m. +Proof. + intros. apply below. intro. rewrite remove_in by trivial. + destruct 1; order. +Qed. + +Lemma remove_bst m x : Bst m -> Bst (remove x m). +Proof. + functional induction (remove x m); simpl; intros; cleanf; inv Bst. + - trivial. + - apply merge0_bst; eauto. + - apply bal_bst; auto using remove_lt. + - apply bal_bst; auto using remove_gt. +Qed. +Hint Resolve remove_bst remove_gt remove_lt. + +Lemma remove_spec1 m x : Bst m -> find x (remove x m) = None. +Proof. + intros. apply not_find_iff; auto. rewrite remove_in; intuition. +Qed. + +Lemma remove_spec2 m x y : Bst m -> ~ x == y -> + find y (remove x m) = find y m. +Proof. + functional induction (remove x m); simpl; intros; cleanf; inv Bst. + - trivial. + - case X.compare_spec; intros; try order; + rewrite find_mapsto_equiv; auto. + + intros. rewrite merge0_mapsto; intuition; order. + + apply merge0_bst; auto. red; intros; transitivity y0; order. + + intros. rewrite merge0_mapsto; intuition; order. + + apply merge0_bst; auto. now apply between with y0. + - rewrite bal_find by auto. simpl. case X.compare_spec; auto. + - rewrite bal_find by auto. simpl. case X.compare_spec; auto. +Qed. + +(** * join *) + +Lemma join_in l x d r y : + y ∈ (join l x d r) <-> y == x \/ y ∈ l \/ y ∈ r. +Proof. + join_tac l x d r. + - simpl join. 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. + +Lemma join_bst l x d r : + Bst (create l x d r) -> Bst (join l x d r). +Proof. + join_tac l x d r; unfold create in *; + inv Bst; inv Above; inv Below; auto. + - simpl. auto. + - apply bal_bst; auto. + apply below. intro. rewrite join_in. intuition_in; order. + - apply bal_bst; auto. + apply above. intro. rewrite join_in. intuition_in; order. +Qed. +Hint Resolve join_bst. + +Lemma join_find l x d r y : + Bst (create l x d r) -> + find y (join l x d r) = find y (create l x d r). +Proof. + unfold create at 1. + join_tac l x d r; trivial. + - simpl in *. inv Bst. + rewrite add_find; trivial. + case X.compare_spec; intros; trivial. + apply not_find_iff; auto. intro. order. + - clear Hlr. factornode l. simpl. inv Bst. + rewrite add_find by auto. + case X.compare_spec; intros; trivial. + apply not_find_iff; auto. intro. order. + - clear Hrl LT. factornode r. inv Bst; inv Above; inv Below. + rewrite bal_find; auto; simpl. + + rewrite Hlr; auto; simpl. + repeat (case X.compare_spec; trivial; try order). + + apply below. intro. rewrite join_in. intuition_in; order. + - clear Hlr LT LT'. factornode l. inv Bst; inv Above; inv Below. + rewrite bal_find; auto; simpl. + + rewrite Hrl; auto; simpl. + repeat (case X.compare_spec; trivial; try order). + + apply above. intro. rewrite join_in. intuition_in; order. +Qed. + +(** * split *) + +Lemma split_in_l0 m x y : y ∈ (split x m)#l -> y ∈ m. +Proof. + functional induction (split x m); cleansplit; + rewrite ?join_in; intuition. +Qed. + +Lemma split_in_r0 m x y : y ∈ (split x m)#r -> y ∈ m. +Proof. + functional induction (split x m); cleansplit; + rewrite ?join_in; intuition. +Qed. + +Lemma split_in_l m x y : Bst m -> + (y ∈ (split x m)#l <-> y ∈ m /\ y < x). +Proof. + functional induction (split x m); intros; cleansplit; + rewrite ?join_in, ?IHt; intuition_in; order. +Qed. + +Lemma split_in_r m x y : Bst m -> + (y ∈ (split x m)#r <-> y ∈ m /\ x < y). +Proof. + functional induction (split x m); intros; cleansplit; + rewrite ?join_in, ?IHt; intuition_in; order. +Qed. + +Lemma split_in_o m x : (split x m)#o = find x m. +Proof. + functional induction (split x m); intros; cleansplit; auto. +Qed. + +Lemma split_lt_l m x : Bst m -> x >> (split x m)#l. +Proof. + intro. apply above. intro. rewrite split_in_l; intuition; order. +Qed. + +Lemma split_lt_r m x y : y >> m -> y >> (split x m)#r. +Proof. + intro. apply above. intros z Hz. apply split_in_r0 in Hz. order. +Qed. + +Lemma split_gt_r m x : Bst m -> x << (split x m)#r. +Proof. + intro. apply below. intro. rewrite split_in_r; intuition; order. +Qed. + +Lemma split_gt_l m x y : y << m -> y << (split x m)#l. +Proof. + intro. apply below. intros z Hz. apply split_in_l0 in Hz. order. +Qed. +Hint Resolve split_lt_l split_lt_r split_gt_l split_gt_r. + +Lemma split_bst_l m x : Bst m -> Bst (split x m)#l. +Proof. + functional induction (split x m); intros; cleansplit; intuition; + auto using join_bst. +Qed. + +Lemma split_bst_r m x : Bst m -> Bst (split x m)#r. +Proof. + functional induction (split x m); intros; cleansplit; intuition; + auto using join_bst. +Qed. +Hint Resolve split_bst_l split_bst_r. + +Lemma split_find m x y : Bst m -> + find y m = match X.compare y x with + | Eq => (split x m)#o + | Lt => find y (split x m)#l + | Gt => find y (split x m)#r + end. +Proof. + functional induction (split x m); intros; cleansplit. + - now case X.compare. + - repeat case X.compare_spec; trivial; order. + - simpl in *. rewrite join_find, IHt; auto. + simpl. repeat case X.compare_spec; trivial; order. + - rewrite join_find, IHt; auto. + simpl; repeat case X.compare_spec; trivial; order. +Qed. + +(** * Concatenation *) + +Lemma concat_in m1 m2 y : + y ∈ (concat m1 m2) <-> y ∈ m1 \/ y ∈ m2. +Proof. + functional induction (concat m1 m2); intros; try factornode m1. + - intuition_in. + - intuition_in. + - factor_remove_min m2 R. + rewrite join_in, (remove_min_in R); simpl; intuition. +Qed. + +Lemma concat_bst m1 m2 : Bst m1 -> Bst m2 -> m1 <<< m2 -> + Bst (concat m1 m2). +Proof. + functional induction (concat m1 m2); intros B1 B2 LT; auto; + try factornode m1. + factor_remove_min m2 R. + apply join_bst, create_bst; auto. + - now apply (remove_min_bst R). + - apply above. intros y Hy. apply LT; trivial. + rewrite (remove_min_in R); now left. + - now apply (remove_min_gt R). +Qed. +Hint Resolve concat_bst. + +Definition oelse {A} (o1 o2:option A) := + match o1 with + | Some x => Some x + | None => o2 + end. + +Lemma concat_find m1 m2 y : Bst m1 -> Bst m2 -> m1 <<< m2 -> + find y (concat m1 m2) = oelse (find y m2) (find y m1). +Proof. + functional induction (concat m1 m2); intros B1 B2 B; auto; try factornode m1. + - destruct (find y m2); auto. + - factor_remove_min m2 R. + assert (xd#1 >> m1). + { apply above. intros z Hz. apply B; trivial. + rewrite (remove_min_in R). now left. } + rewrite join_find; simpl; auto. + + rewrite (remove_min_find R B2 y). + case X.compare_spec; intros; auto. + destruct (find y m2'); trivial. + simpl. symmetry. apply not_find_iff; eauto. + + apply create_bst; auto. + * now apply (remove_min_bst R). + * now apply (remove_min_gt R). +Qed. + + +(** * Elements *) + +Notation eqk := (PX.eqk (elt:= elt)). +Notation eqke := (PX.eqke (elt:= elt)). +Notation ltk := (PX.ltk (elt:= elt)). + +Lemma bindings_aux_mapsto : forall (s:t elt) acc x e, + InA eqke (x,e) (bindings_aux acc s) <-> MapsTo x e s \/ InA eqke (x,e) acc. +Proof. + induction s as [ | l Hl x e r Hr h ]; simpl; auto. + intuition. + inversion H0. + intros. + rewrite Hl. + destruct (Hr acc x0 e0); clear Hl Hr. + intuition; inversion_clear H3; intuition. + compute in H0. destruct H0; simpl in *; subst; intuition. +Qed. + +Lemma bindings_mapsto : forall (s:t elt) x e, + InA eqke (x,e) (bindings s) <-> MapsTo x e s. +Proof. + intros; generalize (bindings_aux_mapsto s nil x e); intuition. + inversion_clear H0. +Qed. + +Lemma bindings_in : forall (s:t elt) x, L.PX.In x (bindings s) <-> x ∈ s. +Proof. + intros. + unfold L.PX.In. + rewrite <- In_alt; unfold In0. + split; intros (y,H); exists y. + - now rewrite <- bindings_mapsto. + - unfold L.PX.MapsTo; now rewrite bindings_mapsto. +Qed. + +Lemma bindings_aux_sort : forall (s:t elt) acc, + Bst s -> sort ltk acc -> + (forall x e y, InA eqke (x,e) acc -> y ∈ s -> y < x) -> + sort ltk (bindings_aux acc s). +Proof. + induction s as [ | l Hl y e r Hr h]; simpl; intuition. + inv Bst. + apply Hl; auto. + - constructor. + + apply Hr; eauto. + + clear Hl Hr. + apply InA_InfA with (eqA:=eqke); auto with *. + intros (y',e') Hy'. + apply bindings_aux_mapsto in Hy'. compute. intuition; eauto. + - clear Hl Hr. intros x e' y' Hx Hy'. + inversion_clear Hx. + + compute in H. destruct H; simpl in *. order. + + apply bindings_aux_mapsto in H. intuition eauto. +Qed. + +Lemma bindings_sort : forall s : t elt, Bst s -> sort ltk (bindings s). +Proof. + intros; unfold bindings; apply bindings_aux_sort; auto. + intros; inversion H0. +Qed. +Hint Resolve bindings_sort. + +Lemma bindings_nodup : forall s : t elt, Bst s -> NoDupA eqk (bindings s). +Proof. + intros; apply PX.Sort_NoDupA; auto. +Qed. + +Lemma bindings_aux_cardinal m acc : + (length acc + cardinal m)%nat = length (bindings_aux acc m). +Proof. + revert acc. induction m; simpl; intuition. + rewrite <- IHm1; simpl. + rewrite <- IHm2. rewrite Nat.add_succ_r, <- Nat.add_assoc. + f_equal. f_equal. apply Nat.add_comm. +Qed. + +Lemma bindings_cardinal m : cardinal m = length (bindings m). +Proof. + exact (bindings_aux_cardinal m nil). +Qed. + +Lemma bindings_app : + forall (s:t elt) acc, bindings_aux acc s = bindings s ++ acc. +Proof. + induction s; simpl; intros; auto. + rewrite IHs1, IHs2. + unfold bindings; simpl. + rewrite 2 IHs1, IHs2, !app_nil_r, !app_ass; auto. +Qed. + +Lemma bindings_node : + forall (t1 t2:t elt) x e z l, + bindings t1 ++ (x,e) :: bindings t2 ++ l = + bindings (Node t1 x e t2 z) ++ l. +Proof. + unfold bindings; simpl; intros. + rewrite !bindings_app, !app_nil_r, !app_ass; auto. +Qed. + +(** * Fold *) + +Definition fold' {A} (f : key -> elt -> A -> A)(s : t elt) := + L.fold f (bindings s). + +Lemma fold_equiv_aux {A} (s : t elt) (f : key -> elt -> A -> A) (a : A) acc : + L.fold f (bindings_aux acc s) a = L.fold f acc (fold f s a). +Proof. + revert a acc. + induction s; simpl; trivial. + intros. rewrite IHs1. simpl. apply IHs2. +Qed. + +Lemma fold_equiv {A} (s : t elt) (f : key -> elt -> A -> A) (a : A) : + fold f s a = fold' f s a. +Proof. + unfold fold', bindings. now rewrite fold_equiv_aux. +Qed. + +Lemma fold_spec (s:t elt)(Hs:Bst s){A}(i:A)(f : key -> elt -> A -> A) : + fold f s i = fold_left (fun a p => f p#1 p#2 a) (bindings s) i. +Proof. + rewrite fold_equiv. unfold fold'. now rewrite L.fold_spec. +Qed. + +(** * Comparison *) + +(** [flatten_e e] returns the list of bindings of the enumeration [e] + i.e. the list of bindings actually compared *) + +Fixpoint flatten_e (e : enumeration elt) : list (key*elt) := match e with + | End _ => nil + | More x e t r => (x,e) :: bindings t ++ flatten_e r + end. + +Lemma flatten_e_bindings : + forall (l:t elt) r x d z e, + bindings l ++ flatten_e (More x d r e) = + bindings (Node l x d r z) ++ flatten_e e. +Proof. + intros; apply bindings_node. +Qed. + +Lemma cons_1 : forall (s:t elt) e, + flatten_e (cons s e) = bindings s ++ flatten_e e. +Proof. + induction s; auto; intros. + simpl flatten_e; rewrite IHs1; apply flatten_e_bindings; auto. +Qed. + +(** 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. + unfold IfEq; destruct b; simpl; intros; case X.compare_spec; simpl; + try rewrite H0; auto; order. +Qed. + +Lemma equal_end_IfEq : forall e2, + IfEq (equal_end e2) nil (flatten_e e2). +Proof. + destruct e2; red; auto. +Qed. + +Lemma equal_more_IfEq : + forall x1 d1 (cont:enumeration elt -> bool) x2 d2 r2 e2 l, + IfEq (cont (cons r2 e2)) l (bindings 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. + unfold IfEq; simpl; intros; destruct X.compare; simpl; auto. + rewrite <-andb_lazy_alt; f_equal; auto. +Qed. + +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) (bindings m1 ++ l) (flatten_e e2). +Proof. + induction m1 as [|l1 Hl1 x1 d1 r1 Hr1 h1]; intros; auto. + rewrite <- bindings_node; simpl. + apply Hl1; auto. + clear e2; intros [|x2 d2 r2 e2]. + simpl; red; auto. + apply equal_more_IfEq. + rewrite <- cons_1; auto. +Qed. + +Lemma equal_IfEq : forall (m1 m2:t elt), + IfEq (equal cmp m1 m2) (bindings m1) (bindings m2). +Proof. + intros; unfold equal. + rewrite <- (app_nil_r (bindings m1)). + replace (bindings m2) with (flatten_e (cons m2 (End _))) + by (rewrite cons_1; simpl; rewrite app_nil_r; auto). + apply equal_cont_IfEq. + intros. + apply equal_end_IfEq; auto. +Qed. + +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). + +Lemma Equivb_bindings : forall s s', + Equivb s s' <-> L.Equivb cmp (bindings s) (bindings s'). +Proof. +unfold Equivb, L.Equivb; split; split; intros. +do 2 rewrite bindings_in; firstorder. +destruct H. +apply (H2 k); rewrite <- bindings_mapsto; auto. +do 2 rewrite <- bindings_in; firstorder. +destruct H. +apply (H2 k); unfold L.PX.MapsTo; rewrite bindings_mapsto; auto. +Qed. + +Lemma equal_Equivb : forall (s s': t elt), Bst s -> Bst s' -> + (equal cmp s s' = true <-> Equivb s s'). +Proof. + intros s s' B B'. + rewrite Equivb_bindings, <- equal_IfEq. + split; [apply L.equal_2|apply L.equal_1]; auto. +Qed. + +End Elt. + +Section Map. +Variable elt elt' : Type. +Variable f : elt -> elt'. + +Lemma map_spec m x : + find x (map f m) = option_map f (find x m). +Proof. +induction m; simpl; trivial. case X.compare_spec; auto. +Qed. + +Lemma map_in m x : x ∈ (map f m) <-> x ∈ m. +Proof. +induction m; simpl; intuition_in. +Qed. + +Lemma map_bst m : Bst m -> Bst (map f m). +Proof. +induction m; simpl; auto. intros; inv Bst; constructor; auto. +- apply above. intro. rewrite map_in. intros. order. +- apply below. intro. rewrite map_in. intros. order. +Qed. + +End Map. +Section Mapi. +Variable elt elt' : Type. +Variable f : key -> elt -> elt'. + +Lemma mapi_spec m x : + exists y:key, + X.eq y x /\ find x (mapi f m) = option_map (f y) (find x m). +Proof. + induction m; simpl. + - now exists x. + - case X.compare_spec; simpl; auto. intros. now exists k. +Qed. + +Lemma mapi_in m x : x ∈ (mapi f m) <-> x ∈ m. +Proof. +induction m; simpl; intuition_in. +Qed. + +Lemma mapi_bst m : Bst m -> Bst (mapi f m). +Proof. +induction m; simpl; auto. intros; inv Bst; constructor; auto. +- apply above. intro. rewrite mapi_in. intros. order. +- apply below. intro. rewrite mapi_in. intros. order. +Qed. + +End Mapi. + +Section Mapo. +Variable elt elt' : Type. +Variable f : key -> elt -> option elt'. + +Lemma mapo_in m x : + x ∈ (mapo f m) -> + exists y d, X.eq y x /\ MapsTo x d m /\ f y d <> None. +Proof. +functional induction (mapo f m); simpl; auto; intro H. +- inv In. +- rewrite join_in in H; destruct H as [H|[H|H]]. + + exists x0, d. do 2 (split; auto). congruence. + + destruct (IHt H) as (y & e & ? & ? & ?). exists y, e. auto. + + destruct (IHt0 H) as (y & e & ? & ? & ?). exists y, e. auto. +- rewrite concat_in in H; destruct H as [H|H]. + + destruct (IHt H) as (y & e & ? & ? & ?). exists y, e. auto. + + destruct (IHt0 H) as (y & e & ? & ? & ?). exists y, e. auto. +Qed. + +Lemma mapo_lt m x : x >> m -> x >> mapo f m. +Proof. + intros H. apply above. intros y Hy. + destruct (mapo_in Hy) as (y' & e & ? & ? & ?). order. +Qed. + +Lemma mapo_gt m x : x << m -> x << mapo f m. +Proof. + intros H. apply below. intros y Hy. + destruct (mapo_in Hy) as (y' & e & ? & ? & ?). order. +Qed. +Hint Resolve mapo_lt mapo_gt. + +Lemma mapo_bst m : Bst m -> Bst (mapo f m). +Proof. +functional induction (mapo f m); simpl; auto; intro H; inv Bst. +- apply join_bst, create_bst; auto. +- apply concat_bst; auto. apply between with x; auto. +Qed. +Hint Resolve mapo_bst. + +Ltac nonify e := + replace e with (@None elt) by + (symmetry; rewrite not_find_iff; auto; intro; order). + +Definition obind {A B} (o:option A) (f:A->option B) := + match o with Some a => f a | None => None end. + +Lemma mapo_find m x : + Bst m -> + exists y, X.eq y x /\ + find x (mapo f m) = obind (find x m) (f y). +Proof. +functional induction (mapo f m); simpl; auto; intros B; + inv Bst. +- now exists x. +- rewrite join_find; auto. + + simpl. case X.compare_spec; simpl; intros. + * now exists x0. + * destruct IHt as (y' & ? & ?); auto. + exists y'; split; trivial. + * destruct IHt0 as (y' & ? & ?); auto. + exists y'; split; trivial. + + constructor; auto using mapo_lt, mapo_gt. +- rewrite concat_find; auto. + + destruct IHt0 as (y' & ? & ->); auto. + destruct IHt as (y'' & ? & ->); auto. + case X.compare_spec; simpl; intros. + * nonify (find x r). nonify (find x l). simpl. now exists x0. + * nonify (find x r). now exists y''. + * nonify (find x l). exists y'. split; trivial. + destruct (find x r); simpl; trivial. + now destruct (f y' e). + + apply between with x0; auto. +Qed. + +End Mapo. + +Section Gmerge. +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 -> + exists y, X.eq y x /\ + find x (mapl m) = obind (find x m) (fun d => f0 y (Some d) None). +Hypothesis mapr_f0 : forall x m, Bst m -> + exists y, X.eq y x /\ + find x (mapr m) = obind (find x m) (fun d => f0 y None (Some d)). + +Notation gmerge := (gmerge f mapl mapr). + +Lemma gmerge_in m m' y : Bst m -> Bst m' -> + y ∈ (gmerge m m') -> y ∈ m \/ y ∈ m'. +Proof. + functional induction (gmerge m m'); intros B1 B2 H; + try factornode m2; inv Bst. + - right. apply find_in. + generalize (in_find (mapr_bst B2) H). + destruct (@mapr_f0 y m2) as (y' & ? & ->); trivial. + intros A B. rewrite B in A. now elim A. + - left. apply find_in. + generalize (in_find (mapl_bst B1) H). + destruct (@mapl_f0 y m2) as (y' & ? & ->); trivial. + intros A B. rewrite B in A. now elim A. + - rewrite join_in in *. revert IHt1 IHt0 H. cleansplit. + generalize (split_bst_l x1 B2) (split_bst_r x1 B2). + rewrite split_in_r, split_in_l; intuition_in. + - rewrite concat_in in *. revert IHt1 IHt0 H; cleansplit. + generalize (split_bst_l x1 B2) (split_bst_r x1 B2). + rewrite split_in_r, split_in_l; intuition_in. +Qed. + +Lemma gmerge_lt m m' x : Bst m -> Bst m' -> + x >> m -> x >> m' -> x >> gmerge m m'. +Proof. + intros. apply above. intros y Hy. + apply gmerge_in in Hy; intuition_in; order. +Qed. + +Lemma gmerge_gt m m' x : Bst m -> Bst m' -> + x << m -> x << m' -> x << gmerge m m'. +Proof. + intros. apply below. intros y Hy. + apply gmerge_in in Hy; intuition_in; order. +Qed. +Hint Resolve gmerge_lt gmerge_gt. +Hint Resolve split_bst_l split_bst_r split_lt_l split_gt_r. + +Lemma gmerge_bst m m' : Bst m -> Bst m' -> Bst (gmerge m m'). +Proof. + functional induction (gmerge m m'); intros B1 B2; auto; + factornode m2; inv Bst; + (apply join_bst, create_bst || apply concat_bst); + revert IHt1 IHt0; cleansplit; intuition. + apply between with x1; auto. +Qed. +Hint Resolve gmerge_bst. + +Lemma oelse_none_r {A} (o:option A) : oelse o None = o. +Proof. now destruct o. Qed. + +Ltac nonify e := + let E := fresh "E" in + assert (E : e = None); + [ rewrite not_find_iff; auto; intro U; + try apply gmerge_in in U; intuition_in; order + | rewrite E; clear E ]. + +Lemma gmerge_find m m' x : Bst m -> Bst m' -> + In x m \/ In x m' -> + exists y, X.eq y x /\ + find x (gmerge m m') = f0 y (find x m) (find x m'). +Proof. + functional induction (gmerge m m'); intros B1 B2 H; + try factornode m2; inv Bst. + - destruct H; [ intuition_in | ]. + destruct (@mapr_f0 x m2) as (y,(Hy,E)); trivial. + exists y; split; trivial. + rewrite E. simpl. apply in_find in H; trivial. + destruct (find x m2); simpl; intuition. + - destruct H; [ | intuition_in ]. + destruct (@mapl_f0 x m2) as (y,(Hy,E)); trivial. + exists y; split; trivial. + rewrite E. simpl. apply in_find in H; trivial. + destruct (find x m2); simpl; intuition. + - generalize (split_bst_l x1 B2) (split_bst_r x1 B2). + rewrite (split_find x1 x B2). + rewrite e1 in *; simpl in *. intros. + rewrite join_find by (cleansplit; constructor; auto). + simpl. case X.compare_spec; intros. + + exists x1. split; auto. now rewrite <- e3, f0_f. + + apply IHt1; auto. clear IHt1 IHt0. + cleansplit; rewrite split_in_l; trivial. + intuition_in; order. + + apply IHt0; auto. clear IHt1 IHt0. + cleansplit; rewrite split_in_r; trivial. + intuition_in; order. + - generalize (split_bst_l x1 B2) (split_bst_r x1 B2). + rewrite (split_find x1 x B2). + pose proof (split_lt_l x1 B2). + pose proof (split_gt_r x1 B2). + rewrite e1 in *; simpl in *. intros. + rewrite concat_find by (try apply between with x1; auto). + case X.compare_spec; intros. + + clear IHt0 IHt1. + exists x1. split; auto. rewrite <- f0_f, e2. + nonify (find x (gmerge r1 r2')). + nonify (find x (gmerge l1 l2')). trivial. + + nonify (find x (gmerge r1 r2')). + simpl. apply IHt1; auto. clear IHt1 IHt0. + intuition_in; try order. + right. cleansplit. now apply split_in_l. + + nonify (find x (gmerge l1 l2')). simpl. + rewrite oelse_none_r. + apply IHt0; auto. clear IHt1 IHt0. + intuition_in; try order. + right. cleansplit. now apply split_in_r. +Qed. + +End Gmerge. + +Section Merge. +Variable elt elt' elt'' : Type. +Variable f : key -> option elt -> option elt' -> option elt''. + +Lemma merge_bst m m' : Bst m -> Bst m' -> Bst (merge f m m'). +Proof. +unfold merge; intros. +apply gmerge_bst with f; + auto using mapo_bst, mapo_find. +Qed. + +Lemma merge_spec1 m m' x : Bst m -> Bst m' -> + In x m \/ In x m' -> + exists y, X.eq y x /\ + find x (merge f m m') = f y (find x m) (find x m'). +Proof. + unfold merge; intros. + edestruct (gmerge_find (f0:=f)) as (y,(Hy,E)); + eauto using mapo_bst. + - reflexivity. + - intros. now apply mapo_find. + - intros. now apply mapo_find. +Qed. + +Lemma merge_spec2 m m' x : Bst m -> Bst m' -> + In x (merge f m m') -> In x m \/ In x m'. +Proof. +unfold merge; intros. +eapply gmerge_in with (f0:=f); try eassumption; + auto using mapo_bst, mapo_find. +Qed. + +End Merge. +End Proofs. +End Raw. + +(** * Encapsulation + + Now, in order to really provide a functor implementing [S], we + need to encapsulate everything into a type of balanced binary search trees. *) + +Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. + + Module E := X. + Module Raw := Raw I X. + Import Raw.Proofs. + + Record tree (elt:Type) := + Mk {this :> Raw.tree elt; is_bst : Raw.Bst this}. + + Definition t := tree. + Definition key := E.t. + + Section Elt. + Variable elt elt' elt'': Type. + + Implicit Types m : t elt. + Implicit Types x y : key. + Implicit Types e : elt. + + Definition empty : t elt := Mk (empty_bst elt). + Definition is_empty m : bool := Raw.is_empty m.(this). + Definition add x e m : t elt := Mk (add_bst x e m.(is_bst)). + Definition remove x m : t elt := Mk (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' := Mk (map_bst f m.(is_bst)). + Definition mapi (f:key->elt->elt') m : t elt' := + Mk (mapi_bst f m.(is_bst)). + Definition merge f m (m':t elt') : t elt'' := + Mk (merge_bst f m.(is_bst) m'.(is_bst)). + Definition bindings m : list (key*elt) := Raw.bindings m.(this). + Definition cardinal m := Raw.cardinal m.(this). + Definition fold {A} (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 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. + + Instance MapsTo_compat : + Proper (E.eq==>Logic.eq==>Logic.eq==>iff) MapsTo. + Proof. + intros k k' Hk e e' He m m' Hm. unfold MapsTo; simpl. + now rewrite Hk, He, Hm. + Qed. + + Lemma find_spec m x e : find x m = Some e <-> MapsTo x e m. + Proof. apply find_spec. apply is_bst. Qed. + + Lemma mem_spec m x : mem x m = true <-> In x m. + Proof. + unfold In, mem; rewrite In_alt. apply mem_spec. apply is_bst. + Qed. + + Lemma empty_spec x : find x empty = None. + Proof. apply empty_spec. Qed. + + Lemma is_empty_spec m : is_empty m = true <-> forall x, find x m = None. + Proof. apply is_empty_spec. Qed. + + Lemma add_spec1 m x e : find x (add x e m) = Some e. + Proof. apply add_spec1. apply is_bst. Qed. + Lemma add_spec2 m x y e : ~ E.eq x y -> find y (add x e m) = find y m. + Proof. apply add_spec2. apply is_bst. Qed. + + Lemma remove_spec1 m x : find x (remove x m) = None. + Proof. apply remove_spec1. apply is_bst. Qed. + Lemma remove_spec2 m x y : ~E.eq x y -> find y (remove x m) = find y m. + Proof. apply remove_spec2. apply is_bst. Qed. + + Lemma bindings_spec1 m x e : + InA eq_key_elt (x,e) (bindings m) <-> MapsTo x e m. + Proof. apply bindings_mapsto. Qed. + + Lemma bindings_spec2 m : sort lt_key (bindings m). + Proof. apply bindings_sort. apply is_bst. Qed. + + Lemma bindings_spec2w m : NoDupA eq_key (bindings m). + Proof. apply bindings_nodup. apply is_bst. Qed. + + Lemma fold_spec m {A} (i : A) (f : key -> elt -> A -> A) : + fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (bindings m) i. + Proof. apply fold_spec. apply is_bst. Qed. + + Lemma cardinal_spec m : cardinal m = length (bindings m). + Proof. apply bindings_cardinal. 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' -> eq_elt e e'). + Definition Equivb cmp := Equiv (Cmp cmp). + + Lemma Equivb_Equivb cmp m m' : + Equivb cmp m m' <-> Raw.Proofs.Equivb cmp m m'. + Proof. + 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_spec m m' cmp : + equal cmp m m' = true <-> Equivb cmp m m'. + Proof. rewrite Equivb_Equivb. apply equal_Equivb; apply is_bst. Qed. + + End Elt. + + Lemma map_spec {elt elt'} (f:elt->elt') m x : + find x (map f m) = option_map f (find x m). + Proof. apply map_spec. Qed. + + Lemma mapi_spec {elt elt'} (f:key->elt->elt') m x : + exists y:key, E.eq y x /\ find x (mapi f m) = option_map (f y) (find x m). + Proof. apply mapi_spec. Qed. + + Lemma merge_spec1 {elt elt' elt''} + (f:key->option elt->option elt'->option elt'') m m' x : + In x m \/ In x m' -> + exists y:key, E.eq y x /\ + find x (merge f m m') = f y (find x m) (find x m'). + Proof. + unfold In. rewrite !In_alt. apply merge_spec1; apply is_bst. + Qed. + + Lemma merge_spec2 {elt elt' elt''} + (f:key -> option elt->option elt'->option elt'') m m' x : + In x (merge f m m') -> In x m \/ In x m'. + Proof. + unfold In. rewrite !In_alt. apply merge_spec2; apply is_bst. + Qed. + +End IntMake. + + +Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: + Sord with Module Data := D + with Module MapS.E := X. + + Module Data := D. + Module Import MapS := IntMake(I)(X). + Module LO := MMapList.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 bindings *) + + 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. + + (** Comparison of left tree, middle element, then right tree *) + + 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 compare m1 m2 := + compare_cont m1.(this) compare_end (R.cons m2 .(this) (Raw.End _)). + + (** Correctness of this comparison *) + + 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 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; case X.compare_spec; auto; try P.MX.order. + intros. right. split; auto. now symmetry. + Qed. + Hint Resolve cons_Cmp. + + Lemma compare_end_Cmp e2 : + Cmp (compare_end e2) nil (P.flatten_e e2). + Proof. + destruct e2; simpl; auto. + Qed. + + Lemma compare_more_Cmp x1 d1 cont x2 d2 r2 e2 l : + Cmp (cont (R.cons r2 e2)) l (R.bindings 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; case X.compare_spec; simpl; + try case D.compare_spec; simpl; auto; + case X.compare_spec; try P.MX.order; 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.bindings s1 ++ l) (P.flatten_e e2). + Proof. + induction s1 as [|l1 Hl1 x1 d1 r1 Hr1 h1] using P.tree_ind; + intros; auto. + rewrite <- P.bindings_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 m1 m2 : + Cmp (compare m1 m2) (bindings m1) (bindings m2). + Proof. + destruct m1 as (s1,H1), m2 as (s2,H2). + unfold compare, bindings; simpl. + rewrite <- (app_nil_r (R.bindings s1)). + replace (R.bindings s2) with (P.flatten_e (R.cons s2 (R.End _))) by + (rewrite P.cons_1; simpl; rewrite app_nil_r; auto). + auto using compare_cont_Cmp, compare_end_Cmp. + Qed. + + Definition eq (m1 m2 : t) := LO.eq_list (bindings m1) (bindings m2). + Definition lt (m1 m2 : t) := LO.lt_list (bindings m1) (bindings m2). + + Lemma compare_spec m1 m2 : CompSpec eq lt m1 m2 (compare m1 m2). + Proof. + assert (H := compare_Cmp m1 m2). + unfold Cmp in H. + destruct (compare m1 m2); auto. + Qed. + + (* Proofs about [eq] and [lt] *) + + Definition sbindings (m1 : t) := + LO.MapS.Mk (P.bindings_sort m1.(is_bst)). + + Definition seq (m1 m2 : t) := LO.eq (sbindings m1) (sbindings m2). + Definition slt (m1 m2 : t) := LO.lt (sbindings m1) (sbindings m2). + + Lemma eq_seq : forall m1 m2, eq m1 m2 <-> seq m1 m2. + Proof. + unfold eq, seq, sbindings, bindings, LO.eq; intuition. + Qed. + + Lemma lt_slt : forall m1 m2, lt m1 m2 <-> slt m1 m2. + Proof. + unfold lt, slt, sbindings, bindings, LO.lt; intuition. + Qed. + + Lemma eq_spec m m' : eq m m' <-> Equivb cmp m m'. + Proof. + rewrite eq_seq; unfold seq. + rewrite Equivb_Equivb. + rewrite P.Equivb_bindings. apply LO.eq_spec. + Qed. + + Instance eq_equiv : Equivalence eq. + Proof. + constructor; red; [intros x|intros x y| intros x y z]; + rewrite !eq_seq; apply LO.eq_equiv. + Qed. + + Instance lt_compat : Proper (eq ==> eq ==> iff) lt. + Proof. + intros m1 m2 H1 m1' m2' H2. rewrite !lt_slt. rewrite eq_seq in *. + now apply LO.lt_compat. + Qed. + + Instance lt_strorder : StrictOrder lt. + Proof. + constructor; red; [intros x; red|intros x y z]; + rewrite !lt_slt; apply LO.lt_strorder. + Qed. + +End IntMake_ord. + +(* For concrete use inside Coq, we propose an instantiation of [Int] by [Z]. *) + +Module Make (X: OrderedType) <: S with Module E := X + :=IntMake(Z_as_Int)(X). + +Module Make_ord (X: OrderedType)(D: OrderedType) + <: Sord with Module Data := D + with Module MapS.E := X + :=IntMake_ord(Z_as_Int)(X)(D). |