From f21509c476b20e5446335c967b1e81f87ceb4f6c Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 24 Feb 2012 12:53:09 +0000 Subject: [PATCH] - "functional" component moved to Apps_2 - property S5 of the candidates of reducibility almost proved ... --- .../{Basic_2 => Apps_2}/functional/lift.ma | 1 + .../Apps_2/functional/notation.ma | 27 ++++++++++++ .../{Basic_2 => Apps_2}/functional/rtm.ma | 0 .../functional/rtm_step.ma | 2 +- .../{Basic_2 => Apps_2}/functional/subst.ma | 2 +- .../Basic_2/computation/cprs_tstc_vector.ma | 34 ++++++++++++++ .../Basic_2/computation/csn_aaa.ma | 6 +-- .../{csn_cr.ma => csn_lcpr_vector.ma} | 42 ++++++++++++------ .../Basic_2/computation/csn_lift.ma | 20 +++++---- .../Basic_2/grammar/term_simple.ma | 5 +++ .../lambda_delta/Basic_2/grammar/tstc.ma | 2 - .../contribs/lambda_delta/Basic_2/notation.ma | 16 +++---- matita/matita/contribs/lambda_delta/Makefile | 44 ++++++++++--------- 13 files changed, 142 insertions(+), 59 deletions(-) rename matita/matita/contribs/lambda_delta/{Basic_2 => Apps_2}/functional/lift.ma (98%) create mode 100644 matita/matita/contribs/lambda_delta/Apps_2/functional/notation.ma rename matita/matita/contribs/lambda_delta/{Basic_2 => Apps_2}/functional/rtm.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => Apps_2}/functional/rtm_step.ma (98%) rename matita/matita/contribs/lambda_delta/{Basic_2 => Apps_2}/functional/subst.ma (98%) create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_tstc_vector.ma rename matita/matita/contribs/lambda_delta/Basic_2/computation/{csn_cr.ma => csn_lcpr_vector.ma} (69%) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/functional/lift.ma b/matita/matita/contribs/lambda_delta/Apps_2/functional/lift.ma similarity index 98% rename from matita/matita/contribs/lambda_delta/Basic_2/functional/lift.ma rename to matita/matita/contribs/lambda_delta/Apps_2/functional/lift.ma index 780467209..aefa1576d 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/functional/lift.ma +++ b/matita/matita/contribs/lambda_delta/Apps_2/functional/lift.ma @@ -14,6 +14,7 @@ include "Ground_2/tri.ma". include "Basic_2/substitution/lift.ma". +include "Apps_2/functional/notation.ma". (* RELOCATION ***************************************************************) diff --git a/matita/matita/contribs/lambda_delta/Apps_2/functional/notation.ma b/matita/matita/contribs/lambda_delta/Apps_2/functional/notation.ma new file mode 100644 index 000000000..48df845c1 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Apps_2/functional/notation.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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE "functional" COMPONENT ********************************) + +notation "hvbox( ↑ [ d , break e ] break T )" + non associative with precedence 55 + for @{ 'Lift $d $e $T }. + +notation "hvbox( [ d ← break V ] break T )" + non associative with precedence 55 + for @{ 'Subst $V $d $T }. + +notation "hvbox( T1 ⇨ break T2 )" + non associative with precedence 45 + for @{ 'SRed $T1 $T2 }. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/functional/rtm.ma b/matita/matita/contribs/lambda_delta/Apps_2/functional/rtm.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/functional/rtm.ma rename to matita/matita/contribs/lambda_delta/Apps_2/functional/rtm.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/functional/rtm_step.ma b/matita/matita/contribs/lambda_delta/Apps_2/functional/rtm_step.ma similarity index 98% rename from matita/matita/contribs/lambda_delta/Basic_2/functional/rtm_step.ma rename to matita/matita/contribs/lambda_delta/Apps_2/functional/rtm_step.ma index c1dc7dcb1..5b2a4eb2c 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/functional/rtm_step.ma +++ b/matita/matita/contribs/lambda_delta/Apps_2/functional/rtm_step.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/functional/rtm.ma". +include "Apps_2/functional/rtm.ma". (* REDUCTION AND TYPE MACHINE ***********************************************) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/functional/subst.ma b/matita/matita/contribs/lambda_delta/Apps_2/functional/subst.ma similarity index 98% rename from matita/matita/contribs/lambda_delta/Basic_2/functional/subst.ma rename to matita/matita/contribs/lambda_delta/Apps_2/functional/subst.ma index b12e9b413..6aa75625d 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/functional/subst.ma +++ b/matita/matita/contribs/lambda_delta/Apps_2/functional/subst.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "Basic_2/unfold/delift_lift.ma". -include "Basic_2/functional/lift.ma". +include "Apps_2/functional/lift.ma". (* CORE SUBSTITUTION ********************************************************) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_tstc_vector.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_tstc_vector.ma new file mode 100644 index 000000000..d073bad24 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_tstc_vector.ma @@ -0,0 +1,34 @@ +(**************************************************************************) +(* ___ *) +(* ||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/substitution/lift_vector.ma". +include "Basic_2/computation/cprs_tstc.ma". + +(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) + +(* Vector form of forward lemmas involving same top term constructor ********) + +lemma cpr_fwd_theta_vector: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → + ∀V,T,U. L ⊢ ⒶV1s. ⓓV. T ➡ U → + ⒶV1s. ⓓV. T ≃ U ∨ L ⊢ ⓓV. ⒶV2s. T ➡* U. +#L #V1s #V2s * -V1s -V2s /3 width=1/ +#V1s #V2s #V1a #V2a #HV12a * -V1s -V2s /2 width=1 by cpr_fwd_theta/ -HV12a +#V1s #V2s #V1b #V2b #_ #_ #V #U #T #H +elim (cpr_inv_appl1_simple … H ?) -H // +#V0 #T0 #_ #_ #H destruct /2 width=1/ +qed-. + +axiom cprs_fwd_theta_vector: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → + ∀V,T,U. L ⊢ ⒶV1s. ⓓV. T ➡* U → + ⒶV1s. ⓓV. T ≃ U ∨ L ⊢ ⓓV. ⒶV2s. T ➡* U. \ No newline at end of file diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_aaa.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_aaa.ma index 8bc613aa4..421a3a7f7 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_aaa.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_aaa.ma @@ -13,13 +13,13 @@ (**************************************************************************) include "Basic_2/computation/acp_aaa.ma". -include "Basic_2/computation/csn_cr.ma". +include "Basic_2/computation/csn_lcpr_vector.ma". (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) -(* Main properties **********************************************************) +(* Properties concerning atomic arity assignment ****************************) -theorem csn_aaa: ∀L,T,A. L ⊢ T ÷ A → L ⊢ ⬇* T. +lemma csn_aaa: ∀L,T,A. L ⊢ T ÷ A → L ⊢ ⬇* T. #L #T #A #H @(acp_aaa … csn_acp csn_acr … H) qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lcpr_vector.ma similarity index 69% rename from matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.ma rename to matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lcpr_vector.ma index 81c179293..36e44ce6d 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lcpr_vector.ma @@ -13,14 +13,14 @@ (**************************************************************************) include "Basic_2/computation/acp_cr.ma". +include "Basic_2/computation/cprs_tstc_vector.ma". include "Basic_2/computation/csn_lcpr.ma". include "Basic_2/computation/csn_vector.ma". -(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) +(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERM VECTORS **********************) (* Advanced properties ******************************************************) (* - (* Basic_1: was only: sn3_appl_appls *) lemma csn_appl_appls_simple_tstc: ∀L,Vs,V,T1. L ⊢ ⬇* V → L ⊢ ⬇* T1 → (∀T2. L ⊢ ⒶVs.T1 ➡* T2 → (ⒶVs.T1 ≃ T2 → False) → L ⊢ ⬇* ⓐV. T2) → @@ -33,21 +33,35 @@ lemma csn_appl_appls_simple_tstc: ∀L,Vs,V,T1. L ⊢ ⬇* V → L ⊢ ⬇* T1 [ @H2T1 ] qed. - +*) lemma csn_applv_theta: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → ∀V,T. L ⊢ ⬇* ⓓV. ⒶV2s. T → L ⊢ ⬇* V → L ⊢ ⬇* ⒶV1s. ⓓV. T. #L #V1s #V2s * -V1s -V2s /2 width=1/ -#V1s #V2s #V1 #V2 #HV12 * -V1s -V2s /2 width=3/ -#V1s #V2s #W1 #W2 #HW12 #HV12s #V #T #H #HV -lapply (csn_appl_theta … HV12 … H) -H -HV12 #H -lapply (csn_fwd_pair_sn … H) #HV1 -@csn_appl_simple // #X #H1 #H2 -whd in ⊢ (? ? %); -*) +#V1s #V2s #V1 #V2 #HV12 #H +generalize in match HV12; -HV12 generalize in match V2; -V2 generalize in match V1; -V1 +elim H -V1s -V2s /2 width=3/ +#V1s #V2s #V1 #V2 #HV12 #HV12s #IHV12s #W1 #W2 #HW12 #V #T #H #HV +lapply (csn_appl_theta … HW12 … H) -H -HW12 #H +lapply (csn_fwd_pair_sn … H) #HW1 +lapply (csn_fwd_flat_dx … H) #H1 +@csn_appl_simple_tstc // -HW1 /2 width=3/ -IHV12s -HV -H1 #X #H1 #H2 +elim (cprs_fwd_theta_vector … (V2::V2s) … H1) -H1 /2 width=1/ -HV12s -HV12 +[ -H #H elim (H2 ?) -H2 // +| -H2 #H1 @(csn_cprs_trans … H) -H /2 width=1/ +] +qed. (* -lemma csn_S5: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → - ∀V,T. L. ⓓV ⊢ ⬇* ⒶV2s. T → L ⊢ ⬇* V → L ⊢ ⬇* ⒶV1s. ⓓV. T. -#L #V1s #V2s #H elim H -V1s -V2s /2 width=1/ +theorem csn_acr: acr cpr (eq …) (csn …) (λL,T. L ⊢ ⬇* T). +@mk_acr // +[ +| +| +| #L #V1 #V2 #HV12 #V #T #H #HVT + @(csn_applv_theta … HV12) -HV12 // + @(csn_abbr) // +| +| @csn_lift +] +qed. *) - axiom csn_acr: acr cpr (eq …) (csn …) (λL,T. L ⊢ ⬇* T). diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lift.ma index 1326a8bb4..01d983c0c 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lift.ma @@ -43,15 +43,6 @@ qed. (* Advanced properties ******************************************************) -lemma csn_acp: acp cpr (eq …) (csn …). -@mk_acp -[ /2 width=1/ -| /2 width=3/ -| /2 width=5/ -| @cnf_lift -] -qed. - (* Basic_1: was: sn3_abbr *) lemma csn_lref_abbr: ∀L,K,V,i. ⇩[0, i] L ≡ K. ⓓV → K ⊢ ⬇* V → L ⊢ ⬇* #i. #L #K #V #i #HLK #HV @@ -96,3 +87,14 @@ elim (eq_false_inv_tpair_dx … H2) -H2 @IHT1 -IHT1 // -HLT02 /2 width=1/ ] qed. + +(* Main properties **********************************************************) + +theorem csn_acp: acp cpr (eq …) (csn …). +@mk_acp +[ /2 width=1/ +| /2 width=3/ +| /2 width=5/ +| @cnf_lift +] +qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_simple.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_simple.ma index 557299afd..9b6c08270 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_simple.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_simple.ma @@ -34,3 +34,8 @@ qed. lemma simple_inv_bind: ∀I,V,T. 𝐒[ⓑ{I} V. T] → False. /2 width=6/ qed-. + +lemma simple_inv_pair: ∀I,V,T. 𝐒[②{I}V.T] → ∃J. I = Flat2 J. +* /2 width=2/ #I #V #T #H +elim (simple_inv_bind … H) +qed-. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/tstc.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/tstc.ma index 9c91d59f9..75ec4c523 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/tstc.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/tstc.ma @@ -97,8 +97,6 @@ lemma tstc_dec: ∀T1,T2. Decidable (T1 ≃ T2). ] qed. -axiom simple_inv_pair: ∀I,V,T. 𝐒[②{I}V.T] → ∃J. I = Flat2 J. - lemma simple_tstc_repl_dx: ∀T1,T2. T1 ≃ T2 → 𝐒[T1] → 𝐒[T2]. #T1 #T2 * -T1 -T2 // #I #V1 #V2 #T1 #T2 #H diff --git a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma index 7d05a2f67..0aabfd481 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma @@ -294,16 +294,14 @@ notation "hvbox( T1 break [ R ] ⊑ break T2 )" non associative with precedence 45 for @{ 'CrSubEq $T1 $R $T2 }. -(* Functional ***************************************************************) +(* Conversion ***************************************************************) -notation "hvbox( ↑ [ d , break e ] break T )" - non associative with precedence 55 - for @{ 'Lift $d $e $T }. +notation "hvbox( L ⊢ break term 90 T1 ⬌ break T2 )" + non associative with precedence 45 + for @{ 'PConv $L $T1 $T2 }. -notation "hvbox( [ d ← break V ] break T )" - non associative with precedence 55 - for @{ 'Subst $V $d $T }. +(* Congruence ***************************************************************) -notation "hvbox( T1 ⇨ break T2 )" +notation "hvbox( L ⊢ break term 90 T1 ⬌* break T2 )" non associative with precedence 45 - for @{ 'SRed $T1 $T2 }. + for @{ 'PConvStar $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambda_delta/Makefile b/matita/matita/contribs/lambda_delta/Makefile index e5a20a1f3..3ce097690 100644 --- a/matita/matita/contribs/lambda_delta/Makefile +++ b/matita/matita/contribs/lambda_delta/Makefile @@ -5,7 +5,7 @@ XOA = xoa.native CONF = Ground_2/xoa.conf.xml TARGETS = Ground_2/xoa_natation.ma Ground_2/xoa.ma -PACKAGES = Ground_2 Basic_2 +PACKAGES = Ground_2 Basic_2 Apps_2 all: @@ -25,10 +25,12 @@ stats: $(PACKAGES:%=%.stats) %.stats: CHARS = $(shell cat $(MAS) | wc -c) -%.stats: C1 = $(shell grep "inductive\|record" $(MAS) | wc -l) -%.stats: C2 = $(shell grep "definition\|let rec" $(MAS) | wc -l) +%.stats: C1 = $(shell grep "inductive \|record " $(MAS) | wc -l) +%.stats: C2 = $(shell grep "definition \|let rec " $(MAS) | wc -l) +%.stats: C3 = $(shell grep "inductive \|record \|definition \|let rec " $(MAS) | wc -l) %.stats: P1 = $(shell grep "theorem " $(MAS) | wc -l) %.stats: P2 = $(shell grep "lemma " $(MAS) | wc -l) +%.stats: P3 = $(shell grep "lemma \|theorem " $(MAS) | wc -l) %.stats: TBL = ld_$*_sum @@ -65,20 +67,22 @@ stats: $(PACKAGES:%=%.stats) @printf ' %-6s %3i' Marks `grep "(\*\*)" $(MAS) | wc -l` @printf ' %-10s' '' @printf '\x1B[0m\n' - @printf 'name "$(TBL)"\n\n' > $*/$(TBL).tbl - @printf 'table {\n' >> $*/$(TBL).tbl - @printf ' class "grey" [ "category"\n' >> $*/$(TBL).tbl - @printf ' [ "objects" * ]\n' >> $*/$(TBL).tbl - @printf ' ]\n' >> $*/$(TBL).tbl - @printf ' class "green" [ "propositions"\n' >> $*/$(TBL).tbl - @printf ' [ "theorems" "$(P1)" * ]\n' >> $*/$(TBL).tbl - @printf ' [ "lemmas" "$(P2)" * ]\n' >> $*/$(TBL).tbl - @printf ' ]\n' >> $*/$(TBL).tbl - @printf ' class "yellow" [ "concepts"\n' >> $*/$(TBL).tbl - @printf ' [ "declared" "$(C1)" * ]\n' >> $*/$(TBL).tbl - @printf ' [ "defined" "$(C2)" * ]\n' >> $*/$(TBL).tbl - @printf ' ]\n' >> $*/$(TBL).tbl - @printf '}\n\n' >> $*/$(TBL).tbl - @printf 'class "component" { 0 }\n\n' >> $*/$(TBL).tbl - @printf 'class "plane" { 1 } { 3 } \n\n' >> $*/$(TBL).tbl - @printf 'class "number" { 2 } { 4 } \n\n' >> $*/$(TBL).tbl + @printf 'name "$(TBL)"\n\n' > $*/$(TBL).tbl + @printf 'table {\n' >> $*/$(TBL).tbl + @printf ' class "grey" [ "category"\n' >> $*/$(TBL).tbl + @printf ' [ "objects" * ]\n' >> $*/$(TBL).tbl + @printf ' ]\n' >> $*/$(TBL).tbl + @printf ' class "green" [ "propositions"\n' >> $*/$(TBL).tbl + @printf ' [ "theorems" "$(P1)" * ]\n' >> $*/$(TBL).tbl + @printf ' [ "lemmas" "$(P2)" * ]\n' >> $*/$(TBL).tbl + @printf ' [ "total" "$(P3)" * ]\n' >> $*/$(TBL).tbl + @printf ' ]\n' >> $*/$(TBL).tbl + @printf ' class "yellow" [ "concepts"\n' >> $*/$(TBL).tbl + @printf ' [ "declared" "$(C1)" * ]\n' >> $*/$(TBL).tbl + @printf ' [ "defined" "$(C2)" * ]\n' >> $*/$(TBL).tbl + @printf ' [ "total" "$(C3)" * ]\n' >> $*/$(TBL).tbl + @printf ' ]\n' >> $*/$(TBL).tbl + @printf '}\n\n' >> $*/$(TBL).tbl + @printf 'class "component" { 0 }\n\n' >> $*/$(TBL).tbl + @printf 'class "plane" { 1 } { 3 } { 5 } \n\n' >> $*/$(TBL).tbl + @printf 'class "number" { 2 } { 4 } { 6 } \n\n' >> $*/$(TBL).tbl -- 2.39.2