From: Ferruccio Guidi Date: Sat, 13 Oct 2012 21:35:45 +0000 (+0000) Subject: - parallel reduction for local environments: we proved the equivalence X-Git-Tag: make_still_working~1496 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7bedf1797ba168f0742194b2add69575e5d4a5cd;p=helm.git - parallel reduction for local environments: we proved the equivalence between the old context-sensitive version and the focalized version - as a result, the context-sensitive version disappears with its derivatives --- diff --git a/matita/matita/contribs/lambda_delta/Makefile b/matita/matita/contribs/lambda_delta/Makefile index 964277d7f..a1bea3529 100644 --- a/matita/matita/contribs/lambda_delta/Makefile +++ b/matita/matita/contribs/lambda_delta/Makefile @@ -47,17 +47,17 @@ stats: $(PACKAGES:%=%.stats) %.stats: @printf '\x1B[1;40;37m' - @printf '%-15s %-42s' 'Statistics for:' $* + @printf '%-15s %-43s' 'Statistics for:' $* @printf '\x1B[0m\n' @printf '\x1B[1;40;35m' @printf '%-8s %6i' Chars $(CHARS) @printf ' %-8s %5i' Lines `cat $(MAS) | wc -l` @printf ' %-6s %3i' Pages `echo $$(($(CHARS) / 5120))` - @printf ' %-10s' '' + @printf ' %-11s' '' @printf '\x1B[0m\n' @printf '\x1B[1;40;36m' @printf '%-8s %6i' Sources `ls $(MAS) | wc -l` - @printf ' %-40s' '' + @printf ' %-41s' '' # @printf ' %-8s %5i' Objs `ls *.vo | wc -l` # @printf ' %-6s %3i' Files `ls *.v | wc -l` @printf '\x1B[0m\n' @@ -65,18 +65,18 @@ stats: $(PACKAGES:%=%.stats) @printf '%-8s %6i' Theorems `grep "theorem " $(MAS) | wc -l` @printf ' %-8s %5i' Lemmas `grep "lemma " $(MAS) | wc -l` @printf ' %-6s %3i' Facts `grep "fact " $(MAS) | wc -l` - @printf ' %-6s %3i' Proofs `grep qed $(MAS) | wc -l` + @printf ' %-6s %4i' Proofs `grep qed $(MAS) | wc -l` @printf '\x1B[0m\n' @printf '\x1B[1;40;33m' @printf '%-8s %6i' Defs `grep "definition\|let rec\|inductive\|record" $(MAS) | wc -l` - @printf ' %-40s' '' + @printf ' %-41s' '' # @printf ' %-8s %5i' Local `grep "Local" *.v | wc -l` @printf '\x1B[0m\n' @printf '\x1B[1;40;31m' @printf '%-8s %6i' Axioms `grep axiom $(MAS) | wc -l` @printf ' %-8s %5i' Comments `grep "(\*[^*:]*$$" $(MAS) | wc -l` @printf ' %-6s %3i' Marks `grep "(\*\*)" $(MAS) | wc -l` - @printf ' %-10s' '' + @printf ' %-11s' '' @printf '\x1B[0m\n' # summary #################################################################### diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_aaa.ma new file mode 100644 index 000000000..e04e3c784 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_aaa.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cpr_aaa.ma". +include "basic_2/computation/cprs.ma". + +(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) + +(* Properties about atomic arity assignment on terms ************************) + +lemma aaa_cprs_conf: ∀L,T1,A. L ⊢ T1 ⁝ A → ∀T2. L ⊢ T1 ➡* T2 → L ⊢ T2 ⁝ A. +#L #T1 #A #HT1 #T2 #HT12 +@(TC_Conf3 … HT1 ? HT12) /2 width=3/ +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_cprs.ma index d350f0977..8f94b0fa7 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_cprs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_cprs.ma @@ -14,8 +14,8 @@ include "basic_2/reducibility/cpr_lift.ma". include "basic_2/reducibility/cpr_cpr.ma". -include "basic_2/reducibility/lcpr_cpr.ma". -include "basic_2/computation/cprs_lcpr.ma". +include "basic_2/reducibility/lfpr_cpr.ma". +include "basic_2/computation/cprs_lfpr.ma". (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) @@ -45,7 +45,7 @@ lemma cpr_abbr1: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV1 ⊢ T1 ➡ T lemma cpr_abbr2: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV2 ⊢ T1 ➡ T2 → ∀a. L ⊢ ⓓ{a}V1. T1 ➡* ⓓ{a}V2. T2. #L #V1 #V2 #HV12 #T1 #T2 #HT12 -lapply (lcpr_cpr_trans (L. ⓓV1) … HT12) /2 width=1/ +lapply (lfpr_cpr_trans (L. ⓓV1) … HT12) /2 width=1/ qed. (* Basic_1: was: pr3_strip *) @@ -117,7 +117,7 @@ lemma cprs_abbr2_dx: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV2 ⊢ T1 #L #V1 #V2 #HV12 #T1 #T2 #HT12 #a @(cprs_ind_dx … HT12) -T1 [ /2 width=1/ | #T1 #T #HT1 #_ #IHT1 - lapply (lcpr_cpr_trans (L. ⓓV1) … HT1) -HT1 /2 width=1/ #HT1 + lapply (lfpr_cpr_trans (L. ⓓV1) … HT1) -HT1 /2 width=1/ #HT1 @(cprs_trans … IHT1) -IHT1 /2 width=1/ ] qed. @@ -142,7 +142,7 @@ lemma cprs_beta_dx: ∀L,V1,V2,W,T1,T2. qed. (* Basic_1: was only: pr3_pr2_pr3_t pr3_wcpr0_t *) -lemma lcpr_cprs_trans: ∀L1,L2. L1 ⊢ ➡ L2 → +lemma lcpr_cprs_trans: ∀L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2. #L1 #L2 #HL12 #T1 #T2 #H @(cprs_ind … H) -T2 // #T #T2 #_ #HT2 #IHT2 diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcpr.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcpr.ma deleted file mode 100644 index 86f2a13ea..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcpr.ma +++ /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_ltpss.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/computation/cprs_lcprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcprs.ma deleted file mode 100644 index 9131ba4c2..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcprs.ma +++ /dev/null @@ -1,56 +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/computation/cprs_cprs.ma". -include "basic_2/computation/lcprs_lcprs.ma". - -(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) - -(* Properties exploiting context-senstive computation on local environments *) - -(* Basic_1: was just: pr3_pr3_pr3_t *) -lemma lcprs_cprs_trans: ∀L1,L2. L1 ⊢ ➡* L2 → - ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2. -#L1 #L2 #HL12 @(lcprs_ind … HL12) -L2 // /3 width=3/ -qed. - -lemma lcprs_cpr_trans: ∀L1,L2. L1 ⊢ ➡* L2 → - ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡* T2. -/3 width=3 by lcprs_cprs_trans, inj/ qed. - -(* Advanced inversion lemmas ************************************************) - -(* Basic_1: was pr3_gen_abbr *) -lemma cprs_inv_abbr1: ∀a,L,V1,T1,U2. L ⊢ ⓓ{a}V1. T1 ➡* U2 → - (∃∃V2,T2. L ⊢ V1 ➡* V2 & L. ⓓV1 ⊢ T1 ➡* T2 & - U2 = ⓓ{a}V2. T2 - ) ∨ - ∃∃T2. L. ⓓV1 ⊢ T1 ➡* T2 & ⇧[0, 1] U2 ≡ T2 & a = true. -#a #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/ -#U0 #U2 #_ #HU02 * * -[ #V0 #T0 #HV10 #HT10 #H destruct - elim (cpr_inv_abbr1 … HU02) -HU02 * - [ #V #V2 #T2 #HV0 #HV2 #HT02 #H destruct - lapply (cpr_intro … HV0 … HV2) -HV2 #HV02 - lapply (ltpr_cpr_trans (L.ⓓV0) … HT02) /2 width=1/ -V #HT02 - lapply (lcprs_cprs_trans (L. ⓓV1) … HT02) -HT02 /2 width=1/ /4 width=5/ - | #T2 #HT02 #HUT2 - lapply (lcprs_cpr_trans (L.ⓓV1) … HT02) -HT02 /2 width=1/ -V0 #HT02 - lapply (cprs_trans … HT10 … HT02) -T0 /3 width=3/ - ] -| #U1 #HTU1 #HU01 - elim (lift_total U2 0 1) #U #HU2 - lapply (cpr_lift (L.ⓓV1) … HU01 … HU2 HU02) -U0 /2 width=1/ /4 width=3/ -] -qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lfpr.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lfpr.ma new file mode 100644 index 000000000..a06643577 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lfpr.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/ltpr_tps.ma". +include "basic_2/reducibility/cpr_ltpss.ma". +include "basic_2/reducibility/lfpr.ma". +include "basic_2/computation/cprs.ma". + +(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) + +(* Properties concerning focalized parallel reduction on local environments *) + +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 lfpr_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/computation/cprs_lfprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lfprs.ma new file mode 100644 index 000000000..33620d01c --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lfprs.ma @@ -0,0 +1,56 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/computation/cprs_cprs.ma". +include "basic_2/computation/lfprs_lfprs.ma". + +(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) + +(* Properties on focalized computation for local environments ***************) + +(* Basic_1: was just: pr3_pr3_pr3_t *) +lemma lfprs_cprs_trans: ∀L1,L2. ⦃L1⦄ ➡* ⦃L2⦄ → + ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2. +#L1 #L2 #HL12 @(lfprs_ind … HL12) -L2 // /3 width=3/ +qed. + +lemma lfprs_cpr_trans: ∀L1,L2. ⦃L1⦄ ➡* ⦃L2⦄ → + ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡* T2. +/3 width=3 by lfprs_cprs_trans, inj/ qed. + +(* Advanced inversion lemmas ************************************************) + +(* Basic_1: was pr3_gen_abbr *) +lemma cprs_inv_abbr1: ∀a,L,V1,T1,U2. L ⊢ ⓓ{a}V1. T1 ➡* U2 → + (∃∃V2,T2. L ⊢ V1 ➡* V2 & L. ⓓV1 ⊢ T1 ➡* T2 & + U2 = ⓓ{a}V2. T2 + ) ∨ + ∃∃T2. L. ⓓV1 ⊢ T1 ➡* T2 & ⇧[0, 1] U2 ≡ T2 & a = true. +#a #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/ +#U0 #U2 #_ #HU02 * * +[ #V0 #T0 #HV10 #HT10 #H destruct + elim (cpr_inv_abbr1 … HU02) -HU02 * + [ #V #V2 #T2 #HV0 #HV2 #HT02 #H destruct + lapply (cpr_intro … HV0 … HV2) -HV2 #HV02 + lapply (ltpr_cpr_trans (L.ⓓV0) … HT02) /2 width=1/ -V #HT02 + lapply (lfprs_cprs_trans (L. ⓓV1) … HT02) -HT02 /2 width=1/ /4 width=5/ + | #T2 #HT02 #HUT2 + lapply (lfprs_cpr_trans (L.ⓓV1) … HT02) -HT02 /2 width=1/ -V0 #HT02 + lapply (cprs_trans … HT10 … HT02) -T0 /3 width=3/ + ] +| #U1 #HTU1 #HU01 + elim (lift_total U2 0 1) #U #HU2 + lapply (cpr_lift (L.ⓓV1) … HU01 … HU2 HU02) -U0 /2 width=1/ /4 width=3/ +] +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma index ab8329cbc..f7afb8df7 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma @@ -14,7 +14,7 @@ include "basic_2/grammar/tstc.ma". include "basic_2/computation/cprs_lift.ma". -include "basic_2/computation/cprs_lcprs.ma". +include "basic_2/computation/cprs_lfprs.ma". (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma deleted file mode 100644 index 58807c524..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma +++ /dev/null @@ -1,147 +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/grammar/tstc_tstc.ma". -include "basic_2/computation/cprs_cprs.ma". -include "basic_2/computation/csn_lift.ma". -include "basic_2/computation/csn_cpr.ma". -include "basic_2/computation/csn_alt.ma". - -(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) - -(* Advanced properties ******************************************************) - -lemma csn_lcpr_conf: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T. L1 ⊢ ⬊* T → L2 ⊢ ⬊* T. -#L1 #L2 #HL12 #T #H @(csn_ind_alt … H) -T #T #_ #IHT -@csn_intro #T0 #HLT0 #HT0 -@IHT /2 width=2/ -IHT -HT0 /2 width=3/ -qed. - -lemma csn_abbr: ∀a,L,V. L ⊢ ⬊* V → ∀T. L. ⓓV ⊢ ⬊* T → L ⊢ ⬊* ⓓ{a}V. T. -#a #L #V #HV elim HV -V #V #_ #IHV #T #HT @(csn_ind_alt … HT) -T #T #HT #IHT -@csn_intro #X #H1 #H2 -elim (cpr_inv_abbr1 … H1) -H1 * -[ #V0 #V1 #T1 #HLV0 #HLV01 #HLT1 #H destruct - lapply (cpr_intro … HLV0 HLV01) -HLV01 #HLV1 - lapply (ltpr_cpr_trans (L. ⓓV) … HLT1) /2 width=1/ -V0 #HLT1 - elim (eq_false_inv_tpair_sn … H2) -H2 - [ #HV1 @IHV // /2 width=1/ -HV1 - @(csn_lcpr_conf (L. ⓓV)) /2 width=1/ -HLV1 /2 width=3/ - | -IHV -HLV1 * #H destruct /3 width=1/ - ] -| -IHV -IHT -H2 #T0 #HLT0 #HT0 - lapply (csn_cpr_trans … HT … HLT0) -T #HLT0 - lapply (csn_inv_lift … HLT0 … HT0) -T0 /2 width=3/ -] -qed. - -fact csn_appl_beta_aux: ∀a,L,W. L ⊢ ⬊* W → ∀U. L ⊢ ⬊* U → - ∀V,T. U = ⓓ{a}V. T → L ⊢ ⬊* ⓐV. ⓛ{a}W. T. -#a #L #W #H elim H -W #W #_ #IHW #X #H @(csn_ind_alt … H) -X #X #HVT #IHVT #V #T #H destruct -lapply (csn_fwd_pair_sn … HVT) #HV -lapply (csn_fwd_bind_dx … HVT) #HT -HVT -@csn_intro #X #H #H2 -elim (cpr_inv_appl1 … H) -H * -[ #V0 #Y #HLV0 #H #H0 destruct - elim (cpr_inv_abst1 … H Abbr V) -H #W0 #T0 #HLW0 #HLT0 #H destruct - elim (eq_false_inv_beta … H2) -H2 - [ -IHVT #HW0 @IHW -IHW [1,5: // |3: skip ] -HLW0 /2 width=1/ -HW0 - @csn_abbr /2 width=3/ -HV - @(csn_lcpr_conf (L. ⓓV)) /2 width=1/ -V0 /2 width=3/ - | -IHW -HLW0 -HV -HT * #H #HVT0 destruct - @(IHVT … HVT0) -IHVT -HVT0 // /2 width=1/ - ] -| -IHW -IHVT -H2 #b #V0 #W0 #T0 #T1 #HLV0 #HLT01 #H1 #H2 destruct - lapply (lcpr_cpr_trans (L. ⓓV) … HLT01) -HLT01 /2 width=1/ #HLT01 - @csn_abbr /2 width=3/ -HV - @(csn_lcpr_conf (L. ⓓV)) /2 width=1/ -V0 /2 width=3/ -| -IHW -IHVT -HV -HT -H2 #b #V0 #V1 #W0 #W1 #T0 #T1 #_ #_ #_ #_ #H destruct -] -qed. - -(* Basic_1: was: sn3_beta *) -lemma csn_appl_beta: ∀a,L,W. L ⊢ ⬊* W → ∀V,T. L ⊢ ⬊* ⓓ{a}V. T → - L ⊢ ⬊* ⓐV. ⓛ{a}W. T. -/2 width=3/ qed. - -fact csn_appl_theta_aux: ∀a,L,U. L ⊢ ⬊* U → ∀V1,V2. ⇧[0, 1] V1 ≡ V2 → - ∀V,T. U = ⓓ{a}V. ⓐV2. T → L ⊢ ⬊* ⓐV1. ⓓ{a}V. T. -#a #L #X #H @(csn_ind_alt … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct -lapply (csn_fwd_pair_sn … HVT) #HV -lapply (csn_fwd_bind_dx … HVT) -HVT #HVT -@csn_intro #X #HL #H -elim (cpr_inv_appl1 … HL) -HL * -[ -HV #V0 #Y #HLV10 #HL #H0 destruct - elim (cpr_inv_abbr1 … HL) -HL * - [ #V3 #V4 #T3 #HV3 #HLV34 #HLT3 #H0 destruct - lapply (cpr_intro … HV3 HLV34) -HLV34 #HLV34 - elim (lift_total V0 0 1) #V5 #HV05 - elim (term_eq_dec (ⓓ{a}V.ⓐV2.T) (ⓓ{a}V4.ⓐV5.T3)) - [ -IHVT #H0 destruct - elim (eq_false_inv_tpair_sn … H) -H - [ -HLV10 -HLV34 -HV3 -HLT3 -HVT - >(lift_inj … HV12 … HV05) -V5 - #H elim (H ?) // - | * #_ #H elim (H ?) // - ] - | -H -HVT #H - lapply (cpr_lift (L. ⓓV) … HV12 … HV05 HLV10) -HLV10 -HV12 /2 width=1/ #HV25 - lapply (ltpr_cpr_trans (L. ⓓV) … HLT3) /2 width=1/ -HLT3 #HLT3 - @(IHVT … H … HV05) -IHVT // -H -HV05 /3 width=1/ - ] - | -H -IHVT #T0 #HLT0 #HT0 #H0 destruct - lapply (csn_cpr_trans … HVT (ⓐV2.T0) ?) /2 width=1/ -T #HVT0 - lapply (csn_inv_lift L … 1 HVT0 ? ? ?) -HVT0 [ /2 width=4/ |2,3: skip | /2 width=1/ ] -V2 -T0 #HVY - @(csn_cpr_trans … HVY) /2 width=1/ - ] -| -HV -HV12 -HVT -IHVT -H #b #V0 #W0 #T0 #T1 #_ #_ #H destruct -| -IHVT -H #b #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HLW01 #HLT01 #HV03 #H1 #H2 destruct - lapply (cpr_lift (L. ⓓW0) … HV12 … HV03 HLV10) -HLV10 -HV12 -HV03 /2 width=1/ #HLV23 - lapply (lcpr_cpr_trans (L. ⓓW0) … HLT01) -HLT01 /2 width=1/ #HLT01 - @csn_abbr /2 width=3/ -HV - @(csn_lcpr_conf (L. ⓓW0)) /2 width=1/ -W1 - @(csn_cprs_trans … HVT) -HVT /2 width=1/ -] -qed. - -lemma csn_appl_theta: ∀a,V1,V2. ⇧[0, 1] V1 ≡ V2 → - ∀L,V,T. L ⊢ ⬊* ⓓ{a}V. ⓐV2. T → L ⊢ ⬊* ⓐV1. ⓓ{a}V. T. -/2 width=5/ qed. - -(* Basic_1: was only: sn3_appl_appl *) -lemma csn_appl_simple_tstc: ∀L,V. L ⊢ ⬊* V → ∀T1. - L ⊢ ⬊* T1 → - (∀T2. L ⊢ T1 ➡* T2 → (T1 ≃ T2 → ⊥) → L ⊢ ⬊* ⓐV. T2) → - 𝐒⦃T1⦄ → L ⊢ ⬊* ⓐV. T1. -#L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #H @(csn_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1 -@csn_intro #X #HL #H -elim (cpr_inv_appl1_simple … HL ?) -HL // -#V0 #T0 #HLV0 #HLT10 #H0 destruct -elim (eq_false_inv_tpair_sn … H) -H -[ -IHT1 #HV0 - @(csn_cpr_trans … (ⓐV0.T1)) /2 width=1/ -HLT10 - @IHV -IHV // -H1T1 -H3T1 /2 width=1/ -HV0 - #T2 #HLT12 #HT12 - @(csn_cpr_trans … (ⓐV.T2)) /2 width=1/ -HLV0 - @H2T1 -H2T1 // -HLT12 /2 width=1/ -| -IHV -H1T1 -HLV0 * #H #H1T10 destruct - elim (tstc_dec T1 T0) #H2T10 - [ @IHT1 -IHT1 // /2 width=1/ -H1T10 /2 width=3/ -H3T1 - #T2 #HLT02 #HT02 - @H2T1 -H2T1 /2 width=3/ -HLT10 -HLT02 /3 width=3/ - | -IHT1 -H3T1 -H1T10 - @H2T1 -H2T1 /2 width=1/ - ] -] -qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lfpr.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lfpr.ma new file mode 100644 index 000000000..444dcf8f3 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lfpr.ma @@ -0,0 +1,147 @@ +(**************************************************************************) +(* ___ *) +(* ||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/tstc_tstc.ma". +include "basic_2/computation/cprs_cprs.ma". +include "basic_2/computation/csn_lift.ma". +include "basic_2/computation/csn_cpr.ma". +include "basic_2/computation/csn_alt.ma". + +(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) + +(* Advanced properties ******************************************************) + +lemma csn_lfpr_conf: ∀L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀T. L1 ⊢ ⬊* T → L2 ⊢ ⬊* T. +#L1 #L2 #HL12 #T #H @(csn_ind_alt … H) -T #T #_ #IHT +@csn_intro #T0 #HLT0 #HT0 +@IHT /2 width=2/ -IHT -HT0 /2 width=3/ +qed. + +lemma csn_abbr: ∀a,L,V. L ⊢ ⬊* V → ∀T. L. ⓓV ⊢ ⬊* T → L ⊢ ⬊* ⓓ{a}V. T. +#a #L #V #HV elim HV -V #V #_ #IHV #T #HT @(csn_ind_alt … HT) -T #T #HT #IHT +@csn_intro #X #H1 #H2 +elim (cpr_inv_abbr1 … H1) -H1 * +[ #V0 #V1 #T1 #HLV0 #HLV01 #HLT1 #H destruct + lapply (cpr_intro … HLV0 HLV01) -HLV01 #HLV1 + lapply (ltpr_cpr_trans (L. ⓓV) … HLT1) /2 width=1/ -V0 #HLT1 + elim (eq_false_inv_tpair_sn … H2) -H2 + [ #HV1 @IHV // /2 width=1/ -HV1 + @(csn_lfpr_conf (L. ⓓV)) /2 width=1/ -HLV1 /2 width=3/ + | -IHV -HLV1 * #H destruct /3 width=1/ + ] +| -IHV -IHT -H2 #T0 #HLT0 #HT0 + lapply (csn_cpr_trans … HT … HLT0) -T #HLT0 + lapply (csn_inv_lift … HLT0 … HT0) -T0 /2 width=3/ +] +qed. + +fact csn_appl_beta_aux: ∀a,L,W. L ⊢ ⬊* W → ∀U. L ⊢ ⬊* U → + ∀V,T. U = ⓓ{a}V. T → L ⊢ ⬊* ⓐV. ⓛ{a}W. T. +#a #L #W #H elim H -W #W #_ #IHW #X #H @(csn_ind_alt … H) -X #X #HVT #IHVT #V #T #H destruct +lapply (csn_fwd_pair_sn … HVT) #HV +lapply (csn_fwd_bind_dx … HVT) #HT -HVT +@csn_intro #X #H #H2 +elim (cpr_inv_appl1 … H) -H * +[ #V0 #Y #HLV0 #H #H0 destruct + elim (cpr_inv_abst1 … H Abbr V) -H #W0 #T0 #HLW0 #HLT0 #H destruct + elim (eq_false_inv_beta … H2) -H2 + [ -IHVT #HW0 @IHW -IHW [1,5: // |3: skip ] -HLW0 /2 width=1/ -HW0 + @csn_abbr /2 width=3/ -HV + @(csn_lfpr_conf (L. ⓓV)) /2 width=1/ -V0 /2 width=3/ + | -IHW -HLW0 -HV -HT * #H #HVT0 destruct + @(IHVT … HVT0) -IHVT -HVT0 // /2 width=1/ + ] +| -IHW -IHVT -H2 #b #V0 #W0 #T0 #T1 #HLV0 #HLT01 #H1 #H2 destruct + lapply (lfpr_cpr_trans (L. ⓓV) … HLT01) -HLT01 /2 width=1/ #HLT01 + @csn_abbr /2 width=3/ -HV + @(csn_lfpr_conf (L. ⓓV)) /2 width=1/ -V0 /2 width=3/ +| -IHW -IHVT -HV -HT -H2 #b #V0 #V1 #W0 #W1 #T0 #T1 #_ #_ #_ #_ #H destruct +] +qed. + +(* Basic_1: was: sn3_beta *) +lemma csn_appl_beta: ∀a,L,W. L ⊢ ⬊* W → ∀V,T. L ⊢ ⬊* ⓓ{a}V. T → + L ⊢ ⬊* ⓐV. ⓛ{a}W. T. +/2 width=3/ qed. + +fact csn_appl_theta_aux: ∀a,L,U. L ⊢ ⬊* U → ∀V1,V2. ⇧[0, 1] V1 ≡ V2 → + ∀V,T. U = ⓓ{a}V. ⓐV2. T → L ⊢ ⬊* ⓐV1. ⓓ{a}V. T. +#a #L #X #H @(csn_ind_alt … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct +lapply (csn_fwd_pair_sn … HVT) #HV +lapply (csn_fwd_bind_dx … HVT) -HVT #HVT +@csn_intro #X #HL #H +elim (cpr_inv_appl1 … HL) -HL * +[ -HV #V0 #Y #HLV10 #HL #H0 destruct + elim (cpr_inv_abbr1 … HL) -HL * + [ #V3 #V4 #T3 #HV3 #HLV34 #HLT3 #H0 destruct + lapply (cpr_intro … HV3 HLV34) -HLV34 #HLV34 + elim (lift_total V0 0 1) #V5 #HV05 + elim (term_eq_dec (ⓓ{a}V.ⓐV2.T) (ⓓ{a}V4.ⓐV5.T3)) + [ -IHVT #H0 destruct + elim (eq_false_inv_tpair_sn … H) -H + [ -HLV10 -HLV34 -HV3 -HLT3 -HVT + >(lift_inj … HV12 … HV05) -V5 + #H elim (H ?) // + | * #_ #H elim (H ?) // + ] + | -H -HVT #H + lapply (cpr_lift (L. ⓓV) … HV12 … HV05 HLV10) -HLV10 -HV12 /2 width=1/ #HV25 + lapply (ltpr_cpr_trans (L. ⓓV) … HLT3) /2 width=1/ -HLT3 #HLT3 + @(IHVT … H … HV05) -IHVT // -H -HV05 /3 width=1/ + ] + | -H -IHVT #T0 #HLT0 #HT0 #H0 destruct + lapply (csn_cpr_trans … HVT (ⓐV2.T0) ?) /2 width=1/ -T #HVT0 + lapply (csn_inv_lift L … 1 HVT0 ? ? ?) -HVT0 [ /2 width=4/ |2,3: skip | /2 width=1/ ] -V2 -T0 #HVY + @(csn_cpr_trans … HVY) /2 width=1/ + ] +| -HV -HV12 -HVT -IHVT -H #b #V0 #W0 #T0 #T1 #_ #_ #H destruct +| -IHVT -H #b #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HLW01 #HLT01 #HV03 #H1 #H2 destruct + lapply (cpr_lift (L. ⓓW0) … HV12 … HV03 HLV10) -HLV10 -HV12 -HV03 /2 width=1/ #HLV23 + lapply (lfpr_cpr_trans (L. ⓓW0) … HLT01) -HLT01 /2 width=1/ #HLT01 + @csn_abbr /2 width=3/ -HV + @(csn_lfpr_conf (L. ⓓW0)) /2 width=1/ -W1 + @(csn_cprs_trans … HVT) -HVT /2 width=1/ +] +qed. + +lemma csn_appl_theta: ∀a,V1,V2. ⇧[0, 1] V1 ≡ V2 → + ∀L,V,T. L ⊢ ⬊* ⓓ{a}V. ⓐV2. T → L ⊢ ⬊* ⓐV1. ⓓ{a}V. T. +/2 width=5/ qed. + +(* Basic_1: was only: sn3_appl_appl *) +lemma csn_appl_simple_tstc: ∀L,V. L ⊢ ⬊* V → ∀T1. + L ⊢ ⬊* T1 → + (∀T2. L ⊢ T1 ➡* T2 → (T1 ≃ T2 → ⊥) → L ⊢ ⬊* ⓐV. T2) → + 𝐒⦃T1⦄ → L ⊢ ⬊* ⓐV. T1. +#L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #H @(csn_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1 +@csn_intro #X #HL #H +elim (cpr_inv_appl1_simple … HL ?) -HL // +#V0 #T0 #HLV0 #HLT10 #H0 destruct +elim (eq_false_inv_tpair_sn … H) -H +[ -IHT1 #HV0 + @(csn_cpr_trans … (ⓐV0.T1)) /2 width=1/ -HLT10 + @IHV -IHV // -H1T1 -H3T1 /2 width=1/ -HV0 + #T2 #HLT12 #HT12 + @(csn_cpr_trans … (ⓐV.T2)) /2 width=1/ -HLV0 + @H2T1 -H2T1 // -HLT12 /2 width=1/ +| -IHV -H1T1 -HLV0 * #H #H1T10 destruct + elim (tstc_dec T1 T0) #H2T10 + [ @IHT1 -IHT1 // /2 width=1/ -H1T10 /2 width=3/ -H3T1 + #T2 #HLT02 #HT02 + @H2T1 -H2T1 /2 width=3/ -HLT10 -HLT02 /3 width=3/ + | -IHT1 -H3T1 -H1T10 + @H2T1 -H2T1 /2 width=1/ + ] +] +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma index 91e3653f3..cfee668b9 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma @@ -14,7 +14,7 @@ include "basic_2/computation/acp_cr.ma". include "basic_2/computation/cprs_tstc_vector.ma". -include "basic_2/computation/csn_lcpr.ma". +include "basic_2/computation/csn_lfpr.ma". include "basic_2/computation/csn_vector.ma". (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERM VECTORS **********************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs.ma deleted file mode 100644 index 7661358dc..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs.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/reducibility/lcpr.ma". - -(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *************) - -definition lcprs: relation lenv ≝ TC … lcpr. - -interpretation - "context-sensitive parallel computation (environment)" - 'CPRedStar L1 L2 = (lcprs L1 L2). - -(* Basic eliminators ********************************************************) - -lemma lcprs_ind: ∀L1. ∀R:predicate lenv. R L1 → - (∀L,L2. L1 ⊢ ➡* L → L ⊢ ➡ L2 → R L → R L2) → - ∀L2. L1 ⊢ ➡* L2 → R L2. -#L1 #R #HL1 #IHL1 #L2 #HL12 -@(TC_star_ind … HL1 IHL1 … HL12) // -qed-. - -lemma lcprs_ind_dx: ∀L2. ∀R:predicate lenv. R L2 → - (∀L1,L. L1 ⊢ ➡ L → L ⊢ ➡* L2 → R L → R L1) → - ∀L1. L1 ⊢ ➡* L2 → R L1. -#L2 #R #HL2 #IHL2 #L1 #HL12 -@(TC_star_ind_dx … HL2 IHL2 … HL12) // -qed-. - -(* Basic properties *********************************************************) - -lemma lcprs_refl: ∀L. L ⊢ ➡* L. -/2 width=1/ qed. - -lemma lcprs_strap1: ∀L1,L,L2. - L1 ⊢ ➡* L → L ⊢ ➡ L2 → L1 ⊢ ➡* L2. -/2 width=3/ qed. - -lemma lcprs_strap2: ∀L1,L,L2. - L1 ⊢ ➡ L → L ⊢ ➡* L2 → L1 ⊢ ➡* L2. -/2 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs_aaa.ma deleted file mode 100644 index 73a6261e3..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs_aaa.ma +++ /dev/null @@ -1,35 +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/lcpr_aaa.ma". -include "basic_2/computation/cprs.ma". -include "basic_2/computation/lcprs.ma". - -(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *************) - -(* Properties about atomic arity assignment on terms ************************) - -lemma aaa_lcprs_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. L1 ⊢ ➡* L2 → L2 ⊢ T ⁝ A. -#L1 #T #A #HT #L2 #HL12 -@(TC_Conf3 … (λL,A. L ⊢ T ⁝ A) … HT ? HL12) /2 width=3/ -qed. - -lemma aaa_cprs_conf: ∀L,T1,A. L ⊢ T1 ⁝ A → ∀T2. L ⊢ T1 ➡* T2 → L ⊢ T2 ⁝ A. -#L #T1 #A #HT1 #T2 #HT12 -@(TC_Conf3 … HT1 ? HT12) /2 width=3/ -qed. - -lemma aaa_lcprs_cprs_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/computation/lcprs_cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs_cprs.ma deleted file mode 100644 index 2a33e92e7..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs_cprs.ma +++ /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/reducibility/lcpr_cpr.ma". -include "basic_2/computation/cprs.ma". -include "basic_2/computation/lcprs.ma". - -(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *************) - -(* Advanced properties ******************************************************) - -lemma lcprs_pair_dx: ∀I,L1,L2. L1 ⊢ ➡ L2 → ∀V1,V2. L2 ⊢ V1 ➡* V2 → - L1. ⓑ{I} V1 ⊢ ➡* L2. ⓑ{I} V2. -#I #L1 #L2 #HL12 #V1 #V2 #H @(cprs_ind … H) -V2 -/3 width=1/ /3 width=5/ -qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs_lcprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs_lcprs.ma deleted file mode 100644 index 64851e801..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs_lcprs.ma +++ /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/reducibility/lcpr_lcpr.ma". -include "basic_2/computation/lcprs_cprs.ma". - -(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *************) - -(* Advanced properties ******************************************************) - -lemma lcprs_strip: ∀L,L1. L ⊢ ➡* L1 → ∀L2. L ⊢ ➡ L2 → - ∃∃L0. L1 ⊢ ➡ L0 & L2 ⊢ ➡* L0. -/3 width=3/ qed. - -(* Main properties **********************************************************) - -theorem lcprs_conf: ∀L,L1. L ⊢ ➡* L1 → ∀L2. L ⊢ ➡* L2 → - ∃∃L0. L1 ⊢ ➡* L0 & L2 ⊢ ➡* L0. -/3 width=3/ qed. - -theorem lcprs_trans: ∀L1,L. L1 ⊢ ➡* L → ∀L2. L ⊢ ➡* L2 → L1 ⊢ ➡* L2. -/2 width=3/ qed. - -lemma lcprs_pair: ∀L1,L2. L1 ⊢ ➡* L2 → ∀V1,V2. L2 ⊢ V1 ➡* V2 → - ∀I. L1. ⓑ{I} V1 ⊢ ➡* L2. ⓑ{I} V2. -#L1 #L2 #H @(lcprs_ind … H) -L2 /2 width=1/ -#L #L2 #_ #HL2 #IHL1 #V1 #V2 #HV12 #I -@(lcprs_trans … (L.ⓑ{I}V1)) /2 width=1/ -qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lfprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lfprs.ma new file mode 100644 index 000000000..a193f3c0a --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/lfprs.ma @@ -0,0 +1,50 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lfpr.ma". + +(* FOCALIZED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *********************) + +definition lfprs: relation lenv ≝ TC … lfpr. + +interpretation + "focalized parallel computation (environment)" + 'FocalizedPRedStar L1 L2 = (lfprs L1 L2). + +(* Basic eliminators ********************************************************) + +lemma lfprs_ind: ∀L1. ∀R:predicate lenv. R L1 → + (∀L,L2. ⦃L1⦄ ➡* ⦃L⦄ → ⦃L⦄ ➡ ⦃L2⦄ → R L → R L2) → + ∀L2. ⦃L1⦄ ➡* ⦃L2⦄ → R L2. +#L1 #R #HL1 #IHL1 #L2 #HL12 +@(TC_star_ind … HL1 IHL1 … HL12) // +qed-. + +lemma lfprs_ind_dx: ∀L2. ∀R:predicate lenv. R L2 → + (∀L1,L. ⦃L1⦄ ➡ ⦃L⦄ → ⦃L⦄ ➡* ⦃L2⦄ → R L → R L1) → + ∀L1. ⦃L1⦄ ➡* ⦃L2⦄ → R L1. +#L2 #R #HL2 #IHL2 #L1 #HL12 +@(TC_star_ind_dx … HL2 IHL2 … HL12) // +qed-. + +(* Basic properties *********************************************************) + +lemma lfprs_refl: ∀L. ⦃L⦄ ➡* ⦃L⦄. +/2 width=1/ qed. + +lemma lfprs_strap1: ∀L1,L,L2. ⦃L1⦄ ➡* ⦃L⦄ → ⦃L⦄ ➡ ⦃L2⦄ → ⦃L1⦄ ➡* ⦃L2⦄. +/2 width=3/ qed. + +lemma lfprs_strap2: ∀L1,L,L2. ⦃L1⦄ ➡ ⦃L⦄ → ⦃L⦄ ➡* ⦃L2⦄ → ⦃L1⦄ ➡* ⦃L2⦄. +/2 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lfprs_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lfprs_aaa.ma new file mode 100644 index 000000000..a1337787c --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/lfprs_aaa.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/reducibility/lfpr_aaa.ma". +include "basic_2/computation/lfprs.ma". + +(* FOCALIZED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *********************) + +(* Properties about atomic arity assignment on terms ************************) + +lemma aaa_lfprs_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. ⦃L1⦄ ➡* ⦃L2⦄ → L2 ⊢ T ⁝ A. +#L1 #T #A #HT #L2 #HL12 +@(TC_Conf3 … (λL,A. L ⊢ T ⁝ A) … HT ? HL12) /2 width=3/ +qed. +(* +(* Note: this should be rephrased in terms of fprs *) +lemma aaa_lfprs_cprs_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/computation/lfprs_cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lfprs_cprs.ma new file mode 100644 index 000000000..b0f7c4a94 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/lfprs_cprs.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lfpr_cpr.ma". +include "basic_2/computation/cprs.ma". +include "basic_2/computation/lfprs.ma". + +(* FOCALIZED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *********************) + +(* Advanced properties ******************************************************) + +lemma lfprs_pair_dx: ∀I,L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀V1,V2. L2 ⊢ V1 ➡* V2 → + ⦃L1. ⓑ{I} V1⦄ ➡* ⦃L2. ⓑ{I} V2⦄. +#I #L1 #L2 #HL12 #V1 #V2 #H @(cprs_ind … H) -V2 +/3 width=1/ /3 width=5/ +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lfprs_lfprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lfprs_lfprs.ma new file mode 100644 index 000000000..e3866fd2e --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/lfprs_lfprs.ma @@ -0,0 +1,40 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lfpr_lfpr.ma". +include "basic_2/computation/lfprs_cprs.ma". + +(* FOCALIZED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *********************) + +(* Advanced properties ******************************************************) + +lemma lfprs_strip: ∀L,L1. ⦃L⦄ ➡* ⦃L1⦄ → ∀L2. ⦃L⦄ ➡ ⦃L2⦄ → + ∃∃L0. ⦃L1⦄ ➡ ⦃L0⦄ & ⦃L2⦄ ➡* ⦃L0⦄. +/3 width=3/ qed. + +(* Main properties **********************************************************) + +theorem lfprs_conf: ∀L,L1. ⦃L⦄ ➡* ⦃L1⦄ → ∀L2. ⦃L⦄ ➡* ⦃L2⦄ → + ∃∃L0. ⦃L1⦄ ➡* ⦃L0⦄ & ⦃L2⦄ ➡* ⦃L0⦄. +/3 width=3/ qed. + +theorem lfprs_trans: ∀L1,L. ⦃L1⦄ ➡* ⦃L⦄ → ∀L2. ⦃L⦄ ➡* ⦃L2⦄ → ⦃L1⦄ ➡* ⦃L2⦄. +/2 width=3/ qed. + +lemma lfprs_pair: ∀L1,L2. ⦃L1⦄ ➡* ⦃L2⦄ → ∀V1,V2. L2 ⊢ V1 ➡* V2 → + ∀I. ⦃L1. ⓑ{I} V1⦄ ➡* ⦃L2. ⓑ{I} V2⦄. +#L1 #L2 #H @(lfprs_ind … H) -L2 /2 width=1/ +#L #L2 #_ #HL2 #IHL1 #V1 #V2 #HV12 #I +@(lfprs_trans … (L.ⓑ{I}V1)) /2 width=1/ +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/conversion/lcpc.ma b/matita/matita/contribs/lambda_delta/basic_2/conversion/lcpc.ma deleted file mode 100644 index 6ca577deb..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/conversion/lcpc.ma +++ /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/reducibility/lcpr.ma". - -(* CONTEXT-SENSITIVE PARALLEL CONVERSION ON LOCAL ENVIRONMENTS **************) - -definition lcpc: relation lenv ≝ - λL1,L2. L1 ⊢ ➡ L2 ∨ L2 ⊢ ➡ L1. - -interpretation - "context-sensitive parallel conversion (local environment)" - 'CPConv L1 L2 = (lcpc L1 L2). - -(* Basic properties *********************************************************) - -lemma lcpc_refl: ∀L. L ⊢ ⬌ L. -/2 width=1/ qed. - -lemma lcpc_sym: ∀L1,L2. L1 ⊢ ⬌ L2 → L2 ⊢ ⬌ L1. -#L1 #L2 * /2 width=1/ -qed. - -lemma lcpc_lcpr: ∀L1,L2. L1 ⊢ ⬌ L2 → ∃∃L. L1 ⊢ ➡ L & L2 ⊢ ➡ L. -#L1 #L2 * /2 width=3/ -qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/conversion/lcpc_lcpc.ma b/matita/matita/contribs/lambda_delta/basic_2/conversion/lcpc_lcpc.ma deleted file mode 100644 index d52bcd101..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/conversion/lcpc_lcpc.ma +++ /dev/null @@ -1,23 +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/conversion/lcpc.ma". - -(* CONTEXT-SENSITIVE PARALLEL CONVERSION ON LOCAL ENVIRONMENTS **************) - -(* Main properties **********************************************************) - -theorem lcpc_conf: ∀L0,L1,L2. L0 ⊢ ⬌ L1 → L0 ⊢ ⬌ L2 → - ∃∃L. L1 ⊢ ⬌ L & L2 ⊢ ⬌ L. -/3 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/conversion/lfpc.ma b/matita/matita/contribs/lambda_delta/basic_2/conversion/lfpc.ma new file mode 100644 index 000000000..273873abd --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/conversion/lfpc.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/reducibility/lfpr.ma". + +(* FOCALIZED PARALLEL CONVERSION ON LOCAL ENVIRONMENTS **********************) + +definition lfpc: relation lenv ≝ + λL1,L2. ⦃L1⦄ ➡ ⦃L2⦄ ∨ ⦃L2⦄ ➡ ⦃L1⦄. + +interpretation + "focalized parallel conversion (local environment)" + 'FocalizedPConv L1 L2 = (lfpc L1 L2). + +(* Basic properties *********************************************************) + +lemma lfpc_refl: ∀L. ⦃L⦄ ⬌ ⦃L⦄. +/2 width=1/ qed. + +lemma lfpc_sym: ∀L1,L2. ⦃L1⦄ ⬌ ⦃L2⦄ → ⦃L2⦄ ⬌ ⦃L1⦄. +#L1 #L2 * /2 width=1/ +qed. + +lemma lfpc_lfpr: ∀L1,L2. ⦃L1⦄ ⬌ ⦃L2⦄ → ∃∃L. ⦃L1⦄ ➡ ⦃L⦄ & ⦃L2⦄ ➡ ⦃L⦄. +#L1 #L2 * /2 width=3/ +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/conversion/lfpc_lfpc.ma b/matita/matita/contribs/lambda_delta/basic_2/conversion/lfpc_lfpc.ma new file mode 100644 index 000000000..69e444adb --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/conversion/lfpc_lfpc.ma @@ -0,0 +1,23 @@ +(**************************************************************************) +(* ___ *) +(* ||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/conversion/lfpc.ma". + +(* FOCALIZED PARALLEL CONVERSION ON LOCAL ENVIRONMENTS **********************) + +(* Main properties **********************************************************) + +theorem lfpc_conf: ∀L0,L1,L2. ⦃L0⦄ ⬌ ⦃L1⦄ → ⦃L0⦄ ⬌ ⦃L2⦄ → + ∃∃L. ⦃L1⦄ ⬌ ⦃L⦄ & ⦃L2⦄ ⬌ ⦃L⦄. +/3 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_aaa.ma index f5953fedb..fd6645538 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_aaa.ma @@ -15,7 +15,7 @@ include "basic_2/computation/csn_aaa.ma". include "basic_2/computation/xprs_aaa.ma". include "basic_2/computation/xprs_cprs.ma". -include "basic_2/equivalence/lcpcs_aaa.ma". +include "basic_2/equivalence/cpcs_aaa.ma". include "basic_2/dynamic/snv.ma". (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_aaa.ma new file mode 100644 index 000000000..363b8acd3 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_aaa.ma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/computation/cprs_aaa.ma". +include "basic_2/equivalence/cpcs_cpcs.ma". + +(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************) + +(* Main properties about atomic arity assignment on terms *******************) + +theorem aaa_cpcs_mono: ∀L,T1,T2. L ⊢ T1 ⬌* T2 → + ∀A1. L ⊢ T1 ⁝ A1 → ∀A2. L ⊢ T2 ⁝ A2 → + A1 = A2. +#L #T1 #T2 #HT12 #A1 #HA1 #A2 #HA2 +elim (cpcs_inv_cprs … HT12) -HT12 #T #HT1 #HT2 +lapply (aaa_cprs_conf … HA1 … HT1) -T1 #HA1 +lapply (aaa_cprs_conf … HA2 … HT2) -T2 #HA2 +lapply (aaa_mono … HA1 … HA2) -L -T // +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs.ma deleted file mode 100644 index d30e504ba..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs.ma +++ /dev/null @@ -1,70 +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/conversion/lcpc.ma". - -(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON LOCAL EBVIRONMENTS *************) - -definition lcpcs: relation lenv ≝ TC … lcpc. - -interpretation "context-sensitive parallel equivalence (local environment)" - 'CPConvStar L1 L2 = (lcpcs L1 L2). - -(* Basic eliminators ********************************************************) - -lemma lcpcs_ind: ∀L1. ∀R:predicate lenv. R L1 → - (∀L,L2. L1 ⊢ ⬌* L → L ⊢ ⬌ L2 → R L → R L2) → - ∀L2. L1 ⊢ ⬌* L2 → R L2. -#L1 #R #HL1 #IHL1 #L2 #HL12 @(TC_star_ind … HL1 IHL1 … HL12) // -qed-. - -lemma lcpcs_ind_dx: ∀L2. ∀R:predicate lenv. R L2 → - (∀L1,L. L1 ⊢ ⬌ L → L ⊢ ⬌* L2 → R L → R L1) → - ∀L1. L1 ⊢ ⬌* L2 → R L1. -#L2 #R #HL2 #IHL2 #L1 #HL12 -@(TC_star_ind_dx … HL2 IHL2 … HL12) // -qed-. - -(* Basic properties *********************************************************) - -lemma lcpcs_refl: ∀L. L ⊢ ⬌* L. -/2 width=1/ qed. - -lemma lcpcs_strap1: ∀L1,L,L2. L1 ⊢ ⬌* L → L ⊢ ⬌ L2 → L1 ⊢ ⬌* L2. -/2 width=3/ qed. - -lemma lcpcs_strap2: ∀L1,L,L2. L1 ⊢ ⬌ L → L ⊢ ⬌* L2 → L1 ⊢ ⬌* L2. -/2 width=3/ qed. - -lemma lcpcs_lcpr_dx: ∀L1,L2. L1 ⊢ ➡ L2 → L1 ⊢ ⬌* L2. -/3 width=1/ qed. - -lemma lcpcs_lcpr_sn: ∀L1,L2. L2 ⊢ ➡ L1 → L1 ⊢ ⬌* L2. -/3 width=1/ qed. - -lemma lcpcs_lcpr_strap1: ∀L1,L. L1 ⊢ ⬌* L → ∀L2. L ⊢ ➡ L2 → L1 ⊢ ⬌* L2. -/3 width=3/ qed. - -lemma lcpcs_lcpr_strap2: ∀L1,L. L1 ⊢ ➡ L → ∀L2. L ⊢ ⬌* L2 → L1 ⊢ ⬌* L2. -/3 width=3/ qed. - -lemma lcpcs_lcpr_div: ∀L1,L. L1 ⊢ ⬌* L → ∀L2. L2 ⊢ ➡ L → L1 ⊢ ⬌* L2. -/3 width=3/ qed. - -lemma lcpcs_lcpr_conf: ∀L1,L. L ⊢ ➡ L1 → ∀L2. L ⊢ ⬌* L2 → L1 ⊢ ⬌* L2. -/3 width=3/ qed. - -lemma lcprs_comm: ∀L1,L2. L1 ⊢ ⬌* L2 → L2 ⊢ ⬌* L1. -#L1 #L2 #H @(lcpcs_ind … H) -L2 // /3 width=3/ -qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_aaa.ma deleted file mode 100644 index aa2b8ef2a..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_aaa.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/computation/lcprs_aaa.ma". -include "basic_2/equivalence/cpcs_cpcs.ma". -include "basic_2/equivalence/lcpcs_lcpcs.ma". - -(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON LOCAL EBVIRONMENTS *************) - -(* Main properties about atomic arity assignment on terms *******************) - -theorem aaa_lcpcs_mono: ∀L1,L2. L1 ⊢ ⬌* L2 → - ∀T,A1. L1 ⊢ T ⁝ A1 → ∀A2. L2 ⊢ T ⁝ A2 → - A1 = A2. -#L1 #L2 #HL12 #T #A1 #HT1 #A2 #HT2 -elim (lcpcs_inv_lcprs … HL12) -HL12 #L #HL1 #HL2 -lapply (aaa_lcprs_conf … HT1 … HL1) -L1 #HT1 -lapply (aaa_lcprs_conf … HT2 … HL2) -L2 #HT2 -lapply (aaa_mono … HT1 … HT2) -L -T // -qed-. - -theorem aaa_cpcs_mono: ∀L,T1,T2. L ⊢ T1 ⬌* T2 → - ∀A1. L ⊢ T1 ⁝ A1 → ∀A2. L ⊢ T2 ⁝ A2 → - A1 = A2. -#L #T1 #T2 #HT12 #A1 #HA1 #A2 #HA2 -elim (cpcs_inv_cprs … HT12) -HT12 #T #HT1 #HT2 -lapply (aaa_cprs_conf … HA1 … HT1) -T1 #HA1 -lapply (aaa_cprs_conf … HA2 … HT2) -T2 #HA2 -lapply (aaa_mono … HA1 … HA2) -L -T // -qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_lcpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_lcpcs.ma deleted file mode 100644 index 876161bd2..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_lcpcs.ma +++ /dev/null @@ -1,50 +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/computation/lcprs_lcprs.ma". -include "basic_2/conversion/lcpc_lcpc.ma". -include "basic_2/equivalence/lcpcs_lcprs.ma". - -(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON LOCAL ENVIRONMENTS *************) - -(* Advanced inversion lemmas ************************************************) - -lemma lcpcs_inv_lcprs: ∀L1,L2. L1 ⊢ ⬌* L2 → - ∃∃L. L1 ⊢ ➡* L & L2 ⊢ ➡* L. -#L1 #L2 #H @(lcpcs_ind … H) -L2 -[ /3 width=3/ -| #L #L2 #_ #HL2 * #L0 #HL10 elim HL2 -HL2 #HL2 #HL0 - [ elim (lcprs_strip … HL0 … HL2) -L #L #HL0 #HL2 - lapply (lcprs_strap1 … HL10 … HL0) -L0 /2 width=3/ - | lapply (lcprs_strap2 … HL2 … HL0) -L /2 width=3/ - ] -] -qed-. - -(* Advanced properties ******************************************************) - -lemma lcpcs_strip: ∀L,L1. L ⊢ ⬌* L1 → ∀L2. L ⊢ ⬌ L2 → - ∃∃L0. L1 ⊢ ⬌ L0 & L2 ⊢ ⬌* L0. -/3 width=3/ qed. - -(* Main properties **********************************************************) - -theorem lcpcs_trans: ∀L1,L. L1 ⊢ ⬌* L → ∀L2. L ⊢ ⬌* L2 → L1 ⊢ ⬌* L2. -/2 width=3/ qed. - -theorem lcpcs_canc_sn: ∀L,L1,L2. L ⊢ ⬌* L1 → L ⊢ ⬌* L2 → L1 ⊢ ⬌* L2. -/3 width=3 by lcpcs_trans, lcprs_comm/ qed. - -theorem lcpcs_canc_dx: ∀L,L1,L2. L1 ⊢ ⬌* L → L2 ⊢ ⬌* L → L1 ⊢ ⬌* L2. -/3 width=3 by lcpcs_trans, lcprs_comm/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_lcprs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_lcprs.ma deleted file mode 100644 index 4d2757a2e..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_lcprs.ma +++ /dev/null @@ -1,48 +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/computation/lcprs.ma". -include "basic_2/equivalence/lcpcs.ma". - -(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON LOCAL ENVIRONMENTS *************) - -(* Properties about context sensitive computation on local environments *****) - -lemma lcpcs_lcprs_dx: ∀L1,L2. L1 ⊢ ➡* L2 → L1 ⊢ ⬌* L2. -#L1 #L2 #H @(lcprs_ind … H) -L2 /width=1/ /3 width=3/ -qed. - -lemma lcpcs_lcprs_sn: ∀L1,L2. L2 ⊢ ➡* L1 → L1 ⊢ ⬌* L2. -#L1 #L2 #H @(lcprs_ind_dx … H) -L2 /width=1/ /3 width=3/ -qed. - -lemma lcpcs_lcprs_strap1: ∀L1,L. L1 ⊢ ⬌* L → ∀L2. L ⊢ ➡* L2 → L1 ⊢ ⬌* L2. -#L1 #L #HL1 #L2 #H @(lcprs_ind … H) -L2 /width=1/ /2 width=3/ -qed. - -lemma lcpcs_lcprs_strap2: ∀L1,L. L1 ⊢ ➡* L → ∀L2. L ⊢ ⬌* L2 → L1 ⊢ ⬌* L2. -#L1 #L #H #L2 #HL2 @(lcprs_ind_dx … H) -L1 /width=1/ /2 width=3/ -qed. - -lemma lcpcs_lcprs_div: ∀L1,L. L1 ⊢ ⬌* L → ∀L2. L2 ⊢ ➡* L → L1 ⊢ ⬌* L2. -#L1 #L #HL1 #L2 #H @(lcprs_ind_dx … H) -L2 /width=1/ /2 width=3/ -qed. - -lemma lcpcs_lcprs_conf: ∀L1,L. L ⊢ ➡* L1 → ∀L2. L ⊢ ⬌* L2 → L1 ⊢ ⬌* L2. -#L1 #L #H #L2 #HL2 @(lcprs_ind … H) -L1 /width=1/ /2 width=3/ -qed. - -lemma lcprs_div: ∀L1,L. L1 ⊢ ➡* L → ∀L2. L2 ⊢ ➡* L → L1 ⊢ ⬌* L2. -#L1 #L #HL1 #L2 #H @(lcprs_ind_dx … H) -L2 /2 width=1/ /2 width=3/ -qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs.ma new file mode 100644 index 000000000..c3cbf6c01 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs.ma @@ -0,0 +1,70 @@ +(**************************************************************************) +(* ___ *) +(* ||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/conversion/lfpc.ma". + +(* FOCALIZED PARALLEL EQUIVALENCE ON LOCAL ENVIRONMENTS *********************) + +definition lfpcs: relation lenv ≝ TC … lfpc. + +interpretation "focalized parallel equivalence (local environment)" + 'FocalizedPConvStar L1 L2 = (lfpcs L1 L2). + +(* Basic eliminators ********************************************************) + +lemma lfpcs_ind: ∀L1. ∀R:predicate lenv. R L1 → + (∀L,L2. ⦃L1⦄ ⬌* ⦃L⦄ → ⦃L⦄ ⬌ ⦃L2⦄ → R L → R L2) → + ∀L2. ⦃L1⦄ ⬌* ⦃L2⦄ → R L2. +#L1 #R #HL1 #IHL1 #L2 #HL12 @(TC_star_ind … HL1 IHL1 … HL12) // +qed-. + +lemma lfpcs_ind_dx: ∀L2. ∀R:predicate lenv. R L2 → + (∀L1,L. ⦃L1⦄ ⬌ ⦃L⦄ → ⦃L⦄ ⬌* ⦃L2⦄ → R L → R L1) → + ∀L1. ⦃L1⦄ ⬌* ⦃L2⦄ → R L1. +#L2 #R #HL2 #IHL2 #L1 #HL12 +@(TC_star_ind_dx … HL2 IHL2 … HL12) // +qed-. + +(* Basic properties *********************************************************) + +lemma lfpcs_refl: ∀L. ⦃L⦄ ⬌* ⦃L⦄. +/2 width=1/ qed. + +lemma lfpcs_strap1: ∀L1,L,L2. ⦃L1⦄ ⬌* ⦃L⦄ → ⦃L⦄ ⬌ ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +/2 width=3/ qed. + +lemma lfpcs_strap2: ∀L1,L,L2. ⦃L1⦄ ⬌ ⦃L⦄ → ⦃L⦄ ⬌* ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +/2 width=3/ qed. + +lemma lfpcs_lfpr_dx: ∀L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +/3 width=1/ qed. + +lemma lfpcs_lfpr_sn: ∀L1,L2. ⦃L2⦄ ➡ ⦃L1⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +/3 width=1/ qed. + +lemma lfpcs_lfpr_strap1: ∀L1,L. ⦃L1⦄ ⬌* ⦃L⦄ → ∀L2. ⦃L⦄ ➡ ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +/3 width=3/ qed. + +lemma lfpcs_lfpr_strap2: ∀L1,L. ⦃L1⦄ ➡ ⦃L⦄ → ∀L2. ⦃L⦄ ⬌* ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +/3 width=3/ qed. + +lemma lfpcs_lfpr_div: ∀L1,L. ⦃L1⦄ ⬌* ⦃L⦄ → ∀L2. ⦃L2⦄ ➡ ⦃L⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +/3 width=3/ qed. + +lemma lfpcs_lfpr_conf: ∀L1,L. ⦃L⦄ ➡ ⦃L1⦄ → ∀L2. ⦃L⦄ ⬌* ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +/3 width=3/ qed. + +lemma lfprs_comm: ∀L1,L2. ⦃L1⦄ ⬌* ⦃L2⦄ → ⦃L2⦄ ⬌* ⦃L1⦄. +#L1 #L2 #H @(lfpcs_ind … H) -L2 // /3 width=3/ +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs_aaa.ma new file mode 100644 index 000000000..b7cea0b7a --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs_aaa.ma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/computation/lfprs_aaa.ma". +include "basic_2/equivalence/lfpcs_lfpcs.ma". + +(* FOCALIZED PARALLEL EQUIVALENCE ON LOCAL ENVIRONMENTS *********************) + +(* Main properties about atomic arity assignment on terms *******************) + +theorem aaa_lfpcs_mono: ∀L1,L2. ⦃L1⦄ ⬌* ⦃L2⦄ → + ∀T,A1. L1 ⊢ T ⁝ A1 → ∀A2. L2 ⊢ T ⁝ A2 → + A1 = A2. +#L1 #L2 #HL12 #T #A1 #HT1 #A2 #HT2 +elim (lfpcs_inv_lfprs … HL12) -HL12 #L #HL1 #HL2 +lapply (aaa_lfprs_conf … HT1 … HL1) -L1 #HT1 +lapply (aaa_lfprs_conf … HT2 … HL2) -L2 #HT2 +lapply (aaa_mono … HT1 … HT2) -L -T // +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs_lfpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs_lfpcs.ma new file mode 100644 index 000000000..fcbeb9b8a --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs_lfpcs.ma @@ -0,0 +1,50 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/computation/lfprs_lfprs.ma". +include "basic_2/conversion/lfpc_lfpc.ma". +include "basic_2/equivalence/lfpcs_lfprs.ma". + +(* FOCALIZED PARALLEL EQUIVALENCE ON LOCAL ENVIRONMENTS *********************) + +(* Advanced inversion lemmas ************************************************) + +lemma lfpcs_inv_lfprs: ∀L1,L2. ⦃L1⦄ ⬌* ⦃L2⦄ → + ∃∃L. ⦃L1⦄ ➡* ⦃L⦄ & ⦃L2⦄ ➡* ⦃L⦄. +#L1 #L2 #H @(lfpcs_ind … H) -L2 +[ /3 width=3/ +| #L #L2 #_ #HL2 * #L0 #HL10 elim HL2 -HL2 #HL2 #HL0 + [ elim (lfprs_strip … HL0 … HL2) -L #L #HL0 #HL2 + lapply (lfprs_strap1 … HL10 … HL0) -L0 /2 width=3/ + | lapply (lfprs_strap2 … HL2 … HL0) -L /2 width=3/ + ] +] +qed-. + +(* Advanced properties ******************************************************) + +lemma lfpcs_strip: ∀L,L1. ⦃L⦄ ⬌* ⦃L1⦄ → ∀L2. ⦃L⦄ ⬌ ⦃L2⦄ → + ∃∃L0. ⦃L1⦄ ⬌ ⦃L0⦄ & ⦃L2⦄ ⬌* ⦃L0⦄. +/3 width=3/ qed. + +(* Main properties **********************************************************) + +theorem lfpcs_trans: ∀L1,L. ⦃L1⦄ ⬌* ⦃L⦄ → ∀L2. ⦃L⦄ ⬌* ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +/2 width=3/ qed. + +theorem lfpcs_canc_sn: ∀L,L1,L2. ⦃L⦄ ⬌* ⦃L1⦄ → ⦃L⦄ ⬌* ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +/3 width=3 by lfpcs_trans, lfprs_comm/ qed. + +theorem lfpcs_canc_dx: ∀L,L1,L2. ⦃L1⦄ ⬌* ⦃L⦄ → ⦃L2⦄ ⬌* ⦃L⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +/3 width=3 by lfpcs_trans, lfprs_comm/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs_lfprs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs_lfprs.ma new file mode 100644 index 000000000..baf2caf27 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs_lfprs.ma @@ -0,0 +1,48 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/computation/lfprs.ma". +include "basic_2/equivalence/lfpcs.ma". + +(* FOCALIZED PARALLEL EQUIVALENCE ON LOCAL ENVIRONMENTS *********************) + +(* Properties on focalized computation for local environments ***************) + +lemma lfpcs_lfprs_dx: ∀L1,L2. ⦃L1⦄ ➡* ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +#L1 #L2 #H @(lfprs_ind … H) -L2 /width=1/ /3 width=3/ +qed. + +lemma lfpcs_lfprs_sn: ∀L1,L2. ⦃L2⦄ ➡* ⦃L1⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +#L1 #L2 #H @(lfprs_ind_dx … H) -L2 /width=1/ /3 width=3/ +qed. + +lemma lfpcs_lfprs_strap1: ∀L1,L. ⦃L1⦄ ⬌* ⦃L⦄ → ∀L2. ⦃L⦄ ➡* ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +#L1 #L #HL1 #L2 #H @(lfprs_ind … H) -L2 /width=1/ /2 width=3/ +qed. + +lemma lfpcs_lfprs_strap2: ∀L1,L. ⦃L1⦄ ➡* ⦃L⦄ → ∀L2. ⦃L⦄ ⬌* ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +#L1 #L #H #L2 #HL2 @(lfprs_ind_dx … H) -L1 /width=1/ /2 width=3/ +qed. + +lemma lfpcs_lfprs_div: ∀L1,L. ⦃L1⦄ ⬌* ⦃L⦄ → ∀L2. ⦃L2⦄ ➡* ⦃L⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +#L1 #L #HL1 #L2 #H @(lfprs_ind_dx … H) -L2 /width=1/ /2 width=3/ +qed. + +lemma lfpcs_lfprs_conf: ∀L1,L. ⦃L⦄ ➡* ⦃L1⦄ → ∀L2. ⦃L⦄ ⬌* ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +#L1 #L #H #L2 #HL2 @(lfprs_ind … H) -L1 /width=1/ /2 width=3/ +qed. + +lemma lfprs_div: ∀L1,L. ⦃L1⦄ ➡* ⦃L⦄ → ∀L2. ⦃L2⦄ ➡* ⦃L⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +#L1 #L #HL1 #L2 #H @(lfprs_ind_dx … H) -L2 /2 width=1/ /2 width=3/ +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_shift.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_shift.ma index 837b1c670..bbdc8e7d0 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_shift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_shift.ma @@ -26,7 +26,7 @@ interpretation "shift (closure)" 'Append L T = (shift L T). (* Basic properties *********************************************************) lemma shift_append_assoc: ∀L,K. ∀T:term. (L @@ K) @@ T = L @@ K @@ T. -#L #K elim K -K normalize // +#L #K elim K -K // normalize // qed. (* Basic inversion lemmas ***************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_append.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_append.ma index 2f6932188..f58f96076 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_append.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_append.ma @@ -47,7 +47,8 @@ lemma append_inj_sn: ∀K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 → |K1| = |K2| → | #K1 #I1 #V1 #IH * normalize [ #L1 #L2 #_ append_length in H2; #H elim (plus_xySz_x_false … (sym_eq … H)) | #K2 #I2 #V2 #L1 #L2 #H1 #H2 destruct (**) (* destruct does not simplify well *) - elim (IH … e0 ?) -IH -H1 /2 width=1/ -H2 #H1 #H2 destruct /2 width=1/ + -H1 (**) (* destruct: the destucted equality is not erased *) + elim (IH … e0 ?) -IH // -H2 #H1 #H2 destruct /2 width=1/ ] ] qed-. @@ -100,3 +102,19 @@ lemma lenv_ind_dx: ∀R:predicate lenv. R ⋆ → (∀I,L,V. R L → R (⋆.ⓑ{I}V @@ L)) → ∀L. R L. /3 width=2 by lenv_ind_dx_aux/ qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma length_inv_pos_sn_append: ∀d,L. 1 + d = |L| → + ∃∃I,K,V. d = |K| & L = ⋆. ⓑ{I}V @@ K. +#d >commutative_plus @(nat_ind_plus … d) -d +[ #L #H elim (length_inv_pos_sn … H) -H #I #K #V #H1 #H2 destruct + >(length_inv_zero_sn … H1) -K + @(ex2_3_intro … (⋆)) // (**) (* explicit constructor *) +| #d #IHd #L #H elim (length_inv_pos_sn … H) -H #I #K #V #H1 #H2 destruct + >H1 in IHd; -H1 #IHd + elim (IHd K ?) -IHd // #J #L #W #H1 #H2 destruct + @(ex2_3_intro … (L.ⓑ{I}V)) // (**) (* explicit constructor *) + >append_length /2 width=1/ +] +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px.ma index c3d05949f..41710626a 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px.ma @@ -74,6 +74,32 @@ lemma lpx_fwd_length: ∀R,L1,L2. lpx R L1 L2 → |L1| = |L2|. #R #L1 #L2 #H elim H -L1 -L2 normalize // qed-. +(* Advanced inversion lemmas ************************************************) + +lemma lpx_inv_append1: ∀R,L1,K1,L. lpx R (K1 @@ L1) L → + ∃∃K2,L2. lpx R K1 K2 & lpx R L1 L2 & L = K2 @@ L2. +#R #L1 elim L1 -L1 normalize +[ #K1 #K2 #HK12 + @(ex3_2_intro … K2 (⋆)) // (**) (* explicit constructor, /2 width=5/ does not work *) +| #L1 #I #V1 #IH #K1 #X #H + elim (lpx_inv_pair1 … H) -H #L #V2 #H1 #HV12 #H destruct + elim (IH … H1) -IH -H1 #K2 #L2 #HK12 #HL12 #H destruct + @(ex3_2_intro … HK12) [2: /2 width=2/ | skip | // ] (* explicit constructor, /3 width=5/ does not work *) +] +qed-. + +lemma lpx_inv_append2: ∀R,L2,K2,L. lpx R L (K2 @@ L2) → + ∃∃K1,L1. lpx R K1 K2 & lpx R L1 L2 & L = K1 @@ L1. +#R #L2 elim L2 -L2 normalize +[ #K2 #K1 #HK12 + @(ex3_2_intro … K1 (⋆)) // (**) (* explicit constructor, /2 width=5/ does not work *) +| #L2 #I #V2 #IH #K2 #X #H + elim (lpx_inv_pair2 … H) -H #L #V1 #H1 #HV12 #H destruct + elim (IH … H1) -IH -H1 #K1 #L1 #HK12 #HL12 #H destruct + @(ex3_2_intro … HK12) [2: /2 width=2/ | skip | // ] (* explicit constructor, /3 width=5/ does not work *) +] +qed-. + (* Basic properties *********************************************************) lemma lpx_refl: ∀R. reflexive ? R → reflexive … (lpx R). @@ -125,7 +151,7 @@ lemma TC_lpx_pair_sn: ∀R. reflexive ? R → /4 width=5 by lpx_refl, lpx_pair, inj, step/ (**) (* too slow without trace *) qed. -lemma lpx_TC: ∀R,L1,L2. TC … (lpx R) L1 L2 → lpx (TC … R) L1 L2. +lemma lpx_TC: ∀R,L1,L2. TC … (lpx R) L1 L2 → lpx (TC … R) L1 L2. #R #L1 #L2 #H elim H -L2 /2 width=1/ /2 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma index ab02943a8..fbbb1085e 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/notation.ma @@ -308,10 +308,6 @@ notation "hvbox( L ⊢ break term 46 T1 ➡ break term 46 T2 )" non associative with precedence 45 for @{ 'PRed $L $T1 $T2 }. -notation "hvbox( L1 ⊢ ➡ break term 46 L2 )" - non associative with precedence 45 - for @{ 'CPRed $L1 $L2 }. - notation "hvbox( ⦃ L1 ⦄ ➡ break ⦃ L2 ⦄ )" non associative with precedence 45 for @{ 'FocalizedPRed $L1 $L2 }. @@ -320,6 +316,10 @@ notation "hvbox( ⦃ L1, break T1 ⦄ ➡ break ⦃ L2 , break T2 ⦄ )" non associative with precedence 45 for @{ 'FocalizedPRed $L1 $T1 $L2 $T2 }. +notation "hvbox( L ⊢ break ⦃ L1, break T1 ⦄ ➡ break ⦃ L2 , break T2 ⦄ )" + non associative with precedence 45 + for @{ 'FocalizedPRed $L $L1 $T1 $L2 $T2 }. + notation "hvbox( ⦃ L1 ⦄ ➡ ➡ break ⦃ L2 ⦄ )" non associative with precedence 45 for @{ 'FocalizedPRedAlt $L1 $L2 }. @@ -330,27 +330,27 @@ notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 ➸ break [ g ] break (* Computation **************************************************************) -notation "hvbox( T1 ➡* break term 46 T2 )" +notation "hvbox( T1 ➡ * break term 46 T2 )" non associative with precedence 45 for @{ 'PRedStar $T1 $T2 }. -notation "hvbox( L ⊢ break term 46 T1 ➡* break term 46 T2 )" +notation "hvbox( L ⊢ break term 46 T1 ➡ * break term 46 T2 )" non associative with precedence 45 for @{ 'PRedStar $L $T1 $T2 }. -notation "hvbox( T1 ➡➡* break term 46 T2 )" +notation "hvbox( T1 ➡ ➡ * break term 46 T2 )" non associative with precedence 45 for @{ 'PRedStarAlt $T1 $T2 }. -notation "hvbox( L1 ⊢ ➡* break term 46 L2 )" +notation "hvbox( ⦃ L1 ⦄ ➡ * ⦃ L2 ⦄ )" non associative with precedence 45 - for @{ 'CPRedStar $L1 $L2 }. + for @{ 'FocalizedPRedStar $L1 $L2 }. -notation "hvbox( L ⊢ break term 46 T1 ➡* break 𝐍 ⦃ T2 ⦄ )" +notation "hvbox( L ⊢ break term 46 T1 ➡ * break 𝐍 ⦃ T2 ⦄ )" non associative with precedence 45 for @{ 'PEval $L $T1 $T2 }. -notation "hvbox( ⬊ * term 46 T )" +notation "hvbox( ⬊ * term 46 T )" non associative with precedence 45 for @{ 'SN $T }. @@ -384,9 +384,9 @@ notation "hvbox( L ⊢ break term 46 T1 ⬌ break term 46 T2 )" non associative with precedence 45 for @{ 'PConv $L $T1 $T2 }. -notation "hvbox( T1 ⊢ ⬌ break term 46 T2 )" +notation "hvbox( ⦃ L1 ⦄ ⬌ ⦃ L2 ⦄ )" non associative with precedence 45 - for @{ 'CPConv $T1 $T2 }. + for @{ 'FocalizedPConv $L1 $L2 }. (* Equivalence **************************************************************) @@ -394,9 +394,9 @@ notation "hvbox( L ⊢ break term 46 T1 ⬌* break term 46 T2 )" non associative with precedence 45 for @{ 'PConvStar $L $T1 $T2 }. -notation "hvbox( T1 ⊢ ⬌* break term 46 T2 )" +notation "hvbox( ⦃ L1 ⦄ ⬌ * ⦃ L2 ⦄ )" non associative with precedence 45 - for @{ 'CPConvStar $T1 $T2 }. + for @{ 'FocalizedPConvStar $L1 $L2 }. (* Dynamic typing ***********************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr.ma new file mode 100644 index 000000000..95c01d19f --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr.ma @@ -0,0 +1,55 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cpr.ma". +include "basic_2/reducibility/fpr.ma". + +(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON CLOSURES *************************) + +definition cfpr: lenv → bi_relation lenv term ≝ + λL,L1,T1,L2,T2. |L1| = |L2| ∧ L ⊢ L1 @@ T1 ➡ L2 @@ T2. + +interpretation + "context-sensitive parallel reduction (closure)" + 'FocalizedPRed L L1 T1 L2 T2 = (cfpr L L1 T1 L2 T2). + +(* Basic properties *********************************************************) + +lemma cfpr_refl: ∀L. bi_reflexive … (cfpr L). +/2 width=1/ qed. + +lemma fpr_cfpr: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → ⋆ ⊢ ⦃L1, T1⦄ ➡ ⦃L2, T2⦄. +#L1 #L2 #T1 #T2 * /3 width=1/ +qed. + +(* Basic inversion lemmas ***************************************************) + +lemma cfpr_inv_atom1: ∀L,L2,T1,T2. L ⊢ ⦃⋆, T1⦄ ➡ ⦃L2, T2⦄ → L ⊢ T1 ➡ T2 ∧ L2 = ⋆. +#L #L2 #T1 #T2 * #H >(length_inv_zero_sn … H) /2 width=1/ +qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma fpr_inv_pair1_sn: ∀I,K1,L2,V1,T1,T2. ⦃⋆.ⓑ{I}V1@@K1, T1⦄ ➡ ⦃L2, T2⦄ → + ∃∃K2,V2. V1 ➡ V2 & + ⋆.ⓑ{I}V2 ⊢ ⦃K1, T1⦄ ➡ ⦃K2, T2⦄ & + L2 = ⋆.ⓑ{I}V2@@K2. +#I1 #K1 #L2 #V1 #T1 #T2 * >append_length #H +elim (length_inv_pos_sn_append … H) -H #I2 #K2 #V2 #HK12 #H destruct +>shift_append_assoc >shift_append_assoc normalize in ⊢ (%→?); #H +elim (tpr_inv_bind1 … H) -H * +[ #V0 #T #T0 #HV10 #HT1 #HT0 #H destruct /5 width=5/ +| #T0 #_ #_ #H destruct +] +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_aaa.ma new file mode 100644 index 000000000..f893a5c14 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_aaa.ma @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||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_ltpss_sn.ma". +include "basic_2/reducibility/ltpr_aaa.ma". +include "basic_2/reducibility/cpr_aaa.ma". +include "basic_2/reducibility/cfpr_cpr.ma". + +(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON CLOSURES *************************) + +(* Properties about atomic arity assignment on terms ************************) + +lemma aaa_fpr_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → + ∀L2,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → L2 ⊢ T2 ⁝ A. +#L1 #T1 #A #HT1 #L2 #T2 #H +elim (fpr_inv_all … H) -H +/4 width=5 by aaa_cpr_conf, aaa_ltpr_conf, aaa_ltpss_sn_conf/ +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_cpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_cpr.ma new file mode 100644 index 000000000..f37cb5159 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_cpr.ma @@ -0,0 +1,66 @@ +(**************************************************************************) +(* ___ *) +(* ||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.ma". +include "basic_2/reducibility/cpr_tpss.ma". +include "basic_2/reducibility/cpr_cpr.ma". +include "basic_2/reducibility/cfpr_ltpss.ma". + +(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON CLOSURES *************************) + +(* Advanced properties ******************************************************) + +lemma fpr_all: ∀L1,L. L1 ➡ L → ∀L2,T1,T2. L ⊢ T1 ➡ T2 → + L ⊢ ▶* [0, |L|] L2 → ⦃L1, T1⦄ ➡ ⦃L2, T2⦄. +#L1 #L #H elim H -L1 -L +[ #L2 #T1 #T2 #HT12 #HL2 + lapply (ltpss_sn_inv_atom1 … HL2) -HL2 #H destruct + lapply (cpr_inv_atom … HT12) -HT12 /2 width=1/ +| #I #L1 #L #V1 #V #_ #HV1 #IH #X #T1 #T2 #HT12 #H + elim (ltpss_sn_inv_tpss21 … H ?) -H // append_length >append_length #H + lapply (injective_plus_r … H) -H #H + @(ex3_1_intro … (⋆.ⓑ{I}V@@Y)) append_length H -H >commutative_plus /3 width=1/ +] +qed-. + +lemma fpr_inv_all: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → + ∃∃L. L1 ➡ L & L ⊢ T1 ➡ T2 & L ⊢ ▶* [0, |L|] L2. +#L1 #L2 #T1 #T2 #H +lapply (fpr_cfpr … H) -H #H +elim (cfpr_inv_all … H) -H /2 width=4/ +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_ltpss.ma new file mode 100644 index 000000000..424911376 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_ltpss.ma @@ -0,0 +1,39 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cpr_lift.ma". +include "basic_2/reducibility/cpr_ltpss.ma". +include "basic_2/reducibility/cfpr.ma". + +(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON CLOSURES *************************) + +(* Advanced inversion lemmas ************************************************) + +lemma cfpr_inv_pair1: ∀I,L,K1,L2,V1,T1,T2. L ⊢ ⦃⋆.ⓑ{I}V1@@K1, T1⦄ ➡ ⦃L2, T2⦄ → + ∃∃K2,V,V2. V1 ➡ V & L ⊢ V ▶* [0, |L|] V2 & + L.ⓑ{I}V ⊢ ⦃K1, T1⦄ ➡ ⦃K2, T2⦄ & + L2 = ⋆.ⓑ{I}V2@@K2. +* #L #K1 #L2 #V1 #T1 #T2 * >append_length #H +elim (length_inv_pos_sn_append … H) -H #I2 #K2 #V2 #HK12 #H destruct +>shift_append_assoc >shift_append_assoc normalize in ⊢ (??%%→?); #H +[ elim (cpr_inv_abbr1 … H) -H * + [ #V #V0 #T0 #HV1 #HV0 #HT10 #H destruct /3 width=7/ + | #T0 #_ #_ #H destruct + ] +| elim (cpr_inv_abst1 … H Abst V2) -H + #V #T * #V0 #HV10 #HV0 #HT1 #H destruct + lapply (ltpss_sn_cpr_trans (L.ⓛV0) … 0 (|L|+1) … HT1) -HT1 /2 width=1/ #HT12 + /3 width=7/ +] +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_aaa.ma new file mode 100644 index 000000000..7c1273334 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_aaa.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||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_ltpss_sn.ma". +include "basic_2/reducibility/ltpr_aaa.ma". +include "basic_2/reducibility/cpr.ma". + +(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************) + +(* Properties about atomic arity assignment on terms ************************) + +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. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma index 43bce2b1a..b54510e8c 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma @@ -134,7 +134,7 @@ elim (cpr_inv_appl1 … H) -H * elim (simple_inv_bind … HT1) ] qed-. - + (* Relocation properties ****************************************************) (* Basic_1: was: pr2_lift *) diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_tpss.ma new file mode 100644 index 000000000..e5afe8737 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_tpss.ma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||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/tpss_tpss.ma". +include "basic_2/reducibility/cpr.ma". + +(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************) + +(* Properties on partial unfold for terms ***********************************) + +lemma cpr_tpss_trans: ∀L,T1,T. L ⊢ T1 ➡ T → + ∀T2. L ⊢ T ▶* [O, |L|] T2 → L ⊢ T1 ➡ T2. +#L #T1 #T * #T0 #HT10 #HT0 #T2 #HT2 +lapply (tpss_trans_eq … HT0 HT2) -T /2 width=3/ +qed. + +lemma cpr_tps_trans: ∀L,T1,T. L ⊢ T1 ➡ T → + ∀T2. L ⊢ T ▶ [O, |L|] T2 → L ⊢ T1 ➡ T2. +/3 width=3/ 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 b4c15e856..391061565 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr.ma @@ -14,13 +14,13 @@ include "basic_2/reducibility/tpr.ma". -(* FOCALIZED PARALLEL REDUCTION ON CLOSURES *********************************) +(* CONTEXT-FREE PARALLEL REDUCTION ON CLOSURES ******************************) definition fpr: bi_relation lenv term ≝ λL1,T1,L2,T2. |L1| = |L2| ∧ L1 @@ T1 ➡ L2 @@ T2. interpretation - "focalized parallel reduction (closure)" + "context-free parallel reduction (closure)" 'FocalizedPRed L1 T1 L2 T2 = (fpr L1 T1 L2 T2). (* Basic properties *********************************************************) @@ -28,31 +28,37 @@ interpretation lemma fpr_refl: bi_reflexive … fpr. /2 width=1/ qed. +lemma fpr_shift: ∀I1,I2,L1,L2,V1,V2,T1,T2. + ⦃L1, -ⓑ{I1}V1.T1⦄ ➡ ⦃L2, -ⓑ{I2}V2.T2⦄ → + ⦃L1.ⓑ{I1}V1, T1⦄ ➡ ⦃L2.ⓑ{I2}V2, T2⦄. +#I1 #I2 #L1 #L2 #V1 #V2 #T1 #T2 * #HL12 #HT12 +@conj // normalize // (**) (* explicit constructor *) +qed. + (* Basic inversion lemmas ***************************************************) lemma fpr_inv_atom1: ∀L2,T1,T2. ⦃⋆, T1⦄ ➡ ⦃L2, T2⦄ → T1 ➡ T2 ∧ L2 = ⋆. #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. -#I1 #K1 #L2 #V1 #T1 #T2 * #H -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. + +(* Basic forward lemmas *****************************************************) + +lemma fpr_fwd_pair1: ∀I1,K1,L2,V1,T1,T2. ⦃K1.ⓑ{I1}V1, T1⦄ ➡ ⦃L2, T2⦄ → + ∃∃I2,K2,V2. ⦃K1, -ⓑ{I1}V1.T1⦄ ➡ ⦃K2, -ⓑ{I2}V2.T2⦄ & + L2 = K2.ⓑ{I2}V2. +#I1 #K1 #L2 #V1 #T1 #T2 * #H +elim (length_inv_pos_sn … H) -H #I2 #K2 #V2 #HK12 #H destruct /3 width=5/ +qed-. + +lemma fpr_fwd_pair3: ∀I2,L1,K2,V2,T1,T2. ⦃L1, T1⦄ ➡ ⦃K2.ⓑ{I2}V2, T2⦄ → + ∃∃I1,K1,V1. ⦃K1, -ⓑ{I1}V1.T1⦄ ➡ ⦃K2, -ⓑ{I2}V2.T2⦄ & + L1 = K1.ⓑ{I1}V1. #I2 #L1 #K2 #V2 #T1 #T2 * #H -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/ +elim (length_inv_pos_dx … H) -H #I1 #K1 #V1 #HK12 #H destruct /3 width=5/ qed-. -*) diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr_cpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr_cpr.ma new file mode 100644 index 000000000..e034710b2 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr_cpr.ma @@ -0,0 +1,61 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cfpr_cpr.ma". + +(* FOCALIZED PARALLEL REDUCTION ON CLOSURES *********************************) + +(* Advanced propertis *******************************************************) + +lemma fpr_bind_sn: ∀L1,L2,V1,V2. ⦃L1, V1⦄ ➡ ⦃L2, V2⦄ → ∀T1,T2. T1 ➡ T2 → + ∀a,I. ⦃L1, ⓑ{a,I}V1.T1⦄ ➡ ⦃L2, ⓑ{a,I}V2.T2⦄. +#L1 #L2 #V1 #V2 #H #T1 #T2 #HT12 #a #I +elim (fpr_inv_all … H) /3 width=4/ +qed. + +(* Advanced forward lemmas **************************************************) + +lemma fpr_fwd_shift_bind_minus: ∀I1,I2,L1,L2,V1,V2,T1,T2. + ⦃L1, -ⓑ{I1}V1.T1⦄ ➡ ⦃L2, -ⓑ{I2}V2.T2⦄ → + ⦃L1, V1⦄ ➡ ⦃L2, V2⦄ ∧ I1 = I2. +* #I2 #L1 #L2 #V1 #V2 #T1 #T2 #H +elim (fpr_inv_all … H) -H #L #HL1 #H #HL2 +[ elim (cpr_inv_abbr1 … H) -H * + [ #V #V0 #T #HV1 #HV0 #_ #H destruct /4 width=4/ + | #T #_ #_ #H destruct + ] +| elim (cpr_inv_abst1 … H Abst V2) -H + #V #T #HV1 #_ #H destruct /3 width=4/ +] +qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma fpr_inv_pair1: ∀I,K1,L2,V1,T1,T2. ⦃K1.ⓑ{I}V1, T1⦄ ➡ ⦃L2, T2⦄ → + ∃∃K2,V2. ⦃K1, V1⦄ ➡ ⦃K2, V2⦄ & + ⦃K1, -ⓑ{I}V1.T1⦄ ➡ ⦃K2, -ⓑ{I}V2.T2⦄ & + L2 = K2.ⓑ{I}V2. +#I1 #K1 #X #V1 #T1 #T2 #H +elim (fpr_fwd_pair1 … H) -H #I2 #K2 #V2 #HT12 #H destruct +elim (fpr_fwd_shift_bind_minus … HT12) #HV12 #H destruct /2 width=5/ +qed-. + +lemma fpr_inv_pair3: ∀I,L1,K2,V2,T1,T2. ⦃L1, T1⦄ ➡ ⦃K2.ⓑ{I}V2, T2⦄ → + ∃∃K1,V1. ⦃K1, V1⦄ ➡ ⦃K2, V2⦄ & + ⦃K1, -ⓑ{I}V1.T1⦄ ➡ ⦃K2, -ⓑ{I}V2.T2⦄ & + L1 = K1.ⓑ{I}V1. +#I2 #X #K2 #V2 #T1 #T2 #H +elim (fpr_fwd_pair3 … H) -H #I1 #K1 #V1 #HT12 #H destruct +elim (fpr_fwd_shift_bind_minus … HT12) #HV12 #H destruct /2 width=5/ +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 deleted file mode 100644 index ed93e5cf9..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr.ma +++ /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/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 -. - -interpretation - "context-sensitive parallel reduction (environment)" - 'CPRed L1 L2 = (lcpr L1 L2). - -(* Basic properties *********************************************************) - -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_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 deleted file mode 100644 index d25abb4b5..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_aaa.ma +++ /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_ltpss_sn.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/reducibility/lcpr_cpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_cpr.ma deleted file mode 100644 index 22f3a398c..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_cpr.ma +++ /dev/null @@ -1,29 +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_sn_ltpss_sn.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 * -<(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. 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 deleted file mode 100644 index d526b345e..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_lcpr.ma +++ /dev/null @@ -1,39 +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_ltpss_sn.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 (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_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/ -qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr.ma new file mode 100644 index 000000000..c8adecd25 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr.ma @@ -0,0 +1,40 @@ +(**************************************************************************) +(* ___ *) +(* ||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.ma". +include "basic_2/reducibility/ltpr.ma". + +(* FOCALIZED PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ***********************) + +definition lfpr: relation lenv ≝ + λL1,L2. ∃∃L. L1 ➡ L & L ⊢ ▶* [0, |L|] L2 +. + +interpretation + "focalized parallel reduction (environment)" + 'FocalizedPRed L1 L2 = (lfpr L1 L2). + +(* Basic properties *********************************************************) + +lemma lfpr_refl: ∀L. ⦃L⦄ ➡ ⦃L⦄. +/2 width=3/ qed. + +lemma ltpss_sn_lfpr: ∀L1,L2,d,e. L1 ⊢ ▶* [d, e] L2 → ⦃L1⦄ ➡ ⦃L2⦄. +/3 width=5/ qed. + +(* Basic inversion lemmas ***************************************************) + +lemma lfpr_inv_atom1: ∀L2. ⦃⋆⦄ ➡ ⦃L2⦄ → L2 = ⋆. +#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/lfpr_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_aaa.ma new file mode 100644 index 000000000..6f6c49df3 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_aaa.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||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_ltpss_sn.ma". +include "basic_2/reducibility/ltpr_aaa.ma". +include "basic_2/reducibility/lfpr.ma". + +(* FOCALIZED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS **********************) + +(* Properties about atomic arity assignment on terms ************************) + +lemma aaa_lfpr_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. ⦃L1⦄ ➡ ⦃L2⦄ → L2 ⊢ T ⁝ A. +#L1 #T #A #HT #L2 * /3 width=5/ +qed. 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 bfb483781..adff7ad07 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 @@ -13,7 +13,8 @@ (**************************************************************************) include "basic_2/grammar/lenv_px_bi.ma". -include "basic_2/reducibility/fpr.ma". +include "basic_2/reducibility/fpr_cpr.ma". +include "basic_2/reducibility/lfpr_fpr.ma". (* FOCALIZED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS **********************) @@ -29,6 +30,15 @@ interpretation lemma lfpra_refl: reflexive … lfpra. /2 width=1/ qed. +lemma fpr_lfpra: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → ⦃L1⦄ ➡➡ ⦃L2⦄. +#L1 elim L1 -L1 +[ #L2 #T1 #T2 #H + elim (fpr_inv_atom1 … H) -H #_ #H destruct // +| #L1 #I #V1 #IH #L2 #T1 #T2 #H + elim (fpr_inv_pair1 … H) -H #L #V #HV1 #HL1 #H destruct /3 width=3/ +] +qed. + (* Basic inversion lemmas ***************************************************) lemma lfpra_inv_atom1: ∀L2. ⦃⋆⦄ ➡➡ ⦃L2⦄ → L2 = ⋆. @@ -47,48 +57,23 @@ lemma lfpra_inv_pair2: ∀L1,K2,I,V2. ⦃L1⦄ ➡➡ ⦃K2. ⓑ{I} V2⦄ → L1 = K1. ⓑ{I} V1. /2 width=1 by lpx_bi_inv_pair2/ qed-. +lemma lfpra_inv_fpr: ∀L1,L2. ⦃L1⦄ ➡➡ ⦃L2⦄ → ∀T.⦃L1, T⦄ ➡ ⦃L2, T⦄. +#L1 #L2 * -L1 -L2 // /3 width=1/ +qed-. + (* Basic forward lemmas *****************************************************) 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 - elim (fpr_inv_atom1 … H) -H #_ #H destruct // -| #L1 #I #V1 #T1 #IH #Y #X #H - elim (fpr_inv_pair1 … H) -H #L2 #V2 #HL12 #H destruct - @lpx_bi_pair - [ @(IH … HL12) - | @IH - - /3 width=4/ +(* Main properties **********************************************************) -lemma fpr_lfpra: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → ⦃L1⦄ ➡➡ ⦃L2⦄. -#L1 elim L1 -L1 -[ #L2 #T1 #T2 #H - elim (fpr_inv_atom1 … H) -H #_ #H destruct // -| #L1 #I #V1 #IH #L2 #T1 #T2 #H - elim (fpr_inv_pair1 … H) -H #L #V #HL1 #H destruct - @lpx_bi_pair /2 width=3/ - - /4 width=3/ - -(* -include "basic_2/reducibility/lcpr.ma". - -lemma lcpr_pair2: ∀L1,L2. L1 ⊢ ➡ L2 → ∀V1,V2. ⦃L1, V1⦄ ➡ ⦃L2, V2⦄ → - ∀I. L1. ⓑ{I} V1 ⊢ ➡ L2. ⓑ{I} V2. -#L1 #L2 * #L #HL1 #HL2 #V1 #V2 * -#H1 #H2 #I -@(ex2_1_intro … (L.ⓑ{I}V1)) /2 width=1/ -@tpss_ - -(* -<(ltpss_fwd_length … HL2) /4 width=5/ +theorem lfpr_lfpra: ∀L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ → ⦃L1⦄ ➡➡ ⦃L2⦄. +#L1 #L2 #H +lapply (lfpr_inv_fpr … H (⋆0)) -H /2 width=3/ qed. -*) -*) -*) \ No newline at end of file + +theorem lfpra_lfpr: ∀L1,L2. ⦃L1⦄ ➡➡ ⦃L2⦄ → ⦃L1⦄ ➡ ⦃L2⦄. +#L1 #L2 #H +lapply (lfpra_inv_fpr … H (⋆0)) -H /2 width=3/ +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_cpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_cpr.ma new file mode 100644 index 000000000..2a40f58bd --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_cpr.ma @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||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_ltpss_sn.ma". +include "basic_2/reducibility/cpr.ma". +include "basic_2/reducibility/lfpr.ma". + +(* FOCALIZED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS **********************) + +(* Advanced properties ****************************************************) + +lemma lfpr_pair_cpr: ∀L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀V1,V2. L2 ⊢ V1 ➡ V2 → + ∀I. ⦃L1. ⓑ{I} V1⦄ ➡ ⦃L2. ⓑ{I} V2⦄. +#L1 #L2 * #L #HL1 #HL2 #V1 #V2 * +<(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. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_fpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_fpr.ma new file mode 100644 index 000000000..9a226be58 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_fpr.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/reducibility/lfpr.ma". +include "basic_2/reducibility/cfpr_cpr.ma". + +(* FOCALIZED PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ***********************) + +(* Inversion lemmas on context-free parallel reduction for closures *********) + +lemma fpr_lfpr: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → ⦃L1⦄ ➡ ⦃L2⦄. +#L1 #L2 #T1 #T2 #H +elim (fpr_inv_all … H) -H /2 width=3/ +qed. + +(* Inversion lemmas on context-free parallel reduction for closures *********) + +lemma lfpr_inv_fpr: ∀L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀T. ⦃L1, T⦄ ➡ ⦃L2, T⦄. +#L1 #L2 * /2 width=4/ +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_lfpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_lfpr.ma new file mode 100644 index 000000000..7031e792b --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_lfpr.ma @@ -0,0 +1,39 @@ +(**************************************************************************) +(* ___ *) +(* ||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_ltpss_sn.ma". +include "basic_2/reducibility/ltpr_ltpr.ma". +include "basic_2/reducibility/lfpr.ma". + +(* FOCALIZED PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ***********************) + +(* Main properties **********************************************************) + +theorem lfpr_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 (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_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/ +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 index 67986d336..a910ea7df 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr.ma @@ -28,6 +28,9 @@ interpretation lemma ltpr_refl: reflexive … ltpr. /2 width=1/ qed. +lemma ltpr_append: ∀K1,K2. K1 ➡ K2 → ∀L1,L2:lenv. L1 ➡ L2 → K1 @@ L1 ➡ K2 @@ L2. +/2 width=1/ qed. + (* Basic inversion lemmas ***************************************************) (* Basic_1: was: wcpr0_gen_sort *) @@ -51,4 +54,14 @@ lemma ltpr_inv_pair2: ∀L1,K2,I,V2. L1 ➡ K2. ⓑ{I} V2 → lemma ltpr_fwd_length: ∀L1,L2. L1 ➡ L2 → |L1| = |L2|. /2 width=2 by lpx_fwd_length/ qed-. +(* Advanced inversion lemmas ************************************************) + +lemma ltpr_inv_append1: ∀K1,L1. ∀L:lenv. K1 @@ L1 ➡ L → + ∃∃K2,L2. K1 ➡ K2 & L1 ➡ L2 & L = K2 @@ L2. +/2 width=1 by lpx_inv_append1/ qed-. + +lemma ltpr_inv_append2: ∀L:lenv. ∀K2,L2. L ➡ K2 @@ L2 → + ∃∃K1,L1. K1 ➡ K2 & L1 ➡ L2 & L = K1 @@ L1. +/2 width=1 by lpx_inv_append2/ qed-. + (* Basic_1: removed theorems 2: wcpr0_getl wcpr0_getl_back *) 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 16353b450..b05484129 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma @@ -220,11 +220,25 @@ lemma tpr_fwd_shift1: ∀L1,T1,T. L1 @@ T1 ➡ T → ] ] qed-. - -lemma tpr_fwd_shift_bind_minus: ∀L1,L2. |L1| = |L2| → ∀I1,I2,V1,V2,T1,T2. - L1 @@ -ⓑ{I1}V1.T1 ➡ L2 @@ -ⓑ{I2}V2.T2 → - L1 𝟙 L2 ∧ I1 = I2. -#L1 #L2 #HL12 #I1 #I2 #V1 #V2 #T1 #T2 #H +*) + + +(* + >shift_append_assoc >shift_append_assoc >shift_append_assoc >shift_append_assoc normalize #H + elim (tpr_inv_bind1 … H) -H * + [ #V #T #T0 #HV1 #HT1 #HT0 #H destruct /2 width=1/ + | #T #_ #_ #H destruct + ] + + lapply (IH … HT12) + + + >shift_append_assoc >shift_append_assoc >shift_append_assoc #HT12 + lapply (shift_inj … HT12) -HT12 + + + + #L2 #HL12 #I1 #I2 #V1 #V2 #T1 #T2 #H elim (tpr_fwd_shift1 (L1.ⓑ{I1}V1) … H) -H #Y #X #HY #HX elim (ltop_inv_pair1 … HY) -HY #L #V #HL1 #H destruct elim (shift_inj (L2.ⓑ{I2}V2) … HX ?) -HX diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_aaa.ma index 051ef0514..bce096e3b 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_aaa.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/static/ssta_aaa.ma". -include "basic_2/reducibility/lcpr_aaa.ma". +include "basic_2/reducibility/cpr_aaa.ma". include "basic_2/reducibility/xpr.ma". (* EXTENDED PARALLEL REDUCTION ON TERMS *************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx.ma index ad0c002b4..d9d704221 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx.ma @@ -233,6 +233,11 @@ lemma ltpss_dx_append_le: ∀K1,K2,d. K1 ▶* [d, |K1| - d] K2 → L1 @@ K1 ▶* [d, |K1| - d + e] L2 @@ K2. /2 width=1 by ltpss_dx_append_le_aux/ qed. +lemma ltpss_dx_append_zero: ∀K1,K2. K1 ▶* [0, |K1|] K2 → + ∀L1,L2,e. L1 ▶* [0, e] L2 → + L1 @@ K1 ▶* [0, |K1| + e] L2 @@ K2. +/2 width=1/ qed. + lemma ltpss_dx_append_ge: ∀K1,K2,d,e. K1 ▶* [d, e] K2 → ∀L1,L2. L1 ▶* [d - |K1|, e] L2 → |K1| ≤ d → L1 @@ K1 ▶* [d, e] L2 @@ K2. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn_ltpss_sn.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn_ltpss_sn.ma index ef8e554d0..7aa2c5df2 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn_ltpss_sn.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn_ltpss_sn.ma @@ -70,14 +70,17 @@ qed. (* Advanced forward lemmas **************************************************) lemma tps_fwd_shift1: ∀L1,L,T1,T,d,e. L ⊢ L1 @@ T1 ▶ [d, e] T → - ∃∃L2,T2. L @@ L1 ⊢ ▶* [d + |L1|, e] L @@ L2 & T = L2 @@ T2. + ∃∃L2,T2. L @@ L1 ⊢ ▶* [d + |L1|, e] L @@ L2 & + L @@ L2 ⊢ T1 ▶ [d + |L1|, e] T2 & + T = L2 @@ T2. #L1 @(lenv_ind_dx … L1) -L1 -[ #L #T1 #T #d #e #_ @ex2_2_intro [3: // |4: // |1,2: skip ] (**) (* /2 width=4/ does not work *) +[ #L #T1 #T #d #e #HT1 + @ex3_2_intro [3: // |5: // |4: normalize /2 width=1/ |1,2: skip ] (**) (* /2 width=4/ does not work *) | #I #L1 #V1 #IH #L #T1 #T #d #e >shift_append_assoc #H elim (tps_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct - elim (IH … HT12) -IH -T1 #L2 #T #HL12 #H destruct + elim (IH … HT12) -IH -HT12 #L2 #T #HL12 #HT1 #H destruct append_length