Require Import MyTactics.
Require Import LambdaCalculusSyntax.
Require Import LambdaCalculusValues.
Require Import LambdaCalculusReduction.
Require Import STLCDefinition.
Require Import STLCLemmas.

This is a failed attempt to prove the lemma jt_te_substitution_0 in a direct way, without introducing the auxiliary judgement js. See STLCLemmas for a valid proof.

Goal (* jt_te_substitution_0 *)
  forall Delta t1 U,
  jt Delta t1 U ->
  forall Gamma t2 T,
  Delta = T .: Gamma ->
  jt Gamma t2 T ->
  jt Gamma t1.[t2/] U.
forall (Delta : tyenv) (t1 : term) (U : ty),
jt Delta t1 U ->
forall (Gamma : var -> ty) (t2 : term) (T : ty),
Delta = T .: Gamma ->
jt Gamma t2 T -> jt Gamma t1.[t2/] U
Proof.
forall (Delta : tyenv) (t1 : term) (U : ty),
jt Delta t1 U ->
forall (Gamma : var -> ty) (t2 : term) (T : ty),
Delta = T .: Gamma ->
jt Gamma t2 T -> jt Gamma t1.[t2/] U
  (* Let us attempt to naively prove this statement by induction. *)
  induction 1; intros; subst; asimpl.
x: var
Gamma0: var -> ty
t2: term
T0: ty
H1: jt Gamma0 t2 T0
jt Gamma0 ((t2 .: ids) x) ((T0 .: Gamma0) x)
t: term
T, U: ty
Gamma0: var -> ty
T0: ty
IHjt: forall (Gamma : var -> ty) 
  (t2 : term) (T1 : ty),
T .: T0 .: Gamma0 = T1 .: Gamma ->
jt Gamma t2 T1 -> jt Gamma t.[t2/] U
H: jt (T .: T0 .: Gamma0) t U
t2: term
H1: jt Gamma0 t2 T0
jt Gamma0 (Lam t.[ids 0 .: lift 1 t2 .: ren (+1)])
  (TyFun T U)
t1, t2: term
T, U: ty
Gamma0: var -> ty
T0: ty
IHjt2: forall (Gamma : var -> ty) 
  (t3 : term) (T1 : ty),
T0 .: Gamma0 = T1 .: Gamma ->
jt Gamma t3 T1 -> jt Gamma t2.[t3/] T
IHjt1: forall (Gamma : var -> ty) 
  (t2 : term) (T1 : ty),
T0 .: Gamma0 = T1 .: Gamma ->
jt Gamma t2 T1 ->
jt Gamma t1.[t2/] (TyFun T U)
H0: jt (T0 .: Gamma0) t2 T
H: jt (T0 .: Gamma0) t1 (TyFun T U)
t0: term
H2: jt Gamma0 t0 T0
jt Gamma0 (App t1.[t0/] t2.[t0/]) U
  all: swap 2 3. (* deal with JTApp before JTLam *)
x: var
Gamma0: var -> ty
t2: term
T0: ty
H1: jt Gamma0 t2 T0
jt Gamma0 ((t2 .: ids) x) ((T0 .: Gamma0) x)
t1, t2: term
T, U: ty
Gamma0: var -> ty
T0: ty
IHjt2: forall (Gamma : var -> ty) 
  (t3 : term) (T1 : ty),
T0 .: Gamma0 = T1 .: Gamma ->
jt Gamma t3 T1 -> jt Gamma t2.[t3/] T
IHjt1: forall (Gamma : var -> ty) 
  (t2 : term) (T1 : ty),
T0 .: Gamma0 = T1 .: Gamma ->
jt Gamma t2 T1 ->
jt Gamma t1.[t2/] (TyFun T U)
H0: jt (T0 .: Gamma0) t2 T
H: jt (T0 .: Gamma0) t1 (TyFun T U)
t0: term
H2: jt Gamma0 t0 T0
jt Gamma0 (App t1.[t0/] t2.[t0/]) U
t: term
T, U: ty
Gamma0: var -> ty
T0: ty
IHjt: forall (Gamma : var -> ty) 
  (t2 : term) (T1 : ty),
