--- /dev/null
+Require drop_props.
+Require csubst0_defs.
+Require pc3_props.
+Require pc3_subst0.
+Require ty0_defs.
+Require ty0_lift.
+Require ty0_props.
+
+ Section ty0_fsubst0. (****************************************************)
+
+(*#* #stop macro *)
+
+ Tactic Definition IH H0 v1 v2 v3 v4 v5 :=
+ LApply (H0 v1 v2 v3 v4); [ Intros H_x | XEAuto ];
+ LApply H_x; [ Clear H_x; Intros H_x | XEAuto ];
+ LApply (H_x v5); [ Clear H_x; Intros | XEAuto ].
+
+ Tactic Definition IHT :=
+ Match Context With
+ [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 ?1 ?2 c2 t2) ->
+ (wf0 ?3 c2) ->
+ (e:C) (drop i (0) ?1 (CTail e (Bind Abbr) u0)) -> ?;
+ _: (subst0 ?4 ?5 ?2 ?6);
+ _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
+ IH H ?4 ?5 ?1 ?6 ?9.
+
+ Tactic Definition IHTb1 :=
+ Match Context With
+ [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 (CTail ?1 (Bind ?11) ?10) ?2 c2 t2) ->
+ (wf0 ?3 c2) ->
+ (e:C) (drop i (0) (CTail ?1 (Bind ?11) ?10) (CTail e (Bind Abbr) u0)) -> ?;
+ _: (subst0 ?4 ?5 ?10 ?6);
+ _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
+ IH H '(S ?4) ?5 '(CTail ?1 (Bind ?11) ?6) ?2 ?9.
+
+ Tactic Definition IHTb2 :=
+ Match Context With
+ [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 (CTail ?1 (Bind ?11) ?10) ?2 c2 t2) ->
+ (wf0 ?3 c2) ->
+ (e:C) (drop i (0) (CTail ?1 (Bind ?11) ?10) (CTail e (Bind Abbr) u0)) -> ?;
+ _: (subst0 (s (Bind ?11) ?4) ?5 ?2 ?6);
+ _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
+ IH H '(S ?4) ?5 '(CTail ?1 (Bind ?11) ?10) ?6 ?9.
+
+ Tactic Definition IHC :=
+ Match Context With
+ [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 ?1 ?2 c2 t2) ->
+ (wf0 ?3 c2) ->
+ (e:C) (drop i (0) ?1 (CTail e (Bind Abbr) u0)) -> ?;
+ _: (csubst0 ?4 ?5 ?1 ?6);
+ _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
+ IH H ?4 ?5 ?6 ?2 ?9.
+
+ Tactic Definition IHCb :=
+ Match Context With
+ [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 (CTail ?1 (Bind ?11) ?10) ?2 c2 t2) ->
+ (wf0 ?3 c2) ->
+ (e:C) (drop i (0) (CTail ?1 (Bind ?11) ?10) (CTail e (Bind Abbr) u0)) -> ?;
+ _: (csubst0 ?4 ?5 ?1 ?6);
+ _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
+ IH H '(S ?4) ?5 '(CTail ?6 (Bind ?11) ?10) ?2 ?9.
+
+ Tactic Definition IHTTb :=
+ Match Context With
+ [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 (CTail ?1 (Bind ?11) ?10) ?2 c2 t2) ->
+ (wf0 ?3 c2) ->
+ (e:C) (drop i (0) (CTail ?1 (Bind ?11) ?10) (CTail e (Bind Abbr) u0)) -> ?;
+ _: (subst0 ?4 ?5 ?10 ?6);
+ _: (subst0 (s (Bind ?11) ?4) ?5 ?2 ?7);
+ _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
+ IH H '(S ?4) ?5 '(CTail ?1 (Bind ?11) ?6) ?7 ?9.
+
+ Tactic Definition IHCT :=
+ Match Context With
+ [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 ?1 ?2 c2 t2) ->
+ (wf0 ?3 c2) ->
+ (e:C) (drop i (0) ?1 (CTail e (Bind Abbr) u0)) -> ?;
+ _: (csubst0 ?4 ?5 ?1 ?6);
+ _: (subst0 ?4 ?5 ?2 ?7);
+ _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
+ IH H ?4 ?5 ?6 ?7 ?9.
+
+ Tactic Definition IHCTb1 :=
+ Match Context With
+ [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 (CTail ?1 (Bind ?11) ?10) ?2 c2 t2) ->
+ (wf0 ?3 c2) ->
+ (e:C) (drop i (0) (CTail ?1 (Bind ?11) ?10) (CTail e (Bind Abbr) u0)) -> ?;
+ _: (csubst0 ?4 ?5 ?1 ?6);
+ _: (subst0 ?4 ?5 ?10 ?7);
+ _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
+ IH H '(S ?4) ?5 '(CTail ?6 (Bind ?11) ?7) ?2 ?9.
+
+ Tactic Definition IHCTb2 :=
+ Match Context With
+ [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 (CTail ?1 (Bind ?11) ?10) ?2 c2 t2) ->
+ (wf0 ?3 c2) ->
+ (e:C) (drop i (0) (CTail ?1 (Bind ?11) ?10) (CTail e (Bind Abbr) u0)) -> ?;
+ _: (csubst0 ?4 ?5 ?1 ?6);
+ _: (subst0 (s (Bind ?11) ?4) ?5 ?2 ?7);
+ _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
+ IH H '(S ?4) ?5 '(CTail ?6 (Bind ?11) ?10) ?7 ?9.
+
+ Tactic Definition IHCTTb :=
+ Match Context With
+ [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 (CTail ?1 (Bind ?11) ?10) ?2 c2 t2) ->
+ (wf0 ?3 c2) ->
+ (e:C) (drop i (0) (CTail ?1 (Bind ?11) ?10) (CTail e (Bind Abbr) u0)) -> ?;
+ _: (csubst0 ?4 ?5 ?1 ?6);
+ _: (subst0 ?4 ?5 ?10 ?7);
+ _: (subst0 (s (Bind ?11) ?4) ?5 ?2 ?8);
+ _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
+ IH H '(S ?4) ?5 '(CTail ?6 (Bind ?11) ?7) ?8 ?9.
+
+(*#* #start macro *)
+
+(*#* #caption "substitution preserves types" *)
+(*#* #cap #cap c1, c2, e, t1, t2, t #alpha u in V *)
+
+(* NOTE: This breaks the mutual recursion between ty0_subst0 and ty0_csubst0 *)
+ Theorem ty0_fsubst0: (g:?; c1:?; t1,t:?) (ty0 g c1 t1 t) ->
+ (i:?; u,c2,t2:?) (fsubst0 i u c1 t1 c2 t2) ->
+ (wf0 g c2) ->
+ (e:?) (drop i (0) c1 (CTail e (Bind Abbr) u)) ->
+ (ty0 g c2 t2 t).
+
+(*#* #stop file *)
+
+ Intros until 1; XElim H.
+(* case 1: ty0_conv *)
+ Intros until 6; XElim H4; Intros.
+(* case 1.1: fsubst0_t *)
+ IHT; EApply ty0_conv; XEAuto.
+(* case 1.2: fsubst0_c *)
+ IHC; EApply ty0_conv; Try EApply pc3_fsubst0; XEAuto.
+(* case 1.3: fsubst0_b *)
+ IHCT; IHCT; EApply ty0_conv; Try EApply pc3_fsubst0; XEAuto.
+(* case 2: ty0_sort *)
+ Intros until 2; XElim H0; Intros.
+(* case 2.1: fsubst0_t *)
+ Subst0GenBase.
+(* case 2.2: fsubst0_c *)
+ XAuto.
+(* case 2.3: fsubst0_b *)
+ Subst0GenBase.
+(* case 3: ty0_abbr *)
+ Intros until 5; XElim H3; Intros; Clear c1 c2 t t1 t2.
+(* case 3.1: fsubst0_t *)
+ Subst0GenBase; Rewrite H6; Rewrite <- H3 in H5; Clear H3 H6 i t3.
+ DropDis; Inversion H5; Rewrite <- H6 in H0; Rewrite H7 in H1; XEAuto.
+(* case 3.2: fsubst0_c *)
+ Apply (lt_le_e n i); Intros; CSubst0Drop.
+(* case 3.2.1: n < i, none *)
+ EApply ty0_abbr; XEAuto.
+(* case 3.2.2: n < i, csubst0_fst *)
+ Inversion H0; CSubst0Drop.
+ Rewrite <- H10 in H7; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H8;
+ Clear H0 H10 H11 H12 x0 x1 x2.
+ DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase | XAuto ].
+ IHT; EApply ty0_abbr; XEAuto.
+(* case 3.2.3: n < i, csubst0_snd *)
+ Inversion H0; CSubst0Drop.
+ Rewrite <- H10 in H8; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H7;
+ Clear H0 H10 H11 H12 x0 x1 x3.
+ DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase; CSubst0Drop | XAuto ].
+ IHC; EApply ty0_abbr; XEAuto.
+(* case 3.2.4: n < i, csubst0_both *)
+ Inversion H0; CSubst0Drop.
+ Rewrite <- H11 in H9; Rewrite <- H12 in H7; Rewrite <- H12 in H8; Rewrite <- H12 in H9; Rewrite <- H13 in H8;
+ Clear H0 H11 H12 H13 x0 x1 x3.
+ DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase; CSubst0Drop | XAuto ].
+ IHCT; EApply ty0_abbr; XEAuto.
+(* case 3.2.5: n >= i *)
+ EApply ty0_abbr; XEAuto.
+(* case 3.3: fsubst0_b *)
+ Subst0GenBase; Rewrite H7; Rewrite <- H3 in H4; Rewrite <- H3 in H6; Clear H3 H7 i t3.
+ DropDis; Inversion H6; Rewrite <- H7 in H0; Rewrite H8 in H1.
+ CSubst0Drop; XEAuto.
+(* case 4: ty0_abst *)
+ Intros until 5; XElim H3; Intros; Clear c1 c2 t t1 t2.
+(* case 4.1: fsubst0_t *)
+ Subst0GenBase; Rewrite H3 in H0; DropDis; Inversion H0.
+(* case 4.2: fsubst0_c *)
+ Apply (lt_le_e n i); Intros; CSubst0Drop.
+(* case 4.2.1: n < i, none *)
+ EApply ty0_abst; XEAuto.
+(* case 4.2.2: n < i, csubst0_fst *)
+ Inversion H0; CSubst0Drop.
+ Rewrite <- H10 in H7; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H8; Rewrite <- H12;
+ Clear H0 H10 H11 H12 x0 x1 x2.
+ DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase | XAuto ].
+ IHT; EApply ty0_conv;
+ [ EApply ty0_lift | EApply ty0_abst | EApply pc3_lift ]; XEAuto.
+(* case 4.2.3: n < i, csubst0_snd *)
+ Inversion H0; CSubst0Drop.
+ Rewrite <- H10 in H8; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H7; Rewrite <- H12;
+ Clear H0 H10 H11 H12 x0 x1 x3.
+ DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase; CSubst0Drop | XAuto ].
+ IHC; EApply ty0_abst; XEAuto.
+(* case 4.2.4: n < i, csubst0_both *)
+ Inversion H0; CSubst0Drop.
+ Rewrite <- H11 in H9; Rewrite <- H12 in H7; Rewrite <- H12 in H8; Rewrite <- H12 in H9; Rewrite <- H13 in H8; Rewrite <- H13;
+ Clear H0 H11 H12 H13 x0 x1 x3.
+ DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase; CSubst0Drop | XAuto ].
+ IHCT; IHC; EApply ty0_conv;
+ [ EApply ty0_lift | EApply ty0_abst
+ | EApply pc3_lift; Try EApply pc3_fsubst0; Try Apply H0
+ ]; XEAuto.
+(* case 4.2.4: n >= i *)
+ EApply ty0_abst; XEAuto.
+(* case 4.3: fsubst0_b *)
+ Subst0GenBase; Rewrite H3 in H0; DropDis; Inversion H0.
+(* case 5: ty0_bind *)
+ Intros until 7; XElim H5; Intros; Clear H4.
+(* case 5.1: fsubst0_t *)
+ Subst0GenBase; Rewrite H4; Clear H4 t6.
+(* case 5.1.1: subst0 on left argument *)
+ Ty0Correct; IHT; IHTb1; Ty0Correct.
+ EApply ty0_conv;
+ [ EApply ty0_bind | EApply ty0_bind | EApply pc3_fsubst0 ]; XEAuto.
+(* case 5.1.2: subst0 on right argument *)
+ IHTb2; Ty0Correct; EApply ty0_bind; XEAuto.
+(* case 5.1.3: subst0 on both arguments *)
+ Ty0Correct; IHT; IHTb1; IHTTb; Ty0Correct.
+ EApply ty0_conv;
+ [ EApply ty0_bind | EApply ty0_bind | EApply pc3_fsubst0 ]; XEAuto.
+(* case 5.2: fsubst0_c *)
+ IHC; IHCb; Ty0Correct; EApply ty0_bind; XEAuto.
+(* case 5.3: fsubst0_b *)
+ Subst0GenBase; Rewrite H4; Clear H4 t6.
+(* case 5.3.1: subst0 on left argument *)
+ IHC; IHCb; Ty0Correct; Ty0Correct; IHCT; IHCTb1; Ty0Correct.
+ EApply ty0_conv;
+ [ EApply ty0_bind | EApply ty0_bind
+ | EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]; XEAuto.
+(* case 5.3.2: subst0 on right argument *)
+ IHC; IHCTb2; Ty0Correct; EApply ty0_bind; XEAuto.
+(* case 5.3.3: subst0 on both arguments *)
+ IHC; IHCb; Ty0Correct; Ty0Correct; IHCT; IHCTTb; Ty0Correct.
+ EApply ty0_conv;
+ [ EApply ty0_bind | EApply ty0_bind
+ | EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]; XEAuto.
+(* case 6: ty0_appl *)
+ Intros until 5; XElim H3; Intros.
+(* case 6.1: fsubst0_t *)
+ Subst0GenBase; Rewrite H3; Clear H3 c1 c2 t t1 t2 t3.
+(* case 6.1.1: subst0 on left argument *)
+ Ty0Correct; Ty0GenBase; IHT; Ty0Correct.
+ EApply ty0_conv;
+ [ EApply ty0_appl | EApply ty0_appl | EApply pc3_fsubst0 ]; XEAuto.
+(* case 6.1.2: subst0 on right argument *)
+ IHT; EApply ty0_appl; XEAuto.
+(* case 6.1.3: subst0 on both arguments *)
+ Ty0Correct; Ty0GenBase; Move H after H10; Ty0Correct; IHT; Clear H2; IHT.
+ EApply ty0_conv;
+ [ EApply ty0_appl | EApply ty0_appl | EApply pc3_fsubst0 ]; XEAuto.
+(* case 6.2: fsubst0_c *)
+ IHC; Clear H2; IHC; EApply ty0_appl; XEAuto.
+(* case 6.3: fsubst0_b *)
+ Subst0GenBase; Rewrite H3; Clear H3 c1 c2 t t1 t2 t3.
+(* case 6.3.1: subst0 on left argument *)
+ IHC; Ty0Correct; Ty0GenBase; Clear H2; IHC; IHCT.
+ EApply ty0_conv;
+ [ EApply ty0_appl | EApply ty0_appl
+ | EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]; XEAuto.
+(* case 6.3.2: subst0 on right argument *)
+ IHCT; Clear H2; IHC; EApply ty0_appl; XEAuto.
+(* case 6.3.3: subst0 on both arguments *)
+ IHC; Ty0Correct; Ty0GenBase; IHCT; Clear H2; IHC; Ty0Correct; IHCT.
+ EApply ty0_conv;
+ [ EApply ty0_appl | EApply ty0_appl
+ | EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]; XEAuto.
+(* case 7: ty0_cast *)
+ Clear c1 t t1; Intros until 5; XElim H3; Intros; Clear c2 t3.
+(* case 7.1: fsubst0_t *)
+ Subst0GenBase; Rewrite H3; Clear H3 t4.
+(* case 7.1.1: subst0 on left argument *)
+ IHT; EApply ty0_conv;
+ [ Idtac
+ | EApply ty0_cast;
+ [ EApply ty0_conv; [ Idtac | Idtac | Apply pc3_s; EApply pc3_fsubst0 ]
+ | Idtac ]
+ | EApply pc3_fsubst0 ]; XEAuto.
+(* case 7.1.2: subst0 on right argument *)
+ IHT; EApply ty0_cast; XEAuto.
+(* case 7.1.3: subst0 on both arguments *)
+ IHT; Clear H2; IHT.
+ EApply ty0_conv;
+ [ Idtac
+ | EApply ty0_cast;
+ [ EApply ty0_conv; [ Idtac | Idtac | Apply pc3_s; EApply pc3_fsubst0 ]
+ | Idtac ]
+ | EApply pc3_fsubst0 ]; XEAuto.
+(* case 7.2: fsubst0_c *)
+ IHC; Clear H2; IHC; EApply ty0_cast; XEAuto.
+(* case 6.3: fsubst0_b *)
+ Subst0GenBase; Rewrite H3; Clear H3 t4.
+(* case 7.3.1: subst0 on left argument *)
+ IHC; IHCT; Clear H2; IHC.
+ EApply ty0_conv;
+ [ Idtac
+ | EApply ty0_cast;
+ [ EApply ty0_conv; [ Idtac | Idtac | Apply pc3_s; EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]
+ | Idtac ]
+ | EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]; XEAuto.
+(* case 7.3.2: subst0 on right argument *)
+ IHCT; IHC; EApply ty0_cast; XEAuto.
+(* case 7.3.3: subst0 on both arguments *)
+ IHC; IHCT; Clear H2; IHCT.
+ EApply ty0_conv;
+ [ Idtac
+ | EApply ty0_cast;
+ [ EApply ty0_conv; [ Idtac | Idtac | Apply pc3_s; EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]
+ | Idtac ]
+ | EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]; XEAuto.
+ Qed.
+
+ Theorem ty0_csubst0: (g:?; c1:?; t1,t2:?) (ty0 g c1 t1 t2) ->
+ (e:?; u:?; i:?) (drop i (0) c1 (CTail e (Bind Abbr) u)) ->
+ (c2:?) (wf0 g c2) -> (csubst0 i u c1 c2) ->
+ (ty0 g c2 t1 t2).
+ Intros; EApply ty0_fsubst0; XEAuto.
+ Qed.
+
+ Theorem ty0_subst0: (g:?; c:?; t1,t:?) (ty0 g c t1 t) ->
+ (e:?; u:?; i:?) (drop i (0) c (CTail e (Bind Abbr) u)) ->
+ (t2:?) (subst0 i u t1 t2) -> (ty0 g c t2 t).
+ Intros; EApply ty0_fsubst0; XEAuto.
+ Qed.
+
+ End ty0_fsubst0.
+
+ Hints Resolve ty0_subst0 : ltlc.
+
projects / helm.git / blobdiff