matita/matita/contribs/lambdadelta/basic_2A/etc/delift/thin_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/unfold/ltpss_sn_ldrop.ma".
  16 include "basic_2/unfold/thin.ma".
  17
  18 (* BASIC LOCAL ENVIRONMENT THINNING *****************************************)
  19
  20 (* Properties on local environment slicing **********************************)
  21
  22 lemma thin_ldrop_conf_ge: ∀L0,L1,d1,e1. ▼*[d1, e1] L0 ≡ L1 →
  23                           ∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
  24                           d1 + e1 ≤ e2 → ⇩[0, e2 - e1] L1 ≡ L2.
  25 #L0 #L1 #d1 #e1 * /3 width=8 by ltpss_sn_ldrop_conf_ge, ldrop_conf_ge/
  26 qed.
  27
  28 lemma thin_ldrop_conf_be: ∀L0,L1,d1,e1. ▼*[d1, e1] L0 ≡ L1 →
  29                           ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
  30                           ∃∃L. ▼*[0, d1 + e1 - e2] L2 ≡ L & ⇩[0, d1] L1 ≡ L.
  31 #L0 #L1 #d1 #e1 * #L #HL0 #HL1 #L2 #e2 #HL02 #Hd1e2 #He2de1
  32 elim (ltpss_sn_ldrop_conf_be … HL0 … HL02 ? ?) -L0 // #L0 #HL20 #HL0
  33 elim (ldrop_conf_be … HL1 … HL0 ? ?) -L // -Hd1e2 -He2de1 /3 width=3/
  34 qed.
  35
  36 lemma thin_ldrop_conf_le: ∀L0,L1,d1,e1. ▼*[d1, e1] L0 ≡ L1 →
  37                           ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
  38                           ∃∃L. ▼*[d1 - e2, e1] L2 ≡ L & ⇩[0, e2] L1 ≡ L.
  39 #L0 #L1 #d1 #e1 * #L #HL0 #HL1 #L2 #e2 #HL02 #He2d1
  40 elim (ltpss_sn_ldrop_conf_le … HL0 … HL02 ?) -L0 // #L0 #HL20 #HL0
  41 elim (ldrop_conf_le … HL1 … HL0 ?) -L // -He2d1 /3 width=3/
  42 qed.
  43
  44 lemma thin_ldrop_trans_ge: ∀L1,L0,d1,e1. ▼*[d1, e1] L1 ≡ L0 →
  45                            ∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
  46                            d1 ≤ e2 → ⇩[0, e1 + e2] L1 ≡ L2.
  47 #L1 #L0 #d1 #e1 * #L #HL1 #HL0 #L2 #e2 #HL02 #Hd1e2
  48 lapply (ldrop_trans_ge … HL0 … HL02 ?) -L0 // #HL2
  49 lapply (ltpss_sn_ldrop_trans_ge … HL1 … HL2 ?) -L // /2 width=1/
  50 qed.
  51
  52 lemma thin_ldrop_trans_le: ∀L1,L0,d1,e1. ▼*[d1, e1] L1 ≡ L0 →
  53                            ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
  54                            ∃∃L. ▼*[d1 - e2, e1] L ≡ L2 & ⇩[0, e2] L1 ≡ L.
  55 #L1 #L0 #d1 #e1 * #L #HL1 #HL0 #L2 #e2 #HL02 #He2d1
  56 elim (ldrop_trans_le … HL0 … HL02 He2d1) -L0 #L0 #HL0 #HL02
  57 elim (ltpss_sn_ldrop_trans_le … HL1 … HL0 He2d1) -L -He2d1 /3 width=3/
  58 qed.