matita/matita/contribs/lambda_delta/basic_2/unfold/delift_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/unfold/tpss_lift.ma".
  16 include "basic_2/unfold/delift.ma".
  17
  18 (* INVERSE BASIC TERM RELOCATION  *******************************************)
  19
  20 (* Advanced properties ******************************************************)
  21
  22 lemma delift_lref_be: ∀L,K,V1,V2,U2,i,d,e. d ≤ i → i < d + e →
  23                       ⇩[0, i] L ≡ K. ⓓV1 → K ⊢ V1 ▼*[0, d + e - i - 1] ≡ V2 →
  24                       ⇧[0, d] V2 ≡ U2 → L ⊢ #i ▼*[d, e] ≡ U2.
  25 #L #K #V1 #V2 #U2 #i #d #e #Hdi #Hide #HLK * #V #HV1 #HV2 #HVU2
  26 elim (lift_total V 0 (i+1)) #U #HVU
  27 lapply (lift_trans_be … HV2 … HVU ? ?) -HV2 // >minus_plus <plus_minus_m_m /2 width=1/ #HV2U
  28 lapply (lift_conf_be … HVU2 … HV2U ?) //
  29 >commutative_plus in ⊢ (??%??→?); <minus_plus_m_m /3 width=6/
  30 qed.
  31
  32 (* Advanced inversion lemmas ************************************************)
  33
  34 lemma delift_inv_lref1_lt: ∀L,U2,i,d,e. L ⊢ #i ▼*[d, e] ≡ U2 → i < d → U2 = #i.
  35 #L #U2 #i #d #e * #U #HU #HU2 #Hid
  36 elim (tpss_inv_lref1 … HU) -HU
  37 [ #H destruct >(lift_inv_lref2_lt … HU2) //
  38 | * #K #V1 #V2 #Hdi
  39   lapply (lt_to_le_to_lt … Hid Hdi) -Hid -Hdi #Hi
  40   elim (lt_refl_false … Hi)
  41 ]
  42 qed-.
  43
  44 lemma delift_inv_lref1_be: ∀L,U2,d,e,i. L ⊢ #i ▼*[d, e] ≡ U2 →
  45                            d ≤ i → i < d + e →
  46                            ∃∃K,V1,V2. ⇩[0, i] L ≡ K. ⓓV1 &
  47                                       K ⊢ V1 ▼*[0, d + e - i - 1] ≡ V2 &
  48                                       ⇧[0, d] V2 ≡ U2.
  49 #L #U2 #d #e #i * #U #HU #HU2 #Hdi #Hide
  50 elim (tpss_inv_lref1 … HU) -HU
  51 [ #H destruct elim (lift_inv_lref2_be … HU2 ? ?) //
  52 | * #K #V1 #V #_ #_ #HLK #HV1 #HVU
  53   elim (lift_div_be … HVU … HU2 ? ?) -U // /2 width=1/ /3 width=6/
  54 ]
  55 qed-.
  56
  57 lemma delift_inv_lref1_ge: ∀L,U2,i,d,e. L ⊢ #i ▼*[d, e] ≡ U2 →
  58                            d + e ≤ i → U2 = #(i - e).
  59 #L #U2 #i #d #e * #U #HU #HU2 #Hdei
  60 elim (tpss_inv_lref1 … HU) -HU
  61 [ #H destruct >(lift_inv_lref2_ge … HU2) //
  62 | * #K #V1 #V2 #_ #Hide
  63   lapply (lt_to_le_to_lt … Hide Hdei) -Hide -Hdei #Hi
  64   elim (lt_refl_false … Hi)
  65 ]
  66 qed-.
  67
  68 lemma delift_inv_lref1: ∀L,U2,i,d,e. L ⊢ #i ▼*[d, e] ≡ U2 →
  69                         ∨∨ (i < d ∧ U2 = #i)
  70                         |  (∃∃K,V1,V2. d ≤ i & i < d + e &
  71                                        ⇩[0, i] L ≡ K. ⓓV1 &
  72                                        K ⊢ V1 ▼*[0, d + e - i - 1] ≡ V2 &
  73                                        ⇧[0, d] V2 ≡ U2
  74                            )
  75                         |  (d + e ≤ i ∧ U2 = #(i - e)).
  76 #L #U2 #i #d #e #H
  77 elim (lt_or_ge i d) #Hdi
  78 [ elim (delift_inv_lref1_lt … H Hdi) -H /3 width=1/
  79 | elim (lt_or_ge i (d+e)) #Hide
  80   [ elim (delift_inv_lref1_be … H Hdi Hide) -H /3 width=6/
  81   | elim (delift_inv_lref1_ge … H Hide) -H /3 width=1/
  82   ]
  83 ]
  84 qed-.
  85
  86 (* Properties on basic term relocation **************************************)
  87
  88 lemma delift_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 ▼*[dt, et] ≡ T2 →
  89                       ∀L,U1,d,e. dt + et ≤ d → ⇩[d, e] L ≡ K →
  90                       ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d - et, e] T2 ≡ U2 →
  91                       L ⊢ U1 ▼*[dt, et] ≡ U2.
  92 #K #T1 #T2 #dt #et * #T #HT1 #HT2 #L #U1 #d #e #Hdetd #HLK #HTU1 #U2 #HTU2
  93 elim (lift_total T d e) #U #HTU
  94 lapply (tpss_lift_le … HT1 … HLK HTU1 … HTU) -T1 -HLK // #HU1
  95 elim (lift_trans_ge … HT2 … HTU ?) -T // -Hdetd #T #HT2 #HTU
  96 >(lift_mono … HTU2 … HT2) -T2 /2 width=3/
  97 qed.
  98
  99 lemma delift_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 ▼*[dt, et] ≡ T2 →
 100                       ∀L,U1,d,e. dt ≤ d → d ≤ dt + et →
 101                       ⇩[d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 →
 102                       L ⊢ U1 ▼*[dt, et + e] ≡ T2.
 103 #K #T1 #T2 #dt #et * #T #HT1 #HT2 #L #U1 #d #e #Hdtd #Hddet #HLK #HTU1
 104 elim (lift_total T d e) #U #HTU
 105 lapply (tpss_lift_be … HT1 … HLK HTU1 … HTU) -T1 -HLK // #HU1
 106 lapply (lift_trans_be … HT2 … HTU ? ?) -T // -Hdtd -Hddet /2 width=3/
 107 qed.
 108
 109 lemma delift_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 ▼*[dt, et] ≡ T2 →
 110                       ∀L,U1,d,e. d ≤ dt → ⇩[d, e] L ≡ K →
 111                       ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 →
 112                       L ⊢ U1 ▼*[dt + e, et] ≡ U2.
 113 #K #T1 #T2 #dt #et * #T #HT1 #HT2 #L #U1 #d #e #Hddt #HLK #HTU1 #U2 #HTU2
 114 elim (lift_total T d e) #U #HTU
 115 lapply (tpss_lift_ge … HT1 … HLK HTU1 … HTU) -T1 -HLK // #HU1
 116 elim (lift_trans_le … HT2 … HTU ?) -T // -Hddt #T #HT2 #HTU
 117 >(lift_mono … HTU2 … HT2) -T2 /2 width=3/
 118 qed.
 119
 120 lemma delift_inv_lift1_eq: ∀L,U1,T2,d,e. L ⊢ U1 ▼*[d, e] ≡ T2 →
 121                            ∀K. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → T1 = T2.
 122 #L #U1 #T2 #d #e * #U2 #HU12 #HTU2 #K #HLK #T1 #HTU1
 123 lapply (tpss_inv_lift1_eq … HU12 … HTU1) -L -K #H destruct
 124 lapply (lift_inj … HTU1 … HTU2) -U2 //
 125 qed-.
 126
 127 lemma delift_lift_div_be: ∀L,T1,T,d,e,i. L ⊢ T1 ▼*[i, d + e - i] ≡ T →
 128                           ∀T2. ⇧[d, i - d] T2 ≡ T → d ≤ i → i ≤ d + e →
 129                           L ⊢ T1 ▼*[d, e] ≡ T2.
 130 #L #T1 #T #d #e #i * #T0 #HT10 #HT0 #T2 #HT2 #Hdi #Hide
 131 lapply (tpss_weak … HT10 d e ? ?) -HT10 // [ >commutative_plus /2 width=1/ ] #HT10
 132 lapply (lift_trans_be … HT2 … HT0 ? ?) -T //
 133 >commutative_plus >commutative_plus in ⊢ (? ? (? % ?) ? ? → ?);
 134 <minus_le_minus_minus_comm // <plus_minus_m_m [ /2 width=3/ | /2 width=1/ ]
 135 qed.