matita/matita/contribs/lambdadelta/basic_2A/computation/lsx_drop.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_2A/multiple/lleq_drop.ma".
  16 include "basic_2A/reduction/lpx_drop.ma".
  17 include "basic_2A/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,l,i. |L| ≤ i → G ⊢ ⬊*[h, g, #i, l] L.
  24 #h #g #G #L1 #l #i #HL1 @lsx_intro
  25 #L2 #HL12 #H elim H -H
  26 /4 width=6 by lpx_fwd_length, lleq_free, le_repl_sn_conf_aux/
  27 qed.
  28
  29 lemma lsx_lref_skip: ∀h,g,G,L,l,i. yinj i < l → G ⊢ ⬊*[h, g, #i, l] L.
  30 #h #g #G #L1 #l #i #HL1 @lsx_intro
  31 #L2 #HL12 #H elim H -H
  32 /3 width=4 by lpx_fwd_length, lleq_skip/
  33 qed.
  34
  35 (* Advanced forward lemmas **************************************************)
  36
  37 lemma lsx_fwd_lref_be: ∀h,g,I,G,L,l,i. l ≤ yinj i → G ⊢ ⬊*[h, g, #i, l] L →
  38                        ∀K,V. ⬇[i] L ≡ K.ⓑ{I}V → G ⊢ ⬊*[h, g, V, 0] K.
  39 #h #g #I #G #L #l #i #Hli #H @(lsx_ind … H) -L
  40 #L1 #_ #IHL1 #K1 #V #HLK1 @lsx_intro
  41 #K2 #HK12 #HnK12 lapply (drop_fwd_drop2 … HLK1)
  42 #H2LK1 elim (drop_lpx_trans … H2LK1 … HK12) -H2LK1 -HK12
  43 #L2 #HL12 #H2LK2 #H elim (lreq_drop_conf_be … H … HLK1) -H /2 width=1 by ylt_inj/
  44 #Y #_ #HLK2 lapply (drop_fwd_drop2 … HLK2)
  45 #HY lapply (drop_mono … HY … H2LK2) -HY -H2LK2 #H destruct
  46 /4 width=10 by lleq_inv_lref_ge/
  47 qed-.
  48
  49 (* Properties on relocation *************************************************)
  50
  51 lemma lsx_lift_le: ∀h,g,G,K,T,U,lt,l,m. lt ≤ yinj l →
  52                    ⬆[l, m] T ≡ U → G ⊢ ⬊*[h, g, T, lt] K →
  53                    ∀L. ⬇[Ⓕ, l, m] L ≡ K → G ⊢ ⬊*[h, g, U, lt] L.
  54 #h #g #G #K #T #U #lt #l #m #Hltl #HTU #H @(lsx_ind … H) -K
  55 #K1 #_ #IHK1 #L1 #HLK1 @lsx_intro
  56 #L2 #HL12 #HnU elim (lpx_drop_conf … HLK1 … HL12) -HL12
  57 /4 width=10 by lleq_lift_le/
  58 qed-.
  59
  60 lemma lsx_lift_ge: ∀h,g,G,K,T,U,lt,l,m. yinj l ≤ lt →
  61                    ⬆[l, m] T ≡ U → G ⊢ ⬊*[h, g, T, lt] K →
  62                    ∀L. ⬇[Ⓕ, l, m] L ≡ K → G ⊢ ⬊*[h, g, U, lt + m] L.
  63 #h #g #G #K #T #U #lt #l #m #Hllt #HTU #H @(lsx_ind … H) -K
  64 #K1 #_ #IHK1 #L1 #HLK1 @lsx_intro
  65 #L2 #HL12 #HnU elim (lpx_drop_conf … HLK1 … HL12) -HL12
  66 /4 width=9 by lleq_lift_ge/
  67 qed-.
  68
  69 (* Inversion lemmas on relocation *******************************************)
  70
  71 lemma lsx_inv_lift_le: ∀h,g,G,L,T,U,lt,l,m. lt ≤ yinj l →
  72                        ⬆[l, m] T ≡ U → G ⊢ ⬊*[h, g, U, lt] L →
  73                        ∀K. ⬇[Ⓕ, l, m] L ≡ K → G ⊢ ⬊*[h, g, T, lt] K.
  74 #h #g #G #L #T #U #lt #l #m #Hltl #HTU #H @(lsx_ind … H) -L
  75 #L1 #_ #IHL1 #K1 #HLK1 @lsx_intro
  76 #K2 #HK12 #HnT elim (drop_lpx_trans … HLK1 … HK12) -HK12
  77 /4 width=10 by lleq_inv_lift_le/
  78 qed-.
  79
  80 lemma lsx_inv_lift_be: ∀h,g,G,L,T,U,lt,l,m. yinj l ≤ lt → lt ≤ l + m →
  81                        ⬆[l, m] T ≡ U → G ⊢ ⬊*[h, g, U, lt] L →
  82                        ∀K. ⬇[Ⓕ, l, m] L ≡ K → G ⊢ ⬊*[h, g, T, l] K.
  83 #h #g #G #L #T #U #lt #l #m #Hllt #Hltlm #HTU #H @(lsx_ind … H) -L
  84 #L1 #_ #IHL1 #K1 #HLK1 @lsx_intro
  85 #K2 #HK12 #HnT elim (drop_lpx_trans … HLK1 … HK12) -HK12
  86 /4 width=11 by lleq_inv_lift_be/
  87 qed-.
  88
  89 lemma lsx_inv_lift_ge: ∀h,g,G,L,T,U,lt,l,m. yinj l + yinj m ≤ lt →
  90                        ⬆[l, m] T ≡ U → G ⊢ ⬊*[h, g, U, lt] L →
  91                        ∀K. ⬇[Ⓕ, l, m] L ≡ K → G ⊢ ⬊*[h, g, T, lt-m] K.
  92 #h #g #G #L #T #U #lt #l #m #Hlmlt #HTU #H @(lsx_ind … H) -L
  93 #L1 #_ #IHL1 #K1 #HLK1 @lsx_intro
  94 #K2 #HK12 #HnT elim (drop_lpx_trans … HLK1 … HK12) -HK12
  95 /4 width=9 by lleq_inv_lift_ge/
  96 qed-.