X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Funfold%2Fltpss_tpss.ma;h=24f1a595e65961a608d6299aa2e1de97cc44c6d1;hb=16bbb2d6b16d5647d944f18f0fd6d4dd3df431fe;hp=c75119b66af51e71a2ce56cf1f1299e9120ff520;hpb=7aa41e02e64bd09df253cc4267a44b4f49b16e03;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 c75119b66..24f1a595e 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 @@ -19,23 +19,23 @@ include "Basic_2/unfold/ltpss.ma". (* 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. +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. +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. +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 @@ -43,13 +43,13 @@ lemma ltpss_tpss_trans_eq: ∀L0,L1,d,e. L0 [d, e] ≫* L1 → ] 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. +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 → - L1 ⊢ T2 [d2, e2] ≫* U2. + L0 ⊢ T2 [d2, e2] ▶* U2 → L0 [d1, e1] ▶* L1 → + 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 @@ -58,15 +58,15 @@ lemma ltpss_tpss_conf_ge: ∀L0,L1,T2,U2,d1,e1,d2,e2. d1 + e1 ≤ d2 → 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 ⊢ 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 ⊢ 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 [ /2 width=3/ | -HTU2 #L #L1 #_ #HL1 * #W2 #HTW2 #HUW2 @@ -79,13 +79,13 @@ lemma ltpss_tpss_conf_eq: ∀L0,L1,T2,U2,d,e. 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. + 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. +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 @@ -96,16 +96,16 @@ lemma ltpss_tpss_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≫* T2 → ] 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. +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 [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 @@ -116,15 +116,15 @@ lemma ltpss_tps2: ∀L1,L2,I,e. 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 [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. +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 @@ -135,17 +135,17 @@ lemma ltpss_tps1: ∀L1,L2,I,d,e. L1 [d, e] ≫* L2 → 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 [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. +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 @@ -155,10 +155,10 @@ lemma ltpss_fwd_tpss21: ∀e,K1,I,V1,L2. 0 < e → K1. 𝕓{I} V1 [0, e] ≫* L2 ] 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. +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