# Library Maps

``` ```
Applicative finite maps are the main data structure used in this project. A finite map associates data to keys. The two main operations are `set k d m`, which returns a map identical to `m` except that `d` is associated to `k`, and `get k m` which returns the data associated to key `k` in map `m`. In this library, we distinguish two kinds of maps:
• Trees: the `get` operation returns an option type, either `None` if no data is associated to the key, or `Some d` otherwise.
• Maps: the `get` operation always returns a data. If no data was explicitly associated with the key, a default data provided at map initialization time is returned.

In this library, we provide efficient implementations of trees and maps whose keys range over the type `positive` of binary positive integers or any type that can be injected into `positive`. The implementation is based on radix-2 search trees (uncompressed Patricia trees) and guarantees logarithmic-time operations. An inefficient implementation of maps as functions is also provided.
``` Require Import Coqlib. Set Implicit Arguments. ```

# The abstract signatures of trees

``` Module Type TREE.   Variable elt: Type.   Variable elt_eq: forall (a b: elt), {a = b} + {a <> b}.   Variable t: Type -> Type.   Variable eq: forall (A: Type), (forall (x y: A), {x=y} + {x<>y}) ->                 forall (a b: t A), {a = b} + {a <> b}.   Variable empty: forall (A: Type), t A.   Variable get: forall (A: Type), elt -> t A -> option A.   Variable set: forall (A: Type), elt -> A -> t A -> t A.   Variable remove: forall (A: Type), elt -> t A -> t A. ```
The ``good variables'' properties for trees, expressing commutations between `get`, `set` and `remove`.
```   Hypothesis gempty:     forall (A: Type) (i: elt), get i (empty A) = None.   Hypothesis gss:     forall (A: Type) (i: elt) (x: A) (m: t A), get i (set i x m) = Some x.   Hypothesis gso:     forall (A: Type) (i j: elt) (x: A) (m: t A),     i <> j -> get i (set j x m) = get i m.   Hypothesis gsspec:     forall (A: Type) (i j: elt) (x: A) (m: t A),     get i (set j x m) = if elt_eq i j then Some x else get i m.   Hypothesis gsident:     forall (A: Type) (i: elt) (m: t A) (v: A),     get i m = Some v -> set i v m = m.   Hypothesis grs:     forall (A: Type) (i: elt) (m: t A), get i (remove i m) = None.   Hypothesis gro:     forall (A: Type) (i j: elt) (m: t A),     i <> j -> get i (remove j m) = get i m.   Hypothesis grspec:     forall (A: Type) (i j: elt) (m: t A),     get i (remove j m) = if elt_eq i j then None else get i m. ```
Extensional equality between trees.
```   Variable beq: forall (A: Type), (A -> A -> bool) -> t A -> t A -> bool.   Hypothesis beq_correct:     forall (A: Type) (P: A -> A -> Prop) (cmp: A -> A -> bool),     (forall (x y: A), cmp x y = true -> P x y) ->     forall (t1 t2: t A), beq cmp t1 t2 = true ->     forall (x: elt),     match get x t1, get x t2 with     | None, None => True     | Some y1, Some y2 => P y1 y2     | _, _ => False     end. ```
Applying a function to all data of a tree.
```   Variable map:     forall (A B: Type), (elt -> A -> B) -> t A -> t B.   Hypothesis gmap:     forall (A B: Type) (f: elt -> A -> B) (i: elt) (m: t A),     get i (map f m) = option_map (f i) (get i m). ```
Applying a function pairwise to all data of two trees.
```   Variable combine:     forall (A: Type), (option A -> option A -> option A) -> t A -> t A -> t A.   Hypothesis gcombine:     forall (A: Type) (f: option A -> option A -> option A),     f None None = None ->     forall (m1 m2: t A) (i: elt),     get i (combine f m1 m2) = f (get i m1) (get i m2).   Hypothesis combine_commut:     forall (A: Type) (f g: option A -> option A -> option A),     (forall (i j: option A), f i j = g j i) ->     forall (m1 m2: t A),     combine f m1 m2 = combine g m2 m1. ```
Enumerating the bindings of a tree.
```   Variable elements:     forall (A: Type), t A -> list (elt * A).   Hypothesis elements_correct:     forall (A: Type) (m: t A) (i: elt) (v: A),     get i m = Some v -> In (i, v) (elements m).   Hypothesis elements_complete:     forall (A: Type) (m: t A) (i: elt) (v: A),     In (i, v) (elements m) -> get i m = Some v.   Hypothesis elements_keys_norepet:     forall (A: Type) (m: t A),     list_norepet (List.map (@fst elt A) (elements m)). ```
Folding a function over all bindings of a tree.
```   Variable fold:     forall (A B: Type), (B -> elt -> A -> B) -> t A -> B -> B.   Hypothesis fold_spec:     forall (A B: Type) (f: B -> elt -> A -> B) (v: B) (m: t A),     fold f m v =     List.fold_left (fun a p => f a (fst p) (snd p)) (elements m) v. End TREE. ```

