matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_frees.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/multiple/fqup.ma".
  16 include "basic_2/multiple/frees_lift.ma".
  17 include "basic_2/reduction/lpx_ldrop.ma".
  18
  19 (* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
  20 (*
  21 lemma cofrees_lsuby_conf: ∀L1,U,i. L1 ⊢ i ~ϵ 𝐅*⦃U⦄ →
  22                           ∀L2. lsuby L1 L2 → L2 ⊢ i ~ϵ 𝐅*⦃U⦄.
  23 /3 width=3 by lsuby_cpys_trans/ qed-.
  24
  25 lemma lpx_cpx_cofrees_conf: ∀h,g,G,L1,U1,U2. ⦃G, L1⦄ ⊢ U1 ➡[h, g] U2 →
  26                             ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 →
  27                             ∀i. L1 ⊢ i ~ϵ 𝐅*⦃U1⦄ → L2 ⊢ i ~ϵ 𝐅*⦃U2⦄.
  28 #h #g #G #L1 #U1 @(fqup_wf_ind_eq … G L1 U1) -G -L1 -U1
  29 #G0 #L0 #U0 #IH #G #L1 * *
  30 [ -IH #k #HG #HL #HU #U2 #H elim (cpx_inv_sort1 … H) -H
  31   [| * #l #_ ] #H destruct //
  32 | #j #HG #HL #HU #U2 #H #L2 #HL12 #i #Hi elim (cpx_inv_lref1 … H) -H
  33   [ #H destruct elim (lt_or_eq_or_gt i j) #Hji
  34     [ -IH -HL12 /2 width=4 by cofrees_lref_gt/
  35     | -IH -HL12 destruct elim (cofrees_inv_lref_eq … Hi)
  36     | elim (lt_or_ge j (|L2|)) /2 width=5 by cofrees_lref_free/ #Hj
  37       elim (ldrop_O1_lt (Ⓕ) L1 j) [2: >(lpx_fwd_length … HL12) // ] #I #K1 #W1 #HLK1
  38       elim (lpx_ldrop_conf … HLK1 … HL12) -HL12 #Y #H #HLK2
  39       elim (lpx_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct
  40       lapply (cofrees_inv_lref_lt … Hi … HLK1) -Hi // #HW1
  41       lapply (IH … HW12 … HK12 … HW1) /2 width=2 by fqup_lref/ -L1 -K1 -W1 #HW2
  42       /2 width=9 by cofrees_lref_lt/ (**) (* full auto too slow *)
  43     ]
  44   | * #I #K1 #W1 #W0 #HLK1 #HW10 #HW0U2 elim (lt_or_ge j i) #Hji
  45     [ lapply (ldrop_fwd_drop2 … HLK1) #H0
  46       elim (lpx_ldrop_conf … H0 … HL12) #K2 #HK12 #HLK2
  47       @(cofrees_lift_ge … HLK2 … HW0U2) //
  48       @(IH … HW10) /2 width=2 by fqup_lref/ -L2 -K2 -W0 -U2 -IH
  49       <minus_plus /2 width=7 by cofrees_inv_lref_lt/
  50     | -IH lapply (ldrop_fwd_drop2 … HLK1) -HLK1 #HLK1
  51       elim (lpx_ldrop_conf … HLK1 … HL12) -I -L1 -W1
  52       /2 width=12 by cofrees_lift_be/
  53     ]
  54   ]
  55 | -IH #p #HG #HL #HU #U2 #H lapply (cpx_inv_gref1 … H) -H
  56   #H destruct //
  57 | #a #I #W1 #U1 #HG #HL #HU #X #HX #L2 #HL12 #i #Hi destruct
  58   elim (cofrees_inv_bind … Hi) -Hi #HW1 #HU1
  59   elim (cpx_inv_bind1 … HX) -HX
  60   [ * #W2 #U2 #HW12 #HU12 #H destruct /4 width=8 by cofrees_bind, lpx_pair/
  61   |
  62   ]
  63 | #I #W1 #X1 #HG #HL #HU #X2 #HX2 #L2 #HL12 #i #Hi destruct
  64   elim (cofrees_inv_flat … Hi) -Hi #HW1 #HX1
  65   elim (cpx_inv_flat1 … HX2) -HX2 *
  66   [ #W2 #U2 #HW12 #HU12 #H destruct /3 width=7 by cofrees_flat/
  67   | #HU12 #H destruct /2 width=7 by/
  68   | #HW12 #H destruct /2 width=7 by/
  69   | #b #W2 #V1 #V2 #U1 #U2 #HW12 #HV12 #HU12 #H1 #H2 #H3 destruct
  70     elim (cofrees_inv_bind … HX1) -HX1 #HV1 #HU1
  71     @cofrees_bind [ /3 width=7 by cofrees_flat/ ]
  72     @(cofrees_lsuby_conf (L2.ⓛV2)) /3 width=7 by lpx_pair, lsuby_succ/
  73   |
  74
  75
  76 *)