Require Import MyTactics. Require Import Sequences. Require Import LambdaCalculusSyntax. Require Import LambdaCalculusValues. Require Import LambdaCalculusReduction. Require Import SystemFDefinition. Require Import SystemFLemmas.
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.
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. *)forall (Gamma : tyenv) (t : term) (T : ty), jf Gamma t T -> forall t' : term, cbv t t' -> jf Gamma t' T(* JFApp *)Gamma:tyenvt1, t2:termT, U:tyH:jf Gamma t1 (TyFun T U)H0:jf Gamma t2 TIHjf1:forall t' : term, cbv t1 t' -> jf Gamma t' (TyFun T U)IHjf2:forall t' : term, cbv t2 t' -> jf Gamma t' Tt':termH1:cbv (App t1 t2) t'jf Gamma t' UGamma:var -> tyt:termT:tyH:jf (Gamma >> ren (+1)) t TIHjf:forall t' : term, cbv t t' -> jf (Gamma >> ren (+1)) t' Tt':termH1:cbv t t'jf Gamma t' (TyAll T)Gamma:tyenvt:termT, U:{bind ty}H:jf Gamma t (TyAll T)IHjf:forall t' : term, cbv t t' -> jf Gamma t' (TyAll T)t':termH1:cbv t t'jf Gamma t' T.[U/]Gamma:tyenvt1, t2:termT, U:tyH:jf Gamma t1 (TyFun T U)H0:jf Gamma t2 TIHjf1:forall t' : term, cbv t1 t' -> jf Gamma t' (TyFun T U)IHjf2:forall t' : term, cbv t2 t' -> jf Gamma t' Tt':termH1:cbv (App t1 t2) t'jf Gamma t' U(* RedBetaV. A beta-redex, `App (Lam t) v`, reduces to `t.[v/]`. *)Gamma:tyenvt2:termT, U:tyt:termH:jf Gamma (Lam t) (TyFun T U)H0:jf Gamma t2 TIHjf1:forall t' : term, cbv (Lam t) t' -> jf Gamma t' (TyFun T U)IHjf2:forall t' : term, cbv t2 t' -> jf Gamma t' TH4:cbv_mask RuleBetaVH5:is_value t2jf Gamma t.[t2/] UGamma:tyenvt1, t2:termT, U:tyH:jf Gamma t1 (TyFun T U)H0:jf Gamma t2 TIHjf1:forall t' : term, cbv t1 t' -> jf Gamma t' (TyFun T U)IHjf2:forall t' : term, cbv t2 t' -> jf Gamma t' Tt3:termH4:cbv_mask RuleAppLH6:cbv t1 t3jf Gamma (App t3 t2) UGamma:tyenvt1, t2:termT, U:tyH:jf Gamma t1 (TyFun T U)H0:jf Gamma t2 TIHjf1:forall t' : term, cbv t1 t' -> jf Gamma t' (TyFun T U)IHjf2:forall t' : term, cbv t2 t' -> jf Gamma t' Tu2:termH4:cbv_mask RuleAppVRH5:is_value t1H7:cbv t2 u2jf Gamma (App t1 u2) UGamma:tyenvt2:termT, U:tyt:termH:jf Gamma (Lam t) (TyFun T U)H0:jf Gamma t2 TIHjf1:forall t' : term, cbv (Lam t) t' -> jf Gamma t' (TyFun T U)IHjf2:forall t' : term, cbv t2 t' -> jf Gamma t' TH4:cbv_mask RuleBetaVH5:is_value t2jf Gamma t.[t2/] 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.Gamma:tyenvt2:termT, U:tyt:termH:jf Gamma (Lam t) (TyFun T U)H0:jf Gamma t2 TIHjf1:forall t' : term, cbv (Lam t) t' -> jf Gamma t' (TyFun T U)IHjf2:forall t' : term, cbv t2 t' -> jf Gamma t' TH4:cbv_mask RuleBetaVH5:is_value t2jf (T .: Gamma) t U
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:
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 Uforall (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(* Case: JFLam. *)Gamma:var -> tyt:termT, U:tyH:jf (T .: Gamma) t UIHjf:forall (t0 : {bind term}) (T0 U0 : ty), t = Lam t0 -> U = TyFun T0 U0 -> jf (T0 .: T .: Gamma) t0 U0t0:{bind term}T0, U0:tyH0:Lam t = Lam t0H1:TyFun T U = TyFun T0 U0jf (T0 .: Gamma) t0 U0Gamma:tyenvT, 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 UH:jf Gamma (Lam t0) (TyAll T)T0, U0:tyH2:T.[U/] = TyFun T0 U0jf (T0 .: Gamma) t0 U0congruence.Gamma:var -> tyt:termT, U:tyH:jf (T .: Gamma) t UIHjf:forall (t0 : {bind term}) (T0 U0 : ty), t = Lam t0 -> U = TyFun T0 U0 -> jf (T0 .: T .: Gamma) t0 U0t0:{bind term}T0, U0:tyH0:Lam t = Lam t0H1:TyFun T U = TyFun T0 U0jf (T0 .: Gamma) t0 U0(* Case: JFTyApp. *)Gamma:tyenvT, 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 UH:jf Gamma (Lam t0) (TyAll T)T0, U0:tyH2:T.[U/] = TyFun T0 U0jf (T0 .: Gamma) t0 U0(* The induction hypothesis has the unsatisfiable requirement `TyAll _ = TyFun _ _`. *)Gamma:tyenvT, 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 UH:jf Gamma (Lam t0) (TyAll T)T0, U0:tyH2:T.[U/] = TyFun T0 U0jf (T0 .: Gamma) t0 U0(* We are stuck. *) Abort.Gamma:tyenvT, U:{bind ty}t0:{bind term}H:jf Gamma (Lam t0) (TyAll T)T0, U0:tyH2:T.[U/] = TyFun T0 U0jf (T0 .: Gamma) t0 U0
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.
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 Uforall (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(* This time, we have three subgoals instead of two. *)Gamma:var -> tyt:termT, U:tyH:jf (T .: Gamma) t UIHjf:forall (t0 : {bind term}) (T0 U0 : ty), t = Lam t0 -> star sub U (TyFun T0 U0) -> jf (T0 .: T .: Gamma) t0 U0t0:{bind term}T0, U0:tyH0:Lam t = Lam t0H1:star sub (TyFun T U) (TyFun T0 U0)jf (T0 .: Gamma) t0 U0Gamma:var -> tyT:tyt0:{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 UH:jf (Gamma >> ren (+1)) (Lam t0) TT0, U:tyH2:star sub (TyAll T) (TyFun T0 U)jf (T0 .: Gamma) t0 UGamma:tyenvT, 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 UH:jf Gamma (Lam t0) (TyAll T)T0, U0:tyH2:star sub T.[U/] (TyFun T0 U0)jf (T0 .: Gamma) t0 U0(* Case: JFLam. *)Gamma:var -> tyt:termT, U:tyH:jf (T .: Gamma) t UIHjf:forall (t0 : {bind term}) (T0 U0 : ty), t = Lam t0 -> star sub U (TyFun T0 U0) -> jf (T0 .: T .: Gamma) t0 U0t0:{bind term}T0, U0:tyH0:Lam t = Lam t0H1:star sub (TyFun T U) (TyFun T0 U0)jf (T0 .: Gamma) t0 U0Gamma:tyenvT, 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 UH:jf Gamma (Lam t0) (TyAll T)T0, U0:tyH2:star sub T.[U/] (TyFun T0 U0)jf (T0 .: Gamma) t0 U0Gamma:var -> tyT:tyt0:{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 UH:jf (Gamma >> ren (+1)) (Lam t0) TT0, U:tyH2:star sub (TyAll T) (TyFun T0 U)jf (T0 .: Gamma) t0 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.) *)Gamma:var -> tyt:termT, U:tyH:jf (T .: Gamma) t UIHjf:forall (t0 : {bind term}) (T0 U0 : ty), t = Lam t0 -> star sub U (TyFun T0 U0) -> jf (T0 .: T .: Gamma) t0 U0t0:{bind term}T0, U0:tyH0:Lam t = Lam t0H1:star sub (TyFun T U) (TyFun T0 U0)jf (T0 .: Gamma) t0 U0(* The result is then immediate. *) congruence.Gamma:var -> tyt:termT0, U0:tyH:jf (T0 .: Gamma) t U0IHjf:forall (t0 : {bind term}) (T U : ty), t = Lam t0 -> star sub U0 (TyFun T U) -> jf (T .: T0 .: Gamma) t0 Ut0:{bind term}H0:Lam t = Lam t0jf (T0 .: Gamma) t0 U0(* Case: JFTyApp. *)Gamma:tyenvT, 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 UH:jf Gamma (Lam t0) (TyAll T)T0, U0:tyH2:star sub T.[U/] (TyFun T0 U0)jf (T0 .: Gamma) t0 U0Gamma:var -> tyT:tyt0:{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 UH:jf (Gamma >> ren (+1)) (Lam t0) TT0, U:tyH2:star sub (TyAll T) (TyFun T0 U)jf (T0 .: Gamma) t0 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. *)Gamma:tyenvT, 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 UH:jf Gamma (Lam t0) (TyAll T)T0, U0:tyH2:star sub T.[U/] (TyFun T0 U0)jf (T0 .: Gamma) t0 U0Gamma:tyenvT, 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 UH:jf Gamma (Lam t0) (TyAll T)T0, U0:tyH2:star sub T.[U/] (TyFun T0 U0)Lam t0 = Lam t0Gamma:tyenvT, 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 UH:jf Gamma (Lam t0) (TyAll T)T0, U0:tyH2:star sub T.[U/] (TyFun T0 U0)star sub (TyAll T) (TyFun T0 U0)eauto.Gamma:tyenvT, 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 UH:jf Gamma (Lam t0) (TyAll T)T0, U0:tyH2:star sub T.[U/] (TyFun T0 U0)Lam t0 = Lam t0Gamma:tyenvT, 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 UH:jf Gamma (Lam t0) (TyAll T)T0, U0:tyH2:star sub T.[U/] (TyFun T0 U0)star sub (TyAll T) (TyFun T0 U0)eauto using sub with sequences. }Gamma:tyenvT, 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 UH:jf Gamma (Lam t0) (TyAll T)T0, U0:tyH2:star sub T.[U/] (TyFun T0 U0)star sub (TyAll T) (TyFun T0 U0)(* Case: JTyAbs. *)Gamma:var -> tyT:tyt0:{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 UH:jf (Gamma >> ren (+1)) (Lam t0) TT0, U:tyH2: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. *)Gamma:var -> tyT:tyt0:{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 UH:jf (Gamma >> ren (+1)) (Lam t0) TT0, U:tyH2:star sub (TyAll T) (TyFun T0 U)jf (T0 .: Gamma) t0 UGamma:var -> tyT:tyt0:{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 UH:jf (Gamma >> ren (+1)) (Lam t0) TT0, U, b:tyH0:sub (TyAll T) bH1:star sub b (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: *)Gamma:var -> tyT:tyt0:{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 UH:jf (Gamma >> ren (+1)) (Lam t0) TT0, U:tyU0:{bind ty}H1:star sub T.[U0/] (TyFun T0 U)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.Gamma:var -> tyT:tyt0:{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 UH:jf (Gamma >> ren (+1)) (Lam t0) TT0, U:tyU0:{bind ty}H1:star sub T.[U0/] (TyFun T0 U)H0:jf Gamma (Lam t0) T.[?Goal/]jf (T0 .: Gamma) t0 U
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.
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. *)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(* Case: `n` is 0. The type derivation must end with `JTNLam`. *)Gamma:tyenvt:{bind term}T, U, T0, U0:tyH:jtn 0 Gamma (Lam t) (TyFun T0 U0)n:natH1:jtn n (T0 .: Gamma) t U0H3:star sub (TyFun T0 U0) (TyFun T U)jt (T .: Gamma) t Un:natIHn: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 UGamma:tyenvt:{bind term}T, U, T0:tyH:jtn (S n) Gamma (Lam t) (TyAll T0)H1:jtn n (Gamma >> ren (+1)) (Lam t) T0H6:star sub (TyAll T0) (TyFun T U)jt (T .: Gamma) t Un:natIHn: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 UGamma:tyenvt:{bind term}T, U:tyT0, 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(* 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.) *)Gamma:tyenvt:{bind term}T, U, T0, U0:tyH:jtn 0 Gamma (Lam t) (TyFun T0 U0)n:natH1:jtn n (T0 .: Gamma) t U0H3:star sub (TyFun T0 U0) (TyFun T U)jt (T .: Gamma) t U(* The result is then immediate. *) eauto with jt.Gamma:tyenvt:{bind term}T, U:tyH:jtn 0 Gamma (Lam t) (TyFun T U)n:natH1:jtn n (T .: Gamma) t Ujt (T .: Gamma) t U(* Case: `n` is `S m`. The type derivation ends with `JTNTyAbs`. *)n:natIHn: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 UGamma:tyenvt:{bind term}T, U, T0:tyH:jtn (S n) Gamma (Lam t) (TyAll T0)H1:jtn n (Gamma >> ren (+1)) (Lam t) T0H6:star sub (TyAll T0) (TyFun T U)jt (T .: Gamma) t Un:natIHn: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 UGamma:tyenvt:{bind term}T, U:tyT0, 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(* 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. *)n:natIHn: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 UGamma:tyenvt:{bind term}T, U, T0:tyH:jtn (S n) Gamma (Lam t) (TyAll T0)H1:jtn n (Gamma >> ren (+1)) (Lam t) T0H6:star sub (TyAll T0) (TyFun T U)jt (T .: Gamma) t Un:natIHn: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 UGamma:tyenvt:{bind term}T, U, T0:tyH:jtn (S n) Gamma (Lam t) (TyAll T0)H1:jtn n (Gamma >> ren (+1)) (Lam t) T0b:tyH0:sub (TyAll T0) bH2:star sub b (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: *)n:natIHn: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 UGamma:tyenvt:{bind term}T, U, T0:tyH:jtn (S n) Gamma (Lam t) (TyAll T0)H1:jtn n (Gamma >> ren (+1)) (Lam t) T0U0:{bind ty}H2:star sub T0.[U0/] (TyFun T U)jt (T .: Gamma) t U(* 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:natIHn: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 UGamma:tyenvt:{bind term}T, U, T0:tyH:jtn (S n) Gamma (Lam t) (TyAll T0)H1:jtn n (Gamma >> ren (+1)) (Lam t) T0U0:{bind ty}H2:star sub T0.[U0/] (TyFun T U)jtn n Gamma (Lam t) T0.[U0/](* Case: `n` is `S m`. The type derivation ends with `JTNApp`. *)n:natIHn: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 UGamma:tyenvt:{bind term}T, U:tyT0, 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.n:natIHn: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 UGamma:tyenvt:{bind term}T, U:tyT0, 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
The inversion lemma can be reformulated in terms of jf
.
forall (Gamma : tyenv) (t : {bind term}) (T U : ty), jf Gamma (Lam t) (TyFun T U) -> jf (T .: Gamma) t Uforall (Gamma : tyenv) (t : {bind term}) (T U : ty), jf Gamma (Lam t) (TyFun T U) -> jf (T .: Gamma) t UGamma:tyenvt:{bind term}T, U:tyH:jf Gamma (Lam t) (TyFun T U)jf (T .: Gamma) t UGamma:tyenvt:{bind term}T, U:tyH:jf Gamma (Lam t) (TyFun T U)H0:jt Gamma (Lam t) (TyFun T U)jf (T .: Gamma) t UGamma:tyenvt:{bind term}T, U:tyH:jf Gamma (Lam t) (TyFun T U)H0:exists n : nat, jtn n Gamma (Lam t) (TyFun T U)jf (T .: Gamma) t UGamma:tyenvt:{bind term}T, U:tyH:jf Gamma (Lam t) (TyFun T U)x:natH0:jtn x Gamma (Lam t) (TyFun T U)jf (T .: Gamma) t UGamma:tyenvt:{bind term}T, U:tyH:jf Gamma (Lam t) (TyFun T U)x:natH0:jtn x Gamma (Lam t) (TyFun T U)fact:=jt (?Goal .: Gamma) t ?Goal0:Propstar sub (TyFun T U) (TyFun ?Goal ?Goal0)Gamma:tyenvt:{bind term}T, U:tyH:jf Gamma (Lam t) (TyFun T U)x:natH0:jtn x Gamma (Lam t) (TyFun T U)H1:jt (?Goal .: Gamma) t ?Goal0jf (T .: Gamma) t Ueauto with sequences.Gamma:tyenvt:{bind term}T, U:tyH:jf Gamma (Lam t) (TyFun T U)x:natH0:jtn x Gamma (Lam t) (TyFun T U)fact:=jt (?Goal .: Gamma) t ?Goal0:Propstar sub (TyFun T U) (TyFun ?Goal ?Goal0)eauto using jt_jf. Qed.Gamma:tyenvt:{bind term}T, U:tyH:jf Gamma (Lam t) (TyFun T U)x:natH0:jtn x Gamma (Lam t) (TyFun T U)H1:jt (T .: Gamma) t Ujf (T .: Gamma) t U
The typing judgement is preserved by one step of reduction.
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. *)forall (Gamma : tyenv) (t : term) (T : ty), jf Gamma t T -> forall t' : term, cbv t t' -> jf Gamma t' T(* JFApp *)Gamma:tyenvt1, t2:termT, U:tyH:jf Gamma t1 (TyFun T U)H0:jf Gamma t2 TIHjf1:forall t' : term, cbv t1 t' -> jf Gamma t' (TyFun T U)IHjf2:forall t' : term, cbv t2 t' -> jf Gamma t' Tt':termH1:cbv (App t1 t2) t'jf Gamma t' UGamma:var -> tyt:termT:tyH:jf (Gamma >> ren (+1)) t TIHjf:forall t' : term, cbv t t' -> jf (Gamma >> ren (+1)) t' Tt':termH1:cbv t t'jf Gamma t' (TyAll T)Gamma:tyenvt:termT, U:{bind ty}H:jf Gamma t (TyAll T)IHjf:forall t' : term, cbv t t' -> jf Gamma t' (TyAll T)t':termH1:cbv t t'jf Gamma t' T.[U/]Gamma:tyenvt1, t2:termT, U:tyH:jf Gamma t1 (TyFun T U)H0:jf Gamma t2 TIHjf1:forall t' : term, cbv t1 t' -> jf Gamma t' (TyFun T U)IHjf2:forall t' : term, cbv t2 t' -> jf Gamma t' Tt':termH1:cbv (App t1 t2) t'jf Gamma t' U(* RedBetaV. A beta-redex, `App (Lam t) v`, reduces to `t.[v/]`. *)Gamma:tyenvt2:termT, U:tyt:termH:jf Gamma (Lam t) (TyFun T U)H0:jf Gamma t2 TIHjf1:forall t' : term, cbv (Lam t) t' -> jf Gamma t' (TyFun T U)IHjf2:forall t' : term, cbv t2 t' -> jf Gamma t' TH4:cbv_mask RuleBetaVH5:is_value t2jf Gamma t.[t2/] UGamma:tyenvt1, t2:termT, U:tyH:jf Gamma t1 (TyFun T U)H0:jf Gamma t2 TIHjf1:forall t' : term, cbv t1 t' -> jf Gamma t' (TyFun T U)IHjf2:forall t' : term, cbv t2 t' -> jf Gamma t' Tt3:termH4:cbv_mask RuleAppLH6:cbv t1 t3jf Gamma (App t3 t2) UGamma:tyenvt1, t2:termT, U:tyH:jf Gamma t1 (TyFun T U)H0:jf Gamma t2 TIHjf1:forall t' : term, cbv t1 t' -> jf Gamma t' (TyFun T U)IHjf2:forall t' : term, cbv t2 t' -> jf Gamma t' Tu2:termH4:cbv_mask RuleAppVRH5:is_value t1H7:cbv t2 u2jf Gamma (App t1 u2) UGamma:tyenvt2:termT, U:tyt:termH:jf Gamma (Lam t) (TyFun T U)H0:jf Gamma t2 TIHjf1:forall t' : term, cbv (Lam t) t' -> jf Gamma t' (TyFun T U)IHjf2:forall t' : term, cbv t2 t' -> jf Gamma t' TH4:cbv_mask RuleBetaVH5:is_value t2jf Gamma t.[t2/] 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:tyenvt2:termT, U:tyt:termH:jf Gamma (Lam t) (TyFun T U)H0:jf Gamma t2 TIHjf1:forall t' : term, cbv (Lam t) t' -> jf Gamma t' (TyFun T U)IHjf2:forall t' : term, cbv t2 t' -> jf Gamma t' TH4:cbv_mask RuleBetaVH5:is_value t2jf (T .: Gamma) t U(* RedAppL. *)Gamma:tyenvt1, t2:termT, U:tyH:jf Gamma t1 (TyFun T U)H0:jf Gamma t2 TIHjf1:forall t' : term, cbv t1 t' -> jf Gamma t' (TyFun T U)IHjf2:forall t' : term, cbv t2 t' -> jf Gamma t' Tt3:termH4:cbv_mask RuleAppLH6:cbv t1 t3jf Gamma (App t3 t2) UGamma:tyenvt1, t2:termT, U:tyH:jf Gamma t1 (TyFun T U)H0:jf Gamma t2 TIHjf1:forall t' : term, cbv t1 t' -> jf Gamma t' (TyFun T U)IHjf2:forall t' : term, cbv t2 t' -> jf Gamma t' Tu2:termH4:cbv_mask RuleAppVRH5:is_value t1H7:cbv t2 u2jf Gamma (App t1 u2) Ueauto with jf.Gamma:tyenvt1, t2:termT, U:tyH:jf Gamma t1 (TyFun T U)H0:jf Gamma t2 TIHjf1:forall t' : term, cbv t1 t' -> jf Gamma t' (TyFun T U)IHjf2:forall t' : term, cbv t2 t' -> jf Gamma t' Tt3:termH4:cbv_mask RuleAppLH6:cbv t1 t3jf Gamma (App t3 t2) U(* RedAppVR. *)Gamma:tyenvt1, t2:termT, U:tyH:jf Gamma t1 (TyFun T U)H0:jf Gamma t2 TIHjf1:forall t' : term, cbv t1 t' -> jf Gamma t' (TyFun T U)IHjf2:forall t' : term, cbv t2 t' -> jf Gamma t' Tu2:termH4:cbv_mask RuleAppVRH5:is_value t1H7:cbv t2 u2jf Gamma (App t1 u2) Ueauto with jf. }Gamma:tyenvt1, t2:termT, U:tyH:jf Gamma t1 (TyFun T U)H0:jf Gamma t2 TIHjf1:forall t' : term, cbv t1 t' -> jf Gamma t' (TyFun T U)IHjf2:forall t' : term, cbv t2 t' -> jf Gamma t' Tu2:termH4:cbv_mask RuleAppVRH5:is_value t1H7:cbv t2 u2jf Gamma (App t1 u2) U(* JTNTyAbs *)Gamma:var -> tyt:termT:tyH:jf (Gamma >> ren (+1)) t TIHjf:forall t' : term, cbv t t' -> jf (Gamma >> ren (+1)) t' Tt':termH1:cbv t t'jf Gamma t' (TyAll T)Gamma:tyenvt:termT, U:{bind ty}H:jf Gamma t (TyAll T)IHjf:forall t' : term, cbv t t' -> jf Gamma t' (TyAll T)t':termH1:cbv t t'jf Gamma t' T.[U/]eauto with jf.Gamma:var -> tyt:termT:tyH:jf (Gamma >> ren (+1)) t TIHjf:forall t' : term, cbv t t' -> jf (Gamma >> ren (+1)) t' Tt':termH1:cbv t t'jf Gamma t' (TyAll T)(* JTNTyApp *)Gamma:tyenvt:termT, U:{bind ty}H:jf Gamma t (TyAll T)IHjf:forall t' : term, cbv t t' -> jf Gamma t' (TyAll T)t':termH1:cbv t t'jf Gamma t' T.[U/]eauto with jf. } Qed.Gamma:tyenvt:termT, U:{bind ty}H:jf Gamma t (TyAll T)IHjf:forall t' : term, cbv t t' -> jf Gamma t' (TyAll T)t':termH1:cbv t t'jf Gamma t' T.[U/]
An inversion lemma: if a closed value admits a function type TyFun T1 T2
,
then it must be a lambda-abstraction.
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`. *)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'(* Case: JTNLam. *)Gamma:tyenvt0:termT0, U:tyH:jtn 0 Gamma (Lam t0) (TyFun T0 U)n:natH0:jtn n (T0 .: Gamma) t0 UT1, T2:tyH1: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:natIHn: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:tyenvt:termT0:tyH:jtn (S n) Gamma t (TyAll T0)H1:jtn n (Gamma >> ren (+1)) t T0T1, T2:tyH6:star sub (TyAll T0) (TyFun T1 T2)H7:closed tH8:is_value texists t' : {bind term}, t = Lam t'n:natIHn: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:tyenvt:termT0, U:{bind ty}H:jtn (S n) Gamma t T0.[U/]H1:jtn n Gamma t (TyAll T0)T1, T2:tyH6:star sub T0.[U/] (TyFun T1 T2)H7:closed tH8:is_value texists t' : {bind term}, t = Lam t'eauto.Gamma:tyenvt0:termT0, U:tyH:jtn 0 Gamma (Lam t0) (TyFun T0 U)n:natH0:jtn n (T0 .: Gamma) t0 UT1, T2:tyH1: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'(* Case: JTNTyAbs. *)n:natIHn: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:tyenvt:termT0:tyH:jtn (S n) Gamma t (TyAll T0)H1:jtn n (Gamma >> ren (+1)) t T0T1, T2:tyH6:star sub (TyAll T0) (TyFun T1 T2)H7:closed tH8:is_value texists t' : {bind term}, t = Lam t'n:natIHn: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:tyenvt:termT0, U:{bind ty}H:jtn (S n) Gamma t T0.[U/]H1:jtn n Gamma t (TyAll T0)T1, T2:tyH6:star sub T0.[U/] (TyFun T1 T2)H7:closed tH8:is_value texists t' : {bind term}, t = Lam t'n:natIHn: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:tyenvt:termT0:tyH:jtn (S n) Gamma t (TyAll T0)H1:jtn n (Gamma >> ren (+1)) t T0T1, T2:tyH6:star sub (TyAll T0) (TyFun T1 T2)H7:closed tH8:is_value texists t' : {bind term}, t = Lam t'n:natIHn: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:tyenvt:termT0:tyH:jtn (S n) Gamma t (TyAll T0)H1:jtn n (Gamma >> ren (+1)) t T0T1, T2:tyH7:closed tH8:is_value tb:tyH0:sub (TyAll T0) bH2:star sub b (TyFun T1 T2)exists t' : {bind term}, t = Lam t'n:natIHn: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:tyenvt:termT0:tyH:jtn (S n) Gamma t (TyAll T0)H1:jtn n (Gamma >> ren (+1)) t T0T1, T2:tyH7:closed tH8:is_value tU:{bind ty}H2:star sub T0.[U/] (TyFun T1 T2)exists t' : {bind term}, t = Lam t'eauto using jtn_ty_substitution_0.n:natIHn: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:tyenvt:termT0:tyH:jtn (S n) Gamma t (TyAll T0)H1:jtn n (Gamma >> ren (+1)) t T0T1, T2:tyH7:closed tH8:is_value tU:{bind ty}H2:star sub T0.[U/] (TyFun T1 T2)jtn n ?Gamma t T0.[U/](* Case: JTNTyApp. *)n:natIHn: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:tyenvt:termT0, U:{bind ty}H:jtn (S n) Gamma t T0.[U/]H1:jtn n Gamma t (TyAll T0)T1, T2:tyH6:star sub T0.[U/] (TyFun T1 T2)H7:closed tH8:is_value texists t' : {bind term}, t = Lam t'eauto using sub with sequences. } Qed.n:natIHn: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:tyenvt:termT0, U:{bind ty}H:jtn (S n) Gamma t T0.[U/]H1:jtn n Gamma t (TyAll T0)T1, T2:tyH6:star sub T0.[U/] (TyFun T1 T2)H7:closed tH8:is_value texists t' : {bind term}, 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'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'Gamma:tyenvt:termT1, T2:tyH:jf Gamma t (TyFun T1 T2)H0:closed tH1:is_value texists t' : {bind term}, t = Lam t'Gamma:tyenvt:termT1, T2:tyH:jf Gamma t (TyFun T1 T2)H0:closed tH1:is_value tH2:jt Gamma t (TyFun T1 T2)exists t' : {bind term}, t = Lam t'Gamma:tyenvt:termT1, T2:tyH:jf Gamma t (TyFun T1 T2)H0:closed tH1:is_value tH2:exists n : nat, jtn n Gamma t (TyFun T1 T2)exists t' : {bind term}, t = Lam t'Gamma:tyenvt:termT1, T2:tyH:jf Gamma t (TyFun T1 T2)H0:closed tH1:is_value tx:natH2:jtn x Gamma t (TyFun T1 T2)exists t' : {bind term}, t = Lam t'Gamma:tyenvt:termT1, T2:tyH:jf Gamma t (TyFun T1 T2)H0:closed tH1:is_value tx:natH2:jtn x Gamma t (TyFun T1 T2)fact:=exists t' : {bind term}, t = Lam t':Propstar sub (TyFun T1 T2) (TyFun ?T1 ?T2)Gamma:tyenvT1, T2:tyx0:{bind term}H1:is_value (Lam x0)H0:closed (Lam x0)H:jf Gamma (Lam x0) (TyFun T1 T2)x:natH2:jtn x Gamma (Lam x0) (TyFun T1 T2)exists t' : {bind term}, Lam x0 = Lam t'eauto with sequences.Gamma:tyenvt:termT1, T2:tyH:jf Gamma t (TyFun T1 T2)H0:closed tH1:is_value tx:natH2:jtn x Gamma t (TyFun T1 T2)fact:=exists t' : {bind term}, t = Lam t':Propstar sub (TyFun T1 T2) (TyFun ?T1 ?T2)eauto using jt_jf. Qed.Gamma:tyenvT1, T2:tyx0:{bind term}H1:is_value (Lam x0)H0:closed (Lam x0)H:jf Gamma (Lam x0) (TyFun T1 T2)x:natH2:jtn x Gamma (Lam x0) (TyFun T1 T2)exists t' : {bind term}, Lam x0 = Lam t'
The progress theorem: a closed, well-typed term must either be able to make one step of reduction or be a value.
forall (Gamma : tyenv) (t : term) (T : ty), jf Gamma t T -> closed t -> (exists t' : term, cbv t t') \/ is_value tforall (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. *)forall (Gamma : tyenv) (t : term) (T : ty), jf Gamma t T -> closed t -> (exists t' : term, cbv t t') \/ is_value t(* Case: JFVar. *)Gamma:var -> tyx:varH0:closed (Var x)(exists t' : term, cbv (Var x) t') \/ is_value (Var x)Gamma:var -> tyt:termT, U:tyH:jf (T .: Gamma) t UIHjf:closed t -> (exists t' : term, cbv t t') \/ is_value tH0:closed (Lam t)(exists t' : term, cbv (Lam t) t') \/ is_value (Lam t)Gamma:tyenvt1, t2:termT, U:tyH:jf Gamma t1 (TyFun T U)H0:jf Gamma t2 TIHjf1:closed t1 -> (exists t' : term, cbv t1 t') \/ is_value t1IHjf2:closed t2 -> (exists t' : term, cbv t2 t') \/ is_value t2H1:closed (App t1 t2)(exists t' : term, cbv (App t1 t2) t') \/ is_value (App t1 t2)Gamma:var -> tyt:termT:tyH:jf (Gamma >> ren (+1)) t TIHjf:closed t -> (exists t' : term, cbv t t') \/ is_value tH1:closed t(exists t' : term, cbv t t') \/ is_value tGamma:tyenvt:termT, U:{bind ty}H:jf Gamma t (TyAll T)IHjf:closed t -> (exists t' : term, cbv t t') \/ is_value tH1:closed t(exists t' : term, cbv t t') \/ is_value tGamma:var -> tyx:varH0:closed (Var x)(exists t' : term, cbv (Var x) t') \/ is_value (Var x)eauto with closed.Gamma:var -> tyx:varH0:closed (Var x)False(* Case: JFLam. *)Gamma:var -> tyt:termT, U:tyH:jf (T .: Gamma) t UIHjf:closed t -> (exists t' : term, cbv t t') \/ is_value tH0:closed (Lam t)(exists t' : term, cbv (Lam t) t') \/ is_value (Lam t)Gamma:tyenvt1, t2:termT, U:tyH:jf Gamma t1 (TyFun T U)H0:jf Gamma t2 TIHjf1:closed t1 -> (exists t' : term, cbv t1 t') \/ is_value t1IHjf2:closed t2 -> (exists t' : term, cbv t2 t') \/ is_value t2H1:closed (App t1 t2)(exists t' : term, cbv (App t1 t2) t') \/ is_value (App t1 t2)Gamma:var -> tyt:termT:tyH:jf (Gamma >> ren (+1)) t TIHjf:closed t -> (exists t' : term, cbv t t') \/ is_value tH1:closed t(exists t' : term, cbv t t') \/ is_value tGamma:tyenvt:termT, U:{bind ty}H:jf Gamma t (TyAll T)IHjf:closed t -> (exists t' : term, cbv t t') \/ is_value tH1:closed t(exists t' : term, cbv t t') \/ is_value tobvious.Gamma:var -> tyt:termT, U:tyH:jf (T .: Gamma) t UIHjf:closed t -> (exists t' : term, cbv t t') \/ is_value tH0:closed (Lam t)(exists t' : term, cbv (Lam t) t') \/ is_value (Lam t)(* Case: JFApp. *)Gamma:tyenvt1, t2:termT, U:tyH:jf Gamma t1 (TyFun T U)H0:jf Gamma t2 TIHjf1:closed t1 -> (exists t' : term, cbv t1 t') \/ is_value t1IHjf2:closed t2 -> (exists t' : term, cbv t2 t') \/ is_value t2H1:closed (App t1 t2)(exists t' : term, cbv (App t1 t2) t') \/ is_value (App t1 t2)Gamma:var -> tyt:termT:tyH:jf (Gamma >> ren (+1)) t TIHjf:closed t -> (exists t' : term, cbv t t') \/ is_value tH1:closed t(exists t' : term, cbv t t') \/ is_value tGamma:tyenvt:termT, U:{bind ty}H:jf Gamma t (TyAll T)IHjf:closed t -> (exists t' : term, cbv t t') \/ is_value tH1:closed t(exists t' : term, cbv t t') \/ is_value tGamma:tyenvt1, t2:termT, U:tyH:jf Gamma t1 (TyFun T U)H0:jf Gamma t2 TIHjf1:closed t1 -> (exists t' : term, cbv t1 t') \/ is_value t1IHjf2:closed t2 -> (exists t' : term, cbv t2 t') \/ is_value t2H1:closed (App t1 t2)(exists t' : term, cbv (App t1 t2) t') \/ is_value (App t1 t2)Gamma:tyenvt1, t2:termT, U:tyH:jf Gamma t1 (TyFun T U)H0:jf Gamma t2 TIHjf2:closed t2 -> (exists t' : term, cbv t2 t') \/ is_value t2H1:closed (App t1 t2)H2:is_value t1(exists t' : term, cbv (App t1 t2) t') \/ is_value (App t1 t2)Gamma:tyenvt1, t2:termT, U:tyH:jf Gamma t1 (TyFun T U)H0:jf Gamma t2 TH1:closed (App t1 t2)H2:is_value t1H3:is_value t2(exists t' : term, cbv (App t1 t2) t') \/ is_value (App t1 t2)(* Because `t1` is a closed value and has a function type, it must be a lambda-abstraction. *)Gamma:tyenvt1, t2:termT, U:tyH:jf Gamma t1 (TyFun T U)H0:jf Gamma t2 TH1:closed (App t1 t2)H2:is_value t1H3:is_value t2exists t' : term, cbv (App t1 t2) t'Gamma:tyenvt1, t2:termT, U:tyH:jf Gamma t1 (TyFun T U)H0:jf Gamma t2 TH1:closed (App t1 t2)H2:is_value t1H3:is_value t2fact:=exists t' : {bind term}, t1 = Lam t':Propclosed t1Gamma:tyenvt2:termT, U:tyx:{bind term}H:jf Gamma (Lam x) (TyFun T U)H0:jf Gamma t2 TH2:is_value (Lam x)H1:closed (App (Lam x) t2)H3:is_value t2exists t' : term, cbv (App (Lam x) t2) t'eauto with closed.Gamma:tyenvt1, t2:termT, U:tyH:jf Gamma t1 (TyFun T U)H0:jf Gamma t2 TH1:closed (App t1 t2)H2:is_value t1H3:is_value t2fact:=exists t' : {bind term}, t1 = Lam t':Propclosed t1(* Therefore, we have a beta-redex. *) obvious.Gamma:tyenvt2:termT, U:tyx:{bind term}H:jf Gamma (Lam x) (TyFun T U)H0:jf Gamma t2 TH2:is_value (Lam x)H1:closed (App (Lam x) t2)H3:is_value t2exists t' : term, cbv (App (Lam x) t2) t'(* Case: JFTyAbs. *)Gamma:var -> tyt:termT:tyH:jf (Gamma >> ren (+1)) t TIHjf:closed t -> (exists t' : term, cbv t t') \/ is_value tH1:closed t(exists t' : term, cbv t t') \/ is_value tGamma:tyenvt:termT, U:{bind ty}H:jf Gamma t (TyAll T)IHjf:closed t -> (exists t' : term, cbv t t') \/ is_value tH1:closed t(exists t' : term, cbv t t') \/ is_value teauto.Gamma:var -> tyt:termT:tyH:jf (Gamma >> ren (+1)) t TIHjf:closed t -> (exists t' : term, cbv t t') \/ is_value tH1:closed t(exists t' : term, cbv t t') \/ is_value t(* Case: JFTyApp. *)Gamma:tyenvt:termT, U:{bind ty}H:jf Gamma t (TyAll T)IHjf:closed t -> (exists t' : term, cbv t t') \/ is_value tH1:closed t(exists t' : term, cbv t t') \/ is_value teauto. } Qed.Gamma:tyenvt:termT, U:{bind ty}H:jf Gamma t (TyAll T)IHjf:closed t -> (exists t' : term, cbv t t') \/ is_value tH1:closed t(exists t' : term, cbv t t') \/ is_value t