update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / etc / nta / nta.etc

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta.etc
index fa4a8ed8f175cb22e8952b7ec3c7807853df1bbf..166fd2105a13bd98cf1938e2ccc1a2470d3f3912 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta.etc
@@ -1,53 +1,63 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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/static/sh.ma".
-include "basic_2/equivalence/cpcs.ma".
-
-(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
-
-inductive nta (h:sh): lenv → relation term ≝
-| nta_sort: ∀L,k. nta h L (⋆k) (⋆(next h k))
-| nta_ldef: ∀L,K,V,W,U,i. ⇩[0, i] L ≡ K. ⓓV → nta h K V W →
-            ⇧[0, i + 1] W ≡ U → nta h L (#i) U
-| nta_ldec: ∀L,K,W,V,U,i. ⇩[0, i] L ≡ K. ⓛW → nta h K W V →
-            ⇧[0, i + 1] W ≡ U → nta h L (#i) U
-| nta_bind: ∀I,L,V,W,T,U. nta h L V W → nta h (L. ⓑ{I} V) T U →
-            nta h L (ⓑ{I}V.T) (ⓑ{I}V.U)
-| nta_appl: ∀L,V,W,T,U. nta h L V W → nta h L (ⓛW.T) (ⓛW.U) →
-            nta h L (ⓐV.ⓛW.T) (ⓐV.ⓛW.U)
-| nta_pure: ∀L,V,W,T,U. nta h L T U → nta h L (ⓐV.U) W →
-            nta h L (ⓐV.T) (ⓐV.U)
-| nta_cast: ∀L,T,U. nta h L T U → nta h L (ⓝU. T) U
-| nta_conv: ∀L,T,U1,U2,V2. nta h L T U1 → L ⊢ U1 ⬌* U2 → nta h L U2 V2 →
-            nta h L T U2
-.
-
-interpretation "native type assignment (term)"
-   'NativeType h L T U = (nta h L T U).
-
-(* Basic properties *********************************************************)
-
-(* Basic_1: was: ty3_cast *)
-lemma nta_cast_old: ∀h,L,W,T,U.
-                    ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ U : W → ⦃h, L⦄ ⊢ ⓝU.T : ⓝW.U.
-/4 width=3/ qed.
-
-(* Basic_1: was: ty3_typecheck *)
-lemma nta_typecheck: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∃T0. ⦃h, L⦄ ⊢ ⓝU.T : T0.
-/3 width=2/ qed.
-
-(* Basic_1: removed theorems 4:
-            ty3_getl_subst0 ty3_fsubst0 ty3_csubst0 ty3_subst0
-*)
+(* Basic_1: was by definition: ty3_abst *)
+(* Basic_2A1: was by definition: nta_ldec ntaa_ldec *)
+lemma nta_ldec_drops
+
+(* Basic_1: was by definition: ty3_bind *)
+(* Basic_2A1: was by definition: nta_bind ntaa_bind *)
+lemma nta_bind
+
+(* Basic_2A1: was by definition: nta_pure ntaa_pure *)
+lemma nta_pure
+
+(* Basic_1: was: ty3_gen_bind *)
+(* Basic_2A1: was: nta_inv_bind1 ntaa_inv_bind1 *)
+lemma nta_inv_bind_sn
+
+(* Basic_1: was: ty3_gen_lref *)
+(* Basic_2A1: was: nta_inv_lref1 *)
+lemma nta_inv_lref_sn_drops
+
+(* Basic_1: uses: ty3_gen_abst_abst *)
+lemma nta_inv_abst_bi
+
+(* Advanced properties ******************************************************)
+
+| ntaa_cast: ∀L,T,U,W. ntaa h L T U → ntaa h L U W → ntaa h L (ⓝU. T) U
+
+lemma nta_cast_alt: ∀h,L,T,W,U. ⦃h, L⦄ ⊢ T  : W → ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ ⓝW.T : U.
+#h #L #T #W #U #HTW #HTU
+lapply (nta_mono … HTW … HTU) #HWU
+elim (nta_fwd_correct … HTU) -HTU /3 width=3/
+qed.
+
+lemma nta_ind_alt: ∀h. ∀Q:lenv→relation term.
+   (∀L,k. Q L ⋆k ⋆(next h k)) →
+   (∀L,K,V,W,U,i.
+      ⇩[O, i] L ≡ K.ⓓV → ⦃h, K⦄ ⊢ V : W → ⇧[O, i + 1] W ≡ U →
+      Q K V W → Q L (#i) U
+   ) →
+   (∀L,K,W,V,U,i.
+      ⇩[O, i] L ≡ K.ⓛW → ⦃h, K⦄ ⊢ W : V → ⇧[O, i + 1] W ≡ U →
+      Q K W V → Q L (#i) U
+   ) →
+   (∀I,L,V,W,T,U.
+      ⦃h, L⦄ ⊢ V : W → ⦃h, L.ⓑ{I}V⦄ ⊢ T : U →
+      Q L V W → Q (L.ⓑ{I}V) T U → Q L (ⓑ{I}V.T) (ⓑ{I}V.U)
+   ) →
+   (∀L,V,W,T,U.
+      ⦃h, L⦄ ⊢ V : W → ⦃h, L⦄ ⊢ (ⓛW.T):(ⓛW.U) →
+      Q L V W →Q L (ⓛW.T) (ⓛW.U) →Q L (ⓐV.ⓛW.T) (ⓐV.ⓛW.U)
+   ) →
+   (∀L,V,W,T,U.
+      ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ (ⓐV.U) : W →
+      Q L T U → Q L (ⓐV.U) W → Q L (ⓐV.T) (ⓐV.U)
+   ) →
+   (∀L,T,U,W.
+      ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ U : W →
+      Q L T U → Q L U W → Q L (ⓝU.T) U
+   ) →
+   (∀L,T,U1,U2,V2.
+      ⦃h, L⦄ ⊢ T : U1 → L ⊢ U1 ⬌* U2 → ⦃h, L⦄ ⊢ U2 : V2 →
+      Q L T U1 →Q L U2 V2 →Q L T U2
+   ) →
+   ∀L,T,U. ⦃h, L⦄ ⊢ T : U → Q L T U.