Coral.Metalib.AssocList
(* This file is distributed under the terms of the MIT License, also
known as the X11 Licence. A copy of this license is in the README
file that accompanied the original distribution of this file.
Based on code written by:
Brian Aydemir
Aaron Bohannon
Arthur Charg\'eraud
With contributions from:
Edsko de Vries:
uniq_reorder_1, uniq_reorder_2, binds_In_inv *)
known as the X11 Licence. A copy of this license is in the README
file that accompanied the original distribution of this file.
Based on code written by:
Brian Aydemir
Aaron Bohannon
Arthur Charg\'eraud
With contributions from:
Edsko de Vries:
uniq_reorder_1, uniq_reorder_2, binds_In_inv *)
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 Coq.Strings.String.
Require Import Metalib.CoqFSetDecide.
Require Import Metalib.CoqListFacts.
Require Import Metalib.LibTactics.
Require Import Metalib.CoqFSetInterface.
(* *********************************************************************** *)
Implementation
(* Implementation note (BEA, XXX): Very little support for
- Inversion on association lists when one is opaque.
- No real support for get.
- No real support for maps.
- No support for permutations. *)
Require Import Coq.Classes.Equivalence.
Require Import Coq.Classes.EquivDec.
Require Import Metalib.CoqEqDec.
Module Make
(X : UsualDecidableType)
(KeySet : FSetInterface.WSfun X).
(* SCW: Make an instance of EqDef_eq for X so that we can use the "==" in get below. *)
Instance EqDec_of_X : @EqDec X.t eq eq_equivalence.
Proof. exact X.eq_dec. Defined.
Instance EqDec_eq_of_X: @EqDec_eq X.t.
Proof. exact (EqDec_eq_of_EqDec X.t EqDec_of_X). Defined.
Open Scope coqeqdec_scope.
Import KeySet.
Module Import D := CoqFSetDecide.WDecide_fun X KeySet.
Module KeySetProperties := FSetProperties.WProperties_fun X KeySet.
Module KeySetFacts := FSetFacts.WFacts_fun X KeySet.
(* *********************************************************************** *)
Set Implicit Arguments.
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.
Definition one (C : Type) (item : C) : list C := cons item nil.
Notation "x ~ a" := (one (x, a)) (at level 50) : list_scope.
Arguments app _%type_scope _%list_scope _%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 == 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 : ∀ 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.
Unset Implicit Arguments.
(* *********************************************************************** *)
List properties
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.
Proof. clear. reflexivity. Qed.
Lemma cons_app_assoc :
(cons x l1) ++ l2 = cons x (l1 ++ l2).
Proof. clear. reflexivity. Qed.
Lemma app_assoc :
(l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
Proof. clear. auto with datatypes. Qed.
Lemma app_nil_1 :
nil ++ l = l.
Proof. clear. reflexivity. Qed.
Lemma app_nil_2 :
l ++ nil = l.
Proof. clear. auto with datatypes. Qed.
Lemma in_nil_iff :
List.In x nil ↔ False.
Proof. clear. split; inversion 1. Qed.
Lemma in_one_iff :
List.In x (one y) ↔ x = y.
Proof.
clear. split.
inversion 1 as [ | HIn]; intuition.
constructor; intuition.
Qed.
Lemma in_app_iff :
List.In x (l1 ++ l2) ↔ List.In x l1 ∨ List.In x l2.
Proof. clear. split; auto using List.in_or_app, List.in_app_or. Qed.
End ListProperties.
(* *********************************************************************** *)
Properties of map and dom
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.
Proof. clear. reflexivity. Qed.
Lemma map_one :
map f (x ~ b) = (x ~ f b).
Proof. clear. reflexivity. Qed.
Lemma map_cons :
map f ((x, b) :: E) = x ~ f b ++ map f E.
Proof. clear. reflexivity. Qed.
Lemma map_app :
map f (E ++ F) = map f E ++ map f F.
Proof. clear. unfold map. rewrite List.map_app. reflexivity. Qed.
Lemma dom_nil :
dom (@nil (X.t×A)) = empty.
Proof. clear. reflexivity. Qed.
Lemma dom_one :
dom (x ~ b) [=] singleton x.
Proof. clear. intros. simpl. fsetdec. Qed.
Lemma dom_cons :
dom ((x, b) :: E) [=] union (singleton x) (dom E).
Proof. clear. intros. simpl. fsetdec. Qed.
Lemma dom_app :
dom (E ++ F) [=] union (dom E) (dom F).
Proof. clear. intros. induction E as [ | [? ?] ]; simpl; fsetdec. Qed.
Lemma dom_map :
dom (map f E) [=] dom E.
Proof. clear. intros. induction E as [ | [? ?] ]; simpl; fsetdec. Qed.
End Properties.
(* *********************************************************************** *)
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 rewrite_alist tactic
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.
(* *********************************************************************** *)
Induction
Lemma alist_ind : ∀ (A : Type) (P : list (X.t × A) → Type),
(P nil) →
(∀ x a xs, P xs → P (x ~ a ++ xs)) →
(∀ xs, P xs).
Proof.
induction xs as [ | [x a] xs ].
auto.
change (P (x ~ a ++ xs)). auto.
Defined.
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.
(* *********************************************************************** *)
Basic facts about disjoint
Section Disjoint.
Implicit Types A B C : Type.
Lemma disjoint_sym_1 :
∀ A B (E : list (X.t×A)) (F : list (X.t×B)),
disjoint E F →
disjoint F E.
Proof. unfold disjoint. fsetdec. Qed.
Lemma disjoint_sym :
∀ A B (E : list (X.t×A)) (F : list (X.t×B)),
disjoint E F ↔ disjoint F E.
Proof. intuition auto using disjoint_sym_1. Qed.
Lemma disjoint_nil_1 :
∀ A B (E : list (X.t×B)),
disjoint (@nil (X.t×A)) E.
Proof. unfold disjoint. fsetdec. Qed.
Lemma disjoint_one_1 :
∀ A B (x : X.t) (a : A) (F : list (X.t×B)),
disjoint (x ~ a) F →
~ In x (dom F).
Proof. unfold disjoint. simpl. fsetdec. Qed.
Lemma disjoint_one_2 :
∀ A B (x : X.t) (a : A) (F : list (X.t×B)),
~ In x (dom F) →
disjoint (x ~ a) F.
Proof. unfold disjoint. simpl. fsetdec. Qed.
Lemma disjoint_one_l :
∀ A B (x : X.t) (a : A) (E : list (X.t×B)),
disjoint (x ~ a) E ↔ ~ In x (dom E).
Proof. unfold disjoint. simpl. split; fsetdec. Qed.
Lemma disjoint_one_r :
∀ A B (x : X.t) (a : A) (E : list (X.t×B)),
disjoint E (x ~ a) ↔ ~ In x (dom E).
Proof. intros. rewrite disjoint_sym. apply disjoint_one_l. Qed.
Lemma disjoint_cons_1 :
∀ A B x a (E : list (X.t×A)) (F : list (X.t×B)),
disjoint ((x, a) :: E) F →
~ In x (dom F).
Proof. unfold disjoint. simpl. fsetdec. Qed.
Lemma disjoint_cons_2 :
∀ A B x a (E : list (X.t×A)) (F : list (X.t×B)),
disjoint ((x, a) :: E) F →
disjoint E F.
Proof. unfold disjoint. simpl. fsetdec. Qed.
Lemma disjoint_cons_3 :
∀ 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.
Proof. unfold disjoint. simpl. fsetdec. Qed.
Lemma disjoint_cons_l :
∀ 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.
Proof.
split.
eauto using disjoint_cons_1, disjoint_cons_2.
intros [? ?]. auto using disjoint_cons_3.
Qed.
Lemma disjoint_cons_r :
∀ 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.
Proof. intros. rewrite disjoint_sym. apply disjoint_cons_l. Qed.
Lemma disjoint_app_1 :
∀ A B (E F : list (X.t×A)) (G : list (X.t×B)),
disjoint (E ++ F) G →
disjoint E G.
Proof. unfold disjoint. intros. rewrite dom_app in ×. fsetdec. Qed.
Lemma disjoint_app_2 :
∀ A B (E F : list (X.t×A)) (G : list (X.t×B)),
disjoint (E ++ F) G →
disjoint F G.
Proof. unfold disjoint. intros. rewrite dom_app in ×. fsetdec. Qed.
Lemma disjoint_app_3 :
∀ A B (E F : list (X.t×A)) (G : list (X.t×B)),
disjoint E G →
disjoint F G →
disjoint (E ++ F) G.
Proof. unfold disjoint. intros. rewrite dom_app in ×. fsetdec. Qed.
Lemma disjoint_app_l :
∀ A B (E F : list (X.t×A)) (G : list (X.t×B)),
disjoint (E ++ F) G ↔ disjoint E G ∧ disjoint F G.
Proof.
intuition eauto 2 using
disjoint_app_1, disjoint_app_2, disjoint_app_3.
Qed.
Lemma disjoint_app_r :
∀ A B (E F : list (X.t×A)) (G : list (X.t×B)),
disjoint G (E ++ F) ↔ disjoint E G ∧ disjoint F G.
Proof. intros. rewrite disjoint_sym. apply disjoint_app_l. Qed.
Lemma disjoint_map_1 :
∀ A B C (E : list (X.t×A)) (F : list (X.t×B)) (f:A→C),
disjoint (map f E) F →
disjoint E F.
Proof. unfold disjoint. intros. rewrite dom_map in ×. fsetdec. Qed.
Lemma disjoint_map_2 :
∀ A B C (E : list (X.t×A)) (F : list (X.t×B)) (f:A→C),
disjoint E F →
disjoint (map f E) F.
Proof. unfold disjoint. intros. rewrite dom_map in ×. fsetdec. Qed.
Lemma disjoint_map_l :
∀ A B C (E : list (X.t×A)) (F : list (X.t×B)) (f:A→C),
disjoint (map f E) F ↔ disjoint E F.
Proof. intuition eauto using disjoint_map_1, disjoint_map_2. Qed.
Lemma disjoint_map_r :
∀ A B C (E : list (X.t×A)) (F : list (X.t×B)) (f:A→C),
disjoint F (map f E) ↔ disjoint E F.
Proof. intros. rewrite disjoint_sym. apply disjoint_map_l. Qed.
End Disjoint.
(* *********************************************************************** *)
Basic facts about uniq
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).
Proof.
clear. rewrite_alist ((x ~ b) ++ nil).
apply uniq_push. apply uniq_nil. apply empty_1.
Qed.
Lemma uniq_cons_1 :
uniq ((x, a) :: E) →
uniq E.
Proof. clear. inversion 1. trivial. Qed.
Lemma uniq_cons_2 :
uniq ((x, a) :: E) →
~ In x (dom E).
Proof. clear. inversion 1. trivial. Qed.
Lemma uniq_cons_3 :
uniq E →
~ In x (dom E) →
uniq ((x, a) :: E).
Proof.
clear. intros. change (uniq (x ~ a ++ E)). apply uniq_push; trivial.
Qed.
Lemma uniq_cons_iff :
uniq ((x, a) :: E) ↔ uniq E ∧ ~ In x (dom E).
Proof.
clear. split.
eauto using uniq_cons_1, uniq_cons_2.
intros [? ?]. auto using uniq_cons_3.
Qed.
Lemma uniq_app_1 :
uniq (E ++ F) → uniq E.
Proof.
clear. intros J. alist induction E.
apply uniq_nil.
inversion J; subst. rewrite dom_app in ×. apply uniq_push.
auto.
fsetdec.
Qed.
Lemma uniq_app_2 :
uniq (E ++ F) → uniq F.
Proof.
clear. intros J. alist induction E.
auto.
inversion J; subst. auto.
Qed.
Lemma uniq_app_3 :
uniq (E ++ F) → disjoint E F.
Proof.
clear. intros J. unfold disjoint. alist induction E as [ | ? ? ? IH ].
fsetdec.
inversion J; subst. simpl_alist in ×. lapply IH.
fsetdec.
auto.
Qed.
Lemma uniq_app_4 :
uniq E →
uniq F →
disjoint E F →
uniq (E ++ F).
Proof.
clear. intros HE HF Hd. alist induction E as [ | x1 a1 E' ].
auto.
inversion HE; subst. rewrite app_assoc. apply uniq_push.
rewrite disjoint_app_l, disjoint_one_l in ×. intuition.
rewrite disjoint_app_l, disjoint_one_l, dom_app in ×. fsetdec.
Qed.
Lemma uniq_app_iff :
uniq (E ++ F) ↔ uniq E ∧ uniq F ∧ disjoint E F.
Proof.
clear; intuition auto using
uniq_app_1, uniq_app_2, uniq_app_3, uniq_app_4.
Qed.
Lemma uniq_map_1 :
uniq (map f E) →
uniq E.
Proof.
clear. intros J. alist induction E as [ | x1 a1 E' ].
apply uniq_nil.
inversion J; subst. rewrite dom_map in ×. apply uniq_push; auto.
Qed.
Lemma uniq_map_2 :
uniq E →
uniq (map f E).
Proof.
clear. intros J. alist induction E as [ | x1 a1 E' ].
apply uniq_nil.
inversion J; subst. simpl_alist. apply uniq_push.
auto.
rewrite dom_map. trivial.
Qed.
Lemma uniq_map_iff :
uniq (map f E) ↔ uniq E.
Proof. clear. intuition auto using uniq_map_1, uniq_map_2. Qed.
End UniqProperties.
(* *********************************************************************** *)
Basic facts about binds
Section BindsProperties.
Variable A B : Type.
Variables f : A → B.
Variables x y : X.t.
Variables a b : A.
Variables b0 : B.
Variables E F G : list (X.t×A).
Lemma binds_nil_iff :
binds x a nil ↔ False.
Proof. clear. split. inversion 1. intuition. Qed.
Lemma binds_one_1 :
binds x a (y ~ b) →
x = y.
Proof.
clear. intros H. inversion H as [HEq | HIn].
inversion HEq; intuition.
inversion HIn.
Qed.
Lemma binds_one_2 :
binds x a (y ~ b) →
a = b.
Proof.
clear. intros H. inversion H as [HEq | HIn].
inversion HEq; intuition.
inversion HIn.
Qed.
Lemma binds_one_3 :
x = y →
a = b →
binds x a (y ~ b).
Proof. clear. unfold binds. intros. simpl. left. congruence. Qed.
Lemma binds_one_iff :
binds x a (y ~ b) ↔ x = y ∧ a = b.
Proof.
clear. intuition auto using binds_one_1, binds_one_2, binds_one_3.
Qed.
Lemma binds_cons_1 :
binds x a ((y, b) :: E) →
(x = y ∧ a = b) ∨ binds x a E.
Proof. clear. inversion 1 as [J | J]; try injection J; auto. Qed.
Lemma binds_cons_2 :
x = y →
a = b →
binds x a ((y, b) :: E).
Proof. clear. unfold binds. simpl. left. f_equal; auto. Qed.
Lemma binds_cons_3 :
binds x a E →
binds x a ((y, b) :: E).
Proof. clear. unfold binds. simpl. right. trivial. Qed.
Lemma binds_cons_iff :
binds x a ((y, b) :: E) ↔ (x = y ∧ a = b) ∨ binds x a E.
Proof.
clear. intuition auto using binds_cons_1, binds_cons_2, binds_cons_3.
Qed.
Lemma binds_app_1 :
binds x a (E ++ F) →
binds x a E ∨ binds x a F.
Proof. clear. unfold binds. rewrite in_app_iff. auto. Qed.
Lemma binds_app_2 :
binds x a E →
binds x a (E ++ F).
Proof. clear. unfold binds. rewrite in_app_iff. auto. Qed.
Lemma binds_app_3 :
binds x a F →
binds x a (E ++ F).
Proof. clear. unfold binds. rewrite in_app_iff. auto. Qed.
Lemma binds_app_iff :
binds x a (E ++ F) ↔ binds x a E ∨ binds x a F.
Proof. clear. unfold binds. rewrite in_app_iff. split; auto. Qed.
Lemma binds_map_1 :
(∀ a b, f a = f b → a = b) →
binds x (f a) (map f E) →
binds x a E.
Proof.
clear. alist induction E; intros ?.
inversion 1.
unfold binds in ×. simpl. intros [K | K].
left. injection K. intros. f_equal; auto.
right. auto.
Qed.
Lemma binds_map_2 :
binds x a E →
binds x (f a) (map f E).
Proof.
clear. alist induction E.
inversion 1.
unfold binds in ×. simpl. intros [? | ?].
left. congruence.
right. auto.
Qed.
Lemma binds_map_3 :
binds x b0 (map f E) →
∃ a, f a = b0 ∧ binds x a E.
Proof.
alist induction E.
- inversion 1.
- unfold binds in ×. simpl. intros [? | ?].
inversion H; subst.
∃ a0. auto.
destruct IHl as [a1 [EQ B0]]; auto.
∃ a1. auto.
Qed.
Lemma binds_dom_contradiction : ∀ (E : list (X.t×A)),
binds x a E →
~ In x (dom E) →
False.
Proof.
clear. intros E H1 H2.
alist induction E as [ | ? ? ? IH ].
inversion H1.
unfold binds in ×. simpl in ×. destruct H1 as [J | J].
injection J. fsetdec.
eapply IH. auto. fsetdec.
Qed.
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)).
Proof.
clear. intros J1 J2.
rewrite uniq_app_iff in J1. unfold disjoint in J1.
rewrite binds_app_iff in J2.
assert (~ In x (dom F) ∨ ~ In x (dom E)) by fsetdec.
intuition eauto using binds_dom_contradiction.
Qed.
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))).
Proof.
clear. intuition auto using binds_app_uniq_1, binds_app_2, binds_app_3.
Qed.
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).
Proof.
clear. intros J1 J2.
change ((y, b) :: E) with (y ~ b ++ E) in J1.
change ((y, b) :: E) with (y ~ b ++ E) in J2.
eapply binds_app_uniq_1 in J1; [ | eassumption ].
destruct J1 as [[J3 ?] | [? ?]].
unfold binds in J3. simpl in J3. destruct J3 as [J4 | ].
injection J4. intros. subst. auto.
intuition.
simpl in ×. right. split; [ trivial | fsetdec ].
Qed.
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)).
Proof.
clear. intuition auto using binds_cons_uniq_1, binds_cons_2, binds_cons_3.
Qed.
End BindsProperties2.
(* *********************************************************************** *)
Hint Resolve
@app_assoc @app_nil_2 @map_app @dom_one @dom_cons @dom_app @dom_map : core.
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 : core.
Hint Resolve
@binds_one_3 @binds_cons_2 @binds_cons_3 @binds_app_2 @binds_app_3
@binds_map_2 : core.
(* *********************************************************************** *)
List properties
Section AssortedListProperties.
Variable X : Type.
Variables x : X.
Variables xs ys zs : list X.
Lemma one_eq_app :
one x ++ xs = ys ++ zs →
(∃ qs, ys = x :: qs ∧ xs = qs ++ zs) ∨
(ys = nil ∧ zs = x :: xs).
Proof. clear. auto using CoqListFacts.cons_eq_app. Qed.
Lemma app_eq_one :
ys ++ zs = one x ++ xs →
(∃ qs, ys = x :: qs ∧ xs = qs ++ zs) ∨
(ys = nil ∧ zs = x :: xs).
Proof. clear. auto using CoqListFacts.app_eq_cons. Qed.
Lemma nil_neq_one_mid :
nil ≠ xs ++ one x ++ ys.
Proof. clear. induction xs; simpl_alist; intros J; inversion J. Qed.
Lemma one_mid_neq_nil :
xs ++ one x ++ ys ≠ nil.
Proof. clear. intros H. symmetry in H. auto using nil_neq_one_mid. Qed.
End AssortedListProperties.
(* *********************************************************************** *)
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]".
(* *********************************************************************** *)
Facts about 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).
Proof. clear. solve_uniq. Qed.
Lemma uniq_remove_mid :
uniq (E ++ F ++ G) →
uniq (E ++ G).
Proof. clear. solve_uniq. Qed.
Lemma uniq_reorder_1 :
uniq (E ++ F) →
uniq (F ++ E).
Proof. clear. solve_uniq. Qed.
Lemma uniq_reorder_2 :
uniq (E ++ F ++ G) →
uniq (F ++ E ++ G).
Proof. clear. solve_uniq. Qed.
Lemma uniq_map_app_l : ∀ (f : A → A),
uniq (F ++ E) →
uniq (map f F ++ E).
Proof. clear. solve_uniq. Qed.
Lemma fresh_mid_tail :
uniq (F ++ (x ~ a) ++ E) →
~ In x (dom E).
Proof. clear. solve_uniq. Qed.
Lemma fresh_mid_head :
uniq (F ++ (x ~ a) ++ E) →
~ In x (dom F).
Proof. clear. solve_uniq. Qed.
End UniqDerived.
(* *********************************************************************** *)
Tactic support for binds
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.
(* *********************************************************************** *)
Facts about binds
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 :
(∀ a b : A, {a = b} + {a ≠ b}) →
{binds x a E} + {~ binds x a E}.
Proof.
clear. intros. unfold binds. apply List.In_dec.
decide equality.
apply X.eq_dec.
Defined.
Lemma binds_lookup :
{a : A | binds x a E} + (∀ a, ~ binds x a E).
Proof with intuition eauto.
clear. intros. alist induction E as [ | x1 a1 ? [[a' J] | J] ]...
destruct (X.eq_dec x x1)...
right. unfold binds. intros a' [K | ?]...
unfold X.eq in ×. injection K...
Defined.
Lemma binds_lookup_dec :
decidable (∃ a, binds x a E).
Proof with intuition eauto.
clear. intros. unfold decidable.
destruct binds_lookup as [[? ?] | ?]...
right. intros [? ?]...
Defined.
Lemma binds_weaken :
binds x a (E ++ G) →
binds x a (E ++ F ++ G).
Proof. clear. intros H. analyze_binds H. Qed.
Lemma binds_mid_eq :
binds x a (F ++ (x ~ b) ++ E) →
uniq (F ++ (x ~ b) ++ E) →
a = b.
Proof. clear. intros J ?. analyze_binds_uniq J. Qed.
Lemma binds_remove_mid :
binds x a (F ++ (y ~ b) ++ G) →
x ≠ y →
binds x a (F ++ G).
Proof. clear. intros H. analyze_binds H. Qed.
Lemma binds_In : ∀ x a (E : list (X.t×A)),
binds x a E →
In x (dom E).
Proof.
clear. alist induction E as [ | y ? F ]; intros J; simpl_alist.
analyze_binds J.
analyze_binds J; subst; auto with set.
Qed.
Lemma binds_In_inv : ∀ x (E : list (X.t×A)),
In x (dom E) →
∃ a, binds x a E.
Proof.
clear. alist induction E as [ | y b F IH ]; intros J.
simpl_alist in J. fsetdec.
simpl_alist in J. apply union_1 in J. destruct J as [J | J].
∃ b. apply singleton_1 in J. auto.
apply IH in J. destruct J. eauto.
Qed.
Lemma binds_unique :
binds x a E →
binds x b E →
uniq E →
a = b.
Proof.
clear. alist induction E as [ | ? ? F IH ].
inversion 1.
unfold binds. simpl. intros [J1 | J1] [J2 | J2] J3.
Case "left / left".
congruence.
Case "left / right".
assert (In x (dom F)). eapply binds_In. apply J2.
injection J1; intros; subst.
solve_uniq.
Case "right / left".
assert (In x (dom F)). eapply binds_In. apply J1.
injection J2; intros; subst.
solve_uniq.
Case "right / right".
unfold binds in ×.
eapply IH; trivial.
solve_uniq.
Qed.
Lemma fresh_app_l :
uniq (F ++ E) →
binds x a E →
~ In x (dom F).
Proof.
clear. intros.
assert (In x (dom E)) by eauto using binds_In.
solve_uniq.
Qed.
Lemma fresh_app_r :
uniq (F ++ E) →
binds x a F →
~ In x (dom E).
Proof.
clear. intros.
assert (In x (dom F)) by eauto using binds_In.
solve_uniq.
Qed.
End BindsDerived.
(* *********************************************************************** *)
Hint Resolve @nil_neq_one_mid @one_mid_neq_nil : core.
Hint Resolve @uniq_insert_mid @uniq_map_app_l : core.
Hint Immediate @uniq_remove_mid : core.
Hint Resolve @binds_weaken : core.
Hint Immediate @binds_remove_mid @binds_In : core.
End Make.