milestone update in ground_2 and basic_2A

[helm.git] / matita / matita / contribs / lambdadelta / basic_2A / etc / cny / cny.etc

diff --git a/matita/matita/contribs/lambdadelta/basic_2A/etc/cny/cny.etc b/matita/matita/contribs/lambdadelta/basic_2A/etc/cny/cny.etc
new file mode 100644 (file)
index 0000000..81919dc
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2A/etc/cny/cny.etc
@@ -0,0 +1,114 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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-.