# The abstract signatures of maps

``` Module Type MAP.   Variable elt: Type.   Variable elt_eq: forall (a b: elt), {a = b} + {a <> b}.   Variable t: Type -> Type.   Variable init: forall (A: Type), A -> t A.   Variable get: forall (A: Type), elt -> t A -> A.   Variable set: forall (A: Type), elt -> A -> t A -> t A.   Hypothesis gi:     forall (A: Type) (i: elt) (x: A), get i (init x) = x.   Hypothesis gss:     forall (A: Type) (i: elt) (x: A) (m: t A), get i (set i x m) = x.   Hypothesis gso:     forall (A: Type) (i j: elt) (x: A) (m: t A),     i <> j -> get i (set j x m) = get i m.   Hypothesis gsspec:     forall (A: Type) (i j: elt) (x: A) (m: t A),     get i (set j x m) = if elt_eq i j then x else get i m.   Hypothesis gsident:     forall (A: Type) (i j: elt) (m: t A), get j (set i (get i m) m) = get j m.   Variable map: forall (A B: Type), (A -> B) -> t A -> t B.   Hypothesis gmap:     forall (A B: Type) (f: A -> B) (i: elt) (m: t A),     get i (map f m) = f(get i m). End MAP. ```

# An implementation of trees over type `positive`

