(** * Typed lambda calculus (TAPL Chapter 9)

We now turn to languages with functions. The presence of variables,
typing contexts and substitutions complicates formal reasoning about
the languages. *)

Require Export Logic.
Require Export notations.



(** ** Decidable equality for numbers

We have chosen to represent variable identifiers simply as natural
numbers. This is reasonable enough, since the only thing we want from
identifiers is that there is an infinite number of them and that we
can effectively compare them for equality.

This latter point is worth explicating. An effective method for
comparing numbers for equality is a function that can tell us whether
two numbers are the same or not. We already have such a function:
[beq_nat]. We now have to prove that [beq_nat n m] actually returns
[true] if and only if [n = m]. *)

Theorem beq_nat_eq : forall n m, beq_nat n m = true <-> n = m.
Proof.
(** Exercise **)
Admitted.

(** Given the above result, it directly follows that equality of numbers
is decidable. *)

Corollary nat_eq_dec : forall n m : nat, n = m \/ n <> m.
Proof.
  intros n m.
  destruct (beq_nat_eq n m) as [f g].
  destruct (beq_nat n m).
    Case "beq_nat n m = true".
    left.
    apply f.
    reflexivity.

    Case "beq_nat n m = false".
    right.
    intro nQm.
    discriminate g.
    apply nQm.
Qed.


(** In practice we often need to track the dependency between the
result of an application of [beq_nat] and the equality of its
arguments. The following versions of the result make this
easier. *)

Definition decides b P := match b with true => P | false => ~P end.

Corollary beq_decides_eq_nat : forall n m, decides (beq_nat n m) (n = m).
Proof.
  intros n m.
  destruct (beq_nat_eq n m) as [f g].
  destruct (beq_nat n m).
    Case "beq_nat n m = true".
    apply f.
    reflexivity.
    
    Case "beq_nat n m = false".
    intro nQm.
    discriminate g.
    apply nQm.
Qed.

Corollary beq_nat_eq_dec : forall x y, 
  (beq_nat x y = true /\ x = y) \/ (beq_nat x y = false /\ x <> y).
Proof.
  intros x y.
  assert (Q := beq_decides_eq_nat x y).
  destruct (beq_nat x y); simpl in Q |- *; auto using or_introl, or_intror, conj.
Qed.




Module typed_bool_fun.

Require Export typed_bool_fun_lang.

Hint Constructors term val eval type typing and or ex bound fvs : bool_fun.

Definition well_typed (t : term) : Prop :=
  exists T, |- t : T.

(** ** Canonical forms (TAPL 9.3.4)

The canonical forms lemmas are exactly similar to those we encountered
previously, except now for values of a function type we have the notion
of "function values", i.e. abstractions. *)

Inductive bv : term -> Prop :=
| bv_true : bv true
| bv_false : bv false
.

Inductive fv : term -> Prop :=
| fv_abs x T t : fv (\ x : T , t).

Hint Constructors bv fv : bool_fun.

Lemma canonical_forms_bool : forall v, val v -> |- v : Bool -> bv v.
Proof.
  intros v val_v v_Bool.
  induction val_v; inversion v_Bool; subst; 
    try inversion H; eauto with bool_fun.
Qed.

Lemma canonical_forms_fun : forall v T1 T2, val v -> |- v : (T1 -> T2) -> fv v.
Proof.
  intros v T1 T2 val_v v_F.
  induction val_v; inversion v_F; subst; 
    try inversion H; eauto with bool_fun.
Qed.

Hint Resolve canonical_forms_bool canonical_forms_fun : bool_fun.


(** ** Progress (TAPL 9.3.5)

The progress theorem for simply typed lambda calculus (with booleans)
is similar to the one for the plain boolean language. The new cases to
consider are abstractions (which are values immediately), variables
(which cannot appear outside an abstraction in an empty typing
context), and applications (which are handled very much like
conditionals).

A technical complication arises due to the presence of contexts in the
typing relation, and in particular due to the fact that the emptiness
of the context is crucial for the [T_Var] case. When we have a
hypothesis of the form [{} |- t : T], the standard induction tactic
forgets the emptiness of the context and makes the [T_Var] case
impossible to prove.

The way to deal with this is to use the [remember] tactic to replace
[{}] with [G] in the hypothesis and add a new hypothesis [G = {}] in
the context. Then we can do induction and use [subst] to replace [G]
once again with [{}].

It should be noted that this only works because in all the cases we
consider, the context in the inductive hypotheses is the same,
i.e. [{}]. We could not use the inductive hypotheses in the [T_Abs]
case, but thankfully we don't need to, since abstractions are directly
values. *)

