matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "basic_2/relocation/cpy_lift.ma".
  16 include "basic_2/substitution/cpys.ma".
  17
  18 (* CONTEXT-SENSITIVE EXTENDED MULTIPLE SUBSTITUTION FOR TERMS ***************)
  19
  20 (* Advanced properties ******************************************************)
  21
  22 lemma cpys_subst: ∀I,G,L,K,V,U1,i,d,e.
  23                   d ≤ yinj i → i < d + e →
  24                   ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ▶*[0, ⫰(d+e-i)] U1 →
  25                   ∀U2. ⇧[0, i+1] U1 ≡ U2 → ⦃G, L⦄ ⊢ #i ▶*[d, e] U2.
  26 #I #G #L #K #V #U1 #i #d #e #Hdi #Hide #HLK #H @(cpys_ind … H) -U1
  27 [ /3 width=5 by cpy_cpys, cpy_subst/
  28 | #U #U1 #_ #HU1 #IHU #U2 #HU12
  29   elim (lift_total U 0 (i+1)) #U0 #HU0
  30   lapply (IHU … HU0) -IHU #H
  31   lapply (ldrop_fwd_drop2 … HLK) -HLK #HLK
  32   lapply (cpy_lift_ge … HU1 … HLK HU0 HU12 ?) -HU1 -HLK -HU0 -HU12 // #HU02
  33   lapply (cpy_weak … HU02 d e ? ?) -HU02
  34   [2,3: /2 width=3 by cpys_strap1, yle_succ_dx/ ]
  35   >yplus_O1 <yplus_inj >ymax_pre_sn_comm /2 width=1 by ylt_fwd_le_succ/
  36 ]
  37 qed.
  38
  39 lemma cpys_subst_Y2: ∀I,G,L,K,V,U1,i,d.
  40                      d ≤ yinj i →
  41                      ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ▶*[0, ∞] U1 →
  42                      ∀U2. ⇧[0, i+1] U1 ≡ U2 → ⦃G, L⦄ ⊢ #i ▶*[d, ∞] U2.
  43 #I #G #L #K #V #U1 #i #d #Hdi #HLK #HVU1 #U2 #HU12
  44 @(cpys_subst … HLK … HU12) >yminus_Y_inj //
  45 qed.
  46
  47 (* Advanced inverion lemmas *************************************************)
  48
  49 lemma cpys_inv_atom1: ∀I,G,L,T2,d,e. ⦃G, L⦄ ⊢ ⓪{I} ▶*[d, e] T2 →
  50                       T2 = ⓪{I} ∨
  51                       ∃∃J,K,V1,V2,i. d ≤ yinj i & i < d + e &
  52                                     ⇩[i] L ≡ K.ⓑ{J}V1 &
  53                                      ⦃G, K⦄ ⊢ V1 ▶*[0, ⫰(d+e-i)] V2 &
  54                                      ⇧[O, i+1] V2 ≡ T2 &
  55                                      I = LRef i.
  56 #I #G #L #T2 #d #e #H @(cpys_ind … H) -T2
  57 [ /2 width=1 by or_introl/
  58 | #T #T2 #_ #HT2 *
  59   [ #H destruct
  60     elim (cpy_inv_atom1 … HT2) -HT2 [ /2 width=1 by or_introl/ | * /3 width=11 by ex6_5_intro, or_intror/ ]
  61   | * #J #K #V1 #V #i #Hdi #Hide #HLK #HV1 #HVT #HI
  62     lapply (ldrop_fwd_drop2 … HLK) #H
  63     elim (cpy_inv_lift1_ge_up … HT2 … H … HVT) -HT2 -H -HVT
  64     [2,3,4: /2 width=1 by ylt_fwd_le_succ, yle_succ_dx/ ]
  65     /4 width=11 by cpys_strap1, ex6_5_intro, or_intror/
  66   ]
  67 ]
  68 qed-.
  69
  70 lemma cpys_inv_lref1: ∀G,L,T2,i,d,e. ⦃G, L⦄ ⊢ #i ▶*[d, e] T2 →
  71                       T2 = #i ∨
  72                       ∃∃I,K,V1,V2. d ≤ i & i < d + e &
  73                                    ⇩[i] L ≡ K.ⓑ{I}V1 &
  74                                    ⦃G, K⦄ ⊢ V1 ▶*[0, ⫰(d+e-i)] V2 &
  75                                    ⇧[O, i+1] V2 ≡ T2.
  76 #G #L #T2 #i #d #e #H elim (cpys_inv_atom1 … H) -H /2 width=1 by or_introl/
  77 * #I #K #V1 #V2 #j #Hdj #Hjde #HLK #HV12 #HVT2 #H destruct /3 width=7 by ex5_4_intro, or_intror/
  78 qed-.
  79
  80 lemma cpys_inv_lref1_ldrop: ∀G,L,T2,i,d,e. ⦃G, L⦄ ⊢ #i ▶*[d, e] T2 →
  81                             ∀I,K,V1. ⇩[i] L ≡ K.ⓑ{I}V1 →
  82                             ∀V2. ⇧[O, i+1] V2 ≡ T2 →
  83                             ∧∧ ⦃G, K⦄ ⊢ V1 ▶*[0, ⫰(d+e-i)] V2
  84                              & d ≤ i
  85                              & i < d + e.
  86 #G #L #T2 #i #d #e #H #I #K #V1 #HLK #V2 #HVT2 elim (cpys_inv_lref1 … H) -H
  87 [ #H destruct elim (lift_inv_lref2_be … HVT2) -HVT2 -HLK //
  88 | * #Z #Y #X1 #X2 #Hdi #Hide #HLY #HX12 #HXT2
  89   lapply (lift_inj … HXT2 … HVT2) -T2 #H destruct
  90   lapply (ldrop_mono … HLY … HLK) -L #H destruct
  91   /2 width=1 by and3_intro/
  92 ]
  93 qed-.
  94
  95 (* Properties on relocation *************************************************)
  96
  97 lemma cpys_lift_le: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*[dt, et] T2 →
  98                     ∀L,U1,s,d,e. dt + et ≤ yinj d → ⇩[s, d, e] L ≡ K →
  99                     ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 →
 100                     ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2.
 101 #G #K #T1 #T2 #dt #et #H #L #U1 #s #d #e #Hdetd #HLK #HTU1 @(cpys_ind … H) -T2
 102 [ #U2 #H >(lift_mono … HTU1 … H) -H //
 103 | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
 104   elim (lift_total T d e) #U #HTU
 105   lapply (IHT … HTU) -IHT #HU1
 106   lapply (cpy_lift_le … HT2 … HLK HTU HTU2 ?) -HT2 -HLK -HTU -HTU2 /2 width=3 by cpys_strap1/
 107 ]
 108 qed-.
 109
 110 lemma cpys_lift_be: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*[dt, et] T2 →
 111                     ∀L,U1,s,d,e. dt ≤ yinj d → d ≤ dt + et →
 112                     ⇩[s, d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 →
 113                     ∀U2. ⇧[d, e] T2 ≡ U2 → ⦃G, L⦄ ⊢ U1 ▶*[dt, et + e] U2.
 114 #G #K #T1 #T2 #dt #et #H #L #U1 #s #d #e #Hdtd #Hddet #HLK #HTU1 @(cpys_ind … H) -T2
 115 [ #U2 #H >(lift_mono … HTU1 … H) -H //
 116 | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
 117   elim (lift_total T d e) #U #HTU
 118   lapply (IHT … HTU) -IHT #HU1
 119   lapply (cpy_lift_be … HT2 … HLK HTU HTU2 ? ?) -HT2 -HLK -HTU -HTU2 /2 width=3 by cpys_strap1/
 120 ]
 121 qed-.
 122
 123 lemma cpys_lift_ge: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*[dt, et] T2 →
 124                     ∀L,U1,s,d,e. yinj d ≤ dt → ⇩[s, d, e] L ≡ K →
 125                     ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 →
 126                     ⦃G, L⦄ ⊢ U1 ▶*[dt+e, et] U2.
 127 #G #K #T1 #T2 #dt #et #H #L #U1 #s #d #e #Hddt #HLK #HTU1 @(cpys_ind … H) -T2
 128 [ #U2 #H >(lift_mono … HTU1 … H) -H //
 129 | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
 130   elim (lift_total T d e) #U #HTU
 131   lapply (IHT … HTU) -IHT #HU1
 132   lapply (cpy_lift_ge … HT2 … HLK HTU HTU2 ?) -HT2 -HLK -HTU -HTU2 /2 width=3 by cpys_strap1/
 133 ]
 134 qed-.
 135
 136 (* Inversion lemmas for relocation ******************************************)
 137
 138 lemma cpys_inv_lift1_le: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2 →
 139                          ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
 140                          dt + et ≤ d →
 141                          ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[dt, et] T2 & ⇧[d, e] T2 ≡ U2.
 142 #G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hdetd @(cpys_ind … H) -U2
 143 [ /2 width=3 by ex2_intro/
 144 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
 145   elim (cpy_inv_lift1_le … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
 146 ]
 147 qed-.
 148
 149 lemma cpys_inv_lift1_be: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2 →
 150                          ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
 151                          dt ≤ d → yinj d + e ≤ dt + et →
 152                          ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[dt, et - e] T2 & ⇧[d, e] T2 ≡ U2.
 153 #G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hdtd #Hdedet @(cpys_ind … H) -U2
 154 [ /2 width=3 by ex2_intro/
 155 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
 156   elim (cpy_inv_lift1_be … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
 157 ]
 158 qed-.
 159
 160 lemma cpys_inv_lift1_ge: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2 →
 161                          ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
 162                          yinj d + e ≤ dt →
 163                          ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[dt - e, et] T2 & ⇧[d, e] T2 ≡ U2.
 164 #G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hdedt @(cpys_ind … H) -U2
 165 [ /2 width=3 by ex2_intro/
 166 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
 167   elim (cpy_inv_lift1_ge … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
 168 ]
 169 qed-.
 170
 171 (* Advanced inversion lemmas on relocation **********************************)
 172
 173 lemma cpys_inv_lift1_ge_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2 →
 174                             ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
 175                             d ≤ dt → dt ≤ yinj d + e → yinj d + e ≤ dt + et →
 176                             ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[d, dt + et - (yinj d + e)] T2 &
 177                                  ⇧[d, e] T2 ≡ U2.
 178 #G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet @(cpys_ind … H) -U2
 179 [ /2 width=3 by ex2_intro/
 180 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
 181   elim (cpy_inv_lift1_ge_up … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
 182 ]
 183 qed-.
 184
 185 lemma cpys_inv_lift1_be_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2 →
 186                             ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
 187                             dt ≤ d → dt + et ≤ yinj d + e →
 188                             ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[dt, d - dt] T2 & ⇧[d, e] T2 ≡ U2.
 189 #G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hdtd #Hdetde @(cpys_ind … H) -U2
 190 [ /2 width=3 by ex2_intro/
 191 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
 192   elim (cpy_inv_lift1_be_up … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
 193 ]
 194 qed-.
 195
 196 lemma cpys_inv_lift1_le_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2 →
 197                             ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
 198                             dt ≤ d → d ≤ dt + et → dt + et ≤ yinj d + e →
 199                             ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[dt, d - dt] T2 & ⇧[d, e] T2 ≡ U2.
 200 #G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hdtd #Hddet #Hdetde @(cpys_ind … H) -U2
 201 [ /2 width=3 by ex2_intro/
 202 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
 203   elim (cpy_inv_lift1_le_up … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
 204 ]
 205 qed-.
 206
 207 lemma cpys_inv_lift1_subst: ∀G,L,W1,W2,d,e. ⦃G, L⦄ ⊢ W1 ▶*[d, e] W2 →
 208                             ∀K,V1,i. ⇩[i+1] L ≡ K → ⇧[O, i+1] V1 ≡ W1 →
 209                             d ≤ yinj i → i < d + e →
 210                             ∃∃V2.  ⦃G, K⦄ ⊢ V1 ▶*[O, ⫰(d+e-i)] V2 & ⇧[O, i+1] V2 ≡ W2.
 211 #G #L #W1 #W2 #d #e #HW12 #K #V1 #i #HLK #HVW1 #Hdi #Hide
 212 elim (cpys_inv_lift1_ge_up … HW12 … HLK … HVW1 ? ? ?) //
 213 >yplus_O1 <yplus_inj >yplus_SO2
 214 [ >yminus_succ2 /2 width=3 by ex2_intro/
 215 | /2 width=1 by ylt_fwd_le_succ1/
 216 | /2 width=3 by yle_trans/
 217 ]
 218 qed-.