matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw.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/preditnormal_4.ma".
  16 include "static_2/syntax/tweq.ma".
  17 include "basic_2/rt_computation/cpms.ma".
  18
  19 (* NORMAL TERMS FOR T-UNUNBOUND WHD RT-TRANSITION ***************************)
  20
  21 definition cnuw (h) (G) (L): predicate term ≝
  22            λT1. ∀n,T2. ❪G,L❫ ⊢ T1 ➡*[n,h] T2 → T1 ≅ T2.
  23
  24 interpretation
  25   "normality for t-unbound weak head context-sensitive parallel rt-transition (term)"
  26   'PRedITNormal h G L T = (cnuw h G L T).
  27
  28 (* Basic properties *********************************************************)
  29
  30 lemma cnuw_sort (h) (G) (L): ∀s. ❪G,L❫ ⊢ ➡𝐍𝐖*[h] ⋆s.
  31 #h #G #L #s1 #n #X #H
  32 lapply (cpms_inv_sort1 … H) -H #H destruct //
  33 qed.
  34
  35 lemma cnuw_ctop (h) (G): ∀i. ❪G,⋆❫ ⊢ ➡𝐍𝐖*[h] #i.
  36 #h #G #i #n #X #H
  37 elim (cpms_inv_lref1_ctop … H) -H #H #_ destruct //
  38 qed.
  39
  40 lemma cnuw_zero_unit (h) (G) (L): ∀I. ❪G,L.ⓤ[I]❫ ⊢ ➡𝐍𝐖*[h] #0.
  41 #h #G #L #I #n #X #H
  42 elim (cpms_inv_zero1_unit … H) -H #H #_ destruct //
  43 qed.
  44
  45 lemma cnuw_gref (h) (G) (L): ∀l. ❪G,L❫ ⊢ ➡𝐍𝐖*[h] §l.
  46 #h #G #L #l1 #n #X #H
  47 elim (cpms_inv_gref1 … H) -H #H #_ destruct //
  48 qed.
  49
  50 (* Basic_inversion lemmas ***************************************************)
  51
  52 lemma cnuw_inv_zero_pair (h) (I) (G) (L): ∀V. ❪G,L.ⓑ[I]V❫ ⊢ ➡𝐍𝐖*[h] #0 → ⊥.
  53 #h * #G #L #V #H
  54 elim (lifts_total V (𝐔❨1❩)) #W #HVW
  55 [ lapply (H 0 W ?) [ /3 width=3 by cpm_cpms, cpm_delta/ ]
  56 | lapply (H 1 W ?) [ /3 width=3 by cpm_cpms, cpm_ell/ ]
  57 ] -H #HW
  58 lapply (tweq_inv_lref_sn … HW) -HW #H destruct
  59 /2 width=5 by lifts_inv_lref2_uni_lt/
  60 qed-.
  61
  62 lemma cnuw_inv_cast (h) (G) (L):
  63       ∀V,T. ❪G,L❫ ⊢ ➡𝐍𝐖*[h] ⓝV.T → ⊥.
  64 #h #G #L #V #T #H
  65 lapply (H 0 T ?) [ /3 width=1 by cpm_cpms, cpm_eps/ ] -H #H
  66 /2 width=3 by tweq_inv_cast_xy_y/
  67 qed-.
  68
  69 (* Basic forward lemmas *****************************************************)
  70
  71 lemma cnuw_fwd_appl (h) (G) (L):
  72       ∀V,T. ❪G,L❫ ⊢ ➡𝐍𝐖*[h] ⓐV.T → ❪G,L❫ ⊢ ➡𝐍𝐖*[h] T.
  73 #h #G #L #V #T1 #HT1 #n #T2 #HT12
  74 lapply (HT1 n (ⓐV.T2) ?) -HT1
  75 /2 width=3 by cpms_appl_dx, tweq_inv_appl_bi/
  76 qed-.