X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Funfold%2Fltpss_tpss.ma;h=2b1b8377c2f5c128f871e87917b1a9eeb2a7872c;hb=6ebf3e5a09012b3349c6020fe692c3b22020684a;hp=24f1a595e65961a608d6299aa2e1de97cc44c6d1;hpb=eb918fc784eacd2094e3986ba321ef47690d9983;p=helm.git diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tpss.ma index 24f1a595e..2b1b8377c 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tpss.ma @@ -12,158 +12,127 @@ (* *) (**************************************************************************) -include "Basic_2/unfold/tpss_ltps.ma". -include "Basic_2/unfold/ltpss.ma". +include "basic_2/unfold/tpss_lift.ma". +include "basic_2/unfold/ltpss_tps.ma". -(* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************) +(* PARALLEL UNFOLD ON LOCAL ENVIRONMENTS ************************************) (* Properties concerning partial unfold on terms ****************************) -lemma ltpss_tpss_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ▶* L0 → - ∀T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶* U2 → - d1 + e1 ≤ d2 → L1 ⊢ T2 [d2, e2] ▶* U2. -#L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0 // -#L #L0 #_ #HL0 #IHL #T2 #U2 #d2 #e2 #HTU2 #Hde1d2 -lapply (ltps_tpss_trans_ge … HL0 HTU2) -HL0 -HTU2 /2 width=1/ -qed. - -lemma ltpss_tps_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ▶* L0 → - ∀T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 → - d1 + e1 ≤ d2 → L1 ⊢ T2 [d2, e2] ▶* U2. -#L1 #L0 #d1 #e1 #HL10 #T2 #U2 #d2 #e2 #HTU2 #Hde1d2 -@(ltpss_tpss_trans_ge … HL10 … Hde1d2) /2 width=1/ (**) (* /3 width=6/ is too slow *) -qed. - -lemma ltpss_tpss_trans_eq: ∀L0,L1,d,e. L0 [d, e] ▶* L1 → - ∀T2,U2. L1 ⊢ T2 [d, e] ▶* U2 → L0 ⊢ T2 [d, e] ▶* U2. -#L0 #L1 #d #e #H @(ltpss_ind … H) -L1 -[ /2 width=1/ -| #L #L1 #_ #HL1 #IHL #T2 #U2 #HTU2 - lapply (ltps_tpss_trans_eq … HL1 HTU2) -HL1 -HTU2 /2 width=1/ -] -qed. - -lemma ltpss_tps_trans_eq: ∀L0,L1,d,e. L0 [d, e] ▶* L1 → - ∀T2,U2. L1 ⊢ T2 [d, e] ▶ U2 → L0 ⊢ T2 [d, e] ▶* U2. -/3 width=3/ qed. - -lemma ltpss_tpss_conf_ge: ∀L0,L1,T2,U2,d1,e1,d2,e2. d1 + e1 ≤ d2 → - L0 ⊢ T2 [d2, e2] ▶* U2 → L0 [d1, e1] ▶* L1 → +lemma ltpss_tpss_conf_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶* U2 → + ∀L1,d1,e1. L0 [d1, e1] ▶* L1 → d1 + e1 ≤ d2 → L1 ⊢ T2 [d2, e2] ▶* U2. -#L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde1d2 #HTU2 #H @(ltpss_ind … H) -L1 -[ // -| -HTU2 #L #L1 #_ #HL1 #IHL - lapply (ltps_tpss_conf_ge … HL1 IHL) -HL1 -IHL // -] +#L0 #T2 #U2 #d2 #e2 #H #L1 #d1 #e1 #HL01 #Hde1d2 @(tpss_ind … H) -U2 // +#U #U2 #_ #HU2 #IHU +lapply (ltpss_tps_conf_ge … HU2 … HL01 ?) -L0 // -Hde1d2 /2 width=3/ qed. -lemma ltpss_tps_conf_ge: ∀L0,L1,T2,U2,d1,e1,d2,e2. d1 + e1 ≤ d2 → - L0 ⊢ T2 [d2, e2] ▶ U2 → L0 [d1, e1] ▶* L1 → - L1 ⊢ T2 [d2, e2] ▶* U2. -#L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde1d2 #HTU2 #HL01 -@(ltpss_tpss_conf_ge … Hde1d2 … HL01) /2 width=1/ (**) (* /3 width=6/ is too slow *) -qed. - -lemma ltpss_tpss_conf_eq: ∀L0,L1,T2,U2,d,e. - L0 ⊢ T2 [d, e] ▶* U2 → L0 [d, e] ▶* L1 → - ∃∃T. L1 ⊢ T2 [d, e] ▶* T & L1 ⊢ U2 [d, e] ▶* T. -#L0 #L1 #T2 #U2 #d #e #HTU2 #H @(ltpss_ind … H) -L1 +(* Basic_1: was: subst1_subst1_back *) +lemma ltpss_tps_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 → + ∀L1,d1,e1. L0 [d1, e1] ▶* L1 → + ∃∃T. L1 ⊢ T2 [d2, e2] ▶ T & + L1 ⊢ U2 [d1, e1] ▶* T. +#L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2 [ /2 width=3/ -| -HTU2 #L #L1 #_ #HL1 * #W2 #HTW2 #HUW2 - elim (ltps_tpss_conf … HL1 HTW2) -HTW2 #T #HT2 #HW2T - elim (ltps_tpss_conf … HL1 HUW2) -HL1 -HUW2 #U #HU2 #HW2U - elim (tpss_conf_eq … HW2T … HW2U) -HW2T -HW2U #V #HTV #HUV - lapply (tpss_trans_eq … HT2 … HTV) -T - lapply (tpss_trans_eq … HU2 … HUV) -U /2 width=3/ +| #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL01 + elim (lt_or_ge i2 d1) #Hi2d1 + [ elim (ltpss_ldrop_conf_le … HL01 … HLK0 ?) -L0 /2 width=2/ #X #H #HLK1 + elim (ltpss_inv_tpss11 … H ?) -H /2 width=1/ #K1 #V1 #_ #HV01 #H destruct + lapply (ldrop_fwd_ldrop2 … HLK1) #H + elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1 + lapply (tpss_lift_ge … HV01 … H HVW0 … HVW1) -V0 -H // >minus_plus minus_plus >commutative_plus /2 width=1/ + | lapply (ltpss_ldrop_conf_ge … HL01 … HLK0 ?) -L0 // /3 width=4/ + ] + ] +| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01 + elim (IHVW2 … HL01) -IHVW2 #V #HV2 #HVW2 + elim (IHTU2 (L1. ⓑ{I} V) (d1 + 1) e1 ?) -IHTU2 /2 width=1/ -HL01 /3 width=5/ +| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01 + elim (IHVW2 … HL01) -IHVW2 + elim (IHTU2 … HL01) -IHTU2 -HL01 /3 width=5/ ] qed. - -lemma ltpss_tps_conf_eq: ∀L0,L1,T2,U2,d,e. - L0 ⊢ T2 [d, e] ▶ U2 → L0 [d, e] ▶* L1 → - ∃∃T. L1 ⊢ T2 [d, e] ▶* T & L1 ⊢ U2 [d, e] ▶* T. -/3 width=3/ qed. - -lemma ltpss_tpss_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ▶* T2 → - ∀L2,ds,es. L1 [ds, es] ▶* L2 → - ∃∃T. L2 ⊢ T1 [d, e] ▶* T & L1 ⊢ T2 [ds, es] ▶* T. -#L1 #T1 #T2 #d #e #HT12 #L2 #ds #es #H @(ltpss_ind … H) -L2 -[ /3 width=3/ -| #L #L2 #HL1 #HL2 * #T #HT1 #HT2 - elim (ltps_tpss_conf … HL2 HT1) -HT1 #T0 #HT10 #HT0 - lapply (ltps_tpss_trans_eq … HL2 … HT0) -HL2 -HT0 #HT0 - lapply (ltpss_tpss_trans_eq … HL1 … HT0) -HL1 -HT0 #HT0 - lapply (tpss_trans_eq … HT2 … HT0) -T /2 width=3/ -] + +lemma ltpss_tpss_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶* U2 → + ∀L1,d1,e1. L1 [d1, e1] ▶* L0 → d1 + e1 ≤ d2 → + L1 ⊢ T2 [d2, e2] ▶* U2. +#L0 #T2 #U2 #d2 #e2 #H #L1 #d1 #e1 #HL01 #Hde1d2 @(tpss_ind … H) -U2 // +#U #U2 #_ #HU2 #IHU +lapply (ltpss_tps_trans_ge … HU2 … HL01 ?) -L0 // -Hde1d2 /2 width=3/ qed. -lemma ltpss_tps_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ▶ T2 → - ∀L2,ds,es. L1 [ds, es] ▶* L2 → - ∃∃T. L2 ⊢ T1 [d, e] ▶* T & L1 ⊢ T2 [ds, es] ▶* T. -/3 width=1/ qed. - -(* Advanced properties ******************************************************) - -lemma ltpss_tps2: ∀L1,L2,I,e. - L1 [0, e] ▶* L2 → ∀V1,V2. L2 ⊢ V1 [0, e] ▶ V2 → - L1. ⓑ{I} V1 [0, e + 1] ▶* L2. ⓑ{I} V2. -#L1 #L2 #I #e #H @(ltpss_ind … H) -L2 -[ /3 width=1/ -| #L #L2 #_ #HL2 #IHL #V1 #V2 #HV12 - elim (ltps_tps_trans … HV12 … HL2) -HV12 #V #HV1 #HV2 - lapply (IHL … HV1) -IHL -HV1 #HL1 - @step /2 width=5/ (**) (* /3 width=5/ is too slow *) +(* Basic_1: was: subst1_subst1 *) +lemma ltpss_tps_trans: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 → + ∀L1,d1,e1. L1 [d1, e1] ▶* L0 → + ∃∃T. L1 ⊢ T2 [d2, e2] ▶ T & + L0 ⊢ T [d1, e1] ▶* U2. +#L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2 +[ /2 width=3/ +| #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL10 + elim (lt_or_ge i2 d1) #Hi2d1 + [ elim (ltpss_ldrop_trans_le … HL10 … HLK0 ?) -HL10 /2 width=2/ #X #H #HLK1 + elim (ltpss_inv_tpss12 … H ?) -H /2 width=1/ #K1 #V1 #_ #HV01 #H destruct + lapply (ldrop_fwd_ldrop2 … HLK0) -HLK0 #H + elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1 + lapply (tpss_lift_ge … HV01 … H HVW1 … HVW0) -V0 -H // >minus_plus minus_plus >commutative_plus /2 width=1/ + | lapply (ltpss_ldrop_trans_ge … HL10 … HLK0 ?) -HL10 -HLK0 // /3 width=4/ + ] + ] +| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10 + elim (IHVW2 … HL10) -IHVW2 #V #HV2 #HVW2 + elim (IHTU2 (L1. ⓑ{I} V) (d1 + 1) e1 ?) -IHTU2 /2 width=1/ -HL10 /3 width=5/ +| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10 + elim (IHVW2 … HL10) -IHVW2 + elim (IHTU2 … HL10) -IHTU2 -HL10 /3 width=5/ ] qed. -lemma ltpss_tps2_lt: ∀L1,L2,I,V1,V2,e. - L1 [0, e - 1] ▶* L2 → L2 ⊢ V1 [0, e - 1] ▶ V2 → - 0 < e → L1. ⓑ{I} V1 [0, e] ▶* L2. ⓑ{I} V2. -#L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He ->(plus_minus_m_m e 1) // /2 width=1/ -qed. - -lemma ltpss_tps1: ∀L1,L2,I,d,e. L1 [d, e] ▶* L2 → - ∀V1,V2. L2 ⊢ V1 [d, e] ▶ V2 → - L1. ⓑ{I} V1 [d + 1, e] ▶* L2. ⓑ{I} V2. -#L1 #L2 #I #d #e #H @(ltpss_ind … H) -L2 -[ /3 width=1/ -| #L #L2 #_ #HL2 #IHL #V1 #V2 #HV12 - elim (ltps_tps_trans … HV12 … HL2) -HV12 #V #HV1 #HV2 - lapply (IHL … HV1) -IHL -HV1 #HL1 - @step /2 width=5/ (**) (* /3 width=5/ is too slow *) +fact ltpss_tps_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e. + L1 ⊢ T2 [d, e] ▶ U2 → ∀L0. L0 [d, e] ▶* L1 → + Y1 = L1 → X2 = T2 → L0 ⊢ T2 [d, e] ▶* U2. +#Y1 #X2 @(cw_wf_ind … Y1 X2) -Y1 -X2 #Y1 #X2 #IH +#L1 #T2 #U2 #d #e * -L1 -T2 -U2 -d -e +[ // +| #L1 #K1 #V1 #W1 #i #d #e #Hdi #Hide #HLK1 #HVW1 #L0 #HL10 #H1 #H2 destruct + lapply (ldrop_fwd_lw … HLK1) #H1 normalize in H1; + elim (ltpss_ldrop_trans_be … HL10 … HLK1 ? ?) -HL10 -HLK1 // /2 width=2/ #X #H #HLK0 + elim (ltpss_inv_tpss22 … H ?) -H /2 width=1/ #K0 #V0 #HK01 #HV01 #H destruct + lapply (tpss_fwd_tw … HV01) #H2 + lapply (transitive_le (#[K1] + #[V0]) … H1) -H1 /2 width=1/ -H2 #H + lapply (IH … HV01 … HK01 ? ?) -IH -HV01 -HK01 + [1,3: // |2,4: skip | normalize /2 width=1/ | /3 width=6/ ] +| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #L0 #HL0 #H1 #H2 destruct + lapply (tps_lsubs_conf … HT12 (L. ⓑ{I} V1) ?) -HT12 /2 width=1/ #HT12 + lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=2/ ] #HV12 + lapply (IH … HT12 (L0. ⓑ{I} V1) ? ? ?) -IH -HT12 [1,3,5: /2 width=2/ |2,4: skip | normalize // ] -HL0 #HT12 + lapply (tpss_lsubs_conf … HT12 (L0. ⓑ{I} V2) ?) -HT12 /2 width=1/ +| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #L0 #HL0 #H1 #H2 destruct + lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=3/ ] + lapply (IH … HT12 … HL0 ? ?) -IH -HT12 [1,3,5: normalize // |2,4: skip ] -HL0 /2 width=1/ ] qed. -lemma ltpss_tps1_lt: ∀L1,L2,I,V1,V2,d,e. - L1 [d - 1, e] ▶* L2 → L2 ⊢ V1 [d - 1, e] ▶ V2 → - 0 < d → L1. ⓑ{I} V1 [d, e] ▶* L2. ⓑ{I} V2. -#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd ->(plus_minus_m_m d 1) // /2 width=1/ -qed. - -(* Advanced forward lemmas **************************************************) - -lemma ltpss_fwd_tpss21: ∀e,K1,I,V1,L2. 0 < e → K1. ⓑ{I} V1 [0, e] ▶* L2 → - ∃∃K2,V2. K1 [0, e - 1] ▶* K2 & K1 ⊢ V1 [0, e - 1] ▶* V2 & - L2 = K2. ⓑ{I} V2. -#e #K1 #I #V1 #L2 #He #H @(ltpss_ind … H) -L2 -[ /2 width=5/ -| #L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct - elim (ltps_inv_tps21 … HL2 ?) -HL2 // #K2 #V2 #HK2 #HV2 #H - lapply (ltps_tps_trans_eq … HV2 … HK2) -HV2 #HV2 - lapply (ltpss_tpss_trans_eq … HK1 … HV2) -HV2 #HV2 /3 width=5/ -] -qed-. +lemma ltps_tps_trans_eq: ∀L1,T2,U2,d,e. L1 ⊢ T2 [d, e] ▶ U2 → + ∀L0. L0 [d, e] ▶ L1 → L0 ⊢ T2 [d, e] ▶* U2. +/2 width=5/ qed. -lemma ltpss_fwd_tpss11: ∀d,e,I,K1,V1,L2. 0 < d → K1. ⓑ{I} V1 [d, e] ▶* L2 → - ∃∃K2,V2. K1 [d - 1, e] ▶* K2 & - K1 ⊢ V1 [d - 1, e] ▶* V2 & - L2 = K2. ⓑ{I} V2. -#d #e #K1 #I #V1 #L2 #Hd #H @(ltpss_ind … H) -L2 -[ /2 width=5/ -| #L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct - elim (ltps_inv_tps11 … HL2 ?) -HL2 // #K2 #V2 #HK2 #HV2 #H - lapply (ltps_tps_trans_eq … HV2 … HK2) -HV2 #HV2 - lapply (ltpss_tpss_trans_eq … HK1 … HV2) -HV2 #HV2 /3 width=5/ -] -qed-. +lemma ltps_tpss_trans_eq: ∀L0,L1,T2,U2,d,e. L0 [d, e] ▶ L1 → + L1 ⊢ T2 [d, e] ▶* U2 → L0 ⊢ T2 [d, e] ▶* U2. +#L0 #L1 #T2 #U2 #d #e #HL01 #H @(tpss_ind … H) -U2 // +#U #U2 #_ #HU2 #IHU @(tpss_trans_eq … IHU) /2 width=3/ +qed. +*)