``` Module PTree <: TREE.   Definition elt := positive.   Definition elt_eq := peq.   Inductive tree (A : Type) : Type :=     | Leaf : tree A     | Node : tree A -> option A -> tree A -> tree A   .   Implicit Arguments Leaf [A].   Implicit Arguments Node [A].   Definition t := tree.   Theorem eq : forall (A : Type),     (forall (x y: A), {x=y} + {x<>y}) ->     forall (a b : t A), {a = b} + {a <> b}.      Definition empty (A : Type) := (Leaf : t A).   Fixpoint get (A : Type) (i : positive) (m : t A) {struct i} : option A :=     match m with     | Leaf => None     | Node l o r =>         match i with         | xH => o         | xO ii => get ii l         | xI ii => get ii r         end     end.   Fixpoint set (A : Type) (i : positive) (v : A) (m : t A) {struct i} : t A :=     match m with     | Leaf =>         match i with         | xH => Node Leaf (Some v) Leaf         | xO ii => Node (set ii v Leaf) None Leaf         | xI ii => Node Leaf None (set ii v Leaf)         end     | Node l o r =>         match i with         | xH => Node l (Some v) r         | xO ii => Node (set ii v l) o r         | xI ii => Node l o (set ii v r)         end     end.   Fixpoint remove (A : Type) (i : positive) (m : t A) {struct i} : t A :=     match i with     | xH =>         match m with         | Leaf => Leaf         | Node Leaf o Leaf => Leaf         | Node l o r => Node l None r         end     | xO ii =>         match m with         | Leaf => Leaf         | Node l None Leaf =>             match remove ii l with             | Leaf => Leaf             | mm => Node mm None Leaf             end         | Node l o r => Node (remove ii l) o r         end     | xI ii =>         match m with         | Leaf => Leaf         | Node Leaf None r =>             match remove ii r with             | Leaf => Leaf             | mm => Node Leaf None mm             end         | Node l o r => Node l o (remove ii r)         end     end.   Theorem gempty:     forall (A: Type) (i: positive), get i (empty A) = None.      Theorem gss:     forall (A: Type) (i: positive) (x: A) (m: t A), get i (set i x m) = Some x.        Lemma gleaf : forall (A : Type) (i : positive), get i (Leaf : t A) = None.        Theorem gso:     forall (A: Type) (i j: positive) (x: A) (m: t A),     i <> j -> get i (set j x m) = get i m.      Theorem gsspec:     forall (A: Type) (i j: positive) (x: A) (m: t A),     get i (set j x m) = if peq i j then Some x else get i m.      Theorem gsident:     forall (A: Type) (i: positive) (m: t A) (v: A),     get i m = Some v -> set i v m = m.        Lemma rleaf : forall (A : Type) (i : positive), remove i (Leaf : t A) = Leaf.        Theorem grs:     forall (A: Type) (i: positive) (m: t A), get i (remove i m) = None.      Theorem gro:     forall (A: Type) (i j: positive) (m: t A),     i <> j -> get i (remove j m) = get i m.      Theorem grspec:     forall (A: Type) (i j: elt) (m: t A),     get i (remove j m) = if elt_eq i j then None else get i m.      Section EXTENSIONAL_EQUALITY.     Variable A: Type.     Variable eqA: A -> A -> Prop.     Variable beqA: A -> A -> bool.     Hypothesis beqA_correct: forall x y, beqA x y = true -> eqA x y.     Definition exteq (m1 m2: t A) : Prop :=       forall (x: elt),       match get x m1, get x m2 with       | None, None => True       | Some y1, Some y2 => eqA y1 y2       | _, _ => False       end.     Fixpoint bempty (m: t A) : bool :=       match m with       | Leaf => true       | Node l None r => bempty l && bempty r       | Node l (Some _) r => false       end.     Lemma bempty_correct:       forall m, bempty m = true -> forall x, get x m = None.          Fixpoint beq (m1 m2: t A) {struct m1} : bool :=       match m1, m2 with       | Leaf, _ => bempty m2       | _, Leaf => bempty m1       | Node l1 o1 r1, Node l2 o2 r2 =>           match o1, o2 with           | None, None => true           | Some y1, Some y2 => beqA y1 y2           | _, _ => false           end           && beq l1 l2 && beq r1 r2       end.     Lemma beq_correct:       forall m1 m2, beq m1 m2 = true -> exteq m1 m2.        End EXTENSIONAL_EQUALITY.     Fixpoint append (i j : positive) {struct i} : positive :=       match i with       | xH => j       | xI ii => xI (append ii j)       | xO ii => xO (append ii j)       end.     Lemma append_assoc_0 : forall (i j : positive),                            append i (xO j) = append (append i (xO xH)) j.          Lemma append_assoc_1 : forall (i j : positive),                            append i (xI j) = append (append i (xI xH)) j.          Lemma append_neutral_r : forall (i : positive), append i xH = i.          Lemma append_neutral_l : forall (i : positive), append xH i = i.          Fixpoint xmap (A B : Type) (f : positive -> A -> B) (m : t A) (i : positive)              {struct m} : t B :=       match m with       | Leaf => Leaf       | Node l o r => Node (xmap f l (append i (xO xH)))                            (option_map (f i) o)                            (xmap f r (append i (xI xH)))       end.   Definition map (A B : Type) (f : positive -> A -> B) m := xmap f m xH.     Lemma xgmap:       forall (A B: Type) (f: positive -> A -> B) (i j : positive) (m: t A),       get i (xmap f m j) = option_map (f (append j i)) (get i m).        Theorem gmap:     forall (A B: Type) (f: positive -> A -> B) (i: positive) (m: t A),     get i (map f m) = option_map (f i) (get i m).      Definition Node' (A: Type) (l: t A) (x: option A) (r: t A): t A :=     match l, x, r with     | Leaf, None, Leaf => Leaf     | _, _, _ => Node l x r     end.   Lemma gnode':     forall (A: Type) (l r: t A) (x: option A) (i: positive),     get i (Node' l x r) = get i (Node l x r).      Section COMBINE.   Variable A: Type.   Variable f: option A -> option A -> option A.   Hypothesis f_none_none: f None None = None.   Fixpoint xcombine_l (m : t A) {struct m} : t A :=       match m with       | Leaf => Leaf       | Node l o r => Node' (xcombine_l l) (f o None) (xcombine_l r)       end.   Lemma xgcombine_l :           forall (m: t A) (i : positive),           get i (xcombine_l m) = f (get i m) None.        Fixpoint xcombine_r (m : t A) {struct m} : t A :=       match m with       | Leaf => Leaf       | Node l o r => Node' (xcombine_r l) (f None o) (xcombine_r r)       end.   Lemma xgcombine_r :           forall (m: t A) (i : positive),           get i (xcombine_r m) = f None (get i m).        Fixpoint combine (m1 m2 : t A) {struct m1} : t A :=     match m1 with     | Leaf => xcombine_r m2     | Node l1 o1 r1 =>         match m2 with         | Leaf => xcombine_l m1         | Node l2 o2 r2 => Node' (combine l1 l2) (f o1 o2) (combine r1 r2)         end     end.   Theorem gcombine:       forall (m1 m2: t A) (i: positive),       get i (combine m1 m2) = f (get i m1) (get i m2).      End COMBINE.   Lemma xcombine_lr :     forall (A : Type) (f g : option A -> option A -> option A) (m : t A),     (forall (i j : option A), f i j = g j i) ->     xcombine_l f m = xcombine_r g m.        Theorem combine_commut:     forall (A: Type) (f g: option A -> option A -> option A),     (forall (i j: option A), f i j = g j i) ->     forall (m1 m2: t A),     combine f m1 m2 = combine g m2 m1.        Fixpoint xelements (A : Type) (m : t A) (i : positive) {struct m}              : list (positive * A) :=       match m with       | Leaf => nil       | Node l None r =>           (xelements l (append i (xO xH))) ++ (xelements r (append i (xI xH)))       | Node l (Some x) r =>           (xelements l (append i (xO xH)))           ++ ((i, x) :: xelements r (append i (xI xH)))       end.   Definition elements A (m : t A) := xelements m xH.     Lemma xelements_correct:       forall (A: Type) (m: t A) (i j : positive) (v: A),       get i m = Some v -> In (append j i, v) (xelements m j).        Theorem elements_correct:     forall (A: Type) (m: t A) (i: positive) (v: A),     get i m = Some v -> In (i, v) (elements m).        Fixpoint xget (A : Type) (i j : positive) (m : t A) {struct j} : option A :=       match i, j with       | _, xH => get i m       | xO ii, xO jj => xget ii jj m       | xI ii, xI jj => xget ii jj m       | _, _ => None       end.     Lemma xget_left :       forall (A : Type) (j i : positive) (m1 m2 : t A) (o : option A) (v : A),       xget i (append j (xO xH)) m1 = Some v -> xget i j (Node m1 o m2) = Some v.          Lemma xelements_ii :       forall (A: Type) (m: t A) (i j : positive) (v: A),       In (xI i, v) (xelements m (xI j)) -> In (i, v) (xelements m j).          Lemma xelements_io :       forall (A: Type) (m: t A) (i j : positive) (v: A),       ~In (xI i, v) (xelements m (xO j)).          Lemma xelements_oo :       forall (A: Type) (m: t A) (i j : positive) (v: A),       In (xO i, v) (xelements m (xO j)) -> In (i, v) (xelements m j).          Lemma xelements_oi :       forall (A: Type) (m: t A) (i j : positive) (v: A),       ~In (xO i, v) (xelements m (xI j)).          Lemma xelements_ih :       forall (A: Type) (m1 m2: t A) (o: option A) (i : positive) (v: A),       In (xI i, v) (xelements (Node m1 o m2) xH) -> In (i, v) (xelements m2 xH).          Lemma xelements_oh :       forall (A: Type) (m1 m2: t A) (o: option A) (i : positive) (v: A),       In (xO i, v) (xelements (Node m1 o m2) xH) -> In (i, v) (xelements m1 xH).          Lemma xelements_hi :       forall (A: Type) (m: t A) (i : positive) (v: A),       ~In (xH, v) (xelements m (xI i)).          Lemma xelements_ho :       forall (A: Type) (m: t A) (i : positive) (v: A),       ~In (xH, v) (xelements m (xO i)).          Lemma get_xget_h :       forall (A: Type) (m: t A) (i: positive), get i m = xget i xH m.          Lemma xelements_complete:       forall (A: Type) (i j : positive) (m: t A) (v: A),       In (i, v) (xelements m j) -> xget i j m = Some v.        Theorem elements_complete:     forall (A: Type) (m: t A) (i: positive) (v: A),     In (i, v) (elements m) -> get i m = Some v.      Lemma in_xelements:     forall (A: Type) (m: t A) (i k: positive) (v: A),     In (k, v) (xelements m i) ->     exists j, k = append i j.      Definition xkeys (A: Type) (m: t A) (i: positive) :=     List.map (@fst positive A) (xelements m i).   Lemma in_xkeys:     forall (A: Type) (m: t A) (i k: positive),     In k (xkeys m i) ->     exists j, k = append i j.      Remark list_append_cons_norepet:     forall (A: Type) (l1 l2: list A) (x: A),     list_norepet l1 -> list_norepet l2 -> list_disjoint l1 l2 ->     ~In x l1 -> ~In x l2 ->     list_norepet (l1 ++ x :: l2).      Lemma append_injective:     forall i j1 j2, append i j1 = append i j2 -> j1 = j2.      Lemma xelements_keys_norepet:     forall (A: Type) (m: t A) (i: positive),     list_norepet (xkeys m i).      Theorem elements_keys_norepet:     forall (A: Type) (m: t A),     list_norepet (List.map (@fst elt A) (elements m)).      Fixpoint xfold (A B: Type) (f: B -> positive -> A -> B)                  (i: positive) (m: t A) (v: B) {struct m} : B :=     match m with     | Leaf => v     | Node l None r =>         let v1 := xfold f (append i (xO xH)) l v in         xfold f (append i (xI xH)) r v1     | Node l (Some x) r =>         let v1 := xfold f (append i (xO xH)) l v in         let v2 := f v1 i x in         xfold f (append i (xI xH)) r v2     end.   Definition fold (A B : Type) (f: B -> positive -> A -> B) (m: t A) (v: B) :=     xfold f xH m v.   Lemma xfold_xelements:     forall (A B: Type) (f: B -> positive -> A -> B) m i v,     xfold f i m v =     List.fold_left (fun a p => f a (fst p) (snd p))                    (xelements m i)                    v.      Theorem fold_spec:     forall (A B: Type) (f: B -> positive -> A -> B) (v: B) (m: t A),     fold f m v =     List.fold_left (fun a p => f a (fst p) (snd p)) (elements m) v.    End PTree. ```

