X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fmultiple%2Fcpys_lift.ma;h=d21e9cce0ffd1ebf8a6c597fbac18c4d1fa0e1bc;hb=43282d3750af8831c8100c60d75c56fdfb7ff3c9;hp=d69de694e279bb1b82f7e9348b504a0e9578ac27;hpb=6c985e4e2e7846a2b9abd0c84569f21c24e9ce2f;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_lift.ma index d69de694e..d21e9cce0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_lift.ma @@ -21,8 +21,8 @@ include "basic_2/multiple/cpys.ma". lemma cpys_subst: ∀I,G,L,K,V,U1,i,d,e. d ≤ yinj i → i < d + e → - ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ▶*[0, ⫰(d+e-i)] U1 → - ∀U2. ⇧[0, i+1] U1 ≡ U2 → ⦃G, L⦄ ⊢ #i ▶*[d, e] U2. + ⬇[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ▶*[0, ⫰(d+e-i)] U1 → + ∀U2. ⬆[0, i+1] U1 ≡ U2 → ⦃G, L⦄ ⊢ #i ▶*[d, e] U2. #I #G #L #K #V #U1 #i #d #e #Hdi #Hide #HLK #H @(cpys_ind … H) -U1 [ /3 width=5 by cpy_cpys, cpy_subst/ | #U #U1 #_ #HU1 #IHU #U2 #HU12 @@ -38,8 +38,8 @@ qed. lemma cpys_subst_Y2: ∀I,G,L,K,V,U1,i,d. d ≤ yinj i → - ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ▶*[0, ∞] U1 → - ∀U2. ⇧[0, i+1] U1 ≡ U2 → ⦃G, L⦄ ⊢ #i ▶*[d, ∞] U2. + ⬇[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ▶*[0, ∞] U1 → + ∀U2. ⬆[0, i+1] U1 ≡ U2 → ⦃G, L⦄ ⊢ #i ▶*[d, ∞] U2. #I #G #L #K #V #U1 #i #d #Hdi #HLK #HVU1 #U2 #HU12 @(cpys_subst … HLK … HU12) >yminus_Y_inj // qed. @@ -49,9 +49,9 @@ qed. lemma cpys_inv_atom1: ∀I,G,L,T2,d,e. ⦃G, L⦄ ⊢ ⓪{I} ▶*[d, e] T2 → T2 = ⓪{I} ∨ ∃∃J,K,V1,V2,i. d ≤ yinj i & i < d + e & - ⇩[i] L ≡ K.ⓑ{J}V1 & + ⬇[i] L ≡ K.ⓑ{J}V1 & ⦃G, K⦄ ⊢ V1 ▶*[0, ⫰(d+e-i)] V2 & - ⇧[O, i+1] V2 ≡ T2 & + ⬆[O, i+1] V2 ≡ T2 & I = LRef i. #I #G #L #T2 #d #e #H @(cpys_ind … H) -T2 [ /2 width=1 by or_introl/ @@ -70,24 +70,24 @@ qed-. lemma cpys_inv_lref1: ∀G,L,T2,i,d,e. ⦃G, L⦄ ⊢ #i ▶*[d, e] T2 → T2 = #i ∨ ∃∃I,K,V1,V2. d ≤ i & i < d + e & - ⇩[i] L ≡ K.ⓑ{I}V1 & + ⬇[i] L ≡ K.ⓑ{I}V1 & ⦃G, K⦄ ⊢ V1 ▶*[0, ⫰(d+e-i)] V2 & - ⇧[O, i+1] V2 ≡ T2. + ⬆[O, i+1] V2 ≡ T2. #G #L #T2 #i #d #e #H elim (cpys_inv_atom1 … H) -H /2 width=1 by or_introl/ * #I #K #V1 #V2 #j #Hdj #Hjde #HLK #HV12 #HVT2 #H destruct /3 width=7 by ex5_4_intro, or_intror/ qed-. lemma cpys_inv_lref1_Y2: ∀G,L,T2,i,d. ⦃G, L⦄ ⊢ #i ▶*[d, ∞] T2 → T2 = #i ∨ - ∃∃I,K,V1,V2. d ≤ i & ⇩[i] L ≡ K.ⓑ{I}V1 & - ⦃G, K⦄ ⊢ V1 ▶*[0, ∞] V2 & ⇧[O, i+1] V2 ≡ T2. + ∃∃I,K,V1,V2. d ≤ i & ⬇[i] L ≡ K.ⓑ{I}V1 & + ⦃G, K⦄ ⊢ V1 ▶*[0, ∞] V2 & ⬆[O, i+1] V2 ≡ T2. #G #L #T2 #i #d #H elim (cpys_inv_lref1 … H) -H /2 width=1 by or_introl/ * >yminus_Y_inj /3 width=7 by or_intror, ex4_4_intro/ qed-. lemma cpys_inv_lref1_drop: ∀G,L,T2,i,d,e. ⦃G, L⦄ ⊢ #i ▶*[d, e] T2 → - ∀I,K,V1. ⇩[i] L ≡ K.ⓑ{I}V1 → - ∀V2. ⇧[O, i+1] V2 ≡ T2 → + ∀I,K,V1. ⬇[i] L ≡ K.ⓑ{I}V1 → + ∀V2. ⬆[O, i+1] V2 ≡ T2 → ∧∧ ⦃G, K⦄ ⊢ V1 ▶*[0, ⫰(d+e-i)] V2 & d ≤ i & i < d + e. @@ -103,8 +103,8 @@ qed-. (* Properties on relocation *************************************************) lemma cpys_lift_le: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*[dt, et] T2 → - ∀L,U1,s,d,e. dt + et ≤ yinj d → ⇩[s, d, e] L ≡ K → - ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 → + ∀L,U1,s,d,e. dt + et ≤ yinj d → ⬇[s, d, e] L ≡ K → + ⬆[d, e] T1 ≡ U1 → ∀U2. ⬆[d, e] T2 ≡ U2 → ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2. #G #K #T1 #T2 #dt #et #H #L #U1 #s #d #e #Hdetd #HLK #HTU1 @(cpys_ind … H) -T2 [ #U2 #H >(lift_mono … HTU1 … H) -H // @@ -117,8 +117,8 @@ qed-. lemma cpys_lift_be: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*[dt, et] T2 → ∀L,U1,s,d,e. dt ≤ yinj d → d ≤ dt + et → - ⇩[s, d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 → - ∀U2. ⇧[d, e] T2 ≡ U2 → ⦃G, L⦄ ⊢ U1 ▶*[dt, et + e] U2. + ⬇[s, d, e] L ≡ K → ⬆[d, e] T1 ≡ U1 → + ∀U2. ⬆[d, e] T2 ≡ U2 → ⦃G, L⦄ ⊢ U1 ▶*[dt, et + e] U2. #G #K #T1 #T2 #dt #et #H #L #U1 #s #d #e #Hdtd #Hddet #HLK #HTU1 @(cpys_ind … H) -T2 [ #U2 #H >(lift_mono … HTU1 … H) -H // | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2 @@ -129,8 +129,8 @@ lemma cpys_lift_be: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*[dt, et] T2 → qed-. lemma cpys_lift_ge: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*[dt, et] T2 → - ∀L,U1,s,d,e. yinj d ≤ dt → ⇩[s, d, e] L ≡ K → - ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 → + ∀L,U1,s,d,e. yinj d ≤ dt → ⬇[s, d, e] L ≡ K → + ⬆[d, e] T1 ≡ U1 → ∀U2. ⬆[d, e] T2 ≡ U2 → ⦃G, L⦄ ⊢ U1 ▶*[dt+e, et] U2. #G #K #T1 #T2 #dt #et #H #L #U1 #s #d #e #Hddt #HLK #HTU1 @(cpys_ind … H) -T2 [ #U2 #H >(lift_mono … HTU1 … H) -H // @@ -144,9 +144,9 @@ qed-. (* Inversion lemmas for relocation ******************************************) lemma cpys_inv_lift1_le: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2 → - ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → + ∀K,s,d,e. ⬇[s, d, e] L ≡ K → ∀T1. ⬆[d, e] T1 ≡ U1 → dt + et ≤ d → - ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[dt, et] T2 & ⇧[d, e] T2 ≡ U2. + ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[dt, et] T2 & ⬆[d, e] T2 ≡ U2. #G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hdetd @(cpys_ind … H) -U2 [ /2 width=3 by ex2_intro/ | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU @@ -155,9 +155,9 @@ lemma cpys_inv_lift1_le: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2 qed-. lemma cpys_inv_lift1_be: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2 → - ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → + ∀K,s,d,e. ⬇[s, d, e] L ≡ K → ∀T1. ⬆[d, e] T1 ≡ U1 → dt ≤ d → yinj d + e ≤ dt + et → - ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[dt, et - e] T2 & ⇧[d, e] T2 ≡ U2. + ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[dt, et - e] T2 & ⬆[d, e] T2 ≡ U2. #G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hdtd #Hdedet @(cpys_ind … H) -U2 [ /2 width=3 by ex2_intro/ | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU @@ -166,9 +166,9 @@ lemma cpys_inv_lift1_be: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2 qed-. lemma cpys_inv_lift1_ge: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2 → - ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → + ∀K,s,d,e. ⬇[s, d, e] L ≡ K → ∀T1. ⬆[d, e] T1 ≡ U1 → yinj d + e ≤ dt → - ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[dt - e, et] T2 & ⇧[d, e] T2 ≡ U2. + ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[dt - e, et] T2 & ⬆[d, e] T2 ≡ U2. #G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hdedt @(cpys_ind … H) -U2 [ /2 width=3 by ex2_intro/ | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU @@ -179,10 +179,10 @@ qed-. (* Advanced inversion lemmas on relocation **********************************) lemma cpys_inv_lift1_ge_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2 → - ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → + ∀K,s,d,e. ⬇[s, d, e] L ≡ K → ∀T1. ⬆[d, e] T1 ≡ U1 → d ≤ dt → dt ≤ yinj d + e → yinj d + e ≤ dt + et → ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[d, dt + et - (yinj d + e)] T2 & - ⇧[d, e] T2 ≡ U2. + ⬆[d, e] T2 ≡ U2. #G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet @(cpys_ind … H) -U2 [ /2 width=3 by ex2_intro/ | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU @@ -191,9 +191,9 @@ lemma cpys_inv_lift1_ge_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U qed-. lemma cpys_inv_lift1_be_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2 → - ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → + ∀K,s,d,e. ⬇[s, d, e] L ≡ K → ∀T1. ⬆[d, e] T1 ≡ U1 → dt ≤ d → dt + et ≤ yinj d + e → - ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[dt, d - dt] T2 & ⇧[d, e] T2 ≡ U2. + ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[dt, d - dt] T2 & ⬆[d, e] T2 ≡ U2. #G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hdtd #Hdetde @(cpys_ind … H) -U2 [ /2 width=3 by ex2_intro/ | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU @@ -202,9 +202,9 @@ lemma cpys_inv_lift1_be_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U qed-. lemma cpys_inv_lift1_le_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2 → - ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → + ∀K,s,d,e. ⬇[s, d, e] L ≡ K → ∀T1. ⬆[d, e] T1 ≡ U1 → dt ≤ d → d ≤ dt + et → dt + et ≤ yinj d + e → - ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[dt, d - dt] T2 & ⇧[d, e] T2 ≡ U2. + ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[dt, d - dt] T2 & ⬆[d, e] T2 ≡ U2. #G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hdtd #Hddet #Hdetde @(cpys_ind … H) -U2 [ /2 width=3 by ex2_intro/ | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU @@ -213,9 +213,9 @@ lemma cpys_inv_lift1_le_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U qed-. lemma cpys_inv_lift1_subst: ∀G,L,W1,W2,d,e. ⦃G, L⦄ ⊢ W1 ▶*[d, e] W2 → - ∀K,V1,i. ⇩[i+1] L ≡ K → ⇧[O, i+1] V1 ≡ W1 → + ∀K,V1,i. ⬇[i+1] L ≡ K → ⬆[O, i+1] V1 ≡ W1 → d ≤ yinj i → i < d + e → - ∃∃V2. ⦃G, K⦄ ⊢ V1 ▶*[O, ⫰(d+e-i)] V2 & ⇧[O, i+1] V2 ≡ W2. + ∃∃V2. ⦃G, K⦄ ⊢ V1 ▶*[O, ⫰(d+e-i)] V2 & ⬆[O, i+1] V2 ≡ W2. #G #L #W1 #W2 #d #e #HW12 #K #V1 #i #HLK #HVW1 #Hdi #Hide elim (cpys_inv_lift1_ge_up … HW12 … HLK … HVW1 ? ? ?) // >yplus_O1 yplus_SO2