From: Ferruccio Guidi Date: Thu, 2 Nov 2017 17:34:36 +0000 (+0000) Subject: - exclusion binder in local environments X-Git-Tag: make_still_working~417 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=be2870b722324a1813ac9e72ebcb2cda6c8733d7 - exclusion binder in local environments the update is now complete, after bugs fixed in lfdeq.ma - minor corrections --- diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile index e0817c219..6bb435082 100644 --- a/matita/matita/contribs/lambdadelta/Makefile +++ b/matita/matita/contribs/lambdadelta/Makefile @@ -204,20 +204,20 @@ define SUMMARY_TEMPLATE @printf ' SUMMARY $(1)\n' @printf 'name "$$(basename $$(@F))"\n\n' > $$@ @printf 'table {\n' >> $$@ - @printf ' class "gray" [ "category"\n' >> $$@ + @printf ' class "gray" [ "category"\n' >> $$@ @printf ' [ "objects" * ]\n' >> $$@ @printf ' ]\n' >> $$@ - @printf ' class "water" [ "sizes"\n' >> $$@ + @printf ' class "water" [ "sizes"\n' >> $$@ @printf ' [ "files" "$$(S1)" ]\n' >> $$@ @printf ' [ "characters" "$$(S2)" ]\n' >> $$@ @printf ' [ "nodes" "$$(S4)" ]\n' >> $$@ @printf ' ]\n' >> $$@ - @printf ' class "grass" [ "propositions"\n' >> $$@ + @printf ' class "green" [ "propositions"\n' >> $$@ @printf ' [ "theorems" "$$(P1)" ]\n' >> $$@ @printf ' [ "lemmas" "$$(P2)" ]\n' >> $$@ @printf ' [ "total" "$$(P3)" ]\n' >> $$@ @printf ' ]\n' >> $$@ - @printf ' class "yellow" [ "concepts"\n' >> $$@ + @printf ' class "grass" [ "concepts"\n' >> $$@ @printf ' [ "declared" "$$(C1)" ]\n' >> $$@ @printf ' [ "defined" "$$(C2)" ]\n' >> $$@ @printf ' [ "total" "$$(C3)" ]\n' >> $$@ diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpxs/lpxs_fqus.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpxs/lpxs_fqus.etc new file mode 100644 index 000000000..cfe64e5ae --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpxs/lpxs_fqus.etc @@ -0,0 +1,141 @@ +(**************************************************************************) +(* ___ *) +(* ||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.ma". + +(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****) + + + +(* 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-. + +lemma lpxs_lleq_fqu_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, o] L1 → K1 ≡[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊐ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, o] L2 & K2 ≡[T2, 0] L2. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 +[ #I #G1 #L1 #V1 #X #H1 #H2 elim (lpxs_inv_pair2 … H1) -H1 + #K0 #V0 #H1KL1 #_ #H destruct + elim (lleq_inv_lref_ge_dx … H2 ? I L1 V1) -H2 // + #K1 #H #H2KL1 lapply (drop_inv_O2 … H) -H #H destruct + /2 width=4 by fqu_lref_O, ex3_intro/ +| * [ #a ] #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H + [ elim (lleq_inv_bind … H) + | elim (lleq_inv_flat … H) + ] -H /2 width=4 by fqu_pair_sn, ex3_intro/ +| #a #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_bind_O … H) -H + /3 width=4 by lpxs_pair, fqu_bind_dx, ex3_intro/ +| #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_flat … H) -H + /2 width=4 by fqu_flat_dx, ex3_intro/ +| #G1 #L1 #L #T1 #U1 #k #HL1 #HTU1 #K1 #H1KL1 #H2KL1 + elim (drop_O1_le (Ⓕ) (k+1) K1) + [ #K #HK1 lapply (lleq_inv_lift_le … H2KL1 … HK1 HL1 … HTU1 ?) -H2KL1 // + #H2KL elim (lpxs_drop_trans_O1 … H1KL1 … HL1) -L1 + #K0 #HK10 #H1KL lapply (drop_mono … HK10 … HK1) -HK10 #H destruct + /3 width=4 by fqu_drop, ex3_intro/ + | lapply (drop_fwd_length_le2 … HL1) -L -T1 -o + lapply (lleq_fwd_length … H2KL1) // + ] +] +qed-. + +lemma lpxs_lleq_fquq_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, o] L1 → K1 ≡[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊐⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, o] L2 & K2 ≡[T2, 0] L2. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1 +elim (fquq_inv_gen … H) -H +[ #H elim (lpxs_lleq_fqu_trans … H … H1KL1 H2KL1) -L1 + /3 width=4 by fqu_fquq, ex3_intro/ +| * #HG #HL #HT destruct /2 width=4 by ex3_intro/ +] +qed-. + +lemma lpxs_lleq_fqup_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, o] L1 → K1 ≡[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊐+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, o] L2 & K2 ≡[T2, 0] L2. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 +[ #G2 #L2 #T2 #H #K1 #H1KL1 #H2KL1 elim (lpxs_lleq_fqu_trans … H … H1KL1 H2KL1) -L1 + /3 width=4 by fqu_fqup, ex3_intro/ +| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #K1 #H1KL1 #H2KL1 elim (IHT1 … H2KL1) // -L1 + #K #HT1 #H1KL #H2KL elim (lpxs_lleq_fqu_trans … HT2 … H1KL H2KL) -L + /3 width=5 by fqup_strap1, ex3_intro/ +] +qed-. + +lemma lpxs_lleq_fqus_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, o] L1 → K1 ≡[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊐* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, o] L2 & K2 ≡[T2, 0] L2. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1 +elim (fqus_inv_gen … H) -H +[ #H elim (lpxs_lleq_fqup_trans … H … H1KL1 H2KL1) -L1 + /3 width=4 by fqup_fqus, ex3_intro/ +| * #HG #HL #HT destruct /2 width=4 by ex3_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma index b675ddec7..a0f48f828 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma @@ -52,8 +52,8 @@ qed. (* Basic_1: was just: sn3_abbr *) (* Basic_2A1: was: csx_lref_bind *) -lemma csx_lref_drops: ∀h,o,I,G,L,K,V,i. ⬇*[i] L ≡ K.ⓑ{I}V → - ⦃G, K⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃#i⦄. +lemma csx_lref_pair: ∀h,o,I,G,L,K,V,i. ⬇*[i] L ≡ K.ⓑ{I}V → + ⦃G, K⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃#i⦄. #h #o #I #G #L #K #V #i #HLK #HV @csx_intro #X #H #Hi elim (cpx_inv_lref1_drops … H) -H [ #H destruct elim Hi // @@ -67,8 +67,8 @@ qed. (* Basic_1: was: sn3_gen_def *) (* Basic_2A1: was: csx_inv_lref_bind *) -lemma csx_inv_lref_drops: ∀h,o,I,G,L,K,V,i. ⬇*[i] L ≡ K.ⓑ{I}V → - ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃#i⦄ → ⦃G, K⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄. +lemma csx_inv_lref_pair: ∀h,o,I,G,L,K,V,i. ⬇*[i] L ≡ K.ⓑ{I}V → + ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃#i⦄ → ⦃G, K⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄. #h #o #I #G #L #K #V #i #HLK #Hi elim (lifts_total V (𝐔❴⫯i❵)) /4 width=9 by csx_inv_lifts, csx_cpx_trans, cpx_delta_drops, drops_isuni_fwd_drop2/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma index fa81a32d2..c010a31a9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma @@ -41,7 +41,7 @@ lemma csx_applv_delta: ∀h,o,I,G,L,K,V1,i. ⬇*[i] L ≡ K.ⓑ{I}V1 → ∀V2. ⬆*[⫯i] V1 ≡ V2 → ∀Vs. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⒶVs.V2⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⒶVs.#i⦄. #h #o #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs -[ /4 width=11 by csx_inv_lifts, csx_lref_drops, drops_isuni_fwd_drop2/ +[ /4 width=11 by csx_inv_lifts, csx_lref_pair, drops_isuni_fwd_drop2/ | #V #Vs #IHV #H1T lapply (csx_fwd_pair_sn … H1T) #HV lapply (csx_fwd_flat_dx … H1T) #H2T diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fpbs.ma deleted file mode 100644 index c756c4ab8..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fpbs.ma +++ /dev/null @@ -1,33 +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/fpbs.ma". -include "basic_2/computation/csx_lleq.ma". -include "basic_2/computation/csx_lpx.ma". - -(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) - -(* Advanced properties ******************************************************) - -lemma csx_fpb_conf: ∀h,o,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, o] T1 → - ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≽[h, o] ⦃G2, L2, T2⦄ → ⦃G2, L2⦄ ⊢ ⬊*[h, o] T2. -#h #o #G1 #L1 #T1 #HT1 #G2 #L2 #T2 * -/2 width=5 by csx_cpx_trans, csx_fquq_conf, csx_lpx_conf, csx_lleq_conf/ -qed-. - -lemma csx_fpbs_conf: ∀h,o,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, o] T1 → - ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → ⦃G2, L2⦄ ⊢ ⬊*[h, o] T2. -#h #o #G1 #L1 #T1 #HT1 #G2 #L2 #T2 #H @(fpbs_ind … H) -G2 -L2 -T2 -/2 width=5 by csx_fpb_conf/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_csx.ma new file mode 100644 index 000000000..c756c4ab8 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_csx.ma @@ -0,0 +1,33 @@ +(**************************************************************************) +(* ___ *) +(* ||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/fpbs.ma". +include "basic_2/computation/csx_lleq.ma". +include "basic_2/computation/csx_lpx.ma". + +(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) + +(* Advanced properties ******************************************************) + +lemma csx_fpb_conf: ∀h,o,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, o] T1 → + ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≽[h, o] ⦃G2, L2, T2⦄ → ⦃G2, L2⦄ ⊢ ⬊*[h, o] T2. +#h #o #G1 #L1 #T1 #HT1 #G2 #L2 #T2 * +/2 width=5 by csx_cpx_trans, csx_fquq_conf, csx_lpx_conf, csx_lleq_conf/ +qed-. + +lemma csx_fpbs_conf: ∀h,o,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, o] T1 → + ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → ⦃G2, L2⦄ ⊢ ⬊*[h, o] T2. +#h #o #G1 #L1 #T1 #HT1 #G2 #L2 #T2 #H @(fpbs_ind … H) -G2 -L2 -T2 +/2 width=5 by csx_fpb_conf/ +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 deleted file mode 100644 index dd559526f..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqus.ma +++ /dev/null @@ -1,121 +0,0 @@ -(* 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-. - -lemma lpxs_lleq_fqu_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, o] L1 → K1 ≡[T1, 0] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊐ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, o] L2 & K2 ≡[T2, 0] L2. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 -[ #I #G1 #L1 #V1 #X #H1 #H2 elim (lpxs_inv_pair2 … H1) -H1 - #K0 #V0 #H1KL1 #_ #H destruct - elim (lleq_inv_lref_ge_dx … H2 ? I L1 V1) -H2 // - #K1 #H #H2KL1 lapply (drop_inv_O2 … H) -H #H destruct - /2 width=4 by fqu_lref_O, ex3_intro/ -| * [ #a ] #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H - [ elim (lleq_inv_bind … H) - | elim (lleq_inv_flat … H) - ] -H /2 width=4 by fqu_pair_sn, ex3_intro/ -| #a #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_bind_O … H) -H - /3 width=4 by lpxs_pair, fqu_bind_dx, ex3_intro/ -| #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_flat … H) -H - /2 width=4 by fqu_flat_dx, ex3_intro/ -| #G1 #L1 #L #T1 #U1 #k #HL1 #HTU1 #K1 #H1KL1 #H2KL1 - elim (drop_O1_le (Ⓕ) (k+1) K1) - [ #K #HK1 lapply (lleq_inv_lift_le … H2KL1 … HK1 HL1 … HTU1 ?) -H2KL1 // - #H2KL elim (lpxs_drop_trans_O1 … H1KL1 … HL1) -L1 - #K0 #HK10 #H1KL lapply (drop_mono … HK10 … HK1) -HK10 #H destruct - /3 width=4 by fqu_drop, ex3_intro/ - | lapply (drop_fwd_length_le2 … HL1) -L -T1 -o - lapply (lleq_fwd_length … H2KL1) // - ] -] -qed-. - -lemma lpxs_lleq_fquq_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, o] L1 → K1 ≡[T1, 0] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊐⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, o] L2 & K2 ≡[T2, 0] L2. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1 -elim (fquq_inv_gen … H) -H -[ #H elim (lpxs_lleq_fqu_trans … H … H1KL1 H2KL1) -L1 - /3 width=4 by fqu_fquq, ex3_intro/ -| * #HG #HL #HT destruct /2 width=4 by ex3_intro/ -] -qed-. - -lemma lpxs_lleq_fqup_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, o] L1 → K1 ≡[T1, 0] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊐+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, o] L2 & K2 ≡[T2, 0] L2. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 -[ #G2 #L2 #T2 #H #K1 #H1KL1 #H2KL1 elim (lpxs_lleq_fqu_trans … H … H1KL1 H2KL1) -L1 - /3 width=4 by fqu_fqup, ex3_intro/ -| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #K1 #H1KL1 #H2KL1 elim (IHT1 … H2KL1) // -L1 - #K #HT1 #H1KL #H2KL elim (lpxs_lleq_fqu_trans … HT2 … H1KL H2KL) -L - /3 width=5 by fqup_strap1, ex3_intro/ -] -qed-. - -lemma lpxs_lleq_fqus_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, o] L1 → K1 ≡[T1, 0] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊐* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, o] L2 & K2 ≡[T2, 0] L2. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1 -elim (fqus_inv_gen … H) -H -[ #H elim (lpxs_lleq_fqup_trans … H … H1KL1 H2KL1) -L1 - /3 width=4 by fqup_fqus, ex3_intro/ -| * #HG #HL #HT destruct /2 width=4 by ex3_intro/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma index 24fa630b6..14c939fac 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma @@ -51,8 +51,8 @@ lemma lfsx_sort: ∀h,o,G,L,s. G ⊢ ⬈*[h, o, ⋆s] 𝐒⦃L⦄. #h #o #G #L1 #s @lfsx_intro #L2 #H #Hs elim Hs -Hs elim (lfpx_inv_sort … H) -H * [ #H1 #H2 destruct // -| #I #K1 #K2 #V1 #V2 #HK12 #H1 #H2 destruct - /4 width=4 by lfdeq_sort, lfxs_isid, frees_sort_gen, frees_inv_sort/ +| #I1 #I2 #K1 #K2 #HK12 #H1 #H2 destruct + /4 width=4 by lfdeq_sort, lfxs_isid, frees_sort, frees_inv_sort/ ] qed. @@ -61,8 +61,8 @@ lemma lfsx_gref: ∀h,o,G,L,p. G ⊢ ⬈*[h, o, §p] 𝐒⦃L⦄. #h #o #G #L1 #s @lfsx_intro #L2 #H #Hs elim Hs -Hs elim (lfpx_inv_gref … H) -H * [ #H1 #H2 destruct // -| #I #K1 #K2 #V1 #V2 #HK12 #H1 #H2 destruct - /4 width=4 by lfdeq_gref, lfxs_isid, frees_gref_gen, frees_inv_gref/ +| #I1 #I2 #K1 #K2 #HK12 #H1 #H2 destruct + /4 width=4 by lfdeq_gref, lfxs_isid, frees_gref, frees_inv_gref/ ] 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 33d4cf482..1e49546fd 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_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_lsubr.ma cpxs_aaa.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma +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_lfpx.ma cpxs_cnx.ma cpxs_cpxs.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 diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma index 2d219c5ce..2d86a95a6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma @@ -94,25 +94,25 @@ lemma lfdeq_atom: ∀h,o,I. ⋆ ≡[h, o, ⓪{I}] ⋆. /2 width=1 by lfxs_atom/ qed. (* Basic_2A1: uses: lleq_sort *) -lemma lfdeq_sort: ∀h,o,I,L1,L2,V1,V2,s. - L1 ≡[h, o, ⋆s] L2 → L1.ⓑ{I}V1 ≡[h, o, ⋆s] L2.ⓑ{I}V2. +lemma lfdeq_sort: ∀h,o,I1,I2,L1,L2,s. + L1 ≡[h, o, ⋆s] L2 → L1.ⓘ{I1} ≡[h, o, ⋆s] L2.ⓘ{I2}. /2 width=1 by lfxs_sort/ qed. -lemma lfdeq_pair: ∀h,o,I,L1,L2,V. - L1 ≡[h, o, V] L2 → L1.ⓑ{I}V ≡[h, o, #0] L2.ⓑ{I}V. +lemma lfdeq_pair: ∀h,o,I,L1,L2,V1,V2. L1 ≡[h, o, V1] L2 → V1 ≡[h, o] V2 → + L1.ⓑ{I}V1 ≡[h, o, #0] L2.ⓑ{I}V2. /2 width=1 by lfxs_pair/ qed. - +(* lemma lfdeq_unit: ∀h,o,f,I,L1,L2. 𝐈⦃f⦄ → L1 ⪤*[cdeq_ext h o, cfull, f] L2 → L1.ⓤ{I} ≡[h, o, #0] L2.ⓤ{I}. /2 width=3 by lfxs_unit/ qed. - -lemma lfdeq_lref: ∀h,o,I,L1,L2,V1,V2,i. - L1 ≡[h, o, #i] L2 → L1.ⓑ{I}V1 ≡[h, o, #⫯i] L2.ⓑ{I}V2. +*) +lemma lfdeq_lref: ∀h,o,I1,I2,L1,L2,i. + L1 ≡[h, o, #i] L2 → L1.ⓘ{I1} ≡[h, o, #⫯i] L2.ⓘ{I2}. /2 width=1 by lfxs_lref/ qed. (* Basic_2A1: uses: lleq_gref *) -lemma lfdeq_gref: ∀h,o,I,L1,L2,V1,V2,l. - L1 ≡[h, o, §l] L2 → L1.ⓑ{I}V1 ≡[h, o, §l] L2.ⓑ{I}V2. +lemma lfdeq_gref: ∀h,o,I1,I2,L1,L2,l. + L1 ≡[h, o, §l] L2 → L1.ⓘ{I1} ≡[h, o, §l] L2.ⓘ{I2}. /2 width=1 by lfxs_gref/ qed. lemma lfdeq_bind_repl_dx: ∀h,o,I,I1,L1,L2.∀T:term. @@ -128,7 +128,7 @@ lemma lfdeq_inv_atom_sn: ∀h,o,Y2. ∀T:term. ⋆ ≡[h, o, T] Y2 → Y2 = ⋆. lemma lfdeq_inv_atom_dx: ∀h,o,Y1. ∀T:term. Y1 ≡[h, o, T] ⋆ → Y1 = ⋆. /2 width=3 by lfxs_inv_atom_dx/ qed-. - +(* lemma lfdeq_inv_zero: ∀h,o,Y1,Y2. Y1 ≡[h, o, #0] Y2 → ∨∨ Y1 = ⋆ ∧ Y2 = ⋆ | ∃∃I,L1,L2,V1,V2. L1 ≡[h, o, V1] L2 & V1 ≡[h, o] V2 & @@ -138,7 +138,7 @@ lemma lfdeq_inv_zero: ∀h,o,Y1,Y2. Y1 ≡[h, o, #0] Y2 → #h #o #Y1 #Y2 #H elim (lfxs_inv_zero … H) -H * /3 width=9 by or3_intro0, or3_intro1, or3_intro2, ex4_5_intro, ex4_4_intro, conj/ qed-. - +*) lemma lfdeq_inv_lref: ∀h,o,Y1,Y2,i. Y1 ≡[h, o, #⫯i] Y2 → (Y1 = ⋆ ∧ Y2 = ⋆) ∨ ∃∃I1,I2,L1,L2. L1 ≡[h, o, #i] L2 & 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 2123e5fd9..8b1cc6982 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 @@ -88,9 +88,8 @@ table { ] [ { "strongly normalizing rt-computation" * } { [ "lcosx ( ? ⊢ ~⬊*[?,?,?] ? )" "lcosx_cpx" * ] - [ "lsx ( ? ⊢ ⬊*[?,?,?,?] ? )" "lsx_alt ( ? ⊢ ⬊⬊*[?,?,?,?] ? )" "lsx_drop" + "lsx_lpx" + "lsx_lpxs" + "llsx_csx" * ] - [ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_theq_vector" + "csx_aaa" * ] - [ "csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csx_lift" + "csx_lleq" + "csx_lpx" + "csx_lpxs" + "csx_fpbs" * ] + [ "lsx_drop" + "lsx_lpx" + "lsx_lpxs" + "llsx_csx" * ] + [ "csx_lleq" + "csx_lpxs" + "csx_fpbs" * ] } ] [ { "parallel qrst-computation" * } { @@ -109,15 +108,9 @@ table { ] *) [ { "uncounted context-sensitive rt-computation" * } { -(* - [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_drop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ] - [ "cpxs_lreq" + "cpxs_lleq" + "cpxs_aaa" * ] -*) -(* [ "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" * ] -*) + [ "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_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lfpxs" * ] [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_fqus" + "cpxs_lsubr" + "cpxs_lfdeq" + "cpxs_aaa" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ] }