matita/matita/contribs/lambdadelta/basic_2/etc_2A1/cny/cny_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 "basic_2/relocation/cpy_lift.ma".
  16 include "basic_2/relocation/cny.ma".
  17
  18 (* NORMAL TERMS FOR CONTEXT-SENSITIVE EXTENDED SUBSTITUTION *****************)
  19
  20 (* Properties on relocation *************************************************)
  21
  22 lemma cny_lift_le: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, K⦄ ⊢ ▶[dt, et] 𝐍⦃T⦄ → ⇩[s, d, e] L ≡ K →
  23                    ⇧[d, e] T ≡ U → dt + et ≤ d → ⦃G, L⦄ ⊢ ▶[dt, et] 𝐍⦃U⦄.
  24 #G #L #K #T1 #U1 #s #d #dt #e #et #HT1 #HLK #HTU1 #Hdetd #U2 #HU12
  25 elim (cpy_inv_lift1_le … HU12 … HLK … HTU1) // -L -Hdetd #T2 #HT12
  26 >(HT1 … HT12) -K /2 width=5 by lift_mono/
  27 qed-.
  28
  29 lemma cny_lift_be: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, K⦄ ⊢ ▶[dt, et] 𝐍⦃T⦄ → ⇩[s, d, e] L ≡ K →
  30                    ⇧[d, e] T ≡ U → dt ≤ d → yinj d ≤ dt + et → ⦃G, L⦄ ⊢ ▶[dt, et+e] 𝐍⦃U⦄.
  31 #G #L #K #T1 #U1 #s #d #dt #e #et #HT1 #HLK #HTU1 #Hdtd #Hddet #U2 #HU12
  32 elim (cpy_inv_lift1_be … HU12 … HLK … HTU1) /2 width=1 by monotonic_yle_plus_dx/ -L -Hdtd -Hddet #T2
  33 >yplus_minus_inj #HT12 >(HT1 … HT12) -K /2 width=5 by lift_mono/
  34 qed-.
  35
  36 lemma cny_lift_ge: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, K⦄ ⊢ ▶[dt, et] 𝐍⦃T⦄ → ⇩[s, d, e] L ≡ K →
  37                    ⇧[d, e] T ≡ U → d ≤ dt → ⦃G, L⦄ ⊢ ▶[dt+e, et] 𝐍⦃U⦄.
  38 #G #L #K #T1 #U1 #s #d #dt #e #et #HT1 #HLK #HTU1 #Hddt #U2 #HU12
  39 elim (cpy_inv_lift1_ge … HU12 … HLK … HTU1) /2 width=1 by monotonic_yle_plus_dx/ -L -Hddt #T2
  40 >yplus_minus_inj #HT12 >(HT1 … HT12) -K /2 width=5 by lift_mono/
  41 qed-.
  42
  43 (* Inversion lemmas on relocation *******************************************)
  44
  45 lemma cny_inv_lift_le: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, L⦄ ⊢ ▶[dt, et] 𝐍⦃U⦄ → ⇩[s, d, e] L ≡ K →
  46                        ⇧[d, e] T ≡ U → dt + et ≤ d → ⦃G, K⦄ ⊢ ▶[dt, et] 𝐍⦃T⦄.
  47 #G #L #K #T1 #U1 #s #d #dt #e #et #HU1 #HLK #HTU1 #Hdetd #T2 #HT12
  48 elim (lift_total T2 d e) #U2 #HTU2
  49 lapply (cpy_lift_le … HT12 … HLK … HTU1 … HTU2 ?) // -K -Hdetd #HU12
  50 lapply (HU1 … HU12) -L /2 width=5 by lift_inj/
  51 qed-.
  52
  53 lemma cny_inv_lift_be: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, L⦄ ⊢ ▶[dt, et] 𝐍⦃U⦄ → ⇩[s, d, e] L ≡ K →
  54                        ⇧[d, e] T ≡ U → dt ≤ d → yinj d + e ≤ dt + et → ⦃G, K⦄ ⊢ ▶[dt, et-e] 𝐍⦃T⦄.
  55 #G #L #K #T1 #U1 #s #d #dt #e #et #HU1 #HLK #HTU1 #Hdtd #Hdedet #T2 #HT12
  56 lapply (yle_fwd_plus_ge_inj … Hdedet) // #Heet
  57 elim (yle_inv_plus_inj2 … Hdedet) -Hdedet #Hddete #Hedet
  58 elim (lift_total T2 d e) #U2 #HTU2
  59 lapply (cpy_lift_be … HT12 … HLK … HTU1 … HTU2 ? ?) // [ >yplus_minus_assoc_inj // ] -K -Hdtd -Hddete
  60 >ymax_pre_sn // -Heet #HU12
  61 lapply (HU1 … HU12) -L /2 width=5 by lift_inj/
  62 qed-.
  63
  64 lemma cny_inv_lift_ge: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, L⦄ ⊢ ▶[dt, et] 𝐍⦃U⦄ → ⇩[s, d, e] L ≡ K →
  65                        ⇧[d, e] T ≡ U → yinj d + e ≤ dt → ⦃G, K⦄ ⊢ ▶[dt-e, et] 𝐍⦃T⦄.
  66 #G #L #K #T1 #U1 #s #d #dt #e #et #HU1 #HLK #HTU1 #Hdedt #T2 #HT12
  67 elim (yle_inv_plus_inj2 … Hdedt) -Hdedt #Hddte #Hedt
  68 elim (lift_total T2 d e) #U2 #HTU2
  69 lapply (cpy_lift_ge … HT12 … HLK … HTU1 … HTU2 ?) // -K -Hddte
  70 >ymax_pre_sn // -Hedt #HU12
  71 lapply (HU1 … HU12) -L /2 width=5 by lift_inj/
  72 qed-.
  73
  74 (* Advanced inversion lemmas on relocation **********************************)
  75
  76 lemma cny_inv_lift_ge_up: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, L⦄ ⊢ ▶[dt, et] 𝐍⦃U⦄ → ⇩[s, d, e] L ≡ K →
  77                           ⇧[d, e] T ≡ U → d ≤ dt → dt ≤ yinj d + e → yinj d + e ≤ dt + et →
  78                           ⦃G, K⦄ ⊢ ▶[d, dt + et - (yinj d + e)] 𝐍⦃T⦄.
  79 #G #L #K #T1 #U1 #s #d #dt #e #et #HU1 #HLK #HTU1 #Hddt #Hdtde #Hdedet
  80 lapply (cny_narrow … HU1 (d+e) (dt+et-(d+e)) ? ?) -HU1 [ >ymax_pre_sn_comm ] // #HU1
  81 lapply (cny_inv_lift_ge … HU1 … HLK … HTU1 ?) // -L -U1
  82 >yplus_minus_inj //
  83 qed-.
  84
  85 lemma cny_inv_lift_subst: ∀G,L,K,V,W,i,d,e. d ≤ yinj i → i < d + e →
  86                           ⇩[i+1] L ≡ K → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃W⦄ →
  87                           ⇧[O, i+1] V ≡ W → ⦃G, K⦄ ⊢ ▶[O, ⫰(d+e-i)] 𝐍⦃V⦄.
  88 #G #L #K #V #W #i #d #e #Hdi #Hide #HLK #HW #HVW
  89 lapply (cny_inv_lift_ge_up … HW … HLK … HVW ? ? ?) //
  90 >yplus_O1 <yplus_inj >yplus_SO2
  91 [ /2 width=1 by ylt_fwd_le_succ1/
  92 | /2 width=3 by yle_trans/
  93 | >yminus_succ2 //
  94 ]
  95 qed-.
  96
  97 (* Advanced properties ******************************************************)
  98
  99 (* Note: this should be applicable in a forward manner *)
 100 lemma cny_lift_ge_up: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, K⦄ ⊢ ▶[yinj d, dt + et - (yinj d + yinj e)] 𝐍⦃T⦄ →
 101                       ⇩[s, d, e] L ≡ K → ⇧[d, e] T ≡ U →
 102                       yinj d ≤ dt → dt ≤ yinj d + yinj e → yinj d + yinj e ≤ dt + et →
 103                       ⦃G, L⦄ ⊢ ▶[dt, et] 𝐍⦃U⦄.
 104 #G #L #K #T1 #U1 #s #d #dt #e #et #HT1 #HLK #HTU1 #Hddt #Hdtde #Hdedet
 105 lapply (cny_lift_be … HT1 … HLK … HTU1 ? ?) // -K -T1
 106 #HU1 @(cny_narrow … HU1) -HU1 // (**) (* auto fails *)
 107 qed-.
 108
 109 lemma cny_lift_subst: ∀G,L,K,V,W,i,d,e. d ≤ yinj i → i < d + e →
 110                       ⇩[i+1] L ≡ K → ⦃G, K⦄ ⊢ ▶[O, ⫰(d+e-i)] 𝐍⦃V⦄ →
 111                       ⇧[O, i+1] V ≡ W → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃W⦄.
 112 #G #L #K #V #W #i #d #e #Hdi #Hide #HLK #HV #HVW
 113 @(cny_lift_ge_up … HLK … HVW) // >yplus_O1 <yplus_inj >yplus_SO2
 114 [ >yminus_succ2 //
 115 | /2 width=3 by yle_trans/
 116 | /2 width=1 by ylt_fwd_le_succ1/
 117 ]
 118 qed-.