matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_tpss.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_tpss.ma".
  16 include "basic_2/unfold/ltpsss.ma".
  17
  18 (* ITERATED PARTIAL UNFOLD ON LOCAL ENVIRONMENTS ****************************)
  19
  20 (* Properties concerning partial substitution on terms **********************)
  21
  22 lemma ltpsss_tps2: ∀L1,L2,I,e.
  23                    L1 [0, e] ▶** L2 → ∀V1,V2. L2 ⊢ V1 [0, e] ▶ V2 →
  24                    L1. ⓑ{I} V1 [0, e + 1] ▶** L2. ⓑ{I} V2.
  25 #L1 #L2 #I #e #H @(ltpsss_ind … H) -L2
  26 [ /3 width=1/
  27 | #L #L2 #_ #HL2 #IHL #V1 #V2 #HV12
  28   elim (ltpss_tps_trans … HV12 … HL2) -HV12 #V #HV1 #HV2
  29   lapply (IHL … HV1) -IHL -HV1 /3 width=5/
  30 ]
  31 qed.
  32
  33 lemma ltpsss_tps2_lt: ∀L1,L2,I,V1,V2,e.
  34                       L1 [0, e - 1] ▶** L2 → L2 ⊢ V1 [0, e - 1] ▶ V2 →
  35                       0 < e → L1. ⓑ{I} V1 [0, e] ▶** L2. ⓑ{I} V2.
  36 #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He
  37 >(plus_minus_m_m e 1) // /2 width=1/
  38 qed.
  39
  40 lemma ltpsss_tps1: ∀L1,L2,I,d,e. L1 [d, e] ▶** L2 →
  41                    ∀V1,V2. L2 ⊢ V1 [d, e] ▶ V2 →
  42                    L1. ⓑ{I} V1 [d + 1, e] ▶** L2. ⓑ{I} V2.
  43 #L1 #L2 #I #d #e #H @(ltpsss_ind … H) -L2
  44 [ /3 width=1/
  45 | #L #L2 #_ #HL2 #IHL #V1 #V2 #HV12
  46   elim (ltpss_tps_trans … HV12 … HL2) -HV12 #V #HV1 #HV2
  47   lapply (IHL … HV1) -IHL -HV1 /3 width=5/
  48 ]
  49 qed.
  50
  51 lemma ltpsss_tps1_lt: ∀L1,L2,I,V1,V2,d,e.
  52                       L1 [d - 1, e] ▶** L2 → L2 ⊢ V1 [d - 1, e] ▶ V2 →
  53                       0 < d → L1. ⓑ{I} V1 [d, e] ▶** L2. ⓑ{I} V2.
  54 #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd
  55 >(plus_minus_m_m d 1) // /2 width=1/
  56 qed.
  57
  58 (* Properties concerning partial unfold on terms ****************************)
  59
  60 lemma ltpsss_tpss_conf_ge: ∀L0,L1,T2,U2,d1,e1,d2,e2. d1 + e1 ≤ d2 →
  61                            L0 ⊢ T2 [d2, e2] ▶* U2 → L0 [d1, e1] ▶** L1 →
  62                            L1 ⊢ T2 [d2, e2] ▶* U2.
  63 #L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde1d2 #HTU2 #H @(ltpsss_ind … H) -L1 //
  64 -HTU2 #L #L1 #_ #HL1 #IHL
  65 lapply (ltpss_tpss_conf_ge … IHL … HL1 ?) -HL1 -IHL //
  66 qed.
  67
  68 lemma ltpsss_tpss_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ▶** L0 →
  69                             ∀T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶* U2 →
  70                             d1 + e1 ≤ d2 → L1 ⊢ T2 [d2, e2] ▶* U2.
  71 #L1 #L0 #d1 #e1 #H @(ltpsss_ind … H) -L0 //
  72 #L #L0 #_ #HL0 #IHL #T2 #U2 #d2 #e2 #HTU2 #Hde1d2
  73 lapply (ltpss_tpss_trans_ge … HTU2 … HL0 ?) -HL0 -HTU2 // /2 width=1/
  74 qed.