From bbac36729dab046d61019081c1523af06d876103 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 14 Mar 2012 15:39:49 +0000 Subject: [PATCH] - property S4 of strongly normalizing term proved! --- .../contribs/lambda_delta/basic_2/basic_1.txt | 6 +---- .../lambda_delta/basic_2/computation/cprs.ma | 4 +-- .../basic_2/computation/cprs_lift.ma | 19 ++++++++++++++ .../basic_2/computation/cprs_tstc.ma | 12 +++++++++ .../basic_2/computation/cprs_tstc_vector.ma | 25 +++++++++++++++++++ .../lambda_delta/basic_2/computation/csn.ma | 5 ++-- .../basic_2/computation/csn_lcpr_vector.ma | 23 ++++++++++++++++- 7 files changed, 84 insertions(+), 10 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 b360bb20d..5370377e6 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt +++ b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt @@ -250,11 +250,9 @@ pr2/clen pr2_gen_ctail pr2/fwd pr2_gen_void pr2/props pr2_ctail pr2/subst1 pr2_gen_cabbr - -pr3/fwd pr3_gen_lref pr3/fwd pr3_gen_void -pr3/fwd pr3_gen_bind pr3/pr1 pr3_pr1 + pr3/pr3 pr3_strip pr3/props pr3_thin_dx pr3/props pr3_head_1 @@ -270,8 +268,6 @@ sn3/props sn3_shift sn3/props sn3_change sn3/props sn3_gen_def sn3/props sn3_cdelta -sn3/props sn3_appl_lref -sn3/props sn3_appl_abbr sn3/props sn3_appl_appls sn3/props sn3_appls_lref sn3/props sns3_lifts 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 ed6ee27e3..a91c9d8b5 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma @@ -82,7 +82,7 @@ elim (cpr_inv_cast1 … HU2) -HU2 /3 width=3/ * #W2 #T2 #HW2 #HT2 #H destruct /4 width=5/ qed-. -(* Basic_1: removed theorems 5: - clear_pr3_trans pr3_cflat +(* 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_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma index 5ee21be85..32dcb2ce9 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma @@ -19,6 +19,25 @@ include "basic_2/computation/cprs.ma". (* Advanced inversion lemmas ************************************************) +(* Basic_1: was: pr3_gen_lref *) +lemma cprs_inv_lref1: ∀L,T2,i. L ⊢ #i ➡* T2 → + T2 = #i ∨ + ∃∃K,V1,T1. ⇩[0, i] L ≡ K. ⓓV1 & + K ⊢ V1 ➡* T1 & + ⇧[0, i + 1] T1 ≡ T2 & + i < |L|. +#L #T2 #i #H @(cprs_ind … H) -T2 /2 width=1/ +#T #T2 #_ #HT2 * +[ #H destruct + elim (cpr_inv_lref1 … HT2) -HT2 /2 width=1/ + * #K #V1 #T1 #HLK #HVT1 #HT12 #Hi + @or_intror @(ex4_3_intro … HLK … HT12) // /3 width=3/ (**) (* explicit constructors *) +| * #K #V1 #T1 #HLK #HVT1 #HT1 #Hi + lapply (ldrop_fwd_ldrop2 … HLK) #H0LK + elim (cpr_inv_lift … H0LK … HT1 … HT2) -H0LK -T /4 width=6/ +] +qed-. + (* Basic_1: was: pr3_gen_abst *) lemma cprs_inv_abst1: ∀I,W,L,V1,T1,U2. L ⊢ ⓛV1. T1 ➡* U2 → ∃∃V2,T2. L ⊢ V1 ➡* V2 & L. ⓑ{I} W ⊢ T1 ➡* T2 & 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 6969f7c60..c7f49d1cf 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 @@ -35,6 +35,18 @@ elim (cprs_inv_appl1 … H) -H * ] qed-. +(* Note: probably this is an inversion lemma *) +lemma cprs_fwd_delta: ∀L,K,V1,i. ⇩[0, i] L ≡ K. ⓓV1 → + ∀V2. ⇧[0, i + 1] V1 ≡ V2 → + ∀U. L ⊢ #i ➡* U → + #i ≃ U ∨ L ⊢ V2 ➡* U. +#L #K #V1 #i #HLK #V2 #HV12 #U #H +elim (cprs_inv_lref1 … H) -H /2 width=1/ +* #K0 #V0 #U0 #HLK0 #HVU0 #HU0 #_ +lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H destruct +lapply (ldrop_fwd_ldrop2 … HLK) -HLK /3 width=9/ +qed-. + lemma cprs_fwd_theta: ∀L,V1,V,T,U. L ⊢ ⓐV1. ⓓV. T ➡* U → ∀V2. ⇧[0, 1] V1 ≡ V2 → ⓐV1. ⓓV. T ≃ U ∨ L ⊢ ⓓV. ⓐV2. 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 4b65a08df..d12a9f498 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 @@ -44,6 +44,31 @@ elim (cprs_inv_appl1 … H) -H * ] qed-. +lemma cprs_fwd_delta_vector: ∀L,K,V1,i. ⇩[0, i] L ≡ K. ⓓV1 → + ∀V2. ⇧[0, i + 1] V1 ≡ V2 → + ∀Vs,U. L ⊢ ⒶVs.#i ➡* U → + ⒶVs.#i ≃ U ∨ L ⊢ ⒶVs.V2 ➡* U. +#L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs /2 width=4 by cprs_fwd_delta/ +#V #Vs #IHVs #U #H -K -V1 +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 -i (**) (* explicit constructor *) + @(cprs_trans … HU) -U + @(cprs_strap1 … (ⓐV0.ⓛW0.T0)) [ /2 width=1/ ] -V -V2 -Vs /3 width=1/ + ] +| #V0 #V1 #V3 #T0 #HV0 #HV01 #HT0 #HU + elim (IHVs … HT0) -IHVs -HT0 #HT0 + [ elim (tstc_inv_bind_appls_simple … HT0 ?) // + | @or_intror -i (**) (* explicit constructor *) + @(cprs_trans … HU) -U + @(cprs_strap1 … (ⓐV0.ⓓV3.T0)) [ /2 width=1/ ] -V -V2 -Vs /3 width=3/ + ] +] +qed-. + (* Basic_1: was: pr3_iso_appls_abbr *) lemma cprs_fwd_theta_vector: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → ∀V,T,U. L ⊢ ⒶV1s. ⓓ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 2890fb9b1..5552c6fb7 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma @@ -82,7 +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 7: - sn3_gen_cflat sn3_cflat sn3_appl_cast sn3_appl_beta +(* Basic_1: removed theorems 9: + 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 *) 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 c185ef2c6..5f5465b4f 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 @@ -52,6 +52,27 @@ lapply (csn_fwd_flat_dx … H1T) #H2T ] 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 → @@ -93,7 +114,7 @@ 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.39.2