matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.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_transition/lpx_reqx.ma".
  16 include "basic_2/rt_computation/csx_drops.ma".
  17
  18 (* STRONGLY NORMALIZING TERMS FOR EXTENDED PARALLEL RT-TRANSITION ***********)
  19
  20 (* Advanced properties ******************************************************)
  21
  22 lemma csx_teqx_trans (G) (L):
  23       ∀T1. ❪G,L❫ ⊢ ⬈*𝐒 T1 →
  24       ∀T2. T1 ≛ T2 → ❪G,L❫ ⊢ ⬈*𝐒 T2.
  25 #G #L #T1 #H @(csx_ind … H) -T1 #T #_ #IH #T2 #HT2
  26 @csx_intro #T1 #HT21 #HnT21
  27 lapply (teqx_cpx_trans … HT2 … HT21) -HT21 #HT1
  28 /4 width=5 by teqx_repl/
  29 qed-.
  30
  31 lemma csx_cpx_trans (G) (L):
  32       ∀T1. ❪G,L❫ ⊢ ⬈*𝐒 T1 →
  33       ∀T2. ❪G,L❫ ⊢ T1 ⬈ T2 → ❪G,L❫ ⊢ ⬈*𝐒 T2.
  34 #G #L #T1 #H @(csx_ind … H) -T1 #T1 #HT1 #IHT1 #T2 #HLT12
  35 elim (teqx_dec T1 T2) /3 width=4 by csx_teqx_trans/
  36 qed-.
  37
  38 (* Basic_1: was just: sn3_cast *)
  39 lemma csx_cast (G) (L):
  40       ∀W. ❪G,L❫ ⊢ ⬈*𝐒 W →
  41       ∀T. ❪G,L❫ ⊢ ⬈*𝐒 T → ❪G,L❫ ⊢ ⬈*𝐒 ⓝW.T.
  42 #G #L #W #HW @(csx_ind … HW) -W
  43 #W #HW #IHW #T #HT @(csx_ind … HT) -T
  44 #T #HT #IHT @csx_intro
  45 #X #H1 #H2 elim (cpx_inv_cast1 … H1) -H1
  46 [ * #W0 #T0 #HLW0 #HLT0 #H destruct
  47   elim (tneqx_inv_pair … H2) -H2
  48   [ -W -T #H elim H -H //
  49   | -HW -IHT /3 width=3 by csx_cpx_trans/
  50   | -HW -HT -IHW /4 width=3 by csx_cpx_trans, cpx_pair_sn/
  51   ]
  52 |*: /3 width=3 by csx_cpx_trans/
  53 ]
  54 qed.
  55
  56 (* Basic_1: was just: sn3_abbr *)
  57 (* Basic_2A1: was: csx_lref_bind *)
  58 lemma csx_lref_pair_drops (G) (L):
  59       ∀I,K,V,i. ⇩[i] L ≘ K.ⓑ[I]V →
  60       ❪G,K❫ ⊢ ⬈*𝐒 V → ❪G,L❫ ⊢ ⬈*𝐒 #i.
  61 #G #L #I #K #V #i #HLK #HV
  62 @csx_intro #X #H #Hi elim (cpx_inv_lref1_drops … H) -H
  63 [ #H destruct elim Hi //
  64 | -Hi * #I0 #K0 #V0 #V1 #HLK0 #HV01 #HV1
  65   lapply (drops_mono … HLK0 … HLK) -HLK #H destruct
  66   /3 width=8 by csx_lifts, csx_cpx_trans, drops_isuni_fwd_drop2/
  67 ]
  68 qed.
  69
  70 (* Advanced inversion lemmas ************************************************)
  71
  72 (* Basic_1: was: sn3_gen_def *)
  73 (* Basic_2A1: was: csx_inv_lref_bind *)
  74 lemma csx_inv_lref_pair_drops (G) (L):
  75       ∀I,K,V,i. ⇩[i] L ≘ K.ⓑ[I]V →
  76       ❪G,L❫ ⊢ ⬈*𝐒 #i → ❪G,K❫ ⊢ ⬈*𝐒 V.
  77 #G #L #I #K #V #i #HLK #Hi
  78 elim (lifts_total V (𝐔❨↑i❩))
  79 /4 width=9 by csx_inv_lifts, csx_cpx_trans, cpx_delta_drops, drops_isuni_fwd_drop2/
  80 qed-.
  81
  82 lemma csx_inv_lref_drops (G) (L):
  83       ∀i. ❪G,L❫ ⊢ ⬈*𝐒 #i →
  84       ∨∨ ⇩*[Ⓕ,𝐔❨i❩] L ≘ ⋆
  85        | ∃∃I,K. ⇩[i] L ≘ K.ⓤ[I]
  86        | ∃∃I,K,V. ⇩[i] L ≘ K.ⓑ[I]V & ❪G,K❫ ⊢ ⬈*𝐒 V.
  87 #G #L #i #H elim (drops_F_uni L i) /2 width=1 by or3_intro0/
  88 * * /4 width=9 by csx_inv_lref_pair_drops, ex2_3_intro, ex1_2_intro, or3_intro2, or3_intro1/
  89 qed-.