Top.Util.Signatures

IMPORTANT

THIS IS A COPY OF THE Environment FILE, RENAMED TO Signatures

Operations, lemmas, and tactics for working with environments, association lists whose keys are labels. 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

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

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

Module Signatures.

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 labels that it maps.

Fixpoint dom (E : list (label × A)) : labels :=
  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 (label × A)) : list (label × B) :=
  match E with
  | nil ⇒ nil
  | (x, V) :: E' ⇒ (x, f V) :: map f E'
  end.

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

Fixpoint get (x : label) (E : list (label × A)) : option A :=
  match E with
  | nil ⇒ None
  | (y,a) :: E' ⇒ if eq_label_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 label is bound at most once.

Inductive ok : list (label × A) → Prop :=
  | ok_nil :
      ok nil
  | ok_cons : ∀ (E : list (label × A)) (x : label) (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 (label × A)) :=
  get x E = Some b.

End Relations.

Properties of operations

Section OpProperties.
Variable A B : Type.
Implicit Types E F : list (label × 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 : label × A) := x :: nil.

Lemma cons_concat : ∀ (A : Type) (E : list (label × 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 : label) (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

(*

TODO adding this hint globally causes lsetdec to not terminate...

Hint Extern 1 (~ In _ _) => simpl_env in *; lsetdec : core. *)

Properties of well-formedness and freshness

Section OkProperties.


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

Facts about when an environment is well-formed.

Lemma ok_push : ∀ (E : list (label × A)) (x : label) (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 label 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 (label × 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 (label × 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)

(*
Hint Resolve binds_map binds_concat_ok binds_weaken binds_weaken_at_head : core.

Hint Immediate binds_remove_mid binds_remove_mid_cons : core. *)

End Signatures.

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

Tactic Notation "srewrite_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; Signatures.simpl_env; reflexivity ]
  end.