From 913512bbc9202f2109d53acd43dc8c0270b17184 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 25 Apr 2012 15:54:27 +0000 Subject: [PATCH] - lambda_delta: bug fix in static type assignment some theorems on delift and thin - nat: eliminator for nat with "+1" rather than "S" --- .../lambda_delta/apps_2/functional/subst.ma | 14 +-- .../lambda_delta/basic_2/dynamic/nta.ma | 4 +- .../lambda_delta/basic_2/dynamic/nta_lift.ma | 27 +++-- .../lambda_delta/basic_2/dynamic/nta_sta.ma | 47 ++++++++ .../basic_2/equivalence/cpcs_cpcs.ma | 4 + .../contribs/lambda_delta/basic_2/notation.ma | 8 ++ .../basic_2/reducibility/ltpr_aaa.ma | 2 +- .../lambda_delta/basic_2/static/sta.ma | 18 ++-- .../lambda_delta/basic_2/static/sta_lift.ma | 14 ++- .../lambda_delta/basic_2/static/sta_sta.ma | 4 +- .../basic_2/substitution/ldrop.ma | 11 +- .../basic_2/substitution/lift_lift.ma | 9 ++ .../lambda_delta/basic_2/unfold/delift.ma | 27 +++-- .../lambda_delta/basic_2/unfold/delift_alt.ma | 100 ++++++++++++++++++ .../basic_2/unfold/delift_delift.ma | 29 +++++ .../basic_2/unfold/delift_lift.ma | 35 +++++- .../lambda_delta/basic_2/unfold/thin.ma | 25 +++++ .../basic_2/unfold/thin_delift.ma | 48 +++++++++ .../lambda_delta/ground_2/xoa.conf.xml | 1 + .../contribs/lambda_delta/ground_2/xoa.ma | 8 ++ .../lambda_delta/ground_2/xoa_notation.ma | 10 ++ matita/matita/lib/arithmetics/nat.ma | 4 + 22 files changed, 395 insertions(+), 54 deletions(-) create mode 100644 matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_sta.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/unfold/delift_delift.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/unfold/thin.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/unfold/thin_delift.ma diff --git a/matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma b/matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma index bbeeb10f4..e8ba1c2f2 100644 --- a/matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma +++ b/matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma @@ -52,21 +52,21 @@ theorem fsubst_inv_delift: ∀K,V,T1,L,T2,d. ⇩[0, d] L ≡ K. ⓓV → L ⊢ T1 [d, 1] ≡ T2 → [d ← V] T1 = T2. #K #V #T1 elim T1 -T1 [ * #i #L #T2 #d #HLK #H - [ -HLK >(delift_fwd_sort1 … H) -H // + [ -HLK >(delift_inv_sort1 … H) -H // | elim (lt_or_eq_or_gt i d) #Hid normalize - [ -HLK >(delift_fwd_lref1_lt … H) -H // /2 width=1/ + [ -HLK >(delift_inv_lref1_lt … H) -H // /2 width=1/ | destruct - elim (delift_fwd_lref1_be … H ? ?) -H // #K0 #V0 #V2 #HLK0 + elim (delift_inv_lref1_be … H ? ?) -H // #K0 #V0 #V2 #HLK0 lapply (ldrop_mono … HLK0 … HLK) -HLK0 -HLK #H >minus_plus (delift_inv_refl_O2 … HV2) -V >(flift_inv_lift … HVT2) -V2 // - | -HLK >(delift_fwd_lref1_ge … H) -H // /2 width=1/ + | -HLK >(delift_inv_lref1_ge … H) -H // /2 width=1/ ] - | -HLK >(delift_fwd_gref1 … H) -H // + | -HLK >(delift_inv_gref1 … H) -H // ] | * #I #V1 #T1 #IHV1 #IHT1 #L #X #d #HLK #H - [ elim (delift_fwd_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct + [ elim (delift_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct <(IHV1 … HV12) -IHV1 -HV12 // <(IHT1 … HT12) -IHT1 -HT12 // /2 width=1/ - | elim (delift_fwd_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct + | elim (delift_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct <(IHV1 … HV12) -IHV1 -HV12 // <(IHT1 … HT12) -IHT1 -HT12 // ] ] diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta.ma index 99592cdd9..9f42e7fca 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta.ma @@ -25,8 +25,8 @@ inductive nta (h:sh): lenv → relation term ≝ ⇧[0, i + 1] W ≡ U → nta h L (#i) U | nta_bind: ∀I,L,V,W,T,U. nta h L V W → nta h (L. ⓑ{I} V) T U → nta h L (ⓑ{I}V.T) (ⓑ{I}V.U) -| nta_appl: ∀L,V,W,U,T1,T2. nta h L V W → nta h L W U → nta h (L.ⓛW) T1 T2 → - nta h L (ⓐV.ⓛW.T1) (ⓐV.ⓛW.T2) +| nta_appl: ∀L,V,W,T,U. nta h L V W → nta h L (ⓛW.T) (ⓛW.U) → + nta h L (ⓐV.ⓛW.T) (ⓐV.ⓛW.U) | nta_pure: ∀L,V,W,T,U. nta h L T U → nta h L (ⓐV.U) W → nta h L (ⓐV.T) (ⓐV.U) | nta_cast: ∀L,T,U. nta h L T U → nta h L (ⓣU. T) U diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_lift.ma index a0ece8cbf..1bdb9b1ac 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_lift.ma @@ -26,7 +26,7 @@ fact nta_inv_sort1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀k0. T = ⋆k0 | #L #K #V #W #U #i #_ #_ #_ #_ #k0 #H destruct | #L #K #W #V #U #i #_ #_ #_ #_ #k0 #H destruct | #I #L #V #W #T #U #_ #_ #_ #_ #k0 #H destruct -| #L #V #W #U #T1 #T2 #_ #_ #_ #_ #_ #_ #k0 #H destruct +| #L #V #W #T #U #_ #_ #_ #_ #k0 #H destruct | #L #V #W #T #U #_ #_ #_ #_ #k0 #H destruct | #L #T #U #_ #_ #k0 #H destruct | #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #k0 #H destruct @@ -51,7 +51,7 @@ fact nta_inv_lref1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀j. T = #j → | #L #K #V #W #U #i #HLK #HVW #HWU #_ #j #H destruct /3 width=8/ | #L #K #W #V #U #i #HLK #HWV #HWU #_ #j #H destruct /3 width=8/ | #I #L #V #W #T #U #_ #_ #_ #_ #j #H destruct -| #L #V #W #U #T1 #T2 #_ #_ #_ #_ #_ #_ #j #H destruct +| #L #V #W #T #U #_ #_ #_ #_ #j #H destruct | #L #V #W #T #U #_ #_ #_ #_ #j #H destruct | #L #T #U #_ #_ #j #H destruct | #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #j #H destruct @@ -78,7 +78,7 @@ fact nta_inv_bind1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀J,X,Y. T = ⓑ{J | #L #K #V #W #U #i #_ #_ #_ #_ #J #X #Y #H destruct | #L #K #W #V #U #i #_ #_ #_ #_ #J #X #Y #H destruct | #I #L #V #W #T #U #HVW #HTU #_ #_ #J #X #Y #H destruct /2 width=3/ -| #L #V #W #U #T1 #T2 #_ #_ #_ #_ #_ #_ #J #X #Y #H destruct +| #L #V #W #T #U #_ #_ #_ #_ #J #X #Y #H destruct | #L #V #W #T #U #_ #_ #_ #_ #J #X #Y #H destruct | #L #T #U #_ #_ #J #X #Y #H destruct | #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #J #X #Y #H destruct @@ -100,7 +100,7 @@ fact nta_inv_cast1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. T = ⓣY.X | #L #K #V #W #U #i #_ #_ #_ #_ #X #Y #H destruct | #L #K #W #V #U #i #_ #_ #_ #_ #X #Y #H destruct | #I #L #V #W #T #U #_ #_ #_ #_ #X #Y #H destruct -| #L #V #W #U #T1 #T2 #_ #_ #_ #_ #_ #_ #X #Y #H destruct +| #L #V #W #T #U #_ #_ #_ #_ #X #Y #H destruct | #L #V #W #T #U #_ #_ #_ #_ #X #Y #H destruct | #L #T #U #HTU #_ #X #Y #H destruct /2 width=1/ | #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #X #Y #H destruct @@ -146,15 +146,13 @@ lemma nta_lift: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 : U1 → ∀L2,d,e. ⇩[d, e] elim (lift_inv_bind1 … H2) -H2 #X #U2 #H1 #HU12 #H2 destruct lapply (lift_mono … H1 … HV12) -H1 #H destruct elim (lift_total W1 d e) /4 width=6/ -| #L1 #V1 #W1 #U1 #T11 #T12 #_ #_ #_ #IHVW1 #IHWU1 #IHT112 #L2 #d #e #HL21 #X1 #H1 #X2 #H2 +| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2 elim (lift_inv_flat1 … H1) -H1 #V2 #X #HV12 #H1 #H destruct - elim (lift_inv_bind1 … H1) -H1 #W2 #T12 #HW12 #HT112 #H destruct - elim (lift_inv_flat1 … H2) -H2 #X0 #X #H0 #H2 #H destruct - elim (lift_inv_bind1 … H2) -H2 #Y0 #T22 #H2 #HT122 #H destruct - lapply (lift_mono … H0 … HV12) -H0 #H destruct - lapply (lift_mono … H2 … HW12) -H2 #H destruct - elim (lift_total U1 d e) #U2 #HU12 - @nta_appl [2,3: /2 width=5/ | skip | /3 width=5/ ] (**) (* explicit constructor, /4 width=6/ is too slow *) + elim (lift_inv_bind1 … H1) -H1 #W2 #T2 #HW12 #HT12 #H destruct + elim (lift_inv_flat1 … H2) -H2 #Y2 #X #HY #H2 #H destruct + elim (lift_inv_bind1 … H2) -H2 #X2 #U2 #HX #HU12 #H destruct + lapply (lift_mono … HY … HV12) -HY #H destruct + lapply (lift_mono … HX … HW12) -HX #H destruct /4 width=6/ | #L1 #V1 #W1 #T1 #U1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2 elim (lift_inv_flat1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H destruct elim (lift_inv_flat1 … H2) -H2 #X #U2 #H1 #HU12 #H2 destruct @@ -183,7 +181,8 @@ lemma nta_fwd_correct: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∃T0. ⦃h, L⦄ lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK elim (lift_total V 0 (i+1)) /3 width=10/ | #I #L #V #W #T #U #HVW #_ #_ * /3 width=2/ -| #L #V #W #U #T1 #T2 #HVW #HWU #_ #_ #_ * /3 width=2/ +| #L #V #W #T #U #HVW #_ #_ * #X #H + elim (nta_inv_bind1 … H) -H /4 width=2/ | #L #V #W #T #U #_ #HUW * #T0 #HUT0 /3 width=2/ | #L #T #U #_ * /2 width=2/ | /2 width=2/ @@ -197,5 +196,5 @@ lemma nta_appl_old: ∀h,L,V,W,T,U. ⦃h, L⦄ ⊢ V : W → ⦃h, L⦄ ⊢ T : ⦃h, L⦄ ⊢ ⓐV.T : ⓐV.ⓛW.U. #h #L #V #W #T #U #HVW #HTU elim (nta_fwd_correct … HTU) #X #H -elim (nta_inv_bind1 … H) -H #V0 #T0 #HWV0 #HUT0 #_ -X /3 width=2/ +elim (nta_inv_bind1 … H) -H /4 width=2/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_sta.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_sta.ma new file mode 100644 index 000000000..d064d2e7d --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_sta.ma @@ -0,0 +1,47 @@ +(**************************************************************************) +(* ___ *) +(* ||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/sta.ma". +include "basic_2/dynamic/nta_lift.ma". + +(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************) + +axiom pippo: ∀h,L,X,Y1,U. ⦃h, L⦄ ⊢ ⓐX.Y1 : U → ∀Y2. L ⊢ Y1 ⬌* Y2 → + ∀U2. ⦃h, L⦄ ⊢ Y2 : U2 → ⦃h, L⦄ ⊢ ⓐX.Y2 : U. + +(* Properties on static type assignment *************************************) + +lemma nta_fwd_sta: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → + ∃∃U0. ⦃h, L⦄ ⊢ T • U0 & L ⊢ U0 ⬌* U & ⦃h, L⦄ ⊢ T : U0. +#h #L #T #U #H elim H -L -T -U +[ /2 width=4/ +| #L #K #V #W1 #V1 #i #HLK #_ #HWV1 * #W0 #H1VW0 #HW01 #H2VW0 + elim (lift_total W0 0 (i+1)) #V0 #HWV0 + lapply (ldrop_fwd_ldrop2 … HLK) #HLK0 + lapply (cpcs_lift … HLK0 … HWV0 … HWV1 HW01) -HLK0 -HWV1 -HW01 /3 width=9/ +| #L #K #W #V1 #W1 #i #HLK #HWV1 #HW1 * /3 width=9/ +| #I #L #V #W #T #U #_ #_ * #W0 #_ #_ #H2VW0 * /3 width=4/ +| #L #V #W #T #U #_ #_ * #W0 #_ #HW0 #H2VW0 * #X #H1 #HX #H2 + elim (sta_inv_bind1 … H1) -H1 #U0 #HTU0 #H destruct + elim (nta_inv_bind1 … H2) /4 width=4/ +| #L #V #W #T #U #_ #_ * #U0 #H1TU0 #HU0 #H2TU0 * #W0 #_ #_ #H2UW0 -W + elim (nta_fwd_correct … H2TU0) #T0 #HUT0 + @(ex3_1_intro … (ⓐV.U0)) /2 width=1/ -H1TU0 + @(nta_pure … W0 … H2TU0) -T /3 width=3/ +| #L #T #U #HTU * #U0 #H1TU0 #HU0 #H2TU0 + elim (nta_fwd_correct … H2TU0) -H2TU0 /4 width=8/ +| #L #T #U1 #U2 #V2 #_ #HU12 #_ * #U0 #H1TU0 #HU01 #H2TU0 #_ + lapply (cpcs_trans … HU01 … HU12) -U1 /2 width=4/ +] +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma index 6054aaeb3..ddf9e7865 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma @@ -99,6 +99,10 @@ lemma cpcs_abbr_dx: ∀L,V,T1,T2. L.ⓓV ⊢ T1 ⬌* T2 → L ⊢ ⓓV. T1 ⬌* elim (cpcs_inv_cprs … HT12) -HT12 /3 width=5 by cprs_div, cprs_abbr1/ (**) (* /3 width=5/ is a bit slow *) qed. +lemma cpcs_bind_dx: ∀I,L,V,T1,T2. L.ⓑ{I}V ⊢ T1 ⬌* T2 → + L ⊢ ⓑ{I}V. T1 ⬌* ⓑ{I}V. T2. +* /2 width=1/ /2 width=2/ qed. + lemma cpcs_abbr_sn: ∀L,V1,V2,T. L ⊢ V1 ⬌* V2 → L ⊢ ⓓV1. T ⬌* ⓓV2. T. #L #V1 #V2 #T #HV12 elim (cpcs_inv_cprs … HV12) -HV12 /3 width=5 by cprs_div, cprs_abbr1/ (**) (* /3 width=5/ is a bit slow *) diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma index dc4bda396..9d0c9e34b 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/notation.ma @@ -192,6 +192,14 @@ notation "hvbox( L ⊢ break term 90 T1 break [ d , break e ] ≡ break T2 )" non associative with precedence 45 for @{ 'TSubst $L $T1 $d $e $T2 }. +notation "hvbox( T1 break [ d , break e ] ≡≡ break term 46 T2 )" + non associative with precedence 45 + for @{ 'TSubstAlt $T1 $d $e $T2 }. + +notation "hvbox( L ⊢ break term 90 T1 break [ d , break e ] ≡≡ break term 46 T2 )" + non associative with precedence 45 + for @{ 'TSubstAlt $L $T1 $d $e $T2 }. + (* Static typing ************************************************************) notation "hvbox( L ⊢ break term 90 T ÷ break A )" diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma index 5bf592294..31370c5e0 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma @@ -28,7 +28,7 @@ fact aaa_ltpr_tpr_conf_aux: ∀L,T,L1,T1,A. L1 ⊢ T1 ÷ A → L = L1 → T = T1 >(tpr_inv_atom1 … H) -H // | #I #L1 #K1 #V1 #B #i #HLK1 #HK1 #H1 #H2 #L2 #HL12 #T2 #H destruct >(tpr_inv_atom1 … H) -T2 - lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKV1 + lapply (ldrop_pair2_fwd_cw … HLK1 (#i)) #HKV1 elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #HLK2 #H elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct lapply (IH … HKV1 … HK1 … HK12 … HV12) // -L1 -K1 -V1 /2 width=5/ diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/sta.ma b/matita/matita/contribs/lambda_delta/basic_2/static/sta.ma index 93769e9f5..4c38a083b 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/static/sta.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/static/sta.ma @@ -27,7 +27,7 @@ inductive sta (h:sh): lenv → relation term ≝ sta h L (ⓑ{I}V.T) (ⓑ{I}V.U) | sta_appl: ∀L,V,T,U. sta h L T U → sta h L (ⓐV.T) (ⓐV.U) -| sta_cast: ∀L,T,U. sta h L T U → sta h L (ⓣU. T) U +| sta_cast: ∀L,W,T,U. sta h L T U → sta h L (ⓣW. T) U . interpretation "static type assignment (term)" @@ -43,7 +43,7 @@ fact sta_inv_sort1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T • U → ∀k0. T = ⋆k0 | #L #K #W #V #U #i #_ #_ #_ #k0 #H destruct | #I #L #V #T #U #_ #k0 #H destruct | #L #V #T #U #_ #k0 #H destruct -| #L #T #U #_ #k0 #H destruct +| #L #W #T #U #_ #k0 #H destruct qed. (* Basic_1: was: sty0_gen_sort *) @@ -63,7 +63,7 @@ fact sta_inv_lref1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T • U → ∀j. T = #j → | #L #K #W #V #U #i #HLK #HWV #HWU #j #H destruct /3 width=6/ | #I #L #V #T #U #_ #j #H destruct | #L #V #T #U #_ #j #H destruct -| #L #T #U #_ #j #H destruct +| #L #W #T #U #_ #j #H destruct ] qed. @@ -85,7 +85,7 @@ fact sta_inv_bind1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T • U → ∀J,X,Y. T = ⓑ | #L #K #W #V #U #i #_ #_ #_ #J #X #Y #H destruct | #I #L #V #T #U #HTU #J #X #Y #H destruct /2 width=3/ | #L #V #T #U #_ #J #X #Y #H destruct -| #L #T #U #_ #J #X #Y #H destruct +| #L #W #T #U #_ #J #X #Y #H destruct ] qed. @@ -102,7 +102,7 @@ fact sta_inv_appl1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T • U → ∀X,Y. T = ⓐY. | #L #K #W #V #U #i #_ #_ #_ #X #Y #H destruct | #I #L #V #T #U #_ #X #Y #H destruct | #L #V #T #U #HTU #X #Y #H destruct /2 width=3/ -| #L #T #U #_ #X #Y #H destruct +| #L #W #T #U #_ #X #Y #H destruct ] qed. @@ -112,17 +112,17 @@ lemma sta_inv_appl1: ∀h,L,Y,X,U. ⦃h, L⦄ ⊢ ⓐY.X • U → /2 width=3/ qed-. fact sta_inv_cast1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T • U → ∀X,Y. T = ⓣY.X → - ⦃h, L⦄ ⊢ X • Y ∧ U = Y. + ⦃h, L⦄ ⊢ X • U. #h #L #T #U * -L -T -U [ #L #k #X #Y #H destruct | #L #K #V #W #U #i #_ #_ #_ #X #Y #H destruct | #L #K #W #V #U #i #_ #_ #_ #X #Y #H destruct | #I #L #V #T #U #_ #X #Y #H destruct | #L #V #T #U #_ #X #Y #H destruct -| #L #T #U #HTU #X #Y #H destruct /2 width=1/ +| #L #W #T #U #HTU #X #Y #H destruct // ] qed. (* Basic_1: was: sty0_gen_cast *) -lemma sta_inv_cast1: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓣY.X • U → ⦃h, L⦄ ⊢ X • Y ∧ U = Y. -/2 width=3/ qed-. +lemma sta_inv_cast1: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓣY.X • U → ⦃h, L⦄ ⊢ X • U. +/2 width=4/ qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/sta_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/static/sta_lift.ma index 1c624e145..45465cbce 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/static/sta_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/static/sta_lift.ma @@ -53,9 +53,8 @@ lemma sta_lift: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 • U1 → ∀L2,d,e. ⇩[d, e elim (lift_inv_flat1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H destruct elim (lift_inv_flat1 … H2) -H2 #X #U2 #H1 #HU12 #H2 destruct lapply (lift_mono … H1 … HV12) -H1 #H destruct /4 width=5/ -| #L1 #T1 #U1 #_ #IHTU1 #L2 #d #e #HL21 #X #H #U2 #HU12 - elim (lift_inv_flat1 … H) -H #X2 #T2 #HUX2 #HT12 #H destruct - lapply (lift_mono … HUX2 … HU12) -HUX2 #H destruct /3 width=5/ +| #L1 #W1 #T1 #U1 #_ #IHTU1 #L2 #d #e #HL21 #X #H #U2 #HU12 + elim (lift_inv_flat1 … H) -H #W2 #T2 #_ #HT12 #H destruct /3 width=5/ ] qed. @@ -96,10 +95,9 @@ lemma sta_inv_lift: ∀h,L2,T2,U2. ⦃h, L2⦄ ⊢ T2 • U2 → ∀L1,d,e. ⇩[ | #L2 #V2 #T2 #U2 #_ #IHTU2 #L1 #d #e #HL21 #X #H elim (lift_inv_flat2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct elim (IHTU2 … HL21 … HT12) -L2 -HT12 /3 width=5/ -| #L2 #T2 #U2 #_ #IHTU2 #L1 #d #e #HL21 #X #H - elim (lift_inv_flat2 … H) -H #U1 #T1 #HU12 #HT12 #H destruct - elim (IHTU2 … HL21 … HT12) -L2 -HT12 #U0 #HTU0 #HU02 - lapply (lift_inj … HU02 … HU12) -HU02 #H destruct /3 width=3/ +| #L2 #W2 #T2 #U2 #_ #IHTU2 #L1 #d #e #HL21 #X #H + elim (lift_inv_flat2 … H) -H #W1 #T1 #_ #HT12 #H destruct + elim (IHTU2 … HL21 … HT12) -L2 -HT12 /3 width=3/ ] qed. @@ -117,6 +115,6 @@ lemma sta_fwd_correct: ∀h,L,T,U. ⦃h, L⦄ ⊢ T • U → ∃T0. ⦃h, L⦄ elim (lift_total V 0 (i+1)) /3 width=10/ | #I #L #V #T #U #_ * /3 width=2/ | #L #V #T #U #_ * #T0 #HUT0 /3 width=2/ -| #L #T #U #_ * /2 width=2/ +| #L #W #T #U #_ * /2 width=2/ ] qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/sta_sta.ma b/matita/matita/contribs/lambda_delta/basic_2/static/sta_sta.ma index cee17f8df..cfbb192fa 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/static/sta_sta.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/static/sta_sta.ma @@ -38,7 +38,7 @@ theorem sta_mono: ∀h,L,T,U1. ⦃h, L⦄ ⊢ T • U1 → elim (sta_inv_bind1 … H) -H #U2 #HTU2 #H destruct /3 width=1/ | #L #V #T #U1 #_ #IHTU1 #X #H elim (sta_inv_appl1 … H) -H #U2 #HTU2 #H destruct /3 width=1/ -| #L #T #U1 #_ #_ #U2 #H - elim (sta_inv_cast1 … H) -H // +| #L #W #T #U1 #_ #IHTU1 #U2 #H + lapply (sta_inv_cast1 … H) -H /2 width=1/ ] qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma index 4550fde4b..73a9ff92e 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma @@ -135,6 +135,15 @@ lemma ldrop_ldrop_lt: ∀L1,L2,I,V,e. #L1 #L2 #I #V #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/ qed. +lemma ldrop_O1: ∀L,i. i < |L| → ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V. +#L elim L -L +[ #i #H elim (lt_zero_false … H) +| #L #I #V #IHL #i @(nat_ind_plus … i) -i /2 width=4/ #i #_ #H + lapply (lt_plus_to_lt_l … H) -H #Hi + elim (IHL i ?) // /3 width=4/ +] +qed. + lemma ldrop_lsubs_ldrop1_abbr: ∀L1,L2,d,e. L1 [d, e] ≼ L2 → ∀K1,V,i. ⇩[0, i] L1 ≡ K1. ⓓV → d ≤ i → i < d + e → @@ -187,7 +196,7 @@ lemma ldrop_fwd_lw: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → #[L2] ≤ #[L1]. ] qed-. -lemma ldrop_pair2_fwd_fw: ∀I,L,K,V,d,e. ⇩[d, e] L ≡ K. ⓑ{I} V → +lemma ldrop_pair2_fwd_cw: ∀I,L,K,V,d,e. ⇩[d, e] L ≡ K. ⓑ{I} V → ∀T. #[K, V] < #[L, T]. #I #L #K #V #d #e #H #T lapply (ldrop_fwd_lw … H) -H #H diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift.ma index e70389973..727d486d4 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift.ma @@ -198,3 +198,12 @@ theorem lift_trans_ge: ∀d1,e1,T1,T. ⇧[d1, e1] T1 ≡ T → elim (IHT12 … HT20 ?) -IHT12 -HT20 // /3 width=5/ ] qed. + +(* Advanced properties ******************************************************) + +lemma lift_conf_le: ∀T,T1,d. ⇧[O, d] T ≡ T1 → ∀T2,e. ⇧[O, d + e] T ≡ T2 → + ⇧[d, e] T1 ≡ T2. +#T #T1 #d #HT1 #T2 #e #HT2 +elim (lift_split … HT2 d d ? ? ?) -HT2 // #X #H +>(lift_mono … H … HT1) -T // +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma index 851e3d996..7620ae092 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma @@ -24,11 +24,26 @@ interpretation "delift (term)" (* Basic properties *********************************************************) +lemma delift_refl_O2: ∀L,T,d. L ⊢ T [d, 0] ≡ T. +/2 width=3/ qed. + lemma delift_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≡ T2 → ∀L2. L1 [d, e] ≼ L2 → L2 ⊢ T1 [d, e] ≡ T2. #L1 #T1 #T2 #d #e * /3 width=3/ qed. +lemma delift_sort: ∀L,d,e,k. L ⊢ ⋆k [d, e] ≡ ⋆k. +/2 width=3/ qed. + +lemma delift_lref_lt: ∀L,d,e,i. i < d → L ⊢ #i [d, e] ≡ #i. +/3 width=3/ qed. + +lemma delift_lref_ge: ∀L,d,e,i. d + e ≤ i → L ⊢ #i [d, e] ≡ #(i - e). +/3 width=3/ qed. + +lemma delift_gref: ∀L,d,e,p. L ⊢ §p [d, e] ≡ §p. +/2 width=3/ qed. + lemma delift_bind: ∀I,L,V1,V2,T1,T2,d,e. L ⊢ V1 [d, e] ≡ V2 → L. ⓑ{I} V2 ⊢ T1 [d+1, e] ≡ T2 → L ⊢ ⓑ{I} V1. T1 [d, e] ≡ ⓑ{I} V2. T2. @@ -42,21 +57,21 @@ lemma delift_flat: ∀I,L,V1,V2,T1,T2,d,e. #I #L #V1 #V2 #T1 #T2 #d #e * #V #HV1 #HV2 * /3 width=5/ qed. -(* Basic forward lemmas *****************************************************) +(* Basic inversion lemmas ***************************************************) -lemma delift_fwd_sort1: ∀L,U2,d,e,k. L ⊢ ⋆k [d, e] ≡ U2 → U2 = ⋆k. +lemma delift_inv_sort1: ∀L,U2,d,e,k. L ⊢ ⋆k [d, e] ≡ U2 → U2 = ⋆k. #L #U2 #d #e #k * #U #HU >(tpss_inv_sort1 … HU) -HU #HU2 >(lift_inv_sort2 … HU2) -HU2 // qed-. -lemma delift_fwd_gref1: ∀L,U2,d,e,p. L ⊢ §p [d, e] ≡ U2 → U2 = §p. +lemma delift_inv_gref1: ∀L,U2,d,e,p. L ⊢ §p [d, e] ≡ U2 → U2 = §p. #L #U #d #e #p * #U #HU >(tpss_inv_gref1 … HU) -HU #HU2 >(lift_inv_gref2 … HU2) -HU2 // qed-. -lemma delift_fwd_bind1: ∀I,L,V1,T1,U2,d,e. L ⊢ ⓑ{I} V1. T1 [d, e] ≡ U2 → +lemma delift_inv_bind1: ∀I,L,V1,T1,U2,d,e. L ⊢ ⓑ{I} V1. T1 [d, e] ≡ U2 → ∃∃V2,T2. L ⊢ V1 [d, e] ≡ V2 & L. ⓑ{I} V2 ⊢ T1 [d+1, e] ≡ T2 & U2 = ⓑ{I} V2. T2. @@ -66,7 +81,7 @@ elim (lift_inv_bind2 … HU2) -HU2 #V2 #T2 #HV2 #HT2 lapply (tpss_lsubs_conf … HT1 (L. ⓑ{I} V2) ?) -HT1 /2 width=1/ /3 width=5/ qed-. -lemma delift_fwd_flat1: ∀I,L,V1,T1,U2,d,e. L ⊢ ⓕ{I} V1. T1 [d, e] ≡ U2 → +lemma delift_inv_flat1: ∀I,L,V1,T1,U2,d,e. L ⊢ ⓕ{I} V1. T1 [d, e] ≡ U2 → ∃∃V2,T2. L ⊢ V1 [d, e] ≡ V2 & L ⊢ T1 [d, e] ≡ T2 & U2 = ⓕ{I} V2. T2. @@ -75,8 +90,6 @@ elim (tpss_inv_flat1 … HU) -HU #V #T #HV1 #HT1 #X destruct elim (lift_inv_flat2 … HU2) -HU2 /3 width=5/ qed-. -(* Basic Inversion lemmas ***************************************************) - lemma delift_inv_refl_O2: ∀L,T1,T2,d. L ⊢ T1 [d, 0] ≡ T2 → T1 = T2. #L #T1 #T2 #d * #T #HT1 >(tpss_inv_refl_O2 … HT1) -HT1 #HT2 diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma new file mode 100644 index 000000000..c5fdcaadd --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma @@ -0,0 +1,100 @@ +(**************************************************************************) +(* ___ *) +(* ||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/delift_lift.ma". + +(* DELIFT ON TERMS **********************************************************) + +(* alternative definition of delift *) +inductive delifta: nat → nat → lenv → relation term ≝ +| delifta_sort : ∀L,d,e,k. delifta d e L (⋆k) (⋆k) +| delifta_lref_lt: ∀L,d,e,i. i < d → delifta d e L (#i) (#i) +| delifta_lref_be: ∀L,K,V1,V2,W2,i,d,e. d ≤ i → i < d + e → + ⇩[0, i] L ≡ K. ⓓV1 → delifta 0 (d + e - i - 1) K V1 V2 → + ⇧[0, d] V2 ≡ W2 → delifta d e L (#i) W2 +| delifta_lref_ge: ∀L,d,e,i. d + e ≤ i → delifta d e L (#i) (#(i - e)) +| delifta_gref : ∀L,d,e,p. delifta d e L (§p) (§p) +| delifta_bind : ∀L,I,V1,V2,T1,T2,d,e. + delifta d e L V1 V2 → delifta (d + 1) e (L. ⓑ{I} V2) T1 T2 → + delifta d e L (ⓑ{I} V1. T1) (ⓑ{I} V2. T2) +| delifta_flat : ∀L,I,V1,V2,T1,T2,d,e. + delifta d e L V1 V2 → delifta d e L T1 T2 → + delifta d e L (ⓕ{I} V1. T1) (ⓕ{I} V2. T2) +. + +interpretation "delift (term) alternative" + 'TSubstAlt L T1 d e T2 = (delifta d e L T1 T2). + +(* Basic properties *********************************************************) + +lemma delifta_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≡≡ T2 → + ∀L2. L1 [d, e] ≼ L2 → L2 ⊢ T1 [d, e] ≡≡ T2. +#L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e // /2 width=1/ +[ #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #_ #HVW2 #IHV12 #L2 #HL12 + elim (ldrop_lsubs_ldrop1_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/ +| /4 width=1/ +| /3 width=1/ +] +qed. + +lemma delift_delifta: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≡ T2 → L ⊢ T1 [d, e] ≡≡ T2. +#L #T1 @(cw_wf_ind … L T1) -L -T1 #L #T1 elim T1 -T1 +[ * #i #IH #T2 #d #e #H + [ >(delift_inv_sort1 … H) -H // + | elim (delift_inv_lref1 … H) -H * /2 width=1/ + #K #V1 #V2 #Hdi #Hide #HLK #HV12 #HVT2 + lapply (ldrop_pair2_fwd_cw … HLK) #H + lapply (IH … HV12) // -H /2 width=6/ + | >(delift_inv_gref1 … H) -H // + ] +| * #I #V1 #T1 #_ #_ #IH #X #d #e #H + [ elim (delift_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct + lapply (delift_lsubs_conf … HT12 (L.ⓑ{I}V1) ?) -HT12 /2 width=1/ #HT12 + lapply (IH … HV12) -HV12 // #HV12 + lapply (IH … HT12) -IH -HT12 /2 width=1/ #HT12 + lapply (delifta_lsubs_conf … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/ + | elim (delift_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct + lapply (IH … HV12) -HV12 // + lapply (IH … HT12) -IH -HT12 // /2 width=1/ + ] +] +qed. + +(* Basic inversion lemmas ***************************************************) + +lemma delifta_delift: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≡≡ T2 → L ⊢ T1 [d, e] ≡ T2. +#L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e // /2 width=1/ /2 width=6/ +qed-. + +lemma delift_ind_alt: ∀R:ℕ→ℕ→lenv→relation term. + (∀L,d,e,k. R d e L (⋆k) (⋆k)) → + (∀L,d,e,i. i < d → R d e L (#i) (#i)) → + (∀L,K,V1,V2,W2,i,d,e. d ≤ i → i < d + e → + ⇩[O, i] L ≡ K.ⓓV1 → K ⊢ V1 [O, d + e - i - 1] ≡ V2 → + ⇧[O, d] V2 ≡ W2 → R O (d+e-i-1) K V1 V2 → R d e L #i W2 + ) → + (∀L,d,e,i. d + e ≤ i → R d e L (#i) (#(i - e))) → + (∀L,d,e,p. R d e L (§p) (§p)) → + (∀L,I,V1,V2,T1,T2,d,e. L ⊢ V1 [d, e] ≡ V2 → + L.ⓑ{I}V2 ⊢ T1 [d + 1, e] ≡ T2 → R d e L V1 V2 → + R (d+1) e (L.ⓑ{I}V2) T1 T2 → R d e L (ⓑ{I}V1.T1) (ⓑ{I}V2.T2) + ) → + (∀L,I,V1,V2,T1,T2,d,e. L ⊢ V1 [d, e] ≡ V2 → + L⊢ T1 [d, e] ≡ T2 → R d e L V1 V2 → + R d e L T1 T2 → R d e L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2) + ) → + ∀d,e,L,T1,T2. L ⊢ T1 [d, e] ≡ T2 → R d e L T1 T2. +#R #H1 #H2 #H3 #H4 #H5 #H6 #H7 #d #e #L #T1 #T2 #H elim (delift_delifta … H) -L -T1 -T2 -d -e +// /2 width=1 by delifta_delift/ /3 width=1 by delifta_delift/ /3 width=7 by delifta_delift/ +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_delift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_delift.ma new file mode 100644 index 000000000..9ae9831c8 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_delift.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/tpss_tpss.ma". +include "basic_2/unfold/delift.ma". + +(* DELIFT ON TERMS **********************************************************) + +(* Main properties **********************************************************) + +theorem delift_mono: ∀L,T,T1,T2,d,e. + L ⊢ T [d, e] ≡ T1 → L ⊢ T [d, e] ≡ T2 → T1 = T2. +#L #T #T1 #T2 #d #e * #U1 #H1TU1 #H2TU1 * #U2 #H1TU2 #H2TU2 +elim (tpss_conf_eq … H1TU1 … H1TU2) -T #U #HU1 #HU2 +lapply (tpss_inv_lift1_eq … HU1 … H2TU1) -HU1 #H destruct +lapply (tpss_inv_lift1_eq … HU2 … H2TU2) -HU2 #H destruct +lapply (lift_inj … H2TU1 … H2TU2) // +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma index 5ae82271d..8266a9ae3 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma @@ -17,9 +17,20 @@ include "basic_2/unfold/delift.ma". (* DELIFT ON TERMS **********************************************************) +(* Advanced properties ******************************************************) + +lemma delift_lref_be: ∀L,K,V1,V2,U2,i,d,e. d ≤ i → i < d + e → + ⇩[0, i] L ≡ K. ⓓV1 → K ⊢ V1 [0, d + e - i - 1] ≡ V2 → + ⇧[0, d] V2 ≡ U2 → L ⊢ #i [d, e] ≡ U2. +#L #K #V1 #V2 #U2 #i #d #e #Hdi #Hide #HLK * #V #HV1 #HV2 #HVU2 +elim (lift_total V 0 (i+1)) #U #HVU +lapply (lift_trans_be … HV2 … HVU ? ?) -HV2 // >minus_plus (lift_inv_lref2_lt … HU2) // @@ -29,7 +40,7 @@ elim (tpss_inv_lref1 … HU) -HU ] qed-. -lemma delift_fwd_lref1_be: ∀L,U2,d,e,i. L ⊢ #i [d, e] ≡ U2 → +lemma delift_inv_lref1_be: ∀L,U2,d,e,i. L ⊢ #i [d, e] ≡ U2 → d ≤ i → i < d + e → ∃∃K,V1,V2. ⇩[0, i] L ≡ K. ⓓV1 & K ⊢ V1 [0, d + e - i - 1] ≡ V2 & @@ -42,7 +53,7 @@ elim (tpss_inv_lref1 … HU) -HU ] qed-. -lemma delift_fwd_lref1_ge: ∀L,U2,i,d,e. L ⊢ #i [d, e] ≡ U2 → +lemma delift_inv_lref1_ge: ∀L,U2,i,d,e. L ⊢ #i [d, e] ≡ U2 → d + e ≤ i → U2 = #(i - e). #L #U2 #i #d #e * #U #HU #HU2 #Hdei elim (tpss_inv_lref1 … HU) -HU @@ -52,3 +63,21 @@ elim (tpss_inv_lref1 … HU) -HU elim (lt_refl_false … Hi) ] qed-. + +lemma delift_inv_lref1: ∀L,U2,i,d,e. L ⊢ #i [d, e] ≡ U2 → + ∨∨ (i < d ∧ U2 = #i) + | (∃∃K,V1,V2. d ≤ i & i < d + e & + ⇩[0, i] L ≡ K. ⓓV1 & + K ⊢ V1 [0, d + e - i - 1] ≡ V2 & + ⇧[0, d] V2 ≡ U2 + ) + | (d + e ≤ i ∧ U2 = #(i - e)). +#L #U2 #i #d #e #H +elim (lt_or_ge i d) #Hdi +[ elim (delift_inv_lref1_lt … H Hdi) -H /3 width=1/ +| elim (lt_or_ge i (d+e)) #Hide + [ elim (delift_inv_lref1_be … H Hdi Hide) -H /3 width=6/ + | elim (delift_inv_lref1_ge … H Hide) -H /3 width=1/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/thin.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/thin.ma new file mode 100644 index 000000000..0b4da98f9 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/thin.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/unfold/ltpss.ma". + +(* DELIFT ON LOCAL ENVIRONMENTS ********************************************) + +definition thin: nat → nat → relation lenv ≝ + λd,e,L1,L2. ∃∃L. L1 [d, e] ▶* L & ⇩[d, e] L ≡ L2. + +interpretation "delift (local environment)" + 'TSubst L1 d e L2 = (thin d e L1 L2). + +(* Basic properties *********************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/thin_delift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/thin_delift.ma new file mode 100644 index 000000000..849826663 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/thin_delift.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/unfold/tpss_alt.ma". +include "basic_2/unfold/ltpss_ltpss.ma". +include "basic_2/unfold/delift_alt.ma". +include "basic_2/unfold/thin.ma". + +(* DELIFT ON LOCAL ENVIRONMENTS *********************************************) + +(* Properties on deflift on terms *******************************************) + +lemma thin_delift1: ∀L1,L2,d,e. L1 [d, e] ≡ L2 → ∀V1,V2. L1 ⊢ V1 [d, e] ≡ V2 → + ∀I. L1.ⓑ{I}V1 [d + 1, e] ≡ L2.ⓑ{I}V2. +#L1 #L2 #d #e * #L #HL1 #HL2 #V1 #V2 * #V #HV1 #HV2 #I +elim (ltpss_tpss_conf … HV1 … HL1) -HV1 #V0 #HV10 #HV0 +elim (tpss_inv_lift1_be … HV0 … HL2 … HV2 ? ?) -HV0 // (delift_inv_sort1 … H) -X /2 width=3/ + | elim (delift_inv_lref1 … H) -H * [1,3: /3 width=3/ | /3 width=6/ ] + | >(delift_inv_gref1 … H) -X /2 width=3/ + ] +| #L #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #_ #HVW2 #IHV12 #T1 #dd #ee #H #K2 #HLK2 #Hdd #Hddee + lapply + + @(ex2_1_intro … X) // /2 width=6/ +*) diff --git a/matita/matita/contribs/lambda_delta/ground_2/xoa.conf.xml b/matita/matita/contribs/lambda_delta/ground_2/xoa.conf.xml index d18d4192a..fff92a290 100644 --- a/matita/matita/contribs/lambda_delta/ground_2/xoa.conf.xml +++ b/matita/matita/contribs/lambda_delta/ground_2/xoa.conf.xml @@ -15,6 +15,7 @@ xoa_notation basics/pts.ma 1 2 + 1 3 2 1 2 2 2 3 diff --git a/matita/matita/contribs/lambda_delta/ground_2/xoa.ma b/matita/matita/contribs/lambda_delta/ground_2/xoa.ma index 5a3a40024..6fe0ca037 100644 --- a/matita/matita/contribs/lambda_delta/ground_2/xoa.ma +++ b/matita/matita/contribs/lambda_delta/ground_2/xoa.ma @@ -24,6 +24,14 @@ inductive ex1_2 (A0,A1:Type[0]) (P0:A0→A1→Prop) : Prop ≝ interpretation "multiple existental quantifier (1, 2)" 'Ex P0 = (ex1_2 ? ? P0). +(* multiple existental quantifier (1, 3) *) + +inductive ex1_3 (A0,A1,A2:Type[0]) (P0:A0→A1→A2→Prop) : Prop ≝ + | ex1_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → ex1_3 ? ? ? ? +. + +interpretation "multiple existental quantifier (1, 3)" 'Ex P0 = (ex1_3 ? ? ? P0). + (* multiple existental quantifier (2, 1) *) inductive ex2_1 (A0:Type[0]) (P0,P1:A0→Prop) : Prop ≝ diff --git a/matita/matita/contribs/lambda_delta/ground_2/xoa_notation.ma b/matita/matita/contribs/lambda_delta/ground_2/xoa_notation.ma index edd014ef0..86f68b608 100644 --- a/matita/matita/contribs/lambda_delta/ground_2/xoa_notation.ma +++ b/matita/matita/contribs/lambda_delta/ground_2/xoa_notation.ma @@ -24,6 +24,16 @@ notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0)" non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) }. +(* multiple existental quantifier (1, 3) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) }. + (* multiple existental quantifier (2, 1) *) notation > "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1)" diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma index d806697b8..b937c077f 100644 --- a/matita/matita/lib/arithmetics/nat.ma +++ b/matita/matita/lib/arithmetics/nat.ma @@ -452,6 +452,10 @@ qed-. (* More general conclusion **************************************************) +theorem nat_ind_plus: ∀R:predicate nat. + R 0 → (∀n. R n → R (n + 1)) → ∀n. R n. +/3 width=1 by nat_ind/ qed-. + theorem lt_O_n_elim: ∀n:nat. 0 < n → ∀P:nat → Prop.(∀m:nat.P (S m)) → P n. #n (elim n) // #abs @False_ind /2/ @absurd -- 2.39.2