Library Generic_Env_List

Require Import Utf8.
Set Implicit Arguments.

Module of an implementation of environments with lists

Require Import Generic_Var.

Module Generic_Env_List_Def (Var : Generic_Var).

Require Import List Bool.

Lemma list_length_S : forall A (l : list A) n,
  length l = S n -> exists x, exists l', l = x :: l'.
Proof.
  induction l as [ | a ]; intros n Hlen; simpl in *; inversion Hlen;
    exists a; exists l; auto.
Qed.

Require Sets.Image.

Import Var.

Definitions

Definition gen_env A := list (TVar * A).

Section Core_Definitions.

Variable A B : Type.
Implicit Types x y : TVar.
Implicit Types xs ys : list TVar.
Implicit Types v w : A.
Implicit Types vs ws : list A.
Implicit Types E F G : gen_env A.
Implicit Types f g : A -> B.

Definition eq_keys_dec := Var.eq_var_dec.

Preliminary properties of eq_keys_dec.

Lemma eq_keys_true : forall A x (a b : A),
  (if eq_keys_dec x x then a else b) = a.
Proof. intros. case (eq_keys_dec x x); congruence. Qed.

Lemma eq_keys_false : forall A x y (a b : A),
  x <> y -> (if eq_keys_dec x y then a else b) = b.
Proof. intros. case (eq_keys_dec x y); congruence. Qed.

Definition empty : gen_env A := nil.

Definition single x v := (x, v) :: nil.

Fixpoint singles xs vs : gen_env A :=
  match xs, vs with
    | x :: xs, v :: vs => (x, v) :: (singles xs vs)
    | _, _ => nil
  end
.

Definition concat E F := F ++ E.

Fixpoint get x E : option A :=
  match E with
    | nil => None
    | (y, v) :: E' => if eq_keys_dec x y then Some v else get x E'
  end
.

Fixpoint dom E : list TVar :=
  match E with
    | nil => nil
    | (x, _) :: E' => x :: (dom E')
  end
.

Fixpoint img E : list A :=
  match E with
    | nil => nil
    | (_, v) :: E' => v :: (img E')
  end
.

Definition belongs x E :=
  List.In x (dom E).

Definition all_belongs xs E :=
  forall x, List.In x xs -> belongs x E.

Definition notin x E :=
  ~ belongs x E.

Definition all_notin xs E :=
  forall x, List.In x xs -> notin x E.

Fixpoint map f E : gen_env B :=
  match E with
    | nil => nil
    | (x, v) :: E' => (x, f v) :: map f E'
  end
.

Fixpoint update_one E x v : gen_env A :=
  match E with
    | nil => nil
    | (y, v') :: E' =>
      if eq_keys_dec x y then (y, v) :: E'
        else (y, v') :: (update_one E' x v)
  end
.

Fixpoint update E F : gen_env A :=
  match F with
    | nil => E
    | (x, v) :: F' => update_one (update E F') x v
  end
.

Fixpoint remove x E : gen_env A :=
  match E with
    | nil => nil
    | (y, v) :: E => if eq_keys_dec x y then E else (y, v) :: (remove x E)
  end
.

Fixpoint all_remove xs E : gen_env A :=
  match xs with
    | nil => E
    | x :: xs => all_remove xs (remove x E)
  end
.

End Core_Definitions.

x ∶ v is the notation for a singleton environment mapping x to v.

Notation "x '∶' v" := (single x v)
(at level 63) : gen_env_scope.

xs ∷ vs is the notation for an environment mapping xs to vs.

Notation "xs '∷' vs" := (singles xs vs)
(at level 63) : gen_env_scope.

E & F is the notation for concatenation of E and F.

Notation "E '&' F" := (concat E F)
(at level 65, left associativity) : gen_env_scope.

E ∖ { x } is the notation for removing x from E.

Notation "E '∖' '{' x '}'" := (remove x E)
(at level 64, left associativity) : gen_env_scope.

E ∖ xs is the notation for removing xs from E.

Notation "E '∖' xs" := (all_remove xs E)
(at level 64, left associativity) : gen_env_scope.

E ::= F is the notation for updating of E with F.

Notation "E '::=' F" := (update E F)
(at level 65, left associativity) : gen_env_scope.

x ∈ E to be read x is bound in E.

Notation "x '∈' E" := (belongs x E)
(at level 67) : gen_env_scope.

xs ⊂ E to be read xs are bound in E.

Notation "xs '⊂' E" := (all_belongs xs E)
(at level 67) : gen_env_scope.

x '∉' E to be read x is unbound in E.

Notation "x '∉' E" := (notin x E)
(at level 67) : gen_env_scope.

xs '⊄' E to be read xs are unbound in E.

Notation "xs '⊄' E" := (all_notin xs E)
(at level 67) : gen_env_scope.

Bind Scope gen_env_scope with gen_env.
Delimit Scope gen_env_scope with gen_env.
Local Open Scope gen_env_scope.

Section Prop_Definitions.

Variable A B : Type.
Implicit Types x y : TVar.
Implicit Types xs ys : list TVar.
Implicit Types v w : A.
Implicit Types vs ws : list A.
Implicit Types E F G : gen_env A.
Implicit Types f g : A -> B.

Inductive ok : gen_env A -> Prop :=
| ok_nil : ok nil
| ok_cons : forall x v F, ok F ∧ ¬ belongs x F -> ok ((x, v) :: F)
.

Definition binds x v E := get x E = Some v.

Definition all_binds E F := forall x v, binds x v E -> binds x v F.

Definition eq E F := all_binds E F ∧ all_binds F E.

End Prop_Definitions.

x '∹' v '⋲' E to be read x is bound to v in E.

Notation "x '∹' v '⋲' E" := (binds x v E)
(at level 65) : gen_env_scope.

E '⊏' F to be read F all_binds E, i.e. E is included in F.

Notation "E '⊏' F" := (all_binds E F)
(at level 65) : gen_env_scope.

E '≍' F to be read F is equivalent to E, i.e. E binds as F.

Notation "E '≍' F" := (eq E F)
(at level 68) : gen_env_scope.

Bind Scope gen_env_scope with gen_env.
Delimit Scope gen_env_scope with gen_env.
Local Open Scope gen_env_scope.

Properties

Section Properties.
Variable A B : Type.
Implicit Types x y : TVar.
Implicit Types xs ys : list TVar.
Implicit Types v w : A.
Implicit Types vs ws : list A.
Implicit Types E F G : gen_env A.
Implicit Types f g : A -> B.

Primary properties

Induction scheme over environments.

Lemma env_ind : forall (P : gen_env A -> Prop),
  (P (@empty A)) ->
  (forall E x v, P E -> P (E & (x ∶ v))) ->
  (forall E, P E).
Proof.
  unfold concat, single, singles.
  induction E as [ | (x, v) ]; simpl in *; auto.
Qed.

Properties of singulars

Lemma singles_empty :
  nil ∷ nil = (@empty A ).
Proof. auto. Qed.

Lemma singles_cons : forall x xs v vs,
  (x :: xs) ∷ (v :: vs) = (xs ∷ vs) & (x ∶ v).
Proof. auto. Qed.

Lemma singles_empty_r : forall xs,
  xs ∷ nil = (@empty A ).
Proof. induction xs as [ | x ]; auto. Qed.

Lemma singles_empty_l : forall vs,
  nil ∷ vs = (@empty A ).
Proof. induction vs as [ | v ]; auto. Qed.

Properties of concatenation

Lemma concat_empty_r : forall E,
  E & (@empty A ) = E.
Proof. auto. Qed.

Lemma concat_empty_l : forall E,
  (@empty A ) & E = E.
Proof.
  induction E as [ | (x, v) ]; unfold concat in *;
    simpl in *; [ | rewrite IHE ]; auto.
Qed.

Lemma concat_assoc : forall E F G,
  E & (F & G) = (E & F) & G.
Proof.
  intros. unfold concat. rewrite app_assoc. auto.
Qed.

Properties of get

Lemma get_empty : forall x,
  get x (@empty A) = None.
Proof. auto. Qed.

Lemma get_single_eq : forall x y v,
  x = y ->
  get x (y ∶ v) = Some v.
Proof. intros. rewrite H. simpl. apply eq_keys_true. Qed.

Lemma get_dec : forall x E,
  { v : A | get x E = Some v } + { get x E = None }.
Proof.
  intros. induction E as [ | (y, w) ].
  right; auto. simpl. destruct (eq_keys_dec x y).
  left; exists w; auto. auto.
Qed.

Properties of dom

Lemma dom_empty :
  dom (@empty A) = nil.
Proof. auto. Qed.

Lemma dom_empty_inv : forall E,
  dom (E) = nil ->
  E = (@empty A ).
Proof. induction E as [ | (x, v) ]; intros; auto. inversion H. Qed.

Lemma dom_single : forall x v,
  dom (x ∶ v) = x :: nil.
Proof. auto. Qed.

Lemma dom_singles : forall xs vs,
  length xs = length vs ->
  dom (xs ∷ vs) = xs.
Proof.
  induction xs; induction vs; intros; auto.
  inversion H. simpl. inversion H.
  rewrite (IHxs vs H1); auto.
Qed.

Lemma dom_singles_incl : forall xs vs,
  List.incl (dom (xs ∷ vs)) xs.
Proof.
  induction xs; induction vs; intros; simpl; auto.
  apply incl_refl.
  unfold List.incl; intros; inversion H.
  apply List.incl_cons. simpl; auto.
  apply List.incl_tl. auto.
Qed.

Lemma dom_concat : forall E F,
  dom (E & F) = List.app (dom F) (dom E).
Proof.
  intros E F; generalize E; induction F as [ | (x, v) ];
    intros; simpl in *; auto.
  rewrite IHF. reflexivity.
Qed.

Properties of img

Lemma img_empty :
  img (@empty A) = nil.
Proof. auto. Qed.

Lemma img_empty_inv : forall E,
  img (E) = nil ->
  E = (@empty A ).
Proof. induction E as [ | (x, v) ]; intros; auto. inversion H. Qed.

Lemma img_single : forall x v,
  img (x ∶ v) = v :: nil.
Proof. auto. Qed.

Lemma img_singles : forall xs vs,
  length xs = length vs ->
  img (xs ∷ vs) = vs.
Proof.
  induction xs; induction vs; intros; auto.
  inversion H. simpl. inversion H.
  rewrite (IHxs vs H1); auto.
Qed.

Lemma img_singles_incl : forall xs vs,
  List.incl (img (xs ∷ vs)) vs.
Proof.
  induction xs; induction vs; intros; simpl; auto.
  apply incl_refl.
  unfold List.incl; intros; inversion H.
  apply incl_refl.
  apply List.incl_cons. simpl; auto.
  apply List.incl_tl. auto.
Qed.

Lemma img_concat : forall E F,
  img (E & F) = List.app (img F) (img E).
Proof.
  intros E F; generalize E; induction F as [ | (x, v) ];
    intros; simpl in *; auto.
  rewrite IHF. reflexivity.
Qed.

Lemma dom_img_id : forall E,
  (dom E) ∷ (img E) = E.
Proof.
  induction E as [ | (x, v) ]; simpl in *; auto. rewrite IHE; auto.
Qed.

Lemma length_dom_img_eq : forall E,
  length (dom E) = length (img E).
Proof. induction E as [ | (x, v) ]; simpl in *; auto. Qed.

Properties of belongs

