From: Ferruccio Guidi Date: Sun, 6 Oct 2013 15:05:04 +0000 (+0000) Subject: bug fix in big-tree reduction X-Git-Tag: make_still_working~1098 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1407456d2415e2872b97ae70cae05eb47c1995c5;p=helm.git bug fix in big-tree reduction --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma index 98a890ffe..5a7e77736 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "basic_2/notation/relations/btpredstarproper_8.ma". +include "basic_2/substitution/fsupp.ma". include "basic_2/reduction/fpbc.ma". include "basic_2/computation/fpbs.ma". @@ -69,7 +70,7 @@ qed-. lemma fsupp_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄. #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsupp_ind … L2 T2 H) -G2 -L2 -T2 -/3 width=5 by fsupp_fpbs, fpbc_fsup, fpbc_fpbg, fpbg_inj/ +/4 width=5 by fpbg_strap1, fpbc_fpbg, fpbc_fsup, fpb_fsupq, fsup_fsupq/ qed. lemma cpxs_fpbg: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma index dc8e8f185..ebebb4577 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/notation/relations/btpredstar_8.ma". -include "basic_2/substitution/fsupp.ma". +include "basic_2/substitution/fsups.ma". include "basic_2/reduction/fpb.ma". include "basic_2/computation/cpxs.ma". include "basic_2/computation/lpxs.ma". @@ -55,11 +55,10 @@ lemma fpbs_strap2: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. /2 width=5 by tri_TC_strap/ qed-. -(* Note: this is a general property of bi_TC *) -lemma fsupp_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → +lemma fsups_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsupp_ind … L2 T2 H) -G2 -L2 -T2 -/3 width=5 by fpb_fsup, tri_step, fpb_fpbs/ +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsups_ind … L2 T2 H) -G2 -L2 -T2 +/3 width=5 by fpb_fsupq, tri_step/ qed. lemma cpxs_fpbs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma new file mode 100644 index 000000000..f04f3587f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.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/notation/relations/btpredstaralt_8.ma". +include "basic_2/computation/fpbs_fpbs.ma". + +(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) + +(* Note: alternative definition of fpbs *) +definition fpbsa: ∀h. sd h → tri_relation genv lenv term ≝ + λh,g,G1,L1,T1,G2,L2,T2. + ∃∃L,T. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L, T⦄ & ⦃G2, L⦄ ⊢ T ➡*[h, g] T2 & ⦃G2, L⦄ ⊢ ➡*[h, g] L2. + +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). + +(* Main inversion lemmas ****************************************************) + +theorem fpbsa_inv_fpbs: ∀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 * +/4 width=5 by fpbs_trans, fsups_fpbs, cpxs_fpbs, lpxs_fpbs/ +qed-. 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 new file mode 100644 index 000000000..227a666f2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstaralt_8.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'BTPRedStarAlt $h $g $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma index 947c4eda3..734e7b597 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma @@ -13,15 +13,15 @@ (**************************************************************************) include "basic_2/notation/relations/btpred_8.ma". -include "basic_2/relocation/fsup.ma". +include "basic_2/relocation/fsupq.ma". include "basic_2/reduction/lpx.ma". (* "BIG TREE" PARALLEL REDUCTION FOR CLOSURES *******************************) inductive fpb (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝ -| fpb_fsup: ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → fpb h g G1 L1 T1 G2 L2 T2 -| fpb_cpx : ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T2 → fpb h g G1 L1 T1 G1 L1 T2 -| fpb_lpx : ∀L2. ⦃G1, L1⦄ ⊢ ➡[h, g] L2 → fpb h g G1 L1 T1 G1 L2 T1 +| fpb_fsupq: ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → fpb h g G1 L1 T1 G2 L2 T2 +| fpb_cpx : ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T2 → fpb h g G1 L1 T1 G1 L1 T2 +| fpb_lpx : ∀L2. ⦃G1, L1⦄ ⊢ ➡[h, g] L2 → fpb h g G1 L1 T1 G1 L2 T1 . interpretation diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc.ma index a485258ad..a2b62d2a1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "basic_2/notation/relations/btpredproper_8.ma". +include "basic_2/relocation/fsupq_alt.ma". include "basic_2/reduction/fpb.ma". (* "BIG TREE" PROPER PARALLEL REDUCTION FOR CLOSURES ************************) @@ -31,7 +32,7 @@ interpretation lemma fpbc_fpb: ∀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 * -G2 -L2 -T2 -/2 width=1 by fpb_fsup, fpb_cpx/ +/3 width=1 by fpb_fsupq, fpb_cpx, fsup_fsupq/ qed. lemma cpr_fpbc: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → @@ -44,7 +45,10 @@ lemma fpb_inv_fpbc: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ ∨ ∧∧ G1 = G2 & ⦃G1, L1⦄ ⊢ ➡[h, g] L2 & T1 = T2. #h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 -/3 width=1 by and3_intro, or_introl, or_intror, fpbc_fsup/ -#T2 #HT12 elim (term_eq_dec T1 T2) #H destruct -/4 width=1 by and3_intro, or_introl, or_intror, fpbc_cpx/ +/3 width=1 by and3_intro, or_intror/ +[ #G2 #L2 #T2 #H elim (fsupq_inv_gen … H) -H [| * ] + /3 width=1 by fpbc_fsup, and3_intro, or_introl, or_intror/ +| #T2 #HT12 elim (term_eq_dec T1 T2) #H destruct + /4 width=1 by and3_intro, or_introl, or_intror, fpbc_cpx/ +] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq_alt.ma index e9bc6c533..54e161f7f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq_alt.ma @@ -33,19 +33,29 @@ lemma fsupqa_ldrop: ∀G1,G2,K1,K2,T1,T2. ⦃G1, K1, T1⦄ ⊃⊃⸮ ⦃G2, K2, ∀L1,d,e. ⇩[d, e] L1 ≡ K1 → ∀U1. ⇧[d, e] T1 ≡ U1 → ⦃G1, L1, U1⦄ ⊃⊃⸮ ⦃G2, K2, T2⦄. #G1 #G2 #K1 #K2 #T1 #T2 * [ /3 width=7/ ] * #H1 #H2 #H3 destruct -#L1 #d #e #HLK #U1 #HTU elim (eq_or_gt e) [2: /3 width=5/ ] #H destruct +#L1 #d #e #HLK #U1 #HTU elim (eq_or_gt e) +/3 width=5 by fsup_ldrop_lt, or_introl/ #H destruct >(ldrop_inv_O2 … HLK) -L1 >(lift_inv_O2 … HTU) -T2 -d // qed. (* Main properties **********************************************************) theorem fsupq_fsupqa: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃⊃⸮ ⦃G2, L2, T2⦄. -#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 // /2 width=1/ /2 width=7/ +#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 +/2 width=7 by fsupqa_ldrop, fsup_lref_O, fsup_pair_sn, fsup_bind_dx, fsup_flat_dx, or_introl/ qed. (* Main inversion properties ************************************************) theorem fsupqa_inv_fsupq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⊃⸮ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄. -#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -H /2 width=1/ +#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -H /2 width=1 by fsup_fsupq/ * #H1 #H2 #H3 destruct // qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma fsupq_inv_gen: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → +⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ ∨ (∧∧ G1 = G2 & L1 = L2 & T1 = T2). +#G1 #G2 #L1 #L2 #T1 #T2 #H elim (fsupq_fsupqa … H) -H [| * ] +/2 width=1 by or_introl/ +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 a7ffa62aa..c5f04455d 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 @@ -86,7 +86,7 @@ table { ] [ { "\"big tree\" parallel computation" * } { [ "fpbg ( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fpbg" * ] - [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_fpbs" * ] + [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_fpbs" * ] } ] [ { "decomposed extended computation" * } {