From: Ferruccio Guidi Date: Mon, 11 Feb 2013 22:56:54 +0000 (+0000) Subject: more service lemmas in nat and lambdadelta X-Git-Tag: make_still_working~1260 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=18df696e2c97546e5d42e86d18691b8546339160;p=helm.git more service lemmas in nat and lambdadelta --- 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 0370df1f8..ef2915cea 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fprs_cprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fprs_cprs.ma @@ -29,6 +29,20 @@ lemma fprs_bind2_minus: ∀I,L1,L2,V1,T1,U2. ⦃L1, -ⓑ{I}V1.T1⦄ ➡* ⦃L2, elim (fpr_bind2_minus … HU2) -HU2 /3 width=4/ qed-. +lemma fprs_lift: ∀K1,K2,T1,T2. ⦃K1, T1⦄ ➡* ⦃K2, T2⦄ → + ∀d,e,L1. ⇩[d, e] L1 ≡ K1 → + ∀U1,U2. ⇧[d, e] T1 ≡ U1 → ⇧[d, e] T2 ≡ U2 → + ∃∃L2. ⦃L1, U1⦄ ➡* ⦃L2, U2⦄ & ⇩[d, e] L2 ≡ K2. +#K1 #K2 #T1 #T2 #HT12 @(fprs_ind … HT12) -K2 -T2 +[ #d #e #L1 #HLK1 #U1 #U2 #HTU1 #HTU2 + >(lift_mono … HTU2 … HTU1) -U2 /2 width=3/ +| #K #K2 #T #T2 #_ #HT2 #IHT1 #d #e #L1 #HLK1 #U1 #U2 #HTU1 #HTU2 + elim (lift_total T d e) #U #HTU + elim (IHT1 … HLK1 … HTU1 HTU) -K1 -T1 #L #HU1 #HKL + elim (fpr_lift … HT2 … HKL … HTU HTU2) -K -T -T2 /3 width=4/ +] +qed-. + (* Advanced inversion lemmas ************************************************) lemma fprs_inv_pair1: ∀I,K1,L2,V1,T1,T2. ⦃K1.ⓑ{I}V1, T1⦄ ➡* ⦃L2, T2⦄ → 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 ace4e08d2..aa6795a12 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma @@ -12,17 +12,14 @@ (* *) (**************************************************************************) - -include "basic_2/reducibility/ltpr.ma". +include "basic_2/static/ssta_ltpss_dx.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_cpcs.ma". -include "basic_2/equivalence/fpcs_fpcs.ma". +include "basic_2/equivalence/lfpcs_fpcs.ma". include "basic_2/dynamic/snv_ssta.ma". (* -include "basic_2/static/ssta_ltpss_dx.ma". -include "basic_2/dynamic/snv_lift.ma". +anclude "basic_2/dynamic/snv_lift.ma". *) (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) @@ -48,10 +45,51 @@ fact ssta_ltpr_tpr_aux: ∀h,g,n. ( ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → ⦃h, L1⦄ ⊩ T1 :[g] → ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄. #h #g #n #IH3 #IH2 #IH1 #L1 * * [|||| *] -[ -| -| -| +[ #k #_ #Y #l #H1 #L2 #HL12 #X #H2 #_ -IH3 -IH1 + elim (ssta_inv_sort1 … H1) -H1 #Hkl #H destruct + >(tpr_inv_atom1 … H2) -X /4 width=6/ +| #i #Hn #U1 #l #H1 #L2 #HL12 #X #H2 #H3 destruct -IH3 + elim (ssta_inv_lref1 … H1) -H1 * #K1 + >(tpr_inv_atom1 … H2) -X + elim (snv_inv_lref … H3) -H3 #I0 #K0 #V0 #H #HV1 + [ #V1 #W1 #HLK1 #HVW1 #HWU1 + lapply (ldrop_mono … H … HLK1) -H #H destruct + lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKV1 + elim (ltpr_ldrop_conf … HLK1 … HL12) #X #H #HLK2 + elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct + elim (IH1 … HVW1 K2 … HV12) -IH1 -HVW1 -HV12 // -HV1 -HKV1 #W2 #HVW2 #HW12 + lapply (ldrop_fwd_ldrop2 … HLK1) -V1 #H1 + lapply (ldrop_fwd_ldrop2 … HLK2) #H2 + elim (lift_total W2 0 (i+1)) #U2 #HWU2 + lapply (fpcs_lift … HW12 … H1 H2 … HWU1 … HWU2) -H1 -H2 -W1 [ /3 width=1/ ] /3 width=6/ + | #V1 #W1 #l0 #HLK1 #HVW1 #HVU1 #H destruct + lapply (ldrop_mono … H … HLK1) -H #H destruct + lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKV1 + elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 #X #H #HLK2 + elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct + elim (IH1 … HVW1 K2 … HV12) -IH1 -HVW1 // -HV1 -HK12 -HKV1 #W2 #HVW2 #_ -W1 + elim (lift_total V2 0 (i+1)) #U2 #HVU2 + lapply (tpr_lift … HV12 … HVU1 … HVU2) -V1 /4 width=6/ + ] +| #p #Hn #U1 #l #H1 -IH3 -IH1 + elim (ssta_inv_gref1 … H1) +| #a #I #V1 #T1 #Hn #Y #l #H1 #L2 #HL12 #X #H2 #H3 destruct -IH3 + elim (ssta_inv_bind1 … H1) -H1 #U1 #HTU1 #H destruct + elim (snv_inv_bind … H3) -H3 #_ #HT1 + elim (tpr_inv_bind1 … H2) -H2 * + [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct + elim (IH1 … HTU1 (L2.ⓑ{I}V2) … HT10) -IH1 -HTU1 -HT10 // -T1 /3 width=1/ #U0 #HTU0 #HU10 + lapply (tps_lsubs_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 [ /2 width=1/ ] #HT02 + elim (ssta_tps_conf … HTU0 … HT02) -T0 #U2 #HTU2 #HU02 + lapply (cpr_intro … U0 … HU02) -HU02 // #HU02 + lapply (fpcs_fpr_strap1 … HU10 (L2.ⓑ{I}V2) U2 ?) [ /2 width=1/ ] -U0 #HU12 + lapply (fpcs_fwd_shift … HU12 a) -HU12 /3 width=3/ + | #T2 #HT12 #HT2 #H1 #H2 destruct + elim (IH1 … HTU1 (L2.ⓓV1) … HT12) -IH1 -HTU1 -HT12 // -T1 [2: /3 width=1/ ] #U2 #HTU2 #HU12 + lapply (fpcs_fwd_shift … HU12 true) -HU12 #HU12 + elim (ssta_inv_lift1 … HTU2 … HT2) -T2 [3: /2 width=1/ |2: skip ] #U #HXU #HU2 + lapply (fpcs_fpr_strap1 … HU12 L2 U ?) -HU12 [ /3 width=3/ ] -U2 /2 width=3/ + ] | #V1 #T1 #Hn #Y #l #H1 #L2 #HL12 #X #H2 #H3 destruct elim (ssta_inv_appl1 … H1) -H1 #U1 #HTU1 #H destruct elim (snv_inv_appl … H3) -H3 #a #W1 #W10 #U10 #l0 #HV1 #HT1 #HVW1 #HW10 #HTU10 diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs_fpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs_fpcs.ma new file mode 100644 index 000000000..8f3688890 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs_fpcs.ma @@ -0,0 +1,52 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/computation/fprs_cprs.ma". +include "basic_2/computation/lfprs_fprs.ma". +include "basic_2/equivalence/fpcs_fpcs.ma". +include "basic_2/equivalence/lfpcs_lfpcs.ma". + +(* FOCALIZED PARALLEL EQUIVALENCE ON LOCAL ENVIRONMENTS *********************) + +(* Inversion lemmas on context-free parallel equivalence for closures *******) + +lemma lfpcs_inv_fpcs: ∀L1,L2. ⦃L1⦄ ⬌* ⦃L2⦄ → ∀T. ⦃L1, T⦄ ⬌* ⦃L2, T⦄. +#L1 #L2 #HL12 #T +elim (lfpcs_inv_lfprs … HL12) -HL12 #L #HL1 #HL2 +lapply (lfprs_inv_fprs … HL1 T) -HL1 +lapply (lfprs_inv_fprs … HL2 T) -HL2 /2 width=4/ +qed-. + +(* Properties on context-free parallel equivalence for closures *************) + +lemma fpcs_lfpcs: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +#L1 #L2 #T1 #T2 #HT12 +elim (fpcs_inv_fprs … HT12) -HT12 /3 width=5 by fprs_lfprs, lfprs_div/ (**) (* auto too slow without trace *) +qed. + +lemma fpcs_lift: ∀K1,K2,T1,T2. ⦃K1, T1⦄ ⬌* ⦃K2, T2⦄ → + ∀L1,L2. ⦃L1⦄ ⬌* ⦃L2⦄ → + ∀d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 → + ∀U1,U2. ⇧[d, e] T1 ≡ U1 → ⇧[d, e] T2 ≡ U2 → + ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄. +#K1 #K2 #T1 #T2 #HT12 #L1 #L2 #HL12 #d #e #HLK1 #HLK2 #U1 #U2 #HTU1 #HTU2 +elim (fpcs_inv_fprs … HT12) -HT12 #K #T #HT1 #HT2 +elim (lift_total T d e) #U #HTU +elim (fprs_lift … HT1 … HLK1 … HTU1 HTU) -K1 -T1 #K1 #HU1 #_ +elim (fprs_lift … HT2 … HLK2 … HTU2 HTU) -K2 -T2 -T #K2 #HU2 #_ -K -d -e +lapply (lfpcs_lfprs_conf K1 … HL12) -HL12 /2 width=3/ #H +lapply (lfpcs_lfprs_strap1 … H K2 ?) -H /2 width=3/ #HK12 +lapply (lfpcs_inv_fpcs … HK12 U) -HK12 #HU +/3 width=4 by fpcs_fprs_strap2, fpcs_fprs_div/ +qed. 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 95aef01d4..a6f57bbf9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr_cpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr_cpr.ma @@ -18,9 +18,27 @@ include "basic_2/reducibility/cfpr_cpr.ma". (* Properties on context-sensitive parallel reduction for terms *************) +lemma ltpr_tpr_fpr: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. T1 ➡ T2 → ⦃L1, T1⦄ ➡ ⦃L2, T2⦄. +/3 width=4/ qed. + lemma cpr_fpr: ∀L,T1,T2. L ⊢ T1 ➡ T2 → ⦃L, T1⦄ ➡ ⦃L, T2⦄. /2 width=4/ qed. +lemma fpr_lift: ∀K1,K2,T1,T2. ⦃K1, T1⦄ ➡ ⦃K2, T2⦄ → + ∀d,e,L1. ⇩[d, e] L1 ≡ K1 → + ∀U1,U2. ⇧[d, e] T1 ≡ U1 → ⇧[d, e] T2 ≡ U2 → + ∃∃L2. ⦃L1, U1⦄ ➡ ⦃L2, U2⦄ & ⇩[d, e] L2 ≡ K2. +#K1 #K2 #T1 #T2 #HT12 #d #e #L1 #HLK1 #U1 #U2 #HTU1 #HTU2 +elim (fpr_inv_all … HT12) -HT12 #K #HK1 #HT12 #HK2 +elim (ldrop_ltpr_trans … HLK1 … HK1) -K1 #L #HL1 #HLK +lapply (cpr_lift … HLK … HTU1 … HTU2 HT12) -T1 -T2 #HU12 +elim (le_or_ge (|K|) d) #Hd +[ elim (ldrop_ltpss_sn_trans_ge … HLK … HK2 …) +| elim (ldrop_ltpss_sn_trans_be … HLK … HK2 …) +] // -Hd #L2 #HL2 #HLK2 +lapply (ltpss_sn_weak_all … HL2) -K /3 width=4/ +qed-. + (* Advanced properties ******************************************************) lemma fpr_bind_sn: ∀L1,L2,V1,V2. ⦃L1, V1⦄ ➡ ⦃L2, V2⦄ → ∀T1,T2. T1 ➡ T2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma index 3cd0134bb..7ffa93cb4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma @@ -79,6 +79,19 @@ lemma ssta_inv_lref1: ∀h,g,L,U,i,l. ⦃h, L⦄ ⊢ #i •[g, l] U → ). /2 width=3/ qed-. +fact ssta_inv_gref1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → ∀p0. T = §p0 → ⊥. +#h #g #L #T #U #l * -L -T -U -l +[ #L #k #l #_ #p0 #H destruct +| #L #K #V #W #U #i #l #_ #_ #_ #p0 #H destruct +| #L #K #W #V #U #i #l #_ #_ #_ #p0 #H destruct +| #a #I #L #V #T #U #l #_ #p0 #H destruct +| #L #V #T #U #l #_ #p0 #H destruct +| #L #W #T #U #l #_ #p0 #H destruct +qed. + +lemma ssta_inv_gref1: ∀h,g,L,U,p,l. ⦃h, L⦄ ⊢ §p •[g, l] U → ⊥. +/2 width=9/ qed-. + fact ssta_inv_bind1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → ∀a,I,X,Y. T = ⓑ{a,I}Y.X → ∃∃Z. ⦃h, L.ⓑ{I}Y⦄ ⊢ X •[g, l] Z & U = ⓑ{a,I}Y.Z. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ldrop.ma index d92978daf..dda41e4c3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ldrop.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "basic_2/unfold/tpss_lift.ma". include "basic_2/unfold/ltpss_sn.ma". (* SN PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************) @@ -129,3 +130,60 @@ lemma ltpss_sn_ldrop_trans_le: ∀L1,L0,d1,e1. L1 ⊢ ▶* [d1, e1] L0 → ] ] qed. + +lemma ldrop_ltpss_sn_trans_be: ∀L1,K1,d1,e1. ⇩[d1, e1] L1 ≡ K1 → + ∀K2,d2,e2. K1 ⊢ ▶* [d2, e2] K2 → + d2 ≤ d1 → d1 ≤ d2 + e2 → + ∃∃L2. L1 ⊢ ▶* [d2, e1 + e2] L2 & + ⇩[d1, e1] L2 ≡ K2. +#L1 #K1 #d1 #e1 #H elim H -L1 -K1 -d1 -e1 +[ #d1 #e1 #K2 #d2 #e2 #H #_ #_ + >(ltpss_sn_inv_atom1 … H) -H /2 width=3/ +| #K1 #I #V1 #K2 #d2 #e2 #HK12 #H #_ + lapply (le_n_O_to_eq … H) -H #H destruct /2 width=3/ +| #L1 #K1 #I #V #e1 #_ #IHLK1 #K2 #d2 #e2 #HK12 #H1 #H2 + elim (IHLK1 … HK12 H1 H2) -K1 -H2 + lapply (le_n_O_to_eq … H1) -H1 #H destruct /3 width=5/ +| #L1 #K1 #I #V1 #W1 #d1 #e1 #HLK1 #HWV1 #IHLK1 #X #d2 #e2 #H #Hd21 #Hd12 + elim (eq_or_gt d2) #Hd2 [ -Hd21 elim (eq_or_gt e2) #He2 ] destruct + [ lapply (le_n_O_to_eq … Hd12) -Hd12 plus_minus_commutative // #L2 #HL12 #HLK2 + elim (lift_total W2 d1 e1) #V2 #HWV2 + lapply (tpss_lift_be … HW12 … HLK1 HWV1 … HWV2) -HLK1 -W1 // /2 width=1/ + >plus_minus // >commutative_plus /4 width=5/ + | elim (ltpss_sn_inv_tpss11 … H Hd2) -H #K2 #W2 #HK12 #HW12 #H destruct + elim (IHLK1 … HK12 …) -IHLK1 [2: >plus_minus // ] /2 width=1/ #L2 #HL12 #HLK2 + elim (lift_total W2 d1 e1) #V2 #HWV2 + lapply (tpss_lift_be … HW12 … HLK1 HWV1 … HWV2) -HLK1 -W1 [ >plus_minus // ] /2 width=1/ + >commutative_plus /3 width=5/ + ] +] +qed-. + +lemma ldrop_ltpss_sn_trans_ge: ∀L1,K1,d1,e1. ⇩[d1, e1] L1 ≡ K1 → + ∀K2,d2,e2. K1 ⊢ ▶* [d2, e2] K2 → d2 + e2 ≤ d1 → + ∃∃L2. L1 ⊢ ▶* [d2, e2] L2 & ⇩[d1, e1] L2 ≡ K2. +#L1 #K1 #d1 #e1 #H elim H -L1 -K1 -d1 -e1 +[ #d1 #e1 #K2 #d2 #e2 #H #_ + >(ltpss_sn_inv_atom1 … H) -H /2 width=3/ +| #K1 #I #V1 #K2 #d2 #e2 #HK12 #H + elim (plus_le_0 … H) -H #H1 #H2 destruct /2 width=3/ +| #L1 #K1 #I #V #e1 #_ #IHLK1 #K2 #d2 #e2 #HK12 #H + elim (IHLK1 … HK12 H) -K1 + elim (plus_le_0 … H) -H #H1 #H2 destruct #L2 #HL12 + >(ltpss_sn_inv_refl_O2 … HL12) -L1 /3 width=5/ +| #L1 #K1 #I #V1 #W1 #d1 #e1 #HLK1 #HWV1 #IHLK1 #X #d2 #e2 #H #Hd21 + elim (eq_or_gt d2) #Hd2 [ elim (eq_or_gt e2) #He2 ] destruct + [ -IHLK1 -Hd21 <(ltpss_sn_inv_refl_O2 … H) -X /3 width=5/ + | elim (ltpss_sn_inv_tpss21 … H He2) -H #K2 #W2 #HK12 #HW12 #H destruct + elim (IHLK1 … HK12 …) -IHLK1 /2 width=1/ #L2 #HL12 #HLK2 + elim (lift_total W2 d1 e1) #V2 #HWV2 + lapply (tpss_lift_le … HW12 … HLK1 HWV1 … HWV2) -HLK1 -W1 /2 width=1/ /3 width=5/ + | elim (ltpss_sn_inv_tpss11 … H Hd2) -H #K2 #W2 #HK12 #HW12 #H destruct + elim (IHLK1 … HK12 …) -IHLK1 [2: >plus_minus // /2 width=1/ ] #L2 #HL12 #HLK2 + elim (lift_total W2 d1 e1) #V2 #HWV2 + lapply (tpss_lift_le … HW12 … HLK1 HWV1 … HWV2) -HLK1 -W1 [ >plus_minus // /2 width=1/ ] /3 width=5/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_tpss.ma index 0708932e4..d23c1a255 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_tpss.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_tpss.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "basic_2/unfold/tpss_lift.ma". include "basic_2/unfold/ltpss_sn_tps.ma". (* SN PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/thin_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/thin_ldrop.ma index 498660e1c..f26c26f01 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/thin_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/thin_ldrop.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "basic_2/substitution/ldrop_ldrop.ma". include "basic_2/unfold/ltpss_sn_ldrop.ma". include "basic_2/unfold/thin.ma". diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma index c707c3207..7bd51c318 100644 --- a/matita/matita/lib/arithmetics/nat.ma +++ b/matita/matita/lib/arithmetics/nat.ma @@ -686,6 +686,10 @@ lapply (minus_le x y)