X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fpr3_gen.v;h=e96f49fc3f02f5f9201c5eb3c4056d64c8a6029f;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=855c4deab66d8a11fb0379c66289cd30415f5b85;hpb=1b21075e987872a2e3103203b4e67c939e4a9f6a;p=helm.git diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr3_gen.v b/helm/coq-contribs/LAMBDA-TYPES/pr3_gen.v index 855c4deab..e96f49fc3 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/pr3_gen.v +++ b/helm/coq-contribs/LAMBDA-TYPES/pr3_gen.v @@ -4,181 +4,129 @@ Require pr2_gen. Require pr3_defs. Require pr3_props. - Section pr3_gen_void. (***************************************************) + Section pr3_gen_lift. (***************************************************) + +(*#* #caption "generation lemma for lift" *) +(*#* #cap #cap c #alpha e in D, t1 in U1, t2 in U2, x in T, d in i *) + + Theorem pr3_gen_lift: (c:?; t1,x:?; h,d:?) (pr3 c (lift h d t1) x) -> + (e:?) (drop h d c e) -> + (EX t2 | x = (lift h d t2) & (pr3 e t1 t2)). + Intros until 1; InsertEq H '(lift h d t1); + UnIntro H t1; XElim H; Clear y x; Intros; Rename x into t4. +(* case 1 : pr3_refl *) + XEAuto. +(* case 2 : pr3_sing *) + Rewrite H2 in H; Pr2Gen. + LApply (H1 x); [ Clear H1; Intros H1 | XAuto ]. + LApply (H1 e); [ Clear H1; Intros H1 | XAuto ]. + XElim H1; XEAuto. + Qed. + + End pr3_gen_lift. + + Section pr3_gen_lref. (***************************************************) + + Theorem pr3_gen_lref: (c:?; x:?; n:?) (pr3 c (TLRef n) x) -> + x = (TLRef n) \/ + (EX d u v | (drop n (0) c (CTail d (Bind Abbr) u)) & + (pr3 d u v) & + x = (lift (S n) (0) v) + ). + Intros; InsertEq H '(TLRef n); XElim H; Clear y x; Intros. +(* case 1: pr3_refl *) + XAuto. +(* case 2: pr3_sing *) + Rewrite H2 in H; Clear H2 t1; Pr2GenBase. +(* case 2.1: pr2_free *) + XAuto. +(* case 2.2: pr2_delta *) + Rewrite H4 in H0; Clear H1 H4 t2. + LApply (pr3_gen_lift c x1 t3 (S n) (0)); [ Clear H0; Intros | XAuto ]. + LApply (H x0); [ Clear H; Intros | XEAuto ]. + XElim H; XEAuto. + Qed. + + End pr3_gen_lref. + + Section pr3_gen_bind. (***************************************************) Tactic Definition IH := Match Context With - [ H: (u,t:T) (TTail (Bind Void) ?1 ?2) = (TTail (Bind Void) u t) -> ? |- ? ] -> + | [ H: (u,t:T) (TTail (Bind Void) ?1 ?2) = (TTail (Bind Void) u t) -> ? |- ? ] -> LApply (H ?1 ?2); [ Clear H; Intros H | XAuto ]; - XElim H1; Intros H1; XElim H1; Intros. - - Theorem pr3_gen_void : (c:?; u1,t1,x:?) (pr3 c (TTail (Bind Void) u1 t1) x) -> - (EX u2 t2 | x = (TTail (Bind Void) u2 t2) & - (pr3 c u1 u2) & (b:?; u:?) - (pr3 (CTail c (Bind b) u) t1 t2) - ) \/ - (EX u | (pr3 c u1 u) & - (pr3 (CTail c (Bind Void) u) t1 (lift (1) (0) x)) - ). + XDecompose H + | [ H: (u,t:T) (TTail (Bind Abbr) ?1 ?2) = (TTail (Bind Abbr) u t) -> ? |- ? ] -> + LApply (H ?1 ?2); [ Clear H; Intros H | XAuto ]; + XDecompose H. + + Theorem pr3_gen_void: (c:?; u1,t1,x:?) (pr3 c (TTail (Bind Void) u1 t1) x) -> + (EX u2 t2 | x = (TTail (Bind Void) u2 t2) & + (pr3 c u1 u2) & (b:?; u:?) + (pr3 (CTail c (Bind b) u) t1 t2) + ) \/ + (pr3 (CTail c (Bind Void) u1) t1 (lift (1) (0) x)). Intros until 1; InsertEq H '(TTail (Bind Void) u1 t1); UnIntro t1 H; UnIntro u1 H; XElim H; Intros. -(* case 1 : pr3_r *) +(* case 1 : pr3_refl *) Rewrite H; XEAuto. -(* case 2 : pr3_u *) +(* case 2 : pr3_sing *) Rewrite H2 in H; Clear H2 t0; Pr2Gen. (* case 2.1 : short step: compatibility *) - Rewrite H in H0; Rewrite H in H1; Clear H t2; IH. -(* case 2.1.1 : long step: compatibility *) - Rewrite H; Rewrite H in H0; XEAuto. -(* case 2.1.2 : long step: zeta *) - XEAuto. + Rewrite H3 in H1; Clear H0 H3 t2. + IH; Try Pr3Context; Try Rewrite H2; XEAuto. (* case 2.2 : short step: zeta *) - Clear H1; Right. - EApply ex2_intro; [ XAuto | Idtac ]. - EApply pr3_u; [ Idtac | EApply pr3_lift ]. - XEAuto. XAuto. XAuto. + XEAuto. Qed. - End pr3_gen_void. - - Section pr3_gen_abbr. (***************************************************) - - Tactic Definition IH := - LApply (H1 x0 x1); [ Clear H1; Intros H1 | XAuto ]; - XElim H1; - [ Intros H1; XElim H1; - Do 4 Intro; Intros H_x; XElim H_x; - [ Intros | Intros H_x; XElim H_x; Intros ] - | Intros H1; XElim H1; Intros ]. - - Theorem pr3_gen_abbr : (c:?; u1,t1,x:?) (pr3 c (TTail (Bind Abbr) u1 t1) x) -> - (EX u2 t2 | x = (TTail (Bind Abbr) u2 t2) & - (pr3 c u1 u2) & - ((b:?; u:?) (pr3 (CTail c (Bind b) u) t1 t2)) \/ - (EX u3 t3 y | (pr3 c (TTail (Bind Abbr) u3 t3) x) & - (pr3 c u1 u3) & - (b:?; u:?) (pr3 (CTail c (Bind b) u) t1 y) & - (subst0 (0) u3 y t3) - ) - ) \/ - (EX u | (pr3 c u1 u) & - (pr3 (CTail c (Bind Abbr) u) t1 (lift (1) (0) x)) - ). + Theorem pr3_gen_abbr: (c:?; u1,t1,x:?) (pr3 c (TTail (Bind Abbr) u1 t1) x) -> + (EX u2 t2 | x = (TTail (Bind Abbr) u2 t2) & + (pr3 c u1 u2) & + (pr3 (CTail c (Bind Abbr) u1) t1 t2) + ) \/ + (pr3 (CTail c (Bind Abbr) u1) t1 (lift (1) (0) x)). Intros until 1; InsertEq H '(TTail (Bind Abbr) u1 t1); UnIntro H t1; UnIntro H u1; XElim H; Clear y x; Intros; Rename x into u1; Rename x0 into t4. -(* case 1 : pr3_r *) +(* case 1: pr3_refl *) Rewrite H; XEAuto. -(* case 2 : pr3_u *) +(* case 2: pr3_sing *) Rewrite H2 in H; Clear H2 t1; Pr2Gen. -(* case 2.1 : short step: compatibility *) - Rewrite H in H0; Rewrite H in H1; Clear H t2; IH. -(* case 2.1.1 : long step: compatibility *) - Rewrite H; Rewrite H in H0; Clear H t3. - Left; EApply ex3_2_intro; XEAuto. -(* case 2.1.2 : long step: delta *) - Rewrite H; Rewrite H in H0; Rewrite H in H4; Clear H t3. - Left; EApply ex3_2_intro; - [ XEAuto | XEAuto - | Right; EApply ex4_3_intro; - [ EApply pr3_t; [ XAuto | Apply H4 ] | XEAuto | Idtac | Apply H7 ] ]. +(* case 2.1: short step: compatibility *) + Rewrite H3 in H1; Clear H0 H3 t2. + IH; Repeat Pr3Context; + Try (Rewrite H0; Clear H0 t3; Left; EApply ex3_2_intro); XEAuto. -(* case 2.1.3 : long step: zeta *) +(* case 2.2: short step: beta *) + Rewrite H3 in H1; Clear H0 H3 t1. + IH; Repeat Pr3Context; + Try (Rewrite H0; Clear H0 t3; Left; EApply ex3_2_intro); XEAuto. -(* case 2.2 : short step: delta *) - Rewrite H in H0; Rewrite H in H1; Clear H t2; IH. -(* case 2.2.1 : long step: compatibility *) - Left; EApply ex3_2_intro; - [ XEAuto | XEAuto - | Right; EApply ex4_3_intro; [ Rewrite H | Idtac | Idtac | Apply H4 ] ]. - XAuto. XAuto. XAuto. -(* case 2.2.2 : long step: delta *) - Left; EApply ex3_2_intro; - [ XEAuto | XEAuto - | Right; EApply ex4_3_intro; - [ EApply pr3_t; [ Apply pr3_tail_12 | Apply H5 ] - | Idtac | Idtac | Apply H4 ] ]. - XAuto. EApply pr3_t; [ Apply H7 | XEAuto ]. XAuto. XAuto. -(* case 2.2.3 : long step: zeta *) - Right; Apply ex2_intro with x := x0; [ XAuto | Idtac ]. - Apply pr3_u with t2 := x; [ XAuto | Idtac ]. - Apply pr3_u with t2 := x1; [ XEAuto | Idtac ]. - Pr3Context; XAuto. -(* case 2.3 : short step: zeta *) - Clear H1; Right. - EApply ex2_intro; [ XAuto | Idtac ]. - EApply pr3_u; [ Idtac | EApply pr3_lift ]. - XEAuto. XAuto. XAuto. - Qed. - - End pr3_gen_abbr. - - Section pr3_gen_abst. (***************************************************) - - Theorem pr3_gen_abst : (c:?; u1,t1,x:?) - (pr3 c (TTail (Bind Abst) u1 t1) x) -> - (EX u2 t2 | x = (TTail (Bind Abst) u2 t2) & - (pr3 c u1 u2) & (b:?; u:?) - (pr3 (CTail c (Bind b) u) t1 t2) - ). - Intros until 1; InsertEq H '(TTail (Bind Abst) u1 t1); - UnIntro H t1; UnIntro H u1; XElim H; Clear y x; Intros; - Rename x into u1; Rename x0 into t4. -(* case 1 : pr3_r *) - Rewrite H; XEAuto. -(* case 2 : pr3_u *) - Rewrite H2 in H; Clear H2 t1. - Pr2GenBase. - LApply (H1 x0 x1); [ Clear H H1; Intros | XAuto ]. - XElim H; XEAuto. - Qed. - - End pr3_gen_abst. - - Section pr3_gen_lift. (***************************************************) - -(*#* #start file *) - -(*#* #caption "generation lemma for lift" *) -(*#* #cap #cap c #alpha e in D, t1 in U1, t2 in U2, x in T, d in i *) - - Theorem pr3_gen_lift : (c:?; t1,x:?; h,d:?) (pr3 c (lift h d t1) x) -> - (e:?) (drop h d c e) -> - (EX t2 | x = (lift h d t2) & (pr3 e t1 t2)). - -(*#* #stop file *) - - Intros until 1; InsertEq H '(lift h d t1); - UnIntro H t1; XElim H; Clear y x; Intros; Rename x into t4. -(* case 1 : pr3_r *) +(* case 2.3: short step: delta *) + Rewrite H3 in H1; Clear H0 H3 t2. + IH; Repeat Pr3Context; + Try (Rewrite H0; Clear H0 t3; Left; EApply ex3_2_intro); + XDEAuto 7. +(* case 2.4: short step: zeta *) XEAuto. -(* case 2 : pr3_u *) - Rewrite H2 in H; Pr2Gen. - LApply (H1 x); [ Clear H1; Intros H1 | XAuto ]. - LApply (H1 e); [ Clear H1; Intros H1 | XAuto ]. - XElim H1; XEAuto. Qed. - End pr3_gen_lift. + End pr3_gen_bind. Tactic Definition Pr3Gen := Match Context With - | [ H: (pr3 ?1 (TTail (Bind Abst) ?2 ?3) ?4) |- ? ] -> - LApply (pr3_gen_abst ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ]; - XElim H; Intros - | [ H: (pr3 ?1 (TTail (Bind Abbr) ?2 ?3) ?4) |- ? ] -> - LApply (pr3_gen_abbr ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ]; - XElim H; - [ Intros H; XElim H; - Do 4 Intro; Intros H_x; XElim H_x; - [ Intros | Intros H_x; XElim H_x; Intros ] - | Intros H; XElim H; Intros ] + | [ H: (pr3 ?1 (TLRef ?2) ?3) |- ? ] -> + LApply (pr3_gen_lref ?1 ?3 ?2); [ Clear H; Intros H | XAuto ]; + XDecompose H | [ H: (pr3 ?1 (TTail (Bind Void) ?2 ?3) ?4) |- ? ] -> LApply (pr3_gen_void ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ]; - XElim H; Intros H; XElim H; Intros + XDecompose H + | [ H: (pr3 ?1 (TTail (Bind Abbr) ?2 ?3) ?4) |- ? ] -> + LApply (pr3_gen_abbr ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ]; + XDecompose H | [ H0: (pr3 ?1 (lift ?2 ?3 ?4) ?5); H1: (drop ?2 ?3 ?1 ?6) |- ? ] -> LApply (pr3_gen_lift ?1 ?4 ?5 ?2 ?3); [ Clear H0; Intros H0 | XAuto ]; LApply (H0 ?6); [ Clear H0; Intros H0 | XAuto ]; - XElim H0; Intros - | _ -> Pr2Gen. + XDecompose H0 + | _ -> Pr3GenBase.