Lemma belongs_empty : forall x,
  x ∈ (@empty A ) ->
  False.
Proof. auto. Qed.

Lemma belongs_single : forall x y v,
  x = y ->
  x ∈ (y ∶ v).
Proof. unfold belongs; simpl; auto. Qed.

Lemma belongs_single_inv : forall x y v,
  x ∈ (y ∶ v) ->
  x = y.
Proof.
  unfold belongs; simpl; intros; inversion H; auto; inversion H0.
Qed.

Lemma belongs_singles : forall x xs vs,
  length xs = length vs ->
  List.In x xs ->
  x ∈ (xs ∷ vs).
Proof.
  intros; unfold belongs; simpl; auto.
  rewrite dom_singles; auto.
Qed.

Lemma belongs_singles_inv : forall x xs vs,
  length xs = length vs ->
  x ∈ (xs ∷ vs) ->
  List.In x xs.
Proof.
  intros; unfold belongs in *; simpl in *; auto.
  rewrite dom_singles in H0; auto.
Qed.

Lemma belongs_concat_l : forall x F G,
  x ∈ F ->
  x ∈ (F & G).
Proof.
  unfold belongs. intros. rewrite dom_concat.
  apply List.in_or_app. right; auto.
Qed.

Lemma belongs_concat_r : forall x F G,
  x ∈ F ->
  x ∈ (G & F).
Proof.
  unfold belongs. intros. rewrite dom_concat.
  apply List.in_or_app. left; auto.
Qed.

Lemma belongs_concat_inv : forall x F G,
  x ∈ (F & G) ->
  x ∈ F ∨ x ∈ G.
Proof.
  unfold belongs. intros. rewrite dom_concat in * |-.
  apply or_comm. apply List.in_app_or; auto.
Qed.

Lemma belongs_dom : forall x E,
  x ∈ E ->
  List.In x (dom E).
Proof. auto. Qed.

Lemma belongs_dom_inv : forall x E,
  List.In x (dom E) ->
  x ∈ E.
Proof. auto. Qed.

Properties of all_belongs

Lemma all_belongs_belongs : forall x xs E,
  (x :: xs) ⊂ E ->
  x ∈ E ∧ xs ⊂ E.
Proof.
  unfold all_belongs. intros. simpl in *.
  split; [ | intros ]; apply H; auto.
Qed.

Lemma belongs_all_belongs : forall x xs E,
  x ∈ E ∧ xs ⊂ E ->
  (x :: xs) ⊂ E.
Proof.
  unfold all_belongs. intros. simpl in *.
  destruct H. destruct H0; [ rewrite <- H0 | apply H1]; auto.
Qed.

Lemma all_belongs_empty : forall xs,
  xs ⊂ (@empty A ) ->
  xs = nil.
Proof.
  induction xs as [ | x ]; intro; simpl in *; auto.
  unfold all_belongs, belongs in H.
  rewrite dom_empty in H. simpl in H.
  elim H with x. left; auto.
Qed.

Lemma all_belongs_nil : forall E,
  nil ⊂ E.
Proof. unfold all_belongs; simpl; intros; inversion H. Qed.

Lemma all_belongs_single : forall xs y v,
  xs = y :: nil ->
  xs ⊂ (y ∶ v).
Proof.
  intros. rewrite H. unfold all_belongs. intros. auto.
Qed.

Lemma all_belongs_single_inv : forall xs y v,
  length xs = 1 ->
  xs ⊂ (y ∶ v) ->
  xs = y :: nil.
Proof.
  induction xs as [ | x ]; intros; simpl in *; auto;
    inversion H.
  assert (xs = nil) as Hxsnil by
    (induction xs; simpl in *; auto; inversion H2).
  rewrite Hxsnil; f_equal.
  unfold all_belongs in H0; simpl in H0.
  assert (x ∈ (y ∶ v)) by
    (apply H0; left; auto).
  inversion H1; auto. inversion H3.
Qed.

Lemma all_belongs_singles : forall xs ys vs,
  length ys = length vs ->
  List.incl xs ys ->
  xs ⊂ (ys ∷ vs).
Proof.
  unfold all_belongs. intros. apply belongs_singles; auto.
Qed.

Lemma all_belongs_singles_inv : forall xs ys vs,
  xs ⊂ (ys ∷ vs) ->
  List.incl xs ys.
