From 0c302a9fda708e5019e48d14c5419a8a65190745 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 29 Sep 2018 16:21:54 +0200
Subject: [PATCH] update in basic_2 and apps_2

+ more results on typing
+ first results on iterated typing
+ minor corrections
---
 .../lambdadelta/apps_2/examples/ex_cnv_eta.ma |  2 +-
 .../lambdadelta/apps_2/web/apps_2.ldw.xml     |  4 +-
 .../lambdadelta/basic_2/dynamic/nta_cpcs.ma   |  1 -
 .../basic_2/dynamic/nta_preserve.ma           | 37 ++++++++++++++++++
 .../lambdadelta/basic_2/etc/nta/nta.etc       | 23 +----------
 .../lambdadelta/basic_2/i_dynamic/ntas.ma     | 38 +++++++++++++++++++
 .../ntas_lift.etc => i_dynamic/ntas_etc.ma}   |  3 +-
 .../hod/ntas.etc => i_dynamic/ntas_nta.ma}    | 25 +++---------
 .../basic_2/notation/relations/colon_7.ma     | 19 ++++++++++
 .../basic_2/notation/relations/colonstar_6.ma | 19 ++++++++++
 .../lambdadelta/basic_2/web/basic_2_src.tbl   |  6 +--
 11 files changed, 128 insertions(+), 49 deletions(-)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas.ma
 rename matita/matita/contribs/lambdadelta/basic_2/{etc_2A1/hod/ntas_lift.etc => i_dynamic/ntas_etc.ma} (99%)
 rename matita/matita/contribs/lambdadelta/basic_2/{etc_2A1/hod/ntas.etc => i_dynamic/ntas_nta.ma} (74%)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/colon_7.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/colonstar_6.ma

diff --git a/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cnv_eta.ma b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cnv_eta.ma
index f5bc8f427..704301fe0 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cnv_eta.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cnv_eta.ma
@@ -17,7 +17,7 @@ include "basic_2/dynamic/cnv.ma".
 
 (* EXAMPLES *****************************************************************)
 
-(* Extended validy (basic?_2) vs. restricted validity (basic_1) *************)
+(* Extended validy (basic_2B) vs. restricted validity (basic_1A) ************)
 
 (* Note: extended validity of a closure, height of cnv_appl > 1 *)
 lemma cnv_extended (h) (p): ∀G,L,s. ⦃G, L.ⓛ⋆s.ⓛⓛ{p}⋆s.⋆s.ⓛ#0⦄ ⊢ ⓐ#2.#0 ![Ⓕ,h].
diff --git a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml
index 8b3db76c3..c556f085c 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml
+++ b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml
@@ -38,7 +38,7 @@
    </body>
    <table name="apps_2_sum"/>
    <news class="alpha" date="2018 April 30.">
-         The Models component is started for λδ version 2.
+         The Models component is started for λδ-2B.
    </news>
    <news class="alpha" date="2017 March 6.">
          The Examples component is moved from the Core directory.
@@ -48,7 +48,7 @@
    </news>
    <news class="alpha" date="2011 December 20.">
          The Functional component is started
-         inside the specification of λδ version 2.
+         inside the specification of λδ-2A.
    </news>
    <news class="alpha" date="2011 December 12.">
          The MLTT1 component is started.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpcs.ma
index 4d695a3ec..0dd3441f2 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpcs.ma
@@ -50,4 +50,3 @@ elim (cnv_inv_cast … H) -H #X1 #HX2 #_ #HX21 #H
 lapply (cpms_inv_sort1 … H) -H #H destruct
 /2 width=1 by cpcs_cprs_sn/
 qed-.
- 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma
index ab3b33ad5..4e37eb806 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma
@@ -31,6 +31,17 @@ elim (cnv_fwd_cpm_SO … HT) #U #HTU
 /4 width=2 by cnv_cpms_nta, cpm_cpms, ex_intro/
 qed-.
 
+(* Basic_1: was: ty3_typecheck *)
+lemma nta_typecheck (a) (h) (G) (L):
+      ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] U → ∃T0. ⦃G,L⦄ ⊢ ⓝU.T :[a,h] T0.
+/3 width=1 by cnv_cast, cnv_nta_sn/ qed-.
+
+(* Basic_1: was: ty3_correct *)
+(* Basic_2A1: was: ntaa_fwd_correct *)
+lemma nta_fwd_correct (a) (h) (G) (L):
+      ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] U → ∃T0. ⦃G,L⦄ ⊢ U :[a,h] T0.
+/3 width=2 by nta_fwd_cnv_dx, cnv_nta_sn/ qed-.
+
 lemma nta_pure_cnv (h) (G) (L):
       ∀T,U. ⦃G,L⦄ ⊢ T :*[h] U →
       ∀V. ⦃G,L⦄ ⊢ ⓐV.U !*[h] → ⦃G,L⦄ ⊢ ⓐV.T :*[h] ⓐV.U.
@@ -106,6 +117,32 @@ elim (cpms_inv_cast1 … H2) -H2 [ * || * ]
 ]
 qed-.
 
