# Library compcert.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 Equivalence EquivDec.
Require Import Coqlib.

LocalLocal
Set Implicit Arguments.

# The abstract signatures of trees

Module Type TREE.
Variable elt: Type.
Variable elt_eq: (a b: elt), {a = b} + {a b}.
Variable t: TypeType.
Variable empty: (A: Type), t A.
Variable get: (A: Type), eltt Aoption A.
Variable set: (A: Type), eltAt At A.
Variable remove: (A: Type), eltt At A.

The ``good variables'' properties for trees, expressing commutations between get, set and remove.
Hypothesis gempty:
(A: Type) (i: elt), get i (empty A) = None.
Hypothesis gss:
(A: Type) (i: elt) (x: A) (m: t A), get i (set i x m) = Some x.
Hypothesis gso:
(A: Type) (i j: elt) (x: A) (m: t A),
i jget i (set j x m) = get i m.
Hypothesis gsspec:
(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:
(A: Type) (i: elt) (m: t A) (v: A),
get i m = Some vset i v m = m.
Hypothesis grs:
(A: Type) (i: elt) (m: t A), get i (remove i m) = None.
Hypothesis gro:
(A: Type) (i j: elt) (m: t A),
i jget i (remove j m) = get i m.
Hypothesis grspec:
(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: (A: Type), (AAbool) → t At Abool.
Hypothesis beq_correct:
(A: Type) (eqA: AAbool) (t1 t2: t A),
beq eqA t1 t2 = true
( (x: elt),
match get x t1, get x t2 with
| None, NoneTrue
| Some y1, Some y2eqA y1 y2 = true
| _, _False
end).

Applying a function to all data of a tree.
Variable map:
(A B: Type), (eltAB) → t At B.
Hypothesis gmap:
(A B: Type) (f: eltAB) (i: elt) (m: t A),
get i (map f m) = option_map (f i) (get i m).

Same as map, but the function does not receive the elt argument.
Variable map1:
(A B: Type), (AB) → t At B.
Hypothesis gmap1:
(A B: Type) (f: AB) (i: elt) (m: t A),
get i (map1 f m) = option_map f (get i m).

Applying a function pairwise to all data of two trees.
Variable combine:
(A B C: Type), (option Aoption Boption C) → t At Bt C.
Hypothesis gcombine:
(A B C: Type) (f: option Aoption Boption C),
f None None = None
(m1: t A) (m2: t B) (i: elt),
get i (combine f m1 m2) = f (get i m1) (get i m2).
Hypothesis combine_commut:
(A B: Type) (f g: option Aoption Aoption B),
( (i j: option A), f i j = g j i) →
(m1 m2: t A),
combine f m1 m2 = combine g m2 m1.

Enumerating the bindings of a tree.
Variable elements:
(A: Type), t Alist (elt × A).
Hypothesis elements_correct:
(A: Type) (m: t A) (i: elt) (v: A),
get i m = Some vIn (i, v) (elements m).
Hypothesis elements_complete:
(A: Type) (m: t A) (i: elt) (v: A),
In (i, v) (elements m) → get i m = Some v.
Hypothesis elements_keys_norepet:
(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:
(A B: Type), (BeltAB) → t ABB.
Hypothesis fold_spec:
(A B: Type) (f: BeltAB) (v: B) (m: t A),
fold f m v =
List.fold_left (fun a pf a (fst p) (snd p)) (elements m) v.
Same as fold, but the function does not receive the elt argument.
Variable fold1:
(A B: Type), (BAB) → t ABB.
Hypothesis fold1_spec:
(A B: Type) (f: BAB) (v: B) (m: t A),
fold1 f m v =
List.fold_left (fun a pf a (snd p)) (elements m) v.
End TREE.

# The abstract signatures of maps

Module Type MAP.
Variable elt: Type.
Variable elt_eq: (a b: elt), {a = b} + {a b}.
Variable t: TypeType.
Variable init: (A: Type), At A.
Variable get: (A: Type), eltt AA.
Variable set: (A: Type), eltAt At A.
Hypothesis gi:
(A: Type) (i: elt) (x: A), get i (init x) = x.
Hypothesis gss:
(A: Type) (i: elt) (x: A) (m: t A), get i (set i x m) = x.
Hypothesis gso:
(A: Type) (i j: elt) (x: A) (m: t A),
i jget i (set j x m) = get i m.
Hypothesis gsspec:
(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:
(A: Type) (i j: elt) (m: t A), get j (set i (get i m) m) = get j m.
Variable map: (A B: Type), (AB) → t At B.
Hypothesis gmap:
(A B: Type) (f: AB) (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 Aoption Atree Atree A.

Implicit Arguments Leaf [A].
Implicit Arguments Node [A].
Scheme tree_ind := Induction for tree Sort Prop.

Definition t := tree.

Definition empty (A : Type) := (Leaf : t A).

Fixpoint get (A : Type) (i : positive) (m : t A) {struct i} : option A :=
match m with
| LeafNone
| Node l o r
match i with
| xHo
| xO iiget ii l
| xI iiget 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
| xHNode Leaf (Some v) Leaf
| xO iiNode (set ii v Leaf) None Leaf
| xI iiNode Leaf None (set ii v Leaf)
end
| Node l o r
match i with
| xHNode l (Some v) r
| xO iiNode (set ii v l) o r
| xI iiNode 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
| LeafLeaf
| Node Leaf o LeafLeaf
| Node l o rNode l None r
end
| xO ii
match m with
| LeafLeaf
| Node l None Leaf
match remove ii l with
| LeafLeaf
| mmNode mm None Leaf
end
| Node l o rNode (remove ii l) o r
end
| xI ii
match m with
| LeafLeaf
| Node Leaf None r
match remove ii r with
| LeafLeaf
| mmNode Leaf None mm
end
| Node l o rNode l o (remove ii r)
end
end.

Theorem gempty:
(A: Type) (i: positive), get i (empty A) = None.

Theorem gss:
(A: Type) (i: positive) (x: A) (m: t A), get i (set i x m) = Some x.

Lemma gleaf : (A : Type) (i : positive), get i (Leaf : t A) = None.

Theorem gso:
(A: Type) (i j: positive) (x: A) (m: t A),
i jget i (set j x m) = get i m.

Theorem gsspec:
(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:
(A: Type) (i: positive) (m: t A) (v: A),
get i m = Some vset i v m = m.

Theorem set2:
(A: Type) (i: elt) (m: t A) (v1 v2: A),
set i v2 (set i v1 m) = set i v2 m.

Lemma rleaf : (A : Type) (i : positive), remove i (Leaf : t A) = Leaf.

Theorem grs:
(A: Type) (i: positive) (m: t A), get i (remove i m) = None.

Theorem gro:
(A: Type) (i j: positive) (m: t A),
i jget i (remove j m) = get i m.

Theorem grspec:
(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 BOOLEAN_EQUALITY.

Variable A: Type.
Variable beqA: AAbool.

Fixpoint bempty (m: t A) : bool :=
match m with
| Leaftrue
| Node l None rbempty l && bempty r
| Node l (Some _) rfalse
end.

Fixpoint beq (m1 m2: t A) {struct m1} : bool :=
match m1, m2 with
| Leaf, _bempty m2
| _, Leafbempty m1
| Node l1 o1 r1, Node l2 o2 r2
match o1, o2 with
| None, Nonetrue
| Some y1, Some y2beqA y1 y2
| _, _false
end
&& beq l1 l2 && beq r1 r2
end.

Lemma bempty_correct:
m, bempty m = true ( x, get x m = None).

Lemma beq_correct:
m1 m2,
beq m1 m2 = true
( (x: elt),
match get x m1, get x m2 with
| None, NoneTrue
| Some y1, Some y2beqA y1 y2 = true
| _, _False
end).

End BOOLEAN_EQUALITY.

Fixpoint append (i j : positive) {struct i} : positive :=
match i with
| xHj
| xI iixI (append ii j)
| xO iixO (append ii j)
end.

Lemma append_assoc_0 : (i j : positive),
append i (xO j) = append (append i (xO xH)) j.

Lemma append_assoc_1 : (i j : positive),
append i (xI j) = append (append i (xI xH)) j.

Lemma append_neutral_r : (i : positive), append i xH = i.

Lemma append_neutral_l : (i : positive), append xH i = i.

Fixpoint xmap (A B : Type) (f : positiveAB) (m : t A) (i : positive)
{struct m} : t B :=
match m with
| LeafLeaf
| Node l o rNode (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 : positiveAB) m := xmap f m xH.

Lemma xgmap:
(A B: Type) (f: positiveAB) (i j : positive) (m: t A),
get i (xmap f m j) = option_map (f (append j i)) (get i m).

Theorem gmap:
(A B: Type) (f: positiveAB) (i: positive) (m: t A),
get i (map f m) = option_map (f i) (get i m).

Fixpoint map1 (A B: Type) (f: AB) (m: t A) {struct m} : t B :=
match m with
| LeafLeaf
| Node l o rNode (map1 f l) (option_map f o) (map1 f r)
end.

Theorem gmap1:
(A B: Type) (f: AB) (i: elt) (m: t A),
get i (map1 f m) = option_map f (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, LeafLeaf
| _, _, _Node l x r
end.

Lemma gnode':
(A: Type) (l r: t A) (x: option A) (i: positive),
get i (Node' l x r) = get i (Node l x r).

Fixpoint filter1 (A: Type) (pred: Abool) (m: t A) {struct m} : t A :=
match m with
| LeafLeaf
| Node l o r
let o' := match o with NoneNone | Some xif pred x then o else None end in
Node' (filter1 pred l) o' (filter1 pred r)
end.

Theorem gfilter1:
(A: Type) (pred: Abool) (i: elt) (m: t A),
get i (filter1 pred m) =
match get i m with NoneNone | Some xif pred x then Some x else None end.

Section COMBINE.

Variables A B C: Type.
Variable f: option Aoption Boption C.
Hypothesis f_none_none: f None None = None.

Fixpoint xcombine_l (m : t A) {struct m} : t C :=
match m with
| LeafLeaf
| Node l o rNode' (xcombine_l l) (f o None) (xcombine_l r)
end.

Lemma xgcombine_l :
(m: t A) (i : positive),
get i (xcombine_l m) = f (get i m) None.

Fixpoint xcombine_r (m : t B) {struct m} : t C :=
match m with
| LeafLeaf
| Node l o rNode' (xcombine_r l) (f None o) (xcombine_r r)
end.

Lemma xgcombine_r :
(m: t B) (i : positive),
get i (xcombine_r m) = f None (get i m).

Fixpoint combine (m1: t A) (m2: t B) {struct m1} : t C :=
match m1 with
| Leafxcombine_r m2
| Node l1 o1 r1
match m2 with
| Leafxcombine_l m1
| Node l2 o2 r2Node' (combine l1 l2) (f o1 o2) (combine r1 r2)
end
end.

Theorem gcombine:
(m1: t A) (m2: t B) (i: positive),
get i (combine m1 m2) = f (get i m1) (get i m2).

End COMBINE.

Lemma xcombine_lr :
(A B: Type) (f g : option Aoption Aoption B) (m : t A),
( (i j : option A), f i j = g j i) →
xcombine_l f m = xcombine_r g m.

Theorem combine_commut:
(A B: Type) (f g: option Aoption Aoption B),
( (i j: option A), f i j = g j i) →
(m1 m2: t A),
combine f m1 m2 = combine g m2 m1.

Fixpoint xelements (A : Type) (m : t A) (i : positive)
(k: list (positive × A)) {struct m}
: list (positive × A) :=
match m with
| Leafk
| Node l None r
xelements l (append i (xO xH)) (xelements r (append i (xI xH)) k)
| Node l (Some x) r
xelements l (append i (xO xH))
((i, x) :: xelements r (append i (xI xH)) k)
end.

Definition elements (A: Type) (m : t A) := xelements m xH nil.

Lemma xelements_incl:
(A: Type) (m: t A) (i : positive) k x,
In x kIn x (xelements m i k).

Lemma xelements_correct:
(A: Type) (m: t A) (i j : positive) (v: A) k,
get i m = Some vIn (append j i, v) (xelements m j k).

Theorem elements_correct:
(A: Type) (m: t A) (i: positive) (v: A),
get i m = Some vIn (i, v) (elements m).

Fixpoint xget (A : Type) (i j : positive) (m : t A) {struct j} : option A :=
match i, j with
| _, xHget i m
| xO ii, xO jjxget ii jj m
| xI ii, xI jjxget ii jj m
| _, _None
end.

Lemma xget_diag :
(A : Type) (i : positive) (m1 m2 : t A) (o : option A),
xget i i (Node m1 o m2) = o.

Lemma xget_left :
(A : Type) (j i : positive) (m1 m2 : t A) (o : option A) (v : A),
xget i (append j (xO xH)) m1 = Some vxget i j (Node m1 o m2) = Some v.

Lemma xget_right :
(A : Type) (j i : positive) (m1 m2 : t A) (o : option A) (v : A),
xget i (append j (xI xH)) m2 = Some vxget i j (Node m1 o m2) = Some v.

Lemma xelements_complete:
(A: Type) (m: t A) (i j : positive) (v: A) k,
In (i, v) (xelements m j k) → xget i j m = Some v In (i, v) k.

Lemma get_xget_h :
(A: Type) (m: t A) (i: positive), get i m = xget i xH m.

Theorem elements_complete:
(A: Type) (m: t A) (i: positive) (v: A),
In (i, v) (elements m) → get i m = Some v.

Lemma in_xelements:
(A: Type) (m: t A) (i k: positive) (v: A) l,
In (k, v) (xelements m i l) →
( j, k = append i j) In (k, v) l.

Definition xkeys (A: Type) (m: t A) (i: positive) (l: list (positive × A)) :=
List.map (@fst positive A) (xelements m i l).

Lemma in_xkeys:
(A: Type) (m: t A) (i k: positive) l,
In k (xkeys m i l) →
( j, k = append i j) In k (List.map fst l).

Lemma append_injective:
i j1 j2, append i j1 = append i j2j1 = j2.

Lemma xelements_keys_norepet:
(A: Type) (m: t A) (i: positive) l,
( k v, get k m = Some v¬In (append i k) (List.map fst l)) →
list_norepet (List.map fst l) →
list_norepet (xkeys m i l).

Theorem elements_keys_norepet:
(A: Type) (m: t A),
list_norepet (List.map (@fst elt A) (elements m)).

Remark xelements_empty:
(A: Type) (m: t A) i l, ( i, get i m = None) → xelements m i l = l.

Theorem elements_canonical_order:
(A B: Type) (R: ABProp) (m: t A) (n: t B),
( i x, get i m = Some x y, get i n = Some y R x y) →
( i y, get i n = Some y x, get i m = Some x R x y) →
list_forall2
(fun i_x i_yfst i_x = fst i_y R (snd i_x) (snd i_y))
(elements m) (elements n).

Theorem elements_extensional:
(A: Type) (m n: t A),
( i, get i m = get i n) →
elements m = elements n.

Fixpoint xfold (A B: Type) (f: BpositiveAB)
(i: positive) (m: t A) (v: B) {struct m} : B :=
match m with
| Leafv
| 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: BpositiveAB) (m: t A) (v: B) :=
xfold f xH m v.

Lemma xfold_xelements:
(A B: Type) (f: BpositiveAB) m i v l,
List.fold_left (fun a pf a (fst p) (snd p)) l (xfold f i m v) =
List.fold_left (fun a pf a (fst p) (snd p)) (xelements m i l) v.

Theorem fold_spec:
(A B: Type) (f: BpositiveAB) (v: B) (m: t A),
fold f m v =
List.fold_left (fun a pf a (fst p) (snd p)) (elements m) v.

Fixpoint fold1 (A B: Type) (f: BAB) (m: t A) (v: B) {struct m} : B :=
match m with
| Leafv
| Node l None r
let v1 := fold1 f l v in
fold1 f r v1
| Node l (Some x) r
let v1 := fold1 f l v in
let v2 := f v1 x in
fold1 f r v2
end.

Lemma fold1_xelements:
(A B: Type) (f: BAB) m i v l,
List.fold_left (fun a pf a (snd p)) l (fold1 f m v) =
List.fold_left (fun a pf a (snd p)) (xelements m i l) v.

Theorem fold1_spec:
(A B: Type) (f: BAB) (v: B) (m: t A),
fold1 f m v =
List.fold_left (fun a pf a (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 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 xx
| Nonefst m
end.

Definition set (A : Type) (i : positive) (x : A) (m : t A) :=
(fst m, PTree.set i x (snd m)).

Theorem gi:
(A: Type) (i: positive) (x: A), get i (init x) = x.

Theorem gss:
(A: Type) (i: positive) (x: A) (m: t A), get i (set i x m) = x.

Theorem gso:
(A: Type) (i j: positive) (x: A) (m: t A),
i jget i (set j x m) = get i m.

Theorem gsspec:
(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:
(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 : AB) (m : t A) : t B :=
(f (fst m), PTree.map1 f (snd m)).

Theorem gmap:
(A B: Type) (f: AB) (i: positive) (m: t A),
get i (map f m) = f(get i m).

Theorem set2:
(A: Type) (i: elt) (x y: A) (m: t A),
set i y (set i x m) = set i y m.

End PMap.

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

Module Type INDEXED_TYPE.
Variable t: Type.
Variable index: tpositive.
Hypothesis index_inj: (x y: t), index x = index yx = y.
Variable eq: (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 : TypeType := PMap.t.
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: AB) (m: t A) : t B := PMap.map f m.

Lemma gi:
(A: Type) (x: A) (i: X.t), get i (init x) = x.

Lemma gss:
(A: Type) (i: X.t) (x: A) (m: t A), get i (set i x m) = x.

Lemma gso:
(A: Type) (i j: X.t) (x: A) (m: t A),
i jget i (set j x m) = get i m.

Lemma gsspec:
(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:
(A B: Type) (f: AB) (i: X.t) (m: t A),
get i (map f m) = f(get i m).

Lemma set2:
(A: Type) (i: elt) (x y: A) (m: t A),
set i y (set i x m) = set i y m.

End IMap.

Module ZIndexed.
Definition t := Z.
Definition index (z: Z): positive :=
match z with
| Z0xH
| Zpos pxO p
| Zneg pxI p
end.
Lemma index_inj: (x y: Z), index x = index yx = y.
Definition eq := zeq.
End ZIndexed.

Module ZMap := IMap(ZIndexed).

Module NIndexed.
Definition t := N.
Definition index (n: N): positive :=
match n with
| N0xH
| Npos pxO p
end.
Lemma index_inj: (x y: N), index x = index yx = y.
Lemma eq: (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: (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.tA.
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:
(A: Type) (i: elt) (x: A), init x i = x.
Lemma gss:
(A: Type) (i: elt) (x: A) (m: t A), (set i x m) i = x.
Lemma gso:
(A: Type) (i j: elt) (x: A) (m: t A),
i j → (set j x m) i = m i.
Lemma gsspec:
(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:
(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: AB) (m: t A) :=
fun (x: X.t) ⇒ f(m x).
Lemma gmap:
(A B: Type) (f: AB) (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: AT.eltVA.
Variable P: T.t VAProp.
Variable init: A.
Variable m_final: T.t V.

Hypothesis P_compat:
m m' a,
( x, T.get x m = T.get x m') →
P m aP m' a.

Hypothesis H_base:
P (T.empty _) init.

Hypothesis H_rec:
m a k v,
T.get k m = NoneT.get k m_final = Some vP m aP (T.set k v m) (f a k v).

Let f' (a: A) (p : T.elt × V) := f a (fst p) (snd p).

Let P' (l: list (T.elt × V)) (a: A) : Prop :=
m, list_equiv l (T.elements m) → P m a.

Remark H_base':
P' nil init.

Remark H_rec':
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:
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 aP' (l2 ++ l1) (List.fold_left f' l1 a).

Theorem fold_rec:
P m_final (T.fold f m_final init).

End TREE_FOLD_IND.

A nonnegative measure over trees

Section MEASURE.

Variable V: Type.

Definition cardinal (x: T.t V) : nat := List.length (T.elements x).

Remark list_incl_length:
(A: Type) (l1: list A), list_norepet l1
(l2: list A), List.incl l1 l2 → (List.length l1 List.length l2)%nat.

Remark list_length_incl:
(A: Type) (l1: list A), list_norepet l1
l2, List.incl l1 l2List.length l1 = List.length l2List.incl l2 l1.

Remark list_strict_incl_length:
(A: Type) (l1 l2: list A) (x: A),
list_norepet l1List.incl l1 l2¬In x l1In x l2
(List.length l1 < List.length l2)%nat.

Remark list_norepet_map:
(A B: Type) (f: AB) (l: list A),
list_norepet (List.map f l) → list_norepet l.

Theorem cardinal_remove:
x m y, T.get x m = Some y → (cardinal (T.remove x m) < cardinal m)%nat.

End MEASURE.

Forall and exists

Section FORALL_EXISTS.

Variable A: Type.

Definition for_all (m: T.t A) (f: T.eltAbool) : bool :=
T.fold (fun b x ab && f x a) m true.

Lemma for_all_correct:
m f,
for_all m f = true ( x a, T.get x m = Some af x a = true).

Definition exists_ (m: T.t A) (f: T.eltAbool) : bool :=
T.fold (fun b x ab || f x a) m false.

Lemma exists_correct:
m f,
exists_ m f = true ( x a, T.get x m = Some a f x a = true).

Remark exists_for_all:
m f,
exists_ m f = negb (for_all m (fun x anegb (f x a))).

Remark for_all_exists:
m f,
for_all m f = negb (exists_ m (fun x anegb (f x a))).

Lemma for_all_false:
m f,
for_all m f = false ( x a, T.get x m = Some a f x a = false).

Lemma exists_false:
m f,
exists_ m f = false ( x a, T.get x m = Some af x a = false).

End FORALL_EXISTS.

Section BOOLEAN_EQUALITY.

Variable A: Type.
Variable beqA: AAbool.

Theorem beq_false:
m1 m2,
T.beq beqA m1 m2 = false
x, match T.get x m1, T.get x m2 with
| None, NoneFalse
| Some a1, Some a2beqA a1 a2 = false
| _, _True
end.

End BOOLEAN_EQUALITY.

Extensional equality between trees

Section EXTENSIONAL_EQUALITY.

Variable A: Type.
Variable eqA: AAProp.
Hypothesis eqAeq: Equivalence eqA.

Definition Equal (m1 m2: T.t A) : Prop :=
x, match T.get x m1, T.get x m2 with
| None, NoneTrue
| Some a1, Some a2a1 === a2
| _, _False
end.

Lemma Equal_refl: m, Equal m m.

Lemma Equal_sym: m1 m2, Equal m1 m2Equal m2 m1.

Lemma Equal_trans: m1 m2 m3, Equal m1 m2Equal m2 m3Equal m1 m3.

Instance Equal_Equivalence : Equivalence Equal := {
Equivalence_Reflexive := Equal_refl;
Equivalence_Symmetric := Equal_sym;
Equivalence_Transitive := Equal_trans
}.

Program Definition Equal_dec (m1 m2: T.t A) : { m1 === m2 } + { m1 =/= m2 } :=
match T.beq (fun a1 a2proj_sumbool (a1 == a2)) m1 m2 with
| trueleft _
| falseright _
end.

Instance Equal_EqDec : EqDec (T.t A) Equal := Equal_dec.

End EXTENSIONAL_EQUALITY.

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