Set Implicit Arguments.
Require Import MyTactics.
Require Import DeBruijn.
Require Import Types.
Require Import TypeEquality.
Require Import MoreTypeEquality.
Require Import TypeContexts.
Require Import FocusPaths.
Require Import Coercions.
Require Import Programs.
Require Import Subtyping.
Require Import Typing.
Require Import Environments.
Require Import PreliminaryLemmas.
Require Import Multiplicity.
Hint Extern 1 =>
rewrite <-
lift_subst_1_ty :
type_substitution.
Hint Extern 1 =>
rewrite env_subst_lift :
type_substitution.
Hint Extern 1 =>
rewrite <-
lift_subst_1_ty_ctx :
type_substitution.
Hint Resolve jpath_subst :
type_substitution.
-------------------------------------------------------------------------
Stability of typing by type substitution.
Lemma jco_type_substitution:
forall C c T,
jco C c T ->
forall U k,
wf U ->
jco (
subst_ty_env U k C)
c (
subst_ty U k T).
Proof.
induction 1;
intros;
simpl in *;
CoDefocus:
repeat rewrite subst_fill;
simpl;
eauto 8
with type_substitution.
CoForallElim
rewrite subst_subst_ty;
eauto.
CoExistsIntro
rewrite subst_subst_ty;
eauto.
CoTensorExchange
repeat rewrite subst_tensors;
simpl.
econstructor;
eauto.
rewrite map_length;
eauto.
Qed.
Lemma jco_type_substitution_nil_arrow:
forall c T1 T2,
jco nil c (
T1 -->
T2) ->
forall U k,
wf U ->
jco nil c (
subst_ty U k T1 -->
subst_ty U k T2).
Proof.
Lemma jp_type_substitution:
forall p T1 T2,
jp p T1 T2 ->
forall k U,
wf U ->
jp p (
subst_ty U k T1) (
subst_ty U k T2).
Proof.
induction 1;
simpl;
intros;
repeat rewrite subst_fill;
simpl;
eauto 6
with type_substitution.
Qed.
Hint Resolve jco_type_substitution_nil_arrow jp_type_substitution :
type_substitution.
Hint Extern 3 =>
rewrite <-
subst_subst_ty :
type_substitution.
Hint Extern 3 =>
rewrite lift_subst_1_ty :
type_substitution.
Lemma j_type_substitution:
(
forall R M E v T,
jv R M E v T ->
forall k U,
wf U ->
jv R M (
subst_ty_env U k E)
v (
subst_ty U k T)
) /\ (
forall R vs T,
ji R vs T ->
forall k U,
wf U ->
ji R vs (
subst_ty U k T)
) /\ (
forall R M E t T,
jt R M E t T ->
forall k U,
wf U ->
jt R M (
subst_ty_env U k E)
t (
subst_ty U k T)
).
Proof.
apply jvit_ind;
simpl in *;
intros;
econstructor;
simpl;
eauto with type_substitution.
Qed.
Lemma j_type_substitution_0:
(
forall R M E v T,
jv R M (
E!)
v T ->
forall U,
wf U ->
jv R M E v (
subst_ty U 0
T)
) /\ (
forall R M E t T,
jt R M (
E!)
t T ->
forall U,
wf U ->
jt R M E t (
subst_ty U 0
T)
).
Proof.
Lemma j_type_substitution_0_term:
forall R M E t T,
jt R M (
E!)
t T ->
forall U,
wf U ->
jt R M E t (
subst_ty U 0
T).
Proof.
Lemma j_term_type_substitution_unpack:
forall R M E T1 t T2,
jt R M (
E!;;
T1)
t (
lift_ty 0
T2) ->
forall U,
wf U ->
jt R M (
E;;
subst_ty U 0
T1)
t T2.
Proof.