Library Substitution
The Substitution Lemma
Require Export Weakening.
Implicit Types x y z : var.
Implicit Types F G H : basetype.
Implicit Types A B C : inttype.
Implicit Types U V W : type.
Implicit Types Gamma Delta : context.
Typed Substitutions allow to go from one context to another and are formed inductively as follows:
- Renamings are TypedSubstitutions
- If sigma is a Typed Substitution from Gamma to Delta, and t has type U in Deltat, then t .: sigma is a Typed Substitution from U .: Gamma to Deltat & Delta.
Inductive tysub : (var -> term) -> context -> nat -> context -> Prop :=
| tysubRen xi Gamma Delta : tyren xi Gamma Delta -> tysub xi Gamma 0 Delta
| tysubCons {sigma Gamma n Delta} : tysub sigma Gamma n Delta ->
forall {Deltat m t U},
ty m Deltat t U ->
forall Gamma', Gamma' =1 U .: Gamma ->
forall Delta', Deltat & Delta ==1 Delta' ->
tysub (t .: sigma) Gamma' (n + m) Delta'.
The Beta Substutition is a Typed Substitution
Lemma tysub_beta {n Gamma Delta t U} :
ty n Delta t U ->
tysub (t .: ids) (U .: Gamma) n (Delta & Gamma).
intros tyt.
change n with (0 + n).
econstructor ; eauto.
constructor. exists (fun x => Some x) ; eauto.
Qed.
ty n Delta t U ->
tysub (t .: ids) (U .: Gamma) n (Delta & Gamma).
intros tyt.
change n with (0 + n).
econstructor ; eauto.
constructor. exists (fun x => Some x) ; eauto.
Qed.
Variables that are not used in the Typed Substitution can be mapped to any type
Lemma tysub_lift {sigma Gamma n Delta} : tysub sigma Gamma n Delta ->
tysub (sigma >>> rename (+1)) Gamma n (OMEGA .: Delta).
induction 1 as [? ? ? [ceta Bi1 Bi2 T] | ].
- constructor. exists (fun x => match x with 0 => None | S x' => ceta x' end) ; auto.
intros [|v] x e ; try discriminate.
rewrite (Bi1 v x) ; simpl ; auto.
- asimpl in *.
assert ((OMEGA .: Deltat) & (OMEGA .: Delta) ==1 OMEGA .: Delta') by eauto.
eauto using tysubCons, weakening.
Qed.
Extending with the identity mapping does not break Typed Substitutions
Lemma tysub_up {sigma Gamma n Delta} : tysub sigma Gamma n Delta -> forall U,
tysub (up sigma) (U .: Gamma) n (U .: Delta).
intros ts U.
assert ((U .: Empty) 0 >= U) by eauto.
replace n with (n + 0) by omega.
assert ((U .: Empty) & (OMEGA .: Delta) ==1 U .: Delta) by eauto.
assert (ty 0 (U .: Empty) (ids 0) U) by eauto using tyVarU.
econstructor ; eauto using tysub_lift.
Qed.
tysub (up sigma) (U .: Gamma) n (U .: Delta).
intros ts U.
assert ((U .: Empty) 0 >= U) by eauto.
replace n with (n + 0) by omega.
assert ((U .: Empty) & (OMEGA .: Delta) ==1 U .: Delta) by eauto.
assert (ty 0 (U .: Empty) (ids 0) U) by eauto using tyVarU.
econstructor ; eauto using tysub_lift.
Qed.
Typing of variables with F-Types is stable under substitution
Lemma tysubst_var {Gamma x F} : Gamma x >= F ->
forall sigma Delta n, tysub sigma Gamma n Delta -> ty n Delta (sigma x) F.
Proof with eauto 6 using tyren_var, tycsub, ty_subsume, tymon, cte_csub_R.
intros e sigma Delta n ts.
revert x F e. induction ts ; intros x F e ; eauto using tyren_var.
replace (Gamma' x) with ((U .: Gamma) x) in e by congruence.
destruct x ; simpl in *...
Qed.
Typed Substitutions can be split according to the source context
Lemma tysub_split {sigma Gamma n Delta} : tysub sigma Gamma n Delta -> forall {Gamma1 Gamma2}, Gamma1 & Gamma2 ==1 Gamma ->
exists n1 n2 Delta1 Delta2, n = n1 + n2 /\ Delta ==1 Delta1 & Delta2 /\ tysub sigma Gamma1 n1 Delta1 /\ tysub sigma Gamma2 n2 Delta2.
induction 1 as [xi ? ? tr | ? ? ? ? ? ? ? ? ? ? ? ? eG ? eD ] ; intros Gamma1 Gamma2 e.
- destruct (tyren_split tr e) as [Delta1 [Delta2 [R1 [R2 H]]]] ; eauto 10 using tysubRen.
- destruct (IHtysub (drop 1 Gamma1) (drop 1 Gamma2)) as [n1' [n2' [D1' [D2' [A1 [A2 [A3 A4]]]]]]].
{ intros x ; simpl. now rewrite (e (S x)), eG. }
assert (I : ty m Deltat t (Gamma1 0 * Gamma2 0)).
{ now rewrite (e 0), eG. }
destruct (invtyInt I) as [n1 [n2 [Deltat1 [Deltat2 [B1 [B2 [B3 B4]]]]]]].
exists (n1' + n1), (n2' + n2), (Deltat1 & D1'), (Deltat2 & D2').
intuition ; eauto 3 using tysubCons, cons_drop_inv.
rewrite <- eD, A2, <- B2.
rewrite ! cte_assoc_cint.
intros x ; simpl ; eauto.
Qed.
Typing is stable under substiution
Theorem tysubst {n Gamma s A} : ty n Gamma s A ->
forall {sigma Delta m}, tysub sigma Gamma m Delta -> ty (n + m) Delta s.[ sigma ] A.
induction 1 ; intros sigma Gamma' c ts ; simpl ; asimpl ; eauto using tysubst_var, tymon, tysub_up.
- destruct (tysub_split ts e) as [n1 [n2 [Delta1 [Delta2 [? [? [ts1 ts2]]]]]]].
replace (n + m + c) with ((n + n1) + (m + n2)) by omega.
eauto.
- destruct (tysub_split ts e) as [n1 [n2 [Delta1 [Delta2 [? [? [ts1 ts2]]]]]]].
replace (n + m + c) with ((n + n1) + (m + n2)) by omega.
eauto.
Qed.