From fb4c641d43be3d601104751363782553bea0fb6b Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 1 Sep 2018 13:48:31 +0200 Subject: [PATCH] update in basic_2 and ground_2 + more results on restricted transition + minor additions to the arith library --- .../basic_2/dynamic/cnv_cpm_conf.ma | 50 +++---- .../basic_2/dynamic/cnv_cpm_tdeq.ma | 124 ++++++++++++++---- .../basic_2/dynamic/cnv_cpm_trans.ma | 22 ++-- .../basic_2/dynamic/cnv_cpms_conf.ma | 18 ++- .../basic_2/dynamic/cnv_cpms_tdeq.etc | 52 ++++++++ .../basic_2/dynamic/cnv_preserve_far.ma | 79 ++--------- .../basic_2/dynamic/cnv_preserve_sub.ma | 72 ++++++++++ .../basic_2/rt_computation/cpms_fpbg.ma | 5 + .../basic_2/rt_computation/fpbg_cpxs.ma | 10 +- .../lambdadelta/basic_2/rt_transition/cnx.ma | 2 +- .../lambdadelta/basic_2/rt_transition/cpm.ma | 9 ++ .../basic_2/rt_transition/cpm_tdeq.ma | 26 +++- .../lambdadelta/basic_2/web/basic_2_src.tbl | 2 +- .../lambdadelta/ground_2/lib/arith.ma | 67 ++-------- .../lambdadelta/ground_2/lib/arith_2a.ma | 77 +++++++++++ .../ground_2/notation/xoa/ex_5_1.ma | 26 ++++ .../ground_2/notation/xoa/ex_9_3.ma | 26 ++++ .../lambdadelta/ground_2/web/ground_2_src.tbl | 2 +- .../lambdadelta/ground_2/xoa/ex_5_1.ma | 28 ++++ .../lambdadelta/ground_2/xoa/ex_9_3.ma | 28 ++++ .../lambdadelta/ground_2/xoa2.conf.xml | 2 + .../lambdadelta/ground_2/ynat/ynat_pred.ma | 2 +- 22 files changed, 535 insertions(+), 194 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdeq.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_sub.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/lib/arith_2a.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/xoa/ex_5_1.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/xoa/ex_9_3.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/xoa/ex_5_1.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/xoa/ex_9_3.ma 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 75e1ae220..7a62a9acd 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 @@ -18,11 +18,11 @@ 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_far.ma". +include "basic_2/dynamic/cnv_preserve_sub.ma". (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) -(* Far diamond propery with t-bound rt-transition for terms *****************) +(* Sub diamond propery with t-bound rt-transition for terms *****************) fact cnv_cpm_conf_lpr_atom_atom_aux (h) (G) (L1) (L2) (I): ∃∃T. ⦃G,L1⦄ ⊢ ⓪{I} ➡*[0,h] T & ⦃G, L2⦄ ⊢ ⓪{I} ➡*[O,h] T. @@ -48,7 +48,7 @@ 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 (cnv_cpm_conf_lpr_far … IH … HV1 … HVX … HK1 … HK2) [|*: /2 width=1 by fqup_fpbg/ ] -L -K -V +elim (cnv_cpm_conf_lpr_sub … IH … HV1 … HVX … HK1 … HK2) [|*: /2 width=1 by fqup_fpbg/ ] -L -K -V eq_minus_O // #W0 #H1 #H2 -IH2 -IH1 -L1 -W1 -T1 -U1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_conf.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_conf.ma index ee7c6101b..e6fb158e6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_conf.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_conf.ma @@ -12,12 +12,26 @@ (* *) (**************************************************************************) +include "basic_2/notation/relations/predstar_7.ma". include "basic_2/dynamic/cnv_cpm_trans.ma". include "basic_2/dynamic/cnv_cpm_conf.ma". (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) -(* Far confluence propery with t-bound rt-computation for terms *************) +definition cpsms (n) (h) (o): relation4 genv lenv term term ≝ λG,L,T1,T2. + ∃∃n1,n2,T. T1 ≛[h,o] T → ⊥ & ⦃G, L⦄ ⊢ T1 ➡[n1,h] T & ⦃G, L⦄ ⊢ T ➡*[n2,h] T2 & n1+n2 = n. + +interpretation + "context-sensitive parallel stratified t-bound rt-computarion (term)" + 'PRedStar n h o G L T1 T2 = (cpsms n h o G L T1 T2). + +definition IH_cnv_cpsms_conf_lpr (a) (h) (o): relation3 genv lenv term ≝ + λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] → + ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡*[n1,h,o] T1 → ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡*[n2,h,o] T2 → + ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 → + ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G, L2⦄ ⊢ T2 ➡*[n1-n2,h] T. + +(* Sub confluence propery with t-bound rt-computation for terms *************) fact cnv_cpsms_conf_lpr_aux (a) (h) (o): ∀G0,L0,T0. @@ -33,7 +47,7 @@ lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … HX02 … L0 ?) // #HX2 elim (cnv_cpm_conf_lpr_aux … IH2 IH1 … HX01 … HX02 … L0 … L0) // #Z0 #HXZ10 #HXZ20 cut (⦃G0,L0,T0⦄ >[h,o] ⦃G0,L0,X1⦄) [ /4 width=5 by cpms_fwd_fpbs, cpm_fpb, ex2_3_intro/ ] #H1fpbg (**) (* cut *) lapply (fpbg_fpbs_trans ??? G0 ? L0 ? Z0 ? … H1fpbg) [ /2 width=2 by cpms_fwd_fpbs/ ] #H2fpbg -lapply (cnv_cpms_trans_lpr_far … IH2 … HXZ10 … L0 ?) // #HZ0 +lapply (cnv_cpms_trans_lpr_sub … IH2 … HXZ10 … L0 ?) // #HZ0 elim (IH1 … HXT1 … HXZ10 … L1 … L0) [|*: /4 width=2 by fpb_fpbg, cpm_fpb/ ] -HXT1 -HXZ10 #Z1 #HTZ1 #HZ01 elim (IH1 … HXT2 … HXZ20 … L2 … L0) [|*: /4 width=2 by fpb_fpbg, cpm_fpb/ ] -HXT2 -HXZ20 #Z2 #HTZ2 #HZ02 elim (IH1 … HZ01 … HZ02 L1 … L2) // -L0 -T0 -X1 -X2 -Z0 #Z #HZ01 #HZ02 diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdeq.etc b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdeq.etc new file mode 100644 index 000000000..da155423c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdeq.etc @@ -0,0 +1,52 @@ +(* +axiom cpms_tdneq_fwd_step_sn (n) (h) (o) (G) (L): + ∀T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[n,h] T2 → (T1 ≛[h,o] T2 → ⊥) → + ∃∃n1,n2,T,T0. ⦃G, L⦄ ⊢ T1 ➡[n1,h] T & T1 ≛[h,o] T → ⊥ & ⦃G, L⦄ ⊢ T ➡*[n2,h] T0 & T0 ≛[h,o] T2 & n1+n2 = n. +axiom plus_Sxy_y_false: ∀y,x. ↑(x+y) = y → ⊥. + +lemma cnv_cpm_tdeq_trans (a) (h) (o) (G) (L): + ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → + ∀n,T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛[h,o] T2 → ⦃G,L⦄ ⊢ T2 ![a,h]. +#a #h #o #G #L #T1 @(fqup_wf_ind_eq (Ⓣ) … G L T1) -G -L -T1 +#G0 #L0 #T0 #IH #G #L * [| * [| * ]] +[ #I #_ #_ #_ #H0 #n #X #H1X #H2X -G0 -L0 -T0 + elim (cpm_tdeq_inv_atom_sn … H1X H2X) -H1X -H2X * + [ #H #_ destruct // + | #s #H #_ #_ #_ destruct // + ] +| #p #I #V1 #T1 #HG #HL #HT #H0 #n #X #H1X #H2X destruct + elim (cnv_inv_bind … H0) #HV1 #_ + elim (cpm_tdeq_inv_bind_sn … H0 … H1X H2X) -H0 -H1X -H2X #T2 #H1T #H2T #H3T #H destruct + /3 width=6 by cnv_bind/ +| #V1 #T1 #HG #HL #HT #H0 #n #X #H1X #H2X destruct + elim (cnv_inv_appl … H0) #m #p #W1 #U1 #Hm #HV1 #_ #HVW1 #HTU1 + elim (cpm_tdeq_inv_appl_sn … H0 … H1X H2X) -H0 -H1X -H2X #T2 #H1T #H2T #H3T #H destruct + @(cnv_appl … Hm … HVW1) + +(* Properties with restricted rt-transition for terms ***********************) + +lemma pippo (a) (h) (o) (G) (L): + ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → + ∀n1,T. ⦃G,L⦄ ⊢ T1 ➡[n1,h] T → T1 ≛[h,o] T → + ∀n2,T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 → + ∃∃T0. ⦃G,L⦄ ⊢ T1 ➡[n2,h] T0 & ⦃G,L⦄ ⊢ T0 ➡[n1,h] T2 & T0 ≛[h,o] T2. +#a #h #o #G #L #T1 @(fqup_wf_ind_eq (Ⓣ) … G L T1) -G -L -T1 +#G0 #L0 #T0 #IH #G #L * [| * [| * ]] +[ #I #_ #_ #_ #_ #n1 #X1 #H1X #H2X #n2 #X2 #HX2 -G0 -L0 -T0 + elim (cpm_tdeq_inv_atom_sn … H1X H2X) -H1X -H2X * + [ #H1 #H2 destruct /2 width=4 by ex3_intro/ + | #s #H1 #H2 #H3 #Hs destruct + elim (cpm_inv_sort1 … HX2) -HX2 #H #Hn2 destruct >iter_n_Sm + /5 width=6 by cpm_sort_iter, tdeq_sort, deg_iter, deg_next, ex3_intro/ + ] +| #p #I #V1 #T1 #HG #HL #HT #H0 #n1 #X1 #H1X #H2X #n2 #X2 #HX2 destruct + elim (cpm_tdeq_inv_bind_sn … H0 … H1X H2X) -H0 -H1X -H2X #T #H1T1 #H2T1 #H3T1 #H destruct + elim (cpm_inv_bind1 … HX2) -HX2 * + [ #V2 #T2 #HV12 #HT2 #H destruct + elim (IH … H1T1 … H2T1 H3T1 … HT2) -IH -H1T1 -H2T1 -H3T1 -HT2 [2: // ] #T0 #HT10 #H1T02 #H2T02 + @(ex3_intro … (ⓑ{p,I}V2.T0)) + [ /2 width=1 by cpm_bind/ + | + | /2 width=1 by tdeq_pair/ + +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_far.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_far.ma index 971541b21..7ab0ff8a2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_far.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_far.ma @@ -12,75 +12,22 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/predstar_7.ma". -include "basic_2/rt_computation/fpbg.ma". -include "basic_2/rt_computation/cpms_fpbs.ma". -include "basic_2/dynamic/cnv.ma". +include "basic_2/dynamic/cnv_cpm_trans.ma". (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) -(* Inductive premises for the preservation results **************************) +(* Far properties for preservation ******************************************) -definition cpsms (n) (h) (o): relation4 genv lenv term term ≝ λG,L,T1,T2. - ∃∃n1,n2,T. T1 ≛[h,o] T → ⊥ & ⦃G, L⦄ ⊢ T1 ➡[n1,h] T & ⦃G, L⦄ ⊢ T ➡*[n2,h] T2 & n1+n2 = n. - -interpretation - "context-sensitive parallel stratified t-bound rt-computarion (term)" - 'PRedStar n h o G L T1 T2 = (cpsms n h o G L T1 T2). - -definition IH_cnv_cpm_trans_lpr (a) (h): relation3 genv lenv term ≝ - λG,L1,T1. ⦃G, L1⦄ ⊢ T1 ![a,h] → - ∀n,T2. ⦃G, L1⦄ ⊢ T1 ➡[n,h] T2 → - ∀L2. ⦃G, L1⦄ ⊢ ➡[h] L2 → ⦃G, L2⦄ ⊢ T2 ![a,h]. - -definition IH_cnv_cpms_trans_lpr (a) (h): relation3 genv lenv term ≝ - λG,L1,T1. ⦃G, L1⦄ ⊢ T1 ![a,h] → - ∀n,T2. ⦃G, L1⦄ ⊢ T1 ➡*[n,h] T2 → - ∀L2. ⦃G, L1⦄ ⊢ ➡[h] L2 → ⦃G, L2⦄ ⊢ T2 ![a,h]. - -definition IH_cnv_cpm_conf_lpr (a) (h): relation3 genv lenv term ≝ - λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] → - ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡[n1,h] T1 → ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡[n2,h] T2 → - ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 → - ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G, L2⦄ ⊢ T2 ➡*[n1-n2,h] T. - -definition IH_cnv_cpms_strip_lpr (a) (h): relation3 genv lenv term ≝ - λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] → - ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡*[n1,h] T1 → ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡[n2,h] T2 → - ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 → - ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G, L2⦄ ⊢ T2 ➡*[n1-n2,h] T. - -definition IH_cnv_cpms_conf_lpr (a) (h): relation3 genv lenv term ≝ - λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] → - ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡*[n1,h] T1 → ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡*[n2,h] T2 → - ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 → - ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G, L2⦄ ⊢ T2 ➡*[n1-n2,h] T. - -definition IH_cnv_cpsms_conf_lpr (a) (h) (o): relation3 genv lenv term ≝ - λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] → - ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡*[n1,h,o] T1 → ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡*[n2,h,o] T2 → - ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 → - ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G, L2⦄ ⊢ T2 ➡*[n1-n2,h] T. - -(* Properties for preservation **********************************************) - -lemma cnv_cpms_trans_lpr_far (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_cpms_trans_lpr a h G1 L1 T1. -#a #h #o #G0 #L0 #T0 #IH #G1 #L1 #T1 #H01 #HT1 #n #T2 #H +fact cnv_cpms_trans_lpr_far (a) (h) (o): + ∀G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) → + (∀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 = G1 → L0 = L1 → T0 = T1 → IH_cnv_cpms_trans_lpr a h G1 L1 T1. +#a #h #o #G0 #L0 #T0 #IH2 #IH1 #G1 #L1 #T1 #HG #HL #HT #H0 #n #T2 #H destruct @(cpms_ind_dx … H) -n -T2 -/4 width=7 by cpms_fwd_fpbs, fpbg_fpbs_trans/ +[ #L2 #HL12 @(cnv_cpm_trans_lpr_aux … IH2 IH1 … H0 … 0 T1 … HL12) -L2 -IH2 -IH1 -H0 // +| #n2 #n2 #T #T2 #HT1 #IH #HT2 #L2 #HL12 destruct + @(cnv_cpm_trans_lpr_aux … o … HT2 … HL12) [1,2,3,6,7,8,9: /2 width=2 by/ ] -n2 -L2 -T2 -IH + /3 width=4 by cpms_fpbg_trans/ +] qed-. - -lemma cnv_cpm_conf_lpr_far (a) (h) (o): - ∀G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) → - ∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_conf_lpr a h G1 L1 T1. -/3 width=8 by cpm_cpms/ qed-. - -lemma cnv_cpms_strip_lpr_far (a) (h) (o): - ∀G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) → - ∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_strip_lpr a h G1 L1 T1. -/3 width=8 by cpm_cpms/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_sub.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_sub.ma new file mode 100644 index 000000000..f86bc1b59 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_sub.ma @@ -0,0 +1,72 @@ +(**************************************************************************) +(* ___ *) +(* ||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/fpbg.ma". +include "basic_2/rt_computation/cpms_fpbs.ma". +include "basic_2/dynamic/cnv.ma". + +(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) + +(* Inductive premises for the preservation results **************************) + +definition IH_cnv_cpm_trans_lpr (a) (h): relation3 genv lenv term ≝ + λG,L1,T1. ⦃G, L1⦄ ⊢ T1 ![a,h] → + ∀n,T2. ⦃G, L1⦄ ⊢ T1 ➡[n,h] T2 → + ∀L2. ⦃G, L1⦄ ⊢ ➡[h] L2 → ⦃G, L2⦄ ⊢ T2 ![a,h]. + +definition IH_cnv_cpms_trans_lpr (a) (h): relation3 genv lenv term ≝ + λG,L1,T1. ⦃G, L1⦄ ⊢ T1 ![a,h] → + ∀n,T2. ⦃G, L1⦄ ⊢ T1 ➡*[n,h] T2 → + ∀L2. ⦃G, L1⦄ ⊢ ➡[h] L2 → ⦃G, L2⦄ ⊢ T2 ![a,h]. + +definition IH_cnv_cpm_conf_lpr (a) (h): relation3 genv lenv term ≝ + λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] → + ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡[n1,h] T1 → ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡[n2,h] T2 → + ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 → + ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G, L2⦄ ⊢ T2 ➡*[n1-n2,h] T. + +definition IH_cnv_cpms_strip_lpr (a) (h): relation3 genv lenv term ≝ + λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] → + ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡*[n1,h] T1 → ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡[n2,h] T2 → + ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 → + ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G, L2⦄ ⊢ T2 ➡*[n1-n2,h] T. + +definition IH_cnv_cpms_conf_lpr (a) (h): relation3 genv lenv term ≝ + λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] → + ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡*[n1,h] T1 → ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡*[n2,h] T2 → + ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 → + ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G, L2⦄ ⊢ T2 ➡*[n1-n2,h] T. + +(* Auxiliary properties for preservation ************************************) + +fact cnv_cpms_trans_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_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/ +qed-. + +fact cnv_cpm_conf_lpr_sub (a) (h) (o): + ∀G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) → + ∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_conf_lpr a h G1 L1 T1. +/3 width=8 by cpm_cpms/ qed-. + +fact cnv_cpms_strip_lpr_sub (a) (h) (o): + ∀G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) → + ∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_strip_lpr a h G1 L1 T1. +/3 width=8 by cpm_cpms/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_fpbg.ma index e5a6ca6b7..7e40bcc6c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_fpbg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_fpbg.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "basic_2/rt_computation/fpbg_fqup.ma". +include "basic_2/rt_computation/fpbg_fpbs.ma". include "basic_2/rt_computation/cpms_fpbs.ma". (* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************) @@ -22,3 +23,7 @@ include "basic_2/rt_computation/cpms_fpbs.ma". lemma fqup_cpms_fwd_fpbg (h) (o): ∀G1,G2,L1,L2,T1,T. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T⦄ → ∀n,T2. ⦃G2, L2⦄ ⊢ T ➡*[n,h] T2 → ⦃G1, L1, T1⦄ >[h,o] ⦃G2, L2, T2⦄. /3 width=5 by cpms_fwd_fpbs, fqup_fpbg,fpbg_fpbs_trans/ 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/fpbg_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_cpxs.ma index 960979cac..e70619a8d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_cpxs.ma @@ -14,16 +14,20 @@ include "basic_2/rt_computation/cpxs_tdeq.ma". include "basic_2/rt_computation/fpbs_cpxs.ma". -include "basic_2/rt_computation/fpbg.ma". +include "basic_2/rt_computation/fpbg_fpbs.ma". (* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************) (* Properties with unbound context-sensitive parallel rt-computation ********) (* Basic_2A1: was: cpxs_fpbg *) -lemma cpxs_tdneq_fpbg: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → - (T1 ≛[h, o] T2 → ⊥) → ⦃G, L, T1⦄ >[h, o] ⦃G, L, T2⦄. +lemma cpxs_tdneq_fpbg (h) (o): ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → + (T1 ≛[h, o] T2 → ⊥) → ⦃G, L, T1⦄ >[h, o] ⦃G, L, T2⦄. #h #o #G #L #T1 #T2 #H #H0 elim (cpxs_tdneq_fwd_step_sn … H … H0) -H -H0 /4 width=5 by cpxs_tdeq_fpbs, fpb_cpx, ex2_3_intro/ qed. + +lemma cpxs_fpbg_trans (h) (o): ∀G1,L1,T1,T. ⦃G1, L1⦄ ⊢ T1 ⬈*[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, cpxs_fpbs/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx.ma index 13e746d7f..cc2397d0f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx.ma @@ -33,7 +33,7 @@ lapply (H (⋆(next h s)) ?) -H /2 width=2 by cpx_ess/ -G -L #H elim (tdeq_inv_sort1 … H) -H #s0 #d #H1 #H2 #H destruct lapply (deg_next … H1) #H0 lapply (deg_mono … H0 … H2) -H0 -H2 #H -<(pred_inv_refl … H) -H // +>(pred_inv_fix_sn … H) -H // qed-. lemma cnx_inv_abst: ∀h,o,p,G,L,V,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃ⓛ{p}V.T⦄ → diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma index a8202b637..4ab5cff51 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma @@ -119,6 +119,15 @@ qed. lemma cpr_refl: ∀h,G,L. reflexive … (cpm h G L 0). /3 width=3 by cpg_refl, ex2_intro/ qed. +(* Advanced properties ******************************************************) + +lemma cpm_sort_iter (h) (G) (L): + ∀n. n ≤ 1 → + ∀s. ⦃G,L⦄ ⊢ ⋆s ➡ [n,h] ⋆((next h)^n s). +#h #G #L * // +#n #H #s <(le_n_O_to_eq n) /2 width=1 by le_S_S_to_le/ +qed. + (* Basic inversion lemmas ***************************************************) lemma cpm_inv_atom1: ∀n,h,J,G,L,T2. ⦃G, L⦄ ⊢ ⓪{J} ➡[n, h] T2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_tdeq.ma index 0b15ef813..ed7d341d4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_tdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_tdeq.ma @@ -19,12 +19,32 @@ include "basic_2/rt_transition/cpm_drops.ma". (* Inversion lemmas with degree-based equivalence for terms *****************) -lemma cpm_tdeq_inv_lref (n) (h) (o) (G) (L) (i): - ∀X. ⦃G, L⦄ ⊢ #i ➡[n,h] X → #i ≛[h,o] X → - ∧∧ X = #i & n = 0. +lemma cpm_tdeq_inv_lref_sn (n) (h) (o) (G) (L) (i): + ∀X. ⦃G,L⦄ ⊢ #i ➡[n,h] X → #i ≛[h,o] X → + ∧∧ X = #i & n = 0. #n #h #o #G #L #i #X #H1 #H2 lapply (tdeq_inv_lref1 … H2) -H2 #H destruct elim (cpm_inv_lref1_drops … H1) -H1 // * [| #m ] #K #V1 #V2 #_ #_ #H -V1 elim (lifts_inv_lref2_uni_lt … H) -H // qed-. + +lemma cpm_tdeq_inv_atom_sn (n) (h) (o) (I) (G) (L): + ∀X. ⦃G,L⦄ ⊢ ⓪{I} ➡[n,h] X → ⓪{I} ≛[h,o] X → + ∨∨ ∧∧ X = ⓪{I} & n = 0 + | ∃∃s. X = ⋆(next h s) & I = Sort s & n = 1 & deg h o s 0. +#n #h #o * #s #G #L #X #H1 #H2 +[ elim (cpm_inv_sort1 … H1) -H1 + cases n -n [| #n ] #H #Hn destruct + [ /3 width=1 by or_introl, conj/ + | elim (tdeq_inv_sort1 … H2) -H2 #x #d #Hs + <(le_n_O_to_eq n) [| /2 width=3 by le_S_S_to_le/ ] -n #Hx #H destruct + lapply (deg_next … Hs) #H + lapply (deg_mono … H Hx) -H -Hx #Hd + lapply (pred_inv_fix_sn … Hd) -Hd #H destruct + /3 width=4 by refl, ex4_intro, or_intror/ + ] +| elim (cpm_tdeq_inv_lref_sn … H1 H2) -H1 -H2 /3 width=1 by or_introl, conj/ +| elim (cpm_inv_gref1 … H1) -H1 -H2 /3 width=1 by or_introl, conj/ +] +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 45e8c1318..a805b584e 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_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_sub" + "cnv_preserve_far" (* + "cnv_preserve" *) * ] } ] } diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma index 24d1d47fb..a29899d45 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma @@ -49,7 +49,7 @@ lemma max_SS: ∀n1,n2. ↑(n1∨n2) = (↑n1 ∨ ↑n2). [ >(le_to_leb_true … H) | >(not_le_to_leb_false … H) ] -H // qed. -(* Equations ****************************************************************) +(* Equalities ***************************************************************) lemma plus_SO: ∀n. n + 1 = ↑n. // qed. @@ -57,8 +57,11 @@ lemma plus_SO: ∀n. n + 1 = ↑n. lemma minus_plus_m_m_commutative: ∀n,m:nat. n = m + n - m. // qed-. -lemma plus_n_2: ∀n. n + 2 = n + 1 + 1. -// qed. +lemma plus_to_minus_2: ∀m1,m2,n1,n2. n1 ≤ m1 → n2 ≤ m2 → + m1+n2 = m2+n1 → m1-n1 = m2-n2. +#m1 #m2 #n1 #n2 #H1 #H2 #H +@plus_to_minus >plus_minus_associative // +qed-. (* Note: uses minus_minus_comm, minus_plus_m_m, commutative_plus, plus_minus *) lemma plus_minus_minus_be: ∀x,y,z. y ≤ z → z ≤ x → (x - z) + (z - y) = x - y. @@ -81,29 +84,6 @@ lemma le_plus_minus_comm: ∀n,m,p. p ≤ m → m + n - p = m - p + n. lemma minus_minus_comm3: ∀n,x,y,z. n-x-y-z = n-y-z-x. // qed. -lemma arith_b1: ∀a,b,c1. c1 ≤ b → a - c1 - (b - c1) = a - b. -#a #b #c1 #H >minus_minus_comm >minus_le_minus_minus_comm // -qed-. - -lemma arith_b2: ∀a,b,c1,c2. c1 + c2 ≤ b → a - c1 - c2 - (b - c1 - c2) = a - b. -#a #b #c1 #c2 #H >minus_plus >minus_plus >minus_plus /2 width=1 by arith_b1/ -qed-. - -lemma arith_c1x: ∀x,a,b,c1. x + c1 + a - (b + c1) = x + a - b. -/3 by monotonic_le_minus_l, le_to_le_to_eq, le_n/ qed. - -lemma arith_h1: ∀a1,a2,b,c1. c1 ≤ a1 → c1 ≤ b → - a1 - c1 + a2 - (b - c1) = a1 + a2 - b. -#a1 #a2 #b #c1 #H1 #H2 >plus_minus /2 width=1 by arith_b2/ -qed-. - -lemma arith_i: ∀x,y,z. y < x → x+z-y-1 = x-y-1+z. -/2 width=1 by plus_minus/ qed-. - -lemma plus_to_minus_2: ∀m1,m2,n1,n2. n1 ≤ m1 → n2 ≤ m2 → - m1+n2 = m2+n1 → m1-n1 = m2-n2. -/2 width=1 by arith_b1/ qed-. - lemma idempotent_max: ∀n:nat. n = (n ∨ n). #n normalize >le_to_leb_true // qed. @@ -134,12 +114,6 @@ lemma lt_or_eq_or_gt: ∀m,n. ∨∨ m < n | n = m | n < m. #m #Hm * /3 width=1 by not_le_to_lt, le_S_S, or3_intro2/ qed-. -fact le_repl_sn_conf_aux: ∀x,y,z:nat. x ≤ z → x = y → y ≤ z. -// qed-. - -fact le_repl_sn_trans_aux: ∀x,y,z:nat. x ≤ z → y = x → y ≤ z. -// qed-. - lemma monotonic_le_minus_l2: ∀x1,x2,y,z. x1 ≤ x2 → x1 - y - z ≤ x2 - y - z. /3 width=1 by monotonic_le_minus_l/ qed. @@ -171,23 +145,6 @@ lemma max_S1_le_S: ∀n1,n2,n. (n1 ∨ n2) ≤ n → (↑n1 ∨ n2) ≤ ↑n. lemma max_S2_le_S: ∀n1,n2,n. (n1 ∨ n2) ≤ n → (n1 ∨ ↑n2) ≤ ↑n. /2 width=1 by max_S1_le_S/ qed-. -lemma arith_j: ∀x,y,z. x-y-1 ≤ x-(y-z)-1. -/3 width=1 by monotonic_le_minus_l, monotonic_le_minus_r/ qed. - -lemma arith_k_sn: ∀z,x,y,n. z < x → x+n ≤ y → x-z-1+n ≤ y-z-1. -#z #x #y #n #Hzx #Hxny ->plus_minus [2: /2 width=1 by monotonic_le_minus_r/ ] ->plus_minus [2: /2 width=1 by lt_to_le/ ] -/2 width=1 by monotonic_le_minus_l2/ -qed. - -lemma arith_k_dx: ∀z,x,y,n. z < x → y ≤ x+n → y-z-1 ≤ x-z-1+n. -#z #x #y #n #Hzx #Hyxn ->plus_minus [2: /2 width=1 by monotonic_le_minus_r/ ] ->plus_minus [2: /2 width=1 by lt_to_le/ ] -/2 width=1 by monotonic_le_minus_l2/ -qed. - (* Inversion & forward lemmas ***********************************************) lemma lt_refl_false: ∀n. n < n → ⊥. @@ -220,8 +177,9 @@ lemma plus_xySz_x_false: ∀z,x,y. x + y + S z = x → ⊥. lemma plus_xSy_x_false: ∀y,x. x + S y = x → ⊥. /2 width=4 by plus_xySz_x_false/ qed-. -lemma pred_inv_refl: ∀m. pred m = m → m = 0. -* // normalize #m #H elim (lt_refl_false m) // +lemma pred_inv_fix_sn: ∀x. ↓x = x → 0 = x. +* // #x H -H @@ -333,10 +288,6 @@ lemma iter_O: ∀B:Type[0]. ∀f:B→B.∀b. f^0 b = b. lemma iter_S: ∀B:Type[0]. ∀f:B→B.∀b,l. f^(S l) b = f (f^l b). // qed. -lemma iter_SO: ∀B:Type[0]. ∀f:B→B. ∀b,l. f^(l+1) b = f (f^l b). -#B #f #b #l >commutative_plus // -qed. - lemma iter_n_Sm: ∀B:Type[0]. ∀f:B→B. ∀b,l. f^l (f b) = f (f^l b). #B #f #b #l elim l -l normalize // qed. diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith_2a.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith_2a.ma new file mode 100644 index 000000000..c49b13b87 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith_2a.ma @@ -0,0 +1,77 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "ground_2/lib/arith.ma". + +(* ARITHMETICAL PROPERTIES FOR λδ-2B ****************************************) + +(* Equalities ***************************************************************) + +lemma plus_n_2: ∀n. n + 2 = n + 1 + 1. +// qed. + +lemma arith_b1: ∀a,b,c1. c1 ≤ b → a - c1 - (b - c1) = a - b. +#a #b #c1 #H >minus_minus_comm >minus_le_minus_minus_comm // +qed-. + +lemma arith_b2: ∀a,b,c1,c2. c1 + c2 ≤ b → a - c1 - c2 - (b - c1 - c2) = a - b. +#a #b #c1 #c2 #H >minus_plus >minus_plus >minus_plus /2 width=1 by arith_b1/ +qed-. + +lemma arith_c1x: ∀x,a,b,c1. x + c1 + a - (b + c1) = x + a - b. +/3 by monotonic_le_minus_l, le_to_le_to_eq, le_n/ qed. + +lemma arith_h1: ∀a1,a2,b,c1. c1 ≤ a1 → c1 ≤ b → + a1 - c1 + a2 - (b - c1) = a1 + a2 - b. +#a1 #a2 #b #c1 #H1 #H2 >plus_minus /2 width=1 by arith_b2/ +qed-. + +lemma arith_i: ∀x,y,z. y < x → x+z-y-1 = x-y-1+z. +/2 width=1 by plus_minus/ qed-. + +(* Properties ***************************************************************) + +fact le_repl_sn_conf_aux: ∀x,y,z:nat. x ≤ z → x = y → y ≤ z. +// qed-. + +fact le_repl_sn_trans_aux: ∀x,y,z:nat. x ≤ z → y = x → y ≤ z. +// qed-. + +lemma arith_j: ∀x,y,z. x-y-1 ≤ x-(y-z)-1. +/3 width=1 by monotonic_le_minus_l, monotonic_le_minus_r/ qed. + +lemma arith_k_sn: ∀z,x,y,n. z < x → x+n ≤ y → x-z-1+n ≤ y-z-1. +#z #x #y #n #Hzx #Hxny +>plus_minus [2: /2 width=1 by monotonic_le_minus_r/ ] +>plus_minus [2: /2 width=1 by lt_to_le/ ] +/2 width=1 by monotonic_le_minus_l2/ +qed. + +lemma arith_k_dx: ∀z,x,y,n. z < x → y ≤ x+n → y-z-1 ≤ x-z-1+n. +#z #x #y #n #Hzx #Hyxn +>plus_minus [2: /2 width=1 by monotonic_le_minus_r/ ] +>plus_minus [2: /2 width=1 by lt_to_le/ ] +/2 width=1 by monotonic_le_minus_l2/ +qed. + +(* Inversion & forward lemmas ***********************************************) + +lemma lt_plus_SO_to_le: ∀x,y. x < y + 1 → x ≤ y. +/2 width=1 by monotonic_pred/ qed-. + +(* Iterators ****************************************************************) + +lemma iter_SO: ∀B:Type[0]. ∀f:B→B. ∀b,l. f^(l+1) b = f (f^l b). +#B #f #b #l >commutative_plus // +qed. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/ex_5_1.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/ex_5_1.ma new file mode 100644 index 000000000..a31168095 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/ex_5_1.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +(* multiple existental quantifier (5, 1) *) + +notation > "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.$P0) (λ${ident x0}.$P1) (λ${ident x0}.$P2) (λ${ident x0}.$P3) (λ${ident x0}.$P4) }. + +notation < "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.$P0) (λ${ident x0}:$T0.$P1) (λ${ident x0}:$T0.$P2) (λ${ident x0}:$T0.$P3) (λ${ident x0}:$T0.$P4) }. + diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/ex_9_3.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/ex_9_3.ma new file mode 100644 index 000000000..609f6974d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/ex_9_3.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +(* multiple existental quantifier (9, 3) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7 break & term 19 P8)" + non associative with precedence 20 + for @{ 'Ex3 (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P6) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P7) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P8) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7 break & term 19 P8)" + non associative with precedence 20 + for @{ 'Ex3 (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P6) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P7) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P8) }. + diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl index 33ace356b..501d4f30f 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl @@ -59,7 +59,7 @@ table { [ { "" * } { [ "stream ( ? ⨮{?} ? )" "stream_eq ( ? ≗{?} ? )" "stream_hdtl ( ⫰{?}? )" "stream_tls ( ⫰*{?}[?]? )" * ] [ "list ( Ⓔ{?} ) ( ? ⨮{?} ? )" "list_length ( |?| )" * ] - [ "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? ) ( ↑? ) ( ↓? ) ( ? ∨ ? ) ( ? ∧ ? )" "arith_2b" * ] + [ "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? ) ( ↑? ) ( ↓? ) ( ? ∨ ? ) ( ? ∧ ? )" "arith_2a" "arith_2b" * ] [ "ltc" "ltc_ctc" * ] [ "logic ( ⊥ ) ( ⊤ )" "relations ( ? ⊆ ? )" "functions" "exteq ( ? ≐{?,?} ? )" "star" * ] } diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa/ex_5_1.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa/ex_5_1.ma new file mode 100644 index 000000000..e137f98f8 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa/ex_5_1.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +include "basics/pts.ma". + +include "ground_2/notation/xoa/ex_5_1.ma". + +(* multiple existental quantifier (5, 1) *) + +inductive ex5 (A0:Type[0]) (P0,P1,P2,P3,P4:A0→Prop) : Prop ≝ + | ex5_intro: ∀x0. P0 x0 → P1 x0 → P2 x0 → P3 x0 → P4 x0 → ex5 ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (5, 1)" 'Ex P0 P1 P2 P3 P4 = (ex5 ? P0 P1 P2 P3 P4). + diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa/ex_9_3.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa/ex_9_3.ma new file mode 100644 index 000000000..fd300b4cc --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa/ex_9_3.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +include "basics/pts.ma". + +include "ground_2/notation/xoa/ex_9_3.ma". + +(* multiple existental quantifier (9, 3) *) + +inductive ex9_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3,P4,P5,P6,P7,P8:A0→A1→A2→Prop) : Prop ≝ + | ex9_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → P3 x0 x1 x2 → P4 x0 x1 x2 → P5 x0 x1 x2 → P6 x0 x1 x2 → P7 x0 x1 x2 → P8 x0 x1 x2 → ex9_3 ? ? ? ? ? ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (9, 3)" 'Ex3 P0 P1 P2 P3 P4 P5 P6 P7 P8 = (ex9_3 ? ? ? P0 P1 P2 P3 P4 P5 P6 P7 P8). + diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa2.conf.xml b/matita/matita/contribs/lambdadelta/ground_2/xoa2.conf.xml index 8adc7626b..d40726d02 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa2.conf.xml +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa2.conf.xml @@ -5,6 +5,8 @@ ground_2/xoa ground_2/notation/xoa basics/pts.ma + 5 1 5 7 + 9 3 diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma index b49dbda04..b64e38877 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma @@ -37,5 +37,5 @@ lemma ypred_Y: (↓∞) = ∞. lemma ypred_inv_refl: ∀m:ynat. ↓m = m → m = 0 ∨ m = ∞. * // #m #H lapply (yinj_inj … H) -H (**) (* destruct lemma needed *) -/4 width=1 by pred_inv_refl, or_introl, eq_f/ +/4 width=1 by pred_inv_fix_sn, or_introl, eq_f/ qed-. -- 2.39.2