matita/matita/contribs/lambdadelta/basic_2/etc/cpt/cpt_cpm.etc

   1 (* Properties with t-bound rt-transition for terms **************************)
   2
   3 axiom cpt_total (h) (n) (G) (L) (T):
   4       ∃U. ⦃G,L⦄ ⊢ T ⬆[h,n] U.
   5
   6 lemma pippo (h) (G) (L) (T0):
   7       ∀T1. ⦃G,L⦄ ⊢ T1 ➡[h] T0 → ∀n,T2. ⦃G,L⦄ ⊢ T0 ⬆[h,n] T2 →
   8       ∃∃T. ⦃G,L⦄ ⊢ T1 ⬆[h,n] T & ⦃G,L⦄ ⊢ T ➡[h] T2.
   9 #h #G #L #T0 #T1 #H
  10 @(cpr_ind … H) -G -L -T0 -T1
  11 [ #I #G #L #n #T2 #HT2
  12   /2 width=3 by ex2_intro/
  13 | #G #K #V1 #V0 #W0 #_ #IH #HVW0 #n #T2 #HT2
  14   elim (cpt_inv_lifts_sn … HT2 (Ⓣ) … K … HVW0) -W0
  15   [| /3 width=1 by drops_refl, drops_drop/ ] #V2 #HVT2 #HV02
  16   elim (IH … HV02) -V0 #V0 #HV10 #HV02
  17 |
  18 |
  19 |
  20 |
  21 |
  22 | #p #G #L #V1 #V0 #W1 #W0 #T1 #T0 #_ #_ #_ #IHV #IHW #IHT #n #X #HX
  23   elim (cpt_inv_bind_sn … HX) -HX #X0 #T2 #HX #HT02 #H destruct
  24   elim (cpt_inv_cast_sn … HX) -HX *
  25   [ #W2 #V2 #HW02 #HV02 #H destruct
  26     elim (cpt_total h n G (L.ⓛW1) T0) #T3 #HT03
  27     elim (IHV … HV02) -V0 #V0 #HV10 #HV02
  28     elim (IHW … HW02) -W0 #W0 #HW10 #HW02
  29     elim (IHT … HT02) -T0 #T0 #HT10 #HT02
  30     @(ex2_intro … (ⓐV0.ⓛ{p}W0.T0))
  31     [ /3 width=1 by cpt_appl, cpt_bind/
  32     | @(cpm_beta … HV02 HW02)
  33
  34   | #m #_ #H destruct
  35   ]
  36
  37 lemma cpm_cpt_cpr (h) (n) (G) (L):
  38       ∀T1,T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 →
  39       ∃∃T0. ⦃G,L⦄ ⊢ T1 ⬆[h,n] T0 & ⦃G,L⦄ ⊢ T0 ➡[h] T2.
  40 #h #n #G #L #T1 #T2 #H
  41 @(cpm_ind … H) -n -G -L -T1 -T2
  42 [ #I #G #L /2 width=3 by ex2_intro/
  43 | #G #L #s /3 width=3 by cpm_sort, ex2_intro/
  44 | #n #G #K #V1 #V2 #W2 #_ * #V0 #HV10 #HV02 #HVW2
  45   elim (lifts_total V0 (𝐔❴1❵)) #W0 #HVW0
  46   lapply (cpm_lifts_bi … HV02 (Ⓣ) … (K.ⓓV1) … HVW0 … HVW2) -HVW2
  47   [ /3 width=1 by drops_refl, drops_drop/ ] -HV02 #HW02
  48   /3 width=3 by cpt_delta, ex2_intro/
  49 | #n #G #K #V1 #V2 #W2 #_ * #V0 #HV10 #HV02 #HVW2
  50   elim (lifts_total V0 (𝐔❴1❵)) #W0 #HVW0
  51   lapply (cpm_lifts_bi … HV02 (Ⓣ) … (K.ⓛV1) … HVW0 … HVW2) -HVW2
  52   [ /3 width=1 by drops_refl, drops_drop/ ] -HV02 #HW02
  53   /3 width=3 by cpt_ell, ex2_intro/
  54 | #n #I #G #K #T2 #U2 #i #_ * #T0 #HT0 #HT02 #HTU2
  55   elim (lifts_total T0 (𝐔❴1❵)) #U0 #HTU0
  56   lapply (cpm_lifts_bi … HT02 (Ⓣ) … (K.ⓘ{I}) … HTU0 … HTU2) -HTU2
  57   [ /3 width=1 by drops_refl, drops_drop/ ] -HT02 #HU02
  58   /3 width=3 by cpt_lref, ex2_intro/
  59 | #n #p #I #G #L #V1 #V2 #T1 #T2 #HV12 #_ #_ * #T0 #HT10 #HT02
  60   /3 width=5 by cpt_bind, cpm_bind, ex2_intro/
  61 | #n #G #L #V1 #V2 #T1 #T2 #HV12 #_ #_ * #T0 #HT10 #HT02
  62   /3 width=5 by cpt_appl, cpm_appl, ex2_intro/
  63 | #n #G #L #V1 #V2 #T1 #T2 #_ #_ * #V0 #HV10 #HV02 * #T0 #HT10 #HT02
  64   /3 width=5 by cpt_cast, cpm_cast, ex2_intro/
  65 | #n #G #L #V #U1 #T1 #T2 #HTU1 #_ * #T0 #HT10 #HT02
  66   elim (cpt_lifts_sn … HT10 (Ⓣ) … (L.ⓓV) … HTU1) -T1
  67   [| /3 width=1 by drops_refl, drops_drop/ ] #U0 #HTU0 #HU10
  68   /3 width=6 by cpt_bind, cpm_zeta, ex2_intro/
  69 | #n #G #L #U #T1 #T2 #_ * #T0 #HT10 #HT02
  70 | #n #G #L #U1 #U2 #T #_ * #U0 #HU10 #HU02
  71   /3 width=3 by cpt_ee, ex2_intro/
  72 | #n #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #_ #_ #_ * #T0 #HT10 #HT02
  73   /4 width=7 by cpt_appl, cpt_bind, cpm_beta, ex2_intro/
  74 | #n #p #G #L #V1 #V2 #V0 #W1 #W2 #T1 #T2 #HV12 #HW12 #_ #_ #_ * #T0 #HT10 #HT02 #HV20
  75   /4 width=9 by cpt_appl, cpt_bind, cpm_theta, ex2_intro/
  76 ]
  77
  78 (* Forward lemmas with t-bound rt-transition for terms **********************)
  79
  80 lemma pippo (h) (G) (L) (T0):
  81       ∀T1. ⦃G,L⦄ ⊢ T1 ➡[h] T0 →
  82       ∀n,T2. ⦃G,L⦄ ⊢ T0 ⬆[h,n] T2 → ⦃G,L⦄ ⊢ T1 ➡[n,h] T2.
  83 #h #G #L #T0 #T1 #H
  84 @(cpr_ind … H) -G -L -T0 -T1
  85 [ #I #G #L #n #T2 #HT2
  86   /2 width=1 by cpt_fwd_cpm/
  87 | #G #K #V1 #V0 #W0 #_ #IH #HVW0 #n #T2 #HT2
  88   elim (cpt_inv_lifts_sn … HT2 (Ⓣ) … K … HVW0) -W0
  89   [| /3 width=1 by drops_refl, drops_drop/ ] #V2 #HVT2 #HV02
  90   lapply (IH … HV02) -V0 #HV12
  91   /2 width=3 by cpm_delta/
  92 |
  93 |
  94 |
  95 |
  96 |
  97 | #p #G #L #V1 #V0 #W1 #W0 #T1 #T0 #_ #_ #_ #IHV #IHW #IHT #n #X #HX
  98   elim (cpt_inv_bind_sn … HX) -HX #X0 #T2 #HX #HT02 #H destruct
  99   elim (cpt_inv_cast_sn … HX) -HX *
 100   [ #W2 #V2 #HW02 #HV02 #H destruct
 101     elim (cpt_total h n G (L.ⓛW1) T0) #T2 #HT02
 102     lapply (IHV … HV02) -V0 #HV12
 103     lapply (IHW … HW02) -W0 #HW12
 104     lapply (IHT … HT02) -T0 #HT12
 105     @(cpm_beta … HV12 HW12) //
 106
 107   | #m #_ #H destruct
 108   ]