+(* Basic_1: uses: ty3_gen_cast *)
+lemma nta_inv_cast_sn_old (a) (h) (G) (L) (X2):
+      ∀T0,T1. ⦃G,L⦄ ⊢ ⓝT1.T0 :[a,h] X2 →
+      ∃∃T2. ⦃G,L⦄ ⊢ T0 :[a,h] T1 & ⦃G,L⦄ ⊢ T1 :[a,h] T2 & ⦃G,L⦄ ⊢ ⓝT2.T1 ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![a,h].
+#a #h #G #L #X2 #T0 #T1 #H
+elim (cnv_inv_cast … H) -H #X0 #HX2 #H1 #HX20 #H2
+elim (cnv_inv_cast … H1) #X #HT1 #HT0 #HT1X #HT0X
+elim (cpms_inv_cast1 … H2) -H2 [ * || * ]
+[ #U1 #U0 #HTU1 #HTU0 #H destruct
+  elim (cnv_cpms_conf … HT0 … HT0X … HTU0) -HT0 -HT0X -HTU0
+  <minus_n_n #X0 #HX0 #HUX0
+  lapply (cprs_trans … HT1X … HX0) -X #HT1X0
+  /5 width=7 by cnv_cpms_nta, cpcs_cprs_div, cprs_div, cpms_cast, ex4_intro/
+| #HTX0
+  elim (cnv_cpms_conf … HT0 … HT0X … HTX0) -HT0 -HT0X -HTX0
+  <minus_n_n #X1 #HX1 #HX01
+  elim (cnv_nta_sn … HT1) -HT1 #U1 #HTU1
+  lapply (cprs_trans … HT1X … HX1) -X #HTX1
+  lapply (cprs_trans … HX20 … HX01) -X0 #HX21
+  /4 width=5 by cprs_div, cpms_eps, ex4_intro/
+| #n #HT1X0 #H destruct -X -HT0
+  elim (cnv_nta_sn … HT1) -HT1 #U1 #HTU1
+  /4 width=5 by cprs_div, cpms_eps, ex4_intro/
+]
+qed-.
+
 (* Forward lemmas based on preservation *************************************)
 
 (* Basic_1: was: ty3_unique *)
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 7c9fc0d69..db33815a7 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta.etc
@@ -9,31 +9,12 @@ lemma nta_pure
 (* Basic_2A1: was: nta_inv_bind1 ntaa_inv_bind1 *)
 lemma nta_inv_bind_sn
 
-| ntaa_cast: ∀L,T,U,W. ntaa h L T U → ntaa h L U W → ntaa h L (ⓝU. T) U
-
 (* 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_inv_cast1: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓝY.X : U →  ⦃h, L⦄ ⊢ X : Y ∧ L ⊢ Y ⬌* U.
-/2 width=3/ qed-.
-
-(* Basic_1: uses: ty3_gen_cast *)
-lemma nta_inv_cast_sn_old (a) (h) (G) (L) (X2):
-      ∀T0,T1. ⦃G,L⦄ ⊢ ⓝT1.T0 :[a,h] X2 →
-      ∃∃T2. ⦃G,L⦄ ⊢ T0 :[a,h] T1 & ⦃G,L⦄ ⊢ T1 :[a,h] T2 & ⦃G,L⦄ ⊢ ⓝT2.T1 ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![a,h].
-
-(* 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: was: ty3_correct *)
-(* Basic_2A1: was: ntaa_fwd_correct *)
-lemma nta_fwd_correct: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∃T0. ⦃h, L⦄ ⊢ U : T0.
-#h #L #T #U #H
-elim (ntaa_fwd_correct … (nta_ntaa … H)) -H /3 width=2 by ntaa_nta, ex_intro/
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas.ma b/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas.ma
new file mode 100644
index 000000000..3c65cbd7c
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas.ma
@@ -0,0 +1,38 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/colon_7.ma".
+include "basic_2/notation/relations/colon_6.ma".
+include "basic_2/notation/relations/colonstar_6.ma".
+include "basic_2/dynamic/cnv.ma".
+
+(* ITERATED NATIVE TYPE ASSIGNMENT FOR TERMS ********************************)
+
+definition ntas (a) (h) (n) (G) (L): relation term ≝ λT,U.
+           ∃∃U0. ⦃G,L⦄ ⊢ U ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] & ⦃G,L⦄ ⊢ U ➡*[h] U0 & ⦃G, L⦄ ⊢ T ➡*[n,h] U0.
+
+interpretation "iterated native type assignment (term)"
+   'Colon a h n G L T U = (ntas a h n G L T U).
+
+interpretation "restricted iterated native type assignment (term)"
+   'Colon h n G L T U = (ntas true h n G L T U).
+
+interpretation "extended iterated native type assignment (term)"
+   'ColonStar h n G L T U = (ntas false h n G L T U).
+
+(* Basic properties *********************************************************)
+
+lemma ntas_refl (a) (h) (G) (L):
+      ∀T. ⦃G,L⦄ ⊢ T ![a,h] → ⦃G,L⦄ ⊢ T :[a,h,0] T.
+/2 width=3 by ex4_intro/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_2A1/hod/ntas_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_etc.ma
similarity index 99%
rename from matita/matita/contribs/lambdadelta/basic_2/etc_2A1/hod/ntas_lift.etc
rename to matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_etc.ma
index 1adced79d..0d531af18 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc_2A1/hod/ntas_lift.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_etc.ma
@@ -11,7 +11,7 @@
 (*        v         GNU General Public License Version 2                  *)
 (*                                                                        *)
 (**************************************************************************)