# An implementation of maps over type `positive`

``` Module PMap <: MAP.   Definition elt := positive.   Definition elt_eq := peq.   Definition t (A : Type) : Type := (A * PTree.t A)%type.   Definition eq: forall (A: Type), (forall (x y: A), {x=y} + {x<>y}) ->                  forall (a b: t A), {a = b} + {a <> b}.      Definition init (A : Type) (x : A) :=     (x, PTree.empty A).   Definition get (A : Type) (i : positive) (m : t A) :=     match PTree.get i (snd m) with     | Some x => x     | None => fst m     end.   Definition set (A : Type) (i : positive) (x : A) (m : t A) :=     (fst m, PTree.set i x (snd m)).   Theorem gi:     forall (A: Type) (i: positive) (x: A), get i (init x) = x.      Theorem gss:     forall (A: Type) (i: positive) (x: A) (m: t A), get i (set i x m) = x.      Theorem gso:     forall (A: Type) (i j: positive) (x: A) (m: t A),     i <> j -> get i (set j x m) = get i m.      Theorem gsspec:     forall (A: Type) (i j: positive) (x: A) (m: t A),     get i (set j x m) = if peq i j then x else get i m.      Theorem gsident:     forall (A: Type) (i j: positive) (m: t A),     get j (set i (get i m) m) = get j m.      Definition map (A B : Type) (f : A -> B) (m : t A) : t B :=     (f (fst m), PTree.map (fun _ => f) (snd m)).   Theorem gmap:     forall (A B: Type) (f: A -> B) (i: positive) (m: t A),     get i (map f m) = f(get i m).    End PMap. ```

