matita/matita/contribs/lambdadelta/basic_2/relocation/cny_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/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_lift_inv_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_lift_inv_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_lift_inv_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 properties ******************************************************)
  75
  76 fact cny_subst_aux: ∀G,L,K,V,W,i,d,e. d ≤ yinj i → i < d + e →
  77                     ⇩[i+1] L ≡ K → ⦃G, K⦄ ⊢ ▶[O, ⫰(d+e-i)] 𝐍⦃V⦄ →
  78                     ⇧[O, i+1] V ≡ W → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃W⦄.
  79 #G #L #K #V #W #i #d #e #Hdi #Hide #HLK #HV #HVW
  80 lapply (cny_lift_be … HV … HLK … HVW ? ?) // -HV -HLK -HVW
  81 #HW @(cny_narrow … HW) -HW //
  82 qed-.
  83
  84 lemma cny_subst: ∀I,G,L,K,V,W,i,d,e. d ≤ yinj i → i < d + e →
  85                  ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ ▶[O, ⫰(d+e-i)] 𝐍⦃V⦄ →
  86                  ⇧[O, i+1] V ≡ W → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃W⦄.
  87 /3 width=13 by cny_subst_aux, ldrop_fwd_drop2/ qed-.
  88
  89 (* Advanced inversion lemmas ************************************************)
  90
  91 fact cny_inv_subst_aux: ∀G,L,K,V,W,i,d,e. d ≤ yinj i → i < d + e →
  92                         ⇩[i+1] L ≡ K → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃W⦄ →
  93                         ⇧[O, i+1] V ≡ W → ⦃G, K⦄ ⊢ ▶[O, ⫰(d+e-i)] 𝐍⦃V⦄.
  94 #G #L #K #V #W #i #d #e #Hdi #Hide #HLK #HW #HVW
  95 lapply (cny_narrow … HW (i+1) (⫰(d+e-i)) ? ?) -HW
  96 [ >yplus_SO2 <yplus_succ_swap >ylt_inv_O1
  97   [ >ymax_pre_sn_comm /2 width=2 by ylt_fwd_le/
  98   | lapply (monotonic_ylt_minus_dx … Hide i ?) //
  99   ]
 100 | /2 width=3 by yle_trans/
 101 | #HW lapply (cny_lift_inv_ge … HW … HLK … HVW ?) // -L -W
 102   >yplus_inj >yminus_refl //
 103 ]
 104 qed-.
 105
 106 lemma cny_inv_subst: ∀I,G,L,K,V,W,i,d,e. d ≤ yinj i → i < d + e →
 107                      ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃W⦄ →
 108                      ⇧[O, i+1] V ≡ W →  ⦃G, K⦄ ⊢ ▶[O, ⫰(d+e-i)] 𝐍⦃V⦄.
 109 /3 width=13 by cny_inv_subst_aux, ldrop_fwd_drop2/ qed-.