From 6c86c70b005e3f3efd375868b27f3cff84febfad Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 13 Nov 2012 20:50:33 +0000 Subject: [PATCH] - one axiom removed from sd - traces added to auto to make it work - bugfix in Makefile - more notation and existentials for staff to be committed - some minor additions --- matita/matita/contribs/lambda_delta/Makefile | 4 +-- .../lambda_delta/basic_2/computation/xprs.ma | 1 + .../basic_2/computation/xprs_lsubss.ma | 27 +++++++++++++++++ .../lambda_delta/basic_2/dynamic/snv_ssta.ma | 29 +++++-------------- .../lambda_delta/basic_2/grammar/cl_weight.ma | 17 +++++++---- .../contribs/lambda_delta/basic_2/notation.ma | 8 ++--- .../basic_2/reducibility/xpr_lsubss.ma | 28 ++++++++++++++++++ .../lambda_delta/basic_2/static/sd.ma | 18 +++++++----- .../lambda_delta/basic_2/unfold/frsups.ma | 1 - .../lambda_delta/basic_2/unfold/ltpss_dx.ma | 3 +- .../lambda_delta/ground_2/xoa.conf.xml | 1 + .../contribs/lambda_delta/ground_2/xoa.ma | 8 +++++ .../lambda_delta/ground_2/xoa_notation.ma | 10 +++++++ 13 files changed, 112 insertions(+), 43 deletions(-) create mode 100644 matita/matita/contribs/lambda_delta/basic_2/computation/xprs_lsubss.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_lsubss.ma diff --git a/matita/matita/contribs/lambda_delta/Makefile b/matita/matita/contribs/lambda_delta/Makefile index 7d2fee6bf..3e696b6b6 100644 --- a/matita/matita/contribs/lambda_delta/Makefile +++ b/matita/matita/contribs/lambda_delta/Makefile @@ -19,7 +19,7 @@ all: # xoa ######################################################################## -xoa: $(TARGETS) +xoa: $(XOA_TARGETS) $(XOA_TARGETS): $(XOA_CONF) @echo " EXEC $(XOA) $(XOA_CONF)" @@ -106,7 +106,7 @@ define SUMMARY_TEMPLATE @printf ' ]\n' >> $$@ @printf ' class "cyan" [ "sizes"\n' >> $$@ @printf ' [ "files" "$$(V1)" ]\n' >> $$@ - @printf ' [ "bytes" "$$(V2)" ]\n' >> $$@ + @printf ' [ "characters" "$$(V2)" ]\n' >> $$@ @printf ' [ * ]\n' >> $$@ @printf ' ]\n' >> $$@ @printf ' class "green" [ "propositions"\n' >> $$@ diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/xprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs.ma index 34e93db9d..854c5da27 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/xprs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "basic_2/static/lsubss.ma". include "basic_2/reducibility/xpr.ma". (* include "basic_2/reducibility/cnf.ma". diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_lsubss.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_lsubss.ma new file mode 100644 index 000000000..c883c14f3 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_lsubss.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reducibility/xpr_lsubss.ma". +include "basic_2/computation/xprs.ma". + +(* EXTENDED PARALLEL COMPUTATION ON TERMS ***********************************) + +(* Properties on lenv ref for stratified type assignment ********************) + +lemma lsubss_xprs_trans: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → + ∀T1,T2. ⦃h, L2⦄ ⊢ T1 •➡*[g] T2 → ⦃h, L1⦄ ⊢ T1 •➡*[g] T2. +#h #g #L1 #L2 #HL12 #T1 #T2 #H @(xprs_ind … H) -T2 // +#T #T2 #_ #HT2 #IHT1 +lapply (lsubss_xpr_trans … HL12 … HT2) -L2 /2 width=3/ +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_ssta.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_ssta.ma index a934ca08e..bd6b2121d 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_ssta.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_ssta.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "basic_2/static/ssta.ma". include "basic_2/dynamic/snv.ma". (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) @@ -31,23 +30,16 @@ lemma snv_ssta: ∀h,g,L,T. ⦃h, L⦄ ⊩ T :[g] → ∃∃U,l. ⦃h, L⦄ ⊢ | #L #W #T #U #l #_ #_ #HTU #_ #_ #_ /3 width=3/ (**) (* auto fails without the last #_ *) ] qed-. -(* + fact snv_ssta_conf_aux: ∀h,g,L,T. ( - ∀L0,T1,U1,l1. ⦃h, L0⦄ ⊢ T1 •[g, l1] U1 → - ∀T2,U2,l2. ⦃h, L0⦄ ⊢ T2 •[g, l2] U2 → - L0 ⊢ T1 ⬌* T2 → ⦃h, L0⦄ ⊩ T1 :[g] → ⦃h, L0⦄ ⊩ T2 :[g] → - #{L0, T1} < #{L ,T} → - l1 = l2 ∧ L0 ⊢ U1 ⬌* U2 - ) → ( ∀L0,T0. ⦃h, L0⦄ ⊩ T0 :[g] → ∀U0. ⦃h, L0⦄ ⊢ T0 •➡*[g] U0 → - #{L0, T0} < #{L ,T} → - ⦃h, L0⦄ ⊩ U0 :[g] + #{L0, T0} < #{L ,T} → ⦃h, L0⦄ ⊩ U0 :[g] ) → ∀L0,T0. ⦃h, L0⦄ ⊩ T0 :[g] → - ∀U0,l. ⦃h, L⦄ ⊢ T0 •[g, l + 1] U0 → + ∀U0,l. ⦃h, L0⦄ ⊢ T0 •[g, l + 1] U0 → L0 = L → T0 = T → ⦃h, L0⦄ ⊩ U0 :[g]. -#h #g #L #T #IH2 #IH1 #L0 #T0 * -L0 -T0 +#h #g #L #T #IH1 #L0 #T0 * -L0 -T0 [ | | @@ -55,13 +47,6 @@ fact snv_ssta_conf_aux: ∀h,g,L,T. ( elim (ssta_inv_appl1 … H) -H #U0 #HTU0 #H destruct lapply (IH1 … HT0 U0 ? ?) // [ /3 width=2/ ] -HTU0 #HU0 @(snv_appl … HV HU0 HVW HW0) -HV -HU0 -HVW -HW0 -| #L0 #W #T0 #W0 #l0 #HW #HT0 #HTW0 #HW0 #X #l #H #H1 #H2 destruct - elim (ssta_inv_cast1 … H) -H plus_n_2 - @deg_SO_pos >iter_SO /2 width=1/ (**) (* explicit constructor: iter_SO is needed *) ] qed. @@ -96,6 +92,14 @@ let rec sd_l (h:sh) (k:nat) (l:nat) on l : sd h ≝ (* Basic properties *********************************************************) +lemma deg_pred: ∀h,g,k,l. deg h g (next h k) (l + 1) → deg h g k (l + 2). +#h #g #k #l #H1 +elim (deg_total h g k) #l0 #H0 +lapply (deg_next … H0) #H2 +lapply (deg_mono … H1 H2) -H1 -H2 #H +<(associative_plus l 1 1) >H 6 4 6 6 6 7 + 7 4 7 7 3 4 diff --git a/matita/matita/contribs/lambda_delta/ground_2/xoa.ma b/matita/matita/contribs/lambda_delta/ground_2/xoa.ma index f4296024f..9da161d42 100644 --- a/matita/matita/contribs/lambda_delta/ground_2/xoa.ma +++ b/matita/matita/contribs/lambda_delta/ground_2/xoa.ma @@ -184,6 +184,14 @@ inductive ex6_7 (A0,A1,A2,A3,A4,A5,A6:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2 interpretation "multiple existental quantifier (6, 7)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_7 ? ? ? ? ? ? ? P0 P1 P2 P3 P4 P5). +(* multiple existental quantifier (7, 4) *) + +inductive ex7_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→Prop) : Prop ≝ + | ex7_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → P3 x0 x1 x2 x3 → P4 x0 x1 x2 x3 → P5 x0 x1 x2 x3 → P6 x0 x1 x2 x3 → ex7_4 ? ? ? ? ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (7, 4)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_4 ? ? ? ? P0 P1 P2 P3 P4 P5 P6). + (* multiple existental quantifier (7, 7) *) inductive ex7_7 (A0,A1,A2,A3,A4,A5,A6:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→A4→A5→A6→Prop) : Prop ≝ diff --git a/matita/matita/contribs/lambda_delta/ground_2/xoa_notation.ma b/matita/matita/contribs/lambda_delta/ground_2/xoa_notation.ma index ed4b83f83..9e2f4d099 100644 --- a/matita/matita/contribs/lambda_delta/ground_2/xoa_notation.ma +++ b/matita/matita/contribs/lambda_delta/ground_2/xoa_notation.ma @@ -224,6 +224,16 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P5) }. +(* multiple existental quantifier (7, 4) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 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)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P6) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 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)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P6) }. + (* multiple existental quantifier (7, 7) *) notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 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)" -- 2.39.2