Proof.
  unfold all_belongs. intros. unfold belongs in H.
  unfold List.incl. intros. apply H in H0.
  assert (forall x l l', List.In x l -> List.incl l l' -> List.In x l')
    as Hincl by auto.
  apply Hincl with (dom (ys ∷ vs)); auto.
  apply dom_singles_incl.
Qed.

Lemma all_belongs_concat_l : forall xs F G,
  xs ⊂ F ->
  xs ⊂ (F & G).
Proof.
  intros. unfold all_belongs in *. intros. apply H in H0.
  apply belongs_concat_l; auto.
Qed.

Lemma all_belongs_concat_r : forall xs F G,
  xs ⊂ F ->
  xs ⊂ (G & F).
Proof.
  intros. unfold all_belongs in *. intros. apply H in H0.
  apply belongs_concat_r; auto.
Qed.

Lemma all_belongs_dom : forall xs E,
  xs ⊂ E ->
  List.incl xs (dom E).
Proof. auto. Qed.

Lemma all_belongs_dom_inv : forall xs E F,
  List.incl xs (dom E) ->
  xs ⊂ E.
Proof. auto. Qed.

Properties of notin

Lemma notin_belongs : forall x E,
  x ∉ E ->
  ¬ x ∈ E.
Proof. auto. Qed.

Lemma belongs_notin : forall x E,
  x ∈ E ->
  ¬ x ∉ E.
Proof. auto. Qed.

Lemma notin_belongs_neq : forall x y E,
  x ∈ E -> y ∉ E ->
  x <> y.
Proof. intros. intro. apply H0. rewrite H1 in *; auto. Qed.

Lemma notin_empty : forall x,
  x ∉ (@empty A ).
Proof. unfold notin. auto. Qed.

Lemma notin_single : forall x y v,
  x <> y ->
  x ∉ (y ∶ v).
Proof.
  intros x y v Hneq Hin. elim Hneq.
  apply belongs_single_inv with v; auto.
Qed.

Lemma notin_single_inv : forall x y v,
  x ∉ (y ∶ v) ->
  x <> y.
Proof.
  intros x y v Hnotin Heq. elim Hnotin.
  apply belongs_single; auto.
Qed.

Lemma notin_singles : forall x xs vs,
  ¬ List.In x xs ->
  x ∉ (xs ∷ vs).
Proof.
  intros x xs vs Hnotin Hin. elim Hnotin.
  unfold belongs in Hin.
  assert (forall x l l', List.In x l -> List.incl l l' -> List.In x l')
    as Hincl by auto.
  apply Hincl with (dom (xs ∷ vs)); auto. apply dom_singles_incl.
Qed.

Lemma notin_singles_inv : forall x xs vs,
  length xs = length vs ->
  x ∉ (xs ∷ vs) ->
  ¬ List.In x xs.
Proof.
  intros x xs vs Heq Hnotin Hin. elim Hnotin.
  unfold belongs. rewrite dom_singles; auto.
Qed.

Lemma notin_concat : forall x F G,
  x ∉ F -> x ∉ G ->
  x ∉ (F & G).
Proof.
  intros x F G HnotinF HnotinG HinFG. apply belongs_concat_inv in HinFG.
  destruct HinFG; [ elim HnotinF | elim HnotinG ]; auto.
Qed.

Lemma notin_concat_inv : forall x F G,
  x ∉ (F & G) ->
  x ∉ F ∧ x ∉ G.
Proof.
  intros x F G Hnotin.
  split; intro Hin; elim Hnotin;
    [ apply belongs_concat_l | apply belongs_concat_r ]; auto.
Qed.

Lemma notin_dom : forall x E,
  x ∉ E ->
  ¬ List.In x (dom E).
Proof. auto. Qed.

Lemma notin_dom_inv : forall x E F,
  ¬ List.In x (dom E) ->
  x ∉ E.
Proof. auto. Qed.

Properties of all_notin

Lemma all_notin_empty_l : forall E,
  nil ⊄ E.
Proof. unfold all_notin; intros. inversion H. Qed.

Lemma all_notin_notin : forall x xs E,
  (x :: xs) ⊄ E ->
  x ∉ E ∧ xs ⊄ E.
Proof.
  unfold all_notin; simpl. intros. auto.
Qed.

Lemma notin_all_notin : forall x xs E,
  x ∉ E ∧ xs ⊄ E ->
  (x :: xs) ⊄ E.
Proof.
  unfold all_notin; simpl. intros.
  destruct H. destruct H0; [ rewrite <- H0 | ]; auto.
Qed.

Lemma all_notin_belongs_neq : forall x ys E,
  x ∈ E -> ys ⊄ E ->
  ¬ List.In x ys.
Proof.
  intros. unfold all_notin in *. intro. apply H0 in H1. contradiction.
Qed.

Lemma all_notin_empty_r : forall xs,
  xs ⊄ (@empty A ).
Proof.
  unfold all_notin. intros. apply notin_empty.
Qed.

Lemma all_notin_nil : forall E,
  nil ⊄ E.
Proof. unfold all_notin. intros. inversion H. Qed.

Lemma all_notin_single : forall xs y v,
  ¬ List.In y xs ->
  xs ⊄ (y ∶ v).
Proof.
  intros. unfold all_notin. intros.
  apply notin_single. intro. rewrite H1 in H0.
  contradiction.
Qed.

Lemma all_notin_single_inv : forall xs y v,
  xs ⊄ (y ∶ v) ->
  ¬ List.In y xs.
Proof.
  unfold all_notin. intros. intro.
  apply H in H0. apply H0. apply belongs_single; auto.
Qed.

Lemma all_notin_singles : forall xs ys vs,
  List.Forall (fun x => ¬ List.In x ys) xs ->
  xs ⊄ (ys ∷ vs).
Proof.
  intros xs ys vs Hforall.
  unfold all_notin; intros x Hin.
  apply notin_singles.
  apply (List.Forall_forall (fun x => ¬ In x ys) xs); intros; auto.
Qed.

Lemma all_notin_singles_inv : forall xs ys vs,
  length ys = length vs ->
  xs ⊄ (ys ∷ vs) ->
  List.Forall (fun x => ¬ List.In x ys) xs.
Proof.
  intros xs ys vs Heq Hnotin. unfold all_notin in Hnotin.
  elim (List.Forall_forall (fun x => ¬ In x ys) xs); intros.
  apply H0. intros. apply Hnotin in H1.
  apply notin_singles_inv with vs; auto.
Qed.

Lemma all_notin_concat : forall xs F G,
  xs ⊄ F -> xs ⊄ G ->
  xs ⊄ (F & G).
Proof.
  intros. unfold all_notin in *. intros.
  apply notin_concat; auto.
Qed.

Lemma all_notin_concat_inv : forall xs F G,
  xs ⊄ (F & G) ->
  xs ⊄ F ∧ xs ⊄ G.
Proof.
  intros. unfold all_notin in *.
  split; intros; apply H in H0;
    apply notin_concat_inv in H0; destruct H0; auto.
Qed.

Lemma all_notin_dom : forall xs E,
  xs ⊄ E ->
  List.Forall (fun x => ¬ List.In x (dom E)) xs.
Proof.
  intros. unfold all_notin, notin, belongs in *.
  apply List.Forall_forall; auto.
Qed.

Lemma all_notin_dom_inv : forall xs E,
  List.Forall (fun x => ¬ List.In x (dom E)) xs ->
  xs ⊄ E.
Proof.
  intros. unfold all_notin, notin, belongs.
  apply List.Forall_forall; auto.
Qed.

Properties of ok

Lemma ok_empty :
  ok (@empty A).
Proof. apply ok_nil. Qed.

Lemma ok_NoDup_dom_eq : forall E,
  ok E <-> List.NoDup (dom E).
Proof.
  intros. induction E as [ | (x, v) ]; split; intros; simpl in *.
  apply List.NoDup_nil. apply ok_empty. inversion H. destruct H1.
  apply List.NoDup_cons; auto. apply IHE; auto.
  inversion H. apply ok_cons; split; auto. apply IHE; auto.
Qed.

Lemma ok_single : forall x v,
  ok (x ∶ v).
Proof.
  intros. apply ok_cons. split; [ apply ok_nil | ]; auto.
Qed.

Lemma ok_singles : forall xs vs,
  List.NoDup xs ->
  ok (xs ∷ vs).
Proof.
  induction xs; induction vs; intros; simpl in *; auto.
  apply ok_nil. apply ok_nil. apply ok_cons.
  assert (List.NoDup xs ∧ ¬ List.In a xs) as Hdup by
    (rewrite <- List.app_nil_l in H; split;
      [ apply List.NoDup_remove_1 in H | apply List.NoDup_remove_2 in H ];
      auto). destruct Hdup.
  apply IHxs with vs in H0.
  split; auto.
  unfold belongs.
  assert (forall x l l', ¬ List.In x l' -> List.incl l l' -> ¬ List.In x l)
    as Hincl by auto.
  apply Hincl with xs; auto.
  apply dom_singles_incl.
Qed.

Lemma ok_singles_inv : forall xs vs,
  length xs = length vs ->
  ok (xs ∷ vs) ->
  List.NoDup xs.
Proof.
  induction xs; induction vs; intros; simpl in *; auto.
  apply List.NoDup_nil. apply List.NoDup_nil.
  inversion H. inversion H. inversion H0. destruct H3.
  apply (IHxs vs) in H2; auto.
  unfold belongs in H6. rewrite dom_singles in H6; auto.
  apply List.NoDup_cons; auto.
Qed.

Lemma ok_concat : forall E F,
  ok E -> ok F ->
  (dom E) ⊄ F -> (dom F) ⊄ E ->
  ok (E & F).
Proof.
  intros. induction F as [ | (x, v) ]; simpl in *; auto.
  apply all_notin_notin in H2. destruct H2.
  inversion H0. destruct H5. clear x0 v0 F0 H0 H4 H6 H7.
  assert (dom E ⊄ F & x ∶ v) by auto. clear H1.
  apply all_notin_concat_inv in H0. destruct H0.
  apply all_notin_single_inv in H1.
  apply ok_cons.
  split. apply IHF; auto. apply notin_concat; auto.
Qed.

Lemma ok_concat_inv : forall E F,
  ok (E & F) ->
  ok E ∧ ok F ∧ (dom E) ⊄ F ∧ (dom F) ⊄ E.
Proof.
  intros.
  induction F as [ | (x, v) ]; simpl in *.
  split. auto. split. apply ok_empty.
  split. apply all_notin_empty_r.
  unfold all_notin; intros; contradiction.
  inversion H. destruct H1. clear x0 v0 F0 H0 H2 H3.
  apply IHF in H1. destruct H1. destruct H1. destruct H2.
  apply notin_concat_inv in H4. destruct H4.
  split. auto. split. apply ok_cons. split; auto.
  split.

  assert (dom E ⊄ F & x ∶ v). apply all_notin_concat; auto.
  unfold all_notin. intros. apply notin_single. intro.
  rewrite H7 in *. contradiction.
  auto.

  unfold all_notin in *. intros. simpl in H6.
  destruct H6; auto. rewrite <- H6; auto.
Qed.

Lemma ok_concat_comm : forall E F,
  ok (E & F) ->
  ok (F & E).
Proof.
  intros. apply ok_concat_inv in H. destruct H. destruct H0. destruct H1.
  apply ok_concat; auto.
Qed.

Lemma belongs_ok_concat_inv_l : forall x F G,
  ok (F & G) ->
  x ∈ F ->
  x ∉ G.
Proof.
  intros. apply ok_concat_inv in H.
  destruct H. destruct H1. destruct H2.
  unfold all_notin, notin, belongs in *.
  auto.
Qed.

Lemma belongs_ok_concat_inv_r : forall x F G,
  ok (F & G) ->
  x ∈ G ->
  x ∉ F.
Proof.
  intros. apply ok_concat_inv in H.
  destruct H. destruct H1. destruct H2.
  unfold all_notin, notin, belongs in *.
  auto.
Qed.

Lemma concat_not_ok : forall x F G,
  x ∈ F -> x ∈ G ->
  ¬ ok (F & G).
Proof.
  intros. intro. apply (belongs_ok_concat_inv_r x F G) in H1; auto.
Qed.

Lemma ok_dom : forall E,
  List.NoDup (dom E) -> ok E.
Proof.
  induction E as [ | (x, v) ]; intros; simpl in *; auto.
  apply ok_empty. inversion H. assert (ok (E & (x ∶ v))); auto.
  apply ok_concat; auto. apply ok_single. apply all_notin_single; auto.
  rewrite dom_single. apply notin_all_notin. split; auto.
  apply all_notin_empty_l.
Qed.

Lemma ok_dom_inv : forall E,
  ok E -> List.NoDup (dom E).
Proof.
  induction E as [ | (x, v) ]; intros; simpl in *; auto.
  apply List.NoDup_nil.
  assert (ok (E & (x ∶ v))) by auto. clear H. apply ok_concat_inv in H0.
  destruct H0. destruct H0. destruct H1.
  rewrite dom_single in *. apply all_notin_notin in H2. destruct H2.
  unfold notin, belongs in H2.
  apply List.NoDup_cons; auto.
Qed.

Properties of map

Lemma map_empty : forall f,
  map f (@empty A) = (@empty B ).
Proof. auto. Qed.

Lemma map_single : forall f x v,
  map f (x ∶ v) = x ∶ (f v).
Proof. auto. Qed.

Lemma map_singles : forall f xs vs,
  map f (xs ∷ vs) = xs ∷ (List.map f vs).
Proof.
  induction xs; induction vs; simpl in *; auto.
  f_equal. apply IHxs.
Qed.

Lemma map_concat : forall f E F,
  map f (E & F) = (map f E) & (map f F).
Proof.
  intros. induction F as [ | (x, v) ]; simpl; auto.
  rewrite IHF. reflexivity.
Qed.

Lemma dom_map : forall E f,
  dom (map f E) = dom E.
Proof.
  intros; induction E as [ | (x, v) ]; simpl; auto.
  rewrite IHE; auto.
Qed.

Lemma belongs_map : forall x E f,
  x ∈ E ->
  x ∈ (map f E).
Proof.
  unfold belongs. intros; rewrite dom_map; auto.
Qed.

Lemma belongs_map_inv : forall x E f,
  x ∈ (map f E) ->
  x ∈ E.
Proof.
  unfold belongs. intros; rewrite dom_map in * |-; auto.
Qed.

Lemma all_belongs_map : forall xs E f,
  xs ⊂ E ->
  xs ⊂ (map f E).
Proof.
  unfold all_belongs; intros. apply H in H0. apply belongs_map; auto.
Qed.

Lemma all_belongs_map_inv : forall xs E f,
  xs ⊂ (map f E) ->
  xs ⊂ E.
Proof.
  unfold all_belongs; intros. apply H in H0.
  apply belongs_map_inv with f; auto.
Qed.

Lemma notin_map : forall x E f,
  x ∉ E ->
  x ∉ (map f E).
Proof.
  intros x E f Hnotin Hin. elim Hnotin.
  apply belongs_map_inv with f; auto.
Qed.

Lemma notin_map_inv : forall x E f,
  x ∉ (map f E) ->
  x ∉ E.
Proof.
  intros x E f Hnotin Hin. elim Hnotin.
  apply belongs_map; auto.
Qed.

Lemma all_notin_map : forall xs E f,
  xs ⊄ E ->
  xs ⊄ (map f E).
Proof.
  intros. unfold all_notin in *. intros.
  apply H in H0. apply notin_map; auto.
Qed.

Lemma all_notin_map_inv : forall xs E f,
  xs ⊄ (map f E) ->
  xs ⊄ E.
Proof.
  intros. unfold all_notin in *; intros.
  apply H in H0. apply notin_map_inv with f; auto.
Qed.

Lemma ok_map : forall E f,
  ok E ->
  ok (map f E).
Proof.
  intros. induction E as [ | (x, v) ]; simpl in *; auto.
  apply ok_nil. apply ok_cons.
  inversion H. clear x0 v0 F H0 H2 H3. destruct H1.
  split; auto. apply notin_map; auto.
Qed.

Lemma ok_map_inv : forall E f,
  ok (map f E) ->
  ok E.
Proof.
  intros. induction E as [ | (x, v) ]; simpl in *; auto.
  apply ok_nil. apply ok_cons.
  inversion H. clear x0 v0 F H0 H2 H3. destruct H1.
  split; auto. apply notin_map_inv with f; auto.
Qed.

Properties of update

Lemma update_empty_r : forall E,
  E ::= (@empty A ) = E.
Proof. auto. Qed.

Lemma update_empty_l : forall E,
  (@empty A ) ::= E = (@empty A ).
Proof.
  induction E as [ | (x, v) ]; simpl; auto.
  rewrite IHE. auto.
Qed.

Lemma update_single : forall x v y w,
  x = y ->
  (x ∶ v) ::= (y ∶ w) = (x ∶ w).
Proof. intros. rewrite H. simpl. apply eq_keys_true. Qed.

Lemma update_single_neq : forall x v y w,
  x <> y ->
  (x ∶ v) ::= (y ∶ w) = (x ∶ v).
Proof. intros. simpl. apply eq_keys_false; auto. Qed.

Lemma update_concat_r : forall E F G,
  E ::= (F & G) = (E ::= F) ::= G.
Proof.
  induction G as [ | (x, v) ]; simpl; auto.
  rewrite IHG. auto.
Qed.

Lemma dom_update_one : forall E x v,
  dom (update_one E x v) = dom E.
Proof.
  induction E as [ | (y, w) ]; intros; auto.
  simpl. destruct (eq_keys_dec x y); simpl; auto. rewrite IHE; auto.
Qed.

Lemma dom_update : forall E F,
  dom (E ::= F) = dom E.
Proof.
  induction F as [ | (x, v) ]; simpl in *; auto.
  rewrite dom_update_one, IHF; auto.
Qed.

Lemma belongs_update_one : forall x E y v,
  x ∈ E ->
  x ∈ update_one E y v.
Proof.
  unfold belongs. intros; rewrite dom_update_one; auto.
Qed.

Lemma belongs_update : forall x E F,
  x ∈ E ->
  x ∈ (E ::= F).
Proof.
  unfold belongs. intros; rewrite dom_update; auto.
Qed.

Lemma belongs_update_one_inv : forall x E y v,
  x ∈ update_one E y v ->
  x ∈ E.
Proof.
  unfold belongs. intros; rewrite dom_update_one in * |-; auto.
Qed.

Lemma belongs_update_inv : forall x E F,
  x ∈ (E ::= F) ->
  x ∈ E.
Proof.
  unfold belongs. intros; rewrite dom_update in * |-; auto.
Qed.

Lemma all_belongs_update : forall xs E F,
  xs ⊂ E ->
  xs ⊂ (E ::= F).
Proof.
  unfold all_belongs; intros. apply H in H0. apply belongs_update; auto.
Qed.

Lemma all_belongs_update_inv : forall xs E F,
  xs ⊂ (E ::= F) ->
  xs ⊂ E.
Proof.
  unfold all_belongs; intros. apply H in H0.
  apply belongs_update_inv with F; auto.
Qed.

Lemma notin_update_one : forall x E y v,
  x ∉ E ->
  x ∉ update_one E y v.
Proof.
  intros x E y v Hnotin Hin. elim Hnotin.
  apply belongs_update_one_inv with y v; auto.
Qed.

Lemma notin_update : forall x E F,
  x ∉ E ->
  x ∉ (E ::= F).
Proof.
  intros x E F Hnotin Hin. elim Hnotin.
  apply belongs_update_inv with F; auto.
Qed.

Lemma notin_update_one_inv : forall x E y v,
  x ∉ update_one E y v ->
  x ∉ E.
Proof.
  intros x E y v Hnotin Hin. elim Hnotin.
  apply belongs_update_one; auto.
Qed.

Lemma notin_update_inv : forall x E F,
  x ∉ (E ::= F) ->
  x ∉ E.
Proof.
  intros x E F Hnotin Hin. elim Hnotin.
  apply belongs_update; auto.
Qed.

Lemma all_notin_update : forall xs E F,
  xs ⊄ E ->
  xs ⊄ (E ::= F).
Proof.
  intros. unfold all_notin in *. intros.
  apply H in H0. apply notin_update; auto.
Qed.

Lemma all_notin_update_inv : forall xs E F,
  xs ⊄ (E ::= F) ->
  xs ⊄ E.
Proof.
  intros. unfold all_notin in *; intros.
  apply H in H0. apply notin_update_inv with F; auto.
Qed.

Lemma update_one_notin : forall E x v,
  x ∉ E ->
  update_one E x v = E.
Proof.
  induction E as [ | (y, w) ]; intros; simpl in *; auto.
  assert (x ∉ (E & (y ∶ w))) by auto.
  apply notin_concat_inv in H0. destruct H0.
  apply notin_single_inv in H1. rewrite eq_keys_false; auto.
  apply IHE with x v in H0. rewrite H0; auto.
Qed.

Lemma update_notin : forall E F,
  (dom F) ⊄ E ->
  E ::= F = E.
Proof.
  induction F as [ | (x, v) ]; unfold all_belongs;
    intros; simpl in *; auto.
  apply all_notin_notin in H.
  destruct H.
  apply IHF in H0. rewrite H0.
  apply update_one_notin; auto.
Qed.

Lemma map_update_one : forall f E x v,
  map f (update_one E x v) =
  update_one (map f E) x (f v).
Proof.
  intros. induction E as [ | (y, w) ]; simpl; auto.
  destruct (eq_keys_dec x y); simpl; auto. rewrite IHE; auto.
Qed.

Lemma map_update : forall f E F,
  map f (E ::= F) = (map f E) ::= (map f F).
Proof.
  intros. induction F as [ | (x, v) ]; simpl; auto.
  rewrite <- IHF. apply map_update_one.
Qed.

Lemma ok_update_one : forall E x v,
  ok E ->
  ok (update_one E x v).
Proof.
  intros. induction E as [ | (y, w) ]; simpl in *; auto.
  inversion H. destruct H1.
  destruct (eq_keys_dec x y); auto.
  apply ok_cons. auto.
  apply ok_cons. split; auto. apply notin_update_one; auto.
Qed.

Lemma ok_update : forall E F,
  ok E ->
  ok (E ::= F).
Proof.
  intros. induction F as [ | (x, v) ]; simpl in *; auto.
  apply ok_update_one; auto.
Qed.

Lemma ok_update_one_inv : forall E x v,
  ok (update_one E x v) ->
  ok E.
Proof.
  intros. induction E as [ | (y, w) ]; simpl in *; auto.
  apply ok_cons.
  destruct (eq_keys_dec x y); inversion H; destruct H1;
    split; auto; apply notin_update_one_inv with x v; auto.
Qed.

Lemma ok_update_inv : forall E F,
  ok (E ::= F) ->
  ok E.
Proof.
  intros. induction F as [ | (x, v) ]; simpl in *; auto.
  apply ok_update_one_inv in H; auto.
Qed.

Lemma update_one_concat_l : forall E F x v,
  ok (E & F) ->
  update_one (E & F) x v =
  update_one E x v & update_one F x v.
Proof.
  intros. induction F as [ | (y, w) ]; simpl in *; auto.
  inversion H. destruct H1. clear x0 v0 F0 H0 H2 H3 H.
  rewrite IHF; auto.
  destruct (eq_keys_dec x y). rewrite e in *. simpl.
  rewrite update_one_notin; auto.
  apply notin_concat_inv in H4. destruct H4; auto. auto.
Qed.

Lemma update_concat_l : forall E F G,
  ok (E & F) ->
  (E & F) ::= G = (E ::= G) & (F ::= G).
Proof.
  intros. induction G as [ | (x, v) ]; simpl in *; auto.
  rewrite IHG. apply update_one_concat_l.
  apply ok_concat_inv in H. destruct H. destruct H0. destruct H1.
  assert (ok (E ::= G)) by (apply ok_update; auto).
  assert (ok (F ::= G)) by (apply ok_update; auto).
  apply ok_concat; auto; rewrite dom_update; apply all_notin_update; auto.
Qed.

Properties of remove

Lemma remove_empty : forall x,
  (@empty A ) ∖ {x} = (@empty A ).
Proof. auto. Qed.

Lemma remove_single_eq : forall x v y,
  x = y ->
  (x ∶ v) ∖ {y} = (@empty A ).
Proof. intros. rewrite H. simpl. apply eq_keys_true. Qed.

Lemma remove_single_not_eq : forall x v y,
  x <> y ->
  (x ∶ v) ∖ {y} = (x ∶ v).
Proof. intros. simpl. apply eq_keys_false; auto. Qed.

Lemma remove_notin : forall x E,
  x ∉ E ->
  E ∖ {x} = E.
Proof.
  intros. induction E as [ | (y, v) ]; simpl; auto.
  assert (x ∉ E & (y ∶ v)) by auto. clear H.
  apply notin_concat_inv in H0. destruct H0. apply IHE in H. rewrite H.
  apply notin_single_inv in H0. apply eq_keys_false; auto.
Qed.

Lemma notin_remove_notin : forall x y E,
  x ∉ E ->
  x ∉ (E ∖ {y}).
Proof.
  intros. induction E as [ | (z, v) ]; simpl; auto.
  assert (x ∉ E & (z ∶ v)) by auto. clear H.
  apply notin_concat_inv in H0. destruct H0.
  apply notin_single_inv in H0.
  destruct (eq_keys_dec y z); auto.
  apply IHE in H.
  assert (x ∉ (E ∖ {y}) & (z ∶ v)).
  apply notin_concat; auto. apply notin_single; auto.
  auto.
Qed.

Lemma all_notin_remove_notin : forall xs y E,
  xs ⊄ E ->
  xs ⊄ (E ∖ {y}).
Proof.
  intros. induction xs as [ | x ].
  unfold all_notin. intros. inversion H0.
  apply all_notin_notin in H. destruct H.
  apply IHxs in H0.
  apply notin_all_notin. split; auto.
  apply notin_remove_notin; auto.
Qed.

Lemma belongs_remove : forall x y E,
  x <> y -> x ∈ E ->
  x ∈ (E ∖ {y}).
Proof.
  induction E as [ | (z, v) ]; intros; simpl in *; auto.
  assert (x ∈ E & (z ∶ v)) by auto; clear H0.
  apply belongs_concat_inv in H1.
  destruct H1; destruct (eq_keys_dec y z); auto.
  assert (x ∈ (E ∖ {y}) & (z ∶ v)); auto.
  apply belongs_concat_l; auto.
  rewrite e in *. apply belongs_single_inv in H0. contradiction.
  assert (x ∈ (E ∖ {y}) & (z ∶ v)); auto.
  apply belongs_concat_r; auto.
Qed.

Lemma belongs_remove_inv : forall x y E,
  ok E ->
  x ∈ (E ∖ {y}) -> x <> y.
Proof.
  intros. intro. rewrite H1 in *. clear x H1.
  induction E as [ | (x, v) ]; simpl in *; auto.
  inversion H. clear x0 v0 F H1 H3 H4. destruct H2.
  destruct (eq_keys_dec y x). rewrite e in *; contradiction.
  assert (y ∈ ((E ∖ {y}) & (x ∶ v))) by auto. clear H0.
  apply belongs_concat_inv in H3. destruct H3; auto.
  apply belongs_single_inv in H0; auto.
Qed.

Lemma remove_belongs_concat_r : forall x E F,
  x ∈ F ->
  (E & F) ∖ {x} = E & (F ∖ {x}).
Proof.
  intros. induction F as [ | (y, v) ]; simpl; auto. inversion H.
  assert (x ∈ F & (y ∶ v)) by auto. clear H.
  apply belongs_concat_inv in H0. destruct H0.
  apply IHF in H. rewrite H.
  destruct (eq_keys_dec x y); auto.
  apply belongs_single_inv in H. rewrite H.
  rewrite ?eq_keys_true; auto.
Qed.

Lemma remove_belongs_concat_l : forall x E F,
  x ∉ F ->
  (E & F) ∖ {x} = (E ∖ {x}) & F.
Proof.
  intros. induction F as [ | (y, v) ]; simpl; auto.
  assert (x ∉ F & (y ∶ v)) by auto. clear H.
  apply notin_concat_inv in H0. destruct H0.
  apply IHF in H. rewrite H.
  destruct (eq_keys_dec x y); auto.
  apply notin_single_inv in H0. contradiction.
Qed.

Lemma remove_ok_notin : forall x E,
  ok E ->
  x ∉ (E ∖ {x}).
Proof.
  intros. induction E as [ | (y, v) ]; simpl.
  apply notin_empty. inversion H. destruct H1.
  apply IHE in H1.
  destruct (eq_keys_dec x y).
  rewrite e in *; auto.
  assert (x ∉ (E ∖ {x}) & y ∶ v).
  apply notin_concat; auto. apply notin_single; auto.
  auto.
Qed.

Lemma remove_all_belongs : forall x xs F,
  ¬ List.In x xs -> (x :: xs) ⊂ F ->
  xs ⊂ (F ∖ {x}).
Proof.
  intros. unfold all_belongs in *. intros. simpl in H0.
  apply belongs_remove; auto. intro. rewrite H2 in *. contradiction.
Qed.

Lemma remove_map : forall f E x,
  (map f E) ∖ {x} = map f (E ∖ {x}).
Proof.
  intros. induction E as [ | (y, v)]; simpl; auto. rewrite IHE.
  destruct (eq_keys_dec x y); auto.
Qed.

Lemma remove_update_one : forall x y v E,
  ok E ->
  (update_one E y v) ∖ {x} = update_one (E ∖ {x}) y v.
Proof.
  intros. induction E as [ | (y', v') ]. auto. simpl.
  inversion H. clear x0 v0 F H0 H2 H3 H. destruct H1.
  apply IHE in H.

  destruct (eq_keys_dec x y'). rewrite e in *. clear x e.

  destruct (eq_keys_dec y y'); simpl;
    destruct (eq_keys_dec y y'); simpl;
      rewrite ?eq_keys_true; auto.

  rewrite e, update_one_notin in *; auto. contradiction.

  destruct (eq_keys_dec y y'); simpl;
    destruct (eq_keys_dec y y'); simpl;
      destruct (eq_keys_dec x y'); simpl; auto.
  contradiction. contradiction. contradiction. contradiction.
  contradiction. contradiction. f_equal; auto.
Qed.

Lemma remove_update : forall x E F,
  ok E ->
  (E ::= F) ∖ {x} = (E ∖ {x}) ::= F.
Proof.
  intros. induction F as [ | (y, v) ]; simpl; auto.
  rewrite <- IHF. apply remove_update_one.
  apply ok_update; auto.
Qed.

Lemma remove_update_eq : forall x y v E,
  x = y ->
  (E ::= (y ∶ v)) ∖ {x} = E ∖ {x}.
Proof.
  intros. induction E as [ | (y', v') ]; simpl; auto.
  rewrite H in *; clear x H.
  destruct (eq_keys_dec y y'); simpl. rewrite e in *.
  rewrite eq_keys_true; auto. rewrite eq_keys_false; auto.
  f_equal; auto.
Qed.

Lemma ok_remove : forall x E,
  ok E ->
  ok (E ∖ {x}).
Proof.
  intros. induction E as [ | (y, v) ]; simpl; auto.
  inversion H. destruct H1.
  destruct (eq_keys_dec x y); auto.
  apply IHE in H1. apply ok_cons. split; auto.
  apply notin_remove_notin; auto.
Qed.

Properties of all_remove

Lemma all_remove_remove : forall x xs E,
  E ∖ (x :: xs) = (E ∖ {x}) ∖ xs.
Proof. auto. Qed.

Lemma all_remove_empty : forall xs,
  (@empty A ) ∖ xs = (@empty A ).
Proof. induction xs as [ | x ]; simpl; auto. Qed.

Lemma all_remove_single_in : forall x v xs,
  List.In x xs ->
  (x ∶ v) ∖ xs = (@empty A ).
Proof.
  induction xs as [ | y ]; intros; simpl in *; auto; inversion H.
  rewrite H0 in *. rewrite eq_keys_true. apply all_remove_empty.
  destruct (eq_keys_dec y x). apply all_remove_empty. auto.
Qed.

Lemma all_remove_single_not_in : forall x v xs,
  ¬ List.In x xs ->
  (x ∶ v) ∖ xs = (x ∶ v).
Proof.
  intros. induction xs as [ | y ]; simpl; auto.
  assert (x ≠ y ∧ ¬In x xs) by
    (split; intro; apply H;
      [ rewrite H0; apply in_eq | apply in_cons; auto ]).
  destruct H0. apply IHxs in H1. rewrite <- H1. f_equal.
  apply eq_keys_false; auto.
Qed.

Lemma all_remove_singles_in : forall xs vs ys,
  xs = ys -> length xs = length vs ->
  (xs ∷ vs) ∖ ys = (@empty A ).
Proof.
  intros xs vs ys Heq. rewrite Heq in *; clear xs Heq.
  generalize vs. clear vs.
  induction ys as [ | y ]; induction vs as [ | v ];
    intros; simpl in *; auto.
  inversion H. rewrite eq_keys_true; auto.
Qed.

Lemma all_remove_singles_not_in : forall xs vs ys,
  List.Forall (fun x => ¬ List.In x xs) ys ->
  (xs ∷ vs) ∖ ys = (xs ∷ vs).
Proof.
  intros. induction ys as [ | y ]; simpl; auto. inversion H.
  rewrite remove_notin; auto. apply notin_singles; auto.
Qed.

Lemma all_remove_notin : forall xs E,
  xs ⊄ E ->
  E ∖ xs = E.
Proof.
  intros. induction xs as [ | x ]; simpl; auto.
  apply all_notin_notin in H. destruct H.
  rewrite remove_notin; auto.
Qed.

Lemma notin_all_remove_notin : forall x ys E,
  x ∉ E ->
  x ∉ (E ∖ ys).
Proof.
  induction ys as [ | y ]; simpl; auto.
  intros.
  assert (x ∉ E ∖ {y}) by (apply notin_remove_notin; auto).
  auto.
Qed.

Lemma all_notin_all_remove_notin : forall xs ys E,
  xs ⊄ E ->
  xs ⊄ (E ∖ ys).
Proof.
  induction ys as [ | y ]; simpl; auto.
  intros.
  assert (xs ⊄ E ∖ {y}) by (apply all_notin_remove_notin; auto).
  auto.
Qed.

Lemma all_remove_ok_notin : forall xs E,
  ok E ->
  xs ⊄ (E ∖ xs).
Proof.
  induction xs as [ | x ]; intros; simpl.
  unfold all_notin. intros. inversion H0.
  apply notin_all_notin. split.
  apply notin_all_remove_notin. apply remove_ok_notin; auto.
  apply IHxs. apply ok_remove; auto.
Qed.

Lemma all_remove_belongs_concat_r : forall xs E F,
  List.NoDup xs ->
  xs ⊂ F ->
  (E & F) ∖ xs = E & (F ∖ xs).
Proof.
  induction xs as [ | x ]; intros; simpl; auto.
  generalize H0. intro. inversion H.
  apply all_belongs_belongs in H0. destruct H0.
  rewrite remove_belongs_concat_r; auto.
  rewrite IHxs; auto.
  apply remove_all_belongs; auto.
Qed.

Lemma all_remove_belongs_concat_l : forall xs E F,
  xs ⊄ F ->
  (E & F) ∖ xs = (E ∖ xs) & F.
Proof.
  induction xs as [ | x ]; intros; simpl; auto.
  apply all_notin_notin in H. destruct H.
  rewrite remove_belongs_concat_l; auto.
Qed.

Lemma all_remove_map : forall f E xs,
  (map f E) ∖ xs = map f (E ∖ xs).
Proof.
  intros. generalize E.
  induction xs as [ | x ]; intros; simpl; auto.
  rewrite remove_map. auto.
Qed.

Lemma all_remove_update : forall xs E F,
  ok E ->
  (E ::= F) ∖ xs = (E ∖ xs) ::= F.
Proof.
  intros. generalize H. generalize E. clear E H.
  induction xs as [ | x ]; intros; simpl; auto.
  rewrite remove_update; auto. apply IHxs. apply ok_remove; auto.
Qed.

Lemma ok_all_remove : forall xs E,
  ok E ->
  ok (E ∖ xs).
Proof.
  induction xs as [ | x ]; intros; simpl in *; auto.
  assert (ok (E ∖ {x})). apply ok_remove; auto. auto.
Qed.

Properties of binds

Lemma binds_empty : forall x v,
  x ∹ v ⋲ (@empty A ) ->
  False.
Proof. intros. inversion H. Qed.

Lemma binds_single : forall x v y w,
  x = y -> v = w ->
  x ∹ v ⋲ (y ∶ w).
Proof. intros. rewrite H, H0. unfold binds. simpl. apply eq_keys_true. Qed.

Lemma binds_single_inv : forall x v y w,
  x ∹ v ⋲ (y ∶ w) ->
  x = y ∧ v = w.
Proof.
  intros. inversion H.
  destruct (eq_keys_dec x y); inversion H1; auto.
Qed.

Lemma binds_singles : forall x v y w ys ws,
  x = y -> v = w ->
  x ∹ v ⋲ (y :: ys ∷ w :: ws).
Proof.
  intros. simpl. rewrite H, H0.
  unfold binds. simpl. apply eq_keys_true.
Qed.

Lemma binds_singles_inv : forall x v y w ys ws,
  x ∹ v ⋲ (y :: ys ∷ w :: ws) ->
  (x = y ∧ v = w) ∨ (x ∹ v ⋲ (ys ∷ ws)).
Proof.
  intros. simpl in *. inversion H.
  destruct (eq_keys_dec x y). inversion H1; auto. auto.
Qed.

Lemma binds_eq_inv : forall x v w E,
  x ∹ v ⋲ E -> x ∹ w ⋲ E ->
  v = w.
Proof.
  intros. inversion H. inversion H0. rewrite H2 in H3. inversion H3; auto.
Qed.

Lemma binds_concat_r : forall x v F G,
  x ∹ v ⋲ G ->
  x ∹ v ⋲ (F & G).
Proof.
  intros. induction G as [ | (y, w) ]; simpl in *; inversion H.
  unfold binds. simpl. destruct (eq_keys_dec x y); auto.
  apply IHG in H1. auto.
Qed.

Lemma binds_concat_l : forall x v F G,
  x ∹ v ⋲ F ->
  x ∉ G ->
  x ∹ v ⋲ (F & G).
Proof.
  intros. induction G as [ | (y, w) ]; simpl in *; auto.
  assert (x ∉ G & (y ∶ w)) as Hnotin by auto.
  apply notin_concat_inv in Hnotin. destruct Hnotin.
  apply IHG in H1.
  apply notin_single_inv in H2.
  unfold binds. simpl. rewrite eq_keys_false; auto.
Qed.

Lemma binds_concat_inv : forall x v F G,
  x ∹ v ⋲ (F & G) ->
  x ∹ v ⋲ G ∨ (x ∉ G ∧ x ∹ v ⋲ F).
Proof.
  induction G as [ | (y, w) ]; intros; simpl in *; auto.
  right; split; [ apply notin_empty | ]; auto.
  inversion H. destruct (eq_keys_dec x y). inversion H1.
  rewrite e, H2 in *. left. unfold binds. simpl.
  apply eq_keys_true.
  apply IHG in H1. destruct H1.
  left. unfold binds. simpl.
  rewrite eq_keys_false; auto.
  right. destruct H0. split; auto. assert (x ∉ G & y ∶ w); auto.
  apply notin_concat; auto. apply notin_single; auto.
Qed.

Lemma binds_belongs : forall x v F,
  x ∹ v ⋲ F ->
  x ∈ F.
Proof.
  induction F as [ | (y, w) ]; intros; simpl in *; inversion H; auto.
  unfold belongs; simpl; auto.
  destruct (eq_keys_dec x y); auto. right. apply IHF; auto.
Qed.

Lemma belongs_binds : forall x F,
  x ∈ F ->
  exists v, x ∹ v ⋲ F.
Proof.
  induction F as [ | (y, w) ]; intros; auto.
  inversion H. destruct (eq_keys_dec x y). rewrite e in *.
  exists w. unfold binds; simpl.
  apply eq_keys_true.
  assert (x ∈ F & y ∶ w) by auto. clear H.
  apply belongs_concat_inv in H0. destruct H0.
  apply IHF in H. destruct H. exists x0.
  unfold binds; simpl. rewrite eq_keys_false; auto.
  apply belongs_single_inv in H. contradiction.
Qed.

Lemma binds_map : forall x v E f,
  x ∹ v ⋲ E ->
  x ∹ (f v) ⋲ (map f E).
Proof.
  intros. induction E as [ | (y, w) ]; inversion H.
  unfold binds; simpl. destruct (eq_keys_dec x y).
  inversion H1. auto.
  apply IHE in H1. auto.
Qed.

Lemma binds_map_inv : forall x (w : B) E f,
  x ∹ w ⋲ (map f E) ->
  exists v, x ∹ v ⋲ E /\ w = f v.
Proof.
  intros. induction E as [ | (y, w') ]; simpl in *; inversion H.
  destruct (eq_keys_dec x y).
  inversion H1. rewrite e in *. exists w'. split; auto.
  assert (y ∹ w' ⋲ (E & (y ∶ w'))) by
    (apply binds_concat_r; apply binds_single; auto).
  auto.
  apply IHE in H1. destruct H1. exists x0. destruct H0.
  split; auto.
  assert (x ∹ x0 ⋲ (E & (y ∶ w'))).
  apply binds_concat_l; auto. apply notin_single; auto. auto.
Qed.

Lemma binds_update_one_notin : forall x v y w F,
  x ∹ v ⋲ F ->
  x <> y ->
  x ∹ v ⋲ (update_one F y w).
Proof.
  intros. induction F as [ | (z, w') ]. inversion H. simpl.
  destruct (eq_keys_dec y z).
  unfold binds in *; simpl in *.
  destruct (eq_keys_dec x z). rewrite <- e0 in *. elim H0; auto.
  auto.
  unfold binds in *; simpl in *.
  destruct (eq_keys_dec x z). auto. auto.
Qed.

Lemma binds_update_notin : forall x v F G,
  x ∹ v ⋲ F ->
  x ∉ G ->
  x ∹ v ⋲ (F ::= G).
Proof.
  intros. induction G as [ | (y, w) ]; simpl; auto.
  assert (x ∉ G & y ∶ w) by auto. clear H0. apply notin_concat_inv in H1.
  destruct H1. apply notin_single_inv in H1.
  apply binds_update_one_notin; auto.
Qed.

Lemma binds_update_one_self : forall x v F,
  x ∈ F ->
  x ∹ v ⋲ (update_one F x v).
Proof.
  induction F as [ | (y, w) ]; intros. inversion H. simpl.
  destruct (eq_keys_dec x y).
  rewrite e in *; simpl in *.
  unfold binds; simpl. apply eq_keys_true.
  unfold binds; simpl. rewrite eq_keys_false; auto.
  assert (x ∈ F & y ∶ w) by auto. clear H.
  apply belongs_concat_inv in H0. destruct H0.
  apply IHF in H; auto.
  apply belongs_single_inv in H. contradiction.
Qed.

Lemma binds_update_self : forall x v E,
  x ∈ E ->
  x ∹ v ⋲ (E ::= (x ∶ v)).
Proof. apply binds_update_one_self. Qed.

Lemma binds_update_one_in : forall x y v w F,
  x <> y ->
  x ∹ v ⋲ F ->
  x ∹ v ⋲ update_one F y w.
Proof.
  intros. induction F as [ | (y', w') ]. inversion H0.
  assert (x ∹ v ⋲ (F & y' ∶ w')) by auto. clear H0.
  apply binds_concat_inv in H1.
  destruct H1.
  apply binds_single_inv in H0. destruct H0. rewrite H0, H1 in *.
  simpl. rewrite eq_keys_false; auto.
  assert (y' ∹ w' ⋲ (update_one F y w & y' ∶ w')) by
    (apply binds_concat_r; apply binds_single; auto). auto.
  destruct H0. apply notin_single_inv in H0.
  simpl. destruct (eq_keys_dec y y').
  assert (x ∹ v ⋲ (F & y' ∶ w)).
  apply binds_concat_l; auto. apply notin_single; auto. auto.
  assert (x ∹ v ⋲ (update_one F y w & y' ∶ w')).
  apply binds_concat_l; auto. apply notin_single; auto. auto.
Qed.

Lemma binds_update_in : forall x v F G,
  x ∈ F ->
  x ∹ v ⋲ G ->
  x ∹ v ⋲ (F ::= G).
Proof.
  intros. induction G as [ | (y, w) ]; simpl; auto.
  inversion H0.
  assert (x ∹ v ⋲ (G & y ∶ w)) by auto. clear H0.
  apply binds_concat_inv in H1. destruct H1.
  apply binds_single_inv in H0. destruct H0. rewrite H0, H1 in *.
  apply (belongs_update y F G) in H. apply binds_update_one_self; auto.
  destruct H0. apply notin_single_inv in H0.
  apply binds_update_one_in; auto.
Qed.

Lemma binds_update_one_inv : forall x y v w E,
  x ∹ v ⋲ update_one E y w ->
  (x <> y ∧ x ∹ v ⋲ E) ∨ (x ∈ E ∧ x = y ∧ v = w).
Proof.
  intros. induction E as [ | (y', w') ]; simpl in *.
  apply binds_empty in H. inversion H.
  destruct (eq_keys_dec y y'). rewrite <- e in *. clear y' e.
  assert (x ∹ v ⋲ (E & y ∶ w)) by auto. clear H.
  apply binds_concat_inv in H0. destruct H0.
  apply binds_single_inv in H. destruct H. rewrite H, H0 in *.
  right. split; auto.
  assert (y ∈ (E & y ∶ w')). apply belongs_concat_r.
  apply belongs_single; auto.
  auto.
  destruct H. apply notin_single_inv in H.
  left. split; auto.
  assert (x ∹ v ⋲ (E & y ∶ w')). apply binds_concat_l; auto.
  apply notin_single; auto.
  auto.
  assert (x ∹ v ⋲ (update_one E y w & y' ∶ w')) by auto. clear H.
  apply binds_concat_inv in H0. destruct H0.
  apply binds_single_inv in H. destruct H. rewrite H, H0 in *.
  left. split; auto.
  assert (y' ∹ w' ⋲ (E & y' ∶ w')). apply binds_concat_r; auto.
  apply binds_single; auto. auto.
  destruct H. apply notin_single_inv in H. apply IHE in H0.
  destruct H0; destruct H0.
  left. split; auto.
  assert (x ∹ v ⋲ (E & y' ∶ w')). apply binds_concat_l; auto.
  apply notin_single; auto.
  auto.
  destruct H1. rewrite H1, H2 in *.
  right. split; auto.
  assert (y ∈ (E & y' ∶ w')). apply belongs_concat_l; auto. auto.
Qed.

Lemma binds_update_inv : forall x v F G,
  x ∹ v ⋲ (F ::= G) ->
  (x ∉ G ∧ x ∹ v ⋲ F) ∨ (x ∈ F ∧ x ∹ v ⋲ G).
Proof.
  intros. induction G as [ | (y, w) ]; simpl in *.
  left; split; auto. apply notin_empty.
  apply binds_update_one_inv in H. destruct H; destruct H.
  apply IHG in H0. destruct H0; destruct H0.
  left. split; auto.
  assert (x ∉ (G & y ∶ w)). apply notin_concat; auto.
  apply notin_single; auto. auto.
  right. split; auto.
  assert (x ∹ v ⋲ (G & y ∶ w)). apply binds_concat_l; auto.
  apply notin_single; auto.
  auto.
  destruct H0. rewrite H0, H1 in *.
  right. split; auto. apply belongs_update_inv with G; auto.
  assert (y ∹ w ⋲ (G & y ∶ w)). apply binds_concat_r; auto.
  apply binds_single; auto.
  auto.
Qed.

Lemma binds_remove : forall x y v E,
  x <> y -> x ∹ v ⋲ E ->
  x ∹ v ⋲ (E ∖ {y}).
Proof.
  intros. induction E as [ | (y', w') ]; simpl in *; auto.
  destruct (eq_keys_dec y y'). rewrite <- e in *; clear y' e.
  assert (x ∹ v ⋲ (E & y ∶ w')) by auto. clear H0.
  apply binds_concat_inv in H1. destruct H1.
  apply binds_single_inv in H0. destruct H0; contradiction.
  destruct H0; auto.
  assert (x ∹ v ⋲ (E & y' ∶ w')) by auto. clear H0.
  apply binds_concat_inv in H1. destruct H1.
  apply binds_single_inv in H0. destruct H0. rewrite <- H0, <- H1 in *.
  assert (x ∹ v ⋲ ((E ∖ {y}) & x ∶ v)). apply binds_concat_r.
  apply binds_single; auto.
  auto.
  destruct H0.
  assert (x ∹ v ⋲ ((E ∖ {y}) & y' ∶ w')). apply binds_concat_l; auto. auto.
Qed.

Lemma binds_remove_inv : forall x y v E,
  x <> y -> x ∹ v ⋲ (E ∖ {y}) ->
  x ∹ v ⋲ E.
Proof.
  intros. induction E as [ | (y', w') ]; simpl in *; auto.
  destruct (eq_keys_dec y y'). rewrite e in *.
  assert (x ∹ v ⋲ (E & y' ∶ w')). apply binds_concat_l; auto.
  apply notin_single; auto. auto.
  assert (x ∹ v ⋲ ((E ∖ {y}) & y' ∶ w')) by auto. clear H0.
  apply binds_concat_inv in H1. destruct H1.
  assert (x ∹ v ⋲ (E & y' ∶ w')). apply binds_concat_r; auto. auto.
  destruct H0.
  assert (x ∹ v ⋲ (E & y' ∶ w')). apply binds_concat_l; auto. auto.
Qed.

Lemma binds_all_remove : forall x ys v E,
  ¬ List.In x ys -> x ∹ v ⋲ E ->
  x ∹ v ⋲ (E ∖ ys).
Proof.
  induction ys as [ | y ]; intros; simpl in *; auto.
  assert (y <> x ∧ ¬ List.In x ys). split; auto. destruct H1.
  apply IHys; auto. apply binds_remove; auto.
Qed.

Lemma binds_all_remove_inv : forall x ys v E,
  ¬ List.In x ys -> x ∹ v ⋲ (E ∖ ys) ->
  x ∹ v ⋲ E.
Proof.
  induction ys as [ | y ]; intros; simpl in *; auto.
  assert (y <> x ∧ ¬ List.In x ys). split; auto. destruct H1.
  apply binds_remove_inv with y; auto.
Qed.

Lemma binds_concat_ok_comm : forall x v F G,
  binds x v (F & G) ->
  ok (F & G) ->
  binds x v (G & F).
Proof.
  intros. apply binds_concat_inv in H. destruct H.
  assert (x ∈ G) by (apply binds_belongs with v; auto).
  assert (x ∉ F) by (apply belongs_ok_concat_inv_r with G; auto).
  apply binds_concat_l; auto.
  destruct H. apply binds_concat_r; auto.
Qed.

Lemma binds_dec_exists : forall x E,
  { v | x ∹ v ⋲ E } + { forall v, ¬ x ∹ v ⋲ E }.
Proof.
  intros. unfold binds.
  elim get_dec with x E; intro; [ left | right ]; auto.
  intro. rewrite b. intro. inversion H.
Qed.

Lemma binds_dec : forall x v E,
  (forall w w', { w = w' } + { ¬ w = w' }) ->
  { x ∹ v ⋲ E } + { ¬ x ∹ v ⋲ E }.
Proof.
  intros. elim binds_dec_exists with x E; intro.
  destruct a. elim (X v x0); intro. left; rewrite a; auto.
  right. intro. assert (v = x0) by (apply binds_eq_inv with x E; auto).
  auto.
  right; auto.
Qed.

Properties of all_binds

Lemma all_binds_binds : forall x v E,
  (x ∶ v) ⊏ E ->
  x ∹ v ⋲ E.
Proof.
  unfold all_binds. intros. apply (H x v). apply binds_single; auto.
Qed.

Lemma binds_all_binds : forall x v E,
  x ∹ v ⋲ E ->
  (x ∶ v) ⊏ E.
Proof.
  unfold all_binds. intros. apply binds_single_inv in H0.
  destruct H0; rewrite H0, H1; auto.
Qed.

Lemma all_binds_empty_l : forall E,
  (@empty A ) ⊏ E.
Proof. unfold all_binds. intros. inversion H. Qed.

Lemma all_binds_empty_r : forall E,
  E ⊏ (@empty A ) ->
  E = (@empty A ).
Proof.
  induction E as [ | (x, v) ]; intros; simpl in *; auto.
  unfold all_binds in H.
  assert (x ∹ v ⋲ (@empty A )) by
    (apply H; assert (x ∹ v ⋲ (E & (x ∶ v))) by
      (apply binds_concat_r; apply binds_single; auto); auto).
  inversion H0.
Qed.

Lemma all_binds_single_empty : forall x v,
  (x ∶ v) ⊏ (@empty A ) ->
  False.
Proof.
  intros. apply all_binds_binds in H. apply binds_empty in H; auto.
Qed.

Lemma all_binds_single_single : forall x v y w,
  x = y -> v = w ->
  (x ∶ v) ⊏ (y ∶ w).
Proof.
  intros. rewrite H, H0. apply binds_all_binds. apply binds_single; auto.
Qed.

Lemma all_binds_single_single_inv : forall x v y w,
  (x ∶ v) ⊏ (y ∶ w) ->
  x = y ∧ v = w.
Proof.
  intros. apply all_binds_binds in H. apply binds_single_inv; auto.
Qed.

Lemma all_binds_single_push_inv : forall x v y w E,
  (x ∶ v) ⊏ (E & (y ∶ w)) ->
  (x = y ∧ v = w) ∨ (x <> y ∧ (x ∶ v) ⊏ E).
Proof.
  intros. apply all_binds_binds in H. apply binds_concat_inv in H.
  destruct H. apply binds_single_inv in H. left; auto.
  destruct H. apply notin_single_inv in H.
  apply binds_all_binds in H0. right; auto.
Qed.

Lemma all_binds_single_singles : forall x v y w ys ws,
  x = y -> v = w ->
  (x ∶ v) ⊏ (y :: ys ∷ w :: ws).
Proof. intros. apply binds_all_binds. apply binds_singles; auto. Qed.

Lemma all_binds_single_singles_inv : forall x v y w ys ws,
  (x ∶ v) ⊏ (y :: ys ∷ w :: ws) ->
  (x = y ∧ v = w) ∨ ((x ∶ v) ⊏ (ys ∷ ws)).
Proof.
  intros. apply all_binds_binds in H. apply binds_singles_inv in H.
  destruct H; [ left | right ]; auto. apply binds_all_binds; auto.
Qed.

Lemma all_binds_single_eq_inv : forall x v w E,
  (x ∶ v) ⊏ E -> (x ∶ w) ⊏ E ->
  v = w.
Proof.
  intros. apply all_binds_binds in H. apply all_binds_binds in H0.
  apply binds_eq_inv with x E; auto.
Qed.

Lemma all_binds_singles_singles : forall xs vs ys ws,
  xs = ys -> vs = ws ->
  (xs ∷ vs) ⊏ (ys ∷ ws).
Proof.
  intros. rewrite H, H0. unfold all_binds. intros; auto.
Qed.

Lemma all_binds_concat_r : forall E F G,
  E ⊏ G ->
  E ⊏ (F & G).
Proof.
  intros; unfold all_binds in *; intros.
  apply binds_concat_r; auto.
Qed.

Lemma all_binds_concat_l : forall E F G,
  E ⊏ F ->
  (dom E) ⊄ G ->
  E ⊏ (F & G).
Proof.
  intros; unfold all_binds in *; intros.
  apply binds_concat_l; auto.
  apply binds_belongs in H1. auto.
Qed.

Lemma all_binds_l_concat : forall E F G,
  E ⊏ G -> F ⊏ G ->
  (E & F) ⊏ G.
Proof.
  intros. unfold all_binds in *. intros. apply binds_concat_inv in H1.
  destruct H1; auto. destruct H1. auto.
Qed.

Lemma all_binds_l_concat_inv : forall E F G,
  ok (E & F) ->
  (E & F) ⊏ G ->
  E ⊏ G ∧ F ⊏ G.
Proof.
  intros. unfold all_binds in *.
  split; intros.
  apply H0. apply binds_concat_l; auto.
  apply belongs_ok_concat_inv_l with E; auto.
  apply binds_belongs with v; auto.
  apply H0. apply binds_concat_r; auto.
Qed.

Lemma all_binds_concat_compat : forall E F G,
  E ⊏ F ->
  (E & G) ⊏ (F & G).
Proof.
  intros. induction G as [ | (x, v) ]; simpl in *; auto.
  unfold all_binds. intros.
  assert (x0 ∹ v0 ⋲ ((F & G) & (x ∶ v))); auto.
  assert (x0 ∹ v0 ⋲ ((E & G) & (x ∶ v))) by auto. clear H0.
  apply binds_concat_inv in H1. destruct H1.
  apply binds_concat_r; auto. destruct H0.
  apply binds_concat_l; auto.
Qed.

Lemma all_binds_singles_eq_inv : forall xs vs vs' F,
  List.NoDup xs ->
  length xs = length vs ->
  length xs = length vs' ->
  xs ∷ vs ⊏ F -> xs ∷ vs' ⊏ F ->
  vs = vs'.
Proof.
  induction xs; induction vs; induction vs'; intros; simpl in *; auto.
  inversion H1. inversion H0. inversion H0. inversion H0. inversion H1.
  inversion H0; inversion H1. clear H0 H1. inversion H. clear x l H0 H1 H.
  assert (((xs ∷ vs) & (a ∶ a0)) ⊏ F) by auto. clear H2.
  assert (((xs ∷ vs') & (a ∶ a1)) ⊏ F) by auto. clear H3.
  apply all_binds_l_concat_inv in H. apply all_binds_l_concat_inv in H0.
  destruct H; destruct H0.
  assert (vs = vs') as Heq1 by (apply IHxs with F; auto).
  assert (a0 = a1) as Heq2
    by (apply all_binds_single_eq_inv with a F; auto).
  rewrite Heq1, Heq2; auto.
  apply ok_concat. apply ok_singles; auto.
  apply ok_single. rewrite dom_singles.
  apply all_notin_single; auto. auto.
  rewrite dom_single. apply notin_all_notin.
  split. apply notin_singles; auto. apply all_notin_empty_l.
  apply ok_concat. apply ok_singles; auto.
  apply ok_single. rewrite dom_singles.
  apply all_notin_single; auto. auto.
  rewrite dom_single. apply notin_all_notin.
  split. apply notin_singles; auto. apply all_notin_empty_l.
Qed.

Lemma all_binds_belongs : forall E F,
  E ⊏ F ->
  (dom E) ⊂ F.
Proof.
  unfold all_binds, all_belongs. intros.
  apply belongs_binds in H0. destruct H0. apply H in H0.
  apply binds_belongs with x0; auto.
Qed.

Lemma belongs_all_binds : forall x F,
  x ∈ F ->
  exists v, (x ∶ v) ⊏ F.
Proof.
  intros. unfold all_binds. apply belongs_binds in H. destruct H.
  exists x0. intros. apply binds_single_inv in H0. destruct H0.
  rewrite H0, H1; auto.
Qed.

Lemma all_belongs_all_binds : forall xs F,
  xs ⊂ F ->
  exists vs, (xs ∷ vs) ⊏ F.
Proof.
  induction xs as [ | x ]; intros.
  exists nil; simpl; apply all_binds_empty_l; auto.
  apply all_belongs_belongs in H. destruct H. apply IHxs in H0. destruct H0.
  apply belongs_binds in H. destruct H.
  exists (x1 :: x0). simpl. unfold all_binds. intros. inversion H1.
  destruct (eq_keys_dec x2 x). inversion H3. rewrite e, <- H4; auto.
  auto.
Qed.

Lemma all_binds_map : forall f E F,
  E ⊏ F ->
  map f E ⊏ map f F.
Proof.
  intros. unfold all_binds in *. intros.
  apply binds_map_inv in H0. destruct H0. destruct H0.
  apply H in H0. rewrite H1. apply binds_map. auto.
Qed.

Lemma all_binds_map_inv : forall f E F,
  Image.injective A B f ->
  map f E ⊏ map f F ->
  E ⊏ F.
Proof.
  intros. unfold all_binds in *. intros.
  assert (x ∹ (f v) ⋲ map f E) by (apply binds_map; auto).
  apply H0 in H2. apply binds_map_inv in H2. destruct H2. destruct H2.
  unfold Image.injective in *. apply H in H3. rewrite H3; auto.
Qed.

Lemma all_binds_update_self : forall E F,
  (dom E) ⊂ F ->
  E ⊏ (F ::= E).
Proof.
  intros. unfold all_binds. intros.
  induction E as [ | (y, w) ]. inversion H0.
  simpl.

  simpl in H. apply all_belongs_belongs in H. destruct H.
  assert (x ∹ v ⋲ (E & y ∶ w)) by auto. clear H0.
  apply binds_concat_inv in H2.

  destruct (eq_keys_dec x y). rewrite e in *.
  destruct H2. apply binds_single_inv in H0. destruct H0. rewrite H2 in *.
  apply binds_update_one_self. apply belongs_update; auto.
  destruct H0. apply notin_single_inv in H0. elim H0; auto.

  destruct H2. apply binds_single_inv in H0. destruct H0. contradiction.
  destruct H0. apply IHE in H1; auto. apply binds_update_one_notin; auto.
Qed.

Lemma all_binds_update : forall E F G,
  E ⊏ F ->
  (E ::= G) ⊏ (F ::= G).
Proof.
  intros. unfold all_binds in *. intros.
  apply binds_update_inv in H0. destruct H0; destruct H0.
  apply binds_update_notin; auto.
  apply belongs_binds in H0. destruct H0.
  apply H in H0. apply binds_belongs in H0.
  apply binds_update_in; auto.
Qed.

Lemma all_binds_remove : forall y E F,
  y ∉ E -> E ⊏ F ->
  E ⊏ (F ∖ {y}).
Proof.
  intros. unfold all_binds in *. intros. apply binds_remove; auto.
  apply binds_belongs in H1. apply notin_belongs_neq with E; auto.
Qed.

Lemma all_binds_remove_inv : forall y E F,
  y ∉ E -> E ⊏ (F ∖ {y}) ->
  E ⊏ F.
Proof.
  intros. unfold all_binds in *. intros.
  apply binds_remove_inv with y; auto.
  apply binds_belongs in H1. apply notin_belongs_neq with E; auto.
Qed.

Lemma all_binds_all_remove : forall ys E F,
  ys ⊄ E -> E ⊏ F ->
  E ⊏ (F ∖ ys).
Proof.
  intros. unfold all_binds in *. intros. apply binds_all_remove; auto.
  apply binds_belongs in H1. apply all_notin_belongs_neq with E; auto.
Qed.

Lemma all_binds_all_remove_inv : forall ys E F,
  ys ⊄ E -> E ⊏ (F ∖ ys) ->
  E ⊏ F.
Proof.
  intros. unfold all_binds in *. intros.
  apply binds_all_remove_inv with ys; auto.
  apply binds_belongs in H1. apply all_notin_belongs_neq with E; auto.
Qed.

Lemma all_binds_remove_compat : forall x E F,
  ok E -> ok F ->
  E ⊏ F ->
  E ∖ {x} ⊏ F ∖ {x}.
Proof.
  intros. unfold all_binds in *. intros.
  assert (x0 <> x) by
    (apply belongs_remove_inv with E; auto;
      apply binds_belongs with v; auto).
  apply binds_remove; auto. apply H1.
  apply binds_remove_inv with x; auto.
Qed.

Lemma all_binds_all_remove_compat : forall xs E F,
  ok E -> ok F ->
  E ⊏ F ->
  E ∖ xs ⊏ F ∖ xs.
Proof.
  induction xs as [ | x ]; intros; simpl in *; auto.
  assert (E ∖ {x} ⊏ F ∖ {x}) by (apply all_binds_remove_compat; auto).
  apply IHxs; auto; apply ok_remove; auto.
Qed.

Lemma all_binds_ok_concat_inv : forall E F G,
  ok (E & F) ->
  (E & F) ⊏ G ->
  E ⊏ G ∧ F ⊏ G.
Proof.
  intros; unfold all_binds in *.
  split; intros; apply H0.
  apply binds_concat_l; auto. apply binds_belongs in H1.
  apply belongs_ok_concat_inv_l with E; auto.
  apply binds_concat_r; auto.
Qed.

Lemma all_binds_concat_ok_comm : forall E F G,
  E ⊏ (F & G) ->
  ok (F & G) ->
  E ⊏ (G & F).
Proof.
  intros. unfold all_binds in *. intros.
  apply binds_concat_ok_comm; auto.
Qed.

Lemma all_binds_refl : forall E F,
  E = F ->
  E ⊏ F.
Proof. intros; rewrite H; unfold all_binds; auto. Qed.

Lemma all_binds_anti_sym : forall E F,
  E ⊏ F -> F ⊏ E ->
  E ≍ F.
Proof. unfold eq; auto. Qed.

Lemma all_binds_trans : forall E F G,
  E ⊏ F -> F ⊏ G ->
  E ⊏ G.
Proof. unfold all_binds; intros; auto. Qed.

Lemma all_binds_dec_exists : forall xs F,
  List.NoDup xs ->
  { vs | length xs = length vs ∧ (xs ∷ vs) ⊏ F }
  + { forall vs, length xs = length vs -> ¬ (xs ∷ vs) ⊏ F }.
Proof.
  intros. unfold all_binds. induction xs as [ | x ].

  Focus.
  left. exists nil. split; auto. simpl; intros.
  apply binds_empty in H0. inversion H0.

  assert (~ List.In x xs ∧ List.NoDup xs) as Hnodup by
    (inversion H; auto). clear H.
  destruct Hnodup.
  destruct IHxs; auto.

  Focus.
  destruct s. destruct a.
  elim binds_dec_exists with x F; intro. destruct a.
  left. exists (x1 :: x0). split; simpl; auto. intros.
  assert (x2 ∹ v ⋲ ((xs ∷ x0) & (x ∶ x1))) by auto. clear H3.
  apply binds_concat_inv in H4. destruct H4; auto.
  apply binds_single_inv in H3. destruct H3. rewrite H3, H4 in *; auto.
  destruct H3; auto.

  right. intros. inversion H1.
  apply eq_sym in H3. apply list_length_S in H3. destruct H3. destruct H3.
  rewrite H3 in *; simpl in *.
  intro. apply (b x1). apply (H4 x x1).
  assert (x ∹ x1 ⋲ ((xs ∷ x2) & (x ∶ x1))). apply binds_concat_r.
  apply binds_single; auto. auto.

  Focus.
  right. intros. inversion H1.
  apply eq_sym in H1. apply list_length_S in H1. destruct H1. destruct H1.
  rewrite H1 in *; simpl in *. clear vs H1.
  intro. apply (n x1); auto. intros. apply H1.
  assert (x2 ∹ v ⋲ ((xs ∷ x1) & (x ∶ x0))); auto.
  apply binds_concat_l; auto.
  apply binds_belongs in H2. inversion H3.
  apply belongs_singles_inv in H2; auto.
  apply notin_single. intro. rewrite H4 in *; auto.
Qed.

Lemma all_binds_dec : forall E F,
  ok E ->
  (forall w w', { w = w' } + { ¬ w = w' }) ->
  {E ⊏ F} + {¬ E ⊏ F}.
Proof.
  assert ((forall w w', { w = w' } + { ¬ w = w' }) ->
    forall ws ws', { ws = ws' } + { ¬ ws = ws' }).
  induction ws; induction ws'; auto. right; intro; inversion H.
  right; intro; inversion H. destruct (X a a0); destruct (IHws ws').
  left; rewrite e, e0; auto. right. intro. inversion H; auto.
  right. intro. inversion H; auto. right. intro. inversion H; auto.

  intros. assert (forall ws ws', { ws = ws' } + { ¬ ws = ws' }) by auto.

  assert (List.NoDup (dom E)) by (apply ok_dom_inv; auto).
  elim all_binds_dec_exists with (dom E) F; auto; intro.
  destruct a. destruct a.
  elim (X1 x (img E)); intro. left; rewrite a in *.
  rewrite dom_img_id in *; auto.
  right. intro. rewrite <- (dom_img_id E) in H3.
  assert (x = img E).
  apply all_binds_singles_eq_inv with (dom E) F; auto.
  apply length_dom_img_eq. auto.
  right. intro. apply (b (img E)).
  apply length_dom_img_eq. rewrite dom_img_id; auto.
Qed.

Properties of eq

Lemma eq_refl : forall E F,
  E = F ->
  E ≍ F.
Proof. unfold eq. intro. split; apply all_binds_refl; auto. Qed.

Lemma eq_sym : forall E F,
  E ≍ F ->
  F ≍ E.
Proof. unfold eq; intros; destruct H; split; auto. Qed.

Lemma eq_trans : forall E F G,
  E ≍ F -> F ≍ G ->
  E ≍ G.
Proof.
  unfold eq; intros. destruct H, H0.
  split; apply all_binds_trans with F; auto.
Qed.

Lemma eq_binds : forall x v E F,
  E ≍ F ->
  binds x v E ->
  binds x v F.
Proof. intros. unfold eq in *. destruct H. auto. Qed.

Lemma eq_concat : forall E F G,
  E ≍ F ->
  (E & G) ≍ (F & G).
Proof.
  unfold eq; intros. destruct H. split; apply all_binds_concat_compat; auto.
Qed.

Lemma eq_concat_comm : forall E F,
  ok (E & F) ->
  (E & F) ≍ (F & E).
Proof.
  intros. unfold eq.
  split; apply all_binds_concat_ok_comm; auto.
  auto; apply all_binds_refl; auto.
  apply all_binds_refl; auto. apply ok_concat_comm; auto.
Qed.

Lemma eq_get : forall E F,
  E ≍ F ->
  forall x, get x E = get x F.
Proof.
  intros. unfold eq in H. destruct H.
  unfold all_binds in *. unfold binds in *.
  elim get_dec with x E; elim get_dec with x F; intros.
  destruct a; destruct a0.
  rewrite e, e0. apply H in e0. rewrite e in e0. auto.
  destruct a. apply H in e. rewrite b in e. inversion e.
  destruct a. apply H0 in e. rewrite e in b. inversion b.
  rewrite b, b0; auto.
Qed.

Lemma eq_get_inv : forall E F,
  (forall x, get x E = get x F) ->
  E ≍ F.
Proof.
  intros. unfold eq, all_binds, binds.
  split; intros. rewrite <- H; auto. rewrite H; auto.
Qed.

Lemma eq_map : forall f E F,
  E ≍ F ->
  map f E ≍ map f F.
Proof.
  intros. unfold eq in *. destruct H. split; apply all_binds_map; auto.
Qed.

Lemma eq_map_inv : forall f E F,
  Image.injective A B f ->
  map f E ≍ map f F ->
  E ≍ F.
Proof.
  intros. unfold eq in *. destruct H0.
  split; apply all_binds_map_inv with f; auto.
Qed.

Lemma eq_remove : forall x E F,
  ok E -> ok F ->
  E ≍ F ->
  E ∖ {x} ≍ F ∖ {x}.
Proof.
  intros. unfold eq in *. destruct H1.
  split; apply all_binds_remove_compat; auto.
Qed.

Lemma eq_all_remove : forall xs E F,
  ok E -> ok F ->
  E ≍ F ->
  E ∖ xs ≍ F ∖ xs.
Proof.
  intros. unfold eq in *. destruct H1.
  split; apply all_binds_all_remove_compat; auto.
Qed.

Lemma eq_update : forall E F G,
  E ≍ F ->
  (E ::= G) ≍ (F ::= G).
Proof.
  intros. unfold eq in *. destruct H. split; apply all_binds_update; auto.
Qed.

Lemma eq_belongs : forall x E F,
  E ≍ F ->
  x ∈ E ->
  x ∈ F.
Proof.
  intros. unfold eq in *. destruct H. unfold all_binds in *.
  apply belongs_binds in H0. destruct H0.
  apply H in H0. apply binds_belongs with x0; auto.
Qed.

Lemma eq_all_belongs : forall xs E F,
  E ≍ F ->
  xs ⊂ E ->
  xs ⊂ F.
Proof.
  intros. unfold eq in *. destruct H.
  apply all_binds_belongs in H. unfold all_belongs in *.
  intros. apply H. apply H0; auto.
Qed.

Lemma eq_notin : forall x E F,
  E ≍ F ->
  x ∉ E ->
  x ∉ F.
Proof.
  intros. unfold eq in *. destruct H. unfold all_binds in *.
  intro. apply belongs_binds in H2. destruct H2.
  apply H1 in H2. apply binds_belongs in H2. contradiction.
Qed.

Lemma eq_all_notin : forall xs E F,
  E ≍ F ->
  xs ⊄ E ->
  xs ⊄ F.
Proof.
  intros. unfold all_notin in *. intros. apply H0 in H1.
  apply eq_notin with E; auto.
Qed.

Lemma eq_dec : forall E F,
  (forall w w', { w = w' } + { ¬ w = w' }) ->
  ok E -> ok F ->
  { E ≍ F } + { ¬ E ≍ F }.
Proof.
  intros; unfold eq.
  elim all_binds_dec with E F; elim all_binds_dec with F E; intros; auto;
    right; intro Heq; destruct Heq; contradiction.
Qed.

Lemma update_is_remove_concat : forall x v E,
  x ∈ E ->
  E ::= (x ∶ v) ≍ (E ∖ {x}) & (x ∶ v).
Proof.
  intros. unfold eq. split; unfold all_binds; intros.
  apply binds_update_inv in H0. destruct H0; destruct H0.
  apply binds_concat_l; auto. apply notin_single_inv in H0.
  apply binds_remove; auto.
  apply binds_concat_r; auto.
  apply binds_concat_inv in H0. destruct H0.
  apply binds_single_inv in H0. destruct H0. rewrite H0, H1.
  apply binds_update_self; auto.
  destruct H0. apply binds_update_notin; auto.
  apply binds_remove_inv with x; auto. apply notin_single_inv with v; auto.
Qed.

End Properties.

End Generic_Env_List_Def.

Require Import Generic_Env.

Module Generic_Env_List (Var : Generic_Var) : Generic_Env_Type (Var)
  := Generic_Env_List_Def Var.