From: Ferruccio Guidi Date: Mon, 19 Mar 2018 19:12:15 +0000 (+0100) Subject: update in basic_2 X-Git-Tag: make_still_working~350 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=afd4afa9489fa65019ad7cdc274e261f6993b871 update in basic_2 + advances on fpbg + Makefile update --- diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile index ff89218d2..a340e2ef3 100644 --- a/matita/matita/contribs/lambdadelta/Makefile +++ b/matita/matita/contribs/lambdadelta/Makefile @@ -28,7 +28,10 @@ ORIGS := basic_2/basic_1.orig CONTRIB := lambdadelta_2 -TAGS := all xoa xoa2 orig elim deps top leaf stats tbls trim contrib clean +WWW := ../../../../helm/www/lambdadelta + +TAGS := all xoa xoa2 orig elim deps top leaf stats tbls trim contrib clean \ + www up-html PACKAGES := ground_2 basic_2 apps_2 alpha_1 XPACKAGES := ground_2 basic_2 @@ -257,7 +260,17 @@ contrib: # clean ###################################################################### clean: - @$(RM) `find -name "*~" -type f -print` + $(H)$(RM) `find -name "*~" -type f -print` + +# www ###################################################################### + +www: + $(H)$(MAKE) --no-print-directory -C $(WWW) www + +# www ###################################################################### + +up-html: + $(H)$(MAKE) --no-print-directory -C $(WWW) up-html ############################################################################## diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs.etc index 05e7c375d..920d114f5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs.etc @@ -3,14 +3,3 @@ lemma cprs_cpxs: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈* T2 → ⦃G, L⦄ ⊢ #h #o #G #L #T1 #T2 #H @(cprs_ind … H) -T2 /3 width=3 by cpxs_strap1, cpr_cpx/ qed. - -lemma cpxs_neq_inv_step_sn: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 = T2 → ⊥) → - ∃∃T. ⦃G, L⦄ ⊢ T1 ⬈[h] T & T1 = T → ⊥ & ⦃G, L⦄ ⊢ T ⬈*[h] T2. -#h #o #G #L #T1 #T2 #H @(cpxs_ind_dx … H) -T1 -[ #H elim H -H // -| #T1 #T #H1 #H2 #IH2 #H12 elim (eq_term_dec T1 T) #H destruct - [ -H1 -H2 /3 width=1 by/ - | -IH2 /3 width=4 by ex3_intro/ (**) (* auto fails without clear *) - ] -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg_lift.etc index 4fe3be22f..04110fe21 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg_lift.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg_lift.etc @@ -22,3 +22,7 @@ include "basic_2/computation/fpbg.ma". lemma sta_fpbg: ∀h,o,G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 ▪[h, o] d+1 → ⦃G, L⦄ ⊢ T1 •*[h, 1] T2 → ⦃G, L, T1⦄ >≛[h, o] ⦃G, L, T2⦄. /4 width=2 by fpb_fpbg, sta_fpb/ qed. + +lemma lstas_fpbg: ∀h,o,G,L,T1,T2,d2. ⦃G, L⦄ ⊢ T1 •*[h, d2] T2 → (T1 = T2 → ⊥) → + ∀d1. d2 ≤ d1 → ⦃G, L⦄ ⊢ T1 ▪[h, o] d1 → ⦃G, L, T1⦄ >≛[h, o] ⦃G, L, T2⦄. +/3 width=5 by lstas_cpxs, cpxs_fpbg/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazybtpredstarproper_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazybtpredstarproper_8.ma deleted file mode 100644 index b1dcc127a..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazybtpredstarproper_8.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ >≡ [ break term 46 h, break term 46 o ] ⦃ break term 46 G2, break term 46 L2, break term 46 T2 ⦄ )" - non associative with precedence 45 - for @{ 'LazyBTPRedStarProper $h $o $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubtystarproper_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubtystarproper_8.ma new file mode 100644 index 000000000..15b61d624 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubtystarproper_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 o ] ⦃ break term 46 G2, break term 46 L2, break term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'PRedSubTyStarProper $h $o $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma index f1bb3e025..2a60dd3d4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma @@ -145,5 +145,3 @@ elim (cpx_inv_cast1 … HU2) -HU2 /3 width=3 by cpxs_strap1, or3_intro1, or3_int lapply (cpxs_strap1 … HW1 … HW2) -W lapply (cpxs_strap1 … HT1 … HT2) -T /3 width=5 by or3_intro0, ex3_2_intro/ qed-. - -(* Basic_2A1: removed theorems 1: cpxs_neq_inv_step_sn *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tdeq.ma index 10433b267..3d1fa9e71 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tdeq.ma @@ -27,16 +27,19 @@ lemma tdeq_cpxs_trans: ∀h,o,U1,T1. U1 ≛[h, o] T1 → ∀G,L,T2. ⦃G, L⦄ qed-. (* Note: this requires tdeq to be symmetric *) -lemma cpxs_tdneq_inv_step_sn: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≛[h, o] T2 → ⊥) → +(* Nasic_2A1: uses: cpxs_neq_inv_step_sn *) +lemma cpxs_tdneq_fwd_step_sn: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≛[h, o] T2 → ⊥) → ∃∃T,T0. ⦃G, L⦄ ⊢ T1 ⬈[h] T & T1 ≛[h, o] T → ⊥ & ⦃G, L⦄ ⊢ T ⬈*[h] T0 & T0 ≛[h, o] T2. #h #o #G #L #T1 #T2 #H @(cpxs_ind_dx … H) -T1 [ #H elim H -H // -| #T1 #T #H1 #H2 #IH #Hn12 elim (tdeq_dec h o T1 T) #H destruct - [ -H1 -H2 elim IH -IH /3 width=3 by tdeq_trans/ -Hn12 - #X #X2 #HTX #HnTX #HX2 #HXT2 elim (tdeq_cpx_trans … H … HTX) -HTX - #X1 #HTX1 #HX1 elim (tdeq_cpxs_trans … HX1 … HX2) -HX2 - /5 width=8 by tdeq_canc_sn, tdeq_trans, ex4_2_intro/ (* Note: 2 tdeq_trans *) - | -IH -Hn12 /3 width=6 by ex4_2_intro/ +| #T1 #T0 #HT10 #HT02 #IH #Hn12 + elim (tdeq_dec h o T1 T0) [ -HT10 -HT02 #H10 | -IH #Hn10 ] + [ elim IH -IH /3 width=3 by tdeq_trans/ -Hn12 + #T3 #T4 #HT03 #Hn03 #HT34 #H42 + elim (tdeq_cpx_trans … H10 … HT03) -HT03 #T5 #HT15 #H53 + elim (tdeq_cpxs_trans … H53 … HT34) -HT34 #T6 #HT56 #H64 + /5 width=8 by tdeq_canc_sn, (* 2x *) tdeq_trans, ex4_2_intro/ + | /3 width=6 by ex4_2_intro/ ] ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma index 87a5e890f..a709858ad 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma @@ -50,9 +50,9 @@ lapply (tdneq_tdeq_canc_dx … H … HV02) -H #HnTV0 elim (tdeq_dec h o T1 T0) #H [ lapply (tdeq_tdneq_trans … H … HnTV0) -H -HnTV0 #Hn10 lapply (cpxs_trans … HT10 … HTV0) -T0 #H10 - elim (cpxs_tdneq_inv_step_sn … H10 … Hn10) -H10 -Hn10 + elim (cpxs_tdneq_fwd_step_sn … H10 … Hn10) -H10 -Hn10 /3 width=8 by tdeq_trans/ -| elim (cpxs_tdneq_inv_step_sn … HT10 … H) -HT10 -H #T #V #HT1 #HnT1 #HTV #HVT0 +| elim (cpxs_tdneq_fwd_step_sn … HT10 … H) -HT10 -H #T #V #HT1 #HnT1 #HTV #HVT0 elim (tdeq_cpxs_trans … HVT0 … HTV0) -T0 /3 width=8 by cpxs_trans, tdeq_trans/ ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma index 49376aad6..de77a268f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma @@ -12,28 +12,39 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/lazybtpredstarproper_8.ma". -include "basic_2/reduction/fpb.ma". -include "basic_2/computation/fpbs.ma". +include "basic_2/notation/relations/predsubtystarproper_8.ma". +include "basic_2/rt_transition/fpb.ma". +include "basic_2/rt_computation/fpbs.ma". -(* "QRST" PROPER PARALLEL COMPUTATION FOR CLOSURES **************************) +(* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************) definition fpbg: ∀h. sd h → tri_relation genv lenv term ≝ λh,o,G1,L1,T1,G2,L2,T2. ∃∃G,L,T. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G, L, T⦄ & ⦃G, L, T⦄ ≥[h, o] ⦃G2, L2, T2⦄. -interpretation "'qrst' proper parallel computation (closure)" - 'LazyBTPRedStarProper h o G1 L1 T1 G2 L2 T2 = (fpbg h o G1 L1 T1 G2 L2 T2). +interpretation "proper parallel rst-computation (closure)" + 'PRedSubTyStarProper h o G1 L1 T1 G2 L2 T2 = (fpbg h o G1 L1 T1 G2 L2 T2). (* Basic properties *********************************************************) lemma fpb_fpbg: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄. + ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄. /2 width=5 by ex2_3_intro/ qed. lemma fpbg_fpbq_trans: ∀h,o,G1,G,G2,L1,L,L2,T1,T,T2. - ⦃G1, L1, T1⦄ >≛[h, o] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≽[h, o] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄. + ⦃G1, L1, T1⦄ >[h, o] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≽[h, o] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄. #h #o #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 * /3 width=9 by fpbs_strap1, ex2_3_intro/ qed-. + +(* Note: this is used in the closure proof *) +lemma fpbg_fpbs_trans: ∀h,o,G,G2,L,L2,T,T2. ⦃G, L, T⦄ ≥[h, o] ⦃G2, L2, T2⦄ → + ∀G1,L1,T1. ⦃G1, L1, T1⦄ >[h, o] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄. +#h #o #G #G2 #L #L2 #T #T2 #H @(fpbs_ind_dx … H) -G -L -T /3 width=5 by fpbg_fpbq_trans/ +qed-. + +(* Basic_2A1: uses: fpbg_fleq_trans *) +lemma fpbg_ffdeq_trans: ∀h,o,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ >[h, o] ⦃G, L, T⦄ → + ∀G2,L2,T2. ⦃G, L, T⦄ ≛[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄. +/3 width=5 by fpbg_fpbq_trans, fpbq_ffdeq/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_cpxs.ma new file mode 100644 index 000000000..ee1e1ecad --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_cpxs.ma @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/rt_computation/cpxs_tdeq.ma". +include "basic_2/rt_computation/fpbs_cpxs.ma". +include "basic_2/rt_computation/fpbg.ma". + +(* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES **************************) + +(* Properties with uncounted context-sensitive parallel rt-computation ******) + +(* Basic_2A1: was: cpxs_fpbg *) +lemma cpxs_tdneq_fpbg: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → + (T1 ≛[h, o] T2 → ⊥) → ⦃G, L, T1⦄ >[h, o] ⦃G, L, T2⦄. +#h #o #G #L #T1 #T2 #H #H0 +elim (cpxs_tdneq_fwd_step_sn … H … H0) -H -H0 +/4 width=5 by cpxs_tdeq_fpbs, fpb_cpx, ex2_3_intro/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fleq.ma deleted file mode 100644 index 2196b8ad1..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fleq.ma +++ /dev/null @@ -1,73 +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/multiple/fleq_fleq.ma". -include "basic_2/reduction/fpbq_alt.ma". -include "basic_2/computation/fpbg.ma". - -(* "QRST" PROPER PARALLEL COMPUTATION FOR CLOSURES **************************) - -(* Properties on lazy equivalence for closures ******************************) - -lemma fpbg_fleq_trans: ∀h,o,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ >≛[h, o] ⦃G, L, T⦄ → - ∀G2,L2,T2. ⦃G, L, T⦄ ≡[0] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄. -/3 width=5 by fpbg_fpbq_trans, fleq_fpbq/ qed-. - -lemma fleq_fpbg_trans: ∀h,o,G,G2,L,L2,T,T2. ⦃G, L, T⦄ >≛[h, o] ⦃G2, L2, T2⦄ → - ∀G1,L1,T1. ⦃G1, L1, T1⦄ ≡[0] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄. -#h #o #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,o,G1,G2,L1,L2,T1,T2. - ⦃G1, L1, T1⦄ ≡[0] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 * /2 width=1 by lleq_fpbs/ -qed. - -lemma fpbg_fwd_fpbs: ∀h,o,G1,G2,L1,L2,T1,T2. - ⦃G1, L1, T1⦄ >≛[h,o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 * -/3 width=5 by fpbs_strap2, fpb_fpbq/ -qed-. - -lemma fpbs_fpbg: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ ≡[0] ⦃G2, L2, T2⦄ ∨ - ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄. -#h #o #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_fpb_trans: ∀h,o,F1,F2,K1,K2,T1,T2. ⦃F1, K1, T1⦄ ≥[h, o] ⦃F2, K2, T2⦄ → - ∀G2,L2,U2. ⦃F2, K2, T2⦄ ≻[h, o] ⦃G2, L2, U2⦄ → - ∃∃G1,L1,U1. ⦃F1, K1, T1⦄ ≻[h, o] ⦃G1, L1, U1⦄ & ⦃G1, L1, U1⦄ ≥[h, o] ⦃G2, L2, U2⦄. -#h #o #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/rt_computation/fpbg_fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbg.ma index 28748f278..636f20955 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbg.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "basic_2/computation/fpbg_fpbs.ma". +include "basic_2/rt_computation/fpbg_fpbs.ma". -(* "QRST" PROPER PARALLEL COMPUTATION FOR CLOSURES **************************) +(* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************) (* Main properties **********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbs.ma index 2118c2c16..b188e7880 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbs.ma @@ -12,57 +12,83 @@ (* *) (**************************************************************************) -include "basic_2/computation/lpxs_lleq.ma". -include "basic_2/computation/fpbs_lift.ma". -include "basic_2/computation/fpbg_fleq.ma". +include "basic_2/static/ffdeq_fqup.ma". +include "basic_2/static/ffdeq_ffdeq.ma". +include "basic_2/rt_transition/fpbq_fpb.ma". +include "basic_2/rt_computation/fpbg.ma". -(* "QRST" PROPER PARALLEL COMPUTATION FOR CLOSURES **************************) +(* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************) -(* Properties on "qrst" parallel reduction on closures **********************) +(* Advanced forward lemmas **************************************************) + +lemma fpbg_fwd_fpbs: ∀h,o,G1,G2,L1,L2,T1,T2. + ⦃G1, L1, T1⦄ >[h,o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 * +/3 width=5 by fpbs_strap2, fpb_fpbq/ +qed-. + +(* Advanced properties with degree-based equivalence on closures ************) + +(* Basic_2A1: uses: fleq_fpbg_trans *) +lemma ffdeq_fpbg_trans: ∀h,o,G,G2,L,L2,T,T2. ⦃G, L, T⦄ >[h, o] ⦃G2, L2, T2⦄ → + ∀G1,L1,T1. ⦃G1, L1, T1⦄ ≛[h, o] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄. +#h #o #G #G2 #L #L2 #T #T2 * #G0 #L0 #T0 #H0 #H02 #G1 #L1 #T1 #H1 +elim (ffdeq_fpb_trans … H1 … H0) -G -L -T +/4 width=9 by fpbs_strap2, fpbq_ffdeq, ex2_3_intro/ +qed-. + +(* Properties with parallel proper rst-reduction on closures ****************) lemma fpb_fpbg_trans: ∀h,o,G1,G,G2,L1,L,L2,T1,T,T2. - ⦃G1, L1, T1⦄ ≻[h, o] ⦃G, L, T⦄ → ⦃G, L, T⦄ >≛[h, o] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄. + ⦃G1, L1, T1⦄ ≻[h, o] ⦃G, L, T⦄ → ⦃G, L, T⦄ >[h, o] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄. /3 width=5 by fpbg_fwd_fpbs, ex2_3_intro/ qed-. +(* Properties with parallel rst-reduction on closures ***********************) + lemma fpbq_fpbg_trans: ∀h,o,G1,G,G2,L1,L,L2,T1,T,T2. - ⦃G1, L1, T1⦄ ≽[h, o] ⦃G, L, T⦄ → ⦃G, L, T⦄ >≛[h, o] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄. -#h #o #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/ + ⦃G1, L1, T1⦄ ≽[h, o] ⦃G, L, T⦄ → ⦃G, L, T⦄ >[h, o] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄. +#h #o #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2 +elim (fpbq_inv_fpb … H1) -H1 +/2 width=5 by ffdeq_fpbg_trans, fpb_fpbg_trans/ qed-. -(* Properties on "qrst" parallel compuutation on closures *******************) +(* Properties with parallel rst-compuutation on closures ********************) lemma fpbs_fpbg_trans: ∀h,o,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G, L, T⦄ → - ∀G2,L2,T2. ⦃G, L, T⦄ >≛[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄. + ∀G2,L2,T2. ⦃G, L, T⦄ >[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄. #h #o #G1 #G #L1 #L #T1 #T #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,o,G,G2,L,L2,T,T2. ⦃G, L, T⦄ ≥[h, o] ⦃G2, L2, T2⦄ → - ∀G1,L1,T1. ⦃G1, L1, T1⦄ >≛[h, o] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄. -#h #o #G #G2 #L #L2 #T #T2 #H @(fpbs_ind_dx … H) -G -L -T /3 width=5 by fpbg_fpbq_trans/ +(* Advanced inversion lemmas of parallel rst-computation on closures ********) + +(* Basic_2A1: was: fpbs_fpbg *) +lemma fpbs_inv_fpbg: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → + ∨∨ ⦃G1, L1, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄ + | ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind … H) -G2 -L2 -T2 +[ /2 width=1 by or_introl/ +| #G #G2 #L #L2 #T #T2 #_ #H2 * #H1 + elim (fpbq_inv_fpb … H2) -H2 #H2 + [ /3 width=5 by ffdeq_trans, or_introl/ + | elim (ffdeq_fpb_trans … H1 … H2) -G -L -T + /4 width=5 by ex2_3_intro, or_intror, ffdeq_fpbs/ + | /3 width=5 by fpbg_ffdeq_trans, or_intror/ + | /4 width=5 by fpbg_fpbq_trans, fpb_fpbq, or_intror/ + ] +] qed-. -(* Note: this is used in the closure proof *) -lemma fqup_fpbg: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim (fqup_inv_step_sn … H) -H -/3 width=5 by fqus_fpbs, fpb_fqu, ex2_3_intro/ -qed. - -lemma cpxs_fpbg: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, o] T2 → - (T1 = T2 → ⊥) → ⦃G, L, T1⦄ >≛[h, o] ⦃G, L, T2⦄. -#h #o #G #L #T1 #T2 #H #H0 elim (cpxs_neq_inv_step_sn … H … H0) -H -H0 -/4 width=5 by cpxs_fpbs, fpb_cpx, ex2_3_intro/ -qed. - -lemma lstas_fpbg: ∀h,o,G,L,T1,T2,d2. ⦃G, L⦄ ⊢ T1 •*[h, d2] T2 → (T1 = T2 → ⊥) → - ∀d1. d2 ≤ d1 → ⦃G, L⦄ ⊢ T1 ▪[h, o] d1 → ⦃G, L, T1⦄ >≛[h, o] ⦃G, L, T2⦄. -/3 width=5 by lstas_cpxs, cpxs_fpbg/ qed. - -lemma lpxs_fpbg: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 → - (L1 ≡[T, 0] L2 → ⊥) → ⦃G, L1, T⦄ >≛[h, o] ⦃G, L2, T⦄. -#h #o #G #L1 #L2 #T #H #H0 elim (lpxs_nlleq_inv_step_sn … H … H0) -H -H0 -/4 width=5 by fpb_lpx, lpxs_lleq_fpbs, ex2_3_intro/ -qed. +(* Advanced properties of parallel rst-computation on closures **************) + +lemma fpbs_fpb_trans: ∀h,o,F1,F2,K1,K2,T1,T2. ⦃F1, K1, T1⦄ ≥[h, o] ⦃F2, K2, T2⦄ → + ∀G2,L2,U2. ⦃F2, K2, T2⦄ ≻[h, o] ⦃G2, L2, U2⦄ → + ∃∃G1,L1,U1. ⦃F1, K1, T1⦄ ≻[h, o] ⦃G1, L1, U1⦄ & ⦃G1, L1, U1⦄ ≥[h, o] ⦃G2, L2, U2⦄. +#h #o #F1 #F2 #K1 #K2 #T1 #T2 #H elim (fpbs_inv_fpbg … H) -H +[ #H12 #G2 #L2 #U2 #H2 elim (ffdeq_fpb_trans … H12 … H2) -F2 -K2 -T2 + /3 width=5 by ffdeq_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/rt_computation/fpbg_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqup.ma new file mode 100644 index 000000000..6cebf2c21 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqup.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/rt_computation/fpbs_fqup.ma". +include "basic_2/rt_computation/fpbg.ma". + +(* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************) + +(* Properties with plus-iterated structural successor for closures **********) + +(* Note: this is used in the closure proof *) +lemma fqup_fpbg: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim (fqup_inv_step_sn … H) -H +/3 width=5 by fqus_fpbs, fpb_fqu, ex2_3_intro/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_lfpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_lfpxs.ma new file mode 100644 index 000000000..bbed2be86 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_lfpxs.ma @@ -0,0 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||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_ffdeq.ma". +include "basic_2/computation/fpbg_ffdeq.ma". + +(* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES **************************) + +lemma lpxs_fpbg: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 → + (L1 ≡[T, 0] L2 → ⊥) → ⦃G, L1, T⦄ >≛[h, o] ⦃G, L2, T⦄. +#h #o #G #L1 #L2 #T #H #H0 elim (lpxs_nlleq_inv_step_sn … H … H0) -H -H0 +/4 width=5 by fpb_lpx, lpxs_lleq_fpbs, ex2_3_intro/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma index 2b13efb0e..74eae9335 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma @@ -53,7 +53,7 @@ lemma fpbs_strap2: ∀h,o,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≽[h, o] ⦃G, L, T⦄ ≥[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. /2 width=5 by tri_TC_strap/ qed-. -(* Basic_2A1: uses: lleq_fpbs *) +(* Basic_2A1: uses: lleq_fpbs fleq_fpbs *) lemma ffdeq_fpbs: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. /3 width=1 by fpbq_fpbs, fpbq_ffdeq/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpxs.ma index 479863b3e..8500d2ddd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpxs.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "basic_2/static/ffdeq_fqup.ma". include "basic_2/rt_computation/cpxs.ma". include "basic_2/rt_computation/fpbs_fqup.ma". @@ -36,6 +37,10 @@ lemma cpxs_fpbs_trans: ∀h,o,G1,G2,L1,L2,T,T2. ⦃G1, L1, T⦄ ≥[h, o] ⦃G2, /3 width=5 by fpbs_strap2, fpbq_cpx/ qed-. +lemma cpxs_tdeq_fpbs: ∀h,o,G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬈*[h] T → + ∀T2. T ≛[h, o] T2 → ⦃G, L, T1⦄ ≥[h, o] ⦃G, L, T2⦄. +/4 width=3 by cpxs_fpbs_trans, ffdeq_fpbs, tdeq_ffdeq/ qed. + (* Properties with star-iterated structural successor for closures **********) lemma cpxs_fqus_fpbs: ∀h,o,G1,L1,T1,T. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] T → diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt index 6516dbc12..09efad79b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -7,3 +7,4 @@ csx_vector.ma csx_cnx_vector.ma csx_csx_vector.ma lfsx.ma lfsx_drops.ma lfsx_fqup.ma lfsx_lpx.ma lfsx_lpxs.ma lfsx_lfpxs.ma lfsx_csx.ma lfsx_lfsx.ma lsubsx.ma lsubsx_lfsx.ma lsubsx_lsubsx.ma fpbs.ma fpbs_fqup.ma fpbs_fqus.ma fpbs_aaa.ma fpbs_fpb.ma fpbs_cpxs.ma fpbs_lfpxs.ma fpbs_csx.ma fpbs_fpbs.ma +fpbg.ma fpbg_fqup.ma fpbg_cpxs.ma fpbg_fpbs.ma fpbg_fpbg.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq_fqup.ma index 5d1288abb..15baed91f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq_fqup.ma @@ -17,6 +17,12 @@ include "basic_2/static/ffdeq.ma". (* DEGREE-BASED EQUIVALENCE FOR CLOSURES ON REFERRED ENTRIES ****************) +(* Properties with degree-based equivalence for terms ***********************) + +lemma tdeq_ffdeq: ∀h,o,T1,T2. T1 ≛[h, o] T2 → + ∀G,L. ⦃G, L, T1⦄ ≛[h, o] ⦃G, L, T2⦄. +/2 width=1 by ffdeq_intro_sn/ qed. + (* Advanced properties ******************************************************) lemma ffdeq_refl: ∀h,o. tri_reflexive … (ffdeq h o). 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 7c3e2412b..9bf043c34 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 @@ -87,7 +87,7 @@ table { } ] [ { "parallel qrst-computation" * } { - [ [ "" ] "fpbg ( ⦃?,?,?⦄ >≛[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fleq" + "fpbg_fpbs" + "fpbg_fpbg" * ] + } ] [ { "decomposed rt-computation" * } { @@ -101,6 +101,7 @@ table { ] *) [ { "uncounted context-sensitive parallel rst-computation" * } { + [ [ "proper for closures" ] "fpbg" + "( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ )" "fpbg_fqup" + "fpbg_cpxs" + "fpbg_fpbs" + "fpbg_fpbg" * ] [ [ "for closures" ] "fpbs" + "( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_fqup" + "fpbs_fqus" + "fpbs_aaa" + "fpbs_fpb" + "fpbs_cpxs" + "fpbs_lfpxs" + "fpbs_csx" + "fpbs_fpbs" * ] } ]