From 1604f2ee65c57eefb7c6b3122eab2a9f32e0552d Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 9 Mar 2018 00:02:50 +0100 Subject: [PATCH] long awaited update in basic_2 csx_lfsx eventually proved! (major result on lfsx) --- .../lambdadelta/basic_2/relocation/lex_tc.ma | 9 +++ .../basic_2/rt_computation/lfpxs.ma | 2 - .../basic_2/rt_computation/lfpxs_cpxs.ma | 2 - .../basic_2/rt_computation/lfpxs_fqup.ma | 1 - .../basic_2/rt_computation/lfsx_csx.ma | 55 +++++++++---------- .../basic_2/rt_computation/lpxs.ma | 5 ++ .../basic_2/rt_computation/lpxs_cpxs.ma | 26 +++++++++ .../basic_2/rt_computation/lpxs_lpx.ma | 31 +++++++++++ .../basic_2/rt_computation/partial.txt | 4 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 2 +- 10 files changed, 99 insertions(+), 38 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_cpxs.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpx.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lex_tc.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lex_tc.ma index 9a7621f9c..d9112a12e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lex_tc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lex_tc.ma @@ -52,3 +52,12 @@ lapply (monotonic_TC … (lexs cfull (cext2 R) 𝐈𝐝) … HL12) -HL12 ] qed-. +lemma lex_ltc_step_dx: ∀R. c_reflexive … R → s_rs_transitive … R (λ_. lex R) → + ∀L1,L. lex (LTC … R) L1 L → + ∀L2. lex R L L2 → lex (LTC … R) L1 L2. +/4 width=3 by lex_ltc, lex_inv_ltc, step/ qed-. + +lemma lex_ltc_step_sn: ∀R. c_reflexive … R → s_rs_transitive … R (λ_. lex R) → + ∀L1,L. lex R L1 L → + ∀L2. lex (LTC … R) L L2 → lex (LTC … R) L1 L2. +/4 width=3 by lex_ltc, lex_inv_ltc, TC_strap/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs.ma index e711286a1..fc6ad071e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs.ma @@ -31,11 +31,9 @@ interpretation lemma lfpx_lfpxs: ∀h,G,T,L1,L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2. /2 width=1 by inj/ qed. -(* Basic_2A1: was just: lpxs_strap1 *) lemma lfpxs_step_dx: ∀h,G,T,L1,L,L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L → ⦃G, L⦄ ⊢ ⬈[h, T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2. /2 width=3 by tc_lfxs_step_dx/ qed. -(* Basic_2A1: was just: lpxs_strap2 *) lemma lfpxs_step_sn: ∀h,G,T,L1,L,L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L → ⦃G, L⦄ ⊢ ⬈*[h, T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2. /2 width=3 by tc_lfxs_step_sn/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_cpxs.ma index e5369c116..472e94af1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_cpxs.ma @@ -24,13 +24,11 @@ lemma lfpxs_pair_refl: ∀h,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 → ∀I,T. ⦃G, L.ⓑ{I}V1⦄ ⊢ ⬈*[h, T] L.ⓑ{I}V2. /2 width=1 by tc_lfxs_pair_refl/ qed. -(* Basic_2A1: uses: lpxs_cpx_trans *) lemma lfpxs_cpx_trans: ∀h,G. s_r_transitive … (cpx h G) (lfpxs h G). #h #G @s_r_trans_LTC2 @lfpx_cpxs_trans (**) (* auto fails *) qed-. (* Note: lfpxs_cpx_conf does not hold, thus we cannot invoke s_r_trans_LTC1 *) -(* Basic_2A1: uses: lpxs_cpxs_trans *) lemma lfpxs_cpxs_trans: ∀h,G. s_rs_transitive … (cpx h G) (lfpxs h G). #h #G @s_r_to_s_rs_trans @s_r_trans_LTC2 @s_rs_trans_TC1 /2 width=3 by lfpx_cpxs_trans/ (**) (* full auto too slow *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqup.ma index 0f90e90e2..6c7615ce4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqup.ma @@ -19,7 +19,6 @@ include "basic_2/rt_computation/lfpxs.ma". (* Advanced properties ******************************************************) -(* Basic_2A1: uses: lpxs_refl *) lemma lfpxs_refl: ∀h,G,T. reflexive … (lfpxs h G T). /2 width=1 by tc_lfxs_refl/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_csx.ma index eb4418777..5310d8ab7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_csx.ma @@ -11,17 +11,15 @@ (* v GNU General Public License Version 2 *) (* *) (**************************************************************************) -(* + +include "basic_2/rt_computation/lpxs_lpx.ma". +include "basic_2/rt_computation/lpxs_cpxs.ma". include "basic_2/rt_computation/csx_cpxs.ma". include "basic_2/rt_computation/csx_lsubr.ma". -include "basic_2/rt_computation/lfsx_lpxs.ma". -*) +include "basic_2/rt_computation/lfsx_lpx.ma". include "basic_2/rt_computation/lsubsx_lfsx.ma". (* STRONGLY NORMALIZING LOCAL ENV.S FOR UNCOUNTED PARALLEL RT-TRANSITION ****) -(* -axiom lpxs_trans: ∀h,G. Transitive … (lpxs h G). -*) (* Advanced properties ******************************************************) @@ -31,46 +29,43 @@ lemma lfsx_pair_lpxs: ∀h,o,G,K1,V. ⦃G, K1⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ → ∀I. G ⊢ ⬈*[h, o, #0] 𝐒⦃K2.ⓑ{I}V⦄. #h #o #G #K1 #V #H @(csx_ind_cpxs … H) -V #V0 #_ #IHV0 #K2 #H -@(lfsx_ind_lpxs … H) -K2 #K0 #HK0 #IHK0 #HK10 #I -@lfsx_intro_lpxs #Y #HY #HnY -elim (lpxs_inv_pair_sn … HY) -HY #K2 #V2 #HK02 #HV02 #H destruct +@(lfsx_ind_lpx … H) -K2 #K0 #HK0 #IHK0 #HK10 #I +@lfsx_intro_lpx #Y #HY #HnY +elim (lpx_inv_pair_sn … HY) -HY #K2 #V2 #HK02 #HV02 #H destruct elim (tdeq_dec h o V0 V2) #HnV02 destruct [ -IHV0 -HV02 -HK0 | -IHK0 -HnY ] -[ /5 width=5 by lfsx_lfdeq_trans, lpxs_trans, lfdeq_pair/ +[ /5 width=5 by lfsx_lfdeq_trans, lpxs_step_dx, lfdeq_pair/ | @(IHV0 … HnV02) -IHV0 -HnV02 - [ - | /3 width=3 by lfsx_lpxs_trans, lfsx_cpxs_trans/ - | /2 width=3 by lpxs_trans/ + [ /2 width=3 by lpxs_cpx_trans/ + | /3 width=3 by lfsx_lpx_trans, lfsx_cpx_trans/ + | /2 width=3 by lpxs_step_dx/ ] - -(* - @(lfsx_lpxs_trans … (K0.ⓑ{I}V2)) - [ @(IHV0 … HnV02 … HK10) -IHV0 -HnV02 - [ - | /2 width=3 by lfsx_cpxs_trans/ - ] - | - ] -*) +] +qed. (* Basic_2A1: uses: lsx_lref_be *) -lemma lfsx_lref_pair: ∀h,o,G,K,V. ⦃G, K⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ → G ⊢ ⬈*[h, o, V] 𝐒⦃K⦄ → - ∀I,L,i. ⬇*[i] L ≡ K.ⓑ{I}V → G ⊢ ⬈*[h, o, #i] 𝐒⦃L⦄. -#h #o #G #K #V #HV #HK #I #L #i #HLK -@(lfsx_lifts … (#0) … HLK) -L /2 width=3 by lfsx_pair_lpxs/ +lemma lfsx_lref_pair_drops: ∀h,o,G,K,V. ⦃G, K⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ → G ⊢ ⬈*[h, o, V] 𝐒⦃K⦄ → + ∀I,i,L. ⬇*[i] L ≡ K.ⓑ{I}V → G ⊢ ⬈*[h, o, #i] 𝐒⦃L⦄. +#h #o #G #K #V #HV #HK #I #i elim i -i +[ #L #H >(drops_fwd_isid … H) -H /2 width=3 by lfsx_pair_lpxs/ +| #i #IH #L #H + elim (drops_inv_bind2_isuni_next … H) -H // #J #Y #HY #H destruct + @(lfsx_lifts … (𝐔❴1❵)) /3 width=6 by drops_refl, drops_drop/ (**) (* full auto fails *) +] qed. (* Main properties **********************************************************) -theorem csx_lsx: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄. +(* Basic_2A1: uses: csx_lsx *) +theorem csx_lfsx: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄. #h #o #G #L #T @(fqup_wf_ind_eq (Ⓕ) … G L T) -G -L -T #Z #Y #X #IH #G #L * * // [ #i #HG #HL #HT #H destruct elim (csx_inv_lref … H) -H [ |*: * ] [ /2 width=1 by lfsx_lref_atom/ | /2 width=3 by lfsx_lref_unit/ - | /4 width=6 by lfsx_lref_pair, fqup_lref/ + | /4 width=6 by lfsx_lref_pair_drops, fqup_lref/ ] -| #a #I #V #T #HG #HL #HT #H destruct +| #p #I #V #T #HG #HL #HT #H destruct elim (csx_fwd_bind_unit … H Void) -H /3 width=1 by lfsx_bind_void/ | #I #V #T #HG #HL #HT #H destruct elim (csx_fwd_flat … H) -H /3 width=1 by lfsx_flat/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma index 507e0c3ef..8b08043fd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma @@ -25,6 +25,11 @@ interpretation "uncounted parallel rt-computation (local environment)" 'PRedTySnStar h G L1 L2 = (lpxs h G L1 L2). +(* Basic properties *********************************************************) + +lemma lpxs_refl: ∀h,G. reflexive … (lpxs h G). +/2 width=1 by lex_refl/ qed. + (* Basic inversion lemmas ***************************************************) lemma lpxs_inv_bind_sn: ∀h,G,I1,L2,K1. ⦃G, K1.ⓘ{I1}⦄ ⊢⬈*[h] L2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_cpxs.ma new file mode 100644 index 000000000..b663f6a61 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_cpxs.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||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_computation/lfpxs_cpxs.ma". +include "basic_2/rt_computation/lfpxs_lpxs.ma". + +(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENVIRONMENTS *****************) + +(* Properties with uncounted context-sensitive rt-computation for terms *****) + +lemma lpxs_cpx_trans: ∀h,G. s_r_transitive … (cpx h G) (λ_.lpxs h G). +/3 width=3 by lfpxs_cpx_trans, lfpxs_lpxs/ qed-. + +lemma lpxs_cpxs_trans: ∀h,G. s_rs_transitive … (cpx h G) (λ_.lpxs h G). +/3 width=3 by lfpxs_cpxs_trans, lfpxs_lpxs/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpx.ma new file mode 100644 index 000000000..d4a602932 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpx.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lex_tc.ma". +include "basic_2/rt_computation/lpxs.ma". +include "basic_2/rt_computation/cpxs_lpx.ma". + +(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENVIRONMENTS *****************) + +(* Properties with uncounted rt-transition for local environments ***********) + +(* Basic_2A1: was: lpxs_strap1 *) +lemma lpxs_step_dx: ∀h,G,L1,L. ⦃G, L1⦄ ⊢ ⬈*[h] L → + ∀L2. ⦃G, L⦄ ⊢ ⬈[h] L2 → ⦃G, L1⦄ ⊢ ⬈*[h] L2. +/3 width=3 by lpx_cpxs_trans, lex_ltc_step_dx/ qed-. + +(* Basic_2A1: was: lpxs_strap2 *) +lemma lpxs_step_sn: ∀h,G,L1,L. ⦃G, L1⦄ ⊢ ⬈[h] L → + ∀L2. ⦃G, L⦄ ⊢ ⬈*[h] L2 → ⦃G, L1⦄ ⊢ ⬈*[h] L2. +/3 width=3 by lpx_cpxs_trans, lex_ltc_step_sn/ 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 d730cd54f..a5cc2eae9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -1,8 +1,8 @@ cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_fqus.ma cpxs_lsubr.ma cpxs_lfdeq.ma cpxs_aaa.ma cpxs_lpx.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma cpxs_ext.ma -lpxs.ma lpxs_length.ma +lpxs.ma lpxs_length.ma lpxs_lpx.ma lpxs_cpxs.ma lfpxs.ma lfpxs_length.ma lfpxs_drops.ma lfpxs_fqup.ma lfpxs_lfdeq.ma lfpxs_aaa.ma lfpxs_cpxs.ma lfpxs_lpxs.ma lfpxs_lfpxs.ma csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_lsubr.ma csx_lfdeq.ma csx_aaa.ma csx_gcp.ma csx_gcr.ma csx_lfpx.ma csx_cnx.ma csx_cpxs.ma csx_lfpxs.ma csx_csx.ma csx_vector.ma csx_cnx_vector.ma csx_csx_vector.ma -lfsx.ma lfsx_drops.ma lfsx_fqup.ma lfsx_lpx.ma lfsx_lpxs.ma lfsx_lfpxs.ma lfsx_lfsx.ma +lfsx.ma lfsx_drops.ma lfsx_fqup.ma lfsx_lpx.ma lfsx_lpxs.ma lfsx_lfpxs.ma lfsx_csx.ma lfsx_lfsx.ma lsubsx.ma lsubsx_lfsx.ma lsubsx_lsubsx.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 8ea1a603f..64c160295 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 @@ -112,7 +112,7 @@ table { [ [ "strongly normalizing for term vectors" ] "csx_vector" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ] [ [ "strongly normalizing for terms" ] "csx" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_lfdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_lfpxs" + "csx_csx" * ] [ [ "for lenvs on referred entries" ] "lfpxs" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lpxs" + "lfpxs_lfpxs" * ] - [ [ "for lenvs on all entries" ] "lpxs" + "( ⦃?,?⦄ ⊢ ⬈*[?] ? )" "lpxs_length" * ] + [ [ "for lenvs on all entries" ] "lpxs" + "( ⦃?,?⦄ ⊢ ⬈*[?] ? )" "lpxs_length" + "lpxs_lpx" + "lpxs_cpxs" * ] [ [ "for binders" ] "cpxs_ext" + "( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" * ] [ [ "for terms" ] "cpxs" + "( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_fqus" + "cpxs_lsubr" + "cpxs_lfdeq" + "cpxs_aaa" + "cpxs_lpx" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ] } -- 2.39.2