X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Flambda-delta%2Fsubstitution%2Flift.ma;h=a5b15e1100d74da3278a51f706b50aa1bc729554;hb=14fef03bcc79583593a129bf9c68bdf690a10eb7;hp=a550123b51486976e28605fe25ed9b831b17696b;hpb=1df995bc8675c8b1118889cf470fc4d1d2ab5a22;p=helm.git diff --git a/matita/matita/lib/lambda-delta/substitution/lift.ma b/matita/matita/lib/lambda-delta/substitution/lift.ma index a550123b5..a5b15e110 100644 --- a/matita/matita/lib/lambda-delta/substitution/lift.ma +++ b/matita/matita/lib/lambda-delta/substitution/lift.ma @@ -9,27 +9,222 @@ \ / V_______________________________________________________________ *) -include "lambda-delta/language/term.ma". +include "lambda-delta/syntax/term.ma". (* RELOCATION ***************************************************************) inductive lift: term → nat → nat → term → Prop ≝ - | lift_sort : ∀k,d,e. lift (⋆k) d e (⋆k) - | lift_lref_lt: ∀i,d,e. i < d → lift (#i) d e (#i) - | lift_lref_ge: ∀i,d,e. d ≤ i → lift (#i) d e (#(i + e)) - | lift_con2 : ∀I,V1,V2,T1,T2,d,e. - lift V1 d e V2 → lift T1 (d + 1) e T2 → - lift (♭I V1. T1) d e (♭I V2. T2) +| lift_sort : ∀k,d,e. lift (⋆k) d e (⋆k) +| lift_lref_lt: ∀i,d,e. i < d → lift (#i) d e (#i) +| lift_lref_ge: ∀i,d,e. d ≤ i → lift (#i) d e (#(i + e)) +| lift_bind : ∀I,V1,V2,T1,T2,d,e. + lift V1 d e V2 → lift T1 (d + 1) e T2 → + lift (𝕓{I} V1. T1) d e (𝕓{I} V2. T2) +| lift_flat : ∀I,V1,V2,T1,T2,d,e. + lift V1 d e V2 → lift T1 d e T2 → + lift (𝕗{I} V1. T1) d e (𝕗{I} V2. T2) . interpretation "relocation" 'RLift T1 d e T2 = (lift T1 d e T2). -(* The basic inversion lemmas ***********************************************) +(* Basic properties *********************************************************) + +lemma lift_lref_ge_minus: ∀d,e,i. d + e ≤ i → ↑[d, e] #(i - e) ≡ #i. +#d #e #i #H >(plus_minus_m_m i e) in ⊢ (? ? ? ? %) /3/ +qed. + +lemma lift_refl: ∀T,d. ↑[d, 0] T ≡ T. +#T elim T -T +[ // +| #i #d elim (lt_or_ge i d) /2/ +| #I elim I -I /2/ +] +qed. + +lemma lift_total: ∀T1,d,e. ∃T2. ↑[d,e] T1 ≡ T2. +#T1 elim T1 -T1 +[ /2/ +| #i #d #e elim (lt_or_ge i d) /3/ +| * #I #V1 #T1 #IHV1 #IHT1 #d #e + elim (IHV1 d e) -IHV1 #V2 #HV12 + [ elim (IHT1 (d+1) e) -IHT1 /3/ + | elim (IHT1 d e) -IHT1 /3/ + ] +] +qed. + +lemma lift_split: ∀d1,e2,T1,T2. ↑[d1, e2] T1 ≡ T2 → ∀d2,e1. + d1 ≤ d2 → d2 ≤ d1 + e1 → e1 ≤ e2 → + ∃∃T. ↑[d1, e1] T1 ≡ T & ↑[d2, e2 - e1] T ≡ T2. +#d1 #e2 #T1 #T2 #H elim H -H d1 e2 T1 T2 +[ /3/ +| #i #d1 #e2 #Hid1 #d2 #e1 #Hd12 #_ #_ + lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2 /4/ +| #i #d1 #e2 #Hid1 #d2 #e1 #_ #Hd21 #He12 + lapply (transitive_le …(i+e1) Hd21 ?) /2/ -Hd21 #Hd21 + <(arith_d1 i e2 e1) // /3/ +| #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12 + elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b + elim (IHT (d2+1) … ? ? He12) /3 width = 5/ +| #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12 + elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b + elim (IHT d2 … ? ? He12) /3 width = 5/ +] +qed. + +(* Basic inversion lemmas ***************************************************) + +lemma lift_inv_refl_aux: ∀d,e,T1,T2. ↑[d, e] T1 ≡ T2 → e = 0 → T1 = T2. +#d #e #T1 #T2 #H elim H -H d e T1 T2 /3/ +qed. + +lemma lift_inv_refl: ∀d,T1,T2. ↑[d, 0] T1 ≡ T2 → T1 = T2. +/2/ qed. + +lemma lift_inv_sort1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀k. T1 = ⋆k → T2 = ⋆k. +#d #e #T1 #T2 * -d e T1 T2 // +[ #i #d #e #_ #k #H destruct +| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct +| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct +] +qed. + +lemma lift_inv_sort1: ∀d,e,T2,k. ↑[d,e] ⋆k ≡ T2 → T2 = ⋆k. +/2 width=5/ qed. + +lemma lift_inv_lref1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀i. T1 = #i → + (i < d ∧ T2 = #i) ∨ (d ≤ i ∧ T2 = #(i + e)). +#d #e #T1 #T2 * -d e T1 T2 +[ #k #d #e #i #H destruct +| #j #d #e #Hj #i #Hi destruct /3/ +| #j #d #e #Hj #i #Hi destruct /3/ +| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #i #H destruct +| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #i #H destruct +] +qed. + +lemma lift_inv_lref1: ∀d,e,T2,i. ↑[d,e] #i ≡ T2 → + (i < d ∧ T2 = #i) ∨ (d ≤ i ∧ T2 = #(i + e)). +/2/ qed. + +lemma lift_inv_lref1_lt: ∀d,e,T2,i. ↑[d,e] #i ≡ T2 → i < d → T2 = #i. +#d #e #T2 #i #H elim (lift_inv_lref1 … H) -H * // +#Hdi #_ #Hid lapply (le_to_lt_to_lt … Hdi Hid) -Hdi Hid #Hdd +elim (lt_refl_false … Hdd) +qed. + +lemma lift_inv_lref1_ge: ∀d,e,T2,i. ↑[d,e] #i ≡ T2 → d ≤ i → T2 = #(i + e). +#d #e #T2 #i #H elim (lift_inv_lref1 … H) -H * // +#Hid #_ #Hdi lapply (le_to_lt_to_lt … Hdi Hid) -Hdi Hid #Hdd +elim (lt_refl_false … Hdd) +qed. + +lemma lift_inv_bind1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → + ∀I,V1,U1. T1 = 𝕓{I} V1.U1 → + ∃∃V2,U2. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 & + T2 = 𝕓{I} V2. U2. +#d #e #T1 #T2 * -d e T1 T2 +[ #k #d #e #I #V1 #U1 #H destruct +| #i #d #e #_ #I #V1 #U1 #H destruct +| #i #d #e #_ #I #V1 #U1 #H destruct +| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V1 #U1 #H destruct /2 width=5/ +| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V1 #U1 #H destruct +] +qed. + +lemma lift_inv_bind1: ∀d,e,T2,I,V1,U1. ↑[d,e] 𝕓{I} V1. U1 ≡ T2 → + ∃∃V2,U2. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 & + T2 = 𝕓{I} V2. U2. +/2/ qed. + +lemma lift_inv_flat1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → + ∀I,V1,U1. T1 = 𝕗{I} V1.U1 → + ∃∃V2,U2. ↑[d,e] V1 ≡ V2 & ↑[d,e] U1 ≡ U2 & + T2 = 𝕗{I} V2. U2. +#d #e #T1 #T2 * -d e T1 T2 +[ #k #d #e #I #V1 #U1 #H destruct +| #i #d #e #_ #I #V1 #U1 #H destruct +| #i #d #e #_ #I #V1 #U1 #H destruct +| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V1 #U1 #H destruct +| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V1 #U1 #H destruct /2 width=5/ +] +qed. + +lemma lift_inv_flat1: ∀d,e,T2,I,V1,U1. ↑[d,e] 𝕗{I} V1. U1 ≡ T2 → + ∃∃V2,U2. ↑[d,e] V1 ≡ V2 & ↑[d,e] U1 ≡ U2 & + T2 = 𝕗{I} V2. U2. +/2/ qed. lemma lift_inv_sort2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀k. T2 = ⋆k → T1 = ⋆k. -#d #e #T1 #T2 #H elim H -H d e T1 T2 // - [ #i #d #e #_ #k #H destruct (***) (* DESTRUCT FAILS *) +#d #e #T1 #T2 * -d e T1 T2 // +[ #i #d #e #_ #k #H destruct +| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct +| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct +] +qed. lemma lift_inv_sort2: ∀d,e,T1,k. ↑[d,e] T1 ≡ ⋆k → T1 = ⋆k. -#d #e #T1 #k #H lapply (lift_inv_sort2_aux … H) /2/ -qed. +/2 width=5/ qed. + +lemma lift_inv_lref2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀i. T2 = #i → + (i < d ∧ T1 = #i) ∨ (d + e ≤ i ∧ T1 = #(i - e)). +#d #e #T1 #T2 * -d e T1 T2 +[ #k #d #e #i #H destruct +| #j #d #e #Hj #i #Hi destruct /3/ +| #j #d #e #Hj #i #Hi destruct