Coral.Env: generic environments

Author: Benoît Montagu
Copyright © Inria 2020 CeCILL-B License
Synopsis: Environments, generic functions on environments, and basic properties.

Require Import Metalib.Metatheory.
Require Import Lia.

Environment are association lists that are indexed by atoms.
Definition env (A: Type) := list (atom × A).

Extra results about map


Lemma map_id' {A} (e: env A):
  map id e = e.
Proof.
  unfold map. rewrite <- map_id.
  apply map_ext.
  intros [? ?]. reflexivity.
Qed.

Lemma map_map' {A B C} (f: B → C) (g: A → B) (e: env A):
  map f (map g e) = map (fun x ⇒ f (g x)) e.
Proof.
  unfold map. rewrite map_map. apply map_ext.
  intros [? ?]. reflexivity.
Qed.

Definition mapi and its properties

mapi f [(x1, a1), ..., (xn, an)] is the environment [(x1, f x1 a1), ..., (xn, f xn an)].
Definition mapi {A B} (f: atom → A → B) (e: env A) : env B :=
  List.map (fun b ⇒ match b with (x, a) ⇒ (x, f x a) end) e.

Section Mapi.
  Variables A B : Type.
  Variable f : atom → A → B.
  Variable x : atom.
  Variable b : A.
  Variables E F : list (atom × A).

  Lemma mapi_nil :
    mapi f (@nil (atom × A)) = nil.
  Proof. clear. reflexivity. Qed.

  Lemma mapi_one :
    mapi f (x ¬ b) = (x ¬ f x b).
  Proof. clear. reflexivity. Qed.

  Lemma mapi_cons :
    mapi f ((x, b) :: E) = x ¬ f x b ++ mapi f E.
  Proof. clear. reflexivity. Qed.

  Lemma mapi_app :
    mapi f (E ++ F) = mapi f E ++ mapi f F.
  Proof. clear. unfold mapi. rewrite List.map_app. reflexivity. Qed.

  Lemma dom_mapi :
    dom (mapi f E) [=] dom E.
  Proof. clear. intros. induction E as [ | [? ?] ]; simpl; fsetdec. Qed.

  Lemma get_mapi :
    get x (mapi f E) =
    match get x E with
    | Some a ⇒ Some (f x a)
    | None ⇒ None
    end.
  Proof.
    env induction E; simpl; auto.
    destruct (x == x0); subst; auto.
  Qed.
End Mapi.

Extra results about get


Lemma get_update_this {A: Type} x (a: A) (e: env A) :
  get x (x ¬ a ++ e) = Some a.
Proof.
  simpl. destruct (x == x); congruence.
Qed.
Hint Resolve get_update_this : core.

Lemma get_update_other {A: Type} y x (a: A) (e: env A) :
  y ≠ x →
  get y (x ¬ a ++ e) = get y e.
Proof.
  simpl. destruct (y == x); congruence.
Qed.
Hint Resolve get_update_other : core.

Lemma get_decompose_env {A} (e: env A) x (a: A) :
  get x e = Some a ↔
  ∃ e1 e2, e = e1 ++ [(x, a)] ++ e2 ∧ x `notin` dom e1.
Proof.
  revert a. env induction e; intros.
  - split; intro H.
    + exfalso. simpl in H. discriminate.
    + exfalso.
      destruct H as [e1 [e2 [Heq Hx]]].
      destruct e1; simpl in Heq; discriminate.
  - simpl get. destruct (x == x0); subst.
    + split; intro H.
      × inversion H; subst. ∃ nil, xs. split; auto.
      × { f_equal. destruct H as [e1 [e2 [Heq Hx0]]].
          destruct e1 as [| [y b] e1].
          - simpl in Heq. congruence.
          - exfalso. simpl in Heq. inversion Heq; subst; clear Heq.
            simpl in Hx0. fsetdec.
        }
    + rewrite IHe. clear IHe.
      split; intros [e1 [e2 [Heq Hx]]]; subst.
      × { ∃ ([(x0, a)] ++ e1), e2. split.
          - simpl_env. reflexivity.
          - simpl. fsetdec.
        }
      × { destruct e1 as [| [y b] e1].
          - exfalso. simpl in Heq. congruence.
          - simpl in Heq. inversion Heq; subst; clear Heq.
            ∃ e1, e2. split.
            + simpl_env. reflexivity.
            + simpl in Hx. auto.
        }
Qed.

Lemma get_map {A B} (f: A → B) x (e: env A):
  get x (map f e) =
  match get x e with
  | Some a ⇒ Some (f a)
  | None ⇒ None
  end.
Proof.
  env induction e; simpl; auto.
  destruct (x == x0); subst; auto.
Qed.

Lemma get_app_left {A} x (e1 e2: env A):
  get x e1 ≠ None →
  get x (e1 ++ e2) = get x e1.
Proof.
  intro H. env induction e1; simpl in *; auto.
  - contradiction.
  - destruct (x == x0); subst; auto.
Qed.

Lemma get_app_right {A} x (e1 e2: env A):
  get x e1 = None →
  get x (e1 ++ e2) = get x e2.
Proof.
  intro H. env induction e1; simpl in *; auto.
  destruct (x == x0); subst; auto.
  congruence.
Qed.

Lemma get_in_dom {A} x (a: A) (e: list (atom × A)):
  get x e = Some a →
  x `in` dom e.
Proof.
  intro H. env induction e.
  - simpl in H. discriminate.
  - simpl in H. destruct (x == x0); subst.
    + simpl. fsetdec.
    + simpl. specialize (IHe H). fsetdec.
Qed.

Hint Resolve get_in_dom : core.

Lemma get_notin_dom {A} x (e: list (atom × A)):
  get x e = None ↔ x `notin` dom e.
Proof.
  split; intro H.
  - { env induction e; simpl in ×.
      - fsetdec.
      - destruct (x == x0); subst.
        + discriminate.
        + specialize (IHe H). fsetdec.
    }
  - { case_eq (get x e); intros; auto. apply get_in_dom in H0. exfalso. fsetdec. }
Qed.

Hint Resolve get_notin_dom : core.

Lemma in_in_dom {A} x (a: A) (e: list (atom × A)):
  In (x, a) e →
  x `in` dom e.
Proof.
   intro H. revert a H. env induction e; intros.
  - simpl in H. contradiction.
  - simpl in H. destruct H.
    + inversion H; subst.
      simpl. fsetdec.
    + simpl. specialize (IHe _ H). fsetdec.
Qed.

Hint Resolve in_in_dom : core.

Lemma get_Some_in {A} x (a: A) (e: list (atom × A)):
  get x e = Some a →
  In (x, a) e.
Proof.
  intro H. env induction e; simpl in *; auto; try discriminate.
  destruct (x == x0); subst.
  - left. congruence.
  - right. auto.
Qed.

Hint Resolve get_Some_in : core.

Lemma get_None_in {A} x (e: list (atom × A)):
  get x e = None ↔ ∀ a, ¬ In (x, a) e.
Proof.
  env induction e; simpl in *; auto.
  - tauto.
  - destruct (x == x0); subst.
    + split; intro; try discriminate.
      exfalso. apply (H a). left. reflexivity.
    + rewrite IHe. clear IHe.
      split; intros H b Hb; apply (H b); clear H; auto.
      destruct Hb; congruence.
Qed.

Hint Resolve get_None_in : core.

Extension ordering of environments leq_env

leq_env e1 e2 holds when e2 contains at least the same bindings as e1. This is Definition 2.3 of the ICFP'20 paper.
Definition leq_env {A: Type} (env1 env2: env A): Prop :=
  ∀ x v, get x env1 = Some v → get x env2 = Some v.

The empty environment is the bottom element for leq_env.
Lemma leq_env_nil_l {A: Type} (e: env A) :
  leq_env nil e.
Proof.
  intros x v H. simpl in H. congruence.
Qed.

