X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsubstitution%2Fcpye_lift.ma;h=3c0abe617b7db6e88b5f6c018bfc1ef8b6abc268;hb=d95bd78c09617ad212fa9e96837a15fc907dcfca;hp=1d494871ced9faa4362fb670d80cb57856aa6c88;hpb=e2527c6784c2593ca67af35fafaf0b3725d80a60;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpye_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpye_lift.ma index 1d494871c..3c0abe617 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpye_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpye_lift.ma @@ -25,10 +25,10 @@ lemma cpye_subst: ∀I,G,L,K,V1,V2,W2,i,d,e. d ≤ yinj i → i < d + e → ⇩[i] L ≡ K.ⓑ{I}V1 → ⦃G, K⦄ ⊢ V1 ▶*[O, ⫰(d+e-i)] 𝐍⦃V2⦄ → ⇧[O, i+1] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃W2⦄. #I #G #L #K #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK * -/4 width=13 by cpys_subst, cny_subst_aux, ldrop_fwd_drop2, conj/ +/4 width=13 by cpys_subst, cny_lift_subst, ldrop_fwd_drop2, conj/ qed. -lemma cpys_total: ∀G,L,T1,d,e. ∃T2. ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄. +lemma cpye_total: ∀G,L,T1,d,e. ∃T2. ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄. #G #L #T1 @(fqup_wf_ind_eq … G L T1) -G -L -T1 #Z #Y #X #IH #G #L * * [ #k #HG #HL #HT #d #e destruct -IH /2 width=2 by ex_intro/ @@ -64,7 +64,7 @@ lemma cpye_inv_lref1: ∀G,L,T2,d,e,i. ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃T2⦄ /3 width=1 by or4_intro0, or4_intro1, or4_intro2, conj/ | * #I #K #V1 #V2 #Hdi #Hide #HLK #HV12 #HVT2 @or4_intro3 @(ex5_4_intro … HLK … HVT2) (**) (* explicit constructor *) - /4 width=13 by cny_inv_subst_aux, ldrop_fwd_drop2, conj/ + /4 width=13 by cny_inv_lift_subst, ldrop_fwd_drop2, conj/ ] qed-. @@ -78,16 +78,92 @@ lemma cpye_inv_lref1_free: ∀G,L,T2,d,e,i. ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃ elim (ylt_yle_false … H) // qed-. +lemma cpye_inv_lref1_lget: ∀G,L,T2,d,e,i. ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃T2⦄ → + ∀I,K,V1. ⇩[i] L ≡ K.ⓑ{I}V1 → + ∨∨ d + e ≤ yinj i ∧ T2 = #i + | yinj i < d ∧ T2 = #i + | ∃∃V2. d ≤ yinj i & yinj i < d + e & + ⦃G, K⦄ ⊢ V1 ▶*[yinj 0, ⫰(d+e-yinj i)] 𝐍⦃V2⦄ & + ⇧[O, i+1] V2 ≡ T2. +#G #L #T2 #d #e #i #H #I #K #V1 #HLK elim (cpye_inv_lref1 … H) -H * +[ #H elim (lt_refl_false i) -T2 -d + @(lt_to_le_to_lt … H) -H /2 width=5 by ldrop_fwd_length_lt2/ +| /3 width=1 by or3_intro0, conj/ +| /3 width=1 by or3_intro1, conj/ +| #Z #Y #X1 #X2 #Hdi #Hide #HLY #HX12 #HXT2 + lapply (ldrop_mono … HLY … HLK) -HLY -HLK #H destruct + /3 width=3 by or3_intro2, ex4_intro/ +] +qed-. + +lemma cpye_inv_lref1_subst_ex: ∀G,L,T2,d,e,i. ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃T2⦄ → + ∀I,K,V1. d ≤ yinj i → yinj i < d + e → + ⇩[i] L ≡ K.ⓑ{I}V1 → + ∃∃V2. ⦃G, K⦄ ⊢ V1 ▶*[yinj 0, ⫰(d+e-yinj i)] 𝐍⦃V2⦄ & + ⇧[O, i+1] V2 ≡ T2. +#G #L #T2 #d #e #i #H #I #K #V1 #Hdi #Hide #HLK +elim (cpye_inv_lref1_lget … H … HLK) -H * /2 width=3 by ex2_intro/ +#H elim (ylt_yle_false … H) // +qed-. + lemma cpye_inv_lref1_subst: ∀G,L,T2,d,e,i. ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃T2⦄ → ∀I,K,V1,V2. d ≤ yinj i → yinj i < d + e → ⇩[i] L ≡ K.ⓑ{I}V1 → ⇧[O, i+1] V2 ≡ T2 → ⦃G, K⦄ ⊢ V1 ▶*[yinj 0, ⫰(d+e-yinj i)] 𝐍⦃V2⦄. -#G #L #T2 #d #e #i #H #I #K #V1 #V2 #Hdi #Hide #HLK #HVT2 elim (cpye_inv_lref1 … H) -H * -[ #H elim (lt_refl_false i) -V2 -T2 -d - @(lt_to_le_to_lt … H) -H /2 width=5 by ldrop_fwd_length_lt2/ -|2,3: #H elim (ylt_yle_false … H) // -| #Z #Y #X1 #X2 #_ #_ #HLY #HX12 #HXT2 - lapply (ldrop_mono … HLY … HLK) -HLY -HLK #H destruct - lapply (lift_inj … HXT2 … HVT2) -HXT2 -HVT2 #H destruct // -] +#G #L #T2 #d #e #i #H #I #K #V1 #V2 #Hdi #Hide #HLK #HVT2 +elim (cpye_inv_lref1_subst_ex … H … HLK) -H -HLK // +#X2 #H0 #HXT2 lapply (lift_inj … HXT2 … HVT2) -HXT2 -HVT2 #H destruct // +qed-. + +(* Inversion lemmas on relocation *******************************************) + +lemma cpye_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 → + dt + et ≤ d → + ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[dt, et] 𝐍⦃T2⦄ & ⇧[d, e] T2 ≡ U2. +#G #L #U1 #U2 #dt #et * #HU12 #HU2 #K #s #d #e #HLK #T1 #HTU1 #Hdetd +elim (cpys_inv_lift1_le … HU12 … HLK … HTU1) -U1 // #T2 #HT12 #HTU2 +lapply (cny_inv_lift_le … HU2 … HLK … HTU2 ?) -L +/3 width=3 by ex2_intro, conj/ +qed-. + +lemma cpye_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 → + dt ≤ d → yinj d + e ≤ dt + et → + ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[dt, et - e] 𝐍⦃T2⦄ & ⇧[d, e] T2 ≡ U2. +#G #L #U1 #U2 #dt #et * #HU12 #HU2 #K #s #d #e #HLK #T1 #HTU1 #Hdtd #Hdedet +elim (cpys_inv_lift1_be … HU12 … HLK … HTU1) -U1 // #T2 #HT12 #HTU2 +lapply (cny_inv_lift_be … HU2 … HLK … HTU2 ? ?) -L +/3 width=3 by ex2_intro, conj/ +qed-. + +lemma cpye_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 → + yinj d + e ≤ dt → + ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[dt - e, et] 𝐍⦃T2⦄ & ⇧[d, e] T2 ≡ U2. +#G #L #U1 #U2 #dt #et * #HU12 #HU2 #K #s #d #e #HLK #T1 #HTU1 #Hdedt +elim (cpys_inv_lift1_ge … HU12 … HLK … HTU1) -U1 // #T2 #HT12 #HTU2 +lapply (cny_inv_lift_ge … HU2 … HLK … HTU2 ?) -L +/3 width=3 by ex2_intro, conj/ +qed-. + +lemma cpye_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 → + 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. +#G #L #U1 #U2 #dt #et * #HU12 #HU2 #K #s #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet +elim (cpys_inv_lift1_ge_up … HU12 … HLK … HTU1) -U1 // #T2 #HT12 #HTU2 +lapply (cny_inv_lift_ge_up … HU2 … HLK … HTU2 ? ? ?) -L +/3 width=3 by ex2_intro, conj/ +qed-. + +lemma cpye_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 → + d ≤ yinj i → i < d + e → + ∃∃V2. ⦃G, K⦄ ⊢ V1 ▶*[O, ⫰(d+e-i)] 𝐍⦃V2⦄ & ⇧[O, i+1] V2 ≡ W2. +#G #L #W1 #W2 #d #e * #HW12 #HW2 #K #V1 #i #HLK #HVW1 #Hdi #Hide +elim (cpys_inv_lift1_subst … HW12 … HLK … HVW1) -W1 // #V2 #HV12 #HVW2 +lapply (cny_inv_lift_subst … HLK HW2 HVW2) -L +/3 width=3 by ex2_intro, conj/ qed-.