From: Ferruccio Guidi Date: Sun, 22 Jul 2012 12:38:39 +0000 (+0000) Subject: - we polarized binders to control zeta reduction X-Git-Tag: make_still_working~1598 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a2144f09d1bd7022c1f2dfd4909a1fb9772c8d56;p=helm.git - we polarized binders to control zeta reduction - confluence and strong normalization proved --- diff --git a/matita/matita/contribs/lambda_delta/apps_2/functional/lift.ma b/matita/matita/contribs/lambda_delta/apps_2/functional/lift.ma index e2c802c51..361350c68 100644 --- a/matita/matita/contribs/lambda_delta/apps_2/functional/lift.ma +++ b/matita/matita/contribs/lambda_delta/apps_2/functional/lift.ma @@ -25,8 +25,8 @@ let rec flift d e U on U ≝ match U with | GRef _ ⇒ U ] | TPair I V T ⇒ match I with - [ Bind2 I ⇒ ⓑ{I} (flift d e V). (flift (d+1) e T) - | Flat2 I ⇒ ⓕ{I} (flift d e V). (flift d e T) + [ Bind2 a I ⇒ ⓑ{a,I} (flift d e V). (flift (d+1) e T) + | Flat2 I ⇒ ⓕ{I} (flift d e V). (flift d e T) ] ]. @@ -37,7 +37,7 @@ interpretation "functional relocation" 'Lift d e T = (flift d e T). theorem flift_lift: ∀T,d,e. ⇧[d, e] T ≡ ↑[d, e] T. #T elim T -T [ * #i #d #e // - elim (lt_or_eq_or_gt i d) #Hid normalize + elim (lt_or_eq_or_gt i d) #Hid normalize [ >(tri_lt ?????? Hid) /2 width=1/ | /2 width=1/ | >(tri_gt ?????? Hid) /3 width=2/ diff --git a/matita/matita/contribs/lambda_delta/apps_2/functional/rtm_step.ma b/matita/matita/contribs/lambda_delta/apps_2/functional/rtm_step.ma index bf04f72c9..ed16d5091 100644 --- a/matita/matita/contribs/lambda_delta/apps_2/functional/rtm_step.ma +++ b/matita/matita/contribs/lambda_delta/apps_2/functional/rtm_step.ma @@ -43,13 +43,13 @@ inductive rtm_step: relation rtm ≝ rtm_step (mk_rtm G u E S (ⓐV. T)) (mk_rtm G u E ({E, V} @ S) T) | rtm_beta : ∀G,u,E,F,V,S,W,T. - rtm_step (mk_rtm G u E ({F, V} @ S) (ⓛW. T)) + rtm_step (mk_rtm G u E ({F, V} @ S) (+ⓛW. T)) (mk_rtm G u (E. ④{Abbr} {u, F, V}) S T) | rtm_push : ∀G,u,E,W,T. - rtm_step (mk_rtm G u E ⟠ (ⓛW. T)) + rtm_step (mk_rtm G u E ⟠ (+ⓛW. T)) (mk_rtm G (u + 1) (E. ④{Abst} {u, E, W}) ⟠ T) | rtm_theta : ∀G,u,E,S,V,T. - rtm_step (mk_rtm G u E S (ⓓV. T)) + rtm_step (mk_rtm G u E S (+ⓓV. T)) (mk_rtm G u (E. ④{Abbr} {u, E, V}) S T) . 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 814579790..e19af6108 100644 --- a/matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma +++ b/matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma @@ -24,8 +24,8 @@ let rec fsubst W d U on U ≝ match U with | GRef _ ⇒ U ] | TPair I V T ⇒ match I with - [ Bind2 I ⇒ ⓑ{I} (fsubst W d V). (fsubst W (d+1) T) - | Flat2 I ⇒ ⓕ{I} (fsubst W d V). (fsubst W d T) + [ Bind2 a I ⇒ ⓑ{a,I} (fsubst W d V). (fsubst W (d+1) T) + | Flat2 I ⇒ ⓕ{I} (fsubst W d V). (fsubst W d T) ] ]. @@ -63,7 +63,7 @@ theorem fsubst_inv_delift: ∀K,V,T1,L,T2,d. ⇩[0, d] L ≡ K. ⓓV → ] | -HLK >(delift_inv_gref1 … H) -H // ] -| * #I #V1 #T1 #IHV1 #IHT1 #L #X #d #HLK #H +| * [ #a ] #I #V1 #T1 #IHV1 #IHT1 #L #X #d #HLK #H [ 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_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/acp_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/acp_aaa.ma index 1b2536c8b..f4da11310 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/acp_aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/acp_aaa.ma @@ -58,13 +58,13 @@ theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP. @(s4 … HB … ◊ … HV2 HLK2) @(s7 … HB … HKV2B) // ] -| #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20 +| #a #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20 elim (lifts_inv_bind1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct lapply (aacr_acr … H1RP H2RP A) #HA lapply (aacr_acr … H1RP H2RP B) #HB lapply (s1 … HB) -HB #HB @(s5 … HA … ◊ ◊) // /3 width=5/ -| #L #W #T #B #A #HLWB #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL02 +| #a #L #W #T #B #A #HLWB #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL02 elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct @(aacr_abst … H1RP H2RP) [ lapply (aacr_acr … H1RP H2RP B) #HB diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/acp_cr.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/acp_cr.ma index 5b8a2c1ea..b0b15e665 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/acp_cr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/acp_cr.ma @@ -31,7 +31,7 @@ definition S2 ≝ λRR:lenv→relation term. λRS:relation term. λRP,C:lenv→p (* Note: this is Tait's ii *) definition S3 ≝ λRP,C:lenv→predicate term. - ∀L,Vs,V,T,W. C L (ⒶVs. ⓓV. T) → RP L W → C L (ⒶVs. ⓐV. ⓛW. T). + ∀a,L,Vs,V,T,W. C L (ⒶVs. ⓓ{a}V. T) → RP L W → C L (ⒶVs. ⓐV. ⓛ{a}W. T). definition S4 ≝ λRP,C:lenv→predicate term. ∀L,K,Vs,V1,V2,i. C L (ⒶVs. V2) → ⇧[0, i + 1] V1 ≡ V2 → @@ -39,7 +39,7 @@ definition S4 ≝ λRP,C:lenv→predicate term. ∀L,K,Vs,V1,V2,i. definition S5 ≝ λRP,C:lenv→predicate term. ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → - ∀V,T. C (L. ⓓV) (ⒶV2s. T) → RP L V → C L (ⒶV1s. ⓓV. T). + ∀a,V,T. C (L. ⓓV) (ⒶV2s. T) → RP L V → C L (ⒶV1s. ⓓ{a}V. T). definition S6 ≝ λRP,C:lenv→predicate term. ∀L,Vs,T,W. C L (ⒶVs. T) → RP L W → C L (ⒶVs. ⓝW. T). @@ -120,7 +120,7 @@ lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → elim (lifts_inv_applv1 … H) -H #V0s #T0 #HV0s #HT0 #H destruct lapply (s1 … IHB … HB) #HV0 @(s2 … IHA … (V0 @ V0s)) /2 width=4 by lifts_simple_dx/ /3 width=6/ -| #L #Vs #U #T #W #HA #HW #L0 #V0 #X #des #HB #HL0 #H +| #a #L #Vs #U #T #W #HA #HW #L0 #V0 #X #des #HB #HL0 #H elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct elim (lifts_inv_flat1 … HY) -HY #U0 #X #HU0 #HX #H destruct elim (lifts_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT0 #H destruct @@ -135,7 +135,7 @@ lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → elim (lifts_lift_trans … Hdes0 … HVW1 … HW12) // -Hdes0 -Hi0 #V3 #HV13 #HVW2 >(lift_mono … HV13 … HV12) in HVW2; -V3 #HVW2 @(s4 … IHA … (V0 @ V0s) … HW12 HL02) /3 width=4/ -| #L #V1s #V2s #HV12s #V #T #HA #HV #L0 #V10 #X #des #HB #HL0 #H +| #L #V1s #V2s #HV12s #a #V #T #HA #HV #L0 #V10 #X #des #HB #HL0 #H elim (lifts_inv_applv1 … H) -H #V10s #Y #HV10s #HY #H destruct elim (lifts_inv_bind1 … HY) -HY #V0 #T0 #HV0 #HT0 #H destruct elim (lift_total V10 0 1) #V20 #HV120 @@ -156,12 +156,12 @@ lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → qed. lemma aacr_abst: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → - ∀L,W,T,A,B. RP L W → ( + ∀a,L,W,T,A,B. RP L W → ( ∀L0,V0,T0,des. ⇩*[des] L0 ≡ L → ⇧*[des + 1] T ≡ T0 → ⦃L0, V0⦄ ϵ[RP] 〚B〛 → ⦃L0. ⓓV0, T0⦄ ϵ[RP] 〚A〛 ) → - ⦃L, ⓛW. T⦄ ϵ[RP] 〚②B. A〛. -#RR #RS #RP #H1RP #H2RP #L #W #T #A #B #HW #HA #L0 #V0 #X #des #HB #HL0 #H + ⦃L, ⓛ{a}W. T⦄ ϵ[RP] 〚②B. A〛. +#RR #RS #RP #H1RP #H2RP #a #L #W #T #A #B #HW #HA #L0 #V0 #X #des #HB #HL0 #H lapply (aacr_acr … H1RP H2RP A) #HCA lapply (aacr_acr … H1RP H2RP B) #HCB elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct 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 5d4d74399..d350f0977 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 @@ -22,16 +22,16 @@ include "basic_2/computation/cprs_lcpr.ma". (* Advanced properties ******************************************************) lemma cprs_abst_dx: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀V,T1,T2. - L.ⓛV ⊢ T1 ➡* T2 → L ⊢ ⓛV1. T1 ➡* ⓛV2. T2. -#L #V1 #V2 #HV12 #V #T1 #T2 #HT12 @(cprs_ind … HT12) -T2 + L.ⓛV ⊢ T1 ➡* T2 → ∀a. L ⊢ ⓛ{a}V1. T1 ➡* ⓛ{a}V2. T2. +#L #V1 #V2 #HV12 #V #T1 #T2 #HT12 #a @(cprs_ind … HT12) -T2 [ /3 width=2/ | /3 width=6 by cprs_strap1, cpr_abst/ (**) (* /3 width=6/ is too slow *) ] qed. lemma cprs_abbr1_dx: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV1 ⊢ T1 ➡* T2 → - L ⊢ ⓓV1. T1 ➡* ⓓV2. T2. -#L #V1 #V2 #HV12 #T1 #T2 #HT12 @(cprs_ind_dx … HT12) -T1 + ∀a. L ⊢ ⓓ{a}V1. T1 ➡* ⓓ{a}V2. T2. +#L #V1 #V2 #HV12 #T1 #T2 #HT12 #a @(cprs_ind_dx … HT12) -T1 [ /3 width=5/ | #T1 #T #HT1 #_ #IHT1 @(cprs_strap2 … IHT1) -IHT1 /2 width=1/ @@ -39,11 +39,11 @@ lemma cprs_abbr1_dx: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV1 ⊢ T1 qed. lemma cpr_abbr1: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV1 ⊢ T1 ➡ T2 → - L ⊢ ⓓV1. T1 ➡* ⓓV2. T2. + ∀a. L ⊢ ⓓ{a}V1. T1 ➡* ⓓ{a}V2. T2. /3 width=1/ qed. lemma cpr_abbr2: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV2 ⊢ T1 ➡ T2 → - L ⊢ ⓓV1. T1 ➡* ⓓV2. 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/ qed. @@ -57,23 +57,23 @@ lemma cprs_strip: ∀L,T1,T. L ⊢ T ➡* T1 → ∀T2. L ⊢ T ➡ T2 → (* Basic_1: was pr3_gen_appl *) lemma cprs_inv_appl1: ∀L,V1,T1,U2. L ⊢ ⓐV1. T1 ➡* U2 → - ∨∨ ∃∃V2,T2. L ⊢ V1 ➡* V2 & L ⊢ T1 ➡* T2 & - U2 = ⓐV2. T2 - | ∃∃V2,W,T. L ⊢ V1 ➡* V2 & - L ⊢ T1 ➡* ⓛW. T & L ⊢ ⓓV2. T ➡* U2 - | ∃∃V0,V2,V,T. L ⊢ V1 ➡* V0 & ⇧[0,1] V0 ≡ V2 & - L ⊢ T1 ➡* ⓓV. T & L ⊢ ⓓV. ⓐV2. T ➡* U2. + ∨∨ ∃∃V2,T2. L ⊢ V1 ➡* V2 & L ⊢ T1 ➡* T2 & + U2 = ⓐV2. T2 + | ∃∃a,V2,W,T. L ⊢ V1 ➡* V2 & + L ⊢ T1 ➡* ⓛ{a}W. T & L ⊢ ⓓ{a}V2. T ➡* U2 + | ∃∃a,V0,V2,V,T. L ⊢ V1 ➡* V0 & ⇧[0,1] V0 ≡ V2 & + L ⊢ T1 ➡* ⓓ{a}V. T & L ⊢ ⓓ{a}V. ⓐV2. T ➡* U2. #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/ #U #U2 #_ #HU2 * * [ #V0 #T0 #HV10 #HT10 #H destruct elim (cpr_inv_appl1 … HU2) -HU2 * [ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5/ - | #V2 #W2 #T #T2 #HV02 #HT2 #H1 #H2 destruct /4 width=7/ - | #V #V2 #W0 #W2 #T #T2 #HV0 #HW02 #HT2 #HV2 #H1 #H2 destruct - @or3_intro2 @(ex4_4_intro … HV2 HT10) /2 width=3/ /3 width=1/ (**) (* explicit constructor. /5 width=8/ is too slow because TC_transitive gets in the way *) + | #a #V2 #W2 #T #T2 #HV02 #HT2 #H1 #H2 destruct /4 width=7/ + | #a #V #V2 #W0 #W2 #T #T2 #HV0 #HW02 #HT2 #HV2 #H1 #H2 destruct + @or3_intro2 @(ex4_5_intro … HV2 HT10) /2 width=3/ /3 width=1/ (**) (* explicit constructor. /5 width=8/ is too slow because TC_transitive gets in the way *) ] -| /4 width=8/ -| /4 width=10/ +| /4 width=9/ +| /4 width=11/ ] qed-. @@ -93,12 +93,12 @@ lemma cprs_flat: ∀I,L,T1,T2. L ⊢ T1 ➡* T2 → ∀V1,V2. L ⊢ V1 ➡* V2 L ⊢ ⓕ{I} V1. T1 ➡* ⓕ{I} V2. T2. #I #L #T1 #T2 #HT12 #V1 #V2 #HV12 @(cprs_ind … HV12) -V2 /2 width=1/ #V #V2 #_ #HV2 #IHV1 -@(cprs_trans … IHV1) -IHV1 /2 width=1/ +@(cprs_trans … IHV1) -IHV1 /2 width=1/ qed. lemma cprs_abst: ∀L,V1,V2. L ⊢ V1 ➡* V2 → ∀V,T1,T2. - L.ⓛV ⊢ T1 ➡* T2 → L ⊢ ⓛV1. T1 ➡* ⓛV2. T2. -#L #V1 #V2 #HV12 #V #T1 #T2 #HT12 @(cprs_ind … HV12) -V2 + L.ⓛV ⊢ T1 ➡* T2 → ∀a. L ⊢ ⓛ{a}V1. T1 ➡* ⓛ{a}V2. T2. +#L #V1 #V2 #HV12 #V #T1 #T2 #HT12 #a @(cprs_ind … HV12) -V2 [ lapply (cprs_lsubs_trans … HT12 (L.ⓛV1) ?) -HT12 /2 width=2/ | #V0 #V2 #_ #HV02 #IHV01 @(cprs_trans … IHV01) -V1 /2 width=2/ @@ -106,15 +106,15 @@ lemma cprs_abst: ∀L,V1,V2. L ⊢ V1 ➡* V2 → ∀V,T1,T2. qed. lemma cprs_abbr1: ∀L,V1,T1,T2. L. ⓓV1 ⊢ T1 ➡* T2 → ∀V2. L ⊢ V1 ➡* V2 → - L ⊢ ⓓV1. T1 ➡* ⓓV2. T2. -#L #V1 #T1 #T2 #HT12 #V2 #HV12 @(cprs_ind … HV12) -V2 /2 width=1/ + ∀a.L ⊢ ⓓ{a}V1. T1 ➡* ⓓ{a}V2. T2. +#L #V1 #T1 #T2 #HT12 #V2 #HV12 #a @(cprs_ind … HV12) -V2 /2 width=1/ #V #V2 #_ #HV2 #IHV1 @(cprs_trans … IHV1) -IHV1 /2 width=1/ qed. lemma cprs_abbr2_dx: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV2 ⊢ T1 ➡* T2 → - L ⊢ ⓓV1. T1 ➡* ⓓV2. T2. -#L #V1 #V2 #HV12 #T1 #T2 #HT12 @(cprs_ind_dx … HT12) -T1 + ∀a. L ⊢ ⓓ{a}V1. T1 ➡* ⓓ{a}V2. T2. +#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 @@ -123,16 +123,17 @@ lemma cprs_abbr2_dx: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV2 ⊢ T1 qed. lemma cprs_abbr2: ∀L,V1,V2. L ⊢ V1 ➡* V2 → ∀T1,T2. L. ⓓV2 ⊢ T1 ➡* T2 → - L ⊢ ⓓV1. T1 ➡* ⓓV2. T2. + ∀a. L ⊢ ⓓ{a}V1. T1 ➡* ⓓ{a}V2. T2. #L #V1 #V2 #HV12 @(cprs_ind … HV12) -V2 /2 width=1/ -#V #V2 #_ #HV2 #IHV1 #T1 #T2 #HT12 -lapply (IHV1 T1 T1 ?) -IHV1 // #HV1 +#V #V2 #_ #HV2 #IHV1 #T1 #T2 #HT12 #a +lapply (IHV1 T1 T1 ? a) -IHV1 // #HV1 @(cprs_trans … HV1) -HV1 /2 width=1/ qed. lemma cprs_beta_dx: ∀L,V1,V2,W,T1,T2. - L ⊢ V1 ➡ V2 → L.ⓛW ⊢ T1 ➡* T2 → L ⊢ ⓐV1.ⓛW.T1 ➡* ⓓV2.T2. -#L #V1 #V2 #W #T1 #T2 #HV12 #HT12 @(cprs_ind … HT12) -T2 + L ⊢ V1 ➡ V2 → L.ⓛW ⊢ T1 ➡* T2 → + ∀a.L ⊢ ⓐV1.ⓛ{a}W.T1 ➡* ⓓ{a}V2.T2. +#L #V1 #V2 #W #T1 #T2 #HV12 #HT12 #a @(cprs_ind … HT12) -T2 [ /3 width=1/ | -HV12 #T #T2 #_ #HT2 #IHT1 lapply (cpr_lsubs_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2 diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_delift.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_delift.ma index 96dd5bab7..6b7892611 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_delift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_delift.ma @@ -21,9 +21,9 @@ include "basic_2/computation/cprs.ma". (* Properties on inverse basic term relocation ******************************) (* Note: this should be stated with tprs *) -lemma cprs_zeta_delift: ∀L,V,T1,T2. L.ⓓV ⊢ ▼*[O, 1] T1 ≡ T2 → L ⊢ ⓓV.T1 ➡* T2. +lemma cprs_zeta_delift: ∀L,V,T1,T2. L.ⓓV ⊢ ▼*[O, 1] T1 ≡ T2 → L ⊢ +ⓓV.T1 ➡* T2. #L #V #T1 #T2 * #T #HT1 #HT2 -@(cprs_strap2 … (ⓓV.T)) [ /3 width=3/ | @inj /3 width=3/ ] (**) (* explicit constructor, /5 width=3/ is too slow *) +@(cprs_strap2 … (+ⓓV.T)) [ /3 width=3/ | @inj /3 width=3/ ] (**) (* explicit constructor, /5 width=3/ is too slow *) qed. (* Basic_1: was only: pr3_gen_cabbr *) 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 index 5efdb4fa2..9131ba4c2 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcprs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcprs.ma @@ -32,12 +32,12 @@ lemma lcprs_cpr_trans: ∀L1,L2. L1 ⊢ ➡* L2 → (* Advanced inversion lemmas ************************************************) (* Basic_1: was pr3_gen_abbr *) -lemma cprs_inv_abbr1: ∀L,V1,T1,U2. L ⊢ ⓓV1. T1 ➡* U2 → +lemma cprs_inv_abbr1: ∀a,L,V1,T1,U2. L ⊢ ⓓ{a}V1. T1 ➡* U2 → (∃∃V2,T2. L ⊢ V1 ➡* V2 & L. ⓓV1 ⊢ T1 ➡* T2 & - U2 = ⓓV2. T2 + U2 = ⓓ{a}V2. T2 ) ∨ - ∃∃T2. L. ⓓV1 ⊢ T1 ➡* T2 & ⇧[0, 1] U2 ≡ T2. -#L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/ + ∃∃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 * diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma index de134f056..36ce0ef83 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma @@ -39,17 +39,17 @@ lemma cprs_inv_lref1: ∀L,T2,i. L ⊢ #i ➡* T2 → qed-. (* Basic_1: was: pr3_gen_abst *) -lemma cprs_inv_abst1: ∀I,W,L,V1,T1,U2. L ⊢ ⓛV1. T1 ➡* U2 → +lemma cprs_inv_abst1: ∀I,W,a,L,V1,T1,U2. L ⊢ ⓛ{a}V1. T1 ➡* U2 → ∃∃V2,T2. L ⊢ V1 ➡* V2 & L. ⓑ{I} W ⊢ T1 ➡* T2 & - U2 = ⓛV2. T2. -#I #W #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /2 width=5/ + U2 = ⓛ{a}V2. T2. +#I #W #a #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /2 width=5/ #U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct elim (cpr_inv_abst1 … HU2 I W) -HU2 #V2 #T2 #HV2 #HT2 #H destruct /3 width=5/ qed-. -lemma cprs_inv_abst: ∀L,V1,V2,T1,T2. L ⊢ ⓛV1. T1 ➡* ⓛV2. T2 → ∀I,W. +lemma cprs_inv_abst: ∀a,L,V1,V2,T1,T2. L ⊢ ⓛ{a}V1. T1 ➡* ⓛ{a}V2. T2 → ∀I,W. L ⊢ V1 ➡* V2 ∧ L. ⓑ{I} W ⊢ T1 ➡* T2. -#L #V1 #V2 #T1 #T2 #H #I #W +#a #L #V1 #V2 #T1 #T2 #H #I #W elim (cprs_inv_abst1 I W … H) -H #V #T #HV1 #HT1 #H destruct /2 width=1/ 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 879b0bdae..ab8329cbc 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 @@ -26,16 +26,16 @@ lemma cprs_fwd_cnf: ∀L,T. L ⊢ 𝐍⦃T⦄ → ∀U. L ⊢ T ➡* U → T ≃ qed-. (* Basic_1: was: pr3_iso_beta *) -lemma cprs_fwd_beta: ∀L,V,W,T,U. L ⊢ ⓐV. ⓛW. T ➡* U → - ⓐV. ⓛW. T ≃ U ∨ L ⊢ ⓓV. T ➡* U. -#L #V #W #T #U #H +lemma cprs_fwd_beta: ∀a,L,V,W,T,U. L ⊢ ⓐV. ⓛ{a}W. T ➡* U → + ⓐV. ⓛ{a}W. T ≃ U ∨ L ⊢ ⓓ{a}V. T ➡* U. +#a #L #V #W #T #U #H elim (cprs_inv_appl1 … H) -H * [ #V0 #T0 #_ #_ #H destruct /2 width=1/ -| #V0 #W0 #T0 #HV0 #HT0 #HU +| #b #V0 #W0 #T0 #HV0 #HT0 #HU elim (cprs_inv_abst1 Abbr V … HT0) -HT0 #W1 #T1 #_ #HT1 #H destruct -W1 @or_intror -W @(cprs_trans … HU) -U /2 width=1/ (**) (* explicit constructor *) -| #V1 #V2 #V0 #T1 #_ #_ #HT1 #_ +| #b #V1 #V2 #V0 #T1 #_ #_ #HT1 #_ elim (cprs_inv_abst1 Abbr V … HT1) -HT1 #W2 #T2 #_ #_ #H destruct ] qed-. @@ -52,34 +52,34 @@ lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H destruct lapply (ldrop_fwd_ldrop2 … HLK) -HLK /3 width=9/ qed-. -lemma cprs_fwd_theta: ∀L,V1,V,T,U. L ⊢ ⓐV1. ⓓV. T ➡* U → - ∀V2. ⇧[0, 1] V1 ≡ V2 → ⓐV1. ⓓV. T ≃ U ∨ - L ⊢ ⓓV. ⓐV2. T ➡* U. -#L #V1 #V #T #U #H #V2 #HV12 +lemma cprs_fwd_theta: ∀a,L,V1,V,T,U. L ⊢ ⓐV1. ⓓ{a}V. T ➡* U → + ∀V2. ⇧[0, 1] V1 ≡ V2 → ⓐV1. ⓓ{a}V. T ≃ U ∨ + L ⊢ ⓓ{a}V. ⓐV2. T ➡* U. +#a #L #V1 #V #T #U #H #V2 #HV12 elim (cprs_inv_appl1 … H) -H * [ -HV12 #V0 #T0 #_ #_ #H destruct /2 width=1/ -| #V0 #W #T0 #HV10 #HT0 #HU +| #b #V0 #W #T0 #HV10 #HT0 #HU elim (cprs_inv_abbr1 … HT0) -HT0 * [ #V3 #T3 #_ #_ #H destruct - | #X #HT2 #H + | #X #HT2 #H #H0 destruct elim (lift_inv_bind1 … H) -H #W2 #T2 #HW2 #HT02 #H destruct @or_intror @(cprs_trans … HU) -U (**) (* explicit constructor *) - @(cprs_trans … (ⓓV.ⓐV2.ⓛW2.T2)) [ /3 width=1/ ] -T - @(cprs_strap2 … (ⓐV1.ⓛW.T0)) [ /5 width=7/ ] -V -V2 -W2 -T2 - @(cprs_strap2 … (ⓓV1.T0)) [ /3 width=1/ ] -W /2 width=1/ + @(cprs_trans … (+ⓓV.ⓐV2.ⓛ{b}W2.T2)) [ /3 width=1/ ] -T + @(cprs_strap2 … (ⓐV1.ⓛ{b}W.T0)) [ /5 width=7/ ] -V -V2 -W2 -T2 + @(cprs_strap2 … (ⓓ{b}V1.T0)) [ /3 width=1/ ] -W /2 width=1/ ] -| #V3 #V4 #V0 #T0 #HV13 #HV34 #HT0 #HU +| #b #V3 #V4 #V0 #T0 #HV13 #HV34 #HT0 #HU @or_intror @(cprs_trans … HU) -U (**) (* explicit constructor *) elim (cprs_inv_abbr1 … HT0) -HT0 * [ #V5 #T5 #HV5 #HT5 #H destruct lapply (cprs_lift (L.ⓓV) … HV12 … HV13 … HV34) -V1 -V3 /2 width=1/ /3 width=1/ - | #X #HT1 #H + | #X #HT1 #H #H0 destruct elim (lift_inv_bind1 … H) -H #V5 #T5 #HV05 #HT05 #H destruct lapply (cprs_lift (L.ⓓV0) … HV12 … HV13 … HV34) -V3 /2 width=1/ #HV24 - @(cprs_trans … (ⓓV.ⓐV2.ⓓV5.T5)) [ /3 width=1/ ] -T - @(cprs_strap2 … (ⓐV1.ⓓV0.T0)) [ /5 width=7/ ] -V -V5 -T5 - @(cprs_strap2 … (ⓓV0.ⓐV2.T0)) [ /3 width=3/ ] -V1 /3 width=1/ + @(cprs_trans … (+ⓓV.ⓐV2.ⓓ{b}V5.T5)) [ /3 width=1/ ] -T + @(cprs_strap2 … (ⓐV1.ⓓ{b}V0.T0)) [ /5 width=7/ ] -V -V5 -T5 + @(cprs_strap2 … (ⓓ{b}V0.ⓐV2.T0)) [ /3 width=3/ ] -V1 /3 width=1/ ] ] qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc_vector.ma index a6aedd799..fd3eb585e 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc_vector.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc_vector.ma @@ -26,35 +26,35 @@ lemma cprs_fwd_cnf_vector: ∀L,T. 𝐒⦃T⦄ → L ⊢ 𝐍⦃T⦄ → ∀Vs, #V #Vs #IHVs #U #H elim (cprs_inv_appl1 … H) -H * [ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1/ -| #V0 #W0 #T0 #HV0 #HT0 #HU +| #a #V0 #W0 #T0 #HV0 #HT0 #HU lapply (IHVs … HT0) -IHVs -HT0 #HT0 elim (tstc_inv_bind_appls_simple … HT0 ?) // -| #V1 #V2 #V0 #T0 #HV1 #HV12 #HT0 #HU +| #a #V1 #V2 #V0 #T0 #HV1 #HV12 #HT0 #HU lapply (IHVs … HT0) -IHVs -HT0 #HT0 elim (tstc_inv_bind_appls_simple … HT0 ?) // ] qed-. (* Basic_1: was: pr3_iso_appls_beta *) -lemma cprs_fwd_beta_vector: ∀L,Vs,V,W,T,U. L ⊢ ⒶVs. ⓐV. ⓛW. T ➡* U → - ⒶVs. ⓐV. ⓛW. T ≃ U ∨ L ⊢ ⒶVs. ⓓV. T ➡* U. -#L #Vs elim Vs -Vs /2 width=1 by cprs_fwd_beta/ +lemma cprs_fwd_beta_vector: ∀a,L,Vs,V,W,T,U. L ⊢ ⒶVs. ⓐV. ⓛ{a}W. T ➡* U → + ⒶVs. ⓐV. ⓛ{a}W. T ≃ U ∨ L ⊢ ⒶVs. ⓓ{a}V. T ➡* U. +#a #L #Vs elim Vs -Vs /2 width=1 by cprs_fwd_beta/ #V0 #Vs #IHVs #V #W #T #U #H elim (cprs_inv_appl1 … H) -H * [ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1/ -| #V1 #W1 #T1 #HV01 #HT1 #HU +| #b #V1 #W1 #T1 #HV01 #HT1 #HU elim (IHVs … HT1) -IHVs -HT1 #HT1 [ elim (tstc_inv_bind_appls_simple … HT1 ?) // | @or_intror -W (**) (* explicit constructor *) @(cprs_trans … HU) -U - @(cprs_strap1 … (ⓐV1.ⓛW1.T1)) [ /2 width=1/ ] -V -V0 -Vs -T /3 width=1/ + @(cprs_strap1 … (ⓐV1.ⓛ{b}W1.T1)) [ /2 width=1/ ] -V -V0 -Vs -T /3 width=1/ ] -| #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU +| #b #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU elim (IHVs … HT1) -IHVs -HT1 #HT1 [ elim (tstc_inv_bind_appls_simple … HT1 ?) // | @or_intror -W (**) (* explicit constructor *) @(cprs_trans … HU) -U - @(cprs_strap1 … (ⓐV1.ⓓV3.T1)) [ /2 width=1/ ] -V -V0 -Vs -T /3 width=3/ + @(cprs_strap1 … (ⓐV1.ⓓ{b}V3.T1)) [ /2 width=1/ ] -V -V0 -Vs -T /3 width=3/ ] ] qed-. @@ -67,29 +67,29 @@ lemma cprs_fwd_delta_vector: ∀L,K,V1,i. ⇩[0, i] L ≡ K. ⓓV1 → #V #Vs #IHVs #U #H -K -V1 elim (cprs_inv_appl1 … H) -H * [ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1/ -| #V0 #W0 #T0 #HV0 #HT0 #HU +| #b #V0 #W0 #T0 #HV0 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0 [ elim (tstc_inv_bind_appls_simple … HT0 ?) // | @or_intror -i (**) (* explicit constructor *) @(cprs_trans … HU) -U - @(cprs_strap1 … (ⓐV0.ⓛW0.T0)) [ /2 width=1/ ] -V -V2 -Vs /3 width=1/ + @(cprs_strap1 … (ⓐV0.ⓛ{b}W0.T0)) [ /2 width=1/ ] -V -V2 -Vs /3 width=1/ ] -| #V0 #V1 #V3 #T0 #HV0 #HV01 #HT0 #HU +| #b #V0 #V1 #V3 #T0 #HV0 #HV01 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0 [ elim (tstc_inv_bind_appls_simple … HT0 ?) // | @or_intror -i (**) (* explicit constructor *) @(cprs_trans … HU) -U - @(cprs_strap1 … (ⓐV0.ⓓV3.T0)) [ /2 width=1/ ] -V -V2 -Vs /3 width=3/ + @(cprs_strap1 … (ⓐV0.ⓓ{b}V3.T0)) [ /2 width=1/ ] -V -V2 -Vs /3 width=3/ ] ] qed-. (* Basic_1: was: pr3_iso_appls_abbr *) lemma cprs_fwd_theta_vector: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → - ∀V,T,U. L ⊢ ⒶV1s. ⓓV. T ➡* U → - ⒶV1s. ⓓV. T ≃ U ∨ L ⊢ ⓓV. ⒶV2s. T ➡* U. + ∀a,V,T,U. L ⊢ ⒶV1s. ⓓ{a}V. T ➡* U → + ⒶV1s. ⓓ{a}V. T ≃ U ∨ L ⊢ ⓓ{a}V. ⒶV2s. T ➡* U. #L #V1s #V2s * -V1s -V2s /3 width=1/ -#V1s #V2s #V1a #V2a #HV12a #HV12s +#V1s #V2s #V1a #V2a #HV12a #HV12s #a generalize in match HV12a; -HV12a generalize in match V2a; -V2a generalize in match V1a; -V1a @@ -97,7 +97,7 @@ elim HV12s -V1s -V2s /2 width=1 by cprs_fwd_theta/ #V1s #V2s #V1b #V2b #HV12b #_ #IHV12s #V1a #V2a #HV12a #V #T #U #H elim (cprs_inv_appl1 … H) -H * [ -IHV12s -HV12a -HV12b #V0 #T0 #_ #_ #H destruct /2 width=1/ -| #V0a #W0 #T0 #HV10a #HT0 #HU +| #b #V0a #W0 #T0 #HV10a #HT0 #HU elim (IHV12s … HV12b … HT0) -IHV12s -HT0 #HT0 [ -HV12a -HV12b -HV10a -HU elim (tstc_inv_pair1 … HT0) #V1 #T1 #H destruct @@ -105,14 +105,14 @@ elim (cprs_inv_appl1 … H) -H * @(cprs_trans … HU) -U elim (cprs_inv_abbr1 … HT0) -HT0 * [ -HV12a -HV12b -HV10a #V1 #T1 #_ #_ #H destruct - | -V1b #X #HT1 #H + | -V1b #X #HT1 #H #H0 destruct elim (lift_inv_bind1 … H) -H #W1 #T1 #HW01 #HT01 #H destruct - @(cprs_trans … (ⓓV.ⓐV2a.ⓛW1.T1)) [ /3 width=1/ ] -T -V2b -V2s - @(cprs_strap2 … (ⓐV1a.ⓛW0.T0)) [ /5 width=7/ ] -V -V2a -W1 -T1 - @(cprs_strap2 … (ⓓV1a.T0)) [ /3 width=1/ ] -W0 /2 width=1/ + @(cprs_trans … (+ⓓV.ⓐV2a.ⓛ{b}W1.T1)) [ /3 width=1/ ] -T -V2b -V2s + @(cprs_strap2 … (ⓐV1a.ⓛ{b}W0.T0)) [ /5 width=7/ ] -V -V2a -W1 -T1 + @(cprs_strap2 … (ⓓ{b}V1a.T0)) [ /3 width=1/ ] -W0 /2 width=1/ ] ] -| #V0a #Va #V0 #T0 #HV10a #HV0a #HT0 #HU +| #b #V0a #Va #V0 #T0 #HV10a #HV0a #HT0 #HU elim (IHV12s … HV12b … HT0) -HV12b -IHV12s -HT0 #HT0 [ -HV12a -HV10a -HV0a -HU elim (tstc_inv_pair1 … HT0) #V1 #T1 #H destruct @@ -121,13 +121,13 @@ elim (cprs_inv_appl1 … H) -H * elim (cprs_inv_abbr1 … HT0) -HT0 * [ #V1 #T1 #HV1 #HT1 #H destruct lapply (cprs_lift (L.ⓓV) … HV12a … HV10a … HV0a) -V1a -V0a [ /2 width=1/ ] #HV2a - @(cprs_trans … (ⓓV.ⓐV2a.T1)) [ /3 width=1/ ] -T -V2b -V2s /3 width=1/ - | #X #HT1 #H + @(cprs_trans … (ⓓ{a}V.ⓐV2a.T1)) [ /3 width=1/ ] -T -V2b -V2s /3 width=1/ + | #X #HT1 #H #H0 destruct elim (lift_inv_bind1 … H) -H #V1 #T1 #HW01 #HT01 #H destruct lapply (cprs_lift (L.ⓓV0) … HV12a … HV10a … HV0a) -V0a [ /2 width=1/ ] #HV2a - @(cprs_trans … (ⓓV.ⓐV2a.ⓓV1.T1)) [ /3 width=1/ ] -T -V2b -V2s - @(cprs_strap2 … (ⓐV1a.ⓓV0.T0)) [ /5 width=7/ ] -V -V1 -T1 - @(cprs_strap2 … (ⓓV0.ⓐV2a.T0)) [ /3 width=3/ ] -V1a /3 width=1/ + @(cprs_trans … (+ⓓV.ⓐV2a.ⓓ{b}V1.T1)) [ /3 width=1/ ] -T -V2b -V2s + @(cprs_strap2 … (ⓐV1a.ⓓ{b}V0.T0)) [ /5 width=7/ ] -V -V1 -T1 + @(cprs_strap2 … (ⓓ{b}V0.ⓐV2a.T0)) [ /3 width=3/ ] -V1a /3 width=1/ ] ] ] @@ -140,18 +140,18 @@ lemma cprs_fwd_tau_vector: ∀L,Vs,W,T,U. L ⊢ ⒶVs. ⓝW. T ➡* U → #V #Vs #IHVs #W #T #U #H elim (cprs_inv_appl1 … H) -H * [ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1/ -| #V0 #W0 #T0 #HV0 #HT0 #HU +| #b #V0 #W0 #T0 #HV0 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0 [ elim (tstc_inv_bind_appls_simple … HT0 ?) // | @or_intror -W (**) (* explicit constructor *) @(cprs_trans … HU) -U - @(cprs_strap1 … (ⓐV0.ⓛW0.T0)) [ /2 width=1/ ] -V -Vs -T /3 width=1/ + @(cprs_strap1 … (ⓐV0.ⓛ{b}W0.T0)) [ /2 width=1/ ] -V -Vs -T /3 width=1/ ] -| #V0 #V1 #V2 #T0 #HV0 #HV01 #HT0 #HU +| #b #V0 #V1 #V2 #T0 #HV0 #HV01 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0 [ elim (tstc_inv_bind_appls_simple … HT0 ?) // | @or_intror -W (**) (* explicit constructor *) @(cprs_trans … HU) -U - @(cprs_strap1 … (ⓐV0.ⓓV2.T0)) [ /2 width=1/ ] -V -Vs -T /3 width=3/ + @(cprs_strap1 … (ⓐV0.ⓓ{b}V2.T0)) [ /2 width=1/ ] -V -Vs -T /3 width=3/ ] qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr.ma index 594e76139..ccfd6015b 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr.ma @@ -30,12 +30,12 @@ lemma csn_fwd_pair_sn: ∀I,L,V,T. L ⊢ ⬊* ②{I} V. T → L ⊢ ⬊* V. /2 width=5/ qed. fact csn_fwd_bind_dx_aux: ∀L,U. L ⊢ ⬊* U → - ∀I,V,T. U = ⓑ{I} V. T → L. ⓑ{I} V ⊢ ⬊* T. -#L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct + ∀a,I,V,T. U = ⓑ{a,I} V. T → L. ⓑ{I} V ⊢ ⬊* T. +#L #U #H elim H -H #U0 #_ #IH #a #I #V #T #H destruct @csn_intro #T2 #HLT2 #HT2 -@(IH (ⓑ{I} V. T2)) -IH // /2 width=1/ -HLT2 #H destruct /2 width=1/ +@(IH (ⓑ{a,I} V. T2)) -IH // /2 width=1/ -HLT2 #H destruct /2 width=1/ qed. (* Basic_1: was: sn3_gen_bind *) -lemma csn_fwd_bind_dx: ∀I,L,V,T. L ⊢ ⬊* ⓑ{I} V. T → L. ⓑ{I} V ⊢ ⬊* T. -/2 width=3/ qed. +lemma csn_fwd_bind_dx: ∀a,I,L,V,T. L ⊢ ⬊* ⓑ{a,I} V. T → L. ⓑ{I} V ⊢ ⬊* T. +/2 width=4/ qed. 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 index 5aa47837d..58807c524 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma @@ -28,8 +28,8 @@ lemma csn_lcpr_conf: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T. L1 ⊢ ⬊* T → L2 ⊢ @IHT /2 width=2/ -IHT -HT0 /2 width=3/ qed. -lemma csn_abbr: ∀L,V. L ⊢ ⬊* V → ∀T. L. ⓓV ⊢ ⬊* T → L ⊢ ⬊* ⓓV. T. -#L #V #HV elim HV -V #V #_ #IHV #T #HT @(csn_ind_alt … HT) -T #T #HT #IHT +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 @@ -46,9 +46,9 @@ elim (cpr_inv_abbr1 … H1) -H1 * ] qed. -fact csn_appl_beta_aux: ∀L,W. L ⊢ ⬊* W → ∀U. L ⊢ ⬊* U → - ∀V,T. U = ⓓV. T → L ⊢ ⬊* ⓐV. ⓛW. T. -#L #W #H elim H -W #W #_ #IHW #X #H @(csn_ind_alt … H) -X #X #HVT #IHVT #V #T #H destruct +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 @@ -62,22 +62,22 @@ elim (cpr_inv_appl1 … H) -H * | -IHW -HLW0 -HV -HT * #H #HVT0 destruct @(IHVT … HVT0) -IHVT -HVT0 // /2 width=1/ ] -| -IHW -IHVT -H2 #V0 #W0 #T0 #T1 #HLV0 #HLT01 #H1 #H2 destruct +| -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 #V0 #V1 #W0 #W1 #T0 #T1 #_ #_ #_ #_ #H destruct +| -IHW -IHVT -HV -HT -H2 #b #V0 #V1 #W0 #W1 #T0 #T1 #_ #_ #_ #_ #H destruct ] qed. (* Basic_1: was: sn3_beta *) -lemma csn_appl_beta: ∀L,W. L ⊢ ⬊* W → ∀V,T. L ⊢ ⬊* ⓓV. T → - L ⊢ ⬊* ⓐV. ⓛW. T. +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: ∀L,U. L ⊢ ⬊* U → ∀V1,V2. ⇧[0, 1] V1 ≡ V2 → - ∀V,T. U = ⓓV. ⓐV2. T → L ⊢ ⬊* ⓐV1. ⓓV. T. -#L #X #H @(csn_ind_alt … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct +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 @@ -87,7 +87,7 @@ elim (cpr_inv_appl1 … 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 (ⓓV.ⓐV2.T) (ⓓV4.ⓐV5.T3)) + 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 @@ -100,13 +100,13 @@ elim (cpr_inv_appl1 … HL) -HL * 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 + | -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 #V0 #W0 #T0 #T1 #_ #_ #H destruct -| -IHVT -H #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HLW01 #HLT01 #HV03 #H1 #H2 destruct +| -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 @@ -115,8 +115,8 @@ elim (cpr_inv_appl1 … HL) -HL * ] qed. -lemma csn_appl_theta: ∀V1,V2. ⇧[0, 1] V1 ≡ V2 → - ∀L,V,T. L ⊢ ⬊* ⓓV. ⓐV2. T → L ⊢ ⬊* ⓐV1. ⓓV. T. +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 *) diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma index 271cc8bc6..4fd784d75 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma @@ -58,8 +58,8 @@ elim (cpr_inv_lref1 … H) -H ] qed. -lemma csn_abst: ∀L,W. L ⊢ ⬊* W → ∀I,V,T. L. ⓑ{I} V ⊢ ⬊* T → L ⊢ ⬊* ⓛW. T. -#L #W #HW elim HW -W #W #_ #IHW #I #V #T #HT @(csn_ind … HT) -T #T #HT #IHT +lemma csn_abst: ∀a,L,W. L ⊢ ⬊* W → ∀I,V,T. L. ⓑ{I} V ⊢ ⬊* T → L ⊢ ⬊* ⓛ{a}W. T. +#a #L #W #HW elim HW -W #W #_ #IHW #I #V #T #HT @(csn_ind … HT) -T #T #HT #IHT @csn_intro #X #H1 #H2 elim (cpr_inv_abst1 … H1 I V) -H1 #W0 #T0 #HLW0 #HLT0 #H destruct 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 a33fc0ddc..91e3653f3 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 @@ -34,10 +34,10 @@ elim (H0 ?) -H0 // qed. (* Basic_1: was: sn3_appls_beta *) -lemma csn_applv_beta: ∀L,W. L ⊢ ⬊* W → - ∀Vs,V,T. L ⊢ ⬊* ⒶVs.ⓓV.T → - L ⊢ ⬊* ⒶVs. ⓐV.ⓛW. T. -#L #W #HW #Vs elim Vs -Vs /2 width=1/ -HW +lemma csn_applv_beta: ∀a,L,W. L ⊢ ⬊* W → + ∀Vs,V,T. L ⊢ ⬊* ⒶVs.ⓓ{a}V.T → + L ⊢ ⬊* ⒶVs. ⓐV.ⓛ{a}W. T. +#a #L #W #HW #Vs elim Vs -Vs /2 width=1/ -HW #V0 #Vs #IHV #V #T #H1T lapply (csn_fwd_pair_sn … H1T) #HV0 lapply (csn_fwd_flat_dx … H1T) #H2T @@ -69,10 +69,10 @@ lemma csn_applv_delta: ∀L,K,V1,i. ⇩[0, i] L ≡ K. ⓓV1 → qed. (* Basic_1: was: sn3_appls_abbr *) -lemma csn_applv_theta: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → - ∀V,T. L ⊢ ⬊* ⓓV. ⒶV2s. T → L ⊢ ⬊* V → - L ⊢ ⬊* ⒶV1s. ⓓV. T. -#L #V1s #V2s * -V1s -V2s /2 width=1/ +lemma csn_applv_theta: ∀a,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → + ∀V,T. L ⊢ ⬊* ⓓ{a}V. ⒶV2s. T → L ⊢ ⬊* V → + L ⊢ ⬊* ⒶV1s. ⓓ{a}V. T. +#a #L #V1s #V2s * -V1s -V2s /2 width=1/ #V1s #V2s #V1 #V2 #HV12 #H generalize in match HV12; -HV12 generalize in match V2; -V2 generalize in match V1; -V1 elim H -V1s -V2s /2 width=3/ @@ -108,7 +108,7 @@ theorem csn_acr: acr cpr (eq …) (csn …) (λL,T. L ⊢ ⬊* T). [ /3 width=1/ | /2 width=1/ | /2 width=6/ -| #L #V1 #V2 #HV12 #V #T #H #HVT +| #L #V1 #V2 #HV12 #a #V #T #H #HVT @(csn_applv_theta … HV12) -HV12 // @(csn_abbr) // | /2 width=1/ diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/xprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs.ma index 775e136cb..2eb8903e1 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/xprs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs.ma @@ -45,14 +45,16 @@ qed-. lemma xprs_refl: ∀h,g,L,T. ⦃h, L⦄ ⊢ T ➸*[g] T. /2 width=1/ qed. -lemma xprs_strap1: ∀h,g,L,T1,T,T2. +axiom xprs_strap1: ∀h,g,L,T1,T,T2. ⦃h, L⦄ ⊢ T1 ➸*[g] T → ⦃h, L⦄ ⊢ T ➸[g] T2 → ⦃h, L⦄ ⊢ T1 ➸*[g] T2. +(**) (* NTypeChecker failure /2 width=3/ qed. - -lemma xprs_strap2: ∀h,g,L,T1,T,T2. +*) +axiom xprs_strap2: ∀h,g,L,T1,T,T2. ⦃h, L⦄ ⊢ T1 ➸[g] T → ⦃h, L⦄ ⊢ T ➸*[g] T2 → ⦃h, L⦄ ⊢ T1 ➸*[g] T2. +(**) (* NTypeChecker failure /2 width=3/ qed. - +*) (* Basic inversion lemmas ***************************************************) (* axiom xprs_inv_cnf1: ∀L,T,U. L ⊢ T ➡* U → L ⊢ 𝐍⦃T⦄ → T = U. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_aaa.ma new file mode 100644 index 000000000..2de7cbcd8 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_aaa.ma @@ -0,0 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||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/xpr_aaa.ma". +include "basic_2/computation/xprs.ma". + +(* EXTENDED PARALLEL COMPUTATION ON TERMS ***********************************) + +(* Properties on atomic arity assignment for terms **************************) + +lemma xprs_aaa: ∀h,g,L,T,A. L ⊢ T ⁝ A → ∀U. ⦃h, L⦄ ⊢ T ➸*[g] U → L ⊢ U ⁝ A. +#h #g #L #T #A #HT #U #H @(xprs_ind … H) -U // /2 width=5/ +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_cprs.ma new file mode 100644 index 000000000..0d2e22c58 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_cprs.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/computation/cprs.ma". +include "basic_2/computation/xprs.ma". + +(* EXTENDED PARALLEL COMPUTATION ON TERMS ***********************************) + +(* properties on context sensitive parallel computation for terms ***********) + +lemma cprs_xprs: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → ⦃h, L⦄ ⊢ T1 ➸*[g] T2. +#h #g #L #T1 #T2 #H @(cprs_ind … H) -T2 // +/3 width=3 by xprs_strap1, cpr_xpr/ (**) (* NTypeChecker failure without trace *) +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_lift.ma index 534badc84..54bdc487a 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_lift.ma @@ -20,9 +20,9 @@ include "basic_2/computation/xprs.ma". (* Advanced forward lemmas **************************************************) -lemma xprs_fwd_abst1: ∀h,g,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓛV1. T1 ➸*[g] U2 → - ∃∃V2,T2. L ⊢ V1 ➡* V2 & U2 = ⓛV2. T2. -#h #g #L #V1 #T1 #U2 #H @(xprs_ind … H) -U2 /2 width=4/ +lemma xprs_fwd_abst1: ∀h,g,a,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓛ{a}V1. T1 ➸*[g] U2 → + ∃∃V2,T2. L ⊢ V1 ➡* V2 & U2 = ⓛ{a}V2. T2. +#h #g #a #L #V1 #T1 #U2 #H @(xprs_ind … H) -U2 /2 width=4/ #U #U2 #_ #HU2 * #V #T #HV1 #H destruct elim (xpr_inv_abst1 … HU2) -HU2 #V2 #T2 #HV2 #_ #H destruct /3 width=4/ qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv.ma index 23a93550c..25b85269e 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv.ma @@ -21,10 +21,10 @@ include "basic_2/equivalence/cpcs.ma". inductive snv (h:sh) (g:sd h): lenv → predicate term ≝ | snv_sort: ∀L,k. snv h g L (⋆k) | snv_lref: ∀I,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → snv h g K V → snv h g L (#i) -| snv_bind: ∀I,L,V,T. snv h g L V → snv h g (L.ⓑ{I}V) T → snv h g L (ⓑ{I}V.T) -| snv_appl: ∀L,V,W,W0,T,U,l. snv h g L V → snv h g L T → +| snv_bind: ∀a,I,L,V,T. snv h g L V → snv h g (L.ⓑ{I}V) T → snv h g L (ⓑ{a,I}V.T) +| snv_appl: ∀a,L,V,W,W0,T,U,l. snv h g L V → snv h g L T → ⦃h, L⦄ ⊢ V •[g, l + 1] W → L ⊢ W ➡* W0 → - ⦃h, L⦄ ⊢ T ➸*[g] ⓛW0.U → snv h g L (ⓐV.T) + ⦃h, L⦄ ⊢ T ➸*[g] ⓛ{a}W0.U → snv h g L (ⓐV.T) | snv_cast: ∀L,W,T,U,l. snv h g L W → snv h g L T → ⦃h, L⦄ ⊢ T •[g, l + 1] U → L ⊢ U ⬌* W → snv h g L (ⓝW.T) . @@ -34,36 +34,36 @@ interpretation "stratified native validity (term)" (* Basic inversion lemmas ***************************************************) -lemma snv_inv_bind_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀I,V,T. X = ⓑ{I}V.T → +lemma snv_inv_bind_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀a,I,V,T. X = ⓑ{a,I}V.T → ⦃h, L⦄ ⊩ V :[g] ∧ ⦃h, L.ⓑ{I}V⦄ ⊩ T :[g]. #h #g #L #X * -L -X -[ #L #k #I #V #T #H destruct -| #I0 #L #K #V0 #i #_ #_ #I #V #T #H destruct -| #I0 #L #V0 #T0 #HV0 #HT0 #I #V #T #H destruct /2 width=1/ -| #L #V0 #W0 #W00 #T0 #U0 #l #_ #_ #_ #_ #_ #I #V #T #H destruct -| #L #W0 #T0 #U0 #l #_ #_ #_ #_ #I #V #T #H destruct +[ #L #k #a #I #V #T #H destruct +| #I0 #L #K #V0 #i #_ #_ #a #I #V #T #H destruct +| #b #I0 #L #V0 #T0 #HV0 #HT0 #a #I #V #T #H destruct /2 width=1/ +| #b #L #V0 #W0 #W00 #T0 #U0 #l #_ #_ #_ #_ #_ #a #I #V #T #H destruct +| #L #W0 #T0 #U0 #l #_ #_ #_ #_ #a #I #V #T #H destruct ] qed. -lemma snv_inv_bind: ∀h,g,I,L,V,T. ⦃h, L⦄ ⊩ ⓑ{I}V.T :[g] → +lemma snv_inv_bind: ∀h,g,a,I,L,V,T. ⦃h, L⦄ ⊩ ⓑ{a,I}V.T :[g] → ⦃h, L⦄ ⊩ V :[g] ∧ ⦃h, L.ⓑ{I}V⦄ ⊩ T :[g]. -/2 width=3/ qed-. +/2 width=4/ qed-. lemma snv_inv_appl_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀V,T. X = ⓐV.T → - ∃∃W,W0,U,l. ⦃h, L⦄ ⊩ V :[g] & ⦃h, L⦄ ⊩ T :[g] & + ∃∃a,W,W0,U,l. ⦃h, L⦄ ⊩ V :[g] & ⦃h, L⦄ ⊩ T :[g] & ⦃h, L⦄ ⊢ V •[g, l + 1] W & L ⊢ W ➡* W0 & - ⦃h, L⦄ ⊢ T ➸*[g] ⓛW0.U. + ⦃h, L⦄ ⊢ T ➸*[g] ⓛ{a}W0.U. #h #g #L #X * -L -X [ #L #k #V #T #H destruct | #I #L #K #V0 #i #_ #_ #V #T #H destruct -| #I #L #V0 #T0 #_ #_ #V #T #H destruct -| #L #V0 #W0 #W00 #T0 #U0 #l #HV0 #HT0 #HVW0 #HW00 #HTU0 #V #T #H destruct /2 width=7/ +| #a #I #L #V0 #T0 #_ #_ #V #T #H destruct +| #a #L #V0 #W0 #W00 #T0 #U0 #l #HV0 #HT0 #HVW0 #HW00 #HTU0 #V #T #H destruct /2 width=8/ | #L #W0 #T0 #U0 #l #_ #_ #_ #_ #V #T #H destruct ] qed. lemma snv_inv_appl: ∀h,g,L,V,T. ⦃h, L⦄ ⊩ ⓐV.T :[g] → - ∃∃W,W0,U,l. ⦃h, L⦄ ⊩ V :[g] & ⦃h, L⦄ ⊩ T :[g] & + ∃∃a,W,W0,U,l. ⦃h, L⦄ ⊩ V :[g] & ⦃h, L⦄ ⊩ T :[g] & ⦃h, L⦄ ⊢ V •[g, l + 1] W & L ⊢ W ➡* W0 & - ⦃h, L⦄ ⊢ T ➸*[g] ⓛW0.U. + ⦃h, L⦄ ⊢ T ➸*[g] ⓛ{a}W0.U. /2 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 new file mode 100644 index 000000000..f5953fedb --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_aaa.ma @@ -0,0 +1,43 @@ +(**************************************************************************) +(* ___ *) +(* ||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/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/dynamic/snv.ma". + +(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) + +(* Properties on atomic arity assignment for terms **************************) + +lemma snv_aaa: ∀h,g,L,T. ⦃h, L⦄ ⊩ T :[g] → ∃A. L ⊢ T ⁝ A. +#h #g #L #T #H elim H -L -T +[ /2 width=2/ +| #I #L #K #V #i #HLK #_ * /3 width=6/ +| #a * #L #V #T #_ #_ * #B #HV * #A #HA /3 width=2/ +| #a #L #V #W #W0 #T #U #l #_ #_ #HVW #HW0 #HTU * #B #HV * #X #HT + lapply (xprs_aaa h g … HV W0 ?) + [ /3 width=3 by xprs_strap2, ssta_xpr, cprs_xprs/ ] -W #HW0 (**) (* NTypeChecker failure without trace *) + lapply (xprs_aaa … HT … HTU) -HTU #H + elim (aaa_inv_abst … H) -H #B0 #A #H1 #HU #H2 destruct + lapply (aaa_mono … H1 … HW0) -W0 #H destruct /3 width=4/ +| #L #W #T #U #l #_ #_ #HTU #HUW * #B #HW * #A #HT + lapply (aaa_cpcs_mono … HUW A … HW) -HUW /2 width=7/ -HTU #H destruct /3 width=3/ +] +qed-. + +lemma snv_csn: ∀h,g,L,T. ⦃h, L⦄ ⊩ T :[g] → L ⊢ ⬊* T. +#h #g #L #T #H elim (snv_aaa … H) -H /2 width=2/ +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_lift.ma index a2e407e30..6d79ef571 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_lift.ma @@ -32,15 +32,15 @@ lemma snv_lift: ∀h,g,K,T. ⦃h, K⦄ ⊩ T :[g] → ∀L,d,e. ⇩[d, e] L ≡ /3 width=8/ | lapply (ldrop_trans_ge … HLK … HK0 ?) -K // -Hid /3 width=8/ ] -| #I #K #V #T #_ #_ #IHV #IHT #L #d #e #HLK #X #H +| #a #I #K #V #T #_ #_ #IHV #IHT #L #d #e #HLK #X #H elim (lift_inv_bind1 … H) -H #W #U #HVW #HTU #H destruct /4 width=4/ -| #K #V #V0 #V1 #T #T1 #l #_ #_ #HV0 #HV01 #HT1 #IHV #IHT #L #d #e #HLK #X #H +| #a #K #V #V0 #V1 #T #T1 #l #_ #_ #HV0 #HV01 #HT1 #IHV #IHT #L #d #e #HLK #X #H elim (lift_inv_flat1 … H) -H #W #U #HVW #HTU #H destruct elim (lift_total V0 d e) #W0 #HVW0 elim (lift_total V1 d e) #W1 #HVW1 elim (lift_total T1 (d+1) e) #U1 #HTU1 - @(snv_appl … W0 … W1 … U1 l) + @(snv_appl … a … W0 … W1 … U1 l) [ /2 width=4/ | /2 width=4/ | /2 width=9/ | /2 width=9/ ] @(xprs_lift … HLK … HTU … HT1) /2 width=1/ | #K #V0 #T #V #l #_ #_ #HTV #HV0 #IHV0 #IHT #L #d #e #HLK #X #H @@ -62,15 +62,15 @@ lemma snv_inv_lift: ∀h,g,L,U. ⦃h, L⦄ ⊩ U :[g] → ∀K,d,e. ⇩[d, e] L /3 width=8/ | lapply (ldrop_conf_ge … HLK … HL0 ?) -L // -Hid /3 width=8/ ] -| #I #L #W #U #_ #_ #IHW #IHU #K #d #e #HLK #X #H +| #a #I #L #W #U #_ #_ #IHW #IHU #K #d #e #HLK #X #H elim (lift_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct /4 width=4/ -| #L #W #W0 #W1 #U #U1 #l #_ #_ #HW0 #HW01 #HU1 #IHW #IHU #K #d #e #HLK #X #H +| #a #L #W #W0 #W1 #U #U1 #l #_ #_ #HW0 #HW01 #HU1 #IHW #IHU #K #d #e #HLK #X #H elim (lift_inv_flat2 … H) -H #V #T #HVW #HTU #H destruct elim (ssta_inv_lift1 … HW0 … HLK … HVW) -HW0 #V0 #HV0 #HVW0 elim (cprs_inv_lift1 … HLK … HVW0 … HW01) -W0 #V1 #HVW1 #HV01 elim (xprs_inv_lift1 … HLK … HTU … HU1) -HU1 #X #H #HTU elim (lift_inv_bind2 … H) -H #Y #T1 #HY #HTU1 #H destruct - lapply (lift_inj … HY … HVW1) -HY #H destruct /3 width=7/ + lapply (lift_inj … HY … HVW1) -HY #H destruct /3 width=8/ | #L #W0 #U #W #l #_ #_ #HUW #HW0 #IHW0 #IHU #K #d #e #HLK #X #H elim (lift_inv_flat2 … H) -H #V0 #T #HVW0 #HTU #H destruct elim (ssta_inv_lift1 … HUW … HLK … HTU) -HUW #V #HTV #HVW 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 31a8d0b49..04c071f20 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 @@ -42,39 +42,39 @@ lapply (cprs_inv_sort1 … H2) -L #H destruct // qed-. (* Basic_1: was: pc3_gen_sort_abst *) -lemma cpcs_inv_sort_abst: ∀L,W,T,k. L ⊢ ⋆k ⬌* ⓛW.T → ⊥. -#L #W #T #k #H +lemma cpcs_inv_sort_abst: ∀a,L,W,T,k. L ⊢ ⋆k ⬌* ⓛ{a}W.T → ⊥. +#a #L #W #T #k #H elim (cpcs_inv_cprs … H) -H #X #H1 >(cprs_inv_sort1 … H1) -X #H2 elim (cprs_inv_abst1 Abst W … H2) -H2 #W0 #T0 #_ #_ #H destruct qed-. (* Basic_1: was: pc3_gen_abst *) -lemma cpcs_inv_abst: ∀L,W1,W2,T1,T2. L ⊢ ⓛW1.T1 ⬌* ⓛW2.T2 → ∀I,V. - L ⊢ W1 ⬌* W2 ∧ L. ②{I}V ⊢ T1 ⬌* T2. -#L #W1 #W2 #T1 #T2 #H #I #V +lemma cpcs_inv_abst: ∀a1,a2,L,W1,W2,T1,T2. L ⊢ ⓛ{a1}W1.T1 ⬌* ⓛ{a2}W2.T2 → ∀I,V. + ∧∧ L ⊢ W1 ⬌* W2 & L. ②{I}V ⊢ T1 ⬌* T2 & a1 = a2. +#a1 #a2 #L #W1 #W2 #T1 #T2 #H #I #V elim (cpcs_inv_cprs … H) -H #T #H1 #H2 elim (cprs_inv_abst1 I V … H1) -H1 #W0 #T0 #HW10 #HT10 #H destruct elim (cprs_inv_abst1 I V … H2) -H2 #W #T #HW2 #HT2 #H destruct /3 width=3/ qed-. (* Basic_1: was: pc3_gen_abst_shift *) -lemma cpcs_inv_abst_shift: ∀L,W1,W2,T1,T2. L ⊢ ⓛW1.T1 ⬌* ⓛW2.T2 → ∀W. - L ⊢ W1 ⬌* W2 ∧ L. ⓛW ⊢ T1 ⬌* T2. -#L #W1 #W2 #T1 #T2 #H #W +lemma cpcs_inv_abst_shift: ∀a1,a2,L,W1,W2,T1,T2. L ⊢ ⓛ{a1}W1.T1 ⬌* ⓛ{a2}W2.T2 → ∀W. + ∧∧ L ⊢ W1 ⬌* W2 & L. ⓛW ⊢ T1 ⬌* T2 & a1 = a2. +#a1 #a2 #L #W1 #W2 #T1 #T2 #H #W lapply (cpcs_inv_abst … H Abst W) -H // qed. -lemma cpcs_inv_abst1: ∀L,W1,T1,T. L ⊢ ⓛW1.T1 ⬌* T → - ∃∃W2,T2. L ⊢ T ➡* ⓛW2.T2 & L ⊢ ⓛW1.T1 ➡* ⓛW2.T2. -#L #W1 #T1 #T #H +lemma cpcs_inv_abst1: ∀a,L,W1,T1,T. L ⊢ ⓛ{a}W1.T1 ⬌* T → + ∃∃W2,T2. L ⊢ T ➡* ⓛ{a}W2.T2 & L ⊢ ⓛ{a}W1.T1 ➡* ⓛ{a}W2.T2. +#a #L #W1 #T1 #T #H elim (cpcs_inv_cprs … H) -H #X #H1 #H2 elim (cprs_inv_abst1 Abst W1 … H1) -H1 #W2 #T2 #HW12 #HT12 #H destruct @(ex2_2_intro … H2) -H2 /2 width=2/ (**) (* explicit constructor, /3 width=6/ is slow *) qed-. -lemma cpcs_inv_abst2: ∀L,W1,T1,T. L ⊢ T ⬌* ⓛW1.T1 → - ∃∃W2,T2. L ⊢ T ➡* ⓛW2.T2 & L ⊢ ⓛW1.T1 ➡* ⓛW2.T2. +lemma cpcs_inv_abst2: ∀a,L,W1,T1,T. L ⊢ T ⬌* ⓛ{a}W1.T1 → + ∃∃W2,T2. L ⊢ T ➡* ⓛ{a}W2.T2 & L ⊢ ⓛ{a}W1.T1 ➡* ⓛ{a}W2.T2. /3 width=1 by cpcs_inv_abst1, cpcs_sym/ qed-. (* Basic_1: was: pc3_gen_lift *) @@ -117,43 +117,43 @@ lemma cpcs_flat_dx_tpr_rev: ∀L,V1,V2. V2 ➡ V1 → ∀T1,T2. L ⊢ T1 ⬌* T2 ∀I. L ⊢ ⓕ{I}V1. T1 ⬌* ⓕ{I}V2. T2. /3 width=1/ qed. -lemma cpcs_abst: ∀L,V1,V2. L ⊢ V1 ⬌* V2 → - ∀V,T1,T2. L.ⓛV ⊢ T1 ⬌* T2 → L ⊢ ⓛV1. T1 ⬌* ⓛV2. T2. -#L #V1 #V2 #HV12 #V #T1 #T2 #HT12 +lemma cpcs_abst: ∀a,L,V1,V2. L ⊢ V1 ⬌* V2 → + ∀V,T1,T2. L.ⓛV ⊢ T1 ⬌* T2 → L ⊢ ⓛ{a}V1. T1 ⬌* ⓛ{a}V2. T2. +#a #L #V1 #V2 #HV12 #V #T1 #T2 #HT12 elim (cpcs_inv_cprs … HV12) -HV12 elim (cpcs_inv_cprs … HT12) -HT12 /3 width=6 by cprs_div, cprs_abst/ (**) (* /3 width=6/ is a bit slow *) qed. -lemma cpcs_abbr_dx: ∀L,V,T1,T2. L.ⓓV ⊢ T1 ⬌* T2 → L ⊢ ⓓV. T1 ⬌* ⓓV. T2. -#L #V #T1 #T2 #HT12 +lemma cpcs_abbr_dx: ∀a,L,V,T1,T2. L.ⓓV ⊢ T1 ⬌* T2 → L ⊢ ⓓ{a}V. T1 ⬌* ⓓ{a}V. T2. +#a #L #V #T1 #T2 #HT12 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_bind_dx: ∀a,I,L,V,T1,T2. L.ⓑ{I}V ⊢ T1 ⬌* T2 → + L ⊢ ⓑ{a,I}V. T1 ⬌* ⓑ{a,I}V. T2. +#a * /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 +lemma cpcs_abbr_sn: ∀a,L,V1,V2,T. L ⊢ V1 ⬌* V2 → L ⊢ ⓓ{a}V1. T ⬌* ⓓ{a}V2. T. +#a #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 *) qed. -lemma cpcs_bind_sn: ∀I,L,V1,V2,T. L ⊢ V1 ⬌* V2 → L ⊢ ⓑ{I}V1. T ⬌* ⓑ{I}V2. T. -* /2 width=1/ /2 width=2/ qed. +lemma cpcs_bind_sn: ∀a,I,L,V1,V2,T. L ⊢ V1 ⬌* V2 → L ⊢ ⓑ{a,I}V1. T ⬌* ⓑ{a,I}V2. T. +#a * /2 width=1/ /2 width=2/ qed. -lemma cpcs_beta_dx: ∀L,V1,V2,W,T1,T2. - L ⊢ V1 ➡ V2 → L.ⓛW ⊢ T1 ⬌* T2 → L ⊢ ⓐV1.ⓛW.T1 ⬌* ⓓV2.T2. -#L #V1 #V2 #W #T1 #T2 #HV12 #HT12 +lemma cpcs_beta_dx: ∀a,L,V1,V2,W,T1,T2. + L ⊢ V1 ➡ V2 → L.ⓛW ⊢ T1 ⬌* T2 → L ⊢ ⓐV1.ⓛ{a}W.T1 ⬌* ⓓ{a}V2.T2. +#a #L #V1 #V2 #W #T1 #T2 #HV12 #HT12 elim (cpcs_inv_cprs … HT12) -HT12 #T #HT1 #HT2 -lapply (cprs_beta_dx … HV12 HT1) -HV12 -HT1 #HT1 +lapply (cprs_beta_dx … HV12 HT1 a) -HV12 -HT1 #HT1 lapply (cprs_lsubs_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2 @(cprs_div … HT1) /2 width=1/ qed. -lemma cpcs_beta_dx_tpr_rev: ∀L,V1,V2,W,T1,T2. +lemma cpcs_beta_dx_tpr_rev: ∀a,L,V1,V2,W,T1,T2. V1 ➡ V2 → L.ⓛW ⊢ T2 ⬌* T1 → - L ⊢ ⓓV2.T2 ⬌* ⓐV1.ⓛW.T1. + L ⊢ ⓓ{a}V2.T2 ⬌* ⓐV1.ⓛ{a}W.T1. /4 width=1/ qed. (* Note: it does not hold replacing |L1| with |L2| *) @@ -192,14 +192,14 @@ theorem cpcs_canc_sn: ∀L,T,T1,T2. L ⊢ T ⬌* T1 → L ⊢ T ⬌* T2 → L theorem cpcs_canc_dx: ∀L,T,T1,T2. L ⊢ T1 ⬌* T → L ⊢ T2 ⬌* T → L ⊢ T1 ⬌* T2. /3 width=3 by cpcs_trans, cprs_comm/ qed. (**) (* /3 width=3/ is too slow *) -lemma cpcs_abbr1: ∀L,V1,V2. L ⊢ V1 ⬌* V2 → ∀T1,T2. L.ⓓV1 ⊢ T1 ⬌* T2 → - L ⊢ ⓓV1. T1 ⬌* ⓓV2. T2. -#L #V1 #V2 #HV12 #T1 #T2 #HT12 -@(cpcs_trans … (ⓓV1.T2)) /2 width=1/ +lemma cpcs_abbr1: ∀a,L,V1,V2. L ⊢ V1 ⬌* V2 → ∀T1,T2. L.ⓓV1 ⊢ T1 ⬌* T2 → + L ⊢ ⓓ{a}V1. T1 ⬌* ⓓ{a}V2. T2. +#a #L #V1 #V2 #HV12 #T1 #T2 #HT12 +@(cpcs_trans … (ⓓ{a}V1.T2)) /2 width=1/ qed. -lemma cpcs_abbr2: ∀L,V1,V2. L ⊢ V1 ⬌* V2 → ∀T1,T2. L.ⓓV2 ⊢ T1 ⬌* T2 → - L ⊢ ⓓV1. T1 ⬌* ⓓV2. T2. -#L #V1 #V2 #HV12 #T1 #T2 #HT12 -@(cpcs_trans … (ⓓV2.T1)) /2 width=1/ +lemma cpcs_abbr2: ∀a,L,V1,V2. L ⊢ V1 ⬌* V2 → ∀T1,T2. L.ⓓV2 ⊢ T1 ⬌* T2 → + L ⊢ ⓓ{a}V1. T1 ⬌* ⓓ{a}V2. T2. +#a #L #V1 #V2 #HV12 #T1 #T2 #HT12 +@(cpcs_trans … (ⓓ{a}V2.T1)) /2 width=1/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_delift.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_delift.ma index e6638ea3f..810083108 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_delift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_delift.ma @@ -20,25 +20,25 @@ include "basic_2/equivalence/cpcs_cpcs.ma". (* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************) (* Advanced inversion lemmas ************************************************) - -lemma cprs_inv_appl1_cpcs: ∀L,V1,T1,U2. L ⊢ ⓐV1. T1 ➡* U2 → ( - ∃∃V2,T2. L ⊢ V1 ➡* V2 & L ⊢ T1 ➡* T2 & - L ⊢ U2 ➡* ⓐV2. T2 +(* does not holds +axiom cprs_inv_appl1_cpcs: ∀L,V1,T1,U2. L ⊢ ⓐV1. T1 ➡* U2 → ( + ∃∃V2,T2. L ⊢ V1 ➡* V2 & L ⊢ T1 ➡* T2 & + L ⊢ U2 ➡* ⓐV2. T2 ) ∨ - ∃∃V2,W,T. L ⊢ V1 ➡* V2 & - L ⊢ T1 ➡* ⓛW. T & L ⊢ ⓓV2. T ⬌* U2. + ∃∃a,V2,W,T. L ⊢ V1 ➡* V2 & + L ⊢ T1 ➡* ⓛ{a}W. T & L ⊢ ⓓ{a}V2. T ⬌* U2. #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/ #U #U2 #_ #HU2 * * [ #V0 #T0 #HV10 #HT10 #HUT0 elim (cprs_strip … HUT0 … HU2) -U #U #H #HU2 elim (cpr_inv_appl1 … H) -H * [ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5/ - | #V2 #W2 #T #T2 #HV02 #HT2 #H1 #H2 destruct + | #b #V2 #W2 #T #T2 #HV02 #HT2 #H1 #H2 destruct lapply (cprs_strap1 … HV10 HV02) -V0 #HV12 - lapply (cprs_div ? (ⓓV2.T) ? ? ? HU2) -HU2 /2 width=1/ /3 width=6/ - | #V #V2 #W0 #W2 #T #T2 #HV0 #HW02 #HT2 #HV2 #H1 #H2 destruct + lapply (cprs_div ? (ⓓ{b}V2.T) ? ? ? HU2) -HU2 /2 width=1/ /3 width=7/ + | #b #V #V2 #W0 #W2 #T #T2 #HV0 #HW02 #HT2 #HV2 #H1 #H2 destruct lapply (cprs_strap1 … HV10 HV0) -V0 #HV1 - lapply (cprs_trans … HT10 (ⓓW2.T2) ?) -HT10 /2 width=1/ -W0 -T #HT1 + lapply (cprs_trans … HT10 (ⓓ{b}W2.T2) ?) -HT10 /2 width=1/ -W0 -T #HT1 elim (sfr_delift (L.ⓓW2) (ⓐV2.T2) 0 1 ? ?) // #X #H1 lapply (cprs_zeta_delift … H1) #H2 lapply (cprs_trans … HU2 … H2) -HU2 -H2 #HU2T3 @@ -50,8 +50,9 @@ lemma cprs_inv_appl1_cpcs: ∀L,V1,T1,U2. L ⊢ ⓐV1. T1 ➡* U2 → ( | /4 width=8/ ] qed-. - -lemma cprs_inv_appl_abst: ∀L,V,T,W,U. L ⊢ ⓐV.T ➡* ⓛW.U → +*) +(* maybe holds +axiom cprs_inv_appl_abst: ∀L,V,T,W,U. L ⊢ ⓐV.T ➡* ⓛW.U → ∃∃W0,T0,V1,T1. L ⊢ T ➡* ⓛW0.T0 & L ⊢ ⓓV.T0 ➡* ⓛV1.T1 & L ⊢ ⓛW.U ➡* ⓛV1.T1. @@ -64,11 +65,11 @@ elim (cprs_inv_appl1_cpcs … H) -H * lapply (cprs_trans … (ⓓV.T0) … H1) -H1 /2 width=1/ -V0 /2 width=7/ ] qed-. - +*) (* Properties on inverse basic term relocation ******************************) lemma cpcs_zeta_delift_comm: ∀L,V,T1,T2. L.ⓓV ⊢ ▼*[O, 1] T1 ≡ T2 → - L ⊢ T2 ⬌* ⓓV.T1. + L ⊢ T2 ⬌* +ⓓV.T1. /3 width=1/ qed. (* Basic_1: was only: pc3_gen_cabbr *) diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/sstas/sstas.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/sstas/sstas.etc new file mode 100644 index 000000000..5954145d9 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/sstas/sstas.etc @@ -0,0 +1,110 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 •* break [ g ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'StaticTypeStar $h $g $L $T1 $T2 }. + +include "basic_2/static/ssta.ma". + +(* ITERATED STRATIFIED STATIC TYPE ASSIGNMENTON TERMS ***********************) + +inductive sstas (h:sh) (g:sd h) (L:lenv): relation term ≝ +| sstas_refl: ∀T,U. ⦃h, L⦄ ⊢ T •[g, 0] U → sstas h g L T T +| sstas_step: ∀T,U1,U2,l. ⦃h, L⦄ ⊢ T •[g, l+1] U1 → sstas h g L U1 U2 → + sstas h g L T U2. + +interpretation "stratified unwind (term)" + 'StaticTypeStar h g L T U = (sstas h g L T U). + +(* Basic eliminators ********************************************************) + +fact sstas_ind_alt_aux: ∀h,g,L,U2. ∀R:predicate term. + (∀T. ⦃h, L⦄ ⊢ U2 •[g , 0] T → R U2) → + (∀T,U1,l. ⦃h, L⦄ ⊢ T •[g, l + 1] U1 → + ⦃h, L⦄ ⊢ U1 •* [g] U2 → R U1 → R T + ) → + ∀T,U. ⦃h, L⦄ ⊢ T •*[g] U → U = U2 → R T. +#h #g #L #U2 #R #H1 #H2 #T #U #H elim H -H -T -U /2 width=2/ /3 width=5/ +qed-. + +lemma sstas_ind_alt: ∀h,g,L,U2. ∀R:predicate term. + (∀T. ⦃h, L⦄ ⊢ U2 •[g , 0] T → R U2) → + (∀T,U1,l. ⦃h, L⦄ ⊢ T •[g, l + 1] U1 → + ⦃h, L⦄ ⊢ U1 •* [g] U2 → R U1 → R T + ) → + ∀T. ⦃h, L⦄ ⊢ T •*[g] U2 → R T. +/3 width=9 by sstas_ind_alt_aux/ qed-. + +(* Basic inversion lemmas ***************************************************) + +fact sstas_inv_sort1_aux: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U → ∀k. T = ⋆k → + ∀l. deg h g k l → U = ⋆((next h)^l k). +#h #g #L #T #U #H @(sstas_ind_alt … H) -T +[ #U0 #HU0 #k #H #l #Hkl destruct + elim (ssta_inv_sort1 … HU0) -L #HkO #_ -U0 + >(deg_mono … Hkl HkO) -g -l // +| #T0 #U0 #l0 #HTU0 #_ #IHU0 #k #H #l #Hkl destruct + elim (ssta_inv_sort1 … HTU0) -L #HkS #H destruct + lapply (deg_mono … Hkl HkS) -Hkl #H destruct + >(IHU0 (next h k) ? l0) -IHU0 // /2 width=1/ >iter_SO >iter_n_Sm // +] +qed. + +lemma sstas_inv_sort1: ∀h,g,L,U,k. ⦃h, L⦄ ⊢ ⋆k •*[g] U → ∀l. deg h g k l → + U = ⋆((next h)^l k). +/2 width=6/ qed-. + +fact sstas_inv_bind1_aux: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U → + ∀J,X,Y. T = ⓑ{J}Y.X → + ∃∃Z. ⦃h, L.ⓑ{J}Y⦄ ⊢ X •*[g] Z & U = ⓑ{J}Y.Z. +#h #g #L #T #U #H @(sstas_ind_alt … H) -T +[ #U0 #HU0 #J #X #Y #H destruct + elim (ssta_inv_bind1 … HU0) -HU0 #X0 #HX0 #H destruct /3 width=3/ +| #T0 #U0 #l #HTU0 #_ #IHU0 #J #X #Y #H destruct + elim (ssta_inv_bind1 … HTU0) -HTU0 #X0 #HX0 #H destruct + elim (IHU0 J X0 Y ?) -IHU0 // #X1 #HX01 #H destruct /3 width=4/ +] +qed. + +lemma sstas_inv_bind1: ∀h,g,J,L,Y,X,U. ⦃h, L⦄ ⊢ ⓑ{J}Y.X •*[g] U → + ∃∃Z. ⦃h, L.ⓑ{J}Y⦄ ⊢ X •*[g] Z & U = ⓑ{J}Y.Z. +/2 width=3/ qed-. + +fact sstas_inv_appl1_aux: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U → ∀X,Y. T = ⓐY.X → + ∃∃Z. ⦃h, L⦄ ⊢ X •*[g] Z & U = ⓐY.Z. +#h #g #L #T #U #H @(sstas_ind_alt … H) -T +[ #U0 #HU0 #X #Y #H destruct + elim (ssta_inv_appl1 … HU0) -HU0 #X0 #HX0 #H destruct /3 width=3/ +| #T0 #U0 #l #HTU0 #_ #IHU0 #X #Y #H destruct + elim (ssta_inv_appl1 … HTU0) -HTU0 #X0 #HX0 #H destruct + elim (IHU0 X0 Y ?) -IHU0 // #X1 #HX01 #H destruct /3 width=4/ +] +qed. + +lemma sstas_inv_appl1: ∀h,g,L,Y,X,U. ⦃h, L⦄ ⊢ ⓐY.X •*[g] U → + ∃∃Z. ⦃h, L⦄ ⊢ X •*[g] Z & U = ⓐY.Z. +/2 width=3/ qed-. + +(* Basic forward lemmas *****************************************************) + +lemma sstas_fwd_correct: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U → + ∃∃W. ⦃h, L⦄ ⊢ U •[g, 0] W & ⦃h, L⦄ ⊢ U •*[g] U. +#h #g #L #T #U #H @(sstas_ind_alt … H) -T /2 width=1/ /3 width=2/ +qed-. + +(* Basic_1: removed theorems 7: + sty1_bind sty1_abbr sty1_appl sty1_cast2 + sty1_lift sty1_correct sty1_trans +*) diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/sstas/sstas_lift.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/sstas/sstas_lift.etc new file mode 100644 index 000000000..838c7b6d4 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/sstas/sstas_lift.etc @@ -0,0 +1,57 @@ +(**************************************************************************) +(* ___ *) +(* ||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/ssta_lift.ma". +include "basic_2/unwind/sstas.ma". + +(* ITERATED STRATIFIED STATIC TYPE ASSIGNMENTON TERMS ***********************) + +(* Advanced properties ******************************************************) + +lemma sstas_total_S: ∀h,g,L,l,T,U. ⦃h, L⦄ ⊢ T•[g, l + 1]U → + ∃∃W. ⦃h, L⦄ ⊢ T •*[g] W & ⦃h, L⦄ ⊢ U •*[g] W. +#h #g #L #l @(nat_ind_plus … l) -l +[ #T #U #HTU + elim (ssta_fwd_correct … HTU) /4 width=4/ +| #l #IHl #T #U #HTU + elim (ssta_fwd_correct … HTU) (lift_mono … HX … HU12) -X + elim (lift_total T1 d e) /3 width=10/ +| #T0 #U0 #l0 #HTU0 #_ #IHU01 #L2 #d #e #HL21 #T2 #HT02 #U2 #HU12 + elim (lift_total U0 d e) /3 width=10/ +] +qed. + +lemma sstas_inv_lift1: ∀h,g,L2,T2,U2. ⦃h, L2⦄ ⊢ T2 •*[g] U2 → + ∀L1,d,e. ⇩[d, e] L2 ≡ L1 → ∀T1. ⇧[d, e] T1 ≡ T2 → + ∃∃U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 & ⇧[d, e] U1 ≡ U2. +#h #g #L2 #T2 #U2 #H @(sstas_ind_alt … H) -T2 +[ #T2 #HUT2 #L1 #d #e #HL21 #U1 #HU12 + elim (ssta_inv_lift1 … HUT2 … HL21 … HU12) -HUT2 -HL21 /3 width=3/ +| #T0 #U0 #l0 #HTU0 #_ #IHU01 #L1 #d #e #HL21 #U1 #HU12 + elim (ssta_inv_lift1 … HTU0 … HL21 … HU12) -HTU0 -HU12 #U #HU1 #HU0 + elim (IHU01 … HL21 … HU0) -IHU01 -HL21 -U0 /3 width=4/ +] +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/sstas/sstas_ltpss.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/sstas/sstas_ltpss.etc new file mode 100644 index 000000000..e0aa94207 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/sstas/sstas_ltpss.etc @@ -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/static/ssta_ltpss.ma". +include "basic_2/unwind/sstas.ma". + +(* ITERATED STRATIFIED STATIC TYPE ASSIGNMENTON TERMS ***********************) + +(* Properties about parallel unfold *****************************************) + +lemma sstas_ltpss_tpss_conf: ∀h,g,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 → + ∀L2,d,e. L1 ▶* [d, e] L2 → + ∀T2. L2 ⊢ T1 ▶* [d, e] T2 → + ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*[g] U2 & + L2 ⊢ U1 ▶* [d, e] U2. +#h #g #L1 #T1 #U1 #H @(sstas_ind_alt … H) -T1 +[ #T1 #HUT1 #L2 #d #e #HL12 #U2 #HU12 + elim (ssta_ltpss_tpss_conf … HUT1 … HL12 … HU12) -HUT1 -HL12 /3 width=3/ +| #T0 #U0 #l0 #HTU0 #_ #IHU01 #L2 #d #e #HL12 #T #HT0 + elim (ssta_ltpss_tpss_conf … HTU0 … HL12 … HT0) -HTU0 -HT0 #U #HTU #HU0 + elim (IHU01 … HL12 … HU0) -IHU01 -HL12 -U0 /3 width=4/ +] +qed. + +lemma sstas_ltpss_tps_conf: ∀h,g,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 → + ∀L2,d,e. L1 ▶* [d, e] L2 → + ∀T2. L2 ⊢ T1 ▶ [d, e] T2 → + ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*[g] U2 & L2 ⊢ U1 ▶* [d, e] U2. +/3 width=5/ qed. + +lemma sstas_ltpss_conf: ∀h,g,L1,T,U1. ⦃h, L1⦄ ⊢ T •*[g] U1 → + ∀L2,d,e. L1 ▶* [d, e] L2 → + ∃∃U2. ⦃h, L2⦄ ⊢ T •*[g] U2 & L2 ⊢ U1 ▶* [d, e] U2. +/2 width=5/ qed. + +lemma sstas_tpss_conf: ∀h,g,L,T1,U1. ⦃h, L⦄ ⊢ T1 •*[g] U1 → + ∀T2,d,e. L ⊢ T1 ▶* [d, e] T2 → + ∃∃U2. ⦃h, L⦄ ⊢ T2 •*[g] U2 & L ⊢ U1 ▶* [d, e] U2. +/2 width=5/ qed. + +lemma sstas_tps_conf: ∀h,g,L,T1,U1. ⦃h, L⦄ ⊢ T1 •*[g] U1 → + ∀T2,d,e. L ⊢ T1 ▶ [d, e] T2 → + ∃∃U2. ⦃h, L⦄ ⊢ T2 •*[g] U2 & L ⊢ U1 ▶* [d, e] U2. +/2 width=5/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/sstas/sstas_sstas.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/sstas/sstas_sstas.etc new file mode 100644 index 000000000..2f7e261b4 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/sstas/sstas_sstas.etc @@ -0,0 +1,74 @@ +(**************************************************************************) +(* ___ *) +(* ||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". +include "basic_2/static/ssta_ssta.ma". +include "basic_2/unwind/sstas_lift.ma". + +(* ITERATED STRATIFIED STATIC TYPE ASSIGNMENTON TERMS ***********************) + +(* Advanced inversion lemmas ************************************************) + +lemma sstas_inv_O: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U → + ∀T0. ⦃h, L⦄ ⊢ T •[g , 0] T0 → U = T. +#h #g #L #T #U #H @(sstas_ind_alt … H) -T // +#T0 #U0 #l0 #HTU0 #_ #_ #T1 #HT01 +elim (ssta_mono … HTU0 … HT01) (sstas_inv_O … HU12 … HUT1) -h -L -T1 -U2 // +| #T0 #U0 #l0 #HTU0 #_ #IHU01 #U2 #HU12 + lapply (sstas_inv_S … HU12 … HTU0) -T0 -l0 /2 width=1/ +] +qed-. + +(* More advancd inversion lemmas ********************************************) + +fact sstas_inv_lref1_aux: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U → ∀j. T = #j → + ∃∃I,K,V,W. ⇩[0, j] L ≡ K. ⓑ{I}V & ⦃h, K⦄ ⊢ V •*[g] W & + L ⊢ ▼*[0, j + 1] U ≡ W. +#h #g #L #T #U #H @(sstas_ind_alt … H) -T +[ #T #HUT #j #H destruct + elim (ssta_inv_lref1 … HUT) -HUT * #K #V #W [2: #l] #HLK #HVW #HVT + [ (sstas_mono … HWX … HWT) -X -W /3 width=7/ + ] +] +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 ea82bde3c..319569fe5 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 @@ -18,7 +18,7 @@ include "basic_2/grammar/lenv.ma". let rec shift L T on L ≝ match L with [ LAtom ⇒ T -| LPair L I V ⇒ shift L (ⓑ{I} V. T) +| LPair L I V ⇒ shift L (-ⓑ{I} V. T) ]. interpretation "shift (closure)" 'Append L T = (shift L T). diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_weight.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_weight.ma index 69f76386b..f5f7feb7f 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_weight.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_weight.ma @@ -31,7 +31,7 @@ axiom cw_wf_ind: ∀R:lenv→predicate term. ∀L,T. R L T. (* Basic_1: was: flt_shift *) -lemma cw_shift: ∀K,I,V,T. #[K. ⓑ{I} V, T] < #[K, ②{I} V. T]. +lemma cw_shift: ∀a,K,I,V,T. #[K. ⓑ{I} V, T] < #[K, ⓑ{a,I} V. T]. normalize // qed. @@ -53,8 +53,8 @@ lemma cw_tpair_dx_sn: ∀I1,I2,L,V1,V2,T. #[L, V2] < #[L, ②{I1}V1.②{I2}V2.T] #I1 #I2 #L #V1 #V2 #T normalize in ⊢ (? % %); /2 width=1/ qed. -lemma cw_tpair_dx_sn_shift: ∀I1,I2,L,V1,V2,T. #[L.ⓑ{I2}V2, T] < #[L, ②{I1}V1.②{I2}V2.T]. -#I1 #I2 #L #V1 #V2 #T normalize in ⊢ (? % %); /2 width=1/ +lemma cw_tpair_dx_sn_shift: ∀a2,I1,I2,L,V1,V2,T. #[L.ⓑ{I2}V2, T] < #[L, ②{I1}V1.ⓑ{a2,I2}V2.T]. +#a2 #I1 #I2 #L #V1 #V2 #T normalize in ⊢ (? % %); /2 width=1/ qed. (* Basic_1: removed theorems 6: diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/item.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/item.ma index deeaf047f..323f22f88 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/item.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/item.ma @@ -38,14 +38,10 @@ inductive flat2: Type[0] ≝ (* binary items *) inductive item2: Type[0] ≝ - | Bind2: bind2 → item2 (* binding item *) - | Flat2: flat2 → item2 (* non-binding item *) + | Bind2: bool → bind2 → item2 (* polarized binding item *) + | Flat2: flat2 → item2 (* non-binding item *) . -coercion Bind2. - -coercion Flat2. - (* Basic properties *********************************************************) axiom item0_eq_dec: ∀I1,I2:item0. Decidable (I1 = I2). diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/term.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/term.ma index 0cfa1b024..5ccb5e4ac 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/term.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/term.ma @@ -29,7 +29,13 @@ interpretation "term construction (binary)" 'SnItem2 I T1 T2 = (TPair I T1 T2). interpretation "term binding construction (binary)" - 'SnBind2 I T1 T2 = (TPair (Bind2 I) T1 T2). + 'SnBind2 a I T1 T2 = (TPair (Bind2 a I) T1 T2). + +interpretation "term positive binding construction (binary)" + 'SnBind2Pos I T1 T2 = (TPair (Bind2 true I) T1 T2). + +interpretation "term negative binding construction (binary)" + 'SnBind2Neg I T1 T2 = (TPair (Bind2 false I) T1 T2). interpretation "term flat construction (binary)" 'SnFlat2 I T1 T2 = (TPair (Flat2 I) T1 T2). @@ -44,10 +50,22 @@ interpretation "global reference (term)" 'GRef p = (TAtom (GRef p)). interpretation "abbreviation (term)" - 'SnAbbr T1 T2 = (TPair (Bind2 Abbr) T1 T2). + 'SnAbbr a T1 T2 = (TPair (Bind2 a Abbr) T1 T2). + +interpretation "positive abbreviation (term)" + 'SnAbbrPos T1 T2 = (TPair (Bind2 true Abbr) T1 T2). + +interpretation "negative abbreviation (term)" + 'SnAbbrNeg T1 T2 = (TPair (Bind2 false Abbr) T1 T2). interpretation "abstraction (term)" - 'SnAbst T1 T2 = (TPair (Bind2 Abst) T1 T2). + 'SnAbst a T1 T2 = (TPair (Bind2 a Abst) T1 T2). + +interpretation "positive abstraction (term)" + 'SnAbstPos T1 T2 = (TPair (Bind2 true Abst) T1 T2). + +interpretation "negative abstraction (term)" + 'SnAbstNeg T1 T2 = (TPair (Bind2 false Abst) T1 T2). interpretation "application (term)" 'SnAppl T1 T2 = (TPair (Flat2 Appl) T1 T2). @@ -97,11 +115,11 @@ elim (term_eq_dec T1 T2) /3 width=1/ #HT12 destruct @or_intror @conj // #HT12 destruct /2 width=1/ qed-. -lemma eq_false_inv_beta: ∀V1,V2,W1,W2,T1,T2. - (ⓐV1. ⓛW1. T1 = ⓐV2. ⓛW2 .T2 →⊥) → +lemma eq_false_inv_beta: ∀a,V1,V2,W1,W2,T1,T2. + (ⓐV1. ⓛ{a}W1. T1 = ⓐV2. ⓛ{a}W2 .T2 → ⊥) → (W1 = W2 → ⊥) ∨ - (W1 = W2 ∧ (ⓓV1. T1 = ⓓV2. T2 → ⊥)). -#V1 #V2 #W1 #W2 #T1 #T2 #H + (W1 = W2 ∧ (ⓓ{a}V1. T1 = ⓓ{a}V2. T2 → ⊥)). +#a #V1 #V2 #W1 #W2 #T1 #T2 #H elim (eq_false_inv_tpair_sn … H) -H [ #HV12 elim (term_eq_dec W1 W2) /3 width=1/ #H destruct @or_intror @conj // #H destruct /2 width=1/ diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/term_simple.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/term_simple.ma index 83aff07c4..328dc55a6 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/term_simple.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/term_simple.ma @@ -24,23 +24,21 @@ inductive simple: predicate term ≝ interpretation "simple (term)" 'Simple T = (simple T). (* Basic inversion lemmas ***************************************************) - -fact simple_inv_bind_aux: ∀T. 𝐒⦃T⦄ → ∀J,W,U. T = ⓑ{J} W. U → ⊥. +(* +lemma mt: ∀R1,R2:Prop. (R1 → R2) → (R2 → ⊥) → R1 → ⊥. +/3 width=1/ qed. +*) +fact simple_inv_bind_aux: ∀T. 𝐒⦃T⦄ → ∀a,J,W,U. T = ⓑ{a,J} W. U → ⊥. #T * -T -[ #I #J #W #U #H destruct -| #I #V #T #J #W #U #H destruct +[ #I #a #J #W #U #H destruct +| #I #V #T #a #J #W #U #H destruct ] qed. -lemma simple_inv_bind: ∀I,V,T. 𝐒⦃ⓑ{I} V. T⦄ → ⊥. -/2 width=6/ qed-. +lemma simple_inv_bind: ∀a,I,V,T. 𝐒⦃ⓑ{a,I} V. T⦄ → ⊥. +/2 width=7/ qed-. (**) (* auto fails if mt is enabled *) lemma simple_inv_pair: ∀I,V,T. 𝐒⦃②{I}V.T⦄ → ∃J. I = Flat2 J. -* /2 width=2/ #I #V #T #H +* /2 width=2/ #a #I #V #T #H elim (simple_inv_bind … H) qed-. - -(* -lemma mt: ∀R1,R2:Prop. (R1 → R2) → (R2 → ⊥) → R1 → ⊥. -/3 width=1/ qed-. -*) diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/term_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/term_vector.ma index 3be7a3839..7169d1af4 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/term_vector.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/term_vector.ma @@ -20,7 +20,7 @@ include "basic_2/grammar/term_simple.ma". let rec applv Vs T on Vs ≝ match Vs with [ nil ⇒ T - | cons hd tl ⇒ ⓐhd. (applv tl T) + | cons hd tl ⇒ ⓐhd. (applv tl T) ]. interpretation "application o vevtor (term)" @@ -28,6 +28,6 @@ interpretation "application o vevtor (term)" (* properties concerning simple terms ***************************************) -lemma applv_simple: ∀T,Vs. 𝐒⦃T⦄ -> 𝐒⦃ⒶVs.T⦄. +lemma applv_simple: ∀T,Vs. 𝐒⦃T⦄ → 𝐒⦃ⒶVs.T⦄. #T * // qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/tshf.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/tshf.ma index 34561ebf6..a8873c18b 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/tshf.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/tshf.ma @@ -18,7 +18,8 @@ include "basic_2/grammar/term_simple.ma". inductive tshf: relation term ≝ | tshf_atom: ∀I. tshf (⓪{I}) (⓪{I}) - | tshf_abst: ∀V1,V2,T1,T2. tshf (ⓛV1. T1) (ⓛV2. T2) + | tshf_abbr: ∀V1,V2,T1,T2. tshf (-ⓓV1. T1) (-ⓓV2. T2) + | tshf_abst: ∀a,V1,V2,T1,T2. tshf (ⓛ{a}V1. T1) (ⓛ{a}V2. T2) | tshf_appl: ∀V1,V2,T1,T2. tshf T1 T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄ → tshf (ⓐV1. T1) (ⓐV2. T2) . @@ -40,8 +41,11 @@ lemma tshf_refl1: ∀T1,T2. T1 ≈ T2 → T1 ≈ T1. lemma simple_tshf_repl_dx: ∀T1,T2. T1 ≈ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄. #T1 #T2 #H elim H -T1 -T2 // -#V1 #V2 #T1 #T2 #H -elim (simple_inv_bind … H) +[ #V1 #V2 #T1 #T2 #H + elim (simple_inv_bind … H) +| #a #V1 #V2 #T1 #T2 #H + elim (simple_inv_bind … H) +] qed. (**) (* remove from index *) lemma simple_tshf_repl_sn: ∀T1,T2. T1 ≈ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄. @@ -49,17 +53,20 @@ lemma simple_tshf_repl_sn: ∀T1,T2. T1 ≈ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄ (* Basic inversion lemmas ***************************************************) -fact tshf_inv_bind1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = ⓑ{I}W1.U1 → - ∃∃W2,U2. I = Abst & T2 = ⓛW2. U2. +fact tshf_inv_bind1_aux: ∀T1,T2. T1 ≈ T2 → ∀a,I,W1,U1. T1 = ⓑ{a,I}W1.U1 → + ∃∃W2,U2. T2 = ⓑ{a,I}W2. U2 & + (Bind2 a I = Bind2 false Abbr ∨ I = Abst). #T1 #T2 * -T1 -T2 -[ #J #I #W1 #U1 #H destruct -| #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct /2 width=3/ -| #V1 #V2 #T1 #T2 #H_ #_ #_ #I #W1 #U1 #H destruct +[ #J #a #I #W1 #U1 #H destruct +| #V1 #V2 #T1 #T2 #a #I #W1 #U1 #H destruct /3 width=3/ +| #b #V1 #V2 #T1 #T2 #a #I #W1 #U1 #H destruct /3 width=3/ +| #V1 #V2 #T1 #T2 #_ #_ #_ #a #I #W1 #U1 #H destruct ] qed. -lemma tshf_inv_bind1: ∀I,W1,U1,T2. ⓑ{I}W1.U1 ≈ T2 → - ∃∃W2,U2. I = Abst & T2 = ⓛW2. U2. +lemma tshf_inv_bind1: ∀a,I,W1,U1,T2. ⓑ{a,I}W1.U1 ≈ T2 → + ∃∃W2,U2. T2 = ⓑ{a,I}W2. U2 & + (Bind2 a I = Bind2 false Abbr ∨ I = Abst). /2 width=5/ qed-. fact tshf_inv_flat1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = ⓕ{I}W1.U1 → @@ -68,6 +75,7 @@ fact tshf_inv_flat1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = ⓕ{I}W1.U1 #T1 #T2 * -T1 -T2 [ #J #I #W1 #U1 #H destruct | #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct +| #a #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct | #V1 #V2 #T1 #T2 #HT12 #HT1 #HT2 #I #W1 #U1 #H destruct /2 width=5/ ] qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc_vector.ma index bd4f877d4..1e35292ef 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc_vector.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc_vector.ma @@ -20,9 +20,9 @@ include "basic_2/grammar/tstc.ma". (* Advanced inversion lemmas ************************************************) (* Basic_1: was only: iso_flats_lref_bind_false iso_flats_flat_bind_false *) -lemma tstc_inv_bind_appls_simple: ∀I,Vs,V2,T1,T2. ⒶVs.T1 ≃ ⓑ{I} V2. T2 → +lemma tstc_inv_bind_appls_simple: ∀a,I,Vs,V2,T1,T2. ⒶVs.T1 ≃ ⓑ{a,I} V2. T2 → 𝐒⦃T1⦄ → ⊥. -#I #Vs #V2 #T1 #T2 #H +#a #I #Vs #V2 #T1 #T2 #H elim (tstc_inv_pair2 … H) -H #V0 #T0 elim Vs -Vs normalize [ #H destruct #H diff --git a/matita/matita/contribs/lambda_delta/basic_2/names.txt b/matita/matita/contribs/lambda_delta/basic_2/names.txt index 1a4b33044..6c34328b4 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/names.txt +++ b/matita/matita/contribs/lambda_delta/basic_2/names.txt @@ -9,14 +9,13 @@ IH : reserved: inductive premise I,J : item K,L : local environment M,N : reserved: future use -O : -P,Q : reserved: future use (lambda_delta 4) +O,P,Q : R : generic predicate (relation) S : RTM stack T,U,V,W: term X,Y,Z : reserved: transient objet denoted by a capital letter -a,b : reserved: future use (lambda_delta 4) +a,b : binder polarity c : reserved: future use (lambda_delta 3) d : relocation depth e : relocation height diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma index 509e6a7e8..d6d38ef61 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/notation.ma @@ -48,21 +48,45 @@ notation "hvbox( ② { I } break term 55 T1 . break term 55 T )" non associative with precedence 55 for @{ 'SnItem2 $I $T1 $T }. -notation "hvbox( ⓑ { I } break term 55 T1 . break term 55 T )" +notation "hvbox( ⓑ { a , I } break term 55 T1 . break term 55 T )" non associative with precedence 55 - for @{ 'SnBind2 $I $T1 $T }. + for @{ 'SnBind2 $a $I $T1 $T }. + +notation "hvbox( + ⓑ { I } break term 55 T1 . break term 55 T )" + non associative with precedence 55 + for @{ 'SnBind2Pos $I $T1 $T }. + +notation "hvbox( - ⓑ { I } break term 55 T1 . break term 55 T )" + non associative with precedence 55 + for @{ 'SnBind2Neg $I $T1 $T }. notation "hvbox( ⓕ { I } break term 55 T1 . break term 55 T )" non associative with precedence 55 for @{ 'SnFlat2 $I $T1 $T }. -notation "hvbox( ⓓ term 55 T1 . break term 55 T2 )" +notation "hvbox( ⓓ { a } term 55 T1 . break term 55 T2 )" + non associative with precedence 55 + for @{ 'SnAbbr $a $T1 $T2 }. + +notation "hvbox( + ⓓ term 55 T1 . break term 55 T2 )" + non associative with precedence 55 + for @{ 'SnAbbrPos $T1 $T2 }. + +notation "hvbox( - ⓓ term 55 T1 . break term 55 T2 )" non associative with precedence 55 - for @{ 'SnAbbr $T1 $T2 }. + for @{ 'SnAbbrNeg $T1 $T2 }. -notation "hvbox( ⓛ term 55 T1 . break term 55 T2 )" +notation "hvbox( ⓛ { a } term 55 T1 . break term 55 T2 )" non associative with precedence 55 - for @{ 'SnAbst $T1 $T2 }. + for @{ 'SnAbst $a $T1 $T2 }. + +notation "hvbox( + ⓛ term 55 T1 . break term 55 T2 )" + non associative with precedence 55 + for @{ 'SnAbstPos $T1 $T2 }. + +notation "hvbox( - ⓛ term 55 T1 . break term 55 T2 )" + non associative with precedence 55 + for @{ 'SnAbstNeg $T1 $T2 }. notation "hvbox( ⓐ term 55 T1 . break term 55 T2 )" non associative with precedence 55 @@ -232,9 +256,9 @@ notation "hvbox( h ⊢ break term 46 L1 • ⊑ [ g ] break term 46 L2 )" (* Unwind *******************************************************************) -notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 •* break [ g ] break term 46 T2 )" +notation "hvbox( L1 ⊢ ⧫* break term 46 T ≡ break term 46 L2 )" non associative with precedence 45 - for @{ 'StaticTypeStar $h $g $L $T1 $T2 }. + for @{ 'Unwind $L1 $T $L2 }. (* Reducibility *************************************************************) @@ -298,6 +322,14 @@ 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 }. + +notation "hvbox( ⦃ L1, break T1 ⦄ ➡ break ⦃ L2 , break T2 ⦄ )" + non associative with precedence 45 + for @{ 'FocalizedPRed $L1 $T1 $L2 $T2 }. + notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 ➸ break [ g ] break term 46 T2 )" non associative with precedence 45 for @{ 'XPRed $h $g $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.ma index ecb32ceed..6c980e7bf 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.ma @@ -36,8 +36,8 @@ lapply (ldrop_mono … HLK … HLK0) -L #H destruct qed. (* Basic_1: was: nf2_abst *) -lemma cnf_abst: ∀I,L,V,W,T. L ⊢ 𝐍⦃W⦄ → L. ⓑ{I} V ⊢ 𝐍⦃T⦄ → L ⊢ 𝐍⦃ⓛW.T⦄. -#I #L #V #W #T #HW #HT #X #H +lemma cnf_abst: ∀a,I,L,V,W,T. L ⊢ 𝐍⦃W⦄ → L. ⓑ{I} V ⊢ 𝐍⦃T⦄ → L ⊢ 𝐍⦃ⓛ{a}W.T⦄. +#a #I #L #V #W #T #HW #HT #X #H elim (cpr_inv_abst1 … H I V) -H #W0 #T0 #HW0 #HT0 #H destruct >(HW … HW0) -W0 >(HT … HT0) -T0 // qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_cpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_cpr.ma index 87eaa161f..8d2eb1f1d 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_cpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_cpr.ma @@ -19,16 +19,16 @@ include "basic_2/reducibility/cpr.ma". (* Advanced properties ******************************************************) -lemma cpr_bind_sn: ∀I,L,V1,V2,T1,T2. L ⊢ V1 ➡ V2 → T1 ➡ T2 → - L ⊢ ⓑ{I} V1. T1 ➡ ⓑ{I} V2. T2. -#I #L #V1 #V2 #T1 #T2 * #V #HV1 #HV2 #HT12 +lemma cpr_bind_sn: ∀a,I,L,V1,V2,T1,T2. L ⊢ V1 ➡ V2 → T1 ➡ T2 → + L ⊢ ⓑ{a,I} V1. T1 ➡ ⓑ{a,I} V2. T2. +#a #I #L #V1 #V2 #T1 #T2 * #V #HV1 #HV2 #HT12 @ex2_1_intro [2: @(tpr_delta … HV1 HT12) | skip ] /2 width=3/ (* /3 width=5/ is too slow *) qed. (* Basic_1: was only: pr2_gen_cbind *) -lemma cpr_bind_dx: ∀I,L,V1,V2,T1,T2. V1 ➡ V2 → L. ⓑ{I} V2 ⊢ T1 ➡ T2 → - L ⊢ ⓑ{I} V1. T1 ➡ ⓑ{I} V2. T2. -#I #L #V1 #V2 #T1 #T2 #HV12 * #T #HT1 normalize #HT2 +lemma cpr_bind_dx: ∀a,I,L,V1,V2,T1,T2. V1 ➡ V2 → L. ⓑ{I} V2 ⊢ T1 ➡ T2 → + L ⊢ ⓑ{a,I} V1. T1 ➡ ⓑ{a,I} V2. T2. +#a #I #L #V1 #V2 #T1 #T2 #HV12 * #T #HT1 normalize #HT2 elim (tpss_split_up … HT2 1 ? ?) -HT2 // #T0 (lift_mono … HWU1 … HV0U2) -W -U1 /2 width=1/ -| #I #L #V #T #U1 #l1 #_ #IHTU1 #X #l2 #H +| #a #I #L #V #T #U1 #l1 #_ #IHTU1 #X #l2 #H elim (ssta_inv_bind1 … H) -H #U2 #HTU2 #H destruct elim (IHTU1 … HTU2) -T /3 width=1/ | #L #V #T #U1 #l1 #_ #IHTU1 #X #l2 #H diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/lift.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/lift.ma index 622f4ef53..49a453ffa 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/lift.ma @@ -25,9 +25,9 @@ inductive lift: nat → nat → relation term ≝ | lift_lref_lt: ∀i,d,e. i < d → lift d e (#i) (#i) | lift_lref_ge: ∀i,d,e. d ≤ i → lift d e (#i) (#(i + e)) | lift_gref : ∀p,d,e. lift d e (§p) (§p) -| lift_bind : ∀I,V1,V2,T1,T2,d,e. +| lift_bind : ∀a,I,V1,V2,T1,T2,d,e. lift d e V1 V2 → lift (d + 1) e T1 T2 → - lift d e (ⓑ{I} V1. T1) (ⓑ{I} V2. T2) + lift d e (ⓑ{a,I} V1. T1) (ⓑ{a,I} V2. T2) | lift_flat : ∀I,V1,V2,T1,T2,d,e. lift d e V1 V2 → lift d e T1 T2 → lift d e (ⓕ{I} V1. T1) (ⓕ{I} V2. T2) @@ -47,7 +47,7 @@ lemma lift_inv_refl_O2: ∀d,T1,T2. ⇧[d, 0] T1 ≡ T2 → T1 = T2. fact lift_inv_sort1_aux: ∀d,e,T1,T2. ⇧[d,e] T1 ≡ T2 → ∀k. T1 = ⋆k → T2 = ⋆k. #d #e #T1 #T2 * -d -e -T1 -T2 // [ #i #d #e #_ #k #H destruct -| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct +| #a #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct ] qed. @@ -62,7 +62,7 @@ fact lift_inv_lref1_aux: ∀d,e,T1,T2. ⇧[d,e] T1 ≡ T2 → ∀i. T1 = #i → | #j #d #e #Hj #i #Hi destruct /3 width=1/ | #j #d #e #Hj #i #Hi destruct /3 width=1/ | #p #d #e #i #H destruct -| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #i #H destruct +| #a #I #V1 #V2 #T1 #T2 #d #e #_ #_ #i #H destruct | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #i #H destruct ] qed. @@ -86,7 +86,7 @@ qed-. fact lift_inv_gref1_aux: ∀d,e,T1,T2. ⇧[d,e] T1 ≡ T2 → ∀p. T1 = §p → T2 = §p. #d #e #T1 #T2 * -d -e -T1 -T2 // [ #i #d #e #_ #k #H destruct -| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct +| #a #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct ] qed. @@ -95,22 +95,22 @@ lemma lift_inv_gref1: ∀d,e,T2,p. ⇧[d,e] §p ≡ T2 → T2 = §p. /2 width=5/ qed-. fact lift_inv_bind1_aux: ∀d,e,T1,T2. ⇧[d,e] T1 ≡ T2 → - ∀I,V1,U1. T1 = ⓑ{I} V1.U1 → + ∀a,I,V1,U1. T1 = ⓑ{a,I} V1.U1 → ∃∃V2,U2. ⇧[d,e] V1 ≡ V2 & ⇧[d+1,e] U1 ≡ U2 & - T2 = ⓑ{I} V2. U2. + T2 = ⓑ{a,I} V2. U2. #d #e #T1 #T2 * -d -e -T1 -T2 -[ #k #d #e #I #V1 #U1 #H destruct -| #i #d #e #_ #I #V1 #U1 #H destruct -| #i #d #e #_ #I #V1 #U1 #H destruct -| #p #d #e #I #V1 #U1 #H destruct -| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V1 #U1 #H destruct /2 width=5/ -| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V1 #U1 #H destruct +[ #k #d #e #a #I #V1 #U1 #H destruct +| #i #d #e #_ #a #I #V1 #U1 #H destruct +| #i #d #e #_ #a #I #V1 #U1 #H destruct +| #p #d #e #a #I #V1 #U1 #H destruct +| #b #J #W1 #W2 #T1 #T2 #d #e #HW #HT #a #I #V1 #U1 #H destruct /2 width=5/ +| #J #W1 #W2 #T1 #T2 #d #e #_ #HT #a #I #V1 #U1 #H destruct ] qed. -lemma lift_inv_bind1: ∀d,e,T2,I,V1,U1. ⇧[d,e] ⓑ{I} V1. U1 ≡ T2 → +lemma lift_inv_bind1: ∀d,e,T2,a,I,V1,U1. ⇧[d,e] ⓑ{a,I} V1. U1 ≡ T2 → ∃∃V2,U2. ⇧[d,e] V1 ≡ V2 & ⇧[d+1,e] U1 ≡ U2 & - T2 = ⓑ{I} V2. U2. + T2 = ⓑ{a,I} V2. U2. /2 width=3/ qed-. fact lift_inv_flat1_aux: ∀d,e,T1,T2. ⇧[d,e] T1 ≡ T2 → @@ -122,7 +122,7 @@ fact lift_inv_flat1_aux: ∀d,e,T1,T2. ⇧[d,e] T1 ≡ T2 → | #i #d #e #_ #I #V1 #U1 #H destruct | #i #d #e #_ #I #V1 #U1 #H destruct | #p #d #e #I #V1 #U1 #H destruct -| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V1 #U1 #H destruct +| #a #J #W1 #W2 #T1 #T2 #d #e #_ #_ #I #V1 #U1 #H destruct | #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V1 #U1 #H destruct /2 width=5/ ] qed. @@ -135,7 +135,7 @@ lemma lift_inv_flat1: ∀d,e,T2,I,V1,U1. ⇧[d,e] ⓕ{I} V1. U1 ≡ T2 → fact lift_inv_sort2_aux: ∀d,e,T1,T2. ⇧[d,e] T1 ≡ T2 → ∀k. T2 = ⋆k → T1 = ⋆k. #d #e #T1 #T2 * -d -e -T1 -T2 // [ #i #d #e #_ #k #H destruct -| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct +| #a #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct ] qed. @@ -151,7 +151,7 @@ fact lift_inv_lref2_aux: ∀d,e,T1,T2. ⇧[d,e] T1 ≡ T2 → ∀i. T2 = #i → | #j #d #e #Hj #i #Hi destruct /3 width=1/ | #j #d #e #Hj #i #Hi destruct (plus_minus_m_m e2 e1 ?) // /3 width=3/ | /3 width=3/ -| #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12 +| #a #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12 elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b elim (IHT (d2+1) … ? ? He12) /2 width=1/ /3 width=5/ | #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12 @@ -346,7 +346,7 @@ lemma is_lift_dec: ∀T2,d,e. Decidable (∃T1. ⇧[d,e] T1 ≡ T2). | lapply (false_lt_to_le … Hide) -Hide /4 width=2/ ] ] -| * #I #V2 #T2 #IHV2 #IHT2 #d #e +| * [ #a ] #I #V2 #T2 #IHV2 #IHT2 #d #e [ elim (IHV2 d e) -IHV2 [ * #V1 #HV12 elim (IHT2 (d+1) e) -IHT2 [ * #T1 #HT12 @or_introl /3 width=2/ 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 f302b16ad..3e18bff32 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 @@ -29,7 +29,7 @@ theorem lift_inj: ∀d,e,T1,U. ⇧[d,e] T1 ≡ U → ∀T2. ⇧[d,e] T2 ≡ U lapply (lift_inv_lref2_ge … HX ?) -HX // /2 width=1/ | #p #d #e #X #HX lapply (lift_inv_gref2 … HX) -HX // -| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX +| #a #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX elim (lift_inv_bind2 … HX) -HX #V #T #HV1 #HT1 #HX destruct /3 width=1/ | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX elim (lift_inv_flat2 … HX) -HX #V #T #HV1 #HT1 #HX destruct /3 width=1/ @@ -58,7 +58,7 @@ theorem lift_div_le: ∀d1,e1,T1,T. ⇧[d1, e1] T1 ≡ T → ] | #p #d1 #e1 #d2 #e2 #T2 #Hk #Hd12 lapply (lift_inv_gref2 … Hk) -Hk #Hk destruct /3 width=3/ -| #I #W1 #W #U1 #U #d1 #e1 #_ #_ #IHW #IHU #d2 #e2 #T2 #H #Hd12 +| #a #I #W1 #W #U1 #U #d1 #e1 #_ #_ #IHW #IHU #d2 #e2 #T2 #H #Hd12 lapply (lift_inv_bind2 … H) -H * #W2 #U2 #HW2 #HU2 #H destruct elim (IHW … HW2 ?) // -IHW -HW2 #W0 #HW2 #HW1 >plus_plus_comm_23 in HU2; #HU2 elim (IHU … HU2 ?) /2 width=1/ /3 width=5/ @@ -88,7 +88,7 @@ theorem lift_div_be: ∀d1,e1,T1,T. ⇧[d1, e1] T1 ≡ T → @lift_lref_ge_minus_eq [ >plus_minus_commutative // | /2 width=1/ ] ] | #p #d1 #e1 #e #e2 #T2 #H >(lift_inv_gref2 … H) -H /2 width=3/ -| #I #V1 #V #T1 #T #d1 #e1 #_ #_ #IHV1 #IHT1 #e #e2 #X #H #He1 #He1e2 +| #a #I #V1 #V #T1 #T #d1 #e1 #_ #_ #IHV1 #IHT1 #e #e2 #X #H #He1 #He1e2 elim (lift_inv_bind2 … H) -H #V2 #T2 #HV2 #HT2 #H destruct elim (IHV1 … HV2 ? ?) -V // >plus_plus_comm_23 in HT2; #HT2 elim (IHT1 … HT2 ? ?) -T // -He1 -He1e2 /3 width=5/ @@ -109,7 +109,7 @@ theorem lift_mono: ∀d,e,T,U1. ⇧[d,e] T ≡ U1 → ∀U2. ⇧[d,e] T ≡ U2 lapply (lift_inv_lref1_ge … HX ?) -HX // | #p #d #e #X #HX lapply (lift_inv_gref1 … HX) -HX // -| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX +| #a #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX elim (lift_inv_bind1 … HX) -HX #V #T #HV1 #HT1 #HX destruct /3 width=1/ | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX elim (lift_inv_flat1 … HX) -HX #V #T #HV1 #HT1 #HX destruct /3 width=1/ @@ -133,7 +133,7 @@ theorem lift_trans_be: ∀d1,e1,T1,T. ⇧[d1, e1] T1 ≡ T → ] | #p #d1 #e1 #d2 #e2 #T2 #HT2 #_ #_ >(lift_inv_gref1 … HT2) -HT2 // -| #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hd12 #Hd21 +| #a #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hd12 #Hd21 elim (lift_inv_bind1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct lapply (IHV12 … HV20 ? ?) // -IHV12 -HV20 #HV10 lapply (IHT12 … HT20 ? ?) /2 width=1/ @@ -160,7 +160,7 @@ theorem lift_trans_le: ∀d1,e1,T1,T. ⇧[d1, e1] T1 ≡ T → >plus_plus_comm_23 /4 width=3/ | #p #d1 #e1 #d2 #e2 #X #HX #_ >(lift_inv_gref1 … HX) -HX /2 width=3/ -| #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hd21 +| #a #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hd21 elim (lift_inv_bind1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct elim (IHV12 … HV20 ?) -IHV12 -HV20 // elim (IHT12 … HT20 ?) -IHT12 -HT20 /2 width=1/ /3 width=5/ @@ -187,7 +187,7 @@ theorem lift_trans_ge: ∀d1,e1,T1,T. ⇧[d1, e1] T1 ≡ T → elim (lift_inv_lref1 … HX) -HX * #Hied #HX destruct /4 width=3/ | #p #d1 #e1 #d2 #e2 #X #HX #_ >(lift_inv_gref1 … HX) -HX /2 width=3/ -| #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hded +| #a #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hded elim (lift_inv_bind1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct elim (IHV12 … HV20 ?) -IHV12 -HV20 // elim (IHT12 … HT20 ?) -IHT12 -HT20 /2 width=1/ #T diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma index 303604958..88de45dd1 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma @@ -20,9 +20,9 @@ inductive tps: nat → nat → lenv → relation term ≝ | tps_atom : ∀L,I,d,e. tps d e L (⓪{I}) (⓪{I}) | tps_subst: ∀L,K,V,W,i,d,e. d ≤ i → i < d + e → ⇩[0, i] L ≡ K. ⓓV → ⇧[0, i + 1] V ≡ W → tps d e L (#i) W -| tps_bind : ∀L,I,V1,V2,T1,T2,d,e. +| tps_bind : ∀L,a,I,V1,V2,T1,T2,d,e. tps d e L V1 V2 → tps (d + 1) e (L. ⓑ{I} V2) T1 T2 → - tps d e L (ⓑ{I} V1. T1) (ⓑ{I} V2. T2) + tps d e L (ⓑ{a,I} V1. T1) (ⓑ{a,I} V2. T2) | tps_flat : ∀L,I,V1,V2,T1,T2,d,e. tps d e L V1 V2 → tps d e L T1 T2 → tps d e L (ⓕ{I} V1. T1) (ⓕ{I} V2. T2) @@ -58,9 +58,9 @@ lemma tps_full: ∀K,V,T1,L,d. ⇩[0, d] L ≡ (K. ⓓV) → destruct elim (lift_total V 0 (i+1)) #W #HVW elim (lift_split … HVW i i ? ? ?) // /3 width=4/ -| * #I #W1 #U1 #IHW1 #IHU1 #L #d #HLK +| * [ #a ] #I #W1 #U1 #IHW1 #IHU1 #L #d #HLK elim (IHW1 … HLK) -IHW1 #W2 #W #HW12 #HW2 - [ elim (IHU1 (L. ⓑ{I} W2) (d+1) ?) -IHU1 /2 width=1/ -HLK /3 width=8/ + [ elim (IHU1 (L. ⓑ{I} W2) (d+1) ?) -IHU1 /2 width=1/ -HLK /3 width=9/ | elim (IHU1 … HLK) -IHU1 -HLK /3 width=8/ ] ] @@ -110,7 +110,7 @@ lemma tps_split_up: ∀L,T1,T2,d,e. L ⊢ T1 ▶ [d, e] T2 → ∀i. d ≤ i → generalize in match Hide; -Hide (**) (* rewriting in the premises, rewrites in the goal too *) >(plus_minus_m_m … Hjde) in ⊢ (% → ?); -Hjde /4 width=4/ ] -| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #i #Hdi #Hide +| #L #a #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #i #Hdi #Hide elim (IHV12 i ? ?) -IHV12 // #V #HV1 #HV2 elim (IHT12 (i + 1) ? ?) -IHT12 /2 width=1/ -Hdi -Hide >arith_c1x #T #HT1 #HT2 @@ -133,7 +133,7 @@ lemma tps_split_down: ∀L,T1,T2,d,e. L ⊢ T1 ▶ [d, e] T2 → | -Hdi -Hdj >(plus_minus_m_m (d+e) j) in Hide; // -Hjde /3 width=4/ ] -| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #i #Hdi #Hide +| #L #a #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #i #Hdi #Hide elim (IHV12 i ? ?) -IHV12 // #V #HV1 #HV2 elim (IHT12 (i + 1) ? ?) -IHT12 /2 width=1/ -Hdi -Hide >arith_c1x #T #HT1 #HT2 @@ -155,7 +155,7 @@ fact tps_inv_atom1_aux: ∀L,T1,T2,d,e. L ⊢ T1 ▶ [d, e] T2 → ∀I. T1 = #L #T1 #T2 #d #e * -L -T1 -T2 -d -e [ #L #I #d #e #J #H destruct /2 width=1/ | #L #K #V #T2 #i #d #e #Hdi #Hide #HLK #HVT2 #I #H destruct /3 width=8/ -| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #J #H destruct +| #L #a #I #V1 #V2 #T1 #T2 #d #e #_ #_ #J #H destruct | #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #J #H destruct ] qed. @@ -194,22 +194,22 @@ elim (tps_inv_atom1 … H) -H // qed-. fact tps_inv_bind1_aux: ∀d,e,L,U1,U2. L ⊢ U1 ▶ [d, e] U2 → - ∀I,V1,T1. U1 = ⓑ{I} V1. T1 → + ∀a,I,V1,T1. U1 = ⓑ{a,I} V1. T1 → ∃∃V2,T2. L ⊢ V1 ▶ [d, e] V2 & L. ⓑ{I} V2 ⊢ T1 ▶ [d + 1, e] T2 & - U2 = ⓑ{I} V2. T2. + U2 = ⓑ{a,I} V2. T2. #d #e #L #U1 #U2 * -d -e -L -U1 -U2 -[ #L #k #d #e #I #V1 #T1 #H destruct -| #L #K #V #W #i #d #e #_ #_ #_ #_ #I #V1 #T1 #H destruct -| #L #J #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #I #V #T #H destruct /2 width=5/ -| #L #J #V1 #V2 #T1 #T2 #d #e #_ #_ #I #V #T #H destruct +[ #L #k #d #e #a #I #V1 #T1 #H destruct +| #L #K #V #W #i #d #e #_ #_ #_ #_ #a #I #V1 #T1 #H destruct +| #L #b #J #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #a #I #V #T #H destruct /2 width=5/ +| #L #J #V1 #V2 #T1 #T2 #d #e #_ #_ #a #I #V #T #H destruct ] qed. -lemma tps_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ ⓑ{I} V1. T1 ▶ [d, e] U2 → +lemma tps_inv_bind1: ∀d,e,L,a,I,V1,T1,U2. L ⊢ ⓑ{a,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. + U2 = ⓑ{a,I} V2. T2. /2 width=3/ qed-. fact tps_inv_flat1_aux: ∀d,e,L,U1,U2. L ⊢ U1 ▶ [d, e] U2 → @@ -219,7 +219,7 @@ fact tps_inv_flat1_aux: ∀d,e,L,U1,U2. L ⊢ U1 ▶ [d, e] U2 → #d #e #L #U1 #U2 * -d -e -L -U1 -U2 [ #L #k #d #e #I #V1 #T1 #H destruct | #L #K #V #W #i #d #e #_ #_ #_ #_ #I #V1 #T1 #H destruct -| #L #J #V1 #V2 #T1 #T2 #d #e #_ #_ #I #V #T #H destruct +| #L #a #J #V1 #V2 #T1 #T2 #d #e #_ #_ #I #V #T #H destruct | #L #J #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #I #V #T #H destruct /2 width=5/ ] qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/tps_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps_lift.ma index 6f712e8a7..5ffc94922 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/tps_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps_lift.ma @@ -64,7 +64,7 @@ lemma tps_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 ▶ [dt, et] T2 → elim (ldrop_trans_le … HLK … HKV ?) -K /2 width=2/ #X #HLK #H elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K #Y #_ #HVY >(lift_mono … HVY … HVW) -Y -HVW #H destruct /2 width=4/ -| #K #I #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hdetd +| #K #a #I #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hdetd elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct @tps_bind [ /2 width=6/ | @IHT12 /2 width=6/ ] (**) (* /3 width=6/ is too slow, arith3 needed to avoid crash *) @@ -95,7 +95,7 @@ lemma tps_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 ▶ [dt, et] T2 → lapply (lift_trans_be … HVW … HWU2 ? ?) -W // /2 width=1/ >plus_plus_comm_23 #HVU2 lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K // -Hid /3 width=4/ ] -| #K #I #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hdtd #Hddet +| #K #a #I #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hdtd #Hddet elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct @tps_bind [ /2 width=6/ | @IHT12 [3,4: // | skip |5,6: /2 width=1/ | /2 width=1/ ] @@ -120,7 +120,7 @@ lemma tps_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 ▶ [dt, et] T2 → lapply (lift_inv_lref1_ge … H … Hid) -H #H destruct lapply (lift_trans_be … HVW … HWU2 ? ?) -W // /2 width=1/ >plus_plus_comm_23 #HVU2 lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K // -Hid /3 width=4/ -| #K #I #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hddt +| #K #a #I #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hddt elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct @tps_bind [ /2 width=5/ | /3 width=5/ ] (**) (* explicit constructor *) @@ -146,7 +146,7 @@ lemma tps_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 ▶ [dt, et] U2 → lapply (lift_inv_lref2_lt … H … Hid) -H #H destruct elim (ldrop_conf_lt … HLK … HLKV ?) -L // #L #U #HKL #_ #HUV elim (lift_trans_le … HUV … HVW ?) -V // >minus_plus plus_minus // commutative_plus >plus_minus // /2 width=1/ ] ] (**) (* explicit constructor, uses monotonic_lt_minus_l *) ] -| #L #I #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdtd #Hdedet +| #L #a #I #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdtd #Hdedet elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct elim (IHV12 … HLK … HWV1 ? ?) -V1 // #W2 #HW12 #HWV2 elim (IHU12 … HTU1 ? ?) -U1 [5: @ldrop_skip // |2: skip |3: >plus_plus_comm_23 >(plus_plus_comm_23 dt) /2 width=1/ |4: /2 width=1/ ] (**) (* 29s without the rewrites *) @@ -215,7 +215,7 @@ lemma tps_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 ▶ [dt, et] U2 → elim (lift_split … HVW d (i - e + 1) ? ? ?) -HVW [4: // |3: /2 width=1/ |2: /3 width=1/ ] -Hdei -Hdie #V0 #HV10 >plus_minus // plus_minus // /2 width=1/ ] ] (**) (* explicit constructor, uses monotonic_lt_minus_l *) -| #L #I #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdetd +| #L #a #I #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdetd elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct elim (le_inv_plus_l … Hdetd) #_ #Hedt elim (IHV12 … HLK … HWV1 ?) -V1 // #W2 #HW12 #HWV2 @@ -240,7 +240,7 @@ lemma tps_inv_lift1_eq: ∀L,U1,U2,d,e. | lapply (lt_to_le_to_lt … Hide … H) -Hide -H #H elim (lt_refl_false … H) ] -| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX +| #L #a #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX elim (lift_inv_bind2 … HX) -HX #V #T #HV1 #HT1 #H destruct >IHV12 // >IHT12 // | #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/tps_tps.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps_tps.ma index 6bbb15a76..3882750bd 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/tps_tps.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps_tps.ma @@ -31,7 +31,7 @@ theorem tps_conf_eq: ∀L,T0,T1,d1,e1. L ⊢ T0 ▶ [d1, e1] T1 → lapply (ldrop_mono … HLK1 … HLK2) -HLK1 -HLK2 #H destruct >(lift_mono … HVT1 … HVT2) -HVT1 -HVT2 /2 width=3/ ] -| #L #I #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #X #d2 #e2 #HX +| #L #a #I #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #X #d2 #e2 #HX elim (tps_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct lapply (tps_lsubs_trans … HT02 (L. ⓑ{I} V1) ?) -HT02 /2 width=1/ #HT02 elim (IHV01 … HV02) -V0 #V #HV1 #HV2 @@ -66,7 +66,7 @@ theorem tps_conf_neq: ∀L1,T0,T1,d1,e1. L1 ⊢ T0 ▶ [d1, e1] T1 → elim (lt_refl_false … H) ] ] -| #L1 #I #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #L2 #X #d2 #e2 #HX #H +| #L1 #a #I #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #L2 #X #d2 #e2 #HX #H elim (tps_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct elim (IHV01 … HV02 H) -V0 #V #HV1 #HV2 elim (IHT01 … HT02 ?) -T0 @@ -98,7 +98,7 @@ theorem tps_trans_ge: ∀L,T1,T0,d,e. L ⊢ T1 ▶ [d, e] T0 → | #L #K #V #V2 #i #d #e #Hdi #Hide #HLK #HVW #T2 #HVT2 #He lapply (tps_weak … HVT2 0 (i +1) ? ?) -HVT2 /2 width=1/ #HVT2 <(tps_inv_lift1_eq … HVT2 … HVW) -HVT2 /2 width=4/ -| #L #I #V1 #V0 #T1 #T0 #d #e #_ #_ #IHV10 #IHT10 #X #H #He +| #L #a #I #V1 #V0 #T1 #T0 #d #e #_ #_ #IHV10 #IHT10 #X #H #He elim (tps_inv_bind1 … H) -H #V2 #T2 #HV02 #HT02 #H destruct lapply (tps_lsubs_trans … HT02 (L. ⓑ{I} V0) ?) -HT02 /2 width=1/ #HT02 lapply (IHT10 … HT02 He) -T0 #HT12 @@ -117,7 +117,7 @@ theorem tps_trans_down: ∀L,T1,T0,d1,e1. L ⊢ T1 ▶ [d1, e1] T0 → lapply (transitive_le … Hde2d1 Hdi1) -Hde2d1 #Hde2i1 lapply (tps_weak … HWT2 0 (i1 + 1) ? ?) -HWT2 normalize /2 width=1/ -Hde2i1 #HWT2 <(tps_inv_lift1_eq … HWT2 … HVW) -HWT2 /4 width=4/ -| #L #I #V1 #V0 #T1 #T0 #d1 #e1 #_ #_ #IHV10 #IHT10 #X #d2 #e2 #HX #de2d1 +| #L #a #I #V1 #V0 #T1 #T0 #d1 #e1 #_ #_ #IHV10 #IHT10 #X #d2 #e2 #HX #de2d1 elim (tps_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct lapply (tps_lsubs_trans … HT02 (L. ⓑ{I} V0) ?) -HT02 /2 width=1/ #HT02 elim (IHV10 … HV02 ?) -IHV10 -HV02 // #V 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 3c9ecc3ca..1af082f28 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma @@ -48,10 +48,10 @@ lemma delift_lref_ge: ∀L,d,e,i. d + e ≤ i → L ⊢ ▼*[d, e] #i ≡ #(i - lemma delift_gref: ∀L,d,e,p. L ⊢ ▼*[d, e] §p ≡ §p. /2 width=3/ qed. -lemma delift_bind: ∀I,L,V1,V2,T1,T2,d,e. +lemma delift_bind: ∀a,I,L,V1,V2,T1,T2,d,e. L ⊢ ▼*[d, e] V1 ≡ V2 → L. ⓑ{I} V2 ⊢ ▼*[d+1, e] T1 ≡ T2 → - L ⊢ ▼*[d, e] ⓑ{I} V1. T1 ≡ ⓑ{I} V2. T2. -#I #L #V1 #V2 #T1 #T2 #d #e * #V #HV1 #HV2 * #T #HT1 #HT2 + L ⊢ ▼*[d, e] ⓑ{a,I} V1. T1 ≡ ⓑ{a,I} V2. T2. +#a #I #L #V1 #V2 #T1 #T2 #d #e * #V #HV1 #HV2 * #T #HT1 #HT2 lapply (tpss_lsubs_trans … HT1 (L. ⓑ{I} V) ?) -HT1 /2 width=1/ /3 width=5/ qed. @@ -75,11 +75,11 @@ lemma delift_inv_gref1: ∀L,U2,d,e,p. L ⊢ ▼*[d, e] §p ≡ U2 → U2 = §p. >(lift_inv_gref2 … HU2) -HU2 // qed-. -lemma delift_inv_bind1: ∀I,L,V1,T1,U2,d,e. L ⊢ ▼*[d, e] ⓑ{I} V1. T1 ≡ U2 → +lemma delift_inv_bind1: ∀a,I,L,V1,T1,U2,d,e. L ⊢ ▼*[d, e] ⓑ{a,I} V1. T1 ≡ U2 → ∃∃V2,T2. L ⊢ ▼*[d, e] V1 ≡ V2 & L. ⓑ{I} V2 ⊢ ▼*[d+1, e] T1 ≡ T2 & - U2 = ⓑ{I} V2. T2. -#I #L #V1 #T1 #U2 #d #e * #U #HU #HU2 + U2 = ⓑ{a,I} V2. T2. +#a #I #L #V1 #T1 #U2 #d #e * #U #HU #HU2 elim (tpss_inv_bind1 … HU) -HU #V #T #HV1 #HT1 #X destruct elim (lift_inv_bind2 … HU2) -HU2 #V2 #T2 #HV2 #HT2 lapply (tpss_lsubs_trans … HT1 (L. ⓑ{I} V2) ?) -HT1 /2 width=1/ /3 width=5/ 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 index 53832e0be..84c8bee70 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma @@ -25,9 +25,9 @@ inductive delifta: nat → nat → lenv → relation term ≝ ⇧[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_bind : ∀L,a,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 d e L (ⓑ{a,I} V1. T1) (ⓑ{a,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) @@ -58,7 +58,7 @@ lemma delift_delifta: ∀L,T1,T2,d,e. L ⊢ ▼*[d, e] T1 ≡ T2 → L ⊢ ▼ lapply (IH … HV12) // -H /2 width=6/ | >(delift_inv_gref1 … H) -H // ] -| * #I #V1 #T1 #_ #_ #IH #X #d #e #H +| * [ #a ] #I #V1 #T1 #_ #_ #IH #X #d #e #H [ elim (delift_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct lapply (delift_lsubs_trans … HT12 (L.ⓑ{I}V1) ?) -HT12 /2 width=1/ #HT12 lapply (IH … HV12) -HV12 // #HV12 @@ -86,9 +86,9 @@ lemma delift_ind_alt: ∀R:ℕ→ℕ→lenv→relation term. ) → (∀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 ⊢ ▼*[d, e] V1 ≡ V2 → + (∀L,a,I,V1,V2,T1,T2,d,e. L ⊢ ▼*[d, e] V1 ≡ V2 → L.ⓑ{I}V2 ⊢ ▼*[d + 1, e] T1 ≡ 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) + R (d+1) e (L.ⓑ{I}V2) T1 T2 → R d e L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2) ) → (∀L,I,V1,V2,T1,T2,d,e. L ⊢ ▼*[d, e] V1 ≡ V2 → L⊢ ▼*[d, e] T1 ≡ T2 → R d e L V1 V2 → 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 9fe72f82d..26c4e3e8a 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 @@ -47,7 +47,7 @@ fact sfr_delift_aux: ∀L,T,T1,d,e. d + e ≤ |L| → ≽ [d, e] L → T = T1 elim (IH … HKL … HK ?) -IH -HKL -HK [3: // |2: skip |4: >H -H /2 width=1/ ] -Hde -H #V2 #V12 (**) (* H erased two times *) elim (lift_total V2 0 d) /3 width=7/ -| #I #V1 #T1 #d #e #Hde #HL #H destruct +| #a #I #V1 #T1 #d #e #Hde #HL #H destruct elim (IH … V1 … Hde HL ?) [2,4: // |3: skip ] #V2 #HV12 elim (IH (L.ⓑ{I}V1) T1 ? ? (d+1) e ? ? ?) -IH [3,6: // |2: skip |4,5: /2 width=1/ ] -Hde -HL #T2 #HT12 lapply (delift_lsubs_trans … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/ /3 width=4/ diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts.ma index 8846eec0b..f447d729a 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts.ma @@ -81,10 +81,10 @@ lemma lifts_inv_gref1: ∀T2,p,des. ⇧*[des] §p ≡ T2 → T2 = §p. qed-. (* Basic_1: was: lift1_bind *) -lemma lifts_inv_bind1: ∀I,T2,des,V1,U1. ⇧*[des] ⓑ{I} V1. U1 ≡ T2 → +lemma lifts_inv_bind1: ∀a,I,T2,des,V1,U1. ⇧*[des] ⓑ{a,I} V1. U1 ≡ T2 → ∃∃V2,U2. ⇧*[des] V1 ≡ V2 & ⇧*[des + 1] U1 ≡ U2 & - T2 = ⓑ{I} V2. U2. -#I #T2 #des elim des -des + T2 = ⓑ{a,I} V2. U2. +#a #I #T2 #des elim des -des [ #V1 #U1 #H <(lifts_inv_nil … H) -H /2 width=5/ | #d #e #des #IHdes #V1 #U1 #H @@ -122,10 +122,10 @@ qed-. (* Basic properties *********************************************************) -lemma lifts_bind: ∀I,T2,V1,V2,des. ⇧*[des] V1 ≡ V2 → +lemma lifts_bind: ∀a,I,T2,V1,V2,des. ⇧*[des] V1 ≡ V2 → ∀T1. ⇧*[des + 1] T1 ≡ T2 → - ⇧*[des] ⓑ{I} V1. T1 ≡ ⓑ{I} V2. T2. -#I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des + ⇧*[des] ⓑ{a,I} V1. T1 ≡ ⓑ{a,I} V2. T2. +#a #I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des [ #V #T1 #H >(lifts_inv_nil … H) -H // | #V1 #V #V2 #des #d #e #HV1 #_ #IHV #T1 #H elim (lifts_inv_cons … H) -H /3 width=3/ diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.ma index 1d1d91018..8885b2339 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.ma @@ -58,7 +58,7 @@ fact ltpss_tpss_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e. lapply (tpss_trans_eq … HV01 HV12) -V1 #HV02 lapply (IH … HV02 … HK01 ? ?) -IH -HV02 -HK01 [1,3: // |2,4: skip | normalize /2 width=1/ | /2 width=6/ ] -| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #L0 #HL0 #H1 #H2 destruct +| #L #a #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #L0 #HL0 #H1 #H2 destruct lapply (tpss_lsubs_trans … HT12 (L. ⓑ{I} V1) ?) -HT12 /2 width=1/ #HT12 lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=2/ ] #HV12 lapply (IH … HT12 (L0. ⓑ{I} V1) ? ? ?) -IH -HT12 [1,3,5: /2 width=2/ |2,4: skip | normalize // ] -HL0 #HT12 diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tps.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tps.ma index df8a73c5a..dde21c93d 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tps.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tps.ma @@ -26,7 +26,7 @@ lemma ltpss_tps_conf_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 → | #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL01 #Hde1d2 lapply (transitive_le … Hde1d2 Hdi2) -Hde1d2 #Hde1i2 lapply (ltpss_ldrop_conf_ge … HL01 … HLK0 ?) -L0 // /2 width=4/ -| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01 #Hde1d2 +| #L0 #a #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01 #Hde1d2 @tps_bind [ /2 width=4/ | @IHTU2 -IHTU2 -IHVW2 [3: /2 by ltpss_tpss1/ |1,2: skip | /2 width=1/ ] ] (**) (* explicit constructor *) | /3 width=4/ ] @@ -40,7 +40,7 @@ lemma ltpss_tps_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 → | #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL10 #Hde1d2 lapply (transitive_le … Hde1d2 Hdi2) -Hde1d2 #Hde1i2 lapply (ltpss_ldrop_trans_ge … HL10 … HLK0 ?) -L0 // /2 width=4/ -| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10 #Hde1d2 +| #L0 #a #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10 #Hde1d2 @tps_bind [ /2 width=4/ | @IHTU2 -IHTU2 -IHVW2 [3: /2 by ltpss_tpss1/ |1,2: skip | /2 width=1/ ] ] (**) (* explicit constructor *) | /3 width=4/ ] diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tpss.ma index 52b52e55d..f071019f8 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tpss.ma @@ -51,7 +51,7 @@ lemma ltpss_tps_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 → | lapply (ltpss_ldrop_conf_ge … HL01 … HLK0 ?) -L0 // /3 width=4/ ] ] -| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01 +| #L0 #a #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01 elim (IHVW2 … HL01) -IHVW2 #V #HV2 #HVW2 elim (IHTU2 (L1. ⓑ{I} V) (d1 + 1) e1 ?) -IHTU2 /2 width=1/ -HL01 /3 width=5/ | #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01 @@ -92,7 +92,7 @@ lemma ltpss_tps_trans: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 → | lapply (ltpss_ldrop_trans_ge … HL10 … HLK0 ?) -HL10 -HLK0 // /3 width=4/ ] ] -| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10 +| #L0 #a #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10 elim (IHVW2 … HL10) -IHVW2 #V #HV2 #HVW2 elim (IHTU2 (L1. ⓑ{I} V) (d1 + 1) e1 ?) -IHTU2 /2 width=1/ -HL10 /3 width=5/ | #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10 diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma index b44570c2f..d0f964186 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma @@ -52,16 +52,16 @@ lemma tpss_refl: ∀d,e,L,T. L ⊢ T ▶* [d, e] T. /2 width=1/ qed. lemma tpss_bind: ∀L,V1,V2,d,e. L ⊢ V1 ▶* [d, e] V2 → - ∀I,T1,T2. L. ⓑ{I} V2 ⊢ T1 ▶* [d + 1, e] T2 → - L ⊢ ⓑ{I} V1. T1 ▶* [d, e] ⓑ{I} V2. T2. + ∀a,I,T1,T2. L. ⓑ{I} V2 ⊢ T1 ▶* [d + 1, e] T2 → + L ⊢ ⓑ{a,I} V1. T1 ▶* [d, e] ⓑ{a,I} V2. T2. #L #V1 #V2 #d #e #HV12 elim HV12 -V2 -[ #V2 #HV12 #I #T1 #T2 #HT12 elim HT12 -T2 +[ #V2 #HV12 #a #I #T1 #T2 #HT12 elim HT12 -T2 [ /3 width=5/ | #T #T2 #_ #HT2 #IHT @step /2 width=5/ (**) (* /3 width=5/ is too slow *) ] -| #V #V2 #_ #HV12 #IHV #I #T1 #T2 #HT12 +| #V #V2 #_ #HV12 #IHV #a #I #T1 #T2 #HT12 lapply (tpss_lsubs_trans … HT12 (L. ⓑ{I} V) ?) -HT12 /2 width=1/ #HT12 - lapply (IHV … HT12) -IHV -HT12 #HT12 @step /2 width=5/ (**) (* /3 width=5/ is too slow *) + lapply (IHV a … HT12) -IHV -HT12 #HT12 @step /2 width=5/ (**) (* /3 width=5/ is too slow *) ] qed. @@ -124,11 +124,11 @@ lemma tpss_inv_gref1: ∀L,T2,p,d,e. L ⊢ §p ▶* [d, e] T2 → T2 = §p. ] qed-. -lemma tpss_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ ⓑ{I} V1. T1 ▶* [d, e] U2 → +lemma tpss_inv_bind1: ∀d,e,L,a,I,V1,T1,U2. L ⊢ ⓑ{a,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. -#d #e #L #I #V1 #T1 #U2 #H @(tpss_ind … H) -U2 + U2 = ⓑ{a,I} V2. T2. +#d #e #L #a #I #V1 #T1 #U2 #H @(tpss_ind … H) -U2 [ /2 width=5/ | #U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct elim (tps_inv_bind1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_alt.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_alt.ma index 30b7e80ac..ae1dcf624 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_alt.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_alt.ma @@ -22,9 +22,9 @@ inductive tpssa: nat → nat → lenv → relation term ≝ | tpssa_subst: ∀L,K,V1,V2,W2,i,d,e. d ≤ i → i < d + e → ⇩[0, i] L ≡ K. ⓓV1 → tpssa 0 (d + e - i - 1) K V1 V2 → ⇧[0, i + 1] V2 ≡ W2 → tpssa d e L (#i) W2 -| tpssa_bind : ∀L,I,V1,V2,T1,T2,d,e. +| tpssa_bind : ∀L,a,I,V1,V2,T1,T2,d,e. tpssa d e L V1 V2 → tpssa (d + 1) e (L. ⓑ{I} V2) T1 T2 → - tpssa d e L (ⓑ{I} V1. T1) (ⓑ{I} V2. T2) + tpssa d e L (ⓑ{a,I} V1. T1) (ⓑ{a,I} V2. T2) | tpssa_flat : ∀L,I,V1,V2,T1,T2,d,e. tpssa d e L V1 V2 → tpssa d e L T1 T2 → tpssa d e L (ⓕ{I} V1. T1) (ⓕ{I} V2. T2) @@ -60,7 +60,7 @@ lemma tpssa_tps_trans: ∀L,T1,T,d,e. L ⊢ T1 ▶▶* [d, e] T → lapply (ldrop_fwd_ldrop2 … HLK) #H0LK lapply (tps_weak … H 0 (d+e) ? ?) -H // #H elim (tps_inv_lift1_be … H … H0LK … HVW2 ? ?) -H -H0LK -HVW2 // /3 width=6/ -| #L #I #V1 #V #T1 #T #d #e #_ #_ #IHV1 #IHT1 #X #H +| #L #a #I #V1 #V #T1 #T #d #e #_ #_ #IHV1 #IHT1 #X #H elim (tps_inv_bind1 … H) -H #V2 #T2 #HV2 #HT2 #H destruct lapply (tps_lsubs_trans … HT2 (L.ⓑ{I}V) ?) -HT2 /2 width=1/ #HT2 lapply (IHV1 … HV2) -IHV1 -HV2 #HV12 @@ -87,9 +87,9 @@ lemma tpss_ind_alt: ∀R:ℕ→ℕ→lenv→relation term. ⇩[O, i] L ≡ K.ⓓV1 → K ⊢ V1 ▶* [O, d + e - i - 1] V2 → ⇧[O, i + 1] V2 ≡ W2 → R O (d+e-i-1) K V1 V2 → R d e L #i W2 ) → - (∀L,I,V1,V2,T1,T2,d,e. L ⊢ V1 ▶* [d, e] V2 → + (∀L,a,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) + R (d+1) e (L.ⓑ{I}V2) T1 T2 → R d e L (ⓑ{a,I}V1.T1) (ⓑ{a,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 → diff --git a/matita/matita/contribs/lambda_delta/basic_2/unwind/sstas.ma b/matita/matita/contribs/lambda_delta/basic_2/unwind/sstas.ma deleted file mode 100644 index 9152b44ae..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/unwind/sstas.ma +++ /dev/null @@ -1,106 +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/ssta.ma". - -(* STRATIFIED UNWIND ON TERMS ***********************************************) - -inductive sstas (h:sh) (g:sd h) (L:lenv): relation term ≝ -| sstas_refl: ∀T,U. ⦃h, L⦄ ⊢ T •[g, 0] U → sstas h g L T T -| sstas_step: ∀T,U1,U2,l. ⦃h, L⦄ ⊢ T •[g, l+1] U1 → sstas h g L U1 U2 → - sstas h g L T U2. - -interpretation "stratified unwind (term)" - 'StaticTypeStar h g L T U = (sstas h g L T U). - -(* Basic eliminators ********************************************************) - -fact sstas_ind_alt_aux: ∀h,g,L,U2. ∀R:predicate term. - (∀T. ⦃h, L⦄ ⊢ U2 •[g , 0] T → R U2) → - (∀T,U1,l. ⦃h, L⦄ ⊢ T •[g, l + 1] U1 → - ⦃h, L⦄ ⊢ U1 •* [g] U2 → R U1 → R T - ) → - ∀T,U. ⦃h, L⦄ ⊢ T •*[g] U → U = U2 → R T. -#h #g #L #U2 #R #H1 #H2 #T #U #H elim H -H -T -U /2 width=2/ /3 width=5/ -qed-. - -lemma sstas_ind_alt: ∀h,g,L,U2. ∀R:predicate term. - (∀T. ⦃h, L⦄ ⊢ U2 •[g , 0] T → R U2) → - (∀T,U1,l. ⦃h, L⦄ ⊢ T •[g, l + 1] U1 → - ⦃h, L⦄ ⊢ U1 •* [g] U2 → R U1 → R T - ) → - ∀T. ⦃h, L⦄ ⊢ T •*[g] U2 → R T. -/3 width=9 by sstas_ind_alt_aux/ qed-. - -(* Basic inversion lemmas ***************************************************) - -fact sstas_inv_sort1_aux: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U → ∀k. T = ⋆k → - ∀l. deg h g k l → U = ⋆((next h)^l k). -#h #g #L #T #U #H @(sstas_ind_alt … H) -T -[ #U0 #HU0 #k #H #l #Hkl destruct - elim (ssta_inv_sort1 … HU0) -L #HkO #_ -U0 - >(deg_mono … Hkl HkO) -g -l // -| #T0 #U0 #l0 #HTU0 #_ #IHU0 #k #H #l #Hkl destruct - elim (ssta_inv_sort1 … HTU0) -L #HkS #H destruct - lapply (deg_mono … Hkl HkS) -Hkl #H destruct - >(IHU0 (next h k) ? l0) -IHU0 // /2 width=1/ >iter_SO >iter_n_Sm // -] -qed. - -lemma sstas_inv_sort1: ∀h,g,L,U,k. ⦃h, L⦄ ⊢ ⋆k •*[g] U → ∀l. deg h g k l → - U = ⋆((next h)^l k). -/2 width=6/ qed-. - -fact sstas_inv_bind1_aux: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U → - ∀J,X,Y. T = ⓑ{J}Y.X → - ∃∃Z. ⦃h, L.ⓑ{J}Y⦄ ⊢ X •*[g] Z & U = ⓑ{J}Y.Z. -#h #g #L #T #U #H @(sstas_ind_alt … H) -T -[ #U0 #HU0 #J #X #Y #H destruct - elim (ssta_inv_bind1 … HU0) -HU0 #X0 #HX0 #H destruct /3 width=3/ -| #T0 #U0 #l #HTU0 #_ #IHU0 #J #X #Y #H destruct - elim (ssta_inv_bind1 … HTU0) -HTU0 #X0 #HX0 #H destruct - elim (IHU0 J X0 Y ?) -IHU0 // #X1 #HX01 #H destruct /3 width=4/ -] -qed. - -lemma sstas_inv_bind1: ∀h,g,J,L,Y,X,U. ⦃h, L⦄ ⊢ ⓑ{J}Y.X •*[g] U → - ∃∃Z. ⦃h, L.ⓑ{J}Y⦄ ⊢ X •*[g] Z & U = ⓑ{J}Y.Z. -/2 width=3/ qed-. - -fact sstas_inv_appl1_aux: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U → ∀X,Y. T = ⓐY.X → - ∃∃Z. ⦃h, L⦄ ⊢ X •*[g] Z & U = ⓐY.Z. -#h #g #L #T #U #H @(sstas_ind_alt … H) -T -[ #U0 #HU0 #X #Y #H destruct - elim (ssta_inv_appl1 … HU0) -HU0 #X0 #HX0 #H destruct /3 width=3/ -| #T0 #U0 #l #HTU0 #_ #IHU0 #X #Y #H destruct - elim (ssta_inv_appl1 … HTU0) -HTU0 #X0 #HX0 #H destruct - elim (IHU0 X0 Y ?) -IHU0 // #X1 #HX01 #H destruct /3 width=4/ -] -qed. - -lemma sstas_inv_appl1: ∀h,g,L,Y,X,U. ⦃h, L⦄ ⊢ ⓐY.X •*[g] U → - ∃∃Z. ⦃h, L⦄ ⊢ X •*[g] Z & U = ⓐY.Z. -/2 width=3/ qed-. - -(* Basic forward lemmas *****************************************************) - -lemma sstas_fwd_correct: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U → - ∃∃W. ⦃h, L⦄ ⊢ U •[g, 0] W & ⦃h, L⦄ ⊢ U •*[g] U. -#h #g #L #T #U #H @(sstas_ind_alt … H) -T /2 width=1/ /3 width=2/ -qed-. - -(* Basic_1: removed theorems 7: - sty1_bind sty1_abbr sty1_appl sty1_cast2 - sty1_lift sty1_correct sty1_trans -*) diff --git a/matita/matita/contribs/lambda_delta/basic_2/unwind/sstas_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/unwind/sstas_lift.ma deleted file mode 100644 index 28302d71b..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/unwind/sstas_lift.ma +++ /dev/null @@ -1,57 +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/ssta_lift.ma". -include "basic_2/unwind/sstas.ma". - -(* STRATIFIED UNWIND ON TERMS ***********************************************) - -(* Advanced properties ******************************************************) - -lemma sstas_total_S: ∀h,g,L,l,T,U. ⦃h, L⦄ ⊢ T•[g, l + 1]U → - ∃∃W. ⦃h, L⦄ ⊢ T •*[g] W & ⦃h, L⦄ ⊢ U •*[g] W. -#h #g #L #l @(nat_ind_plus … l) -l -[ #T #U #HTU - elim (ssta_fwd_correct … HTU) /4 width=4/ -| #l #IHl #T #U #HTU - elim (ssta_fwd_correct … HTU) (lift_mono … HX … HU12) -X - elim (lift_total T1 d e) /3 width=10/ -| #T0 #U0 #l0 #HTU0 #_ #IHU01 #L2 #d #e #HL21 #T2 #HT02 #U2 #HU12 - elim (lift_total U0 d e) /3 width=10/ -] -qed. - -lemma sstas_inv_lift1: ∀h,g,L2,T2,U2. ⦃h, L2⦄ ⊢ T2 •*[g] U2 → - ∀L1,d,e. ⇩[d, e] L2 ≡ L1 → ∀T1. ⇧[d, e] T1 ≡ T2 → - ∃∃U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 & ⇧[d, e] U1 ≡ U2. -#h #g #L2 #T2 #U2 #H @(sstas_ind_alt … H) -T2 -[ #T2 #HUT2 #L1 #d #e #HL21 #U1 #HU12 - elim (ssta_inv_lift1 … HUT2 … HL21 … HU12) -HUT2 -HL21 /3 width=3/ -| #T0 #U0 #l0 #HTU0 #_ #IHU01 #L1 #d #e #HL21 #U1 #HU12 - elim (ssta_inv_lift1 … HTU0 … HL21 … HU12) -HTU0 -HU12 #U #HU1 #HU0 - elim (IHU01 … HL21 … HU0) -IHU01 -HL21 -U0 /3 width=4/ -] -qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unwind/sstas_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unwind/sstas_ltpss.ma deleted file mode 100644 index 0ef8f47e7..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/unwind/sstas_ltpss.ma +++ /dev/null @@ -1,55 +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/ssta_ltpss.ma". -include "basic_2/unwind/sstas.ma". - -(* STRATIFIED UNWIND ON TERMS ***********************************************) - -(* Properties about parallel unfold *****************************************) - -lemma sstas_ltpss_tpss_conf: ∀h,g,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 → - ∀L2,d,e. L1 ▶* [d, e] L2 → - ∀T2. L2 ⊢ T1 ▶* [d, e] T2 → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*[g] U2 & - L2 ⊢ U1 ▶* [d, e] U2. -#h #g #L1 #T1 #U1 #H @(sstas_ind_alt … H) -T1 -[ #T1 #HUT1 #L2 #d #e #HL12 #U2 #HU12 - elim (ssta_ltpss_tpss_conf … HUT1 … HL12 … HU12) -HUT1 -HL12 /3 width=3/ -| #T0 #U0 #l0 #HTU0 #_ #IHU01 #L2 #d #e #HL12 #T #HT0 - elim (ssta_ltpss_tpss_conf … HTU0 … HL12 … HT0) -HTU0 -HT0 #U #HTU #HU0 - elim (IHU01 … HL12 … HU0) -IHU01 -HL12 -U0 /3 width=4/ -] -qed. - -lemma sstas_ltpss_tps_conf: ∀h,g,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 → - ∀L2,d,e. L1 ▶* [d, e] L2 → - ∀T2. L2 ⊢ T1 ▶ [d, e] T2 → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*[g] U2 & L2 ⊢ U1 ▶* [d, e] U2. -/3 width=5/ qed. - -lemma sstas_ltpss_conf: ∀h,g,L1,T,U1. ⦃h, L1⦄ ⊢ T •*[g] U1 → - ∀L2,d,e. L1 ▶* [d, e] L2 → - ∃∃U2. ⦃h, L2⦄ ⊢ T •*[g] U2 & L2 ⊢ U1 ▶* [d, e] U2. -/2 width=5/ qed. - -lemma sstas_tpss_conf: ∀h,g,L,T1,U1. ⦃h, L⦄ ⊢ T1 •*[g] U1 → - ∀T2,d,e. L ⊢ T1 ▶* [d, e] T2 → - ∃∃U2. ⦃h, L⦄ ⊢ T2 •*[g] U2 & L ⊢ U1 ▶* [d, e] U2. -/2 width=5/ qed. - -lemma sstas_tps_conf: ∀h,g,L,T1,U1. ⦃h, L⦄ ⊢ T1 •*[g] U1 → - ∀T2,d,e. L ⊢ T1 ▶ [d, e] T2 → - ∃∃U2. ⦃h, L⦄ ⊢ T2 •*[g] U2 & L ⊢ U1 ▶* [d, e] U2. -/2 width=5/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unwind/sstas_sstas.ma b/matita/matita/contribs/lambda_delta/basic_2/unwind/sstas_sstas.ma deleted file mode 100644 index 03cbc46c7..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/unwind/sstas_sstas.ma +++ /dev/null @@ -1,74 +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/delift_lift.ma". -include "basic_2/static/ssta_ssta.ma". -include "basic_2/unwind/sstas_lift.ma". - -(* STRATIFIED UNWIND ON TERMS ***********************************************) - -(* Advanced inversion lemmas ************************************************) - -lemma sstas_inv_O: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U → - ∀T0. ⦃h, L⦄ ⊢ T •[g , 0] T0 → U = T. -#h #g #L #T #U #H @(sstas_ind_alt … H) -T // -#T0 #U0 #l0 #HTU0 #_ #_ #T1 #HT01 -elim (ssta_mono … HTU0 … HT01) (sstas_inv_O … HU12 … HUT1) -h -L -T1 -U2 // -| #T0 #U0 #l0 #HTU0 #_ #IHU01 #U2 #HU12 - lapply (sstas_inv_S … HU12 … HTU0) -T0 -l0 /2 width=1/ -] -qed-. - -(* More advancd inversion lemmas ********************************************) - -fact sstas_inv_lref1_aux: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U → ∀j. T = #j → - ∃∃I,K,V,W. ⇩[0, j] L ≡ K. ⓑ{I}V & ⦃h, K⦄ ⊢ V •*[g] W & - L ⊢ ▼*[0, j + 1] U ≡ W. -#h #g #L #T #U #H @(sstas_ind_alt … H) -T -[ #T #HUT #j #H destruct - elim (ssta_inv_lref1 … HUT) -HUT * #K #V #W [2: #l] #HLK #HVW #HVT - [ (sstas_mono … HWX … HWT) -X -W /3 width=7/ - ] -] -qed-. 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 f1eaa39dd..2d7b981c1 100644 --- a/matita/matita/contribs/lambda_delta/ground_2/xoa.conf.xml +++ b/matita/matita/contribs/lambda_delta/ground_2/xoa.conf.xml @@ -23,15 +23,19 @@ 3 2 3 3 3 4 + 4 1 4 2 4 3 4 4 + 4 5 5 2 5 3 5 4 + 5 5 6 4 6 6 - 7 6 + 6 7 + 7 7 3 4 3 diff --git a/matita/matita/contribs/lambda_delta/ground_2/xoa.ma b/matita/matita/contribs/lambda_delta/ground_2/xoa.ma index d96b471e6..3d265bc47 100644 --- a/matita/matita/contribs/lambda_delta/ground_2/xoa.ma +++ b/matita/matita/contribs/lambda_delta/ground_2/xoa.ma @@ -88,6 +88,14 @@ inductive ex3_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2:A0→A1→A2→A3→Prop) : Prop interpretation "multiple existental quantifier (3, 4)" 'Ex P0 P1 P2 = (ex3_4 ? ? ? ? P0 P1 P2). +(* multiple existental quantifier (4, 1) *) + +inductive ex4_1 (A0:Type[0]) (P0,P1,P2,P3:A0→Prop) : Prop ≝ + | ex4_1_intro: ∀x0. P0 x0 → P1 x0 → P2 x0 → P3 x0 → ex4_1 ? ? ? ? ? +. + +interpretation "multiple existental quantifier (4, 1)" 'Ex P0 P1 P2 P3 = (ex4_1 ? P0 P1 P2 P3). + (* multiple existental quantifier (4, 2) *) inductive ex4_2 (A0,A1:Type[0]) (P0,P1,P2,P3:A0→A1→Prop) : Prop ≝ @@ -112,6 +120,14 @@ inductive ex4_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3:A0→A1→A2→A3→Prop) : P interpretation "multiple existental quantifier (4, 4)" 'Ex P0 P1 P2 P3 = (ex4_4 ? ? ? ? P0 P1 P2 P3). +(* multiple existental quantifier (4, 5) *) + +inductive ex4_5 (A0,A1,A2,A3,A4:Type[0]) (P0,P1,P2,P3:A0→A1→A2→A3→A4→Prop) : Prop ≝ + | ex4_5_intro: ∀x0,x1,x2,x3,x4. P0 x0 x1 x2 x3 x4 → P1 x0 x1 x2 x3 x4 → P2 x0 x1 x2 x3 x4 → P3 x0 x1 x2 x3 x4 → ex4_5 ? ? ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (4, 5)" 'Ex P0 P1 P2 P3 = (ex4_5 ? ? ? ? ? P0 P1 P2 P3). + (* multiple existental quantifier (5, 2) *) inductive ex5_2 (A0,A1:Type[0]) (P0,P1,P2,P3,P4:A0→A1→Prop) : Prop ≝ @@ -136,6 +152,14 @@ inductive ex5_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4:A0→A1→A2→A3→Prop) interpretation "multiple existental quantifier (5, 4)" 'Ex P0 P1 P2 P3 P4 = (ex5_4 ? ? ? ? P0 P1 P2 P3 P4). +(* multiple existental quantifier (5, 5) *) + +inductive ex5_5 (A0,A1,A2,A3,A4:Type[0]) (P0,P1,P2,P3,P4:A0→A1→A2→A3→A4→Prop) : Prop ≝ + | ex5_5_intro: ∀x0,x1,x2,x3,x4. P0 x0 x1 x2 x3 x4 → P1 x0 x1 x2 x3 x4 → P2 x0 x1 x2 x3 x4 → P3 x0 x1 x2 x3 x4 → P4 x0 x1 x2 x3 x4 → ex5_5 ? ? ? ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (5, 5)" 'Ex P0 P1 P2 P3 P4 = (ex5_5 ? ? ? ? ? P0 P1 P2 P3 P4). + (* multiple existental quantifier (6, 4) *) inductive ex6_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→A3→Prop) : Prop ≝ @@ -152,13 +176,21 @@ inductive ex6_6 (A0,A1,A2,A3,A4,A5:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→A3 interpretation "multiple existental quantifier (6, 6)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_6 ? ? ? ? ? ? P0 P1 P2 P3 P4 P5). -(* multiple existental quantifier (7, 6) *) +(* multiple existental quantifier (6, 7) *) + +inductive ex6_7 (A0,A1,A2,A3,A4,A5,A6:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→A3→A4→A5→A6→Prop) : Prop ≝ + | ex6_7_intro: ∀x0,x1,x2,x3,x4,x5,x6. P0 x0 x1 x2 x3 x4 x5 x6 → P1 x0 x1 x2 x3 x4 x5 x6 → P2 x0 x1 x2 x3 x4 x5 x6 → P3 x0 x1 x2 x3 x4 x5 x6 → P4 x0 x1 x2 x3 x4 x5 x6 → P5 x0 x1 x2 x3 x4 x5 x6 → ex6_7 ? ? ? ? ? ? ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (6, 7)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_7 ? ? ? ? ? ? ? P0 P1 P2 P3 P4 P5). + +(* multiple existental quantifier (7, 7) *) -inductive ex7_6 (A0,A1,A2,A3,A4,A5:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→A4→A5→Prop) : Prop ≝ - | ex7_6_intro: ∀x0,x1,x2,x3,x4,x5. P0 x0 x1 x2 x3 x4 x5 → P1 x0 x1 x2 x3 x4 x5 → P2 x0 x1 x2 x3 x4 x5 → P3 x0 x1 x2 x3 x4 x5 → P4 x0 x1 x2 x3 x4 x5 → P5 x0 x1 x2 x3 x4 x5 → P6 x0 x1 x2 x3 x4 x5 → ex7_6 ? ? ? ? ? ? ? ? ? ? ? ? ? +inductive ex7_7 (A0,A1,A2,A3,A4,A5,A6:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→A4→A5→A6→Prop) : Prop ≝ + | ex7_7_intro: ∀x0,x1,x2,x3,x4,x5,x6. P0 x0 x1 x2 x3 x4 x5 x6 → P1 x0 x1 x2 x3 x4 x5 x6 → P2 x0 x1 x2 x3 x4 x5 x6 → P3 x0 x1 x2 x3 x4 x5 x6 → P4 x0 x1 x2 x3 x4 x5 x6 → P5 x0 x1 x2 x3 x4 x5 x6 → P6 x0 x1 x2 x3 x4 x5 x6 → ex7_7 ? ? ? ? ? ? ? ? ? ? ? ? ? ? . -interpretation "multiple existental quantifier (7, 6)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_6 ? ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6). +interpretation "multiple existental quantifier (7, 7)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_7 ? ? ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6). (* multiple disjunction connective (3) *) 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 44453eae0..8a167c86a 100644 --- a/matita/matita/contribs/lambda_delta/ground_2/xoa_notation.ma +++ b/matita/matita/contribs/lambda_delta/ground_2/xoa_notation.ma @@ -104,6 +104,16 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) }. +(* multiple existental quantifier (4, 1) *) + +notation > "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.$P0) (λ${ident x0}.$P1) (λ${ident x0}.$P2) (λ${ident x0}.$P3) }. + +notation < "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.$P0) (λ${ident x0}:$T0.$P1) (λ${ident x0}:$T0.$P2) (λ${ident x0}:$T0.$P3) }. + (* multiple existental quantifier (4, 2) *) notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" @@ -134,6 +144,16 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) }. +(* multiple existental quantifier (4, 5) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P3) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P3) }. + (* multiple existental quantifier (5, 2) *) notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)" @@ -164,6 +184,16 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P4) }. +(* multiple existental quantifier (5, 5) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P4) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P4) }. + (* multiple existental quantifier (6, 4) *) notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)" @@ -184,15 +214,25 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P5) }. -(* multiple existental quantifier (7, 6) *) +(* multiple existental quantifier (6, 7) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P5) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P5) }. + +(* multiple existental quantifier (7, 7) *) -notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)" +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)" non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P6) }. + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P6) }. -notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)" +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)" non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P6) }. + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P6) }. (* multiple disjunction connective (3) *) diff --git a/matita/matita/contribs/lambda_delta/ma2etc.sh b/matita/matita/contribs/lambda_delta/ma2etc.sh new file mode 100644 index 000000000..e546af776 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/ma2etc.sh @@ -0,0 +1 @@ +for FILE in `find $1 -name "*.ma"`; do svn mv $FILE ${FILE/%.ma/.etc} ; done