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
In this library, we provide efficient implementations of trees and maps whose keys range over the type
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, eitherNone
if no data is associated to the key, orSome 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.
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.
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.
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.
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.
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).
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.
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).
Notation "a ! b" := (PTree.get b a) (at level 1).
Notation "a !! b" := (PMap.get b a) (at level 1).