(***************************************************************************
* Preservation and Progress for mini-ML (CBV) - Infrastructure             *
* Arthur Charguéraud, July 2007, Coq v8.1                                  *
***************************************************************************)

Set Implicit Arguments.
Require Import List Metatheory ML_Definitions.


(* move to environment *)

Lemma ok_iter_push : forall (A:Set) n E xs (vs:list A),
  fresh (dom E) n xs ->
  ok E ->
  ok (E & iter_push xs vs).
Proof.
  introv Fr Ok. gen E n vs. induction xs; intros; simpl. auto.  
  destruct vs; simpls. auto. destruct n; destruct Fr.
  rewrite iter_push_cons. rewrite* <- concat_assoc.
Qed.

Hint Resolve ok_iter_push.


(* ====================================================================== *)
(** * Additional Definitions used in the Proofs *)

(* ********************************************************************** *)
(** ** Free Type Variables *)

(** Computing free variables of a list of terms. *)

Definition typ_fv_list :=
  List.fold_right (fun t acc => typ_fv t \u acc) {}.

(** Computing free variables of a type scheme. *)

Definition sch_fv M := 
  typ_fv (sch_type M).


(* ********************************************************************** *)
(** ** Free Term Variables *)

(** Computing free variables of a term. *)

Fixpoint trm_fv (t : trm) {struct t} : vars :=
  match t with
  | trm_bvar i j  => {}
  | trm_fvar x    => {{x}}
  | trm_abs t1    => (trm_fv t1)
  | trm_fix t1    => (trm_fv t1)
  | trm_let t1 t2 => (trm_fv t1) \u (trm_fv t2)
  | trm_match t1 p1 b t2 => (trm_fv t1) \u (trm_fv b) \u (trm_fv t2)
  | trm_app t1 t2 => (trm_fv t1) \u (trm_fv t2)
  | trm_unit      => {}
  | trm_nat n     => {}
  | trm_add       => {}
  | trm_pair t1 t2 => (trm_fv t1) \u (trm_fv t2)
  | trm_inj1 t1   => (trm_fv t1)
  | trm_inj2 t1   => (trm_fv t1)
  | trm_loc l     => {}
  | trm_ref t1    => (trm_fv t1)
  | trm_get t1    => (trm_fv t1)
  | trm_set t1 t2 => (trm_fv t1) \u (trm_fv t2)
  | trm_raise t1    => (trm_fv t1)
  | trm_catch t1 t2 => (trm_fv t1) \u (trm_fv t2)
  end.

(* ********************************************************************** *)
(** ** Free Variables in Environments *)

(** Computing free type variables of the values of an environment. *)

Definition env_fv := 
  fv_in sch_fv.

(** Computing free type variables of the values for store typing. *)

Definition phi_fv := 
  fv_in typ_fv.


(* ********************************************************************** *)
(** ** Type substitution for free names *)

(** Substitution for names for types *)

Fixpoint typ_subst (Z : var) (U : typ) (T : typ) {struct T} : typ :=
  match T with
  | typ_bvar i      => typ_bvar i
  | typ_fvar X      => if X == Z then U else (typ_fvar X)
  | typ_arrow T1 T2 => typ_arrow (typ_subst Z U T1) (typ_subst Z U T2)
  | typ_unit        => typ_unit  
  | typ_nat         => typ_nat  
  | typ_prod T1 T2  => typ_prod (typ_subst Z U T1) (typ_subst Z U T2)
  | typ_sum T1 T2   => typ_sum (typ_subst Z U T1) (typ_subst Z U T2)
  | typ_ref T1      => typ_ref (typ_subst Z U T1) 
  end.

(** Iterated substitution for types  *)

Fixpoint typ_substs (Zs : list var) (Us : list typ) (T : typ)
   {struct Zs} : typ :=
  match Zs, Us with
  | Z::Zs', U::Us' => typ_substs Zs' Us' (typ_subst Z U T)
  | _, _ => T
  end.    

(** Substitution for names for schemes. *)