T .: T0 .: Gamma0 = T1 .: Gamma ->
jt Gamma t2 T1 -> jt Gamma t.[t2/] U
H: jt (T .: T0 .: Gamma0) t U
t2: term
H1: jt Gamma0 t2 T0
jt Gamma0 (Lam t.[ids 0 .: lift 1 t2 .: ren (+1)])
  (TyFun T U)
  (* JTVar. *)
  { (* By cases on the variable `x`. Either it is zero, or nonzero. *)
x: var
Gamma0: var -> ty
t2: term
T0: ty
H1: jt Gamma0 t2 T0
jt Gamma0 ((t2 .: ids) x) ((T0 .: Gamma0) x)
    destruct x as [|x].
Gamma0: var -> ty
t2: term
T0: ty
H1: jt Gamma0 t2 T0
jt Gamma0 ((t2 .: ids) 0) ((T0 .: Gamma0) 0)
x: nat
Gamma0: var -> ty
t2: term
T0: ty
H1: jt Gamma0 t2 T0
jt Gamma0 ((t2 .: ids) (S x)) ((T0 .: Gamma0) (S x))
    {
Gamma0: var -> ty
t2: term
T0: ty
H1: jt Gamma0 t2 T0
jt Gamma0 ((t2 .: ids) 0) ((T0 .: Gamma0) 0) asimpl.
Gamma0: var -> ty
t2: term
T0: ty
H1: jt Gamma0 t2 T0
jt Gamma0 t2 T0 eauto. }
x: nat
Gamma0: var -> ty
t2: term
T0: ty
H1: jt Gamma0 t2 T0
jt Gamma0 ((t2 .: ids) (S x)) ((T0 .: Gamma0) (S x))
    {
x: nat
Gamma0: var -> ty
t2: term
T0: ty
H1: jt Gamma0 t2 T0
jt Gamma0 ((t2 .: ids) (S x)) ((T0 .: Gamma0) (S x)) asimpl.
x: nat
Gamma0: var -> ty
t2: term
T0: ty
H1: jt Gamma0 t2 T0
jt Gamma0 (ids x) (Gamma0 x) eauto with jt. } }
t1, t2: term
T, U: ty
Gamma0: var -> ty
T0: ty
IHjt2: forall (Gamma : var -> ty) 
  (t3 : term) (T1 : ty),
T0 .: Gamma0 = T1 .: Gamma ->
jt Gamma t3 T1 -> jt Gamma t2.[t3/] T
IHjt1: forall (Gamma : var -> ty) 
  (t2 : term) (T1 : ty),
T0 .: Gamma0 = T1 .: Gamma ->
jt Gamma t2 T1 ->
jt Gamma t1.[t2/] (TyFun T U)
H0: jt (T0 .: Gamma0) t2 T
H: jt (T0 .: Gamma0) t1 (TyFun T U)
t0: term
H2: jt Gamma0 t0 T0
jt Gamma0 (App t1.[t0/] t2.[t0/]) U
t: term
T, U: ty
Gamma0: var -> ty
T0: ty
IHjt: forall (Gamma : var -> ty) 
  (t2 : term) (T1 : ty),
T .: T0 .: Gamma0 = T1 .: Gamma ->
jt Gamma t2 T1 -> jt Gamma t.[t2/] U
H: jt (T .: T0 .: Gamma0) t U
t2: term
H1: jt Gamma0 t2 T0
jt Gamma0 (Lam t.[ids 0 .: lift 1 t2 .: ren (+1)])
  (TyFun T U)
  (* JTApp. *)
  (* This case just works, thanks to the induction hypotheses. *)
  {
t1, t2: term
T, U: ty
Gamma0: var -> ty
T0: ty
IHjt2: forall (Gamma : var -> ty) 
  (t3 : term) (T1 : ty),
T0 .: Gamma0 = T1 .: Gamma ->
jt Gamma t3 T1 -> jt Gamma t2.[t3/] T
IHjt1: forall (Gamma : var -> ty) 
  (t2 : term) (T1 : ty),
T0 .: Gamma0 = T1 .: Gamma ->
jt Gamma t2 T1 ->
jt Gamma t1.[t2/] (TyFun T U)
H0: jt (T0 .: Gamma0) t2 T
H: jt (T0 .: Gamma0) t1 (TyFun T U)
t0: term
H2: jt Gamma0 t0 T0
jt Gamma0 (App t1.[t0/] t2.[t0/]) U eauto with jt. }
t: term
T, U: ty
Gamma0: var -> ty
T0: ty
IHjt: forall (Gamma : var -> ty) 
  (t2 : term) (T1 : ty),
