From: Ferruccio Guidi Date: Wed, 12 Sep 2018 13:55:58 +0000 (+0200) Subject: update in ground_2, static_2, basic_2 X-Git-Tag: make_still_working~282 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=b98ec1a1a37602eca524dc5487c357a200bbb5b6 update in ground_2, static_2, basic_2 + minor additioms --- 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 7a62a9acd..b9b6e4bf8 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 @@ -15,7 +15,6 @@ include "ground_2/lib/arith_2b.ma". include "basic_2/rt_transition/lpr_lpr.ma". include "basic_2/rt_computation/cpms_lsubr.ma". -include "basic_2/rt_computation/cpms_fpbg.ma". include "basic_2/rt_computation/cpms_cpms.ma". include "basic_2/dynamic/cnv_drops.ma". include "basic_2/dynamic/cnv_preserve_sub.ma". @@ -220,7 +219,7 @@ elim (cnv_inv_bind … H0) -H0 #HW0 #HT0 elim (cpr_conf_lpr … HV01 … HV02 … HL01 … HL02) #V #HV1 #HV2 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 (cpm_lifts_sn … HV2 (Ⓣ) … (L2.ⓓW2) … HVU2) -HV2 -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_sub … IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ] #T #HT1 #HT2 -L0 -V0 -W0 -T0 @@ -396,10 +395,10 @@ fact cnv_cpm_conf_lpr_aux (a) (h) (o): [ #I #HG0 #HL0 #HT0 #HT #n1 #X1 #HX1 #n2 #X2 #HX2 #L1 #HL1 #L2 #HL2 destruct elim (cpm_inv_atom1_drops … HX1) -HX1 * elim (cpm_inv_atom1_drops … HX2) -HX2 * - [ #H21 #H22 #H11 #H12 destruct -L -a -o + [ #H21 #H22 #H11 #H12 destruct -a -o -L [h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_trans_lpr a h G1 L1 T1. #a #h #o #G0 #L0 #T0 #IH #G1 #L1 #T1 #H01 #HT1 #n #T2 #H @(cpms_ind_dx … H) -n -T2 -/4 width=7 by cpms_fwd_fpbs, fpbg_fpbs_trans/ +/3 width=7 by fpbg_cpms_trans/ qed-. fact cnv_cpm_conf_lpr_sub (a) (h) (o): diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cnv/cnv_cpm_tdeq1_conf.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cnv/cnv_cpm_tdeq1_conf.etc new file mode 100644 index 000000000..01de9e4d1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cnv/cnv_cpm_tdeq1_conf.etc @@ -0,0 +1,377 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cpm_lsubr.ma". +include "basic_2/rt_transition/lpr_drops.ma". +include "basic_2/dynamic/cnv_drops.ma". +include "basic_2/dynamic/cnv_cpm_tdeq.ma". +include "basic_2/dynamic/cnv_preserve_sub.ma". + +(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) + +definition IH_cnv_cpm_tdeq1_conf_lpr (a) (h) (o): relation3 genv lenv term ≝ + λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] → + ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡[n1,h] T1 → T0 ≛[h,o] T1 → + ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡[n2,h] T2 → + ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → L0 ≛[h, o, T0] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 → + ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡[n2-n1,h] T & ⦃G, L2⦄ ⊢ T2 ➡[n1-n2,h] T & T2 ≛[h,o] T. + +definition IH_cnv_cpms_tdeq1_strip_lpr (a) (h) (o): relation3 genv lenv term ≝ + λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] → + ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡[n1,h] T1 → T0 ≛[h,o] T1 → + ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡*[n2,h] T2 → + ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → L0 ≛[h, o, T0] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 → + ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G, L2⦄ ⊢ T2 ➡[n1-n2,h] T & T2 ≛[h,o] T. + +definition IH_cnv_cpm_tdeq2_conf_lpr (a) (h) (o): relation3 genv lenv term ≝ + λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] → + ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡[n1,h] T1 → T0 ≛[h,o] T1 → + ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡[n2,h] T2 → T0 ≛[h,o] T2 → + ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 → + ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡[n2-n1,h] T & T1 ≛[h,o] T & ⦃G, L2⦄ ⊢ T2 ➡[n1-n2,h] T & T2 ≛[h,o] T. + +definition IH_cnv_cpm_tdeq2_strip_lpr (a) (h) (o): relation3 genv lenv term ≝ + λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] → + ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡[n1,h] T1 → T0 ≛[h,o] T1 → + ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡*[n2,h] T2 → T0 ≛[h,o] T2 → + ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 → + ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[n2-n1,h] T & T1 ≛[h,o] T & ⦃G, L2⦄ ⊢ T2 ➡[n1-n2,h] T & T2 ≛[h,o] T. + +include "ground_2/lib/arith_2b.ma". +include "basic_2/rt_computation/cpms_rdeq.ma". +include "basic_2/rt_computation/cpms_fpbg.ma". + +fact cnv_cpms_tdeq1_strip_lpr_sub (a) (h) (o): + ∀G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_tdeq1_conf_lpr a h o G1 L1 T1) → + ∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_tdeq1_strip_lpr a h o G1 L1 T1. +#a #h #o #G #L #T #IH2 #IH1 #G0 #L0 #T0 #H0 #HT0 #n1 #T1 #H1T01 #H2T01 #n2 #T2 #H @(cpms_ind_dx … H) -n2 -T2 +[ #L1 #H1L01 #H2L01 #L2 #HL02 -IH2 + elim (IH1 … H1T01 H2T01 0 T0 … L1 … L2) // -L0 -IH1 -H2T01 #T3 #HT13 #H1T03 #H2T03 + /3 width=4 by cpm_cpms, ex3_intro/ +| #n #n2 #X2 #T2 #HX2 #IHX2 #HXT2 #L1 #H1L01 #H2L01 #L2 #HL02 -H1T01 -H2T01 + elim (IHX2 L1 … L0) -IHX2 // #X1 #HTX1 #H1X21 #H2X21 + elim (IH1 … H1X21 H2X21 … HXT2 L1 … L2) + [|*: /3 width=12 by cnv_cpms_trans_lpr_sub, fpbg_cpms_trans, cpms_rdeq_conf_sn/ ] -X2 -IH1 -IH2 #X2 #HX12 #H1TX2 #H2TX2 + >arith_l3 @(ex3_intro … H2TX2) /2 width=3 by cpms_step_dx/ (**) (* explict constructor *) +] +qed-. + +(* Sub diamond propery with restricted rt-transition for terms **************) + +fact cnv_cpm_tdeq1_conf_lpr_atom_atom_aux (h) (o) (G) (L1) (L2) (I): + ∃∃T. ⦃G,L1⦄ ⊢ ⓪{I} ➡[0,h] T & ⦃G, L2⦄ ⊢ ⓪{I} ➡[O,h] T & ⓪{I} ≛[h,o] T. +/2 width=4 by ex3_intro/ qed-. + +fact cnv_cpm_tdeq1_conf_lpr_atom_ess_aux (h) (o) (G) (L1) (L2) (s): + ∃∃T. ⦃G,L1⦄ ⊢ ⋆s ➡[1,h] T & ⦃G,L2⦄ ⊢ ⋆(next h s) ➡[h] T & ⋆(next h s) ≛[h,o] T. +/2 width=4 by ex3_intro/ qed-. + +fact cnv_cpm_tdeq1_conf_lpr_ess_atom_aux (h) (o) (G) (L1) (L2) (s): + deg h o s 0 → + ∃∃T. ⦃G,L1⦄ ⊢ ⋆(next h s) ➡[h] T & ⦃G,L2⦄ ⊢⋆s ➡[1,h] T & ⋆s ≛[h,o] T. +/4 width=6 by tdeq_sort, deg_next, ex3_intro/ qed-. + +fact cnv_cpm_tdeq1_conf_lpr_atom_delta_aux (a) (h) (o) (G) (L) (i): + (∀G0,L0,T0. ⦃G,L,#i⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_tdeq1_conf_lpr a h o G0 L0 T0) → + ⦃G,L⦄ ⊢ #i ![a,h] → + ∀K,V. ⬇*[i]L ≘ K.ⓓV → + ∀n,XV. ⦃G,K⦄ ⊢ V ➡[n,h] XV → + ∀X. ⬆*[↑i]XV ≘ X → + ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → L ≛[h,o,#i] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 → + ∃∃T. ⦃G,L1⦄ ⊢ #i ➡[n,h] T & ⦃G,L2⦄ ⊢ X ➡[h] T & X ≛[h,o] T. +#a #h #o #G #L #i #IH #HT #K #V #HLK #n #XV #HVX #X #HXV #L1 #H1L1 #H2L1 #L2 #HL2 +lapply (cnv_lref_fwd_drops … HT … HLK) -HT #HV +elim (lpr_drops_conf … HLK … H1L1) -H1L1 // #Y1 #H1 #HLK1 +elim (lpr_inv_pair_sn … H1) -H1 #K1 #V1 #H1K1 #H1V1 #H destruct +elim (rdeq_inv_lref_pair_bi … H2L1 … HLK … HLK1) -H2L1 #H2K1 #H2V1 #_ +elim (lpr_drops_conf … HLK … HL2) -HL2 // #Y2 #H2 #HLK2 +elim (lpr_inv_pair_sn … H2) -H2 #K2 #V2 #HK2 #_ #H destruct +lapply (drops_isuni_fwd_drop2 … HLK2) -V2 // #HLK2 +lapply (fqup_lref (Ⓣ) … G … HLK) -HLK #HLK +elim (IH … H1V1 H2V1 … HVX … H1K1 H2K1 … HK2) [|*: /2 width=1 by fqup_fpbg/ ] -L -K -V +[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_tdeq1_conf_lpr a h o G0 L0 T0) → + ⦃G,L⦄⊢#i![a,h] → + ∀K,W. ⬇*[i]L ≘ K.ⓛW → + ∀n,XW. ⦃G,K⦄ ⊢ W ➡[n,h] XW → + ∀X. ⬆*[↑i]XW ≘ X → + ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → L ≛[h,o,#i] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 → + ∃∃T. ⦃G,L1⦄ ⊢ #i ➡[↑n,h] T & ⦃G,L2⦄ ⊢ X ➡[h] T & X ≛[h,o] T. +#a #h #o #G #L #i #IH #HT #K #W #HLK #n #XW #HWX #X #HXW #L1 #H1L1 #H2L1 #L2 #HL2 +lapply (cnv_lref_fwd_drops … HT … HLK) -HT #HW +elim (lpr_drops_conf … HLK … H1L1) -H1L1 // #Y1 #H1 #HLK1 +elim (lpr_inv_pair_sn … H1) -H1 #K1 #W1 #H1K1 #H1W1 #H destruct +elim (rdeq_inv_lref_pair_bi … H2L1 … HLK … HLK1) -H2L1 #H2K1 #H2W1 #_ +elim (lpr_drops_conf … HLK … HL2) -HL2 // #Y2 #H2 #HLK2 +elim (lpr_inv_pair_sn … H2) -H2 #K2 #W2 #HK2 #_ #H destruct +lapply (drops_isuni_fwd_drop2 … HLK2) -W2 // #HLK2 +lapply (fqup_lref (Ⓣ) … G … HLK) -HLK #HLK +elim (IH … H1W1 H2W1 … HWX … H1K1 H2K1 … HK2) [|*: /2 width=1 by fqup_fpbg/ ] -L -K -W +[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_tdeq1_conf_lpr a h o G0 L0 T0) → + ⦃G,L⦄ ⊢ ⓑ{p,I}V.T ![a,h] → + ∀V2. ⦃G,L⦄ ⊢ V ➡[h] V2 → + ∀n1,T1. ⦃G,L.ⓑ{I}V⦄ ⊢ T ➡[n1,h] T1 → T ≛[h,o] T1 → + ∀n2,T2. ⦃G,L.ⓑ{I}V⦄ ⊢ T ➡[n2,h] T2 → + ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → L ≛[h,o,ⓑ{p,I}V.T] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 → + ∃∃T. ⦃G,L1⦄ ⊢ ⓑ{p,I}V.T1 ➡[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓑ{p,I}V2.T2 ➡[n1-n2,h] T & ⓑ{p,I}V2.T2 ≛[h,o] T. +#a #h #o #p #I #G0 #L0 #V0 #T0 #IH #H0 +#V2 #HV02 #n1 #T1 #H1T01 #H2T01 #n2 #T2 #HT02 +#L1 #H1L01 #H2L01 #L2 #HL02 +elim (cnv_inv_bind … H0) -H0 #HV0 #HT0 +elim (rdeq_inv_bind … H2L01) -H2L01 #H0L01 #H2L01 +elim (IH … V0 … 0 V0 … HV02 … H1L01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ] +-H0L01 [h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_tdeq1_conf_lpr a h o G0 L0 T0) → + ⦃G,L⦄ ⊢ +ⓓV.T ![a,h] → + ∀n1,T1. ⦃G,L.ⓓV⦄ ⊢ T ➡[n1,h] T1 → T ≛[h,o] T1 → + ∀T2. ⬆*[1]T2 ≘ T → ∀n2,XT2. ⦃G,L⦄ ⊢ T2 ➡[n2,h] XT2 → + ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → L ≛[h,o,+ⓓV.T]L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 → + ∃∃T. ⦃G,L1⦄ ⊢ +ⓓV.T1 ➡[n2-n1,h] T & ⦃G,L2⦄ ⊢ XT2 ➡[n1-n2,h] T & XT2 ≛[h,o] T. +#a #h #o #G0 #L0 #V0 #T0 #IH #H0 +#n1 #T1 #H1T01 #H2T01 #T2 #HT20 #n2 #XT2 #HXT2 +#L1 #H1L01 #H2L01 #L2 #HL02 +elim (cnv_inv_bind … H0) -H0 #_ #HT0 +elim (rdeq_inv_bind … H2L01) -H2L01 #_ #H2L01 +lapply (cnv_inv_lifts … HT0 (Ⓣ) … L0 … HT20) -HT0 +[ /3 width=3 by drops_refl, drops_drop/ ] #HT2 +elim (cpm_inv_lifts_sn … H1T01 (Ⓣ) … L0 … HT20) -H1T01 +[| /3 width=1 by drops_refl, drops_drop/ ] #XT1 #HXT1 #H1XT12 +lapply (tdeq_inv_lifts_bi … H2T01 … HT20 … HXT1) -H2T01 #H2XT12 +lapply (rdeq_inv_lifts_bi … H2L01 (Ⓣ) … L0 L1 … HT20) -H2L01 +[4:|*: /3 width=1 by drops_refl, drops_drop/ ] #H2L01 +elim (IH … H1XT12 H2XT12 … HXT2 … H1L01 … HL02) +[|*: /3 width=1 by fqup_fpbg, fqup_zeta/ ] -L0 -T0 #T #HT1 #H1T2 #H2T2 +/3 width=4 by cpm_zeta, ex3_intro/ +qed-. + +fact cnv_cpm_tdeq1_conf_lpr_appl_appl_aux (a) (h) (o) (G) (L) (V) (T): + (∀G0,L0,T0. ⦃G,L,ⓐV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_tdeq1_conf_lpr a h o G0 L0 T0) → + ⦃G,L⦄ ⊢ ⓐV.T ![a,h] → + ∀V2. ⦃G,L⦄ ⊢ V ➡[h] V2 → + ∀n1,T1. ⦃G,L⦄ ⊢ T ➡[n1,h] T1 → T ≛[h,o] T1 → + ∀n2,T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 → + ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → L ≛[h,o,ⓐV.T] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 → + ∃∃T. ⦃G,L1⦄ ⊢ ⓐV.T1 ➡[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓐV2.T2 ➡[n1-n2,h] T & ⓐV2.T2 ≛[h,o] T. +#a #h #o #G0 #L0 #V0 #T0 #IH #H0 +#V2 #HV02 #n1 #T1 #H1T01 #H2T01 #n2 #T2 #HT02 +#L1 #H1L01 #H2L01 #L2 #HL02 +elim (cnv_inv_appl … H0) -H0 #n0 #p0 #X01 #X02 #_ #HV0 #HT0 #_ #_ -n0 -p0 -X01 -X02 +elim (rdeq_inv_flat … H2L01) -H2L01 #H0L01 #H2L01 +elim (IH … V0 … 0 V0 … HV02 … H1L01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ] +-H0L01 [h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_tdeq1_conf_lpr a h o G0 L0 T0) → + ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.T ![a,h] → + ∀V2. ⦃G,L⦄ ⊢ V ➡[h] V2 → ∀W2. ⦃G,L⦄ ⊢ W ➡[h] W2 → + ∀n1,T1. ⦃G,L⦄ ⊢ ⓛ{p}W.T ➡[n1,h] T1 → ⓛ{p}W.T ≛[h,o] T1 → + ∀n2,T2. ⦃G,L.ⓛW⦄ ⊢ T ➡[n2,h] T2 → + ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → L ≛[h,o,ⓐV.ⓛ{p}W.T] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 → + ∃∃T. ⦃G,L1⦄ ⊢ ⓐV.T1 ➡[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓓ{p}ⓝW2.V2.T2 ➡[n1-n2,h] T & ⓓ{p}ⓝW2.V2.T2 ≛[h,o] T. +#a #h #o #p #G0 #L0 #V0 #W0 #T0 #IH #H0 +#V2 #HV02 #W2 #HW02 #n1 #X #H1X #H2X #n2 #T2 #HT02 +#L1 #H1L01 #H2L01 #L2 #HL02 +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 (cpm_inv_abst1 … H1X) -H1X #W1 #T1 #H1W01 #H1T01 #H destruct +elim (tdeq_inv_pair … H2X) -H2X #_ #H2W01 #H2T01 +elim (rdeq_inv_flat … H2L01) -H2L01 #H0L01 #H2L01 +elim (rdeq_inv_bind … H2L01) -H2L01 #H3L01 #H2L01 +elim (IH … V0 … 0 V0 … HV02 … H1L01 H0L01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ] +-HV0 -HV02 -H0L01 [h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_tdeq1_conf_lpr a h o G0 L0 T0) → + ⦃G,L⦄ ⊢ ⓐV.ⓓ{p}W.T ![a,h] → + ∀V2. ⦃G,L⦄ ⊢ V ➡[h] V2 → ∀W2. ⦃G,L⦄ ⊢ W ➡[h] W2 → + ∀n1,T1. ⦃G,L⦄ ⊢ ⓓ{p}W.T ➡[n1,h] T1 → ⓓ{p}W.T ≛[h,o] T1 → + ∀n2,T2. ⦃G,L.ⓓW⦄ ⊢ T ➡[n2,h] T2 → ∀U2. ⬆*[1]V2 ≘ U2 → + ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → L ≛[h,o,ⓐV.ⓓ{p}W.T] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 → + ∃∃T. ⦃G,L1⦄ ⊢ ⓐV.T1 ➡[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓓ{p}W2.ⓐU2.T2 ➡[n1-n2,h] T & ⓓ{p}W2.ⓐU2.T2 ≛[h,o] T. +#a #h #o #p #G0 #L0 #V0 #W0 #T0 #IH #H0 +#V2 #HV02 #W2 #HW02 #n1 #X #H1X #H2X #n2 #T2 #HT02 #U2 #HVU2 +#L1 #H1L01 #H2L01 #L2 #HL02 +elim (cnv_inv_appl … H0) -H0 #n0 #p0 #X01 #X02 #_ #HV0 #H0 #_ #_ -n0 -p0 -X01 -X02 +elim (cpm_tdeq_inv_bind_sn … H0 … H1X H2X) -H0 -H1X -H2X #T1 #HW0 #HT0 #H1T01 #H2T01 #H destruct +elim (rdeq_inv_flat … H2L01) -H2L01 #H0L01 #H2L01 +elim (rdeq_inv_bind … H2L01) -H2L01 #H3L01 #H2L01 +elim (IH … V0 … 0 V0 … HV02 … H1L01 H0L01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ] +-HV0 -HV02 -H0L01 [h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_tdeq1_conf_lpr a h o G0 L0 T0) → + ⦃G,L⦄ ⊢ ⓝV.T ![a,h] → + ∀n1,V1. ⦃G,L⦄ ⊢ V ➡[n1,h] V1 → V ≛[h,o] V1 → + ∀n2,V2. ⦃G,L⦄ ⊢ V ➡[n2,h] V2 → + ∀T1. ⦃G,L⦄ ⊢ T ➡[n1,h] T1 → T ≛[h,o] T1 → + ∀T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 → + ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → L ≛[h,o,ⓝV.T] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 → + ∃∃T. ⦃G,L1⦄ ⊢ ⓝV1.T1 ➡[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓝV2.T2 ➡[n1-n2,h] T & ⓝV2.T2≛[h,o]T. +#a #h #o #G0 #L0 #V0 #T0 #IH #H0 +#n1 #V1 #H1V01 #H2V01 #n2 #V2 #HV02 #T1 #H1T01 #H2T01 #T2 #HT02 +#L1 #H1L01 #H2L01 #L2 #HL02 +elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #HT0 #_ #_ -X0 +elim (rdeq_inv_flat … H2L01) -H2L01 #H0L01 #H2L01 +elim (IH … H1V01 H2V01 … HV02 … H1L01 H0L01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ] +elim (IH … H1T01 H2T01 … HT02 … H1L01 H2L01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ] +#T #HT1 #H1T2 #H2T2 #V #HV1 #H1V2 #H2V2 -L0 -V0 -T0 +/3 width=6 by cpm_cast, tdeq_pair, ex3_intro/ +qed-. +(* +fact cnv_cpm_tdeq1_conf_lpr_cast_epsilon_aux (a) (h) (o) (G) (L) (V) (T): + (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_tdeq1_conf_lpr a h o G0 L0 T0) → + ⦃G,L⦄ ⊢ ⓝV.T ![a,h] → + ∀n1,V1. ⦃G,L⦄ ⊢ V ➡[n1,h] V1 → V ≛[h,o] V1 → + ∀T1. ⦃G,L⦄ ⊢ T ➡[n1,h] T1 → T ≛[h,o] T1 → + ∀n2,T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 → + ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → L ≛[h,o,ⓝV.T] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 → + ∃∃T. ⦃G,L1⦄ ⊢ ⓝV1.T1 ➡[n2-n1,h] T & ⦃G,L2⦄ ⊢ T2 ➡[n1-n2,h] T & T2 ≛[h,o] T. +#a #h #o #G0 #L0 #V0 #T0 #IH #H0 +#n1 #V1 #HV01 #T1 #HT01 #n2 #T2 #HT02 +#L1 #HL01 #L2 #HL02 +elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #HT0 #_ #_ -X0 +elim (cnv_cpm_conf_lpr_sub … IH … HT01 … HT02 … HL01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ] +#T #HT1 #HT2 -L0 -V0 -T0 +/3 width=3 by cpms_eps, ex2_intro/ +qed-. +*) +fact cnv_cpm_tdeq1_conf_lpr_cast_ee_aux (a) (h) (o) (G) (L) (V) (T): + (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_trans_lpr a h G0 L0 T0) → + (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_tdeq1_conf_lpr a h o G0 L0 T0) → + ⦃G,L⦄ ⊢ ⓝV.T ![a,h] → + ∀n1,V1. ⦃G,L⦄ ⊢ V ➡[n1,h] V1 → V ≛[h,o] V1 → + ∀n2,V2. ⦃G,L⦄ ⊢ V ➡[n2,h] V2 → + ∀T1. ⦃G,L⦄ ⊢ T ➡[n1,h] T1 → T ≛[h,o]T1 → + ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → L ≛[h,o,ⓝV.T]L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 → + ∃∃T. ⦃G,L1⦄ ⊢ ⓝV1.T1 ➡[↑n2-n1,h] T & ⦃G,L2⦄ ⊢ V2 ➡[n1-↑n2,h] T & V2 ≛[h,o] T. +#a #h #o #G0 #L0 #V0 #T0 #IH2 #IH1 #H0 +#n1 #V1 #H1V01 #H2V01 #n2 #V2 #HV02 #T1 #H1T01 #H2T01 +#L1 #H1L01 #H2L01 #L2 #HL02 +(* n2=0 n1=1 *) + -H1V01 -H2V01 +elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #HT0 #HVX0 #HTX0 +elim (rdeq_inv_flat … H2L01) -H2L01 #H0L01 #H2L01 +lapply (cnv_cpms_trans_lpr_sub … IH2 … HVX0 … L0 ?) [4:|*: /2 width=1 by fqup_fpbg/ ] #HX0 +elim (cnv_cpms_strip_lpr_sub … IH1 … HVX0 … HV02 … L0 … HL02) [|*: /2 width=1 by fqup_fpbg/ ] +elim (cnv_cpms_strip_lpr_sub … IH1 … HTX0 … HT01 … L0 … HL01) [|*: /2 width=1 by fqup_fpbg/ ] +-HV02 -HTX0 -HT01 minus_plus #H2 +lapply (cpms_trans … HT1 … HTU) -T [h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_tdeq1_conf_lpr a h o G1 L1 T1) → + ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_cnv_cpm_tdeq1_conf_lpr a h o G1 L1 T1. +#a #h #o #G0 #L0 #T0 #IH2 #IH1 #G #L * [| * [| * ]] +[ #I #HG0 #HL0 #HT0 #HT #n1 #X1 #H1X1 #H2X1 #n2 #X2 #HX2 #L1 #H1L1 #H2L1 #L2 #HL2 destruct + elim (cpm_tdeq_inv_atom_sn … H1X1 H2X1) -H1X1 -H2X1 * + elim (cpm_inv_atom1_drops … HX2) -HX2 * + [ #H21 #H22 #H11 #H12 destruct -a -L + [h,o] ⦃G2, L2, T2⦄. /3 width=5 by cpms_fwd_fpbs, fqup_fpbg,fpbg_fpbs_trans/ qed-. +lemma fpbg_cpms_trans (h) (o) (n): ∀G1,G2,L1,L2,T1,T. ⦃G1, L1, T1⦄ >[h,o] ⦃G2, L2, T⦄ → + ∀T2. ⦃G2, L2⦄ ⊢ T ➡*[n,h] T2 → ⦃G1, L1, T1⦄ >[h,o] ⦃G2, L2, T2⦄. +/3 width=5 by fpbg_fpbs_trans, cpms_fwd_fpbs/ qed-. + lemma cpms_fpbg_trans (h) (o) (n): ∀G1,L1,T1,T. ⦃G1, L1⦄ ⊢ T1 ➡*[n,h] T → ∀G2,L2,T2. ⦃G1, L1, T⦄ >[h,o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h,o] ⦃G2, L2, T2⦄. /3 width=5 by fpbs_fpbg_trans, cpms_fwd_fpbs/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_rdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_rdeq.ma new file mode 100644 index 000000000..b335ae603 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_rdeq.ma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/rt_computation/cpxs_rdeq.ma". +include "basic_2/rt_computation/cpms_cpxs.ma". + +(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************) + +(* Properties with degree-based equivalence for local environments **********) + +lemma cpms_rdeq_conf_sn (h) (n) (o) (G) (L1) (L2): + ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ➡*[n,h] T2 → + L1 ≛[h,o,T1] L2 → L1 ≛[h,o,T2] L2. +/3 width=4 by cpms_fwd_cpxs, cpxs_rdeq_conf_sn/ qed-. + +lemma cpms_rdeq_conf_dx (h) (n) (o) (G) (L1) (L2): + ∀T1,T2. ⦃G, L2⦄ ⊢ T1 ➡*[n,h] T2 → + L1 ≛[h,o,T1] L2 → L1 ≛[h,o,T2] L2. +/3 width=4 by cpms_fwd_cpxs, cpxs_rdeq_conf_dx/ 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 eaee5cf14..336b99505 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_cpm_tdeq" + "cnv_cpm_tdpos" + "cnv_cpms_tdpos" + "cnv_cpms_conf" + "cnv_preserve_sub" + "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_cpm_tdpos" + "cnv_cpms_tdpos" + "cnv_cpms_conf" + "cnv_preserve_sub" + "cnv_preserve" * ] } ] } @@ -61,7 +61,7 @@ table { } ] [ { "t-bound context-sensitive parallel rt-computation" * } { - [ [ "for terms" ] "cpms" + "( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpms_drops" + "cpms_lsubr" + "cpms_aaa" + "cpms_lpr" + "cpms_cpxs" + "cpms_fpbs" + "cpms_fpbg" + "cpms_cpms" * ] + [ [ "for terms" ] "cpms" + "( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpms_drops" + "cpms_lsubr" + "cpms_rdeq" + "cpms_aaa" + "cpms_lpr" + "cpms_cpxs" + "cpms_fpbs" + "cpms_fpbg" + "cpms_cpms" * ] } ] [ { "unbound context-sensitive parallel rst-computation" * } { diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith_2b.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith_2b.ma index 4a1ced644..c6203acd4 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith_2b.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith_2b.ma @@ -32,8 +32,13 @@ elim (le_or_ge (m11+m12) m21) #Hm1121 ] qed. +lemma arith_l3 (m) (n1) (n2): n1+n2-m = n1-m+(n2-(m-n1)). +// qed. + lemma arith_l2 (n1) (n2): ↑n2-n1 = 1-n1+(n2-(n1-1)). -* // qed. +#n1 #n2