(***************************************************************************
* Generic Environments for Programming Language Metatheory                 *
* Brian Aydemir & Arthur Charguéraud, July 2007, Coq v8.1                  *
***************************************************************************)

Set Implicit Arguments.
Require Import LibTactics List Decidable
  Metatheory_Var Metatheory_Fresh Metatheory_Tactics.

(* ********************************************************************** *)
(** * Module type of an implementation of environments *)

Module Type EnvType.

(* ---------------------------------------------------------------------- *)
(** ** Definition *)

Parameter env : Type -> Type.

Section Definitions.
Variable A B : Type.

Parameter empty : env A.
Parameter single : var -> A -> env A.
Parameter concat : env A -> env A -> env A.

Parameter to_list : env A -> list (var * A).
Parameter dom : env A -> vars.
Parameter map : (A -> B) -> env A -> env B.
Parameter map_keys : (var -> var) -> env A -> env A.
Parameter get : var -> env A -> option A.

End Definitions.

Implicit Arguments empty [A].


(* ---------------------------------------------------------------------- *)
(** ** Notations *)

(** [x ~ a] is the notation for a singleton environment mapping x to a. *)

Notation "x ~ a" := (single x a)
  (at level 63, left associativity) : env_scope.

(** [E & F] is the notation for concatenation of E and F. *)

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

(** [x # E] to be read x fresh from E captures the fact that 
    x is unbound in E . *)

Notation "x '#' E" := (x \notin (dom E)) (at level 67) : env_scope.

Bind Scope env_scope with env.
Delimit Scope env_scope with env.
Open Local Scope env_scope.


(* ---------------------------------------------------------------------- *)
(** ** Properties *)

Section Properties.
Variable A B : Type.
Implicit Types k x : var.
Implicit Types v : A.
Implicit Types E F G : env A.
Implicit Types f : A -> B.
Implicit Types r : var -> var.

Parameter env_ind : forall (P : env A -> Prop),
  (P empty) ->
  (forall E x v, P E -> P (E & x ~ v)) ->
  (forall E, P E).

Parameter to_list_isomorphism : forall E F,
  to_list E = to_list F -> E = F.

Parameter to_list_empty :
  to_list (@empty A) = nil.
Parameter to_list_single : forall x v,
  to_list (x ~ v) = (x,v)::nil.
Parameter to_list_concat : forall E F,
  to_list (E & F) = to_list F ++ to_list E.

Parameter dom_empty :
  dom (@empty A) = {}.
Parameter dom_single : forall x v,
  dom (x ~ v) = {{x}}.
Parameter dom_concat : forall E F,
  dom (E & F) = dom E \u dom F.

Parameter map_empty : forall f,
  map f empty = empty.
Parameter map_single : forall f x v,
  map f (x ~ v) = (x ~ f v).
Parameter map_concat : forall f E F,
  map f (E & F) = map f E & map f F.

Parameter map_keys_empty : forall r,
  map_keys r (@empty A) = empty.
Parameter map_keys_single : forall r x v,
  map_keys r (x ~ v) = (r x ~ v).
Parameter map_keys_concat : forall r E F,
  map_keys r (E & F) = map_keys r E & map_keys r F.

Parameter get_empty : forall k,
  get k (@empty A) = None.
Parameter get_single : forall k x v,
  get k (x ~ v) = if eq_var_dec k x 
                    then Some v 
                    else None.
Parameter get_concat : forall k E F,
  get k (E & F) = match get k F with 
                  | None => get k E 
                  | Some v => Some v 
                  end.

End Properties.

End EnvType.




(* ********************************************************************** *)
(** * Implementation of environments with lists *)
 
Module EnvList : EnvType.

(* ---------------------------------------------------------------------- *)
(** ** Definitions *)

Definition env (A:Type) := list (var * A).

Section Definitions.

Variable A B : Type.
Implicit Types k x : var.
Implicit Types v : A.
Implicit Types E F G : env A.
Implicit Types f : A -> B.
Implicit Types r : var -> var.

Definition empty : env A := nil.
Definition single x v := (x,v)::nil.
Definition concat E F := F ++ E.

Definition to_list E := E.

Fixpoint dom (E : env A) : vars :=
  match E with
  | nil => {}
  | (x,_) :: E' => {{x}} \u (dom E')
  end.

Fixpoint map (f : A -> B) (E : env A) {struct E} : env B :=
  match E with
  | nil => nil
  | (x,v) :: E' => (x, f v) :: map f E'
  end.

Fixpoint map_keys (r : var -> var) (E : env A) {struct E} : env A :=
  match E with
  | nil => nil
  | (x,v) :: E' => (r x, v) :: map_keys r E'
  end.

Fixpoint get (k : var) (E : env A) {struct E} : option A :=
  match E with
  | nil => None
  | (x,v) :: E' => if eq_var_dec k x then Some v else get k E'
  end.

End Definitions.

Implicit Arguments empty [A].


(* ---------------------------------------------------------------------- *)
(** ** Notations *)

