+++ /dev/null
-Require drop_props.
-Require csubst0_defs.
-Require fsubst0_defs.
-Require pc3_props.
-Require pc3_subst0.
-Require ty0_defs.
-Require ty0_gen.
-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_snd *)
- IHT; EApply ty0_conv; XEAuto.
-(* case 1.2: fsubst0_fst *)
- IHC; EApply ty0_conv; Try EApply pc3_fsubst0; XEAuto.
-(* case 1.3: fsubst0_both *)
- IHCT; IHCT; EApply ty0_conv; Try EApply pc3_fsubst0; XEAuto.
-(* case 2: ty0_sort *)
- Intros until 2; XElim H0; Intros.
-(* case 2.1: fsubst0_snd *)
- Subst0GenBase.
-(* case 2.2: fsubst0_fst *)
- XAuto.
-(* case 2.3: fsubst0_both *)
- Subst0GenBase.
-(* case 3: ty0_abbr *)
- Intros until 5; XElim H3; Intros; Clear c1 c2 t t1 t2.
-(* case 3.1: fsubst0_snd *)
- 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_fst *)
- 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_snd *)
- 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_fst *)
- 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_both *)
- 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_snd *)
- Subst0GenBase; Rewrite H3 in H0; DropDis; Inversion H0.
-(* case 4.2: fsubst0_fst *)
- 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_snd *)
- 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_fst *)
- 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_both *)
- Subst0GenBase; Rewrite H3 in H0; DropDis; Inversion H0.
-(* case 5: ty0_bind *)
- Intros until 7; XElim H5; Intros; Clear H4.
-(* case 5.1: fsubst0_snd *)
- 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_fst *)
- IHC; IHCb; Ty0Correct; EApply ty0_bind; XEAuto.
-(* case 5.3: fsubst0_both *)
- 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_snd *)
- 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_fst *)
- IHC; Clear H2; IHC; EApply ty0_appl; XEAuto.
-(* case 6.3: fsubst0_both *)
- 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_snd *)
- 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_fst *)
- IHC; Clear H2; IHC; EApply ty0_cast; XEAuto.
-(* case 6.3: fsubst0_both *)
- 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