From 80178d6cf86b78bb9fc47f397f4bcfb1fd15a24f Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 19 Jun 2013 15:01:49 +0000 Subject: [PATCH] - partial commit :( some work on supclosure and extended reduction ... --- .../lambdadelta/basic_2/computation/cprs.ma | 15 +- .../lambdadelta/basic_2/computation/cpxs.ma | 149 ++++++++++++++++++ .../basic_2/computation/cpxs_lift.ma | 87 ++++++++++ .../contribs/lambdadelta/basic_2/notation.ma | 4 + .../lambdadelta/basic_2/reduction/cpx.ma | 4 +- .../lambdadelta/basic_2/reduction/cpx_lift.ma | 26 ++- .../lambdadelta/basic_2/relocation/fsup.ma | 34 ++-- .../lambdadelta/basic_2/relocation/ldrop.ma | 23 +++ .../contribs/lambdadelta/basic_2/static/sd.ma | 7 + .../lambdadelta/basic_2/web/basic_2_src.tbl | 4 + matita/matita/lib/arithmetics/nat.ma | 9 +- 11 files changed, 329 insertions(+), 33 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma index d3aaae5de..f1f6495bd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma @@ -114,18 +114,15 @@ qed. lemma cprs_beta_dx: ∀a,L,V1,V2,W,T1,T2. L ⊢ V1 ➡ V2 → L.ⓛW ⊢ T1 ➡* T2 → L ⊢ ⓐV1.ⓛ{a}W.T1 ➡* ⓓ{a}V2.T2. -#a #L #V1 #V2 #W #T1 #T2 #HV12 #H elim H -T2 /3 width=1/ -#T #T2 #_ #HT2 #IHT1 -@(cprs_strap1 … IHT1) -V1 -T1 /3 width=2/ +#a #L #V1 #V2 #W #T1 #T2 #HV12 * -T2 /3 width=1/ +/4 width=6 by cprs_strap1, cprs_bind_dx, cprs_flat_dx, cpr_beta/ (**) (* auto too slow without trace *) qed. -lemma cprs_theta_dx: ∀a,L,V1,V,V2,W1,T1,T2. +lemma cprs_theta_dx: ∀a,L,V1,V,V2,W1,W2,T1,T2. L ⊢ V1 ➡ V → ⇧[0, 1] V ≡ V2 → L.ⓓW1 ⊢ T1 ➡* T2 → - ∀W2. L ⊢ W1 ➡ W2 → L ⊢ ⓐV1.ⓓ{a}W1.T1 ➡* ⓓ{a}W2.ⓐV2.T2. -#a #L #V1 #V #V2 #W1 #T1 #T2 #HV1 #HV2 #H elim H -T2 [ /3 width=3/ ] -#T #T2 #_ #HT2 #IHT1 #W2 #HW12 -lapply (IHT1 W1 ?) -IHT1 // #HT1 -@(cprs_strap1 … HT1) -HT1 -V -V1 /3 width=1/ + L ⊢ W1 ➡ W2 → L ⊢ ⓐV1.ⓓ{a}W1.T1 ➡* ⓓ{a}W2.ⓐV2.T2. +#a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 * -T2 [ /3 width=3/ ] +/4 width=9 by cprs_strap1, cprs_bind_dx, cprs_flat_dx, cpr_theta/ (**) (* auto too slow without trace *) qed. (* Basic inversion lemmas ***************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma new file mode 100644 index 000000000..202d14d14 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma @@ -0,0 +1,149 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/reduction/cpx.ma". +include "basic_2/computation/cprs.ma". + +(* EXTENDED CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS *****************) + +definition cpxs: ∀h. sd h → lenv → relation term ≝ + λh,g. LTC … (cpx h g). + +interpretation "extended context-sensitive parallel computation (term)" + 'PRedStar h g L T1 T2 = (cpxs h g L T1 T2). + +(* Basic eliminators ********************************************************) + +lemma cpxs_ind: ∀h,g,L,T1. ∀R:predicate term. R T1 → + (∀T,T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T → ⦃h, L⦄ ⊢ T ➡[g] T2 → R T → R T2) → + ∀T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 → R T2. +#h #g #L #T1 #R #HT1 #IHT1 #T2 #HT12 +@(TC_star_ind … HT1 IHT1 … HT12) // +qed-. + +lemma cpxs_ind_dx: ∀h,g,L,T2. ∀R:predicate term. R T2 → + (∀T1,T. ⦃h, L⦄ ⊢ T1 ➡[g] T → ⦃h, L⦄ ⊢ T ➡*[g] T2 → R T → R T1) → + ∀T1. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 → R T1. +#h #g #L #T2 #R #HT2 #IHT2 #T1 #HT12 +@(TC_star_ind_dx … HT2 IHT2 … HT12) // +qed-. + +(* Basic properties *********************************************************) + +lemma cpxs_refl: ∀h,g,L,T. ⦃h, L⦄ ⊢ T ➡*[g] T. +/2 width=1/ qed. + +lemma cpx_cpxs: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 ➡[g] T2 → ⦃h, L⦄ ⊢ T1 ➡*[g] T2. +/2 width=1/ qed. + +lemma cpxs_strap1: ∀h,g,L,T1,T. ⦃h, L⦄ ⊢ T1 ➡*[g] T → + ∀T2. ⦃h, L⦄ ⊢ T ➡[g] T2 → ⦃h, L⦄ ⊢ T1 ➡*[g] T2. +normalize /2 width=3/ qed. + +lemma cpxs_strap2: ∀h,g,L,T1,T. ⦃h, L⦄ ⊢ T1 ➡[g] T → + ∀T2. ⦃h, L⦄ ⊢ T ➡*[g] T2 → ⦃h, L⦄ ⊢ T1 ➡*[g] T2. +normalize /2 width=3/ qed. + +lemma cprs_cpxs: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → ⦃h, L⦄ ⊢ T1 ➡*[g] T2. +#h #g #L #T1 #T2 #H @(cprs_ind … H) -T2 // /3 width=3/ +qed. + +lemma cpxs_bind_dx: ∀h,g,L,V1,V2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 → + ∀I,T1,T2. ⦃h, L. ⓑ{I}V1⦄ ⊢ T1 ➡*[g] T2 → + ∀a. ⦃h, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[g] ⓑ{a,I}V2.T2. +#h #g #L #V1 #V2 #HV12 #I #T1 #T2 #HT12 #a @(cpxs_ind_dx … HT12) -T1 +/3 width=1/ /3 width=3/ +qed. + +lemma cpxs_flat_dx: ∀h,g,L,V1,V2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 → + ∀T1,T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 → + ∀I. ⦃h, L⦄ ⊢ ⓕ{I} V1. T1 ➡*[g] ⓕ{I} V2. T2. +#h #g #L #V1 #V2 #HV12 #T1 #T2 #HT12 @(cpxs_ind … HT12) -T2 /3 width=1/ /3 width=5/ +qed. + +lemma cpxs_flat_sn: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 ➡[g] T2 → + ∀V1,V2. ⦃h, L⦄ ⊢ V1 ➡*[g] V2 → + ∀I. ⦃h, L⦄ ⊢ ⓕ{I} V1. T1 ➡*[g] ⓕ{I} V2. T2. +#h #g #L #T1 #T2 #HT12 #V1 #V2 #H @(cpxs_ind … H) -V2 /3 width=1/ /3 width=5/ +qed. + +lemma cpxs_zeta: ∀h,g,L,V,T1,T,T2. ⇧[0, 1] T2 ≡ T → + ⦃h, L.ⓓV⦄ ⊢ T1 ➡*[g] T → ⦃h, L⦄ ⊢ +ⓓV.T1 ➡*[g] T2. +#h #g #L #V #T1 #T #T2 #HT2 #H @(TC_ind_dx … T1 H) -T1 /3 width=3/ +qed. + +lemma cpxs_tau: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 → ∀V. ⦃h, L⦄ ⊢ ⓝV.T1 ➡*[g] T2. +#h #g #L #T1 #T2 #H elim H -T2 /2 width=3/ /3 width=1/ +qed. + +lemma cpxs_beta_dx: ∀h,g,a,L,V1,V2,W,T1,T2. + ⦃h, L⦄ ⊢ V1 ➡[g] V2 → ⦃h, L.ⓛW⦄ ⊢ T1 ➡*[g] T2 → + ⦃h, L⦄ ⊢ ⓐV1.ⓛ{a}W.T1 ➡*[g] ⓓ{a}V2.T2. +#h #g #a #L #V1 #V2 #W #T1 #T2 #HV12 * -T2 /3 width=1/ +/4 width=6 by cpxs_strap1, cpxs_bind_dx, cpxs_flat_dx, cpx_beta/ (**) (* auto too slow without trace *) +qed. + +lemma cpxs_theta_dx: ∀h,g,a,L,V1,V,V2,W1,W2,T1,T2. + ⦃h, L⦄ ⊢ V1 ➡[g] V → ⇧[0, 1] V ≡ V2 → ⦃h, L.ⓓW1⦄ ⊢ T1 ➡*[g] T2 → + ⦃h, L⦄ ⊢ W1 ➡[g] W2 → ⦃h, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡*[g] ⓓ{a}W2.ⓐV2.T2. +#h #g #a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 * -T2 [ /3 width=3/ ] +/4 width=9 by cpxs_strap1, cpxs_bind_dx, cpxs_flat_dx, cpx_theta/ (**) (* auto too slow without trace *) +qed. + +(* Basic inversion lemmas ***************************************************) + +lemma cpxs_inv_sort1: ∀h,g,L,U2,k. ⦃h, L⦄ ⊢ ⋆k ➡*[g] U2 → + ∃∃n,l. deg h g k (n+l) & U2 = ⋆((next h)^n k). +#h #g #L #U2 #k #H @(cpxs_ind … H) -U2 +[ elim (deg_total h g k) #l #Hkl + @(ex2_2_intro … 0 … Hkl) -Hkl // +| #U #U2 #_ #HU2 * #n #l #Hknl #H destruct + elim (cpx_inv_sort1 … HU2) -HU2 + [ #H destruct /2 width=4/ + | * #l0 #Hkl0 #H destruct -l + @(ex2_2_intro … (n+1) l0) /2 width=1/ >iter_SO // + ] +] +qed-. + +lemma cpxs_inv_appl1: ∀h,g,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓐV1.T1 ➡*[g] U2 → + ∨∨ ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡*[g] V2 & ⦃h, L⦄ ⊢ T1 ➡*[g] T2 & + U2 = ⓐV2. T2 + | ∃∃a,V2,W,T. ⦃h, L⦄ ⊢ V1 ➡*[g] V2 & + ⦃h, L⦄ ⊢ T1 ➡*[g] ⓛ{a}W.T & ⦃h, L⦄ ⊢ ⓓ{a}V2.T ➡*[g] U2 + | ∃∃a,V0,V2,V,T. ⦃h, L⦄ ⊢ V1 ➡*[g] V0 & ⇧[0,1] V0 ≡ V2 & + ⦃h, L⦄ ⊢ T1 ➡*[g] ⓓ{a}V.T & ⦃h, L⦄ ⊢ ⓓ{a}V.ⓐV2.T ➡*[g] U2. +#h #g #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 [ /3 width=5/ ] +#U #U2 #_ #HU2 * * +[ #V0 #T0 #HV10 #HT10 #H destruct + elim (cpx_inv_appl1 … HU2) -HU2 * + [ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5/ + | #a #V2 #W2 #T #T2 #HV02 #HT2 #H1 #H2 destruct + lapply (cpxs_strap1 … HV10 … HV02) -V0 /5 width=7/ + | #a #V #V2 #W0 #W2 #T #T2 #HV0 #HV2 #HW02 #HT2 #H1 #H2 destruct + @or3_intro2 @(ex4_5_intro … HV2 HT10) /2 width=3/ /3 width=1/ (**) (* explicit constructor. /5 width=8/ is too slow because TC_transitive gets in the way *) + ] +| /4 width=9/ +| /4 width=11/ +] +qed-. + +lemma cpxs_inv_cast1: ∀h,g,L,W1,T1,U2. ⦃h, L⦄ ⊢ ⓝW1.T1 ➡*[g] U2 → ⦃h, L⦄ ⊢ T1 ➡*[g] U2 ∨ + ∃∃W2,T2. ⦃h, L⦄ ⊢ W1 ➡*[g] W2 & ⦃h, L⦄ ⊢ T1 ➡*[g] T2 & U2 = ⓝW2.T2. +#h #g #L #W1 #T1 #U2 #H @(cpxs_ind … H) -U2 /3 width=5/ +#U2 #U #_ #HU2 * /3 width=3/ * +#W #T #HW1 #HT1 #H destruct +elim (cpx_inv_cast1 … HU2) -HU2 /3 width=3/ * +#W2 #T2 #HW2 #HT2 #H destruct /4 width=5/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma new file mode 100644 index 000000000..47d66618b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma @@ -0,0 +1,87 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/reduction/cpx_lift.ma". +include "basic_2/computation/cpxs.ma". + +(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************) + +(* Advanced properties ******************************************************) + +lemma cpxs_delta: ∀h,g,I,L,K,V,V2,i. + ⇩[0, i] L ≡ K. ⓑ{I}V → ⦃h, K⦄ ⊢ V ➡*[g] V2 → + ∀W2. ⇧[0, i + 1] V2 ≡ W2 → ⦃h, L⦄ ⊢ #i ➡*[g] W2. +#h #g #I #L #K #V #V2 #i #HLK #H elim H -V2 [ /3 width=9/ ] +#V1 #V2 #_ #HV12 #IHV1 #W2 #HVW2 +lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK +elim (lift_total V1 0 (i+1)) /4 width=11 by cpx_lift, cpxs_strap1/ +qed. + +(* Advanced inversion lemmas ************************************************) + +lemma cpxs_inv_lref1: ∀h,g,L,T2,i. ⦃h, L⦄ ⊢ #i ➡*[g] T2 → + T2 = #i ∨ + ∃∃I,K,V1,T1. ⇩[0, i] L ≡ K.ⓑ{I}V1 & ⦃h, K⦄ ⊢ V1 ➡*[g] T1 & + ⇧[0, i + 1] T1 ≡ T2. +#h #g #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1/ +#T #T2 #_ #HT2 * +[ #H destruct + elim (cpx_inv_lref1 … HT2) -HT2 /2 width=1/ + * /4 width=7/ +| * #I #K #V1 #T1 #HLK #HVT1 #HT1 + lapply (ldrop_fwd_ldrop2 … HLK) #H0LK + elim (cpx_inv_lift1 … HT2 … H0LK … HT1) -H0LK -T /4 width=7/ +] +qed-. + +(* Relocation properties ****************************************************) + +(* Basic_1: was: pr3_lift *) +lemma cpxs_lift: ∀h,g. l_liftable (cpxs h g). +/3 width=9/ qed. + +(* Basic_1: was: pr3_gen_lift *) +lemma cpxs_inv_lift1: ∀h,g. l_deliftable_sn (cpxs h g). +/3 width=5 by l_deliftable_sn_LTC, cpx_inv_lift1/ +qed-. + +(* Properties on supclosure *************************************************) + +include "basic_2/substitution/fsups.ma". + +lemma fsupq_cpxs_trans: ∀h,g,L1,L2,T2,U2. ⦃h, L2⦄ ⊢ T2 ➡*[g] U2 → + ∀T1. ⦃L1, T1⦄ ⊃⸮ ⦃L2, T2⦄ → + ∃∃U1. ⦃h, L1⦄ ⊢ T1 ➡*[g] U1 & ⦃L1, U1⦄ ⊃* ⦃L2, U2⦄. +#h #g #L1 #L2 #T2 #U2 #H @(cpxs_ind_dx … H) -T2 [ (* /3 width=3/ *) | +#T #T2 #HT2 #_ #IHTU2 #T1 #HT1 +elim (fsupq_cpx_trans … HT1 … HT2) -T #T #HT1 #HT2 +elim (IHTU2 … HT2) -T2 /3 width=3/ + + +(* + elim H -L1 -L2 -T1 -T2 [2,3,4,5: /3 width=5/ ] +[ #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2 + elim (IHT12 … HTU2) -IHT12 -HTU2 #T #HT1 #HT2 + elim (lift_total T d e) #U #HTU + lapply (cpx_lift … HT1 … HLK1 … HTU1 … HTU) -HT1 -HTU1 /3 width=11/ +| #I #L1 #V2 #U2 #HVU2 + elim (lift_total U2 0 1) /4 width=9/ +] +qed-. + +lemma fsup_ssta_trans: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → + ∀U2,l. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l+1, U2⦄ → + ∃∃U1. ⦃h, L1⦄ ⊢ T1 ➡[g] U1 & ⦃L1, U1⦄ ⊃⸮ ⦃L2, U2⦄. +/3 width=4 by fsup_cpx_trans, ssta_cpx/ qed-. +*) \ No newline at end of file diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation.ma b/matita/matita/contribs/lambdadelta/basic_2/notation.ma index c8c98ecfc..a0e62745a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation.ma @@ -154,6 +154,10 @@ notation "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ⊃⸮ break ⦃ term 46 L non associative with precedence 45 for @{ 'SupTermOpt $L1 $T1 $L2 $T2 }. +notation "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ⊃⊃⸮ break ⦃ term 46 L2 , break term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'SupTermOptAlt $L1 $T1 $L2 $T2 }. + notation "hvbox( L ⊢ break ⌘ ⦃ term 46 T ⦄ ≡ break term 46 k )" non associative with precedence 45 for @{ 'ICM $L $T $k }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma index 935d5c7b0..33063d819 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma @@ -109,10 +109,10 @@ lemma cpx_inv_atom1: ∀h,g,J,L,T2. ⦃h, L⦄ ⊢ ⓪{J} ➡[g] T2 → /2 width=3 by cpx_inv_atom1_aux/ qed-. lemma cpx_inv_sort1: ∀h,g,L,T2,k. ⦃h, L⦄ ⊢ ⋆k ➡[g] T2 → T2 = ⋆k ∨ - ∃∃k,l. deg h g k (l+1) & T2 = ⋆(next h k). + ∃∃l. deg h g k (l+1) & T2 = ⋆(next h k). #h #g #L #T2 #k #H elim (cpx_inv_atom1 … H) -H /2 width=1/ * -[ #k0 #l #Hkl #H1 #H2 destruct /3 width=4/ +[ #k0 #l0 #Hkl0 #H1 #H2 destruct /3 width=4/ | #I #K #V #V2 #i #_ #_ #_ #H destruct ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma index 427c0a28b..325fcbf82 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma @@ -111,20 +111,30 @@ qed-. (* Properties on supclosure *************************************************) -lemma fsup_cpx_trans: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → - ∀U2. ⦃h, L2⦄ ⊢ T2 ➡[g] U2 → - ∃∃U1. ⦃h, L1⦄ ⊢ T1 ➡[g] U1 & ⦃L1, U1⦄ ⊃⸮ ⦃L2, U2⦄. -#h #g #L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 [2,3,4,5: /3 width=5/ ] -[ #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2 +lemma fsupq_cpx_trans: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃⸮ ⦃L2, T2⦄ → + ∀U2. ⦃h, L2⦄ ⊢ T2 ➡[g] U2 → + ∃∃U1. ⦃h, L1⦄ ⊢ T1 ➡[g] U1 & ⦃L1, U1⦄ ⊃⸮ ⦃L2, U2⦄. +#h #g #L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 [1: /2 width=3/ |3,4,5: /3 width=3/ ] +[ #I #L1 #V2 #U2 #HVU2 + elim (lift_total U2 0 1) /4 width=9/ +| #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2 elim (IHT12 … HTU2) -IHT12 -HTU2 #T #HT1 #HT2 elim (lift_total T d e) #U #HTU lapply (cpx_lift … HT1 … HLK1 … HTU1 … HTU) -HT1 -HTU1 /3 width=11/ -| #I #L1 #V2 #U2 #HVU2 - elim (lift_total U2 0 1) /4 width=9/ ] qed-. +lemma fsupq_ssta_trans: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃⸮ ⦃L2, T2⦄ → + ∀U2,l. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l+1, U2⦄ → + ∃∃U1. ⦃h, L1⦄ ⊢ T1 ➡[g] U1 & ⦃L1, U1⦄ ⊃⸮ ⦃L2, U2⦄. +/3 width=4 by fsupq_cpx_trans, ssta_cpx/ qed-. + +lemma fsup_cpx_trans: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → + ∀U2. ⦃h, L2⦄ ⊢ T2 ➡[g] U2 → + ∃∃U1. ⦃h, L1⦄ ⊢ T1 ➡[g] U1 & ⦃L1, U1⦄ ⊃⸮ ⦃L2, U2⦄. +/3 width=3 by fsupq_cpx_trans, fsup_fsupq/ qed-. + lemma fsup_ssta_trans: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀U2,l. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l+1, U2⦄ → ∃∃U1. ⦃h, L1⦄ ⊢ T1 ➡[g] U1 & ⦃L1, U1⦄ ⊃⸮ ⦃L2, U2⦄. -/3 width=4 by fsup_cpx_trans, ssta_cpx/ qed-. +/3 width=4 by fsupq_ssta_trans, fsup_fsupq/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma index a964988d7..d10d9d28b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma @@ -18,13 +18,15 @@ include "basic_2/relocation/ldrop.ma". (* SUPCLOSURE ***************************************************************) inductive fsup: bi_relation lenv term ≝ -| fsup_lref_O : ∀I,L,V. fsup (L.ⓑ{I}V) (#0) L V -| fsup_pair_sn: ∀I,L,V,T. fsup L (②{I}V.T) L V -| fsup_bind_dx: ∀a,I,L,V,T. fsup L (ⓑ{a,I}V.T) (L.ⓑ{I}V) T -| fsup_flat_dx: ∀I,L,V,T. fsup L (ⓕ{I}V.T) L T -| fsup_ldrop : ∀L1,K1,K2,T1,T2,U1,d,e. - ⇩[d, e] L1 ≡ K1 → ⇧[d, e] T1 ≡ U1 → - fsup K1 T1 K2 T2 → fsup L1 U1 K2 T2 +| fsup_lref_O : ∀I,L,V. fsup (L.ⓑ{I}V) (#0) L V +| fsup_pair_sn : ∀I,L,V,T. fsup L (②{I}V.T) L V +| fsup_bind_dx : ∀a,I,L,V,T. fsup L (ⓑ{a,I}V.T) (L.ⓑ{I}V) T +| fsup_flat_dx : ∀I,L,V,T. fsup L (ⓕ{I}V.T) L T +| fsup_ldrop_lt: ∀L,K,T,U,d,e. + ⇩[d, e] L ≡ K → ⇧[d, e] T ≡ U → |K| < |L| → fsup L U K T +| fsup_ldrop : ∀L1,K1,K2,T1,T2,U1,d,e. + ⇩[d, e] L1 ≡ K1 → ⇧[d, e] T1 ≡ U1 → + fsup K1 T1 K2 T2 → fsup L1 U1 K2 T2 . interpretation @@ -49,20 +51,26 @@ qed. lemma fsup_fwd_fw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ♯{L2, T2} < ♯{L1, T1}. #L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 // -#L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 -lapply (ldrop_fwd_lw … HLK1) -HLK1 #HLK1 -lapply (lift_fwd_tw … HTU1) -HTU1 #HTU1 -@(lt_to_le_to_lt … IHT12) -IHT12 /2 width=1/ +[ #L #K #T #U #d #e #HLK #HTU #HKL + lapply (ldrop_fwd_lw_lt … HLK HKL) -HKL -HLK #HKL + lapply (lift_fwd_tw … HTU) -d -e #H + normalize in ⊢ (?%%); /2 width=1/ +| #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 + lapply (ldrop_fwd_lw … HLK1) -HLK1 #HLK1 + lapply (lift_fwd_tw … HTU1) -HTU1 #HTU1 + @(lt_to_le_to_lt … IHT12) -IHT12 /2 width=1/ +] qed-. fact fsup_fwd_length_lref1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀i. T1 = #i → |L2| < |L1|. #L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 -[5: #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #i #H destruct +[1,5: normalize // +|3: #a +|6: #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #i #H destruct lapply (ldrop_fwd_length … HLK1) -HLK1 #HLK1 elim (lift_inv_lref2 … HTU1) -HTU1 * #Hdei #H destruct @(lt_to_le_to_lt … HLK1) /2 width=2/ -| normalize // |3: #a ] #I #L #V #T #j #H destruct qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma index 7d3b3b0ce..f51640fa1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma @@ -296,6 +296,29 @@ lemma ldrop_fwd_O1_length: ∀L1,L2,e. ⇩[0, e] L1 ≡ L2 → |L2| = |L1| - e. ] qed-. +lemma ldrop_fwd_lw_eq: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → + |L1| = |L2| → ♯{L2} = ♯{L1}. +#L1 #L2 #d #e #H elim H -L1 -L2 -d -e // +[ #L1 #L2 #I #V #e #HL12 #_ + lapply (ldrop_fwd_O1_length … HL12) -HL12 #HL21 >HL21 -HL21 normalize #H -I + lapply (discr_plus_xy_minus_xz … H) -e #H destruct +| #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #HL12 normalize in ⊢ (??%%→??%%); #H -I + >(lift_fwd_tw … HV21) -V2 /3 width=1 by eq_f2/ (**) (* auto is a bit slow without trace *) +] +qed-. + +lemma ldrop_fwd_lw_lt: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → + |L2| < |L1| → ♯{L2} < ♯{L1}. +#L1 #L2 #d #e #H elim H -L1 -L2 -d -e // +[ #L #I #V #H elim (lt_refl_false … H) +| #L1 #L2 #I #V #e #HL12 #_ #_ + lapply (ldrop_fwd_lw … HL12) -HL12 #HL12 + @(le_to_lt_to_lt … HL12) -HL12 // +| #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12 normalize in ⊢ (?%%→?%%); #H -I + >(lift_fwd_tw … HV21) -V2 /4 width=2 by lt_minus_to_plus, lt_plus_to_lt_l/ (**) (* auto too slow without trace *) +] +qed-. + (* Basic_1: removed theorems 50: drop_ctail drop_skip_flat cimp_flat_sx cimp_flat_dx cimp_bind cimp_getl_conf diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma b/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma index d6737a8ba..79d9f0740 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma @@ -100,6 +100,13 @@ lapply (deg_mono … H1 H2) -H1 -H2 #H <(associative_plus l 1 1) >H iter_SO #H +lapply (deg_pred … H) -H <(associative_plus l0 1 1) #H +lapply (IHl … H) -IHl -H // +qed. + lemma sd_l_SS: ∀h,k,l. sd_l h k (l + 2) = sd_l h (next h k) (l + 1). #h #k #l plus_n_Sm #H lapply (IHx … H) -x -z #H destruct +] +qed-. + (* Negated equalities *******************************************************) theorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m. -- 2.39.2