matita/matita/contribs/lambdadelta/basic_2A/etc/llpx_sn/lpx_conj.etc

   1 include "basic_2/relocation/lleq_alt.ma".
   2 include "basic_2/reduction/cpx_lleq.ma".
   3 include "basic_2/reduction/lpx_lleq.ma".
   4
   5 lemma not_ex_to_all_not: ∀A:Type[0]. ∀R:predicate A.
   6                          ((∃a. R a)→⊥) → (∀a. R a → ⊥).
   7 /3 width=2 by ex_intro/ qed-.
   8
   9 lemma lt_repl_sn_trans_tw: ∀L1,L2,T1,T2. ♯{L1, T1} < ♯{L2, T2} →
  10                            ∀U1. ♯{U1} = ♯{T1} → ♯{L1, U1} < ♯{L2, T2}.
  11 normalize in ⊢ (?→?→?→?→?%%→?→?→?%%); //
  12 qed-.
  13
  14 axiom cpx_fwd_lift1: ∀h,g,G,L,U1,U2. ⦃G, L⦄ ⊢ U1 ➡[h, g] U2 →
  15                      ∀T1,d,e. ⇧[d, e] T1 ≡ U1 → ∃T2. ⇧[d, e] T2 ≡ U2.
  16 (*
  17 #h #g #G #L #U1 #U2 #H elim H -G -L -U1 -U2
  18 [ * #i #G #L #T1 #d #e #H
  19   [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=2 by ex_intro/
  20   | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=2 by lift_lref_ge_minus, lift_lref_lt, ex_intro/
  21   | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=2 by ex_intro/
  22   ]
  23 | #G #L #k #l #Hkl #T1 #d #e #H
  24   lapply (lift_inv_sort2 … H) -H #H destruct /3 width=3 by ex_intro/
  25 | #I #G #L #K #V1 #V2 #W2 #i #HLK #HV12 #HVW2 #IHV2 #T1 #d #e #H
  26   elim (lift_inv_lref2 … H) -H * #Hid #H destruct
  27   [ elim (ldrop_conf_lt … HLK … HLV) -L // #L #U #HKL #HLV #HUV
  28     elim (IHV2 … HLV … HUV) -V #U2 #HUV2 #HU2
  29     elim (lift_trans_le … HUV2 … HVW2) -V2 // >minus_plus <plus_minus_m_m /3 width=9 by cpx_delta, ex2_intro/
  30   | elim (le_inv_plus_l … Hid) #Hdie #Hei
  31     lapply (ldrop_conf_ge … HLK … HLV ?) -L // #HKLV
  32     elim (lift_split … HVW2 d (i - e + 1)) -HVW2 /3 width=1 by le_S, le_S_S/ -Hid -Hdie
  33     #V1 #HV1 >plus_minus // <minus_minus /2 width=1 by le_S/ <minus_n_n <plus_n_O /3 width=9 by cpx_delta, ex2_intro/
  34   ]
  35 | #a #I #G #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #s #d #e #HLK #X #H
  36   elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
  37   elim (IHV12 … HLK … HWV1) -IHV12 #W2 #HW12 #HWV2
  38   elim (IHU12 … HTU1) -IHU12 -HTU1 /3 width=6 by cpx_bind, ldrop_skip, lift_bind, ex2_intro/
  39 | #I #G #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #s #d #e #HLK #X #H
  40   elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
  41   elim (IHV12 … HLK … HWV1) -V1
  42   elim (IHU12 … HLK … HTU1) -U1 -HLK /3 width=5 by cpx_flat, lift_flat, ex2_intro/
  43 | #G #L #V #U1 #U #U2 #_ #HU2 #IHU1 #K #s #d #e #HLK #X #H
  44   elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
  45   elim (IHU1 (K.ⓓW1) s … HTU1) /2 width=1/ -L -U1 #T #HTU #HT1
  46   elim (lift_div_le … HU2 … HTU) -U /3 width=5 by cpx_zeta, ex2_intro/
  47 | #G #L #V #U1 #U2 #_ #IHU12 #K #s #d #e #HLK #X #H
  48   elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
  49   elim (IHU12 … HLK … HTU1) -L -U1 /3 width=3 by cpx_tau, ex2_intro/
  50 | #G #L #V1 #V2 #U1 #_ #IHV12 #K #s #d #e #HLK #X #H
  51   elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
  52   elim (IHV12 … HLK … HWV1) -L -V1 /3 width=3 by cpx_ti, ex2_intro/
  53 | #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #K #s #d #e #HLK #X #HX
  54   elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct
  55   elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct
  56   elim (IHV12 … HLK … HV01) -V1 #V3 #HV32 #HV03
  57   elim (IHT12 (K.ⓛW0) s … HT01) -T1 /2 width=1 by ldrop_skip/ #T3 #HT32 #HT03
  58   elim (IHW12 … HLK … HW01) -W1
  59   /4 width=7 by cpx_beta, lift_bind, lift_flat, ex2_intro/
  60 | #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #K #s #d #e #HLK #X #HX
  61   elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct
  62   elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct
  63   elim (IHV1 … HLK … HV01) -V1 #V3 #HV3 #HV03
  64   elim (IHT12 (K.ⓓW0) s … HT01) -T1 /2 width=1 by ldrop_skip/ #T3 #HT32 #HT03
  65   elim (IHW12 … HLK … HW01) -W1 #W3 #HW32 #HW03
  66   elim (lift_trans_le … HV3 … HV2) -V
  67   /4 width=9 by cpx_theta, lift_bind, lift_flat, ex2_intro/
  68 ]
  69 qed-.
  70 *)
  71 lemma cpx_fwd_nlift2: ∀h,g,G,L,U1,U2. ⦃G, L⦄ ⊢ U1 ➡[h, g] U2 → ∀d,e.
  72                       (∀T2. ⇧[d, e] T2 ≡ U2 → ⊥) → (∀T1. ⇧[d, e] T1 ≡ U1 → ⊥).
  73 #h #g #G #L #U1 #U2 #HU12 #d #e #HnU2 #T1 #HTU1
  74 elim (cpx_fwd_lift1 … HU12 … HTU1) -L -U1 /2 width=2 by/
  75 qed-.
  76
  77 fact lleq_lpx_cpx_trans_aux: ∀h,g,G,T1,L1s,L1d,d. L1s ⋕[T1, d] L1d →
  78                              ∀Y,L2d. ⦃G, Y⦄ ⊢ ➡[h, g] L2d → Y = L1d → d = 0 →
  79                              ∀T2. ⦃G, L1d⦄ ⊢ T1 ➡[h, g] T2 →
  80                              ∃∃L2s. ⦃G, L1s⦄ ⊢ ➡[h, g] L2s & L2s ⋕[T2, d] L2d.
  81 #h #g #G #T1 #L1s @(f2_ind … rfw … L1s T1) -L1s -T1 #n #IH
  82 #Ys #U1 #Hn #Yd #d #HU1 elim (lleq_fwd_alt … HU1) #H #IHU1
  83 #Y #L2d * -Y -L2d
  84 [ -IH -IHU1 -HU1 #HY #Hd #U2 #HU12 destruct
  85   >(length_inv_zero_dx … H) -Ys /2 width=3 by ex2_intro/
  86 | #Id #L1d #L2d #W1d #W2d #HL12d #HW12d #HY #Hd #U2 #HU12 destruct
  87   elim (length_inv_pos_dx … H) -H #Is #L1s #W1s #_ #H destruct
  88   elim (is_lift_dec U1 0 1) [ -IHU1 -HW12d | -HU1 ]
  89   [ * #T1 #HTU1 lapply (lift_fwd_tw … HTU1) #H
  90     lapply (lleq_inv_lift_le … HU1 L1s L1d … HTU1 ?) -HU1 /2 width=1 by ldrop_drop/
  91     #HT1 elim (cpx_inv_lift1 … HU12 L1d … HTU1) -HU12 -HTU1 /2 width=4 by ldrop_drop/
  92     #T2 #HTU2 #HT12 elim (IH … HT1 … HL12d … HT12) /2 width=3 by lt_repl_sn_trans_tw/ -IH -HT1 -HT12 -H
  93     #L2s #HL12s #HT2 @(ex2_intro … (L2s.ⓑ{Is}W1s))
  94     /3 width=10 by lleq_lift_le, lpx_pair, ldrop_drop/ (**) (* full auto too slow *)
  95   | #HnU1 lapply (not_ex_to_all_not … HnU1) -HnU1 #HnU1
  96     elim (IHU1 … HnU1) [2,3,4: // |5,6,7,8,9,10: skip ] -HnU1 #H1 #H2 #HW1s destruct
  97     elim (IH … HW1s … HL12d … HW12d) // #L2s #HL12s #HW2d
  98     @(ex2_intro … (L2s.ⓑ{Id}W2d)) /3 width=3 by lleq_cpx_trans, lpx_pair/
  99     lapply (lleq_fwd_length … HW2d) #HL2sd -HW12d -HW1s
 100     @lleq_intro_alt [ normalize // ] -HL2sd
 101     #I2s #I2d #K2s #K2d #V2s #V2d #i @(nat_ind_plus … i) -i
 102     [ #_ #_ #HLK2s #HLK2d -IH -IHU1 -HU12 -HL12s -HL12d
 103       lapply (ldrop_inv_O2 … HLK2s) -HLK2s #H destruct
 104       lapply (ldrop_inv_O2 … HLK2d) -HLK2d #H destruct /2 width=1 by and3_intro/
 105     | #i #_ #_ #HnU2 #HLK2s #HLK2d
 106       lapply (cpx_fwd_nlift2 … HU12 … HnU2) -HU12 -HnU2 #HnU1
 107       lapply (ldrop_inv_drop1 … HLK2s) -HLK2s #HLK2s
 108       lapply (ldrop_inv_drop1 … HLK2d) -HLK2d #HLK2d
 109       elim (lpx_ldrop_trans_O1 … HL12s … HLK2s) -L2s #Y #HLK1s #H
 110       elim (lpx_inv_pair2 … H) -H #K1s #V1s #HK12s #HV12s #H destruct
 111       elim (lpx_ldrop_trans_O1 … HL12d … HLK2d) -L2d #Y #HLK1d #H
 112       elim (lpx_inv_pair2 … H) -H #K1d #V1d #HK12d #HV12d #H destruct
 113       elim (IHU1 … HnU1) [2,3,4: /2 width=2 by ldrop_drop/ | 5,6,7,8,9,10: skip ] -IHU1 -HnU1 -HLK1d
 114       #H1 #H2 #HV1d destruct
 115       lapply (ldrop_fwd_rfw … HLK1s) -HLK1s #H
 116       elim (IH … HV1d … HK12d … HV12d) // -IH -HV1d -HK12d -HV12d
 117       [ #Y #H1Y #H2Y
 118
 119
 120