matita/matita/contribs/lambdadelta/basic_2/computation/lcosx_cpx.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/computation/lsx_drop.ma".
  16 include "basic_2/computation/lsx_lpx.ma".
  17 include "basic_2/computation/lsx_lpxs.ma".
  18 include "basic_2/computation/lcosx.ma".
  19
  20 (* SN EXTENDED STRONGLY CONORMALIZING LOCAL ENVIRONMENTS ********************)
  21
  22 (* Properties on extended context-sensitive parallel reduction for term *****)
  23
  24 lemma lsx_cpx_trans_lcosx: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, o] T2 →
  25                            ∀l. G ⊢ ~⬊*[h, o, l] L →
  26                            G ⊢ ⬊*[h, o, T1, l] L → G ⊢ ⬊*[h, o, T2, l] L.
  27 #h #o #G #L #T1 #T2 #H elim H -G -L -T1 -T2 //
  28 [ #I #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #l #HL #H
  29   elim (ylt_split i l) #Hli [ -H | -HL ]
  30   [ <(ymax_pre_sn l (⫯i)) /2 width=1 by ylt_fwd_le_succ1/
  31     elim (lcosx_drop_trans_lt … HL … HLK) // -HL -Hli
  32     lapply (drop_fwd_drop2 … HLK) -HLK /3 width=7 by lsx_lift_ge/
  33   | lapply (lsx_fwd_lref_be … H … HLK) // -H -Hli
  34     lapply (drop_fwd_drop2 … HLK) -HLK
  35     /4 width=10 by lsx_ge, lsx_lift_le/
  36   ]
  37 | #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #l #HL #H
  38   elim (lsx_inv_bind … H) -H #HV1 #HT1
  39   @lsx_bind /2 width=2 by/ (**) (* explicit constructor *)
  40   @(lsx_lreq_conf … (L.ⓑ{I}V1)) /3 width=1 by lcosx_pair, lreq_succ/
  41 | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #l #HL #H
  42   elim (lsx_inv_flat … H) -H /3 width=1 by lsx_flat/
  43 | #G #L #V #U1 #U2 #T2 #_ #HTU2 #IHU12 #l #HL #H
  44   elim (lsx_inv_bind … H) -H #HV #HU1
  45   <(ypred_succ l) <yminus_SO2
  46   /4 width=7 by lcosx_pair, lsx_inv_lift_ge, drop_drop/
  47 | #G #L #V #T1 #T2 #_ #IHT12 #l #HL #H
  48   elim (lsx_inv_flat … H) -H /2 width=1 by/
  49 | #G #L #V1 #V2 #T #_ #IHV12 #l #HL #H
  50   elim (lsx_inv_flat … H) -H /2 width=1 by/
  51 | #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #l #HL #H
  52   elim (lsx_inv_flat … H) -H #HV1 #H
  53   elim (lsx_inv_bind … H) -H #HW1 #HT1
  54   @lsx_bind /3 width=1 by lsx_flat/ (**) (* explicit constructor *)
  55   @(lsx_lreq_conf … (L.ⓛW1)) /3 width=1 by lcosx_pair, lreq_succ/
  56 | #a #G #L #V1 #V2 #U2 #W1 #W2 #T1 #T2 #_ #HVU2 #_ #_ #IHV12 #IHW12 #IHT12 #l #HL #H
  57   elim (lsx_inv_flat … H) -H #HV1 #H
  58   elim (lsx_inv_bind … H) -H #HW1 #HT1
  59   @lsx_bind /2 width=1 by/ (**) (* explicit constructor *)
  60   @lsx_flat [ <yplus_SO2 /3 width=7 by lsx_lift_ge, drop_drop/ ]
  61   @(lsx_lreq_conf … (L.ⓓW1)) /3 width=1 by lcosx_pair, lreq_succ/
  62 ]
  63 qed-.
  64
  65 lemma lsx_cpx_trans_O: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, o] T2 →
  66                        G ⊢ ⬊*[h, o, T1, 0] L → G ⊢ ⬊*[h, o, T2, 0] L.
  67 /2 width=3 by lsx_cpx_trans_lcosx/ qed-.