From: Ferruccio Guidi Date: Fri, 16 Mar 2018 19:45:42 +0000 (+0100) Subject: update in basic_2 X-Git-Tag: make_still_working~352 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=54c9014b6657403c6e235c652176218e750d4b8a update in basic_2 + first results on fpbs + minor fixes --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpbs/fpbs_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpbs/fpbs_lift.etc new file mode 100644 index 000000000..69f1a77fa --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpbs/fpbs_lift.etc @@ -0,0 +1,36 @@ +(**************************************************************************) +(* ___ *) +(* ||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_lift.ma". +include "basic_2/computation/fpbs.ma". + +(* "QRST" PARALLEL COMPUTATION FOR CLOSURES *********************************) + +(* Advanced properties ******************************************************) + +lemma lstas_fpbs: ∀h,o,G,L,T1,T2,d2. ⦃G, L⦄ ⊢ T1 •*[h, d2] T2 → + ∀d1. d2 ≤ d1 → ⦃G, L⦄ ⊢ T1 ▪[h, o] d1 → ⦃G, L, T1⦄ ≥[h, o] ⦃G, L, T2⦄. +/3 width=5 by cpxs_fpbs, lstas_cpxs/ qed. + +lemma sta_fpbs: ∀h,o,G,L,T,U,d. + ⦃G, L⦄ ⊢ T ▪[h, o] d+1 → ⦃G, L⦄ ⊢ T •*[h, 1] U → + ⦃G, L, T⦄ ≥[h, o] ⦃G, L, U⦄. +/2 width=5 by lstas_fpbs/ qed. + +(* Note: this is used in the closure proof *) +lemma cpr_lpr_sta_fpbs: ∀h,o,G,L1,L2,T1,T2,U2,d2. + ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L1⦄ ⊢ ➡ L2 → + ⦃G, L2⦄ ⊢ T2 ▪[h, o] d2+1 → ⦃G, L2⦄ ⊢ T2 •*[h, 1] U2 → + ⦃G, L1, T1⦄ ≥[h, o] ⦃G, L2, U2⦄. +/4 width=5 by fpbs_strap1, cpr_lpr_fpbs, sta_cpx, fpbq_cpx/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx/lpx_fquq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx/lpx_fquq.etc index 799808fc6..a775683dd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx/lpx_fquq.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx/lpx_fquq.etc @@ -1,9 +1,7 @@ -(* Properties on supclosure *************************************************) - -lemma fqu_lpx_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → - ∀K2. ⦃G2, L2⦄ ⊢ ➡[h, o] K2 → - ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡[h, o] K1 & ⦃G1, L1⦄ ⊢ T1 ➡[h, o] T & ⦃G1, K1, T⦄ ⊐ ⦃G2, K2, T2⦄. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 +lemma fqu_lpx_trans: ∀h,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ → + ∀K2. ⦃G2, L2⦄ ⊢ ⬈[h] K2 → + ∃∃K1,T. ⦃G1, L1⦄ ⊢ ⬈[h] K1 & ⦃G1, L1⦄ ⊢ T1 ⬈[h] T & ⦃G1, K1, T⦄ ⊐[b] ⦃G2, K2, T2⦄. +#h #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 /3 width=5 by fqu_lref_O, fqu_pair_sn, fqu_flat_dx, lpx_pair, ex3_2_intro/ [ #a #I #G2 #L2 #V2 #T2 #X #H elim (lpx_inv_pair1 … H) -H #K2 #W2 #HLK2 #HVW2 #H destruct @@ -15,33 +13,10 @@ lemma fqu_lpx_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T qed-. lemma fquq_lpx_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → - ∀K2. ⦃G2, L2⦄ ⊢ ➡[h, o] K2 → - ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡[h, o] K1 & ⦃G1, L1⦄ ⊢ T1 ➡[h, o] T & ⦃G1, K1, T⦄ ⊐⸮ ⦃G2, K2, T2⦄. + ∀K2. ⦃G2, L2⦄ ⊢ ⬈[h, o] K2 → + ∃∃K1,T. ⦃G1, L1⦄ ⊢ ⬈[h, o] K1 & ⦃G1, L1⦄ ⊢ T1 ⬈[h, o] T & ⦃G1, K1, T⦄ ⊐⸮ ⦃G2, K2, T2⦄. #h #o #G1 #G2 #L1 #L2 #T1 #T2 #H #K2 #HLK2 elim (fquq_inv_gen … H) -H [ #HT12 elim (fqu_lpx_trans … HT12 … HLK2) /3 width=5 by fqu_fquq, ex3_2_intro/ | * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/ ] qed-. - -lemma lpx_fqu_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 elim H -G1 -G2 -L1 -L2 -T1 -T2 -/3 width=7 by fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, lpx_pair, ex3_2_intro/ -[ #I #G1 #L1 #V1 #X #H elim (lpx_inv_pair2 … H) -H - #K1 #W1 #HKL1 #HWV1 #H destruct elim (lift_total V1 0 1) - /4 width=7 by cpx_delta, fqu_drop, drop_drop, ex3_2_intro/ -| #G #L1 #K1 #T1 #U1 #k #HLK1 #HTU1 #L0 #HL01 - elim (lpx_drop_trans_O1 … HL01 … HLK1) -L1 - /3 width=5 by fqu_drop, ex3_2_intro/ -] -qed-. - -lemma lpx_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 #H #K1 #HKL1 elim (fquq_inv_gen … H) -H -[ #HT12 elim (lpx_fqu_trans … HT12 … HKL1) /3 width=5 by fqu_fquq, ex3_2_intro/ -| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/ -] -qed-. 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 index cfe64e5ae..96f1ab4aa 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpxs/lpxs_fqus.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpxs/lpxs_fqus.etc @@ -20,28 +20,6 @@ include "basic_2/rt_transition/lfpx.ma". (* 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 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstaralt_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstaralt_8.ma deleted file mode 100644 index dff2063a3..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstaralt_8.ma +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≥ ≥ [ break term 46 h, break term 46 o ] ⦃ break term 46 G2, break term 46 L2, break term 46 T2 ⦄ )" - non associative with precedence 45 - for @{ 'BTPRedStarAlt $h $o $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_ffdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_ffdeq.ma new file mode 100644 index 000000000..f4777a7fb --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_ffdeq.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/static/ffdeq.ma". +include "basic_2/rt_computation/cpxs_lfdeq.ma". + +(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************) + +(* Properties with degree-based equivalence for closures ********************) + +lemma ffdeq_cpxs_trans: ∀h,o,G1,G2,L1,L2,T1,T. ⦃G1, L1, T1⦄ ≛[h, o] ⦃G2, L2, T⦄ → + ∀T2. ⦃G2, L2⦄ ⊢ T ⬈*[h] T2 → + ∃∃T0. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] T0 & ⦃G1, L1, T0⦄ ≛[h, o] ⦃G2, L2, T2⦄. +#h #o #G1 #G2 #L1 #L2 #T1 #T #H #T2 #HT2 +elim (ffdeq_inv_gen_dx … H) -H #H #HL12 #HT1 destruct +elim (lfdeq_cpxs_trans … HT2 … HL12) #T0 #HT0 #HT02 +lapply (cpxs_lfdeq_conf_dx … HT2 … HL12) -HL12 #HL12 +elim (tdeq_cpxs_trans … HT1 … HT0) -T #T #HT1 #HT0 +/4 width=5 by ffdeq_intro_dx, tdeq_trans, ex2_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfdeq.ma index 2a331abf9..12142f2c9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfdeq.ma @@ -32,9 +32,9 @@ elim (tdeq_cpxs_trans … H2 … H3) -T #U0 #H2 #H3 qed-. (* Basic_2A1: was just: cpxs_lleq_conf *) -lemma cpxs_lfdeq_trans: ∀h,o,G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ⬈*[h] T1 → - ∀L2. L0 ≛[h, o, T0] L2 → - ∃∃T. ⦃G, L2⦄ ⊢ T0 ⬈*[h] T & T ≛[h, o] T1. +lemma cpxs_lfdeq_conf: ∀h,o,G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ⬈*[h] T1 → + ∀L2. L0 ≛[h, o, T0] L2 → + ∃∃T. ⦃G, L2⦄ ⊢ T0 ⬈*[h] T & T ≛[h, o] T1. /3 width=3 by lfdeq_cpxs_trans, lfdeq_sym/ qed-. (* Basic_2A1: was just: cpxs_lleq_conf_dx *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfpx.ma index 2b12ff438..bd1f44a92 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfpx.ma @@ -12,7 +12,8 @@ (* *) (**************************************************************************) -include "basic_2/rt_transition/lfpx_fsle.ma". +include "basic_2/rt_transition/cpx_fqus.ma". +include "basic_2/rt_transition/lfpx_fquq.ma". include "basic_2/rt_computation/cpxs_drops.ma". include "basic_2/rt_computation/cpxs_cpxs.ma". @@ -66,3 +67,31 @@ lemma cpxs_bind2_dx: ∀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=5 by lfpx_cpxs_trans, cpxs_bind_dx, lfpx_pair_refl/ qed. + +(* Properties with plus-iterated structural successor for closures **********) + +(* Basic_2A1: uses: lpx_fqup_trans *) +lemma lfpx_fqup_trans: ∀h,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ⬈[h, T1] L1 → + ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ⬈*[h] T & ⦃G1, K1, T⦄ ⊐+[b] ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ⬈[h, T2] L2. +#h #b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 +[ #G2 #L2 #T2 #H12 #K1 #HKL1 elim (lfpx_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 (lfpx_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-. + +(* Properties with star-iterated structural successor for closures **********) + +(* Basic_2A1: uses: lpx_fqus_trans *) +lemma lfpx_fqus_trans: ∀h,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ⬈[h, T1] L1 → + ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ⬈*[h] T & ⦃G1, K1, T⦄ ⊐*[b] ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ⬈[h, T2] L2. +#h #b #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #HKL1 elim (fqus_inv_fqup … H) -H +[ #H12 elim (lfpx_fqup_trans … H12 … HKL1) -L1 /3 width=5 by fqup_fqus, ex3_2_intro/ +| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tdeq.ma index 152925b12..10433b267 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tdeq.ma @@ -20,7 +20,7 @@ include "basic_2/rt_computation/cpxs.ma". (* Properties with degree-based equivalence for terms ***********************) lemma tdeq_cpxs_trans: ∀h,o,U1,T1. U1 ≛[h, o] T1 → ∀G,L,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → - ∃∃U2. ⦃G, L⦄ ⊢ U1 ⬈*[h] U2 & U2 ≛[h, o] T2. + ∃∃U2. ⦃G, L⦄ ⊢ U1 ⬈*[h] U2 & U2 ≛[h, o] T2. #h #o #U1 #T1 #HUT1 #G #L #T2 #HT12 @(cpxs_ind … HT12) -T2 /2 width=3 by ex2_intro/ #T #T2 #_ #HT2 * #U #HU1 #HUT elim (tdeq_cpx_trans … HUT … HT2) -T -T1 /3 width=3 by ex2_intro, cpxs_strap1/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma index 125efb684..2b13efb0e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma @@ -12,19 +12,17 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/btpredstar_8.ma". -include "basic_2/multiple/fqus.ma". -include "basic_2/reduction/fpbq.ma". -include "basic_2/computation/cpxs.ma". -include "basic_2/computation/lpxs.ma". +include "ground_2/lib/star.ma". +include "basic_2/notation/relations/predsubtystar_8.ma". +include "basic_2/rt_transition/fpbq.ma". -(* "QRST" PARALLEL COMPUTATION FOR CLOSURES *********************************) +(* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************) definition fpbs: ∀h. sd h → tri_relation genv lenv term ≝ λh,o. tri_TC … (fpbq h o). -interpretation "'qrst' parallel computation (closure)" - 'BTPRedStar h o G1 L1 T1 G2 L2 T2 = (fpbs h o G1 L1 T1 G2 L2 T2). +interpretation "parallel rst-computation (closure)" + 'PRedSubTyStar h o G1 L1 T1 G2 L2 T2 = (fpbs h o G1 L1 T1 G2 L2 T2). (* Basic eliminators ********************************************************) @@ -55,107 +53,20 @@ lemma fpbs_strap2: ∀h,o,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≽[h, o] ⦃G, L, T⦄ ≥[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. /2 width=5 by tri_TC_strap/ qed-. -lemma fqup_fpbs: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 -/4 width=5 by fqu_fquq, fpbq_fquq, tri_step/ -qed. +(* Basic_2A1: uses: lleq_fpbs *) +lemma ffdeq_fpbs: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. +/3 width=1 by fpbq_fpbs, fpbq_ffdeq/ qed. -lemma fqus_fpbs: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 -/3 width=5 by fpbq_fquq, tri_step/ -qed. - -lemma cpxs_fpbs: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, o] T2 → ⦃G, L, T1⦄ ≥[h, o] ⦃G, L, T2⦄. -#h #o #G #L #T1 #T2 #H @(cpxs_ind … H) -T2 -/3 width=5 by fpbq_cpx, fpbs_strap1/ -qed. - -lemma lpxs_fpbs: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 → ⦃G, L1, T⦄ ≥[h, o] ⦃G, L2, T⦄. -#h #o #G #L1 #L2 #T #H @(lpxs_ind … H) -L2 -/3 width=5 by fpbq_lpx, fpbs_strap1/ -qed. - -lemma lleq_fpbs: ∀h,o,G,L1,L2,T. L1 ≡[T, 0] L2 → ⦃G, L1, T⦄ ≥[h, o] ⦃G, L2, T⦄. -/3 width=1 by fpbq_fpbs, fpbq_lleq/ qed. - -lemma cprs_fpbs: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L, T1⦄ ≥[h, o] ⦃G, L, T2⦄. -/3 width=1 by cprs_cpxs, cpxs_fpbs/ qed. - -lemma lprs_fpbs: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1, T⦄ ≥[h, o] ⦃G, L2, T⦄. -/3 width=1 by lprs_lpxs, lpxs_fpbs/ qed. - -lemma fpbs_fqus_trans: ∀h,o,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G, L, T⦄ → - ⦃G, L, T⦄ ⊐* ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. -#h #o #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H @(fqus_ind … H) -G2 -L2 -T2 -/3 width=5 by fpbs_strap1, fpbq_fquq/ -qed-. - -lemma fpbs_fqup_trans: ∀h,o,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G, L, T⦄ → - ⦃G, L, T⦄ ⊐+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. -/3 width=5 by fpbs_fqus_trans, fqup_fqus/ qed-. - -lemma fpbs_cpxs_trans: ∀h,o,G1,G,L1,L,T1,T,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G, L, T⦄ → - ⦃G, L⦄ ⊢ T ➡*[h, o] T2 → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G, L, T2⦄. -#h #o #G1 #G #L1 #L #T1 #T #T2 #H1 #H @(cpxs_ind … H) -T2 -/3 width=5 by fpbs_strap1, fpbq_cpx/ -qed-. - -lemma fpbs_lpxs_trans: ∀h,o,G1,G,L1,L,L2,T1,T. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G, L, T⦄ → - ⦃G, L⦄ ⊢ ➡*[h, o] L2 → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G, L2, T⦄. -#h #o #G1 #G #L1 #L #L2 #T1 #T #H1 #H @(lpxs_ind … H) -L2 -/3 width=5 by fpbs_strap1, fpbq_lpx/ -qed-. - -lemma fpbs_lleq_trans: ∀h,o,G1,G,L1,L,L2,T1,T. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G, L, T⦄ → - L ≡[T, 0] L2 → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G, L2, T⦄. -/3 width=5 by fpbs_strap1, fpbq_lleq/ qed-. - -lemma fqus_fpbs_trans: ∀h,o,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G, L, T⦄ ≥[h, o] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ ⊐* ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. -#h #o #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H @(fqus_ind_dx … H) -G1 -L1 -T1 -/3 width=5 by fpbs_strap2, fpbq_fquq/ -qed-. - -lemma cpxs_fpbs_trans: ∀h,o,G1,G2,L1,L2,T1,T,T2. ⦃G1, L1, T⦄ ≥[h, o] ⦃G2, L2, T2⦄ → - ⦃G1, L1⦄ ⊢ T1 ➡*[h, o] T → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. -#h #o #G1 #G2 #L1 #L2 #T1 #T #T2 #H1 #H @(cpxs_ind_dx … H) -T1 -/3 width=5 by fpbs_strap2, fpbq_cpx/ -qed-. - -lemma lpxs_fpbs_trans: ∀h,o,G1,G2,L1,L,L2,T1,T2. ⦃G1, L, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → - ⦃G1, L1⦄ ⊢ ➡*[h, o] L → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. -#h #o #G1 #G2 #L1 #L #L2 #T1 #T2 #H1 #H @(lpxs_ind_dx … H) -L1 -/3 width=5 by fpbs_strap2, fpbq_lpx/ -qed-. - -lemma lleq_fpbs_trans: ∀h,o,G1,G2,L1,L,L2,T1,T2. ⦃G1, L, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → - L1 ≡[T1, 0] L → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. -/3 width=5 by fpbs_strap2, fpbq_lleq/ qed-. - -lemma cpxs_fqus_fpbs: ∀h,o,G1,G2,L1,L2,T1,T,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, o] T → - ⦃G1, L1, T⦄ ⊐* ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. -/3 width=5 by fpbs_fqus_trans, cpxs_fpbs/ qed. - -lemma cpxs_fqup_fpbs: ∀h,o,G1,G2,L1,L2,T1,T,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, o] T → - ⦃G1, L1, T⦄ ⊐+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. -/3 width=5 by fpbs_fqup_trans, cpxs_fpbs/ qed. - -lemma fqus_lpxs_fpbs: ∀h,o,G1,G2,L1,L,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L, T2⦄ → - ⦃G2, L⦄ ⊢ ➡*[h, o] L2 → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. -/3 width=3 by fpbs_lpxs_trans, fqus_fpbs/ qed. - -lemma cpxs_fqus_lpxs_fpbs: ∀h,o,G1,G2,L1,L,L2,T1,T,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, o] T → - ⦃G1, L1, T⦄ ⊐* ⦃G2, L, T2⦄ → ⦃G2, L⦄ ⊢ ➡*[h, o] L2 → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. -/3 width=5 by cpxs_fqus_fpbs, fpbs_lpxs_trans/ qed. - -lemma lpxs_lleq_fpbs: ∀h,o,G,L1,L,L2,T. ⦃G, L1⦄ ⊢ ➡*[h, o] L → - L ≡[T, 0] L2 → ⦃G, L1, T⦄ ≥[h, o] ⦃G, L2, T⦄. -/3 width=3 by lpxs_fpbs_trans, lleq_fpbs/ qed. - -(* Note: this is used in the closure proof *) -lemma cpr_lpr_fpbs: ∀h,o,G,L1,L2,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L1⦄ ⊢ ➡ L2 → - ⦃G, L1, T1⦄ ≥[h, o] ⦃G, L2, T2⦄. -/4 width=5 by fpbs_strap1, fpbq_fpbs, lpr_fpbq, cpr_fpbq/ -qed. +(* Basic_2A1: uses: fpbs_lleq_trans *) +lemma fpbs_ffdeq_trans: ∀h,o,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G, L, T⦄ → + ∀G2,L2,T2. ⦃G, L, T⦄ ≛[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. +/3 width=9 by fpbs_strap1, fpbq_ffdeq/ qed-. + +(* Basic_2A1: uses: lleq_fpbs_trans *) +lemma ffdeq_fpbs_trans: ∀h,o,G,G2,L,L2,T,T2. ⦃G, L, T⦄ ≥[h, o] ⦃G2, L2, T2⦄ → + ∀G1,L1,T1. ⦃G1, L1, T1⦄ ≛[h, o] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. +/3 width=5 by fpbs_strap2, fpbq_ffdeq/ qed-. + +(* Basic_2A1: removed theorems 3: + fpb_fpbsa_trans fpbs_fpbsa fpbsa_inv_fpbs +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_alt.ma deleted file mode 100644 index 2f6753934..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_alt.ma +++ /dev/null @@ -1,82 +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/notation/relations/btpredstaralt_8.ma". -include "basic_2/multiple/lleq_fqus.ma". -include "basic_2/computation/cpxs_lleq.ma". -include "basic_2/computation/lpxs_lleq.ma". -include "basic_2/computation/fpbs.ma". - -(* "QREST" PARALLEL COMPUTATION FOR CLOSURES ********************************) - -(* Note: alternative definition of fpbs *) -definition fpbsa: ∀h. sd h → tri_relation genv lenv term ≝ - λh,o,G1,L1,T1,G2,L2,T2. - ∃∃L0,L,T. ⦃G1, L1⦄ ⊢ T1 ➡*[h, o] T & - ⦃G1, L1, T⦄ ⊐* ⦃G2, L0, T2⦄ & - ⦃G2, L0⦄ ⊢ ➡*[h, o] L & L ≡[T2, 0] L2. - -interpretation "'big tree' parallel computation (closure) alternative" - 'BTPRedStarAlt h o G1 L1 T1 G2 L2 T2 = (fpbsa h o G1 L1 T1 G2 L2 T2). - -(* Basic properties *********************************************************) - -lemma fpb_fpbsa_trans: ∀h,o,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≽[h, o] ⦃G, L, T⦄ → - ∀G2,L2,T2. ⦃G, L, T⦄ ≥≥[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥≥[h, o] ⦃G2, L2, T2⦄. -#h #o #G1 #G #L1 #L #T1 #T * -G -L -T [ #G #L #T #HG1 | #T #HT1 | #L #HL1 | #L #HL1 ] -#G2 #L2 #T2 * #L00 #L0 #T0 #HT0 #HG2 #HL00 #HL02 -[ elim (fquq_cpxs_trans … HT0 … HG1) -T - /3 width=7 by fqus_strap2, ex4_3_intro/ -| /3 width=7 by cpxs_strap2, ex4_3_intro/ -| lapply (lpx_cpxs_trans … HT0 … HL1) -HT0 #HT10 - elim (lpx_fqus_trans … HG2 … HL1) -L - /3 width=7 by lpxs_strap2, cpxs_trans, ex4_3_intro/ -| lapply (lleq_cpxs_trans … HT0 … HL1) -HT0 #HT0 - lapply (cpxs_lleq_conf_sn … HT0 … HL1) -HL1 #HL1 - elim (lleq_fqus_trans … HG2 … HL1) -L #K00 #HG12 #HKL00 - elim (lleq_lpxs_trans … HL00 … HKL00) -L00 - /3 width=9 by lleq_trans, ex4_3_intro/ -] -qed-. - -(* Main properties **********************************************************) - -theorem fpbs_fpbsa: ∀h,o,G1,G2,L1,L2,T1,T2. - ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥≥[h, o] ⦃G2, L2, T2⦄. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind_dx … H) -G1 -L1 -T1 -/2 width=7 by fpb_fpbsa_trans, ex4_3_intro/ -qed. - -(* Main inversion lemmas ****************************************************) - -theorem fpbsa_inv_fpbs: ∀h,o,G1,G2,L1,L2,T1,T2. - ⦃G1, L1, T1⦄ ≥≥[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 * -/3 width=5 by cpxs_fqus_lpxs_fpbs, fpbs_strap1, fpbq_lleq/ -qed-. - -(* Advanced properties ******************************************************) - -lemma fpbs_intro_alt: ∀h,o,G1,G2,L1,L0,L,L2,T1,T,T2. - ⦃G1, L1⦄ ⊢ T1 ➡*[h, o] T → ⦃G1, L1, T⦄ ⊐* ⦃G2, L0, T2⦄ → - ⦃G2, L0⦄ ⊢ ➡*[h, o] L → L ≡[T2, 0] L2 → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ . -/3 width=7 by fpbsa_inv_fpbs, ex4_3_intro/ qed. - -(* Advanced inversion lemmas *************************************************) - -lemma fpbs_inv_alt: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → - ∃∃L0,L,T. ⦃G1, L1⦄ ⊢ T1 ➡*[h, o] T & - ⦃G1, L1, T⦄ ⊐* ⦃G2, L0, T2⦄ & - ⦃G2, L0⦄ ⊢ ➡*[h, o] L & L ≡[T2, 0] L2. -/2 width=1 by fpbs_fpbsa/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpxs.ma new file mode 100644 index 000000000..479863b3e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpxs.ma @@ -0,0 +1,49 @@ +(**************************************************************************) +(* ___ *) +(* ||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.ma". +include "basic_2/rt_computation/fpbs_fqup.ma". + +(* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************) + +(* Properties with uncounted context-sensitive parallel rt-computation ******) + +lemma cpxs_fpbs: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → ⦃G, L, T1⦄ ≥[h, o] ⦃G, L, T2⦄. +#h #o #G #L #T1 #T2 #H @(cpxs_ind … H) -T2 +/3 width=5 by fpbq_cpx, fpbs_strap1/ +qed. + +lemma fpbs_cpxs_trans: ∀h,o,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G, L, T⦄ → + ∀T2. ⦃G, L⦄ ⊢ T ⬈*[h] T2 → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G, L, T2⦄. +#h #o #G1 #G #L1 #L #T1 #T #H1 #T2 #H @(cpxs_ind … H) -T2 +/3 width=5 by fpbs_strap1, fpbq_cpx/ +qed-. + +lemma cpxs_fpbs_trans: ∀h,o,G1,G2,L1,L2,T,T2. ⦃G1, L1, T⦄ ≥[h, o] ⦃G2, L2, T2⦄ → + ∀T1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] T → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. +#h #o #G1 #G2 #L1 #L2 #T #T2 #H1 #T1 #H @(cpxs_ind_dx … H) -T1 +/3 width=5 by fpbs_strap2, fpbq_cpx/ +qed-. + +(* Properties with star-iterated structural successor for closures **********) + +lemma cpxs_fqus_fpbs: ∀h,o,G1,L1,T1,T. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] T → + ∀G2,L2,T2. ⦃G1, L1, T⦄ ⊐* ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. +/3 width=5 by fpbs_fqus_trans, cpxs_fpbs/ qed. + +(* Properties with plus-iterated structural successor for closures **********) + +lemma cpxs_fqup_fpbs: ∀h,o,G1,L1,T1,T. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] T → + ∀G2,L2,T2. ⦃G1, L1, T⦄ ⊐+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. +/3 width=5 by fpbs_fqup_trans, cpxs_fpbs/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fqup.ma new file mode 100644 index 000000000..af425aa48 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fqup.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/s_computation/fqus_fqup.ma". +include "basic_2/rt_computation/fpbs_fqus.ma". + +(* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************) + +(* Properties with plus-iterated structural successor for closures **********) + +lemma fqup_fpbs: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 +/4 width=5 by fqu_fquq, fpbq_fquq, tri_step/ +qed. + +lemma fpbs_fqup_trans: ∀h,o,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G, L, T⦄ → + ∀G2,L2,T2. ⦃G, L, T⦄ ⊐+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. +/3 width=5 by fpbs_fqus_trans, fqup_fqus/ qed-. + +lemma fqup_fpbs_trans: ∀h,o,G,G2,L,L2,T,T2. ⦃G, L, T⦄ ≥[h, o] ⦃G2, L2, T2⦄ → + ∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊐+ ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. +/3 width=5 by fqus_fpbs_trans, fqup_fqus/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fqus.ma new file mode 100644 index 000000000..3c8274371 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fqus.ma @@ -0,0 +1,38 @@ +(**************************************************************************) +(* ___ *) +(* ||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/s_computation/fqus.ma". +include "basic_2/rt_computation/fpbs.ma". + +(* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************) + +(* Properties with star-iterated structural successor for closures **********) + +lemma fqus_fpbs: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 +/3 width=5 by fpbq_fquq, tri_step/ +qed. + +lemma fpbs_fqus_trans: ∀h,o,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G, L, T⦄ → + ∀G2,L2,T2. ⦃G, L, T⦄ ⊐* ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. +#h #o #G1 #G #L1 #L #T1 #T #H1 #G2 #L2 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 +/3 width=5 by fpbs_strap1, fpbq_fquq/ +qed-. + +lemma fqus_fpbs_trans: ∀h,o,G,G2,L,L2,T,T2. ⦃G, L, T⦄ ≥[h, o] ⦃G2, L2, T2⦄ → + ∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊐* ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. +#h #o #G #G2 #L #L2 #T #T2 #H1 #G1 #L1 #T1 #H @(fqus_ind_dx … H) -G1 -L1 -T1 +/3 width=5 by fpbs_strap2, fpbq_fquq/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lfprs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lfprs.ma new file mode 100644 index 000000000..ed03e166c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lfprs.ma @@ -0,0 +1,13 @@ +(* +lemma cprs_fpbs: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h] T2 → ⦃G, L, T1⦄ ≥[h, o] ⦃G, L, T2⦄. +/3 width=1 by cprs_cpxs, cpxs_fpbs/ qed. + +lemma lprs_fpbs: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1, T⦄ ≥[h, o] ⦃G, L2, T⦄. +/3 width=1 by lprs_lpxs, lpxs_fpbs/ qed. + +(* Note: this is used in the closure proof *) +lemma cpr_lpr_fpbs: ∀h,o,G,L1,L2,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L1⦄ ⊢ ➡ L2 → + ⦃G, L1, T1⦄ ≥[h, o] ⦃G, L2, T2⦄. +/4 width=5 by fpbs_strap1, fpbq_fpbs, lpr_fpbq, cpr_fpbq/ +qed. +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lfpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lfpxs.ma new file mode 100644 index 000000000..c95e8bf9c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lfpxs.ma @@ -0,0 +1,103 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/ffdeq_fqup.ma". +include "basic_2/static/ffdeq_fqus.ma". +include "basic_2/static/ffdeq_ffdeq.ma". +include "basic_2/rt_computation/cpxs_fqus.ma". +include "basic_2/rt_computation/cpxs_ffdeq.ma". +include "basic_2/rt_computation/cpxs_lfpx.ma". +include "basic_2/rt_computation/lfpxs_ffdeq.ma". +include "basic_2/rt_computation/fpbs_cpxs.ma". + +(* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************) + +(* Properties with uncounted parallel rt-computation on referred entries ****) + +(* Basic_2A1: uses: lpxs_fpbs *) +lemma lfpxs_fpbs: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → ⦃G, L1, T⦄ ≥[h, o] ⦃G, L2, T⦄. +#h #o #G #L1 #L2 #T #H @(lfpxs_ind_sn … H) -L2 +/3 width=5 by fpbq_lfpx, fpbs_strap1/ +qed. + +(* Basic_2A1: uses: fpbs_lpxs_trans *) +lemma fpbs_lfpxs_trans: ∀h,o,G1,G2,L1,L,T1,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L, T2⦄ → + ∀L2. ⦃G2, L⦄ ⊢ ⬈*[h, T2] L2 → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. +#h #o #G1 #G2 #L1 #L #T1 #T2 #H1 #L2 #H @(lfpxs_ind_sn … H) -L2 +/3 width=5 by fpbs_strap1, fpbq_lfpx/ +qed-. + +(* Basic_2A1: uses: lpxs_fpbs_trans *) +lemma lfpxs_fpbs_trans: ∀h,o,G1,G2,L,L2,T1,T2. ⦃G1, L, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → + ∀L1. ⦃G1, L1⦄ ⊢ ⬈*[h, T1] L → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. +#h #o #G1 #G2 #L #L2 #T1 #T2 #H1 #L1 #H @(lfpxs_ind_dx … H) -L1 +/3 width=5 by fpbs_strap2, fpbq_lfpx/ +qed-. + +(* Basic_2A1: uses: lpxs_lleq_fpbs *) +lemma lpxs_ffdeq_fpbs: ∀h,o,G1,L1,L,T1. ⦃G1, L1⦄ ⊢ ⬈*[h, T1] L → + ∀G2,L2,T2. ⦃G1, L, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. +/3 width=3 by lfpxs_fpbs_trans, ffdeq_fpbs/ qed. + +(* Properties with star-iterated structural successor for closures **********) + +(* Basic_2A1: uses: fqus_lpxs_fpbs *) +lemma fqus_lfpxs_fpbs: ∀h,o,G1,G2,L1,L,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L, T2⦄ → + ∀L2. ⦃G2, L⦄ ⊢ ⬈*[h, T2] L2 → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. +/3 width=3 by fpbs_lfpxs_trans, fqus_fpbs/ qed. + +(* Properties with uncounted context-sensitive parallel rt-computation ******) + +(* Basic_2A1: uses: cpxs_fqus_lpxs_fpbs *) +lemma cpxs_fqus_lfpxs_fpbs: ∀h,o,G1,L1,T1,T. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] T → + ∀G2,L,T2. ⦃G1, L1, T⦄ ⊐* ⦃G2, L, T2⦄ → + ∀L2.⦃G2, L⦄ ⊢ ⬈*[h, T2] L2 → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. +/3 width=5 by cpxs_fqus_fpbs, fpbs_lfpxs_trans/ qed. + +(* Advanced properties ******************************************************) + +(* Basic_2A1: uses: fpbs_intro_alt *) +lemma fpbs_intro_star: ∀h,o,G1,L1,T1,T. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] T → + ∀G,L,T0. ⦃G1, L1, T⦄ ⊐* ⦃G, L, T0⦄ → + ∀L0. ⦃G, L⦄ ⊢ ⬈*[h, T0] L0 → + ∀G2,L2,T2. ⦃G, L0, T0⦄ ≛[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ . +/3 width=5 by cpxs_fqus_lfpxs_fpbs, fpbs_strap1, fpbq_ffdeq/ qed. + +(* Advanced inversion lemmas *************************************************) + +(* Basic_2A1: uses: fpbs_inv_alt *) +lemma fpbs_inv_star: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → + ∃∃G,L,L0,T,T0. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] T & ⦃G1, L1, T⦄ ⊐* ⦃G, L, T0⦄ + & ⦃G, L⦄ ⊢ ⬈*[h, T0] L0 & ⦃G, L0, T0⦄ ≛[h, o] ⦃G2, L2, T2⦄. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind_dx … H) -G1 -L1 -T1 +[ /2 width=9 by ex4_5_intro/ +| #G1 #G0 #L1 #L0 #T1 #T0 * -G0 -L0 -T0 + [ #G0 #L0 #T0 #H10 #_ * #G3 #L3 #L4 #T3 #T4 #HT03 #H34 #HL34 #H42 + elim (fquq_cpxs_trans … HT03 … H10) -T0 + /3 width=9 by fqus_strap2, ex4_5_intro/ + | #T0 #HT10 #_ * #G3 #L3 #L4 #T3 #T4 #HT03 #H34 #HL34 #H42 + /3 width=9 by cpxs_strap2, ex4_5_intro/ + | #L0 #HL10 #_ * #G3 #L3 #L4 #T3 #T4 #HT13 #H34 #HL34 #H42 + lapply (lfpx_cpxs_trans … HT13 … HL10) -HT13 #HT13 + lapply (lfpx_cpxs_conf … HT13 … HL10) -HL10 #HL10 + elim (lfpx_fqus_trans … H34 … HL10) -L0 + /3 width=9 by lfpxs_step_sn, cpxs_trans, ex4_5_intro/ + | #G0 #L0 #T0 #H10 #_ * #G3 #L3 #L4 #T3 #T4 #HT03 #H34 #HL34 #H42 + elim (ffdeq_cpxs_trans … H10 … HT03) -T0 #T0 #HT10 #H03 + elim (ffdeq_fqus_trans … H03 … H34) -G0 -L0 -T3 #G0 #L0 #T3 #H03 #H34 + elim (ffdeq_lfpxs_trans … H34 … HL34) -L3 #L3 #HL03 #H34 + /3 width=13 by ffdeq_trans, ex4_5_intro/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lift.ma deleted file mode 100644 index 69f1a77fa..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lift.ma +++ /dev/null @@ -1,36 +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_lift.ma". -include "basic_2/computation/fpbs.ma". - -(* "QRST" PARALLEL COMPUTATION FOR CLOSURES *********************************) - -(* Advanced properties ******************************************************) - -lemma lstas_fpbs: ∀h,o,G,L,T1,T2,d2. ⦃G, L⦄ ⊢ T1 •*[h, d2] T2 → - ∀d1. d2 ≤ d1 → ⦃G, L⦄ ⊢ T1 ▪[h, o] d1 → ⦃G, L, T1⦄ ≥[h, o] ⦃G, L, T2⦄. -/3 width=5 by cpxs_fpbs, lstas_cpxs/ qed. - -lemma sta_fpbs: ∀h,o,G,L,T,U,d. - ⦃G, L⦄ ⊢ T ▪[h, o] d+1 → ⦃G, L⦄ ⊢ T •*[h, 1] U → - ⦃G, L, T⦄ ≥[h, o] ⦃G, L, U⦄. -/2 width=5 by lstas_fpbs/ qed. - -(* Note: this is used in the closure proof *) -lemma cpr_lpr_sta_fpbs: ∀h,o,G,L1,L2,T1,T2,U2,d2. - ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L1⦄ ⊢ ➡ L2 → - ⦃G, L2⦄ ⊢ T2 ▪[h, o] d2+1 → ⦃G, L2⦄ ⊢ T2 •*[h, 1] U2 → - ⦃G, L1, T1⦄ ≥[h, o] ⦃G, L2, U2⦄. -/4 width=5 by fpbs_strap1, cpr_lpr_fpbs, sta_cpx, fpbq_cpx/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_ffdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_ffdeq.ma new file mode 100644 index 000000000..04f0d89fc --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_ffdeq.ma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/ffdeq.ma". +include "basic_2/rt_computation/lfpxs_lfdeq.ma". + +(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****) + +(* Properties with degree-based equivalence on closures *********************) + +lemma ffdeq_lfpxs_trans: ∀h,o,G1,G2,L1,L0,T1,T2. ⦃G1, L1, T1⦄ ≛[h, o] ⦃G2, L0, T2⦄ → + ∀L2. ⦃G2, L0⦄ ⊢⬈*[h, T2] L2 → + ∃∃L. ⦃G1, L1⦄ ⊢⬈*[h, T1] L & ⦃G1, L, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄. +#h #o #G1 #G2 #L1 #L0 #T1 #T2 #H1 #L2 #HL02 +elim (ffdeq_inv_gen_dx … H1) -H1 #HG #HL10 #HT12 destruct +elim (lfdeq_lfpxs_trans … HL02 … HL10) -L0 #L0 #HL10 #HL02 +lapply (tdeq_lfpxs_trans … HT12 … HL10) -HL10 #HL10 +/3 width=3 by ffdeq_intro_dx, ex2_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfdeq.ma index 75c9f227a..2eda15369 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfdeq.ma @@ -17,6 +17,17 @@ include "basic_2/rt_computation/lfpxs_fqup.ma". (* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****) +(* Properties with degree-based equivalence on terms ************************) + +lemma lfpxs_tdeq_trans: ∀h,o,G. s_r_confluent1 … (cdeq h o) (lfpxs h G). +#h #o #G #L1 #T1 #T2 #HT12 #L2 #H @(lfpxs_ind_sn … H) -L2 +/3 width=6 by lfpxs_step_dx, lfpx_tdeq_conf/ +qed-. + +lemma tdeq_lfpxs_trans: ∀h,o,T1,T2. T1 ≛[h, o] T2 → + ∀G,L1,L2. ⦃G, L1⦄ ⊢⬈*[h, T2] L2 → ⦃G, L1⦄ ⊢⬈*[h, T1] L2. +/3 width=4 by lfpxs_tdeq_trans, tdeq_sym/ qed-. + (* Properties with degree-based equivalence on referred entries *************) (* Basic_2A1: was: lleq_lpxs_trans *) 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 85df12939..1297cfb04 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,9 @@ -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.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_fqus.ma cpxs_lsubr.ma cpxs_lfdeq.ma cpxs_ffdeq.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_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 +lfpxs.ma lfpxs_length.ma lfpxs_drops.ma lfpxs_fqup.ma lfpxs_lfdeq.ma lfpxs_ffdeq.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_fqus.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_csx.ma lfsx_lfsx.ma lsubsx.ma lsubsx_lfsx.ma lsubsx_lsubsx.ma +fpbs.ma fpbs_fqus.ma fpbs_fqup.ma fpbs_cpxs.ma fpbs_lfpxs.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_fquq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_fquq.ma new file mode 100644 index 000000000..7378f0cd7 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_fquq.ma @@ -0,0 +1,55 @@ +(**************************************************************************) +(* ___ *) +(* ||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_drops.ma". +include "basic_2/rt_transition/lfpx_fsle.ma". +include "basic_2/s_transition/fquq.ma". + +(* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****) + +(* Properties with extended structural successor for closures ***************) + +(* Basic_2A1: uses: lpx_fqu_trans *) +lemma lfpx_fqu_trans: ∀h,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ⬈[h, T1] L1 → + ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ⬈[h] T & ⦃G1, K1, T⦄ ⊐[b] ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ⬈[h, T2] L2. +#h #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 +[ #I #G #K #V #K1 #H + elim (lfpx_inv_zero_pair_dx … H) -H #K0 #V0 #HK0 #HV0 #H destruct + elim (lifts_total V (𝐔❴1❵)) #T #HVT + /3 width=7 by lfpx_cpx_conf, cpx_delta, fqu_drop, ex3_2_intro/ +| /3 width=7 by lfpx_fwd_pair_sn, cpx_pair_sn, fqu_pair_sn, ex3_2_intro/ +| /3 width=6 by lfpx_fwd_bind_dx, cpx_pair_sn, fqu_bind_dx, ex3_2_intro/ +| /3 width=8 by lfpx_fwd_bind_dx_void, cpx_pair_sn, fqu_clear, ex3_2_intro/ +| /3 width=7 by lfpx_fwd_flat_dx, cpx_pair_sn, fqu_flat_dx, ex3_2_intro/ +| #I #G #K #T #U #HTU #K1 #H + elim (lfpx_drops_trans … H (Ⓣ) … HTU) -H + [|*: /3 width=2 by drops_refl, drops_drop/ ] -I #K0 #HK10 #HK0 + elim (drops_inv_succ … HK10) -HK10 #I #Y #HY #H destruct + lapply (drops_fwd_isid … HY ?) -HY // #H destruct + /3 width=5 by fqu_drop, ex3_2_intro/ +] +qed-. + +(* Properties with extended optional structural successor for closures ******) + +(* Basic_2A1: uses: lpx_fquq_trans *) +lemma lfpx_fquq_trans: ∀h,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮[b] ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ⬈[h, T1] L1 → + ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ⬈[h] T & ⦃G1, K1, T⦄ ⊐⸮[b] ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ⬈[h, T2] L2. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #HKL1 cases H -H +[ #H12 elim (lfpx_fqu_trans … H12 … HKL1) -L1 /3 width=5 by fqu_fquq, ex3_2_intro/ +| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq_fqus.ma new file mode 100644 index 000000000..46a9640d9 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq_fqus.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/static/lfdeq_fqus.ma". +include "basic_2/static/ffdeq.ma". + +(* DEGREE-BASED EQUIVALENCE FOR CLOSURES ON REFERRED ENTRIES ****************) + +(* Properties with star-iterated structural successor for closures **********) + +lemma ffdeq_fqus_trans: ∀h,o,b,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≛[h, o] ⦃G, L, T⦄ → + ∀G2,L2,T2. ⦃G, L, T⦄ ⊐*[b] ⦃G2, L2, T2⦄ → + ∃∃G,L0,T0. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G, L0, T0⦄ & ⦃G, L0, T0⦄ ≛[h, o] ⦃G2, L2, T2⦄. +#h #o #b #G1 #G #L1 #L #T1 #T #H1 #G2 #L2 #T2 #H2 +elim(ffdeq_inv_gen_dx … H1) -H1 #HG #HL1 #HT1 destruct +elim (lfdeq_fqus_trans … H2 … HL1) -L #L #T0 #H2 #HT02 #HL2 +elim (tdeq_fqus_trans … H2 … HT1) -T #L0 #T #H2 #HT0 #HL0 +lapply (tdeq_lfdeq_conf … HT02 … HL0) -HL0 #HL0 +/4 width=7 by ffdeq_intro_dx, lfdeq_trans, tdeq_trans, ex2_3_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqus.ma index f78c3e8eb..84685ca10 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqus.ma @@ -19,7 +19,7 @@ include "basic_2/static/lfdeq_lfdeq.ma". (* DEGREE-BASED EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ******) -(* Properties with supclosure ***********************************************) +(* Properties with extended structural successor for closures ***************) lemma fqu_tdeq_conf: ∀h,o,b,G1,G2,L1,L2,U1,T1. ⦃G1, L1, U1⦄ ⊐[b] ⦃G2, L2, T1⦄ → ∀U2. U1 ≛[h, o] U2 → @@ -53,7 +53,7 @@ elim (fqu_tdeq_conf … o … H12 U2) -H12 /3 width=5 by lfdeq_sym, tdeq_sym, ex3_2_intro/ qed-. -(* Basic_2A1: was just: lleq_fqu_trans *) +(* Basic_2A1: uses: lleq_fqu_trans *) lemma lfdeq_fqu_trans: ∀h,o,b,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐[b] ⦃G2, K2, U⦄ → ∀L1. L1 ≛[h, o, T] L2 → ∃∃K1,U0. ⦃G1, L1, T⦄ ⊐[b] ⦃G2, K1, U0⦄ & U0 ≛[h, o] U & K1 ≛[h, o, U] K2. @@ -78,6 +78,18 @@ lemma lfdeq_fqu_trans: ∀h,o,b,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐[b] ⦃G2, K ] qed-. +(* Properties with optional structural successor for closures ***************) + +lemma tdeq_fquq_trans: ∀h,o,b,G1,G2,L1,L2,U1,T1. ⦃G1, L1, U1⦄ ⊐⸮[b] ⦃G2, L2, T1⦄ → + ∀U2. U2 ≛[h, o] U1 → + ∃∃L,T2. ⦃G1, L1, U2⦄ ⊐⸮[b] ⦃G2, L, T2⦄ & T2 ≛[h, o] T1 & L ≛[h, o, T1] L2. +#h #o #b #G1 #G2 #L1 #L2 #U1 #T1 #H elim H -H +[ #H #U2 #HU21 elim (tdeq_fqu_trans … H … HU21) -U1 + /3 width=5 by fqu_fquq, ex3_2_intro/ +| * #HG #HL #HT destruct /2 width=5 by ex3_2_intro/ +] +qed-. + (* Basic_2A1: was just: lleq_fquq_trans *) lemma lfdeq_fquq_trans: ∀h,o,b,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐⸮[b] ⦃G2, K2, U⦄ → ∀L1. L1 ≛[h, o, T] L2 → @@ -88,6 +100,8 @@ lemma lfdeq_fquq_trans: ∀h,o,b,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐⸮[b] ⦃G ] qed-. +(* Properties with plus-iterated structural successor for closures **********) + (* Basic_2A1: was just: lleq_fqup_trans *) lemma lfdeq_fqup_trans: ∀h,o,b,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐+[b] ⦃G2, K2, U⦄ → ∀L1. L1 ≛[h, o, T] L2 → @@ -104,6 +118,33 @@ lemma lfdeq_fqup_trans: ∀h,o,b,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐+[b] ⦃G2, ] qed-. +lemma tdeq_fqup_trans: ∀h,o,b,G1,G2,L1,L2,U1,T1. ⦃G1, L1, U1⦄ ⊐+[b] ⦃G2, L2, T1⦄ → + ∀U2. U2 ≛[h, o] U1 → + ∃∃L,T2. ⦃G1, L1, U2⦄ ⊐+[b] ⦃G2, L, T2⦄ & T2 ≛[h, o] T1 & L ≛[h, o, T1] L2. +#h #o #b #G1 #G2 #L1 #L2 #U1 #T1 #H @(fqup_ind_dx … H) -G1 -L1 -U1 +[ #G1 #L1 #U1 #H #U2 #HU21 elim (tdeq_fqu_trans … H … HU21) -U1 + /3 width=5 by fqu_fqup, ex3_2_intro/ +| #G1 #G #L1 #L #U1 #U #H #_ #IH #U2 #HU21 + elim (tdeq_fqu_trans … H … HU21) -U1 #L0 #T #H1 #HTU #HL0 + lapply (tdeq_lfdeq_div … HTU … HL0) -HL0 #HL0 + elim (IH … HTU) -U #K2 #U1 #H2 #HUT1 #HKL2 + elim (lfdeq_fqup_trans … H2 … HL0) -L #K #U #H2 #HU1 #HK2 + lapply (tdeq_lfdeq_conf … HUT1 … HK2) -HK2 #HK2 + /3 width=7 by lfdeq_trans, fqup_strap2, tdeq_trans, ex3_2_intro/ +] +qed-. + +(* Properties with star-iterated structural successor for closures **********) + +lemma tdeq_fqus_trans: ∀h,o,b,G1,G2,L1,L2,U1,T1. ⦃G1, L1, U1⦄ ⊐*[b] ⦃G2, L2, T1⦄ → + ∀U2. U2 ≛[h, o] U1 → + ∃∃L,T2. ⦃G1, L1, U2⦄ ⊐*[b] ⦃G2, L, T2⦄ & T2 ≛[h, o] T1 & L ≛[h, o, T1] L2. +#h #o #b #G1 #G2 #L1 #L2 #U1 #T1 #H #U2 #HU21 elim(fqus_inv_fqup … H) -H +[ #H elim (tdeq_fqup_trans … H … HU21) -U1 /3 width=5 by fqup_fqus, ex3_2_intro/ +| * #HG #HL #HT destruct /2 width=5 by ex3_2_intro/ +] +qed-. + (* Basic_2A1: was just: lleq_fqus_trans *) lemma lfdeq_fqus_trans: ∀h,o,b,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐*[b] ⦃G2, K2, U⦄ → ∀L1. L1 ≛[h, o, T] 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 c7a9c21e6..4852da28e 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 @@ -93,7 +93,7 @@ table { ] [ { "parallel qrst-computation" * } { [ [ "" ] "fpbg ( ⦃?,?,?⦄ >≛[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fleq" + "fpbg_fpbs" + "fpbg_fpbg" * ] - [ [ "" ] "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_aaa" + "fpbs_fpb" + "fpbs_fpbs" * ] + [ [ "" ] "fpbs_alt" + "fpbs_aaa" + "fpbs_fpb" + "fpbs_fpbs" * ] } ] [ { "decomposed rt-computation" * } { @@ -106,15 +106,19 @@ table { } ] *) + [ { "uncounted context-sensitive parallel rst-computation" * } { + [ [ "for closures" ] "fpbs" + "( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_fqup" + "fpbs_fqus" + "fpbs_cpxs" + "fpbs_lfpxs" * ] + } + ] [ { "uncounted context-sensitive parallel rt-computation" * } { [ [ "refinement for lenvs on selected entries" ] "lsubsx" + "( ? ⊢ ? ⊆ⓧ[?,?,?] ? )" "lsubsx_lfsx" + "lsubsx_lsubsx" * ] [ [ "strongly normalizing for lenvs on referred entries" ] "lfsx" + "( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_drops" + "lfsx_fqup" + "lfsx_cpx" + "lfsx_cpxs" + "lfsx_lfpxs" + "lfsx_lfsx" * ] [ [ "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_fqus" + "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 referred entries" ] "lfpxs" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_ffdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lpxs" + "lfpxs_lfpxs" * ] [ [ "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" * ] + [ [ "for terms" ] "cpxs" + "( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_fqus" + "cpxs_lsubr" + "cpxs_lfdeq" + "cpxs_ffdeq" + "cpxs_aaa" + "cpxs_lpx" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ] } ] } @@ -138,7 +142,7 @@ table { ] [ { "uncounted context-sensitive parallel rt-transition" * } { [ [ "normal form for terms" ] "cnx" + "( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" + "cnx_cnx" * ] - [ [ "for lenvs on referred entries" ] "lfpx" + "( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_fsle" + "lfpx_lfdeq" + "lfpx_aaa" + "lfpx_lpx" + "lfpx_lfpx" * ] + [ [ "for lenvs on referred entries" ] "lfpx" + "( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fquq" + "lfpx_fqup" + "lfpx_fsle" + "lfpx_lfdeq" + "lfpx_aaa" + "lfpx_lpx" + "lfpx_lfpx" * ] [ [ "for lenvs on all entries" ] "lpx" + "( ⦃?,?⦄ ⊢ ⬈[?] ? )" * ] [ [ "for binders" ] "cpx_ext" + "( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" * ] [ [ "for terms" ] "cpx" + "( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfeq" + "cpx_lfdeq" * ] @@ -172,7 +176,7 @@ table { } ] [ { "degree-based equivalence" * } { - [ [ "for closures on referred entries" ] "ffdeq" + "( ⦃?,?,?⦄ ≛[?,?] ⦃?,?,?⦄ )" "ffdeq_fqup" + "ffdeq_ffdeq" * ] + [ [ "for closures on referred entries" ] "ffdeq" + "( ⦃?,?,?⦄ ≛[?,?] ⦃?,?,?⦄ )" "ffdeq_fqup" + "ffdeq_fqus" + "ffdeq_ffdeq" * ] [ [ "for lenvs on referred entries" ] "lfdeq" + "( ? ≛[?,?,?] ? )" "lfdeq_length" + "lfdeq_drops" + "lfdeq_fqup" + "lfdeq_fqus" + "lfdeq_lfeq" + "lfdeq_lfdeq" * ] } ]