update in ground_2, static_2, basic_2, apps_2, alpha_1

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / i_dynamic / ntas_preserve.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_preserve.ma b/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_preserve.ma
index 5d391caed00423c60f442fa801631e62a06131f4..b8759a27d6794d7ec762ca921cbf8892e9446693 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_preserve.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_preserve.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground_2/xoa/ex_7_5.ma".
 include "basic_2/rt_equivalence/cpcs_cprs.ma".
 include "basic_2/dynamic/cnv_preserve.ma".
 include "basic_2/i_dynamic/ntas.ma".
@@ -21,15 +22,24 @@ include "basic_2/i_dynamic/ntas.ma".
 (* Properties based on preservation *****************************************)
 
 lemma cnv_cpms_ntas (h) (a) (G) (L):
-      â\88\80T. â¦\83G,Lâ¦\84 â\8a¢ T ![h,a] â\86\92 â\88\80n,U.â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡*[n,h] U â\86\92 â¦\83G,Lâ¦\84 ⊢ T :*[h,a,n] U.
+      â\88\80T. â\9dªG,Lâ\9d« â\8a¢ T ![h,a] â\86\92 â\88\80n,U.â\9dªG,Lâ\9d« â\8a¢ T â\9e¡*[n,h] U â\86\92 â\9dªG,Lâ\9d« ⊢ T :*[h,a,n] U.
 /3 width=4 by ntas_intro, cnv_cpms_trans/ qed.
 
 (* Inversion lemmas based on preservation ***********************************)
 
+lemma ntas_inv_plus (h) (a) (n1) (n2) (G) (L):
+      ∀T1,T2. ❪G,L❫ ⊢ T1 :*[h,a,n1+n2] T2 →
+      ∃∃T0. ❪G,L❫ ⊢ T1 :*[h,a,n1] T0 & ❪G,L❫ ⊢ T0 :*[h,a,n2] T2.
+#h #a #n1 #n2 #G #L #T1 #T2 * #X0 #HT2 #HT1 #H20 #H10
+elim (cpms_inv_plus … H10) -H10 #T0 #H10 #H00
+lapply (cnv_cpms_trans … HT1 … H10) #HT0
+/3 width=6 by cnv_cpms_ntas, ntas_intro, ex2_intro/
+qed-.
+
 lemma ntas_inv_appl_sn (h) (a) (m) (G) (L) (V) (T):
-      â\88\80X. â¦\83G,Lâ¦\84 ⊢ ⓐV.T :*[h,a,m] X →
-      â\88¨â\88¨ â\88\83â\88\83n,p,W,U,U0. n â\89¤ m & ad a n & â¦\83G,Lâ¦\84 â\8a¢ V :*[h,a,1] W & â¦\83G,Lâ¦\84 â\8a¢ T :*[h,a,n] â\93\9b{p}W.U0 & â¦\83G,L.â\93\9bWâ¦\84 â\8a¢ U0 :*[h,a,m-n] U & â¦\83G,Lâ¦\84 â\8a¢ â\93\90V.â\93\9b{p}W.U â¬\8c*[h] X & â¦\83G,Lâ¦\84 ⊢ X ![h,a]
-       | â\88\83â\88\83n,p,W,U,U0. m â\89¤ n & ad a n & â¦\83G,Lâ¦\84 â\8a¢ V :*[h,a,1] W & â¦\83G,Lâ¦\84 â\8a¢ T :*[h,a,m] U & â¦\83G,Lâ¦\84 â\8a¢ U :*[h,a,n-m] â\93\9b{p}W.U0 & â¦\83G,Lâ¦\84 â\8a¢ â\93\90V.U â¬\8c*[h] X & â¦\83G,Lâ¦\84 ⊢ X ![h,a].
+      â\88\80X. â\9dªG,Lâ\9d« ⊢ ⓐV.T :*[h,a,m] X →
+      â\88¨â\88¨ â\88\83â\88\83n,p,W,U,U0. n â\89¤ m & ad a n & â\9dªG,Lâ\9d« â\8a¢ V :*[h,a,1] W & â\9dªG,Lâ\9d« â\8a¢ T :*[h,a,n] â\93\9b[p]W.U0 & â\9dªG,L.â\93\9bWâ\9d« â\8a¢ U0 :*[h,a,m-n] U & â\9dªG,Lâ\9d« â\8a¢ â\93\90V.â\93\9b[p]W.U â¬\8c*[h] X & â\9dªG,Lâ\9d« ⊢ X ![h,a]
+       | â\88\83â\88\83n,p,W,U,U0. m â\89¤ n & ad a n & â\9dªG,Lâ\9d« â\8a¢ V :*[h,a,1] W & â\9dªG,Lâ\9d« â\8a¢ T :*[h,a,m] U & â\9dªG,Lâ\9d« â\8a¢ U :*[h,a,n-m] â\93\9b[p]W.U0 & â\9dªG,Lâ\9d« â\8a¢ â\93\90V.U â¬\8c*[h] X & â\9dªG,Lâ\9d« ⊢ X ![h,a].
 #h #a #m #G #L #V #T #X
 * #X0 #HX #HVT #HX0 #HTX0
 elim (cnv_inv_appl … HVT) #n #p #W #U0 #Ha #HV #HT #HVW #HTU0
