X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Funfold%2Ftpss.ma;h=16a0d3e4d9fb9a39e6b673c6e3704040a9cc3029;hb=16bbb2d6b16d5647d944f18f0fd6d4dd3df431fe;hp=98a8caa509a45a343446a54f623385c771845d61;hpb=7aa41e02e64bd09df253cc4267a44b4f49b16e03;p=helm.git diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss.ma index 98a8caa50..16a0d3e4d 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss.ma @@ -25,41 +25,41 @@ interpretation "partial unfold (term)" (* Basic eliminators ********************************************************) lemma tpss_ind: ∀d,e,L,T1. ∀R:predicate term. R T1 → - (∀T,T2. L ⊢ T1 [d, e] ≫* T → L ⊢ T [d, e] ≫ T2 → R T → R T2) → - ∀T2. L ⊢ T1 [d, e] ≫* T2 → R T2. + (∀T,T2. L ⊢ T1 [d, e] ▶* T → L ⊢ T [d, e] ▶ T2 → R T → R T2) → + ∀T2. L ⊢ T1 [d, e] ▶* T2 → R T2. #d #e #L #T1 #R #HT1 #IHT1 #T2 #HT12 @(TC_star_ind … HT1 IHT1 … HT12) // qed-. (* Basic properties *********************************************************) lemma tpss_strap: ∀L,T1,T,T2,d,e. - L ⊢ T1 [d, e] ≫ T → L ⊢ T [d, e] ≫* T2 → L ⊢ T1 [d, e] ≫* T2. + L ⊢ T1 [d, e] ▶ T → L ⊢ T [d, e] ▶* T2 → L ⊢ T1 [d, e] ▶* T2. /2 width=3/ qed. -lemma tpss_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≫* T2 → - ∀L2. L1 [d, e] ≼ L2 → L2 ⊢ T1 [d, e] ≫* T2. +lemma tpss_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ▶* T2 → + ∀L2. L1 [d, e] ≼ L2 → L2 ⊢ T1 [d, e] ▶* T2. /3 width=3/ qed. -lemma tpss_refl: ∀d,e,L,T. L ⊢ T [d, e] ≫* T. +lemma tpss_refl: ∀d,e,L,T. L ⊢ T [d, e] ▶* T. /2 width=1/ qed. -lemma tpss_bind: ∀L,V1,V2,d,e. L ⊢ V1 [d, e] ≫* V2 → - ∀I,T1,T2. L. 𝕓{I} V2 ⊢ T1 [d + 1, e] ≫* T2 → - L ⊢ 𝕓{I} V1. T1 [d, e] ≫* 𝕓{I} V2. T2. +lemma tpss_bind: ∀L,V1,V2,d,e. L ⊢ V1 [d, e] ▶* V2 → + ∀I,T1,T2. L. ⓑ{I} V2 ⊢ T1 [d + 1, e] ▶* T2 → + L ⊢ ⓑ{I} V1. T1 [d, e] ▶* ⓑ{I} V2. T2. #L #V1 #V2 #d #e #HV12 elim HV12 -V2 [ #V2 #HV12 #I #T1 #T2 #HT12 elim HT12 -T2 [ /3 width=5/ | #T #T2 #_ #HT2 #IHT @step /2 width=5/ (**) (* /3 width=5/ is too slow *) ] | #V #V2 #_ #HV12 #IHV #I #T1 #T2 #HT12 - lapply (tpss_lsubs_conf … HT12 (L. 𝕓{I} V) ?) -HT12 /2 width=1/ #HT12 + lapply (tpss_lsubs_conf … HT12 (L. ⓑ{I} V) ?) -HT12 /2 width=1/ #HT12 lapply (IHV … HT12) -IHV -HT12 #HT12 @step /2 width=5/ (**) (* /3 width=5/ is too slow *) ] qed. lemma tpss_flat: ∀L,I,V1,V2,T1,T2,d,e. - L ⊢ V1 [d, e] ≫ * V2 → L ⊢ T1 [d, e] ≫* T2 → - L ⊢ 𝕗{I} V1. T1 [d, e] ≫* 𝕗{I} V2. T2. + L ⊢ V1 [d, e] ▶ * V2 → L ⊢ T1 [d, e] ▶* T2 → + L ⊢ ⓕ{I} V1. T1 [d, e] ▶* ⓕ{I} V2. T2. #L #I #V1 #V2 #T1 #T2 #d #e #HV12 elim HV12 -V2 [ #V2 #HV12 #HT12 elim HT12 -T2 [ /3 width=1/ @@ -70,9 +70,9 @@ lemma tpss_flat: ∀L,I,V1,V2,T1,T2,d,e. ] qed. -lemma tpss_weak: ∀L,T1,T2,d1,e1. L ⊢ T1 [d1, e1] ≫* T2 → +lemma tpss_weak: ∀L,T1,T2,d1,e1. L ⊢ T1 [d1, e1] ▶* T2 → ∀d2,e2. d2 ≤ d1 → d1 + e1 ≤ d2 + e2 → - L ⊢ T1 [d2, e2] ≫* T2. + L ⊢ T1 [d2, e2] ▶* T2. #L #T1 #T2 #d1 #e1 #H #d1 #d2 #Hd21 #Hde12 @(tpss_ind … H) -T2 [ // | #T #T2 #_ #HT12 #IHT @@ -81,7 +81,7 @@ lemma tpss_weak: ∀L,T1,T2,d1,e1. L ⊢ T1 [d1, e1] ≫* T2 → qed. lemma tpss_weak_top: ∀L,T1,T2,d,e. - L ⊢ T1 [d, e] ≫* T2 → L ⊢ T1 [d, |L| - d] ≫* T2. + L ⊢ T1 [d, e] ▶* T2 → L ⊢ T1 [d, |L| - d] ▶* T2. #L #T1 #T2 #d #e #H @(tpss_ind … H) -T2 [ // | #T #T2 #_ #HT12 #IHT @@ -90,7 +90,7 @@ lemma tpss_weak_top: ∀L,T1,T2,d,e. qed. lemma tpss_weak_all: ∀L,T1,T2,d,e. - L ⊢ T1 [d, e] ≫* T2 → L ⊢ T1 [0, |L|] ≫* T2. + L ⊢ T1 [d, e] ▶* T2 → L ⊢ T1 [0, |L|] ▶* T2. #L #T1 #T2 #d #e #HT12 lapply (tpss_weak … HT12 0 (d + e) ? ?) -HT12 // #HT12 lapply (tpss_weak_top … HT12) // @@ -99,7 +99,7 @@ qed. (* Basic inversion lemmas ***************************************************) (* Note: this can be derived from tpss_inv_atom1 *) -lemma tpss_inv_sort1: ∀L,T2,k,d,e. L ⊢ ⋆k [d, e] ≫* T2 → T2 = ⋆k. +lemma tpss_inv_sort1: ∀L,T2,k,d,e. L ⊢ ⋆k [d, e] ▶* T2 → T2 = ⋆k. #L #T2 #k #d #e #H @(tpss_ind … H) -T2 [ // | #T #T2 #_ #HT2 #IHT destruct @@ -107,21 +107,30 @@ lemma tpss_inv_sort1: ∀L,T2,k,d,e. L ⊢ ⋆k [d, e] ≫* T2 → T2 = ⋆k. ] qed-. -lemma tpss_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕓{I} V1. T1 [d, e] ≫* U2 → - ∃∃V2,T2. L ⊢ V1 [d, e] ≫* V2 & - L. 𝕓{I} V2 ⊢ T1 [d + 1, e] ≫* T2 & - U2 = 𝕓{I} V2. T2. +(* Note: this can be derived from tpss_inv_atom1 *) +lemma tpss_inv_gref1: ∀L,T2,p,d,e. L ⊢ §p [d, e] ▶* T2 → T2 = §p. +#L #T2 #p #d #e #H @(tpss_ind … H) -T2 +[ // +| #T #T2 #_ #HT2 #IHT destruct + >(tps_inv_gref1 … HT2) -HT2 // +] +qed-. + +lemma tpss_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ ⓑ{I} V1. T1 [d, e] ▶* U2 → + ∃∃V2,T2. L ⊢ V1 [d, e] ▶* V2 & + L. ⓑ{I} V2 ⊢ T1 [d + 1, e] ▶* T2 & + U2 = ⓑ{I} V2. T2. #d #e #L #I #V1 #T1 #U2 #H @(tpss_ind … H) -U2 [ /2 width=5/ | #U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct elim (tps_inv_bind1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H - lapply (tpss_lsubs_conf … HT1 (L. 𝕓{I} V2) ?) -HT1 /2 width=1/ /3 width=5/ + lapply (tpss_lsubs_conf … HT1 (L. ⓑ{I} V2) ?) -HT1 /2 width=1/ /3 width=5/ ] qed-. -lemma tpss_inv_flat1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕗{I} V1. T1 [d, e] ≫* U2 → - ∃∃V2,T2. L ⊢ V1 [d, e] ≫* V2 & L ⊢ T1 [d, e] ≫* T2 & - U2 = 𝕗{I} V2. T2. +lemma tpss_inv_flat1: ∀d,e,L,I,V1,T1,U2. L ⊢ ⓕ{I} V1. T1 [d, e] ▶* U2 → + ∃∃V2,T2. L ⊢ V1 [d, e] ▶* V2 & L ⊢ T1 [d, e] ▶* T2 & + U2 = ⓕ{I} V2. T2. #d #e #L #I #V1 #T1 #U2 #H @(tpss_ind … H) -U2 [ /2 width=5/ | #U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct @@ -129,7 +138,7 @@ lemma tpss_inv_flat1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕗{I} V1. T1 [d, e] ≫* U2 ] qed-. -lemma tpss_inv_refl_O2: ∀L,T1,T2,d. L ⊢ T1 [d, 0] ≫* T2 → T1 = T2. +lemma tpss_inv_refl_O2: ∀L,T1,T2,d. L ⊢ T1 [d, 0] ▶* T2 → T1 = T2. #L #T1 #T2 #d #H @(tpss_ind … H) -T2 [ // | #T #T2 #_ #HT2 #IHT <(tps_inv_refl_O2 … HT2) -HT2 //