From 65ebca171de29dd33be87b4b063385d1f6b9ce70 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 15 Dec 2013 13:48:17 +0000 Subject: [PATCH] eliminators of arited terms based on "big tree" proper computation --- .../basic_2/computation/fpbs_aaa.ma | 27 ++++++++ .../basic_2/computation/fsb_aaa.ma | 48 +++++++++++--- .../lambdadelta/basic_2/reduction/fpb_aaa.ma | 27 ++++++++ .../lambdadelta/basic_2/static/aaa_fqus.ma | 63 +++++++++++++++++++ .../lambdadelta/basic_2/static/aaa_lift.ma | 28 ++++----- .../lambdadelta/basic_2/web/basic_2_src.tbl | 6 +- 6 files changed, 173 insertions(+), 26 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_aaa.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_aaa.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/static/aaa_fqus.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_aaa.ma new file mode 100644 index 000000000..7cef76336 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_aaa.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reduction/fpb_aaa.ma". +include "basic_2/computation/fpbs.ma". + +(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) + +(* Properties on atomic arity assignment for terms **************************) + +lemma aaa_fpbs_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → + ∀A1. ⦃G1, L1⦄ ⊢ T1 ⁝ A1 → ∃A2. ⦃G2, L2⦄ ⊢ T2 ⁝ A2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind … H) -G2 -L2 -T2 /2 width=2 by ex_intro/ +#G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #A #HA elim (IH1 … HA) -IH1 -A +/2 width=8 by aaa_fpb_conf/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma index 49b11f971..1074ef74d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "basic_2/computation/fpbs_aaa.ma". include "basic_2/computation/csx_aaa.ma". include "basic_2/computation/fsb_csx.ma". @@ -28,14 +29,43 @@ theorem aaa_fsba: ∀h,g,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ ⦥ /3 width=2 by fsb_fsba, aaa_fsb/ qed. (* Advanced eliminators on atomica arity assignment for terms ***************) -(* -fact aaa_ind_fpbu: ∀h,g. ∀R:relation3 genv lenv term. - (∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A → - (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) → - R G1 L1 T1 - ) → - ∀G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ∀A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T. + +fact aaa_ind_fpbu_aux: ∀h,g. ∀R:relation3 genv lenv term. + (∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A → + (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) → + R G1 L1 T1 + ) → + ∀G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ∀A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T. #h #g #R #IH #G #L #T #H @(csx_ind_fpbu … H) -G -L -T #G1 #L1 #T1 #H1 #IH1 #A1 #HTA1 @IH -IH // -#G2 #L2 #T2 #H12 @IH1 // -*) +#G2 #L2 #T2 #H12 elim (aaa_fpbs_conf h g … G2 … L2 … T2 … HTA1) -A1 +/2 width=2 by fpbu_fwd_fpbs/ +qed-. + +lemma aaa_ind_fpbu: ∀h,g. ∀R:relation3 genv lenv term. + (∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A → + (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) → + R G1 L1 T1 + ) → + ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T. +/4 width=4 by aaa_ind_fpbu_aux, aaa_csx/ qed-. + +fact aaa_ind_fpbg_aux: ∀h,g. ∀R:relation3 genv lenv term. + (∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A → + (∀G2,L2,T2. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) → + R G1 L1 T1 + ) → + ∀G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ∀A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T. +#h #g #R #IH #G #L #T #H @(csx_ind_fpbg … H) -G -L -T +#G1 #L1 #T1 #H1 #IH1 #A1 #HTA1 @IH -IH // +#G2 #L2 #T2 #H12 elim (aaa_fpbs_conf h g … G2 … L2 … T2 … HTA1) -A1 +/2 width=2 by fpbg_fwd_fpbs/ +qed-. + +lemma aaa_ind_fpbg: ∀h,g. ∀R:relation3 genv lenv term. + (∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A → + (∀G2,L2,T2. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) → + R G1 L1 T1 + ) → + ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T. +/4 width=4 by aaa_ind_fpbg_aux, aaa_csx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_aaa.ma new file mode 100644 index 000000000..d61a11ae0 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_aaa.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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/aaa_fqus.ma". +include "basic_2/reduction/lpx_aaa.ma". +include "basic_2/reduction/fpb.ma". + +(* "BIG TREE" PARALLEL REDUCTION FOR CLOSURES *******************************) + +(* Properties on atomic arity assignment for terms **************************) + +lemma aaa_fpb_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ → + ∀A1. ⦃G1, L1⦄ ⊢ T1 ⁝ A1 → ∃A2. ⦃G2, L2⦄ ⊢ T2 ⁝ A2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 +/3 width=6 by aaa_lpx_conf, aaa_cpx_conf, aaa_fquq_conf, ex_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_fqus.ma new file mode 100644 index 000000000..cc3777262 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_fqus.ma @@ -0,0 +1,63 @@ +(**************************************************************************) +(* ___ *) +(* ||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/substitution/fqus_alt.ma". +include "basic_2/static/aaa_lift.ma". + +(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************) + +(* Properties on supclosure *************************************************) + +lemma aaa_fqu_conf: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → + ∀A1. ⦃G1, L1⦄ ⊢ T1 ⁝ A1 → ∃A2. ⦃G2, L2⦄ ⊢ T2 ⁝ A2. +#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 +[ #I #G #L #T #A #H elim (aaa_inv_lref … H) -H + #J #K #V #H #HA lapply (ldrop_inv_O2 … H) -H + #H destruct /2 width=2 by ex_intro/ +| * [ #a ] * #G #L #V #T #X #H + [ elim (aaa_inv_abbr … H) + | elim (aaa_inv_abst … H) + | elim (aaa_inv_appl … H) + | elim (aaa_inv_cast … H) + ] -H /2 width=2 by ex_intro/ +| #a * #G #L #V #T #X #H + [ elim (aaa_inv_abbr … H) + | elim (aaa_inv_abst … H) + ] -H /2 width=2 by ex_intro/ +| * #G #L #V #T #X #H + [ elim (aaa_inv_appl … H) + | elim (aaa_inv_cast … H) + ] -H /2 width=2 by ex_intro/ +| /3 width=8 by aaa_inv_lift, ex_intro/ +] +qed-. + +lemma aaa_fquq_conf: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → + ∀A1. ⦃G1, L1⦄ ⊢ T1 ⁝ A1 → ∃A2. ⦃G2, L2⦄ ⊢ T2 ⁝ A2. +#G1 #G2 #L1 #L2 #T1 #T2 #H elim(fquq_inv_gen … H) -H /2 width=6 by aaa_fqu_conf/ +* #H1 #H2 #H3 destruct /2 width=2 by ex_intro/ +qed-. + +lemma aaa_fqup_conf: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → + ∀A1. ⦃G1, L1⦄ ⊢ T1 ⁝ A1 → ∃A2. ⦃G2, L2⦄ ⊢ T2 ⁝ A2. +#G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 +[2: #G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #A #HA elim (IH1 … HA) -IH1 -A ] +/2 width=6 by aaa_fqu_conf/ +qed-. + +lemma aaa_fqus_conf: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → + ∀A1. ⦃G1, L1⦄ ⊢ T1 ⁝ A1 → ∃A2. ⦃G2, L2⦄ ⊢ T2 ⁝ A2. +#G1 #G2 #L1 #L2 #T1 #T2 #H elim(fqus_inv_gen … H) -H /2 width=6 by aaa_fqup_conf/ +* #H1 #H2 #H3 destruct /2 width=2 by ex_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lift.ma index bcbb5c207..ea039002f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lift.ma @@ -17,7 +17,7 @@ include "basic_2/static/aaa.ma". (* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************) -(* Properties concerning basic relocation ***********************************) +(* Properties on basic relocation *******************************************) lemma aaa_lift: ∀G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 → ∀T2. ⇧[d, e] T1 ≡ T2 → ⦃G, L2⦄ ⊢ T2 ⁝ A. @@ -26,23 +26,23 @@ lemma aaa_lift: ∀G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A → ∀L2,d,e. ⇩[d, e] >(lift_inv_sort1 … H) -H // | #I #G #L1 #K1 #V1 #B #i #HLK1 #_ #IHB #L2 #d #e #HL21 #T2 #H elim (lift_inv_lref1 … H) -H * #Hid #H destruct - [ elim (ldrop_trans_le … HL21 … HLK1) -L1 /2 width=2/ #X #HLK2 #H - elim (ldrop_inv_skip2 … H) -H /2 width=1/ -Hid #K2 #V2 #HK21 #HV12 #H destruct + [ elim (ldrop_trans_le … HL21 … HLK1) -L1 /2 width=2 by lt_to_le/ #X #HLK2 #H + elim (ldrop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hid #K2 #V2 #HK21 #HV12 #H destruct /3 width=8/ - | lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/ + | lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 /3 width=8 by aaa_lref/ ] | #a #G #L1 #V1 #T1 #B #A #_ #_ #IHB #IHA #L2 #d #e #HL21 #X #H elim (lift_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct - /4 width=4/ + /4 width=4 by aaa_abbr, ldrop_skip/ | #a #G #L1 #V1 #T1 #B #A #_ #_ #IHB #IHA #L2 #d #e #HL21 #X #H elim (lift_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct - /4 width=4/ + /4 width=4 by aaa_abst, ldrop_skip/ | #G #L1 #V1 #T1 #B #A #_ #_ #IHB #IHA #L2 #d #e #HL21 #X #H elim (lift_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct - /3 width=4/ + /3 width=4 by aaa_appl/ | #G #L1 #V1 #T1 #A #_ #_ #IH1 #IH2 #L2 #d #e #HL21 #X #H elim (lift_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct - /3 width=4/ + /3 width=4 by aaa_cast/ ] qed. @@ -53,20 +53,20 @@ lemma aaa_inv_lift: ∀G,L2,T2,A. ⦃G, L2⦄ ⊢ T2 ⁝ A → ∀L1,d,e. ⇩[d, >(lift_inv_sort2 … H) -H // | #I #G #L2 #K2 #V2 #B #i #HLK2 #_ #IHB #L1 #d #e #HL21 #T1 #H elim (lift_inv_lref2 … H) -H * #Hid #H destruct - [ elim (ldrop_conf_lt … HL21 … HLK2) -L2 // -Hid /3 width=8/ - | lapply (ldrop_conf_ge … HL21 … HLK2 ?) -L2 // -Hid /3 width=8/ + [ elim (ldrop_conf_lt … HL21 … HLK2) -L2 /3 width=8 by aaa_lref/ + | lapply (ldrop_conf_ge … HL21 … HLK2 ?) -L2 /3 width=8 by aaa_lref/ ] | #a #G #L2 #V2 #T2 #B #A #_ #_ #IHB #IHA #L1 #d #e #HL21 #X #H elim (lift_inv_bind2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct - /4 width=4/ + /4 width=4 by aaa_abbr, ldrop_skip/ | #a #G #L2 #V2 #T2 #B #A #_ #_ #IHB #IHA #L1 #d #e #HL21 #X #H elim (lift_inv_bind2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct - /4 width=4/ + /4 width=4 by aaa_abst, ldrop_skip/ | #G #L2 #V2 #T2 #B #A #_ #_ #IHB #IHA #L1 #d #e #HL21 #X #H elim (lift_inv_flat2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct - /3 width=4/ + /3 width=4 by aaa_appl/ | #G #L2 #V2 #T2 #A #_ #_ #IH1 #IH2 #L1 #d #e #HL21 #X #H elim (lift_inv_flat2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct - /3 width=4/ + /3 width=4 by aaa_cast/ ] 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 48a2983e9..4f3d0f8dd 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 { [ "fpbg ( ⦃?,?,?⦄ >⋕[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fpns" + "fpbg_fpbg" * ] [ "fpbc ( ⦃?,?,?⦄ ≻⋕[?,?] ⦃?,?,?⦄ )" "fpbc_fpns" + "fpbc_fpbs" * ] [ "fpbu ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpbu_lift" + "fpbu_fpns" * ] - [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_fpns" + "fpbs_fpbs" * ] + [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_aaa" + "fpbs_fpns" + "fpbs_fpbs" * ] } ] [ { "parallel computation for \"big tree\" normal forms" * } { @@ -127,7 +127,7 @@ table { class "water" [ { "reduction" * } { [ { "\"big tree\" parallel reduction" * } { - [ "fpb ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )" "fpb_lift" * ] + [ "fpb ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )" "fpb_lift" + "fpb_aaa" * ] } ] [ { "context-sensitive extended normal forms" * } { @@ -185,7 +185,7 @@ table { } ] [ { "atomic arity assignment" * } { - [ "aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_lift" + "aaa_lifts" + "aaa_da" + "aaa_ssta" + "aaa_aaa" * ] + [ "aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_lift" + "aaa_lifts" + "aaa_fqus" + "aaa_da" + "aaa_ssta" + "aaa_aaa" * ] } ] [ { "stratified static type assignment" * } { -- 2.39.2