matita/matita/contribs/lambdadelta/basic_2/etc/leq/lpx_leq.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/reduction/cpx_leq.ma".
  16 include "basic_2/reduction/lpx_ldrop.ma".
  17
  18 (**) (* to be proved later *)
  19 axiom- lleq_beta: ∀L2s,L2d,V2,W2,T2,d.
  20                   L2s.ⓛW2 ⋕[d+1, T2] L2d.ⓛW2 →
  21                   L2s.ⓓⓝW2.V2 ⋕[d+1, T2] L2d.ⓓⓝW2.V2.
  22
  23 (* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
  24
  25 (* Properties using equivalences for local environments *********************)
  26
  27 lemma lleq_cpx_conf_leq_dx: ∀h,g,G,L1s,L1d,T1,d. L1s ⋕[d, T1] L1d → L1s ≃[d, ∞] L1d →
  28                             ∀T2. ⦃G, L1d⦄ ⊢ T1 ➡[h, g] T2 →
  29                             ∀L2s. ⦃G, L1s⦄ ⊢ ➡[h, g] L2s → L1s ≃[0, d] L2s →
  30                             ∀L2d. ⦃G, L1d⦄ ⊢ ➡[h, g] L2d → L1d ≃[0, d] L2d →
  31                             L2s ≃[d, ∞] L2d → L2s ⋕[d, T2] L2d.
  32 #h #g #G #L1s #L1d #T1 #d #H elim H -L1s -L1d -T1 -d
  33 [ #L1s #L1d #d #k #_ #_ #X #H2 #L2s #_ #_ #L2d #_ #_ #H3
  34   lapply (leq_fwd_length … H3) -H3 #HL2sd
  35   elim (cpx_inv_sort1 … H2) -H2 [| * #l #_ ]
  36   #H destruct /2 width=1 by lleq_sort/
  37 | #Is #Id #L1s #L1d #K1s #K1d #V1s #V1d #d #i #Hid #HLK1s #HLK1d #_ #_ #_ #IHV1d #H1 #X #H2 #L2s #H1s #H2s #L2d #H1d #H2d #H3
  38   elim (ldrop_leq_conf_lt … H1 … HLK1s) -H1 /2 width=1 by ylt_inj/
  39   <yminus_SO2 >yminus_inj #Y #H1 #HY
  40   lapply (ldrop_mono … HY … HLK1d) -HY #H destruct
  41   elim (lpx_ldrop_conf … HLK1s … H1s) -H1s #Y #H #HLK2s
  42   elim (lpx_inv_pair1 … H) -H #K2s #V2s #H1s #HV12s #H destruct
  43   elim (lpx_ldrop_conf … HLK1d … H1d) -H1d #Y #H #HLK2d
  44   elim (lpx_inv_pair1 … H) -H #K2d #V2d #H1d #HV12d #H destruct
  45   elim (ldrop_leq_conf_be … H2s … HLK1s) -H2s /2 width=1 by ylt_inj/
  46   >yplus_O1 <yminus_SO2 >yminus_inj #Z #Y #X #HK12s #H
  47   lapply (ldrop_mono … H … HLK2s) -H #H destruct
  48   elim (ldrop_leq_conf_be … H2d … HLK1d) -H2d /2 width=1 by ylt_inj/
  49   >yplus_O1 <yminus_SO2 >yminus_inj #Z #Y #X #HK12d #H
  50   lapply (ldrop_mono … H … HLK2d) -H #H destruct
  51   elim (ldrop_leq_conf_lt … H3 … HLK2s) -H3 /2 width=1 by ylt_inj/
  52   <yminus_SO2 >yminus_inj #Y #H3 #HY
  53   lapply (ldrop_mono … HY … HLK2d) -HY #H destruct
  54   elim (cpx_inv_lref1 … H2) -H2 -L1s
  55   [ -L1d #H destruct /3 width=15 by lleq_skip/
  56   | * #Z #Y #X1 #X2 #H #HX12 #HX2 lapply (ldrop_mono … H … HLK1d) -L1d
  57     #H destruct >(plus_minus_m_m d (i+1)) //
  58     lapply (ldrop_fwd_ldrop2 … HLK2s) -HLK2s
  59     lapply (ldrop_fwd_ldrop2 … HLK2d) -HLK2d
  60     /3 width=9 by lleq_lift_ge/
  61   ]
  62 | #I #L1s #L1d #K1s #K1d #V1 #d #i #Hdi #HLK1s #HLK1d #_ #IHV1 #H1 #X #H2 #L2s #H1s #H2s #L2d #H1d #H2d #H3
  63   elim (ldrop_leq_conf_be … H1 … HLK1s) -H1 /2 width=1 by ylt_Y, yle_inj/ #Z #Y #X #H1 #HY
  64   lapply (ldrop_mono … HY … HLK1d) -HY #H destruct
  65   elim (lpx_ldrop_conf … HLK1s … H1s) -H1s #Y #H #HLK2s
  66   elim (lpx_inv_pair1 … H) -H #K2s #V2s #H1s #HV12s #H destruct
  67   elim (lpx_ldrop_conf … HLK1d … H1d) -H1d #Y #H #HLK2d
  68   elim (lpx_inv_pair1 … H) -H #K2d #V2d #H1d #HV12d #H destruct
  69   lapply (ldrop_leq_conf_ge … H2s … HLK1s ?) /2 width=1 by yle_inj/ #H
  70   lapply (ldrop_mono … H … HLK2s) -H #H destruct
  71   lapply (ldrop_leq_conf_ge … H2d … HLK1d ?) /2 width=1 by yle_inj/ #H
  72   lapply (ldrop_mono … H … HLK2d) -H #H destruct
  73   elim (ldrop_leq_conf_be … H3 … HLK2s) -H3 /2 width=1 by ylt_Y, yle_inj/
  74   >yminus_Y_inj #Z #Y #X #H3 #HY
  75   lapply (ldrop_mono … HY … HLK2d) -HY #H destruct
  76   elim (cpx_inv_lref1 … H2) -H2 -L1s
  77   [ -L1d #H destruct /3 width=12 by lleq_lref/
  78   | * #Z #Y #X1 #X2 #H #HX12 #HX2 lapply (ldrop_mono … H … HLK1d) -L1d
  79     #H destruct
  80     lapply (ldrop_fwd_ldrop2 … HLK2s) -HLK2s #HLK2s
  81     lapply (ldrop_fwd_ldrop2 … HLK2d) -HLK2d #HLK2d
  82     @(lleq_ge … 0) /3 width=10 by lleq_lift_le/ (**) (* full auto too slow *)
  83   ]
  84 | #L1s #L1d #d #i #HL1s #HL1d #_ #_ #X #H2 #L2s #_ #_ #L2s #_ #H2d #H3
  85   lapply (leq_fwd_length … H2d) -H2d
  86   lapply (leq_fwd_length … H3) -H3
  87   elim (cpx_inv_lref1 … H2) -H2
  88   [ #H destruct /2 width=1 by lleq_free/
  89   | -L1s * #I #K1d #V1 #V2 #HLK1d
  90     lapply (ldrop_fwd_length_lt2 … HLK1d) -HLK1d #H
  91     elim (lt_refl_false … i) /2 width=3 by lt_to_le_to_lt/ (**) (* full auto too slow *)
  92   ]
  93 | #L1s #L1d #d #k #_ #_ #X #H2 #L2s #_ #_ #L2d #_ #_ #H3
  94   lapply (leq_fwd_length … H3) -H3 #HL2sd
  95   lapply (cpx_inv_gref1 … H2) -H2
  96   #H destruct /2 width=1 by lleq_gref/
  97 | #a #I #L1s #L1d #V1 #T1 #d #HV1 #_ #IHV1 #IHT1 #H1 #X #H2 #L2s #H1s #H2s #L2d #H1d #H2d #H3
  98   elim (cpx_inv_bind1 … H2) -H2 *
  99   [ #V2 #T2 #HV12 #HT12 #H destruct
 100     /5 width=5 by lpx_pair, lleq_cpx_trans_leq, lleq_bind, leq_pair, leq_succ/
 101   | #T2 #HT12 #HT2X #H1 #H2 destruct >(minus_plus_m_m d 1)
 102     /4 width=9 by lpx_pair, lleq_inv_lift_ge, ldrop_ldrop, leq_pair, leq_succ/
 103   ]
 104 | #I #L1s #L1d #V1 #T1 #d #HV1 #_ #IHV1 #IHT1 #H1 #X #H2 #L2s #H1s #H2s #L2d #H1d #H2d #H3
 105   elim (cpx_inv_flat1 … H2) -H2 *
 106   [ #V2 #T2 #HV12 #HT12 #H destruct /3 width=1 by lleq_flat/
 107   | #HT1X #H destruct /2 width=1 by/
 108   | #HV1X #H destruct /2 width=1 by/
 109   | #a #V2 #W1 #W2 #T0 #T2 #HV12 #HW12 #HT02 #H1 #H2 #H3 destruct
 110     lapply (IHT1 … (ⓛ{a}W2.T2) … L2s … L2d ? ? ?) -IHT1 /2 width=1 by cpx_bind/ #H
 111     elim (lleq_inv_bind … H) -H -HW12 -HT02 #HW2 #HT2
 112     /4 width=1 by lleq_beta, lleq_flat, lleq_bind/
 113   | #a #V0 #V2 #W1 #W2 #T0 #T2 #HV10 #HV02 #HW12 #HT02 #H1 #H2 #H3 destruct
 114     lapply (IHT1 … (ⓓ{a}W2.T2) … L2s … L2d ? ? ?) -IHT1 /2 width=1 by cpx_bind/ #H
 115     elim (lleq_inv_bind … H) -H -HW12 -HT02
 116     /5 width=9 by lleq_lift_ge, lleq_flat, lleq_bind, ldrop_ldrop/
 117   ]
 118 ]
 119 qed-.
 120
 121 lemma lleq_cpx_conf_dx: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 →
 122                         ∀L1. L1 ⋕[0, T1] L2 → L1 ⋕[0, T2] L2.
 123 #h #g #G #L2 #T1 #T2 #HT12 #L1 #HT1 lapply (lleq_fwd_length … HT1)
 124 /3 width=13 by lleq_cpx_conf_leq_dx, leq_O_Y/
 125 qed-.