Definition sch_subst Z U M := 
  Sch (sch_arity M) (typ_subst Z U (sch_type M)).

(** Iterated substitution for schemes. *)

Definition sch_substs Zs Us M := 
  Sch (sch_arity M) (typ_substs Zs Us (sch_type M)).

(* ********************************************************************** *)
(** ** Term substitution for free names *)

(** Computing free variables of a list of terms. *)

Definition trm_fv_list :=
  List.fold_right (fun t acc => trm_fv t \u acc) {}.

(** Substitution for names *)

Fixpoint trm_subst (z : var) (u : trm) (t : trm) {struct t} : trm :=
  match t with
  | trm_bvar i j  => trm_bvar i j
  | trm_fvar x    => if x == z then u else (trm_fvar x)
  | trm_abs t1    => trm_abs (trm_subst z u t1)
  | trm_fix t1    => trm_fix (trm_subst z u t1)
  | trm_let t1 t2 => trm_let (trm_subst z u t1) (trm_subst z u t2)
  | trm_match t1 p1 e t2 => trm_match (trm_subst z u t1) p1 
                               (trm_subst z u e)
                               (trm_subst z u t2)
  | trm_app t1 t2 => trm_app (trm_subst z u t1) (trm_subst z u t2)
  | trm_unit      => trm_unit
  | trm_nat n     => trm_nat n
  | trm_add       => trm_add
  | trm_pair t1 t2 => trm_pair (trm_subst z u t1) (trm_subst z u t2)
  | trm_inj1 t1  => trm_inj1 (trm_subst z u t1) 
  | trm_inj2 t1  => trm_inj2 (trm_subst z u t1) 
  | trm_loc l     => trm_loc l
  | trm_ref t1    => trm_ref (trm_subst z u t1)
  | trm_get t1    => trm_get (trm_subst z u t1)
  | trm_set t1 t2 => trm_set (trm_subst z u t1) (trm_subst z u t2)
  | trm_raise t1    => trm_raise (trm_subst z u t1)
  | trm_catch t1 t2 => trm_catch (trm_subst z u t1) (trm_subst z u t2)
  end.

Notation "[ z ~> u ] t" := (trm_subst z u t) (at level 68).

(** Iterated substitution *)

Fixpoint substs (zs : list var) (us : list trm) (t : trm)
   {struct zs} : trm :=
  match zs, us with
  | z::zs', u::us' => substs zs' us' ([z ~> u]t)
  | _, _ => t
  end.    

(** Predicate caraterizing lists of a given number of terms *)

Definition terms := list_for_n term.

(* ********************************************************************** *)
(** ** Iterated typing *)

(** Iterated typing *)

Inductive typings (E : env) (P : phi) : list trm -> list typ -> Prop :=
  | typings_nil : typings E P nil nil 
  | typings_cons : forall ts Us t U,
      typings E P ts Us ->
      typing E P t U ->
      typings E P (t::ts) (U::Us).



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

(* ********************************************************************** *)
(** ** Instanciation of Tactics *)

Ltac gather_vars :=
  let A := gather_vars_with (fun x : vars => x) in
  let B := gather_vars_with (fun x : var => {{ x }}) in
  let C := gather_vars_with (fun x : env => dom x) in
  let D := gather_vars_with (fun x : trm => trm_fv x) in
  let E := gather_vars_with (fun x : typ => typ_fv x) in
  let F := gather_vars_with (fun x : list trm => trm_fv_list x) in
  let G := gather_vars_with (fun x : list typ => typ_fv_list x) in
  let H := gather_vars_with (fun x : env => env_fv x) in
  let I := gather_vars_with (fun x : sch => sch_fv x) in
  let J := gather_vars_with (fun x : phi => phi_fv x) in
  constr:(A \u B \u C \u D \u E \u F \u G \u H \u I \u J).

Tactic Notation "pick_fresh" ident(x) :=
  let L := gather_vars in (pick_fresh_gen L x).

Tactic Notation "pick_freshes" constr(n) ident(x) :=
  let L := gather_vars in (pick_freshes_gen L n x).

