From: Ferruccio Guidi Date: Sat, 29 Sep 2012 17:28:48 +0000 (+0000) Subject: - full commit for the transtive closure of ltpss! X-Git-Tag: make_still_working~1502 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cc21d0caa6229b7d1a905f9b62de2af4f40cc863;p=helm.git - full commit for the transtive closure of ltpss! --- diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_ltpss.ma index 6dc6714a9..43385668b 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_ltpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_ltpss.ma @@ -18,24 +18,24 @@ include "basic_2/equivalence/cpcs_cpcs.ma". (* Properties concerning partial unfold on local environments ***************) -lemma ltpss_cpr_conf: ∀L1,L2,d,e. L1 ▶* [d, e] L2 → - ∀T1,T2. L1 ⊢ T1 ➡ T2 → L2 ⊢ T1 ⬌* T2. +lemma ltpss_dx_cpr_conf: ∀L1,L2,d,e. L1 ▶* [d, e] L2 → + ∀T1,T2. L1 ⊢ T1 ➡ T2 → L2 ⊢ T1 ⬌* T2. #L1 #L2 #d #e #HL12 #T1 #T2 * -lapply (ltpss_weak_all … HL12) ->(ltpss_fwd_length … HL12) -HL12 #HL12 #T #HT1 #HT2 -elim (ltpss_tpss_conf … HT2 … HL12) -L1 #T0 #HT0 #HT20 +lapply (ltpss_dx_weak_all … HL12) +>(ltpss_dx_fwd_length … HL12) -HL12 #HL12 #T #HT1 #HT2 +elim (ltpss_dx_tpss_conf … HT2 … HL12) -L1 #T0 #HT0 #HT20 @(cprs_div … T0) /3 width=3/ (**) (* /4/ is too slow *) qed. -lemma ltpss_cprs_conf: ∀L1,L2,d,e. L1 ▶* [d, e] L2 → - ∀T1,T2. L1 ⊢ T1 ➡* T2 → L2 ⊢ T1 ⬌* T2. +lemma ltpss_dx_cprs_conf: ∀L1,L2,d,e. L1 ▶* [d, e] L2 → + ∀T1,T2. L1 ⊢ T1 ➡* T2 → L2 ⊢ T1 ⬌* T2. #L1 #L2 #d #e #HL12 #T1 #T2 #H @(cprs_ind … H) -T2 // #T #T2 #_ #HT2 #IHT1 @(cpcs_trans … IHT1) -T1 /2 width=5/ qed. -lemma ltpss_cpcs_conf: ∀L1,L2,d,e. L1 ▶* [d, e] L2 → - ∀T1,T2. L1 ⊢ T1 ⬌* T2 → L2 ⊢ T1 ⬌* T2. +lemma ltpss_dx_cpcs_conf: ∀L1,L2,d,e. L1 ▶* [d, e] L2 → + ∀T1,T2. L1 ⊢ T1 ⬌* T2 → L2 ⊢ T1 ⬌* T2. #L1 #L2 #d #e #HL12 #T1 #T2 #H elim (cpcs_inv_cprs … H) -H #T #HT1 #HT2 @(cpcs_canc_dx … T) /2 width=5/ diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/cpr_ltpsss.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/cpr_ltpsss.etc deleted file mode 100644 index 0890e462b..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/cpr_ltpsss.etc +++ /dev/null @@ -1,25 +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/ltpsss.ma". -include "basic_2/reducibility/cpr_ltpss.ma". - -(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************) - -(* Properties on iterated partial unfold on local environments **************) - -lemma ltpsss_cpr_trans: ∀L1,L2,d,e. L1 [d, e] ▶** L2 → - ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡ T2. -#L1 #L2 #d #e #HL12 #T1 #T2 #HT12 @(ltpsss_ind_dx … HL12) -L1 // /2 width=5/ -qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/cprs_lcpr.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/cprs_lcpr.etc deleted file mode 100644 index bb7896c30..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/cprs_lcpr.etc +++ /dev/null @@ -1,46 +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/reducibility/ltpr_tps.ma". -include "basic_2/reducibility/cpr_ltpsss.ma". -include "basic_2/reducibility/lcpr.ma". -include "basic_2/computation/cprs.ma". - -(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) - -(* Properties concerning context-sensitive parallel reduction on lenv's *****) - -lemma ltpr_tpss_trans: ∀L1,L2. L1 ➡ L2 → ∀T1,T2,d,e. L2 ⊢ T1 [d, e] ▶* T2 → - ∃∃T. L1 ⊢ T1 [d, e] ▶* T & L1 ⊢ T ➡* T2. -#L1 #L2 #HL12 #T1 #T2 #d #e #H @(tpss_ind … H) -T2 -[ /2 width=3/ -| #T #T2 #_ #HT2 * #T0 #HT10 #HT0 - elim (ltpr_tps_trans … HT2 … HL12) -L2 #T3 #HT3 #HT32 - @(ex2_1_intro … HT10) -T1 (**) (* explicit constructors *) - @(cprs_strap1 … T3 …) /2 width=1/ -HT32 - @(cprs_strap1 … HT0) -HT0 /3 width=3/ -] -qed. - -(* Basic_1: was just: pr3_pr0_pr2_t *) -lemma ltpr_cpr_trans: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡* T2. -#L1 #L2 #HL12 #T1 #T2 * #T #HT1 -<(ltpr_fwd_length … HL12) #HT2 -elim (ltpr_tpss_trans … HL12 … HT2) -L2 /3 width=3/ -qed. - -(* Basic_1: was just: pr3_pr2_pr2_t *) -lemma lcpr_cpr_trans: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡* T2. -#L1 #L2 * /3 width=7/ -qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr.etc deleted file mode 100644 index 4d8a341bc..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr.etc +++ /dev/null @@ -1,37 +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/ltpsss.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 width=3/ qed. - -(* Basic inversion lemmas ***************************************************) - -lemma lcpr_inv_atom1: ∀L2. ⋆ ⊢ ➡ L2 → L2 = ⋆. -#L2 * #L #HL >(ltpr_inv_atom1 … HL) -HL #HL2 >(ltpsss_inv_atom1 … HL2) -HL2 // -qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr_aaa.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr_aaa.etc deleted file mode 100644 index 77f384e58..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr_aaa.etc +++ /dev/null @@ -1,34 +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/static/aaa_ltpsss.ma". -include "basic_2/reducibility/ltpr_aaa.ma". -include "basic_2/reducibility/cpr.ma". -include "basic_2/reducibility/lcpr.ma". - -(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *************) - -(* Properties about atomic arity assignment on terms ************************) - -lemma aaa_lcpr_conf: ∀L1,T,A. L1 ⊢ T ÷ A → ∀L2. L1 ⊢ ➡ L2 → L2 ⊢ T ÷ A. -#L1 #T #A #HT #L2 * /3 width=5/ -qed. - -lemma aaa_cpr_conf: ∀L,T1,A. L ⊢ T1 ÷ A → ∀T2. L ⊢ T1 ➡ T2 → L ⊢ T2 ÷ A. -#L #T1 #A #HT1 #T2 * /3 width=5/ -qed. - -lemma aaa_lcpr_cpr_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2. L1 ⊢ ➡ L2 → - ∀T2. L2 ⊢ T1 ➡ T2 → L2 ⊢ T2 ÷ A. -/3 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr_cpr.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr_cpr.etc deleted file mode 100644 index 3d833fc02..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr_cpr.etc +++ /dev/null @@ -1,27 +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/ltpsss_ltpsss.ma". -include "basic_2/reducibility/cpr.ma". -include "basic_2/reducibility/lcpr.ma". - -(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *************) - -(* Advanced properties ****************************************************) - -lemma lcpr_pair: ∀L1,L2. L1 ⊢ ➡ L2 → ∀V1,V2. L2 ⊢ V1 ➡ V2 → - ∀I. L1. ⓑ{I} V1 ⊢ ➡ L2. ⓑ{I} V2. -#L1 #L2 * #L #HL1 #HL2 #V1 #V2 * -<(ltpsss_fwd_length … HL2) /4 width=5/ -qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr_lcpr.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr_lcpr.etc deleted file mode 100644 index 5d7e4739e..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr_lcpr.etc +++ /dev/null @@ -1,40 +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/ltpsss_ltpsss.ma". -include "basic_2/reducibility/ltpr_ltpsss.ma". -include "basic_2/reducibility/ltpr_ltpr.ma". -include "basic_2/reducibility/lcpr.ma". - -(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ***************) - -(* Main properties **********************************************************) - -theorem lcpr_conf: ∀L0,L1,L2. L0 ⊢ ➡ L1 → L0 ⊢ ➡ L2 → - ∃∃L. L1 ⊢ ➡ L & L2 ⊢ ➡ L. -#K0 #L1 #L2 * #K1 #HK01 #HKL1 * #K2 #HK02 #HKL2 -lapply (ltpr_fwd_length … HK01) #H ->(ltpr_fwd_length … HK02) in H; #H -elim (ltpr_conf … HK01 … HK02) -K0 #K #HK1 #HK2 -lapply (ltpsss_fwd_length … HKL1) #H1 -lapply (ltpsss_fwd_length … HKL2) #H2 ->H1 in HKL1 H; -H1 #HKL1 ->H2 in HKL2; -H2 #HKL2 #H -elim (ltpr_ltpsss_conf … HKL1 … HK1) -K1 #K1 #HK1 #HLK1 -elim (ltpr_ltpsss_conf … HKL2 … HK2) -K2 #K2 #HK2 #HLK2 -elim (ltpsss_conf … HK1 … HK2) -K #K #HK1 #HK2 -lapply (ltpr_fwd_length … HLK1) #H1 -lapply (ltpr_fwd_length … HLK2) #H2 -/3 width=5/ -qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpr_ltpsss.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpr_ltpsss.etc deleted file mode 100644 index d0c29e726..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpr_ltpsss.etc +++ /dev/null @@ -1,28 +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/ltpsss.ma". -include "basic_2/reducibility/ltpr_ltpss.ma". - -(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************) - -(* Properties on iterated parallel unfold on local environments *************) - -lemma ltpr_ltpsss_conf: ∀L1,K1,d,e. L1 [d, e] ▶** K1 → ∀L2. L1 ➡ L2 → - ∃∃K2. L2 [d, e] ▶** K2 & K1 ➡ K2. -#L1 #K1 #d #e #H @(ltpsss_ind … H) -K1 /2 width=3/ -#K #K1 #_ #HK1 #IHK #L2 #HL12 -elim (IHK … HL12) -L1 #K2 #HLK2 #HK2 -elim (ltpr_ltpss_conf … HK1 … HK2) -K /3 width=3/ -qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/top/lenv_top.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/top/lenv_top.etc new file mode 100644 index 000000000..ab90cebe7 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/top/lenv_top.etc @@ -0,0 +1,68 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +notation "hvbox( T1 𝟙 break term 46 T2 )" + non associative with precedence 45 + for @{ 'RTop $T1 $T2 }. + +include "basic_2/grammar/lenv_px.ma". + +(* POINTWISE EXTENSION OF TOP RELATION FOR TERMS ****************************) + +definition ttop: relation term ≝ λT1,T2. True. + +definition ltop: relation lenv ≝ lpx ttop. + +interpretation + "top reduction (environment)" + 'RTop L1 L2 = (ltop L1 L2). + +(* Basic properties *********************************************************) + +lemma ltop_refl: reflexive … ltop. +/2 width=1/ qed. + +lemma ltop_sym: symmetric … ltop. +/2 width=1/ qed. + +lemma ltop_trans: transitive … ltop. +/2 width=3/ qed. + +lemma ltop_append: ∀K1,K2. K1 𝟙 K2 → ∀L1,L2. L1 𝟙 L2 → L1 @@ K1 𝟙 L2 @@ K2. +/2 width=1/ qed. + +(* Basic inversion lemmas ***************************************************) + +lemma ltop_inv_atom1: ∀L2. ⋆ 𝟙 L2 → L2 = ⋆. +/2 width=2 by lpx_inv_atom1/ qed-. + +lemma ltop_inv_pair1: ∀K1,I,V1,L2. K1. ⓑ{I} V1 𝟙 L2 → + ∃∃K2,V2. K1 𝟙 K2 & L2 = K2. ⓑ{I} V2. +#K1 #I #V1 #L2 #H +elim (lpx_inv_pair1 … H) -H /2 width=4/ +qed-. + +lemma ltop_inv_atom2: ∀L1. L1 𝟙 ⋆ → L1 = ⋆. +/2 width=2 by lpx_inv_atom2/ qed-. + +lemma ltop_inv_pair2: ∀L1,K2,I,V2. L1 𝟙 K2. ⓑ{I} V2 → + ∃∃K1,V1. K1 𝟙 K2 & L1 = K1. ⓑ{I} V1. +#L1 #K2 #I #V2 #H +elim (lpx_inv_pair2 … H) -H /2 width=4/ +qed-. + +(* Basic forward lemmas *****************************************************) + +lemma ltop_fwd_length: ∀L1,L2. L1 𝟙 L2 → |L1| = |L2|. +/2 width=2 by lpx_fwd_length/ qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/top/lenv_top.ma b/matita/matita/contribs/lambda_delta/basic_2/etc/top/lenv_top.ma deleted file mode 100644 index ab90cebe7..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/etc/top/lenv_top.ma +++ /dev/null @@ -1,68 +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 *) -(* *) -(**************************************************************************) - -notation "hvbox( T1 𝟙 break term 46 T2 )" - non associative with precedence 45 - for @{ 'RTop $T1 $T2 }. - -include "basic_2/grammar/lenv_px.ma". - -(* POINTWISE EXTENSION OF TOP RELATION FOR TERMS ****************************) - -definition ttop: relation term ≝ λT1,T2. True. - -definition ltop: relation lenv ≝ lpx ttop. - -interpretation - "top reduction (environment)" - 'RTop L1 L2 = (ltop L1 L2). - -(* Basic properties *********************************************************) - -lemma ltop_refl: reflexive … ltop. -/2 width=1/ qed. - -lemma ltop_sym: symmetric … ltop. -/2 width=1/ qed. - -lemma ltop_trans: transitive … ltop. -/2 width=3/ qed. - -lemma ltop_append: ∀K1,K2. K1 𝟙 K2 → ∀L1,L2. L1 𝟙 L2 → L1 @@ K1 𝟙 L2 @@ K2. -/2 width=1/ qed. - -(* Basic inversion lemmas ***************************************************) - -lemma ltop_inv_atom1: ∀L2. ⋆ 𝟙 L2 → L2 = ⋆. -/2 width=2 by lpx_inv_atom1/ qed-. - -lemma ltop_inv_pair1: ∀K1,I,V1,L2. K1. ⓑ{I} V1 𝟙 L2 → - ∃∃K2,V2. K1 𝟙 K2 & L2 = K2. ⓑ{I} V2. -#K1 #I #V1 #L2 #H -elim (lpx_inv_pair1 … H) -H /2 width=4/ -qed-. - -lemma ltop_inv_atom2: ∀L1. L1 𝟙 ⋆ → L1 = ⋆. -/2 width=2 by lpx_inv_atom2/ qed-. - -lemma ltop_inv_pair2: ∀L1,K2,I,V2. L1 𝟙 K2. ⓑ{I} V2 → - ∃∃K1,V1. K1 𝟙 K2 & L1 = K1. ⓑ{I} V1. -#L1 #K2 #I #V2 #H -elim (lpx_inv_pair2 … H) -H /2 width=4/ -qed-. - -(* Basic forward lemmas *****************************************************) - -lemma ltop_fwd_length: ∀L1,L2. L1 𝟙 L2 → |L1| = |L2|. -/2 width=2 by lpx_fwd_length/ qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_ltpss.ma index 08da2e373..b728d9dc2 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_ltpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_ltpss.ma @@ -12,16 +12,16 @@ (* *) (**************************************************************************) -include "basic_2/unfold/ltpss_ltpss.ma". +include "basic_2/unfold/ltpss_sn_ltpss_sn.ma". include "basic_2/reducibility/cpr.ma". (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************) (* Properties concerning partial unfold on local environments ***************) -lemma ltpss_cpr_trans: ∀L1,L2,d,e. L1 ▶* [d, e] L2 → - ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡ T2. +lemma ltpss_sn_cpr_trans: ∀L1,L2,d,e. L1 ⊢ ▶* [d, e] L2 → + ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡ T2. #L1 #L2 #d #e #HL12 #T1 #T2 * -lapply (ltpss_weak_all … HL12) -<(ltpss_fwd_length … HL12) -HL12 /3 width=5/ +lapply (ltpss_sn_weak_all … HL12) +<(ltpss_sn_fwd_length … HL12) -HL12 /3 width=5/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr.ma index 46c201147..b4c15e856 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr.ma @@ -34,7 +34,7 @@ lemma fpr_inv_atom1: ∀L2,T1,T2. ⦃⋆, T1⦄ ➡ ⦃L2, T2⦄ → T1 ➡ T2 #L2 #T1 #T2 * #H lapply (length_inv_zero_sn … H) -H #H destruct /2 width=1/ qed-. - +(* lemma fpr_inv_pair1: ∀I,K1,L2,V1,T1,T2. ⦃K1.ⓑ{I}V1, T1⦄ ➡ ⦃L2, T2⦄ → ∃∃K2,V2. ⦃K1, -ⓑ{I}V1.T1⦄ ➡ ⦃K2, -ⓑ{I}V2.T2⦄ & L2 = K2.ⓑ{I}V2. @@ -42,12 +42,12 @@ lemma fpr_inv_pair1: ∀I,K1,L2,V1,T1,T2. ⦃K1.ⓑ{I}V1, T1⦄ ➡ ⦃L2, T2⦄ elim (length_inv_pos_sn … H) -H #I2 #K2 #V2 #HK12 #H destruct #H elim (tpr_fwd_shift_bind_minus … H) // #_ #H0 destruct /3 width=4/ qed-. - +*) lemma fpr_inv_atom3: ∀L1,T1,T2. ⦃L1,T1⦄ ➡ ⦃⋆,T2⦄ → T1 ➡ T2 ∧ L1 = ⋆. #L1 #T1 #T2 * #H lapply (length_inv_zero_dx … H) -H #H destruct /2 width=1/ qed-. - +(* lemma fpr_inv_pair3: ∀I,L1,K2,V2,T1,T2. ⦃L1, T1⦄ ➡ ⦃K2.ⓑ{I}V2, T2⦄ → ∃∃K1,V1. ⦃K1, -ⓑ{I}V1.T1⦄ ➡ ⦃K2, -ⓑ{I}V2.T2⦄ & L1 = K1.ⓑ{I}V1. @@ -55,3 +55,4 @@ lemma fpr_inv_pair3: ∀I,L1,K2,V2,T1,T2. ⦃L1, T1⦄ ➡ ⦃K2.ⓑ{I}V2, T2⦄ elim (length_inv_pos_dx … H) -H #I1 #K1 #V1 #HK12 #H destruct #H elim (tpr_fwd_shift_bind_minus … H) // #_ #H0 destruct /3 width=4/ 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 index 6f0527b33..ed93e5cf9 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr.ma @@ -12,13 +12,13 @@ (* *) (**************************************************************************) -include "basic_2/unfold/ltpss.ma". +include "basic_2/unfold/ltpss_sn.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 + λL1,L2. ∃∃L. L1 ➡ L & L ⊢ ▶* [0, |L|] L2 . interpretation @@ -30,8 +30,11 @@ interpretation lemma lcpr_refl: ∀L. L ⊢ ➡ L. /2 width=3/ qed. +lemma ltpss_sn_lcpr: ∀L1,L2,d,e. L1 ⊢ ▶* [d, e] L2 → L1 ⊢ ➡ L2. +/3 width=5/ 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 // +#L2 * #L #HL >(ltpr_inv_atom1 … HL) -HL #HL2 >(ltpss_sn_inv_atom1 … HL2) -HL2 // qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_aaa.ma index 50c559734..d25abb4b5 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_aaa.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "basic_2/static/aaa_ltpss_sn.ma". include "basic_2/reducibility/ltpr_aaa.ma". include "basic_2/reducibility/cpr.ma". include "basic_2/reducibility/lcpr.ma". diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_cpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_cpr.ma index 69edad2aa..22f3a398c 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_cpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_cpr.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/unfold/ltpss_ltpss.ma". +include "basic_2/unfold/ltpss_sn_ltpss_sn.ma". include "basic_2/reducibility/cpr.ma". include "basic_2/reducibility/lcpr.ma". @@ -23,9 +23,7 @@ include "basic_2/reducibility/lcpr.ma". lemma lcpr_pair: ∀L1,L2. L1 ⊢ ➡ L2 → ∀V1,V2. L2 ⊢ V1 ➡ V2 → ∀I. L1. ⓑ{I} V1 ⊢ ➡ L2. ⓑ{I} V2. #L1 #L2 * #L #HL1 #HL2 #V1 #V2 * -<(ltpss_fwd_length … HL2) /4 width=5/ +<(ltpss_sn_fwd_length … HL2) #V #HV1 #HV2 #I +lapply (ltpss_sn_tpss_trans_eq … HV2 … HL2) -HV2 #V2 +@(ex2_1_intro … (L.ⓑ{I}V)) /2 width=1/ (**) (* explicit constructor *) qed. - -lemma ltpss_lcpr: ∀L1,L2,d,e. L1 ▶* [d, e] L2 → L1 ⊢ ➡ L2. -#L1 #L2 #d #e #H elim H -L1 -L2 -d -e // /3 width=3/ -qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_lcpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_lcpr.ma index 4b1f9b51a..d526b345e 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_lcpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_lcpr.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/reducibility/ltpr_ltpss.ma". +include "basic_2/reducibility/ltpr_ltpss_sn.ma". include "basic_2/reducibility/ltpr_ltpr.ma". include "basic_2/reducibility/lcpr.ma". @@ -26,13 +26,13 @@ theorem lcpr_conf: ∀L0,L1,L2. L0 ⊢ ➡ L1 → L0 ⊢ ➡ L2 → lapply (ltpr_fwd_length … HK01) #H >(ltpr_fwd_length … HK02) in H; #H elim (ltpr_conf … HK01 … HK02) -K0 #K #HK1 #HK2 -lapply (ltpss_fwd_length … HKL1) #H1 -lapply (ltpss_fwd_length … HKL2) #H2 +lapply (ltpss_sn_fwd_length … HKL1) #H1 +lapply (ltpss_sn_fwd_length … HKL2) #H2 >H1 in HKL1 H; -H1 #HKL1 >H2 in HKL2; -H2 #HKL2 #H -elim (ltpr_ltpss_conf … HKL1 … HK1) -K1 #K1 #HK1 #HLK1 -elim (ltpr_ltpss_conf … HKL2 … HK2) -K2 #K2 #HK2 #HLK2 -elim (ltpss_conf … HK1 … HK2) -K #K #HK1 #HK2 +elim (ltpr_ltpss_sn_conf … HKL1 … HK1) -K1 #K1 #HK1 #HLK1 +elim (ltpr_ltpss_sn_conf … HKL2 … HK2) -K2 #K2 #HK2 #HLK2 +elim (ltpss_sn_conf … HK1 … HK2) -K #K #HK1 #HK2 lapply (ltpr_fwd_length … HLK1) #H1 lapply (ltpr_fwd_length … HLK2) #H2 /3 width=5/ diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_alt.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_alt.ma index 46f98452e..bfb483781 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_alt.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_alt.ma @@ -53,7 +53,7 @@ lemma lfpra_fwd_length: ∀L1,L2. ⦃L1⦄ ➡➡ ⦃L2⦄ → |L1| = |L2|. /2 width=2 by lpx_bi_fwd_length/ qed-. (****************************************************************************) - +(* lemma fpr_lfpra: ∀L1,T1,L2,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → ⦃L1⦄ ➡➡ ⦃L2⦄. #L1 #T1 @(cw_wf_ind … L1 T1) -L1 -T1 * [ #T1 #_ #L2 #T2 #H @@ -90,4 +90,5 @@ lemma lcpr_pair2: ∀L1,L2. L1 ⊢ ➡ L2 → ∀V1,V2. ⦃L1, V1⦄ ➡ ⦃L2, <(ltpss_fwd_length … HL2) /4 width=5/ qed. *) +*) *) \ No newline at end of file diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma index df0ecca47..ef63ad095 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/static/aaa_ltpss.ma". +include "basic_2/static/aaa_ltpss_dx.ma". include "basic_2/static/lsuba_aaa.ma". include "basic_2/reducibility/ltpr_ldrop.ma". diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpss.ma deleted file mode 100644 index 34221e4c5..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpss.ma +++ /dev/null @@ -1,36 +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/reducibility/tpr_tpss.ma". - -(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************) - -(* Properties concerning parallel unfold on local environments **************) - -lemma ltpr_ltpss_conf: ∀L1,K1,d,e. L1 ▶* [d, e] K1 → ∀L2. L1 ➡ L2 → - ∃∃K2. L2 ▶* [d, e] K2 & K1 ➡ K2. -#L1 #K1 #d #e #H elim H -L1 -K1 -d -e -[ /2 width=3/ -| #L1 #I #V1 #X #H - elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct /3 width=5/ -| #L1 #K1 #I #V1 #W1 #e #_ #HVW1 #IHLK1 #X #H - elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct - elim (IHLK1 … HL12) -L1 #K2 #HLK2 #HK12 - elim (tpr_tpss_ltpr … HK12 … HV12 … HVW1) -V1 /3 width=5/ -| #L1 #K1 #I #V1 #W1 #d #e #_ #HVW1 #IHLK1 #X #H - elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct - elim (IHLK1 … HL12) -L1 #K2 #HLK2 #HK12 - elim (tpr_tpss_ltpr … HK12 … HV12 … HVW1) -V1 /3 width=5/ -] -qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpss_dx.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpss_dx.ma new file mode 100644 index 000000000..cee1cb49e --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpss_dx.ma @@ -0,0 +1,36 @@ +(**************************************************************************) +(* ___ *) +(* ||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 LOCAL ENVIRONMENTS ********************) + +(* Properties concerning dx parallel unfold on local environments ***********) + +lemma ltpr_ltpss_dx_conf: ∀L1,K1,d,e. L1 ▶* [d, e] K1 → ∀L2. L1 ➡ L2 → + ∃∃K2. L2 ▶* [d, e] K2 & K1 ➡ K2. +#L1 #K1 #d #e #H elim H -L1 -K1 -d -e +[ /2 width=3/ +| #L1 #I #V1 #X #H + elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct /3 width=5/ +| #L1 #K1 #I #V1 #W1 #e #_ #HVW1 #IHLK1 #X #H + elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct + elim (IHLK1 … HL12) -L1 #K2 #HLK2 #HK12 + elim (tpr_tpss_ltpr … HK12 … HV12 … HVW1) -V1 /3 width=5/ +| #L1 #K1 #I #V1 #W1 #d #e #_ #HVW1 #IHLK1 #X #H + elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct + elim (IHLK1 … HL12) -L1 #K2 #HLK2 #HK12 + elim (tpr_tpss_ltpr … HK12 … HV12 … HVW1) -V1 /3 width=5/ +] +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpss_sn.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpss_sn.ma new file mode 100644 index 000000000..823762356 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpss_sn.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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_sn_alt.ma". +include "basic_2/reducibility/ltpr_ltpss_dx.ma". + +(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************) + +(* Properties on sn parallel unfold on local environments *******************) + +(* Note: this can also be proved like ltpr_ltpss_dx_conf *) +lemma ltpr_ltpss_sn_conf: ∀L1,K1,d,e. L1 ⊢ ▶* [d, e] K1 → ∀L2. L1 ➡ L2 → + ∃∃K2. L2 ⊢ ▶* [d, e] K2 & K1 ➡ K2. +#L1 #K1 #d #e #H +lapply (ltpss_sn_ltpssa … H) -H #H +@(ltpssa_ind … H) -K1 /2 width=3/ +#K #K1 #_ #HK1 #IHK #L2 #HL12 +elim (IHK … HL12) -L1 #K2 #HLK2 #HK2 +elim (ltpr_ltpss_dx_conf … HK1 … HK2) -K /3 width=3/ +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 index a74757b2a..16353b450 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma @@ -204,7 +204,7 @@ lemma tpr_inv_lref2: ∀T1,i. T1 ➡ #i → /2 width=3/ qed-. (* Basic forward lemmas *****************************************************) - +(* lemma tpr_fwd_shift1: ∀L1,T1,T. L1 @@ T1 ➡ T → ∃∃L2,T2. L1 𝟙 L2 & T = L2 @@ T2. #L1 @(lenv_ind_dx … L1) -L1 @@ -232,7 +232,7 @@ elim (shift_inj (L2.ⓑ{I2}V2) … HX ?) -HX | lapply (ltop_fwd_length … HL1) -HL1 normalize // ] 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_tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpss.ma index 19f737b09..f3ea69327 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpss.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/unfold/ltpss_ltpss.ma". +include "basic_2/unfold/ltpss_dx_ltpss_dx.ma". include "basic_2/reducibility/ltpr_ldrop.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) @@ -51,7 +51,7 @@ lemma tpr_tps_ltpr: ∀T1,T2. T1 ➡ T2 → elim (IHT1 … HTU1 (L2. ⓑ{I} W2) ?) -T1 /2 width=1/ -HL12 #U #HU1 #HTU elim (tpss_strip_neq … HTU … HT2 ?) -T /2 width=1/ #U2 #HU2 #HTU2 lapply (tps_lsubs_trans … HU2 (L2. ⓑ{I} V2) ?) -HU2 /2 width=1/ #HU2 - elim (ltpss_tps_conf … HU2 (L2. ⓑ{I} W2) (d + 1) e ?) -HU2 /2 width=1/ #U3 #HU3 #HU23 + elim (ltpss_dx_tps_conf … HU2 (L2. ⓑ{I} W2) (d + 1) e ?) -HU2 /2 width=1/ #U3 #HU3 #HU23 lapply (tps_lsubs_trans … HU3 (⋆. ⓑ{I} W2) ?) -HU3 /2 width=1/ #HU3 lapply (tpss_lsubs_trans … HU23 (L2. ⓑ{I} W2) ?) -HU23 /2 width=1/ #HU23 lapply (tpss_trans_eq … HTU2 … HU23) -U2 /3 width=5/