Set Implicit Arguments.
Require Import Lib_Tactic List Decidable Metatheory_Var Metatheory_Fresh.
Module Env.
Section Definitions.
Variable A : Set.
Implicit Types x : var.
Implicit Types a : A.
Definition env := list (var * A).
Definition empty : env := nil.
Definition single x a := (x,a) :: nil.
Definition concat (E F : env) := F ++ E.
Fixpoint dom (E : env) : vars :=
match E with
| nil => {}
| (x, _) :: E' => {{x}} \u (dom E')
end.
Fixpoint map (f : A -> A) (E : env) {struct E} : env :=
match E with
| nil => nil
| (x, V) :: E' => (x, f V) :: map f E'
end.
Fixpoint get (x : var) (E : env) {struct E} : option A :=
match E with
| nil => None
| (y,a) :: E' => if eq_var_dec x y then Some a else get x E'
end.
End Definitions.
Implicit Arguments empty [A].
Notation "x ~ a" := (single x a)
(at level 31, left associativity) : env_scope.
Notation "E & F" := (concat E F)
(at level 40, left associativity) : env_scope.
Notation "x '#' E" := (x \notin (dom E)) (at level 60) : env_scope.
Bind Scope env_scope with env.
Open Local Scope env_scope.
Section Relations.
Variable A : Set.
Inductive ok : env A -> Prop :=
| ok_empty :
ok empty
| ok_push : forall E x a,
ok E -> x # E -> ok (E & x ~ a).
Definition binds x a (E : env A) :=
get x E = Some a.
Definition env_prop (P : A -> Prop) (E : env A) :=
forall x a, binds x a E -> P a.
Definition extends (E E' : env A) :=
forall x a, binds x a E -> binds x a E'.
End Relations.
Hint Constructors ok.
Open Local Scope env_scope.
Section OpProperties.
Variable A : Set.
Implicit Types E F : env A.
Implicit Types a b : A.
Lemma concat_empty : forall E,
E & empty = E.
Proof.
auto.
Qed.
Lemma concat_assoc : forall E F G,
(E & F) & G = E & (F & G).
Proof.
induction G; simpl; congruence.
Qed.
Lemma map_concat : forall f E F,
map f (E & F) = (map f E) & (map f F).
Proof.
induction F as [|(x,a)]; simpl; congruence.
Qed.
Lemma concat_assoc_map_push : forall f E F y V,
(E & map f F) & y ~ (f V) = E & (map f (F & y ~ V)).
Proof.
auto.
Qed.
Lemma eq_empty_inv : forall x a E F,
empty = E & x ~ a & F -> False.
Proof.
induction F as [|(y,b)]; simpl; discriminate.
Qed.
Lemma eq_push_inv : forall E x a E' x' a',
E & x ~ a = E' & x' ~ a' -> E = E' /\ x = x' /\ a = a'.
Proof.
simpl. intros. inversions* H.
Qed.
Lemma dom_empty :
dom (A:=A) empty = {}.
Proof.
auto.
Qed.
Lemma dom_single : forall x a,
dom (x ~ a) = {{x}}.
Proof.
simpl. intros. apply union_empty_r.
Qed.
Lemma dom_push : forall x a E,
dom (E & x ~ a) = {{x}} \u dom E.
Proof.
auto.
Qed.
Lemma dom_cons : forall x a E,
dom ((x,a) :: E) = {{x}} \u dom E.
Proof.
auto.
Qed.
Lemma dom_concat : forall E F,
dom (E & F) = dom E \u dom F.
Proof.
induction F as [|(x,a)]; simpl.
symmetry. apply union_empty_r.
rewrite IHF. apply union_comm_assoc.
Qed.
Lemma dom_map : forall f E,
dom (map f E) = dom E.
Proof.
induction E as [|(x,a)]; simpl; congruence.
Qed.
End OpProperties.
Implicit Arguments eq_empty_inv [A x a E F].
Implicit Arguments eq_push_inv [A E x a E' x' a'].
Hint Rewrite
concat_empty
map_concat
dom_empty dom_single dom_push dom_cons dom_concat dom_map : rew_env.
Hint Rewrite <- concat_assoc : rew_env.
Tactic Notation "simpl_env" :=
autorewrite with rew_env in *.
Hint Extern 1 (_ # _) => simpl_env; notin_solve.
Ltac env_fix_core :=
let go := try env_fix_core in
match goal with
| H: context [(?x,?a)::?E] |- _ =>
( (progress (change ((x,a)::E) with (E & x ~ a) in H))
|| (progress (unsimpl (E & x ~ a) in H)) ); go
| |- context [(?x,?a)::?E] =>
( (progress (change ((x,a)::E) with (E & x ~ a)))
|| (progress (unsimpl (E & x ~ a))) ); go
| H: context [@nil ((var * ?A)%type)] |- _ =>
progress (change (@nil ((var * A)%type)) with (@empty A) in H); go
| |- context [@nil ((var * ?A)%type)] =>
progress (change (@nil ((var * A)%type)) with (@empty A)); go
end.
Ltac env_fix := try env_fix_core.
Section OkProperties.
Variable A : Set.
Implicit Types E F : env A.
Implicit Types a b : A.
Hint Constructors ok.
Lemma ok_concat_inv : forall E F,
ok (E & F) -> ok E /\ ok F.
Proof.
induction F as [|(x,a)]; simpl; env_fix; intros Ok.
auto*.
inversions Ok. split. auto*. apply* ok_push.
Qed.
Lemma ok_remove : forall F E G,
ok (E & F & G) -> ok (E & G).
Proof.
induction G as [|(y,a)]; simpl; env_fix; intros Ok.
induction F as [|(y,a)]; simpl.
auto.
inversions* Ok.
inversions* Ok.
Qed.
Lemma ok_map : forall E F (f : A -> A),
ok (E & F) -> ok (E & map f F).
intros. induction F as [|(y,a)]; simpl; env_fix.
auto.
rewrite <- concat_assoc in H. inversions* H.
Qed.
Lemma fresh_mid : forall E F x a,
ok (E & x ~ a & F) -> x # E.
Proof.
induction F; simpl; introv Ok; inversions Ok; env_fix.
auto.
inversions H1; env_fix.
contradictions. fold (@empty A) in H0. apply* eq_empty_inv.
simpls*.
Qed.
End OkProperties.
Hint Resolve fresh_mid ok_map.
Hint Extern 1 (ok (?E & ?G)) =>
match goal with H: context [E & ?F & G] |- _ =>
apply (@ok_remove _ F) end.
Section BindsProperties.
Variable A : Set.
Implicit Types E F : env A.
Implicit Types a b : A.
Hint Extern 1 (_ \notin _) => notin_solve.
Lemma binds_head : forall x a E,
binds x a (E & x ~ a).
Proof.
intros. unfold binds. simpl. case_var*.
Qed.
Lemma binds_tail : forall x y a b E,
x <> y -> binds x a E -> binds x a (E & y ~ b).
Proof.
intros. unfold binds. simpl. case_var*.
Qed.
Lemma binds_func : forall x a b E,
binds x a E -> binds x b E -> a = b.
Proof.
unfold binds. introv B1 B2.
poses H (trans_eq (sym_eq B1) B2).
inversion* H.
Qed.
Lemma binds_empty : forall x a,
binds x a empty -> False.
Proof.
introv H. inversions H.
Qed.
Lemma binds_fresh : forall x a E,
binds x a E -> x # E -> False.
Proof.
unfold binds. induction E as [|(y,b)]; simpl; intros Has Fresh.
contradictions.
case_var*. notin_contradiction.
Qed.
Lemma binds_concat_fresh : forall x a E F,
binds x a E -> x # F -> binds x a (E & F).
Proof.
unfold binds. induction F as [|(y,b)]; simpl; intros.
auto. case_var*. notin_contradiction.
Qed.
Lemma binds_concat_ok : forall x a E F,
binds x a E -> ok (E & F) -> binds x a (E & F).
Proof.
unfolds binds. induction F as [|(y,b)]; simpl; intros Map Ok.
auto.
inversions Ok. case_var.
contradictions. apply* (@binds_fresh y a E).
auto.
Qed.
Lemma binds_prepend : forall x a E F,
binds x a F -> binds x a (E & F).
Proof.
unfold binds. induction F as [|(y,b)]; simpl; intros Map.
contradictions. case_var*.
Qed.
Lemma binds_concat_inv : forall x a E F,
binds x a (E & F) -> (x # F /\ binds x a E) \/ (binds x a F).
Proof.
unfold binds. induction F as [|(y,b)]; simpl; intros Map.
left*.
case_var.
right*.
destruct (IHF Map) as [[Fr Map2] | Map2]. left*. right*.
Qed.
Lemma binds_map : forall x a f E,
binds x a E -> binds x (f a) (map f E).
Proof.
unfold binds. induction E as [|(y,b)]; simpl; intros Map.
contradictions. case_var*. inversions* Map.
Qed.
Lemma binds_mid : forall x a E F,
ok (E & x ~ a & F) -> binds x a (E & x ~ a & F).
Proof.
unfold binds. induction F as [|(y,b)]; simpl; intros Ok.
case_var*.
inversions Ok. case_var.
simpl_env. notin_contradiction.
auto.
Qed.
Lemma binds_mid_eq : forall z a b E F,
binds z a (E & z ~ b & F) -> ok (E & z ~ b & F) -> a = b.
Proof.
unfold binds. induction F as [|(y,c)]; simpl; intros Map Ok.
case_var*. inversions* Map.
inversions Ok. case_var.
inversions Ok. simpl_env. notin_contradiction.
auto.
Qed.
Lemma binds_single_inv : forall x y a b,
binds x a (y ~ b) -> x = y /\ a = b.
Proof.
unfold binds. simpl. intros. case_var.
inversions* H.
contradictions.
Qed.
Lemma binds_weaken : forall x a E F G,
binds x a (E & G) -> ok (E & F & G) ->
binds x a (E & F & G).
Proof.
unfold binds. induction G as [|(y,b)]; simpl; intros Map Ok.
apply* binds_concat_ok.
inversions Ok. case_var*.
Qed.
Lemma binds_dec : forall E x a,
(forall a1 a2 : A, {a1 = a2} + {a1 <> a2}) ->
decidable (binds x a E).
Proof.
introv Dec. remember (get x E) as B. symmetry in HeqB.
unfold binds. destruct B as [a'|].
destruct (Dec a a'). subst.
left*.
right. intros H. congruence.
right. intros H. congruence.
Qed.
End BindsProperties.
Implicit Arguments binds_concat_inv [A x a E F].
Hint Resolve binds_head binds_tail.
Section ExtendsProperties.
Variable A : Set.
Implicit Types E F : env A.
Lemma extends_self : forall E,
extends E E.
Proof.
introz. auto.
Qed.
Lemma extends_push : forall E x a,
x # E -> extends E (E & x ~ a).
Proof.
introz. apply* binds_tail.
destruct (x0 == x).
subst. contradictions. apply* binds_fresh.
auto.
Qed.
Lemma binds_inj : forall E x a b,
binds x a E -> binds x b E -> a = b.
Proof.
unfold binds. intros. congruence.
Qed.
Lemma extends_binds : forall E x a,
binds x a E -> extends E (E & x ~ a).
Proof.
introz. unfolds binds. simpl. case_var. congruence. auto.
Qed.
End ExtendsProperties.
Hint Resolve extends_self extends_push extends_binds.
Section IterPush.
Variable A : Set.
Implicit Types E F : env A.
Definition iter_push (xs : list var) (vs : list A) :=
rev (combine xs vs).
Lemma iter_push_nil : forall xs,
iter_push xs nil = nil.
Proof.
induction xs; simpl*.
Qed.
Lemma iter_push_cons : forall x (v : A) xs vs,
iter_push (x::xs) (v::vs) = (x ~ v) & (iter_push xs vs).
Proof.
auto*.
Qed.
Lemma ok_concat_iter_push : forall xs E (Us : list A),
ok E ->
fresh (dom E) (length xs) xs ->
ok (E & iter_push xs Us).
Proof.
induction xs; simpl; intros. auto.
destruct H0. destruct Us; simpls. auto.
rewrite iter_push_cons. rewrite* <- concat_assoc.
Qed.
End IterPush.
Hint Resolve ok_concat_iter_push.
Fixpoint fv_in (A : Set) (fv : A -> vars) (E : env A) {struct E} : vars :=
match E with
| nil => {}
| (x,a)::E' => (fv a) \u fv_in fv E'
end.
Lemma fv_in_spec : forall (A : Set) (fv : A -> vars) x a (E : env A),
binds x a E -> (fv a) << (fv_in fv E).
Proof.
unfold binds; induction E as [|(y,b)]; simpl; intros B.
contradictions.
case_var.
inversions B. apply subset_union_weak_l.
apply* (@subset_trans (fv_in fv E)). apply subset_union_weak_r.
Qed.
Opaque binds.
Tactic Notation "binds_get" constr(H) "as" ident(EQ) :=
match type of H with binds ?z ?a (?E & ?x ~ ?b & ?F) =>
let K := fresh in assert (K : ok (E & x ~ b & F));
[ auto | poses EQ (@binds_mid_eq _ z a b E F H K); clear K ] end.
Tactic Notation "binds_get" constr(H) :=
let EQ := fresh in binds_get H as EQ;
try match type of EQ with
| ?f _ = ?f _ => inversions EQ; clear EQ
| ?x = ?y => subst x end.
Ltac binds_single H :=
match type of H with binds ?x ?a (?y ~ ?b) =>
destruct (binds_single_inv H);
try discriminate; try subst y;
try match goal with N: ?x <> ?x |- _ =>
contradictions; apply N; reflexivity end end.
Tactic Notation "binds_case" constr(H) "as" ident(B1) ident(B2) :=
let Fr := fresh "Fr" in
destruct (binds_concat_inv H) as [[Fr B1] | B2].
Ltac binds_cases H :=
let go B := clear H;
first [ binds_single B | binds_cases B | idtac ] in
let B1 := fresh "B" in let B2 := fresh "B" in
binds_case H as B1 B2; simpl_env; [ go B1 | go B2 ].
Hint Resolve
binds_concat_fresh binds_concat_ok
binds_prepend binds_map.
Tactic Notation "apply_ih_bind" constr(H) :=
do_rew concat_assoc (eapply H).
Tactic Notation "apply_ih_bind" "*" constr(H) :=
do_rew* concat_assoc (eapply H).
Tactic Notation "apply_ih_map_bind" constr(H) :=
do_rew concat_assoc_map_push (eapply H).
Tactic Notation "apply_ih_map_bind" "*" constr(H) :=
do_rew* concat_assoc_map_push (eapply H).
Tactic Notation "apply_empty" constr(lemma) :=
let H := fresh in poses H (@lemma empty);
simpl in H; eapply H; env_fix; clear H.
Tactic Notation "apply_empty" "*" constr(lemma) :=
apply_empty lemma; auto*.
End Env.