T .: T0 .: Gamma0 = T1 .: Gamma ->
jt Gamma t2 T1 -> jt Gamma t.[t2/] U
H: jt (T .: T0 .: Gamma0) t U
t2: term
H1: jt Gamma0 t2 T0
jt Gamma0 (Lam t.[ids 0 .: lift 1 t2 .: ren (+1)])
  (TyFun T U)
  (* JTLam. *)
  { (* We must typecheck a lambda, so we must apply JTLam. *)
t: term
T, U: ty
Gamma0: var -> ty
T0: ty
IHjt: forall (Gamma : var -> ty) 
  (t2 : term) (T1 : ty),
T .: T0 .: Gamma0 = T1 .: Gamma ->
jt Gamma t2 T1 -> jt Gamma t.[t2/] U
H: jt (T .: T0 .: Gamma0) t U
t2: term
H1: jt Gamma0 t2 T0
jt Gamma0 (Lam t.[ids 0 .: lift 1 t2 .: ren (+1)])
  (TyFun T U)
    eapply JTLam.
t: term
T, U: ty
Gamma0: var -> ty
T0: ty
IHjt: forall (Gamma : var -> ty) 
  (t2 : term) (T1 : ty),
T .: T0 .: Gamma0 = T1 .: Gamma ->
jt Gamma t2 T1 -> jt Gamma t.[t2/] U
H: jt (T .: T0 .: Gamma0) t U
t2: term
H1: jt Gamma0 t2 T0
jt (T .: Gamma0) t.[ids 0 .: lift 1 t2 .: ren (+1)] U
    (* We would now like to apply the induction hypothesis, but this
       fails, because the statement of the lemma allows substituting a
       term for variable 0, but we are now attempting to substitute a
       term for variable 1. *)
    Fail eapply IHjt.
The command has indeed failed with message:
In environment
t : term
T, U : ty
Gamma0 : var -> ty
T0 : ty
IHjt : forall (Gamma : var -> ty) (t2 : term)
         (T1 : ty),
       T .: T0 .: Gamma0 = T1 .: Gamma ->
       jt Gamma t2 T1 -> jt Gamma t.[t2/] U
H : jt (T .: T0 .: Gamma0) t U
t2 : term
H1 : jt Gamma0 t2 T0
Unable to unify "jt ?M5092 t.[?M5093/] U" with
 "jt (T .: Gamma0) t.[ids 0 .: lift 1 t2 .: ren (+1)]
    U".
t: term
T, U: ty
Gamma0: var -> ty
T0: ty
IHjt: forall (Gamma : var -> ty) 
  (t2 : term) (T1 : ty),
T .: T0 .: Gamma0 = T1 .: Gamma ->
jt Gamma t2 T1 -> jt Gamma t.[t2/] U
H: jt (T .: T0 .: Gamma0) t U
t2: term
H1: jt Gamma0 t2 T0
jt (T .: Gamma0) t.[ids 0 .: lift 1 t2 .: ren (+1)] U
    (* The moral of the story is that it is preferable to state a lemma
       that allows applying an arbitrary substitution (of terms for
       term variables) to a term. This will give rise to statements
       that are more general, therefore both more powerful and easier
       to read. See STLCLemmas. *)
Abort.

The subject reduction theorem, also known as type preservation: the typing judgement is preserved by one step of reduction.

This is proved here for cbv, but could be proved for other notions of reduction, such as cbn, or strong reduction.

Lemma jt_preservation:
  forall Gamma t T,
  jt Gamma t T ->
  forall t',
  cbv t t' ->
  jt Gamma t' T.
forall (Gamma : tyenv) (t : term) (T : ty),
jt Gamma t T ->
forall t' : term, cbv t t' -> jt Gamma t' T
Proof.
forall (Gamma : tyenv) (t : term) (T : ty),
jt Gamma t T ->
forall t' : term, cbv t t' -> jt Gamma t' T
  (* By induction on the type derivation,
     then by cases on `cbv t t'`. *)
  induction 1; intros; subst; invert_cbv.
Gamma: tyenv
t2: term
T, U: ty
t: term
H: jt Gamma (Lam t) (TyFun T U)
H0: jt Gamma t2 T
IHjt1: forall t' : term,
cbv (Lam t) t' -> jt Gamma t' (TyFun T U)
IHjt2: forall t' : term, cbv t2 t' -> jt Gamma t' T
H4: cbv_mask RuleBetaV
H5: is_value t2
jt Gamma t.[t2/] U
Gamma: tyenv
t1, t2: term
T, U: ty
H: jt Gamma t1 (TyFun T U)
H0: jt Gamma t2 T
IHjt1: forall t' : term,
cbv t1 t' -> jt Gamma t' (TyFun T U)
IHjt2: forall t' : term, cbv t2 t' -> jt Gamma t' T
t3: term
H4: cbv_mask RuleAppL
H6: cbv t1 t3
jt Gamma (App t3 t2) U
Gamma: tyenv
t1, t2: term
T, U: ty
H: jt Gamma t1 (TyFun T U)
H0: jt Gamma t2 T
IHjt1: forall t' : term,
cbv t1 t' -> jt Gamma t' (TyFun T U)
IHjt2: forall t' : term, cbv t2 t' -> jt Gamma t' T
u2: term
H4: cbv_mask RuleAppVR
H5: is_value t1
H7: cbv t2 u2
jt Gamma (App t1 u2) U
  (* Case: JApp/RedBetaV. *)
  {
Gamma: tyenv
t2: term
T, U: ty
t: term
H: jt Gamma (Lam t) (TyFun T U)
H0: jt Gamma t2 T
IHjt1: forall t' : term,
cbv (Lam t) t' -> jt Gamma t' (TyFun T U)
IHjt2: forall t' : term, cbv t2 t' -> jt Gamma t' T
H4: cbv_mask RuleBetaV
H5: is_value t2
jt Gamma t.[t2/] U pick_jt (Lam t) invert.
Gamma: tyenv
t2: term
T, U: ty
t: term
H0: jt Gamma t2 T
IHjt1: forall t' : term,
cbv (Lam t) t' -> jt Gamma t' (TyFun T U)
IHjt2: forall t' : term, cbv t2 t' -> jt Gamma t' T
H4: cbv_mask RuleBetaV
H5: is_value t2
H6: jt (T .: Gamma) t U
jt Gamma t.[t2/] U
    eauto using jt_te_substitution_0. }
Gamma: tyenv
t1, t2: term
T, U: ty
H: jt Gamma t1 (TyFun T U)
H0: jt Gamma t2 T
IHjt1: forall t' : term,
cbv t1 t' -> jt Gamma t' (TyFun T U)
IHjt2: forall t' : term, cbv t2 t' -> jt Gamma t' T
t3: term
H4: cbv_mask RuleAppL
H6: cbv t1 t3
jt Gamma (App t3 t2) U
Gamma: tyenv
t1, t2: term
T, U: ty
H: jt Gamma t1 (TyFun T U)
H0: jt Gamma t2 T
IHjt1: forall t' : term,
cbv t1 t' -> jt Gamma t' (TyFun T U)
IHjt2: forall t' : term, cbv t2 t' -> jt Gamma t' T
u2: term
H4: cbv_mask RuleAppVR
H5: is_value t1
H7: cbv t2 u2
jt Gamma (App t1 u2) U
  (* Case: JApp/RedAppL. *)
  {
Gamma: tyenv
t1, t2: term
T, U: ty
H: jt Gamma t1 (TyFun T U)
H0: jt Gamma t2 T
IHjt1: forall t' : term,
cbv t1 t' -> jt Gamma t' (TyFun T U)
IHjt2: forall t' : term, cbv t2 t' -> jt Gamma t' T
t3: term
H4: cbv_mask RuleAppL
H6: cbv t1 t3
jt Gamma (App t3 t2) U eauto with jt. }
Gamma: tyenv
t1, t2: term
T, U: ty
H: jt Gamma t1 (TyFun T U)
H0: jt Gamma t2 T
IHjt1: forall t' : term,
cbv t1 t' -> jt Gamma t' (TyFun T U)
IHjt2: forall t' : term, cbv t2 t' -> jt Gamma t' T
u2: term
H4: cbv_mask RuleAppVR
H5: is_value t1
H7: cbv t2 u2
jt Gamma (App t1 u2) U
  (* Case: JApp/RedAppVR. *)
  {
Gamma: tyenv
t1, t2: term
T, U: ty
H: jt Gamma t1 (TyFun T U)
H0: jt Gamma t2 T
IHjt1: forall t' : term,
cbv t1 t' -> jt Gamma t' (TyFun T U)
IHjt2: forall t' : term, cbv t2 t' -> jt Gamma t' T
u2: term
H4: cbv_mask RuleAppVR
H5: is_value t1
H7: cbv t2 u2
jt Gamma (App t1 u2) U eauto with jt. }
Qed.

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

Lemma invert_jt_TyFun:
  forall Gamma t T1 T2,
  jt Gamma t (TyFun T1 T2) ->
  closed t ->
  is_value t ->
  exists t', t = Lam t'.
forall (Gamma : tyenv) (t : term) (T1 T2 : ty),
jt 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),
jt Gamma t (TyFun T1 T2) ->
closed t ->
is_value t -> exists t' : {bind term}, t = Lam t'
  (* By cases. The type system is so simple that an induction is not
     even required here. An induction would be required if the type
     system had non-syntax-directed rules, such as a subtyping rule, or
     type abstraction and type instantiation rules, as in System F. *)
  inversion 1; intros; subst.
