matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.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/lleq_ldrop.ma".
  16 include "basic_2/computation/lpxs_ldrop.ma".
  17 include "basic_2/computation/lsx.ma".
  18
  19 (* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
  20
  21 (* Advanced properties ******************************************************)
  22
  23 lemma lsx_lref_free: ∀h,g,G,L,d,i. |L| ≤ i → G ⊢ ⋕⬊*[h, g, #i, d] L.
  24 #h #g #G #L1 #d #i #HL1 @lsx_intro
  25 #L2 #HL12 #H elim H -H
  26 /4 width=6 by lpxs_fwd_length, lleq_free, le_repl_sn_conf_aux/
  27 qed.
  28
  29 lemma lsx_lref_skip: ∀h,g,G,L,d,i. yinj i < d → G ⊢ ⋕⬊*[h, g, #i, d] L.
  30 #h #g #G #L1 #d #i #HL1 @lsx_intro
  31 #L2 #HL12 #H elim H -H
  32 /3 width=4 by lpxs_fwd_length, lleq_skip/
  33 qed.
  34
  35 (* Properties on relocation *************************************************)
  36
  37 lemma lsx_lift_le: ∀h,g,G,K,T,U,dt,d,e. dt ≤ yinj d →
  38                    ⇧[d, e] T ≡ U → G ⊢ ⋕⬊*[h, g, T, dt] K →
  39                    ∀L. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⋕⬊*[h, g, U, dt] L.
  40 #h #g #G #K #T #U #dt #d #e #Hdtd #HTU #H @(lsx_ind … H) -K
  41 #K1 #_ #IHK1 #L1 #HLK1 @lsx_intro
  42 #L2 #HL12 #HnU elim (lpxs_ldrop_conf … HLK1 … HL12) -HL12
  43 /4 width=10 by lleq_lift_le/
  44 qed-.
  45
  46 lemma lsx_lift_ge: ∀h,g,G,K,T,U,dt,d,e. yinj d ≤ dt →
  47                    ⇧[d, e] T ≡ U → G ⊢ ⋕⬊*[h, g, T, dt] K →
  48                    ∀L. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⋕⬊*[h, g, U, dt + e] L.
  49 #h #g #G #K #T #U #dt #d #e #Hddt #HTU #H @(lsx_ind … H) -K
  50 #K1 #_ #IHK1 #L1 #HLK1 @lsx_intro
  51 #L2 #HL12 #HnU elim (lpxs_ldrop_conf … HLK1 … HL12) -HL12
  52 /4 width=9 by lleq_lift_ge/
  53 qed-.
  54
  55 (* Inversion lemmas on relocation *******************************************)
  56
  57 lemma lsx_inv_lift_le: ∀h,g,G,L,T,U,dt,d,e. dt ≤ yinj d →
  58                        ⇧[d, e] T ≡ U → G ⊢ ⋕⬊*[h, g, U, dt] L →
  59                        ∀K. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⋕⬊*[h, g, T, dt] K.
  60 #h #g #G #L #T #U #dt #d #e #Hdtd #HTU #H @(lsx_ind … H) -L
  61 #L1 #_ #IHL1 #K1 #HLK1 @lsx_intro
  62 #K2 #HK12 #HnT elim (ldrop_lpxs_trans … HLK1 … HK12) -HK12
  63 /4 width=10 by lleq_inv_lift_le/
  64 qed-.
  65
  66 lemma lsx_inv_lift_be: ∀h,g,G,L,T,U,dt,d,e. yinj d ≤ dt → dt ≤ d + e →
  67                        ⇧[d, e] T ≡ U → G ⊢ ⋕⬊*[h, g, U, dt] L →
  68                        ∀K. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⋕⬊*[h, g, T, d] K.
  69 #h #g #G #L #T #U #dt #d #e #Hddt #Hdtde #HTU #H @(lsx_ind … H) -L
  70 #L1 #_ #IHL1 #K1 #HLK1 @lsx_intro
  71 #K2 #HK12 #HnT elim (ldrop_lpxs_trans … HLK1 … HK12) -HK12
  72 /4 width=11 by lleq_inv_lift_be/
  73 qed-.
  74
  75 lemma lsx_inv_lift_ge: ∀h,g,G,L,T,U,dt,d,e. yinj d + yinj e ≤ dt →
  76                        ⇧[d, e] T ≡ U → G ⊢ ⋕⬊*[h, g, U, dt] L →
  77                        ∀K. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⋕⬊*[h, g, T, dt-e] K.
  78 #h #g #G #L #T #U #dt #d #e #Hdedt #HTU #H @(lsx_ind … H) -L
  79 #L1 #_ #IHL1 #K1 #HLK1 @lsx_intro
  80 #K2 #HK12 #HnT elim (ldrop_lpxs_trans … HLK1 … HK12) -HK12
  81 /4 width=9 by lleq_inv_lift_ge/
  82 qed-.