From 62211b3b2d76ba387663c9e553fbe4d2dbd92c82 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 20 Jan 2014 15:59:12 +0000 Subject: [PATCH] commit completed: now we support two versions of slicing for local environments --- .../lambdadelta/basic_2/computation/acp.ma | 10 +- .../basic_2/computation/acp_aaa.ma | 7 +- .../lambdadelta/basic_2/computation/acp_cr.ma | 45 ++++---- .../basic_2/computation/cpds_lift.ma | 9 +- .../basic_2/computation/cprs_lift.ma | 21 ++-- .../basic_2/computation/cpxs_cpxs.ma | 2 +- .../basic_2/computation/cpxs_cpys.ma | 27 ++++- .../basic_2/computation/cpxs_lift.ma | 14 +-- .../basic_2/computation/cpxs_tstc.ma | 44 ++++---- .../basic_2/computation/cpxs_tstc_vector.ma | 57 +++++----- .../basic_2/computation/csx_lift.ma | 22 ++-- .../basic_2/computation/csx_lpx.ma | 57 +++++----- .../basic_2/computation/csx_tstc_vector.ma | 54 +++++----- .../basic_2/computation/lprs_cprs.ma | 29 ++--- .../basic_2/computation/lpxs_cpxs.ma | 2 +- .../basic_2/computation/lsubc_ldrop.ma | 44 ++++---- .../basic_2/computation/lsubc_ldrops.ma | 8 +- .../basic_2/dynamic/lsubsv_ldrop.ma | 44 ++++---- .../basic_2/dynamic/lsubsv_lsstas.ma | 8 +- .../lambdadelta/basic_2/dynamic/snv.ma | 14 +-- .../lambdadelta/basic_2/dynamic/snv_da_lpr.ma | 4 +- .../lambdadelta/basic_2/dynamic/snv_lift.ma | 62 ++++++----- .../lambdadelta/basic_2/dynamic/snv_lpr.ma | 8 +- .../basic_2/dynamic/snv_lsstas_lpr.ma | 6 +- .../basic_2/equivalence/cpcs_cpcs.ma | 101 ++++++++---------- .../basic_2/substitution/ldrops_ldrop.ma | 11 +- .../lambdadelta/basic_2/web/basic_2.ldw.xml | 5 + 27 files changed, 363 insertions(+), 352 deletions(-) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma index aa62952b4..5de150697 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma @@ -21,11 +21,11 @@ definition CP1 ≝ λRR:relation4 genv lenv term term. λRS:relation term. ∀G,L. ∃k. NF … (RR G L) RS (⋆k). definition CP2 ≝ λRR:relation4 genv lenv term term. λRS:relation term. - ∀G,L0,L,T,T0,d,e. NF … (RR G L) RS T → - ⇩[d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → NF … (RR G L0) RS T0. + ∀G,L0,L,T,T0,s,d,e. NF … (RR G L) RS T → + ⇩[s, d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → NF … (RR G L0) RS T0. definition CP2s ≝ λRR:relation4 genv lenv term term. λRS:relation term. - ∀G,L0,L,des. ⇩*[des] L0 ≡ L → + ∀G,L0,L,s,des. ⇩*[s, des] L0 ≡ L → ∀T,T0. ⇧*[des] T ≡ T0 → NF … (RR G L) RS T → NF … (RR G L0) RS T0. @@ -47,10 +47,10 @@ record acp (RR:relation4 genv lenv term term) (RS:relation term) (RP:relation3 g (* Basic_1: was: nf2_lift1 *) lemma acp_lifts: ∀RR,RS. CP2 RR RS → CP2s RR RS. -#RR #RS #HRR #G #L1 #L2 #des #H elim H -L1 -L2 -des +#RR #RS #HRR #G #L1 #L2 #s #des #H elim H -L1 -L2 -des [ #L #T1 #T2 #H #HT1 <(lifts_inv_nil … H) -H // | #L1 #L #L2 #des #d #e #_ #HL2 #IHL #T2 #T1 #H #HLT2 - elim (lifts_inv_cons … H) -H /3 width=9/ + elim (lifts_inv_cons … H) -H /3 width=10 by/ ] qed. 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 23cc43031..3c393b9a3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma @@ -25,7 +25,7 @@ include "basic_2/computation/lsubc_ldrops.ma". (* Basic_1: was: sc3_arity_csubc *) theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) → - ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L0,des. ⇩*[des] L0 ≡ L1 → + ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L0,des. ⇩*[Ⓕ, des] L0 ≡ L1 → ∀T0. ⇧*[des] T ≡ T0 → ∀L2. G ⊢ L2 ⊑[RP] L0 → ⦃G, L2, T0⦄ ϵ[RP] 〚A〛. #RR #RS #RP #H1RP #H2RP #G #L1 #T #A #H elim H -G -L1 -T -A @@ -67,8 +67,9 @@ theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP. @(aacr_abst … H1RP H2RP) [ /2 width=5 by/ ] #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 by ldrops_trans, lifts_trans/ #HLW2B - @(IHA (L2. ⓛW3) … (des + 1 @@ des3 + 1)) -IHA /2 width=3/ /3 width=5 by lsubc_abbr, ldrops_trans, ldrops_skip/ + lapply (aaa_lifts … L2 W3 … (des @@ des3) … HLWB) -HLWB /2 width=4 by ldrops_trans, lifts_trans/ #HLW2B + @(IHA (L2. ⓛW3) … (des + 1 @@ des3 + 1)) -IHA + /3 width=5 by lsubc_abbr, ldrops_trans, ldrops_skip, lifts_trans/ | #G #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 by ldrops_nil, lifts_nil/ 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 1b0d56c7c..fa9508a28 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma @@ -39,8 +39,8 @@ definition S4 ≝ λRP,C:relation3 genv lenv term. ∀G,L,Vs. all … (RP G L) Vs → ∀k. C G L (ⒶVs.⋆k). definition S5 ≝ λC:relation3 genv lenv term. ∀I,G,L,K,Vs,V1,V2,i. - C G L (ⒶVs.V2) → ⇧[0, i + 1] V1 ≡ V2 → - ⇩[0, i] L ≡ K.ⓑ{I}V1 → C G L (ⒶVs.#i). + C G L (ⒶVs.V2) → ⇧[0, i+1] V1 ≡ V2 → + ⇩[i] L ≡ K.ⓑ{I}V1 → C G L (ⒶVs.#i). definition S6 ≝ λRP,C:relation3 genv lenv term. ∀G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → @@ -50,10 +50,10 @@ definition S7 ≝ λC:relation3 genv lenv term. ∀G,L,Vs,T,W. C G L (ⒶVs.T) → C G L (ⒶVs.W) → C G L (ⒶVs.ⓝW.T). definition S8 ≝ λC:relation3 genv lenv term. ∀G,L2,L1,T1,d,e. - C G L1 T1 → ∀T2. ⇩[d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → C G L2 T2. + C G L1 T1 → ∀T2. ⇩[Ⓕ, d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → C G L2 T2. definition S8s ≝ λC:relation3 genv lenv term. - ∀G,L1,L2,des. ⇩*[des] L2 ≡ L1 → + ∀G,L1,L2,des. ⇩*[Ⓕ, des] L2 ≡ L1 → ∀T1,T2. ⇧*[des] T1 ≡ T2 → C G L1 T1 → C G L2 T2. (* properties of the abstract candidate of reducibility *) @@ -73,7 +73,7 @@ let rec aacr (RP:relation3 genv lenv term) (A:aarity) (G:genv) (L:lenv) on A: pr λT. match A with [ AAtom ⇒ RP G L T | APair B A ⇒ ∀L0,V0,T0,des. - aacr RP B G L0 V0 → ⇩*[des] L0 ≡ L → ⇧*[des] T ≡ T0 → + aacr RP B G L0 V0 → ⇩*[Ⓕ, des] L0 ≡ L → ⇧*[des] T ≡ T0 → aacr RP A G L0 (ⓐV0.T0) ]. @@ -86,27 +86,26 @@ interpretation (* Basic_1: was: sc3_lift1 *) lemma acr_lifts: ∀C. S8 C → S8s C. #C #HC #G #L1 #L2 #des #H elim H -L1 -L2 -des -[ #L #T1 #T2 #H #HT1 - <(lifts_inv_nil … H) -H // +[ #L #T1 #T2 #H #HT1 <(lifts_inv_nil … H) -H // | #L1 #L #L2 #des #d #e #_ #HL2 #IHL #T2 #T1 #H #HLT2 - elim (lifts_inv_cons … H) -H /3 width=9 by/ + elim (lifts_inv_cons … H) -H /3 width=10 by/ ] qed. lemma rp_lifts: ∀RR,RS,RP. acr RR RS RP (λG,L,T. RP G L T) → - ∀des,G,L0,L,V,V0. ⇩*[des] L0 ≡ L → ⇧*[des] V ≡ V0 → + ∀des,G,L0,L,V,V0. ⇩*[Ⓕ, des] L0 ≡ L → ⇧*[des] V ≡ V0 → RP G L V → RP G L0 V0. #RR #RS #RP #HRP #des #G #L0 #L #V #V0 #HL0 #HV0 #HV -@acr_lifts /width=6 by/ +@acr_lifts /width=7 by/ @(s8 … HRP) qed. (* Basic_1: was only: sns3_lifts1 *) lemma rp_liftsv_all: ∀RR,RS,RP. acr RR RS RP (λG,L,T. RP G L T) → - ∀des,G,L0,L,Vs,V0s. ⇧*[des] Vs ≡ V0s → ⇩*[des] L0 ≡ L → + ∀des,G,L0,L,Vs,V0s. ⇩*[Ⓕ, des] L0 ≡ L → ⇧*[des] Vs ≡ V0s → all … (RP G L) Vs → all … (RP G L0) V0s. -#RR #RS #RP #HRP #des #G #L0 #L #Vs #V0s #H elim H -Vs -V0s normalize // -#T1s #T2s #T1 #T2 #HT12 #_ #IHT2s #HL0 * /3 width=6 by rp_lifts, conj/ +#RR #RS #RP #HRP #des #G #L0 #L #Vs #V0s #HL0 #H elim H -Vs -V0s normalize // +#T1s #T2s #T1 #T2 #HT12 #_ #IHT2s * /3 width=7 by rp_lifts, conj/ qed. (* Basic_1: was: @@ -127,17 +126,17 @@ lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) elim (lifts_inv_applv1 … H) -H #V0s #T0 #HV0s #HT0 #H destruct lapply (s1 … IHB … HB) #HV0 @(s2 … IHA … (V0 @ V0s)) - /3 width=13 by rp_liftsv_all, acp_lifts, cp2, lifts_simple_dx, conj/ + /3 width=14 by rp_liftsv_all, acp_lifts, cp2, lifts_simple_dx, conj/ | #a #G #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)) /5 width=5 by lifts_applv, lifts_flat, lifts_bind/ -| #G #L #Vs #HVs #k #L0 #V0 #X #hdes #HB #HL0 #H + @(s3 … IHA … (V0 @ V0s)) /5 width=6 by lifts_applv, lifts_flat, lifts_bind/ +| #G #L #Vs #HVs #k #L0 #V0 #X #des #HB #HL0 #H elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct >(lifts_inv_sort1 … HY) -Y lapply (s1 … IHB … HB) #HV0 - @(s4 … IHA … (V0 @ V0s)) /3 width=6 by rp_liftsv_all, conj/ + @(s4 … IHA … (V0 @ V0s)) /3 width=7 by rp_liftsv_all, conj/ | #I #G #L #K #Vs #V1 #V2 #i #HA #HV12 #HLK #L0 #V0 #X #des #HB #HL0 #H elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct elim (lifts_inv_lref1 … HY) -HY #i0 #Hi0 #H destruct @@ -147,15 +146,15 @@ lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) elim (lift_total W1 0 (i0 + 1)) #W2 #HW12 elim (lifts_lift_trans … Hdes0 … HVW1 … HW12) // -Hdes0 -Hi0 #V3 #HV13 #HVW2 >(lift_mono … HV13 … HV12) in HVW2; -V3 #HVW2 - @(s5 … IHA … (V0 @ V0s) … HW12 HL02) /3 width=4 by lifts_applv/ + @(s5 … IHA … (V0 @ V0s) … HW12 HL02) /3 width=5 by lifts_applv/ | #G #L #V1s #V2s #HV12s #a #V #T #HA #HV #L0 #V10 #X #des #HB #HL0 #H elim (lifts_inv_applv1 … H) -H #V10s #Y #HV10s #HY #H destruct elim (lifts_inv_bind1 … HY) -HY #V0 #T0 #HV0 #HT0 #H destruct elim (lift_total V10 0 1) #V20 #HV120 elim (liftv_total 0 1 V10s) #V20s #HV120s - @(s6 … IHA … (V10 @ V10s) (V20 @ V20s)) /3 width=6 by rp_lifts, liftv_cons/ - @(HA … (des + 1)) /2 width=1 by ldrops_skip/ - [ @(s8 … IHB … HB … HV120) /2 width=1 by ldrop_ldrop/ + @(s6 … IHA … (V10 @ V10s) (V20 @ V20s)) /3 width=7 by rp_lifts, liftv_cons/ + @(HA … (des + 1)) /2 width=2 by ldrops_skip/ + [ @(s8 … IHB … HB … HV120) /2 width=2 by ldrop_drop/ | @lifts_applv // elim (liftsv_liftv_trans_le … HV10s … HV120s) -V10s #V10s #HV10s #HV120s >(liftv_mono … HV12s … HV10s) -V1s // @@ -163,14 +162,14 @@ lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) | #G #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)) /3 width=4 by lifts_applv/ + @(s7 … IHA … (V0 @ V0s)) /3 width=5 by lifts_applv/ | /3 width=7 by ldrops_cons, lifts_cons/ ] qed. lemma aacr_abst: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) → ∀a,G,L,W,T,A,B. ⦃G, L, W⦄ ϵ[RP] 〚B〛 → ( - ∀L0,V0,W0,T0,des. ⇩*[des] L0 ≡ L → ⇧*[des ] W ≡ W0 → ⇧*[des + 1] T ≡ T0 → + ∀L0,V0,W0,T0,des. ⇩*[Ⓕ, des] L0 ≡ L → ⇧*[des ] W ≡ W0 → ⇧*[des + 1] T ≡ T0 → ⦃G, L0, V0⦄ ϵ[RP] 〚B〛 → ⦃G, L0, W0⦄ ϵ[RP] 〚B〛 → ⦃G, L0.ⓓⓝW0.V0, T0⦄ ϵ[RP] 〚A〛 ) → ⦃G, L, ⓛ{a}W.T⦄ ϵ[RP] 〚②B.A〛. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_lift.ma index 4f4b77df4..b35ebad49 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_lift.ma @@ -21,14 +21,15 @@ include "basic_2/computation/cpds.ma". (* Relocation properties ****************************************************) lemma cpds_lift: ∀h,g,G. l_liftable (cpds h g G). -#h #g #G #K #T1 #T2 * #T #l1 #l2 #Hl12 #Hl1 #HT1 #HT2 #L #d #e +#h #g #G #K #T1 #T2 * #T #l1 #l2 #Hl12 #Hl1 #HT1 #HT2 #L #s #d #e elim (lift_total T d e) -/3 width=15 by cprs_lift, da_lift, lsstas_lift, ex4_3_intro/ +/3 width=16 by cprs_lift, da_lift, lsstas_lift, ex4_3_intro/ qed. lemma cpds_inv_lift1: ∀h,g,G. l_deliftable_sn (cpds h g G). -#h #g #G #L #U1 #U2 * #U #l1 #l2 #Hl12 #Hl1 #HU1 #HU2 #K #d #e #HLK #T1 #HTU1 +#h #g #G #L #U1 #U2 * #U #l1 #l2 #Hl12 #Hl1 #HU1 #HU2 #K #s #d #e #HLK #T1 #HTU1 lapply (da_inv_lift … Hl1 … HLK … HTU1) -Hl1 #Hl1 elim (lsstas_inv_lift1 … HU1 … HLK … HTU1) -U1 #T #HTU #HT1 -elim (cprs_inv_lift1 … HU2 … HLK … HTU) -U -L /3 width=9/ +elim (cprs_inv_lift1 … HU2 … HLK … HTU) -U -L +/3 width=9 by ex4_3_intro, ex2_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma index 6298274bc..ca1556a8e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma @@ -21,12 +21,12 @@ include "basic_2/computation/cprs.ma". (* Note: apparently this was missing in basic_1 *) lemma cprs_delta: ∀G,L,K,V,V2,i. - ⇩[0, i] L ≡ K.ⓓV → ⦃G, K⦄ ⊢ V ➡* V2 → + ⇩[i] L ≡ K.ⓓV → ⦃G, K⦄ ⊢ V ➡* V2 → ∀W2. ⇧[0, i + 1] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ➡* W2. -#G #L #K #V #V2 #i #HLK #H elim H -V2 [ /3 width=6/ ] +#G #L #K #V #V2 #i #HLK #H elim H -V2 [ /3 width=6 by cpr_cprs, cpr_delta/ ] #V1 #V2 #_ #HV12 #IHV1 #W2 #HVW2 lapply (ldrop_fwd_drop2 … HLK) -HLK #HLK -elim (lift_total V1 0 (i+1)) /4 width=11 by cpr_lift, cprs_strap1/ +elim (lift_total V1 0 (i+1)) /4 width=12 by cpr_lift, cprs_strap1/ qed. (* Advanced inversion lemmas ************************************************) @@ -34,16 +34,17 @@ qed. (* Basic_1: was: pr3_gen_lref *) lemma cprs_inv_lref1: ∀G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡* T2 → T2 = #i ∨ - ∃∃K,V1,T1. ⇩[0, i] L ≡ K. ⓓV1 & ⦃G, K⦄ ⊢ V1 ➡* T1 & + ∃∃K,V1,T1. ⇩[i] L ≡ K.ⓓV1 & ⦃G, K⦄ ⊢ V1 ➡* T1 & ⇧[0, i + 1] T1 ≡ T2. -#G #L #T2 #i #H @(cprs_ind … H) -T2 /2 width=1/ +#G #L #T2 #i #H @(cprs_ind … H) -T2 /2 width=1 by or_introl/ #T #T2 #_ #HT2 * [ #H destruct - elim (cpr_inv_lref1 … HT2) -HT2 /2 width=1/ - * /4 width=6/ + elim (cpr_inv_lref1 … HT2) -HT2 /2 width=1 by or_introl/ + * /4 width=6 by cpr_cprs, ex3_3_intro, or_intror/ | * #K #V1 #T1 #HLK #HVT1 #HT1 lapply (ldrop_fwd_drop2 … HLK) #H0LK - elim (cpr_inv_lift1 … HT2 … H0LK … HT1) -H0LK -T /4 width=6/ + elim (cpr_inv_lift1 … HT2 … H0LK … HT1) -H0LK -T + /4 width=6 by cprs_strap1, ex3_3_intro, or_intror/ ] qed-. @@ -51,9 +52,9 @@ qed-. (* Basic_1: was: pr3_lift *) lemma cprs_lift: ∀G. l_liftable (cprs G). -/3 width=9/ qed. +/3 width=10 by l_liftable_LTC, cpr_lift/ qed. (* Basic_1: was: pr3_gen_lift *) lemma cprs_inv_lift1: ∀G. l_deliftable_sn (cprs G). -/3 width=5 by l_deliftable_sn_LTC, cpr_inv_lift1/ +/3 width=6 by l_deliftable_sn_LTC, cpr_inv_lift1/ qed-. 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 e4c5cea84..21dd2a4cd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma @@ -159,7 +159,7 @@ lemma fqu_cpxs_trans_neq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, ] | #G #L #K #T1 #U1 #e #HLK #HTU1 #T2 #HT12 #H elim (lift_total T2 0 (e+1)) #U2 #HTU2 @(ex3_intro … U2) - [1,3: /2 width=9 by cpxs_lift, fqu_drop/ + [1,3: /2 width=10 by cpxs_lift, fqu_drop/ | #H0 destruct /3 width=5 by lift_inj/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpys.ma index 0bbe9835c..7ab36e5be 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpys.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpys.ma @@ -13,23 +13,40 @@ (**************************************************************************) include "basic_2/substitution/cpys_cpys.ma". +include "basic_2/reduction/cpx_cpys.ma". include "basic_2/computation/cpxs_cpxs.ma". (* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************) (* Main properties **********************************************************) -lemma cpx_fwd_cpys_tpxs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → +axiom cpys_split_down: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 → + ∀i. d ≤ i → i ≤ d + e → + ∃∃T. ⦃G, L⦄ ⊢ T1 ▶*×[i, d+e-i] T & ⦃G, L⦄ ⊢ T ▶*×[d, i-d] T2. + +lemma cpys_tpxs_trans: ∀h,g,G,L,T1,T,d,e. ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T → + ∀T2. ⦃G, ⋆⦄ ⊢ T ➡*[h, g] T2 → ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2. +#h #g #G #L #T1 #T #d #e #HT1 #T2 #H @(cpxs_ind … H) -T2 +/3 width=5 by cpxs_strap1, cpys_cpx, lsubr_cpx_trans, cpx_cpxs/ +qed-. + +axiom cpx_fwd_cpys_tpxs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → ∃∃T. ⦃G, L⦄ ⊢ T1 ▶*×[0, ∞] T & ⦃G, ⋆⦄ ⊢ T ➡*[h, g] T2. +(* #h #g #G #L #T1 #T2 #H elim H -G -L -T1 -T2 [ /2 width=3 by ex2_intro/ | /4 width=3 by cpx_cpxs, cpx_sort, ex2_intro/ | #I #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 * #V #HV1 #HV2 elim (lift_total V 0 (i+1)) #W #HVW - @(ex2_intro … W) /2 width=7 by cpys_subst_Y2/ + lapply (cpxs_lift … HV2 (⋆) (Ⓣ) … HVW … HVW2) + [ @ldrop_atom #H destruct | /3 width=7 by cpys_subst_Y2, ex2_intro/ ] | #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ * #V #HV1 #HV2 * #T #HT1 #HT2 - elim (cpys_split_up … HT1 1) -HT1 // #T0 #HT10 #HT0 + elim (cpys_split_down … HT1 1) -HT1 // #T0 #HT10 #HT0 +(* @(ex2_intro … (ⓑ{a,I}V.T0)) - [ @(cpys_bind … HV1) -HV1 + [ @cpys_bind // | @(cpxs_bind … HV2) -HV2 - ] + + /2 width=5 by cpys_tpxs_trans/ + ] +*)*) \ No newline at end of file diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma index 2d6797667..de9a897b9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma @@ -33,12 +33,12 @@ lapply (lsstas_da_conf … HT1 … Hl2) -HT1 qed. lemma cpxs_delta: ∀h,g,I,G,L,K,V,V2,i. - ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ➡*[h, g] V2 → - ∀W2. ⇧[0, i + 1] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ➡*[h, g] W2. + ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ➡*[h, g] V2 → + ∀W2. ⇧[0, i+1] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ➡*[h, g] W2. #h #g #I #G #L #K #V #V2 #i #HLK #H elim H -V2 [ /3 width=9 by cpx_cpxs, cpx_delta/ | #V1 lapply (ldrop_fwd_drop2 … HLK) -HLK - elim (lift_total V1 0 (i+1)) /4 width=11 by cpx_lift, cpxs_strap1/ + elim (lift_total V1 0 (i+1)) /4 width=12 by cpx_lift, cpxs_strap1/ ] qed. @@ -46,8 +46,8 @@ qed. lemma cpxs_inv_lref1: ∀h,g,G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡*[h, g] T2 → T2 = #i ∨ - ∃∃I,K,V1,T1. ⇩[0, i] L ≡ K.ⓑ{I}V1 & ⦃G, K⦄ ⊢ V1 ➡*[h, g] T1 & - ⇧[0, i + 1] T1 ≡ T2. + ∃∃I,K,V1,T1. ⇩[i] L ≡ K.ⓑ{I}V1 & ⦃G, K⦄ ⊢ V1 ➡*[h, g] T1 & + ⇧[0, i+1] T1 ≡ T2. #h #g #G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/ #T #T2 #_ #HT2 * [ #H destruct @@ -63,10 +63,10 @@ qed-. (* Relocation properties ****************************************************) lemma cpxs_lift: ∀h,g,G. l_liftable (cpxs h g G). -/3 width=9 by cpx_lift, cpxs_strap1, l_liftable_LTC/ qed. +/3 width=10 by cpx_lift, cpxs_strap1, l_liftable_LTC/ qed. lemma cpxs_inv_lift1: ∀h,g,G. l_deliftable_sn (cpxs h g G). -/3 width=5 by l_deliftable_sn_LTC, cpx_inv_lift1/ +/3 width=6 by l_deliftable_sn_LTC, cpx_inv_lift1/ qed-. (* Properties on supclosure *************************************************) 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 30745dd38..ec36d47f1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma @@ -28,13 +28,13 @@ lemma cpxs_fwd_sort: ∀h,g,G,L,U,k. ⦃G, L⦄ ⊢ ⋆k ➡*[h, g] U → ⋆k ≃ U ∨ ⦃G, L⦄ ⊢ ⋆(next h k) ➡*[h, g] U. #h #g #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/ +[ #k #_ #H -l destruct /2 width=1 by or_introl/ | #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/ + [ #H lapply (tstc_inv_atom1 … H) -H #H >H -H /2 width=1 by or_intror/ + | generalize in match Hnl; -Hnl @(nat_ind_plus … n) -n + /4 width=3 by cpxs_strap2, cpx_sort, or_intror/ | >iter_SO >iter_n_Sm // ] ] @@ -45,26 +45,26 @@ lemma cpxs_fwd_beta: ∀h,g,a,G,L,V,W,T,U. ⦃G, L⦄ ⊢ ⓐV.ⓛ{a}W.T ➡*[h, ⓐV.ⓛ{a}W.T ≃ U ∨ ⦃G, L⦄ ⊢ ⓓ{a}ⓝW.V.T ➡*[h, g] U. #h #g #a #G #L #V #W #T #U #H elim (cpxs_inv_appl1 … H) -H * -[ #V0 #T0 #_ #_ #H destruct /2 width=1/ +[ #V0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair, or_introl/ | #b #W0 #T0 #HT0 #HU elim (cpxs_inv_abst1 … HT0) -HT0 #W1 #T1 #HW1 #HT1 #H destruct - lapply (lsubr_cpxs_trans … HT1 (L.ⓓⓝW.V) ?) -HT1 /2 width=1/ #HT1 - @or_intror @(cpxs_trans … HU) -U /3 width=1/ (**) (* explicit constructor *) + lapply (lsubr_cpxs_trans … HT1 (L.ⓓⓝW.V) ?) -HT1 + /5 width=3 by cpxs_trans, cpxs_bind, cpxs_pair_sn, lsubr_abst, or_intror/ | #b #V1 #V2 #V0 #T1 #_ #_ #HT1 #_ elim (cpxs_inv_abst1 … HT1) -HT1 #W2 #T2 #_ #_ #H destruct ] qed-. (* Note: probably this is an inversion lemma *) -lemma cpxs_fwd_delta: ∀h,g,I,G,L,K,V1,i. ⇩[0, i] L ≡ K.ⓑ{I}V1 → +lemma cpxs_fwd_delta: ∀h,g,I,G,L,K,V1,i. ⇩[i] L ≡ K.ⓑ{I}V1 → ∀V2. ⇧[0, i + 1] V1 ≡ V2 → ∀U. ⦃G, L⦄ ⊢ #i ➡*[h, g] U → #i ≃ U ∨ ⦃G, L⦄ ⊢ V2 ➡*[h, g] U. #h #g #I #G #L #K #V1 #i #HLK #V2 #HV12 #U #H -elim (cpxs_inv_lref1 … H) -H /2 width=1/ +elim (cpxs_inv_lref1 … H) -H /2 width=1 by or_introl/ * #I0 #K0 #V0 #U0 #HLK0 #HVU0 #HU0 lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H destruct -lapply (ldrop_fwd_drop2 … HLK) -HLK /3 width=9/ +/4 width=10 by cpxs_lift, ldrop_fwd_drop2, or_intror/ qed-. lemma cpxs_fwd_theta: ∀h,g,a,G,L,V1,V,T,U. ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}V.T ➡*[h, g] U → @@ -72,29 +72,29 @@ lemma cpxs_fwd_theta: ∀h,g,a,G,L,V1,V,T,U. ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}V.T ➡* ⦃G, L⦄ ⊢ ⓓ{a}V.ⓐV2.T ➡*[h, g] U. #h #g #a #G #L #V1 #V #T #U #H #V2 #HV12 elim (cpxs_inv_appl1 … H) -H * -[ -HV12 #V0 #T0 #_ #_ #H destruct /2 width=1/ +[ -HV12 #V0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair, or_introl/ | #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)) [2: /2 width=1/ ] - /4 width=7 by cpx_zeta, lift_bind, lift_flat/ (**) (* auto too slow without trace *) + @(cpxs_trans … (+ⓓV.ⓐV2.ⓛ{b}W2.T2)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T + @(cpxs_strap2 … (ⓐV1.ⓛ{b}W.T0)) [2: /2 width=1 by cpxs_beta_dx/ ] + /4 width=7 by cpx_zeta, lift_bind, lift_flat/ ] | #b #V3 #V4 #V0 #T0 #HV13 #HV34 #HT0 #HU @or_intror @(cpxs_trans … HU) -U (**) (* explicit constructor *) elim (cpxs_inv_abbr1 … HT0) -HT0 * [ #V5 #T5 #HV5 #HT5 #H destruct - lapply (cpxs_lift … HV13 (L.ⓓV) … HV12 … HV34) -V1 -V3 /2 width=1/ - /3 width=1/ + lapply (cpxs_lift … HV13 (L.ⓓV) … HV12 … HV34) -V1 -V3 + /3 width=2 by cpxs_flat, cpxs_bind, ldrop_drop/ | #X #HT1 #H #H0 destruct 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)) [ /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/ + lapply (cpxs_lift … HV13 (L.ⓓV0) … HV12 … HV34) -V3 /2 width=2 by ldrop_drop/ #HV24 + @(cpxs_trans … (+ⓓV.ⓐV2.ⓓ{b}V5.T5)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T + @(cpxs_strap2 … (ⓐV1.ⓓ{b}V0.T0)) [ /4 width=7 by cpx_zeta, lift_bind, lift_flat/ ] -V -V5 -T5 + @(cpxs_strap2 … (ⓓ{b}V0.ⓐV2.T0)) /3 width=3 by cpxs_pair_sn, cpxs_bind_dx, cpr_cpx, cpr_theta/ ] ] qed-. @@ -102,6 +102,6 @@ qed-. lemma cpxs_fwd_cast: ∀h,g,G,L,W,T,U. ⦃G, L⦄ ⊢ ⓝW.T ➡*[h, g] U → ∨∨ ⓝW. T ≃ U | ⦃G, L⦄ ⊢ T ➡*[h, g] U | ⦃G, L⦄ ⊢ W ➡*[h, g] U. #h #g #G #L #W #T #U #H -elim (cpxs_inv_cast1 … H) -H /2 width=1/ * -#W0 #T0 #_ #_ #H destruct /2 width=1/ +elim (cpxs_inv_cast1 … H) -H /2 width=1 by or3_intro1, or3_intro2/ * +#W0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair, or3_intro0/ qed-. 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 cea820cfb..08cf4d2cd 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 @@ -26,7 +26,7 @@ lemma cpxs_fwd_cnx_vector: ∀h,g,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍[h, #h #g #G #L #T #H1T #H2T #Vs elim Vs -Vs [ @(cpxs_fwd_cnx … H2T) ] (**) (* /2 width=3 by cpxs_fwd_cnx/ does not work *) #V #Vs #IHVs #U #H elim (cpxs_inv_appl1 … H) -H * -[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1/ +[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair/ | #a #W0 #T0 #HT0 #HU lapply (IHVs … HT0) -IHVs -HT0 #HT0 elim (tstc_inv_bind_appls_simple … HT0) // @@ -41,20 +41,20 @@ lemma cpxs_fwd_sort_vector: ∀h,g,G,L,k,Vs,U. ⦃G, L⦄ ⊢ ⒶVs.⋆k ➡*[h, #h #g #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/ +[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by tstc_pair, or_introl/ | #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/ + @(cpxs_strap1 … (ⓐV.ⓛ{a}W1.T1)) /3 width=1 by cpxs_flat_dx, cpr_cpx, cpr_beta/ ] | #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/ + @(cpxs_strap1 … (ⓐV1.ⓓ{a}V3.T1)) /3 width=3 by cpxs_flat, cpr_cpx, cpr_theta/ ] ] qed-. @@ -66,45 +66,45 @@ lemma cpxs_fwd_beta_vector: ∀h,g,a,G,L,Vs,V,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓐV. #h #g #a #G #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/ +[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by tstc_pair, or_introl/ | #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 … (ⓐV0.ⓛ{b}W1.T1)) [ /2 width=1/ ] -V -Vs -T /3 width=1/ + @(cpxs_strap1 … (ⓐV0.ⓛ{b}W1.T1)) /3 width=1 by cpxs_flat_dx, cpr_cpx, cpr_beta/ ] | #b #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.ⓓ{b}V3.T1)) [ /2 width=1/ ] -V -V0 -Vs -T /3 width=3/ + @(cpxs_strap1 … (ⓐV1.ⓓ{b}V3.T1)) /3 width=3 by cpxs_flat, cpr_cpx, cpr_theta/ ] ] qed-. -lemma cpxs_fwd_delta_vector: ∀h,g,I,G,L,K,V1,i. ⇩[0, i] L ≡ K.ⓑ{I}V1 → +lemma cpxs_fwd_delta_vector: ∀h,g,I,G,L,K,V1,i. ⇩[i] L ≡ K.ⓑ{I}V1 → ∀V2. ⇧[0, i + 1] V1 ≡ V2 → ∀Vs,U. ⦃G, L⦄ ⊢ ⒶVs.#i ➡*[h, g] U → ⒶVs.#i ≃ U ∨ ⦃G, L⦄ ⊢ ⒶVs.V2 ➡*[h, g] U. #h #g #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs /2 width=5 by cpxs_fwd_delta/ #V #Vs #IHVs #U #H -K -V1 elim (cpxs_inv_appl1 … H) -H * -[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1/ +[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair, or_introl/ | #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 … (ⓐV.ⓛ{b}W0.T0)) [ /2 width=1/ ] -V2 -Vs /3 width=1/ + @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) /3 width=1 by cpxs_flat_dx, cpr_cpx, cpr_beta/ ] | #b #V0 #V1 #V3 #T0 #HV0 #HV01 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0 [ elim (tstc_inv_bind_appls_simple … HT0) // | @or_intror -i (**) (* explicit constructor *) @(cpxs_trans … HU) -U - @(cpxs_strap1 … (ⓐV0.ⓓ{b}V3.T0)) [ /2 width=1/ ] -V -V2 -Vs /3 width=3/ + @(cpxs_strap1 … (ⓐV0.ⓓ{b}V3.T0)) /3 width=3 by cpxs_flat, cpr_cpx, cpr_theta/ ] ] qed-. @@ -113,7 +113,7 @@ qed-. lemma cpxs_fwd_theta_vector: ∀h,g,G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → ∀a,V,T,U. ⦃G, L⦄ ⊢ ⒶV1s.ⓓ{a}V.T ➡*[h, g] U → ⒶV1s. ⓓ{a}V. T ≃ U ∨ ⦃G, L⦄ ⊢ ⓓ{a}V.ⒶV2s.T ➡*[h, g] U. -#h #g #G #L #V1s #V2s * -V1s -V2s /3 width=1/ +#h #g #G #L #V1s #V2s * -V1s -V2s /3 width=1 by or_intror/ #V1s #V2s #V1a #V2a #HV12a #HV12s #a generalize in match HV12a; -HV12a generalize in match V2a; -V2a @@ -121,7 +121,7 @@ generalize in match V1a; -V1a 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/ +[ -IHV12s -HV12a -HV12b #V0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair, or_introl/ | #b #W0 #T0 #HT0 #HU elim (IHV12s … HV12b … HT0) -IHV12s -HT0 #HT0 [ -HV12a -HV12b -HU @@ -132,9 +132,9 @@ elim (cpxs_inv_appl1 … H) -H * [ -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)) [2: /2 width=1/ ] - /4 width=7 by cpx_zeta, lift_bind, lift_flat/ (* auto too slow without trace *) + @(cpxs_trans … (+ⓓV.ⓐV2a.ⓛ{b}W1.T1)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T -V2b -V2s + @(cpxs_strap2 … (ⓐV1a.ⓛ{b}W0.T0)) + /4 width=7 by cpxs_beta_dx, cpx_zeta, lift_bind, lift_flat/ ] ] | #b #V0a #Va #V0 #T0 #HV10a #HV0a #HT0 #HU @@ -145,14 +145,14 @@ elim (cpxs_inv_appl1 … H) -H * @(cpxs_trans … HU) -U elim (cpxs_inv_abbr1 … HT0) -HT0 * [ #V1 #T1 #HV1 #HT1 #H destruct - lapply (cpxs_lift … HV10a (L.ⓓV) … HV12a … HV0a) -V1a -V0a [ /2 width=1/ ] #HV2a - @(cpxs_trans … (ⓓ{a}V.ⓐV2a.T1)) [ /3 width=1/ ] -T -V2b -V2s /3 width=1/ + lapply (cpxs_lift … HV10a (L.ⓓV) (Ⓣ) … HV12a … HV0a) -V1a -V0a [ /2 width=1 by ldrop_drop/ ] #HV2a + @(cpxs_trans … (ⓓ{a}V.ⓐV2a.T1)) /3 width=1 by cpxs_bind, cpxs_pair_sn, cpxs_flat_dx, cpxs_bind_dx/ | #X #HT1 #H #H0 destruct 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)) [ /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/ + lapply (cpxs_lift … HV10a (L.ⓓV0) (Ⓣ) … HV12a … HV0a) -V0a [ /2 width=1 by ldrop_drop/ ] #HV2a + @(cpxs_trans … (+ⓓV.ⓐV2a.ⓓ{b}V1.T1)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T -V2b -V2s + @(cpxs_strap2 … (ⓐV1a.ⓓ{b}V0.T0)) [ /4 width=7 by cpx_zeta, lift_bind, lift_flat/ ] -V -V1 -T1 + @(cpxs_strap2 … (ⓓ{b}V0.ⓐV2a.T0)) /3 width=3 by cpxs_pair_sn, cpxs_bind_dx, cpr_cpx, cpr_theta/ ] ] ] @@ -166,26 +166,25 @@ lemma cpxs_fwd_cast_vector: ∀h,g,G,L,Vs,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓝW.T ➡ #h #g #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 #W0 #T0 #HT0 #HU - elim (IHVs … HT0) -IHVs -HT0 #HT0 +[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair, or3_intro0/ +| #b #W0 #T0 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0 [ elim (tstc_inv_bind_appls_simple … HT0) // | @or3_intro1 -W (**) (* explicit constructor *) @(cpxs_trans … HU) -U - @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) /2 width=1/ + @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) /2 width=1 by cpxs_flat_dx, cpx_beta/ | @or3_intro2 -T (**) (* explicit constructor *) @(cpxs_trans … HU) -U - @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) /2 width=1/ + @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) /2 width=1 by cpxs_flat_dx, cpx_beta/ ] | #b #V0 #V1 #V2 #T0 #HV0 #HV01 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0 [ elim (tstc_inv_bind_appls_simple … HT0) // | @or3_intro1 -W (**) (* explicit constructor *) @(cpxs_trans … HU) -U - @(cpxs_strap1 … (ⓐV0.ⓓ{b}V2.T0)) [ /2 width=1/ ] -V -Vs -T /2 width=3/ + @(cpxs_strap1 … (ⓐV0.ⓓ{b}V2.T0)) /2 width=3 by cpxs_flat, cpx_theta/ | @or3_intro2 -T (**) (* explicit constructor *) @(cpxs_trans … HU) -U - @(cpxs_strap1 … (ⓐV0.ⓓ{b}V2.T0)) [ /2 width=1/ ] -V -Vs -W /2 width=3/ + @(cpxs_strap1 … (ⓐV0.ⓓ{b}V2.T0)) /2 width=3 by cpxs_flat, cpx_theta/ ] ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma index 4f06e7912..5ad268e0f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma @@ -21,9 +21,9 @@ include "basic_2/computation/csx.ma". (* Relocation properties ****************************************************) (* Basic_1: was just: sn3_lift *) -lemma csx_lift: ∀h,g,G,L2,L1,T1,d,e. ⦃G, L1⦄ ⊢ ⬊*[h, g] T1 → - ∀T2. ⇩[d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → ⦃G, L2⦄ ⊢ ⬊*[h, g] T2. -#h #g #G #L2 #L1 #T1 #d #e #H elim H -T1 #T1 #_ #IHT1 #T2 #HL21 #HT12 +lemma csx_lift: ∀h,g,G,L2,L1,T1,s,d,e. ⦃G, L1⦄ ⊢ ⬊*[h, g] T1 → + ∀T2. ⇩[s, d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → ⦃G, L2⦄ ⊢ ⬊*[h, g] T2. +#h #g #G #L2 #L1 #T1 #s #d #e #H elim H -T1 #T1 #_ #IHT1 #T2 #HL21 #HT12 @csx_intro #T #HLT2 #HT2 elim (cpx_inv_lift1 … HLT2 … HL21 … HT12) -HLT2 #T0 #HT0 #HLT10 @(IHT1 … HLT10) // -L1 -L2 #H destruct @@ -31,9 +31,9 @@ elim (cpx_inv_lift1 … HLT2 … HL21 … HT12) -HLT2 #T0 #HT0 #HLT10 qed. (* Basic_1: was just: sn3_gen_lift *) -lemma csx_inv_lift: ∀h,g,G,L2,L1,T1,d,e. ⦃G, L1⦄ ⊢ ⬊*[h, g] T1 → - ∀T2. ⇩[d, e] L1 ≡ L2 → ⇧[d, e] T2 ≡ T1 → ⦃G, L2⦄ ⊢ ⬊*[h, g] T2. -#h #g #G #L2 #L1 #T1 #d #e #H elim H -T1 #T1 #_ #IHT1 #T2 #HL12 #HT21 +lemma csx_inv_lift: ∀h,g,G,L2,L1,T1,s,d,e. ⦃G, L1⦄ ⊢ ⬊*[h, g] T1 → + ∀T2. ⇩[s, d, e] L1 ≡ L2 → ⇧[d, e] T2 ≡ T1 → ⦃G, L2⦄ ⊢ ⬊*[h, g] T2. +#h #g #G #L2 #L1 #T1 #s #d #e #H elim H -T1 #T1 #_ #IHT1 #T2 #HL12 #HT21 @csx_intro #T #HLT2 #HT2 elim (lift_total T d e) #T0 #HT0 lapply (cpx_lift … HLT2 … HL12 … HT21 … HT0) -HLT2 #HLT10 @@ -44,7 +44,7 @@ qed. (* Advanced inversion lemmas ************************************************) (* Basic_1: was: sn3_gen_def *) -lemma csx_inv_lref_bind: ∀h,g,I,G,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → +lemma csx_inv_lref_bind: ∀h,g,I,G,L,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, L⦄ ⊢ ⬊*[h, g] #i → ⦃G, K⦄ ⊢ ⬊*[h, g] V. #h #g #I #G #L #K #V #i #HLK #Hi elim (lift_total V 0 (i+1)) @@ -54,14 +54,14 @@ qed-. (* Advanced properties ******************************************************) (* Basic_1: was just: sn3_abbr *) -lemma csx_lref_bind: ∀h,g,I,G,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ ⬊*[h, g] V → ⦃G, L⦄ ⊢ ⬊*[h, g] #i. +lemma csx_lref_bind: ∀h,g,I,G,L,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ ⬊*[h, g] V → ⦃G, L⦄ ⊢ ⬊*[h, g] #i. #h #g #I #G #L #K #V #i #HLK #HV @csx_intro #X #H #Hi elim (cpx_inv_lref1 … H) -H [ #H destruct elim Hi // | -Hi * #I0 #K0 #V0 #V1 #HLK0 #HV01 #HV1 lapply (ldrop_mono … HLK0 … HLK) -HLK #H destruct - /3 width=7 by csx_lift, csx_cpx_trans, ldrop_fwd_drop2/ + /3 width=8 by csx_lift, csx_cpx_trans, ldrop_fwd_drop2/ ] qed. @@ -82,7 +82,7 @@ qed. lemma csx_fqu_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 → ⦃G2, L2⦄ ⊢ ⬊*[h, g] T2. #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 -/2 width=7 by csx_inv_lref_bind, csx_inv_lift, csx_fwd_flat_dx, csx_fwd_bind_dx, csx_fwd_pair_sn/ +/2 width=8 by csx_inv_lref_bind, csx_inv_lift, csx_fwd_flat_dx, csx_fwd_bind_dx, csx_fwd_pair_sn/ qed-. lemma csx_fquq_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → @@ -112,7 +112,7 @@ qed-. theorem csx_acp: ∀h,g. acp (cpx h g) (eq …) (csx h g). #h #g @mk_acp [ #G #L elim (deg_total h g 0) /3 width=8 by cnx_sort_iter, ex_intro/ -| /3 width=12 by cnx_lift/ +| /3 width=13 by cnx_lift/ | /2 width=3 by csx_fwd_flat_dx/ | /2 width=1 by csx_cast/ ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma index c387f545c..d1211415a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma @@ -23,9 +23,8 @@ include "basic_2/computation/csx_lift.ma". lemma csx_lpx_conf: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → ∀T. ⦃G, L1⦄ ⊢ ⬊*[h, g] T → ⦃G, L2⦄ ⊢ ⬊*[h, g] T. -#h #g #G #L1 #L2 #HL12 #T #H @(csx_ind_alt … H) -T #T #_ #IHT -@csx_intro #T0 #HLT0 #HT0 -@IHT /2 width=2/ -IHT -HT0 /2 width=3 by lpx_cpx_trans/ +#h #g #G #L1 #L2 #HL12 #T #H @(csx_ind_alt … H) -T +/4 width=3 by csx_intro, lpx_cpx_trans/ qed. lemma csx_abst: ∀h,g,a,G,L,W. ⦃G, L⦄ ⊢ ⬊*[h, g] W → @@ -36,8 +35,8 @@ elim (cpx_inv_abst1 … H1) -H1 #W0 #T0 #HLW0 #HLT0 #H destruct elim (eq_false_inv_tpair_sn … H2) -H2 [ -IHT #H lapply (csx_cpx_trans … HLT0) // -HT - #HT0 lapply (csx_lpx_conf … (L.ⓛW0) … HT0) -HT0 /2 width=1/ /3 width=1/ -| -IHW -HLW0 -HT * #H destruct /3 width=1/ + #HT0 lapply (csx_lpx_conf … (L.ⓛW0) … HT0) -HT0 /3 width=1 by lpx_pair/ +| -IHW -HLW0 -HT * #H destruct /3 width=1 by/ ] qed. @@ -48,13 +47,11 @@ lemma csx_abbr: ∀h,g,a,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V → elim (cpx_inv_abbr1 … H1) -H1 * [ #V1 #T1 #HLV1 #HLT1 #H destruct elim (eq_false_inv_tpair_sn … H2) -H2 - [ #HV1 @IHV // /2 width=1/ -HV1 - @(csx_lpx_conf … (L.ⓓV)) /2 width=1/ -HLV1 /2 width=3 by csx_cpx_trans/ - | -IHV -HLV1 * #H destruct /3 width=1/ + [ /4 width=5 by csx_cpx_trans, csx_lpx_conf, lpx_pair/ + | -IHV -HLV1 * #H destruct /3 width=1 by cpx_cpxs/ ] -| -IHV -IHT -H2 #T0 #HLT0 #HT0 - lapply (csx_cpx_trans … HT … HLT0) -T #HLT0 - lapply (csx_inv_lift … HLT0 … HT0) -T0 /2 width=3/ +| -IHV -IHT -H2 + /3 width=8 by csx_cpx_trans, csx_inv_lift, ldrop_drop/ ] qed. @@ -66,11 +63,11 @@ fact csx_appl_beta_aux: ∀h,g,a,G,L,U1. ⦃G, L⦄ ⊢ ⬊*[h, g] U1 → elim (cpx_inv_appl1 … H1) -H1 * [ -HT1 #V0 #Y #HLV0 #H #H0 destruct elim (cpx_inv_abst1 … H) -H #W0 #T0 #HLW0 #HLT0 #H destruct - @IHT1 -IHT1 [4: // | skip |3: #H destruct /2 width=1/ ] -H2 - lapply (lsubr_cpx_trans … HLT0 (L.ⓓⓝW.V) ?) -HLT0 [ /2 width=1/ ] /3 width=1/ + @IHT1 -IHT1 [4: // | skip |3: #H destruct /2 width=1 by/ ] -H2 + lapply (lsubr_cpx_trans … HLT0 (L.ⓓⓝW.V) ?) -HLT0 /3 width=1 by cpx_bind, cpx_flat, lsubr_abst/ | -IHT1 -H2 #b #V0 #W0 #W2 #T0 #T2 #HLV0 #HLW02 #HLT02 #H1 #H3 destruct - lapply (lsubr_cpx_trans … HLT02 (L.ⓓⓝW0.V) ?) -HLT02 [ /2 width=1/ ] #HT02 - @(csx_cpx_trans … HT1) -HT1 /3 width=1/ + lapply (lsubr_cpx_trans … HLT02 (L.ⓓⓝW0.V) ?) -HLT02 + /4 width=5 by csx_cpx_trans, cpx_bind, cpx_flat, lsubr_abst/ | -HT1 -IHT1 -H2 #b #V0 #V1 #W0 #W1 #T0 #T3 #_ #_ #_ #_ #H destruct ] qed-. @@ -99,20 +96,20 @@ elim (cpx_inv_appl1 … HL) -HL * | * #_ #H elim H // ] | -H -HVT #H - lapply (cpx_lift … HLV10 (L. ⓓV) … HV12 … HV04) -HLV10 -HV12 /2 width=1/ #HV24 - @(IHVT … H … HV04) -IHVT // -H -HV04 /4 width=1/ + lapply (cpx_lift … HLV10 (L.ⓓV) (Ⓣ) … HV12 … HV04) -HLV10 -HV12 /2 width=1 by ldrop_drop/ #HV24 + @(IHVT … H … HV04) -IHVT /4 width=1 by cpx_cpxs, cpx_bind, cpx_flat/ ] | -H -IHVT #T0 #HLT0 #HT0 #H0 destruct - lapply (csx_cpx_trans … HVT (ⓐV2.T0) ?) /2 width=1/ -T #HVT0 - lapply (csx_inv_lift … L … 1 HVT0 ? ? ?) -HVT0 [ /2 width=4/ |2,3: skip | /2 width=1/ ] -V2 -T0 #HVY - @(csx_cpx_trans … HVY) /2 width=1/ + lapply (csx_cpx_trans … HVT (ⓐV2.T0) ?) /2 width=1 by cpx_flat/ -T #HVT0 + lapply (csx_inv_lift … L … (Ⓣ) … 1 HVT0 ? ? ?) -HVT0 + /3 width=5 by csx_cpx_trans, cpx_pair_sn, ldrop_drop, lift_flat/ ] | -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 + lapply (cpx_lift … HLV10 (L. ⓓW0) … HV12 … HV03) -HLV10 -HV12 -HV03 /2 width=2 by ldrop_drop/ #HLV23 @csx_abbr /2 width=3 by csx_cpx_trans/ -HV - @(csx_lpx_conf … (L. ⓓW0)) /2 width=1/ -W1 - @(csx_cpxs_trans … HVT) -HVT /3 width=1/ + @(csx_lpx_conf … (L.ⓓW0)) /2 width=1 by lpx_pair/ -W1 + /4 width=5 by csx_cpxs_trans, cpx_cpxs, cpx_flat/ ] qed-. @@ -130,18 +127,12 @@ elim (cpx_inv_appl1_simple … HL) -HL // #V0 #T0 #HLV0 #HLT10 #H0 destruct elim (eq_false_inv_tpair_sn … H) -H [ -IHT1 #HV0 - @(csx_cpx_trans … (ⓐV0.T1)) /2 width=1/ -HLT10 - @IHV -IHV // -H1T1 -H3T1 /2 width=1/ -HV0 - #T2 #HLT12 #HT12 - @(csx_cpx_trans … (ⓐV.T2)) /2 width=1/ -HLV0 - @H2T1 -H2T1 // -HLT12 /2 width=1/ + @(csx_cpx_trans … (ⓐV0.T1)) /2 width=1 by cpx_flat/ -HLT10 + @IHV -IHV /4 width=3 by csx_cpx_trans, cpx_pair_sn/ | -IHV -H1T1 -HLV0 * #H #H1T10 destruct elim (tstc_dec T1 T0) #H2T10 - [ @IHT1 -IHT1 // /2 width=1/ -H1T10 /2 width=3/ -H3T1 - #T2 #HLT02 #HT02 - @H2T1 -H2T1 /2 width=3/ -HLT10 -HLT02 /3 width=3/ - | -IHT1 -H3T1 -H1T10 - @H2T1 -H2T1 /2 width=1/ + [ @IHT1 -IHT1 /4 width=3 by cpxs_strap2, cpxs_strap1, tstc_canc_sn, simple_tstc_repl_dx/ + | -IHT1 -H3T1 -H1T10 /3 width=1 by cpx_cpxs/ ] ] qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma index e16b976a7..55099d325 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma @@ -27,7 +27,7 @@ lemma csx_applv_cnx: ∀h,g,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T #h #g #G #L #T #H1T #H2T #Vs elim Vs -Vs [ #_ @(cnx_csx … H2T) ] (**) (* /2 width=1/ does not work *) #V #Vs #IHV #H elim (csxv_inv_cons … H) -H #HV #HVs -@csx_appl_simple_tstc // -HV /2 width=1/ -IHV -HVs +@csx_appl_simple_tstc /2 width=1 by applv_simple/ -IHV -HV -HVs #X #H #H0 lapply (cpxs_fwd_cnx_vector … H) -H // -H1T -H2T #H elim (H0) -H0 // @@ -35,49 +35,47 @@ qed. lemma csx_applv_sort: ∀h,g,G,L,k,Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Vs → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.⋆k. #h #g #G #L #k elim (deg_total h g k) -#l generalize in match k; -k @(nat_ind_plus … l) -l [ /3 width=1/ ] +#l generalize in match k; -k @(nat_ind_plus … l) -l [ /3 width=1 by csx_applv_cnx, cnx_sort, simple_atom/ ] #l #IHl #k #Hkl lapply (deg_next_SO … Hkl) -Hkl -#Hkl #Vs elim Vs -Vs /2 width=1/ +#Hkl #Vs elim Vs -Vs /2 width=1 by/ #V #Vs #IHVs #HVVs elim (csxv_inv_cons … HVVs) #HV #HVs -@csx_appl_simple_tstc // -HV /2 width=1/ -IHVs -HVs +@csx_appl_simple_tstc /2 width=1 by applv_simple, simple_atom/ -IHVs -HV -HVs #X #H #H0 elim (cpxs_fwd_sort_vector … H) -H #H [ elim H0 -H0 // -| -H0 @(csx_cpxs_trans … (Ⓐ(V@Vs).⋆(next h k))) /2 width=1/ +| -H0 @(csx_cpxs_trans … (Ⓐ(V@Vs).⋆(next h k))) /2 width=1 by cpxs_flat_dx/ ] qed. (* Basic_1: was just: sn3_appls_beta *) lemma csx_applv_beta: ∀h,g,a,G,L,Vs,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.ⓓ{a}ⓝW.V.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs. ⓐV.ⓛ{a}W.T. -#h #g #a #G #L #Vs elim Vs -Vs /2 width=1/ +#h #g #a #G #L #Vs elim Vs -Vs /2 width=1 by csx_appl_beta/ #V0 #Vs #IHV #V #W #T #H1T lapply (csx_fwd_pair_sn … H1T) #HV0 lapply (csx_fwd_flat_dx … H1T) #H2T -@csx_appl_simple_tstc // -HV0 /2 width=1/ -IHV -H2T +@csx_appl_simple_tstc /2 width=1 by applv_simple, simple_flat/ -IHV -HV0 -H2T #X #H #H0 elim (cpxs_fwd_beta_vector … H) -H #H [ -H1T elim H0 -H0 // -| -H0 @(csx_cpxs_trans … H1T) -H1T /2 width=1/ +| -H0 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/ ] qed. -lemma csx_applv_delta: ∀h,g,I,G,L,K,V1,i. ⇩[0, i] L ≡ K.ⓑ{I}V1 → +lemma csx_applv_delta: ∀h,g,I,G,L,K,V1,i. ⇩[i] L ≡ K.ⓑ{I}V1 → ∀V2. ⇧[0, i + 1] V1 ≡ V2 → ∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] (ⒶVs.V2) → ⦃G, L⦄ ⊢ ⬊*[h, g] (ⒶVs.#i). #h #g #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs -[ #H - lapply (ldrop_fwd_drop2 … HLK) #HLK0 - lapply (csx_inv_lift … H … HLK0 HV12) -V2 -HLK0 /2 width=5/ +[ /4 width=12 by csx_inv_lift, csx_lref_bind, ldrop_fwd_drop2/ | #V #Vs #IHV #H1T lapply (csx_fwd_pair_sn … H1T) #HV lapply (csx_fwd_flat_dx … H1T) #H2T - @csx_appl_simple_tstc // -HV /2 width=1/ -IHV -H2T + @csx_appl_simple_tstc /2 width=1 by applv_simple, simple_atom/ -IHV -HV -H2T #X #H #H0 elim (cpxs_fwd_delta_vector … HLK … HV12 … H) -HLK -HV12 -H #H [ -H1T elim H0 -H0 // - | -H0 @(csx_cpxs_trans … H1T) -H1T /2 width=1/ + | -H0 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/ ] ] qed. @@ -86,46 +84,46 @@ qed. lemma csx_applv_theta: ∀h,g,a,G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → ∀V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V.ⒶV2s.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶV1s.ⓓ{a}V.T. -#h #g #a #G #L #V1s #V2s * -V1s -V2s /2 width=1/ +#h #g #a #G #L #V1s #V2s * -V1s -V2s /2 width=1 by/ #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/ +elim H -V1s -V2s /2 width=3 by csx_appl_theta/ #V1s #V2s #V1 #V2 #HV12 #HV12s #IHV12s #W1 #W2 #HW12 #V #T #H lapply (csx_appl_theta … HW12 … H) -H -HW12 #H lapply (csx_fwd_pair_sn … H) #HW1 lapply (csx_fwd_flat_dx … H) #H1 -@csx_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 +@csx_appl_simple_tstc /2 width=3 by simple_flat/ -IHV12s -HW1 -H1 #X #H1 #H2 +elim (cpxs_fwd_theta_vector … (V2@V2s) … H1) -H1 /2 width=1 by liftv_cons/ -HV12s -HV12 [ -H #H elim H2 -H2 // -| -H2 #H1 @(csx_cpxs_trans … H) -H /2 width=1/ +| -H2 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/ ] qed. (* Basic_1: was just: sn3_appls_cast *) lemma csx_applv_cast: ∀h,g,G,L,Vs,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.W → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.ⓝW.T. -#h #g #G #L #Vs elim Vs -Vs /2 width=1/ +#h #g #G #L #Vs elim Vs -Vs /2 width=1 by csx_cast/ #V #Vs #IHV #W #T #H1W #H1T lapply (csx_fwd_pair_sn … H1W) #HV lapply (csx_fwd_flat_dx … H1W) #H2W lapply (csx_fwd_flat_dx … H1T) #H2T -@csx_appl_simple_tstc // -HV /2 width=1/ -IHV -H2W -H2T +@csx_appl_simple_tstc /2 width=1 by applv_simple, simple_flat/ -IHV -HV -H2W -H2T #X #H #H0 elim (cpxs_fwd_cast_vector … H) -H #H [ -H1W -H1T elim H0 -H0 // -| -H1W -H0 @(csx_cpxs_trans … H1T) -H1T /2 width=1/ -| -H1T -H0 @(csx_cpxs_trans … H1W) -H1W /2 width=1/ +| -H1W -H0 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/ +| -H1T -H0 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/ ] qed. theorem csx_acr: ∀h,g. acr (cpx h g) (eq …) (csx h g) (λG,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T). #h #g @mk_acr // -[ /3 width=1/ -|2,3,6: /2 width=1/ -| /2 width=7/ +[ /3 width=1 by csx_applv_cnx/ +|2,3,6: /2 width=1 by csx_applv_beta, csx_applv_sort, csx_applv_cast/ +| /2 width=7 by csx_applv_delta/ | #G #L #V1s #V2s #HV12s #a #V #T #H #HV @(csx_applv_theta … HV12s) -HV12s - @(csx_abbr) // -| @csx_lift + @csx_abbr // +| /2 width=8 by csx_lift/ ] qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_cprs.ma index a1c408660..70345be5c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_cprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_cprs.ma @@ -49,13 +49,13 @@ lemma lprs_cprs_conf_dx: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡* T1 → ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T. #G #L0 #T0 #T1 #HT01 #L1 #H elim H -L1 [ #L1 #HL01 - elim (cprs_lpr_conf_dx … HT01 … HL01) -L0 /2 width=3/ + elim (cprs_lpr_conf_dx … HT01 … HL01) -L0 /2 width=3 by ex2_intro/ | #L #L1 #_ #HL1 * #T #HT1 #HT0 -L0 elim (cprs_lpr_conf_dx … HT1 … HL1) -HT1 #T2 #HT2 #HT12 elim (cprs_lpr_conf_dx … HT0 … HL1) -L #T3 #HT3 #HT03 elim (cprs_conf … HT2 … HT3) -T #T #HT2 #HT3 lapply (cprs_trans … HT03 … HT3) -T3 - lapply (cprs_trans … HT12 … HT2) -T2 /2 width=3/ + lapply (cprs_trans … HT12 … HT2) -T2 /2 width=3 by ex2_intro/ ] qed-. @@ -69,7 +69,7 @@ lemma lprs_cprs_conf_sn: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡* T1 → ∃∃T. ⦃G, L0⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T. #G #L0 #T0 #T1 #HT01 #L1 #HL01 elim (lprs_cprs_conf_dx … HT01 … HL01) -HT01 #T #HT1 -lapply (lprs_cprs_trans … HT1 … HL01) -HT1 /2 width=3/ +lapply (lprs_cprs_trans … HT1 … HL01) -HT1 /2 width=3 by ex2_intro/ qed-. lemma lprs_cpr_conf_sn: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡ T1 → @@ -81,7 +81,7 @@ lemma cprs_bind2: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡* V2 → ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡* T2 → ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡* ⓑ{a,I}V2.T2. #G #L #V1 #V2 #HV12 #I #T1 #T2 #HT12 -lapply (lprs_cprs_trans … HT12 (L.ⓑ{I}V1) ?) /2 width=1/ +lapply (lprs_cprs_trans … HT12 (L.ⓑ{I}V1) ?) /2 width=1 by lprs_pair, cprs_bind/ qed. (* Inversion lemmas on context-sensitive parallel computation for terms *****) @@ -90,18 +90,18 @@ qed. lemma cprs_inv_abst1: ∀a,G,L,W1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ➡* U2 → ∃∃W2,T2. ⦃G, L⦄ ⊢ W1 ➡* W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ➡* T2 & U2 = ⓛ{a}W2.T2. -#a #G #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /2 width=5/ +#a #G #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /2 width=5 by ex3_2_intro/ #U0 #U2 #_ #HU02 * #V0 #T0 #HV10 #HT10 #H destruct elim (cpr_inv_abst1 … HU02) -HU02 #V2 #T2 #HV02 #HT02 #H destruct -lapply (lprs_cpr_trans … HT02 (L.ⓛV1) ?) /2 width=1/ -HT02 #HT02 +lapply (lprs_cpr_trans … HT02 (L.ⓛV1) ?) /2 width=1 by lprs_pair/ -HT02 #HT02 lapply (cprs_strap1 … HV10 … HV02) -V0 -lapply (cprs_trans … HT10 … HT02) -T0 /2 width=5/ +lapply (cprs_trans … HT10 … HT02) -T0 /2 width=5 by ex3_2_intro/ qed-. lemma cprs_inv_abst: ∀a,G,L,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ➡* ⓛ{a}W2.T2 → ⦃G, L⦄ ⊢ W1 ➡* W2 ∧ ⦃G, L.ⓛW1⦄ ⊢ T1 ➡* T2. #a #G #L #W1 #W2 #T1 #T2 #H -elim (cprs_inv_abst1 … H) -H #W #T #HW1 #HT1 #H destruct /2 width=1/ +elim (cprs_inv_abst1 … H) -H #W #T #HW1 #HT1 #H destruct /2 width=1 by conj/ qed-. (* Basic_1: was pr3_gen_abbr *) @@ -110,21 +110,22 @@ lemma cprs_inv_abbr1: ∀a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{a}V1.T1 ➡* U2 → U2 = ⓓ{a}V2.T2 ) ∨ ∃∃T2. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡* T2 & ⇧[0, 1] U2 ≡ T2 & a = true. -#a #G #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/ +#a #G #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5 by ex3_2_intro, or_introl/ #U0 #U2 #_ #HU02 * * [ #V0 #T0 #HV10 #HT10 #H destruct elim (cpr_inv_abbr1 … HU02) -HU02 * [ #V2 #T2 #HV02 #HT02 #H destruct - lapply (lprs_cpr_trans … HT02 (L.ⓓV1) ?) /2 width=1/ -HT02 #HT02 + lapply (lprs_cpr_trans … HT02 (L.ⓓV1) ?) /2 width=1 by lprs_pair/ -HT02 #HT02 lapply (cprs_strap1 … HV10 … HV02) -V0 - lapply (cprs_trans … HT10 … HT02) -T0 /3 width=5/ + lapply (cprs_trans … HT10 … HT02) -T0 /3 width=5 by ex3_2_intro, or_introl/ | #T2 #HT02 #HUT2 - lapply (lprs_cpr_trans … HT02 (L.ⓓV1) ?) -HT02 /2 width=1/ -V0 #HT02 - lapply (cprs_trans … HT10 … HT02) -T0 /3 width=3/ + lapply (lprs_cpr_trans … HT02 (L.ⓓV1) ?) -HT02 /2 width=1 by lprs_pair/ -V0 #HT02 + lapply (cprs_trans … HT10 … HT02) -T0 /3 width=3 by ex3_intro, or_intror/ ] | #U1 #HTU1 #HU01 elim (lift_total U2 0 1) #U #HU2 - lapply (cpr_lift … HU02 (L.ⓓV1) … HU01 … HU2) -U0 /2 width=1/ /4 width=3/ + lapply (cpr_lift … HU02 (L.ⓓV1) … HU01 … HU2) -U0 + /4 width=3 by cprs_strap1, ldrop_drop, ex3_intro, or_intror/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma index c961d137c..b22ee7c89 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma @@ -77,7 +77,7 @@ lemma cpxs_inv_abbr1: ∀h,g,a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{a}V1.T1 ➡*[h, ] | #U1 #HTU1 #HU01 elim (lift_total U2 0 1) #U #HU2 - /6 width=11 by cpxs_strap1, cpx_lift, ldrop_drop, ex3_intro, or_intror/ + /6 width=12 by cpxs_strap1, cpx_lift, ldrop_drop, ex3_intro, or_intror/ ] 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 2c352dc89..c2cd35475 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_ldrop.ma @@ -21,46 +21,52 @@ include "basic_2/computation/lsubc.ma". (* Basic_1: was: csubc_drop_conf_O *) (* Note: the constant 0 can not be generalized *) -lemma lsubc_ldrop_O1_trans: ∀RP,G,L1,L2. G ⊢ L1 ⊑[RP] L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 → - ∃∃K1. ⇩[0, e] L1 ≡ K1 & G ⊢ K1 ⊑[RP] K2. +lemma lsubc_ldrop_O1_trans: ∀RP,G,L1,L2. G ⊢ L1 ⊑[RP] L2 → ∀K2,s,e. ⇩[s, 0, e] L2 ≡ K2 → + ∃∃K1. ⇩[s, 0, e] L1 ≡ K1 & G ⊢ K1 ⊑[RP] K2. #RP #G #L1 #L2 #H elim H -L1 -L2 -[ #X #e #H elim (ldrop_inv_atom1 … H) -H /2 width=3/ -| #I #L1 #L2 #V #_ #IHL12 #X #e #H +[ #X #s #e #H elim (ldrop_inv_atom1 … H) -H /4 width=3 by ldrop_atom, ex2_intro/ +| #I #L1 #L2 #V #_ #IHL12 #X #s #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=3/ - | elim (IHL12 … H) -L2 /3 width=3/ + [ elim (IHL12 L2 s 0) -IHL12 // #X #H <(ldrop_inv_O2 … H) -H + /3 width=3 by lsubc_pair, ldrop_pair, ex2_intro/ + | elim (IHL12 … H) -L2 /3 width=3 by ldrop_drop_lt, ex2_intro/ ] -| #L1 #L2 #V #W #A #HV #H1W #H2W #_ #IHL12 #X #e #H +| #L1 #L2 #V #W #A #HV #H1W #H2W #_ #IHL12 #X #s #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=8/ - | elim (IHL12 … H) -L2 /3 width=3/ + [ elim (IHL12 L2 s 0) -IHL12 // #X #H <(ldrop_inv_O2 … H) -H + /3 width=8 by lsubc_abbr, ldrop_pair, ex2_intro/ + | elim (IHL12 … H) -L2 /3 width=3 by ldrop_drop_lt, ex2_intro/ ] +] qed-. (* Basic_1: was: csubc_drop_conf_rev *) lemma ldrop_lsubc_trans: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) → - ∀G,L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀K2. G ⊢ K1 ⊑[RP] K2 → - ∃∃L2. G ⊢ L1 ⊑[RP] L2 & ⇩[d, e] L2 ≡ K2. + ∀G,L1,K1,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ∀K2. G ⊢ K1 ⊑[RP] K2 → + ∃∃L2. G ⊢ L1 ⊑[RP] L2 & ⇩[Ⓕ, d, e] L2 ≡ K2. #RR #RS #RP #Hacp #Hacr #G #L1 #K1 #d #e #H elim H -L1 -K1 -d -e -[ #d #X #H elim (lsubc_inv_atom1 … H) -H /2 width=3/ +[ #d #e #He #X #H elim (lsubc_inv_atom1 … H) -H + >He /2 width=3 by ex2_intro/ | #L1 #I #V1 #X #H elim (lsubc_inv_pair1 … H) -H * - [ #K1 #HLK1 #H destruct /3 width=3/ - | #K1 #V #W1 #A #HV1 #H1W1 #H2W1 #HLK1 #H1 #H2 #H3 destruct /3 width=4/ + [ #K1 #HLK1 #H destruct /3 width=3 by lsubc_pair, ldrop_pair, ex2_intro/ + | #K1 #V #W1 #A #HV1 #H1W1 #H2W1 #HLK1 #H1 #H2 #H3 destruct + /3 width=4 by lsubc_abbr, ldrop_pair, ex2_intro/ ] -| #L1 #K1 #I #V1 #e #_ #IHLK1 #K2 #HK12 - elim (IHLK1 … HK12) -K1 /3 width=5/ -| #L1 #K1 #I #V1 #V2 #d #e #HLK1 #HV21 #IHLK1 #X #H +| #I #L1 #K1 #V1 #e #_ #IHLK1 #K2 #HK12 + elim (IHLK1 … HK12) -K1 /3 width=5 by lsubc_pair, ldrop_drop, ex2_intro/ +| #I #L1 #K1 #V1 #V2 #d #e #HLK1 #HV21 #IHLK1 #X #H elim (lsubc_inv_pair1 … H) -H * [ #K2 #HK12 #H destruct - elim (IHLK1 … HK12) -K1 /3 width=5/ + elim (IHLK1 … HK12) -K1 /3 width=5 by lsubc_pair, ldrop_skip, ex2_intro/ | #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 HV3) -HV2 - lapply (s8 … HA … H1W2 … HLK1 HW23) -H1W2 /4 width=10/ + lapply (s8 … HA … H1W2 … HLK1 HW23) -H1W2 + /4 width=11 by lsubc_abbr, aaa_lift, ldrop_skip, ex2_intro/ ] ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_ldrops.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_ldrops.ma index 36e48a49b..7acb1fc7a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_ldrops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_ldrops.ma @@ -21,12 +21,12 @@ include "basic_2/computation/lsubc_ldrop.ma". (* Basic_1: was: csubc_drop1_conf_rev *) lemma ldrops_lsubc_trans: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) → - ∀G,L1,K1,des. ⇩*[des] L1 ≡ K1 → ∀K2. G ⊢ K1 ⊑[RP] K2 → - ∃∃L2. G ⊢ L1 ⊑[RP] L2 & ⇩*[des] L2 ≡ K2. + ∀G,L1,K1,des. ⇩*[Ⓕ, des] L1 ≡ K1 → ∀K2. G ⊢ K1 ⊑[RP] K2 → + ∃∃L2. G ⊢ L1 ⊑[RP] L2 & ⇩*[Ⓕ, des] L2 ≡ K2. #RR #RS #RP #Hacp #Hacr #G #L1 #K1 #des #H elim H -L1 -K1 -des -[ /2 width=3/ +[ /2 width=3 by ldrops_nil, ex2_intro/ | #L1 #L #K1 #des #d #e #_ #HLK1 #IHL #K2 #HK12 elim (ldrop_lsubc_trans … Hacp Hacr … HLK1 … HK12) -Hacp -Hacr -K1 #K #HLK #HK2 - elim (IHL … HLK) -IHL -HLK /3 width=5/ + elim (IHL … HLK) -IHL -HLK /3 width=5 by ldrops_cons, ex2_intro/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ldrop.ma index 7bf755141..3f184b6d2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ldrop.ma @@ -20,46 +20,46 @@ include "basic_2/dynamic/lsubsv.ma". (* Note: the constant 0 cannot be generalized *) lemma lsubsv_ldrop_O1_conf: ∀h,g,G,L1,L2. G ⊢ L1 ¡⊑[h, g] L2 → - ∀K1,e. ⇩[0, e] L1 ≡ K1 → - ∃∃K2. G ⊢ K1 ¡⊑[h, g] K2 & ⇩[0, e] L2 ≡ K2. + ∀K1,s,e. ⇩[s, 0, e] L1 ≡ K1 → + ∃∃K2. G ⊢ K1 ¡⊑[h, g] K2 & ⇩[s, 0, e] L2 ≡ K2. #h #g #G #L1 #L2 #H elim H -L1 -L2 -[ /2 width=3/ -| #I #L1 #L2 #V #_ #IHL12 #K1 #e #H +[ /2 width=3 by ex2_intro/ +| #I #L1 #L2 #V #_ #IHL12 #K1 #s #e #H elim (ldrop_inv_O1_pair1 … H) -H * #He #HLK1 [ destruct - elim (IHL12 L1 0) -IHL12 // #X #HL12 #H - <(ldrop_inv_O2 … H) in HL12; -H /3 width=3/ - | elim (IHL12 … HLK1) -L1 /3 width=3/ + elim (IHL12 L1 s 0) -IHL12 // #X #HL12 #H + <(ldrop_inv_O2 … H) in HL12; -H /3 width=3 by lsubsv_pair, ldrop_pair, ex2_intro/ + | elim (IHL12 … HLK1) -L1 /3 width=3 by ldrop_drop_lt, ex2_intro/ ] -| #L1 #L2 #W #V #l #H1W #HV #HVW #H2W #H1l #H2l #_ #IHL12 #K1 #e #H +| #L1 #L2 #W #V #l #H1W #HV #HVW #H2W #H1l #H2l #_ #IHL12 #K1 #s #e #H elim (ldrop_inv_O1_pair1 … H) -H * #He #HLK1 [ destruct - elim (IHL12 L1 0) -IHL12 // #X #HL12 #H - <(ldrop_inv_O2 … H) in HL12; -H /3 width=4/ - | elim (IHL12 … HLK1) -L1 /3 width=3/ + elim (IHL12 L1 s 0) -IHL12 // #X #HL12 #H + <(ldrop_inv_O2 … H) in HL12; -H /3 width=4 by lsubsv_abbr, ldrop_pair, ex2_intro/ + | elim (IHL12 … HLK1) -L1 /3 width=3 by ldrop_drop_lt, ex2_intro/ ] ] qed-. (* Note: the constant 0 cannot be generalized *) lemma lsubsv_ldrop_O1_trans: ∀h,g,G,L1,L2. G ⊢ L1 ¡⊑[h, g] L2 → - ∀K2,e. ⇩[0, e] L2 ≡ K2 → - ∃∃K1. G ⊢ K1 ¡⊑[h, g] K2 & ⇩[0, e] L1 ≡ K1. + ∀K2,s, e. ⇩[s, 0, e] L2 ≡ K2 → + ∃∃K1. G ⊢ K1 ¡⊑[h, g] K2 & ⇩[s, 0, e] L1 ≡ K1. #h #g #G #L1 #L2 #H elim H -L1 -L2 -[ /2 width=3/ -| #I #L1 #L2 #V #_ #IHL12 #K2 #e #H +[ /2 width=3 by ex2_intro/ +| #I #L1 #L2 #V #_ #IHL12 #K2 #s #e #H elim (ldrop_inv_O1_pair1 … H) -H * #He #HLK2 [ destruct - elim (IHL12 L2 0) -IHL12 // #X #HL12 #H - <(ldrop_inv_O2 … H) in HL12; -H /3 width=3/ - | elim (IHL12 … HLK2) -L2 /3 width=3/ + elim (IHL12 L2 s 0) -IHL12 // #X #HL12 #H + <(ldrop_inv_O2 … H) in HL12; -H /3 width=3 by lsubsv_pair, ldrop_pair, ex2_intro/ + | elim (IHL12 … HLK2) -L2 /3 width=3 by ldrop_drop_lt, ex2_intro/ ] -| #L1 #L2 #W #V #l #H1W #HV #HVW #H2W #H1l #H2l #_ #IHL12 #K2 #e #H +| #L1 #L2 #W #V #l #H1W #HV #HVW #H2W #H1l #H2l #_ #IHL12 #K2 #s #e #H elim (ldrop_inv_O1_pair1 … H) -H * #He #HLK2 [ destruct - elim (IHL12 L2 0) -IHL12 // #X #HL12 #H - <(ldrop_inv_O2 … H) in HL12; -H /3 width=4/ - | elim (IHL12 … HLK2) -L2 /3 width=3/ + elim (IHL12 L2 s 0) -IHL12 // #X #HL12 #H + <(ldrop_inv_O2 … H) in HL12; -H /3 width=4 by lsubsv_abbr, ldrop_pair, ex2_intro/ + | elim (IHL12 … HLK2) -L2 /3 width=3 by ldrop_drop_lt, ex2_intro/ ] ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsstas.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsstas.ma index 8283ea541..f975e0fbd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsstas.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsstas.ma @@ -27,7 +27,7 @@ lemma lsubsv_lsstas_trans: ∀h,g,G,L2,T,U2,l1. ⦃G, L2⦄ ⊢ T •*[h, g, l1] ∀L1. G ⊢ L1 ¡⊑[h, g] L2 → ∃∃U1. ⦃G, L1⦄ ⊢ T •*[h, g, l1] U1 & ⦃G, L1⦄ ⊢ U1 ⬌* U2. #h #g #G #L2 #T #U #l1 #H @(lsstas_ind_alt … H) -G -L2 -T -U -l1 -[1,2: /2 width=3/ +[1,2: /2 width=3 by lstar_O, ex2_intro/ | #G #L2 #K2 #X #Y #U #i #l1 #HLK2 #_ #HYU #IHXY #l2 #Hl12 #Hl2 #L1 #HL12 elim (da_inv_lref … Hl2) -Hl2 * #K0 #V0 [| #l0 ] #HK0 #HV0 lapply (ldrop_mono … HK0 … HLK2) -HK0 #H destruct @@ -37,7 +37,7 @@ lemma lsubsv_lsstas_trans: ∀h,g,G,L2,T,U2,l1. ⦃G, L2⦄ ⊢ T •*[h, g, l1] elim (IHXY … Hl12 HV0 … HK12) -K2 -l2 #T #HXT #HTY lapply (ldrop_fwd_drop2 … HLK1) #H elim (lift_total T 0 (i+1)) - /3 width=11 by lsstas_ldef, cpcs_lift, ex2_intro/ + /3 width=12 by lsstas_ldef, cpcs_lift, ex2_intro/ | #V #l0 #_ #_ #_ #_ #_ #_ #_ #H destruct ] | #G #L2 #K2 #X #Y #U #i #l1 #l #HLK2 #_ #_ #HYU #IHXY #l2 #Hl12 #Hl2 #L1 #HL12 -l @@ -52,7 +52,7 @@ lemma lsubsv_lsstas_trans: ∀h,g,G,L2,T,U2,l1. ⦃G, L2⦄ ⊢ T •*[h, g, l1] elim (IHXY … Hl12 HV0 … HK12) -K2 -Hl12 #Y0 lapply (ldrop_fwd_drop2 … HLK1) elim (lift_total Y0 0 (i+1)) - /3 width=11 by lsstas_ldec, cpcs_lift, ex2_intro/ + /3 width=12 by lsstas_ldec, cpcs_lift, ex2_intro/ | #V #l #_ #_ #HVX #_ #HV #HX #HK12 #_ #H destruct lapply (da_mono … HX … HV0) -HX #H destruct elim (IHXY … Hl12 HV0 … HK12) -K2 #Y0 #HXY0 #HY0 @@ -62,7 +62,7 @@ lemma lsubsv_lsstas_trans: ∀h,g,G,L2,T,U2,l1. ⦃G, L2⦄ ⊢ T •*[h, g, l1] lapply (cpcs_trans … HWY0 … HY0) -Y0 lapply (ldrop_fwd_drop2 … HLK1) elim (lift_total W 0 (i+1)) - /4 width=11 by lsstas_ldef, lsstas_cast, cpcs_lift, ex2_intro/ + /4 width=12 by lsstas_ldef, lsstas_cast, cpcs_lift, ex2_intro/ ] | #a #I #G #L2 #V2 #T2 #U2 #l1 #_ #IHTU2 #l2 #Hl12 #Hl2 #L1 #HL12 lapply (da_inv_bind … Hl2) -Hl2 #Hl2 diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma index a85645f07..7bdef30fa 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma @@ -25,7 +25,7 @@ definition scast: ∀h. sd h → nat → relation4 genv lenv term term ≝ (* activate genv *) inductive snv (h:sh) (g:sd h): relation3 genv lenv term ≝ | snv_sort: ∀G,L,k. snv h g G L (⋆k) -| snv_lref: ∀I,G,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → snv h g G K V → snv h g G L (#i) +| snv_lref: ∀I,G,L,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V → snv h g G K V → snv h g G L (#i) | snv_bind: ∀a,I,G,L,V,T. snv h g G L V → snv h g G (L.ⓑ{I}V) T → snv h g G L (ⓑ{a,I}V.T) | snv_appl: ∀a,G,L,V,W,W0,T,U,l. snv h g G L V → snv h g G L T → ⦃G, L⦄ ⊢ V ▪[h, g] l+1 → ⦃G, L⦄ ⊢ V •[h, g] W → ⦃G, L⦄ ⊢ W ➡* W0 → @@ -40,10 +40,10 @@ interpretation "stratified native validity (term)" (* Basic inversion lemmas ***************************************************) fact snv_inv_lref_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀i. X = #i → - ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ¡[h, g]. + ∃∃I,K,V. ⇩[i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ¡[h, g]. #h #g #G #L #X * -G -L -X [ #G #L #k #i #H destruct -| #I #G #L #K #V #i0 #HLK #HV #i #H destruct /2 width=5/ +| #I #G #L #K #V #i0 #HLK #HV #i #H destruct /2 width=5 by ex2_3_intro/ | #a #I #G #L #V #T #_ #_ #i #H destruct | #a #G #L #V #W #W0 #T #U #l #_ #_ #_ #_ #_ #_ #i #H destruct | #G #L #W #T #U #l #_ #_ #_ #_ #_ #i #H destruct @@ -51,7 +51,7 @@ fact snv_inv_lref_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀i. X = #i qed-. lemma snv_inv_lref: ∀h,g,G,L,i. ⦃G, L⦄ ⊢ #i ¡[h, g] → - ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ¡[h, g]. + ∃∃I,K,V. ⇩[i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ¡[h, g]. /2 width=3 by snv_inv_lref_aux/ qed-. fact snv_inv_gref_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀p. X = §p → ⊥. @@ -72,7 +72,7 @@ fact snv_inv_bind_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀a,I,V,T. X #h #g #G #L #X * -G -L -X [ #G #L #k #a #I #V #T #H destruct | #I0 #G #L #K #V0 #i #_ #_ #a #I #V #T #H destruct -| #b #I0 #G #L #V0 #T0 #HV0 #HT0 #a #I #V #T #H destruct /2 width=1/ +| #b #I0 #G #L #V0 #T0 #HV0 #HT0 #a #I #V #T #H destruct /2 width=1 by conj/ | #b #G #L #V0 #W0 #W00 #T0 #U0 #l #_ #_ #_ #_#_ #_ #a #I #V #T #H destruct | #G #L #W0 #T0 #U0 #l #_ #_ #_ #_ #_ #a #I #V #T #H destruct ] @@ -90,7 +90,7 @@ fact snv_inv_appl_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀V,T. X = [ #G #L #k #V #T #H destruct | #I #G #L #K #V0 #i #_ #_ #V #T #H destruct | #a #I #G #L #V0 #T0 #_ #_ #V #T #H destruct -| #a #G #L #V0 #W0 #W00 #T0 #U0 #l #HV0 #HT0 #Hl #HVW0 #HW00 #HTU0 #V #T #H destruct /2 width=8/ +| #a #G #L #V0 #W0 #W00 #T0 #U0 #l #HV0 #HT0 #Hl #HVW0 #HW00 #HTU0 #V #T #H destruct /2 width=8 by ex6_5_intro/ | #G #L #W0 #T0 #U0 #l #_ #_ #_ #_ #_ #V #T #H destruct ] qed-. @@ -109,7 +109,7 @@ fact snv_inv_cast_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀W,T. X = | #I #G #L #K #V #i #_ #_ #W #T #H destruct | #a #I #G #L #V #T0 #_ #_ #W #T #H destruct | #a #G #L #V #W0 #W00 #T0 #U #l #_ #_ #_ #_ #_ #_ #W #T #H destruct -| #G #L #W0 #T0 #U0 #l #HW0 #HT0 #Hl #HTU0 #HUW0 #W #T #H destruct /2 width=4/ +| #G #L #W0 #T0 #U0 #l #HW0 #HT0 #Hl #HTU0 #HUW0 #W #T #H destruct /2 width=4 by ex5_2_intro/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma index f86f5bd15..5adc067d5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma @@ -29,7 +29,7 @@ fact da_cpr_lpr_aux: ∀h,g,G0,L0,T0. #h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ] [ #k #_ #_ #_ #_ #l #H2 #X3 #H3 #L2 #_ -IH3 -IH2 -IH1 lapply (da_inv_sort … H2) -H2 - lapply (cpr_inv_sort1 … H3) -H3 #H destruct /2 width=1/ + lapply (cpr_inv_sort1 … H3) -H3 #H destruct /2 width=1 by da_sort/ | #i #HG0 #HL0 #HT0 #H1 #l #H2 #X3 #H3 #L2 #HL12 destruct -IH3 -IH2 elim (snv_inv_lref … H1) -H1 #I0 #K0 #X0 #H #HX0 elim (da_inv_lref … H2) -H2 * #K1 [ #V1 | #W1 #l1 ] #HLK1 [ #HV1 | #HW1 #H ] destruct @@ -46,7 +46,7 @@ fact da_cpr_lpr_aux: ∀h,g,G0,L0,T0. elim (lpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2 elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #_ #H destruct lapply (ldrop_fwd_drop2 … HLK2) -V2 - /4 width=7 by da_lift, fqup_fpbg/ + /4 width=8 by da_lift, fqup_fpbg/ ] | #p #_ #_ #HT0 #H1 destruct -IH3 -IH2 -IH1 elim (snv_inv_gref … H1) diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma index bb7ac6ca5..b86534984 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma @@ -20,63 +20,67 @@ include "basic_2/dynamic/snv.ma". (* Relocation properties ****************************************************) -lemma snv_lift: ∀h,g,G,K,T. ⦃G, K⦄ ⊢ T ¡[h, g] → ∀L,d,e. ⇩[d, e] L ≡ K → +lemma snv_lift: ∀h,g,G,K,T. ⦃G, K⦄ ⊢ T ¡[h, g] → ∀L,s,d,e. ⇩[s, d, e] L ≡ K → ∀U. ⇧[d, e] T ≡ U → ⦃G, L⦄ ⊢ U ¡[h, g]. #h #g #G #K #T #H elim H -G -K -T -[ #G #K #k #L #d #e #_ #X #H +[ #G #K #k #L #s #d #e #_ #X #H >(lift_inv_sort1 … H) -X -K -d -e // -| #I #G #K #K0 #V #i #HK0 #_ #IHV #L #d #e #HLK #X #H +| #I #G #K #K0 #V #i #HK0 #_ #IHV #L #s #d #e #HLK #X #H elim (lift_inv_lref1 … H) * #Hid #H destruct - [ elim (ldrop_trans_le … HLK … HK0) -K /2 width=2/ #X #HL0 #H - elim (ldrop_inv_skip2 … H) -H /2 width=1/ -Hid #L0 #W #HLK0 #HVW #H destruct - /3 width=8/ - | lapply (ldrop_trans_ge … HLK … HK0 ?) -K // -Hid /3 width=8/ + [ elim (ldrop_trans_le … HLK … HK0) -K /2 width=2 by lt_to_le/ #X #HL0 #H + elim (ldrop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hid #L0 #W #HLK0 #HVW #H destruct + /3 width=9 by snv_lref/ + | lapply (ldrop_trans_ge … HLK … HK0 ?) -K + /3 width=9 by snv_lref, ldrop_inv_gen/ ] -| #a #I #G #K #V #T #_ #_ #IHV #IHT #L #d #e #HLK #X #H +| #a #I #G #K #V #T #_ #_ #IHV #IHT #L #s #d #e #HLK #X #H elim (lift_inv_bind1 … H) -H #W #U #HVW #HTU #H destruct - /4 width=4/ -| #a #G #K #V #V0 #V1 #T #T1 #l #_ #_ #Hl #HV0 #HV01 #HT1 #IHV #IHT #L #d #e #HLK #X #H + /4 width=5 by snv_bind, ldrop_skip/ +| #a #G #K #V #V0 #V1 #T #T1 #l #_ #_ #Hl #HV0 #HV01 #HT1 #IHV #IHT #L #s #d #e #HLK #X #H elim (lift_inv_flat1 … H) -H #W #U #HVW #HTU #H destruct elim (lift_total V0 d e) #W0 #HVW0 elim (lift_total V1 d e) #W1 #HVW1 elim (lift_total T1 (d+1) e) #U1 #HTU1 @(snv_appl … a … W0 … W1 … U1 l) - [1,2: /2 width=4/ | /2 width=7/ |4,5: /2 width=9/ ] - @(cpds_lift … HT1 … HLK … HTU) /2 width=1/ -| #G #K #V0 #T #V #l #_ #_ #Hl #HTV #HV0 #IHV0 #IHT #L #d #e #HLK #X #H + [1,2,3,4,5: /2 width=10 by cprs_lift, ssta_lift, da_lift/ ] + @(cpds_lift … HT1 … HLK … HTU) /2 width=1 by lift_bind/ (**) (* full auto raises typecjhecker failure *) +| #G #K #V0 #T #V #l #_ #_ #Hl #HTV #HV0 #IHV0 #IHT #L #s #d #e #HLK #X #H elim (lift_inv_flat1 … H) -H #W0 #U #HVW0 #HTU #H destruct - elim (lift_total V d e) #W #HVW - @(snv_cast … W l) [1,2: /2 width=4/ | /2 width=7/ |4,5: /2 width=9/ ] + elim (lift_total V d e) + /3 width=12 by snv_cast, cpcs_lift, ssta_lift, da_lift/ ] qed. -lemma snv_inv_lift: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ U ¡[h, g] → ∀K,d,e. ⇩[d, e] L ≡ K → +lemma snv_inv_lift: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ U ¡[h, g] → ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T. ⇧[d, e] T ≡ U → ⦃G, K⦄ ⊢ T ¡[h, g]. #h #g #G #L #U #H elim H -G -L -U -[ #G #L #k #K #d #e #_ #X #H +[ #G #L #k #K #s #d #e #_ #X #H >(lift_inv_sort2 … H) -X -L -d -e // -| #I #G #L #L0 #W #i #HL0 #_ #IHW #K #d #e #HLK #X #H +| #I #G #L #L0 #W #i #HL0 #_ #IHW #K #s #d #e #HLK #X #H elim (lift_inv_lref2 … H) * #Hid #H destruct - [ elim (ldrop_conf_le … HLK … HL0) -L /2 width=2/ #X #HK0 #H - elim (ldrop_inv_skip1 … H) -H /2 width=1/ -Hid #K0 #V #HLK0 #HVW #H destruct - /3 width=8/ - | lapply (ldrop_conf_ge … HLK … HL0 ?) -L // -Hid /3 width=8/ + [ elim (ldrop_conf_le … HLK … HL0) -L /2 width=2 by lt_to_le/ #X #HK0 #H + elim (ldrop_inv_skip1 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hid #K0 #V #HLK0 #HVW #H destruct + /3 width=12 by snv_lref/ + | lapply (ldrop_conf_ge … HLK … HL0 ?) -L /3 width=9 by snv_lref/ ] -| #a #I #G #L #W #U #_ #_ #IHW #IHU #K #d #e #HLK #X #H - elim (lift_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct /4 width=4/ -| #a #G #L #W #W0 #W1 #U #U1 #l #_ #_ #Hl #HW0 #HW01 #HU1 #IHW #IHU #K #d #e #HLK #X #H +| #a #I #G #L #W #U #_ #_ #IHW #IHU #K #s #d #e #HLK #X #H + elim (lift_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct + /4 width=5 by snv_bind, ldrop_skip/ +| #a #G #L #W #W0 #W1 #U #U1 #l #_ #_ #Hl #HW0 #HW01 #HU1 #IHW #IHU #K #s #d #e #HLK #X #H elim (lift_inv_flat2 … H) -H #V #T #HVW #HTU #H destruct lapply (da_inv_lift … Hl … HLK … HVW) -Hl #Hl elim (ssta_inv_lift1 … HW0 … HLK … HVW) -HW0 #V0 #HVW0 #HV0 elim (cprs_inv_lift1 … HW01 … HLK … HVW0) -W0 #V1 #HVW1 #HV01 elim (cpds_inv_lift1 … HU1 … HLK … HTU) -HU1 #X #H #HTU elim (lift_inv_bind2 … H) -H #Y #T1 #HY #HTU1 #H destruct - lapply (lift_inj … HY … HVW1) -HY #H destruct /3 width=8/ -| #G #L #W0 #U #W #l #_ #_ #Hl #HUW #HW0 #IHW0 #IHU #K #d #e #HLK #X #H + lapply (lift_inj … HY … HVW1) -HY #H destruct + /3 width=8 by snv_appl/ +| #G #L #W0 #U #W #l #_ #_ #Hl #HUW #HW0 #IHW0 #IHU #K #s #d #e #HLK #X #H elim (lift_inv_flat2 … H) -H #V0 #T #HVW0 #HTU #H destruct lapply (da_inv_lift … Hl … HLK … HTU) -Hl #Hl elim (ssta_inv_lift1 … HUW … HLK … HTU) -HUW #V #HVW #HTV - lapply (cpcs_inv_lift G … HLK … HVW … HVW0 ?) // -W /3 width=4/ + lapply (cpcs_inv_lift G … HLK … HVW … HVW0 ?) // -W + /3 width=8 by snv_cast/ ] qed-. @@ -89,7 +93,7 @@ lemma snv_fqu_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2 elim (snv_inv_lref … H) -H #I2 #L2 #V2 #H #HV2 lapply (ldrop_inv_O2 … H) -H #H destruct // |2: * -|5,6: /3 width=7 by snv_inv_lift/ +|5,6: /3 width=8 by snv_inv_lift/ ] [1,3: #a #I #G1 #L1 #V1 #T1 #H elim (snv_inv_bind … H) -H // |2,4: * #G1 #L1 #V1 #T1 #H diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma index 75bf56d43..367312794 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma @@ -38,7 +38,7 @@ fact snv_cpr_lpr_aux: ∀h,g,G0,L0,T0. [ #H destruct -HLK1 /4 width=10 by fqup_fpbg, snv_lref/ | * #K0 #V0 #W0 #H #HVW0 #W0 -HV12 lapply (ldrop_mono … H … HLK1) -HLK1 -H #H destruct - lapply (ldrop_fwd_drop2 … HLK2) -HLK2 /4 width=7 by fqup_fpbg, snv_lift/ + lapply (ldrop_fwd_drop2 … HLK2) -HLK2 /4 width=8 by fqup_fpbg, snv_lift/ ] | #p #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2 -IH1 elim (snv_inv_gref … H1) @@ -103,13 +103,13 @@ fact snv_cpr_lpr_aux: ∀h,g,G0,L0,T0. elim (ssta_cpr_lpr_aux … IH3 … HVW1 … HV10 … HL12) /2 width=2 by fqup_fpbg/ -IH3 -HVW1 #X #H1 #H2 lapply (cpcs_canc_sn … H2 HW10) -W10 #H2 elim (lift_total X 0 1) #W20 #H3 - lapply (ssta_lift … H1 (L2.ⓓW2) … HV02 … H3) /2 width=1 by ldrop_drop/ -H1 #HVW20 - lapply (cpcs_lift … (L2.ⓓW2) … H3 … HW13 H2) /2 width=1 by ldrop_drop/ -HW13 -H3 -H2 #HW320 + lapply (ssta_lift … H1 (L2.ⓓW2) … HV02 … H3) /2 width=2 by ldrop_drop/ -H1 #HVW20 + lapply (cpcs_lift … (L2.ⓓW2) … H3 … HW13 H2) /2 width=2 by ldrop_drop/ -HW13 -H3 -H2 #HW320 lapply (cpcs_cprs_strap1 … HW320 … HW1) -W3 #HW20 elim (cpcs_inv_cprs … HW20) -HW20 #W3 #HW203 #HW3 lapply (cpds_cprs_trans … (ⓛ{a}W3.U2) HTU2 ?) /2 width=1 by cprs_bind/ -HW3 -HTU2 #HTU2 lapply (IH2 … Hl0 … HV10 … HL12) /2 width=1 by fqup_fpbg/ -IH2 -Hl0 #Hl0 - lapply (da_lift … Hl0 (L2.ⓓW2) … HV02) /2 width=1 by ldrop_drop/ -Hl0 #Hl0 + lapply (da_lift … Hl0 (L2.ⓓW2) … HV02) /2 width=2 by ldrop_drop/ -Hl0 #Hl0 lapply (IH1 … HW02 … HL12) /2 width=1 by fqup_fpbg/ -HW0 #HW2 lapply (IH1 … HV10 … HL12) /2 width=1 by fqup_fpbg/ -HV1 -HV10 #HV0 lapply (IH1 … HT02 (L2.ⓓW2) ?) /2 width=1 by fqup_fpbg, lpr_pair/ -L1 #HT2 diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma index a7b6e3e77..9213b4d57 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma @@ -52,13 +52,13 @@ fact lsstas_cpr_lpr_aux: ∀h,g,G0,L0,T0. ] [ elim (IH1 … HWl1 … HW0 … HW12 … HK12) -IH1 -HW0 /2 width=1 by fqup_fpbg/ #V2 #HWV2 #HV2 elim (lift_total V2 0 (i+1)) - /6 width=11 by fqup_fpbg, cpcs_lift, lsstas_ldec, ex2_intro/ + /6 width=12 by fqup_fpbg, cpcs_lift, lsstas_ldec, ex2_intro/ | elim (IH1 … HVl1 … HW0 … HV12 … HK12) -IH1 -HVl1 -HW0 -HV12 -HK12 -IH2 /2 width=1 by fqup_fpbg/ #W2 #HVW2 #HW02 elim (lift_total W2 0 (i+1)) - /4 width=11 by cpcs_lift, lsstas_ldef, ex2_intro/ + /4 width=12 by cpcs_lift, lsstas_ldef, ex2_intro/ | elim (IH1 … HVl1 … HW0 … HVX0 … HK12) -IH1 -HVl1 -HW0 -HVX0 -HK12 -IH2 -V2 /2 width=1 by fqup_fpbg/ -l1 #W2 #HXW2 #HW02 elim (lift_total W2 0 (i+1)) - /3 width=11 by cpcs_lift, lsstas_lift, ex2_intro/ + /3 width=12 by cpcs_lift, lsstas_lift, ex2_intro/ ] | #p #_ #_ #HT0 #H1 destruct -IH4 -IH3 -IH2 -IH1 elim (snv_inv_gref … H1) diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma index e6ef1a9ad..cf1c5d95f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma @@ -25,18 +25,16 @@ lemma cpcs_inv_cprs: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T2 → #G #L #T1 #T2 #H @(cpcs_ind … H) -T2 [ /3 width=3/ | #T #T2 #_ #HT2 * #T0 #HT10 elim HT2 -HT2 #HT2 #HT0 - [ elim (cprs_strip … HT0 … HT2) -T #T #HT0 #HT2 - lapply (cprs_strap1 … HT10 … HT0) -T0 /2 width=3/ - | lapply (cprs_strap2 … HT2 … HT0) -T /2 width=3/ + [ elim (cprs_strip … HT0 … HT2) -T /3 width=3 by cprs_strap1, ex2_intro/ + | /3 width=5 by cprs_strap2, ex2_intro/ ] ] qed-. (* Basic_1: was: pc3_gen_sort *) lemma cpcs_inv_sort: ∀G,L,k1,k2. ⦃G, L⦄ ⊢ ⋆k1 ⬌* ⋆k2 → k1 = k2. -#G #L #k1 #k2 #H -elim (cpcs_inv_cprs … H) -H #T #H1 ->(cprs_inv_sort1 … H1) -T #H2 +#G #L #k1 #k2 #H elim (cpcs_inv_cprs … H) -H +#T #H1 >(cprs_inv_sort1 … H1) -T #H2 lapply (cprs_inv_sort1 … H2) -L #H destruct // qed-. @@ -45,7 +43,7 @@ lemma cpcs_inv_abst1: ∀a,G,L,W1,T1,T. ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ⬌* T → #a #G #L #W1 #T1 #T #H elim (cpcs_inv_cprs … H) -H #X #H1 #H2 elim (cprs_inv_abst1 … H1) -H1 #W2 #T2 #HW12 #HT12 #H destruct -@(ex2_2_intro … H2) -H2 /2 width=2/ (**) (* explicit constructor, /3 width=6/ is slow *) +/3 width=6 by cprs_bind, ex2_2_intro/ qed-. lemma cpcs_inv_abst2: ∀a,G,L,W1,T1,T. ⦃G, L⦄ ⊢ T ⬌* ⓛ{a}W1.T1 → @@ -61,53 +59,49 @@ elim (cprs_inv_abst1 … H2) -H2 #W0 #T0 #_ #_ #H destruct qed-. (* Basic_1: was: pc3_gen_lift *) -lemma cpcs_inv_lift: ∀G,L,K,d,e. ⇩[d, e] L ≡ K → +lemma cpcs_inv_lift: ∀G,L,K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀T2,U2. ⇧[d, e] T2 ≡ U2 → ⦃G, L⦄ ⊢ U1 ⬌* U2 → ⦃G, K⦄ ⊢ T1 ⬌* T2. -#G #L #K #d #e #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HU12 +#G #L #K #s #d #e #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HU12 elim (cpcs_inv_cprs … HU12) -HU12 #U #HU1 #HU2 elim (cprs_inv_lift1 … HU1 … HLK … HTU1) -U1 #T #HTU #HT1 elim (cprs_inv_lift1 … HU2 … HLK … HTU2) -L -U2 #X #HXU ->(lift_inj … HXU … HTU) -X -U -d -e /2 width=3/ +>(lift_inj … HXU … HTU) -X -U -d -e /2 width=3 by cprs_div/ qed-. (* Advanced properties ******************************************************) lemma lpr_cpcs_trans: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → ∀T1,T2. ⦃G, L2⦄ ⊢ T1 ⬌* T2 → ⦃G, L1⦄ ⊢ T1 ⬌* T2. -#G #L1 #L2 #HL12 #T1 #T2 #H -elim (cpcs_inv_cprs … H) -H #T #HT1 #HT2 -lapply (lpr_cprs_trans … HT1 … HL12) -HT1 -lapply (lpr_cprs_trans … HT2 … HL12) -L2 /2 width=3/ +#G #L1 #L2 #HL12 #T1 #T2 #H elim (cpcs_inv_cprs … H) -H +/4 width=5 by cprs_div, lpr_cprs_trans/ qed-. lemma lprs_cpcs_trans: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → ∀T1,T2. ⦃G, L2⦄ ⊢ T1 ⬌* T2 → ⦃G, L1⦄ ⊢ T1 ⬌* T2. -#G #L1 #L2 #HL12 #T1 #T2 #H -elim (cpcs_inv_cprs … H) -H #T #HT1 #HT2 -lapply (lprs_cprs_trans … HT1 … HL12) -HT1 -lapply (lprs_cprs_trans … HT2 … HL12) -L2 /2 width=3/ +#G #L1 #L2 #HL12 #T1 #T2 #H elim (cpcs_inv_cprs … H) -H +/4 width=5 by cprs_div, lprs_cprs_trans/ qed-. lemma cpr_cprs_conf_cpcs: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T ➡* T1 → ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -#G #L #T #T1 #T2 #HT1 #HT2 -elim (cprs_strip … HT1 … HT2) /2 width=3 by cpr_cprs_div/ +#G #L #T #T1 #T2 #HT1 #HT2 elim (cprs_strip … HT1 … HT2) -HT1 -HT2 +/2 width=3 by cpr_cprs_div/ qed-. lemma cprs_cpr_conf_cpcs: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T ➡* T1 → ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T2 ⬌* T1. -#G #L #T #T1 #T2 #HT1 #HT2 -elim (cprs_strip … HT1 … HT2) /2 width=3 by cprs_cpr_div/ +#G #L #T #T1 #T2 #HT1 #HT2 elim (cprs_strip … HT1 … HT2) -HT1 -HT2 +/2 width=3 by cprs_cpr_div/ qed-. lemma cprs_conf_cpcs: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T ➡* T1 → ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -#G #L #T #T1 #T2 #HT1 #HT2 -elim (cprs_conf … HT1 … HT2) /2 width=3/ +#G #L #T #T1 #T2 #HT1 #HT2 elim (cprs_conf … HT1 … HT2) -HT1 -HT2 +/2 width=3 by cprs_div/ qed-. lemma lprs_cprs_conf: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ⦃G, L2⦄ ⊢ T1 ⬌* T2. -#G #L1 #L2 #HL12 #T1 #T2 #HT12 -elim (lprs_cprs_conf_dx … HT12 … HL12) -L1 /2 width=3/ +#G #L1 #L2 #HL12 #T1 #T2 #HT12 elim (lprs_cprs_conf_dx … HT12 … HL12) -L1 +/2 width=3 by cprs_div/ qed-. (* Basic_1: was: pc3_wcpr0_t *) @@ -125,42 +119,40 @@ lemma lpr_cpr_conf: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → (* Basic_1: was only: pc3_thin_dx *) lemma cpcs_flat: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬌* V2 → ∀T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T2 → ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬌* ⓕ{I}V2.T2. -#G #L #V1 #V2 #HV12 #T1 #T2 #HT12 #I -elim (cpcs_inv_cprs … HV12) -HV12 #V #HV1 #HV2 -elim (cpcs_inv_cprs … HT12) -HT12 /3 width=5 by cprs_flat, cprs_div/ (**) (* /3 width=5/ is too slow *) +#G #L #V1 #V2 #HV12 #T1 #T2 #HT12 +elim (cpcs_inv_cprs … HV12) -HV12 +elim (cpcs_inv_cprs … HT12) -HT12 +/3 width=5 by cprs_flat, cprs_div/ qed. lemma cpcs_flat_dx_cpr_rev: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V2 ➡ V1 → ∀T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T2 → ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬌* ⓕ{I}V2.T2. -/3 width=1/ qed. +/3 width=1 by cpr_cpcs_sn, cpcs_flat/ qed. lemma cpcs_bind_dx: ∀a,I,G,L,V,T1,T2. ⦃G, L.ⓑ{I}V⦄ ⊢ T1 ⬌* T2 → ⦃G, L⦄ ⊢ ⓑ{a,I}V.T1 ⬌* ⓑ{a,I}V.T2. -#a #I #G #L #V #T1 #T2 #HT12 -elim (cpcs_inv_cprs … HT12) -HT12 /3 width=5 by cprs_div, cprs_bind/ (**) (* /3 width=5/ is a bit slow *) +#a #I #G #L #V #T1 #T2 #HT12 elim (cpcs_inv_cprs … HT12) -HT12 +/3 width=5 by cprs_div, cprs_bind/ qed. lemma cpcs_bind_sn: ∀a,I,G,L,V1,V2,T. ⦃G, L⦄ ⊢ V1 ⬌* V2 → ⦃G, L⦄ ⊢ ⓑ{a,I}V1. T ⬌* ⓑ{a,I}V2. T. -#a #I #G #L #V1 #V2 #T #HV12 -elim (cpcs_inv_cprs … HV12) -HV12 /3 width=5 by cprs_div, cprs_bind/ (**) (* /3 width=5/ is a bit slow *) +#a #I #G #L #V1 #V2 #T #HV12 elim (cpcs_inv_cprs … HV12) -HV12 +/3 width=5 by cprs_div, cprs_bind/ qed. lemma lsubr_cpcs_trans: ∀G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ⬌* T2 → ∀L2. L2 ⊑ L1 → ⦃G, L2⦄ ⊢ T1 ⬌* T2. -#G #L1 #T1 #T2 #HT12 -elim (cpcs_inv_cprs … HT12) -HT12 -/3 width=5 by cprs_div, lsubr_cprs_trans/ (**) (* /3 width=5/ is a bit slow *) +#G #L1 #T1 #T2 #HT12 elim (cpcs_inv_cprs … HT12) -HT12 +/3 width=5 by cprs_div, lsubr_cprs_trans/ qed-. (* Basic_1: was: pc3_lift *) -lemma cpcs_lift: ∀G,L,K,d,e. ⇩[d, e] L ≡ K → +lemma cpcs_lift: ∀G,L,K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀T2,U2. ⇧[d, e] T2 ≡ U2 → ⦃G, K⦄ ⊢ T1 ⬌* T2 → ⦃G, L⦄ ⊢ U1 ⬌* U2. -#G #L #K #d #e #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HT12 +#G #L #K #s #d #e #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HT12 elim (cpcs_inv_cprs … HT12) -HT12 #T #HT1 #HT2 -elim (lift_total T d e) #U #HTU -lapply (cprs_lift … HT1 … HLK … HTU1 … HTU) -T1 #HU1 -lapply (cprs_lift … HT2 … HLK … HTU2 … HTU) -K -T2 -T -d -e /2 width=3/ +elim (lift_total T d e) /3 width=12 by cprs_div, cprs_lift/ qed. lemma cpcs_strip: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T ⬌* T1 → ∀T2. ⦃G, L⦄ ⊢ T ⬌ T2 → @@ -175,16 +167,15 @@ lemma cpcs_inv_abst_sn: ∀a1,a2,G,L,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{a1}W1.T1 elim (cpcs_inv_cprs … H) -H #T #H1 #H2 elim (cprs_inv_abst1 … H1) -H1 #W0 #T0 #HW10 #HT10 #H destruct elim (cprs_inv_abst1 … H2) -H2 #W #T #HW2 #HT2 #H destruct -lapply (lprs_cprs_conf … (L.ⓛW) … HT2) /2 width=1/ -HT2 #HT2 -lapply (lprs_cpcs_trans … (L.ⓛW1) … HT2) /2 width=1/ -HT2 #HT2 +lapply (lprs_cprs_conf … (L.ⓛW) … HT2) /2 width=1 by lprs_pair/ -HT2 #HT2 +lapply (lprs_cpcs_trans … (L.ⓛW1) … HT2) /2 width=1 by lprs_pair/ -HT2 #HT2 /4 width=3 by and3_intro, cprs_div, cpcs_cprs_div, cpcs_sym/ qed-. lemma cpcs_inv_abst_dx: ∀a1,a2,G,L,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{a1}W1.T1 ⬌* ⓛ{a2}W2.T2 → ∧∧ ⦃G, L⦄ ⊢ W1 ⬌* W2 & ⦃G, L.ⓛW2⦄ ⊢ T1 ⬌* T2 & a1 = a2. -#a1 #a2 #G #L #W1 #W2 #T1 #T2 #HT12 -lapply (cpcs_sym … HT12) -HT12 #HT12 -elim (cpcs_inv_abst_sn … HT12) -HT12 /3 width=1/ +#a1 #a2 #G #L #W1 #W2 #T1 #T2 #HT12 lapply (cpcs_sym … HT12) -HT12 +#HT12 elim (cpcs_inv_abst_sn … HT12) -HT12 /3 width=1 by cpcs_sym, and3_intro/ qed-. (* Main properties **********************************************************) @@ -194,28 +185,24 @@ theorem cpcs_trans: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌* T → ∀T2. ⦃G, L⦄ #G #L #T1 #T #HT1 #T2 @(trans_TC … HT1) qed-. theorem cpcs_canc_sn: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T ⬌* T1 → ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -/3 width=3 by cpcs_trans, cpcs_sym/ qed-. (**) (* /3 width=3/ is too slow *) +/3 width=3 by cpcs_trans, cpcs_sym/ qed-. theorem cpcs_canc_dx: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T → ⦃G, L⦄ ⊢ T2 ⬌* T → ⦃G, L⦄ ⊢ T1 ⬌* T2. -/3 width=3 by cpcs_trans, cpcs_sym/ qed-. (**) (* /3 width=3/ is too slow *) +/3 width=3 by cpcs_trans, cpcs_sym/ qed-. lemma cpcs_bind1: ∀a,I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬌* V2 → ∀T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬌* T2 → ⦃G, L⦄ ⊢ ⓑ{a,I}V1. T1 ⬌* ⓑ{a,I}V2. T2. -#a #I #G #L #V1 #V2 #HV12 #T1 #T2 #HT12 -@(cpcs_trans … (ⓑ{a,I}V1.T2)) /2 width=1/ -qed. +/3 width=3 by cpcs_trans, cpcs_bind_sn, cpcs_bind_dx/ qed. lemma cpcs_bind2: ∀a,I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬌* V2 → ∀T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ⬌* T2 → ⦃G, L⦄ ⊢ ⓑ{a,I}V1. T1 ⬌* ⓑ{a,I}V2. T2. -#a #I #G #L #V1 #V2 #HV12 #T1 #T2 #HT12 -@(cpcs_trans … (ⓑ{a,I}V2.T1)) /2 width=1/ -qed. +/3 width=3 by cpcs_trans, cpcs_bind_sn, cpcs_bind_dx/ qed. (* Basic_1: was: pc3_wcpr0 *) lemma lpr_cpcs_conf: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ⬌* T2 → ⦃G, L2⦄ ⊢ T1 ⬌* T2. -#G #L1 #L2 #HL12 #T1 #T2 #H -elim (cpcs_inv_cprs … H) -H /3 width=5 by cpcs_canc_dx, lpr_cprs_conf/ +#G #L1 #L2 #HL12 #T1 #T2 #H elim (cpcs_inv_cprs … H) -H +/3 width=5 by cpcs_canc_dx, lpr_cprs_conf/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrop.ma index 958052e5b..302829e62 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrop.ma @@ -24,12 +24,13 @@ lemma ldrops_ldrop_trans: ∀L1,L,des. ⇩*[Ⓕ, des] L1 ≡ L → ∀L2,i. ⇩[ @⦃i, des⦄ ≡ i0 & des ▭ i ≡ des0. #L1 #L #des #H elim H -L1 -L -des [ /2 width=7 by ldrops_nil, minuss_nil, at_nil, ex4_3_intro/ -| #L1 #L3 #L #des3 #d #e #_ #HL3 #IHL13 #L2 #i #HL2 +| #L1 #L0 #L #des #d #e #_ #HL0 #IHL0 #L2 #i #HL2 elim (lt_or_ge i d) #Hid - [ elim (ldrop_trans_le … HL3 … HL2) -L /2 width=2 by lt_to_le/ - #L #HL3 #HL2 elim (IHL13 … HL3) -L3 /3 width=7 by ldrops_cons, minuss_lt, at_lt, ex4_3_intro/ - | lapply (ldrop_trans_ge … HL3 … HL2 ?) -L // #HL32 - elim (IHL13 … HL32) -L3 /3 width=7 by minuss_ge, at_ge, ex4_3_intro/ + [ elim (ldrop_trans_le … HL0 … HL2) -L /2 width=2 by lt_to_le/ + #L #HL0 #HL2 elim (IHL0 … HL0) -L0 /3 width=7 by ldrops_cons, minuss_lt, at_lt, ex4_3_intro/ + | lapply (ldrop_trans_ge … HL0 … HL2 ?) -L // #HL02 + elim (IHL0 … HL02) -L0 /3 width=7 by minuss_ge, at_ge, ex4_3_intro/ ] ] qed-. + diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml index 21d828012..06a65ff53 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml @@ -33,6 +33,11 @@ Closure of context-sensitive extended computation for native validity. + + Parametrized slicing for local environments + comprises both versions of this operation + (one from basic_1, the other used in basic_2 till now). + Passive support for global environments. -- 2.39.2