matita/matita/contribs/lambdadelta/basic_2/etc/llor/lpxs_llor.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/relocation/llor.ma".
  16 include "basic_2/computation/cpxs_lleq.ma".
  17 include "basic_2/computation/lpxs_ldrop.ma".
  18 include "basic_2/computation/lpxs_cpxs.ma".
  19 include "basic_2/computation/lpxs_lpxs.ma".
  20
  21 (* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
  22
  23 axiom llor_fwd_sort: ∀L1,L2,L,d,k. L1 ⩖ [⋆k, d] L2 ≡ L → L = L2.
  24
  25 axiom llor_fwd_lref: ∀L1,L2,L,d,i. L1 ⩖ [#i, d] L2 ≡ L →
  26                      ∨∨ (|L| ≤ i ∧ L = L2)
  27                       | (yinj i < d ∧ L = L2)
  28                       | ∃∃I1,I2,K1,K2,K,V1,V2. ⇩[i] L1 ≡ K1.ⓑ{I1}V1 &
  29                                                ⇩[i] L2 ≡ K2.ⓑ{I2}V2 &
  30                                                ⇩[i] L ≡ K.ⓑ{I2}V1 &
  31                                                L2 ≃[yinj 0, yinj i] L &
  32                                                K1 ⩖[V1, yinj 0] K2 ≡ K &
  33                                                d ≤ yinj i.
  34
  35
  36 axiom llor_fwd_lref_lt: ∀L1,L2,L,d,i. L1 ⩖ [#i, d] L2 ≡ L → i < d → L = L2.
  37
  38 axiom llor_inv_lref_be: ∀L1,L2,L,d,i. L1 ⩖ [#i, d] L2 ≡ L → d ≤ i →
  39                         ∀I1,I2,K1,K2,V1,V2. ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
  40                         ∃∃K. ⇩[i] L ≡ K.ⓑ{I2}V1 & L2 ≃[0, i] L &
  41                              K1 ⩖[V1, 0] K2 ≡ K.
  42
  43 axiom llor_fwd_gref: ∀L1,L2,L,d,p. L1 ⩖ [§p, d] L2 ≡ L → L = L2.
  44
  45 axiom llor_inv_bind: ∀a,I,L1,L2,L,V,T,d. L1 ⩖ [ⓑ{a,I}V.T, d] L2 ≡ L →
  46                      ∃∃L0. L1 ⩖ [V, d] L2 ≡ L0 & L1.ⓑ{I}V ⩖ [T, ⫯d] L0.ⓑ{I}V ≡ L.ⓑ{I}V.
  47
  48 axiom llor_inv_flat: ∀I,L1,L2,L,V,T,d. L1 ⩖ [ⓕ{I}V.T, d] L2 ≡ L →
  49                      ∃∃L0. L1 ⩖ [V, d] L2 ≡ L0 & L1 ⩖ [T, d] L0 ≡ L.
  50
  51 axiom llor_fwd_length_13: ∀L1,L2,L,T,d. L1 ⩖ [T, d] L2 ≡ L → |L1| = |L|.
  52
  53 (* Properties obn lazy union for local environments *************************)
  54
  55 lemma lpxs_llor_sn: ∀h,g,G,L1s,L0,L1d,T,d. L1s ⩖[T, d] L0 ≡ L1d →
  56                     ∀L2s,L2d. L2s ⩖[T, d] L0 ≡ L2d →
  57                     ⦃G, L1s⦄ ⊢ ➡*[h, g] L2s → ⦃G, L1d⦄ ⊢ ➡*[h, g] L2d.
  58 #h #g #G #L1s #L0 #L1d #T #d #H elim H -L1s -L0 -L1d -T -d
  59 [ #L1s #L0 #d #k #_ #L2s #L2d #H #_ >(llor_fwd_sort … H) //
  60 | #L1s #L0 #d #i #_ #Hid #L2s #L2d #H #_ >(llor_fwd_lref_lt … H) //
  61 | #I1s #I0 #L1s #L0 #L1d #K1s #K0 #K1d #V1s #V0 #d #i #Hdi #HLK1s #HLK0 #HLK1d #HL01d #HV1s #IHV1s #L2s #L2d #H #HL12s
  62   elim (lpxs_ldrop_conf … HLK1s … HL12s) -L1s #Y #H #HLK2s
  63   elim (lpxs_inv_pair1 … H) -H #K2s #V2s #HK12s #HV12s #H destruct
  64   elim (llor_inv_lref_be … H … HLK2s HLK0) // -L2s -HLK0 -Hdi #K2d #HLK2d #HL02d #HV2s
  65   lapply (leq_canc_sn … HL01d … HL02d) -L0 #HL12d
  66   lapply (IHV1s … K2d … HK12s) -IHV1s -HK12s [2: #HK12d
  67
  68
  69
  70
  71 [ #I2d #I1s #L2d #L1s #L2s #K2d #K1s #K2s #V2d #V1s #d #i #Hdi #HLK2d #HLK1s #HLK2s #HL12s #_ #IHV2s #L1d #HL1sd #HL12d
  72   elim (lpxs_ldrop_trans_O1 … HL12d … HLK2d) -L2d #Y #HLK1d #H
  73   elim (lpxs_inv_pair2 … H) -H #K1d #V1d #HK12d #HV12d #H destruct
  74   elim (lleq_inv_lref_ge … HL1sd … HLK1s HLK1d) // -d -I2d #H #HV1d destruct
  75   lapply (lleq_cpxs_conf_dx … HV12d … HV1d) #HV2d
  76   lapply (lleq_cpxs_trans … HV12d … HV1d) -HV12d -HV1d #HV12d
  77   lapply (IHV2s … HV2d HK12d) -L1d -K1d -K2d #HK12s
  78   elim (ldrop_lpxs_trans h g G … HLK1s (K2s.ⓑ{I1s}V2d)) /2 width=1 by lpxs_pair/ -V1d -K1s #Y #HL1sY #HYK2s #H
  79   lapply (leq_canc_sn … HL12s … H) -HL12s -H #HL2sY
  80   lapply (ldrop_O_inj … HLK2s HYK2s) -I1s -K2s -V2d #H
  81   lapply (leq_join … HL2sY … H) -HL2sY -H #HL2sY
  82   >(leq_inv_O_Y … HL2sY) -HL2sY //
  83
  84
  85
  86
  87
  88 lemma lleq_lpxs_trans_llor: ∀h,g,G,L1s,L2s,L2d,T,d. L2d ⩖[T, d] L1s ≡ L2s →
  89                             ∀L1d. L1s ⋕[T, d] L1d → ⦃G, L1d⦄ ⊢ ➡*[h, g] L2d → ⦃G, L1s⦄ ⊢ ➡*[h, g] L2s.
  90 #h #g #G #L1s #L2s #L2d #T #d #H elim H -L1s -L2s -L2d -T -d //
  91 [ #I2d #I1s #L2d #L1s #L2s #K2d #K1s #K2s #V2d #V1s #d #i #Hdi #HLK2d #HLK1s #HLK2s #HL12s #_ #IHV2s #L1d #HL1sd #HL12d
  92   elim (lpxs_ldrop_trans_O1 … HL12d … HLK2d) -L2d #Y #HLK1d #H
  93   elim (lpxs_inv_pair2 … H) -H #K1d #V1d #HK12d #HV12d #H destruct
  94   elim (lleq_inv_lref_ge … HL1sd … HLK1s HLK1d) // -d -I2d #H #HV1d destruct
  95   lapply (lleq_cpxs_conf_dx … HV12d … HV1d) #HV2d
  96   lapply (lleq_cpxs_trans … HV12d … HV1d) -HV12d -HV1d #HV12d
  97   lapply (IHV2s … HV2d HK12d) -L1d -K1d -K2d #HK12s
  98   elim (ldrop_lpxs_trans h g G … HLK1s (K2s.ⓑ{I1s}V2d)) /2 width=1 by lpxs_pair/ -V1d -K1s #Y #HL1sY #HYK2s #H
  99   lapply (leq_canc_sn … HL12s … H) -HL12s -H #HL2sY
 100   lapply (ldrop_O_inj … HLK2s HYK2s) -I1s -K2s -V2d #H
 101   lapply (leq_join … HL2sY … H) -HL2sY -H #HL2sY
 102   >(leq_inv_O_Y … HL2sY) -HL2sY //
 103 (*
 104 | #a #I #L2d #L1s #L0 #L2s #V #T #d #H0 #_ #IHV #IHT #L1d #H #HL12d
 105   elim (lleq_inv_bind … H) -H #HV #HT
 106 *)
 107 | #I #L2d #L1s #LV #LT #L2s #V #T #d #H0 #_ #_ #IHV #IHT #IH #L1d #H #HL12d
 108   elim (lleq_inv_flat … H) -H #HV #HT
 109   lapply (IHV … HV HL12d) -HV #H1
 110   lapply (IHT … HT HL12d) #H2
 111
 112
 113
 114    @(lpxs_trans … LV) /2 width=3 by/ -IHV
 115   lapply (IHT … HL12d) // -IHT #H @(IH … H) -IH -H
 116
 117   @(IH … HL12d) -IHT -IHV
 118
 119   /4 width=5 by lpxs_trans/
 120
 121
 122 lemma lleq_lpx_conf_llor: ∀h,g,G,L1,L2,T,d. L1 ⋕[T, d] L2 → ∀K1. ⦃G, L1⦄ ⊢ ➡[h, g] K1 →
 123                           ∀K2. K1 ⩖[T, d] L2 ≡ K2 →  ⦃G, L2⦄ ⊢ ➡[h, g] K2.
 124 #h #g #G #L1 #L2 #T #d #H @(lleq_ind_alt … H) -L1 -L2 -T -d
 125 [ #L1 #L2 #d #k #HL12 #K1 #HLK1 #K2 #H