From 420a46d71dc2c9b7e88514a717ea9637b842ce6a Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 6 Feb 2013 20:51:46 +0000 Subject: [PATCH] - lambdadelta: more service lemmas ... - matitadep: bug fix due to new invocation from Makefile --- .../binaries/matitadep/matitadep.ml | 2 +- .../basic_2/computation/fprs_cprs.ma | 75 +++++++++++++------ .../basic_2/computation/lfprs_cprs.ma | 3 + .../basic_2/computation/lfprs_fprs.ma | 38 ++++++++++ .../basic_2/computation/lfprs_ltprs.ma | 23 ++++++ .../lambdadelta/basic_2/computation/ltprs.ma | 6 ++ .../lambdadelta/basic_2/dynamic/snv_ltpr.ma | 16 ++-- .../basic_2/equivalence/fpcs_cpcs.ma | 31 +++++++- .../lambdadelta/basic_2/reducibility/cpr.ma | 8 ++ .../basic_2/reducibility/fpr_cpr.ma | 25 ++++++- .../lambdadelta/basic_2/reducibility/lfpr.ma | 3 + .../basic_2/reducibility/lfpr_cpr.ma | 2 +- .../basic_2/reducibility/lfpr_fpr.ma | 2 +- .../lambdadelta/basic_2/reducibility/tpr.ma | 9 +++ 14 files changed, 208 insertions(+), 35 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_fprs.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_ltprs.ma diff --git a/matita/components/binaries/matitadep/matitadep.ml b/matita/components/binaries/matitadep/matitadep.ml index ebb87695f..fdf5e980f 100644 --- a/matita/components/binaries/matitadep/matitadep.ml +++ b/matita/components/binaries/matitadep/matitadep.ml @@ -40,7 +40,7 @@ let check () = Hashtbl.iter iter graph let rec read ich = - let _ = Scanf.fscanf ich "./%s@:include \"%s@\". " init in + let _ = Scanf.fscanf ich "%s@:include \"%s@\". " init in read ich let _ = diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fprs_cprs.ma index 4e7a633c3..0464705b9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fprs_cprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fprs_cprs.ma @@ -13,18 +13,67 @@ (**************************************************************************) include "basic_2/reducibility/fpr_cpr.ma". -include "basic_2/computation/cprs.ma". -include "basic_2/computation/fprs.ma". +include "basic_2/computation/cprs_lfprs.ma". +include "basic_2/computation/lfprs_ltprs.ma". +include "basic_2/computation/lfprs_fprs.ma". (* CONTEXT-FREE PARALLEL COMPUTATION ON CLOSURES ****************************) +(* Advanced inversion lemmas ************************************************) + +lemma fprs_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. +#I #K1 #L2 #V1 #T1 #T2 #H @(fprs_ind … H) -L2 -T2 /2 width=5/ +#L #L2 #T #T2 #_ #HT2 * #K #V #HV1 #HT1 #H destruct +elim (fpr_inv_pair1 … HT2) -HT2 #K2 #V2 #HV2 #HT2 #H destruct /3 width=5/ +qed-. + +lemma fprs_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 #L1 #K2 #V2 #T1 #T2 #H @(fprs_ind_dx … H) -L1 -T1 /2 width=5/ +#L1 #L #T1 #T #HT1 #_ * #K #V #HV2 #HT2 #H destruct +elim (fpr_inv_pair3 … HT1) -HT1 #K1 #V1 #HV1 #HT1 #H destruct /3 width=5/ +qed-. + +(* Advanced forward lemmas **************************************************) + +lemma fprs_fwd_bind2_minus: ∀I,L1,L,V1,T1,T. ⦃L1, -ⓑ{I}V1.T1⦄ ➡* ⦃L, T⦄ → ∀b. + ∃∃V2,T2. ⦃L1, ⓑ{b,I}V1.T1⦄ ➡* ⦃L, ⓑ{b,I}V2.T2⦄ & + T = -ⓑ{I}V2.T2. +#I #L1 #L #V1 #T1 #T #H1 #b @(fprs_ind … H1) -L -T /2 width=4/ +#L0 #L #T0 #T #_ #H0 * #W1 #U1 #HTU1 #H destruct +elim (fpr_fwd_bind2_minus … H0 b) -H0 /3 width=4/ +qed-. + +lemma fprs_fwd_pair1_full: ∀I,K1,L2,V1,T1,T2. ⦃K1.ⓑ{I}V1, T1⦄ ➡* ⦃L2, T2⦄ → + ∀b. ∃∃K2,V2. ⦃K1, V1⦄ ➡* ⦃K2, V2⦄ & + ⦃K1, ⓑ{b,I}V1.T1⦄ ➡* ⦃K2, ⓑ{b,I}V2.T2⦄ & + L2 = K2.ⓑ{I}V2. +#I #K1 #L2 #V1 #T1 #T2 #H #b +elim (fprs_inv_pair1 … H) -H #K2 #V2 #HV12 #HT12 #H destruct +elim (fprs_fwd_bind2_minus … HT12 b) -HT12 #W1 #U1 #HTU1 #H destruct /2 width=5/ +qed-. + (* Properties on context-sensitive parallel computation for terms ***********) lemma cprs_fprs: ∀L,T1,T2. L ⊢ T1 ➡* T2 → ⦃L, T1⦄ ➡* ⦃L, T2⦄. #L #T1 #T2 #H @(cprs_ind … H) -T2 // /3 width=4/ qed. + +(* Forward lemmas on context-sensitive parallel computation for terms *******) + +lemma fprs_fwd_cprs: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → L1 ⊢ T1 ➡* T2. +#L1 #L2 #T1 #T2 #H @(fprs_ind … H) -L2 -T2 // +#L #L2 #T #T2 #H1 #H2 #IH1 +elim (fpr_inv_all … H2) -H2 #L0 #HL0 #HT2 #_ -L2 +lapply (lfprs_cpr_trans L1 … HT2) -HT2 /3 width=3/ +qed-. (* -(* Advanced propertis *******************************************************) +(* Advanced properties ******************************************************) lamma 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⦄. @@ -47,24 +96,4 @@ elim (fpr_inv_all … H) -H #L #HL1 #H #HL2 #V #T #HV1 #_ #H destruct /3 width=4/ ] qed-. - -(* Advanced inversion lemmas ************************************************) - -lamma 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-. - -lamma 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/lambdadelta/basic_2/computation/lfprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_cprs.ma index b0f7c4a94..6eb25b377 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_cprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_cprs.ma @@ -25,3 +25,6 @@ lemma lfprs_pair_dx: ∀I,L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀V1,V2. L2 ⊢ V1 #I #L1 #L2 #HL12 #V1 #V2 #H @(cprs_ind … H) -V2 /3 width=1/ /3 width=5/ qed. +(* +lamma lfprs_cprs_conf: ∀L1,L,L2,T1,T2. ⦃L1⦄ ➡* ⦃L2⦄ → L1 ⊢ T1 ➡* T2 → ⦃L1, T1⦄ ➡* ⦃L2, T2⦄. +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_fprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_fprs.ma new file mode 100644 index 000000000..940a5044d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_fprs.ma @@ -0,0 +1,38 @@ +(**************************************************************************) +(* ___ *) +(* ||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_fpr.ma". +include "basic_2/computation/fprs_fprs.ma". +include "basic_2/computation/lfprs.ma". + +(* FOCALIZED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *********************) + +(* Inversion lemmas on context-free parallel reduction for closures *********) + +lemma lfprs_inv_fprs: ∀L1,L2. ⦃L1⦄ ➡* ⦃L2⦄ → ∀T. ⦃L1, T⦄ ➡* ⦃L2, T⦄. +#L1 #L2 #H @(lfprs_ind … H) -L2 // +#L #L2 #_ #HL2 #IHL1 #T +lapply (lfpr_inv_fpr … HL2 T) -HL2 /3 width=4/ +qed-. + +(* Properties on context-free parallel computation for closures *************) + +lemma fprs_lfprs: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → ⦃L1⦄ ➡* ⦃L2⦄. +#L1 #L2 #T1 #T2 #H @(fprs_ind … H) -L2 -T2 // /3 width=5/ +qed. + +lemma lfprs_fprs_trans: ∀L1,L,L2,T1,T2. ⦃L1⦄ ➡* ⦃L⦄ → ⦃L, T1⦄ ➡* ⦃L2, T2⦄ → ⦃L1, T1⦄ ➡* ⦃L2, T2⦄. +#L1 #L #L2 #T1 #T2 #HL1 #HL2 +lapply (lfprs_inv_fprs … HL1 T1) -HL1 /2 width=4/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_ltprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_ltprs.ma new file mode 100644 index 000000000..99ae801d7 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_ltprs.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/computation/ltprs.ma". +include "basic_2/computation/lfprs.ma". + +(* FOCALIZED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *********************) + +(* Properties on context-free parallel computation for local environments ***) + +lemma ltprs_lfprs: ∀L1,L2. L1 ➡* L2 → ⦃L1⦄ ➡* ⦃L2⦄. +/3 width=3/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs.ma index b7b0e1094..34ad45039 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs.ma @@ -44,6 +44,12 @@ qed-. lemma ltprs_refl: reflexive … ltprs. /2 width=1/ qed. +lemma ltprs_strap1: ∀L1,L,L2. L1 ➡* L → L ➡ L2 → L1 ➡* L2. +/2 width=3/ qed. + +lemma ltprs_strap2: ∀L1,L,L2. L1 ➡ L → L ➡* L2 → L1 ➡* L2. +/2 width=3/ qed. + (* Basic inversion lemmas ***************************************************) lemma ltprs_inv_atom1: ∀L2. ⋆ ➡* L2 → L2 = ⋆. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma index 92168e908..07ac7b543 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) + include "basic_2/reducibility/ltpr.ma". include "basic_2/computation/xprs_lift.ma". include "basic_2/equivalence/cpcs_cpcs.ma". include "basic_2/equivalence/lsubse_ssta.ma". -include "basic_2/equivalence/fpcs.ma". +include "basic_2/equivalence/fpcs_cpcs.ma". +include "basic_2/equivalence/fpcs_fpcs.ma". include "basic_2/dynamic/snv_ssta.ma". (* include "basic_2/static/ssta_ltpss_dx.ma". -include "basic_2/equivalence/fpcs_fpcs.ma". include "basic_2/dynamic/snv_lift.ma". *) (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) @@ -67,10 +68,15 @@ fact ssta_ltpr_tpr_aux: ∀h,g,n. ( elim (IH1 … HVW1 … HL12 … HV12) -HVW1 // -HV1 #W2 #HVW2 #HW12 elim (IH1 … HWV … HL12 W) -HWV // -HW #V0 #HWV0 #_ elim (IH1 … HTU2 (L2.ⓛW) … HT20 HT2) -IH1 -HTU2 -HT20 -HT2 // [2: /2 width=1/ ] #U20 #HTU20 #HU20 + lapply (lfpr_inv_fpr L1 L2 … W) [ /2 width=1/ ] -HL12 #HL12 elim (lsubse_ssta_trans … HTU20 (L2.ⓓV2) ?) -HTU20 - [ #U #HTU20 #HU20 -HWV0 -HL12 -W1 -W2 - @(ex2_intro … (ⓓ{b}V2.U)) [ /2 width=1/ ] -T20 -l - | @(lsubse_abbr … HVW2) // -g -h -b -l -l1 -V -V0 -V1 -V2 -T2 -T20 -U0 + [ #U #HTU20 #HU20 -HWV0 -HL12 -W1 -W2 + @(ex2_intro … (ⓓ{b}V2.U)) [ /2 width=1/ ] -h -l -l1 -V -V0 -T2 -T20 -U0 + @(fpcs_fprs_strap2 ? L1 … (ⓓ{b}V2.U2)) [ /4 width=1/ ] -V1 + @fpcs_shift_full -b + @(fpcs_canc_dx ?? (L2.ⓓV2) … U20) [2: /2 width=1/ ] -U + | -b -l -V -V1 -T2 -T20 -U0 -U2 -U20 + /6 width=6 by lsubse_abbr, fpcs_inv_cpcs, fpcs_canc_sn, fpcs_fprs_strap1, cpcs_fpcs, bi_inj/ ] ] | diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_cpcs.ma index 4b51a7084..eda395e98 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_cpcs.ma @@ -14,13 +14,42 @@ include "basic_2/computation/fprs_cprs.ma". include "basic_2/equivalence/cpcs_cpcs.ma". -include "basic_2/equivalence/fpcs_fprs.ma". +include "basic_2/equivalence/fpcs_fpcs.ma". (* CONTEXT-FREE PARALLEL EQUIVALENCE ON CLOSURES ****************************) +(* Advanced properties ******************************************************) + +lemma fpcs_shift: ∀I,L1,L2,V1,V2,T1,T2. ⦃L1.ⓑ{I}V1, T1⦄ ⬌* ⦃L2.ⓑ{I}V2, T2⦄ → + ⦃L1, -ⓑ{I}V1.T1⦄ ⬌* ⦃L2, -ⓑ{I}V2.T2⦄. +#I #L1 #L2 #V1 #V2 #T1 #T2 #H12 +elim (fpcs_inv_fprs … H12) -H12 #L #T #H1 #H2 +elim (fprs_inv_pair1 … H1) -H1 #K1 #U1 #_ #HTU1 #H destruct +elim (fprs_inv_pair1 … H2) -H2 #K2 #U2 #_ #HTU2 #H destruct /2 width=4/ +qed. + +lemma fpcs_bind_minus: ∀I,L1,L2,V1,V2,T1,T2. ⦃L1, -ⓑ{I}V1.T1⦄ ⬌* ⦃L2, -ⓑ{I}V2.T2⦄ → + ∀b. ⦃L1, ⓑ{b,I}V1.T1⦄ ⬌* ⦃L2, ⓑ{b,I}V2.T2⦄. +#I #L1 #L2 #V1 #V2 #T1 #T2 #H12 #b +elim (fpcs_inv_fprs … H12) -H12 #L #T #H1 #H2 +elim (fprs_fwd_bind2_minus … H1 b) -H1 #W1 #U1 #HTU1 #H destruct +elim (fprs_fwd_bind2_minus … H2 b) -H2 #W2 #U2 #HTU2 #H destruct /2 width=4/ +qed. + +lemma fpcs_shift_full: ∀I,L1,L2,V1,V2,T1,T2. ⦃L1.ⓑ{I}V1, T1⦄ ⬌* ⦃L2.ⓑ{I}V2, T2⦄ → + ∀b. ⦃L1, ⓑ{b,I}V1.T1⦄ ⬌* ⦃L2, ⓑ{b,I}V2.T2⦄. +/3 width=1/ qed. + (* Properties on context-sensitive parallel equivalence for terms ***********) lemma cpcs_fpcs: ∀L,T1,T2. L ⊢ T1 ⬌* T2 → ⦃L, T1⦄ ⬌* ⦃L, T2⦄. #L #T1 #T2 #H elim (cpcs_inv_cprs … H) -H /3 width=4 by fprs_div, cprs_fprs/ (**) (* too slow without trace *) qed. + +(* Inversion lemmas on context-sensitive parallel equivalence for terms *****) + +lemma fpcs_inv_cpcs: ∀L,T1,T2. ⦃L, T1⦄ ⬌* ⦃L, T2⦄ → L ⊢ T1 ⬌* T2. +#L #T1 #T2 #H +elim (fpcs_inv_fprs … H) -H /3 width=4 by cprs_div, fprs_fwd_cprs/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma index fffaad098..ae8e01bbc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma @@ -88,6 +88,14 @@ qed-. (* Basic forward lemmas *****************************************************) +lemma cpr_fwd_bind1_minus: ∀I,L,V1,T1,T. L ⊢ -ⓑ{I}V1.T1 ➡ T → ∀b. + ∃∃V2,T2. L ⊢ ⓑ{b,I}V1.T1 ➡ ⓑ{b,I}V2.T2 & + T = -ⓑ{I}V2.T2. +#I #L #V1 #T1 #T * #X #H1 #H2 #b +elim (tpr_fwd_bind1_minus … H1 b) -H1 #V0 #T0 #HT10 #H destruct +elim (tpss_inv_bind1 … H2) -H2 #V2 #T2 #HV02 #HT02 #H destruct /4 width=5/ +qed-. + lemma cpr_fwd_shift1: ∀L,L1,T1,T. L ⊢ L1 @@ T1 ➡ T → ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2. #L #L1 #T1 #T * #X #H1 #H2 diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr_cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr_cpr.ma index 0de0b98f5..9bd19002a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr_cpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr_cpr.ma @@ -21,7 +21,7 @@ include "basic_2/reducibility/cfpr_cpr.ma". lemma cpr_fpr: ∀L,T1,T2. L ⊢ T1 ➡ T2 → ⦃L, T1⦄ ➡ ⦃L, T2⦄. /2 width=4/ qed. -(* Advanced propertis *******************************************************) +(* Advanced properties ******************************************************) 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⦄. @@ -31,6 +31,14 @@ qed. (* Advanced forward lemmas **************************************************) +lemma fpr_fwd_bind2_minus: ∀I,L1,L,V1,T1,T. ⦃L1, -ⓑ{I}V1.T1⦄ ➡ ⦃L, T⦄ → ∀b. + ∃∃V2,T2. ⦃L1, ⓑ{b,I}V1.T1⦄ ➡ ⦃L, ⓑ{b,I}V2.T2⦄ & + T = -ⓑ{I}V2.T2. +#I #L1 #L #V1 #T1 #T #H1 #b +elim (fpr_inv_all … H1) -H1 #L0 #HL10 #HT1 #HL0 +elim (cpr_fwd_bind1_minus … HT1 b) -HT1 /3 width=4/ +qed-. + 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. @@ -49,7 +57,7 @@ qed-. 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⦄ & + ⦃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 @@ -58,9 +66,20 @@ 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⦄ & + ⦃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-. + +(* More advanced forward lemmas *********************************************) + +lemma fpr_fwd_pair1_full: ∀I,K1,L2,V1,T1,T2. ⦃K1.ⓑ{I}V1, T1⦄ ➡ ⦃L2, T2⦄ → + ∀b. ∃∃K2,V2. ⦃K1, V1⦄ ➡ ⦃K2, V2⦄ & + ⦃K1, ⓑ{b,I}V1.T1⦄ ➡ ⦃K2, ⓑ{b,I}V2.T2⦄ & + L2 = K2.ⓑ{I}V2. +#I #K1 #L2 #V1 #T1 #T2 #H #b +elim (fpr_inv_pair1 … H) -H #K2 #V2 #HV12 #HT12 #H destruct +elim (fpr_fwd_bind2_minus … HT12 b) -HT12 #W1 #U1 #HTU1 #H destruct /2 width=5/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr.ma index 5e1ba7992..44745490e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr.ma @@ -34,6 +34,9 @@ lemma lfpr_refl: ∀L. ⦃L⦄ ➡ ⦃L⦄. lemma ltpss_sn_lfpr: ∀L1,L2,d,e. L1 ⊢ ▶* [d, e] L2 → ⦃L1⦄ ➡ ⦃L2⦄. /3 width=5/ qed. +lemma ltpr_lfpr: ∀L1,L2. L1 ➡ L2 → ⦃L1⦄ ➡ ⦃L2⦄. +/3 width=3/ qed. + (* Basic inversion lemmas ***************************************************) lemma lfpr_inv_atom1: ∀L2. ⦃⋆⦄ ➡ ⦃L2⦄ → L2 = ⋆. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_cpr.ma index 4ce12bcc6..04686f960 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_cpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_cpr.ma @@ -18,7 +18,7 @@ include "basic_2/reducibility/lfpr.ma". (* FOCALIZED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS **********************) -(* Advanced properties ****************************************************) +(* Advanced properties ******************************************************) lemma lfpr_pair_cpr: ∀L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀V1,V2. L2 ⊢ V1 ➡ V2 → ∀I. ⦃L1. ⓑ{I} V1⦄ ➡ ⦃L2. ⓑ{I} V2⦄. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_fpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_fpr.ma index 9a226be58..9dc995fc7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_fpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_fpr.ma @@ -17,7 +17,7 @@ include "basic_2/reducibility/cfpr_cpr.ma". (* FOCALIZED PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ***********************) -(* Inversion lemmas on context-free parallel reduction for closures *********) +(* Properties 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 diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr.ma index 957b5f3a8..280410b80 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr.ma @@ -205,6 +205,15 @@ lemma tpr_inv_lref2: ∀T1,i. T1 ➡ #i → (* Basic forward lemmas *****************************************************) +lemma tpr_fwd_bind1_minus: ∀I,V1,T1,T. -ⓑ{I}V1.T1 ➡ T → ∀b. + ∃∃V2,T2. ⓑ{b,I}V1.T1 ➡ ⓑ{b,I}V2.T2 & + T = -ⓑ{I}V2.T2. +#I #V1 #T1 #T #H #b elim (tpr_inv_bind1 … H) -H * +[ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct /3 width=4/ +| #T2 #_ #_ #H destruct +] +qed-. + lemma tpr_fwd_shift1: ∀L1,T1,T. L1 @@ T1 ➡ T → ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2. #L1 @(lenv_ind_dx … L1) -L1 normalize -- 2.39.2