From d4ab51c20dbccd1e88cd2c4dcdaf3b4e56301155 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 17 Apr 2017 19:40:28 +0000 Subject: [PATCH] - advances on lfpxs ... - some instances of Conf3 discovered - some refactoring --- .../basic_2/i_static/tc_lfxs_drops.ma | 72 +++++++++++++++++++ .../basic_2/rt_computation/cpxs_aaa.ma | 6 +- .../basic_2/rt_computation/lfprs_aaa.ma | 3 + .../{lfpxs_etc.ma => lfprs_lfpxs.ma} | 0 .../{lpxs_drop.ma => lfpxs_aaa.ma} | 20 +++--- .../{lpxs_aaa.ma => lfpxs_drops.ma} | 28 ++++---- .../basic_2/rt_computation/partial.txt | 2 +- .../basic_2/rt_transition/lfpr_aaa.ma | 7 +- .../basic_2/rt_transition/lfpx_aaa.ma | 7 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 4 +- 10 files changed, 110 insertions(+), 39 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_drops.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfprs_aaa.ma rename matita/matita/contribs/lambdadelta/basic_2/rt_computation/{lfpxs_etc.ma => lfprs_lfpxs.ma} (100%) rename matita/matita/contribs/lambdadelta/basic_2/rt_computation/{lpxs_drop.ma => lfpxs_aaa.ma} (64%) rename matita/matita/contribs/lambdadelta/basic_2/rt_computation/{lpxs_aaa.ma => lfpxs_drops.ma} (57%) diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_drops.ma new file mode 100644 index 000000000..64bb1f3f1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_drops.ma @@ -0,0 +1,72 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relocation/lreq_lreq.ma". +include "basic_2/static/lfxs_drops.ma". +include "basic_2/i_static/tc_lfxs.ma". + +(* ITERATED EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ***) + +definition tc_dedropable_sn: predicate (relation3 lenv term term) ≝ + λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 → + ∀K2,T. K1 ⦻**[R, T] K2 → ∀U. ⬆*[f] T ≡ U → + ∃∃L2. L1 ⦻**[R, U] L2 & ⬇*[b, f] L2 ≡ K2 & L1 ≡[f] L2. + +definition tc_dropable_sn: predicate (relation3 lenv term term) ≝ + λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 → 𝐔⦃f⦄ → + ∀L2,U. L1 ⦻**[R, U] L2 → ∀T. ⬆*[f] T ≡ U → + ∃∃K2. K1 ⦻**[R, T] K2 & ⬇*[b, f] L2 ≡ K2. + +definition tc_dropable_dx: predicate (relation3 lenv term term) ≝ + λR. ∀L1,L2,U. L1 ⦻**[R, U] L2 → + ∀b,f,K2. ⬇*[b, f] L2 ≡ K2 → 𝐔⦃f⦄ → ∀T. ⬆*[f] T ≡ U → + ∃∃K1. ⬇*[b, f] L1 ≡ K1 & K1 ⦻**[R, T] K2. + +(* Properties with generic slicing for local environments *******************) + +lemma dedropable_sn_LTC: ∀R. dedropable_sn R → tc_dedropable_sn R. +#R #HR #b #f #L1 #K1 #HLK1 #K2 #T #H elim H -K2 +[ #K2 #HK12 #U #HTU elim (HR … HLK1 … HK12 … HTU) -K1 -T -HR + /3 width=4 by ex3_intro, inj/ +| #K #K2 #_ #HK2 #IH #U #HTU -HLK1 + elim (IH … HTU) -IH #L #HL1 #HLK + elim (HR … HLK … HK2 … HTU) -K -T -HR + /3 width=6 by lreq_trans, tc_lfxs_step_dx, ex3_intro/ +] +qed-. + +(* Inversion lemmas with generic slicing for local environments *************) + +lemma dropable_sn_LTC: ∀R. dropable_sn R → tc_dropable_sn R. +#R #HR #b #f #L1 #K1 #HLK1 #Hf #L2 #U #H elim H -L2 +[ #L2 #HL12 #T #HTU elim (HR … HLK1 … HL12 … HTU) -L1 -U -HR + /3 width=3 by inj, ex2_intro/ +| #L #L2 #_ #HL2 #IH #T #HTU -HLK1 + elim (IH … HTU) -IH #K #HK1 #HLK + elim (HR … HLK … HL2 … HTU) -L -U -HR + /3 width=3 by tc_lfxs_step_dx, ex2_intro/ +] +qed-. + +lemma dropable_dx_LTC: ∀R. dropable_dx R → tc_dropable_dx R. +#R #HR #L1 #L2 #U #H elim H -L2 +[ #L2 #HL12 #b #f #K2 #HLK2 #Hf #T #HTU + elim (HR … HL12 … HLK2 … HTU) -L2 -U -HR + /3 width=3 by inj, ex2_intro/ +| #L #L2 #_ #HL2 #IH #b #f #K2 #HLK2 #Hf #T #HTU + elim (HR … HL2 … HLK2 … HTU) -L2 -HR // #K #HLK #HK2 + elim (IH … HLK … HTU) -IH -L -U + /3 width=5 by tc_lfxs_step_dx, ex2_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_aaa.ma index 3fa11c673..24aa4a6aa 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_aaa.ma @@ -19,8 +19,6 @@ include "basic_2/rt_computation/cpxs.ma". (* Properties with atomic arity assignment on terms *************************) -lemma cpxs_aaa_conf: ∀h,G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → - ∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A. -#h #G #L #T1 #A #HT1 #T2 #HT12 -@(TC_Conf3 … HT1 ? HT12) -A -T1 -T2 /2 width=5 by cpx_aaa_conf/ +lemma cpxs_aaa_conf: ∀h,G,L. Conf3 … (aaa G L) (cpxs h G L). +#h #G #L @TC_Conf3 @cpx_aaa_conf (**) (* auto fails *) qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfprs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfprs_aaa.ma new file mode 100644 index 000000000..f88fb3239 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfprs_aaa.ma @@ -0,0 +1,3 @@ +lemma lprs_aaa_conf: ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → + ∀L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L2⦄ ⊢ T ⁝ A. +/3 width=5 by lprs_lpxs, lpxs_aaa_conf/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfprs_lfpxs.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfprs_lfpxs.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_aaa.ma similarity index 64% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_drop.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_aaa.ma index c75d754f9..e3cbc16a4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_drop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_aaa.ma @@ -12,18 +12,14 @@ (* *) (**************************************************************************) -include "basic_2/reduction/lpx_drop.ma". -include "basic_2/computation/lpxs.ma". +include "basic_2/rt_transition/lfpx_aaa.ma". +include "basic_2/rt_computation/lfpxs.ma". -(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************) +(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****) -(* Properties on local environment slicing ***********************************) +(* Properties with atomic arity assignment on terms **************************) -lemma lpxs_drop_conf: ∀h,o,G. dropable_sn (lpxs h o G). -/3 width=3 by dropable_sn_TC, lpx_drop_conf/ qed-. - -lemma drop_lpxs_trans: ∀h,o,G. dedropable_sn (lpxs h o G). -/3 width=3 by dedropable_sn_TC, drop_lpx_trans/ qed-. - -lemma lpxs_drop_trans_O1: ∀h,o,G. dropable_dx (lpxs h o G). -/3 width=3 by dropable_dx_TC, lpx_drop_trans_O1/ qed-. +(* Basic_2A1: uses: lpxs_aaa_conf *) +lemma lfpxs_aaa_conf: ∀h,G,T. Conf3 … (λL. aaa G L T) (lfpxs h G T). +#h #G #T @TC_Conf3 @lfpx_aaa_conf (**) (* auto fails *) +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_drops.ma similarity index 57% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_drops.ma index 0dfdd95e2..7f4060200 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_drops.ma @@ -12,19 +12,23 @@ (* *) (**************************************************************************) -include "basic_2/reduction/lpx_aaa.ma". -include "basic_2/computation/lpxs.ma". +include "basic_2/i_static/tc_lfxs_drops.ma". +include "basic_2/rt_transition/lfpx_drops.ma". -(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************) +(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****) -(* Properties about atomic arity assignment on terms ************************) +(* Properties with generic slicing for local environments *******************) -lemma lpxs_aaa_conf: ∀h,o,G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → - ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 → ⦃G, L2⦄ ⊢ T ⁝ A. -#h #o #G #L1 #T #A #HT #L2 #HL12 -@(TC_Conf3 … (λL,A. ⦃G, L⦄ ⊢ T ⁝ A) … HT ? HL12) /2 width=5 by lpx_aaa_conf/ -qed-. +(* Basic_2A1: uses: drop_lpxs_trans *) +lemma drops_lfpxs_trans: ∀h,G. tc_dedropable_sn (cpx h G). +/3 width=5 by drops_lfpx_trans, dedropable_sn_LTC/ qed-. -lemma lprs_aaa_conf: ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → - ∀L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L2⦄ ⊢ T ⁝ A. -/3 width=5 by lprs_lpxs, lpxs_aaa_conf/ qed-. +(* Inversion lemmas with generic slicing for local environments *************) + +(* Basic_2A1: uses: lpxs_drop_conf *) +lemma lfpxs_drops_conf: ∀h,G. tc_dropable_sn (cpx h G). +/3 width=5 by lfpx_drops_conf, dropable_sn_LTC/ qed-. + +(* Basic_2A1: uses: lpxs_drop_trans_O1 *) +lemma lfpxs_drops_trans: ∀h,G. tc_dropable_dx (cpx h G). +/3 width=5 by lfpx_drops_trans, dropable_dx_LTC/ qed-. 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 876994e66..33d4cf482 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -1,5 +1,5 @@ cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_lsubr.ma cpxs_aaa.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma -lfpxs.ma lfpxs_length.ma lfpxs_fqup.ma lfpxs_lfdeq.ma lfpxs_cpxs.ma lfpxs_lfpxs.ma +lfpxs.ma lfpxs_length.ma lfpxs_drops.ma lfpxs_fqup.ma lfpxs_lfdeq.ma lfpxs_aaa.ma lfpxs_cpxs.ma lfpxs_lfpxs.ma csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_lsubr.ma csx_aaa.ma csx_gcp.ma csx_gcr.ma csx_lfpx.ma csx_cnx.ma csx_cpxs.ma csx_csx.ma csx_vector.ma csx_cnx_vector.ma csx_csx_vector.ma lfsx.ma lfsx_fqup.ma lfsx_lfpxs.ma lfsx_lfsx.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_aaa.ma index eb455f036..899bfc1cf 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_aaa.ma @@ -19,10 +19,9 @@ include "basic_2/rt_transition/lfpr_lfpx.ma". (* Properties with atomic arity assignment for terms ************************) -lemma cpr_aaa_conf: ∀h,G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → - ∀T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A. +lemma cpr_aaa_conf: ∀h,G,L. Conf3 … (aaa G L) (cpm 0 h G L). /3 width=5 by cpx_aaa_conf, cpm_fwd_cpx/ qed-. -lemma lfpr_aaa_conf: ∀h,G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → - ∀L2. ⦃G, L1⦄ ⊢ ➡[h, T] L2 → ⦃G, L2⦄ ⊢ T ⁝ A. +(* Basic_2A1: uses: lpr_aaa_conf *) +lemma lfpr_aaa_conf: ∀h,G,T. Conf3 … (λL. aaa G L T) (lfpr h G T). /3 width=4 by lfpx_aaa_conf, lfpr_fwd_lfpx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_aaa.ma index bc6e8a43a..8c5fc717f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_aaa.ma @@ -73,10 +73,9 @@ lemma cpx_aaa_conf_lfpx: ∀h,G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A → ] qed-. -lemma cpx_aaa_conf: ∀h,G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → - ∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A. +lemma cpx_aaa_conf: ∀h,G,L. Conf3 … (aaa G L) (cpx h G L). /2 width=6 by cpx_aaa_conf_lfpx/ qed-. -lemma lfpx_aaa_conf: ∀h,G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → - ∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → ⦃G, L2⦄ ⊢ T ⁝ A. +(* Basic_2A1: uses: lpx_aaa_conf *) +lemma lfpx_aaa_conf: ∀h,G,T. Conf3 … (λL. aaa G L T) (lfpx h G T). /2 width=6 by cpx_aaa_conf_lfpx/ qed-. 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 db3bcf966..673982592 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 @@ -116,7 +116,7 @@ table { [ "lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_fqup" + "lfsx_lfpxs" + "lfsx_lfsx" * ] [ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ] [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_csx" * ] - [ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_cpxs" + "lfpxs_lfpxs" * ] + [ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lfpxs" * ] [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_lsubr" + "cpxs_aaa" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ] } ] @@ -150,7 +150,7 @@ table { class "water" [ { "iterated static typing" * } { [ { "iterated extension on referred entries" * } { - [ "tc_lfxs ( ? ⦻**[?,?] ? )" "tc_lfxs_length" + "tc_lfxs_fqup" + "tc_lfxs_tc_lfxs" * ] + [ "tc_lfxs ( ? ⦻**[?,?] ? )" "tc_lfxs_length" + "tc_lfxs_drops" + "tc_lfxs_fqup" + "tc_lfxs_tc_lfxs" * ] } ] } -- 2.39.2