Require Import MyTactics. Require Import Sequences. Require Import LambdaCalculusSyntax. Require Import LambdaCalculusValues. Require Import LambdaCalculusReduction. Require Import SystemFDefinition.
This typing judgement is indexed with an integer n
which counts the
number of outstanding type abstractions and type applications, that
is, the number of type abstractions and type applications that are not
buried under a syntax-directed typing rule.
This integer index is used in the proof of the type substitution lemma
jtn_ty_substitution
, where we prove that n
is preserved, and in
the proof of the inversion lemma invert_jtn_Lam_TyFun
, which is
carried out by induction over n
.
Inductive jtn : nat -> tyenv -> term -> ty -> Prop :=
| JTNVar:
forall Gamma x T,
Gamma x = T ->
jtn 0 Gamma (Var x) T
| JTNLam:
forall n Gamma t T U,
jtn n (T .: Gamma) t U ->
jtn 0 Gamma (Lam t) (TyFun T U)
| JTNApp:
forall n1 n2 Gamma t1 t2 T U,
jtn n1 Gamma t1 (TyFun T U) ->
jtn n2 Gamma t2 T ->
jtn 0 Gamma (App t1 t2) U
| JTNTyAbs:
forall n Gamma Gamma' t T,
jtn n Gamma' t T ->
Gamma' = Gamma >> ren (+1) ->
jtn (S n) Gamma t (TyAll T)
| JTNTyApp:
forall n Gamma t T U T',
jtn n Gamma t (TyAll T) ->
T' = T.[U/] ->
jtn (S n) Gamma t T'
.
The following hint allows eauto with jtn
to apply the above typing rules.
It is convenient to define a simpler typing judgement which is not indexed
with an integer n
. We use this judgement when we do not care about n
.
Definition jt Gamma t T :=
exists n,
jtn n Gamma t T.
The following hint allows eauto with jt
to exploit the fact that
j n Gamma t T
implies jt Gamma t T
.
It is convenient to reformulate the typing rules at the level of jt
.
This is somewhat redundant, but nothing complicated is going on here.
forall (Gamma : var -> ty) (x : var) (T : ty), Gamma x = T -> jt Gamma (Var x) Tforall (Gamma : var -> ty) (x : var) (T : ty), Gamma x = T -> jt Gamma (Var x) Tforall (Gamma : var -> ty) (x : var) (T : ty), Gamma x = T -> exists n : nat, jtn n Gamma (Var x) TGamma:var -> tyx:varT:tyH:Gamma x = Texists n : nat, jtn n Gamma (Var x) Teauto using jtn. Qed.Gamma:var -> tyx:varexists n : nat, jtn n Gamma (Var x) (Gamma x)forall (Gamma : var -> ty) (t : term) (T U : ty), jt (T .: Gamma) t U -> jt Gamma (Lam t) (TyFun T U)forall (Gamma : var -> ty) (t : term) (T U : ty), jt (T .: Gamma) t U -> jt Gamma (Lam t) (TyFun T U)forall (Gamma : var -> ty) (t : term) (T U : ty), (exists n : nat, jtn n (T .: Gamma) t U) -> exists n : nat, jtn n Gamma (Lam t) (TyFun T U)Gamma:var -> tyt:termT, U:tyH:exists n : nat, jtn n (T .: Gamma) t Uexists n : nat, jtn n Gamma (Lam t) (TyFun T U)eauto using jtn. Qed.Gamma:var -> tyt:termT, U:tyx:natH:jtn x (T .: Gamma) t Uexists n : nat, jtn n Gamma (Lam t) (TyFun T U)forall (Gamma : tyenv) (t1 t2 : term) (T U : ty), jt Gamma t1 (TyFun T U) -> jt Gamma t2 T -> jt Gamma (App t1 t2) Uforall (Gamma : tyenv) (t1 t2 : term) (T U : ty), jt Gamma t1 (TyFun T U) -> jt Gamma t2 T -> jt Gamma (App t1 t2) Uforall (Gamma : tyenv) (t1 t2 : term) (T U : ty), (exists n : nat, jtn n Gamma t1 (TyFun T U)) -> (exists n : nat, jtn n Gamma t2 T) -> exists n : nat, jtn n Gamma (App t1 t2) UGamma:tyenvt1, t2:termT, U:tyH:exists n : nat, jtn n Gamma t1 (TyFun T U)H0:exists n : nat, jtn n Gamma t2 Texists n : nat, jtn n Gamma (App t1 t2) Ueauto using jtn. Qed.Gamma:tyenvt1, t2:termT, U:tyx0:natH:jtn x0 Gamma t1 (TyFun T U)x:natH0:jtn x Gamma t2 Texists n : nat, jtn n Gamma (App t1 t2) Uforall (Gamma : var -> ty) (Gamma' : tyenv) (t : term) (T : ty), jt Gamma' t T -> Gamma' = Gamma >> ren (+1) -> jt Gamma t (TyAll T)forall (Gamma : var -> ty) (Gamma' : tyenv) (t : term) (T : ty), jt Gamma' t T -> Gamma' = Gamma >> ren (+1) -> jt Gamma t (TyAll T)forall (Gamma : var -> ty) (Gamma' : tyenv) (t : term) (T : ty), (exists n : nat, jtn n Gamma' t T) -> Gamma' = Gamma >> ren (+1) -> exists n : nat, jtn n Gamma t (TyAll T)Gamma:var -> tyGamma':tyenvt:termT:tyH:exists n : nat, jtn n Gamma' t TH0:Gamma' = Gamma >> ren (+1)exists n : nat, jtn n Gamma t (TyAll T)eauto using jtn. Qed.Gamma:var -> tyt:termT:tyx:natH:jtn x (Gamma >> ren (+1)) t Texists n : nat, jtn n Gamma t (TyAll T)forall (Gamma : tyenv) (t : term) (T U T' : {bind ty}), jt Gamma t (TyAll T) -> T' = T.[U/] -> jt Gamma t T'forall (Gamma : tyenv) (t : term) (T U T' : {bind ty}), jt Gamma t (TyAll T) -> T' = T.[U/] -> jt Gamma t T'forall (Gamma : tyenv) (t : term) (T U T' : {bind ty}), (exists n : nat, jtn n Gamma t (TyAll T)) -> T' = T.[U/] -> exists n : nat, jtn n Gamma t T'Gamma:tyenvt:termT, U, T':{bind ty}H:exists n : nat, jtn n Gamma t (TyAll T)H0:T' = T.[U/]exists n : nat, jtn n Gamma t T'eauto using jtn. Qed.Gamma:tyenvt:termT, U:{bind ty}x:natH:jtn x Gamma t (TyAll T)exists n : nat, jtn n Gamma t T.[U/]
The following hint allows eauto with jt
to use the above lemmas.
The judgements jt
and jf
are equivalent. So, we have just given an
alternate definition of System F.
forall (n : nat) (Gamma : tyenv) (t : term) (T : ty), jtn n Gamma t T -> jf Gamma t Tinduction 1; intros; subst; eauto with jf. Qed.forall (n : nat) (Gamma : tyenv) (t : term) (T : ty), jtn n Gamma t T -> jf Gamma t Tforall (Gamma : tyenv) (t : term) (T : ty), jt Gamma t T -> jf Gamma t Tforall (Gamma : tyenv) (t : term) (T : ty), jt Gamma t T -> jf Gamma t Tforall (Gamma : tyenv) (t : term) (T : ty), (exists n : nat, jtn n Gamma t T) -> jf Gamma t TGamma:tyenvt:termT:tyH:exists n : nat, jtn n Gamma t Tjf Gamma t Teauto using jtn_jf. Qed.Gamma:tyenvt:termT:tyx:natH:jtn x Gamma t Tjf Gamma t Tforall (Gamma : tyenv) (t : term) (T : ty), jf Gamma t T -> jt Gamma t Tinduction 1; intros; subst; eauto with jt. Qed.forall (Gamma : tyenv) (t : term) (T : ty), jf Gamma t T -> jt Gamma t T
The typing judgement jtn
is preserved by a type substitution theta
,
which maps type variables to types.
We prove that the measure n
is preserved by such a substitution.
This is required in the proof of invert_jtn_Lam_TyFun
, where we
apply a substitution to the type derivation before exploiting the
induction hypothesis.
forall (n : nat) (Gamma : tyenv) (t : term) (T : ty), jtn n Gamma t T -> forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = T.[theta] -> jtn n Gamma' t T'(* A detailed proof, where every case is dealt with explicitly: *)forall (n : nat) (Gamma : tyenv) (t : term) (T : ty), jtn n Gamma t T -> forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = T.[theta] -> jtn n Gamma' t T'(* JTNVar *)Gamma:var -> tyx:vartheta:var -> tyjtn 0 (Gamma >> theta) (Var x) (Gamma x).[theta]n:natGamma:var -> tyt:termT, U:tyH:jtn n (T .: Gamma) t UIHjtn:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = T .: Gamma >> theta -> T' = U.[theta] -> jtn n Gamma' t T'theta:var -> tyjtn 0 (Gamma >> theta) (Lam t) (TyFun T U).[theta]n1, n2:natGamma:tyenvt1, t2:termT, U:tyH:jtn n1 Gamma t1 (TyFun T U)H0:jtn n2 Gamma t2 TIHjtn1:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = (TyFun T U).[theta] -> jtn n1 Gamma' t1 T'IHjtn2:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = T.[theta] -> jtn n2 Gamma' t2 T'theta:var -> tyjtn 0 (Gamma >> theta) (App t1 t2) U.[theta]n:natGamma:var -> tyt:termT:tyH:jtn n (Gamma >> ren (+1)) t TIHjtn:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> ren (+1) >> theta -> T' = T.[theta] -> jtn n Gamma' t T'theta:var -> tyjtn (S n) (Gamma >> theta) t (TyAll T).[theta]n:natGamma:tyenvt:termT, U:{bind ty}H:jtn n Gamma t (TyAll T)IHjtn:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = (TyAll T).[theta] -> jtn n Gamma' t T'theta:var -> tyjtn (S n) (Gamma >> theta) t T.[U/].[theta]Gamma:var -> tyx:vartheta:var -> tyjtn 0 (Gamma >> theta) (Var x) (Gamma x).[theta]autosubst.Gamma:var -> tyx:vartheta:var -> ty(Gamma >> theta) x = (Gamma x).[theta](* JTNLam *)n:natGamma:var -> tyt:termT, U:tyH:jtn n (T .: Gamma) t UIHjtn:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = T .: Gamma >> theta -> T' = U.[theta] -> jtn n Gamma' t T'theta:var -> tyjtn 0 (Gamma >> theta) (Lam t) (TyFun T U).[theta]n1, n2:natGamma:tyenvt1, t2:termT, U:tyH:jtn n1 Gamma t1 (TyFun T U)H0:jtn n2 Gamma t2 TIHjtn1:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = (TyFun T U).[theta] -> jtn n1 Gamma' t1 T'IHjtn2:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = T.[theta] -> jtn n2 Gamma' t2 T'theta:var -> tyjtn 0 (Gamma >> theta) (App t1 t2) U.[theta]n:natGamma:var -> tyt:termT:tyH:jtn n (Gamma >> ren (+1)) t TIHjtn:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> ren (+1) >> theta -> T' = T.[theta] -> jtn n Gamma' t T'theta:var -> tyjtn (S n) (Gamma >> theta) t (TyAll T).[theta]n:natGamma:tyenvt:termT, U:{bind ty}H:jtn n Gamma t (TyAll T)IHjtn:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = (TyAll T).[theta] -> jtn n Gamma' t T'theta:var -> tyjtn (S n) (Gamma >> theta) t T.[U/].[theta]n:natGamma:var -> tyt:termT, U:tyH:jtn n (T .: Gamma) t UIHjtn:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = T .: Gamma >> theta -> T' = U.[theta] -> jtn n Gamma' t T'theta:var -> tyjtn 0 (Gamma >> theta) (Lam t) (TyFun T U).[theta]n:natGamma:var -> tyt:termT, U:tyH:jtn n (T .: Gamma) t UIHjtn:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = T .: Gamma >> theta -> T' = U.[theta] -> jtn n Gamma' t T'theta:var -> tyjtn ?n (T.[theta] .: Gamma >> theta) t U.[theta]n:natGamma:var -> tyt:termT, U:tyH:jtn n (T .: Gamma) t UIHjtn:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = T .: Gamma >> theta -> T' = U.[theta] -> jtn n Gamma' t T'theta:var -> tyT.[theta] .: Gamma >> theta = T .: Gamma >> ?thetan:natGamma:var -> tyt:termT, U:tyH:jtn n (T .: Gamma) t UIHjtn:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = T .: Gamma >> theta -> T' = U.[theta] -> jtn n Gamma' t T'theta:var -> tyU.[theta] = U.[?theta]eauto.n:natGamma:var -> tyt:termT, U:tyH:jtn n (T .: Gamma) t UIHjtn:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = T .: Gamma >> theta -> T' = U.[theta] -> jtn n Gamma' t T'theta:var -> tyU.[theta] = U.[theta](* JTNApp *)n1, n2:natGamma:tyenvt1, t2:termT, U:tyH:jtn n1 Gamma t1 (TyFun T U)H0:jtn n2 Gamma t2 TIHjtn1:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = (TyFun T U).[theta] -> jtn n1 Gamma' t1 T'IHjtn2:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = T.[theta] -> jtn n2 Gamma' t2 T'theta:var -> tyjtn 0 (Gamma >> theta) (App t1 t2) U.[theta]n:natGamma:var -> tyt:termT:tyH:jtn n (Gamma >> ren (+1)) t TIHjtn:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> ren (+1) >> theta -> T' = T.[theta] -> jtn n Gamma' t T'theta:var -> tyjtn (S n) (Gamma >> theta) t (TyAll T).[theta]n:natGamma:tyenvt:termT, U:{bind ty}H:jtn n Gamma t (TyAll T)IHjtn:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = (TyAll T).[theta] -> jtn n Gamma' t T'theta:var -> tyjtn (S n) (Gamma >> theta) t T.[U/].[theta]n1, n2:natGamma:tyenvt1, t2:termT, U:tyH:jtn n1 Gamma t1 (TyFun T U)H0:jtn n2 Gamma t2 TIHjtn1:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = (TyFun T U).[theta] -> jtn n1 Gamma' t1 T'IHjtn2:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = T.[theta] -> jtn n2 Gamma' t2 T'theta:var -> tyjtn 0 (Gamma >> theta) (App t1 t2) U.[theta]n1, n2:natGamma:tyenvt1, t2:termT, U:tyH:jtn n1 Gamma t1 (TyFun T U)H0:jtn n2 Gamma t2 TIHjtn1:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = (TyFun T U).[theta] -> jtn n1 Gamma' t1 T'IHjtn2:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = T.[theta] -> jtn n2 Gamma' t2 T'theta:var -> tyjtn ?n1 (Gamma >> theta) t1 (TyFun ?T U.[theta])n1, n2:natGamma:tyenvt1, t2:termT, U:tyH:jtn n1 Gamma t1 (TyFun T U)H0:jtn n2 Gamma t2 TIHjtn1:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = (TyFun T U).[theta] -> jtn n1 Gamma' t1 T'IHjtn2:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = T.[theta] -> jtn n2 Gamma' t2 T'theta:var -> tyjtn ?n2 (Gamma >> theta) t2 ?Tn1, n2:natGamma:tyenvt1, t2:termT, U:tyH:jtn n1 Gamma t1 (TyFun T U)H0:jtn n2 Gamma t2 TIHjtn1:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = (TyFun T U).[theta] -> jtn n1 Gamma' t1 T'IHjtn2:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = T.[theta] -> jtn n2 Gamma' t2 T'theta:var -> tyGamma >> theta = Gamma >> ?thetan1, n2:natGamma:tyenvt1, t2:termT, U:tyH:jtn n1 Gamma t1 (TyFun T U)H0:jtn n2 Gamma t2 TIHjtn1:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = (TyFun T U).[theta] -> jtn n1 Gamma' t1 T'IHjtn2:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = T.[theta] -> jtn n2 Gamma' t2 T'theta:var -> tyTyFun ?T U.[theta] = (TyFun T U).[?theta]n1, n2:natGamma:tyenvt1, t2:termT, U:tyH:jtn n1 Gamma t1 (TyFun T U)H0:jtn n2 Gamma t2 TIHjtn1:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = (TyFun T U).[theta] -> jtn n1 Gamma' t1 T'IHjtn2:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = T.[theta] -> jtn n2 Gamma' t2 T'theta:var -> tyjtn ?n2 (Gamma >> theta) t2 ?Tn1, n2:natGamma:tyenvt1, t2:termT, U:tyH:jtn n1 Gamma t1 (TyFun T U)H0:jtn n2 Gamma t2 TIHjtn1:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = (TyFun T U).[theta] -> jtn n1 Gamma' t1 T'IHjtn2:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = T.[theta] -> jtn n2 Gamma' t2 T'theta:var -> tyTyFun ?T U.[theta] = (TyFun T U).[theta]n1, n2:natGamma:tyenvt1, t2:termT, U:tyH:jtn n1 Gamma t1 (TyFun T U)H0:jtn n2 Gamma t2 TIHjtn1:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = (TyFun T U).[theta] -> jtn n1 Gamma' t1 T'IHjtn2:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = T.[theta] -> jtn n2 Gamma' t2 T'theta:var -> tyjtn ?n2 (Gamma >> theta) t2 ?Tn1, n2:natGamma:tyenvt1, t2:termT, U:tyH:jtn n1 Gamma t1 (TyFun T U)H0:jtn n2 Gamma t2 TIHjtn1:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = (TyFun T U).[theta] -> jtn n1 Gamma' t1 T'IHjtn2:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = T.[theta] -> jtn n2 Gamma' t2 T'theta:var -> tyTyFun ?T U.[theta] = TyFun T.[theta] U.[theta]n1, n2:natGamma:tyenvt1, t2:termT, U:tyH:jtn n1 Gamma t1 (TyFun T U)H0:jtn n2 Gamma t2 TIHjtn1:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = (TyFun T U).[theta] -> jtn n1 Gamma' t1 T'IHjtn2:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = T.[theta] -> jtn n2 Gamma' t2 T'theta:var -> tyjtn ?n2 (Gamma >> theta) t2 ?Teauto.n1, n2:natGamma:tyenvt1, t2:termT, U:tyH:jtn n1 Gamma t1 (TyFun T U)H0:jtn n2 Gamma t2 TIHjtn1:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = (TyFun T U).[theta] -> jtn n1 Gamma' t1 T'IHjtn2:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = T.[theta] -> jtn n2 Gamma' t2 T'theta:var -> tyjtn ?n2 (Gamma >> theta) t2 T.[theta](* JTNTyAbs *)n:natGamma:var -> tyt:termT:tyH:jtn n (Gamma >> ren (+1)) t TIHjtn:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> ren (+1) >> theta -> T' = T.[theta] -> jtn n Gamma' t T'theta:var -> tyjtn (S n) (Gamma >> theta) t (TyAll T).[theta]n:natGamma:tyenvt:termT, U:{bind ty}H:jtn n Gamma t (TyAll T)IHjtn:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = (TyAll T).[theta] -> jtn n Gamma' t T'theta:var -> tyjtn (S n) (Gamma >> theta) t T.[U/].[theta]n:natGamma:var -> tyt:termT:tyH:jtn n (Gamma >> ren (+1)) t TIHjtn:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> ren (+1) >> theta -> T' = T.[theta] -> jtn n Gamma' t T'theta:var -> tyjtn (S n) (Gamma >> theta) t (TyAll T).[theta]n:natGamma:var -> tyt:termT:tyH:jtn n (Gamma >> ren (+1)) t TIHjtn:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> ren (+1) >> theta -> T' = T.[theta] -> jtn n Gamma' t T'theta:var -> tyjtn n ?Gamma' t T.[up theta]n:natGamma:var -> tyt:termT:tyH:jtn n (Gamma >> ren (+1)) t TIHjtn:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> ren (+1) >> theta -> T' = T.[theta] -> jtn n Gamma' t T'theta:var -> ty?Gamma' = Gamma >> theta >> ren (+1)n:natGamma:var -> tyt:termT:tyH:jtn n (Gamma >> ren (+1)) t TIHjtn:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> ren (+1) >> theta -> T' = T.[theta] -> jtn n Gamma' t T'theta:var -> ty?Gamma' = Gamma >> ren (+1) >> ?thetan:natGamma:var -> tyt:termT:tyH:jtn n (Gamma >> ren (+1)) t TIHjtn:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> ren (+1) >> theta -> T' = T.[theta] -> jtn n Gamma' t T'theta:var -> tyT.[up theta] = T.[?theta]n:natGamma:var -> tyt:termT:tyH:jtn n (Gamma >> ren (+1)) t TIHjtn:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> ren (+1) >> theta -> T' = T.[theta] -> jtn n Gamma' t T'theta:var -> ty?Gamma' = Gamma >> theta >> ren (+1)n:natGamma:var -> tyt:termT:tyH:jtn n (Gamma >> ren (+1)) t TIHjtn:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> ren (+1) >> theta -> T' = T.[theta] -> jtn n Gamma' t T'theta:var -> tyT.[up theta] = T.[?theta]n:natGamma:var -> tyt:termT:tyH:jtn n (Gamma >> ren (+1)) t TIHjtn:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> ren (+1) >> theta -> T' = T.[theta] -> jtn n Gamma' t T'theta:var -> tyGamma >> ren (+1) >> ?theta = Gamma >> theta >> ren (+1)autosubst.n:natGamma:var -> tyt:termT:tyH:jtn n (Gamma >> ren (+1)) t TIHjtn:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> ren (+1) >> theta -> T' = T.[theta] -> jtn n Gamma' t T'theta:var -> tyGamma >> ren (+1) >> up theta = Gamma >> theta >> ren (+1)(* JTNTyApp *)n:natGamma:tyenvt:termT, U:{bind ty}H:jtn n Gamma t (TyAll T)IHjtn:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = (TyAll T).[theta] -> jtn n Gamma' t T'theta:var -> tyjtn (S n) (Gamma >> theta) t T.[U/].[theta]n:natGamma:tyenvt:termT, U:{bind ty}H:jtn n Gamma t (TyAll T)IHjtn:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = (TyAll T).[theta] -> jtn n Gamma' t T'theta:var -> tyjtn (S n) (Gamma >> theta) t T.[U/].[theta]n:natGamma:tyenvt:termT, U:{bind ty}H:jtn n Gamma t (TyAll T)IHjtn:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = (TyAll T).[theta] -> jtn n Gamma' t T'theta:var -> tyjtn n (Gamma >> theta) t (TyAll ?T)n:natGamma:tyenvt:termT, U:{bind ty}H:jtn n Gamma t (TyAll T)IHjtn:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = (TyAll T).[theta] -> jtn n Gamma' t T'theta:var -> tyT.[U/].[theta] = ?T.[?U/]n:natGamma:tyenvt:termT, U:{bind ty}H:jtn n Gamma t (TyAll T)IHjtn:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = (TyAll T).[theta] -> jtn n Gamma' t T'theta:var -> tyGamma >> theta = Gamma >> ?thetan:natGamma:tyenvt:termT, U:{bind ty}H:jtn n Gamma t (TyAll T)IHjtn:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = (TyAll T).[theta] -> jtn n Gamma' t T'theta:var -> tyTyAll ?T = (TyAll T).[?theta]n:natGamma:tyenvt:termT, U:{bind ty}H:jtn n Gamma t (TyAll T)IHjtn:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = (TyAll T).[theta] -> jtn n Gamma' t T'theta:var -> tyT.[U/].[theta] = ?T.[?U/]n:natGamma:tyenvt:termT, U:{bind ty}H:jtn n Gamma t (TyAll T)IHjtn:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = (TyAll T).[theta] -> jtn n Gamma' t T'theta:var -> tyTyAll ?T = (TyAll T).[theta]n:natGamma:tyenvt:termT, U:{bind ty}H:jtn n Gamma t (TyAll T)IHjtn:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = (TyAll T).[theta] -> jtn n Gamma' t T'theta:var -> tyT.[U/].[theta] = ?T.[?U/]autosubst. }n:natGamma:tyenvt:termT, U:{bind ty}H:jtn n Gamma t (TyAll T)IHjtn:forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = (TyAll T).[theta] -> jtn n Gamma' t T'theta:var -> tyT.[U/].[theta] = T.[up theta].[?U/](* A shorter script, where all cases are dealt with uniformly: *) induction 1; intros; subst; econstructor; eauto with autosubst. Qed.forall (n : nat) (Gamma : tyenv) (t : term) (T : ty), jtn n Gamma t T -> forall (Gamma' : var -> ty) (T' : ty) (theta : var -> ty), Gamma' = Gamma >> theta -> T' = T.[theta] -> jtn n Gamma' t T'
As a corollary, if the term t
has type T
under a type environment that extends Gamma
with one type variable,
then for every type U
,
the term t
has type T.[U/]
under Gamma
.
Again, the measure n
is preserved by this substitution.
forall (n : nat) (Gamma : var -> ty) (t : term) (T U : ty), jtn n (Gamma >> ren (+1)) t T -> jtn n Gamma t T.[U/]forall (n : nat) (Gamma : var -> ty) (t : term) (T U : ty), jtn n (Gamma >> ren (+1)) t T -> jtn n Gamma t T.[U/]n:natGamma:var -> tyt:termT, U:tyH:jtn n (Gamma >> ren (+1)) t Tjtn n Gamma t T.[U/]autosubst. Qed.n:natGamma:var -> tyt:termT, U:tyH:jtn n (Gamma >> ren (+1)) t TGamma = Gamma >> ren (+1) >> U .: ids
As a corollary, the same properties hold of the judgement jf
.
forall (Gamma : tyenv) (t : term) (T : ty) (theta : var -> ty), jf Gamma t T -> jf (Gamma >> theta) t T.[theta]forall (Gamma : tyenv) (t : term) (T : ty) (theta : var -> ty), jf Gamma t T -> jf (Gamma >> theta) t T.[theta]Gamma:tyenvt:termT:tytheta:var -> tyH:jf Gamma t Tjf (Gamma >> theta) t T.[theta]Gamma:tyenvt:termT:tytheta:var -> tyH:jf Gamma t TH0:jt Gamma t Tjf (Gamma >> theta) t T.[theta]Gamma:tyenvt:termT:tytheta:var -> tyH:jf Gamma t TH0:exists n : nat, jtn n Gamma t Tjf (Gamma >> theta) t T.[theta]Gamma:tyenvt:termT:tytheta:var -> tyH:jf Gamma t Tx:natH0:jtn x Gamma t Tjf (Gamma >> theta) t T.[theta]eauto using jtn_jf. Qed.Gamma:tyenvt:termT:tytheta:var -> tyH:jf Gamma t Tx:natH0:jtn x Gamma t TH1:jtn x (Gamma >> ?Goal) t T.[?Goal]jf (Gamma >> theta) t T.[theta]forall (Gamma : var -> ty) (t : term) (T U : ty), jf (Gamma >> ren (+1)) t T -> jf Gamma t T.[U/]forall (Gamma : var -> ty) (t : term) (T U : ty), jf (Gamma >> ren (+1)) t T -> jf Gamma t T.[U/]Gamma:var -> tyt:termT, U:tyH:jf (Gamma >> ren (+1)) t Tjf Gamma t T.[U/]Gamma:var -> tyt:termT, U:tyH:jf (Gamma >> ren (+1)) t TH0:jt (Gamma >> ren (+1)) t Tjf Gamma t T.[U/]Gamma:var -> tyt:termT, U:tyH:jf (Gamma >> ren (+1)) t TH0:exists n : nat, jtn n (Gamma >> ren (+1)) t Tjf Gamma t T.[U/]Gamma:var -> tyt:termT, U:tyH:jf (Gamma >> ren (+1)) t Tx:natH0:jtn x (Gamma >> ren (+1)) t Tjf Gamma t T.[U/]eauto using jtn_jf. Qed.Gamma:var -> tyt:termT, U:tyH:jf (Gamma >> ren (+1)) t Tx:natH0:jtn x (Gamma >> ren (+1)) t TH1:jtn x Gamma t T.[?Goal/]jf Gamma t T.[U/]
The typing judgement is preserved by a renaming xi
that maps
term variables to term variables. Note that xi
need not be
injective.
forall (Gamma : tyenv) (t : term) (U : ty), jf Gamma t U -> forall (Gamma' : var -> ty) (xi : var -> var), Gamma = xi >>> Gamma' -> jf Gamma' t.[ren xi] U(* A detailed proof, where every case is dealt with explicitly: *)forall (Gamma : tyenv) (t : term) (U : ty), jf Gamma t U -> forall (Gamma' : var -> ty) (xi : var -> var), Gamma = xi >>> Gamma' -> jf Gamma' t.[ren xi] U(* JFVar *)x:varGamma':var -> tyxi:var -> varjf Gamma' (Var x).[ren xi] ((xi >>> Gamma') x)t:termT, U:tyGamma':var -> tyxi:var -> varIHjf:forall (Gamma'0 : var -> ty) (xi0 : var -> var), T .: xi >>> Gamma' = xi0 >>> Gamma'0 -> jf Gamma'0 t.[ren xi0] UH:jf (T .: xi >>> Gamma') t Ujf Gamma' (Lam t).[ren xi] (TyFun T U)t1, t2:termT, U:tyGamma':var -> tyxi:var -> varIHjf2:forall (Gamma'0 : var -> ty) (xi0 : var -> var), xi >>> Gamma' = xi0 >>> Gamma'0 -> jf Gamma'0 t2.[ren xi0] TIHjf1:forall (Gamma'0 : var -> ty) (xi0 : var -> var), xi >>> Gamma' = xi0 >>> Gamma'0 -> jf Gamma'0 t1.[ren xi0] (TyFun T U)H0:jf (xi >>> Gamma') t2 TH:jf (xi >>> Gamma') t1 (TyFun T U)jf Gamma' (App t1 t2).[ren xi] Ut:termT:tyGamma'0:var -> tyxi:var -> varIHjf:forall (Gamma' : var -> ty) (xi0 : var -> var), xi >>> Gamma'0 >> ren (+1) = xi0 >>> Gamma' -> jf Gamma' t.[ren xi0] TH:jf (xi >>> Gamma'0 >> ren (+1)) t Tjf Gamma'0 t.[ren xi] (TyAll T)t:termT, U:{bind ty}Gamma':var -> tyxi:var -> varIHjf:forall (Gamma'0 : var -> ty) (xi0 : var -> var), xi >>> Gamma' = xi0 >>> Gamma'0 -> jf Gamma'0 t.[ren xi0] (TyAll T)H:jf (xi >>> Gamma') t (TyAll T)jf Gamma' t.[ren xi] T.[U/]x:varGamma':var -> tyxi:var -> varjf Gamma' (Var x).[ren xi] ((xi >>> Gamma') x)x:varGamma':var -> tyxi:var -> varjf Gamma' (ids (xi x)) (Gamma' (xi x))eauto.x:varGamma':var -> tyxi:var -> varGamma' (xi x) = Gamma' (xi x)(* JFLam *)t:termT, U:tyGamma':var -> tyxi:var -> varIHjf:forall (Gamma'0 : var -> ty) (xi0 : var -> var), T .: xi >>> Gamma' = xi0 >>> Gamma'0 -> jf Gamma'0 t.[ren xi0] UH:jf (T .: xi >>> Gamma') t Ujf Gamma' (Lam t).[ren xi] (TyFun T U)t1, t2:termT, U:tyGamma':var -> tyxi:var -> varIHjf2:forall (Gamma'0 : var -> ty) (xi0 : var -> var), xi >>> Gamma' = xi0 >>> Gamma'0 -> jf Gamma'0 t2.[ren xi0] TIHjf1:forall (Gamma'0 : var -> ty) (xi0 : var -> var), xi >>> Gamma' = xi0 >>> Gamma'0 -> jf Gamma'0 t1.[ren xi0] (TyFun T U)H0:jf (xi >>> Gamma') t2 TH:jf (xi >>> Gamma') t1 (TyFun T U)jf Gamma' (App t1 t2).[ren xi] Ut:termT:tyGamma'0:var -> tyxi:var -> varIHjf:forall (Gamma' : var -> ty) (xi0 : var -> var), xi >>> Gamma'0 >> ren (+1) = xi0 >>> Gamma' -> jf Gamma' t.[ren xi0] TH:jf (xi >>> Gamma'0 >> ren (+1)) t Tjf Gamma'0 t.[ren xi] (TyAll T)t:termT, U:{bind ty}Gamma':var -> tyxi:var -> varIHjf:forall (Gamma'0 : var -> ty) (xi0 : var -> var), xi >>> Gamma' = xi0 >>> Gamma'0 -> jf Gamma'0 t.[ren xi0] (TyAll T)H:jf (xi >>> Gamma') t (TyAll T)jf Gamma' t.[ren xi] T.[U/]t:termT, U:tyGamma':var -> tyxi:var -> varIHjf:forall (Gamma'0 : var -> ty) (xi0 : var -> var), T .: xi >>> Gamma' = xi0 >>> Gamma'0 -> jf Gamma'0 t.[ren xi0] UH:jf (T .: xi >>> Gamma') t Ujf Gamma' (Lam t).[ren xi] (TyFun T U)t:termT, U:tyGamma':var -> tyxi:var -> varIHjf:forall (Gamma'0 : var -> ty) (xi0 : var -> var), T .: xi >>> Gamma' = xi0 >>> Gamma'0 -> jf Gamma'0 t.[ren xi0] UH:jf (T .: xi >>> Gamma') t Ujf Gamma' (Lam t.[ren (upren xi)]) (TyFun T U)t:termT, U:tyGamma':var -> tyxi:var -> varIHjf:forall (Gamma'0 : var -> ty) (xi0 : var -> var), T .: xi >>> Gamma' = xi0 >>> Gamma'0 -> jf Gamma'0 t.[ren xi0] UH:jf (T .: xi >>> Gamma') t Ujf (T .: Gamma') t.[ren (upren xi)] Uautosubst.t:termT, U:tyGamma':var -> tyxi:var -> varIHjf:forall (Gamma'0 : var -> ty) (xi0 : var -> var), T .: xi >>> Gamma' = xi0 >>> Gamma'0 -> jf Gamma'0 t.[ren xi0] UH:jf (T .: xi >>> Gamma') t UT .: xi >>> Gamma' = upren xi >>> T .: Gamma'(* JFApp *)t1, t2:termT, U:tyGamma':var -> tyxi:var -> varIHjf2:forall (Gamma'0 : var -> ty) (xi0 : var -> var), xi >>> Gamma' = xi0 >>> Gamma'0 -> jf Gamma'0 t2.[ren xi0] TIHjf1:forall (Gamma'0 : var -> ty) (xi0 : var -> var), xi >>> Gamma' = xi0 >>> Gamma'0 -> jf Gamma'0 t1.[ren xi0] (TyFun T U)H0:jf (xi >>> Gamma') t2 TH:jf (xi >>> Gamma') t1 (TyFun T U)jf Gamma' (App t1 t2).[ren xi] Ut:termT:tyGamma'0:var -> tyxi:var -> varIHjf:forall (Gamma' : var -> ty) (xi0 : var -> var), xi >>> Gamma'0 >> ren (+1) = xi0 >>> Gamma' -> jf Gamma' t.[ren xi0] TH:jf (xi >>> Gamma'0 >> ren (+1)) t Tjf Gamma'0 t.[ren xi] (TyAll T)t:termT, U:{bind ty}Gamma':var -> tyxi:var -> varIHjf:forall (Gamma'0 : var -> ty) (xi0 : var -> var), xi >>> Gamma' = xi0 >>> Gamma'0 -> jf Gamma'0 t.[ren xi0] (TyAll T)H:jf (xi >>> Gamma') t (TyAll T)jf Gamma' t.[ren xi] T.[U/]t1, t2:termT, U:tyGamma':var -> tyxi:var -> varIHjf2:forall (Gamma'0 : var -> ty) (xi0 : var -> var), xi >>> Gamma' = xi0 >>> Gamma'0 -> jf Gamma'0 t2.[ren xi0] TIHjf1:forall (Gamma'0 : var -> ty) (xi0 : var -> var), xi >>> Gamma' = xi0 >>> Gamma'0 -> jf Gamma'0 t1.[ren xi0] (TyFun T U)H0:jf (xi >>> Gamma') t2 TH:jf (xi >>> Gamma') t1 (TyFun T U)jf Gamma' (App t1 t2).[ren xi] Ut1, t2:termT, U:tyGamma':var -> tyxi:var -> varIHjf2:forall (Gamma'0 : var -> ty) (xi0 : var -> var), xi >>> Gamma' = xi0 >>> Gamma'0 -> jf Gamma'0 t2.[ren xi0] TIHjf1:forall (Gamma'0 : var -> ty) (xi0 : var -> var), xi >>> Gamma' = xi0 >>> Gamma'0 -> jf Gamma'0 t1.[ren xi0] (TyFun T U)H0:jf (xi >>> Gamma') t2 TH:jf (xi >>> Gamma') t1 (TyFun T U)jf Gamma' (App t1.[ren xi] t2.[ren xi]) Ut1, t2:termT, U:tyGamma':var -> tyxi:var -> varIHjf2:forall (Gamma'0 : var -> ty) (xi0 : var -> var), xi >>> Gamma' = xi0 >>> Gamma'0 -> jf Gamma'0 t2.[ren xi0] TIHjf1:forall (Gamma'0 : var -> ty) (xi0 : var -> var), xi >>> Gamma' = xi0 >>> Gamma'0 -> jf Gamma'0 t1.[ren xi0] (TyFun T U)H0:jf (xi >>> Gamma') t2 TH:jf (xi >>> Gamma') t1 (TyFun T U)jf Gamma' t1.[ren xi] (TyFun ?T U)t1, t2:termT, U:tyGamma':var -> tyxi:var -> varIHjf2:forall (Gamma'0 : var -> ty) (xi0 : var -> var), xi >>> Gamma' = xi0 >>> Gamma'0 -> jf Gamma'0 t2.[ren xi0] TIHjf1:forall (Gamma'0 : var -> ty) (xi0 : var -> var), xi >>> Gamma' = xi0 >>> Gamma'0 -> jf Gamma'0 t1.[ren xi0] (TyFun T U)H0:jf (xi >>> Gamma') t2 TH:jf (xi >>> Gamma') t1 (TyFun T U)jf Gamma' t2.[ren xi] ?Teauto.t1, t2:termT, U:tyGamma':var -> tyxi:var -> varIHjf2:forall (Gamma'0 : var -> ty) (xi0 : var -> var), xi >>> Gamma' = xi0 >>> Gamma'0 -> jf Gamma'0 t2.[ren xi0] TIHjf1:forall (Gamma'0 : var -> ty) (xi0 : var -> var), xi >>> Gamma' = xi0 >>> Gamma'0 -> jf Gamma'0 t1.[ren xi0] (TyFun T U)H0:jf (xi >>> Gamma') t2 TH:jf (xi >>> Gamma') t1 (TyFun T U)jf Gamma' t2.[ren xi] T(* JFTyAbs *)t:termT:tyGamma'0:var -> tyxi:var -> varIHjf:forall (Gamma' : var -> ty) (xi0 : var -> var), xi >>> Gamma'0 >> ren (+1) = xi0 >>> Gamma' -> jf Gamma' t.[ren xi0] TH:jf (xi >>> Gamma'0 >> ren (+1)) t Tjf Gamma'0 t.[ren xi] (TyAll T)t:termT, U:{bind ty}Gamma':var -> tyxi:var -> varIHjf:forall (Gamma'0 : var -> ty) (xi0 : var -> var), xi >>> Gamma' = xi0 >>> Gamma'0 -> jf Gamma'0 t.[ren xi0] (TyAll T)H:jf (xi >>> Gamma') t (TyAll T)jf Gamma' t.[ren xi] T.[U/]t:termT:tyGamma'0:var -> tyxi:var -> varIHjf:forall (Gamma' : var -> ty) (xi0 : var -> var), xi >>> Gamma'0 >> ren (+1) = xi0 >>> Gamma' -> jf Gamma' t.[ren xi0] TH:jf (xi >>> Gamma'0 >> ren (+1)) t Tjf Gamma'0 t.[ren xi] (TyAll T)t:termT:tyGamma'0:var -> tyxi:var -> varIHjf:forall (Gamma' : var -> ty) (xi0 : var -> var), xi >>> Gamma'0 >> ren (+1) = xi0 >>> Gamma' -> jf Gamma' t.[ren xi0] TH:jf (xi >>> Gamma'0 >> ren (+1)) t Tjf Gamma'0 t.[ren xi] (TyAll T)t:termT:tyGamma'0:var -> tyxi:var -> varIHjf:forall (Gamma' : var -> ty) (xi0 : var -> var), xi >>> Gamma'0 >> ren (+1) = xi0 >>> Gamma' -> jf Gamma' t.[ren xi0] TH:jf (xi >>> Gamma'0 >> ren (+1)) t Tjf ?Gamma' t.[ren xi] Tt:termT:tyGamma'0:var -> tyxi:var -> varIHjf:forall (Gamma' : var -> ty) (xi0 : var -> var), xi >>> Gamma'0 >> ren (+1) = xi0 >>> Gamma' -> jf Gamma' t.[ren xi0] TH:jf (xi >>> Gamma'0 >> ren (+1)) t T?Gamma' = Gamma'0 >> ren (+1)t:termT:tyGamma'0:var -> tyxi:var -> varIHjf:forall (Gamma' : var -> ty) (xi0 : var -> var), xi >>> Gamma'0 >> ren (+1) = xi0 >>> Gamma' -> jf Gamma' t.[ren xi0] TH:jf (xi >>> Gamma'0 >> ren (+1)) t Txi >>> Gamma'0 >> ren (+1) = xi >>> ?Gamma't:termT:tyGamma'0:var -> tyxi:var -> varIHjf:forall (Gamma' : var -> ty) (xi0 : var -> var), xi >>> Gamma'0 >> ren (+1) = xi0 >>> Gamma' -> jf Gamma' t.[ren xi0] TH:jf (xi >>> Gamma'0 >> ren (+1)) t T?Gamma' = Gamma'0 >> ren (+1)autosubst.t:termT:tyGamma'0:var -> tyxi:var -> varIHjf:forall (Gamma' : var -> ty) (xi0 : var -> var), xi >>> Gamma'0 >> ren (+1) = xi0 >>> Gamma' -> jf Gamma' t.[ren xi0] TH:jf (xi >>> Gamma'0 >> ren (+1)) t TGamma'0 >>> subst ((+1) >>> ids) = Gamma'0 >> ren (+1)(* JFTyApp *)t:termT, U:{bind ty}Gamma':var -> tyxi:var -> varIHjf:forall (Gamma'0 : var -> ty) (xi0 : var -> var), xi >>> Gamma' = xi0 >>> Gamma'0 -> jf Gamma'0 t.[ren xi0] (TyAll T)H:jf (xi >>> Gamma') t (TyAll T)jf Gamma' t.[ren xi] T.[U/]t:termT, U:{bind ty}Gamma':var -> tyxi:var -> varIHjf:forall (Gamma'0 : var -> ty) (xi0 : var -> var), xi >>> Gamma' = xi0 >>> Gamma'0 -> jf Gamma'0 t.[ren xi0] (TyAll T)H:jf (xi >>> Gamma') t (TyAll T)jf Gamma' t.[ren xi] T.[U/]t:termT, U:{bind ty}Gamma':var -> tyxi:var -> varIHjf:forall (Gamma'0 : var -> ty) (xi0 : var -> var), xi >>> Gamma' = xi0 >>> Gamma'0 -> jf Gamma'0 t.[ren xi0] (TyAll T)H:jf (xi >>> Gamma') t (TyAll T)jf Gamma' t.[ren xi] T.[U/]t:termT, U:{bind ty}Gamma':var -> tyxi:var -> varIHjf:forall (Gamma'0 : var -> ty) (xi0 : var -> var), xi >>> Gamma' = xi0 >>> Gamma'0 -> jf Gamma'0 t.[ren xi0] (TyAll T)H:jf (xi >>> Gamma') t (TyAll T)jf Gamma' t.[ren xi] (TyAll ?T)t:termT, U:{bind ty}Gamma':var -> tyxi:var -> varIHjf:forall (Gamma'0 : var -> ty) (xi0 : var -> var), xi >>> Gamma' = xi0 >>> Gamma'0 -> jf Gamma'0 t.[ren xi0] (TyAll T)H:jf (xi >>> Gamma') t (TyAll T)T.[U/] = ?T.[?U/]eauto. }t:termT, U:{bind ty}Gamma':var -> tyxi:var -> varIHjf:forall (Gamma'0 : var -> ty) (xi0 : var -> var), xi >>> Gamma' = xi0 >>> Gamma'0 -> jf Gamma'0 t.[ren xi0] (TyAll T)H:jf (xi >>> Gamma') t (TyAll T)T.[U/] = T.[?U/](* A shorter script, where all cases are dealt with uniformly: *) induction 1; intros; subst; asimpl; econstructor; eauto with autosubst. Qed.forall (Gamma : tyenv) (t : term) (U : ty), jf Gamma t U -> forall (Gamma' : var -> ty) (xi : var -> var), Gamma = xi >>> Gamma' -> jf Gamma' t.[ren xi] U
As a corollary, jf
is preserved by the renaming (+1)
.
forall (Gamma : tyenv) (t : term) (T U : ty), jf Gamma t U -> jf (T .: Gamma) (lift 1 t) Uforall (Gamma : tyenv) (t : term) (T U : ty), jf Gamma t U -> jf (T .: Gamma) (lift 1 t) UGamma:tyenvt:termT, U:tyH:jf Gamma t Ujf (T .: Gamma) (lift 1 t) UGamma:tyenvt:termT, U:tyH:jf Gamma t Ujf ?Gamma t UGamma:tyenvt:termT, U:tyH:jf Gamma t U?Gamma = (+1) >>> T .: Gammaautosubst. Qed.Gamma:tyenvt:termT, U:tyH:jf Gamma t UGamma = (+1) >>> T .: Gamma
The typing judgement is extended to substitutions.
Definition js Gamma sigma Delta :=
forall x : var,
jf Gamma (sigma x) (Delta x).
The following are basic lemmas about js
.
forall Gamma : tyenv, js Gamma ids Gammaforall Gamma : tyenv, js Gamma ids Gammaeauto with jf. Qed.forall (Gamma : tyenv) (x : var), jf Gamma (ids x) (Gamma x)forall (Gamma : tyenv) (t : term) (sigma : var -> term) (T : ty) (Delta : var -> ty), jf Gamma t T -> js Gamma sigma Delta -> js Gamma (t .: sigma) (T .: Delta)forall (Gamma : tyenv) (t : term) (sigma : var -> term) (T : ty) (Delta : var -> ty), jf Gamma t T -> js Gamma sigma Delta -> js Gamma (t .: sigma) (T .: Delta)intros [|x]; asimpl; eauto. Qed.Gamma:tyenvt:termsigma:var -> termT:tyDelta:var -> tyH:jf Gamma t TH0:js Gamma sigma Deltajs Gamma (t .: sigma) (T .: Delta)forall (Gamma : tyenv) (sigma : var -> term) (Delta : var -> ty) (T : ty), js Gamma sigma Delta -> js (T .: Gamma) (up sigma) (T .: Delta)forall (Gamma : tyenv) (sigma : var -> term) (Delta : var -> ty) (T : ty), js Gamma sigma Delta -> js (T .: Gamma) (up sigma) (T .: Delta)Gamma:tyenvsigma:var -> termDelta:var -> tyT:tyH:js Gamma sigma Deltajs (T .: Gamma) (up sigma) (T .: Delta)Gamma:tyenvsigma:var -> termDelta:var -> tyT:tyH:js Gamma sigma Deltajf (T .: Gamma) (ids 0) TGamma:tyenvsigma:var -> termDelta:var -> tyT:tyH:js Gamma sigma Deltax:natjf (T .: Gamma) (lift 1 (sigma x)) (Delta x)eauto with jf.Gamma:tyenvsigma:var -> termDelta:var -> tyT:tyH:js Gamma sigma Deltajf (T .: Gamma) (ids 0) TGamma:tyenvsigma:var -> termDelta:var -> tyT:tyH:js Gamma sigma Deltax:natjf (T .: Gamma) (lift 1 (sigma x)) (Delta x)eauto using jf_te_renaming_0. } Qed.Gamma:tyenvsigma:var -> termDelta:var -> tyT:tyH:js Gamma sigma Deltax:natjf (T .: Gamma) (lift 1 (sigma x)) (Delta x)
In the following statement, theta
is a substitution of types for
type variables. It is post-composed with the type environments
Gamma
and Delta
.
forall (Gamma : tyenv) (sigma : var -> term) (Delta theta : var -> ty), js Gamma sigma Delta -> js (Gamma >> theta) sigma (Delta >> theta)forall (Gamma : tyenv) (sigma : var -> term) (Delta theta : var -> ty), js Gamma sigma Delta -> js (Gamma >> theta) sigma (Delta >> theta)eauto using jf_ty_substitution. Qed.forall (Gamma : tyenv) (sigma : var -> term) (Delta theta : var -> ty), (forall x : var, jf Gamma (sigma x) (Delta x)) -> forall x : var, jf (Gamma >> theta) (sigma x) ((Delta >> theta) x)
The typing judgement is preserved by a well-typed substitution sigma
of (all) term variables to terms.
forall (Delta : tyenv) (t : term) (U : ty), jf Delta t U -> forall (Gamma : tyenv) (sigma : var -> term), js Gamma sigma Delta -> jf Gamma t.[sigma] Uinduction 1; intros; subst; asimpl; eauto using js_up, js_ty_substitution with jf. Qed.forall (Delta : tyenv) (t : term) (U : ty), jf Delta t U -> forall (Gamma : tyenv) (sigma : var -> term), js Gamma sigma Delta -> jf Gamma t.[sigma] U
As a corollary, the typing judgement is preserved by a well-typed substitution of one term for one variable, namely variable 0.
This property is exploited in the proof of subject reduction, in the case of beta-reduction.
forall (Gamma : var -> ty) (t1 t2 : term) (T U : ty), jf (T .: Gamma) t1 U -> jf Gamma t2 T -> jf Gamma t1.[t2/] Ueauto using jf_te_substitution, js_ids, js_cons. Qed.forall (Gamma : var -> ty) (t1 t2 : term) (T U : ty), jf (T .: Gamma) t1 U -> jf Gamma t2 T -> jf Gamma t1.[t2/] U