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