From 654f0003b43c7b58d2fec8a8cd7184c190f180c3 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 7 Oct 2013 20:53:32 +0000 Subject: [PATCH] some improvements towards an alternative definition of fpbs ... --- .../lambdadelta/basic_2/computation/fpbs.ma | 2 +- .../basic_2/computation/fpbs_alt.ma | 19 +++++ .../lambdadelta/basic_2/reduction/cpx_lift.ma | 84 ++++++++++--------- .../basic_2/reduction/lpx_ldrop.ma | 18 ++++ 4 files changed, 81 insertions(+), 42 deletions(-) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma index ebebb4577..00f4a93aa 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma @@ -29,7 +29,7 @@ interpretation "'big tree' parallel computation (closure)" (* Basic eliminators ********************************************************) lemma fpbs_ind: ∀h,g,G1,L1,T1. ∀R:relation3 genv lenv term. R G1 L1 T1 → - (∀L,G2,G,L2,T,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≽[h, g] ⦃G2, L2, T2⦄ → R G L T → R G2 L2 T2) → + (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≽[h, g] ⦃G2, L2, T2⦄ → R G L T → R G2 L2 T2) → ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2. /3 width=8 by tri_TC_star_ind/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma index f04f3587f..26e945a93 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "basic_2/notation/relations/btpredstaralt_8.ma". +include "basic_2/computation/lpxs_cpxs.ma". include "basic_2/computation/fpbs_fpbs.ma". (* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) @@ -25,6 +26,24 @@ definition fpbsa: ∀h. sd h → tri_relation genv lenv term ≝ interpretation "'big tree' parallel computation (closure) alternative" 'BTPRedStarAlt h g G1 L1 T1 G2 L2 T2 = (fpbsa h g G1 L1 T1 G2 L2 T2). +(* Basic properties *********************************************************) + +lemma fpbsa_fpb_trans: ∀h,g,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≥≥[h, g] ⦃G, L, T⦄ → + ∀G2,L2,T2. ⦃G, L, T⦄ ≽[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥≥[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G #L1 #L #T1 #T * #L0 #T0 #H10 #HT0 #HL0 #G2 #L2 #T2 * -G2 -L2 -T2 +[ #G2 #L2 #T2 #H2 +| /4 width=7 by lpxs_cpx_trans, cpxs_trans, ex3_2_intro/ +| /3 width=7 by lpxs_strap1, ex3_2_intro/ +] + +(* Main properties **********************************************************) + +theorem fpbs_fpbsa: ∀h,g,G1,G2,L1,L2,T1,T2. + ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥≥[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind … H) -G2 -L2 -T2 +/2 width=5 by fpbsa_fpb_trans, ex3_2_intro/ +qed. + (* Main inversion lemmas ****************************************************) theorem fpbsa_inv_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma index 05ed4ce0c..72b624fd3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma @@ -24,16 +24,16 @@ include "basic_2/reduction/cpx.ma". lemma ssta_cpx: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 •[h, g] T2 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2. #h #g #G #L #T1 #T2 #l #H elim H -G -L -T1 -T2 -[ #G #L #k #H lapply (da_inv_sort … H) -H /2 width=2/ +[ /3 width=4 by cpx_sort, da_inv_sort/ | #G #L #K #V #U #W #i #HLK #_ #HWU #IHVW #H elim (da_inv_lref … H) -H * #K0 #V0 [| #l0 ] #HLK0 - lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H destruct /3 width=7/ + lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H destruct /3 width=7 by cpx_delta/ | #G #L #K #W #U #l0 #i #HLK #_ #HWU #H elim (da_inv_lref … H) -H * #K0 #W0 [| #l1 ] #HLK0 - lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H destruct /2 width=7/ -| #a #I #G #L #V #T #U #_ #IHTU #H lapply (da_inv_bind … H) -H /3 width=1/ -| #G #L #V #T #U #_ #IHTU #H lapply (da_inv_flat … H) -H /3 width=1/ -| #G #L #W #T #U #_ #IHTU #H lapply (da_inv_flat … H) -H /3 width=1/ + lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H destruct /2 width=7 by cpx_delta/ +| /4 width=2 by cpx_bind, da_inv_bind/ +| /4 width=3 by cpx_flat, da_inv_flat/ +| /4 width=3 by cpx_tau, da_inv_flat/ ] qed. @@ -45,94 +45,94 @@ lemma cpx_lift: ∀h,g,G. l_liftable (cpx h g G). >(lift_mono … H1 … H2) -H1 -H2 // | #G #K #k #l #Hkl #L #d #e #_ #U1 #H1 #U2 #H2 >(lift_inv_sort1 … H1) -U1 - >(lift_inv_sort1 … H2) -U2 /2 width=2/ + >(lift_inv_sort1 … H2) -U2 /2 width=2 by cpx_sort/ | #I #G #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #d #e #HLK #U1 #H #U2 #HWU2 elim (lift_inv_lref1 … H) * #Hid #H destruct [ elim (lift_trans_ge … HVW2 … HWU2) -W2 // plus_plus_comm_23 #HVU2 - lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K // -Hid /3 width=7/ + elim (ldrop_trans_le … HLK … HKV) -K /2 width=2 by lt_to_le/ #X #HLK #H + elim (ldrop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hid #K #Y #HKV #HVY #H destruct /3 width=9 by cpx_delta/ + | lapply (lift_trans_be … HVW2 … HWU2 ? ?) -W2 /2 width=1 by le_S/ >plus_plus_comm_23 #HVU2 + lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K /3 width=7 by cpx_delta/ ] | #a #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2 elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct - elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /4 width=5/ + elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /4 width=5 by cpx_bind, ldrop_skip/ | #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2 elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct - elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /3 width=6/ + elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /3 width=6 by cpx_flat/ | #G #K #V #T1 #T #T2 #_ #HT2 #IHT1 #L #d #e #HLK #U1 #H #U2 #HTU2 elim (lift_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct - elim (lift_conf_O1 … HTU2 … HT2) -T2 /4 width=5/ + elim (lift_conf_O1 … HTU2 … HT2) -T2 /4 width=5 by cpx_zeta, ldrop_skip/ | #G #K #V #T1 #T2 #_ #IHT12 #L #d #e #HLK #U1 #H #U2 #HTU2 - elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=5/ + elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=5 by cpx_tau/ | #G #K #V1 #V2 #T #_ #IHV12 #L #d #e #HLK #U1 #H #U2 #HVU2 - elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=5/ + elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=5 by cpx_ti/ | #a #G #K #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L #d #e #HLK #X1 #HX1 #X2 #HX2 elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct elim (lift_inv_bind1 … HX2) -HX2 #X #T3 #HX #HT23 #HX2 destruct - elim (lift_inv_flat1 … HX) -HX #W3 #V3 #HW23 #HV23 #HX destruct /4 width=5/ + elim (lift_inv_flat1 … HX) -HX #W3 #V3 #HW23 #HV23 #HX destruct /4 width=5 by cpx_beta, ldrop_skip/ | #a #G #K #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L #d #e #HLK #X1 #HX1 #X2 #HX2 elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct elim (lift_inv_bind1 … HX2) -HX2 #W3 #X #HW23 #HX #HX2 destruct elim (lift_inv_flat1 … HX) -HX #V3 #T3 #HV3 #HT23 #HX destruct - elim (lift_trans_ge … HV2 … HV3) -V2 // /4 width=5/ + elim (lift_trans_ge … HV2 … HV3) -V2 /4 width=5 by cpx_theta, ldrop_skip/ ] qed. lemma cpx_inv_lift1: ∀h,g,G. l_deliftable_sn (cpx h g G). #h #g #G #L #U1 #U2 #H elim H -G -L -U1 -U2 [ * #G #L #i #K #d #e #_ #T1 #H - [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3/ - | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3/ - | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3/ + [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by cpx_atom, lift_sort, ex2_intro/ + | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3 by cpx_atom, lift_lref_ge_minus, lift_lref_lt, ex2_intro/ + | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by cpx_atom, lift_gref, ex2_intro/ ] | #G #L #k #l #Hkl #K #d #e #_ #T1 #H - lapply (lift_inv_sort2 … H) -H #H destruct /3 width=3/ + lapply (lift_inv_sort2 … H) -H #H destruct /3 width=3 by cpx_sort, lift_sort, ex2_intro/ | #I #G #L #LV #V #V2 #W2 #i #HLV #HV2 #HVW2 #IHV2 #K #d #e #HLK #T1 #H elim (lift_inv_lref2 … H) -H * #Hid #H destruct [ elim (ldrop_conf_lt … HLK … HLV) -L // #L #U #HKL #HLV #HUV elim (IHV2 … HLV … HUV) -V #U2 #HUV2 #HU2 - elim (lift_trans_le … HUV2 … HVW2) -V2 // >minus_plus minus_plus plus_minus // plus_minus //