Notation "x ~ a" := (single x a)
  (at level 63, left associativity) : env_scope.
Notation "E & F" := (concat E F) 
  (at level 65, left associativity) : env_scope.
Notation "x '#' E" := (x \notin (dom E)) (at level 67) : env_scope.
Bind Scope env_scope with env.
Delimit Scope env_scope with env.
Open Local Scope env_scope.


(* ---------------------------------------------------------------------- *)
(** ** Properties *)

Section Properties.

Variable A B : Type.
Implicit Types k x : var.
Implicit Types v : A.
Implicit Types E F G : env A.
Implicit Types f : A -> B.
Implicit Types r : var -> var.

Lemma env_ind : forall (P : env A -> Prop),
  (P empty) ->
  (forall E x v, P E -> P (E & x ~ v)) ->
  (forall E, P E).
Proof.
  unfold concat, single. induction E as [|(x,v)]; simpls~.
Qed.

Lemma to_list_isomorphism : forall E F,
  to_list E = to_list F -> E = F.
Proof. auto*. Qed.

Lemma to_list_empty :
  to_list (@empty A) = nil.
Proof. auto. Qed.
Lemma to_list_single : forall x v,
  to_list (x ~ v) = (x,v)::nil.
Proof. auto. Qed.
Lemma to_list_concat : forall E F,
  to_list (E & F) = to_list F ++ to_list E.
Proof.
  intros. gen E. induction F; intros; 
   unfold concat, to_list; simple~.
Qed.

Lemma dom_empty :
  dom (@empty A) = {}.
Proof. auto. Qed.
Lemma dom_single : forall x v,
  dom (x ~ v) = {{x}}.
Proof. intros. unfold single, dom. rewrite~ union_empty_r. Qed.
Lemma dom_concat : forall E F,
  dom (E & F) = dom E \u dom F.
Proof. 
  intros. gen E. induction F as [|(x,v)]; intros; simple~.
  rewrite~ union_empty_r.
  rewrite IHF. rewrite~ union_comm_assoc.
Qed.

Lemma map_empty : forall f,
  map f empty = empty.
Proof. auto. Qed.
Lemma map_single : forall f x v,
  map f (x ~ v) = (x ~ f v).
Proof. auto. Qed.
Lemma map_concat : forall f E F,
  map f (E & F) = map f E & map f F.
Proof. 
  intros. gen E. induction F as [|(x,v)]; intros; simple~.
  rewrite IHF. fequals.
Qed.

Lemma map_keys_empty : forall r,
  map_keys r (@empty A) = empty.
Proof. auto. Qed.
Lemma map_keys_single : forall r x v,
  map_keys r (x ~ v) = (r x ~ v).
Proof. auto. Qed.
Lemma map_keys_concat : forall r E F,
  map_keys r (E & F) = map_keys r E & map_keys r F.
Proof.
  intros. gen E. induction F as [|(x,v)]; intros; simple~.
  rewrite IHF. fequals.
Qed.

Lemma get_empty : forall k,
  get k (@empty A) = None.
Proof. auto. Qed.
Lemma get_single : forall k x v,
  get k (x ~ v) = if k ==x 
                    then Some v 
                    else None.
Proof. auto. Qed.
Lemma get_concat : forall k E F,
  get k (E & F) = match get k F with 
                  | None => get k E 
                  | Some v => Some v 
                  end.
Proof.
  intros. induction F as [|(x,v)]; simpl.
  auto. case_var~.
Qed.

End Properties.

End EnvList.



(* ********************************************************************** *)
(** * Environments *)

Export EnvList.
Open Local Scope env_scope.

(* ---------------------------------------------------------------------- *)
(** ** Additional definitions *)

Section MoreDefinitions.
Variable A : Type.
Implicit Types E F : env A.

(** [environemnt A] is another name for [env A]. *)

Definition environment := env A.

(** Keys and values of an environment. *)

Definition keys E := List.map (@fst _ _) (to_list E).
Definition values E := List.map (@snd _ _) (to_list E).

(** Well-formed environments contains no duplicate bindings. *)

Inductive ok : env A -> Prop :=
  | ok_empty :
      ok empty
  | ok_push : forall E x v,
      ok E -> x # E -> ok (E & x ~ v).

(** An environment contains a binding from x to a iff the most recent
  binding on x is mapped to a *)

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

(** Inclusion of an environment in another one. *)

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

(** Inclusion of an environment in another one. *)

Definition singles (xs : list var) (vs : list A) : env A := 
  List.fold_right (fun p acc =>
    acc & (fst p ~ snd p)) empty (combine xs vs).

(** Computing free variables contained in an environment. *)

Definition fold_vars (fv : A -> vars) (E : env A) :=
  List.fold_right (fun v acc => fv v \u acc) {} (values E).

End MoreDefinitions.

(** [xs ~* vs] is the notation for [single_iter xs vs]. *)

Notation "xs ~* vs" := (singles xs vs)
  (at level 63, left associativity) : env_scope.

Hint Constructors ok.


