Top.Util.Environment

Operations, lemmas, and tactics for working with environments, association lists whose keys are atoms. Unless stated otherwise, implicit arguments will not be declared by default.

Authors: Brian Aydemir and Arthur Charguéraud, with help from Aaron Bohannon, Benjamin Pierce, Jeffrey Vaughan, Dimitrios Vytiniotis, Stephanie Weirich, and Steve Zdancewic.

Table of contents:

• Overview
• Functions on environments
• Relations on environments
• Properties of operations
• Automation and tactics (I)
• Properties of well-formedness and freshness
• Properties of binds
• Automation and tactics (II)
• Additional properties of binds
• Automation and tactics (III)

Overview

An environment is a list of pairs, where the first component of each pair is an atom. We view the second component of each pair as being bound to the first component. In a well-formed environment, there is at most one binding for any given atom. Bindings at the head of the list are "more recent" than bindings toward the tail of the list, and we view an environment as growing on the left, i.e., at its head.

We normally work only with environments built up from the following: the empty list, one element lists, and concatenations of two lists. This seems to be more convenient in practice. For example, we don't need to distinguish between consing on a binding and concatenating a binding, a difference that Coq's tactics can be sensitive to.

However, basic definitions are by induction on the usual structure of lists (nil and cons).

To make it convenient to write one element lists, we define a special notation. Note that this notation is local to this particular library, to allow users to use alternate notations if they desire.

Notation "[ x ]" := (cons x nil).

In the remainder of this library, we define a number of operations, lemmas, and tactics that simplify working with environments.

Functions on environments

Implicit arguments will be declared by default for the definitions in this section.

Section Definitions.

Variables A B : Type.

The domain of an environment is the set of atoms that it maps.

Fixpoint dom (E : list (atom × A)) : atoms :=
  match E with
  | nil ⇒ empty
  | (x, _) :: E' ⇒ union (singleton x) (dom E')
  end.

map applies a function to all bindings in the environment.

Fixpoint map (f : A → B) (E : list (atom × A)) : list (atom × B) :=
  match E with
  | nil ⇒ nil
  | (x, V) :: E' ⇒ (x, f V) :: map f E'
  end.

get returns the value bound to the given atom in an environment or None if the given atom is not bound. If the atom has multiple bindings, the one nearest to the head of the environment is returned.

Fixpoint get (x : atom) (E : list (atom × A)) : option A :=
  match E with
  | nil ⇒ None
  | (y,a) :: E' ⇒ if eq_atom_dec x y then Some a else get x E'
  end.

End Definitions.

Relations on environments

Implicit arguments will be declared by default for the definitions in this section.

Section Relations.

Variable A : Type.

An environment is well-formed if and only if each atom is bound at most once.

Inductive ok : list (atom × A) → Prop :=
  | ok_nil :
      ok nil
  | ok_cons : ∀ (E : list (atom × A)) (x : atom) (a : A),
      ok E → ¬ In x (dom E) → ok ((x, a) :: E).

An environment E contains a binding from x to b, denoted (binds x b E), if and only if the most recent binding for x is mapped to b.

Definition binds x b (E : list (atom × A)) :=
  get x E = Some b.

End Relations.

Properties of operations

Section OpProperties.
Variable A B : Type.
Implicit Types E F : list (atom × A).
Implicit Types a b : A.

Facts about concatenation

Lemma concat_nil : ∀ E,
  E ++ nil = E.

Lemma nil_concat : ∀ E,
  nil ++ E = E.

Lemma concat_assoc : ∀ E F G,
  (G ++ F) ++ E = G ++ (F ++ E).

map commutes with environment-building operations

Lemma map_nil : ∀ (f : A → B),
  map f nil = nil.

Lemma map_single : ∀ (f : A → B) y b,
  map f [(y,b)] = [(y, f b)].

Lemma map_push : ∀ (f : A → B) y b E,
  map f ([(y,b)] ++ E) = [(y, f b)] ++ map f E.

Lemma map_concat : ∀ (f : A → B) E F,
  map f (F ++ E) = (map f F) ++ (map f E).

Facts about the domain of an environment

Lemma dom_nil :
  @dom A nil = empty.

Lemma dom_single : ∀ x a,
  dom [(x,a)] = singleton x.

Lemma dom_push : ∀ x a E,
  dom ([(x,a)] ++ E) = union (singleton x) (dom E).

Lemma dom_concat : ∀ E F,
  dom (F ++ E) = union (dom F) (dom E).

Lemma dom_map : ∀ (f : A → B) E,
  dom (map f E) = dom E.

Other trivial rewrites

Lemma cons_concat_assoc : ∀ x a E F,
   ((x, a) :: E) ++ F = (x, a) :: (E ++ F).

End OpProperties.

Automation and tactics (I)

simpl_env

The simpl_env tactic can be used to put environments in the standardized form described above, with the additional properties that concatenation is associated to the right and empty environments are removed. Similar to the simpl tactic, we define "in ×" and "in H" variants of simpl_env.

Definition singleton_list (A : Type) (x : atom × A) := x :: nil.

Lemma cons_concat : ∀ (A : Type) (E : list (atom × A)) x a,
  (x, a) :: E = singleton_list A (x, a) ++ E.

Lemma map_singleton_list : ∀ (A B : Type) (f : A → B) y b,
  map f (singleton_list A (y,b)) = [(y, f b)].

Lemma dom_singleton_list : ∀ (A : Type) (x : atom) (a : A),
  dom (singleton_list A (x,a)) = singleton x.




Tactic Notation "simpl_env" "in" hyp(H) :=
  simpl_env_change_aux;
  autorewrite with rew_env in H;
  unfold singleton_list in ×.

