Library Stdlib.FSets.FMapAVL



FMapAVL

This module implements maps using AVL trees. It follows the implementation from Ocaml's standard library.
See the comments at the beginning of FSetAVL for more details.

Require Import FMapInterface FMapList ZArith Int.

Set Implicit Arguments.

Notations and helper lemma about pairs

Declare Scope pair_scope.
Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope.
Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope.

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.
#[global]
Hint Transparent key : core.

Trees

Trees

The fifth field of Node is the height of the tree

#[universes(template)]
Inductive tree {elt : Type} :=
  | Leaf : tree
  | Node : tree -> key -> elt -> tree -> int -> tree.
Arguments tree : clear implicits.

Section Elt.

Variable elt : Type.

Notation t := (tree elt).

Implicit Types m : t.

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 : t := 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
             | LT _ => mem x l
             | EQ _ => true
             | GT _ => mem x r
         end
   end.

Fixpoint find x m : option elt :=
   match m with
     | Leaf => None
     | Node l y d r _ => match X.compare x y with
             | LT _ => find x l
             | EQ _ => Some d
             | GT _ => find x r
         end
   end.

Helper functions

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.

Definition bal l x d r :=
  let hl := height l in
  let hr := height r in
  if gt_le_dec hl (hr+2) then
    match l with
     | Leaf => assert_false l x d r
     | Node ll lx ld lr _ =>
       if ge_lt_dec (height ll) (height lr) then
         create ll lx ld (create lr x d r)
       else
         match lr with
          | Leaf => assert_false l x d r
          | Node lrl lrx lrd lrr _ =>
              create (create ll lx ld lrl) lrx lrd (create lrr x d r)
         end
    end
  else
    if gt_le_dec hr (hl+2) then
      match r with
       | Leaf => assert_false l x d r
       | Node rl rx rd rr _ =>
         if ge_lt_dec (height rr) (height rl) then
            create (create l x d rl) rx rd rr
         else
           match rl with
            | Leaf => assert_false l x d r
            | Node rll rlx rld rlr _ =>
                create (create l x d rll) rlx rld (create rlr rx rd rr)
           end
      end
    else
      create l x d r.

Insertion


Fixpoint add x d m :=
  match m with
   | Leaf => Node Leaf x d Leaf 1
   | Node l y d' r h =>
      match X.compare x y with
         | LT _ => bal (add x d l) y d' r
         | EQ _ => Node l y d r h
         | GT _ => bal l y d' (add x d r)
      end
  end.

Extraction of minimum binding

Morally, remove_min is to be applied to a non-empty tree t = Node l x e r h. Since we can't deal here with assert false for t=Leaf, we pre-unpack t (and forget about h).

