Renamings of term variables

The typing judgement is preserved by a renaming xi that maps term variables to term variables.

Note that xi need not be injective or surjective.

When xi is not surjective, we get a weakening lemma (see the next lemma, below). When xi is not injective, we obtain a contraction lemma (not shown here).

Lemma jt_te_renaming:
  forall Gamma t U,
  jt Gamma t U ->
  forall Gamma' xi,
  Gamma = xi >>> Gamma' ->
  jt Gamma' t.[ren xi] U.
forall (Gamma : tyenv) (t : term) (U : ty),
jt Gamma t U ->
forall (Gamma' : var -> ty) (xi : var -> var),
Gamma = xi >>> Gamma' -> jt Gamma' t.[ren xi] U
Proof.
forall (Gamma : tyenv) (t : term) (U : ty),
jt Gamma t U ->
forall (Gamma' : var -> ty) (xi : var -> var),
Gamma = xi >>> Gamma' -> jt Gamma' t.[ren xi] U
  (* A detailed proof, where every case is dealt with explicitly: *)
  induction 1; intros; subst.
x:var
Gamma':var -> ty
xi:var -> var
jt Gamma' (Var x).[ren xi] ((xi >>> Gamma') x)
t:term
T, U:ty
Gamma':var -> ty
xi:var -> var
IHjt:forall (Gamma'0 : var -> ty) (xi0 : var -> var),
T .: xi >>> Gamma' = xi0 >>> Gamma'0 ->
jt Gamma'0 t.[ren xi0] U
H:jt (T .: xi >>> Gamma') t U
jt Gamma' (Lam t).[ren xi] (TyFun T U)
t1, t2:term
T, U:ty
Gamma':var -> ty
xi:var -> var
IHjt2:forall (Gamma'0 : var -> ty)
  (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jt Gamma'0 t2.[ren xi0] T
IHjt1:forall (Gamma'0 : var -> ty)
  (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jt Gamma'0 t1.[ren xi0] (TyFun T U)
H0:jt (xi >>> Gamma') t2 T
H:jt (xi >>> Gamma') t1 (TyFun T U)
jt Gamma' (App t1 t2).[ren xi] U
  (* JTVar *)
  {
x:var
Gamma':var -> ty
xi:var -> var
jt Gamma' (Var x).[ren xi] ((xi >>> Gamma') x) asimpl.
x:var
Gamma':var -> ty
xi:var -> var
jt Gamma' (ids (xi x)) (Gamma' (xi x)) econstructor.
x:var
Gamma':var -> ty
xi:var -> var
Gamma' (xi x) = Gamma' (xi x) eauto. }
t:term
T, U:ty
Gamma':var -> ty
xi:var -> var
IHjt:forall (Gamma'0 : var -> ty) (xi0 : var -> var),
T .: xi >>> Gamma' = xi0 >>> Gamma'0 ->
jt Gamma'0 t.[ren xi0] U
H:jt (T .: xi >>> Gamma') t U
jt Gamma' (Lam t).[ren xi] (TyFun T U)
t1, t2:term
T, U:ty
Gamma':var -> ty
xi:var -> var
IHjt2:forall (Gamma'0 : var -> ty)
  (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jt Gamma'0 t2.[ren xi0] T
IHjt1:forall (Gamma'0 : var -> ty)
  (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jt Gamma'0 t1.[ren xi0] (TyFun T U)
H0:jt (xi >>> Gamma') t2 T
H:jt (xi >>> Gamma') t1 (TyFun T U)
jt Gamma' (App t1 t2).[ren xi] U
  (* JTLam *)
  {
t:term
T, U:ty
Gamma':var -> ty
xi:var -> var
IHjt:forall (Gamma'0 : var -> ty) (xi0 : var -> var),
T .: xi >>> Gamma' = xi0 >>> Gamma'0 ->
jt Gamma'0 t.[ren xi0] U
H:jt (T .: xi >>> Gamma') t U
jt Gamma' (Lam t).[ren xi] (TyFun T U) asimpl.
t:term
T, U:ty
Gamma':var -> ty
xi:var -> var
IHjt:forall (Gamma'0 : var -> ty) (xi0 : var -> var),
T .: xi >>> Gamma' = xi0 >>> Gamma'0 ->
jt Gamma'0 t.[ren xi0] U
H:jt (T .: xi >>> Gamma') t U
jt Gamma' (Lam t.[ren (upren xi)]) (TyFun T U) econstructor.
t:term
T, U:ty
Gamma':var -> ty
xi:var -> var
IHjt:forall (Gamma'0 : var -> ty) (xi0 : var -> var),
T .: xi >>> Gamma' = xi0 >>> Gamma'0 ->
jt Gamma'0 t.[ren xi0] U
H:jt (T .: xi >>> Gamma') t U
jt (T .: Gamma') t.[ren (upren xi)] U eapply IHjt.
t:term
T, U:ty
Gamma':var -> ty
xi:var -> var
IHjt:forall (Gamma'0 : var -> ty) (xi0 : var -> var),
T .: xi >>> Gamma' = xi0 >>> Gamma'0 ->
jt Gamma'0 t.[ren xi0] U
H:jt (T .: xi >>> Gamma') t U
T .: xi >>> Gamma' = upren xi >>> T .: Gamma' autosubst. }
t1, t2:term
T, U:ty
Gamma':var -> ty
xi:var -> var
IHjt2:forall (Gamma'0 : var -> ty)
  (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jt Gamma'0 t2.[ren xi0] T
IHjt1:forall (Gamma'0 : var -> ty)
  (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jt Gamma'0 t1.[ren xi0] (TyFun T U)
H0:jt (xi >>> Gamma') t2 T
H:jt (xi >>> Gamma') t1 (TyFun T U)
jt Gamma' (App t1 t2).[ren xi] U
  (* JTApp *)
  {
t1, t2:term
T, U:ty
Gamma':var -> ty
xi:var -> var
IHjt2:forall (Gamma'0 : var -> ty)
  (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jt Gamma'0 t2.[ren xi0] T
IHjt1:forall (Gamma'0 : var -> ty)
  (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jt Gamma'0 t1.[ren xi0] (TyFun T U)
H0:jt (xi >>> Gamma') t2 T
H:jt (xi >>> Gamma') t1 (TyFun T U)
jt Gamma' (App t1 t2).[ren xi] U asimpl.
t1, t2:term
T, U:ty
Gamma':var -> ty
xi:var -> var
IHjt2:forall (Gamma'0 : var -> ty)
  (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jt Gamma'0 t2.[ren xi0] T
IHjt1:forall (Gamma'0 : var -> ty)
  (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jt Gamma'0 t1.[ren xi0] (TyFun T U)
H0:jt (xi >>> Gamma') t2 T
H:jt (xi >>> Gamma') t1 (TyFun T U)
jt Gamma' (App t1.[ren xi] t2.[ren xi]) U econstructor.
t1, t2:term
T, U:ty
Gamma':var -> ty
xi:var -> var
IHjt2:forall (Gamma'0 : var -> ty)
  (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jt Gamma'0 t2.[ren xi0] T
IHjt1:forall (Gamma'0 : var -> ty)
  (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jt Gamma'0 t1.[ren xi0] (TyFun T U)
H0:jt (xi >>> Gamma') t2 T
H:jt (xi >>> Gamma') t1 (TyFun T U)
jt Gamma' t1.[ren xi] (TyFun ?T U)
t1, t2:term
T, U:ty
Gamma':var -> ty
xi:var -> var
IHjt2:forall (Gamma'0 : var -> ty)
  (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jt Gamma'0 t2.[ren xi0] T
IHjt1:forall (Gamma'0 : var -> ty)
  (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jt Gamma'0 t1.[ren xi0] (TyFun T U)
H0:jt (xi >>> Gamma') t2 T
H:jt (xi >>> Gamma') t1 (TyFun T U)
jt Gamma' t2.[ren xi] ?T eauto.
t1, t2:term
T, U:ty
Gamma':var -> ty
xi:var -> var
IHjt2:forall (Gamma'0 : var -> ty)
  (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jt Gamma'0 t2.[ren xi0] T
IHjt1:forall (Gamma'0 : var -> ty)
  (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jt Gamma'0 t1.[ren xi0] (TyFun T U)
H0:jt (xi >>> Gamma') t2 T
H:jt (xi >>> Gamma') t1 (TyFun T U)
jt Gamma' t2.[ren xi] T eauto. }
Restart.
forall (Gamma : tyenv) (t : term) (U : ty),
jt Gamma t U ->
forall (Gamma' : var -> ty) (xi : var -> var),
Gamma = xi >>> Gamma' -> jt Gamma' t.[ren xi] U
  (* A shorter script, where all cases are dealt with uniformly: *)
  induction 1; intros; subst; asimpl;
  econstructor; eauto with autosubst.
Qed.

As a corollary, jt is preserved by the renaming (+1).

This lemma is usually known as a weakening lemma, where the word "weakening" is used in the sense of linear logic. On paper, in nominal style (as opposed to de Bruijn style), one would write: if the typing judgement Γ ⊢ t : U holds, and if the variable x does not occur in t, then the typing judgement Γ; x : T ⊢ t : U holds.

Here, the variable x is represented by the de Bruijn index 0.

Lemma jt_te_renaming_0:
  forall Gamma t T U,
  jt Gamma t U ->
  jt (T .: Gamma) (lift 1 t) U.
forall (Gamma : tyenv) (t : term) (T U : ty),
jt Gamma t U -> jt (T .: Gamma) (lift 1 t) U
Proof.
forall (Gamma : tyenv) (t : term) (T U : ty),
jt Gamma t U -> jt (T .: Gamma) (lift 1 t) U
  intros.
Gamma:tyenv
t:term
T, U:ty
H:jt Gamma t U
jt (T .: Gamma) (lift 1 t) U eapply jt_te_renaming.
Gamma:tyenv
t:term
T, U:ty
H:jt Gamma t U
jt ?Gamma t U
Gamma:tyenv
t:term
T, U:ty
H:jt Gamma t U
?Gamma = (+1) >>> T .: Gamma eauto.
Gamma:tyenv
t:term
T, U:ty
H:jt Gamma t U
Gamma = (+1) >>> T .: Gamma autosubst.
Qed.

Substitutions of terms for term variables

The typing judgement is extended to substitutions of terms for term variables.

With respect to a type environment Gamma, a substitution sigma has type Delta if and only if, for every variable x, the term sigma x has type Delta x.

This auxiliary judgement encourages us to think of terms of total substitutions, where every variable is replaced by a term. This concept turns out to be easier to understand and manipulate, especially during proofs by induction. Of course one always later consider the special case of a substitution that seems to affect just one variable, say variable 0. (In reality, such a substitution affects all variables, as the variables other than 0 are renumbered.)

Definition js Gamma sigma Delta :=
  forall x : var,
  jt Gamma (sigma x) (Delta x).

The following are basic lemmas about js.

The identity substitution has type Gamma in environment Gamma.

Lemma js_ids:
  forall Gamma,
  js Gamma ids Gamma.
forall Gamma : tyenv, js Gamma ids Gamma
Proof.
forall Gamma : tyenv, js Gamma ids Gamma
  unfold js.
forall (Gamma : tyenv) (x : var),
jt Gamma (ids x) (Gamma x) eauto with jt.
Qed.

The typing judgement js behaves like an infinite list of typing judgements jt. So, one can prepend one more jt judgement in front of it.

Lemma js_cons:
  forall Gamma t sigma T Delta,
  jt 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),
jt Gamma t T ->
js Gamma sigma Delta ->
js Gamma (t .: sigma) (T .: Delta)
Proof.
forall (Gamma : tyenv) (t : term)
  (sigma : var -> term) (T : ty) (Delta : var -> ty),
jt Gamma t T ->
js Gamma sigma Delta ->
js Gamma (t .: sigma) (T .: Delta)
  intros.
Gamma:tyenv
t:term
sigma:var -> term
T:ty
Delta:var -> ty
H:jt Gamma t T
H0:js Gamma sigma Delta
js Gamma (t .: sigma) (T .: Delta) intros [|x]; asimpl; eauto.
Qed.

The typing judgement js is preserved by the introduction of a new term variable. That is, a typing judgement js can be pushed under a lambda-abstraction.

Lemma js_up:
  forall Gamma sigma Delta T,
  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)
Proof.
forall (Gamma : tyenv) (sigma : var -> term)
  (Delta : var -> ty) (T : ty),
js Gamma sigma Delta ->
js (T .: Gamma) (up sigma) (T .: Delta)
  intros.
Gamma:tyenv
sigma:var -> term
Delta:var -> ty
T:ty
H:js Gamma sigma Delta
js (T .: Gamma) (up sigma) (T .: Delta) eapply js_cons.
Gamma:tyenv
sigma:var -> term
Delta:var -> ty
T:ty
H:js Gamma sigma Delta
jt (T .: Gamma) (ids 0) T
Gamma:tyenv
sigma:var -> term
Delta:var -> ty
T:ty
H:js Gamma sigma Delta
js (T .: Gamma) (sigma >>> rename (+1)) Delta
  {
Gamma:tyenv
sigma:var -> term
Delta:var -> ty
T:ty
H:js Gamma sigma Delta
jt (T .: Gamma) (ids 0) T eauto with jt. }
Gamma:tyenv
sigma:var -> term
Delta:var -> ty
T:ty
H:js Gamma sigma Delta
js (T .: Gamma) (sigma >>> rename (+1)) Delta
  {
Gamma:tyenv
sigma:var -> term
Delta:var -> ty
T:ty
H:js Gamma sigma Delta
js (T .: Gamma) (sigma >>> rename (+1)) Delta intro x.
Gamma:tyenv
sigma:var -> term
Delta:var -> ty
T:ty
H:js Gamma sigma Delta
x:var
jt (T .: Gamma) ((sigma >>> rename (+1)) x) (Delta x) asimpl.
Gamma:tyenv
sigma:var -> term
Delta:var -> ty
T:ty
H:js Gamma sigma Delta
x:var
jt (T .: Gamma) (lift 1 (sigma x)) (Delta x) eauto using jt_te_renaming_0. }
Qed.

The typing judgement is preserved by a well-typed substitution sigma of (all) term variables to terms.

Lemma jt_te_substitution:
  forall Delta t U,
  jt Delta t U ->
  forall Gamma sigma,
  js Gamma sigma Delta ->
  jt Gamma t.[sigma] U.
forall (Delta : tyenv) (t : term) (U : ty),
jt Delta t U ->
forall (Gamma : tyenv) (sigma : var -> term),
js Gamma sigma Delta -> jt Gamma t.[sigma] U
Proof.
forall (Delta : tyenv) (t : term) (U : ty),
jt Delta t U ->
forall (Gamma : tyenv) (sigma : var -> term),
js Gamma sigma Delta -> jt Gamma t.[sigma] U
  (* A short script, where all cases are dealt with in the same way: *)
  induction 1; intros; subst; asimpl; eauto using js_up with jt.
Qed.

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.

Lemma jt_te_substitution_0:
  forall Gamma t1 t2 T U,
  jt (T .: Gamma) t1 U ->
  jt Gamma t2 T ->
  jt Gamma t1.[t2/] U.
forall (Gamma : var -> ty) (t1 t2 : term) (T U : ty),
jt (T .: Gamma) t1 U ->
jt Gamma t2 T -> jt Gamma t1.[t2/] U
Proof.
forall (Gamma : var -> ty) (t1 t2 : term) (T U : ty),
jt (T .: Gamma) t1 U ->
jt Gamma t2 T -> jt Gamma t1.[t2/] U
  (* One can do the proof step by step as follows: *)
  intros.
Gamma:var -> ty
t1, t2:term
T, U:ty
H:jt (T .: Gamma) t1 U
H0:jt Gamma t2 T
jt Gamma t1.[t2/] U eapply jt_te_substitution.
Gamma:var -> ty
t1, t2:term
T, U:ty
H:jt (T .: Gamma) t1 U
H0:jt Gamma t2 T
jt ?Delta t1 U
Gamma:var -> ty
t1, t2:term
T, U:ty
H:jt (T .: Gamma) t1 U
H0:jt Gamma t2 T
js Gamma (t2 .: ids) ?Delta
  {
Gamma:var -> ty
t1, t2:term
T, U:ty
H:jt (T .: Gamma) t1 U
H0:jt Gamma t2 T
jt ?Delta t1 U eauto. }
Gamma:var -> ty
t1, t2:term
T, U:ty
H:jt (T .: Gamma) t1 U
H0:jt Gamma t2 T
js Gamma (t2 .: ids) (T .: Gamma)
  {
Gamma:var -> ty
t1, t2:term
T, U:ty
H:jt (T .: Gamma) t1 U
H0:jt Gamma t2 T
js Gamma (t2 .: ids) (T .: Gamma) eapply js_cons.
Gamma:var -> ty
t1, t2:term
T, U:ty
H:jt (T .: Gamma) t1 U
H0:jt Gamma t2 T
jt Gamma t2 T
Gamma:var -> ty
t1, t2:term
T, U:ty
H:jt (T .: Gamma) t1 U
H0:jt Gamma t2 T
js Gamma ids Gamma
    {
Gamma:var -> ty
t1, t2:term
T, U:ty
H:jt (T .: Gamma) t1 U
H0:jt Gamma t2 T
jt Gamma t2 T eauto. }
Gamma:var -> ty
t1, t2:term
T, U:ty
H:jt (T .: Gamma) t1 U
H0:jt Gamma t2 T
js Gamma ids Gamma
    {
Gamma:var -> ty
t1, t2:term
T, U:ty
H:jt (T .: Gamma) t1 U
H0:jt Gamma t2 T
js Gamma ids Gamma eapply js_ids. } }
  (* Of course one can also let Coq find the proof by itself: *)
  Restart.
forall (Gamma : var -> ty) (t1 t2 : term) (T U : ty),
jt (T .: Gamma) t1 U ->
jt Gamma t2 T -> jt Gamma t1.[t2/] U eauto using jt_te_substitution, js_ids, js_cons.
Qed.