| This code is written by Xavier Leroy as part of the Compcert project: http://pauillac.inria.fr/~xleroy/compcert-backend/ |
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:
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 List TheoryList.
Require Import Coqlib.
Require Import Specif Monad ListUtil Tactics.
Set Implicit Arguments.
The abstract signatures of trees |
Module Type TREE.
Variable elt: Set.
Variable elt_eq: forall (a b: elt), {a = b} + {a <> b}.
Variable t: Set -> Set.
Variable eq: forall (A: Set), (forall (x y: A), {x=y} + {x<>y}) ->
forall (a b: t A), {a = b} + {a <> b}.
Variable empty: forall (A: Set), t A.
Variable get: forall (A: Set), elt -> t A -> option A.
Variable set: forall (A: Set), elt -> A -> t A -> t A.
Variable remove: forall (A: Set), elt -> t A -> t A.
The ``good variables'' properties for trees, expressing
commutations between get, set and remove.
|
Hypothesis gempty:
forall (A: Set) (i: elt), get i (empty A) = None.
Hypothesis gss:
forall (A: Set) (i: elt) (x: A) (m: t A), get i (set i x m) = Some x.
Hypothesis gso:
forall (A: Set) (i j: elt) (x: A) (m: t A),
i <> j -> get i (set j x m) = get i m.
Hypothesis gsspec:
forall (A: Set) (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: Set) (i: elt) (m: t A) (v: A),
get i m = Some v -> set i v m = m.
Hypothesis grs:
forall (A: Set) (i: elt) (m: t A), get i (remove i m) = None.
Hypothesis gro:
forall (A: Set) (i j: elt) (m: t A),
i <> j -> get i (remove j m) = get i m.
| Applying a function to all data of a tree. |
Variable map:
forall (A B: Set), (elt -> A -> B) -> t A -> t B.
Hypothesis gmap:
forall (A B: Set) (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: Set), (option A -> option A -> option A) -> t A -> t A -> t A.
Hypothesis gcombine:
forall (A: Set) (f: option A -> option A -> option A)
(m1 m2: t A) (i: elt),
f None None = None ->
get i (combine f m1 m2) = f (get i m1) (get i m2).
Hypothesis combine_commut:
forall (A: Set) (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: Set), t A -> list (elt * A).
Hypothesis elements_correct:
forall (A: Set) (m: t A) (i: elt) (v: A),
get i m = Some v -> In (i, v) (elements m).
Hypothesis elements_complete:
forall (A: Set) (m: t A) (i: elt) (v: A),
In (i, v) (elements m) -> get i m = Some v.
Hypothesis elements_keys_norepet:
forall (A: Set) (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: Set), (B -> elt -> A -> B) -> t A -> B -> B.
Hypothesis fold_spec:
forall (A B: Set) (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: Set.
Variable elt_eq: forall (a b: elt), {a = b} + {a <> b}.
Variable t: Set -> Set.
Variable init: forall (A: Set), A -> t A.
Variable get: forall (A: Set), elt -> t A -> A.
Variable set: forall (A: Set), elt -> A -> t A -> t A.
Hypothesis gi:
forall (A: Set) (i: elt) (x: A), get i (init x) = x.
Hypothesis gss:
forall (A: Set) (i: elt) (x: A) (m: t A), get i (set i x m) = x.
Hypothesis gso:
forall (A: Set) (i j: elt) (x: A) (m: t A),
i <> j -> get i (set j x m) = get i m.
Hypothesis gsspec:
forall (A: Set) (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: Set) (i j: elt) (m: t A), get j (set i (get i m) m) = get j m.
Variable map: forall (A B: Set), (A -> B) -> t A -> t B.
Hypothesis gmap:
forall (A B: Set) (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
|
Module PTree <: TREE.
Definition elt := positive.
Definition elt_eq := peq.
Inductive tree (A : Set) : Set :=
| 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 : Set),
(forall (x y: A), {x=y} + {x<>y}) ->
forall (a b : t A), {a = b} + {a <> b}.
Definition empty (A : Set) := (Leaf : t A).
Fixpoint get (A : Set) (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 : Set) (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 : Set) (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: Set) (i: positive), get i (empty A) = None.
Theorem gss:
forall (A: Set) (i: positive) (x: A) (m: t A), get i (set i x m) = Some x.
Lemma gleaf : forall (A : Set) (i : positive), get i (Leaf : t A) = None.
Theorem gso:
forall (A: Set) (i j: positive) (x: A) (m: t A),
i <> j -> get i (set j x m) = get i m.
Theorem gsspec:
forall (A: Set) (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: Set) (i: positive) (m: t A) (v: A),
get i m = Some v -> set i v m = m.
Lemma rleaf : forall (A : Set) (i : positive), remove i (Leaf : t A) = Leaf.
Theorem grs:
forall (A: Set) (i: positive) (m: t A), get i (remove i m) = None.
Theorem gro:
forall (A: Set) (i j: positive) (m: t A),
i <> j -> get i (remove j m) = get i m.
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 : Set) (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 : Set) (f : positive -> A -> B) m := xmap f m xH.
Lemma xgmap:
forall (A B: Set) (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: Set) (f: positive -> A -> B) (i: positive) (m: t A),
get i (map f m) = option_map (f i) (get i m).
Fixpoint xcombine_l (A : Set) (f : option A -> option A -> option A)
(m : t A) {struct m} : t A :=
match m with
| Leaf => Leaf
| Node l o r => Node (xcombine_l f l) (f o None) (xcombine_l f r)
end.
Lemma xgcombine_l :
forall (A : Set) (f : option A -> option A -> option A)
(i : positive) (m : t A),
f None None = None -> get i (xcombine_l f m) = f (get i m) None.
Fixpoint xcombine_r (A : Set) (f : option A -> option A -> option A)
(m : t A) {struct m} : t A :=
match m with
| Leaf => Leaf
| Node l o r => Node (xcombine_r f l) (f None o) (xcombine_r f r)
end.
Lemma xgcombine_r :
forall (A : Set) (f : option A -> option A -> option A)
(i : positive) (m : t A),
f None None = None -> get i (xcombine_r f m) = f None (get i m).
Fixpoint combine (A : Set) (f : option A -> option A -> option A)
(m1 m2 : t A) {struct m1} : t A :=
match m1 with
| Leaf => xcombine_r f m2
| Node l1 o1 r1 =>
match m2 with
| Leaf => xcombine_l f m1
| Node l2 o2 r2 => Node (combine f l1 l2) (f o1 o2) (combine f r1 r2)
end
end.
Lemma xgcombine:
forall (A: Set) (f: option A -> option A -> option A) (i: positive)
(m1 m2: t A),
f None None = None ->
get i (combine f m1 m2) = f (get i m1) (get i m2).
Theorem gcombine:
forall (A: Set) (f: option A -> option A -> option A)
(m1 m2: t A) (i: positive),
f None None = None ->
get i (combine f m1 m2) = f (get i m1) (get i m2).
Lemma xcombine_lr :
forall (A : Set) (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: Set) (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 : Set) (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)))
++ (cons (i, x) (xelements r (append i (xI xH))))
end.
Definition elements A (m : t A) := xelements m xH.
Lemma xelements_correct:
forall (A: Set) (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: Set) (m: t A) (i: positive) (v: A),
get i m = Some v -> In (i, v) (elements m).
Fixpoint xget (A : Set) (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 : Set) (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: Set) (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: Set) (m: t A) (i j : positive) (v: A),
~In (xI i, v) (xelements m (xO j)).
Lemma xelements_oo :
forall (A: Set) (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: Set) (m: t A) (i j : positive) (v: A),
~In (xO i, v) (xelements m (xI j)).
Lemma xelements_ih :
forall (A: Set) (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: Set) (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: Set) (m: t A) (i : positive) (v: A),
~In (xH, v) (xelements m (xI i)).
Lemma xelements_ho :
forall (A: Set) (m: t A) (i : positive) (v: A),
~In (xH, v) (xelements m (xO i)).
Lemma get_xget_h :
forall (A: Set) (m: t A) (i: positive), get i m = xget i xH m.
Lemma xelements_complete:
forall (A: Set) (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: Set) (m: t A) (i: positive) (v: A),
In (i, v) (elements m) -> get i m = Some v.
Lemma in_xelements:
forall (A: Set) (m: t A) (i k: positive) (v: A),
In (k, v) (xelements m i) ->
exists j, k = append i j.
Definition xkeys (A: Set) (m: t A) (i: positive) :=
List.map (@fst positive A) (xelements m i).
Lemma in_xkeys:
forall (A: Set) (m: t A) (i k: positive),
In k (xkeys m i) ->
exists j, k = append i j.
Remark list_append_cons_norepet:
forall (A: Set) (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 ++ cons x l2).
Lemma append_injective:
forall i j1 j2, append i j1 = append i j2 -> j1 = j2.
Lemma xelements_keys_norepet:
forall (A: Set) (m: t A) (i: positive),
list_norepet (xkeys m i).
Theorem elements_keys_norepet:
forall (A: Set) (m: t A),
list_norepet (List.map (@fst elt A) (elements m)).
Definition fold (A B : Set) (f: B -> positive -> A -> B) (tr: t A) (v: B) :=
List.fold_left (fun a p => f a (fst p) (snd p)) (elements tr) v.
Theorem fold_spec:
forall (A B: Set) (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
|
Module PMap <: MAP.
Definition elt := positive.
Definition elt_eq := peq.
Definition t (A : Set) : Set := (A * PTree.t A)%type.
Definition init (A : Set) (x : A) :=
(x, PTree.empty A).
Definition get (A : Set) (i : positive) (m : t A) :=
match PTree.get i (snd m) with
| Some x => x
| None => fst m
end.
Definition set (A : Set) (i : positive) (x : A) (m : t A) :=
(fst m, PTree.set i x (snd m)).
Theorem gi:
forall (A: Set) (i: positive) (x: A), get i (init x) = x.
Theorem gss:
forall (A: Set) (i: positive) (x: A) (m: t A), get i (set i x m) = x.
Theorem gso:
forall (A: Set) (i j: positive) (x: A) (m: t A),
i <> j -> get i (set j x m) = get i m.
Theorem gsspec:
forall (A: Set) (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: Set) (i j: positive) (m: t A),
get j (set i (get i m) m) = get j m.
Definition map (A B : Set) (f : A -> B) (m : t A) : t B :=
(f (fst m), PTree.map (fun _ => f) (snd m)).
Theorem gmap:
forall (A B: Set) (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
|
Module Type INDEXED_TYPE.
Variable t: Set.
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}.
Variable invert : positive -> t.
Hypothesis invert_index : forall x, invert (index x) = x.
End INDEXED_TYPE.
Module IMap(X: INDEXED_TYPE).
Definition elt := X.t.
Definition elt_eq := X.eq.
Definition t : Set -> Set := PMap.t.
Definition init (A: Set) (x: A) := PMap.init x.
Definition get (A: Set) (i: X.t) (m: t A) := PMap.get (X.index i) m.
Definition set (A: Set) (i: X.t) (v: A) (m: t A) := PMap.set (X.index i) v m.
Definition map (A B: Set) (f: A -> B) (m: t A) : t B := PMap.map f m.
Lemma gi:
forall (A: Set) (x: A) (i: X.t), get i (init x) = x.
Lemma gss:
forall (A: Set) (i: X.t) (x: A) (m: t A), get i (set i x m) = x.
Lemma gso:
forall (A: Set) (i j: X.t) (x: A) (m: t A),
i <> j -> get i (set j x m) = get i m.
Lemma gsspec:
forall (A: Set) (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: Set) (f: A -> B) (i: X.t) (m: t A),
get i (map f m) = f(get i m).
Definition elements (A : Set) (m : t A) : A * list (X.t * A) :=
(fst m, List.map (fun kv => (X.invert (fst kv), snd kv)) (PTree.elements (snd m))).
Definition subMap : forall (A : Set) (p : A -> A -> Prop)
(f : forall t1 t2, pred_option (p t1 t2)) (m1 m2 : t A),
pred_option (forall r, p (get r m1) (get r m2)).
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.
Definition invert (x : positive) :=
match x with
| xH => Z0
| xO p => Zpos p
| xI p => Zneg p
end.
Theorem invert_index : forall x, invert (index x) = x.
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}.
Definition invert (x : positive) :=
match x with
| xO p => Npos p
| _ => N0
end.
Theorem invert_index : forall x, invert (index x) = x.
End NIndexed.
Module NMap := IMap(NIndexed).
An implementation of maps over any type with decidable equality |
Module Type EQUALITY_TYPE.
Variable t: Set.
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: Set) := X.t -> A.
Definition init (A: Set) (v: A) := fun (_: X.t) => v.
Definition get (A: Set) (x: X.t) (m: t A) := m x.
Definition set (A: Set) (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: Set) (i: elt) (x: A), init x i = x.
Lemma gss:
forall (A: Set) (i: elt) (x: A) (m: t A), (set i x m) i = x.
Lemma gso:
forall (A: Set) (i j: elt) (x: A) (m: t A),
i <> j -> (set j x m) i = m i.
Lemma gsspec:
forall (A: Set) (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: Set) (i j: elt) (m: t A), get j (set i (get i m) m) = get j m.
Definition map (A B: Set) (f: A -> B) (m: t A) :=
fun (x: X.t) => f(m x).
Lemma gmap:
forall (A B: Set) (f: A -> B) (i: elt) (m: t A),
get i (map f m) = f(get i m).
Lemma exten:
forall (A: Set) (m1 m2: t A),
(forall x: X.t, m1 x = m2 x) -> m1 = m2.
End EMap.
Useful notations |
Notation "a ! b" := (PTree.get b a) (at level 1).
Notation "a !! b" := (PMap.get b a) (at level 1).