]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw.ma
e86bee33195934be7d4b33ce136291b34a100a38
[helm.git] / 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/teqw.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 ➡*[h,n] 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 (teqw_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 teqw_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, teqw_inv_appl_bi/
76 qed-.