# An implementation of maps over any type that injects into type `positive`

``` Module Type INDEXED_TYPE.   Variable t: Type.   Variable index: t -> positive.   Hypothesis index_inj: forall (x y: t), index x = index y -> x = y.   Variable eq: forall (x y: t), {x = y} + {x <> y}. End INDEXED_TYPE. Module IMap(X: INDEXED_TYPE).   Definition elt := X.t.   Definition elt_eq := X.eq.   Definition t : Type -> Type := PMap.t.   Definition eq: forall (A: Type), (forall (x y: A), {x=y} + {x<>y}) ->                  forall (a b: t A), {a = b} + {a <> b} := PMap.eq.   Definition init (A: Type) (x: A) := PMap.init x.   Definition get (A: Type) (i: X.t) (m: t A) := PMap.get (X.index i) m.   Definition set (A: Type) (i: X.t) (v: A) (m: t A) := PMap.set (X.index i) v m.   Definition map (A B: Type) (f: A -> B) (m: t A) : t B := PMap.map f m.   Lemma gi:     forall (A: Type) (x: A) (i: X.t), get i (init x) = x.      Lemma gss:     forall (A: Type) (i: X.t) (x: A) (m: t A), get i (set i x m) = x.      Lemma gso:     forall (A: Type) (i j: X.t) (x: A) (m: t A),     i <> j -> get i (set j x m) = get i m.      Lemma gsspec:     forall (A: Type) (i j: X.t) (x: A) (m: t A),     get i (set j x m) = if X.eq i j then x else get i m.      Lemma gmap:     forall (A B: Type) (f: A -> B) (i: X.t) (m: t A),     get i (map f m) = f(get i m).    End IMap. Module ZIndexed.   Definition t := Z.   Definition index (z: Z): positive :=     match z with     | Z0 => xH     | Zpos p => xO p     | Zneg p => xI p     end.   Lemma index_inj: forall (x y: Z), index x = index y -> x = y.      Definition eq := zeq. End ZIndexed. Module ZMap := IMap(ZIndexed). Module NIndexed.   Definition t := N.   Definition index (n: N): positive :=     match n with     | N0 => xH     | Npos p => xO p     end.   Lemma index_inj: forall (x y: N), index x = index y -> x = y.      Lemma eq: forall (x y: N), {x = y} + {x <> y}.    End NIndexed. Module NMap := IMap(NIndexed). ```