Tactic Notation "apply_fresh" constr(T) :=
  apply_fresh_base_simple T gather_vars.

Tactic Notation "apply_fresh" "*" constr(T) :=
  apply_fresh T; auto*.


(* ********************************************************************** *)
(** ** Automation *)

Hint Constructors type term phi_ok sto_ok pat_typing typing value red typings.

Lemma trm_def_fresh : trm_fv trm_def = {}.
Proof.
  auto.
Qed.
Lemma typ_def_fresh : typ_fv typ_def = {}.
Proof.
  auto.
Qed.

Hint Extern 1 (_ \notin trm_fv trm_def) =>
  rewrite trm_def_fresh.
Hint Extern 1 (_ \notin typ_fv typ_def) =>
  rewrite typ_def_fresh.
Hint Extern 1 (_ \notin typ_fv typ_exn) =>
  rewrite typ_exn_fresh.

Hint Extern 1 (terms _ _) => split; auto.
Hint Extern 1 (types _ _) => split; auto.

(* ====================================================================== *)
(** ** Properties of iterated operator *)
 
Lemma typ_fv_list_map : forall ts1 ts2,
  typ_fv_list (ts1 ++ ts2) = typ_fv_list ts1 \u typ_fv_list ts2.
Proof.
  induction ts1; simpl; intros. 
  rewrite* union_empty_l.
  rewrite IHts1. rewrite* union_assoc.
Qed.

Lemma trm_fv_list_map : forall ts1 ts2,
  trm_fv_list (ts1 ++ ts2) = trm_fv_list ts1 \u trm_fv_list ts2.
Proof.
  induction ts1; simpl; intros. 
  rewrite* union_empty_l.
  rewrite IHts1. rewrite* union_assoc.
Qed.

Lemma typings_concat : forall E P ts1 Us1 ts2 Us2,
  typings E P ts1 Us1 ->
  typings E P ts2 Us2 ->
  typings E P (ts1++ts2) (Us1++Us2).
Proof.
  induction ts1; introv Typ1 Typ2; inversions Typ1; simpl*.
Qed.


(* ====================================================================== *)
(** * Properties of terms *)

(* ********************************************************************** *)
(** ** Properties of substitution *)



(** Substitution for a fresh name is identity. *)

Lemma subst_fresh : forall x t u, 
  x \notin trm_fv t -> 
  [x ~> u] t = t.
Proof.
  intros. induction t; simpls; f_equal*.
  case_var*. notin_contradiction.
Qed.

Lemma subst_fresh_list : forall z u ts,
  z \notin trm_fv_list ts ->
  ts = List.map (trm_subst z u) ts.
Proof.
  induction ts; simpl; intros Fr.
  auto. f_equal. rewrite~ subst_fresh. auto.
Qed.

Lemma subst_fresh_trm_fvars : forall z u xs,
  fresh ({{z}}) (length xs) xs ->
  trm_fvars xs = List.map (trm_subst z u) (trm_fvars xs).
Proof.
  intros. apply subst_fresh_list.
  induction xs; simpls. auto.
    destruct H. notin_simpls; auto. 
Qed.

Lemma substs_fresh : forall xs us t, 
  fresh (trm_fv t) (length xs) xs -> 
  substs xs us t = t.
Proof.
  induction xs; simpl; intros us t Fr.
  auto. destruct us. auto.
  inversions Fr. rewrite* subst_fresh.
Qed.

(** Substitution distributes on the open operation. *)

Lemma subst_open : forall x u t1 t2, term u -> 
  [x ~> u] (t1 ^^ t2) = ([x ~> u]t1) ^^ (List.map (trm_subst x u) t2).
Proof.
  intros. unfold open, opens. simpl. generalize 0.
  induction t1; intros; simpl; f_equal*.
  case_nat*. unfold trm_nth.
   apply list_map_nth. apply* subst_fresh. 
  case_var*. apply* open_rec_term.
Qed.

(** Substitution and open_var for distinct names commute. *)

