(***************************************************************************
* A tutorial file for STLC in locally nameless style                       *
***************************************************************************)




Set Implicit Arguments.
Require Import LibLN.

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

(* ********************************************************************** *)
(** ** Grammars *)

(** Grammar of types. We have two constructors, one for type variables
    and one for arrow types of the form [T1 -> T2].
*)

Inductive typ : Set :=
  | typ_var   : var -> typ
  | typ_arrow : typ -> typ -> typ.

(** Grammar of pre-terms. We use a locally nameless representation for the
    simply-typed lambda calculus, where bound variables are represented as 
    natural numbers (de Bruijn indices) and free variables are represented as
    atoms. The type [var], defined in the library LibLN_Var, represents
    'names' or 'atoms'. One central assumption is that it is always possible
    to generate an atom fresh for any given finite set of atoms (lemma 
    [var_fresh]). 
*)

Inductive trm : Set :=
  | trm_bvar : nat -> trm
  | trm_fvar : var -> trm
  | trm_abs  : trm -> trm
  | trm_app  : trm -> trm -> trm.

(** We declare the constructors for indices and variables to be coercions. 
    That way, if Coq sees a nat where it expects an exp, it will implicitly 
    insert an application of bvar; and similarly for atoms. In real metatheory
    developments, we usually do not need such coercions. However, they will
    be very useful for carrying out examples in this tutorial. 
*)

Coercion trm_bvar : nat >-> trm.
Coercion trm_fvar : var >-> trm.


(** For example, we can encode the expression (\x. Y x) as below.
    Because "Y" is free variable in this term, we need to assume an atom 
    for this name.
 *)

Parameter Y : var.
Definition demo_rep1 := trm_abs (trm_app Y 0).

(** Another example: the encoding of (\x. \y. (y x)) *)

Definition demo_rep2 := trm_abs (trm_abs (trm_app 0 1)).

(** Exercise: convert the following lambda calculus term to locally 
    nameless representation: \s. \z. s(s z) *)

Definition demo_two := trm_abs (trm_abs (trm_app 1 (trm_app 1 0))).

(** There are two important advantages of the locally nameless
    representation:
     - Alpha-equivalent terms have a unique representation, 
       we're always working up to alpha-equivalence.
     - Operations such as free variable substitution and free
       variable calculation have simple recursive definitions
      (and therefore are simple to reason about).

    Weighed against these advantages are two drawbacks:
     - The [trm] datatype admits terms, such as [trm_abs 3], where
       indices are unbound. 
       A term is called "locally closed" when it contains 
       no unbound indices. 
     - We must define *both* bound variable & free variable 
       substitution and reason about how these operations 
       interact with eachother.
    
*)

(* ********************************************************************** *)
(** ** Opening *)

(** Opening replaces an index with a term. It corresponds to informal
    substitution for a bound variable, such as in the rule for beta
    reduction. Note that only "dangling" indices (those that do not
    refer to any abstraction) can be opened. Opening has no effect for
    terms that are locally closed.

    Natural numbers are just an inductive datatype with two
    constructors: O and S, defined in Coq.Init.Datatypes.

    We make several simplifying assumptions in defining [open_rec].
    First, we assume that the argument [u] is locally closed.  This
    assumption simplifies the implementation since we do not need to
    shift indices in [u] when passing under a binder.  Second, we
    assume that this function is initially called with index zero and
    that zero is the only unbound index in the term.  This eliminates
    the need to possibly subtract one in the case of indices.

    There is no need to worry about variable capture because bound
    variables are indices.
*)

Fixpoint open_rec (k : nat) (u : trm) (t : trm) {struct t} : trm :=
  match t with
  | trm_bvar i    => If k = i then u else (trm_bvar i)
  | trm_fvar x    => trm_fvar x
  | trm_abs t1    => trm_abs (open_rec (S k) u t1)
  | trm_app t1 t2 => trm_app (open_rec k u t1) (open_rec k u t2)
  end.