-
+(*
 include "basic_2/dynamic/nta_lift.ma".
 include "basic_2/hod/ntas.ma".
 
@@ -69,3 +69,4 @@ 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/
 *)
+*)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_2A1/hod/ntas.etc b/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_nta.ma
similarity index 74%
rename from matita/matita/contribs/lambdadelta/basic_2/etc_2A1/hod/ntas.etc
rename to matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_nta.ma
index 8cfaa343b..c9ae6d1eb 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc_2A1/hod/ntas.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_nta.ma
@@ -12,29 +12,18 @@
 (*                                                                        *)
 (**************************************************************************)
 
-notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 : : * break term 46 T2 )"
-   non associative with precedence 45
-   for @{ 'NativeTypeStarAlt $h $L $T1 $T2 }.
-
 include "basic_2/dynamic/nta.ma".
+include "basic_2/i_dynamic/ntas.ma".
+
+(* ITERATED NATIVE TYPE ASSIGNMENT FOR TERMS ********************************)
 
-(* HIGHER ORDER NATIVE TYPE ASSIGNMENT ON TERMS *****************************)
+(*
 
 definition ntas: sh → lenv → relation term ≝
                  λh,L. star … (nta h L).
 
-interpretation "higher order native type assignment (term)"
-   'NativeTypeStar h L T U = (ntas h L T U).
-
 (* Basic eliminators ********************************************************)
-(*
-lemma cprs_ind: ∀L,T1. ∀R:predicate term. R T1 →
-                (∀T,T2. L ⊢ T1 ➡* T → L ⊢ T ➡ T2 → R T → R T2) →
-                ∀T2. L ⊢ T1 ➡* T2 → R T2.
-#L #T1 #R #HT1 #IHT1 #T2 #HT12
-@(TC_star_ind … HT1 IHT1 … HT12) //
-qed-.
-*)
+
 axiom ntas_ind_dx: ∀h,L,T2. ∀R:predicate term. R T2 →
                    (∀T1,T. ⦃h, L⦄ ⊢ T1 : T → ⦃h, L⦄ ⊢ T :* T2 → R T → R T1) →
                    ∀T1. ⦃h, L⦄ ⊢ T1 :* T2 → R T1.
@@ -45,9 +34,6 @@ qed-.
 *)
 (* Basic properties *********************************************************)
 
-lemma ntas_refl: ∀h,L,T. ⦃h, L⦄ ⊢ T :* T.
-// qed.
-
 lemma ntas_strap1: ∀h,L,T1,T,T2.
                    ⦃h, L⦄ ⊢ T1 :* T → ⦃h, L⦄  ⊢ T : T2 → ⦃h, L⦄  ⊢ T1 :* T2.
 /2 width=3/ qed.
@@ -55,3 +41,4 @@ lemma ntas_strap1: ∀h,L,T1,T,T2.
 lemma ntas_strap2: ∀h,L,T1,T,T2.
                    ⦃h, L⦄  ⊢ T1 : T → ⦃h, L⦄ ⊢ T :* T2 → ⦃h, L⦄ ⊢ T1 :* T2.
 /2 width=3/ qed.
+*)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/colon_7.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/colon_7.ma
new file mode 100644
index 000000000..6d9fb69bd
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/colon_7.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 :[ break term 46 a, break term 46 h, break term 46 n ] break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'Colon $a $h $n $G $L $T1 $T2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/colonstar_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/colonstar_6.ma
new file mode 100644
index 000000000..72fbe6e88
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/colonstar_6.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 :*[ break term 46 h, break term 46 n ] break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'ColonStar $h $n $G $L $T1 $T2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
index 60c0e71f6..6126c2f68 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -9,16 +9,14 @@ table {
         ]
      }
    ]
-(*
    class "wine"
    [ { "iterated dynamic typing" * } {
-        [ { "" (* "higher order native type assignment" *) * } {
-             [ [ "" ] (* "ntas ( ⦃?,?⦄ ⊢ ? :* ? )" "nta_lift" *) * ]
+        [ { "context-sensitive iterated native type assignment" * } {
+             [ [ "for terms" ] "ntas" + "( ⦃?,?⦄ ⊢ ? :[?,?,?] ? )" + "( ⦃?,?⦄ ⊢ ? :[?,?] ? )" + "( ⦃?,?⦄ ⊢ ? :*[?,?] ? )" * ] 
           }
         ]
      }
    ]
-*)
    class "magenta"
    [ { "dynamic typing" * } {
         [ { "context-sensitive native type assignment" * } {
-- 
2.39.2