diff options
Diffstat (limited to 'theories/MMaps/MMapAVL.v')
| -rw-r--r-- | theories/MMaps/MMapAVL.v | 2158 |
1 files changed, 0 insertions, 2158 deletions
diff --git a/theories/MMaps/MMapAVL.v b/theories/MMaps/MMapAVL.v deleted file mode 100644 index d840f1f3..00000000 --- a/theories/MMaps/MMapAVL.v +++ /dev/null @@ -1,2158 +0,0 @@ -(***********************************************************************) -(* 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). |