From 9aa2722ff4aa7868ffd14e5a820cd6dc79e2c8a6 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 18 Aug 2018 15:51:05 +0200 Subject: [PATCH] severe bug found in parallel zeta + partial commit: component "dynamic" corrected + some additions towards preservation --- .../lambdadelta/basic_2/dynamic/cnv.ma | 11 ++ .../basic_2/dynamic/cnv_cpm_conf.ma | 51 ++++---- .../basic_2/dynamic/cnv_cpm_tdeq.ma | 109 ++++++++++++++++++ .../basic_2/dynamic/cnv_cpm_trans.ma | 6 +- .../lambdadelta/basic_2/dynamic/cnv_fsb.ma | 6 + .../basic_2/rt_computation/fpbg.ma | 8 ++ .../basic_2/rt_computation/fpbg_fqup.ma | 6 + .../lambdadelta/basic_2/web/basic_2_src.tbl | 2 +- 8 files changed, 171 insertions(+), 28 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma index 97c1feca2..bde05a33c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma @@ -140,6 +140,17 @@ lemma cnv_inv_cast (a) (h): ∀G,L,U,T. ⦃G, L⦄ ⊢ ⓝU.T ![a, h] → ⦃G, L⦄ ⊢ U ➡*[h] U0 & ⦃G, L⦄ ⊢ T ➡*[1, h] U0. /2 width=3 by cnv_inv_cast_aux/ qed-. +(* Basic forward lemmas *****************************************************) + +lemma cnv_fwd_flat (a) (h) (I) (G) (L): + ∀V,T. ⦃G, L⦄ ⊢ ⓕ{I}V.T ![a,h] → + ∧∧ ⦃G, L⦄ ⊢ V ![a,h] & ⦃G, L⦄ ⊢ T ![a,h]. +#a #h * #G #L #V #T #H +[ elim (cnv_inv_appl … H) #n #p #W #U #_ #HV #HT #_ #_ +| elim (cnv_inv_cast … H) #U #HV #HT #_ #_ +] -H /2 width=1 by conj/ +qed-. + (* Basic_2A1: removed theorems 6: snv_fwd_da snv_fwd_lstas snv_cast_scpes shnv_cast shnv_inv_cast snv_shnv_cast diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma index 70398eaac..75e1ae220 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma @@ -128,37 +128,39 @@ qed-. fact cnv_cpm_conf_lpr_bind_zeta_aux (a) (h) (o) (G) (L) (V) (T): (∀G0,L0,T0. ⦃G,L,+ⓓV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) → ⦃G,L⦄ ⊢ +ⓓV.T ![a,h] → - ∀V1. ⦃G,L⦄ ⊢V ➡[h] V1 → - ∀n1,T1. ⦃G,L.ⓓV⦄ ⊢ T ➡[n1,h] T1 → ∀n2,T2. ⦃G,L.ⓓV⦄ ⊢ T ➡[n2,h] T2 → - ∀XT2. ⬆*[1]XT2 ≘ T2 → + ∀V1. ⦃G,L⦄ ⊢V ➡[h] V1 → ∀n1,T1. ⦃G,L.ⓓV⦄ ⊢ T ➡[n1,h] T1 → + ∀T2. ⬆*[1]T2 ≘ T → ∀n2,XT2. ⦃G,L⦄ ⊢ T2 ➡[n2,h] XT2 → ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 → ∃∃T. ⦃G,L1⦄ ⊢ +ⓓV1.T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ XT2 ➡*[n1-n2,h] T. #a #h #o #G0 #L0 #V0 #T0 #IH #H0 -#V1 #HV01 #n1 #T1 #HT01 #n2 #T2 #HT02 #XT2 #HXT2 +#V1 #HV01 #n1 #T1 #HT01 #T2 #HT20 #n2 #XT2 #HXT2 #L1 #HL01 #L2 #HL02 elim (cnv_inv_bind … H0) -H0 #_ #HT0 -elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 (L1.ⓓV1) … (L2.ⓓV1)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ] -L0 -T0 -V0 -#T #HT1 #HT2 -elim (cpms_inv_lifts_sn … HT2 (Ⓣ) … L2 … HXT2) -T2 [| /3 width=1 by drops_refl, drops_drop/ ] #XT #HXT #HXT2 +lapply (cnv_inv_lifts … HT0 (Ⓣ) … L0 … HT20) -HT0 +[ /3 width=3 by drops_refl, drops_drop/ ] #HT2 +elim (cpm_inv_lifts_sn … HT01 (Ⓣ) … L0 … HT20) -HT01 +[| /3 width=1 by drops_refl, drops_drop/ ] #XT1 #HXT1 #HXT12 +elim (cnv_cpm_conf_lpr_far … IH … HXT12 … HXT2 … HL01 … HL02) +[|*: /3 width=1 by fqup_fpbg, fqup_zeta/ ] -L0 -T0 -V0 #T #HT1 #HT2 /3 width=3 by cpms_zeta, ex2_intro/ qed-. fact cnv_cpm_conf_lpr_zeta_zeta_aux (a) (h) (o) (G) (L) (V) (T): (∀G0,L0,T0. ⦃G,L,+ⓓV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) → ⦃G,L⦄ ⊢ +ⓓV.T ![a,h] → - ∀n1,T1. ⦃G,L.ⓓV⦄ ⊢ T ➡[n1,h] T1 → ∀n2,T2. ⦃G,L.ⓓV⦄ ⊢ T ➡[n2,h] T2 → - ∀XT1. ⬆*[1]XT1 ≘ T1 → ∀XT2. ⬆*[1]XT2 ≘ T2 → + ∀T1. ⬆*[1]T1 ≘ T → ∀T2. ⬆*[1]T2 ≘ T → + ∀n1,XT1. ⦃G,L⦄ ⊢ T1 ➡[n1,h] XT1 → ∀n2,XT2. ⦃G,L⦄ ⊢ T2 ➡[n2,h] XT2 → ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 → ∃∃T. ⦃G,L1⦄ ⊢ XT1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ XT2 ➡*[n1-n2,h] T. #a #h #o #G0 #L0 #V0 #T0 #IH #H0 -#n1 #T1 #HT01 #n2 #T2 #HT02 #XT1 #HXT1 #XT2 #HXT2 +#T1 #HT10 #T2 #HT20 #n1 #XT1 #HXT1 #n2 #XT2 #HXT2 #L1 #HL01 #L2 #HL02 elim (cnv_inv_bind … H0) -H0 #_ #HT0 -elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 (L1.ⓓV0) … (L2.ⓓV0)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ] -L0 -T0 -#T #HT1 #HT2 -elim (cpms_inv_lifts_sn … HT1 (Ⓣ) … L1 … HXT1) -T1 /3 width=2 by drops_refl, drops_drop/ #XT #HXT #HXT1 -elim (cpms_inv_lifts_sn … HT2 (Ⓣ) … L2 … HXT2) -T2 /3 width=2 by drops_refl, drops_drop/ #X #H #HXT2 -lapply (lifts_inj … H … HXT) -T #H destruct +lapply (lifts_inj … HT10 … HT20) -HT10 #H destruct +lapply (cnv_inv_lifts … HT0 (Ⓣ) … L0 … HT20) -HT0 +[ /3 width=3 by drops_refl, drops_drop/ ] #HT2 +elim (cnv_cpm_conf_lpr_far … IH … HXT1 … HXT2 … HL01 … HL02) +[|*: /3 width=1 by fqup_fpbg, fqup_zeta/ ] -L0 -T0 #T #HT1 #HT2 /2 width=3 by ex2_intro/ qed-. @@ -216,18 +218,19 @@ fact cnv_cpm_conf_lpr_appl_theta_aux (a) (h) (o) (p) (G) (L) (V) (W) (T): elim (cnv_inv_appl … H0) -H0 #n0 #p0 #X01 #X02 #_ #HV0 #H0 #_ #_ -n0 -p0 -X01 -X02 elim (cnv_inv_bind … H0) -H0 #HW0 #HT0 elim (cpr_conf_lpr … HV01 … HV02 … HL01 … HL02) #V #HV1 #HV2 -elim (cpm_lifts_sn … HV2 (Ⓣ) … (L2.ⓓW2) … HVU2) -HVU2 [| /3 width=1 by drops_refl, drops_drop/ ] #U #HVU #HU2 elim (cpm_inv_abbr1 … HX) -HX * [ #W1 #T1 #HW01 #HT01 #H destruct + elim (cpm_lifts_sn … HV2 (Ⓣ) … (L2.ⓓW2) … HVU2) -HVU2 [| /3 width=1 by drops_refl, drops_drop/ ] #U #HVU #HU2 elim (cpr_conf_lpr … HW01 … HW02 … HL01 … HL02) #W #HW1 #HW2 elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ] #T #HT1 #HT2 -L0 -V0 -W0 -T0 /4 width=7 by cpms_theta_dx, cpms_appl_dx, cpms_bind_dx, ex2_intro/ -| #T1 #HT01 #HX #H destruct - elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 (L1.ⓓW2) … (L2.ⓓW2)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ] - #T #HT1 #HT2 -L0 -V0 -W0 -T0 - elim (cpms_inv_lifts_sn … HT1 (Ⓣ) … L1 … HX) -T1 [| /3 width=1 by drops_refl, drops_drop/ ] #X0 #HXT #HX0 - /4 width=7 by cpms_zeta, cpms_appl_dx, lifts_flat, ex2_intro/ +| #X0 #HXT0 #H1X0 #H destruct + lapply (cnv_inv_lifts … HT0 (Ⓣ) … L0 … HXT0) -HT0 [ /3 width=3 by drops_refl, drops_drop/ ] #H2X0 + elim (cpm_inv_lifts_sn … HT02 (Ⓣ) … L0 … HXT0) -HT02 [| /3 width=1 by drops_refl, drops_drop/ ] #X2 #HXT2 #HX02 + elim (cnv_cpm_conf_lpr_far … IH … H1X0 … HX02 … HL01 … HL02) + [|*: /4 width=5 by fqup_fpbg, fqup_strap1, fqu_drop/ ] #T #HT1 #HT2 -L0 -V0 -W0 -T0 + /4 width=8 by cpms_zeta, cpms_appl_dx, lifts_flat, ex2_intro/ ] qed-. @@ -436,11 +439,11 @@ fact cnv_cpm_conf_lpr_aux (a) (h) (o): elim (cpm_inv_bind1 … HX2) -HX2 * [ #V2 #T2 #HV2 #HT2 #H21 #V1 #T1 #HV1 #HT1 #H11 destruct -IH2 @(cnv_cpm_conf_lpr_bind_bind_aux … IH1) -IH1 /1 width=1 by/ - | #T2 #HT2 #HXT2 #H21 #H22 #V1 #T1 #HV1 #HT1 #H11 destruct -IH2 + | #T2 #HT2 #HTX2 #H21 #H22 #V1 #T1 #HV1 #HT1 #H11 destruct -IH2 @(cnv_cpm_conf_lpr_bind_zeta_aux … IH1) -IH1 /1 width=3 by/ - | #V2 #T2 #HV2 #HT2 #H21 #T1 #HT1 #HXT1 #H11 #H12 destruct -IH2 + | #V2 #T2 #HV2 #HT2 #H21 #T1 #HT1 #HTX1 #H11 #H12 destruct -IH2 @ex2_commute @(cnv_cpm_conf_lpr_bind_zeta_aux … IH1) -IH1 /1 width=3 by/ - | #T2 #HT2 #HXT2 #H21 #H22 #T1 #HT1 #HXT1 #H11 #H12 destruct -IH2 + | #T2 #HT2 #HTX2 #H21 #H22 #T1 #HT1 #HTX1 #H11 #H12 destruct -IH2 @(cnv_cpm_conf_lpr_zeta_zeta_aux … IH1) -IH1 /1 width=3 by/ ] | #V #T #HG0 #HL0 #HT0 #HT #n1 #X1 #HX1 #n2 #X2 #HX2 #L1 #HL1 #L2 #HL2 destruct diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma new file mode 100644 index 000000000..c539798bf --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma @@ -0,0 +1,109 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/rt_transition/cpr.ma". +include "basic_2/rt_computation/fpbg_fqup.ma". +include "basic_2/dynamic/cnv_fsb.ma". + +(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************) + +(* Inversion lemmas with degree-based equivalence for terms *****************) + +lemma cnv_cpr_tdeq_fwd_refl (a) (h) (o) (G) (L): + ∀T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 → T1 ≛[h,o] T2 → + ⦃G, L⦄ ⊢ T1 ![a,h] → T1 = T2. +#a #h #o #G #L #T1 #T2 #H @(cpr_ind … H) -G -L -T1 -T2 +[ // +| #G #K #V1 #V2 #X2 #_ #_ #_ #H1 #_ -a -G -K -V1 -V2 + lapply (tdeq_inv_lref1 … H1) -H1 #H destruct // +| #I #G #K #T2 #X2 #i #_ #_ #_ #H1 #_ -a -I -G -K -T2 + lapply (tdeq_inv_lref1 … H1) -H1 #H destruct // +| #p #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #H1 #H2 + elim (tdeq_inv_pair1 … H1) -H1 #V0 #T0 #HV0 #HT0 #H destruct + elim (cnv_inv_bind … H2) -H2 #HV1 #HT1 + /3 width=3 by eq_f2/ +| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #H1 #H2 + elim (tdeq_inv_pair1 … H1) -H1 #V0 #T0 #HV0 #HT0 #H destruct + elim (cnv_fwd_flat … H2) -H2 #HV1 #HT1 + /3 width=3 by eq_f2/ +| #G #K #V #T1 #X1 #X2 #HXT1 #HX12 #_ #H1 #H2 + elim (cnv_fpbg_refl_false … o … H2) -a + @(fpbg_tdeq_div … H1) -H1 + /3 width=9 by cpm_tdneq_cpm_fpbg, cpm_zeta, tdeq_lifts_inv_pair_sn/ +| #G #L #U #T1 #T2 #HT12 #_ #H1 #H2 + elim (cnv_fpbg_refl_false … o … H2) -a + @(fpbg_tdeq_div … H1) -H1 + /3 width=6 by cpm_tdneq_cpm_fpbg, cpm_eps, tdeq_inv_pair_xy_y/ +| #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #H1 #_ + elim (tdeq_inv_pair … H1) -H1 #H #_ #_ destruct +| #p #G #L #V1 #V2 #X2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H1 #_ + elim (tdeq_inv_pair … H1) -H1 #H #_ #_ destruct +] +qed-. + +lemma cpm_tdeq_inv_bind (a) (h) (o) (n) (p) (I) (G) (L): + ∀V,T1. ⦃G, L⦄ ⊢ ⓑ{p,I}V.T1 ![a,h] → + ∀X. ⦃G, L⦄ ⊢ ⓑ{p,I}V.T1 ➡[n,h] X → ⓑ{p,I}V.T1 ≛[h,o] X → + ∃∃T2. ⦃G, L.ⓑ{I}V⦄ ⊢ T1 ➡[n,h] T2 & T1 ≛[h,o] T2 & X = ⓑ{p,I}V.T2. +#a #h #o #n #p #I #G #L #V #T1 #H0 #X #H1 #H2 +elim (cpm_inv_bind1 … H1) -H1 * +[ #XV #T2 #HXV #HT12 #H destruct + elim (tdeq_inv_pair … H2) -H2 #_ #H2XV #H2T12 + elim (cnv_inv_bind … H0) -H0 #HV #_ + lapply (cnv_cpr_tdeq_fwd_refl … HXV H2XV HV) #H destruct -HXV -H2XV -HV + /2 width=4 by ex3_intro/ +| #X1 #HXT1 #HX1 #H1 #H destruct + elim (cnv_fpbg_refl_false … o … H0) -a + @(fpbg_tdeq_div … H2) -H2 + /3 width=9 by cpm_tdneq_cpm_fpbg, cpm_zeta, tdeq_lifts_inv_pair_sn/ +] +qed-. + +lemma cpm_tdeq_inv_appl (a) (h) (o) (n) (G) (L): + ∀V,T1. ⦃G, L⦄ ⊢ ⓐV.T1 ![a,h] → + ∀X. ⦃G, L⦄ ⊢ ⓐV.T1 ➡[n,h] X → ⓐV.T1 ≛[h,o] X → + ∃∃T2. ⦃G, L⦄ ⊢ T1 ➡[n,h] T2 & T1 ≛[h,o] T2 & X = ⓐV.T2. +#a #h #o #n #G #L #V #T1 #H0 #X #H1 #H2 +elim (cpm_inv_appl1 … H1) -H1 * +[ #XV #T2 #HXV #HT12 #H destruct + elim (tdeq_inv_pair … H2) -H2 #_ #H2XV #H2T12 + elim (cnv_inv_appl … H0) -H0 #m #q #W #U #_ #HV #_ #_ #_ -m -q -W -U + lapply (cnv_cpr_tdeq_fwd_refl … HXV H2XV HV) #H destruct -HXV -H2XV -HV + /2 width=4 by ex3_intro/ +| #q #V2 #W1 #W2 #XT #T2 #_ #_ #_ #H1 #H destruct -H0 + elim (tdeq_inv_pair … H2) -H2 #H #_ #_ destruct +| #q #V2 #XV #W1 #W2 #XT #T2 #_ #_ #_ #_ #H1 #H destruct -H0 + elim (tdeq_inv_pair … H2) -H2 #H #_ #_ destruct +] +qed-. + +lemma cpm_tdeq_inv_cast (a) (h) (o) (n) (G) (L): + ∀U1,T1. ⦃G, L⦄ ⊢ ⓝU1.T1 ![a,h] → + ∀X. ⦃G, L⦄ ⊢ ⓝU1.T1 ➡[n,h] X → ⓝU1.T1 ≛[h,o] X → + ∃∃U2,T2. ⦃G, L⦄ ⊢ U1 ➡[n,h] U2 & U1 ≛[h,o] U2 & ⦃G, L⦄ ⊢ T1 ➡[n,h] T2 & T1 ≛[h,o] T2 & X = ⓝU2.T2. +#a #h #o #n #G #L #U1 #T1 #H0 #X #H1 #H2 +elim (cpm_inv_cast1 … H1) -H1 [ * || * ] +[ #U2 #T2 #HU12 #HT12 #H destruct -H0 + elim (tdeq_inv_pair … H2) -H2 #_ #H2U12 #H2T12 + /2 width=7 by ex5_2_intro/ +| #HT1X + elim (cnv_fpbg_refl_false … o … H0) -a + @(fpbg_tdeq_div … H2) -H2 + /3 width=6 by cpm_tdneq_cpm_fpbg, cpm_eps, tdeq_inv_pair_xy_y/ +| #m #HU1X #H destruct + elim (cnv_fpbg_refl_false … o … H0) -a + @(fpbg_tdeq_div … H2) -H2 + /3 width=6 by cpm_tdneq_cpm_fpbg, cpm_ee, tdeq_inv_pair_xy_x/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma index ac40d7823..7fc3ae3b4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma @@ -31,7 +31,7 @@ fact cnv_cpm_trans_lpr_aux (a) (h) (o): ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_cnv_cpm_trans_lpr a h G1 L1 T1. #a #h #o #G0 #L0 #T0 #IH2 #IH1 #G1 #L1 * * [|||| * ] [ #s #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #_ destruct -IH2 -IH1 -H1 - elim (cpm_inv_sort1 … H2) -H2 * #H1 #H2 destruct // + elim (cpm_inv_sort1 … H2) -H2 #H #_ destruct // | #i #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct -IH2 elim (cnv_inv_lref_drops … H1) -H1 #I #K1 #V1 #HLK1 #HV1 elim (lpr_drops_conf … HLK1 … HL12) -HL12 // #Y #H #HLK2 @@ -52,8 +52,8 @@ fact cnv_cpm_trans_lpr_aux (a) (h) (o): elim (cnv_inv_bind … H1) -H1 #HV1 #HT1 elim (cpm_inv_bind1 … H2) -H2 * [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=9 by fqup_fpbg, cnv_bind, lpr_pair/ - | #T2 #HT12 #HXT2 #H1 #H2 destruct -HV1 - /4 width=11 by fqup_fpbg, cnv_inv_lifts, lpr_pair, drops_refl, drops_drop/ + | #X1 #HXT1 #HX1 #H1 #H2 destruct -HV1 + /5 width=7 by cnv_inv_lifts, fqup_fpbg, fqup_zeta, drops_refl, drops_drop/ ] | #V1 #T1 #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct elim (cnv_inv_appl … H1) -H1 #n #p #W1 #U1 #Hn #HV1 #HT1 #HVW1 #HTU1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fsb.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fsb.ma index e7c4a6c61..4ce63d92a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fsb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fsb.ma @@ -23,3 +23,9 @@ include "basic_2/dynamic/cnv_aaa.ma". lemma cnv_fwd_fsb (a) (h) (o): ∀G,L,T. ⦃G, L⦄ ⊢ T ![a, h] → ≥[h, o] 𝐒⦃G, L, T⦄. #a #h #o #G #L #T #H elim (cnv_fwd_aaa … H) -H /2 width=2 by aaa_fsb/ qed-. + +(* Inversion lemmas with proper parallel rst-computation for closures *******) + +lemma cnv_fpbg_refl_false (a) (h) (o) (G) (L) (T): + ⦃G, L⦄ ⊢ T ![a,h] → ⦃G, L, T⦄ >[h,o] ⦃G, L, T⦄ → ⊥. +/3 width=7 by cnv_fwd_fsb, fsb_fpbg_refl_false/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma index e3232f7e1..bda560f42 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma @@ -48,3 +48,11 @@ qed-. lemma fpbg_fdeq_trans: ∀h,o,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ >[h, o] ⦃G, L, T⦄ → ∀G2,L2,T2. ⦃G, L, T⦄ ≛[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄. /3 width=5 by fpbg_fpbq_trans, fpbq_fdeq/ qed-. + +(* Properties with t-bound rt-transition for terms **************************) + +lemma cpm_tdneq_cpm_fpbg (h) (o) (G) (L): + ∀n1,T1,T. ⦃G, L⦄ ⊢ T1 ➡[n1,h] T → (T1 ≛[h,o] T → ⊥) → + ∀n2,T2. ⦃G, L⦄ ⊢ T ➡[n2,h] T2 → + ⦃G, L, T1⦄ >[h,o] ⦃G, L, T2⦄. +/4 width=5 by fpbq_fpbs, cpm_fpbq, cpm_fpb, ex2_3_intro/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqup.ma index 6cebf2c21..ce02c890a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqup.ma @@ -17,6 +17,12 @@ include "basic_2/rt_computation/fpbg.ma". (* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************) +(* Advanced properties with degree-based equivalence for terms **************) + +lemma fpbg_tdeq_div: ∀h,o,G1,G2,L1,L2,T1,T. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T⦄ → + ∀T2. T2 ≛[h, o] T → ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄. +/4 width=5 by fpbg_fdeq_trans, tdeq_fdeq, tdeq_sym/ qed-. + (* Properties with plus-iterated structural successor for closures **********) (* Note: this is used in the closure proof *) 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 65ad7dd16..45e8c1318 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 @@ -31,7 +31,7 @@ table { *) [ { "context-sensitive native validity" * } { [ [ "restricted refinement for lenvs" ] "lsubv ( ? ⊢ ? ⫃![?,?] ? )" "lsubv_drops" + "lsubv_lsubr" + "lsubv_lsuba" + "lsubv_cpms" + "lsubv_cpcs" + "lsubv_cnv" + "lsubv_lsubv" * ] - [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpms_conf" + "cnv_preserve_far" (* + "cnv_preserve" *) * ] + [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpms_conf" + "cnv_preserve_far" (* + "cnv_preserve" *) * ] } ] } -- 2.39.2