From 5431da8145e4a84596d312fc02b552881d119100 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 1 Oct 2018 18:10:23 +0200 Subject: [PATCH] update in basic_2 + nta_drops completed --- .../lambdadelta/basic_2/dynamic/nta.ma | 48 ------- .../lambdadelta/basic_2/dynamic/nta_drops.ma | 125 ++++++++++-------- .../lambdadelta/basic_2/dynamic/nta_etc.ma | 57 ++++++++ .../lambdadelta/basic_2/etc/nta/nta.etc | 4 + .../lambdadelta/basic_2/web/basic_2_src.tbl | 2 +- 5 files changed, 129 insertions(+), 107 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_etc.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma index 8f6e4c6be..194211191 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma @@ -81,54 +81,6 @@ lemma nta_fwd_cnv_dx (a) (h) (G) (L): 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 *) 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 d8184be86..046b87460 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_drops.ma @@ -11,72 +11,81 @@ (* v GNU General Public License Version 2 *) (* *) (**************************************************************************) -(* -include "basic_2/dynamic/nta_alt.ma". -(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************) +include "basic_2/dynamic/cnv_drops.ma". +include "basic_2/dynamic/nta.ma". -(* Advanced inversion lemmas ************************************************) +(* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************) -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 - ) ∨ - (∃∃K,W,V,U0. ⇩[0, j] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W : V & - ⇧[0, j + 1] W ≡ U0 & L ⊢ U0 ⬌* U - ). -#h #L #T #U #H elim H -L -T -U -[ #L #k #j #H destruct -| #L #K #V #W #U #i #HLK #HVW #HWU #_ #j #H destruct /3 width=8/ -| #L #K #W #V #U #i #HLK #HWV #HWU #_ #j #H destruct /3 width=8/ -| #I #L #V #W #T #U #_ #_ #_ #_ #j #H destruct -| #L #V #W #T #U #_ #_ #_ #_ #j #H destruct -| #L #V #W #T #U #_ #_ #_ #_ #j #H destruct -| #L #T #U #_ #_ #j #H destruct -| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #j #H destruct - elim (IHTU1 ??) -IHTU1 [4: // |2: skip ] * #K #V #W #U0 #HLK #HVW #HWU0 #HU01 - lapply (cpcs_trans … HU01 … HU12) -U1 /3 width=8/ -] -qed. +(* Advanced properties ******************************************************) -(* Basic_1: was ty3_gen_lref *) -lemma nta_inv_lref1: ∀h,L,U,i. ⦃h, L⦄ ⊢ #i : U → - (∃∃K,V,W,U0. ⇩[0, i] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V : W & - ⇧[0, i + 1] W ≡ U0 & L ⊢ U0 ⬌* U - ) ∨ - (∃∃K,W,V,U0. ⇩[0, i] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W : V & - ⇧[0, i + 1] W ≡ U0 & L ⊢ U0 ⬌* U - ). -/2 width=3/ qed-. +lemma nta_ldef (a) (h) (G) (K): + ∀V,W. ⦃G,K⦄ ⊢ V :[a,h] W → + ∀U. ⬆*[1] W ≘ U → ⦃G,K.ⓓV⦄ ⊢ #0 :[a,h] U. +#a #h #G #K #V #W #H #U #HWU +elim (cnv_inv_cast … H) -H #X #HW #HV #HWX #HVX +lapply (cnv_lifts … HW (Ⓣ) … (K.ⓓV) … HWU) -HW +[ /3 width=3 by drops_refl, drops_drop/ ] #HU +elim (cpms_lifts_sn … HWX … (Ⓣ) … (K.ⓓV) … HWU) -W +[| /3 width=3 by drops_refl, drops_drop/ ] #XW #HXW #HUXW +/3 width=5 by cnv_zero, cnv_cast, cpms_delta/ +qed. -(* Advanced forvard lemmas **************************************************) +lemma nta_ldec_cnv (a) (h) (G) (K): + ∀W. ⦃G,K⦄ ⊢ W ![a,h] → + ∀U. ⬆*[1] W ≘ U → ⦃G,K.ⓛW⦄ ⊢ #0 :[a,h] U. +#a #h #G #K #W #HW #U #HWU +lapply (cnv_lifts … HW (Ⓣ) … (K.ⓛW) … HWU) +/3 width=5 by cnv_zero, cnv_cast, cpms_ell, drops_refl, drops_drop/ +qed. -fact nta_fwd_pure1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. T = ⓐY.X → - ∃∃V,W. ⦃h, L⦄ ⊢ Y : W & ⦃h, L⦄ ⊢ X : V & L ⊢ ⓐY.V ⬌* 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 #HVW #HTU #_ #_ #X #Y #H destruct /2 width=3/ -| #L #V #W #T #U #HTU #_ #_ #IHUW #X #Y #H destruct - elim (IHUW U Y ?) -IHUW // /2 width=3/ -| #L #T #U #_ #_ #X #Y #H destruct -| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #X #Y #H destruct - elim (IHTU1 ???) -IHTU1 [4: // |2,3: skip ] #V #W #HYW #HXV #HU1 - lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=3/ -] +lemma nta_lref (a) (h) (I) (G) (K): + ∀T,i. ⦃G,K⦄ ⊢ #i :[a,h] T → + ∀U. ⬆*[1] T ≘ U → ⦃G,K.ⓘ{I}⦄ ⊢ #(↑i) :[a,h] U. +#a #h #I #G #K #T #i #H #U #HTU +elim (cnv_inv_cast … H) -H #X #HT #Hi #HTX #H2 +lapply (cnv_lifts … HT (Ⓣ) … (K.ⓘ{I}) … HTU) -HT +[ /3 width=3 by drops_refl, drops_drop/ ] #HU +lapply (cnv_lifts … Hi (Ⓣ) (𝐔❴1❵) (K.ⓘ{I}) ???) -Hi +[4:|*: /3 width=3 by drops_refl, drops_drop/ ] #Hi +elim (cpms_lifts_sn … HTX … (Ⓣ) … (K.ⓘ{I}) … HTU) -T +[| /3 width=3 by drops_refl, drops_drop/ ] #XU #HXU #HUXU +/3 width=5 by cnv_cast, cpms_lref/ qed. -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-. +(* Properties with generic slicing for local environments *******************) -(* Properties on relocation *************************************************) +lemma nta_lifts_sn (a) (h) (G): d_liftable2_sn … lifts (nta a h G). +#a #h #G #K #T1 #T2 #H #b #f #L #HLK #U1 #HTU1 +elim (cnv_inv_cast … H) -H #X #HT2 #HT1 #HT2X #HT1X +elim (lifts_total T2 f) #U2 #HTU2 +lapply (cnv_lifts … HT2 … HLK … HTU2) -HT2 #HU2 +lapply (cnv_lifts … HT1 … HLK … HTU1) -HT1 #HU1 +elim (cpms_lifts_sn … HT2X … HLK … HTU2) -HT2X #X2 #HX2 #HUX2 +elim (cpms_lifts_sn … HT1X … HLK … HTU1) -T1 #X1 #HX1 #HUX1 +lapply (lifts_mono … HX2 … HX1) -K -X #H destruct +/3 width=6 by cnv_cast, ex2_intro/ +qed-. (* 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. -*) +(* Basic_2A1: was: nta_lift ntaa_lift *) +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 *) +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. +#a #h #G #K #L #i #V #W #HVW #U #HWU #HLK +elim (lifts_split_trans … HWU (𝐔❴1❵) (𝐔❴i❵)) [| // ] #X #HWX #HXU +/3 width=9 by nta_lifts_bi, nta_ldef/ +qed. + +lemma nta_ldec_drops_cnv (a) (h) (G) (K) (L) (i): + ∀W. ⦃G,K⦄ ⊢ W ![a,h] → + ∀U. ⬆*[↑i] W ≘ U → ⬇*[i] L ≘ K.ⓛW → ⦃G,L⦄ ⊢ #i :[a,h] U. +#a #h #G #K #L #i #W #HW #U #HWU #HLK +elim (lifts_split_trans … HWU (𝐔❴1❵) (𝐔❴i❵)) [| // ] #X #HWX #HXU +/3 width=9 by nta_lifts_bi, nta_ldec_cnv/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_etc.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_etc.ma new file mode 100644 index 000000000..0701dcf8b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_etc.ma @@ -0,0 +1,57 @@ +(* +(* Advanced inversion lemmas ************************************************) + + +(* Basic_1: was ty3_gen_lref *) +lemma nta_inv_lref1: ∀h,L,U,i. ⦃h, L⦄ ⊢ #i : U → + (∃∃K,V,W,U0. ⇩[0, i] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V : W & + ⇧[0, i + 1] W ≡ U0 & L ⊢ U0 ⬌* U + ) ∨ + (∃∃K,W,V,U0. ⇩[0, i] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W : V & + ⇧[0, i + 1] W ≡ U0 & L ⊢ U0 ⬌* U + ). +/2 width=3/ qed-. + +(* Advanced forvard lemmas **************************************************) + +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-. + +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-. + +*) 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 db33815a7..43364f208 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta.etc @@ -9,6 +9,10 @@ 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 + (* 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/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index 6126c2f68..1ada2adc1 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_cpms" + "nta_cpcs" + "nta_preserve" * ] + [ [ "for terms" ] "nta" + "( ⦃?,?⦄ ⊢ ? :[?,?] ? )" + "( ⦃?,?⦄ ⊢ ? :[?] ? )" + "( ⦃?,?⦄ ⊢ ? :*[?] ? )" "nta_drops" + "nta_cpms" + "nta_cpcs" + "nta_preserve" * ] } ] [ { "context-sensitive native validity" * } { -- 2.39.2