When leq_env e1 e2, if there is no binding for x in e2, then there is also no binding for x in e1.
Lemma leq_env_get_None {A: Type} (env1 env2: env A) x:
  leq_env env1 env2 →
  get x env2 = None →
  get x env1 = None.
Proof.
  intros Hleq Hx. case_eq (get x env1); intros; auto.
  apply Hleq in H. congruence.
Qed.

The next two lemmas constitute Lemma 2.4 of the ICFP'20 paper.
leq_env is a reflexive relation.
Lemma leq_env_refl {A: Type} (env: env A): leq_env env env.
Proof.
  intros x v H. assumption.
Qed.

leq_env is a transitive relation.
Lemma leq_env_trans {A: Type} (env1 env2 env3: env A):
  leq_env env1 env2 → leq_env env2 env3 → leq_env env1 env3.
Proof.
  intros H12 H23 x v H. eauto.
Qed.

Add Parametric Relation (A: Type): (env A) (@leq_env A)
    reflexivity proved by leq_env_refl
    transitivity proved by leq_env_trans
      as leq_env_rel.

The only environment that is below the empty environment is the empty environment.
Lemma leq_env_nil_r_inv {A: Type} (e: env A):
  leq_env e nil →
  e = nil.
Proof.
  intro H. destruct e; auto.
  destruct p as [x v].
  assert (get x nil = Some v).
  { apply H. simpl_env. auto. }
  simpl in H0. congruence.
Qed.

Adding a new binding to an environment makes it greater.
Lemma leq_env_update {A: Type} (e: env A) x (a: A):
  get x e = None →
  leq_env e (x ¬ a ++ e).
Proof.
  intros H y v Hy.
  destruct (y == x); subst.
  - congruence.
  - rewrite get_update_other; auto.
Qed.

Adding an already existing binding with the same value to an environment makes it greater.
Lemma leq_env_update2 {A: Type} (e: env A) x (a: A):
  get x e = Some a →
  leq_env e (x ¬ a ++ e).
Proof.
  intros H y v Hy.
  destruct (y == x); subst.
  - rewrite get_update_this. congruence.
  - rewrite get_update_other; auto.
Qed.

Adding an already existing binding with the same value to an environment makes it smaller.
Lemma leq_env_update3 {A: Type} (e: env A) x (a: A):
  get x e = Some a →
  leq_env (x ¬ a ++ e) e.
Proof.
  intros H y v Hy.
  destruct (y == x); subst.
  - rewrite get_update_this in Hy. congruence.
  - rewrite get_update_other in Hy; auto.
Qed.

leq_env is preserved by addition of bindings.
Lemma leq_env_update_stable {A: Type} (e1 e2: env A) x (a: A):
  leq_env e1 e2 →
  leq_env (x ¬ a ++ e1) (x ¬ a ++ e2).
Proof.
  intros H y v Hy.
  destruct (y == x); subst.
  - rewrite get_update_this in ×. assumption.
  - rewrite get_update_other in *; auto.
Qed.

If leq_env e1 e2, then the domain of e1 is smaller than e2's.
Lemma leq_env_dom {A} (e1 e2: env A) :
  leq_env e1 e2 →
  dom e1 [<=] dom e2.
Proof.
  intros Hleq x Hx.
  case_eq (get x e2); intros.
  - eauto using get_in_dom.
  - eapply leq_env_get_None in H; eauto.
    apply get_notin_dom in H.
    exfalso. fsetdec.
Qed.

Hint Resolve leq_env_dom : core.

Exchanging two distinct bindings gives an extended environment.
Lemma leq_env_swap {A} x1 v1 x2 v2 (e: env A):
  x1 ≠ x2 →
  leq_env (x1 ¬ v1 ++ x2 ¬ v2 ++ e) (x2 ¬ v2 ++ x1 ¬ v1 ++ e).
Proof.
  intros Hneq z vz Hget.
  simpl in ×. destruct (z == x1); subst.
  - destruct (x1 == x2); [ contradiction | ].
    destruct (x1 == x1); congruence.
  - destruct (z == x2); subst; assumption.
Qed.

Definition of all_env and its basic properties

all_env P e is true when the property P holds for every element in e.
Fixpoint all_env {A} (P: A → Prop) (e: env A) : Prop :=
  match e with
  | nil ⇒ True
  | (x, v) :: e ⇒ P v ∧ all_env P e
  end.

Lemma all_env_get {A} (P: A → Prop) (e: env A) x v :
  all_env P e →
  get x e = Some v →
  P v.
Proof.
  intros He Hx. env induction e; simpl in ×.
  - discriminate.
  - destruct He as [Ha Hxs]. destruct (x == x0); subst; auto.
    inversion Hx; subst; auto.
Qed.

Lemma all_env_in {A} (P: A → Prop) (e: env A):
  all_env P e ↔
  ∀ x t, In (x, t) e → P t.
Proof.
  env induction e; simpl.
  - firstorder.
  - split.
    + intros [Ha Hxs] y ty.
      rewrite IHe in Hxs. clear IHe.
      intros [H|H].
      × congruence.
      × eauto.
    + intro H. split.
      × eapply H; eauto.
      × rewrite IHe. clear IHe.
        intros y ty Hy. eapply H; eauto.
Qed.

all_env commutes with conjunction.
Lemma all_env_split {A} (P1 P2: A → Prop) (e: env A) :
  all_env (fun x ⇒ P1 x ∧ P2 x) e
  ↔ (all_env P1 e ∧ all_env P2 e).
Proof.
  env induction e; simpl.
  - tauto.
  - rewrite IHe. tauto.
Qed.

Subsumption for all_env.
Lemma all_env_sub {A} (P1 P2: A → Prop) (e: env A) :
  (∀ x, P1 x → P2 x) →
  all_env P1 e →
  all_env P2 e.
Proof.
  intros H H1. env induction e; simpl in ×.
  - tauto.
  - destruct H1. split; auto.
Qed.

Definition of remove_all and its basic properties

remove_all x e removes all the bindings for the variable x from the environment e.
Fixpoint remove_all {A} x (e: env A) : env A :=
  match e with
  | nil ⇒ nil
  | (y, a) :: e ⇒ if y == x then remove_all x e else (y, a) :: remove_all x e
  end.

Lemma get_remove_all_this {A} x (e: env A):
  get x (remove_all x e) = None.
Proof.
  env induction e; simpl; auto.
  destruct (x0 == x); auto.
  simpl. destruct (x == x0); subst; auto. contradiction.
Qed.

Lemma get_remove_all_other {A} y x (e: env A):
  y ≠ x →
  get y (remove_all x e) = get y e.
Proof.
  intro Hy. env induction e; simpl; auto.
  destruct (x0 == x); subst; auto.
  - destruct (y == x); auto. contradiction.
  - simpl. destruct (y == x0); subst; auto.
Qed.

Removing the bindings for a variable that is already absent leaves the environment unchanged.
Lemma remove_all_absent {A} x (e: env A):
  get x e = None →
  remove_all x e = e.
Proof.
  intro H. env induction e; simpl; auto.
  destruct (x0 == x); subst.
  - rewrite get_update_this in H. discriminate.
  - rewrite get_update_other in H; auto. rewrite IHe; auto.
Qed.

remove_all commutes with concatenation.
Lemma remove_all_app {A} x (e1 e2: env A):
  remove_all x (e1 ++ e2) = remove_all x e1 ++ remove_all x e2.
Proof.
  env induction e1; simpl; auto.
  destruct (x0 == x); subst; auto.
  simpl_env. congruence.
Qed.

Lemma remove_all_cons_uniq {A} x v (e: env A):
  uniq (x ¬ v ++ e) →
  remove_all x (x ¬ v ++ e) = e.
Proof.
  intro H. rewrite remove_all_app.
  simpl. destruct (x == x); [| contradiction].
  simpl. apply remove_all_absent.
  apply get_notin_dom. solve_uniq.
Qed.

remove_all commutes with dom
Lemma dom_remove_all {A} x (e: env A):
  dom (remove_all x e) [=] remove x (dom e).