Gamma: tyenv
T1, T2: ty
x: var
H: jt Gamma (Var x) (TyFun T1 T2)
H0: Gamma x = TyFun T1 T2
H4: closed (Var x)
H5: is_value (Var x)
exists t' : {bind term}, Var x = Lam t'
Gamma: tyenv
T1, T2: ty
t0: term
H: jt Gamma (Lam t0) (TyFun T1 T2)
H3: jt (T1 .: Gamma) t0 T2
H5: closed (Lam t0)
H6: is_value (Lam t0)
exists t' : {bind term}, Lam t0 = Lam t'
Gamma: tyenv
T1, T2: ty
t1, t2: term
H: jt Gamma (App t1 t2) (TyFun T1 T2)
T: ty
H0: jt Gamma t1 (TyFun T (TyFun T1 T2))
H1: jt Gamma t2 T
H5: closed (App t1 t2)
H6: is_value (App t1 t2)
exists t' : {bind term}, App t1 t2 = Lam t'
  (* Case: JVar. A variable is not closed. Contradiction. *)
  {
Gamma: tyenv
T1, T2: ty
x: var
H: jt Gamma (Var x) (TyFun T1 T2)
H0: Gamma x = TyFun T1 T2
H4: closed (Var x)
H5: is_value (Var x)
exists t' : {bind term}, Var x = Lam t' false.
Gamma: tyenv
T1, T2: ty
x: var
H: jt Gamma (Var x) (TyFun T1 T2)
H0: Gamma x = TyFun T1 T2
H4: closed (Var x)
H5: is_value (Var x)
False eauto with closed. }
Gamma: tyenv
T1, T2: ty
t0: term
H: jt Gamma (Lam t0) (TyFun T1 T2)
H3: jt (T1 .: Gamma) t0 T2
H5: closed (Lam t0)
H6: is_value (Lam t0)
exists t' : {bind term}, Lam t0 = Lam t'
Gamma: tyenv
T1, T2: ty
t1, t2: term
H: jt Gamma (App t1 t2) (TyFun T1 T2)
T: ty
H0: jt Gamma t1 (TyFun T (TyFun T1 T2))
H1: jt Gamma t2 T
H5: closed (App t1 t2)
H6: is_value (App t1 t2)
exists t' : {bind term}, App t1 t2 = Lam t'
  (* Case: JLam. Immediate. *)
  {
Gamma: tyenv
T1, T2: ty
t0: term
H: jt Gamma (Lam t0) (TyFun T1 T2)
H3: jt (T1 .: Gamma) t0 T2
H5: closed (Lam t0)
H6: is_value (Lam t0)
exists t' : {bind term}, Lam t0 = Lam t' obvious. }
Gamma: tyenv
T1, T2: ty
t1, t2: term
H: jt Gamma (App t1 t2) (TyFun T1 T2)
T: ty
H0: jt Gamma t1 (TyFun T (TyFun T1 T2))
H1: jt Gamma t2 T
H5: closed (App t1 t2)
H6: is_value (App t1 t2)
exists t' : {bind term}, App t1 t2 = Lam t'
  (* Case: JApp. An application is not a value. Contradiction. *)
  {
Gamma: tyenv
T1, T2: ty
t1, t2: term
H: jt Gamma (App t1 t2) (TyFun T1 T2)
T: ty
H0: jt Gamma t1 (TyFun T (TyFun T1 T2))
H1: jt Gamma t2 T
H5: closed (App t1 t2)
H6: is_value (App t1 t2)
exists t' : {bind term}, App t1 t2 = Lam t' false.
Gamma: tyenv
T1, T2: ty
t1, t2: term
H: jt Gamma (App t1 t2) (TyFun T1 T2)
T: ty
H0: jt Gamma t1 (TyFun T (TyFun T1 T2))
H1: jt Gamma t2 T
H5: closed (App t1 t2)
H6: is_value (App t1 t2)
False obvious. }
Qed.

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

