matita/matita/contribs/lambdadelta/basic_2A/etc_yminus/cpys/cpys_lift.etc

   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 "ground_2/xoa/ex_4_4.ma".
  16 include "ground_2/xoa/ex_6_5.ma".
  17 include "basic_2A/substitution/cpy_lift.ma".
  18 include "basic_2A/multiple/cpys.ma".
  19
  20 (* CONTEXT-SENSITIVE EXTENDED MULTIPLE SUBSTITUTION FOR TERMS ***************)
  21
  22 (* Advanced properties ******************************************************)
  23
  24 lemma cpys_subst: ∀I,G,L,K,V,U1,i,l,m.
  25                   l ≤ yinj i → i < l + m →
  26                   ⬇[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ▶*[0, ↓(l+m-i)] U1 →
  27                   ∀U2. ⬆[0, i+1] U1 ≡ U2 → ⦃G, L⦄ ⊢ #i ▶*[l, m] U2.
  28 #I #G #L #K #V #U1 #i #l #m #Hli #Hilm #HLK #H @(cpys_ind … H) -U1
  29 [ /3 width=5 by cpy_cpys, cpy_subst/
  30 | #U #U1 #_ #HU1 #IHU #U2 #HU12
  31   elim (lift_total U 0 (i+1)) #U0 #HU0
  32   lapply (IHU … HU0) -IHU #H
  33   lapply (drop_fwd_drop2 … HLK) -HLK #HLK
  34   lapply (cpy_lift_ge … HU1 … HLK HU0 HU12 ?) -HU1 -HLK -HU0 -HU12 // #HU02
  35   lapply (cpy_weak … HU02 l m ? ?) -HU02
  36   [2,3: /2 width=3 by cpys_strap1, yle_succ_dx/ ]
  37   >yplus_O1 <yplus_inj >ymax_pre_sn_comm /2 width=1 by ylt_fwd_le_succ/
  38 ]
  39 qed.
  40
  41 lemma cpys_subst_Y2: ∀I,G,L,K,V,U1,i,l.
  42                      l ≤ yinj i →
  43                      ⬇[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ▶*[0, ∞] U1 →
  44                      ∀U2. ⬆[0, i+1] U1 ≡ U2 → ⦃G, L⦄ ⊢ #i ▶*[l, ∞] U2.
  45 #I #G #L #K #V #U1 #i #l #Hli #HLK #HVU1 #U2 #HU12
  46 @(cpys_subst … HLK … HU12) >yminus_Y_inj //
  47 qed.
  48
  49 (* Advanced inversion lemmas *************************************************)
  50
  51 lemma cpys_inv_atom1: ∀I,G,L,T2,l,m. ⦃G, L⦄ ⊢ ⓪{I} ▶*[l, m] T2 →
  52                       T2 = ⓪{I} ∨
  53                       ∃∃J,K,V1,V2,i. l ≤ yinj i & i < l + m &
  54                                     ⬇[i] L ≡ K.ⓑ{J}V1 &
  55                                      ⦃G, K⦄ ⊢ V1 ▶*[0, ↓(l+m-i)] V2 &
  56                                      ⬆[O, i+1] V2 ≡ T2 &
  57                                      I = LRef i.
  58 #I #G #L #T2 #l #m #H @(cpys_ind … H) -T2
  59 [ /2 width=1 by or_introl/
  60 | #T #T2 #_ #HT2 *
  61   [ #H destruct
  62     elim (cpy_inv_atom1 … HT2) -HT2 [ /2 width=1 by or_introl/ | * /3 width=11 by ex6_5_intro, or_intror/ ]
  63   | * #J #K #V1 #V #i #Hli #Hilm #HLK #HV1 #HVT #HI
  64     lapply (drop_fwd_drop2 … HLK) #H
  65     elim (cpy_inv_lift1_ge_up … HT2 … H … HVT) -HT2 -H -HVT
  66     [2,3,4: /2 width=1 by ylt_fwd_le_succ, yle_succ_dx/ ]
  67     /4 width=11 by cpys_strap1, ex6_5_intro, or_intror/
  68   ]
  69 ]
  70 qed-.
  71
  72 lemma cpys_inv_lref1: ∀G,L,T2,i,l,m. ⦃G, L⦄ ⊢ #i ▶*[l, m] T2 →
  73                       T2 = #i ∨
  74                       ∃∃I,K,V1,V2. l ≤ i & i < l + m &
  75                                    ⬇[i] L ≡ K.ⓑ{I}V1 &
  76                                    ⦃G, K⦄ ⊢ V1 ▶*[0, ↓(l+m-i)] V2 &
  77                                    ⬆[O, i+1] V2 ≡ T2.
  78 #G #L #T2 #i #l #m #H elim (cpys_inv_atom1 … H) -H /2 width=1 by or_introl/
  79 * #I #K #V1 #V2 #j #Hlj #Hjlm #HLK #HV12 #HVT2 #H destruct /3 width=7 by ex5_4_intro, or_intror/
  80 qed-.
  81
  82 lemma cpys_inv_lref1_Y2: ∀G,L,T2,i,l. ⦃G, L⦄ ⊢ #i ▶*[l, ∞] T2 →
  83                          T2 = #i ∨
  84                          ∃∃I,K,V1,V2. l ≤ i & ⬇[i] L ≡ K.ⓑ{I}V1 &
  85                                       ⦃G, K⦄ ⊢ V1 ▶*[0, ∞] V2 & ⬆[O, i+1] V2 ≡ T2.
  86 #G #L #T2 #i #l #H elim (cpys_inv_lref1 … H) -H /2 width=1 by or_introl/
  87 * >yminus_Y_inj /3 width=7 by or_intror, ex4_4_intro/
  88 qed-.
  89
  90 lemma cpys_inv_lref1_drop: ∀G,L,T2,i,l,m. ⦃G, L⦄ ⊢ #i ▶*[l, m] T2 →
  91                             ∀I,K,V1. ⬇[i] L ≡ K.ⓑ{I}V1 →
  92                             ∀V2. ⬆[O, i+1] V2 ≡ T2 →
  93                             ∧∧ ⦃G, K⦄ ⊢ V1 ▶*[0, ↓(l+m-i)] V2
  94                              & l ≤ i
  95                              & i < l + m.
  96 #G #L #T2 #i #l #m #H #I #K #V1 #HLK #V2 #HVT2 elim (cpys_inv_lref1 … H) -H
  97 [ #H destruct elim (lift_inv_lref2_be … HVT2) -HVT2 -HLK //
  98 | * #Z #Y #X1 #X2 #Hli #Hilm #HLY #HX12 #HXT2
  99   lapply (lift_inj … HXT2 … HVT2) -T2 #H destruct
 100   lapply (drop_mono … HLY … HLK) -L #H destruct
 101   /2 width=1 by and3_intro/
 102 ]
 103 qed-.
 104
 105 (* Properties on relocation *************************************************)
 106
 107 lemma cpys_lift_le: ∀G,K,T1,T2,lt,mt. ⦃G, K⦄ ⊢ T1 ▶*[lt, mt] T2 →
 108                     ∀L,U1,s,l,m. lt + mt ≤ yinj l → ⬇[s, l, m] L ≡ K →
 109                     ⬆[l, m] T1 ≡ U1 → ∀U2. ⬆[l, m] T2 ≡ U2 →
 110                     ⦃G, L⦄ ⊢ U1 ▶*[lt, mt] U2.
 111 #G #K #T1 #T2 #lt #mt #H #L #U1 #s #l #m #Hlmtl #HLK #HTU1 @(cpys_ind … H) -T2
 112 [ #U2 #H >(lift_mono … HTU1 … H) -H //
 113 | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
 114   elim (lift_total T l m) #U #HTU
 115   lapply (IHT … HTU) -IHT #HU1
 116   lapply (cpy_lift_le … HT2 … HLK HTU HTU2 ?) -HT2 -HLK -HTU -HTU2 /2 width=3 by cpys_strap1/
 117 ]
 118 qed-.
 119
 120 lemma cpys_lift_be: ∀G,K,T1,T2,lt,mt. ⦃G, K⦄ ⊢ T1 ▶*[lt, mt] T2 →
 121                     ∀L,U1,s,l,m. lt ≤ yinj l → l ≤ lt + mt →
 122                     ⬇[s, l, m] L ≡ K → ⬆[l, m] T1 ≡ U1 →
 123                     ∀U2. ⬆[l, m] T2 ≡ U2 → ⦃G, L⦄ ⊢ U1 ▶*[lt, mt + m] U2.
 124 #G #K #T1 #T2 #lt #mt #H #L #U1 #s #l #m #Hltl #Hllmt #HLK #HTU1 @(cpys_ind … H) -T2
 125 [ #U2 #H >(lift_mono … HTU1 … H) -H //
 126 | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
 127   elim (lift_total T l m) #U #HTU
 128   lapply (IHT … HTU) -IHT #HU1
 129   lapply (cpy_lift_be … HT2 … HLK HTU HTU2 ? ?) -HT2 -HLK -HTU -HTU2 /2 width=3 by cpys_strap1/
 130 ]
 131 qed-.
 132
 133 lemma cpys_lift_ge: ∀G,K,T1,T2,lt,mt. ⦃G, K⦄ ⊢ T1 ▶*[lt, mt] T2 →
 134                     ∀L,U1,s,l,m. yinj l ≤ lt → ⬇[s, l, m] L ≡ K →
 135                     ⬆[l, m] T1 ≡ U1 → ∀U2. ⬆[l, m] T2 ≡ U2 →
 136                     ⦃G, L⦄ ⊢ U1 ▶*[lt+m, mt] U2.
 137 #G #K #T1 #T2 #lt #mt #H #L #U1 #s #l #m #Hllt #HLK #HTU1 @(cpys_ind … H) -T2
 138 [ #U2 #H >(lift_mono … HTU1 … H) -H //
 139 | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
 140   elim (lift_total T l m) #U #HTU
 141   lapply (IHT … HTU) -IHT #HU1
 142   lapply (cpy_lift_ge … HT2 … HLK HTU HTU2 ?) -HT2 -HLK -HTU -HTU2 /2 width=3 by cpys_strap1/
 143 ]
 144 qed-.
 145
 146 (* Inversion lemmas for relocation ******************************************)
 147
 148 lemma cpys_inv_lift1_le: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶*[lt, mt] U2 →
 149                          ∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 →
 150                          lt + mt ≤ l →
 151                          ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[lt, mt] T2 & ⬆[l, m] T2 ≡ U2.
 152 #G #L #U1 #U2 #lt #mt #H #K #s #l #m #HLK #T1 #HTU1 #Hlmtl @(cpys_ind … H) -U2
 153 [ /2 width=3 by ex2_intro/
 154 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
 155   elim (cpy_inv_lift1_le … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
 156 ]
 157 qed-.
 158
 159 lemma cpys_inv_lift1_be: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶*[lt, mt] U2 →
 160                          ∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 →
 161                          lt ≤ l → yinj l + m ≤ lt + mt →
 162                          ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[lt, mt - m] T2 & ⬆[l, m] T2 ≡ U2.
 163 #G #L #U1 #U2 #lt #mt #H #K #s #l #m #HLK #T1 #HTU1 #Hltl #Hlmlmt @(cpys_ind … H) -U2
 164 [ /2 width=3 by ex2_intro/
 165 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
 166   elim (cpy_inv_lift1_be … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
 167 ]
 168 qed-.
 169
 170 lemma cpys_inv_lift1_ge: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶*[lt, mt] U2 →
 171                          ∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 →
 172                          yinj l + m ≤ lt →
 173                          ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[lt - m, mt] T2 & ⬆[l, m] T2 ≡ U2.
 174 #G #L #U1 #U2 #lt #mt #H #K #s #l #m #HLK #T1 #HTU1 #Hlmlt @(cpys_ind … H) -U2
 175 [ /2 width=3 by ex2_intro/
 176 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
 177   elim (cpy_inv_lift1_ge … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
 178 ]
 179 qed-.
 180
 181 (* Advanced inversion lemmas on relocation **********************************)
 182
 183 lemma cpys_inv_lift1_ge_up: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶*[lt, mt] U2 →
 184                             ∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 →
 185                             l ≤ lt → lt ≤ yinj l + m → yinj l + m ≤ lt + mt →
 186                             ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[l, lt + mt - (yinj l + m)] T2 &
 187                                  ⬆[l, m] T2 ≡ U2.
 188 #G #L #U1 #U2 #lt #mt #H #K #s #l #m #HLK #T1 #HTU1 #Hllt #Hltlm #Hlmlmt @(cpys_ind … H) -U2
 189 [ /2 width=3 by ex2_intro/
 190 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
 191   elim (cpy_inv_lift1_ge_up … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
 192 ]
 193 qed-.
 194
 195 lemma cpys_inv_lift1_be_up: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶*[lt, mt] U2 →
 196                             ∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 →
 197                             lt ≤ l → lt + mt ≤ yinj l + m →
 198                             ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[lt, l - lt] T2 & ⬆[l, m] T2 ≡ U2.
 199 #G #L #U1 #U2 #lt #mt #H #K #s #l #m #HLK #T1 #HTU1 #Hltl #Hlmtlm @(cpys_ind … H) -U2
 200 [ /2 width=3 by ex2_intro/
 201 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
 202   elim (cpy_inv_lift1_be_up … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
 203 ]
 204 qed-.
 205
 206 lemma cpys_inv_lift1_le_up: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶*[lt, mt] U2 →
 207                             ∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 →
 208                             lt ≤ l → l ≤ lt + mt → lt + mt ≤ yinj l + m →
 209                             ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[lt, l - lt] T2 & ⬆[l, m] T2 ≡ U2.
 210 #G #L #U1 #U2 #lt #mt #H #K #s #l #m #HLK #T1 #HTU1 #Hltl #Hllmt #Hlmtlm @(cpys_ind … H) -U2
 211 [ /2 width=3 by ex2_intro/
 212 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
 213   elim (cpy_inv_lift1_le_up … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
 214 ]
 215 qed-.
 216
 217 lemma cpys_inv_lift1_subst: ∀G,L,W1,W2,l,m. ⦃G, L⦄ ⊢ W1 ▶*[l, m] W2 →
 218                             ∀K,V1,i. ⬇[i+1] L ≡ K → ⬆[O, i+1] V1 ≡ W1 →
 219                             l ≤ yinj i → i < l + m →
 220                             ∃∃V2.  ⦃G, K⦄ ⊢ V1 ▶*[O, ↓(l+m-i)] V2 & ⬆[O, i+1] V2 ≡ W2.
 221 #G #L #W1 #W2 #l #m #HW12 #K #V1 #i #HLK #HVW1 #Hli #Hilm
 222 elim (cpys_inv_lift1_ge_up … HW12 … HLK … HVW1 ? ? ?) //
 223 >yplus_O1 <yplus_inj >yplus_SO2
 224 [ >yminus_succ2 /2 width=3 by ex2_intro/
 225 | /2 width=1 by ylt_fwd_le_succ1/
 226 | /2 width=3 by yle_trans/
 227 ]
 228 qed-.