X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fty0_sred_props.v;h=1606efc5c0e9fc217c6bb4c9b00175da44ee9a76;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=6fb7f17e102aed06dbb494924f997fcad46672ec;hpb=1b21075e987872a2e3103203b4e67c939e4a9f6a;p=helm.git diff --git a/helm/coq-contribs/LAMBDA-TYPES/ty0_sred_props.v b/helm/coq-contribs/LAMBDA-TYPES/ty0_sred_props.v index 6fb7f17e1..1606efc5c 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/ty0_sred_props.v +++ b/helm/coq-contribs/LAMBDA-TYPES/ty0_sred_props.v @@ -3,6 +3,7 @@ Require drop_props. Require pc3_props. Require pc3_gen. Require ty0_defs. +Require ty0_gen. Require ty0_props. Require ty0_sred. @@ -25,62 +26,62 @@ Require ty0_sred. (*#* #caption "generation lemma for lift" *) (*#* #cap #cap t2 #alpha c in C1, e in C2, t1 in T, x in T1, d in i *) - Theorem ty0_gen_lift : (g:?; c:?; t1,x:?; h,d:?) - (ty0 g c (lift h d t1) x) -> - (e:?) (wf0 g e) -> (drop h d c e) -> - (EX t2 | (pc3 c (lift h d t2) x) & (ty0 g e t1 t2)). + Theorem ty0_gen_lift: (g:?; c:?; t1,x:?; h,d:?) + (ty0 g c (lift h d t1) x) -> + (e:?) (wf0 g e) -> (drop h d c e) -> + (EX t2 | (pc3 c (lift h d t2) x) & (ty0 g e t1 t2)). (*#* #stop file *) Intros until 1; InsertEq H '(lift h d t1); UnIntro H d; UnIntro H t1; XElim H; Intros; Rename x0 into t3; Rename x1 into d0. -(* case 1 : ty0_conv *) +(* case 1: ty0_conv *) IH e; XEAuto. -(* case 2 : ty0_sort *) +(* case 2: ty0_sort *) LiftGenBase; Rewrite H0; Clear H0 t. EApply ex2_intro; [ Rewrite lift_sort; XAuto | XAuto ]. -(* case 3 : ty0_abbr *) +(* case 3: ty0_abbr *) Apply (lt_le_e n d0); Intros. -(* case 3.1 : n < d0 *) +(* case 3.1: n < d0 *) LiftGenBase; DropS; Rewrite H3; Clear H3 t3. Rewrite (le_plus_minus (S n) d0); [ Idtac | XAuto ]. Rewrite (lt_plus_minus n d0) in H5; [ DropDis; IH x1 | XAuto ]. EApply ex2_intro; [ Rewrite lift_d; [ EApply pc3_lift; XEAuto | XEAuto ] | EApply ty0_abbr; XEAuto ]. -(* case 3.2 : n >= d0 *) +(* case 3.2: n >= d0 *) Apply (lt_le_e n (plus d0 h)); Intros. -(* case 3.2.1 : n < d0 + h *) +(* case 3.2.1: n < d0 + h *) LiftGenBase. -(* case 3.2.2 : n >= d0 + h *) +(* case 3.2.2: n >= d0 + h *) Rewrite (le_plus_minus_sym h n) in H3; [ Idtac | XEAuto ]. LiftGenBase; DropDis; Rewrite H3; Clear H3 t3. EApply ex2_intro; [ Idtac | EApply ty0_abbr; XEAuto ]. Rewrite lift_free; [ Idtac | XEAuto | XAuto ]. Rewrite <- plus_n_Sm; Rewrite <- le_plus_minus; XEAuto. -(* case 4 : ty0_abst *) +(* case 4: ty0_abst *) Apply (lt_le_e n d0); Intros. -(* case 4.1 : n < d0 *) +(* case 4.1: n < d0 *) LiftGenBase; Rewrite H3; Clear H3 t3. Rewrite (le_plus_minus (S n) d0); [ Idtac | XAuto ]. Rewrite (lt_plus_minus n d0) in H5; [ DropDis; Rewrite H0; IH x1 | XAuto ]. EApply ex2_intro; [ Rewrite lift_d | EApply ty0_abst ]; XEAuto. -(* case 4.2 : n >= d0 *) +(* case 4.2: n >= d0 *) Apply (lt_le_e n (plus d0 h)); Intros. -(* case 4.2.1 : n < d0 + h *) +(* case 4.2.1: n < d0 + h *) LiftGenBase. -(* case 4.2.2 : n >= d0 + h *) +(* case 4.2.2: n >= d0 + h *) Rewrite (le_plus_minus_sym h n) in H3; [ Idtac | XEAuto ]. LiftGenBase; DropDis; Rewrite H3; Clear H3 t3. EApply ex2_intro; [ Idtac | EApply ty0_abst; XEAuto ]. Rewrite lift_free; [ Idtac | XEAuto | XAuto ]. Rewrite <- plus_n_Sm; Rewrite <- le_plus_minus; XEAuto. -(* case 5 : ty0_bind *) +(* case 5: ty0_bind *) LiftGenBase; Rewrite H5; Rewrite H8; Rewrite H8 in H2; Clear H5 t3. Move H0 after H2; IH e; IH '(CTail e (Bind b) x0); Ty0Correct. EApply ex2_intro; [ Rewrite lift_bind; XEAuto | XEAuto ]. -(* case 6 : ty0_appl *) +(* case 6: ty0_appl *) LiftGenBase; Rewrite H3; Rewrite H6; Clear H3 c t3 x y. IH e; IH e; Pc3Gen; Pc3T; Pc3Gen; Pc3T. Move H3 after H12; Ty0Correct; Ty0SRed; Ty0GenBase; Wf0Ty0. @@ -91,7 +92,7 @@ Require ty0_sred. [ EApply ty0_conv | EApply ty0_conv; [ EApply ty0_bind | Idtac | Idtac ] ] ]; XEAuto. -(* case 7 : ty0_cast *) +(* case 7: ty0_cast *) LiftGenBase; Rewrite H3; Rewrite H6; Rewrite H6 in H0. IH e; IH e; Pc3Gen; XEAuto. Qed. @@ -107,7 +108,7 @@ Require ty0_sred. LApply H0; [ Clear H0 H1; Intros H0 | XAuto ]; XElim H0; Intros | [ H0: (ty0 ?1 ?2 (lift ?3 ?4 ?5) ?6); - _ : (wf0 ?1 ?7) |- ? ] -> + _: (wf0 ?1 ?7) |- ? ] -> LApply (ty0_gen_lift ?1 ?2 ?5 ?6 ?3 ?4); [ Clear H0; Intros H0 | XAuto ]; LApply (H0 ?7); [ Clear H0; Intros H0 | XAuto ]; LApply H0; [ Clear H0; Intros H0 | XAuto ]; @@ -121,22 +122,22 @@ Require ty0_sred. (*#* #caption "drop preserves well-formedness" *) (*#* #cap #alpha c in C1, e in C2, d in i *) - Theorem wf0_drop : (c,e:?; d,h:?) (drop h d c e) -> - (g:?) (wf0 g c) -> (wf0 g e). + Theorem wf0_drop: (c,e:?; d,h:?) (drop h d c e) -> + (g:?) (wf0 g c) -> (wf0 g e). (*#* #stop proof *) XElim c. -(* case 1 : CSort *) +(* case 1: CSort *) Intros; DropGenBase; Rewrite H; XAuto. -(* case 2 : CTail k *) +(* case 2: CTail k *) Intros c IHc; XElim k; ( XElim d; [ XEAuto | Intros d IHd; Intros; DropGenBase; Rewrite H; Rewrite H1 in H0; Clear IHd H H1 e t; Inversion H0; Clear H3 H4 b0 u ]). -(* case 2.1 : Bind, d > 0 *) +(* case 2.1: Bind, d > 0 *) Ty0Gen; XEAuto. Qed. @@ -145,8 +146,8 @@ Require ty0_sred. (*#* #caption "type reduction" *) (*#* #cap #cap c, t1, t2 #alpha u in T *) - Theorem ty0_tred : (g:?; c:?; u,t1:?) (ty0 g c u t1) -> - (t2:?) (pr3 c t1 t2) -> (ty0 g c u t2). + Theorem ty0_tred: (g:?; c:?; u,t1:?) (ty0 g c u t1) -> + (t2:?) (pr3 c t1 t2) -> (ty0 g c u t2). (*#* #stop proof *) @@ -158,13 +159,13 @@ Require ty0_sred. (*#* #caption "subject conversion" *) (*#* #cap #cap c, u1, u2, t1, t2 *) - Theorem ty0_sconv : (g:?; c:?; u1,t1:?) (ty0 g c u1 t1) -> - (u2,t2:?) (ty0 g c u2 t2) -> - (pc3 c u1 u2) -> (pc3 c t1 t2). + Theorem ty0_sconv: (g:?; c:?; u1,t1:?) (ty0 g c u1 t1) -> + (u2,t2:?) (ty0 g c u2 t2) -> + (pc3 c u1 u2) -> (pc3 c t1 t2). (*#* #stop file *) - Intros; Pc3Confluence; Repeat Ty0SRed; XEAuto. + Intros; Pc3Unfold; Repeat Ty0SRed; XEAuto. Qed.