From fca909e9e53de73771e1b47e94434ae8f747d7fb Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 10 Aug 2014 18:41:31 +0000 Subject: [PATCH] some renaming and a minor addition --- .../{cpxs_tstc.ma => cpxs_tsts.ma} | 12 ++-- ...pxs_tstc_vector.ma => cpxs_tsts_vector.ma} | 42 +++++++------- .../basic_2/computation/csx_aaa.ma | 6 +- .../basic_2/computation/csx_lift.ma | 6 +- .../basic_2/computation/csx_lpx.ma | 8 +-- ...{csx_tstc_vector.ma => csx_tsts_vector.ma} | 20 +++---- .../basic_2/computation/{acp.ma => gcp.ma} | 8 +-- .../computation/{acp_aaa.ma => gcp_aaa.ma} | 36 ++++++------ .../computation/{acp_cr.ma => gcp_cr.ma} | 50 ++++++++--------- .../lambdadelta/basic_2/computation/lsubc.ma | 13 ++++- .../basic_2/computation/lsubc_drop.ma | 8 +-- .../basic_2/computation/lsubc_drops.ma | 8 +-- .../basic_2/computation/lsubc_lsuba.ma | 8 +-- .../basic_2/grammar/{tstc.ma => tsts.ma} | 56 +++++++++---------- .../grammar/{tstc_tstc.ma => tsts_tsts.ma} | 16 +++--- .../{tstc_vector.ma => tsts_vector.ma} | 8 +-- .../lambdadelta/basic_2/multiple/drops.ma | 2 +- .../lambdadelta/basic_2/multiple/lifts.ma | 2 +- .../basic_2/multiple/lifts_lift.ma | 2 +- .../basic_2/multiple/{gr2.ma => mr2.ma} | 4 +- .../multiple/{gr2_minus.ma => mr2_minus.ma} | 6 +- .../multiple/{gr2_gr2.ma => mr2_mr2.ma} | 4 +- .../multiple/{gr2_plus.ma => mr2_plus.ma} | 6 +- .../lambdadelta/basic_2/web/basic_2.ldw.xml | 4 ++ .../lambdadelta/basic_2/web/basic_2_src.tbl | 18 +++--- 25 files changed, 182 insertions(+), 171 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/computation/{cpxs_tstc.ma => cpxs_tsts.ma} (93%) rename matita/matita/contribs/lambdadelta/basic_2/computation/{cpxs_tstc_vector.ma => cpxs_tsts_vector.ma} (87%) rename matita/matita/contribs/lambdadelta/basic_2/computation/{csx_tstc_vector.ma => csx_tsts_vector.ma} (90%) rename matita/matita/contribs/lambdadelta/basic_2/computation/{acp.ma => gcp.ma} (90%) rename matita/matita/contribs/lambdadelta/basic_2/computation/{acp_aaa.ma => gcp_aaa.ma} (79%) rename matita/matita/contribs/lambdadelta/basic_2/computation/{acp_cr.ma => gcp_cr.ma} (84%) rename matita/matita/contribs/lambdadelta/basic_2/grammar/{tstc.ma => tsts.ma} (62%) rename matita/matita/contribs/lambdadelta/basic_2/grammar/{tstc_tstc.ma => tsts_tsts.ma} (74%) rename matita/matita/contribs/lambdadelta/basic_2/grammar/{tstc_vector.ma => tsts_vector.ma} (87%) rename matita/matita/contribs/lambdadelta/basic_2/multiple/{gr2.ma => mr2.ma} (96%) rename matita/matita/contribs/lambdadelta/basic_2/multiple/{gr2_minus.ma => mr2_minus.ma} (95%) rename matita/matita/contribs/lambdadelta/basic_2/multiple/{gr2_gr2.ma => mr2_mr2.ma} (93%) rename matita/matita/contribs/lambdadelta/basic_2/multiple/{gr2_plus.ma => mr2_plus.ma} (91%) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tsts.ma similarity index 93% rename from matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tsts.ma index c3125bedb..b1d0f1116 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tsts.ma @@ -12,12 +12,12 @@ (* *) (**************************************************************************) -include "basic_2/grammar/tstc.ma". +include "basic_2/grammar/tsts.ma". include "basic_2/computation/lpxs_cpxs.ma". (* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************) -(* Forward lemmas involving same top term constructor ***********************) +(* Forward lemmas involving same top term structure *************************) lemma cpxs_fwd_cnx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ∀U. ⦃G, L⦄ ⊢ T ➡*[h, g] U → T ≂ U. #h #g #G #L #T #HT #U #H @@ -32,7 +32,7 @@ elim (cpxs_inv_sort1 … H) -H #n #l generalize in match k; -k @(nat_ind_plus | #n #IHn #k >plus_plus_comm_23 #Hnl #H destruct lapply (deg_next_SO … Hnl) -Hnl #Hnl elim (IHn … Hnl) -IHn - [ #H lapply (tstc_inv_atom1 … H) -H #H >H -H /2 width=1 by or_intror/ + [ #H lapply (tsts_inv_atom1 … H) -H #H >H -H /2 width=1 by or_intror/ | generalize in match Hnl; -Hnl @(nat_ind_plus … n) -n /4 width=3 by cpxs_strap2, cpx_st, or_intror/ | >iter_SO >iter_n_Sm // @@ -45,7 +45,7 @@ lemma cpxs_fwd_beta: ∀h,g,a,G,L,V,W,T,U. ⦃G, L⦄ ⊢ ⓐV.ⓛ{a}W.T ➡*[h, ⓐV.ⓛ{a}W.T ≂ U ∨ ⦃G, L⦄ ⊢ ⓓ{a}ⓝW.V.T ➡*[h, g] U. #h #g #a #G #L #V #W #T #U #H elim (cpxs_inv_appl1 … H) -H * -[ #V0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair, or_introl/ +[ #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/ | #b #W0 #T0 #HT0 #HU elim (cpxs_inv_abst1 … HT0) -HT0 #W1 #T1 #HW1 #HT1 #H destruct lapply (lsubr_cpxs_trans … HT1 (L.ⓓⓝW.V) ?) -HT1 @@ -72,7 +72,7 @@ lemma cpxs_fwd_theta: ∀h,g,a,G,L,V1,V,T,U. ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}V.T ➡* ⦃G, L⦄ ⊢ ⓓ{a}V.ⓐV2.T ➡*[h, g] U. #h #g #a #G #L #V1 #V #T #U #H #V2 #HV12 elim (cpxs_inv_appl1 … H) -H * -[ -HV12 #V0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair, or_introl/ +[ -HV12 #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/ | #b #W #T0 #HT0 #HU elim (cpxs_inv_abbr1 … HT0) -HT0 * [ #V3 #T3 #_ #_ #H destruct @@ -103,5 +103,5 @@ lemma cpxs_fwd_cast: ∀h,g,G,L,W,T,U. ⦃G, L⦄ ⊢ ⓝW.T ➡*[h, g] U → ∨∨ ⓝW. T ≂ U | ⦃G, L⦄ ⊢ T ➡*[h, g] U | ⦃G, L⦄ ⊢ W ➡*[h, g] U. #h #g #G #L #W #T #U #H elim (cpxs_inv_cast1 … H) -H /2 width=1 by or3_intro1, or3_intro2/ * -#W0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair, or3_intro0/ +#W0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or3_intro0/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tsts_vector.ma similarity index 87% rename from matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tsts_vector.ma index becbd624d..bfbad281c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tsts_vector.ma @@ -12,13 +12,13 @@ (* *) (**************************************************************************) -include "basic_2/grammar/tstc_vector.ma". +include "basic_2/grammar/tsts_vector.ma". include "basic_2/substitution/lift_vector.ma". -include "basic_2/computation/cpxs_tstc.ma". +include "basic_2/computation/cpxs_tsts.ma". (* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************) -(* Vector form of forward lemmas involving same top term constructor ********) +(* Vector form of forward lemmas involving same top term structure **********) (* Basic_1: was just: nf2_iso_appls_lref *) lemma cpxs_fwd_cnx_vector: ∀h,g,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → @@ -26,13 +26,13 @@ lemma cpxs_fwd_cnx_vector: ∀h,g,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, #h #g #G #L #T #H1T #H2T #Vs elim Vs -Vs [ @(cpxs_fwd_cnx … H2T) ] (**) (* /2 width=3 by cpxs_fwd_cnx/ does not work *) #V #Vs #IHVs #U #H elim (cpxs_inv_appl1 … H) -H * -[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair/ +[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair/ | #a #W0 #T0 #HT0 #HU lapply (IHVs … HT0) -IHVs -HT0 #HT0 - elim (tstc_inv_bind_applv_simple … HT0) // + elim (tsts_inv_bind_applv_simple … HT0) // | #a #V1 #V2 #V0 #T0 #HV1 #HV12 #HT0 #HU lapply (IHVs … HT0) -IHVs -HT0 #HT0 - elim (tstc_inv_bind_applv_simple … HT0) // + elim (tsts_inv_bind_applv_simple … HT0) // ] qed-. @@ -41,17 +41,17 @@ lemma cpxs_fwd_sort_vector: ∀h,g,G,L,k,Vs,U. ⦃G, L⦄ ⊢ ⒶVs.⋆k ➡*[h, #h #g #G #L #k #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_sort/ #V #Vs #IHVs #U #H elim (cpxs_inv_appl1 … H) -H * -[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by tstc_pair, or_introl/ +[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/ | #a #W1 #T1 #HT1 #HU elim (IHVs … HT1) -IHVs -HT1 #HT1 - [ elim (tstc_inv_bind_applv_simple … HT1) // + [ elim (tsts_inv_bind_applv_simple … HT1) // | @or_intror (**) (* explicit constructor *) @(cpxs_trans … HU) -U @(cpxs_strap1 … (ⓐV.ⓛ{a}W1.T1)) /3 width=1 by cpxs_flat_dx, cpr_cpx, cpr_beta/ ] | #a #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU elim (IHVs … HT1) -IHVs -HT1 #HT1 - [ elim (tstc_inv_bind_applv_simple … HT1) // + [ elim (tsts_inv_bind_applv_simple … HT1) // | @or_intror (**) (* explicit constructor *) @(cpxs_trans … HU) -U @(cpxs_strap1 … (ⓐV1.ⓓ{a}V3.T1)) /3 width=3 by cpxs_flat, cpr_cpx, cpr_theta/ @@ -66,17 +66,17 @@ lemma cpxs_fwd_beta_vector: ∀h,g,a,G,L,Vs,V,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓐV. #h #g #a #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_beta/ #V0 #Vs #IHVs #V #W #T #U #H elim (cpxs_inv_appl1 … H) -H * -[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by tstc_pair, or_introl/ +[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/ | #b #W1 #T1 #HT1 #HU elim (IHVs … HT1) -IHVs -HT1 #HT1 - [ elim (tstc_inv_bind_applv_simple … HT1) // + [ elim (tsts_inv_bind_applv_simple … HT1) // | @or_intror (**) (* explicit constructor *) @(cpxs_trans … HU) -U @(cpxs_strap1 … (ⓐV0.ⓛ{b}W1.T1)) /3 width=1 by cpxs_flat_dx, cpr_cpx, cpr_beta/ ] | #b #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU elim (IHVs … HT1) -IHVs -HT1 #HT1 - [ elim (tstc_inv_bind_applv_simple … HT1) // + [ elim (tsts_inv_bind_applv_simple … HT1) // | @or_intror (**) (* explicit constructor *) @(cpxs_trans … HU) -U @(cpxs_strap1 … (ⓐV1.ⓓ{b}V3.T1)) /3 width=3 by cpxs_flat, cpr_cpx, cpr_theta/ @@ -91,17 +91,17 @@ lemma cpxs_fwd_delta_vector: ∀h,g,I,G,L,K,V1,i. ⇩[i] L ≡ K.ⓑ{I}V1 → #h #g #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs /2 width=5 by cpxs_fwd_delta/ #V #Vs #IHVs #U #H -K -V1 elim (cpxs_inv_appl1 … H) -H * -[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair, or_introl/ +[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/ | #b #W0 #T0 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0 - [ elim (tstc_inv_bind_applv_simple … HT0) // + [ elim (tsts_inv_bind_applv_simple … HT0) // | @or_intror -i (**) (* explicit constructor *) @(cpxs_trans … HU) -U @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) /3 width=1 by cpxs_flat_dx, cpr_cpx, cpr_beta/ ] | #b #V0 #V1 #V3 #T0 #HV0 #HV01 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0 - [ elim (tstc_inv_bind_applv_simple … HT0) // + [ elim (tsts_inv_bind_applv_simple … HT0) // | @or_intror -i (**) (* explicit constructor *) @(cpxs_trans … HU) -U @(cpxs_strap1 … (ⓐV0.ⓓ{b}V3.T0)) /3 width=3 by cpxs_flat, cpr_cpx, cpr_theta/ @@ -121,11 +121,11 @@ generalize in match V1a; -V1a elim HV12s -V1s -V2s /2 width=1 by cpxs_fwd_theta/ #V1s #V2s #V1b #V2b #HV12b #_ #IHV12s #V1a #V2a #HV12a #V #T #U #H elim (cpxs_inv_appl1 … H) -H * -[ -IHV12s -HV12a -HV12b #V0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair, or_introl/ +[ -IHV12s -HV12a -HV12b #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/ | #b #W0 #T0 #HT0 #HU elim (IHV12s … HV12b … HT0) -IHV12s -HT0 #HT0 [ -HV12a -HV12b -HU - elim (tstc_inv_pair1 … HT0) #V1 #T1 #H destruct + elim (tsts_inv_pair1 … HT0) #V1 #T1 #H destruct | @or_intror -V1s (**) (* explicit constructor *) @(cpxs_trans … HU) -U elim (cpxs_inv_abbr1 … HT0) -HT0 * @@ -140,7 +140,7 @@ elim (cpxs_inv_appl1 … H) -H * | #b #V0a #Va #V0 #T0 #HV10a #HV0a #HT0 #HU elim (IHV12s … HV12b … HT0) -HV12b -IHV12s -HT0 #HT0 [ -HV12a -HV10a -HV0a -HU - elim (tstc_inv_pair1 … HT0) #V1 #T1 #H destruct + elim (tsts_inv_pair1 … HT0) #V1 #T1 #H destruct | @or_intror -V1s -V1b (**) (* explicit constructor *) @(cpxs_trans … HU) -U elim (cpxs_inv_abbr1 … HT0) -HT0 * @@ -166,9 +166,9 @@ lemma cpxs_fwd_cast_vector: ∀h,g,G,L,Vs,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓝW.T ➡ #h #g #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_cast/ #V #Vs #IHVs #W #T #U #H elim (cpxs_inv_appl1 … H) -H * -[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair, or3_intro0/ +[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or3_intro0/ | #b #W0 #T0 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0 - [ elim (tstc_inv_bind_applv_simple … HT0) // + [ elim (tsts_inv_bind_applv_simple … HT0) // | @or3_intro1 -W (**) (* explicit constructor *) @(cpxs_trans … HU) -U @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) /2 width=1 by cpxs_flat_dx, cpx_beta/ @@ -178,7 +178,7 @@ elim (cpxs_inv_appl1 … H) -H * ] | #b #V0 #V1 #V2 #T0 #HV0 #HV01 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0 - [ elim (tstc_inv_bind_applv_simple … HT0) // + [ elim (tsts_inv_bind_applv_simple … HT0) // | @or3_intro1 -W (**) (* explicit constructor *) @(cpxs_trans … HU) -U @(cpxs_strap1 … (ⓐV0.ⓓ{b}V2.T0)) /2 width=3 by cpxs_flat, cpx_theta/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_aaa.ma index 0a42fb1f1..6d8aa3ed9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_aaa.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "basic_2/computation/acp_aaa.ma". +include "basic_2/computation/gcp_aaa.ma". include "basic_2/computation/cpxs_aaa.ma". -include "basic_2/computation/csx_tstc_vector.ma". +include "basic_2/computation/csx_tsts_vector.ma". (* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) @@ -22,7 +22,7 @@ include "basic_2/computation/csx_tstc_vector.ma". theorem aaa_csx: ∀h,g,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ ⬊*[h, g] T. #h #g #G #L #T #A #H -@(acp_aaa … (csx_acp h g) (csx_acr h g) … H) +@(gcr_aaa … (csx_gcp h g) (csx_gcr h g) … H) qed. (* Advanced eliminators *****************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma index f81114656..ade57bbd9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/reduction/cnx_lift.ma". -include "basic_2/computation/acp.ma". +include "basic_2/computation/gcp.ma". include "basic_2/computation/csx.ma". (* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) @@ -109,8 +109,8 @@ qed-. (* Main properties **********************************************************) -theorem csx_acp: ∀h,g. acp (cpx h g) (eq …) (csx h g). -#h #g @mk_acp +theorem csx_gcp: ∀h,g. gcp (cpx h g) (eq …) (csx h g). +#h #g @mk_gcp [ /3 width=13 by cnx_lift/ | #G #L elim (deg_total h g 0) /3 width=8 by cnx_sort_iter, ex_intro/ | /2 width=3 by csx_fwd_flat_dx/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma index 0f6cb8370..bd0ebff18 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/grammar/tstc_tstc.ma". +include "basic_2/grammar/tsts_tsts.ma". include "basic_2/computation/cpxs_cpxs.ma". include "basic_2/computation/csx_alt.ma". include "basic_2/computation/csx_lift.ma". @@ -118,7 +118,7 @@ lemma csx_appl_theta: ∀h,g,a,V1,V2. ⇧[0, 1] V1 ≡ V2 → /2 width=5 by csx_appl_theta_aux/ qed. (* Basic_1: was just: sn3_appl_appl *) -lemma csx_appl_simple_tstc: ∀h,g,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V → ∀T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 → +lemma csx_appl_simple_tsts: ∀h,g,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V → ∀T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 → (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 ≂ T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.T2) → 𝐒⦃T1⦄ → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.T1. #h #g #G #L #V #H @(csx_ind … H) -V #V #_ #IHV #T1 #H @(csx_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1 @@ -130,8 +130,8 @@ elim (eq_false_inv_tpair_sn … H) -H @(csx_cpx_trans … (ⓐV0.T1)) /2 width=1 by cpx_flat/ -HLT10 @IHV -IHV /4 width=3 by csx_cpx_trans, cpx_pair_sn/ | -IHV -H1T1 -HLV0 * #H #H1T10 destruct - elim (tstc_dec T1 T0) #H2T10 - [ @IHT1 -IHT1 /4 width=3 by cpxs_strap2, cpxs_strap1, tstc_canc_sn, simple_tstc_repl_dx/ + elim (tsts_dec T1 T0) #H2T10 + [ @IHT1 -IHT1 /4 width=3 by cpxs_strap2, cpxs_strap1, tsts_canc_sn, simple_tsts_repl_dx/ | -IHT1 -H3T1 -H1T10 /3 width=1 by cpx_cpxs/ ] ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tsts_vector.ma similarity index 90% rename from matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/csx_tsts_vector.ma index 9573d288b..33f847019 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tsts_vector.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "basic_2/computation/acp_cr.ma". -include "basic_2/computation/cpxs_tstc_vector.ma". +include "basic_2/computation/gcp_cr.ma". +include "basic_2/computation/cpxs_tsts_vector.ma". include "basic_2/computation/csx_lpx.ma". include "basic_2/computation/csx_vector.ma". @@ -27,7 +27,7 @@ lemma csx_applv_cnx: ∀h,g,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍 #h #g #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_tstc /2 width=1 by applv_simple/ -IHV -HV -HVs +@csx_appl_simple_tsts /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 // @@ -40,7 +40,7 @@ lemma csx_applv_sort: ∀h,g,G,L,k,Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Vs → ⦃G, L #Hkl #Vs elim Vs -Vs /2 width=1 by/ #V #Vs #IHVs #HVVs elim (csxv_inv_cons … HVVs) #HV #HVs -@csx_appl_simple_tstc /2 width=1 by applv_simple, simple_atom/ -IHVs -HV -HVs +@csx_appl_simple_tsts /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 // @@ -55,7 +55,7 @@ lemma csx_applv_beta: ∀h,g,a,G,L,Vs,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.ⓓ #V0 #Vs #IHV #V #W #T #H1T lapply (csx_fwd_pair_sn … H1T) #HV0 lapply (csx_fwd_flat_dx … H1T) #H2T -@csx_appl_simple_tstc /2 width=1 by applv_simple, simple_flat/ -IHV -HV0 -H2T +@csx_appl_simple_tsts /2 width=1 by applv_simple, simple_flat/ -IHV -HV0 -H2T #X #H #H0 elim (cpxs_fwd_beta_vector … H) -H #H [ -H1T elim H0 -H0 // @@ -71,7 +71,7 @@ lemma csx_applv_delta: ∀h,g,I,G,L,K,V1,i. ⇩[i] L ≡ K.ⓑ{I}V1 → | #V #Vs #IHV #H1T lapply (csx_fwd_pair_sn … H1T) #HV lapply (csx_fwd_flat_dx … H1T) #H2T - @csx_appl_simple_tstc /2 width=1 by applv_simple, simple_atom/ -IHV -HV -H2T + @csx_appl_simple_tsts /2 width=1 by applv_simple, simple_atom/ -IHV -HV -H2T #X #H #H0 elim (cpxs_fwd_delta_vector … HLK … HV12 … H) -HLK -HV12 -H #H [ -H1T elim H0 -H0 // @@ -92,7 +92,7 @@ elim H -V1s -V2s /2 width=3 by csx_appl_theta/ lapply (csx_appl_theta … HW12 … H) -H -HW12 #H lapply (csx_fwd_pair_sn … H) #HW1 lapply (csx_fwd_flat_dx … H) #H1 -@csx_appl_simple_tstc /2 width=3 by simple_flat/ -IHV12s -HW1 -H1 #X #H1 #H2 +@csx_appl_simple_tsts /2 width=3 by simple_flat/ -IHV12s -HW1 -H1 #X #H1 #H2 elim (cpxs_fwd_theta_vector … (V2@V2s) … H1) -H1 /2 width=1 by liftv_cons/ -HV12s -HV12 [ -H #H elim H2 -H2 // | -H2 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/ @@ -107,7 +107,7 @@ lemma csx_applv_cast: ∀h,g,G,L,Vs,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.W → lapply (csx_fwd_pair_sn … H1W) #HV lapply (csx_fwd_flat_dx … H1W) #H2W lapply (csx_fwd_flat_dx … H1T) #H2T -@csx_appl_simple_tstc /2 width=1 by applv_simple, simple_flat/ -IHV -HV -H2W -H2T +@csx_appl_simple_tsts /2 width=1 by applv_simple, simple_flat/ -IHV -HV -H2W -H2T #X #H #H0 elim (cpxs_fwd_cast_vector … H) -H #H [ -H1W -H1T elim H0 -H0 // @@ -116,8 +116,8 @@ elim (cpxs_fwd_cast_vector … H) -H #H ] qed. -theorem csx_acr: ∀h,g. acr (cpx h g) (eq …) (csx h g) (csx h g). -#h #g @mk_acr // +theorem csx_gcr: ∀h,g. gcr (cpx h g) (eq …) (csx h g) (csx h g). +#h #g @mk_gcr // [ /2 width=8 by csx_lift/ | /3 width=1 by csx_applv_cnx/ |3,4,7: /2 width=1 by csx_applv_beta, csx_applv_sort, csx_applv_cast/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/gcp.ma similarity index 90% rename from matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/gcp.ma index 6bcbfe4c7..67dd3f6d6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/gcp.ma @@ -15,7 +15,7 @@ include "basic_2/grammar/genv.ma". include "basic_2/multiple/drops.ma". -(* ABSTRACT COMPUTATION PROPERTIES ******************************************) +(* GENERIC COMPUTATION PROPERTIES *******************************************) definition candidate: Type[0] ≝ relation3 genv lenv term. @@ -34,8 +34,8 @@ definition CP1 ≝ λRR:relation4 genv lenv term term. λRS:relation term. definition CP2 ≝ λRP:candidate. ∀G,L,T,k. RP G L (ⓐ⋆k.T) → RP G L T. -(* requirements for abstract computation properties *) -record acp (RR:relation4 genv lenv term term) (RS:relation term) (RP:candidate) : Prop ≝ +(* requirements for generic computation properties *) +record gcp (RR:relation4 genv lenv term term) (RS:relation term) (RP:candidate) : Prop ≝ { cp0: CP0 RR RS; cp1: CP1 RR RS; cp2: CP2 RP @@ -44,7 +44,7 @@ record acp (RR:relation4 genv lenv term term) (RS:relation term) (RP:candidate) (* Basic properties *********************************************************) (* Basic_1: was: nf2_lift1 *) -lemma acp_lifts: ∀RR,RS. CP0 RR RS → CP0s RR RS. +lemma gcp_lifts: ∀RR,RS. CP0 RR RS → CP0s RR RS. #RR #RS #HRR #G #L1 #L2 #s #des #H elim H -L1 -L2 -des [ #L #T1 #T2 #H #HT1 <(lifts_inv_nil … H) -H // diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_aaa.ma similarity index 79% rename from matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/gcp_aaa.ma index be5351c2b..c890be39e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_aaa.ma @@ -18,23 +18,23 @@ include "basic_2/static/aaa_lifts.ma". include "basic_2/static/aaa_aaa.ma". include "basic_2/computation/lsubc_drops.ma". -(* ABSTRACT COMPUTATION PROPERTIES ******************************************) +(* GENERIC COMPUTATION PROPERTIES *******************************************) (* Main properties **********************************************************) (* Basic_1: was: sc3_arity_csubc *) -theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP. - acp RR RS RP → acr RR RS RP RP → - ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L0,des. ⇩*[Ⓕ, des] L0 ≡ L1 → - ∀T0. ⇧*[des] T ≡ T0 → ∀L2. G ⊢ L2 ⫃[RP] L0 → - ⦃G, L2, T0⦄ ϵ[RP] 〚A〛. +theorem acr_aaa_csubc_lifts: ∀RR,RS,RP. + gcp RR RS RP → gcr RR RS RP RP → + ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L0,des. ⇩*[Ⓕ, des] L0 ≡ L1 → + ∀T0. ⇧*[des] T ≡ T0 → ∀L2. G ⊢ L2 ⫃[RP] L0 → + ⦃G, L2, T0⦄ ϵ[RP] 〚A〛. #RR #RS #RP #H1RP #H2RP #G #L1 #T #A #H elim H -G -L1 -T -A [ #G #L #k #L0 #des #HL0 #X #H #L2 #HL20 >(lifts_inv_sort1 … H) -H - lapply (aacr_acr … H1RP H2RP (⓪)) #HAtom + lapply (acr_gcr … H1RP H2RP (⓪)) #HAtom @(s4 … HAtom … (◊)) // | #I #G #L1 #K1 #V1 #B #i #HLK1 #HKV1B #IHB #L0 #des #HL01 #X #H #L2 #HL20 - lapply (aacr_acr … H1RP H2RP B) #HB + lapply (acr_gcr … H1RP H2RP B) #HB elim (lifts_inv_lref1 … H) -H #i1 #Hi1 #H destruct lapply (drop_fwd_drop2 … HLK1) #HK1b elim (drops_drop_trans … HL01 … HLK1) #X #des1 #i0 #HL0 #H #Hi0 #Hdes1 @@ -58,13 +58,13 @@ theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP. ] | #a #G #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20 elim (lifts_inv_bind1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct - lapply (aacr_acr … H1RP H2RP A) #HA - lapply (aacr_acr … H1RP H2RP B) #HB + lapply (acr_gcr … H1RP H2RP A) #HA + lapply (acr_gcr … H1RP H2RP B) #HB lapply (s1 … HB) -HB #HB @(s6 … HA … (◊) (◊)) /3 width=5 by lsubc_pair, drops_skip, liftv_nil/ | #a #G #L #W #T #B #A #HLWB #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL02 elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct - @(aacr_abst … H1RP H2RP) [ /2 width=5 by/ ] + @(acr_abst … H1RP H2RP) [ /2 width=5 by/ ] #L3 #V3 #W3 #T3 #des3 #HL32 #HW03 #HT03 #H1B #H2B elim (drops_lsubc_trans … H1RP H2RP … HL32 … HL02) -L2 #L2 #HL32 #HL20 lapply (aaa_lifts … L2 W3 … (des @@ des3) … HLWB) -HLWB /2 width=4 by drops_trans, lifts_trans/ #HLW2B @@ -75,19 +75,19 @@ theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP. /3 width=10 by drops_nil, lifts_nil/ | #G #L #V #T #A #_ #_ #IH1A #IH2A #L0 #des #HL0 #X #H #L2 #HL20 elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct - lapply (aacr_acr … H1RP H2RP A) #HA + lapply (acr_gcr … H1RP H2RP A) #HA @(s7 … HA … (◊)) /2 width=5 by/ ] qed. (* Basic_1: was: sc3_arity *) -lemma aacr_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP RP → - ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L, T⦄ ϵ[RP] 〚A〛. -/2 width=8 by drops_nil, lifts_nil, aacr_aaa_csubc_lifts/ qed. +lemma acr_aaa: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP → + ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L, T⦄ ϵ[RP] 〚A〛. +/2 width=8 by drops_nil, lifts_nil, acr_aaa_csubc_lifts/ qed. -lemma acp_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP RP → +lemma gcr_aaa: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP → ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → RP G L T. #RR #RS #RP #H1RP #H2RP #G #L #T #A #HT -lapply (aacr_acr … H1RP H2RP A) #HA -@(s1 … HA) /2 width=4 by aacr_aaa/ +lapply (acr_gcr … H1RP H2RP A) #HA +@(s1 … HA) /2 width=4 by acr_aaa/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_cr.ma similarity index 84% rename from matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/gcp_cr.ma index 1537d175c..537769345 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_cr.ma @@ -14,12 +14,12 @@ include "basic_2/notation/relations/ineint_5.ma". include "basic_2/grammar/aarity.ma". -include "basic_2/multiple/gr2_gr2.ma". +include "basic_2/multiple/mr2_mr2.ma". include "basic_2/multiple/lifts_lift_vector.ma". include "basic_2/multiple/drops_drop.ma". -include "basic_2/computation/acp.ma". +include "basic_2/computation/gcp.ma". -(* ABSTRACT COMPUTATION PROPERTIES ******************************************) +(* GENERIC COMPUTATION PROPERTIES *******************************************) definition S0 ≝ λC:candidate. ∀G,L2,L1,T1,d,e. C G L1 T1 → ∀T2. ⇩[Ⓕ, d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → C G L2 T2. @@ -56,8 +56,8 @@ definition S6 ≝ λRP,C:candidate. definition S7 ≝ λC:candidate. ∀G,L,Vs,T,W. C G L (ⒶVs.T) → C G L (ⒶVs.W) → C G L (ⒶVs.ⓝW.T). -(* properties of the abstract candidate of reducibility *) -record acr (RR:relation4 genv lenv term term) (RS:relation term) (RP,C:candidate) : Prop ≝ +(* requirements for the generic reducibility candidate *) +record gcr (RR:relation4 genv lenv term term) (RS:relation term) (RP,C:candidate) : Prop ≝ { s0: S0 C; s1: S1 RP C; s2: S2 RR RS RP C; @@ -73,21 +73,21 @@ definition cfun: candidate → candidate → candidate ≝ λC1,C2,G,K,T. ∀L,V,U,des. ⇩*[Ⓕ, des] L ≡ K → ⇧*[des] T ≡ U → C1 G L V → C2 G L (ⓐV.U). -(* the candidate associated to an atomic arity *) -let rec aacr (RP:candidate) (A:aarity) on A: candidate ≝ +(* the reducibility candidate associated to an atomic arity *) +let rec acr (RP:candidate) (A:aarity) on A: candidate ≝ match A with [ AAtom ⇒ RP -| APair B A ⇒ cfun (aacr RP B) (aacr RP A) +| APair B A ⇒ cfun (acr RP B) (acr RP A) ]. interpretation "candidate of reducibility of an atomic arity (abstract)" - 'InEInt RP G L T A = (aacr RP A G L T). + 'InEInt RP G L T A = (acr RP A G L T). (* Basic properties *********************************************************) (* Basic_1: was: sc3_lift1 *) -lemma acr_lifts: ∀C. S0 C → S0s C. +lemma gcr_lifts: ∀C. S0 C → S0s C. #C #HC #G #L1 #L2 #des #H elim H -L1 -L2 -des [ #L #T1 #T2 #H #HT1 <(lifts_inv_nil … H) -H // | #L1 #L #L2 #des #d #e #_ #HL2 #IHL #T2 #T1 #H #HLT2 @@ -95,16 +95,16 @@ lemma acr_lifts: ∀C. S0 C → S0s C. ] qed. -lemma rp_lifts: ∀RR,RS,RP. acr RR RS RP RP → +lemma rp_lifts: ∀RR,RS,RP. gcr RR RS RP RP → ∀des,G,L0,L,V,V0. ⇩*[Ⓕ, des] L0 ≡ L → ⇧*[des] V ≡ V0 → RP G L V → RP G L0 V0. #RR #RS #RP #HRP #des #G #L0 #L #V #V0 #HL0 #HV0 #HV -@acr_lifts /width=7 by/ +@gcr_lifts /width=7 by/ @(s0 … HRP) qed. (* Basic_1: was only: sns3_lifts1 *) -lemma rp_liftsv_all: ∀RR,RS,RP. acr RR RS RP RP → +lemma rp_liftsv_all: ∀RR,RS,RP. gcr RR RS RP RP → ∀des,G,L0,L,Vs,V0s. ⇩*[Ⓕ, des] L0 ≡ L → ⇧*[des] Vs ≡ V0s → all … (RP G L) Vs → all … (RP G L0) V0s. #RR #RS #RP #HRP #des #G #L0 #L #Vs #V0s #HL0 #H elim H -Vs -V0s normalize // @@ -114,10 +114,10 @@ qed. (* Basic_1: was: sc3_sn3 sc3_abst sc3_appl sc3_abbr sc3_bind sc3_cast sc3_lift *) -lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP RP → - ∀A. acr RR RS RP (aacr RP A). +lemma acr_gcr: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP → + ∀A. gcr RR RS RP (acr RP A). #RR #RS #RP #H1RP #H2RP #A elim A -A normalize // -#B #A #IHB #IHA @mk_acr normalize +#B #A #IHB #IHA @mk_gcr normalize [ /3 width=7 by drops_cons, lifts_cons/ | #G #L #T #H elim (cp1 … H1RP G L) #k #HK @@ -130,7 +130,7 @@ lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP RP → elim (lifts_inv_applv1 … H) -H #V0s #T0 #HV0s #HT0 #H destruct lapply (s1 … IHB … HB) #HV0 @(s2 … IHA … (V0 @ V0s)) - /3 width=14 by rp_liftsv_all, acp_lifts, cp0, lifts_simple_dx, conj/ + /3 width=14 by rp_liftsv_all, gcp_lifts, cp0, lifts_simple_dx, conj/ | #a #G #L #Vs #U #T #W #HA #L0 #V0 #X #des #HL0 #H #HB elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct elim (lifts_inv_flat1 … HY) -HY #U0 #X #HU0 #HX #H destruct @@ -170,17 +170,17 @@ lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP RP → ] qed. -lemma aacr_abst: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP RP → - ∀a,G,L,W,T,A,B. ⦃G, L, W⦄ ϵ[RP] 〚B〛 → ( - ∀L0,V0,W0,T0,des. ⇩*[Ⓕ, des] L0 ≡ L → ⇧*[des] W ≡ W0 → ⇧*[des + 1] T ≡ T0 → +lemma acr_abst: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP → + ∀a,G,L,W,T,A,B. ⦃G, L, W⦄ ϵ[RP] 〚B〛 → ( + ∀L0,V0,W0,T0,des. ⇩*[Ⓕ, des] L0 ≡ L → ⇧*[des] W ≡ W0 → ⇧*[des + 1] T ≡ T0 → ⦃G, L0, V0⦄ ϵ[RP] 〚B〛 → ⦃G, L0, W0⦄ ϵ[RP] 〚B〛 → ⦃G, L0.ⓓⓝW0.V0, T0⦄ ϵ[RP] 〚A〛 - ) → - ⦃G, L, ⓛ{a}W.T⦄ ϵ[RP] 〚②B.A〛. + ) → + ⦃G, L, ⓛ{a}W.T⦄ ϵ[RP] 〚②B.A〛. #RR #RS #RP #H1RP #H2RP #a #G #L #W #T #A #B #HW #HA #L0 #V0 #X #des #HL0 #H #HB -lapply (aacr_acr … H1RP H2RP A) #HCA -lapply (aacr_acr … H1RP H2RP B) #HCB +lapply (acr_gcr … H1RP H2RP A) #HCA +lapply (acr_gcr … H1RP H2RP B) #HCB elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct -lapply (acr_lifts … HL0 … HW0 HW) -HW [ @(s0 … HCB) ] #HW0 +lapply (gcr_lifts … HL0 … HW0 HW) -HW [ @(s0 … HCB) ] #HW0 @(s3 … HCA … (◊)) @(s6 … HCA … (◊) (◊)) // [ @(HA … HL0) // diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma index 7c0a785ca..adc75dd3b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma @@ -13,10 +13,11 @@ (**************************************************************************) include "basic_2/notation/relations/lrsubeqc_4.ma". +include "basic_2/static/lsubr.ma". include "basic_2/static/aaa.ma". -include "basic_2/computation/acp_cr.ma". +include "basic_2/computation/gcp_cr.ma". -(* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****) +(* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************) inductive lsubc (RP) (G): relation lenv ≝ | lsubc_atom: lsubc RP G (⋆) (⋆) @@ -26,7 +27,7 @@ inductive lsubc (RP) (G): relation lenv ≝ . interpretation - "local environment refinement (abstract candidates of reducibility)" + "local environment refinement (generic reducibility)" 'LRSubEqC RP G L1 L2 = (lsubc RP G L1 L2). (* Basic inversion lemmas ***************************************************) @@ -95,6 +96,12 @@ lemma lsubc_inv_pair2: ∀RP,I,G,L1,K2,W. G ⊢ L1 ⫃[RP] K2.ⓑ{I} W → L1 = K1.ⓓⓝW.V & I = Abst. /2 width=3 by lsubc_inv_pair2_aux/ qed-. +(* Basic forward lemmas *****************************************************) + +lemma lsubc_fwd_lsubr: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → L1 ⫃ L2. +#RP #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubr_pair, lsubr_beta/ +qed-. + (* Basic properties *********************************************************) (* Basic_1: was just: csubc_refl *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drop.ma index 9b46f01f0..36f35527c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drop.ma @@ -15,7 +15,7 @@ include "basic_2/static/aaa_lift.ma". include "basic_2/computation/lsubc.ma". -(* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****) +(* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************) (* Properties concerning basic local environment slicing ********************) @@ -42,10 +42,10 @@ qed-. (* Basic_1: was: csubc_drop_conf_rev *) lemma drop_lsubc_trans: ∀RR,RS,RP. - acp RR RS RP → acr RR RS RP RP → + gcp RR RS RP → gcr RR RS RP RP → ∀G,L1,K1,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ∀K2. G ⊢ K1 ⫃[RP] K2 → ∃∃L2. G ⊢ L1 ⫃[RP] L2 & ⇩[Ⓕ, d, e] L2 ≡ K2. -#RR #RS #RP #Hacp #Hacr #G #L1 #K1 #d #e #H elim H -L1 -K1 -d -e +#RR #RS #RP #Hgcp #Hgcr #G #L1 #K1 #d #e #H elim H -L1 -K1 -d -e [ #d #e #He #X #H elim (lsubc_inv_atom1 … H) -H >He /2 width=3 by ex2_intro/ | #L1 #I #V1 #X #H @@ -63,7 +63,7 @@ lemma drop_lsubc_trans: ∀RR,RS,RP. | #K2 #V #W2 #A #HV2 #H1W2 #H2W2 #HK12 #H1 #H2 #H3 destruct elim (lift_inv_flat1 … HV21) -HV21 #W3 #V3 #HW23 #HV3 #H destruct elim (IHLK1 … HK12) #K #HL1K #HK2 - lapply (aacr_acr … Hacp Hacr A) -Hacp -Hacr #HA + lapply (acr_gcr … Hgcp Hgcr A) -Hgcp -Hgcr #HA lapply (s0 … HA … HV2 … HLK1 HV3) -HV2 lapply (s0 … HA … H1W2 … HLK1 HW23) -H1W2 /4 width=11 by lsubc_beta, aaa_lift, drop_skip, ex2_intro/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drops.ma index 5685fd1ef..e1c30a75a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drops.ma @@ -14,19 +14,19 @@ include "basic_2/computation/lsubc_drop.ma". -(* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****) +(* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************) (* Properties concerning generic local environment slicing ******************) (* Basic_1: was: csubc_drop1_conf_rev *) lemma drops_lsubc_trans: ∀RR,RS,RP. - acp RR RS RP → acr RR RS RP RP → + gcp RR RS RP → gcr RR RS RP RP → ∀G,L1,K1,des. ⇩*[Ⓕ, des] L1 ≡ K1 → ∀K2. G ⊢ K1 ⫃[RP] K2 → ∃∃L2. G ⊢ L1 ⫃[RP] L2 & ⇩*[Ⓕ, des] L2 ≡ K2. -#RR #RS #RP #Hacp #Hacr #G #L1 #K1 #des #H elim H -L1 -K1 -des +#RR #RS #RP #Hgcp #Hgcr #G #L1 #K1 #des #H elim H -L1 -K1 -des [ /2 width=3 by drops_nil, ex2_intro/ | #L1 #L #K1 #des #d #e #_ #HLK1 #IHL #K2 #HK12 - elim (drop_lsubc_trans … Hacp Hacr … HLK1 … HK12) -Hacp -Hacr -K1 #K #HLK #HK2 + elim (drop_lsubc_trans … Hgcp Hgcr … HLK1 … HK12) -Hgcp -Hgcr -K1 #K #HLK #HK2 elim (IHL … HLK) -IHL -HLK /3 width=5 by drops_cons, ex2_intro/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_lsuba.ma index d8dcf0e8d..3a17f0e5b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_lsuba.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_lsuba.ma @@ -13,14 +13,14 @@ (**************************************************************************) include "basic_2/static/lsuba.ma". -include "basic_2/computation/acp_aaa.ma". +include "basic_2/computation/gcp_aaa.ma". -(* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****) +(* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************) (* properties concerning lenv refinement for atomic arity assignment ********) -lemma lsuba_lsubc: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP RP → +lemma lsuba_lsubc: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP → ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → G ⊢ L1 ⫃[RP] L2. #RR #RS #RP #H1RP #H2RP #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubc_pair/ -#L1 #L2 #W #V #A #H elim (aaa_inv_cast … H) -H /3 width=4 by aacr_aaa, lsubc_beta/ +#L1 #L2 #W #V #A #H elim (aaa_inv_cast … H) -H /3 width=4 by acr_aaa, lsubc_beta/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/tstc.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/tsts.ma similarity index 62% rename from matita/matita/contribs/lambdadelta/basic_2/grammar/tstc.ma rename to matita/matita/contribs/lambdadelta/basic_2/grammar/tsts.ma index a861d18a6..d3bc8ee96 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/tstc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/tsts.ma @@ -15,27 +15,27 @@ include "basic_2/notation/relations/topiso_2.ma". include "basic_2/grammar/term_simple.ma". -(* SAME TOP TERM CONSTRUCTOR ************************************************) +(* SAME TOP TERM STRUCTURE **************************************************) -inductive tstc: relation term ≝ - | tstc_atom: ∀I. tstc (⓪{I}) (⓪{I}) - | tstc_pair: ∀I,V1,V2,T1,T2. tstc (②{I}V1.T1) (②{I}V2.T2) +inductive tsts: relation term ≝ + | tsts_atom: ∀I. tsts (⓪{I}) (⓪{I}) + | tsts_pair: ∀I,V1,V2,T1,T2. tsts (②{I}V1.T1) (②{I}V2.T2) . -interpretation "same top constructor (term)" 'TopIso T1 T2 = (tstc T1 T2). +interpretation "same top structure (term)" 'TopIso T1 T2 = (tsts T1 T2). (* Basic inversion lemmas ***************************************************) -fact tstc_inv_atom1_aux: ∀T1,T2. T1 ≂ T2 → ∀I. T1 = ⓪{I} → T2 = ⓪{I}. +fact tsts_inv_atom1_aux: ∀T1,T2. T1 ≂ T2 → ∀I. T1 = ⓪{I} → T2 = ⓪{I}. #T1 #T2 * -T1 -T2 // #J #V1 #V2 #T1 #T2 #I #H destruct qed-. (* Basic_1: was: iso_gen_sort iso_gen_lref *) -lemma tstc_inv_atom1: ∀I,T2. ⓪{I} ≂ T2 → T2 = ⓪{I}. -/2 width=3 by tstc_inv_atom1_aux/ qed-. +lemma tsts_inv_atom1: ∀I,T2. ⓪{I} ≂ T2 → T2 = ⓪{I}. +/2 width=3 by tsts_inv_atom1_aux/ qed-. -fact tstc_inv_pair1_aux: ∀T1,T2. T1 ≂ T2 → ∀I,W1,U1. T1 = ②{I}W1.U1 → +fact tsts_inv_pair1_aux: ∀T1,T2. T1 ≂ T2 → ∀I,W1,U1. T1 = ②{I}W1.U1 → ∃∃W2,U2. T2 = ②{I}W2. U2. #T1 #T2 * -T1 -T2 [ #J #I #W1 #U1 #H destruct @@ -44,19 +44,19 @@ fact tstc_inv_pair1_aux: ∀T1,T2. T1 ≂ T2 → ∀I,W1,U1. T1 = ②{I}W1.U1 qed-. (* Basic_1: was: iso_gen_head *) -lemma tstc_inv_pair1: ∀I,W1,U1,T2. ②{I}W1.U1 ≂ T2 → +lemma tsts_inv_pair1: ∀I,W1,U1,T2. ②{I}W1.U1 ≂ T2 → ∃∃W2,U2. T2 = ②{I}W2. U2. -/2 width=5 by tstc_inv_pair1_aux/ qed-. +/2 width=5 by tsts_inv_pair1_aux/ qed-. -fact tstc_inv_atom2_aux: ∀T1,T2. T1 ≂ T2 → ∀I. T2 = ⓪{I} → T1 = ⓪{I}. +fact tsts_inv_atom2_aux: ∀T1,T2. T1 ≂ T2 → ∀I. T2 = ⓪{I} → T1 = ⓪{I}. #T1 #T2 * -T1 -T2 // #J #V1 #V2 #T1 #T2 #I #H destruct qed-. -lemma tstc_inv_atom2: ∀I,T1. T1 ≂ ⓪{I} → T1 = ⓪{I}. -/2 width=3 by tstc_inv_atom2_aux/ qed-. +lemma tsts_inv_atom2: ∀I,T1. T1 ≂ ⓪{I} → T1 = ⓪{I}. +/2 width=3 by tsts_inv_atom2_aux/ qed-. -fact tstc_inv_pair2_aux: ∀T1,T2. T1 ≂ T2 → ∀I,W2,U2. T2 = ②{I}W2.U2 → +fact tsts_inv_pair2_aux: ∀T1,T2. T1 ≂ T2 → ∀I,W2,U2. T2 = ②{I}W2.U2 → ∃∃W1,U1. T1 = ②{I}W1.U1. #T1 #T2 * -T1 -T2 [ #J #I #W2 #U2 #H destruct @@ -64,45 +64,45 @@ fact tstc_inv_pair2_aux: ∀T1,T2. T1 ≂ T2 → ∀I,W2,U2. T2 = ②{I}W2.U2 ] qed-. -lemma tstc_inv_pair2: ∀I,T1,W2,U2. T1 ≂ ②{I}W2.U2 → +lemma tsts_inv_pair2: ∀I,T1,W2,U2. T1 ≂ ②{I}W2.U2 → ∃∃W1,U1. T1 = ②{I}W1.U1. -/2 width=5 by tstc_inv_pair2_aux/ qed-. +/2 width=5 by tsts_inv_pair2_aux/ qed-. (* Basic properties *********************************************************) (* Basic_1: was: iso_refl *) -lemma tstc_refl: reflexive … tstc. +lemma tsts_refl: reflexive … tsts. #T elim T -T // qed. -lemma tstc_sym: symmetric … tstc. +lemma tsts_sym: symmetric … tsts. #T1 #T2 #H elim H -T1 -T2 // qed-. -lemma tstc_dec: ∀T1,T2. Decidable (T1 ≂ T2). +lemma tsts_dec: ∀T1,T2. Decidable (T1 ≂ T2). * #I1 [2: #V1 #T1 ] * #I2 [2,4: #V2 #T2 ] [ elim (eq_item2_dec I1 I2) #HI12 - [ destruct /2 width=1 by tstc_pair, or_introl/ + [ destruct /2 width=1 by tsts_pair, or_introl/ | @or_intror #H - elim (tstc_inv_pair1 … H) -H #V #T #H destruct /2 width=1 by/ + elim (tsts_inv_pair1 … H) -H #V #T #H destruct /2 width=1 by/ ] | @or_intror #H - lapply (tstc_inv_atom1 … H) -H #H destruct + lapply (tsts_inv_atom1 … H) -H #H destruct | @or_intror #H - lapply (tstc_inv_atom2 … H) -H #H destruct + lapply (tsts_inv_atom2 … H) -H #H destruct | elim (eq_item0_dec I1 I2) #HI12 [ destruct /2 width=1 by or_introl/ | @or_intror #H - lapply (tstc_inv_atom2 … H) -H #H destruct /2 width=1 by/ + lapply (tsts_inv_atom2 … H) -H #H destruct /2 width=1 by/ ] ] qed. -lemma simple_tstc_repl_dx: ∀T1,T2. T1 ≂ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄. +lemma simple_tsts_repl_dx: ∀T1,T2. T1 ≂ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄. #T1 #T2 * -T1 -T2 // #I #V1 #V2 #T1 #T2 #H elim (simple_inv_pair … H) -H #J #H destruct // qed-. -lemma simple_tstc_repl_sn: ∀T1,T2. T1 ≂ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄. -/3 width=3 by simple_tstc_repl_dx, tstc_sym/ qed-. +lemma simple_tsts_repl_sn: ∀T1,T2. T1 ≂ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄. +/3 width=3 by simple_tsts_repl_dx, tsts_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/tstc_tstc.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/tsts_tsts.ma similarity index 74% rename from matita/matita/contribs/lambdadelta/basic_2/grammar/tstc_tstc.ma rename to matita/matita/contribs/lambdadelta/basic_2/grammar/tsts_tsts.ma index 83a17a679..d46b497c8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/tstc_tstc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/tsts_tsts.ma @@ -12,21 +12,21 @@ (* *) (**************************************************************************) -include "basic_2/grammar/tstc.ma". +include "basic_2/grammar/tsts.ma". -(* SAME TOP TERM CONSTRUCTOR ************************************************) +(* SAME TOP TERM STRUCTURE **************************************************) (* Main properties **********************************************************) (* Basic_1: was: iso_trans *) -theorem tstc_trans: Transitive … tstc. +theorem tsts_trans: Transitive … tsts. #T1 #T * -T1 -T // #I #V1 #V #T1 #T #X #H -elim (tstc_inv_pair1 … H) -H #V2 #T2 #H destruct // +elim (tsts_inv_pair1 … H) -H #V2 #T2 #H destruct // qed-. -theorem tstc_canc_sn: ∀T,T1. T ≂ T1 → ∀T2. T ≂ T2 → T1 ≂ T2. -/3 width=3 by tstc_trans, tstc_sym/ qed-. +theorem tsts_canc_sn: ∀T,T1. T ≂ T1 → ∀T2. T ≂ T2 → T1 ≂ T2. +/3 width=3 by tsts_trans, tsts_sym/ qed-. -theorem tstc_canc_dx: ∀T1,T. T1 ≂ T → ∀T2. T2 ≂ T → T1 ≂ T2. -/3 width=3 by tstc_trans, tstc_sym/ qed-. +theorem tsts_canc_dx: ∀T1,T. T1 ≂ T → ∀T2. T2 ≂ T → T1 ≂ T2. +/3 width=3 by tsts_trans, tsts_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/tsts_vector.ma similarity index 87% rename from matita/matita/contribs/lambdadelta/basic_2/grammar/tstc_vector.ma rename to matita/matita/contribs/lambdadelta/basic_2/grammar/tsts_vector.ma index df30d65b8..936804ce9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/tstc_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/tsts_vector.ma @@ -13,17 +13,17 @@ (**************************************************************************) include "basic_2/grammar/term_vector.ma". -include "basic_2/grammar/tstc.ma". +include "basic_2/grammar/tsts.ma". -(* SAME TOP TERM CONSTRUCTOR ************************************************) +(* SAME TOP TERM STRUCTURE **************************************************) (* Advanced inversion lemmas ************************************************) (* Basic_1: was only: iso_flats_lref_bind_false iso_flats_flat_bind_false *) -lemma tstc_inv_bind_applv_simple: ∀a,I,Vs,V2,T1,T2. ⒶVs.T1 ≂ ⓑ{a,I} V2. T2 → +lemma tsts_inv_bind_applv_simple: ∀a,I,Vs,V2,T1,T2. ⒶVs.T1 ≂ ⓑ{a,I} V2. T2 → 𝐒⦃T1⦄ → ⊥. #a #I #Vs #V2 #T1 #T2 #H -elim (tstc_inv_pair2 … H) -H #V0 #T0 +elim (tsts_inv_pair2 … H) -H #V0 #T0 elim Vs -Vs normalize [ #H destruct #H /2 width=5 by simple_inv_bind/ | #V #Vs #_ #H destruct diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/drops.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/drops.ma index ff9574ab6..1c0c18888 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/drops.ma @@ -15,7 +15,7 @@ include "basic_2/notation/relations/rdropstar_3.ma". include "basic_2/notation/relations/rdropstar_4.ma". include "basic_2/substitution/drop.ma". -include "basic_2/multiple/gr2_minus.ma". +include "basic_2/multiple/mr2_minus.ma". include "basic_2/multiple/lifts.ma". (* ITERATED LOCAL ENVIRONMENT SLICING ***************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts.ma index 217878d05..67e93078e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts.ma @@ -14,7 +14,7 @@ include "basic_2/notation/relations/rliftstar_3.ma". include "basic_2/substitution/lift.ma". -include "basic_2/multiple/gr2_plus.ma". +include "basic_2/multiple/mr2_plus.ma". (* GENERIC TERM RELOCATION **************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lift.ma index efa5038d2..5761094ab 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lift.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/substitution/lift_lift.ma". -include "basic_2/multiple/gr2_minus.ma". +include "basic_2/multiple/mr2_minus.ma". include "basic_2/multiple/lifts.ma". (* GENERIC TERM RELOCATION **************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/gr2.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2.ma similarity index 96% rename from matita/matita/contribs/lambdadelta/basic_2/multiple/gr2.ma rename to matita/matita/contribs/lambdadelta/basic_2/multiple/mr2.ma index 57bb952b4..bf4331b89 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/gr2.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2.ma @@ -15,7 +15,7 @@ include "basic_2/notation/relations/rat_3.ma". include "basic_2/grammar/term_vector.ma". -(* GENERIC RELOCATION WITH PAIRS ********************************************) +(* MULTIPLE RELOCATION WITH PAIRS *******************************************) inductive at: list2 nat nat → relation nat ≝ | at_nil: ∀i. at (⟠) i i @@ -25,7 +25,7 @@ inductive at: list2 nat nat → relation nat ≝ at des (i1 + e) i2 → at ({d, e} @ des) i1 i2 . -interpretation "application (generic relocation with pairs)" +interpretation "application (multiple relocation with pairs)" 'RAt i1 des i2 = (at des i1 i2). (* Basic inversion lemmas ***************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/gr2_minus.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_minus.ma similarity index 95% rename from matita/matita/contribs/lambdadelta/basic_2/multiple/gr2_minus.ma rename to matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_minus.ma index 4cc93992b..a60ba3956 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/gr2_minus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_minus.ma @@ -13,9 +13,9 @@ (**************************************************************************) include "basic_2/notation/relations/rminus_3.ma". -include "basic_2/multiple/gr2.ma". +include "basic_2/multiple/mr2.ma". -(* GENERIC RELOCATION WITH PAIRS ********************************************) +(* MULTIPLE RELOCATION WITH PAIRS *******************************************) inductive minuss: nat → relation (list2 nat nat) ≝ | minuss_nil: ∀i. minuss i (⟠) (⟠) @@ -25,7 +25,7 @@ inductive minuss: nat → relation (list2 nat nat) ≝ minuss i ({d, e} @ des1) des2 . -interpretation "minus (generic relocation with pairs)" +interpretation "minus (multiple relocation with pairs)" 'RMinus des1 i des2 = (minuss i des1 des2). (* Basic inversion lemmas ***************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/gr2_gr2.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_mr2.ma similarity index 93% rename from matita/matita/contribs/lambdadelta/basic_2/multiple/gr2_gr2.ma rename to matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_mr2.ma index 0c04d5bc5..03c660fe0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/gr2_gr2.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_mr2.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "basic_2/multiple/gr2.ma". +include "basic_2/multiple/mr2.ma". -(* GENERIC RELOCATION WITH PAIRS ********************************************) +(* MULTIPLE RELOCATION WITH PAIRS *******************************************) (* Main properties **********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/gr2_plus.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_plus.ma similarity index 91% rename from matita/matita/contribs/lambdadelta/basic_2/multiple/gr2_plus.ma rename to matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_plus.ma index 4c96bfdfb..d589181ee 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/gr2_plus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_plus.ma @@ -12,16 +12,16 @@ (* *) (**************************************************************************) -include "basic_2/multiple/gr2.ma". +include "basic_2/multiple/mr2.ma". -(* GENERIC RELOCATION WITH PAIRS ********************************************) +(* MULTIPLE RELOCATION WITH PAIRS *******************************************) let rec pluss (des:list2 nat nat) (i:nat) on des ≝ match des with [ nil2 ⇒ ⟠ | cons2 d e des ⇒ {d + i, e} @ pluss des i ]. -interpretation "plus (generic relocation with pairs)" +interpretation "plus (multiple relocation with pairs)" 'plus x y = (pluss x y). (* Basic inversion lemmas ***************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml index 7a26896f5..07c82f98a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml @@ -27,10 +27,14 @@ pp. 53-78]. + + Stage "B" Context-sensitive subject equivalence for native type assignment. + + Stage "A": "Weakening the Applicability Condition" Preservation of stratified native validity for context-sensitive computation on terms. 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 81cd8e41d..b14263c1d 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 @@ -94,7 +94,7 @@ table { [ { "strongly normalizing extended computation" * } { [ "lcosx ( ? ⊢ ~⬊*[?,?,?] ? )" "lcosx_cpx" * ] [ "lsx ( ? ⊢ ⬊*[?,?,?,?] ? )" "lsx_alt ( ? ⊢ ⬊⬊*[?,?,?,?] ? )" "lsx_drop" + "lsx_lpx" + "lsx_lpxs" + "llsx_csx" * ] - [ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_tstc_vector" + "csx_aaa" * ] + [ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_tsts_vector" + "csx_aaa" * ] [ "csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csx_lift" + "csx_lleq" + "csx_lpx" + "csx_lpxs" + "csx_fpbs" * ] } ] @@ -111,7 +111,7 @@ table { ] [ { "context-sensitive extended computation" * } { [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_drop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ] - [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpxs_tstc" + "cpxs_tstc_vector" + "cpxs_leq" + "cpxs_lift" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_cpxs" * ] + [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpxs_tsts" + "cpxs_tsts_vector" + "cpxs_leq" + "cpxs_lift" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_cpxs" * ] } ] [ { "context-sensitive computation" * } { @@ -119,12 +119,12 @@ table { [ "cprs ( ⦃?,?⦄ ⊢ ? ➡* ?)" "cprs_lift" + "cprs_cprs" * ] } ] - [ { "local env. ref. for abstract candidates of reducibility" * } { + [ { "local env. ref. for generic reducibility" * } { [ "lsubc ( ? ⊢ ? ⫃[?] ? )" "lsubc_drop" + "lsubc_drops" + "lsubc_lsuba" * ] } ] - [ { "support for abstract computation properties" * } { - [ "acp" "acp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )" "acp_aaa" * ] + [ { "support for generic computation properties" * } { + [ "gcp" "gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )" "gcp_aaa" * ] } ] } @@ -252,8 +252,8 @@ table { [ "lifts ( ⇧*[?] ? ≡ ? )" "lifts_lift" + "lifts_lifts" * ] } ] - [ { "support for generic relocation" * } { - [ "gr2 ( @⦃?,?⦄ ≡ ? )" "gr2_plus ( ? + ? )" "gr2_minus ( ? ▭ ? ≡ ? )" "gr2_gr2" * ] + [ { "support for multiple relocation" * } { + [ "mr2 ( @⦃?,?⦄ ≡ ? )" "mr2_plus ( ? + ? )" "mr2_minus ( ? ▭ ? ≡ ? )" "mr2_mr2" * ] } ] } @@ -298,8 +298,8 @@ table { [ "leq ( ? ⩬[?,?] ? )" "leq_leq" * ] } ] - [ { "same top term constructor" * } { - [ "tstc ( ? ≂ ? )" "tstc_tstc" + "tstc_vector" * ] + [ { "same top term structure" * } { + [ "tsts ( ? ≂ ? )" "tsts_tsts" + "tsts_vector" * ] } ] [ { "closures" * } { -- 2.39.2