Library AssocList
Require Import Decidable.
Require Import FSetWeak.
Require Import List.
Require Import AdditionalTactics.
Require Import ListFacts.
Require Import FSetWeakDecide.
We implement association lists as a functor over an implementation
of finite sets of keys. This allows us to define a domain
function on association lists that returns a finite set of keys,
as opposed to, say, a list of keys. Note that the
UsualDecidableType
argument requires that equality on keys be
eq
(Coq's "built-in" equality) and decidable.
Note that our library has an implicit convention for the "normal
form" of an association list. This normal form requires that a
list be built only from
This allows association lists to be written in a slightly more uniform manner when compared to using both
We have considered other alternative implementations, but the scheme described above seems to work the best in practice.
nil
(the empty list), one
(the
singleton list), and app
(concatenation). Additionally,
concatenations should be associated to the right and the list
should not contain any nil
terms, unless it is the empty list
itself.
This allows association lists to be written in a slightly more uniform manner when compared to using both
cons
and app
to
build them. The downsides are that Coq's simpl
tactic will
simplify instances of one
down to cons
and that there are
instances in which one needs to write association lists that are
not in normal form (typically, some concatenation will need to be
associated to the left). The simpl_alist
and rewrite_alist
tactics below are designed to minimize the impact of these
downsides.
We have considered other alternative implementations, but the scheme described above seems to work the best in practice.
Module Make
(X : UsualDecidableType)
(Import KeySet : FSetWeakInterface.S with Module E := X).
Module Import D := Decide KeySet.
Module KeySetProperties := Properties KeySet.
This section defines the following basic operations and
predicates on association lists.
Implicit arguments are declared by default for these definitions. We define some local notations to make the definition of
-
one
: Constructs an association list consisting of exactly one binding. -
map
: Maps a function over the values in an association list. -
dom
: Computes the domain of an association list, i.e., the set consisting of its keys. -
disjoint
: Binary predicate that holds when the domains of two association lists are disjoint. -
binds
: Ternary predicate that holds when a key-value pair appears somewhere in an association list. -
uniq
: Unary predicate that holds when an association list binds any given key at most once. Note thatuniq_push
is defined in terms ofone
, due to our normal form for association lists.
Implicit arguments are declared by default for these definitions. We define some local notations to make the definition of
uniq
easier to read and to be consistent with
the notations used in the rest of this library.
Section Definitions.
Variables A B C : Type.
Definition one (C : Type) (item : C) : list C := cons item nil.
Definition map (f : A -> B) (E : list (X.t*A)) : list (X.t*B) :=
List.map (fun b => match b with (x, a) => (x, f a) end) E.
Fixpoint dom (A : Type) (E : list (X.t*A)) {struct E} : KeySet.t :=
match E with
| nil => empty
| (x, _) :: E' => add x (dom E')
end.
Definition disjoint (E : list (X.t*A)) (F : list (X.t*B)) : Prop :=
Subset (inter (dom E) (dom F)) empty.
Definition binds (x : X.t) (a : A) (E : list (X.t*A)) : Prop :=
List.In (x, a) E.
Notation Local "x ~ a" := (one (x, a)) (at level 68).
Notation Local "x `notin` E" := (~ KeySet.In x E) (at level 69).
Inductive uniq : list (X.t*A) -> Prop :=
| uniq_nil :
uniq nil
| uniq_push : forall x a E,
uniq E ->
x `notin` dom E ->
uniq ((x ~ a) ++ E).
End Definitions.
We make a local notation for
one
, and for operations and
predicate on finite sets, in order to make the statements of the
lemmas below more readable. The notations are local so that
users of this functor may choose their own notations.
Notation Local "[ i ]" := (one i).
Notation Local "x ~ T" := (one (x, T)) (at level 68).
Notation Local "E `union` F" :=
(KeySet.union E F) (at level 69, right associativity).
Notation Local "x `in` E" :=
(KeySet.In x E) (at level 69).
Notation Local "x `notin` E" :=
(~ KeySet.In x E) (at level 69).
Notation Local "E [=] F" :=
(KeySet.Equal E F) (at level 70, no associativity).
Notation Local "E [<=] F" :=
(KeySet.Subset E F) (at level 70, no associativity).
The following block of properties is used mainly for rewriting
association lists into the normal form described above. See the
simpl_alist
and rewrite_alist
tactics below.
Section ListProperties.
Variables X : Type.
Variables x y : X.
Variables l l1 l2 l3 : list X.
Lemma cons_app_one :
cons x l = [ x ] ++ l.
Lemma cons_app_assoc :
(cons x l1) ++ l2 = cons x (l1 ++ l2).
Lemma app_assoc :
(l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
Lemma app_nil_1 :
nil ++ l = l.
Lemma app_nil_2 :
l ++ nil = l.
Lemma in_one :
List.In x [ y ] <-> x = y.
Lemma in_app :
List.In x (l1 ++ l2) <-> List.In x l1 \/ List.In x l2.
End ListProperties.
Hint Rewrite cons_app_one cons_app_assoc app_assoc : rewr_list.
Hint Rewrite app_nil_1 app_nil_2 : rewr_list.
Hint Rewrite in_one in_app : rewr_list_in.
The following block of properties is an assortment of
structural properties about lists.
Section AssortedListProperties.
Variables X : Type.
Variables x y : X.
Variables l l1 l2 l3 : list X.
Lemma one_eq_app :
[ x ] ++ l1 = l2 ++ l3 ->
(exists qs, l2 = x :: qs /\ l1 = qs ++ l3) \/
(l2 = nil /\ l3 = x :: l1).
Lemma app_eq_one :
l2 ++ l3 = [ x ] ++ l1 ->
(exists qs, l2 = x :: qs /\ l1 = qs ++ l3) \/
(l2 = nil /\ l3 = x :: l1).
Lemma nil_neq_one_mid :
nil <> l1 ++ [ x ] ++ l2.
Lemma one_mid_neq_nil :
l1 ++ [ x ] ++ l2 <> nil.
End AssortedListProperties.
The following lemmas are used mainly to simplify applications of
map
and dom
to association lists. See also the simpl_alist
and rewrite_alist
tactics below.
Section Properties.
Variables A B : Type.
Variables f : A -> B.
Variables x : X.t.
Variables b : A.
Variables E F G : list (X.t*A).
Lemma map_nil :
map f nil = nil.
Lemma map_cons :
map f ((x, b) :: E) = (x, f b) :: map f E.
Lemma map_one :
map f (x ~ b) = (x ~ f b).
Lemma map_app :
map f (E ++ F) = map f E ++ map f F.
Lemma dom_nil :
(@dom A nil) = empty.
Lemma dom_cons :
dom ((x, b) :: E) [=] singleton x `union` dom E.
Lemma dom_one :
dom (x ~ b) [=] singleton x.
Lemma dom_app :
dom (E ++ F) [=] dom E `union` dom F.
Lemma dom_map :
dom (map f E) [=] dom E.
End Properties.
Hint Rewrite map_nil map_cons map_one map_app : rewr_map.
Hint Rewrite dom_nil dom_cons dom_one dom_app dom_map : rewr_dom.
The
simpl_alist
tactic rewrites association lists so that they
are in the normal form described above. Similar to the simpl
tactic, we define "in *
" and "in H
" variants of the tactic.
Ltac simpl_alist :=
autorewrite with rewr_list rewr_list_in rewr_map rewr_dom.
Tactic Notation "simpl_alist" "in" hyp(H) :=
autorewrite with rewr_list rewr_list_in rewr_map rewr_dom in H.
Tactic Notation "simpl_alist" "in" "*" :=
autorewrite with rewr_list rewr_list_in rewr_map rewr_dom in *.
The tactic
(rewrite_alist E)
replaces an association list in
the conclusion of the goal with E
. Suitability for
replacement is determined by whether simpl_alist
can put E
and the chosen environment in the same normal form, up to
convertibility's in Coq. We also define an "in H
" variant
that performs the replacement in a hypothesis H
.
Tactic Notation "rewrite_alist" constr(E) :=
match goal with
| |- context[?x] =>
change x with E
| |- context[?x] =>
replace x with E;
[ | try reflexivity; simpl_alist; reflexivity ]
end.
Tactic Notation "rewrite_alist" constr(E) "in" hyp(H) :=
match type of H with
| context[?x] =>
change x with E in H
| context[?x] =>
replace x with E in H;
[ | try reflexivity; simpl_alist; reflexivity ]
end.
Section BasicDisjointFacts.
Implicit Types A B C : Type.
Lemma disjoint_sym_1 :
forall A B (E : list (X.t*A)) (F : list (X.t*B)),
disjoint E F ->
disjoint F E.
Lemma disjoint_sym :
forall A B (E : list (X.t*A)) (F : list (X.t*B)),
disjoint E F <-> disjoint F E.
Lemma disjoint_one_1 :
forall A B (x : X.t) (a : A) (F : list (X.t*B)),
disjoint (x ~ a) F ->
x `notin` dom F.
Lemma disjoint_one_2 :
forall A B (x : X.t) (a : A) (F : list (X.t*B)),
x `notin` dom F ->
disjoint (x ~ a) F.
Lemma disjoint_one_l :
forall A B (x : X.t) (a : A) (E : list (X.t*B)),
disjoint (x ~ a) E <-> x `notin` dom E.
Lemma disjoint_one_r :
forall A B (x : X.t) (a : A) (E : list (X.t*B)),
disjoint E (x ~ a) <-> x `notin` dom E.
Lemma disjoint_app_1 :
forall A B (E F : list (X.t*A)) (G : list (X.t*B)),
disjoint (E ++ F) G ->
disjoint E G.
Lemma disjoint_app_2 :
forall A B (E F : list (X.t*A)) (G : list (X.t*B)),
disjoint (E ++ F) G ->
disjoint F G.
Lemma disjoint_app_3 :
forall A B (E F : list (X.t*A)) (G : list (X.t*B)),
disjoint E G ->
disjoint F G ->
disjoint (E ++ F) G.
Lemma disjoint_app_l :
forall A B (E F : list (X.t*A)) (G : list (X.t*B)),
disjoint (E ++ F) G <-> disjoint E G /\ disjoint F G.
Lemma disjoint_app_r :
forall A B (E F : list (X.t*A)) (G : list (X.t*B)),
disjoint G (E ++ F) <-> disjoint E G /\ disjoint F G.
Lemma disjoint_map_1 :
forall A B C (E : list (X.t*A)) (F : list (X.t*B)) (f : A -> C),
disjoint (map f E) F ->
disjoint E F.
Lemma disjoint_map_2 :
forall A B C (E : list (X.t*A)) (F : list (X.t*B)) (f : A -> C),
disjoint E F ->
disjoint (map f E) F.
Lemma disjoint_map_l :
forall A B C (E : list (X.t*A)) (F : list (X.t*B)) (f : A -> C),
disjoint (map f E) F <-> disjoint E F.
Lemma disjoint_map_r :
forall A B C (E : list (X.t*A)) (F : list (X.t*B)) (f : A -> C),
disjoint F (map f E) <-> disjoint E F.
End BasicDisjointFacts.
The following lemmas are facts about
uniq
with respect to the
basic functions (one
, app
, and map
) that can be used to
build association lists.
Section UniqProperties.
Variables A B : Type.
Variables f : A -> B.
Variables x : X.t.
Variables b : A.
Variables E F G : list (X.t*A).
Lemma uniq_one :
uniq (x ~ b).
Lemma uniq_app_1 :
uniq (E ++ F) -> uniq E.
Lemma uniq_app_2 :
uniq (E ++ F) -> uniq F.
Lemma uniq_app_3 :
uniq (E ++ F) -> disjoint E F.
Lemma uniq_app_4 :
uniq E ->
uniq F ->
disjoint E F ->
uniq (E ++ F).
Lemma uniq_app :
uniq (E ++ F) <-> uniq E /\ uniq F /\ disjoint E F.
Lemma uniq_map_1 :
uniq (map f E) ->
uniq E.
Lemma uniq_map_2 :
uniq E ->
uniq (map f E).
Lemma uniq_map :
uniq (map f E) <-> uniq E.
End UniqProperties.
Hint Rewrite
disjoint_one_l disjoint_one_r
disjoint_app_l disjoint_app_r
disjoint_map_l disjoint_map_r
uniq_app uniq_map
: rewr_uniq.
This tactic attempts to solve goals about
Implementation note: The second
uniq
. Given its
definition, it's likely to work only when the hypotheses in the
goal already contain all the relevant uniq
propositions.
Thus, the tactic may not be generally useful. It is useful,
however, for proving facts about uniq
such as the ones below.
Implementation note: The second
simpl_alist
in the definition
is because of disjoint_one_{l,r}
. The "|| fail
" at the end
is so that in the case of failure, the error message reported to
the user is not the one from fsetdec
.
Ltac solve_uniq :=
try trivial;
simpl_alist in *;
autorewrite with rewr_uniq in *;
simpl_alist in *;
intuition (
auto using uniq_nil, uniq_one ||
(rewrite -> disjoint_sym; auto) ||
(unfold disjoint in *; fsetdec))
|| fail.
Section UniqDerived.
Variables A : Type.
Variables x y : X.t.
Variables a b : A.
Variables E F G : list (X.t*A).
Lemma uniq_cons :
uniq E ->
x `notin` dom E ->
uniq ((x, a) :: E).
Lemma uniq_insert_mid :
uniq (G ++ E) ->
x `notin` dom (G ++ E) ->
uniq (G ++ (x ~ a) ++ E).
Lemma uniq_remove_mid :
uniq (E ++ F ++ G) ->
uniq (E ++ G).
Lemma uniq_map_app_l : forall (f : A -> A),
uniq (F ++ E) ->
uniq (map f F ++ E).
Lemma fresh_mid_tail :
uniq (F ++ (x ~ a) ++ E) ->
x `notin` dom E.
Lemma fresh_mid_head :
uniq (F ++ (x ~ a) ++ E) ->
x `notin` dom E.
End UniqDerived.
The following lemmas are facts about
Note:
binds
with respect to the
basic functions (one
and app
) that can be used to build
association lists.
Note:
map
is treated further below.
Section BindsProperties.
Variables A : Type.
Variables x y : X.t.
Variables a b : A.
Variables E F G : list (X.t*A).
Lemma binds_nil :
binds x a nil <-> False.
Lemma binds_one_1 :
x = y ->
a = b ->
binds x a (y ~ b).
Lemma binds_one_2 :
binds x a (y ~ b) ->
x = y.
Lemma binds_one_3 :
binds x a (y ~ b) ->
a = b.
Lemma binds_one :
binds x a (y ~ b) <-> x = y /\ a = b.
Lemma binds_app_1 :
binds x a E ->
binds x a (E ++ F).
Lemma binds_app_2 :
binds x a F ->
binds x a (E ++ F).
Lemma binds_app_3 :
binds x a (E ++ F) ->
binds x a E \/ binds x a F.
Lemma binds_app :
binds x a (E ++ F) <-> binds x a E \/ binds x a F.
End BindsProperties.
Hint Rewrite binds_nil binds_one binds_app : rewr_binds.
Hint Rewrite binds_nil binds_one : rewr_binds_uniq.
Section MoreBindsProperties.
Variables A : Type.
Variables x y : X.t.
Variables a b : A.
Variables E F G : list (X.t*A).
Lemma binds_dom_contradiction: forall (E : list (X.t*A)),
binds x a E ->
x `notin` dom E ->
False.
Lemma binds_app_uniq :
uniq (E ++ F) ->
(binds x a (E ++ F) <->
(binds x a E /\ x `notin` dom F) \/
(binds x a F /\ x `notin` dom E)).
End MoreBindsProperties.
Hint Rewrite binds_app_uniq using solve_uniq : rewr_binds_uniq.
The
apply_binds_dom_contradiction
tactic solves a goal by
applying the binds_dom_contradiction
lemma. The tactic
succeeds only if the the hypotheses of the lemma are immediately
satisfied.
Ltac apply_binds_dom_contradiction :=
match goal with
| H : binds ?x ?a ?E, J : ?x `notin` (dom ?E) |- _ =>
assert False by apply (@binds_dom_contradiction _ _ _ _ H J);
intuition
| H : binds ?x ?a ?E, J : ?x `in` (dom ?E) -> False |- _ =>
assert False by apply (@binds_dom_contradiction _ _ _ _ H J);
intuition
end.
The
solve_binds
tactic attempts to solve goals about binds
.
Given its definition, it's likely to work only when the
hypotheses in the goal already contain all the relevant binds
propositions. Thus, the tactic may not be generally useful. It
is useful, however, for proving facts about binds
such as the
ones below.
Ltac solve_binds :=
simpl_alist in *;
autorewrite with rewr_binds in *;
intuition (auto || fsetdec || apply_binds_dom_contradiction)
|| fail.
The tactics
Implementation notes:
analyze_binds
and analyze_binds_uniq
tactics
take as an argument a hypotheses about binds
and perform a
case analysis based on the structure of the association list.
In the case of analyze_binds_uniq
, the analysis is performed
assuming that the association list is uniq
. The lemmas
binds_app
and binds_app_uniq
are examples of such case
analysis.
Implementation notes:
- The initial calls to
simpl_alist
put the relevant association lists into normal form. - In the case of
binds_app_uniq
, we assert that the association list isuniq
. This enables theautorewrite
step to succeed. - Rather than work on
H
itself, we copy it and work on the copy. Thus, in instances where the analysis leaves unsolved subgoals, it is still possible to see the original hypothesis. - The rest of the tactic breaks apart the copy of H and tries several simple means for solving the resulting subgoals.
Ltac analyze_binds H :=
simpl_alist;
simpl_alist in H;
match type of H with
| binds ?x ?a ?E =>
let J := fresh in
pose proof H as J;
autorewrite with rewr_binds in J;
simpl_alist in J;
try (progress decompose [and or] J; clear J);
try solve [trivial | discriminate | intuition | fsetdec]
end.
Ltac analyze_binds_uniq H :=
simpl_alist;
simpl_alist in H;
match type of H with
| binds ?x ?a ?E =>
match goal with
| H : uniq ?E |- _ => idtac
| _ => assert (uniq E); [ try solve_uniq | ]
end;
let J := fresh in
pose proof H as J;
autorewrite with rewr_binds_uniq in J;
simpl_alist in J;
try (progress decompose [and or] J; clear J);
try solve [trivial | discriminate | intuition | fsetdec]
end.
Section BindsDerived.
Variables A B : Type.
Variables f : A -> B.
Variables x y : X.t.
Variables a b : A.
Variables E F G : list (X.t*A).
Lemma binds_dec :
(forall a b : A, {a = b} + {a <> b}) ->
{binds x a E} + {~ binds x a E}.
Lemma binds_lookup_dec :
decidable (exists a, binds x a E).
Lemma binds_lookup_dec_specif :
{a : A | binds x a E} + (forall a, ~ binds x a E).
Lemma binds_map :
binds x a E ->
binds x (f a) (map f E).
Lemma binds_map_inv :
(forall a b, f a = f b -> a = b) ->
binds x (f a) (map f E) ->
binds x a E.
Lemma binds_weaken :
binds x a (E ++ G) ->
binds x a (E ++ F ++ G).
Lemma binds_mid_eq :
binds x a (F ++ (x ~ b) ++ E) ->
uniq (F ++ (x ~ b) ++ E) ->
a = b.
Lemma binds_remove_mid :
binds x a (F ++ (y ~ b) ++ G) ->
x <> y ->
binds x a (F ++ G).
Lemma binds_In : forall x a (E : list (X.t*A)),
binds x a E ->
x `in` dom E.
Lemma binds_unique :
binds x a E ->
binds x b E ->
uniq E ->
a = b.
Lemma fresh_app_l :
uniq (F ++ E) ->
binds x a E ->
x `notin` dom F.
Lemma fresh_app_r :
uniq (F ++ E) ->
binds x a F ->
x `notin` dom E.
End BindsDerived.
End Make.
This page has been generated by coqdoc