From: Ferruccio Guidi Date: Fri, 17 Jan 2014 17:45:00 +0000 (+0000) Subject: - commit of the "substitution" component X-Git-Tag: make_still_working~997 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e5378812c068074f0ac627541d3f066e135c8824;p=helm.git - commit of the "substitution" component - some renaming - we disabled the old notation for ldrop to capture its instances syntactically --- 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 3656d36f6..23cc43031 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma @@ -36,7 +36,7 @@ theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP. | #I #G #L1 #K1 #V1 #B #i #HLK1 #HKV1B #IHB #L0 #des #HL01 #X #H #L2 #HL20 lapply (aacr_acr … H1RP H2RP B) #HB elim (lifts_inv_lref1 … H) -H #i1 #Hi1 #H destruct - lapply (ldrop_fwd_ldrop2 … HLK1) #HK1b + lapply (ldrop_fwd_drop2 … HLK1) #HK1b elim (ldrops_ldrop_trans … HL01 … HLK1) #X #des1 #i0 #HL0 #H #Hi0 #Hdes1 >(at_mono … Hi1 … Hi0) -i1 elim (ldrops_inv_skip2 … Hdes1 … H) -des1 #K0 #V0 #des0 #Hdes0 #HK01 #HV10 #H destruct @@ -48,7 +48,7 @@ theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP. @(s5 … HB … (◊) … HV0 HLK2) /3 width=7 by ldrops_cons, lifts_cons/ (* Note: uses IHB HL20 V2 HV0 *) | -HLK1 -IHB -HL01 -HL20 -HK1b -Hi0 -Hdes0 #K2 #V2 #A2 #HKV2A #H1KV0A #H2KV0A #_ #H1 #H2 destruct - lapply (ldrop_fwd_ldrop2 … HLK2) #HLK2b + lapply (ldrop_fwd_drop2 … HLK2) #HLK2b lapply (aaa_lifts … HK01 … HV10 HKV1B) -HKV1B -HK01 -HV10 #HKV0B lapply (aaa_mono … H2KV0A … HKV0B) #H destruct -H2KV0A -HKV0B elim (lift_total V0 0 (i0 +1)) #V3 #HV03 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 e570307ac..6298274bc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma @@ -25,7 +25,7 @@ lemma cprs_delta: ∀G,L,K,V,V2,i. ∀W2. ⇧[0, i + 1] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ➡* W2. #G #L #K #V #V2 #i #HLK #H elim H -V2 [ /3 width=6/ ] #V1 #V2 #_ #HV12 #IHV1 #W2 #HVW2 -lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK +lapply (ldrop_fwd_drop2 … HLK) -HLK #HLK elim (lift_total V1 0 (i+1)) /4 width=11 by cpr_lift, cprs_strap1/ qed. @@ -42,7 +42,7 @@ lemma cprs_inv_lref1: ∀G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡* T2 → elim (cpr_inv_lref1 … HT2) -HT2 /2 width=1/ * /4 width=6/ | * #K #V1 #T1 #HLK #HVT1 #HT1 - lapply (ldrop_fwd_ldrop2 … HLK) #H0LK + lapply (ldrop_fwd_drop2 … HLK) #H0LK elim (cpr_inv_lift1 … HT2 … H0LK … HT1) -H0LK -T /4 width=6/ ] 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 fa14bfc25..e4c5cea84 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma @@ -142,7 +142,7 @@ lemma fqu_cpxs_trans_neq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 [ #I #G #L #V1 #V2 #HV12 #_ elim (lift_total V2 0 1) #U2 #HVU2 @(ex3_intro … U2) - [1,3: /3 width=7 by fqu_drop, cpxs_delta, ldrop_pair, ldrop_ldrop/ + [1,3: /3 width=7 by fqu_drop, cpxs_delta, ldrop_pair, ldrop_drop/ | #H destruct /2 width=7 by lift_inv_lref2_be/ ] | #I #G #L #V1 #T #V2 #HV12 #H @(ex3_intro … (②{I}V2.T)) 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 0c9cfe1e7..2d6797667 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma @@ -37,7 +37,7 @@ lemma cpxs_delta: ∀h,g,I,G,L,K,V,V2,i. ∀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_ldrop2 … HLK) -HLK +| #V1 lapply (ldrop_fwd_drop2 … HLK) -HLK elim (lift_total V1 0 (i+1)) /4 width=11 by cpx_lift, cpxs_strap1/ ] qed. @@ -54,7 +54,7 @@ lemma cpxs_inv_lref1: ∀h,g,G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡*[h, g] T2 → elim (cpx_inv_lref1 … HT2) -HT2 /2 width=1 by or_introl/ * /4 width=7 by cpx_cpxs, ex3_4_intro, or_intror/ | * #I #K #V1 #T1 #HLK #HVT1 #HT1 - lapply (ldrop_fwd_ldrop2 … HLK) #H0LK + lapply (ldrop_fwd_drop2 … HLK) #H0LK elim (cpx_inv_lift1 … HT2 … H0LK … HT1) -H0LK -T /4 width=7 by cpxs_strap1, ex3_4_intro, or_intror/ ] 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 faae2dd87..30745dd38 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma @@ -64,7 +64,7 @@ lemma cpxs_fwd_delta: ∀h,g,I,G,L,K,V1,i. ⇩[0, i] L ≡ K.ⓑ{I}V1 → elim (cpxs_inv_lref1 … H) -H /2 width=1/ * #I0 #K0 #V0 #U0 #HLK0 #HVU0 #HU0 lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H destruct -lapply (ldrop_fwd_ldrop2 … HLK) -HLK /3 width=9/ +lapply (ldrop_fwd_drop2 … HLK) -HLK /3 width=9/ qed-. lemma cpxs_fwd_theta: ∀h,g,a,G,L,V1,V,T,U. ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}V.T ➡*[h, g] U → 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 5194bedfe..4f06e7912 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma @@ -48,7 +48,7 @@ lemma csx_inv_lref_bind: ∀h,g,I,G,L,K,V,i. ⇩[0, 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)) -/4 width=9 by csx_inv_lift, csx_cpx_trans, cpx_delta, ldrop_fwd_ldrop2/ +/4 width=9 by csx_inv_lift, csx_cpx_trans, cpx_delta, ldrop_fwd_drop2/ qed-. (* Advanced properties ******************************************************) @@ -61,7 +61,7 @@ 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_ldrop2/ + /3 width=7 by csx_lift, csx_cpx_trans, ldrop_fwd_drop2/ ] 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 f32a267c9..e16b976a7 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 @@ -68,7 +68,7 @@ lemma csx_applv_delta: ∀h,g,I,G,L,K,V1,i. ⇩[0, i] L ≡ K.ⓑ{I}V1 → ∀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_ldrop2 … HLK) #HLK0 + lapply (ldrop_fwd_drop2 … HLK) #HLK0 lapply (csx_inv_lift … H … HLK0 HV12) -V2 -HLK0 /2 width=5/ | #V #Vs #IHV #H1T lapply (csx_fwd_pair_sn … H1T) #HV 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 10600383a..c961d137c 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_ldrop, ex3_intro, or_intror/ + /6 width=11 by cpxs_strap1, cpx_lift, ldrop_drop, ex3_intro, or_intror/ ] 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 500d2f687..8283ea541 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsstas.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsstas.ma @@ -35,7 +35,7 @@ lemma lsubsv_lsstas_trans: ∀h,g,G,L2,T,U2,l1. ⦃G, L2⦄ ⊢ T •*[h, g, l1] elim (lsubsv_inv_pair2 … H) -H * #K1 [ | -HYU -IHXY -HLK1 ] [ #HK12 #H destruct elim (IHXY … Hl12 HV0 … HK12) -K2 -l2 #T #HXT #HTY - lapply (ldrop_fwd_ldrop2 … HLK1) #H + lapply (ldrop_fwd_drop2 … HLK1) #H elim (lift_total T 0 (i+1)) /3 width=11 by lsstas_ldef, cpcs_lift, ex2_intro/ | #V #l0 #_ #_ #_ #_ #_ #_ #_ #H destruct @@ -50,7 +50,7 @@ lemma lsubsv_lsstas_trans: ∀h,g,G,L2,T,U2,l1. ⦃G, L2⦄ ⊢ T •*[h, g, l1] lapply (lsubsv_fwd_lsubd … HK12) #H lapply (lsubd_da_trans … HV0 … H) -H elim (IHXY … Hl12 HV0 … HK12) -K2 -Hl12 #Y0 - lapply (ldrop_fwd_ldrop2 … HLK1) + lapply (ldrop_fwd_drop2 … HLK1) elim (lift_total Y0 0 (i+1)) /3 width=11 by lsstas_ldec, cpcs_lift, ex2_intro/ | #V #l #_ #_ #HVX #_ #HV #HX #HK12 #_ #H destruct @@ -60,7 +60,7 @@ lemma lsubsv_lsstas_trans: ∀h,g,G,L2,T,U2,l1. ⦃G, L2⦄ ⊢ T •*[h, g, l1] elim (lsstas_total … HVW (l1+1)) -W #W #HVW lapply (HVX … Hl12 HVW HXY0) -HVX -Hl12 -HXY0 #HWY0 lapply (cpcs_trans … HWY0 … HY0) -Y0 - lapply (ldrop_fwd_ldrop2 … HLK1) + lapply (ldrop_fwd_drop2 … HLK1) elim (lift_total W 0 (i+1)) /4 width=11 by lsstas_ldef, lsstas_cast, cpcs_lift, ex2_intro/ ] 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 b44137664..f86f5bd15 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 @@ -45,7 +45,7 @@ fact da_cpr_lpr_aux: ∀h,g,G0,L0,T0. lapply (fqup_lref … G1 … HLK1) 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_ldrop2 … HLK2) -V2 + lapply (ldrop_fwd_drop2 … HLK2) -V2 /4 width=7 by da_lift, fqup_fpbg/ ] | #p #_ #_ #HT0 #H1 destruct -IH3 -IH2 -IH1 @@ -57,7 +57,7 @@ fact da_cpr_lpr_aux: ∀h,g,G0,L0,T0. [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=9 by da_bind, fqup_fpbg, lpr_pair/ | #T2 #HT12 #HT2 #H1 #H2 destruct - /4 width=11 by da_inv_lift, fqup_fpbg, lpr_pair, ldrop_ldrop/ + /4 width=11 by da_inv_lift, fqup_fpbg, lpr_pair, ldrop_drop/ ] | #V1 #T1 #HG0 #HL0 #HT0 #H1 #l #H2 #X3 #H3 #L2 #HL12 destruct elim (snv_inv_appl … H1) -H1 #b0 #W1 #W0 #T0 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HT10 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 60e0d2619..75bf56d43 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_ldrop2 … HLK2) -HLK2 /4 width=7 by fqup_fpbg, snv_lift/ + lapply (ldrop_fwd_drop2 … HLK2) -HLK2 /4 width=7 by fqup_fpbg, snv_lift/ ] | #p #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2 -IH1 elim (snv_inv_gref … H1) @@ -47,7 +47,7 @@ fact snv_cpr_lpr_aux: ∀h,g,G0,L0,T0. elim (cpr_inv_bind1 … H2) -H2 * [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=8 by fqup_fpbg, snv_bind, lpr_pair/ | #T2 #HT12 #HXT2 #H1 #H2 destruct -HV1 - /4 width=10 by fqup_fpbg, snv_inv_lift, lpr_pair, ldrop_ldrop/ + /4 width=10 by fqup_fpbg, snv_inv_lift, lpr_pair, ldrop_drop/ ] | #V1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct elim (snv_inv_appl … H1) -H1 #a #W10 #W1 #U1 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HTU1 @@ -103,17 +103,17 @@ 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_ldrop/ -H1 #HVW20 - lapply (cpcs_lift … (L2.ⓓW2) … H3 … HW13 H2) /2 width=1 by ldrop_ldrop/ -HW13 -H3 -H2 #HW320 + 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 (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_ldrop/ -Hl0 #Hl0 + lapply (da_lift … Hl0 (L2.ⓓW2) … HV02) /2 width=1 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 - lapply (snv_lift … HV0 (L2.ⓓW2) … HV02) /3 width=7 by snv_bind, snv_appl, ldrop_ldrop/ + lapply (snv_lift … HV0 (L2.ⓓW2) … HV02) /3 width=7 by snv_bind, snv_appl, ldrop_drop/ ] | #W1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 elim (snv_inv_cast … H1) -H1 #U1 #l0 #HW1 #HT1 #Hl0 #HTU1 #HUW1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas.ma index d13c47cd3..739caf494 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas.ma @@ -37,7 +37,7 @@ fact snv_lsstas_aux: ∀h,g,G0,L0,T0. lapply (ldrop_mono … HLK0 … HLK1) -HLK0 #H destruct [ lapply (le_plus_to_le_r … Hl21) -Hl21 #Hl21 ] lapply (fqup_lref … G1 … HLK1) #H - lapply (ldrop_fwd_ldrop2 … HLK1) -HLK1 /4 width=8 by fqup_fpbg, snv_lift/ + lapply (ldrop_fwd_drop2 … HLK1) -HLK1 /4 width=8 by fqup_fpbg, snv_lift/ | #p #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X #H2 destruct -IH4 -IH3 -IH2 -IH1 elim (snv_inv_gref … H1) | #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X #H2 destruct -IH4 -IH3 -IH2 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 d43f443ef..a7b6e3e77 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 @@ -44,7 +44,7 @@ fact lsstas_cpr_lpr_aux: ∀h,g,G0,L0,T0. lapply (fqup_lref … G1 … HLK1) #HKV1 elim (lpr_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2 elim (lpr_inv_pair1 … H) -H #K2 [ #W2 | #V2 ] #HK12 [ #HW12 | #HV12 ] #H destruct - lapply (ldrop_fwd_ldrop2 … HLK2) #H2 + lapply (ldrop_fwd_drop2 … HLK2) #H2 elim (cpr_inv_lref1 … H3) -H3 [1,3: #H destruct -HLK1 |2,4: * #K0 #V0 #X0 #H #HVX0 #HX0 @@ -73,7 +73,7 @@ fact lsstas_cpr_lpr_aux: ∀h,g,G0,L0,T0. | #T3 #HT13 #HXT3 #H1 #H2 destruct elim (IH1 … Hl1 … HTU1 … HT13 (L2.ⓓV1)) -IH1 -Hl1 -HTU1 -HT13 /2 width=1 by fqup_fpbg, lpr_pair/ -T1 -HL12 #U3 #HTU3 #HU13 elim (lsstas_inv_lift1 … HTU3 L2 … HXT3) -T3 - /5 width=8 by cpcs_cpr_strap1, cpcs_bind1, cpr_zeta, ldrop_ldrop, ex2_intro/ + /5 width=8 by cpcs_cpr_strap1, cpcs_bind1, cpr_zeta, ldrop_drop, ex2_intro/ ] | #V1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X2 #H2 #X3 #H3 #L2 #HL12 destruct elim (snv_inv_appl … H1) -H1 #a #W1 #W10 #U10 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HTU10 diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma index bc5044b6d..0f015cc32 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma @@ -55,7 +55,7 @@ lemma lsubr_cpx_trans: ∀h,g,G. lsub_trans … (cpx h g G) lsubr. [ // | /2 width=2 by cpx_sort/ | #I #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12 - elim (lsubr_fwd_ldrop2_bind … HL12 … HLK1) -HL12 -HLK1 * + elim (lsubr_fwd_drop2_bind … HL12 … HLK1) -HL12 -HLK1 * /4 width=7 by cpx_delta, cpx_ti/ |4,9: /4 width=1 by cpx_bind, cpx_beta, lsubr_bind/ |5,7,8: /3 width=1 by cpx_flat, cpx_tau, cpx_ti/ @@ -88,7 +88,7 @@ lemma cpx_delift: ∀h,g,I,G,K,V,T1,L,d. ⇩[0, d] L ≡ (K.ⓑ{I}V) → elim (lift_split … HVW i i) /3 width=7 by cpx_delta, ex2_2_intro/ | * [ #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 /3 width=9 by cpx_bind, ldrop_ldrop, lift_bind, ex2_2_intro/ + [ elim (IHU1 (L. ⓑ{I} W1) (d+1)) -IHU1 /3 width=9 by cpx_bind, ldrop_drop, lift_bind, ex2_2_intro/ | elim (IHU1 … HLK) -IHU1 -HLK /3 width=8 by cpx_flat, lift_flat, ex2_2_intro/ ] ] 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 505eabf1a..4da4e21c8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma @@ -145,7 +145,7 @@ lemma fqu_cpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T /3 width=3 by fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, cpx_pair_sn, cpx_bind, cpx_flat, ex2_intro/ [ #I #G #L #V2 #U2 #HVU2 elim (lift_total U2 0 1) - /4 width=7 by fqu_drop, cpx_delta, ldrop_pair, ldrop_ldrop, ex2_intro/ + /4 width=7 by fqu_drop, cpx_delta, ldrop_pair, ldrop_drop, ex2_intro/ | #G #L #K #T1 #U1 #e #HLK1 #HTU1 #T2 #HTU2 elim (lift_total T2 0 (e+1)) /3 width=11 by cpx_lift, fqu_drop, ex2_intro/ @@ -200,7 +200,7 @@ lemma fqu_cpx_trans_neq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 [ #I #G #L #V1 #V2 #HV12 #_ elim (lift_total V2 0 1) #U2 #HVU2 @(ex3_intro … U2) - [1,3: /3 width=7 by fqu_drop, cpx_delta, ldrop_pair, ldrop_ldrop/ + [1,3: /3 width=7 by fqu_drop, cpx_delta, ldrop_pair, ldrop_drop/ | #H destruct /2 width=7 by lift_inv_lref2_be/ ] | #I #G #L #V1 #T #V2 #HV12 #H @(ex3_intro … (②{I}V2.T)) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma index bc56f721e..d810ae175 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma @@ -51,15 +51,15 @@ lemma lleq_cpx_conf_dx: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 → | /3 width=3 by lleq_fwd_length, lleq_sort/ | #I2 #G #L2 #K2 #V1 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV12 #L1 #H elim (lleq_inv_lref_ge_dx … H … HLK2) // -H #I1 #K1 #HLK1 #HV1 - lapply (ldrop_fwd_ldrop2 … HLK1) -HLK1 #HLK1 - lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 #HLK2 + lapply (ldrop_fwd_drop2 … HLK1) -HLK1 #HLK1 + lapply (ldrop_fwd_drop2 … HLK2) -HLK2 #HLK2 @(lleq_lift_le … HLK1 HLK2 … HVW2) -HLK1 -HLK2 -HVW2 /2 width=1 by/ (**) (* full auto too slow *) | #a #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #H elim (lleq_inv_bind_O … H) -H /4 width=5 by lleq_bind_repl_SO, lleq_bind/ | #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #H elim (lleq_inv_flat … H) -H /3 width=1 by lleq_flat/ | #G #L2 #V #T1 #T2 #T #_ #HT2 #IHT12 #L1 #H elim (lleq_inv_bind_O … H) -H - /3 width=10 by lleq_inv_lift_le, ldrop_ldrop/ + /3 width=10 by lleq_inv_lift_le, ldrop_drop/ | #G #L2 #V #T1 #T2 #_ #IHT12 #L1 #H elim (lleq_inv_flat … H) -H /2 width=1 by/ | #G #L2 #V1 #V2 #T #_ #IHV12 #L1 #H elim (lleq_inv_flat … H) -H /2 width=1 by/ | #a #G #L2 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L1 #H elim (lleq_inv_flat … H) -H @@ -68,7 +68,7 @@ lemma lleq_cpx_conf_dx: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 → | #a #G #L2 #V1 #V2 #V #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #L1 #H elim (lleq_inv_flat … H) -H #HV1 #H elim (lleq_inv_bind_O … H) -H #HW1 #HT1 @lleq_bind_O /2 width=1 by/ @lleq_flat (**) (* full auto too slow *) - [ /3 width=10 by lleq_lift_le, ldrop_ldrop/ + [ /3 width=10 by lleq_lift_le, ldrop_drop/ | /3 width=3 by lleq_bind_repl_O/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma index 933bcd637..fb9e9e691 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma @@ -40,7 +40,7 @@ elim (lpr_ldrop_conf … HLK0 … HL01) -HL01 #X1 #H1 #HLK1 elim (lpr_inv_pair1 … H1) -H1 #K1 #V1 #HK01 #HV01 #H destruct elim (lpr_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2 elim (lpr_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct -lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2 +lapply (ldrop_fwd_drop2 … HLK2) -W2 #HLK2 lapply (fqup_lref … G … HLK0) -HLK0 #HLK0 elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2 elim (lift_total V 0 (i+1)) @@ -66,10 +66,10 @@ fact cpr_conf_lpr_delta_delta: lapply (ldrop_mono … H … HLK0) -H #H destruct elim (lpr_ldrop_conf … HLK0 … HL01) -HL01 #X1 #H1 #HLK1 elim (lpr_inv_pair1 … H1) -H1 #K1 #W1 #HK01 #_ #H destruct -lapply (ldrop_fwd_ldrop2 … HLK1) -W1 #HLK1 +lapply (ldrop_fwd_drop2 … HLK1) -W1 #HLK1 elim (lpr_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2 elim (lpr_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct -lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2 +lapply (ldrop_fwd_drop2 … HLK2) -W2 #HLK2 lapply (fqup_lref … G … HLK0) -HLK0 #HLK0 elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2 elim (lift_total V 0 (i+1)) /3 width=11 by cpr_lift, ex2_intro/ @@ -107,7 +107,7 @@ fact cpr_conf_lpr_bind_zeta: #G #L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01 #T2 #HT02 #X2 #HXT2 #L1 #HL01 #L2 #HL02 elim (IH … HT01 … HT02 (L1.ⓓV1) … (L2.ⓓV1)) -IH -HT01 -HT02 /2 width=1 by lpr_pair/ -L0 -V0 -T0 #T #HT1 #HT2 -elim (cpr_inv_lift1 … HT2 L2 … HXT2) -T2 /3 width=3 by cpr_zeta, ldrop_ldrop, ex2_intro/ +elim (cpr_inv_lift1 … HT2 L2 … HXT2) -T2 /3 width=3 by cpr_zeta, ldrop_drop, ex2_intro/ qed-. fact cpr_conf_lpr_zeta_zeta: @@ -124,8 +124,8 @@ fact cpr_conf_lpr_zeta_zeta: #G #L0 #V0 #T0 #IH #T1 #HT01 #X1 #HXT1 #T2 #HT02 #X2 #HXT2 #L1 #HL01 #L2 #HL02 elim (IH … HT01 … HT02 (L1.ⓓV0) … (L2.ⓓV0)) -IH -HT01 -HT02 /2 width=1 by lpr_pair/ -L0 -T0 #T #HT1 #HT2 -elim (cpr_inv_lift1 … HT1 L1 … HXT1) -T1 /2 width=1 by ldrop_ldrop/ #T1 #HT1 #HXT1 -elim (cpr_inv_lift1 … HT2 L2 … HXT2) -T2 /2 width=1 by ldrop_ldrop/ #T2 #HT2 #HXT2 +elim (cpr_inv_lift1 … HT1 L1 … HXT1) -T1 /2 width=1 by ldrop_drop/ #T1 #HT1 #HXT1 +elim (cpr_inv_lift1 … HT2 L2 … HXT2) -T2 /2 width=1 by ldrop_drop/ #T2 #HT2 #HXT2 lapply (lift_inj … HT2 … HT1) -T #H destruct /2 width=3 by ex2_intro/ qed-. @@ -217,7 +217,7 @@ fact cpr_conf_lpr_flat_theta: #V2 #HV02 #U2 #HVU2 #W2 #HW02 #T2 #HT02 #L1 #HL01 #L2 #HL02 elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2 elim (lift_total V 0 1) #U #HVU -lapply (cpr_lift … HV2 (L2.ⓓW2) … HVU2 … HVU) -HVU2 /2 width=1 by ldrop_ldrop/ #HU2 +lapply (cpr_lift … HV2 (L2.ⓓW2) … HVU2 … HVU) -HVU2 /2 width=1 by ldrop_drop/ #HU2 elim (cpr_inv_abbr1 … H) -H * [ #W1 #T1 #HW01 #HT01 #H destruct elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1 by/ @@ -226,7 +226,7 @@ elim (cpr_inv_abbr1 … H) -H * | #T1 #HT01 #HXT1 #H destruct elim (IH … HT01 … HT02 (L1.ⓓW2) … (L2.ⓓW2)) /2 width=1 by lpr_pair/ -L0 -V0 -W0 -T0 #T #HT1 #HT2 elim (cpr_inv_lift1 … HT1 L1 … HXT1) -HXT1 - /4 width=9 by cpr_flat, cpr_zeta, ldrop_ldrop, lift_flat, ex2_intro/ + /4 width=9 by cpr_flat, cpr_zeta, ldrop_drop, lift_flat, ex2_intro/ ] qed-. @@ -271,8 +271,8 @@ elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1 by/ #V #HV1 elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1 by/ elim (IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) /2 width=1 by lpr_pair/ -L0 -V0 -W0 -T0 elim (lift_total V 0 1) #U #HVU -lapply (cpr_lift … HV1 (L1.ⓓW1) … HVU1 … HVU) -HVU1 /2 width=1 by ldrop_ldrop/ -lapply (cpr_lift … HV2 (L2.ⓓW2) … HVU2 … HVU) -HVU2 /2 width=1 by ldrop_ldrop/ +lapply (cpr_lift … HV1 (L1.ⓓW1) … HVU1 … HVU) -HVU1 /2 width=1 by ldrop_drop/ +lapply (cpr_lift … HV2 (L2.ⓓW2) … HVU2 … HVU) -HVU2 /2 width=1 by ldrop_drop/ /4 width=7 by cpr_bind, cpr_flat, ex2_intro/ (**) (* full auto not tried *) qed-. 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 e21810ea5..3537c8d01 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma @@ -36,7 +36,7 @@ lemma aaa_cpx_lpx_conf: ∀h,g,G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A → lapply (ldrop_mono … H … HLK1) -H #H destruct elim (lpx_ldrop_conf … HLK1 … HL12) -L1 #Z #H #HLK2 elim (lpx_inv_pair1 … H) -H #K2 #V0 #HK12 #_ #H destruct - lapply (ldrop_fwd_ldrop2 … HLK2) -V0 /3 width=7/ + lapply (ldrop_fwd_drop2 … HLK2) -V0 /3 width=7/ ] | #a #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 elim (cpx_inv_abbr1 … H) -H * diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma index 705d5695e..b6c3584ed 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma @@ -61,7 +61,7 @@ lemma lpx_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T /3 width=7 by fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, lpx_pair, ex3_2_intro/ [ #I #G1 #L1 #V1 #X #H elim (lpx_inv_pair2 … H) -H #K1 #W1 #HKL1 #HWV1 #H destruct elim (lift_total V1 0 1) - /4 width=7 by cpx_delta, fqu_drop, ldrop_ldrop, ex3_2_intro/ + /4 width=7 by cpx_delta, fqu_drop, ldrop_drop, ex3_2_intro/ | #G #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #L0 #HL01 elim (lpx_ldrop_trans_O1 … HL01 … HLK1) -L1 /3 width=5 by fqu_drop, ex3_2_intro/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma index b26b7e95b..af0172fdb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma @@ -36,11 +36,11 @@ inductive ldrop (s:bool): relation4 nat nat lenv lenv ≝ interpretation "basic slicing (local environment) abstract" 'RDrop s d e L1 L2 = (ldrop s d e L1 L2). - +(* interpretation "basic slicing (local environment) general" 'RDrop d e L1 L2 = (ldrop true d e L1 L2). - +*) interpretation "basic slicing (local environment) lget" 'RDrop e L1 L2 = (ldrop false O e L1 L2). diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_ssta.ma index 45cf9cda7..5cccd8fe1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_ssta.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_ssta.ma @@ -27,7 +27,7 @@ lemma aaa_ssta_conf: ∀h,g,G,L. Conf3 … (aaa G L) (ssta h g G L). | #I #G #L #K #V #B #i #HLK #HV #IHV #U #H elim (ssta_inv_lref1 … H) -H * #K0 #V0 #W0 #HLK0 #HVW0 #HU lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H0 destruct - lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK + lapply (ldrop_fwd_drop2 … HLK) -HLK #HLK @(aaa_lift … HLK … HU) -HU -L // -HV /2 width=2/ | #a #G #L #V #T #B #A #HV #_ #_ #IHT #X #H elim (ssta_inv_bind1 … H) -H #U #HTU #H destruct /3 width=2/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lift.ma index 94aec3b15..ff975d25a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lift.ma @@ -108,11 +108,11 @@ lemma ssta_da_conf: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T •[h, g] U → | #G #L #K #V #U #W #i #HLK #_ #HWU #IHVW #l #H elim (da_inv_lref … H) -H * #K0 #V0 [| #l0] #HLK0 #HV0 lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H destruct - lapply (ldrop_fwd_ldrop2 … HLK) -HLK /3 width=7/ + lapply (ldrop_fwd_drop2 … HLK) -HLK /3 width=7/ | #G #L #K #W #U #l0 #i #HLK #_ #HWU #l #H -l0 elim (da_inv_lref … H) -H * #K0 #V0 [| #l1] #HLK0 #HV0 [| #H0 ] lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H destruct - lapply (ldrop_fwd_ldrop2 … HLK) -HLK /3 width=7/ + lapply (ldrop_fwd_drop2 … HLK) -HLK /3 width=7/ | #a #I #G #L #V #T #U #_ #IHTU #l #H lapply (da_inv_bind … H) -H /3 width=1/ | #G #L #V #T #U #_ #IHTU #l #H @@ -129,11 +129,11 @@ lemma ssta_fwd_correct: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T •[h, g] U → #h #g #G #L #T #U #H elim H -G -L -T -U [ /2 width=2/ | #G #L #K #V #U #W #i #HLK #_ #HWU * #T #HWT - lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK + lapply (ldrop_fwd_drop2 … HLK) -HLK #HLK elim (lift_total T 0 (i+1)) /3 width=10/ | #G #L #K #W #U #l #i #HLK #HWl #HWU elim (da_ssta … HWl) -HWl #T #HWT - lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK + lapply (ldrop_fwd_drop2 … HLK) -HLK #HLK elim (lift_total T 0 (i+1)) /3 width=10/ | #a #I #G #L #V #T #U #_ * /3 width=2/ | #G #L #V #T #U #_ * #T0 #HUT0 /3 width=2/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma index 929007118..3fb179ed2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma @@ -21,7 +21,7 @@ include "basic_2/substitution/cpys_lift.ma". inductive cpysa: ynat → ynat → relation4 genv lenv term term ≝ | cpysa_atom : ∀I,G,L,d,e. cpysa d e G L (⓪{I}) (⓪{I}) | cpysa_subst: ∀I,G,L,K,V1,V2,W2,i,d,e. d ≤ yinj i → i < d+e → - ⇩[0, i] L ≡ K.ⓑ{I}V1 → cpysa 0 (⫰(d+e-i)) G K V1 V2 → + ⇩[i] L ≡ K.ⓑ{I}V1 → cpysa 0 (⫰(d+e-i)) G K V1 V2 → ⇧[0, i+1] V2 ≡ W2 → cpysa d e G L (#i) W2 | cpysa_bind : ∀a,I,G,L,V1,V2,T1,T2,d,e. cpysa d e G L V1 V2 → cpysa (⫯d) e G (L.ⓑ{I}V2) T1 T2 → @@ -58,7 +58,7 @@ lemma cpysa_cpy_trans: ∀G,L,T1,T,d,e. ⦃G, L⦄ ⊢ T1 ▶▶*×[d, e] T → [ #I #G #L #d #e #X #H elim (cpy_inv_atom1 … H) -H // * /2 width=7 by cpysa_subst/ | #I #G #L #K #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK #_ #HVW2 #IHV12 #T2 #H - lapply (ldrop_fwd_ldrop2 … HLK) #H0LK + lapply (ldrop_fwd_drop2 … HLK) #H0LK lapply (cpy_weak … H 0 (d+e) ? ?) -H // #H elim (cpy_inv_lift1_be … H … H0LK … HVW2) -H -H0LK -HVW2 /3 width=7 by cpysa_subst, ylt_fwd_le_succ/ @@ -86,7 +86,7 @@ qed-. lemma cpys_ind_alt: ∀R:ynat→ynat→relation4 genv lenv term term. (∀I,G,L,d,e. R d e G L (⓪{I}) (⓪{I})) → (∀I,G,L,K,V1,V2,W2,i,d,e. d ≤ yinj i → i < d + e → - ⇩[O, i] L ≡ K.ⓑ{I}V1 → ⦃G, K⦄ ⊢ V1 ▶*×[O, ⫰(d+e-i)] V2 → + ⇩[i] L ≡ K.ⓑ{I}V1 → ⦃G, K⦄ ⊢ V1 ▶*×[O, ⫰(d+e-i)] V2 → ⇧[O, i+1] V2 ≡ W2 → R O (⫰(d+e-i)) G K V1 V2 → R d e G L (#i) W2 ) → (∀a,I,G,L,V1,V2,T1,T2,d,e. ⦃G, L⦄ ⊢ V1 ▶*×[d, e] V2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cpys.ma index aec0c7913..a3eedc255 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cpys.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cpys.ma @@ -59,11 +59,11 @@ lemma cpys_split_up: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 → qed-. lemma cpys_inv_lift1_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 → - ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → - d ≤ dt → dt ≤ d + e → d + e ≤ dt + et → - ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[d, dt + et - (d + e)] T2 & + ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → + d ≤ dt → dt ≤ yinj d + e → yinj d + e ≤ dt + et → + ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[d, dt + et - (yinj d + e)] T2 & ⇧[d, e] T2 ≡ U2. -#G #L #U1 #U2 #dt #et #HU12 #K #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet +#G #L #U1 #U2 #dt #et #HU12 #K #s #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet elim (cpys_split_up … HU12 (d + e)) -HU12 // -Hdedet #U #HU1 #HU2 lapply (cpys_weak … HU1 d e ? ?) -HU1 // [ >ymax_pre_sn_comm // ] -Hddt -Hdtde #HU1 lapply (cpys_inv_lift1_eq … HU1 … HTU1) -HU1 #HU1 destruct diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma index c4b9518e6..4a621d7d6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma @@ -21,14 +21,14 @@ include "basic_2/substitution/cpys.ma". lemma cpys_subst: ∀I,G,L,K,V,U1,i,d,e. d ≤ yinj i → i < d + e → - ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ▶*×[0, ⫰(d+e-i)] U1 → + ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ▶*×[0, ⫰(d+e-i)] U1 → ∀U2. ⇧[0, i+1] U1 ≡ U2 → ⦃G, L⦄ ⊢ #i ▶*×[d, e] U2. #I #G #L #K #V #U1 #i #d #e #Hdi #Hide #HLK #H @(cpys_ind … H) -U1 [ /3 width=5 by cpy_cpys, cpy_subst/ | #U #U1 #_ #HU1 #IHU #U2 #HU12 elim (lift_total U 0 (i+1)) #U0 #HU0 lapply (IHU … HU0) -IHU #H - lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK + lapply (ldrop_fwd_drop2 … HLK) -HLK #HLK lapply (cpy_lift_ge … HU1 … HLK HU0 HU12 ?) -HU1 -HLK -HU0 -HU12 // #HU02 lapply (cpy_weak … HU02 d e ? ?) -HU02 [2,3: /2 width=3 by cpys_strap1, yle_succ_dx/ ] @@ -38,7 +38,7 @@ qed. lemma cpys_subst_Y2: ∀I,G,L,K,V,U1,i,d. d ≤ yinj i → - ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ▶*×[0, ∞] U1 → + ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ▶*×[0, ∞] U1 → ∀U2. ⇧[0, i+1] U1 ≡ U2 → ⦃G, L⦄ ⊢ #i ▶*×[d, ∞] U2. #I #G #L #K #V #U1 #i #d #Hdi #HLK #HVU1 #U2 #HU12 @(cpys_subst … HLK … HU12) >yminus_Y_inj // @@ -49,7 +49,7 @@ qed. lemma cpys_inv_atom1: ∀I,G,L,T2,d,e. ⦃G, L⦄ ⊢ ⓪{I} ▶*×[d, e] T2 → T2 = ⓪{I} ∨ ∃∃J,K,V1,V2,i. d ≤ yinj i & i < d + e & - ⇩[O, i] L ≡ K.ⓑ{J}V1 & + ⇩[i] L ≡ K.ⓑ{J}V1 & ⦃G, K⦄ ⊢ V1 ▶*×[0, ⫰(d+e-i)] V2 & ⇧[O, i+1] V2 ≡ T2 & I = LRef i. @@ -59,7 +59,7 @@ lemma cpys_inv_atom1: ∀I,G,L,T2,d,e. ⦃G, L⦄ ⊢ ⓪{I} ▶*×[d, e] T2 → [ #H destruct elim (cpy_inv_atom1 … HT2) -HT2 [ /2 width=1 by or_introl/ | * /3 width=11 by ex6_5_intro, or_intror/ ] | * #J #K #V1 #V #i #Hdi #Hide #HLK #HV1 #HVT #HI - lapply (ldrop_fwd_ldrop2 … HLK) #H + lapply (ldrop_fwd_drop2 … HLK) #H elim (cpy_inv_lift1_ge_up … HT2 … H … HVT) -HT2 -H -HVT [2,3,4: /2 width=1 by ylt_fwd_le_succ, yle_succ_dx/ ] /4 width=11 by cpys_strap1, ex6_5_intro, or_intror/ @@ -70,7 +70,7 @@ qed-. lemma cpys_inv_lref1: ∀G,L,T2,i,d,e. ⦃G, L⦄ ⊢ #i ▶*×[d, e] T2 → T2 = #i ∨ ∃∃I,K,V1,V2. d ≤ i & i < d + e & - ⇩[O, i] L ≡ K.ⓑ{I}V1 & + ⇩[i] L ≡ K.ⓑ{I}V1 & ⦃G, K⦄ ⊢ V1 ▶*×[0, ⫰(d+e-i)] V2 & ⇧[O, i+1] V2 ≡ T2. #G #L #T2 #i #d #e #H elim (cpys_inv_atom1 … H) -H /2 width=1 by or_introl/ @@ -78,7 +78,7 @@ lemma cpys_inv_lref1: ∀G,L,T2,i,d,e. ⦃G, L⦄ ⊢ #i ▶*×[d, e] T2 → qed-. lemma cpys_inv_lref1_ldrop: ∀G,L,T2,i,d,e. ⦃G, L⦄ ⊢ #i ▶*×[d, e] T2 → - ∀I,K,V1. ⇩[O, i] L ≡ K.ⓑ{I}V1 → + ∀I,K,V1. ⇩[i] L ≡ K.ⓑ{I}V1 → ∀V2. ⇧[O, i+1] V2 ≡ T2 → ∧∧ ⦃G, K⦄ ⊢ V1 ▶*×[0, ⫰(d+e-i)] V2 & d ≤ i @@ -95,10 +95,10 @@ qed-. (* Properties on relocation *************************************************) lemma cpys_lift_le: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*×[dt, et] T2 → - ∀L,U1,d,e. dt + et ≤ yinj d → ⇩[d, e] L ≡ K → + ∀L,U1,s,d,e. dt + et ≤ yinj d → ⇩[s, d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 → ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2. -#G #K #T1 #T2 #dt #et #H #L #U1 #d #e #Hdetd #HLK #HTU1 @(cpys_ind … H) -T2 +#G #K #T1 #T2 #dt #et #H #L #U1 #s #d #e #Hdetd #HLK #HTU1 @(cpys_ind … H) -T2 [ #U2 #H >(lift_mono … HTU1 … H) -H // | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2 elim (lift_total T d e) #U #HTU @@ -108,10 +108,10 @@ lemma cpys_lift_le: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*×[dt, et] T2 → qed-. lemma cpys_lift_be: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*×[dt, et] T2 → - ∀L,U1,d,e. dt ≤ yinj d → d ≤ dt + et → - ⇩[d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 → + ∀L,U1,s,d,e. dt ≤ yinj d → d ≤ dt + et → + ⇩[s, d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 → ⦃G, L⦄ ⊢ U1 ▶*×[dt, et + e] U2. -#G #K #T1 #T2 #dt #et #H #L #U1 #d #e #Hdtd #Hddet #HLK #HTU1 @(cpys_ind … H) -T2 +#G #K #T1 #T2 #dt #et #H #L #U1 #s #d #e #Hdtd #Hddet #HLK #HTU1 @(cpys_ind … H) -T2 [ #U2 #H >(lift_mono … HTU1 … H) -H // | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2 elim (lift_total T d e) #U #HTU @@ -121,10 +121,10 @@ lemma cpys_lift_be: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*×[dt, et] T2 → qed-. lemma cpys_lift_ge: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*×[dt, et] T2 → - ∀L,U1,d,e. yinj d ≤ dt → ⇩[d, e] L ≡ K → + ∀L,U1,s,d,e. yinj d ≤ dt → ⇩[s, d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 → ⦃G, L⦄ ⊢ U1 ▶*×[dt+e, et] U2. -#G #K #T1 #T2 #dt #et #H #L #U1 #d #e #Hddt #HLK #HTU1 @(cpys_ind … H) -T2 +#G #K #T1 #T2 #dt #et #H #L #U1 #s #d #e #Hddt #HLK #HTU1 @(cpys_ind … H) -T2 [ #U2 #H >(lift_mono … HTU1 … H) -H // | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2 elim (lift_total T d e) #U #HTU @@ -136,10 +136,10 @@ qed-. (* Inversion lemmas for relocation ******************************************) lemma cpys_inv_lift1_le: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 → - ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → + ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → dt + et ≤ d → ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[dt, et] T2 & ⇧[d, e] T2 ≡ U2. -#G #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdetd @(cpys_ind … H) -U2 +#G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hdetd @(cpys_ind … H) -U2 [ /2 width=3 by ex2_intro/ | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU elim (cpy_inv_lift1_le … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/ @@ -147,10 +147,10 @@ lemma cpys_inv_lift1_le: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 qed-. lemma cpys_inv_lift1_be: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 → - ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → - dt ≤ d → d + e ≤ dt + et → + ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → + dt ≤ d → yinj d + e ≤ dt + et → ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[dt, et - e] T2 & ⇧[d, e] T2 ≡ U2. -#G #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdedet @(cpys_ind … H) -U2 +#G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hdtd #Hdedet @(cpys_ind … H) -U2 [ /2 width=3 by ex2_intro/ | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU elim (cpy_inv_lift1_be … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/ @@ -158,10 +158,10 @@ lemma cpys_inv_lift1_be: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 qed-. lemma cpys_inv_lift1_ge: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 → - ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → - d + e ≤ dt → + ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → + yinj d + e ≤ dt → ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[dt - e, et] T2 & ⇧[d, e] T2 ≡ U2. -#G #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdedt @(cpys_ind … H) -U2 +#G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hdedt @(cpys_ind … H) -U2 [ /2 width=3 by ex2_intro/ | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU elim (cpy_inv_lift1_ge … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/ @@ -171,11 +171,11 @@ qed-. (* Advanced inversion lemmas on relocation **********************************) lemma cpys_inv_lift1_ge_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 → - ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → - d ≤ dt → dt ≤ d + e → d + e ≤ dt + et → - ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[d, dt + et - (d + e)] T2 & + ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → + d ≤ dt → dt ≤ yinj d + e → yinj d + e ≤ dt + et → + ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[d, dt + et - (yinj d + e)] T2 & ⇧[d, e] T2 ≡ U2. -#G #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet @(cpys_ind … H) -U2 +#G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet @(cpys_ind … H) -U2 [ /2 width=3 by ex2_intro/ | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU elim (cpy_inv_lift1_ge_up … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/ @@ -183,10 +183,10 @@ lemma cpys_inv_lift1_ge_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] qed-. lemma cpys_inv_lift1_be_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 → - ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → - dt ≤ d → dt + et ≤ d + e → + ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → + dt ≤ d → dt + et ≤ yinj d + e → ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[dt, d - dt] T2 & ⇧[d, e] T2 ≡ U2. -#G #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdetde @(cpys_ind … H) -U2 +#G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hdtd #Hdetde @(cpys_ind … H) -U2 [ /2 width=3 by ex2_intro/ | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU elim (cpy_inv_lift1_be_up … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/ @@ -194,10 +194,10 @@ lemma cpys_inv_lift1_be_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] qed-. lemma cpys_inv_lift1_le_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 → - ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → - dt ≤ d → d ≤ dt + et → dt + et ≤ d + e → + ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → + dt ≤ d → d ≤ dt + et → dt + et ≤ yinj d + e → ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[dt, d - dt] T2 & ⇧[d, e] T2 ≡ U2. -#G #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hddet #Hdetde @(cpys_ind … H) -U2 +#G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hdtd #Hddet #Hdetde @(cpys_ind … H) -U2 [ /2 width=3 by ex2_intro/ | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU elim (cpy_inv_lift1_le_up … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup.ma index 82a8f5ed0..e68fe729b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup.ma @@ -37,7 +37,7 @@ lemma fqup_strap2: ∀G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄. /2 width=5 by tri_TC_strap/ qed. -lemma fqup_ldrop: ∀G1,G2,L1,K1,K2,T1,T2,U1,e. ⇩[0, e] L1 ≡ K1 → ⇧[0, e] T1 ≡ U1 → +lemma fqup_ldrop: ∀G1,G2,L1,K1,K2,T1,T2,U1,e. ⇩[e] L1 ≡ K1 → ⇧[0, e] T1 ≡ U1 → ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ → ⦃G1, L1, U1⦄ ⊃+ ⦃G2, K2, T2⦄. #G1 #G2 #L1 #K1 #K2 #T1 #T2 #U1 #e #HLK1 #HTU1 #HT12 elim (eq_or_gt … e) #H destruct [ >(ldrop_inv_O2 … HLK1) -L1 <(lift_inv_O2 … HTU1) -U1 // @@ -45,7 +45,7 @@ lemma fqup_ldrop: ∀G1,G2,L1,K1,K2,T1,T2,U1,e. ⇩[0, e] L1 ≡ K1 → ⇧[0, e ] qed-. -lemma fqup_lref: ∀I,G,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, L, #i⦄ ⊃+ ⦃G, K, V⦄. +lemma fqup_lref: ∀I,G,L,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, L, #i⦄ ⊃+ ⦃G, K, V⦄. /3 width=6 by fqu_lref_O, fqu_fqup, lift_lref_ge, fqup_ldrop/ qed. lemma fqup_pair_sn: ∀I,G,L,V,T. ⦃G, L, ②{I}V.T⦄ ⊃+ ⦃G, L, V⦄. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus.ma index 325be4b39..c05bb1145 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus.ma @@ -56,7 +56,7 @@ lemma fqus_strap2: ∀G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G, L, /2 width=5 by tri_TC_strap/ qed-. lemma fqus_ldrop: ∀G1,G2,K1,K2,T1,T2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ → - ∀L1,U1,e. ⇩[0, e] L1 ≡ K1 → ⇧[0, e] T1 ≡ U1 → + ∀L1,U1,e. ⇩[e] L1 ≡ K1 → ⇧[0, e] T1 ≡ U1 → ⦃G1, L1, U1⦄ ⊃* ⦃G2, K2, T2⦄. #G1 #G2 #K1 #K2 #T1 #T2 #H @(fqus_ind … H) -G2 -K2 -T2 /3 width=5 by fqus_strap1, fquq_fqus, fquq_drop/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops.ma index 912487a44..868b8ec2a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops.ma @@ -13,53 +13,59 @@ (**************************************************************************) include "basic_2/notation/relations/rdropstar_3.ma". +include "basic_2/notation/relations/rdropstar_4.ma". include "basic_2/relocation/ldrop.ma". include "basic_2/substitution/gr2_minus.ma". include "basic_2/substitution/lifts.ma". -(* GENERIC LOCAL ENVIRONMENT SLICING ****************************************) +(* ITERATED LOCAL ENVIRONMENT SLICING ***************************************) -inductive ldrops: list2 nat nat → relation lenv ≝ -| ldrops_nil : ∀L. ldrops (⟠) L L +inductive ldrops (s:bool): list2 nat nat → relation lenv ≝ +| ldrops_nil : ∀L. ldrops s (⟠) L L | ldrops_cons: ∀L1,L,L2,des,d,e. - ldrops des L1 L → ⇩[d,e] L ≡ L2 → ldrops ({d, e} @ des) L1 L2 + ldrops s des L1 L → ⇩[s, d, e] L ≡ L2 → ldrops s ({d, e} @ des) L1 L2 . -interpretation "generic local environment slicing" - 'RDropStar des T1 T2 = (ldrops des T1 T2). +interpretation "iterated slicing (local environment) abstract" + 'RDropStar s des T1 T2 = (ldrops s des T1 T2). +(* +interpretation "iterated slicing (local environment) general" + 'RDropStar des T1 T2 = (ldrops true des T1 T2). +*) (* Basic inversion lemmas ***************************************************) -fact ldrops_inv_nil_aux: ∀L1,L2,des. ⇩*[des] L1 ≡ L2 → des = ⟠ → L1 = L2. -#L1 #L2 #des * -L1 -L2 -des // +fact ldrops_inv_nil_aux: ∀L1,L2,s,des. ⇩*[s, des] L1 ≡ L2 → des = ⟠ → L1 = L2. +#L1 #L2 #s #des * -L1 -L2 -des // #L1 #L #L2 #d #e #des #_ #_ #H destruct qed-. (* Basic_1: was: drop1_gen_pnil *) -lemma ldrops_inv_nil: ∀L1,L2. ⇩*[⟠] L1 ≡ L2 → L1 = L2. -/2 width=3 by ldrops_inv_nil_aux/ qed-. +lemma ldrops_inv_nil: ∀L1,L2,s. ⇩*[s, ⟠] L1 ≡ L2 → L1 = L2. +/2 width=4 by ldrops_inv_nil_aux/ qed-. -fact ldrops_inv_cons_aux: ∀L1,L2,des. ⇩*[des] L1 ≡ L2 → +fact ldrops_inv_cons_aux: ∀L1,L2,s,des. ⇩*[s, des] L1 ≡ L2 → ∀d,e,tl. des = {d, e} @ tl → - ∃∃L. ⇩*[tl] L1 ≡ L & ⇩[d, e] L ≡ L2. -#L1 #L2 #des * -L1 -L2 -des + ∃∃L. ⇩*[s, tl] L1 ≡ L & ⇩[s, d, e] L ≡ L2. +#L1 #L2 #s #des * -L1 -L2 -des [ #L #d #e #tl #H destruct | #L1 #L #L2 #des #d #e #HT1 #HT2 #hd #he #tl #H destruct /2 width=3 by ex2_intro/ +] qed-. (* Basic_1: was: drop1_gen_pcons *) -lemma ldrops_inv_cons: ∀L1,L2,d,e,des. ⇩*[{d, e} @ des] L1 ≡ L2 → - ∃∃L. ⇩*[des] L1 ≡ L & ⇩[d, e] L ≡ L2. +lemma ldrops_inv_cons: ∀L1,L2,s,d,e,des. ⇩*[s, {d, e} @ des] L1 ≡ L2 → + ∃∃L. ⇩*[s, des] L1 ≡ L & ⇩[s, d, e] L ≡ L2. /2 width=3 by ldrops_inv_cons_aux/ qed-. -lemma ldrops_inv_skip2: ∀I,des,i,des2. des ▭ i ≡ des2 → - ∀L1,K2,V2. ⇩*[des2] L1 ≡ K2. ⓑ{I} V2 → +lemma ldrops_inv_skip2: ∀I,s,des,des2,i. des ▭ i ≡ des2 → + ∀L1,K2,V2. ⇩*[s, des2] L1 ≡ K2. ⓑ{I} V2 → ∃∃K1,V1,des1. des + 1 ▭ i + 1 ≡ des1 + 1 & - ⇩*[des1] K1 ≡ K2 & + ⇩*[s, des1] K1 ≡ K2 & ⇧*[des1] V2 ≡ V1 & L1 = K1. ⓑ{I} V1. -#I #des #i #des2 #H elim H -des -i -des2 +#I #s #des #des2 #i #H elim H -des -des2 -i [ #i #L1 #K2 #V2 #H >(ldrops_inv_nil … H) -L1 /2 width=7 by lifts_nil, minuss_nil, ex4_3_intro, ldrops_nil/ | #des #des2 #d #e #i #Hid #_ #IHdes2 #L1 #K2 #V2 #H @@ -77,9 +83,9 @@ qed-. (* Basic properties *********************************************************) (* Basic_1: was: drop1_skip_bind *) -lemma ldrops_skip: ∀L1,L2,des. ⇩*[des] L1 ≡ L2 → ∀V1,V2. ⇧*[des] V2 ≡ V1 → - ∀I. ⇩*[des + 1] L1. ⓑ{I} V1 ≡ L2. ⓑ{I} V2. -#L1 #L2 #des #H elim H -L1 -L2 -des +lemma ldrops_skip: ∀L1,L2,s,des. ⇩*[s, des] L1 ≡ L2 → ∀V1,V2. ⇧*[des] V2 ≡ V1 → + ∀I. ⇩*[s, des + 1] L1.ⓑ{I}V1 ≡ L2.ⓑ{I}V2. +#L1 #L2 #s #des #H elim H -L1 -L2 -des [ #L #V1 #V2 #HV12 #I >(lifts_inv_nil … HV12) -HV12 // | #L1 #L #L2 #des #d #e #_ #HL2 #IHL #V1 #V2 #H #I 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 22eed845f..958052e5b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrop.ma @@ -15,21 +15,21 @@ include "basic_2/relocation/ldrop_ldrop.ma". include "basic_2/substitution/ldrops.ma". -(* GENERIC LOCAL ENVIRONMENT SLICING ****************************************) +(* ITERATED LOCAL ENVIRONMENT SLICING ***************************************) (* Properties concerning basic local environment slicing ********************) -lemma ldrops_ldrop_trans: ∀L1,L,des. ⇩*[des] L1 ≡ L → ∀L2,i. ⇩[0, i] L ≡ L2 → - ∃∃L0,des0,i0. ⇩[0, i0] L1 ≡ L0 & ⇩*[des0] L0 ≡ L2 & +lemma ldrops_ldrop_trans: ∀L1,L,des. ⇩*[Ⓕ, des] L1 ≡ L → ∀L2,i. ⇩[i] L ≡ L2 → + ∃∃L0,des0,i0. ⇩[i0] L1 ≡ L0 & ⇩*[Ⓕ, des0] L0 ≡ L2 & @⦃i, des⦄ ≡ i0 & des ▭ i ≡ des0. #L1 #L #des #H elim H -L1 -L -des -[ /2 width=7/ +[ /2 width=7 by ldrops_nil, minuss_nil, at_nil, ex4_3_intro/ | #L1 #L3 #L #des3 #d #e #_ #HL3 #IHL13 #L2 #i #HL2 elim (lt_or_ge i d) #Hid - [ elim (ldrop_trans_le … HL3 … HL2) -L /2 width=2/ #L #HL3 #HL2 - elim (IHL13 … HL3) -L3 /3 width=7/ + [ 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/ + elim (IHL13 … HL32) -L3 /3 width=7 by minuss_ge, at_ge, ex4_3_intro/ ] ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrops.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrops.ma index a4dbfb02e..474862b8c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrops.ma @@ -14,12 +14,12 @@ include "basic_2/substitution/ldrops_ldrop.ma". -(* GENERIC LOCAL ENVIRONMENT SLICING ****************************************) +(* ITERATED LOCAL ENVIRONMENT SLICING ***************************************) (* Main properties **********************************************************) (* Basic_1: was: drop1_trans *) -theorem ldrops_trans: ∀L,L2,des2. ⇩*[des2] L ≡ L2 → ∀L1,des1. ⇩*[des1] L1 ≡ L → - ⇩*[des2 @@ des1] L1 ≡ L2. -#L #L2 #des2 #H elim H -L -L2 -des2 // /3 width=3/ -qed. +theorem ldrops_trans: ∀L,L2,s,des2. ⇩*[s, des2] L ≡ L2 → ∀L1,des1. ⇩*[s, des1] L1 ≡ L → + ⇩*[s, des2 @@ des1] L1 ≡ L2. +#L #L2 #s #des2 #H elim H -L -L2 -des2 /3 width=3 by ldrops_cons/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma index 577343c6e..47d88486d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma @@ -100,14 +100,14 @@ lemma lleq_fwd_length: ∀L1,L2,T,d. L1 ⋕[T, d] L2 → |L1| = |L2|. #L1 #L2 #T #d * // qed-. -lemma lleq_fwd_ldrop_sn: ∀L1,L2,T,d. L1 ⋕[d, T] L2 → ∀K1,i. ⇩[0, i] L1 ≡ K1 → - ∃K2. ⇩[0, i] L2 ≡ K2. +lemma lleq_fwd_ldrop_sn: ∀L1,L2,T,d. L1 ⋕[d, T] L2 → ∀K1,i. ⇩[i] L1 ≡ K1 → + ∃K2. ⇩[i] L2 ≡ K2. #L1 #L2 #T #d #H #K1 #i #HLK1 lapply (lleq_fwd_length … H) -H #HL12 lapply (ldrop_fwd_length_le2 … HLK1) -HLK1 /2 width=1 by ldrop_O1_le/ qed-. -lemma lleq_fwd_ldrop_dx: ∀L1,L2,T,d. L1 ⋕[d, T] L2 → ∀K2,i. ⇩[0, i] L2 ≡ K2 → - ∃K1. ⇩[0, i] L1 ≡ K1. +lemma lleq_fwd_ldrop_dx: ∀L1,L2,T,d. L1 ⋕[d, T] L2 → ∀K2,i. ⇩[i] L2 ≡ K2 → + ∃K1. ⇩[i] L1 ≡ K1. /3 width=6 by lleq_fwd_ldrop_sn, lleq_sym/ qed-. lemma lleq_fwd_bind_sn: ∀a,I,L1,L2,V,T,d. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma index 0d99e8e1e..70bd0d615 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma @@ -19,7 +19,7 @@ inductive lleqa: relation4 ynat term lenv lenv ≝ | lleqa_sort: ∀L1,L2,d,k. |L1| = |L2| → lleqa d (⋆k) L1 L2 | lleqa_skip: ∀L1,L2,d,i. |L1| = |L2| → yinj i < d → lleqa d (#i) L1 L2 | lleqa_lref: ∀I1,I2,L1,L2,K1,K2,V,d,i. d ≤ yinj i → - ⇩[0, i] L1 ≡ K1.ⓑ{I1}V → ⇩[0, i] L2 ≡ K2.ⓑ{I2}V → + ⇩[i] L1 ≡ K1.ⓑ{I1}V → ⇩[i] L2 ≡ K2.ⓑ{I2}V → lleqa (yinj 0) V K1 K2 → lleqa d (#i) L1 L2 | lleqa_free: ∀L1,L2,d,i. |L1| = |L2| → |L1| ≤ i → |L2| ≤ i → lleqa d (#i) L1 L2 | lleqa_gref: ∀L1,L2,d,p. |L1| = |L2| → lleqa d (§p) L1 L2 @@ -61,7 +61,7 @@ lemma lleq_ind_alt: ∀R:relation4 ynat term lenv lenv. ( ∀L1,L2,d,i. |L1| = |L2| → yinj i < d → R d (#i) L1 L2 ) → ( ∀I1,I2,L1,L2,K1,K2,V,d,i. d ≤ yinj i → - ⇩[O, i] L1 ≡ K1.ⓑ{I1}V → ⇩[O, i] L2 ≡ K2.ⓑ{I2}V → + ⇩[i] L1 ≡ K1.ⓑ{I1}V → ⇩[i] L2 ≡ K2.ⓑ{I2}V → K1 ⋕[V, yinj O] K2 → R (yinj O) V K1 K2 → R d (#i) L1 L2 ) → ( ∀L1,L2,d,i. |L1| = |L2| → |L1| ≤ i → |L2| ≤ i → R d (#i) L1 L2 diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ext.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ext.ma index a1cf4458d..d6bb03fa7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ext.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ext.ma @@ -19,7 +19,7 @@ include "basic_2/substitution/lleq_alt.ma". (* Advanced inversion lemmas ************************************************) fact lleq_inv_S_aux: ∀L1,L2,T,d0. L1 ⋕[T, d0] L2 → ∀d. d0 = d + 1 → - ∀K1,K2,I,V. ⇩[0, d] L1 ≡ K1.ⓑ{I}V → ⇩[0, d] L2 ≡ K2.ⓑ{I}V → + ∀K1,K2,I,V. ⇩[d] L1 ≡ K1.ⓑ{I}V → ⇩[d] L2 ≡ K2.ⓑ{I}V → K1 ⋕[V, 0] K2 → L1 ⋕[T, d] L2. #L1 #L2 #T #d0 #H @(lleq_ind_alt … H) -L1 -L2 -T -d0 /2 width=1 by lleq_gref, lleq_free, lleq_sort/ @@ -29,14 +29,14 @@ fact lleq_inv_S_aux: ∀L1,L2,T,d0. L1 ⋕[T, d0] L2 → ∀d. d0 = d + 1 → | #I1 #I2 #L1 #L2 #K11 #K22 #V #d0 #i #Hd0i #HLK11 #HLK22 #HV #_ #d #H #K1 #K2 #J #W #_ #_ #_ destruct /3 width=8 by lleq_lref, yle_pred_sn/ | #a #I #L1 #L2 #V #T #d0 #_ #_ #IHV #IHT #d #H #K1 #K2 #J #W #HLK1 #HLK2 destruct - /4 width=7 by lleq_bind, ldrop_ldrop/ + /4 width=7 by lleq_bind, ldrop_drop/ | #I #L1 #L2 #V #T #d0 #_ #_ #IHV #IHT #d #H #K1 #K2 #J #W #HLK1 #HLK2 destruct /3 width=7 by lleq_flat/ ] qed-. lemma lleq_inv_S: ∀T,L1,L2,d. L1 ⋕[T, d+1] L2 → - ∀K1,K2,I,V. ⇩[0, d] L1 ≡ K1.ⓑ{I}V → ⇩[0, d] L2 ≡ K2.ⓑ{I}V → + ∀K1,K2,I,V. ⇩[d] L1 ≡ K1.ⓑ{I}V → ⇩[d] L2 ≡ K2.ⓑ{I}V → K1 ⋕[V, 0] K2 → L1 ⋕[T, d] L2. /2 width=7 by lleq_inv_S_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ldrop.ma index 126da3dd3..9cb597c6f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ldrop.ma @@ -26,7 +26,7 @@ lemma lleq_skip: ∀L1,L2,d,i. yinj i < d → |L1| = |L2| → L1 ⋕[#i, d] L2. qed. lemma lleq_lref: ∀I1,I2,L1,L2,K1,K2,V,d,i. d ≤ yinj i → - ⇩[0, i] L1 ≡ K1.ⓑ{I1}V → ⇩[0, i] L2 ≡ K2.ⓑ{I2}V → + ⇩[i] L1 ≡ K1.ⓑ{I1}V → ⇩[i] L2 ≡ K2.ⓑ{I2}V → K1 ⋕[V, 0] K2 → L1 ⋕[#i, d] L2. #I1 #I2 #L1 #L2 #K1 #K2 #V #d #i #Hdi #HLK1 #HLK2 * #HK12 #IH @conj [ -IH | -HK12 ] [ lapply (ldrop_fwd_length … HLK1) -HLK1 #H1 @@ -50,31 +50,31 @@ qed. (* Properties on relocation *************************************************) lemma lleq_lift_le: ∀K1,K2,T,dt. K1 ⋕[T, dt] K2 → - ∀L1,L2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 → + ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 → ∀U. ⇧[d, e] T ≡ U → dt ≤ d → L1 ⋕[U, dt] L2. #K1 #K2 #T #dt * #HK12 #IHT #L1 #L2 #d #e #HLK1 #HLK2 #U #HTU #Hdtd lapply (ldrop_fwd_length … HLK1) lapply (ldrop_fwd_length … HLK2) #H2 #H1 @conj // -HK12 -H1 -H2 #U0 @conj #HU0 [ letin HLKA ≝ HLK1 letin HLKB ≝ HLK2 | letin HLKA ≝ HLK2 letin HLKB ≝ HLK1 ] elim (cpys_inv_lift1_be … HU0 … HLKA … HTU) // -HU0 >yminus_Y_inj #T0 #HT0 #HTU0 -elim (IHT T0) [ #H #_ | #_ #H ] -IHT /3 width=11 by cpys_lift_be/ +elim (IHT T0) [ #H #_ | #_ #H ] -IHT /3 width=12 by cpys_lift_be/ qed-. lemma lleq_lift_ge: ∀K1,K2,T,dt. K1 ⋕[T, dt] K2 → - ∀L1,L2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 → + ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 → ∀U. ⇧[d, e] T ≡ U → d ≤ dt → L1 ⋕[U, dt+e] L2. #K1 #K2 #T #dt * #HK12 #IHT #L1 #L2 #d #e #HLK1 #HLK2 #U #HTU #Hddt lapply (ldrop_fwd_length … HLK1) lapply (ldrop_fwd_length … HLK2) #H2 #H1 @conj // -HK12 -H1 -H2 #U0 @conj #HU0 [ letin HLKA ≝ HLK1 letin HLKB ≝ HLK2 | letin HLKA ≝ HLK2 letin HLKB ≝ HLK1 ] elim (cpys_inv_lift1_ge … HU0 … HLKA … HTU) /2 width=1 by monotonic_yle_plus_dx/ -HU0 >yplus_minus_inj #T0 #HT0 #HTU0 -elim (IHT T0) [ #H #_ | #_ #H ] -IHT /3 width=9 by cpys_lift_ge/ +elim (IHT T0) [ #H #_ | #_ #H ] -IHT /3 width=10 by cpys_lift_ge/ qed-. (* Inversion lemmas on relocation *******************************************) lemma lleq_inv_lift_le: ∀L1,L2,U,dt. L1 ⋕[U, dt] L2 → - ∀K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 → + ∀K1,K2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 → ∀T. ⇧[d, e] T ≡ U → dt ≤ d → K1 ⋕[T, dt] K2. #L1 #L2 #U #dt * #HL12 #IH #K1 #K2 #d #e #HLK1 #HLK2 #T #HTU #Hdtd lapply (ldrop_fwd_length_minus2 … HLK1) lapply (ldrop_fwd_length_minus2 … HLK2) @@ -89,8 +89,8 @@ lapply (cpys_lift_be … HT0 … HLKA … HTU … HTU0) // -HT0 qed-. lemma lleq_inv_lift_ge: ∀L1,L2,U,dt. L1 ⋕[U, dt] L2 → - ∀K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 → - ∀T. ⇧[d, e] T ≡ U → d+e ≤ dt → K1 ⋕[T, dt-e] K2. + ∀K1,K2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 → + ∀T. ⇧[d, e] T ≡ U → yinj d + e ≤ dt → K1 ⋕[T, dt-e] K2. #L1 #L2 #U #dt * #HL12 #IH #K1 #K2 #d #e #HLK1 #HLK2 #T #HTU #Hdedt lapply (ldrop_fwd_length_minus2 … HLK1) lapply (ldrop_fwd_length_minus2 … HLK2) #H2 #H1 @conj // -HL12 -H1 -H2 @@ -105,8 +105,8 @@ lapply (cpys_lift_ge … HT0 … HLKA … HTU … HTU0) // -HT0 -Hddt qed-. lemma lleq_inv_lift_be: ∀L1,L2,U,dt. L1 ⋕[U, dt] L2 → - ∀K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 → - ∀T. ⇧[d, e] T ≡ U → d ≤ dt → dt ≤ d + e → K1 ⋕[T, d] K2. + ∀K1,K2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 → + ∀T. ⇧[d, e] T ≡ U → d ≤ dt → dt ≤ yinj d + e → K1 ⋕[T, d] K2. #L1 #L2 #U #dt * #HL12 #IH #K1 #K2 #d #e #HLK1 #HLK2 #T #HTU #Hddt #Hdtde lapply (ldrop_fwd_length_minus2 … HLK1) lapply (ldrop_fwd_length_minus2 … HLK2) #H2 #H1 @conj // -HL12 -H1 -H2 diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma index 97f2dd675..01e08e9f9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma @@ -20,8 +20,8 @@ include "basic_2/substitution/lleq_ldrop.ma". lemma lleq_fwd_lref: ∀L1,L2. ∀d:ynat. ∀i:nat. L1 ⋕[#i, d] L2 → ∨∨ |L1| ≤ i ∧ |L2| ≤ i | yinj i < d - | ∃∃I1,I2,K1,K2,V. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V & - ⇩[0, i] L2 ≡ K2.ⓑ{I2}V & + | ∃∃I1,I2,K1,K2,V. ⇩[i] L1 ≡ K1.ⓑ{I1}V & + ⇩[i] L2 ≡ K2.ⓑ{I2}V & K1 ⋕[V, yinj 0] K2 & d ≤ yinj i. #L1 #L2 #d #i * #HL12 #IH elim (lt_or_ge i (|L1|)) /3 width=3 by or3_intro0, conj/ elim (ylt_split i d) /2 width=1 by or3_intro1/ #Hdi #Hi @@ -46,9 +46,9 @@ lapply (cpys_antisym_eq … H12 … H21) -H12 -H21 #H destruct qed-. lemma lleq_fwd_lref_dx: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → - ∀I2,K2,V. ⇩[0, i] L2 ≡ K2.ⓑ{I2}V → + ∀I2,K2,V. ⇩[i] L2 ≡ K2.ⓑ{I2}V → i < d ∨ - ∃∃I1,K1. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V & K1 ⋕[V, 0] K2 & d ≤ i. + ∃∃I1,K1. ⇩[i] L1 ≡ K1.ⓑ{I1}V & K1 ⋕[V, 0] K2 & d ≤ i. #L1 #L2 #d #i #H #I2 #K2 #V #HLK2 elim (lleq_fwd_lref … H) -H [ * || * ] [ #_ #H elim (lt_refl_false i) lapply (ldrop_fwd_length_lt2 … HLK2) -HLK2 @@ -60,9 +60,9 @@ lemma lleq_fwd_lref_dx: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → qed-. lemma lleq_fwd_lref_sn: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → - ∀I1,K1,V. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V → + ∀I1,K1,V. ⇩[i] L1 ≡ K1.ⓑ{I1}V → i < d ∨ - ∃∃I2,K2. ⇩[0, i] L2 ≡ K2.ⓑ{I2}V & K1 ⋕[V, 0] K2 & d ≤ i. + ∃∃I2,K2. ⇩[i] L2 ≡ K2.ⓑ{I2}V & K1 ⋕[V, 0] K2 & d ≤ i. #L1 #L2 #d #i #HL12 #I1 #K1 #V #HLK1 elim (lleq_fwd_lref_dx L2 … d … HLK1) -HLK1 [2: * ] /4 width=6 by lleq_sym, ex3_2_intro, or_introl, or_intror/ qed-. @@ -70,8 +70,8 @@ qed-. (* Advanced inversion lemmas ************************************************) lemma lleq_inv_lref_ge_dx: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → d ≤ i → - ∀I2,K2,V. ⇩[0, i] L2 ≡ K2.ⓑ{I2}V → - ∃∃I1,K1. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V & K1 ⋕[V, 0] K2. + ∀I2,K2,V. ⇩[i] L2 ≡ K2.ⓑ{I2}V → + ∃∃I1,K1. ⇩[i] L1 ≡ K1.ⓑ{I1}V & K1 ⋕[V, 0] K2. #L1 #L2 #d #i #H #Hdi #I2 #K2 #V #HLK2 elim (lleq_fwd_lref_dx … H … HLK2) -L2 [ #H elim (ylt_yle_false … H Hdi) | * /2 width=4 by ex2_2_intro/ @@ -79,8 +79,8 @@ lemma lleq_inv_lref_ge_dx: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → d ≤ i → qed-. lemma lleq_inv_lref_ge_sn: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → d ≤ i → - ∀I1,K1,V. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V → - ∃∃I2,K2. ⇩[0, i] L2 ≡ K2.ⓑ{I2}V & K1 ⋕[V, 0] K2. + ∀I1,K1,V. ⇩[i] L1 ≡ K1.ⓑ{I1}V → + ∃∃I2,K2. ⇩[i] L2 ≡ K2.ⓑ{I2}V & K1 ⋕[V, 0] K2. #L1 #L2 #d #i #HL12 #Hdi #I1 #K1 #V #HLK1 elim (lleq_inv_lref_ge_dx L2 … Hdi … HLK1) -Hdi -HLK1 /3 width=4 by lleq_sym, ex2_2_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_alt.ma index 3019423b4..6fab6dec6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_alt.ma @@ -47,10 +47,10 @@ lemma lsstasa_step_dx: ∀h,g,G,L,T1,T,l. ⦃G, L⦄ ⊢ T1 ••*[h, g, l] T [ /2 width=1/ | #G #L #l #k #X #H >(ssta_inv_sort1 … H) -X >commutative_plus // | #G #L #K #V #W #U #i #l #HLK #_ #HWU #IHVW #U2 #HU2 - lapply (ldrop_fwd_ldrop2 … HLK) #H + lapply (ldrop_fwd_drop2 … HLK) #H elim (ssta_inv_lift1 … HU2 … H … HWU) -H -U /3 width=6/ | #G #L #K #W #V #U #i #l #l0 #HLK #HWl0 #_ #HVU #IHWV #U2 #HU2 - lapply (ldrop_fwd_ldrop2 … HLK) #H + lapply (ldrop_fwd_drop2 … HLK) #H elim (ssta_inv_lift1 … HU2 … H … HVU) -H -U /3 width=8/ | #a #I #G #L #V #T1 #U1 #l #_ #IHTU1 #X #H elim (ssta_inv_bind1 … H) -H #U #HU1 #H destruct /3 width=1/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_lift.ma index c4c27e9fd..76c9c27f3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_lift.ma @@ -39,7 +39,7 @@ lemma lsstas_inv_lref1: ∀h,g,G,L,U,i,l. ⦃G, L⦄ ⊢ #i •*[h, g, l+1] U #h #g #G #L #U #i #l #H elim (lsstas_inv_step_sn … H) -H #X #H #HXU elim (ssta_inv_lref1 … H) -H * #K [ #V #W | #W #l0 ] #HLK [ #HVW | #HWl0 ] #HWX -lapply (ldrop_fwd_ldrop2 … HLK) #H0LK +lapply (ldrop_fwd_drop2 … HLK) #H0LK elim (lsstas_inv_lift1 … HXU … H0LK … HWX) -H0LK -X /3 width=8/ /4 width=6/ qed-. @@ -66,7 +66,7 @@ lemma lsstas_ldef: ∀h,g,G,L,K,V,i. ⇩[0, i] L ≡ K.ⓓV → ∀W,l. ⦃G, K⦄ ⊢ V •*[h, g, l+1] W → ∀U. ⇧[0, i+1] W ≡ U → ⦃G, L⦄ ⊢ #i •*[h, g, l+1] U. #h #g #G #L #K #V #i #HLK #W #l #HVW #U #HWU -lapply (ldrop_fwd_ldrop2 … HLK) +lapply (ldrop_fwd_drop2 … HLK) elim (lsstas_inv_step_sn … HVW) -HVW #W0 elim (lift_total W0 0 (i+1)) /3 width=11/ qed. @@ -75,7 +75,7 @@ lemma lsstas_ldec: ∀h,g,G,L,K,W,i. ⇩[0, i] L ≡ K.ⓛW → ∀l0. ⦃G, K ∀V,l. ⦃G, K⦄ ⊢ W •*[h, g, l] V → ∀U. ⇧[0, i+1] V ≡ U → ⦃G, L⦄ ⊢ #i •*[h, g, l+1] U. #h #g #G #L #K #W #i #HLK #T #HWT #V #l #HWV #U #HVU -lapply (ldrop_fwd_ldrop2 … HLK) #H +lapply (ldrop_fwd_drop2 … HLK) #H elim (lift_total W 0 (i+1)) /3 width=11/ qed. 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 da58e39aa..d2d8186af 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 @@ -221,7 +221,7 @@ table { [ "fqup ( ⦃?,?,?⦄ ⊃+ ⦃?,?,?⦄ )" "fqup_fqup" * ] } ] - [ { "generic local env. slicing" * } { + [ { "iterated local env. slicing" * } { [ "ldrops ( ⇩*[?,?] ? ≡ ? )" "ldrops_ldrop" + "ldrops_ldrops" * ] } ]