matita/matita/contribs/lambdadelta/basic_2/etc/cpr_cpm.etc

   1 include "basic_2/rt_transition/cpm_drops.ma".
   2 include "basic_2/rt_transition/cpr.ma".
   3 (*
   4 theorem cpm_cpm_trans_swap (h) (G) (L) (T1):
   5         ∀n1,T. ⦃G,L⦄ ⊢ T1 ➡[n1,h] T → ∀n2,T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 → n1 ≤ n2 →
   6         ∃∃T0. ⦃G,L⦄ ⊢ T1 ➡[n2,h] T0 & ⦃G,L⦄ ⊢ T0 ➡[n1,h] T2.
   7 #h #G #L #T1 #n1 #T #H
   8 @(cpm_ind … H) -n1 -G -L -T1 -T
   9 [ #I #G #L #n2 #T2 #HT2 #_ /2 width=3 by ex2_intro/
  10 | #G #L #s #n2 #X2 #H #_
  11   elim (cpm_inv_sort1 … H) -H #H #Hn2 destruct >iter_n_Sm
  12   /3 width=3 by cpm_sort, ex2_intro/
  13 | #n1 #G #K #V1 #V #W #_ #IH #HVW #n2 #T2 #HT2 #Hn
  14   elim (cpm_inv_lifts_sn … HT2 (Ⓣ) … HVW) -W
  15   [|*: /3 width=2 by drops_refl, drops_drop/ ] #V2 #HVT2 #HV2
  16   elim (IH … HV2) -V [| // ] #V0 #HV10 #HV02
  17   elim (lifts_total V0 (𝐔❴1❵)) #T0 #HVT0
  18   lapply (cpm_lifts_bi … HV02 (Ⓣ) … (K.ⓓV1) … HVT0 … HVT2) -V2
  19   [ /3 width=2 by drops_refl, drops_drop/ ] #HT02
  20   /3 width=3 by cpm_delta, ex2_intro/
  21 | #n1 #G #K #V1 #V #W #_ #IH #HVW #m2 #T2 #HT2 #H
  22   elim (le_inv_S1 … H) -H #n2 #Hn #H destruct
  23   elim (cpm_inv_lifts_sn … HT2 (Ⓣ) … HVW) -W
  24   [|*: /3 width=2 by drops_refl, drops_drop/ ] #V2 #HVT2 #HV2
  25   elim (IH … HV2) -V [| /2 width=1 by le_S/ ] #V0 #HV10 #HV02
  26   elim (lifts_total V0 (𝐔❴1❵)) #T0 #HVT0
  27   lapply (cpm_lifts_bi … HV02 (Ⓣ) … (K.ⓛV1) … HVT0 … HVT2) -V2
  28   [ /3 width=2 by drops_refl, drops_drop/ ] #HT02
  29   /3 width=5 by cpm_ell, ex2_intro/
  30 *)
  31
  32 (* Note: cpm_cpm_trans_swap does not hold: take L = K.ⓛV1, T1 = #0, n2 = 0 *)
  33 theorem cpr_cpm_trans_swap (h) (G) (L):
  34         ∀T1,T. ⦃G,L⦄ ⊢ T1 ➡[h] T → ∀n2,T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 →
  35         ∃∃T0. ⦃G,L⦄ ⊢ T1 ➡[n2,h] T0 & ⦃G,L⦄ ⊢ T0 ➡[h] T2.
  36 #h #G #L #T1 #T #H
  37 @(cpr_ind … H) -G -L -T1 -T
  38 [ #I #G #L #n2 #T2 #HT2 /2 width=3 by ex2_intro/
  39 | #G #K #V1 #V #W #_ #IH #HVW #n2 #T2 #HT2
  40   elim (cpm_inv_lifts_sn … HT2 (Ⓣ) … HVW) -W
  41   [|*: /3 width=2 by drops_refl, drops_drop/ ] #V2 #HVT2 #HV2
  42   elim (IH … HV2) -V #V0 #HV10 #HV02
  43   elim (lifts_total V0 (𝐔❴1❵)) #T0 #HVT0
  44   lapply (cpm_lifts_bi … HV02 (Ⓣ) … (K.ⓓV1) … HVT0 … HVT2) -V2
  45   [ /3 width=2 by drops_refl, drops_drop/ ] #HT02
  46   /3 width=3 by cpm_delta, ex2_intro/
  47 | #I #G #K #T #U #i #_ #IH #HTU #n2 #U2 #HU2
  48   elim (cpm_inv_lifts_sn … HU2 (Ⓣ) … HTU) -U
  49   [|*: /3 width=2 by drops_refl, drops_drop/ ] #T2 #HTU2 #HT2
  50   elim (IH … HT2) -T #T0 #HT0 #HT02
  51   elim (lifts_total T0 (𝐔❴1❵)) #U0 #HTU0
  52   lapply (cpm_lifts_bi … HT02 (Ⓣ) … (K.ⓘ{I}) … HTU0 … HTU2) -T2
  53   [ /3 width=2 by drops_refl, drops_drop/ ] #HU02
  54   /3 width=3 by cpm_lref, ex2_intro/
  55 | #p #I #G #L #V1 #V #T1 #T #_ #_ #IHV #IHT #n2 #X2 #H
  56   elim (cpm_inv_bind1 … H) -H *
  57   [ #V2 #T2 #HV2 #HT2 #H destruct