From 10fa9ea840893d1b452200a402612f923765967e Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 27 Feb 2012 21:43:36 +0000 Subject: [PATCH] - property S6 of stronfly normalizing terms proved - more properties concerning context sensitive computation --- .../contribs/lambda_delta/Basic_2/Basic_1.txt | 5 -- .../lambda_delta/Basic_2/computation/cprs.ma | 19 ++++++ .../Basic_2/computation/cprs_cprs.ma | 59 +++++++++++++++---- .../Basic_2/computation/cprs_tstc.ma | 20 +++++++ .../Basic_2/computation/cprs_tstc_vector.ma | 37 +++++++++++- .../Basic_2/computation/csn_lcpr.ma | 1 - .../Basic_2/computation/csn_lcpr_vector.ma | 24 +++++++- .../lambda_delta/Basic_2/grammar/tstc.ma | 4 -- .../Basic_2/reducibility/cpr_cpr.ma | 1 - 9 files changed, 145 insertions(+), 25 deletions(-) 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 ae211d291..5e2e3d961 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt +++ b/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt @@ -252,17 +252,13 @@ pr2/fwd pr2_gen_void pr2/props pr2_ctail pr2/subst1 pr2_gen_cabbr -pr3/fwd pr3_gen_sort pr3/fwd pr3_gen_abst -pr3/fwd pr3_gen_cast -pr3/fwd pr3_gen_lift pr3/fwd pr3_gen_lref pr3/fwd pr3_gen_void pr3/fwd pr3_gen_abbr pr3/fwd pr3_gen_appl pr3/fwd pr3_gen_bind pr3/iso pr3_iso_appls_abbr -pr3/iso pr3_iso_appls_cast pr3/iso pr3_iso_appl_bind pr3/iso pr3_iso_appls_appl_bind pr3/iso pr3_iso_appls_bind @@ -277,7 +273,6 @@ pr3/props pr3_head_21 pr3/props pr3_head_12 pr3/props pr3_flat pr3/props pr3_pr3_pr3_t -pr3/props pr3_lift pr3/props pr3_eta pr3/subst1 pr3_subst1 pr3/subst1 pr3_gen_cabbr 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 3e4289e27..12cd0791f 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs.ma @@ -63,4 +63,23 @@ lemma cprs_flat_dx: ∀I,L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L ⊢ T1 ➡* T2 @(cprs_strap1 … IHT2) -IHT2 /2 width=1/ qed. +(* Basic inversion lemmas ***************************************************) + +(* Basic_1: was: pr3_gen_sort *) +lemma cprs_inv_sort1: ∀L,U2,k. L ⊢ ⋆k ➡* U2 → U2 = ⋆k. +#L #U2 #k #H @(cprs_ind … H) -U2 // +#U2 #U #_ #HU2 #IHU2 destruct +>(cpr_inv_sort1 … HU2) -HU2 // +qed-. + +(* Basic_1: was: pr3_gen_cast *) +lemma cprs_inv_cast1: ∀L,W1,T1,U2. L ⊢ ⓣW1.T1 ➡* U2 → L ⊢ T1 ➡* U2 ∨ + ∃∃W2,T2. L ⊢ W1 ➡* W2 & L ⊢ T1 ➡* T2 & U2 = ⓣW2.T2. +#L #W1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/ +#U2 #U #_ #HU2 * /3 width=3/ * +#W #T #HW1 #HT1 #H destruct +elim (cpr_inv_cast1 … HU2) -HU2 /3 width=3/ * +#W2 #T2 #HW2 #HT2 #H destruct /4 width=5/ +qed-. + (* Basic_1: removed theorems 2: clear_pr3_trans pr3_cflat *) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_cprs.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_cprs.ma index 9f8d517e2..54a94b496 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_cprs.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_cprs.ma @@ -12,7 +12,9 @@ (* *) (**************************************************************************) +include "Basic_2/reducibility/cpr_lift.ma". include "Basic_2/reducibility/cpr_cpr.ma". +include "Basic_2/reducibility/lcpr_cpr.ma". include "Basic_2/computation/cprs_lcpr.ma". (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) @@ -22,7 +24,7 @@ include "Basic_2/computation/cprs_lcpr.ma". lemma cprs_abbr_dx: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV1 ⊢ T1 ➡* T2 → L ⊢ ⓓV1. T1 ➡* ⓓV2. T2. #L #V1 #V2 #HV12 #T1 #T2 #HT12 @(cprs_ind_dx … HT12) -T1 -[ /3 width=1/ +[ /3 width=5/ | #T1 #T #HT1 #_ #IHT1 @(cprs_strap2 … IHT1) -IHT1 /2 width=1/ ] @@ -32,21 +34,58 @@ lemma cpr_abbr: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV1 ⊢ T1 ➡ T2 L ⊢ ⓓV1. T1 ➡* ⓓV2. T2. /3 width=1/ qed. -(* Basic_1: was only: pr3_pr2_pr3_t *) -lemma lcpr_cprs_trans: ∀L1,L2. L1 ⊢ ➡ L2 → - ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2. -#L1 #L2 #HL12 #T1 #T2 #H @(cprs_ind … H) -T2 // -#T #T2 #_ #HT2 #IHT2 /3 width=5/ +lemma cpr_abbr2: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV2 ⊢ T1 ➡ T2 → + L ⊢ ⓓV1. T1 ➡* ⓓV2. T2. +#L #V1 #V2 #HV12 #T1 #T2 #HT12 +lapply (lcpr_cpr_trans (L. ⓓV1) … HT12) /2 width=1/ qed. -(* Main propertis ***********************************************************) +(* Advanced inversion lemmas ************************************************) -(* Basic_1: was: pr3_t *) -theorem cprs_trans: ∀L,T1,T. L ⊢ T1 ➡* T → ∀T2. L ⊢ T ➡* T2 → L ⊢ T1 ➡* T2. -/2 width=3/ qed. +(* Basic_1: was pr3_gen_appl *) +lemma cprs_inv_appl1: ∀L,V1,T1,U2. L ⊢ ⓐV1. T1 ➡* U2 → + ∨∨ ∃∃V2,T2. L ⊢ V1 ➡* V2 & L ⊢ T1 ➡* T2 & + U2 = ⓐV2. T2 + | ∃∃V2,W,T. L ⊢ V1 ➡* V2 & + L ⊢ T1 ➡* ⓛW. T & L ⊢ ⓓV2. T ➡* U2 + | ∃∃V0,V2,V,T. L ⊢ V1 ➡* V0 & ⇧[0,1] V0 ≡ V2 & + L ⊢ T1 ➡* ⓓV. T & L ⊢ ⓓV. ⓐV2. T ➡* U2. +#L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/ +#U #U2 #_ #HU2 * * +[ #V0 #T0 #HV10 #HT10 #H destruct + elim (cpr_inv_appl1 … HU2) -HU2 * + [ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5/ + | #V2 #W2 #T #T2 #HV02 #HT2 #H1 #H2 destruct /4 width=7/ + | #V #V2 #W0 #W2 #T #T2 #HV0 #HW02 #HT2 #HV2 #H1 #H2 destruct + @or3_intro2 @(ex4_4_intro … HV2 HT10) /2 width=3/ /3 width=1/ (**) (* explicit constructor. /5 width=8/ is too slow because TC_transitive gets in the way *) + ] +| /4 width=8/ +| /4 width=10/ +] +qed-. + +(* Main propertis ***********************************************************) (* Basic_1: was: pr3_confluence *) theorem cprs_conf: ∀L,T1,T. L ⊢ T ➡* T1 → ∀T2. L ⊢ T ➡* T2 → ∃∃T0. L ⊢ T1 ➡* T0 & L ⊢ T2 ➡* T0. /3 width=3/ qed. +(* Basic_1: was: pr3_t *) +theorem cprs_trans: ∀L,T1,T. L ⊢ T1 ➡* T → ∀T2. L ⊢ T ➡* T2 → L ⊢ T1 ➡* T2. +/2 width=3/ qed. + +lemma cprs_flat: ∀I,L,T1,T2. L ⊢ T1 ➡* T2 → ∀V1,V2. L ⊢ V1 ➡* V2 → + L ⊢ ⓕ{I} V1. T1 ➡* ⓕ{I} V2. T2. +#I #L #T1 #T2 #HT12 #V1 #V2 #HV12 @(cprs_ind … HV12) -V2 /2 width=1/ +#V #V2 #_ #HV2 #IHV1 +@(cprs_trans … IHV1) -IHV1 /2 width=1/ +qed. + +(* Basic_1: was only: pr3_pr2_pr3_t *) +lemma lcpr_cprs_trans: ∀L1,L2. L1 ⊢ ➡ L2 → + ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2. +#L1 #L2 #HL12 #T1 #T2 #H @(cprs_ind … H) -T2 // +#T #T2 #_ #HT2 #IHT2 +@(cprs_trans … IHT2) /2 width=3/ +qed. 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 e19eb68b8..e623c7b90 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 @@ -13,13 +13,26 @@ (**************************************************************************) include "Basic_2/grammar/tstc.ma". +(* include "Basic_2/reducibility/cpr_lift.ma". include "Basic_2/reducibility/lcpr_cpr.ma". +*) include "Basic_2/computation/cprs_cprs.ma". (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) (* Forward lemmas involving same top term constructor ***********************) +(* +lemma cpr_fwd_beta: ∀L,V,W,T,U. L ⊢ ⓐV. ⓛW. T ➡ U → + ⓐV. ⓛW. T ≃ U ∨ L ⊢ ⓓV. T ➡* U. +#L #V #W #T #U #H +elim (cpr_inv_appl1 … H) -H * +[ #V0 #X #_ #_ #H destruct /2 width=1/ +| #V0 #W0 #T1 #T2 #HV0 #HT12 #H1 #H2 destruct + lapply (lcpr_cpr_trans (L. ⓓV) … HT12) -HT12 /2 width=1/ /3 width=1/ +| #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #H destruct +] +qed-. lemma cpr_fwd_theta: ∀L,V1,V,T,U. L ⊢ ⓐV1. ⓓV. T ➡ U → ∀V2. ⇧[0, 1] V1 ≡ V2 → ⓐV1. ⓓV. T ≃ U ∨ @@ -34,3 +47,10 @@ elim (cpr_inv_appl1 … H) -H * /4 width=1/ ] qed-. +*) +lemma cprs_fwd_tau: ∀L,W,T,U. L ⊢ ⓣW. T ➡* U → + ⓣW. T ≃ U ∨ L ⊢ T ➡* U. +#L #W #T #U #H +elim (cprs_inv_cast1 … H) -H /2 width=1/ * +#W0 #T0 #_ #_ #H destruct /2 width=1/ +qed-. 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 d073bad24..3e6f4a20d 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 @@ -12,12 +12,23 @@ (* *) (**************************************************************************) +include "Basic_2/grammar/tstc_vector.ma". 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_beta_vector: ∀L,V,W,T,U,Vs. L ⊢ ⒶVs. ⓐV. ⓛW. T ➡ U → + ⒶVs. ⓐV. ⓛW. T ≃ U ∨ L ⊢ ⒶVs. ⓓV. T ➡* U. +#L #V #W #T #U * /2 width=1 by cpr_fwd_beta/ +#V0 #Vs #H +elim (cpr_inv_appl1_simple … H ?) -H +[ #V1 #T1 #_ #_ #H destruct /2 width=1/ +| elim Vs -Vs // +] +qed-. lemma cpr_fwd_theta_vector: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → ∀V,T,U. L ⊢ ⒶV1s. ⓓV. T ➡ U → @@ -28,7 +39,31 @@ lemma cpr_fwd_theta_vector: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → elim (cpr_inv_appl1_simple … H ?) -H // #V0 #T0 #_ #_ #H destruct /2 width=1/ qed-. +*) + +(* Basic_1: was: pr3_iso_appls_cast *) +lemma cprs_fwd_tau_vector: ∀L,Vs,W,T,U. L ⊢ ⒶVs. ⓣW. T ➡* U → + ⒶVs. ⓣW. T ≃ U ∨ L ⊢ ⒶVs. T ➡* U. +#L #Vs elim Vs -Vs /2 width=1 by cprs_fwd_tau/ +#V #Vs #IHVs #W #T #U #H +elim (cprs_inv_appl1 … H) -H * +[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1/ +| #V0 #W0 #T0 #HV0 #HT0 #HU + elim (IHVs … HT0) -IHVs -HT0 #HT0 + [ elim (tstc_inv_bind_appls_simple … HT0 ?) // + | @or_intror + @(cprs_trans … HU) -HU + @(cprs_strap1 … (ⓐV0.ⓛW0.T0)) /2 width=1/ -HV0 -HT0 /3 width=1/ + ] +| #V0 #V1 #V2 #T0 #HV0 #HV01 #HT0 #HU + elim (IHVs … HT0) -IHVs -HT0 #HT0 + [ elim (tstc_inv_bind_appls_simple … HT0 ?) // + | @or_intror + @(cprs_trans … HU) -HU + @(cprs_strap1 … (ⓐV0.ⓓV2.T0)) /2 width=1/ -HV0 -HT0 /3 width=3/ +] +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 + ⒶV1s. ⓓV. T ≃ U ∨ L ⊢ ⓓV. ⒶV2s. T ➡* U. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lcpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lcpr.ma index 98ee18437..303be5997 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lcpr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lcpr.ma @@ -13,7 +13,6 @@ (**************************************************************************) include "Basic_2/grammar/tstc_tstc.ma". -include "Basic_2/reducibility/lcpr_cpr.ma". include "Basic_2/computation/cprs_cprs.ma". include "Basic_2/computation/csn_lift.ma". include "Basic_2/computation/csn_cpr.ma". 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 index 36e44ce6d..4ff8c039b 100644 --- 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 @@ -35,7 +35,8 @@ lemma csn_appl_appls_simple_tstc: ∀L,Vs,V,T1. L ⊢ ⬇* V → L ⊢ ⬇* T1 qed. *) lemma csn_applv_theta: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → - ∀V,T. L ⊢ ⬇* ⓓV. ⒶV2s. T → L ⊢ ⬇* V → L ⊢ ⬇* ⒶV1s. ⓓV. T. + ∀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 @@ -50,6 +51,23 @@ elim (cprs_fwd_theta_vector … (V2::V2s) … H1) -H1 /2 width=1/ -HV12s -HV12 | -H2 #H1 @(csn_cprs_trans … H) -H /2 width=1/ ] qed. + +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 // @@ -59,8 +77,8 @@ theorem csn_acr: acr cpr (eq …) (csn …) (λL,T. L ⊢ ⬇* T). | #L #V1 #V2 #HV12 #V #T #H #HVT @(csn_applv_theta … HV12) -HV12 // @(csn_abbr) // -| -| @csn_lift +| /2 width=1/ +| @csn_lift ] 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 75ec4c523..c4c44c9f3 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/tstc.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/tstc.ma @@ -105,7 +105,3 @@ qed. (**) (* remove from index *) lemma simple_tstc_repl_sn: ∀T1,T2. T1 ≃ T2 → 𝐒[T2] → 𝐒[T1]. /3 width=3/ qed-. - -(* Basic_1: removed theorems 2: - iso_flats_lref_bind_false iso_flats_flat_bind_false -*) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_cpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_cpr.ma index 236b953d8..92db70f0f 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_cpr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_cpr.ma @@ -35,7 +35,6 @@ lapply (tpss_tps … HT0) -HT0 #HT0 @ex2_1_intro [2: @(tpr_delta … HV12 HT1 HT0) | skip | /2 width=1/ ] (**) (* /3 width=5/ is too slow *) qed. - (* Basic_1: was only: pr2_head_1 *) lemma cpr_pair_sn: ∀I,L,V1,V2,T1,T2. L ⊢ V1 ➡ V2 → T1 ➡ T2 → L ⊢ ②{I} V1. T1 ➡ ②{I} V2. T2. -- 2.39.2