From: Ferruccio Guidi Date: Mon, 17 Apr 2017 19:40:28 +0000 (+0000) Subject: - advances on lfpxs ... X-Git-Tag: make_still_working~456 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d4ab51c20dbccd1e88cd2c4dcdaf3b4e56301155;p=helm.git - advances on lfpxs ... - some instances of Conf3 discovered - some refactoring --- 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/lfprs_lfpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfprs_lfpxs.ma new file mode 100644 index 000000000..8c8679a47 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfprs_lfpxs.ma @@ -0,0 +1,3 @@ +(* Basic_2A1: was just: lprs_lpxs *) +lemma lprs_lfpxs: ∀h,o,G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1⦄ ⊢ ➡*[h, o] L2. +/3 width=3 by lpr_lpx, monotonic_TC/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_aaa.ma new file mode 100644 index 000000000..e3cbc16a4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_aaa.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rt_transition/lfpx_aaa.ma". +include "basic_2/rt_computation/lfpxs.ma". + +(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****) + +(* Properties with atomic arity assignment on terms **************************) + +(* 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/lfpxs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_drops.ma new file mode 100644 index 000000000..7f4060200 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_drops.ma @@ -0,0 +1,34 @@ +(**************************************************************************) +(* ___ *) +(* ||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/i_static/tc_lfxs_drops.ma". +include "basic_2/rt_transition/lfpx_drops.ma". + +(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****) + +(* Properties with generic slicing for local environments *******************) + +(* 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-. + +(* 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/lfpxs_etc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma deleted file mode 100644 index 8c8679a47..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma +++ /dev/null @@ -1,3 +0,0 @@ -(* Basic_2A1: was just: lprs_lpxs *) -lemma lprs_lfpxs: ∀h,o,G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1⦄ ⊢ ➡*[h, o] L2. -/3 width=3 by lpr_lpx, monotonic_TC/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_aaa.ma deleted file mode 100644 index 0dfdd95e2..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_aaa.ma +++ /dev/null @@ -1,30 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/reduction/lpx_aaa.ma". -include "basic_2/computation/lpxs.ma". - -(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************) - -(* Properties about atomic arity assignment on terms ************************) - -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-. - -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/lpxs_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_drop.ma deleted file mode 100644 index c75d754f9..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_drop.ma +++ /dev/null @@ -1,29 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/reduction/lpx_drop.ma". -include "basic_2/computation/lpxs.ma". - -(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************) - -(* Properties on local environment slicing ***********************************) - -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-. 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" * ] } ] }