From: Ferruccio Guidi Date: Fri, 6 Dec 2013 14:41:51 +0000 (+0000) Subject: partial commit ... X-Git-Tag: make_still_working~1024 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bd264ed7070e6fbb8d77fc85994e0ceb684fca7c;p=helm.git partial commit ... - fleq removed and replaced by fpns - improved proper "big tree" reduction - some missing lemmas --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma index ae51de39d..91ddd1621 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma @@ -43,73 +43,84 @@ qed-. (* Basic properties *********************************************************) lemma cpxs_refl: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ➡*[h, g] T. -/2 width=1/ qed. +/2 width=1 by inj/ qed. lemma cpx_cpxs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2. -/2 width=1/ qed. +/2 width=1 by inj/ qed. lemma cpxs_strap1: ∀h,g,G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T → ∀T2. ⦃G, L⦄ ⊢ T ➡[h, g] T2 → ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2. -normalize /2 width=3/ qed. +normalize /2 width=3 by step/ qed. lemma cpxs_strap2: ∀h,g,G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡[h, g] T → ∀T2. ⦃G, L⦄ ⊢ T ➡*[h, g] T2 → ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2. -normalize /2 width=3/ qed. +normalize /2 width=3 by TC_strap/ qed. lemma lsubr_cpxs_trans: ∀h,g,G. lsub_trans … (cpxs h g G) lsubr. /3 width=5 by lsubr_cpx_trans, TC_lsub_trans/ qed-. lemma cprs_cpxs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2. -#h #g #G #L #T1 #T2 #H @(cprs_ind … H) -T2 // /3 width=3/ +#h #g #G #L #T1 #T2 #H @(cprs_ind … H) -T2 /3 width=3 by cpxs_strap1, cpr_cpx/ qed. lemma cpxs_bind_dx: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡[h, g] V2 → ∀I,T1,T2. ⦃G, L. ⓑ{I}V1⦄ ⊢ T1 ➡*[h, g] T2 → ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[h, g] ⓑ{a,I}V2.T2. #h #g #G #L #V1 #V2 #HV12 #I #T1 #T2 #HT12 #a @(cpxs_ind_dx … HT12) -T1 -/3 width=1/ /3 width=3/ +/3 width=3 by cpxs_strap2, cpx_cpxs, cpx_pair_sn, cpx_bind/ qed. lemma cpxs_flat_dx: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡[h, g] V2 → ∀T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ➡*[h, g] ⓕ{I}V2.T2. -#h #g #G #L #V1 #V2 #HV12 #T1 #T2 #HT12 @(cpxs_ind … HT12) -T2 /3 width=1/ /3 width=5/ +#h #g #G #L #V1 #V2 #HV12 #T1 #T2 #HT12 @(cpxs_ind … HT12) -T2 +/3 width=5 by cpxs_strap1, cpx_cpxs, cpx_pair_sn, cpx_flat/ qed. lemma cpxs_flat_sn: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → ∀V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 → ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ➡*[h, g] ⓕ{I}V2.T2. -#h #g #G #L #T1 #T2 #HT12 #V1 #V2 #H @(cpxs_ind … H) -V2 /3 width=1/ /3 width=5/ +#h #g #G #L #T1 #T2 #HT12 #V1 #V2 #H @(cpxs_ind … H) -V2 +/3 width=5 by cpxs_strap1, cpx_cpxs, cpx_pair_sn, cpx_flat/ +qed. + +lemma cpxs_pair_sn: ∀h,g,I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 → + ∀T. ⦃G, L⦄ ⊢ ②{I}V1.T ➡*[h, g] ②{I}V2.T. +#h #g #I #G #L #V1 #V2 #H @(cpxs_ind … H) -V2 +/3 width=3 by cpxs_strap1, cpx_pair_sn/ qed. lemma cpxs_zeta: ∀h,g,G,L,V,T1,T,T2. ⇧[0, 1] T2 ≡ T → ⦃G, L.ⓓV⦄ ⊢ T1 ➡*[h, g] T → ⦃G, L⦄ ⊢ +ⓓV.T1 ➡*[h, g] T2. -#h #g #G #L #V #T1 #T #T2 #HT2 #H @(TC_ind_dx … T1 H) -T1 /3 width=3/ +#h #g #G #L #V #T1 #T #T2 #HT2 #H @(cpxs_ind_dx … H) -T1 +/3 width=3 by cpxs_strap2, cpx_cpxs, cpx_bind, cpx_zeta/ qed. lemma cpxs_tau: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → ∀V. ⦃G, L⦄ ⊢ ⓝV.T1 ➡*[h, g] T2. -#h #g #G #L #T1 #T2 #H elim H -T2 /2 width=3/ /3 width=1/ +#h #g #G #L #T1 #T2 #H @(cpxs_ind … H) -T2 +/3 width=3 by cpxs_strap1, cpx_cpxs, cpx_tau/ qed. lemma cpxs_ti: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 → ∀T. ⦃G, L⦄ ⊢ ⓝV1.T ➡*[h, g] V2. -#h #g #G #L #V1 #V2 #H elim H -V2 /2 width=3/ /3 width=1/ +#h #g #G #L #V1 #V2 #H @(cpxs_ind … H) -V2 +/3 width=3 by cpxs_strap1, cpx_cpxs, cpx_ti/ qed. lemma cpxs_beta_dx: ∀h,g,a,G,L,V1,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h, g] V2 → ⦃G, L.ⓛW1⦄ ⊢ T1 ➡*[h, g] T2 → ⦃G, L⦄ ⊢ W1 ➡[h, g] W2 → ⦃G, L⦄ ⊢ ⓐV1.ⓛ{a}W1.T1 ➡*[h, g] ⓓ{a}ⓝW2.V2.T2. -#h #g #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 * -T2 /3 width=1/ -/4 width=7 by cpxs_strap1, cpxs_bind_dx, cpxs_flat_dx, cpx_beta/ (**) (* auto too slow without trace *) +#h #g #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 * -T2 +/4 width=7 by cpx_cpxs, cpxs_strap1, cpxs_bind_dx, cpxs_flat_dx, cpx_beta/ qed. lemma cpxs_theta_dx: ∀h,g,a,G,L,V1,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h, g] V → ⇧[0, 1] V ≡ V2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡*[h, g] T2 → ⦃G, L⦄ ⊢ W1 ➡[h, g] W2 → ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡*[h, g] ⓓ{a}W2.ⓐV2.T2. -#h #g #a #G #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 *) +#h #g #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 * -T2 +/4 width=9 by cpx_cpxs, cpxs_strap1, cpxs_bind_dx, cpxs_flat_dx, cpx_theta/ qed. (* Basic inversion lemmas ***************************************************) @@ -121,7 +132,7 @@ lemma cpxs_inv_sort1: ∀h,g,G,L,U2,k. ⦃G, L⦄ ⊢ ⋆k ➡*[h, g] U2 → @(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/ + [ #H destruct /2 width=4 by ex2_2_intro/ | * #l0 #Hkl0 #H destruct -l @(ex2_2_intro … (n+1) l0) /2 width=1 by deg_inv_prec/ >iter_SO // ] @@ -132,19 +143,19 @@ lemma cpxs_inv_cast1: ∀h,g,G,L,W1,T1,U2. ⦃G, L⦄ ⊢ ⓝW1.T1 ➡*[h, g] U2 ∨∨ ∃∃W2,T2. ⦃G, L⦄ ⊢ W1 ➡*[h, g] W2 & ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 & U2 = ⓝW2.T2 | ⦃G, L⦄ ⊢ T1 ➡*[h, g] U2 | ⦃G, L⦄ ⊢ W1 ➡*[h, g] U2. -#h #g #G #L #W1 #T1 #U2 #H @(cpxs_ind … H) -U2 /3 width=5/ -#U2 #U #_ #HU2 * /3 width=3/ * +#h #g #G #L #W1 #T1 #U2 #H @(cpxs_ind … H) -U2 /3 width=5 by or3_intro0, ex3_2_intro/ +#U2 #U #_ #HU2 * /3 width=3 by cpxs_strap1, or3_intro1, or3_intro2/ * #W #T #HW1 #HT1 #H destruct -elim (cpx_inv_cast1 … HU2) -HU2 /3 width=3/ * +elim (cpx_inv_cast1 … HU2) -HU2 /3 width=3 by cpxs_strap1, or3_intro1, or3_intro2/ * #W2 #T2 #HW2 #HT2 #H destruct lapply (cpxs_strap1 … HW1 … HW2) -W -lapply (cpxs_strap1 … HT1 … HT2) -T /3 width=5/ +lapply (cpxs_strap1 … HT1 … HT2) -T /3 width=5 by or3_intro0, ex3_2_intro/ qed-. lemma cpxs_inv_cnx1: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T ➡*[h, g] U → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → T = U. #h #g #G #L #T #U #H @(cpxs_ind_dx … H) -T // #T0 #T #H1T0 #_ #IHT #H2T0 -lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1/ +lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1 by/ qed-. lemma cpxs_neq_inv_step_sn: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma index 730671630..fa14bfc25 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma @@ -20,56 +20,51 @@ include "basic_2/computation/cpxs_lift.ma". (* Main properties **********************************************************) theorem cpxs_trans: ∀h,g,G,L. Transitive … (cpxs h g G L). -#h #g #G #L #T1 #T #HT1 #T2 @trans_TC @HT1 qed-. (**) (* auto /3 width=3/ does not work because a δ-expansion gets in the way *) +#h #g #G #L #T1 #T #HT1 #T2 +@trans_TC @HT1 qed-. (**) (* auto /3 width=3/ does not work because a δ-expansion gets in the way *) theorem cpxs_bind: ∀h,g,a,I,G,L,V1,V2,T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡*[h, g] T2 → ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 → ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[h, g] ⓑ{a,I}V2.T2. -#h #g #a #I #G #L #V1 #V2 #T1 #T2 #HT12 #H @(cpxs_ind … H) -V2 /2 width=1/ -#V #V2 #_ #HV2 #IHV1 -@(cpxs_trans … IHV1) -V1 /2 width=1/ +#h #g #a #I #G #L #V1 #V2 #T1 #T2 #HT12 #H @(cpxs_ind … H) -V2 +/3 width=5 by cpxs_trans, cpxs_bind_dx/ qed. theorem cpxs_flat: ∀h,g,I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 → ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ➡*[h, g] ⓕ{I}V2.T2. -#h #g #I #G #L #V1 #V2 #T1 #T2 #HT12 #H @(cpxs_ind … H) -V2 /2 width=1/ -#V #V2 #_ #HV2 #IHV1 -@(cpxs_trans … IHV1) -IHV1 /2 width=1/ +#h #g #I #G #L #V1 #V2 #T1 #T2 #HT12 #H @(cpxs_ind … H) -V2 +/3 width=5 by cpxs_trans, cpxs_flat_dx/ qed. theorem cpxs_beta_rc: ∀h,g,a,G,L,V1,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h, g] V2 → ⦃G, L.ⓛW1⦄ ⊢ T1 ➡*[h, g] T2 → ⦃G, L⦄ ⊢ W1 ➡*[h, g] W2 → ⦃G, L⦄ ⊢ ⓐV1.ⓛ{a}W1.T1 ➡*[h, g] ⓓ{a}ⓝW2.V2.T2. -#h #g #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HT12 #H @(cpxs_ind … H) -W2 /2 width=1/ -#W #W2 #_ #HW2 #IHW1 -@(cpxs_trans … IHW1) -IHW1 /3 width=1/ +#h #g #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HT12 #H @(cpxs_ind … H) -W2 +/4 width=5 by cpxs_trans, cpxs_beta_dx, cpxs_bind_dx, cpx_pair_sn/ qed. theorem cpxs_beta: ∀h,g,a,G,L,V1,V2,W1,W2,T1,T2. ⦃G, L.ⓛW1⦄ ⊢ T1 ➡*[h, g] T2 → ⦃G, L⦄ ⊢ W1 ➡*[h, g] W2 → ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 → ⦃G, L⦄ ⊢ ⓐV1.ⓛ{a}W1.T1 ➡*[h, g] ⓓ{a}ⓝW2.V2.T2. -#h #g #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HT12 #HW12 #H @(cpxs_ind … H) -V2 /2 width=1/ -#V #V2 #_ #HV2 #IHV1 -@(cpxs_trans … IHV1) -IHV1 /3 width=1/ +#h #g #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HT12 #HW12 #H @(cpxs_ind … H) -V2 +/4 width=5 by cpxs_trans, cpxs_beta_rc, cpxs_bind_dx, cpx_flat/ qed. theorem cpxs_theta_rc: ∀h,g,a,G,L,V1,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h, g] V → ⇧[0, 1] V ≡ V2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡*[h, g] T2 → ⦃G, L⦄ ⊢ W1 ➡*[h, g] W2 → ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡*[h, g] ⓓ{a}W2.ⓐV2.T2. -#h #g #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HT12 #H elim H -W2 /2 width=3/ -#W #W2 #_ #HW2 #IHW1 -@(cpxs_trans … IHW1) -IHW1 /2 width=1/ +#h #g #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HT12 #H @(cpxs_ind … H) -W2 +/3 width=5 by cpxs_trans, cpxs_theta_dx, cpxs_bind_dx/ qed. theorem cpxs_theta: ∀h,g,a,G,L,V1,V,V2,W1,W2,T1,T2. ⇧[0, 1] V ≡ V2 → ⦃G, L⦄ ⊢ W1 ➡*[h, g] W2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡*[h, g] T2 → ⦃G, L⦄ ⊢ V1 ➡*[h, g] V → ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡*[h, g] ⓓ{a}W2.ⓐV2.T2. -#h #g #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV2 #HW12 #HT12 #H @(TC_ind_dx … V1 H) -V1 /2 width=3/ -#V1 #V0 #HV10 #_ #IHV0 -@(cpxs_trans … IHV0) -IHV0 /2 width=1/ +#h #g #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV2 #HW12 #HT12 #H @(TC_ind_dx … V1 H) -V1 +/3 width=5 by cpxs_trans, cpxs_theta_rc, cpxs_flat_dx/ qed. (* Advanced inversion lemmas ************************************************) @@ -80,20 +75,20 @@ lemma cpxs_inv_appl1: ∀h,g,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓐV1.T1 ➡*[h, g] U2 | ∃∃a,W,T. ⦃G, L⦄ ⊢ T1 ➡*[h, g] ⓛ{a}W.T & ⦃G, L⦄ ⊢ ⓓ{a}ⓝW.V1.T ➡*[h, g] U2 | ∃∃a,V0,V2,V,T. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V0 & ⇧[0,1] V0 ≡ V2 & ⦃G, L⦄ ⊢ T1 ➡*[h, g] ⓓ{a}V.T & ⦃G, L⦄ ⊢ ⓓ{a}V.ⓐV2.T ➡*[h, g] U2. -#h #g #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 [ /3 width=5/ ] +#h #g #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 [ /3 width=5 by or3_intro0, ex3_2_intro/ ] #U #U2 #_ #HU2 * * [ #V0 #T0 #HV10 #HT10 #H destruct elim (cpx_inv_appl1 … HU2) -HU2 * - [ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5/ + [ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5 by cpxs_strap1, or3_intro0, ex3_2_intro/ | #a #V2 #W #W2 #T #T2 #HV02 #HW2 #HT2 #H1 #H2 destruct lapply (cpxs_strap1 … HV10 … HV02) -V0 #HV12 - lapply (lsubr_cpx_trans … HT2 (L.ⓓⓝW.V1) ?) -HT2 /2 width=1/ #HT2 - @or3_intro1 @(ex2_3_intro … HT10) -HT10 /3 width=1/ (**) (* explicit constructor. /5 width=8/ is too slow because TC_transitive gets in the way *) + lapply (lsubr_cpx_trans … HT2 (L.ⓓⓝW.V1) ?) -HT2 + /5 width=5 by cpxs_bind, cpxs_flat_dx, cpx_cpxs, lsubr_abst, ex2_3_intro, or3_intro1/ | #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 *) + /5 width=10 by cpxs_flat_sn, cpxs_bind_dx, cpxs_strap1, ex4_5_intro, or3_intro2/ ] -| /4 width=9/ -| /4 width=11/ +| /4 width=9 by cpxs_strap1, or3_intro1, ex2_3_intro/ +| /4 width=11 by cpxs_strap1, or3_intro2, ex4_5_intro/ ] qed-. @@ -101,22 +96,22 @@ qed-. lemma lpx_cpx_trans: ∀h,g,G. s_r_trans … (cpx h g G) (lpx h g G). #h #g #G #L2 #T1 #T2 #HT12 elim HT12 -G -L2 -T1 -T2 -[ /2 width=3/ -| /3 width=2/ +[ /2 width=3 by / +| /3 width=2 by cpx_cpxs, cpx_sort/ | #I #G #L2 #K2 #V0 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV02 #L1 #HL12 elim (lpx_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H elim (lpx_inv_pair2 … H) -H #K1 #V1 #HK12 #HV10 #H destruct lapply (IHV02 … HK12) -K2 #HV02 - lapply (cpxs_strap2 … HV10 … HV02) -V0 /2 width=7/ + lapply (cpxs_strap2 … HV10 … HV02) -V0 /2 width=7 by cpxs_delta/ | #a #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #HL12 - lapply (IHT12 (L1.ⓑ{I}V1) ?) -IHT12 /2 width=1/ /3 width=1/ -|5,7,8: /3 width=1/ + lapply (IHT12 (L1.ⓑ{I}V1) ?) -IHT12 /3 width=1 by cpxs_bind, lpx_pair/ +|5,7,8: /3 width=1 by cpxs_flat, cpxs_ti, cpxs_tau/ | #G #L2 #V2 #T1 #T #T2 #_ #HT2 #IHT1 #L1 #HL12 - lapply (IHT1 (L1.ⓓV2) ?) -IHT1 /2 width=1/ /2 width=3/ + lapply (IHT1 (L1.ⓓV2) ?) -IHT1 /2 width=3 by cpxs_zeta, lpx_pair/ | #a #G #L2 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L1 #HL12 - lapply (IHT12 (L1.ⓛW1) ?) -IHT12 /2 width=1/ /3 width=1/ + lapply (IHT12 (L1.ⓛW1) ?) -IHT12 /3 width=1 by cpxs_beta, lpx_pair/ | #a #G #L2 #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L1 #HL12 - lapply (IHT12 (L1.ⓓW1) ?) -IHT12 /2 width=1/ /3 width=3/ + lapply (IHT12 (L1.ⓓW1) ?) -IHT12 /3 width=3 by cpxs_theta, cpxs_strap1, lpx_pair/ ] qed-. @@ -124,7 +119,7 @@ lemma cpx_bind2: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡[h, g] V2 → ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡[h, g] T2 → ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[h, g] ⓑ{a,I}V2.T2. #h #g #G #L #V1 #V2 #HV12 #I #T1 #T2 #HT12 -lapply (lpx_cpx_trans … HT12 (L.ⓑ{I}V1) ?) /2 width=1/ +lapply (lpx_cpx_trans … HT12 (L.ⓑ{I}V1) ?) /2 width=1 by cpxs_bind_dx, lpx_pair/ qed. (* Advanced properties ******************************************************) @@ -136,5 +131,67 @@ lemma cpxs_bind2_dx: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡[h, g] V2 → ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡*[h, g] T2 → ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[h, g] ⓑ{a,I}V2.T2. #h #g #G #L #V1 #V2 #HV12 #I #T1 #T2 #HT12 -lapply (lpx_cpxs_trans … HT12 (L.ⓑ{I}V1) ?) /2 width=1/ +lapply (lpx_cpxs_trans … HT12 (L.ⓑ{I}V1) ?) /2 width=1 by cpxs_bind_dx, lpx_pair/ qed. + +(* Properties on supclosure *************************************************) + +lemma fqu_cpxs_trans_neq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → + ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 → (T2 = U2 → ⊥) → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊃ ⦃G2, L2, U2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 +[ #I #G #L #V1 #V2 #HV12 #_ elim (lift_total V2 0 1) + #U2 #HVU2 @(ex3_intro … U2) + [1,3: /3 width=7 by fqu_drop, cpxs_delta, ldrop_pair, ldrop_ldrop/ + | #H destruct /2 width=7 by lift_inv_lref2_be/ + ] +| #I #G #L #V1 #T #V2 #HV12 #H @(ex3_intro … (②{I}V2.T)) + [1,3: /2 width=4 by fqu_pair_sn, cpxs_pair_sn/ + | #H0 destruct /2 width=1 by/ + ] +| #a #I #G #L #V #T1 #T2 #HT12 #H @(ex3_intro … (ⓑ{a,I}V.T2)) + [1,3: /2 width=4 by fqu_bind_dx, cpxs_bind/ + | #H0 destruct /2 width=1 by/ + ] +| #I #G #L #V #T1 #T2 #HT12 #H @(ex3_intro … (ⓕ{I}V.T2)) + [1,3: /2 width=4 by fqu_flat_dx, cpxs_flat/ + | #H0 destruct /2 width=1 by/ + ] +| #G #L #K #T1 #U1 #e #HLK #HTU1 #T2 #HT12 #H elim (lift_total T2 0 (e+1)) + #U2 #HTU2 @(ex3_intro … U2) + [1,3: /2 width=9 by cpxs_lift, fqu_drop/ + | #H0 destruct /3 width=5 by lift_inj/ +] +qed-. + +lemma fquq_cpxs_trans_neq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → + ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 → (T2 = U2 → ⊥) → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊃⸮ ⦃G2, L2, U2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fquq_inv_gen … H12) -H12 +[ #H12 elim (fqu_cpxs_trans_neq … H12 … HTU2 H) -T2 + /3 width=4 by fqu_fquq, ex3_intro/ +| * #HG #HL #HT destruct /3 width=4 by ex3_intro/ +] +qed-. + +lemma fqup_cpxs_trans_neq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → + ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 → (T2 = U2 → ⊥) → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊃+ ⦃G2, L2, U2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind_dx … H) -G1 -L1 -T1 +[ #G1 #L1 #T1 #H12 #U2 #HTU2 #H elim (fqu_cpxs_trans_neq … H12 … HTU2 H) -T2 + /3 width=4 by fqu_fqup, ex3_intro/ +| #G #G1 #L #L1 #T #T1 #H1 #_ #IH12 #U2 #HTU2 #H elim (IH12 … HTU2 H) -T2 + #U1 #HTU1 #H #H12 elim (fqu_cpxs_trans_neq … H1 … HTU1 H) -T1 + /3 width=8 by fqup_strap2, ex3_intro/ +] +qed-. + +lemma fqus_cpxs_trans_neq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → + ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 → (T2 = U2 → ⊥) → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fqus_inv_gen … H12) -H12 +[ #H12 elim (fqup_cpxs_trans_neq … H12 … HTU2 H) -T2 + /3 width=4 by fqup_fqus, ex3_intro/ +| * #HG #HL #HT destruct /3 width=4 by ex3_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_alt.ma index ccd336acb..df23e1f2a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_alt.ma @@ -33,22 +33,26 @@ lemma csxa_ind: ∀h,g,G,L. ∀R:predicate term. (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → R T2) → R T1 ) → ∀T. ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T → R T. -#h #g #G #L #R #H0 #T1 #H elim H -T1 #T1 #HT1 #IHT1 -@H0 -H0 /3 width=1/ -IHT1 /4 width=1/ +#h #g #G #L #R #H0 #T1 #H elim H -T1 /5 width=1 by SN_intro/ qed-. (* Basic properties *********************************************************) +lemma csx_intro_cprs: ∀h,g,G,L,T1. + (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊*[h, g] T2) → + ⦃G, L⦄ ⊢ ⬊*[h, g] T1. +/4 width=1 by cpx_cpxs, csx_intro/ qed. + (* Basic_1: was just: sn3_intro *) lemma csxa_intro: ∀h,g,G,L,T1. (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T2) → ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T1. -/4 width=1/ qed. +/4 width=1 by SN_intro/ qed. fact csxa_intro_aux: ∀h,g,G,L,T1. ( ∀T,T2. ⦃G, L⦄ ⊢ T ➡*[h, g] T2 → T1 = T → (T1 = T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T2 ) → ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T1. -/4 width=3/ qed-. +/4 width=3 by csxa_intro/ qed-. (* Basic_1: was just: sn3_pr3_trans (old version) *) lemma csxa_cpxs_trans: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T1 → @@ -56,8 +60,8 @@ lemma csxa_cpxs_trans: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T1 → #h #g #G #L #T1 #H elim H -T1 #T1 #HT1 #IHT1 #T2 #HLT12 @csxa_intro #T #HLT2 #HT2 elim (eq_term_dec T1 T2) #HT12 -[ -IHT1 -HLT12 destruct /3 width=1/ -| -HT1 -HT2 /3 width=4/ +[ -IHT1 -HLT12 destruct /3 width=1 by/ +| -HT1 -HT2 /3 width=4 by/ qed. (* Basic_1: was just: sn3_pr2_intro (old version) *) @@ -70,8 +74,8 @@ lemma csxa_intro_cpx: ∀h,g,G,L,T1. ( elim H // | #T0 #T #HLT1 #HLT2 #IHT #HT10 #HT12 destruct elim (eq_term_dec T0 T) #HT0 - [ -HLT1 -HLT2 -H /3 width=1/ - | -IHT -HT12 /4 width=3/ + [ -HLT1 -HLT2 -H /3 width=1 by/ + | -IHT -HT12 /4 width=3 by csxa_cpxs_trans/ ] ] qed. @@ -79,17 +83,17 @@ qed. (* Main properties **********************************************************) theorem csx_csxa: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T. -#h #g #G #L #T #H @(csx_ind … H) -T /4 width=1/ +#h #g #G #L #T #H @(csx_ind … H) -T /4 width=1 by csxa_intro_cpx/ qed. theorem csxa_csx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] T. -#h #g #G #L #T #H @(csxa_ind … H) -T /4 width=1/ +#h #g #G #L #T #H @(csxa_ind … H) -T /4 width=1 by cpx_cpxs, csx_intro/ qed. (* Basic_1: was just: sn3_pr3_trans *) lemma csx_cpxs_trans: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 → ∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → ⦃G, L⦄ ⊢ ⬊*[h, g] T2. -#h #g #G #L #T1 #HT1 #T2 #H @(cpxs_ind … H) -T2 // /2 width=3 by csx_cpx_trans/ +#h #g #G #L #T1 #HT1 #T2 #H @(cpxs_ind … H) -T2 /2 width=3 by csx_cpx_trans/ qed-. (* Main eliminators *********************************************************) @@ -99,6 +103,5 @@ lemma csx_ind_alt: ∀h,g,G,L. ∀R:predicate term. (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → R T2) → R T1 ) → ∀T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → R T. -#h #g #G #L #R #H0 #T1 #H @(csxa_ind … (csx_csxa … H)) -T1 #T1 #HT1 #IHT1 -@H0 -H0 /2 width=1/ -HT1 /3 width=1/ +#h #g #G #L #R #H0 #T1 #H @(csxa_ind … (csx_csxa … H)) -T1 /4 width=1 by csxa_csx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_fpbc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_fpbc.ma new file mode 100644 index 000000000..b97478371 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_fpbc.ma @@ -0,0 +1,30 @@ +include "basic_2/computation/fpbc.ma". + +(* Advanced eliminators *****************************************************) + +fact csx_ind_fpbc_aux: ∀h,g. ∀R:relation3 genv lenv term. + (∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 → + (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) → + R G1 L1 T1 + ) → + ∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 → + ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → R G2 L2 T2. +#h #g #R #IH1 #G1 #L1 #T1 #H @(csx_ind … H) -T1 +#T1 @(fqup_wf_ind … G1 L1 T1) -G1 -L1 -T1 +#G1 #L1 #T1 #IH2 #H1 #IH3 #G2 #L2 #T2 #H12 @IH1 -IH1 /2 width=5 by csx_fqus_conf/ +#G #L #T * +[ #G0 #L0 #T0 #H20 lapply (fqus_fqup_trans … H12 H20) -G2 -L2 -T2 + #H10 @(IH2 … H10) -IH2 /2 width=5 by csx_fqup_conf/ + #T2 #HT02 #H #G3 #L3 #T3 #HT23 elim (fqup_cpx_trans_neq … H10 … HT02 H) -T0 + /4 width=8 by fqup_fqus_trans, fqup_fqus/ +| #T0 #HT20 #H elim (fqus_cpxs_trans_neq … H12 … HT20 H) -T2 /3 width=4 by/ +] +qed-. + +lemma csx_ind_fpbc: ∀h,g. ∀R:relation3 genv lenv term. + (∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 → + (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) → + R G1 L1 T1 + ) → + ∀G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → R G L T. +/4 width=8 by csx_ind_fpbc_fqus/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma index 6c38825c8..5194bedfe 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma @@ -13,7 +13,6 @@ (**************************************************************************) include "basic_2/reduction/cnx_lift.ma". -include "basic_2/reduction/fpbc.ma". include "basic_2/computation/acp.ma". include "basic_2/computation/csx.ma". @@ -108,35 +107,6 @@ lemma csx_fqus_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, ] qed-. -(* Advanced eliminators *****************************************************) - -lemma csx_ind_fpbc_fqus: ∀h,g. ∀R:relation3 genv lenv term. - (∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 → - (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) → - R G1 L1 T1 - ) → - ∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 → - ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → R G2 L2 T2. -#h #g #R #IH1 #G1 #L1 #T1 #H @(csx_ind … H) -T1 -#T1 @(fqup_wf_ind … G1 L1 T1) -G1 -L1 -T1 -#G1 #L1 #T1 #IH2 #H1 #IH3 #G2 #L2 #T2 #H12 @IH1 -IH1 /2 width=5 by csx_fqus_conf/ -#G #L #T * -[ #G0 #L0 #T0 #H20 lapply (fqus_strap1_fqu … H12 H20) -G2 -L2 -T2 - #H10 @(IH2 … H10) -IH2 /2 width=5 by csx_fqup_conf/ - #T2 #HT02 #H #G3 #L3 #T3 #HT23 elim (fqup_cpx_trans_neq … H10 … HT02 H) -T0 - /4 width=8 by fqup_fqus_trans, fqup_fqus/ -| #T0 #HT20 #H elim (fqus_cpx_trans_neq … H12 … HT20 H) -T2 /3 width=4 by/ -] -qed-. - -lemma csx_ind_fpbc: ∀h,g. ∀R:relation3 genv lenv term. - (∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 → - (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) → - R G1 L1 T1 - ) → - ∀G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → R G L T. -/4 width=8 by csx_ind_fpbc_fqus/ qed-. - (* Main properties **********************************************************) theorem csx_acp: ∀h,g. acp (cpx h g) (eq …) (csx h g). diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fleq.ma deleted file mode 100644 index da608196c..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fleq.ma +++ /dev/null @@ -1,32 +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/lazyeq_8.ma". -include "basic_2/computation/lpxs.ma". - -(* EQUIVALENT "BIG TREE" NORMAL FORMS ***************************************) - -(* Note: this definition works but is not symmetric nor decidable *) -definition fleq: ∀h. sd h → tri_relation genv lenv term ≝ - λh,g,G1,L1,T1,G2,L2,T2. - ∧∧ G1 = G2 & ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 & T1 = T2. - -interpretation - "equivalent 'big tree' normal forms (closure)" - 'LazyEq h g G1 L1 T1 G2 L2 T2 = (fleq h g G1 L1 T1 G2 L2 T2). - -(* Basic_properties *********************************************************) - -lemma fleq_refl: ∀h,g. tri_reflexive … (fleq h g). -/2 width=1 by and3_intro/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc.ma new file mode 100644 index 000000000..a66e1ac90 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc.ma @@ -0,0 +1,47 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relocation/lleq.ma". +include "basic_2/computation/fpbs.ma". + +(* ATOMIC "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES ***************) + +inductive fpbc (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝ +| fpbc_fqup: ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → fpbc h g G1 L1 T1 G2 L2 T2 +| fpbc_cpxs: ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → fpbc h g G1 L1 T1 G1 L1 T2 +| fpbc_lpxs: ∀L2. ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[0, T1] L2 → ⊥) → fpbc h g G1 L1 T1 G1 L2 T1 +. + +interpretation + "'big tree' proper parallel reduction (closure)" + 'BTPRedProper h g G1 L1 T1 G2 L2 T2 = (fpbc h g G1 L1 T1 G2 L2 T2). + +(* Basic properties *********************************************************) + +lemma cprs_fpbc: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) → + ⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄. +/3 width=1 by fpbc_cpxs, cprs_cpxs/ qed. + +lemma lprs_fpbc: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡* L2 → (L1 ⋕[0, T] L2 → ⊥) → + ⦃G, L1, T⦄ ≻[h, g] ⦃G, L2, T⦄. +/3 width=1 by fpbc_lpxs, lprs_lpxs/ qed. + +(* Basic forward lemmas *****************************************************) + +lemma fpbc_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 * -G2 -L2 -T2 +/3 width=1 by lpxs_fpbs, cpxs_fpbs, fqup_fpbs/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fpns.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fpns.ma new file mode 100644 index 000000000..fc1a71f5b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fpns.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/computation/lpxs_lleq.ma". +include "basic_2/computation/fpns.ma". +include "basic_2/computation/fpbs_alt.ma". +include "basic_2/computation/fpbc.ma". + +(* ATOMIC "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES ***************) + +(* Forward lemmas on parallel computation for "big tree" normal forms *******) + +lemma fpbs_fwd_fpbc_sn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, 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(fpbs_fpbsa … H) -H +#L #T #HT1 #HT2 #HL2 elim (eq_term_dec T1 T) #H destruct +[ -HT1 elim (fqus_inv_gen … HT2) -HT2 + [ #HT2 elim (fqup_inv_step_sn … HT2) -HT2 + #H6 #H7 #H8 #H9 #H10 @or_intror @(ex2_3_intro … H6 H7 H8) + /5 width=9 by fpbsa_inv_fpbs, fpbc_fqup, fqu_fqup, ex3_2_intro, ex2_3_intro, or_intror/ + | * #HG #HL #HT destruct elim (lleq_dec T2 L L2 0) #H + [ /3 width=1 by fpns_intro, or_introl/ + | elim (lpxs_nlleq_inv_step_sn … HL2 H) -HL2 -H + /5 width=5 by fpbc_lpxs, lpxs_fpbs, ex2_3_intro, or_intror/ + ] + ] +| elim (cpxs_neq_inv_step_sn … HT1 H) -HT1 -H + /5 width=9 by fpbsa_inv_fpbs, fpbc_cpxs, cpx_cpxs, ex3_2_intro, ex2_3_intro, or_intror/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_lift.ma new file mode 100644 index 000000000..6915c72cf --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_lift.ma @@ -0,0 +1,32 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/ssta_ssta.ma". +include "basic_2/computation/cpxs_lift.ma". +include "basic_2/computation/fpbc.ma". + +(* ATOMIC "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES ***************) + +(* Advanced properties ******************************************************) + +lemma lsstas_fpbc: ∀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_cpxs, lsstas_cpxs/ qed. + +lemma ssta_fpbc: ∀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⦄. +#h #g #G #L #T1 #T2 #l #HT1 #HT12 elim (eq_term_dec T1 T2) +/3 width=5 by ssta_lsstas, lsstas_fpbc/ #H destruct +elim (ssta_inv_refl_pos … HT1 … HT12) +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma index faf5dd7d9..a96b0bbbd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma @@ -13,8 +13,7 @@ (**************************************************************************) include "basic_2/notation/relations/btpredstarproper_8.ma". -include "basic_2/reduction/fpbc.ma". -include "basic_2/computation/fpbs.ma". +include "basic_2/computation/fpbc.ma". (* GENEARAL "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES *************) @@ -24,6 +23,9 @@ inductive fpbg (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝ 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)" @@ -34,5 +36,5 @@ interpretation "'big tree' proper parallel computation (closure)" 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=5 by fpbg_cpxs, fpbg_fqup, fqu_fqup, cpx_cpxs/ +/3 width=9 by fpbg_fqup, fpbg_cpxs, fpbg_lpxs/ 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 9022732dc..97846fda4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "basic_2/computation/lpxs_lpxs.ma". include "basic_2/computation/fpbs_alt.ma". include "basic_2/computation/fpbg.ma". @@ -22,20 +23,26 @@ include "basic_2/computation/fpbg.ma". 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_fqup_fpbs, fpbs_trans, lpxs_fpbs, cpxs_fpbs/ +/3 width=5 by cpxs_fqus_lpxs_fpbs, cpxs_fqup_fpbs, fpbs_trans, lpxs_fpbs, cpxs_fpbs/ qed-. -lemma fpbg_fwd_fpb_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⦄. +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 -[ #L2 #T2 #HT12 #H #HL12 - elim (cpxs_neq_inv_step_sn … HT12 H) -HT12 -H - /4 width=9 by fpbsa_inv_fpbs, fpbc_cpx, ex3_2_intro, ex2_3_intro/ +[ /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 elim (fqup_inv_step_sn … HT2) -HT2 - /4 width=9 by fpbsa_inv_fpbs, fpbc_fqu, ex3_2_intro, ex2_3_intro/ - | elim (cpxs_neq_inv_step_sn … HT1 H) -HT1 -H - /5 width=9 by fpbsa_inv_fpbs, fpbc_cpx, fqup_fqus, ex3_2_intro, ex2_3_intro/ + [ -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-. 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 7a964e40f..26dec0777 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/computation/cpxs_lift.ma". +include "basic_2/computation/fpbc_lift.ma". include "basic_2/computation/fpbg.ma". (* GENERAL "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *********************) @@ -21,4 +21,8 @@ include "basic_2/computation/fpbg.ma". 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 fpbg_cpxs, lsstas_cpxs/ qed. +/4 width=5 by fpbc_fpbg, lsstas_fpbc/ 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. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fleq.ma deleted file mode 100644 index 826500bf1..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fleq.ma +++ /dev/null @@ -1,36 +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/reduction/fpbc.ma". -include "basic_2/computation/fleq.ma". -include "basic_2/computation/fpbs_alt.ma". - -(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) - -(* Forward lemmas on equivalent "big tree" normal forms *********************) - -lemma fpbs_fwd_fpb_sn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, 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(fpbs_fpbsa … H) -H -#L #T #HT1 #HT2 #HL2 elim (eq_term_dec T1 T) #H destruct -[ -HT1 elim (fqus_inv_gen … HT2) -HT2 - [ #HT2 elim (fqup_inv_step_sn … HT2) -HT2 - /5 width=9 by fpbsa_inv_fpbs, fpbc_fqu, ex3_2_intro, ex2_3_intro, or_intror/ - | * #HG #HL #HT destruct /3 width=1 by and3_intro, or_introl/ - ] -| elim (cpxs_neq_inv_step_sn … HT1 H) -HT1 -H - /5 width=9 by fpbsa_inv_fpbs, fpbc_cpx, ex3_2_intro, ex2_3_intro, or_intror/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbs.ma index 1135589db..6a868cfa9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbs.ma @@ -32,3 +32,11 @@ lemma cpr_lpr_ssta_fpbs: ∀h,g,G,L1,L2,T1,T2,U2,l2. lemma cpxs_fqup_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⦄. /3 width=5 by fpbs_trans, cpxs_fpbs, fqup_fpbs/ 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⦄. +/3 width=5 by fpbs_trans, cpxs_fpbs, fqus_fpbs/ qed. + +lemma cpxs_fqus_lpxs_fpbs: ∀h,g,G1,G2,L1,L,L2,T1,T,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T → + ⦃G1, L1, T⦄ ⊃* ⦃G2, L, T2⦄ → ⦃G2, L⦄ ⊢ ➡*[h, g] L2 → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. +/3 width=5 by fpbs_trans, cpxs_fqus_fpbs, lpxs_fpbs/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma index a6d662799..64090eec9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma @@ -13,8 +13,8 @@ (**************************************************************************) include "basic_2/notation/relations/btsn_5.ma". -include "basic_2/reduction/fpbc.ma". -include "basic_2/computation/csx.ma". +include "basic_2/computation/fpbc.ma". +include "basic_2/computation/csx_alt.ma". (* "BIG TREE" 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, fpbc_cpx/ +#h #g #G #L #T #H elim H -G -L -T /5 width=1 by csx_intro_cprs, fpbc_cpxs/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma index dd325e85a..a36a267a5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma @@ -18,6 +18,20 @@ include "basic_2/computation/lpxs_cpxs.ma". (* SN EXTENDED PARALLEL COMPUTATION FOR LOCAL ENVIRONMENTS ******************) +(* Inversion lemmas on lazy equivalence for local environments **************) + +lemma lpxs_nlleq_inv_step_sn: ∀h,g,G,L1,L2,T,d. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[d, T] L2 → ⊥) → + ∃∃L. ⦃G, L1⦄ ⊢ ➡*[h, g] L & L1 ⋕[d, T] L → ⊥ & ⦃G, L⦄ ⊢ ➡*[h, g] L2. +#h #g #G #L1 #L2 #T #d #H @(lpxs_ind_dx … H) -L1 +[ #H elim H -H // +| #L1 #L #H1 #H2 #IH2 #H12 elim (lleq_dec T L1 L d) #H + [ -H2 elim IH2 -IH2 + /4 width=4 by lpxs_strap2, lleq_canc_sn, lleq_trans, ex3_intro/ + | -IH2 -H12 /3 width=4 by lpx_lpxs, ex3_intro/ (**) (* auto fails without clear *) + ] +] +qed-. + (* Properties on lazy equivalence for local environments ********************) lemma lpxs_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_8.ma deleted file mode 100644 index 052b1ad75..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_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 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" - non associative with precedence 45 - for @{ 'LazyEq $h $g $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc.ma deleted file mode 100644 index 45e671601..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc.ma +++ /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 *) -(* *) -(**************************************************************************) - -include "basic_2/notation/relations/btpredproper_8.ma". -include "basic_2/reduction/fpb.ma". - -(* "BIG TREE" PROPER PARALLEL REDUCTION FOR CLOSURES ************************) - -inductive fpbc (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝ -| fpbc_fqu: ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → fpbc h g G1 L1 T1 G2 L2 T2 -| fpbc_cpx: ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T2 → (T1 = T2 → ⊥) → fpbc h g G1 L1 T1 G1 L1 T2 -. - -interpretation - "'big tree' proper parallel reduction (closure)" - 'BTPRedProper h g G1 L1 T1 G2 L2 T2 = (fpbc h g G1 L1 T1 G2 L2 T2). - -(* Basic properties *********************************************************) - -lemma cpr_fpbc: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → - ⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄. -/3 width=1 by fpbc_cpx, cpr_cpx/ qed. - -(* Basic forward lemmas *****************************************************) - -lemma fpbc_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, fqu_fquq/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc_lift.ma deleted file mode 100644 index 987258b79..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc_lift.ma +++ /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/static/ssta_ssta.ma". -include "basic_2/reduction/cpx_lift.ma". -include "basic_2/reduction/fpbc.ma". - -(* "BIG TREE" PROPER PARALLEL REDUCTION FOR CLOSURES ************************) - -(* Advanced properties ******************************************************) - -lemma ssta_fpbc: ∀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⦄. -#h #g #G #L #T1 #T2 #l #HT1 #HT12 elim (eq_term_dec T1 T2) -/3 width=5 by fpbc_cpx, ssta_cpx/ #H destruct -elim (ssta_inv_refl_pos … HT1 … HT12) -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index 9d490be16..bdd170770 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 @@ -88,14 +88,15 @@ table { [ "csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csx_lift" + "csx_lpx" * ] } ] - [ { "parallel computation for \"big tree\" normal forms" * } { - [ "fpns ( ⦃?,?,?⦄ ⊢ ⋕➡*[?,?] ⦃?,?,?⦄ )" "fpns_fpns" * ] - } - ] [ { "\"big tree\" parallel computation" * } { [ "fpbr ( ⦃?,?,?⦄ ⊃≥[?,?] ⦃?,?,?⦄ )" "fpbr_fpbr" * ] [ "fpbg ( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fpbg" * ] - [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_fleq" + "fpbs_fpbs" * ] + [ "fpbc ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpbc_lift" + "fpbc_fpns" * ] + [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_fpbs" * ] + } + ] + [ { "parallel computation for \"big tree\" normal forms" * } { + [ "fpns ( ⦃?,?,?⦄ ⊢ ⋕➡*[?,?] ⦃?,?,?⦄ )" "fpns_fpns" * ] } ] [ { "decomposed extended computation" * } { @@ -125,7 +126,6 @@ table { class "water" [ { "reduction" * } { [ { "\"big tree\" parallel reduction" * } { - [ "fpbc ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpbc_lift" * ] [ "fpb ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )" "fpb_lift" * ] } ]