matita/matita/contribs/lambdadelta/basic_2A/etc/cpr/ltpss_sn_ldrop.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 "basic_2/substitution/fsup.ma".
  16 include "basic_2/unfold/tpss_lift.ma".
  17 include "basic_2/unfold/ltpss_sn.ma".
  18
  19 (* SN PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************)
  20
  21 (* Properies on local environment slicing ***********************************)
  22
  23 lemma ltpss_sn_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 ⊢ ▶* [d1, e1] L1 →
  24                               ∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
  25                               d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2.
  26 #L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
  27 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H //
  28 | //
  29 | normalize #K0 #K1 #I #V0 #V1 #e1 #_ #_ #IHK01 #L2 #e2 #H #He12
  30   elim (le_inv_plus_l … He12) #_ #He2
  31   lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
  32   lapply (IHK01 … HK0L2 ?) -K0 /2 width=1/
  33 | #K0 #K1 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2
  34   elim (le_inv_plus_l … Hd1e2) #_ #He2
  35   lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
  36   lapply (IHK01 … HK0L2 ?) -K0 /2 width=1/
  37 ]
  38 qed.
  39
  40 lemma ltpss_sn_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 ⊢ ▶* [d1, e1] L0 →
  41                                ∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
  42                                d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2.
  43 #L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1
  44 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H //
  45 | //
  46 | normalize #K1 #K0 #I #V1 #V0 #e1 #_ #_ #IHK10 #L2 #e2 #H #He12
  47   elim (le_inv_plus_l … He12) #_ #He2
  48   lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
  49   lapply (IHK10 … HK0L2 ?) -K0 /2 width=1/
  50 | #K0 #K1 #I #V1 #V0 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2
  51   elim (le_inv_plus_l … Hd1e2) #_ #He2
  52   lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
  53   lapply (IHK10 … HK0L2 ?) -IHK10 -HK0L2 /2 width=1/
  54 ]
  55 qed.
  56
  57 lemma ltpss_sn_ldrop_conf_be: ∀L0,L1,d1,e1. L0 ⊢ ▶* [d1, e1] L1 →
  58                               ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
  59                               ∃∃L. L2 ⊢ ▶* [0, d1 + e1 - e2] L & ⇩[0, e2] L1 ≡ L.
  60 #L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
  61 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
  62 | normalize #L #I #V #L2 #e2 #HL2 #_ #He2
  63   lapply (le_n_O_to_eq … He2) -He2 #H destruct
  64   lapply (ldrop_inv_refl … HL2) -HL2 #H destruct /2 width=3/
  65 | normalize #K0 #K1 #I #V0 #V1 #e1 #HK01 #HV01 #IHK01 #L2 #e2 #H #_ #He21
  66   lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2
  67   [ -IHK01 -He21 destruct <minus_n_O /3 width=3/
  68   | -HK01 -HV01 <minus_le_minus_minus_comm //
  69     elim (IHK01 … HK0L2 ? ?) -K0 // /2 width=1/ /3 width=3/
  70   ]
  71 | #K0 #K1 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2 #He2de1
  72   elim (le_inv_plus_l … Hd1e2) #_ #He2
  73   <minus_le_minus_minus_comm //
  74   lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
  75   elim (IHK01 … HK0L2 ? ?) -K0 /2 width=1/ /3 width=3/
  76 ]
  77 qed.
  78
  79 lemma ltpss_sn_ldrop_trans_be: ∀L1,L0,d1,e1. L1 ⊢ ▶* [d1, e1] L0 →
  80                                ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
  81                                ∃∃L. L ⊢ ▶* [0, d1 + e1 - e2] L2 & ⇩[0, e2] L1 ≡ L.
  82 #L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1
  83 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
  84 | normalize #L #I #V #L2 #e2 #HL2 #_ #He2
  85   lapply (le_n_O_to_eq … He2) -He2 #H destruct
  86   lapply (ldrop_inv_refl … HL2) -HL2 #H destruct /2 width=3/
  87 | normalize #K1 #K0 #I #V1 #V0 #e1 #HK10 #HV10 #IHK10 #L2 #e2 #H #_ #He21
  88   lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2
  89   [ -IHK10 -He21 destruct <minus_n_O /3 width=3/
  90   | -HK10 -HV10 <minus_le_minus_minus_comm //
  91     elim (IHK10 … HK0L2 ? ?) -K0 // /2 width=1/ /3 width=3/
  92   ]
  93 | #K1 #K0 #I #V1 #V0 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2 #He2de1
  94   elim (le_inv_plus_l … Hd1e2) #_ #He2
  95   <minus_le_minus_minus_comm //
  96   lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
  97   elim (IHK10 … HK0L2 ? ?) -K0 /2 width=1/ /3 width=3/
  98 ]
  99 qed.
 100
 101 lemma ltpss_sn_ldrop_conf_le: ∀L0,L1,d1,e1. L0 ⊢ ▶* [d1, e1] L1 →
 102                               ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
 103                               ∃∃L. L2 ⊢ ▶* [d1 - e2, e1] L & ⇩[0, e2] L1 ≡ L.
 104 #L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
 105 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
 106 | /2 width=3/
 107 | normalize #K0 #K1 #I #V0 #V1 #e1 #HK01 #HV01 #_ #L2 #e2 #H #He2
 108   lapply (le_n_O_to_eq … He2) -He2 #He2 destruct
 109   lapply (ldrop_inv_refl … H) -H #H destruct /3 width=3/
 110 | #K0 #K1 #I #V0 #V1 #d1 #e1 #HK01 #HV01 #IHK01 #L2 #e2 #H #He2d1
 111   lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2
 112   [ -IHK01 -He2d1 destruct <minus_n_O /3 width=3/
 113   | -HK01 -HV01 <minus_le_minus_minus_comm //
 114     elim (IHK01 … HK0L2 ?) -K0 /2 width=1/ /3 width=3/
 115   ]
 116 ]
 117 qed.
 118
 119 lemma ltpss_sn_ldrop_trans_le: ∀L1,L0,d1,e1. L1 ⊢ ▶* [d1, e1] L0 →
 120                                ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
 121                                ∃∃L. L ⊢ ▶* [d1 - e2, e1] L2 & ⇩[0, e2] L1 ≡ L.
 122 #L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1
 123 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
 124 | /2 width=3/
 125 | normalize #K1 #K0 #I #V1 #V0 #e1 #HK10 #HV10 #_ #L2 #e2 #H #He2
 126   lapply (le_n_O_to_eq … He2) -He2 #He2 destruct
 127   lapply (ldrop_inv_refl … H) -H #H destruct /3 width=3/
 128 | #K1 #K0 #I #V1 #V0 #d1 #e1 #HK10 #HV10 #IHK10 #L2 #e2 #H #He2d1
 129   lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2
 130   [ -IHK10 -He2d1 destruct <minus_n_O /3 width=3/
 131   | -HK10 -HV10 <minus_le_minus_minus_comm //
 132     elim (IHK10 … HK0L2 ?) -K0 /2 width=1/ /3 width=3/
 133   ]
 134 ]
 135 qed.
 136
 137 lemma ldrop_ltpss_sn_trans_le: ∀L1,K1,d1,e1. ⇩[d1, e1] L1 ≡ K1 →
 138                                ∀K2,d2,e2. K1 ⊢ ▶* [d2, e2] K2 → d1 ≤ d2 →
 139                                ∃∃L2. L1 ⊢ ▶* [d2 + e1, e2] L2 & ⇩[d1, e1] L2 ≡ K2.
 140 #L1 #K1 #d1 #e1 #H elim H -L1 -K1 -d1 -e1
 141 [ #d1 #e1 #K2 #d2 #e2 #H #_
 142   >(ltpss_sn_inv_atom1 … H) -H /2 width=3/
 143 | /2 width=3/
 144 | #L1 #K1 #I #V #e1 #_ #IHLK1 #K2 #d2 #e2 #HK12 #Hd
 145   elim (IHLK1 … HK12 Hd) -K1 -Hd /3 width=5/
 146 | #L1 #K1 #I #V1 #W1 #d1 #e1 #HLK1 #HWV1 #IHLK1 #X #d2 #e2 #H #Hd12
 147   elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #Hd2
 148   elim (ltpss_sn_inv_tpss11 … H Hd2) -H #K2 #W2 #HK12 #HW12 #H destruct
 149   elim (IHLK1 … HK12 … Hd12) -IHLK1 -HK12 <le_plus_minus_comm // #L2 #HL12 #HLK2
 150   elim (lift_total W2 d1 e1) #V2 #HWV2
 151   lapply (tpss_lift_ge … HW12 … HLK1 HWV1 … HWV2) -HLK1 -W1 // -Hd12
 152   <le_plus_minus_comm // /4 width=5/
 153 ]
 154 qed-.
 155
 156 lemma ldrop_ltpss_sn_trans_be: ∀L1,K1,d1,e1. ⇩[d1, e1] L1 ≡ K1 →
 157                                ∀K2,d2,e2. K1 ⊢ ▶* [d2, e2] K2 →
 158                                d2 ≤ d1 → d1 ≤ d2 + e2 →
 159                                ∃∃L2. L1 ⊢ ▶* [d2, e1 + e2] L2 &
 160                                      ⇩[d1, e1] L2 ≡ K2.
 161 #L1 #K1 #d1 #e1 #H elim H -L1 -K1 -d1 -e1
 162 [ #d1 #e1 #K2 #d2 #e2 #H #_ #_
 163   >(ltpss_sn_inv_atom1 … H) -H /2 width=3/
 164 | #K1 #I #V1 #K2 #d2 #e2 #HK12 #H #_
 165   lapply (le_n_O_to_eq … H) -H #H destruct /2 width=3/
 166 | #L1 #K1 #I #V #e1 #_ #IHLK1 #K2 #d2 #e2 #HK12 #H1 #H2
 167   elim (IHLK1 … HK12 H1 H2) -K1 -H2
 168   lapply (le_n_O_to_eq … H1) -H1 #H destruct /3 width=5/
 169 | #L1 #K1 #I #V1 #W1 #d1 #e1 #HLK1 #HWV1 #IHLK1 #X #d2 #e2 #H #Hd21 #Hd12
 170   elim (eq_or_gt d2) #Hd2 [ -Hd21 elim (eq_or_gt e2) #He2 ] destruct
 171   [ lapply (le_n_O_to_eq … Hd12) -Hd12 <plus_n_Sm #H destruct
 172   | elim (ltpss_sn_inv_tpss21 … H He2) -H #K2 #W2 #HK12 #HW12 #H destruct
 173     elim (IHLK1 … HK12 …) -IHLK1 // /2 width=1/ >plus_minus_commutative // #L2 #HL12 #HLK2
 174     elim (lift_total W2 d1 e1) #V2 #HWV2
 175     lapply (tpss_lift_be … HW12 … HLK1 HWV1 … HWV2) -HLK1 -W1 // /2 width=1/
 176     >plus_minus // >commutative_plus /4 width=5/
 177   | elim (ltpss_sn_inv_tpss11 … H Hd2) -H #K2 #W2 #HK12 #HW12 #H destruct
 178     elim (IHLK1 … HK12 …) -IHLK1 [2: >plus_minus // ] /2 width=1/ #L2 #HL12 #HLK2
 179     elim (lift_total W2 d1 e1) #V2 #HWV2
 180     lapply (tpss_lift_be … HW12 … HLK1 HWV1 … HWV2) -HLK1 -W1 [ >plus_minus // ] /2 width=1/
 181     >commutative_plus /3 width=5/
 182   ]
 183 ]
 184 qed-.
 185
 186 lemma ldrop_ltpss_sn_trans_ge: ∀L1,K1,d1,e1. ⇩[d1, e1] L1 ≡ K1 →
 187                                ∀K2,d2,e2. K1 ⊢ ▶* [d2, e2] K2 → d2 + e2 ≤ d1 →
 188                                ∃∃L2. L1 ⊢ ▶* [d2, e2] L2 & ⇩[d1, e1] L2 ≡ K2.
 189 #L1 #K1 #d1 #e1 #H elim H -L1 -K1 -d1 -e1
 190 [ #d1 #e1 #K2 #d2 #e2 #H #_
 191   >(ltpss_sn_inv_atom1 … H) -H /2 width=3/
 192 | #K1 #I #V1 #K2 #d2 #e2 #HK12 #H
 193   elim (plus_le_0 … H) -H #H1 #H2 destruct /2 width=3/
 194 | #L1 #K1 #I #V #e1 #_ #IHLK1 #K2 #d2 #e2 #HK12 #H
 195   elim (IHLK1 … HK12 H) -K1
 196   elim (plus_le_0 … H) -H #H1 #H2 destruct #L2 #HL12
 197   >(ltpss_sn_inv_refl_O2 … HL12) -L1 /3 width=5/
 198 | #L1 #K1 #I #V1 #W1 #d1 #e1 #HLK1 #HWV1 #IHLK1 #X #d2 #e2 #H #Hd21
 199   elim (eq_or_gt d2) #Hd2 [ elim (eq_or_gt e2) #He2 ] destruct
 200   [ -IHLK1 -Hd21 <(ltpss_sn_inv_refl_O2 … H) -X /3 width=5/
 201   | elim (ltpss_sn_inv_tpss21 … H He2) -H #K2 #W2 #HK12 #HW12 #H destruct
 202     elim (IHLK1 … HK12 …) -IHLK1 /2 width=1/ #L2 #HL12 #HLK2
 203     elim (lift_total W2 d1 e1) #V2 #HWV2
 204     lapply (tpss_lift_le … HW12 … HLK1 HWV1 … HWV2) -HLK1 -W1 /2 width=1/ /3 width=5/
 205   | elim (ltpss_sn_inv_tpss11 … H Hd2) -H #K2 #W2 #HK12 #HW12 #H destruct
 206     elim (IHLK1 … HK12 …) -IHLK1 [2: >plus_minus // /2 width=1/ ] #L2 #HL12 #HLK2
 207     elim (lift_total W2 d1 e1) #V2 #HWV2
 208     lapply (tpss_lift_le … HW12 … HLK1 HWV1 … HWV2) -HLK1 -W1 [ >plus_minus // /2 width=1/ ] /3 width=5/
 209   ]
 210 ]
 211 qed-.
 212
 213 (* Properties on supclosure *************************************************)
 214
 215 lemma fsup_tpss_trans_full: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀U2. L2 ⊢ T2 ▶*[0,|L2|] U2 →
 216                             ∃∃L,U1. L1 ⊢ ▶*[0,|L1|] L & L ⊢ T1 ▶*[0,|L|] U1 & ⦃L, U1⦄ ⊃ ⦃L2, T2⦄.
 217 #L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 [1,2,3,4,5: /3 width=5/ ]
 218 #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2
 219 elim (IHT12 … HTU2) -IHT12 -HTU2 #K #T #HK1 #HT1 #HT2
 220 elim (lift_total T d e) #U #HTU
 221 lapply (ltpss_sn_fwd_length … HK1) #H >H in HK1; -H #HK1
 222 elim (le_or_ge d (|K|)) #Hd
 223 [ elim (ldrop_ltpss_sn_trans_be … HLK1 … HK1 … Hd) // -HLK1 -HK1 #L2 #HL12 #HL2K
 224   lapply (tpss_lift_be … HT1 … Hd HL2K HTU1 … HTU) // -HT1 -HTU1 #HU1
 225 | elim (ldrop_ltpss_sn_trans_ge … HLK1 … HK1 Hd) -HLK1 -HK1 #L2 #HL12 #HL2K
 226   lapply (tpss_lift_le … HT1 … Hd HL2K HTU1 … HTU) -HT1 -HTU1 #HU1
 227 ]
 228 lapply (ltpss_sn_weak_full … HL12) -HL12 #HL12
 229 lapply (tpss_weak_full … HU1) -HU1 #HU1
 230 @(ex3_2_intro … L2 U) // /2 width=7/ (**) (* explicit constructor: auto /3 width=14/ too slow *)
 231 qed-.