matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpx.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/rt_computation/cpxs_lpx.ma".
  16 include "basic_2/rt_computation/csx_cpxs.ma".
  17
  18 (* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
  19
  20 (* Properties with unbound parallel rt-transition on all entries ************)
  21
  22 lemma csx_lpx_conf (h) (G) (L1):
  23       ∀T. ❪G,L1❫ ⊢ ⬈*𝐒[h] T →
  24       ∀L2. ❪G,L1❫ ⊢ ⬈[h] L2 → ❪G,L2❫ ⊢ ⬈*𝐒[h] T.
  25 #h #G #L1 #T #H @(csx_ind_cpxs … H) -T
  26 /4 width=3 by csx_intro, lpx_cpx_trans/
  27 qed-.
  28
  29 (* Advanced properties ******************************************************)
  30
  31 lemma csx_abst (h) (G) (L):
  32       ∀p,W. ❪G,L❫ ⊢ ⬈*𝐒[h] W →
  33       ∀T. ❪G,L.ⓛW❫ ⊢ ⬈*𝐒[h] T → ❪G,L❫ ⊢ ⬈*𝐒[h] ⓛ[p]W.T.
  34 #h #G #L #p #W #HW
  35 @(csx_ind … HW) -W #W #_ #IHW #T #HT
  36 @(csx_ind … HT) -T #T #HT #IHT
  37 @csx_intro #X #H1 #H2
  38 elim (cpx_inv_abst1 … H1) -H1 #W0 #T0 #HLW0 #HLT0 #H destruct
  39 elim (tneqx_inv_pair  … H2) -H2
  40 [ #H elim H -H //
  41 | -IHT #H lapply (csx_cpx_trans … HLT0) // -HT #HT0
  42   /4 width=5 by csx_lpx_conf, lpx_pair/
  43 | -IHW -HT /4 width=3 by csx_cpx_trans, cpx_pair_sn/
  44 ]
  45 qed.
  46
  47 lemma csx_abbr (h) (G) (L):
  48       ∀p,V. ❪G,L❫ ⊢ ⬈*𝐒[h] V →
  49       ∀T. ❪G,L.ⓓV❫ ⊢ ⬈*𝐒[h] T → ❪G,L❫ ⊢ ⬈*𝐒[h] ⓓ[p]V.T.
  50 #h #G #L #p #V #HV
  51 @(csx_ind … HV) -V #V #_ #IHV #T #HT
  52 @(csx_ind_cpxs … HT) -T #T #HT #IHT
  53 @csx_intro #X #H1 #H2
  54 elim (cpx_inv_abbr1 … H1) -H1 *
  55 [ #V1 #T1 #HLV1 #HLT1 #H destruct
  56   elim (tneqx_inv_pair … H2) -H2
  57   [ #H elim H -H //
  58   | /4 width=5 by csx_cpx_trans, csx_lpx_conf, lpx_pair/
  59   | -IHV /4 width=3 by csx_cpx_trans, cpx_cpxs, cpx_pair_sn/
  60   ]
  61 | #U #HUT #HUX #_ -p
  62   /5 width=7 by csx_cpx_trans, csx_inv_lifts, drops_drop, drops_refl/
  63 ]
  64 qed.
  65
  66 lemma csx_bind (h) (G) (L):
  67       ∀p,I,V. ❪G,L❫ ⊢ ⬈*𝐒[h] V →
  68       ∀T. ❪G,L.ⓑ[I]V❫ ⊢ ⬈*𝐒[h] T → ❪G,L❫ ⊢ ⬈*𝐒[h] ⓑ[p,I]V.T.
  69 #h #G #L #p * #V #HV #T #HT
  70 /2 width=1 by csx_abbr, csx_abst/
  71 qed.
  72
  73 fact csx_appl_theta_aux (h) (G) (L):
  74      ∀p,U. ❪G,L❫ ⊢ ⬈*𝐒[h] U → ∀V1,V2. ⇧[1] V1 ≘ V2 →
  75      ∀V,T. U = ⓓ[p]V.ⓐV2.T → ❪G,L❫ ⊢ ⬈*𝐒[h] ⓐV1.ⓓ[p]V.T.
  76 #h #G #L #p #X #H
  77 @(csx_ind_cpxs … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct
  78 lapply (csx_fwd_pair_sn … HVT) #HV
  79 lapply (csx_fwd_bind_dx … HVT) -HVT #HVT
  80 @csx_intro #X #HL #H
  81 elim (cpx_inv_appl1 … HL) -HL *
  82 [ -HV #V0 #Y #HLV10 #HL #H0 destruct
  83   elim (cpx_inv_abbr1 … HL) -HL *
  84   [ #V3 #T3 #HV3 #HLT3 #H0 destruct
  85     elim (cpx_lifts_sn … HLV10 (Ⓣ) … (L.ⓓV) … HV12) -HLV10 /3 width=1 by drops_refl, drops_drop/ #V4 #HV04 #HV24
  86     elim (teqx_dec (ⓓ[p]V.ⓐV2.T) (ⓓ[p]V3.ⓐV4.T3)) #H0
  87     [ -IHVT -HV3 -HV24 -HLT3
  88       elim (teqx_inv_pair … H0) -H0 #_ #HV3 #H0
  89       elim (teqx_inv_pair … H0) -H0 #_ #HV24 #HT3
  90       elim (tneqx_inv_pair … H) -H #H elim H -H -G -L
  91       /3 width=6 by teqx_inv_lifts_bi, teqx_pair/
  92     | -V1 @(IHVT … H0 … HV04) -V0 /4 width=1 by cpx_cpxs, cpx_flat, cpx_bind/
  93     ]
  94   | #T0 #HT0 #HLT0 #H0 destruct -H -IHVT
  95     lapply (csx_inv_lifts … HVT (Ⓣ) … L ???) -HVT
  96     [5:|*: /3 width=4 by drops_refl, drops_drop, lifts_flat/ ] -V2 -T #HVT
  97     /3 width=5 by csx_cpx_trans, cpx_flat/
  98   ]
  99 | -HV -HV12 -HVT -IHVT -H #b #V0 #W0 #W1 #T0 #T1 #_ #_ #_ #H destruct
 100 | -IHVT -H #b #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HV03 #HLW01 #HLT01 #H1 #H2 destruct
 101   lapply (cpx_lifts_bi … HLV10 (Ⓣ) … (L.ⓓW0) … HV12 … HV03) -HLV10 -HV12 -HV03 /3 width=1 by drops_refl, drops_drop/ #HLV23
 102   @csx_abbr /2 width=3 by csx_cpx_trans/ -HV
 103   @(csx_lpx_conf … (L.ⓓW0)) /2 width=1 by lpx_pair/ -W1
 104   /4 width=5 by csx_cpxs_trans, cpx_cpxs, cpx_flat/
 105 ]
 106 qed-.
 107
 108 lemma csx_appl_theta (h) (G) (L):
 109       ∀p,V,V2,T. ❪G,L❫ ⊢ ⬈*𝐒[h] ⓓ[p]V.ⓐV2.T →
 110       ∀V1. ⇧[1] V1 ≘ V2 → ❪G,L❫ ⊢ ⬈*𝐒[h] ⓐV1.ⓓ[p]V.T.
 111 /2 width=5 by csx_appl_theta_aux/ qed.