Lemma subst_open_vars : forall x ys u t, 
  fresh {{x}} (length ys) ys -> 
  term u ->
  ([x ~> u]t) ^ ys = [x ~> u] (t ^ ys).
Proof.
  introv Fr Tu. rewrite* subst_open. 
  unfold trm_fvars. f_equal.
  induction ys; simpls. auto.
  destruct Fr. case_var. 
    notin_contradiction. f_equal*.
Qed.

(** Opening up an abstraction of body t with a term u is the same as opening
  up the abstraction with a fresh name x and then substituting u for x. *)

Lemma substs_intro_ind : forall t xs us vs, 
  fresh (trm_fv t \u trm_fv_list vs \u trm_fv_list us) (length xs) xs -> 
  terms (length xs) us ->
  terms (length vs) vs ->
  t ^^ (vs ++ us) = substs xs us (t ^^ (vs ++ (trm_fvars xs))).
Proof.
  induction xs; simpl; introv Fr Tu Tv; 
   destruct Tu; destruct us; try solve [ contradictions ].
  auto.
  inversions H0. inversions Fr. clear H0 Fr. simpls.
  rewrite list_concat_right.
  forward (IHxs us (vs++t0::nil)) as K; clear IHxs.
    rewrite* trm_fv_list_map.
    auto. 
    split~. inversions Tv. apply* list_forall_concat.
  rewrite K. clear K. 
  f_equal. rewrite~ subst_open. rewrite~ subst_fresh. 
  f_equal. rewrite map_app.
  simpl. case_var; try solve [ contradictions* ].
  rewrite <- list_concat_right. 
  f_equal. apply~ subst_fresh_list.
  f_equal. apply* subst_fresh_trm_fvars.
Qed.

Lemma substs_intro : forall xs t us, 
  fresh (trm_fv t \u trm_fv_list us) (length xs) xs -> 
  terms (length xs) us ->
  t ^^ us = substs xs us (t ^ xs).
Proof.
  intros. apply* (@substs_intro_ind t xs us nil).
Qed.


(* ********************************************************************** *)
(** ** Terms are stable through substitutions *)

(** Terms are stable by substitution *)

Lemma subst_term : forall t z u,
  term u -> term t -> term ([z ~> u]t).
Proof.
  induction 2; simpl*.
  case_var*.
  apply_fresh term_abs. intros y Fr.
   rewrite* subst_open_vars. 
  apply_fresh term_fix. intros y f Fr.
   rewrite* subst_open_vars.
  apply_fresh term_let. auto. intros y Fr.
   rewrite* subst_open_vars.
  apply_fresh* term_match. intros ys Fr.
   rewrite* subst_open_vars.
Qed.

Hint Resolve subst_term.

(** Terms are stable by iterated substitution *)

Lemma substs_terms : forall xs us t,
  terms (length xs) us ->
  term t ->
  term (substs xs us t).
Proof.
  induction xs; destruct us; introv TU TT; simpl; auto.
  inversions TU. simpls. inversions H. inversions* H0.
Qed.

(* Bodys are stable by substitution *)

Lemma subst_bodys : forall z u n t,
  term u -> bodys n t -> bodys n ([z ~> u]t).
Proof.
  introv. intros Wu [L Bt]. exists (L \u {{z}}).
  introv Fr. rewrite~ subst_open_vars.
Qed.

Hint Resolve subst_bodys.


(* ********************************************************************** *)
(** ** Terms are stable through open *)

(** Conversion from locally closed abstractions and bodies *)

Lemma term_abs_to_body : forall t1, 
  term (trm_abs t1) -> bodys 1 t1.
Proof.
  intros. unfold bodys. inversions* H.
  exists L. intros.
  destruct xs; simpl in H0; destruct H0.
  destruct xs; simpl in H2; destruct H2. auto.
Qed.

Lemma body_to_term_abs : forall t1,
  bodys 1 t1 -> term (trm_abs t1).
Proof. 
  destruct 1. apply_fresh* term_abs.
Qed.

Lemma term_fix_to_body : forall t1,
  term (trm_fix t1) -> bodys 2 t1.
