X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Funfold%2Fltpss_ltpss.ma;h=f866adc126cd41eb357b208098568ee8a483a81c;hb=039f4f6db3a3c128959cd471eb78f575906e07b6;hp=ce2271b705f0b8f4b3622b0c593718a57b845021;hpb=6ebf3e5a09012b3349c6020fe692c3b22020684a;p=helm.git diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.ma index ce2271b70..f866adc12 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.ma @@ -13,16 +13,17 @@ (**************************************************************************) include "basic_2/unfold/tpss_tpss.ma". +include "basic_2/unfold/tpss_alt.ma". include "basic_2/unfold/ltpss_tpss.ma". (* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************) (* Advanced properties ******************************************************) -lemma ltpss_tpss_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. +lemma ltpss_tpss_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 #L1 #d1 #e1 #HL01 @(tpss_ind … H) -U2 /2 width=3/ #U #U2 #_ #HU2 * #X2 #HTX2 #HUX2 elim (ltpss_tps_conf … HU2 … HL01) -L0 #X1 #HUX1 #HU2X1 @@ -31,8 +32,8 @@ lapply (tpss_trans_eq … HU2X1 … HX1) -X1 /3 width=3/ qed. lemma ltpss_tpss_trans_down: ∀L0,L1,T2,U2,d1,e1,d2,e2. d2 + e2 ≤ d1 → - L1 [d1, e1] ▶* L0 → L0 ⊢ T2 [d2, e2] ▶* U2 → - ∃∃T. L1 ⊢ T2 [d2, e2] ▶* T & L0 ⊢ T [d1, e1] ▶* U2. + L1 ▶* [d1, e1] L0 → L0 ⊢ T2 ▶* [d2, e2] U2 → + ∃∃T. L1 ⊢ T2 ▶* [d2, e2] T & L0 ⊢ T ▶* [d1, e1] U2. #L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde2d1 #HL10 #H @(tpss_ind … H) -U2 [ /2 width=3/ | #U #U2 #_ #HU2 * #T #HT2 #HTU @@ -42,11 +43,45 @@ lemma ltpss_tpss_trans_down: ∀L0,L1,T2,U2,d1,e1,d2,e2. d2 + e2 ≤ d1 → ] qed. +fact ltpss_tpss_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 #H @(tpss_ind_alt … H) -L1 -T2 -U2 -d -e +[ // +| #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #HV12 #HVW2 #_ #L0 #HL01 #H1 #H2 destruct + lapply (ldrop_fwd_lw … HLK1) #H1 normalize in H1; + elim (ltpss_ldrop_trans_be … HL01 … HLK1 ? ?) -HL01 -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 (tpss_trans_eq … HV01 HV12) -V1 #HV02 + lapply (IH … HV02 … HK01 ? ?) -IH -HV02 -HK01 + [1,3: // |2,4: skip | normalize /2 width=1/ | /2 width=6/ ] +| #L #a #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #L0 #HL0 #H1 #H2 destruct + lapply (tpss_lsubs_trans … 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_trans … 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_tpss_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_tps_trans_eq: ∀L0,L1,T2,U2,d,e. L0 ▶* [d, e] L1 → + L1 ⊢ T2 ▶ [d, e] U2 → L0 ⊢ T2 ▶* [d, e] U2. +/3 width=3/ qed. + (* Main properties **********************************************************) -fact ltpss_conf_aux: ∀K,K1,L1,d1,e1. K1 [d1, e1] ▶* L1 → - ∀K2,L2,d2,e2. K2 [d2, e2] ▶* L2 → K1 = K → K2 = K → - ∃∃L. L1 [d2, e2] ▶* L & L2 [d1, e1] ▶* L. +fact ltpss_conf_aux: ∀K,K1,L1,d1,e1. K1 ▶* [d1, e1] L1 → + ∀K2,L2,d2,e2. K2 ▶* [d2, e2] L2 → K1 = K → K2 = K → + ∃∃L. L1 ▶* [d2, e2] L & L2 ▶* [d1, e1] L. #K @(lw_wf_ind … K) -K #K #IH #K1 #L1 #d1 #e1 * -K1 -L1 -d1 -e1 [ -IH /2 width=3/ | -IH #K1 #I1 #V1 #K2 #L2 #d2 #e2 * -K2 -L2 -d2 -e2 @@ -94,7 +129,18 @@ fact ltpss_conf_aux: ∀K,K1,L1,d1,e1. K1 [d1, e1] ▶* L1 → ] qed. -lemma ltpss_conf: ∀L0,L1,d1,e1. L0 [d1, e1] ▶* L1 → - ∀L2,d2,e2. L0 [d2, e2] ▶* L2 → - ∃∃L. L1 [d2, e2] ▶* L & L2 [d1, e1] ▶* L. +lemma ltpss_conf: ∀L0,L1,d1,e1. L0 ▶* [d1, e1] L1 → + ∀L2,d2,e2. L0 ▶* [d2, e2] L2 → + ∃∃L. L1 ▶* [d2, e2] L & L2 ▶* [d1, e1] L. /2 width=7/ qed. + +theorem ltpss_trans_eq: ∀L1,L,d,e. L1 ▶* [d, e] L → + ∀L2. L ▶* [d, e] L2 → L1 ▶* [d, e] L2. +#L1 #L #d #e #H elim H -L1 -L -d -e // +[ #L1 #L #I #V1 #V #e #_ #HV1 #IHL1 #X #H + elim (ltpss_inv_tpss21 … H ?) -H //