Lemma jt_progress:
  forall Gamma t T,
  jt Gamma t T ->
  closed t ->
  (exists t', cbv t t') \/ is_value t.
forall (Gamma : tyenv) (t : term) (T : ty),
jt 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),
jt Gamma t T ->
closed t -> (exists t' : term, cbv t t') \/ is_value t
Proof.
forall (Gamma : tyenv) (t : term) (T : ty),
jt 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: jt (T .: Gamma) t U
IHjt: 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: jt Gamma t1 (TyFun T U)
H0: jt Gamma t2 T
IHjt1: closed t1 ->
(exists t' : term, cbv t1 t') \/ is_value t1
IHjt2: 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)
  (* Case: JVar. *)
  {
Gamma: var -> ty
x: var
H0: closed (Var x)
(exists t' : term, cbv (Var x) t') \/ is_value (Var x) (* A variable does not reduce, so we must find a contradiction among
       our hypotheses. Here, the hypothesis that `t` is closed provides
       such a contradiction. (We could also exploit the fact that,
       according to our definition of `is_value`, a variable is a value,
       but it is preferable not to do so if we can avoid it.) *)
    false.
Gamma: var -> ty
x: var
H0: closed (Var x)
False eauto with closed. }
Gamma: var -> ty
t: term
T, U: ty
H: jt (T .: Gamma) t U
IHjt: 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: jt Gamma t1 (TyFun T U)
H0: jt Gamma t2 T
IHjt1: closed t1 ->
(exists t' : term, cbv t1 t') \/ is_value t1
IHjt2: 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)
  (* Case: JLam. *)
  { (* A lambda-abstraction is a value. *)
Gamma: var -> ty
t: term
T, U: ty
H: jt (T .: Gamma) t U
IHjt: 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: jt Gamma t1 (TyFun T U)
H0: jt Gamma t2 T
IHjt1: closed t1 ->
(exists t' : term, cbv t1 t') \/ is_value t1
IHjt2: 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)
  (* Case: JApp. *)
  {
Gamma: tyenv
t1, t2: term
T, U: ty
H: jt Gamma t1 (TyFun T U)
H0: jt Gamma t2 T
IHjt1: closed t1 ->
(exists t' : term, cbv t1 t') \/ is_value t1
IHjt2: 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) (* Apply the induction hypothesis to `t1`. If `t1` reduces, then
       obviously `App t1 t2` reduces as well, so we are finished. There
       remains to consider the case where `t1` is a value. *)
    use_ih IHjt1.
Gamma: tyenv
t1, t2: term
T, U: ty
H: jt Gamma t1 (TyFun T U)
H0: jt Gamma t2 T
IHjt2: 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)
    (* Reason in the same way about `t2`. *)
    use_ih IHjt2.
Gamma: tyenv
t1, t2: term
T, U: ty
H: jt Gamma t1 (TyFun T U)
H0: jt 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)
    (* We wish to prove that `App t1 t2` is a beta-redex. *)
    left.
Gamma: tyenv
t1, t2: term
T, U: ty
H: jt Gamma t1 (TyFun T U)
H0: jt 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_jt_TyFun.
Gamma: tyenv
t1, t2: term
T, U: ty
H: jt Gamma t1 (TyFun T U)
H0: jt 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: jt Gamma (Lam x) (TyFun T U)
H0: jt 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: jt Gamma t1 (TyFun T U)
H0: jt 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: jt Gamma (Lam x) (TyFun T U)
H0: jt 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. }
Qed.