Proof.
  intros. unfold bodys. inversions* H. 
  exists L. intros.
  destruct xs; simpl in H0; destruct H0.
  destruct xs; simpl in H2; destruct H2.
  destruct xs; simpl in H3; destruct H3.
  auto.
Qed.

Lemma body_to_term_fix : forall t1,
  bodys 2 t1 -> term (trm_fix t1).
Proof.
   destruct 1. apply_fresh* term_fix.
Qed.

Lemma term_let_to_body : forall t1 t2, 
  term (trm_let t1 t2) -> bodys 1 t2.
Proof.
  intros. unfold bodys. inversions* H.
  exists L. intros.
  destruct xs; simpl in H0; destruct H0.
  destruct xs; simpl in H1; destruct H1. auto.
Qed.

Lemma body_to_term_let : forall t1 t2,
  term t1 -> bodys 1 t2 -> term (trm_let t1 t2).
Proof. 
  destruct 2. apply_fresh* term_let.
Qed.

Lemma term_match_to_body : forall t1 t2 b p, 
  term (trm_match t1 p b t2) -> bodys (pat_arity p) b.
Proof.
  intros. unfold bodys. inversions* H.
Qed.

Lemma body_to_term_match : forall t1 t2 b p,
  term t1 -> term t2 -> bodys (pat_arity p) b -> 
  term (trm_match t1 p b t2).
Proof. 
  destruct 3. apply_fresh* term_match.
Qed.
 
Hint Resolve body_to_term_abs term_abs_to_body
             body_to_term_fix term_fix_to_body
             body_to_term_match
             body_to_term_let.

Hint Extern 1 (bodys (pat_arity ?p) ?e) =>
  match goal with H: context [trm_match ?t1 p e ?t2] |- _ =>
    apply (@term_match_to_body t1 t2) end.

Hint Extern 1 (bodys 1 ?t2) =>
  match goal with H: context [trm_let ?t1 t2] |- _ =>
    apply (@term_let_to_body t1) end.

(** ** Opening a body with a term gives a term *)

Lemma open_terms : forall t us,
  bodys (length us) t ->
  terms (length us) us -> 
  term (t ^^ us).
Proof. 
  introv [L K] WT. pick_freshes (length us) xs. poses Fr' Fr.
  rewrite (fresh_length _ _ _  Fr) in WT, Fr'.
  rewrite~ (@substs_intro xs). apply* substs_terms.
Qed.

Hint Resolve open_terms.

(** The matching function returns a list of terms of the expected length. *)

Lemma pat_match_terms : forall p t ts,
  (pat_match p t) = Some ts -> term t -> 
  terms (pat_arity p) ts.
Proof.
  induction p; simpl; introv EQ TT;
   try solve [ inversions EQ; auto ]; 
   destruct t; inversions EQ; inversions TT; auto*.
  remember (pat_match p1 t1) as K1. symmetry in HeqK1.
   remember (pat_match p2 t2) as K2. symmetry in HeqK2. 
   destruct K1 as [ts1|]; destruct K2 as [ts2|]; try discriminate.
   inversions EQ. unfolds terms. apply* list_for_n_concat.
Qed.

(* ====================================================================== *)
(** * Properties of types *)

(** Open on a type is the identity. *)

Lemma typ_open_type : forall T Us,
  type T -> T = typ_open T Us.
Proof.
  introv W. induction T; simpls; inversions W; f_equal*.
Qed.

(** Substitution for a fresh name is identity. *)

Lemma typ_subst_fresh : forall X U T, 
  X \notin typ_fv T -> 
  typ_subst X U T = T.
Proof.
  intros. induction T; simpls; f_equal*.
  case_var*. notin_contradiction.
Qed.

Lemma typ_subst_fresh_list : forall z u ts,
  z \notin typ_fv_list ts ->
  ts = List.map (typ_subst z u) ts.
Proof.
  induction ts; simpl; intros Fr.
  auto. f_equal. rewrite~ typ_subst_fresh. auto.
Qed.

