From 3443885ee60fbcb90e2d106e67d3b7f7e3c59bad Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 21 Feb 2012 18:30:32 +0000 Subject: [PATCH] - more properties on strongly normalizing terms ... --- .../Basic_2/computation/csn_cr.ma | 14 +++++ .../Basic_2/computation/csn_lcpr.ma | 28 ++++++++++ .../Basic_2/computation/csn_lift.ma | 14 +---- .../Basic_2/grammar/{thom.ma => tshf.ma} | 32 +++++------ .../lambda_delta/Basic_2/grammar/tstc.ma | 54 ++++++++++++++----- .../Basic_2/reducibility/twhnf.ma | 24 ++++----- 6 files changed, 113 insertions(+), 53 deletions(-) rename matita/matita/contribs/lambda_delta/Basic_2/grammar/{thom.ma => tshf.ma} (71%) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.ma index e71d2bd3e..81c179293 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.ma @@ -20,6 +20,20 @@ include "Basic_2/computation/csn_vector.ma". (* 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. + 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/ 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 77ae2f9db..98ee18437 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 @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +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". @@ -117,3 +118,30 @@ qed. lemma csn_appl_theta: ∀V1,V2. ⇧[0, 1] V1 ≡ V2 → ∀L,V,T. L ⊢ ⬇* ⓓV. ⓐV2. T → L ⊢ ⬇* ⓐV1. ⓓV. T. /2 width=5/ qed. + +(* Basic_1: was only: sn3_appl_appl *) +lemma csn_appl_simple_tstc: ∀L,V. L ⊢ ⬇* V → ∀T1. + L ⊢ ⬇* T1 → + (∀T2. L ⊢ T1 ➡* T2 → (T1 ≃ T2 → False) → L ⊢ ⬇* ⓐV. T2) → + 𝐒[T1] → L ⊢ ⬇* ⓐV. T1. +#L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #H @(csn_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1 +@csn_intro #X #HL #H +elim (cpr_inv_appl1_simple … HL ?) -HL // +#V0 #T0 #HLV0 #HLT10 #H0 destruct +elim (eq_false_inv_tpair_sn … H) -H +[ -IHT1 #HV0 + @(csn_cpr_trans … (ⓐV0.T1)) /2 width=1/ -HLT10 + @IHV -IHV // -H1T1 -H3T1 /2 width=1/ -HV0 + #T2 #HLT12 #HT12 + @(csn_cpr_trans … (ⓐV.T2)) /2 width=1/ -HLV0 + @H2T1 -H2T1 // -HLT12 /2 width=1/ +| -IHV -H1T1 -HLV0 * #H #H1T10 destruct + elim (tstc_dec T1 T0) #H2T10 + [ @IHT1 -IHT1 // /2 width=1/ -H1T10 /2 width=3/ -H3T1 + #T2 #HLT02 #HT02 + @H2T1 -H2T1 /2 width=3/ -HLT10 -HLT02 /3 width=3/ + | -IHT1 -H3T1 -H1T10 + @H2T1 -H2T1 /2 width=1/ + ] +] +qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lift.ma index de29660f0..1326a8bb4 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lift.ma @@ -78,7 +78,6 @@ elim (eq_false_inv_tpair_sn … H2) -H2 ] qed. -(* Basic_1: was only: sn3_appl_appl *) lemma csn_appl_simple: ∀L,V. L ⊢ ⬇* V → ∀T1. (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → False) → L ⊢ ⬇* ⓐV. T2) → 𝐒[T1] → L ⊢ ⬇* ⓐV. T1. @@ -92,19 +91,8 @@ elim (eq_false_inv_tpair_dx … H2) -H2 @IHT1 -IHT1 // /2 width=1/ | -HLT10 * #H #HV0 destruct @IHV -IHV // -HT1 /2 width=1/ -HV0 - #T2 #HLT02 #HT02 + #T2 #HLT02 #HT02 @(csn_cpr_trans … (ⓐV.T2)) /2 width=1/ -HLV0 @IHT1 -IHT1 // -HLT02 /2 width=1/ ] qed. - -(* Basic_1: was only: sn3_appl_appls *) -lemma csn_appl_appls_simple: ∀L,V. L ⊢ ⬇* V → ∀Vs,T1. - (∀T2. L ⊢ ⒶVs.T1 ➡ T2 → (ⒶVs.T1 = T2 → False) → L ⊢ ⬇* ⓐV. T2) → - 𝐒[T1] → L ⊢ ⬇* ⓐV. ⒶVs. T1. -#L #V #HV #Vs elim Vs -Vs -[ @csn_appl_simple // -| #V0 #Vs #_ #T1 #HT1 #_ - @csn_appl_simple // -HV @HT1 -] -qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/tshf.ma similarity index 71% rename from matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma rename to matita/matita/contribs/lambda_delta/Basic_2/grammar/tshf.ma index 5b90bd1d3..364a530e1 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/tshf.ma @@ -14,42 +14,42 @@ include "Basic_2/grammar/term_simple.ma". -(* HOMOMORPHIC TERMS ********************************************************) +(* SAME HEAD TERM FORMS *****************************************************) -inductive thom: relation term ≝ - | thom_atom: ∀I. thom (⓪{I}) (⓪{I}) - | thom_abst: ∀V1,V2,T1,T2. thom (ⓛV1. T1) (ⓛV2. T2) - | thom_appl: ∀V1,V2,T1,T2. thom T1 T2 → 𝐒[T1] → 𝐒[T2] → - thom (ⓐV1. T1) (ⓐV2. T2) +inductive tshf: relation term ≝ + | tshf_atom: ∀I. tshf (⓪{I}) (⓪{I}) + | tshf_abst: ∀V1,V2,T1,T2. tshf (ⓛV1. T1) (ⓛV2. T2) + | tshf_appl: ∀V1,V2,T1,T2. tshf T1 T2 → 𝐒[T1] → 𝐒[T2] → + tshf (ⓐV1. T1) (ⓐV2. T2) . -interpretation "homomorphic (term)" 'napart T1 T2 = (thom T1 T2). +interpretation "same head form (term)" 'napart T1 T2 = (tshf T1 T2). (* Basic properties *********************************************************) -lemma thom_sym: ∀T1,T2. T1 ≈ T2 → T2 ≈ T1. +lemma tshf_sym: ∀T1,T2. T1 ≈ T2 → T2 ≈ T1. #T1 #T2 #H elim H -T1 -T2 /2 width=1/ qed. -lemma thom_refl2: ∀T1,T2. T1 ≈ T2 → T2 ≈ T2. +lemma tshf_refl2: ∀T1,T2. T1 ≈ T2 → T2 ≈ T2. #T1 #T2 #H elim H -T1 -T2 // /2 width=1/ qed. -lemma thom_refl1: ∀T1,T2. T1 ≈ T2 → T1 ≈ T1. +lemma tshf_refl1: ∀T1,T2. T1 ≈ T2 → T1 ≈ T1. /3 width=2/ qed. -lemma simple_thom_repl_dx: ∀T1,T2. T1 ≈ T2 → 𝐒[T1] → 𝐒[T2]. +lemma simple_tshf_repl_dx: ∀T1,T2. T1 ≈ T2 → 𝐒[T1] → 𝐒[T2]. #T1 #T2 #H elim H -T1 -T2 // #V1 #V2 #T1 #T2 #H elim (simple_inv_bind … H) qed. (**) (* remove from index *) -lemma simple_thom_repl_sn: ∀T1,T2. T1 ≈ T2 → 𝐒[T2] → 𝐒[T1]. +lemma simple_tshf_repl_sn: ∀T1,T2. T1 ≈ T2 → 𝐒[T2] → 𝐒[T1]. /3 width=3/ qed-. (* Basic inversion lemmas ***************************************************) -fact thom_inv_bind1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = ⓑ{I}W1.U1 → +fact tshf_inv_bind1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = ⓑ{I}W1.U1 → ∃∃W2,U2. I = Abst & T2 = ⓛW2. U2. #T1 #T2 * -T1 -T2 [ #J #I #W1 #U1 #H destruct @@ -58,11 +58,11 @@ fact thom_inv_bind1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = ⓑ{I}W1.U1 ] qed. -lemma thom_inv_bind1: ∀I,W1,U1,T2. ⓑ{I}W1.U1 ≈ T2 → +lemma tshf_inv_bind1: ∀I,W1,U1,T2. ⓑ{I}W1.U1 ≈ T2 → ∃∃W2,U2. I = Abst & T2 = ⓛW2. U2. /2 width=5/ qed-. -fact thom_inv_flat1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = ⓕ{I}W1.U1 → +fact tshf_inv_flat1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = ⓕ{I}W1.U1 → ∃∃W2,U2. U1 ≈ U2 & 𝐒[U1] & 𝐒[U2] & I = Appl & T2 = ⓐW2. U2. #T1 #T2 * -T1 -T2 @@ -72,7 +72,7 @@ fact thom_inv_flat1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = ⓕ{I}W1.U1 ] qed. -lemma thom_inv_flat1: ∀I,W1,U1,T2. ⓕ{I}W1.U1 ≈ T2 → +lemma tshf_inv_flat1: ∀I,W1,U1,T2. ⓕ{I}W1.U1 ≈ T2 → ∃∃W2,U2. U1 ≈ U2 & 𝐒[U1] & 𝐒[U2] & I = Appl & T2 = ⓐW2. U2. /2 width=4/ 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 26bb95386..9c91d59f9 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/tstc.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/tstc.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/grammar/term.ma". +include "Basic_2/grammar/term_simple.ma". (* SAME TOP TERM CONSTRUCTOR ************************************************) @@ -23,17 +23,6 @@ inductive tstc: relation term ≝ interpretation "same top constructor (term)" 'Iso T1 T2 = (tstc T1 T2). -(* Basic properties *********************************************************) - -(* Basic_1: was: iso_refl *) -lemma tstc_refl: ∀T. T ≃ T. -#T elim T -T // -qed. - -lemma tstc_sym: ∀T1,T2. T1 ≃ T2 → T2 ≃ T1. -#T1 #T2 #H elim H -T1 -T2 // -qed. - (* Basic inversion lemmas ***************************************************) fact tstc_inv_atom1_aux: ∀T1,T2. T1 ≃ T2 → ∀I. T1 = ⓪{I} → T2 = ⓪{I}. @@ -78,6 +67,47 @@ lemma tstc_inv_pair2: ∀I,T1,W2,U2. T1 ≃ ②{I}W2.U2 → ∃∃W1,U1. T1 = ②{I}W1. U1. /2 width=5/ qed-. +(* Basic properties *********************************************************) + +(* Basic_1: was: iso_refl *) +lemma tstc_refl: ∀T. T ≃ T. +#T elim T -T // +qed. + +lemma tstc_sym: ∀T1,T2. T1 ≃ T2 → T2 ≃ T1. +#T1 #T2 #H elim H -T1 -T2 // +qed. + +lemma tstc_dec: ∀T1,T2. Decidable (T1 ≃ T2). +* #I1 [2: #V1 #T1 ] * #I2 [2,4: #V2 #T2 ] +[ elim (item2_eq_dec I1 I2) #HI12 + [ destruct /2 width=1/ + | @or_intror #H + elim (tstc_inv_pair1 … H) -H #V #T #H destruct /2 width=1/ + ] +| @or_intror #H + lapply (tstc_inv_atom1 … H) -H #H destruct +| @or_intror #H + lapply (tstc_inv_atom2 … H) -H #H destruct +| elim (item0_eq_dec I1 I2) #HI12 + [ destruct /2 width=1/ + | @or_intror #H + lapply (tstc_inv_atom2 … H) -H #H destruct /2 width=1/ + ] +] +qed. + +axiom simple_inv_pair: ∀I,V,T. 𝐒[②{I}V.T] → ∃J. I = Flat2 J. + +lemma simple_tstc_repl_dx: ∀T1,T2. T1 ≃ T2 → 𝐒[T1] → 𝐒[T2]. +#T1 #T2 * -T1 -T2 // +#I #V1 #V2 #T1 #T2 #H +elim (simple_inv_pair … H) -H #J #H destruct // +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/twhnf.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/twhnf.ma index 2497ea273..90598b1e7 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/twhnf.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/twhnf.ma @@ -12,12 +12,12 @@ (* *) (**************************************************************************) -include "Basic_2/grammar/thom.ma". +include "Basic_2/grammar/tshf.ma". include "Basic_2/reducibility/tpr.ma". (* CONTEXT-FREE WEAK HEAD NORMAL TERMS **************************************) -definition twhnf: predicate term ≝ NF … tpr thom. +definition twhnf: predicate term ≝ NF … tpr tshf. interpretation "context-free weak head normality (term)" @@ -25,32 +25,32 @@ interpretation (* Basic inversion lemmas ***************************************************) -lemma twhnf_inv_thom: ∀T. 𝐖𝐇𝐍[T] → T ≈ T. +lemma twhnf_inv_tshf: ∀T. 𝐖𝐇𝐍[T] → T ≈ T. normalize /2 width=1/ qed-. (* Basic properties *********************************************************) -lemma tpr_thom: ∀T1,T2. T1 ➡ T2 → T1 ≈ T1 → T1 ≈ T2. +lemma tpr_tshf: ∀T1,T2. T1 ➡ T2 → T1 ≈ T1 → T1 ≈ T2. #T1 #T2 #H elim H -T1 -T2 // [ #I #V1 #V2 #T1 #T2 #_ #_ #_ #IHT12 #H - elim (thom_inv_flat1 … H) -H #W2 #U2 #HT1U2 #HT1 #_ #H1 #H2 destruct + elim (tshf_inv_flat1 … H) -H #W2 #U2 #HT1U2 #HT1 #_ #H1 #H2 destruct lapply (IHT12 HT1U2) -IHT12 -HT1U2 #HUT2 - lapply (simple_thom_repl_dx … HUT2 HT1) /2 width=1/ + lapply (simple_tshf_repl_dx … HUT2 HT1) /2 width=1/ | #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #H - elim (thom_inv_flat1 … H) -H #W2 #U2 #_ #H + elim (tshf_inv_flat1 … H) -H #W2 #U2 #_ #H elim (simple_inv_bind … H) | #I #V1 #V2 #T1 #T #T2 #_ #_ #_ #_ #_ #H - elim (thom_inv_bind1 … H) -H #W2 #U2 #H destruct // + elim (tshf_inv_bind1 … H) -H #W2 #U2 #H destruct // | #V2 #V1 #V #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H - elim (thom_inv_flat1 … H) -H #U1 #U2 #_ #H + elim (tshf_inv_flat1 … H) -H #U1 #U2 #_ #H elim (simple_inv_bind … H) | #V #T #T1 #T2 #_ #_ #_ #H - elim (thom_inv_bind1 … H) -H #W2 #U2 #H destruct + elim (tshf_inv_bind1 … H) -H #W2 #U2 #H destruct | #V #T1 #T2 #_ #_ #H - elim (thom_inv_flat1 … H) -H #W2 #U2 #_ #_ #_ #H destruct + elim (tshf_inv_flat1 … H) -H #W2 #U2 #_ #_ #_ #H destruct ] qed. -lemma twhnf_thom: ∀T. T ≈ T → 𝐖𝐇𝐍[T]. +lemma twhnf_tshf: ∀T. T ≈ T → 𝐖𝐇𝐍[T]. /2 width=1/ qed. -- 2.39.2