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