Library CTPC.Dict
Require Import List.
Set Implicit Arguments.
Module Type DICT_DOMAIN.
Parameter A : Set.
Parameter A_eq_dec : forall (x y : A), {x = y} + {x <> y}.
End DICT_DOMAIN.
Module Type DICT.
Parameter A : Set.
Parameter dict : Set -> Set.
Parameter empty : forall B : Set, B -> dict B.
Parameter upd : forall B : Set, dict B -> A -> B -> dict B.
Parameter sel : forall B : Set, dict B -> A -> B.
Axiom sel_empty : forall (B : Set) (v : B) (a : A),
sel (empty v) a = v.
Axiom sel_upd_eq : forall (B : Set) (d : dict B) (a : A) (v : B),
sel (upd d a v) a = v.
Axiom sel_upd_ne : forall (B : Set) (d : dict B) (a : A) (v : B) (a' : A),
a' <> a
-> sel (upd d a v) a' = sel d a'.
Parameter dict_eq_dec : forall (B : Set) (B_eq_dec : forall (x y : B), {x = y} + {x <> y})
(d1 d2 : dict B), {d1 = d2} + {d1 <> d2}.
Axiom empty_inj : forall (B : Set) (d : dict B) (a : A) (v1 v2 : B),
empty v1 <> upd d a v2.
Axiom upd_inj : forall (B : Set) (d1 d2 : dict B) (a1 a2 : A) (v1 v2 : B),
upd d1 a1 v1 = upd d2 a2 v2
-> d1 = d2 /\ a1 = a2 /\ v1 = v2.
Parameter keys : forall B, dict B -> list A.
Parameter default : forall B, dict B -> B.
Axiom keys_empty : forall (B : Set) (v : B),
keys (empty v) = nil.
Axiom keys_upd : forall (B : Set) (d : dict B) (a : A) (v : B),
keys (upd d a v) = a :: keys d.
Axiom keys_ok : forall B (d : dict B) a,
~In a (keys d)
-> sel d a = default d.
End DICT.
Module Dict (Dom : DICT_DOMAIN) : DICT
with Definition A := Dom.A.
Import Dom.
Section Range.
Variable B : Set.
Definition dict := (B * list (A * B))%type.
Definition empty (v : B) : dict := (v, nil).
Definition upd (d : dict) (a : A) (v : B) : dict :=
(fst d, (a, v) :: snd d).
Fixpoint sel' (ls : list (A * B)) (a : A) {struct ls} : option B :=
match ls with
| nil => None
| (a', b) :: ls' =>
if A_eq_dec a a'
then Some b
else sel' ls' a
end.
Definition sel (d : dict) (a : A) : B :=
match sel' (snd d) a with
| None => fst d
| Some v => v
end.
Theorem sel_empty : forall (v : B) (a : A),
sel (empty v) a = v.
Theorem sel_upd_eq : forall (d : dict) (a : A) (v : B),
sel (upd d a v) a = v.
Theorem sel_upd_ne : forall (d : dict) (a : A) (v : B) (a' : A),
a' <> a
-> sel (upd d a v) a' = sel d a'.
Definition dict_eq_dec : forall (B_eq_dec : forall (x y : B), {x = y} + {x <> y})
(d1 d2 : dict), {d1 = d2} + {d1 <> d2}.
Theorem empty_inj : forall (d : dict) (a : A) (v1 v2 : B),
empty v1 <> upd d a v2.
Theorem upd_inj : forall (d1 d2 : dict) (a1 a2 : A) (v1 v2 : B),
upd d1 a1 v1 = upd d2 a2 v2
-> d1 = d2 /\ a1 = a2 /\ v1 = v2.
Definition keys (d : dict) : list A := map (fun p => fst p) (snd d).
Definition default (d : dict) : B := fst d.
Theorem keys_ok' : forall d a,
~In a (map (fun p => fst p) d)
-> sel' d a = None.
Theorem keys_empty : forall (v : B),
keys (empty v) = nil.
Theorem keys_upd : forall (d : dict) (a : A) (v : B),
keys (upd d a v) = a :: keys d.
Theorem keys_ok : forall (d : dict) a,
~In a (keys d)
-> sel d a = default d.
End Range.
Definition A := A.
End Dict.
Index
This page has been generated by coqdoc