Library Metatheory_Env
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.
Environments is represented as an associative list.
Definition env := list (var * A).
Empty environment.
Definition empty : env := nil.
An environment containing only one binding mapping x to a.
Definition single x a := (x,a) :: nil.
Concatenation of environments E and F.
Definition concat (E F : env) := F ++ E.
Comutes the domain of the environment, i.e. the set of vars mapped.
Fixpoint dom (E : env) : vars :=
match E with
| nil => {}
| (x, _) :: E' => {{x}} \u (dom E')
end.
map
applies a function to all the values mapped by the environment.
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.
get
locates a binding in an environment.
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].
x ~ a
is the notation for a singleton environment mapping x to a.
Notation "x ~ a" := (single x a)
(at level 31, left associativity) : env_scope.
E & F
is the notation for concatenation of E and F.
Notation "E & F" := (concat E F)
(at level 40, left associativity) : env_scope.
x # E
to be read x fresh from E captures the fact that
x is unbound in E .
Notation "x '#' E" := (x \notin (dom E)) (at level 60) : env_scope.
Open Local Scope env_scope.
Section Relations.
Variable A : Set.
An environment is well-formed iff it contains no duplicate
bindings.
Inductive ok : env A -> Prop :=
| ok_empty :
ok empty
| ok_push : forall E x a,
ok E -> x # E -> ok (E & x ~ a).
An environment contains a binding from x to a iff the most recent
binding on x is mapped to a
Definition binds x a (E : env A) :=
get x E = Some a.
Proposition capturing the idea that a proposition P holds on all
values containted in the environment.
Definition env_prop (P : A -> Prop) (E : env A) :=
forall x a, binds x a E -> P a.
Inclusion of an environment in another one.
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.
Concatenation with an empty environment is identity.
Lemma concat_empty : forall E,
E & empty = E.
Concatenation is associative.
Lemma concat_assoc : forall E F G,
(E & F) & G = E & (F & G).
Map commutes with substitution.
Lemma map_concat : forall f E F,
map f (E & F) = (map f E) & (map f F).
Interaction of associativity and map.
Lemma concat_assoc_map_push : forall f E F y V,
(E & map f F) & y ~ (f V) = E & (map f (F & y ~ V)).
Inversion results.
Lemma eq_empty_inv : forall x a E F,
empty = E & x ~ a & F -> False.
Lemma eq_push_inv : forall E x a E' x' a',
E & x ~ a = E' & x' ~ a' -> E = E' /\ x = x' /\ a = a'.
Domain of an empty environment.
Lemma dom_empty :
dom (A:=A) empty = {}.
Domain of a singleton environment.
Lemma dom_single : forall x a,
dom (x ~ a) = {{x}}.
Domain of a push is the head variable union the domain of the tail.
Lemma dom_push : forall x a E,
dom (E & x ~ a) = {{x}} \u dom E.
Domain of a cons is the head variable union the domain of the tail.
Lemma dom_cons : forall x a E,
dom ((x,a) :: E) = {{x}} \u dom E.
Domain of a concatenation is the union of the domains.
Lemma dom_concat : forall E F,
dom (E & F) = dom E \u dom F.
Map preserves the domain.
Lemma dom_map : forall f E,
dom (map f E) = dom E.
End OpProperties.
Implicit Arguments eq_empty_inv [A x a E F].
Implicit Arguments eq_push_inv [A E x a E' x' a'].
Simplification tactics
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.
The
env_fix
tactic is used to convert environments
from (x,a)::E
to E & x ~ a
.
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.
Inversion for ok on concat
Lemma ok_concat_inv : forall E F,
ok (E & F) -> ok E /\ ok F.
Removing bindings preserves ok
Lemma ok_remove : forall F E G,
ok (E & F & G) -> ok (E & G).
Mapping values preserves ok
Lemma ok_map : forall E F (f : A -> A),
ok (E & F) -> ok (E & map f F).
A binding in the middle of an environment has a var fresh
from all the bindings before it
Lemma fresh_mid : forall E F x a,
ok (E & x ~ a & F) -> x # E.
End OkProperties.
Automation
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.
Binds at head
Lemma binds_head : forall x a E,
binds x a (E & x ~ a).
Binds in tail
Lemma binds_tail : forall x y a b E,
x <> y -> binds x a E -> binds x a (E & y ~ b).
Binds is functional
Lemma binds_func : forall x a b E,
binds x a E -> binds x b E -> a = b.
No binding in an empty environment
Lemma binds_empty : forall x a,
binds x a empty -> False.
No binding on x if x is fresh from the environment
Lemma binds_fresh : forall x a E,
binds x a E -> x # E -> False.
Binding on x preserved by concatenation if x is fresh
for the extension
Lemma binds_concat_fresh : forall x a E F,
binds x a E -> x # F -> binds x a (E & F).
Binding on x preserved by concatenation if the result
of the concatenation is a well-formed environment
Lemma binds_concat_ok : forall x a E F,
binds x a E -> ok (E & F) -> binds x a (E & F).
Bindings preserved by pre-catenation
Lemma binds_prepend : forall x a E F,
binds x a F -> binds x a (E & F).
Case analysis on the belonging of a binding to a concatenation
Lemma binds_concat_inv : forall x a E F,
binds x a (E & F) -> (x # F /\ binds x a E) \/ (binds x a F).
Interaction of binds and map
Lemma binds_map : forall x a f E,
binds x a E -> binds x (f a) (map f E).
Retreive the binding on x from an environment
E & (x~a) & F
Lemma binds_mid : forall x a E F,
ok (E & x ~ a & F) -> binds x a (E & x ~ a & F).
The binding on x in the environment
E & (x~a) & F
can only
be bound to a if that environment is well-formed
Lemma binds_mid_eq : forall z a b E F,
binds z a (E & z ~ b & F) -> ok (E & z ~ b & F) -> a = b.
Inversion on a binding in an atomic environment
Lemma binds_single_inv : forall x y a b,
binds x a (y ~ b) -> x = y /\ a = b.
Interaction between binds and the insertion of bindings.
In theory we don't need this lemma since it would suffice
to use the binds_cases tactics, but since weakening is a
very common operation we provide a lemma for it.
Lemma binds_weaken : forall x a E F G,
binds x a (E & G) -> ok (E & F & G) ->
binds x a (E & F & G).
Lemma binds_dec : forall E x a,
(forall a1 a2 : A, {a1 = a2} + {a1 <> a2}) ->
decidable (binds x a E).
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.
Lemma extends_push : forall E x a,
x # E -> extends E (E & x ~ a).
Lemma binds_inj : forall E x a b,
binds x a E -> binds x b E -> a = b.
Lemma extends_binds : forall E x a,
binds x a E -> extends E (E & x ~ a).
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.
Lemma iter_push_cons : forall x (v : A) xs vs,
iter_push (x::xs) (v::vs) = (x ~ v) & (iter_push xs vs).
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).
End IterPush.
Hint Resolve ok_concat_iter_push.
Computing free variables contained in an environment.
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.
Specification of the above function in terms of
bind
.
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).
Opaque binds.
binds_get H as EQ
produces from an hypothesis H
of
the form binds x a (E & x ~ b & F)
the equality EQ: a = b
.
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.
binds_get H
expects an hypothesis H
of the form
binds x a (E & x ~ b & F)
and substitute a
for b
in the goal.
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.
binds_single H
derives from an hypothesis H
of the form
binds x a (y ~ b)
the equalities x = y
and a = b
, then
it substitutes x
for y
in the goal or deduce a contradiction
if x <> y
can be found in the context.
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.
binds_case H as B1 B2
derives from an hypothesis H
of the form
binds x a (E & F)
two subcases: B1: binds x a E
(with a freshness
condition x # F
) and B2: binds x a F
.
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].
binds_case H
makes a case analysis on an hypothesis H
of the form
binds x a E
where E can be constructed using concatenation and
singletons. It calls binds_single
when reaching a singleton.
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 ].
Automation
Hint Resolve
binds_concat_fresh binds_concat_ok
binds_prepend binds_map.
Tactic to apply an induction hypothesis modulo a rewrite of
the associativity of the environment necessary to handle the
inductive rules dealing with binders.
apply_ih_bind
is in
fact just a syntactical sugar for do_rew concat_assoc (eapply H)
which in turns stands for
rewrite concat_assoc; eapply H; rewrite <- concat_assoc
.
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).
Similar as the above, except in the case where there
is also a map function, so we need to use
concat_assoc_map_push
for rewriting.
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).
apply_empty
applies a lemma of the form "forall E:env, P E"
in the particular case where E is empty. The tricky step is
the simplification of "P empty" before the "apply" tactic is
called, and this is necessary for Coq to recognize that the
lemma indeed applies.
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.