Library TreeAl
Require Import
Coqlib
Maps
DLib.
Set Implicit Arguments.
Module Type TYPE_EQ.
Variable s: Type.
Variable t: Type.
Variable t_of_s : s → t.
Variable s_of_t : t → s.
Hypothesis inj : ∀ x : s, s_of_t (t_of_s x) = x.
Hypothesis surj: ∀ x : t, t_of_s (s_of_t x) = x.
Variable eq: ∀ (x y: s), {x = y} + {x ≠ y}.
End TYPE_EQ.
Module TYPE_EQ_PROP (X:TYPE_EQ).
Lemma injective (a b: X.s) :
a ≠ b → X.t_of_s a ≠ X.t_of_s b.
Corollary injective' (a b: X.s) :
X.t_of_s a = X.t_of_s b → a = b.
Lemma tinjective (a b: X.t) :
a ≠ b → X.s_of_t a ≠ X.s_of_t b.
Lemma tinjective' (a b: X.t) :
X.s_of_t a = X.s_of_t b → a = b.
End TYPE_EQ_PROP.
Module Z_EQ_POS : TYPE_EQ
with Definition s := Z
with Definition t := positive.
Definition s := Z.
Definition t := positive.
Definition t_of_s (z: s) : t :=
match z with
| Z0 ⇒ xH
| Zpos p ⇒ xO p
| Zneg p ⇒ xI p
end.
Definition s_of_t (p: t) : s :=
match p with
| xH ⇒ Z0
| xO x ⇒ Zpos x
| xI x ⇒ Zneg x
end.
Lemma inj : ∀ x : s, s_of_t (t_of_s x) = x.
Lemma surj: ∀ x : t, t_of_s (s_of_t x) = x.
Definition eq: ∀ (x y: s), {x = y} + {x ≠ y} :=
Z_eq_dec.
End Z_EQ_POS.
Lemma fold_left_map:
∀ {A B C} (f: A → B) (g: C → B → C) xs a,
fold_left g (map f xs) a = fold_left (fun a x ⇒ g a (f x)) xs a.
Module BijTree (X:TYPE_EQ) (TTree: TREE with Definition elt := X.t) <: TREE.
Module P := TYPE_EQ_PROP(X).
Hint Resolve P.injective P.injective' P.tinjective P.tinjective'.
Definition elt: Type := X.s.
Definition elt_eq: ∀ (a b: elt), {a = b} + {a ≠ b} := X.eq.
Definition t: Type → Type := TTree.t.
Definition empty: ∀ (A: Type), t A := TTree.empty.
Definition get A i g : option A := TTree.get (X.t_of_s i) g.
Definition set A i v g : t A := TTree.set (X.t_of_s i) v g.
Definition remove A i g : t A := TTree.remove (X.t_of_s i) g.
Lemma gempty: ∀ (A: Type) (i: elt), get i (empty A) = None.
Lemma gss: ∀ (A: Type) (i: elt) (x: A) (m: t A), get i (set i x m) = Some x.
Lemma gso: ∀ (A: Type) (i j: elt) (x: A) (m: t A),
i ≠ j → get i (set j x m) = get i m.
Lemma 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.
Lemma gsident: ∀ (A: Type) (i: elt) (m: t A) (v: A),
get i m = Some v → set i v m = m.
Lemma grs: ∀ (A: Type) (i: elt) (m: t A), get i (remove i m) = None.
Lemma gro: ∀ (A: Type) (i j: elt) (m: t A),
i ≠ j → get i (remove j m) = get i m.
Lemma 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.
Definition beq A cmp (t1 t2: t A) : bool :=
TTree.beq cmp t1 t2.
Lemma beq_correct:
∀ (A: Type) (eqA: A → A → bool) (t1 t2: t A),
beq eqA t1 t2 = true ↔
(∀ (x: elt),
match get x t1, get x t2 with
| None, None ⇒ True
| Some y1, Some y2 ⇒ eqA y1 y2 = true
| _, _ ⇒ False
end).
Coqlib
Maps
DLib.
Set Implicit Arguments.
Module Type TYPE_EQ.
Variable s: Type.
Variable t: Type.
Variable t_of_s : s → t.
Variable s_of_t : t → s.
Hypothesis inj : ∀ x : s, s_of_t (t_of_s x) = x.
Hypothesis surj: ∀ x : t, t_of_s (s_of_t x) = x.
Variable eq: ∀ (x y: s), {x = y} + {x ≠ y}.
End TYPE_EQ.
Module TYPE_EQ_PROP (X:TYPE_EQ).
Lemma injective (a b: X.s) :
a ≠ b → X.t_of_s a ≠ X.t_of_s b.
Corollary injective' (a b: X.s) :
X.t_of_s a = X.t_of_s b → a = b.
Lemma tinjective (a b: X.t) :
a ≠ b → X.s_of_t a ≠ X.s_of_t b.
Lemma tinjective' (a b: X.t) :
X.s_of_t a = X.s_of_t b → a = b.
End TYPE_EQ_PROP.
Module Z_EQ_POS : TYPE_EQ
with Definition s := Z
with Definition t := positive.
Definition s := Z.
Definition t := positive.
Definition t_of_s (z: s) : t :=
match z with
| Z0 ⇒ xH
| Zpos p ⇒ xO p
| Zneg p ⇒ xI p
end.
Definition s_of_t (p: t) : s :=
match p with
| xH ⇒ Z0
| xO x ⇒ Zpos x
| xI x ⇒ Zneg x
end.
Lemma inj : ∀ x : s, s_of_t (t_of_s x) = x.
Lemma surj: ∀ x : t, t_of_s (s_of_t x) = x.
Definition eq: ∀ (x y: s), {x = y} + {x ≠ y} :=
Z_eq_dec.
End Z_EQ_POS.
Lemma fold_left_map:
∀ {A B C} (f: A → B) (g: C → B → C) xs a,
fold_left g (map f xs) a = fold_left (fun a x ⇒ g a (f x)) xs a.
Module BijTree (X:TYPE_EQ) (TTree: TREE with Definition elt := X.t) <: TREE.
Module P := TYPE_EQ_PROP(X).
Hint Resolve P.injective P.injective' P.tinjective P.tinjective'.
Definition elt: Type := X.s.
Definition elt_eq: ∀ (a b: elt), {a = b} + {a ≠ b} := X.eq.
Definition t: Type → Type := TTree.t.
Definition empty: ∀ (A: Type), t A := TTree.empty.
Definition get A i g : option A := TTree.get (X.t_of_s i) g.
Definition set A i v g : t A := TTree.set (X.t_of_s i) v g.
Definition remove A i g : t A := TTree.remove (X.t_of_s i) g.
Lemma gempty: ∀ (A: Type) (i: elt), get i (empty A) = None.
Lemma gss: ∀ (A: Type) (i: elt) (x: A) (m: t A), get i (set i x m) = Some x.
Lemma gso: ∀ (A: Type) (i j: elt) (x: A) (m: t A),
i ≠ j → get i (set j x m) = get i m.
Lemma 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.
Lemma gsident: ∀ (A: Type) (i: elt) (m: t A) (v: A),
get i m = Some v → set i v m = m.
Lemma grs: ∀ (A: Type) (i: elt) (m: t A), get i (remove i m) = None.
Lemma gro: ∀ (A: Type) (i j: elt) (m: t A),
i ≠ j → get i (remove j m) = get i m.
Lemma 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.
Definition beq A cmp (t1 t2: t A) : bool :=
TTree.beq cmp t1 t2.
Lemma beq_correct:
∀ (A: Type) (eqA: A → A → bool) (t1 t2: t A),
beq eqA t1 t2 = true ↔
(∀ (x: elt),
match get x t1, get x t2 with
| None, None ⇒ True
| Some y1, Some y2 ⇒ eqA y1 y2 = true
| _, _ ⇒ False
end).
Applying a function to all data of a tree.
Definition map A B (f: elt → A → B) (g: t A) : t B :=
TTree.map (fun e ⇒ (f (X.s_of_t e))) g.
Lemma gmap: ∀ (A B: Type) (f: elt → A → B) (i: elt) (m: t A),
get i (map f m) = option_map (f i) (get i m).
TTree.map (fun e ⇒ (f (X.s_of_t e))) g.
Lemma gmap: ∀ (A B: Type) (f: elt → A → B) (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.
Definition map1 A B (f: A → B) g := TTree.map1 f g.
Lemma gmap1:
∀ (A B: Type) (f: A → B) (i: elt) (m: t A),
get i (map1 f m) = option_map f (get i m).
Lemma gmap1:
∀ (A B: Type) (f: A → B) (i: elt) (m: t A),
get i (map1 f m) = option_map f (get i m).
Filtering data that match a given predicate. * )
Variable filter1:
forall (A: Type), (A -> bool) -> t A -> t A.
Hypothesis gfilter1:
forall (A: Type) (pred: A -> bool) (i: elt) (m: t A),
get i (filter1 pred m) =
match get i m with None => None | Some x => if pred x then Some x else None end.
Applying a function pairwise to all data of two trees.
Definition combine A B C (f:option A → option B → option C) g1 g2 : t C :=
TTree.combine f g1 g2.
Lemma gcombine:
∀ (A B C: Type) (f: option A → option B → option 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).
Lemma combine_commut:
∀ (A B: Type) (f g: option A → option A → option B),
(∀ (i j: option A), f i j = g j i) →
∀ (m1 m2: t A),
combine f m1 m2 = combine g m2 m1.
TTree.combine f g1 g2.
Lemma gcombine:
∀ (A B C: Type) (f: option A → option B → option 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).
Lemma combine_commut:
∀ (A B: Type) (f g: option A → option A → option 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.
Definition elements A g : list (elt × A) :=
List.map (fun q ⇒ (X.s_of_t (fst q), snd q))
(TTree.elements g).
Lemma elements_correct:
∀ (A: Type) (m: t A) (i: elt) (v: A),
get i m = Some v → In (i, v) (elements m).
Lemma elements_complete:
∀ (A: Type) (m: t A) (i: elt) (v: A),
In (i, v) (elements m) → get i m = Some v.
Lemma elements_keys_norepet:
∀ (A: Type) (m: t A),
list_norepet (List.map (@fst elt A) (elements m)).
List.map (fun q ⇒ (X.s_of_t (fst q), snd q))
(TTree.elements g).
Lemma elements_correct:
∀ (A: Type) (m: t A) (i: elt) (v: A),
get i m = Some v → In (i, v) (elements m).
Lemma elements_complete:
∀ (A: Type) (m: t A) (i: elt) (v: A),
In (i, v) (elements m) → get i m = Some v.
Lemma 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.
Definition fold A B f (g: t A) b : B :=
TTree.fold (fun x k v ⇒ f x (X.s_of_t k) v) g b.
Lemma fold_spec:
∀ (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.
TTree.fold (fun x k v ⇒ f x (X.s_of_t k) v) g b.
Lemma fold_spec:
∀ (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.
Folding a function over all rhs of bindings of a tree.
Definition fold1 A B f (g: t A) b : B :=
TTree.fold1 (fun x v ⇒ f x v) g b.
Lemma fold1_spec:
∀ (A B: Type) (f: B → A → B) (v: B) (m: t A),
fold1 f m v =
List.fold_left (fun a p ⇒ f a (snd p)) (elements m) v.
End BijTree.
Module ZTree <: TREE with Definition elt := Z := BijTree(Z_EQ_POS)(PTree).
Module SumTree (L:TREE) (R:TREE) <: TREE.
Definition elt := (L.elt + R.elt)%type.
Definition elt_eq: ∀ (a b: elt), {a = b} + {a ≠ b}.
Definition t (A: Type) : Type := (L.t A × R.t A)%type.
Definition empty A : t A := (L.empty A, R.empty A).
Definition get A k m : option A :=
match k with
| inl x ⇒ L.get x (fst m)
| inr x ⇒ R.get x (snd m)
end.
Definition set A k v m : t A :=
match k with
| inl x ⇒ (L.set x v (fst m), snd m)
| inr x ⇒ (fst m, R.set x v (snd m))
end.
Definition remove A k m : t A :=
match k with
| inl x ⇒ (L.remove x (fst m), snd m)
| inr x ⇒ (fst m, R.remove x (snd m))
end.
Lemma gempty:
∀ (A: Type) (i: elt), get i (empty A) = None.
Lemma gss:
∀ (A: Type) (i: elt) (x: A) (m: t A), get i (set i x m) = Some x.
Lemma gso:
∀ (A: Type) (i j: elt) (x: A) (m: t A),
i ≠ j → get i (set j x m) = get i m.
Lemma 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.
Lemma gsident:
∀ (A: Type) (i: elt) (m: t A) (v: A),
get i m = Some v → set i v m = m.
Lemma grs:
∀ (A: Type) (i: elt) (m: t A), get i (remove i m) = None.
Lemma gro:
∀ (A: Type) (i j: elt) (m: t A),
i ≠ j → get i (remove j m) = get i m.
Lemma 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.
TTree.fold1 (fun x v ⇒ f x v) g b.
Lemma fold1_spec:
∀ (A B: Type) (f: B → A → B) (v: B) (m: t A),
fold1 f m v =
List.fold_left (fun a p ⇒ f a (snd p)) (elements m) v.
End BijTree.
Module ZTree <: TREE with Definition elt := Z := BijTree(Z_EQ_POS)(PTree).
Module SumTree (L:TREE) (R:TREE) <: TREE.
Definition elt := (L.elt + R.elt)%type.
Definition elt_eq: ∀ (a b: elt), {a = b} + {a ≠ b}.
Definition t (A: Type) : Type := (L.t A × R.t A)%type.
Definition empty A : t A := (L.empty A, R.empty A).
Definition get A k m : option A :=
match k with
| inl x ⇒ L.get x (fst m)
| inr x ⇒ R.get x (snd m)
end.
Definition set A k v m : t A :=
match k with
| inl x ⇒ (L.set x v (fst m), snd m)
| inr x ⇒ (fst m, R.set x v (snd m))
end.
Definition remove A k m : t A :=
match k with
| inl x ⇒ (L.remove x (fst m), snd m)
| inr x ⇒ (fst m, R.remove x (snd m))
end.
Lemma gempty:
∀ (A: Type) (i: elt), get i (empty A) = None.
Lemma gss:
∀ (A: Type) (i: elt) (x: A) (m: t A), get i (set i x m) = Some x.
Lemma gso:
∀ (A: Type) (i j: elt) (x: A) (m: t A),
i ≠ j → get i (set j x m) = get i m.
Lemma 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.
Lemma gsident:
∀ (A: Type) (i: elt) (m: t A) (v: A),
get i m = Some v → set i v m = m.
Lemma grs:
∀ (A: Type) (i: elt) (m: t A), get i (remove i m) = None.
Lemma gro:
∀ (A: Type) (i j: elt) (m: t A),
i ≠ j → get i (remove j m) = get i m.
Lemma 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.
Definition beq A (cmp: A → A → bool) (m1 m2: t A) : bool :=
let '(l1, r1) := m1 in
let '(l2, r2) := m2 in
L.beq cmp l1 l2 && R.beq cmp r1 r2.
Lemma beq_correct:
∀ (A: Type) (eqA: A → A → bool) (t1 t2: t A),
beq eqA t1 t2 = true ↔
(∀ (x: elt),
match get x t1, get x t2 with
| None, None ⇒ True
| Some y1, Some y2 ⇒ eqA y1 y2 = true
| _, _ ⇒ False
end).
let '(l1, r1) := m1 in
let '(l2, r2) := m2 in
L.beq cmp l1 l2 && R.beq cmp r1 r2.
Lemma beq_correct:
∀ (A: Type) (eqA: A → A → bool) (t1 t2: t A),
beq eqA t1 t2 = true ↔
(∀ (x: elt),
match get x t1, get x t2 with
| None, None ⇒ True
| Some y1, Some y2 ⇒ eqA y1 y2 = true
| _, _ ⇒ False
end).
Applying a function to all data of a tree.
Definition map A B (f: elt → A → B) (m: t A) : t B :=
let '(l, r) := m in
(L.map (fun k ⇒ f (inl _ k)) l,
R.map (fun k ⇒ f (inr _ k)) r).
Lemma gmap:
∀ (A B: Type) (f: elt → A → B) (i: elt) (m: t A),
get i (map f m) = option_map (f i) (get i m).
Definition map1 A B (f: A → B) (m: t A) : t B :=
(L.map1 f (fst m), R.map1 f (snd m)).
Lemma gmap1:
∀ (A B: Type) (f: A → B) (i: elt) (m: t A),
get i (map1 f m) = option_map f (get i m).
Definition combine A B C (f: option A → option B → option C) (m1: t A) (m2: t B) : t C :=
let '(l1, r1) := m1 in
let '(l2, r2) := m2 in
(L.combine f l1 l2, R.combine f r1 r2).
Lemma gcombine:
∀ (A B C: Type) (f: option A → option B → option 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).
Lemma combine_commut:
∀ (A B: Type) (f g: option A → option A → option B),
(∀ (i j: option A), f i j = g j i) →
∀ (m1 m2: t A),
combine f m1 m2 = combine g m2 m1.
let '(l, r) := m in
(L.map (fun k ⇒ f (inl _ k)) l,
R.map (fun k ⇒ f (inr _ k)) r).
Lemma gmap:
∀ (A B: Type) (f: elt → A → B) (i: elt) (m: t A),
get i (map f m) = option_map (f i) (get i m).
Definition map1 A B (f: A → B) (m: t A) : t B :=
(L.map1 f (fst m), R.map1 f (snd m)).
Lemma gmap1:
∀ (A B: Type) (f: A → B) (i: elt) (m: t A),
get i (map1 f m) = option_map f (get i m).
Definition combine A B C (f: option A → option B → option C) (m1: t A) (m2: t B) : t C :=
let '(l1, r1) := m1 in
let '(l2, r2) := m2 in
(L.combine f l1 l2, R.combine f r1 r2).
Lemma gcombine:
∀ (A B C: Type) (f: option A → option B → option 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).
Lemma combine_commut:
∀ (A B: Type) (f g: option A → option A → option 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.
Definition elements A (m: t A) : list (elt × A) :=
(List.map (fun k ⇒ (inl _ (fst k), snd k)) (L.elements (fst m)))
++
(List.map (fun k ⇒ (inr _ (fst k), snd k)) (R.elements (snd m)))
.
Lemma elements_correct:
∀ (A: Type) (m: t A) (i: elt) (v: A),
get i m = Some v → In (i, v) (elements m).
Lemma elements_complete:
∀ (A: Type) (m: t A) (i: elt) (v: A),
In (i, v) (elements m) → get i m = Some v.
Lemma elements_keys_norepet:
∀ (A: Type) (m: t A),
list_norepet (List.map (@fst elt A) (elements m)).
Definition fold A B (f: B → elt → A → B) (m: t A) (v: B) : B :=
(R.fold (fun b k ⇒ f b (inr _ k)) (snd m)
(L.fold (fun b k ⇒ f b (inl _ k)) (fst m) v)).
Lemma fold_spec:
∀ (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.
Definition fold1 A B (f: B → A → B) (m: t A) (v: B) : B :=
(R.fold1 (fun b ⇒ f b) (snd m)
(L.fold1 (fun b ⇒ f b) (fst m) v)).
Lemma fold1_spec:
∀ (A B: Type) (f: B → A → B) (v: B) (m: t A),
fold1 f m v =
List.fold_left (fun a p ⇒ f a (snd p)) (elements m) v.
End SumTree.
(List.map (fun k ⇒ (inl _ (fst k), snd k)) (L.elements (fst m)))
++
(List.map (fun k ⇒ (inr _ (fst k), snd k)) (R.elements (snd m)))
.
Lemma elements_correct:
∀ (A: Type) (m: t A) (i: elt) (v: A),
get i m = Some v → In (i, v) (elements m).
Lemma elements_complete:
∀ (A: Type) (m: t A) (i: elt) (v: A),
In (i, v) (elements m) → get i m = Some v.
Lemma elements_keys_norepet:
∀ (A: Type) (m: t A),
list_norepet (List.map (@fst elt A) (elements m)).
Definition fold A B (f: B → elt → A → B) (m: t A) (v: B) : B :=
(R.fold (fun b k ⇒ f b (inr _ k)) (snd m)
(L.fold (fun b k ⇒ f b (inl _ k)) (fst m) v)).
Lemma fold_spec:
∀ (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.
Definition fold1 A B (f: B → A → B) (m: t A) (v: B) : B :=
(R.fold1 (fun b ⇒ f b) (snd m)
(L.fold1 (fun b ⇒ f b) (fst m) v)).
Lemma fold1_spec:
∀ (A B: Type) (f: B → A → B) (v: B) (m: t A),
fold1 f m v =
List.fold_left (fun a p ⇒ f a (snd p)) (elements m) v.
End SumTree.