From: Ferruccio Guidi Date: Fri, 15 Jul 2005 18:18:13 +0000 (+0000) Subject: some reorganization and some corrections X-Git-Tag: pre_notation~3 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1ea21db6644417e6cd3c44c84915712a5321a37a;p=helm.git some reorganization and some corrections --- diff --git a/helm/coq-contribs/LAMBDA-TYPES/cpr0_props.v b/helm/coq-contribs/LAMBDA-TYPES/cpr0_props.v deleted file mode 100644 index 1050288ee..000000000 --- a/helm/coq-contribs/LAMBDA-TYPES/cpr0_props.v +++ /dev/null @@ -1,103 +0,0 @@ -(*#* #stop file *) - -Require pr0_subst0. -Require pr3_defs. -Require pr3_props. -Require cpr0_defs. - - Section cpr0_drop. (******************************************************) - - Theorem cpr0_drop : (c1,c2:?) (cpr0 c1 c2) -> (h:?; e1:?; u1:?; k:?) - (drop h (0) c1 (CTail e1 k u1)) -> - (EX e2 u2 | (drop h (0) c2 (CTail e2 k u2)) & - (cpr0 e1 e2) & (pr0 u1 u2) - ). - Intros until 1; XElim H. -(* case 1 : cpr0_refl *) - XEAuto. -(* case 2 : cpr0_cont *) - XElim h. -(* case 2.1 : h = 0 *) - Intros; DropGenBase. - Inversion H2; Rewrite H6 in H1; Rewrite H4 in H; XEAuto. -(* case 2.2 : h > 0 *) - XElim k; Intros; DropGenBase. -(* case 2.2.1 : Bind *) - LApply (H0 n e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ]. - XElim H0; XEAuto. -(* case 2.2.2 : Flat *) - LApply (H0 (S n) e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ]. - XElim H0; XEAuto. - Qed. - - Theorem cpr0_drop_back : (c1,c2:?) (cpr0 c2 c1) -> (h:?; e1:?; u1:?; k:?) - (drop h (0) c1 (CTail e1 k u1)) -> - (EX e2 u2 | (drop h (0) c2 (CTail e2 k u2)) & - (cpr0 e2 e1) & (pr0 u2 u1) - ). - Intros until 1; XElim H. -(* case 1 : cpr0_refl *) - XEAuto. -(* case 2 : cpr0_cont *) - XElim h. -(* case 2.1 : h = 0 *) - Intros; DropGenBase. - Inversion H2; Rewrite H6 in H1; Rewrite H4 in H; XEAuto. -(* case 2.2 : h > 0 *) - XElim k; Intros; DropGenBase. -(* case 2.2.1 : Bind *) - LApply (H0 n e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ]. - XElim H0; XEAuto. -(* case 2.2.2 : Flat *) - LApply (H0 (S n) e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ]. - XElim H0; XEAuto. - Qed. - - End cpr0_drop. - - Tactic Definition Cpr0Drop := - Match Context With - | [ _: (drop ?1 (0) ?2 (CTail ?3 ?4 ?5)); - _: (cpr0 ?2 ?6) |- ? ] -> - LApply (cpr0_drop ?2 ?6); [ Intros H_x | XAuto ]; - LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ]; - XElim H_x; Intros - | [ _: (drop ?1 (0) ?2 (CTail ?3 ?4 ?5)); - _: (cpr0 ?6 ?2) |- ? ] -> - LApply (cpr0_drop_back ?2 ?6); [ Intros H_x | XAuto ]; - LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ]; - XElim H_x; Intros - | [ _: (drop ?1 (0) (CTail ?2 ?7 ?8) (CTail ?3 ?4 ?5)); - _: (cpr0 ?2 ?6) |- ? ] -> - LApply (cpr0_drop (CTail ?2 ?7 ?8) (CTail ?6 ?7 ?8)); [ Intros H_x | XAuto ]; - LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ]; - XElim H_x; Intros - | [ _: (drop ?1 (0) (CTail ?2 ?7 ?8) (CTail ?3 ?4 ?5)); - _: (cpr0 ?6 ?2) |- ? ] -> - LApply (cpr0_drop_back (CTail ?2 ?7 ?8) (CTail ?6 ?7 ?8)); [ Intros H_x | XAuto ]; - LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ]; - XElim H_x; Intros. - - Section cpr0_pr3. (*******************************************************) - - Theorem cpr0_pr3_t : (c1,c2:?) (cpr0 c2 c1) -> (t1,t2:?) (pr3 c1 t1 t2) -> - (pr3 c2 t1 t2). - Intros until 1; XElim H; Intros. -(* case 1 : cpr0_refl *) - XAuto. -(* case 2 : cpr0_cont *) - Pr3Context. - XElim H1; Intros. -(* case 2.1 : pr3_r *) - XAuto. -(* case 2.2 : pr3_u *) - EApply pr3_t; [ Idtac | XEAuto ]. Clear H2 H3 c1 c2 t1 t2 t4 u2. - Inversion_clear H1. -(* case 2.2.1 : pr2_pr0 *) - XAuto. -(* case 2.2.1 : pr2_delta *) - Cpr0Drop; Pr0Subst0. - EApply pr3_u; [ EApply pr2_delta; XEAuto | XAuto ]. - Qed. - - End cpr0_pr3. diff --git a/helm/coq-contribs/LAMBDA-TYPES/fsubst0_defs.v b/helm/coq-contribs/LAMBDA-TYPES/fsubst0_defs.v new file mode 100644 index 000000000..c7382bf20 --- /dev/null +++ b/helm/coq-contribs/LAMBDA-TYPES/fsubst0_defs.v @@ -0,0 +1,20 @@ +Require Export subst0_defs. +Require Export csubst0_defs. + +(*#* #caption "axioms for strict substitution in focalized terms", + "substituted term part", + "substituted context part", + "substituted both parts" +*) +(*#* #cap #cap c1, c2, t1, t2 #alpha v in W *) + + Inductive fsubst0 [i:nat; v:T; c1:C; t1:T] : C -> T -> Prop := + | fsubst0_snd : (t2:?) (subst0 i v t1 t2) -> (fsubst0 i v c1 t1 c1 t2) + | fsubst0_fst : (c2:?) (csubst0 i v c1 c2) -> (fsubst0 i v c1 t1 c2 t1) + | fsubst0_both : (t2:?) (subst0 i v t1 t2) -> + (c2:?) (csubst0 i v c1 c2) -> (fsubst0 i v c1 t1 c2 t2). + +(*#* #stop file *) + + Hint fsubst0 : ltlc := Constructors fsubst0. + diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr3_props.v b/helm/coq-contribs/LAMBDA-TYPES/pr3_props.v index 106bfe66c..b5c7df937 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/pr3_props.v +++ b/helm/coq-contribs/LAMBDA-TYPES/pr3_props.v @@ -1,73 +1,70 @@ Require subst0_subst0. Require pr0_subst0. +Require cpr0_defs. Require pr2_lift. +Require pr2_gen. Require pr3_defs. -(*#* #caption "main properties of predicate \\texttt{pr3}" *) +(*#* #caption "main properties of the relation $\\PrT{}{}{}$" *) (*#* #clauses *) (*#* #stop file *) Section pr3_context. (****************************************************) - Theorem pr3_pr0_pr2_t : (u1,u2:?) (pr0 u1 u2) -> - (c:?; t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) -> - (pr3 (CTail c k u1) t1 t2). - Intros. - Inversion H0; Clear H0; XAuto. + Theorem pr3_pr0_pr2_t: (u1,u2:?) (pr0 u1 u2) -> + (c:?; t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) -> + (pr3 (CTail c k u1) t1 t2). + Intros; Inversion H0; Clear H0; XAuto. NewInduction i. -(* case 1 : pr2_delta i = 0 *) - DropGenBase; Inversion H0; Clear H0 H3 H4 c k. - Rewrite H5 in H; Clear H5 u2. +(* case 1 : pr2_delta i = 0 *) + DropGenBase; Inversion H0; Clear H0 H4 H5 H6 c k t. + Rewrite H7 in H; Clear H7 u2. Pr0Subst0; XEAuto. (* case 2 : pr2_delta i > 0 *) NewInduction k; DropGenBase; XEAuto. Qed. - Theorem pr3_pr2_pr2_t : (c:?; u1,u2:?) (pr2 c u1 u2) -> - (t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) -> - (pr3 (CTail c k u1) t1 t2). + Theorem pr3_pr2_pr2_t: (c:?; u1,u2:?) (pr2 c u1 u2) -> + (t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) -> + (pr3 (CTail c k u1) t1 t2). Intros until 1; Inversion H; Clear H; Intros. -(* case 1 : pr2_pr0 *) +(* case 1 : pr2_free *) EApply pr3_pr0_pr2_t; [ Apply H0 | XAuto ]. (* case 2 : pr2_delta *) - Inversion H; [ XAuto | NewInduction i0 ]. + Inversion H; [ XAuto | NewInduction i0 ]. (* case 2.1 : i0 = 0 *) - DropGenBase; Inversion H2; Clear H2. - Rewrite <- H5; Rewrite H6 in H; Rewrite <- H7 in H3; Clear H5 H6 H7 d0 k u0. - Subst0Subst0; Arith9'In H4 i. (*; XDEAuto 7. + 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. + Subst0Subst0; Arith9'In H4 i; Clear H2 H H6 u2. + Pr0Subst0; Apply pr3_sing with t2:=x0; XEAuto. (* case 2.2 : i0 > 0 *) Clear IHi0; NewInduction k; DropGenBase; XEAuto. Qed. - Theorem pr3_pr2_pr3_t : (c:?; u2,t1,t2:?; k:?) - (pr3 (CTail c k u2) t1 t2) -> - (u1:?) (pr2 c u1 u2) -> - (pr3 (CTail c k u1) t1 t2). + Theorem pr3_pr2_pr3_t: (c:?; u2,t1,t2:?; k:?) + (pr3 (CTail c k u2) t1 t2) -> + (u1:?) (pr2 c u1 u2) -> + (pr3 (CTail c k u1) t1 t2). Intros until 1; XElim H; Intros. -(* case 1 : pr3_r *) +(* case 1 : pr3_refl *) XAuto. -(* case 2 : pr3_u *) +(* case 2 : pr3_sing *) EApply pr3_t. EApply pr3_pr2_pr2_t; [ Apply H2 | Apply H ]. XAuto. Qed. -(*#* #start file *) - (*#* #caption "reduction inside context items" *) (*#* #cap #cap t1, t2 #alpha c in E, u1 in V1, u2 in V2, k in z *) - Theorem pr3_pr3_pr3_t : (c:?; u1,u2:?) (pr3 c u1 u2) -> - (t1,t2:?; k:?) (pr3 (CTail c k u2) t1 t2) -> - (pr3 (CTail c k u1) t1 t2). - -(*#* #stop file *) - + Theorem pr3_pr3_pr3_t: (c:?; u1,u2:?) (pr3 c u1 u2) -> + (t1,t2:?; k:?) (pr3 (CTail c k u2) t1 t2) -> + (pr3 (CTail c k u1) t1 t2). Intros until 1; XElim H; Intros. -(* case 1 : pr3_r *) +(* case 1 : pr3_refl *) XAuto. -(* case 2 : pr3_u *) +(* case 2 : pr3_sing *) EApply pr3_pr2_pr3_t; [ Apply H1; XAuto | XAuto ]. Qed. @@ -76,34 +73,29 @@ Require pr3_defs. Tactic Definition Pr3Context := Match Context With | [ H1: (pr0 ?2 ?3); H2: (pr2 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] -> - LApply (pr3_pr0_pr2_t ?2 ?3); [ Clear H1; Intros H1 | XAuto ]; - LApply (H1 ?1 ?5 ?6 ?4); [ Clear H1 H2; Intros | XAuto ] + LApply (pr3_pr0_pr2_t ?2 ?3); [ Intros H_x | XAuto ]; + LApply (H_x ?1 ?5 ?6 ?4); [ Clear H_x H2; Intros | XAuto ] | [ H1: (pr0 ?2 ?3); H2: (pr3 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] -> LApply (pr3_pr2_pr3_t ?1 ?3 ?5 ?6 ?4); [ Clear H2; Intros H2 | XAuto ]; - LApply (H2 ?2); [ Clear H1 H2; Intros | XAuto ] + LApply (H2 ?2); [ Clear H2; Intros | XAuto ] | [ H1: (pr2 ?1 ?2 ?3); H2: (pr2 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] -> - LApply (pr3_pr2_pr2_t ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ]; - LApply (H1 ?5 ?6 ?4); [ Clear H1 H2; Intros | XAuto ] + LApply (pr3_pr2_pr2_t ?1 ?2 ?3); [ Intros H_x | XAuto ]; + LApply (H_x ?5 ?6 ?4); [ Clear H_x H2; Intros | XAuto ] | [ H1: (pr2 ?1 ?2 ?3); H2: (pr3 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] -> LApply (pr3_pr2_pr3_t ?1 ?3 ?5 ?6 ?4); [ Clear H2; Intros H2 | XAuto ]; - LApply (H2 ?2); [ Clear H1 H2; Intros | XAuto ] + LApply (H2 ?2); [ Clear H2; Intros | XAuto ] | [ H1: (pr3 ?1 ?2 ?3); H2: (pr3 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] -> - LApply (pr3_pr3_pr3_t ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ]; - LApply (H1 ?5 ?6 ?4); [ Clear H1 H2; Intros | XAuto ]. + LApply (pr3_pr3_pr3_t ?1 ?2 ?3); [ Intros H_x | XAuto ]; + LApply (H_x ?5 ?6 ?4); [ Clear H_x H2; Intros | XAuto ]. Section pr3_lift. (*******************************************************) -(*#* #start file *) - (*#* #caption "conguence with lift" *) (*#* #cap #cap c, t1, t2 #alpha e in D, d in i *) - Theorem pr3_lift : (c,e:?; h,d:?) (drop h d c e) -> - (t1,t2:?) (pr3 e t1 t2) -> - (pr3 c (lift h d t1) (lift h d t2)). - -(*#* #stop file *) - + Theorem pr3_lift: (c,e:?; h,d:?) (drop h d c e) -> + (t1,t2:?) (pr3 e t1 t2) -> + (pr3 c (lift h d t1) (lift h d t2)). Intros until 2; XElim H0; Intros; XEAuto. Qed. @@ -111,4 +103,25 @@ Require pr3_defs. Hints Resolve pr3_lift : ltlc. -*) + Section pr3_cpr0. (*******************************************************) + + Theorem pr3_cpr0_t: (c1,c2:?) (cpr0 c2 c1) -> (t1,t2:?) (pr3 c1 t1 t2) -> + (pr3 c2 t1 t2). + Intros until 1; XElim H; Intros. +(* case 1 : cpr0_refl *) + XAuto. +(* case 2 : cpr0_comp *) + Pr3Context; Clear H1. + XElim H2; Intros. +(* case 2.1 : pr3_refl *) + XAuto. +(* case 2.2 : pr3_sing *) + EApply pr3_t; [ Idtac | XEAuto ]. Clear H2 H3 c1 c2 t1 t2 t4 u2. + Inversion_clear H1. +(* case 2.2.1 : pr2_free *) + XAuto. +(* case 2.2.1 : pr2_delta *) + Cpr0Drop; Pr0Subst0; Apply pr3_sing with t2:=x; XEAuto. + Qed. + + End pr3_cpr0.