(** Many common applications of opening replace index zero with an
    expression or variable.  The following definition provides a
    convenient shorthand for such uses.  Note that the order of
    arguments is switched relative to the definition above.  For
    example, [(open e x)] can be read as "substitute the variable [x]
    for index [0] in [e]" and "open [e] with the variable [x]."
    Recall that the coercions above let us write [x] in place of
    [(fvar x)].
*)

Definition open t u := open_rec 0 u t.

(** We define notations for [open_rec] and [open]. *)

Notation "{ k ~> u } t" := (open_rec k u t) (at level 67).
Notation "t ^^ u" := (open t u) (at level 67).

(** We also define a notation for the specialization of [open] to
    the case where the argument is a free variable. This notation
    is not needed when [trm_fvar] is declared as a coercion like
    we do in this tutorial, but it is very handy when we don't want
    to have such a coercion. (Coercions are very convenient for
    simple developments, but they can make things very obscur when
    it comes to scaling up to larger developments.)  *)

Notation "t ^ x" := (open t (trm_fvar x)).

(** This next demo shows the operation of [open].  For example, the
   locally nameless representation of the term (\y. (\x. (y x)) y)
   is [abs (app (abs (app 1 0)) 0)]. To look at the body
   without the outer abstraction, we need to replace the indices that
   refer to that abstraction with a name.
   Therefore, we show that we can open the body of the abstraction
   above with Y to produce [app (abs (app Y 0)) Y)].
   The tactic [case_if] is used to simplify conditionals.
*)

Lemma demo_open :
  open (trm_app (trm_abs (trm_app 1 0)) 0) Y =
       (trm_app (trm_abs (trm_app Y 0)) Y).
Proof.
  unfold open. unfold open_rec. case_if. case_if. case_if. auto.
Qed.


(* ********************************************************************** *)
(** ** Local closure *)

(** Recall that [trm] admits terms that contain unbound indices. 
    We say that a term is locally closed, 
    when no indices appearing in it are unbound.  The proposition 
    [term e] holds when an expression [e] is locally closed.

    The inductive definition below formalizes local closure such that
    the resulting induction principle serves as the structural
    induction principle over (locally closed) expressions.  In
    particular, unlike induction for type [trm], there is no cases
    for bound variables.  Thus, the induction principle corresponds more
    closely to informal practice than the one arising from the
    definition of pre-terms.
*)

Inductive term : trm -> Prop :=
  | term_var : forall x,
      term (trm_fvar x)
  | term_abs : forall L t1,
      (forall x, x \notin L -> term (t1 ^ x)) ->
      term (trm_abs t1)
  | term_app : forall t1 t2,
      term t1 -> 
      term t2 -> 
      term (trm_app t1 t2).

(** For tactics to work well, it is very important that lists of
    names to avoid, such as [L], appear as first argument of the
    constructors. 
*)


(* ********************************************************************** *)
(** ** Semantics *)

(** We now define the semantics of our call-by-value lambda calculus. 
    We define values and small-step reduction. Note the hypotheses 
    which ensure that the relations hold only for locally closed terms. *)

Inductive value : trm -> Prop :=
  | value_abs : forall t1, 
      term (trm_abs t1) -> value (trm_abs t1).

