X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fpc3_props.v;h=28aa031507847ed705a456f7f2549eb78c52fc78;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=6f48a27fee4470734972e50424f33fe97a13528e;hpb=a8052b7482d5573eca2776ea11cb7a4b06236fbd;p=helm.git diff --git a/helm/coq-contribs/LAMBDA-TYPES/pc3_props.v b/helm/coq-contribs/LAMBDA-TYPES/pc3_props.v index 6f48a27fe..28aa03150 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/pc3_props.v +++ b/helm/coq-contribs/LAMBDA-TYPES/pc3_props.v @@ -8,25 +8,47 @@ Require pr3_props. Require pr3_confluence. Require pc3_defs. - Section pc3_confluence. (*************************************************) + Section pc3_trans. (******************************************************) - Theorem pc3_confluence: (c:?; t1,t2:?) (pc3 c t1 t2) -> - (EX t0 | (pr3 c t1 t0) & (pr3 c t2 t0)). - Intros; XElim H; Intros. -(* case 1: pc3_r *) - XEAuto. -(* case 2: pc3_u *) - Clear H0; XElim H1; Intros. - Inversion_clear H; [ XEAuto | Pr3Confluence; XEAuto ]. + Theorem pc3_t: (t2,c,t1:?) (pc3 c t1 t2) -> + (t3:?) (pc3 c t2 t3) -> (pc3 c t1 t3). + Intros; Repeat Pc3Unfold; Pr3Confluence; XEAuto. Qed. - End pc3_confluence. + Theorem pc3_pr2_u2: (c:?; t0,t1:?) (pr2 c t0 t1) -> + (t2:?) (pc3 c t0 t2) -> (pc3 c t1 t2). + Intros; Apply (pc3_t t0); XAuto. + Qed. + + Theorem pc3_tail_12: (c:?; u1,u2:?) (pc3 c u1 u2) -> + (k:?; t1,t2:?) (pc3 (CTail c k u2) t1 t2) -> + (pc3 c (TTail k u1 t1) (TTail k u2 t2)). + Intros. + EApply pc3_t; [ Apply pc3_tail_1 | Apply pc3_tail_2 ]; XAuto. + Qed. + + Theorem pc3_tail_21: (c:?; u1,u2:?) (pc3 c u1 u2) -> + (k:?; t1,t2:?) (pc3 (CTail c k u1) t1 t2) -> + (pc3 c (TTail k u1 t1) (TTail k u2 t2)). + Intros. + EApply pc3_t; [ Apply pc3_tail_2 | Apply pc3_tail_1 ]; XAuto. + Qed. + + End pc3_trans. + + Hints Resolve pc3_t pc3_tail_12 pc3_tail_21 : ltlc. - Tactic Definition Pc3Confluence := + Tactic Definition Pc3T := Match Context With - [ H: (pc3 ?1 ?2 ?3) |- ? ] -> - LApply (pc3_confluence ?1 ?2 ?3); [ Clear H; Intros H | XAuto ]; - XElim H; Intros. + | [ _: (pr3 ?1 ?2 (TTail ?3 ?4 ?5)); _: (pc3 ?1 ?6 ?4) |- ? ] -> + LApply (pc3_t (TTail ?3 ?4 ?5) ?1 ?2); [ Intros H_x | XAuto ]; + LApply (H_x (TTail ?3 ?6 ?5)); [ Clear H_x; Intros | Apply pc3_s; XAuto ] + | [ _: (pc3 ?1 ?2 ?3); _: (pr3 ?1 ?3 ?4) |- ? ] -> + LApply (pc3_t ?3 ?1 ?2); [ Intros H_x | XAuto ]; + LApply (H_x ?4); [ Clear H_x; Intros | XAuto ] + | [ _: (pc3 ?1 ?2 ?3); _: (pc3 ?1 ?4 ?3) |- ? ] -> + LApply (pc3_t ?3 ?1 ?2); [ Intros H_x | XAuto ]; + LApply (H_x ?4); [ Clear H_x; Intros | XAuto ]. Section pc3_context. (****************************************************) @@ -55,7 +77,7 @@ Require pc3_defs. DropGenBase; Inversion H4; Clear H3 H4 H7 t t4. Rewrite <- H9; Rewrite H10 in H; Rewrite <- H11 in H6; Clear H9 H10 H11 d0 k u0. Pr0Subst0; Subst0Subst0; Arith9'In H6 i. - EApply pc3_pr3_u. + EApply pc3_pr2_u. EApply pr2_delta; XEAuto. Apply pc3_pr2_x; EApply pr2_delta; [ Idtac | XEAuto | XEAuto ]; XEAuto. (* case 2.2: i0 > 0 *) @@ -82,7 +104,7 @@ Require pc3_defs. (* case 1: pr3_refl *) XAuto. (* case 2: pr3_sing *) - Apply H1; Pc3Confluence. + Apply H1; Pc3Unfold. EApply pc3_t; [ Idtac | Apply pc3_s ]; EApply pc3_pr2_pr3_t; XEAuto. Qed. @@ -114,8 +136,8 @@ Require pc3_defs. (pc3 c (lift h d t1) (lift h d t2)). Intros. - Pc3Confluence. - EApply pc3_pr3_t; (EApply pr3_lift; [ XEAuto | Apply H0 Orelse Apply H1 ]). + Pc3Unfold. + EApply pc3_pr3_t; (EApply pr3_lift; [ XEAuto | Apply H1 Orelse Apply H2 ]). Qed. End pc3_lift. @@ -137,7 +159,7 @@ Require pc3_defs. XAuto. (* case 1.2.2: pr2_delta *) Cpr0Drop; Pr0Subst0. - EApply pc3_pr3_u; [ EApply pr2_delta; XEAuto | XAuto ]. + EApply pc3_pr2_u; [ EApply pr2_delta; XEAuto | XAuto ]. Qed. Theorem pc3_cpr0_t: (c1,c2:?) (cpr0 c1 c2) -> @@ -147,16 +169,65 @@ Require pc3_defs. (* case 1: cpr0_refl *) XAuto. (* case 2: cpr0_comp *) - Pc3Context; Pc3Confluence. + Pc3Context; Pc3Unfold. EApply pc3_t; [ Idtac | Apply pc3_s ]; EApply pc3_cpr0_t_aux; XEAuto. Qed. Theorem pc3_cpr0: (c1,c2:?) (cpr0 c1 c2) -> (t1,t2:?) (pc3 c1 t1 t2) -> (pc3 c2 t1 t2). - Intros; Pc3Confluence. + Intros; Pc3Unfold. EApply pc3_t; [ Idtac | Apply pc3_s ]; EApply pc3_cpr0_t; XEAuto. Qed. End pc3_cpr0. Hints Resolve pc3_cpr0 : ltlc. + + Section pc3_ind_left. (***************************************************) + + Inductive pc3_left [c:C] : T -> T -> Prop := + | pc3_left_r : (t:?) (pc3_left c t t) + | pc3_left_ur: (t1,t2:?) (pr2 c t1 t2) -> (t3:?) (pc3_left c t2 t3) -> + (pc3_left c t1 t3) + | pc3_left_ux: (t1,t2:?) (pr2 c t1 t2) -> (t3:?) (pc3_left c t1 t3) -> + (pc3_left c t2 t3). + + Hint pc3_left: ltlc := Constructors pc3_left. + + Remark pc3_left_pr3: (c:?; t1,t2:?) (pr3 c t1 t2) -> (pc3_left c t1 t2). + Intros; XElim H; XEAuto. + Qed. + + Remark pc3_left_trans: (c:?; t1,t2:?) (pc3_left c t1 t2) -> + (t3:?) (pc3_left c t2 t3) -> (pc3_left c t1 t3). + Intros until 1; XElim H; XEAuto. + Qed. + + Hints Resolve pc3_left_trans : ltlc. + + Remark pc3_left_sym: (c:?; t1,t2:?) (pc3_left c t1 t2) -> + (pc3_left c t2 t1). + Intros; XElim H; XEAuto. + Qed. + + Hints Resolve pc3_left_sym pc3_left_pr3 : ltlc. + + Remark pc3_left_pc3: (c:?; t1,t2:?) (pc3 c t1 t2) -> (pc3_left c t1 t2). + Intros; Pc3Unfold; XEAuto. + Qed. + + Remark pc3_pc3_left: (c:?; t1,t2:?) (pc3_left c t1 t2) -> (pc3 c t1 t2). + Intros; XElim H; XEAuto. + Qed. + + Hints Resolve pc3_left_pc3 pc3_pc3_left : ltlc. + + Theorem pc3_ind_left: (c:C; P:(T->T->Prop)) + ((t:T) (P t t)) -> + ((t1,t2:T) (pr2 c t1 t2) -> (t3:T) (pc3 c t2 t3) -> (P t2 t3) -> (P t1 t3)) -> + ((t1,t2:T) (pr2 c t1 t2) -> (t3:T) (pc3 c t1 t3) -> (P t1 t3) -> (P t2 t3)) -> + (t,t0:T) (pc3 c t t0) -> (P t t0). + Intros; ElimType (pc3_left c t t0); XEAuto. + Qed. + + End pc3_ind_left.