Library Metatheory_Env

Require Import Lib_Tactic List Decidable Metatheory_Var Metatheory_Fresh.

Definitions of Environments


Module Env.

Structure and Basic Operations on Environments


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.

Notations


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.

Relations on environemnts


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.

Properties of Environemnts


Hint Constructors ok.

Open Local Scope env_scope.

Properties of Operations


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.

Properties of Well-formedness and Freshness


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.

Properties of the binds relation


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.

Properties of environment inclusion


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.

Iteration of pushing bindings in the environment


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.

Gathering free variables of the values contained in an

environment

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).

Tactics


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.

Other tactics (syntactical sugar for tactics)


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.