From dc20d16b32940a94d29a04de0d4fe1f80e00a73f Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 2 Nov 2018 21:52:43 +0100 Subject: [PATCH] update in basic_2 MIME-Version: 1.0 Content-Type: text/plain; charset=utf8 Content-Transfer-Encoding: 8bit + more properties on types from λδ-1A including: type preservation by valid r-equivalence --- .../basic_2/dynamic/cnv_preserve.ma | 16 ++ .../lambdadelta/basic_2/dynamic/nta_aaa.ma | 56 +++++ .../lambdadelta/basic_2/dynamic/nta_cpms.ma | 18 +- .../lambdadelta/basic_2/dynamic/nta_drops.ma | 2 +- .../lambdadelta/basic_2/dynamic/nta_fsb.ma | 32 +++ .../lambdadelta/basic_2/dynamic/nta_ind.ma | 2 +- .../basic_2/dynamic/nta_preserve.ma | 65 +++++ .../basic_2/dynamic/nta_preserve_cpcs.ma | 62 +++++ .../lambdadelta/basic_2/etc/missing.txt | 7 + .../lambdadelta/basic_2/etc/nta/nta.etc | 11 +- .../basic_2/etc/{ => nta}/nta_extra.etc | 0 .../{etc_2A1 => etc}/nta/nta_ltpss.etc | 0 .../basic_2/{etc_2A1 => etc}/nta/nta_sta.etc | 4 + .../basic_2/{etc_2A1 => etc}/nta/nta_thin.etc | 0 .../basic_2/etc_2A1/{nta => lsubn}/lsubn.etc | 0 .../etc_2A1/{nta => lsubn}/lsubn_cpcs.etc | 0 .../etc_2A1/{nta => lsubn}/lsubn_ldrop.etc | 0 .../etc_2A1/{nta => lsubn}/lsubn_nta.etc | 0 .../basic_2/etc_2A1/nta/nta_aaa.etc | 49 ---- .../basic_2/etc_2A1/nta/nta_alt.etc | 190 -------------- .../basic_2/etc_2A1/nta/nta_ltpr.etc | 235 ------------------ .../etc_2A1/{ => snv}/snv_preserve.etc | 0 .../lambdadelta/basic_2/web/basic_2_src.tbl | 2 +- 23 files changed, 268 insertions(+), 483 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_aaa.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_fsb.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve_cpcs.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/missing.txt rename matita/matita/contribs/lambdadelta/basic_2/etc/{ => nta}/nta_extra.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_2A1 => etc}/nta/nta_ltpss.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_2A1 => etc}/nta/nta_sta.etc (94%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_2A1 => etc}/nta/nta_thin.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc_2A1/{nta => lsubn}/lsubn.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc_2A1/{nta => lsubn}/lsubn_cpcs.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc_2A1/{nta => lsubn}/lsubn_ldrop.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc_2A1/{nta => lsubn}/lsubn_nta.etc (100%) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc_2A1/nta/nta_aaa.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc_2A1/nta/nta_alt.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc_2A1/nta/nta_ltpr.etc rename matita/matita/contribs/lambdadelta/basic_2/etc_2A1/{ => snv}/snv_preserve.etc (100%) 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 9e93c859d..c4edc5508 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve.ma @@ -54,7 +54,23 @@ lemma cnv_cpms_trans_lpr (a) (h) (G) (L) (T): IH_cnv_cpms_trans_lpr a h G L T. @(cpms_ind_dx … H) -n -T2 /3 width=6 by cnv_cpm_trans_lpr/ qed-. +lemma cnv_cpm_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_cpm_trans_lpr/ qed-. + +(* Note: this is the preservation property *) 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-. + +lemma cnv_lpr_trans (a) (h) (G): + ∀L1,T. ⦃G,L1⦄ ⊢ T ![a,h] → ∀L2. ⦃G,L1⦄ ⊢ ➡[h] L2 → ⦃G,L2⦄ ⊢ T ![a,h]. +/2 width=6 by cnv_cpm_trans_lpr/ qed-. + +lemma cnv_lprs_trans (a) (h) (G): + ∀L1,T. ⦃G,L1⦄ ⊢ T ![a,h] → ∀L2. ⦃G,L1⦄ ⊢ ➡*[h] L2 → ⦃G,L2⦄ ⊢ T ![a,h]. +#a #h #G #L1 #T #HT #L2 #H +@(lprs_ind_dx … H) -L2 /2 width=3 by cnv_lpr_trans/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_aaa.ma new file mode 100644 index 000000000..0161996dd --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_aaa.ma @@ -0,0 +1,56 @@ +(**************************************************************************) +(* ___ *) +(* ||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/dynamic/cnv_aaa.ma". +include "basic_2/dynamic/nta.ma". + +(* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************) + +(* Forward lemmas with atomic arity assignment for terms ********************) + +(* Note: this means that no type is a universe *) +lemma nta_fwd_aaa (a) (h) (G) (L): + ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] U → ∃∃A. ⦃G,L⦄ ⊢ T ⁝ A & ⦃G,L⦄ ⊢ U ⁝ A. +#a #h #G #L #T #U #H +elim (cnv_fwd_aaa … H) -H #A #H +elim (aaa_inv_cast … H) -H #HU #HT +/2 width=3 by ex2_intro/ +qed-. + +(* Advanced inversion lemmas ************************************************) + +(* Basic_1: uses: ty3_predicative *) +lemma nta_abst_predicative (a) (h) (p) (G) (L): + ∀W,T. ⦃G,L⦄ ⊢ ⓛ{p}W.T :[a,h] W → ⊥. +#a #h #p #G #L #W #T #H +elim (nta_fwd_aaa … H) -a -h #X #H #H1W +elim (aaa_inv_abst … H) -p #B #A #H2W #_ #H destruct -T +lapply (aaa_mono … H1W … H2W) -G -L -W #H +elim (discr_apair_xy_x … H) +qed-. + +(* Basic_2A1: uses: ty3_repellent *) +theorem nta_abst_repellent (a) (h) (p) (G) (K): + ∀W,T,U1. ⦃G,K⦄ ⊢ ⓛ{p}W.T :[a,h] U1 → + ∀U2. ⦃G,K.ⓛW⦄ ⊢ T :[a,h] U2 → ⬆*[1] U1 ≘ U2 → ⊥. +#a #h #p #G #K #W #T #U1 #H1 #U2 #H2 #HU12 +elim (nta_fwd_aaa … H2) -H2 #A2 #H2T #H2U2 +elim (nta_fwd_aaa … H1) -H1 #X1 #H1 #HU1 +elim (aaa_inv_abst … H1) -a -h -p #B #A1 #_ #H1T #H destruct +lapply (aaa_mono … H1T … H2T) -T #H destruct +lapply (aaa_inv_lifts … H2U2 (Ⓣ) … K … HU12) +[ /3 width=1 by drops_refl, drops_drop/ ] -W -U2 #H2U1 +lapply (aaa_mono … HU1 … H2U1) -G -K -U1 #H +elim (discr_apair_xy_y … H) +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 index 1cdaf8c46..8dbb60c79 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpms.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpms.ma @@ -18,10 +18,10 @@ include "basic_2/dynamic/nta.ma". (* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************) -(* Properties with rt_computation for terms *********************************) +(* Properties with advanced rt_computation for terms ************************) (* Basic_2A1: was by definition nta_appl ntaa_appl *) -lemma nta_beta (a) (h) (p) (G) (K): +lemma nta_appl_abst (a) (h) (p) (G) (K): ∀V,W. ⦃G,K⦄ ⊢ V :[a,h] W → ∀T,U. ⦃G,K.ⓛW⦄ ⊢ T :[a,h] U → ⦃G,K⦄ ⊢ ⓐV.ⓛ{p}W.T :[a,h] ⓐV.ⓛ{p}W.U. #a #h #p #G #K #V #W #H1 #T #U #H2 @@ -47,3 +47,17 @@ elim (cprs_conf … HWX1 … HW0) -HW0 #X0 #HX10 #HWX0 | /2 width=1 by cpms_appl_dx/ ] qed. + +(* Inversion lemmas with advanced rt_computation for terms ******************) + +lemma nta_inv_abst_bi_cnv (a) (h) (p) (G) (K) (W): + ∀T,U. ⦃G,K⦄ ⊢ ⓛ{p}W.T :[a,h] ⓛ{p}W.U → + ∧∧ ⦃G,K⦄ ⊢ W ![a,h] & ⦃G,K.ⓛW⦄ ⊢ T :[a,h] U. +#a #h #p #G #K #W #T #U #H +elim (cnv_inv_cast … H) -H #X #HWU #HWT #HUX #HTX +elim (cnv_inv_bind … HWU) -HWU #HW #HU +elim (cnv_inv_bind … HWT) -HWT #_ #HT +elim (cpms_inv_abst_sn … HUX) -HUX #W0 #X0 #_ #HUX0 #H destruct +elim (cpms_inv_abst_bi … HTX) -HTX #_ #HTX0 -W0 +/3 width=3 by cnv_cast, conj/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_drops.ma index 046b87460..b65c1bdc8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_drops.ma @@ -73,7 +73,7 @@ lemma nta_lifts_bi (a) (h) (G): d_liftable2_bi … lifts (nta a h G). /3 width=12 by nta_lifts_sn, d_liftable2_sn_bi, lifts_mono/ qed-. (* Basic_1: was by definition: ty3_abbr *) -(* Basic_2A1: was by definition: nta_ldef *) +(* Basic_2A1: was by definition: nta_ldef ntaa_ldef *) lemma nta_ldef_drops (a) (h) (G) (K) (L) (i): ∀V,W. ⦃G,K⦄ ⊢ V :[a,h] W → ∀U. ⬆*[↑i] W ≘ U → ⬇*[i] L ≘ K.ⓓV → ⦃G,L⦄ ⊢ #i :[a,h] U. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_fsb.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_fsb.ma new file mode 100644 index 000000000..b96b1cfd5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_fsb.ma @@ -0,0 +1,32 @@ +(**************************************************************************) +(* ___ *) +(* ||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/dynamic/cnv_fsb.ma". +include "basic_2/dynamic/nta.ma". + +(* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************) + +(* Forward lemmas with strongly rst-normalizing closures ********************) + +(* Note: this is an extended stong normalization property *) +(* Note: this might use fsb_inv_cast (still to be proved) *) +(* Basic_1: uses: ty3_sn3 *) +(* Basic_2A1: uses: nta_fwd_csn *) +theorem nta_fwd_fsb (a) (h) (o) (G) (L): + ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] U → + ∧∧ ≥[h,o] 𝐒⦃G,L,T⦄ & ≥[h,o] 𝐒⦃G,L,U⦄. +#a #h #o #G #L #T #U #H +elim (cnv_inv_cast … H) #X #HU #HT #_ #_ -X +/3 width=2 by cnv_fwd_fsb, conj/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma index 4de1ae801..4f9b52385 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma @@ -179,5 +179,5 @@ lemma nta_ind_ext_cnv (h) (Q:relation4 …): lapply (nta_fwd_cnv_dx … HTU) #H elim (cnv_inv_bind … H) -H #_ #HU elim (cnv_nta_sn … HU) -HU #X #HUX -/4 width=2 by nta_beta, nta_fwd_cnv_sn/ +/4 width=2 by nta_appl_abst, nta_fwd_cnv_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 b308c118d..8d69b3ca2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma @@ -56,6 +56,47 @@ elim (cpms_inv_abst_sn … H) -H #X3 #X4 #HX13 #HX24 #H destruct #H destruct qed. +(* Basic_1: uses: ty3_sred_wcpr0_pr0 *) +lemma nta_cpr_conf_lpr (a) (h) (G): + ∀L1,T1,U. ⦃G,L1⦄ ⊢ T1 :[a,h] U → ∀T2. ⦃G,L1⦄ ⊢ T1 ➡[h] T2 → + ∀L2. ⦃G,L1⦄ ⊢ ➡[h] L2 → ⦃G,L2⦄ ⊢ T2 :[a,h] U. +#a #h #G #L1 #T1 #U #H #T2 #HT12 #L2 #HL12 +/3 width=6 by cnv_cpm_trans_lpr, cpm_cast/ +qed-. + +(* Basic_1: uses: ty3_sred_pr2 ty3_sred_pr0 *) +lemma nta_cpr_conf (a) (h) (G) (L): + ∀T1,U. ⦃G,L⦄ ⊢ T1 :[a,h] U → + ∀T2. ⦃G,L⦄ ⊢ T1 ➡[h] T2 → ⦃G,L⦄ ⊢ T2 :[a,h] U. +#a #h #G #L #T1 #U #H #T2 #HT12 +/3 width=6 by cnv_cpm_trans, cpm_cast/ +qed-. + +(* Note: this is the preservation property *) +(* Basic_1: uses: ty3_sred_pr3 ty3_sred_pr1 *) +lemma nta_cprs_conf (a) (h) (G) (L): + ∀T1,U. ⦃G,L⦄ ⊢ T1 :[a,h] U → + ∀T2. ⦃G,L⦄ ⊢ T1 ➡*[h] T2 → ⦃G,L⦄ ⊢ T2 :[a,h] U. +#a #h #G #L #T1 #U #H #T2 #HT12 +/3 width=6 by cnv_cpms_trans, cpms_cast/ +qed-. + +(* Basic_1: uses: ty3_cred_pr2 *) +lemma nta_lpr_conf (a) (h) (G): + ∀L1,T,U. ⦃G,L1⦄ ⊢ T :[a,h] U → + ∀L2. ⦃G,L1⦄ ⊢ ➡[h] L2 → ⦃G,L2⦄ ⊢ T :[a,h] U. +#a #h #G #L1 #T #U #HTU #L2 #HL12 +/2 width=3 by cnv_lpr_trans/ +qed-. + +(* Basic_1: uses: ty3_cred_pr3 *) +lemma nta_lprs_conf (a) (h) (G): + ∀L1,T,U. ⦃G,L1⦄ ⊢ T :[a,h] U → + ∀L2. ⦃G,L1⦄ ⊢ ➡*[h] L2 → ⦃G,L2⦄ ⊢ T :[a,h] U. +#a #h #G #L1 #T #U #HTU #L2 #HL12 +/2 width=3 by cnv_lprs_trans/ +qed-. + (* Inversion lemmas based on preservation ***********************************) lemma nta_inv_ldef_sn (a) (h) (G) (K) (V): @@ -206,6 +247,19 @@ elim (cpms_inv_cast1 … H2) -H2 [ * || * ] ] qed-. +(* Basic_1: uses: ty3_gen_lift *) +(* Note: "⦃G,L⦄ ⊢ U2 ⬌*[h] X2" can be "⦃G,L⦄ ⊢ X2 ➡*[h] U2" *) +lemma nta_inv_lifts_sn (a) (h) (G): + ∀L,T2,X2. ⦃G,L⦄ ⊢ T2 :[a,h] X2 → + ∀b,f,K. ⬇*[b,f] L ≘ K → ∀T1. ⬆*[f] T1 ≘ T2 → + ∃∃U1,U2. ⦃G,K⦄ ⊢ T1 :[a,h] U1 & ⬆*[f] U1 ≘ U2 & ⦃G,L⦄ ⊢ U2 ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![a,h]. +#a #h #G #L #T2 #X2 #H #b #f #K #HLK #T1 #HT12 +elim (cnv_inv_cast … H) -H #U2 #HX2 #HT2 #HXU2 #HTU2 +lapply (cnv_inv_lifts … HT2 … HLK … HT12) -HT2 #HT1 +elim (cpms_inv_lifts_sn … HTU2 … HLK … HT12) -T2 -HLK #U1 #HU12 #HTU1 +/3 width=5 by cnv_cpms_nta, cpcs_cprs_sn, ex4_2_intro/ +qed-. + (* Forward lemmas based on preservation *************************************) (* Basic_1: was: ty3_unique *) @@ -217,3 +271,14 @@ elim (cnv_inv_cast … H2) -H2 #X2 #_ #HT #HUX2 #HTX2 lapply (cnv_cpms_conf_eq … HT … HTX1 … HTX2) -T #HX12 /3 width=3 by cpcs_cprs_div, cpcs_cprs_step_sn/ qed-. + +(* Advanced properties ******************************************************) + +(* Basic_1: uses: ty3_sconv_pc3 *) +lemma nta_cpcs_bi (a) (h) (G) (L): + ∀T1,U1. ⦃G,L⦄ ⊢ T1 :[a,h] U1 → ∀T2,U2. ⦃G,L⦄ ⊢ T2 :[a,h] U2 → + ⦃G,L⦄ ⊢ T1 ⬌*[h] T2 → ⦃G,L⦄ ⊢ U1 ⬌*[h] U2. +#a #h #G #L #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HT12 +elim (cpcs_inv_cprs … HT12) -HT12 #T0 #HT10 #HT02 +/3 width=6 by nta_mono, nta_cprs_conf/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve_cpcs.ma new file mode 100644 index 000000000..cbcd378a4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve_cpcs.ma @@ -0,0 +1,62 @@ +(**************************************************************************) +(* ___ *) +(* ||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/dynamic/nta_cpcs.ma". +include "basic_2/dynamic/nta_preserve.ma". + +(* NATIVE TYPE ASSIGNMENT FOR TERMS ****************************************) + +(* Properties based on type equivalence and preservation *******************) + +(* Basic_1: uses: ty3_tred *) +lemma nta_cprs_trans (a) (h) (G) (L): + ∀T,U1. ⦃G,L⦄ ⊢ T :[a,h] U1 → ∀U2. ⦃G,L⦄ ⊢ U1 ➡*[h] U2 → ⦃G,L⦄ ⊢ T :[a,h] U2. +#a #h #G #L #T #U1 #H #U2 #HU12 +/4 width=4 by nta_conv_cnv, nta_fwd_cnv_dx, cnv_cpms_trans, cpcs_cprs_dx/ +qed-. + +(* Basic_1: uses: ty3_sred_back *) +lemma cprs_nta_trans (a) (h) (G) (L): + ∀T1,U0. ⦃G,L⦄ ⊢ T1 :[a,h] U0 → ∀T2. ⦃G,L⦄ ⊢ T1 ➡*[h] T2 → + ∀U. ⦃G,L⦄ ⊢ T2 :[a,h] U → ⦃G,L⦄ ⊢ T1 :[a,h] U. +#a #h #G #L #T1 #U0 #HT1 #T2 #HT12 #U #H +lapply (nta_cprs_conf … HT1 … HT12) -HT12 #HT2 +/4 width=6 by nta_mono, nta_conv_cnv, nta_fwd_cnv_dx/ +qed-. + +lemma cprs_nta_trans_cnv (a) (h) (G) (L): + ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → ∀T2. ⦃G,L⦄ ⊢ T1 ➡*[h] T2 → + ∀U. ⦃G,L⦄ ⊢ T2 :[a,h] U → ⦃G,L⦄ ⊢ T1 :[a,h] U. +#a #h #G #L #T1 #HT1 #T2 #HT12 #U #H +elim (cnv_nta_sn … HT1) -HT1 #U0 #HT1 +/2 width=3 by cprs_nta_trans/ +qed-. + +(* Basic_1: uses: ty3_sconv *) +lemma nta_cpcs_conf (a) (h) (G) (L): + ∀T1,U. ⦃G,L⦄ ⊢ T1 :[a,h] U → ∀T2. ⦃G,L⦄ ⊢ T1 ⬌*[h] T2 → + ∀U0. ⦃G,L⦄ ⊢ T2 :[a,h] U0 → ⦃G,L⦄ ⊢ T2 :[a,h] U. +#a #h #G #L #T1 #U #HT1 #T2 #HT12 #U0 #HT2 +elim (cpcs_inv_cprs … HT12) -HT12 #T0 #HT10 #HT02 +/3 width=5 by cprs_nta_trans, nta_cprs_conf/ +qed-. + +(* Note: type preservation by valid r-equivalence *) +lemma nta_cpcs_conf_cnv (a) (h) (G) (L): + ∀T1,U. ⦃G,L⦄ ⊢ T1 :[a,h] U → + ∀T2. ⦃G,L⦄ ⊢ T1 ⬌*[h] T2 → ⦃G,L⦄ ⊢ T2 ![a,h] → ⦃G,L⦄ ⊢ T2 :[a,h] U. +#a #h #G #L #T1 #U #HT1 #T2 #HT12 #HT2 +elim (cnv_nta_sn … HT2) -HT2 #U0 #HT2 +/2 width=3 by nta_cpcs_conf/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/missing.txt b/matita/matita/contribs/lambdadelta/basic_2/etc/missing.txt new file mode 100644 index 000000000..00d31a949 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/missing.txt @@ -0,0 +1,7 @@ +ty3_gen_cvoid +ty3_acyclic +ty3_gen_appl_nf2 +ty3_nf2_inv_all (and following) +pc3_dec +pc3_abst_dec +ty3_inference 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 8df1f8f5e..166fd2105 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta.etc @@ -1,3 +1,7 @@ +(* 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 @@ -9,14 +13,13 @@ lemma nta_pure (* Basic_2A1: was: nta_inv_bind1 ntaa_inv_bind1 *) lemma nta_inv_bind_sn -(* Basic_1: was by definition: ty3_abst *) -(* Basic_2A1: was by definition: nta_ldec *) -lemma nta_ldec_drops - (* 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 diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/nta_extra.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_extra.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/nta_extra.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_extra.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_2A1/nta/nta_ltpss.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_ltpss.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_2A1/nta/nta_ltpss.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_ltpss.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_2A1/nta/nta_sta.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_sta.etc similarity index 94% rename from matita/matita/contribs/lambdadelta/basic_2/etc_2A1/nta/nta_sta.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_sta.etc index 6268b98b1..b465eab41 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc_2A1/nta/nta_sta.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_sta.etc @@ -40,3 +40,7 @@ lemma nta_fwd_sta: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → lapply (cpcs_trans … HU01 … HU12) -U1 /2 width=3/ ] qed-. +(* + Lemma ty3_sty0: (g:?; c:?; u,t1:?) (ty3 g c u t1) -> + (t2:?) (sty0 g c u t2) -> (ty3 g c u t2). +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_2A1/nta/nta_thin.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_thin.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_2A1/nta/nta_thin.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_thin.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_2A1/nta/lsubn.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_2A1/lsubn/lsubn.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_2A1/nta/lsubn.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc_2A1/lsubn/lsubn.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_2A1/nta/lsubn_cpcs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_2A1/lsubn/lsubn_cpcs.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_2A1/nta/lsubn_cpcs.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc_2A1/lsubn/lsubn_cpcs.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_2A1/nta/lsubn_ldrop.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_2A1/lsubn/lsubn_ldrop.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_2A1/nta/lsubn_ldrop.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc_2A1/lsubn/lsubn_ldrop.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_2A1/nta/lsubn_nta.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_2A1/lsubn/lsubn_nta.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_2A1/nta/lsubn_nta.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc_2A1/lsubn/lsubn_nta.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_2A1/nta/nta_aaa.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_2A1/nta/nta_aaa.etc deleted file mode 100644 index 962856983..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc_2A1/nta/nta_aaa.etc +++ /dev/null @@ -1,49 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/computation/csn_aaa.ma". -include "basic_2/equivalence/lcpcs_aaa.ma". -include "basic_2/dynamic/nta.ma". - -(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************) - -(* Forward lemmas on atomic arity assignment for terms **********************) - -lemma nta_fwd_aaa: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∃∃A. L ⊢ T ⁝ A & L ⊢ U ⁝ A. -#h #L #T #U #H elim H -L -T -U -[ /2 width=3/ -| #L #K #V #W #U #i #HLK #_ #HWU * #B #HV #HW - lapply (ldrop_fwd_ldrop2 … HLK) /3 width=9/ -| #L #K #W #V #U #i #HLK #_ #HWU * #B #HW #_ -V - lapply (ldrop_fwd_ldrop2 … HLK) /3 width=9/ -| * #L #V #W #T #U #_ #_ * #B #HV #HW * #A #HT #HU - [ /3 width=3/ | /3 width=5/ ] -| #L #V #W #T #U #_ #_ * #B #HV #HW * #X #H1 #H2 - elim (aaa_inv_abst … H1) -H1 #B1 #A1 #HW1 #HT #H destruct - elim (aaa_inv_abst … H2) -H2 #B2 #A #_ #HU #H destruct - lapply (aaa_mono … HW1 … HW) -HW1 #H destruct /4 width=5/ -| #L #V #W #T #U #_ #_ * #X #HT #HUX * #A #H #_ -W - elim (aaa_inv_appl … H) -H #B #HV #HUA - lapply (aaa_mono … HUA … HUX) -HUX #H destruct /3 width=5/ -| #L #T #U #_ * #A #HT #HU /3 width=3/ -| #L #T #U1 #U2 #V2 #_ #HU12 #_ * #X #HT #HU1 * #A #HU2 #_ - lapply (aaa_cpcs_mono … HU12 … HU1 … HU2) -U1 #H destruct /2 width=3/ -] -qed-. - -(* Note: this is the stong normalization property *) -(* Basic_1: was only: ty3_sn3 *) -theorem nta_fwd_csn: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → L ⊢ ⬇* T ∧ L ⊢ ⬇* U. -#h #L #T #U #H elim (nta_fwd_aaa … H) -H /3 width=2/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_2A1/nta/nta_alt.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_2A1/nta/nta_alt.etc deleted file mode 100644 index 8cbd59518..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc_2A1/nta/nta_alt.etc +++ /dev/null @@ -1,190 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/equivalence/cpcs_cpcs.ma". -include "basic_2/dynamic/nta.ma". - -(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************) - -(* alternative definition of nta *) -inductive ntaa (h:sh): lenv → relation term ≝ -| ntaa_sort: ∀L,k. ntaa h L (⋆k) (⋆(next h k)) -| ntaa_ldef: ∀L,K,V,W,U,i. ⇩[0, i] L ≡ K. ⓓV → ntaa h K V W → - ⇧[0, i + 1] W ≡ U → ntaa h L (#i) U -| ntaa_ldec: ∀L,K,W,V,U,i. ⇩[0, i] L ≡ K. ⓛW → ntaa h K W V → - ⇧[0, i + 1] W ≡ U → ntaa h L (#i) U -| ntaa_bind: ∀I,L,V,W,T,U. ntaa h L V W → ntaa h (L. ⓑ{I} V) T U → - ntaa h L (ⓑ{I}V.T) (ⓑ{I}V.U) -| ntaa_appl: ∀L,V,W,T,U. ntaa h L V W → ntaa h L (ⓛW.T) (ⓛW.U) → - ntaa h L (ⓐV.ⓛW.T) (ⓐV.ⓛW.U) -| ntaa_pure: ∀L,V,W,T,U. ntaa h L T U → ntaa h L (ⓐV.U) W → - ntaa h L (ⓐV.T) (ⓐV.U) -| ntaa_cast: ∀L,T,U,W. ntaa h L T U → ntaa h L U W → ntaa h L (ⓝU. T) U -| ntaa_conv: ∀L,T,U1,U2,V2. ntaa h L T U1 → L ⊢ U1 ⬌* U2 → ntaa h L U2 V2 → - ntaa h L T U2 -. - -interpretation "native type assignment (term) alternative" - 'NativeTypeAlt h L T U = (ntaa h L T U). - -(* Advanced inversion lemmas ************************************************) - -fact ntaa_inv_bind1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T :: U → ∀J,X,Y. T = ⓑ{J}Y.X → - ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y :: Z1 & ⦃h, L.ⓑ{J}Y⦄ ⊢ X :: Z2 & - L ⊢ ⓑ{J}Y.Z2 ⬌* U. -#h #L #T #U #H elim H -L -T -U -[ #L #k #J #X #Y #H destruct -| #L #K #V #W #U #i #_ #_ #_ #_ #J #X #Y #H destruct -| #L #K #W #V #U #i #_ #_ #_ #_ #J #X #Y #H destruct -| #I #L #V #W #T #U #HVW #HTU #_ #_ #J #X #Y #H destruct /2 width=3/ -| #L #V #W #T #U #_ #_ #_ #_ #J #X #Y #H destruct -| #L #V #W #T #U #_ #_ #_ #_ #J #X #Y #H destruct -| #L #T #U #W #_ #_ #_ #_ #J #X #Y #H destruct -| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #J #X #Y #H destruct - elim (IHTU1 ????) -IHTU1 [5: // |2,3,4: skip ] #Z1 #Z2 #HZ1 #HZ2 #HU1 - lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=3/ -] -qed. - -lemma ntaa_inv_bind1: ∀h,J,L,Y,X,U. ⦃h, L⦄ ⊢ ⓑ{J}Y.X :: U → - ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y :: Z1 & ⦃h, L.ⓑ{J}Y⦄ ⊢ X :: Z2 & - L ⊢ ⓑ{J}Y.Z2 ⬌* U. -/2 width=3/ qed-. - -lemma ntaa_nta: ∀h,L,T,U. ⦃h, L⦄ ⊢ T :: U → ⦃h, L⦄ ⊢ T : U. -#h #L #T #U #H elim H -L -T -U -// /2 width=1/ /2 width=2/ /2 width=3/ /2 width=6/ -qed-. - -(* Properties on relocation *************************************************) - -lemma ntaa_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. -#h #L1 #T1 #U1 #H elim H -L1 -T1 -U1 -[ #L1 #k #L2 #d #e #HL21 #X1 #H1 #X2 #H2 - >(lift_inv_sort1 … H1) -X1 - >(lift_inv_sort1 … H2) -X2 // -| #L1 #K1 #V1 #W1 #W #i #HLK1 #_ #HW1 #IHVW1 #L2 #d #e #HL21 #X #H #U2 #HWU2 - elim (lift_inv_lref1 … H) * #Hid #H destruct - [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // #W2 #HW12 #HWU2 - elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H - elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #V2 #HK21 #HV12 #H destruct - /3 width=8/ - | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2 - lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/ - ] -| #L1 #K1 #W1 #V1 #W #i #HLK1 #_ #HW1 #IHWV1 #L2 #d #e #HL21 #X #H #U2 #HWU2 - elim (lift_inv_lref1 … H) * #Hid #H destruct - [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // (cprs_inv_sort1 … H) -H // -| -| -| -| -| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHTU1 #IHUW1 #L2 #HL12 #T2 #H - elim (cprs_inv_appl1 … H) -H * - [ #V2 #T0 #HV12 #HT10 #H destruct - elim (nta_fwd_correct h L2 (ⓐV1.T1) (ⓐV1.U1) ?) [2: /3 width=2/ ] #U - @(nta_conv … (ⓐV2.U1)) (* /2 width=1/*) [ /4 width=2/] (**) (* explicit constructor, /5 width=5/ is too slow *) - | #V2 #W2 #T0 #HV12 #HT10 #HT02 - lapply (IHTU1 … HL12 (ⓛW2.T0) ?) -IHTU1 /2 width=1/ -HT10 #H - elim (nta_inv_bind1 … H) -H #W #U0 #HW2 #HTU0 #HU01 - elim (cpcs_inv_abst1 … HU01) -HU01 #W #U #HU1 #HU0 - lapply (IHUW1 … HL12 (ⓐV2.ⓛW.U) ?) -IHUW1 -HL12 /2 width=1/ -HV12 #H - - - - elim (nta_fwd_pure1 … H) -H #W0 #U2 #HVU2 #H #HW01 - elim (nta_inv_bind1 … H) -H #W3 #U3 #HW3 #HU3 #H - elim (cpcs_inv_abst1 … H) -H #W4 #U4 -*) -(* -axiom nta_ltpr_tpr_conf: ∀h,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → ∀L2. L1 ➡ L2 → - ∀T2. T1 ➡ T2 → ⦃h, L2⦄ ⊢ T2 : U. -#h #L1 #T1 #U #H @(nta_ind_alt … H) -L1 -T1 -U -[ #L1 #k #L2 #_ #T2 #H - >(tpr_inv_atom1 … H) -H // -| #L1 #K1 #V1 #W #U #i #HLK1 #_ #HWU #IHV1 #L2 #HL12 #T2 #H - >(tpr_inv_atom1 … H) -T2 - elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #HLK2 #H - elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=6/ -| #L1 #K1 #W1 #V1 #U1 #i #HLK1 #HWV1 #HWU1 #IHWV1 #L2 #HL12 #T2 #H - >(tpr_inv_atom1 … H) -T2 - elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #HLK2 #H - elim (ltpr_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct - lapply (ldrop_fwd_ldrop2 … HLK2) #HLK - elim (lift_total V1 0 (i+1)) #W #HW - lapply (nta_lift h … HLK … HWU1 … HW) /2 width=1/ -HLK -HW - elim (lift_total W2 0 (i+1)) #U2 #HWU2 - lapply (tpr_lift … HW12 … HWU1 … HWU2) -HWU1 #HU12 - @(nta_conv … U2) /2 width=1/ /3 width=6/ (**) (* explicit constructor, /3 width=6/ is too slow *) -| #I #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #HL12 #X #H - elim (tpr_inv_bind1 … H) -H * - [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct - lapply (IHVW1 … HL12 … HV12) #HV2W1 - lapply (IHVW1 L2 … V1 ?) // -IHVW1 #HWV1 - lapply (IHTU1 (L2.ⓑ{I}V2) … HT10) -HT10 /2 width=1/ #HT0U1 - lapply (IHTU1 (L2.ⓑ{I}V1) ? T1 ?) -IHTU1 // /2 width=1/ -HL12 #H - lapply (tps_lsubs_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 /2 width=1/ #HT02 - lapply (nta_tps_conf … HT0U1 … HT02) -T0 #HT2U1 - elim (nta_fwd_correct … H) -H #U2 #HU12 - @(nta_conv … (ⓑ{I}V2.U1)) /2 width=2/ /3 width=1/ (**) (* explicit constructor, /4 width=6/ is too slow *) - | #T #HT1 #HTX #H destruct - lapply (IHVW1 … HL12 V1 ?) -IHVW1 // #HVW1 - elim (lift_total X 0 1) #Y #HXY - lapply (tpr_lift … HTX … HT1 … HXY) -T #H - lapply (IHTU1 (L2.ⓓV1) … H) -T1 /2 width=1/ -L1 #H - elim (nta_fwd_correct … H) #T1 #HUT1 - elim (nta_thin_conf … H L2 0 (0+1) ? ?) -H /2 width=1/ /3 width=1/ #T #U #HTU #H - normalize in ⊢ (??%??? → ?); #HU1 - lapply (delift_inv_lift1_eq … H L2 … HXY) -Y /2 width=1/ #H destruct - @(nta_conv … U) // /2 width=2/ - ] -| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #HL12 #X #H - elim (tpr_inv_appl1 … H) -H * - [ #V2 #Y #HV12 #HY #H destruct - elim (tpr_inv_abst1 … HY) -HY #W2 #T2 #HW12 #HT12 #H destruct - lapply (IHTU1 L2 ? (ⓛW1.T1) ?) // #H - elim (nta_fwd_correct … H) -H #X #H - elim (nta_inv_bind1 … H) -H #W #U #HW #HU #_ - @(nta_conv … (ⓐV2.ⓛW1.U1)) /4 width=2/ (**) (* explicit constructor, /5 width=5/ is too slow *) - | #V2 #W2 #T0 #T2 #HV12 #HT02 #H1 #H2 destruct - lapply (IHVW1 … HL12 … HV12) #HVW2 - lapply (IHVW1 … HL12 V1 ?) -IHVW1 // #HV1W2 - lapply (IHTU1 … HL12 (ⓛW2.T2) ?) -IHTU1 -HL12 /2 width=1/ -HT02 #H1 - elim (nta_fwd_correct … H1) #T #H2 - elim (nta_inv_bind1 … H1) -H1 #W #U2 #HW2 #HTU2 #H - elim (cpcs_inv_abst … H Abst W2) -H #_ #HU21 - elim (nta_inv_bind1 … H2) -H2 #W0 #U0 #_ #H #_ -T -W0 - lapply (lsubn_nta_trans … HTU2 (L2.ⓓV2) ?) -HTU2 /2 width=1/ #HTU2 - @(nta_conv … (ⓓV2.U2)) /2 width=2/ /3 width=2/ (**) (* explicit constructor, /4 width=5/ is too slow *) - | #V0 #V2 #W0 #W2 #T0 #T2 #_ #_ #_ #_ #H destruct - ] -| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHTU1 #IHUW1 #L2 #HL12 #X #H - elim (tpr_inv_appl1 … H) -H * - [ #V2 #T2 #HV12 #HT12 #H destruct - elim (nta_fwd_correct h L2 (ⓐV1.T1) (ⓐV1.U1) ?) [2: /3 width=2/ ] #U - @(nta_conv … (ⓐV2.U1)) /2 width=1/ /4 width=2/ (**) (* explicit constructor, /5 width=5/ is too slow *) - | #V2 #W2 #T0 #T2 #HV12 #HT02 #H1 #H2 destruct - lapply (IHTU1 … HL12 (ⓛW2.T2) ?) -IHTU1 /2 width=1/ -T0 #H - elim (nta_inv_bind1 … H) -H #W #U2 #HW2 #HTU2 #HU21 - lapply (IHUW1 … HL12 (ⓐV2.U1) ?) -IHUW1 -HL12 /2 width=1/ #H - elim (nta_inv_pure1 … H) -H #V0 #U0 #U #HV20 #HU10 #HU0W1 #HU0 - @(nta_conv … (ⓓV2.U2)) - [2: @nta_bind // - @(lsubn_nta_trans … HTU2) @lsubn_abbr // -(* - lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HB - lapply (IH … HB0 … HL12 W2 ?) -HB0 /width=5/ #HB0 - lapply (IH … HA0 … (L2.ⓛW2) … HT02) -IH -HA0 -HT02 /width=5/ -T0 /2 width=1/ -L1 -V1 /4 width=7/ -*) -*) -(* -axiom pippo: ⦃h, L⦄ ⊢ ⓐV.X : Y → - ∃∃W,T. L ⊢ X ➡* ⓛW.T & ⦃h, L⦄ ⊢ ⓐV : W. - -*) -(* SEGMENT 2 -| #L1 #T1 #U1 #W1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL12 #X #H - elim (tpss_inv_flat1 … H) -H #U2 #T2 #HU12 #HT12 #H destruct - lapply (cpr_tpss … HU12) /4 width=4/ -| #L1 #T1 #U11 #U12 #U #_ #HU112 #_ #IHTU11 #IHU12 #L2 #d #e #HL12 #T2 #HT12 - @(nta_conv … U11) /2 width=5/ (**) (* explicot constructor, /3 width=7/ is too slow *) -] -qed. -*) - -(* SEGMENT 3 -fact nta_ltpr_tpr_conf_aux: ∀h,L,T,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → L = L1 → T = T1 → - ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → ⦃h, L2⦄ ⊢ T2 : U. - - - | #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HW02 #HT02 #HV02 #H1 #H2 destruct - elim (nta_inv_abbr … HT1) -HT1 #B0 #HW0 #HT0 - lapply (IH … HW0 … HL12 … HW02) -HW0 /width=5/ #HW2 - lapply (IH … HV1 … HL12 … HV10) -HV1 -HV10 /width=5/ #HV0 - lapply (IH … HT0 … (L2.ⓓW2) … HT02) -IH -HT0 -HT02 /width=5/ -V1 -T0 /2 width=1/ -L1 -W0 #HT2 - @(nta_abbr … HW2) -HW2 - @(nta_appl … HT2) -HT2 /3 width=7/ (**) (* explict constructors, /5 width=7/ is too slow *) - ] -| #L1 #V1 #T1 #A #HV1 #HT1 #H1 #H2 #L2 #HL12 #X #H destruct - elim (tpr_inv_cast1 … H) -H - [ * #V2 #T2 #HV12 #HT12 #H destruct - lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HV2 - lapply (IH … HT1 … HL12 … HT12) -IH -HT1 -HL12 -HT12 /width=5/ -L1 -V1 -T1 /2 width=1/ - | -HV1 #HT1X - lapply (IH … HT1 … HL12 … HT1X) -IH -HT1 -HL12 -HT1X /width=5/ - ] -] -qed. - -/2 width=9/ qed. - -axiom nta_ltpr_conf: ∀L1,T,A. L1 ⊢ T : A → ∀L2. L1 ➡ L2 → L2 ⊢ T : A. -/2 width=5/ qed. - -axiom nta_tpr_conf: ∀L,T1,A. L ⊢ T1 : A → ∀T2. T1 ➡ T2 → L ⊢ T2 : A. -/2 width=5/ qed. -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_2A1/snv_preserve.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_2A1/snv/snv_preserve.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_2A1/snv_preserve.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc_2A1/snv/snv_preserve.etc 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 f02240094..cb69bdfb9 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 @@ -20,7 +20,7 @@ table { class "magenta" [ { "dynamic typing" * } { [ { "context-sensitive native type assignment" * } { - [ [ "for terms" ] "nta" + "( ⦃?,?⦄ ⊢ ? :[?,?] ? )" + "( ⦃?,?⦄ ⊢ ? :[?] ? )" + "( ⦃?,?⦄ ⊢ ? :*[?] ? )" "nta_drops" + "nta_cpms" + "nta_cpcs" + "nta_preserve" + "nta_ind" * ] + [ [ "for terms" ] "nta" + "( ⦃?,?⦄ ⊢ ? :[?,?] ? )" + "( ⦃?,?⦄ ⊢ ? :[?] ? )" + "( ⦃?,?⦄ ⊢ ? :*[?] ? )" "nta_drops" + "nta_aaa" + "nta_fsb" + "nta_cpms" + "nta_cpcs" + "nta_preserve" + "nta_preserve_cpcs" + "nta_ind" * ] } ] [ { "context-sensitive native validity" * } { -- 2.39.2