@@ -51,58 +61,3 @@ elim (le_or_ge n m) #Hnm
   /5 width=11 by cnv_cpms_ntas, cnv_cpms_trans, ex7_5_intro, or_intror/
 ]
 qed-.
-
-(*
-(* Advanced properties on native type assignment for terms ******************)
-
-lemma nta_pure_ntas: ∀h,L,U,W,Y. ⦃h,L⦄ ⊢ U :* ⓛW.Y → ∀T. ⦃h,L⦄ ⊢ T : U →
-                     ∀V. ⦃h,L⦄ ⊢ V : W →  ⦃h,L⦄ ⊢ ⓐV.T : ⓐV.U.
-#h #L #U #W #Y #H @(ntas_ind_dx … H) -U /2 width=1/ /3 width=2/
-qed.
-
-axiom pippo: ∀h,L,T,W,Y. ⦃h,L⦄ ⊢ T :* ⓛW.Y → ∀U. ⦃h,L⦄ ⊢ T : U →
-             ∃Z. ⦃h,L⦄ ⊢ U :* ⓛW.Z.
-(* REQUIRES SUBJECT CONVERSION
-#h #L #T #W #Y #H @(ntas_ind_dx … H) -T
-[ #U #HYU
-  elim (nta_fwd_correct … HYU) #U0 #HU0 
-  elim (nta_inv_bind1 … HYU) #W0 #Y0 #HW0 #HY0 #HY0U
-*)
-
-(* Advanced inversion lemmas on native type assignment for terms ************)
-
-fact nta_inv_pure1_aux: ∀h,L,Z,U. ⦃h,L⦄ ⊢ Z : U → ∀X,Y. Z = ⓐY.X →
-                        ∃∃W,V,T. ⦃h,L⦄ ⊢ Y : W & ⦃h,L⦄ ⊢ X : V &
-                                 L ⊢ ⓐY.V ⬌* U & ⦃h,L⦄ ⊢ V :* ⓛW.T.
-#h #L #Z #U #H elim H -L -Z -U
-[ #L #k #X #Y #H destruct
-| #L #K #V #W #U #i #_ #_ #_ #_ #X #Y #H destruct
-| #L #K #W #V #U #i #_ #_ #_ #_ #X #Y #H destruct
-| #I #L #V #W #T #U #_ #_ #_ #_ #X #Y #H destruct
-| #L #V #W #Z #U #HVW #HZU #_ #_ #X #Y #H destruct /2 width=7/
-| #L #V #W #Z #U #HZU #_ #_ #IHUW #X #Y #H destruct
-  elim (IHUW U Y ?) -IHUW // /3 width=9/
-| #L #Z #U #_ #_ #X #Y #H destruct
-| #L #Z #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #X #Y #H destruct
-  elim (IHTU1 ???) -IHTU1 [4: // |2,3: skip ] #W #V #T #HYW #HXV #HU1 #HVT
-  lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=7/
-]
-qed.
-
-(* Basic_1: was only: ty3_gen_appl *)
-lemma nta_inv_pure1: ∀h,L,Y,X,U. ⦃h,L⦄ ⊢ ⓐY.X : U →
-                     ∃∃W,V,T. ⦃h,L⦄ ⊢ Y : W & ⦃h,L⦄ ⊢ X : V &
-                              L ⊢ ⓐY.V ⬌* U & ⦃h,L⦄ ⊢ V :* ⓛW.T.
-/2 width=3/ qed-.
-
-axiom nta_inv_appl1: ∀h,L,Z,Y,X,U. ⦃h,L⦄ ⊢ ⓐZ.ⓛY.X : U →
-                     ∃∃W. ⦃h,L⦄ ⊢ Z : Y & ⦃h,L⦄ ⊢ ⓛY.X : ⓛY.W &
-                     L ⊢ ⓐZ.ⓛY.W ⬌* U.
-(* REQUIRES SUBJECT REDUCTION
-#h #L #Z #Y #X #U #H
-elim (nta_inv_pure1 … H) -H #W #V #T #HZW #HXV #HVU #HVT
-elim (nta_inv_bind1 … HXV) -HXV #Y0 #X0 #HY0 #HX0 #HX0V
-lapply (cpcs_trans … (ⓐZ.ⓛY.X0) … HVU) -HVU /2 width=1/ -HX0V #HX0U
-@(ex3_1_intro … HX0U) /2 width=2/
-*)
-*)