Require pr0_lift.
Require pr0_subst1.
Require cpr0_defs.
-Require cpr0_props.
+Require pc1_props.
Require pc3_props.
Require pc3_gen.
Require ty0_defs.
+Require ty0_gen.
Require ty0_lift.
Require ty0_props.
Require ty0_subst0.
Require ty0_gen_context.
Require csub0_defs.
+Require csub0_props.
(*#* #caption "subject reduction" #clauses *)
(*#* #caption "base case" *)
(*#* #cap #cap c1, c2 #alpha t1 in T, t2 in T1, t in T2 *)
- Theorem ty0_sred_cpr0_pr0 : (g:?; c1:?; t1,t:?) (ty0 g c1 t1 t) ->
- (c2:?) (wf0 g c2) -> (cpr0 c1 c2) ->
- (t2:?) (pr0 t1 t2) -> (ty0 g c2 t2 t).
+ Theorem ty0_sred_cpr0_pr0: (g:?; c1:?; t1,t:?) (ty0 g c1 t1 t) ->
+ (c2:?) (wf0 g c2) -> (cpr0 c1 c2) ->
+ (t2:?) (pr0 t1 t2) -> (ty0 g c2 t2 t).
(*#* #stop file *)
Intros until 1; XElim H; Intros.
-(* case 1 : ty0_conv *)
+(* case 1: ty0_conv *)
IH1c; IH0c; EApply ty0_conv; XEAuto.
-(* case 2 : ty0_sort *)
+(* case 2: ty0_sort *)
Inversion H2; XAuto.
-(* case 3 : ty0_abbr *)
+(* case 3: ty0_abbr *)
Inversion H5; Cpr0Drop; IH1c; XEAuto.
-(* case 4 : ty0_abst *)
+(* case 4: ty0_abst *)
Intros; Inversion H5; Cpr0Drop; IH0; IH1.
EApply ty0_conv;
[ EApply ty0_lift; [ Idtac | XAuto | XEAuto ]
| EApply ty0_abst
| EApply pc3_lift ]; XEAuto.
-(* case 5 : ty0_bind *)
+(* case 5: ty0_bind *)
Intros; Inversion H7; Clear H7.
-(* case 5.1 : pr0_refl *)
+(* case 5.1: pr0_refl *)
IH0c; IH0Bc; IH0Bc.
EApply ty0_bind; XEAuto.
-(* case 5.2 : pr0_cont *)
+(* case 5.2: pr0_cont *)
IH0; IH0B; Ty0Correct; IH3B; Ty0Correct.
EApply ty0_conv; [ EApply ty0_bind | EApply ty0_bind | Idtac ]; XEAuto.
-(* case 5.3 : pr0_delta *)
+(* case 5.3: pr0_delta *)
Rewrite <- H8 in H1; Rewrite <- H8 in H2;
Rewrite <- H8 in H3; Rewrite <- H8 in H4; Clear H8 b.
IH0; IH0B; Ty0Correct; IH3B; Ty0Correct.
EApply ty0_conv; [ EApply ty0_bind | EApply ty0_bind | Idtac ]; XEAuto.
-(* case 5.4 : pr0_zeta *)
+(* case 5.4: pr0_zeta *)
Rewrite <- H11 in H1; Rewrite <- H11 in H2; Clear H8 H9 H10 H11 b0 t2 t7 u0.
IH0; IH1BLc; Move H3 after H8; IH0Bc; Ty0Correct; Move H8 after H4; Clear H H0 H1 H3 H6 c c1 t t1;
NewInduction b.
-(* case 5.4.1 : Abbr *)
+(* case 5.4.1: Abbr *)
Ty0GenContext; Subst1Gen; LiftGen; Rewrite H in H1; Clear H x0.
EApply ty0_conv;
[ EApply ty0_bind; XEAuto | XEAuto
| EApply pc3_pr3_x;
EApply (pr3_t (TTail (Bind Abbr) u (lift (1) (0) x1))); XEAuto ].
-(* case 5.4.2 : Abst *)
+(* case 5.4.2: Abst *)
EqFalse.
-(* case 5.4.3 : Void *)
+(* case 5.4.3: Void *)
Ty0GenContext; Rewrite H0; Rewrite H0 in H2; Clear H0 t3.
LiftGen; Rewrite <- H in H1; Clear H x0.
EApply ty0_conv; [ EApply ty0_bind; XEAuto | XEAuto | XAuto ].
-(* case 6 : ty0_appl *)
+(* case 6: ty0_appl *)
Intros; Inversion H5; Clear H5.
-(* case 6.1 : pr0_refl *)
+(* case 6.1: pr0_refl *)
IH0c; IH0c; EApply ty0_appl; XEAuto.
-(* case 6.2 : pr0_cont *)
+(* case 6.2: pr0_cont *)
Clear H6 H7 H8 H9 c1 k t t1 t2 t3 u1.
IH0; Ty0Correct; Ty0GenBase; IH1c; IH0; IH1c.
EApply ty0_conv;
[ EApply ty0_appl; [ XEAuto | EApply ty0_bind; XEAuto ]
| EApply ty0_appl; XEAuto
| XEAuto ].
-(* case 6.3 : pr0_beta *)
+(* case 6.3: pr0_beta *)
Rewrite <- H7 in H1; Rewrite <- H7 in H2; Clear H6 H7 H9 c1 t t1 t2 v v1.
IH1T; IH0c; Ty0Correct; Ty0GenBase; IH0; IH1c.
Move H5 after H13; Ty0GenBase; Pc3Gen; Repeat CSub0Ty0.
| EApply ty0_bind
| Apply (pc3_t (TTail (Bind Abbr) v2 t0))
]; XEAuto.
-(* case 6.4 : pr0_delta *)
+(* case 6.4: pr0_delta *)
Rewrite <- H7 in H1; Rewrite <- H7 in H2; Clear H6 H7 H11 c1 t t1 t2 v v1.
IH1T2c; Clear H1; Ty0Correct; NonLinear; Ty0GenBase; IH1; IH0c.
Move H5 after H1; Ty0GenBase; Pc3Gen; Rewrite lift_bind in H0.
]; XEAuto
| Idtac ].
Rewrite <- lift_bind; Apply pc3_pc1;
- Apply (pc1_u (TTail (Flat Appl) v2 (TTail (Bind b) u2 (lift (1) (0) (TTail (Bind Abst) u t0))))); XAuto.
-(* case 7 : ty0_cast *)
+ Apply (pc1_pr0_u2 (TTail (Flat Appl) v2 (TTail (Bind b) u2 (lift (1) (0) (TTail (Bind Abst) u t0))))); XAuto.
+(* case 7: ty0_cast *)
Intros; Inversion H5; Clear H5.
-(* case 7.1 : pr0_refl *)
+(* case 7.1: pr0_refl *)
IH0c; IH0c; EApply ty0_cast; XEAuto.
-(* case 7.2 : pr0_cont *)
+(* case 7.2: pr0_cont *)
Clear H6 H7 H8 H9 c1 k u1 t t1 t4 t5.
IH0; IH1c; IH1c.
EApply ty0_conv;
[ XEAuto
| EApply ty0_cast; [ EApply ty0_conv; XEAuto | XEAuto ]
| XAuto ].
-(* case 7.3 : pr0_eps *)
+(* case 7.3: pr0_epsilon *)
XAuto.
Qed.
Section ty0_sred_pr3. (**********************************************)
- Theorem ty0_sred_pr1 : (c:?; t1,t2:?) (pr1 t1 t2) ->
- (g:?; t:?) (ty0 g c t1 t) ->
- (ty0 g c t2 t).
+ Theorem ty0_sred_pr1: (c:?; t1,t2:?) (pr1 t1 t2) ->
+ (g:?; t:?) (ty0 g c t1 t) ->
+ (ty0 g c t2 t).
Intros until 1; XElim H; Intros.
-(* case 1 : pr1_r *)
+(* case 1: pr1_r *)
XAuto.
-(* case 2 : pr1_u *)
+(* case 2: pr1_u *)
EApply H1; EApply ty0_sred_cpr0_pr0; XEAuto.
Qed.
- Theorem ty0_sred_pr2 : (c:?; t1,t2:?) (pr2 c t1 t2) ->
- (g:?; t:?) (ty0 g c t1 t) ->
- (ty0 g c t2 t).
+ Theorem ty0_sred_pr2: (c:?; t1,t2:?) (pr2 c t1 t2) ->
+ (g:?; t:?) (ty0 g c t1 t) ->
+ (ty0 g c t2 t).
Intros until 1; XElim H; Intros.
-(* case 1 : pr2_pr0 *)
+(* case 1: pr2_free *)
EApply ty0_sred_cpr0_pr0; XEAuto.
-(* case 2 : pr2_u *)
- XEAuto.
+(* case 2: pr2_u *)
+ EApply ty0_subst0; Try EApply ty0_sred_cpr0_pr0; XEAuto.
Qed.
(*#* #start file *)
-(*#* #caption "general case" *)
+(*#* #caption "general case without the reduction in the context" *)
(*#* #cap #cap c #alpha t1 in T, t2 in T1, t in T2 *)
- Theorem ty0_sred_pr3 : (c:?; t1,t2:?) (pr3 c t1 t2) ->
- (g:?; t:?) (ty0 g c t1 t) ->
- (ty0 g c t2 t).
+ Theorem ty0_sred_pr3: (c:?; t1,t2:?) (pr3 c t1 t2) ->
+ (g:?; t:?) (ty0 g c t1 t) ->
+ (ty0 g c t2 t).
(*#* #stop file *)
Intros until 1; XElim H; Intros.
-(* case 1 : pr3_r *)
+(* case 1: pr3_refl *)
XAuto.
-(* case 2 : pr3_u *)
+(* case 2: pr3_sing *)
EApply H1; EApply ty0_sred_pr2; XEAuto.
Qed.
projects / helm.git / blobdiff