Tactic Notation "simpl_env" "in" "*" :=
  simpl_env_change_aux;
  autorewrite with rew_env in *;
  unfold singleton_list in ×.

rewrite_env

The tactic (rewrite_env E) replaces an environment in the conclusion of the goal with E. Suitability for replacement is determined by whether simpl_env can put E and the chosen environment in the same normal form, up to convertability in Coq. We also define a "in H" variant that performs the replacement in a hypothesis H.

Tactic Notation "rewrite_env" constr(E) :=
  match goal with
    | |- context[?x] ⇒
      change x with E
    | |- context[?x] ⇒
      replace x with E; [ | try reflexivity; simpl_env; reflexivity ]
  end.

Tactic Notation "rewrite_env" 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_env; reflexivity ]
  end.

Hints

(* ********************************************************************** *)

Properties of well-formedness and freshness

Section OkProperties.
Variable A B : Type.
Implicit Types E F : list (atom × A).
Implicit Types a b : A.

Facts about when an environment is well-formed.

Lemma ok_push : ∀ (E : list (atom × A)) (x : atom) (a : A),
      ok E → ¬ In x (dom E) → ok ([(x, a)] ++ E).

Lemma ok_singleton : ∀ x a,
  ok [(x,a)].

Lemma ok_remove_mid : ∀ F E G,
  ok (G ++ F ++ E) → ok (G ++ E).

Lemma ok_remove_mid_cons : ∀ x a E G,
  ok (G ++ (x, a) :: E) →
  ok (G ++ E).

Lemma ok_map : ∀ E (f : A → B),
  ok E → ok (map f E).

Lemma ok_map_app_l : ∀ E F (f : A → A),
  ok (F ++ E) → ok (map f F ++ E).

A binding in the middle of an environment has an atom fresh from all bindings before and after it.

Lemma fresh_mid_tail : ∀ E F x a,
  ok (F ++ [(x,a)] ++ E) → ¬ In x (dom E).

Lemma fresh_mid_head : ∀ E F x a,
  ok (F ++ [(x,a)] ++ E) → ¬ In x (dom F).

End OkProperties.

Properties of binds

Section BindsProperties.
Variable A B : Type.
Implicit Types E F : list (atom × A).
Implicit Types a b : A.

Introduction forms for binds

The following properties allow one to view binds as an inductively defined predicate. This is the preferred way of working with the relation.

Lemma binds_singleton : ∀ x a,
  binds x a [(x,a)].

Lemma binds_tail : ∀ x a E F,
  binds x a E → ¬ In x (dom F) → binds x a (F ++ E).

Lemma binds_head : ∀ x a E F,
  binds x a F → binds x a (F ++ E).

Case analysis on binds

Lemma binds_concat_inv : ∀ x a E F,
  binds x a (F ++ E) → (¬ In x (dom F) ∧ binds x a E) ∨ (binds x a F).

Lemma binds_singleton_inv : ∀ x y a b,
  binds x a [(y,b)] → x = y ∧ a = b.

Retrieving bindings from an environment

Lemma binds_mid : ∀ x a E F,
  ok (F ++ [(x,a)] ++ E) → binds x a (F ++ [(x,a)] ++ E).

Lemma binds_mid_eq : ∀ z a b E F,
  binds z a (F ++ [(z,b)] ++ E) → ok (F ++ [(z,b)] ++ E) → a = b.

Lemma binds_mid_eq_cons : ∀ x a b E F,
  binds x a (F ++ (x,b) :: E) →
  ok (F ++ (x,b) :: E) →
  a = b.

End BindsProperties.

Automation and tactics (II)

Hints

binds_get

The tactic (binds_get H) takes a hypothesis H of the form (binds x a (F ++ [(x,b)] ++ E)) and introduces the equality a=b into the context. Then, the tactic checks if the equality is discriminable and otherwise tries substituting b for a. The auto tactic is used to show that (ok (F ++ [(x,b)] ++ E)), which is needed to prove the equality a=b from H.

binds_cases

The tactic (binds_case H) performs a case analysis on an hypothesis H of the form (binds x a E). There will be one subgoal for each component of E that x could be bound in, and each subgoal will have appropriate freshness conditions on x. Some attempts are made to automatically discharge contradictory cases.

Additional properties of binds

The following lemmas are proven in manner that should be independent of the concrete definition of binds.

Section AdditionalBindsProperties.
Variable A B : Type.
Implicit Types E F : list (atom × A).
Implicit Types a b : A.

Lemmas about the relationship between binds and the domain of an environment.

Lemma binds_In : ∀ a x E,
  binds x a E → In x (dom E).

Lemma binds_fresh : ∀ x a E,
  ¬ In x (dom E) → ¬ binds x a E.

Additional lemmas for showing that a binding is in an environment.

Lemma binds_map : ∀ x a (f : A → B) E,
  binds x a E → binds x (f a) (map f E).

Lemma binds_concat_ok : ∀ x a E F,
  binds x a E → ok (F ++ E) → binds x a (F ++ E).

Lemma binds_weaken : ∀ x a E F G,
  binds x a (G ++ E) →
  ok (G ++ F ++ E) →
  binds x a (G ++ F ++ E).

Lemma binds_weaken_at_head : ∀ x a F G,
  binds x a G →
  ok (F ++ G) →
  binds x a (F ++ G).

Lemma binds_remove_mid : ∀ x y a b F G,
  binds x a (F ++ [(y,b)] ++ G) →
  x ≠ y →
  binds x a (F ++ G).

Lemma binds_remove_mid_cons : ∀ x y a b E G,
  binds x a (G ++ (y, b) :: E) →
  x ≠ y →
  binds x a (G ++ E).

End AdditionalBindsProperties.

Automation and tactics (III)