(* ---------------------------------------------------------------------- *)
(** ** Rewriting tactics *)

Hint Rewrite to_list_empty to_list_single
 to_list_concat : calc_to_list.
Hint Rewrite dom_empty dom_single dom_concat : calc_dom.
Hint Rewrite map_empty map_single map_concat : calc_map.
Hint Rewrite map_keys_empty map_keys_single 
 map_keys_concat : calc_map_keys.
Hint Rewrite get_empty get_single get_concat : calc_get.

Ltac calc_to_list := autorewrite with calc_to_list.



(* ---------------------------------------------------------------------- *)
(** ** Structural properties *)

Ltac false_extended :=
  solve [ intros_all; false ]
  || false.

Section StructProperties.

Variable A : Type.
Implicit Types x : var.
Implicit Types v : A.
Implicit Types E F : env A.

Definition list_equiv := to_list_isomorphism.

Lemma list_equiv_eq : forall E F,
  E = F -> to_list E = to_list F.
Proof. intros. subst~. Qed.

Lemma list_equiv_neq : forall E F,
  E = F -> to_list E <> to_list F -> False.
Proof. intros. subst~. Qed.

Lemma env_case : forall E,
  E = empty \/ exist x v E', E = E' & x ~ v.
Proof. induction E using env_ind; auto*. Qed.

Lemma concat_empty_r : forall E,
  E & empty = E.
Proof. intros. applys list_equiv. calc_to_list. auto. Qed.

Lemma concat_empty_l : forall E,
  empty & E = E.
Proof.
  intros. applys list_equiv. calc_to_list. 
  rewrite~ <- app_nil_end.
Qed.

Lemma concat_assoc : forall E F G,
  E & (F & G) = (E & F) & G.
Proof.
  intros. applys list_equiv. 
  calc_to_list. applys app_ass. 
Qed.

Lemma empty_single_inv : forall x v,
  empty = x ~ v -> False.
Proof.
  introv H. apply (list_equiv_neq H).
  calc_to_list. false_extended. 
Qed.

Lemma empty_concat_inv : forall E F,
  empty = E & F -> empty = E /\ empty = F.
Proof. 
  introv H. generalize (list_equiv_eq H).
  calc_to_list. intros K. skip.
Qed.

Lemma empty_push_inv : forall E x v,
  empty = E & x ~ v -> False.
Proof.
  intros. apply (@empty_single_inv x v). 
  auto* (empty_concat_inv H).
Qed.

Lemma empty_mid_inv : forall E F x v,
  empty = E & x ~ v & F -> False.
Proof.
  intros. destruct (env_case F) as [|[? [? [? ?]]]]; subst.
  rewrite concat_empty_r in H. apply* empty_push_inv.
  rewrite concat_assoc in H. apply* empty_push_inv.
Qed.

Lemma eq_single_inv : forall x1 x2 v1 v2,
  x1 ~ v1 = x2 ~ v2 ->
  x1 = x2 /\ v1 = v2.
Proof. 
  intros. generalize (list_equiv_eq H). calc_to_list.
  intros K. inversions~ K.
Qed.

Lemma eq_push_inv : forall x1 x2 v1 v2 E1 E2,
  E1 & x1 ~ v1 = E2 & x2 ~ v2 -> 
  x1 = x2 /\ v1 = v2 /\ E1 = E2.
Proof.
  intros. generalize (list_equiv_eq H). calc_to_list. 
  intros K. inversions K. auto* list_equiv.
Qed.

End StructProperties.

Hint Rewrite concat_empty_r concat_empty_l concat_assoc : calc_concat.

Tactic Notation "calc_concat" := 
  autorewrite with calc_concat.
Tactic Notation "calc_concat" "in" hyp(H) := 
  autorewrite with calc_concat in H.
Tactic Notation "calc_concat" "in" "*" := 
  autorewrite with calc_concat in *.


(* ---------------------------------------------------------------------- *)
(** ** Extra properties of basic operations map *)

Section BasicProperties.

Variable A : Type.
Implicit Types x : var.
Implicit Types v : A.
Implicit Types E F : env A.

Lemma dom_push : forall x v E,
  dom (E & x ~ v) = {{x}} \u dom E.
Proof.  
  intros. rewrite dom_concat. rewrite dom_single.
  rewrite~ union_comm.
Qed.

Lemma get_push : forall k x v E,
  get k (E & x ~ v) = 
    if k == x 
      then Some v 
      else get k E.
Proof.
  intros. rewrite get_concat. rewrite get_single.
  case_var~.
Qed.

End BasicProperties.



(* ---------------------------------------------------------------------- *)
(** ** Properties of map *)

Section MapProperties.

Variable A : Type.
Implicit Types x : var.
Implicit Types v : A.
Implicit Types E F : env A.

Lemma dom_map : forall (B:Type) (f:A->B) E,
  dom (map f E) = dom E.
Proof.
  induction E using env_ind.
  rewrite map_empty. do 2 rewrite dom_empty. auto.
  rewrite map_concat. rewrite map_single. 
  rewrite_all dom_concat. rewrite_all dom_single. congruence.