Fixpoint remove_min l x d r : t*(key*elt) :=
  match l with
    | Leaf => (r,(x,d))
    | Node ll lx ld lr lh =>
       let (l',m) := remove_min ll lx ld lr in
       (bal l' x d r, m)
  end.

Merging two trees

merge t1 t2 builds the union of t1 and t2 assuming all elements of t1 to be smaller than all elements of t2, and |height t1 - height t2| <= 2.

Definition merge s1 s2 := match s1,s2 with
  | Leaf, _ => s2
  | _, Leaf => s1
  | _, Node l2 x2 d2 r2 h2 =>
    match remove_min l2 x2 d2 r2 with
      (s2',(x,d)) => bal s1 x d s2'
    end
end.

Deletion


Fixpoint remove x m := match m with
  | Leaf => Leaf
  | Node l y d r h =>
      match X.compare x y with
         | LT _ => bal (remove x l) y d r
         | EQ _ => merge l r
         | GT _ => bal l y d (remove x r)
      end
   end.

join

Same as bal but does not assume anything regarding heights of l and r.

Fixpoint join l : key -> elt -> t -> t :=
  match l with
    | Leaf => add
    | Node ll lx ld lr lh => fun x d =>
       fix join_aux (r:t) : t := match r with
          | Leaf => add x d l
          | Node rl rx rd rr rh =>
               if gt_le_dec lh (rh+2) then bal ll lx ld (join lr x d r)
               else if gt_le_dec rh (lh+2) then bal (join_aux rl) rx rd rr
               else create l x d r
          end
  end.

Splitting

split x m returns a triple (l, o, r) where
  • l is the set of elements of m that are < x
  • r is the set of elements of m that are > x
  • o is the result of find x m.

Record triple := mktriple { t_left:t; t_opt:option elt; t_right:t }.
Notation "<< l , b , r >>" := (mktriple l b r) (at level 9).

Fixpoint split x m : triple := match m with
  | Leaf => << Leaf, None, Leaf >>
  | Node l y d r h =>
     match X.compare x y with
      | LT _ => let (ll,o,rl) := split x l in << ll, o, join rl y d r >>
      | EQ _ => << l, Some d, r >>
      | GT _ => let (rl,o,rr) := split x r in << join l y d rl, o, rr >>
     end
 end.

Concatenation

Same as merge but does not assume anything about heights.

Definition concat m1 m2 :=
   match m1, m2 with
      | Leaf, _ => m2
      | _ , Leaf => m1
      | _, Node l2 x2 d2 r2 _ =>
            let (m2',xd) := remove_min l2 x2 d2 r2 in
            join m1 xd#1 xd#2 m2'
   end.

Elements

elements_tree_aux acc t catenates the elements of t in infix order to the list acc

Fixpoint elements_aux (acc : list (key*elt)) m : list (key*elt) :=
  match m with
   | Leaf => acc
   | Node l x d r _ => elements_aux ((x,d) :: elements_aux acc r) l
  end.

then elements is an instantiation with an empty acc

Definition elements := elements_aux nil.

Fold


Fixpoint fold (A : Type) (f : key -> elt -> A -> A) (m : t) : A -> A :=
 fun a => match m with
  | Leaf => a
  | Node l x d r _ => fold f r (f x d (fold f l a))
 end.

Comparison


Variable cmp : elt->elt->bool.

Enumeration of the elements of a tree


Inductive enumeration :=
 | End : enumeration
 | More : key -> elt -> t -> enumeration -> enumeration.

cons m e adds the elements of tree m on the head of enumeration e.

Fixpoint cons m e : enumeration :=
 match m with
  | Leaf => e
  | Node l x d r h => cons l (More x d r e)
 end.

One step of comparison of elements

Definition equal_more x1 d1 (cont:enumeration->bool) e2 :=
 match e2 with
 | End => false
 | More x2 d2 r2 e2 =>
     match X.compare x1 x2 with
      | EQ _ => cmp d1 d2 &&& cont (cons r2 e2)
      | _ => false
     end
 end.

Comparison of left tree, middle element, then right tree

Fixpoint equal_cont m1 (cont:enumeration->bool) e2 :=
 match m1 with
  | Leaf => cont e2
  | Node l1 x1 d1 r1 _ =>
     equal_cont l1 (equal_more x1 d1 (equal_cont r1 cont)) e2
  end.

Initial continuation

Definition equal_end e2 := match e2 with End => true | _ => false end.

The complete comparison

Definition equal m1 m2 := equal_cont m1 equal_end (cons m2 End).

End Elt.
Notation t := tree.
Arguments Leaf : clear implicits.
Arguments Node [elt].

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.


Fixpoint mapi (elt elt' : Type)(f : key -> elt -> elt')(m : t elt) : t elt' :=
  match m with
   | Leaf _ => Leaf _
   | Node l x d r h => Node (mapi f l) x (f x d) (mapi f r) h
  end.

Map with removal


Fixpoint map_option (elt elt' : Type)(f : key -> elt -> option elt')(m : t elt)
  : t elt' :=
  match m with
   | Leaf _ => Leaf _
   | Node l x d r h =>
      match f x d with
       | Some d' => join (map_option f l) x d' (map_option f r)
       | None => concat (map_option f l) (map_option f r)
      end
  end.

Optimized map2

Suggestion by B. Gregoire: a map2 function with specialized arguments 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 Map2_opt.
Variable elt elt' elt'' : Type.
Variable f : key -> elt -> option elt' -> option elt''.
Variable mapl : t elt -> t elt''.
Variable mapr : t elt' -> t elt''.

Fixpoint map2_opt m1 m2 :=
 match m1, m2 with
  | Leaf _, _ => mapr m2
  | _, Leaf _ => mapl m1
  | Node l1 x1 d1 r1 h1, _ =>
     let (l2',o2,r2') := split x1 m2 in
     match f x1 d1 o2 with
      | Some e => join (map2_opt l1 l2') x1 e (map2_opt r1 r2')
      | None => concat (map2_opt l1 l2') (map2_opt r1 r2')
     end
 end.

End Map2_opt.

Map2

The map2 function of the Map interface can be implemented via map2_opt and map_option.

Section Map2.
Variable elt elt' elt'' : Type.
Variable f : option elt -> option elt' -> option elt''.

Definition map2 : t elt -> t elt' -> t elt'' :=
 map2_opt
   (fun _ d o => f (Some d) o)
   (map_option (fun _ d => f (Some d) None))
   (map_option (fun _ d' => f None (Some d'))).

End Map2.

Invariants


Section Invariants.
Variable elt : Type.

Occurrence in a tree


Inductive MapsTo (x : key)(e : elt) : t elt -> Prop :=
  | MapsRoot : forall l r h y,
      X.eq x y -> MapsTo x e (Node l y e r h)
  | MapsLeft : forall l r h y e',
      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

lt_tree x s: all elements in s are smaller than x (resp. greater for gt_tree)

Definition lt_tree x m := forall y, In y m -> X.lt y x.
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 ->
     lt_tree x l -> gt_tree 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 := FMapList.Raw X.

#[local] Ltac caseq :=
match goal with [ |- context [match ?t with _ => _ end] ] =>
  let cmp := fresh in
  let H := fresh in
  remember t as cmp eqn:H; symmetry in H; destruct cmp
end.

Lemma mem_ind [elt : Type] [x : X.t] [P : t elt -> bool -> Prop] :
  (forall m : t elt, m = Leaf elt -> P (Leaf elt) false) ->
  (forall (m l : t elt) (y : key) (_x : elt) (r : t elt) (_x0 : int),
   m = Node l y _x r _x0 ->
   forall _x1 : X.lt x y,
   X.compare x y = LT _x1 -> P l (mem x l) -> P (Node l y _x r _x0) (mem x l)) ->
  (forall (m l : t elt) (y : key) (_x : elt) (r : t elt) (_x0 : int),
   m = Node l y _x r _x0 ->
   forall _x1 : X.eq x y, X.compare x y = EQ _x1 -> P (Node l y _x r _x0) true) ->
  (forall (m l : t elt) (y : key) (_x : elt) (r : t elt) (_x0 : int),
   m = Node l y _x r _x0 ->
   forall _x1 : X.lt y x,
   X.compare x y = GT _x1 -> P r (mem x r) -> P (Node l y _x r _x0) (mem x r)) ->
   forall m : t elt, P m (mem x m).

Lemma find_ind [elt : Type] [x : X.t] [P : t elt -> option elt -> Prop] :
  (forall m : t elt, m = Leaf elt -> P (Leaf elt) None) ->
  (forall (m l : t elt) (y : key) (d : elt) (r : t elt) (_x : int),
   m = Node l y d r _x ->
   forall _x0 : X.lt x y,
   X.compare x y = LT _x0 -> P l (find x l) -> P (Node l y d r _x) (find x l)) ->
  (forall (m l : t elt) (y : key) (d : elt) (r : t elt) (_x : int),
   m = Node l y d r _x ->
   forall _x0 : X.eq x y, X.compare x y = EQ _x0 -> P (Node l y d r _x) (Some d)) ->
  (forall (m l : t elt) (y : key) (d : elt) (r : t elt) (_x : int),
   m = Node l y d r _x ->
   forall _x0 : X.lt y x,
   X.compare x y = GT _x0 -> P r (find x r) -> P (Node l y d r _x) (find x r)) ->
  forall m : t elt, P m (find x m).

Lemma bal_ind [elt : Type] [P : t elt -> key -> elt -> t elt -> t elt -> Prop] :
  (forall (l : t elt) (x : key) (d : elt) (r : t elt),
   let hl := height l in
   let hr := height r in
   forall _x : hl > hr + 2,
   gt_le_dec hl (hr + 2) = left _x -> l = Leaf elt -> P (Leaf elt) x d r (assert_false l x d r)) ->
  (forall (l : t elt) (x : key) (d : elt) (r : t elt),
   let hl := height l in
   let hr := height r in
   forall _x : hl > hr + 2,
   gt_le_dec hl (hr + 2) = left _x ->
   forall (ll : t elt) (lx : key) (ld : elt) (lr : t elt) (_x0 : int),
   l = Node ll lx ld lr _x0 ->
   forall _x1 : height ll >= height lr,
   ge_lt_dec (height ll) (height lr) = left _x1 ->
   P (Node ll lx ld lr _x0) x d r (create ll lx ld (create lr x d r))) ->
  (forall (l : t elt) (x : key) (d : elt) (r : t elt),
   let hl := height l in
   let hr := height r in
   forall _x : hl > hr + 2,
   gt_le_dec hl (hr + 2) = left _x ->
   forall (ll : t elt) (lx : key) (ld : elt) (lr : t elt) (_x0 : int),
   l = Node ll lx ld lr _x0 ->
   forall _x1 : height ll < height lr,
   ge_lt_dec (height ll) (height lr) = right _x1 ->
   lr = Leaf elt -> P (Node ll lx ld (Leaf elt) _x0) x d r (assert_false l x d r)) ->
  (forall (l : t elt) (x : key) (d : elt) (r : t elt),
   let hl := height l in
   let hr := height r in
   forall _x : hl > hr + 2,
   gt_le_dec hl (hr + 2) = left _x ->
   forall (ll : t elt) (lx : key) (ld : elt) (lr : t elt) (_x0 : int),
   l = Node ll lx ld lr _x0 ->
   forall _x1 : height ll < height lr,
   ge_lt_dec (height ll) (height lr) = right _x1 ->
   forall (lrl : t elt) (lrx : key) (lrd : elt) (lrr : t elt) (_x2 : int),
   lr = Node lrl lrx lrd lrr _x2 ->
   P (Node ll lx ld (Node lrl lrx lrd lrr _x2) _x0) x d r
     (create (create ll lx ld lrl) lrx lrd (create lrr x d r))) ->
  (forall (l : t elt) (x : key) (d : elt) (r : t elt),
   let hl := height l in
   let hr := height r in
   forall _x : hl <= hr + 2,
   gt_le_dec hl (hr + 2) = right _x ->
   forall _x0 : hr > hl + 2,
   gt_le_dec hr (hl + 2) = left _x0 -> r = Leaf elt -> P l x d (Leaf elt) (assert_false l x d r)) ->
  (forall (l : t elt) (x : key) (d : elt) (r : t elt),
   let hl := height l in
   let hr := height r in
   forall _x : hl <= hr + 2,
   gt_le_dec hl (hr + 2) = right _x ->
   forall _x0 : hr > hl + 2,
   gt_le_dec hr (hl + 2) = left _x0 ->
   forall (rl : t elt) (rx : key) (rd : elt) (rr : t elt) (_x1 : int),
   r = Node rl rx rd rr _x1 ->
   forall _x2 : height rr >= height rl,
   ge_lt_dec (height rr) (height rl) = left _x2 ->
   P l x d (Node rl rx rd rr _x1) (create (create l x d rl) rx rd rr)) ->
  (forall (l : t elt) (x : key) (d : elt) (r : t elt),
   let hl := height l in
   let hr := height r in
   forall _x : hl <= hr + 2,
   gt_le_dec hl (hr + 2) = right _x ->
   forall _x0 : hr > hl + 2,
   gt_le_dec hr (hl + 2) = left _x0 ->
   forall (rl : t elt) (rx : key) (rd : elt) (rr : t elt) (_x1 : int),
   r = Node rl rx rd rr _x1 ->
   forall _x2 : height rr < height rl,
   ge_lt_dec (height rr) (height rl) = right _x2 ->
   rl = Leaf elt -> P l x d (Node (Leaf elt) rx rd rr _x1) (assert_false l x d r)) ->
  (forall (l : t elt) (x : key) (d : elt) (r : t elt),
   let hl := height l in
   let hr := height r in
   forall _x : hl <= hr + 2,
   gt_le_dec hl (hr + 2) = right _x ->
   forall _x0 : hr > hl + 2,
   gt_le_dec hr (hl + 2) = left _x0 ->
   forall (rl : t elt) (rx : key) (rd : elt) (rr : t elt) (_x1 : int),
   r = Node rl rx rd rr _x1 ->
   forall _x2 : height rr < height rl,
   ge_lt_dec (height rr) (height rl) = right _x2 ->
   forall (rll : t elt) (rlx : key) (rld : elt) (rlr : t elt) (_x3 : int),
   rl = Node rll rlx rld rlr _x3 ->
   P l x d (Node (Node rll rlx rld rlr _x3) rx rd rr _x1)
     (create (create l x d rll) rlx rld (create rlr rx rd rr))) ->
  (forall (l : t elt) (x : key) (d : elt) (r : t elt),
   let hl := height l in
   let hr := height r in
   forall _x : hl <= hr + 2,
   gt_le_dec hl (hr + 2) = right _x ->
   forall _x0 : hr <= hl + 2, gt_le_dec hr (hl + 2) = right _x0 -> P l x d r (create l x d r)) ->
  forall (l : t elt) (x : key) (d : elt) (r : t elt), P l x d r (bal l x d r).

Lemma add_ind [elt : Type] [x : key] [d : elt] [P : t elt -> t elt -> Prop] :
  (forall m : t elt, m = Leaf elt -> P (Leaf elt) (Node (Leaf elt) x d (Leaf elt) 1)) ->
  (forall (m l : t elt) (y : key) (d' : elt) (r : t elt) (h : int),
   m = Node l y d' r h ->
   forall _x : X.lt x y,
   X.compare x y = LT _x -> P l (add x d l) -> P (Node l y d' r h) (bal (add x d l) y d' r)) ->
  (forall (m l : t elt) (y : key) (d' : elt) (r : t elt) (h : int),
   m = Node l y d' r h ->
   forall _x : X.eq x y, X.compare x y = EQ _x -> P (Node l y d' r h) (Node l y d r h)) ->
  (forall (m l : t elt) (y : key) (d' : elt) (r : t elt) (h : int),
   m = Node l y d' r h ->
   forall _x : X.lt y x,
   X.compare x y = GT _x -> P r (add x d r) -> P (Node l y d' r h) (bal l y d' (add x d r))) ->
  forall m : t elt, P m (add x d m).

Lemma remove_min_ind [elt : Type] [P : t elt -> key -> elt -> t elt -> t elt * (key * elt) -> Prop] :
  (forall (l : t elt) (x : key) (d : elt) (r : t elt),
   l = Leaf elt -> P (Leaf elt) x d r (r, (x, d))) ->
  (forall (l : t elt) (x : key) (d : elt) (r ll : t elt) (lx : key)
     (ld : elt) (lr : t elt) (_x : int),
   l = Node ll lx ld lr _x ->
   P ll lx ld lr (remove_min ll lx ld lr) ->
   forall (l' : t elt) (m : key * elt),
   remove_min ll lx ld lr = (l', m) -> P (Node ll lx ld lr _x) x d r (bal l' x d r, m)) ->
  forall (l : t elt) (x : key) (d : elt) (r : t elt), P l x d r (remove_min l x d r).

Lemma merge_ind [elt : Type] [P : t elt -> t elt -> t elt -> Prop] :
  (forall s1 s2 : t elt, s1 = Leaf elt -> P (Leaf elt) s2 s2) ->
  (forall (s1 s2 _x : t elt) (_x0 : key) (_x1 : elt) (_x2 : t elt) (_x3 : int),
   s1 = Node _x _x0 _x1 _x2 _x3 -> s2 = Leaf elt -> P (Node _x _x0 _x1 _x2 _x3) (Leaf elt) s1) ->
  (forall (s1 s2 _x : t elt) (_x0 : key) (_x1 : elt) (_x2 : t elt) (_x3 : int),
   s1 = Node _x _x0 _x1 _x2 _x3 ->
   forall (l2 : t elt) (x2 : key) (d2 : elt) (r2 : t elt) (_x4 : int),
   s2 = Node l2 x2 d2 r2 _x4 ->
   forall (s2' : t elt) (p : key * elt),
   remove_min l2 x2 d2 r2 = (s2', p) ->
   forall (x : key) (d : elt),
   p = (x, d) -> P (Node _x _x0 _x1 _x2 _x3) (Node l2 x2 d2 r2 _x4) (bal s1 x d s2')) ->
  forall s1 s2 : t elt, P s1 s2 (merge s1 s2).

Lemma remove_ind [elt : Type] [x : X.t] [P : t elt -> t elt -> Prop] :
  (forall m : t elt, m = Leaf elt -> P (Leaf elt) (Leaf elt)) ->
  (forall (m l : t elt) (y : key) (d : elt) (r : t elt) (_x : int),
   m = Node l y d r _x ->
   forall _x0 : X.lt x y,
   X.compare x y = LT _x0 -> P l (remove x l) -> P (Node l y d r _x) (bal (remove x l) y d r)) ->
  (forall (m l : t elt) (y : key) (d : elt) (r : t elt) (_x : int),
   m = Node l y d r _x ->
   forall _x0 : X.eq x y, X.compare x y = EQ _x0 -> P (Node l y d r _x) (merge l r)) ->
  (forall (m l : t elt) (y : key) (d : elt) (r : t elt) (_x : int),
   m = Node l y d r _x ->
   forall _x0 : X.lt y x,
   X.compare x y = GT _x0 -> P r (remove x r) -> P (Node l y d r _x) (bal l y d (remove x r))) ->
  forall m : t elt, P m (remove x m).

Lemma concat_ind [elt : Type] [P : t elt -> t elt -> t elt -> Prop] :
  (forall m1 m2 : t elt, m1 = Leaf elt -> P (Leaf elt) m2 m2) ->
  (forall (m1 m2 _x : t elt) (_x0 : key) (_x1 : elt) (_x2 : t elt) (_x3 : int),
   m1 = Node _x _x0 _x1 _x2 _x3 -> m2 = Leaf elt -> P (Node _x _x0 _x1 _x2 _x3) (Leaf elt) m1) ->
  (forall (m1 m2 _x : t elt) (_x0 : key) (_x1 : elt) (_x2 : t elt) (_x3 : int),
   m1 = Node _x _x0 _x1 _x2 _x3 ->
   forall (l2 : t elt) (x2 : key) (d2 : elt) (r2 : t elt) (_x4 : int),
   m2 = Node l2 x2 d2 r2 _x4 ->
   forall (m2' : t elt) (xd : key * elt),
   remove_min l2 x2 d2 r2 = (m2', xd) ->
   P (Node _x _x0 _x1 _x2 _x3) (Node l2 x2 d2 r2 _x4) (join m1 xd#1 xd#2 m2')) ->
  forall m1 m2 : t elt, P m1 m2 (concat m1 m2).

Lemma split_ind [elt : Type] [x : X.t] [P : t elt -> triple elt -> Prop] :
  (forall m : t elt, m = Leaf elt -> P (Leaf elt) << Leaf elt, None, Leaf elt >>) ->
  (forall (m l : t elt) (y : key) (d : elt) (r : t elt) (_x : int),
   m = Node l y d r _x ->
   forall _x0 : X.lt x y,
   X.compare x y = LT _x0 ->
   P l (split x l) ->
   forall (ll : t elt) (o : option elt) (rl : t elt),
   split x l = << ll, o, rl >> -> P (Node l y d r _x) << ll, o, join rl y d r >>) ->
  (forall (m l : t elt) (y : key) (d : elt) (r : t elt) (_x : int),
   m = Node l y d r _x ->
   forall _x0 : X.eq x y, X.compare x y = EQ _x0 -> P (Node l y d r _x) << l, Some d, r >>) ->
  (forall (m l : t elt) (y : key) (d : elt) (r : t elt) (_x : int),
   m = Node l y d r _x ->
   forall _x0 : X.lt y x,
   X.compare x y = GT _x0 ->
   P r (split x r) ->
   forall (rl : t elt) (o : option elt) (rr : t elt),
   split x r = << rl, o, rr >> -> P (Node l y d r _x) << join l y d rl, o, rr >>) ->
  forall m : t elt, P m (split x m).

Lemma map_option_ind [elt elt' : Type] [f : key -> elt -> option elt'] [P : t elt -> t elt' -> Prop] :
  (forall m : t elt, m = Leaf elt -> P (Leaf elt) (Leaf elt')) ->
  (forall (m l : t elt) (x : key) (d : elt) (r : t elt) (_x : int),
   m = Node l x d r _x ->
   forall d' : elt',
   f x d = Some d' ->
   P l (map_option f l) ->
   P r (map_option f r) -> P (Node l x d r _x) (join (map_option f l) x d' (map_option f r))) ->
  (forall (m l : t elt) (x : key) (d : elt) (r : t elt) (_x : int),
   m = Node l x d r _x ->
   f x d = None ->
   P l (map_option f l) ->
   P r (map_option f r) -> P (Node l x d r _x) (concat (map_option f l) (map_option f r))) ->
  forall m : t elt, P m (map_option f m).

Lemma map2_opt_ind [elt elt' elt'' : Type] [f : key -> elt -> option elt' -> option elt'']
  [mapl : t elt -> t elt''] [mapr : t elt' -> t elt'']
  [P : t elt -> t elt' -> t elt'' -> Prop] :
  (forall (m1 : t elt) (m2 : t elt'), m1 = Leaf elt -> P (Leaf elt) m2 (mapr m2)) ->
  (forall (m1 : t elt) (m2 : t elt') (l1 : t elt) (x1 : key) (d1 : elt) (r1 : t elt) (_x : int),
   m1 = Node l1 x1 d1 r1 _x -> m2 = Leaf elt' -> P (Node l1 x1 d1 r1 _x) (Leaf elt') (mapl m1)) ->
  (forall (m1 : t elt) (m2 : t elt') (l1 : t elt) (x1 : key) (d1 : elt) (r1 : t elt) (_x : int),
   m1 = Node l1 x1 d1 r1 _x ->
   forall (_x0 : t elt') (_x1 : key) (_x2 : elt') (_x3 : t elt') (_x4 : int),
   m2 = Node _x0 _x1 _x2 _x3 _x4 ->
   forall (l2' : t elt') (o2 : option elt') (r2' : t elt'),
   split x1 m2 = << l2', o2, r2' >> ->
   forall e : elt'',
   f x1 d1 o2 = Some e ->
   P l1 l2' (map2_opt f mapl mapr l1 l2') ->
   P r1 r2' (map2_opt f mapl mapr r1 r2') ->
   P (Node l1 x1 d1 r1 _x) (Node _x0 _x1 _x2 _x3 _x4)
     (join (map2_opt f mapl mapr l1 l2') x1 e (map2_opt f mapl mapr r1 r2'))) ->
  (forall (m1 : t elt) (m2 : t elt') (l1 : t elt) (x1 : key) (d1 : elt) (r1 : t elt) (_x : int),
   m1 = Node l1 x1 d1 r1 _x ->
   forall (_x0 : t elt') (_x1 : key) (_x2 : elt') (_x3 : t elt') (_x4 : int),
   m2 = Node _x0 _x1 _x2 _x3 _x4 ->
   forall (l2' : t elt') (o2 : option elt') (r2' : t elt'),
   split x1 m2 = << l2', o2, r2' >> ->
   f x1 d1 o2 = None ->
   P l1 l2' (map2_opt f mapl mapr l1 l2') ->
   P r1 r2' (map2_opt f mapl mapr r1 r2') ->
   P (Node l1 x1 d1 r1 _x) (Node _x0 _x1 _x2 _x3 _x4)
     (concat (map2_opt f mapl mapr l1 l2') (map2_opt f mapl mapr r1 r2'))) ->
  forall (m1 : t elt) (m2 : t elt'), P m1 m2 (map2_opt f mapl mapr m1 m2).

Automation and dedicated tactics.


#[global]
Hint Constructors tree MapsTo In bst : core.
#[global]
Hint Unfold lt_tree gt_tree : core.

Tactic Notation "factornode" ident(l) ident(x) ident(d) ident(r) ident(h)
 "as" ident(s) :=
 set (s:=Node l x d r h) in *; clearbody s; clear l x d r h.

A tactic for cleaning hypothesis after use of functional induction.

Ltac clearf :=
 match goal with
  | H := _ |- _ => subst; subst H; clearf
  | H : (@Logic.eq (Compare _ _ _ _) _ _) |- _ => clear H; clearf
  | H : (@Logic.eq (sumbool _ _) _ _) |- _ => clear H; clearf
  | _ => idtac
 end.

A tactic to repeat inversion_clear on all hyps of the form (f (Node ...))

Ltac inv f :=
  match goal with
     | H:f (Leaf _) |- _ => inversion_clear H; inv f
     | 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.

Helper tactic concerning order of elements.

Ltac order := match goal with
 | U: lt_tree _ ?s, V: In _ ?s |- _ => generalize (U _ V); clear U; order
 | U: gt_tree _ ?s, V: In _ ?s |- _ => generalize (U _ V); clear U; order
 | _ => MX.order
end.

Ltac intuition_in := repeat (intuition auto; inv In; inv MapsTo).


Ltac join_tac :=
 intros ?l; induction l as [| ?ll _ ?lx ?ld ?lr ?Hlr ?lh];
   [ | intros ?x ?d ?r; induction r as [| ?rl ?Hrl ?rx ?rd ?rr _ ?rh]; unfold join;
     [ | destruct (gt_le_dec lh (rh+2)) as [?GT|?LE];
       [ match goal with |- context [ bal ?u ?v ?w ?z ] =>
           replace (bal u v w z)
           with (bal ll lx ld (join lr x d (Node rl rx rd rr rh))); [ | auto]
         end
       | destruct (gt_le_dec rh (lh+2)) as [?GT'|?LE'];
         [ 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.

Section Elt.
Variable elt:Type.
Implicit Types m r : t elt.

Basic results about MapsTo, In, lt_tree, gt_tree, height

Facts about MapsTo and In.

Lemma MapsTo_In : forall k e m, MapsTo k e m -> In k m.
#[local]
Hint Resolve MapsTo_In : core.

Lemma In_MapsTo : forall k m, In k m -> exists e, MapsTo k e m.

Lemma In_alt : forall k m, In0 k m <-> In k m.

Lemma MapsTo_1 :
 forall m x y e, X.eq x y -> MapsTo x e m -> MapsTo y e m.
#[local]
Hint Immediate MapsTo_1 : core.

Lemma In_1 :
 forall m x y, X.eq x y -> In x m -> In y m.

Lemma In_node_iff :
 forall l x e r h y,
  In y (Node l x e r h) <-> In y l \/ X.eq y x \/ In y r.

Results about lt_tree and gt_tree

Lemma lt_leaf : forall x, lt_tree x (Leaf elt).

Lemma gt_leaf : forall x, gt_tree x (Leaf elt).

Lemma lt_tree_node : forall x y l r e h,
 lt_tree x l -> lt_tree x r -> X.lt y x -> lt_tree x (Node l y e r h).

Lemma gt_tree_node : forall x y l r e h,
 gt_tree x l -> gt_tree x r -> X.lt x y -> gt_tree x (Node l y e r h).

#[local]
Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node : core.

Lemma lt_left : forall x y l r e h,
 lt_tree x (Node l y e r h) -> lt_tree x l.

Lemma lt_right : forall x y l r e h,
 lt_tree x (Node l y e r h) -> lt_tree x r.

Lemma gt_left : forall x y l r e h,
 gt_tree x (Node l y e r h) -> gt_tree x l.

Lemma gt_right : forall x y l r e h,
 gt_tree x (Node l y e r h) -> gt_tree x r.

#[local]
Hint Resolve lt_left lt_right gt_left gt_right : core.

Lemma lt_tree_not_in :
 forall x m, lt_tree x m -> ~ In x m.

Lemma lt_tree_trans :
 forall x y, X.lt x y -> forall m, lt_tree x m -> lt_tree y m.

Lemma gt_tree_not_in :
 forall x m, gt_tree x m -> ~ In x m.

Lemma gt_tree_trans :
 forall x y, X.lt y x -> forall m, gt_tree x m -> gt_tree y m.

#[local]
Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans : core.

Empty map


Definition Empty m := forall (a:key)(e:elt) , ~ MapsTo a e m.

Lemma empty_bst : bst (empty elt).

Lemma empty_1 : Empty (empty elt).

Emptyness test


Lemma is_empty_1 : forall m, Empty m -> is_empty m = true.

Lemma is_empty_2 : forall m, is_empty m = true -> Empty m.

Membership


Lemma mem_1 : forall m x, bst m -> In x m -> mem x m = true.

Lemma mem_2 : forall m x, mem x m = true -> In x m.

Lemma find_1 : forall m x e, bst m -> MapsTo x e m -> find x m = Some e.

Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m.

Lemma find_iff : forall m x e, bst m ->
 (find x m = Some e <-> MapsTo x e m).

Lemma find_in : forall m x, find x m <> None -> In x m.

Lemma in_find : forall m x, bst m -> In x m -> find x m <> None.

Lemma find_in_iff : forall m x, bst m ->
 (find x m <> None <-> In x m).

Lemma not_find_iff : forall m x, bst m ->
 (find x m = None <-> ~In x m).

Lemma find_find : forall m m' x,
 find x m = find x m' <->
 (forall d, find x m = Some d <-> find x m' = Some d).

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')).

Lemma find_in_equiv : forall m m' x, bst m -> bst m' ->
 find x m = find x m' ->
 (In x m <-> In x m').

Helper functions


Lemma create_bst :
 forall l x e r, bst l -> bst r -> lt_tree x l -> gt_tree x r ->
 bst (create l x e r).
#[local]
Hint Resolve create_bst : core.

Lemma create_in :
 forall l x e r y,
  In y (create l x e r) <-> X.eq y x \/ In y l \/ In y r.

Lemma bal_bst : forall l x e r, bst l -> bst r ->
 lt_tree x l -> gt_tree x r -> bst (bal l x e r).
#[local]
Hint Resolve bal_bst : core.

Lemma bal_in : forall l x e r y,
 In y (bal l x e r) <-> X.eq y x \/ In y l \/ In y r.

Lemma bal_mapsto : forall l x e r y e',
 MapsTo y e' (bal l x e r) <-> MapsTo y e' (create l x e r).

Lemma bal_find : forall l x e r y,
 bst l -> bst r -> lt_tree x l -> gt_tree x r ->
 find y (bal l x e r) = find y (create l x e r).

Insertion


Lemma add_in : forall m x y e,
 In y (add x e m) <-> X.eq y x \/ In y m.

Lemma add_bst : forall m x e, bst m -> bst (add x e m).
#[local]
Hint Resolve add_bst : core.

Lemma add_1 : forall m x y e, X.eq x y -> MapsTo y e (add x e m).

Lemma add_2 : forall m x y e e', ~X.eq x y ->
 MapsTo y e m -> MapsTo y e (add x e' m).

Lemma add_3 : forall m x y e e', ~X.eq x y ->
 MapsTo y e (add x e' m) -> MapsTo y e m.

Lemma add_find : forall m x y e, bst m ->
 find y (add x e m) =
  match X.compare y x with EQ _ => Some e | _ => find y m end.

Extraction of minimum binding


Lemma remove_min_in : forall l x e r h y,
 In y (Node l x e r h) <->
  X.eq y (remove_min l x e r)#2#1 \/ In y (remove_min l x e r)#1.

Lemma remove_min_mapsto : forall l x e r h y e',
  MapsTo y e' (Node l x e r h) <->
   ((X.eq y (remove_min l x e r)#2#1) /\ e' = (remove_min l x e r)#2#2)
    \/ MapsTo y e' (remove_min l x e r)#1.

Lemma remove_min_bst : forall l x e r h,
 bst (Node l x e r h) -> bst (remove_min l x e r)#1.
#[local]
Hint Resolve remove_min_bst : core.

Lemma remove_min_gt_tree : forall l x e r h,
 bst (Node l x e r h) ->
 gt_tree (remove_min l x e r)#2#1 (remove_min l x e r)#1.
#[local]
Hint Resolve remove_min_gt_tree : core.

Lemma remove_min_find : forall l x e r h y,
 bst (Node l x e r h) ->
 find y (Node l x e r h) =
   match X.compare y (remove_min l x e r)#2#1 with
    | LT _ => None
    | EQ _ => Some (remove_min l x e r)#2#2
    | GT _ => find y (remove_min l x e r)#1
   end.

Merging two trees


Lemma merge_in : forall m1 m2 y, bst m1 -> bst m2 ->
 (In y (merge m1 m2) <-> In y m1 \/ In y m2).

Lemma merge_mapsto : forall m1 m2 y e, bst m1 -> bst m2 ->
  (MapsTo y e (merge m1 m2) <-> MapsTo y e m1 \/ MapsTo y e m2).

Lemma merge_bst : forall m1 m2, bst m1 -> bst m2 ->
 (forall y1 y2 : key, In y1 m1 -> In y2 m2 -> X.lt y1 y2) ->
 bst (merge m1 m2).

Deletion


Lemma remove_in : forall m x y, bst m ->
 (In y (remove x m) <-> ~ X.eq y x /\ In y m).

Lemma remove_bst : forall m x, bst m -> bst (remove x m).

Lemma remove_1 : forall m x y, bst m -> X.eq x y -> ~ In y (remove x m).

Lemma remove_2 : forall m x y e, bst m -> ~X.eq x y ->
 MapsTo y e m -> MapsTo y e (remove x m).

Lemma remove_3 : forall m x y e, bst m ->
 MapsTo y e (remove x m) -> MapsTo y e m.

join


Lemma join_in : forall l x d r y,
 In y (join l x d r) <-> X.eq y x \/ In y l \/ In y r.

Lemma join_bst : forall l x d r, bst l -> bst r ->
 lt_tree x l -> gt_tree x r -> bst (join l x d r).
#[local]
Hint Resolve join_bst : core.

Lemma join_find : forall l x d r y,
 bst l -> bst r -> lt_tree x l -> gt_tree x r ->
 find y (join l x d r) = find y (create l x d r).

split


Lemma split_in_1 : forall m x, bst m -> forall y,
 (In y (split x m)#l <-> In y m /\ X.lt y x).

Lemma split_in_2 : forall m x, bst m -> forall y,
 (In y (split x m)#r <-> In y m /\ X.lt x y).

Lemma split_in_3 : forall m x, bst m ->
 (split x m)#o = find x m.

Lemma split_bst : forall m x, bst m ->
 bst (split x m)#l /\ bst (split x m)#r.

Lemma split_lt_tree : forall m x, bst m -> lt_tree x (split x m)#l.

Lemma split_gt_tree : forall m x, bst m -> gt_tree x (split x m)#r.

Lemma split_find : forall m x y, bst m ->
 find y m = match X.compare y x with
              | LT _ => find y (split x m)#l
              | EQ _ => (split x m)#o
              | GT _ => find y (split x m)#r
            end.

Concatenation


Lemma concat_in : forall m1 m2 y,
 In y (concat m1 m2) <-> In y m1 \/ In y m2.

Lemma concat_bst : forall m1 m2, bst m1 -> bst m2 ->
 (forall y1 y2, In y1 m1 -> In y2 m2 -> X.lt y1 y2) ->
 bst (concat m1 m2).
#[local]
Hint Resolve concat_bst : core.

Lemma concat_find : forall m1 m2 y, bst m1 -> bst m2 ->
 (forall y1 y2, In y1 m1 -> In y2 m2 -> X.lt y1 y2) ->
 find y (concat m1 m2) =
  match find y m2 with Some d => Some d | None => find y m1 end.

Elements


Notation eqk := (PX.eqk (elt:= elt)).
Notation eqke := (PX.eqke (elt:= elt)).
Notation ltk := (PX.ltk (elt:= elt)).

Lemma elements_aux_mapsto : forall (s:t elt) acc x e,
 InA eqke (x,e) (elements_aux acc s) <-> MapsTo x e s \/ InA eqke (x,e) acc.

Lemma elements_mapsto : forall (s:t elt) x e, InA eqke (x,e) (elements s) <-> MapsTo x e s.

Lemma elements_in : forall (s:t elt) x, L.PX.In x (elements s) <-> In x s.

Lemma elements_aux_sort : forall (s:t elt) acc, bst s -> sort ltk acc ->
 (forall x e y, InA eqke (x,e) acc -> In y s -> X.lt y x) ->
 sort ltk (elements_aux acc s).

Lemma elements_sort : forall s : t elt, bst s -> sort ltk (elements s).
#[local]
Hint Resolve elements_sort : core.

Lemma elements_nodup : forall s : t elt, bst s -> NoDupA eqk (elements s).

Lemma elements_aux_cardinal :
 forall (m:t elt) acc, (length acc + cardinal m)%nat = length (elements_aux acc m).

Lemma elements_cardinal : forall (m:t elt), cardinal m = length (elements m).

Lemma elements_app :
 forall (s:t elt) acc, elements_aux acc s = elements s ++ acc.

Lemma elements_node :
 forall (t1 t2:t elt) x e z l,
 elements t1 ++ (x,e) :: elements t2 ++ l =
 elements (Node t1 x e t2 z) ++ l.

Fold


Definition fold' (A : Type) (f : key -> elt -> A -> A)(s : t elt) :=
  L.fold f (elements s).

Lemma fold_equiv_aux :
 forall (A : Type) (s : t elt) (f : key -> elt -> A -> A) (a : A) acc,
 L.fold f (elements_aux acc s) a = L.fold f acc (fold f s a).

Lemma fold_equiv :
 forall (A : Type) (s : t elt) (f : key -> elt -> A -> A) (a : A),
 fold f s a = fold' f s a.

Lemma fold_1 :
 forall (s:t elt)(Hs:bst s)(A : Type)(i:A)(f : key -> elt -> A -> A),
 fold f s i = fold_left (fun a p => f p#1 p#2 a) (elements s) i.

Comparison

flatten_e e returns the list of elements of the enumeration e i.e. the list of elements actually compared

Fixpoint flatten_e (e : enumeration elt) : list (key*elt) := match e with
  | End _ => nil
  | More x e t r => (x,e) :: elements t ++ flatten_e r
 end.

Lemma flatten_e_elements :
 forall (l:t elt) r x d z e,
 elements l ++ flatten_e (More x d r e) =
 elements (Node l x d r z) ++ flatten_e e.

Lemma cons_1 : forall (s:t elt) e,
  flatten_e (cons s e) = elements s ++ flatten_e e.

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).

Lemma equal_end_IfEq : forall e2,
  IfEq (equal_end e2) nil (flatten_e e2).

Lemma equal_more_IfEq :
 forall x1 d1 (cont:enumeration elt -> bool) x2 d2 r2 e2 l,
  IfEq (cont (cons r2 e2)) l (elements r2 ++ flatten_e e2) ->
    IfEq (equal_more cmp x1 d1 cont (More x2 d2 r2 e2)) ((x1,d1)::l)
       (flatten_e (More x2 d2 r2 e2)).

Lemma equal_cont_IfEq : forall m1 cont e2 l,
  (forall e, IfEq (cont e) l (flatten_e e)) ->
  IfEq (equal_cont cmp m1 cont e2) (elements m1 ++ l) (flatten_e e2).

Lemma equal_IfEq : forall (m1 m2:t elt),
  IfEq (equal cmp m1 m2) (elements m1) (elements m2).

Definition Equivb m m' :=
  (forall k, In k m <-> In k m') /\
  (forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true).

Lemma Equivb_elements : forall s s',
 Equivb s s' <-> L.Equivb cmp (elements s) (elements s').

Lemma equal_Equivb : forall (s s': t elt), bst s -> bst s' ->
  (equal cmp s s' = true <-> Equivb s s').

End Elt.

Section Map.
Variable elt elt' : Type.
Variable f : elt -> elt'.

Lemma map_1 : forall (m: t elt)(x:key)(e:elt),
    MapsTo x e m -> MapsTo x (f e) (map f m).

Lemma map_2 : forall (m: t elt)(x:key),
    In x (map f m) -> In x m.

Lemma map_bst : forall m, bst m -> bst (map f m).

End Map.
Section Mapi.
Variable elt elt' : Type.
Variable f : key -> elt -> elt'.

Lemma mapi_1 : forall (m: tree elt)(x:key)(e:elt),
    MapsTo x e m -> exists y, X.eq y x /\ MapsTo x (f y e) (mapi f m).

Lemma mapi_2 : forall (m: t elt)(x:key),
    In x (mapi f m) -> In x m.

Lemma mapi_bst : forall m, bst m -> bst (mapi f m).

End Mapi.

Section Map_option.
Variable elt elt' : Type.
Variable f : key -> elt -> option elt'.
Hypothesis f_compat : forall x x' d, X.eq x x' -> f x d = f x' d.

Lemma map_option_2 : forall (m:t elt)(x:key),
 In x (map_option f m) -> exists d, MapsTo x d m /\ f x d <> None.

Lemma map_option_bst : forall m, bst m -> bst (map_option f m).
#[local]
Hint Resolve map_option_bst : core.

Ltac nonify e :=
 replace e with (@None elt) by
  (symmetry; rewrite not_find_iff; auto; intro; order).

Lemma map_option_find : forall (m:t elt)(x:key),
 bst m ->
 find x (map_option f m) =
  match (find x m) with Some d => f x d | None => None end.

End Map_option.

Section Map2_opt.
Variable elt elt' elt'' : Type.
Variable f0 : key -> option elt -> option elt' -> option elt''.
Variable f : key -> elt -> option elt' -> option elt''.
Variable mapl : t elt -> t elt''.
Variable mapr : t elt' -> t elt''.
Hypothesis f0_f : forall x d o, f x d o = f0 x (Some d) o.
Hypothesis mapl_bst : forall m, bst m -> bst (mapl m).
Hypothesis mapr_bst : forall m', bst m' -> bst (mapr m').
Hypothesis mapl_f0 : forall x m, bst m ->
 find x (mapl m) =
  match find x m with Some d => f0 x (Some d) None | None => None end.
Hypothesis mapr_f0 : forall x m', bst m' ->
 find x (mapr m') =
  match find x m' with Some d' => f0 x None (Some d') | None => None end.
Hypothesis f0_compat : forall x x' o o', X.eq x x' -> f0 x o o' = f0 x' o o'.

Notation map2_opt := (map2_opt f mapl mapr).

Lemma map2_opt_2 : forall m m' y, bst m -> bst m' ->
  In y (map2_opt m m') -> In y m \/ In y m'.

Lemma map2_opt_bst : forall m m', bst m -> bst m' ->
 bst (map2_opt m m').
#[local]
Hint Resolve map2_opt_bst : core.

Ltac map2_aux :=
 match goal with
  | H : In ?x _ \/ In ?x ?m,
    H' : find ?x ?m = find ?x ?m', B:bst ?m, B':bst ?m' |- _ =>
    destruct H; [ intuition_in; order |
                  rewrite <-(find_in_equiv B B' H'); auto ]
 end.

Ltac nonify t :=
 match t with (find ?y (map2_opt ?m ?m')) =>
 replace t with (@None elt'');
 [ | symmetry; rewrite not_find_iff; auto; intro;
     destruct (@map2_opt_2 m m' y); auto; order ]
 end.

Lemma map2_opt_1 : forall m m' y, bst m -> bst m' ->
 In y m \/ In y m' ->
 find y (map2_opt m m') = f0 y (find y m) (find y m').

End Map2_opt.

Section Map2.
Variable elt elt' elt'' : Type.
Variable f : option elt -> option elt' -> option elt''.

Lemma map2_bst : forall m m', bst m -> bst m' -> bst (map2 f m m').

Lemma map2_1 : forall m m' y, bst m -> bst m' ->
  In y m \/ In y m' -> find y (map2 f m m') = f (find y m) (find y m').

Lemma map2_2 : forall m m' y, bst m -> bst m' ->
  In y (map2 f m m') -> In y m \/ In y m'.

End Map2.
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.

 #[universes(template)]
 Record bst (elt:Type) :=
  Bst {this :> Raw.tree elt; is_bst : Raw.bst this}.

 Definition t := bst.
 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 := Bst (empty_bst elt).
 Definition is_empty m : bool := Raw.is_empty (this m).
 Definition add x e m : t elt := Bst (add_bst x e (is_bst m)).
 Definition remove x m : t elt := Bst (remove_bst x (is_bst m)).
 Definition mem x m : bool := Raw.mem x (this m).
 Definition find x m : option elt := Raw.find x (this m).
 Definition map f m : t elt' := Bst (map_bst f (is_bst m)).
 Definition mapi (f:key->elt->elt') m : t elt' :=
  Bst (mapi_bst f (is_bst m)).
 Definition map2 f m (m':t elt') : t elt'' :=
  Bst (map2_bst f (is_bst m) (is_bst m')).
 Definition elements m : list (key*elt) := Raw.elements (this m).
 Definition cardinal m := Raw.cardinal (this m).
 Definition fold (A:Type) (f:key->elt->A->A) m i := Raw.fold (A:=A) f (this m) i.
 Definition equal cmp m m' : bool := Raw.equal cmp (this m) (this m').

 Definition MapsTo x e m : Prop := Raw.MapsTo x e (this m).
 Definition In x m : Prop := Raw.In0 x (this m).
 Definition Empty m : Prop := Empty (this m).

 Definition eq_key : (key*elt) -> (key*elt) -> Prop := @PX.eqk elt.
 Definition eq_key_elt : (key*elt) -> (key*elt) -> Prop := @PX.eqke elt.
 Definition lt_key : (key*elt) -> (key*elt) -> Prop := @PX.ltk elt.

 Lemma MapsTo_1 : forall m x y e, E.eq x y -> MapsTo x e m -> MapsTo y e m.

 Lemma mem_1 : forall m x, In x m -> mem x m = true.

 Lemma mem_2 : forall m x, mem x m = true -> In x m.

 Lemma empty_1 : Empty empty.

 Lemma is_empty_1 : forall m, Empty m -> is_empty m = true.
 Lemma is_empty_2 : forall m, is_empty m = true -> Empty m.

 Lemma add_1 : forall m x y e, E.eq x y -> MapsTo y e (add x e m).
 Lemma add_2 : forall m x y e e', ~ E.eq x y -> MapsTo y e m -> MapsTo y e (add x e' m).
 Lemma add_3 : forall m x y e e', ~ E.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m.

 Lemma remove_1 : forall m x y, E.eq x y -> ~ In y (remove x m).
 Lemma remove_2 : forall m x y e, ~ E.eq x y -> MapsTo y e m -> MapsTo y e (remove x m).
 Lemma remove_3 : forall m x y e, MapsTo y e (remove x m) -> MapsTo y e m.

 Lemma find_1 : forall m x e, MapsTo x e m -> find x m = Some e.
 Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m.

 Lemma fold_1 : forall m (A : Type) (i : A) (f : key -> elt -> A -> A),
        fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.

 Lemma elements_1 : forall m x e,
   MapsTo x e m -> InA eq_key_elt (x,e) (elements m).

 Lemma elements_2 : forall m x e,
   InA eq_key_elt (x,e) (elements m) -> MapsTo x e m.

 Lemma elements_3 : forall m, sort lt_key (elements m).

 Lemma elements_3w : forall m, NoDupA eq_key (elements m).

 Lemma cardinal_1 : forall m, cardinal m = length (elements m).

 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 : forall cmp m m',
  Equivb cmp m m' <-> Raw.Proofs.Equivb cmp m m'.

 Lemma equal_1 : forall m m' cmp,
   Equivb cmp m m' -> equal cmp m m' = true.

 Lemma equal_2 : forall m m' cmp,
   equal cmp m m' = true -> Equivb cmp m m'.

 End Elt.

 Lemma map_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)(f:elt->elt'),
        MapsTo x e m -> MapsTo x (f e) (map f m).

 Lemma map_2 : forall (elt elt':Type)(m:t elt)(x:key)(f:elt->elt'), In x (map f m) -> In x m.

 Lemma mapi_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)
        (f:key->elt->elt'), MapsTo x e m ->
        exists y, E.eq y x /\ MapsTo x (f y e) (mapi f m).
 Lemma mapi_2 : forall (elt elt':Type)(m: t elt)(x:key)
        (f:key->elt->elt'), In x (mapi f m) -> In x m.

 Lemma map2_1 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt')
    (x:key)(f:option elt->option elt'->option elt''),
    In x m \/ In x m' ->
    find x (map2 f m m') = f (find x m) (find x m').

 Lemma map2_2 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt')
     (x:key)(f:option elt->option elt'->option elt''),
     In x (map2 f m m') -> In x m \/ In x m'.

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 := FMapList.Make_ord(X)(D).
  Module R := Raw.
  Module P := Raw.Proofs.

  Definition t := MapS.t D.t.

  Definition cmp e e' :=
   match D.compare e e' with EQ _ => true | _ => false end.

One step of comparison of elements

  Definition compare_more x1 d1 (cont:R.enumeration D.t -> comparison) e2 :=
   match e2 with
    | R.End _ => Gt
    | R.More x2 d2 r2 e2 =>
       match X.compare x1 x2 with
        | EQ _ => match D.compare d1 d2 with
                   | EQ _ => cont (R.cons r2 e2)
                   | LT _ => Lt
                   | GT _ => Gt
                  end
        | LT _ => Lt
        | GT _ => Gt
       end
   end.

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_pure s1 s2 :=
   compare_cont s1 compare_end (R.cons s2 (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 : forall c x1 x2 d1 d2 l1 l2,
   X.eq x1 x2 -> D.eq d1 d2 ->
   Cmp c l1 l2 -> Cmp c ((x1,d1)::l1) ((x2,d2)::l2).
  #[global]
  Hint Resolve cons_Cmp : core.

  Lemma compare_end_Cmp :
   forall e2, Cmp (compare_end e2) nil (P.flatten_e e2).

  Lemma compare_more_Cmp : forall x1 d1 cont x2 d2 r2 e2 l,
    Cmp (cont (R.cons r2 e2)) l (R.elements r2 ++ P.flatten_e e2) ->
     Cmp (compare_more x1 d1 cont (R.More x2 d2 r2 e2)) ((x1,d1)::l)
       (P.flatten_e (R.More x2 d2 r2 e2)).

  Lemma compare_cont_Cmp : forall s1 cont e2 l,
   (forall e, Cmp (cont e) l (P.flatten_e e)) ->
   Cmp (compare_cont s1 cont e2) (R.elements s1 ++ l) (P.flatten_e e2).

  Lemma compare_Cmp : forall s1 s2,
   Cmp (compare_pure s1 s2) (R.elements s1) (R.elements s2).

The dependent-style compare

  Definition eq (m1 m2 : t) := LO.eq_list (elements m1) (elements m2).
  Definition lt (m1 m2 : t) := LO.lt_list (elements m1) (elements m2).

  Definition compare (s s':t) : Compare lt eq s s'.


  Definition selements (m1 : t) :=
   LO.MapS.Build_slist (P.elements_sort (is_bst m1)).

  Definition seq (m1 m2 : t) := LO.eq (selements m1) (selements m2).
  Definition slt (m1 m2 : t) := LO.lt (selements m1) (selements m2).

  Lemma eq_seq : forall m1 m2, eq m1 m2 <-> seq m1 m2.

  Lemma lt_slt : forall m1 m2, lt m1 m2 <-> slt m1 m2.

  Lemma eq_1 : forall (m m' : t), Equivb cmp m m' -> eq m m'.

  Lemma eq_2 : forall m m', eq m m' -> Equivb cmp m m'.

  Lemma eq_refl : forall m : t, eq m m.

  Lemma eq_sym : forall m1 m2 : t, eq m1 m2 -> eq m2 m1.

  Lemma eq_trans : forall m1 m2 m3 : t, eq m1 m2 -> eq m2 m3 -> eq m1 m3.

  Lemma lt_trans : forall m1 m2 m3 : t, lt m1 m2 -> lt m2 m3 -> lt m1 m3.

  Lemma lt_not_eq : forall m1 m2 : t, lt m1 m2 -> ~ eq m1 m2.

End IntMake_ord.


Module Make (X: OrderedType) <: S with Module E := X
 :=IntMake(Z_as_Int)(X).

Module Make_ord (X: OrderedType)(D: OrderedType)
 <: Sord with Module Data := D
            with Module MapS.E := X
 :=IntMake_ord(Z_as_Int)(X)(D).