From f62eeb3c7824564ccbe4fff6e75ddee46ca39cc0 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 20 Jul 2013 22:10:11 +0000 Subject: [PATCH] - new extendedd beta-reductum involving native type annotation - extended strong normalization for simply typed terms (milestone) - some renaming --- .../lambdadelta/basic_2/computation/acp.ma | 8 +- .../basic_2/computation/acp_aaa.ma | 30 ++--- .../lambdadelta/basic_2/computation/acp_cr.ma | 52 ++++---- .../basic_2/computation/{cpe.ma => cpre.ma} | 18 +-- .../computation/{cpe_cpe.ma => cpre_cpre.ma} | 8 +- .../lambdadelta/basic_2/computation/cprs.ma | 4 +- .../lambdadelta/basic_2/computation/cpxe.ma | 34 +++++ .../lambdadelta/basic_2/computation/cpxs.ma | 57 ++++---- .../basic_2/computation/cpxs_cpxs.ma | 61 +++++++-- .../basic_2/computation/cpxs_tstc.ma | 39 ++++-- .../basic_2/computation/cpxs_tstc_vector.ma | 87 ++++++++----- .../lambdadelta/basic_2/computation/csn.ma | 22 +++- .../basic_2/computation/csn_aaa.ma | 8 +- .../basic_2/computation/csn_lift.ma | 1 + .../basic_2/computation/csn_lpx.ma | 47 +++---- .../basic_2/computation/csn_tstc_vector.ma | 120 +++++++++-------- .../basic_2/computation/csn_vector.ma | 16 ++- .../lambdadelta/basic_2/computation/dxprs.ma | 2 +- .../basic_2/computation/dxprs_aaa.ma | 2 +- .../lambdadelta/basic_2/computation/lpxs.ma | 5 +- .../lambdadelta/basic_2/computation/lsubc.ma | 66 +++++----- .../basic_2/computation/lsubc_ldrop.ma | 13 +- .../basic_2/computation/lsubc_lsuba.ma | 5 +- .../lambdadelta/basic_2/dynamic/snv_aaa.ma | 2 +- .../basic_2/equivalence/cpcs_aaa.ma | 2 +- .../lambdadelta/basic_2/grammar/term.ma | 15 --- .../contribs/lambdadelta/basic_2/names.txt | 7 +- .../contribs/lambdadelta/basic_2/notation.ma | 18 ++- .../lambdadelta/basic_2/reduction/cnx.ma | 13 +- .../lambdadelta/basic_2/reduction/cpr.ma | 2 +- .../lambdadelta/basic_2/reduction/cpx.ma | 123 +++++++++++------- .../lambdadelta/basic_2/reduction/cpx_cix.ma | 4 +- .../lambdadelta/basic_2/reduction/cpx_lift.ma | 18 ++- .../lambdadelta/basic_2/reduction/lpx.ma | 6 +- .../lambdadelta/basic_2/reduction/lpx_aaa.ma | 14 +- .../lambdadelta/basic_2/reduction/lsubx.ma | 101 ++++++++++++++ .../basic_2/reduction/lsubx_lsubx.ma | 53 ++++++++ .../contribs/lambdadelta/basic_2/static/sd.ma | 29 +++-- .../lambdadelta/basic_2/substitution/cpss.ma | 2 +- .../lambdadelta/basic_2/substitution/lsubr.ma | 13 +- .../basic_2/substitution/lsubr_lsubr.ma | 2 + .../lambdadelta/basic_2/unfold/cpqs.ma | 2 +- .../lambdadelta/basic_2/web/basic_2.ldw.xml | 11 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 18 ++- .../contribs/lambdadelta/ground_2/star.ma | 9 ++ .../lambdadelta/ground_2/xoa.conf.xml | 4 + .../contribs/lambdadelta/ground_2/xoa.ma | 36 +++++ .../lambdadelta/ground_2/xoa_notation.ma | 36 +++++ 48 files changed, 827 insertions(+), 418 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/computation/{cpe.ma => cpre.ma} (76%) rename matita/matita/contribs/lambdadelta/basic_2/computation/{cpe_cpe.ma => cpre_cpre.ma} (85%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/cpxe.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/reduction/lsubx.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/reduction/lsubx_lsubx.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma index 4ad5ffb5e..136ebacea 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma @@ -29,13 +29,17 @@ definition CP2s ≝ λRR:lenv→relation term. λRS:relation term. NF … (RR L) RS T → NF … (RR L0) RS T0. definition CP3 ≝ λRP:lenv→predicate term. - ∀L,V,k. RP L (ⓐ⋆k.V) → RP L V. + ∀L,T,k. RP L (ⓐ⋆k.T) → RP L T. + +definition CP4 ≝ λRP:lenv→predicate term. + ∀L,W,T. RP L W → RP L T → RP L (ⓝW.T). (* requirements for abstract computation properties *) record acp (RR:lenv->relation term) (RS:relation term) (RP:lenv→predicate term) : Prop ≝ { cp1: CP1 RR RS; cp2: CP2 RR RS; - cp3: CP3 RP + cp3: CP3 RP; + cp4: CP4 RP }. (* Basic properties *********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma index 5e5d699e9..77b705f97 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma @@ -47,13 +47,14 @@ theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP. elim (lifts_lift_trans … Hi0 … Hdes0 … HV10 … HV0) -HV10 #V2 #HV12 #HV2 @(s5 … HB … ◊ … HV0 HLK2) /3 width=7/ (* uses IHB HL20 V2 HV0 *) | -HLK1 -IHB -HL01 -HL20 -HK1b -Hi0 -Hdes0 - #K2 #V2 #A2 #HKV2A #HKV0A #_ #H1 #H2 destruct + #K2 #V2 #A2 #HKV2A #H1KV0A #H2KV0A #_ #H1 #H2 destruct lapply (ldrop_fwd_ldrop2 … HLK2) #HLK2b lapply (aaa_lifts … HK01 … HV10 HKV1B) -HKV1B -HK01 -HV10 #HKV0B - >(aaa_mono … HKV0A … HKV0B) in HKV2A; -HKV0A -HKV0B #HKV2B + lapply (aaa_mono … H2KV0A … HKV0B) #H destruct -H2KV0A -HKV0B + elim (lift_total V0 0 (i0 +1)) #V3 #HV03 elim (lift_total V2 0 (i0 +1)) #V #HV2 - @(s5 … HB … ◊ … HV2 HLK2) - @(s8 … HB … HKV2B) // + @(s5 … HB … ◊ … (ⓝV3.V) … HLK2) [2: /2 width=1/ ] + @(s7 … HB … ◊) [ @(s8 … HB … HKV2A) // | @(s8 … HB … H1KV0A) // ] ] | #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 @@ -63,25 +64,18 @@ theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP. @(s6 … HA … ◊ ◊) // /3 width=5/ | #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 - @(s1 … HB) /2 width=5/ - | -IHB - #L3 #V3 #T3 #des3 #HL32 #HT03 #HB - elim (lifts_total des3 W0) #W2 #HW02 - elim (ldrops_lsubc_trans … H1RP H2RP … HL32 … HL02) -L2 #L2 #HL32 #HL20 - lapply (aaa_lifts … L2 W2 … (des @@ des3) … HLWB) -HLWB /2 width=3/ #HLW2B - @(IHA (L2. ⓛW2) … (des + 1 @@ des3 + 1)) -IHA - /2 width=3/ /3 width=5/ - ] + @(aacr_abst … H1RP H2RP) [ /2 width=5/ ] + #L3 #V3 #W3 #T3 #des3 #HL32 #HW03 #HT03 #H1B #H2B + elim (ldrops_lsubc_trans … H1RP H2RP … HL32 … HL02) -L2 #L2 #HL32 #HL20 + lapply (aaa_lifts … L2 W3 … (des @@ des3) … HLWB) -HLWB /2 width=3/ #HLW2B + @(IHA (L2. ⓛW3) … (des + 1 @@ des3 + 1)) -IHA /2 width=3/ /3 width=5/ | #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20 elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct /3 width=10/ | #L #V #T #A #_ #_ #IH1A #IH2A #L0 #des #HL0 #X #H #L2 #HL20 - elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct + elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct lapply (aacr_acr … H1RP H2RP A) #HA - lapply (s1 … HA) #H - @(s7 … HA … ◊) /2 width=5/ /3 width=5/ + @(s7 … HA … ◊) /2 width=5/ ] qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma index a91a9f318..9e5059012 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma @@ -29,23 +29,23 @@ definition S2 ≝ λRR:lenv→relation term. λRS:relation term. λRP,C:lenv→p ∀L,Vs. all … (RP L) Vs → ∀T. 𝐒⦃T⦄ → NF … (RR L) RS T → C L (ⒶVs.T). -(* Note: this is Tait's ii *) -definition S3 ≝ λRP,C:lenv→predicate term. - ∀a,L,Vs,V,T,W. C L (ⒶVs. ⓓ{a}V. T) → RP L W → C L (ⒶVs. ⓐV. ⓛ{a}W. T). +(* Note: this generalizes Tait's ii *) +definition S3 ≝ λC:lenv→predicate term. + ∀a,L,Vs,V,T,W. C L (ⒶVs.ⓓ{a}ⓝW.V.T) → C L (ⒶVs.ⓐV.ⓛ{a}W.T). definition S4 ≝ λRP,C:lenv→predicate term. ∀L,Vs. all … (RP L) Vs → ∀k. C L (ⒶVs.⋆k). -definition S5 ≝ λRP,C:lenv→predicate term. ∀I,L,K,Vs,V1,V2,i. - C L (ⒶVs. V2) → ⇧[0, i + 1] V1 ≡ V2 → - ⇩[0, i] L ≡ K. ⓑ{I}V1 → C L (Ⓐ Vs. #i). +definition S5 ≝ λC:lenv→predicate term. ∀I,L,K,Vs,V1,V2,i. + C L (ⒶVs.V2) → ⇧[0, i + 1] V1 ≡ V2 → + ⇩[0, i] L ≡ K.ⓑ{I}V1 → C L (Ⓐ Vs.#i). definition S6 ≝ λRP,C:lenv→predicate term. ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → - ∀a,V,T. C (L. ⓓV) (ⒶV2s. T) → RP L V → C L (ⒶV1s. ⓓ{a}V. T). + ∀a,V,T. C (L.ⓓV) (ⒶV2s.T) → RP L V → C L (ⒶV1s.ⓓ{a}V.T). -definition S7 ≝ λRP,C:lenv→predicate term. - ∀L,Vs,T,W. C L (ⒶVs. T) → RP L W → C L (ⒶVs. ⓝW. T). +definition S7 ≝ λC:lenv→predicate term. + ∀L,Vs,T,W. C L (ⒶVs.T) → C L (ⒶVs.W) → C L (ⒶVs.ⓝW.T). definition S8 ≝ λC:lenv→predicate term. ∀L2,L1,T1,d,e. C L1 T1 → ∀T2. ⇩[d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → C L2 T2. @@ -58,11 +58,11 @@ definition S8s ≝ λC:lenv→predicate term. record acr (RR:lenv->relation term) (RS:relation term) (RP,C:lenv→predicate term) : Prop ≝ { s1: S1 RP C; s2: S2 RR RS RP C; - s3: S3 RP C; + s3: S3 C; s4: S4 RP C; - s5: S5 RP C; + s5: S5 C; s6: S6 RP C; - s7: S7 RP C; + s7: S7 C; s8: S8 C }. @@ -71,7 +71,7 @@ let rec aacr (RP:lenv→predicate term) (A:aarity) (L:lenv) on A: predicate term λT. match A with [ AAtom ⇒ RP L T | APair B A ⇒ ∀L0,V0,T0,des. aacr RP B L0 V0 → ⇩*[des] L0 ≡ L → ⇧*[des] T ≡ T0 → - aacr RP A L0 (ⓐV0. T0) + aacr RP A L0 (ⓐV0.T0) ]. interpretation @@ -125,11 +125,11 @@ 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/ -| #a #L #Vs #U #T #W #HA #HW #L0 #V0 #X #des #HB #HL0 #H +| #a #L #Vs #U #T #W #HA #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 - @(s3 … IHA … (V0 @ V0s)) /2 width=6 by rp_lifts/ /4 width=5/ + @(s3 … IHA … (V0 @ V0s)) /5 width=5/ | #L #Vs #HVs #k #L0 #V0 #X #hdes #HB #HL0 #H elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct >(lifts_inv_sort1 … HY) -Y @@ -150,7 +150,7 @@ lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → elim (lifts_inv_bind1 … HY) -HY #V0 #T0 #HV0 #HT0 #H destruct elim (lift_total V10 0 1) #V20 #HV120 elim (liftv_total 0 1 V10s) #V20s #HV120s - @(s6 … IHA … (V10 @ V10s) (V20 @ V20s)) /2 width=1/ /2 width=6 by rp_lifts/ + @(s6 … IHA … (V10 @ V10s) (V20 @ V20s)) /2 width=1/ /3 width=6 by rp_lifts/ @(HA … (des + 1)) /2 width=1/ [ @(s8 … IHB … HB … HV120) /2 width=1/ | @lifts_applv // @@ -160,24 +160,28 @@ lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → | #L #Vs #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 #W0 #T0 #HW0 #HT0 #H destruct - @(s7 … IHA … (V0 @ V0s)) /2 width=6 by rp_lifts/ /3 width=4/ + @(s7 … IHA … (V0 @ V0s)) /3 width=4/ | /3 width=7/ ] qed. lemma aacr_abst: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → - ∀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〛 + ∀a,L,W,T,A,B. ⦃L, W⦄ ϵ[RP] 〚B〛 → ( + ∀L0,V0,W0,T0,des. ⇩*[des] L0 ≡ L → ⇧*[des ] W ≡ W0 → ⇧*[des + 1] T ≡ T0 → + ⦃L0, V0⦄ ϵ[RP] 〚B〛 → ⦃L0, W0⦄ ϵ[RP] 〚B〛 → ⦃L0.ⓓⓝW0.V0, T0⦄ ϵ[RP] 〚A〛 ) → - ⦃L, ⓛ{a}W. T⦄ ϵ[RP] 〚②B. A〛. + ⦃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 -lapply (s1 … HCB) -HCB #HCB -@(s3 … HCA … ◊) /2 width=6 by rp_lifts/ -@(s6 … HCA … ◊ ◊) // /2 width=1/ /2 width=3/ +lapply (acr_lifts … HL0 … HW0 HW) -HW [ @(s8 … HCB) ] #HW0 +@(s3 … HCA … ◊) +@(s6 … HCA … ◊ ◊) // +[ @(HA … HL0) // +| lapply (s1 … HCB) -HCB #HCB + @(cp4 … H1RP) /2 width=1/ +] qed. (* Basic_1: removed theorems 2: sc3_arity_gen sc3_repl *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpe.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpre.ma similarity index 76% rename from matita/matita/contribs/lambdadelta/basic_2/computation/cpe.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/cpre.ma index 285e6e4fc..1a67e2b46 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpe.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpre.ma @@ -17,19 +17,21 @@ include "basic_2/computation/csn.ma". (* CONTEXT-SENSITIVE PARALLEL EVALUATION ON TERMS **************************) -definition cpe: lenv → relation term ≝ - λL,T1,T2. L ⊢ T1 ➡* T2 ∧ L ⊢ 𝐍⦃T2⦄. +definition cpre: lenv → relation term ≝ + λL,T1,T2. L ⊢ T1 ➡* T2 ∧ L ⊢ 𝐍⦃T2⦄. interpretation "context-sensitive parallel evaluation (term)" - 'PEval L T1 T2 = (cpe L T1 T2). + 'PEval L T1 T2 = (cpre L T1 T2). (* Basic_properties *********************************************************) -(* Basic_1: was: nf2_sn3 *) -lemma cpe_csn: ∀L,T1. L ⊢ ⬊* T1 → ∃T2. L ⊢ T1 ➡* 𝐍⦃T2⦄. -#L #T1 #H @(csn_ind … H) -T1 +(* Basic_1: was just: nf2_sn3 *) +axiom csn_cpre: ∀h,g,L,T1. ⦃h, L⦄ ⊢ ⬊*[g] T1 → ∃T2. L ⊢ T1 ➡* 𝐍⦃T2⦄. +(* +#h #g #L #T1 #H @(csn_ind … H) -T1 #T1 #_ #IHT1 -elim (cnf_dec L T1) /3 width=3/ +elim (cnr_dec L T1) /3 width=3/ * #T #H1T1 #H2T1 -elim (IHT1 … H1T1 H2T1) -IHT1 -H2T1 #T2 * /4 width=3/ +elim (IHT1 … H2T1) -IHT1 -H2T1 [2: /2 width=2/ ] #T2 * /4 width=3/ qed. +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpe_cpe.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpre_cpre.ma similarity index 85% rename from matita/matita/contribs/lambdadelta/basic_2/computation/cpe_cpe.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/cpre_cpre.ma index ec770787b..cac970e9a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpe_cpe.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpre_cpre.ma @@ -13,16 +13,16 @@ (**************************************************************************) include "basic_2/computation/cprs_cprs.ma". -include "basic_2/computation/cpe.ma". +include "basic_2/computation/cpre.ma". (* CONTEXT-SENSITIVE PARALLEL EVALUATION ON TERMS **************************) (* Main properties *********************************************************) (* Basic_1: was: nf2_pr3_confluence *) -theorem cpe_mono: ∀L,T,T1. L ⊢ T ➡* 𝐍⦃T1⦄ → ∀T2. L ⊢ T ➡* 𝐍⦃T2⦄ → T1 = T2. +theorem cpre_mono: ∀L,T,T1. L ⊢ T ➡* 𝐍⦃T1⦄ → ∀T2. L ⊢ T ➡* 𝐍⦃T2⦄ → T1 = T2. #L #T #T1 * #H1T1 #H2T1 #T2 * #H1T2 #H2T2 elim (cprs_conf … H1T1 … H1T2) -T #T #HT1 ->(cprs_inv_cnf1 … HT1 H2T1) -T1 #HT2 ->(cprs_inv_cnf1 … HT2 H2T2) -T2 // +>(cprs_inv_cnr1 … HT1 H2T1) -T1 #HT2 +>(cprs_inv_cnr1 … HT2 H2T2) -T2 // qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma index 1b3bcf666..c0e440d69 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma @@ -66,8 +66,8 @@ lemma cprs_cpss_trans: ∀L,T1,T. L ⊢ T1 ➡* T → ∀T2. L ⊢ T ▶* T2 → lemma cpss_cprs_trans: ∀L,T1,T. L ⊢ T1 ▶* T → ∀T2. L ⊢ T ➡* T2 → L ⊢ T1 ➡* T2. /3 width=3/ qed-. -lemma cprs_lsubr_trans: lsubr_trans … cprs. -/3 width=3 by cpr_lsubr_trans, TC_lsubr_trans/ +lemma cprs_lsubr_trans: lsub_trans … cprs lsubr. +/3 width=5 by cpr_lsubr_trans, TC_lsub_trans/ qed-. (* Basic_1: was: pr3_pr1 *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxe.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxe.ma new file mode 100644 index 000000000..51ab24d5e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxe.ma @@ -0,0 +1,34 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cpxs.ma". +include "basic_2/computation/csn.ma". + +(* CONTEXT-SENSITIVE EXTENDED PARALLEL EVALUATION ON TERMS ******************) + +definition cpxe: ∀h. sd h → lenv → relation term ≝ + λh,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 ∧ ⦃h, L⦄ ⊢ 𝐍[g]⦃T2⦄. + +interpretation "context-sensitive extended parallel evaluation (term)" + 'PEval h g L T1 T2 = (cpxe h g L T1 T2). + +(* Basic_properties *********************************************************) + +lemma csn_cpxe: ∀h,g,L,T1. ⦃h, L⦄ ⊢ ⬊*[g] T1 → ∃T2. ⦃h, L⦄ ⊢ T1 ➡*[g] 𝐍⦃T2⦄. +#h #g #L #T1 #H @(csn_ind … H) -T1 +#T1 #_ #IHT1 +elim (cnx_dec h g L T1) /3 width=3/ +* #T #H1T1 #H2T1 +elim (IHT1 … H1T1 H2T1) -IHT1 -H2T1 #T2 * /4 width=3/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma index ba775d00d..028798162 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma @@ -55,10 +55,15 @@ lemma cpxs_strap2: ∀h,g,L,T1,T. ⦃h, L⦄ ⊢ T1 ➡[g] T → ∀T2. ⦃h, L⦄ ⊢ T ➡*[g] T2 → ⦃h, L⦄ ⊢ T1 ➡*[g] T2. normalize /2 width=3/ qed. -lemma cprs_cpxs: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → ⦃h, L⦄ ⊢ T1 ➡*[g] T2. +lemma lsubx_cpxs_trans: ∀h,g. lsub_trans … (cpxs h g) lsubx. +/3 width=5 by lsubx_cpx_trans, TC_lsub_trans/ +qed-. + +axiom cprs_cpxs: ∀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/ qed. - +*) lemma cpxs_bind_dx: ∀h,g,L,V1,V2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 → ∀I,T1,T2. ⦃h, L. ⓑ{I}V1⦄ ⊢ T1 ➡*[g] T2 → ∀a. ⦃h, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[g] ⓑ{a,I}V2.T2. @@ -87,11 +92,15 @@ lemma cpxs_tau: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 → ∀V. ⦃h, L #h #g #L #T1 #T2 #H elim H -T2 /2 width=3/ /3 width=1/ qed. -lemma cpxs_beta_dx: ∀h,g,a,L,V1,V2,W,T1,T2. - ⦃h, L⦄ ⊢ V1 ➡[g] V2 → ⦃h, L.ⓛW⦄ ⊢ T1 ➡*[g] T2 → - ⦃h, L⦄ ⊢ ⓐV1.ⓛ{a}W.T1 ➡*[g] ⓓ{a}V2.T2. -#h #g #a #L #V1 #V2 #W #T1 #T2 #HV12 * -T2 /3 width=1/ -/4 width=6 by cpxs_strap1, cpxs_bind_dx, cpxs_flat_dx, cpx_beta/ (**) (* auto too slow without trace *) +lemma cpxs_ti: ∀h,g,L,V1,V2. ⦃h, L⦄ ⊢ V1 ➡*[g] V2 → ∀T. ⦃h, L⦄ ⊢ ⓝV1.T ➡*[g] V2. +#h #g #L #V1 #V2 #H elim H -V2 /2 width=3/ /3 width=1/ +qed. + +lemma cpxs_beta_dx: ∀h,g,a,L,V1,V2,W1,W2,T1,T2. + ⦃h, L⦄ ⊢ V1 ➡[g] V2 → ⦃h, L.ⓛW1⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ W1 ➡[g] W2 → + ⦃h, L⦄ ⊢ ⓐV1.ⓛ{a}W1.T1 ➡*[g] ⓓ{a}ⓝW2.V2.T2. +#h #g #a #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 * -T2 /3 width=1/ +/4 width=7 by cpxs_strap1, cpxs_bind_dx, cpxs_flat_dx, cpx_beta/ (**) (* auto too slow without trace *) qed. lemma cpxs_theta_dx: ∀h,g,a,L,V1,V,V2,W1,W2,T1,T2. @@ -112,40 +121,22 @@ lemma cpxs_inv_sort1: ∀h,g,L,U2,k. ⦃h, L⦄ ⊢ ⋆k ➡*[g] U2 → elim (cpx_inv_sort1 … HU2) -HU2 [ #H destruct /2 width=4/ | * #l0 #Hkl0 #H destruct -l - @(ex2_2_intro … (n+1) l0) /2 width=1/ >iter_SO // - ] -] -qed-. - -lemma cpxs_inv_appl1: ∀h,g,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓐV1.T1 ➡*[g] U2 → - ∨∨ ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡*[g] V2 & ⦃h, L⦄ ⊢ T1 ➡*[g] T2 & - U2 = ⓐV2. T2 - | ∃∃a,V2,W,T. ⦃h, L⦄ ⊢ V1 ➡*[g] V2 & - ⦃h, L⦄ ⊢ T1 ➡*[g] ⓛ{a}W.T & ⦃h, L⦄ ⊢ ⓓ{a}V2.T ➡*[g] U2 - | ∃∃a,V0,V2,V,T. ⦃h, L⦄ ⊢ V1 ➡*[g] V0 & ⇧[0,1] V0 ≡ V2 & - ⦃h, L⦄ ⊢ T1 ➡*[g] ⓓ{a}V.T & ⦃h, L⦄ ⊢ ⓓ{a}V.ⓐV2.T ➡*[g] U2. -#h #g #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 [ /3 width=5/ ] -#U #U2 #_ #HU2 * * -[ #V0 #T0 #HV10 #HT10 #H destruct - elim (cpx_inv_appl1 … HU2) -HU2 * - [ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5/ - | #a #V2 #W2 #T #T2 #HV02 #HT2 #H1 #H2 destruct - lapply (cpxs_strap1 … HV10 … HV02) -V0 /5 width=7/ - | #a #V #V2 #W0 #W2 #T #T2 #HV0 #HV2 #HW02 #HT2 #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 *) + @(ex2_2_intro … (n+1) l0) /2 width=1 by deg_inv_prec/ >iter_SO // ] -| /4 width=9/ -| /4 width=11/ ] qed-. -lemma cpxs_inv_cast1: ∀h,g,L,W1,T1,U2. ⦃h, L⦄ ⊢ ⓝW1.T1 ➡*[g] U2 → ⦃h, L⦄ ⊢ T1 ➡*[g] U2 ∨ - ∃∃W2,T2. ⦃h, L⦄ ⊢ W1 ➡*[g] W2 & ⦃h, L⦄ ⊢ T1 ➡*[g] T2 & U2 = ⓝW2.T2. +lemma cpxs_inv_cast1: ∀h,g,L,W1,T1,U2. ⦃h, L⦄ ⊢ ⓝW1.T1 ➡*[g] U2 → + ∨∨ ∃∃W2,T2. ⦃h, L⦄ ⊢ W1 ➡*[g] W2 & ⦃h, L⦄ ⊢ T1 ➡*[g] T2 & U2 = ⓝW2.T2 + | ⦃h, L⦄ ⊢ T1 ➡*[g] U2 + | ⦃h, L⦄ ⊢ W1 ➡*[g] U2. #h #g #L #W1 #T1 #U2 #H @(cpxs_ind … H) -U2 /3 width=5/ #U2 #U #_ #HU2 * /3 width=3/ * #W #T #HW1 #HT1 #H destruct elim (cpx_inv_cast1 … HU2) -HU2 /3 width=3/ * -#W2 #T2 #HW2 #HT2 #H destruct /4 width=5/ +#W2 #T2 #HW2 #HT2 #H destruct +lapply (cpxs_strap1 … HW1 … HW2) -W +lapply (cpxs_strap1 … HT1 … HT2) -T /3 width=5/ qed-. lemma cpxs_inv_cnx1: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T ➡*[g] U → ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ → T = U. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma index 08696ac93..da372de97 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma @@ -38,32 +38,65 @@ theorem cpxs_flat: ∀h,g,I,L,V1,V2,T1,T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 → @(cpxs_trans … IHV1) -IHV1 /2 width=1/ qed. -theorem cpxs_beta: ∀h,g,a,L,V1,V2,W,T1,T2. - ⦃h, L.ⓛW⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ V1 ➡*[g] V2 → - ⦃h, L⦄ ⊢ ⓐV1.ⓛ{a}W.T1 ➡*[g] ⓓ{a}V2.T2. -#h #g #a #L #V1 #V2 #W #T1 #T2 #HT12 #H @(cpxs_ind … H) -V2 /2 width=1/ +theorem cpxs_beta_rc: ∀h,g,a,L,V1,V2,W1,W2,T1,T2. + ⦃h, L⦄ ⊢ V1 ➡[g] V2 → ⦃h, L.ⓛW1⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ W1 ➡*[g] W2 → + ⦃h, L⦄ ⊢ ⓐV1.ⓛ{a}W1.T1 ➡*[g] ⓓ{a}ⓝW2.V2.T2. +#h #g #a #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HT12 #H @(cpxs_ind … H) -W2 /2 width=1/ +#W #W2 #_ #HW2 #IHW1 +@(cpxs_trans … IHW1) -IHW1 /3 width=1/ +qed. + +theorem cpxs_beta: ∀h,g,a,L,V1,V2,W1,W2,T1,T2. + ⦃h, L.ⓛW1⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ W1 ➡*[g] W2 → ⦃h, L⦄ ⊢ V1 ➡*[g] V2 → + ⦃h, L⦄ ⊢ ⓐV1.ⓛ{a}W1.T1 ➡*[g] ⓓ{a}ⓝW2.V2.T2. +#h #g #a #L #V1 #V2 #W1 #W2 #T1 #T2 #HT12 #HW12 #H @(cpxs_ind … H) -V2 /2 width=1/ #V #V2 #_ #HV2 #IHV1 -@(cpxs_trans … IHV1) /2 width=1/ +@(cpxs_trans … IHV1) -IHV1 /3 width=1/ qed. theorem cpxs_theta_rc: ∀h,g,a,L,V1,V,V2,W1,W2,T1,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V → ⇧[0, 1] V ≡ V2 → - ⦃h, L.ⓓW1⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ W1 ➡*[g] W2 → - ⦃h, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡*[g] ⓓ{a}W2.ⓐV2.T2. + ⦃h, L.ⓓW1⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ W1 ➡*[g] W2 → + ⦃h, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡*[g] ⓓ{a}W2.ⓐV2.T2. #h #g #a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HT12 #H elim H -W2 /2 width=3/ #W #W2 #_ #HW2 #IHW1 -@(cpxs_trans … IHW1) /2 width=1/ +@(cpxs_trans … IHW1) -IHW1 /2 width=1/ qed. theorem cpxs_theta: ∀h,g,a,L,V1,V,V2,W1,W2,T1,T2. ⇧[0, 1] V ≡ V2 → ⦃h, L⦄ ⊢ W1 ➡*[g] W2 → - ⦃h, L.ⓓW1⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ V1 ➡*[g] V → - ⦃h, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡*[g] ⓓ{a}W2.ⓐV2.T2. + ⦃h, L.ⓓW1⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ V1 ➡*[g] V → + ⦃h, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡*[g] ⓓ{a}W2.ⓐV2.T2. #h #g #a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV2 #HW12 #HT12 #H @(TC_ind_dx … V1 H) -V1 /2 width=3/ #V1 #V0 #HV10 #_ #IHV0 -@(cpxs_trans … IHV0) /2 width=1/ +@(cpxs_trans … IHV0) -IHV0 /2 width=1/ qed. +(* Advanced inversion lemmas ************************************************) + +lemma cpxs_inv_appl1: ∀h,g,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓐV1.T1 ➡*[g] U2 → + ∨∨ ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡*[g] V2 & ⦃h, L⦄ ⊢ T1 ➡*[g] T2 & + U2 = ⓐV2. T2 + | ∃∃a,W,T. ⦃h, L⦄ ⊢ T1 ➡*[g] ⓛ{a}W.T & ⦃h, L⦄ ⊢ ⓓ{a}ⓝW.V1.T ➡*[g] U2 + | ∃∃a,V0,V2,V,T. ⦃h, L⦄ ⊢ V1 ➡*[g] V0 & ⇧[0,1] V0 ≡ V2 & + ⦃h, L⦄ ⊢ T1 ➡*[g] ⓓ{a}V.T & ⦃h, L⦄ ⊢ ⓓ{a}V.ⓐV2.T ➡*[g] U2. +#h #g #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 [ /3 width=5/ ] +#U #U2 #_ #HU2 * * +[ #V0 #T0 #HV10 #HT10 #H destruct + elim (cpx_inv_appl1 … HU2) -HU2 * + [ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5/ + | #a #V2 #W #W2 #T #T2 #HV02 #HW2 #HT2 #H1 #H2 destruct + lapply (cpxs_strap1 … HV10 … HV02) -V0 #HV12 + lapply (lsubx_cpx_trans … HT2 (L.ⓓⓝW.V1) ?) -HT2 /2 width=1/ #HT2 + @or3_intro1 @(ex2_3_intro … HT10) -HT10 /3 width=1/ (**) (* explicit constructor. /5 width=8/ is too slow because TC_transitive gets in the way *) + | #a #V #V2 #W0 #W2 #T #T2 #HV0 #HV2 #HW02 #HT2 #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=9/ +| /4 width=11/ +] +qed-. + (* Properties on sn extended parallel reduction for local environments ******) lemma lpx_cpx_trans: ∀h,g. s_r_trans … (cpx h g) (lpx h g). @@ -77,11 +110,11 @@ lemma lpx_cpx_trans: ∀h,g. s_r_trans … (cpx h g) (lpx h g). lapply (cpxs_strap2 … HV10 … HV02) -V0 /2 width=7/ | #a #I #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #HL12 lapply (IHT12 (L1.ⓑ{I}V1) ?) -IHT12 /2 width=1/ /3 width=1/ -|5,7: /3 width=1/ +|5,7,8: /3 width=1/ | #L2 #V2 #T1 #T #T2 #_ #HT2 #IHT1 #L1 #HL12 lapply (IHT1 (L1.ⓓV2) ?) -IHT1 /2 width=1/ /2 width=3/ -| #a #L2 #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #HL12 - lapply (IHT12 (L1.ⓛW) ?) -IHT12 /2 width=1/ /3 width=1/ +| #a #L2 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L1 #HL12 + lapply (IHT12 (L1.ⓛW1) ?) -IHT12 /2 width=1/ /3 width=1/ | #a #L2 #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L1 #HL12 lapply (IHT12 (L1.ⓓW1) ?) -IHT12 /2 width=1/ /3 width=3/ ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma index e8478aa84..115a366f9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma @@ -24,17 +24,32 @@ lemma cpxs_fwd_cnx: ∀h,g,L,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ → ∀U. ⦃h, L >(cpxs_inv_cnx1 … H HT) -L -T // qed-. +lemma cpxs_fwd_sort: ∀h,g,L,U,k. ⦃h, L⦄ ⊢ ⋆k ➡*[g] U → + ⋆k ≃ U ∨ ⦃h, L⦄ ⊢ ⋆(next h k) ➡*[g] U. +#h #g #L #U #k #H +elim (cpxs_inv_sort1 … H) -H #n #l generalize in match k; -k @(nat_ind_plus … n) -n +[ #k #_ #H -l destruct /2 width=1/ +| #n #IHn #k >plus_plus_comm_23 #Hnl #H destruct + lapply (deg_next_SO … Hnl) -Hnl #Hnl + elim (IHn … Hnl) -IHn + [ #H lapply (tstc_inv_atom1 … H) -H #H >H -H /2 width=1/ + | generalize in match Hnl; -Hnl @(nat_ind_plus … n) -n /2 width=1/ + #n #_ /4 width=3/ + | >iter_SO >iter_n_Sm // + ] +] +qed-. + (* Basic_1: was just: pr3_iso_beta *) lemma cpxs_fwd_beta: ∀h,g,a,L,V,W,T,U. ⦃h, L⦄ ⊢ ⓐV.ⓛ{a}W.T ➡*[g] U → - ⓐV.ⓛ{a}W.T ≃ U ∨ - ∃∃T0. ⦃h, L.ⓛW⦄ ⊢ T ➡*[g] T0 & ⦃h, L⦄ ⊢ ⓓ{a}V.T0 ➡*[g] U. + ⓐV.ⓛ{a}W.T ≃ U ∨ ⦃h, L⦄ ⊢ ⓓ{a}ⓝW.V.T ➡*[g] U. #h #g #a #L #V #W #T #U #H elim (cpxs_inv_appl1 … H) -H * [ #V0 #T0 #_ #_ #H destruct /2 width=1/ -| #b #V0 #W0 #T0 #HV0 #HT0 #HU - elim (cpxs_inv_abst1 … HT0) -HT0 #W1 #T1 #_ #HT1 #H destruct -W1 - @or_intror @(ex2_intro … HT1) -W (**) (* explicit constructors *) - @(cpxs_trans … HU) -U /2 width=1/ +| #b #W0 #T0 #HT0 #HU + elim (cpxs_inv_abst1 … HT0) -HT0 #W1 #T1 #HW1 #HT1 #H destruct + lapply (lsubx_cpxs_trans … HT1 (L.ⓓⓝW.V) ?) -HT1 /2 width=1/ #HT1 + @or_intror @(cpxs_trans … HU) -U /3 width=1/ (**) (* explicit constructor *) | #b #V1 #V2 #V0 #T1 #_ #_ #HT1 #_ elim (cpxs_inv_abst1 … HT1) -HT1 #W2 #T2 #_ #_ #H destruct ] @@ -58,15 +73,15 @@ lemma cpxs_fwd_theta: ∀h,g,a,L,V1,V,T,U. ⦃h, L⦄ ⊢ ⓐV1.ⓓ{a}V.T ➡*[g #h #g #a #L #V1 #V #T #U #H #V2 #HV12 elim (cpxs_inv_appl1 … H) -H * [ -HV12 #V0 #T0 #_ #_ #H destruct /2 width=1/ -| #b #V0 #W #T0 #HV10 #HT0 #HU +| #b #W #T0 #HT0 #HU elim (cpxs_inv_abbr1 … HT0) -HT0 * [ #V3 #T3 #_ #_ #H destruct | #X #HT2 #H #H0 destruct elim (lift_inv_bind1 … H) -H #W2 #T2 #HW2 #HT02 #H destruct @or_intror @(cpxs_trans … HU) -U (**) (* explicit constructor *) @(cpxs_trans … (+ⓓV.ⓐV2.ⓛ{b}W2.T2)) [ /3 width=1/ ] -T - @(cpxs_strap2 … (ⓐV1.ⓛ{b}W.T0)) [ /5 width=7/ ] -V -V2 -W2 -T2 - @(cpxs_strap2 … (ⓓ{b}V1.T0)) [ /3 width=1/ ] -W /2 width=1/ + @(cpxs_strap2 … (ⓐV1.ⓛ{b}W.T0)) [2: /2 width=1/ ] + /4 width=7 by cpx_zeta, lift_bind, lift_flat/ (**) (* auto too slow without trace *) ] | #b #V3 #V4 #V0 #T0 #HV13 #HV34 #HT0 #HU @or_intror @(cpxs_trans … HU) -U (**) (* explicit constructor *) @@ -78,14 +93,14 @@ elim (cpxs_inv_appl1 … H) -H * elim (lift_inv_bind1 … H) -H #V5 #T5 #HV05 #HT05 #H destruct lapply (cpxs_lift … HV13 (L.ⓓV0) … HV12 … HV34) -V3 /2 width=1/ #HV24 @(cpxs_trans … (+ⓓV.ⓐV2.ⓓ{b}V5.T5)) [ /3 width=1/ ] -T - @(cpxs_strap2 … (ⓐV1.ⓓ{b}V0.T0)) [ /5 width=7/ ] -V -V5 -T5 + @(cpxs_strap2 … (ⓐV1.ⓓ{b}V0.T0)) [ /4 width=7 by cpx_zeta, lift_bind, lift_flat/ ] -V -V5 -T5 (**) (* auto too slow without trace *) @(cpxs_strap2 … (ⓓ{b}V0.ⓐV2.T0)) [ /3 width=3/ ] -V1 /3 width=1/ ] ] qed-. -lemma cpxs_fwd_tau: ∀h,g,L,W,T,U. ⦃h, L⦄ ⊢ ⓝW.T ➡*[g] U → - ⓝW. T ≃ U ∨ ⦃h, L⦄ ⊢ T ➡*[g] U. +lemma cpxs_fwd_cast: ∀h,g,L,W,T,U. ⦃h, L⦄ ⊢ ⓝW.T ➡*[g] U → + ∨∨ ⓝW. T ≃ U | ⦃h, L⦄ ⊢ T ➡*[g] U | ⦃h, L⦄ ⊢ W ➡*[g] U. #h #g #L #W #T #U #H elim (cpxs_inv_cast1 … H) -H /2 width=1/ * #W0 #T0 #_ #_ #H destruct /2 width=1/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma index dffa50fba..61f43dda6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma @@ -27,7 +27,7 @@ lemma cpxs_fwd_cnx_vector: ∀h,g,L,T. 𝐒⦃T⦄ → ⦃h, L⦄ ⊢ 𝐍[g] #V #Vs #IHVs #U #H elim (cpxs_inv_appl1 … H) -H * [ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1/ -| #a #V0 #W0 #T0 #HV0 #HT0 #HU +| #a #W0 #T0 #HT0 #HU lapply (IHVs … HT0) -IHVs -HT0 #HT0 elim (tstc_inv_bind_appls_simple … HT0) // | #a #V1 #V2 #V0 #T0 #HV1 #HV12 #HT0 #HU @@ -36,27 +36,48 @@ elim (cpxs_inv_appl1 … H) -H * ] qed-. +lemma cpxs_fwd_sort_vector: ∀h,g,L,k,Vs,U. ⦃h, L⦄ ⊢ ⒶVs.⋆k ➡*[g] U → + ⒶVs.⋆k ≃ U ∨ ⦃h, L⦄ ⊢ ⒶVs.⋆(next h k) ➡*[g] U. +#h #g #L #k #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_sort/ +#V #Vs #IHVs #U #H +elim (cpxs_inv_appl1 … H) -H * +[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1/ +| #a #W1 #T1 #HT1 #HU + elim (IHVs … HT1) -IHVs -HT1 #HT1 + [ elim (tstc_inv_bind_appls_simple … HT1) // + | @or_intror (**) (* explicit constructor *) + @(cpxs_trans … HU) -U + @(cpxs_strap1 … (ⓐV.ⓛ{a}W1.T1)) [ /2 width=1/ ] -Vs /3 width=1/ + ] +| #a #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU + elim (IHVs … HT1) -IHVs -HT1 #HT1 + [ elim (tstc_inv_bind_appls_simple … HT1) // + | @or_intror (**) (* explicit constructor *) + @(cpxs_trans … HU) -U + @(cpxs_strap1 … (ⓐV1.ⓓ{a}V3.T1)) [ /2 width=1/ ] -Vs /3 width=3/ + ] +] +qed-. + + (* Basic_1: was just: pr3_iso_appls_beta *) lemma cpxs_fwd_beta_vector: ∀h,g,a,L,Vs,V,W,T,U. ⦃h, L⦄ ⊢ ⒶVs.ⓐV.ⓛ{a}W.T ➡*[g] U → - ⒶVs. ⓐV. ⓛ{a}W. T ≃ U ∨ - ∃∃T0.⦃h, L.ⓛW⦄ ⊢ T ➡*[g] T0 & ⦃h, L⦄ ⊢ ⒶVs.ⓓ{a}V.T0 ➡*[g] U. + ⒶVs. ⓐV. ⓛ{a}W. T ≃ U ∨ ⦃h, L⦄ ⊢ ⒶVs.ⓓ{a}ⓝW.V.T ➡*[g] U. #h #g #a #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_beta/ #V0 #Vs #IHVs #V #W #T #U #H elim (cpxs_inv_appl1 … H) -H * [ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1/ -| #b #V1 #W1 #T1 #HV01 #HT1 #HU - elim (IHVs … HT1) -IHVs -HT1 - [ #HT1 elim (tstc_inv_bind_appls_simple … HT1) // - | * #T0 #HT0 #HT01 - @or_intror @(ex2_intro … HT0) -W (**) (* explicit constructor *) +| #b #W1 #T1 #HT1 #HU + elim (IHVs … HT1) -IHVs -HT1 #HT1 + [ elim (tstc_inv_bind_appls_simple … HT1) // + | @or_intror (**) (* explicit constructor *) @(cpxs_trans … HU) -U - @(cpxs_strap1 … (ⓐV1.ⓛ{b}W1.T1)) [ /2 width=1/ ] -V -V0 -Vs -T /3 width=1/ + @(cpxs_strap1 … (ⓐV0.ⓛ{b}W1.T1)) [ /2 width=1/ ] -V -Vs -T /3 width=1/ ] | #b #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU - elim (IHVs … HT1) -IHVs -HT1 - [ #HT1 elim (tstc_inv_bind_appls_simple … HT1) // - | * #T0 #HT0 #HT01 - @or_intror @(ex2_intro … HT0) -W (**) (* explicit constructor *) + elim (IHVs … HT1) -IHVs -HT1 #HT1 + [ elim (tstc_inv_bind_appls_simple … HT1) // + | @or_intror (**) (* explicit constructor *) @(cpxs_trans … HU) -U @(cpxs_strap1 … (ⓐV1.ⓓ{b}V3.T1)) [ /2 width=1/ ] -V -V0 -Vs -T /3 width=3/ ] @@ -71,12 +92,12 @@ lemma cpxs_fwd_delta_vector: ∀h,g,I,L,K,V1,i. ⇩[0, i] L ≡ K.ⓑ{I}V1 → #V #Vs #IHVs #U #H -K -V1 elim (cpxs_inv_appl1 … H) -H * [ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1/ -| #b #V0 #W0 #T0 #HV0 #HT0 #HU +| #b #W0 #T0 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0 [ elim (tstc_inv_bind_appls_simple … HT0) // | @or_intror -i (**) (* explicit constructor *) @(cpxs_trans … HU) -U - @(cpxs_strap1 … (ⓐV0.ⓛ{b}W0.T0)) [ /2 width=1/ ] -V -V2 -Vs /3 width=1/ + @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) [ /2 width=1/ ] -V2 -Vs /3 width=1/ ] | #b #V0 #V1 #V3 #T0 #HV0 #HV01 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0 @@ -101,19 +122,19 @@ elim HV12s -V1s -V2s /2 width=1 by cpxs_fwd_theta/ #V1s #V2s #V1b #V2b #HV12b #_ #IHV12s #V1a #V2a #HV12a #V #T #U #H elim (cpxs_inv_appl1 … H) -H * [ -IHV12s -HV12a -HV12b #V0 #T0 #_ #_ #H destruct /2 width=1/ -| #b #V0a #W0 #T0 #HV10a #HT0 #HU +| #b #W0 #T0 #HT0 #HU elim (IHV12s … HV12b … HT0) -IHV12s -HT0 #HT0 - [ -HV12a -HV12b -HV10a -HU + [ -HV12a -HV12b -HU elim (tstc_inv_pair1 … HT0) #V1 #T1 #H destruct | @or_intror -V1s (**) (* explicit constructor *) @(cpxs_trans … HU) -U elim (cpxs_inv_abbr1 … HT0) -HT0 * - [ -HV12a -HV12b -HV10a #V1 #T1 #_ #_ #H destruct + [ -HV12a -HV12b #V1 #T1 #_ #_ #H destruct | -V1b #X #HT1 #H #H0 destruct elim (lift_inv_bind1 … H) -H #W1 #T1 #HW01 #HT01 #H destruct @(cpxs_trans … (+ⓓV.ⓐV2a.ⓛ{b}W1.T1)) [ /3 width=1/ ] -T -V2b -V2s - @(cpxs_strap2 … (ⓐV1a.ⓛ{b}W0.T0)) [ /5 width=7/ ] -V -V2a -W1 -T1 - @(cpxs_strap2 … (ⓓ{b}V1a.T0)) [ /3 width=1/ ] -W0 /2 width=1/ + @(cpxs_strap2 … (ⓐV1a.ⓛ{b}W0.T0)) [2: /2 width=1/ ] + /4 width=7 by cpx_zeta, lift_bind, lift_flat/ (* auto too slow without trace *) ] ] | #b #V0a #Va #V0 #T0 #HV10a #HV0a #HT0 #HU @@ -130,7 +151,7 @@ elim (cpxs_inv_appl1 … H) -H * elim (lift_inv_bind1 … H) -H #V1 #T1 #HW01 #HT01 #H destruct lapply (cpxs_lift … HV10a (L.ⓓV0) … HV12a … HV0a) -V0a [ /2 width=1/ ] #HV2a @(cpxs_trans … (+ⓓV.ⓐV2a.ⓓ{b}V1.T1)) [ /3 width=1/ ] -T -V2b -V2s - @(cpxs_strap2 … (ⓐV1a.ⓓ{b}V0.T0)) [ /5 width=7/ ] -V -V1 -T1 + @(cpxs_strap2 … (ⓐV1a.ⓓ{b}V0.T0)) [ /4 width=7 by cpx_zeta, lift_bind, lift_flat/ ] -V -V1 -T1 (* auto too slow without trace *) @(cpxs_strap2 … (ⓓ{b}V0.ⓐV2a.T0)) [ /3 width=3/ ] -V1a /3 width=1/ ] ] @@ -138,25 +159,33 @@ elim (cpxs_inv_appl1 … H) -H * qed-. (* Basic_1: was just: pr3_iso_appls_cast *) -lemma cpxs_fwd_tau_vector: ∀h,g,L,Vs,W,T,U. ⦃h, L⦄ ⊢ ⒶVs.ⓝW.T ➡*[g] U → - ⒶVs. ⓝW. T ≃ U ∨ ⦃h, L⦄ ⊢ ⒶVs.T ➡*[g] U. -#h #g #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_tau/ +lemma cpxs_fwd_cast_vector: ∀h,g,L,Vs,W,T,U. ⦃h, L⦄ ⊢ ⒶVs.ⓝW.T ➡*[g] U → + ∨∨ ⒶVs. ⓝW. T ≃ U + | ⦃h, L⦄ ⊢ ⒶVs.T ➡*[g] U + | ⦃h, L⦄ ⊢ ⒶVs.W ➡*[g] U. +#h #g #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_cast/ #V #Vs #IHVs #W #T #U #H elim (cpxs_inv_appl1 … H) -H * [ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1/ -| #b #V0 #W0 #T0 #HV0 #HT0 #HU +| #b #W0 #T0 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0 [ elim (tstc_inv_bind_appls_simple … HT0) // - | @or_intror -W (**) (* explicit constructor *) + | @or3_intro1 -W (**) (* explicit constructor *) + @(cpxs_trans … HU) -U + @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) /2 width=1/ + | @or3_intro2 -T (**) (* explicit constructor *) @(cpxs_trans … HU) -U - @(cpxs_strap1 … (ⓐV0.ⓛ{b}W0.T0)) [ /2 width=1/ ] -V -Vs -T /3 width=1/ + @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) /2 width=1/ ] | #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 *) + | @or3_intro1 -W (**) (* explicit constructor *) + @(cpxs_trans … HU) -U + @(cpxs_strap1 … (ⓐV0.ⓓ{b}V2.T0)) [ /2 width=1/ ] -V -Vs -T /2 width=3/ + | @or3_intro2 -T (**) (* explicit constructor *) @(cpxs_trans … HU) -U - @(cpxs_strap1 … (ⓐV0.ⓓ{b}V2.T0)) [ /2 width=1/ ] -V -Vs -T /3 width=3/ + @(cpxs_strap1 … (ⓐV0.ⓓ{b}V2.T0)) [ /2 width=1/ ] -V -Vs -W /2 width=3/ ] ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn.ma index 92719458e..08709419c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csn.ma @@ -43,10 +43,6 @@ lemma csn_intro: ∀h,g,L,T1. ⦃h, L⦄ ⊢ ⬊*[g] T1. /4 width=1/ qed. -(* Basic_1: was just: sn3_nf2 *) -lemma cnx_csn: ∀h,g,L,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ → ⦃h, L⦄ ⊢ ⬊*[g] T. -/2 width=1/ qed. - lemma csn_cpx_trans: ∀h,g,L,T1. ⦃h, L⦄ ⊢ ⬊*[g] T1 → ∀T2. ⦃h, L⦄ ⊢ T1 ➡[g] T2 → ⦃h, L⦄ ⊢ ⬊*[g] T2. #h #g #L #T1 #H elim H -T1 #T1 #HT1 #IHT1 #T2 #HLT12 @@ -56,10 +52,24 @@ elim (term_eq_dec T1 T2) #HT12 | -HT1 -HT2 /3 width=4/ qed-. +(* Basic_1: was just: sn3_nf2 *) +lemma cnx_csn: ∀h,g,L,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ → ⦃h, L⦄ ⊢ ⬊*[g] T. +/2 width=1/ qed. + +lemma cnx_sort: ∀h,g,L,k. ⦃h, L⦄ ⊢ ⬊*[g] ⋆k. +#h #g #L #k elim (deg_total h g k) +#l generalize in match k; -k @(nat_ind_plus … l) -l /3 width=1/ +#l #IHl #k #Hkl lapply (deg_next_SO … Hkl) -Hkl +#Hkl @csn_intro #X #H #HX elim (cpx_inv_sort1 … H) -H +[ #H destruct elim HX // +| -HX * #l0 #_ #H destruct -l0 /2 width=1/ +] +qed. + (* Basic_1: was just: sn3_cast *) lemma csn_cast: ∀h,g,L,W. ⦃h, L⦄ ⊢ ⬊*[g] W → ∀T. ⦃h, L⦄ ⊢ ⬊*[g] T → ⦃h, L⦄ ⊢ ⬊*[g] ⓝW.T. -#h #g #L #W #HW elim HW -W #W #_ #IHW #T #HT @(csn_ind … HT) -T #T #HT #IHT +#h #g #L #W #HW @(csn_ind … HW) -W #W #HW #IHW #T #HT @(csn_ind … HT) -T #T #HT #IHT @csn_intro #X #H1 #H2 elim (cpx_inv_cast1 … H1) -H1 [ * #W0 #T0 #HLW0 #HLT0 #H destruct @@ -67,7 +77,7 @@ elim (cpx_inv_cast1 … H1) -H1 [ /3 width=3 by csn_cpx_trans/ | -HLW0 * #H destruct /3 width=1/ ] -| /3 width=3 by csn_cpx_trans/ +|2,3: /3 width=3 by csn_cpx_trans/ ] qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_aaa.ma index 9932205f8..cd8d5a64b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_aaa.ma @@ -15,11 +15,11 @@ include "basic_2/computation/acp_aaa.ma". include "basic_2/computation/csn_tstc_vector.ma". -(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) +(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) (* Main properties concerning atomic arity assignment ***********************) -theorem csn_aaa: ∀L,T,A. L ⊢ T ⁝ A → L ⊢ ⬊* T. -#L #T #A #H -@(acp_aaa … csn_acp csn_acr … H) +theorem csn_aaa: ∀h,g,L,T,A. L ⊢ T ⁝ A → ⦃h, L⦄ ⊢ ⬊*[g] T. +#h #g #L #T #A #H +@(acp_aaa … (csn_acp h g) (csn_acr h g) … H) qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma index 21d97b774..e57f37d9d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma @@ -96,5 +96,6 @@ theorem csn_acp: ∀h,g. acp (cpx h g) (eq …) (csn h g). #l #Hl lapply (cnx_sort_iter … L … Hl) /2 width=2/ | @cnx_lift | /2 width=3 by csn_fwd_flat_dx/ +| /2 width=1/ ] qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lpx.ma index 7fcc3fa0e..9a57a2ca5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lpx.ma @@ -58,43 +58,26 @@ elim (cpx_inv_abbr1 … H1) -H1 * ] qed. -fact csn_appl_beta_aux: ∀h,g,a,L,U1. ⦃h, L⦄ ⊢ ⬊*[g] U1 → ∀V. ⦃h, L⦄ ⊢ ⬊*[g] V → - ∀W,T1. U1 = ⓛ{a}W.T1 → ( - ∀T2. ⦃h, L.ⓛW⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ ⬊*[g] ⓓ{a}V.T2 - ) → ⦃h, L⦄ ⊢ ⬊*[g] ⓐV.ⓛ{a}W.T1. -#h #g #a #L #X1 #H @(csn_ind … H) -X1 -#X1 #HT1 #IHT1 #X2 #H @(csn_ind … H) -X2 -#V #HV #IHV #W #T1 #H1 #IHT2 destruct +fact csn_appl_beta_aux: ∀h,g,a,L,U1. ⦃h, L⦄ ⊢ ⬊*[g] U1 → + ∀V,W,T1. U1 = ⓓ{a}ⓝW.V.T1 → ⦃h, L⦄ ⊢ ⬊*[g] ⓐV.ⓛ{a}W.T1. +#h #g #a #L #X #H @(csn_ind … H) -X +#X #HT1 #IHT1 #V #W #T1 #H1 destruct @csn_intro #X #H1 #H2 elim (cpx_inv_appl1 … H1) -H1 * -[ #V0 #Y #HLV0 #H #H0 destruct +[ -HT1 #V0 #Y #HLV0 #H #H0 destruct elim (cpx_inv_abst1 … H) -H #W0 #T0 #HLW0 #HLT0 #H destruct - elim (eq_false_inv_tpair_dx … H2) -H2 - [ lapply (csn_cpx_trans … HV … HLV0) -HV #HV0 #HWT0 - @IHT1 -IHT1 [4,5: // |1: skip |2,3: /2 width=1/ ] -HWT0 -HV0 #T2 #HT02 - lapply (lpx_cpxs_trans … HT02 (L.ⓛW) ?) [ /2 width=1/ ] -W0 #HT02 - lapply (cpxs_strap2 … HLT0 … HT02) -T0 #HT12 - lapply (IHT2 … HT12) -T1 #HT2 - @(csn_cpx_trans … HT2) -HT2 /2 width=1/ - | -HV -HT1 -IHT1 -HLW0 -HLT0 * #H #HV0 destruct - @IHV -IHV [1,3: // |2: /2 width=1/ ] -HV0 #T2 #HT02 - lapply (IHT2 … HT02) -IHT2 -HT02 #HT2 - @(csn_cpx_trans … HT2) -HT2 /2 width=1/ - ] -| -HT1 -IHT1 -HV -IHV -H2 #b #V0 #W0 #T0 #T3 #HLV0 #HLT01 #H1 #H2 destruct - lapply (IHT2 T3 ?) [ /2 width=1/ ] -IHT2 -HLT01 #HT3 - @(csn_cpx_trans … HT3) -HT3 /2 width=1/ -| -HT1 -IHT1 -HV -IHV -IHT2 -H2 #b #V0 #V1 #W0 #W1 #T0 #T3 #_ #_ #_ #_ #H destruct + @IHT1 -IHT1 [4: // | skip |3: #H destruct /2 width=1/ ] -H2 + lapply (lsubx_cpx_trans … HLT0 (L.ⓓⓝW.V) ?) -HLT0 [ /2 width=1/ ] /3 width=1/ +| -IHT1 -H2 #b #V0 #W0 #W2 #T0 #T2 #HLV0 #HLW02 #HLT02 #H1 #H3 destruct + lapply (lsubx_cpx_trans … HLT02 (L.ⓓⓝW0.V) ?) -HLT02 [ /2 width=1/ ] #HT02 + @(csn_cpx_trans … HT1) -HT1 /3 width=1/ +| -HT1 -IHT1 -H2 #b #V0 #V1 #W0 #W1 #T0 #T3 #_ #_ #_ #_ #H destruct ] qed-. (* Basic_1: was just: sn3_beta *) -lemma csn_appl_beta: ∀h,g,a,L,W,T1. ⦃h, L⦄ ⊢ ⬊*[g] ⓛ{a}W.T1 → ∀V. ( - ∀T2. ⦃h, L.ⓛW⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ ⬊*[g] ⓓ{a}V.T2 - ) → ⦃h, L⦄ ⊢ ⬊*[g] ⓐV.ⓛ{a}W.T1. -#h #g #a #L #W #T1 #HWT1 #V #IHT2 lapply (IHT2 T1 ?) // -#HVT1 lapply (csn_fwd_pair_sn … HVT1) -HVT1 -/3 width=3 by csn_appl_beta_aux/ qed. +lemma csn_appl_beta: ∀h,g,a,L,V,W,T. ⦃h, L⦄ ⊢ ⬊*[g] ⓓ{a}ⓝW.V.T → ⦃h, L⦄ ⊢ ⬊*[g] ⓐV.ⓛ{a}W.T. +/2 width=3 by csn_appl_beta_aux/ qed. fact csn_appl_theta_aux: ∀h,g,a,L,U. ⦃h, L⦄ ⊢ ⬊*[g] U → ∀V1,V2. ⇧[0, 1] V1 ≡ V2 → ∀V,T. U = ⓓ{a}V.ⓐV2.T → ⦃h, L⦄ ⊢ ⬊*[g] ⓐV1.ⓓ{a}V.T. @@ -124,7 +107,7 @@ elim (cpx_inv_appl1 … HL) -HL * lapply (csn_inv_lift … L … 1 HVT0 ? ? ?) -HVT0 [ /2 width=4/ |2,3: skip | /2 width=1/ ] -V2 -T0 #HVY @(csn_cpx_trans … HVY) /2 width=1/ ] -| -HV -HV12 -HVT -IHVT -H #b #V0 #W0 #T0 #T1 #_ #_ #H destruct +| -HV -HV12 -HVT -IHVT -H #b #V0 #W0 #W1 #T0 #T1 #_ #_ #_ #H destruct | -IHVT -H #b #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HV03 #HLW01 #HLT01 #H1 #H2 destruct lapply (cpx_lift … HLV10 (L. ⓓW0) … HV12 … HV03) -HLV10 -HV12 -HV03 /2 width=1/ #HLV23 @csn_abbr /2 width=3 by csn_cpx_trans/ -HV @@ -143,7 +126,7 @@ lemma csn_appl_simple_tstc: ∀h,g,L,V. ⦃h, L⦄ ⊢ ⬊*[g] V → ∀T1. ⦃h 𝐒⦃T1⦄ → ⦃h, L⦄ ⊢ ⬊*[g] ⓐV.T1. #h #g #L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #H @(csn_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1 @csn_intro #X #HL #H -elim (cpx_inv_appl1_simple … HL ?) -HL // +elim (cpx_inv_appl1_simple … HL) -HL // #V0 #T0 #HLV0 #HLT10 #H0 destruct elim (eq_false_inv_tpair_sn … H) -H [ -IHT1 #HV0 diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_tstc_vector.ma index 7ed4cb5db..123704979 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_tstc_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_tstc_vector.ma @@ -13,105 +13,119 @@ (**************************************************************************) include "basic_2/computation/acp_cr.ma". -include "basic_2/computation/cprs_tstc_vector.ma". -include "basic_2/computation/csn_lpr.ma". +include "basic_2/computation/cpxs_tstc_vector.ma". +include "basic_2/computation/csn_lpx.ma". include "basic_2/computation/csn_vector.ma". -(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERM VECTORS **********************) +(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERM VECTORS *************) (* Advanced properties ******************************************************) -(* Basic_1: was only: sn3_appls_lref *) -lemma csn_applv_cnf: ∀L,T. 𝐒⦃T⦄ → L ⊢ 𝐍⦃T⦄ → - ∀Vs. L ⊢ ⬊* Vs → L ⊢ ⬊* ⒶVs.T. -#L #T #H1T #H2T #Vs elim Vs -Vs [ #_ @(csn_cnf … H2T) ] (**) (* /2 width=1/ does not work *) +(* Basic_1: was just: sn3_appls_lref *) +lemma csn_applv_cnx: ∀h,g,L,T. 𝐒⦃T⦄ → ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ → + ∀Vs. ⦃h, L⦄ ⊢ ⬊*[g] Vs → ⦃h, L⦄ ⊢ ⬊*[g] ⒶVs.T. +#h #g #L #T #H1T #H2T #Vs elim Vs -Vs [ #_ @(cnx_csn … H2T) ] (**) (* /2 width=1/ does not work *) #V #Vs #IHV #H elim (csnv_inv_cons … H) -H #HV #HVs @csn_appl_simple_tstc // -HV /2 width=1/ -IHV -HVs #X #H #H0 -lapply (cprs_fwd_cnf_vector … H) -H // -H1T -H2T #H -elim (H0 ?) -H0 // +lapply (cpxs_fwd_cnx_vector … H) -H // -H1T -H2T #H +elim (H0) -H0 // qed. -(* Basic_1: was: sn3_appls_beta *) -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 +lemma csn_applv_sort: ∀h,g,L,k,Vs. ⦃h, L⦄ ⊢ ⬊*[g] Vs → ⦃h, L⦄ ⊢ ⬊*[g] ⒶVs.⋆k. +#h #g #L #k elim (deg_total h g k) +#l generalize in match k; -k @(nat_ind_plus … l) -l [ /3 width=1/ ] +#l #IHl #k #Hkl lapply (deg_next_SO … Hkl) -Hkl +#Hkl #Vs elim Vs -Vs /2 width=1/ +#V #Vs #IHVs #HVVs +elim (csnv_inv_cons … HVVs) #HV #HVs +@csn_appl_simple_tstc // -HV /2 width=1/ -IHVs -HVs +#X #H #H0 +elim (cpxs_fwd_sort_vector … H) -H #H +[ elim H0 -H0 // +| -H0 @(csn_cpxs_trans … (Ⓐ(V@Vs).⋆(next h k))) /2 width=1/ +] +qed. + +(* Basic_1: was just: sn3_appls_beta *) +lemma csn_applv_beta: ∀h,g,a,L,Vs,V,W,T. ⦃h, L⦄ ⊢ ⬊*[g] ⒶVs.ⓓ{a}ⓝW.V.T → + ⦃h, L⦄ ⊢ ⬊*[g] ⒶVs. ⓐV.ⓛ{a}W.T. +#h #g #a #L #Vs elim Vs -Vs /2 width=1/ +#V0 #Vs #IHV #V #W #T #H1T lapply (csn_fwd_pair_sn … H1T) #HV0 lapply (csn_fwd_flat_dx … H1T) #H2T @csn_appl_simple_tstc // -HV0 /2 width=1/ -IHV -H2T #X #H #H0 -elim (cprs_fwd_beta_vector … H) -H #H -[ -H1T elim (H0 ?) -H0 // -| -H0 @(csn_cprs_trans … H1T) -H1T /2 width=1/ +elim (cpxs_fwd_beta_vector … H) -H #H +[ -H1T elim H0 -H0 // +| -H0 @(csn_cpxs_trans … H1T) -H1T /2 width=1/ ] qed. -lemma csn_applv_delta: ∀L,K,V1,i. ⇩[0, i] L ≡ K. ⓓV1 → +lemma csn_applv_delta: ∀h,g,I,L,K,V1,i. ⇩[0, i] L ≡ K.ⓑ{I}V1 → ∀V2. ⇧[0, i + 1] V1 ≡ V2 → - ∀Vs.L ⊢ ⬊* (ⒶVs. V2) → L ⊢ ⬊* (ⒶVs. #i). -#L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs + ∀Vs. ⦃h, L⦄ ⊢ ⬊*[g] (ⒶVs.V2) → ⦃h, L⦄ ⊢ ⬊*[g] (ⒶVs.#i). +#h #g #I #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs [ #H lapply (ldrop_fwd_ldrop2 … HLK) #HLK0 - lapply (csn_inv_lift … H … HLK0 HV12) -V2 -HLK0 /2 width=4/ + lapply (csn_inv_lift … H … HLK0 HV12) -V2 -HLK0 /2 width=5/ | #V #Vs #IHV #H1T lapply (csn_fwd_pair_sn … H1T) #HV lapply (csn_fwd_flat_dx … H1T) #H2T @csn_appl_simple_tstc // -HV /2 width=1/ -IHV -H2T #X #H #H0 - elim (cprs_fwd_delta_vector … HLK … HV12 … H) -HLK -HV12 -H #H - [ -H1T elim (H0 ?) -H0 // - | -H0 @(csn_cprs_trans … H1T) -H1T /2 width=1/ + elim (cpxs_fwd_delta_vector … HLK … HV12 … H) -HLK -HV12 -H #H + [ -H1T elim H0 -H0 // + | -H0 @(csn_cpxs_trans … H1T) -H1T /2 width=1/ ] ] qed. -(* Basic_1: was: sn3_appls_abbr *) -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/ +(* Basic_1: was just: sn3_appls_abbr *) +lemma csn_applv_theta: ∀h,g,a,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → + ∀V,T. ⦃h, L⦄ ⊢ ⬊*[g] ⓓ{a}V.ⒶV2s.T → + ⦃h, L⦄ ⊢ ⬊*[g] ⒶV1s.ⓓ{a}V.T. +#h #g #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/ -#V1s #V2s #V1 #V2 #HV12 #HV12s #IHV12s #W1 #W2 #HW12 #V #T #H #HV +#V1s #V2s #V1 #V2 #HV12 #HV12s #IHV12s #W1 #W2 #HW12 #V #T #H lapply (csn_appl_theta … HW12 … H) -H -HW12 #H lapply (csn_fwd_pair_sn … H) #HW1 lapply (csn_fwd_flat_dx … H) #H1 -@csn_appl_simple_tstc // -HW1 /2 width=3/ -IHV12s -HV -H1 #X #H1 #H2 -elim (cprs_fwd_theta_vector … (V2@V2s) … H1) -H1 /2 width=1/ -HV12s -HV12 -[ -H #H elim (H2 ?) -H2 // -| -H2 #H1 @(csn_cprs_trans … H) -H /2 width=1/ +@csn_appl_simple_tstc // -HW1 /2 width=3/ -IHV12s -H1 #X #H1 #H2 +elim (cpxs_fwd_theta_vector … (V2@V2s) … H1) -H1 /2 width=1/ -HV12s -HV12 +[ -H #H elim H2 -H2 // +| -H2 #H1 @(csn_cpxs_trans … H) -H /2 width=1/ ] qed. -(* Basic_1: was: sn3_appls_cast *) -lemma csn_applv_tau: ∀L,W. L ⊢ ⬊* W → - ∀Vs,T. L ⊢ ⬊* ⒶVs. T → - L ⊢ ⬊* ⒶVs. ⓝW. T. -#L #W #HW #Vs elim Vs -Vs /2 width=1/ -HW -#V #Vs #IHV #T #H1T -lapply (csn_fwd_pair_sn … H1T) #HV +(* Basic_1: was just: sn3_appls_cast *) +lemma csn_applv_cast: ∀h,g,L,Vs,W,T. ⦃h, L⦄ ⊢ ⬊*[g] ⒶVs.W → ⦃h, L⦄ ⊢ ⬊*[g] ⒶVs.T → + ⦃h, L⦄ ⊢ ⬊*[g] ⒶVs.ⓝW.T. +#h #g #L #Vs elim Vs -Vs /2 width=1/ +#V #Vs #IHV #W #T #H1W #H1T +lapply (csn_fwd_pair_sn … H1W) #HV +lapply (csn_fwd_flat_dx … H1W) #H2W lapply (csn_fwd_flat_dx … H1T) #H2T -@csn_appl_simple_tstc // -HV /2 width=1/ -IHV -H2T +@csn_appl_simple_tstc // -HV /2 width=1/ -IHV -H2W -H2T #X #H #H0 -elim (cprs_fwd_tau_vector … H) -H #H -[ -H1T elim (H0 ?) -H0 // -| -H0 @(csn_cprs_trans … H1T) -H1T /2 width=1/ +elim (cpxs_fwd_cast_vector … H) -H #H +[ -H1W -H1T elim H0 -H0 // +| -H1W -H0 @(csn_cpxs_trans … H1T) -H1T /2 width=1/ +| -H1T -H0 @(csn_cpxs_trans … H1W) -H1W /2 width=1/ ] qed. -theorem csn_acr: acr cpr (eq …) (csn …) (λL,T. L ⊢ ⬊* T). -@mk_acr // +theorem csn_acr: ∀h,g. acr (cpx h g) (eq …) (csn h g) (λL,T. ⦃h, L⦄ ⊢ ⬊*[g] T). +#h #g @mk_acr // [ /3 width=1/ -| /2 width=1/ -| /2 width=6/ -| #L #V1 #V2 #HV12 #a #V #T #H #HVT - @(csn_applv_theta … HV12) -HV12 // +|2,3,6: /2 width=1/ +| /2 width=7/ +| #L #V1s #V2s #HV12s #a #V #T #H #HV + @(csn_applv_theta … HV12s) -HV12s @(csn_abbr) // -| /2 width=1/ | @csn_lift ] qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_vector.ma index a0f887d6f..c655be403 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_vector.ma @@ -15,24 +15,26 @@ include "basic_2/grammar/term_vector.ma". include "basic_2/computation/csn.ma". -(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERM VECTORS **********************) +(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERM VECTORS *************) -definition csnv: lenv → predicate (list term) ≝ - λL. all … (csn L). +definition csnv: ∀h. sd h → lenv → predicate (list term) ≝ + λh,g,L. all … (csn h g L). interpretation "context-sensitive strong normalization (term vector)" - 'SN L Ts = (csnv L Ts). + 'SN h g L Ts = (csnv h g L Ts). (* Basic inversion lemmas ***************************************************) -lemma csnv_inv_cons: ∀L,T,Ts. L ⊢ ⬊* T @ Ts → L ⊢ ⬊* T ∧ L ⊢ ⬊* Ts. +lemma csnv_inv_cons: ∀h,g,L,T,Ts. ⦃h, L⦄ ⊢ ⬊*[g] T @ Ts → + ⦃h, L⦄ ⊢ ⬊*[g] T ∧ ⦃h, L⦄ ⊢ ⬊*[g] Ts. normalize // qed-. (* Basic forward lemmas *****************************************************) -lemma csn_fwd_applv: ∀L,T,Vs. L ⊢ ⬊* Ⓐ Vs. T → L ⊢ ⬊* Vs ∧ L ⊢ ⬊* T. -#L #T #Vs elim Vs -Vs /2 width=1/ +lemma csn_fwd_applv: ∀h,g,L,T,Vs. ⦃h, L⦄ ⊢ ⬊*[g] Ⓐ Vs.T → + ⦃h, L⦄ ⊢ ⬊*[g] Vs ∧ ⦃h, L⦄ ⊢ ⬊*[g] T. +#h #g #L #T #Vs elim Vs -Vs /2 width=1/ #V #Vs #IHVs #HVs lapply (csn_fwd_pair_sn … HVs) #HV lapply (csn_fwd_flat_dx … HVs) -HVs #HVs diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs.ma index 2b3dc50cb..3f2b0fb09 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs.ma @@ -21,7 +21,7 @@ definition dxprs: ∀h. sd h → lenv → relation term ≝ λh,g,L,T1,T2. ∃∃T. ⦃h, L⦄ ⊢ T1 •*[g] T & L ⊢ T ➡* T2. interpretation "decomposed extended parallel computation (term)" - 'DecomposedXPRedStar h g L T1 T2 = (dxprs h g L T1 T2). + 'DecomposedPRedStar h g L T1 T2 = (dxprs h g L T1 T2). (* Basic properties *********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_aaa.ma index 80b0c7ceb..b2ad6412e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_aaa.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/unfold/sstas_aaa.ma". -include "basic_2/computation/cprs_aaa.ma". +include "basic_2/computation/cpxs_aaa.ma". include "basic_2/computation/dxprs.ma". (* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs.ma index 2f979ae46..83f2459e8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs.ma @@ -40,9 +40,10 @@ qed-. (* Basic properties *********************************************************) -lemma lprs_lpxs: ∀h,g,L1,L2. L1 ⊢ ➡* L2 → ⦃h, L1⦄ ⊢ ➡*[g] L2. +axiom lprs_lpxs: ∀h,g,L1,L2. L1 ⊢ ➡* L2 → ⦃h, L1⦄ ⊢ ➡*[g] L2. +(* /3 width=3/ qed. - +*) lemma lpx_lpxs: ∀h,g,L1,L2. ⦃h, L1⦄ ⊢ ➡[g] L2 → ⦃h, L1⦄ ⊢ ➡*[g] L2. /2 width=1/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma index bcf6c7714..a3cc36b24 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma @@ -20,8 +20,8 @@ include "basic_2/computation/acp_cr.ma". inductive lsubc (RP:lenv→predicate term): relation lenv ≝ | lsubc_atom: lsubc RP (⋆) (⋆) | lsubc_pair: ∀I,L1,L2,V. lsubc RP L1 L2 → lsubc RP (L1. ⓑ{I} V) (L2. ⓑ{I} V) -| lsubc_abbr: ∀L1,L2,V,W,A. ⦃L1, V⦄ ϵ[RP] 〚A〛 → L2 ⊢ W ⁝ A → - lsubc RP L1 L2 → lsubc RP (L1. ⓓV) (L2. ⓛW) +| lsubc_abbr: ∀L1,L2,V,W,A. ⦃L1, V⦄ ϵ[RP] 〚A〛 → ⦃L1, W⦄ ϵ[RP] 〚A〛 → L2 ⊢ W ⁝ A → + lsubc RP L1 L2 → lsubc RP (L1. ⓓⓝW.V) (L2. ⓛW) . interpretation @@ -34,69 +34,69 @@ fact lsubc_inv_atom1_aux: ∀RP,L1,L2. L1 ⊑[RP] L2 → L1 = ⋆ → L2 = ⋆. #RP #L1 #L2 * -L1 -L2 [ // | #I #L1 #L2 #V #_ #H destruct -| #L1 #L2 #V #W #A #_ #_ #_ #H destruct +| #L1 #L2 #V #W #A #_ #_ #_ #_ #H destruct ] -qed. +qed-. -(* Basic_1: was: csubc_gen_sort_r *) +(* Basic_1: was just: csubc_gen_sort_r *) lemma lsubc_inv_atom1: ∀RP,L2. ⋆ ⊑[RP] L2 → L2 = ⋆. -/2 width=4/ qed-. +/2 width=4 by lsubc_inv_atom1_aux/ qed-. -fact lsubc_inv_pair1_aux: ∀RP,L1,L2. L1 ⊑[RP] L2 → ∀I,K1,V. L1 = K1. ⓑ{I} V → - (∃∃K2. K1 ⊑[RP] K2 & L2 = K2. ⓑ{I} V) ∨ - ∃∃K2,W,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A & - K1 ⊑[RP] K2 & - L2 = K2. ⓛW & I = Abbr. +fact lsubc_inv_pair1_aux: ∀RP,L1,L2. L1 ⊑[RP] L2 → ∀I,K1,X. L1 = K1.ⓑ{I}X → + (∃∃K2. K1 ⊑[RP] K2 & L2 = K2. ⓑ{I}X) ∨ + ∃∃K2,V,W,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & ⦃K1, W⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A & + K1 ⊑[RP] K2 & + L2 = K2. ⓛW & X = ⓝW.V & I = Abbr. #RP #L1 #L2 * -L1 -L2 [ #I #K1 #V #H destruct | #J #L1 #L2 #V #HL12 #I #K1 #W #H destruct /3 width=3/ -| #L1 #L2 #V1 #W2 #A #HV1 #HW2 #HL12 #I #K1 #V #H destruct /3 width=7/ +| #L1 #L2 #V1 #W2 #A #HV1 #H1W2 #H2W2 #HL12 #I #K1 #V #H destruct /3 width=10/ ] -qed. +qed-. (* Basic_1: was: csubc_gen_head_r *) -lemma lsubc_inv_pair1: ∀RP,I,K1,L2,V. K1. ⓑ{I} V ⊑[RP] L2 → - (∃∃K2. K1 ⊑[RP] K2 & L2 = K2. ⓑ{I} V) ∨ - ∃∃K2,W,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A & - K1 ⊑[RP] K2 & - L2 = K2. ⓛW & I = Abbr. -/2 width=3/ qed-. +lemma lsubc_inv_pair1: ∀RP,I,K1,L2,X. K1.ⓑ{I}X ⊑[RP] L2 → + (∃∃K2. K1 ⊑[RP] K2 & L2 = K2.ⓑ{I}X) ∨ + ∃∃K2,V,W,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & ⦃K1, W⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A & + K1 ⊑[RP] K2 & + L2 = K2. ⓛW & X = ⓝW.V & I = Abbr. +/2 width=3 by lsubc_inv_pair1_aux/ qed-. fact lsubc_inv_atom2_aux: ∀RP,L1,L2. L1 ⊑[RP] L2 → L2 = ⋆ → L1 = ⋆. #RP #L1 #L2 * -L1 -L2 [ // | #I #L1 #L2 #V #_ #H destruct -| #L1 #L2 #V #W #A #_ #_ #_ #H destruct +| #L1 #L2 #V #W #A #_ #_ #_ #_ #H destruct ] -qed. +qed-. -(* Basic_1: was: csubc_gen_sort_l *) +(* Basic_1: was just: csubc_gen_sort_l *) lemma lsubc_inv_atom2: ∀RP,L1. L1 ⊑[RP] ⋆ → L1 = ⋆. -/2 width=4/ qed-. +/2 width=4 by lsubc_inv_atom2_aux/ qed-. fact lsubc_inv_pair2_aux: ∀RP,L1,L2. L1 ⊑[RP] L2 → ∀I,K2,W. L2 = K2. ⓑ{I} W → (∃∃K1. K1 ⊑[RP] K2 & L1 = K1. ⓑ{I} W) ∨ - ∃∃K1,V,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A & + ∃∃K1,V,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & ⦃K1, W⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A & K1 ⊑[RP] K2 & - L1 = K1. ⓓV & I = Abst. + L1 = K1. ⓓⓝW.V & I = Abst. #RP #L1 #L2 * -L1 -L2 [ #I #K2 #W #H destruct | #J #L1 #L2 #V #HL12 #I #K2 #W #H destruct /3 width=3/ -| #L1 #L2 #V1 #W2 #A #HV1 #HW2 #HL12 #I #K2 #W #H destruct /3 width=7/ +| #L1 #L2 #V1 #W2 #A #HV1 #H1W2 #H2W2 #HL12 #I #K2 #W #H destruct /3 width=8/ ] -qed. +qed-. -(* Basic_1: was: csubc_gen_head_l *) +(* Basic_1: was just: csubc_gen_head_l *) lemma lsubc_inv_pair2: ∀RP,I,L1,K2,W. L1 ⊑[RP] K2. ⓑ{I} W → - (∃∃K1. K1 ⊑[RP] K2 & L1 = K1. ⓑ{I} W) ∨ - ∃∃K1,V,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A & + (∃∃K1. K1 ⊑[RP] K2 & L1 = K1.ⓑ{I} W) ∨ + ∃∃K1,V,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & ⦃K1, W⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A & K1 ⊑[RP] K2 & - L1 = K1. ⓓV & I = Abst. -/2 width=3/ qed-. + L1 = K1.ⓓⓝW.V & I = Abst. +/2 width=3 by lsubc_inv_pair2_aux/ qed-. (* Basic properties *********************************************************) -(* Basic_1: was: csubc_refl *) +(* Basic_1: was just: csubc_refl *) lemma lsubc_refl: ∀RP,L. L ⊑[RP] L. #RP #L elim L -L // /2 width=1/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_ldrop.ma index f376f63f0..60b58598b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_ldrop.ma @@ -30,9 +30,9 @@ lemma lsubc_ldrop_O1_trans: ∀RP,L1,L2. L1 ⊑[RP] L2 → ∀K2,e. ⇩[0, e] L2 [ elim (IHL12 L2 0) -IHL12 // #X #H <(ldrop_inv_O2 … H) -H /3 width=3/ | elim (IHL12 … H) -L2 /3 width=3/ ] -| #L1 #L2 #V #W #A #HV #HW #_ #IHL12 #X #e #H +| #L1 #L2 #V #W #A #HV #H1W #H2W #_ #IHL12 #X #e #H elim (ldrop_inv_O1_pair1 … H) -H * #He #H destruct - [ elim (IHL12 L2 0) -IHL12 // #X #H <(ldrop_inv_O2 … H) -H /3 width=7/ + [ elim (IHL12 L2 0) -IHL12 // #X #H <(ldrop_inv_O2 … H) -H /3 width=8/ | elim (IHL12 … H) -L2 /3 width=3/ ] qed-. @@ -47,7 +47,7 @@ lemma ldrop_lsubc_trans: ∀RR,RS,RP. | #L1 #I #V1 #X #H elim (lsubc_inv_pair1 … H) -H * [ #K1 #HLK1 #H destruct /3 width=3/ - | #K1 #W1 #A #HV1 #HW1 #HLK1 #H1 #H2 destruct /3 width=3/ + | #K1 #V #W1 #A #HV1 #H1W1 #H2W1 #HLK1 #H1 #H2 #H3 destruct /3 width=4/ ] | #L1 #K1 #I #V1 #e #_ #IHLK1 #K2 #HK12 elim (IHLK1 … HK12) -K1 /3 width=5/ @@ -55,11 +55,12 @@ lemma ldrop_lsubc_trans: ∀RR,RS,RP. elim (lsubc_inv_pair1 … H) -H * [ #K2 #HK12 #H destruct elim (IHLK1 … HK12) -K1 /3 width=5/ - | #K2 #W2 #A #HV2 #HW2 #HK12 #H1 #H2 destruct + | #K2 #V #W2 #A #HV2 #H1W2 #H2W2 #HK12 #H1 #H2 #H3 destruct + elim (lift_inv_flat1 … HV21) -HV21 #W3 #V3 #HW23 #HV3 #H destruct elim (IHLK1 … HK12) #K #HL1K #HK2 lapply (aacr_acr … Hacp Hacr A) -Hacp -Hacr #HA - lapply (s8 … HA … HV2 … HLK1 HV21) -HV2 - elim (lift_total W2 d e) /4 width=9/ + lapply (s8 … HA … HV2 … HLK1 HV3) -HV2 + lapply (s8 … HA … H1W2 … HLK1 HW23) -H1W2 /4 width=10/ ] ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_lsuba.ma index aad454f62..b77900e2f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_lsuba.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_lsuba.ma @@ -18,9 +18,10 @@ include "basic_2/computation/acp_aaa.ma". (* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****) (* properties concerning lenv refinement for atomic arity assignment ********) - -lemma lsubc_lsuba: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → +(* +lamma lsubc_lsuba: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → ∀L1,L2. L1 ⁝⊑ L2 → L1 ⊑[RP] L2. #RR #RS #RP #H1RP #H2RP #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ /3 width=4/ qed. +*) \ No newline at end of file diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma index b5835bef9..47a2b015c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma @@ -36,6 +36,6 @@ lemma snv_fwd_aaa: ∀h,g,L,T. ⦃h, L⦄ ⊢ T ¡[g] → ∃A. L ⊢ T ⁝ A. ] qed-. -lemma snv_fwd_csn: ∀h,g,L,T. ⦃h, L⦄ ⊢ T ¡[g] → L ⊢ ⬊* T. +lemma snv_fwd_csn: ∀h,g,L,T. ⦃h, L⦄ ⊢ T ¡[g] → ⦃h, L⦄ ⊢ ⬊*[g] T. #h #g #L #T #H elim (snv_fwd_aaa … H) -H /2 width=2/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_aaa.ma index 363b8acd3..190092f86 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_aaa.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/computation/cprs_aaa.ma". +include "basic_2/computation/cpxs_aaa.ma". include "basic_2/equivalence/cpcs_cpcs.ma". (* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/term.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/term.ma index 9e6e55ed0..9e7d860b4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/term.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/term.ma @@ -115,21 +115,6 @@ 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: ∀a,V1,V2,W1,W2,T1,T2. - (ⓐV1. ⓛ{a}W1. T1 = ⓐV2. ⓛ{a}W2 .T2 → ⊥) → - (W1 = W2 → ⊥) ∨ - (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/ -| * #H1 #H2 destruct - elim (eq_false_inv_tpair_sn … H2) -H2 /3 width=1/ - * #H #HT12 destruct - @or_intror @conj // #H destruct /2 width=1/ -] -qed. - (* Basic_1: removed theorems 3: not_void_abst not_abbr_void not_abst_void *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/names.txt b/matita/matita/contribs/lambdadelta/basic_2/names.txt index 8b80babf9..de1f37869 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/names.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/names.txt @@ -76,6 +76,7 @@ x: extended reduction - forth letter (if present) -p: non-reflexive transitive closure (plus) -q: reflexive closure (question) -s: reflexive transitive closure (star) +e: reflexive transitive closure to normal form (evaluation) +p: non-reflexive transitive closure (plus) +q: reflexive closure (question) +s: reflexive transitive closure (star) diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation.ma b/matita/matita/contribs/lambdadelta/basic_2/notation.ma index 2a0b3c119..140086abb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation.ma @@ -190,7 +190,7 @@ notation "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ⊃ * break ⦃ term 46 L2 notation "hvbox( L1 ⊑ break term 46 L2 )" non associative with precedence 45 - for @{ 'SubEq $L1 $L2 }. + for @{ 'CrSubEq $L1 $L2 }. notation "hvbox( L ⊢ break term 46 T1 ▶* break term 46 T2 )" non associative with precedence 45 @@ -292,6 +292,10 @@ notation "hvbox( T1 ⊑ break [ term 46 R ] break term 46 T2 )" non associative with precedence 45 for @{ 'CrSubEq $T1 $R $T2 }. +notation "hvbox( L1 ⓝ ⊑ break term 46 L2 )" + non associative with precedence 45 + for @{ 'CrSubEqT $L1 $L2 }. + notation "hvbox( L ⊢ break term 46 T1 ➡ * break term 46 T2 )" non associative with precedence 45 for @{ 'PRedStar $L $T1 $T2 }. @@ -320,10 +324,6 @@ notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 • * non associative with precedence 45 for @{ 'DecomposedPRedStar $h $g $L $T1 $T2 }. -notation "hvbox( L ⊢ break term 46 T1 ➡ * break 𝐍 ⦃ term 46 T2 ⦄ )" - non associative with precedence 45 - for @{ 'PEval $L $T1 $T2 }. - notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ ⬊ * break [ term 46 g ] break term 46 T )" non associative with precedence 45 for @{ 'SN $h $g $L $T }. @@ -332,6 +332,14 @@ notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ ⬊ ⬊ * break [ term 4 non associative with precedence 45 for @{ 'SNAlt $h $g $L $T }. +notation "hvbox( L ⊢ break term 46 T1 ➡ * break 𝐍 ⦃ term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'PEval $L $T1 $T2 }. + +notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ break term 46 T1 ➡ * break [ term 46 g ] break 𝐍 ⦃ term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'PEval $h $g $L $T1 $T2 }. + (* Conversion ***************************************************************) notation "hvbox( L ⊢ break term 46 T1 ⬌ break term 46 T2 )" diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma index ecc67cb4f..2ed0e8957 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma @@ -56,7 +56,8 @@ lemma cnx_inv_abbr: ∀h,g,L,V,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃-ⓓV.T⦄ → ] qed-. -lemma cnx_inv_zeta: ∀h,g,L,V,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃+ⓓV.T⦄ → ⊥. +axiom cnx_inv_zeta: ∀h,g,L,V,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃+ⓓV.T⦄ → ⊥. +(* #h #g #L #V #T #H elim (is_lift_dec T 0 1) [ * #U #HTU lapply (H U ?) -H /2 width=3/ #H destruct @@ -66,7 +67,7 @@ lemma cnx_inv_zeta: ∀h,g,L,V,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃+ⓓV.T⦄ → ⊥. lapply (H (+ⓓV.T2) ?) -H /5 width=1/ -HT2 #H destruct /3 width=2/ ] qed-. - +*) lemma cnx_inv_appl: ∀h,g,L,V,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃ⓐV.T⦄ → ∧∧ ⦃h, L⦄ ⊢ 𝐍[g]⦃V⦄ & ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ & 𝐒⦃T⦄. #h #g #L #V1 #T1 #HVT1 @and3_intro @@ -75,7 +76,7 @@ lemma cnx_inv_appl: ∀h,g,L,V,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃ⓐV.T⦄ → | generalize in match HVT1; -HVT1 elim T1 -T1 * // #a * #W1 #U1 #_ #_ #H [ elim (lift_total V1 0 1) #V2 #HV12 lapply (H (ⓓ{a}W1.ⓐV2.U1) ?) -H /3 width=3/ -HV12 #H destruct - | lapply (H (ⓓ{a}V1.U1) ?) -H /3 width=1/ #H destruct + | lapply (H (ⓓ{a}ⓝW1.V1.U1) ?) -H /3 width=1/ #H destruct ] qed-. @@ -85,12 +86,12 @@ lemma cnx_inv_tau: ∀h,g,L,V,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃ⓝV.T⦄ → ⊥. qed-. (* Basic forward lemmas *****************************************************) - -lemma cnx_fwd_cnr: ∀h,g,L,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ → L ⊢ 𝐍⦃T⦄. +(* +lamma cnx_fwd_cnr: ∀h,g,L,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ → L ⊢ 𝐍⦃T⦄. #h #g #L #T #H #U #HTU @H /2 width=1/ (**) (* auto fails because a δ-expansion gets in the way *) qed-. - +*) (* Basic properties *********************************************************) lemma cnx_sort: ∀h,g,L,k. deg h g k 0 → ⦃h, L⦄ ⊢ 𝐍[g]⦃⋆k⦄. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma index d7c59c80d..e1d4af93c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma @@ -45,7 +45,7 @@ interpretation "context-sensitive parallel reduction (term)" (* Basic properties *********************************************************) -lemma cpr_lsubr_trans: lsubr_trans … cpr. +lemma cpr_lsubr_trans: lsub_trans … cpr lsubr. #L1 #T1 #T2 #H elim H -L1 -T1 -T2 [ // | #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12 diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma index 7a08bc435..35d4819f4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma @@ -14,6 +14,7 @@ include "basic_2/static/ssta.ma". include "basic_2/reduction/cpr.ma". +include "basic_2/reduction/lsubx.ma". (* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************) @@ -24,20 +25,22 @@ inductive cpx (h) (g): lenv → relation term ≝ ⇩[0, i] L ≡ K.ⓑ{I}V → cpx h g K V V2 → ⇧[0, i + 1] V2 ≡ W2 → cpx h g L (#i) W2 | cpx_bind : ∀a,I,L,V1,V2,T1,T2. - cpx h g L V1 V2 → cpx h g (L. ⓑ{I} V1) T1 T2 → - cpx h g L (ⓑ{a,I} V1. T1) (ⓑ{a,I} V2. T2) + cpx h g L V1 V2 → cpx h g (L. ⓑ{I}V1) T1 T2 → + cpx h g L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2) | cpx_flat : ∀I,L,V1,V2,T1,T2. cpx h g L V1 V2 → cpx h g L T1 T2 → - cpx h g L (ⓕ{I} V1. T1) (ⓕ{I} V2. T2) + cpx h g L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2) | cpx_zeta : ∀L,V,T1,T,T2. cpx h g (L.ⓓV) T1 T → - ⇧[0, 1] T2 ≡ T → cpx h g L (+ⓓV. T1) T2 -| cpx_tau : ∀L,V,T1,T2. cpx h g L T1 T2 → cpx h g L (ⓝV. T1) T2 -| cpx_beta : ∀a,L,V1,V2,W,T1,T2. - cpx h g L V1 V2 → cpx h g (L.ⓛW) T1 T2 → - cpx h g L (ⓐV1. ⓛ{a}W. T1) (ⓓ{a}V2. T2) + ⇧[0, 1] T2 ≡ T → cpx h g L (+ⓓV.T1) T2 +| cpx_tau : ∀L,V,T1,T2. cpx h g L T1 T2 → cpx h g L (ⓝV.T1) T2 +| cpx_ti : ∀L,V1,V2,T. cpx h g L V1 V2 → cpx h g L (ⓝV1.T) V2 +| cpx_beta : ∀a,L,V1,V2,W1,W2,T1,T2. + cpx h g L V1 V2 → cpx h g L W1 W2 → cpx h g (L.ⓛW1) T1 T2 → + cpx h g L (ⓐV1.ⓛ{a}W1.T1) (ⓓ{a}ⓝW2.V2.T2) | cpx_theta: ∀a,L,V1,V,V2,W1,W2,T1,T2. - cpx h g L V1 V → ⇧[0, 1] V ≡ V2 → cpx h g L W1 W2 → cpx h g (L.ⓓW1) T1 T2 → - cpx h g L (ⓐV1. ⓓ{a}W1. T1) (ⓓ{a}W2. ⓐV2. T2) + cpx h g L V1 V → ⇧[0, 1] V ≡ V2 → cpx h g L W1 W2 → + cpx h g (L.ⓓW1) T1 T2 → + cpx h g L (ⓐV1.ⓓ{a}W1.T1) (ⓓ{a}W2.ⓐV2.T2) . interpretation @@ -46,15 +49,28 @@ interpretation (* Basic properties *********************************************************) +lemma lsubx_cpx_trans: ∀h,g. lsub_trans … (cpx h g) lsubx. +#h #g #L1 #T1 #T2 #H elim H -L1 -T1 -T2 +[ // +| /2 width=2/ +| #I #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12 + elim (lsubx_fwd_ldrop2_bind … HL12 … HLK1) -HL12 -HLK1 * + [ /3 width=7/ | /4 width=7/ ] +|4,9: /4 width=1/ +|5,7,8: /3 width=1/ +|6,10: /4 width=3/ +] +qed-. + (* Note: this is "∀h,g,L. reflexive … (cpx h g L)" *) lemma cpx_refl: ∀h,g,T,L. ⦃h, L⦄ ⊢ T ➡[g] T. #h #g #T elim T -T // * /2 width=1/ qed. - -lemma cpr_cpx: ∀h,g,L,T1,T2. L ⊢ T1 ➡ T2 → ⦃h, L⦄ ⊢ T1 ➡[g] T2. +(* +lamma cpr_cpx: ∀h,g,L,T1,T2. L ⊢ T1 ➡ T2 → ⦃h, L⦄ ⊢ T1 ➡[g] T2. #h #g #L #T1 #T2 #H elim H -L -T1 -T2 // /2 width=1/ /2 width=3/ /2 width=7/ qed. - +*) fact ssta_cpx_aux: ∀h,g,L,T1,T2,l0. ⦃h, L⦄ ⊢ T1 •[g] ⦃l0, T2⦄ → ∀l. l0 = l+1 → ⦃h, L⦄ ⊢ T1 ➡[g] T2. #h #g #L #T1 #T2 #l0 #H elim H -L -T1 -T2 -l0 /2 width=2/ /2 width=7/ /3 width=2/ /3 width=7/ @@ -67,10 +83,20 @@ lemma cpx_pair_sn: ∀h,g,I,L,V1,V2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 → ∀T. ⦃h, L⦄ ⊢ ②{I}V1.T ➡[g] ②{I}V2.T. #h #g * /2 width=1/ qed. -lemma cpx_delift: ∀h,g,L,K,V,T1,d. ⇩[0, d] L ≡ (K. ⓓV) → +lemma cpx_delift: ∀h,g,I,K,V,T1,L,d. ⇩[0, d] L ≡ (K.ⓑ{I}V) → ∃∃T2,T. ⦃h, L⦄ ⊢ T1 ➡[g] T2 & ⇧[d, 1] T ≡ T2. -#h #g #L #K #V #T1 #d #HLK -elim (cpr_delift … HLK) -HLK /3 width=4/ +#h #g #I #K #V #T1 elim T1 -T1 +[ * #i #L #d #HLK /2 width=4/ + elim (lt_or_eq_or_gt i d) #Hid [1,3: /3 width=4/ ] + destruct + elim (lift_total V 0 (i+1)) #W #HVW + elim (lift_split … HVW i i) // /3 width=7/ +| * [ #a ] #I #W1 #U1 #IHW1 #IHU1 #L #d #HLK + elim (IHW1 … HLK) -IHW1 #W2 #W #HW12 #HW2 + [ elim (IHU1 (L. ⓑ{I} W1) (d+1)) -IHU1 /2 width=1/ -HLK /3 width=9/ + | elim (IHU1 … HLK) -IHU1 -HLK /3 width=8/ + ] +] qed-. lemma cpx_append: ∀h,g. l_appendable_sn … (cpx h g). @@ -96,7 +122,8 @@ fact cpx_inv_atom1_aux: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 ➡[g] T2 → ∀J. T1 | #I #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct | #L #V #T1 #T #T2 #_ #_ #J #H destruct | #L #V #T1 #T2 #_ #J #H destruct -| #a #L #V1 #V2 #W #T1 #T2 #_ #_ #J #H destruct +| #L #V1 #V2 #T #_ #J #H destruct +| #a #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #J #H destruct | #a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #J #H destruct ] qed-. @@ -138,8 +165,8 @@ qed-. fact cpx_inv_bind1_aux: ∀h,g,L,U1,U2. ⦃h, L⦄ ⊢ U1 ➡[g] U2 → ∀a,J,V1,T1. U1 = ⓑ{a,J} V1. T1 → ( - ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L.ⓑ{J}V1⦄ ⊢ T1 ➡[g] T2 & - U2 = ⓑ{a,J} V2. T2 + ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L.ⓑ{J}V1⦄ ⊢ T1 ➡[g] T2 & + U2 = ⓑ{a,J} V2. T2 ) ∨ ∃∃T. ⦃h, L.ⓓV1⦄ ⊢ T1 ➡[g] T & ⇧[0, 1] U2 ≡ T & a = true & J = Abbr. @@ -151,14 +178,15 @@ fact cpx_inv_bind1_aux: ∀h,g,L,U1,U2. ⦃h, L⦄ ⊢ U1 ➡[g] U2 → | #I #L #V1 #V2 #T1 #T2 #_ #_ #b #J #W1 #U1 #H destruct | #L #V #T1 #T #T2 #HT1 #HT2 #b #J #W1 #U1 #H destruct /3 width=3/ | #L #V #T1 #T2 #_ #b #J #W1 #U1 #H destruct -| #a #L #V1 #V2 #W #T1 #T2 #_ #_ #b #J #W1 #U1 #H destruct +| #L #V1 #V2 #T #_ #b #J #W1 #U1 #H destruct +| #a #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #b #J #W1 #U1 #H destruct | #a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #b #J #W1 #U1 #H destruct ] qed-. lemma cpx_inv_bind1: ∀h,g,a,I,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡[g] U2 → ( - ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L.ⓑ{I}V1⦄ ⊢ T1 ➡[g] T2 & - U2 = ⓑ{a,I} V2. T2 + ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L.ⓑ{I}V1⦄ ⊢ T1 ➡[g] T2 & + U2 = ⓑ{a,I} V2. T2 ) ∨ ∃∃T. ⦃h, L.ⓓV1⦄ ⊢ T1 ➡[g] T & ⇧[0, 1] U2 ≡ T & a = true & I = Abbr. @@ -168,14 +196,14 @@ lemma cpx_inv_abbr1: ∀h,g,a,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓓ{a}V1.T1 ➡[g] U2 ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L.ⓓ V1⦄ ⊢ T1 ➡[g] T2 & U2 = ⓓ{a} V2. T2 ) ∨ - ∃∃T. ⦃h, L.ⓓV1⦄ ⊢ T1 ➡[g] T & ⇧[0, 1] U2 ≡ T & a = true. + ∃∃T. ⦃h, L.ⓓV1⦄ ⊢ T1 ➡[g] T & ⇧[0, 1] U2 ≡ T & a = true. #h #g #a #L #V1 #T1 #U2 #H elim (cpx_inv_bind1 … H) -H * /3 width=3/ /3 width=5/ qed-. lemma cpx_inv_abst1: ∀h,g,a,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓛ{a}V1.T1 ➡[g] U2 → - ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L.ⓛ V1⦄ ⊢ T1 ➡[g] T2 & - U2 = ⓛ{a} V2. T2. + ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L.ⓛ V1⦄ ⊢ T1 ➡[g] T2 & + U2 = ⓛ{a} V2. T2. #h #g #a #L #V1 #T1 #U2 #H elim (cpx_inv_bind1 … H) -H * [ /3 width=5/ @@ -186,11 +214,13 @@ qed-. fact cpx_inv_flat1_aux: ∀h,g,L,U,U2. ⦃h, L⦄ ⊢ U ➡[g] U2 → ∀J,V1,U1. U = ⓕ{J} V1. U1 → ∨∨ ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L⦄ ⊢ U1 ➡[g] T2 & - U2 = ⓕ{J} V2. T2 + U2 = ⓕ{J} V2.T2 | (⦃h, L⦄ ⊢ U1 ➡[g] U2 ∧ J = Cast) - | ∃∃a,V2,W,T1,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L.ⓛW⦄ ⊢ T1 ➡[g] T2 & - U1 = ⓛ{a}W. T1 & - U2 = ⓓ{a}V2. T2 & J = Appl + | (⦃h, L⦄ ⊢ V1 ➡[g] U2 ∧ J = Cast) + | ∃∃a,V2,W1,W2,T1,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L⦄ ⊢ W1 ➡[g] W2 & + ⦃h, L.ⓛW1⦄ ⊢ T1 ➡[g] T2 & + U1 = ⓛ{a}W1.T1 & + U2 = ⓓ{a}ⓝW2.V2.T2 & J = Appl | ∃∃a,V,V2,W1,W2,T1,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V & ⇧[0,1] V ≡ V2 & ⦃h, L⦄ ⊢ W1 ➡[g] W2 & ⦃h, L.ⓓW1⦄ ⊢ T1 ➡[g] T2 & U1 = ⓓ{a}W1. T1 & @@ -203,7 +233,8 @@ fact cpx_inv_flat1_aux: ∀h,g,L,U,U2. ⦃h, L⦄ ⊢ U ➡[g] U2 → | #I #L #V1 #V2 #T1 #T2 #HV12 #HT12 #J #W1 #U1 #H destruct /3 width=5/ | #L #V #T1 #T #T2 #_ #_ #J #W1 #U1 #H destruct | #L #V #T1 #T2 #HT12 #J #W1 #U1 #H destruct /3 width=1/ -| #a #L #V1 #V2 #W #T1 #T2 #HV12 #HT12 #J #W1 #U1 #H destruct /3 width=9/ +| #L #V1 #V2 #T #HV12 #J #W1 #U1 #H destruct /3 width=1/ +| #a #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12 #J #W1 #U1 #H destruct /3 width=11/ | #a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HW12 #HT12 #J #W1 #U1 #H destruct /3 width=13/ ] qed-. @@ -212,9 +243,11 @@ lemma cpx_inv_flat1: ∀h,g,I,L,V1,U1,U2. ⦃h, L⦄ ⊢ ⓕ{I}V1.U1 ➡[g] U2 ∨∨ ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L⦄ ⊢ U1 ➡[g] T2 & U2 = ⓕ{I} V2. T2 | (⦃h, L⦄ ⊢ U1 ➡[g] U2 ∧ I = Cast) - | ∃∃a,V2,W,T1,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L.ⓛW⦄ ⊢ T1 ➡[g] T2 & - U1 = ⓛ{a}W. T1 & - U2 = ⓓ{a}V2. T2 & I = Appl + | (⦃h, L⦄ ⊢ V1 ➡[g] U2 ∧ I = Cast) + | ∃∃a,V2,W1,W2,T1,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L⦄ ⊢ W1 ➡[g] W2 & + ⦃h, L.ⓛW1⦄ ⊢ T1 ➡[g] T2 & + U1 = ⓛ{a}W1.T1 & + U2 = ⓓ{a}ⓝW2.V2.T2 & I = Appl | ∃∃a,V,V2,W1,W2,T1,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V & ⇧[0,1] V ≡ V2 & ⦃h, L⦄ ⊢ W1 ➡[g] W2 & ⦃h, L.ⓓW1⦄ ⊢ T1 ➡[g] T2 & U1 = ⓓ{a}W1. T1 & @@ -224,15 +257,16 @@ lemma cpx_inv_flat1: ∀h,g,I,L,V1,U1,U2. ⦃h, L⦄ ⊢ ⓕ{I}V1.U1 ➡[g] U2 lemma cpx_inv_appl1: ∀h,g,L,V1,U1,U2. ⦃h, L⦄ ⊢ ⓐ V1.U1 ➡[g] U2 → ∨∨ ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L⦄ ⊢ U1 ➡[g] T2 & U2 = ⓐ V2. T2 - | ∃∃a,V2,W,T1,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L.ⓛW⦄ ⊢ T1 ➡[g] T2 & - U1 = ⓛ{a}W. T1 & U2 = ⓓ{a}V2. T2 + | ∃∃a,V2,W1,W2,T1,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L⦄ ⊢ W1 ➡[g] W2 & + ⦃h, L.ⓛW1⦄ ⊢ T1 ➡[g] T2 & + U1 = ⓛ{a}W1.T1 & U2 = ⓓ{a}ⓝW2.V2.T2 | ∃∃a,V,V2,W1,W2,T1,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V & ⇧[0,1] V ≡ V2 & ⦃h, L⦄ ⊢ W1 ➡[g] W2 & ⦃h, L.ⓓW1⦄ ⊢ T1 ➡[g] T2 & U1 = ⓓ{a}W1. T1 & U2 = ⓓ{a}W2. ⓐV2. T2. #h #g #L #V1 #U1 #U2 #H elim (cpx_inv_flat1 … H) -H * [ /3 width=5/ -| #_ #H destruct -| /3 width=9/ +|2,3: #_ #H destruct +| /3 width=11/ | /3 width=13/ ] qed-. @@ -244,21 +278,22 @@ lemma cpx_inv_appl1_simple: ∀h,g,L,V1,T1,U. ⦃h, L⦄ ⊢ ⓐV1.T1 ➡[g] U #h #g #L #V1 #T1 #U #H #HT1 elim (cpx_inv_appl1 … H) -H * [ /2 width=5/ -| #a #V2 #W #U1 #U2 #_ #_ #H #_ destruct +| #a #V2 #W1 #W2 #U1 #U2 #_ #_ #_ #H #_ destruct elim (simple_inv_bind … HT1) | #a #V #V2 #W1 #W2 #U1 #U2 #_ #_ #_ #_ #H #_ destruct elim (simple_inv_bind … HT1) ] qed-. -lemma cpx_inv_cast1: ∀h,g,L,V1,U1,U2. ⦃h, L⦄ ⊢ ⓝ V1.U1 ➡[g] U2 → ( - ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L⦄ ⊢ U1 ➡[g] T2 & - U2 = ⓝ V2. T2 - ) ∨ ⦃h, L⦄ ⊢ U1 ➡[g] U2. +lemma cpx_inv_cast1: ∀h,g,L,V1,U1,U2. ⦃h, L⦄ ⊢ ⓝ V1.U1 ➡[g] U2 → + ∨∨ ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L⦄ ⊢ U1 ➡[g] T2 & + U2 = ⓝ V2. T2 + | ⦃h, L⦄ ⊢ U1 ➡[g] U2 + | ⦃h, L⦄ ⊢ V1 ➡[g] U2. #h #g #L #V1 #U1 #U2 #H elim (cpx_inv_flat1 … H) -H * [ /3 width=5/ -| /2 width=1/ -| #a #V2 #W #T1 #T2 #_ #_ #_ #_ #H destruct +|2,3: /2 width=1/ +| #a #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #H destruct | #a #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #H destruct ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cix.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cix.ma index b7a0406cb..7567f9f9c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cix.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cix.ma @@ -40,7 +40,9 @@ lemma cpx_fwd_cix: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 ➡[g] T2 → ⦃h, L⦄ elim (cix_inv_ri2 … H) /2 width=1/ | #L #V1 #T1 #T2 #_ #_ #H elim (cix_inv_ri2 … H) /2 width=1/ -| #a #L #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #H +| #L #V1 #V2 #T #_ #_ #H + elim (cix_inv_ri2 … H) /2 width=1/ +| #a #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #H elim (cix_inv_appl … H) -H #_ #_ #H elim (simple_inv_bind … H) | #a #L #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma index 325fcbf82..01ee35766 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma @@ -46,10 +46,13 @@ lemma cpx_lift: ∀h,g. l_liftable (cpx h g). elim (lift_conf_O1 … HTU2 … HT2) -T2 /4 width=5/ | #K #V #T1 #T2 #_ #IHT12 #L #d #e #HLK #U1 #H #U2 #HTU2 elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=5/ -| #a #K #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #X1 #HX1 #X2 #HX2 +| #K #V1 #V2 #T #_ #IHV12 #L #d #e #HLK #U1 #H #U2 #HVU2 + elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=5/ +| #a #K #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L #d #e #HLK #X1 #HX1 #X2 #HX2 elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct - elim (lift_inv_bind1 … HX2) -HX2 #V3 #T3 #HV23 #HT23 #HX2 destruct /4 width=5/ + elim (lift_inv_bind1 … HX2) -HX2 #X #T3 #HX #HT23 #HX2 destruct + elim (lift_inv_flat1 … HX) -HX #W3 #V3 #HW23 #HV23 #HX destruct /4 width=5/ | #a #K #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L #d #e #HLK #X1 #HX1 #X2 #HX2 elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct @@ -93,11 +96,16 @@ lemma cpx_inv_lift1: ∀h,g. l_deliftable_sn (cpx h g). | #L #V #U1 #U2 #_ #IHU12 #K #d #e #HLK #X #H elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct elim (IHU12 … HLK … HTU1) -L -U1 /3 width=3/ -| #a #L #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #K #d #e #HLK #X #HX +| #L #V1 #V2 #U1 #_ #IHV12 #K #d #e #HLK #X #H + elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct + elim (IHV12 … HLK … HWV1) -L -V1 /3 width=3/ +| #a #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #K #d #e #HLK #X #HX elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct - elim (IHV12 … HLK … HV01) -V1 - elim (IHT12 (K.ⓛW0) … HT01) -T1 /2 width=1/ /3 width=5/ + elim (IHV12 … HLK … HV01) -V1 #V3 #HV32 #HV03 + elim (IHT12 (K.ⓛW0) … HT01) -T1 /2 width=1/ #T3 #HT32 #HT03 + elim (IHW12 … HLK … HW01) -W1 #W3 #HW32 #HW03 + @ex2_intro [2: /3 width=2/ | skip |3: /2 width=1/ ] (**) (* /4 width=6/ is slow *) | #a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #K #d #e #HLK #X #HX elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx.ma index 8460d99ce..683accf54 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx.ma @@ -52,11 +52,11 @@ lemma lpx_pair: ∀h,g,I,K1,K2,V1,V2. ⦃h, K1⦄ ⊢ ➡[g] K2 → ⦃h, K1⦄ lemma lpx_append: ∀h,g,K1,K2. ⦃h, K1⦄ ⊢ ➡[g] K2 → ∀L1,L2. ⦃h, L1⦄ ⊢ ➡[g] L2 → ⦃h, L1 @@ K1⦄ ⊢ ➡[g] L2 @@ K2. /3 width=1 by lpx_sn_append, cpx_append/ qed. - -lemma lpr_lpx: ∀h,g,L1,L2. L1 ⊢ ➡ L2 → ⦃h, L1⦄ ⊢ ➡[g] L2. +(* +lamma lpr_lpx: ∀h,g,L1,L2. L1 ⊢ ➡ L2 → ⦃h, L1⦄ ⊢ ➡[g] L2. #h #g #L1 #L2 #H elim H -L1 -L2 // /3 width=1/ qed. - +*) (* Basic forward lemmas *****************************************************) lemma lpx_fwd_length: ∀h,g,L1,L2. ⦃h, L1⦄ ⊢ ➡[g] L2 → |L1| = |L2|. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma index 56eebf47c..4d9d55261 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma @@ -47,11 +47,11 @@ lemma aaa_cpx_lpx_conf: ∀h,g,L1,T1,A. L1 ⊢ T1 ⁝ A → ∀T2. ⦃h, L1⦄ | #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 elim (cpx_inv_appl1 … H) -H * [ #V2 #T2 #HV12 #HT12 #H destruct /3 width=3/ - | #b #V2 #W1 #U1 #U2 #HV12 #HU12 #H1 #H2 destruct + | #b #V2 #W1 #W2 #U1 #U2 #HV12 #HW12 #HU12 #H1 #H2 destruct lapply (IHV1 … HV12 … HL12) -IHV1 -HV12 #HV2 - lapply (IHT1 (ⓛ{b}W1.U2) … HL12) -IHT1 /2 width=1/ -L1 #H + lapply (IHT1 (ⓛ{b}W2.U2) … HL12) -IHT1 /2 width=1/ -L1 #H elim (aaa_inv_abst … H) -H #B0 #A0 #HW1 #HU2 #H destruct - lapply (lsuba_aaa_trans … HU2 (L2.ⓓV2) ?) -HU2 /2 width=2/ /2 width=3/ + lapply (lsuba_aaa_trans … HU2 (L2.ⓓⓝW2.V2) ?) -HU2 /3 width=3/ | #b #V #V2 #W1 #W2 #U1 #U2 #HV1 #HV2 #HW12 #HU12 #H1 #H2 destruct lapply (aaa_lift L2 … B … (L2.ⓓW2) … HV2) -HV2 /2 width=1/ #HV2 lapply (IHT1 (ⓓ{b}W2.U2) … HL12) -IHT1 /2 width=1/ -L1 #H @@ -61,6 +61,7 @@ lemma aaa_cpx_lpx_conf: ∀h,g,L1,T1,A. L1 ⊢ T1 ⁝ A → ∀T2. ⦃h, L1⦄ elim (cpx_inv_cast1 … H) -H [ * #V2 #T2 #HV12 #HT12 #H destruct /3 width=1/ | -IHV1 /2 width=1/ + | -IHT1 /2 width=1/ ] ] qed-. @@ -70,9 +71,10 @@ lemma aaa_cpx_conf: ∀h,g,L,T1,A. L ⊢ T1 ⁝ A → ∀T2. ⦃h, L⦄ ⊢ T1 lemma aaa_lpx_conf: ∀h,g,L1,T,A. L1 ⊢ T ⁝ A → ∀L2. ⦃h, L1⦄ ⊢ ➡[g] L2 → L2 ⊢ T ⁝ A. /2 width=7 by aaa_cpx_lpx_conf/ qed-. - -lemma aaa_cpr_conf: ∀L,T1,A. L ⊢ T1 ⁝ A → ∀T2. L ⊢ T1 ➡ T2 → L ⊢ T2 ⁝ A. +(* +lamma aaa_cpr_conf: ∀L,T1,A. L ⊢ T1 ⁝ A → ∀T2. L ⊢ T1 ➡ T2 → L ⊢ T2 ⁝ A. /3 width=5 by aaa_cpx_conf, cpr_cpx/ qed-. -lemma aaa_lpr_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. L1 ⊢ ➡ L2 → L2 ⊢ T ⁝ A. +lamma aaa_lpr_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. L1 ⊢ ➡ L2 → L2 ⊢ T ⁝ A. /3 width=5 by aaa_lpx_conf, lpr_lpx/ qed-. +*) \ No newline at end of file diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lsubx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lsubx.ma new file mode 100644 index 000000000..3034016f9 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lsubx.ma @@ -0,0 +1,101 @@ +(**************************************************************************) +(* ___ *) +(* ||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/substitution/lsubr.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR EXTENDED REDUCTION **********************) + +inductive lsubx: relation lenv ≝ +| lsubx_sort: ∀L. lsubx L (⋆) +| lsubx_bind: ∀I,L1,L2,V. lsubx L1 L2 → lsubx (L1.ⓑ{I}V) (L2.ⓑ{I}V) +| lsubx_abst: ∀L1,L2,V,W. lsubx L1 L2 → lsubx (L1.ⓓⓝW.V) (L2.ⓛW) +. + +interpretation + "local environment refinement (extended reduction)" + 'CrSubEqT L1 L2 = (lsubx L1 L2). + +(* Basic properties *********************************************************) + +lemma lsubx_refl: ∀L. L ⓝ⊑ L. +#L elim L -L // /2 width=1/ +qed. + +(* Basic inversion lemmas ***************************************************) + +fact lsubx_inv_atom1_aux: ∀L1,L2. L1 ⓝ⊑ L2 → L1 = ⋆ → L2 = ⋆. +#L1 #L2 * -L1 -L2 // +[ #I #L1 #L2 #V #_ #H destruct +| #L1 #L2 #V #W #_ #H destruct +] +qed-. + +lemma lsubx_inv_atom1: ∀L2. ⋆ ⓝ⊑ L2 → L2 = ⋆. +/2 width=3 by lsubx_inv_atom1_aux/ qed-. + +fact lsubx_inv_abst1_aux: ∀L1,L2. L1 ⓝ⊑ L2 → ∀K1,W. L1 = K1.ⓛW → + L2 = ⋆ ∨ ∃∃K2. K1 ⓝ⊑ K2 & L2 = K2.ⓛW. +#L1 #L2 * -L1 -L2 +[ #L #K1 #W #H destruct /2 width=1/ +| #I #L1 #L2 #V #HL12 #K1 #W #H destruct /3 width=3/ +| #L1 #L2 #V1 #V2 #_ #K1 #W #H destruct +] +qed-. + +lemma lsubx_inv_abst1: ∀K1,L2,W. K1.ⓛW ⓝ⊑ L2 → + L2 = ⋆ ∨ ∃∃K2. K1 ⓝ⊑ K2 & L2 = K2.ⓛW. +/2 width=3 by lsubx_inv_abst1_aux/ qed-. + +fact lsubx_inv_abbr2_aux: ∀L1,L2. L1 ⓝ⊑ L2 → ∀K2,W. L2 = K2.ⓓW → + ∃∃K1. K1 ⓝ⊑ K2 & L1 = K1.ⓓW. +#L1 #L2 * -L1 -L2 +[ #L #K2 #W #H destruct +| #I #L1 #L2 #V #HL12 #K2 #W #H destruct /2 width=3/ +| #L1 #L2 #V1 #V2 #_ #K2 #W #H destruct +] +qed-. + +lemma lsubx_inv_abbr2: ∀L1,K2,W. L1 ⓝ⊑ K2.ⓓW → + ∃∃K1. K1 ⓝ⊑ K2 & L1 = K1.ⓓW. +/2 width=3 by lsubx_inv_abbr2_aux/ qed-. + +(* Basic forward lemmas *****************************************************) + +lemma lsubx_fwd_length: ∀L1,L2. L1 ⓝ⊑ L2 → |L2| ≤ |L1|. +#L1 #L2 #H elim H -L1 -L2 // /2 width=1/ +qed-. + +lemma lsubx_fwd_lsubr: ∀L1,L2. L1 ⓝ⊑ L2 → L1 ⊑ L2. +#L1 #L2 #H elim H -L1 -L2 // /2 width=1/ +qed-. + +lemma lsubx_fwd_ldrop2_bind: ∀L1,L2. L1 ⓝ⊑ L2 → + ∀I,K2,W,i. ⇩[0, i] L2 ≡ K2.ⓑ{I}W → + (∃∃K1. K1 ⓝ⊑ K2 & ⇩[0, i] L1 ≡ K1.ⓑ{I}W) ∨ + ∃∃K1,V. K1 ⓝ⊑ K2 & ⇩[0, i] L1 ≡ K1.ⓓⓝW.V. +#L1 #L2 #H elim H -L1 -L2 +[ #L #I #K2 #W #i #H + elim (ldrop_inv_atom1 … H) -H #H destruct +| #J #L1 #L2 #V #HL12 #IHL12 #I #K2 #W #i #H + elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK2 destruct [ -IHL12 | -HL12 ] + [ /3 width=3/ + | elim (IHL12 … HLK2) -IHL12 -HLK2 * /4 width=3/ /4 width=4/ + ] +| #L1 #L2 #V1 #V2 #HL12 #IHL12 #I #K2 #W #i #H + elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK2 destruct [ -IHL12 | -HL12 ] + [ /3 width=4/ + | elim (IHL12 … HLK2) -IHL12 -HLK2 * /4 width=3/ /4 width=4/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lsubx_lsubx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lsubx_lsubx.ma new file mode 100644 index 000000000..4c9d0ef09 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lsubx_lsubx.ma @@ -0,0 +1,53 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reduction/lsubx.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR EXTENDED REDUCTION **********************) + +(* Auxiliary inversion lemmas ***********************************************) + +fact lsubx_inv_bind1_aux: ∀L1,L2. L1 ⓝ⊑ L2 → ∀I,K1,X. L1 = K1.ⓑ{I}X → + ∨∨ L2 = ⋆ + | ∃∃K2. K1 ⓝ⊑ K2 & L2 = K2.ⓑ{I}X + | ∃∃K2,V,W. K1 ⓝ⊑ K2 & L2 = K2.ⓛW & + I = Abbr & X = ⓝW.V. +#L1 #L2 * -L1 -L2 +[ #L #J #K1 #X #H destruct /2 width=1/ +| #I #L1 #L2 #V #HL12 #J #K1 #X #H destruct /3 width=3/ +| #L1 #L2 #V #W #HL12 #J #K1 #X #H destruct /3 width=6/ +] +qed-. + +lemma lsubx_inv_bind1: ∀I,K1,L2,X. K1.ⓑ{I}X ⓝ⊑ L2 → + ∨∨ L2 = ⋆ + | ∃∃K2. K1 ⓝ⊑ K2 & L2 = K2.ⓑ{I}X + | ∃∃K2,V,W. K1 ⓝ⊑ K2 & L2 = K2.ⓛW & + I = Abbr & X = ⓝW.V. +/2 width=3 by lsubx_inv_bind1_aux/ qed-. + +(* Main properties **********************************************************) + +theorem lsubx_trans: Transitive … lsubx. +#L1 #L #H elim H -L1 -L +[ #L1 #X #H + lapply (lsubx_inv_atom1 … H) -H // +| #I #L1 #L #V #_ #IHL1 #X #H + elim (lsubx_inv_bind1 … H) -H // * + #L2 [2: #V2 #W2 ] #HL2 #H1 [ #H2 #H3 ] destruct /3 width=1/ +| #L1 #L #V1 #W #_ #IHL1 #X #H + elim (lsubx_inv_abst1 … H) -H // * + #L2 #HL2 #H destruct /3 width=1/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma b/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma index 35500d952..0c899ad44 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma @@ -90,32 +90,39 @@ let rec sd_l (h:sh) (k:nat) (l:nat) on l : sd h ≝ ] ]. -(* Basic properties *********************************************************) +(* Basic inversion lemmas ***************************************************) -lemma deg_iter: ∀h,g,k,l1,l2. deg h g k l1 → deg h g ((next h)^l2 k) (l1-l2). -#h #g #k #l1 #l2 @(nat_ind_plus … l2) -l2 [ iter_SO H iter_SO #H -lapply (deg_pred … H) -H <(associative_plus l0 1 1) #H +lapply (deg_inv_pred … H) -H <(associative_plus l0 1 1) #H lapply (IHl … H) -IHl -H // +qed-. + +(* Basic properties *********************************************************) + +lemma deg_iter: ∀h,g,k,l1,l2. deg h g k l1 → deg h g ((next h)^l2 k) (l1-l2). +#h #g #k #l1 #l2 @(nat_ind_plus … l2) -l2 [ iter_SO - Closure of extended context-sensitive computation + Closure of context-sensitive extended computation for native validity. - Extended context-sensitive strong normalization + Reaxiomatized β-reductum as in extended β-reduction + + + Context-sensitive extended strong normalization for simply typed terms. @@ -40,13 +43,13 @@ Mutual recursive preservation of stratified native validity - for hyper computation on closures. + for hyper computation on closures. Confluence for context-free parallel reduction on closures. - Term binders polarized to control ζ reduction. + Term binders polarized to control ζ-reduction. Context-sensitive subject equivalence diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index 2754de2a0..879fee757 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -79,12 +79,12 @@ table { ] class "cyan" [ { "computation" * } { - [ { "decomposed extended computation" * } { - [ "dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? )" "dxprs_lift" + "dxprs_lpss" + "dxprs_aaa" + "dxprs_dxprs" * ] + [ { "context-sensitive extended evaluation" * } { + [ "cpxe ( ⦃?,?⦄ ⊢ ➡*[?] 𝐍⦃?⦄ )" * ] } ] - [ { "weakly normalizing computation" * } { - [ "cpe ( ? ⊢ ➡* 𝐍⦃?⦄ )" "cpe_cpe" * ] + [ { "context-sensitive evaluation" * } { + [ "cpre ( ? ⊢ ➡* 𝐍⦃?⦄ )" "cpre_cpre" * ] } ] [ { "strongly normalizing computation" * } { @@ -92,6 +92,10 @@ table { [ "csn ( ? ⊢ ⬊* ? )" "csn_alt ( ? ⊢ ⬊⬊* ? )" "csn_lift" + "csn_lpx" * ] } ] + [ { "decomposed extended computation" * } { + [ "dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? )" "dxprs_lift" + "dxprs_lpss" + "dxprs_aaa" + "dxprs_dxprs" * ] + } + ] [ { "context-sensitive extended computation" * } { [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?] ? )" "lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?] ? )" "lpxs_ldrop" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ] [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?] ? )" "cpxs_tstc" + "cpxs_tstc_vector" + "cpxs_lift" + "cpxs_aaa" + "cpxs_cpxs" * ] @@ -131,6 +135,10 @@ table { [ "crx ( ⦃?,?⦄ ⊢ 𝐑[?]⦃?⦄ )" "crx_append" + "crx_lift" * ] } ] + [ { "local env. ref. for extended reduction" * } { + [ "lsubx ( ? ⓝ⊑ ? )" "lsubx_lsubx" * ] + } + ] [ { "context-sensitive normal forms" * } { [ "cnr ( ? ⊢ 𝐍⦃?⦄ )" "cnr_lift" + "cnr_crr" + "cnr_cir" * ] } @@ -189,7 +197,7 @@ table { ] class "yellow" [ { "substitution" * } { - [ { "parallel substitution" * } { + [ { "parallel substitution" * } { [ "lpss ( ? ⊢ ▶* ? )" "lpss_ldrop" + "lpss_cpss" + "lpss_lpss" * ] [ "cpss ( ? ⊢ ? ▶* ? )" "cpss_lift" * ] } diff --git a/matita/matita/contribs/lambdadelta/ground_2/star.ma b/matita/matita/contribs/lambdadelta/ground_2/star.ma index 671881857..ef0db595a 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/star.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/star.ma @@ -38,6 +38,9 @@ definition bi_confluent: ∀A,B. ∀R: bi_relation A B. Prop ≝ λA,B,R. definition LTC: ∀A:Type[0]. ∀B. (A→relation B) → (A→relation B) ≝ λA,B,R,a. TC … (R a). +definition lsub_trans: ∀A,B. relation2 (A→relation B) (relation A) ≝ λA,B,R1,R2. + ∀L2,T1,T2. R1 L2 T1 T2 → ∀L1. R2 L1 L2 → R1 L1 T1 T2. + definition s_r_trans: ∀A,B. relation2 (A→relation B) (relation A) ≝ λA,B,R1,R2. ∀L2,T1,T2. R1 L2 T1 T2 → ∀L1. R2 L1 L2 → LTC … R1 L1 T1 T2. @@ -191,6 +194,12 @@ lemma bi_TC_decomp_l: ∀A,B. ∀R:bi_relation A B. ] qed-. +lemma TC_lsub_trans: ∀A,B,R,S. lsub_trans A B R S → lsub_trans A B (LTC … R) S. +#A #B #R #S #HRS #L2 #T1 #T2 #H elim H -T2 [ /3 width=3/ ] +#T #T2 #_ #HT2 #IHT1 #L1 #HL12 +lapply (HRS … HT2 … HL12) -HRS -HT2 /3 width=3/ +qed-. + lemma s_r_trans_TC1: ∀A,B,R,S. s_r_trans A B R S → s_rs_trans A B R S. #A #B #R #S #HRS #L2 #T1 #T2 #H elim H -T2 [ /3 width=3/ ] #T #T2 #_ #HT2 #IHT1 #L1 #HL12 diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml b/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml index 43ef2780b..f931752fb 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml @@ -22,14 +22,18 @@ 5 3 5 4 5 5 + 5 6 + 6 3 6 4 6 5 6 6 6 7 + 7 4 7 7 8 5 3 4 + 5 3 4 diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa.ma index f1dcd2830..4fca831e8 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa.ma @@ -152,6 +152,22 @@ inductive ex5_5 (A0,A1,A2,A3,A4:Type[0]) (P0,P1,P2,P3,P4:A0→A1→A2→A3→A4 interpretation "multiple existental quantifier (5, 5)" 'Ex P0 P1 P2 P3 P4 = (ex5_5 ? ? ? ? ? P0 P1 P2 P3 P4). +(* multiple existental quantifier (5, 6) *) + +inductive ex5_6 (A0,A1,A2,A3,A4,A5:Type[0]) (P0,P1,P2,P3,P4:A0→A1→A2→A3→A4→A5→Prop) : Prop ≝ + | ex5_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 → ex5_6 ? ? ? ? ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (5, 6)" 'Ex P0 P1 P2 P3 P4 = (ex5_6 ? ? ? ? ? ? P0 P1 P2 P3 P4). + +(* multiple existental quantifier (6, 3) *) + +inductive ex6_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→Prop) : Prop ≝ + | ex6_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → P3 x0 x1 x2 → P4 x0 x1 x2 → P5 x0 x1 x2 → ex6_3 ? ? ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (6, 3)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_3 ? ? ? P0 P1 P2 P3 P4 P5). + (* 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 ≝ @@ -184,6 +200,14 @@ inductive ex6_7 (A0,A1,A2,A3,A4,A5,A6:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2 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, 4) *) + +inductive ex7_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→Prop) : Prop ≝ + | ex7_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → P3 x0 x1 x2 x3 → P4 x0 x1 x2 x3 → P5 x0 x1 x2 x3 → P6 x0 x1 x2 x3 → ex7_4 ? ? ? ? ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (7, 4)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_4 ? ? ? ? P0 P1 P2 P3 P4 P5 P6). + (* multiple existental quantifier (7, 7) *) 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 ≝ @@ -221,6 +245,18 @@ inductive or4 (P0,P1,P2,P3:Prop) : Prop ≝ interpretation "multiple disjunction connective (4)" 'Or P0 P1 P2 P3 = (or4 P0 P1 P2 P3). +(* multiple disjunction connective (5) *) + +inductive or5 (P0,P1,P2,P3,P4:Prop) : Prop ≝ + | or5_intro0: P0 → or5 ? ? ? ? ? + | or5_intro1: P1 → or5 ? ? ? ? ? + | or5_intro2: P2 → or5 ? ? ? ? ? + | or5_intro3: P3 → or5 ? ? ? ? ? + | or5_intro4: P4 → or5 ? ? ? ? ? +. + +interpretation "multiple disjunction connective (5)" 'Or P0 P1 P2 P3 P4 = (or5 P0 P1 P2 P3 P4). + (* multiple conjunction connective (3) *) inductive and3 (P0,P1,P2:Prop) : Prop ≝ diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa_notation.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa_notation.ma index 02bb27542..ee01b1071 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa_notation.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa_notation.ma @@ -184,6 +184,26 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 br 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 (5, 6) *) + +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)" + 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) }. + +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)" + 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) }. + +(* multiple existental quantifier (6, 3) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 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}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P5) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 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.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P5) }. + (* 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)" @@ -224,6 +244,16 @@ 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.λ${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, 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 break & term 19 P6)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P6) }. + +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 break & term 19 P6)" + 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) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P6) }. + (* multiple existental quantifier (7, 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 break & term 19 P6)" @@ -256,6 +286,12 @@ notation "hvbox(∨∨ term 29 P0 break | term 29 P1 break | term 29 P2 break | non associative with precedence 30 for @{ 'Or $P0 $P1 $P2 $P3 }. +(* multiple disjunction connective (5) *) + +notation "hvbox(∨∨ term 29 P0 break | term 29 P1 break | term 29 P2 break | term 29 P3 break | term 29 P4)" + non associative with precedence 30 + for @{ 'Or $P0 $P1 $P2 $P3 $P4 }. + (* multiple conjunction connective (3) *) notation "hvbox(∧∧ term 34 P0 break & term 34 P1 break & term 34 P2)" -- 2.39.2