Lemma typ_subst_fresh_trm_fvars : forall z u xs,
  fresh ({{z}}) (length xs) xs ->
  typ_fvars xs = List.map (typ_subst z u) (typ_fvars xs).
Proof.
  intros. apply typ_subst_fresh_list.
  induction xs; simpls. auto.
    destruct H. notin_simpls; auto. 
Qed.

Lemma typ_substs_fresh : forall xs us t, 
  fresh (typ_fv t) (length xs) xs -> 
  typ_substs xs us t = t.
Proof.
  induction xs; simpl; intros us t Fr.
  auto. destruct us. auto.
  inversions Fr. rewrite* typ_subst_fresh.
Qed.

(** Substitution distributes on the open operation. *)

Lemma typ_subst_open : forall X U T1 T2, type U -> 
  typ_subst X U (typ_open T1 T2) = 
   typ_open (typ_subst X U T1) (List.map (typ_subst X U) T2).
Proof.
  intros. induction T1; intros; simpl; f_equal*.
  apply list_map_nth. apply* typ_subst_fresh. 
  case_var*. apply* typ_open_type.
Qed.

(** Substitution and open_var for distinct names commute. *)

Lemma typ_subst_open_vars : forall X Ys U T, 
  fresh {{X}} (length Ys) Ys -> 
  type U ->
     typ_open_vars (typ_subst X U T) Ys
   = typ_subst X U (typ_open_vars T Ys).
Proof.
  introv Fr Tu. unfold typ_open_vars.
  rewrite* typ_subst_open. f_equal.
  induction Ys; simpls. auto.
  destruct Fr. case_var. 
    notin_contradiction. f_equal*.
Qed.

(** Opening up an abstraction of body t with a term u is the same as opening
  up the abstraction with a fresh name x and then substituting u for x. *)

Lemma typ_substs_intro_ind : forall T Xs Us Vs, 
  fresh (typ_fv T \u typ_fv_list Vs \u typ_fv_list Us) (length Xs) Xs -> 
  types (length Xs) Us ->
  types (length Vs) Vs ->
  typ_open T (Vs ++ Us) = typ_substs Xs Us (typ_open T (Vs ++ (typ_fvars Xs))).
Proof.
  induction Xs; simpl; introv Fr Tu Tv; 
   destruct Tu; destruct Us; try solve [ contradictions ].
  auto.
  inversions H0. inversions Fr. clear H0 Fr. simpls.
  rewrite list_concat_right.
  forward (IHXs Us (Vs++t::nil)) as K; clear IHXs.
    rewrite* typ_fv_list_map.
    auto. 
    split~. inversions Tv. apply* list_forall_concat.  
  rewrite K. clear K. 
  f_equal. rewrite~ typ_subst_open. rewrite~ typ_subst_fresh.
  f_equal. rewrite map_app.
  simpl. case_var; try solve [ contradictions* ].
  rewrite <- list_concat_right. 
  f_equal. apply~ typ_subst_fresh_list.
  f_equal. apply* typ_subst_fresh_trm_fvars.
Qed.

Lemma typ_substs_intro : forall Xs Us T, 
  fresh (typ_fv T \u typ_fv_list Us) (length Xs) Xs -> 
  types (length Xs) Us ->
  (typ_open T Us) = typ_substs Xs Us (typ_open_vars T Xs).
Proof.
  intros. apply* (@typ_substs_intro_ind T Xs Us nil).
Qed.

(** Types are stable by type substitution *)

Lemma typ_subst_type : forall T Z U,
  type U -> type T -> type (typ_subst Z U T).
Proof.
  induction 2; simpl*. case_var*.
Qed.

Hint Resolve typ_subst_type.

(** Types are stable by iterated type substitution *)

Lemma typ_substs_types : forall Xs Us T,
  types (length Xs) Us ->
  type T ->
  type (typ_substs Xs Us T).
Proof.
  induction Xs; destruct Us; simpl; introv TU TT; auto.
  destruct TU. simpls. inversions H. inversions* H0.
Qed.

(** List of types are stable by type substitution *)

