matita/matita/contribs/lambdadelta/basic_2/etc/leq/ldrop_leq.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 "ground_2/ynat/ynat_plus.ma".
  16 include "basic_2/grammar/leq.ma".
  17 include "basic_2/relocation/ldrop.ma".
  18
  19 (* BASIC SLICING FOR LOCAL ENVIRONMENTS *************************************)
  20
  21 lemma ldrop_leq_conf_ge: ∀L1,L2,d,e. L1 ≃[d, e] L2 →
  22                          ∀I,K,V,i. ⇩[O, i]L1 ≡ K.ⓑ{I}V → d + e ≤ i →
  23                          ⇩[O, i]L2 ≡ K.ⓑ{I}V.
  24 #L1 #L2 #d #e #H elim H -L1 -L2 -d -e
  25 [ #d #e #J #K #W #i #H elim (ldrop_inv_atom1 … H) -H
  26   #H destruct
  27 | #I #L1 #L2 #V #HL12 #IHL12 #J #K #W #i #H #_ elim (ldrop_inv_O1_pair1 … H) -H
  28   * #H1 #H2
  29   [ -IHL12 lapply (leq_inv_O2 … HL12) -HL12
  30     #H3 destruct //
  31   | -HL12 /4 width=1 by ldrop_ldrop_lt, yle_inj/
  32   ]
  33 | #I1 #I2 #L1 #L2 #V1 #V2 #e #_ #IHL12 #J #K #W #i #H1 >yplus_succ_swap
  34   #Hei elim (yle_inv_inj2 … Hei) -Hei
  35   #x #Hei #H elim (yplus_inv_inj … H) -H normalize
  36   #y #z >commutative_plus
  37   #H1 #H2 #H3 destruct elim (le_inv_plus_l … Hei) -Hei
  38   #Hzi #Hi lapply (ldrop_inv_ldrop1_lt … H1 ?) -H1
  39   /4 width=1 by ldrop_ldrop_lt, yle_inj/
  40 | #I #L1 #L2 #V #d #e #_ #IHL12 #J #K #W #i #H0 #Hdei elim (yle_inv_inj2 … Hdei) -Hdei
  41   #x #Hdei #H elim (yplus_inv_inj … H) -H
  42   #y #z >commutative_plus
  43   #H1 #H2 #H3 destruct elim (ysucc_inv_inj_dx … H2) -H2
  44   #x #H1 #H2 destruct elim (le_inv_plus_l … Hdei)
  45   #_ #Hi lapply (ldrop_inv_ldrop1_lt … H0 ?) -H0
  46   [2: #H0 @ldrop_ldrop_lt ] [2,3: /2 width=3 by lt_to_le_to_lt/ ]
  47   /4 width=3 by yle_inj, monotonic_pred/
  48 ]
  49 qed-.
  50
  51 lemma ldrop_leq_conf_be: ∀L1,L2,d,e. L1 ≃[d, e] L2 →
  52                          ∀I1,K1,V1,i. ⇩[O, i]L1 ≡ K1.ⓑ{I1}V1 → d ≤ i → i < d + e →
  53                          ∃∃I2,K2,V2. K1 ≃[0, ⫰(d+e-i)] K2 & ⇩[O, i]L2 ≡ K2.ⓑ{I2}V2.
  54 #L1 #L2 #d #e #H elim H -L1 -L2 -d -e
  55 [ #d #e #J1 #K1 #W1 #i #H elim (ldrop_inv_atom1 … H) -H
  56   #H destruct
  57 | #I #L1 #L2 #V #HL12 #IHL12 #J1 #K1 #W1 #i #_ #_ #H elim (ylt_yle_false … H) //
  58 | #I1 #I2 #L1 #L2 #V1 #V2 #e #HL12 >yplus_O1 >yplus_O1
  59   #IHL12 #J1 #K1 #W1 #i #H #_ elim (eq_or_gt i) #Hi destruct [ -IHL12 | -HL12 ]
  60   [ #_ lapply (ldrop_inv_O2 … H) -H
  61     #H destruct >ypred_succ /2 width=5 by ldrop_pair, ex2_3_intro/
  62   | lapply (ldrop_inv_ldrop1_lt … H ?) -H //
  63     #H <(ylt_inv_O1 i) /2 width=1 by ylt_inj/
  64     #Hie lapply (ylt_inv_succ … Hie) -Hie
  65     #Hie elim (IHL12 … H) -IHL12 -H //
  66     >yminus_succ /3 width=5 by ldrop_ldrop_lt, ex2_3_intro/
  67   ]
  68 | #I #L1 #L2 #V #d #e #_ #IHL12 #J1 #K1 #W1 #i #H #Hdi lapply (ylt_yle_trans 0 … Hdi ?) //
  69   #Hi <(ylt_inv_O1 … Hi) >yplus_succ1 >yminus_succ elim (yle_inv_succ1 … Hdi) -Hdi
  70   #Hdi #_ #Hide lapply (ylt_inv_succ … Hide)
  71   #Hide lapply (ylt_inv_inj … Hi) -Hi
  72   #Hi lapply (ldrop_inv_ldrop1_lt … H ?) -H //
  73   #H elim (IHL12 … H) -IHL12 -H
  74   /3 width=5 by ldrop_ldrop_lt, ex2_3_intro/
  75 ]
  76 qed-.
  77
  78 lemma ldrop_leq_conf_lt: ∀L1,L2,d,e. L1 ≃[d, e] L2 →
  79                          ∀I,K1,V,i. ⇩[O, i]L1 ≡ K1.ⓑ{I}V → i < d →
  80                          ∃∃K2. K1 ≃[⫰(d-i), e] K2 & ⇩[O, i]L2 ≡ K2.ⓑ{I}V.
  81 #L1 #L2 #d #e #H elim H -L1 -L2 -d -e
  82 [ #d #e #J #K1 #W #i #H elim (ldrop_inv_atom1 … H) -H
  83   #H destruct
  84 | #I #L1 #L2 #V #_ #_ #J #K1 #W #i #_ #H elim (ylt_yle_false … H) //
  85 | #I1 #I2 #L1 #L2 #V1 #V2 #e #_ #_ #J #K1 #W #i #_ #H elim (ylt_yle_false … H) //
  86 | #I #L1 #L2 #V #d #e #HL12 #IHL12 #J #K1 #W #i #H elim (eq_or_gt i) #Hi destruct [ -IHL12 | -HL12 ]
  87   [ #_ lapply (ldrop_inv_O2 … H) -H
  88     #H destruct >ypred_succ /2 width=5 by ldrop_pair, ex2_intro/
  89   | lapply (ldrop_inv_ldrop1_lt … H ?) -H //
  90     #H <(ylt_inv_O1 i) /2 width=1 by ylt_inj/
  91     #Hie lapply (ylt_inv_succ … Hie) -Hie
  92     #Hie elim (IHL12 … H) -IHL12 -H
  93     >yminus_succ /3 width=5 by ldrop_ldrop_lt, ex2_intro/
  94   ]
  95 ]
  96 qed-.