Library AssocList
A library for association lists, i.e., lists of pairs
Require Import Coq.FSets.FSets.
Require Import Coq.Lists.List.
Require Import Coq.Logic.Decidable.
Require Import CoqFSetDecide.
Require Import CoqListFacts.
Require Import LibTactics.
We implement association lists as lists of key-value pairs. We
use eq as the equality on both keys and values. This is evident
primarily in the definitions of binds and maps.
(Implementation note: We can generalize the implementation to arbitrary equivalence relations. For now, we have chosen not to, in order to keep the implementation simple and to optimize for what we expect is the common case.)
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 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 (e.g., some concatenations 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.
A Strategy declaration can be used to prevent Coq's tactics from simplifying one, if one so desires.
(Implementation note: We can generalize the implementation to arbitrary equivalence relations. For now, we have chosen not to, in order to keep the implementation simple and to optimize for what we expect is the common case.)
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 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 (e.g., some concatenations 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.
A Strategy declaration can be used to prevent Coq's tactics from simplifying one, if one so desires.
Module Make
(X : UsualDecidableType)
(Import KeySet : FSetInterface.WSfun X).
Module Import D := CoqFSetDecide.WDecide_fun X KeySet.
Module KeySetProperties := FSetProperties.WProperties_fun X KeySet.
Module KeySetFacts := FSetFacts.WFacts_fun X KeySet.
Implicit arguments are enabled for the following definitions.
one constructs an association list consisting of exactly one
binding. We define an infix notation for it and ensure that the
arguments to app are interpreted in the right scope, i.e.,
list_scope.
Implementation note: The level associated with the notation gives it a higher precedence than the "++" notation for app. This should eliminate the need for parentheses. See the definition below of uniq, for example.
Implementation note: The level associated with the notation gives it a higher precedence than the "++" notation for app. This should eliminate the need for parentheses. See the definition below of uniq, for example.
Definition one (C : Type) (item : C) : list C := cons item nil.
Notation "x ~ a" := (one (x, a)) (at level 50) : list_scope.
Open Scope list_scope.
dom computes the domain of an association list, i.e., the
set consisting of its keys.
Fixpoint dom
(C : Type) (E : list (X.t*C))
: KeySet.t :=
match E with
| nil => empty
| (x, _) :: E' => add x (dom E')
end.
get looks up a key in an association list.
Fixpoint get
(C : Type) (x : X.t) (E : list (X.t*C))
: option C :=
match E with
| nil => None
| (y, c) :: F => if X.eq_dec x y then Some c else get x F
end.
binds is a ternary predicate that holds when a key-value pair
appears somewhere in the given association list.
maps is a ternary predicate that holds when the first binding in
the list for the given key is to the given value.
disjoint is a binary predicate that holds when the domains of
two association lists are disjoint.
Definition disjoint
(A B : Type) (E : list (X.t*A)) (F : list (X.t*B))
: Prop :=
inter (dom E) (dom F) [<=] empty.
map applies a function to each of the values in an association
list.
Definition map
(A B : Type) (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.
uniq is unary predicate that holds if and only if each key is
bound at most once in the given association list. Note that
uniq is defined in terms of one, not cons.
Inductive uniq (A : Type) : list (X.t*A) -> Prop :=
| uniq_nil :
uniq nil
| uniq_push : forall x a E,
uniq E ->
~ In x (dom E) ->
uniq (x ~ a ++ E).
Unless stated otherwise, in the remainder of this file, implicit
arguments will not be declared by default.
The following properties are used mainly for rewriting association
lists into the normal form described above. See the simpl_alist
and rewrite_alist tactics below.
Section ListProperties.
Variable X : Type.
Variables x y : X.
Variables l l1 l2 l3 : list X.
Lemma cons_app_one :
cons x l = one 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_nil_iff :
List.In x nil <-> False.
Lemma in_one_iff :
List.In x (one y) <-> x = y.
Lemma in_app_iff :
List.In x (l1 ++ l2) <-> List.In x l1 \/ List.In x l2.
End ListProperties.
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 key : Type.
Variable f : A -> B.
Variable x : X.t.
Variable b : A.
Variables E F G : list (X.t*A).
Lemma map_nil :
map f (@nil (X.t*A)) = nil.
Lemma map_one :
map f (x ~ b) = (x ~ f b).
Lemma map_cons :
map f ((x, b) :: E) = x ~ f b ++ map f E.
Lemma map_app :
map f (E ++ F) = map f E ++ map f F.
Lemma dom_nil :
dom (@nil (X.t*A)) = empty.
Lemma dom_one :
dom (x ~ b) [=] singleton x.
Lemma dom_cons :
dom ((x, b) :: E) [=] union (singleton x) (dom E).
Lemma dom_app :
dom (E ++ F) [=] union (dom E) (dom F).
Lemma dom_map :
dom (map f E) [=] dom E.
End Properties.
Rewriting hints.
Hint Rewrite cons_app_one cons_app_assoc : rewr_list.
Hint Rewrite app_assoc app_nil_1 app_nil_2 : rewr_list.
Hint Rewrite in_nil_iff in_one_iff in_app_iff : rewr_list_in.
Hint Rewrite map_nil map_one map_cons map_app : rewr_map.
Hint Rewrite dom_nil dom_one dom_cons 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_map rewr_dom.
Tactic Notation "simpl_alist" "in" hyp(H) :=
autorewrite with rewr_list rewr_map rewr_dom in H.
Tactic Notation "simpl_alist" "in" "*" :=
autorewrite with rewr_list 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.
Implementation note: The tactic depends on appropriate morphisms being declared for finite set operations.
Implementation note: The tactic depends on appropriate morphisms being declared for finite set operations.
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.
For convenience, we provide a tactic for reasoning by induction on
the structure of an association list. Compared to regular list
induction, in the "cons" case, this tactic automatically
destructs the pair at the head of the list and ensures that the
list is formed using one and app.
Lemma alist_ind : forall (A : Type) (P : list (X.t * A) -> Type),
(P nil) ->
(forall x a xs, P xs -> P (x ~ a ++ xs)) ->
(forall xs, P xs).
Tactic Notation "alist" "induction" ident(E) :=
try (intros until E);
let T := type of E in
let T := eval compute in T in
match T with
| list (?key * ?A) => induction E using (alist_ind A)
end.
Tactic Notation "alist" "induction" ident(E) "as" simple_intropattern(P) :=
try (intros until E);
let T := type of E in
let T := eval compute in T in
match T with
| list (?key * ?A) => induction E as P using (alist_ind A)
end.
Section Disjoint.
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_nil_1 :
forall A B (E : list (X.t*B)),
disjoint (@nil (X.t*A)) E.
Lemma disjoint_one_1 :
forall A B (x : X.t) (a : A) (F : list (X.t*B)),
disjoint (x ~ a) F ->
~ In x (dom F).
Lemma disjoint_one_2 :
forall A B (x : X.t) (a : A) (F : list (X.t*B)),
~ In x (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 <-> ~ In x (dom E).
Lemma disjoint_one_r :
forall A B (x : X.t) (a : A) (E : list (X.t*B)),
disjoint E (x ~ a) <-> ~ In x (dom E).
Lemma disjoint_cons_1 :
forall A B x a (E : list (X.t*A)) (F : list (X.t*B)),
disjoint ((x, a) :: E) F ->
~ In x (dom F).
Lemma disjoint_cons_2 :
forall A B x a (E : list (X.t*A)) (F : list (X.t*B)),
disjoint ((x, a) :: E) F ->
disjoint E F.
Lemma disjoint_cons_3 :
forall A B x a (E : list (X.t*A)) (F : list (X.t*B)),
disjoint E F ->
~ In x (dom F) ->
disjoint ((x, a) :: E) F.
Lemma disjoint_cons_l :
forall A B x a (E : list (X.t*A)) (F : list (X.t*B)),
disjoint ((x, a) :: E) F <-> ~ In x (dom F) /\ disjoint E F.
Lemma disjoint_cons_r :
forall A B x a (E : list (X.t*A)) (F : list (X.t*B)),
disjoint F ((x, a) :: E) <-> ~ In x (dom F) /\ disjoint E F.
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 Disjoint.
Section UniqProperties.
Variables A B : Type.
Variables f : A -> B.
Variables x : X.t.
Variables a b : A.
Variables E F G : list (X.t*A).
Lemma uniq_one_1 :
uniq (x ~ b).
Lemma uniq_cons_1 :
uniq ((x, a) :: E) ->
uniq E.
Lemma uniq_cons_2 :
uniq ((x, a) :: E) ->
~ In x (dom E).
Lemma uniq_cons_3 :
uniq E ->
~ In x (dom E) ->
uniq ((x, a) :: E).
Lemma uniq_cons_iff :
uniq ((x, a) :: E) <-> uniq E /\ ~ In x (dom E).
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_iff :
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_iff :
uniq (map f E) <-> uniq E.
End UniqProperties.
Section BindsProperties.
Variable 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_nil_iff :
binds x a nil <-> False.
Lemma binds_one_1 :
binds x a (y ~ b) ->
x = y.
Lemma binds_one_2 :
binds x a (y ~ b) ->
a = b.
Lemma binds_one_3 :
x = y ->
a = b ->
binds x a (y ~ b).
Lemma binds_one_iff :
binds x a (y ~ b) <-> x = y /\ a = b.
Lemma binds_cons_1 :
binds x a ((y, b) :: E) ->
(x = y /\ a = b) \/ binds x a E.
Lemma binds_cons_2 :
x = y ->
a = b ->
binds x a ((y, b) :: E).
Lemma binds_cons_3 :
binds x a E ->
binds x a ((y, b) :: E).
Lemma binds_cons_iff :
binds x a ((y, b) :: E) <-> (x = y /\ a = b) \/ binds x a E.
Lemma binds_app_1 :
binds x a (E ++ F) ->
binds x a E \/ binds x a F.
Lemma binds_app_2 :
binds x a E ->
binds x a (E ++ F).
Lemma binds_app_3 :
binds x a F ->
binds x a (E ++ F).
Lemma binds_app_iff :
binds x a (E ++ F) <-> binds x a E \/ binds x a F.
Lemma binds_map_1 :
(forall a b, f a = f b -> a = b) ->
binds x (f a) (map f E) ->
binds x a E.
Lemma binds_map_2 :
binds x a E ->
binds x (f a) (map f E).
Lemma binds_dom_contradiction : forall (E : list (X.t*A)),
binds x a E ->
~ In x (dom E) ->
False.
Lemma binds_app_uniq_1 :
uniq (E ++ F) ->
binds x a (E ++ F) ->
(binds x a E /\ ~ In x (dom F)) \/ (binds x a F /\ ~ In x (dom E)).
Lemma binds_app_uniq_iff :
uniq (E ++ F) ->
(binds x a (E ++ F) <->
(binds x a E /\ ~ In x (dom F)) \/
(binds x a F /\ ~ In x (dom E))).
End BindsProperties.
Section BindsProperties2.
Variable 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_cons_uniq_1 :
uniq ((y, b) :: E) ->
binds x a ((y, b) :: E) ->
(x = y /\ a = b /\ ~ In x (dom E)) \/ (binds x a E /\ x <> y).
Lemma binds_cons_uniq_iff :
uniq ((y, b) :: E) ->
(binds x a ((y, b) :: E) <->
(x = y /\ a = b /\ ~ In x (dom E)) \/
(binds x a E /\ x <> y)).
End BindsProperties2.
Hint Resolve
@app_assoc @app_nil_2 @map_app @dom_one @dom_cons @dom_app @dom_map.
Hint Resolve
@disjoint_sym_1 @disjoint_nil_1 @disjoint_one_2 @disjoint_cons_3
@disjoint_app_3 @disjoint_map_2 @uniq_nil @uniq_push @uniq_one_1
@uniq_cons_3 @uniq_app_4 @uniq_map_2.
Hint Resolve
@binds_one_3 @binds_cons_2 @binds_cons_3 @binds_app_2 @binds_app_3
@binds_map_2.
The following properties are an assortment of structural
properties about association lists.
Section AssortedListProperties.
Variable X : Type.
Variables x : X.
Variables xs ys zs : list X.
Lemma one_eq_app :
one x ++ xs = ys ++ zs ->
(exists qs, ys = x :: qs /\ xs = qs ++ zs) \/
(ys = nil /\ zs = x :: xs).
Lemma app_eq_one :
ys ++ zs = one x ++ xs ->
(exists qs, ys = x :: qs /\ xs = qs ++ zs) \/
(ys = nil /\ zs = x :: xs).
Lemma nil_neq_one_mid :
nil <> xs ++ one x ++ ys.
Lemma one_mid_neq_nil :
xs ++ one x ++ ys <> nil.
End AssortedListProperties.
destruct_uniq decomposes all uniq and disjoint hypotheses.
Ltac destruct_uniq :=
match goal with
| H : uniq nil |- _ =>
clear H;
destruct_uniq
| H : uniq (?x ~ ?a) |- _ =>
clear H;
destruct_uniq
| H : uniq ((?x, ?a) :: ?E) |- _ =>
let J := fresh "UniqTac" in
pose proof H as J;
apply uniq_cons_1 in H;
apply uniq_cons_2 in J;
autorewrite with rewr_dom in J;
destruct_uniq
| H : uniq (?E ++ ?F) |- _ =>
let J1 := fresh "UniqTac" in
let J2 := fresh "UniqTac" in
pose proof H as J1;
pose proof H as J2;
apply uniq_app_1 in H;
apply uniq_app_2 in J1;
apply uniq_app_3 in J2;
destruct_uniq
| H : uniq (map ?f ?E) |- _ =>
apply uniq_map_1 in H;
destruct_uniq
| H : disjoint nil ?E |- _ =>
clear H;
destruct_uniq
| H : disjoint (?x ~ ?a) ?F |- _ =>
apply disjoint_one_1 in H;
autorewrite with rewr_dom in H;
destruct_uniq
| H : disjoint ((?x, ?a) :: ?E) ?F |- _ =>
let J := fresh "UniqTac" in
pose proof H as J;
apply disjoint_cons_1 in H;
apply disjoint_cons_2 in J;
autorewrite with rewr_dom in H;
destruct_uniq
| H : disjoint (?E ++ ?F) ?G |- _ =>
let J := fresh "UniqTac" in
pose proof H as J;
apply disjoint_app_1 in H;
apply disjoint_app_2 in J;
destruct_uniq
| H : disjoint (map ?f ?E) ?F |- _ =>
apply disjoint_map_1 in H;
destruct_uniq
| H : disjoint ?E nil |- _ =>
clear H;
destruct_uniq
| H : disjoint ?F (?x ~ ?a) |- _ =>
apply disjoint_sym_1 in H;
destruct_uniq
| H : disjoint ?F ((?x, ?a) :: ?E) |- _ =>
apply disjoint_sym_1 in H;
destruct_uniq
| H : disjoint ?G (?E ++ ?F) |- _ =>
apply disjoint_sym_1 in H;
destruct_uniq
| H : disjoint ?F (map ?f ?E) |- _ =>
apply disjoint_sym_1 in H;
destruct_uniq
| _ =>
idtac
end.
solve_uniq attempts to solve goals by first decomposing
hypotheses about disjoint and uniq and then trying some
simple, if perhaps slow, heuristics.
Ltac solve_uniq :=
intros;
destruct_uniq;
repeat first [ apply uniq_push
| apply uniq_cons_3
| apply uniq_app_4
| apply uniq_one_1
| apply uniq_nil ];
auto;
try tauto;
unfold disjoint in *;
try fsetdec;
fail "Not solvable by [solve_uniq]; try [destruct_uniq]".
Section UniqDerived.
Variable A : Type.
Variables x y : X.t.
Variables a b : A.
Variables E F G : list (X.t*A).
Lemma uniq_insert_mid :
uniq (G ++ E) ->
~ In x (dom G) ->
~ In x (dom E) ->
uniq (G ++ (x ~ a) ++ E).
Lemma uniq_remove_mid :
uniq (E ++ F ++ G) ->
uniq (E ++ G).
Lemma uniq_reorder_1 :
uniq (E ++ F) ->
uniq (F ++ E).
Lemma uniq_reorder_2 :
uniq (E ++ F ++ G) ->
uniq (F ++ 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) ->
~ In x (dom E).
Lemma fresh_mid_head :
uniq (F ++ (x ~ a) ++ E) ->
~ In x (dom F).
End UniqDerived.
destruct_binds_hyp and destruct_binds_hyp_uniq tactics
decompose a hypotheses of the form binds x a E, with the latter
tactic assuming that uniq E holds. The tactic solve_uniq is
used for discharging any uniq obligations that arise.
Implementation note (BEA, XXX): No support for map. I'm not sure what to do about the "injectivity" side condition on binds_map_inv. Perhaps just generate the extra subgoal, on the assumption that the condition is usually provable? It's not as if I want to implement even more tactics here...
Implementation note (BEA, XXX): No support for map. I'm not sure what to do about the "injectivity" side condition on binds_map_inv. Perhaps just generate the extra subgoal, on the assumption that the condition is usually provable? It's not as if I want to implement even more tactics here...
Ltac destruct_binds_hyp H :=
match type of H with
| binds ?x ?a nil =>
inversion H
| binds ?x ?a (?y ~ ?b) =>
let J1 := fresh "BindsTacKey" in
let J2 := fresh "BindsTacVal" in
rename H into J1;
pose proof J1 as J2;
apply binds_one_1 in J1;
apply binds_one_2 in J2;
try (subst x);
try (subst a);
try (subst y);
try (subst b)
| binds ?x ?a ((?y, ?b) :: ?E) =>
change (binds x a (y ~ b ++ E)) in H;
destruct_binds_hyp H
| binds ?x ?a (?E ++ ?F) =>
let J := fresh "BindsTac" in
apply binds_app_1 in H;
destruct H as [J | J];
destruct_binds_hyp J
| _ =>
idtac
end.
Ltac destruct_binds_hyp_uniq H :=
match type of H with
| binds ?x ?a nil =>
inversion H
| binds ?x ?a (?y ~ ?b) =>
let J1 := fresh "BindsTacKey" in
let J2 := fresh "BindsTacVal" in
rename H into J1;
pose proof J1 as J2;
apply binds_one_1 in J1;
apply binds_one_2 in J2;
try (subst x);
try (subst a);
try (subst y);
try (subst b)
| binds ?x ?a ((?y, ?b) :: ?E) =>
change (binds x a (y ~ b ++ E)) in H;
destruct_binds_hyp_uniq H
| binds ?x ?a (?E ++ ?F) =>
let J1 := fresh "BindsTacSideCond" in
assert (J1 : uniq (E ++ F));
[ destruct_uniq; auto
| match type of J1 with
| @uniq ?A _ =>
let J2 := fresh "BindsTac" in
destruct (@binds_app_uniq_1 A x a E F J1 H)
as [[J2 ?] | [J2 ?]];
clear H;
destruct_binds_hyp_uniq J2
end
]
| _ =>
idtac
end.
An auxiliary tactic. Not intended for use on its own.
Ltac analyze_binds_cleanup :=
auto;
try tauto;
try discriminate;
try match goal with
| J : ~ In ?x ?E |- _ =>
match E with
| context [x] => elim J; clear; simpl_alist; auto with set
end
end.
The analyze_binds and analyze_binds_uniq tactics decompose a
hypothesis of the form binds x a E, with the latter assuming
that uniq E holds, and then try some simple heuristics for
solving the resulting goals.
Ltac analyze_binds H :=
destruct_binds_hyp H;
analyze_binds_cleanup.
Ltac analyze_binds_uniq H :=
destruct_binds_hyp_uniq H;
analyze_binds_cleanup.
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 :
{a : A | binds x a E} + (forall a, ~ binds x a E).
Lemma binds_lookup_dec :
decidable (exists a, 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 ->
In x (dom E).
Lemma binds_In_inv : forall x (E : list (X.t*A)),
In x (dom E) ->
exists a, binds x a 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 ->
~ In x (dom F).
Lemma fresh_app_r :
uniq (F ++ E) ->
binds x a F ->
~ In x (dom E).
End BindsDerived.
Hint Resolve @nil_neq_one_mid @one_mid_neq_nil.
Hint Resolve @uniq_insert_mid @uniq_map_app_l.
Hint Immediate @uniq_remove_mid.
Hint Resolve @binds_weaken.
Hint Immediate @binds_remove_mid @binds_In.
End Make.
This page has been generated by coqdoc