Prelude

We begin with a direct attempt to establish type preservation (that is, subject reduction) for System F, and find that we need a key inversion lemma first.

Goal (* jf_preservation *)
  forall Gamma t T,
  jf Gamma t T ->
  forall t',
  cbv t t' ->
  jf Gamma t' T.
forall (Gamma : tyenv) (t : term) (T : ty),
jf Gamma t T ->
forall t' : term, cbv t t' -> jf Gamma t' T
Proof.
forall (Gamma : tyenv) (t : term) (T : ty),
jf Gamma t T ->
forall t' : term, cbv t t' -> jf Gamma t' T
  (* By induction on the type derivation. *)
  induction 1; intros; subst; try solve [ invert_cbv ].
Gamma: tyenv
t1, t2: term
T, U: ty
H: jf Gamma t1 (TyFun T U)
H0: jf Gamma t2 T
IHjf1: forall t' : term,
cbv t1 t' -> jf Gamma t' (TyFun T U)
IHjf2: forall t' : term, cbv t2 t' -> jf Gamma t' T
t': term
H1: cbv (App t1 t2) t'
jf Gamma t' U
Gamma: var -> ty
t: term
T: ty
H: jf (Gamma >> ren (+1)) t T
IHjf: forall t' : term,
cbv t t' -> jf (Gamma >> ren (+1)) t' T
t': term
H1: cbv t t'
jf Gamma t' (TyAll T)
Gamma: tyenv
t: term
T, U: {bind ty}
H: jf Gamma t (TyAll T)
IHjf: forall t' : term,
cbv t t' -> jf Gamma t' (TyAll T)
t': term
H1: cbv t t'
jf Gamma t' T.[U/]
  (* JFApp *)
  { (* By case analysis on `cbv t t'`. *)
Gamma: tyenv
t1, t2: term
T, U: ty
H: jf Gamma t1 (TyFun T U)
H0: jf Gamma t2 T
IHjf1: forall t' : term,
cbv t1 t' -> jf Gamma t' (TyFun T U)
IHjf2: forall t' : term, cbv t2 t' -> jf Gamma t' T
t': term
H1: cbv (App t1 t2) t'
jf Gamma t' U
    invert_cbv.
Gamma: tyenv
t2: term
T, U: ty
t: term
H: jf Gamma (Lam t) (TyFun T U)
H0: jf Gamma t2 T
IHjf1: forall t' : term,
cbv (Lam t) t' -> jf Gamma t' (TyFun T U)
IHjf2: forall t' : term, cbv t2 t' -> jf Gamma t' T
H4: cbv_mask RuleBetaV
H5: is_value t2
jf Gamma t.[t2/] U
Gamma: tyenv
t1, t2: term
T, U: ty
H: jf Gamma t1 (TyFun T U)
H0: jf Gamma t2 T
IHjf1: forall t' : term,
cbv t1 t' -> jf Gamma t' (TyFun T U)
IHjf2: forall t' : term, cbv t2 t' -> jf Gamma t' T
t3: term
H4: cbv_mask RuleAppL
H6: cbv t1 t3
jf Gamma (App t3 t2) U
Gamma: tyenv
t1, t2: term
T, U: ty
H: jf Gamma t1 (TyFun T U)
H0: jf Gamma t2 T
IHjf1: forall t' : term,
cbv t1 t' -> jf Gamma t' (TyFun T U)
IHjf2: forall t' : term, cbv t2 t' -> jf Gamma t' T
u2: term
H4: cbv_mask RuleAppVR
H5: is_value t1
H7: cbv t2 u2
jf Gamma (App t1 u2) U
    (* RedBetaV. A beta-redex, `App (Lam t) v`, reduces to `t.[v/]`. *)
    { (* The idea is to substitute `v` for the variable `0`. *)
Gamma: tyenv
t2: term
T, U: ty
t: term
H: jf Gamma (Lam t) (TyFun T U)
H0: jf Gamma t2 T
IHjf1: forall t' : term,
cbv (Lam t) t' -> jf Gamma t' (TyFun T U)
IHjf2: forall t' : term, cbv t2 t' -> jf Gamma t' T
H4: cbv_mask RuleBetaV
H5: is_value t2
jf Gamma t.[t2/] U
      eapply jf_te_substitution_0; eauto with jf.
Gamma: tyenv
t2: term
T, U: ty
t: term
H: jf Gamma (Lam t) (TyFun T U)
H0: jf Gamma t2 T
IHjf1: forall t' : term,
cbv (Lam t) t' -> jf Gamma t' (TyFun T U)
IHjf2: forall t' : term, cbv t2 t' -> jf Gamma t' T
H4: cbv_mask RuleBetaV
H5: is_value t2
jf (T .: Gamma) t U
      (* This requires us to prove that the function body `t` is
         well-typed under an extended type environment `T .: Gamma`.
         An inversion lemma is needed. *)
Abort.

An inversion lemma (first attempt)

We wish to establish an inversion lemma for the typing rule for lambda-abstractions.

A first version of the statement is as follows: if under Gamma a lambda-abstraction Lam t has type TyFun T U, then under the extended environment T .: Gamma, the term t must have type U. Let us try to prove this:

Goal (* invert_jf_Lam_TyFun *)
  forall Gamma t' T' ,
  jf Gamma t' T' ->
  forall t T U,
  t' = Lam t ->
  T' = TyFun T U ->
  jf (T .: Gamma) t U.
forall (Gamma : tyenv) (t' : term) (T' : ty),
jf Gamma t' T' ->
forall (t : {bind term}) (T U : ty),
t' = Lam t -> T' = TyFun T U -> jf (T .: Gamma) t U
Proof.
forall (Gamma : tyenv) (t' : term) (T' : ty),
jf Gamma t' T' ->
forall (t : {bind term}) (T U : ty),
t' = Lam t -> T' = TyFun T U -> jf (T .: Gamma) t U
  induction 1; intros; subst; try solve [ false; congruence ].
Gamma: var -> ty
t: term
T, U: ty
H: jf (T .: Gamma) t U
IHjf: forall (t0 : {bind term}) (T0 U0 : ty),
t = Lam t0 ->
U = TyFun T0 U0 -> jf (T0 .: T .: Gamma) t0 U0
t0: {bind term}
T0, U0: ty
H0: Lam t = Lam t0
H1: TyFun T U = TyFun T0 U0
jf (T0 .: Gamma) t0 U0
Gamma: tyenv
T, U: {bind ty}
t0: {bind term}
IHjf: forall (t : {bind term}) (T0 U : ty),
Lam t0 = Lam t ->
TyAll T = TyFun T0 U -> jf (T0 .: Gamma) t U
H: jf Gamma (Lam t0) (TyAll T)
T0, U0: ty
H2: T.[U/] = TyFun T0 U0
jf (T0 .: Gamma) t0 U0
  (* Case: JFLam. *)
  {
Gamma: var -> ty
t: term
T, U: ty
H: jf (T .: Gamma) t U
IHjf: forall (t0 : {bind term}) (T0 U0 : ty),
t = Lam t0 ->
U = TyFun T0 U0 -> jf (T0 .: T .: Gamma) t0 U0
t0: {bind term}
T0, U0: ty
H0: Lam t = Lam t0
H1: TyFun T U = TyFun T0 U0
jf (T0 .: Gamma) t0 U0 congruence. }
Gamma: tyenv
T, U: {bind ty}
t0: {bind term}
IHjf: forall (t : {bind term}) (T0 U : ty),
Lam t0 = Lam t ->
TyAll T = TyFun T0 U -> jf (T0 .: Gamma) t U
H: jf Gamma (Lam t0) (TyAll T)
T0, U0: ty
H2: T.[U/] = TyFun T0 U0
jf (T0 .: Gamma) t0 U0
  (* Case: JFTyApp. *)
  {
Gamma: tyenv
T, U: {bind ty}
t0: {bind term}
IHjf: forall (t : {bind term}) (T0 U : ty),
Lam t0 = Lam t ->
TyAll T = TyFun T0 U -> jf (T0 .: Gamma) t U
H: jf Gamma (Lam t0) (TyAll T)
T0, U0: ty
H2: T.[U/] = TyFun T0 U0
jf (T0 .: Gamma) t0 U0 (* The induction hypothesis has the unsatisfiable requirement
       `TyAll _ = TyFun _ _`. *)
    clear IHjf.
Gamma: tyenv
T, U: {bind ty}
t0: {bind term}
H: jf Gamma (Lam t0) (TyAll T)
T0, U0: ty
H2: T.[U/] = TyFun T0 U0
jf (T0 .: Gamma) t0 U0
    (* We are stuck. *)
Abort.

An inversion lemma (second attempt)

The previous attempt fails, because the statement is not general enough. We cannot restrict our attention to the situation where the term Lam t has a function type. We must also reason about the situations where it has a polymorphic type that can be instantiated to a function type.

Thus, we propose a more general statement, where Lam t has type T' and T' can be weakened (via a subsumption relation) to TyFun T U.

This relation is defined by just one rule: the type TyAll T is a subtype of the type T.[U/]. When necessary, we will use the reflexive transitive closure of this relation, [star sub], so as to allow for a sequence of subtyping steps.

Inductive sub : ty -> ty -> Prop :=
| Sub:
    forall T T' U,
    T' = T.[U/] ->
    sub (TyAll T) T'.

Here is a second attempt at the inversion lemma for lambda-abstractions. Instead of requiring an equality between T' and TyFun T U, we allow a sequence of subsumption steps. Thus, this statement is stronger.

Goal (* invert_jf_Lam_TyFun *)
  forall Gamma t' T' ,
  jf Gamma t' T' ->
  forall t T U,
  t' = Lam t ->
  star sub T' (TyFun T U) ->
  jf (T .: Gamma) t U.
forall (Gamma : tyenv) (t' : term) (T' : ty),
jf Gamma t' T' ->
forall (t : {bind term}) (T U : ty),
t' = Lam t ->
star sub T' (TyFun T U) -> jf (T .: Gamma) t U
Proof.
forall (Gamma : tyenv) (t' : term) (T' : ty),
jf Gamma t' T' ->
forall (t : {bind term}) (T U : ty),
t' = Lam t ->
star sub T' (TyFun T U) -> jf (T .: Gamma) t U
  induction 1; intros; subst; try solve [ false; congruence ].
Gamma: var -> ty
t: term
T, U: ty
H: jf (T .: Gamma) t U
IHjf: forall (t0 : {bind term}) (T0 U0 : ty),
t = Lam t0 ->
star sub U (TyFun T0 U0) ->
jf (T0 .: T .: Gamma) t0 U0
t0: {bind term}
T0, U0: ty
H0: Lam t = Lam t0
H1: star sub (TyFun T U) (TyFun T0 U0)
jf (T0 .: Gamma) t0 U0
Gamma: var -> ty
T: ty
t0: {bind term}
IHjf: forall (t : {bind term}) (T0 U : ty),
Lam t0 = Lam t ->
star sub T (TyFun T0 U) ->
jf (T0 .: Gamma >> ren (+1)) t U
H: jf (Gamma >> ren (+1)) (Lam t0) T
T0, U: ty
H2: star sub (TyAll T) (TyFun T0 U)
jf (T0 .: Gamma) t0 U
Gamma: tyenv
T, U: {bind ty}
t0: {bind term}
IHjf: forall (t : {bind term}) (T0 U : ty),
Lam t0 = Lam t ->
star sub (TyAll T) (TyFun T0 U) ->
jf (T0 .: Gamma) t U
H: jf Gamma (Lam t0) (TyAll T)
T0, U0: ty
H2: star sub T.[U/] (TyFun T0 U0)
jf (T0 .: Gamma) t0 U0
  (* This time, we have three subgoals instead of two. *)
  all: swap 2 3.
Gamma: var -> ty
t: term
T, U: ty
H: jf (T .: Gamma) t U
IHjf: forall (t0 : {bind term}) (T0 U0 : ty),
t = Lam t0 ->
star sub U (TyFun T0 U0) ->
jf (T0 .: T .: Gamma) t0 U0
t0: {bind term}
T0, U0: ty
H0: Lam t = Lam t0
H1: star sub (TyFun T U) (TyFun T0 U0)
jf (T0 .: Gamma) t0 U0
Gamma: tyenv
T, U: {bind ty}
t0: {bind term}
IHjf: forall (t : {bind term}) (T0 U : ty),
Lam t0 = Lam t ->
star sub (TyAll T) (TyFun T0 U) ->
jf (T0 .: Gamma) t U
H: jf Gamma (Lam t0) (TyAll T)
T0, U0: ty
H2: star sub T.[U/] (TyFun T0 U0)
jf (T0 .: Gamma) t0 U0
Gamma: var -> ty
T: ty
t0: {bind term}
IHjf: forall (t : {bind term}) (T0 U : ty),
Lam t0 = Lam t ->
star sub T (TyFun T0 U) ->
jf (T0 .: Gamma >> ren (+1)) t U
H: jf (Gamma >> ren (+1)) (Lam t0) T
T0, U: ty
H2: star sub (TyAll T) (TyFun T0 U)
jf (T0 .: Gamma) t0 U

  (* Case: JFLam. *)
  {
Gamma: var -> ty
t: term
T, U: ty
H: jf (T .: Gamma) t U
IHjf: forall (t0 : {bind term}) (T0 U0 : ty),
t = Lam t0 ->
star sub U (TyFun T0 U0) ->
jf (T0 .: T .: Gamma) t0 U0
t0: {bind term}
T0, U0: ty
H0: Lam t = Lam t0
H1: star sub (TyFun T U) (TyFun T0 U0)
jf (T0 .: Gamma) t0 U0 (* We have a hypothesis `star sub (TyFun T' U') (TyFun T U)`.
       Considering the definition of the relation `sub`, this must be a
       sequence of zero subtyping steps, so we must have `T' = T` and
       `U' = U`. To let Coq see this, it suffices to perform case
       analysis. (One could also make it a separate lemma, for clarity.)
       *)
    pick star invert; [ | pick sub invert ].
Gamma: var -> ty
t: term
T0, U0: ty
H: jf (T0 .: Gamma) t U0
IHjf: forall (t0 : {bind term}) (T U : ty),
t = Lam t0 ->
star sub U0 (TyFun T U) ->
jf (T .: T0 .: Gamma) t0 U
t0: {bind term}
H0: Lam t = Lam t0
jf (T0 .: Gamma) t0 U0
    (* The result is then immediate. *)
    congruence. }
Gamma: tyenv
T, U: {bind ty}
t0: {bind term}
IHjf: forall (t : {bind term}) (T0 U : ty),
Lam t0 = Lam t ->
star sub (TyAll T) (TyFun T0 U) ->
jf (T0 .: Gamma) t U
H: jf Gamma (Lam t0) (TyAll T)
T0, U0: ty
H2: star sub T.[U/] (TyFun T0 U0)
jf (T0 .: Gamma) t0 U0
Gamma: var -> ty
T: ty
t0: {bind term}
IHjf: forall (t : {bind term}) (T0 U : ty),
Lam t0 = Lam t ->
star sub T (TyFun T0 U) ->
jf (T0 .: Gamma >> ren (+1)) t U
H: jf (Gamma >> ren (+1)) (Lam t0) T
T0, U: ty
H2: star sub (TyAll T) (TyFun T0 U)
jf (T0 .: Gamma) t0 U

  (* Case: JFTyApp. *)
  {
Gamma: tyenv
T, U: {bind ty}
t0: {bind term}
IHjf: forall (t : {bind term}) (T0 U : ty),
Lam t0 = Lam t ->
star sub (TyAll T) (TyFun T0 U) ->
jf (T0 .: Gamma) t U
H: jf Gamma (Lam t0) (TyAll T)
T0, U0: ty
H2: star sub T.[U/] (TyFun T0 U0)
jf (T0 .: Gamma) t0 U0 (* In that case, it suffices to invoke the induction hypothesis.
       The subtyping sequence `star sub ...` grows by one, as one more
       step is prepended to it. This is precisely the reason why the
       lemma was formulated in this general form. *)
    eapply IHjf.
Gamma: tyenv
T, U: {bind ty}
t0: {bind term}
IHjf: forall (t : {bind term}) (T0 U : ty),
Lam t0 = Lam t ->
star sub (TyAll T) (TyFun T0 U) ->
jf (T0 .: Gamma) t U
H: jf Gamma (Lam t0) (TyAll T)
T0, U0: ty
H2: star sub T.[U/] (TyFun T0 U0)
Lam t0 = Lam t0
Gamma: tyenv
T, U: {bind ty}
t0: {bind term}
IHjf: forall (t : {bind term}) (T0 U : ty),
Lam t0 = Lam t ->
star sub (TyAll T) (TyFun T0 U) ->
jf (T0 .: Gamma) t U
H: jf Gamma (Lam t0) (TyAll T)
T0, U0: ty
H2: star sub T.[U/] (TyFun T0 U0)
star sub (TyAll T) (TyFun T0 U0)
    {
Gamma: tyenv
T, U: {bind ty}
t0: {bind term}
IHjf: forall (t : {bind term}) (T0 U : ty),
Lam t0 = Lam t ->
star sub (TyAll T) (TyFun T0 U) ->
jf (T0 .: Gamma) t U
H: jf Gamma (Lam t0) (TyAll T)
T0, U0: ty
H2: star sub T.[U/] (TyFun T0 U0)
Lam t0 = Lam t0 eauto. }
Gamma: tyenv
T, U: {bind ty}
t0: {bind term}
IHjf: forall (t : {bind term}) (T0 U : ty),
Lam t0 = Lam t ->
star sub (TyAll T) (TyFun T0 U) ->
jf (T0 .: Gamma) t U
H: jf Gamma (Lam t0) (TyAll T)
T0, U0: ty
H2: star sub T.[U/] (TyFun T0 U0)
star sub (TyAll T) (TyFun T0 U0)
    {
Gamma: tyenv
T, U: {bind ty}
t0: {bind term}
IHjf: forall (t : {bind term}) (T0 U : ty),
Lam t0 = Lam t ->
star sub (TyAll T) (TyFun T0 U) ->
jf (T0 .: Gamma) t U
H: jf Gamma (Lam t0) (TyAll T)
T0, U0: ty
H2: star sub T.[U/] (TyFun T0 U0)
star sub (TyAll T) (TyFun T0 U0) eauto using sub with sequences. } }
Gamma: var -> ty
T: ty
t0: {bind term}
IHjf: forall (t : {bind term}) (T0 U : ty),
Lam t0 = Lam t ->
star sub T (TyFun T0 U) ->
jf (T0 .: Gamma >> ren (+1)) t U
H: jf (Gamma >> ren (+1)) (Lam t0) T
T0, U: ty
H2: star sub (TyAll T) (TyFun T0 U)
jf (T0 .: Gamma) t0 U

  (* Case: JTyAbs. *)
  {
Gamma: var -> ty
T: ty
t0: {bind term}
IHjf: forall (t : {bind term}) (T0 U : ty),
Lam t0 = Lam t ->
star sub T (TyFun T0 U) ->
jf (T0 .: Gamma >> ren (+1)) t U
H: jf (Gamma >> ren (+1)) (Lam t0) T
T0, U: ty
H2: star sub (TyAll T) (TyFun T0 U)
jf (T0 .: Gamma) t0 U (* We have a hypothesis `star sub (TyAll T') (TyFun T U)`.
       Considering the definition of the relation `sub`, this must be
       a sequence of at least one subtyping step. To let Coq see this,
       we again perform case analysis. *)
    pick star invert.
Gamma: var -> ty
T: ty
t0: {bind term}
IHjf: forall (t : {bind term}) (T0 U : ty),
Lam t0 = Lam t ->
star sub T (TyFun T0 U) ->
jf (T0 .: Gamma >> ren (+1)) t U
H: jf (Gamma >> ren (+1)) (Lam t0) T
T0, U, b: ty
H0: sub (TyAll T) b
H1: star sub b (TyFun T0 U)
jf (T0 .: Gamma) t0 U pick sub invert.
Gamma: var -> ty
T: ty
t0: {bind term}
IHjf: forall (t : {bind term}) (T0 U : ty),
Lam t0 = Lam t ->
star sub T (TyFun T0 U) ->
jf (T0 .: Gamma >> ren (+1)) t U
H: jf (Gamma >> ren (+1)) (Lam t0) T
T0, U: ty
U0: {bind ty}
H1: star sub T.[U0/] (TyFun T0 U)
jf (T0 .: Gamma) t0 U
    (* Thus, we have one subtyping step from `TyAll T'` to `T'.[U'/]`,
       and from there, the rest of the subtyping sequence leads to
       `TyFun T U`. *)
    (* We are looking at a type abstraction. The term `Lam t` is
       polymorphic: the hypothesis `jf (Gamma >> ren (+1)) (Lam t) T'`
       shows that the term `Lam t` has been type-checked in the
       presence of a new type variable numbered 0. The idea is to
       instantiate this type variable with the type `U'` so as to
       obtain `jf Gamma (Lam t) T'.[U'/]`. Then, we hope to be able to
       exploit the induction hypothesis. Let's try: *)
    forward jf_ty_substitution_0.
Gamma: var -> ty
T: ty
t0: {bind term}
IHjf: forall (t : {bind term}) (T0 U : ty),
Lam t0 = Lam t ->
star sub T (TyFun T0 U) ->
jf (T0 .: Gamma >> ren (+1)) t U
H: jf (Gamma >> ren (+1)) (Lam t0) T
T0, U: ty
U0: {bind ty}
H1: star sub T.[U0/] (TyFun T0 U)
H0: jf Gamma (Lam t0) T.[?Goal/]
jf (T0 .: Gamma) t0 U
    (* The first step has worked: we have `jf Gamma (Lam t) T'.[U'/]`.
       Unfortunately, this new judgement, which has been produced by
       the lemma [jf_ty_substitution_0], is not a child of the typing
       judgement over which we are performing structural induction.
       Thus, there is no induction hypothesis for it. We are stuck. *)
Abort.

An inversion lemma (final attempt)

If we had an explicit syntax for type abstractions and type applications, we would see that what we are doing in the previous proof attempt is to reduce a type redex (that is, a type application of a type abstraction). The difficulty that we are hitting is to prove that this process must terminate.

The intuitive reason why it must terminate is that a type derivation for the term Lam t must end with a finite number of uses of the typing rules JFTyAbs and JFTyApp, and our proof peels them away one by one. Crucially, we must argue that our use of the type substitution lemma jf_ty_substitution_0 preserves the structure of the derivation, so does not increase the number of uses of JFTyAbs and JFTyApp.

To do this, we introduce an auxiliary typing judgment, jtn. (See SystemFLemmas.) This judgement is parameterized with an integer n that counts the number of uses of JFTyAbs and JFTyApp at the root of a type derivation. This allows us to prove the lemma invert_jtn_Lam_TyFun by induction on n.

We show that the judgements jtn and jf are equivalent, that is, jf can be viewed as a version of jtn where the parameter n is ignored. (See SystemFLemmas.) Thus, we can reason in terms of jtn where necessary, and use the simpler judgement jf elsewhere.

Lemma invert_jtn_Lam_TyFun:
  forall n Gamma t T' T U,
  jtn n Gamma (Lam t) T' ->
  star sub T' (TyFun T U) ->
  jt (T .: Gamma) t U.
forall (n : nat) (Gamma : tyenv) (t : {bind term})
  (T' T U : ty),
jtn n Gamma (Lam t) T' ->
star sub T' (TyFun T U) -> jt (T .: Gamma) t U
Proof.
forall (n : nat) (Gamma : tyenv) (t : {bind term})
  (T' T U : ty),
jtn n Gamma (Lam t) T' ->
star sub T' (TyFun T U) -> jt (T .: Gamma) t U
  (* By induction on `n`, and by case analysis on the typing
     judgement. *)
  induction n; inversion 1; intros; subst.
Gamma: tyenv
t: {bind term}
T, U, T0, U0: ty
H: jtn 0 Gamma (Lam t) (TyFun T0 U0)
n: nat
H1: jtn n (T0 .: Gamma) t U0
H3: star sub (TyFun T0 U0) (TyFun T U)
jt (T .: Gamma) t U
n: nat
IHn: forall (Gamma : tyenv) (t : {bind term})
  (T' T U : ty),
jtn n Gamma (Lam t) T' ->
star sub T' (TyFun T U) -> jt (T .: Gamma) t U
Gamma: tyenv
t: {bind term}
T, U, T0: ty
H: jtn (S n) Gamma (Lam t) (TyAll T0)
H1: jtn n (Gamma >> ren (+1)) (Lam t) T0
H6: star sub (TyAll T0) (TyFun T U)
jt (T .: Gamma) t U
n: nat
IHn: forall (Gamma : tyenv) (t : {bind term})
  (T' T U : ty),
jtn n Gamma (Lam t) T' ->
star sub T' (TyFun T U) -> jt (T .: Gamma) t U
Gamma: tyenv
t: {bind term}
T, U: ty
T0, U0: {bind ty}
H: jtn (S n) Gamma (Lam t) T0.[U0/]
H1: jtn n Gamma (Lam t) (TyAll T0)
H6: star sub T0.[U0/] (TyFun T U)
jt (T .: Gamma) t U

  (* Case: `n` is 0. The type derivation must end with `JTNLam`. *)
  {
Gamma: tyenv
t: {bind term}
T, U, T0, U0: ty
H: jtn 0 Gamma (Lam t) (TyFun T0 U0)
n: nat
H1: jtn n (T0 .: Gamma) t U0
H3: star sub (TyFun T0 U0) (TyFun T U)
jt (T .: Gamma) t U (* We have a hypothesis `star sub (TyFun T' U') (TyFun T U)`.
       Considering the definition of the relation `sub`, this must be
       a sequence of zero subtyping steps, so we must have `T' = T`
       and `U' = U`. To let Coq see this, it suffices to perform case
       analysis. (One could also make it a separate lemma, for
       clarity.) *)
    pick star invert; [ | pick sub invert ].
Gamma: tyenv
t: {bind term}
T, U: ty
H: jtn 0 Gamma (Lam t) (TyFun T U)
n: nat
H1: jtn n (T .: Gamma) t U
jt (T .: Gamma) t U
    (* The result is then immediate. *)
    eauto with jt. }
n: nat
IHn: forall (Gamma : tyenv) (t : {bind term})
  (T' T U : ty),
jtn n Gamma (Lam t) T' ->
star sub T' (TyFun T U) -> jt (T .: Gamma) t U
Gamma: tyenv
t: {bind term}
T, U, T0: ty
H: jtn (S n) Gamma (Lam t) (TyAll T0)
H1: jtn n (Gamma >> ren (+1)) (Lam t) T0
H6: star sub (TyAll T0) (TyFun T U)
jt (T .: Gamma) t U
n: nat
IHn: forall (Gamma : tyenv) (t : {bind term})
  (T' T U : ty),
jtn n Gamma (Lam t) T' ->
star sub T' (TyFun T U) -> jt (T .: Gamma) t U
Gamma: tyenv
t: {bind term}
T, U: ty
T0, U0: {bind ty}
H: jtn (S n) Gamma (Lam t) T0.[U0/]
H1: jtn n Gamma (Lam t) (TyAll T0)
H6: star sub T0.[U0/] (TyFun T U)
jt (T .: Gamma) t U

  (* Case: `n` is `S m`. The type derivation ends with `JTNTyAbs`. *)
  {
n: nat
IHn: forall (Gamma : tyenv) (t : {bind term})
  (T' T U : ty),
jtn n Gamma (Lam t) T' ->
star sub T' (TyFun T U) -> jt (T .: Gamma) t U
Gamma: tyenv
t: {bind term}
T, U, T0: ty
H: jtn (S n) Gamma (Lam t) (TyAll T0)
H1: jtn n (Gamma >> ren (+1)) (Lam t) T0
H6: star sub (TyAll T0) (TyFun T U)
jt (T .: Gamma) t U (* We have a hypothesis `star sub (TyAll T') (TyFun T U)`.
       Considering the definition of the relation `sub`, this must be
       a sequence of at least one subtyping step. To let Coq see this,
       we again perform case analysis. *)
    pick star invert.
n: nat
IHn: forall (Gamma : tyenv) (t : {bind term})
  (T' T U : ty),
jtn n Gamma (Lam t) T' ->
star sub T' (TyFun T U) -> jt (T .: Gamma) t U
Gamma: tyenv
t: {bind term}
T, U, T0: ty
H: jtn (S n) Gamma (Lam t) (TyAll T0)
H1: jtn n (Gamma >> ren (+1)) (Lam t) T0
b: ty
H0: sub (TyAll T0) b
H2: star sub b (TyFun T U)
jt (T .: Gamma) t U pick sub invert.
n: nat
IHn: forall (Gamma : tyenv) (t : {bind term})
  (T' T U : ty),
jtn n Gamma (Lam t) T' ->
star sub T' (TyFun T U) -> jt (T .: Gamma) t U
Gamma: tyenv
t: {bind term}
T, U, T0: ty
H: jtn (S n) Gamma (Lam t) (TyAll T0)
H1: jtn n (Gamma >> ren (+1)) (Lam t) T0
U0: {bind ty}
H2: star sub T0.[U0/] (TyFun T U)
jt (T .: Gamma) t U
    (* Thus, we have one subtyping step from `TyAll T'` to `T'.[U'/]`,
       and from there, the rest of the subtyping sequence leads to
       `TyFun T U`. We are looking at a type abstraction: the idea is
       to instantiate this abstraction by substituting the type `U'`
       for the type variable `0`, and then to use the induction
       hypothesis. (This exploits the fact that `jtn_ty_substitution`
       preserves the size of the type derivation.) We express this
       idea, in backward style, by instructing Coq that the proof ends
       with an application of the induction hypothesis: *)
    eapply IHn; [ | eauto ].
n: nat
IHn: forall (Gamma : tyenv) (t : {bind term})
  (T' T U : ty),
jtn n Gamma (Lam t) T' ->
star sub T' (TyFun T U) -> jt (T .: Gamma) t U
Gamma: tyenv
t: {bind term}
T, U, T0: ty
H: jtn (S n) Gamma (Lam t) (TyAll T0)
H1: jtn n (Gamma >> ren (+1)) (Lam t) T0
U0: {bind ty}
H2: star sub T0.[U0/] (TyFun T U)
jtn n Gamma (Lam t) T0.[U0/]
    (* The goal is now to prove that `Lam t` has type `T'.[U'/]` under
       `Gamma`. We know that it has type `TyAll T'` under `Gamma >>
       ren (+1)`, so this is exactly the type substitution lemma. *)
    eauto using jtn_ty_substitution_0. }
n: nat
IHn: forall (Gamma : tyenv) (t : {bind term})
  (T' T U : ty),
jtn n Gamma (Lam t) T' ->
star sub T' (TyFun T U) -> jt (T .: Gamma) t U
Gamma: tyenv
t: {bind term}
T, U: ty
T0, U0: {bind ty}
H: jtn (S n) Gamma (Lam t) T0.[U0/]
H1: jtn n Gamma (Lam t) (TyAll T0)
H6: star sub T0.[U0/] (TyFun T U)
jt (T .: Gamma) t U

  (* Case: `n` is `S m`. The type derivation ends with `JTNApp`. *)
  {
n: nat
IHn: forall (Gamma : tyenv) (t : {bind term})
  (T' T U : ty),
jtn n Gamma (Lam t) T' ->
star sub T' (TyFun T U) -> jt (T .: Gamma) t U
Gamma: tyenv
t: {bind term}
T, U: ty
T0, U0: {bind ty}
H: jtn (S n) Gamma (Lam t) T0.[U0/]
H1: jtn n Gamma (Lam t) (TyAll T0)
H6: star sub T0.[U0/] (TyFun T U)
jt (T .: Gamma) t U (* In that case, it suffices to invoke the induction hypothesis.
       The subtyping sequence `star sub ...` grows by one, as one more
       step is prepended to it. This is precisely the reason why the
       lemma was formulated in this general form. *)
    eapply IHn; eauto using sub with sequences. }

Qed.

The inversion lemma can be reformulated in terms of jf.

Lemma invert_jf_Lam_TyFun:
  forall Gamma t T U,
  jf Gamma (Lam t) (TyFun T U) ->
  jf (T .: Gamma) t U.
forall (Gamma : tyenv) (t : {bind term}) (T U : ty),
jf Gamma (Lam t) (TyFun T U) -> jf (T .: Gamma) t U
Proof.
forall (Gamma : tyenv) (t : {bind term}) (T U : ty),
jf Gamma (Lam t) (TyFun T U) -> jf (T .: Gamma) t U
  intros.
Gamma: tyenv
t: {bind term}
T, U: ty
H: jf Gamma (Lam t) (TyFun T U)
jf (T .: Gamma) t U
  forward jf_jt.
Gamma: tyenv
t: {bind term}
T, U: ty
H: jf Gamma (Lam t) (TyFun T U)
H0: jt Gamma (Lam t) (TyFun T U)
jf (T .: Gamma) t U unfold jt in *.
Gamma: tyenv
t: {bind term}
T, U: ty
H: jf Gamma (Lam t) (TyFun T U)
H0: exists n : nat, jtn n Gamma (Lam t) (TyFun T U)
jf (T .: Gamma) t U unpack.
Gamma: tyenv
t: {bind term}
T, U: ty
H: jf Gamma (Lam t) (TyFun T U)
x: nat
H0: jtn x Gamma (Lam t) (TyFun T U)
jf (T .: Gamma) t U
  forward invert_jtn_Lam_TyFun.
Gamma: tyenv
t: {bind term}
T, U: ty
H: jf Gamma (Lam t) (TyFun T U)
x: nat
H0: jtn x Gamma (Lam t) (TyFun T U)
fact:= jt (?Goal .: Gamma) t ?Goal0: Prop
star sub (TyFun T U) (TyFun ?Goal ?Goal0)
Gamma: tyenv
t: {bind term}
T, U: ty
H: jf Gamma (Lam t) (TyFun T U)
x: nat
H0: jtn x Gamma (Lam t) (TyFun T U)
H1: jt (?Goal .: Gamma) t ?Goal0
jf (T .: Gamma) t U {
Gamma: tyenv
t: {bind term}
T, U: ty
H: jf Gamma (Lam t) (TyFun T U)
x: nat
H0: jtn x Gamma (Lam t) (TyFun T U)
fact:= jt (?Goal .: Gamma) t ?Goal0: Prop
star sub (TyFun T U) (TyFun ?Goal ?Goal0) eauto with sequences. }
Gamma: tyenv
t: {bind term}
T, U: ty
H: jf Gamma (Lam t) (TyFun T U)
x: nat
H0: jtn x Gamma (Lam t) (TyFun T U)
H1: jt (T .: Gamma) t U
jf (T .: Gamma) t U
  eauto using jt_jf.
Qed.

Type preservation

The typing judgement is preserved by one step of reduction.

Lemma jf_preservation:
  forall Gamma t T,
  jf Gamma t T ->
  forall t',
  cbv t t' ->
  jf Gamma t' T.
forall (Gamma : tyenv) (t : term) (T : ty),
jf Gamma t T ->
forall t' : term, cbv t t' -> jf Gamma t' T
Proof.
forall (Gamma : tyenv) (t : term) (T : ty),
jf Gamma t T ->
forall t' : term, cbv t t' -> jf Gamma t' T
  (* By induction on the type derivation. *)
  induction 1; intros; subst; try solve [ invert_cbv ].
Gamma: tyenv
t1, t2: term
T, U: ty
H: jf Gamma t1 (TyFun T U)
H0: jf Gamma t2 T
IHjf1: forall t' : term,
cbv t1 t' -> jf Gamma t' (TyFun T U)
IHjf2: forall t' : term, cbv t2 t' -> jf Gamma t' T
t': term
H1: cbv (App t1 t2) t'
jf Gamma t' U
Gamma: var -> ty
t: term
T: ty
H: jf (Gamma >> ren (+1)) t T
IHjf: forall t' : term,
cbv t t' -> jf (Gamma >> ren (+1)) t' T
t': term
H1: cbv t t'
jf Gamma t' (TyAll T)
Gamma: tyenv
t: term
T, U: {bind ty}
H: jf Gamma t (TyAll T)
IHjf: forall t' : term,
cbv t t' -> jf Gamma t' (TyAll T)
t': term
H1: cbv t t'
jf Gamma t' T.[U/]
  (* JFApp *)
  { (* By case analysis on `cbv t t'`. *)
Gamma: tyenv
t1, t2: term
T, U: ty
H: jf Gamma t1 (TyFun T U)
H0: jf Gamma t2 T
IHjf1: forall t' : term,
cbv t1 t' -> jf Gamma t' (TyFun T U)
IHjf2: forall t' : term, cbv t2 t' -> jf Gamma t' T
t': term
H1: cbv (App t1 t2) t'
jf Gamma t' U
    invert_cbv.
Gamma: tyenv
t2: term
T, U: ty
t: term
H: jf Gamma (Lam t) (TyFun T U)
H0: jf Gamma t2 T
IHjf1: forall t' : term,
cbv (Lam t) t' -> jf Gamma t' (TyFun T U)
IHjf2: forall t' : term, cbv t2 t' -> jf Gamma t' T
H4: cbv_mask RuleBetaV
H5: is_value t2
jf Gamma t.[t2/] U
Gamma: tyenv
t1, t2: term
T, U: ty
H: jf Gamma t1 (TyFun T U)
H0: jf Gamma t2 T
IHjf1: forall t' : term,
cbv t1 t' -> jf Gamma t' (TyFun T U)
IHjf2: forall t' : term, cbv t2 t' -> jf Gamma t' T
t3: term
H4: cbv_mask RuleAppL
H6: cbv t1 t3
jf Gamma (App t3 t2) U
Gamma: tyenv
t1, t2: term
T, U: ty
H: jf Gamma t1 (TyFun T U)
H0: jf Gamma t2 T
IHjf1: forall t' : term,
cbv t1 t' -> jf Gamma t' (TyFun T U)
IHjf2: forall t' : term, cbv t2 t' -> jf Gamma t' T
u2: term
H4: cbv_mask RuleAppVR
H5: is_value t1
H7: cbv t2 u2
jf Gamma (App t1 u2) U
    (* RedBetaV. A beta-redex, `App (Lam t) v`, reduces to `t.[v/]`. *)
    { (* The idea is to substitute `v` for the variable `0`. *)
Gamma: tyenv
t2: term
T, U: ty
t: term
H: jf Gamma (Lam t) (TyFun T U)
H0: jf Gamma t2 T
IHjf1: forall t' : term,
cbv (Lam t) t' -> jf Gamma t' (TyFun T U)
IHjf2: forall t' : term, cbv t2 t' -> jf Gamma t' T
H4: cbv_mask RuleBetaV
H5: is_value t2
jf Gamma t.[t2/] U
      eapply jf_te_substitution_0; eauto with jf.
Gamma: tyenv
t2: term
T, U: ty
t: term
H: jf Gamma (Lam t) (TyFun T U)
H0: jf Gamma t2 T
IHjf1: forall t' : term,
cbv (Lam t) t' -> jf Gamma t' (TyFun T U)
IHjf2: forall t' : term, cbv t2 t' -> jf Gamma t' T
H4: cbv_mask RuleBetaV
H5: is_value t2
jf (T .: Gamma) t U
      (* This requires us to prove that the function body `t` is
         well-typed under an extended type environment `T .: Gamma`.
         Fortunately, this is guaranteed by the inversion lemma
         `invert_jf_Lam_TyFun`. *)
      eapply invert_jf_Lam_TyFun; eauto with sequences. }
Gamma: tyenv
t1, t2: term
T, U: ty
H: jf Gamma t1 (TyFun T U)
H0: jf Gamma t2 T
IHjf1: forall t' : term,
cbv t1 t' -> jf Gamma t' (TyFun T U)
IHjf2: forall t' : term, cbv t2 t' -> jf Gamma t' T
t3: term
H4: cbv_mask RuleAppL
H6: cbv t1 t3
jf Gamma (App t3 t2) U
Gamma: tyenv
t1, t2: term
T, U: ty
H: jf Gamma t1 (TyFun T U)
H0: jf Gamma t2 T
IHjf1: forall t' : term,
cbv t1 t' -> jf Gamma t' (TyFun T U)
IHjf2: forall t' : term, cbv t2 t' -> jf Gamma t' T
u2: term
H4: cbv_mask RuleAppVR
H5: is_value t1
H7: cbv t2 u2
jf Gamma (App t1 u2) U
    (* RedAppL. *)
    {
Gamma: tyenv
t1, t2: term
T, U: ty
H: jf Gamma t1 (TyFun T U)
H0: jf Gamma t2 T
IHjf1: forall t' : term,
cbv t1 t' -> jf Gamma t' (TyFun T U)
IHjf2: forall t' : term, cbv t2 t' -> jf Gamma t' T
t3: term
H4: cbv_mask RuleAppL
H6: cbv t1 t3
jf Gamma (App t3 t2) U eauto with jf. }
Gamma: tyenv
t1, t2: term
T, U: ty
H: jf Gamma t1 (TyFun T U)
H0: jf Gamma t2 T
IHjf1: forall t' : term,
cbv t1 t' -> jf Gamma t' (TyFun T U)
IHjf2: forall t' : term, cbv t2 t' -> jf Gamma t' T
u2: term
H4: cbv_mask RuleAppVR
H5: is_value t1
H7: cbv t2 u2
jf Gamma (App t1 u2) U
    (* RedAppVR. *)
    {
Gamma: tyenv
t1, t2: term
T, U: ty
H: jf Gamma t1 (TyFun T U)
H0: jf Gamma t2 T
IHjf1: forall t' : term,
cbv t1 t' -> jf Gamma t' (TyFun T U)
IHjf2: forall t' : term, cbv t2 t' -> jf Gamma t' T
u2: term
H4: cbv_mask RuleAppVR
H5: is_value t1
H7: cbv t2 u2
jf Gamma (App t1 u2) U eauto with jf. }
  }
Gamma: var -> ty
t: term
T: ty
H: jf (Gamma >> ren (+1)) t T
IHjf: forall t' : term,
cbv t t' -> jf (Gamma >> ren (+1)) t' T
t': term
H1: cbv t t'
jf Gamma t' (TyAll T)
Gamma: tyenv
t: term
T, U: {bind ty}
H: jf Gamma t (TyAll T)
IHjf: forall t' : term,
cbv t t' -> jf Gamma t' (TyAll T)
t': term
H1: cbv t t'
jf Gamma t' T.[U/]
  (* JTNTyAbs *)
  {
Gamma: var -> ty
t: term
T: ty
H: jf (Gamma >> ren (+1)) t T
IHjf: forall t' : term,
cbv t t' -> jf (Gamma >> ren (+1)) t' T
t': term
H1: cbv t t'
jf Gamma t' (TyAll T) eauto with jf. }
Gamma: tyenv
t: term
T, U: {bind ty}
H: jf Gamma t (TyAll T)
IHjf: forall t' : term,
cbv t t' -> jf Gamma t' (TyAll T)
t': term
H1: cbv t t'
jf Gamma t' T.[U/]
  (* JTNTyApp *)
  {
Gamma: tyenv
t: term
T, U: {bind ty}
H: jf Gamma t (TyAll T)
IHjf: forall t' : term,
cbv t t' -> jf Gamma t' (TyAll T)
t': term
H1: cbv t t'
jf Gamma t' T.[U/] eauto with jf. }
Qed.

Progress

An inversion lemma: if a closed value admits a function type TyFun T1 T2, then it must be a lambda-abstraction.

Lemma invert_jtn_TyFun:
  forall n Gamma t T,
  jtn n Gamma t T ->
  forall T1 T2,
  star sub T (TyFun T1 T2) ->
  closed t ->
  is_value t ->
  exists t', t = Lam t'.
forall (n : nat) (Gamma : tyenv) (t : term) (T : ty),
jtn n Gamma t T ->
forall T1 T2 : ty,
star sub T (TyFun T1 T2) ->
closed t ->
is_value t -> exists t' : {bind term}, t = Lam t'
Proof.
forall (n : nat) (Gamma : tyenv) (t : term) (T : ty),
jtn n Gamma t T ->
forall T1 T2 : ty,
star sub T (TyFun T1 T2) ->
closed t ->
is_value t -> exists t' : {bind term}, t = Lam t'
  (* We do not comment this proof in detail. It is analogous in its
     general structure to the proof of `invert_jtn_Lam_TyFun`. *)
  induction n; inversion 1; intros; subst;
  try solve [ false; eauto with closed ].
Gamma: tyenv
t0: term
T0, U: ty
H: jtn 0 Gamma (Lam t0) (TyFun T0 U)
n: nat
H0: jtn n (T0 .: Gamma) t0 U
T1, T2: ty
H1: star sub (TyFun T0 U) (TyFun T1 T2)
H5: closed (Lam t0)
H6: is_value (Lam t0)
exists t' : {bind term}, Lam t0 = Lam t'
n: nat
IHn: forall (Gamma : tyenv) (t : term) (T : ty),
jtn n Gamma t T ->
forall T1 T2 : ty,
star sub T (TyFun T1 T2) ->
closed t ->
is_value t ->
exists t' : {bind term}, t = Lam t'
Gamma: tyenv
t: term
T0: ty
H: jtn (S n) Gamma t (TyAll T0)
H1: jtn n (Gamma >> ren (+1)) t T0
T1, T2: ty
H6: star sub (TyAll T0) (TyFun T1 T2)
H7: closed t
H8: is_value t
exists t' : {bind term}, t = Lam t'
n: nat
IHn: forall (Gamma : tyenv) (t : term) (T : ty),
jtn n Gamma t T ->
forall T1 T2 : ty,
star sub T (TyFun T1 T2) ->
closed t ->
is_value t ->
exists t' : {bind term}, t = Lam t'
Gamma: tyenv
t: term
T0, U: {bind ty}
H: jtn (S n) Gamma t T0.[U/]
H1: jtn n Gamma t (TyAll T0)
T1, T2: ty
H6: star sub T0.[U/] (TyFun T1 T2)
H7: closed t
H8: is_value t
exists t' : {bind term}, t = Lam t'

  (* Case: JTNLam. *)
  {
Gamma: tyenv
t0: term
T0, U: ty
H: jtn 0 Gamma (Lam t0) (TyFun T0 U)
n: nat
H0: jtn n (T0 .: Gamma) t0 U
T1, T2: ty
H1: star sub (TyFun T0 U) (TyFun T1 T2)
H5: closed (Lam t0)
H6: is_value (Lam t0)
exists t' : {bind term}, Lam t0 = Lam t' eauto. }
n: nat
IHn: forall (Gamma : tyenv) (t : term) (T : ty),
jtn n Gamma t T ->
forall T1 T2 : ty,
star sub T (TyFun T1 T2) ->
closed t ->
is_value t ->
exists t' : {bind term}, t = Lam t'
Gamma: tyenv
t: term
T0: ty
H: jtn (S n) Gamma t (TyAll T0)
H1: jtn n (Gamma >> ren (+1)) t T0
T1, T2: ty
H6: star sub (TyAll T0) (TyFun T1 T2)
H7: closed t
H8: is_value t
exists t' : {bind term}, t = Lam t'
n: nat
IHn: forall (Gamma : tyenv) (t : term) (T : ty),
jtn n Gamma t T ->
forall T1 T2 : ty,
star sub T (TyFun T1 T2) ->
closed t ->
is_value t ->
exists t' : {bind term}, t = Lam t'
Gamma: tyenv
t: term
T0, U: {bind ty}
H: jtn (S n) Gamma t T0.[U/]
H1: jtn n Gamma t (TyAll T0)
T1, T2: ty
H6: star sub T0.[U/] (TyFun T1 T2)
H7: closed t
H8: is_value t
exists t' : {bind term}, t = Lam t'

  (* Case: JTNTyAbs. *)
  {
n: nat
IHn: forall (Gamma : tyenv) (t : term) (T : ty),
jtn n Gamma t T ->
forall T1 T2 : ty,
star sub T (TyFun T1 T2) ->
closed t ->
is_value t ->
exists t' : {bind term}, t = Lam t'
Gamma: tyenv
t: term
T0: ty
H: jtn (S n) Gamma t (TyAll T0)
H1: jtn n (Gamma >> ren (+1)) t T0
T1, T2: ty
H6: star sub (TyAll T0) (TyFun T1 T2)
H7: closed t
H8: is_value t
exists t' : {bind term}, t = Lam t' pick star invert.
n: nat
IHn: forall (Gamma : tyenv) (t : term) (T : ty),
jtn n Gamma t T ->
forall T1 T2 : ty,
star sub T (TyFun T1 T2) ->
closed t ->
is_value t ->
exists t' : {bind term}, t = Lam t'
Gamma: tyenv
t: term
T0: ty
H: jtn (S n) Gamma t (TyAll T0)
H1: jtn n (Gamma >> ren (+1)) t T0
T1, T2: ty
H7: closed t
H8: is_value t
b: ty
H0: sub (TyAll T0) b
H2: star sub b (TyFun T1 T2)
exists t' : {bind term}, t = Lam t' pick sub invert.
n: nat
IHn: forall (Gamma : tyenv) (t : term) (T : ty),
jtn n Gamma t T ->
forall T1 T2 : ty,
star sub T (TyFun T1 T2) ->
closed t ->
is_value t ->
exists t' : {bind term}, t = Lam t'
Gamma: tyenv
t: term
T0: ty
H: jtn (S n) Gamma t (TyAll T0)
H1: jtn n (Gamma >> ren (+1)) t T0
T1, T2: ty
H7: closed t
H8: is_value t
U: {bind ty}
H2: star sub T0.[U/] (TyFun T1 T2)
exists t' : {bind term}, t = Lam t'
    eapply IHn; [ | eauto | eauto | eauto ].
n: nat
IHn: forall (Gamma : tyenv) (t : term) (T : ty),
jtn n Gamma t T ->
forall T1 T2 : ty,
star sub T (TyFun T1 T2) ->
closed t ->
is_value t ->
exists t' : {bind term}, t = Lam t'
Gamma: tyenv
t: term
T0: ty
H: jtn (S n) Gamma t (TyAll T0)
H1: jtn n (Gamma >> ren (+1)) t T0
T1, T2: ty
H7: closed t
H8: is_value t
U: {bind ty}
H2: star sub T0.[U/] (TyFun T1 T2)
jtn n ?Gamma t T0.[U/]
    eauto using jtn_ty_substitution_0. }
n: nat
IHn: forall (Gamma : tyenv) (t : term) (T : ty),
jtn n Gamma t T ->
forall T1 T2 : ty,
star sub T (TyFun T1 T2) ->
closed t ->
is_value t ->
exists t' : {bind term}, t = Lam t'
Gamma: tyenv
t: term
T0, U: {bind ty}
H: jtn (S n) Gamma t T0.[U/]
H1: jtn n Gamma t (TyAll T0)
T1, T2: ty
H6: star sub T0.[U/] (TyFun T1 T2)
H7: closed t
H8: is_value t
exists t' : {bind term}, t = Lam t'

  (* Case: JTNTyApp. *)
  {
n: nat
IHn: forall (Gamma : tyenv) (t : term) (T : ty),
jtn n Gamma t T ->
forall T1 T2 : ty,
star sub T (TyFun T1 T2) ->
closed t ->
is_value t ->
exists t' : {bind term}, t = Lam t'
Gamma: tyenv
t: term
T0, U: {bind ty}
H: jtn (S n) Gamma t T0.[U/]
H1: jtn n Gamma t (TyAll T0)
T1, T2: ty
H6: star sub T0.[U/] (TyFun T1 T2)
H7: closed t
H8: is_value t
exists t' : {bind term}, t = Lam t' eauto using sub with sequences. }
Qed.

Lemma invert_jf_TyFun:
  forall Gamma t T1 T2,
  jf Gamma t (TyFun T1 T2) ->
  closed t ->
  is_value t ->
  exists t', t = Lam t'.
forall (Gamma : tyenv) (t : term) (T1 T2 : ty),
jf Gamma t (TyFun T1 T2) ->
closed t ->
is_value t -> exists t' : {bind term}, t = Lam t'
Proof.
forall (Gamma : tyenv) (t : term) (T1 T2 : ty),
jf Gamma t (TyFun T1 T2) ->
closed t ->
is_value t -> exists t' : {bind term}, t = Lam t'
  intros.
Gamma: tyenv
t: term
T1, T2: ty
H: jf Gamma t (TyFun T1 T2)
H0: closed t
H1: is_value t
exists t' : {bind term}, t = Lam t'
  forward jf_jt.
Gamma: tyenv
t: term
T1, T2: ty
H: jf Gamma t (TyFun T1 T2)
H0: closed t
H1: is_value t
H2: jt Gamma t (TyFun T1 T2)
exists t' : {bind term}, t = Lam t' unfold jt in *.
Gamma: tyenv
t: term
T1, T2: ty
H: jf Gamma t (TyFun T1 T2)
H0: closed t
H1: is_value t
H2: exists n : nat, jtn n Gamma t (TyFun T1 T2)
exists t' : {bind term}, t = Lam t' unpack.
Gamma: tyenv
t: term
T1, T2: ty
H: jf Gamma t (TyFun T1 T2)
H0: closed t
H1: is_value t
x: nat
H2: jtn x Gamma t (TyFun T1 T2)
exists t' : {bind term}, t = Lam t'
  forward invert_jtn_TyFun.
Gamma: tyenv
t: term
T1, T2: ty
H: jf Gamma t (TyFun T1 T2)
H0: closed t
H1: is_value t
x: nat
H2: jtn x Gamma t (TyFun T1 T2)
fact:= exists t' : {bind term}, t = Lam t': Prop
star sub (TyFun T1 T2) (TyFun ?T1 ?T2)
Gamma: tyenv
T1, T2: ty
x0: {bind term}
H1: is_value (Lam x0)
H0: closed (Lam x0)
H: jf Gamma (Lam x0) (TyFun T1 T2)
x: nat
H2: jtn x Gamma (Lam x0) (TyFun T1 T2)
exists t' : {bind term}, Lam x0 = Lam t' {
Gamma: tyenv
t: term
T1, T2: ty
H: jf Gamma t (TyFun T1 T2)
H0: closed t
H1: is_value t
x: nat
H2: jtn x Gamma t (TyFun T1 T2)
fact:= exists t' : {bind term}, t = Lam t': Prop
star sub (TyFun T1 T2) (TyFun ?T1 ?T2) eauto with sequences. }
Gamma: tyenv
T1, T2: ty
x0: {bind term}
H1: is_value (Lam x0)
H0: closed (Lam x0)
H: jf Gamma (Lam x0) (TyFun T1 T2)
x: nat
H2: jtn x Gamma (Lam x0) (TyFun T1 T2)
exists t' : {bind term}, Lam x0 = Lam t'
  eauto using jt_jf.
Qed.

The progress theorem: a closed, well-typed term must either be able to make one step of reduction or be a value.

Lemma jf_progress:
  forall Gamma t T,
  jf Gamma t T ->
  closed t ->
  (exists t', cbv t t') \/ is_value t.
forall (Gamma : tyenv) (t : term) (T : ty),
jf Gamma t T ->
closed t -> (exists t' : term, cbv t t') \/ is_value t
Ltac use_ih ih :=
  destruct ih; [ eauto with closed | unpack; eauto with red |  ].
forall (Gamma : tyenv) (t : term) (T : ty),
jf Gamma t T ->
closed t -> (exists t' : term, cbv t t') \/ is_value t
Proof.
forall (Gamma : tyenv) (t : term) (T : ty),
jf Gamma t T ->
closed t -> (exists t' : term, cbv t t') \/ is_value t
  (* By induction on the type derivation. *)
  induction 1; intros; subst.
Gamma: var -> ty
x: var
H0: closed (Var x)
(exists t' : term, cbv (Var x) t') \/ is_value (Var x)
Gamma: var -> ty
t: term
T, U: ty
H: jf (T .: Gamma) t U
IHjf: closed t ->
(exists t' : term, cbv t t') \/ is_value t
H0: closed (Lam t)
(exists t' : term, cbv (Lam t) t') \/ is_value (Lam t)
Gamma: tyenv
t1, t2: term
T, U: ty
H: jf Gamma t1 (TyFun T U)
H0: jf Gamma t2 T
IHjf1: closed t1 ->
(exists t' : term, cbv t1 t') \/ is_value t1
IHjf2: closed t2 ->
(exists t' : term, cbv t2 t') \/ is_value t2
H1: closed (App t1 t2)
(exists t' : term, cbv (App t1 t2) t') \/
is_value (App t1 t2)
Gamma: var -> ty
t: term
T: ty
H: jf (Gamma >> ren (+1)) t T
IHjf: closed t ->
(exists t' : term, cbv t t') \/ is_value t
H1: closed t
(exists t' : term, cbv t t') \/ is_value t
Gamma: tyenv
t: term
T, U: {bind ty}
H: jf Gamma t (TyAll T)
IHjf: closed t ->
(exists t' : term, cbv t t') \/ is_value t
H1: closed t
(exists t' : term, cbv t t') \/ is_value t
  (* Case: JFVar. *)
  {
Gamma: var -> ty
x: var
H0: closed (Var x)
(exists t' : term, cbv (Var x) t') \/ is_value (Var x) false.
Gamma: var -> ty
x: var
H0: closed (Var x)
False eauto with closed. }
Gamma: var -> ty
t: term
T, U: ty
H: jf (T .: Gamma) t U
IHjf: closed t ->
(exists t' : term, cbv t t') \/ is_value t
H0: closed (Lam t)
(exists t' : term, cbv (Lam t) t') \/ is_value (Lam t)
Gamma: tyenv
t1, t2: term
T, U: ty
H: jf Gamma t1 (TyFun T U)
H0: jf Gamma t2 T
IHjf1: closed t1 ->
(exists t' : term, cbv t1 t') \/ is_value t1
IHjf2: closed t2 ->
(exists t' : term, cbv t2 t') \/ is_value t2
H1: closed (App t1 t2)
(exists t' : term, cbv (App t1 t2) t') \/
is_value (App t1 t2)
Gamma: var -> ty
t: term
T: ty
H: jf (Gamma >> ren (+1)) t T
IHjf: closed t ->
(exists t' : term, cbv t t') \/ is_value t
H1: closed t
(exists t' : term, cbv t t') \/ is_value t
Gamma: tyenv
t: term
T, U: {bind ty}
H: jf Gamma t (TyAll T)
IHjf: closed t ->
(exists t' : term, cbv t t') \/ is_value t
H1: closed t
(exists t' : term, cbv t t') \/ is_value t
  (* Case: JFLam. *)
  {
Gamma: var -> ty
t: term
T, U: ty
H: jf (T .: Gamma) t U
IHjf: closed t ->
(exists t' : term, cbv t t') \/ is_value t
H0: closed (Lam t)
(exists t' : term, cbv (Lam t) t') \/ is_value (Lam t) obvious. }
Gamma: tyenv
t1, t2: term
T, U: ty
H: jf Gamma t1 (TyFun T U)
H0: jf Gamma t2 T
IHjf1: closed t1 ->
(exists t' : term, cbv t1 t') \/ is_value t1
IHjf2: closed t2 ->
(exists t' : term, cbv t2 t') \/ is_value t2
H1: closed (App t1 t2)
(exists t' : term, cbv (App t1 t2) t') \/
is_value (App t1 t2)
Gamma: var -> ty
t: term
T: ty
H: jf (Gamma >> ren (+1)) t T
IHjf: closed t ->
(exists t' : term, cbv t t') \/ is_value t
H1: closed t
(exists t' : term, cbv t t') \/ is_value t
Gamma: tyenv
t: term
T, U: {bind ty}
H: jf Gamma t (TyAll T)
IHjf: closed t ->
(exists t' : term, cbv t t') \/ is_value t
H1: closed t
(exists t' : term, cbv t t') \/ is_value t
  (* Case: JFApp. *)
  {
Gamma: tyenv
t1, t2: term
T, U: ty
H: jf Gamma t1 (TyFun T U)
H0: jf Gamma t2 T
IHjf1: closed t1 ->
(exists t' : term, cbv t1 t') \/ is_value t1
IHjf2: closed t2 ->
(exists t' : term, cbv t2 t') \/ is_value t2
H1: closed (App t1 t2)
(exists t' : term, cbv (App t1 t2) t') \/
is_value (App t1 t2) use_ih IHjf1.
Gamma: tyenv
t1, t2: term
T, U: ty
H: jf Gamma t1 (TyFun T U)
H0: jf Gamma t2 T
IHjf2: closed t2 ->
(exists t' : term, cbv t2 t') \/ is_value t2
H1: closed (App t1 t2)
H2: is_value t1
(exists t' : term, cbv (App t1 t2) t') \/
is_value (App t1 t2)
    use_ih IHjf2.
Gamma: tyenv
t1, t2: term
T, U: ty
H: jf Gamma t1 (TyFun T U)
H0: jf Gamma t2 T
H1: closed (App t1 t2)
H2: is_value t1
H3: is_value t2
(exists t' : term, cbv (App t1 t2) t') \/
is_value (App t1 t2)
    left.
Gamma: tyenv
t1, t2: term
T, U: ty
H: jf Gamma t1 (TyFun T U)
H0: jf Gamma t2 T
H1: closed (App t1 t2)
H2: is_value t1
H3: is_value t2
exists t' : term, cbv (App t1 t2) t'
    (* Because `t1` is a closed value and has a function type,
       it must be a lambda-abstraction. *)
    forward invert_jf_TyFun.
Gamma: tyenv
t1, t2: term
T, U: ty
H: jf Gamma t1 (TyFun T U)
H0: jf Gamma t2 T
H1: closed (App t1 t2)
H2: is_value t1
H3: is_value t2
fact:= exists t' : {bind term}, t1 = Lam t': Prop
closed t1
Gamma: tyenv
t2: term
T, U: ty
x: {bind term}
H: jf Gamma (Lam x) (TyFun T U)
H0: jf Gamma t2 T
H2: is_value (Lam x)
H1: closed (App (Lam x) t2)
H3: is_value t2
exists t' : term, cbv (App (Lam x) t2) t' {
Gamma: tyenv
t1, t2: term
T, U: ty
H: jf Gamma t1 (TyFun T U)
H0: jf Gamma t2 T
H1: closed (App t1 t2)
H2: is_value t1
H3: is_value t2
fact:= exists t' : {bind term}, t1 = Lam t': Prop
closed t1 eauto with closed. }
Gamma: tyenv
t2: term
T, U: ty
x: {bind term}
H: jf Gamma (Lam x) (TyFun T U)
H0: jf Gamma t2 T
H2: is_value (Lam x)
H1: closed (App (Lam x) t2)
H3: is_value t2
exists t' : term, cbv (App (Lam x) t2) t'
    (* Therefore, we have a beta-redex. *)
    obvious. }
Gamma: var -> ty
t: term
T: ty
H: jf (Gamma >> ren (+1)) t T
IHjf: closed t ->
(exists t' : term, cbv t t') \/ is_value t
H1: closed t
(exists t' : term, cbv t t') \/ is_value t
Gamma: tyenv
t: term
T, U: {bind ty}
H: jf Gamma t (TyAll T)
IHjf: closed t ->
(exists t' : term, cbv t t') \/ is_value t
H1: closed t
(exists t' : term, cbv t t') \/ is_value t
  (* Case: JFTyAbs. *)
  {
Gamma: var -> ty
t: term
T: ty
H: jf (Gamma >> ren (+1)) t T
IHjf: closed t ->
(exists t' : term, cbv t t') \/ is_value t
H1: closed t
(exists t' : term, cbv t t') \/ is_value t eauto. }
Gamma: tyenv
t: term
T, U: {bind ty}
H: jf Gamma t (TyAll T)
IHjf: closed t ->
(exists t' : term, cbv t t') \/ is_value t
H1: closed t
(exists t' : term, cbv t t') \/ is_value t
  (* Case: JFTyApp. *)
  {
Gamma: tyenv
t: term
T, U: {bind ty}
H: jf Gamma t (TyAll T)
IHjf: closed t ->
(exists t' : term, cbv t t') \/ is_value t
H1: closed t
(exists t' : term, cbv t t') \/ is_value t eauto. }
Qed.