1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "basic_2/notation/relations/psubstnormal_5.ma".
16 include "basic_2/relocation/cpy.ma".
18 (* NORMAL TERMS FOR CONTEXT-SENSITIVE EXTENDED SUBSTITUTION *****************)
20 definition cny: ∀d,e. relation3 genv lenv term ≝
21 λd,e,G,L. NF … (cpy d e G L) (eq …).
24 "normality for context-sensitive extended substitution (term)"
25 'PSubstNormal G L T d e = (cny d e G L T).
27 (* Basic inversion lemmas ***************************************************)
29 lemma cny_inv_lref: ∀G,L,d,e,i. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄ →
30 ∨∨ yinj i < d | d + e ≤ yinj i | |L| ≤ i.
31 #G #L #d #e #i #H elim (ylt_split i d) /2 width=1 by or3_intro0/
32 #Hdi elim (ylt_split i (d+e)) /2 width=1 by or3_intro1/
33 #Hide elim (lt_or_ge i (|L|)) /2 width=1 by or3_intro2/
34 #Hi elim (ldrop_O1_lt L i) //
35 #I #K #V #HLK elim (lift_total V 0 (i+1))
36 #W #HVW lapply (H W ?) -H /2 width=5 by cpy_subst/ -HLK
37 #H destruct elim (lift_inv_lref2_be … HVW) -L -d -e //
40 lemma cny_inv_bind: ∀a,I,G,L,V,T,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃ⓑ{a,I}V.T⦄ →
41 ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃V⦄ ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ ▶[⫯d, e] 𝐍⦃T⦄.
42 #a #I #G #L #V1 #T1 #d #e #HVT1 @conj
43 [ #V2 #HV2 lapply (HVT1 (ⓑ{a,I}V2.T1) ?) -HVT1
44 | #T2 #HT2 lapply (HVT1 (ⓑ{a,I}V1.T2) ?) -HVT1
46 /2 width=1 by cpy_bind/ #H destruct //
49 lemma cny_inv_flat: ∀I,G,L,V,T,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃ⓕ{I}V.T⦄ →
50 ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃V⦄ ∧ ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃T⦄.
51 #I #G #L #V1 #T1 #d #e #HVT1 @conj
52 [ #V2 #HV2 lapply (HVT1 (ⓕ{I}V2.T1) ?) -HVT1
53 | #T2 #HT2 lapply (HVT1 (ⓕ{I}V1.T2) ?) -HVT1
55 /2 width=1 by cpy_flat/ #H destruct //
58 (* Basic properties *********************************************************)
60 lemma lsuby_cny_conf: ∀G,d,e.
61 ∀L1,T. ⦃G, L1⦄ ⊢ ▶[d, e] 𝐍⦃T⦄ →
62 ∀L2. L1 ⊑×[d, e] L2 → ⦃G, L2⦄ ⊢ ▶[d, e] 𝐍⦃T⦄.
63 #G #d #e #L1 #T1 #HT1 #L2 #HL12 #T2 #HT12
64 @HT1 /3 width=3 by lsuby_cpy_trans/
67 lemma cny_sort: ∀G,L,d,e,k. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃⋆k⦄.
68 #G #L #d #e #k #X #H elim (cpy_inv_sort1 … H) -H //
71 lemma cny_lref_free: ∀G,L,d,e,i. |L| ≤ i → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄.
72 #G #L #d #e #i #Hi #X #H elim (cpy_inv_lref1 … H) -H // *
73 #I #K #V #_ #_ #HLK #_ lapply (ldrop_fwd_length_lt2 … HLK) -HLK
74 #H elim (lt_refl_false i) /2 width=3 by lt_to_le_to_lt/
77 lemma cny_lref_atom: ∀G,L,d,e,i. ⇩[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄.
78 #G #L #d #e #i #HL @cny_lref_free >(ldrop_fwd_length … HL) -HL //
81 lemma cny_lref_top: ∀G,L,d,e,i. d+e ≤ yinj i → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄.
82 #G #L #d #e #i #Hdei #X #H elim (cpy_inv_lref1 … H) -H // *
83 #I #K #V #_ #H elim (ylt_yle_false … H) //
86 lemma cny_lref_skip: ∀G,L,d,e,i. yinj i < d → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄.
87 #G #L #d #e #i #Hid #X #H elim (cpy_inv_lref1 … H) -H // *
88 #I #K #V #H elim (ylt_yle_false … H) //
91 lemma cny_gref: ∀G,L,d,e,p. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃§p⦄.
92 #G #L #d #e #p #X #H elim (cpy_inv_gref1 … H) -H //
95 lemma cny_bind: ∀G,L,V,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃V⦄ →
96 ∀I,T. ⦃G, L.ⓑ{I}V⦄ ⊢ ▶[⫯d, e] 𝐍⦃T⦄ →
97 ∀a. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃ⓑ{a,I}V.T⦄.
98 #G #L #V1 #d #e #HV1 #I #T1 #HT1 #a #X #H
99 elim (cpy_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
100 >(HV1 … HV12) -V2 >(HT1 … HT12) -T2 //
103 lemma cny_flat: ∀G,L,V,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃V⦄ →
104 ∀T. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃T⦄ →
105 ∀I. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃ⓕ{I}V.T⦄.
106 #G #L #V1 #d #e #HV1 #T1 #HT1 #I #X #H
107 elim (cpy_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
108 >(HV1 … HV12) -V2 >(HT1 … HT12) -T2 //
111 lemma cny_narrow: ∀G,L,T,d1,e1. ⦃G, L⦄ ⊢ ▶[d1, e1] 𝐍⦃T⦄ →
112 ∀d2,e2. d1 ≤ d2 → d2 + e2 ≤ d1 + e1 → ⦃G, L⦄ ⊢ ▶[d2, e2] 𝐍⦃T⦄.
113 #G #L #T1 #d1 #e1 #HT1 #d2 #e2 #Hd12 #Hde21 #T2 #HT12
114 @HT1 /2 width=5 by cpy_weak/ qed-.