From: Ferruccio Guidi Date: Wed, 14 Mar 2012 19:53:16 +0000 (+0000) Subject: property S2 of strongly normalizing terms proved! X-Git-Tag: make_still_working~1855 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4a5254d45ba455e195b7ae2afca2212446e65ca3;p=helm.git property S2 of strongly normalizing terms proved! --- 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_lcpr_vector.ma deleted file mode 100644 index 5f5465b4f..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr_vector.ma +++ /dev/null @@ -1,126 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/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 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 -] -qed. -*) -(* Basic_1: was: sn3_appls_beta *) -lemma csn_applv_beta: ∀L,W. L ⊢ ⬇* W → - ∀Vs,V,T. L ⊢ ⬇* ⒶVs.ⓓV.T → - L ⊢ ⬇* ⒶVs. ⓐV.ⓛW. T. -#L #W #HW #Vs elim Vs -Vs /2 width=1/ -HW -#V0 #Vs #IHV #V #T #H1T -lapply (csn_fwd_pair_sn … H1T) #HV0 -lapply (csn_fwd_flat_dx … H1T) #H2T -@csn_appl_simple_tstc // -HV0 /2 width=1/ -IHV -H2T -[ #X #H #H0 - elim (cprs_fwd_beta_vector … H) -H #H - [ -H1T elim (H0 ?) -H0 // - | -H0 @(csn_cprs_trans … H1T) -H1T /2 width=1/ - ] -| -H1T elim Vs -Vs // -] -qed. - -lemma csn_applv_delta: ∀L,K,V1,i. ⇩[0, i] L ≡ K. ⓓV1 → - ∀V2. ⇧[0, i + 1] V1 ≡ V2 → - ∀Vs.L ⊢ ⬇* (ⒶVs. V2) → L ⊢ ⬇* (ⒶVs. #i). -#L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs -[ #H - lapply (ldrop_fwd_ldrop2 … HLK) #HLK0 - lapply (csn_inv_lift … H … HLK0 HV12) -V2 -HLK0 /2 width=4/ -| #V #Vs #IHV #H1T - lapply (csn_fwd_pair_sn … H1T) #HV - lapply (csn_fwd_flat_dx … H1T) #H2T - @csn_appl_simple_tstc // -HV /2 width=1/ -IHV -H2T - [ #X #H #H0 - elim (cprs_fwd_delta_vector … HLK … HV12 … H) -HLK -HV12 -H #H - [ -H1T elim (H0 ?) -H0 // - | -H0 @(csn_cprs_trans … H1T) -H1T /2 width=1/ - ] - | -L -K -V -V1 -V2 elim Vs -Vs // - ] -] -qed. - -(* Basic_1: was: sn3_appls_abbr *) -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 #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. - -(* Basic_1: was: sn3_appls_cast *) -lemma csn_applv_tau: ∀L,W. L ⊢ ⬇* W → - ∀Vs,T. L ⊢ ⬇* ⒶVs. T → - L ⊢ ⬇* ⒶVs. ⓣW. T. -#L #W #HW #Vs elim Vs -Vs /2 width=1/ -HW -#V #Vs #IHV #T #H1T -lapply (csn_fwd_pair_sn … H1T) #HV -lapply (csn_fwd_flat_dx … H1T) #H2T -@csn_appl_simple_tstc // -HV /2 width=1/ -IHV -H2T -[ #X #H #H0 - elim (cprs_fwd_tau_vector … H) -H #H - [ -H1T elim (H0 ?) -H0 // - | -H0 @(csn_cprs_trans … H1T) -H1T /2 width=1/ - ] -| -H1T elim Vs -Vs // -] -qed. -(* -theorem csn_acr: acr cpr (eq …) (csn …) (λL,T. L ⊢ ⬇* T). -@mk_acr // -[ -| /2 width=1/ -| /2 width=6/ -| #L #V1 #V2 #HV12 #V #T #H #HVT - @(csn_applv_theta … HV12) -HV12 // - @(csn_abbr) // -| /2 width=1/ -| @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_tstc_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma new file mode 100644 index 000000000..00de73f52 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma @@ -0,0 +1,125 @@ +(**************************************************************************) +(* ___ *) +(* ||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/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 TERM VECTORS **********************) + +(* Advanced properties ******************************************************) + +(* 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 → + L ⊢ ⬇* ⒶVs. ⓐV.ⓛW. T. +#L #W #HW #Vs elim Vs -Vs /2 width=1/ -HW +#V0 #Vs #IHV #V #T #H1T +lapply (csn_fwd_pair_sn … H1T) #HV0 +lapply (csn_fwd_flat_dx … H1T) #H2T +@csn_appl_simple_tstc // -HV0 /2 width=1/ -IHV -H2T +[ #X #H #H0 + elim (cprs_fwd_beta_vector … H) -H #H + [ -H1T elim (H0 ?) -H0 // + | -H0 @(csn_cprs_trans … H1T) -H1T /2 width=1/ + ] +| -H1T elim Vs -Vs // +] +qed. + +lemma csn_applv_delta: ∀L,K,V1,i. ⇩[0, i] L ≡ K. ⓓV1 → + ∀V2. ⇧[0, i + 1] V1 ≡ V2 → + ∀Vs.L ⊢ ⬇* (ⒶVs. V2) → L ⊢ ⬇* (ⒶVs. #i). +#L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs +[ #H + lapply (ldrop_fwd_ldrop2 … HLK) #HLK0 + lapply (csn_inv_lift … H … HLK0 HV12) -V2 -HLK0 /2 width=4/ +| #V #Vs #IHV #H1T + lapply (csn_fwd_pair_sn … H1T) #HV + lapply (csn_fwd_flat_dx … H1T) #H2T + @csn_appl_simple_tstc // -HV /2 width=1/ -IHV -H2T + [ #X #H #H0 + elim (cprs_fwd_delta_vector … HLK … HV12 … H) -HLK -HV12 -H #H + [ -H1T elim (H0 ?) -H0 // + | -H0 @(csn_cprs_trans … H1T) -H1T /2 width=1/ + ] + | -L -K -V -V1 -V2 elim Vs -Vs // + ] +] +qed. + +(* Basic_1: was: sn3_appls_abbr *) +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 #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. + +(* Basic_1: was: sn3_appls_cast *) +lemma csn_applv_tau: ∀L,W. L ⊢ ⬇* W → + ∀Vs,T. L ⊢ ⬇* ⒶVs. T → + L ⊢ ⬇* ⒶVs. ⓣW. T. +#L #W #HW #Vs elim Vs -Vs /2 width=1/ -HW +#V #Vs #IHV #T #H1T +lapply (csn_fwd_pair_sn … H1T) #HV +lapply (csn_fwd_flat_dx … H1T) #H2T +@csn_appl_simple_tstc // -HV /2 width=1/ -IHV -H2T +[ #X #H #H0 + elim (cprs_fwd_tau_vector … H) -H #H + [ -H1T elim (H0 ?) -H0 // + | -H0 @(csn_cprs_trans … H1T) -H1T /2 width=1/ + ] +| -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 + @(csn_applv_theta … HV12) -HV12 // + @(csn_abbr) // +| /2 width=1/ +| @csn_lift +] +qed. 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 →