Qed.

Lemma concat_assoc_map_push : forall f E F x v,
    E & (map f (F & x ~ v)) = (E & map f F) & x ~ (f v).
Proof.
  intros. rewrite map_concat. rewrite map_single.
  rewrite~ concat_assoc.
Qed.

End MapProperties.

(* ---------------------------------------------------------------------- *)
(** ** Hints *)

Ltac simpl_dom :=
  rewrite_all dom_map in *;
  rewrite_all dom_push in *;  
  rewrite_all dom_concat in *;  
  rewrite_all dom_single in *;
  rewrite_all dom_empty in *.

Hint Extern 1 (_ # _) => simpl_dom; notin_solve.

(* ---------------------------------------------------------------------- *)
(** ** Properties of single_iter *)

Section SinglesProperties.
Variable A B : Type.
Implicit Types x : var. 
Implicit Types v : A. 
Implicit Types xs : list var.
Implicit Types vs : list A.
Implicit Types E F : env A.

(* todo with my own list library, it will be easier *)

Lemma singles_empty : 
  nil ~* nil = (@empty A).
Proof. skip. Qed.

Lemma singles_cons : forall x v xs vs,
  (x::xs) ~* (v::vs) = (xs ~* vs) & (x ~ v).
Proof. skip. Qed.

Lemma singles_one : forall x v,
  (x::nil) ~* (v::nil) = (x ~ v).
Proof. skip. Qed.

Lemma singles_two : forall x1 x2 v1 v2,
  (x1::x2::nil) ~* (v1::v2::nil) = (x2 ~ v2 & x1 ~ v1).
Proof. skip. Qed.

Lemma singles_keys : forall xs vs,
  length xs = length vs ->
  keys (xs ~* vs) = xs.
Proof. skip. Qed.

Lemma singles_values : forall xs vs,
  length xs = length vs ->
  values (xs ~* vs) = vs.
Proof. skip. Qed.

Lemma singles_keys_values : forall E,
  E = keys E ~* values E.
Proof. skip. Qed.

(* todo: rename dom_singles et map_singles, ou alias *)

Lemma singles_dom : forall xs vs,
  length xs = length vs ->
  dom (xs ~* vs) = from_list xs.
Proof. skip. Qed.

Lemma singles_map : forall (f : A -> B) xs vs,
  map f (xs ~* vs) = xs ~* (List.map f vs).
Proof. skip. Qed.

Lemma singles_map_keys : forall f xs vs,
  map_keys f (xs ~* vs) = (List.map f xs) ~* vs.
Proof. skip. Qed.

Lemma singles_concat : forall xs1 xs2 vs1 vs2,
  length xs1 = length vs1 ->
  length xs2 = length vs2 ->
  (xs1 ++ xs2) ~* (vs1 ++ vs2) = (xs2 ~* vs2) & (xs1 ~* vs1).
Proof. skip. Qed.

Lemma singles_ok : forall xs vs E,
  ok E ->
  fresh (dom E) (length xs) xs -> 
  ok (E & xs ~* vs).
Proof. skip. Qed.
(*
  induction xs; simpl; intros. auto.
  destruct H0. destruct Us; simpls. auto.
  rewrite iter_push_cons. rewrite* <- concat_assoc.
*)

End SinglesProperties.


(* ---------------------------------------------------------------------- *)
(** ** Properties of well-formedness and freshness *)

Section OkProperties.

Variable A B : Type.
Implicit Types k x : var.
Implicit Types v : A.
Implicit Types E F : env A.

(** ok on concat  -- todo: inutilisé

Lemma ok_concat : forall E F,
  ok E -> ok F -> disjoint (dom E) (dom F) ->
  ok (E & F).

*)

Lemma ok_push_inv : forall E x v,
  ok (E & x ~ v) -> ok E /\ x # E.
Proof.
  intros. inverts H as H1 H2.
  false (empty_push_inv H1).
  destructs 3 (eq_push_inv H). subst~.
Qed.

Lemma ok_push_inv_ok : forall E x v,
  ok (E & x ~ v) -> ok E.
Proof. introv H. destruct* (ok_push_inv H). Qed.

Lemma ok_concat_inv : forall E F,
  ok (E & F) -> ok E /\ ok F.
Proof.
  induction F using env_ind; calc_concat; introv Ok. auto.
  destruct (ok_push_inv Ok). destruct~ IHF.
Qed.

Lemma ok_concat_singles : forall n xs vs E,
  ok E ->
  fresh (dom E) n xs ->
  ok (E & xs ~* vs).
Proof. skip. Qed.

Lemma ok_concat_inv_l : forall E F,
  ok (E & F) -> ok E.
Proof. introv H. destruct* (ok_concat_inv H). Qed.

Lemma ok_concat_inv_r : forall E F,
  ok (E & F) -> ok F.
Proof. introv H. destruct* (ok_concat_inv H). Qed.

Lemma ok_mid_change : forall E F x v1 v2,
  ok (E & x ~ v1 & F) -> ok (E & x ~ v2 & F).
Proof.
  induction F using env_ind; introv; calc_concat; introv Ok.
  destruct* (ok_push_inv Ok).
  destruct* (ok_push_inv Ok).
Qed.

Lemma ok_middle_inv : forall E F x v,
  ok (E & x ~ v & F) -> x # E.
Proof.
  induction F using env_ind; introv; calc_concat; intros Ok;
   destruct (ok_push_inv Ok). auto. apply* IHF.
Qed.

Lemma ok_remove : forall F E G,
  ok (E & F & G) -> ok (E & G).
Proof.
  induction G using env_ind; calc_concat; introv Ok.
  destruct* (ok_concat_inv Ok).
  destruct* (ok_push_inv Ok).
Qed.

Lemma ok_map : forall E (f : A -> B),
  ok E -> ok (map f E).
Proof. 
  induction E using env_ind; introv;
   autorewrite with calc_map; calc_concat; intros Ok.
  auto. destruct* (ok_push_inv Ok).
Qed.

Lemma ok_concat_map: forall E F (f : A -> A),
  ok (E & F) -> ok (E & map f F).
Proof.
  induction F using env_ind; introv;
   autorewrite with calc_map; calc_concat; intros Ok.
  auto. destruct* (ok_push_inv Ok).
Qed.

End OkProperties.

Implicit Arguments ok_push_inv [A E x v].
Implicit Arguments ok_concat_inv [A E F].
Implicit Arguments ok_remove [A F E G].
Implicit Arguments ok_map [A E f].
Implicit Arguments ok_middle_inv [A E F x v].

(** Automation *)

Hint Resolve ok_middle_inv ok_map.

Hint Extern 1 (ok (?E & ?G)) =>
  match goal with H: ok (E & ?F & G) |- _ =>
    apply (ok_remove H) end.

Hint Extern 1 (ok (?E)) =>
  match goal with H: ok (E & _ ~ _) |- _ =>
    apply (ok_push_inv_ok H) end.

Hint Extern 1 (ok (?E)) =>
  match goal with H: ok (E & _) |- _ =>
    apply (ok_concat_inv_l H) end.

Hint Extern 1 (ok (?E)) =>
  match goal with H: ok (_ & E) |- _ =>
    apply (ok_concat_inv_r H) end.

Hint Extern 1 (ok (_ & ?xs ~* ?vs)) =>
  match goal with H: fresh _ ?n xs |- _ =>
  match type of vs with list ?A =>
    apply (@ok_concat_singles A n)
  end end.


(* ---------------------------------------------------------------------- *)
(** ** Properties of the get function *)

Section GetProperties.
Variable A : Type.
Implicit Types E F : env A.
Implicit Types x : var.
Implicit Types v : A.

Lemma get_some : forall x E,
  x \in dom E -> exists v, get x E = Some v. 
Proof. skip. Qed.

Lemma get_some_inv : forall x v E,
  get x E = Some v -> x \in dom E. 
Proof. skip. Qed.

Lemma get_none : forall x v E,
  x # E -> get x E = None. 
Proof. 
  induction E using env_ind; introv In.
  rewrite~ get_empty.
  rewrite~ get_push. case_var.
    simpl_dom. notin_false. 
    auto.
Qed.

Lemma get_none_inv : forall x E,
  get x E = None -> x # E. 
Proof.
  induction E using env_ind; introv Eq.
  simpl_dom. auto.
  rewrite get_push in Eq. case_var~.
Qed.

End GetProperties.


(* ---------------------------------------------------------------------- *)
(** ** Properties of the binds relation *)

Section BindsProperties.
Variable A B : Type.
Implicit Types E F : env A.
Implicit Types x : var.
Implicit Types v : A.

Lemma binds_get : forall x v E,
  binds x v E -> get x E = Some v.
Proof. auto. Qed.

(** Constructor forms *)

Lemma binds_empty_inv : forall x v,
  binds x v empty -> False.
Proof. 
  unfold binds. introv H. rewrite get_empty in H. false. 
Qed.

Lemma binds_single_eq : forall x v,
  binds x v (x ~ v).
Proof.
  intros. unfold binds. rewrite get_single. case_var~.
Qed.

Lemma binds_single_inv : forall x1 x2 v1 v2,
  binds x1 v1 (x2 ~ v2) ->
  x1 = x2 /\ v1 = v2.
Proof.
  unfold binds. introv H. rewrite get_single in H.
  case_var; inversions~ H. 
Qed.

(* todo: introduce a binds_cases tactic *)

Lemma binds_concat_inv : forall x v E1 E2,
  binds x v (E1 & E2) ->
     (binds x v E2)
  \/ (x # E2 /\ binds x v E1).
Proof. skip. Qed.

Lemma binds_concat_inv_ok : forall x v E1 E2,
  ok (E1 & E2) ->
  binds x v (E1 & E2) ->
     (x # E2 /\ binds x v E1)
  \/ (x # E1 /\ binds x v E2).
Proof. skip. Qed.

Lemma binds_push_inv : forall x1 v1 x2 v2 E,
  binds x1 v1 (E & x2 ~ v2) ->
     (x1 = x2 /\ v1 = v2)
  \/ (x1 <> x2 /\ binds x1 v1 E).
Proof. skip. Qed.

Lemma binds_mid_inv : forall x1 v1 x2 v2 E1 E2,
  binds x1 v1 (E1 & x2 ~ v2 & E2) -> 
  ok (E1 & x2 ~ v2 & E2)->
     (x1 # E1 /\ x1 # E2 /\ x1 = x2 /\ v1 = v2)
  \/ (x1 # E2 /\ x1 <> x2 /\ binds x1 v1 E1)
  \/ (x1 # E1 /\ x1 <> x2 /\ binds x1 v1 E2).
Proof. skip. Qed.

Lemma binds_not_mid_inv : forall x v E1 E2 E3,
  binds x v (E1 & E2 & E3) -> 
  x # E2 ->
  ok (E1 & E2 & E3)->
     (x # E3 /\ binds x v E1)
  \/ (x # E1 /\ binds x v E3).
Proof. skip. Qed.

Lemma binds_map : forall x v (f : A -> B) E,
  binds x v E -> binds x (f v) (map f E).
Proof. skip. Qed.

Lemma binds_keys : forall x v f E,
  binds x v E -> binds (f x) v (map_keys f E).
Proof. skip. Qed.

(** Basic forms *)

Lemma binds_func : forall x v1 v2 E,
  binds x v1 E -> binds x v2 E -> v1 = v2.
Proof. skip. Qed.

Lemma binds_fresh_inv : forall x v E,
  binds x v E -> x # E -> False.
Proof. skip. Qed.

(** Derived forms *)

Lemma binds_single_eq_inv : forall x v1 v2,
  binds x v1 (x ~ v2) ->
  v1 = v2.
Proof. skip. Qed.

Lemma binds_push_neq : forall x1 x2 v1 v2 E,
  binds x1 v1 E -> x1 <> x2 -> binds x1 v1 (E & x2 ~ v2).
Proof. skip. Qed.

Lemma binds_push_eq : forall x v E,
 binds x v (E & x ~ v).
Proof. skip. Qed.

Lemma binds_push_eq_inv : forall x v1 v2 E,
  binds x v1 (E & x ~ v2) -> v1 = v2.
Proof. skip. Qed.

Lemma binds_tail : forall x v E,
  x # E -> binds x v (E & x ~ v).
Proof. skip. Qed.

Lemma binds_concat_left : forall x v E1 E2,
  binds x v E1 ->
  x # E2 ->
  binds x v (E1 & E2).
Proof. skip. Qed.

Lemma binds_concat_left_ok : forall x v E1 E2,
  ok (E1 & E2) ->
  binds x v E1 ->
  binds x v (E1 & E2).
Proof. skip. Qed.

Lemma binds_concat_left_inv : forall x v E1 E2,
  binds x v (E1 & E2) ->
  x # E2 ->
  binds x v E1.
Proof. skip. Qed.

Lemma binds_concat_right : forall x v E1 E2,
  binds x v E2 ->
  binds x v (E1 & E2).
Proof. skip. Qed.

Lemma binds_concat_right_inv : forall x v E1 E2,
  binds x v (E1 & E2) ->
  x # E1 ->
  binds x v E2.
Proof. skip. Qed.

Lemma binds_mid_eq : forall x E1 E2 v,
  x # E2 ->
  binds x v (E1 & x ~ v & E2).
Proof. skip. Qed.

(** Metatheory proof forms *)

(** Interaction between binds and the insertion of bindings.
  In theory we don't need this lemma since it would suffice
  to use the binds_cases tactics, but since weakening is a
  very common operation we provide a lemma for it. *)

Lemma binds_weaken : forall x a E F G,
  binds x a (E & G) -> ok (E & F & G) ->
  binds x a (E & F & G).
Proof. skip. Qed.

(* todo: rename in binds_remove *)

Lemma binds_subst : forall x2 v2 x1 v1 E1 E2,
  binds x1 v1 (E1 & x2 ~ v2 & E2) ->
  x1 <> x2 ->
  binds x1 v1 (E1 & E2).
Proof. skip. Qed.

Lemma binds_substs : forall E2 E1 E3 x v,
  binds x v (E1 & E2 & E3) ->
  x # E2 ->
  binds x v (E1 & E3).
Proof. skip. Qed.

Lemma binds_mid_eq_inv : forall x E1 E2 v1 v2,
  binds x v1 (E1 & x ~ v2 & E2) ->
  ok (E1 & x ~ v2 & E2) ->
  v1 = v2.
Proof. skip. Qed.

End BindsProperties.

Implicit Arguments binds_mid_eq_inv [A x E1 E2 v1 v2].

(*
Implicit Arguments binds_concat_inv [A x a E F].
Hint Resolve binds_head binds_tail.
*)

(* ---------------------------------------------------------------------- *)
(** ** Tactics *)

Tactic Notation "binds_mid" :=
  match goal with H: binds ?x ?v1 (_ & ?x ~ ?v2 & _) |- _ =>
    asserts: (v1 = v2); [ apply (binds_mid_eq_inv H) | subst; clear H ] 
  end.
Tactic Notation "binds_mid" "~" :=
  binds_mid; auto_tilde.
Tactic Notation "binds_mid" "*" :=
  binds_mid; auto_star.

Tactic Notation "binds_push" constr(H) :=
  match type of H with binds ?x1 ?v1 (_ & ?x2 ~ ?v2) =>
    destruct (binds_push_inv H) as [[? ?]|[? ?]]; [ subst x2 v2 | ] 
  end.
Tactic Notation "binds_push" "~" constr(H) :=
  binds_push H; auto_tilde.
Tactic Notation "binds_push" "*" constr(H) :=
  binds_push H; auto_star.


(* ---------------------------------------------------------------------- *)
(** ** Properties of environment inclusion *)

Section ExtendsProperties.
Variable A : Type.
Implicit Types x : var.
Implicit Types v : A.
Implicit Types E F : env A.

Lemma extends_refl : forall E,
  extends E E.
Proof. intros_all~. Qed.

Lemma extends_push : forall E x v, 
  x # E -> extends E (E & x ~ v).
Proof. skip. Qed.

Lemma extends_concat_l : forall E F,
  extends F (E & F).
Proof. skip. Qed.

Lemma extends_concat_r : forall E F,
  disjoint (dom E) (dom F) ->
  extends E (E & F).
Proof. skip. Qed.

Lemma extends_push_reoccur : forall E x v,
  binds x v E -> extends E (E & x ~ v).
Proof. skip. Qed.
  (* intros_all. unfolds binds. simpl. case_var. congruence. auto.*)

End ExtendsProperties.

Hint Resolve extends_refl extends_push.



(* ********************************************************************** *)
(** ** Other tactics (syntactical sugar for tactics) *)

(** Tactic to apply an induction hypothesis modulo a rewrite of 
  the associativity of the environment necessary to handle the
  inductive rules dealing with binders. [apply_ih_bind] is in
  fact just a syntactical sugar for [do_rew concat_assoc (eapply H)] 
  which in turns stands for 
  [rewrite concat_assoc; eapply H; rewrite <- concat_assoc]. *)

Tactic Notation "apply_ih_bind" constr(H) :=
  do_rew concat_assoc (applys H).

Tactic Notation "apply_ih_bind" "*" constr(H) :=
  do_rew* concat_assoc (applys H).

(** Similar as the above, except in the case where there
  is also a map function, so we need to use [concat_assoc_map_push]
  for rewriting. *)

Tactic Notation "apply_ih_map_bind" constr(H) :=
  do_rew concat_assoc_map_push (applys H);
  try solve [ rewrite concat_assoc; reflexivity ].

Tactic Notation "apply_ih_map_bind" "*" constr(H) :=
  do_rew* concat_assoc_map_push (applys H);
  try solve [ rewrite concat_assoc; reflexivity ].  

(** [apply_empty] applies a lemma of the form "forall E:env, P E"
    in the particular case where E is empty. The tricky step is
    the simplification of "P empty" before the "apply" tactic is
    called, and this is necessary for Coq to recognize that the
    lemma indeed applies. *)

Tactic Notation "specializes_var" hyp(H) :=
  match type of H with 
  | ?P -> ?Q => fail
  | forall _:_, _ => specializes H Vars __
  end.

Tactic Notation "specializes_vars" hyp(H) :=
  repeat (specializes_var H).

Tactic Notation "clean_empty" hyp(H) :=
  repeat (match type of H with context [map ?f empty] => 
    rewrite (map_empty f) in H end);
  repeat (match type of H with context [?E & empty] => 
    rewrite (concat_empty_r E) in H end).

Tactic Notation "apply_empty" constr(H) :=
  let M := fresh "TEMP" in
  lets M: (@H empty);
  (*todo: annoter le type de empty?*)
  specializes_vars M;
  clean_empty M;
  first [ apply M | eapply M | applys M ]; 
  clear M.
Tactic Notation "apply_empty" "~" constr(H) :=
  apply_empty H; auto_tilde.
Tactic Notation "apply_empty" "*" constr(H) :=
  apply_empty H; auto_star.


(* -todo: old implem with list visible
Tactic Notation "apply_empty" constr(H) :=
  applys (@H empty); 
  rewrite_all concat_empty_r.

Tactic Notation "apply_empty" "~" constr(H) :=
  apply_empty H; auto_tilde.
Tactic Notation "apply_empty" "*" constr(H) :=
  apply_empty H; auto_star.
*)



(* ---------------------------------------------------------------------- *)
(* ---------------------------------------------------------------------- *)
(* ---------------------------------------------------------------------- *)

(* MORE


(* Whether bindings are or not in the context is decidable *)

Lemma binds_dec : forall E x a,
  (forall a1 a2 : A, {a1 = a2} + {a1 <> a2}) ->
  decidable (binds x a E).
Proof.
  introv Dec. remember (get x E) as B. symmetry in HeqB.
  unfold binds. destruct B as [a'|].
  destruct (Dec a a'). subst. 
    left*.
    right. intros H. congruence.
  right. intros H. congruence.
Qed.


(* ********************************************************************** *)
(** ** Gathering free variables of the values contained in an
  environment *)


(** Specification of the above function in terms of [bind]. *)

Lemma fv_in_spec : forall (A : Type) (fv : A -> vars) x a (E : env A),
  binds x a E -> (fv a) << (fv_in fv E).
Proof.
  unfold binds; induction E as [|(y,b)]; simpl; intros B.
  false.
  case_var.
    inversions B. apply subset_union_weak_l.
    apply* (@subset_trans (fv_in fv E)). apply subset_union_weak_r.
Qed.


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

Section OpProperties.
Variable A : Type.
Implicit Types E F : env A.
Implicit Types a b : A.

(** Simplification tactics *)

Hint Rewrite 
  concat_empty 
  map_concat
  dom_empty dom_single dom_push dom_cons dom_concat dom_map : rew_env.
  
Hint Rewrite <- concat_assoc : rew_env.

Tactic Notation "simpl_env" :=
  autorewrite with rew_env in *.

Hint Extern 1 (_ # _) => simpl_env; notin_solve.

(** The [env_fix] tactic is used to convert environments
  from [(x,a)::E] to [E & x ~ a]. *)

(* Duplication in first two cases is to work around a Coq bug
   of the change tactic *)

Ltac env_fix_core :=
  let go := try env_fix_core in
  match goal with 
  | H: context [(?x,?a)::?E] |- _ =>
     (   (progress (change ((x,a)::E) with (E & x ~ a) in H))
      || (progress (unsimpl (E & x ~ a) in H))   ); go
  | |- context [(?x,?a)::?E] =>
    (   (progress (change ((x,a)::E) with (E & x ~ a)))
      || (progress (unsimpl (E & x ~ a)))  ); go
  |  H: context [@nil ((var * ?A)%type)] |- _ =>
      progress (change (@nil ((var * A)%type)) with (@empty A) in H); go
  | |- context [@nil ((var * ?A)%type)] => 
     progress (change (@nil ((var * A)%type)) with (@empty A)); go
  end.

Ltac env_fix := try env_fix_core.



(* ********************************************************************** *)
(** ** Tactics *)

Opaque binds.

(** [binds_get H as EQ] produces from an hypothesis [H] of
  the form [binds x a (E & x ~ b & F)] the equality [EQ: a = b]. *)

Tactic Notation "binds_get" constr(H) "as" ident(EQ) :=
  match type of H with binds ?z ?a (?E & ?x ~ ?b & ?F) =>
    let K := fresh in assert (K : ok (E & x ~ b & F)); 
    [ auto | lets EQ: (@binds_mid_eq _ z a b E F H K); clear K ] end.

(** [binds_get H] expects an hypothesis [H] of the form 
  [binds x a (E & x ~ b & F)] and substitute [a] for [b] in the goal. *)

Tactic Notation "binds_get" constr(H) :=
  let EQ := fresh in binds_get H as EQ;
  try match type of EQ with 
  | ?f _ = ?f _ => inversions EQ; clear EQ
  | ?x = ?y => subst x end.

(** [binds_single H] derives from an hypothesis [H] of the form 
  [binds x a (y ~ b)] the equalities [x = y] and [a = b], then
  it substitutes [x] for [y] in the goal or deduce a contradiction
  if [x <> y] can be found in the context. *)

Ltac binds_single H :=
  match type of H with binds ?x ?a (?y ~ ?b) =>
    destruct (binds_single_inv H); 
    try discriminate; try subst y; 
    try match goal with N: ?x <> ?x |- _ =>
      false; apply N; reflexivity end end.

(** [binds_case H as B1 B2] derives from an hypothesis [H] of the form 
  [binds x a (E & F)] two subcases: [B1: binds x a E] (with a freshness
  condition [x # F]) and [B2: binds x a F]. *)

Tactic Notation "binds_case" constr(H) "as" ident(B1) ident(B2) :=
   let Fr := fresh "Fr" in 
   destruct (binds_concat_inv H) as [[Fr B1] | B2].

(** [binds_case H] makes a case analysis on an hypothesis [H] of the form 
  [binds x a E] where E can be constructed using concatenation and
  singletons. It calls [binds_single] when reaching a singleton. *)

Ltac binds_cases H :=
  let go B := clear H; 
    first [ binds_single B | binds_cases B | idtac ] in
  let B1 := fresh "B" in let B2 := fresh "B" in
  binds_case H as B1 B2; simpl_env; [ go B1 | go B2 ].


(** Automation *)

Hint Resolve 
  binds_concat_fresh binds_concat_ok 
  binds_prepend binds_map.


*)