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_3.ma".
  16 include "static_2/static/reqx.ma".
  17 include "basic_2/rt_transition/lpx.ma".
  18
  19 (* STRONGLY NORMALIZING REFERRED LOCAL ENVS FOR EXTENDED RT-TRANSITION ******)
  20
  21 definition rsx (G) (T): predicate lenv ≝
  22            SN … (lpx G) (λL1,L2. L1 ≅[T] L2).
  23
  24 interpretation
  25   "strong normalization for extended context-sensitive parallel rt-transition on referred entries (local environment)"
  26   'PRedTySNStrong G T L = (rsx G T L).
  27
  28 (* Basic eliminators ********************************************************)
  29
  30 (* Basic_2A1: uses: lsx_ind *)
  31 lemma rsx_ind (G) (T) (Q:predicate …):
  32       (∀L1. G ⊢ ⬈*𝐒[T] L1 →
  33         (∀L2. ❪G,L1❫ ⊢ ⬈ L2 → (L1 ≅[T] L2 → ⊥) → Q L2) →
  34         Q L1
  35       ) →
  36       ∀L. G ⊢ ⬈*𝐒[T] L →  Q L.
  37 #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 (G) (T):
  45       ∀L1.
  46       (∀L2. ❪G,L1❫ ⊢ ⬈ L2 → (L1 ≅[T] L2 → ⊥) → G ⊢ ⬈*𝐒[T] L2) →
  47       G ⊢ ⬈*𝐒[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 (G):
  54       ∀I,L,V,T. G ⊢ ⬈*𝐒[②[I]V.T] L →
  55       G ⊢ ⬈*𝐒[V] L.
  56 #G #I #L #V #T #H
  57 @(rsx_ind … H) -L #L1 #_ #IHL1
  58 @rsx_intro #L2 #HL12 #HnL12
  59 /4 width=3 by reqg_fwd_pair_sn/
  60 qed-.
  61
  62 (* Basic_2A1: uses: lsx_fwd_flat_dx *)
  63 lemma rsx_fwd_flat_dx (G):
  64       ∀I,L,V,T. G ⊢ ⬈*𝐒[ⓕ[I]V.T] L →
  65       G ⊢ ⬈*𝐒[T] L.
  66 #G #I #L #V #T #H
  67 @(rsx_ind … H) -L #L1 #_ #IHL1
  68 @rsx_intro #L2 #HL12 #HnL12
  69 /4 width=3 by reqg_fwd_flat_dx/
  70 qed-.
  71
  72 fact rsx_fwd_pair_aux (G):
  73      ∀L. G ⊢ ⬈*𝐒[#0] L →
  74      ∀I,K,V. L = K.ⓑ[I]V → G ⊢ ⬈*𝐒[V] K.
  75 #G #L #H
  76 @(rsx_ind … H) -L #L1 #_ #IH #I #K1 #V #H destruct
  77 /5 width=5 by lpx_pair, rsx_intro, reqg_fwd_zero_pair/
  78 qed-.
  79
  80 lemma rsx_fwd_pair (G):
  81       ∀I,K,V. G ⊢ ⬈*𝐒[#0] K.ⓑ[I]V → G ⊢ ⬈*𝐒[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 (G):
  88       ∀I,L,V,T. G ⊢ ⬈*𝐒[ⓕ[I]V.T] L →
  89       ∧∧ G ⊢ ⬈*𝐒[V] L & G ⊢ ⬈*𝐒[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 *)