matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_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/unfold/tpss_lift.ma".
  16 include "basic_2/unfold/ltpss_sn.ma".
  17
  18 (* SN PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************)
  19
  20 lemma ltpss_sn_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 ⊢ ▶* [d1, e1] L1 →
  21                               ∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
  22                               d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2.
  23 #L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
  24 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H //
  25 | //
  26 | normalize #K0 #K1 #I #V0 #V1 #e1 #_ #_ #IHK01 #L2 #e2 #H #He12
  27   elim (le_inv_plus_l … He12) #_ #He2
  28   lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
  29   lapply (IHK01 … HK0L2 ?) -K0 /2 width=1/
  30 | #K0 #K1 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2
  31   elim (le_inv_plus_l … Hd1e2) #_ #He2
  32   lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
  33   lapply (IHK01 … HK0L2 ?) -K0 /2 width=1/
  34 ]
  35 qed.
  36
  37 lemma ltpss_sn_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 ⊢ ▶* [d1, e1] L0 →
  38                                ∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
  39                                d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2.
  40 #L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1
  41 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H //
  42 | //
  43 | normalize #K1 #K0 #I #V1 #V0 #e1 #_ #_ #IHK10 #L2 #e2 #H #He12
  44   elim (le_inv_plus_l … He12) #_ #He2
  45   lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
  46   lapply (IHK10 … HK0L2 ?) -K0 /2 width=1/
  47 | #K0 #K1 #I #V1 #V0 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2
  48   elim (le_inv_plus_l … Hd1e2) #_ #He2
  49   lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
  50   lapply (IHK10 … HK0L2 ?) -IHK10 -HK0L2 /2 width=1/
  51 ]
  52 qed.
  53
  54 lemma ltpss_sn_ldrop_conf_be: ∀L0,L1,d1,e1. L0 ⊢ ▶* [d1, e1] L1 →
  55                               ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
  56                               ∃∃L. L2 ⊢ ▶* [0, d1 + e1 - e2] L & ⇩[0, e2] L1 ≡ L.
  57 #L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
  58 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
  59 | normalize #L #I #V #L2 #e2 #HL2 #_ #He2
  60   lapply (le_n_O_to_eq … He2) -He2 #H destruct
  61   lapply (ldrop_inv_refl … HL2) -HL2 #H destruct /2 width=3/
  62 | normalize #K0 #K1 #I #V0 #V1 #e1 #HK01 #HV01 #IHK01 #L2 #e2 #H #_ #He21
  63   lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2
  64   [ -IHK01 -He21 destruct <minus_n_O /3 width=3/
  65   | -HK01 -HV01 <minus_le_minus_minus_comm //
  66     elim (IHK01 … HK0L2 ? ?) -K0 // /2 width=1/ /3 width=3/
  67   ]
  68 | #K0 #K1 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2 #He2de1
  69   elim (le_inv_plus_l … Hd1e2) #_ #He2
  70   <minus_le_minus_minus_comm //
  71   lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
  72   elim (IHK01 … HK0L2 ? ?) -K0 /2 width=1/ /3 width=3/
  73 ]
  74 qed.
  75
  76 lemma ltpss_sn_ldrop_trans_be: ∀L1,L0,d1,e1. L1 ⊢ ▶* [d1, e1] L0 →
  77                                ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
  78                                ∃∃L. L ⊢ ▶* [0, d1 + e1 - e2] L2 & ⇩[0, e2] L1 ≡ L.
  79 #L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1
  80 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
  81 | normalize #L #I #V #L2 #e2 #HL2 #_ #He2
  82   lapply (le_n_O_to_eq … He2) -He2 #H destruct
  83   lapply (ldrop_inv_refl … HL2) -HL2 #H destruct /2 width=3/
  84 | normalize #K1 #K0 #I #V1 #V0 #e1 #HK10 #HV10 #IHK10 #L2 #e2 #H #_ #He21
  85   lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2
  86   [ -IHK10 -He21 destruct <minus_n_O /3 width=3/
  87   | -HK10 -HV10 <minus_le_minus_minus_comm //
  88     elim (IHK10 … HK0L2 ? ?) -K0 // /2 width=1/ /3 width=3/
  89   ]
  90 | #K1 #K0 #I #V1 #V0 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2 #He2de1
  91   elim (le_inv_plus_l … Hd1e2) #_ #He2
  92   <minus_le_minus_minus_comm //
  93   lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
  94   elim (IHK10 … HK0L2 ? ?) -K0 /2 width=1/ /3 width=3/
  95 ]
  96 qed.
  97
  98 lemma ltpss_sn_ldrop_conf_le: ∀L0,L1,d1,e1. L0 ⊢ ▶* [d1, e1] L1 →
  99                               ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
 100                               ∃∃L. L2 ⊢ ▶* [d1 - e2, e1] L & ⇩[0, e2] L1 ≡ L.
 101 #L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
 102 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
 103 | /2 width=3/
 104 | normalize #K0 #K1 #I #V0 #V1 #e1 #HK01 #HV01 #_ #L2 #e2 #H #He2
 105   lapply (le_n_O_to_eq … He2) -He2 #He2 destruct
 106   lapply (ldrop_inv_refl … H) -H #H destruct /3 width=3/
 107 | #K0 #K1 #I #V0 #V1 #d1 #e1 #HK01 #HV01 #IHK01 #L2 #e2 #H #He2d1
 108   lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2
 109   [ -IHK01 -He2d1 destruct <minus_n_O /3 width=3/
 110   | -HK01 -HV01 <minus_le_minus_minus_comm //
 111     elim (IHK01 … HK0L2 ?) -K0 /2 width=1/ /3 width=3/
 112   ]
 113 ]
 114 qed.
 115
 116 lemma ltpss_sn_ldrop_trans_le: ∀L1,L0,d1,e1. L1 ⊢ ▶* [d1, e1] L0 →
 117                                ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
 118                                ∃∃L. L ⊢ ▶* [d1 - e2, e1] L2 & ⇩[0, e2] L1 ≡ L.
 119 #L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1
 120 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
 121 | /2 width=3/
 122 | normalize #K1 #K0 #I #V1 #V0 #e1 #HK10 #HV10 #_ #L2 #e2 #H #He2
 123   lapply (le_n_O_to_eq … He2) -He2 #He2 destruct
 124   lapply (ldrop_inv_refl … H) -H #H destruct /3 width=3/
 125 | #K1 #K0 #I #V1 #V0 #d1 #e1 #HK10 #HV10 #IHK10 #L2 #e2 #H #He2d1
 126   lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2
 127   [ -IHK10 -He2d1 destruct <minus_n_O /3 width=3/
 128   | -HK10 -HV10 <minus_le_minus_minus_comm //
 129     elim (IHK10 … HK0L2 ?) -K0 /2 width=1/ /3 width=3/
 130   ]
 131 ]
 132 qed.
 133
 134 lemma ldrop_ltpss_sn_trans_be: ∀L1,K1,d1,e1. ⇩[d1, e1] L1 ≡ K1 →
 135                                ∀K2,d2,e2. K1 ⊢ ▶* [d2, e2] K2 →
 136                                d2 ≤ d1 → d1 ≤ d2 + e2 →
 137                                ∃∃L2. L1 ⊢ ▶* [d2, e1 + e2] L2 &
 138                                      ⇩[d1, e1] L2 ≡ K2.
 139 #L1 #K1 #d1 #e1 #H elim H -L1 -K1 -d1 -e1
 140 [ #d1 #e1 #K2 #d2 #e2 #H #_ #_
 141   >(ltpss_sn_inv_atom1 … H) -H /2 width=3/
 142 | #K1 #I #V1 #K2 #d2 #e2 #HK12 #H #_
 143   lapply (le_n_O_to_eq … H) -H #H destruct /2 width=3/
 144 | #L1 #K1 #I #V #e1 #_ #IHLK1 #K2 #d2 #e2 #HK12 #H1 #H2
 145   elim (IHLK1 … HK12 H1 H2) -K1 -H2
 146   lapply (le_n_O_to_eq … H1) -H1 #H destruct /3 width=5/
 147 | #L1 #K1 #I #V1 #W1 #d1 #e1 #HLK1 #HWV1 #IHLK1 #X #d2 #e2 #H #Hd21 #Hd12
 148   elim (eq_or_gt d2) #Hd2 [ -Hd21 elim (eq_or_gt e2) #He2 ] destruct
 149   [ lapply (le_n_O_to_eq … Hd12) -Hd12 <plus_n_Sm #H destruct
 150   | elim (ltpss_sn_inv_tpss21 … H He2) -H #K2 #W2 #HK12 #HW12 #H destruct
 151     elim (IHLK1 … HK12 …) -IHLK1 // /2 width=1/ >plus_minus_commutative // #L2 #HL12 #HLK2
 152     elim (lift_total W2 d1 e1) #V2 #HWV2
 153     lapply (tpss_lift_be … HW12 … HLK1 HWV1 … HWV2) -HLK1 -W1 // /2 width=1/
 154     >plus_minus // >commutative_plus /4 width=5/
 155   | elim (ltpss_sn_inv_tpss11 … H Hd2) -H #K2 #W2 #HK12 #HW12 #H destruct
 156     elim (IHLK1 … HK12 …) -IHLK1 [2: >plus_minus // ] /2 width=1/ #L2 #HL12 #HLK2
 157     elim (lift_total W2 d1 e1) #V2 #HWV2
 158     lapply (tpss_lift_be … HW12 … HLK1 HWV1 … HWV2) -HLK1 -W1 [ >plus_minus // ] /2 width=1/
 159     >commutative_plus /3 width=5/
 160   ]
 161 ]
 162 qed-.
 163
 164 lemma ldrop_ltpss_sn_trans_ge: ∀L1,K1,d1,e1. ⇩[d1, e1] L1 ≡ K1 →
 165                                ∀K2,d2,e2. K1 ⊢ ▶* [d2, e2] K2 → d2 + e2 ≤ d1 →
 166                                ∃∃L2. L1 ⊢ ▶* [d2, e2] L2 & ⇩[d1, e1] L2 ≡ K2.
 167 #L1 #K1 #d1 #e1 #H elim H -L1 -K1 -d1 -e1
 168 [ #d1 #e1 #K2 #d2 #e2 #H #_
 169   >(ltpss_sn_inv_atom1 … H) -H /2 width=3/
 170 | #K1 #I #V1 #K2 #d2 #e2 #HK12 #H
 171   elim (plus_le_0 … H) -H #H1 #H2 destruct /2 width=3/
 172 | #L1 #K1 #I #V #e1 #_ #IHLK1 #K2 #d2 #e2 #HK12 #H
 173   elim (IHLK1 … HK12 H) -K1
 174   elim (plus_le_0 … H) -H #H1 #H2 destruct #L2 #HL12
 175   >(ltpss_sn_inv_refl_O2 … HL12) -L1 /3 width=5/
 176 | #L1 #K1 #I #V1 #W1 #d1 #e1 #HLK1 #HWV1 #IHLK1 #X #d2 #e2 #H #Hd21
 177   elim (eq_or_gt d2) #Hd2 [ elim (eq_or_gt e2) #He2 ] destruct
 178   [ -IHLK1 -Hd21 <(ltpss_sn_inv_refl_O2 … H) -X /3 width=5/
 179   | elim (ltpss_sn_inv_tpss21 … H He2) -H #K2 #W2 #HK12 #HW12 #H destruct
 180     elim (IHLK1 … HK12 …) -IHLK1 /2 width=1/ #L2 #HL12 #HLK2
 181     elim (lift_total W2 d1 e1) #V2 #HWV2
 182     lapply (tpss_lift_le … HW12 … HLK1 HWV1 … HWV2) -HLK1 -W1 /2 width=1/ /3 width=5/
 183   | elim (ltpss_sn_inv_tpss11 … H Hd2) -H #K2 #W2 #HK12 #HW12 #H destruct
 184     elim (IHLK1 … HK12 …) -IHLK1 [2: >plus_minus // /2 width=1/ ] #L2 #HL12 #HLK2
 185     elim (lift_total W2 d1 e1) #V2 #HWV2
 186     lapply (tpss_lift_le … HW12 … HLK1 HWV1 … HWV2) -HLK1 -W1 [ >plus_minus // /2 width=1/ ] /3 width=5/
 187   ]
 188 ]
 189 qed-.