diff options
Diffstat (limited to 'theories/FSets/FMapAVL.v')
-rw-r--r-- | theories/FSets/FMapAVL.v | 681 |
1 files changed, 340 insertions, 341 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 8cb1236e..8158324e 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -1,4 +1,3 @@ - (***********************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) @@ -9,13 +8,13 @@ (* Finite map library. *) -(* $Id: FMapAVL.v 11033 2008-06-01 22:56:50Z letouzey $ *) +(* $Id$ *) (** * FMapAVL *) (** This module implements maps using AVL trees. - It follows the implementation from Ocaml's standard library. - + It follows the implementation from Ocaml's standard library. + See the comments at the beginning of FSetAVL for more details. *) @@ -30,8 +29,8 @@ 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 + + Functor of pure functions + separate proofs of invariant preservation *) Module Raw (Import I:Int)(X: OrderedType). @@ -85,20 +84,20 @@ Definition is_empty m := match m with Leaf => true | _ => false end. to achieve logarithmic complexity. *) Fixpoint mem x m : bool := - match m with - | Leaf => false - | Node l y _ r _ => match X.compare x y with - | LT _ => mem x l + match m with + | Leaf => false + | Node l y _ r _ => match X.compare x y with + | LT _ => mem x l | EQ _ => true | GT _ => mem x r end end. -Fixpoint find x m : option elt := - match m with - | Leaf => None - | Node l y d r _ => match X.compare x y with - | LT _ => find x l +Fixpoint find x m : option elt := + match m with + | Leaf => None + | Node l y d r _ => match X.compare x y with + | LT _ => find x l | EQ _ => Some d | GT _ => find x r end @@ -109,7 +108,7 @@ Fixpoint find x m : option elt := (** [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 := +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 @@ -117,45 +116,45 @@ Definition create l x e r := Definition assert_false := create. -Fixpoint bal l x d r := - let hl := height l in +Fixpoint bal l x d r := + let hl := height l in let hr := height r in - if gt_le_dec hl (hr+2) then - match l with + if gt_le_dec hl (hr+2) then + match l with | Leaf => assert_false l x d r - | Node ll lx ld lr _ => - if ge_lt_dec (height ll) (height lr) then + | Node ll lx ld lr _ => + if ge_lt_dec (height ll) (height lr) then create ll lx ld (create lr x d r) - else - match lr with + else + match lr with | Leaf => assert_false l x d r - | Node lrl lrx lrd lrr _ => + | Node lrl lrx lrd lrr _ => create (create ll lx ld lrl) lrx lrd (create lrr x d r) end end - else - if gt_le_dec hr (hl+2) then + else + if gt_le_dec hr (hl+2) then match r with | Leaf => assert_false l x d r | Node rl rx rd rr _ => - if ge_lt_dec (height rr) (height rl) then + if ge_lt_dec (height rr) (height rl) then create (create l x d rl) rx rd rr - else + 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) + | Node rll rlx rld rlr _ => + create (create l x d rll) rlx rld (create rlr rx rd rr) end end - else + else create l x d r. (** * Insertion *) -Fixpoint add x d m := - match m with +Fixpoint add x d m := + match m with | Leaf => Node Leaf x d Leaf 1 - | Node l y d' r h => + | Node l y d' r h => match X.compare x y with | LT _ => bal (add x d l) y d' r | EQ _ => Node l y d r h @@ -165,16 +164,16 @@ Fixpoint add x d m := (** * 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]). + 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) := + +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 + | Node ll lx ld lr lh => + let (l',m) := remove_min ll lx ld lr in (bal l' x d r, m) end. @@ -185,18 +184,18 @@ Fixpoint remove_min l x d r : t*(key*elt) := [|height t1 - height t2| <= 2]. *) -Fixpoint merge s1 s2 := match s1,s2 with - | Leaf, _ => s2 +Fixpoint merge s1 s2 := match s1,s2 with + | Leaf, _ => s2 | _, Leaf => s1 - | _, Node l2 x2 d2 r2 h2 => - match remove_min l2 x2 d2 r2 with + | _, Node l2 x2 d2 r2 h2 => + match remove_min l2 x2 d2 r2 with (s2',(x,d)) => bal s1 x d s2' end end. (** * Deletion *) -Fixpoint remove x m := match m with +Fixpoint remove x m := match m with | Leaf => Leaf | Node l y d r h => match X.compare x y with @@ -206,26 +205,26 @@ Fixpoint remove x m := match m with end end. -(** * join - - Same as [bal] but does not assume anything regarding heights of [l] +(** * 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 + | 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 => + | Node rl rx rd rr rh => if gt_le_dec lh (rh+2) then bal ll lx ld (join lr x d r) - else if gt_le_dec rh (lh+2) then bal (join_aux rl) rx rd rr + else if gt_le_dec rh (lh+2) then bal (join_aux rl) rx rd rr else create l x d r end end. -(** * Splitting +(** * Splitting [split x m] returns a triple [(l, o, r)] where - [l] is the set of elements of [m] that are [< x] @@ -236,17 +235,17 @@ Fixpoint join l : key -> elt -> t -> t := 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 +Fixpoint split x m : triple := match m with | Leaf => << Leaf, None, Leaf >> - | Node l y d r h => - match X.compare x y with + | 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 +(** * Concatenation Same as [merge] but does not assume anything about heights. *) @@ -256,7 +255,7 @@ Definition concat m1 m2 := | Leaf, _ => m2 | _ , Leaf => m1 | _, Node l2 x2 d2 r2 _ => - let (m2',xd) := remove_min l2 x2 d2 r2 in + let (m2',xd) := remove_min l2 x2 d2 r2 in join m1 xd#1 xd#2 m2' end. @@ -277,7 +276,7 @@ Definition elements := elements_aux nil. (** * Fold *) -Fixpoint fold (A : Type) (f : key -> elt -> A -> A) (m : t) : A -> A := +Fixpoint fold (A : Type) (f : key -> elt -> A -> A) (m : t) : A -> A := fun a => match m with | Leaf => a | Node l x d r _ => fold f r (f x d (fold f l a)) @@ -293,11 +292,11 @@ Inductive enumeration := | End : enumeration | More : key -> elt -> t -> enumeration -> enumeration. -(** [cons m e] adds the elements of tree [m] on the head of +(** [cons m e] adds the elements of tree [m] on the head of enumeration [e]. *) -Fixpoint cons m e : enumeration := - match m with +Fixpoint cons m e : enumeration := + match m with | Leaf => e | Node l x d r h => cons l (More x d r e) end. @@ -316,7 +315,7 @@ Definition equal_more x1 d1 (cont:enumeration->bool) e2 := (** Comparison of left tree, middle element, then right tree *) -Fixpoint equal_cont m1 (cont:enumeration->bool) e2 := +Fixpoint equal_cont m1 (cont:enumeration->bool) e2 := match m1 with | Leaf => cont e2 | Node l1 x1 d1 r1 _ => @@ -341,8 +340,8 @@ 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 +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. @@ -350,7 +349,7 @@ Fixpoint map (elt elt' : Type)(f : elt -> elt')(m : t elt) : t elt' := (* * Mapi *) Fixpoint mapi (elt elt' : Type)(f : key -> elt -> elt')(m : t elt) : t elt' := - match m with + match m with | Leaf => Leaf _ | Node l x d r h => Node (mapi f l) x (f x d) (mapi f r) h end. @@ -358,28 +357,28 @@ Fixpoint mapi (elt elt' : Type)(f : key -> elt -> elt')(m : t elt) : t elt' := (** * Map with removal *) Fixpoint map_option (elt elt' : Type)(f : key -> elt -> option elt')(m : t elt) - : t elt' := - match m with + : t elt' := + match m with | Leaf => Leaf _ - | Node l x d r h => - match f x d with + | Node l x d r h => + match f x d with | Some d' => join (map_option f l) x d' (map_option f r) | None => concat (map_option f l) (map_option f r) end end. (** * Optimized map2 - - Suggestion by B. Gregoire: a [map2] function with specialized - arguments allowing to bypass some tree traversal. Instead of one - [f0] of type [key -> option elt -> option elt' -> option elt''], - we ask here for: + + Suggestion by B. Gregoire: a [map2] function with specialized + arguments allowing to bypass some tree traversal. Instead of one + [f0] of type [key -> option elt -> option elt' -> option elt''], + we ask here for: - [f] which is a specialisation of [f0] when first option isn't [None] - [mapl] treats a [tree elt] with [f0] when second option is [None] - [mapr] treats a [tree elt'] with [f0] when first option is [None] - The idea is that [mapl] and [mapr] can be instantaneous (e.g. - the identity or some constant function). + The idea is that [mapl] and [mapr] can be instantaneous (e.g. + the identity or some constant function). *) Section Map2_opt. @@ -388,13 +387,13 @@ Variable f : key -> elt -> option elt' -> option elt''. Variable mapl : t elt -> t elt''. Variable mapr : t elt' -> t elt''. -Fixpoint map2_opt m1 m2 := - match m1, m2 with - | Leaf, _ => mapr m2 +Fixpoint map2_opt m1 m2 := + match m1, m2 with + | Leaf, _ => mapr m2 | _, Leaf => mapl m1 - | Node l1 x1 d1 r1 h1, _ => + | Node l1 x1 d1 r1 h1, _ => let (l2',o2,r2') := split x1 m2 in - match f x1 d1 o2 with + match f x1 d1 o2 with | Some e => join (map2_opt l1 l2') x1 e (map2_opt r1 r2') | None => concat (map2_opt l1 l2') (map2_opt r1 r2') end @@ -403,8 +402,8 @@ Fixpoint map2_opt m1 m2 := End Map2_opt. (** * Map2 - - The [map2] function of the Map interface can be implemented + + The [map2] function of the Map interface can be implemented via [map2_opt] and [map_option]. *) @@ -412,8 +411,8 @@ Section Map2. Variable elt elt' elt'' : Type. Variable f : option elt -> option elt' -> option elt''. -Definition map2 : t elt -> t elt' -> t elt'' := - map2_opt +Definition map2 : t elt -> t elt' -> t elt'' := + map2_opt (fun _ d o => f (Some d) o) (map_option (fun _ d => f (Some d) None)) (map_option (fun _ d' => f None (Some d'))). @@ -432,24 +431,24 @@ Variable elt : Type. 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', + | 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', + | 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', + | 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', + | 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 *) -(** [lt_tree x s]: all elements in [s] are smaller than [x] +(** [lt_tree x s]: all elements in [s] are smaller than [x] (resp. greater for [gt_tree]) *) Definition lt_tree x m := forall y, In y m -> X.lt y x. @@ -459,7 +458,7 @@ Definition gt_tree x m := forall y, In y m -> X.lt x y. Inductive bst : t elt -> Prop := | BSLeaf : bst (Leaf _) - | BSNode : forall x e l r h, bst l -> bst r -> + | BSNode : forall x e l r h, bst l -> bst r -> lt_tree x l -> gt_tree x r -> bst (Node l x e r h). End Invariants. @@ -474,10 +473,10 @@ Module Proofs. 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 bal_ind := Induction for bal Sort Prop. Functional Scheme add_ind := Induction for add Sort Prop. Functional Scheme remove_min_ind := Induction for remove_min Sort Prop. -Functional Scheme merge_ind := Induction for merge Sort Prop. +Functional Scheme merge_ind := Induction for merge Sort Prop. Functional Scheme remove_ind := Induction for remove Sort Prop. Functional Scheme concat_ind := Induction for concat Sort Prop. Functional Scheme split_ind := Induction for split Sort Prop. @@ -489,24 +488,24 @@ Functional Scheme map2_opt_ind := Induction for map2_opt Sort Prop. Hint Constructors tree MapsTo In bst. Hint Unfold lt_tree gt_tree. -Tactic Notation "factornode" ident(l) ident(x) ident(d) ident(r) ident(h) - "as" ident(s) := +Tactic Notation "factornode" ident(l) ident(x) ident(d) ident(r) ident(h) + "as" ident(s) := set (s:=Node l x d r h) in *; clearbody s; clear l x d r h. (** A tactic for cleaning hypothesis after use of functional induction. *) Ltac clearf := - match goal with + match goal with | H : (@Logic.eq (Compare _ _ _ _) _ _) |- _ => clear H; clearf | H : (@Logic.eq (sumbool _ _) _ _) |- _ => clear H; clearf | _ => idtac end. -(** A tactic to repeat [inversion_clear] on all hyps of the +(** A tactic to repeat [inversion_clear] on all hyps of the form [(f (Node ...))] *) Ltac inv f := - match goal with + 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 @@ -518,8 +517,8 @@ Ltac inv f := | _ => idtac end. -Ltac inv_all f := - match goal with +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 @@ -529,7 +528,7 @@ Ltac inv_all f := (** Helper tactic concerning order of elements. *) -Ltac order := match goal with +Ltac order := match goal with | U: lt_tree _ ?s, V: In _ ?s |- _ => generalize (U _ V); clear U; order | U: gt_tree _ ?s, V: In _ ?s |- _ => generalize (U _ V); clear U; order | _ => MX.order @@ -537,21 +536,21 @@ end. Ltac intuition_in := repeat progress (intuition; inv In; inv MapsTo). -(* Function/Functional Scheme can't deal with internal fix. +(* Function/Functional Scheme can't deal with internal fix. Let's do its job by hand: *) -Ltac join_tac := - intros l; induction l as [| ll _ lx ld lr Hlr lh]; +Ltac join_tac := + intros l; induction l as [| ll _ lx ld lr Hlr lh]; [ | intros x d r; induction r as [| rl Hrl rx rd rr _ rh]; unfold join; - [ | destruct (gt_le_dec lh (rh+2)); + [ | destruct (gt_le_dec lh (rh+2)); [ match goal with |- context [ bal ?u ?v ?w ?z ] => - replace (bal u v w z) + replace (bal u v w z) with (bal ll lx ld (join lr x d (Node rl rx rd rr rh))); [ | auto] - end - | destruct (gt_le_dec rh (lh+2)); - [ match goal with |- context [ bal ?u ?v ?w ?z ] => - replace (bal u v w z) - with (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr); [ | auto] + end + | destruct (gt_le_dec rh (lh+2)); + [ match goal with |- context [ bal ?u ?v ?w ?z ] => + replace (bal u v w z) + with (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr); [ | auto] end | ] ] ] ]; intros. @@ -575,7 +574,7 @@ Proof. Qed. Lemma In_alt : forall k m, In0 k m <-> In k m. -Proof. +Proof. split. intros (e,H); eauto. unfold In0; apply In_MapsTo; auto. @@ -588,14 +587,14 @@ Proof. Qed. Hint Immediate MapsTo_1. -Lemma In_1 : +Lemma In_1 : forall m x y, X.eq x y -> In x m -> In y m. Proof. intros m x y; induction m; simpl; intuition_in; eauto. Qed. -Lemma In_node_iff : - forall l x e r h y, +Lemma In_node_iff : + forall l x e r h y, In y (Node l x e r h) <-> In y l \/ X.eq y x \/ In y r. Proof. intuition_in. @@ -613,7 +612,7 @@ Proof. unfold gt_tree in |- *; intros; intuition_in. Qed. -Lemma lt_tree_node : forall x y l r e h, +Lemma lt_tree_node : forall x y l r e h, lt_tree x l -> lt_tree x r -> X.lt y x -> lt_tree x (Node l y e r h). Proof. unfold lt_tree in *; intuition_in; order. @@ -627,25 +626,25 @@ Qed. Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node. -Lemma lt_left : forall x y l r e h, +Lemma lt_left : forall x y l r e h, lt_tree x (Node l y e r h) -> lt_tree x l. Proof. intuition_in. Qed. -Lemma lt_right : forall x y l r e h, +Lemma lt_right : forall x y l r e h, lt_tree x (Node l y e r h) -> lt_tree x r. Proof. intuition_in. Qed. -Lemma gt_left : forall x y l r e h, +Lemma gt_left : forall x y l r e h, gt_tree x (Node l y e r h) -> gt_tree x l. Proof. intuition_in. Qed. -Lemma gt_right : forall x y l r e h, +Lemma gt_right : forall x y l r e h, gt_tree x (Node l y e r h) -> gt_tree x r. Proof. intuition_in. @@ -695,39 +694,39 @@ Qed. (** * Emptyness test *) -Lemma is_empty_1 : forall m, Empty m -> is_empty m = true. +Lemma is_empty_1 : forall m, Empty m -> is_empty m = true. Proof. destruct m as [|r x e l h]; simpl; auto. intro H; elim (H x e); auto. Qed. Lemma is_empty_2 : forall m, is_empty m = true -> Empty m. -Proof. +Proof. destruct m; simpl; intros; try discriminate; red; intuition_in. Qed. (** * Appartness *) Lemma mem_1 : forall m x, bst m -> In x m -> mem x m = true. -Proof. +Proof. intros m x; functional induction (mem x m); auto; intros; clearf; inv bst; intuition_in; order. Qed. -Lemma mem_2 : forall m x, mem x m = true -> In x m. -Proof. +Lemma mem_2 : forall m x, mem x m = true -> In x m. +Proof. intros m x; functional induction (mem x m); auto; intros; discriminate. Qed. Lemma find_1 : forall m x e, bst m -> MapsTo x e m -> find x m = Some e. -Proof. +Proof. intros m x; functional induction (find x m); auto; intros; clearf; - inv bst; intuition_in; simpl; auto; + inv bst; intuition_in; simpl; auto; try solve [order | absurd (X.lt x y); eauto | absurd (X.lt y x); eauto]. Qed. Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m. -Proof. +Proof. intros m x; functional induction (find x m); subst; intros; clearf; try discriminate. constructor 2; auto. @@ -735,7 +734,7 @@ Proof. constructor 3; auto. Qed. -Lemma find_iff : forall m x e, bst m -> +Lemma find_iff : forall m x e, bst m -> (find x m = Some e <-> MapsTo x e m). Proof. split; auto using find_1, find_2. @@ -745,7 +744,7 @@ Lemma find_in : forall m x, find x m <> None -> In x m. Proof. intros. case_eq (find x m); [intros|congruence]. - apply MapsTo_In with e; apply find_2; auto. + apply MapsTo_In with e; apply find_2; auto. Qed. Lemma in_find : forall m x, bst m -> In x m -> find x m <> None. @@ -755,7 +754,7 @@ Proof. rewrite (find_1 H Hd); discriminate. Qed. -Lemma find_in_iff : forall m x, bst m -> +Lemma find_in_iff : forall m x, bst m -> (find x m <> None <-> In x m). Proof. split; auto using find_in, in_find. @@ -771,11 +770,11 @@ Proof. elim H0; apply find_in; congruence. Qed. -Lemma find_find : forall m m' x, - find x m = find x m' <-> +Lemma find_find : forall m m' x, + find x m = find x m' <-> (forall d, find x m = Some d <-> find x m' = Some d). Proof. - intros; destruct (find x m); destruct (find x m'); split; intros; + intros; destruct (find x m); destruct (find x m'); split; intros; try split; try congruence. rewrite H; auto. symmetry; rewrite <- H; auto. @@ -783,7 +782,7 @@ Proof. Qed. Lemma find_mapsto_equiv : forall m m' x, bst m -> bst m' -> - (find x m = find x m' <-> + (find x m = find x m' <-> (forall d, MapsTo x d m <-> MapsTo x d m')). Proof. intros m m' x Hm Hm'. @@ -793,8 +792,8 @@ Proof. rewrite 2 find_iff; auto. Qed. -Lemma find_in_equiv : forall m m' x, bst m -> bst m' -> - find x m = find x m' -> +Lemma find_in_equiv : forall m m' x, bst m -> bst m' -> + find x m = find x m' -> (In x m <-> In x m'). Proof. split; intros; apply find_in; [ rewrite <- H1 | rewrite H1 ]; @@ -803,27 +802,27 @@ Qed. (** * Helper functions *) -Lemma create_bst : - forall l x e r, bst l -> bst r -> lt_tree x l -> gt_tree x r -> +Lemma create_bst : + forall l x e r, bst l -> bst r -> lt_tree x l -> gt_tree x r -> bst (create l x e r). Proof. unfold create; auto. Qed. Hint Resolve create_bst. -Lemma create_in : - forall l x e r y, +Lemma create_in : + forall l x e r y, In y (create l x e r) <-> X.eq y x \/ In y l \/ In y r. Proof. unfold create; split; [ inversion_clear 1 | ]; intuition. Qed. -Lemma bal_bst : forall l x e r, bst l -> bst r -> +Lemma bal_bst : forall l x e r, bst l -> bst r -> lt_tree x l -> gt_tree x r -> bst (bal l x e r). Proof. intros l x e r; functional induction (bal l x e r); intros; clearf; inv bst; repeat apply create_bst; auto; unfold create; try constructor; - (apply lt_tree_node || apply gt_tree_node); auto; + (apply lt_tree_node || apply gt_tree_node); auto; (eapply lt_tree_trans || eapply gt_tree_trans); eauto. Qed. Hint Resolve bal_bst. @@ -842,7 +841,7 @@ Proof. unfold assert_false, create; intuition_in. Qed. -Lemma bal_find : forall l x e r y, +Lemma bal_find : forall l x e r y, bst l -> bst r -> lt_tree x l -> gt_tree x r -> find y (bal l x e r) = find y (create l x e r). Proof. @@ -870,32 +869,32 @@ Qed. Hint Resolve add_bst. Lemma add_1 : forall m x y e, X.eq x y -> MapsTo y e (add x e m). -Proof. - intros m x y e; functional induction (add x e m); +Proof. + intros m x y e; functional induction (add x e m); intros; inv bst; try rewrite bal_mapsto; unfold create; eauto. Qed. -Lemma add_2 : forall m x y e e', ~X.eq x y -> +Lemma add_2 : forall m x y e e', ~X.eq x y -> MapsTo y e m -> MapsTo y e (add x e' m). Proof. intros m x y e e'; induction m; simpl; auto. destruct (X.compare x k); - intros; inv bst; try rewrite bal_mapsto; unfold create; auto; + intros; inv bst; try rewrite bal_mapsto; unfold create; auto; inv MapsTo; auto; order. Qed. -Lemma add_3 : forall m x y e e', ~X.eq x y -> +Lemma add_3 : forall m x y e e', ~X.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m. Proof. - intros m x y e e'; induction m; simpl; auto. + intros m x y e e'; induction m; simpl; auto. intros; inv MapsTo; auto; order. - destruct (X.compare x k); intro; - try rewrite bal_mapsto; auto; unfold create; intros; inv MapsTo; auto; + destruct (X.compare x k); intro; + try rewrite bal_mapsto; auto; unfold create; intros; inv MapsTo; auto; order. Qed. -Lemma add_find : forall m x y e, bst m -> - find y (add x e m) = +Lemma add_find : forall m x y e, bst m -> + find y (add x e m) = match X.compare y x with EQ _ => Some e | _ => find y m end. Proof. intros. @@ -909,7 +908,7 @@ Qed. (** * Extraction of minimum binding *) Lemma remove_min_in : forall l x e r h y, - In y (Node l x e r h) <-> + In y (Node l x e r h) <-> X.eq y (remove_min l x e r)#2#1 \/ In y (remove_min l x e r)#1. Proof. intros l x e r; functional induction (remove_min l x e r); simpl in *; intros. @@ -919,7 +918,7 @@ Proof. Qed. Lemma remove_min_mapsto : forall l x e r h y e', - MapsTo y e' (Node l x e r h) <-> + MapsTo y e' (Node l x e r h) <-> ((X.eq y (remove_min l x e r)#2#1) /\ e' = (remove_min l x e r)#2#2) \/ MapsTo y e' (remove_min l x e r)#1. Proof. @@ -933,7 +932,7 @@ Proof. inversion_clear H3; intuition. Qed. -Lemma remove_min_bst : forall l x e r h, +Lemma remove_min_bst : forall l x e r h, bst (Node l x e r h) -> bst (remove_min l x e r)#1. Proof. intros l x e r; functional induction (remove_min l x e r); simpl in *; intros. @@ -949,8 +948,8 @@ Proof. Qed. Hint Resolve remove_min_bst. -Lemma remove_min_gt_tree : forall l x e r h, - bst (Node l x e r h) -> +Lemma remove_min_gt_tree : forall l x e r h, + bst (Node l x e r h) -> gt_tree (remove_min l x e r)#2#1 (remove_min l x e r)#1. Proof. intros l x e r; functional induction (remove_min l x e r); simpl in *; intros. @@ -968,10 +967,10 @@ Proof. Qed. Hint Resolve remove_min_gt_tree. -Lemma remove_min_find : forall l x e r h y, - bst (Node l x e r h) -> - find y (Node l x e r h) = - match X.compare y (remove_min l x e r)#2#1 with +Lemma remove_min_find : forall l x e r h y, + bst (Node l x e r h) -> + find y (Node l x e r h) = + match X.compare y (remove_min l x e r)#2#1 with | LT _ => None | EQ _ => Some (remove_min l x e r)#2#2 | GT _ => find y (remove_min l x e r)#1 @@ -990,9 +989,9 @@ Qed. (** * Merging two trees *) -Lemma merge_in : forall m1 m2 y, bst m1 -> bst m2 -> +Lemma merge_in : forall m1 m2 y, bst m1 -> bst m2 -> (In y (merge m1 m2) <-> In y m1 \/ In y m2). -Proof. +Proof. intros m1 m2; functional induction (merge m1 m2);intros; try factornode _x _x0 _x1 _x2 _x3 as m1. intuition_in. @@ -1000,10 +999,10 @@ Proof. rewrite bal_in, remove_min_in, e1; simpl; intuition. Qed. -Lemma merge_mapsto : forall m1 m2 y e, bst m1 -> bst m2 -> +Lemma merge_mapsto : forall m1 m2 y e, bst m1 -> bst m2 -> (MapsTo y e (merge m1 m2) <-> MapsTo y e m1 \/ MapsTo y e m2). Proof. - intros m1 m2; functional induction (merge m1 m2); intros; + intros m1 m2; functional induction (merge m1 m2); intros; try factornode _x _x0 _x1 _x2 _x3 as m1. intuition_in. intuition_in. @@ -1013,12 +1012,12 @@ Proof. inversion_clear H1; intuition. Qed. -Lemma merge_bst : forall m1 m2, bst m1 -> bst m2 -> - (forall y1 y2 : key, In y1 m1 -> In y2 m2 -> X.lt y1 y2) -> - bst (merge m1 m2). +Lemma merge_bst : forall m1 m2, bst m1 -> bst m2 -> + (forall y1 y2 : key, In y1 m1 -> In y2 m2 -> X.lt y1 y2) -> + bst (merge m1 m2). Proof. intros m1 m2; functional induction (merge m1 m2); intros; auto; - try factornode _x _x0 _x1 _x2 _x3 as m1. + try factornode _x _x0 _x1 _x2 _x3 as m1. apply bal_bst; auto. generalize (remove_min_bst H0); rewrite e1; simpl in *; auto. intro; intro. @@ -1029,7 +1028,7 @@ Qed. (** * Deletion *) -Lemma remove_in : forall m x y, bst m -> +Lemma remove_in : forall m x y, bst m -> (In y (remove x m) <-> ~ X.eq y x /\ In y m). Proof. intros m x; functional induction (remove x m); simpl; intros. @@ -1049,7 +1048,7 @@ Proof. Qed. Lemma remove_bst : forall m x, bst m -> bst (remove x m). -Proof. +Proof. intros m x; functional induction (remove x m); simpl; intros. auto. (* LT *) @@ -1061,7 +1060,7 @@ Proof. (* EQ *) inv bst. apply merge_bst; eauto. - (* GT *) + (* GT *) inv bst. apply bal_bst; auto. intro; intro. @@ -1070,16 +1069,16 @@ Proof. Qed. Lemma remove_1 : forall m x y, bst m -> X.eq x y -> ~ In y (remove x m). -Proof. +Proof. intros; rewrite remove_in; intuition. Qed. -Lemma remove_2 : forall m x y e, bst m -> ~X.eq x y -> +Lemma remove_2 : forall m x y e, bst m -> ~X.eq x y -> MapsTo y e m -> MapsTo y e (remove x m). Proof. intros m x y e; induction m; simpl; auto. - destruct (X.compare x k); - intros; inv bst; try rewrite bal_mapsto; unfold create; auto; + destruct (X.compare x k); + intros; inv bst; try rewrite bal_mapsto; unfold create; auto; try solve [inv MapsTo; auto]. rewrite merge_mapsto; auto. inv MapsTo; auto; order. @@ -1089,7 +1088,7 @@ Lemma remove_3 : forall m x y e, bst m -> MapsTo y e (remove x m) -> MapsTo y e m. Proof. intros m x y e; induction m; simpl; auto. - destruct (X.compare x k); intros Bs; inv bst; + destruct (X.compare x k); intros Bs; inv bst; try rewrite bal_mapsto; auto; unfold create. intros; inv MapsTo; auto. rewrite merge_mapsto; intuition. @@ -1098,7 +1097,7 @@ Qed. (** * join *) -Lemma join_in : forall l x d r y, +Lemma join_in : forall l x d r y, In y (join l x d r) <-> X.eq y x \/ In y l \/ In y r. Proof. join_tac. @@ -1110,23 +1109,23 @@ Proof. apply create_in. Qed. -Lemma join_bst : forall l x d r, bst l -> bst r -> +Lemma join_bst : forall l x d r, bst l -> bst r -> lt_tree x l -> gt_tree x r -> bst (join l x d r). Proof. - join_tac; auto; try (simpl; auto; fail); inv bst; apply bal_bst; auto; + join_tac; auto; try (simpl; auto; fail); inv bst; apply bal_bst; auto; clear Hrl Hlr z; intro; intros; rewrite join_in in *. intuition; [ apply MX.lt_eq with x | ]; eauto. intuition; [ apply MX.eq_lt with x | ]; eauto. Qed. Hint Resolve join_bst. -Lemma join_find : forall l x d r y, - bst l -> bst r -> lt_tree x l -> gt_tree x r -> +Lemma join_find : forall l x d r y, + bst l -> bst r -> lt_tree x l -> gt_tree x r -> find y (join l x d r) = find y (create l x d r). Proof. join_tac; auto; inv bst; - simpl (join (Leaf elt)); - try (assert (X.lt lx x) by auto); + simpl (join (Leaf elt)); + try (assert (X.lt lx x) by auto); try (assert (X.lt x rx) by auto); rewrite ?add_find, ?bal_find; auto. @@ -1150,10 +1149,10 @@ Qed. (** * split *) -Lemma split_in_1 : forall m x, bst m -> forall y, +Lemma split_in_1 : forall m x, bst m -> forall y, (In y (split x m)#l <-> In y m /\ X.lt y x). Proof. - intros m x; functional induction (split x m); simpl; intros; + intros m x; functional induction (split x m); simpl; intros; inv bst; try clear e0. intuition_in. rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order. @@ -1162,10 +1161,10 @@ Proof. rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order. Qed. -Lemma split_in_2 : forall m x, bst m -> forall y, +Lemma split_in_2 : forall m x, bst m -> forall y, (In y (split x m)#r <-> In y m /\ X.lt x y). -Proof. - intros m x; functional induction (split x m); subst; simpl; intros; +Proof. + intros m x; functional induction (split x m); subst; simpl; intros; inv bst; try clear e0. intuition_in. rewrite join_in. @@ -1174,18 +1173,18 @@ Proof. rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order. Qed. -Lemma split_in_3 : forall m x, bst m -> +Lemma split_in_3 : forall m x, bst m -> (split x m)#o = find x m. Proof. intros m x; functional induction (split x m); subst; simpl; auto; - intros; inv bst; try clear e0; - destruct X.compare; try (order;fail); rewrite <-IHt, e1; auto. + intros; inv bst; try clear e0; + destruct X.compare; try order; trivial; rewrite <- IHt, e1; auto. Qed. -Lemma split_bst : forall m x, bst m -> +Lemma split_bst : forall m x, bst m -> bst (split x m)#l /\ bst (split x m)#r. -Proof. - intros m x; functional induction (split x m); subst; simpl; intros; +Proof. + intros m x; functional induction (split x m); subst; simpl; intros; inv bst; try clear e0; try rewrite e1 in *; simpl in *; intuition; apply join_bst; auto. intros y0. @@ -1204,17 +1203,17 @@ Proof. intros m x B y Hy; rewrite split_in_2 in Hy; intuition. Qed. -Lemma split_find : forall m x y, bst m -> - find y m = match X.compare y x with +Lemma split_find : forall m x y, bst m -> + find y m = match X.compare y x with | LT _ => find y (split x m)#l | EQ _ => (split x m)#o | GT _ => find y (split x m)#r end. Proof. - intros m x; functional induction (split x m); subst; simpl; intros; - inv bst; try clear e0; try rewrite e1 in *; simpl in *; + intros m x; functional induction (split x m); subst; simpl; intros; + inv bst; try clear e0; try rewrite e1 in *; simpl in *; [ destruct X.compare; auto | .. ]; - try match goal with E:split ?x ?t = _, B:bst ?t |- _ => + try match goal with E:split ?x ?t = _, B:bst ?t |- _ => generalize (split_in_1 x B)(split_in_2 x B)(split_bst x B); rewrite E; simpl; destruct 3 end. @@ -1231,7 +1230,7 @@ Qed. (** * Concatenation *) -Lemma concat_in : forall m1 m2 y, +Lemma concat_in : forall m1 m2 y, In y (concat m1 m2) <-> In y m1 \/ In y m2. Proof. intros m1 m2; functional induction (concat m1 m2); intros; @@ -1241,11 +1240,11 @@ Proof. rewrite join_in, remove_min_in, e1; simpl; intuition. Qed. -Lemma concat_bst : forall m1 m2, bst m1 -> bst m2 -> - (forall y1 y2, In y1 m1 -> In y2 m2 -> X.lt y1 y2) -> +Lemma concat_bst : forall m1 m2, bst m1 -> bst m2 -> + (forall y1 y2, In y1 m1 -> In y2 m2 -> X.lt y1 y2) -> bst (concat m1 m2). Proof. - intros m1 m2; functional induction (concat m1 m2); intros; auto; + intros m1 m2; functional induction (concat m1 m2); intros; auto; try factornode _x _x0 _x1 _x2 _x3 as m1. apply join_bst; auto. change (bst (m2',xd)#1); rewrite <-e1; eauto. @@ -1256,19 +1255,19 @@ Proof. Qed. Hint Resolve concat_bst. -Lemma concat_find : forall m1 m2 y, bst m1 -> bst m2 -> - (forall y1 y2, In y1 m1 -> In y2 m2 -> X.lt y1 y2) -> - find y (concat m1 m2) = +Lemma concat_find : forall m1 m2 y, bst m1 -> bst m2 -> + (forall y1 y2, In y1 m1 -> In y2 m2 -> X.lt y1 y2) -> + find y (concat m1 m2) = match find y m2 with Some d => Some d | None => find y m1 end. Proof. - intros m1 m2; functional induction (concat m1 m2); intros; auto; + intros m1 m2; functional induction (concat m1 m2); intros; auto; try factornode _x _x0 _x1 _x2 _x3 as m1. simpl; destruct (find y m2); auto. generalize (remove_min_find y H0)(remove_min_in l2 x2 d2 r2 _x4) - (remove_min_bst H0)(remove_min_gt_tree H0); + (remove_min_bst H0)(remove_min_gt_tree H0); rewrite e1; simpl fst; simpl snd; intros. - + inv bst. rewrite H2, join_find; auto; clear H2. simpl; destruct X.compare; simpl; auto. @@ -1286,7 +1285,7 @@ Notation eqk := (PX.eqk (elt:= elt)). Notation eqke := (PX.eqke (elt:= elt)). Notation ltk := (PX.ltk (elt:= elt)). -Lemma elements_aux_mapsto : forall (s:t elt) acc x e, +Lemma elements_aux_mapsto : forall (s:t elt) acc x e, InA eqke (x,e) (elements_aux acc s) <-> MapsTo x e s \/ InA eqke (x,e) acc. Proof. induction s as [ | l Hl x e r Hr h ]; simpl; auto. @@ -1299,8 +1298,8 @@ Proof. destruct H0; simpl in *; subst; intuition. Qed. -Lemma elements_mapsto : forall (s:t elt) x e, InA eqke (x,e) (elements s) <-> MapsTo x e s. -Proof. +Lemma elements_mapsto : forall (s:t elt) x e, InA eqke (x,e) (elements s) <-> MapsTo x e s. +Proof. intros; generalize (elements_aux_mapsto s nil x e); intuition. inversion_clear H0. Qed. @@ -1324,9 +1323,9 @@ Proof. induction s as [ | l Hl y e r Hr h]; simpl; intuition. inv bst. apply Hl; auto. - constructor. + constructor. apply Hr; eauto. - apply (InA_InfA (PX.eqke_refl (elt:=elt))); intros (y',e') H6. + apply InA_InfA with (eqA:=eqke); auto with *. intros (y',e') H6. destruct (elements_aux_mapsto r acc y' e'); intuition. red; simpl; eauto. red; simpl; eauto. @@ -1382,7 +1381,7 @@ Qed. (** * Fold *) -Definition fold' (A : Type) (f : key -> elt -> A -> A)(s : t elt) := +Definition fold' (A : Type) (f : key -> elt -> A -> A)(s : t elt) := L.fold f (elements s). Lemma fold_equiv_aux : @@ -1401,14 +1400,14 @@ Lemma fold_equiv : forall (A : Type) (s : t elt) (f : key -> elt -> A -> A) (a : A), fold f s a = fold' f s a. Proof. - unfold fold', elements in |- *. + unfold fold', elements in |- *. simple induction s; simpl in |- *; auto; intros. rewrite fold_equiv_aux. rewrite H0. simpl in |- *; auto. Qed. -Lemma fold_1 : +Lemma fold_1 : forall (s:t elt)(Hs:bst s)(A : Type)(i:A)(f : key -> elt -> A -> A), fold f s i = fold_left (fun a p => f p#1 p#2 a) (elements s) i. Proof. @@ -1421,9 +1420,9 @@ Qed. (** * Comparison *) -(** [flatten_e e] returns the list of elements of the enumeration [e] +(** [flatten_e e] returns the list of elements of the enumeration [e] i.e. the list of elements actually compared *) - + Fixpoint flatten_e (e : enumeration elt) : list (key*elt) := match e with | End => nil | More x e t r => (x,e) :: elements t ++ flatten_e r @@ -1431,13 +1430,13 @@ Fixpoint flatten_e (e : enumeration elt) : list (key*elt) := match e with Lemma flatten_e_elements : forall (l:t elt) r x d z e, - elements l ++ flatten_e (More x d r e) = + elements l ++ flatten_e (More x d r e) = elements (Node l x d r z) ++ flatten_e e. Proof. intros; simpl; apply elements_node. Qed. -Lemma cons_1 : forall (s:t elt) e, +Lemma cons_1 : forall (s:t elt) e, flatten_e (cons s e) = elements s ++ flatten_e e. Proof. induction s; simpl; auto; intros. @@ -1450,24 +1449,24 @@ 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 -> +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; destruct X.compare; simpl; + unfold IfEq; destruct b; simpl; intros; destruct X.compare; simpl; try rewrite H0; auto; order. Qed. -Lemma equal_end_IfEq : forall e2, +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 (elements r2 ++ flatten_e e2) -> +Lemma equal_more_IfEq : + forall x1 d1 (cont:enumeration elt -> bool) x2 d2 r2 e2 l, + IfEq (cont (cons r2 e2)) l (elements r2 ++ flatten_e e2) -> IfEq (equal_more cmp x1 d1 cont (More x2 d2 r2 e2)) ((x1,d1)::l) (flatten_e (More x2 d2 r2 e2)). Proof. @@ -1475,7 +1474,7 @@ Proof. rewrite <-andb_lazy_alt; f_equal; auto. Qed. -Lemma equal_cont_IfEq : forall m1 cont e2 l, +Lemma equal_cont_IfEq : forall m1 cont e2 l, (forall e, IfEq (cont e) l (flatten_e e)) -> IfEq (equal_cont cmp m1 cont e2) (elements m1 ++ l) (flatten_e e2). Proof. @@ -1493,18 +1492,18 @@ Lemma equal_IfEq : forall (m1 m2:t elt), Proof. intros; unfold equal. rewrite (app_nil_end (elements m1)). - replace (elements m2) with (flatten_e (cons m2 (End _))) + replace (elements m2) with (flatten_e (cons m2 (End _))) by (rewrite cons_1; simpl; rewrite <-app_nil_end; auto). apply equal_cont_IfEq. intros. apply equal_end_IfEq; auto. Qed. -Definition Equivb m m' := - (forall k, In k m <-> In k m') /\ +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_elements : forall s s', +Lemma Equivb_elements : forall s s', Equivb s s' <-> L.Equivb cmp (elements s) (elements s'). Proof. unfold Equivb, L.Equivb; split; split; intros. @@ -1516,7 +1515,7 @@ destruct H. apply (H2 k); unfold L.PX.MapsTo; rewrite elements_mapsto; auto. Qed. -Lemma equal_Equivb : forall (s s': t elt), bst s -> bst s' -> +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'. @@ -1526,17 +1525,17 @@ Qed. End Elt. -Section Map. +Section Map. Variable elt elt' : Type. -Variable f : elt -> elt'. +Variable f : elt -> elt'. -Lemma map_1 : forall (m: t elt)(x:key)(e:elt), +Lemma map_1 : forall (m: t elt)(x:key)(e:elt), MapsTo x e m -> MapsTo x (f e) (map f m). Proof. induction m; simpl; inversion_clear 1; auto. Qed. -Lemma map_2 : forall (m: t elt)(x:key), +Lemma map_2 : forall (m: t elt)(x:key), In x (map f m) -> In x m. Proof. induction m; simpl; inversion_clear 1; auto. @@ -1545,7 +1544,7 @@ Qed. Lemma map_bst : forall m, bst m -> bst (map f m). Proof. induction m; simpl; auto. -inversion_clear 1; constructor; auto; +inversion_clear 1; constructor; auto; red; auto using map_2. Qed. @@ -1554,7 +1553,7 @@ Section Mapi. Variable elt elt' : Type. Variable f : key -> elt -> elt'. -Lemma mapi_1 : forall (m: tree elt)(x:key)(e:elt), +Lemma mapi_1 : forall (m: tree elt)(x:key)(e:elt), MapsTo x e m -> exists y, X.eq y x /\ MapsTo x (f y e) (mapi f m). Proof. induction m; simpl; inversion_clear 1; auto. @@ -1565,7 +1564,7 @@ destruct (IHm2 _ _ H0). exists x0; intuition. Qed. -Lemma mapi_2 : forall (m: t elt)(x:key), +Lemma mapi_2 : forall (m: t elt)(x:key), In x (mapi f m) -> In x m. Proof. induction m; simpl; inversion_clear 1; auto. @@ -1574,7 +1573,7 @@ Qed. Lemma mapi_bst : forall m, bst m -> bst (mapi f m). Proof. induction m; simpl; auto. -inversion_clear 1; constructor; auto; +inversion_clear 1; constructor; auto; red; auto using mapi_2. Qed. @@ -1585,7 +1584,7 @@ Variable elt elt' : Type. Variable f : key -> elt -> option elt'. Hypothesis f_compat : forall x x' d, X.eq x x' -> f x d = f x' d. -Lemma map_option_2 : forall (m:t elt)(x:key), +Lemma map_option_2 : forall (m:t elt)(x:key), In x (map_option f m) -> exists d, MapsTo x d m /\ f x d <> None. Proof. intros m; functional induction (map_option f m); simpl; auto; intros. @@ -1601,9 +1600,9 @@ Qed. Lemma map_option_bst : forall m, bst m -> bst (map_option f m). Proof. -intros m; functional induction (map_option f m); simpl; auto; intros; +intros m; functional induction (map_option f m); simpl; auto; intros; inv bst. -apply join_bst; auto; intros y H; +apply join_bst; auto; intros y H; destruct (map_option_2 H) as (d0 & ? & ?); eauto using MapsTo_In. apply concat_bst; auto; intros y y' H H'. destruct (map_option_2 H) as (d0 & ? & ?). @@ -1612,22 +1611,22 @@ eapply X.lt_trans with x; eauto using MapsTo_In. Qed. Hint Resolve map_option_bst. -Ltac nonify e := - replace e with (@None elt) by +Ltac nonify e := + replace e with (@None elt) by (symmetry; rewrite not_find_iff; auto; intro; order). -Lemma map_option_find : forall (m:t elt)(x:key), - bst m -> - find x (map_option f m) = +Lemma map_option_find : forall (m:t elt)(x:key), + bst m -> + find x (map_option f m) = match (find x m) with Some d => f x d | None => None end. Proof. intros m; functional induction (map_option f m); simpl; auto; intros; - inv bst; rewrite join_find || rewrite concat_find; auto; simpl; + inv bst; rewrite join_find || rewrite concat_find; auto; simpl; try destruct X.compare; simpl; auto. rewrite (f_compat d e); auto. intros y H; destruct (map_option_2 H) as (? & ? & ?); eauto using MapsTo_In. -intros y H; +intros y H; destruct (map_option_2 H) as (? & ? & ?); eauto using MapsTo_In. rewrite <- IHt, IHt0; auto; nonify (find x0 r); auto. @@ -1653,21 +1652,21 @@ Variable mapr : t elt' -> t elt''. Hypothesis f0_f : forall x d o, f x d o = f0 x (Some d) o. Hypothesis mapl_bst : forall m, bst m -> bst (mapl m). Hypothesis mapr_bst : forall m', bst m' -> bst (mapr m'). -Hypothesis mapl_f0 : forall x m, bst m -> - find x (mapl m) = +Hypothesis mapl_f0 : forall x m, bst m -> + find x (mapl m) = match find x m with Some d => f0 x (Some d) None | None => None end. -Hypothesis mapr_f0 : forall x m', bst m' -> - find x (mapr m') = +Hypothesis mapr_f0 : forall x m', bst m' -> + find x (mapr m') = match find x m' with Some d' => f0 x None (Some d') | None => None end. Hypothesis f0_compat : forall x x' o o', X.eq x x' -> f0 x o o' = f0 x' o o'. Notation map2_opt := (map2_opt f mapl mapr). -Lemma map2_opt_2 : forall m m' y, bst m -> bst m' -> +Lemma map2_opt_2 : forall m m' y, bst m -> bst m' -> In y (map2_opt m m') -> In y m \/ In y m'. Proof. intros m m'; functional induction (map2_opt m m'); intros; - auto; try factornode _x0 _x1 _x2 _x3 _x4 as m2; + auto; try factornode _x0 _x1 _x2 _x3 _x4 as m2; try (generalize (split_in_1 x1 H0 y)(split_in_2 x1 H0 y) (split_bst x1 H0); rewrite e1; simpl; destruct 3; inv bst). @@ -1689,12 +1688,12 @@ destruct (IHt1 y H6 H4 H'); intuition. destruct (IHt0 y H7 H5 H'); intuition. Qed. -Lemma map2_opt_bst : forall m m', bst m -> bst m' -> +Lemma map2_opt_bst : forall m m', bst m -> bst m' -> bst (map2_opt m m'). Proof. intros m m'; functional induction (map2_opt m m'); intros; - auto; try factornode _x0 _x1 _x2 _x3 _x4 as m2; inv bst; - generalize (split_in_1 x1 H0)(split_in_2 x1 H0)(split_bst x1 H0); + auto; try factornode _x0 _x1 _x2 _x3 _x4 as m2; inv bst; + generalize (split_in_1 x1 H0)(split_in_2 x1 H0)(split_bst x1 H0); rewrite e1; simpl in *; destruct 3. apply join_bst; auto. @@ -1711,31 +1710,31 @@ destruct (map2_opt_2 H2 H7 Hy'); intuition. Qed. Hint Resolve map2_opt_bst. -Ltac map2_aux := +Ltac map2_aux := match goal with - | H : In ?x _ \/ In ?x ?m, - H' : find ?x ?m = find ?x ?m', B:bst ?m, B':bst ?m' |- _ => - destruct H; [ intuition_in; order | + | H : In ?x _ \/ In ?x ?m, + H' : find ?x ?m = find ?x ?m', B:bst ?m, B':bst ?m' |- _ => + destruct H; [ intuition_in; order | rewrite <-(find_in_equiv B B' H'); auto ] end. -Ltac nonify t := - match t with (find ?y (map2_opt ?m ?m')) => +Ltac nonify t := + match t with (find ?y (map2_opt ?m ?m')) => replace t with (@None elt''); [ | symmetry; rewrite not_find_iff; auto; intro; destruct (@map2_opt_2 m m' y); auto; order ] end. -Lemma map2_opt_1 : forall m m' y, bst m -> bst m' -> +Lemma map2_opt_1 : forall m m' y, bst m -> bst m' -> In y m \/ In y m' -> find y (map2_opt m m') = f0 y (find y m) (find y m'). Proof. intros m m'; functional induction (map2_opt m m'); intros; - auto; try factornode _x0 _x1 _x2 _x3 _x4 as m2; + auto; try factornode _x0 _x1 _x2 _x3 _x4 as m2; try (generalize (split_in_1 x1 H0)(split_in_2 x1 H0) (split_in_3 x1 H0)(split_bst x1 H0)(split_find x1 y H0) (split_lt_tree (x:=x1) H0)(split_gt_tree (x:=x1) H0); - rewrite e1; simpl in *; destruct 4; intros; inv bst; + rewrite e1; simpl in *; destruct 4; intros; inv bst; subst o2; rewrite H7, ?join_find, ?concat_find; auto). simpl; destruct H1; [ inversion_clear H1 | ]. @@ -1777,23 +1776,23 @@ Variable f : option elt -> option elt' -> option elt''. Lemma map2_bst : forall m m', bst m -> bst m' -> bst (map2 f m m'). Proof. unfold map2; intros. -apply map2_opt_bst with (fun _ => f); auto using map_option_bst; +apply map2_opt_bst with (fun _ => f); auto using map_option_bst; intros; rewrite map_option_find; auto. Qed. -Lemma map2_1 : forall m m' y, bst m -> bst m' -> +Lemma map2_1 : forall m m' y, bst m -> bst m' -> In y m \/ In y m' -> find y (map2 f m m') = f (find y m) (find y m'). Proof. unfold map2; intros. -rewrite (map2_opt_1 (f0:=fun _ => f)); +rewrite (map2_opt_1 (f0:=fun _ => f)); auto using map_option_bst; intros; rewrite map_option_find; auto. Qed. -Lemma map2_2 : forall m m' y, bst m -> bst m' -> +Lemma map2_2 : forall m m' y, bst m -> bst m' -> In y (map2 f m m') -> In y m \/ In y m'. Proof. unfold map2; intros. -eapply map2_opt_2 with (f0:=fun _ => f); eauto; intros. +eapply map2_opt_2 with (f0:=fun _ => f); try eassumption; trivial; intros. apply map_option_bst; auto. apply map_option_bst; auto. rewrite map_option_find; auto. @@ -1806,38 +1805,38 @@ End Raw. (** * Encapsulation - Now, in order to really provide a functor implementing [S], we + 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. + Module Raw := Raw I X. Import Raw.Proofs. - Record bst (elt:Type) := + Record bst (elt:Type) := Bst {this :> Raw.tree elt; is_bst : Raw.bst this}. - - Definition t := bst. + + Definition t := bst. Definition key := E.t. - - Section Elt. + + Section Elt. Variable elt elt' elt'': Type. Implicit Types m : t elt. - Implicit Types x y : key. - Implicit Types e : elt. + Implicit Types x y : key. + Implicit Types e : elt. Definition empty : t elt := Bst (empty_bst elt). Definition is_empty m : bool := Raw.is_empty m.(this). Definition add x e m : t elt := Bst (add_bst x e m.(is_bst)). - Definition remove x m : t elt := Bst (remove_bst x m.(is_bst)). + Definition remove x m : t elt := Bst (remove_bst x m.(is_bst)). Definition mem x m : bool := Raw.mem x m.(this). Definition find x m : option elt := Raw.find x m.(this). Definition map f m : t elt' := Bst (map_bst f m.(is_bst)). - Definition mapi (f:key->elt->elt') m : t elt' := + Definition mapi (f:key->elt->elt') m : t elt' := Bst (mapi_bst f m.(is_bst)). - Definition map2 f m (m':t elt') : t elt'' := + Definition map2 f m (m':t elt') : t elt'' := Bst (map2_bst f m.(is_bst) m'.(is_bst)). Definition elements m : list (key*elt) := Raw.elements m.(this). Definition cardinal m := Raw.cardinal m.(this). @@ -1854,14 +1853,14 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. Lemma MapsTo_1 : forall m x y e, E.eq x y -> MapsTo x e m -> MapsTo y e m. Proof. intros m; exact (@MapsTo_1 _ m.(this)). Qed. - + Lemma mem_1 : forall m x, In x m -> mem x m = true. Proof. unfold In, mem; intros m x; rewrite In_alt; simpl; apply mem_1; auto. apply m.(is_bst). Qed. - - Lemma mem_2 : forall m x, mem x m = true -> In x m. + + Lemma mem_2 : forall m x, mem x m = true -> In x m. Proof. unfold In, mem; intros m x; rewrite In_alt; simpl; apply mem_2; auto. Qed. @@ -1892,7 +1891,7 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. Proof. intros m x y e; exact (@remove_3 elt _ x y e m.(is_bst)). Qed. - Lemma find_1 : forall m x e, MapsTo x e m -> find x m = Some e. + Lemma find_1 : forall m x e, MapsTo x e m -> find x m = Some e. Proof. intros m x e; exact (@find_1 elt _ x e m.(is_bst)). Qed. Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m. Proof. intros m; exact (@find_2 elt m.(this)). Qed. @@ -1901,36 +1900,36 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i. Proof. intros m; exact (@fold_1 elt m.(this) m.(is_bst)). Qed. - Lemma elements_1 : forall m x e, + Lemma elements_1 : forall m x e, MapsTo x e m -> InA eq_key_elt (x,e) (elements m). Proof. intros; unfold elements, MapsTo, eq_key_elt; rewrite elements_mapsto; auto. Qed. - Lemma elements_2 : forall m x e, + Lemma elements_2 : forall m x e, InA eq_key_elt (x,e) (elements m) -> MapsTo x e m. Proof. intros; unfold elements, MapsTo, eq_key_elt; rewrite <- elements_mapsto; auto. Qed. - Lemma elements_3 : forall m, sort lt_key (elements m). + Lemma elements_3 : forall m, sort lt_key (elements m). Proof. intros m; exact (@elements_sort elt m.(this) m.(is_bst)). Qed. - Lemma elements_3w : forall m, NoDupA eq_key (elements m). + Lemma elements_3w : forall m, NoDupA eq_key (elements m). Proof. intros m; exact (@elements_nodup elt m.(this) m.(is_bst)). Qed. Lemma cardinal_1 : forall m, cardinal m = length (elements m). Proof. intro m; exact (@elements_cardinal elt m.(this)). Qed. Definition Equal m m' := forall y, find y m = find y m'. - Definition Equiv (eq_elt:elt->elt->Prop) m m' := - (forall k, In k m <-> In k m') /\ + 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 : forall cmp m m', + Lemma Equivb_Equivb : forall cmp m m', Equivb cmp m m' <-> Raw.Proofs.Equivb cmp m m'. - Proof. + Proof. intros; unfold Equivb, Equiv, Raw.Proofs.Equivb, In; intuition. generalize (H0 k); do 2 rewrite In_alt; intuition. generalize (H0 k); do 2 rewrite In_alt; intuition. @@ -1938,23 +1937,23 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. generalize (H0 k); do 2 rewrite <- In_alt; intuition. Qed. - Lemma equal_1 : forall m m' cmp, - Equivb cmp m m' -> equal cmp m m' = true. - Proof. - unfold equal; intros (m,b) (m',b') cmp; rewrite Equivb_Equivb; + Lemma equal_1 : forall m m' cmp, + Equivb cmp m m' -> equal cmp m m' = true. + Proof. + unfold equal; intros (m,b) (m',b') cmp; rewrite Equivb_Equivb; intros; simpl in *; rewrite equal_Equivb; auto. - Qed. + Qed. - Lemma equal_2 : forall m m' cmp, + Lemma equal_2 : forall m m' cmp, equal cmp m m' = true -> Equivb cmp m m'. - Proof. - unfold equal; intros (m,b) (m',b') cmp; rewrite Equivb_Equivb; + Proof. + unfold equal; intros (m,b) (m',b') cmp; rewrite Equivb_Equivb; intros; simpl in *; rewrite <-equal_Equivb; auto. Qed. End Elt. - Lemma map_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)(f:elt->elt'), + Lemma map_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)(f:elt->elt'), MapsTo x e m -> MapsTo x (f e) (map f m). Proof. intros elt elt' m x e f; exact (@map_1 elt elt' f m.(this) x e). Qed. @@ -1962,10 +1961,10 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. Proof. intros elt elt' m x f; do 2 unfold In in *; do 2 rewrite In_alt; simpl. apply map_2; auto. - Qed. + Qed. Lemma mapi_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt) - (f:key->elt->elt'), MapsTo x e m -> + (f:key->elt->elt'), MapsTo x e m -> exists y, E.eq y x /\ MapsTo x (f y e) (mapi f m). Proof. intros elt elt' m x e f; exact (@mapi_1 elt elt' f m.(this) x e). Qed. Lemma mapi_2 : forall (elt elt':Type)(m: t elt)(x:key) @@ -1975,10 +1974,10 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. Qed. Lemma map2_1 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt') - (x:key)(f:option elt->option elt'->option elt''), - In x m \/ In x m' -> - find x (map2 f m m') = f (find x m) (find x m'). - Proof. + (x:key)(f:option elt->option elt'->option elt''), + In x m \/ In x m' -> + find x (map2 f m m') = f (find x m) (find x m'). + Proof. unfold find, map2, In; intros elt elt' elt'' m m' x f. do 2 rewrite In_alt; intros; simpl; apply map2_1; auto. apply m.(is_bst). @@ -1986,9 +1985,9 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. Qed. Lemma map2_2 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt') - (x:key)(f:option elt->option elt'->option elt''), + (x:key)(f:option elt->option elt'->option elt''), In x (map2 f m m') -> In x m \/ In x m'. - Proof. + Proof. unfold In, map2; intros elt elt' elt'' m m' x f. do 3 rewrite In_alt; intros; simpl in *; eapply map2_2; eauto. apply m.(is_bst). @@ -1998,19 +1997,19 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. End IntMake. -Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: - Sord with Module Data := D +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 Import MapS := IntMake(I)(X). Module LO := FMapList.Make_ord(X)(D). Module R := Raw. Module P := Raw.Proofs. Definition t := MapS.t D.t. - Definition cmp e e' := + Definition cmp e e' := match D.compare e e' with EQ _ => true | _ => false end. (** One step of comparison of elements *) @@ -2020,9 +2019,9 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: | R.End => Gt | R.More x2 d2 r2 e2 => match X.compare x1 x2 with - | EQ _ => match D.compare d1 d2 with + | EQ _ => match D.compare d1 d2 with | EQ _ => cont (R.cons r2 e2) - | LT _ => Lt + | LT _ => Lt | GT _ => Gt end | LT _ => Lt @@ -2046,7 +2045,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: (** The complete comparison *) - Definition compare_pure s1 s2 := + Definition compare_pure s1 s2 := compare_cont s1 compare_end (R.cons s2 (Raw.End _)). (** Correctness of this comparison *) @@ -2058,7 +2057,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: | Gt => (fun l1 l2 => LO.lt_list l2 l1) end. - Lemma cons_Cmp : forall c x1 x2 d1 d2 l1 l2, + Lemma cons_Cmp : forall c x1 x2 d1 d2 l1 l2, X.eq x1 x2 -> D.eq d1 d2 -> Cmp c l1 l2 -> Cmp c ((x1,d1)::l1) ((x2,d2)::l2). Proof. @@ -2077,10 +2076,10 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: Cmp (compare_more x1 d1 cont (R.More x2 d2 r2 e2)) ((x1,d1)::l) (P.flatten_e (R.More x2 d2 r2 e2)). Proof. - simpl; intros; destruct X.compare; simpl; + simpl; intros; destruct X.compare; simpl; try destruct D.compare; simpl; auto; P.MX.elim_comp; auto. Qed. - + Lemma compare_cont_Cmp : forall s1 cont e2 l, (forall e, Cmp (cont e) l (P.flatten_e e)) -> Cmp (compare_cont s1 cont e2) (R.elements s1 ++ l) (P.flatten_e e2). @@ -2110,14 +2109,14 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: Definition compare (s s':t) : Compare lt eq s s'. Proof. - intros (s,b) (s',b'). + destruct s as (s,b), s' as (s',b'). generalize (compare_Cmp s s'). destruct compare_pure; intros; [apply EQ|apply LT|apply GT]; red; auto. Defined. - + (* Proofs about [eq] and [lt] *) - Definition selements (m1 : t) := + Definition selements (m1 : t) := LO.MapS.Build_slist (P.elements_sort m1.(is_bst)). Definition seq (m1 m2 : t) := LO.eq (selements m1) (selements m2). @@ -2154,7 +2153,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: Qed. Lemma eq_refl : forall m : t, eq m m. - Proof. + Proof. intros; rewrite eq_seq; unfold seq; intros; apply LO.eq_refl. Qed. @@ -2171,13 +2170,13 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: Lemma lt_trans : forall m1 m2 m3 : t, lt m1 m2 -> lt m2 m3 -> lt m1 m3. Proof. - intros m1 m2 m3; rewrite 3 lt_slt; unfold slt; + intros m1 m2 m3; rewrite 3 lt_slt; unfold slt; intros; eapply LO.lt_trans; eauto. Qed. Lemma lt_not_eq : forall m1 m2 : t, lt m1 m2 -> ~ eq m1 m2. Proof. - intros m1 m2; rewrite lt_slt, eq_seq; unfold slt, seq; + intros m1 m2; rewrite lt_slt, eq_seq; unfold slt, seq; intros; apply LO.lt_not_eq; auto. Qed. @@ -2188,8 +2187,8 @@ End IntMake_ord. 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 +Module Make_ord (X: OrderedType)(D: OrderedType) + <: Sord with Module Data := D with Module MapS.E := X :=IntMake_ord(Z_as_Int)(X)(D). |