+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/notation/relations/psubstnormal_5.ma".
-include "basic_2/relocation/cpy.ma".
-
-(* NORMAL TERMS FOR CONTEXT-SENSITIVE EXTENDED SUBSTITUTION *****************)
-
-definition cny: ∀d,e. relation3 genv lenv term ≝
- λd,e,G,L. NF … (cpy d e G L) (eq …).
-
-interpretation
- "normality for context-sensitive extended substitution (term)"
- 'PSubstNormal G L T d e = (cny d e G L T).
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma cny_inv_lref: ∀G,L,d,e,i. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄ →
- ∨∨ yinj i < d | d + e ≤ yinj i | |L| ≤ i.
-#G #L #d #e #i #H elim (ylt_split i d) /2 width=1 by or3_intro0/
-#Hdi elim (ylt_split i (d+e)) /2 width=1 by or3_intro1/
-#Hide elim (lt_or_ge i (|L|)) /2 width=1 by or3_intro2/
-#Hi elim (ldrop_O1_lt L i) //
-#I #K #V #HLK elim (lift_total V 0 (i+1))
-#W #HVW lapply (H W ?) -H /2 width=5 by cpy_subst/ -HLK
-#H destruct elim (lift_inv_lref2_be … HVW) -L -d -e //
-qed-.
-
-lemma cny_inv_bind: ∀a,I,G,L,V,T,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃ⓑ{a,I}V.T⦄ →
- ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃V⦄ ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ ▶[⫯d, e] 𝐍⦃T⦄.
-#a #I #G #L #V1 #T1 #d #e #HVT1 @conj
-[ #V2 #HV2 lapply (HVT1 (ⓑ{a,I}V2.T1) ?) -HVT1
-| #T2 #HT2 lapply (HVT1 (ⓑ{a,I}V1.T2) ?) -HVT1
-]
-/2 width=1 by cpy_bind/ #H destruct //
-qed-.
-
-lemma cny_inv_flat: ∀I,G,L,V,T,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃ⓕ{I}V.T⦄ →
- ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃V⦄ ∧ ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃T⦄.
-#I #G #L #V1 #T1 #d #e #HVT1 @conj
-[ #V2 #HV2 lapply (HVT1 (ⓕ{I}V2.T1) ?) -HVT1
-| #T2 #HT2 lapply (HVT1 (ⓕ{I}V1.T2) ?) -HVT1
-]
-/2 width=1 by cpy_flat/ #H destruct //
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma lsuby_cny_conf: ∀G,d,e.
- ∀L1,T. ⦃G, L1⦄ ⊢ ▶[d, e] 𝐍⦃T⦄ →
- ∀L2. L1 ⊑×[d, e] L2 → ⦃G, L2⦄ ⊢ ▶[d, e] 𝐍⦃T⦄.
-#G #d #e #L1 #T1 #HT1 #L2 #HL12 #T2 #HT12
-@HT1 /3 width=3 by lsuby_cpy_trans/
-qed-.
-
-lemma cny_sort: ∀G,L,d,e,k. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃⋆k⦄.
-#G #L #d #e #k #X #H elim (cpy_inv_sort1 … H) -H //
-qed.
-
-lemma cny_lref_free: ∀G,L,d,e,i. |L| ≤ i → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄.
-#G #L #d #e #i #Hi #X #H elim (cpy_inv_lref1 … H) -H // *
-#I #K #V #_ #_ #HLK #_ lapply (ldrop_fwd_length_lt2 … HLK) -HLK
-#H elim (lt_refl_false i) /2 width=3 by lt_to_le_to_lt/
-qed.
-
-lemma cny_lref_atom: ∀G,L,d,e,i. ⇩[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄.
-#G #L #d #e #i #HL @cny_lref_free >(ldrop_fwd_length … HL) -HL //
-qed.
-
-lemma cny_lref_top: ∀G,L,d,e,i. d+e ≤ yinj i → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄.
-#G #L #d #e #i #Hdei #X #H elim (cpy_inv_lref1 … H) -H // *
-#I #K #V #_ #H elim (ylt_yle_false … H) //
-qed.
-
-lemma cny_lref_skip: ∀G,L,d,e,i. yinj i < d → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄.
-#G #L #d #e #i #Hid #X #H elim (cpy_inv_lref1 … H) -H // *
-#I #K #V #H elim (ylt_yle_false … H) //
-qed.
-
-lemma cny_gref: ∀G,L,d,e,p. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃§p⦄.
-#G #L #d #e #p #X #H elim (cpy_inv_gref1 … H) -H //
-qed.
-
-lemma cny_bind: ∀G,L,V,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃V⦄ →
- ∀I,T. ⦃G, L.ⓑ{I}V⦄ ⊢ ▶[⫯d, e] 𝐍⦃T⦄ →
- ∀a. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃ⓑ{a,I}V.T⦄.
-#G #L #V1 #d #e #HV1 #I #T1 #HT1 #a #X #H
-elim (cpy_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
->(HV1 … HV12) -V2 >(HT1 … HT12) -T2 //
-qed.
-
-lemma cny_flat: ∀G,L,V,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃V⦄ →
- ∀T. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃T⦄ →
- ∀I. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃ⓕ{I}V.T⦄.
-#G #L #V1 #d #e #HV1 #T1 #HT1 #I #X #H
-elim (cpy_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
->(HV1 … HV12) -V2 >(HT1 … HT12) -T2 //
-qed.
-
-lemma cny_narrow: ∀G,L,T,d1,e1. ⦃G, L⦄ ⊢ ▶[d1, e1] 𝐍⦃T⦄ →
- ∀d2,e2. d1 ≤ d2 → d2 + e2 ≤ d1 + e1 → ⦃G, L⦄ ⊢ ▶[d2, e2] 𝐍⦃T⦄.
-#G #L #T1 #d1 #e1 #HT1 #d2 #e2 #Hd12 #Hde21 #T2 #HT12
-@HT1 /2 width=5 by cpy_weak/ qed-.