matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_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/substitution/tps_lift.ma".
  16 include "Basic_2/unfold/tpss.ma".
  17
  18 (* PARTIAL UNFOLD ON TERMS **************************************************)
  19
  20 (* Advanced properties ******************************************************)
  21
  22 lemma tpss_subst: ∀L,K,V,U1,i,d,e.
  23                   d ≤ i → i < d + e →
  24                   ⇓[0, i] L ≡ K. 𝕓{Abbr} V → K ⊢ V [0, d + e - i - 1] ≫* U1 →
  25                   ∀U2. ⇑[0, i + 1] U1 ≡ U2 → L ⊢ #i [d, e] ≫* U2.
  26 #L #K #V #U1 #i #d #e #Hdi #Hide #HLK #H @(tpss_ind … H) -U1
  27 [ /3 width=4/
  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_ldrop2 … HLK) -HLK #HLK
  32   lapply (tps_lift_ge … HU1 … HLK HU0 HU12 ?) -HU1 -HLK -HU0 -HU12 // normalize #HU02
  33   lapply (tps_weak … HU02 d e ? ?) -HU02 [ >minus_plus >commutative_plus /2 width=1/ | /2 width=1/ | /2 width=3/ ]
  34 ]
  35 qed.
  36
  37 (* Advanced inverion lemmas *************************************************)
  38
  39 lemma tpss_inv_atom1: ∀L,T2,I,d,e. L ⊢ 𝕒{I} [d, e] ≫* T2 →
  40                       T2 = 𝕒{I} ∨
  41                       ∃∃K,V1,V2,i. d ≤ i & i < d + e &
  42                                    ⇓[O, i] L ≡ K. 𝕓{Abbr} V1 &
  43                                    K ⊢ V1 [0, d + e - i - 1] ≫* V2 &
  44                                    ⇑[O, i + 1] V2 ≡ T2 &
  45                                    I = LRef i.
  46 #L #T2 #I #d #e #H @(tpss_ind … H) -T2
  47 [ /2 width=1/
  48 | #T #T2 #_ #HT2 *
  49   [ #H destruct
  50     elim (tps_inv_atom1 … HT2) -HT2 [ /2 width=1/ | * /3 width=10/ ]
  51   | * #K #V1 #V #i #Hdi #Hide #HLK #HV1 #HVT #HI
  52     lapply (ldrop_fwd_ldrop2 … HLK) #H
  53     elim (tps_inv_lift1_up … HT2 … H … HVT ? ? ?) normalize -HT2 -H -HVT [2,3,4: /2 width=1/ ] #V2 <minus_plus #HV2 #HVT2
  54     @or_intror @(ex6_4_intro … Hdi Hide HLK … HVT2 HI) /2 width=3/ (**) (* /4 width=10/ is too slow *)
  55   ]
  56 ]
  57 qed-.
  58
  59 lemma tpss_inv_lref1: ∀L,T2,i,d,e. L ⊢ #i [d, e] ≫* T2 →
  60                       T2 = #i ∨
  61                       ∃∃K,V1,V2. d ≤ i & i < d + e &
  62                                  ⇓[O, i] L ≡ K. 𝕓{Abbr} V1 &
  63                                  K ⊢ V1 [0, d + e - i - 1] ≫* V2 &
  64                                  ⇑[O, i + 1] V2 ≡ T2.
  65 #L #T2 #i #d #e #H
  66 elim (tpss_inv_atom1 … H) -H /2 width=1/
  67 * #K #V1 #V2 #j #Hdj #Hjde #HLK #HV12 #HVT2 #H destruct /3 width=6/
  68 qed-.
  69
  70 lemma tpss_inv_refl_SO2: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ≫* T2 →
  71                          ∀K,V. ⇓[0, d] L ≡ K. 𝕓{Abst} V → T1 = T2.
  72 #L #T1 #T2 #d #H #K #V #HLK @(tpss_ind … H) -T2 //
  73 #T #T2 #_ #HT2 #IHT <(tps_inv_refl_SO2 … HT2 … HLK) //
  74 qed-.
  75
  76 (* Relocation properties ****************************************************)
  77
  78 lemma tpss_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫* T2 →
  79                     ∀L,U1,d,e. dt + et ≤ d → ⇓[d, e] L ≡ K →
  80                     ⇑[d, e] T1 ≡ U1 → ∀U2. ⇑[d, e] T2 ≡ U2 →
  81                     L ⊢ U1 [dt, et] ≫* U2.
  82 #K #T1 #T2 #dt #et #H #L #U1 #d #e #Hdetd #HLK #HTU1 @(tpss_ind … H) -T2
  83 [ #U2 #H >(lift_mono … HTU1 … H) -H //
  84 | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
  85   elim (lift_total T d e) #U #HTU
  86   lapply (IHT … HTU) -IHT #HU1
  87   lapply (tps_lift_le … HT2 … HLK HTU HTU2 ?) -HT2 -HLK -HTU -HTU2 // /2 width=3/
  88 ]
  89 qed.
  90
  91 lemma tpss_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫* T2 →
  92                     ∀L,U1,d,e. dt ≤ d → d ≤ dt + et →
  93                     ⇓[d, e] L ≡ K → ⇑[d, e] T1 ≡ U1 →
  94                     ∀U2. ⇑[d, e] T2 ≡ U2 → L ⊢ U1 [dt, et + e] ≫* U2.
  95 #K #T1 #T2 #dt #et #H #L #U1 #d #e #Hdtd #Hddet #HLK #HTU1 @(tpss_ind … H) -T2
  96 [ #U2 #H >(lift_mono … HTU1 … H) -H //
  97 | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
  98   elim (lift_total T d e) #U #HTU
  99   lapply (IHT … HTU) -IHT #HU1
 100   lapply (tps_lift_be … HT2 … HLK HTU HTU2 ? ?) -HT2 -HLK -HTU -HTU2 // /2 width=3/
 101 ]
 102 qed.
 103
 104 lemma tpss_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫* T2 →
 105                     ∀L,U1,d,e. d ≤ dt → ⇓[d, e] L ≡ K →
 106                     ⇑[d, e] T1 ≡ U1 → ∀U2. ⇑[d, e] T2 ≡ U2 →
 107                     L ⊢ U1 [dt + e, et] ≫* U2.
 108 #K #T1 #T2 #dt #et #H #L #U1 #d #e #Hddt #HLK #HTU1 @(tpss_ind … H) -T2
 109 [ #U2 #H >(lift_mono … HTU1 … H) -H //
 110 | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
 111   elim (lift_total T d e) #U #HTU
 112   lapply (IHT … HTU) -IHT #HU1
 113   lapply (tps_lift_ge … HT2 … HLK HTU HTU2 ?) -HT2 -HLK -HTU -HTU2 // /2 width=3/
 114 ]
 115 qed.
 116
 117 lemma tpss_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 →
 118                          ∀K,d,e. ⇓[d, e] L ≡ K → ∀T1. ⇑[d, e] T1 ≡ U1 →
 119                          dt + et ≤ d →
 120                          ∃∃T2. K ⊢ T1 [dt, et] ≫* T2 & ⇑[d, e] T2 ≡ U2.
 121 #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdetd @(tpss_ind … H) -U2
 122 [ /2 width=3/
 123 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
 124   elim (tps_inv_lift1_le … HU2 … HLK … HTU ?) -HU2 -HLK -HTU // /3 width=3/
 125 ]
 126 qed.
 127
 128 lemma tpss_inv_lift1_be: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 →
 129                          ∀K,d,e. ⇓[d, e] L ≡ K → ∀T1. ⇑[d, e] T1 ≡ U1 →
 130                          dt ≤ d → d + e ≤ dt + et →
 131                          ∃∃T2. K ⊢ T1 [dt, et - e] ≫* T2 & ⇑[d, e] T2 ≡ U2.
 132 #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdedet @(tpss_ind … H) -U2
 133 [ /2 width=3/
 134 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
 135   elim (tps_inv_lift1_be … HU2 … HLK … HTU ? ?) -HU2 -HLK -HTU // /3 width=3/
 136 ]
 137 qed.
 138
 139 lemma tpss_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 →
 140                          ∀K,d,e. ⇓[d, e] L ≡ K → ∀T1. ⇑[d, e] T1 ≡ U1 →
 141                          d + e ≤ dt →
 142                          ∃∃T2. K ⊢ T1 [dt - e, et] ≫* T2 & ⇑[d, e] T2 ≡ U2.
 143 #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdedt @(tpss_ind … H) -U2
 144 [ /2 width=3/
 145 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
 146   elim (tps_inv_lift1_ge … HU2 … HLK … HTU ?) -HU2 -HLK -HTU // /3 width=3/
 147 ]
 148 qed.
 149
 150 lemma tpss_inv_lift1_eq: ∀L,U1,U2,d,e.
 151                          L ⊢ U1 [d, e] ≫* U2 → ∀T1. ⇑[d, e] T1 ≡ U1 → U1 = U2.
 152 #L #U1 #U2 #d #e #H #T1 #HTU1 @(tpss_ind … H) -U2 //
 153 #U #U2 #_ #HU2 #IHU destruct
 154 <(tps_inv_lift1_eq … HU2 … HTU1) -HU2 -HTU1 //
 155 qed.
 156
 157 lemma tpss_inv_lift1_be_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 →
 158                             ∀K,d,e. ⇓[d, e] L ≡ K → ∀T1. ⇑[d, e] T1 ≡ U1 →
 159                             dt ≤ d → dt + et ≤ d + e →
 160                             ∃∃T2. K ⊢ T1 [dt, d - dt] ≫* T2 & ⇑[d, e] T2 ≡ U2.
 161 #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdetde @(tpss_ind … H) -U2
 162 [ /2 width=3/
 163 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
 164   elim (tps_inv_lift1_be_up … HU2 … HLK … HTU ? ?) -HU2 -HLK -HTU // /3 width=3/
 165 ]
 166 qed.