X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fty0_sred.v;h=99548beb5220547332feb751a85908151a6c69e5;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=dc185a95a417e2f84cae70651509a3f5b60fa2c6;hpb=1b21075e987872a2e3103203b4e67c939e4a9f6a;p=helm.git

diff --git a/helm/coq-contribs/LAMBDA-TYPES/ty0_sred.v b/helm/coq-contribs/LAMBDA-TYPES/ty0_sred.v
index dc185a95a..99548beb5 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/ty0_sred.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/ty0_sred.v
@@ -4,15 +4,17 @@ Require csubst1_defs.
 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 *)
 
@@ -96,66 +98,66 @@ Require csub0_defs.
 (*#* #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.
@@ -164,7 +166,7 @@ Require csub0_defs.
       | 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.
@@ -179,19 +181,19 @@ Require csub0_defs.
         ]; 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.
 
@@ -199,41 +201,41 @@ Require csub0_defs.
 
    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.