matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt_cpm.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/rt_transition/cpm_drops.ma".
  16 include "basic_2/rt_transition/cpt_drops.ma".
  17
  18 (* T-BOUND CONTEXT-SENSITIVE PARALLEL T-TRANSITION FOR TERMS ****************)
  19
  20 (* Properties with t-bound rt-transition for terms **************************)
  21
  22 lemma cpm_cpt_cpr (h) (n) (G) (L):
  23       ∀T1,T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 →
  24       ∃∃T0. ⦃G,L⦄ ⊢ T1 ⬆[h,n] T0 & ⦃G,L⦄ ⊢ T0 ➡[h] T2.
  25 #h #n #G #L #T1 #T2 #H
  26 @(cpm_ind … H) -n -G -L -T1 -T2
  27 [ #I #G #L /2 width=3 by ex2_intro/
  28 | #G #L #s /3 width=3 by cpm_sort, ex2_intro/
  29 | #n #G #K #V1 #V2 #W2 #_ * #V0 #HV10 #HV02 #HVW2
  30   elim (lifts_total V0 (𝐔❴1❵)) #W0 #HVW0
  31   lapply (cpm_lifts_bi … HV02 (Ⓣ) … (K.ⓓV1) … HVW0 … HVW2) -HVW2
  32   [ /3 width=1 by drops_refl, drops_drop/ ] -HV02 #HW02
  33   /3 width=3 by cpt_delta, ex2_intro/
  34 | #n #G #K #V1 #V2 #W2 #_ * #V0 #HV10 #HV02 #HVW2
  35   elim (lifts_total V0 (𝐔❴1❵)) #W0 #HVW0
  36   lapply (cpm_lifts_bi … HV02 (Ⓣ) … (K.ⓛV1) … HVW0 … HVW2) -HVW2
  37   [ /3 width=1 by drops_refl, drops_drop/ ] -HV02 #HW02
  38   /3 width=3 by cpt_ell, ex2_intro/
  39 | #n #I #G #K #T2 #U2 #i #_ * #T0 #HT0 #HT02 #HTU2
  40   elim (lifts_total T0 (𝐔❴1❵)) #U0 #HTU0
  41   lapply (cpm_lifts_bi … HT02 (Ⓣ) … (K.ⓘ{I}) … HTU0 … HTU2) -HTU2
  42   [ /3 width=1 by drops_refl, drops_drop/ ] -HT02 #HU02
  43   /3 width=3 by cpt_lref, ex2_intro/
  44 | #n #p #I #G #L #V1 #V2 #T1 #T2 #HV12 #_ #_ * #T0 #HT10 #HT02
  45   /3 width=5 by cpt_bind, cpm_bind, ex2_intro/
  46 | #n #G #L #V1 #V2 #T1 #T2 #HV12 #_ #_ * #T0 #HT10 #HT02
  47   /3 width=5 by cpt_appl, cpm_appl, ex2_intro/
  48 | #n #G #L #V1 #V2 #T1 #T2 #_ #_ * #V0 #HV10 #HV02 * #T0 #HT10 #HT02
  49   /3 width=5 by cpt_cast, cpm_cast, ex2_intro/
  50 | #n #G #L #V #U1 #T1 #T2 #HTU1 #_ * #T0 #HT10 #HT02
  51   elim (cpt_lifts_sn … HT10 (Ⓣ) … (L.ⓓV) … HTU1) -T1
  52   [| /3 width=1 by drops_refl, drops_drop/ ] #U0 #HTU0 #HU10
  53   /3 width=6 by cpt_bind, cpm_zeta, ex2_intro/
  54 | #n #G #L #U #T1 #T2 #_ * #T0 #HT10 #HT02
  55 | #n #G #L #U1 #U2 #T #_ * #U0 #HU10 #HU02
  56   /3 width=3 by cpt_ee, ex2_intro/
  57 | #n #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #_ #_ #_ * #T0 #HT10 #HT02
  58   /4 width=7 by cpt_appl, cpt_bind, cpm_beta, ex2_intro/
  59 | #n #p #G #L #V1 #V2 #V0 #W1 #W2 #T1 #T2 #HV12 #HW12 #_ #_ #_ * #T0 #HT10 #HT02 #HV20
  60   /4 width=9 by cpt_appl, cpt_bind, cpm_theta, ex2_intro/
  61 ]
  62
  63 (* Forward lemmas with t-bound rt-transition for terms **********************)
  64
  65 lemma cpt_fwd_cpm (h) (n) (G) (L):
  66       ∀T1,T2. ⦃G,L⦄ ⊢ T1 ⬆[h,n] T2 → ⦃G,L⦄ ⊢ T1 ➡[n,h] T2.