From ac7479f9a292448d12761da4345d668d74b8d308 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 22 Feb 2013 21:47:07 +0000 Subject: [PATCH] - "big tree" order implemented - some annotations --- .../contribs/lambdadelta/basic_2/basic_1.txt | 4 +- .../lambdadelta/basic_2/computation/ygt.ma | 95 +++++++++++++++++++ .../yprs_yprs.etc => computation/ygt_ygt.ma} | 6 +- .../dynamic/{snv_fpr.ma => snv_cpr.ma} | 40 +++++++- .../{snv_fpr_ssta.ma => snv_cpr_ssta.ma} | 75 +++++++-------- .../lambdadelta/basic_2/dynamic/snv_dxprs.ma | 69 ++++++++++++++ .../lambdadelta/basic_2/dynamic/snv_fprs.ma | 48 ---------- .../basic_2/equivalence/fpcs_cpcs.ma | 2 +- .../lambdadelta/basic_2/etc/csup/ypr.etc | 41 -------- .../lambdadelta/basic_2/etc/csup/yprs.etc | 52 ---------- .../basic_2/etc/csup/yprs_csups.etc | 25 ----- .../lambdadelta/basic_2/etc/csup/ysteps.etc | 47 --------- .../basic_2/etc/csup/ysteps_csups.etc | 28 ------ .../basic_2/grammar/lenv_weight.ma | 3 +- .../contribs/lambdadelta/basic_2/notation.ma | 8 ++ .../yprs_xprs.etc => reducibility/ysc.ma} | 22 ++--- .../lambdadelta/basic_2/substitution/lift.ma | 1 + 17 files changed, 266 insertions(+), 300 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/ygt.ma rename matita/matita/contribs/lambdadelta/basic_2/{etc/csup/yprs_yprs.etc => computation/ygt_ygt.ma} (86%) rename matita/matita/contribs/lambdadelta/basic_2/dynamic/{snv_fpr.ma => snv_cpr.ma} (66%) rename matita/matita/contribs/lambdadelta/basic_2/dynamic/{snv_fpr_ssta.ma => snv_cpr_ssta.ma} (79%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_dxprs.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_fprs.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/csup/ypr.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/csup/yprs.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/csup/yprs_csups.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/csup/ysteps.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/csup/ysteps_csups.etc rename matita/matita/contribs/lambdadelta/basic_2/{etc/csup/yprs_xprs.etc => reducibility/ysc.ma} (65%) diff --git a/matita/matita/contribs/lambdadelta/basic_2/basic_1.txt b/matita/matita/contribs/lambdadelta/basic_2/basic_1.txt index d64855d0d..817f67b9c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/basic_1.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/basic_1.txt @@ -44,9 +44,8 @@ arity/subst0 arity_fsubst0 arity/subst0 arity_subst0 asucc/fwd asucc_gen_sort asucc/fwd asucc_gen_head + cnt/props cnt_lift -C/props clt_wf__q_ind -C/props clt_wf_ind csuba/arity csuba_arity csuba/arity csuba_arity_rev @@ -119,7 +118,6 @@ leq/props leq_ahead_false_2 lift1/fwd lift1_cons_tail lift1/fwd lifts1_nil lift1/fwd lifts1_cons -lift/props thead_x_lift_y_y lift/props lifts_tapp lift/props lifts_inj llt/props lweight_repl diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/ygt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/ygt.ma new file mode 100644 index 000000000..e5140a8e7 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/ygt.ma @@ -0,0 +1,95 @@ +(**************************************************************************) +(* ___ *) +(* ||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/unwind/sstas.ma". +include "basic_2/reducibility/ysc.ma". +include "basic_2/computation/cprs.ma". + +(* "BIG TREE" ORDER FOR CLOSURES ********************************************) + +definition ygt: ∀h. sd h → bi_relation lenv term ≝ + λh,g. bi_TC … (ysc h g). + +interpretation "'big tree' order (closure)" + 'BTGreaterThan h g L1 T1 L2 T2 = (ygt h g L1 T1 L2 T2). + +(* Basic eliminators ********************************************************) + +lemma ygt_ind: ∀h,g,L1,T1. ∀R:relation2 lenv term. + (∀L2,T2. h ⊢ ⦃L1, T1⦄ ≻[g] ⦃L2, T2⦄ → R L2 T2) → + (∀L,T,L2,T2. h ⊢ ⦃L1, T1⦄ >[g] ⦃L, T⦄ → h ⊢ ⦃L, T⦄ ≻[g] ⦃L2, T2⦄ → R L T → R L2 T2) → + ∀L2,T2. h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄ → R L2 T2. +#h #g #L1 #T1 #R #IH1 #IH2 #L2 #T2 #H +@(bi_TC_ind … IH1 IH2 L2 T2 H) +qed-. (**) (* /3 width=6 by bi_TC_ind/ fails *) + +lemma ygt_ind_dx: ∀h,g,L2,T2. ∀R:relation2 lenv term. + (∀L1,T1. h ⊢ ⦃L1, T1⦄ ≻[g] ⦃L2, T2⦄ → R L1 T1) → + (∀L1,L,T1,T. h ⊢ ⦃L1, T1⦄ ≻[g] ⦃L, T⦄ → h ⊢ ⦃L, T⦄ >[g] ⦃L2, T2⦄ → R L T → R L1 T1) → + ∀L1,T1. h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄ → R L1 T1. +/3 width=6 by bi_TC_ind_dx/ qed-. + +(* Basic properties *********************************************************) + +lemma ygt_strap1: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ >[g] ⦃L, T⦄ → + h ⊢ ⦃L, T⦄ ≻[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄. +/2 width=4/ qed-. + +lemma ygt_strap2: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ ≻[g] ⦃L, T⦄ → + h ⊢ ⦃L, T⦄ >[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄. +/2 width=4/ qed-. + +lemma ygt_cprs_trans: ∀h,g,L1,L,T1,T. h ⊢ ⦃L1, T1⦄ >[g] ⦃L, T⦄ → + ∀T2. L ⊢ T ➡* T2 → h ⊢ ⦃L1, T1⦄ >[g] ⦃L, T2⦄. +#h #g #L1 #L #T1 #T #HLT1 #T2 #H @(cprs_ind … H) -T2 // +#T0 #T2 #_ #HT02 #IHT0 -HLT1 +elim (term_eq_dec T0 T2) #HT02 destruct // +@(ygt_strap1 … IHT0) /3 width=1/ +qed-. + +lemma ygt_sstas_trans: ∀h,g,L1,L,T1,T. h ⊢ ⦃L1, T1⦄ >[g] ⦃L, T⦄ → + ∀T2. ⦃h, L⦄ ⊢ T •*[g] T2 → h ⊢ ⦃L1, T1⦄ >[g] ⦃L, T2⦄. +#h #g #L1 #L #T1 #T #HLT1 #T2 #H @(sstas_ind … H) -T2 // +#T0 #T2 #l #_ #HT02 #IHT0 -HLT1 +@(ygt_strap1 … IHT0) -IHT0 /2 width=2/ +qed-. + +lemma cprs_ygt_trans: ∀h,g,L,T1,T. L ⊢ T1 ➡* T → + ∀L2,T2. h ⊢ ⦃L, T⦄ >[g] ⦃L2, T2⦄ → h ⊢ ⦃L, T1⦄ >[g] ⦃L2, T2⦄. +#h #g #L #T1 #T #H @(cprs_ind … H) -T // +#T0 #T #_ #HT0 #IHT10 #L2 #T2 #HLT2 +elim (term_eq_dec T0 T) #HT0 destruct /2 width=1/ +@IHT10 -IHT10 @(ygt_strap2 … HLT2) /3 width=1/ +qed-. + +lemma sstas_ygt_trans: ∀h,g,L,T1,T. ⦃h, L⦄ ⊢ T1 •*[g] T → + ∀L2,T2. h ⊢ ⦃L, T⦄ >[g] ⦃L2, T2⦄ → h ⊢ ⦃L, T1⦄ >[g] ⦃L2, T2⦄. +#h #g #L #T1 #T #H @(sstas_ind … H) -T // +#T0 #T #l #_ #HT0 #IHT10 #L2 #T2 #HLT2 +@IHT10 -IHT10 @(ygt_strap2 … HLT2) /2 width=2/ +qed-. + +lemma fw_ygt: ∀h,g,L1,L2,T1,T2. ♯{L2, T2} < ♯{L1, T1} → h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄. +/3 width=1/ qed. + +lemma cprs_ygt: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) → h ⊢ ⦃L, T1⦄ >[g] ⦃L, T2⦄. +#h #g #L #T1 #T2 #H @(cprs_ind … H) -T2 +[ #H elim H -H // +| #T #T2 #_ #HT2 #IHT1 #H + elim (term_eq_dec T1 T) #HT1 destruct + [ -IHT1 /4 width=1 by ysc_cpr, bi_inj/ (**) (* auto too slow without trace *) + | -H /4 width=3 by inj, ygt_cprs_trans/ + ] +] +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/yprs_yprs.etc b/matita/matita/contribs/lambdadelta/basic_2/computation/ygt_ygt.ma similarity index 86% rename from matita/matita/contribs/lambdadelta/basic_2/etc/csup/yprs_yprs.etc rename to matita/matita/contribs/lambdadelta/basic_2/computation/ygt_ygt.ma index d737dd817..0c2ae2995 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/yprs_yprs.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/ygt_ygt.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "basic_2/computation/yprs.ma". +include "basic_2/computation/ygt.ma". -(* HYPER PARALLEL COMPUTATION ON TERMS **************************************) +(* "BIG TREE" ORDER FOR CLOSURES ********************************************) -theorem yprs_trans: ∀h,g. bi_transitive … (yprs h g). +theorem ygt_trans: ∀h,g. bi_transitive … (ygt h g). /2 width=4/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_fpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpr.ma similarity index 66% rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_fpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpr.ma index a4aca4b61..a4850ff61 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_fpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpr.ma @@ -12,14 +12,14 @@ (* *) (**************************************************************************) -include "basic_2/dynamic/snv_lift.ma". -include "basic_2/dynamic/snv_fpr_ssta.ma". +include "basic_2/dynamic/snv_ltpss_sn.ma". +include "basic_2/dynamic/snv_cpr_ssta.ma". (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) (* Properties on context-free parallel reduction for closures ***************) -fact snv_ltpr_tpr_aux: ∀h,g,n. ( +axiom snv_ltpr_tpr_aux: ∀h,g,n. ( ∀L1,T1. ♯{L1, T1} < n → ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → ⦃h, L1⦄ ⊩ T1 :[g] → @@ -30,6 +30,7 @@ fact snv_ltpr_tpr_aux: ∀h,g,n. ( ) → ∀L1,T1. ♯{L1, T1} = n → ⦃h, L1⦄ ⊩ T1 :[g] → ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → ⦃h, L2⦄ ⊩ T2 :[g]. +(* #h #g #n #IH2 #IH1 #L1 * * [||||*] [ #k #Hn #H1 #L2 #_ #X #H2 destruct -IH2 -IH1 -L1 >(tpr_inv_atom1 … H2) -X // @@ -77,3 +78,36 @@ fact snv_ltpr_tpr_aux: ∀h,g,n. ( elim (IH2 … HVW1 … HL12 … HV12 HV1) -IH2 -HVW1 -HV12 -HV1 // #W2 #HVW2 #HW12 lapply (fpcs_canc_sn L1 L1 … W10 W1 … HW12) -HW12 /3 width=1/ -W10 #HW12 @(snv_appl … HV2 HT2 HVW2) +*) + +fact snv_cpr_aux: ∀h,g,n. ( + ∀L1,T1. ♯{L1, T1} < n → + ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → + ∀L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀T2. L2 ⊢ T1 ➡ T2 → ⦃h, L1⦄ ⊩ T1 :[g] → + ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄ + ) → ( + ∀L1,T1. ♯{L1, T1} < n → ⦃h, L1⦄ ⊩ T1 :[g] → + ∀L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀T2. ⦃h, L2⦄ ⊢ T1 •*➡*[g] T2 → ⦃h, L2⦄ ⊩ T2 :[g] + ) → + ∀L1,T1. ♯{L1, T1} = n → ⦃h, L1⦄ ⊩ T1 :[g] → + ∀T2. L1 ⊢ T1 ➡ T2 → ⦃h, L1⦄ ⊩ T2 :[g]. +#h #g #n #IH2 #IH1 #L1 #T1 #Hn #HT1 #T2 * #T0 #HT10 #HT02 +lapply (snv_ltpr_tpr_aux … Hn HT1 … HT10) -Hn -HT1 -HT10 [ // | skip | /3 width=6/ | /3 width=5/ ] -n -T1 #HT0 +lapply (snv_tpss_conf … HT0 … HT02) -T0 // +qed-. + +fact snv_lfpr_aux: ∀h,g,n. ( + ∀L1,T1. ♯{L1, T1} < n → + ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → + ∀L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀T2. L2 ⊢ T1 ➡ T2 → ⦃h, L1⦄ ⊩ T1 :[g] → + ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄ + ) → ( + ∀L1,T1. ♯{L1, T1} < n → ⦃h, L1⦄ ⊩ T1 :[g] → + ∀L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀T2. ⦃h, L2⦄ ⊢ T1 •*➡*[g] T2 → ⦃h, L2⦄ ⊩ T2 :[g] + ) → + ∀L1,T1. ♯{L1, T1} = n → ⦃h, L1⦄ ⊩ T1 :[g] → + ∀L2. ⦃L1⦄ ➡ ⦃L2⦄ → ⦃h, L2⦄ ⊩ T1 :[g]. +#h #g #n #IH2 #IH1 #L1 #T1 #Hn #HT1 #L2 * #L #HL1 #HL2 +lapply (snv_ltpr_tpr_aux … Hn HT1 … HL1 ??) -Hn -HT1 -HL1 [ // | skip | /3 width=6/ | /3 width=5/ ] -n -L1 #HT1 +lapply (snv_ltpss_sn_conf … HL2 … HT1) -L // +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_fpr_ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpr_ssta.ma similarity index 79% rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_fpr_ssta.ma rename to matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpr_ssta.ma index 028ca6292..9aa991939 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_fpr_ssta.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpr_ssta.ma @@ -21,7 +21,7 @@ include "basic_2/dynamic/snv_ssta.ma". (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) -(* Properties on context-free parallel reduction for closures ***************) +(* Properties on context-sensitive parallel reduction for terms *************) fact ssta_ltpr_tpr_aux: ∀h,g,n. ( ∀L,T2. ♯{L,T2} < n → @@ -135,33 +135,7 @@ fact ssta_ltpr_tpr_aux: ∀h,g,n. ( ] qed-. -fact ssta_ltpr_cpr_aux: ∀h,g,n. ( - ∀L,T2. ♯{L,T2} < n → - ∀T1. L ⊢ T1 ⬌* T2 → ⦃h, L⦄ ⊩ T1 :[g] → ⦃h, L⦄ ⊩ T2 :[g] → - ∀U1,l1. ⦃h, L⦄ ⊢ T1 •[g, l1] U1 → - ∀U2,l2. ⦃h, L⦄ ⊢ T2 •[g, l2] U2 → - L ⊢ U1 ⬌* U2 ∧ l1 = l2 - ) → ( - ∀L,T. ♯{L,T} < n → ⦃h, L⦄ ⊩ T :[g] → - ∀U,l. ⦃h, L⦄ ⊢ T •[g, l + 1] U → ⦃h, L⦄ ⊩ U :[g] - ) → ( - ∀L1,T1. ♯{L1,T1} < n → - ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → - ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡ T2 → ⦃h, L1⦄ ⊩ T1 :[g] → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄ - ) → - ∀L1,T1. ♯{L1,T1} = n → - ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → - ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡ T2 → ⦃h, L1⦄ ⊩ T1 :[g] → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄. -#h #g #n #IH3 #IH2 #IH1 #L1 #T1 #Hn #U1 #l #HTU1 #L2 #HL12 #T2 * #T0 #HT10 #HT02 #HT1 -elim (ssta_ltpr_tpr_aux … IH3 IH2 … Hn … HTU1 … HL12 … HT10 HT1) --T1 -IH3 -IH2 -HL12 [2: /3 width=5/ ] -n #U0 #HTU0 #HU10 -elim (ssta_tpss_conf … HTU0 … HT02) -T0 #U2 #HTU2 #HU02 -lapply (fpcs_fpr_strap1 … HU10 L2 U2 ?) -HU10 /2 width=3/ -HTU2 /3 width=3/ -qed-. - -fact ssta_fpr_aux: ∀h,g,n. ( +fact ssta_cpr_aux: ∀h,g,n. ( ∀L,T2. ♯{L,T2} < n → ∀T1. L ⊢ T1 ⬌* T2 → ⦃h, L⦄ ⊩ T1 :[g] → ⦃h, L⦄ ⊩ T2 :[g] → ∀U1,l1. ⦃h, L⦄ ⊢ T1 •[g, l1] U1 → @@ -173,17 +147,44 @@ fact ssta_fpr_aux: ∀h,g,n. ( ) → ( ∀L1,T1. ♯{L1,T1} < n → ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → - ∀L2,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → ⦃h, L1⦄ ⊩ T1 :[g] → + ∀L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀T2. L2 ⊢ T1 ➡ T2 → ⦃h, L1⦄ ⊩ T1 :[g] → ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄ ) → ∀L1,T1. ♯{L1,T1} = n → ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → - ∀L2,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → ⦃h, L1⦄ ⊩ T1 :[g] → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄. -#h #g #n #IH3 #IH2 #IH1 #L1 #T1 #Hn #U1 #l #HTU1 #L2 #T2 #H12 #HT1 -elim (fpr_inv_all … H12) -H12 #L #HL1 #HT12 #HL2 -elim (ssta_ltpr_cpr_aux … IH3 IH2 … Hn … HTU1 … HL1 … HT12 HT1) --T1 -IH3 -IH2 -HL1 [2: /3 width=5/ ] -n #U #HTU #HU1 -elim (ssta_ltpss_sn_conf … HTU … HL2) -HTU #U2 #HTU2 #HU2 -lapply (fpcs_fpr_strap1 … HU1 L2 U2 ?) -HU1 /2 width=3/ -HTU2 /3 width=4/ + ∀T2. L1 ⊢ T1 ➡ T2 → ⦃h, L1⦄ ⊩ T1 :[g] → + ∃∃U2. ⦃h, L1⦄ ⊢ T2 •[g, l] U2 & L1 ⊢ U1 ⬌* U2. +#h #g #n #IH3 #IH2 #IH1 #L1 #T1 #Hn #U1 #l #HTU1 #T2 * #T0 #HT10 #HT02 #HT1 +elim (ssta_ltpr_tpr_aux … IH3 IH2 … Hn … HTU1 … HT10 HT1) +-T1 -IH3 -IH2 [3: // |2: skip |4: /3 width=5/ ] -n #U0 #HTU0 #HU10 +lapply (fpcs_inv_cpcs … HU10) -HU10 #HU10 +elim (ssta_tpss_conf … HTU0 … HT02) -T0 #U2 #HTU2 #HU02 +lapply (cpcs_cpr_strap1 … HU10 U2 ?) -HU10 /2 width=3/ +qed-. + +fact ssta_lfpr_aux: ∀h,g,n. ( + ∀L,T2. ♯{L,T2} < n → + ∀T1. L ⊢ T1 ⬌* T2 → ⦃h, L⦄ ⊩ T1 :[g] → ⦃h, L⦄ ⊩ T2 :[g] → + ∀U1,l1. ⦃h, L⦄ ⊢ T1 •[g, l1] U1 → + ∀U2,l2. ⦃h, L⦄ ⊢ T2 •[g, l2] U2 → + L ⊢ U1 ⬌* U2 ∧ l1 = l2 + ) → ( + ∀L,T. ♯{L,T} < n → ⦃h, L⦄ ⊩ T :[g] → + ∀U,l. ⦃h, L⦄ ⊢ T •[g, l + 1] U → ⦃h, L⦄ ⊩ U :[g] + ) → ( + ∀L1,T1. ♯{L1,T1} < n → + ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → + ∀L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀T2. L2 ⊢ T1 ➡ T2 → ⦃h, L1⦄ ⊩ T1 :[g] → + ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄ + ) → + ∀L1,T1. ♯{L1,T1} = n → + ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → + ∀L2. ⦃L1⦄ ➡ ⦃L2⦄ → ⦃h, L1⦄ ⊩ T1 :[g] → + ∃∃U2. ⦃h, L2⦄ ⊢ T1 •[g, l] U2 & ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄. +#h #g #n #IH3 #IH2 #IH1 #L1 #T1 #Hn #U1 #l #HTU1 #L2 * #L #HL1 #HL2 #HT1 +elim (ssta_ltpr_tpr_aux … IH3 IH2 … Hn … HTU1 … HL1 … HT1) -HTU1 -HL1 -HT1 +-IH3 -IH2 [3: // |2: skip |4: /3 width=5/ ] -n #U0 #HTU0 #HU10 +elim (ssta_ltpss_sn_conf … HTU0 … HL2) -HTU0 #U2 #HTU2 #HU02 +lapply (fpcs_fpr_strap1 … HU10 L U2 ?) -HU10 /3 width=3/ -HU02 #HU12 +lapply (fpcs_fpr_strap1 … HU12 L2 U2 ?) /2 width=3/ -h -L1 -T1 -U1 -U0 -l /3 width=4/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_dxprs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_dxprs.ma new file mode 100644 index 000000000..39525c45e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_dxprs.ma @@ -0,0 +1,69 @@ +(**************************************************************************) +(* ___ *) +(* ||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/ygt.ma". +include "basic_2/dynamic/snv_cpr.ma". + +(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) + +(* Properties on context-free parallel computation for closures *************) + +fact ssta_cprs_aux: ∀h,g,L0,T0. ( + ∀L,T2. h ⊢ ⦃L0, T0⦄ >[g] ⦃L, T2⦄ → + ∀T1. L ⊢ T1 ⬌* T2 → ⦃h, L⦄ ⊩ T1 :[g] → ⦃h, L⦄ ⊩ T2 :[g] → + ∀U1,l1. ⦃h, L⦄ ⊢ T1 •[g, l1] U1 → + ∀U2,l2. ⦃h, L⦄ ⊢ T2 •[g, l2] U2 → + L ⊢ U1 ⬌* U2 ∧ l1 = l2 + ) → ( + ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊩ T1 :[g] → + ∀L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀T2. ⦃h, L2⦄ ⊢ T1 •*➡*[g] T2 → ⦃h, L2⦄ ⊩ T2 :[g] + ) → ( + ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → + ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → ⦃h, L1⦄ ⊩ T1 :[g] → + ∀L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀T2. L2 ⊢ T1 ➡* T2 → + ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄ + ) → + ∀L1,T1,T2. L1 ⊢ T1 ➡* T2 → L0 = L1 → T0 = T1 → + ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → ⦃h, L1⦄ ⊩ T1 :[g] → + ∃∃U2. ⦃h, L1⦄ ⊢ T2 •[g, l] U2 & L1 ⊢ U1 ⬌* U2. +#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 #T1 #T2 #H +@(cprs_ind_dx … H) -T1 [ /2 width=3/ ] +#T1 #T #HT1T #HTT2 #IH #H1 #H2 #U1 #l #HTU1 #HT1 destruct +elim (term_eq_dec T1 T) #H destruct [ /2 width=1/ ] -IH +elim (ssta_cpr_aux … HTU1 … HT1T HT1) -HTU1 +[2: // |3: skip |4,5,6: /3 width=9 by inj, dxprs_strap2, fw_ygt/ ] -IH3 #U #HTU #HU1 +lapply (snv_cpr_aux … HT1 … HT1T) -HT1 +[ // | skip |3,4: /3 width=6 by inj, fw_ygt/ ] -IH2 #HT +elim (IH1 … HTU HT … HTT2) -IH1 -HTU -HT -HTT2 // [2: /3 width=1/ ] -T #U2 #HTU2 #HU2 +lapply (fpcs_inv_cpcs … HU2) -HU2 #HU2 +lapply (cpcs_trans … HU1 … HU2) -U /2 width=3/ +qed-. + +fact snv_cprs_aux: ∀h,g,L0,T0. ( + ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → + ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → + ∀L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀T2. L2 ⊢ T1 ➡* T2 → ⦃h, L1⦄ ⊩ T1 :[g] → + ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄ + ) → ( + ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊩ T1 :[g] → + ∀L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀T2. ⦃h, L2⦄ ⊢ T1 •*➡*[g] T2 → ⦃h, L2⦄ ⊩ T2 :[g] + ) → + ∀L1,T1. L0 = L1 → T0 = T1 → ⦃h, L1⦄ ⊩ T1 :[g] → + ∀T2. L1 ⊢ T1 ➡* T2 → ⦃h, L1⦄ ⊩ T2 :[g]. +#h #g #L0 #T0 #IH2 #IH1 #L1 #T1 #H1 #H2 #HT1 #T2 #H +@(cprs_ind … H) -T2 // -HT1 +#T #T2 #HT1T #HTT2 #HT destruct +lapply (snv_cpr_aux … HT … HTT2) -HT -HTT2 [1,5: // |2: skip ] +/4 width=6 by cprs_ygt_trans, inj, fw_ygt/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_fprs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_fprs.ma deleted file mode 100644 index f0e0bb8f7..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_fprs.ma +++ /dev/null @@ -1,48 +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/dynamic/snv_fpr.ma". - -(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) - -(* Properties on context-free parallel computation for closures *************) - -fact ssta_fprs_aux: ∀h,g,n. ( - ∀L,T2. ♯{L,T2} < n → - ∀T1. L ⊢ T1 ⬌* T2 → ⦃h, L⦄ ⊩ T1 :[g] → ⦃h, L⦄ ⊩ T2 :[g] → - ∀U1,l1. ⦃h, L⦄ ⊢ T1 •[g, l1] U1 → - ∀U2,l2. ⦃h, L⦄ ⊢ T2 •[g, l2] U2 → - L ⊢ U1 ⬌* U2 ∧ l1 = l2 - ) → ( - ∀L,T. ♯{L,T} < n → ⦃h, L⦄ ⊩ T :[g] → - ∀U. ⦃h, L⦄ ⊢ T •*➡*[g] U → ⦃h, L⦄ ⊩ U :[g] - ) → ( - ∀L1,T1. ♯{L1,T1} < n → - ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → - ∀L2,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → ⦃h, L1⦄ ⊩ T1 :[g] → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄ - ) → - ∀L1,T1. ♯{L1,T1} = n → - ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → - ∀L2,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → ⦃h, L1⦄ ⊩ T1 :[g] → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄. -#h #g #n #IH3 #IH2 #IH1 #L1 #T1 #Hn #U1 #l #HTU1 #L2 #T2 #H12 #HT1 -@(fprs_ind … H12) -L2 -T2 [-IH1 /2 width=3/ ] (**) (* auto fails without -IH1 *) -#L #L2 #T #T2 #HT1 #HT2 * #U #HTU #HU1 -(* -lapply (IH2 … - -elim (ssta_fpr_aux … IH3 … Hn … HTU1 … HT2 HT1) --T1 -IH3 -IH2 -HL1 [2: /3 width=5/ ] -n #U #HTU #HU1 -*) \ No newline at end of file diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_cpcs.ma index 2d65731b5..b1288f751 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_cpcs.ma @@ -38,7 +38,7 @@ qed. (* Advanced inversion lemmas ************************************************) lemma fpcs_inv_shift: ∀I,L1,L2,V1,V2,T1,T2. ⦃L1.ⓑ{I}V1, T1⦄ ⬌* ⦃L2.ⓑ{I}V2, T2⦄ → - ⦃L1, -ⓑ{I}V1.T1⦄ ⬌* ⦃L2, -ⓑ{I}V2.T2⦄. + ⦃L1, -ⓑ{I}V1.T1⦄ ⬌* ⦃L2, -ⓑ{I}V2.T2⦄. #I #L1 #L2 #V1 #V2 #T1 #T2 #H12 elim (fpcs_inv_fprs … H12) -H12 #L #T #H1 #H2 elim (fprs_inv_pair1 … H1) -H1 #K1 #U1 #_ #HTU1 #H destruct diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/ypr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/csup/ypr.etc deleted file mode 100644 index f1510ab7e..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/ypr.etc +++ /dev/null @@ -1,41 +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 "hvbox( h ⊢ break ⦃ L1, break T1 ⦄ • ⥸ break [ g ] break ⦃ L2 , break T2 ⦄ )" - non associative with precedence 45 - for @{ 'YPRed $h $g $L1 $T1 $L2 $T2 }. - -include "basic_2/substitution/csup.ma". -include "basic_2/reducibility/xpr.ma". - -(* HYPER PARALLEL REDUCTION ON CLOSURES *************************************) - -inductive ypr (h) (g) (L1) (T1): relation2 lenv term ≝ -| ypr_cpr : ∀T2. L1 ⊢ T1 ➡ T2 → ypr h g L1 T1 L1 T2 -| ypr_ssta: ∀T2,l. ⦃h, L1⦄ ⊢ T1 •[g, l + 1] T2 → ypr h g L1 T1 L1 T2 -| ypr_csup: ∀L2,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ → ypr h g L1 T1 L2 T2 -. - -interpretation - "hyper parallel reduction (closure)" - 'YPRed h g L1 T1 L2 T2 = (ypr h g L1 T1 L2 T2). - -(* Basic properties *********************************************************) - -lemma ypr_refl: ∀h,g. bi_reflexive … (ypr h g). -/2 width=1/ qed. - -lemma xpr_ypr: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 •➡[g] T2 → h ⊢ ⦃L, T1⦄ •⥸[g] ⦃L, T2⦄. -#h #g #L #T1 #T2 * /2 width=1/ /2 width=2/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/yprs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/csup/yprs.etc deleted file mode 100644 index 86dc0c135..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/yprs.etc +++ /dev/null @@ -1,52 +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 "hvbox( h ⊢ break ⦃ L1, break T1 ⦄ • ⥸ * break [ g ] break ⦃ L2 , break T2 ⦄ )" - non associative with precedence 45 - for @{ 'YPRedStar $h $g $L1 $T1 $L2 $T2 }. - -include "basic_2/reducibility/ypr.ma". - -(* HYPER PARALLEL COMPUTATION ON CLOSURES ***********************************) - -definition yprs: ∀h. sd h → bi_relation lenv term ≝ - λh,g. bi_TC … (ypr h g). - -interpretation "hyper parallel computation (closure)" - 'YPRedStar h g L1 T1 L2 T2 = (yprs h g L1 T1 L2 T2). - -(* Basic eliminators ********************************************************) - -lemma yprs_ind: ∀h,g,L1,T1. ∀R:relation2 lenv term. R L1 T1 → - (∀L,L2,T,T2. h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L, T⦄ → h ⊢ ⦃L, T⦄ •⥸[g] ⦃L2, T2⦄ → R L T → R L2 T2) → - ∀L2,T2. h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L2, T2⦄ → R L2 T2. -/3 width=7 by bi_TC_star_ind/ qed-. - -lemma yprs_ind_dx: ∀h,g,L2,T2. ∀R:relation2 lenv term. R L2 T2 → - (∀L1,L,T1,T. h ⊢ ⦃L1, T1⦄ •⥸[g] ⦃L, T⦄ → h ⊢ ⦃L, T⦄ •⥸*[g] ⦃L2, T2⦄ → R L T → R L1 T1) → - ∀L1,T1. h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L2, T2⦄ → R L1 T1. -/3 width=7 by bi_TC_star_ind_dx/ qed-. - -(* Basic properties *********************************************************) - -lemma yprs_refl: ∀h,g. bi_reflexive … (yprs h g). -/2 width=1/ qed. - -lemma yprs_strap1: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L, T⦄ → - h ⊢ ⦃L, T⦄ •⥸[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L2, T2⦄. -/2 width=4/ qed. - -lemma yprs_strap2: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ •⥸[g] ⦃L, T⦄ → - h ⊢ ⦃L, T⦄ •⥸*[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L2, T2⦄. -/2 width=4/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/yprs_csups.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/csup/yprs_csups.etc deleted file mode 100644 index 08c939d8d..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/yprs_csups.etc +++ /dev/null @@ -1,25 +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/unfold/csups.ma". -include "basic_2/computation/yprs.ma". - -(* HYPER PARALLEL COMPUTATION ON CLOSURES ***********************************) - -(* Properties on iterated supclosure ****************************************) - -lemma csups_yprs: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ >* ⦃L2, T2⦄ → - h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L2, T2⦄. -#h #g #L1 #L2 #T1 #T2 #H @(csups_ind … H) -L2 -T2 /3 width=1/ /3 width=4/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/ysteps.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/csup/ysteps.etc deleted file mode 100644 index 149e7895b..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/ysteps.etc +++ /dev/null @@ -1,47 +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 "hvbox( h ⊢ break ⦃ L1, break T1 ⦄ • ⭃ * break [ g ] break ⦃ L2 , break T2 ⦄ )" - non associative with precedence 45 - for @{ 'YPRedStepStar $h $g $L1 $T1 $L2 $T2 }. - -include "basic_2/substitution/csup.ma". -include "basic_2/computation/yprs.ma". - -(* ITERATED STEP OF HYPER PARALLEL COMPUTATION ON CLOSURES ******************) - -inductive ysteps (h) (g) (L1) (T1) (L2) (T2): Prop ≝ -| ysteps_intro: h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L2, T2⦄ → (L1 = L2 → T1 = T2 → ⊥) → - ysteps h g L1 T1 L2 T2 -. - -interpretation "iterated step of hyper parallel computation (closure)" - 'YPRedStepStar h g L1 T1 L2 T2 = (ysteps h g L1 T1 L2 T2). - -(* Basic properties *********************************************************) - -lemma ssta_ysteps: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l + 1] U → - h ⊢ ⦃L, T⦄ •⭃*[g] ⦃L, U⦄. -#h #g #L #T #U #l #HTU -@ysteps_intro /3 width=2/ #_ #H destruct -elim (ssta_inv_refl … HTU) -qed. - -lemma csup_ysteps: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ → - h ⊢ ⦃L1, T1⦄ •⭃*[g] ⦃L2, T2⦄. -#h #g #L1 #L2 #T1 #T2 #H -lapply (csup_fwd_cw … H) #H1 -@ysteps_intro /3 width=1/ -H #H2 #H3 destruct -elim (lt_refl_false … H1) -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/ysteps_csups.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/csup/ysteps_csups.etc deleted file mode 100644 index 2e48f396d..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/ysteps_csups.etc +++ /dev/null @@ -1,28 +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/yprs_csups.ma". -include "basic_2/computation/ysteps.ma". - -(* ITERATED STEP OF HYPER PARALLEL COMPUTATION ON CLOSURES ******************) - -(* Properties on iterated supclosure ****************************************) - -lemma csups_ysteps: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ >* ⦃L2, T2⦄ → - h ⊢ ⦃L1, T1⦄ •⭃*[g] ⦃L2, T2⦄. -#h #g #L1 #L2 #T1 #T2 #H -lapply (csups_fwd_cw … H) #H1 -@ysteps_intro /2 width=1/ -H #H2 #H3 destruct -elim (lt_refl_false … H1) -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_weight.ma index 7893bff32..642a3d1b8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_weight.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_weight.ma @@ -29,5 +29,6 @@ interpretation "weight (local environment)" 'Weight L = (lw L). lemma lw_pair: ∀I,L,V. ♯{L} < ♯{L.ⓑ{I}V}. /3 width=1/ qed. -(* Basic_1: removed theorems 2: clt_cong clt_head clt_thead *) +(* Basic_1: removed theorems 4: clt_cong clt_head clt_thead clt_wf_ind *) +(* Basic_1: removed local theorems 1: clt_wf__q_ind *) (* Basic_1: note: clt_thead should be renamed clt_ctail *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation.ma b/matita/matita/contribs/lambdadelta/basic_2/notation.ma index 71e9fae60..d2008a3f8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation.ma @@ -340,6 +340,10 @@ notation "hvbox( ⦃ term 46 L1 ⦄ ➡ ➡ break ⦃ term 46 L2 ⦄ )" non associative with precedence 45 for @{ 'FocalizedPRedAlt $L1 $L2 }. +notation "hvbox( h ⊢ break ⦃ term 46 L1, break term 46 T1 ⦄ ≻ break [ term 46 g ] break ⦃ term 46 L2 , break term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'BTSuccessor $h $g $L1 $T1 $L2 $T2 }. + (* Computation **************************************************************) notation "hvbox( T1 ➡ * break term 46 T2 )" @@ -402,6 +406,10 @@ notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ • * ⬊ * break [ ter non associative with precedence 45 for @{ 'DecomposedXSN $h $g $L $T }. +notation "hvbox( h ⊢ break ⦃ term 46 L1, break term 46 T1 ⦄ > break [ term 46 g ] break ⦃ term 46 L2 , break term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'BTGreaterThan $h $g $L1 $T1 $L2 $T2 }. + (* Conversion ***************************************************************) notation "hvbox( L ⊢ break term 46 T1 ⬌ break term 46 T2 )" diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/yprs_xprs.etc b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ysc.ma similarity index 65% rename from matita/matita/contribs/lambdadelta/basic_2/etc/csup/yprs_xprs.etc rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/ysc.ma index 2feb88a2f..8762efb02 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/yprs_xprs.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ysc.ma @@ -12,17 +12,17 @@ (* *) (**************************************************************************) -include "basic_2/computation/xprs_cprs.ma". -include "basic_2/computation/yprs.ma". +include "basic_2/static/ssta.ma". +include "basic_2/reducibility/cpr.ma". -(* HYPER PARALLEL COMPUTATION ON CLOSURES ***********************************) +(* "BIG TREE" SUCCESSOR ON CLOSURES *****************************************) -(* Properties on extended parallel computation for terms ********************) +inductive ysc (h) (g) (L1) (T1): relation2 lenv term ≝ +| ysc_fw : ∀L2,T2. ♯{L2, T2} < ♯{L1, T1} → ysc h g L1 T1 L2 T2 +| ysc_cpr : ∀T2. L1 ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → ysc h g L1 T1 L1 T2 +| ysc_ssta: ∀T2,l. ⦃h, L1⦄ ⊢ T1 •[g, l + 1] T2 → ysc h g L1 T1 L1 T2 +. -lemma xprs_yprs: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 •➡*[g] T2 → - h ⊢ ⦃L, T1⦄ •⥸*[g] ⦃L, T2⦄. -#h #g #L #T1 #T2 #H @(xprs_ind … H) -T2 // /3 width=4/ -qed. - -lemma cprs_yprs: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → h ⊢ ⦃L, T1⦄ •⥸*[g] ⦃L, T2⦄. -/3 width=1/ qed. +interpretation + "'big tree' successor (closure)" + 'BTSuccessor h g L1 T1 L2 T2 = (ysc h g L1 T1 L2 T2). diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma index bcc1db8b2..ec2cc2df5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma @@ -259,6 +259,7 @@ lemma lift_inv_pair_xy_x: ∀d,e,I,V,T. ⇧[d, e] ②{I} V. T ≡ V → ⊥. ] qed-. +(* Basic_1: was: thead_x_lift_y_y *) lemma lift_inv_pair_xy_y: ∀I,T,V,d,e. ⇧[d, e] ②{I} V. T ≡ T → ⊥. #J #T elim T -T [ * #i #V #d #e #H -- 2.39.2