Inductive red : trm -> trm -> Prop :=
  | red_beta : forall t1 t2,
      term (trm_abs t1) ->
      value t2 ->
      red (trm_app (trm_abs t1) t2) (t1 ^^ t2)
  | red_app_1 : forall t1 t1' t2,
      term t2 ->
      red t1 t1' ->
      red (trm_app t1 t2) (trm_app t1' t2)
  | red_app_2 : forall t1 t2 t2',
      value t1 ->
      red t2 t2' ->
      red (trm_app t1 t2) (trm_app t1 t2').

(** We use the notation [t --> t'] to denote small step reduction. *)

Notation "t --> t'" := (red t t') (at level 68).


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

(** Environments are isomorphic to association lists (lists of pairs of
    keys and values) whose keys are [var]s.  To print environments in a
    pretty way and, in particular, to ensure that new bindings are added
    to the right of existing environments, we do not use the type [list]
    directly but instead use an abstract data type called [env]. More
    precisely, the type [env A] is isomorphic to [list (var * A)].
    Environments are defined in the file [LibEnv]. 

    Here, environments bind [var]s to [typ]s. So, we define [ctx] as a
    shorthand for [env typ]. 
*)
    
Definition ctx := env typ.

(** If [E] and [F] are two contexts, then [E & F] denotes their 
    concatenation. If [x] is a variable and [T] is a type, then 
    [x ~ T] denotes a singleton environment where [x] is bound to [T].
    In particular, [E & x ~ T] denotes a context [E] extended 
    with a binding from [x] to [T]. The empty environment is 
    called [empty].
*)

(** The function [dom] computes the domain of an environment,
    returning a finite set of [var]s. *)
(*
Check dom.
*)

(** The unary predicate [ok] holds when each atom is bound at most
    once in an environment. This property is defined inductively. *)

(*
Print ok.
*)

(** The ternary predicate [binds] holds when a given binding is
    present in an environment.  More specifically, [binds x T E] holds
    when the last binding of [x] binds [x] to the type [T]. *)

(*
Check binds.
*)

(* ********************************************************************** *)
(** ** Typing *)

(** The definition of the typing relation is straightforward.  In
    order to ensure that the relation holds for only well-formed
    environments, we check in the [typing_var] case that the
    environment is [ok].  The structure of typing derivations
    implicitly ensures that the relation holds only for locally closed
    expressions.  Finally, note the use of cofinite quantification in
    the [typing_abs] case. 
*)

Reserved Notation "E |= t ~: T" (at level 69).

Inductive typing : ctx -> trm -> typ -> Prop :=
  | typing_var : forall E x T,
      ok E ->
      binds x T E ->
      E |= (trm_fvar x) ~: T
  | typing_abs : forall L E U T t1,
      (forall x, x \notin L -> 
        (E & x ~ U) |= t1 ^ x ~: T) ->
      E |= (trm_abs t1) ~: (typ_arrow U T)
  | typing_app : forall S T E t1 t2,
      E |= t1 ~: (typ_arrow S T) -> 
      E |= t2 ~: S ->
      E |= (trm_app t1 t2) ~: T

where "E |= t ~: T" := (typing E t T).


(* ********************************************************************** *)
(** ** Statement of theorems *)

(** At this point we can state the theorems that we want to prove.
    Preservation states that if a well-typed term takes a reduction
    step then it produces another well-typed term.
    Progress states that a well-typed term is either a value or it 
    can take a step of reduction. 
*)

Definition preservation_statement := forall E t t' T,
  E |= t ~: T ->
  t --> t' ->
  E |= t' ~: T.

Definition progress_statement := forall t T, 
  empty |= t ~: T ->
     value t 
  \/ exists t', t --> t'.

(** We here reach the end the "trusted base". If we got definitions wrong
    above that point, then we might not be proving what we intend to.
    If, however, we got the definitions right, then no matter how ugly
    our proofs might be, if we reach the Qed of the two theorems that
    we have stated, then we know that our type system is sound.
*)


(* ********************************************************************** *)
(* ********************************************************************** *)
(* ********************************************************************** *)
(** * Infrastructure *)

(** Before we start getting into the proofs, we need to set up a few
    more things.
     - functions definining free variables and substitution,
     - tactics to pick fresh names and to handle freshness-related goals,
     - a few axioms about the behavior of operations on terms.

    We will purposely introduce some axioms, so that we can go straight
    to the proofs that we are interested in. Once we are finished with
    the main proofs, we will do a second pass in order to turn the 
    axioms into proper lemmas.
*)

(* ********************************************************************** *)
(** ** Free variables *)

(** The function [fv], defined below, calculates the set of free
    variables in an expression.  Because we are using locally nameless
    representation, where bound variables are represented as indices,
    any name we see is a free variable of a term.  In particular, this
    makes the [trm_abs] case simple.
*)

Fixpoint fv (t : trm) {struct t} : vars :=
  match t with
  | trm_bvar i    => \{}
  | trm_fvar x    => \{x}
  | trm_abs t1    => (fv t1)
  | trm_app t1 t2 => (fv t1) \u (fv t2)
  end.

(* ********************************************************************** *)
(** ** Substitution *)

(** Substitution replaces a free variable with a term.  The definition
    below is simple for two reasons:
      - Because bound variables are represented using indices, there
        is no need to worry about variable capture.
      - We assume that the term being substituted in is locally
        closed.  Thus, there is no need to shift indices when
        passing under a binder.
*)

Fixpoint subst (z : var) (u : trm) (t : trm) {struct t} : trm :=
  match t with
  | trm_bvar i    => trm_bvar i
  | trm_fvar x    => If x = z then u else (trm_fvar x)
  | trm_abs t1    => trm_abs (subst z u t1)
  | trm_app t1 t2 => trm_app (subst z u t1) (subst z u t2)
  end.

(** We define a notation for free variable substitution that mimics
    standard mathematical notation. *)

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

(** Below is a demo. *)

Parameter Z : var.
Lemma demo_subst1:  [Y ~> Z] (trm_abs (trm_app 0 Y)) = (trm_abs (trm_app 0 Z)).
Proof. simpl. case_if. auto. Qed.


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

(** When picking a fresh atom or applying a rule that uses cofinite
    quantification, choosing a set of atoms to be fresh for can be
    tedious.  In practice, it is simpler to use a tactic to choose the
    set to be as large as possible.

    The first tactic we define, [gather_vars], is used to collect
    together all the atoms in the context.  It relies on an auxiliary
    tactic from [LibLN_Tactics], [gather_vars_with], which collects
    together the atoms appearing in objects of a certain type.  The argument 
    to [gather_vars_with] is a function that should return the set of
    vars appearing in its argument. 
*)

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 : ctx => dom x) in
  let D := gather_vars_with (fun x : trm => fv x) in
  constr:(A \u B \u C \u D).

(** The tactic [pick_fresh_gen L x] creates a new atom fresh 
    from [L] and called [x]. Using the tactic [gather_vars],
    we can automate the construction of [L]. The tactic
    [pick_fresh x] creates a new atom called [x] that is fresh
    for "everything" in the context.
*)

Ltac pick_fresh x :=
  let L := gather_vars in (pick_fresh_gen L x).

(** The tactic [apply_fresh T as y] takes a lemma T of the form 
    [forall L ..., (forall x, x \notin L, P x) -> ... -> Q.]
    and applies it by instantiating L as the set of variables 
    occuring in the context (L is computed using [gather_vars]).
    Moreover, for each subgoal of the form [forall x, x \notin L, P x]
    being generated, the tactic automatically introduces the name [x] 
    as well as the hypothesis [x \notin L].
*)

Tactic Notation "apply_fresh" constr(T) "as" ident(x) :=
  apply_fresh_base T gather_vars x.

(** The tactic [apply_fresh* T as y] is the same as 
    [apply_fresh T as y] except that it calls [intuition eauto]
    subsequently. It is also possible to call [apply_fresh]
    without specifying the name that should be used.
*)

Tactic Notation "apply_fresh" "*" constr(T) "as" ident(x) :=
  apply_fresh T as x; auto*.
Tactic Notation "apply_fresh" constr(T) :=
  apply_fresh_base T gather_vars ltac_no_arg.
Tactic Notation "apply_fresh" "*" constr(T) :=
  apply_fresh T; auto_star.


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

(** Automation is crucial for avoiding to have hundreds of subgoals to
    handle by hand. For the tactics [auto] and [eauto] to be able to
    derive proof automatically, we need to give explicitely the list of
    lemmas that the proof search algorithm should try to exploit.
    The command [Hint Resolve lemma] adds a given lemma to the database
    of proof search. The command [Hint Constructors ind] is equivalent
    to invoking [Hint Resolve] on all of the constructors of the inductive
    type [ind]. We use [Hint Constructors] for all our inductively-defined
    predicates.
*)

Hint Constructors term value red.


(* ********************************************************************** *)
(** ** Axiomatization of the infrastructure *)

Module AxiomatizedVersion.

(** At the point, we introduce two simple axioms and skip the many
    uninteresting auxiliary lemmas that would be required to prove them.

    The first axiom states that substitution for a variable [x] 
    commutes with the operation of opening with another variable [y].

    The second axiom states that the opening of a term [t] with a 
    term [u] can be decomposed in two steps: first opening [t] with
    a variable [x], and second substituting [u] for [x].
*)

Axiom subst_open_var : forall x y u t,
  y <> x -> term u ->
  ([x ~> u]t) ^ y = [x ~> u] (t ^ y).

Axiom subst_intro : forall x t u, 
  x \notin (fv t) -> term u ->
  t ^^ u = [x ~> u](t ^ x).

(** In order to focus our complete attention on the interesting proofs
    first, we add a meta-axiom to tell Coq that it should admit any
    subgoal related to well-formedness, i.e., any goal of the form
    [term t] or [ok E]. We will remove these axioms later on.
    This meta-axiom takes the form of a hint whose action is [skip].
    This hint will be triggered whenever we call [auto]. The [skip]
    tactics simply admits the current goal. *)

Local Hint Extern 1 (term _) => skip.
Local Hint Extern 1 (ok _) => skip.

(** It might also be useful to add an extra meta-axiom, to get rid of
    all the freshness-related subgoals. We do not need here, though. 

    [Hint Extern 1 (_ \notin _) => skip]
*)

(* ********************************************************************** *)
(* ********************************************************************** *)
(* ********************************************************************** *)
(** * Proofs *)

(** Weakening states that if an expression is typeable in some
    environment, then it is typeable in any well-formed extension of
    that environment.  This property is needed to prove the
    substitution lemma.

    As stated below, this lemma is not directly proveable.  The natural
    way to try proving this lemma proceeds by induction on the typing
    derivation for [t].
*)

Lemma typing_weaken_0 : forall E F t T,
   E |= t ~: T -> 
   ok (E & F) ->
   (E & F) |= t ~: T.
Proof.
  introv Typ. induction Typ; intros Ok; subst.
  apply* typing_var.
  apply_fresh* typing_abs as y. (* stuck here *)
Admitted.

(** We are stuck in the [typing_abs] case because the induction
    hypothesis [H0] applies only when we weaken the environment at its
    head.  In this case, however, we need to weaken the environment in
    the middle; compare the conclusion at the point where we are stuck
    to the hypothesis [H], which comes from the given typing derivation.

    We can obtain a more useful induction hypothesis by changing the
    statement to insert new bindings into the middle of the
    environment, instead of at the head.  However, the proof still
    gets stuck, as can be seen by examining each of the cases in
    the proof below. 
*)

Lemma typing_weaken_2 : forall G E F t T,
   (E & G) |= t ~: T -> 
   ok (E & F & G) ->
   (E & F & G) |= t ~: T.
Proof.
  introv Typ.
  (* because of limitations to the [induction] tactic,
     (limitations not entirely solved by [dependent induction]), 
     we need to manually generalize the parameters of the
     judgment that we perform the induction on. *)
  gen_eq H: (E & G). gen G.
  induction Typ; intros G EQ Ok; subst.
  apply* typing_var. apply* binds_weaken.
  (* --begin case abs-- *)
  (* first we compute [L'], the set of used variables *)
  let L := gather_vars in sets L': L.
  (* now we apply [typing_abs] using [L'] *)
  apply (@typing_abs L').
  (* we can introduce a name [y] such that [y \notin L'] *)
  intros y Fry. subst L'.
  (* to apply the induction hypothesis, we need to rewrite
     the context for associativity *)
  rewrite <- concat_assoc.
  (* now we can apply the induction hypothesis *)
  apply H0.
    auto. (* we can prove [y \notin L] *)
    rewrite concat_assoc. auto.
    rewrite concat_assoc. auto.
  (* --end case abs-- *)
  apply* typing_app.
Qed.

(** Using the tactic [apply_fresh] introduced earlier, as well as
    the tactic [apply_ih_bind] which is specialized for applying an
    induction hypothesis up to rewriting of associativity in contexts,
    we obtain a nice and short proof. *)

Lemma typing_weaken : forall G E F t T,
   (E & G) |= t ~: T -> 
   ok (E & F & G) ->
   (E & F & G) |= t ~: T.
Proof.
  introv Typ. gen_eq H: (E & G). gen G.
  induction Typ; intros G EQ Ok; subst.
  apply* typing_var. apply* binds_weaken.
  apply_fresh* typing_abs as y. apply_ih_bind* H0.
  apply* typing_app.
Qed.

(** Proving that typing is preserved by substitution involves very
    similar techniques. The only non trivial part concerns the case
    analysis in the variable case. For that, we use the tactics
    [binds_get] and [binds_cases] which extract information from
    [binds] hypotheses. *)

Lemma typing_subst_1 : forall F E t T z u U,
  (E & z ~ U & F) |= t ~: T ->
  E |= u ~: U ->
  (E & F) |= [z ~> u]t ~: T.
Proof.
  introv Typt Typu. gen_eq G: (E & z ~ U & F). gen F.
  induction Typt; intros G Equ; subst; simpl subst.
  case_var. (* test whether [x] is [z] or not *)
    binds_get H0. (* [T] must be [U] *)
      (* here we want to exploit [typing_weaken] with [G]
         instantiated as [empty], but this is not easy
         because we need to argue that [E & empty = E] *)
      lets M: (@typing_weaken empty E G u U).
      do 2 rewrite concat_empty_r in M.
      apply* M.
    binds_cases H0. 
      apply* typing_var. (* if [x] in [G] *)
      apply* typing_var. (* if [x] in [E] *)
  apply_fresh typing_abs as y.
   rewrite* subst_open_var. apply_ih_bind* H0.
  apply* typing_app.
Qed.

(** As we have seen in the proof above, specializing lemmas 
    on empty environments can be quite tedious. Fortunately,
    the metatheory library includes tactic that greatly helps.
    Calling [apply_empty lemma] is almost equivalent to calling
    [apply (@lemma empty)] except that it rewrites away the
    empty environments on the fly. The proof becomes as follows.
*)

Lemma typing_subst : forall F E t T z u U,
  (E & z ~ U & F) |= t ~: T ->
  E |= u ~: U ->
  (E & F) |= [z ~> u]t ~: T.
Proof.
  introv Typt Typu. gen_eq G: (E & z ~ U & F). gen F.
  induction Typt; intros G Equ; subst; simpl subst.
  case_var.
    binds_get H0. apply_empty* typing_weaken.
    binds_cases H0; apply* typing_var.
  apply_fresh typing_abs as y.
   rewrite* subst_open_var. apply_ih_bind* H0.
  apply* typing_app.
Qed.

(** The proof of preservation appears below.
    Proof sketch: By induction on the typing derivation for [t].

      - [typing_var] case: Variables don't step.

      - [typing_abs] case: Abstractions don't step.

      - [typing_app] case: By case analysis on how [t] steps. The
        [eval_beta] case is interesting, since it follows by the
        substitution lemma.  The others follow directly from the
        induction hypotheses. *)

Lemma preservation_result : preservation_statement.
Proof.
  introv Typ. gen t'.
  induction Typ; intros t' Red; inversions Red.
  inversions Typ1. pick_fresh x. rewrite* (@subst_intro x).
   apply_empty* typing_subst.
  apply* typing_app.
  apply* typing_app.
Qed.

(** The proof of progress appears below.
    Proof sketch: By induction on the typing derivation for [t].

      - [typing_var] case: Can't happen; the empty environment
        doesn't bind anything.

      - [typing_abs] case: Abstractions are values.

      - [typing_app] case: Applications reduce.  The result follows
        from an exhaustive case analysis on whether the two components
        of the application step or are values and the fact that a
        value must be an abstraction. *)

Lemma progress_result : progress_statement.
Proof.
  introv Typ. gen_eq E: (empty:ctx). lets Typ': Typ.
  induction Typ; intros; subst.
  false* binds_empty_inv. 
  left*.
  right. destruct~ IHTyp1 as [Val1 | [t1' Red1]].
    destruct~ IHTyp2 as [Val2 | [t2' Red2]].
      inversions Typ1; inversions Val1. exists* (t0 ^^ t2).
      exists* (trm_app t1 t2'). 
    exists* (trm_app t1' t2).
Qed.

End AxiomatizedVersion.



(* ********************************************************************** *)
(* ********************************************************************** *)
(* ********************************************************************** *)
(** * Removing all axioms *)

Module CompleteVersion.

(** At this point we come back to the infrastructure part and try
    to prove all remaining axioms and meta-axioms. We will need to
    re-check all our proofs. This is usually done in-place in the
    file, however in this tutorial we have copy-pasted all the proofs.
*)

(* ********************************************************************** *)
(** ** Proving the two axioms *)

(** We first set up four lemmas, and then we can prove our two axioms. *)

(** The first lemma is a technical auxiliary lemma which do not 
    want and do not need to read. *)

Lemma open_rec_term_core :forall t j v i u, i <> j ->
  {j ~> v}t = {i ~> u}({j ~> v}t) -> t = {i ~> u}t.
Proof.
  induction t; introv Neq Equ; simpls; inversion* Equ; fequals*.
  case_nat*. case_nat*.
Qed.

(** Substitution on indices is identity on well-formed terms. *)

Lemma open_rec_term : forall t u,
  term t -> forall k, t = {k ~> u}t.
Proof.
  induction 1; intros; simpl; fequals*. unfolds open.
  pick_fresh x. apply* (@open_rec_term_core t1 0 (trm_fvar x)).
Qed.

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

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

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

Lemma subst_open : forall x u t1 t2, term u -> 
  [x ~> u] (t1 ^^ t2) = ([x ~> u]t1) ^^ ([x ~> u]t2).
Proof.
  intros. unfold open. generalize 0.
  induction t1; intros; simpl; fequals*.
  case_nat*. case_var*. apply* open_rec_term.
Qed.

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

Lemma subst_open_var : forall x y u t, y <> x -> term u ->
  ([x ~> u]t) ^ y = [x ~> u] (t ^ y).
Proof. introv Neq Wu. rewrite* subst_open. simpl. case_var*. 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 subst_intro : forall x t u, 
  x \notin (fv t) -> term u ->
  t ^^ u = [x ~> u](t ^ x).
Proof.
  introv Fr Wu. rewrite* subst_open.
  rewrite* subst_fresh. simpl. case_var*.
Qed.


(* ********************************************************************** *)
(** ** Preservation of local closure *)

(** The goal of this section is to set up the appropriate lemmas 
    for proving goals of the form [term t]. First, we defined a
    predicate capturing that a term [t] is the body of a locally
    closed abstraction. *)

Definition body t :=
  exists L, forall x, x \notin L -> term (t ^ x).

(** We then show how to introduce and eliminate [body t]. *)

Lemma term_abs_to_body : forall t1, 
  term (trm_abs t1) -> body t1.
Proof. intros. unfold body. inversion* H. Qed.

Lemma body_to_term_abs : forall t1, 
  body t1 -> term (trm_abs t1).
Proof. intros. inversion* H. Qed.

Hint Resolve term_abs_to_body body_to_term_abs.

(** We prove that terms are stable by substitution *)

Lemma subst_term : forall t z u,
  term u -> term t -> term ([z ~> u]t).
Proof.
  induction 2; simpls*.
  case_var*.
  apply_fresh term_abs. rewrite* subst_open_var.
Qed.

Hint Resolve subst_term.

(** We prove that opening a body with a term gives a term *)

Lemma open_term : forall t u,
  body t -> term u -> term (t ^^ u).
Proof.
  intros. destruct H. pick_fresh y. rewrite* (@subst_intro y).
Qed.

Hint Resolve open_term.


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

(** The last step to set up the infrastructure consists in proving
    that relations are "regular". For example, a typing relation can 
    hold only if the environment has no duplicated keys and the term 
    involved is locally-closed. *)

Lemma typing_regular : forall E e T,
  typing E e T -> ok E /\ term e.
Proof.
  split; induction* H. 
  pick_fresh y. forwards~ : (H0 y).
Qed.

(** Similarly, the value predicate only holds on locally-closed terms. *)

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

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

Lemma red_regular : forall e e',
  red e e' -> term e /\ term e'.
Proof. induction 1; auto* value_regular. Qed.

(** The strength of automation comes from the following custom hints.
    They are easy to set up because the follow a very regular pattern.
    These hints indicate that to prove a goal of the form [ok E],
    it suffices to find in the goal an hypothesis of the form
    [typing E t T] and to exploit the regularity lemma [typing_regular]
    to prove the goal. Similarly, properties of the form [term t]
    can be extracted out of typing or reduction or value judgments.
*)

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 (proj2 (typing_regular H))
  | H: red t _ |- _ => apply (proj1 (red_regular H))
  | H: red _ t |- _ => apply (proj2 (red_regular H))
  | H: value t |- _ => apply (value_regular H)
  end.

(* ********************************************************************** *)
(** ** Checking that the main proofs still type-check *)

(** We conclude our development by showing that, with the appropriate
    hints being set up, we can recompile our proofs without changing 
    any single character in them.
*)

Lemma typing_weaken : forall G E F t T,
   (E & G) |= t ~: T -> 
   ok (E & F & G) ->
   (E & F & G) |= t ~: T.
Proof.
  introv Typ. gen_eq H: (E & G). gen G.
  induction Typ; intros G EQ Ok; subst.
  apply* typing_var. apply* binds_weaken.
  apply_fresh* typing_abs as y. apply_ih_bind* H0.
  apply* typing_app.
Qed.

Lemma typing_subst : forall F E t T z u U,
  (E & z ~ U & F) |= t ~: T ->
  E |= u ~: U ->
  (E & F) |= [z ~> u]t ~: T.
Proof.
  introv Typt Typu. gen_eq G: (E & z ~ U & F). gen F.
  induction Typt; intros G Equ; subst; simpl subst.
  case_var.
    binds_get H0. apply_empty* typing_weaken.
    binds_cases H0; apply* typing_var.
  apply_fresh typing_abs as y.
   rewrite* subst_open_var. apply_ih_bind* H0.
  apply* typing_app.
Qed.

Lemma preservation_result : preservation_statement.
Proof.
  introv Typ. gen t'.
  induction Typ; intros t' Red; inversions Red.
  inversions Typ1. pick_fresh x. rewrite* (@subst_intro x).
   apply_empty* typing_subst.
  apply* typing_app.
  apply* typing_app.
Qed.

Lemma progress_result : progress_statement.
Proof.
  introv Typ. gen_eq E: (empty:ctx). lets Typ': Typ.
  induction Typ; intros; subst.
  false* binds_empty_inv. 
  left*.
  right. destruct~ IHTyp1 as [Val1 | [t1' Red1]].
    destruct~ IHTyp2 as [Val2 | [t2' Red2]].
      inversions Typ1; inversions Val1. exists* (t0 ^^ t2).
      exists* (trm_app t1 t2'). 
    exists* (trm_app t1' t2).
Qed.


End CompleteVersion.