matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_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_2/substitution/ltps_drop.ma".
  16 include "Basic_2/unfold/ltpss.ma".
  17
  18 (* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************)
  19
  20 lemma ltpss_drop_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 @(ltpss_ind … H) -L1 /3 width=6/
  24 qed.
  25
  26 lemma ltpss_drop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≫* L0 →
  27                            ∀L2,e2. ↓[0, e2] L0 ≡ L2 →
  28                            d1 + e1 ≤ e2 → ↓[0, e2] L1 ≡ L2.
  29 #L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0 /3 width=6/
  30 qed.
  31
  32 lemma ltpss_drop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ≫* L1 →
  33                           ∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
  34                           ∃∃L. L2 [0, d1 + e1 - e2] ≫* L & ↓[0, e2] L1 ≡ L.
  35 #L0 #L1 #d1 #e1 #H @(ltpss_ind … H) -L1
  36 [ /2/
  37 | #L #L1 #_ #HL1 #IHL #L2 #e2 #HL02 #Hd1e2 #He2de1
  38   elim (IHL … HL02 Hd1e2 He2de1) -L0 #L0 #HL20 #HL0
  39   elim (ltps_drop_conf_be … HL1 … HL0 Hd1e2 He2de1) -L /3/
  40 ]
  41 qed.
  42
  43 lemma ltpss_drop_trans_be: ∀L1,L0,d1,e1. L1 [d1, e1] ≫* L0 →
  44                            ∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
  45                            ∃∃L. L [0, d1 + e1 - e2] ≫* L2 & ↓[0, e2] L1 ≡ L.
  46 #L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0
  47 [ /2/
  48 | #L #L0 #_ #HL0 #IHL #L2 #e2 #HL02 #Hd1e2 #He2de1
  49   elim (ltps_drop_trans_be … HL0 … HL02 Hd1e2 He2de1) -L0 #L0 #HL02 #HL0
  50   elim (IHL … HL0 Hd1e2 He2de1) -L /3/
  51 ]
  52 qed.
  53
  54 lemma ltpss_drop_conf_le: ∀L0,L1,d1,e1. L0 [d1, e1] ≫* L1 →
  55                           ∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 →
  56                           ∃∃L. L2 [d1 - e2, e1] ≫* L & ↓[0, e2] L1 ≡ L.
  57 #L0 #L1 #d1 #e1 #H @(ltpss_ind … H) -L1
  58 [ /2/
  59 | #L #L1 #_ #HL1 #IHL #L2 #e2 #HL02 #He2d1
  60   elim (IHL … HL02 He2d1) -L0 #L0 #HL20 #HL0
  61   elim (ltps_drop_conf_le … HL1 … HL0 He2d1) -L /3/
  62 ]
  63 qed.
  64
  65 lemma ltpss_drop_trans_le: ∀L1,L0,d1,e1. L1 [d1, e1] ≫* L0 →
  66                            ∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 →
  67                            ∃∃L. L [d1 - e2, e1] ≫* L2 & ↓[0, e2] L1 ≡ L.
  68 #L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0
  69 [ /2/
  70 | #L #L0 #_ #HL0 #IHL #L2 #e2 #HL02 #He2d1
  71   elim (ltps_drop_trans_le … HL0 … HL02 He2d1) -L0 #L0 #HL02 #HL0
  72   elim (IHL … HL0 He2d1) -L /3/
  73 ]
  74 qed.