Lemma typ_subst_type_list : forall Z U Ts n,
  type U -> types n Ts -> 
  types n (List.map (typ_subst Z U) Ts).
Proof.
  unfold types, list_for_n.
  induction Ts; destruct n; simpl; intros TU [EQ TT]. 
  auto. auto. inversion EQ.
  inversions TT. forward~ (IHTs n) as [K1 K2].
Qed.

(** ** Opening a body with a list of types gives a type *)

Lemma typ_open_types : forall T Us,
  typ_body (length Us) T ->
  types (length Us) Us -> 
  type (typ_open T Us).
Proof. 
  introv [L K] WT. pick_freshes (length Us) Xs. poses Fr' Fr.
  rewrite (fresh_length _ _ _  Fr) in WT, Fr'.
  rewrite~ (@typ_substs_intro Xs). apply* typ_substs_types.
Qed.


(* ====================================================================== *)
(** * Properties of schemes *)

(** Substitution for a fresh name is identity. *)

Lemma sch_subst_fresh : forall X U M, 
  X \notin sch_fv M -> 
  sch_subst X U M = M.
Proof.
  intros. destruct M as [n T]. unfold sch_subst.
  rewrite* typ_subst_fresh.
Qed.

(** Trivial lemma to unfolding definition of [sch_subst] by rewriting. *)

Lemma sch_subst_fold : forall Z U T n,
  Sch n (typ_subst Z U T) = sch_subst Z U (Sch n T).
Proof.
  auto.
Qed. 

(** Distributivity of type substitution on opening of scheme. *)

Lemma sch_subst_open : forall Z U M Us,
   type U ->
    typ_subst Z U (sch_open M Us)
  = sch_open (sch_subst Z U M) (List.map (typ_subst Z U) Us).
Proof.
  unfold sch_open. intros. destruct M. simpl.
  rewrite* <- typ_subst_open.
Qed.

(** Distributivity of type substitution on opening of scheme with variables. *)

Lemma sch_subst_open_vars : forall Z U M Xs,
   fresh ({{Z}}) (length Xs) Xs -> 
   type U ->
    typ_subst Z U (sch_open_vars M Xs)
  = sch_open_vars (sch_subst Z U M) Xs.
Proof.
  unfold sch_open_vars. intros. destruct M.
  rewrite* <- typ_subst_open_vars.
Qed.

(** Schemes are stable by type substitution. *)

Lemma sch_subst_type : forall Z U M,
  type U -> scheme M -> scheme (sch_subst Z U M).
Proof.
  unfold scheme, sch_subst. intros Z U [n T] TU S.
  simpls. destruct S as [L K]. exists (L \u {{Z}}).
  introv Fr. rewrite* typ_subst_open_vars.
Qed.

Hint Resolve sch_subst_type.

(** Scheme arity is preserved by type substitution. *)

Lemma sch_subst_arity : forall X U M, 
  sch_arity (sch_subst X U M) = sch_arity M.
Proof.
  auto.
Qed.

(** ** Opening a scheme with a list of types gives a type *)

Lemma sch_open_types : forall M Us,
  scheme M ->
  types (sch_arity M) Us ->
  type (sch_open M Us).
Proof. 
  unfold scheme, sch_open. intros [n T] Us WB [Ar TU].
  simpls. subst n. apply* typ_open_types.
Qed.

Hint Resolve sch_open_types.


(* ====================================================================== *)
(** * Properties of store *)

Lemma phi_ok_binds : forall P l T,
   phi_ok P -> binds l T P -> type T.
Proof.
  unfolds binds. introv. induction P as [|(l1,t1)]; 
   simpl; env_fix; introv Ok Binds.
  contradictions.
  inversions Ok. case_var.
    inversions* Binds.
    auto.
Qed.

Lemma sto_ok_binds : forall mu l t,
   sto_ok mu -> binds l t mu -> term t.
Proof.
  unfolds binds. introv. induction mu as [|(l1,t1)]; 
   simpl; env_fix; introv Ok Binds.
  contradictions.
  inversions Ok. case_var.
    inversions* Binds.
    auto.
