From 4a5254d45ba455e195b7ae2afca2212446e65ca3 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 14 Mar 2012 19:53:16 +0000 Subject: [PATCH] property S2 of strongly normalizing terms proved! --- .../contribs/lambda_delta/basic_2/basic_1.txt | 2 -- .../lambda_delta/basic_2/computation/cprs.ma | 8 ++++- .../basic_2/computation/cprs_tstc.ma | 5 +++ .../basic_2/computation/cprs_tstc_vector.ma | 14 +++++++++ .../lambda_delta/basic_2/computation/csn.ma | 4 +-- .../basic_2/computation/csn_aaa.ma | 2 +- ...{csn_lcpr_vector.ma => csn_tstc_vector.ma} | 31 +++++++++---------- .../basic_2/computation/csn_vector.ma | 7 +++++ 8 files changed, 51 insertions(+), 22 deletions(-) rename matita/matita/contribs/lambda_delta/basic_2/computation/{csn_lcpr_vector.ma => csn_tstc_vector.ma} (88%) diff --git a/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt index 5370377e6..dcb49f2ce 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt +++ b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt @@ -268,8 +268,6 @@ sn3/props sn3_shift sn3/props sn3_change sn3/props sn3_gen_def sn3/props sn3_cdelta -sn3/props sn3_appl_appls -sn3/props sn3_appls_lref sn3/props sns3_lifts sty0/fwd sty0_gen_sort diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma index a91c9d8b5..4341a5a94 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/reducibility/cpr.ma". +include "basic_2/reducibility/cnf.ma". (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) @@ -82,6 +82,12 @@ elim (cpr_inv_cast1 … HU2) -HU2 /3 width=3/ * #W2 #T2 #HW2 #HT2 #H destruct /4 width=5/ qed-. +lemma cprs_inv_cnf1: ∀L,T,U. L ⊢ T ➡* U → L ⊢ 𝐍[T] → T = U. +#L #T #U #H @(cprs_ind_dx … H) -T // +#T0 #T #H1T0 #_ #IHT #H2T0 +lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1/ +qed-. + (* Basic_1: removed theorems 6: clear_pr3_trans pr3_cflat pr3_gen_bind pr3_iso_appl_bind pr3_iso_appls_appl_bind pr3_iso_appls_bind diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma index c7f49d1cf..359174503 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma @@ -20,6 +20,11 @@ include "basic_2/computation/cprs_lcprs.ma". (* Forward lemmas involving same top term constructor ***********************) +lemma cprs_fwd_cnf: ∀L,T. L ⊢ 𝐍[T] → ∀U. L ⊢ T ➡* U → T ≃ U. +#L #T #HT #U #H +>(cprs_inv_cnf1 … H HT) -L -T // +qed-. + (* Basic_1: was: pr3_iso_beta *) lemma cprs_fwd_beta: ∀L,V,W,T,U. L ⊢ ⓐV. ⓛW. T ➡* U → ⓐV. ⓛW. T ≃ U ∨ L ⊢ ⓓV. T ➡* U. 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 index d12a9f498..2f8486cc2 100644 --- 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 @@ -20,6 +20,20 @@ include "basic_2/computation/cprs_tstc.ma". (* Vector form of forward lemmas involving same top term constructor ********) +lemma cprs_fwd_cnf_vector: ∀L,T. 𝐒[T] → L ⊢ 𝐍[T] → ∀Vs,U. L ⊢ ⒶVs.T ➡* U → ⒶVs.T ≃ U. +#L #T #H1T #H2T #Vs elim Vs -Vs [ @(cprs_fwd_cnf … H2T) ] (**) (* /2 width=3 by cprs_fwd_cnf/ does not work *) +#V #Vs #IHVs #U #H +elim (cprs_inv_appl1 … H) -H * +[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1/ +| #V0 #W0 #T0 #HV0 #HT0 #HU + lapply (IHVs … HT0) -IHVs -HT0 #HT0 + elim (tstc_inv_bind_appls_simple … HT0 ?) // +| #V1 #V2 #V0 #T0 #HV1 #HV12 #HT0 #HU + lapply (IHVs … HT0) -IHVs -HT0 #HT0 + elim (tstc_inv_bind_appls_simple … HT0 ?) // +] +qed-. + (* Basic_1: was: pr3_iso_appls_beta *) lemma cprs_fwd_beta_vector: ∀L,Vs,V,W,T,U. L ⊢ ⒶVs. ⓐV. ⓛW. T ➡* U → ⒶVs. ⓐV. ⓛW. T ≃ U ∨ L ⊢ ⒶVs. ⓓV. T ➡* U. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma index 5552c6fb7..14655cdee 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma @@ -82,8 +82,8 @@ qed. lemma csn_fwd_flat_dx: ∀I,L,V,T. L ⊢ ⬇* ⓕ{I} V. T → L ⊢ ⬇* T. /2 width=5/ qed-. -(* Basic_1: removed theorems 9: +(* Basic_1: removed theorems 10: sn3_gen_cflat sn3_cflat sn3_appl_cast sn3_appl_beta sn3_appl_lref sn3_appl_abbr - sn3_bind sn3_appl_bind sn3_appls_bind + sn3_appl_appls sn3_bind sn3_appl_bind sn3_appls_bind *) 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 112e2d4b7..67312a9ac 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,7 +13,7 @@ (**************************************************************************) include "basic_2/computation/acp_aaa.ma". -include "basic_2/computation/csn_lcpr_vector.ma". +include "basic_2/computation/csn_tstc_vector.ma". (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma similarity index 88% rename from matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr_vector.ma rename to matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma index 5f5465b4f..00de73f52 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr_vector.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma @@ -20,20 +20,21 @@ include "basic_2/computation/csn_vector.ma". (* 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) → - 𝐒[T1] → L ⊢ ⬇* ⓐV. ⒶVs. T1. -#L * -[ #V #T1 #HV - @csn_appl_simple_tstc // -| #V0 #Vs #V #T1 #HV #H1T1 #H2T1 #H3T1 - @csn_appl_simple_tstc // -HV - [ @H2T1 + +(* Basic_1: was only: sn3_appls_lref *) +lemma csn_applv_cnf: ∀L,T. 𝐒[T] → L ⊢ 𝐍[T] → + ∀Vs. L ⊢ ⬇* Vs → L ⊢ ⬇* ⒶVs.T. +#L #T #H1T #H2T #Vs elim Vs -Vs [ #_ @(csn_cnf … H2T) ] (**) (* /2 width=1/ does not work *) +#V #Vs #IHV #H +elim (csnv_inv_cons … H) -H #HV #HVs +@csn_appl_simple_tstc // -HV /2 width=1/ -IHV -HVs +[ #X #H #H0 + lapply (cprs_fwd_cnf_vector … H) -H // -H1T -H2T #H + elim (H0 ?) -H0 // +| -L -V elim Vs -Vs // ] qed. -*) + (* Basic_1: was: sn3_appls_beta *) lemma csn_applv_beta: ∀L,W. L ⊢ ⬇* W → ∀Vs,V,T. L ⊢ ⬇* ⒶVs.ⓓV.T → @@ -109,10 +110,10 @@ lapply (csn_fwd_flat_dx … H1T) #H2T | -H1T elim Vs -Vs // ] qed. -(* + theorem csn_acr: acr cpr (eq …) (csn …) (λL,T. L ⊢ ⬇* T). @mk_acr // -[ +[ /3 width=1/ | /2 width=1/ | /2 width=6/ | #L #V1 #V2 #HV12 #V #T #H #HVT @@ -122,5 +123,3 @@ theorem csn_acr: acr cpr (eq …) (csn …) (λL,T. L ⊢ ⬇* T). | @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_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_vector.ma index b4a087a1a..7dab76e23 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_vector.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_vector.ma @@ -26,6 +26,13 @@ interpretation "context-sensitive strong normalization (term vector)" 'SN L Ts = (csnv L Ts). +(* Basic properties *********************************************************) + +lemma all_csnv: ∀L,Vs. all … (csn L) Vs → L ⊢ ⬇* Vs. +#L #Vs elim Vs -Vs // +#V #Vs #IHVs * /3 width=1/ +qed. + (* Basic inversion lemmas ***************************************************) fact csnv_inv_cons_aux: ∀L,Ts. L ⊢ ⬇* Ts → ∀U,Us. Ts = U :: Us → -- 2.39.2