From 7cf0b6c720e4d7fa05dd25ec0ad0478c0802ba67 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 15 Mar 2012 18:00:48 +0000 Subject: [PATCH] - lambda_delta: strong normalization of simply typed terms closed! - star.ma: transitive closure: support for reverse elimination --- .../lambda_delta/basic_2/computation/cprs.ma | 8 +++- .../basic_2/computation/cprs_tstc_vector.ma | 1 + .../basic_2/computation/csn_cpr_vector.ma | 26 +++++++++++++ .../basic_2/computation/csn_tstc_vector.ma | 38 ++++++++----------- .../basic_2/computation/csn_vector.ma | 33 ++-------------- .../basic_2/grammar/term_vector.ma | 8 +++- matita/matita/lib/basics/star.ma | 38 +++++++++++++++++++ 7 files changed, 96 insertions(+), 56 deletions(-) create mode 100644 matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr_vector.ma 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 4341a5a94..5ea230f9b 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma @@ -28,12 +28,16 @@ interpretation "context-sensitive parallel computation (term)" lemma cprs_ind: ∀L,T1. ∀R:predicate term. R T1 → (∀T,T2. L ⊢ T1 ➡* T → L ⊢ T ➡ T2 → R T → R T2) → ∀T2. L ⊢ T1 ➡* T2 → R T2. -#L #T1 #R #HT1 #IHT1 #T2 #HT12 @(TC_star_ind … HT1 IHT1 … HT12) // +#L #T1 #R #HT1 #IHT1 #T2 #HT12 +@(TC_star_ind … HT1 IHT1 … HT12) // qed-. -axiom cprs_ind_dx: ∀L,T2. ∀R:predicate term. R T2 → +lemma cprs_ind_dx: ∀L,T2. ∀R:predicate term. R T2 → (∀T1,T. L ⊢ T1 ➡ T → L ⊢ T ➡* T2 → R T → R T1) → ∀T1. L ⊢ T1 ➡* T2 → R T1. +#L #T2 #R #HT2 #IHT2 #T1 #HT12 +@(TC_star_ind_dx … HT2 IHT2 … HT12) // +qed-. (* Basic properties *********************************************************) 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 2f8486cc2..feaedbf76 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,7 @@ include "basic_2/computation/cprs_tstc.ma". (* Vector form of forward lemmas involving same top term constructor ********) +(* Basic_1: was just: nf2_iso_appls_lref *) 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 diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr_vector.ma new file mode 100644 index 000000000..375d645f2 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr_vector.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||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/csn_cpr.ma". +include "basic_2/computation/csn_vector.ma". + +(* Advanced forward lemmas **************************************************) + +lemma csn_fwd_applv: ∀L,T,Vs. L ⊢ ⬇* Ⓐ Vs. T → L ⊢ ⬇* Vs ∧ L ⊢ ⬇* T. +#L #T #Vs elim Vs -Vs /2 width=1/ +#V #Vs #IHVs #HVs +lapply (csn_fwd_pair_sn … HVs) #HV +lapply (csn_fwd_flat_dx … HVs) -HVs #HVs +elim (IHVs HVs) -IHVs -HVs /3 width=1/ +qed-. 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 index 00de73f52..3aa7170f5 100644 --- 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 @@ -28,11 +28,9 @@ lemma csn_applv_cnf: ∀L,T. 𝐒[T] → L ⊢ 𝐍[T] → #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 // -] +#X #H #H0 +lapply (cprs_fwd_cnf_vector … H) -H // -H1T -H2T #H +elim (H0 ?) -H0 // qed. (* Basic_1: was: sn3_appls_beta *) @@ -44,12 +42,10 @@ lemma csn_applv_beta: ∀L,W. L ⊢ ⬇* W → 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 // +#X #H #H0 +elim (cprs_fwd_beta_vector … H) -H #H +[ -H1T elim (H0 ?) -H0 // +| -H0 @(csn_cprs_trans … H1T) -H1T /2 width=1/ ] qed. @@ -64,12 +60,10 @@ lemma csn_applv_delta: ∀L,K,V1,i. ⇩[0, i] L ≡ K. ⓓV1 → 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 // + #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/ ] ] qed. @@ -102,12 +96,10 @@ lemma csn_applv_tau: ∀L,W. L ⊢ ⬇* W → 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 // +#X #H #H0 +elim (cprs_fwd_tau_vector … H) -H #H +[ -H1T elim (H0 ?) -H0 // +| -H0 @(csn_cprs_trans … H1T) -H1T /2 width=1/ ] 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 7dab76e23..a8663d8ba 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 @@ -17,41 +17,14 @@ include "basic_2/computation/csn.ma". (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERM VECTORS **********************) -inductive csnv (L:lenv): predicate (list term) ≝ -| csnv_nil: csnv L ◊ -| csn_cons: ∀Ts,T. L ⊢ ⬇* T → csnv L Ts → csnv L (T :: Ts) -. +definition csnv: lenv → predicate (list term) ≝ + λL. all … (csn L). 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 → - L ⊢ ⬇* U ∧ L ⊢ ⬇* Us. -#L #Ts * -Ts -[ #U #Us #H destruct -| #Ts #T #HT #HTs #U #Us #H destruct /2 width=1/ -] -qed. - lemma csnv_inv_cons: ∀L,T,Ts. L ⊢ ⬇* T :: Ts → L ⊢ ⬇* T ∧ L ⊢ ⬇* Ts. -/2 width=3/ qed-. - -include "basic_2/computation/csn_cpr.ma". - -lemma csn_fwd_applv: ∀L,T,Vs. L ⊢ ⬇* Ⓐ Vs. T → L ⊢ ⬇* Vs ∧ L ⊢ ⬇* T. -#L #T #Vs elim Vs -Vs /2 width=1/ -#V #Vs #IHVs #HVs -lapply (csn_fwd_pair_sn … HVs) #HV -lapply (csn_fwd_flat_dx … HVs) -HVs #HVs -elim (IHVs HVs) -IHVs -HVs /3 width=1/ -qed-. +normalize // qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/term_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/term_vector.ma index c2ad0f835..7b4923bbe 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/term_vector.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/term_vector.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "ground_2/list.ma". -include "basic_2/grammar/term.ma". +include "basic_2/grammar/term_simple.ma". (* TERMS ********************************************************************) @@ -25,3 +25,9 @@ let rec applv Vs T on Vs ≝ interpretation "application o vevtor (term)" 'SnApplV Vs T = (applv Vs T). + +(* properties concerning simple terms ***************************************) + +lemma applv_simple: ∀T,Vs. 𝐒[T] -> 𝐒[ⒶVs.T]. +#T * // +qed. diff --git a/matita/matita/lib/basics/star.ma b/matita/matita/lib/basics/star.ma index cae3766b1..bac2e771c 100644 --- a/matita/matita/lib/basics/star.ma +++ b/matita/matita/lib/basics/star.ma @@ -153,3 +153,41 @@ lemma TC_star_ind: ∀A,R. reflexive A R → ∀a1. ∀P:predicate A. ∀a2. TC … R a1 a2 → P a2. #A #R #H #a1 #P #Ha1 #IHa1 #a2 #Ha12 elim Ha12 -a2 /3 width=4/ qed. + +inductive TC_dx (A:Type[0]) (R:relation A): A → A → Prop ≝ + |inj_dx: ∀a,c. R a c → TC_dx A R a c + |step_dx : ∀a,b,c. R a b → TC_dx A R b c → TC_dx A R a c. + +lemma TC_dx_strap: ∀A. ∀R: relation A. + ∀a,b,c. TC_dx A R a b → R b c → TC_dx A R a c. +#A #R #a #b #c #Hab elim Hab -a -b /3 width=3/ +qed. + +lemma TC_to_TC_dx: ∀A. ∀R: relation A. + ∀a1,a2. TC … R a1 a2 → TC_dx … R a1 a2. +#A #R #a1 #a2 #Ha12 elim Ha12 -a2 /2 width=3/ +qed. + +lemma TC_dx_to_TC: ∀A. ∀R: relation A. + ∀a1,a2. TC_dx … R a1 a2 → TC … R a1 a2. +#A #R #a1 #a2 #Ha12 elim Ha12 -a1 -a2 /2 width=3/ +qed. + +fact TC_star_ind_dx_aux: ∀A,R. reflexive A R → + ∀a2. ∀P:predicate A. P a2 → + (∀a1,a. R a1 a → TC … R a a2 → P a → P a1) → + ∀a1,a. TC … R a1 a → a = a2 → P a1. +#A #R #HR #a2 #P #Ha2 #H #a1 #a #Ha1 +elim (TC_to_TC_dx ???? Ha1) -a1 -a +[ #a #c #Hac #H destruct /3 width=4/ +| #a #b #c #Hab #Hbc #IH #H destruct /3 width=4/ +] +qed-. + +lemma TC_star_ind_dx: ∀A,R. reflexive A R → + ∀a2. ∀P:predicate A. P a2 → + (∀a1,a. R a1 a → TC … R a a2 → P a → P a1) → + ∀a1. TC … R a1 a2 → P a1. +#A #R #HR #a2 #P #Ha2 #H #a1 #Ha12 +@(TC_star_ind_dx_aux … HR … Ha2 H … Ha12) // +qed-. -- 2.39.2