Proof.
  env induction e; simpl.
  - fsetdec.
  - destruct (x0 == x); subst; simpl; fsetdec.
Qed.

remove_all is a projection: it is idempotent.
Lemma remove_all_projection {A} x (e: env A):
  remove_all x (remove_all x e) = remove_all x e.
Proof.
 apply remove_all_absent.
 apply get_remove_all_this.
Qed.

remove_all commutes with itself.
Lemma remove_all_swap {A} x y (e: env A):
  remove_all x (remove_all y e) = remove_all y (remove_all x e).
Proof.
  destruct (x == y); subst.
  - reflexivity.
  - env induction e; simpl; auto.
    destruct (x0 == y); destruct (x0 == x); subst.
    + contradiction.
    + simpl. destruct (y == y); congruence.
    + simpl. destruct (x == x); congruence.
    + simpl. destruct (x0 == x); destruct (x0 == y); congruence.
Qed.

remove_all shrinks the length of an environment.
Lemma length_remove_all {A} x (e: env A):
  length (remove_all x e) ≤ length e.
Proof.
  env induction e; simpl.
  - reflexivity.
  - destruct (x0 == x); simpl; lia.
Qed.

remove_all preserves all_env P.
Lemma all_env_remove_all {A} (P: A → Prop) x (e: env A):
  all_env P e →
  all_env P (remove_all x e).
Proof.
  intro H. env induction e; simpl in *; auto.
  destruct (x0 == x); subst; simpl; tauto.
Qed.

remove_all x e produces a smaller environment for leq_env.
Lemma leq_env_remove_all {A} (e: env A) x:
  leq_env (remove_all x e) e.
Proof.
  intros y v Hy. destruct (y == x); subst.
  - rewrite get_remove_all_this in Hy. discriminate.
  - rewrite get_remove_all_other in Hy; auto.
Qed.