# An implementation of maps over any type with decidable equality

``` Module Type EQUALITY_TYPE.   Variable t: Type.   Variable eq: forall (x y: t), {x = y} + {x <> y}. End EQUALITY_TYPE. Module EMap(X: EQUALITY_TYPE) <: MAP.   Definition elt := X.t.   Definition elt_eq := X.eq.   Definition t (A: Type) := X.t -> A.   Definition init (A: Type) (v: A) := fun (_: X.t) => v.   Definition get (A: Type) (x: X.t) (m: t A) := m x.   Definition set (A: Type) (x: X.t) (v: A) (m: t A) :=     fun (y: X.t) => if X.eq y x then v else m y.   Lemma gi:     forall (A: Type) (i: elt) (x: A), init x i = x.      Lemma gss:     forall (A: Type) (i: elt) (x: A) (m: t A), (set i x m) i = x.      Lemma gso:     forall (A: Type) (i j: elt) (x: A) (m: t A),     i <> j -> (set j x m) i = m i.      Lemma gsspec:     forall (A: Type) (i j: elt) (x: A) (m: t A),     get i (set j x m) = if elt_eq i j then x else get i m.      Lemma gsident:     forall (A: Type) (i j: elt) (m: t A), get j (set i (get i m) m) = get j m.      Definition map (A B: Type) (f: A -> B) (m: t A) :=     fun (x: X.t) => f(m x).   Lemma gmap:     forall (A B: Type) (f: A -> B) (i: elt) (m: t A),     get i (map f m) = f(get i m).    End EMap. ```

# Additional properties over trees

``` Module Tree_Properties(T: TREE). ```
An induction principle over `fold`.
``` Section TREE_FOLD_IND. Variables V A: Type. Variable f: A -> T.elt -> V -> A. Variable P: T.t V -> A -> Prop. Variable init: A. Variable m_final: T.t V. Hypothesis P_compat:   forall m m' a,   (forall x, T.get x m = T.get x m') ->   P m a -> P m' a. Hypothesis H_base:   P (T.empty _) init. Hypothesis H_rec:   forall m a k v,   T.get k m = None -> T.get k m_final = Some v -> P m a -> P (T.set k v m) (f a k v). Definition f' (a: A) (p : T.elt * V) := f a (fst p) (snd p). Definition P' (l: list (T.elt * V)) (a: A) : Prop :=   forall m, list_equiv l (T.elements m) -> P m a. Remark H_base':   P' nil init. Remark H_rec':   forall k v l a,   ~In k (List.map (@fst T.elt V) l) ->   In (k, v) (T.elements m_final) ->   P' l a ->   P' (l ++ (k, v) :: nil) (f a k v). Lemma fold_rec_aux:   forall l1 l2 a,   list_equiv (l2 ++ l1) (T.elements m_final) ->   list_disjoint (List.map (@fst T.elt V) l1) (List.map (@fst T.elt V) l2) ->   list_norepet (List.map (@fst T.elt V) l1) ->   P' l2 a -> P' (l2 ++ l1) (List.fold_left f' l1 a). Theorem fold_rec:   P m_final (T.fold f m_final init). End TREE_FOLD_IND. End Tree_Properties. Module PTree_Properties := Tree_Properties(PTree). ```

# Useful notations

``` Notation "a ! b" := (PTree.get b a) (at level 1). Notation "a !! b" := (PMap.get b a) (at level 1). ```