From 56dd0e9f60e0dabfb587b014755fd4dad27960bb Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 11 Mar 2017 18:29:51 +0000 Subject: [PATCH] main part of lfpxs_cpxs ... --- .../basic_2/rt_computation/lfpxs.ma | 6 +- .../basic_2/rt_computation/lfpxs_cpxs.ma | 78 +++++++++ .../basic_2/rt_computation/lfpxs_fqus.ma | 58 +++++++ .../basic_2/rt_computation/lpxs_cpxs.ma | 161 ------------------ .../basic_2/rt_computation/partial.txt | 2 +- .../basic_2/rt_transition/lfpr_fqup.ma | 4 + .../basic_2/rt_transition/lfpx_fqup.ma | 4 + .../lambdadelta/basic_2/static/lfxs_fqup.ma | 8 + .../lambdadelta/basic_2/web/basic_2_src.tbl | 2 +- 9 files changed, 159 insertions(+), 164 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_cpxs.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqus.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_cpxs.ma 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 7e1b32915..bfee0b286 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs.ma @@ -51,4 +51,8 @@ lemma lfpxs_inv_atom1: ∀h,G,L2.T. ⦃G, ⋆⦄ ⊢ ⬈*[h, T] L2 → L2 = ⋆. (* Basic_2A1: was just: lpxs_inv_atom2 *) lemma lfpxs_inv_atom2: ∀h,G,L1,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] ⋆ → L1 = ⋆. /2 width=2 by TC_lpx_sn_inv_atom2/ qed-. -*) \ No newline at end of file +*) + +(* Basic_2A1: removed theorems 1: + lpxs_pair +*) 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 new file mode 100644 index 000000000..e565bdc67 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_cpxs.ma @@ -0,0 +1,78 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cpxs_lfpx.ma". +include "basic_2/rt_computation/lfpxs_fqup.ma". + +(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****) + +(* Properties with uncounted context-sensitive rt-computation for terms *****) + +lemma lfpxs_pair: ∀h,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 → + ∀I,T. ⦃G, L.ⓑ{I}V1⦄ ⊢ ⬈*[h, T] L.ⓑ{I}V2. +#h #G #L #V1 #V2 #H @(cpxs_ind … H) -V2 +/3 width=3 by lfpxs_strap1, lfpx_pair/ +qed. + +(* Basic_2A1: was just: lpxs_cpx_trans *) +lemma lfpxs_cpx_trans: ∀h,G. s_r_transitive … (cpx h G) (lfpxs h G). +/3 width=5 by s_r_trans_LTC2, lfpx_cpxs_trans/ qed-. + +(* Note: lfpxs_cpx_conf does not hold, thus we cannot invoke s_r_trans_LTC1 *) +(* Basic_2A1: was just: 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 *) +qed-. + +(* Advanced properties on uncounted rt-computation for terms ****************) + +lemma cpxs_bind2: ∀h,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 → + ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ⬈*[h] T2 → + ∀p. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈*[h] ⓑ{p,I}V2.T2. +/4 width=3 by lfpxs_cpxs_trans, lfpxs_pair, cpxs_bind/ qed. + +(* Advanced inversion lemmas on uncounted rt-computation for terms **********) + +lemma cpxs_inv_abst1: ∀h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{p}V1.T1 ⬈*[h] U2 → + ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 ⬈*[h] T2 & + U2 = ⓛ{p}V2.T2. +#h #p #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /2 width=5 by ex3_2_intro/ +#U0 #U2 #_ #HU02 * #V0 #T0 #HV10 #HT10 #H destruct +elim (cpx_inv_abst1 … HU02) -HU02 #V2 #T2 #HV02 #HT02 #H destruct +lapply (lfpxs_cpx_trans … HT02 (L.ⓛV1) ?) +/3 width=5 by lfpxs_pair, cpxs_trans, cpxs_strap1, ex3_2_intro/ +qed-. + +lemma cpxs_inv_abbr1: ∀h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{p}V1.T1 ⬈*[h] U2 → ( + ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈*[h] T2 & + U2 = ⓓ{p}V2.T2 + ) ∨ + ∃∃T2. ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈*[h] T2 & ⬆*[1] U2 ≡ T2 & p = true. +#h #p #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /3 width=5 by ex3_2_intro, or_introl/ +#U0 #U2 #_ #HU02 * * +[ #V0 #T0 #HV10 #HT10 #H destruct + elim (cpx_inv_abbr1 … HU02) -HU02 * + [ #V2 #T2 #HV02 #HT02 #H destruct + lapply (lfpxs_cpx_trans … HT02 (L.ⓓV1) ?) + /4 width=5 by lfpxs_pair, cpxs_trans, cpxs_strap1, ex3_2_intro, or_introl/ + | #T2 #HT02 #HUT2 + lapply (lfpxs_cpx_trans … HT02 (L.ⓓV1) ?) -HT02 + /4 width=3 by lfpxs_pair, cpxs_trans, ex3_intro, or_intror/ + ] +| #U1 #HTU1 #HU01 + elim (cpx_lifts … HU02 (Ⓣ) … (L.ⓓV1) … HU01) + /4 width=3 by cpxs_strap1, drops_refl, drops_drop, ex3_intro, or_intror/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqus.ma new file mode 100644 index 000000000..17e063b6d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqus.ma @@ -0,0 +1,58 @@ +(* Properties on supclosure *************************************************) + +lemma lpx_fqup_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, o] L1 → + ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, o] T & ⦃G1, K1, T⦄ ⊐+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, o] L2. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 +[ #G2 #L2 #T2 #H12 #K1 #HKL1 elim (lpx_fqu_trans … H12 … HKL1) -L1 + /3 width=5 by cpx_cpxs, fqu_fqup, ex3_2_intro/ +| #G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1 + #L0 #T0 #HT10 #HT0 #HL0 elim (lpx_fqu_trans … H2 … HL0) -L + #L #T3 #HT3 #HT32 #HL2 elim (fqup_cpx_trans … HT0 … HT3) -T + /3 width=7 by cpxs_strap1, fqup_strap1, ex3_2_intro/ +] +qed-. + +lemma lpx_fqus_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, o] L1 → + ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, o] T & ⦃G1, K1, T⦄ ⊐* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, o] L2. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 [ /2 width=5 by ex3_2_intro/ ] +#G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1 +#L0 #T0 #HT10 #HT0 #HL0 elim (lpx_fquq_trans … H2 … HL0) -L +#L #T3 #HT3 #HT32 #HL2 elim (fqus_cpx_trans … HT0 … HT3) -T +/3 width=7 by cpxs_strap1, fqus_strap1, ex3_2_intro/ +qed-. + +lemma lpxs_fquq_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, o] L1 → + ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, o] T & ⦃G1, K1, T⦄ ⊐⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, o] L2. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #HT12 #K1 #H @(lpxs_ind_dx … H) -K1 +[ /2 width=5 by ex3_2_intro/ +| #K1 #K #HK1 #_ * #L #T #HT1 #HT2 #HL2 -HT12 + lapply (lpx_cpxs_trans … HT1 … HK1) -HT1 + elim (lpx_fquq_trans … HT2 … HK1) -K + /3 width=7 by lpxs_strap2, cpxs_strap1, ex3_2_intro/ +] +qed-. + +lemma lpxs_fqup_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, o] L1 → + ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, o] T & ⦃G1, K1, T⦄ ⊐+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, o] L2. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #HT12 #K1 #H @(lpxs_ind_dx … H) -K1 +[ /2 width=5 by ex3_2_intro/ +| #K1 #K #HK1 #_ * #L #T #HT1 #HT2 #HL2 -HT12 + lapply (lpx_cpxs_trans … HT1 … HK1) -HT1 + elim (lpx_fqup_trans … HT2 … HK1) -K + /3 width=7 by lpxs_strap2, cpxs_trans, ex3_2_intro/ +] +qed-. + +lemma lpxs_fqus_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, o] L1 → + ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, o] T & ⦃G1, K1, T⦄ ⊐* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, o] L2. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 /2 width=5 by ex3_2_intro/ +#G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1 +#L0 #T0 #HT10 #HT0 #HL0 elim (lpxs_fquq_trans … H2 … HL0) -L +#L #T3 #HT3 #HT32 #HL2 elim (fqus_cpxs_trans … HT3 … HT0) -T +/3 width=7 by cpxs_trans, fqus_strap1, ex3_2_intro/ +qed-. 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 deleted file mode 100644 index 6e1a9e215..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_cpxs.ma +++ /dev/null @@ -1,161 +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/computation/cpxs_cpxs.ma". -include "basic_2/computation/lpxs.ma". - -(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************) - -(* Advanced properties ******************************************************) - -lemma lpxs_pair: ∀h,o,I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 → - ∀V1,V2. ⦃G, L1⦄ ⊢ V1 ➡*[h, o] V2 → - ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡*[h, o] L2.ⓑ{I}V2. -/2 width=1 by TC_lpx_sn_pair/ qed. - -(* Advanced inversion lemmas ************************************************) - -lemma lpxs_inv_pair1: ∀h,o,I,G,K1,L2,V1. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡*[h, o] L2 → - ∃∃K2,V2. ⦃G, K1⦄ ⊢ ➡*[h, o] K2 & ⦃G, K1⦄ ⊢ V1 ➡*[h, o] V2 & L2 = K2.ⓑ{I}V2. -/3 width=3 by TC_lpx_sn_inv_pair1, lpx_cpxs_trans/ qed-. - -lemma lpxs_inv_pair2: ∀h,o,I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ➡*[h, o] K2.ⓑ{I}V2 → - ∃∃K1,V1. ⦃G, K1⦄ ⊢ ➡*[h, o] K2 & ⦃G, K1⦄ ⊢ V1 ➡*[h, o] V2 & L1 = K1.ⓑ{I}V1. -/3 width=3 by TC_lpx_sn_inv_pair2, lpx_cpxs_trans/ qed-. - -(* Advanced eliminators *****************************************************) - -lemma lpxs_ind_alt: ∀h,o,G. ∀R:relation lenv. - R (⋆) (⋆) → ( - ∀I,K1,K2,V1,V2. - ⦃G, K1⦄ ⊢ ➡*[h, o] K2 → ⦃G, K1⦄ ⊢ V1 ➡*[h, o] V2 → - R K1 K2 → R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2) - ) → - ∀L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 → R L1 L2. -/3 width=4 by TC_lpx_sn_ind, lpx_cpxs_trans/ qed-. - -(* Properties on context-sensitive extended parallel computation for terms **) - -lemma lpxs_cpx_trans: ∀h,o,G. b_c_transitive … (cpx h o G) (λ_.lpxs h o G). -/3 width=5 by b_c_trans_LTC2, lpx_cpxs_trans/ qed-. - -(* Note: alternative proof: /3 width=5 by s_r_trans_TC1, lpxs_cpx_trans/ *) -lemma lpxs_cpxs_trans: ∀h,o,G. b_rs_transitive … (cpx h o G) (λ_.lpxs h o G). -#h #o #G @b_c_to_b_rs_trans @b_c_trans_LTC2 -@b_rs_trans_TC1 /2 width=3 by lpx_cpxs_trans/ (**) (* full auto too slow *) -qed-. - -lemma cpxs_bind2: ∀h,o,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h, o] V2 → - ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡*[h, o] T2 → - ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[h, o] ⓑ{a,I}V2.T2. -/4 width=5 by lpxs_cpxs_trans, lpxs_pair, cpxs_bind/ qed. - -(* Inversion lemmas on context-sensitive ext parallel computation for terms *) - -lemma cpxs_inv_abst1: ∀h,o,a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{a}V1.T1 ➡*[h, o] U2 → - ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡*[h, o] V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 ➡*[h, o] T2 & - U2 = ⓛ{a}V2.T2. -#h #o #a #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /2 width=5 by ex3_2_intro/ -#U0 #U2 #_ #HU02 * #V0 #T0 #HV10 #HT10 #H destruct -elim (cpx_inv_abst1 … HU02) -HU02 #V2 #T2 #HV02 #HT02 #H destruct -lapply (lpxs_cpx_trans … HT02 (L.ⓛV1) ?) -/3 width=5 by lpxs_pair, cpxs_trans, cpxs_strap1, ex3_2_intro/ -qed-. - -lemma cpxs_inv_abbr1: ∀h,o,a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{a}V1.T1 ➡*[h, o] U2 → ( - ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡*[h, o] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ➡*[h, o] T2 & - U2 = ⓓ{a}V2.T2 - ) ∨ - ∃∃T2. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡*[h, o] T2 & ⬆[0, 1] U2 ≡ T2 & a = true. -#h #o #a #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /3 width=5 by ex3_2_intro, or_introl/ -#U0 #U2 #_ #HU02 * * -[ #V0 #T0 #HV10 #HT10 #H destruct - elim (cpx_inv_abbr1 … HU02) -HU02 * - [ #V2 #T2 #HV02 #HT02 #H destruct - lapply (lpxs_cpx_trans … HT02 (L.ⓓV1) ?) - /4 width=5 by lpxs_pair, cpxs_trans, cpxs_strap1, ex3_2_intro, or_introl/ - | #T2 #HT02 #HUT2 - lapply (lpxs_cpx_trans … HT02 (L.ⓓV1) ?) -HT02 - /4 width=3 by lpxs_pair, cpxs_trans, ex3_intro, or_intror/ - ] -| #U1 #HTU1 #HU01 - elim (lift_total U2 0 1) #U #HU2 - /6 width=12 by cpxs_strap1, cpx_lift, drop_drop, ex3_intro, or_intror/ -] -qed-. - -(* More advanced properties *************************************************) - -lemma lpxs_pair2: ∀h,o,I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 → - ∀V1,V2. ⦃G, L2⦄ ⊢ V1 ➡*[h, o] V2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡*[h, o] L2.ⓑ{I}V2. -/3 width=3 by lpxs_pair, lpxs_cpxs_trans/ qed. - -(* Properties on supclosure *************************************************) - -lemma lpx_fqup_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, o] L1 → - ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, o] T & ⦃G1, K1, T⦄ ⊐+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, o] L2. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 -[ #G2 #L2 #T2 #H12 #K1 #HKL1 elim (lpx_fqu_trans … H12 … HKL1) -L1 - /3 width=5 by cpx_cpxs, fqu_fqup, ex3_2_intro/ -| #G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1 - #L0 #T0 #HT10 #HT0 #HL0 elim (lpx_fqu_trans … H2 … HL0) -L - #L #T3 #HT3 #HT32 #HL2 elim (fqup_cpx_trans … HT0 … HT3) -T - /3 width=7 by cpxs_strap1, fqup_strap1, ex3_2_intro/ -] -qed-. - -lemma lpx_fqus_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, o] L1 → - ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, o] T & ⦃G1, K1, T⦄ ⊐* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, o] L2. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 [ /2 width=5 by ex3_2_intro/ ] -#G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1 -#L0 #T0 #HT10 #HT0 #HL0 elim (lpx_fquq_trans … H2 … HL0) -L -#L #T3 #HT3 #HT32 #HL2 elim (fqus_cpx_trans … HT0 … HT3) -T -/3 width=7 by cpxs_strap1, fqus_strap1, ex3_2_intro/ -qed-. - -lemma lpxs_fquq_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, o] L1 → - ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, o] T & ⦃G1, K1, T⦄ ⊐⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, o] L2. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #HT12 #K1 #H @(lpxs_ind_dx … H) -K1 -[ /2 width=5 by ex3_2_intro/ -| #K1 #K #HK1 #_ * #L #T #HT1 #HT2 #HL2 -HT12 - lapply (lpx_cpxs_trans … HT1 … HK1) -HT1 - elim (lpx_fquq_trans … HT2 … HK1) -K - /3 width=7 by lpxs_strap2, cpxs_strap1, ex3_2_intro/ -] -qed-. - -lemma lpxs_fqup_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, o] L1 → - ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, o] T & ⦃G1, K1, T⦄ ⊐+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, o] L2. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #HT12 #K1 #H @(lpxs_ind_dx … H) -K1 -[ /2 width=5 by ex3_2_intro/ -| #K1 #K #HK1 #_ * #L #T #HT1 #HT2 #HL2 -HT12 - lapply (lpx_cpxs_trans … HT1 … HK1) -HT1 - elim (lpx_fqup_trans … HT2 … HK1) -K - /3 width=7 by lpxs_strap2, cpxs_trans, ex3_2_intro/ -] -qed-. - -lemma lpxs_fqus_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, o] L1 → - ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, o] T & ⦃G1, K1, T⦄ ⊐* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, o] L2. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 /2 width=5 by ex3_2_intro/ -#G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1 -#L0 #T0 #HT10 #HT0 #HL0 elim (lpxs_fquq_trans … H2 … HL0) -L -#L #T3 #HT3 #HT32 #HL2 elim (fqus_cpxs_trans … HT3 … HT0) -T -/3 width=7 by cpxs_trans, fqus_strap1, ex3_2_intro/ -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 7118b99b9..2cb53faaa 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -1,4 +1,4 @@ cpxs.ma cpxs_tdeq.ma cpxs_drops.ma cpxs_lfpx.ma cpxs_cpxs.ma -lfpxs.ma lfpxs_fqup.ma +lfpxs.ma lfpxs_fqup.ma lfpxs_cpxs.ma csx.ma csx_cnx.ma csx_cpxs.ma csx_csx.ma csx_vector.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_fqup.ma index 297993014..d0be90869 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_fqup.ma @@ -22,3 +22,7 @@ include "basic_2/rt_transition/lfpr.ma". (* Note: lemma 250 *) lemma lfpr_refl: ∀h,G,T. reflexive … (lfpr h G T). /2 width=1 by lfxs_refl/ qed. + +lemma lfpr_pair: ∀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 lfxs_pair/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_fqup.ma index 99e668266..f7d15c1d2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_fqup.ma @@ -21,3 +21,7 @@ include "basic_2/rt_transition/lfpx.ma". lemma lfpx_refl: ∀h,G,T. reflexive … (lfpx h G T). /2 width=1 by lfxs_refl/ qed. + +lemma lfpx_pair: ∀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 lfxs_pair/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_fqup.ma index 62c5b0564..50fb764fa 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_fqup.ma @@ -22,3 +22,11 @@ include "basic_2/static/lfxs.ma". lemma lfxs_refl: ∀R. (∀L. reflexive … (R L)) → ∀L,T. L ⦻*[R, T] L. #R #HR #L #T elim (frees_total L T) /3 width=3 by lexs_refl, ex2_intro/ qed. + +lemma lfxs_pair: ∀R. (∀L. reflexive … (R L)) → + ∀L,V1,V2. R L V1 V2 → ∀I,T. L.ⓑ{I}V1 ⦻*[R, T] L.ⓑ{I}V2. +#R #HR #L #V1 #V2 #HV12 #I #T +elim (frees_total (L.ⓑ{I}V1) T) #f #Hf +elim (pn_split f) * #g #H destruct +/4 width=3 by lexs_refl, lexs_next, lexs_push, ex2_intro/ +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 729331c1d..20b1e11d6 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 @@ -115,7 +115,7 @@ table { *) [ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" * ] [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx" + "csx_cpxs" + "csx_csx" * ] - [ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_fqup" * ] + [ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_fqup" + "lfpxs_cpxs" * ] [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_drops" + "cpxs_lfpx" + "cpxs_cpxs" * ] } ] -- 2.39.2