From 9afdb35b870c15760f482a1b4a0ad7b4dcd5172b Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 4 Oct 2014 20:42:40 +0000 Subject: [PATCH] - nnAuto: we catch TypeCheckerFailure generated at the end of smart_apply (rel out of context) during equational reasoning, and we treat it as an Error. TO BE UNDERSTTOD (this TypeCheckerFailure dramatically interferes with automatic proof search in \lambda\delta) - lambdadelta: new definition of fpbg without fpbc + some refactoring --- matita/components/ng_tactics/nnAuto.ml | 4 + .../lambdadelta/basic_2/computation/fpbg.ma | 46 +++------- .../basic_2/computation/fpbg_fleq.ma | 55 ++++++++++-- .../basic_2/computation/fpbg_fpbg.ma | 35 +------- .../basic_2/computation/fpbg_fpbs.ma | 46 +++------- .../basic_2/computation/fpbg_lift.ma | 4 +- .../lambdadelta/basic_2/computation/fpbs.ma | 36 ++++---- .../basic_2/computation/fpbs_aaa.ma | 4 +- .../basic_2/computation/fpbs_alt.ma | 2 +- .../computation/{fpbs_fpbu.ma => fpbs_fpb.ma} | 35 +------- .../basic_2/computation/fpbs_lift.ma | 5 +- .../lambdadelta/basic_2/computation/fsb.ma | 4 +- .../basic_2/computation/fsb_aaa.ma | 2 +- .../basic_2/computation/fsb_alt.ma | 7 +- .../basic_2/computation/fsb_csx.ma | 2 + .../lambdadelta/basic_2/etc/fleq/fpbs.etc | 27 ++++++ .../{reduction/fpbc.ma => etc/fpbc/fpbc.etc} | 0 .../fpbc_fleq.ma => etc/fpbc/fpbc_fleq.etc} | 0 .../lambdadelta/basic_2/etc/fpbc/fpbg.etc | 61 +++++++++++++ .../fpbg_lift.etc => fpbc/fpbg_fleq.etc} | 26 ++++-- .../basic_2/etc/fpbc/fpbg_fpbg.etc | 53 +++++++++++ .../basic_2/etc/fpbc/fpbg_fpbs.etc | 88 +++++++++++++++++++ .../fpbs_fleq.ma => etc/fpbc/fpbg_lift.etc} | 13 ++- .../fpbs_fpbc.ma => etc/fpbc/fpbs_fpbc.etc} | 0 .../fpbc/lazybtpredproper_8.etc} | 0 .../lambdadelta/basic_2/etc/fpbg/fpbg.etc | 40 --------- .../basic_2/etc/fpbg/fpbg_fpbg.etc | 57 ------------ .../basic_2/etc/fpbg/fpbg_fpns.etc | 34 ------- .../relations/btpredalt_8.ma} | 4 +- .../lambdadelta/basic_2/reduction/fpb.ma | 26 +++--- .../reduction/{fpbu_fleq.ma => fpb_fleq.ma} | 31 +++---- .../lambdadelta/basic_2/reduction/fpb_lift.ma | 13 +-- .../reduction/{fpbu_lleq.ma => fpb_lleq.ma} | 14 +-- .../lambdadelta/basic_2/reduction/fpbq.ma | 42 +++++++++ .../reduction/{fpb_aaa.ma => fpbq_aaa.ma} | 6 +- .../reduction/{fpbu_lift.ma => fpbq_lift.ma} | 15 ++-- .../lambdadelta/basic_2/reduction/fpbu.ma | 46 ---------- .../lambdadelta/basic_2/substitution/fqu.ma | 14 +++ .../lambdadelta/basic_2/web/basic_2.ldw.xml | 4 +- 39 files changed, 476 insertions(+), 425 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/computation/{fpbs_fpbu.ma => fpbs_fpb.ma} (60%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction/fpbc.ma => etc/fpbc/fpbc.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction/fpbc_fleq.ma => etc/fpbc/fpbc_fleq.etc} (100%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/fpbc/fpbg.etc rename matita/matita/contribs/lambdadelta/basic_2/etc/{fpbg/fpbg_lift.etc => fpbc/fpbg_fleq.etc} (54%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/fpbc/fpbg_fpbg.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/fpbc/fpbg_fpbs.etc rename matita/matita/contribs/lambdadelta/basic_2/{computation/fpbs_fleq.ma => etc/fpbc/fpbg_lift.etc} (75%) rename matita/matita/contribs/lambdadelta/basic_2/{computation/fpbs_fpbc.ma => etc/fpbc/fpbs_fpbc.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/lazybtpredproper_8.ma => etc/fpbc/lazybtpredproper_8.etc} (100%) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg_fpbg.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg_fpns.etc rename matita/matita/contribs/lambdadelta/basic_2/{etc/fpbg/btpredstarproper_8.etc => notation/relations/btpredalt_8.ma} (87%) rename matita/matita/contribs/lambdadelta/basic_2/reduction/{fpbu_fleq.ma => fpb_fleq.ma} (56%) rename matita/matita/contribs/lambdadelta/basic_2/reduction/{fpbu_lleq.ma => fpb_lleq.ma} (76%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/reduction/fpbq.ma rename matita/matita/contribs/lambdadelta/basic_2/reduction/{fpb_aaa.ma => fpbq_aaa.ma} (86%) rename matita/matita/contribs/lambdadelta/basic_2/reduction/{fpbu_lift.ma => fpbq_lift.ma} (71%) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/reduction/fpbu.ma diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml index 25274de81..c42ab8b27 100644 --- a/matita/components/ng_tactics/nnAuto.ml +++ b/matita/components/ng_tactics/nnAuto.ml @@ -632,6 +632,10 @@ let smart_apply t unit_eq status g = | NCicEnvironment.ObjectNotFound s as e -> raise (Error (lazy "eq_coerc non yet defined",Some e)) | Error _ as e -> debug_print (lazy "error"); raise e +(* FG: for now we catch TypeCheckerFailure; to be understood *) + | NCicTypeChecker.TypeCheckerFailure _ -> + debug_print (lazy "TypeCheckerFailure"); + raise (Error (lazy "no proof found",None)) ;; let compare_statuses ~past ~present = diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma index 574c35e10..5c8a6bd20 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma @@ -13,49 +13,27 @@ (**************************************************************************) include "basic_2/notation/relations/lazybtpredstarproper_8.ma". -include "basic_2/reduction/fpbc.ma". +include "basic_2/reduction/fpb.ma". +include "basic_2/computation/fpbs.ma". (* "QRST" PROPER PARALLEL COMPUTATION FOR CLOSURES **************************) definition fpbg: ∀h. sd h → tri_relation genv lenv term ≝ - λh,g. tri_TC … (fpbc h g). + λh,g,G1,L1,T1,G2,L2,T2. + ∃∃G,L,T. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G, L, T⦄ & ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄. interpretation "'qrst' proper parallel computation (closure)" 'LazyBTPRedStarProper h g G1 L1 T1 G2 L2 T2 = (fpbg h g G1 L1 T1 G2 L2 T2). (* Basic properties *********************************************************) -lemma fpbc_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻≡[h, g] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄. -/2 width=1 by tri_inj/ qed. +lemma fpb_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄. +/2 width=5 by ex2_3_intro/ qed. -lemma fpbg_strap1: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. - ⦃G1, L1, T1⦄ >≡[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≻≡[h, g] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄. -/2 width=5 by tri_step/ qed. - -lemma fpbg_strap2: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. - ⦃G1, L1, T1⦄ ≻≡[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ >≡[h, g] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄. -/2 width=5 by tri_TC_strap/ qed. - -lemma fpbu_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h,g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄. -/3 width=1 by fpbu_fpbc, fpbc_fpbg/ qed. - -(* Basic eliminators ********************************************************) - -lemma fpbg_ind: ∀h,g,G1,L1,T1. ∀R:relation3 …. - (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻≡[h, g] ⦃G2, L2, T2⦄ → 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. -#h #g #G1 #L1 #T1 #R #IH1 #IH2 #G2 #L2 #T2 #H -@(tri_TC_ind … IH1 IH2 G2 L2 T2 H) -qed-. - -lemma fpbg_ind_dx: ∀h,g,G2,L2,T2. ∀R:relation3 …. - (∀G1,L1,T1. ⦃G1, L1, T1⦄ ≻≡[h, g] ⦃G2, L2, T2⦄ → R G1 L1 T1) → - (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≻≡[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ >≡[h, g] ⦃G2, L2, T2⦄ → R G L T → R G1 L1 T1) → - ∀G1,L1,T1. ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄ → R G1 L1 T1. -#h #g #G2 #L2 #T2 #R #IH1 #IH2 #G1 #L1 #T1 #H -@(tri_TC_ind_dx … IH1 IH2 G1 L1 T1 H) +lemma fpbg_fpbq_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. + ⦃G1, L1, T1⦄ >≡[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≽[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 * +/3 width=9 by fpbs_strap1, ex2_3_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fleq.ma index 754811ec2..b4b7fb223 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fleq.ma @@ -12,7 +12,8 @@ (* *) (**************************************************************************) -include "basic_2/reduction/fpbc_fleq.ma". +include "basic_2/multiple/fleq_fleq.ma". +include "basic_2/reduction/fpbq_alt.ma". include "basic_2/computation/fpbg.ma". (* "QRST" PROPER PARALLEL COMPUTATION FOR CLOSURES **************************) @@ -21,16 +22,52 @@ include "basic_2/computation/fpbg.ma". lemma fpbg_fleq_trans: ∀h,g,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ >≡[h, g] ⦃G, L, T⦄ → ∀G2,L2,T2. ⦃G, L, T⦄ ≡[0] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G #L1 #L #T1 #T #H @(fpbg_ind … H) -G -L -T -[ /3 width=5 by fpbc_fpbg, fpbc_fleq_trans/ -| /4 width=9 by fpbg_strap1, fpbc_fleq_trans/ -] -qed-. +/3 width=5 by fpbg_fpbq_trans, fleq_fpbq/ qed-. lemma fleq_fpbg_trans: ∀h,g,G,G2,L,L2,T,T2. ⦃G, L, T⦄ >≡[h, g] ⦃G2, L2, T2⦄ → ∀G1,L1,T1. ⦃G1, L1, T1⦄ ≡[0] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄. -#h #g #G #G2 #L #L2 #T #T2 #H @(fpbg_ind_dx … H) -G -L -T -[ /3 width=5 by fpbc_fpbg, fleq_fpbc_trans/ -| /4 width=9 by fpbg_strap2, fleq_fpbc_trans/ +#h #g #G #G2 #L #L2 #T #T2 * #G0 #L0 #T0 #H0 #H02 #G1 #L1 #T1 #H1 +elim (fleq_fpb_trans … H1 … H0) -G -L -T +/4 width=9 by fpbs_strap2, fleq_fpbq, ex2_3_intro/ +qed-. + +(* alternative definition of fpbs *******************************************) + +lemma fleq_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. + ⦃G1, L1, T1⦄ ≡[0] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 * /2 width=1 by lleq_fpbs/ +qed. + +lemma fpbg_fwd_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 * +/3 width=5 by fpbs_strap2, fpb_fpbq/ +qed-. + +lemma fpbs_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ≡[0] ⦃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=1 by or_introl/ +| #G #G2 #L #L2 #T #T2 #_ #H2 * #H1 @(fpbq_ind_alt … H2) -H2 #H2 + [ /3 width=5 by fleq_trans, or_introl/ + | elim (fleq_fpb_trans … H1 … H2) -G -L -T + /4 width=5 by ex2_3_intro, or_intror, fleq_fpbs/ + | /3 width=5 by fpbg_fleq_trans, or_intror/ + | /4 width=5 by fpbg_fpbq_trans, fpb_fpbq, or_intror/ + ] +] +qed-. + +(* Advanced properties of "qrst" parallel computation on closures ***********) + +lemma fpbs_fpbu_trans: ∀h,g,F1,F2,K1,K2,T1,T2. ⦃F1, K1, T1⦄ ≥[h, g] ⦃F2, K2, T2⦄ → + ∀G2,L2,U2. ⦃F2, K2, T2⦄ ≻[h, g] ⦃G2, L2, U2⦄ → + ∃∃G1,L1,U1. ⦃F1, K1, T1⦄ ≻[h, g] ⦃G1, L1, U1⦄ & ⦃G1, L1, U1⦄ ≥[h, g] ⦃G2, L2, U2⦄. +#h #g #F1 #F2 #K1 #K2 #T1 #T2 #H elim (fpbs_fpbg … H) -H +[ #H12 #G2 #L2 #U2 #H2 elim (fleq_fpb_trans … H12 … H2) -F2 -K2 -T2 + /3 width=5 by fleq_fpbs, ex2_3_intro/ +| * #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 + @(ex2_3_intro … H4) -H4 /3 width=5 by fpbs_strap1, fpb_fpbq/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma index 57dd5ebb4..bbbcc2487 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma @@ -12,42 +12,11 @@ (* *) (**************************************************************************) -include "basic_2/computation/fpbs_fpbu.ma". -include "basic_2/computation/fpbs_fpbc.ma". -include "basic_2/computation/fpbs_fpbs.ma". include "basic_2/computation/fpbg_fpbs.ma". (* "QRST" PROPER PARALLEL COMPUTATION FOR CLOSURES **************************) -(* Advanced inversion lemmas ************************************************) - -lemma fpbg_inv_fpbu_sn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄ → - ∃∃G,L,T. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G, L, T⦄ & ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbg_ind_dx … H) -G1 -L1 -T1 -[ #G1 #L1 #T1 * /3 width=5 by fleq_fpbs, ex2_3_intro/ -| #G1 #G #L1 #L #T1 #T * - #G0 #L0 #T0 #H10 #H0 #_ * - /5 width=9 by fpbu_fpbs, fpbs_trans, fleq_fpbs, ex2_3_intro/ -] -qed-. - -(* Advanced forward lemmas **************************************************) - -lemma fpbg_fwd_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 #H @(fpbg_ind … H) -G2 -L2 -T2 -[2: #G #G2 #L #L2 #T #T2 #_ #H2 #IH1 @(fpbs_trans … IH1) -IH1 ] (**) (* full auto fails *) -/2 width=1 by fpbc_fpbs/ -qed-. - -(* Advanced properties ******************************************************) - -lemma fpbs_fpbu_trans: ∀h,g,F1,F2,K1,K2,T1,T2. ⦃F1, K1, T1⦄ ≥[h, g] ⦃F2, K2, T2⦄ → - ∀G2,L2,U2. ⦃F2, K2, T2⦄ ≻[h, g] ⦃G2, L2, U2⦄ → - ∃∃G1,L1,U1. ⦃F1, K1, T1⦄ ≻[h, g] ⦃G1, L1, U1⦄ & ⦃G1, L1, U1⦄ ≥[h, g] ⦃G2, L2, U2⦄. -/5 width=5 by fpbg_inv_fpbu_sn, fpbs_fpbg_trans, fpbc_fpbg, fpbu_fpbc/ qed-. - -(* Man properties ***********************************************************) +(* Main properties **********************************************************) theorem fpbg_trans: ∀h,g. tri_transitive … (fpbg h g). -/2 width=5 by tri_TC_transitive/ qed-. +/3 width=5 by fpbg_fpbs_trans, fpbg_fwd_fpbs/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbs.ma index 4b8662295..b5a303df6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbs.ma @@ -20,47 +20,41 @@ include "basic_2/computation/fpbg_fleq.ma". (* Properties on "qrst" parallel reduction on closures **********************) -lemma fpbg_fpb_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. - ⦃G1, L1, T1⦄ >≡[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≽[h, g] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2 elim (fpb_fpbu … H2) -H2 -/3 width=5 by fpbg_fleq_trans, fpbg_strap1, fpbu_fpbc/ -qed-. - lemma fpb_fpbg_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. - ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ >≡[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ≻[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ >≡[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 elim (fpb_fpbu … H1) -H1 -/3 width=5 by fleq_fpbg_trans, fpbg_strap2, fpbu_fpbc/ +/3 width=5 by fpbg_fwd_fpbs, ex2_3_intro/ qed-. + +lemma fpbq_fpbg_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. + ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ >≡[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2 @(fpbq_ind_alt … H1) -H1 +/2 width=5 by fleq_fpbg_trans, fpb_fpbg_trans/ qed-. (* Properties on "qrst" parallel compuutation on closures *******************) lemma fpbs_fpbg_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 #H @(fpbs_ind … H) -G -L -T /3 width=5 by fpb_fpbg_trans/ +#h #g #G1 #G #L1 #L #T1 #T #H @(fpbs_ind … H) -G -L -T /3 width=5 by fpbq_fpbg_trans/ qed-. (* Note: this is used in the closure proof *) lemma fpbg_fpbs_trans: ∀h,g,G,G2,L,L2,T,T2. ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ∀G1,L1,T1. ⦃G1, L1, T1⦄ >≡[h, g] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄. -#h #g #G #G2 #L #L2 #T #T2 #H @(fpbs_ind_dx … H) -G -L -T /3 width=5 by fpbg_fpb_trans/ +#h #g #G #G2 #L #L2 #T #T2 #H @(fpbs_ind_dx … H) -G -L -T /3 width=5 by fpbg_fpbq_trans/ qed-. -lemma fpbu_fpbs_fpbg: ∀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⦄. -/3 width=5 by fpbg_fpbs_trans, fpbu_fpbg/ qed. - (* Note: this is used in the closure proof *) lemma fqup_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 elim (fqup_inv_step_sn … H) -H -/3 width=5 by fqus_fpbs, fpbu_fqu, fpbu_fpbs_fpbg/ +/3 width=5 by fqus_fpbs, fpb_fqu, ex2_3_intro/ qed. lemma cpxs_fpbg: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → ⦃G, L, T1⦄ >≡[h, g] ⦃G, L, T2⦄. #h #g #G #L #T1 #T2 #H #H0 elim (cpxs_neq_inv_step_sn … H … H0) -H -H0 -/4 width=5 by cpxs_fpbs, fpbu_cpx, fpbu_fpbs_fpbg/ +/4 width=5 by cpxs_fpbs, fpb_cpx, ex2_3_intro/ qed. lemma lstas_fpbg: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, l2] T2 → (T1 = T2 → ⊥) → @@ -70,19 +64,5 @@ lemma lstas_fpbg: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, l2] T2 → (T1 lemma lpxs_fpbg: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ≡[T, 0] L2 → ⊥) → ⦃G, L1, T⦄ >≡[h, g] ⦃G, L2, T⦄. #h #g #G #L1 #L2 #T #H #H0 elim (lpxs_nlleq_inv_step_sn … H … H0) -H -H0 -/4 width=5 by fpbu_fpbs_fpbg, fpbu_lpx, lpxs_lleq_fpbs/ +/4 width=5 by fpb_lpx, lpxs_lleq_fpbs, ex2_3_intro/ qed. - -lemma fpbs_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ ≡[0] ⦃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=1 by or_introl/ -| #G #G2 #L #L2 #T #T2 #_ #H2 * #H1 elim (fpb_fpbu … H2) -H2 #H2 - [ /3 width=5 by fleq_trans, or_introl/ - | /5 width=5 by fpbc_fpbg, fleq_fpbc_trans, fpbu_fpbc, or_intror/ - | /3 width=5 by fpbg_fleq_trans, or_intror/ - | /4 width=5 by fpbg_strap1, fpbu_fpbc, or_intror/ - ] -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_lift.ma index 58ecd1200..1a6da7e17 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_lift.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/reduction/fpbu_lift.ma". +include "basic_2/reduction/fpb_lift.ma". include "basic_2/computation/fpbg.ma". (* "QRST" PARALLEL COMPUTATION FOR CLOSURES *********************************) @@ -21,4 +21,4 @@ include "basic_2/computation/fpbg.ma". lemma sta_fpbg: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T1 •*[h, 1] T2 → ⦃G, L, T1⦄ >≡[h, g] ⦃G, L, T2⦄. -/4 width=2 by fpbu_fpbg, sta_fpbu/ qed. +/4 width=2 by fpb_fpbg, sta_fpb/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma index 0c1568207..79670f2a2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma @@ -14,14 +14,14 @@ include "basic_2/notation/relations/btpredstar_8.ma". include "basic_2/multiple/fqus.ma". -include "basic_2/reduction/fpb.ma". +include "basic_2/reduction/fpbq.ma". include "basic_2/computation/cpxs.ma". include "basic_2/computation/lpxs.ma". (* "QRST" PARALLEL COMPUTATION FOR CLOSURES *********************************) definition fpbs: ∀h. sd h → tri_relation genv lenv term ≝ - λh,g. tri_TC … (fpb h g). + λh,g. tri_TC … (fpbq h g). interpretation "'qrst' parallel computation (closure)" 'BTPRedStar h g G1 L1 T1 G2 L2 T2 = (fpbs h g G1 L1 T1 G2 L2 T2). @@ -43,8 +43,8 @@ lemma fpbs_ind_dx: ∀h,g,G2,L2,T2. ∀R:relation3 genv lenv term. R G2 L2 T2 lemma fpbs_refl: ∀h,g. tri_reflexive … (fpbs h g). /2 width=1 by tri_inj/ qed. -lemma fpb_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⦄. +lemma fpbq_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⦄. /2 width=1 by tri_inj/ qed. lemma fpbs_strap1: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ → @@ -58,27 +58,27 @@ lemma fpbs_strap2: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≽[h, g] lemma fqup_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 @(fqup_ind … H) -G2 -L2 -T2 -/4 width=5 by fqu_fquq, fpb_fquq, tri_step/ +/4 width=5 by fqu_fquq, fpbq_fquq, tri_step/ qed. lemma fqus_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 @(fqus_ind … H) -G2 -L2 -T2 -/3 width=5 by fpb_fquq, tri_step/ +/3 width=5 by fpbq_fquq, 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⦄. #h #g #G #L #T1 #T2 #H @(cpxs_ind … H) -T2 -/3 width=5 by fpb_cpx, fpbs_strap1/ +/3 width=5 by fpbq_cpx, fpbs_strap1/ qed. lemma lpxs_fpbs: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ⦃G, L1, T⦄ ≥[h, g] ⦃G, L2, T⦄. #h #g #G #L1 #L2 #T #H @(lpxs_ind … H) -L2 -/3 width=5 by fpb_lpx, fpbs_strap1/ +/3 width=5 by fpbq_lpx, fpbs_strap1/ qed. lemma lleq_fpbs: ∀h,g,G,L1,L2,T. L1 ≡[T, 0] L2 → ⦃G, L1, T⦄ ≥[h, g] ⦃G, L2, T⦄. -/3 width=1 by fpb_fpbs, fpb_lleq/ qed. +/3 width=1 by fpbq_fpbs, fpbq_lleq/ qed. lemma cprs_fpbs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄. /3 width=1 by cprs_cpxs, cpxs_fpbs/ qed. @@ -89,7 +89,7 @@ lemma lprs_fpbs: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1, T⦄ lemma fpbs_fqus_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊐* ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. #h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H @(fqus_ind … H) -G2 -L2 -T2 -/3 width=5 by fpbs_strap1, fpb_fquq/ +/3 width=5 by fpbs_strap1, fpbq_fquq/ qed-. lemma fpbs_fqup_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ → @@ -99,40 +99,40 @@ lemma fpbs_fqup_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≥[h, g lemma fpbs_cpxs_trans: ∀h,g,G1,G,L1,L,T1,T,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ → ⦃G, L⦄ ⊢ T ➡*[h, g] T2 → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T2⦄. #h #g #G1 #G #L1 #L #T1 #T #T2 #H1 #H @(cpxs_ind … H) -T2 -/3 width=5 by fpbs_strap1, fpb_cpx/ +/3 width=5 by fpbs_strap1, fpbq_cpx/ qed-. lemma fpbs_lpxs_trans: ∀h,g,G1,G,L1,L,L2,T1,T. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ → ⦃G, L⦄ ⊢ ➡*[h, g] L2 → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L2, T⦄. #h #g #G1 #G #L1 #L #L2 #T1 #T #H1 #H @(lpxs_ind … H) -L2 -/3 width=5 by fpbs_strap1, fpb_lpx/ +/3 width=5 by fpbs_strap1, fpbq_lpx/ qed-. lemma fpbs_lleq_trans: ∀h,g,G1,G,L1,L,L2,T1,T. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ → L ≡[T, 0] L2 → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L2, T⦄. -/3 width=5 by fpbs_strap1, fpb_lleq/ qed-. +/3 width=5 by fpbs_strap1, fpbq_lleq/ qed-. lemma fqus_fpbs_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊐* ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. #h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H @(fqus_ind_dx … H) -G1 -L1 -T1 -/3 width=5 by fpbs_strap2, fpb_fquq/ +/3 width=5 by fpbs_strap2, fpbq_fquq/ qed-. lemma cpxs_fpbs_trans: ∀h,g,G1,G2,L1,L2,T1,T,T2. ⦃G1, L1, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. #h #g #G1 #G2 #L1 #L2 #T1 #T #T2 #H1 #H @(cpxs_ind_dx … H) -T1 -/3 width=5 by fpbs_strap2, fpb_cpx/ +/3 width=5 by fpbs_strap2, fpbq_cpx/ qed-. lemma lpxs_fpbs_trans: ∀h,g,G1,G2,L1,L,L2,T1,T2. ⦃G1, L, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1⦄ ⊢ ➡*[h, g] L → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. #h #g #G1 #G2 #L1 #L #L2 #T1 #T2 #H1 #H @(lpxs_ind_dx … H) -L1 -/3 width=5 by fpbs_strap2, fpb_lpx/ +/3 width=5 by fpbs_strap2, fpbq_lpx/ qed-. lemma lleq_fpbs_trans: ∀h,g,G1,G2,L1,L,L2,T1,T2. ⦃G1, L, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → L1 ≡[T1, 0] L → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. -/3 width=5 by fpbs_strap2, fpb_lleq/ qed-. +/3 width=5 by fpbs_strap2, fpbq_lleq/ qed-. lemma cpxs_fqus_fpbs: ∀h,g,G1,G2,L1,L2,T1,T,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T → ⦃G1, L1, T⦄ ⊐* ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. @@ -157,5 +157,5 @@ lemma lpxs_lleq_fpbs: ∀h,g,G,L1,L,L2,T. ⦃G, L1⦄ ⊢ ➡*[h, g] L → (* Note: this is used in the closure proof *) lemma cpr_lpr_fpbs: ∀h,g,G,L1,L2,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L1, T1⦄ ≥[h, g] ⦃G, L2, T2⦄. -/4 width=5 by fpbs_strap1, fpb_fpbs, lpr_fpb, cpr_fpb/ +/4 width=5 by fpbs_strap1, fpbq_fpbs, lpr_fpbq, cpr_fpbq/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_aaa.ma index dbefe3bce..372b571b6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_aaa.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/reduction/fpb_aaa.ma". +include "basic_2/reduction/fpbq_aaa.ma". include "basic_2/computation/fpbs.ma". (* "QRST" PARALLEL COMPUTATION FOR CLOSURES *********************************) @@ -23,5 +23,5 @@ lemma fpbs_aaa_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, ∀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 fpb_aaa_conf/ +/2 width=8 by fpbq_aaa_conf/ 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 10153c2d1..cc6ae1362 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma @@ -63,7 +63,7 @@ qed. 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 * -/3 width=5 by cpxs_fqus_lpxs_fpbs, fpbs_strap1, fpb_lleq/ +/3 width=5 by cpxs_fqus_lpxs_fpbs, fpbs_strap1, fpbq_lleq/ qed-. (* Advanced properties ******************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbu.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpb.ma similarity index 60% rename from matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbu.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpb.ma index d2e880699..00d015628 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbu.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpb.ma @@ -12,8 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/multiple/fleq.ma". -include "basic_2/reduction/fpbu.ma". +include "basic_2/reduction/fpbq_alt.ma". include "basic_2/computation/fpbs_alt.ma". (* "QRST" PARALLEL COMPUTATION FOR CLOSURES *********************************) @@ -37,32 +36,6 @@ qed-. (* Properties on "rst" proper parallel reduction on closures ****************) -lemma fpbu_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⦄. -/3 width=1 by fpb_fpbs, fpbu_fwd_fpb/ qed. - -lemma fpbs_fpbu_sn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ ≡[0] ⦃G2, L2, T2⦄ ∨ - ∃∃G,L,T. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G, L, T⦄ & ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄. -(* ALTERNATIVE PROOF -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind_dx … H) -G1 -L1 -T1 -[ /2 width=1 by or_introl/ -| #G1 #G #L1 #L #T1 #T #H1 #_ * [ #H2 | * #G0 #L0 #T0 #H0 #H02 ] - elim (fpb_fpbu … H1) -H1 #H1 - [ /3 width=1 by -*) -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim(fpbs_inv_alt … H) -H -#L0 #L #T #HT1 #HT2 #HL0 #HL2 elim (eq_term_dec T1 T) #H destruct -[ -HT1 elim (fqus_inv_gen … HT2) -HT2 - [ #H elim (fqup_inv_step_sn … H) -H - /4 width=11 by fpbs_intro_alt, fpbu_fqu, ex2_3_intro, or_intror/ - | * #HG #HL #HT destruct elim (lleq_dec T2 L0 L 0) #H - [ /4 width=3 by fleq_intro, lleq_trans, or_introl/ - | elim (lpxs_nlleq_inv_step_sn … HL0 H) -HL0 -H - /5 width=7 by lpxs_lleq_fpbs, fpbu_lpx, lleq_trans, ex2_3_intro, or_intror/ - ] - ] -| elim (cpxs_neq_inv_step_sn … HT1 H) -HT1 -H - /5 width=11 by fpbs_intro_alt, fpbu_cpx, ex2_3_intro, or_intror/ -] -qed-. +lemma fpb_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⦄. +/3 width=1 by fpbq_fpbs, fpb_fpbq/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma index 4ea86975a..57c53b371 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "basic_2/reduction/fpb_lift.ma". include "basic_2/computation/cpxs_lift.ma". include "basic_2/computation/fpbs.ma". @@ -27,11 +26,11 @@ lemma lstas_fpbs: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, l2] T2 → lemma sta_fpbs: ∀h,g,G,L,T,U,l. ⦃G, L⦄ ⊢ T ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T •*[h, 1] U → ⦃G, L, T⦄ ≥[h, g] ⦃G, L, U⦄. -/4 width=2 by fpb_fpbs, sta_fpb/ qed. +/2 width=5 by lstas_fpbs/ qed. (* Note: this is used in the closure proof *) lemma cpr_lpr_sta_fpbs: ∀h,g,G,L1,L2,T1,T2,U2,l2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, g] l2+1 → ⦃G, L2⦄ ⊢ T2 •*[h, 1] U2 → ⦃G, L1, T1⦄ ≥[h, g] ⦃G, L2, U2⦄. -/4 width=5 by fpbs_strap1, cpr_lpr_fpbs, sta_cpx, fpb_cpx/ qed. +/4 width=5 by fpbs_strap1, cpr_lpr_fpbs, sta_cpx, fpbq_cpx/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma index 95548ecf4..4d44edb46 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/notation/relations/btsn_5.ma". -include "basic_2/reduction/fpbu.ma". +include "basic_2/reduction/fpb.ma". include "basic_2/computation/csx.ma". (* "QRST" STRONGLY NORMALIZING TERMS ****************************************) @@ -43,5 +43,5 @@ qed-. (* Basic inversion lemmas ***************************************************) lemma fsb_inv_csx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⦥[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] T. -#h #g #G #L #T #H elim H -G -L -T /5 width=1 by csx_intro, fpbu_cpx/ +#h #g #G #L #T #H elim H -G -L -T /5 width=1 by csx_intro, fpb_cpx/ 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 2040a3b35..f8928c298 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma @@ -39,7 +39,7 @@ fact aaa_ind_fpbu_aux: ∀h,g. ∀R:relation3 genv lenv term. #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 elim (fpbs_aaa_conf h g … G2 … L2 … T2 … HTA1) -A1 -/2 width=2 by fpbu_fpbs/ +/2 width=2 by fpb_fpbs/ qed-. lemma aaa_ind_fpbu: ∀h,g. ∀R:relation3 genv lenv term. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_alt.ma index 0a32134aa..cf966232a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_alt.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/notation/relations/btsnalt_5.ma". -include "basic_2/computation/fpbg_fpbg.ma". +include "basic_2/computation/fpbg_fpbs.ma". include "basic_2/computation/fsb.ma". (* "QRST" STRONGLY NORMALIZING TERMS ****************************************) @@ -53,15 +53,14 @@ qed-. theorem fsb_fsba: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⦥[h, g] T → ⦃G, L⦄ ⊢ ⦥⦥[h, g] T. #h #g #G #L #T #H @(fsb_ind_alt … H) -G -L -T #G1 #L1 #T1 #_ #IH @fsba_intro -#G2 #L2 #T2 #H elim (fpbg_inv_fpbu_sn … H) -H -/3 width=5 by fsba_fpbs_trans/ +#G2 #L2 #T2 * /3 width=5 by fsba_fpbs_trans/ qed. (* Main inversion lemmas ****************************************************) theorem fsba_inv_fsb: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⦥⦥[h, g] T → ⦃G, L⦄ ⊢ ⦥[h, g] T. #h #g #G #L #T #H @(fsba_ind_alt … H) -G -L -T -/5 width=1 by fsb_intro, fpbc_fpbg, fpbu_fpbc/ +/4 width=1 by fsb_intro, fpb_fpbg/ qed-. (* Advanced properties ******************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma index ceb783b0b..38cbe5c16 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma @@ -12,6 +12,8 @@ (* *) (**************************************************************************) +include "basic_2/computation/fpbs_fpb.ma". +include "basic_2/computation/fpbs_fpbs.ma". include "basic_2/computation/csx_fpbs.ma". include "basic_2/computation/lsx_csx.ma". include "basic_2/computation/fsb_alt.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fleq/fpbs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fleq/fpbs.etc index 546994dfa..017421feb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/fleq/fpbs.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fleq/fpbs.etc @@ -1,3 +1,29 @@ +lemma fpbs_fpbu_sn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ≡[0] ⦃G2, L2, T2⦄ ∨ + ∃∃G,L,T. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G, L, T⦄ & ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄. +(* ALTERNATIVE PROOF +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind_dx … H) -G1 -L1 -T1 +[ /2 width=1 by or_introl/ +| #G1 #G #L1 #L #T1 #T #H1 #_ * [ #H2 | * #G0 #L0 #T0 #H0 #H02 ] + elim (fpb_fpbu … H1) -H1 #H1 + [ /3 width=1 by +*) +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim(fpbs_inv_alt … H) -H +#L0 #L #T #HT1 #HT2 #HL0 #HL2 elim (eq_term_dec T1 T) #H destruct +[ -HT1 elim (fqus_inv_gen … HT2) -HT2 + [ #H elim (fqup_inv_step_sn … H) -H + /4 width=11 by fpbs_intro_alt, fpbu_fqu, ex2_3_intro, or_intror/ + | * #HG #HL #HT destruct elim (lleq_dec T2 L0 L 0) #H + [ /4 width=3 by fleq_intro, lleq_trans, or_introl/ + | elim (lpxs_nlleq_inv_step_sn … HL0 H) -HL0 -H + /5 width=7 by lpxs_lleq_fpbs, fpbu_lpx, lleq_trans, ex2_3_intro, or_intror/ + ] + ] +| elim (cpxs_neq_inv_step_sn … HT1 H) -HT1 -H + /5 width=11 by fpbs_intro_alt, fpbu_cpx, ex2_3_intro, or_intror/ +] +qed-. + (* alternative proof that needs decidability of bteq to go in fpbs.ma * or lpx_fpbc_trans to go in fpbs_lift.ma (possibly) *) @@ -20,3 +46,4 @@ lemma fpbs_fwd_fpb_sn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G ] | #L0 #HL10 #_ * [ /3 width=3 by or_introl, lpx_bteq_trans/ ] * #G3 #L3 #T3 #H13 #H32 + diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/fpbc/fpbc.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/fpbc/fpbc.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc_fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/fpbc/fpbc_fleq.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc_fleq.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/fpbc/fpbc_fleq.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpbc/fpbg.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpbc/fpbg.etc new file mode 100644 index 000000000..574c35e10 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpbc/fpbg.etc @@ -0,0 +1,61 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lazybtpredstarproper_8.ma". +include "basic_2/reduction/fpbc.ma". + +(* "QRST" PROPER PARALLEL COMPUTATION FOR CLOSURES **************************) + +definition fpbg: ∀h. sd h → tri_relation genv lenv term ≝ + λh,g. tri_TC … (fpbc h g). + +interpretation "'qrst' proper parallel computation (closure)" + 'LazyBTPRedStarProper h g G1 L1 T1 G2 L2 T2 = (fpbg h g G1 L1 T1 G2 L2 T2). + +(* Basic properties *********************************************************) + +lemma fpbc_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻≡[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄. +/2 width=1 by tri_inj/ qed. + +lemma fpbg_strap1: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. + ⦃G1, L1, T1⦄ >≡[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≻≡[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄. +/2 width=5 by tri_step/ qed. + +lemma fpbg_strap2: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. + ⦃G1, L1, T1⦄ ≻≡[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ >≡[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄. +/2 width=5 by tri_TC_strap/ qed. + +lemma fpbu_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h,g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄. +/3 width=1 by fpbu_fpbc, fpbc_fpbg/ qed. + +(* Basic eliminators ********************************************************) + +lemma fpbg_ind: ∀h,g,G1,L1,T1. ∀R:relation3 …. + (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻≡[h, g] ⦃G2, L2, T2⦄ → 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. +#h #g #G1 #L1 #T1 #R #IH1 #IH2 #G2 #L2 #T2 #H +@(tri_TC_ind … IH1 IH2 G2 L2 T2 H) +qed-. + +lemma fpbg_ind_dx: ∀h,g,G2,L2,T2. ∀R:relation3 …. + (∀G1,L1,T1. ⦃G1, L1, T1⦄ ≻≡[h, g] ⦃G2, L2, T2⦄ → R G1 L1 T1) → + (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≻≡[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ >≡[h, g] ⦃G2, L2, T2⦄ → R G L T → R G1 L1 T1) → + ∀G1,L1,T1. ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄ → R G1 L1 T1. +#h #g #G2 #L2 #T2 #R #IH1 #IH2 #G1 #L1 #T1 #H +@(tri_TC_ind_dx … IH1 IH2 G1 L1 T1 H) +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpbc/fpbg_fleq.etc similarity index 54% rename from matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg_lift.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/fpbc/fpbg_fleq.etc index 26dec0777..754811ec2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg_lift.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpbc/fpbg_fleq.etc @@ -12,17 +12,25 @@ (* *) (**************************************************************************) -include "basic_2/computation/fpbc_lift.ma". +include "basic_2/reduction/fpbc_fleq.ma". include "basic_2/computation/fpbg.ma". -(* GENERAL "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *********************) +(* "QRST" PROPER PARALLEL COMPUTATION FOR CLOSURES **************************) -(* Advanced properties ******************************************************) +(* Properties on lazy equivalence for closures ******************************) -lemma lsstas_fpbg: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, g, l2] T2 → (T1 = T2 → ⊥) → - ∀l1. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ⦃G, L, T1⦄ >[h, g] ⦃G, L, T2⦄. -/4 width=5 by fpbc_fpbg, lsstas_fpbc/ qed. +lemma fpbg_fleq_trans: ∀h,g,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ >≡[h, g] ⦃G, L, T⦄ → + ∀G2,L2,T2. ⦃G, L, T⦄ ≡[0] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G #L1 #L #T1 #T #H @(fpbg_ind … H) -G -L -T +[ /3 width=5 by fpbc_fpbg, fpbc_fleq_trans/ +| /4 width=9 by fpbg_strap1, fpbc_fleq_trans/ +] +qed-. -lemma ssta_fpbg: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → - ⦃G, L⦄ ⊢ T1 •[h, g] T2 → ⦃G, L, T1⦄ >[h, g] ⦃G, L, T2⦄. -/3 width=2 by fpbc_fpbg, ssta_fpbc/ qed. +lemma fleq_fpbg_trans: ∀h,g,G,G2,L,L2,T,T2. ⦃G, L, T⦄ >≡[h, g] ⦃G2, L2, T2⦄ → + ∀G1,L1,T1. ⦃G1, L1, T1⦄ ≡[0] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄. +#h #g #G #G2 #L #L2 #T #T2 #H @(fpbg_ind_dx … H) -G -L -T +[ /3 width=5 by fpbc_fpbg, fleq_fpbc_trans/ +| /4 width=9 by fpbg_strap2, fleq_fpbc_trans/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpbc/fpbg_fpbg.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpbc/fpbg_fpbg.etc new file mode 100644 index 000000000..57dd5ebb4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpbc/fpbg_fpbg.etc @@ -0,0 +1,53 @@ +(**************************************************************************) +(* ___ *) +(* ||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_fpbu.ma". +include "basic_2/computation/fpbs_fpbc.ma". +include "basic_2/computation/fpbs_fpbs.ma". +include "basic_2/computation/fpbg_fpbs.ma". + +(* "QRST" PROPER PARALLEL COMPUTATION FOR CLOSURES **************************) + +(* Advanced inversion lemmas ************************************************) + +lemma fpbg_inv_fpbu_sn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄ → + ∃∃G,L,T. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G, L, T⦄ & ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbg_ind_dx … H) -G1 -L1 -T1 +[ #G1 #L1 #T1 * /3 width=5 by fleq_fpbs, ex2_3_intro/ +| #G1 #G #L1 #L #T1 #T * + #G0 #L0 #T0 #H10 #H0 #_ * + /5 width=9 by fpbu_fpbs, fpbs_trans, fleq_fpbs, ex2_3_intro/ +] +qed-. + +(* Advanced forward lemmas **************************************************) + +lemma fpbg_fwd_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 #H @(fpbg_ind … H) -G2 -L2 -T2 +[2: #G #G2 #L #L2 #T #T2 #_ #H2 #IH1 @(fpbs_trans … IH1) -IH1 ] (**) (* full auto fails *) +/2 width=1 by fpbc_fpbs/ +qed-. + +(* Advanced properties ******************************************************) + +lemma fpbs_fpbu_trans: ∀h,g,F1,F2,K1,K2,T1,T2. ⦃F1, K1, T1⦄ ≥[h, g] ⦃F2, K2, T2⦄ → + ∀G2,L2,U2. ⦃F2, K2, T2⦄ ≻[h, g] ⦃G2, L2, U2⦄ → + ∃∃G1,L1,U1. ⦃F1, K1, T1⦄ ≻[h, g] ⦃G1, L1, U1⦄ & ⦃G1, L1, U1⦄ ≥[h, g] ⦃G2, L2, U2⦄. +/5 width=5 by fpbg_inv_fpbu_sn, fpbs_fpbg_trans, fpbc_fpbg, fpbu_fpbc/ qed-. + +(* Man properties ***********************************************************) + +theorem fpbg_trans: ∀h,g. tri_transitive … (fpbg h g). +/2 width=5 by tri_TC_transitive/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpbc/fpbg_fpbs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpbc/fpbg_fpbs.etc new file mode 100644 index 000000000..4b8662295 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpbc/fpbg_fpbs.etc @@ -0,0 +1,88 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lpxs_lleq.ma". +include "basic_2/computation/fpbs_lift.ma". +include "basic_2/computation/fpbg_fleq.ma". + +(* "QRST" PROPER PARALLEL COMPUTATION FOR CLOSURES **************************) + +(* Properties on "qrst" parallel reduction on closures **********************) + +lemma fpbg_fpb_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. + ⦃G1, L1, T1⦄ >≡[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≽[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2 elim (fpb_fpbu … H2) -H2 +/3 width=5 by fpbg_fleq_trans, fpbg_strap1, fpbu_fpbc/ +qed-. + +lemma fpb_fpbg_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. + ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ >≡[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 elim (fpb_fpbu … H1) -H1 +/3 width=5 by fleq_fpbg_trans, fpbg_strap2, fpbu_fpbc/ +qed-. + +(* Properties on "qrst" parallel compuutation on closures *******************) + +lemma fpbs_fpbg_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 #H @(fpbs_ind … H) -G -L -T /3 width=5 by fpb_fpbg_trans/ +qed-. + +(* Note: this is used in the closure proof *) +lemma fpbg_fpbs_trans: ∀h,g,G,G2,L,L2,T,T2. ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → + ∀G1,L1,T1. ⦃G1, L1, T1⦄ >≡[h, g] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄. +#h #g #G #G2 #L #L2 #T #T2 #H @(fpbs_ind_dx … H) -G -L -T /3 width=5 by fpbg_fpb_trans/ +qed-. + +lemma fpbu_fpbs_fpbg: ∀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⦄. +/3 width=5 by fpbg_fpbs_trans, fpbu_fpbg/ qed. + +(* Note: this is used in the closure proof *) +lemma fqup_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 elim (fqup_inv_step_sn … H) -H +/3 width=5 by fqus_fpbs, fpbu_fqu, fpbu_fpbs_fpbg/ +qed. + +lemma cpxs_fpbg: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → + (T1 = T2 → ⊥) → ⦃G, L, T1⦄ >≡[h, g] ⦃G, L, T2⦄. +#h #g #G #L #T1 #T2 #H #H0 elim (cpxs_neq_inv_step_sn … H … H0) -H -H0 +/4 width=5 by cpxs_fpbs, fpbu_cpx, fpbu_fpbs_fpbg/ +qed. + +lemma lstas_fpbg: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, l2] T2 → (T1 = T2 → ⊥) → + ∀l1. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ⦃G, L, T1⦄ >≡[h, g] ⦃G, L, T2⦄. +/3 width=5 by lstas_cpxs, cpxs_fpbg/ qed. + +lemma lpxs_fpbg: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → + (L1 ≡[T, 0] L2 → ⊥) → ⦃G, L1, T⦄ >≡[h, g] ⦃G, L2, T⦄. +#h #g #G #L1 #L2 #T #H #H0 elim (lpxs_nlleq_inv_step_sn … H … H0) -H -H0 +/4 width=5 by fpbu_fpbs_fpbg, fpbu_lpx, lpxs_lleq_fpbs/ +qed. + +lemma fpbs_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ≡[0] ⦃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=1 by or_introl/ +| #G #G2 #L #L2 #T #T2 #_ #H2 * #H1 elim (fpb_fpbu … H2) -H2 #H2 + [ /3 width=5 by fleq_trans, or_introl/ + | /5 width=5 by fpbc_fpbg, fleq_fpbc_trans, fpbu_fpbc, or_intror/ + | /3 width=5 by fpbg_fleq_trans, or_intror/ + | /4 width=5 by fpbg_strap1, fpbu_fpbc, or_intror/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/fpbc/fpbg_lift.etc similarity index 75% rename from matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fleq.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/fpbc/fpbg_lift.etc index 4761d6097..58ecd1200 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpbc/fpbg_lift.etc @@ -12,14 +12,13 @@ (* *) (**************************************************************************) -include "basic_2/multiple/fleq.ma". -include "basic_2/computation/fpbs.ma". +include "basic_2/reduction/fpbu_lift.ma". +include "basic_2/computation/fpbg.ma". (* "QRST" PARALLEL COMPUTATION FOR CLOSURES *********************************) -(* Properties on lazy equivalence on closures *******************************) +(* Advanced properties ******************************************************) -lemma fleq_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. - ⦃G1, L1, T1⦄ ≡[0] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 * /2 width=1 by lleq_fpbs/ -qed. +lemma sta_fpbg: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → + ⦃G, L⦄ ⊢ T1 •*[h, 1] T2 → ⦃G, L, T1⦄ >≡[h, g] ⦃G, L, T2⦄. +/4 width=2 by fpbu_fpbg, sta_fpbu/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbc.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/fpbc/fpbs_fpbc.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbc.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/fpbc/fpbs_fpbc.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazybtpredproper_8.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/fpbc/lazybtpredproper_8.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazybtpredproper_8.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/fpbc/lazybtpredproper_8.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg.etc deleted file mode 100644 index a96b0bbbd..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg.etc +++ /dev/null @@ -1,40 +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/btpredstarproper_8.ma". -include "basic_2/computation/fpbc.ma". - -(* GENEARAL "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES *************) - -(* Note: this is not transitive *) -inductive fpbg (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝ -| fpbg_cpxs: ∀L2,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 → - fpbg h g G1 L1 T1 G1 L2 T2 -| fpbg_fqup: ∀G2,L,L2,T,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T → ⦃G1, L1, T⦄ ⊃+ ⦃G2, L, T2⦄ → ⦃G2, L⦄ ⊢ ➡*[h, g] L2 → - fpbg h g G1 L1 T1 G2 L2 T2 -| fpbg_lpxs: ∀G2,L,L0,L2,T,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T → ⦃G1, L1, T⦄ ⊃* ⦃G2, L, T2⦄ → ⦃G2, L⦄ ⊢ ➡*[h, g] L0 → - (L ⋕[0, T2] L0 → ⊥) → ⦃G2, L0⦄ ⊢ ➡*[h, g] L2 → L0 ⋕[0, T2] L2 → - fpbg h g G1 L1 T1 G2 L2 T2 -. - -interpretation "'big tree' proper parallel computation (closure)" - 'BTPRedStarProper h g G1 L1 T1 G2 L2 T2 = (fpbg h g G1 L1 T1 G2 L2 T2). - -(* Basic properties *********************************************************) - -lemma fpbc_fpbg: ∀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 -/3 width=9 by fpbg_fqup, fpbg_cpxs, fpbg_lpxs/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg_fpbg.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg_fpbg.etc deleted file mode 100644 index 97846fda4..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg_fpbg.etc +++ /dev/null @@ -1,57 +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/lpxs_lpxs.ma". -include "basic_2/computation/fpbs_alt.ma". -include "basic_2/computation/fpbg.ma". - -(* GENERAL "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **************) - -(* Advanced forward lemmas **************************************************) - -lemma fpbg_fwd_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 #H elim H -G2 -L2 -T2 -/3 width=5 by cpxs_fqus_lpxs_fpbs, cpxs_fqup_fpbs, fpbs_trans, lpxs_fpbs, cpxs_fpbs/ -qed-. - -lemma fpbg_fwd_fpbc_sn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄ → - ∃∃G,L,T. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G, L, T⦄ & ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G2 -L2 -T2 -[ /4 width=5 by fpbc_cpxs, lpxs_fpbs, ex2_3_intro/ -| #G2 #L #L2 #T #T2 #HT1 #HT2 #HL2 elim (eq_term_dec T1 T) #H destruct - [ -HT1 /3 width=5 by fpbc_fqup, lpxs_fpbs, ex2_3_intro/ - | /5 width=9 by fpbc_cpxs, fpbsa_inv_fpbs, fqup_fqus, ex3_2_intro, ex2_3_intro/ - ] -| #G2 #L #L0 #L2 #T #T2 #HT1 #HT2 #HL0 #H0 #HL02 #H02 - lapply (lpxs_trans … HL0 … HL02) #HL2 - elim (eq_term_dec T1 T) #H destruct - [ -HT1 elim (fqus_inv_gen … HT2) -HT2 - [ /3 width=5 by fpbc_fqup, lpxs_fpbs, ex2_3_intro/ - | * #H1 #H2 #H3 destruct - /4 width=5 by fpbc_lpxs, lpxs_fpbs, ex2_3_intro/ - ] - | /4 width=9 by fpbc_cpxs, fpbsa_inv_fpbs, ex3_2_intro, ex2_3_intro/ - ] -] -qed-. - -(* Advanced properties ******************************************************) - -lemma fqu_fpbs_fpbg: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G, L, T⦄ → - ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H elim(fpbs_fpbsa … H) -H -#L0 #T0 #HT0 #HT02 #HL02 elim (fqu_cpxs_trans … HT0 … H1) -T -/3 width=7 by fpbg_fqup, fqus_strap2_fqu/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg_fpns.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg_fpns.etc deleted file mode 100644 index 0ed65c927..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg_fpns.etc +++ /dev/null @@ -1,34 +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/fpns.ma". -include "basic_2/computation/fpbg.ma". - -(* GENEARAL "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES *************) - -(* Properties on parallel computation for "big tree" normal forms ***********) - -axiom fpns_fpbg_trans: ∀h,g,F1,F2,K1,K2,T1,T2. ⦃F1, K1, T1⦄ ⊢ ⋕➡*[h, g] ⦃F2, K2, T2⦄ → - ∀G2,L2,U2. ⦃F2, K2, T2⦄ >[h, g] ⦃G2, L2, U2⦄ → - ∃∃G1,L1,U1. ⦃F1, K1, T1⦄ >[h, g] ⦃G1, L1, U1⦄ & ⦃G1, L1, U1⦄ ⊢ ⋕➡*[h, g] ⦃G2, L2, U2⦄. -(* -#h #g #F1 #F2 #K1 #K2 #T1 #T2 * -F2 -K2 -T2 -#K2 #HK12 #HT1 #G2 #L2 #U2 * -G2 -L2 -U2 -[ /4 width=9 by fpbc_cpxs, fpns_intro, lpxs_cpxs_trans, lleq_cpxs_conf_dx, ex2_3_intro/ -| #G2 #L2 #U2 #H12 elim (lpxs_lleq_fqup_trans … H12 … HK12 HT1) -K2 - /3 width=5 by fpbc_fqup, fpns_intro, ex2_3_intro/ -| /5 width=5 by fpbc_lpxs, lpxs_trans, lleq_canc_sn, ex2_3_intro/ -] -qed-. -*) \ No newline at end of file diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/btpredstarproper_8.etc b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredalt_8.ma similarity index 87% rename from matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/btpredstarproper_8.etc rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredalt_8.ma index 66d7a34ba..c3f111a0e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/btpredstarproper_8.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredalt_8.ma @@ -14,6 +14,6 @@ (* 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 ⦄ )" +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 @{ 'BTPRedStarProper $h $g $G1 $L1 $T1 $G2 $L2 $T2 }. + for @{ 'BTPRedAlt $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 aaecd70cc..8872199fd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma @@ -12,31 +12,29 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/btpred_8.ma". -include "basic_2/substitution/fquq.ma". +include "basic_2/notation/relations/btpredproper_8.ma". +include "basic_2/substitution/fqu.ma". include "basic_2/multiple/lleq.ma". include "basic_2/reduction/lpx.ma". -(* "QRST" PARALLEL REDUCTION FOR CLOSURES ***********************************) +(* "RST" PROPER PARALLEL COMPUTATION FOR CLOSURES ***************************) inductive fpb (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝ -| fpb_fquq: ∀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_lleq: ∀L2. L1 ≡[T1, 0] L2 → fpb h g G1 L1 T1 G1 L2 T1 +| fpb_fqu: ∀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 → (T1 = T2 → ⊥) → fpb h g G1 L1 T1 G1 L1 T2 +| fpb_lpx: ∀L2. ⦃G1, L1⦄ ⊢ ➡[h, g] L2 → (L1 ≡[T1, 0] L2 → ⊥) → fpb h g G1 L1 T1 G1 L2 T1 . interpretation - "'qrst' parallel reduction (closure)" - 'BTPRed h g G1 L1 T1 G2 L2 T2 = (fpb h g G1 L1 T1 G2 L2 T2). + "'rst' proper parallel reduction (closure)" + 'BTPRedProper h g G1 L1 T1 G2 L2 T2 = (fpb h g G1 L1 T1 G2 L2 T2). (* Basic properties *********************************************************) -lemma fpb_refl: ∀h,g. tri_reflexive … (fpb h g). -/2 width=1 by fpb_cpx/ qed. - -lemma cpr_fpb: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L, T1⦄ ≽[h, g] ⦃G, L, T2⦄. +lemma cpr_fpb: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → + ⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄. /3 width=1 by fpb_cpx, cpr_cpx/ qed. -lemma lpr_fpb: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L1, T⦄ ≽[h, g] ⦃G, L2, T⦄. +lemma lpr_fpb: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡ L2 → (L1 ≡[T, 0] L2 → ⊥) → + ⦃G, L1, T⦄ ≻[h, g] ⦃G, L2, T⦄. /3 width=1 by fpb_lpx, lpr_lpx/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbu_fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_fleq.ma similarity index 56% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/fpbu_fleq.ma rename to matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_fleq.ma index f4a0aed42..788a59364 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbu_fleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_fleq.ma @@ -13,32 +13,29 @@ (**************************************************************************) include "basic_2/multiple/fleq.ma". -include "basic_2/reduction/fpbu_lleq.ma". +include "basic_2/reduction/fpb_lleq.ma". (* "RST" PROPER PARALLEL COMPUTATION FOR CLOSURES ***************************) (* Properties on lazy equivalence for closures ******************************) -lemma fleq_fpbu_trans: ∀h,g,F1,F2,K1,K2,T1,T2. ⦃F1, K1, T1⦄ ≡[0] ⦃F2, K2, T2⦄ → - ∀G2,L2,U2. ⦃F2, K2, T2⦄ ≻[h, g] ⦃G2, L2, U2⦄ → - ∃∃G1,L1,U1. ⦃F1, K1, T1⦄ ≻[h, g] ⦃G1, L1, U1⦄ & ⦃G1, L1, U1⦄ ≡[0] ⦃G2, L2, U2⦄. +lemma fleq_fpb_trans: ∀h,g,F1,F2,K1,K2,T1,T2. ⦃F1, K1, T1⦄ ≡[0] ⦃F2, K2, T2⦄ → + ∀G2,L2,U2. ⦃F2, K2, T2⦄ ≻[h, g] ⦃G2, L2, U2⦄ → + ∃∃G1,L1,U1. ⦃F1, K1, T1⦄ ≻[h, g] ⦃G1, L1, U1⦄ & ⦃G1, L1, U1⦄ ≡[0] ⦃G2, L2, U2⦄. #h #g #F1 #F2 #K1 #K2 #T1 #T2 * -F2 -K2 -T2 -#K2 #HK12 #G2 #L2 #U2 #H12 elim (lleq_fpbu_trans … HK12 … H12) -K2 +#K2 #HK12 #G2 #L2 #U2 #H12 elim (lleq_fpb_trans … HK12 … H12) -K2 /3 width=5 by fleq_intro, ex2_3_intro/ qed-. -lemma fpb_fpbu: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ ≡[0] ⦃G2, L2, T2⦄ ∨ - ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄. +(* Inversion lemmas on lazy equivalence for closures ************************) + +lemma fpb_inv_fleq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ≡[0] ⦃G2, L2, T2⦄ → ⊥. #h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 -[ #G2 #L2 #T2 #H elim (fquq_inv_gen … H) -H - [ /3 width=1 by fpbu_fqu, or_intror/ - | * #H1 #H2 #H3 destruct /2 width=1 by or_introl/ - ] -| #T2 #HT12 elim (eq_term_dec T1 T2) - #HnT12 destruct /4 width=1 by fpbu_cpx, or_intror, or_introl/ -| #L2 #HL12 elim (lleq_dec … T1 L1 L2 0) - /4 width=1 by fpbu_lpx, fleq_intro, or_intror, or_introl/ -| /3 width=1 by fleq_intro, or_introl/ +[ #G2 #L2 #T2 #H12 #H elim (fleq_inv_gen … H) -H + /3 width=8 by lleq_fwd_length, fqu_inv_eq/ +| #T2 #_ #HnT #H elim (fleq_inv_gen … H) -H /2 width=1 by/ +| #L2 #_ #HnL #H elim (fleq_inv_gen … H) -H /2 width=1 by/ ] qed-. + diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_lift.ma index 8c9070a44..5adf85e51 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_lift.ma @@ -12,14 +12,17 @@ (* *) (**************************************************************************) +include "basic_2/unfold/lstas_da.ma". include "basic_2/reduction/cpx_lift.ma". include "basic_2/reduction/fpb.ma". -(* "QRST" PARALLEL REDUCTION FOR CLOSURES ***********************************) +(* "RST" PROPER PARALLEL COMPUTATION FOR CLOSURES ***************************) (* Advanced properties ******************************************************) -lemma sta_fpb: ∀h,g,G,L,T1,T2,l. - ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T1 •*[h, 1] T2 → - ⦃G, L, T1⦄ ≽[h, g] ⦃G, L, T2⦄. -/3 width=4 by fpb_cpx, sta_cpx/ qed. +lemma sta_fpb: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → + ⦃G, L⦄ ⊢ T1 •*[h, 1] T2 → ⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄. +#h #g #G #L #T1 #T2 #l #HT1 #HT12 elim (eq_term_dec T1 T2) +/3 width=2 by fpb_cpx, sta_cpx/ #H destruct +elim (lstas_inv_refl_pos h G L T2 0) // +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbu_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_lleq.ma similarity index 76% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/fpbu_lleq.ma rename to matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_lleq.ma index 9b82c1963..519880ff8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbu_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_lleq.ma @@ -15,20 +15,20 @@ include "basic_2/multiple/lleq_fqus.ma". include "basic_2/multiple/lleq_lleq.ma". include "basic_2/reduction/lpx_lleq.ma". -include "basic_2/reduction/fpbu.ma". +include "basic_2/reduction/fpb.ma". (* "RST" PROPER PARALLEL COMPUTATION FOR CLOSURES ***************************) (* Properties on lazy equivalence for local environments ********************) -lemma lleq_fpbu_trans: ∀h,g,F,K1,K2,T. K1 ≡[T, 0] K2 → - ∀G,L2,U. ⦃F, K2, T⦄ ≻[h, g] ⦃G, L2, U⦄ → - ∃∃L1. ⦃F, K1, T⦄ ≻[h, g] ⦃G, L1, U⦄ & L1 ≡[U, 0] L2. +lemma lleq_fpb_trans: ∀h,g,F,K1,K2,T. K1 ≡[T, 0] K2 → + ∀G,L2,U. ⦃F, K2, T⦄ ≻[h, g] ⦃G, L2, U⦄ → + ∃∃L1. ⦃F, K1, T⦄ ≻[h, g] ⦃G, L1, U⦄ & L1 ≡[U, 0] L2. #h #g #F #K1 #K2 #T #HT #G #L2 #U * -G -L2 -U [ #G #L2 #U #H2 elim (lleq_fqu_trans … H2 … HT) -K2 - /3 width=3 by fpbu_fqu, ex2_intro/ -| /4 width=10 by fpbu_cpx, cpx_lleq_conf_sn, lleq_cpx_trans, ex2_intro/ + /3 width=3 by fpb_fqu, ex2_intro/ +| /4 width=10 by fpb_cpx, cpx_lleq_conf_sn, lleq_cpx_trans, ex2_intro/ | #L2 #HKL2 #HnKL2 elim (lleq_lpx_trans … HKL2 … HT) -HKL2 - /6 width=3 by fpbu_lpx, lleq_canc_sn, ex2_intro/ (* 2 lleq_canc_sn *) + /6 width=3 by fpb_lpx, lleq_canc_sn, ex2_intro/ (* 2 lleq_canc_sn *) ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbq.ma new file mode 100644 index 000000000..3e417b723 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbq.ma @@ -0,0 +1,42 @@ +(**************************************************************************) +(* ___ *) +(* ||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/btpred_8.ma". +include "basic_2/substitution/fquq.ma". +include "basic_2/multiple/lleq.ma". +include "basic_2/reduction/lpx.ma". + +(* "QRST" PARALLEL REDUCTION FOR CLOSURES ***********************************) + +inductive fpbq (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝ +| fpbq_fquq: ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → fpbq h g G1 L1 T1 G2 L2 T2 +| fpbq_cpx : ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T2 → fpbq h g G1 L1 T1 G1 L1 T2 +| fpbq_lpx : ∀L2. ⦃G1, L1⦄ ⊢ ➡[h, g] L2 → fpbq h g G1 L1 T1 G1 L2 T1 +| fpbq_lleq: ∀L2. L1 ≡[T1, 0] L2 → fpbq h g G1 L1 T1 G1 L2 T1 +. + +interpretation + "'qrst' parallel reduction (closure)" + 'BTPRed h g G1 L1 T1 G2 L2 T2 = (fpbq h g G1 L1 T1 G2 L2 T2). + +(* Basic properties *********************************************************) + +lemma fpbq_refl: ∀h,g. tri_reflexive … (fpbq h g). +/2 width=1 by fpbq_cpx/ qed. + +lemma cpr_fpbq: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L, T1⦄ ≽[h, g] ⦃G, L, T2⦄. +/3 width=1 by fpbq_cpx, cpr_cpx/ qed. + +lemma lpr_fpbq: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L1, T⦄ ≽[h, g] ⦃G, L2, T⦄. +/3 width=1 by fpbq_lpx, lpr_lpx/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbq_aaa.ma similarity index 86% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/reduction/fpbq_aaa.ma index 69a0b1fcf..0f3d7fbc6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbq_aaa.ma @@ -15,14 +15,14 @@ include "basic_2/static/aaa_fqus.ma". include "basic_2/static/aaa_lleq.ma". include "basic_2/reduction/lpx_aaa.ma". -include "basic_2/reduction/fpb.ma". +include "basic_2/reduction/fpbq.ma". (* "QRST" PARALLEL REDUCTION FOR CLOSURES ***********************************) (* Properties on atomic arity assignment for terms **************************) -lemma fpb_aaa_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. +lemma fpbq_aaa_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_lleq_conf, lpx_aaa_conf, cpx_aaa_conf, aaa_fquq_conf, ex_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbu_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbq_lift.ma similarity index 71% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/fpbu_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/reduction/fpbq_lift.ma index a0f28b492..d432fae27 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbu_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbq_lift.ma @@ -12,17 +12,14 @@ (* *) (**************************************************************************) -include "basic_2/unfold/lstas_da.ma". include "basic_2/reduction/cpx_lift.ma". -include "basic_2/reduction/fpbu.ma". +include "basic_2/reduction/fpbq.ma". -(* "RST" PROPER PARALLEL COMPUTATION FOR CLOSURES ***************************) +(* "QRST" PARALLEL REDUCTION FOR CLOSURES ***********************************) (* Advanced properties ******************************************************) -lemma sta_fpbu: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → - ⦃G, L⦄ ⊢ T1 •*[h, 1] T2 → ⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄. -#h #g #G #L #T1 #T2 #l #HT1 #HT12 elim (eq_term_dec T1 T2) -/3 width=2 by fpbu_cpx, sta_cpx/ #H destruct -elim (lstas_inv_refl_pos h G L T2 0) // -qed. +lemma sta_fpbq: ∀h,g,G,L,T1,T2,l. + ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T1 •*[h, 1] T2 → + ⦃G, L, T1⦄ ≽[h, g] ⦃G, L, T2⦄. +/3 width=4 by fpbq_cpx, sta_cpx/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbu.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbu.ma deleted file mode 100644 index d6d7c9a0a..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbu.ma +++ /dev/null @@ -1,46 +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/btpredproper_8.ma". -include "basic_2/reduction/fpb.ma". - -(* "RST" PROPER PARALLEL COMPUTATION FOR CLOSURES ***************************) - -inductive fpbu (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝ -| fpbu_fqu: ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → fpbu h g G1 L1 T1 G2 L2 T2 -| fpbu_cpx: ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T2 → (T1 = T2 → ⊥) → fpbu h g G1 L1 T1 G1 L1 T2 -| fpbu_lpx: ∀L2. ⦃G1, L1⦄ ⊢ ➡[h, g] L2 → (L1 ≡[T1, 0] L2 → ⊥) → fpbu h g G1 L1 T1 G1 L2 T1 -. - -interpretation - "'rst' proper parallel reduction (closure)" - 'BTPRedProper h g G1 L1 T1 G2 L2 T2 = (fpbu h g G1 L1 T1 G2 L2 T2). - -(* Basic properties *********************************************************) - -lemma cpr_fpbu: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → - ⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄. -/3 width=1 by fpbu_cpx, cpr_cpx/ qed. - -lemma lpr_fpbu: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡ L2 → (L1 ≡[T, 0] L2 → ⊥) → - ⦃G, L1, T⦄ ≻[h, g] ⦃G, L2, T⦄. -/3 width=1 by fpbu_lpx, lpr_lpx/ qed. - -(* Basic forward lemmas *****************************************************) - -lemma fpbu_fwd_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 -/3 width=1 by fpb_fquq, fpb_cpx, fpb_lpx, fqu_fquq/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqu.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqu.ma index 21697819c..ffc2d1965 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqu.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqu.ma @@ -66,6 +66,20 @@ lemma fqu_fwd_length_lref1: ∀G1,G2,L1,L2,T2,i. ⦃G1, L1, #i⦄ ⊐ ⦃G2, L2, /2 width=7 by fqu_fwd_length_lref1_aux/ qed-. +(* Basic inversion lemmas ***************************************************) + +fact fqu_inv_eq_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → + G1 = G2 → |L1| = |L2| → T1 = T2 → ⊥. +#G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2 normalize +/2 width=4 by discr_tpair_xy_y, discr_tpair_xy_x, plus_xSy_x_false/ +#G #L #K #T #U #e #HLK #_ #_ #H #_ -G -T -U >(drop_fwd_length … HLK) in H; -L +/2 width=4 by plus_xySz_x_false/ +qed-. + +lemma fqu_inv_eq: ∀G,L1,L2,T. ⦃G, L1, T⦄ ⊐ ⦃G, L2, T⦄ → |L1| = |L2| → ⊥. +#G #L1 #L2 #T #H #H0 @(fqu_inv_eq_aux … H … H0) // (**) (* full auto fails *) +qed-. + (* Advanced eliminators *****************************************************) lemma fqu_wf_ind: ∀R:relation3 …. ( diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml index ca4970bcb..9f2c61a64 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml @@ -44,11 +44,11 @@ for context-sensitive computation on terms. - strong qrst-normalization + Strong qrst-normalization for simply typed terms. - lazy equivalence on local environments + Lazy equivalence on local environments addded as q-step to rst-computation on closures (anniversary milestone). -- 2.39.2