Qed.

Hint Resolve phi_ok_binds sto_ok_binds.


(* ====================================================================== *)
(** * Properties of judgments *)


(* ********************************************************************** *)
(** ** Regularity of relations *)

(** The value predicate only holds on locally-closed terms. *)

Lemma value_regular : forall e,
  value e -> term e.
Proof.
  induction 1; auto*.
Qed.

(** A typing relation is restricted to well-formed objects. *)

(* Helper tactics to name all the hypotheses *)

Tactic Notation "split4" "in" ident(H) :=
  let H1 := fresh in let H2 := fresh in
  let H3 := fresh in let H4 := fresh in
  destruct H as [H1 [H2 [H3 H4]]].

Lemma typing_regular : forall E P e T,
  typing E P e T -> ok E /\ phi_ok P /\ term e /\ type T.
Proof.
  intros. induction H; try solve [ split4* ].
  pick_fresh x. forward~ (H1 x) as K. split4 in K.
   inversions H2. splits*.
   apply_fresh term_abs. intros y Fry. forward* (H1 y) as K2.
  pick_fresh x. pick_fresh f. forward~ (H1 f x) as K. split4 in K.
   inversions H2. inversions H8. splits*.
   apply_fresh term_fix. intros g y Fry. forward* (H1 g y) as K2.
  pick_fresh x. forward~ (H4 x) as K. split4 in K.
   inversions H5. splits*. puts value_regular.
   apply_fresh* term_let. intros y Fry. forward* (H4 y) as K2.
  pick_freshes (pat_arity p) xs. forward~ (H2 xs) as K. split4 in K.
   destruct (ok_concat_inv _ _ H4). splits*.
   apply_fresh* term_match. intros ys Frys. forward* (H2 ys) as K2.
  split4 in IHtyping1. inversions* H4.
  split4 in IHtyping. inversions* H3.
Qed. 

(** A fails relation only holds on pairs of locally-closed terms. *)

Lemma fails_regular : forall t e,
  fails t e -> term t /\ term e.
Proof.
  induction 1; use value_regular.
Qed.

(** A reduction relation only holds only on well-formed objects. *)

Lemma red_regular : forall c c',
  red c c' -> 
     (term (fst c) /\ term (fst c'))
  /\ (sto_ok (snd c) /\ sto_ok (snd c')).
Proof.
  induction 1; simpl; env_fix; use value_regular.
  splits~. forward~ (@pat_match_terms _ _ _ H3) as K.
   rewrite (proj1 K) in H1, K. apply* open_terms.
  use (fails_regular H1).
Qed.

(* ********************************************************************** *)
(** ** Automation for well-formedness *)

(** Automation for reasoning on well-formedness. *)

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

Hint Extern 1 (term ?t) =>
  match goal with
  | H: typing _ _ t _ |- _ => apply (proj43 (typing_regular H))
  | H: red (t,_) _ |- _ => apply (proj41 (red_regular H))
  | H: red _ (t,_) |- _ => apply (proj42 (red_regular H))
  | H: value t |- _ => apply (value_regular H)
  | H: fails t _ |- _ => apply (proj1 (fails_regular H))
  | H: fails _ t |- _ => apply (proj2 (fails_regular H))
  end.

Hint Extern 1 (sto_ok ?mu) =>
  match goal with
  | H: red (_,mu) _ |- _ => apply (proj1 (proj2 (red_regular H)))
  | H: red _ (_,mu) |- _ => apply (proj2 (proj2 (red_regular H)))
  | H: sto_typing _ mu |- _ => apply (proj42 H)
  end.

Hint Extern 1 (phi_ok ?P) =>
  match goal with
  | H: typing _ P _ _ |- _ => apply (proj42 (typing_regular H))
  | H: sto_typing P _ |- _ => apply (proj41 H)
  end.

Hint Extern 1 (type ?T) => match goal with
  | H: typing _ _ _ T |- _ => apply (proj44 (typing_regular H))
  end.