Fm_Infrastructure.v

(** Infrastructure lemmas and tactic definitions for Fsub.

    Authors: Edward Lee, Ondrej Lhotak

    This work is based off the POPL'08 Coq tutorial
    authored by: Brian Aydemir and Arthur Chargu\'eraud, with help from
    Aaron Bohannon, Jeffrey Vaughan, and Dimitrios Vytiniotis.

    This file contains a number of definitions, tactics, and lemmas
    that are based only on the syntax of the language at hand.  While
    the exact statements of everything here would change for a
    different language, the general structure of this file (i.e., the
    sequence of definitions, tactics, and lemmas) would remain the
    same.

    Table of contents:
      - #<a href="##fv">Free variables</a>#
      - #<a href="##subst">Substitution</a>#
      - #<a href="##gather_atoms">The "gather_atoms" tactic</a>#
      - #<a href="##properties">Properties of opening and substitution</a>#
      - #<a href="##lc">Local closure is preserved under substitution</a>#
      - #<a href="##nf-properties"> Additional properties of normal forms under opening and substitution</a>#
      - #<a href="##auto">Automation</a>#
      - #<a href="##body">Properties of body_e</a># *)

Require Export Fsub.Fm_Definitions.


(* ********************************************************************** *)
(** * #<a name="fv"></a># Free variables *)

(** In this section, we define free variable functions.  The functions
    [fv_tt] and [fv_te] calculate the set of atoms used as free type
    variables in a type or expression, respectively.  The function
    [fv_ee] calculates the set of atoms used as free expression
    variables in an expression.  Cases involving binders are
    straightforward since bound variables are indices, not names, in
    locally nameless representation. *)

Fixpoint fv_tt (T : typ) {struct T} : atoms :=
  match T with
  | typ_top => {}
  | typ_bvar J => {}
  | typ_fvar X => {{ X }}
  | typ_arrow T1 T2 => (fv_tt T1) `union` (fv_tt T2)
  | typ_all T1 T2 => (fv_tt T1) `union` (fv_tt T2)
  | typ_box T => (fv_tt T)
  | typ_mut M T => (fv_tt T)
  | typ_int T1 T2 => (fv_tt T1) `union` (fv_tt T2)
  | typ_record a T1 => (fv_tt T1)
  end.

Fixpoint fv_te (e : exp) {struct e} : atoms :=
  match e with
  | exp_bvar i => {}
  | exp_fvar x => {}
  | exp_abs V e1  => (fv_tt V) `union` (fv_te e1)
  | exp_app e1 e2 => (fv_te e1) `union` (fv_te e2)
  | exp_tabs V e1 => (fv_tt V) `union` (fv_te e1)
  | exp_tapp e1 V => (fv_tt V) `union` (fv_te e1)
  | exp_let e1 e2 => (fv_te e1) `union` (fv_te e2)
  | exp_box e => (fv_te e)
  | exp_unbox e => (fv_te e)
  | exp_set_box e1 e2 => (fv_te e1) `union` (fv_te e2)
  | exp_ref l => {}
  | exp_seal e => (fv_te e)
  | exp_record r => (fv_te_record r)
  | exp_record_read e a => (fv_te e)
  | exp_record_write e1 a e2 => (fv_te e1) `union` (fv_te e2)
  end
with fv_te_record (r : rec_comp) {struct r} : atoms :=
  match r with
  | rec_empty => {}
  | rec_exp a e r => (fv_te e) `union` (fv_te_record r)
  | rec_ref a l r => (fv_te_record r)
  end.

Fixpoint fv_ee (e : exp) {struct e} : atoms :=
  match e with
  | exp_bvar i => {}
  | exp_fvar x => {{ x }}
  | exp_abs V e1 => (fv_ee e1)
  | exp_app e1 e2 => (fv_ee e1) `union` (fv_ee e2)
  | exp_tabs V e1 => (fv_ee e1)
  | exp_tapp e1 V => (fv_ee e1)
  | exp_let e1 e2 => (fv_ee e1) `union` (fv_ee e2)
  | exp_box e => (fv_ee e)
  | exp_unbox e => (fv_ee e)
  | exp_set_box e1 e2 => (fv_ee e1) `union` (fv_ee e2)
  | exp_ref l => {}
  | exp_seal e => (fv_ee e)
  | exp_record r => (fv_ee_record r)
  | exp_record_read e a => (fv_ee e)
  | exp_record_write e1 a e2 => (fv_ee e1) `union` (fv_ee e2)
  end
with fv_ee_record (r : rec_comp) {struct r} : atoms :=
  match r with
  | rec_empty => {}
  | rec_exp a e r => (fv_ee e) `union` (fv_ee_record r)
  | rec_ref a l r => (fv_ee_record r)
  end.


(* ********************************************************************** *)
(** * #<a name="subst"></a># Substitution *)

(** In this section, we define substitution for expression and type
    variables appearing in types, expressions, and environments.
    Substitution differs from opening because opening replaces indices
    whereas substitution replaces free variables.  The definitions
    below are relatively simple for two reasons.
      - We are using locally nameless representation, where bound
        variables are represented using indices.  Thus, there is no
        need to rename variables to avoid capture.
      - The definitions below assume that the term being substituted
        in, i.e., the second argument to each function, is locally
        closed.  Thus, there is no need to shift indices when passing
        under a binder. *)

Fixpoint subst_tt (Z : atom) (U : typ) (T : typ) {struct T} : typ :=
  match T with
  | typ_top => typ_top
  | typ_bvar J => typ_bvar J
  | typ_fvar X => if X == Z then U else T
  | typ_arrow T1 T2 => typ_arrow (subst_tt Z U T1) (subst_tt Z U T2)
  | typ_all T1 T2 => typ_all (subst_tt Z U T1) (subst_tt Z U T2)
  | typ_box T => typ_box (subst_tt Z U T)
  | typ_mut M T => typ_mut M (subst_tt Z U T)
  | typ_int T1 T2 => typ_int (subst_tt Z U T1) (subst_tt Z U T2)
  | typ_record a T1 => typ_record a (subst_tt Z U T1)
  end.

Fixpoint subst_te (Z : atom) (U : typ) (e : exp) {struct e} : exp :=
  match e with
  | exp_bvar i => exp_bvar i
  | exp_fvar x => exp_fvar x
  | exp_abs V e1 => exp_abs  (subst_tt Z U V)  (subst_te Z U e1)
  | exp_app e1 e2 => exp_app  (subst_te Z U e1) (subst_te Z U e2)
  | exp_tabs V e1 => exp_tabs (subst_tt Z U V)  (subst_te Z U e1)
  | exp_tapp e1 V => exp_tapp (subst_te Z U e1) (subst_tt Z U V)
  | exp_let e1 e2 => exp_let (subst_te Z U e1) (subst_te Z U e2)
  | exp_box e => exp_box (subst_te Z U e)
  | exp_unbox e => exp_unbox (subst_te Z U e)
  | exp_set_box e1 e2 => exp_set_box (subst_te Z U e1) (subst_te Z U e2)
  | exp_ref l => exp_ref l
  | exp_seal e => exp_seal (subst_te Z U e)
  | exp_record r => exp_record (subst_te_record Z U r)
  | exp_record_read e a => exp_record_read (subst_te Z U e) a
  | exp_record_write e1 a e2 => exp_record_write (subst_te Z U e1) a (subst_te Z U e2)
  end
with subst_te_record (Z : atom) (U : typ) (r : rec_comp) {struct r} : rec_comp :=
  match r with
  | rec_empty => rec_empty
  | rec_exp a e r => rec_exp a (subst_te Z U e) (subst_te_record Z U r)
  | rec_ref a l r => rec_ref a l (subst_te_record Z U r)
  end.

Fixpoint subst_ee (z : atom) (u : exp) (e : exp) {struct e} : exp :=
  match e with
  | exp_bvar i => exp_bvar i
  | exp_fvar x => if x == z then u else e
  | exp_abs V e1 => exp_abs V (subst_ee z u e1)
  | exp_app e1 e2 => exp_app (subst_ee z u e1) (subst_ee z u e2)
  | exp_tabs V e1 => exp_tabs V (subst_ee z u e1)
  | exp_tapp e1 V => exp_tapp (subst_ee z u e1) V
  | exp_let e1 e2 => exp_let (subst_ee z u e1) (subst_ee z u e2)
  | exp_box e => exp_box (subst_ee z u e)
  | exp_unbox e => exp_unbox (subst_ee z u e)
  | exp_set_box e1 e2 => exp_set_box (subst_ee z u e1) (subst_ee z u e2)
  | exp_ref l => exp_ref l
  | exp_seal e => exp_seal (subst_ee z u e)
  | exp_record r => exp_record (subst_ee_record z u r)
  | exp_record_read e a => exp_record_read (subst_ee z u e) a
  | exp_record_write e1 a e2 => exp_record_write (subst_ee z u e1) a (subst_ee z u e2)
  end
with subst_ee_record (z : atom) (u : exp) (r : rec_comp) {struct r} : rec_comp :=
  match r with
  | rec_empty => rec_empty
  | rec_exp a e r => rec_exp a (subst_ee z u e) (subst_ee_record z u r)
  | rec_ref a l r => rec_ref a l (subst_ee_record z u r)
  end.

Definition subst_tb (Z : atom) (P : typ) (b : binding) : binding :=
  match b with
  | bind_sub T => bind_sub (subst_tt Z P T)
  | bind_typ T => bind_typ (subst_tt Z P T)
  end.


(* ********************************************************************** *)
(** * #<a name="gather_atoms"></a># The "[gather_atoms]" tactic *)

(** The Metatheory and MetatheoryAtom libraries define a number of
    tactics for working with cofinite quantification and for picking
    fresh atoms.  To specialize those tactics to this language, we
    only need to redefine the [gather_atoms] tactic, which returns the
    set of all atoms in the current context.

    The definition of [gather_atoms] follows a pattern based on
    repeated calls to [gather_atoms_with].  The one argument to this
    tactic is a function that takes an object of some particular type
    and returns a set of atoms that appear in that argument.  It is
    not necessary to understand exactly how [gather_atoms_with] works.
    If we add a new inductive datatype, say for kinds, to our
    language, then we would need to modify [gather_atoms].  On the
    other hand, if we merely add a new type, say products, then there
    is no need to modify [gather_atoms]; the required changes would be
    made in [fv_tt]. *)

Ltac gather_atoms ::=
  let A := gather_atoms_with (fun x : atoms => x) in
  let B := gather_atoms_with (fun x : atom => singleton x) in
  let C := gather_atoms_with (fun x : exp => fv_te x) in
  let D := gather_atoms_with (fun x : exp => fv_ee x) in
  let E := gather_atoms_with (fun x : typ => fv_tt x) in
  let F := gather_atoms_with (fun x : env => dom x) in
  constr:(A `union` B `union` C `union` D `union` E `union` F).


(* ********************************************************************** *)
(** * #<a name="properties"></a># Properties of opening and substitution *)

(** The following lemmas provide useful structural properties of
    substitution and opening.  While the exact statements are language
    specific, we have found that similar properties are needed in a
    wide range of languages.

    Below, we indicate which lemmas depend on which other lemmas.
    Since [te] functions depend on their [tt] counterparts, a similar
    dependency can be found in the lemmas.

    The lemmas are split into three sections, one each for the [tt],
    [te], and [ee] functions.  The most important lemmas are the
    following:
      - Substitution and opening commute with each other, e.g.,
        [subst_tt_open_tt_var].
      - Opening a term is equivalent to opening the term with a fresh
        name and then substituting for that name, e.g.,
        [subst_tt_intro].

    We keep the sections as uniform in structure as possible.  In
    particular, we state explicitly strengthened induction hypotheses
    even when there are more concise ways of proving the lemmas of
    interest. *)


(* ********************************************************************** *)
(** ** Properties of type substitution in types *)

(** The next lemma is the strengthened induction hypothesis for the
    lemma that follows, which states that opening a locally closed
    term is the identity.  This lemma is not otherwise independently
    useful. *)

Lemma open_tt_rec_type_aux : forall T j V i U,
  i <> j ->
  open_tt_rec j V T = open_tt_rec i U (open_tt_rec j V T) ->
  T = open_tt_rec i U T.
Proof with congruence || eauto.
  induction T; intros j V i U Neq H; simpl in *; inversion H; f_equal...
  Case "typ_bvar".
    destruct (j === n)... destruct (i === n)...
Qed.

(** Opening a locally closed term is the identity.  This lemma depends
    on the immediately preceding lemma. *)

Lemma open_tt_rec_type : forall T U k,
  type T ->
  T = open_tt_rec k U T.
Proof with auto.
  intros T U k Htyp. revert k.
  induction Htyp; intros k; simpl; f_equal...
  Case "typ_all".
    unfold open_tt in *.
    pick fresh X.
    apply (open_tt_rec_type_aux T2 0 (typ_fvar X))...
Qed.

(** If a name is fresh for a term, then substituting for it is the
    identity. *)

Lemma subst_tt_fresh : forall Z U T,
   Z `notin` fv_tt T ->
   T = subst_tt Z U T.
Proof with auto.
  induction T; simpl; intro H; f_equal...
  Case "typ_fvar".
    destruct (a == Z); subst...
    contradict H; fsetdec.
Qed.

(** Substitution commutes with opening under certain conditions.  This
    lemma depends on the fact that opening a locally closed term is
    the identity. *)

Lemma subst_tt_open_tt_rec : forall T1 T2 X P k,
  type P ->
  subst_tt X P (open_tt_rec k T2 T1) =
    open_tt_rec k (subst_tt X P T2) (subst_tt X P T1).
Proof with auto.
  intros T1 T2 X P k WP. revert k.
  induction T1; intros k; simpl; f_equal...
  Case "typ_bvar".
    destruct (k === n); subst...
  Case "typ_fvar".
    destruct (a == X); subst... apply open_tt_rec_type...
Qed.

(** The next lemma is a direct corollary of the immediately preceding
    lemma---the index is specialized to zero. *)

Lemma subst_tt_open_tt : forall T1 T2 (X:atom) P,
  type P ->
  subst_tt X P (open_tt T1 T2) = open_tt (subst_tt X P T1) (subst_tt X P T2).
Proof with auto.
  intros.
  unfold open_tt.
  apply subst_tt_open_tt_rec...
Qed.

(** The next lemma is a direct corollary of the immediately preceding
    lemma---here, we're opening the term with a variable.  In
    practice, this lemma seems to be needed as a left-to-right rewrite
    rule, when stated in its current form. *)

Lemma subst_tt_open_tt_var : forall (X Y:atom) P T,
  Y <> X ->
  type P ->
  open_tt (subst_tt X P T) Y = subst_tt X P (open_tt T Y).
Proof with congruence || auto.
  intros X Y P T Neq Wu.
  unfold open_tt.
  rewrite subst_tt_open_tt_rec...
  simpl.
  destruct (Y == X)...
Qed.

(** The next lemma states that opening a term is equivalent to first
    opening the term with a fresh name and then substituting for the
    name.  This is actually the strengthened induction hypothesis for
    the version we use in practice. *)

Lemma subst_tt_intro_rec : forall X T2 U k,
  X `notin` fv_tt T2 ->
  open_tt_rec k U T2 = subst_tt X U (open_tt_rec k (typ_fvar X) T2).
Proof with congruence || auto.
  induction T2; intros U k Fr; simpl in *; f_equal...
  Case "typ_bvar".
    destruct (k === n)... simpl. destruct (X == X)...
  Case "typ_fvar".
    destruct (a == X)... contradict Fr; fsetdec.
Qed.

(** The next lemma is a direct corollary of the immediately preceding
    lemma---the index is specialized to zero.  *)

Lemma subst_tt_intro : forall X T2 U,
  X `notin` fv_tt T2 ->
  open_tt T2 U = subst_tt X U (open_tt T2 X).
Proof with auto.
  intros.
  unfold open_tt.
  apply subst_tt_intro_rec...
Qed.


(* ********************************************************************** *)
(** ** Properties of type substitution in expressions *)

(** This section follows the structure of the previous section.  The
    one notable difference is that we require two auxiliary lemmas to
    show that substituting a type in a locally-closed expression is
    the identity. *)

Lemma open_te_rec_expr_aux : forall e j u i P,
  open_ee_rec j u e = open_te_rec i P (open_ee_rec j u e) ->
  e = open_te_rec i P e
with open_te_record_rec_expr_aux : forall e j u i P,
  open_ee_record_rec j u e = open_te_record_rec i P (open_ee_record_rec j u e) ->
  e = open_te_record_rec i P e.
Proof with congruence || eauto.
------
  induction e; intros j u i P H; simpl in *; inversion H; f_equal...
------
  induction e; intros j u i P H; simpl in *; inversion H; f_equal...
Qed.

Lemma open_te_rec_type_aux : forall e j Q i P,
  i <> j ->
  open_te_rec j Q e = open_te_rec i P (open_te_rec j Q e) ->
  e = open_te_rec i P e
with open_te_record_rec_type_aux : forall e j Q i P,
  i <> j ->
  open_te_record_rec j Q e = open_te_record_rec i P (open_te_record_rec j Q e) ->
  e = open_te_record_rec i P e.
Proof.
------
  induction e; intros j Q i P Neq Heq; simpl in *; inversion Heq;
    f_equal; eauto using open_tt_rec_type_aux.
------
induction e; intros j Q i P Neq Heq; simpl in *; inversion Heq;
  f_equal; eauto using open_tt_rec_type_aux.
Qed.

Lemma open_te_rec_expr : forall e U k,
  expr e ->
  e = open_te_rec k U e
with open_te_record_rec_expr : forall e U k,
  record_comp e ->
  e = open_te_record_rec k U e.
Proof.
------
  intros e U k WF. revert k.
  induction WF; intros k; simpl; f_equal; auto using open_tt_rec_type;
  try solve [
    unfold open_ee in *;
    pick fresh x;
    eapply open_te_rec_expr_aux with (j := 0) (u := exp_fvar x);
    auto
  | unfold open_te in *;
    pick fresh X;
    eapply open_te_rec_type_aux with (j := 0) (Q := typ_fvar X);
    auto
  ].
------
  intros e U k WF. revert k.
  induction WF; intros k; simpl; f_equal; auto using open_tt_rec_type.
Qed.

Lemma subst_te_fresh : forall X U e,
  X `notin` fv_te e ->
  e = subst_te X U e
with subst_te_record_fresh : forall X U e,
  X `notin` fv_te_record e ->
  e = subst_te_record X U e.
Proof.
------
  induction e; simpl; intros; f_equal; auto using subst_tt_fresh.
------
  induction e; simpl; intros; f_equal; auto using subst_tt_fresh.
Qed.

Lemma subst_te_open_te_rec : forall e T X U k,
  type U ->
  subst_te X U (open_te_rec k T e) =
    open_te_rec k (subst_tt X U T) (subst_te X U e)
with subst_te_record_open_te_record_rec : forall e T X U k,
  type U ->
  subst_te_record X U (open_te_record_rec k T e) =
    open_te_record_rec k (subst_tt X U T) (subst_te_record X U e). 
Proof.
------
  intros e T X U k WU. revert k.
  induction e; intros k; simpl; f_equal; auto using subst_tt_open_tt_rec.
------
  intros e T X U k WU. revert k.
  induction e; intros k; simpl; f_equal; auto using subst_tt_open_tt_rec.
Qed.

Lemma subst_te_open_te : forall e T X U,
  type U ->
  subst_te X U (open_te e T) = open_te (subst_te X U e) (subst_tt X U T).
Proof with auto.
  intros.
  unfold open_te.
  apply subst_te_open_te_rec...
Qed.

Lemma subst_te_open_te_var : forall (X Y:atom) U e,
  Y <> X ->
  type U ->
  open_te (subst_te X U e) Y = subst_te X U (open_te e Y).
Proof with congruence || auto.
  intros X Y U e Neq WU.
  unfold open_te.
  rewrite subst_te_open_te_rec...
  simpl.
  destruct (Y == X)...
Qed.

Lemma subst_te_intro_rec : forall X e U k,
  X `notin` fv_te e ->
  open_te_rec k U e = subst_te X U (open_te_rec k (typ_fvar X) e)
with subst_te_record_intro_rec : forall X e U k,
  X `notin` fv_te_record e ->
  open_te_record_rec k U e = subst_te_record X U (open_te_record_rec k (typ_fvar X) e).
Proof.
-------
  induction e; intros U k Fr; simpl in *; f_equal;
    auto using subst_tt_intro_rec.
-------
  induction e; intros U k Fr; simpl in *; f_equal;
    auto using subst_tt_intro_rec.
Qed.

Lemma subst_te_intro : forall X e U,
  X `notin` fv_te e ->
  open_te e U = subst_te X U (open_te e X).
Proof with auto.
  intros.
  unfold open_te.
  apply subst_te_intro_rec...
Qed.


(* ********************************************************************** *)
(** ** Properties of expression substitution in expressions *)

(** This section follows the structure of the previous two sections. *)

Lemma open_ee_rec_expr_aux : forall e j v u i,
  i <> j ->
  open_ee_rec j v e = open_ee_rec i u (open_ee_rec j v e) ->
  e = open_ee_rec i u e
with open_ee_record_rec_expr_aux : forall e j v u i,
  i <> j ->
  open_ee_record_rec j v e = open_ee_record_rec i u (open_ee_record_rec j v e) ->
  e = open_ee_record_rec i u e.  
Proof with congruence || eauto.
------
  induction e; intros j v u i Neq H; simpl in *; inversion H; f_equal...
  Case "exp_bvar".
    destruct (j===n)... destruct (i===n)...
------
  induction e; intros j v u i Neq H; simpl in *; inversion H; f_equal...
Qed.

Lemma open_ee_rec_type_aux : forall e j V u i,
  open_te_rec j V e = open_ee_rec i u (open_te_rec j V e) ->
  e = open_ee_rec i u e
with open_ee_record_rec_type_aux : forall e j V u i,
  open_te_record_rec j V e = open_ee_record_rec i u (open_te_record_rec j V e) ->
  e = open_ee_record_rec i u e.
Proof.
------
  induction e; intros j V u i H; simpl; inversion H; f_equal; eauto.
------
  induction e; intros j V u i H; simpl; inversion H; f_equal; eauto.
Qed.

Lemma open_ee_rec_expr : forall u e k,
  expr e ->
  e = open_ee_rec k u e
with open_ee_record_rec_expr : forall u e k,
  record_comp e ->
  e = open_ee_record_rec k u e.
Proof with auto.
------
  intros u e k Hexpr. revert k.
  induction Hexpr; intro k; simpl; f_equal; auto*;
  try solve [
    unfold open_ee in *;
    pick fresh x;
    eapply open_ee_rec_expr_aux with (j := 0) (v := exp_fvar x);
    auto
  | unfold open_te in *;
    pick fresh X;
    eapply open_ee_rec_type_aux with (j := 0) (V := typ_fvar X);
    auto
  ].
------
  intros u e k Hexpr. revert k.
  induction Hexpr; intro k; simpl; f_equal; auto*.  
Qed.

Lemma subst_ee_fresh : forall (x: atom) u e,
  x `notin` fv_ee e ->
  e = subst_ee x u e
with subst_ee_record_fresh : forall (x: atom) u e,
  x `notin` fv_ee_record e ->
  e = subst_ee_record x u e.
Proof with auto.
------
  intros x u e; induction e; simpl; intro H; f_equal...
  Case "exp_fvar".
    destruct (a==x)...
    contradict H; fsetdec.
------
  intros x u e; induction e; simpl; intro H; f_equal...
Qed.

Lemma subst_ee_open_ee_rec : forall e1 e2 x u k,
  expr u ->
  subst_ee x u (open_ee_rec k e2 e1) =
    open_ee_rec k (subst_ee x u e2) (subst_ee x u e1)
with subst_ee_record_open_ee_record_recrec : forall e1 e2 x u k,
  expr u ->
  subst_ee_record x u (open_ee_record_rec k e2 e1) =
    open_ee_record_rec k (subst_ee x u e2) (subst_ee_record x u e1).
Proof with auto.
------
  intros e1 e2 x u k WP. revert k.
  induction e1; intros k; simpl; f_equal...
  Case "exp_bvar".
    destruct (k === n); subst...
  Case "exp_fvar".
    destruct (a == x); subst... apply open_ee_rec_expr...
------
  intros e1 e2 x u k WP. revert k.
  induction e1; intros k; simpl; f_equal...
Qed.

Lemma subst_ee_open_ee : forall e1 e2 x u,
  expr u ->
  subst_ee x u (open_ee e1 e2) =
    open_ee (subst_ee x u e1) (subst_ee x u e2).
Proof with auto.
  intros.
  unfold open_ee.
  apply subst_ee_open_ee_rec...
Qed.

Lemma subst_ee_open_ee_var : forall (x y:atom) u e,
  y <> x ->
  expr u ->
  open_ee (subst_ee x u e) y = subst_ee x u (open_ee e y).
Proof with congruence || auto.
  intros x y u e Neq Wu.
  unfold open_ee.
  rewrite subst_ee_open_ee_rec...
  simpl.
  destruct (y == x)...
Qed.

Lemma subst_te_open_ee_rec : forall e1 e2 Z P k,
  subst_te Z P (open_ee_rec k e2 e1) =
    open_ee_rec k (subst_te Z P e2) (subst_te Z P e1)
with subst_te_record_open_ee_record_rec : forall e1 e2 Z P k,
  subst_te_record Z P (open_ee_record_rec k e2 e1) =
    open_ee_record_rec k (subst_te Z P e2) (subst_te_record Z P e1).
Proof with auto.
------
  induction e1; intros e2 Z P k; simpl; f_equal...
  Case "exp_bvar".
    destruct (k === n)...
------
  induction e1; intros e2 Z P k; simpl; f_equal...
Qed.

Lemma subst_te_open_ee : forall e1 e2 Z P,
  subst_te Z P (open_ee e1 e2) = open_ee (subst_te Z P e1) (subst_te Z P e2).
Proof with auto.
  intros.
  unfold open_ee.
  apply subst_te_open_ee_rec...
Qed.

Lemma subst_te_open_ee_var : forall Z (x:atom) P e,
  open_ee (subst_te Z P e) x = subst_te Z P (open_ee e x).
Proof with auto.
  intros.
  rewrite subst_te_open_ee...
Qed.

Lemma subst_ee_open_te_rec : forall e P z u k,
  expr u ->
  subst_ee z u (open_te_rec k P e) = open_te_rec k P (subst_ee z u e)
with subst_ee_record_open_te_record_rec : forall e P z u k,
  expr u ->
  subst_ee_record z u (open_te_record_rec k P e) = open_te_record_rec k P (subst_ee_record z u e).
Proof with auto.
------
  induction e; intros P z u k H; simpl; f_equal...
  Case "exp_fvar".
    destruct (a == z)... apply open_te_rec_expr...
------
  induction e; intros P z u k H; simpl; f_equal...
Qed.

Lemma subst_ee_open_te : forall e P z u,
  expr u ->
  subst_ee z u (open_te e P) = open_te (subst_ee z u e) P.
Proof with auto.
  intros.
  unfold open_te.
  apply subst_ee_open_te_rec...
Qed.

Lemma subst_ee_open_te_var : forall z (X:atom) u e,
  expr u ->
  open_te (subst_ee z u e) X = subst_ee z u (open_te e X).
Proof with auto.
  intros z X u e H.
  rewrite subst_ee_open_te...
Qed.

Lemma subst_ee_intro_rec : forall x e u k,
  x `notin` fv_ee e ->
  open_ee_rec k u e = subst_ee x u (open_ee_rec k (exp_fvar x) e)
with subst_ee_record_intro_rec : forall x e u k,
  x `notin` fv_ee_record e ->
  open_ee_record_rec k u e = subst_ee_record x u (open_ee_record_rec k (exp_fvar x) e).
Proof with congruence || auto.
------
  induction e; intros u k Fr; simpl in *; f_equal...
  Case "exp_bvar".
    destruct (k === n)... simpl. destruct (x == x)...
  Case "exp_fvar".
    destruct (a == x)... contradict Fr; fsetdec.
------
  induction e; intros u k Fr; simpl in *; f_equal...
Qed.

Lemma subst_ee_intro : forall x e u,
  x `notin` fv_ee e ->
  open_ee e u = subst_ee x u (open_ee e x).
Proof with auto.
  intros.
  unfold open_ee.
  apply subst_ee_intro_rec...
Qed.


(* *********************************************************************** *)
(** * #<a name="lc"></a># Local closure is preserved under substitution *)

(** While these lemmas may be considered properties of substitution, we
    separate them out due to the lemmas that they depend on. *)

(** The following lemma depends on [subst_tt_open_tt_var]. *)

Lemma subst_tt_type : forall Z P T,
  type T ->
  type P ->
  type (subst_tt Z P T).
Proof with auto.
  intros Z P T HT HP.
  induction HT; simpl...
  Case "type_fvar".
    destruct (X == Z)...
  Case "type_all".
    pick fresh Y and apply type_all...
    rewrite subst_tt_open_tt_var...
Qed.

(** The following lemma depends on [subst_tt_type],
    [subst_te_open_ee_var], and [sbust_te_open_te_var]. *)

Lemma subst_te_expr : forall Z P e,
  expr e ->
  type P ->
  expr (subst_te Z P e)
with subst_te_record_comp : forall Z P e,
  record_comp e ->
  type P ->
  record_comp (subst_te_record Z P e).
Proof with eauto using subst_tt_type.
------
  intros Z P e He Hp.
  induction He; simpl; auto using subst_tt_type;
  try solve [
    econstructor;
    try instantiate (1 := L `union` singleton Z);
    intros;
    try rewrite subst_te_open_ee_var;
    try rewrite subst_te_open_te_var;
    instantiate;
    eauto using subst_tt_type
  ].
------
  intros Z P e He Hp.
  induction He; simpl; auto using subst_tt_type...
Qed.

(** The following lemma depends on [subst_ee_open_ee_var] and
    [subst_ee_open_te_var]. *)

Lemma subst_ee_expr : forall z e1 e2,
  expr e1 ->
  expr e2 ->
  expr (subst_ee z e2 e1)
with subst_ee_record_expr : forall z e1 e2,
  record_comp e1 ->
  expr e2 ->
  record_comp (subst_ee_record z e2 e1).
Proof with auto.
------
  intros z e1 e2 He1 He2.
  induction He1; simpl; auto;
  try solve [
    econstructor;
    try instantiate (1 := L `union` singleton z);
    intros;
    try rewrite subst_ee_open_ee_var;
    try rewrite subst_ee_open_te_var;
    instantiate;
    auto
  ].
  Case "expr_var".
    destruct (x == z)...
------
  intros z e1 e2 He1 He2.
  induction He1; simpl; auto.
Qed.


(* *********************************************************************** *)
(** * #<a name="body"></a># Properties of [body_e] *)

(** The two kinds of facts we need about [body_e] are the following:
      - How to use it to derive that terms are locally closed.
      - How to derive it from the facts that terms are locally closed.

    Since we use it only in the context of [exp_let] and [exp_sum]
    (see the definition of reduction), those two constructors are the
    only ones we consider below. *)

Lemma expr_let_from_body : forall e1 e2,
  expr e1 ->
  body_e e2 ->
  expr (exp_let e1 e2).
Proof.
  intros e1 e2 H [J1 J2].
  pick fresh y and apply expr_let; auto.
Qed.

Lemma body_from_expr_let : forall e1 e2,
  expr (exp_let e1 e2) ->
  body_e e2.
Proof.
  intros e1 e2 H.
  unfold body_e.
  inversion H; eauto.
Qed.

Lemma open_ee_body_e : forall e1 e2,
  body_e e1 -> expr e2 -> expr (open_ee e1 e2).
Proof.
  intros e1 e2 [L H] J.
  pick fresh x.
  rewrite (subst_ee_intro x); auto using subst_ee_expr.
Qed.


Lemma open_tt_rec_fresh : forall S T X k,
  X `notin` fv_tt S ->
  X `notin` fv_tt T ->
  (open_tt_rec k X S = open_tt_rec k X T) ->
  S = T.
Proof with eauto; try solve fsetdec.
  intros * FrS FrT Eq.
  generalize dependent k.
  dependent induction S; dependent induction T; simpl;
    intros k Eq; try autodestruct_if; eauto; inversion Eq; subst;
    simpl fv_tt in *; try solve [fsetdec]; try solve [f_equal; eauto].
Qed.

Lemma record_dom_subst_ee_fresh : forall a x u r,
  a `notin` record_dom r ->
  a `notin` record_dom (subst_ee_record x u r).
Proof with eauto.
  intros.
  dependent induction r; simpl record_dom in *; simpl subst_ee_record in *...
Qed.

Lemma record_dom_subst_te_fresh : forall a X U r,
  a `notin` record_dom r ->
  a `notin` record_dom (subst_te_record X U r).
Proof with eauto.
  intros.
  dependent induction r; simpl record_dom in *; simpl subst_te_record in *...
Qed.

(* *********************************************************************** *)
(** * #<a name="nf-properties"></a># Normal forms and opening/substitution *)

Lemma merge_mutability_open_tt_rec : forall k (X : atom) T m,
  merge_mutability (open_tt_rec k X T) m =
    open_tt_rec k X (merge_mutability T m).
Proof with eauto; try fold open_tt_rec; try fold merge_mutability; try congruence.
  intros k X T m...
  generalize dependent k...
  induction T; intros k; try solve [split; simpl; eauto]...
  - unfold open_tt_rec, merge_mutability...
    destruct (k == n); subst...
  - unfold open_tt_rec, merge_mutability; subst...
Qed.

Lemma normal_form_open_tt_rec : forall k (X : atom) T,
  normal_form_typing (open_tt_rec k X T) = open_tt_rec k X (normal_form_typing T).
Proof with eauto using merge_mutability_open_tt_rec; try fold open_tt_rec normal_form_typing; try congruence.
  intros k X T...
  generalize dependent k.
  induction T; intros k; subst; try solve [split; simpl; eauto];
    try solve
      [unfold open_tt_rec, normal_form_typing; 
      eauto using merge_mutability_open_tt_rec; 
      repeat fold open_tt_rec;
      repeat fold normal_form_typing; try congruence ]...
  - unfold open_tt_rec, normal_form_typing...
    destruct (k == n); subst...
  - unfold open_tt_rec, normal_form_typing...
    rewrite IHT...
Qed.

Lemma normal_form_open_tt : forall (X : atom) T,
  normal_form_typing (open_tt T X) = open_tt (normal_form_typing T) X.
Proof with eauto using normal_form_open_tt_rec.
  intros...
Qed.

Lemma open_tt_normal_equal_rec : forall T L k,
  (forall X, X `notin` L -> open_tt_rec k X T = normal_form_typing (open_tt_rec k X T)) ->
  T = normal_form_typing T.
Proof with eauto;
  try repeat fold merge_mutability in *; try repeat fold normal_form_typing in *.
  intros.
  generalize dependent k.
  induction T; intros k H; subst; simpl...
  - f_equal...
    + apply (IHT1 k)...
      intros X Fr.
      specialize (H X Fr)...
      unfold open_tt_rec in H; fold open_tt_rec in H...
      inversion H...
    + apply (IHT2 k)...
      intros X Fr.
      specialize (H X Fr)...
      unfold open_tt_rec in H; fold open_tt_rec in H...
      inversion H...
  - f_equal...
    + apply (IHT1 k)...
      intros X Fr.
      specialize (H X Fr)...
      unfold open_tt_rec in H; fold open_tt_rec in H...
      inversion H...
    + apply (IHT2 (S k))...
      intros X Fr.
      specialize (H X Fr)...
      unfold open_tt_rec in H; fold open_tt_rec in H...
      inversion H...
  - f_equal...
    apply (IHT k)...
    intros X Fr.
    specialize (H X Fr)...
    unfold open_tt_rec in H; fold open_tt_rec in H...
    inversion H...
  - pick fresh X for (L `union` (fv_tt (merge_mutability (normal_form_typing T) m))
      `union` fv_tt (typ_mut m T)).
    specialize (H X ltac:(eauto))...
    rewrite normal_form_open_tt_rec in H.
    eapply open_tt_rec_fresh...
  - f_equal...
    + apply (IHT1 k)...
      intros X Fr.
      specialize (H X Fr)...
      unfold open_tt_rec in H; fold open_tt_rec in H...
      inversion H...
    + apply (IHT2 k)...
      intros X Fr.
      specialize (H X Fr)...
      unfold open_tt_rec in H; fold open_tt_rec in H...
      inversion H...
  - f_equal...
    apply (IHT k)...
    intros X Fr.
    specialize (H X Fr)...
    unfold open_tt_rec in H; fold open_tt_rec in H...
    inversion H...   
Qed.

(* *********************************************************************** *)
(** * #<a name="auto"></a># Automation *)

(** We add as hints the fact that local closure is preserved under
    substitution.  This is part of our strategy for automatically
    discharging local-closure proof obligations. *)

#[export] Hint Resolve subst_tt_type subst_te_expr subst_ee_expr : core.

(** We also add as hints the lemmas concerning [body_e]. *)

#[export] Hint Resolve expr_let_from_body body_from_expr_let : core.
#[export] Hint Resolve open_ee_body_e : core.

(** When reasoning about the [binds] relation and [map], we
    occasionally encounter situations where the binding is
    over-simplified.  The following hint undoes that simplification,
    thus enabling [Hint]s from the MetatheoryEnv library. *)

#[export] Hint Extern 1 (binds _ (?F (subst_tt ?X ?U ?T)) _) =>
  unsimpl (subst_tb X U (F T)) : core.

#[export] Hint Resolve record_dom_subst_ee_fresh : core.
#[export] Hint Resolve record_dom_subst_te_fresh : core.