From: Ferruccio Guidi Date: Thu, 3 Nov 2011 22:45:59 +0000 (+0000) Subject: - contex-free normal forms started X-Git-Tag: make_still_working~2138 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f75be90562ddd964ef7ed43b956eb908f3133e3a;p=helm.git - contex-free normal forms started - final definition for context-sensitive reduction on local environments - some refactoring --- 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/reducibility/cpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr.ma new file mode 100644 index 000000000..13a5ca150 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr.ma @@ -0,0 +1,96 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cl_shift.ma". +include "Basic_2/unfold/tpss.ma". +include "Basic_2/reducibility/tpr.ma". + +(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************) + +(* Basic_1: includes: pr2_delta1 *) +definition cpr: lenv → relation term ≝ + λL,T1,T2. ∃∃T. T1 ⇒ T & L ⊢ T [0, |L|] ≫* T2. + +interpretation + "context-sensitive parallel reduction (term)" + 'PRed L T1 T2 = (cpr L T1 T2). + +(* Basic properties *********************************************************) + +(* Basic_1: was by definition: pr2_free *) +lemma cpr_pr: ∀T1,T2. T1 ⇒ T2 → ∀L. L ⊢ T1 ⇒ T2. +/2/ qed. + +lemma cpr_tpss: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫* T2 → L ⊢ T1 ⇒ T2. +/3 width=5/ qed. + +lemma cpr_refl: ∀L,T. L ⊢ T ⇒ T. +/2/ qed. + +(* Note: new property *) +(* Basic_1: was only: pr2_thin_dx *) +lemma cpr_flat: ∀I,L,V1,V2,T1,T2. + L ⊢ V1 ⇒ V2 → L ⊢ T1 ⇒ T2 → L ⊢ 𝕗{I} V1. T1 ⇒ 𝕗{I} V2. T2. +#I #L #V1 #V2 #T1 #T2 * #V #HV1 #HV2 * /3 width=5/ +qed. + +lemma cpr_cast: ∀L,V,T1,T2. + L ⊢ T1 ⇒ T2 → L ⊢ 𝕔{Cast} V. T1 ⇒ T2. +#L #V #T1 #T2 * /3/ +qed. + +(* Note: it does not hold replacing |L1| with |L2| *) +(* Basic_1: was only: pr2_change *) +lemma cpr_lsubs_conf: ∀L1,T1,T2. L1 ⊢ T1 ⇒ T2 → + ∀L2. L1 [0, |L1|] ≼ L2 → L2 ⊢ T1 ⇒ T2. +#L1 #T1 #T2 * #T #HT1 #HT2 #L2 #HL12 +lapply (tpss_lsubs_conf … HT2 … HL12) -HT2 HL12 /3/ +qed. + +(* Basic inversion lemmas ***************************************************) + +(* Basic_1: was: pr2_gen_csort *) +lemma cpr_inv_atom: ∀T1,T2. ⋆ ⊢ T1 ⇒ T2 → T1 ⇒ T2. +#T1 #T2 * #T #HT normalize #HT2 +<(tpss_inv_refl_O2 … HT2) -HT2 // +qed. + +(* Basic_1: was: pr2_gen_sort *) +lemma cpr_inv_sort1: ∀L,T2,k. L ⊢ ⋆k ⇒ T2 → T2 = ⋆k. +#L #T2 #k * #X #H +>(tpr_inv_atom1 … H) -H #H +>(tpss_inv_sort1 … H) -H // +qed. + +(* Basic_1: was: pr2_gen_cast *) +lemma cpr_inv_cast1: ∀L,V1,T1,U2. L ⊢ 𝕔{Cast} V1. T1 ⇒ U2 → ( + ∃∃V2,T2. L ⊢ V1 ⇒ V2 & L ⊢ T1 ⇒ T2 & + U2 = 𝕔{Cast} V2. T2 + ) ∨ L ⊢ T1 ⇒ U2. +#L #V1 #T1 #U2 * #X #H #HU2 +elim (tpr_inv_cast1 … H) -H /3/ +* #V #T #HV1 #HT1 #H destruct -X; +elim (tpss_inv_flat1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H destruct -U2 /4 width=5/ +qed. + +(* Basic_1: removed theorems 5: + pr2_head_1 pr2_head_2 pr2_cflat pr2_gen_cflat clear_pr2_trans + Basic_1: removed local theorems 3: + pr2_free_free pr2_free_delta pr2_delta_delta +*) + +(* +pr2/fwd pr2_gen_appl +pr2/fwd pr2_gen_abbr +*) 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 new file mode 100644 index 000000000..2f0e31391 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_cpr.ma @@ -0,0 +1,58 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reducibility/tpr_tpr.ma". +include "Basic_2/reducibility/cpr.ma". + +(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************) + +(* Advanced properties ******************************************************) + +lemma cpr_bind_sn: ∀I,L,V1,V2,T1,T2. L ⊢ V1 ⇒ V2 → T1 ⇒ T2 → + L ⊢ 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2. +#I #L #V1 #V2 #T1 #T2 * #V #HV1 #HV2 #HT12 +@ex2_1_intro [2: @(tpr_delta … HV1 HT12) | skip ] /2/ (* /3 width=5/ is too slow *) +qed. + +(* Basic_1: was only: pr2_gen_cbind *) +lemma cpr_bind_dx: ∀I,L,V1,V2,T1,T2. V1 ⇒ V2 → L. 𝕓{I} V2 ⊢ T1 ⇒ T2 → + L ⊢ 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2. +#I #L #V1 #V2 #T1 #T2 #HV12 * #T #HT1 normalize #HT2 +elim (tpss_split_up … HT2 1 ? ?) -HT2 // #T0 (tpr_inv_atom1 … H) -H #H +elim (tpss_inv_lref1 … H) -H /2/ +* /3 width=6/ +qed. + +(* Basic_1: was: pr2_gen_abst *) +lemma cpr_inv_abst1: ∀V1,T1,U2. 𝕔{Abst} V1. T1 ⇒ U2 → + ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Abst} V2. T2. +/2/ qed. + +(* Relocation properties ****************************************************) + +(* Basic_1: was: pr2_lift *) +lemma cpr_lift: ∀L,K,d,e. ↓[d, e] L ≡ K → + ∀T1,U1. ↑[d, e] T1 ≡ U1 → ∀T2,U2. ↑[d, e] T2 ≡ U2 → + K ⊢ T1 ⇒ T2 → L ⊢ U1 ⇒ U2. +#L #K #d #e #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 * #T #HT1 #HT2 +elim (lift_total T d e) #U #HTU +lapply (tpr_lift … HT1 … HTU1 … HTU) -T1 #HU1 +elim (lt_or_ge (|K|) d) #HKd +[ lapply (tpss_lift_le … HT2 … HLK HTU … HTU2) -T2 T HLK [ /2/ | /3/ ] +| lapply (tpss_lift_be … HT2 … HLK HTU … HTU2) -T2 T HLK // /3/ +] +qed. + +(* Basic_1: was: pr2_gen_lift *) +lemma cpr_inv_lift: ∀L,K,d,e. ↓[d, e] L ≡ K → + ∀T1,U1. ↑[d, e] T1 ≡ U1 → ∀U2. L ⊢ U1 ⇒ U2 → + ∃∃T2. ↑[d, e] T2 ≡ U2 & K ⊢ T1 ⇒ T2. +#L #K #d #e #HLK #T1 #U1 #HTU1 #U2 * #U #HU1 #HU2 +elim (tpr_inv_lift … HU1 … HTU1) -U1 #T #HTU #T1 +elim (lt_or_ge (|L|) d) #HLd +[ elim (tpss_inv_lift1_le … HU2 … HLK … HTU ?) -U HLK [ /5/ | /2/ ] +| elim (lt_or_ge (|L|) (d + e)) #HLde + [ elim (tpss_inv_lift1_be_up … HU2 … HLK … HTU ? ?) -U HLK // [ /5/ | /2/ ] + | elim (tpss_inv_lift1_be … HU2 … HLK … HTU ? ?) -U HLK // /5/ + ] +] +qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_ltpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_ltpr.ma new file mode 100644 index 000000000..486c12ee0 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_ltpr.ma @@ -0,0 +1,46 @@ +(**************************************************************************) +(* ___ *) +(* ||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/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 → + ∃∃U2. L2 ⊢ U1 ⇒ U2 & L2 ⊢ T2 [d, e] ≫* U2. +#L1 #L2 #HL12 #T1 #T2 * #T #HT1 #HT2 #d #e #U1 #HTU1 +elim (tpr_tpss_ltpr … HL12 … HT1 … HTU1) -L1 HT1 #U #HU1 #HTU +elim (tpss_conf_eq … HT2 … HTU) -T /3/ +qed. + +lemma cpr_ltpr_conf_eq: ∀L1,T1,T2. L1 ⊢ T1 ⇒ T2 → ∀L2. L1 ⇒ L2 → + ∃∃T. L2 ⊢ T1 ⇒ T & T2 ⇒ T. +#L1 #T1 #T2 * #T #HT1 #HT2 #L2 #HL12 +>(ltpr_fwd_length … HL12) in HT2 #HT2 +elim (tpr_tpss_ltpr … HL12 … HT2) -L1 HT2 /3/ +qed. + +lemma cpr_ltpr_conf_tpss: ∀L1,L2. L1 ⇒ L2 → ∀T1,T2. L1 ⊢ T1 ⇒ T2 → + ∀d,e,U1. L1 ⊢ T1 [d, e] ≫* U1 → + ∃∃U2. L2 ⊢ U1 ⇒ U2 & L2 ⊢ T2 ⇒ U2. +#L1 #L2 #HL12 #T1 #T2 #HT12 #d #e #U1 #HTU1 +elim (cpr_ltpr_conf_eq … HT12 … HL12) -HT12 #T #HT1 #HT2 +elim (cpr_tpss_ltpr … HL12 … HT1 … HTU1) -L1 HT1 #U2 #HU12 #HTU2 +lapply (tpss_weak_all … HTU2) -HTU2 #HTU2 /3 width=5/ (**) (* /4 width=5/ is too slow *) +qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/lcpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/lcpr.ma new file mode 100644 index 000000000..13545ad84 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/lcpr.ma @@ -0,0 +1,37 @@ +(**************************************************************************) +(* ___ *) +(* ||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/unfold/ltpss.ma". +include "Basic_2/reducibility/ltpr.ma". + +(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *************) + +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 properties *********************************************************) + +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/reducibility/ltpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr.ma new file mode 100644 index 000000000..ecb0ad08c --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr.ma @@ -0,0 +1,89 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reducibility/tpr.ma". + +(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************) + +inductive ltpr: relation lenv ≝ +| ltpr_stom: ltpr (⋆) (⋆) +| ltpr_pair: ∀K1,K2,I,V1,V2. + ltpr K1 K2 → V1 ⇒ V2 → ltpr (K1. 𝕓{I} V1) (K2. 𝕓{I} V2) (*𝕓*) +. + +interpretation + "context-free parallel reduction (environment)" + 'PRed L1 L2 = (ltpr L1 L2). + +(* Basic properties *********************************************************) + +lemma ltpr_refl: ∀L:lenv. L ⇒ L. +#L elim L -L /2/ +qed. + +(* Basic inversion lemmas ***************************************************) + +fact ltpr_inv_atom1_aux: ∀L1,L2. L1 ⇒ L2 → L1 = ⋆ → L2 = ⋆. +#L1 #L2 * -L1 L2 +[ // +| #K1 #K2 #I #V1 #V2 #_ #_ #H destruct +] +qed. + +(* Basic_1: was: wcpr0_gen_sort *) +lemma ltpr_inv_atom1: ∀L2. ⋆ ⇒ L2 → L2 = ⋆. +/2/ qed. + +fact ltpr_inv_pair1_aux: ∀L1,L2. L1 ⇒ L2 → ∀K1,I,V1. L1 = K1. 𝕓{I} V1 → + ∃∃K2,V2. K1 ⇒ 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_1: was: wcpr0_gen_head *) +lemma ltpr_inv_pair1: ∀K1,I,V1,L2. K1. 𝕓{I} V1 ⇒ L2 → + ∃∃K2,V2. K1 ⇒ K2 & V1 ⇒ V2 & L2 = K2. 𝕓{I} V2. +/2/ qed. + +fact ltpr_inv_atom2_aux: ∀L1,L2. L1 ⇒ L2 → L2 = ⋆ → L1 = ⋆. +#L1 #L2 * -L1 L2 +[ // +| #K1 #K2 #I #V1 #V2 #_ #_ #H destruct +] +qed. + +lemma ltpr_inv_atom2: ∀L1. L1 ⇒ ⋆ → L1 = ⋆. +/2/ qed. + +fact ltpr_inv_pair2_aux: ∀L1,L2. L1 ⇒ L2 → ∀K2,I,V2. L2 = K2. 𝕓{I} V2 → + ∃∃K1,V1. K1 ⇒ K2 & V1 ⇒ V2 & L1 = K1. 𝕓{I} V1. +#L1 #L2 * -L1 L2 +[ #K2 #I #V2 #H destruct +| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #K #J #W #H destruct -K2 I V2 /2 width=5/ +] +qed. + +lemma ltpr_inv_pair2: ∀L1,K2,I,V2. L1 ⇒ K2. 𝕓{I} V2 → + ∃∃K1,V1. K1 ⇒ K2 & V1 ⇒ V2 & L1 = K1. 𝕓{I} V1. +/2/ qed. + +(* Basic forward lemmas *****************************************************) + +lemma ltpr_fwd_length: ∀L1,L2. L1 ⇒ L2 → |L1| = |L2|. +#L1 #L2 #H elim H -H L1 L2; normalize // +qed. + +(* Basic_1: removed theorems 2: wcpr0_getl wcpr0_getl_back *) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_ldrop.ma new file mode 100644 index 000000000..485c00fd1 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_ldrop.ma @@ -0,0 +1,52 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reducibility/tpr_lift.ma". +include "Basic_2/reducibility/ltpr.ma". + +(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************) + +(* Basic_1: was: wcpr0_ldrop *) +lemma ltpr_ldrop_conf: ∀L1,K1,d,e. ↓[d, e] L1 ≡ K1 → ∀L2. L1 ⇒ L2 → + ∃∃K2. ↓[d, e] L2 ≡ K2 & K1 ⇒ K2. +#L1 #K1 #d #e #H elim H -H L1 K1 d e +[ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2/ +| #K1 #I #V1 #X #H + elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct /3 width=5/ +| #L1 #K1 #I #V1 #e #_ #IHLK1 #X #H + elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct -X; + elim (IHLK1 … HL12) -IHLK1 HL12 /3/ +| #L1 #K1 #I #V1 #W1 #d #e #_ #HWV1 #IHLK1 #X #H + elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct -X; + elim (tpr_inv_lift … HV12 … HWV1) -HV12 HWV1; + elim (IHLK1 … HL12) -IHLK1 HL12 /3 width=5/ +] +qed. + +(* Basic_1: was: wcpr0_ldrop_back *) +lemma ltpr_ldrop_trans: ∀L1,K1,d,e. ↓[d, e] L1 ≡ K1 → ∀K2. K1 ⇒ K2 → + ∃∃L2. ↓[d, e] L2 ≡ K2 & L1 ⇒ L2. +#L1 #K1 #d #e #H elim H -H L1 K1 d e +[ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2/ +| #K1 #I #V1 #X #H + elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=5/ +| #L1 #K1 #I #V1 #e #_ #IHLK1 #K2 #HK12 + elim (IHLK1 … HK12) -IHLK1 HK12 /3 width=5/ +| #L1 #K1 #I #V1 #W1 #d #e #_ #HWV1 #IHLK1 #X #H + elim (ltpr_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct -X; + elim (lift_total W2 d e) #V2 #HWV2 + lapply (tpr_lift … HW12 … HWV1 … HWV2) -HW12 HWV1; + elim (IHLK1 … HK12) -IHLK1 HK12 /3 width=5/ +] +qed. 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/reducibility/tpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr.ma new file mode 100644 index 000000000..db2c8c69f --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr.ma @@ -0,0 +1,198 @@ +(**************************************************************************) +(* ___ *) +(* ||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.ma". + +(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) + +(* Basic_1: includes: pr0_delta1 *) +inductive tpr: relation term ≝ +| tpr_atom : ∀I. tpr (𝕒{I}) (𝕒{I}) +| tpr_flat : ∀I,V1,V2,T1,T2. tpr V1 V2 → tpr T1 T2 → + tpr (𝕗{I} V1. T1) (𝕗{I} V2. T2) +| tpr_beta : ∀V1,V2,W,T1,T2. + tpr V1 V2 → tpr T1 T2 → + tpr (𝕔{Appl} V1. 𝕔{Abst} W. T1) (𝕔{Abbr} V2. T2) +| tpr_delta: ∀I,V1,V2,T1,T2,T. + tpr V1 V2 → tpr T1 T2 → ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ T → + tpr (𝕓{I} V1. T1) (𝕓{I} V2. T) +| tpr_theta: ∀V,V1,V2,W1,W2,T1,T2. + tpr V1 V2 → ↑[0,1] V2 ≡ V → tpr W1 W2 → tpr T1 T2 → + tpr (𝕔{Appl} V1. 𝕔{Abbr} W1. T1) (𝕔{Abbr} W2. 𝕔{Appl} V. T2) +| tpr_zeta : ∀V,T,T1,T2. ↑[0,1] T1 ≡ T → tpr T1 T2 → + tpr (𝕔{Abbr} V. T) T2 +| tpr_tau : ∀V,T1,T2. tpr T1 T2 → tpr (𝕔{Cast} V. T1) T2 +. + +interpretation + "context-free parallel reduction (term)" + 'PRed T1 T2 = (tpr T1 T2). + +(* Basic properties *********************************************************) + +lemma tpr_bind: ∀I,V1,V2,T1,T2. V1 ⇒ V2 → T1 ⇒ T2 → + 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2. +/2/ qed. + +(* Basic_1: was by definition: pr0_refl *) +lemma tpr_refl: ∀T. T ⇒ T. +#T elim T -T // +#I elim I -I /2/ +qed. + +(* Basic inversion lemmas ***************************************************) + +fact tpr_inv_atom1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I. U1 = 𝕒{I} → U2 = 𝕒{I}. +#U1 #U2 * -U1 U2 +[ // +| #I #V1 #V2 #T1 #T2 #_ #_ #k #H destruct +| #V1 #V2 #W #T1 #T2 #_ #_ #k #H destruct +| #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #k #H destruct +| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #k #H destruct +| #V #T #T1 #T2 #_ #_ #k #H destruct +| #V #T1 #T2 #_ #k #H destruct +] +qed. + +(* Basic_1: was: pr0_gen_sort pr0_gen_lref *) +lemma tpr_inv_atom1: ∀I,U2. 𝕒{I} ⇒ U2 → U2 = 𝕒{I}. +/2/ qed. + +fact tpr_inv_bind1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I,V1,T1. U1 = 𝕓{I} V1. T1 → + (∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 & + ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ T & + U2 = 𝕓{I} V2. T + ) ∨ + ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr. +#U1 #U2 * -U1 U2 +[ #J #I #V #T #H destruct +| #I1 #V1 #V2 #T1 #T2 #_ #_ #I #V #T #H destruct +| #V1 #V2 #W #T1 #T2 #_ #_ #I #V #T #H destruct +| #I1 #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #I0 #V0 #T0 #H destruct -I1 V1 T1 /3 width=7/ +| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #I0 #V0 #T0 #H destruct +| #V #T #T1 #T2 #HT1 #HT12 #I0 #V0 #T0 #H destruct -V T /3/ +| #V #T1 #T2 #_ #I0 #V0 #T0 #H destruct +] +qed. + +lemma tpr_inv_bind1: ∀V1,T1,U2,I. 𝕓{I} V1. T1 ⇒ U2 → + (∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 & + ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ T & + U2 = 𝕓{I} V2. T + ) ∨ + ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr. +/2/ qed. + +(* Basic_1: was pr0_gen_abbr *) +lemma tpr_inv_abbr1: ∀V1,T1,U2. 𝕓{Abbr} V1. T1 ⇒ U2 → + (∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 & + ⋆. 𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T & + U2 = 𝕓{Abbr} V2. T + ) ∨ + ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2. +#V1 #T1 #U2 #H +elim (tpr_inv_bind1 … H) -H * /3 width=7/ +qed. + +fact tpr_inv_flat1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I,V1,U0. U1 = 𝕗{I} V1. U0 → + ∨∨ ∃∃V2,T2. V1 ⇒ V2 & U0 ⇒ T2 & + U2 = 𝕗{I} V2. T2 + | ∃∃V2,W,T1,T2. V1 ⇒ V2 & T1 ⇒ T2 & + U0 = 𝕔{Abst} W. T1 & + U2 = 𝕔{Abbr} V2. T2 & I = Appl + | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 & + ↑[0,1] V2 ≡ V & + U0 = 𝕔{Abbr} W1. T1 & + U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2 & + I = Appl + | (U0 ⇒ U2 ∧ I = Cast). +#U1 #U2 * -U1 U2 +[ #I #J #V #T #H destruct +| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #J #V #T #H destruct -I V1 T1 /3 width=5/ +| #V1 #V2 #W #T1 #T2 #HV12 #HT12 #J #V #T #H destruct -J V1 T /3 width=8/ +| #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #J #V0 #T0 #H destruct +| #V #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #J #V0 #T0 #H + destruct -J V1 T0 /3 width=12/ +| #V #T #T1 #T2 #_ #_ #J #V0 #T0 #H destruct +| #V #T1 #T2 #HT12 #J #V0 #T0 #H destruct -J V T1 /3/ +] +qed. + +lemma tpr_inv_flat1: ∀V1,U0,U2,I. 𝕗{I} V1. U0 ⇒ U2 → + ∨∨ ∃∃V2,T2. V1 ⇒ V2 & U0 ⇒ T2 & + U2 = 𝕗{I} V2. T2 + | ∃∃V2,W,T1,T2. V1 ⇒ V2 & T1 ⇒ T2 & + U0 = 𝕔{Abst} W. T1 & + U2 = 𝕔{Abbr} V2. T2 & I = Appl + | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 & + ↑[0,1] V2 ≡ V & + U0 = 𝕔{Abbr} W1. T1 & + U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2 & + I = Appl + | (U0 ⇒ U2 ∧ I = Cast). +/2/ qed. + +(* Basic_1: was pr0_gen_appl *) +lemma tpr_inv_appl1: ∀V1,U0,U2. 𝕔{Appl} V1. U0 ⇒ U2 → + ∨∨ ∃∃V2,T2. V1 ⇒ V2 & U0 ⇒ T2 & + U2 = 𝕔{Appl} V2. T2 + | ∃∃V2,W,T1,T2. V1 ⇒ V2 & T1 ⇒ T2 & + U0 = 𝕔{Abst} W. T1 & + U2 = 𝕔{Abbr} V2. T2 + | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 & + ↑[0,1] V2 ≡ V & + U0 = 𝕔{Abbr} W1. T1 & + U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2. +#V1 #U0 #U2 #H +elim (tpr_inv_flat1 … H) -H * /3 width=12/ #_ #H destruct +qed. + +(* Basic_1: was: pr0_gen_cast *) +lemma tpr_inv_cast1: ∀V1,T1,U2. 𝕔{Cast} V1. T1 ⇒ U2 → + (∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Cast} V2. T2) + ∨ T1 ⇒ U2. +#V1 #T1 #U2 #H +elim (tpr_inv_flat1 … H) -H * /3 width=5/ +[ #V2 #W #W1 #W2 #_ #_ #_ #_ #H destruct +| #V2 #W #W1 #W2 #T2 #U1 #_ #_ #_ #_ #_ #_ #H destruct +] +qed. + +fact tpr_inv_lref2_aux: ∀T1,T2. T1 ⇒ T2 → ∀i. T2 = #i → + ∨∨ T1 = #i + | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i & + T1 = 𝕔{Abbr} V. T + | ∃∃V,T. T ⇒ #i & T1 = 𝕔{Cast} V. T. +#T1 #T2 * -T1 T2 +[ #I #i #H destruct /2/ +| #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct +| #V1 #V2 #W #T1 #T2 #_ #_ #i #H destruct +| #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #i #H destruct +| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #i #H destruct +| #V #T #T1 #T2 #HT1 #HT12 #i #H destruct /3 width=6/ +| #V #T1 #T2 #HT12 #i #H destruct /3/ +] +qed. + +lemma tpr_inv_lref2: ∀T1,i. T1 ⇒ #i → + ∨∨ T1 = #i + | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i & + T1 = 𝕔{Abbr} V. T + | ∃∃V,T. T ⇒ #i & T1 = 𝕔{Cast} V. T. +/2/ qed. + +(* Basic_1: removed theorems 3: + pr0_subst0_back pr0_subst0_fwd pr0_subst0 + Basic_1: removed local theorems: 1: pr0_delta_tau +*) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma new file mode 100644 index 000000000..0c8235765 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma @@ -0,0 +1,121 @@ +(**************************************************************************) +(* ___ *) +(* ||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/tpr.ma". + +(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) + +(* Relocation properties ****************************************************) + +(* Basic_1: was: pr0_lift *) +lemma tpr_lift: ∀T1,T2. T1 ⇒ T2 → + ∀d,e,U1. ↑[d, e] T1 ≡ U1 → ∀U2. ↑[d, e] T2 ≡ U2 → U1 ⇒ U2. +#T1 #T2 #H elim H -H T1 T2 +[ * #i #d #e #U1 #HU1 #U2 #HU2 + lapply (lift_mono … HU1 … HU2) -HU1 #H destruct -U1 + [ lapply (lift_inv_sort1 … HU2) -HU2 #H destruct -U2 // + | lapply (lift_inv_lref1 … HU2) * * #Hid #H destruct -U2 // + | lapply (lift_inv_gref1 … HU2) -HU2 #H destruct -U2 // + ] +| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2 + elim (lift_inv_flat1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct -X1; + elim (lift_inv_flat1 … HX2) -HX2 #W2 #U2 #HVW2 #HTU2 #HX2 destruct -X2 /3/ +| #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2 + elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct -X1; + elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct -X; + elim (lift_inv_bind1 … HX2) -HX2 #V3 #T3 #HV23 #HT23 #HX2 destruct -X2 /3/ +| #I #V1 #V2 #T1 #T2 #T0 #HV12 #HT12 #HT2 #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2 + elim (lift_inv_bind1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct -X1; + elim (lift_inv_bind1 … HX2) -HX2 #W2 #U0 #HVW2 #HTU0 #HX2 destruct -X2; + elim (lift_total T2 (d + 1) e) #U2 #HTU2 + @tpr_delta + [4: @(tps_lift_le … HT2 … HTU2 HTU0 ?) /2/ |1: skip |2: /2/ |3: /2/ ] (**) (*/3. is too slow *) +| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #d #e #X1 #HX1 #X2 #HX2 + elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct -X1; + elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct -X; + elim (lift_inv_bind1 … HX2) -HX2 #W3 #X #HW23 #HX #HX2 destruct -X2; + elim (lift_inv_flat1 … HX) -HX #V3 #T3 #HV3 #HT23 #HX destruct -X; + elim (lift_trans_ge … HV2 … HV3 ?) -HV2 HV3 V // /3/ +| #V #T #T1 #T2 #HT1 #_ #IHT12 #d #e #X #HX #T0 #HT20 + elim (lift_inv_bind1 … HX) -HX #V3 #T3 #_ #HT3 #HX destruct -X; + elim (lift_trans_ge … HT1 … HT3 ?) -HT1 HT3 T // /3 width=6/ +| #V #T1 #T2 #_ #IHT12 #d #e #X #HX #T #HT2 + elim (lift_inv_flat1 … HX) -HX #V0 #T0 #_ #HT0 #HX destruct -X /3/ +] +qed. + +(* Basic_1: was: pr0_gen_lift *) +lemma tpr_inv_lift: ∀T1,T2. T1 ⇒ T2 → + ∀d,e,U1. ↑[d, e] U1 ≡ T1 → + ∃∃U2. ↑[d, e] U2 ≡ T2 & U1 ⇒ U2. +#T1 #T2 #H elim H -H T1 T2 +[ * #i #d #e #U1 #HU1 + [ lapply (lift_inv_sort2 … HU1) -HU1 #H destruct -U1 /2/ + | lapply (lift_inv_lref2 … HU1) -HU1 * * #Hid #H destruct -U1 /3/ + | lapply (lift_inv_gref2 … HU1) -HU1 #H destruct -U1 /2/ + ] +| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X #HX + elim (lift_inv_flat2 … HX) -HX #V0 #T0 #HV01 #HT01 #HX destruct -X; + elim (IHV12 … HV01) -IHV12 HV01; + elim (IHT12 … HT01) -IHT12 HT01 /3 width=5/ +| #V1 #V2 #W1 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X #HX + elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct -X; + elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct -Y; + elim (IHV12 … HV01) -IHV12 HV01; + elim (IHT12 … HT01) -IHT12 HT01 /3 width=5/ +| #I #V1 #V2 #T1 #T2 #T0 #_ #_ #HT20 #IHV12 #IHT12 #d #e #X #HX + elim (lift_inv_bind2 … HX) -HX #W1 #U1 #HWV1 #HUT1 #HX destruct -X; + elim (IHV12 … HWV1) -IHV12 HWV1 #W2 #HWV2 #HW12 + elim (IHT12 … HUT1) -IHT12 HUT1 #U2 #HUT2 #HU12 + elim (tps_inv_lift1_le … HT20 … HUT2 ?) -HT20 HUT2 // [3: /2 width=5/ |2: skip ] #U0 #HU20 #HUT0 + @ex2_1_intro [2: /2/ |1: skip |3: /2/ ] (**) (* /3 width=5/ is slow *) +| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #d #e #X #HX + elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct -X; + elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct -Y; + elim (IHV12 … HV01) -IHV12 HV01 #V3 #HV32 #HV03 + elim (IHW12 … HW01) -IHW12 HW01 #W3 #HW32 #HW03 + elim (IHT12 … HT01) -IHT12 HT01 #T3 #HT32 #HT03 + elim (lift_trans_le … HV32 … HV2 ?) -HV32 HV2 V2 // #V2 #HV32 #HV2 + @ex2_1_intro [2: /3/ |1: skip |3: /2/ ] (**) (* /4 width=5/ is slow *) +| #V #T #T1 #T2 #HT1 #_ #IHT12 #d #e #X #HX + elim (lift_inv_bind2 … HX) -HX #V0 #T0 #_ #HT0 #H destruct -X; + elim (lift_div_le … HT1 … HT0 ?) -HT1 HT0 T // #T #HT0 #HT1 + elim (IHT12 … HT1) -IHT12 HT1 /3 width=5/ +| #V #T1 #T2 #_ #IHT12 #d #e #X #HX + elim (lift_inv_flat2 … HX) -HX #V0 #T0 #_ #HT01 #H destruct -X; + elim (IHT12 … HT01) -IHT12 HT01 /3/ +] +qed. + +(* Advanced inversion lemmas ************************************************) + +fact tpr_inv_abst1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕔{Abst} V1. T1 → + ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Abst} V2. T2. +#U1 #U2 * -U1 U2 +[ #I #V #T #H destruct +| #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct +| #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct +| #I #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #V0 #T0 #H destruct -I V1 T1; + <(tps_inv_refl_SO2 … HT2 ? ? ?) -HT2 T /2 width=5/ +| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #V0 #T0 #H destruct +| #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct +| #V #T1 #T2 #_ #V0 #T0 #H destruct +] +qed. + +(* Basic_1: was pr0_gen_abst *) +lemma tpr_inv_abst1: ∀V1,T1,U2. 𝕔{Abst} V1. T1 ⇒ U2 → + ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Abst} V2. T2. +/2/ qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpr.ma new file mode 100644 index 000000000..4217ced9a --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpr.ma @@ -0,0 +1,287 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reducibility/tpr_tpss.ma". + +(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) + +(* Confluence lemmas ********************************************************) + +fact tpr_conf_atom_atom: ∀I. ∃∃X. 𝕒{I} ⇒ X & 𝕒{I} ⇒ X. +/2/ qed. + +fact tpr_conf_flat_flat: + ∀I,V0,V1,T0,T1,V2,T2. ( + ∀X0:term. #[X0] < #[V0] + #[T0] + 1 → + ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → + ∃∃X. X1 ⇒ X & X2 ⇒ X + ) → + V0 ⇒ V1 → V0 ⇒ V2 → T0 ⇒ T1 → T0 ⇒ T2 → + ∃∃T0. 𝕗{I} V1. T1 ⇒ T0 & 𝕗{I} V2. T2 ⇒ T0. +#I #V0 #V1 #T0 #T1 #V2 #T2 #IH #HV01 #HV02 #HT01 #HT02 +elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2 +elim (IH … HT01 … HT02) -HT01 HT02 /3 width=5/ +qed. + +fact tpr_conf_flat_beta: + ∀V0,V1,T1,V2,W0,U0,T2. ( + ∀X0:term. #[X0] < #[V0] + (#[W0] + #[U0] + 1) + 1 → + ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → + ∃∃X. X1 ⇒ X & X2 ⇒ X + ) → + V0 ⇒ V1 → V0 ⇒ V2 → + U0 ⇒ T2 → 𝕔{Abst} W0. U0 ⇒ T1 → + ∃∃X. 𝕔{Appl} V1. T1 ⇒ X & 𝕔{Abbr} V2. T2 ⇒ X. +#V0 #V1 #T1 #V2 #W0 #U0 #T2 #IH #HV01 #HV02 #HT02 #H +elim (tpr_inv_abst1 … H) -H #W1 #U1 #HW01 #HU01 #H destruct -T1; +elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2 +elim (IH … HT02 … HU01) -HT02 HU01 IH /3 width=5/ +qed. + +(* basic-1: was: + pr0_cong_upsilon_refl pr0_cong_upsilon_zeta + pr0_cong_upsilon_cong pr0_cong_upsilon_delta +*) +fact tpr_conf_flat_theta: + ∀V0,V1,T1,V2,V,W0,W2,U0,U2. ( + ∀X0:term. #[X0] < #[V0] + (#[W0] + #[U0] + 1) + 1 → + ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → + ∃∃X. X1 ⇒ X & X2 ⇒ X + ) → + V0 ⇒ V1 → V0 ⇒ V2 → ↑[O,1] V2 ≡ V → + W0 ⇒ W2 → U0 ⇒ U2 → 𝕔{Abbr} W0. U0 ⇒ T1 → + ∃∃X. 𝕔{Appl} V1. T1 ⇒ X & 𝕔{Abbr} W2. 𝕔{Appl} V. U2 ⇒ X. +#V0 #V1 #T1 #V2 #V #W0 #W2 #U0 #U2 #IH #HV01 #HV02 #HV2 #HW02 #HU02 #H +elim (IH … HV01 … HV02) -HV01 HV02 // #VV #HVV1 #HVV2 +elim (lift_total VV 0 1) #VVV #HVV +lapply (tpr_lift … HVV2 … HV2 … HVV) #HVVV +elim (tpr_inv_abbr1 … H) -H * +(* case 1: delta *) +[ -HV2 HVV2 #WW2 #UU2 #UU #HWW2 #HUU02 #HUU2 #H destruct -T1; + elim (IH … HW02 … HWW2) -HW02 HWW2 // #W #HW02 #HWW2 + elim (IH … HU02 … HUU02) -HU02 HUU02 IH // #U #HU2 #HUUU2 + elim (tpr_tps_bind … HWW2 HUUU2 … HUU2) -HUU2 HUUU2 #UUU #HUUU2 #HUUU1 + @ex2_1_intro + [2: @tpr_theta [6: @HVV |7: @HWW2 |8: @HUUU2 |1,2,3,4: skip | // ] + |1:skip + |3: @tpr_delta [3: @tpr_flat |1: skip ] /2 width=5/ + ] (**) (* /5 width=14/ is too slow *) +(* case 3: zeta *) +| -HW02 HVV HVVV #UU1 #HUU10 #HUUT1 + elim (tpr_inv_lift … HU02 … HUU10) -HU02 #UU #HUU2 #HUU1 + lapply (tw_lift … HUU10) -HUU10 #HUU10 + elim (IH … HUUT1 … HUU1) -HUUT1 HUU1 IH // -HUU10 #U #HU2 #HUUU2 + @ex2_1_intro + [2: @tpr_flat + |1: skip + |3: @tpr_zeta [2: @lift_flat |1: skip |3: @tpr_flat ] + ] /2 width=5/ (**) (* /5 width=5/ is too slow *) +] +qed. + +fact tpr_conf_flat_cast: + ∀X2,V0,V1,T0,T1. ( + ∀X0:term. #[X0] < #[V0] + #[T0] + 1 → + ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → + ∃∃X. X1 ⇒ X & X2 ⇒ X + ) → + V0 ⇒ V1 → T0 ⇒ T1 → T0 ⇒ X2 → + ∃∃X. 𝕔{Cast} V1. T1 ⇒ X & X2 ⇒ X. +#X2 #V0 #V1 #T0 #T1 #IH #_ #HT01 #HT02 +elim (IH … HT01 … HT02) -HT01 HT02 IH /3/ +qed. + +fact tpr_conf_beta_beta: + ∀W0:term. ∀V0,V1,T0,T1,V2,T2. ( + ∀X0:term. #[X0] < #[V0] + (#[W0] + #[T0] + 1) + 1 → + ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → + ∃∃X. X1 ⇒ X & X2 ⇒ X + ) → + V0 ⇒ V1 → V0 ⇒ V2 → T0 ⇒ T1 → T0 ⇒ T2 → + ∃∃X. 𝕔{Abbr} V1. T1 ⇒X & 𝕔{Abbr} V2. T2 ⇒ X. +#W0 #V0 #V1 #T0 #T1 #V2 #T2 #IH #HV01 #HV02 #HT01 #HT02 +elim (IH … HV01 … HV02) -HV01 HV02 // +elim (IH … HT01 … HT02) -HT01 HT02 IH /3 width=5/ +qed. + +(* Basic_1: was: pr0_cong_delta pr0_delta_delta *) +fact tpr_conf_delta_delta: + ∀I1,V0,V1,T0,T1,TT1,V2,T2,TT2. ( + ∀X0:term. #[X0] < #[V0] + #[T0] + 1 → + ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → + ∃∃X. X1 ⇒ X & X2 ⇒ X + ) → + V0 ⇒ V1 → V0 ⇒ V2 → T0 ⇒ T1 → T0 ⇒ T2 → + ⋆. 𝕓{I1} V1 ⊢ T1 [O, 1] ≫ TT1 → + ⋆. 𝕓{I1} V2 ⊢ T2 [O, 1] ≫ TT2 → + ∃∃X. 𝕓{I1} V1. TT1 ⇒ X & 𝕓{I1} V2. TT2 ⇒ X. +#I1 #V0 #V1 #T0 #T1 #TT1 #V2 #T2 #TT2 #IH #HV01 #HV02 #HT01 #HT02 #HTT1 #HTT2 +elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2 +elim (IH … HT01 … HT02) -HT01 HT02 IH // #T #HT1 #HT2 +elim (tpr_tps_bind … HV1 HT1 … HTT1) -HT1 HTT1 #U1 #TTU1 #HTU1 +elim (tpr_tps_bind … HV2 HT2 … HTT2) -HT2 HTT2 #U2 #TTU2 #HTU2 +elim (tps_conf_eq … HTU1 … HTU2) -HTU1 HTU2 #U #HU1 #HU2 +@ex2_1_intro [2,3: @tpr_delta |1: skip ] /width=10/ (**) (* /3 width=10/ is too slow *) +qed. + +fact tpr_conf_delta_zeta: + ∀X2,V0,V1,T0,T1,TT1,T2. ( + ∀X0:term. #[X0] < #[V0] + #[T0] + 1 → + ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → + ∃∃X. X1 ⇒ X & X2 ⇒ X + ) → + V0 ⇒ V1 → T0 ⇒ T1 → ⋆. 𝕓{Abbr} V1 ⊢ T1 [O,1] ≫ TT1 → + T2 ⇒ X2 → ↑[O, 1] T2 ≡ T0 → + ∃∃X. 𝕓{Abbr} V1. TT1 ⇒ X & X2 ⇒ X. +#X2 #V0 #V1 #T0 #T1 #TT1 #T2 #IH #_ #HT01 #HTT1 #HTX2 #HTT20 +elim (tpr_inv_lift … HT01 … HTT20) -HT01 #TT2 #HTT21 #HTT2 +lapply (tps_inv_lift1_eq … HTT1 … HTT21) -HTT1 #HTT1 destruct -T1; +lapply (tw_lift … HTT20) -HTT20 #HTT20 +elim (IH … HTX2 … HTT2) -HTX2 HTT2 IH /3/ +qed. + +(* Basic_1: was: pr0_upsilon_upsilon *) +fact tpr_conf_theta_theta: + ∀VV1,V0,V1,W0,W1,T0,T1,V2,VV2,W2,T2. ( + ∀X0:term. #[X0] < #[V0] + (#[W0] + #[T0] + 1) + 1 → + ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → + ∃∃X. X1 ⇒ X & X2 ⇒ X + ) → + V0 ⇒ V1 → V0 ⇒ V2 → W0 ⇒ W1 → W0 ⇒ W2 → T0 ⇒ T1 → T0 ⇒ T2 → + ↑[O, 1] V1 ≡ VV1 → ↑[O, 1] V2 ≡ VV2 → + ∃∃X. 𝕔{Abbr} W1. 𝕔{Appl} VV1. T1 ⇒ X & 𝕔{Abbr} W2. 𝕔{Appl} VV2. T2 ⇒ X. +#VV1 #V0 #V1 #W0 #W1 #T0 #T1 #V2 #VV2 #W2 #T2 #IH #HV01 #HV02 #HW01 #HW02 #HT01 #HT02 #HVV1 #HVV2 +elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2 +elim (IH … HW01 … HW02) -HW01 HW02 // #W #HW1 #HW2 +elim (IH … HT01 … HT02) -HT01 HT02 IH // #T #HT1 #HT2 +elim (lift_total V 0 1) #VV #HVV +lapply (tpr_lift … HV1 … HVV1 … HVV) -HV1 HVV1 #HVV1 +lapply (tpr_lift … HV2 … HVV2 … HVV) -HV2 HVV2 HVV #HVV2 +@ex2_1_intro [2,3: @tpr_bind |1:skip ] /2 width=5/ (**) (* /4 width=5/ is too slow *) +qed. + +fact tpr_conf_zeta_zeta: + ∀V0:term. ∀X2,TT0,T0,T1,T2. ( + ∀X0:term. #[X0] < #[V0] + #[TT0] + 1 → + ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → + ∃∃X. X1 ⇒ X & X2 ⇒ X + ) → + T0 ⇒ T1 → T2 ⇒ X2 → + ↑[O, 1] T0 ≡ TT0 → ↑[O, 1] T2 ≡ TT0 → + ∃∃X. T1 ⇒ X & X2 ⇒ X. +#V0 #X2 #TT0 #T0 #T1 #T2 #IH #HT01 #HTX2 #HTT0 #HTT20 +lapply (lift_inj … HTT0 … HTT20) -HTT0 #H destruct -T0; +lapply (tw_lift … HTT20) -HTT20 #HTT20 +elim (IH … HT01 … HTX2) -HT01 HTX2 IH /2/ +qed. + +fact tpr_conf_tau_tau: + ∀V0,T0:term. ∀X2,T1. ( + ∀X0:term. #[X0] < #[V0] + #[T0] + 1 → + ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → + ∃∃X. X1 ⇒ X & X2 ⇒ X + ) → + T0 ⇒ T1 → T0 ⇒ X2 → + ∃∃X. T1 ⇒ X & X2 ⇒ X. +#V0 #T0 #X2 #T1 #IH #HT01 #HT02 +elim (IH … HT01 … HT02) -HT01 HT02 IH /2/ +qed. + +(* Confluence ***************************************************************) + +fact tpr_conf_aux: + ∀Y0:term. ( + ∀X0:term. #[X0] < #[Y0] → + ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → + ∃∃X. X1 ⇒ X & X2 ⇒ X + ) → + ∀X0,X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → X0 = Y0 → + ∃∃X. X1 ⇒ X & X2 ⇒ X. +#Y0 #IH #X0 #X1 #X2 * -X0 X1 +[ #I1 #H1 #H2 destruct -Y0; + lapply (tpr_inv_atom1 … H1) -H1 +(* case 1: atom, atom *) + #H1 destruct -X2 // +| #I #V0 #V1 #T0 #T1 #HV01 #HT01 #H1 #H2 destruct -Y0; + elim (tpr_inv_flat1 … H1) -H1 * +(* case 2: flat, flat *) + [ #V2 #T2 #HV02 #HT02 #H destruct -X2 + /3 width=7 by tpr_conf_flat_flat/ (**) (* /3 width=7/ is too slow *) +(* case 3: flat, beta *) + | #V2 #W #U0 #T2 #HV02 #HT02 #H1 #H2 #H3 destruct -T0 X2 I + /3 width=8 by tpr_conf_flat_beta/ (**) (* /3 width=8/ is too slow *) +(* case 4: flat, theta *) + | #V2 #V #W0 #W2 #U0 #U2 #HV02 #HW02 #HT02 #HV2 #H1 #H2 #H3 destruct -T0 X2 I + /3 width=11 by tpr_conf_flat_theta/ (**) (* /3 width=11/ is too slow *) +(* case 5: flat, tau *) + | #HT02 #H destruct -I + /3 width=6 by tpr_conf_flat_cast/ (**) (* /3 width=6/ is too slow *) + ] +| #V0 #V1 #W0 #T0 #T1 #HV01 #HT01 #H1 #H2 destruct -Y0; + elim (tpr_inv_appl1 … H1) -H1 * +(* case 6: beta, flat (repeated) *) + [ #V2 #T2 #HV02 #HT02 #H destruct -X2 + @ex2_1_comm /3 width=8 by tpr_conf_flat_beta/ +(* case 7: beta, beta *) + | #V2 #WW0 #TT0 #T2 #HV02 #HT02 #H1 #H2 destruct -W0 T0 X2 + /3 width=8 by tpr_conf_beta_beta/ (**) (* /3 width=8/ is too slow *) +(* case 8, beta, theta (excluded) *) + | #V2 #VV2 #WW0 #W2 #TT0 #T2 #_ #_ #_ #_ #H destruct + ] +| #I1 #V0 #V1 #T0 #T1 #TT1 #HV01 #HT01 #HTT1 #H1 #H2 destruct -Y0; + elim (tpr_inv_bind1 … H1) -H1 * +(* case 9: delta, delta *) + [ #V2 #T2 #TT2 #HV02 #HT02 #HTT2 #H destruct -X2 + /3 width=11 by tpr_conf_delta_delta/ (**) (* /3 width=11/ is too slow *) +(* case 10: delta, zata *) + | #T2 #HT20 #HTX2 #H destruct -I1; + /3 width=10 by tpr_conf_delta_zeta/ (**) (* /3 width=10/ is too slow *) + ] +| #VV1 #V0 #V1 #W0 #W1 #T0 #T1 #HV01 #HVV1 #HW01 #HT01 #H1 #H2 destruct -Y0; + elim (tpr_inv_appl1 … H1) -H1 * +(* case 11: theta, flat (repeated) *) + [ #V2 #T2 #HV02 #HT02 #H destruct -X2 + @ex2_1_comm /3 width=11 by tpr_conf_flat_theta/ +(* case 12: theta, beta (repeated) *) + | #V2 #WW0 #TT0 #T2 #_ #_ #H destruct +(* case 13: theta, theta *) + | #V2 #VV2 #WW0 #W2 #TT0 #T2 #V02 #HW02 #HT02 #HVV2 #H1 #H2 destruct -W0 T0 X2 + /3 width=14 by tpr_conf_theta_theta/ (**) (* /3 width=14/ is too slow *) + ] +| #V0 #TT0 #T0 #T1 #HTT0 #HT01 #H1 #H2 destruct -Y0; + elim (tpr_inv_abbr1 … H1) -H1 * +(* case 14: zeta, delta (repeated) *) + [ #V2 #T2 #TT2 #HV02 #HT02 #HTT2 #H destruct -X2 + @ex2_1_comm /3 width=10 by tpr_conf_delta_zeta/ +(* case 15: zeta, zeta *) + | #T2 #HTT20 #HTX2 + /3 width=9 by tpr_conf_zeta_zeta/ (**) (* /3 width=9/ is too slow *) + ] +| #V0 #T0 #T1 #HT01 #H1 #H2 destruct -Y0; + elim (tpr_inv_cast1 … H1) -H1 +(* case 16: tau, flat (repeated) *) + [ * #V2 #T2 #HV02 #HT02 #H destruct -X2 + @ex2_1_comm /3 width=6 by tpr_conf_flat_cast/ +(* case 17: tau, tau *) + | #HT02 + /3 width=5 by tpr_conf_tau_tau/ + ] +] +qed. + +(* Basic_1: was: pr0_confluence *) +theorem tpr_conf: ∀T0:term. ∀T1,T2. T0 ⇒ T1 → T0 ⇒ T2 → + ∃∃T. T1 ⇒ T & T2 ⇒ T. +#T @(tw_wf_ind … T) -T /3 width=6 by tpr_conf_aux/ +qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpss.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpss.ma new file mode 100644 index 000000000..f640d1326 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpss.ma @@ -0,0 +1,94 @@ +(**************************************************************************) +(* ___ *) +(* ||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/unfold/ltpss_ltpss.ma". +include "Basic_2/reducibility/ltpr_ldrop.ma". + +(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) + +(* Unfold properties ********************************************************) + +(* Basic_1: was: pr0_subst1 *) +lemma tpr_tps_ltpr: ∀T1,T2. T1 ⇒ T2 → + ∀L1,d,e,U1. L1 ⊢ T1 [d, e] ≫ U1 → + ∀L2. L1 ⇒ L2 → + ∃∃U2. U1 ⇒ U2 & L2 ⊢ T2 [d, e] ≫* U2. +#T1 #T2 #H elim H -H T1 T2 +[ #I #L1 #d #e #X #H + elim (tps_inv_atom1 … H) -H + [ #H destruct -X /2/ + | * #K1 #V1 #i #Hdi #Hide #HLK1 #HVU1 #H #L2 #HL12 destruct -I; + elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 HL12 #X #HLK2 #H + elim (ltpr_inv_pair1 … H) -H #K2 #V2 #_ #HV12 #H destruct -X; + elim (lift_total V2 0 (i+1)) #U2 #HVU2 + lapply (tpr_lift … HV12 … HVU1 … HVU2) -HV12 HVU1 #HU12 + @ex2_1_intro [2: @HU12 | skip | /3/ ] (**) (* /4 width=6/ is too slow *) + ] +| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12 + elim (tps_inv_flat1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct -X; + elim (IHV12 … HVW1 … HL12) -IHV12 HVW1; + elim (IHT12 … HTU1 … HL12) -IHT12 HTU1 HL12 /3 width=5/ +| #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12 + elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct -X; + elim (tps_inv_bind1 … HY) -HY #WW #TT1 #_ #HTT1 #H destruct -Y; + elim (IHV12 … HVV1 … HL12) -IHV12 HVV1 #VV2 #HVV12 #HVV2 + elim (IHT12 … HTT1 (L2. 𝕓{Abst} WW) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2 + lapply (tpss_lsubs_conf … HTT2 (L2. 𝕓{Abbr} VV2) ?) -HTT2 /3 width=5/ +| #I #V1 #V2 #T1 #T2 #U2 #HV12 #_ #HTU2 #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12 + elim (tps_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct -X; + elim (IHV12 … HVV1 … HL12) -IHV12 HVV1 #VV2 #HVV12 #HVV2 + elim (IHT12 … HTT1 (L2. 𝕓{I} VV2) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2 + elim (tpss_strip_neq … HTT2 … HTU2 ?) -HTT2 HTU2 T2 /2/ #T2 #HTT2 #HUT2 + lapply (tps_lsubs_conf … HTT2 (L2. 𝕓{I} V2) ?) -HTT2 /2/ #HTT2 + elim (ltpss_tps_conf … HTT2 (L2. 𝕓{I} VV2) (d + 1) e ?) -HTT2 /2/ #W2 #HTTW2 #HTW2 + lapply (tpss_lsubs_conf … HTTW2 (⋆. 𝕓{I} VV2) ?) -HTTW2 /2/ #HTTW2 + lapply (tpss_tps … HTTW2) -HTTW2 #HTTW2 + lapply (tpss_lsubs_conf … HTW2 (L2. 𝕓{I} VV2) ?) -HTW2 /2/ #HTW2 + lapply (tpss_trans_eq … HUT2 … HTW2) -HUT2 HTW2 /3 width=5/ +| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #L1 #d #e #X #H #L2 #HL12 + elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct -X; + elim (tps_inv_bind1 … HY) -HY #WW1 #TT1 #HWW1 #HTT1 #H destruct -Y; + elim (IHV12 … HVV1 … HL12) -IHV12 HVV1 #VV2 #HVV12 #HVV2 + elim (IHW12 … HWW1 … HL12) -IHW12 HWW1 #WW2 #HWW12 #HWW2 + elim (IHT12 … HTT1 (L2. 𝕓{Abbr} WW2) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2 + elim (lift_total VV2 0 1) #VV #H2VV + lapply (tpss_lift_ge … HVV2 (L2. 𝕓{Abbr} WW2) … HV2 … H2VV) -HVV2 HV2 /2/ #HVV + @ex2_1_intro [2: @tpr_theta |1: skip |3: @tpss_bind [2: @tpss_flat ] ] /width=11/ (**) (* /4 width=11/ is too slow *) +| #V1 #TT1 #T1 #T2 #HT1 #_ #IHT12 #L1 #d #e #X #H #L2 #HL12 + elim (tps_inv_bind1 … H) -H #V2 #TT2 #HV12 #HTT12 #H destruct -X; + elim (tps_inv_lift1_ge … HTT12 L1 … HT1 ?) -HTT12 HT1 /2/ #T2 #HT12 #HTT2 + elim (IHT12 … HT12 … HL12) -IHT12 HT12 HL12 (tpr_inv_atom1 … H) -H #H ->(tpss_inv_sort1 … H) -H // -qed. - -(* Basic_1: was: pr2_gen_cast *) -lemma cpr_inv_cast1: ∀L,V1,T1,U2. L ⊢ 𝕔{Cast} V1. T1 ⇒ U2 → ( - ∃∃V2,T2. L ⊢ V1 ⇒ V2 & L ⊢ T1 ⇒ T2 & - U2 = 𝕔{Cast} V2. T2 - ) ∨ L ⊢ T1 ⇒ U2. -#L #V1 #T1 #U2 * #X #H #HU2 -elim (tpr_inv_cast1 … H) -H /3/ -* #V #T #HV1 #HT1 #H destruct -X; -elim (tpss_inv_flat1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H destruct -U2 /4 width=5/ -qed. - -(* Basic_1: removed theorems 5: - pr2_head_1 pr2_head_2 pr2_cflat pr2_gen_cflat clear_pr2_trans - Basic_1: removed local theorems 3: - pr2_free_free pr2_free_delta pr2_delta_delta -*) - -(* -pr2/fwd pr2_gen_appl -pr2/fwd pr2_gen_abbr -*) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr_cpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr_cpr.ma deleted file mode 100644 index ff802bfb3..000000000 --- a/matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr_cpr.ma +++ /dev/null @@ -1,58 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/reduction/tpr_tpr.ma". -include "Basic_2/reduction/cpr.ma". - -(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************) - -(* Advanced properties ******************************************************) - -lemma cpr_bind_sn: ∀I,L,V1,V2,T1,T2. L ⊢ V1 ⇒ V2 → T1 ⇒ T2 → - L ⊢ 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2. -#I #L #V1 #V2 #T1 #T2 * #V #HV1 #HV2 #HT12 -@ex2_1_intro [2: @(tpr_delta … HV1 HT12) | skip ] /2/ (* /3 width=5/ is too slow *) -qed. - -(* Basic_1: was only: pr2_gen_cbind *) -lemma cpr_bind_dx: ∀I,L,V1,V2,T1,T2. V1 ⇒ V2 → L. 𝕓{I} V2 ⊢ T1 ⇒ T2 → - L ⊢ 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2. -#I #L #V1 #V2 #T1 #T2 #HV12 * #T #HT1 normalize #HT2 -elim (tpss_split_up … HT2 1 ? ?) -HT2 // #T0 (tpr_inv_atom1 … H) -H #H -elim (tpss_inv_lref1 … H) -H /2/ -* /3 width=6/ -qed. - -(* Basic_1: was: pr2_gen_abst *) -lemma cpr_inv_abst1: ∀V1,T1,U2. 𝕔{Abst} V1. T1 ⇒ U2 → - ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Abst} V2. T2. -/2/ qed. - -(* Relocation properties ****************************************************) - -(* Basic_1: was: pr2_lift *) -lemma cpr_lift: ∀L,K,d,e. ↓[d, e] L ≡ K → - ∀T1,U1. ↑[d, e] T1 ≡ U1 → ∀T2,U2. ↑[d, e] T2 ≡ U2 → - K ⊢ T1 ⇒ T2 → L ⊢ U1 ⇒ U2. -#L #K #d #e #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 * #T #HT1 #HT2 -elim (lift_total T d e) #U #HTU -lapply (tpr_lift … HT1 … HTU1 … HTU) -T1 #HU1 -elim (lt_or_ge (|K|) d) #HKd -[ lapply (tpss_lift_le … HT2 … HLK HTU … HTU2) -T2 T HLK [ /2/ | /3/ ] -| lapply (tpss_lift_be … HT2 … HLK HTU … HTU2) -T2 T HLK // /3/ -] -qed. - -(* Basic_1: was: pr2_gen_lift *) -lemma cpr_inv_lift: ∀L,K,d,e. ↓[d, e] L ≡ K → - ∀T1,U1. ↑[d, e] T1 ≡ U1 → ∀U2. L ⊢ U1 ⇒ U2 → - ∃∃T2. ↑[d, e] T2 ≡ U2 & K ⊢ T1 ⇒ T2. -#L #K #d #e #HLK #T1 #U1 #HTU1 #U2 * #U #HU1 #HU2 -elim (tpr_inv_lift … HU1 … HTU1) -U1 #T #HTU #T1 -elim (lt_or_ge (|L|) d) #HLd -[ elim (tpss_inv_lift1_le … HU2 … HLK … HTU ?) -U HLK [ /5/ | /2/ ] -| elim (lt_or_ge (|L|) (d + e)) #HLde - [ elim (tpss_inv_lift1_be_up … HU2 … HLK … HTU ? ?) -U HLK // [ /5/ | /2/ ] - | elim (tpss_inv_lift1_be … HU2 … HLK … HTU ? ?) -U HLK // /5/ - ] -] -qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr_ltpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr_ltpr.ma deleted file mode 100644 index 3f80fb59c..000000000 --- a/matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr_ltpr.ma +++ /dev/null @@ -1,47 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/reduction/tpr_tpss.ma". -include "Basic_2/reduction/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 → - ∃∃U2. L2 ⊢ U1 ⇒ U2 & L2 ⊢ T2 [d, e] ≫* U2. -#L1 #L2 #HL12 #T1 #T2 * #T #HT1 #HT2 #d #e #U1 #HTU1 -elim (tpr_tpss_ltpr … HL12 … HT1 … HTU1) -L1 HT1 #U #HU1 #HTU -elim (tpss_conf_eq … HT2 … HTU) -T /3/ -qed. - -lemma cpr_ltpr_conf_eq: ∀L1,T1,T2. L1 ⊢ T1 ⇒ T2 → ∀L2. L1 ⇒ L2 → - ∃∃T. L2 ⊢ T1 ⇒ T & T2 ⇒ T. -#L1 #T1 #T2 * #T #HT1 #HT2 #L2 #HL12 ->(ltpr_fwd_length … HL12) in HT2 #HT2 -elim (tpr_tpss_ltpr … HL12 … HT2) -L1 HT2 /3/ -qed. - -lemma cpr_ltpr_conf_tpss: ∀L1,L2. L1 ⇒ L2 → ∀T1,T2. L1 ⊢ T1 ⇒ T2 → - ∀d,e,U1. L1 ⊢ T1 [d, e] ≫* U1 → - ∃∃U2. L2 ⊢ U1 ⇒ U2 & L2 ⊢ T2 ⇒ U2. -#L1 #L2 #HL12 #T1 #T2 #HT12 #d #e #U1 #HTU1 -elim (cpr_ltpr_conf_eq … HT12 … HL12) -HT12 #T #HT1 #HT2 -elim (cpr_tpss_ltpr … HL12 … HT1 … HTU1) -L1 HT1 #U2 #HU12 #HTU2 -lapply (tpss_weak_all … HTU2) -HTU2 #HTU2 /3 width=5/ (**) (* /4 width=5/ is too slow *) -qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reduction/lcpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reduction/lcpr.ma deleted file mode 100644 index 6e0920526..000000000 --- a/matita/matita/contribs/lambda_delta/Basic_2/reduction/lcpr.ma +++ /dev/null @@ -1,41 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/reduction/cpr.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) (*𝕓*) -. - -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. - -lemma lcpr_inv_item1: ∀K1,I,V1,L2. K1. 𝕓{I} V1 ⊢ ⇒ L2 → - ∃∃K2,V2. K1 ⊢ ⇒ K2 & K2 ⊢ V1 ⇒ V2 & L2 = K2. 𝕓{I} V2. -/2/ qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reduction/ltpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reduction/ltpr.ma deleted file mode 100644 index b7a01f3df..000000000 --- a/matita/matita/contribs/lambda_delta/Basic_2/reduction/ltpr.ma +++ /dev/null @@ -1,89 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/reduction/tpr.ma". - -(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************) - -inductive ltpr: relation lenv ≝ -| ltpr_sort: ltpr (⋆) (⋆) -| ltpr_item: ∀K1,K2,I,V1,V2. - ltpr K1 K2 → V1 ⇒ V2 → ltpr (K1. 𝕓{I} V1) (K2. 𝕓{I} V2) (*𝕓*) -. - -interpretation - "context-free parallel reduction (environment)" - 'PRed L1 L2 = (ltpr L1 L2). - -(* Basic properties *********************************************************) - -lemma ltpr_refl: ∀L:lenv. L ⇒ L. -#L elim L -L /2/ -qed. - -(* Basic inversion lemmas ***************************************************) - -fact ltpr_inv_atom1_aux: ∀L1,L2. L1 ⇒ L2 → L1 = ⋆ → L2 = ⋆. -#L1 #L2 * -L1 L2 -[ // -| #K1 #K2 #I #V1 #V2 #_ #_ #H destruct -] -qed. - -(* Basic_1: was: wcpr0_gen_sort *) -lemma ltpr_inv_atom1: ∀L2. ⋆ ⇒ L2 → L2 = ⋆. -/2/ qed. - -fact ltpr_inv_pair1_aux: ∀L1,L2. L1 ⇒ L2 → ∀K1,I,V1. L1 = K1. 𝕓{I} V1 → - ∃∃K2,V2. K1 ⇒ 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_1: was: wcpr0_gen_head *) -lemma ltpr_inv_pair1: ∀K1,I,V1,L2. K1. 𝕓{I} V1 ⇒ L2 → - ∃∃K2,V2. K1 ⇒ K2 & V1 ⇒ V2 & L2 = K2. 𝕓{I} V2. -/2/ qed. - -fact ltpr_inv_atom2_aux: ∀L1,L2. L1 ⇒ L2 → L2 = ⋆ → L1 = ⋆. -#L1 #L2 * -L1 L2 -[ // -| #K1 #K2 #I #V1 #V2 #_ #_ #H destruct -] -qed. - -lemma ltpr_inv_atom2: ∀L1. L1 ⇒ ⋆ → L1 = ⋆. -/2/ qed. - -fact ltpr_inv_pair2_aux: ∀L1,L2. L1 ⇒ L2 → ∀K2,I,V2. L2 = K2. 𝕓{I} V2 → - ∃∃K1,V1. K1 ⇒ K2 & V1 ⇒ V2 & L1 = K1. 𝕓{I} V1. -#L1 #L2 * -L1 L2 -[ #K2 #I #V2 #H destruct -| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #K #J #W #H destruct -K2 I V2 /2 width=5/ -] -qed. - -lemma ltpr_inv_pair2: ∀L1,K2,I,V2. L1 ⇒ K2. 𝕓{I} V2 → - ∃∃K1,V1. K1 ⇒ K2 & V1 ⇒ V2 & L1 = K1. 𝕓{I} V1. -/2/ qed. - -(* Basic forward lemmas *****************************************************) - -lemma ltpr_fwd_length: ∀L1,L2. L1 ⇒ L2 → |L1| = |L2|. -#L1 #L2 #H elim H -H L1 L2; normalize // -qed. - -(* Basic_1: removed theorems 2: wcpr0_getl wcpr0_getl_back *) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reduction/ltpr_ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/reduction/ltpr_ldrop.ma deleted file mode 100644 index 956bf1871..000000000 --- a/matita/matita/contribs/lambda_delta/Basic_2/reduction/ltpr_ldrop.ma +++ /dev/null @@ -1,52 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/reduction/tpr_lift.ma". -include "Basic_2/reduction/ltpr.ma". - -(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************) - -(* Basic_1: was: wcpr0_ldrop *) -lemma ltpr_ldrop_conf: ∀L1,K1,d,e. ↓[d, e] L1 ≡ K1 → ∀L2. L1 ⇒ L2 → - ∃∃K2. ↓[d, e] L2 ≡ K2 & K1 ⇒ K2. -#L1 #K1 #d #e #H elim H -H L1 K1 d e -[ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2/ -| #K1 #I #V1 #X #H - elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct /3 width=5/ -| #L1 #K1 #I #V1 #e #_ #IHLK1 #X #H - elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct -X; - elim (IHLK1 … HL12) -IHLK1 HL12 /3/ -| #L1 #K1 #I #V1 #W1 #d #e #_ #HWV1 #IHLK1 #X #H - elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct -X; - elim (tpr_inv_lift … HV12 … HWV1) -HV12 HWV1; - elim (IHLK1 … HL12) -IHLK1 HL12 /3 width=5/ -] -qed. - -(* Basic_1: was: wcpr0_ldrop_back *) -lemma ltpr_ldrop_trans: ∀L1,K1,d,e. ↓[d, e] L1 ≡ K1 → ∀K2. K1 ⇒ K2 → - ∃∃L2. ↓[d, e] L2 ≡ K2 & L1 ⇒ L2. -#L1 #K1 #d #e #H elim H -H L1 K1 d e -[ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2/ -| #K1 #I #V1 #X #H - elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=5/ -| #L1 #K1 #I #V1 #e #_ #IHLK1 #K2 #HK12 - elim (IHLK1 … HK12) -IHLK1 HK12 /3 width=5/ -| #L1 #K1 #I #V1 #W1 #d #e #_ #HWV1 #IHLK1 #X #H - elim (ltpr_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct -X; - elim (lift_total W2 d e) #V2 #HWV2 - lapply (tpr_lift … HW12 … HWV1 … HWV2) -HW12 HWV1; - elim (IHLK1 … HK12) -IHLK1 HK12 /3 width=5/ -] -qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reduction/tpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reduction/tpr.ma deleted file mode 100644 index db2c8c69f..000000000 --- a/matita/matita/contribs/lambda_delta/Basic_2/reduction/tpr.ma +++ /dev/null @@ -1,198 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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.ma". - -(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) - -(* Basic_1: includes: pr0_delta1 *) -inductive tpr: relation term ≝ -| tpr_atom : ∀I. tpr (𝕒{I}) (𝕒{I}) -| tpr_flat : ∀I,V1,V2,T1,T2. tpr V1 V2 → tpr T1 T2 → - tpr (𝕗{I} V1. T1) (𝕗{I} V2. T2) -| tpr_beta : ∀V1,V2,W,T1,T2. - tpr V1 V2 → tpr T1 T2 → - tpr (𝕔{Appl} V1. 𝕔{Abst} W. T1) (𝕔{Abbr} V2. T2) -| tpr_delta: ∀I,V1,V2,T1,T2,T. - tpr V1 V2 → tpr T1 T2 → ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ T → - tpr (𝕓{I} V1. T1) (𝕓{I} V2. T) -| tpr_theta: ∀V,V1,V2,W1,W2,T1,T2. - tpr V1 V2 → ↑[0,1] V2 ≡ V → tpr W1 W2 → tpr T1 T2 → - tpr (𝕔{Appl} V1. 𝕔{Abbr} W1. T1) (𝕔{Abbr} W2. 𝕔{Appl} V. T2) -| tpr_zeta : ∀V,T,T1,T2. ↑[0,1] T1 ≡ T → tpr T1 T2 → - tpr (𝕔{Abbr} V. T) T2 -| tpr_tau : ∀V,T1,T2. tpr T1 T2 → tpr (𝕔{Cast} V. T1) T2 -. - -interpretation - "context-free parallel reduction (term)" - 'PRed T1 T2 = (tpr T1 T2). - -(* Basic properties *********************************************************) - -lemma tpr_bind: ∀I,V1,V2,T1,T2. V1 ⇒ V2 → T1 ⇒ T2 → - 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2. -/2/ qed. - -(* Basic_1: was by definition: pr0_refl *) -lemma tpr_refl: ∀T. T ⇒ T. -#T elim T -T // -#I elim I -I /2/ -qed. - -(* Basic inversion lemmas ***************************************************) - -fact tpr_inv_atom1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I. U1 = 𝕒{I} → U2 = 𝕒{I}. -#U1 #U2 * -U1 U2 -[ // -| #I #V1 #V2 #T1 #T2 #_ #_ #k #H destruct -| #V1 #V2 #W #T1 #T2 #_ #_ #k #H destruct -| #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #k #H destruct -| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #k #H destruct -| #V #T #T1 #T2 #_ #_ #k #H destruct -| #V #T1 #T2 #_ #k #H destruct -] -qed. - -(* Basic_1: was: pr0_gen_sort pr0_gen_lref *) -lemma tpr_inv_atom1: ∀I,U2. 𝕒{I} ⇒ U2 → U2 = 𝕒{I}. -/2/ qed. - -fact tpr_inv_bind1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I,V1,T1. U1 = 𝕓{I} V1. T1 → - (∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 & - ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ T & - U2 = 𝕓{I} V2. T - ) ∨ - ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr. -#U1 #U2 * -U1 U2 -[ #J #I #V #T #H destruct -| #I1 #V1 #V2 #T1 #T2 #_ #_ #I #V #T #H destruct -| #V1 #V2 #W #T1 #T2 #_ #_ #I #V #T #H destruct -| #I1 #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #I0 #V0 #T0 #H destruct -I1 V1 T1 /3 width=7/ -| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #I0 #V0 #T0 #H destruct -| #V #T #T1 #T2 #HT1 #HT12 #I0 #V0 #T0 #H destruct -V T /3/ -| #V #T1 #T2 #_ #I0 #V0 #T0 #H destruct -] -qed. - -lemma tpr_inv_bind1: ∀V1,T1,U2,I. 𝕓{I} V1. T1 ⇒ U2 → - (∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 & - ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ T & - U2 = 𝕓{I} V2. T - ) ∨ - ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr. -/2/ qed. - -(* Basic_1: was pr0_gen_abbr *) -lemma tpr_inv_abbr1: ∀V1,T1,U2. 𝕓{Abbr} V1. T1 ⇒ U2 → - (∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 & - ⋆. 𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T & - U2 = 𝕓{Abbr} V2. T - ) ∨ - ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2. -#V1 #T1 #U2 #H -elim (tpr_inv_bind1 … H) -H * /3 width=7/ -qed. - -fact tpr_inv_flat1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I,V1,U0. U1 = 𝕗{I} V1. U0 → - ∨∨ ∃∃V2,T2. V1 ⇒ V2 & U0 ⇒ T2 & - U2 = 𝕗{I} V2. T2 - | ∃∃V2,W,T1,T2. V1 ⇒ V2 & T1 ⇒ T2 & - U0 = 𝕔{Abst} W. T1 & - U2 = 𝕔{Abbr} V2. T2 & I = Appl - | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 & - ↑[0,1] V2 ≡ V & - U0 = 𝕔{Abbr} W1. T1 & - U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2 & - I = Appl - | (U0 ⇒ U2 ∧ I = Cast). -#U1 #U2 * -U1 U2 -[ #I #J #V #T #H destruct -| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #J #V #T #H destruct -I V1 T1 /3 width=5/ -| #V1 #V2 #W #T1 #T2 #HV12 #HT12 #J #V #T #H destruct -J V1 T /3 width=8/ -| #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #J #V0 #T0 #H destruct -| #V #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #J #V0 #T0 #H - destruct -J V1 T0 /3 width=12/ -| #V #T #T1 #T2 #_ #_ #J #V0 #T0 #H destruct -| #V #T1 #T2 #HT12 #J #V0 #T0 #H destruct -J V T1 /3/ -] -qed. - -lemma tpr_inv_flat1: ∀V1,U0,U2,I. 𝕗{I} V1. U0 ⇒ U2 → - ∨∨ ∃∃V2,T2. V1 ⇒ V2 & U0 ⇒ T2 & - U2 = 𝕗{I} V2. T2 - | ∃∃V2,W,T1,T2. V1 ⇒ V2 & T1 ⇒ T2 & - U0 = 𝕔{Abst} W. T1 & - U2 = 𝕔{Abbr} V2. T2 & I = Appl - | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 & - ↑[0,1] V2 ≡ V & - U0 = 𝕔{Abbr} W1. T1 & - U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2 & - I = Appl - | (U0 ⇒ U2 ∧ I = Cast). -/2/ qed. - -(* Basic_1: was pr0_gen_appl *) -lemma tpr_inv_appl1: ∀V1,U0,U2. 𝕔{Appl} V1. U0 ⇒ U2 → - ∨∨ ∃∃V2,T2. V1 ⇒ V2 & U0 ⇒ T2 & - U2 = 𝕔{Appl} V2. T2 - | ∃∃V2,W,T1,T2. V1 ⇒ V2 & T1 ⇒ T2 & - U0 = 𝕔{Abst} W. T1 & - U2 = 𝕔{Abbr} V2. T2 - | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 & - ↑[0,1] V2 ≡ V & - U0 = 𝕔{Abbr} W1. T1 & - U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2. -#V1 #U0 #U2 #H -elim (tpr_inv_flat1 … H) -H * /3 width=12/ #_ #H destruct -qed. - -(* Basic_1: was: pr0_gen_cast *) -lemma tpr_inv_cast1: ∀V1,T1,U2. 𝕔{Cast} V1. T1 ⇒ U2 → - (∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Cast} V2. T2) - ∨ T1 ⇒ U2. -#V1 #T1 #U2 #H -elim (tpr_inv_flat1 … H) -H * /3 width=5/ -[ #V2 #W #W1 #W2 #_ #_ #_ #_ #H destruct -| #V2 #W #W1 #W2 #T2 #U1 #_ #_ #_ #_ #_ #_ #H destruct -] -qed. - -fact tpr_inv_lref2_aux: ∀T1,T2. T1 ⇒ T2 → ∀i. T2 = #i → - ∨∨ T1 = #i - | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i & - T1 = 𝕔{Abbr} V. T - | ∃∃V,T. T ⇒ #i & T1 = 𝕔{Cast} V. T. -#T1 #T2 * -T1 T2 -[ #I #i #H destruct /2/ -| #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct -| #V1 #V2 #W #T1 #T2 #_ #_ #i #H destruct -| #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #i #H destruct -| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #i #H destruct -| #V #T #T1 #T2 #HT1 #HT12 #i #H destruct /3 width=6/ -| #V #T1 #T2 #HT12 #i #H destruct /3/ -] -qed. - -lemma tpr_inv_lref2: ∀T1,i. T1 ⇒ #i → - ∨∨ T1 = #i - | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i & - T1 = 𝕔{Abbr} V. T - | ∃∃V,T. T ⇒ #i & T1 = 𝕔{Cast} V. T. -/2/ qed. - -(* Basic_1: removed theorems 3: - pr0_subst0_back pr0_subst0_fwd pr0_subst0 - Basic_1: removed local theorems: 1: pr0_delta_tau -*) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reduction/tpr_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/reduction/tpr_lift.ma deleted file mode 100644 index 7ebd4af8c..000000000 --- a/matita/matita/contribs/lambda_delta/Basic_2/reduction/tpr_lift.ma +++ /dev/null @@ -1,121 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/reduction/tpr.ma". - -(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) - -(* Relocation properties ****************************************************) - -(* Basic_1: was: pr0_lift *) -lemma tpr_lift: ∀T1,T2. T1 ⇒ T2 → - ∀d,e,U1. ↑[d, e] T1 ≡ U1 → ∀U2. ↑[d, e] T2 ≡ U2 → U1 ⇒ U2. -#T1 #T2 #H elim H -H T1 T2 -[ * #i #d #e #U1 #HU1 #U2 #HU2 - lapply (lift_mono … HU1 … HU2) -HU1 #H destruct -U1 - [ lapply (lift_inv_sort1 … HU2) -HU2 #H destruct -U2 // - | lapply (lift_inv_lref1 … HU2) * * #Hid #H destruct -U2 // - | lapply (lift_inv_gref1 … HU2) -HU2 #H destruct -U2 // - ] -| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2 - elim (lift_inv_flat1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct -X1; - elim (lift_inv_flat1 … HX2) -HX2 #W2 #U2 #HVW2 #HTU2 #HX2 destruct -X2 /3/ -| #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2 - elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct -X1; - elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct -X; - elim (lift_inv_bind1 … HX2) -HX2 #V3 #T3 #HV23 #HT23 #HX2 destruct -X2 /3/ -| #I #V1 #V2 #T1 #T2 #T0 #HV12 #HT12 #HT2 #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2 - elim (lift_inv_bind1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct -X1; - elim (lift_inv_bind1 … HX2) -HX2 #W2 #U0 #HVW2 #HTU0 #HX2 destruct -X2; - elim (lift_total T2 (d + 1) e) #U2 #HTU2 - @tpr_delta - [4: @(tps_lift_le … HT2 … HTU2 HTU0 ?) /2/ |1: skip |2: /2/ |3: /2/ ] (**) (*/3. is too slow *) -| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #d #e #X1 #HX1 #X2 #HX2 - elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct -X1; - elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct -X; - elim (lift_inv_bind1 … HX2) -HX2 #W3 #X #HW23 #HX #HX2 destruct -X2; - elim (lift_inv_flat1 … HX) -HX #V3 #T3 #HV3 #HT23 #HX destruct -X; - elim (lift_trans_ge … HV2 … HV3 ?) -HV2 HV3 V // /3/ -| #V #T #T1 #T2 #HT1 #_ #IHT12 #d #e #X #HX #T0 #HT20 - elim (lift_inv_bind1 … HX) -HX #V3 #T3 #_ #HT3 #HX destruct -X; - elim (lift_trans_ge … HT1 … HT3 ?) -HT1 HT3 T // /3 width=6/ -| #V #T1 #T2 #_ #IHT12 #d #e #X #HX #T #HT2 - elim (lift_inv_flat1 … HX) -HX #V0 #T0 #_ #HT0 #HX destruct -X /3/ -] -qed. - -(* Basic_1: was: pr0_gen_lift *) -lemma tpr_inv_lift: ∀T1,T2. T1 ⇒ T2 → - ∀d,e,U1. ↑[d, e] U1 ≡ T1 → - ∃∃U2. ↑[d, e] U2 ≡ T2 & U1 ⇒ U2. -#T1 #T2 #H elim H -H T1 T2 -[ * #i #d #e #U1 #HU1 - [ lapply (lift_inv_sort2 … HU1) -HU1 #H destruct -U1 /2/ - | lapply (lift_inv_lref2 … HU1) -HU1 * * #Hid #H destruct -U1 /3/ - | lapply (lift_inv_gref2 … HU1) -HU1 #H destruct -U1 /2/ - ] -| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X #HX - elim (lift_inv_flat2 … HX) -HX #V0 #T0 #HV01 #HT01 #HX destruct -X; - elim (IHV12 … HV01) -IHV12 HV01; - elim (IHT12 … HT01) -IHT12 HT01 /3 width=5/ -| #V1 #V2 #W1 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X #HX - elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct -X; - elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct -Y; - elim (IHV12 … HV01) -IHV12 HV01; - elim (IHT12 … HT01) -IHT12 HT01 /3 width=5/ -| #I #V1 #V2 #T1 #T2 #T0 #_ #_ #HT20 #IHV12 #IHT12 #d #e #X #HX - elim (lift_inv_bind2 … HX) -HX #W1 #U1 #HWV1 #HUT1 #HX destruct -X; - elim (IHV12 … HWV1) -IHV12 HWV1 #W2 #HWV2 #HW12 - elim (IHT12 … HUT1) -IHT12 HUT1 #U2 #HUT2 #HU12 - elim (tps_inv_lift1_le … HT20 … HUT2 ?) -HT20 HUT2 // [3: /2 width=5/ |2: skip ] #U0 #HU20 #HUT0 - @ex2_1_intro [2: /2/ |1: skip |3: /2/ ] (**) (* /3 width=5/ is slow *) -| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #d #e #X #HX - elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct -X; - elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct -Y; - elim (IHV12 … HV01) -IHV12 HV01 #V3 #HV32 #HV03 - elim (IHW12 … HW01) -IHW12 HW01 #W3 #HW32 #HW03 - elim (IHT12 … HT01) -IHT12 HT01 #T3 #HT32 #HT03 - elim (lift_trans_le … HV32 … HV2 ?) -HV32 HV2 V2 // #V2 #HV32 #HV2 - @ex2_1_intro [2: /3/ |1: skip |3: /2/ ] (**) (* /4 width=5/ is slow *) -| #V #T #T1 #T2 #HT1 #_ #IHT12 #d #e #X #HX - elim (lift_inv_bind2 … HX) -HX #V0 #T0 #_ #HT0 #H destruct -X; - elim (lift_div_le … HT1 … HT0 ?) -HT1 HT0 T // #T #HT0 #HT1 - elim (IHT12 … HT1) -IHT12 HT1 /3 width=5/ -| #V #T1 #T2 #_ #IHT12 #d #e #X #HX - elim (lift_inv_flat2 … HX) -HX #V0 #T0 #_ #HT01 #H destruct -X; - elim (IHT12 … HT01) -IHT12 HT01 /3/ -] -qed. - -(* Advanced inversion lemmas ************************************************) - -fact tpr_inv_abst1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕔{Abst} V1. T1 → - ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Abst} V2. T2. -#U1 #U2 * -U1 U2 -[ #I #V #T #H destruct -| #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct -| #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct -| #I #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #V0 #T0 #H destruct -I V1 T1; - <(tps_inv_refl_SO2 … HT2 ? ? ?) -HT2 T /2 width=5/ -| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #V0 #T0 #H destruct -| #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct -| #V #T1 #T2 #_ #V0 #T0 #H destruct -] -qed. - -(* Basic_1: was pr0_gen_abst *) -lemma tpr_inv_abst1: ∀V1,T1,U2. 𝕔{Abst} V1. T1 ⇒ U2 → - ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Abst} V2. T2. -/2/ qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reduction/tpr_tpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reduction/tpr_tpr.ma deleted file mode 100644 index f13d6af31..000000000 --- a/matita/matita/contribs/lambda_delta/Basic_2/reduction/tpr_tpr.ma +++ /dev/null @@ -1,287 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/reduction/tpr_tpss.ma". - -(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) - -(* Confluence lemmas ********************************************************) - -fact tpr_conf_atom_atom: ∀I. ∃∃X. 𝕒{I} ⇒ X & 𝕒{I} ⇒ X. -/2/ qed. - -fact tpr_conf_flat_flat: - ∀I,V0,V1,T0,T1,V2,T2. ( - ∀X0:term. #[X0] < #[V0] + #[T0] + 1 → - ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → - ∃∃X. X1 ⇒ X & X2 ⇒ X - ) → - V0 ⇒ V1 → V0 ⇒ V2 → T0 ⇒ T1 → T0 ⇒ T2 → - ∃∃T0. 𝕗{I} V1. T1 ⇒ T0 & 𝕗{I} V2. T2 ⇒ T0. -#I #V0 #V1 #T0 #T1 #V2 #T2 #IH #HV01 #HV02 #HT01 #HT02 -elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2 -elim (IH … HT01 … HT02) -HT01 HT02 /3 width=5/ -qed. - -fact tpr_conf_flat_beta: - ∀V0,V1,T1,V2,W0,U0,T2. ( - ∀X0:term. #[X0] < #[V0] + (#[W0] + #[U0] + 1) + 1 → - ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → - ∃∃X. X1 ⇒ X & X2 ⇒ X - ) → - V0 ⇒ V1 → V0 ⇒ V2 → - U0 ⇒ T2 → 𝕔{Abst} W0. U0 ⇒ T1 → - ∃∃X. 𝕔{Appl} V1. T1 ⇒ X & 𝕔{Abbr} V2. T2 ⇒ X. -#V0 #V1 #T1 #V2 #W0 #U0 #T2 #IH #HV01 #HV02 #HT02 #H -elim (tpr_inv_abst1 … H) -H #W1 #U1 #HW01 #HU01 #H destruct -T1; -elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2 -elim (IH … HT02 … HU01) -HT02 HU01 IH /3 width=5/ -qed. - -(* basic-1: was: - pr0_cong_upsilon_refl pr0_cong_upsilon_zeta - pr0_cong_upsilon_cong pr0_cong_upsilon_delta -*) -fact tpr_conf_flat_theta: - ∀V0,V1,T1,V2,V,W0,W2,U0,U2. ( - ∀X0:term. #[X0] < #[V0] + (#[W0] + #[U0] + 1) + 1 → - ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → - ∃∃X. X1 ⇒ X & X2 ⇒ X - ) → - V0 ⇒ V1 → V0 ⇒ V2 → ↑[O,1] V2 ≡ V → - W0 ⇒ W2 → U0 ⇒ U2 → 𝕔{Abbr} W0. U0 ⇒ T1 → - ∃∃X. 𝕔{Appl} V1. T1 ⇒ X & 𝕔{Abbr} W2. 𝕔{Appl} V. U2 ⇒ X. -#V0 #V1 #T1 #V2 #V #W0 #W2 #U0 #U2 #IH #HV01 #HV02 #HV2 #HW02 #HU02 #H -elim (IH … HV01 … HV02) -HV01 HV02 // #VV #HVV1 #HVV2 -elim (lift_total VV 0 1) #VVV #HVV -lapply (tpr_lift … HVV2 … HV2 … HVV) #HVVV -elim (tpr_inv_abbr1 … H) -H * -(* case 1: delta *) -[ -HV2 HVV2 #WW2 #UU2 #UU #HWW2 #HUU02 #HUU2 #H destruct -T1; - elim (IH … HW02 … HWW2) -HW02 HWW2 // #W #HW02 #HWW2 - elim (IH … HU02 … HUU02) -HU02 HUU02 IH // #U #HU2 #HUUU2 - elim (tpr_tps_bind … HWW2 HUUU2 … HUU2) -HUU2 HUUU2 #UUU #HUUU2 #HUUU1 - @ex2_1_intro - [2: @tpr_theta [6: @HVV |7: @HWW2 |8: @HUUU2 |1,2,3,4: skip | // ] - |1:skip - |3: @tpr_delta [3: @tpr_flat |1: skip ] /2 width=5/ - ] (**) (* /5 width=14/ is too slow *) -(* case 3: zeta *) -| -HW02 HVV HVVV #UU1 #HUU10 #HUUT1 - elim (tpr_inv_lift … HU02 … HUU10) -HU02 #UU #HUU2 #HUU1 - lapply (tw_lift … HUU10) -HUU10 #HUU10 - elim (IH … HUUT1 … HUU1) -HUUT1 HUU1 IH // -HUU10 #U #HU2 #HUUU2 - @ex2_1_intro - [2: @tpr_flat - |1: skip - |3: @tpr_zeta [2: @lift_flat |1: skip |3: @tpr_flat ] - ] /2 width=5/ (**) (* /5 width=5/ is too slow *) -] -qed. - -fact tpr_conf_flat_cast: - ∀X2,V0,V1,T0,T1. ( - ∀X0:term. #[X0] < #[V0] + #[T0] + 1 → - ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → - ∃∃X. X1 ⇒ X & X2 ⇒ X - ) → - V0 ⇒ V1 → T0 ⇒ T1 → T0 ⇒ X2 → - ∃∃X. 𝕔{Cast} V1. T1 ⇒ X & X2 ⇒ X. -#X2 #V0 #V1 #T0 #T1 #IH #_ #HT01 #HT02 -elim (IH … HT01 … HT02) -HT01 HT02 IH /3/ -qed. - -fact tpr_conf_beta_beta: - ∀W0:term. ∀V0,V1,T0,T1,V2,T2. ( - ∀X0:term. #[X0] < #[V0] + (#[W0] + #[T0] + 1) + 1 → - ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → - ∃∃X. X1 ⇒ X & X2 ⇒ X - ) → - V0 ⇒ V1 → V0 ⇒ V2 → T0 ⇒ T1 → T0 ⇒ T2 → - ∃∃X. 𝕔{Abbr} V1. T1 ⇒X & 𝕔{Abbr} V2. T2 ⇒ X. -#W0 #V0 #V1 #T0 #T1 #V2 #T2 #IH #HV01 #HV02 #HT01 #HT02 -elim (IH … HV01 … HV02) -HV01 HV02 // -elim (IH … HT01 … HT02) -HT01 HT02 IH /3 width=5/ -qed. - -(* Basic_1: was: pr0_cong_delta pr0_delta_delta *) -fact tpr_conf_delta_delta: - ∀I1,V0,V1,T0,T1,TT1,V2,T2,TT2. ( - ∀X0:term. #[X0] < #[V0] + #[T0] + 1 → - ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → - ∃∃X. X1 ⇒ X & X2 ⇒ X - ) → - V0 ⇒ V1 → V0 ⇒ V2 → T0 ⇒ T1 → T0 ⇒ T2 → - ⋆. 𝕓{I1} V1 ⊢ T1 [O, 1] ≫ TT1 → - ⋆. 𝕓{I1} V2 ⊢ T2 [O, 1] ≫ TT2 → - ∃∃X. 𝕓{I1} V1. TT1 ⇒ X & 𝕓{I1} V2. TT2 ⇒ X. -#I1 #V0 #V1 #T0 #T1 #TT1 #V2 #T2 #TT2 #IH #HV01 #HV02 #HT01 #HT02 #HTT1 #HTT2 -elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2 -elim (IH … HT01 … HT02) -HT01 HT02 IH // #T #HT1 #HT2 -elim (tpr_tps_bind … HV1 HT1 … HTT1) -HT1 HTT1 #U1 #TTU1 #HTU1 -elim (tpr_tps_bind … HV2 HT2 … HTT2) -HT2 HTT2 #U2 #TTU2 #HTU2 -elim (tps_conf_eq … HTU1 … HTU2) -HTU1 HTU2 #U #HU1 #HU2 -@ex2_1_intro [2,3: @tpr_delta |1: skip ] /width=10/ (**) (* /3 width=10/ is too slow *) -qed. - -fact tpr_conf_delta_zeta: - ∀X2,V0,V1,T0,T1,TT1,T2. ( - ∀X0:term. #[X0] < #[V0] + #[T0] + 1 → - ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → - ∃∃X. X1 ⇒ X & X2 ⇒ X - ) → - V0 ⇒ V1 → T0 ⇒ T1 → ⋆. 𝕓{Abbr} V1 ⊢ T1 [O,1] ≫ TT1 → - T2 ⇒ X2 → ↑[O, 1] T2 ≡ T0 → - ∃∃X. 𝕓{Abbr} V1. TT1 ⇒ X & X2 ⇒ X. -#X2 #V0 #V1 #T0 #T1 #TT1 #T2 #IH #_ #HT01 #HTT1 #HTX2 #HTT20 -elim (tpr_inv_lift … HT01 … HTT20) -HT01 #TT2 #HTT21 #HTT2 -lapply (tps_inv_lift1_eq … HTT1 … HTT21) -HTT1 #HTT1 destruct -T1; -lapply (tw_lift … HTT20) -HTT20 #HTT20 -elim (IH … HTX2 … HTT2) -HTX2 HTT2 IH /3/ -qed. - -(* Basic_1: was: pr0_upsilon_upsilon *) -fact tpr_conf_theta_theta: - ∀VV1,V0,V1,W0,W1,T0,T1,V2,VV2,W2,T2. ( - ∀X0:term. #[X0] < #[V0] + (#[W0] + #[T0] + 1) + 1 → - ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → - ∃∃X. X1 ⇒ X & X2 ⇒ X - ) → - V0 ⇒ V1 → V0 ⇒ V2 → W0 ⇒ W1 → W0 ⇒ W2 → T0 ⇒ T1 → T0 ⇒ T2 → - ↑[O, 1] V1 ≡ VV1 → ↑[O, 1] V2 ≡ VV2 → - ∃∃X. 𝕔{Abbr} W1. 𝕔{Appl} VV1. T1 ⇒ X & 𝕔{Abbr} W2. 𝕔{Appl} VV2. T2 ⇒ X. -#VV1 #V0 #V1 #W0 #W1 #T0 #T1 #V2 #VV2 #W2 #T2 #IH #HV01 #HV02 #HW01 #HW02 #HT01 #HT02 #HVV1 #HVV2 -elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2 -elim (IH … HW01 … HW02) -HW01 HW02 // #W #HW1 #HW2 -elim (IH … HT01 … HT02) -HT01 HT02 IH // #T #HT1 #HT2 -elim (lift_total V 0 1) #VV #HVV -lapply (tpr_lift … HV1 … HVV1 … HVV) -HV1 HVV1 #HVV1 -lapply (tpr_lift … HV2 … HVV2 … HVV) -HV2 HVV2 HVV #HVV2 -@ex2_1_intro [2,3: @tpr_bind |1:skip ] /2 width=5/ (**) (* /4 width=5/ is too slow *) -qed. - -fact tpr_conf_zeta_zeta: - ∀V0:term. ∀X2,TT0,T0,T1,T2. ( - ∀X0:term. #[X0] < #[V0] + #[TT0] + 1 → - ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → - ∃∃X. X1 ⇒ X & X2 ⇒ X - ) → - T0 ⇒ T1 → T2 ⇒ X2 → - ↑[O, 1] T0 ≡ TT0 → ↑[O, 1] T2 ≡ TT0 → - ∃∃X. T1 ⇒ X & X2 ⇒ X. -#V0 #X2 #TT0 #T0 #T1 #T2 #IH #HT01 #HTX2 #HTT0 #HTT20 -lapply (lift_inj … HTT0 … HTT20) -HTT0 #H destruct -T0; -lapply (tw_lift … HTT20) -HTT20 #HTT20 -elim (IH … HT01 … HTX2) -HT01 HTX2 IH /2/ -qed. - -fact tpr_conf_tau_tau: - ∀V0,T0:term. ∀X2,T1. ( - ∀X0:term. #[X0] < #[V0] + #[T0] + 1 → - ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → - ∃∃X. X1 ⇒ X & X2 ⇒ X - ) → - T0 ⇒ T1 → T0 ⇒ X2 → - ∃∃X. T1 ⇒ X & X2 ⇒ X. -#V0 #T0 #X2 #T1 #IH #HT01 #HT02 -elim (IH … HT01 … HT02) -HT01 HT02 IH /2/ -qed. - -(* Confluence ***************************************************************) - -fact tpr_conf_aux: - ∀Y0:term. ( - ∀X0:term. #[X0] < #[Y0] → - ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → - ∃∃X. X1 ⇒ X & X2 ⇒ X - ) → - ∀X0,X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → X0 = Y0 → - ∃∃X. X1 ⇒ X & X2 ⇒ X. -#Y0 #IH #X0 #X1 #X2 * -X0 X1 -[ #I1 #H1 #H2 destruct -Y0; - lapply (tpr_inv_atom1 … H1) -H1 -(* case 1: atom, atom *) - #H1 destruct -X2 // -| #I #V0 #V1 #T0 #T1 #HV01 #HT01 #H1 #H2 destruct -Y0; - elim (tpr_inv_flat1 … H1) -H1 * -(* case 2: flat, flat *) - [ #V2 #T2 #HV02 #HT02 #H destruct -X2 - /3 width=7 by tpr_conf_flat_flat/ (**) (* /3 width=7/ is too slow *) -(* case 3: flat, beta *) - | #V2 #W #U0 #T2 #HV02 #HT02 #H1 #H2 #H3 destruct -T0 X2 I - /3 width=8 by tpr_conf_flat_beta/ (**) (* /3 width=8/ is too slow *) -(* case 4: flat, theta *) - | #V2 #V #W0 #W2 #U0 #U2 #HV02 #HW02 #HT02 #HV2 #H1 #H2 #H3 destruct -T0 X2 I - /3 width=11 by tpr_conf_flat_theta/ (**) (* /3 width=11/ is too slow *) -(* case 5: flat, tau *) - | #HT02 #H destruct -I - /3 width=6 by tpr_conf_flat_cast/ (**) (* /3 width=6/ is too slow *) - ] -| #V0 #V1 #W0 #T0 #T1 #HV01 #HT01 #H1 #H2 destruct -Y0; - elim (tpr_inv_appl1 … H1) -H1 * -(* case 6: beta, flat (repeated) *) - [ #V2 #T2 #HV02 #HT02 #H destruct -X2 - @ex2_1_comm /3 width=8 by tpr_conf_flat_beta/ -(* case 7: beta, beta *) - | #V2 #WW0 #TT0 #T2 #HV02 #HT02 #H1 #H2 destruct -W0 T0 X2 - /3 width=8 by tpr_conf_beta_beta/ (**) (* /3 width=8/ is too slow *) -(* case 8, beta, theta (excluded) *) - | #V2 #VV2 #WW0 #W2 #TT0 #T2 #_ #_ #_ #_ #H destruct - ] -| #I1 #V0 #V1 #T0 #T1 #TT1 #HV01 #HT01 #HTT1 #H1 #H2 destruct -Y0; - elim (tpr_inv_bind1 … H1) -H1 * -(* case 9: delta, delta *) - [ #V2 #T2 #TT2 #HV02 #HT02 #HTT2 #H destruct -X2 - /3 width=11 by tpr_conf_delta_delta/ (**) (* /3 width=11/ is too slow *) -(* case 10: delta, zata *) - | #T2 #HT20 #HTX2 #H destruct -I1; - /3 width=10 by tpr_conf_delta_zeta/ (**) (* /3 width=10/ is too slow *) - ] -| #VV1 #V0 #V1 #W0 #W1 #T0 #T1 #HV01 #HVV1 #HW01 #HT01 #H1 #H2 destruct -Y0; - elim (tpr_inv_appl1 … H1) -H1 * -(* case 11: theta, flat (repeated) *) - [ #V2 #T2 #HV02 #HT02 #H destruct -X2 - @ex2_1_comm /3 width=11 by tpr_conf_flat_theta/ -(* case 12: theta, beta (repeated) *) - | #V2 #WW0 #TT0 #T2 #_ #_ #H destruct -(* case 13: theta, theta *) - | #V2 #VV2 #WW0 #W2 #TT0 #T2 #V02 #HW02 #HT02 #HVV2 #H1 #H2 destruct -W0 T0 X2 - /3 width=14 by tpr_conf_theta_theta/ (**) (* /3 width=14/ is too slow *) - ] -| #V0 #TT0 #T0 #T1 #HTT0 #HT01 #H1 #H2 destruct -Y0; - elim (tpr_inv_abbr1 … H1) -H1 * -(* case 14: zeta, delta (repeated) *) - [ #V2 #T2 #TT2 #HV02 #HT02 #HTT2 #H destruct -X2 - @ex2_1_comm /3 width=10 by tpr_conf_delta_zeta/ -(* case 15: zeta, zeta *) - | #T2 #HTT20 #HTX2 - /3 width=9 by tpr_conf_zeta_zeta/ (**) (* /3 width=9/ is too slow *) - ] -| #V0 #T0 #T1 #HT01 #H1 #H2 destruct -Y0; - elim (tpr_inv_cast1 … H1) -H1 -(* case 16: tau, flat (repeated) *) - [ * #V2 #T2 #HV02 #HT02 #H destruct -X2 - @ex2_1_comm /3 width=6 by tpr_conf_flat_cast/ -(* case 17: tau, tau *) - | #HT02 - /3 width=5 by tpr_conf_tau_tau/ - ] -] -qed. - -(* Basic_1: was: pr0_confluence *) -theorem tpr_conf: ∀T0:term. ∀T1,T2. T0 ⇒ T1 → T0 ⇒ T2 → - ∃∃T. T1 ⇒ T & T2 ⇒ T. -#T @(tw_wf_ind … T) -T /3 width=6 by tpr_conf_aux/ -qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reduction/tpr_tpss.ma b/matita/matita/contribs/lambda_delta/Basic_2/reduction/tpr_tpss.ma deleted file mode 100644 index 30d7a4bb8..000000000 --- a/matita/matita/contribs/lambda_delta/Basic_2/reduction/tpr_tpss.ma +++ /dev/null @@ -1,94 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/unfold/ltpss_ltpss.ma". -include "Basic_2/reduction/ltpr_ldrop.ma". - -(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) - -(* Unfold properties ********************************************************) - -(* Basic_1: was: pr0_subst1 *) -lemma tpr_tps_ltpr: ∀T1,T2. T1 ⇒ T2 → - ∀L1,d,e,U1. L1 ⊢ T1 [d, e] ≫ U1 → - ∀L2. L1 ⇒ L2 → - ∃∃U2. U1 ⇒ U2 & L2 ⊢ T2 [d, e] ≫* U2. -#T1 #T2 #H elim H -H T1 T2 -[ #I #L1 #d #e #X #H - elim (tps_inv_atom1 … H) -H - [ #H destruct -X /2/ - | * #K1 #V1 #i #Hdi #Hide #HLK1 #HVU1 #H #L2 #HL12 destruct -I; - elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 HL12 #X #HLK2 #H - elim (ltpr_inv_pair1 … H) -H #K2 #V2 #_ #HV12 #H destruct -X; - elim (lift_total V2 0 (i+1)) #U2 #HVU2 - lapply (tpr_lift … HV12 … HVU1 … HVU2) -HV12 HVU1 #HU12 - @ex2_1_intro [2: @HU12 | skip | /3/ ] (**) (* /4 width=6/ is too slow *) - ] -| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12 - elim (tps_inv_flat1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct -X; - elim (IHV12 … HVW1 … HL12) -IHV12 HVW1; - elim (IHT12 … HTU1 … HL12) -IHT12 HTU1 HL12 /3 width=5/ -| #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12 - elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct -X; - elim (tps_inv_bind1 … HY) -HY #WW #TT1 #_ #HTT1 #H destruct -Y; - elim (IHV12 … HVV1 … HL12) -IHV12 HVV1 #VV2 #HVV12 #HVV2 - elim (IHT12 … HTT1 (L2. 𝕓{Abst} WW) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2 - lapply (tpss_lsubs_conf … HTT2 (L2. 𝕓{Abbr} VV2) ?) -HTT2 /3 width=5/ -| #I #V1 #V2 #T1 #T2 #U2 #HV12 #_ #HTU2 #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12 - elim (tps_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct -X; - elim (IHV12 … HVV1 … HL12) -IHV12 HVV1 #VV2 #HVV12 #HVV2 - elim (IHT12 … HTT1 (L2. 𝕓{I} VV2) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2 - elim (tpss_strip_neq … HTT2 … HTU2 ?) -HTT2 HTU2 T2 /2/ #T2 #HTT2 #HUT2 - lapply (tps_lsubs_conf … HTT2 (L2. 𝕓{I} V2) ?) -HTT2 /2/ #HTT2 - elim (ltpss_tps_conf … HTT2 (L2. 𝕓{I} VV2) (d + 1) e ?) -HTT2 /2/ #W2 #HTTW2 #HTW2 - lapply (tpss_lsubs_conf … HTTW2 (⋆. 𝕓{I} VV2) ?) -HTTW2 /2/ #HTTW2 - lapply (tpss_tps … HTTW2) -HTTW2 #HTTW2 - lapply (tpss_lsubs_conf … HTW2 (L2. 𝕓{I} VV2) ?) -HTW2 /2/ #HTW2 - lapply (tpss_trans_eq … HUT2 … HTW2) -HUT2 HTW2 /3 width=5/ -| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #L1 #d #e #X #H #L2 #HL12 - elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct -X; - elim (tps_inv_bind1 … HY) -HY #WW1 #TT1 #HWW1 #HTT1 #H destruct -Y; - elim (IHV12 … HVV1 … HL12) -IHV12 HVV1 #VV2 #HVV12 #HVV2 - elim (IHW12 … HWW1 … HL12) -IHW12 HWW1 #WW2 #HWW12 #HWW2 - elim (IHT12 … HTT1 (L2. 𝕓{Abbr} WW2) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2 - elim (lift_total VV2 0 1) #VV #H2VV - lapply (tpss_lift_ge … HVV2 (L2. 𝕓{Abbr} WW2) … HV2 … H2VV) -HVV2 HV2 /2/ #HVV - @ex2_1_intro [2: @tpr_theta |1: skip |3: @tpss_bind [2: @tpss_flat ] ] /width=11/ (**) (* /4 width=11/ is too slow *) -| #V1 #TT1 #T1 #T2 #HT1 #_ #IHT12 #L1 #d #e #X #H #L2 #HL12 - elim (tps_inv_bind1 … H) -H #V2 #TT2 #HV12 #HTT12 #H destruct -X; - elim (tps_inv_lift1_ge … HTT12 L1 … HT1 ?) -HTT12 HT1 /2/ #T2 #HT12 #HTT2 - elim (IHT12 … HT12 … HL12) -IHT12 HT12 HL12 (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 }. +