From 62af0cd2bf6623bfeacc7d9436e67c39711648a7 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 9 Jan 2014 15:33:21 +0000 Subject: [PATCH] - ynat: some additions - lleq: we are ready to remove the old definition :) --- .../lambdadelta/basic_2/relocation/cpy.ma | 37 ++++++++ .../basic_2/relocation/cpy_lift.ma | 81 +++++++--------- .../lambdadelta/basic_2/substitution/cpys.ma | 17 ++++ .../basic_2/substitution/cpys_lift.ma | 11 +-- .../lambdadelta/basic_2/substitution/lleq.ma | 24 +++++ .../basic_2/substitution/lleq_alt.ma | 78 ++++++++++++++- .../basic_2/substitution/lleq_ldrop.ma | 75 +++++++++++++++ .../basic_2/substitution/lleq_lleq.ma | 95 ++++++++++++++++++- .../lambdadelta/ground_2/ynat/ynat_minus.ma | 3 + 9 files changed, 365 insertions(+), 56 deletions(-) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma index 80688b963..05b77349e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma @@ -103,6 +103,37 @@ lapply (cpy_weak … HT12 0 (d + e) ? ?) -HT12 /2 width=2 by cpy_weak_top/ qed-. +lemma cpy_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 → + ∀T1,d,e. ⇧[d, e] T1 ≡ U1 → + d ≤ dt → d + e ≤ dt + et → + ∃∃T2. ⦃G, L⦄ ⊢ U1 ▶×[d+e, dt+et-(d+e)] U2 & ⇧[d, e] T2 ≡ U2. +#G #L #U1 #U2 #dt #et #H elim H -G -L -U1 -U2 -dt -et +[ * #i #G #L #dt #et #T1 #d #e #H #_ + [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by ex2_intro/ + | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3 by lift_lref_ge_minus, lift_lref_lt, ex2_intro/ + | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by ex2_intro/ + ] +| #I #G #L #K #V #W #i #dt #et #Hdti #Hidet #HLK #HVW #T1 #d #e #H #Hddt #Hdedet + elim (lift_inv_lref2 … H) -H * #Hid #H destruct [ -V -Hidet -Hdedet | -Hdti -Hddt ] + [ elim (ylt_yle_false … Hddt) -Hddt /3 width=3 by yle_ylt_trans, ylt_inj/ + | elim (le_inv_plus_l … Hid) #Hdie #Hei + elim (lift_split … HVW d (i-e+1) ? ? ?) [2,3,4: /2 width=1 by le_S_S, le_S/ ] -Hdie + #T2 #_ >plus_minus // ymax_pre_sn_comm // (**) (* explicit constructor *) + ] +| #a #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #X #d #e #H #Hddt #Hdedet + elim (lift_inv_bind2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct + elim (IHW12 … HVW1) -V1 -IHW12 // + elim (IHU12 … HTU1) -T1 -IHU12 /2 width=1 by yle_succ/ + yplus_SO2 >yplus_succ1 >yplus_succ1 + /3 width=2 by cpy_bind, lift_bind, ex2_intro/ +| #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #X #d #e #H #Hddt #Hdedet + elim (lift_inv_flat2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct + elim (IHW12 … HVW1) -V1 -IHW12 // elim (IHU12 … HTU1) -T1 -IHU12 + /3 width=2 by cpy_flat, lift_flat, ex2_intro/ +] +qed-. + lemma cpy_split_up: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶×[d, e] T2 → ∀i. i ≤ d + e → ∃∃T. ⦃G, L⦄ ⊢ T1 ▶×[d, i-d] T & ⦃G, L⦄ ⊢ T ▶×[i, d+e-i] T2. #G #L #T1 #T2 #d #e #H elim H -G -L -T1 -T2 -d -e @@ -248,6 +279,12 @@ qed-. lemma cpy_inv_refl_O2: ∀G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 ▶×[d, 0] T2 → T1 = T2. /2 width=6 by cpy_inv_refl_O2_aux/ qed-. +lemma cpy_inv_lift1_eq: ∀G,T1,U1,d,e. ⇧[d, e] T1 ≡ U1 → + ∀L,U2. ⦃G, L⦄ ⊢ U1 ▶×[d, e] U2 → U1 = U2. +#G #T1 #U1 #d #e #HTU1 #L #U2 #HU12 elim (cpy_up … HU12 … HTU1) -HU12 -HTU1 +/2 width=4 by cpy_inv_refl_O2/ +qed-. + (* Basic forward lemmas *****************************************************) lemma cpy_fwd_tw: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶×[d, e] T2 → ♯{T1} ≤ ♯{T2}. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_lift.ma index 7cb26f477..85203f203 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_lift.ma @@ -17,7 +17,7 @@ include "basic_2/relocation/cpy.ma". (* CONTEXT-SENSITIVE EXTENDED ORDINARY SUBSTITUTION FOR TERMS ***************) -(* Relocation properties ****************************************************) +(* Properties on relocation *************************************************) lemma cpy_lift_le: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶×[dt, et] T2 → ∀L,U1,U2,d,e. ⇩[d, e] L ≡ K → @@ -103,15 +103,17 @@ lemma cpy_lift_ge: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶×[dt, et] T2 → ] qed-. +(* Inversion lemmas on relocation *******************************************) + lemma cpy_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 → dt + et ≤ d → ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶×[dt, et] T2 & ⇧[d, e] T2 ≡ U2. #G #L #U1 #U2 #dt #et #H elim H -G -L -U1 -U2 -dt -et -[ * #G #L #i #dt #et #K #d #e #_ #T1 #H #_ - [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by cpy_atom, lift_sort, ex2_intro/ - | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3 by cpy_atom, lift_lref_ge_minus, lift_lref_lt, ex2_intro/ - | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by cpy_atom, lift_gref, ex2_intro/ +[ * #i #G #L #dt #et #K #d #e #_ #T1 #H #_ + [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by ex2_intro/ + | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3 by lift_lref_ge_minus, lift_lref_lt, ex2_intro/ + | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by ex2_intro/ ] | #I #G #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #d #e #HLK #T1 #H #Hdetd lapply (ylt_yle_trans … Hdetd … Hidet) -Hdetd #Hid @@ -119,14 +121,14 @@ lemma cpy_inv_lift1_le: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 lapply (lift_inv_lref2_lt … H … Hid) -H #H destruct elim (ldrop_conf_lt … HLK … HLKV) -L // #L #U #HKL #_ #HUV elim (lift_trans_le … HUV … HVW) -V // >minus_plus yplus_minus_assoc_inj /3 width=1 by monotonic_ylt_minus_dx, yle_inj/ ] -| #a #I #G #L #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdtd #Hdedet - elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct - elim (IHV12 … HLK … HWV1) -V1 // #W2 #HW12 #HWV2 +| #a #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #d #e #HLK #X #H #Hdtd #Hdedet + elim (lift_inv_bind2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct + elim (IHW12 … HLK … HVW1) -W1 // #V2 #HV12 #HVW2 elim (IHU12 … HTU1) -U1 /3 width=5 by cpy_bind, ldrop_skip, lift_bind, yle_succ, ex2_intro/ -| #I #G #L #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdtd #Hdedet - elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct - elim (IHV12 … HLK … HWV1) -V1 // +| #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #d #e #HLK #X #H #Hdtd #Hdedet + elim (lift_inv_flat2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct + elim (IHW12 … HLK … HVW1) -W1 // elim (IHU12 … HLK … HTU1) -U1 -HLK // /3 width=5 by cpy_flat, lift_flat, ex2_intro/ ] @@ -176,10 +178,10 @@ lemma cpy_inv_lift1_ge: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 d + e ≤ dt → ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶×[dt-e, et] T2 & ⇧[d, e] T2 ≡ U2. #G #L #U1 #U2 #dt #et #H elim H -G -L -U1 -U2 -dt -et -[ * #G #L #i #dt #et #K #d #e #_ #T1 #H #_ - [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by cpy_atom, lift_sort, ex2_intro/ - | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3 by cpy_atom, lift_lref_ge_minus, lift_lref_lt, ex2_intro/ - | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by cpy_atom, lift_gref, ex2_intro/ +[ * #i #G #L #dt #et #K #d #e #_ #T1 #H #_ + [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by ex2_intro/ + | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3 by lift_lref_ge_minus, lift_lref_lt, ex2_intro/ + | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by ex2_intro/ ] | #I #G #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #d #e #HLK #T1 #H #Hdedt lapply (yle_trans … Hdedt … Hdti) #Hdei @@ -193,35 +195,20 @@ lemma cpy_inv_lift1_ge: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 [ /2 width=1 by monotonic_yle_minus_dx/ | yminus_succ1_inj /3 width=5 by cpy_bind, lift_bind, ex2_intro/ -| #I #G #L #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdetd - elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct - elim (IHV12 … HLK … HWV1) -V1 // +| #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #d #e #HLK #X #H #Hdetd + elim (lift_inv_flat2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct + elim (IHW12 … HLK … HVW1) -W1 // elim (IHU12 … HLK … HTU1) -U1 -HLK /3 width=5 by cpy_flat, lift_flat, ex2_intro/ ] qed-. -lemma cpy_inv_lift1_eq: ∀G,T1,U1,d,e. ⇧[d, e] T1 ≡ U1 → - ∀L,U2. ⦃G, L⦄ ⊢ U1 ▶×[d, e] U2 → U1 = U2. -#G #T1 #U1 #d #e #H elim H -T1 -U1 -d -e -[ #k #d #e #L #X #H >(cpy_inv_sort1 … H) -H // -| #i #d #e #Hid #L #X #H elim (cpy_inv_lref1 … H) -H // - * #I #K #V #H elim (ylt_yle_false … H) -H /2 width=1 by ylt_inj/ -| #i #d #e #Hdi #L #X #H elim (cpy_inv_lref1 … H) -H // - * #I #K #V #_ #H elim (ylt_yle_false i d) - /2 width=2 by ylt_inv_monotonic_plus_dx, yle_inj/ -| #p #d #e #L #X #H >(cpy_inv_gref1 … H) -H // -| #a #I #V1 #W1 #T1 #U1 #d #e #_ #_ #IHVW1 #IHTU1 #L #X #H elim (cpy_inv_bind1 … H) -H - #W2 #U2 #HW12 #HU12 #H destruct /3 width=2 by eq_f2/ -| #I #V1 #W1 #T1 #U1 #d #e #_ #_ #IHVW1 #IHTU1 #L #X #H elim (cpy_inv_flat1 … H) -H - #W2 #U2 #HW12 #HU12 #H destruct /3 width=2 by eq_f2/ -] -qed-. +(* Advancd inversion lemmas on relocation ***********************************) lemma cpy_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 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma index 594c34062..885bce344 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma @@ -97,6 +97,17 @@ lemma cpys_weak_full: ∀G,L,T1,T2,d,e. /3 width=5 by cpys_strap1, cpy_weak_full/ qed-. +lemma cpys_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 → + ∀T1,d,e. ⇧[d, e] T1 ≡ U1 → + d ≤ dt → d + e ≤ dt + et → + ∃∃T2. ⦃G, L⦄ ⊢ U1 ▶*×[d+e, dt+et-(d+e)] U2 & ⇧[d, e] T2 ≡ U2. +#G #L #U1 #U2 #dt #et #H #T1 #d #e #HTU1 #Hddt #Hdedet @(cpys_ind … H) -U2 +[ /2 width=3 by ex2_intro/ +| -HTU1 #U #U2 #_ #HU2 * #T #HU1 #HTU + elim (cpy_up … HU2 … HTU) -HU2 -HTU /3 width=3 by cpys_strap1, ex2_intro/ +] +qed-. + lemma cpys_append: ∀G,d,e. l_appendable_sn … (cpys d e G). #G #d #e #K #T1 #T2 #H @(cpys_ind … H) -T2 /3 width=3 by cpys_strap1, cpy_append/ @@ -147,6 +158,12 @@ lemma cpys_inv_refl_O2: ∀G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 ▶*×[d, 0] T2 → T1 #T #T2 #_ #HT2 #IHT1 <(cpy_inv_refl_O2 … HT2) -HT2 // qed-. +lemma cpys_inv_lift1_eq: ∀G,L,U1,U2. ∀d,e:nat. + ⦃G, L⦄ ⊢ U1 ▶*×[d, e] U2 → ∀T1. ⇧[d, e] T1 ≡ U1 → U1 = U2. +#G #L #U1 #U2 #d #e #H #T1 #HTU1 @(cpys_ind … H) -U2 +/2 width=7 by cpy_inv_lift1_eq/ +qed-. + (* Basic forward lemmas *****************************************************) lemma cpys_fwd_tw: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 → ♯{T1} ≤ ♯{T2}. 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 69683612c..c4b9518e6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma @@ -92,7 +92,7 @@ lemma cpys_inv_lref1_ldrop: ∀G,L,T2,i,d,e. ⦃G, L⦄ ⊢ #i ▶*×[d, e] T2 ] qed-. -(* Relocation properties ****************************************************) +(* 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 → @@ -133,6 +133,8 @@ lemma cpys_lift_ge: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*×[dt, et] T2 → ] 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 → dt + et ≤ d → @@ -166,12 +168,7 @@ lemma cpys_inv_lift1_ge: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 ] qed-. -lemma cpys_inv_lift1_eq: ∀G,L,U1,U2. ∀d,e:nat. - ⦃G, L⦄ ⊢ U1 ▶*×[d, e] U2 → ∀T1. ⇧[d, e] T1 ≡ U1 → U1 = U2. -#G #L #U1 #U2 #d #e #H #T1 #HTU1 @(cpys_ind … H) -U2 // -#U #U2 #_ #HU2 #IHU destruct -<(cpy_inv_lift1_eq … HTU1 … HU2) -HU2 -HTU1 // -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 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma index 7e48dbca0..75833e23b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma @@ -27,6 +27,13 @@ interpretation (* Basic properties *********************************************************) +lemma lleq_refl: ∀d,T. reflexive … (lleq d T). +/3 width=1 by conj/ qed. + +lemma lleq_sym: ∀d,T. symmetric … (lleq d T). +#d #T #L1 #L2 * /3 width=1 by iff_sym, conj/ +qed-. + lemma lleq_sort: ∀L1,L2,d,k. |L1| = |L2| → L1 ⋕[⋆k, d] L2. #L1 #L2 #d #k #HL12 @conj // -HL12 #U @conj #H >(cpys_inv_sort1 … H) -H // @@ -60,12 +67,29 @@ elim (IHV W) -IHV elim (IHT U) -IHT /3 width=1 by cpys_flat/ qed. +lemma lleq_be: ∀L1,L2,U,dt. L1 ⋕[U, dt] L2 → ∀T,d,e. ⇧[d, e] T ≡ U → + d ≤ dt → dt ≤ d + e → L1 ⋕[U, d] L2. +#L1 #L2 #U #dt * #HL12 #IH #T #d #e #HTU #Hddt #Hdtde @conj // -HL12 +#U0 elim (IH U0) -IH #H12 #H21 @conj +#HU0 elim (cpys_up … HU0 … HTU) // -HU0 /4 width=5 by cpys_weak/ +qed-. + (* Basic forward lemmas *****************************************************) 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. +#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. +/3 width=6 by lleq_fwd_ldrop_sn, lleq_sym/ qed-. + lemma lleq_fwd_bind_sn: ∀a,I,L1,L2,V,T,d. L1 ⋕[ⓑ{a,I}V.T, d] L2 → L1 ⋕[V, d] L2. #a #I #L1 #L2 #V #T #d * #HL12 #H @conj // -HL12 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 10370818c..c7bb1a8a7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma @@ -13,7 +13,6 @@ (**************************************************************************) include "basic_2/notation/relations/lazyeqalt_4.ma". -include "basic_2/substitution/lleq_ldrop.ma". include "basic_2/substitution/lleq_lleq.ma". inductive lleqa: relation4 ynat term lenv lenv ≝ @@ -53,3 +52,80 @@ theorem lleq_lleqa: ∀L1,T,L2,d. L1 ⋕[T, d] L2 → L1 ⋕⋕[T, d] L2. | #I #V #T #Hn #L2 #d #H elim (lleq_inv_flat … H) -H /3 width=1 by lleqa_flat/ ] qed. + +(* Advanced eliminators *****************************************************) + +lemma lleq_ind_alt: ∀R:relation4 ynat term lenv lenv. ( + ∀L1,L2,d,k. |L1| = |L2| → R d (⋆k) L1 L2 + ) → ( + ∀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 → + 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 + ) → ( + ∀L1,L2,d,p. |L1| = |L2| → R d (§p) L1 L2 + ) → ( + ∀a,I,L1,L2,V,T,d. + L1 ⋕[V, d]L2 → L1.ⓑ{I}V ⋕[T, ⫯d] L2.ⓑ{I}V → + R d V L1 L2 → R (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) → R d (ⓑ{a,I}V.T) L1 L2 + ) → ( + ∀I,L1,L2,V,T,d. + L1 ⋕[V, d]L2 → L1 ⋕[T, d] L2 → + R d V L1 L2 → R d T L1 L2 → R d (ⓕ{I}V.T) L1 L2 + ) → + ∀d,T,L1,L2. L1 ⋕[T, d] L2 → R d T L1 L2. +#R #H1 #H2 #H3 #H4 #H5 #H6 #H7 #d #T #L1 #L2 #H elim (lleq_lleqa … H) -H +/3 width=9 by lleqa_inv_lleq/ +qed-. + +(* Advanced properties ******************************************************) + +lemma lleq_ge: ∀L1,L2,T,d1. L1 ⋕[T, d1] L2 → ∀d2. d1 ≤ d2 → L1 ⋕[T, d2] L2. +#L1 #L2 #T #d1 #H @(lleq_ind_alt … H) -L1 -L2 -T -d1 +/4 width=1 by lleq_sort, lleq_free, lleq_gref, lleq_bind, lleq_flat, yle_succ/ +[ /3 width=3 by lleq_skip, ylt_yle_trans/ +| #I1 #I2 #L1 #L2 #K1 #K2 #V #d1 #i #Hi #HLK1 #HLK2 #HV #IHV #d2 #Hd12 elim (ylt_split i d2) + [ lapply (lleq_fwd_length … HV) #HK12 #Hid2 + lapply (ldrop_fwd_length … HLK1) lapply (ldrop_fwd_length … HLK2) + normalize in ⊢ (%→%→?); -I1 -I2 -V -d1 /2 width=1 by lleq_skip/ + | /3 width=8 by lleq_lref, yle_trans/ + ] +] +qed-. + +lemma lleq_bind_O: ∀a,I,L1,L2,V,T. L1 ⋕[V, 0] L2 → L1.ⓑ{I}V ⋕[T, 0] L2.ⓑ{I}V → + L1 ⋕[ⓑ{a,I}V.T, 0] L2. +/3 width=3 by lleq_ge, lleq_bind/ qed. + +(* 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 ⋕[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/ +[ #L1 #L2 #d0 #i #HL12 #Hid #d #H #K1 #K2 #I #V #HLK1 #HLK2 #HV destruct + elim (yle_split_eq i d) /2 width=1 by lleq_skip, ylt_fwd_succ2/ -HL12 -Hid + #H destruct /2 width=8 by lleq_lref/ +| #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/ +| #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 ⋕[V, 0] K2 → L1 ⋕[T, d] L2. +/2 width=7 by lleq_inv_S_aux/ qed-. + +lemma lleq_inv_bind_O: ∀a,I,L1,L2,V,T. L1 ⋕[ⓑ{a,I}V.T, 0] L2 → + L1 ⋕[V, 0] L2 ∧ L1.ⓑ{I}V ⋕[T, 0] L2.ⓑ{I}V. +#a #I #L1 #L2 #V #T #H elim (lleq_inv_bind … H) -H +/3 width=7 by ldrop_pair, conj, lleq_inv_S/ +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 69c0f84b1..126da3dd3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ldrop.ma @@ -46,3 +46,78 @@ lemma lleq_free: ∀L1,L2,d,i. |L1| ≤ i → |L2| ≤ i → |L1| = |L2| → L1 #I #Z #Y #X #_ #_ #H lapply (ldrop_fwd_length_lt2 … H) -H #H elim (lt_refl_false i) /2 width=3 by lt_to_le_to_lt/ 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 → + ∀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/ +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 → + ∀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/ +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 → + ∀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) +#H2 #H1 @conj // -HL12 -H1 -H2 +#T0 elim (lift_total T0 d e) +#U0 #HTU0 elim (IH U0) -IH +#H12 #H21 @conj #HT0 +[ letin HLKA ≝ HLK1 letin HLKB ≝ HLK2 letin H0 ≝ H12 | letin HLKA ≝ HLK2 letin HLKB ≝ HLK1 letin H0 ≝ H21 ] +lapply (cpys_lift_be … HT0 … HLKA … HTU … HTU0) // -HT0 +>yplus_Y1 #HU0 elim (cpys_inv_lift1_be … (H0 HU0) … HLKB … HTU) // -L1 -L2 -U -Hdtd +#X #HT0 #HX lapply (lift_inj … HX … HTU0) -U0 // +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. +#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 +elim (yle_inv_plus_inj2 … Hdedt) #Hddt #Hedt +#T0 elim (lift_total T0 d e) +#U0 #HTU0 elim (IH U0) -IH +#H12 #H21 @conj #HT0 +[ letin HLKA ≝ HLK1 letin HLKB ≝ HLK2 letin H0 ≝ H12 | letin HLKA ≝ HLK2 letin HLKB ≝ HLK1 letin H0 ≝ H21 ] +lapply (cpys_lift_ge … HT0 … HLKA … HTU … HTU0) // -HT0 -Hddt +>ymax_pre_sn // #HU0 elim (cpys_inv_lift1_ge … (H0 HU0) … HLKB … HTU) // -L1 -L2 -U -Hdedt -Hedt +#X #HT0 #HX lapply (lift_inj … HX … HTU0) -U0 // +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. +#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 +#T0 elim (lift_total T0 d e) +#U0 #HTU0 elim (IH U0) -IH +#H12 #H21 @conj #HT0 +[ letin HLKA ≝ HLK1 letin HLKB ≝ HLK2 letin H0 ≝ H12 | letin HLKA ≝ HLK2 letin HLKB ≝ HLK1 letin H0 ≝ H21 ] +lapply (cpys_lift_ge … HT0 … HLKA … HTU … HTU0) // -HT0 +#HU0 lapply (cpys_weak … HU0 dt (∞) ? ?) // -HU0 +#HU0 lapply (H0 HU0) +#HU0 lapply (cpys_weak … HU0 d (∞) ? ?) // -HU0 +#HU0 elim (cpys_inv_lift1_ge_up … HU0 … HLKB … HTU) // -L1 -L2 -U -Hddt -Hdtde +#X #HT0 #HX lapply (lift_inj … HX … HTU0) -U0 // +qed-. 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 7405011e0..0694be69c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/substitution/cpys_cpys.ma". -include "basic_2/substitution/lleq.ma". +include "basic_2/substitution/lleq_ldrop.ma". (* Advanced forward lemmas **************************************************) @@ -44,3 +44,96 @@ lapply (cpys_antisym_eq … H12 … H21) -H12 -H21 #H destruct | elim (cpys_inv_lref1_ldrop … (H21 ?) … HLK1 … HVW) -H21 -H12 ] [1,3: >yminus_Y_inj ] /3 width=7 by cpys_subst_Y2, yle_inj/ qed-. + +lemma lleq_fwd_lref_dx: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → + ∀I2,K2,V. ⇩[0, i] L2 ≡ K2.ⓑ{I2}V → + i < d ∨ + ∃∃I1,K1. ⇩[0, 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 + /2 width=3 by lt_to_le_to_lt/ (**) (* full auto too slow *) +| /2 width=1 by or_introl/ +| #I1 #I2 #K11 #K22 #V0 #HLK11 #HLK22 #HV0 #Hdi lapply (ldrop_mono … HLK22 … HLK2) -L2 + #H destruct /3 width=5 by ex3_2_intro, or_intror/ +] +qed-. + +lemma lleq_fwd_lref_sn: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → + ∀I1,K1,V. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V → + i < d ∨ + ∃∃I2,K2. ⇩[0, 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-. + +(* 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. +#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/ +] +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. +#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-. + +(* Advanced properties ******************************************************) + +lemma lleq_dec: ∀T,L1,L2,d. Decidable (L1 ⋕[T, d] L2). +#T #L1 @(f2_ind … rfw … L1 T) -L1 -T +#n #IH #L1 * * +[ #k #Hn #L2 elim (eq_nat_dec (|L1|) (|L2|)) /3 width=1 by or_introl, lleq_sort/ +| #i #Hn #L2 elim (eq_nat_dec (|L1|) (|L2|)) + [ #HL12 #d elim (ylt_split i d) /3 width=1 by lleq_skip, or_introl/ + #Hdi elim (lt_or_ge i (|L1|)) #HiL1 + elim (lt_or_ge i (|L2|)) #HiL2 /3 width=1 by or_introl, lleq_free/ + elim (ldrop_O1_lt … HiL2) #I2 #K2 #V2 #HLK2 + elim (ldrop_O1_lt … HiL1) #I1 #K1 #V1 #HLK1 + elim (eq_term_dec V2 V1) + [ #H3 elim (IH K1 V1 … K2 0) destruct + /3 width=8 by lleq_lref, ldrop_fwd_rfw, or_introl/ + ] + -IH #H3 @or_intror + #H elim (lleq_fwd_lref … H) -H [1,3,4,6: * ] + [1,3: /3 width=4 by lt_to_le_to_lt, lt_refl_false/ + |5,6: /2 width=4 by ylt_yle_false/ + ] + #Z1 #Z2 #Y1 #Y2 #X #HLY1 #HLY2 #HX #_ + lapply (ldrop_mono … HLY1 … HLK1) -HLY1 -HLK1 + lapply (ldrop_mono … HLY2 … HLK2) -HLY2 -HLK2 + #H2 #H1 destruct /2 width=1 by/ + ] +| #p #Hn #L2 elim (eq_nat_dec (|L1|) (|L2|)) /3 width=1 by or_introl, lleq_gref/ +| #a #I #V #T #Hn #L2 #d destruct + elim (IH L1 V … L2 d) /2 width=1 by/ + elim (IH (L1.ⓑ{I}V) T … (L2.ⓑ{I}V) (d+1)) -IH /3 width=1 by or_introl, lleq_bind/ + #H1 #H2 @or_intror + #H elim (lleq_inv_bind … H) -H /2 width=1 by/ +| #I #V #T #Hn #L2 #d destruct + elim (IH L1 V … L2 d) /2 width=1 by/ + elim (IH L1 T … L2 d) -IH /3 width=1 by or_introl, lleq_flat/ + #H1 #H2 @or_intror + #H elim (lleq_inv_flat … H) -H /2 width=1 by/ +] +-n /4 width=3 by lleq_fwd_length, or_intror/ +qed-. + +(* Main properties **********************************************************) + +theorem lleq_trans: ∀d,T. Transitive … (lleq d T). +#d #T #L1 #L * #HL1 #IH1 #L2 * #HL2 #IH2 /3 width=3 by conj, iff_trans/ +qed-. + +theorem lleq_canc_sn: ∀L,L1,L2,T,d. L ⋕[d, T] L1→ L ⋕[d, T] L2 → L1 ⋕[d, T] L2. +/3 width=3 by lleq_trans, lleq_sym/ qed-. + +theorem lleq_canc_dx: ∀L1,L2,L,T,d. L1 ⋕[d, T] L → L2 ⋕[d, T] L → L1 ⋕[d, T] L2. +/3 width=3 by lleq_trans, lleq_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_minus.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_minus.ma index 10a841cbd..596885cf0 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_minus.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_minus.ma @@ -38,6 +38,9 @@ qed. lemma yminus_O1: ∀x:ynat. 0 - x = 0. * // qed. +lemma yminus_refl: ∀x:ynat. x - x = 0. +* // qed. + lemma yminus_minus_comm: ∀y,z,x. x - y - z = x - z - y. * #y [ * #z [ * // ] ] >yminus_O1 // qed. -- 2.39.2