From c3832abc23bb0907df2deb6751f4a46d213675b7 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 30 Mar 2017 11:30:39 +0000 Subject: [PATCH] - csx_cnx_vector.ma completed - refactoring --- .../basic_2/rt_computation/cpxs_etc.ma | 19 ------ .../lambdadelta/basic_2/rt_computation/csx.ma | 13 ---- .../basic_2/rt_computation/csx_cnx.ma | 13 ++++ .../basic_2/rt_computation/csx_cnx_vector.ma | 56 ++++++++++++++++++ .../basic_2/rt_computation/csx_lfpx.ma | 5 +- .../{csx_theq.ma => csx_simple_theq.ma} | 0 .../basic_2/rt_computation/csx_theq_vector.ma | 59 ++++++------------- .../basic_2/rt_computation/partial.txt | 4 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 4 +- 9 files changed, 95 insertions(+), 78 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma rename matita/matita/contribs/lambdadelta/basic_2/rt_computation/{csx_theq.ma => csx_simple_theq.ma} (100%) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_etc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_etc.ma index a28b01e54..0340000b9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_etc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_etc.ma @@ -5,21 +5,6 @@ include "basic_2/rt_computation/cpxs_cpxs.ma". (* Properties on sn extended parallel reduction for local environments ******) -lemma lpx_cpx_trans: ∀h,G. b_c_transitive … (cpx h G) (λ_.lpx h G). -#h #G #L2 #T1 #T2 #HT12 elim HT12 -G -L2 -T1 -T2 -[ /2 width=3 by/ -| /3 width=2 by cpx_cpxs, cpx_st/ -| #I #G #L2 #K2 #V0 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV02 #L1 #HL12 - elim (lpx_drop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H - elim (lpx_inv_pair2 … H) -H #K1 #V1 #HK12 #HV10 #H destruct - /4 width=7 by cpxs_delta, cpxs_strap2/ -|4,9: /4 width=1 by cpxs_beta, cpxs_bind, lpx_pair/ -|5,7,8: /3 width=1 by cpxs_flat, cpxs_ct, cpxs_eps/ -| /4 width=3 by cpxs_zeta, lpx_pair/ -| /4 width=3 by cpxs_theta, cpxs_strap1, lpx_pair/ -] -qed-. - lemma cpx_bind2: ∀h,o,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈[h, o] V2 → ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ⬈[h, o] T2 → ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ⬈*[h, o] ⓑ{a,I}V2.T2. @@ -27,10 +12,6 @@ lemma cpx_bind2: ∀h,o,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈[h, o] V2 → (* Advanced properties ******************************************************) -lemma lpx_cpxs_trans: ∀h,o,G. b_rs_transitive … (cpx h o G) (λ_.lpx h o G). -#h #o #G @b_c_trans_LTC1 /2 width=3 by lpx_cpx_trans/ (**) (* full auto fails *) -qed-. - lemma cpxs_bind2_dx: ∀h,o,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈[h, o] V2 → ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ⬈*[h, o] T2 → ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ⬈*[h, o] ⓑ{a,I}V2.T2. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma index 5fe697558..c7e8e3dd3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma @@ -45,19 +45,6 @@ lemma csx_intro: ∀h,o,G,L,T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄. /4 width=1 by SN_intro/ qed. -lemma csx_sort: ∀h,o,G,L,s. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃⋆s⦄. -#h #o #G #L #s elim (deg_total h o s) -#d generalize in match s; -s elim d -d -[ #s1 #Hs1 @csx_intro #X #H #HX elim HX -HX - elim (cpx_inv_sort1 … H) -H #H destruct // - /3 width=3 by tdeq_sort, deg_next/ -| #d #IH #s #Hsd lapply (deg_next_SO … Hsd) -Hsd - #Hsd @csx_intro #X #H #HX - elim (cpx_inv_sort1 … H) -H #H destruct /2 width=1 by/ - elim HX // -] -qed. - (* Basic forward lemmas *****************************************************) fact csx_fwd_pair_sn_aux: ∀h,o,G,L,U. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃U⦄ → diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx.ma index 8f9268fab..ea34597b9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx.ma @@ -22,3 +22,16 @@ include "basic_2/rt_computation/csx.ma". (* Basic_1: was just: sn3_nf2 *) lemma cnx_csx: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄. /2 width=1 by NF_to_SN/ qed. + +(* Advanced properties ******************************************************) + +lemma csx_sort: ∀h,o,G,L,s. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃⋆s⦄. +#h #o #G #L #s elim (deg_total h o s) +#d generalize in match s; -s elim d -d +[ /3 width=3 by cnx_csx, cnx_sort/ +| #d #IH #s #Hsd lapply (deg_next_SO … Hsd) -Hsd + #Hsd @csx_intro #X #H #HX + elim (cpx_inv_sort1 … H) -H #H destruct /2 width=1 by/ + elim HX -HX // +] +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma new file mode 100644 index 000000000..ef3d1c20b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.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 *) +(* *) +(**************************************************************************) + +(* STRONGLY NORMALIZING TERM VECTORS FOR UNCOUNTED PARALLEL RT-TRANSITION ***) + +include "basic_2/rt_computation/cpxs_theq_vector.ma". +include "basic_2/rt_computation/csx_simple_theq.ma". +include "basic_2/rt_computation/csx_cnx.ma". +include "basic_2/rt_computation/csx_cpxs.ma". +include "basic_2/rt_computation/csx_vector.ma". + +(* Properties with normal terms for uncounted parallel rt-transition ********) + +(* Basic_1: was just: sn3_appls_lref *) +lemma csx_applv_cnx: ∀h,o,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T⦄ → + ∀Vs. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃Vs⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⒶVs.T⦄. +#h #o #G #L #T #H1T #H2T #Vs elim Vs -Vs +[ #_ normalize in ⊢ (?????%); /2 width=1/ +| #V #Vs #IHV #H + elim (csxv_inv_cons … H) -H #HV #HVs + @csx_appl_simple_theq /2 width=1 by applv_simple/ -IHV -HV -HVs + #X #H #H0 + lapply (cpxs_fwd_cnx_vector … o … H) -H // -H1T -H2T #H + elim (H0) -H0 // +] +qed. + +(* Advanced properties ******************************************************) + +lemma csx_applv_sort: ∀h,o,G,L,s,Vs. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃Vs⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⒶVs.⋆s⦄. +#h #o #G #L #s elim (deg_total h o s) +#d generalize in match s; -s elim d -d +[ /3 width=6 by csx_applv_cnx, cnx_sort, simple_atom/ +| #d #IHd #s #Hd #Vs elim Vs -Vs /2 width=1 by/ + #V #Vs #IHVs #HVVs + elim (csxv_inv_cons … HVVs) #HV #HVs + @csx_appl_simple_theq /2 width=1 by applv_simple, simple_atom/ + #X #H #H0 + elim (cpxs_fwd_sort_vector … o … H) -H #H + [ elim H0 -H0 // + | -H0 @(csx_cpxs_trans … (Ⓐ(V@Vs).⋆(next h s))) + /3 width=1 by cpxs_flat_dx, deg_next_SO/ + ] +] +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfpx.ma index 0c2f894b1..2cfbc1a3f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfpx.ma @@ -13,12 +13,11 @@ (**************************************************************************) include "basic_2/rt_computation/cpxs_lfpx.ma". -include "basic_2/rt_computation/csx_drops.ma". include "basic_2/rt_computation/csx_cpxs.ma". (* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********) -(* Advanced properties ******************************************************) +(* Properties with uncounted parallel rt-transition on referred entries *****) (* Basic_2A1: was just: csx_lpx_conf *) lemma csx_lfpx_conf: ∀h,o,G,L1,T. ⦃G, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → @@ -27,6 +26,8 @@ lemma csx_lfpx_conf: ∀h,o,G,L1,T. ⦃G, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → /5 width=3 by csx_intro, lfpx_cpx_trans, lfpx_cpxs_conf/ qed-. +(* Advanced properties ******************************************************) + lemma csx_abst: ∀h,o,p,G,L,W. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃W⦄ → ∀T. ⦃G, L.ⓛW⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓛ{p}W.T⦄. #h #o #p #G #L #W #HW @(csx_ind … HW) -W diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_theq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_theq.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_theq.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_theq.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_theq_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_theq_vector.ma index 2c8dda2dc..55146e3c2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_theq_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_theq_vector.ma @@ -11,46 +11,25 @@ (* v GNU General Public License Version 2 *) (* *) (**************************************************************************) - +(* include "basic_2/computation/gcp_cr.ma". -include "basic_2/computation/cpxs_theq_vector.ma". -include "basic_2/computation/csx_lpx.ma". -include "basic_2/computation/csx_vector.ma". - -(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERM VECTORS *************) +*) +include "basic_2/rt_computation/cpxs_theq_vector.ma". +include "basic_2/rt_computation/csx_vector.ma". +include "basic_2/rt_computation/csx_theq.ma". +include "basic_2/rt_computation/csx_lfpx.ma". -(* Advanced properties ******************************************************) - -(* Basic_1: was just: sn3_appls_lref *) -lemma csx_applv_cnx: ∀h,o,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃T⦄ → - ∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, o] Vs → ⦃G, L⦄ ⊢ ⬊*[h, o] ⒶVs.T. -#h #o #G #L #T #H1T #H2T #Vs elim Vs -Vs [ #_ @(cnx_csx … H2T) ] (**) (* /2 width=1/ does not work *) -#V #Vs #IHV #H -elim (csxv_inv_cons … H) -H #HV #HVs -@csx_appl_simple_theq /2 width=1 by applv_simple/ -IHV -HV -HVs -#X #H #H0 -lapply (cpxs_fwd_cnx_vector … H) -H // -H1T -H2T #H -elim (H0) -H0 // -qed. +(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********) -lemma csx_applv_sort: ∀h,o,G,L,s,Vs. ⦃G, L⦄ ⊢ ⬊*[h, o] Vs → ⦃G, L⦄ ⊢ ⬊*[h, o] ⒶVs.⋆s. -#h #o #G #L #s elim (deg_total h o s) -#d generalize in match s; -s @(nat_ind_plus … d) -d [ /3 width=6 by csx_applv_cnx, cnx_sort, simple_atom/ ] -#d #IHd #s #Hkd lapply (deg_next_SO … Hkd) -Hkd -#Hkd #Vs elim Vs -Vs /2 width=1 by/ -#V #Vs #IHVs #HVVs -elim (csxv_inv_cons … HVVs) #HV #HVs -@csx_appl_simple_theq /2 width=1 by applv_simple, simple_atom/ -IHVs -HV -HVs -#X #H #H0 -elim (cpxs_fwd_sort_vector … H) -H #H -[ elim H0 -H0 // -| -H0 @(csx_cpxs_trans … (Ⓐ(V@Vs).⋆(next h s))) /2 width=1 by cpxs_flat_dx/ -] -qed. +(* Vector form of properties with head equivalence for terms ****************) +(* +*) +(* +*) (* Basic_1: was just: sn3_appls_beta *) -lemma csx_applv_beta: ∀h,o,a,G,L,Vs,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, o] ⒶVs.ⓓ{a}ⓝW.V.T → - ⦃G, L⦄ ⊢ ⬊*[h, o] ⒶVs. ⓐV.ⓛ{a}W.T. +lemma csx_applv_beta: ∀h,o,p,G,L,Vs,V,W,T. ⦃G, L⦄ ⊢ ⬈*[h, o] ⒶVs.ⓓ{p}ⓝW.V.T → + ⦃G, L⦄ ⊢ ⬈*[h, o] ⒶVs. ⓐV.ⓛ{p}W.T. #h #o #a #G #L #Vs elim Vs -Vs /2 width=1 by csx_appl_beta/ #V0 #Vs #IHV #V #W #T #H1T lapply (csx_fwd_pair_sn … H1T) #HV0 @@ -65,7 +44,7 @@ qed. lemma csx_applv_delta: ∀h,o,I,G,L,K,V1,i. ⬇[i] L ≡ K.ⓑ{I}V1 → ∀V2. ⬆[0, i + 1] V1 ≡ V2 → - ∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, o] (ⒶVs.V2) → ⦃G, L⦄ ⊢ ⬊*[h, o] (ⒶVs.#i). + ∀Vs. ⦃G, L⦄ ⊢ ⬈*[h, o] (ⒶVs.V2) → ⦃G, L⦄ ⊢ ⬈*[h, o] (ⒶVs.#i). #h #o #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs [ /4 width=12 by csx_inv_lift, csx_lref_bind, drop_fwd_drop2/ | #V #Vs #IHV #H1T @@ -82,8 +61,8 @@ qed. (* Basic_1: was just: sn3_appls_abbr *) lemma csx_applv_theta: ∀h,o,a,G,L,V1b,V2b. ⬆[0, 1] V1b ≡ V2b → - ∀V,T. ⦃G, L⦄ ⊢ ⬊*[h, o] ⓓ{a}V.ⒶV2b.T → - ⦃G, L⦄ ⊢ ⬊*[h, o] ⒶV1b.ⓓ{a}V.T. + ∀V,T. ⦃G, L⦄ ⊢ ⬈*[h, o] ⓓ{a}V.ⒶV2b.T → + ⦃G, L⦄ ⊢ ⬈*[h, o] ⒶV1b.ⓓ{a}V.T. #h #o #a #G #L #V1b #V2b * -V1b -V2b /2 width=1 by/ #V1b #V2b #V1 #V2 #HV12 #H generalize in match HV12; -HV12 generalize in match V2; -V2 generalize in match V1; -V1 @@ -100,8 +79,8 @@ elim (cpxs_fwd_theta_vector … (V2@V2b) … H1) -H1 /2 width=1 by liftv_cons/ - qed. (* Basic_1: was just: sn3_appls_cast *) -lemma csx_applv_cast: ∀h,o,G,L,Vs,W,T. ⦃G, L⦄ ⊢ ⬊*[h, o] ⒶVs.W → ⦃G, L⦄ ⊢ ⬊*[h, o] ⒶVs.T → - ⦃G, L⦄ ⊢ ⬊*[h, o] ⒶVs.ⓝW.T. +lemma csx_applv_cast: ∀h,o,G,L,Vs,W,T. ⦃G, L⦄ ⊢ ⬈*[h, o] ⒶVs.W → ⦃G, L⦄ ⊢ ⬈*[h, o] ⒶVs.T → + ⦃G, L⦄ ⊢ ⬈*[h, o] ⒶVs.ⓝW.T. #h #o #G #L #Vs elim Vs -Vs /2 width=1 by csx_cast/ #V #Vs #IHV #W #T #H1W #H1T lapply (csx_fwd_pair_sn … H1W) #HV diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt index 5fa047a73..6c76c4bc8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -1,4 +1,4 @@ cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_lsubr.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma lfpxs.ma lfpxs_fqup.ma lfpxs_cpxs.ma -csx.ma csx_simple.ma csx_theq.ma csx_drops.ma csx_lsubr.ma csx_gcp.ma csx_lfpx.ma csx_cnx.ma csx_cpxs.ma csx_csx.ma -csx_vector.ma +csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_lsubr.ma csx_gcp.ma csx_lfpx.ma csx_cnx.ma csx_cpxs.ma csx_csx.ma +csx_vector.ma csx_cnx_vector.ma 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 8dafdbd32..d2d7a0e35 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 @@ -113,8 +113,8 @@ table { [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_drop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ] [ "cpxs_lreq" + "cpxs_lleq" + "cpxs_aaa" * ] *) - [ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" * ] - [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_theq" + "csx_drops" + "csx_lsubr" + "csx_gcp" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_csx" * ] + [ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" * ] + [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_gcp" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_csx" * ] [ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_fqup" + "lfpxs_cpxs" * ] [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_lsubr" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ] } -- 2.39.2