diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-07-15 10:36:12 +0200 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-07-15 10:36:12 +0200 |
commit | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (patch) | |
tree | 12e8931a4a56da1a1bdfb89d670f4ba38fe08e1f /theories/MMaps | |
parent | cec4741afacd2e80894232850eaf9f9c0e45d6d7 (diff) |
Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg
Diffstat (limited to 'theories/MMaps')
-rw-r--r-- | theories/MMaps/MMapAVL.v | 2158 | ||||
-rw-r--r-- | theories/MMaps/MMapFacts.v | 2434 | ||||
-rw-r--r-- | theories/MMaps/MMapInterface.v | 292 | ||||
-rw-r--r-- | theories/MMaps/MMapList.v | 1144 | ||||
-rw-r--r-- | theories/MMaps/MMapPositive.v | 698 | ||||
-rw-r--r-- | theories/MMaps/MMapWeakList.v | 687 | ||||
-rw-r--r-- | theories/MMaps/MMaps.v | 16 | ||||
-rw-r--r-- | theories/MMaps/vo.itarget | 7 |
8 files changed, 7436 insertions, 0 deletions
diff --git a/theories/MMaps/MMapAVL.v b/theories/MMaps/MMapAVL.v new file mode 100644 index 00000000..d840f1f3 --- /dev/null +++ b/theories/MMaps/MMapAVL.v @@ -0,0 +1,2158 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* Finite map library. *) + +(** * MMapAVL *) + +(** This module implements maps using AVL trees. + It follows the implementation from Ocaml's standard library. + + See the comments at the beginning of MSetAVL for more details. +*) + +Require Import Bool PeanoNat BinInt Int MMapInterface MMapList. +Require Import Orders OrdersFacts OrdersLists. + +Set Implicit Arguments. +Unset Strict Implicit. +(* For nicer extraction, we create inductive principles + only when needed *) +Local Unset Elimination Schemes. + +(** Notations and helper lemma about pairs *) + +Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope. +Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope. + +(** * The Raw functor + + Functor of pure functions + separate proofs of invariant + preservation *) + +Module Raw (Import I:Int)(X: OrderedType). +Local Open Scope pair_scope. +Local Open Scope lazy_bool_scope. +Local Open Scope Int_scope. +Local Notation int := I.t. + +Definition key := X.t. +Hint Transparent key. + +(** * Trees *) + +Section Elt. + +Variable elt : Type. + +(** * Trees + + The fifth field of [Node] is the height of the tree *) + +Inductive tree := + | Leaf : tree + | Node : tree -> key -> elt -> tree -> int -> tree. + +Notation t := tree. + +(** * Basic functions on trees: height and cardinal *) + +Definition height (m : t) : int := + match m with + | Leaf => 0 + | Node _ _ _ _ h => h + end. + +Fixpoint cardinal (m : t) : nat := + match m with + | Leaf => 0%nat + | Node l _ _ r _ => S (cardinal l + cardinal r) + end. + +(** * Empty Map *) + +Definition empty := Leaf. + +(** * Emptyness test *) + +Definition is_empty m := match m with Leaf => true | _ => false end. + +(** * Membership *) + +(** The [mem] function is deciding membership. It exploits the [Bst] property + to achieve logarithmic complexity. *) + +Fixpoint mem x m : bool := + match m with + | Leaf => false + | Node l y _ r _ => + match X.compare x y with + | Eq => true + | Lt => mem x l + | Gt => mem x r + end + end. + +Fixpoint find x m : option elt := + match m with + | Leaf => None + | Node l y d r _ => + match X.compare x y with + | Eq => Some d + | Lt => find x l + | Gt => find x r + end + end. + +(** * Helper functions *) + +(** [create l x r] creates a node, assuming [l] and [r] + to be balanced and [|height l - height r| <= 2]. *) + +Definition create l x e r := + Node l x e r (max (height l) (height r) + 1). + +(** [bal l x e r] acts as [create], but performs one step of + rebalancing if necessary, i.e. assumes [|height l - height r| <= 3]. *) + +Definition assert_false := create. + +Fixpoint bal l x d r := + let hl := height l in + let hr := height r in + if (hr+2) <? hl then + match l with + | Leaf => assert_false l x d r + | Node ll lx ld lr _ => + if (height lr) <=? (height ll) then + create ll lx ld (create lr x d r) + else + match lr with + | Leaf => assert_false l x d r + | Node lrl lrx lrd lrr _ => + create (create ll lx ld lrl) lrx lrd (create lrr x d r) + end + end + else + if (hl+2) <? hr then + match r with + | Leaf => assert_false l x d r + | Node rl rx rd rr _ => + if (height rl) <=? (height rr) then + create (create l x d rl) rx rd rr + else + match rl with + | Leaf => assert_false l x d r + | Node rll rlx rld rlr _ => + create (create l x d rll) rlx rld (create rlr rx rd rr) + end + end + else + create l x d r. + +(** * Insertion *) + +Fixpoint add x d m := + match m with + | Leaf => Node Leaf x d Leaf 1 + | Node l y d' r h => + match X.compare x y with + | Eq => Node l y d r h + | Lt => bal (add x d l) y d' r + | Gt => bal l y d' (add x d r) + end + end. + +(** * Extraction of minimum binding + + Morally, [remove_min] is to be applied to a non-empty tree + [t = Node l x e r h]. Since we can't deal here with [assert false] + for [t=Leaf], we pre-unpack [t] (and forget about [h]). +*) + +Fixpoint remove_min l x d r : t*(key*elt) := + match l with + | Leaf => (r,(x,d)) + | Node ll lx ld lr lh => + let (l',m) := remove_min ll lx ld lr in + (bal l' x d r, m) + end. + +(** * Merging two trees + + [merge0 t1 t2] builds the union of [t1] and [t2] assuming all elements + of [t1] to be smaller than all elements of [t2], and + [|height t1 - height t2| <= 2]. +*) + +Definition merge0 s1 s2 := + match s1,s2 with + | Leaf, _ => s2 + | _, Leaf => s1 + | _, Node l2 x2 d2 r2 h2 => + let '(s2',(x,d)) := remove_min l2 x2 d2 r2 in + bal s1 x d s2' + end. + +(** * Deletion *) + +Fixpoint remove x m := match m with + | Leaf => Leaf + | Node l y d r h => + match X.compare x y with + | Eq => merge0 l r + | Lt => bal (remove x l) y d r + | Gt => bal l y d (remove x r) + end + end. + +(** * join + + Same as [bal] but does not assume anything regarding heights of [l] + and [r]. +*) + +Fixpoint join l : key -> elt -> t -> t := + match l with + | Leaf => add + | Node ll lx ld lr lh => fun x d => + fix join_aux (r:t) : t := match r with + | Leaf => add x d l + | Node rl rx rd rr rh => + if rh+2 <? lh then bal ll lx ld (join lr x d r) + else if lh+2 <? rh then bal (join_aux rl) rx rd rr + else create l x d r + end + end. + +(** * Splitting + + [split x m] returns a triple [(l, o, r)] where + - [l] is the set of elements of [m] that are [< x] + - [r] is the set of elements of [m] that are [> x] + - [o] is the result of [find x m]. +*) + +Record triple := mktriple { t_left:t; t_opt:option elt; t_right:t }. +Notation "〚 l , b , r 〛" := (mktriple l b r) (at level 9). + +Fixpoint split x m : triple := match m with + | Leaf => 〚 Leaf, None, Leaf 〛 + | Node l y d r h => + match X.compare x y with + | Lt => let (ll,o,rl) := split x l in 〚 ll, o, join rl y d r 〛 + | Eq => 〚 l, Some d, r 〛 + | Gt => let (rl,o,rr) := split x r in 〚 join l y d rl, o, rr 〛 + end + end. + +(** * Concatenation + + Same as [merge] but does not assume anything about heights. +*) + +Definition concat m1 m2 := + match m1, m2 with + | Leaf, _ => m2 + | _ , Leaf => m1 + | _, Node l2 x2 d2 r2 _ => + let (m2',xd) := remove_min l2 x2 d2 r2 in + join m1 xd#1 xd#2 m2' + end. + +(** * Bindings *) + +(** [bindings_aux acc t] catenates the bindings of [t] in infix + order to the list [acc] *) + +Fixpoint bindings_aux (acc : list (key*elt)) m : list (key*elt) := + match m with + | Leaf => acc + | Node l x d r _ => bindings_aux ((x,d) :: bindings_aux acc r) l + end. + +(** then [bindings] is an instantiation with an empty [acc] *) + +Definition bindings := bindings_aux nil. + +(** * Fold *) + +Fixpoint fold {A} (f : key -> elt -> A -> A) (m : t) : A -> A := + fun a => match m with + | Leaf => a + | Node l x d r _ => fold f r (f x d (fold f l a)) + end. + +(** * Comparison *) + +Variable cmp : elt->elt->bool. + +(** ** Enumeration of the elements of a tree *) + +Inductive enumeration := + | End : enumeration + | More : key -> elt -> t -> enumeration -> enumeration. + +(** [cons m e] adds the elements of tree [m] on the head of + enumeration [e]. *) + +Fixpoint cons m e : enumeration := + match m with + | Leaf => e + | Node l x d r h => cons l (More x d r e) + end. + +(** One step of comparison of elements *) + +Definition equal_more x1 d1 (cont:enumeration->bool) e2 := + match e2 with + | End => false + | More x2 d2 r2 e2 => + match X.compare x1 x2 with + | Eq => cmp d1 d2 &&& cont (cons r2 e2) + | _ => false + end + end. + +(** Comparison of left tree, middle element, then right tree *) + +Fixpoint equal_cont m1 (cont:enumeration->bool) e2 := + match m1 with + | Leaf => cont e2 + | Node l1 x1 d1 r1 _ => + equal_cont l1 (equal_more x1 d1 (equal_cont r1 cont)) e2 + end. + +(** Initial continuation *) + +Definition equal_end e2 := match e2 with End => true | _ => false end. + +(** The complete comparison *) + +Definition equal m1 m2 := equal_cont m1 equal_end (cons m2 End). + +End Elt. +Notation t := tree. +Notation "〚 l , b , r 〛" := (mktriple l b r) (at level 9). +Notation "t #l" := (t_left t) (at level 9, format "t '#l'"). +Notation "t #o" := (t_opt t) (at level 9, format "t '#o'"). +Notation "t #r" := (t_right t) (at level 9, format "t '#r'"). + + +(** * Map *) + +Fixpoint map (elt elt' : Type)(f : elt -> elt')(m : t elt) : t elt' := + match m with + | Leaf _ => Leaf _ + | Node l x d r h => Node (map f l) x (f d) (map f r) h + end. + +(* * Mapi *) + +Fixpoint mapi (elt elt' : Type)(f : key -> elt -> elt')(m : t elt) : t elt' := + match m with + | Leaf _ => Leaf _ + | Node l x d r h => Node (mapi f l) x (f x d) (mapi f r) h + end. + +(** * Map with removal *) + +Fixpoint mapo (elt elt' : Type)(f : key -> elt -> option elt')(m : t elt) + : t elt' := + match m with + | Leaf _ => Leaf _ + | Node l x d r h => + match f x d with + | Some d' => join (mapo f l) x d' (mapo f r) + | None => concat (mapo f l) (mapo f r) + end + end. + +(** * Generalized merge + + Suggestion by B. Gregoire: a [merge] function with specialized + arguments that allows bypassing some tree traversal. Instead of one + [f0] of type [key -> option elt -> option elt' -> option elt''], + we ask here for: + - [f] which is a specialisation of [f0] when first option isn't [None] + - [mapl] treats a [tree elt] with [f0] when second option is [None] + - [mapr] treats a [tree elt'] with [f0] when first option is [None] + + The idea is that [mapl] and [mapr] can be instantaneous (e.g. + the identity or some constant function). +*) + +Section GMerge. +Variable elt elt' elt'' : Type. +Variable f : key -> elt -> option elt' -> option elt''. +Variable mapl : t elt -> t elt''. +Variable mapr : t elt' -> t elt''. + +Fixpoint gmerge m1 m2 := + match m1, m2 with + | Leaf _, _ => mapr m2 + | _, Leaf _ => mapl m1 + | Node l1 x1 d1 r1 h1, _ => + let (l2',o2,r2') := split x1 m2 in + match f x1 d1 o2 with + | Some e => join (gmerge l1 l2') x1 e (gmerge r1 r2') + | None => concat (gmerge l1 l2') (gmerge r1 r2') + end + end. + +End GMerge. + +(** * Merge + + The [merge] function of the Map interface can be implemented + via [gmerge] and [mapo]. +*) + +Section Merge. +Variable elt elt' elt'' : Type. +Variable f : key -> option elt -> option elt' -> option elt''. + +Definition merge : t elt -> t elt' -> t elt'' := + gmerge + (fun k d o => f k (Some d) o) + (mapo (fun k d => f k (Some d) None)) + (mapo (fun k d' => f k None (Some d'))). + +End Merge. + + + +(** * Invariants *) + +Section Invariants. +Variable elt : Type. + +(** ** Occurrence in a tree *) + +Inductive MapsTo (x : key)(e : elt) : t elt -> Prop := + | MapsRoot : forall l r h y, + X.eq x y -> MapsTo x e (Node l y e r h) + | MapsLeft : forall l r h y e', + MapsTo x e l -> MapsTo x e (Node l y e' r h) + | MapsRight : forall l r h y e', + MapsTo x e r -> MapsTo x e (Node l y e' r h). + +Inductive In (x : key) : t elt -> Prop := + | InRoot : forall l r h y e, + X.eq x y -> In x (Node l y e r h) + | InLeft : forall l r h y e', + In x l -> In x (Node l y e' r h) + | InRight : forall l r h y e', + In x r -> In x (Node l y e' r h). + +Definition In0 k m := exists e:elt, MapsTo k e m. + +(** ** Binary search trees *) + +(** [Above x m] : [x] is strictly greater than any key in [m]. + [Below x m] : [x] is strictly smaller than any key in [m]. *) + +Inductive Above (x:key) : t elt -> Prop := + | AbLeaf : Above x (Leaf _) + | AbNode l r h y e : Above x l -> X.lt y x -> Above x r -> + Above x (Node l y e r h). + +Inductive Below (x:key) : t elt -> Prop := + | BeLeaf : Below x (Leaf _) + | BeNode l r h y e : Below x l -> X.lt x y -> Below x r -> + Below x (Node l y e r h). + +Definition Apart (m1 m2 : t elt) : Prop := + forall x1 x2, In x1 m1 -> In x2 m2 -> X.lt x1 x2. + +(** Alternative statements, equivalent with [LtTree] and [GtTree] *) + +Definition lt_tree x m := forall y, In y m -> X.lt y x. +Definition gt_tree x m := forall y, In y m -> X.lt x y. + +(** [Bst t] : [t] is a binary search tree *) + +Inductive Bst : t elt -> Prop := + | BSLeaf : Bst (Leaf _) + | BSNode : forall x e l r h, Bst l -> Bst r -> + Above x l -> Below x r -> Bst (Node l x e r h). + +End Invariants. + + +(** * Correctness proofs, isolated in a sub-module *) + +Module Proofs. + Module MX := OrderedTypeFacts X. + Module PX := KeyOrderedType X. + Module L := MMapList.Raw X. + +Local Infix "∈" := In (at level 70). +Local Infix "==" := X.eq (at level 70). +Local Infix "<" := X.lt (at level 70). +Local Infix "<<" := Below (at level 70). +Local Infix ">>" := Above (at level 70). +Local Infix "<<<" := Apart (at level 70). + +Scheme tree_ind := Induction for tree Sort Prop. +Scheme Bst_ind := Induction for Bst Sort Prop. +Scheme MapsTo_ind := Induction for MapsTo Sort Prop. +Scheme In_ind := Induction for In Sort Prop. +Scheme Above_ind := Induction for Above Sort Prop. +Scheme Below_ind := Induction for Below Sort Prop. + +Functional Scheme mem_ind := Induction for mem Sort Prop. +Functional Scheme find_ind := Induction for find Sort Prop. +Functional Scheme bal_ind := Induction for bal Sort Prop. +Functional Scheme add_ind := Induction for add Sort Prop. +Functional Scheme remove_min_ind := Induction for remove_min Sort Prop. +Functional Scheme merge0_ind := Induction for merge0 Sort Prop. +Functional Scheme remove_ind := Induction for remove Sort Prop. +Functional Scheme concat_ind := Induction for concat Sort Prop. +Functional Scheme split_ind := Induction for split Sort Prop. +Functional Scheme mapo_ind := Induction for mapo Sort Prop. +Functional Scheme gmerge_ind := Induction for gmerge Sort Prop. + +(** * Automation and dedicated tactics. *) + +Local Hint Constructors tree MapsTo In Bst Above Below. +Local Hint Unfold lt_tree gt_tree Apart. +Local Hint Immediate MX.eq_sym. +Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans. + +Tactic Notation "factornode" ident(s) := + try clear s; + match goal with + | |- context [Node ?l ?x ?e ?r ?h] => + set (s:=Node l x e r h) in *; clearbody s; clear l x e r h + | _ : context [Node ?l ?x ?e ?r ?h] |- _ => + set (s:=Node l x e r h) in *; clearbody s; clear l x e r h + end. + +(** A tactic for cleaning hypothesis after use of functional induction. *) + +Ltac cleanf := + match goal with + | H : X.compare _ _ = Eq |- _ => + rewrite ?H; apply MX.compare_eq in H; cleanf + | H : X.compare _ _ = Lt |- _ => + rewrite ?H; apply MX.compare_lt_iff in H; cleanf + | H : X.compare _ _ = Gt |- _ => + rewrite ?H; apply MX.compare_gt_iff in H; cleanf + | _ => idtac + end. + + +(** A tactic to repeat [inversion_clear] on all hyps of the + form [(f (Node ...))] *) + +Ltac inv f := + match goal with + | H:f (Leaf _) |- _ => inversion_clear H; inv f + | H:f _ (Leaf _) |- _ => inversion_clear H; inv f + | H:f _ _ (Leaf _) |- _ => inversion_clear H; inv f + | H:f _ _ _ (Leaf _) |- _ => inversion_clear H; inv f + | H:f (Node _ _ _ _ _) |- _ => inversion_clear H; inv f + | H:f _ (Node _ _ _ _ _) |- _ => inversion_clear H; inv f + | H:f _ _ (Node _ _ _ _ _) |- _ => inversion_clear H; inv f + | H:f _ _ _ (Node _ _ _ _ _) |- _ => inversion_clear H; inv f + | _ => idtac + end. + +Ltac inv_all f := + match goal with + | H: f _ |- _ => inversion_clear H; inv f + | H: f _ _ |- _ => inversion_clear H; inv f + | H: f _ _ _ |- _ => inversion_clear H; inv f + | H: f _ _ _ _ |- _ => inversion_clear H; inv f + | _ => idtac + end. + +Ltac intuition_in := repeat (intuition; inv In; inv MapsTo). + +(* Function/Functional Scheme can't deal with internal fix. + Let's do its job by hand: *) + +Ltac join_tac l x d r := + revert x d r; + induction l as [| ll _ lx ld lr Hlr lh]; + [ | intros x d r; induction r as [| rl Hrl rx rd rr _ rh]; unfold join; + [ | destruct (rh+2 <? lh) eqn:LT; + [ match goal with |- context [ bal ?u ?v ?w ?z ] => + replace (bal u v w z) + with (bal ll lx ld (join lr x d (Node rl rx rd rr rh))); [ | auto] + end + | destruct (lh+2 <? rh) eqn:LT'; + [ match goal with |- context [ bal ?u ?v ?w ?z ] => + replace (bal u v w z) + with (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr); [ | auto] + end + | ] ] ] ]; intros. + +Ltac cleansplit := + simpl; cleanf; inv Bst; + match goal with + | E:split _ _ = 〚 ?l, ?o, ?r 〛 |- _ => + change l with (〚l,o,r〛#l); rewrite <- ?E; + change o with (〚l,o,r〛#o); rewrite <- ?E; + change r with (〚l,o,r〛#r); rewrite <- ?E + | _ => idtac + end. + +(** * Basic results about [MapsTo], [In], [lt_tree], [gt_tree], [height] *) + +(** Facts about [MapsTo] and [In]. *) + +Lemma MapsTo_In {elt} k (e:elt) m : MapsTo k e m -> k ∈ m. +Proof. + induction 1; auto. +Qed. +Local Hint Resolve MapsTo_In. + +Lemma In_MapsTo {elt} k m : k ∈ m -> exists (e:elt), MapsTo k e m. +Proof. + induction 1; try destruct IHIn as (e,He); exists e; auto. +Qed. + +Lemma In_alt {elt} k (m:t elt) : In0 k m <-> k ∈ m. +Proof. + split. + intros (e,H); eauto. + unfold In0; apply In_MapsTo; auto. +Qed. + +Lemma MapsTo_1 {elt} m x y (e:elt) : + x == y -> MapsTo x e m -> MapsTo y e m. +Proof. + induction m; simpl; intuition_in; eauto. +Qed. +Hint Immediate MapsTo_1. + +Instance MapsTo_compat {elt} : + Proper (X.eq==>Logic.eq==>Logic.eq==>iff) (@MapsTo elt). +Proof. + intros x x' Hx e e' He m m' Hm. subst. + split; now apply MapsTo_1. +Qed. + +Instance In_compat {elt} : + Proper (X.eq==>Logic.eq==>iff) (@In elt). +Proof. + intros x x' H m m' <-. + induction m; simpl; intuition_in; eauto. +Qed. + +Lemma In_node_iff {elt} l x (e:elt) r h y : + y ∈ (Node l x e r h) <-> y ∈ l \/ y == x \/ y ∈ r. +Proof. + intuition_in. +Qed. + +(** Results about [Above] and [Below] *) + +Lemma above {elt} (m:t elt) x : + x >> m <-> forall y, y ∈ m -> y < x. +Proof. + split. + - induction 1; intuition_in; MX.order. + - induction m; constructor; auto. +Qed. + +Lemma below {elt} (m:t elt) x : + x << m <-> forall y, y ∈ m -> x < y. +Proof. + split. + - induction 1; intuition_in; MX.order. + - induction m; constructor; auto. +Qed. + +Lemma AboveLt {elt} (m:t elt) x y : x >> m -> y ∈ m -> y < x. +Proof. + rewrite above; intuition. +Qed. + +Lemma BelowGt {elt} (m:t elt) x y : x << m -> y ∈ m -> x < y. +Proof. + rewrite below; intuition. +Qed. + +Lemma Above_not_In {elt} (m:t elt) x : x >> m -> ~ x ∈ m. +Proof. + induction 1; intuition_in; MX.order. +Qed. + +Lemma Below_not_In {elt} (m:t elt) x : x << m -> ~ x ∈ m. +Proof. + induction 1; intuition_in; MX.order. +Qed. + +Lemma Above_trans {elt} (m:t elt) x y : x < y -> x >> m -> y >> m. +Proof. + induction 2; constructor; trivial; MX.order. +Qed. + +Lemma Below_trans {elt} (m:t elt) x y : y < x -> x << m -> y << m. +Proof. + induction 2; constructor; trivial; MX.order. +Qed. + +Local Hint Resolve + AboveLt Above_not_In Above_trans + BelowGt Below_not_In Below_trans. + +(** Helper tactic concerning order of elements. *) + +Ltac order := match goal with + | U: _ >> ?m, V: _ ∈ ?m |- _ => + generalize (AboveLt U V); clear U; order + | U: _ << ?m, V: _ ∈ ?m |- _ => + generalize (BelowGt U V); clear U; order + | U: _ >> ?m, V: MapsTo _ _ ?m |- _ => + generalize (AboveLt U (MapsTo_In V)); clear U; order + | U: _ << ?m, V: MapsTo _ _ ?m |- _ => + generalize (BelowGt U (MapsTo_In V)); clear U; order + | _ => MX.order +end. + +Lemma between {elt} (m m':t elt) x : + x >> m -> x << m' -> m <<< m'. +Proof. + intros H H' y y' Hy Hy'. order. +Qed. + +Section Elt. +Variable elt:Type. +Implicit Types m r : t elt. + +(** * Membership *) + +Lemma find_1 m x e : Bst m -> MapsTo x e m -> find x m = Some e. +Proof. + functional induction (find x m); cleanf; + intros; inv Bst; intuition_in; order. +Qed. + +Lemma find_2 m x e : find x m = Some e -> MapsTo x e m. +Proof. + functional induction (find x m); cleanf; subst; intros; auto. + - discriminate. + - injection H as ->. auto. +Qed. + +Lemma find_spec m x e : Bst m -> + (find x m = Some e <-> MapsTo x e m). +Proof. + split; auto using find_1, find_2. +Qed. + +Lemma find_in m x : find x m <> None -> x ∈ m. +Proof. + destruct (find x m) eqn:F; intros H. + - apply MapsTo_In with e. now apply find_2. + - now elim H. +Qed. + +Lemma in_find m x : Bst m -> x ∈ m -> find x m <> None. +Proof. + intros H H'. + destruct (In_MapsTo H') as (d,Hd). + now rewrite (find_1 H Hd). +Qed. + +Lemma find_in_iff m x : Bst m -> + (find x m <> None <-> x ∈ m). +Proof. + split; auto using find_in, in_find. +Qed. + +Lemma not_find_iff m x : Bst m -> + (find x m = None <-> ~ x ∈ m). +Proof. + intros H. rewrite <- find_in_iff; trivial. + destruct (find x m); split; try easy. now destruct 1. +Qed. + +Lemma eq_option_alt (o o':option elt) : + o=o' <-> (forall e, o=Some e <-> o'=Some e). +Proof. +split; intros. +- now subst. +- destruct o, o'; rewrite ?H; auto. symmetry; now apply H. +Qed. + +Lemma find_mapsto_equiv : forall m m' x, Bst m -> Bst m' -> + (find x m = find x m' <-> + (forall d, MapsTo x d m <-> MapsTo x d m')). +Proof. + intros m m' x Hm Hm'. rewrite eq_option_alt. + split; intros H d. now rewrite <- 2 find_spec. now rewrite 2 find_spec. +Qed. + +Lemma find_in_equiv : forall m m' x, Bst m -> Bst m' -> + find x m = find x m' -> + (x ∈ m <-> x ∈ m'). +Proof. + split; intros; apply find_in; [ rewrite <- H1 | rewrite H1 ]; + apply in_find; auto. +Qed. + +Lemma find_compat m x x' : Bst m -> X.eq x x' -> find x m = find x' m. +Proof. + intros B E. + destruct (find x' m) eqn:H. + - apply find_1; trivial. rewrite E. now apply find_2. + - rewrite not_find_iff in *; trivial. now rewrite E. +Qed. + +Lemma mem_spec m x : Bst m -> mem x m = true <-> x ∈ m. +Proof. + functional induction (mem x m); auto; intros; cleanf; + inv Bst; intuition_in; try discriminate; order. +Qed. + +(** * Empty map *) + +Lemma empty_bst : Bst (empty elt). +Proof. + constructor. +Qed. + +Lemma empty_spec x : find x (empty elt) = None. +Proof. + reflexivity. +Qed. + +(** * Emptyness test *) + +Lemma is_empty_spec m : is_empty m = true <-> forall x, find x m = None. +Proof. + destruct m as [|r x e l h]; simpl; split; try easy. + intros H. specialize (H x). now rewrite MX.compare_refl in H. +Qed. + +(** * Helper functions *) + +Lemma create_bst l x e r : + Bst l -> Bst r -> x >> l -> x << r -> Bst (create l x e r). +Proof. + unfold create; auto. +Qed. +Hint Resolve create_bst. + +Lemma create_in l x e r y : + y ∈ (create l x e r) <-> y == x \/ y ∈ l \/ y ∈ r. +Proof. + unfold create; split; [ inversion_clear 1 | ]; intuition. +Qed. + +Lemma bal_bst l x e r : Bst l -> Bst r -> + x >> l -> x << r -> Bst (bal l x e r). +Proof. + functional induction (bal l x e r); intros; cleanf; + inv Bst; inv Above; inv Below; + repeat apply create_bst; auto; unfold create; constructor; eauto. +Qed. +Hint Resolve bal_bst. + +Lemma bal_in l x e r y : + y ∈ (bal l x e r) <-> y == x \/ y ∈ l \/ y ∈ r. +Proof. + functional induction (bal l x e r); intros; cleanf; + rewrite !create_in; intuition_in. +Qed. + +Lemma bal_mapsto l x e r y e' : + MapsTo y e' (bal l x e r) <-> MapsTo y e' (create l x e r). +Proof. + functional induction (bal l x e r); intros; cleanf; + unfold assert_false, create; intuition_in. +Qed. + +Lemma bal_find l x e r y : + Bst l -> Bst r -> x >> l -> x << r -> + find y (bal l x e r) = find y (create l x e r). +Proof. + functional induction (bal l x e r); intros; cleanf; trivial; + inv Bst; inv Above; inv Below; + simpl; repeat case X.compare_spec; intuition; order. +Qed. + +(** * Insertion *) + +Lemma add_in m x y e : + y ∈ (add x e m) <-> y == x \/ y ∈ m. +Proof. + functional induction (add x e m); auto; intros; cleanf; + rewrite ?bal_in; intuition_in. setoid_replace y with x; auto. +Qed. + +Lemma add_lt m x e y : y >> m -> x < y -> y >> add x e m. +Proof. + intros. apply above. intros z. rewrite add_in. destruct 1; order. +Qed. + +Lemma add_gt m x e y : y << m -> y < x -> y << add x e m. +Proof. + intros. apply below. intros z. rewrite add_in. destruct 1; order. +Qed. + +Lemma add_bst m x e : Bst m -> Bst (add x e m). +Proof. + functional induction (add x e m); intros; cleanf; + inv Bst; try apply bal_bst; auto using add_lt, add_gt. +Qed. +Hint Resolve add_lt add_gt add_bst. + +Lemma add_spec1 m x e : Bst m -> find x (add x e m) = Some e. +Proof. + functional induction (add x e m); simpl; intros; cleanf; trivial. + - now rewrite MX.compare_refl. + - inv Bst. rewrite bal_find; auto. + simpl. case X.compare_spec; try order; auto. + - inv Bst. rewrite bal_find; auto. + simpl. case X.compare_spec; try order; auto. +Qed. + +Lemma add_spec2 m x y e : Bst m -> ~ x == y -> + find y (add x e m) = find y m. +Proof. + functional induction (add x e m); simpl; intros; cleanf; trivial. + - case X.compare_spec; trivial; order. + - case X.compare_spec; trivial; order. + - inv Bst. rewrite bal_find by auto. simpl. now rewrite IHt. + - inv Bst. rewrite bal_find by auto. simpl. now rewrite IHt. +Qed. + +Lemma add_find m x y e : Bst m -> + find y (add x e m) = + match X.compare y x with Eq => Some e | _ => find y m end. +Proof. + intros. + case X.compare_spec; intros. + - apply find_spec; auto. rewrite H0. apply find_spec; auto. + now apply add_spec1. + - apply add_spec2; trivial; order. + - apply add_spec2; trivial; order. +Qed. + +(** * Extraction of minimum binding *) + +Definition RemoveMin m res := + match m with + | Leaf _ => False + | Node l x e r h => remove_min l x e r = res + end. + +Lemma RemoveMin_step l x e r h m' p : + RemoveMin (Node l x e r h) (m',p) -> + (l = Leaf _ /\ m' = r /\ p = (x,e) \/ + exists m0, RemoveMin l (m0,p) /\ m' = bal m0 x e r). +Proof. + simpl. destruct l as [|ll lx le lr lh]; simpl. + - intros [= -> ->]. now left. + - destruct (remove_min ll lx le lr) as (l',p'). + intros [= <- <-]. right. now exists l'. +Qed. + +Lemma remove_min_mapsto m m' p : RemoveMin m (m',p) -> + forall y e, + MapsTo y e m <-> (y == p#1 /\ e = p#2) \/ MapsTo y e m'. +Proof. + revert m'. + induction m as [|l IH x d r _ h]; [destruct 1|]. + intros m' R. apply RemoveMin_step in R. + destruct R as [(->,(->,->))|[m0 (R,->)]]; intros y e; simpl. + - intuition_in. subst. now constructor. + - rewrite bal_mapsto. unfold create. specialize (IH _ R y e). + intuition_in. +Qed. + +Lemma remove_min_in m m' p : RemoveMin m (m',p) -> + forall y, y ∈ m <-> y == p#1 \/ y ∈ m'. +Proof. + revert m'. + induction m as [|l IH x e r _ h]; [destruct 1|]. + intros m' R y. apply RemoveMin_step in R. + destruct R as [(->,(->,->))|[m0 (R,->)]]. + + intuition_in. + + rewrite bal_in, In_node_iff, (IH _ R); intuition. +Qed. + +Lemma remove_min_lt m m' p : RemoveMin m (m',p) -> + forall y, y >> m -> y >> m'. +Proof. + intros R y L. apply above. intros z Hz. + apply (AboveLt L). + apply (remove_min_in R). now right. +Qed. + +Lemma remove_min_gt m m' p : RemoveMin m (m',p) -> + Bst m -> p#1 << m'. +Proof. + revert m'. + induction m as [|l IH x e r _ h]; [destruct 1|]. + intros m' R H. inv Bst. apply RemoveMin_step in R. + destruct R as [(_,(->,->))|[m0 (R,->)]]; auto. + assert (p#1 << m0) by now apply IH. + assert (In p#1 l) by (apply (remove_min_in R); now left). + apply below. intros z. rewrite bal_in. + intuition_in; order. +Qed. + +Lemma remove_min_bst m m' p : RemoveMin m (m',p) -> + Bst m -> Bst m'. +Proof. + revert m'. + induction m as [|l IH x e r _ h]; [destruct 1|]. + intros m' R H. inv Bst. apply RemoveMin_step in R. + destruct R as [(_,(->,->))|[m0 (R,->)]]; auto. + apply bal_bst; eauto using remove_min_lt. +Qed. + +Lemma remove_min_find m m' p : RemoveMin m (m',p) -> + Bst m -> + forall y, + find y m = + match X.compare y p#1 with + | Eq => Some p#2 + | Lt => None + | Gt => find y m' + end. +Proof. + revert m'. + induction m as [|l IH x e r _ h]; [destruct 1|]. + intros m' R B y. inv Bst. apply RemoveMin_step in R. + destruct R as [(->,(->,->))|[m0 (R,->)]]; auto. + assert (Bst m0) by now apply (remove_min_bst R). + assert (p#1 << m0) by now apply (remove_min_gt R). + assert (x >> m0) by now apply (remove_min_lt R). + assert (In p#1 l) by (apply (remove_min_in R); now left). + simpl in *. + rewrite (IH _ R), bal_find by trivial. clear IH. simpl. + do 2 case X.compare_spec; trivial; try order. +Qed. + +(** * Merging two trees *) + +Ltac factor_remove_min m R := match goal with + | h:int, H:remove_min ?l ?x ?e ?r = ?p |- _ => + assert (R:RemoveMin (Node l x e r h) p) by exact H; + set (m:=Node l x e r h) in *; clearbody m; clear H l x e r +end. + +Lemma merge0_in m1 m2 y : + y ∈ (merge0 m1 m2) <-> y ∈ m1 \/ y ∈ m2. +Proof. + functional induction (merge0 m1 m2); intros; try factornode m1. + - intuition_in. + - intuition_in. + - factor_remove_min l R. rewrite bal_in, (remove_min_in R). + simpl; intuition. +Qed. + +Lemma merge0_mapsto m1 m2 y e : + MapsTo y e (merge0 m1 m2) <-> MapsTo y e m1 \/ MapsTo y e m2. +Proof. + functional induction (merge0 m1 m2); intros; try factornode m1. + - intuition_in. + - intuition_in. + - factor_remove_min l R. rewrite bal_mapsto, (remove_min_mapsto R). + simpl. unfold create; intuition_in. subst. now constructor. +Qed. + +Lemma merge0_bst m1 m2 : Bst m1 -> Bst m2 -> m1 <<< m2 -> + Bst (merge0 m1 m2). +Proof. + functional induction (merge0 m1 m2); intros B1 B2 B12; trivial. + factornode m1. factor_remove_min l R. + apply bal_bst; auto. + - eapply remove_min_bst; eauto. + - apply above. intros z Hz. apply B12; trivial. + rewrite (remove_min_in R). now left. + - now apply (remove_min_gt R). +Qed. +Hint Resolve merge0_bst. + +(** * Deletion *) + +Lemma remove_in m x y : Bst m -> + (y ∈ remove x m <-> ~ y == x /\ y ∈ m). +Proof. + functional induction (remove x m); simpl; intros; cleanf; inv Bst; + rewrite ?merge0_in, ?bal_in, ?IHt; intuition_in; order. +Qed. + +Lemma remove_lt m x y : Bst m -> y >> m -> y >> remove x m. +Proof. + intros. apply above. intro. rewrite remove_in by trivial. + destruct 1; order. +Qed. + +Lemma remove_gt m x y : Bst m -> y << m -> y << remove x m. +Proof. + intros. apply below. intro. rewrite remove_in by trivial. + destruct 1; order. +Qed. + +Lemma remove_bst m x : Bst m -> Bst (remove x m). +Proof. + functional induction (remove x m); simpl; intros; cleanf; inv Bst. + - trivial. + - apply merge0_bst; eauto. + - apply bal_bst; auto using remove_lt. + - apply bal_bst; auto using remove_gt. +Qed. +Hint Resolve remove_bst remove_gt remove_lt. + +Lemma remove_spec1 m x : Bst m -> find x (remove x m) = None. +Proof. + intros. apply not_find_iff; auto. rewrite remove_in; intuition. +Qed. + +Lemma remove_spec2 m x y : Bst m -> ~ x == y -> + find y (remove x m) = find y m. +Proof. + functional induction (remove x m); simpl; intros; cleanf; inv Bst. + - trivial. + - case X.compare_spec; intros; try order; + rewrite find_mapsto_equiv; auto. + + intros. rewrite merge0_mapsto; intuition; order. + + apply merge0_bst; auto. red; intros; transitivity y0; order. + + intros. rewrite merge0_mapsto; intuition; order. + + apply merge0_bst; auto. now apply between with y0. + - rewrite bal_find by auto. simpl. case X.compare_spec; auto. + - rewrite bal_find by auto. simpl. case X.compare_spec; auto. +Qed. + +(** * join *) + +Lemma join_in l x d r y : + y ∈ (join l x d r) <-> y == x \/ y ∈ l \/ y ∈ r. +Proof. + join_tac l x d r. + - simpl join. rewrite add_in. intuition_in. + - rewrite add_in. intuition_in. + - rewrite bal_in, Hlr. clear Hlr Hrl. intuition_in. + - rewrite bal_in, Hrl; clear Hlr Hrl; intuition_in. + - apply create_in. +Qed. + +Lemma join_bst l x d r : + Bst (create l x d r) -> Bst (join l x d r). +Proof. + join_tac l x d r; unfold create in *; + inv Bst; inv Above; inv Below; auto. + - simpl. auto. + - apply bal_bst; auto. + apply below. intro. rewrite join_in. intuition_in; order. + - apply bal_bst; auto. + apply above. intro. rewrite join_in. intuition_in; order. +Qed. +Hint Resolve join_bst. + +Lemma join_find l x d r y : + Bst (create l x d r) -> + find y (join l x d r) = find y (create l x d r). +Proof. + unfold create at 1. + join_tac l x d r; trivial. + - simpl in *. inv Bst. + rewrite add_find; trivial. + case X.compare_spec; intros; trivial. + apply not_find_iff; auto. intro. order. + - clear Hlr. factornode l. simpl. inv Bst. + rewrite add_find by auto. + case X.compare_spec; intros; trivial. + apply not_find_iff; auto. intro. order. + - clear Hrl LT. factornode r. inv Bst; inv Above; inv Below. + rewrite bal_find; auto; simpl. + + rewrite Hlr; auto; simpl. + repeat (case X.compare_spec; trivial; try order). + + apply below. intro. rewrite join_in. intuition_in; order. + - clear Hlr LT LT'. factornode l. inv Bst; inv Above; inv Below. + rewrite bal_find; auto; simpl. + + rewrite Hrl; auto; simpl. + repeat (case X.compare_spec; trivial; try order). + + apply above. intro. rewrite join_in. intuition_in; order. +Qed. + +(** * split *) + +Lemma split_in_l0 m x y : y ∈ (split x m)#l -> y ∈ m. +Proof. + functional induction (split x m); cleansplit; + rewrite ?join_in; intuition. +Qed. + +Lemma split_in_r0 m x y : y ∈ (split x m)#r -> y ∈ m. +Proof. + functional induction (split x m); cleansplit; + rewrite ?join_in; intuition. +Qed. + +Lemma split_in_l m x y : Bst m -> + (y ∈ (split x m)#l <-> y ∈ m /\ y < x). +Proof. + functional induction (split x m); intros; cleansplit; + rewrite ?join_in, ?IHt; intuition_in; order. +Qed. + +Lemma split_in_r m x y : Bst m -> + (y ∈ (split x m)#r <-> y ∈ m /\ x < y). +Proof. + functional induction (split x m); intros; cleansplit; + rewrite ?join_in, ?IHt; intuition_in; order. +Qed. + +Lemma split_in_o m x : (split x m)#o = find x m. +Proof. + functional induction (split x m); intros; cleansplit; auto. +Qed. + +Lemma split_lt_l m x : Bst m -> x >> (split x m)#l. +Proof. + intro. apply above. intro. rewrite split_in_l; intuition; order. +Qed. + +Lemma split_lt_r m x y : y >> m -> y >> (split x m)#r. +Proof. + intro. apply above. intros z Hz. apply split_in_r0 in Hz. order. +Qed. + +Lemma split_gt_r m x : Bst m -> x << (split x m)#r. +Proof. + intro. apply below. intro. rewrite split_in_r; intuition; order. +Qed. + +Lemma split_gt_l m x y : y << m -> y << (split x m)#l. +Proof. + intro. apply below. intros z Hz. apply split_in_l0 in Hz. order. +Qed. +Hint Resolve split_lt_l split_lt_r split_gt_l split_gt_r. + +Lemma split_bst_l m x : Bst m -> Bst (split x m)#l. +Proof. + functional induction (split x m); intros; cleansplit; intuition; + auto using join_bst. +Qed. + +Lemma split_bst_r m x : Bst m -> Bst (split x m)#r. +Proof. + functional induction (split x m); intros; cleansplit; intuition; + auto using join_bst. +Qed. +Hint Resolve split_bst_l split_bst_r. + +Lemma split_find m x y : Bst m -> + find y m = match X.compare y x with + | Eq => (split x m)#o + | Lt => find y (split x m)#l + | Gt => find y (split x m)#r + end. +Proof. + functional induction (split x m); intros; cleansplit. + - now case X.compare. + - repeat case X.compare_spec; trivial; order. + - simpl in *. rewrite join_find, IHt; auto. + simpl. repeat case X.compare_spec; trivial; order. + - rewrite join_find, IHt; auto. + simpl; repeat case X.compare_spec; trivial; order. +Qed. + +(** * Concatenation *) + +Lemma concat_in m1 m2 y : + y ∈ (concat m1 m2) <-> y ∈ m1 \/ y ∈ m2. +Proof. + functional induction (concat m1 m2); intros; try factornode m1. + - intuition_in. + - intuition_in. + - factor_remove_min m2 R. + rewrite join_in, (remove_min_in R); simpl; intuition. +Qed. + +Lemma concat_bst m1 m2 : Bst m1 -> Bst m2 -> m1 <<< m2 -> + Bst (concat m1 m2). +Proof. + functional induction (concat m1 m2); intros B1 B2 LT; auto; + try factornode m1. + factor_remove_min m2 R. + apply join_bst, create_bst; auto. + - now apply (remove_min_bst R). + - apply above. intros y Hy. apply LT; trivial. + rewrite (remove_min_in R); now left. + - now apply (remove_min_gt R). +Qed. +Hint Resolve concat_bst. + +Definition oelse {A} (o1 o2:option A) := + match o1 with + | Some x => Some x + | None => o2 + end. + +Lemma concat_find m1 m2 y : Bst m1 -> Bst m2 -> m1 <<< m2 -> + find y (concat m1 m2) = oelse (find y m2) (find y m1). +Proof. + functional induction (concat m1 m2); intros B1 B2 B; auto; try factornode m1. + - destruct (find y m2); auto. + - factor_remove_min m2 R. + assert (xd#1 >> m1). + { apply above. intros z Hz. apply B; trivial. + rewrite (remove_min_in R). now left. } + rewrite join_find; simpl; auto. + + rewrite (remove_min_find R B2 y). + case X.compare_spec; intros; auto. + destruct (find y m2'); trivial. + simpl. symmetry. apply not_find_iff; eauto. + + apply create_bst; auto. + * now apply (remove_min_bst R). + * now apply (remove_min_gt R). +Qed. + + +(** * Elements *) + +Notation eqk := (PX.eqk (elt:= elt)). +Notation eqke := (PX.eqke (elt:= elt)). +Notation ltk := (PX.ltk (elt:= elt)). + +Lemma bindings_aux_mapsto : forall (s:t elt) acc x e, + InA eqke (x,e) (bindings_aux acc s) <-> MapsTo x e s \/ InA eqke (x,e) acc. +Proof. + induction s as [ | l Hl x e r Hr h ]; simpl; auto. + intuition. + inversion H0. + intros. + rewrite Hl. + destruct (Hr acc x0 e0); clear Hl Hr. + intuition; inversion_clear H3; intuition. + compute in H0. destruct H0; simpl in *; subst; intuition. +Qed. + +Lemma bindings_mapsto : forall (s:t elt) x e, + InA eqke (x,e) (bindings s) <-> MapsTo x e s. +Proof. + intros; generalize (bindings_aux_mapsto s nil x e); intuition. + inversion_clear H0. +Qed. + +Lemma bindings_in : forall (s:t elt) x, L.PX.In x (bindings s) <-> x ∈ s. +Proof. + intros. + unfold L.PX.In. + rewrite <- In_alt; unfold In0. + split; intros (y,H); exists y. + - now rewrite <- bindings_mapsto. + - unfold L.PX.MapsTo; now rewrite bindings_mapsto. +Qed. + +Lemma bindings_aux_sort : forall (s:t elt) acc, + Bst s -> sort ltk acc -> + (forall x e y, InA eqke (x,e) acc -> y ∈ s -> y < x) -> + sort ltk (bindings_aux acc s). +Proof. + induction s as [ | l Hl y e r Hr h]; simpl; intuition. + inv Bst. + apply Hl; auto. + - constructor. + + apply Hr; eauto. + + clear Hl Hr. + apply InA_InfA with (eqA:=eqke); auto with *. + intros (y',e') Hy'. + apply bindings_aux_mapsto in Hy'. compute. intuition; eauto. + - clear Hl Hr. intros x e' y' Hx Hy'. + inversion_clear Hx. + + compute in H. destruct H; simpl in *. order. + + apply bindings_aux_mapsto in H. intuition eauto. +Qed. + +Lemma bindings_sort : forall s : t elt, Bst s -> sort ltk (bindings s). +Proof. + intros; unfold bindings; apply bindings_aux_sort; auto. + intros; inversion H0. +Qed. +Hint Resolve bindings_sort. + +Lemma bindings_nodup : forall s : t elt, Bst s -> NoDupA eqk (bindings s). +Proof. + intros; apply PX.Sort_NoDupA; auto. +Qed. + +Lemma bindings_aux_cardinal m acc : + (length acc + cardinal m)%nat = length (bindings_aux acc m). +Proof. + revert acc. induction m; simpl; intuition. + rewrite <- IHm1; simpl. + rewrite <- IHm2. rewrite Nat.add_succ_r, <- Nat.add_assoc. + f_equal. f_equal. apply Nat.add_comm. +Qed. + +Lemma bindings_cardinal m : cardinal m = length (bindings m). +Proof. + exact (bindings_aux_cardinal m nil). +Qed. + +Lemma bindings_app : + forall (s:t elt) acc, bindings_aux acc s = bindings s ++ acc. +Proof. + induction s; simpl; intros; auto. + rewrite IHs1, IHs2. + unfold bindings; simpl. + rewrite 2 IHs1, IHs2, !app_nil_r, !app_ass; auto. +Qed. + +Lemma bindings_node : + forall (t1 t2:t elt) x e z l, + bindings t1 ++ (x,e) :: bindings t2 ++ l = + bindings (Node t1 x e t2 z) ++ l. +Proof. + unfold bindings; simpl; intros. + rewrite !bindings_app, !app_nil_r, !app_ass; auto. +Qed. + +(** * Fold *) + +Definition fold' {A} (f : key -> elt -> A -> A)(s : t elt) := + L.fold f (bindings s). + +Lemma fold_equiv_aux {A} (s : t elt) (f : key -> elt -> A -> A) (a : A) acc : + L.fold f (bindings_aux acc s) a = L.fold f acc (fold f s a). +Proof. + revert a acc. + induction s; simpl; trivial. + intros. rewrite IHs1. simpl. apply IHs2. +Qed. + +Lemma fold_equiv {A} (s : t elt) (f : key -> elt -> A -> A) (a : A) : + fold f s a = fold' f s a. +Proof. + unfold fold', bindings. now rewrite fold_equiv_aux. +Qed. + +Lemma fold_spec (s:t elt)(Hs:Bst s){A}(i:A)(f : key -> elt -> A -> A) : + fold f s i = fold_left (fun a p => f p#1 p#2 a) (bindings s) i. +Proof. + rewrite fold_equiv. unfold fold'. now rewrite L.fold_spec. +Qed. + +(** * Comparison *) + +(** [flatten_e e] returns the list of bindings of the enumeration [e] + i.e. the list of bindings actually compared *) + +Fixpoint flatten_e (e : enumeration elt) : list (key*elt) := match e with + | End _ => nil + | More x e t r => (x,e) :: bindings t ++ flatten_e r + end. + +Lemma flatten_e_bindings : + forall (l:t elt) r x d z e, + bindings l ++ flatten_e (More x d r e) = + bindings (Node l x d r z) ++ flatten_e e. +Proof. + intros; apply bindings_node. +Qed. + +Lemma cons_1 : forall (s:t elt) e, + flatten_e (cons s e) = bindings s ++ flatten_e e. +Proof. + induction s; auto; intros. + simpl flatten_e; rewrite IHs1; apply flatten_e_bindings; auto. +Qed. + +(** Proof of correction for the comparison *) + +Variable cmp : elt->elt->bool. + +Definition IfEq b l1 l2 := L.equal cmp l1 l2 = b. + +Lemma cons_IfEq : forall b x1 x2 d1 d2 l1 l2, + X.eq x1 x2 -> cmp d1 d2 = true -> + IfEq b l1 l2 -> + IfEq b ((x1,d1)::l1) ((x2,d2)::l2). +Proof. + unfold IfEq; destruct b; simpl; intros; case X.compare_spec; simpl; + try rewrite H0; auto; order. +Qed. + +Lemma equal_end_IfEq : forall e2, + IfEq (equal_end e2) nil (flatten_e e2). +Proof. + destruct e2; red; auto. +Qed. + +Lemma equal_more_IfEq : + forall x1 d1 (cont:enumeration elt -> bool) x2 d2 r2 e2 l, + IfEq (cont (cons r2 e2)) l (bindings r2 ++ flatten_e e2) -> + IfEq (equal_more cmp x1 d1 cont (More x2 d2 r2 e2)) ((x1,d1)::l) + (flatten_e (More x2 d2 r2 e2)). +Proof. + unfold IfEq; simpl; intros; destruct X.compare; simpl; auto. + rewrite <-andb_lazy_alt; f_equal; auto. +Qed. + +Lemma equal_cont_IfEq : forall m1 cont e2 l, + (forall e, IfEq (cont e) l (flatten_e e)) -> + IfEq (equal_cont cmp m1 cont e2) (bindings m1 ++ l) (flatten_e e2). +Proof. + induction m1 as [|l1 Hl1 x1 d1 r1 Hr1 h1]; intros; auto. + rewrite <- bindings_node; simpl. + apply Hl1; auto. + clear e2; intros [|x2 d2 r2 e2]. + simpl; red; auto. + apply equal_more_IfEq. + rewrite <- cons_1; auto. +Qed. + +Lemma equal_IfEq : forall (m1 m2:t elt), + IfEq (equal cmp m1 m2) (bindings m1) (bindings m2). +Proof. + intros; unfold equal. + rewrite <- (app_nil_r (bindings m1)). + replace (bindings m2) with (flatten_e (cons m2 (End _))) + by (rewrite cons_1; simpl; rewrite app_nil_r; auto). + apply equal_cont_IfEq. + intros. + apply equal_end_IfEq; auto. +Qed. + +Definition Equivb m m' := + (forall k, In k m <-> In k m') /\ + (forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true). + +Lemma Equivb_bindings : forall s s', + Equivb s s' <-> L.Equivb cmp (bindings s) (bindings s'). +Proof. +unfold Equivb, L.Equivb; split; split; intros. +do 2 rewrite bindings_in; firstorder. +destruct H. +apply (H2 k); rewrite <- bindings_mapsto; auto. +do 2 rewrite <- bindings_in; firstorder. +destruct H. +apply (H2 k); unfold L.PX.MapsTo; rewrite bindings_mapsto; auto. +Qed. + +Lemma equal_Equivb : forall (s s': t elt), Bst s -> Bst s' -> + (equal cmp s s' = true <-> Equivb s s'). +Proof. + intros s s' B B'. + rewrite Equivb_bindings, <- equal_IfEq. + split; [apply L.equal_2|apply L.equal_1]; auto. +Qed. + +End Elt. + +Section Map. +Variable elt elt' : Type. +Variable f : elt -> elt'. + +Lemma map_spec m x : + find x (map f m) = option_map f (find x m). +Proof. +induction m; simpl; trivial. case X.compare_spec; auto. +Qed. + +Lemma map_in m x : x ∈ (map f m) <-> x ∈ m. +Proof. +induction m; simpl; intuition_in. +Qed. + +Lemma map_bst m : Bst m -> Bst (map f m). +Proof. +induction m; simpl; auto. intros; inv Bst; constructor; auto. +- apply above. intro. rewrite map_in. intros. order. +- apply below. intro. rewrite map_in. intros. order. +Qed. + +End Map. +Section Mapi. +Variable elt elt' : Type. +Variable f : key -> elt -> elt'. + +Lemma mapi_spec m x : + exists y:key, + X.eq y x /\ find x (mapi f m) = option_map (f y) (find x m). +Proof. + induction m; simpl. + - now exists x. + - case X.compare_spec; simpl; auto. intros. now exists k. +Qed. + +Lemma mapi_in m x : x ∈ (mapi f m) <-> x ∈ m. +Proof. +induction m; simpl; intuition_in. +Qed. + +Lemma mapi_bst m : Bst m -> Bst (mapi f m). +Proof. +induction m; simpl; auto. intros; inv Bst; constructor; auto. +- apply above. intro. rewrite mapi_in. intros. order. +- apply below. intro. rewrite mapi_in. intros. order. +Qed. + +End Mapi. + +Section Mapo. +Variable elt elt' : Type. +Variable f : key -> elt -> option elt'. + +Lemma mapo_in m x : + x ∈ (mapo f m) -> + exists y d, X.eq y x /\ MapsTo x d m /\ f y d <> None. +Proof. +functional induction (mapo f m); simpl; auto; intro H. +- inv In. +- rewrite join_in in H; destruct H as [H|[H|H]]. + + exists x0, d. do 2 (split; auto). congruence. + + destruct (IHt H) as (y & e & ? & ? & ?). exists y, e. auto. + + destruct (IHt0 H) as (y & e & ? & ? & ?). exists y, e. auto. +- rewrite concat_in in H; destruct H as [H|H]. + + destruct (IHt H) as (y & e & ? & ? & ?). exists y, e. auto. + + destruct (IHt0 H) as (y & e & ? & ? & ?). exists y, e. auto. +Qed. + +Lemma mapo_lt m x : x >> m -> x >> mapo f m. +Proof. + intros H. apply above. intros y Hy. + destruct (mapo_in Hy) as (y' & e & ? & ? & ?). order. +Qed. + +Lemma mapo_gt m x : x << m -> x << mapo f m. +Proof. + intros H. apply below. intros y Hy. + destruct (mapo_in Hy) as (y' & e & ? & ? & ?). order. +Qed. +Hint Resolve mapo_lt mapo_gt. + +Lemma mapo_bst m : Bst m -> Bst (mapo f m). +Proof. +functional induction (mapo f m); simpl; auto; intro H; inv Bst. +- apply join_bst, create_bst; auto. +- apply concat_bst; auto. apply between with x; auto. +Qed. +Hint Resolve mapo_bst. + +Ltac nonify e := + replace e with (@None elt) by + (symmetry; rewrite not_find_iff; auto; intro; order). + +Definition obind {A B} (o:option A) (f:A->option B) := + match o with Some a => f a | None => None end. + +Lemma mapo_find m x : + Bst m -> + exists y, X.eq y x /\ + find x (mapo f m) = obind (find x m) (f y). +Proof. +functional induction (mapo f m); simpl; auto; intros B; + inv Bst. +- now exists x. +- rewrite join_find; auto. + + simpl. case X.compare_spec; simpl; intros. + * now exists x0. + * destruct IHt as (y' & ? & ?); auto. + exists y'; split; trivial. + * destruct IHt0 as (y' & ? & ?); auto. + exists y'; split; trivial. + + constructor; auto using mapo_lt, mapo_gt. +- rewrite concat_find; auto. + + destruct IHt0 as (y' & ? & ->); auto. + destruct IHt as (y'' & ? & ->); auto. + case X.compare_spec; simpl; intros. + * nonify (find x r). nonify (find x l). simpl. now exists x0. + * nonify (find x r). now exists y''. + * nonify (find x l). exists y'. split; trivial. + destruct (find x r); simpl; trivial. + now destruct (f y' e). + + apply between with x0; auto. +Qed. + +End Mapo. + +Section Gmerge. +Variable elt elt' elt'' : Type. +Variable f0 : key -> option elt -> option elt' -> option elt''. +Variable f : key -> elt -> option elt' -> option elt''. +Variable mapl : t elt -> t elt''. +Variable mapr : t elt' -> t elt''. +Hypothesis f0_f : forall x d o, f x d o = f0 x (Some d) o. +Hypothesis mapl_bst : forall m, Bst m -> Bst (mapl m). +Hypothesis mapr_bst : forall m', Bst m' -> Bst (mapr m'). +Hypothesis mapl_f0 : forall x m, Bst m -> + exists y, X.eq y x /\ + find x (mapl m) = obind (find x m) (fun d => f0 y (Some d) None). +Hypothesis mapr_f0 : forall x m, Bst m -> + exists y, X.eq y x /\ + find x (mapr m) = obind (find x m) (fun d => f0 y None (Some d)). + +Notation gmerge := (gmerge f mapl mapr). + +Lemma gmerge_in m m' y : Bst m -> Bst m' -> + y ∈ (gmerge m m') -> y ∈ m \/ y ∈ m'. +Proof. + functional induction (gmerge m m'); intros B1 B2 H; + try factornode m2; inv Bst. + - right. apply find_in. + generalize (in_find (mapr_bst B2) H). + destruct (@mapr_f0 y m2) as (y' & ? & ->); trivial. + intros A B. rewrite B in A. now elim A. + - left. apply find_in. + generalize (in_find (mapl_bst B1) H). + destruct (@mapl_f0 y m2) as (y' & ? & ->); trivial. + intros A B. rewrite B in A. now elim A. + - rewrite join_in in *. revert IHt1 IHt0 H. cleansplit. + generalize (split_bst_l x1 B2) (split_bst_r x1 B2). + rewrite split_in_r, split_in_l; intuition_in. + - rewrite concat_in in *. revert IHt1 IHt0 H; cleansplit. + generalize (split_bst_l x1 B2) (split_bst_r x1 B2). + rewrite split_in_r, split_in_l; intuition_in. +Qed. + +Lemma gmerge_lt m m' x : Bst m -> Bst m' -> + x >> m -> x >> m' -> x >> gmerge m m'. +Proof. + intros. apply above. intros y Hy. + apply gmerge_in in Hy; intuition_in; order. +Qed. + +Lemma gmerge_gt m m' x : Bst m -> Bst m' -> + x << m -> x << m' -> x << gmerge m m'. +Proof. + intros. apply below. intros y Hy. + apply gmerge_in in Hy; intuition_in; order. +Qed. +Hint Resolve gmerge_lt gmerge_gt. +Hint Resolve split_bst_l split_bst_r split_lt_l split_gt_r. + +Lemma gmerge_bst m m' : Bst m -> Bst m' -> Bst (gmerge m m'). +Proof. + functional induction (gmerge m m'); intros B1 B2; auto; + factornode m2; inv Bst; + (apply join_bst, create_bst || apply concat_bst); + revert IHt1 IHt0; cleansplit; intuition. + apply between with x1; auto. +Qed. +Hint Resolve gmerge_bst. + +Lemma oelse_none_r {A} (o:option A) : oelse o None = o. +Proof. now destruct o. Qed. + +Ltac nonify e := + let E := fresh "E" in + assert (E : e = None); + [ rewrite not_find_iff; auto; intro U; + try apply gmerge_in in U; intuition_in; order + | rewrite E; clear E ]. + +Lemma gmerge_find m m' x : Bst m -> Bst m' -> + In x m \/ In x m' -> + exists y, X.eq y x /\ + find x (gmerge m m') = f0 y (find x m) (find x m'). +Proof. + functional induction (gmerge m m'); intros B1 B2 H; + try factornode m2; inv Bst. + - destruct H; [ intuition_in | ]. + destruct (@mapr_f0 x m2) as (y,(Hy,E)); trivial. + exists y; split; trivial. + rewrite E. simpl. apply in_find in H; trivial. + destruct (find x m2); simpl; intuition. + - destruct H; [ | intuition_in ]. + destruct (@mapl_f0 x m2) as (y,(Hy,E)); trivial. + exists y; split; trivial. + rewrite E. simpl. apply in_find in H; trivial. + destruct (find x m2); simpl; intuition. + - generalize (split_bst_l x1 B2) (split_bst_r x1 B2). + rewrite (split_find x1 x B2). + rewrite e1 in *; simpl in *. intros. + rewrite join_find by (cleansplit; constructor; auto). + simpl. case X.compare_spec; intros. + + exists x1. split; auto. now rewrite <- e3, f0_f. + + apply IHt1; auto. clear IHt1 IHt0. + cleansplit; rewrite split_in_l; trivial. + intuition_in; order. + + apply IHt0; auto. clear IHt1 IHt0. + cleansplit; rewrite split_in_r; trivial. + intuition_in; order. + - generalize (split_bst_l x1 B2) (split_bst_r x1 B2). + rewrite (split_find x1 x B2). + pose proof (split_lt_l x1 B2). + pose proof (split_gt_r x1 B2). + rewrite e1 in *; simpl in *. intros. + rewrite concat_find by (try apply between with x1; auto). + case X.compare_spec; intros. + + clear IHt0 IHt1. + exists x1. split; auto. rewrite <- f0_f, e2. + nonify (find x (gmerge r1 r2')). + nonify (find x (gmerge l1 l2')). trivial. + + nonify (find x (gmerge r1 r2')). + simpl. apply IHt1; auto. clear IHt1 IHt0. + intuition_in; try order. + right. cleansplit. now apply split_in_l. + + nonify (find x (gmerge l1 l2')). simpl. + rewrite oelse_none_r. + apply IHt0; auto. clear IHt1 IHt0. + intuition_in; try order. + right. cleansplit. now apply split_in_r. +Qed. + +End Gmerge. + +Section Merge. +Variable elt elt' elt'' : Type. +Variable f : key -> option elt -> option elt' -> option elt''. + +Lemma merge_bst m m' : Bst m -> Bst m' -> Bst (merge f m m'). +Proof. +unfold merge; intros. +apply gmerge_bst with f; + auto using mapo_bst, mapo_find. +Qed. + +Lemma merge_spec1 m m' x : Bst m -> Bst m' -> + In x m \/ In x m' -> + exists y, X.eq y x /\ + find x (merge f m m') = f y (find x m) (find x m'). +Proof. + unfold merge; intros. + edestruct (gmerge_find (f0:=f)) as (y,(Hy,E)); + eauto using mapo_bst. + - reflexivity. + - intros. now apply mapo_find. + - intros. now apply mapo_find. +Qed. + +Lemma merge_spec2 m m' x : Bst m -> Bst m' -> + In x (merge f m m') -> In x m \/ In x m'. +Proof. +unfold merge; intros. +eapply gmerge_in with (f0:=f); try eassumption; + auto using mapo_bst, mapo_find. +Qed. + +End Merge. +End Proofs. +End Raw. + +(** * Encapsulation + + Now, in order to really provide a functor implementing [S], we + need to encapsulate everything into a type of balanced binary search trees. *) + +Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. + + Module E := X. + Module Raw := Raw I X. + Import Raw.Proofs. + + Record tree (elt:Type) := + Mk {this :> Raw.tree elt; is_bst : Raw.Bst this}. + + Definition t := tree. + Definition key := E.t. + + Section Elt. + Variable elt elt' elt'': Type. + + Implicit Types m : t elt. + Implicit Types x y : key. + Implicit Types e : elt. + + Definition empty : t elt := Mk (empty_bst elt). + Definition is_empty m : bool := Raw.is_empty m.(this). + Definition add x e m : t elt := Mk (add_bst x e m.(is_bst)). + Definition remove x m : t elt := Mk (remove_bst x m.(is_bst)). + Definition mem x m : bool := Raw.mem x m.(this). + Definition find x m : option elt := Raw.find x m.(this). + Definition map f m : t elt' := Mk (map_bst f m.(is_bst)). + Definition mapi (f:key->elt->elt') m : t elt' := + Mk (mapi_bst f m.(is_bst)). + Definition merge f m (m':t elt') : t elt'' := + Mk (merge_bst f m.(is_bst) m'.(is_bst)). + Definition bindings m : list (key*elt) := Raw.bindings m.(this). + Definition cardinal m := Raw.cardinal m.(this). + Definition fold {A} (f:key->elt->A->A) m i := Raw.fold (A:=A) f m.(this) i. + Definition equal cmp m m' : bool := Raw.equal cmp m.(this) m'.(this). + + Definition MapsTo x e m : Prop := Raw.MapsTo x e m.(this). + Definition In x m : Prop := Raw.In0 x m.(this). + + Definition eq_key : (key*elt) -> (key*elt) -> Prop := @PX.eqk elt. + Definition eq_key_elt : (key*elt) -> (key*elt) -> Prop := @PX.eqke elt. + Definition lt_key : (key*elt) -> (key*elt) -> Prop := @PX.ltk elt. + + Instance MapsTo_compat : + Proper (E.eq==>Logic.eq==>Logic.eq==>iff) MapsTo. + Proof. + intros k k' Hk e e' He m m' Hm. unfold MapsTo; simpl. + now rewrite Hk, He, Hm. + Qed. + + Lemma find_spec m x e : find x m = Some e <-> MapsTo x e m. + Proof. apply find_spec. apply is_bst. Qed. + + Lemma mem_spec m x : mem x m = true <-> In x m. + Proof. + unfold In, mem; rewrite In_alt. apply mem_spec. apply is_bst. + Qed. + + Lemma empty_spec x : find x empty = None. + Proof. apply empty_spec. Qed. + + Lemma is_empty_spec m : is_empty m = true <-> forall x, find x m = None. + Proof. apply is_empty_spec. Qed. + + Lemma add_spec1 m x e : find x (add x e m) = Some e. + Proof. apply add_spec1. apply is_bst. Qed. + Lemma add_spec2 m x y e : ~ E.eq x y -> find y (add x e m) = find y m. + Proof. apply add_spec2. apply is_bst. Qed. + + Lemma remove_spec1 m x : find x (remove x m) = None. + Proof. apply remove_spec1. apply is_bst. Qed. + Lemma remove_spec2 m x y : ~E.eq x y -> find y (remove x m) = find y m. + Proof. apply remove_spec2. apply is_bst. Qed. + + Lemma bindings_spec1 m x e : + InA eq_key_elt (x,e) (bindings m) <-> MapsTo x e m. + Proof. apply bindings_mapsto. Qed. + + Lemma bindings_spec2 m : sort lt_key (bindings m). + Proof. apply bindings_sort. apply is_bst. Qed. + + Lemma bindings_spec2w m : NoDupA eq_key (bindings m). + Proof. apply bindings_nodup. apply is_bst. Qed. + + Lemma fold_spec m {A} (i : A) (f : key -> elt -> A -> A) : + fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (bindings m) i. + Proof. apply fold_spec. apply is_bst. Qed. + + Lemma cardinal_spec m : cardinal m = length (bindings m). + Proof. apply bindings_cardinal. Qed. + + Definition Equal m m' := forall y, find y m = find y m'. + Definition Equiv (eq_elt:elt->elt->Prop) m m' := + (forall k, In k m <-> In k m') /\ + (forall k e e', MapsTo k e m -> MapsTo k e' m' -> eq_elt e e'). + Definition Equivb cmp := Equiv (Cmp cmp). + + Lemma Equivb_Equivb cmp m m' : + Equivb cmp m m' <-> Raw.Proofs.Equivb cmp m m'. + Proof. + unfold Equivb, Equiv, Raw.Proofs.Equivb, In. intuition. + generalize (H0 k); do 2 rewrite In_alt; intuition. + generalize (H0 k); do 2 rewrite In_alt; intuition. + generalize (H0 k); do 2 rewrite <- In_alt; intuition. + generalize (H0 k); do 2 rewrite <- In_alt; intuition. + Qed. + + Lemma equal_spec m m' cmp : + equal cmp m m' = true <-> Equivb cmp m m'. + Proof. rewrite Equivb_Equivb. apply equal_Equivb; apply is_bst. Qed. + + End Elt. + + Lemma map_spec {elt elt'} (f:elt->elt') m x : + find x (map f m) = option_map f (find x m). + Proof. apply map_spec. Qed. + + Lemma mapi_spec {elt elt'} (f:key->elt->elt') m x : + exists y:key, E.eq y x /\ find x (mapi f m) = option_map (f y) (find x m). + Proof. apply mapi_spec. Qed. + + Lemma merge_spec1 {elt elt' elt''} + (f:key->option elt->option elt'->option elt'') m m' x : + In x m \/ In x m' -> + exists y:key, E.eq y x /\ + find x (merge f m m') = f y (find x m) (find x m'). + Proof. + unfold In. rewrite !In_alt. apply merge_spec1; apply is_bst. + Qed. + + Lemma merge_spec2 {elt elt' elt''} + (f:key -> option elt->option elt'->option elt'') m m' x : + In x (merge f m m') -> In x m \/ In x m'. + Proof. + unfold In. rewrite !In_alt. apply merge_spec2; apply is_bst. + Qed. + +End IntMake. + + +Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: + Sord with Module Data := D + with Module MapS.E := X. + + Module Data := D. + Module Import MapS := IntMake(I)(X). + Module LO := MMapList.Make_ord(X)(D). + Module R := Raw. + Module P := Raw.Proofs. + + Definition t := MapS.t D.t. + + Definition cmp e e' := + match D.compare e e' with Eq => true | _ => false end. + + (** One step of comparison of bindings *) + + Definition compare_more x1 d1 (cont:R.enumeration D.t -> comparison) e2 := + match e2 with + | R.End _ => Gt + | R.More x2 d2 r2 e2 => + match X.compare x1 x2 with + | Eq => match D.compare d1 d2 with + | Eq => cont (R.cons r2 e2) + | Lt => Lt + | Gt => Gt + end + | Lt => Lt + | Gt => Gt + end + end. + + (** Comparison of left tree, middle element, then right tree *) + + Fixpoint compare_cont s1 (cont:R.enumeration D.t -> comparison) e2 := + match s1 with + | R.Leaf _ => cont e2 + | R.Node l1 x1 d1 r1 _ => + compare_cont l1 (compare_more x1 d1 (compare_cont r1 cont)) e2 + end. + + (** Initial continuation *) + + Definition compare_end (e2:R.enumeration D.t) := + match e2 with R.End _ => Eq | _ => Lt end. + + (** The complete comparison *) + + Definition compare m1 m2 := + compare_cont m1.(this) compare_end (R.cons m2 .(this) (Raw.End _)). + + (** Correctness of this comparison *) + + Definition Cmp c := + match c with + | Eq => LO.eq_list + | Lt => LO.lt_list + | Gt => (fun l1 l2 => LO.lt_list l2 l1) + end. + + Lemma cons_Cmp c x1 x2 d1 d2 l1 l2 : + X.eq x1 x2 -> D.eq d1 d2 -> + Cmp c l1 l2 -> Cmp c ((x1,d1)::l1) ((x2,d2)::l2). + Proof. + destruct c; simpl; intros; case X.compare_spec; auto; try P.MX.order. + intros. right. split; auto. now symmetry. + Qed. + Hint Resolve cons_Cmp. + + Lemma compare_end_Cmp e2 : + Cmp (compare_end e2) nil (P.flatten_e e2). + Proof. + destruct e2; simpl; auto. + Qed. + + Lemma compare_more_Cmp x1 d1 cont x2 d2 r2 e2 l : + Cmp (cont (R.cons r2 e2)) l (R.bindings r2 ++ P.flatten_e e2) -> + Cmp (compare_more x1 d1 cont (R.More x2 d2 r2 e2)) ((x1,d1)::l) + (P.flatten_e (R.More x2 d2 r2 e2)). + Proof. + simpl; case X.compare_spec; simpl; + try case D.compare_spec; simpl; auto; + case X.compare_spec; try P.MX.order; auto. + Qed. + + Lemma compare_cont_Cmp : forall s1 cont e2 l, + (forall e, Cmp (cont e) l (P.flatten_e e)) -> + Cmp (compare_cont s1 cont e2) (R.bindings s1 ++ l) (P.flatten_e e2). + Proof. + induction s1 as [|l1 Hl1 x1 d1 r1 Hr1 h1] using P.tree_ind; + intros; auto. + rewrite <- P.bindings_node; simpl. + apply Hl1; auto. clear e2. intros [|x2 d2 r2 e2]. + simpl; auto. + apply compare_more_Cmp. + rewrite <- P.cons_1; auto. + Qed. + + Lemma compare_Cmp m1 m2 : + Cmp (compare m1 m2) (bindings m1) (bindings m2). + Proof. + destruct m1 as (s1,H1), m2 as (s2,H2). + unfold compare, bindings; simpl. + rewrite <- (app_nil_r (R.bindings s1)). + replace (R.bindings s2) with (P.flatten_e (R.cons s2 (R.End _))) by + (rewrite P.cons_1; simpl; rewrite app_nil_r; auto). + auto using compare_cont_Cmp, compare_end_Cmp. + Qed. + + Definition eq (m1 m2 : t) := LO.eq_list (bindings m1) (bindings m2). + Definition lt (m1 m2 : t) := LO.lt_list (bindings m1) (bindings m2). + + Lemma compare_spec m1 m2 : CompSpec eq lt m1 m2 (compare m1 m2). + Proof. + assert (H := compare_Cmp m1 m2). + unfold Cmp in H. + destruct (compare m1 m2); auto. + Qed. + + (* Proofs about [eq] and [lt] *) + + Definition sbindings (m1 : t) := + LO.MapS.Mk (P.bindings_sort m1.(is_bst)). + + Definition seq (m1 m2 : t) := LO.eq (sbindings m1) (sbindings m2). + Definition slt (m1 m2 : t) := LO.lt (sbindings m1) (sbindings m2). + + Lemma eq_seq : forall m1 m2, eq m1 m2 <-> seq m1 m2. + Proof. + unfold eq, seq, sbindings, bindings, LO.eq; intuition. + Qed. + + Lemma lt_slt : forall m1 m2, lt m1 m2 <-> slt m1 m2. + Proof. + unfold lt, slt, sbindings, bindings, LO.lt; intuition. + Qed. + + Lemma eq_spec m m' : eq m m' <-> Equivb cmp m m'. + Proof. + rewrite eq_seq; unfold seq. + rewrite Equivb_Equivb. + rewrite P.Equivb_bindings. apply LO.eq_spec. + Qed. + + Instance eq_equiv : Equivalence eq. + Proof. + constructor; red; [intros x|intros x y| intros x y z]; + rewrite !eq_seq; apply LO.eq_equiv. + Qed. + + Instance lt_compat : Proper (eq ==> eq ==> iff) lt. + Proof. + intros m1 m2 H1 m1' m2' H2. rewrite !lt_slt. rewrite eq_seq in *. + now apply LO.lt_compat. + Qed. + + Instance lt_strorder : StrictOrder lt. + Proof. + constructor; red; [intros x; red|intros x y z]; + rewrite !lt_slt; apply LO.lt_strorder. + Qed. + +End IntMake_ord. + +(* For concrete use inside Coq, we propose an instantiation of [Int] by [Z]. *) + +Module Make (X: OrderedType) <: S with Module E := X + :=IntMake(Z_as_Int)(X). + +Module Make_ord (X: OrderedType)(D: OrderedType) + <: Sord with Module Data := D + with Module MapS.E := X + :=IntMake_ord(Z_as_Int)(X)(D). diff --git a/theories/MMaps/MMapFacts.v b/theories/MMaps/MMapFacts.v new file mode 100644 index 00000000..69066a7b --- /dev/null +++ b/theories/MMaps/MMapFacts.v @@ -0,0 +1,2434 @@ +(***********************************************************************) +(* 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 maps library *) + +(** This functor derives additional facts from [MMapInterface.S]. These + facts are mainly the specifications of [MMapInterface.S] written using + different styles: equivalence and boolean equalities. +*) + +Require Import Bool Equalities Orders OrdersFacts OrdersLists. +Require Import Morphisms Permutation SetoidPermutation. +Require Export MMapInterface. +Set Implicit Arguments. +Unset Strict Implicit. + +Lemma eq_bool_alt b b' : b=b' <-> (b=true <-> b'=true). +Proof. + destruct b, b'; intuition. +Qed. + +Lemma eq_option_alt {elt}(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 option_map_some {A B}(f:A->B) o : + option_map f o <> None <-> o <> None. +Proof. + destruct o; simpl. now split. split; now destruct 1. +Qed. + +(** * Properties about weak maps *) + +Module WProperties_fun (E:DecidableType)(Import M:WSfun E). + +Definition Empty {elt}(m : t elt) := forall x e, ~MapsTo x e m. + +(** A few things about E.eq *) + +Lemma eq_refl x : E.eq x x. Proof. apply E.eq_equiv. Qed. +Lemma eq_sym x y : E.eq x y -> E.eq y x. Proof. apply E.eq_equiv. Qed. +Lemma eq_trans x y z : E.eq x y -> E.eq y z -> E.eq x z. +Proof. apply E.eq_equiv. Qed. +Hint Immediate eq_refl eq_sym : map. +Hint Resolve eq_trans eq_equivalence E.eq_equiv : map. + +Definition eqb x y := if E.eq_dec x y then true else false. + +Lemma eqb_eq x y : eqb x y = true <-> E.eq x y. +Proof. + unfold eqb; case E.eq_dec; now intuition. +Qed. + +Lemma eqb_sym x y : eqb x y = eqb y x. +Proof. + apply eq_bool_alt. rewrite !eqb_eq. split; apply E.eq_equiv. +Qed. + +(** Initial results about MapsTo and In *) + +Lemma mapsto_fun {elt} m x (e e':elt) : + MapsTo x e m -> MapsTo x e' m -> e=e'. +Proof. +rewrite <- !find_spec. congruence. +Qed. + +Lemma in_find {elt} (m : t elt) x : In x m <-> find x m <> None. +Proof. + unfold In. split. + - intros (e,H). rewrite <-find_spec in H. congruence. + - destruct (find x m) as [e|] eqn:H. + + exists e. now apply find_spec. + + now destruct 1. +Qed. + +Lemma not_in_find {elt} (m : t elt) x : ~In x m <-> find x m = None. +Proof. + rewrite in_find. split; auto. + intros; destruct (find x m); trivial. now destruct H. +Qed. + +Notation in_find_iff := in_find (only parsing). +Notation not_find_in_iff := not_in_find (only parsing). + +(** * [Equal] is a setoid equality. *) + +Infix "==" := Equal (at level 30). + +Lemma Equal_refl {elt} (m : t elt) : m == m. +Proof. red; reflexivity. Qed. + +Lemma Equal_sym {elt} (m m' : t elt) : m == m' -> m' == m. +Proof. unfold Equal; auto. Qed. + +Lemma Equal_trans {elt} (m m' m'' : t elt) : + m == m' -> m' == m'' -> m == m''. +Proof. unfold Equal; congruence. Qed. + +Instance Equal_equiv {elt} : Equivalence (@Equal elt). +Proof. +constructor; [exact Equal_refl | exact Equal_sym | exact Equal_trans]. +Qed. + +Arguments Equal {elt} m m'. + +Instance MapsTo_m {elt} : + Proper (E.eq==>Logic.eq==>Equal==>iff) (@MapsTo elt). +Proof. +intros k k' Hk e e' <- m m' Hm. rewrite <- Hk. +now rewrite <- !find_spec, Hm. +Qed. + +Instance In_m {elt} : + Proper (E.eq==>Equal==>iff) (@In elt). +Proof. +intros k k' Hk m m' Hm. unfold In. +split; intros (e,H); exists e; revert H; + now rewrite Hk, <- !find_spec, Hm. +Qed. + +Instance find_m {elt} : Proper (E.eq==>Equal==>Logic.eq) (@find elt). +Proof. +intros k k' Hk m m' <-. +rewrite eq_option_alt. intros. now rewrite !find_spec, Hk. +Qed. + +Instance mem_m {elt} : Proper (E.eq==>Equal==>Logic.eq) (@mem elt). +Proof. +intros k k' Hk m m' Hm. now rewrite eq_bool_alt, !mem_spec, Hk, Hm. +Qed. + +Instance Empty_m {elt} : Proper (Equal==>iff) (@Empty elt). +Proof. +intros m m' Hm. unfold Empty. now setoid_rewrite Hm. +Qed. + +Instance is_empty_m {elt} : Proper (Equal ==> Logic.eq) (@is_empty elt). +Proof. +intros m m' Hm. rewrite eq_bool_alt, !is_empty_spec. + now setoid_rewrite Hm. +Qed. + +Instance add_m {elt} : Proper (E.eq==>Logic.eq==>Equal==>Equal) (@add elt). +Proof. +intros k k' Hk e e' <- m m' Hm y. +destruct (E.eq_dec k y) as [H|H]. +- rewrite <-H, add_spec1. now rewrite Hk, add_spec1. +- rewrite !add_spec2; trivial. now rewrite <- Hk. +Qed. + +Instance remove_m {elt} : Proper (E.eq==>Equal==>Equal) (@remove elt). +Proof. +intros k k' Hk m m' Hm y. +destruct (E.eq_dec k y) as [H|H]. +- rewrite <-H, remove_spec1. now rewrite Hk, remove_spec1. +- rewrite !remove_spec2; trivial. now rewrite <- Hk. +Qed. + +Instance map_m {elt elt'} : + Proper ((Logic.eq==>Logic.eq)==>Equal==>Equal) (@map elt elt'). +Proof. +intros f f' Hf m m' Hm y. rewrite !map_spec, Hm. +destruct (find y m'); simpl; trivial. f_equal. now apply Hf. +Qed. + +Instance mapi_m {elt elt'} : + Proper ((E.eq==>Logic.eq==>Logic.eq)==>Equal==>Equal) (@mapi elt elt'). +Proof. +intros f f' Hf m m' Hm y. +destruct (mapi_spec f m y) as (x,(Hx,->)). +destruct (mapi_spec f' m' y) as (x',(Hx',->)). +rewrite <- Hm. destruct (find y m); trivial. simpl. +f_equal. apply Hf; trivial. now rewrite Hx, Hx'. +Qed. + +Instance merge_m {elt elt' elt''} : + Proper ((E.eq==>Logic.eq==>Logic.eq==>Logic.eq)==>Equal==>Equal==>Equal) + (@merge elt elt' elt''). +Proof. +intros f f' Hf m1 m1' Hm1 m2 m2' Hm2 y. +destruct (find y m1) as [e1|] eqn:H1. +- apply find_spec in H1. + assert (H : In y m1 \/ In y m2) by (left; now exists e1). + destruct (merge_spec1 f H) as (y1,(Hy1,->)). + rewrite Hm1,Hm2 in H. + destruct (merge_spec1 f' H) as (y2,(Hy2,->)). + rewrite <- Hm1, <- Hm2. apply Hf; trivial. now transitivity y. +- destruct (find y m2) as [e2|] eqn:H2. + + apply find_spec in H2. + assert (H : In y m1 \/ In y m2) by (right; now exists e2). + destruct (merge_spec1 f H) as (y1,(Hy1,->)). + rewrite Hm1,Hm2 in H. + destruct (merge_spec1 f' H) as (y2,(Hy2,->)). + rewrite <- Hm1, <- Hm2. apply Hf; trivial. now transitivity y. + + apply not_in_find in H1. apply not_in_find in H2. + assert (H : ~In y (merge f m1 m2)). + { intro H. apply merge_spec2 in H. intuition. } + apply not_in_find in H. rewrite H. + symmetry. apply not_in_find. intro H'. + apply merge_spec2 in H'. rewrite <- Hm1, <- Hm2 in H'. + intuition. +Qed. + +(* Later: compatibility for cardinal, fold, ... *) + +(** ** Earlier specifications (cf. FMaps) *) + +Section OldSpecs. +Variable elt: Type. +Implicit Type m: t elt. +Implicit Type x y z: key. +Implicit Type e: elt. + +Lemma MapsTo_1 m x y e : E.eq x y -> MapsTo x e m -> MapsTo y e m. +Proof. + now intros ->. +Qed. + +Lemma find_1 m x e : MapsTo x e m -> find x m = Some e. +Proof. apply find_spec. Qed. + +Lemma find_2 m x e : find x m = Some e -> MapsTo x e m. +Proof. apply find_spec. Qed. + +Lemma mem_1 m x : In x m -> mem x m = true. +Proof. apply mem_spec. Qed. + +Lemma mem_2 m x : mem x m = true -> In x m. +Proof. apply mem_spec. Qed. + +Lemma empty_1 : Empty (@empty elt). +Proof. + intros x e. now rewrite <- find_spec, empty_spec. +Qed. + +Lemma is_empty_1 m : Empty m -> is_empty m = true. +Proof. + unfold Empty; rewrite is_empty_spec. setoid_rewrite <- find_spec. + intros H x. specialize (H x). + destruct (find x m) as [e|]; trivial. + now destruct (H e). +Qed. + +Lemma is_empty_2 m : is_empty m = true -> Empty m. +Proof. + rewrite is_empty_spec. intros H x e. now rewrite <- find_spec, H. +Qed. + +Lemma add_1 m x y e : E.eq x y -> MapsTo y e (add x e m). +Proof. + intros <-. rewrite <-find_spec. apply add_spec1. +Qed. + +Lemma add_2 m x y e e' : + ~ E.eq x y -> MapsTo y e m -> MapsTo y e (add x e' m). +Proof. + intro. now rewrite <- !find_spec, add_spec2. +Qed. + +Lemma add_3 m x y e e' : + ~ E.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m. +Proof. + intro. rewrite <- !find_spec, add_spec2; trivial. +Qed. + +Lemma remove_1 m x y : E.eq x y -> ~ In y (remove x m). +Proof. + intros <-. apply not_in_find. apply remove_spec1. +Qed. + +Lemma remove_2 m x y e : + ~ E.eq x y -> MapsTo y e m -> MapsTo y e (remove x m). +Proof. + intro. now rewrite <- !find_spec, remove_spec2. +Qed. + +Lemma remove_3bis m x y e : + find y (remove x m) = Some e -> find y m = Some e. +Proof. + destruct (E.eq_dec x y) as [<-|H]. + - now rewrite remove_spec1. + - now rewrite remove_spec2. +Qed. + +Lemma remove_3 m x y e : MapsTo y e (remove x m) -> MapsTo y e m. +Proof. + rewrite <-!find_spec. apply remove_3bis. +Qed. + +Lemma bindings_1 m x e : + MapsTo x e m -> InA eq_key_elt (x,e) (bindings m). +Proof. apply bindings_spec1. Qed. + +Lemma bindings_2 m x e : + InA eq_key_elt (x,e) (bindings m) -> MapsTo x e m. +Proof. apply bindings_spec1. Qed. + +Lemma bindings_3w m : NoDupA eq_key (bindings m). +Proof. apply bindings_spec2w. Qed. + +Lemma cardinal_1 m : cardinal m = length (bindings m). +Proof. apply cardinal_spec. Qed. + +Lemma fold_1 m (A : Type) (i : A) (f : key -> elt -> A -> A) : + fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (bindings m) i. +Proof. apply fold_spec. Qed. + +Lemma equal_1 m m' cmp : Equivb cmp m m' -> equal cmp m m' = true. +Proof. apply equal_spec. Qed. + +Lemma equal_2 m m' cmp : equal cmp m m' = true -> Equivb cmp m m'. +Proof. apply equal_spec. Qed. + +End OldSpecs. + +Lemma map_1 {elt elt'}(m: t elt)(x:key)(e:elt)(f:elt->elt') : + MapsTo x e m -> MapsTo x (f e) (map f m). +Proof. + rewrite <- !find_spec, map_spec. now intros ->. +Qed. + +Lemma map_2 {elt elt'}(m: t elt)(x:key)(f:elt->elt') : + In x (map f m) -> In x m. +Proof. + rewrite !in_find, map_spec. apply option_map_some. +Qed. + +Lemma mapi_1 {elt elt'}(m: t elt)(x:key)(e:elt)(f:key->elt->elt') : + MapsTo x e m -> + exists y, E.eq y x /\ MapsTo x (f y e) (mapi f m). +Proof. + destruct (mapi_spec f m x) as (y,(Hy,Eq)). + intro H. exists y; split; trivial. + rewrite <-find_spec in *. now rewrite Eq, H. +Qed. + +Lemma mapi_2 {elt elt'}(m: t elt)(x:key)(f:key->elt->elt') : + In x (mapi f m) -> In x m. +Proof. + destruct (mapi_spec f m x) as (y,(Hy,Eq)). + rewrite !in_find. intro H; contradict H. now rewrite Eq, H. +Qed. + +(** The ancestor [map2] of the current [merge] was dealing with functions + on datas only, not on keys. *) + +Definition map2 {elt elt' elt''} (f:option elt->option elt'->option elt'') + := merge (fun _ => f). + +Lemma map2_1 {elt elt' elt''}(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. + intros. unfold map2. + now destruct (merge_spec1 (fun _ => f) H) as (y,(_,->)). +Qed. + +Lemma map2_2 {elt elt' elt''}(m: t elt)(m': t elt') + (x:key)(f:option elt->option elt'->option elt'') : + In x (map2 f m m') -> In x m \/ In x m'. +Proof. apply merge_spec2. Qed. + +Hint Immediate MapsTo_1 mem_2 is_empty_2 + map_2 mapi_2 add_3 remove_3 find_2 : map. +Hint Resolve mem_1 is_empty_1 is_empty_2 add_1 add_2 remove_1 + remove_2 find_1 fold_1 map_1 mapi_1 mapi_2 : map. + +(** ** Specifications written using equivalences *) + +Section IffSpec. +Variable elt: Type. +Implicit Type m: t elt. +Implicit Type x y z: key. +Implicit Type e: elt. + +Lemma in_iff m x y : E.eq x y -> (In x m <-> In y m). +Proof. now intros ->. Qed. + +Lemma mapsto_iff m x y e : E.eq x y -> (MapsTo x e m <-> MapsTo y e m). +Proof. now intros ->. Qed. + +Lemma mem_in_iff m x : In x m <-> mem x m = true. +Proof. symmetry. apply mem_spec. Qed. + +Lemma not_mem_in_iff m x : ~In x m <-> mem x m = false. +Proof. +rewrite mem_in_iff; destruct (mem x m); intuition. +Qed. + +Lemma mem_find m x : mem x m = true <-> find x m <> None. +Proof. + rewrite <- mem_in_iff. apply in_find. +Qed. + +Lemma not_mem_find m x : mem x m = false <-> find x m = None. +Proof. + rewrite <- not_mem_in_iff. apply not_in_find. +Qed. + +Lemma In_dec m x : { In x m } + { ~ In x m }. +Proof. + generalize (mem_in_iff m x). + destruct (mem x m); [left|right]; intuition. +Qed. + +Lemma find_mapsto_iff m x e : MapsTo x e m <-> find x m = Some e. +Proof. symmetry. apply find_spec. Qed. + +Lemma equal_iff m m' cmp : Equivb cmp m m' <-> equal cmp m m' = true. +Proof. symmetry. apply equal_spec. Qed. + +Lemma empty_mapsto_iff x e : MapsTo x e empty <-> False. +Proof. +rewrite <- find_spec, empty_spec. now split. +Qed. + +Lemma not_in_empty x : ~In x (@empty elt). +Proof. +intros (e,H). revert H. apply empty_mapsto_iff. +Qed. + +Lemma empty_in_iff x : In x (@empty elt) <-> False. +Proof. +split; [ apply not_in_empty | destruct 1 ]. +Qed. + +Lemma is_empty_iff m : Empty m <-> is_empty m = true. +Proof. split; [apply is_empty_1 | apply is_empty_2 ]. Qed. + +Lemma add_mapsto_iff m x y e e' : + MapsTo y e' (add x e m) <-> + (E.eq x y /\ e=e') \/ + (~E.eq x y /\ MapsTo y e' m). +Proof. +split. +- intros H. destruct (E.eq_dec x y); [left|right]; split; trivial. + + symmetry. apply (mapsto_fun H); auto with map. + + now apply add_3 with x e. +- destruct 1 as [(H,H')|(H,H')]; subst; auto with map. +Qed. + +Lemma add_mapsto_new m x y e e' : ~In x m -> + MapsTo y e' (add x e m) <-> (E.eq x y /\ e=e') \/ MapsTo y e' m. +Proof. + intros. + rewrite add_mapsto_iff. intuition. + right; split; trivial. contradict H. exists e'. now rewrite H. +Qed. + +Lemma in_add m x y e : In y m -> In y (add x e m). +Proof. + destruct (E.eq_dec x y) as [<-|H']. + - now rewrite !in_find, add_spec1. + - now rewrite !in_find, add_spec2. +Qed. + +Lemma add_in_iff m x y e : In y (add x e m) <-> E.eq x y \/ In y m. +Proof. +split. +- intros H. destruct (E.eq_dec x y); [now left|right]. + rewrite in_find, add_spec2 in H; trivial. now apply in_find. +- intros [<-|H]. + + exists e. now apply add_1. + + now apply in_add. +Qed. + +Lemma add_neq_mapsto_iff m x y e e' : + ~ E.eq x y -> (MapsTo y e' (add x e m) <-> MapsTo y e' m). +Proof. +split; [apply add_3|apply add_2]; auto. +Qed. + +Lemma add_neq_in_iff m x y e : + ~ E.eq x y -> (In y (add x e m) <-> In y m). +Proof. +split; intros (e',H0); exists e'. +- now apply add_3 with x e. +- now apply add_2. +Qed. + +Lemma remove_mapsto_iff m x y e : + MapsTo y e (remove x m) <-> ~E.eq x y /\ MapsTo y e m. +Proof. +split; [split|destruct 1]. +- intro E. revert H. now rewrite <-E, <- find_spec, remove_spec1. +- now apply remove_3 with x. +- now apply remove_2. +Qed. + +Lemma remove_in_iff m x y : In y (remove x m) <-> ~E.eq x y /\ In y m. +Proof. +unfold In; split; [ intros (e,H) | intros (E,(e,H)) ]. +- apply remove_mapsto_iff in H. destruct H; split; trivial. + now exists e. +- exists e. now apply remove_2. +Qed. + +Lemma remove_neq_mapsto_iff : forall m x y e, + ~ E.eq x y -> (MapsTo y e (remove x m) <-> MapsTo y e m). +Proof. +split; [apply remove_3|apply remove_2]; auto. +Qed. + +Lemma remove_neq_in_iff : forall m x y, + ~ E.eq x y -> (In y (remove x m) <-> In y m). +Proof. +split; intros (e',H0); exists e'. +- now apply remove_3 with x. +- now apply remove_2. +Qed. + +Lemma bindings_mapsto_iff m x e : + MapsTo x e m <-> InA eq_key_elt (x,e) (bindings m). +Proof. symmetry. apply bindings_spec1. Qed. + +Lemma bindings_in_iff m x : + In x m <-> exists e, InA eq_key_elt (x,e) (bindings m). +Proof. +unfold In; split; intros (e,H); exists e; now apply bindings_spec1. +Qed. + +End IffSpec. + +Lemma map_mapsto_iff {elt elt'} m x b (f : elt -> elt') : + MapsTo x b (map f m) <-> exists a, b = f a /\ MapsTo x a m. +Proof. +rewrite <-find_spec, map_spec. setoid_rewrite <- find_spec. +destruct (find x m); simpl; split. +- injection 1. now exists e. +- intros (a,(->,H)). now injection H as ->. +- discriminate. +- intros (a,(_,H)); discriminate. +Qed. + +Lemma map_in_iff {elt elt'} m x (f : elt -> elt') : + In x (map f m) <-> In x m. +Proof. +rewrite !in_find, map_spec. apply option_map_some. +Qed. + +Lemma mapi_in_iff {elt elt'} m x (f:key->elt->elt') : + In x (mapi f m) <-> In x m. +Proof. +rewrite !in_find. destruct (mapi_spec f m x) as (y,(_,->)). +apply option_map_some. +Qed. + +(** Unfortunately, we don't have simple equivalences for [mapi] + and [MapsTo]. The only correct one needs compatibility of [f]. *) + +Lemma mapi_inv {elt elt'} m x b (f : key -> elt -> elt') : + MapsTo x b (mapi f m) -> + exists a y, E.eq y x /\ b = f y a /\ MapsTo x a m. +Proof. +rewrite <- find_spec. setoid_rewrite <- find_spec. +destruct (mapi_spec f m x) as (y,(E,->)). +destruct (find x m); simpl. +- injection 1 as <-. now exists e, y. +- discriminate. +Qed. + +Lemma mapi_spec' {elt elt'} (f:key->elt->elt') : + Proper (E.eq==>Logic.eq==>Logic.eq) f -> + forall m x, + find x (mapi f m) = option_map (f x) (find x m). +Proof. + intros. destruct (mapi_spec f m x) as (y,(Hy,->)). + destruct (find x m); simpl; trivial. + now rewrite Hy. +Qed. + +Lemma mapi_1bis {elt elt'} m x e (f:key->elt->elt') : + Proper (E.eq==>Logic.eq==>Logic.eq) f -> + MapsTo x e m -> MapsTo x (f x e) (mapi f m). +Proof. +intros. destruct (mapi_1 f H0) as (y,(->,H2)). trivial. +Qed. + +Lemma mapi_mapsto_iff {elt elt'} m x b (f:key->elt->elt') : + Proper (E.eq==>Logic.eq==>Logic.eq) f -> + (MapsTo x b (mapi f m) <-> exists a, b = f x a /\ MapsTo x a m). +Proof. +rewrite <-find_spec. setoid_rewrite <-find_spec. +intros Pr. rewrite mapi_spec' by trivial. +destruct (find x m); simpl; split. +- injection 1 as <-. now exists e. +- intros (a,(->,H)). now injection H as <-. +- discriminate. +- intros (a,(_,H)). discriminate. +Qed. + +(** Things are even worse for [merge] : we don't try to state any + equivalence, see instead boolean results below. *) + +(** Useful tactic for simplifying expressions like + [In y (add x e (remove z m))] *) + +Ltac map_iff := + repeat (progress ( + rewrite add_mapsto_iff || rewrite add_in_iff || + rewrite remove_mapsto_iff || rewrite remove_in_iff || + rewrite empty_mapsto_iff || rewrite empty_in_iff || + rewrite map_mapsto_iff || rewrite map_in_iff || + rewrite mapi_in_iff)). + +(** ** Specifications written using boolean predicates *) + +Section BoolSpec. + +Lemma mem_find_b {elt}(m:t elt)(x:key) : + mem x m = if find x m then true else false. +Proof. +apply eq_bool_alt. rewrite mem_find. destruct (find x m). +- now split. +- split; (discriminate || now destruct 1). +Qed. + +Variable elt elt' elt'' : Type. +Implicit Types m : t elt. +Implicit Types x y z : key. +Implicit Types e : elt. + +Lemma mem_b m x y : E.eq x y -> mem x m = mem y m. +Proof. now intros ->. Qed. + +Lemma find_o m x y : E.eq x y -> find x m = find y m. +Proof. now intros ->. Qed. + +Lemma empty_o x : find x (@empty elt) = None. +Proof. apply empty_spec. Qed. + +Lemma empty_a x : mem x (@empty elt) = false. +Proof. apply not_mem_find. apply empty_spec. Qed. + +Lemma add_eq_o m x y e : + E.eq x y -> find y (add x e m) = Some e. +Proof. + intros <-. apply add_spec1. +Qed. + +Lemma add_neq_o m x y e : + ~ E.eq x y -> find y (add x e m) = find y m. +Proof. apply add_spec2. Qed. +Hint Resolve add_neq_o : map. + +Lemma add_o m x y e : + find y (add x e m) = if E.eq_dec x y then Some e else find y m. +Proof. +destruct (E.eq_dec x y); auto with map. +Qed. + +Lemma add_eq_b m x y e : + E.eq x y -> mem y (add x e m) = true. +Proof. +intros <-. apply mem_spec, add_in_iff. now left. +Qed. + +Lemma add_neq_b m x y e : + ~E.eq x y -> mem y (add x e m) = mem y m. +Proof. +intros. now rewrite !mem_find_b, add_neq_o. +Qed. + +Lemma add_b m x y e : + mem y (add x e m) = eqb x y || mem y m. +Proof. +rewrite !mem_find_b, add_o. unfold eqb. +now destruct (E.eq_dec x y). +Qed. + +Lemma remove_eq_o m x y : + E.eq x y -> find y (remove x m) = None. +Proof. intros ->. apply remove_spec1. Qed. + +Lemma remove_neq_o m x y : + ~ E.eq x y -> find y (remove x m) = find y m. +Proof. apply remove_spec2. Qed. + +Hint Resolve remove_eq_o remove_neq_o : map. + +Lemma remove_o m x y : + find y (remove x m) = if E.eq_dec x y then None else find y m. +Proof. +destruct (E.eq_dec x y); auto with map. +Qed. + +Lemma remove_eq_b m x y : + E.eq x y -> mem y (remove x m) = false. +Proof. +intros <-. now rewrite mem_find_b, remove_eq_o. +Qed. + +Lemma remove_neq_b m x y : + ~ E.eq x y -> mem y (remove x m) = mem y m. +Proof. +intros. now rewrite !mem_find_b, remove_neq_o. +Qed. + +Lemma remove_b m x y : + mem y (remove x m) = negb (eqb x y) && mem y m. +Proof. +rewrite !mem_find_b, remove_o; unfold eqb. +now destruct (E.eq_dec x y). +Qed. + +Lemma map_o m x (f:elt->elt') : + find x (map f m) = option_map f (find x m). +Proof. apply map_spec. Qed. + +Lemma map_b m x (f:elt->elt') : + mem x (map f m) = mem x m. +Proof. +rewrite !mem_find_b, map_o. now destruct (find x m). +Qed. + +Lemma mapi_b m x (f:key->elt->elt') : + mem x (mapi f m) = mem x m. +Proof. +apply eq_bool_alt; rewrite !mem_spec. apply mapi_in_iff. +Qed. + +Lemma mapi_o m x (f:key->elt->elt') : + Proper (E.eq==>Logic.eq==>Logic.eq) f -> + find x (mapi f m) = option_map (f x) (find x m). +Proof. intros; now apply mapi_spec'. Qed. + +Lemma merge_spec1' (f:key->option elt->option elt'->option elt'') : + Proper (E.eq==>Logic.eq==>Logic.eq==>Logic.eq) f -> + forall (m:t elt)(m':t elt') x, + In x m \/ In x m' -> + find x (merge f m m') = f x (find x m) (find x m'). +Proof. + intros Hf m m' x H. + now destruct (merge_spec1 f H) as (y,(->,->)). +Qed. + +Lemma merge_spec1_none (f:key->option elt->option elt'->option elt'') : + (forall x, f x None None = None) -> + forall (m: t elt)(m': t elt') x, + exists y, E.eq y x /\ find x (merge f m m') = f y (find x m) (find x m'). +Proof. +intros Hf m m' x. +destruct (find x m) as [e|] eqn:Hm. +- assert (H : In x m \/ In x m') by (left; exists e; now apply find_spec). + destruct (merge_spec1 f H) as (y,(Hy,->)). + exists y; split; trivial. now rewrite Hm. +- destruct (find x m') as [e|] eqn:Hm'. + + assert (H : In x m \/ In x m') by (right; exists e; now apply find_spec). + destruct (merge_spec1 f H) as (y,(Hy,->)). + exists y; split; trivial. now rewrite Hm, Hm'. + + exists x. split. reflexivity. rewrite Hf. + apply not_in_find. intro H. + apply merge_spec2 in H. apply not_in_find in Hm. apply not_in_find in Hm'. + intuition. +Qed. + +Lemma merge_spec1'_none (f:key->option elt->option elt'->option elt'') : + Proper (E.eq==>Logic.eq==>Logic.eq==>Logic.eq) f -> + (forall x, f x None None = None) -> + forall (m: t elt)(m': t elt') x, + find x (merge f m m') = f x (find x m) (find x m'). +Proof. + intros Hf Hf' m m' x. + now destruct (merge_spec1_none Hf' m m' x) as (y,(->,->)). +Qed. + +Lemma bindings_o : forall m x, + find x m = findA (eqb x) (bindings m). +Proof. +intros. rewrite eq_option_alt. intro e. +rewrite <- find_mapsto_iff, bindings_mapsto_iff. +unfold eqb. +rewrite <- findA_NoDupA; dintuition; try apply bindings_3w; eauto. +Qed. + +Lemma bindings_b : forall m x, + mem x m = existsb (fun p => eqb x (fst p)) (bindings m). +Proof. +intros. +apply eq_bool_alt. +rewrite mem_spec, bindings_in_iff, existsb_exists. +split. +- intros (e,H). + rewrite InA_alt in H. + destruct H as ((k,e'),((H1,H2),H')); simpl in *; subst e'. + exists (k, e); split; trivial. simpl. now apply eqb_eq. +- intros ((k,e),(H,H')); simpl in *. apply eqb_eq in H'. + exists e. rewrite InA_alt. exists (k,e). now repeat split. +Qed. + +End BoolSpec. + +Section Equalities. +Variable elt:Type. + +(** A few basic equalities *) + +Lemma eq_empty (m: t elt) : m == empty <-> is_empty m = true. +Proof. + unfold Equal. rewrite is_empty_spec. now setoid_rewrite empty_spec. +Qed. + +Lemma add_id (m: t elt) x e : add x e m == m <-> find x m = Some e. +Proof. + split. + - intros H. rewrite <- (H x). apply add_spec1. + - intros H y. rewrite !add_o. now destruct E.eq_dec as [<-|E]. +Qed. + +Lemma add_add_1 (m: t elt) x e : + add x e (add x e m) == add x e m. +Proof. + intros y. rewrite !add_o. destruct E.eq_dec; auto. +Qed. + +Lemma add_add_2 (m: t elt) x x' e e' : + ~E.eq x x' -> add x e (add x' e' m) == add x' e' (add x e m). +Proof. + intros H y. rewrite !add_o. + do 2 destruct E.eq_dec; auto. + elim H. now transitivity y. +Qed. + +Lemma remove_id (m: t elt) x : remove x m == m <-> ~In x m. +Proof. + rewrite not_in_find. split. + - intros H. rewrite <- (H x). apply remove_spec1. + - intros H y. rewrite !remove_o. now destruct E.eq_dec as [<-|E]. +Qed. + +Lemma remove_remove_1 (m: t elt) x : + remove x (remove x m) == remove x m. +Proof. + intros y. rewrite !remove_o. destruct E.eq_dec; auto. +Qed. + +Lemma remove_remove_2 (m: t elt) x x' : + remove x (remove x' m) == remove x' (remove x m). +Proof. + intros y. rewrite !remove_o. do 2 destruct E.eq_dec; auto. +Qed. + +Lemma remove_add_1 (m: t elt) x e : + remove x (add x e m) == remove x m. +Proof. + intro y. rewrite !remove_o, !add_o. now destruct E.eq_dec. +Qed. + +Lemma remove_add_2 (m: t elt) x x' e : + ~E.eq x x' -> remove x' (add x e m) == add x e (remove x' m). +Proof. + intros H y. rewrite !remove_o, !add_o. + do 2 destruct E.eq_dec; auto. + - elim H; now transitivity y. + - symmetry. now apply remove_eq_o. + - symmetry. now apply remove_neq_o. +Qed. + +Lemma add_remove_1 (m: t elt) x e : + add x e (remove x m) == add x e m. +Proof. + intro y. rewrite !add_o, !remove_o. now destruct E.eq_dec. +Qed. + +(** Another characterisation of [Equal] *) + +Lemma Equal_mapsto_iff : forall m1 m2 : t elt, + m1 == m2 <-> (forall k e, MapsTo k e m1 <-> MapsTo k e m2). +Proof. +intros m1 m2. split; [intros Heq k e|intros Hiff]. +rewrite 2 find_mapsto_iff, Heq. split; auto. +intro k. rewrite eq_option_alt. intro e. +rewrite <- 2 find_mapsto_iff; auto. +Qed. + +(** * Relations between [Equal], [Equiv] and [Equivb]. *) + +(** First, [Equal] is [Equiv] with Leibniz on elements. *) + +Lemma Equal_Equiv : forall (m m' : t elt), + m == m' <-> Equiv Logic.eq m m'. +Proof. +intros. rewrite Equal_mapsto_iff. split; intros. +- split. + + split; intros (e,Hin); exists e; [rewrite <- H|rewrite H]; auto. + + intros; apply mapsto_fun with m k; auto; rewrite H; auto. +- split; intros H'. + + destruct H. + assert (Hin : In k m') by (rewrite <- H; exists e; auto). + destruct Hin as (e',He'). + rewrite (H0 k e e'); auto. + + destruct H. + assert (Hin : In k m) by (rewrite H; exists e; auto). + destruct Hin as (e',He'). + rewrite <- (H0 k e' e); auto. +Qed. + +(** [Equivb] and [Equiv] and equivalent when [eq_elt] and [cmp] + are related. *) + +Section Cmp. +Variable eq_elt : elt->elt->Prop. +Variable cmp : elt->elt->bool. + +Definition compat_cmp := + forall e e', cmp e e' = true <-> eq_elt e e'. + +Lemma Equiv_Equivb : compat_cmp -> + forall m m', Equiv eq_elt m m' <-> Equivb cmp m m'. +Proof. + unfold Equivb, Equiv, Cmp; intuition. + red in H; rewrite H; eauto. + red in H; rewrite <-H; eauto. +Qed. +End Cmp. + +(** Composition of the two last results: relation between [Equal] + and [Equivb]. *) + +Lemma Equal_Equivb : forall cmp, + (forall e e', cmp e e' = true <-> e = e') -> + forall (m m':t elt), m == m' <-> Equivb cmp m m'. +Proof. + intros; rewrite Equal_Equiv. + apply Equiv_Equivb; auto. +Qed. + +Lemma Equal_Equivb_eqdec : + forall eq_elt_dec : (forall e e', { e = e' } + { e <> e' }), + let cmp := fun e e' => if eq_elt_dec e e' then true else false in + forall (m m':t elt), m == m' <-> Equivb cmp m m'. +Proof. +intros; apply Equal_Equivb. +unfold cmp; clear cmp; intros. +destruct eq_elt_dec; now intuition. +Qed. + +End Equalities. + +(** * Results about [fold], [bindings], induction principles... *) + +Section Elt. + Variable elt:Type. + + Definition Add x (e:elt) m m' := m' == (add x e m). + + Notation eqke := (@eq_key_elt elt). + Notation eqk := (@eq_key elt). + + Instance eqk_equiv : Equivalence eqk. + Proof. unfold eq_key. destruct E.eq_equiv. constructor; eauto. Qed. + + Instance eqke_equiv : Equivalence eqke. + Proof. + unfold eq_key_elt; split; repeat red; intuition; simpl in *; + etransitivity; eauto. + Qed. + + (** Complements about InA, NoDupA and findA *) + + Lemma InA_eqke_eqk k k' e e' l : + E.eq k k' -> InA eqke (k,e) l -> InA eqk (k',e') l. + Proof. + intros Hk. rewrite 2 InA_alt. + intros ((k'',e'') & (Hk'',He'') & H); simpl in *; subst e''. + exists (k'',e); split; auto. red; simpl. now transitivity k. + Qed. + + Lemma NoDupA_incl {A} (R R':relation A) : + (forall x y, R x y -> R' x y) -> + forall l, NoDupA R' l -> NoDupA R l. + Proof. + intros Incl. + induction 1 as [ | a l E _ IH ]; constructor; auto. + contradict E. revert E. rewrite 2 InA_alt. firstorder. + Qed. + + Lemma NoDupA_eqk_eqke l : NoDupA eqk l -> NoDupA eqke l. + Proof. + apply NoDupA_incl. now destruct 1. + Qed. + + Lemma findA_rev l k : NoDupA eqk l -> + findA (eqb k) l = findA (eqb k) (rev l). + Proof. + intros H. apply eq_option_alt. intros e. unfold eqb. + rewrite <- !findA_NoDupA, InA_rev; eauto with map. reflexivity. + change (NoDupA eqk (rev l)). apply NoDupA_rev; auto using eqk_equiv. + Qed. + + (** * Bindings *) + + Lemma bindings_Empty (m:t elt) : Empty m <-> bindings m = nil. + Proof. + unfold Empty. split; intros H. + - assert (H' : forall a, ~ List.In a (bindings m)). + { intros (k,e) H'. apply (H k e). + rewrite bindings_mapsto_iff, InA_alt. + exists (k,e); repeat split; auto with map. } + destruct (bindings m) as [|p l]; trivial. + destruct (H' p); simpl; auto. + - intros x e. rewrite bindings_mapsto_iff, InA_alt. + rewrite H. now intros (y,(E,H')). + Qed. + + Lemma bindings_empty : bindings (@empty elt) = nil. + Proof. + rewrite <-bindings_Empty; apply empty_1. + Qed. + + (** * Conversions between maps and association lists. *) + + Definition uncurry {U V W : Type} (f : U -> V -> W) : U*V -> W := + fun p => f (fst p) (snd p). + + Definition of_list := + List.fold_right (uncurry (@add _)) (@empty elt). + + Definition to_list := bindings. + + Lemma of_list_1 : forall l k e, + NoDupA eqk l -> + (MapsTo k e (of_list l) <-> InA eqke (k,e) l). + Proof. + induction l as [|(k',e') l IH]; simpl; intros k e Hnodup. + - rewrite empty_mapsto_iff, InA_nil; intuition. + - unfold uncurry; simpl. + inversion_clear Hnodup as [| ? ? Hnotin Hnodup']. + specialize (IH k e Hnodup'); clear Hnodup'. + rewrite add_mapsto_iff, InA_cons, <- IH. + unfold eq_key_elt at 1; simpl. + split; destruct 1 as [H|H]; try (intuition;fail). + destruct (E.eq_dec k k'); [left|right]; split; auto with map. + contradict Hnotin. + apply InA_eqke_eqk with k e; intuition. + Qed. + + Lemma of_list_1b : forall l k, + NoDupA eqk l -> + find k (of_list l) = findA (eqb k) l. + Proof. + induction l as [|(k',e') l IH]; simpl; intros k Hnodup. + apply empty_o. + unfold uncurry; simpl. + inversion_clear Hnodup as [| ? ? Hnotin Hnodup']. + specialize (IH k Hnodup'); clear Hnodup'. + rewrite add_o, IH, eqb_sym. unfold eqb; now destruct E.eq_dec. + Qed. + + Lemma of_list_2 : forall l, NoDupA eqk l -> + equivlistA eqke l (to_list (of_list l)). + Proof. + intros l Hnodup (k,e). + rewrite <- bindings_mapsto_iff, of_list_1; intuition. + Qed. + + Lemma of_list_3 : forall s, Equal (of_list (to_list s)) s. + Proof. + intros s k. + rewrite of_list_1b, bindings_o; auto. + apply bindings_3w. + Qed. + + (** * Fold *) + + (** Alternative specification via [fold_right] *) + + Lemma fold_spec_right m (A:Type)(i:A)(f : key -> elt -> A -> A) : + fold f m i = List.fold_right (uncurry f) i (rev (bindings m)). + Proof. + rewrite fold_1. symmetry. apply fold_left_rev_right. + Qed. + + (** ** Induction principles about fold contributed by S. Lescuyer *) + + (** In the following lemma, the step hypothesis is deliberately restricted + to the precise map m we are considering. *) + + Lemma fold_rec : + forall (A:Type)(P : t elt -> A -> Type)(f : key -> elt -> A -> A), + forall (i:A)(m:t elt), + (forall m, Empty m -> P m i) -> + (forall k e a m' m'', MapsTo k e m -> ~In k m' -> + Add k e m' m'' -> P m' a -> P m'' (f k e a)) -> + P m (fold f m i). + Proof. + intros A P f i m Hempty Hstep. + rewrite fold_spec_right. + set (F:=uncurry f). + set (l:=rev (bindings m)). + assert (Hstep' : forall k e a m' m'', InA eqke (k,e) l -> ~In k m' -> + Add k e m' m'' -> P m' a -> P m'' (F (k,e) a)). + { + intros k e a m' m'' H ? ? ?; eapply Hstep; eauto. + revert H; unfold l; rewrite InA_rev, bindings_mapsto_iff; auto with *. } + assert (Hdup : NoDupA eqk l). + { unfold l. apply NoDupA_rev; try red; unfold eq_key ; eauto with *. + apply bindings_3w. } + assert (Hsame : forall k, find k m = findA (eqb k) l). + { intros k. unfold l. rewrite bindings_o, findA_rev; auto. + apply bindings_3w. } + clearbody l. clearbody F. clear Hstep f. revert m Hsame. induction l. + - (* empty *) + intros m Hsame; simpl. + apply Hempty. intros k e. + rewrite find_mapsto_iff, Hsame; simpl; discriminate. + - (* step *) + intros m Hsame; destruct a as (k,e); simpl. + apply Hstep' with (of_list l); auto. + + rewrite InA_cons; left; red; auto with map. + + inversion_clear Hdup. contradict H. destruct H as (e',He'). + apply InA_eqke_eqk with k e'; auto with map. + rewrite <- of_list_1; auto. + + intro k'. rewrite Hsame, add_o, of_list_1b. simpl. + rewrite eqb_sym. unfold eqb. now destruct E.eq_dec. + inversion_clear Hdup; auto with map. + + apply IHl. + * intros; eapply Hstep'; eauto. + * inversion_clear Hdup; auto. + * intros; apply of_list_1b. inversion_clear Hdup; auto. + Qed. + + (** Same, with [empty] and [add] instead of [Empty] and [Add]. In this + case, [P] must be compatible with equality of sets *) + + Theorem fold_rec_bis : + forall (A:Type)(P : t elt -> A -> Type)(f : key -> elt -> A -> A), + forall (i:A)(m:t elt), + (forall m m' a, Equal m m' -> P m a -> P m' a) -> + (P empty i) -> + (forall k e a m', MapsTo k e m -> ~In k m' -> + P m' a -> P (add k e m') (f k e a)) -> + P m (fold f m i). + Proof. + intros A P f i m Pmorphism Pempty Pstep. + apply fold_rec; intros. + apply Pmorphism with empty; auto. intro k. rewrite empty_o. + case_eq (find k m0); auto; intros e'; rewrite <- find_mapsto_iff. + intro H'; elim (H k e'); auto. + apply Pmorphism with (add k e m'); try intro; auto. + Qed. + + Lemma fold_rec_nodep : + forall (A:Type)(P : A -> Type)(f : key -> elt -> A -> A)(i:A)(m:t elt), + P i -> (forall k e a, MapsTo k e m -> P a -> P (f k e a)) -> + P (fold f m i). + Proof. + intros; apply fold_rec_bis with (P:=fun _ => P); auto. + Qed. + + (** [fold_rec_weak] is a weaker principle than [fold_rec_bis] : + the step hypothesis must here be applicable anywhere. + At the same time, it looks more like an induction principle, + and hence can be easier to use. *) + + Lemma fold_rec_weak : + forall (A:Type)(P : t elt -> A -> Type)(f : key -> elt -> A -> A)(i:A), + (forall m m' a, Equal m m' -> P m a -> P m' a) -> + P empty i -> + (forall k e a m, ~In k m -> P m a -> P (add k e m) (f k e a)) -> + forall m, P m (fold f m i). + Proof. + intros; apply fold_rec_bis; auto. + Qed. + + Lemma fold_rel : + forall (A B:Type)(R : A -> B -> Type) + (f : key -> elt -> A -> A)(g : key -> elt -> B -> B)(i : A)(j : B) + (m : t elt), + R i j -> + (forall k e a b, MapsTo k e m -> R a b -> R (f k e a) (g k e b)) -> + R (fold f m i) (fold g m j). + Proof. + intros A B R f g i j m Rempty Rstep. + rewrite 2 fold_spec_right. set (l:=rev (bindings m)). + assert (Rstep' : forall k e a b, InA eqke (k,e) l -> + R a b -> R (f k e a) (g k e b)). + { intros; apply Rstep; auto. + rewrite bindings_mapsto_iff, <- InA_rev; auto with map. } + clearbody l; clear Rstep m. + induction l; simpl; auto. + apply Rstep'; auto. + destruct a; simpl; rewrite InA_cons; left; red; auto with map. + Qed. + + (** From the induction principle on [fold], we can deduce some general + induction principles on maps. *) + + Lemma map_induction : + forall P : t elt -> Type, + (forall m, Empty m -> P m) -> + (forall m m', P m -> forall x e, ~In x m -> Add x e m m' -> P m') -> + forall m, P m. + Proof. + intros. apply (@fold_rec _ (fun s _ => P s) (fun _ _ _ => tt) tt m); eauto. + Qed. + + Lemma map_induction_bis : + forall P : t elt -> Type, + (forall m m', Equal m m' -> P m -> P m') -> + P empty -> + (forall x e m, ~In x m -> P m -> P (add x e m)) -> + forall m, P m. + Proof. + intros. + apply (@fold_rec_bis _ (fun s _ => P s) (fun _ _ _ => tt) tt m); eauto. + Qed. + + (** [fold] can be used to reconstruct the same initial set. *) + + Lemma fold_identity : forall m : t elt, Equal (fold (@add _) m empty) m. + Proof. + intros. + apply fold_rec with (P:=fun m acc => Equal acc m); auto with map. + intros m' Heq k'. + rewrite empty_o. + case_eq (find k' m'); auto; intros e'; rewrite <- find_mapsto_iff. + intro; elim (Heq k' e'); auto. + intros k e a m' m'' _ _ Hadd Heq k'. + red in Heq. rewrite Hadd, 2 add_o, Heq; auto. + Qed. + + Section Fold_More. + + (** ** Additional properties of fold *) + + (** When a function [f] is compatible and allows transpositions, we can + compute [fold f] in any order. *) + + Variables (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA). + + Lemma fold_Empty (f:key->elt->A->A) : + forall m i, Empty m -> eqA (fold f m i) i. + Proof. + intros. apply fold_rec_nodep with (P:=fun a => eqA a i). + reflexivity. + intros. elim (H k e); auto. + Qed. + + Lemma fold_init (f:key->elt->A->A) : + Proper (E.eq==>eq==>eqA==>eqA) f -> + forall m i i', eqA i i' -> eqA (fold f m i) (fold f m i'). + Proof. + intros Hf m i i' Hi. apply fold_rel with (R:=eqA); auto. + intros. now apply Hf. + Qed. + + (** Transpositions of f (a.k.a diamond property). + Could we swap two sequential calls to f, i.e. do we have: + + f k e (f k' e' a) == f k' e' (f k e a) + + First, we do no need this equation for all keys, but only + when k and k' aren't equal, as suggested by Pierre Castéran. + Think for instance of [f] being [M.add] : in general, we don't have + [M.add k e (M.add k e' m) == M.add k e' (M.add k e m)]. + Fortunately, we will never encounter this situation during a real + [fold], since the keys received by this [fold] are unique. + NB: without this condition, this condition would be + [SetoidList.transpose2]. + + Secondly, instead of the equation above, we now use a statement + with more basic equalities, allowing to prove [fold_commutes] even + when [f] isn't a morphism. + NB: When [f] is a morphism, [Diamond f] gives back the equation above. +*) + + Definition Diamond (f:key->elt->A->A) := + forall k k' e e' a b b', ~E.eq k k' -> + eqA (f k e a) b -> eqA (f k' e' a) b' -> eqA (f k e b') (f k' e' b). + + Lemma fold_commutes (f:key->elt->A->A) : + Diamond f -> + forall i m k e, ~In k m -> + eqA (fold f m (f k e i)) (f k e (fold f m i)). + Proof. + intros Hf i m k e H. + apply fold_rel with (R:= fun a b => eqA a (f k e b)); auto. + - reflexivity. + - intros k' e' b a Hm E. + apply Hf with a; try easy. + contradict H; rewrite <- H. now exists e'. + Qed. + + Hint Resolve NoDupA_eqk_eqke NoDupA_rev bindings_3w : map. + + Lemma fold_Proper (f:key->elt->A->A) : + Proper (E.eq==>eq==>eqA==>eqA) f -> + Diamond f -> + Proper (Equal==>eqA==>eqA) (fold f). + Proof. + intros Hf Hf' m1 m2 Hm i j Hi. + rewrite 2 fold_spec_right. + assert (NoDupA eqk (rev (bindings m1))) by (auto with * ). + assert (NoDupA eqk (rev (bindings m2))) by (auto with * ). + apply fold_right_equivlistA_restr2 with (R:=complement eqk)(eqA:=eqke) + ; auto with *. + - intros (k1,e1) (k2,e2) (Hk,He) a1 a2 Ha; simpl in *. now apply Hf. + - unfold complement, eq_key, eq_key_elt; repeat red. intuition eauto with map. + - intros (k,e) (k',e') z z' h h'; unfold eq_key, uncurry;simpl; auto. + rewrite h'. eapply Hf'; now eauto. + - rewrite <- NoDupA_altdef; auto. + - intros (k,e). + rewrite 2 InA_rev, <- 2 bindings_mapsto_iff, 2 find_mapsto_iff, Hm; + auto with *. + Qed. + + Lemma fold_Equal (f:key->elt->A->A) : + Proper (E.eq==>eq==>eqA==>eqA) f -> + Diamond f -> + forall m1 m2 i, + Equal m1 m2 -> + eqA (fold f m1 i) (fold f m2 i). + Proof. + intros. now apply fold_Proper. + Qed. + + Lemma fold_Add (f:key->elt->A->A) : + Proper (E.eq==>eq==>eqA==>eqA) f -> + Diamond f -> + forall m1 m2 k e i, ~In k m1 -> Add k e m1 m2 -> + eqA (fold f m2 i) (f k e (fold f m1 i)). + Proof. + intros Hf Hf' m1 m2 k e i Hm1 Hm2. + rewrite 2 fold_spec_right. + set (f':=uncurry f). + change (f k e (fold_right f' i (rev (bindings m1)))) + with (f' (k,e) (fold_right f' i (rev (bindings m1)))). + assert (NoDupA eqk (rev (bindings m1))) by (auto with * ). + assert (NoDupA eqk (rev (bindings m2))) by (auto with * ). + apply fold_right_add_restr with + (R:=complement eqk)(eqA:=eqke); auto with *. + - intros (k1,e1) (k2,e2) (Hk,He) a a' Ha; unfold f'; simpl in *. now apply Hf. + - unfold complement, eq_key_elt, eq_key; repeat red; intuition eauto with map. + - intros (k1,e1) (k2,e2) z1 z2; unfold eq_key, f', uncurry; simpl. + eapply Hf'; now eauto. + - rewrite <- NoDupA_altdef; auto. + - rewrite InA_rev, <- bindings_mapsto_iff by (auto with * ). firstorder. + - intros (a,b). + rewrite InA_cons, 2 InA_rev, <- 2 bindings_mapsto_iff, + 2 find_mapsto_iff by (auto with * ). + unfold eq_key_elt; simpl. + rewrite Hm2, !find_spec, add_mapsto_new; intuition. + Qed. + + Lemma fold_add (f:key->elt->A->A) : + Proper (E.eq==>eq==>eqA==>eqA) f -> + Diamond f -> + forall m k e i, ~In k m -> + eqA (fold f (add k e m) i) (f k e (fold f m i)). + Proof. + intros. now apply fold_Add. + Qed. + + End Fold_More. + + (** * Cardinal *) + + Lemma cardinal_fold (m : t elt) : + cardinal m = fold (fun _ _ => S) m 0. + Proof. + rewrite cardinal_1, fold_1. + symmetry; apply fold_left_length; auto. + Qed. + + Lemma cardinal_Empty : forall m : t elt, + Empty m <-> cardinal m = 0. + Proof. + intros. + rewrite cardinal_1, bindings_Empty. + destruct (bindings m); intuition; discriminate. + Qed. + + Lemma Equal_cardinal (m m' : t elt) : + Equal m m' -> cardinal m = cardinal m'. + Proof. + intro. rewrite 2 cardinal_fold. + apply fold_Equal with (eqA:=eq); try congruence; auto with map. + Qed. + + Lemma cardinal_0 (m : t elt) : Empty m -> cardinal m = 0. + Proof. + intros; rewrite <- cardinal_Empty; auto. + Qed. + + Lemma cardinal_S m m' x e : + ~ In x m -> Add x e m m' -> cardinal m' = S (cardinal m). + Proof. + intros. rewrite 2 cardinal_fold. + change S with ((fun _ _ => S) x e). + apply fold_Add with (eqA:=eq); try congruence; auto with map. + Qed. + + Lemma cardinal_inv_1 : forall m : t elt, + cardinal m = 0 -> Empty m. + Proof. + intros; rewrite cardinal_Empty; auto. + Qed. + Hint Resolve cardinal_inv_1 : map. + + Lemma cardinal_inv_2 : + forall m n, cardinal m = S n -> { p : key*elt | MapsTo (fst p) (snd p) m }. + Proof. + intros; rewrite M.cardinal_spec in *. + generalize (bindings_mapsto_iff m). + destruct (bindings m); try discriminate. + exists p; auto. + rewrite H0; destruct p; simpl; auto. + constructor; red; auto with map. + Qed. + + Lemma cardinal_inv_2b : + forall m, cardinal m <> 0 -> { p : key*elt | MapsTo (fst p) (snd p) m }. + Proof. + intros. + generalize (@cardinal_inv_2 m); destruct cardinal. + elim H;auto. + eauto. + Qed. + + Lemma not_empty_mapsto (m : t elt) : + ~Empty m -> exists k e, MapsTo k e m. + Proof. + intro. + destruct (@cardinal_inv_2b m) as ((k,e),H'). + contradict H. now apply cardinal_inv_1. + exists k; now exists e. + Qed. + + Lemma not_empty_in (m:t elt) : + ~Empty m -> exists k, In k m. + Proof. + intro. destruct (not_empty_mapsto H) as (k,Hk). + now exists k. + Qed. + + (** * Additional notions over maps *) + + Definition Disjoint (m m' : t elt) := + forall k, ~(In k m /\ In k m'). + + Definition Partition (m m1 m2 : t elt) := + Disjoint m1 m2 /\ + (forall k e, MapsTo k e m <-> MapsTo k e m1 \/ MapsTo k e m2). + + (** * Emulation of some functions lacking in the interface *) + + Definition filter (f : key -> elt -> bool)(m : t elt) := + fold (fun k e m => if f k e then add k e m else m) m empty. + + Definition for_all (f : key -> elt -> bool)(m : t elt) := + fold (fun k e b => if f k e then b else false) m true. + + Definition exists_ (f : key -> elt -> bool)(m : t elt) := + fold (fun k e b => if f k e then true else b) m false. + + Definition partition (f : key -> elt -> bool)(m : t elt) := + (filter f m, filter (fun k e => negb (f k e)) m). + + (** [update] adds to [m1] all the bindings of [m2]. It can be seen as + an [union] operator which gives priority to its 2nd argument + in case of binding conflit. *) + + Definition update (m1 m2 : t elt) := fold (@add _) m2 m1. + + (** [restrict] keeps from [m1] only the bindings whose key is in [m2]. + It can be seen as an [inter] operator, with priority to its 1st argument + in case of binding conflit. *) + + Definition restrict (m1 m2 : t elt) := filter (fun k _ => mem k m2) m1. + + (** [diff] erases from [m1] all bindings whose key is in [m2]. *) + + Definition diff (m1 m2 : t elt) := filter (fun k _ => negb (mem k m2)) m1. + + (** Properties of these abbreviations *) + + Lemma filter_iff (f : key -> elt -> bool) : + Proper (E.eq==>eq==>eq) f -> + forall m k e, + MapsTo k e (filter f m) <-> MapsTo k e m /\ f k e = true. + Proof. + unfold filter. + set (f':=fun k e m => if f k e then add k e m else m). + intros Hf m. pattern m, (fold f' m empty). apply fold_rec. + + - intros m' Hm' k e. rewrite empty_mapsto_iff. intuition. + elim (Hm' k e); auto. + + - intros k e acc m1 m2 Hke Hn Hadd IH k' e'. + change (Equal m2 (add k e m1)) in Hadd; rewrite Hadd. + unfold f'; simpl. + rewrite add_mapsto_new by trivial. + case_eq (f k e); intros Hfke; simpl; + rewrite ?add_mapsto_iff, IH; clear IH; intuition. + + rewrite <- Hfke; apply Hf; auto with map. + + right. repeat split; trivial. contradict Hn. rewrite Hn. now exists e'. + + assert (f k e = f k' e') by (apply Hf; auto). congruence. + Qed. + + Lemma for_all_filter f m : + for_all f m = is_empty (filter (fun k e => negb (f k e)) m). + Proof. + unfold for_all, filter. + eapply fold_rel with (R:=fun x y => x = is_empty y). + - symmetry. apply is_empty_iff. apply empty_1. + - intros; subst. destruct (f k e); simpl; trivial. + symmetry. apply not_true_is_false. rewrite is_empty_spec. + intros H'. specialize (H' k). now rewrite add_spec1 in H'. + Qed. + + Lemma exists_filter f m : + exists_ f m = negb (is_empty (filter f m)). + Proof. + unfold for_all, filter. + eapply fold_rel with (R:=fun x y => x = negb (is_empty y)). + - symmetry. rewrite negb_false_iff. apply is_empty_iff. apply empty_1. + - intros; subst. destruct (f k e); simpl; trivial. + symmetry. rewrite negb_true_iff. apply not_true_is_false. + rewrite is_empty_spec. + intros H'. specialize (H' k). now rewrite add_spec1 in H'. + Qed. + + Lemma for_all_iff f m : + Proper (E.eq==>eq==>eq) f -> + (for_all f m = true <-> (forall k e, MapsTo k e m -> f k e = true)). + Proof. + intros Hf. + rewrite for_all_filter. + rewrite <- is_empty_iff. unfold Empty. + split; intros H k e; specialize (H k e); + rewrite filter_iff in * by solve_proper; intuition. + - destruct (f k e); auto. + - now rewrite H0 in H2. + Qed. + + Lemma exists_iff f m : + Proper (E.eq==>eq==>eq) f -> + (exists_ f m = true <-> + (exists k e, MapsTo k e m /\ f k e = true)). + Proof. + intros Hf. + rewrite exists_filter. rewrite negb_true_iff. + rewrite <- not_true_iff_false, <- is_empty_iff. + split. + - intros H. apply not_empty_mapsto in H. now setoid_rewrite filter_iff in H. + - unfold Empty. setoid_rewrite filter_iff; trivial. firstorder. + Qed. + + Lemma Disjoint_alt : forall m m', + Disjoint m m' <-> + (forall k e e', MapsTo k e m -> MapsTo k e' m' -> False). + Proof. + unfold Disjoint; split. + intros H k v v' H1 H2. + apply H with k; split. + exists v; trivial. + exists v'; trivial. + intros H k ((v,Hv),(v',Hv')). + eapply H; eauto. + Qed. + + Section Partition. + Variable f : key -> elt -> bool. + Hypothesis Hf : Proper (E.eq==>eq==>eq) f. + + Lemma partition_iff_1 : forall m m1 k e, + m1 = fst (partition f m) -> + (MapsTo k e m1 <-> MapsTo k e m /\ f k e = true). + Proof. + unfold partition; simpl; intros. subst m1. + apply filter_iff; auto. + Qed. + + Lemma partition_iff_2 : forall m m2 k e, + m2 = snd (partition f m) -> + (MapsTo k e m2 <-> MapsTo k e m /\ f k e = false). + Proof. + unfold partition; simpl; intros. subst m2. + rewrite filter_iff. + split; intros (H,H'); split; auto. + destruct (f k e); simpl in *; auto. + rewrite H'; auto. + repeat red; intros. f_equal. apply Hf; auto. + Qed. + + Lemma partition_Partition : forall m m1 m2, + partition f m = (m1,m2) -> Partition m m1 m2. + Proof. + intros. split. + rewrite Disjoint_alt. intros k e e'. + rewrite (@partition_iff_1 m m1), (@partition_iff_2 m m2) + by (rewrite H; auto). + intros (U,V) (W,Z). rewrite <- (mapsto_fun U W) in Z; congruence. + intros k e. + rewrite (@partition_iff_1 m m1), (@partition_iff_2 m m2) + by (rewrite H; auto). + destruct (f k e); intuition. + Qed. + + End Partition. + + Lemma Partition_In : forall m m1 m2 k, + Partition m m1 m2 -> In k m -> {In k m1}+{In k m2}. + Proof. + intros m m1 m2 k Hm Hk. + destruct (In_dec m1 k) as [H|H]; [left|right]; auto. + destruct Hm as (Hm,Hm'). + destruct Hk as (e,He); rewrite Hm' in He; destruct He. + elim H; exists e; auto. + exists e; auto. + Defined. + + Lemma Disjoint_sym : forall m1 m2, Disjoint m1 m2 -> Disjoint m2 m1. + Proof. + intros m1 m2 H k (H1,H2). elim (H k); auto. + Qed. + + Lemma Partition_sym : forall m m1 m2, + Partition m m1 m2 -> Partition m m2 m1. + Proof. + intros m m1 m2 (H,H'); split. + apply Disjoint_sym; auto. + intros; rewrite H'; intuition. + Qed. + + Lemma Partition_Empty : forall m m1 m2, Partition m m1 m2 -> + (Empty m <-> (Empty m1 /\ Empty m2)). + Proof. + intros m m1 m2 (Hdisj,Heq). split. + intro He. + split; intros k e Hke; elim (He k e); rewrite Heq; auto. + intros (He1,He2) k e Hke. rewrite Heq in Hke. destruct Hke. + elim (He1 k e); auto. + elim (He2 k e); auto. + Qed. + + Lemma Partition_Add : + forall m m' x e , ~In x m -> Add x e m m' -> + forall m1 m2, Partition m' m1 m2 -> + exists m3, (Add x e m3 m1 /\ Partition m m3 m2 \/ + Add x e m3 m2 /\ Partition m m1 m3). + Proof. + unfold Partition. intros m m' x e Hn Hadd m1 m2 (Hdisj,Hor). + assert (Heq : Equal m (remove x m')). + { change (Equal m' (add x e m)) in Hadd. rewrite Hadd. + intro k. rewrite remove_o, add_o. + destruct E.eq_dec as [He|Hne]; auto. + rewrite <- He, <- not_find_in_iff; auto. } + assert (H : MapsTo x e m'). + { change (Equal m' (add x e m)) in Hadd; rewrite Hadd. + apply add_1; auto with map. } + rewrite Hor in H; destruct H. + + - (* first case : x in m1 *) + exists (remove x m1); left. split; [|split]. + + (* add *) + change (Equal m1 (add x e (remove x m1))). + intro k. + rewrite add_o, remove_o. + destruct E.eq_dec as [He|Hne]; auto. + rewrite <- He; apply find_1; auto. + + (* disjoint *) + intros k (H1,H2). elim (Hdisj k). split; auto. + rewrite remove_in_iff in H1; destruct H1; auto. + + (* mapsto *) + intros k' e'. + rewrite Heq, 2 remove_mapsto_iff, Hor. + intuition. + elim (Hdisj x); split; [exists e|exists e']; auto. + apply MapsTo_1 with k'; auto with map. + + - (* second case : x in m2 *) + exists (remove x m2); right. split; [|split]. + + (* add *) + change (Equal m2 (add x e (remove x m2))). + intro k. + rewrite add_o, remove_o. + destruct E.eq_dec as [He|Hne]; auto. + rewrite <- He; apply find_1; auto. + + (* disjoint *) + intros k (H1,H2). elim (Hdisj k). split; auto. + rewrite remove_in_iff in H2; destruct H2; auto. + + (* mapsto *) + intros k' e'. + rewrite Heq, 2 remove_mapsto_iff, Hor. + intuition. + elim (Hdisj x); split; [exists e'|exists e]; auto. + apply MapsTo_1 with k'; auto with map. + Qed. + + Lemma Partition_fold : + forall (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA)(f:key->elt->A->A), + Proper (E.eq==>eq==>eqA==>eqA) f -> + Diamond eqA f -> + forall m m1 m2 i, + Partition m m1 m2 -> + eqA (fold f m i) (fold f m1 (fold f m2 i)). + Proof. + intros A eqA st f Comp Tra. + induction m as [m Hm|m m' IH k e Hn Hadd] using map_induction. + + - intros m1 m2 i Hp. rewrite (fold_Empty (eqA:=eqA)); auto. + rewrite (Partition_Empty Hp) in Hm. destruct Hm. + rewrite 2 (fold_Empty (eqA:=eqA)); auto. reflexivity. + + - intros m1 m2 i Hp. + destruct (Partition_Add Hn Hadd Hp) as (m3,[(Hadd',Hp')|(Hadd',Hp')]). + + (* fst case: m3 is (k,e)::m1 *) + assert (~In k m3). + { contradict Hn. destruct Hn as (e',He'). + destruct Hp' as (Hp1,Hp2). exists e'. rewrite Hp2; auto. } + transitivity (f k e (fold f m i)). + apply fold_Add with (eqA:=eqA); auto. + symmetry. + transitivity (f k e (fold f m3 (fold f m2 i))). + apply fold_Add with (eqA:=eqA); auto. + apply Comp; auto with map. + symmetry; apply IH; auto. + + (* snd case: m3 is (k,e)::m2 *) + assert (~In k m3). + { contradict Hn. destruct Hn as (e',He'). + destruct Hp' as (Hp1,Hp2). exists e'. rewrite Hp2; auto. } + assert (~In k m1). + { contradict Hn. destruct Hn as (e',He'). + destruct Hp' as (Hp1,Hp2). exists e'. rewrite Hp2; auto. } + transitivity (f k e (fold f m i)). + apply fold_Add with (eqA:=eqA); auto. + transitivity (f k e (fold f m1 (fold f m3 i))). + apply Comp; auto using IH with map. + transitivity (fold f m1 (f k e (fold f m3 i))). + symmetry. + apply fold_commutes with (eqA:=eqA); auto. + apply fold_init with (eqA:=eqA); auto. + symmetry. + apply fold_Add with (eqA:=eqA); auto. + Qed. + + Lemma Partition_cardinal : forall m m1 m2, Partition m m1 m2 -> + cardinal m = cardinal m1 + cardinal m2. + Proof. + intros. + rewrite (cardinal_fold m), (cardinal_fold m1). + set (f:=fun (_:key)(_:elt)=>S). + setoid_replace (fold f m 0) with (fold f m1 (fold f m2 0)). + rewrite <- cardinal_fold. + apply fold_rel with (R:=fun u v => u = v + cardinal m2); simpl; auto. + apply Partition_fold with (eqA:=eq); compute; auto with map. congruence. + Qed. + + Lemma Partition_partition : forall m m1 m2, Partition m m1 m2 -> + let f := fun k (_:elt) => mem k m1 in + Equal m1 (fst (partition f m)) /\ Equal m2 (snd (partition f m)). + Proof. + intros m m1 m2 Hm f. + assert (Hf : Proper (E.eq==>eq==>eq) f). + intros k k' Hk e e' _; unfold f; rewrite Hk; auto. + set (m1':= fst (partition f m)). + set (m2':= snd (partition f m)). + split; rewrite Equal_mapsto_iff; intros k e. + rewrite (@partition_iff_1 f Hf m m1') by auto. + unfold f. + rewrite <- mem_in_iff. + destruct Hm as (Hm,Hm'). + rewrite Hm'. + intuition. + exists e; auto. + elim (Hm k); split; auto; exists e; auto. + rewrite (@partition_iff_2 f Hf m m2') by auto. + unfold f. + rewrite <- not_mem_in_iff. + destruct Hm as (Hm,Hm'). + rewrite Hm'. + intuition. + elim (Hm k); split; auto; exists e; auto. + elim H1; exists e; auto. + Qed. + + Lemma update_mapsto_iff : forall m m' k e, + MapsTo k e (update m m') <-> + (MapsTo k e m' \/ (MapsTo k e m /\ ~In k m')). + Proof. + unfold update. + intros m m'. + pattern m', (fold (@add _) m' m). apply fold_rec. + + - intros m0 Hm0 k e. + assert (~In k m0) by (intros (e0,He0); apply (Hm0 k e0); auto). + intuition. + elim (Hm0 k e); auto. + + - intros k e m0 m1 m2 _ Hn Hadd IH k' e'. + change (Equal m2 (add k e m1)) in Hadd. + rewrite Hadd, 2 add_mapsto_iff, IH, add_in_iff. clear IH. intuition. + Qed. + + Lemma update_dec : forall m m' k e, MapsTo k e (update m m') -> + { MapsTo k e m' } + { MapsTo k e m /\ ~In k m'}. + Proof. + intros m m' k e H. rewrite update_mapsto_iff in H. + destruct (In_dec m' k) as [H'|H']; [left|right]; intuition. + elim H'; exists e; auto. + Defined. + + Lemma update_in_iff : forall m m' k, + In k (update m m') <-> In k m \/ In k m'. + Proof. + intros m m' k. split. + intros (e,H); rewrite update_mapsto_iff in H. + destruct H; [right|left]; exists e; intuition. + destruct (In_dec m' k) as [H|H]. + destruct H as (e,H). intros _; exists e. + rewrite update_mapsto_iff; left; auto. + destruct 1 as [H'|H']; [|elim H; auto]. + destruct H' as (e,H'). exists e. + rewrite update_mapsto_iff; right; auto. + Qed. + + Lemma diff_mapsto_iff : forall m m' k e, + MapsTo k e (diff m m') <-> MapsTo k e m /\ ~In k m'. + Proof. + intros m m' k e. + unfold diff. + rewrite filter_iff. + intuition. + rewrite mem_1 in *; auto; discriminate. + intros ? ? Hk _ _ _; rewrite Hk; auto. + Qed. + + Lemma diff_in_iff : forall m m' k, + In k (diff m m') <-> In k m /\ ~In k m'. + Proof. + intros m m' k. split. + intros (e,H); rewrite diff_mapsto_iff in H. + destruct H; split; auto. exists e; auto. + intros ((e,H),H'); exists e; rewrite diff_mapsto_iff; auto. + Qed. + + Lemma restrict_mapsto_iff : forall m m' k e, + MapsTo k e (restrict m m') <-> MapsTo k e m /\ In k m'. + Proof. + intros m m' k e. + unfold restrict. + rewrite filter_iff. + intuition. + intros ? ? Hk _ _ _; rewrite Hk; auto. + Qed. + + Lemma restrict_in_iff : forall m m' k, + In k (restrict m m') <-> In k m /\ In k m'. + Proof. + intros m m' k. split. + intros (e,H); rewrite restrict_mapsto_iff in H. + destruct H; split; auto. exists e; auto. + intros ((e,H),H'); exists e; rewrite restrict_mapsto_iff; auto. + Qed. + + (** specialized versions analyzing only keys (resp. bindings) *) + + Definition filter_dom (f : key -> bool) := filter (fun k _ => f k). + Definition filter_range (f : elt -> bool) := filter (fun _ => f). + Definition for_all_dom (f : key -> bool) := for_all (fun k _ => f k). + Definition for_all_range (f : elt -> bool) := for_all (fun _ => f). + Definition exists_dom (f : key -> bool) := exists_ (fun k _ => f k). + Definition exists_range (f : elt -> bool) := exists_ (fun _ => f). + Definition partition_dom (f : key -> bool) := partition (fun k _ => f k). + Definition partition_range (f : elt -> bool) := partition (fun _ => f). + + End Elt. + + Instance cardinal_m {elt} : Proper (Equal ==> Logic.eq) (@cardinal elt). + Proof. intros m m'. apply Equal_cardinal. Qed. + + Instance Disjoint_m {elt} : Proper (Equal ==> Equal ==> iff) (@Disjoint elt). + Proof. + intros m1 m1' Hm1 m2 m2' Hm2. unfold Disjoint. split; intros. + rewrite <- Hm1, <- Hm2; auto. + rewrite Hm1, Hm2; auto. + Qed. + + Instance Partition_m {elt} : + Proper (Equal ==> Equal ==> Equal ==> iff) (@Partition elt). + Proof. + intros m1 m1' Hm1 m2 m2' Hm2 m3 m3' Hm3. unfold Partition. + rewrite <- Hm2, <- Hm3. + split; intros (H,H'); split; auto; intros. + rewrite <- Hm1, <- Hm2, <- Hm3; auto. + rewrite Hm1, Hm2, Hm3; auto. + Qed. + +(* + Instance filter_m0 {elt} (f:key->elt->bool) : + Proper (E.eq==>Logic.eq==>Logic.eq) f -> + Proper (Equal==>Equal) (filter f). + Proof. + intros Hf m m' Hm. apply Equal_mapsto_iff. intros. + now rewrite !filter_iff, Hm. + Qed. +*) + + Instance filter_m {elt} : + Proper ((E.eq==>Logic.eq==>Logic.eq)==>Equal==>Equal) (@filter elt). + Proof. + intros f f' Hf m m' Hm. unfold filter. + rewrite 2 fold_spec_right. + set (l := rev (bindings m)). + set (l' := rev (bindings m')). + set (op := fun (f:key->elt->bool) => + uncurry (fun k e acc => if f k e then add k e acc else acc)). + change (Equal (fold_right (op f) empty l) (fold_right (op f') empty l')). + assert (Hl : NoDupA eq_key l). + { apply NoDupA_rev. apply eqk_equiv. apply bindings_spec2w. } + assert (Hl' : NoDupA eq_key l'). + { apply NoDupA_rev. apply eqk_equiv. apply bindings_spec2w. } + assert (H : PermutationA eq_key_elt l l'). + { apply NoDupA_equivlistA_PermutationA. + - apply eqke_equiv. + - now apply NoDupA_eqk_eqke. + - now apply NoDupA_eqk_eqke. + - intros (k,e); unfold l, l'. rewrite 2 InA_rev, 2 bindings_spec1. + rewrite Equal_mapsto_iff in Hm. apply Hm. } + destruct (PermutationA_decompose (eqke_equiv _) H) as (l0,(P,E)). + transitivity (fold_right (op f) empty l0). + - apply fold_right_equivlistA_restr2 + with (eqA:=Logic.eq)(R:=complement eq_key); auto with *. + + intros p p' <- acc acc' Hacc. + destruct p as (k,e); unfold op, uncurry; simpl. + destruct (f k e); now rewrite Hacc. + + intros (k,e) (k',e') z z'. + unfold op, complement, uncurry, eq_key; simpl. + intros Hk Hz. + destruct (f k e), (f k' e'); rewrite <- Hz; try reflexivity. + now apply add_add_2. + + apply NoDupA_incl with eq_key; trivial. intros; subst; now red. + + apply PermutationA_preserves_NoDupA with l; auto with *. + apply Permutation_PermutationA; auto with *. + apply NoDupA_incl with eq_key; trivial. intros; subst; now red. + + apply NoDupA_altdef. apply NoDupA_rev. apply eqk_equiv. + apply bindings_spec2w. + + apply PermutationA_equivlistA; auto with *. + apply Permutation_PermutationA; auto with *. + - clearbody l'. clear l Hl Hl' H P m m' Hm. + induction E. + + reflexivity. + + simpl. destruct x as (k,e), x' as (k',e'). + unfold op, uncurry at 1 3; simpl. + destruct H; simpl in *. rewrite <- (Hf _ _ H _ _ H0). + destruct (f k e); trivial. now f_equiv. + Qed. + + Instance for_all_m {elt} : + Proper ((E.eq==>Logic.eq==>Logic.eq)==>Equal==>Logic.eq) (@for_all elt). + Proof. + intros f f' Hf m m' Hm. rewrite 2 for_all_filter. + (* Strange: we cannot rewrite Hm here... *) + f_equiv. f_equiv; trivial. + intros k k' Hk e e' He. f_equal. now apply Hf. + Qed. + + Instance exists_m {elt} : + Proper ((E.eq==>Logic.eq==>Logic.eq)==>Equal==>Logic.eq) (@exists_ elt). + Proof. + intros f f' Hf m m' Hm. rewrite 2 exists_filter. + f_equal. now apply is_empty_m, filter_m. + Qed. + + Fact diamond_add {elt} : Diamond Equal (@add elt). + Proof. + intros k k' e e' a b b' Hk <- <-. now apply add_add_2. + Qed. + + Instance update_m {elt} : Proper (Equal ==> Equal ==> Equal) (@update elt). + Proof. + intros m1 m1' Hm1 m2 m2' Hm2. + unfold update. + apply fold_Proper; auto using diamond_add with *. + Qed. + + Instance restrict_m {elt} : Proper (Equal==>Equal==>Equal) (@restrict elt). + Proof. + intros m1 m1' Hm1 m2 m2' Hm2 y. + unfold restrict. + apply eq_option_alt. intros e. + rewrite !find_spec, !filter_iff, Hm1, Hm2. reflexivity. + clear. intros x x' Hx e e' He. now rewrite Hx. + clear. intros x x' Hx e e' He. now rewrite Hx. + Qed. + + Instance diff_m {elt} : Proper (Equal==>Equal==>Equal) (@diff elt). + Proof. + intros m1 m1' Hm1 m2 m2' Hm2 y. + unfold diff. + apply eq_option_alt. intros e. + rewrite !find_spec, !filter_iff, Hm1, Hm2. reflexivity. + clear. intros x x' Hx e e' He. now rewrite Hx. + clear. intros x x' Hx e e' He. now rewrite Hx. + Qed. + +End WProperties_fun. + +(** * Same Properties for self-contained weak maps and for full maps *) + +Module WProperties (M:WS) := WProperties_fun M.E M. +Module Properties := WProperties. + +(** * Properties specific to maps with ordered keys *) + +Module OrdProperties (M:S). + Module Import ME := OrderedTypeFacts M.E. + Module Import O:=KeyOrderedType M.E. + Module Import P:=Properties M. + Import M. + + Section Elt. + Variable elt:Type. + + Definition Above x (m:t elt) := forall y, In y m -> E.lt y x. + Definition Below x (m:t elt) := forall y, In y m -> E.lt x y. + + Section Bindings. + + Lemma sort_equivlistA_eqlistA : forall l l' : list (key*elt), + sort ltk l -> sort ltk l' -> equivlistA eqke l l' -> eqlistA eqke l l'. + Proof. + apply SortA_equivlistA_eqlistA; eauto with *. + Qed. + + Ltac klean := unfold O.eqke, O.ltk, RelCompFun in *; simpl in *. + Ltac keauto := klean; intuition; eauto. + + Definition gtb (p p':key*elt) := + match E.compare (fst p) (fst p') with Gt => true | _ => false end. + Definition leb p := fun p' => negb (gtb p p'). + + Definition bindings_lt p m := List.filter (gtb p) (bindings m). + Definition bindings_ge p m := List.filter (leb p) (bindings m). + + Lemma gtb_1 : forall p p', gtb p p' = true <-> ltk p' p. + Proof. + intros (x,e) (y,e'); unfold gtb; klean. + case E.compare_spec; intuition; try discriminate; ME.order. + Qed. + + Lemma leb_1 : forall p p', leb p p' = true <-> ~ltk p' p. + Proof. + intros (x,e) (y,e'); unfold leb, gtb; klean. + case E.compare_spec; intuition; try discriminate; ME.order. + Qed. + + Instance gtb_compat : forall p, Proper (eqke==>eq) (gtb p). + Proof. + red; intros (x,e) (a,e') (b,e'') H; red in H; simpl in *; destruct H. + generalize (gtb_1 (x,e) (a,e'))(gtb_1 (x,e) (b,e'')); + destruct (gtb (x,e) (a,e')); destruct (gtb (x,e) (b,e'')); klean; auto. + - intros. symmetry; rewrite H2. rewrite <-H, <-H1; auto. + - intros. rewrite H1. rewrite H, <- H2; auto. + Qed. + + Instance leb_compat : forall p, Proper (eqke==>eq) (leb p). + Proof. + intros x a b H. unfold leb; f_equal; apply gtb_compat; auto. + Qed. + + Hint Resolve gtb_compat leb_compat bindings_spec2 : map. + + Lemma bindings_split : forall p m, + bindings m = bindings_lt p m ++ bindings_ge p m. + Proof. + unfold bindings_lt, bindings_ge, leb; intros. + apply filter_split with (eqA:=eqk) (ltA:=ltk); eauto with *. + intros; destruct x; destruct y; destruct p. + rewrite gtb_1 in H; klean. + apply not_true_iff_false in H0. rewrite gtb_1 in H0. klean. ME.order. + Qed. + + Lemma bindings_Add : forall m m' x e, ~In x m -> Add x e m m' -> + eqlistA eqke (bindings m') + (bindings_lt (x,e) m ++ (x,e):: bindings_ge (x,e) m). + Proof. + intros; unfold bindings_lt, bindings_ge. + apply sort_equivlistA_eqlistA; auto with *. + - apply (@SortA_app _ eqke); auto with *. + + apply (@filter_sort _ eqke); auto with *; keauto. + + constructor; auto with map. + * apply (@filter_sort _ eqke); auto with *; keauto. + * rewrite (@InfA_alt _ eqke); auto with *; try (keauto; fail). + { intros. + rewrite filter_InA in H1; auto with *; destruct H1. + rewrite leb_1 in H2. + destruct y; klean. + rewrite <- bindings_mapsto_iff in H1. + assert (~E.eq x t0). + { contradict H. + exists e0; apply MapsTo_1 with t0; auto. + ME.order. } + ME.order. } + { apply (@filter_sort _ eqke); auto with *; keauto. } + + intros. + rewrite filter_InA in H1; auto with *; destruct H1. + rewrite gtb_1 in H3. + destruct y; destruct x0; klean. + inversion_clear H2. + * red in H4; klean; destruct H4; simpl in *. ME.order. + * rewrite filter_InA in H4; auto with *; destruct H4. + rewrite leb_1 in H4. klean; ME.order. + - intros (k,e'). + rewrite InA_app_iff, InA_cons, 2 filter_InA, + <-2 bindings_mapsto_iff, leb_1, gtb_1, + find_mapsto_iff, (H0 k), <- find_mapsto_iff, + add_mapsto_iff by (auto with * ). + change (eqke (k,e') (x,e)) with (E.eq k x /\ e' = e). + klean. + split. + + intros [(->,->)|(Hk,Hm)]. + * right; now left. + * destruct (lt_dec k x); intuition. + + intros [(Hm,LT)|[(->,->)|(Hm,EQ)]]. + * right; split; trivial; ME.order. + * now left. + * destruct (eq_dec x k) as [Hk|Hk]. + elim H. exists e'. now rewrite Hk. + right; auto. + Qed. + + Lemma bindings_Add_Above : forall m m' x e, + Above x m -> Add x e m m' -> + eqlistA eqke (bindings m') (bindings m ++ (x,e)::nil). + Proof. + intros. + apply sort_equivlistA_eqlistA; auto with *. + apply (@SortA_app _ eqke); auto with *. + intros. + inversion_clear H2. + destruct x0; destruct y. + rewrite <- bindings_mapsto_iff in H1. + destruct H3; klean. + rewrite H2. + apply H; firstorder. + inversion H3. + red; intros a; destruct a. + rewrite InA_app_iff, InA_cons, InA_nil, <- 2 bindings_mapsto_iff, + find_mapsto_iff, (H0 t0), <- find_mapsto_iff, + add_mapsto_iff by (auto with *). + change (eqke (t0,e0) (x,e)) with (E.eq t0 x /\ e0 = e). + intuition. + destruct (E.eq_dec x t0) as [Heq|Hneq]; auto. + exfalso. + assert (In t0 m) by (exists e0; auto). + generalize (H t0 H1). + ME.order. + Qed. + + Lemma bindings_Add_Below : forall m m' x e, + Below x m -> Add x e m m' -> + eqlistA eqke (bindings m') ((x,e)::bindings m). + Proof. + intros. + apply sort_equivlistA_eqlistA; auto with *. + change (sort ltk (((x,e)::nil) ++ bindings m)). + apply (@SortA_app _ eqke); auto with *. + intros. + inversion_clear H1. + destruct y; destruct x0. + rewrite <- bindings_mapsto_iff in H2. + destruct H3; klean. + rewrite H1. + apply H; firstorder. + inversion H3. + red; intros a; destruct a. + rewrite InA_cons, <- 2 bindings_mapsto_iff, + find_mapsto_iff, (H0 t0), <- find_mapsto_iff, + add_mapsto_iff by (auto with * ). + change (eqke (t0,e0) (x,e)) with (E.eq t0 x /\ e0 = e). + intuition. + destruct (E.eq_dec x t0) as [Heq|Hneq]; auto. + exfalso. + assert (In t0 m) by (exists e0; auto). + generalize (H t0 H1). + ME.order. + Qed. + + Lemma bindings_Equal_eqlistA : forall (m m': t elt), + Equal m m' -> eqlistA eqke (bindings m) (bindings m'). + Proof. + intros. + apply sort_equivlistA_eqlistA; auto with *. + red; intros. + destruct x; do 2 rewrite <- bindings_mapsto_iff. + do 2 rewrite find_mapsto_iff; rewrite H; split; auto. + Qed. + + End Bindings. + + Section Min_Max_Elt. + + (** We emulate two [max_elt] and [min_elt] functions. *) + + Fixpoint max_elt_aux (l:list (key*elt)) := match l with + | nil => None + | (x,e)::nil => Some (x,e) + | (x,e)::l => max_elt_aux l + end. + Definition max_elt m := max_elt_aux (bindings m). + + Lemma max_elt_Above : + forall m x e, max_elt m = Some (x,e) -> Above x (remove x m). + Proof. + red; intros. + rewrite remove_in_iff in H0. + destruct H0. + rewrite bindings_in_iff in H1. + destruct H1. + unfold max_elt in *. + generalize (bindings_spec2 m). + revert x e H y x0 H0 H1. + induction (bindings m). + simpl; intros; try discriminate. + intros. + destruct a; destruct l; simpl in *. + injection H; clear H; intros; subst. + inversion_clear H1. + red in H; simpl in *; intuition. + now elim H0. + inversion H. + change (max_elt_aux (p::l) = Some (x,e)) in H. + generalize (IHl x e H); clear IHl; intros IHl. + inversion_clear H1; [ | inversion_clear H2; eauto ]. + red in H3; simpl in H3; destruct H3. + destruct p as (p1,p2). + destruct (E.eq_dec p1 x) as [Heq|Hneq]. + rewrite <- Heq; auto. + inversion_clear H2. + inversion_clear H5. + red in H2; simpl in H2; ME.order. + transitivity p1; auto. + inversion_clear H2. + inversion_clear H5. + red in H2; simpl in H2; ME.order. + eapply IHl; eauto with *. + econstructor; eauto. + red; eauto with *. + inversion H2; auto. + Qed. + + Lemma max_elt_MapsTo : + forall m x e, max_elt m = Some (x,e) -> MapsTo x e m. + Proof. + intros. + unfold max_elt in *. + rewrite bindings_mapsto_iff. + induction (bindings m). + simpl; try discriminate. + destruct a; destruct l; simpl in *. + injection H; intros; subst; constructor; red; auto with *. + constructor 2; auto. + Qed. + + Lemma max_elt_Empty : + forall m, max_elt m = None -> Empty m. + Proof. + intros. + unfold max_elt in *. + rewrite bindings_Empty. + induction (bindings m); auto. + destruct a; destruct l; simpl in *; try discriminate. + assert (H':=IHl H); discriminate. + Qed. + + Definition min_elt m : option (key*elt) := match bindings m with + | nil => None + | (x,e)::_ => Some (x,e) + end. + + Lemma min_elt_Below : + forall m x e, min_elt m = Some (x,e) -> Below x (remove x m). + Proof. + unfold min_elt, Below; intros. + rewrite remove_in_iff in H0; destruct H0. + rewrite bindings_in_iff in H1. + destruct H1. + generalize (bindings_spec2 m). + destruct (bindings m). + try discriminate. + destruct p; injection H; intros; subst. + inversion_clear H1. + red in H2; destruct H2; simpl in *; ME.order. + inversion_clear H4. + rewrite (@InfA_alt _ eqke) in H3; eauto with *. + apply (H3 (y,x0)); auto. + Qed. + + Lemma min_elt_MapsTo : + forall m x e, min_elt m = Some (x,e) -> MapsTo x e m. + Proof. + intros. + unfold min_elt in *. + rewrite bindings_mapsto_iff. + destruct (bindings m). + simpl; try discriminate. + destruct p; simpl in *. + injection H; intros; subst; constructor; red; auto with *. + Qed. + + Lemma min_elt_Empty : + forall m, min_elt m = None -> Empty m. + Proof. + intros. + unfold min_elt in *. + rewrite bindings_Empty. + destruct (bindings m); auto. + destruct p; simpl in *; discriminate. + Qed. + + End Min_Max_Elt. + + Section Induction_Principles. + + Lemma map_induction_max : + forall P : t elt -> Type, + (forall m, Empty m -> P m) -> + (forall m m', P m -> forall x e, Above x m -> Add x e m m' -> P m') -> + forall m, P m. + Proof. + intros; remember (cardinal m) as n; revert m Heqn; induction n; intros. + apply X; apply cardinal_inv_1; auto. + + case_eq (max_elt m); intros. + destruct p. + assert (Add k e (remove k m) m). + { apply max_elt_MapsTo, find_spec, add_id in H. + unfold Add. symmetry. now rewrite add_remove_1. } + apply X0 with (remove k m) k e; auto with map. + apply IHn. + assert (S n = S (cardinal (remove k m))). + { rewrite Heqn. + eapply cardinal_S; eauto with map. } + inversion H1; auto. + eapply max_elt_Above; eauto. + + apply X; apply max_elt_Empty; auto. + Qed. + + Lemma map_induction_min : + forall P : t elt -> Type, + (forall m, Empty m -> P m) -> + (forall m m', P m -> forall x e, Below x m -> Add x e m m' -> P m') -> + forall m, P m. + Proof. + intros; remember (cardinal m) as n; revert m Heqn; induction n; intros. + apply X; apply cardinal_inv_1; auto. + + case_eq (min_elt m); intros. + destruct p. + assert (Add k e (remove k m) m). + { apply min_elt_MapsTo, find_spec, add_id in H. + unfold Add. symmetry. now rewrite add_remove_1. } + apply X0 with (remove k m) k e; auto. + apply IHn. + assert (S n = S (cardinal (remove k m))). + { rewrite Heqn. + eapply cardinal_S; eauto with map. } + inversion H1; auto. + eapply min_elt_Below; eauto. + + apply X; apply min_elt_Empty; auto. + Qed. + + End Induction_Principles. + + Section Fold_properties. + + (** The following lemma has already been proved on Weak Maps, + but with one additionnal hypothesis (some [transpose] fact). *) + + Lemma fold_Equal : forall m1 m2 (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA) + (f:key->elt->A->A)(i:A), + Proper (E.eq==>eq==>eqA==>eqA) f -> + Equal m1 m2 -> + eqA (fold f m1 i) (fold f m2 i). + Proof. + intros m1 m2 A eqA st f i Hf Heq. + rewrite 2 fold_spec_right. + apply fold_right_eqlistA with (eqA:=eqke) (eqB:=eqA); auto. + intros (k,e) (k',e') (Hk,He) a a' Ha; simpl in *; apply Hf; auto. + apply eqlistA_rev. apply bindings_Equal_eqlistA. auto. + Qed. + + Lemma fold_Add_Above : forall m1 m2 x e (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA) + (f:key->elt->A->A)(i:A) (P:Proper (E.eq==>eq==>eqA==>eqA) f), + Above x m1 -> Add x e m1 m2 -> + eqA (fold f m2 i) (f x e (fold f m1 i)). + Proof. + intros. rewrite 2 fold_spec_right. set (f':=uncurry f). + transitivity (fold_right f' i (rev (bindings m1 ++ (x,e)::nil))). + apply fold_right_eqlistA with (eqA:=eqke) (eqB:=eqA); auto. + intros (k1,e1) (k2,e2) (Hk,He) a1 a2 Ha; unfold f'; simpl in *. apply P; auto. + apply eqlistA_rev. + apply bindings_Add_Above; auto. + rewrite distr_rev; simpl. + reflexivity. + Qed. + + Lemma fold_Add_Below : forall m1 m2 x e (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA) + (f:key->elt->A->A)(i:A) (P:Proper (E.eq==>eq==>eqA==>eqA) f), + Below x m1 -> Add x e m1 m2 -> + eqA (fold f m2 i) (fold f m1 (f x e i)). + Proof. + intros. rewrite 2 fold_spec_right. set (f':=uncurry f). + transitivity (fold_right f' i (rev (((x,e)::nil)++bindings m1))). + apply fold_right_eqlistA with (eqA:=eqke) (eqB:=eqA); auto. + intros (k1,e1) (k2,e2) (Hk,He) a1 a2 Ha; unfold f'; simpl in *; apply P; auto. + apply eqlistA_rev. + simpl; apply bindings_Add_Below; auto. + rewrite distr_rev; simpl. + rewrite fold_right_app. + reflexivity. + Qed. + + End Fold_properties. + + End Elt. + +End OrdProperties. diff --git a/theories/MMaps/MMapInterface.v b/theories/MMaps/MMapInterface.v new file mode 100644 index 00000000..05c5e5d8 --- /dev/null +++ b/theories/MMaps/MMapInterface.v @@ -0,0 +1,292 @@ +(***********************************************************************) +(* 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 *) + +(** This file proposes interfaces for finite maps *) + +Require Export Bool Equalities Orders SetoidList. +Set Implicit Arguments. +Unset Strict Implicit. + +(** When compared with Ocaml Map, this signature has been split in + several parts : + + - The first parts [WSfun] and [WS] propose signatures for weak + maps, which are maps with no ordering on the key type nor the + data type. [WSfun] and [WS] are almost identical, apart from the + fact that [WSfun] is expressed in a functorial way whereas [WS] + is self-contained. For obtaining an instance of such signatures, + a decidable equality on keys in enough (see for example + [FMapWeakList]). These signatures contain the usual operators + (add, find, ...). The only function that asks for more is + [equal], whose first argument should be a comparison on data. + + - Then comes [Sfun] and [S], that extend [WSfun] and [WS] to the + case where the key type is ordered. The main novelty is that + [bindings] is required to produce sorted lists. + + - Finally, [Sord] extends [S] with a complete comparison function. For + that, the data type should have a decidable total ordering as well. + + If unsure, what you're looking for is probably [S]: apart from [Sord], + all other signatures are subsets of [S]. + + Some additional differences with Ocaml: + + - no [iter] function, useless since Coq is purely functional + - [option] types are used instead of [Not_found] exceptions + +*) + + +Definition Cmp {elt:Type}(cmp:elt->elt->bool) e1 e2 := cmp e1 e2 = true. + +(** ** Weak signature for maps + + No requirements for an ordering on keys nor elements, only decidability + of equality on keys. First, a functorial signature: *) + +Module Type WSfun (E : DecidableType). + + Definition key := E.t. + Hint Transparent key. + + Definition eq_key {elt} (p p':key*elt) := E.eq (fst p) (fst p'). + + Definition eq_key_elt {elt} (p p':key*elt) := + E.eq (fst p) (fst p') /\ (snd p) = (snd p'). + + Parameter t : Type -> Type. + (** the abstract type of maps *) + + Section Ops. + + Parameter empty : forall {elt}, t elt. + (** The empty map. *) + + Variable elt:Type. + + Parameter is_empty : t elt -> bool. + (** Test whether a map is empty or not. *) + + Parameter add : key -> elt -> t elt -> t elt. + (** [add x y m] returns a map containing the same bindings as [m], + plus a binding of [x] to [y]. If [x] was already bound in [m], + its previous binding disappears. *) + + Parameter find : key -> t elt -> option elt. + (** [find x m] returns the current binding of [x] in [m], + or [None] if no such binding exists. *) + + Parameter remove : key -> t elt -> t elt. + (** [remove x m] returns a map containing the same bindings as [m], + except for [x] which is unbound in the returned map. *) + + Parameter mem : key -> t elt -> bool. + (** [mem x m] returns [true] if [m] contains a binding for [x], + and [false] otherwise. *) + + Parameter bindings : t elt -> list (key*elt). + (** [bindings m] returns an assoc list corresponding to the bindings + of [m], in any order. *) + + Parameter cardinal : t elt -> nat. + (** [cardinal m] returns the number of bindings in [m]. *) + + Parameter fold : forall A: Type, (key -> elt -> A -> A) -> t elt -> A -> A. + (** [fold f m a] computes [(f kN dN ... (f k1 d1 a)...)], + where [k1] ... [kN] are the keys of all bindings in [m] + (in any order), and [d1] ... [dN] are the associated data. *) + + Parameter equal : (elt -> elt -> bool) -> t elt -> t elt -> bool. + (** [equal cmp m1 m2] tests whether the maps [m1] and [m2] are equal, + that is, contain equal keys and associate them with equal data. + [cmp] is the equality predicate used to compare the data associated + with the keys. *) + + Variable elt' elt'' : Type. + + Parameter map : (elt -> elt') -> t elt -> t elt'. + (** [map f m] returns a map with same domain as [m], where the associated + value a of all bindings of [m] has been replaced by the result of the + application of [f] to [a]. Since Coq is purely functional, the order + in which the bindings are passed to [f] is irrelevant. *) + + Parameter mapi : (key -> elt -> elt') -> t elt -> t elt'. + (** Same as [map], but the function receives as arguments both the + key and the associated value for each binding of the map. *) + + Parameter merge : (key -> option elt -> option elt' -> option elt'') -> + t elt -> t elt' -> t elt''. + (** [merge f m m'] creates a new map whose bindings belong to the ones + of either [m] or [m']. The presence and value for a key [k] is + determined by [f k e e'] where [e] and [e'] are the (optional) + bindings of [k] in [m] and [m']. *) + + End Ops. + Section Specs. + + Variable elt:Type. + + Parameter MapsTo : key -> elt -> t elt -> Prop. + + Definition In (k:key)(m: t elt) : Prop := exists e:elt, MapsTo k e m. + + Global Declare Instance MapsTo_compat : + Proper (E.eq==>Logic.eq==>Logic.eq==>iff) MapsTo. + + Variable m m' : t elt. + Variable x y : key. + Variable e : elt. + + Parameter find_spec : find x m = Some e <-> MapsTo x e m. + Parameter mem_spec : mem x m = true <-> In x m. + Parameter empty_spec : find x (@empty elt) = None. + Parameter is_empty_spec : is_empty m = true <-> forall x, find x m = None. + Parameter add_spec1 : find x (add x e m) = Some e. + Parameter add_spec2 : ~E.eq x y -> find y (add x e m) = find y m. + Parameter remove_spec1 : find x (remove x m) = None. + Parameter remove_spec2 : ~E.eq x y -> find y (remove x m) = find y m. + + (** Specification of [bindings] *) + Parameter bindings_spec1 : + InA eq_key_elt (x,e) (bindings m) <-> MapsTo x e m. + (** When compared with ordered maps, here comes the only + property that is really weaker: *) + Parameter bindings_spec2w : NoDupA eq_key (bindings m). + + (** Specification of [cardinal] *) + Parameter cardinal_spec : cardinal m = length (bindings m). + + (** Specification of [fold] *) + Parameter fold_spec : + forall {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. + + (** Equality of maps *) + + (** Caveat: there are at least three distinct equality predicates on maps. + - The simpliest (and maybe most natural) way is to consider keys up to + their equivalence [E.eq], but elements up to Leibniz equality, in + the spirit of [eq_key_elt] above. This leads to predicate [Equal]. + - Unfortunately, this [Equal] predicate can't be used to describe + the [equal] function, since this function (for compatibility with + ocaml) expects a boolean comparison [cmp] that may identify more + elements than Leibniz. So logical specification of [equal] is done + via another predicate [Equivb] + - This predicate [Equivb] is quite ad-hoc with its boolean [cmp], + it can be generalized in a [Equiv] expecting a more general + (possibly non-decidable) equality predicate on elements *) + + Definition Equal (m m':t elt) := 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: elt->elt->bool) := Equiv (Cmp cmp). + + (** Specification of [equal] *) + Parameter equal_spec : forall cmp : elt -> elt -> bool, + equal cmp m m' = true <-> Equivb cmp m m'. + + End Specs. + Section SpecMaps. + + Variables elt elt' elt'' : Type. + + Parameter map_spec : forall (f:elt->elt') m x, + find x (map f m) = option_map f (find x m). + + Parameter mapi_spec : forall (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). + + Parameter merge_spec1 : + forall (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'). + + Parameter merge_spec2 : + forall (f:key -> option elt->option elt'->option elt'') m m' x, + In x (merge f m m') -> In x m \/ In x m'. + + End SpecMaps. +End WSfun. + +(** ** Static signature for Weak Maps + + Similar to [WSfun] but expressed in a self-contained way. *) + +Module Type WS. + Declare Module E : DecidableType. + Include WSfun E. +End WS. + + + +(** ** Maps on ordered keys, functorial signature *) + +Module Type Sfun (E : OrderedType). + Include WSfun E. + + Definition lt_key {elt} (p p':key*elt) := E.lt (fst p) (fst p'). + + (** Additional specification of [bindings] *) + + Parameter bindings_spec2 : forall {elt}(m : t elt), sort lt_key (bindings m). + + (** Remark: since [fold] is specified via [bindings], this stronger + specification of [bindings] has an indirect impact on [fold], + which can now be proved to receive bindings in increasing order. *) + +End Sfun. + + +(** ** Maps on ordered keys, self-contained signature *) + +Module Type S. + Declare Module E : OrderedType. + Include Sfun E. +End S. + + + +(** ** Maps with ordering both on keys and datas *) + +Module Type Sord. + + Declare Module Data : OrderedType. + Declare Module MapS : S. + Import MapS. + + Definition t := MapS.t Data.t. + + Include HasEq <+ HasLt <+ IsEq <+ IsStrOrder. + + Definition cmp e e' := + match Data.compare e e' with Eq => true | _ => false end. + + Parameter eq_spec : forall m m', eq m m' <-> Equivb cmp m m'. + + Parameter compare : t -> t -> comparison. + + Parameter compare_spec : forall m1 m2, CompSpec eq lt m1 m2 (compare m1 m2). + +End Sord. + + +(* TODO: provides filter + partition *) + +(* TODO: provide split + Parameter split : key -> t elt -> t elt * option elt * t elt. + + Parameter split_spec k m : + split k m = (filter (fun x -> E.compare x k) m, find k m, filter ...) + + min_binding, max_binding, choose ? +*) diff --git a/theories/MMaps/MMapList.v b/theories/MMaps/MMapList.v new file mode 100644 index 00000000..c521178c --- /dev/null +++ b/theories/MMaps/MMapList.v @@ -0,0 +1,1144 @@ +(***********************************************************************) +(* 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 *) + +(** This file proposes an implementation of the non-dependant interface + [MMapInterface.S] using lists of pairs ordered (increasing) with respect to + left projection. *) + +Require Import MMapInterface OrdersFacts OrdersLists. + +Set Implicit Arguments. +Unset Strict Implicit. + +Module Raw (X:OrderedType). + +Module Import MX := OrderedTypeFacts X. +Module Import PX := KeyOrderedType X. + +Definition key := X.t. +Definition t (elt:Type) := list (X.t * elt). + +Local Notation Sort := (sort ltk). +Local Notation Inf := (lelistA (ltk)). + +Section Elt. +Variable elt : Type. + +Ltac SortLt := + match goal with + | H1 : Sort ?m, H2:Inf (?k',?e') ?m, H3:In ?k ?m |- _ => + assert (X.lt k' k); + [let e := fresh "e" in destruct H3 as (e,H3); + change (ltk (k',e') (k,e)); + apply (Sort_Inf_In H1 H2 (InA_eqke_eqk H3)) | ] + | H1:Sort ?m, H2:Inf (?k',?e') ?m, H3:MapsTo ?k ?e ?m |- _ => + assert (X.lt k' k); + [change (ltk (k',e') (k,e)); + apply (Sort_Inf_In H1 H2 (InA_eqke_eqk H3)) | ] + | H1:Sort ?m, H2:Inf (?k',?e') ?m, H3:InA eqke (?k,?e) ?m |- _ => + assert (X.lt k' k); + [change (ltk (k',e') (k,e)); + apply (Sort_Inf_In H1 H2 (InA_eqke_eqk H3)) | ] + end. + +(** * [find] *) + +Fixpoint find (k:key) (m: t elt) : option elt := + match m with + | nil => None + | (k',x)::m' => + match X.compare k k' with + | Lt => None + | Eq => Some x + | Gt => find k m' + end + end. + +Lemma find_spec m (Hm:Sort m) x e : + find x m = Some e <-> MapsTo x e m. +Proof. + induction m as [|(k,e') m IH]; simpl. + - split. discriminate. inversion 1. + - inversion_clear Hm. + unfold MapsTo in *. rewrite InA_cons, eqke_def. + case X.compare_spec; intros. + + split. injection 1 as ->; auto. + intros [(_,<-)|IN]; trivial. SortLt. MX.order. + + split. discriminate. + intros [(E,<-)|IN]; trivial; try SortLt; MX.order. + + rewrite IH; trivial. split; auto. + intros [(E,<-)|IN]; trivial. MX.order. +Qed. + +(** * [mem] *) + +Fixpoint mem (k : key) (m : t elt) : bool := + match m with + | nil => false + | (k',_) :: l => + match X.compare k k' with + | Lt => false + | Eq => true + | Gt => mem k l + end + end. + +Lemma mem_spec m (Hm:Sort m) x : mem x m = true <-> In x m. +Proof. + induction m as [|(k,e') m IH]; simpl. + - split. discriminate. inversion 1. inversion_clear H0. + - inversion_clear Hm. + rewrite In_cons; simpl. + case X.compare_spec; intros. + + intuition. + + split. discriminate. intros [E|(e,IN)]. MX.order. + SortLt. MX.order. + + rewrite IH; trivial. split; auto. intros [E|IN]; trivial. + MX.order. +Qed. + +(** * [empty] *) + +Definition empty : t elt := nil. + +Lemma empty_spec x : find x empty = None. +Proof. + reflexivity. +Qed. + +Lemma empty_sorted : Sort empty. +Proof. + unfold empty; auto. +Qed. + +(** * [is_empty] *) + +Definition is_empty (l : t elt) : bool := if l then true else false. + +Lemma is_empty_spec m : + is_empty m = true <-> forall x, find x m = None. +Proof. + destruct m as [|(k,e) m]; simpl; split; trivial; try discriminate. + intros H. specialize (H k). now rewrite compare_refl in H. +Qed. + +(** * [add] *) + +Fixpoint add (k : key) (x : elt) (s : t elt) : t elt := + match s with + | nil => (k,x) :: nil + | (k',y) :: l => + match X.compare k k' with + | Lt => (k,x)::s + | Eq => (k,x)::l + | Gt => (k',y) :: add k x l + end + end. + +Lemma add_spec1 m x e : find x (add x e m) = Some e. +Proof. + induction m as [|(k,e') m IH]; simpl. + - now rewrite compare_refl. + - case X.compare_spec; simpl; rewrite ?compare_refl; trivial. + rewrite <- compare_gt_iff. now intros ->. +Qed. + +Lemma add_spec2 m x y e : ~X.eq x y -> find y (add x e m) = find y m. +Proof. + induction m as [|(k,e') m IH]; simpl. + - case X.compare_spec; trivial; MX.order. + - case X.compare_spec; simpl; intros; trivial. + + rewrite <-H. case X.compare_spec; trivial; MX.order. + + do 2 (case X.compare_spec; trivial; try MX.order). + + now rewrite IH. +Qed. + +Lemma add_Inf : forall (m:t elt)(x x':key)(e e':elt), + Inf (x',e') m -> ltk (x',e') (x,e) -> Inf (x',e') (add x e m). +Proof. + induction m. + simpl; intuition. + intros. + destruct a as (x'',e''). + inversion_clear H. + compute in H0,H1. + simpl; case X.compare; intuition. +Qed. +Hint Resolve add_Inf. + +Lemma add_sorted : forall m (Hm:Sort m) x e, Sort (add x e m). +Proof. + induction m. + simpl; intuition. + intros. + destruct a as (x',e'). + simpl; case (X.compare_spec x x'); intuition; inversion_clear Hm; auto. + constructor; auto. + apply Inf_eq with (x',e'); auto. +Qed. + +(** * [remove] *) + +Fixpoint remove (k : key) (s : t elt) : t elt := + match s with + | nil => nil + | (k',x) :: l => + match X.compare k k' with + | Lt => s + | Eq => l + | Gt => (k',x) :: remove k l + end + end. + +Lemma remove_spec1 m (Hm:Sort m) x : find x (remove x m) = None. +Proof. + induction m as [|(k,e') m IH]; simpl; trivial. + inversion_clear Hm. + case X.compare_spec; simpl. + - intros E. rewrite <- E in H0. + apply Sort_Inf_NotIn in H0; trivial. unfold In in H0. + setoid_rewrite <- find_spec in H0; trivial. + destruct (find x m); trivial. + elim H0; now exists e. + - rewrite <- compare_lt_iff. now intros ->. + - rewrite <- compare_gt_iff. intros ->; auto. +Qed. + +Lemma remove_spec2 m (Hm:Sort m) x y : + ~X.eq x y -> find y (remove x m) = find y m. +Proof. + induction m as [|(k,e') m IH]; simpl; trivial. + inversion_clear Hm. + case X.compare_spec; simpl; intros E E'; try rewrite IH; auto. + case X.compare_spec; simpl; trivial; try MX.order. + intros. rewrite <- E in H0,H1. clear E E'. + destruct (find y m) eqn:F; trivial. + apply find_spec in F; trivial. + SortLt. MX.order. +Qed. + +Lemma remove_Inf : forall (m:t elt)(Hm : Sort m)(x x':key)(e':elt), + Inf (x',e') m -> Inf (x',e') (remove x m). +Proof. + induction m. + simpl; intuition. + intros. + destruct a as (x'',e''). + inversion_clear H. + compute in H0. + simpl; case X.compare; intuition. + inversion_clear Hm. + apply Inf_lt with (x'',e''); auto. +Qed. +Hint Resolve remove_Inf. + +Lemma remove_sorted : forall m (Hm:Sort m) x, Sort (remove x m). +Proof. + induction m. + simpl; intuition. + intros. + destruct a as (x',e'). + simpl; case X.compare_spec; intuition; inversion_clear Hm; auto. +Qed. + +(** * [bindings] *) + +Definition bindings (m: t elt) := m. + +Lemma bindings_spec1 m x e : + InA eqke (x,e) (bindings m) <-> MapsTo x e m. +Proof. + reflexivity. +Qed. + +Lemma bindings_spec2 m (Hm:Sort m) : sort ltk (bindings m). +Proof. + auto. +Qed. + +Lemma bindings_spec2w m (Hm:Sort m) : NoDupA eqk (bindings m). +Proof. + now apply Sort_NoDupA. +Qed. + +(** * [fold] *) + +Fixpoint fold (A:Type)(f:key->elt->A->A)(m:t elt) (acc:A) : A := + match m with + | nil => acc + | (k,e)::m' => fold f m' (f k e acc) + end. + +Lemma fold_spec m : forall (A:Type)(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. + induction m as [|(k,e) m IH]; simpl; auto. +Qed. + +(** * [equal] *) + +Fixpoint equal (cmp:elt->elt->bool)(m m' : t elt) : bool := + match m, m' with + | nil, nil => true + | (x,e)::l, (x',e')::l' => + match X.compare x x' with + | Eq => cmp e e' && equal cmp l l' + | _ => false + end + | _, _ => false + end. + +Definition Equivb (cmp:elt->elt->bool) m m' := + (forall k, In k m <-> In k m') /\ + (forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true). + +Lemma equal_1 : forall m (Hm:Sort m) m' (Hm': Sort m') cmp, + Equivb cmp m m' -> equal cmp m m' = true. +Proof. + induction m as [|(k,e) m IH]; destruct m' as [|(k',e') m']; simpl. + - trivial. + - intros _ cmp (H,_). + exfalso. apply (@In_nil elt k'). rewrite H, In_cons. now left. + - intros _ cmp (H,_). + exfalso. apply (@In_nil elt k). rewrite <- H, In_cons. now left. + - intros Hm' cmp E. + inversion_clear Hm; inversion_clear Hm'. + case X.compare_spec; intros E'. + + apply andb_true_intro; split. + * eapply E; eauto. apply InA_cons; now left. + * apply IH; clear IH; trivial. + destruct E as (E1,E2). split. + { intros x. clear E2. + split; intros; SortLt. + specialize (E1 x); rewrite 2 In_cons in E1; simpl in E1. + destruct E1 as ([E1|E1],_); eauto. MX.order. + specialize (E1 x); rewrite 2 In_cons in E1; simpl in E1. + destruct E1 as (_,[E1|E1]); eauto. MX.order. } + { intros x xe xe' Hx HX'. eapply E2; eauto. } + + assert (IN : In k ((k',e')::m')). + { apply E. apply In_cons; now left. } + apply In_cons in IN. simpl in IN. destruct IN as [?|IN]. MX.order. + SortLt. MX.order. + + assert (IN : In k' ((k,e)::m)). + { apply E. apply In_cons; now left. } + apply In_cons in IN. simpl in IN. destruct IN as [?|IN]. MX.order. + SortLt. MX.order. +Qed. + +Lemma equal_2 m (Hm:Sort m) m' (Hm':Sort m') cmp : + equal cmp m m' = true -> Equivb cmp m m'. +Proof. + revert m' Hm'. + induction m as [|(k,e) m IH]; destruct m' as [|(k',e') m']; simpl; + try discriminate. + - split. reflexivity. inversion 1. + - intros Hm'. case X.compare_spec; try discriminate. + rewrite andb_true_iff. intros E (C,EQ). + inversion_clear Hm; inversion_clear Hm'. + apply IH in EQ; trivial. + destruct EQ as (E1,E2). + split. + + intros x. rewrite 2 In_cons; simpl. rewrite <- E1. + intuition; now left; MX.order. + + intros x ex ex'. unfold MapsTo in *. rewrite 2 InA_cons, 2 eqke_def. + intuition; subst. + * trivial. + * SortLt. MX.order. + * SortLt. MX.order. + * eapply E2; eauto. +Qed. + +Lemma equal_spec m (Hm:Sort m) m' (Hm':Sort m') cmp : + equal cmp m m' = true <-> Equivb cmp m m'. +Proof. + split. now apply equal_2. now apply equal_1. +Qed. + +(** This lemma isn't part of the spec of [Equivb], but is used in [MMapAVL] *) + +Lemma equal_cons : forall cmp l1 l2 x y, Sort (x::l1) -> Sort (y::l2) -> + eqk x y -> cmp (snd x) (snd y) = true -> + (Equivb cmp l1 l2 <-> Equivb cmp (x :: l1) (y :: l2)). +Proof. + intros. + inversion H; subst. + inversion H0; subst. + destruct x; destruct y; compute in H1, H2. + split; intros. + apply equal_2; auto. + simpl. + case X.compare_spec; intros; try MX.order. + rewrite H2; simpl. + apply equal_1; auto. + apply equal_2; auto. + generalize (equal_1 H H0 H3). + simpl. + case X.compare_spec; try discriminate. + rewrite andb_true_iff. intuition. +Qed. + +Variable elt':Type. + +(** * [map] and [mapi] *) + +Fixpoint map (f:elt -> elt') (m:t elt) : t elt' := + match m with + | nil => nil + | (k,e)::m' => (k,f e) :: map f m' + end. + +Fixpoint mapi (f: key -> elt -> elt') (m:t elt) : t elt' := + match m with + | nil => nil + | (k,e)::m' => (k,f k e) :: mapi f m' + end. + +End Elt. +Arguments find {elt} k m. +Section Elt2. +Variable elt elt' : Type. + +(** Specification of [map] *) + +Lemma map_spec (f:elt->elt') m x : + find x (map f m) = option_map f (find x m). +Proof. + induction m as [|(k,e) m IH]; simpl; trivial. + now case X.compare_spec. +Qed. + +Lemma map_Inf (f:elt->elt') m x e e' : + Inf (x,e) m -> Inf (x,e') (map f m). +Proof. + induction m as [|(x0,e0) m IH]; simpl; auto. + inversion_clear 1; auto. +Qed. +Hint Resolve map_Inf. + +Lemma map_sorted (f:elt->elt')(m: t elt)(Hm : Sort m) : + Sort (map f m). +Proof. + induction m as [|(x,e) m IH]; simpl; auto. + inversion_clear Hm. constructor; eauto. +Qed. + +(** Specification of [mapi] *) + +Lemma mapi_spec (f:key->elt->elt') m x : + exists y, X.eq y x /\ find x (mapi f m) = option_map (f y) (find x m). +Proof. + induction m as [|(k,e) m IH]; simpl. + - now exists x. + - elim X.compare_spec; intros; simpl. + + now exists k. + + now exists x. + + apply IH. +Qed. + +Lemma mapi_Inf (f:key->elt->elt') m x e : + Inf (x,e) m -> Inf (x,f x e) (mapi f m). +Proof. + induction m as [|(x0,e0) m IH]; simpl; auto. + inversion_clear 1; auto. +Qed. +Hint Resolve mapi_Inf. + +Lemma mapi_sorted (f:key->elt->elt') m (Hm : Sort m) : + Sort (mapi f m). +Proof. + induction m as [|(x,e) m IH]; simpl; auto. + inversion_clear Hm; auto. +Qed. + +End Elt2. +Section Elt3. + +(** * [merge] *) + +Variable elt elt' elt'' : Type. +Variable f : key -> option elt -> option elt' -> option elt''. + +Definition option_cons {A}(k:key)(o:option A)(l:list (key*A)) := + match o with + | Some e => (k,e)::l + | None => l + end. + +Fixpoint merge_l (m : t elt) : t elt'' := + match m with + | nil => nil + | (k,e)::l => option_cons k (f k (Some e) None) (merge_l l) + end. + +Fixpoint merge_r (m' : t elt') : t elt'' := + match m' with + | nil => nil + | (k,e')::l' => option_cons k (f k None (Some e')) (merge_r l') + end. + +Fixpoint merge (m : t elt) : t elt' -> t elt'' := + match m with + | nil => merge_r + | (k,e) :: l => + fix merge_aux (m' : t elt') : t elt'' := + match m' with + | nil => merge_l m + | (k',e') :: l' => + match X.compare k k' with + | Lt => option_cons k (f k (Some e) None) (merge l m') + | Eq => option_cons k (f k (Some e) (Some e')) (merge l l') + | Gt => option_cons k' (f k' None (Some e')) (merge_aux l') + end + end + end. + +Notation oee' := (option elt * option elt')%type. + +Fixpoint combine (m : t elt) : t elt' -> t oee' := + match m with + | nil => map (fun e' => (None,Some e')) + | (k,e) :: l => + fix combine_aux (m':t elt') : list (key * oee') := + match m' with + | nil => map (fun e => (Some e,None)) m + | (k',e') :: l' => + match X.compare k k' with + | Lt => (k,(Some e, None))::combine l m' + | Eq => (k,(Some e, Some e'))::combine l l' + | Gt => (k',(None,Some e'))::combine_aux l' + end + end + end. + +Definition fold_right_pair {A B C}(f: A->B->C->C)(l:list (A*B))(i:C) := + List.fold_right (fun p => f (fst p) (snd p)) i l. + +Definition merge' m m' := + let m0 : t oee' := combine m m' in + let m1 : t (option elt'') := mapi (fun k p => f k (fst p) (snd p)) m0 in + fold_right_pair (option_cons (A:=elt'')) m1 nil. + +Lemma merge_equiv : forall m m', merge' m m' = merge m m'. +Proof. + unfold merge'. + induction m as [|(k,e) m IHm]; intros. + - (* merge_r *) + simpl. + induction m' as [|(k',e') m' IHm']; simpl; rewrite ?IHm'; auto. + - induction m' as [|(k',e') m' IHm']; simpl. + + f_equal. + (* merge_l *) + clear k e IHm. + induction m as [|(k,e) m IHm]; simpl; rewrite ?IHm; auto. + + elim X.compare_spec; intros; simpl; f_equal. + * apply IHm. + * apply IHm. + * apply IHm'. +Qed. + +Lemma combine_Inf : + forall m m' (x:key)(e:elt)(e':elt')(e'':oee'), + Inf (x,e) m -> + Inf (x,e') m' -> + Inf (x,e'') (combine m m'). +Proof. + induction m. + - intros. simpl. eapply map_Inf; eauto. + - induction m'; intros. + + destruct a. + replace (combine ((t0, e0) :: m) nil) with + (map (fun e => (Some e,None (A:=elt'))) ((t0,e0)::m)); auto. + eapply map_Inf; eauto. + + simpl. + destruct a as (k,e0); destruct a0 as (k',e0'). + elim X.compare_spec. + * inversion_clear H; auto. + * inversion_clear H; auto. + * inversion_clear H0; auto. +Qed. +Hint Resolve combine_Inf. + +Lemma combine_sorted m (Hm : Sort m) m' (Hm' : Sort m') : + Sort (combine m m'). +Proof. + revert m' Hm'. + induction m. + - intros; clear Hm. simpl. apply map_sorted; auto. + - induction m'; intros. + + clear Hm'. + destruct a. + replace (combine ((t0, e) :: m) nil) with + (map (fun e => (Some e,None (A:=elt'))) ((t0,e)::m)); auto. + apply map_sorted; auto. + + simpl. + destruct a as (k,e); destruct a0 as (k',e'). + inversion_clear Hm; inversion_clear Hm'. + case X.compare_spec; [intros Heq| intros Hlt| intros Hlt]; + constructor; auto. + * assert (Inf (k, e') m') by (apply Inf_eq with (k',e'); auto). + exact (combine_Inf _ H0 H3). + * assert (Inf (k, e') ((k',e')::m')) by auto. + exact (combine_Inf _ H0 H3). + * assert (Inf (k', e) ((k,e)::m)) by auto. + exact (combine_Inf _ H3 H2). +Qed. + +Lemma merge_sorted m (Hm : Sort m) m' (Hm' : Sort m') : + Sort (merge m m'). +Proof. + intros. + rewrite <- merge_equiv. + unfold merge'. + assert (Hmm':=combine_sorted Hm Hm'). + set (l0:=combine m m') in *; clearbody l0. + set (f':= fun k p => f k (fst p) (snd p)). + assert (H1:=mapi_sorted f' Hmm'). + set (l1:=mapi f' l0) in *; clearbody l1. + clear f' f Hmm' l0 Hm Hm' m m'. + (* Sort fold_right_pair *) + induction l1. + - simpl; auto. + - inversion_clear H1. + destruct a; destruct o; auto. + simpl. + constructor; auto. + clear IHl1. + (* Inf fold_right_pair *) + induction l1. + + simpl; auto. + + destruct a; destruct o; simpl; auto. + * inversion_clear H0; auto. + * inversion_clear H0. inversion_clear H. + compute in H1. + apply IHl1; auto. + apply Inf_lt with (t1, None); auto. +Qed. + +Definition at_least_one (o:option elt)(o':option elt') := + match o, o' with + | None, None => None + | _, _ => Some (o,o') + end. + +Lemma combine_spec m (Hm : Sort m) m' (Hm' : Sort m') (x:key) : + find x (combine m m') = at_least_one (find x m) (find x m'). +Proof. + revert m' Hm'. + induction m. + intros. + simpl. + induction m'. + intros; simpl; auto. + simpl; destruct a. + simpl; destruct (X.compare x t0); simpl; auto. + inversion_clear Hm'; auto. + induction m'. + (* m' = nil *) + intros; destruct a; simpl. + destruct (X.compare_spec x t0) as [ |Hlt|Hlt]; simpl; auto. + inversion_clear Hm; clear H0 Hlt Hm' IHm t0. + induction m; simpl; auto. + inversion_clear H. + destruct a. + simpl; destruct (X.compare x t0); simpl; auto. + (* m' <> nil *) + intros. + destruct a as (k,e); destruct a0 as (k',e'); simpl. + inversion Hm; inversion Hm'; subst. + destruct (X.compare_spec k k'); simpl; + destruct (X.compare_spec x k); + MX.order || destruct (X.compare_spec x k'); + simpl; try MX.order; auto. + - rewrite IHm; auto; simpl. elim X.compare_spec; auto; MX.order. + - rewrite IHm; auto; simpl. elim X.compare_spec; auto; MX.order. + - rewrite IHm; auto; simpl. elim X.compare_spec; auto; MX.order. + - change (find x (combine ((k, e) :: m) m') = Some (Some e, find x m')). + rewrite IHm'; auto; simpl. elim X.compare_spec; auto; MX.order. + - change (find x (combine ((k, e) :: m) m') = at_least_one None (find x m')). + rewrite IHm'; auto; simpl. elim X.compare_spec; auto; MX.order. + - change (find x (combine ((k, e) :: m) m') = + at_least_one (find x m) (find x m')). + rewrite IHm'; auto; simpl. elim X.compare_spec; auto; MX.order. +Qed. + +Definition at_least_one_then_f k (o:option elt)(o':option elt') := + match o, o' with + | None, None => None + | _, _ => f k o o' + end. + +Lemma merge_spec0 m (Hm : Sort m) m' (Hm' : Sort m') (x:key) : + exists y, X.eq y x /\ + find x (merge m m') = at_least_one_then_f y (find x m) (find x m'). +Proof. + intros. + rewrite <- merge_equiv. + unfold merge'. + assert (H:=combine_spec Hm Hm' x). + assert (H2:=combine_sorted Hm Hm'). + set (f':= fun k p => f k (fst p) (snd p)). + set (m0 := combine m m') in *; clearbody m0. + set (o:=find x m) in *; clearbody o. + set (o':=find x m') in *; clearbody o'. + clear Hm Hm' m m'. revert H. + match goal with |- ?G => + assert (G/\(find x m0 = None -> + find x (fold_right_pair option_cons (mapi f' m0) nil) = None)); + [|intuition] end. + induction m0; simpl in *; intuition. + - exists x; split; [easy|]. + destruct o; destruct o'; simpl in *; try discriminate; auto. + - destruct a as (k,(oo,oo')); simpl in *. + inversion_clear H2. + destruct (X.compare_spec x k) as [Heq|Hlt|Hlt]; simpl in *. + + (* x = k *) + exists k; split; [easy|]. + assert (at_least_one_then_f k o o' = f k oo oo'). + { destruct o; destruct o'; simpl in *; inversion_clear H; auto. } + rewrite H2. + unfold f'; simpl. + destruct (f k oo oo'); simpl. + * elim X.compare_spec; trivial; try MX.order. + * destruct (IHm0 H0) as (_,H4); apply H4; auto. + case_eq (find x m0); intros; auto. + assert (eqk (elt:=oee') (k,(oo,oo')) (x,(oo,oo'))). + now compute. + symmetry in H5. + destruct (Sort_Inf_NotIn H0 (Inf_eq H5 H1)). + exists p; apply find_spec; auto. + + (* x < k *) + destruct (f' k (oo,oo')); simpl. + * elim X.compare_spec; trivial; try MX.order. + destruct o; destruct o'; simpl in *; try discriminate; auto. + now exists x. + * apply IHm0; trivial. + rewrite <- H. + case_eq (find x m0); intros; auto. + assert (ltk (elt:=oee') (x,(oo,oo')) (k,(oo,oo'))). + red; auto. + destruct (Sort_Inf_NotIn H0 (Inf_lt H3 H1)). + exists p; apply find_spec; auto. + + (* k < x *) + unfold f'; simpl. + destruct (f k oo oo'); simpl. + * elim X.compare_spec; trivial; try MX.order. + intros. apply IHm0; auto. + * apply IHm0; auto. + + - (* None -> None *) + destruct a as (k,(oo,oo')). + simpl. + inversion_clear H2. + destruct (X.compare_spec x k) as [Hlt|Heq|Hlt]; try discriminate. + + (* x < k *) + unfold f'; simpl. + destruct (f k oo oo'); simpl. + elim X.compare_spec; trivial; try MX.order. intros. + apply IHm0; auto. + case_eq (find x m0); intros; auto. + assert (ltk (elt:=oee') (x,(oo,oo')) (k,(oo,oo'))). + now compute. + destruct (Sort_Inf_NotIn H0 (Inf_lt H3 H1)). + exists p; apply find_spec; auto. + + (* k < x *) + unfold f'; simpl. + destruct (f k oo oo'); simpl. + elim X.compare_spec; trivial; try MX.order. intros. + apply IHm0; auto. + apply IHm0; auto. +Qed. + +(** Specification of [merge] *) + +Lemma merge_spec1 m (Hm : Sort m) m' (Hm' : Sort m')(x:key) : + In x m \/ In x m' -> + exists y, X.eq y x /\ + find x (merge m m') = f y (find x m) (find x m'). +Proof. + intros. + destruct (merge_spec0 Hm Hm' x) as (y,(Hy,H')). + exists y; split; [easy|]. rewrite H'. + destruct H as [(e,H)|(e,H)]; + apply find_spec in H; trivial; rewrite H; simpl; auto. + now destruct (find x m). +Qed. + +Lemma merge_spec2 m (Hm : Sort m) m' (Hm' : Sort m')(x:key) : + In x (merge m m') -> In x m \/ In x m'. +Proof. + intros. + destruct H as (e,H). + apply find_spec in H; auto using merge_sorted. + destruct (merge_spec0 Hm Hm' x) as (y,(Hy,H')). + rewrite H in H'. + destruct (find x m) eqn:F. + - apply find_spec in F; eauto. + - destruct (find x m') eqn:F'. + + apply find_spec in F'; eauto. + + simpl in H'. discriminate. +Qed. + +End Elt3. +End Raw. + +Module Make (X: OrderedType) <: S with Module E := X. +Module Raw := Raw X. +Module E := X. + +Definition key := E.t. +Definition eq_key {elt} := @Raw.PX.eqk elt. +Definition eq_key_elt {elt} := @Raw.PX.eqke elt. +Definition lt_key {elt} := @Raw.PX.ltk elt. + +Record t_ (elt:Type) := Mk + {this :> Raw.t elt; + sorted : sort Raw.PX.ltk this}. +Definition t := t_. + +Definition empty {elt} := Mk (Raw.empty_sorted elt). + +Section Elt. + Variable elt elt' elt'':Type. + + Implicit Types m : t elt. + Implicit Types x y : key. + Implicit Types e : elt. + + Definition is_empty m : bool := Raw.is_empty m.(this). + Definition add x e m : t elt := Mk (Raw.add_sorted m.(sorted) x e). + Definition find x m : option elt := Raw.find x m.(this). + Definition remove x m : t elt := Mk (Raw.remove_sorted m.(sorted) x). + Definition mem x m : bool := Raw.mem x m.(this). + Definition map f m : t elt' := Mk (Raw.map_sorted f m.(sorted)). + Definition mapi (f:key->elt->elt') m : t elt' := + Mk (Raw.mapi_sorted f m.(sorted)). + Definition merge f m (m':t elt') : t elt'' := + Mk (Raw.merge_sorted f m.(sorted) m'.(sorted)). + Definition bindings m : list (key*elt) := Raw.bindings m.(this). + Definition cardinal m := length m.(this). + Definition fold {A:Type}(f:key->elt->A->A) m (i:A) : A := + Raw.fold f m.(this) i. + Definition equal cmp m m' : bool := Raw.equal cmp m.(this) m'.(this). + + Definition MapsTo x e m : Prop := Raw.PX.MapsTo x e m.(this). + Definition In x m : Prop := Raw.PX.In x m.(this). + + 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 m m' : Prop := @Raw.Equivb elt cmp m.(this) m'.(this). + + Instance MapsTo_compat : + Proper (E.eq==>Logic.eq==>Logic.eq==>iff) MapsTo. + Proof. + intros x x' Hx e e' <- m m' <-. unfold MapsTo. now rewrite Hx. + Qed. + + Lemma find_spec m : forall x e, find x m = Some e <-> MapsTo x e m. + Proof. exact (Raw.find_spec m.(sorted)). Qed. + + Lemma mem_spec m : forall x, mem x m = true <-> In x m. + Proof. exact (Raw.mem_spec m.(sorted)). Qed. + + Lemma empty_spec : forall x, find x empty = None. + Proof. exact (Raw.empty_spec _). Qed. + + Lemma is_empty_spec m : is_empty m = true <-> (forall x, find x m = None). + Proof. exact (Raw.is_empty_spec m.(this)). Qed. + + Lemma add_spec1 m : forall x e, find x (add x e m) = Some e. + Proof. exact (Raw.add_spec1 m.(this)). Qed. + Lemma add_spec2 m : forall x y e, ~E.eq x y -> find y (add x e m) = find y m. + Proof. exact (Raw.add_spec2 m.(this)). Qed. + + Lemma remove_spec1 m : forall x, find x (remove x m) = None. + Proof. exact (Raw.remove_spec1 m.(sorted)). Qed. + Lemma remove_spec2 m : forall x y, ~E.eq x y -> find y (remove x m) = find y m. + Proof. exact (Raw.remove_spec2 m.(sorted)). Qed. + + Lemma bindings_spec1 m : forall x e, + InA eq_key_elt (x,e) (bindings m) <-> MapsTo x e m. + Proof. exact (Raw.bindings_spec1 m.(this)). Qed. + Lemma bindings_spec2w m : NoDupA eq_key (bindings m). + Proof. exact (Raw.bindings_spec2w m.(sorted)). Qed. + Lemma bindings_spec2 m : sort lt_key (bindings m). + Proof. exact (Raw.bindings_spec2 m.(sorted)). Qed. + + Lemma cardinal_spec m : cardinal m = length (bindings m). + Proof. reflexivity. Qed. + + Lemma fold_spec m : forall (A : Type) (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. exact (Raw.fold_spec m.(this)). Qed. + + Lemma equal_spec m m' : forall cmp, equal cmp m m' = true <-> Equivb cmp m m'. + Proof. exact (Raw.equal_spec m.(sorted) m'.(sorted)). Qed. + +End Elt. + + Lemma map_spec {elt elt'} (f:elt->elt') m : + forall x, find x (map f m) = option_map f (find x m). + Proof. exact (Raw.map_spec f m.(this)). Qed. + + Lemma mapi_spec {elt elt'} (f:key->elt->elt') m : + forall x, exists y, + E.eq y x /\ find x (mapi f m) = option_map (f y) (find x m). + Proof. exact (Raw.mapi_spec f m.(this)). Qed. + + Lemma merge_spec1 {elt elt' elt''} + (f:key->option elt->option elt'->option elt'') m m' : + forall x, + In x m \/ In x m' -> + exists y, E.eq y x /\ find x (merge f m m') = f y (find x m) (find x m'). + Proof. exact (Raw.merge_spec1 f m.(sorted) m'.(sorted)). Qed. + + Lemma merge_spec2 {elt elt' elt''} + (f:key->option elt->option elt'->option elt'') m m' : + forall x, + In x (merge f m m') -> In x m \/ In x m'. + Proof. exact (Raw.merge_spec2 m.(sorted) m'.(sorted)). Qed. + +End Make. + +Module Make_ord (X: OrderedType)(D : OrderedType) <: +Sord with Module Data := D + with Module MapS.E := X. + +Module Data := D. +Module MapS := Make(X). +Import MapS. + +Module MD := OrderedTypeFacts(D). +Import MD. + +Definition t := MapS.t D.t. + +Definition cmp e e' := + match D.compare e e' with Eq => true | _ => false end. + +Fixpoint eq_list (m m' : list (X.t * D.t)) : Prop := + match m, m' with + | nil, nil => True + | (x,e)::l, (x',e')::l' => + match X.compare x x' with + | Eq => D.eq e e' /\ eq_list l l' + | _ => False + end + | _, _ => False + end. + +Definition eq m m' := eq_list m.(this) m'.(this). + +Fixpoint lt_list (m m' : list (X.t * D.t)) : Prop := + match m, m' with + | nil, nil => False + | nil, _ => True + | _, nil => False + | (x,e)::l, (x',e')::l' => + match X.compare x x' with + | Lt => True + | Gt => False + | Eq => D.lt e e' \/ (D.eq e e' /\ lt_list l l') + end + end. + +Definition lt m m' := lt_list m.(this) m'.(this). + +Lemma eq_equal : forall m m', eq m m' <-> equal cmp m m' = true. +Proof. + intros (l,Hl); induction l. + intros (l',Hl'); unfold eq; simpl. + destruct l'; unfold equal; simpl; intuition. + intros (l',Hl'); unfold eq. + destruct l'. + destruct a; unfold equal; simpl; intuition. + destruct a as (x,e). + destruct p as (x',e'). + unfold equal; simpl. + destruct (X.compare_spec x x') as [Hlt|Heq|Hlt]; simpl; intuition. + unfold cmp at 1. + elim D.compare_spec; try MD.order; simpl. + inversion_clear Hl. + inversion_clear Hl'. + destruct (IHl H (Mk H3)). + unfold equal, eq in H5; simpl in H5; auto. + destruct (andb_prop _ _ H); clear H. + generalize H0; unfold cmp. + elim D.compare_spec; try MD.order; simpl; try discriminate. + destruct (andb_prop _ _ H); clear H. + inversion_clear Hl. + inversion_clear Hl'. + destruct (IHl H (Mk H3)). + unfold equal, eq in H6; simpl in H6; auto. +Qed. + +Lemma eq_spec m m' : eq m m' <-> Equivb cmp m m'. +Proof. + now rewrite eq_equal, equal_spec. +Qed. + +Lemma eq_refl : forall m : t, eq m m. +Proof. + intros (m,Hm); induction m; unfold eq; simpl; auto. + destruct a. + destruct (X.compare_spec t0 t0) as [Hlt|Heq|Hlt]; auto. + - split. reflexivity. inversion_clear Hm. apply (IHm H). + - MapS.Raw.MX.order. + - MapS.Raw.MX.order. +Qed. + +Lemma eq_sym : forall m1 m2 : t, eq m1 m2 -> eq m2 m1. +Proof. + intros (m,Hm); induction m; + intros (m', Hm'); destruct m'; unfold eq; simpl; + try destruct a as (x,e); try destruct p as (x',e'); auto. + destruct (X.compare_spec x x') as [Hlt|Heq|Hlt]; + elim X.compare_spec; try MapS.Raw.MX.order; intuition. + inversion_clear Hm; inversion_clear Hm'. + apply (IHm H0 (Mk H4)); auto. +Qed. + +Lemma eq_trans : forall m1 m2 m3 : t, eq m1 m2 -> eq m2 m3 -> eq m1 m3. +Proof. + intros (m1,Hm1); induction m1; + intros (m2, Hm2); destruct m2; + intros (m3, Hm3); destruct m3; unfold eq; simpl; + try destruct a as (x,e); + try destruct p as (x',e'); + try destruct p0 as (x'',e''); try contradiction; auto. + destruct (X.compare_spec x x') as [Hlt|Heq|Hlt]; + destruct (X.compare_spec x' x'') as [Hlt'|Heq'|Hlt']; + elim X.compare_spec; try MapS.Raw.MX.order; intuition. + now transitivity e'. + inversion_clear Hm1; inversion_clear Hm2; inversion_clear Hm3. + apply (IHm1 H1 (Mk H6) (Mk H8)); intuition. +Qed. + +Instance eq_equiv : Equivalence eq. +Proof. split; [exact eq_refl|exact eq_sym|exact eq_trans]. Qed. + +Lemma lt_trans : forall m1 m2 m3 : t, lt m1 m2 -> lt m2 m3 -> lt m1 m3. +Proof. + intros (m1,Hm1); induction m1; + intros (m2, Hm2); destruct m2; + intros (m3, Hm3); destruct m3; unfold lt; simpl; + try destruct a as (x,e); + try destruct p as (x',e'); + try destruct p0 as (x'',e''); try contradiction; auto. + destruct (X.compare_spec x x') as [Hlt|Heq|Hlt]; + destruct (X.compare_spec x' x'') as [Hlt'|Heq'|Hlt']; + elim X.compare_spec; try MapS.Raw.MX.order; intuition. + left; transitivity e'; auto. + left; MD.order. + left; MD.order. + right. + split. + transitivity e'; auto. + inversion_clear Hm1; inversion_clear Hm2; inversion_clear Hm3. + apply (IHm1 H2 (Mk H6) (Mk H8)); intuition. +Qed. + +Lemma lt_irrefl : forall m, ~ lt m m. +Proof. + intros (m,Hm); induction m; unfold lt; simpl; auto. + destruct a. + destruct (X.compare_spec t0 t0) as [Hlt|Heq|Hlt]; auto. + - intuition. MD.order. inversion_clear Hm. now apply (IHm H0). + - MapS.Raw.MX.order. +Qed. + +Instance lt_strorder : StrictOrder lt. +Proof. split; [exact lt_irrefl|exact lt_trans]. Qed. + +Lemma lt_compat1 : forall m1 m1' m2, eq m1 m1' -> lt m1 m2 -> lt m1' m2. +Proof. + intros (m1,Hm1); induction m1; + intros (m1',Hm1'); destruct m1'; + intros (m2,Hm2); destruct m2; unfold eq, lt; + try destruct a as (x,e); + try destruct p as (x',e'); + try destruct p0 as (x'',e''); try contradiction; simpl; auto. + destruct (X.compare_spec x x') as [Hlt|Heq|Hlt]; + destruct (X.compare_spec x' x'') as [Hlt'|Heq'|Hlt']; + elim X.compare_spec; try MapS.Raw.MX.order; intuition. + left; MD.order. + right. + split. + MD.order. + inversion_clear Hm1; inversion_clear Hm1'; inversion_clear Hm2. + apply (IHm1 H0 (Mk H6) (Mk H8)); intuition. +Qed. + +Lemma lt_compat2 : forall m1 m2 m2', eq m2 m2' -> lt m1 m2 -> lt m1 m2'. +Proof. + intros (m1,Hm1); induction m1; + intros (m2,Hm2); destruct m2; + intros (m2',Hm2'); destruct m2'; unfold eq, lt; + try destruct a as (x,e); + try destruct p as (x',e'); + try destruct p0 as (x'',e''); try contradiction; simpl; auto. + destruct (X.compare_spec x x') as [Hlt|Heq|Hlt]; + destruct (X.compare_spec x' x'') as [Hlt'|Heq'|Hlt']; + elim X.compare_spec; try MapS.Raw.MX.order; intuition. + left; MD.order. + right. + split. + MD.order. + inversion_clear Hm1; inversion_clear Hm2; inversion_clear Hm2'. + apply (IHm1 H0 (Mk H6) (Mk H8)); intuition. +Qed. + +Instance lt_compat : Proper (eq==>eq==>iff) lt. +Proof. + intros m1 m1' H1 m2 m2' H2. split; intros. + now apply (lt_compat2 H2), (lt_compat1 H1). + symmetry in H1, H2. + now apply (lt_compat2 H2), (lt_compat1 H1). +Qed. + +Ltac cmp_solve := + unfold eq, lt; simpl; elim X.compare_spec; try Raw.MX.order; auto. + +Fixpoint compare_list m1 m2 := match m1, m2 with +| nil, nil => Eq +| nil, _ => Lt +| _, nil => Gt +| (k1,e1)::m1, (k2,e2)::m2 => + match X.compare k1 k2 with + | Lt => Lt + | Gt => Gt + | Eq => match D.compare e1 e2 with + | Lt => Lt + | Gt => Gt + | Eq => compare_list m1 m2 + end + end +end. + +Definition compare m1 m2 := compare_list m1.(this) m2.(this). + +Lemma compare_spec : forall m1 m2, CompSpec eq lt m1 m2 (compare m1 m2). +Proof. + unfold CompSpec. + intros (m1,Hm1)(m2,Hm2). unfold compare, eq, lt; simpl. + revert m2 Hm2. + induction m1 as [|(k1,e1) m1 IH1]; destruct m2 as [|(k2,e2) m2]; + try constructor; simpl; intros; auto. + elim X.compare_spec; simpl; try constructor; auto; intros. + elim D.compare_spec; simpl; try constructor; auto; intros. + inversion_clear Hm1; inversion_clear Hm2. + destruct (IH1 H1 _ H3); simpl; try constructor; auto. + elim X.compare_spec; try Raw.MX.order. right. now split. + elim X.compare_spec; try Raw.MX.order. now left. + elim X.compare_spec; try Raw.MX.order; auto. +Qed. + +End Make_ord. diff --git a/theories/MMaps/MMapPositive.v b/theories/MMaps/MMapPositive.v new file mode 100644 index 00000000..d3aab238 --- /dev/null +++ b/theories/MMaps/MMapPositive.v @@ -0,0 +1,698 @@ +(***********************************************************************) +(* 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 *) +(***********************************************************************) + +(** * MMapPositive : an implementation of MMapInterface for [positive] keys. *) + +Require Import Bool PeanoNat BinPos Orders OrdersEx OrdersLists MMapInterface. + +Set Implicit Arguments. +Local Open Scope lazy_bool_scope. +Local Open Scope positive_scope. +Local Unset Elimination Schemes. + +(** This file is an adaptation to the [MMap] framework of a work by + Xavier Leroy and Sandrine Blazy (used for building certified compilers). + Keys are of type [positive], and maps are binary trees: the sequence + of binary digits of a positive number corresponds to a path in such a tree. + This is quite similar to the [IntMap] library, except that no path + compression is implemented, and that the current file is simple enough to be + self-contained. *) + +(** Reverses the positive [y] and concatenate it with [x] *) + +Fixpoint rev_append (y x : positive) : positive := + match y with + | 1 => x + | y~1 => rev_append y x~1 + | y~0 => rev_append y x~0 + end. +Local Infix "@" := rev_append (at level 60). +Definition rev x := x@1. + +(** The module of maps over positive keys *) + +Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. + + Module E:=PositiveOrderedTypeBits. + Module ME:=KeyOrderedType E. + + Definition key := positive : Type. + + Definition eq_key {A} (p p':key*A) := E.eq (fst p) (fst p'). + + Definition eq_key_elt {A} (p p':key*A) := + E.eq (fst p) (fst p') /\ (snd p) = (snd p'). + + Definition lt_key {A} (p p':key*A) := E.lt (fst p) (fst p'). + + Instance eqk_equiv {A} : Equivalence (@eq_key A) := _. + Instance eqke_equiv {A} : Equivalence (@eq_key_elt A) := _. + Instance ltk_strorder {A} : StrictOrder (@lt_key A) := _. + + Inductive tree (A : Type) := + | Leaf : tree A + | Node : tree A -> option A -> tree A -> tree A. + + Arguments Leaf {A}. + + Scheme tree_ind := Induction for tree Sort Prop. + + Definition t := tree. + + Definition empty {A} : t A := Leaf. + + Section A. + Variable A:Type. + + Fixpoint is_empty (m : t A) : bool := + match m with + | Leaf => true + | Node l None r => (is_empty l) &&& (is_empty r) + | _ => false + end. + + Fixpoint find (i : key) (m : t A) : option A := + match m with + | Leaf => None + | Node l o r => + match i with + | xH => o + | xO ii => find ii l + | xI ii => find ii r + end + end. + + Fixpoint mem (i : key) (m : t A) : bool := + match m with + | Leaf => false + | Node l o r => + match i with + | xH => match o with None => false | _ => true end + | xO ii => mem ii l + | xI ii => mem ii r + end + end. + + Fixpoint add (i : key) (v : A) (m : t A) : t A := + match m with + | Leaf => + match i with + | xH => Node Leaf (Some v) Leaf + | xO ii => Node (add ii v Leaf) None Leaf + | xI ii => Node Leaf None (add ii v Leaf) + end + | Node l o r => + match i with + | xH => Node l (Some v) r + | xO ii => Node (add ii v l) o r + | xI ii => Node l o (add ii v r) + end + end. + + (** helper function to avoid creating empty trees that are not leaves *) + + Definition node (l : t A) (o: option A) (r : t A) : t A := + match o,l,r with + | None,Leaf,Leaf => Leaf + | _,_,_ => Node l o r + end. + + Fixpoint remove (i : key) (m : t A) : t A := + match m with + | Leaf => Leaf + | Node l o r => + match i with + | xH => node l None r + | xO ii => node (remove ii l) o r + | xI ii => node l o (remove ii r) + end + end. + + (** [bindings] *) + + Fixpoint xbindings (m : t A) (i : positive) (a: list (key*A)) := + match m with + | Leaf => a + | Node l None r => xbindings l i~0 (xbindings r i~1 a) + | Node l (Some e) r => xbindings l i~0 ((rev i,e) :: xbindings r i~1 a) + end. + + Definition bindings (m : t A) := xbindings m 1 nil. + + (** [cardinal] *) + + Fixpoint cardinal (m : t A) : nat := + match m with + | Leaf => 0%nat + | Node l None r => (cardinal l + cardinal r)%nat + | Node l (Some _) r => S (cardinal l + cardinal r) + end. + + (** Specification proofs *) + + Definition MapsTo (i:key)(v:A)(m:t A) := find i m = Some v. + Definition In (i:key)(m:t A) := exists e:A, MapsTo i e m. + + Lemma MapsTo_compat : Proper (E.eq==>eq==>eq==>iff) MapsTo. + Proof. + intros k k' Hk e e' He m m' Hm. red in Hk. now subst. + Qed. + + Lemma find_spec m x e : find x m = Some e <-> MapsTo x e m. + Proof. reflexivity. Qed. + + Lemma mem_find : + forall m x, mem x m = match find x m with None => false | _ => true end. + Proof. + induction m; destruct x; simpl; auto. + Qed. + + Lemma mem_spec : forall m x, mem x m = true <-> In x m. + Proof. + unfold In, MapsTo; intros m x; rewrite mem_find. + split. + - destruct (find x m). + exists a; auto. + intros; discriminate. + - destruct 1 as (e0,H0); rewrite H0; auto. + Qed. + + Lemma gleaf : forall (i : key), find i Leaf = None. + Proof. destruct i; simpl; auto. Qed. + + Theorem empty_spec: + forall (i: key), find i empty = None. + Proof. exact gleaf. Qed. + + Lemma is_empty_spec m : + is_empty m = true <-> forall k, find k m = None. + Proof. + induction m; simpl. + - intuition. apply empty_spec. + - destruct o. split; try discriminate. + intros H. now specialize (H xH). + rewrite <- andb_lazy_alt, andb_true_iff, IHm1, IHm2. + clear IHm1 IHm2. + split. + + intros (H1,H2) k. destruct k; simpl; auto. + + intros H; split; intros k. apply (H (xO k)). apply (H (xI k)). + Qed. + + Theorem add_spec1: + forall (m: t A) (i: key) (x: A), find i (add i x m) = Some x. + Proof. + intros m i; revert m. + induction i; destruct m; simpl; auto. + Qed. + + Theorem add_spec2: + forall (m: t A) (i j: key) (x: A), + i <> j -> find j (add i x m) = find j m. + Proof. + intros m i j; revert m i. + induction j; destruct i, m; simpl; intros; + rewrite ?IHj, ?gleaf; auto; try congruence. + Qed. + + Lemma rleaf : forall (i : key), remove i Leaf = Leaf. + Proof. destruct i; simpl; auto. Qed. + + Lemma gnode l o r i : find i (node l o r) = find i (Node l o r). + Proof. + destruct o,l,r; simpl; trivial. + destruct i; simpl; now rewrite ?gleaf. + Qed. + + Opaque node. + + Theorem remove_spec1: + forall (m: t A)(i: key), find i (remove i m) = None. + Proof. + induction m; simpl. + - intros; rewrite rleaf. apply gleaf. + - destruct i; simpl remove; rewrite gnode; simpl; auto. + Qed. + + Theorem remove_spec2: + forall (m: t A)(i j: key), + i <> j -> find j (remove i m) = find j m. + Proof. + induction m; simpl; intros. + - now rewrite rleaf. + - destruct i; simpl; rewrite gnode; destruct j; simpl; trivial; + try apply IHm1; try apply IHm2; congruence. + Qed. + + Local Notation InL := (InA eq_key_elt). + + Lemma xbindings_spec: forall m j acc k e, + InL (k,e) (xbindings m j acc) <-> + InL (k,e) acc \/ exists x, k=(j@x) /\ find x m = Some e. + Proof. + induction m as [|l IHl o r IHr]; simpl. + - intros. split; intro H. + + now left. + + destruct H as [H|[x [_ H]]]. assumption. + now rewrite gleaf in H. + - intros j acc k e. case o as [e'|]; + rewrite IHl, ?InA_cons, IHr; clear IHl IHr; split. + + intros [[H|[H|H]]|H]; auto. + * unfold eq_key_elt, E.eq, fst, snd in H. destruct H as (->,<-). + right. now exists 1. + * destruct H as (x,(->,H)). right. now exists x~1. + * destruct H as (x,(->,H)). right. now exists x~0. + + intros [H|H]; auto. + destruct H as (x,(->,H)). + destruct x; simpl in *. + * left. right. right. now exists x. + * right. now exists x. + * left. left. injection H as ->. reflexivity. + + intros [[H|H]|H]; auto. + * destruct H as (x,(->,H)). right. now exists x~1. + * destruct H as (x,(->,H)). right. now exists x~0. + + intros [H|H]; auto. + destruct H as (x,(->,H)). + destruct x; simpl in *. + * left. right. now exists x. + * right. now exists x. + * discriminate. + Qed. + + Lemma lt_rev_append: forall j x y, E.lt x y -> E.lt (j@x) (j@y). + Proof. induction j; intros; simpl; auto. Qed. + + Lemma xbindings_sort m j acc : + sort lt_key acc -> + (forall x p, In x m -> InL p acc -> E.lt (j@x) (fst p)) -> + sort lt_key (xbindings m j acc). + Proof. + revert j acc. + induction m as [|l IHl o r IHr]; simpl; trivial. + intros j acc Hacc Hsacc. destruct o as [e|]. + - apply IHl;[constructor;[apply IHr; [apply Hacc|]|]|]. + + intros. now apply Hsacc. + + case_eq (xbindings r j~1 acc); [constructor|]. + intros (z,e') q H. constructor. + assert (H': InL (z,e') (xbindings r j~1 acc)). + { rewrite H. now constructor. } + clear H q. rewrite xbindings_spec in H'. + destruct H' as [H'|H']. + * apply (Hsacc 1 (z,e')); trivial. now exists e. + * destruct H' as (x,(->,H)). + red. simpl. now apply lt_rev_append. + + intros x (y,e') Hx Hy. inversion_clear Hy. + rewrite H. simpl. now apply lt_rev_append. + rewrite xbindings_spec in H. + destruct H as [H|H]. + * now apply Hsacc. + * destruct H as (z,(->,H)). simpl. + now apply lt_rev_append. + - apply IHl; [apply IHr; [apply Hacc|]|]. + + intros. now apply Hsacc. + + intros x (y,e') Hx H. rewrite xbindings_spec in H. + destruct H as [H|H]. + * now apply Hsacc. + * destruct H as (z,(->,H)). simpl. + now apply lt_rev_append. + Qed. + + Lemma bindings_spec1 m k e : + InA eq_key_elt (k,e) (bindings m) <-> MapsTo k e m. + Proof. + unfold bindings, MapsTo. rewrite xbindings_spec. + split; [ intros [H|(y & H & H')] | intros IN ]. + - inversion H. + - simpl in *. now subst. + - right. now exists k. + Qed. + + Lemma bindings_spec2 m : sort lt_key (bindings m). + Proof. + unfold bindings. + apply xbindings_sort. constructor. inversion 2. + Qed. + + Lemma bindings_spec2w m : NoDupA eq_key (bindings m). + Proof. + apply ME.Sort_NoDupA. + apply bindings_spec2. + Qed. + + Lemma xbindings_length m j acc : + length (xbindings m j acc) = (cardinal m + length acc)%nat. + Proof. + revert j acc. + induction m; simpl; trivial; intros. + destruct o; simpl; rewrite IHm1; simpl; rewrite IHm2; + now rewrite ?Nat.add_succ_r, Nat.add_assoc. + Qed. + + Lemma cardinal_spec m : cardinal m = length (bindings m). + Proof. + unfold bindings. rewrite xbindings_length. simpl. + symmetry. apply Nat.add_0_r. + Qed. + + (** [map] and [mapi] *) + + Variable B : Type. + + Section Mapi. + + Variable f : key -> option A -> option B. + + Fixpoint xmapi (m : t A) (i : key) : t B := + match m with + | Leaf => Leaf + | Node l o r => Node (xmapi l (i~0)) + (f (rev i) o) + (xmapi r (i~1)) + end. + + End Mapi. + + Definition mapi (f : key -> A -> B) m := + xmapi (fun k => option_map (f k)) m 1. + + Definition map (f : A -> B) m := mapi (fun _ => f) m. + + End A. + + Lemma xgmapi: + forall (A B: Type) (f: key -> option A -> option B) (i j : key) (m: t A), + (forall k, f k None = None) -> + find i (xmapi f m j) = f (j@i) (find i m). + Proof. + induction i; intros; destruct m; simpl; rewrite ?IHi; auto. + Qed. + + Theorem mapi_spec0 : + forall (A B: Type) (f: key -> A -> B) (i: key) (m: t A), + find i (mapi f m) = option_map (f i) (find i m). + Proof. + intros. unfold mapi. rewrite xgmapi; simpl; auto. + Qed. + + Lemma mapi_spec : + forall (A B: Type) (f: key -> A -> B) (m: t A) (i:key), + exists j, E.eq j i /\ + find i (mapi f m) = option_map (f j) (find i m). + Proof. + intros. + exists i. split. reflexivity. apply mapi_spec0. + Qed. + + Lemma map_spec : + forall (elt elt':Type)(f:elt->elt')(m: t elt)(x:key), + find x (map f m) = option_map f (find x m). + Proof. + intros; unfold map. apply mapi_spec0. + Qed. + + Section merge. + Variable A B C : Type. + Variable f : key -> option A -> option B -> option C. + + Fixpoint xmerge (m1 : t A)(m2 : t B)(i:positive) : t C := + match m1 with + | Leaf => xmapi (fun k => f k None) m2 i + | Node l1 o1 r1 => + match m2 with + | Leaf => xmapi (fun k o => f k o None) m1 i + | Node l2 o2 r2 => + Node (xmerge l1 l2 (i~0)) + (f (rev i) o1 o2) + (xmerge r1 r2 (i~1)) + end + end. + + Lemma xgmerge: forall (i j: key)(m1:t A)(m2: t B), + (forall i, f i None None = None) -> + find i (xmerge m1 m2 j) = f (j@i) (find i m1) (find i m2). + Proof. + induction i; intros; destruct m1; destruct m2; simpl; auto; + rewrite ?xgmapi, ?IHi; simpl; auto. + Qed. + + End merge. + + Definition merge {A B C}(f:key->option A->option B->option C) m1 m2 := + xmerge + (fun k o1 o2 => match o1,o2 with + | None,None => None + | _, _ => f k o1 o2 + end) + m1 m2 xH. + + Lemma merge_spec1 {A B C}(f:key->option A->option B->option C) : + forall m m' x, + In x m \/ In x m' -> + exists y, E.eq y x /\ + find x (merge f m m') = f y (find x m) (find x m'). + Proof. + intros. exists x. split. reflexivity. + unfold merge. + rewrite xgmerge; simpl; auto. + rewrite <- 2 mem_spec, 2 mem_find in H. + destruct (find x m); simpl; auto. + destruct (find x m'); simpl; auto. intuition discriminate. + Qed. + + Lemma merge_spec2 {A B C}(f:key->option A->option B->option C) : + forall m m' x, In x (merge f m m') -> In x m \/ In x m'. + Proof. + intros. + rewrite <-mem_spec, mem_find in H. + unfold merge in H. + rewrite xgmerge in H; simpl; auto. + rewrite <- 2 mem_spec, 2 mem_find. + destruct (find x m); simpl in *; auto. + destruct (find x m'); simpl in *; auto. + Qed. + + Section Fold. + + Variables A B : Type. + Variable f : key -> A -> B -> B. + + (** the additional argument, [i], records the current path, in + reverse order (this should be more efficient: we reverse this argument + only at present nodes only, rather than at each node of the tree). + we also use this convention in all functions below + *) + + Fixpoint xfold (m : t A) (v : B) (i : key) := + match m with + | Leaf => v + | Node l (Some x) r => + xfold r (f (rev i) x (xfold l v i~0)) i~1 + | Node l None r => + xfold r (xfold l v i~0) i~1 + end. + Definition fold m i := xfold m i 1. + + End Fold. + + Lemma fold_spec : + forall {A}(m:t A){B}(i : B) (f : key -> A -> B -> B), + fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (bindings m) i. + Proof. + unfold fold, bindings. intros A m B i f. revert m i. + set (f' := fun a p => f (fst p) (snd p) a). + assert (H: forall m i j acc, + fold_left f' acc (xfold f m i j) = + fold_left f' (xbindings m j acc) i). + { induction m as [|l IHl o r IHr]; intros; trivial. + destruct o; simpl; now rewrite IHr, <- IHl. } + intros. exact (H m i 1 nil). + Qed. + + Fixpoint equal (A:Type)(cmp : A -> A -> bool)(m1 m2 : t A) : bool := + match m1, m2 with + | Leaf, _ => is_empty m2 + | _, Leaf => is_empty m1 + | Node l1 o1 r1, Node l2 o2 r2 => + (match o1, o2 with + | None, None => true + | Some v1, Some v2 => cmp v1 v2 + | _, _ => false + end) + &&& equal cmp l1 l2 &&& equal cmp r1 r2 + end. + + Definition Equal (A:Type)(m m':t A) := + forall y, find y m = find y m'. + Definition Equiv (A:Type)(eq_elt:A->A->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 (A:Type)(cmp: A->A->bool) := Equiv (Cmp cmp). + + Lemma equal_1 : forall (A:Type)(m m':t A)(cmp:A->A->bool), + Equivb cmp m m' -> equal cmp m m' = true. + Proof. + induction m. + - (* m = Leaf *) + destruct 1 as (E,_); simpl. + apply is_empty_spec; intros k. + destruct (find k m') eqn:F; trivial. + assert (H : In k m') by now exists a. + rewrite <- E in H. + destruct H as (x,H). red in H. now rewrite gleaf in H. + - (* m = Node *) + destruct m'. + + (* m' = Leaf *) + destruct 1 as (E,_); simpl. + destruct o. + * assert (H : In xH (@Leaf A)). + { rewrite <- E. now exists a. } + destruct H as (e,H). now red in H. + * apply andb_true_intro; split; apply is_empty_spec; intros k. + destruct (find k m1) eqn:F; trivial. + assert (H : In (xO k) (@Leaf A)). + { rewrite <- E. exists a; auto. } + destruct H as (x,H). red in H. now rewrite gleaf in H. + destruct (find k m2) eqn:F; trivial. + assert (H : In (xI k) (@Leaf A)). + { rewrite <- E. exists a; auto. } + destruct H as (x,H). red in H. now rewrite gleaf in H. + + (* m' = Node *) + destruct 1. + assert (Equivb cmp m1 m'1). + { split. + intros k; generalize (H (xO k)); unfold In, MapsTo; simpl; auto. + intros k e e'; generalize (H0 (xO k) e e'); unfold In, MapsTo; simpl; auto. } + assert (Equivb cmp m2 m'2). + { split. + intros k; generalize (H (xI k)); unfold In, MapsTo; simpl; auto. + intros k e e'; generalize (H0 (xI k) e e'); unfold In, MapsTo; simpl; auto. } + simpl. + destruct o; destruct o0; simpl. + repeat (apply andb_true_intro; split); auto. + apply (H0 xH); red; auto. + generalize (H xH); unfold In, MapsTo; simpl; intuition. + destruct H4; try discriminate; eauto. + generalize (H xH); unfold In, MapsTo; simpl; intuition. + destruct H5; try discriminate; eauto. + apply andb_true_intro; split; auto. + Qed. + + Lemma equal_2 : forall (A:Type)(m m':t A)(cmp:A->A->bool), + equal cmp m m' = true -> Equivb cmp m m'. + Proof. + induction m. + (* m = Leaf *) + simpl. + split; intros. + split. + destruct 1; red in H0; destruct k; discriminate. + rewrite is_empty_spec in H. + intros (e,H'). red in H'. now rewrite H in H'. + red in H0; destruct k; discriminate. + (* m = Node *) + destruct m'. + (* m' = Leaf *) + simpl. + destruct o; intros; try discriminate. + destruct (andb_prop _ _ H); clear H. + split; intros. + split; unfold In, MapsTo; destruct 1. + destruct k; simpl in *; try discriminate. + rewrite is_empty_spec in H1. + now rewrite H1 in H. + rewrite is_empty_spec in H0. + now rewrite H0 in H. + destruct k; simpl in *; discriminate. + unfold In, MapsTo; destruct k; simpl in *; discriminate. + (* m' = Node *) + destruct o; destruct o0; simpl; intros; try discriminate. + destruct (andb_prop _ _ H); clear H. + destruct (andb_prop _ _ H0); clear H0. + destruct (IHm1 _ _ H2); clear H2 IHm1. + destruct (IHm2 _ _ H1); clear H1 IHm2. + split; intros. + destruct k; unfold In, MapsTo in *; simpl; auto. + split; eauto. + destruct k; unfold In, MapsTo in *; simpl in *. + eapply H4; eauto. + eapply H3; eauto. + congruence. + destruct (andb_prop _ _ H); clear H. + destruct (IHm1 _ _ H0); clear H0 IHm1. + destruct (IHm2 _ _ H1); clear H1 IHm2. + split; intros. + destruct k; unfold In, MapsTo in *; simpl; auto. + split; eauto. + destruct k; unfold In, MapsTo in *; simpl in *. + eapply H3; eauto. + eapply H2; eauto. + try discriminate. + Qed. + + Lemma equal_spec : forall (A:Type)(m m':t A)(cmp:A->A->bool), + equal cmp m m' = true <-> Equivb cmp m m'. + Proof. + split. apply equal_2. apply equal_1. + Qed. + +End PositiveMap. + +(** Here come some additionnal facts about this implementation. + Most are facts that cannot be derivable from the general interface. *) + +Module PositiveMapAdditionalFacts. + Import PositiveMap. + + (* Derivable from the Map interface *) + Theorem gsspec {A} i j x (m: t A) : + find i (add j x m) = if E.eq_dec i j then Some x else find i m. + Proof. + destruct (E.eq_dec i j) as [->|]; + [ apply add_spec1 | apply add_spec2; auto ]. + Qed. + + (* Not derivable from the Map interface *) + Theorem gsident {A} i (m:t A) v : + find i m = Some v -> add i v m = m. + Proof. + revert m. + induction i; destruct m; simpl in *; try congruence. + - intro H; now rewrite (IHi m2 H). + - intro H; now rewrite (IHi m1 H). + Qed. + + Lemma xmapi_ext {A B}(f g: key -> option A -> option B) : + (forall k (o : option A), f k o = g k o) -> + forall m i, xmapi f m i = xmapi g m i. + Proof. + induction m; intros; simpl; auto. now f_equal. + Qed. + + Theorem xmerge_commut{A B C} + (f: key -> option A -> option B -> option C) + (g: key -> option B -> option A -> option C) : + (forall k o1 o2, f k o1 o2 = g k o2 o1) -> + forall m1 m2 i, xmerge f m1 m2 i = xmerge g m2 m1 i. + Proof. + intros E. + induction m1; destruct m2; intros i; simpl; trivial; f_equal; + try apply IHm1_1; try apply IHm1_2; try apply xmapi_ext; + intros; apply E. + Qed. + + Theorem merge_commut{A B C} + (f: key -> option A -> option B -> option C) + (g: key -> option B -> option A -> option C) : + (forall k o1 o2, f k o1 o2 = g k o2 o1) -> + forall m1 m2, merge f m1 m2 = merge g m2 m1. + Proof. + intros E m1 m2. + unfold merge. apply xmerge_commut. + intros k [x1|] [x2|]; trivial. + Qed. + +End PositiveMapAdditionalFacts. diff --git a/theories/MMaps/MMapWeakList.v b/theories/MMaps/MMapWeakList.v new file mode 100644 index 00000000..656c61e1 --- /dev/null +++ b/theories/MMaps/MMapWeakList.v @@ -0,0 +1,687 @@ +(***********************************************************************) +(* 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 *) + +(** This file proposes an implementation of the non-dependant interface + [MMapInterface.WS] using lists of pairs, unordered but without redundancy. *) + +Require Import MMapInterface EqualitiesFacts. + +Set Implicit Arguments. +Unset Strict Implicit. + +Lemma Some_iff {A} (a a' : A) : Some a = Some a' <-> a = a'. +Proof. split; congruence. Qed. + +Module Raw (X:DecidableType). + +Module Import PX := KeyDecidableType X. + +Definition key := X.t. +Definition t (elt:Type) := list (X.t * elt). + +Ltac dec := match goal with + | |- context [ X.eq_dec ?x ?x ] => + let E := fresh "E" in destruct (X.eq_dec x x) as [E|E]; [ | now elim E] + | H : X.eq ?x ?y |- context [ X.eq_dec ?x ?y ] => + let E := fresh "E" in destruct (X.eq_dec x y) as [_|E]; [ | now elim E] + | H : ~X.eq ?x ?y |- context [ X.eq_dec ?x ?y ] => + let E := fresh "E" in destruct (X.eq_dec x y) as [E|_]; [ now elim H | ] + | |- context [ X.eq_dec ?x ?y ] => + let E := fresh "E" in destruct (X.eq_dec x y) as [E|E] +end. + +Section Elt. + +Variable elt : Type. +Notation NoDupA := (@NoDupA _ eqk). + +(** * [find] *) + +Fixpoint find (k:key) (s: t elt) : option elt := + match s with + | nil => None + | (k',x)::s' => if X.eq_dec k k' then Some x else find k s' + end. + +Lemma find_spec : forall m (Hm:NoDupA m) x e, + find x m = Some e <-> MapsTo x e m. +Proof. + unfold PX.MapsTo. + induction m as [ | (k,e) m IH]; simpl. + - split; inversion 1. + - intros Hm k' e'. rewrite InA_cons. + change (eqke (k',e') (k,e)) with (X.eq k' k /\ e' = e). + inversion_clear Hm. dec. + + rewrite Some_iff; intuition. + elim H. apply InA_eqk with (k',e'); auto. + + rewrite IH; intuition. +Qed. + +(** * [mem] *) + +Fixpoint mem (k : key) (s : t elt) : bool := + match s with + | nil => false + | (k',_) :: l => if X.eq_dec k k' then true else mem k l + end. + +Lemma mem_spec : forall m (Hm:NoDupA m) x, mem x m = true <-> In x m. +Proof. + induction m as [ | (k,e) m IH]; simpl; intros Hm x. + - split. discriminate. inversion_clear 1. inversion H0. + - inversion_clear Hm. rewrite PX.In_cons; simpl. + rewrite <- IH by trivial. + dec; intuition. +Qed. + +(** * [empty] *) + +Definition empty : t elt := nil. + +Lemma empty_spec x : find x empty = None. +Proof. + reflexivity. +Qed. + +Lemma empty_NoDup : NoDupA empty. +Proof. + unfold empty; auto. +Qed. + +(** * [is_empty] *) + +Definition is_empty (l : t elt) : bool := if l then true else false. + +Lemma is_empty_spec m : is_empty m = true <-> forall x, find x m = None. +Proof. + destruct m; simpl; intuition; try discriminate. + specialize (H a). + revert H. now dec. +Qed. + +(* Not part of the exported specifications, used later for [merge]. *) + +Lemma find_eq : forall m (Hm:NoDupA m) x x', + X.eq x x' -> find x m = find x' m. +Proof. + induction m; simpl; auto; destruct a; intros. + inversion_clear Hm. + rewrite (IHm H1 x x'); auto. + dec; dec; trivial. + elim E0. now transitivity x. + elim E. now transitivity x'. +Qed. + +(** * [add] *) + +Fixpoint add (k : key) (x : elt) (s : t elt) : t elt := + match s with + | nil => (k,x) :: nil + | (k',y) :: l => if X.eq_dec k k' then (k,x)::l else (k',y)::add k x l + end. + +Lemma add_spec1 m x e : find x (add x e m) = Some e. +Proof. + induction m as [ | (k,e') m IH]; simpl. + - now dec. + - dec; simpl; now dec. +Qed. + +Lemma add_spec2 m x y e : ~X.eq x y -> find y (add x e m) = find y m. +Proof. + intros N. + assert (N' : ~X.eq y x) by now contradict N. + induction m as [ | (k,e') m IH]; simpl. + - dec; trivial. + - repeat (dec; simpl); trivial. elim N. now transitivity k. +Qed. + +Lemma add_InA : forall m x y e e', + ~ X.eq x y -> InA eqk (y,e) (add x e' m) -> InA eqk (y,e) m. +Proof. + induction m as [ | (k,e') m IH]; simpl; intros. + - inversion_clear H0. elim H. symmetry; apply H1. inversion_clear H1. + - revert H0; dec; rewrite !InA_cons. + + rewrite E. intuition. + + intuition. right; eapply IH; eauto. +Qed. + +Lemma add_NoDup : forall m (Hm:NoDupA m) x e, NoDupA (add x e m). +Proof. + induction m as [ | (k,e') m IH]; simpl; intros Hm x e. + - constructor; auto. now inversion 1. + - inversion_clear Hm. dec; constructor; auto. + + contradict H. apply InA_eqk with (x,e); auto. + + contradict H; apply add_InA with x e; auto. +Qed. + +(** * [remove] *) + +Fixpoint remove (k : key) (s : t elt) : t elt := + match s with + | nil => nil + | (k',x) :: l => if X.eq_dec k k' then l else (k',x) :: remove k l + end. + +Lemma remove_spec1 m (Hm: NoDupA m) x : find x (remove x m) = None. +Proof. + induction m as [ | (k,e') m IH]; simpl; trivial. + inversion_clear Hm. + repeat (dec; simpl); auto. + destruct (find x m) eqn:F; trivial. + apply find_spec in F; trivial. + elim H. apply InA_eqk with (x,e); auto. +Qed. + +Lemma remove_spec2 m (Hm: NoDupA m) x y : ~X.eq x y -> + find y (remove x m) = find y m. +Proof. + induction m as [ | (k,e') m IH]; simpl; trivial; intros E. + inversion_clear Hm. + repeat (dec; simpl); auto. + elim E. now transitivity k. +Qed. + +Lemma remove_InA : forall m (Hm:NoDupA m) x y e, + InA eqk (y,e) (remove x m) -> InA eqk (y,e) m. +Proof. + induction m as [ | (k,e') m IH]; simpl; trivial; intros. + inversion_clear Hm. + revert H; dec; rewrite !InA_cons; intuition. + right; eapply H; eauto. +Qed. + +Lemma remove_NoDup : forall m (Hm:NoDupA m) x, NoDupA (remove x m). +Proof. + induction m. + simpl; intuition. + intros. + inversion_clear Hm. + destruct a as (x',e'). + simpl; case (X.eq_dec x x'); auto. + constructor; auto. + contradict H; apply remove_InA with x; auto. +Qed. + +(** * [bindings] *) + +Definition bindings (m: t elt) := m. + +Lemma bindings_spec1 m x e : InA eqke (x,e) (bindings m) <-> MapsTo x e m. +Proof. + reflexivity. +Qed. + +Lemma bindings_spec2w m (Hm:NoDupA m) : NoDupA (bindings m). +Proof. + trivial. +Qed. + +(** * [fold] *) + +Fixpoint fold (A:Type)(f:key->elt->A->A)(m:t elt) (acc : A) : A := + match m with + | nil => acc + | (k,e)::m' => fold f m' (f k e acc) + end. + +Lemma fold_spec : forall m (A:Type)(i:A)(f:key->elt->A->A), + fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (bindings m) i. +Proof. + induction m as [ | (k,e) m IH]; simpl; auto. +Qed. + +(** * [equal] *) + +Definition check (cmp : elt -> elt -> bool)(k:key)(e:elt)(m': t elt) := + match find k m' with + | None => false + | Some e' => cmp e e' + end. + +Definition submap (cmp : elt -> elt -> bool)(m m' : t elt) : bool := + fold (fun k e b => andb (check cmp k e m') b) m true. + +Definition equal (cmp : elt -> elt -> bool)(m m' : t elt) : bool := + andb (submap cmp m m') (submap (fun e' e => cmp e e') m' m). + +Definition Submap (cmp:elt->elt->bool) m m' := + (forall k, In k m -> In k m') /\ + (forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true). + +Definition Equivb (cmp:elt->elt->bool) m m' := + (forall k, In k m <-> In k m') /\ + (forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true). + +Lemma submap_1 : forall m (Hm:NoDupA m) m' (Hm': NoDupA m') cmp, + Submap cmp m m' -> submap cmp m m' = true. +Proof. + unfold Submap, submap. + induction m. + simpl; auto. + destruct a; simpl; intros. + destruct H. + inversion_clear Hm. + assert (H3 : In t0 m'). + { apply H; exists e; auto with *. } + destruct H3 as (e', H3). + assert (H4 : find t0 m' = Some e') by now apply find_spec. + unfold check at 2. rewrite H4. + rewrite (H0 t0); simpl; auto with *. + eapply IHm; auto. + split; intuition. + apply H. + destruct H6 as (e'',H6); exists e''; auto. + apply H0 with k; auto. +Qed. + +Lemma submap_2 : forall m (Hm:NoDupA m) m' (Hm': NoDupA m') cmp, + submap cmp m m' = true -> Submap cmp m m'. +Proof. + unfold Submap, submap. + induction m. + simpl; auto. + intuition. + destruct H0; inversion H0. + inversion H0. + + destruct a; simpl; intros. + inversion_clear Hm. + rewrite andb_b_true in H. + assert (check cmp t0 e m' = true). + clear H1 H0 Hm' IHm. + set (b:=check cmp t0 e m') in *. + generalize H; clear H; generalize b; clear b. + induction m; simpl; auto; intros. + destruct a; simpl in *. + destruct (andb_prop _ _ (IHm _ H)); auto. + rewrite H2 in H. + destruct (IHm H1 m' Hm' cmp H); auto. + unfold check in H2. + case_eq (find t0 m'); [intros e' H5 | intros H5]; + rewrite H5 in H2; try discriminate. + split; intros. + destruct H6 as (e0,H6); inversion_clear H6. + compute in H7; destruct H7; subst. + exists e'. + apply PX.MapsTo_eq with t0; auto with *. + apply find_spec; auto. + apply H3. + exists e0; auto. + inversion_clear H6. + compute in H8; destruct H8; subst. + assert (H8 : MapsTo t0 e'0 m'). { eapply PX.MapsTo_eq; eauto. } + apply find_spec in H8; trivial. congruence. + apply H4 with k; auto. +Qed. + +(** Specification of [equal] *) + +Lemma equal_spec : forall m (Hm:NoDupA m) m' (Hm': NoDupA m') cmp, + equal cmp m m' = true <-> Equivb cmp m m'. +Proof. + unfold Equivb, equal. + split. + - intros. + destruct (andb_prop _ _ H); clear H. + generalize (submap_2 Hm Hm' H0). + generalize (submap_2 Hm' Hm H1). + firstorder. + - intuition. + apply andb_true_intro; split; apply submap_1; unfold Submap; firstorder. +Qed. +End Elt. +Section Elt2. +Variable elt elt' : Type. + +(** * [map] and [mapi] *) + +Fixpoint map (f:elt -> elt') (m:t elt) : t elt' := + match m with + | nil => nil + | (k,e)::m' => (k,f e) :: map f m' + end. + +Fixpoint mapi (f: key -> elt -> elt') (m:t elt) : t elt' := + match m with + | nil => nil + | (k,e)::m' => (k,f k e) :: mapi f m' + end. + +(** Specification of [map] *) + +Lemma map_spec (f:elt->elt')(m:t elt)(x:key) : + find x (map f m) = option_map f (find x m). +Proof. + induction m as [ | (k,e) m IH]; simpl; trivial. + dec; simpl; trivial. +Qed. + +Lemma map_NoDup m (Hm : NoDupA (@eqk elt) m)(f:elt->elt') : + NoDupA (@eqk elt') (map f m). +Proof. + induction m; simpl; auto. + intros. + destruct a as (x',e'). + inversion_clear Hm. + constructor; auto. + contradict H. + clear IHm H0. + induction m; simpl in *; auto. + inversion H. + destruct a; inversion H; auto. +Qed. + +(** Specification of [mapi] *) + +Lemma mapi_spec (f:key->elt->elt')(m:t elt)(x:key) : + exists y, X.eq y x /\ find x (mapi f m) = option_map (f y) (find x m). +Proof. + induction m as [ | (k,e) m IH]; simpl; trivial. + - now exists x. + - dec; simpl. + + now exists k. + + destruct IH as (y,(Hy,H)). now exists y. +Qed. + +Lemma mapi_NoDup : forall m (Hm : NoDupA (@eqk elt) m)(f: key->elt->elt'), + NoDupA (@eqk elt') (mapi f m). +Proof. + induction m; simpl; auto. + intros. + destruct a as (x',e'). + inversion_clear Hm; auto. + constructor; auto. + contradict H. + clear IHm H0. + induction m; simpl in *; auto. + inversion_clear H. + destruct a; inversion_clear H; auto. +Qed. + +End Elt2. + +Lemma mapfst_InA {elt}(m:t elt) x : + InA X.eq x (List.map fst m) <-> In x m. +Proof. + induction m as [| (k,e) m IH]; simpl; auto. + - split; inversion 1. inversion H0. + - rewrite InA_cons, In_cons. simpl. now rewrite IH. +Qed. + +Lemma mapfst_NoDup {elt}(m:t elt) : + NoDupA X.eq (List.map fst m) <-> NoDupA eqk m. +Proof. + induction m as [| (k,e) m IH]; simpl. + - split; constructor. + - split; inversion_clear 1; constructor; try apply IH; trivial. + + contradict H0. rewrite mapfst_InA. eapply In_alt'; eauto. + + rewrite mapfst_InA. contradict H0. now apply In_alt'. +Qed. + +Lemma filter_NoDup f (m:list key) : + NoDupA X.eq m -> NoDupA X.eq (List.filter f m). +Proof. + induction 1; simpl. + - constructor. + - destruct (f x); trivial. constructor; trivial. + contradict H. rewrite InA_alt in *. destruct H as (y,(Hy,H)). + exists y; split; trivial. now rewrite filter_In in H. +Qed. + +Lemma NoDupA_unique_repr (l:list key) x y : + NoDupA X.eq l -> X.eq x y -> List.In x l -> List.In y l -> x = y. +Proof. + intros H E Hx Hy. + induction H; simpl in *. + - inversion Hx. + - intuition; subst; trivial. + elim H. apply InA_alt. now exists y. + elim H. apply InA_alt. now exists x. +Qed. + +Section Elt3. + +Variable elt elt' elt'' : Type. + +Definition restrict (m:t elt)(k:key) := + match find k m with + | None => true + | Some _ => false + end. + +Definition domains (m:t elt)(m':t elt') := + List.map fst m ++ List.filter (restrict m) (List.map fst m'). + +Lemma domains_InA m m' (Hm : NoDupA eqk m) x : + InA X.eq x (domains m m') <-> In x m \/ In x m'. +Proof. + unfold domains. + assert (Proper (X.eq==>eq) (restrict m)). + { intros k k' Hk. unfold restrict. now rewrite (find_eq Hm Hk). } + rewrite InA_app_iff, filter_InA, !mapfst_InA; intuition. + unfold restrict. + destruct (find x m) eqn:F. + - left. apply find_spec in F; trivial. now exists e. + - now right. +Qed. + +Lemma domains_NoDup m m' : NoDupA eqk m -> NoDupA eqk m' -> + NoDupA X.eq (domains m m'). +Proof. + intros Hm Hm'. unfold domains. + apply NoDupA_app; auto with *. + - now apply mapfst_NoDup. + - now apply filter_NoDup, mapfst_NoDup. + - intros x. + rewrite mapfst_InA. intros (e,H). + apply find_spec in H; trivial. + rewrite InA_alt. intros (y,(Hy,H')). + rewrite (find_eq Hm Hy) in H. + rewrite filter_In in H'. destruct H' as (_,H'). + unfold restrict in H'. now rewrite H in H'. +Qed. + +Fixpoint fold_keys (f:key->option elt'') l := + match l with + | nil => nil + | k::l => + match f k with + | Some e => (k,e)::fold_keys f l + | None => fold_keys f l + end + end. + +Lemma fold_keys_In f l x e : + List.In (x,e) (fold_keys f l) <-> List.In x l /\ f x = Some e. +Proof. + induction l as [|k l IH]; simpl. + - intuition. + - destruct (f k) eqn:F; simpl; rewrite IH; clear IH; intuition; + try left; congruence. +Qed. + +Lemma fold_keys_NoDup f l : + NoDupA X.eq l -> NoDupA eqk (fold_keys f l). +Proof. + induction 1; simpl. + - constructor. + - destruct (f x); trivial. + constructor; trivial. contradict H. + apply InA_alt in H. destruct H as ((k,e'),(E,H)). + rewrite fold_keys_In in H. + apply InA_alt. exists k. now split. +Qed. + +Variable f : key -> option elt -> option elt' -> option elt''. + +Definition merge m m' : t elt'' := + fold_keys (fun k => f k (find k m) (find k m')) (domains m m'). + +Lemma merge_NoDup m (Hm:NoDupA (@eqk elt) m) m' (Hm':NoDupA (@eqk elt') m') : + NoDupA (@eqk elt'') (merge m m'). +Proof. + now apply fold_keys_NoDup, domains_NoDup. +Qed. + +Lemma merge_spec1 m (Hm:NoDupA eqk m) m' (Hm':NoDupA eqk m') x : + In x m \/ In x m' -> + exists y:key, X.eq y x /\ + find x (merge m m') = f y (find x m) (find x m'). +Proof. + assert (Hmm' : NoDupA eqk (merge m m')) by now apply merge_NoDup. + rewrite <- domains_InA; trivial. + rewrite InA_alt. intros (y,(Hy,H)). + exists y; split; [easy|]. + rewrite (find_eq Hm Hy), (find_eq Hm' Hy). + destruct (f y (find y m) (find y m')) eqn:F. + - apply find_spec; trivial. + red. apply InA_alt. exists (y,e). split. now split. + unfold merge. apply fold_keys_In. now split. + - destruct (find x (merge m m')) eqn:F'; trivial. + rewrite <- F; clear F. symmetry. + apply find_spec in F'; trivial. + red in F'. rewrite InA_alt in F'. + destruct F' as ((y',e'),(E,F')). + unfold merge in F'; rewrite fold_keys_In in F'. + destruct F' as (H',F'). + compute in E; destruct E as (Hy',<-). + replace y with y'; trivial. + apply (@NoDupA_unique_repr (domains m m')); auto. + now apply domains_NoDup. + now transitivity x. +Qed. + +Lemma merge_spec2 m (Hm:NoDupA eqk m) m' (Hm':NoDupA eqk m') x : + In x (merge m m') -> In x m \/ In x m'. +Proof. + rewrite <- domains_InA; trivial. + intros (e,H). red in H. rewrite InA_alt in H. destruct H as ((k,e'),(E,H)). + unfold merge in H; rewrite fold_keys_In in H. destruct H as (H,_). + apply InA_alt. exists k. split; trivial. now destruct E. +Qed. + +End Elt3. +End Raw. + + +Module Make (X: DecidableType) <: WS with Module E:=X. + Module Raw := Raw X. + + Module E := X. + Definition key := E.t. + Definition eq_key {elt} := @Raw.PX.eqk elt. + Definition eq_key_elt {elt} := @Raw.PX.eqke elt. + + Record t_ (elt:Type) := Mk + {this :> Raw.t elt; + nodup : NoDupA Raw.PX.eqk this}. + Definition t := t_. + + Definition empty {elt} : t elt := Mk (Raw.empty_NoDup elt). + +Section Elt. + Variable elt elt' elt'':Type. + Implicit Types m : t elt. + Implicit Types x y : key. + Implicit Types e : elt. + + Definition find x m : option elt := Raw.find x m.(this). + Definition mem x m : bool := Raw.mem x m.(this). + Definition is_empty m : bool := Raw.is_empty m.(this). + Definition add x e m : t elt := Mk (Raw.add_NoDup m.(nodup) x e). + Definition remove x m : t elt := Mk (Raw.remove_NoDup m.(nodup) x). + Definition map f m : t elt' := Mk (Raw.map_NoDup m.(nodup) f). + Definition mapi (f:key->elt->elt') m : t elt' := + Mk (Raw.mapi_NoDup m.(nodup) f). + Definition merge f m (m':t elt') : t elt'' := + Mk (Raw.merge_NoDup f m.(nodup) m'.(nodup)). + Definition bindings m : list (key*elt) := Raw.bindings m.(this). + Definition cardinal m := length m.(this). + Definition fold {A}(f:key->elt->A->A) m (i:A) : A := Raw.fold f m.(this) i. + Definition equal cmp m m' : bool := Raw.equal cmp m.(this) m'.(this). + Definition MapsTo x e m : Prop := Raw.PX.MapsTo x e m.(this). + Definition In x m : Prop := Raw.PX.In x m.(this). + + 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 m m' : Prop := Raw.Equivb cmp m.(this) m'.(this). + + Instance MapsTo_compat : + Proper (E.eq==>Logic.eq==>Logic.eq==>iff) MapsTo. + Proof. + intros x x' Hx e e' <- m m' <-. unfold MapsTo. now rewrite Hx. + Qed. + + Lemma find_spec m : forall x e, find x m = Some e <-> MapsTo x e m. + Proof. exact (Raw.find_spec m.(nodup)). Qed. + + Lemma mem_spec m : forall x, mem x m = true <-> In x m. + Proof. exact (Raw.mem_spec m.(nodup)). Qed. + + Lemma empty_spec : forall x, find x empty = None. + Proof. exact (Raw.empty_spec _). Qed. + + Lemma is_empty_spec m : is_empty m = true <-> (forall x, find x m = None). + Proof. exact (Raw.is_empty_spec m.(this)). Qed. + + Lemma add_spec1 m : forall x e, find x (add x e m) = Some e. + Proof. exact (Raw.add_spec1 m.(this)). Qed. + Lemma add_spec2 m : forall x y e, ~E.eq x y -> find y (add x e m) = find y m. + Proof. exact (Raw.add_spec2 m.(this)). Qed. + + Lemma remove_spec1 m : forall x, find x (remove x m) = None. + Proof. exact (Raw.remove_spec1 m.(nodup)). Qed. + Lemma remove_spec2 m : forall x y, ~E.eq x y -> find y (remove x m) = find y m. + Proof. exact (Raw.remove_spec2 m.(nodup)). Qed. + + Lemma bindings_spec1 m : forall x e, + InA eq_key_elt (x,e) (bindings m) <-> MapsTo x e m. + Proof. exact (Raw.bindings_spec1 m.(this)). Qed. + Lemma bindings_spec2w m : NoDupA eq_key (bindings m). + Proof. exact (Raw.bindings_spec2w m.(nodup)). Qed. + + Lemma cardinal_spec m : cardinal m = length (bindings m). + Proof. reflexivity. Qed. + + Lemma fold_spec m : forall (A : Type) (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. exact (Raw.fold_spec m.(this)). Qed. + + Lemma equal_spec m m' : forall cmp, equal cmp m m' = true <-> Equivb cmp m m'. + Proof. exact (Raw.equal_spec m.(nodup) m'.(nodup)). Qed. + +End Elt. + + Lemma map_spec {elt elt'} (f:elt->elt') m : + forall x, find x (map f m) = option_map f (find x m). + Proof. exact (Raw.map_spec f m.(this)). Qed. + + Lemma mapi_spec {elt elt'} (f:key->elt->elt') m : + forall x, exists y, + E.eq y x /\ find x (mapi f m) = option_map (f y) (find x m). + Proof. exact (Raw.mapi_spec f m.(this)). Qed. + + Lemma merge_spec1 {elt elt' elt''} + (f:key->option elt->option elt'->option elt'') m m' : + forall x, + In x m \/ In x m' -> + exists y, E.eq y x /\ find x (merge f m m') = f y (find x m) (find x m'). + Proof. exact (Raw.merge_spec1 f m.(nodup) m'.(nodup)). Qed. + + Lemma merge_spec2 {elt elt' elt''} + (f:key->option elt->option elt'->option elt'') m m' : + forall x, + In x (merge f m m') -> In x m \/ In x m'. + Proof. exact (Raw.merge_spec2 m.(nodup) m'.(nodup)). Qed. + +End Make. diff --git a/theories/MMaps/MMaps.v b/theories/MMaps/MMaps.v new file mode 100644 index 00000000..054d0722 --- /dev/null +++ b/theories/MMaps/MMaps.v @@ -0,0 +1,16 @@ +(***********************************************************************) +(* 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 *) +(***********************************************************************) + + +Require Export Orders OrdersEx OrdersAlt. +Require Export Equalities. +Require Export MMapInterface. +Require Export MMapFacts. +Require Export MMapWeakList. +Require Export MMapList. +Require Export MMapPositive. diff --git a/theories/MMaps/vo.itarget b/theories/MMaps/vo.itarget new file mode 100644 index 00000000..a7bbd266 --- /dev/null +++ b/theories/MMaps/vo.itarget @@ -0,0 +1,7 @@ +MMapInterface.vo +MMapFacts.vo +MMapWeakList.vo +MMapList.vo +MMapPositive.vo +MMaps.vo +MMapAVL.vo
\ No newline at end of file |