leq_env is preserved by remove_all.
Lemma leq_env_remove_all_stable {A} (e e': env A) x:
  leq_env e e' →
  leq_env (remove_all x e) (remove_all x e').
Proof.
  intros H y v Hy. destruct (y == x); subst.
  - rewrite get_remove_all_this in ×. assumption.
  - rewrite get_remove_all_other in *; auto.
Qed.

If there is a binding for x in e, then removing this binding and adding it again produces a larger environment for leq_env.
Lemma leq_env_reorder1 {A} (e: env A) x a:
  get x e = Some a →
  leq_env e (x ¬ a ++ remove_all x e).
Proof.
  intros Hx y b Hy. destruct (y == x); subst.
  - rewrite get_update_this. congruence.
  - rewrite get_update_other; auto. rewrite get_remove_all_other; auto.
Qed.

If there is a binding for x in e, then removing this binding and adding it again produces a smaller environment for leq_env.
Lemma leq_env_reorder2 {A} (e: env A) x a:
  get x e = Some a →
  leq_env (x ¬ a ++ remove_all x e) e.
Proof.
  intros Hx y b Hy. destruct (y == x); subst.
  - rewrite get_update_this in Hy. congruence.
  - rewrite get_update_other in Hy; auto. rewrite get_remove_all_other in Hy; auto.
Qed.

Definition of mapi2 and its basic properties

Auxiliary function map2_aux

Inductive that describes the calling sequence of map2_aux, and is used to prove its termination, in the style of bar-induction.
Inductive map2_calls {A} : env A → Prop :=
| map2_calls_nil:
    map2_calls nil
| map2_calls_cons x v e1:
    map2_calls (remove_all x e1) →
    map2_calls ((x, v) :: e1).

map2_calls is inhabited for every environment.
Lemma map2_calls_init {A} (e: env A) : map2_calls e.
Proof.
  revert e.
  assert (∀ n (e: env A), length e < n → map2_calls e).
  { intro n. induction n; intros e Hlen.
    - abstract (exfalso; lia).
    - destruct e as [| [x v] e].
      + constructor.
      + constructor.
        apply IHn.
        abstract (assert (length (remove_all x e) ≤ length e) by auto using length_remove_all;
                  simpl in Hlen; lia).
  }
  intros e.
  apply (H (S (length e))). abstract lia.
Defined.

Auxiliary lemma for the definition of map2_aux.
Lemma map2_calls_invert_cons {A} e x (v: A) (r: env A) (Hind: map2_calls e) :
  e = (x, v) :: r →
  map2_calls (remove_all x r).
Proof.
  intros Heq. destruct Hind.
  - exfalso. abstract inversion Heq.
  - assert (remove_all x r = remove_all x0 e1) as Heq'.
    { abstract congruence. }
    rewrite Heq'. assumption.
Defined.

If e1 and e2 have the same domains, map2_aux f e1 e2 Hind returns Some e where e is an environment with the same domain as e1 and e2, and that contains the bindings (x, f x v1 v2) whenever get x e1 = Some v1 and get x e2 = Some v2. map2_aux f e1 e2 Hind returns None if the environment do not have the same domains.
Fixpoint mapi2_aux {A B C} (f: atom → A → B → C) (e1: env A) (e2: env B) (Hind: map2_calls e1) { struct Hind } : option (env C) :=
  match e1 as x1 return e1 = x1 → option (env C) with
  | nil ⇒
    fun _ ⇒
      match e2 with
      | nil ⇒ Some nil
      | _ ⇒ None
      end
  | (x, v1) :: r1 ⇒
    fun Heq ⇒
      match get x e2 with
      | Some v2 ⇒
        match mapi2_aux f (remove_all x r1) (remove_all x e2) (map2_calls_invert_cons e1 x v1 r1 Hind Heq) with
        | Some r ⇒ Some ((x, f x v1 v2) :: r)
        | None ⇒ None
        end
      | None ⇒
        None
    end
  end eq_refl.

Unfolding lemma for map2_aux.
Lemma mapi2_aux_equation {A B C} (f: atom → A → B → C) (e1: env A) (e2: env B) (Hind: map2_calls e1):
  mapi2_aux f e1 e2 Hind =
  match e1 as l return e1 = l → option (env C) with
  | nil ⇒
    fun _ ⇒
      match e2 with
      | nil ⇒ Some nil
      | _ ⇒ None
      end
  | (x, v) :: r1 ⇒
    fun Heq ⇒
      match get x e2 with
      | Some v2 ⇒
        match mapi2_aux f (remove_all x r1) (remove_all x e2) (map2_calls_invert_cons e1 x v r1 Hind Heq) with
        | Some r ⇒ Some ((x, f x v v2) :: r)
        | None ⇒ None
        end
      | None ⇒ None
      end
  end eq_refl.
Proof.
  destruct Hind; reflexivity.
Qed.

The result of map2_aux does not depend on its argument of type map2_calls. (Strong version)
Lemma mapi2_aux_proof_irrelevant_strong {A B C} (f: atom → A → B → C) (e e1 e1': env A) (e2: env B)
      (Hind: map2_calls e) (Hind1: map2_calls e1) (Hind1': map2_calls e1'):
  e = e1 →
  e = e1' →
  mapi2_aux f e1 e2 Hind1 = mapi2_aux f e1' e2 Hind1'.
Proof.
  revert e1 e1' Hind1 Hind1' e2.
  induction Hind; intros.
  - destruct Hind1; [| discriminate].
    destruct Hind1'; [| discriminate].
    reflexivity.
  - destruct Hind1; [ discriminate |].
    destruct Hind1'; [ discriminate |].
    inversion H; subst.
    inversion H0; subst.
    simpl.
    rewrite (IHHind (remove_all x1 e3) (remove_all x1 e3)
                    (eq_ind_r (fun e : env A ⇒ map2_calls e) Hind1
                              (map2_calls_invert_cons_subproof0 A x1 v1 e3 x1 v1 e3 eq_refl))
                    (eq_ind_r (fun e : env A ⇒ map2_calls e) Hind1'
                              (map2_calls_invert_cons_subproof0 A x1 v1 e3 x1 v1 e3 eq_refl)));
      reflexivity.
Qed.

The result of map2_aux does not depend on its argument of type map2_calls.
Lemma mapi2_aux_proof_irrelevant {A B C} (f: atom → A → B → C) (e1: env A) (e2: env B)
      (Hind1: map2_calls e1) (Hind2: map2_calls e1):
  mapi2_aux f e1 e2 Hind1 = mapi2_aux f e1 e2 Hind2.
Proof.
  apply (mapi2_aux_proof_irrelevant_strong f e1 e1 e1 e2 Hind1 Hind1 Hind2 eq_refl eq_refl).
Qed.

Induction principle for mapi2_aux. (Strong version)
Lemma mapi2_aux_induction_strong {A B C} (f: atom → A → B → C) (e: env A) (Hind: map2_calls e) :
  ∀ (P: env A → env B → option (env C) → Prop),
    (∀ (e1: env A) (e2: env B) (Hind: map2_calls e1),
        e1 = nil →
        P e1 e2 (mapi2_aux f e1 e2 Hind)) →
    (∀ (e1: env A) (e2: env B) (Hind: map2_calls e1),
        ∀ x v e1' (Heq: e1 = (x, v) :: e1'),
          P (remove_all x e1')
            (remove_all x e2)
            (mapi2_aux f (remove_all x e1') (remove_all x e2) (map2_calls_invert_cons e1 x v e1' Hind Heq)) →
          P e1 e2 (mapi2_aux f e1 e2 Hind)
    ) →
    ∀ (e1: env A) (e2: env B) (Hind: map2_calls e1),
      e = e1 →
      P e1 e2 (mapi2_aux f e1 e2 Hind) .
Proof.
  intro P.
  induction Hind.
  - intros Hnil Hcons e1 e2 Hind Heq. destruct Hind; [| discriminate].
    apply Hnil; auto.
  - intros Hnil Hcons e0 e2 Hind0 Heq. destruct Hind0; [ discriminate |].
    inversion Heq; subst. clear Heq.
    apply Hcons with (Heq := eq_refl).
    apply IHHind; auto.
Qed.

Induction principle for mapi2_aux.
Lemma mapi2_aux_induction {A B C} (f: atom → A → B → C) :
  ∀ (P: env A → env B → option (env C) → Prop)
    (Hnil: ∀ (e1: env A) (e2: env B) (Hind: map2_calls e1),
        e1 = nil →
        P e1 e2 (mapi2_aux f e1 e2 Hind))
    (Hcons: ∀ (e1: env A) (e2: env B) (Hind: map2_calls e1),
        ∀ x v e1' (Heq: e1 = (x, v) :: e1'),
        P (remove_all x e1')
          (remove_all x e2)
          (mapi2_aux f (remove_all x e1') (remove_all x e2) (map2_calls_invert_cons e1 x v e1' Hind Heq)) →
        P e1 e2 (mapi2_aux f e1 e2 Hind)
    ),
    ∀ (e1: env A) (e2: env B) (Hind: map2_calls e1),
      P e1 e2 (mapi2_aux f e1 e2 Hind) .
Proof.
  intros P Hnil Hcons e1 e2 Hind.
  apply mapi2_aux_induction_strong with (e := e1); auto.
Qed.

Environments that have the same bindings have the same domains.
Lemma ext_env_same_dom {A} (e1 e2: env A):
  (∀ x, get x e1 = get x e2) →
  dom e1 [=] dom e2.
Proof.
  intros H x. split; intro Hx.
  - case_eq (get x e2); intros.
    + apply get_in_dom in H0. assumption.
    + exfalso. rewrite <- H in H0. apply get_notin_dom in H0. contradiction.
  - case_eq (get x e1); intros.
    + apply get_in_dom in H0. assumption.
    + exfalso. rewrite H in H0. apply get_notin_dom in H0. contradiction.
Qed.

remove_all preserves extensional equality of environment.
Lemma remove_all_ext_env {A} x (e1 e2: env A):
  (∀ y, get y e1 = get y e2) →
  (∀ y, get y (remove_all x e1) = get y (remove_all x e2)).
Proof.
  intros H y.
  destruct (y == x); subst.
  - repeat rewrite get_remove_all_this. reflexivity.
  - repeat rewrite get_remove_all_other; auto.
Qed.

The mapi2 function and its properties.

If e1 and e2 have the same domains, mapi2 f e1 e2 returns Some e where e is an environment with the same domain as e1 and e2, and that contains the bindings (x, f x v1 v2) whenever get x e1 = Some v1 and get x e2 = Some v2. map2 f e1 e2 returns None if the environment do not have the same domains.
Definition mapi2 {A B C} (f: atom → A → B → C) (e1: env A) (e2: env B) : option (env C) :=
  mapi2_aux f e1 e2 (map2_calls_init e1).

Unfolding lemma for mapi2.
Lemma mapi2_equation {A B C} (f: atom → A → B → C) (e1: env A) (e2: env B):
  mapi2 f e1 e2 =
  match e1 with
  | nil ⇒
    match e2 with
    | nil ⇒ Some nil
    | _ ⇒ None
    end
  | (x, v) :: r1 ⇒
    match get x e2 with
    | Some v2 ⇒
      match mapi2 f (remove_all x r1) (remove_all x e2) with
      | Some r ⇒ Some ((x, f x v v2) :: r)
      | None ⇒ None
      end
    | None ⇒ None
    end
  end.
Proof.
  unfold mapi2.
  rewrite mapi2_aux_equation.
  destruct e1 as [| [x v] e1].
  - reflexivity.
  - rewrite (mapi2_aux_proof_irrelevant f (remove_all x e1) (remove_all x e2)
                                       (map2_calls_invert_cons ((x, v) :: e1) x v e1 (map2_calls_init ((x, v) :: e1)) eq_refl)
                                       (map2_calls_init (remove_all x e1))).
    reflexivity.
Qed.

Induction principle for mapi2.
Lemma mapi2_induction {A B C} (f: atom → A → B → C) :
  ∀ (P: env A → env B → option (env C) → Prop)
    (Hnil: ∀ (e2: env B),
        P nil e2 (mapi2 f nil e2))
    (Hcons: ∀ x v (e1: env A) (e2: env B),
        P (remove_all x e1)
          (remove_all x e2)
          (mapi2 f (remove_all x e1) (remove_all x e2)) →
        P ((x, v) :: e1) e2 (mapi2 f ((x, v) :: e1) e2)
    ),
    ∀ (e1: env A) (e2: env B),
      P e1 e2 (mapi2 f e1 e2) .
Proof.
  intros P Hnil Hcons e1 e2.
  unfold mapi2. apply mapi2_aux_induction.
  - intros e1' e3' Hind Heq. subst e1'.
    rewrite (mapi2_aux_proof_irrelevant _ _ _ Hind map2_calls_nil).
    apply Hnil.
  - intros e1' e2' Hind x v e1'' Heq H. subst e1'.
    rewrite (mapi2_aux_proof_irrelevant _ _ _ (map2_calls_invert_cons ((x, v) :: e1'') x v e1'' Hind eq_refl) (map2_calls_init (remove_all x e1''))) in H.
    apply Hcons with (v := v) in H.
    rewrite (mapi2_aux_proof_irrelevant _ _ _ Hind (map2_calls_init ((x, v) :: e1''))).
    assumption.
Qed.

get x (mapi2 f e1 e2) = Some (f x e1 e2) whenever get x e1 = Some v1 and get x e2 = Some v2.
Lemma mapi2_get {A B C} (f: atom → A → B → C) (e1: env A) (e2: env B) (e3: env C) x v1 v2 v3:
  mapi2 f e1 e2 = Some e3 →
  get x e1 = Some v1 →
  get x e2 = Some v2 →
  get x e3 = Some v3 →
  v3 = f x v1 v2.
Proof.
  revert e3 v1 v2 v3.
  pattern e1, e2, (mapi2 f e1 e2).
  apply mapi2_induction; clear e1 e2.
  - intros e2 e3 v1 v2 v3 Heq H1 H2 H3.
    simpl in H1. discriminate.
  - intros y v e1 e2 Hind e3 v1 v2 v3 Heq H1 H2 H3.
    rewrite mapi2_equation in Heq.
    case_eq (get y e2); intros; rewrite H in Heq; try discriminate.
    case_eq (mapi2 f (remove_all y e1) (remove_all y e2));
      intros; rewrite H0 in Heq; try discriminate.
    inversion Heq; subst. clear Heq.
    simpl in H1, H3. destruct (x == y); subst.
    + congruence.
    + rewrite <- (get_remove_all_other x y) in H1; auto.
      rewrite <- (get_remove_all_other x y) in H2; auto.
      eapply Hind; eauto.
Qed.

mapi2 f e1 e2 has the same domain as e1.
Lemma mapi2_dom1 {A B C} (f: atom → A → B → C) (e1: env A) (e2: env B) (e3: env C):
  mapi2 f e1 e2 = Some e3 →
  dom e1 [=] dom e3.
Proof.
  revert e3.
  pattern e1, e2, (mapi2 f e1 e2). apply mapi2_induction; clear e1 e2.
  - intros e2 e3 Heq. rewrite mapi2_equation in Heq.
    destruct e2; inversion Heq; subst. reflexivity.
  - intros x v e1 e2 Hind e3 Heq. rewrite mapi2_equation in Heq.
    destruct (get x e2); [| discriminate ].
    destruct (mapi2 f (remove_all x e1) (remove_all x e2)); [| discriminate ].
    inversion Heq; subst. clear Heq.
    simpl. rewrite <- Hind; auto.
    rewrite dom_remove_all. fsetdec.
Qed.

mapi2 f e1 e2 has the same domain as e2.
Lemma mapi2_dom2 {A B C} (f: atom → A → B → C) (e1: env A) (e2: env B) (e3: env C):
  mapi2 f e1 e2 = Some e3 →
  dom e2 [=] dom e3.
Proof.
  revert e3.
  pattern e1, e2, (mapi2 f e1 e2). apply mapi2_induction; clear e1 e2.
  - intros e2 e3 Heq. rewrite mapi2_equation in Heq.
    destruct e2; inversion Heq; subst. reflexivity.
  - intros x v e1 e2 Hind e3 Heq. rewrite mapi2_equation in Heq.
    case_eq (get x e2); intros; rewrite H in Heq; [| discriminate ].
    destruct (mapi2 f (remove_all x e1) (remove_all x e2)); [| discriminate ].
    inversion Heq; subst. clear Heq.
    simpl. rewrite <- Hind; auto.
    rewrite dom_remove_all. apply get_in_dom in H.
    fsetdec.
Qed.

mapi2 f e1 e2 succeeds iff e1 and e2 have the same domain.
Lemma mapi2_not_None_iff {A B C} (f: atom → A → B → C) (e1: env A) (e2: env B):
  mapi2 f e1 e2 ≠ None ↔ dom e1 [=] dom e2.
Proof.
  pattern e1, e2, (mapi2 f e1 e2). apply mapi2_induction; clear e1 e2.
  - intros e2. rewrite mapi2_equation. destruct e2 as [| [x v] e2]; simpl.
    + split; intro; [ reflexivity | congruence ].
    + split; intro.
      × congruence.
      × exfalso.
        assert (x `in` empty).
        { apply (H x). fsetdec. }
        fsetdec.
  - intros x v e1 e2 Hind. rewrite mapi2_equation.
    case_eq (get x e2); intros.
    + case_eq (mapi2 f (remove_all x e1) (remove_all x e2)); intros.
      × split; intro; [| congruence].
        assert (dom (remove_all x e1) [=] dom (remove_all x e2)) as Hdom.
        { transitivity (dom e).
          - eapply mapi2_dom1; eauto.
          - symmetry. eapply mapi2_dom2; eauto.
        }
        repeat rewrite dom_remove_all in Hdom.
        simpl. apply get_in_dom in H.
        fsetdec.
      × split; intro; [congruence |].
        intros _. revert H0. apply Hind.
        repeat rewrite dom_remove_all.
        apply get_in_dom in H. simpl in H1.
        fsetdec.
    + split; intro; [ congruence |].
      exfalso. simpl in H0. apply get_notin_dom in H. fsetdec.
Qed.

mapi2 produces an environment with no duplicates.
Lemma mapi2_uniq {A B C} (f: atom → A → B → C) (e1: env A) (e2: env B) (e3: env C):
  mapi2 f e1 e2 = Some e3 →
  uniq e3.
Proof.
  revert e3. pattern e1, e2, (mapi2 f e1 e2). apply mapi2_induction; clear e1 e2; intros.
  - rewrite mapi2_equation in H. destruct e2; inversion H; subst. auto.
  - rewrite mapi2_equation in H0.
    case_eq (get x e2); intros; rewrite H1 in H0; try discriminate.
    case_eq (mapi2 f (remove_all x e1) (remove_all x e2)); intros;
      rewrite H2 in H0; inversion H0; subst; clear H0.
    constructor; [ solve [eauto] |].
    apply mapi2_dom1 in H2. rewrite dom_remove_all in H2. fsetdec.
Qed.

mapi2 commutes with remove_all in case of success.
Lemma mapi2_remove_all_Some {A B C} x (f: atom → A → B → C) (e1: env A) (e2: env B) (e3: env C) :
  mapi2 f e1 e2 = Some e3 →
  mapi2 f (remove_all x e1) (remove_all x e2) = Some (remove_all x e3).
Proof.
  revert e3.
  pattern e1, e2, (mapi2 f e1 e2). apply mapi2_induction; clear e1 e2; intros.
  - simpl. rewrite mapi2_equation in ×.
    destruct e2; inversion H; subst; reflexivity.
  - rewrite mapi2_equation in H0.
    case_eq (get x0 e2); intros; rewrite H1 in H0; try discriminate.
    case_eq (mapi2 f (remove_all x0 e1) (remove_all x0 e2)); intros;
      rewrite H2 in H0; inversion H0; subst; clear H0.
    simpl. destruct (x0 == x); subst.
    + apply H in H2. repeat rewrite remove_all_projection in H2. assumption.
    + rewrite mapi2_equation. rewrite get_remove_all_other; auto. rewrite H1.
      apply H in H2.
      repeat rewrite (remove_all_swap x x0) in H2.
      rewrite H2.
      reflexivity.
Qed.

mapi2 commutes with remove_all in case of failure.
Lemma mapi2_remove_all_None {A B C} x (f: atom → A → B → C) (e1: env A) (e2: env B) :
  mapi2 f (remove_all x e1) (remove_all x e2) = None →
  mapi2 f e1 e2 = None.
Proof.
  intro H.
  case_eq (mapi2 f e1 e2); intros; auto.
  assert (dom e1 [=] dom e2) as Hdom.
  { transitivity (dom e); [| symmetry]; eauto using mapi2_dom1, mapi2_dom2. }
  exfalso. revert H.
  { apply mapi2_not_None_iff. repeat rewrite dom_remove_all. fsetdec. }
Qed.

mapi2 preserves extensional equality on environments.
Lemma mapi2_ext_Some {A B C} (f f': atom → A → B → C) (e1 e1': env A) (e2 e2': env B)
      (e3 e3': env C):
  (∀ x a b, f x a b = f' x a b) →
  (∀ x, get x e1 = get x e1') →
  (∀ x, get x e2 = get x e2') →
  mapi2 f e1 e2 = Some e3 →
  mapi2 f' e1' e2' = Some e3' →
  (∀ x, get x e3 = get x e3').
Proof.
  intro Hf.
  revert e1' e2' e3 e3'.
  pattern e1, e2, (mapi2 f e1 e2). apply mapi2_induction; clear e1 e2; intros.
  - rewrite mapi2_equation in H1.
    destruct e1' as [| [y vy] e1'].
    + rewrite mapi2_equation in H2.
      destruct e2 as [| [y2 v2] e2]; destruct e2' as [| [y2' v2'] e2']; congruence.
    + exfalso. specialize (H y). simpl in H. destruct (y == y) in H; congruence.
  - rewrite mapi2_equation in H2.
    case_eq (get x e2); intros; rewrite H4 in H2; try discriminate.
    case_eq (mapi2 f (remove_all x e1) (remove_all x e2)); intros; rewrite H5 in H2; inversion H2; subst; clear H2.
    simpl. destruct (x0 == x); subst.
    + assert (get x e1' = Some v) as Hx1.
      { specialize (H0 x). simpl in H0. destruct (x == x); congruence. }
      assert (get x e2' = Some b) as Hx2.
      { rewrite H1 in H4. assumption. }
      case_eq (get x e3'); intros.
      × assert (c = f' x v b) by eauto using mapi2_get.
        rewrite Hf. congruence.
      × exfalso. apply get_in_dom in Hx1. apply get_notin_dom in H2.
        apply mapi2_dom1 in H3. fsetdec.
    + apply (mapi2_remove_all_Some x) in H3.
      rewrite (H (remove_all x e1') (remove_all x e2') e (remove_all x e3')); auto.
      × rewrite get_remove_all_other; auto.
      × { intros y. specialize (H0 y). simpl in H0. destruct (y == x); subst.
          - repeat rewrite get_remove_all_this. reflexivity.
          - repeat rewrite get_remove_all_other; auto.
        }
      × auto using remove_all_ext_env.
Qed.

If P (f x v1 v2) holds for every binding (x, v1) in e1 and (x, v2) in e2, then all_env P holds on mapi2 f e1 e2.
Lemma mapi2_all_env {A B C} (P: C → Prop) (f: atom → A → B → C) (e1: env A) (e2: env B) (e3: env C):
  (∀ x v1 v2,
      get x e1 = Some v1 →
      get x e2 = Some v2 →
      P (f x v1 v2)
  ) →
  mapi2 f e1 e2 = Some e3 →
  all_env P e3.
Proof.
  revert e3.
  pattern e1, e2, (mapi2 f e1 e2). apply mapi2_induction; clear e1 e2; intros.
  - rewrite mapi2_equation in H0. destruct e2; inversion H0; subst.
    simpl. trivial.
  - rewrite mapi2_equation in H1.
    case_eq (get x e2); intros; rewrite H2 in H1; try discriminate.
    case_eq (mapi2 f (remove_all x e1) (remove_all x e2)); intros; rewrite H3 in H1;
      inversion H1; subst; clear H1.
    split.
    + apply (H0 x); auto.
      simpl. destruct (x == x); congruence.
    + apply H; auto.
      intros y v1 v2 Hy1 Hy2.
      specialize (H0 y v1 v2). simpl in H0.
      destruct (y == x); subst.
      × exfalso. rewrite get_remove_all_this in Hy1. discriminate.
      × rewrite get_remove_all_other in Hy1; auto.
        rewrite get_remove_all_other in Hy2; auto.
Qed.

Definition of map2 and its basic properties

If e1 and e2 have the same domains, map2 f e1 e2 returns Some e where e is an environment with the same domain as e1 and e2, and that contains the bindings (x, f v1 v2) whenever get x e1 = Some v1 and get x e2 = Some v2. map2 f e1 e2 returns None if the environment do not have the same domains.
Definition map2 {A B C} (f: A → B → C) (e1: env A) (e2: env B) : option (env C) :=
  mapi2 (fun _ ⇒ f) e1 e2.

Unfolding lemma for map2.
Lemma map2_equation {A B C} (f: A → B → C) (e1: env A) (e2: env B):
  map2 f e1 e2 =
  match e1 with
  | nil ⇒
    match e2 with
    | nil ⇒ Some nil
    | _ ⇒ None
    end
  | (x, v) :: r1 ⇒
    match get x e2 with
    | Some v2 ⇒
      match map2 f (remove_all x r1) (remove_all x e2) with
      | Some r ⇒ Some ((x, f v v2) :: r)
      | None ⇒ None
      end
    | None ⇒ None
    end
  end.
Proof.
  unfold map2. apply mapi2_equation.
Qed.

Induction principle for map2.
Lemma map2_induction {A B C} (f: A → B → C) :
  ∀ (P: env A → env B → option (env C) → Prop)
    (Hnil: ∀ (e2: env B),
        P nil e2 (map2 f nil e2))
    (Hcons: ∀ x v (e1: env A) (e2: env B),
        P (remove_all x e1)
          (remove_all x e2)
          (map2 f (remove_all x e1) (remove_all x e2)) →
        P ((x, v) :: e1) e2 (map2 f ((x, v) :: e1) e2)
    ),
    ∀ (e1: env A) (e2: env B),
      P e1 e2 (map2 f e1 e2) .
Proof.
  unfold map2. apply mapi2_induction.
Qed.

get x (map2 f e1 e2) = Some (f x e1 e2) whenever get x e1 = Some v1 and get x e2 = Some v2.
Lemma map2_get {A B C} (f: A → B → C) (e1: env A) (e2: env B) (e3: env C) x v1 v2 v3:
  map2 f e1 e2 = Some e3 →
  get x e1 = Some v1 →
  get x e2 = Some v2 →
  get x e3 = Some v3 →
  v3 = f v1 v2.
Proof.
  unfold map2. apply mapi2_get.
Qed.

map2 f e1 e2 has the same domain as e1.
Lemma map2_dom1 {A B C} (f: A → B → C) (e1: env A) (e2: env B) (e3: env C):
  map2 f e1 e2 = Some e3 →
  dom e1 [=] dom e3.
Proof.
  unfold map2. apply mapi2_dom1.
Qed.

map2 f e1 e2 has the same domain as e2.
Lemma map2_dom2 {A B C} (f: A → B → C) (e1: env A) (e2: env B) (e3: env C):
  map2 f e1 e2 = Some e3 →
  dom e2 [=] dom e3.
Proof.
  unfold map2. apply mapi2_dom2.
Qed.

map2 f e1 e2 succeeds iff e1 and e2 have the same domain.
Lemma map2_not_None_iff {A B C} (f: A → B → C) (e1: env A) (e2: env B):
  map2 f e1 e2 ≠ None ↔ dom e1 [=] dom e2.
Proof.
  unfold map2. apply mapi2_not_None_iff.
Qed.

map2 produces an environment with no duplicates.
Lemma map2_uniq {A B C} (f: A → B → C) (e1: env A) (e2: env B) (e3: env C):
  map2 f e1 e2 = Some e3 →
  uniq e3.
Proof.
  unfold map2. apply mapi2_uniq.
Qed.

map2 commutes with remove_all in case of success.
Lemma map2_remove_all_Some {A B C} x (f: A → B → C) (e1: env A) (e2: env B) (e3: env C) :
  map2 f e1 e2 = Some e3 →
  map2 f (remove_all x e1) (remove_all x e2) = Some (remove_all x e3).
Proof.
  unfold map2. apply mapi2_remove_all_Some.
Qed.

map2 commutes with remove_all in case of failure.
Lemma map2_remove_all_None {A B C} x (f: A → B → C) (e1: env A) (e2: env B) :
  map2 f (remove_all x e1) (remove_all x e2) = None →
  map2 f e1 e2 = None.
Proof.
  unfold map2. apply mapi2_remove_all_None.
Qed.

map2 preserves extensional equality on environments.
Lemma map2_ext_Some {A B C} (f f': A → B → C) (e1 e1': env A) (e2 e2': env B)
      (e3 e3': env C):
  (∀ a b, f a b = f' a b) →
  (∀ x, get x e1 = get x e1') →
  (∀ x, get x e2 = get x e2') →
  map2 f e1 e2 = Some e3 →
  map2 f' e1' e2' = Some e3' →
  (∀ x, get x e3 = get x e3').
Proof.
  unfold map2. intros.
  eapply mapi2_ext_Some with (f0 := fun _ ⇒ f) (f'0 := fun _ ⇒ f'); eauto.
Qed.

If P (f v1 v2) holds for every binding (x, v1) in e1 and (x, v2) in e2, then all_env P holds on map2 f e1 e2.
Lemma map2_all_env {A B C} (P: C → Prop) (f: A → B → C) (e1: env A) (e2: env B) (e3: env C):
  (∀ x v1 v2,
      get x e1 = Some v1 →
      get x e2 = Some v2 →
      P (f v1 v2)
  ) →
  map2 f e1 e2 = Some e3 →
  all_env P e3.
Proof.
  unfold map2. apply mapi2_all_env.
Qed.

Definition of fold_env_dom and its basic properties

fold_env_dom f e acc folds over the environment e using a fold function that also takes as argument the set of bindings that remains to be visited.
Definition fold_env_dom {A B} (f: atom → A → atoms → B → B) (E: env A) (acc: B) : B × atoms :=
  fold_right
    (fun p acc ⇒
       match acc with
       | (b, s) ⇒
         match p with
         | (x, a) ⇒
           (f x a s b,
            add x s)
         end
       end
    )
    (acc, empty)
    E.

The second result of fold_env_dom f e acc is the domain of e.
Lemma fold_env_dom_snd {A B} (f: atom → A → atoms → B → B) (E: env A) (acc: B) :
  snd (fold_env_dom f E acc) [=] dom E.
Proof.
  env induction E.
  - reflexivity.
  - simpl. case_eq (fold_env_dom f xs acc); intros.
    rewrite H in IHE. simpl in ×. fsetdec.
Qed.

Definition of map_env_dom and its basic properties

map_env_dom f e performs a map on the environment e with a function that takes as argument the domain of the environment that goes after the current binding.
Definition map_env_dom {A B} (f: atom → A → atoms → B) (E: env A) : env B :=
  fst (fold_env_dom (fun x a s acc ⇒ (x, f x a s) :: acc) E nil).

If e = e2 ++ [(x, a)] ++ e1 where x is not bound by e2, then map_env_dom f e contains maps the variable x to a value that is equal to f x a (dom e1).
Lemma map_env_dom_spec {A B} (f: atom → A → atoms → B) (E1: env A) x (a: A) (E2: env A) (b: B) (equal: B → B → Prop):
  (∀ x a S1 S2, S1 [=] S2 → equal (f x a S1) (f x a S2)) →
  x `notin` dom E2 →
  get x (map_env_dom f (E2 ++ [(x, a)] ++ E1)) = Some b →
  equal b (f x a (dom E1)).
Proof.
  intro Hequiv.
  remember (E2 ++ [(x, a)] ++ E1) as E.
  generalize dependent E2.
  generalize dependent a.
  generalize dependent x.
  generalize dependent E1.
  generalize dependent b.
  env induction E; intros.
  - exfalso. simpl in H0. discriminate.
  - destruct E2 as [| [y c] E2].
    + simpl in HeqE. inversion HeqE; subst; clear HeqE.
      simpl in H0. unfold map_env_dom in H0. simpl in H0.
      case_eq (fold_env_dom
                 (fun (x : atom) (a : A) (s : atoms) (acc : list (atom × B)) ⇒
                    (x, f x a s) :: acc) E1 nil); intros.
      rewrite H1 in H0. simpl in H0.
      destruct (x0 == x0); [| contradiction ].
      inversion H0; subst; clear H0.
      assert (t [=] dom E1) as Hdom.
      { pose proof (fold_env_dom_snd
                      (fun (x : atom) (a : A) (s : atoms) (acc : list (atom × B)) ⇒
                         (x, f x a s) :: acc) E1 nil) as Hdom.
        rewrite H1 in Hdom. assumption.
      }
      apply Hequiv. assumption.
    + simpl in HeqE. inversion HeqE; subst. clear HeqE.
      assert (x0 ≠ y) as Hneq by auto.
      unfold map_env_dom in H0. simpl in H0.
      case_eq (fold_env_dom
                 (fun (x : atom) (a : A) (s : atoms) (acc : list (atom × B)) ⇒
                    (x, f x a s) :: acc) (E2 ++ (x0, a0) :: E1) nil); intros.
      rewrite H1 in H0.
      simpl in H0. destruct (x0 == y); [ contradiction |].
      apply (IHE b E1 x0 a0 E2).
      × reflexivity.
      × auto.
      × unfold map_env_dom. rewrite H1. assumption.
Qed.

map_env_dom preserves the domain of environments.
Lemma map_env_dom_dom {A B} (f: atom → A → atoms → B) (E: env A):
  dom (map_env_dom f E) [=] dom E.
Proof.
  env induction E.
  - reflexivity.
  - unfold map_env_dom in ×. simpl.
    case_eq (fold_env_dom
               (fun (x0 : atom) (a0 : A) (s : atoms) (acc : list (atom × B)) ⇒
                  (x0, f x0 a0 s) :: acc) xs nil); intros.
    rewrite H in IHE. simpl in IHE. simpl. fsetdec.
Qed.

map_env_dom preserves and reflects the uniqueness of bindings.
Lemma map_env_dom_uniq {A B} (f: atom → A → atoms → B) (E: env A):
  uniq E ↔ uniq (map_env_dom f E).
Proof.
  env induction E.
  - unfold map_env_dom. simpl.
    split; intro; constructor.
  - pose proof (map_env_dom_dom f xs) as Hdom.
    unfold map_env_dom in ×. simpl.
    case_eq (fold_env_dom
               (fun (x0 : atom) (a0 : A) (s : atoms) (acc : list (atom × B)) ⇒
                  (x0, f x0 a0 s) :: acc) xs nil); intros.
    rewrite H in IHE. simpl in IHE.
    rewrite H in Hdom. simpl in Hdom.
    simpl.
    split; intro Huniq; inversion Huniq; subst; constructor; auto.
    + solve_uniq.
    + fsetdec.
    + solve_uniq.
    + fsetdec.
Qed.

Definition of forall_env_dom and its basic properties

forall_env_dom P e checks that every binding in e satisfies P, for a function P that takes as argument the domain of the environment that goes after the current binding.
Definition forall_env_dom {A} (f: atom → A → atoms → Prop) (E: env A) : Prop :=
  fst (fold_env_dom (fun x a s acc ⇒ f x a s ∧ acc) E True).

forall_env_dom P ((x, a) :: e) is equivalent to P x a (dom e) ∧ forall_env_dom P e.
Lemma forall_env_dom_cons {A} (f: atom → A → atoms → Prop) x (a: A) (E: env A) :
  (∀ x a S1 S2, S1 [=] S2 → f x a S1 → f x a S2) →
  forall_env_dom f ((x, a) :: E) ↔
  (f x a (dom E) ∧ forall_env_dom f E).
Proof.
  intro Hmorphism.
  unfold forall_env_dom. simpl.
  case_eq (fold_env_dom
             (fun (x0 : atom) (a0 : A) (s : atoms) (acc : Prop) ⇒ f x0 a0 s ∧ acc) E True); intros.
  simpl.
  assert (t [=] dom E).
  { pose proof (fold_env_dom_snd (fun (x0 : atom) (a0 : A) (s : atoms) (acc : Prop) ⇒ f x0 a0 s ∧ acc) E True) as Heq.
    rewrite H in Heq. assumption.
  }
  split; intros [Hf Hp]; (split; [| assumption]).
  - eapply Hmorphism; eauto.
  - eapply Hmorphism; eauto. symmetry. assumption.
Qed.

If forall_env_dom P (e2 ++ [(x, a)] ++ e1) holds and x is not bound by e2, then P x a (dom e1) holds.
Lemma forall_env_dom_spec {A} (f: atom → A → atoms → Prop) (E1: env A) x (a: A) (E2: env A):
  (∀ x a S1 S2, S1 [=] S2 → f x a S1 → f x a S2) →
  x `notin` dom E2 →
  forall_env_dom f (E2 ++ [(x, a)] ++ E1) →
  f x a (dom E1).
Proof.
  intro Hmorphism.
  remember (E2 ++ [(x, a)] ++ E1) as E.
  generalize dependent E2.
  generalize dependent a.
  generalize dependent x.
  generalize dependent E1.
  env induction E; intros.
  - exfalso. destruct E2; simpl in HeqE; discriminate.
  - destruct E2 as [| [y c] E2].
    + simpl in HeqE. inversion HeqE; subst; clear HeqE.
      simpl in H0. unfold forall_env_dom in H0. simpl in H0.
      case_eq (fold_env_dom
                 (fun (x : atom) (a : A) (s : atoms) (acc : Prop) ⇒ f x a s ∧ acc) E1 True); intros.
      rewrite H1 in H0. simpl in H0. destruct H0 as [Hf HP].
      assert (t [=] dom E1) as Hdom.
      { pose proof (fold_env_dom_snd
                      (fun (x : atom) (a : A) (s : atoms) (acc : Prop) ⇒ f x a s ∧ acc) E1 True) as Hdom.
        rewrite H1 in Hdom. assumption.
      }
      eapply Hmorphism; eassumption.
    + simpl in HeqE. inversion HeqE; subst. clear HeqE.
      assert (x0 ≠ y) as Hneq by auto.
      unfold forall_env_dom in H0. simpl in H0.
      case_eq (fold_env_dom
                 (fun (x : atom) (a : A) (s : atoms) (acc : Prop) ⇒ f x a s ∧ acc)
                 (E2 ++ (x0, a0) :: E1) True); intros.
      rewrite H1 in H0.
      simpl in H0. destruct H0 as [Hf HP].
      apply (IHE E1 x0 a0 E2).
      × reflexivity.
      × auto.
      × unfold forall_env_dom. rewrite H1. assumption.
Qed.

env_of_atoms

env_of_atoms f S builds an environment e with domain S such that get x e = Some (f x)
Definition env_of_atoms {A:Type} (f: atom → A) S : env A :=
  AtomSetImpl.fold (fun x e ⇒ (x ¬ f x) ++ e) S nil.

env_of_atoms builds an environment with no duplicate binding.
Lemma env_of_atoms_uniq {A} (f: atom → A) S :
  uniq (env_of_atoms f S).
Proof.
  revert S.
  assert (∀ l,
             NoDupA Atom.eq l →
             ∀ acc,
               uniq acc →
               (∀ x, x `in` dom acc → ¬ InA Atom.eq x l) →
               uniq
                 (fold_left (fun (a : list (atom × A)) (e : atom) ⇒ [(e, f e)] ++ a) l acc)).
  { intros l Hnodup. induction l; intros acc Huniq Hdisj; simpl; auto.
    apply IHl.
    - inversion Hnodup; subst. assumption.
    - constructor; auto.
      intro Hin. apply (Hdisj a); auto. constructor. reflexivity.
    - intros x Hx Hin. simpl in Hx.
      inversion Hnodup; subst.
      simpl in H1.
      assert (x `in` dom acc ∨ x `notin` dom acc) as [H|H] by fsetdec.
      + apply (Hdisj x); auto.
      + assert (x = a) by fsetdec; subst. auto.
  }
  intro S.
  unfold env_of_atoms.
  rewrite AtomSetImpl.fold_1.
  apply H; auto using AtomSetImpl.elements_3w.
  intros x Hx _. simpl in Hx. fsetdec.
Qed.

Auxiliary lemma about fold_right and add.
Lemma fold_right_add l a acc:
  fold_right add (add a acc) l [=] add a (fold_right add acc l).
Proof.
  induction l; simpl.
  - reflexivity.
  - rewrite IHl. clear IHl. fsetdec.
Qed.

Another auxiliary lemma about fold_left, fold_right and add.
Lemma fold_left_right_add_strong l acc1 acc2:
  acc1 [=] acc2 →
  fold_left (fun s x ⇒ add x s) l acc1 [=] fold_right add acc2 l.
Proof.
  revert acc1 acc2. induction l; intros acc1 acc2 Heq; simpl; auto.
  rewrite (IHl (add a acc1) (add a acc2)).
  - apply fold_right_add.
  - rewrite Heq. reflexivity.
Qed.

Auxiliary lemma about fold_left, fold_right and add.
Lemma fold_left_right_add l acc:
  fold_left (fun s x ⇒ add x s) l acc [=] fold_right add acc l.
Proof.
  apply fold_left_right_add_strong. reflexivity.
Qed.

The domain of env_of_atoms f S is S.
Definition env_of_atoms_dom {A:Type} (f: atom → A) S :
  dom (env_of_atoms f S) [=] S.
Proof.
  revert S.
  assert (∀ l acc,
             dom
               (fold_left (fun (a : list (atom × A)) (e : atom) ⇒ [(e, f e)] ++ a) l acc)
               [=] fold_right add empty l `union` dom acc).
  { intro l. induction l; intro acc; simpl.
    - fsetdec.
    - rewrite IHl. simpl. fsetdec.
  }
  intros S.
  unfold env_of_atoms.
  rewrite AtomSetImpl.fold_1.
  rewrite H.
  rewrite <- fold_left_right_add.
  rewrite <- AtomSetImpl.fold_1.
  rewrite AtomSetProperties.fold_identity.
  fsetdec.
Qed.

Auxiliary lemma between InA, get and fold_left.
Lemma get_fold_left_fresh {A:Type} (f: atom → A) l x acc :
  ¬ InA Atom.eq x l →
  get x (fold_left (fun (a : list (atom × A)) (y : atom) ⇒ (y, f y) :: a) l acc)
  = get x acc.
Proof.
  revert acc. induction l; intros acc Hx; simpl.
  - reflexivity.
  - rewrite IHl; auto.
    simpl. destruct (x == a); subst; auto.
    exfalso. apply Hx. clear Hx. constructor. reflexivity.
Qed.

If there is a binding for x in env_of_atoms f S, then its value is f x.
Lemma env_of_atoms_get_inv {A:Type} (f: atom → A) S x v :
  get x (env_of_atoms f S) = Some v →
  v = f x.
Proof.
  revert S.
  assert (∀ l acc,
             x `notin` dom acc →
             NoDupA Atom.eq l →
             get x
                 (fold_left (fun (a : list (atom × A)) (y : atom) ⇒ [(y, f y)] ++ a) l acc) = Some v →
             v = f x
         ).
  { intro l. induction l; intros acc Hx Hdup Hget; simpl in ×.
    - exfalso. apply get_in_dom in Hget. contradiction.
    - destruct (x == a); subst.
      + rewrite get_fold_left_fresh in Hget.
        × simpl in Hget. destruct (a == a); congruence.
        × inversion Hdup; subst. assumption.
      + apply (IHl ((a, f a) :: acc)); auto.
        inversion Hdup; subst. assumption.
  }
  intros S.
  unfold env_of_atoms.
  rewrite AtomSetImpl.fold_1.
  apply H; auto using AtomSetImpl.elements_3w.
Qed.

There is no binding for x in env_of_atoms f S iff x does not belong to S.
Lemma env_of_atoms_get_None {A:Type} (f: atom → A) S x :
  x `notin` S ↔ get x (env_of_atoms f S) = None.
Proof.
  rewrite get_notin_dom. rewrite env_of_atoms_dom. reflexivity.
Qed.

If x belongs to S, then get x (env_of_atoms f S) = Some (f x).
Lemma env_of_atoms_get {A:Type} (f: atom → A) S x :
  x `in` S →
  get x (env_of_atoms f S) = Some (f x).
Proof.
  intro H.
  case_eq (get x (env_of_atoms f S)); intros.
  - apply env_of_atoms_get_inv in H0. congruence.
  - exfalso. rewrite <- env_of_atoms_get_None in H0. contradiction.
Qed.