From f75be90562ddd964ef7ed43b956eb908f3133e3a Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 3 Nov 2011 22:45:59 +0000 Subject: [PATCH] - contex-free normal forms started - final definition for context-sensitive reduction on local environments - some refactoring --- .../contribs/lambda_delta/Basic_2/notation.ma | 34 ++++- .../{reduction => reducibility}/cpr.ma | 2 +- .../{reduction => reducibility}/cpr_cpr.ma | 4 +- .../{reduction => reducibility}/cpr_lift.ma | 4 +- .../{reduction => reducibility}/cpr_ltpr.ma | 5 +- .../{reduction => reducibility}/lcpr.ma | 28 ++--- .../{reduction => reducibility}/ltpr.ma | 6 +- .../{reduction => reducibility}/ltpr_ldrop.ma | 4 +- .../lambda_delta/Basic_2/reducibility/tnf.ma | 105 ++++++++++++++++ .../{reduction => reducibility}/tpr.ma | 0 .../{reduction => reducibility}/tpr_lift.ma | 2 +- .../{reduction => reducibility}/tpr_tpr.ma | 2 +- .../{reduction => reducibility}/tpr_tpss.ma | 2 +- .../lambda_delta/Basic_2/reducibility/trf.ma | 119 ++++++++++++++++++ .../Basic_2/substitution/lift_lift.ma | 4 +- .../lambda_delta/Basic_2/unfold/ltpss.ma | 20 ++- .../lambda_delta/Basic_2/unfold/ltpss_tpss.ma | 2 +- .../contribs/lambda_delta/Ground_2/star.ma | 13 ++ .../lambda_delta/Ground_2/xoa.conf.xml | 4 +- .../contribs/lambda_delta/Ground_2/xoa.ma | 8 ++ .../lambda_delta/Ground_2/xoa_notation.ma | 6 + 21 files changed, 323 insertions(+), 51 deletions(-) rename matita/matita/contribs/lambda_delta/Basic_2/{reduction => reducibility}/cpr.ma (98%) rename matita/matita/contribs/lambda_delta/Basic_2/{reduction => reducibility}/cpr_cpr.ma (97%) rename matita/matita/contribs/lambda_delta/Basic_2/{reduction => reducibility}/cpr_lift.ma (97%) rename matita/matita/contribs/lambda_delta/Basic_2/{reduction => reducibility}/cpr_ltpr.ma (96%) rename matita/matita/contribs/lambda_delta/Basic_2/{reduction => reducibility}/lcpr.ma (64%) rename matita/matita/contribs/lambda_delta/Basic_2/{reduction => reducibility}/ltpr.ma (96%) rename matita/matita/contribs/lambda_delta/Basic_2/{reduction => reducibility}/ltpr_ldrop.ma (96%) create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf.ma rename matita/matita/contribs/lambda_delta/Basic_2/{reduction => reducibility}/tpr.ma (100%) rename matita/matita/contribs/lambda_delta/Basic_2/{reduction => reducibility}/tpr_lift.ma (99%) rename matita/matita/contribs/lambda_delta/Basic_2/{reduction => reducibility}/tpr_tpr.ma (99%) rename matita/matita/contribs/lambda_delta/Basic_2/{reduction => reducibility}/tpr_tpss.ma (99%) create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/reducibility/trf.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma index 4383616be..b0ac4ff32 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma @@ -100,7 +100,31 @@ notation "hvbox( L ⊢ break term 90 T1 break [ d , break e ] ≫* break T2 )" non associative with precedence 45 for @{ 'PSubstStar $L $T1 $d $e $T2 }. -(* Reduction ****************************************************************) +(* Reducibility *************************************************************) + +notation "hvbox( ℝ [ T ] )" + non associative with precedence 45 + for @{ 'Reducible $T }. + +notation "hvbox( L ⊢ ℝ [ T ] )" + non associative with precedence 45 + for @{ 'Reducible $L $T }. + +notation "hvbox( 𝕀 [ T ] )" + non associative with precedence 45 + for @{ 'NotReducible $T }. + +notation "hvbox( L ⊢ 𝕀 [ T ] )" + non associative with precedence 45 + for @{ 'NotReducible $L $T }. + +notation "hvbox( ℕ [ T ] )" + non associative with precedence 45 + for @{ 'Normal $T }. + +notation "hvbox( L ⊢ ℕ [ T ] )" + non associative with precedence 45 + for @{ 'Normal $L $T }. notation "hvbox( T1 ⇒ break T2 )" non associative with precedence 45 @@ -127,3 +151,11 @@ notation "hvbox( L ⊢ break term 90 T1 ⇒* break T2 )" notation "hvbox( L1 ⊢ ⇒* break L2 )" non associative with precedence 45 for @{ 'CPRedStar $L1 $L2 }. + +notation "hvbox( ⇓ T )" + non associative with precedence 45 + for @{ 'SN $T }. + +notation "hvbox( L ⊢ ⇓ T )" + non associative with precedence 45 + for @{ 'SN $L $T }. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr.ma similarity index 98% rename from matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr.ma rename to matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr.ma index e70b9c537..13a5ca150 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr.ma @@ -14,7 +14,7 @@ include "Basic_2/grammar/cl_shift.ma". include "Basic_2/unfold/tpss.ma". -include "Basic_2/reduction/tpr.ma". +include "Basic_2/reducibility/tpr.ma". (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr_cpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_cpr.ma similarity index 97% rename from matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr_cpr.ma rename to matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_cpr.ma index ff802bfb3..2f0e31391 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr_cpr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_cpr.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/reduction/tpr_tpr.ma". -include "Basic_2/reduction/cpr.ma". +include "Basic_2/reducibility/tpr_tpr.ma". +include "Basic_2/reducibility/cpr.ma". (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_lift.ma similarity index 97% rename from matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr_lift.ma rename to matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_lift.ma index 885670fb4..4c2101504 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr_lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_lift.ma @@ -13,8 +13,8 @@ (**************************************************************************) include "Basic_2/unfold/tpss_lift.ma". -include "Basic_2/reduction/tpr_lift.ma". -include "Basic_2/reduction/cpr.ma". +include "Basic_2/reducibility/tpr_lift.ma". +include "Basic_2/reducibility/cpr.ma". (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr_ltpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_ltpr.ma similarity index 96% rename from matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr_ltpr.ma rename to matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_ltpr.ma index 3f80fb59c..486c12ee0 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr_ltpr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_ltpr.ma @@ -12,15 +12,14 @@ (* *) (**************************************************************************) -include "Basic_2/reduction/tpr_tpss.ma". -include "Basic_2/reduction/cpr.ma". +include "Basic_2/reducibility/tpr_tpss.ma". +include "Basic_2/reducibility/cpr.ma". (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************) (* Unfold properties ********************************************************) (* Note: we could invoke tpss_weak_all instead of ltpr_fwd_length *) - (* Basic_1: was only: pr2_subst1 *) lemma cpr_tpss_ltpr: ∀L1,L2. L1 ⇒ L2 → ∀T1,T2. L2 ⊢ T1 ⇒ T2 → ∀d,e,U1. L1 ⊢ T1 [d, e] ≫* U1 → diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reduction/lcpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/lcpr.ma similarity index 64% rename from matita/matita/contribs/lambda_delta/Basic_2/reduction/lcpr.ma rename to matita/matita/contribs/lambda_delta/Basic_2/reducibility/lcpr.ma index 6e0920526..13545ad84 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reduction/lcpr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/lcpr.ma @@ -12,30 +12,26 @@ (* *) (**************************************************************************) -include "Basic_2/reduction/cpr.ma". +include "Basic_2/unfold/ltpss.ma". +include "Basic_2/reducibility/ltpr.ma". (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *************) -inductive lcpr: relation lenv ≝ -| lcpr_sort: lcpr (⋆) (⋆) -| lcpr_item: ∀K1,K2,I,V1,V2. - lcpr K1 K2 → K2 ⊢ V1 ⇒ V2 → lcpr (K1. 𝕓{I} V1) (K2. 𝕓{I} V2) (*𝕓*) +definition lcpr: relation lenv ≝ + λL1,L2. ∃∃L. L1 ⇒ L & L [0, |L|] ≫* L2 . interpretation "context-sensitive parallel reduction (environment)" 'CPRed L1 L2 = (lcpr L1 L2). -(* Basic inversion lemmas ***************************************************) - -fact lcpr_inv_item1_aux: ∀L1,L2. L1 ⊢ ⇒ L2 → ∀K1,I,V1. L1 = K1. 𝕓{I} V1 → - ∃∃K2,V2. K1 ⊢ ⇒ K2 & K2 ⊢ V1 ⇒ V2 & L2 = K2. 𝕓{I} V2. -#L1 #L2 * -L1 L2 -[ #K1 #I #V1 #H destruct -| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #L #J #W #H destruct - K1 I V1 /2 width=5/ -] -qed. +(* Basic properties *********************************************************) -lemma lcpr_inv_item1: ∀K1,I,V1,L2. K1. 𝕓{I} V1 ⊢ ⇒ L2 → - ∃∃K2,V2. K1 ⊢ ⇒ K2 & K2 ⊢ V1 ⇒ V2 & L2 = K2. 𝕓{I} V2. +lemma lcpr_refl: ∀L. L ⊢ ⇒ L. /2/ qed. + +(* Basic inversion lemmas ***************************************************) + +lemma lcpr_inv_atom1: ∀L2. ⋆ ⊢ ⇒ L2 → L2 = ⋆. +#L2 * #L #HL >(ltpr_inv_atom1 … HL) -HL #HL2 >(ltpss_inv_atom1 … HL2) -HL2 // +qed-. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reduction/ltpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr.ma similarity index 96% rename from matita/matita/contribs/lambda_delta/Basic_2/reduction/ltpr.ma rename to matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr.ma index b7a01f3df..ecb0ad08c 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reduction/ltpr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr.ma @@ -12,13 +12,13 @@ (* *) (**************************************************************************) -include "Basic_2/reduction/tpr.ma". +include "Basic_2/reducibility/tpr.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************) inductive ltpr: relation lenv ≝ -| ltpr_sort: ltpr (⋆) (⋆) -| ltpr_item: ∀K1,K2,I,V1,V2. +| ltpr_stom: ltpr (⋆) (⋆) +| ltpr_pair: ∀K1,K2,I,V1,V2. ltpr K1 K2 → V1 ⇒ V2 → ltpr (K1. 𝕓{I} V1) (K2. 𝕓{I} V2) (*𝕓*) . diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reduction/ltpr_ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_ldrop.ma similarity index 96% rename from matita/matita/contribs/lambda_delta/Basic_2/reduction/ltpr_ldrop.ma rename to matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_ldrop.ma index 956bf1871..485c00fd1 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reduction/ltpr_ldrop.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_ldrop.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/reduction/tpr_lift.ma". -include "Basic_2/reduction/ltpr.ma". +include "Basic_2/reducibility/tpr_lift.ma". +include "Basic_2/reducibility/ltpr.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf.ma new file mode 100644 index 000000000..5d55e2ae6 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf.ma @@ -0,0 +1,105 @@ +(**************************************************************************) +(* ___ *) +(* ||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/substitution/tps_lift.ma". +include "Basic_2/reducibility/trf.ma". +include "Basic_2/reducibility/tpr.ma". + +(* CONTEXT-FREE NORMAL TERMS ************************************************) + +definition tnf: term → Prop ≝ + NF … tpr (eq …). + +interpretation + "context-free normality (term)" + 'Normal T = (tnf T). + +(* Basic inversion lemmas ***************************************************) + +lemma tnf_inv_abst: ∀V,T. ℕ[𝕔{Abst}V.T] → ℕ[V] ∧ ℕ[T]. +#V1 #T1 #HVT1 @conj +[ #V2 #HV2 lapply (HVT1 (𝕔{Abst}V2.T1) ?) -HVT1 /2/ -HV2 #H destruct -V1 T1 // +| #T2 #HT2 lapply (HVT1 (𝕔{Abst}V1.T2) ?) -HVT1 /2/ -HT2 #H destruct -V1 T1 // +] +qed. + +lemma tnf_inv_appl: ∀V,T. ℕ[𝕔{Appl}V.T] → ∧∧ ℕ[V] & ℕ[T] & 𝕊[T]. +#V1 #T1 #HVT1 @and3_intro +[ #V2 #HV2 lapply (HVT1 (𝕔{Appl}V2.T1) ?) -HVT1 /2/ -HV2 #H destruct -V1 T1 // +| #T2 #HT2 lapply (HVT1 (𝕔{Appl}V1.T2) ?) -HVT1 /2/ -HT2 #H destruct -V1 T1 // +| generalize in match HVT1 -HVT1; elim T1 -T1 * // * #W1 #U1 #_ #_ #H + [ elim (lift_total V1 0 1) #V2 #HV12 + lapply (H (𝕔{Abbr}W1.𝕔{Appl}V2.U1) ?) -H /2/ -HV12 #H destruct + | lapply (H (𝕔{Abbr}V1.U1) ?) -H /2/ #H destruct +] +qed. + +axiom tnf_inv_abbr: ∀V,T. ℕ[𝕔{Abbr}V.T] → False. + +axiom tnf_inv_cast: ∀V,T. ℕ[𝕔{Cast}V.T] → False. + +(* Basic properties *********************************************************) + +lemma tpr_tif_eq: ∀T1,T2. T1 ⇒ T2 → 𝕀[T1] → T1 = T2. +#T1 #T2 #H elim H -T1 T2 +[ // +| * #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H + [ elim (tif_inv_appl … H) -H #HV1 #HT1 #_ + >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 // + | elim (tif_inv_cast … H) + ] +| #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #H + elim (tif_inv_appl … H) -H #_ #_ #H + elim (simple_inv_bind … H) +| * #V1 #V2 #T1 #T #T2 #_ #_ #HT2 #IHV1 #IHT1 #H + [ -HT2 IHV1 IHT1; elim (tif_inv_abbr … H) + | <(tps_inv_refl_SO2 … HT2 ?) -HT2 // + elim (tif_inv_abst … H) -H #HV1 #HT1 + >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 // + ] +| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H + elim (tif_inv_appl … H) -H #_ #_ #H + elim (simple_inv_bind … H) +| #V1 #T1 #T2 #T #_ #_ #_ #H + elim (tif_inv_abbr … H) +| #V1 #T1 #T #_ #_ #H + elim (tif_inv_cast … H) +] +qed. + +theorem tif_tnf: ∀T1. 𝕀[T1] → ℕ[T1]. +/2/ qed. + +(* Note: this property is unusual *) +theorem tnf_trf_false: ∀T1. ℝ[T1] → ℕ[T1] → False. +#T1 #H elim H -T1 +[ #V #T #_ #IHV #H elim (tnf_inv_abst … H) -H /2/ +| #V #T #_ #IHT #H elim (tnf_inv_abst … H) -H /2/ +| #V #T #_ #IHV #H elim (tnf_inv_appl … H) -H /2/ +| #V #T #_ #IHV #H elim (tnf_inv_appl … H) -H /2/ +| #V #T #H elim (tnf_inv_abbr … H) +| #V #T #H elim (tnf_inv_cast … H) +| #V #W #T #H elim (tnf_inv_appl … H) -H #_ #_ #H + elim (simple_inv_bind … H) +] +qed. + +theorem tnf_tif: ∀T1. ℕ[T1] → 𝕀[T1]. +/2/ qed. + +lemma tnf_abst: ∀V,T. ℕ[V] → ℕ[T] → ℕ[𝕔{Abst}V.T]. +/4 width=1/ qed. + +lemma tnf_appl: ∀V,T. ℕ[V] → ℕ[T] → 𝕊[T] → ℕ[𝕔{Appl}V.T]. +/4 width=1/ qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reduction/tpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/reduction/tpr.ma rename to matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reduction/tpr_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma similarity index 99% rename from matita/matita/contribs/lambda_delta/Basic_2/reduction/tpr_lift.ma rename to matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma index 7ebd4af8c..0c8235765 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reduction/tpr_lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "Basic_2/substitution/tps_lift.ma". -include "Basic_2/reduction/tpr.ma". +include "Basic_2/reducibility/tpr.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reduction/tpr_tpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpr.ma similarity index 99% rename from matita/matita/contribs/lambda_delta/Basic_2/reduction/tpr_tpr.ma rename to matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpr.ma index f13d6af31..4217ced9a 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reduction/tpr_tpr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpr.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/reduction/tpr_tpss.ma". +include "Basic_2/reducibility/tpr_tpss.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reduction/tpr_tpss.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpss.ma similarity index 99% rename from matita/matita/contribs/lambda_delta/Basic_2/reduction/tpr_tpss.ma rename to matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpss.ma index 30d7a4bb8..f640d1326 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reduction/tpr_tpss.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpss.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "Basic_2/unfold/ltpss_ltpss.ma". -include "Basic_2/reduction/ltpr_ldrop.ma". +include "Basic_2/reducibility/ltpr_ldrop.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/trf.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/trf.ma new file mode 100644 index 000000000..d0050452b --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/trf.ma @@ -0,0 +1,119 @@ +(**************************************************************************) +(* ___ *) +(* ||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/grammar/term_simple.ma". + +(* CONTEXT-FREE REDUCIBLE AND IRREDUCIBLE TERMS *****************************) + +(* reducible terms *) +inductive trf: term → Prop ≝ +| trf_abst_sn: ∀V,T. trf V → trf (𝕔{Abst} V. T) +| trf_abst_dx: ∀V,T. trf T → trf (𝕔{Abst} V. T) +| trf_appl_sn: ∀V,T. trf V → trf (𝕔{Appl} V. T) +| trf_appl_dx: ∀V,T. trf T → trf (𝕔{Appl} V. T) +| trf_abbr : ∀V,T. trf (𝕔{Abbr} V. T) +| trf_cast : ∀V,T. trf (𝕔{Cast} V. T) +| trf_beta : ∀V,W,T. trf (𝕔{Appl} V. 𝕔{Abst} W. T) +. + +interpretation + "context-free reducibility (term)" + 'Reducible T = (trf T). + +(* irreducible terms *) +definition tif: term → Prop ≝ + λT. ℝ[T] → False. + +interpretation + "context-free irreducibility (term)" + 'NotReducible T = (tif T). + +(* Basic inversion lemmas ***************************************************) + +fact trf_inv_atom_aux: ∀I,T. ℝ[T] → T = 𝕒{I} → False. +#I #T * -T +[ #V #T #_ #H destruct +| #V #T #_ #H destruct +| #V #T #_ #H destruct +| #V #T #_ #H destruct +| #V #T #H destruct +| #V #T #H destruct +| #V #W #T #H destruct +] +qed. + +lemma trf_inv_atom: ∀I. ℝ[𝕒{I}] → False. +/2/ qed. + +fact trf_inv_abst_aux: ∀W,U,T. ℝ[T] → T = 𝕔{Abst} W. U → ℝ[W] ∨ ℝ[U]. +#W #U #T * -T +[ #V #T #HV #H destruct -V T /2/ +| #V #T #HT #H destruct -V T /2/ +| #V #T #_ #H destruct +| #V #T #_ #H destruct +| #V #T #H destruct +| #V #T #H destruct +| #V #W0 #T #H destruct +] +qed. + +lemma trf_inv_abst: ∀V,T. ℝ[𝕔{Abst}V.T] → ℝ[V] ∨ ℝ[T]. +/2/ qed. + +fact trf_inv_appl_aux: ∀W,U,T. ℝ[T] → T = 𝕔{Appl} W. U → + ∨∨ ℝ[W] | ℝ[U] | (𝕊[U] → False). +#W #U #T * -T +[ #V #T #_ #H destruct +| #V #T #_ #H destruct +| #V #T #HV #H destruct -V T /2/ +| #V #T #HT #H destruct -V T /2/ +| #V #T #H destruct +| #V #T #H destruct +| #V #W0 #T #H destruct -V U + @or3_intro2 #H elim (simple_inv_bind … H) +] +qed. + +lemma trf_inv_appl: ∀W,U. ℝ[𝕔{Appl}W.U] → ∨∨ ℝ[W] | ℝ[U] | (𝕊[U] → False). +/2/ qed. + +lemma tif_inv_abbr: ∀V,T. 𝕀[𝕔{Abbr}V.T] → False. +/2/ qed. + +lemma tif_inv_abst: ∀V,T. 𝕀[𝕔{Abst}V.T] → 𝕀[V] ∧ 𝕀[T]. +/4/ qed. + +lemma tif_inv_appl: ∀V,T. 𝕀[𝕔{Appl}V.T] → ∧∧ 𝕀[V] & 𝕀[T] & 𝕊[T]. +#V #T #HVT @and3_intro /3/ +generalize in match HVT -HVT; elim T -T // +* // * #U #T #_ #_ #H elim (H ?) -H /2/ +qed. + +lemma tif_inv_cast: ∀V,T. 𝕀[𝕔{Cast}V.T] → False. +/2/ qed. + +(* Basic properties *********************************************************) + +lemma tif_atom: ∀I. 𝕀[𝕒{I}]. +/2/ qed. + +lemma tif_abst: ∀V,T. 𝕀[V] → 𝕀[T] → 𝕀[𝕔 {Abst}V.T]. +#V #T #HV #HT #H +elim (trf_inv_abst … H) -H /2/ +qed. + +lemma tif_appl: ∀V,T. 𝕀[V] → 𝕀[T] → 𝕊[T] → 𝕀[𝕔{Appl}V.T]. +#V #T #HV #HT #S #H +elim (trf_inv_appl … H) -H /2/ +qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma index 2f1e3ac3c..6feb72e03 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma @@ -69,7 +69,7 @@ theorem lift_div_le: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → ] qed. -theorem lift_mono: ∀d,e,T,U1. ↑[d,e] T ≡ U1 → ∀U2. ↑[d,e] T ≡ U2 → U1 = U2. +theorem lift_mono: ∀d,e,T,U1. ↑[d,e] T ≡ U1 → ∀U2. ↑[d,e] T ≡ U2 → U1 = U2. #d #e #T #U1 #H elim H -H d e T U1 [ #k #d #e #X #HX lapply (lift_inv_sort1 … HX) -HX // @@ -166,6 +166,6 @@ theorem lift_trans_ge: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → | #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hded elim (lift_inv_flat1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct -X; elim (IHV12 … HV20 ?) -IHV12 HV20 // - elim (IHT12 … HT20 ?) -IHT12 HT20 // /3 width=5/ (**) (* just /3 width=5/ crashes *) + elim (IHT12 … HT20 ?) -IHT12 HT20 // /3 width=5/ ] qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss.ma index eb7803efe..582c2caa0 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss.ma @@ -52,20 +52,17 @@ lemma ltpss_inv_atom1: ∀d,e,L2. ⋆ [d, e] ≫* L2 → L2 = ⋆. #L #L2 #_ #HL2 #IHL destruct -L >(ltps_inv_atom1 … HL2) -HL2 // qed. -(* -fact ltps_inv_atom2_aux: ∀d,e,L1,L2. - L1 [d, e] ≫ L2 → L2 = ⋆ → L1 = ⋆. -#d #e #L1 #L2 * -d e L1 L2 -[ // -| #L #I #V #H destruct -| #L1 #L2 #I #V1 #V2 #e #_ #_ #H destruct -| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H destruct -] + +fact ltpss_inv_atom2_aux: ∀d,e,L1,L2. + L1 [d, e] ≫* L2 → L2 = ⋆ → L1 = ⋆. +#d #e #L1 #L2 #H @(ltpss_ind … H) -L2 // +#L2 #L #_ #HL2 #IHL2 #H destruct -L; +lapply (ltps_inv_atom2 … HL2) -HL2 /2/ qed. -lemma ldrop_inv_atom2: ∀d,e,L1. L1 [d, e] ≫ ⋆ → L1 = ⋆. +lemma ltpss_inv_atom2: ∀d,e,L1. L1 [d, e] ≫* ⋆ → L1 = ⋆. /2 width=5/ qed. - +(* fact ltps_inv_tps22_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → d = 0 → 0 < e → ∀K2,I,V2. L2 = K2. 𝕓{I} V2 → ∃∃K1,V1. K1 [0, e - 1] ≫ K2 & @@ -103,5 +100,4 @@ lemma ltps_inv_tps12: ∀L1,K2,I,V2,d,e. L1 [d, e] ≫ K2. 𝕓{I} V2 → 0 < d K2 ⊢ V1 [d - 1, e] ≫ V2 & L1 = K1. 𝕓{I} V1. /2/ qed. - *) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_tpss.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_tpss.ma index b855d9f43..367093b0a 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_tpss.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_tpss.ma @@ -143,7 +143,7 @@ qed. (* Advanced forward lemmas **************************************************) -lemma ltpss_fwd_tpsa21: ∀e,K1,I,V1,L2. 0 < e → K1. 𝕓{I} V1 [0, e] ≫* L2 → +lemma ltpss_fwd_tpss21: ∀e,K1,I,V1,L2. 0 < e → K1. 𝕓{I} V1 [0, e] ≫* L2 → ∃∃K2,V2. K1 [0, e - 1] ≫* K2 & K1 ⊢ V1 [0, e - 1] ≫* V2 & L2 = K2. 𝕓{I} V2. #e #K1 #I #V1 #L2 #He #H @(ltpss_ind … H) -L2 diff --git a/matita/matita/contribs/lambda_delta/Ground_2/star.ma b/matita/matita/contribs/lambda_delta/Ground_2/star.ma index ffc5ab1ac..e68ab1785 100644 --- a/matita/matita/contribs/lambda_delta/Ground_2/star.ma +++ b/matita/matita/contribs/lambda_delta/Ground_2/star.ma @@ -107,3 +107,16 @@ lemma TC_star_ind: ∀A,R. reflexive A R → ∀a1. ∀P:A→Prop. ∀a2. TC … R a1 a2 → P a2. #A #R #H #a1 #P #Ha1 #IHa1 #a2 #Ha12 elim Ha12 -Ha12 a2 /3/ qed. + +definition NF: ∀A. relation A → relation A → A → Prop ≝ + λA,R,S,a1. ∀a2. R a1 a2 → S a1 a2. + +inductive SN (A) (R,S:relation A): A → Prop ≝ +| SN_intro: ∀a1. (∀a2. R a1 a2 → (S a1 a2 → False) → SN A R S a2) → SN A R S a1 +. + +lemma NF_to_SN: ∀A,R,S,a. NF A R S a → SN A R S a. +#A #R #S #a1 #Ha1 +@SN_intro #a2 #HRa12 #HSa12 +elim (HSa12 ?) -HSa12 /2/ +qed. diff --git a/matita/matita/contribs/lambda_delta/Ground_2/xoa.conf.xml b/matita/matita/contribs/lambda_delta/Ground_2/xoa.conf.xml index 8634d7256..ac5635c7c 100644 --- a/matita/matita/contribs/lambda_delta/Ground_2/xoa.conf.xml +++ b/matita/matita/contribs/lambda_delta/Ground_2/xoa.conf.xml @@ -10,7 +10,7 @@ -->
- contribs/lambda_delta/Ground-2/ + contribs/lambda_delta/Ground_2/ xoa xoa_notation basics/pts.ma @@ -29,8 +29,6 @@ 7 6 3 4 -
diff --git a/matita/matita/contribs/lambda_delta/Ground_2/xoa.ma b/matita/matita/contribs/lambda_delta/Ground_2/xoa.ma index 2b7af4503..2b75c902d 100644 --- a/matita/matita/contribs/lambda_delta/Ground_2/xoa.ma +++ b/matita/matita/contribs/lambda_delta/Ground_2/xoa.ma @@ -141,3 +141,11 @@ inductive or4 (P0,P1,P2,P3:Prop) : Prop ≝ interpretation "multiple disjunction connective (4)" 'Or P0 P1 P2 P3 = (or4 P0 P1 P2 P3). +(* multiple conjunction connective (3) *) + +inductive and3 (P0,P1,P2:Prop) : Prop ≝ + | and3_intro: P0 → P1 → P2 → and3 ? ? ? +. + +interpretation "multiple conjunction connective (3)" 'And P0 P1 P2 = (and3 P0 P1 P2). + diff --git a/matita/matita/contribs/lambda_delta/Ground_2/xoa_notation.ma b/matita/matita/contribs/lambda_delta/Ground_2/xoa_notation.ma index 47e3268b4..80f9762a6 100644 --- a/matita/matita/contribs/lambda_delta/Ground_2/xoa_notation.ma +++ b/matita/matita/contribs/lambda_delta/Ground_2/xoa_notation.ma @@ -156,3 +156,9 @@ notation "hvbox(∨∨ term 29 P0 break | term 29 P1 break | term 29 P2 break | non associative with precedence 30 for @{ 'Or $P0 $P1 $P2 $P3 }. +(* multiple conjunction connective (3) *) + +notation "hvbox(∧∧ term 34 P0 break & term 34 P1 break & term 34 P2)" + non associative with precedence 35 + for @{ 'And $P0 $P1 $P2 }. + -- 2.39.2