Theorem progress t : well_typed t -> val t \/ exists t', t --> t'.
Proof with eauto with bool_fun.
  intros t [T t_T].
  remember {}%ctx as G.
  induction t_T; subst G...

    Case "T_If {} t1 t2 t3 T t_T1 t_T2 t_T3".
    destruct IHt_T1 as [val_t1 | [t1' t1Et1']]...
      SCase "val t1".
      elimtype (bv t1)...

    Case "T_Var {} x T H".
    (* Impossible to have a bound variable in an empty context. *)
    inversion H.

    Case "T_App {} t1 t2 T12 T11 t_T1 t_T2".
    destruct IHt_T1 as [val_t1 | [t1' t1Et1']]...
      SCase "val t1".
      destruct IHt_T2 as [val_t2 | [t2' t2Et2']]...
        SSCase "val t2".
        elimtype (fv t1)...
Qed.



(** ** Closed terms

Firstly, a basic definition: a term is _closed_, if no variables
appear free in it. (Recall that a variable appears free in a term if it
is not bound, i.e. the variable occurs outside of any abstractions that
bind the same variable. Hence [x] appears free in [((\y:T.y) $ x)%tm]
but [y] does not.) *)

Definition closed (t : term) := forall x, ~(fvs t x).

(** There is an obvious connection between free variables and typing:
if [G |- t : T], and a variable [x] appears free in [t], then [x] must
appear in [G] (i.e. it must be bound to some [T'] in [G]. *)

Lemma free_in_context : forall G t T x, 
  (G |- t : T) -> fvs t x -> exists T', bound x T' G.
Proof.
  intros G t T x G_t_T x_f_t.
  induction G_t_T; inversion x_f_t; subst; auto.
    Case "T_Var".
      SCase "FVS_Var".
      exists T.
      apply H.
    
    Case "T_Abs".
      SCase "FVS_Abs".
      destruct (IHG_t_T H4) as [T' B].
      exists T'.
      inversion B; subst.
        SSCase "B_Here".
        contradiction H3.
        reflexivity.

        SSCase "B_Next".
        assumption.
Qed.

(** A direct corollary is that if a term is well-typed (i.e. has some
type in an empty context), then it must be closed. *)

Corollary well_typed_is_closed : forall t, well_typed t -> closed t.
Proof.
  intros t [T t_T].
  red.
  red.
  intros x x_f_t.
  destruct (free_in_context {} t T x t_T x_f_t) as [T' B].
  inversion B.
Qed.

(** ** Context invariance

Instead of explicit permutation and weakening lemmas (as in TAPL 9.3.6
and 9.3.7), we prove a somewhat more general property about the typing
relation: only the types of the variables that occur free in [t] matter
when typing it. That is, if [G] and [G'] give the same type to all the
variables that appear free in [t], then if [G |- t : T], then also [G'
|- t : T]. *)

Lemma context_invariance : 
  forall G G' t T,
  (forall x T', fvs t x -> bound x T' G -> bound x T' G')  ->
  G |- t : T  ->
  G' |- t : T.
Proof with eauto 20 with bool_fun.
  intros G G' t T H G_t_T.
  induction G_t_T in G', H |- *...
(** The only interesting case is the one for abstractions. After
    applying the typing rule for abstractions, it remains to show that
    [G', x:T1 |- t2 : T2] if [G, x:T1 |- t2 : T2]. We then use the
    inductive hypothesis, which was generalized over _all_
    contexts, so we can apply it to the extended contexts above.
    
    Then it remains to show that for any variable [x0] free in [t2],
    [G',x:T1] binds it to the same types as [G,x:T1]. This is proven
    by considering whether [x0] was found from the head of [G, x:T1].
    If it was, then [x0 = x], and both contexts bind it to [T1]. If it
    is not, then [x0 <> x], and we use the original hypothesis that
    says that [G'] binds variables free in [t] to the same types as
    [G].

    Then it remains to show that [x0], which is free in [t2], is also
    free in [t = \x:T1. t2]. This follows from the fact that [x0 <>
    x], so the lambda will not bind [x0].

    It turns out that most of this reasoning can be implemented by
    automation. Still, it can be instructive exercise to solve
    everything after the [inversion] manually. *)

    Case "T_Abs,  t = (\x:T1, t2),  T = T1 -> T2,  G, x:T1 |- t2 : T2".
    apply T_Abs.
    apply IHG_t_T.
    intros x' T' x'_f_t2 B.
    inversion B...
Qed.


(** ** Weakening in an empty context

As a direct corollary, if [t] has type [T] in an empty context (and
is therefore closed), it has type [T] in any context.

Note that we cannot prove the most general form of weakening (if [G |-
t : T] then [G, x:S |- t : T], because [x] might appear free in
[t]. *)

Corollary empty_weakening : forall G t T, |- t : T -> G |- t : T.
Proof with eauto with bool_fun.
  intros G t T t_T.
  apply (context_invariance {})...
    intros x T' x_f_t x_B_E.
    inversion x_B_E.
Qed.

(** ** Shadowed variable removal

An additional lemma that we need is the followign: if the same
variable name appears twice in a row in a context, the one that is
shadowed by the other can be removed without altering the typing of a
term.

The intuitive justification should be clear: if a variable is shadowed
by another one with the same name, then it cannot be referenced and no
term can depend on its type.

Formally, we prove the lemma by applying context invariance and then
showing that the context with the shadowed variable binds all
variables to the same type as the context without the shadowed
variable.  The proof makes for the first time use of the decidability
of equality between numbers: When considering contexts [G, x:S', x:S]
and [G, x:S] and looking up a variable [x'], then we need to consider
both the cases where [x = x'] and [x <> x']. In the first case, both
contexts bind [x] to [S]. In the second case, both contexts bind [x']
to whatever [G] binds them to.

For explicitness, the proof script is given manually below. Automation
could be used to shorten the proof. *)

Lemma shadowed_removable : forall G x S S' t T,
  {{G, x : S'}, x : S}%ctx |- t : T -> {G, x : S} |- t : T.
Proof.
  intros G x S S' t T.
  apply context_invariance.
  intros x' T' x'_f_t2 x'_B_G1.
  destruct (nat_eq_dec x x') as [xQx' | nxQx'].
    Case "x = x'".
    subst x'.
    inversion x'_B_G1; subst.
      SCase "B_Here".
      apply B_Here.

      SCase "B_Next".
      contradiction H3.
      reflexivity.
          
    Case "x <> x'".
    inversion x'_B_G1; subst.
      SCase "B_Here".
      apply B_Here.

      SCase "B_Next".
      inversion H5; subst.
        SSCase "B_Here".
        contradiction H3.
        reflexivity.

        SSCase "B_Next".
        apply B_Next.
        apply H4.
        apply H7.
Qed.

(** ** Permutation (TAPL 9.3.6)

Another result we need is the fact that in a context, two adjacent
variable typings can switch places. It is a prerequisite, though, that
the variables are distinct. The reason for this is that [G, x:S, x:T
|- x : T], but [G, x:T, x:S |- x : S].

The proof is very similar to the one above, so we use automation to
skip the boring parts. *)

Lemma permutation : forall G x y S U t T, 
  x <> y  ->
  {{G, x : S}, y : U}%ctx |- t : T  ->
  {{G, y : U}, x : S}%ctx |- t : T.
Proof with eauto with bool_fun.
  intros G x y S U t T xNQy.
  apply context_invariance.
  intros x' T' x'_f_t2 x'_B_G1.
  inversion x'_B_G1; subst...
    Case "B_Here".
    apply B_Next...
    red...

    Case "B_Next".
    inversion H5...
Qed.

(** ** Type preservation under substitution (TAPL 9.3.8)

We now get to the most involved theorem so far, type preservation for
substitution. Note that the theorem in TAPL is more general than is
really needed. The languages we are considering are designed so that we
only substitute _closed values_ for variables, so we can assume that
the term to be substituted can be typed in an empty context.

The most challenging part of the proof is following the operation of the
substitution function. Note that when it encounters a variable or an
abstraction, the substitution function compares variables for equality.
We need to be able to consider both the case where the comparison is
true and the case where it is false. Moreover, we need to know that when
the comparison returns true, the compared terms are actually equal, and
when it returns false, they are not.

Recall that we use just plain natural numbers as variable identifiers.
The previous result about the decidability of their equality now comes
handy. First, we use [beq_decides_eq_nat x v] to get [Q : decides
(beq_nat x v) (x = v)]. Then we use the [destruct] tactic on [beq_nat x
v]. This gives us two subgoals, one where [beq_nat x v] has been
replaced with [true] and one where it has been replaced with [false].
Simplifying [Q] we now get [Q : x = v] and [Q : x <> v] in the subgoals.
*)

Theorem subst_preservation : forall G x S s t T,
  {G, x : S} |- t : T   -> 
  {} |- s : S           -> 
  G |- [x |-> s]t : T.
Proof with eauto with bool_fun.
  intros G x S s t T t_T s_S.

(** Once again it is crucial that we do a general enough induction: we
  do induction on terms on the general property that for _any_
  context [G] and type [T] such that [G |- t : T], we have [G |- [x |->
  s]t]. This allows us to use a different context when applying an
  inductive hypothesis. *)

  induction t in G, T, t_T |- *; simpl; inversion t_T; subst...

    Case "t = TmVar y, T_Var".
    rename v into y.
    assert (Q := beq_decides_eq_nat x y).
    destruct (beq_nat x y); simpl in Q.
(** We are substituting in the variable [x]. Because the context
      ends with [x : S], we know that the type [T] must be [S]. We also
      know that the substitution function replaces [x] with [S] so it
      remains to show that [G |- s : S]. This we get directly from [|- s
      : S] with weakening. *)
      SCase "x = y".
      subst y.
      inversion H1; subst.
        SSCase "B_Here".
        apply empty_weakening.
        apply s_S.

        SSCase "B_Next".
        contradiction H4.
        reflexivity.

(** We are substituting in some variable that is not [x]. In that
      case, the substitution function leaves the original term as it is.
      It remains to show that [G |- v : T]. This must be true, since [G,
      x : S |- T], and [x <> v]. *)
      SCase "x <> y".
      apply T_Var.
      inversion H1; subst.
        SSCase "B_Here".
        contradiction Q.
        reflexivity.

        SSCase "B_Next".
        assumption.
 
    Case "T_Abs,  t = \y:T1, t2,  T = T1 -> T2".
    (* Rename the variables to the ones used in TAPL. Note that for
       some reason TAPL uses T = T2 -> T1 here instead of T1 -> T2. *)
    rename v into y, T2 into T1, t into T2, t0 into t1.
    assert (Q := beq_decides_eq_nat x y).
    destruct (beq_nat x y); simpl in Q.
(** We are substituting in an abstraction which binds [x]. In
      this case the substitution will leave it as it is and we have to
      show just that we can remove the original [x] from the context
      and the term remains well-typed. This is done directly by the
      shadowed variable removal lemma. *)
      SCase "x = y".
      subst y.
      apply T_Abs.
      eapply shadowed_removable...

(** We are substituting in an abstraction which does not bind
      [x]. (This is the only case that is considered in TAPL.) After
      applying the [T_Abs] rule we need to prove 

      [G, y:T2 |- [x |-> s]t1 : T1]

      We can then use the inductive hypothesis (which, thanks to its
      generality, can be given the extended context above), and are
      left with proving

      [G, y:T2, x:S |- t1 : T1]

      This can then be proven by the permutation lemma and our
      hypothesis (from considering the T_Abs case):

      [G, x:S, y:T2 |- t1 : T1]. *)
      SCase "x <> y".
      apply T_Abs.
      apply IHt.
      apply permutation...
Qed.

(** ** Type preservation under evaluation (TAPL 9.3.9)

The actual type preservation theorem follows by a relatively simple
induction on the derivation of the typing judgement, followed by an
inversion on the evaluation judgement. The only interesting case is
the one for the [T_Abs], [E_AppAbs], where we have to use the
above substitution preservation lemma.  *)

Theorem preservation : forall t t' T, 
  |- t : T    ->  
  t --> t'    ->  
  |- t' : T.
Proof.
(** Exercise **)
Admitted.

(** *)

End typed_bool_fun.

(** **)