From 5c92c318030a05c766b3f6070dbd23589cbdee04 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 27 Sep 2018 20:00:57 +0200 Subject: [PATCH] update in basic_2 and static_2 + first results on type assignment + more notation for validity + eta-conversion defined (for use in linking the notions of validity) --- .../lambdadelta/basic_2/dynamic/cnv.ma | 8 + .../lambdadelta/basic_2/dynamic/cnv_aaa.ma | 10 ++ .../basic_2/dynamic/cnv_cpm_tdeq_trans.ma | 2 +- .../basic_2/dynamic/cnv_preserve.ma | 11 ++ .../lambdadelta/basic_2/dynamic/nta.ma | 137 ++++++++++++++++++ .../lambdadelta/basic_2/dynamic/nta_cpcs.ma | 53 +++++++ .../lambdadelta/basic_2/dynamic/nta_cpms.ma | 49 +++++++ .../nta/nta_lift.etc => dynamic/nta_drops.ma} | 68 +-------- .../basic_2/dynamic/nta_preserve.ma | 119 +++++++++++++++ .../basic_2/etc/notation/notation.etc | 12 -- .../lambdadelta/basic_2/etc/nta/nta.etc | 39 +++++ .../lambdadelta/basic_2/etc_2A1/nta/nta.etc | 53 ------- .../basic_2/etc_2A1/nta/nta_nta.etc | 59 -------- .../basic_2/notation/relations/colon_5.ma | 19 +++ .../basic_2/notation/relations/colon_6.ma | 19 +++ .../basic_2/notation/relations/colonstar_5.ma | 19 +++ .../basic_2/notation/relations/exclaim_4.ma | 19 +++ .../notation/relations/exclaimstar_4.ma | 19 +++ .../basic_2/rt_computation/cpms.ma | 48 +++++- .../basic_2/rt_computation/cprs.ma | 16 +- .../lambdadelta/basic_2/rt_transition/cpm.ma | 5 +- .../basic_2/rt_transition/cpm_aaa.ma | 25 ++++ .../lambdadelta/basic_2/web/basic_2_src.tbl | 19 +-- .../static_2/notation/relations/pconveta_4.ma | 19 +++ .../lambdadelta/static_2/static/cpce.ma | 39 +++++ .../lambdadelta/static_2/web/static_2_src.tbl | 4 + 26 files changed, 671 insertions(+), 219 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpcs.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpms.ma rename matita/matita/contribs/lambdadelta/basic_2/{etc_2A1/nta/nta_lift.etc => dynamic/nta_drops.ma} (61%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc_2A1/nta/nta.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc_2A1/nta/nta_nta.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/colon_5.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/colon_6.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/colonstar_5.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/exclaim_4.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/exclaimstar_4.ma create mode 100644 matita/matita/contribs/lambdadelta/static_2/notation/relations/pconveta_4.ma create mode 100644 matita/matita/contribs/lambdadelta/static_2/static/cpce.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma index 92b22a46a..c3fa8e11b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma @@ -13,6 +13,8 @@ (**************************************************************************) include "basic_2/notation/relations/exclaim_5.ma". +include "basic_2/notation/relations/exclaim_4.ma". +include "basic_2/notation/relations/exclaimstar_4.ma". include "basic_2/rt_computation/cpms.ma". (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) @@ -33,6 +35,12 @@ inductive cnv (a) (h): relation3 genv lenv term ≝ interpretation "context-sensitive native validity (term)" 'Exclaim a h G L T = (cnv a h G L T). +interpretation "context-sensitive restricted native validity (term)" + 'Exclaim h G L T = (cnv true h G L T). + +interpretation "context-sensitive extended native validity (term)" + 'ExclaimStar h G L T = (cnv false h G L T). + (* Basic inversion lemmas ***************************************************) fact cnv_inv_zero_aux (a) (h): ∀G,L,X. ⦃G, L⦄ ⊢ X ![a, h] → X = #0 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma index 18e245959..e5b5d6f7a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "basic_2/rt_transition/cpm_aaa.ma". include "basic_2/rt_computation/cpms_aaa.ma". include "basic_2/dynamic/cnv.ma". @@ -40,3 +41,12 @@ lemma cnv_fwd_aaa (a) (h): ∀G,L,T. ⦃G, L⦄ ⊢ T ![a, h] → ∃A. ⦃G, L /3 width=3 by aaa_cast, ex_intro/ ] qed-. + +(* Forward lemmas with t_bound rt_transition for terms **********************) + +lemma cnv_fwd_cpm_SO (a) (h) (G) (L): + ∀T. ⦃G, L⦄ ⊢ T ![a, h] → ∃U. ⦃G,L⦄ ⊢ T ➡[1,h] U. +#a #h #G #L #T #H +elim (cnv_fwd_aaa … H) -H #A #HA +/2 width=2 by aaa_cpm_SO/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq_trans.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq_trans.ma index a0bda539d..7b1937258 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq_trans.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq_trans.ma @@ -35,7 +35,7 @@ fact cnv_cpm_tdeq_cpm_trans_sub (a) (h) (o) (G0) (L0) (T0): [ #H1 #H2 destruct /2 width=4 by ex3_intro/ | #s #H1 #H2 #H3 #Hs destruct elim (cpm_inv_sort1 … HX2) -HX2 #H #Hn2 destruct >iter_n_Sm - /5 width=6 by cpm_sort_iter, tdeq_sort, deg_iter, deg_next, ex3_intro/ + /5 width=6 by cpm_sort, tdeq_sort, deg_iter, deg_next, ex3_intro/ ] | #p #I #V1 #T1 #HG #HL #HT #H0 #n1 #X1 #H1X #H2X #n2 #X2 #HX2 destruct elim (cpm_tdeq_inv_bind_sn … H0 … H1X H2X) -H0 -H1X -H2X #T #_ #H0T1 #H1T1 #H2T1 #H destruct diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve.ma index 4ea01e534..9e93c859d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve.ma @@ -42,8 +42,19 @@ qed-. (* Advanced preservation properties *****************************************) +lemma cnv_cpms_conf (a) (h) (G) (L): + ∀T0. ⦃G,L⦄ ⊢ T0 ![a,h] → + ∀n1,T1. ⦃G,L⦄ ⊢ T0 ➡*[n1,h] T1 → ∀n2,T2. ⦃G,L⦄ ⊢ T0 ➡*[n2,h] T2 → + ∃∃T. ⦃G,L⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G,L⦄ ⊢ T2 ➡*[n1-n2,h] T. +/2 width=8 by cnv_cpms_conf_lpr/ qed-. + (* Basic_2A1: uses: snv_cprs_lpr *) lemma cnv_cpms_trans_lpr (a) (h) (G) (L) (T): IH_cnv_cpms_trans_lpr a h G L T. #a #h #G #L1 #T1 #HT1 #n #T2 #H @(cpms_ind_dx … H) -n -T2 /3 width=6 by cnv_cpm_trans_lpr/ qed-. + +lemma cnv_cpms_trans (a) (h) (G) (L): + ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → + ∀n,T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 → ⦃G,L⦄ ⊢ T2 ![a,h]. +/2 width=6 by cnv_cpms_trans_lpr/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma new file mode 100644 index 000000000..8f6e4c6be --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma @@ -0,0 +1,137 @@ +(**************************************************************************) +(* ___ *) +(* ||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_6.ma". +include "basic_2/notation/relations/colon_5.ma". +include "basic_2/notation/relations/colonstar_5.ma". +include "basic_2/dynamic/cnv.ma". + +(* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************) + +definition nta (a) (h): relation4 genv lenv term term ≝ + λG,L,T,U. ⦃G,L⦄ ⊢ ⓝU.T ![a,h]. + +interpretation "native type assignment (term)" + 'Colon a h G L T U = (nta a h G L T U). + +interpretation "restricted native type assignment (term)" + 'Colon h G L T U = (nta true h G L T U). + +interpretation "extended native type assignment (term)" + 'ColonStar h G L T U = (nta false h G L T U). + +(* Basic properties *********************************************************) + +(* Basic_1: was by definition: ty3_sort *) +(* Basic_2A1: was by definition: nta_sort ntaa_sort *) +lemma nta_sort (a) (h) (G) (L) (s): ⦃G,L⦄ ⊢ ⋆s :[a,h] ⋆(next h s). +#a #h #G #L #s /2 width=3 by cnv_sort, cnv_cast, cpms_sort/ +qed. + +lemma nta_bind_cnv (a) (h) (G) (K): + ∀V. ⦃G,K⦄ ⊢ V ![a,h] → + ∀I,T,U. ⦃G,K.ⓑ{I}V⦄ ⊢ T :[a,h] U → + ∀p. ⦃G,K⦄ ⊢ ⓑ{p,I}V.T :[a,h] ⓑ{p,I}V.U. +#a #h #G #K #V #HV #I #T #U #H #p +elim (cnv_inv_cast … H) -H #X #HU #HT #HUX #HTX +/3 width=5 by cnv_bind, cnv_cast, cpms_bind_dx/ +qed. + +(* Basic_2A1: was by definition: nta_cast *) +lemma nta_cast (a) (h) (G) (L): + ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] U → ⦃G,L⦄ ⊢ ⓝU.T :[a,h] U. +#a #h #G #L #T #U #H +elim (cnv_inv_cast … H) #X #HU #HT #HUX #HTX +/3 width=3 by cnv_cast, cpms_eps/ +qed. + +(* Basic_1: was by definition: ty3_cast *) +lemma nta_cast_old (a) (h) (G) (L): + ∀T0,T1. ⦃G,L⦄ ⊢ T0 :[a,h] T1 → + ∀T2. ⦃G,L⦄ ⊢ T1 :[a,h] T2 → ⦃G,L⦄ ⊢ ⓝT1.T0 :[a,h] ⓝT2.T1. +#a #h #G #L #T0 #T1 #H1 #T2 #H2 +elim (cnv_inv_cast … H1) #X1 #_ #_ #HTX1 #HTX01 +elim (cnv_inv_cast … H2) #X2 #_ #_ #HTX2 #HTX12 +/3 width=3 by cnv_cast, cpms_eps/ +qed. + +(* Basic_forward lemmas *****************************************************) + +lemma nta_fwd_cnv_sn (a) (h) (G) (L): + ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] U → ⦃G,L⦄ ⊢ T ![a,h]. +#a #h #G #L #T #U #H +elim (cnv_inv_cast … H) -H #X #_ #HT #_ #_ // +qed-. + +(* Note: this is nta_fwd_correct_cnv *) +lemma nta_fwd_cnv_dx (a) (h) (G) (L): + ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] U → ⦃G,L⦄ ⊢ U ![a,h]. +#a #h #G #L #T #U #H +elim (cnv_inv_cast … H) -H #X #HU #_ #_ #_ // +qed-. + +(* + +| 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 +. + +(* Basic properties *********************************************************) + +lemma nta_ind_alt: ∀h. ∀R:lenv→relation term. + (∀L,k. R 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 → + R K V W → R L (#i) U + ) → + (∀L,K,W,V,U,i. + ⇩[O, i] L ≡ K.ⓛW → ⦃h, K⦄ ⊢ W : V → ⇧[O, i + 1] W ≡ U → + R K W V → R L (#i) U + ) → + (∀I,L,V,W,T,U. + ⦃h, L⦄ ⊢ V : W → ⦃h, L.ⓑ{I}V⦄ ⊢ T : U → + R L V W → R (L.ⓑ{I}V) T U → R L (ⓑ{I}V.T) (ⓑ{I}V.U) + ) → + (∀L,V,W,T,U. + ⦃h, L⦄ ⊢ V : W → ⦃h, L⦄ ⊢ (ⓛW.T):(ⓛW.U) → + R L V W →R L (ⓛW.T) (ⓛW.U) →R L (ⓐV.ⓛW.T) (ⓐV.ⓛW.U) + ) → + (∀L,V,W,T,U. + ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ (ⓐV.U) : W → + R L T U → R L (ⓐV.U) W → R L (ⓐV.T) (ⓐV.U) + ) → + (∀L,T,U,W. + ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ U : W → + R L T U → R L U W → R L (ⓝU.T) U + ) → + (∀L,T,U1,U2,V2. + ⦃h, L⦄ ⊢ T : U1 → L ⊢ U1 ⬌* U2 → ⦃h, L⦄ ⊢ U2 : V2 → + R L T U1 →R L U2 V2 →R L T U2 + ) → + ∀L,T,U. ⦃h, L⦄ ⊢ T : U → R L T U. +#h #R #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #L #T #U #H elim (nta_ntaa … H) -L -T -U +// /3 width=1 by ntaa_nta/ /3 width=3 by ntaa_nta/ /3 width=4 by ntaa_nta/ +/3 width=7 by ntaa_nta/ +qed-. + +*) + +(* Basic_1: removed theorems 4: + ty3_getl_subst0 ty3_fsubst0 ty3_csubst0 ty3_subst0 +*) +(* Basic_2A1: removed theorems 2: + ntaa_nta nta_ntaa +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpcs.ma new file mode 100644 index 000000000..4d695a3ec --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpcs.ma @@ -0,0 +1,53 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rt_equivalence/cpcs_cprs.ma". +include "basic_2/dynamic/nta.ma". + +(* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************) + +(* Properties with r-equivalence for terms **********************************) + +lemma nta_conv_cnv (a) (h) (G) (L) (T): + ∀U1. ⦃G,L⦄ ⊢ T :[a,h] U1 → + ∀U2. ⦃G,L⦄ ⊢ U1 ⬌*[h] U2 → ⦃G,L⦄ ⊢ U2 ![a,h] → ⦃G,L⦄ ⊢ T :[a,h] U2. +#a #h #G #L #T #U1 #H1 #U2 #HU12 #HU2 +elim (cnv_inv_cast … H1) -H1 #X1 #HU1 #HT #HUX1 #HTX1 +lapply (cpcs_cprs_conf … HUX1 … HU12) -U1 #H +elim (cpcs_inv_cprs … H) -H #X2 #HX12 #HU12 +/3 width=5 by cnv_cast, cpms_cprs_trans/ +qed-. + +(* Basic_1: was by definition: ty3_conv *) +(* Basic_2A1: was by definition: nta_conv ntaa_conv *) +lemma nta_conv (a) (h) (G) (L) (T): + ∀U1. ⦃G,L⦄ ⊢ T :[a,h] U1 → + ∀U2. ⦃G,L⦄ ⊢ U1 ⬌*[h] U2 → + ∀W2. ⦃G,L⦄ ⊢ U2 :[a,h] W2 → ⦃G,L⦄ ⊢ T :[a,h] U2. +#a #h #G #L #T #U1 #H1 #U2 #HU12 #W2 #H2 +/3 width=3 by nta_conv_cnv, nta_fwd_cnv_sn/ +qed-. + +(* Inversion lemmas with r-equivalence for terms ***************************) + +(* Basic_1: was: ty3_gen_sort *) +(* Basic_2A1: was: nta_inv_sort1 *) +lemma nta_inv_sort_sn (a) (h) (G) (L) (X2): + ∀s. ⦃G,L⦄ ⊢ ⋆s :[a,h] X2 → ⦃G,L⦄ ⊢ ⋆(next h s) ⬌*[h] X2. +#a #h #G #L #X2 #s #H +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_cpms.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpms.ma new file mode 100644 index 000000000..71cc3f94e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpms.ma @@ -0,0 +1,49 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rt_computation/cprs_cprs.ma". +include "basic_2/rt_computation/lprs_cpms.ma". +include "basic_2/dynamic/nta.ma". + +(* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************) + +(* Properties with rt_computation for terms *********************************) + +(* Basic_2A1: was by definition nta_appl ntaa_appl *) +lemma nta_beta (a) (h) (p) (G) (L): + ∀V,W. ⦃G,L⦄ ⊢ V :[a,h] W → + ∀T,U. ⦃G,L⦄ ⊢ ⓛ{p}W.T :[a,h] ⓛ{p}W.U → ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.T :[a,h] ⓐV.ⓛ{p}W.U. +#a #h #p #G #L #V #W #H1 #T #U #H2 +elim (cnv_inv_cast … H1) -H1 #X1 #HW #HV #HWX1 #HVX1 +elim (cnv_inv_cast … H2) -H2 #X2 #HU #HT #HUX2 #HTX2 +/4 width=7 by cnv_cast, cnv_appl, cpms_bind, cpms_appl_dx/ +qed. + +(* Basic_1: was by definition: ty3_appl *) +(* Basic_2A1: was nta_appl_old *) +lemma nta_appl (h) (p) (G) (L): + ∀V,W. ⦃G,L⦄ ⊢ V :[h] W → + ∀T,U. ⦃G,L⦄ ⊢ T :[h] ⓛ{p}W.U → ⦃G,L⦄ ⊢ ⓐV.T :[h] ⓐV.ⓛ{p}W.U. +#h #p #G #L #V #W #H1 #T #U #H2 +elim (cnv_inv_cast … H1) -H1 #X1 #HW #HV #HWX1 #HVX1 +elim (cnv_inv_cast … H2) -H2 #X2 #HU #HT #HUX2 #HTX2 +elim (cpms_inv_abst_sn … HUX2) #W0 #U0 #HW0 #HU0 #H destruct +elim (cprs_conf … HWX1 … HW0) -HW0 #X0 #HX10 #HWX0 +@(cnv_cast … (ⓐV.ⓛ{p}W0.U0)) (**) (* full auto too slow *) +[ /3 width=7 by cnv_appl, cpms_bind/ +| /4 width=11 by cnv_appl, cpms_cprs_trans, cpms_bind/ +| /2 width=1 by cpms_appl_dx/ +| /2 width=1 by cpms_appl_dx/ +] +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_2A1/nta/nta_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_drops.ma similarity index 61% rename from matita/matita/contribs/lambdadelta/basic_2/etc_2A1/nta/nta_lift.etc rename to matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_drops.ma index 57e06a1e9..d8184be86 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc_2A1/nta/nta_lift.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_drops.ma @@ -11,33 +11,13 @@ (* v GNU General Public License Version 2 *) (* *) (**************************************************************************) - +(* include "basic_2/dynamic/nta_alt.ma". (* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************) (* Advanced inversion lemmas ************************************************) -fact nta_inv_sort1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀k0. T = ⋆k0 → - L ⊢ ⋆(next h k0) ⬌* U. -#h #L #T #U #H elim H -L -T -U -[ #L #k #k0 #H destruct // -| #L #K #V #W #U #i #_ #_ #_ #_ #k0 #H destruct -| #L #K #W #V #U #i #_ #_ #_ #_ #k0 #H destruct -| #I #L #V #W #T #U #_ #_ #_ #_ #k0 #H destruct -| #L #V #W #T #U #_ #_ #_ #_ #k0 #H destruct -| #L #V #W #T #U #_ #_ #_ #_ #k0 #H destruct -| #L #T #U #_ #_ #k0 #H destruct -| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #k0 #H destruct - lapply (IHTU1 ??) -IHTU1 [ // | skip ] #Hk0 - lapply (cpcs_trans … Hk0 … HU12) -U1 // -] -qed. - -(* Basic_1: was: ty3_gen_sort *) -lemma nta_inv_sort1: ∀h,L,U,k. ⦃h, L⦄ ⊢ ⋆k : U → L ⊢ ⋆(next h k) ⬌* U. -/2 width=3/ qed-. - fact nta_inv_lref1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀j. T = #j → (∃∃K,V,W,U0. ⇩[0, j] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V : W & ⇧[0, j + 1] W ≡ U0 & L ⊢ U0 ⬌* U @@ -69,34 +49,6 @@ lemma nta_inv_lref1: ∀h,L,U,i. ⦃h, L⦄ ⊢ #i : U → ). /2 width=3/ qed-. -(* Basic_1: was: ty3_gen_bind *) -lemma nta_inv_bind1: ∀h,I,L,Y,X,U. ⦃h, L⦄ ⊢ ⓑ{I}Y.X : U → - ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y : Z1 & ⦃h, L.ⓑ{I}Y⦄ ⊢ X : Z2 & - L ⊢ ⓑ{I}Y.Z2 ⬌* U. -#h #I #L #Y #X #U #H -elim (ntaa_inv_bind1 … (nta_ntaa … H)) -H /3 width=3 by ntaa_nta, ex3_2_intro/ -qed-. - -fact nta_inv_cast1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. T = ⓝY.X → - ⦃h, L⦄ ⊢ X : Y ∧ L ⊢ Y ⬌* U. -#h #L #T #U #H elim H -L -T -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 #T #U #_ #_ #_ #_ #X #Y #H destruct -| #L #V #W #T #U #_ #_ #_ #_ #X #Y #H destruct -| #L #T #U #HTU #_ #X #Y #H destruct /2 width=1/ -| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #X #Y #H destruct - elim (IHTU1 ???) -IHTU1 [4: // |2,3: skip ] #HXY #HU1 - lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=1/ -] -qed. - -(* Basic_1: was: ty3_gen_cast *) -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-. - (* Advanced forvard lemmas **************************************************) fact nta_fwd_pure1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. T = ⓐY.X → @@ -120,25 +72,11 @@ lemma nta_fwd_pure1: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓐY.X : U → ∃∃V,W. ⦃h, L⦄ ⊢ Y : W & ⦃h, L⦄ ⊢ X : V & L ⊢ ⓐY.V ⬌* U. /2 width=3/ qed-. -(* Basic_1: was: ty3_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-. - -(* Advanced properties ******************************************************) - -(* Basic_1: was: ty3_appl *) -lemma nta_appl_old: ∀h,L,V,W,T,U. ⦃h, L⦄ ⊢ V : W → ⦃h, L⦄ ⊢ T : ⓛW.U → - ⦃h, L⦄ ⊢ ⓐV.T : ⓐV.ⓛW.U. -#h #L #V #W #T #U #HVW #HTU -elim (nta_fwd_correct … HTU) #X #H -elim (nta_inv_bind1 … H) -H /4 width=2/ -qed. - (* Properties on relocation *************************************************) (* Basic_1: was: ty3_lift *) +(* Basic_2A1: was: ntaa_lift *) lemma nta_lift: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 : U1 → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 → ∀T2. ⇧[d, e] T1 ≡ T2 → ∀U2. ⇧[d, e] U1 ≡ U2 → ⦃h, L2⦄ ⊢ T2 : U2. /4 width=9 by ntaa_nta, nta_ntaa, ntaa_lift/ 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 new file mode 100644 index 000000000..ab3b33ad5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma @@ -0,0 +1,119 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rt_equivalence/cpcs_cprs.ma". +include "basic_2/dynamic/cnv_preserve.ma". +include "basic_2/dynamic/nta.ma". + +(* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************) + +(* Properties based on preservation *****************************************) + +lemma cnv_cpms_nta (a) (h) (G) (L): + ∀T. ⦃G,L⦄ ⊢ T ![a,h] → ∀U.⦃G,L⦄ ⊢ T ➡*[1,h] U → ⦃G,L⦄ ⊢ T :[a,h] U. +/3 width=4 by cnv_cast, cnv_cpms_trans/ qed. + +lemma cnv_nta_sn (a) (h) (G) (L): + ∀T. ⦃G,L⦄ ⊢ T ![a,h] → ∃U. ⦃G,L⦄ ⊢ T :[a,h] U. +#a #h #G #L #T #HT +elim (cnv_fwd_cpm_SO … HT) #U #HTU +/4 width=2 by cnv_cpms_nta, cpm_cpms, ex_intro/ +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. +#h #G #L #T #U #H1 #V #H2 +elim (cnv_inv_cast … H1) -H1 #X0 #HU #HT #HUX0 #HTX0 +elim (cnv_inv_appl … H2) #n #p #X1 #X2 #_ #HV #_ #HVX1 #HUX2 +elim (cnv_cpms_conf … HU … HUX0 … HUX2) -HU -HUX2 +