matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx.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/notation/relations/predtysnstrong_4.ma".
  16 include "static_2/static/reqx.ma".
  17 include "basic_2/rt_transition/lpx.ma".
  18
  19 (* STRONGLY NORMALIZING REFERRED LOCAL ENV.S FOR UNBOUND RT-TRANSITION ******)
  20
  21 definition rsx (h) (G) (T): predicate lenv ≝
  22            SN … (lpx h G) (reqx T).
  23
  24 interpretation
  25    "strong normalization for unbound context-sensitive parallel rt-transition on referred entries (local environment)"
  26    'PRedTySNStrong h T G L = (rsx h G T L).
  27
  28 (* Basic eliminators ********************************************************)
  29
  30 (* Basic_2A1: uses: lsx_ind *)
  31 lemma rsx_ind (h) (G) (T) (Q:predicate lenv):
  32       (∀L1. G ⊢ ⬈*[h,T] 𝐒❪L1❫ →
  33             (∀L2. ❪G,L1❫ ⊢ ⬈[h] L2 → (L1 ≛[T] L2 → ⊥) → Q L2) →
  34             Q L1
  35       ) →
  36       ∀L. G ⊢ ⬈*[h,T] 𝐒❪L❫ →  Q L.
  37 #h #G #T #Q #H0 #L1 #H elim H -L1
  38 /5 width=1 by SN_intro/
  39 qed-.
  40
  41 (* Basic properties *********************************************************)
  42
  43 (* Basic_2A1: uses: lsx_intro *)
  44 lemma rsx_intro (h) (G) (T):
  45       ∀L1.
  46       (∀L2. ❪G,L1❫ ⊢ ⬈[h] L2 → (L1 ≛[T] L2 → ⊥) → G ⊢ ⬈*[h,T] 𝐒❪L2❫) →
  47       G ⊢ ⬈*[h,T] 𝐒❪L1❫.
  48 /5 width=1 by SN_intro/ qed.
  49
  50 (* Basic forward lemmas *****************************************************)
  51
  52 (* Basic_2A1: uses: lsx_fwd_pair_sn lsx_fwd_bind_sn lsx_fwd_flat_sn *)
  53 lemma rsx_fwd_pair_sn (h) (G):
  54       ∀I,L,V,T. G ⊢ ⬈*[h,②[I]V.T] 𝐒❪L❫ →
  55       G ⊢ ⬈*[h,V] 𝐒❪L❫.
  56 #h #G #I #L #V #T #H
  57 @(rsx_ind … H) -L #L1 #_ #IHL1
  58 @rsx_intro #L2 #HL12 #HnL12
  59 /4 width=3 by reqx_fwd_pair_sn/
  60 qed-.
  61
  62 (* Basic_2A1: uses: lsx_fwd_flat_dx *)
  63 lemma rsx_fwd_flat_dx (h) (G):
  64       ∀I,L,V,T. G ⊢ ⬈*[h,ⓕ[I]V.T] 𝐒❪L❫ →
  65       G ⊢ ⬈*[h,T] 𝐒❪L❫.
  66 #h #G #I #L #V #T #H
  67 @(rsx_ind … H) -L #L1 #_ #IHL1
  68 @rsx_intro #L2 #HL12 #HnL12
  69 /4 width=3 by reqx_fwd_flat_dx/
  70 qed-.
  71
  72 fact rsx_fwd_pair_aux (h) (G):
  73      ∀L. G ⊢ ⬈*[h,#0] 𝐒❪L❫ →
  74      ∀I,K,V. L = K.ⓑ[I]V → G ⊢ ⬈*[h,V] 𝐒❪K❫.
  75 #h #G #L #H
  76 @(rsx_ind … H) -L #L1 #_ #IH #I #K1 #V #H destruct
  77 /5 width=5 by lpx_pair, rsx_intro, reqx_fwd_zero_pair/
  78 qed-.
  79
  80 lemma rsx_fwd_pair (h) (G):
  81       ∀I,K,V. G ⊢ ⬈*[h,#0] 𝐒❪K.ⓑ[I]V❫ → G ⊢ ⬈*[h,V] 𝐒❪K❫.
  82 /2 width=4 by rsx_fwd_pair_aux/ qed-.
  83
  84 (* Basic inversion lemmas ***************************************************)
  85
  86 (* Basic_2A1: uses: lsx_inv_flat *)
  87 lemma rsx_inv_flat (h) (G):
  88       ∀I,L,V,T. G ⊢ ⬈*[h,ⓕ[I]V.T] 𝐒❪L❫ →
  89       ∧∧ G ⊢ ⬈*[h,V] 𝐒❪L❫ & G ⊢ ⬈*[h,T] 𝐒❪L❫.
  90 /3 width=3 by rsx_fwd_pair_sn, rsx_fwd_flat_dx, conj/ qed-.
  91
  92 (* Basic_2A1: removed theorems 9:
  93               lsx_ge_up lsx_ge
  94               lsxa_ind lsxa_intro lsxa_lleq_trans lsxa_lpxs_trans lsxa_intro_lpx lsx_lsxa lsxa_inv_lsx
  95 *)