From 114ab6653242120dca8382327447ac24cb255f42 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 1 Dec 2013 20:57:54 +0000 Subject: [PATCH] - improved arithmetics for natural numbers with infinity - some properties of equivalence for local environments - improved lazy equivalence for local environments - we commit just the "relocation" component --- .../relations/{lazyeq_3.ma => lazyeq_4.ma} | 4 +- .../relocation/{fqu_fqu.ma => fqu_lleq.ma} | 14 +- .../relocation/{fquq_fquq.ma => fquq_lleq.ma} | 8 +- .../lambdadelta/basic_2/relocation/ldrop.ma | 88 ++-- .../basic_2/relocation/ldrop_append.ma | 11 +- .../basic_2/relocation/ldrop_ldrop.ma | 73 +-- .../basic_2/relocation/ldrop_leq.ma | 96 ++++ .../lambdadelta/basic_2/relocation/lleq.ma | 165 ++++--- .../basic_2/relocation/lleq_lleq.ma | 420 +++++++++++++++--- .../notation/functions/predecessor_1.ma | 4 +- .../notation/functions/successor_1.ma | 4 +- .../lambdadelta/ground_2/ynat/ynat_le.ma | 15 + .../lambdadelta/ground_2/ynat/ynat_lt.ma | 17 +- .../lambdadelta/ground_2/ynat/ynat_minus.ma | 61 +++ .../lambdadelta/ground_2/ynat/ynat_plus.ma | 66 ++- 15 files changed, 820 insertions(+), 226 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{lazyeq_3.ma => lazyeq_4.ma} (90%) rename matita/matita/contribs/lambdadelta/basic_2/relocation/{fqu_fqu.ma => fqu_lleq.ma} (83%) rename matita/matita/contribs/lambdadelta/basic_2/relocation/{fquq_fquq.ma => fquq_lleq.ma} (89%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_minus.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_4.ma similarity index 90% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_3.ma rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_4.ma index acae727a4..ade7b790b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_3.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_4.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( L1 ⋕ break [ term 46 T ] break term 46 L2 )" +notation "hvbox( L1 ⋕ break [ term 46 d , break term 46 T ] break term 46 L2 )" non associative with precedence 45 - for @{ 'LazyEq $T $L1 $L2 }. + for @{ 'LazyEq $d $T $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fqu_fqu.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fqu_lleq.ma similarity index 83% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/fqu_fqu.ma rename to matita/matita/contribs/lambdadelta/basic_2/relocation/fqu_lleq.ma index cbcaa4943..530f4dfa5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fqu_fqu.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/fqu_lleq.ma @@ -17,13 +17,13 @@ include "basic_2/relocation/fqu.ma". (* SUPCLOSURE ***************************************************************) -(* Advanced properties ******************************************************) +(* Properties on lazy equivalence for local environments ********************) lemma lleq_fqu_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃ ⦃G2, K2, U⦄ → - ∀L1. L1 ⋕[T] L2 → - ∃∃K1. ⦃G1, L1, T⦄ ⊃ ⦃G2, K1, U⦄ & K1 ⋕[U] K2. + ∀L1. L1 ⋕[0, T] L2 → + ∃∃K1. ⦃G1, L1, T⦄ ⊃ ⦃G2, K1, U⦄ & K1 ⋕[0, U] K2. #G1 #G2 #L2 #K2 #T #U #H elim H -G1 -G2 -L2 -K2 -T -U -[ #I #G #L2 #V #L1 #H elim (lleq_inv_lref_dx … H I L2 V) -H // +[ #I #G #L2 #V #L1 #H elim (lleq_inv_lref_ge_dx … H … I L2 V) -H // #K1 #H1 #H2 lapply (ldrop_inv_O2 … H1) -H1 #H destruct /2 width=3 by fqu_lref_O, ex2_intro/ | * [ #a ] #I #G #L2 #V #T #L1 #H @@ -31,13 +31,13 @@ lemma lleq_fqu_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃ ⦃G2, K2, U⦄ | elim (lleq_inv_flat … H) ] -H /2 width=3 by fqu_pair_sn, ex2_intro/ -| #a #I #G #L2 #V #T #L1 #H elim (lleq_inv_bind … H) -H - /2 width=3 by fqu_bind_dx, ex2_intro/ +| #a #I #G #L2 #V #T #L1 #H elim (lleq_inv_bind_O … H) -H + #H3 #H4 /2 width=3 by fqu_bind_dx, ex2_intro/ | #I #G #L2 #V #T #L1 #H elim (lleq_inv_flat … H) -H /2 width=3 by fqu_flat_dx, ex2_intro/ | #G #L2 #K2 #T #U #e #HLK2 #HTU #L1 #HL12 elim (ldrop_O1_le (e+1) L1) - [ /3 width=11 by fqu_drop, lleq_inv_lift, ex2_intro/ + [ /3 width=12 by fqu_drop, lleq_inv_lift_le, ex2_intro/ | lapply (ldrop_fwd_length_le2 … HLK2) -K2 lapply (lleq_fwd_length … HL12) -T -U // ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_fquq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_lleq.ma similarity index 89% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_fquq.ma rename to matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_lleq.ma index d7152d1ce..b4d814649 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_fquq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_lleq.ma @@ -12,16 +12,16 @@ (* *) (**************************************************************************) -include "basic_2/relocation/fqu_fqu.ma". +include "basic_2/relocation/fqu_lleq.ma". include "basic_2/relocation/fquq_alt.ma". (* OPTIONAL SUPCLOSURE ******************************************************) -(* Advanced properties ******************************************************) +(* Properties on lazy equivalence for local environments ********************) lemma lleq_fquq_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃⸮ ⦃G2, K2, U⦄ → - ∀L1. L1 ⋕[T] L2 → - ∃∃K1. ⦃G1, L1, T⦄ ⊃⸮ ⦃G2, K1, U⦄ & K1 ⋕[U] K2. + ∀L1. L1 ⋕[0, T] L2 → + ∃∃K1. ⦃G1, L1, T⦄ ⊃⸮ ⦃G2, K1, U⦄ & K1 ⋕[0, U] K2. #G1 #G2 #L2 #K2 #T #U #H #L1 #HL12 elim(fquq_inv_gen … H) -H [ #H elim (lleq_fqu_trans … H … HL12) -L2 /3 width=3 by fqu_fquq, ex2_intro/ | * #HG #HL #HT destruct /2 width=3 by ex2_intro/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma index 68b23637c..ee4780d88 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma @@ -18,7 +18,7 @@ include "basic_2/grammar/lenv_length.ma". include "basic_2/grammar/cl_restricted_weight.ma". include "basic_2/relocation/lift.ma". -(* LOCAL ENVIRONMENT SLICING ************************************************) +(* BASIC SLICING FOR LOCAL ENVIRONMENTS *************************************) (* Basic_1: includes: drop_skip_bind *) inductive ldrop: relation4 nat nat lenv lenv ≝ @@ -30,7 +30,9 @@ inductive ldrop: relation4 nat nat lenv lenv ≝ ldrop (d + 1) e (L1. ⓑ{I} V1) (L2. ⓑ{I} V2) . -interpretation "local slicing" 'RDrop d e L1 L2 = (ldrop d e L1 L2). +interpretation + "basic slicing (local environment)" + 'RDrop d e L1 L2 = (ldrop d e L1 L2). definition l_liftable: predicate (lenv → relation term) ≝ λR. ∀K,T1,T2. R K T1 T2 → ∀L,d,e. ⇩[d, e] L ≡ K → @@ -58,7 +60,7 @@ definition dropable_dx: predicate (relation lenv) ≝ fact ldrop_inv_atom1_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → L1 = ⋆ → L2 = ⋆ ∧ e = 0. #d #e #L1 #L2 * -d -e -L1 -L2 -[ /2 width=1/ +[ /2 width=1 by conj/ | #L #I #V #H destruct | #L1 #L2 #I #V #e #_ #H destruct | #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H destruct @@ -75,8 +77,8 @@ fact ldrop_inv_O1_pair1_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → d = 0 → (0 < e ∧ ⇩[d, e - 1] K ≡ L2). #d #e #L1 #L2 * -d -e -L1 -L2 [ #d #_ #K #I #V #H destruct -| #L #I #V #_ #K #J #W #HX destruct /3 width=1/ -| #L1 #L2 #I #V #e #HL12 #_ #K #J #W #H destruct /3 width=1/ +| #L #I #V #_ #K #J #W #HX destruct /3 width=1 by or_introl, conj/ +| #L1 #L2 #I #V #e #HL12 #_ #K #J #W #H destruct /3 width=1 by or_intror, conj/ | #L1 #L2 #I #V1 #V2 #d #e #_ #_ >commutative_plus normalize #H destruct ] qed-. @@ -93,13 +95,18 @@ elim (lt_refl_false … H) qed-. (* Basic_1: was: drop_gen_drop *) -lemma ldrop_inv_ldrop1: ∀e,K,I,V,L2. - ⇩[0, e] K. ⓑ{I} V ≡ L2 → 0 < e → ⇩[0, e - 1] K ≡ L2. +lemma ldrop_inv_ldrop1_lt: ∀e,K,I,V,L2. + ⇩[0, e] K. ⓑ{I} V ≡ L2 → 0 < e → ⇩[0, e - 1] K ≡ L2. #e #K #I #V #L2 #H #He elim (ldrop_inv_O1_pair1 … H) -H * // #H destruct elim (lt_refl_false … He) qed-. +lemma ldrop_inv_ldrop1: ∀e,K,I,V,L2. + ⇩[0, e+1] K. ⓑ{I} V ≡ L2 → ⇩[0, e] K ≡ L2. +#e #K #I #V #L2 #H lapply (ldrop_inv_ldrop1_lt … H ?) -H // +qed-. + fact ldrop_inv_skip1_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → 0 < d → ∀I,K1,V1. L1 = K1. ⓑ{I} V1 → ∃∃K2,V2. ⇩[d - 1, e] K1 ≡ K2 & @@ -109,7 +116,7 @@ fact ldrop_inv_skip1_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → 0 < d → [ #d #_ #I #K #V #H destruct | #L #I #V #H elim (lt_refl_false … H) | #L1 #L2 #I #V #e #_ #H elim (lt_refl_false … H) -| #X #L2 #Y #Z #V2 #d #e #HL12 #HV12 #_ #I #L1 #V1 #H destruct /2 width=5/ +| #X #L2 #Y #Z #V2 #d #e #HL12 #HV12 #_ #I #L1 #V1 #H destruct /2 width=5 by ex3_2_intro/ ] qed-. @@ -127,7 +134,7 @@ lemma ldrop_inv_O1_pair2: ∀I,K,V,e,L1. ⇩[0, e] L1 ≡ K. ⓑ{I} V → [ #H elim (ldrop_inv_atom1 … H) -H #H destruct | #L1 #I1 #V1 #H elim (ldrop_inv_O1_pair1 … H) -H * - [ #H1 #H2 destruct /3 width=1/ + [ #H1 #H2 destruct /3 width=1 by or_introl, conj/ | /3 width=5/ ] ] @@ -142,7 +149,7 @@ fact ldrop_inv_skip2_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → 0 < d → [ #d #_ #I #K #V #H destruct | #L #I #V #H elim (lt_refl_false … H) | #L1 #L2 #I #V #e #_ #H elim (lt_refl_false … H) -| #L1 #X #Y #V1 #Z #d #e #HL12 #HV12 #_ #I #L2 #V2 #H destruct /2 width=5/ +| #L1 #X #Y #V1 #Z #d #e #HL12 #HV12 #_ #I #L2 #V2 #H destruct /2 width=5 by ex3_2_intro/ ] qed-. @@ -157,18 +164,18 @@ lemma ldrop_inv_skip2: ∀d,e,I,L1,K2,V2. ⇩[d, e] L1 ≡ K2. ⓑ{I} V2 → 0 < (* Basic_1: was by definition: drop_refl *) lemma ldrop_refl: ∀L,d. ⇩[d, 0] L ≡ L. #L elim L -L // -#L #I #V #IHL #d @(nat_ind_plus … d) -d // /2 width=1/ +#L #I #V #IHL #d @(nat_ind_plus … d) -d /2 width=1 by ldrop_pair, ldrop_skip/ qed. lemma ldrop_ldrop_lt: ∀L1,L2,I,V,e. ⇩[0, e - 1] L1 ≡ L2 → 0 < e → ⇩[0, e] L1. ⓑ{I} V ≡ L2. -#L1 #L2 #I #V #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/ +#L1 #L2 #I #V #e #HL12 #He >(plus_minus_m_m e 1) /2 width=1 by ldrop_ldrop/ qed. lemma ldrop_skip_lt: ∀L1,L2,I,V1,V2,d,e. ⇩[d - 1, e] L1 ≡ L2 → ⇧[d - 1, e] V2 ≡ V1 → 0 < d → ⇩[d, e] L1. ⓑ{I} V1 ≡ L2. ⓑ{I} V2. -#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV21 #Hd >(plus_minus_m_m d 1) // /2 width=1/ +#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV21 #Hd >(plus_minus_m_m d 1) /2 width=1 by ldrop_skip/ qed. lemma ldrop_O1_le: ∀e,L. e ≤ |L| → ∃K. ⇩[0, e] L ≡ K. @@ -176,16 +183,16 @@ lemma ldrop_O1_le: ∀e,L. e ≤ |L| → ∃K. ⇩[0, e] L ≡ K. #e #IHe * [ #H lapply (le_n_O_to_eq … H) -H >commutative_plus normalize #H destruct | #L #I #V normalize #H - elim (IHe L) -IHe /2 width=1/ -H /3 width=2/ + elim (IHe L) -IHe /2 width=1/ -H /3 width=2 by ldrop_ldrop, ex_intro/ ] qed. lemma ldrop_O1_lt: ∀L,e. e < |L| → ∃∃I,K,V. ⇩[0, e] L ≡ K.ⓑ{I}V. #L elim L -L [ #e #H elim (lt_zero_false … H) -| #L #I #V #IHL #e @(nat_ind_plus … e) -e /2 width=4/ +| #L #I #V #IHL #e @(nat_ind_plus … e) -e /2 width=4 by ldrop_pair, ex1_3_intro/ #e #_ normalize #H - elim (IHL e) -IHL /2 width=1/ -H /3 width=4/ + elim (IHL e) -IHL /3 width=4 by ldrop_ldrop, lt_plus_to_minus_r, lt_plus_to_lt_l, ex1_3_intro/ ] qed. @@ -193,55 +200,55 @@ lemma l_liftable_LTC: ∀R. l_liftable R → l_liftable (LTC … R). #R #HR #K #T1 #T2 #H elim H -T2 [ /3 width=9/ | #T #T2 #_ #HT2 #IHT1 #L #d #e #HLK #U1 #HTU1 #U2 #HTU2 - elim (lift_total T d e) /4 width=11 by step/ (**) (* auto too slow without trace *) + elim (lift_total T d e) /4 width=11 by step/ ] qed. lemma l_deliftable_sn_LTC: ∀R. l_deliftable_sn R → l_deliftable_sn (LTC … R). #R #HR #L #U1 #U2 #H elim H -U2 [ #U2 #HU12 #K #d #e #HLK #T1 #HTU1 - elim (HR … HU12 … HLK … HTU1) -HR -L -U1 /3 width=3/ + elim (HR … HU12 … HLK … HTU1) -HR -L -U1 /3 width=3 by inj, ex2_intro/ | #U #U2 #_ #HU2 #IHU1 #K #d #e #HLK #T1 #HTU1 elim (IHU1 … HLK … HTU1) -IHU1 -U1 #T #HTU #HT1 - elim (HR … HU2 … HLK … HTU) -HR -L -U /3 width=5/ + elim (HR … HU2 … HLK … HTU) -HR -L -U /3 width=5 by step, ex2_intro/ ] qed. lemma dropable_sn_TC: ∀R. dropable_sn R → dropable_sn (TC … R). #R #HR #L1 #K1 #d #e #HLK1 #L2 #H elim H -L2 [ #L2 #HL12 - elim (HR … HLK1 … HL12) -HR -L1 /3 width=3/ + elim (HR … HLK1 … HL12) -HR -L1 /3 width=3 by inj, ex2_intro/ | #L #L2 #_ #HL2 * #K #HK1 #HLK - elim (HR … HLK … HL2) -HR -L /3 width=3/ + elim (HR … HLK … HL2) -HR -L /3 width=3 by step, ex2_intro/ ] qed. lemma dedropable_sn_TC: ∀R. dedropable_sn R → dedropable_sn (TC … R). #R #HR #L1 #K1 #d #e #HLK1 #K2 #H elim H -K2 [ #K2 #HK12 - elim (HR … HLK1 … HK12) -HR -K1 /3 width=3/ + elim (HR … HLK1 … HK12) -HR -K1 /3 width=3 by inj, ex2_intro/ | #K #K2 #_ #HK2 * #L #HL1 #HLK - elim (HR … HLK … HK2) -HR -K /3 width=3/ + elim (HR … HLK … HK2) -HR -K /3 width=3 by step, ex2_intro/ ] qed. lemma dropable_dx_TC: ∀R. dropable_dx R → dropable_dx (TC … R). #R #HR #L1 #L2 #H elim H -L2 [ #L2 #HL12 #K2 #e #HLK2 - elim (HR … HL12 … HLK2) -HR -L2 /3 width=3/ + elim (HR … HL12 … HLK2) -HR -L2 /3 width=3 by inj, ex2_intro/ | #L #L2 #_ #HL2 #IHL1 #K2 #e #HLK2 elim (HR … HL2 … HLK2) -HR -L2 #K #HLK #HK2 - elim (IHL1 … HLK) -L /3 width=5/ + elim (IHL1 … HLK) -L /3 width=5 by step, ex2_intro/ ] qed. lemma l_deliftable_sn_llstar: ∀R. l_deliftable_sn R → ∀l. l_deliftable_sn (llstar … R l). #R #HR #l #L #U1 #U2 #H @(lstar_ind_r … l U2 H) -l -U2 -[ /2 width=3/ +[ /2 width=3 by lstar_O, ex2_intro/ | #l #U #U2 #_ #HU2 #IHU1 #K #d #e #HLK #T1 #HTU1 elim (IHU1 … HLK … HTU1) -IHU1 -U1 #T #HTU #HT1 - elim (HR … HU2 … HLK … HTU) -HR -L -U /3 width=5/ + elim (HR … HU2 … HLK … HTU) -HR -L -U /3 width=5 by lstar_dx, ex2_intro/ ] qed. @@ -255,17 +262,17 @@ lemma ldrop_fwd_ldrop2: ∀L1,I2,K2,V2,e. ⇩[O, e] L1 ≡ K2. ⓑ{I2} V2 → | #K1 #I1 #V1 #IHL1 #I2 #K2 #V2 #e #H elim (ldrop_inv_O1_pair1 … H) -H * #He #H [ -IHL1 destruct /2 width=1/ - | @ldrop_ldrop >(plus_minus_m_m e 1) // /2 width=3/ + | @ldrop_ldrop >(plus_minus_m_m e 1) /2 width=3 by / ] ] qed-. lemma ldrop_fwd_length: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → |L1| = |L2| + e. -#L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize /2 width=1/ +#L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize /2 width=1 by / qed-. lemma ldrop_fwd_length_minus2: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → |L2| = |L1| - e. -#L1 #L2 #d #e #H lapply (ldrop_fwd_length … H) -H /2 width=1/ +#L1 #L2 #d #e #H lapply (ldrop_fwd_length … H) -H /2 width=1 by plus_minus, le_n/ qed-. lemma ldrop_fwd_length_minus4: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → e = |L1| - |L2|. @@ -287,22 +294,29 @@ lapply (ldrop_fwd_length … H) normalize in ⊢ (%→?); -I2 -V2 // qed-. lemma ldrop_fwd_length_lt4: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → 0 < e → |L2| < |L1|. -#L1 #L2 #d #e #H lapply (ldrop_fwd_length … H) -H /2 width=1/ +#L1 #L2 #d #e #H lapply (ldrop_fwd_length … H) -H /2 width=1 by lt_minus_to_plus_r/ qed-. -lemma ldrop_fwd_length_eq: ∀L1,L2,K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 → - |L1| = |L2| → |K1| = |K2|. +lemma ldrop_fwd_length_eq1: ∀L1,L2,K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 → + |L1| = |L2| → |K1| = |K2|. #L1 #L2 #K1 #K2 #d #e #HLK1 #HLK2 #HL12 lapply (ldrop_fwd_length … HLK1) -HLK1 lapply (ldrop_fwd_length … HLK2) -HLK2 -/2 width=2 by injective_plus_r/ (**) (* full auto fails *) +/2 width=2 by injective_plus_r/ +qed-. + +lemma ldrop_fwd_length_eq2: ∀L1,L2,K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 → + |K1| = |K2| → |L1| = |L2|. +#L1 #L2 #K1 #K2 #d #e #HLK1 #HLK2 #HL12 +lapply (ldrop_fwd_length … HLK1) -HLK1 +lapply (ldrop_fwd_length … HLK2) -HLK2 // qed-. lemma ldrop_fwd_lw: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ♯{L2} ≤ ♯{L1}. #L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize -[ /2 width=3/ +[ /2 width=3 by transitive_le/ | #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12 - >(lift_fwd_tw … HV21) -HV21 /2 width=1/ + >(lift_fwd_tw … HV21) -HV21 /2 width=1 by monotonic_le_plus_l/ ] qed-. @@ -313,7 +327,7 @@ lemma ldrop_fwd_lw_lt: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → 0 < e → ♯{L2} < lapply (ldrop_fwd_lw … HL12) -HL12 #HL12 @(le_to_lt_to_lt … HL12) -HL12 // | #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12 #H normalize in ⊢ (?%%); -I - >(lift_fwd_tw … HV21) -V2 /3 by lt_minus_to_plus/ (**) (* auto too slow without trace *) + >(lift_fwd_tw … HV21) -V2 /3 by lt_minus_to_plus/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_append.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_append.ma index 9b49fdd5b..2da9f9ed9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_append.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_append.ma @@ -22,7 +22,8 @@ include "basic_2/relocation/ldrop.ma". fact ldrop_O1_append_sn_le_aux: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → d = 0 → e ≤ |L1| → ∀L. ⇩[0, e] L @@ L1 ≡ L @@ L2. -#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize // /4 width=1/ +#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize +/4 width=1 by ldrop_skip_lt, ldrop_ldrop, arith_b1, lt_minus_to_plus_r, monotonic_pred/ qed-. lemma ldrop_O1_append_sn_le: ∀L1,L2,e. ⇩[0, e] L1 ≡ L2 → e ≤ |L1| → @@ -38,7 +39,7 @@ lemma ldrop_O1_inv_append1_ge: ∀K,L1,L2,e. ⇩[0, e] L1 @@ L2 ≡ K → elim (ldrop_inv_O1_pair1 … H) -H * #H2e #HL12 destruct [ lapply (le_n_O_to_eq … H1e) -H1e -IHL2 >commutative_plus normalize #H destruct -| minus_minus_comm /3 width=1/ +| minus_minus_comm /3 width=1 by monotonic_pred/ ] qed-. @@ -53,11 +54,7 @@ lemma ldrop_O1_inv_append1_le: ∀K,L1,L2,e. ⇩[0, e] L1 @@ L2 ≡ K → e ≤ [ #H1 #_ #K2 #H2 lapply (ldrop_inv_O2 … H1) -H1 #H1 lapply (ldrop_inv_O2 … H2) -H2 #H2 destruct // - | #e #_ #H1 #H #K2 #H2 - lapply (le_plus_to_le_r … H) -H - lapply (ldrop_inv_ldrop1 … H1 ?) -H1 // - lapply (ldrop_inv_ldrop1 … H2 ?) -H2 // - (lift_inj … HVT1 … HVT2) -HVT1 -HVT2 @@ -40,13 +40,13 @@ theorem ldrop_conf_ge: ∀d1,e1,L,L1. ⇩[d1, e1] L ≡ L1 → ⇩[0, e2 - e1] L1 ≡ L2. #d1 #e1 #L #L1 #H elim H -d1 -e1 -L -L1 // [ #L #K #I #V #e #_ #IHLK #e2 #L2 #H #He2 - lapply (ldrop_inv_ldrop1 … H ?) -H /2 width=2/ #HL2 - minus_minus_comm /3 width=1/ + lapply (ldrop_inv_ldrop1_lt … H ?) -H /2 width=2 by ltn_to_ltO/ #HL2 + minus_minus_comm /3 width=1 by monotonic_pred/ | #L #K #I #V1 #V2 #d #e #_ #_ #IHLK #e2 #L2 #H #Hdee2 lapply (transitive_le 1 … Hdee2) // #He2 - lapply (ldrop_inv_ldrop1 … H ?) -H // -He2 #HL2 + lapply (ldrop_inv_ldrop1_lt … H ?) -H // -He2 #HL2 lapply (transitive_le (1 + e) … Hdee2) // #Hee2 - @ldrop_ldrop_lt >minus_minus_comm /3 width=1/ (**) (* explicit constructor *) + @ldrop_ldrop_lt >minus_minus_comm /3 width=1 by O, lt_minus_to_plus_r, monotonic_le_minus_r, monotonic_pred/ (**) (* explicit constructor *) ] qed. @@ -56,21 +56,21 @@ theorem ldrop_conf_be: ∀L0,L1,d1,e1. ⇩[d1, e1] L0 ≡ L1 → ∃∃L. ⇩[0, d1 + e1 - e2] L2 ≡ L & ⇩[0, d1] L1 ≡ L. #L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1 [ #d1 #L2 #e2 #H #Hd1 #_ elim (ldrop_inv_atom1 … H) -H #H1 #H2 destruct - <(le_n_O_to_eq … Hd1) -d1 /2 width=3/ + <(le_n_O_to_eq … Hd1) -d1 /2 width=3 by ldrop_atom, ex2_intro/ | normalize #L #I #V #L2 #e2 #HL2 #_ #He2 lapply (le_n_O_to_eq … He2) -He2 #H destruct - lapply (ldrop_inv_O2 … HL2) -HL2 #H destruct /2 width=3/ + lapply (ldrop_inv_O2 … HL2) -HL2 #H destruct /2 width=3 by ldrop_pair, ex2_intro/ | normalize #L0 #K0 #I #V1 #e1 #HLK0 #IHLK0 #L2 #e2 #H #_ #He21 lapply (ldrop_inv_O1_pair1 … H) -H * * #He2 #HL20 - [ -IHLK0 -He21 destruct plus_plus_comm_23 #_ #_ #IHLK0 #L2 #e2 #H #Hd1e2 #He2de1 elim (le_inv_plus_l … Hd1e2) #_ #He2 minus_le_minus_minus_comm // /3 width=3/ + elim (IHK01 … HK0L2) -IHK01 -HK0L2 /2 width=1 by monotonic_pred/ + >minus_le_minus_minus_comm /3 width=3 by ldrop_ldrop_lt, ex2_intro/ ] ] qed. @@ -104,8 +105,8 @@ theorem ldrop_trans_ge: ∀d1,e1,L1,L. ⇩[d1, e1] L1 ≡ L → | #L1 #L2 #I #V1 #V2 #d #e #H_ #_ #IHL12 #e2 #L #H #Hde2 lapply (lt_to_le_to_lt 0 … Hde2) // #He2 lapply (lt_to_le_to_lt … (e + e2) He2 ?) // #Hee2 - lapply (ldrop_inv_ldrop1 … H ?) -H // #HL2 - @ldrop_ldrop_lt // >le_plus_minus // @IHL12 /2 width=1/ (**) (* explicit constructor *) + lapply (ldrop_inv_ldrop1_lt … H ?) -H // #HL2 + @ldrop_ldrop_lt // >le_plus_minus /3 width=1 by monotonic_pred/ ] qed. @@ -115,18 +116,18 @@ theorem ldrop_trans_le: ∀d1,e1,L1,L. ⇩[d1, e1] L1 ≡ L → ∃∃L0. ⇩[0, e2] L1 ≡ L0 & ⇩[d1 - e2, e1] L0 ≡ L2. #d1 #e1 #L1 #L #H elim H -d1 -e1 -L1 -L [ #d #e2 #L2 #H - elim (ldrop_inv_atom1 … H) -H /2 width=3/ + elim (ldrop_inv_atom1 … H) -H /2 width=3 by ldrop_atom, ex2_intro/ | #K #I #V #e2 #L2 #HL2 #H - lapply (le_n_O_to_eq … H) -H #H destruct /2 width=3/ + lapply (le_n_O_to_eq … H) -H #H destruct /2 width=3 by ldrop_pair, ex2_intro/ | #L1 #L2 #I #V #e #_ #IHL12 #e2 #L #HL2 #H lapply (le_n_O_to_eq … H) -H #H destruct elim (IHL12 … HL2) -IHL12 -HL2 // #L0 #H #HL0 - lapply (ldrop_inv_O2 … H) -H #H destruct /3 width=5/ + lapply (ldrop_inv_O2 … H) -H #H destruct /3 width=5 by ldrop_pair, ldrop_ldrop, ex2_intro/ | #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #IHL12 #e2 #L #H #He2d elim (ldrop_inv_O1_pair1 … H) -H * - [ -He2d -IHL12 #H1 #H2 destruct /3 width=5/ + [ -He2d -IHL12 #H1 #H2 destruct /3 width=5 by ldrop_pair, ldrop_skip, ex2_intro/ | -HL12 -HV12 #He2 #HL2 - elim (IHL12 … HL2) -L2 [ >minus_le_minus_minus_comm // /3 width=3/ | /2 width=1/ ] + elim (IHL12 … HL2) -L2 [ >minus_le_minus_minus_comm // /3 width=3 by ldrop_ldrop_lt, ex2_intro/ | /2 width=1 by monotonic_pred/ ] ] ] qed. @@ -142,7 +143,7 @@ lemma l_liftable_llstar: ∀R. l_liftable R → ∀l. l_liftable (llstar … R l [ #L #d #e #_ #U1 #HTU1 #U2 #HTU2 -HR -K >(lift_mono … HTU2 … HTU1) -T1 -U2 -d -e // | #l #T #T2 #_ #HT2 #IHT1 #L #d #e #HLK #U1 #HTU1 #U2 #HTU2 - elim (lift_total T d e) /3 width=11 by lstar_dx/ (**) (* auto too slow without trace *) + elim (lift_total T d e) /3 width=11 by lstar_dx/ ] qed. @@ -153,8 +154,8 @@ lemma ldrop_conf_lt: ∀d1,e1,L,L1. ⇩[d1, e1] L ≡ L1 → ∃∃K1,V1. ⇩[0, e2] L1 ≡ K1. ⓑ{I} V1 & ⇩[d, e1] K2 ≡ K1 & ⇧[d, e1] V1 ≡ V2. #d1 #e1 #L #L1 #H1 #e2 #K2 #I #V2 #H2 #He2d1 -elim (ldrop_conf_le … H1 … H2) -L [2: /2 width=2/] #K #HL1K #HK2 -elim (ldrop_inv_skip1 … HK2) -HK2 [2: /2 width=1/] #K1 #V1 #HK21 #HV12 #H destruct /2 width=5/ +elim (ldrop_conf_le … H1 … H2) -L /2 width=2 by lt_to_le/ #K #HL1K #HK2 +elim (ldrop_inv_skip1 … HK2) -HK2 /2 width=1 by lt_plus_to_minus_r/ #K1 #V1 #HK21 #HV12 #H destruct /2 width=5 by ex3_2_intro/ qed. (* Note: apparently this was missing in basic_1 *) @@ -164,14 +165,14 @@ lemma ldrop_trans_lt: ∀d1,e1,L1,L. ⇩[d1, e1] L1 ≡ L → ∃∃L0,V0. ⇩[0, e2] L1 ≡ L0.ⓑ{I}V0 & ⇩[d, e1] L0 ≡ L2 & ⇧[d, e1] V2 ≡ V0. #d1 #e1 #L1 #L #HL1 #e2 #L2 #I #V2 #HL2 #Hd21 -elim (ldrop_trans_le … HL1 … HL2) -L [2: /2 width=1/ ] #L0 #HL10 #HL02 -elim (ldrop_inv_skip2 … HL02) -HL02 [2: /2 width=1/ ] #L #V1 #HL2 #HV21 #H destruct /2 width=5/ +elim (ldrop_trans_le … HL1 … HL2) -L /2 width=1 by lt_to_le/ #L0 #HL10 #HL02 +elim (ldrop_inv_skip2 … HL02) -HL02 /2 width=1 by lt_plus_to_minus_r/ #L #V1 #HL2 #HV21 #H destruct /2 width=5 by ex3_2_intro/ qed-. lemma ldrop_trans_ge_comm: ∀d1,e1,e2,L1,L2,L. ⇩[d1, e1] L1 ≡ L → ⇩[0, e2] L ≡ L2 → d1 ≤ e2 → ⇩[0, e2 + e1] L1 ≡ L2. -#e1 #e1 #e2 >commutative_plus /2 width=5/ +#e1 #e1 #e2 >commutative_plus /2 width=5 by ldrop_trans_ge/ qed. lemma ldrop_conf_div: ∀I1,L,K,V1,e1. ⇩[0, e1] L ≡ K. ⓑ{I1} V1 → @@ -187,5 +188,15 @@ elim (discr_minus_x_xy … H) -H [1,3: normalize H in HK; #HK lapply (ldrop_inv_O2 … HK) -HK #H destruct -lapply (inv_eq_minus_O … H) -H /3 width=1/ +lapply (inv_eq_minus_O … H) -H /3 width=1 by le_to_le_to_eq, and3_intro/ +qed-. + +(* Advanced forward lemmas **************************************************) + +lemma ldrop_fwd_be: ∀L,K,d,e,i. ⇩[d, e] L ≡ K → |K| ≤ i → i < d → |L| ≤ i. +#L #K #d #e #i #HLK #HK #Hd elim (lt_or_ge i (|L|)) // +#HL elim (ldrop_O1_lt … HL) #I #K0 #V #HLK0 -HL +elim (ldrop_conf_lt … HLK … HLK0) // -HLK -HLK0 -Hd +#K1 #V1 #HK1 #_ #_ lapply (ldrop_fwd_length_lt2 … HK1) -I -K1 -V1 +#H elim (lt_refl_false i) /2 width=3 by lt_to_le_to_lt/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma new file mode 100644 index 000000000..2c58473a3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma @@ -0,0 +1,96 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground_2/ynat/ynat_plus.ma". +include "basic_2/grammar/leq.ma". +include "basic_2/relocation/ldrop.ma". + +(* BASIC SLICING FOR LOCAL ENVIRONMENTS *************************************) + +lemma ldrop_leq_conf_ge: ∀L1,L2,d,e. L1 ≃[d, e] L2 → + ∀I,K,V,i. ⇩[O, i]L1 ≡ K.ⓑ{I}V → d + e ≤ i → + ⇩[O, i]L2 ≡ K.ⓑ{I}V. +#L1 #L2 #d #e #H elim H -L1 -L2 -d -e +[ #d #e #J #K #W #i #H elim (ldrop_inv_atom1 … H) -H + #H destruct +| #I #L1 #L2 #V #HL12 #IHL12 #J #K #W #i #H #_ elim (ldrop_inv_O1_pair1 … H) -H + * #H1 #H2 + [ -IHL12 lapply (leq_inv_O2 … HL12) -HL12 + #H3 destruct // + | -HL12 /4 width=1 by ldrop_ldrop_lt, yle_inj/ + ] +| #I1 #I2 #L1 #L2 #V1 #V2 #e #_ #IHL12 #J #K #W #i #H1 >yplus_succ_swap + #Hei elim (yle_inv_inj2 … Hei) -Hei + #x #Hei #H elim (yplus_inv_inj … H) -H normalize + #y #z >commutative_plus + #H1 #H2 #H3 destruct elim (le_inv_plus_l … Hei) -Hei + #Hzi #Hi lapply (ldrop_inv_ldrop1_lt … H1 ?) -H1 + /4 width=1 by ldrop_ldrop_lt, yle_inj/ +| #I #L1 #L2 #V #d #e #_ #IHL12 #J #K #W #i #H0 #Hdei elim (yle_inv_inj2 … Hdei) -Hdei + #x #Hdei #H elim (yplus_inv_inj … H) -H + #y #z >commutative_plus + #H1 #H2 #H3 destruct elim (ysucc_inv_inj_dx … H2) -H2 + #x #H1 #H2 destruct elim (le_inv_plus_l … Hdei) + #_ #Hi lapply (ldrop_inv_ldrop1_lt … H0 ?) -H0 + [2: #H0 @ldrop_ldrop_lt ] [2,3: /2 width=3 by lt_to_le_to_lt/ ] + /4 width=3 by yle_inj, monotonic_pred/ +] +qed-. + +lemma ldrop_leq_conf_be: ∀L1,L2,d,e. L1 ≃[d, e] L2 → + ∀I1,K1,V1,i. ⇩[O, i]L1 ≡ K1.ⓑ{I1}V1 → d ≤ i → i < d + e → + ∃∃I2,K2,V2. K1 ≃[0, ⫰(d+e-i)] K2 & ⇩[O, i]L2 ≡ K2.ⓑ{I2}V2. +#L1 #L2 #d #e #H elim H -L1 -L2 -d -e +[ #d #e #J1 #K1 #W1 #i #H elim (ldrop_inv_atom1 … H) -H + #H destruct +| #I #L1 #L2 #V #HL12 #IHL12 #J1 #K1 #W1 #i #_ #_ #H elim (ylt_yle_false … H) // +| #I1 #I2 #L1 #L2 #V1 #V2 #e #HL12 >yplus_O_sn >yplus_O_sn + #IHL12 #J1 #K1 #W1 #i #H #_ elim (eq_or_gt i) #Hi destruct [ -IHL12 | -HL12 ] + [ #_ lapply (ldrop_inv_O2 … H) -H + #H destruct >ypred_succ /2 width=5 by ldrop_pair, ex2_3_intro/ + | lapply (ldrop_inv_ldrop1_lt … H ?) -H // + #H <(ylt_inv_O1 i) /2 width=1 by ylt_inj/ + #Hie lapply (ylt_inv_succ … Hie) -Hie + #Hie elim (IHL12 … H) -IHL12 -H // + >yminus_succ /3 width=5 by ldrop_ldrop_lt, ex2_3_intro/ + ] +| #I #L1 #L2 #V #d #e #_ #IHL12 #J1 #K1 #W1 #i #H #Hdi lapply (ylt_yle_trans 0 … Hdi ?) // + #Hi <(ylt_inv_O1 … Hi) >yplus_succ1 >yminus_succ lapply (yle_fwd_succ1 … Hdi) -Hdi + #Hdi #Hide lapply (ylt_inv_succ … Hide) + #Hide lapply (ylt_inv_inj … Hi) -Hi + #Hi lapply (ldrop_inv_ldrop1_lt … H ?) -H // + #H elim (IHL12 … H) -IHL12 -H + /3 width=5 by ldrop_ldrop_lt, ex2_3_intro/ +] +qed-. + +lemma ldrop_leq_conf_lt: ∀L1,L2,d,e. L1 ≃[d, e] L2 → + ∀I,K1,V,i. ⇩[O, i]L1 ≡ K1.ⓑ{I}V → i < d → + ∃∃K2. K1 ≃[⫰(d-i), e] K2 & ⇩[O, i]L2 ≡ K2.ⓑ{I}V. +#L1 #L2 #d #e #H elim H -L1 -L2 -d -e +[ #d #e #J #K1 #W #i #H elim (ldrop_inv_atom1 … H) -H + #H destruct +| #I #L1 #L2 #V #_ #_ #J #K1 #W #i #_ #H elim (ylt_yle_false … H) // +| #I1 #I2 #L1 #L2 #V1 #V2 #e #_ #_ #J #K1 #W #i #_ #H elim (ylt_yle_false … H) // +| #I #L1 #L2 #V #d #e #HL12 #IHL12 #J #K1 #W #i #H elim (eq_or_gt i) #Hi destruct [ -IHL12 | -HL12 ] + [ #_ lapply (ldrop_inv_O2 … H) -H + #H destruct >ypred_succ /2 width=5 by ldrop_pair, ex2_intro/ + | lapply (ldrop_inv_ldrop1_lt … H ?) -H // + #H <(ylt_inv_O1 i) /2 width=1 by ylt_inj/ + #Hie lapply (ylt_inv_succ … Hie) -Hie + #Hie elim (IHL12 … H) -IHL12 -H + >yminus_succ /3 width=5 by ldrop_ldrop_lt, ex2_intro/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq.ma index f460918a6..407d414de 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq.ma @@ -12,111 +12,148 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/lazyeq_3.ma". +include "basic_2/notation/relations/lazyeq_4.ma". include "basic_2/relocation/ldrop.ma". (* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************) -inductive lleq: term → relation lenv ≝ -| lleq_sort: ∀L1,L2,k. |L1| = |L2| → lleq (⋆k) L1 L2 -| lleq_lref: ∀I,L1,L2,K1,K2,V,i. +inductive lleq: nat → term → relation lenv ≝ +| lleq_sort: ∀L1,L2,d,k. |L1| = |L2| → lleq d (⋆k) L1 L2 +| lleq_skip: ∀I1,I2,L1,L2,K1,K2,V1,V2,d,i. i < d → + ⇩[0, i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[0, i] L2 ≡ K2.ⓑ{I2}V2 → + lleq (d-i-1) V1 K1 K2 → lleq (d-i-1) V2 K1 K2 → lleq d (#i) L1 L2 +| lleq_lref: ∀I,L1,L2,K1,K2,V,d,i. d ≤ i → ⇩[0, i] L1 ≡ K1.ⓑ{I}V → ⇩[0, i] L2 ≡ K2.ⓑ{I}V → - lleq V K1 K2 → lleq (#i) L1 L2 -| lleq_free: ∀L1,L2,i. |L1| ≤ i → |L2| ≤ i → |L1| = |L2| → lleq (#i) L1 L2 -| lleq_gref: ∀L1,L2,p. |L1| = |L2| → lleq (§p) L1 L2 -| lleq_bind: ∀a,I,L1,L2,V,T. - lleq V L1 L2 → lleq T (L1.ⓑ{I}V) (L2.ⓑ{I}V) → - lleq (ⓑ{a,I}V.T) L1 L2 -| lleq_flat: ∀I,L1,L2,V,T. - lleq V L1 L2 → lleq T L1 L2 → lleq (ⓕ{I}V.T) L1 L2 + lleq 0 V K1 K2 → lleq d (#i) L1 L2 +| lleq_free: ∀L1,L2,d,i. |L1| ≤ i → |L2| ≤ i → |L1| = |L2| → lleq d (#i) L1 L2 +| lleq_gref: ∀L1,L2,d,p. |L1| = |L2| → lleq d (§p) L1 L2 +| lleq_bind: ∀a,I,L1,L2,V,T,d. + lleq d V L1 L2 → lleq (d+1) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) → + lleq d (ⓑ{a,I}V.T) L1 L2 +| lleq_flat: ∀I,L1,L2,V,T,d. + lleq d V L1 L2 → lleq d T L1 L2 → lleq d (ⓕ{I}V.T) L1 L2 . interpretation "lazy equivalence (local environment)" - 'LazyEq T L1 L2 = (lleq T L1 L2). + 'LazyEq d T L1 L2 = (lleq d T L1 L2). (* Basic_properties *********************************************************) -lemma lleq_sym: ∀T. symmetric … (lleq T). -#T #L1 #L2 #H elim H -T -L1 -L2 -/2 width=7 by lleq_sort, lleq_lref, lleq_free, lleq_gref, lleq_bind, lleq_flat/ +lemma lleq_sym: ∀d,T. symmetric … (lleq d T). +#d #T #L1 #L2 #H elim H -d -T -L1 -L2 +/2 width=10 by lleq_sort, lleq_skip, lleq_lref, lleq_free, lleq_gref, lleq_bind, lleq_flat/ qed-. -lemma lleq_refl: ∀T. reflexive … (lleq T). -#T #L @(f2_ind … rfw … L T) +(* Note this is: "∀d,T. reflexive … (lleq d T)" *) +axiom lleq_refl: ∀T,L,d. L ⋕[d, T] L. +(* +#T #L @(f2_ind … rfw … L T) -L -T #n #IH #L * * /3 width=1 by lleq_sort, lleq_gref, lleq_bind, lleq_flat/ #i #H elim (lt_or_ge i (|L|)) /2 width=1 by lleq_free/ -#HiL elim (ldrop_O1_lt … HiL) -HiL destruct /4 width=7 by lleq_lref, ldrop_fwd_rfw/ +#HiL #d elim (lt_or_ge i d) /2 width=1 by lleq_skip/ +elim (ldrop_O1_lt … HiL) -HiL destruct /4 width=7 by lleq_lref, ldrop_fwd_rfw/ qed. +*) + +lemma lleq_ge: ∀L1,L2,T,d1. L1 ⋕[d1, T] L2 → ∀d2. d1 ≤ d2 → L1 ⋕[d2, T] L2. +#L1 #L2 #T #d1 #H elim H -L1 -L2 -T -d1 +/4 width=1 by lleq_sort, lleq_free, lleq_gref, lleq_bind, lleq_flat, le_S_S/ +[ /5 width=10 by lleq_skip, lt_to_le_to_lt, monotonic_le_minus_l, monotonic_pred/ (**) (* a bit slow *) +| #I #L1 #L2 #K1 #K2 #V #d1 #i #Hi #HLK1 #HLK2 #HV #IHV #d2 #Hd12 elim (lt_or_ge i d2) + [ -d1 /3 width=10 by lleq_skip/ + | /3 width=7 by lleq_lref, transitive_le/ + ] +] +qed-. (* Basic inversion lemmas ***************************************************) -fact lleq_inv_lref_aux: ∀X,L1,L2. L1 ⋕[X] L2 → ∀i. X = #i → - (|L1| ≤ i ∧ |L2| ≤ i) ∨ - ∃∃I,K1,K2,V. ⇩[0, i] L1 ≡ K1.ⓑ{I}V & - ⇩[0, i] L2 ≡ K2.ⓑ{I}V & - K1 ⋕[V] K2. -#X #L1 #L2 * -X -L1 -L2 -[ #L1 #L2 #k #_ #j #H destruct -| #I #L1 #L2 #K1 #K2 #V #i #HLK1 #HLK2 #HK12 #j #H destruct /3 width=7 by ex3_4_intro, or_intror/ -| #L1 #L2 #i #HL1 #HL2 #_ #j #H destruct /3 width=1 by or_introl, conj/ -| #L1 #L2 #p #_ #j #H destruct -| #a #I #L1 #L2 #V #T #_ #_ #j #H destruct -| #I #L1 #L2 #V #T #_ #_ #j #H destruct +fact lleq_inv_lref_aux: ∀d,X,L1,L2. L1 ⋕[d, X] L2 → ∀i. X = #i → + ∨∨ |L1| ≤ i ∧ |L2| ≤ i + | ∃∃I1,I2,K1,K2,V1,V2. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V1 & + ⇩[0, i] L2 ≡ K2.ⓑ{I2}V2 & + K1 ⋕[d-i-1, V1] K2 & + K1 ⋕[d-i-1, V2] K2 & + i < d + | ∃∃I,K1,K2,V. ⇩[0, i] L1 ≡ K1.ⓑ{I}V & + ⇩[0, i] L2 ≡ K2.ⓑ{I}V & + K1 ⋕[0, V] K2 & d ≤ i. +#d #X #L1 #L2 * -d -X -L1 -L2 +[ #L1 #L2 #d #k #_ #j #H destruct +| #I1 #I2 #L1 #L2 #K1 #K2 #V1 #V2 #d #i #Hid #HLK1 #HLK2 #HV1 #HV2 #j #H destruct /3 width=10 by or3_intro1, ex5_6_intro/ +| #I #L1 #L2 #K1 #K2 #V #d #i #Hdi #HLK1 #HLK2 #HK12 #j #H destruct /3 width=7 by or3_intro2, ex4_4_intro/ +| #L1 #L2 #d #i #HL1 #HL2 #_ #j #H destruct /3 width=1 by or3_intro0, conj/ +| #L1 #L2 #d #p #_ #j #H destruct +| #a #I #L1 #L2 #V #T #d #_ #_ #j #H destruct +| #I #L1 #L2 #V #T #d #_ #_ #j #H destruct ] qed-. -lemma lleq_inv_lref: ∀L1,L2,i. L1 ⋕[#i] L2 → - (|L1| ≤ i ∧ |L2| ≤ i) ∨ - ∃∃I,K1,K2,V. ⇩[0, i] L1 ≡ K1.ⓑ{I}V & - ⇩[0, i] L2 ≡ K2.ⓑ{I}V & - K1 ⋕[V] K2. +lemma lleq_inv_lref: ∀L1,L2,d,i. L1 ⋕[d, #i] L2 → + ∨∨ |L1| ≤ i ∧ |L2| ≤ i + | ∃∃I1,I2,K1,K2,V1,V2. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V1 & + ⇩[0, i] L2 ≡ K2.ⓑ{I2}V2 & + K1 ⋕[d-i-1, V1] K2 & + K1 ⋕[d-i-1, V2] K2 & + i < d + | ∃∃I,K1,K2,V. ⇩[0, i] L1 ≡ K1.ⓑ{I}V & + ⇩[0, i] L2 ≡ K2.ⓑ{I}V & + K1 ⋕[0, V] K2 & d ≤ i. /2 width=3 by lleq_inv_lref_aux/ qed-. -fact lleq_inv_bind_aux: ∀X,L1,L2. L1 ⋕[X] L2 → ∀a,I,V,T. X = ⓑ{a,I}V.T → - L1 ⋕[V] L2 ∧ L1.ⓑ{I}V ⋕[T] L2.ⓑ{I}V. -#X #L1 #L2 * -X -L1 -L2 -[ #L1 #L2 #k #_ #b #J #W #U #H destruct -| #I #L1 #L2 #K1 #K2 #V #i #_ #_ #_ #b #J #W #U #H destruct -| #L1 #L2 #i #_ #_ #_ #b #J #W #U #H destruct -| #L1 #L2 #p #_ #b #J #W #U #H destruct -| #a #I #L1 #L2 #V #T #HV #HT #b #J #W #U #H destruct /2 width=1 by conj/ -| #I #L1 #L2 #V #T #_ #_ #b #J #W #U #H destruct +fact lleq_inv_bind_aux: ∀d,X,L1,L2. L1 ⋕[d,X] L2 → ∀a,I,V,T. X = ⓑ{a,I}V.T → + L1 ⋕[d, V] L2 ∧ L1.ⓑ{I}V ⋕[d+1, T] L2.ⓑ{I}V. +#d #X #L1 #L2 * -d -X -L1 -L2 +[ #L1 #L2 #d #k #_ #b #J #W #U #H destruct +| #I1 #I2 #L1 #L2 #K1 #K2 #V1 #V2 #d #i #_ #_ #_ #_ #_ #b #J #W #U #H destruct +| #I #L1 #L2 #K1 #K2 #V #d #i #_ #_ #_ #_ #b #J #W #U #H destruct +| #L1 #L2 #d #i #_ #_ #_ #b #J #W #U #H destruct +| #L1 #L2 #d #p #_ #b #J #W #U #H destruct +| #a #I #L1 #L2 #V #T #d #HV #HT #b #J #W #U #H destruct /2 width=1 by conj/ +| #I #L1 #L2 #V #T #d #_ #_ #b #J #W #U #H destruct ] qed-. -lemma lleq_inv_bind: ∀a,I,L1,L2,V,T. L1 ⋕[ ⓑ{a,I}V.T] L2 → - L1 ⋕[V] L2 ∧ L1.ⓑ{I}V ⋕[T] L2.ⓑ{I}V. +lemma lleq_inv_bind: ∀a,I,L1,L2,V,T,d. L1 ⋕[d, ⓑ{a,I}V.T] L2 → + L1 ⋕[d, V] L2 ∧ L1.ⓑ{I}V ⋕[d+1, T] L2.ⓑ{I}V. /2 width=4 by lleq_inv_bind_aux/ qed-. -fact lleq_inv_flat_aux: ∀X,L1,L2. L1 ⋕[X] L2 → ∀I,V,T. X = ⓕ{I}V.T → - L1 ⋕[V] L2 ∧ L1 ⋕[T] L2. -#X #L1 #L2 * -X -L1 -L2 -[ #L1 #L2 #k #_ #J #W #U #H destruct -| #I #L1 #L2 #K1 #K2 #V #i #_ #_ #_ #J #W #U #H destruct -| #L1 #L2 #i #_ #_ #_ #J #W #U #H destruct -| #L1 #L2 #p #_ #J #W #U #H destruct -| #a #I #L1 #L2 #V #T #_ #_ #J #W #U #H destruct -| #I #L1 #L2 #V #T #HV #HT #J #W #U #H destruct /2 width=1 by conj/ +fact lleq_inv_flat_aux: ∀d,X,L1,L2. L1 ⋕[d, X] L2 → ∀I,V,T. X = ⓕ{I}V.T → + L1 ⋕[d, V] L2 ∧ L1 ⋕[d, T] L2. +#d #X #L1 #L2 * -d -X -L1 -L2 +[ #L1 #L2 #d #k #_ #J #W #U #H destruct +| #I1 #I2 #L1 #L2 #K1 #K2 #V1 #V2 #d #i #_ #_ #_ #_ #_ #J #W #U #H destruct +| #I #L1 #L2 #K1 #K2 #V #d #i #_ #_ #_ #_ #J #W #U #H destruct +| #L1 #L2 #d #i #_ #_ #_ #J #W #U #H destruct +| #L1 #L2 #d #p #_ #J #W #U #H destruct +| #a #I #L1 #L2 #V #T #d #_ #_ #J #W #U #H destruct +| #I #L1 #L2 #V #T #d #HV #HT #J #W #U #H destruct /2 width=1 by conj/ ] qed-. -lemma lleq_inv_flat: ∀I,L1,L2,V,T. L1 ⋕[ ⓕ{I}V.T] L2 → - L1 ⋕[V] L2 ∧ L1 ⋕[T] L2. +lemma lleq_inv_flat: ∀I,L1,L2,V,T,d. L1 ⋕[d, ⓕ{I}V.T] L2 → + L1 ⋕[d, V] L2 ∧ L1 ⋕[d, T] L2. /2 width=4 by lleq_inv_flat_aux/ qed-. (* Basic forward lemmas *****************************************************) -lemma lleq_fwd_length: ∀L1,L2,T. L1 ⋕[T] L2 → |L1| = |L2|. -#L1 #L2 #T #H elim H -L1 -L2 -T // -#I #L1 #L2 #K1 #K2 #V #i #HLK1 #HLK2 #_ #IHK12 +lemma lleq_fwd_length: ∀L1,L2,T,d. L1 ⋕[d, T] L2 → |L1| = |L2|. +#L1 #L2 #T #d #H elim H -L1 -L2 -T -d // +[ #I1 #I2 #L1 #L2 #K1 #K2 #V1 #V2 #d #i #_ #HLK1 #HLK2 #_ #_ #HK12 #_ +| #I #L1 #L2 #K1 #K2 #V #d #i #_ #HLK1 #HLK2 #_ #IHK12 +] lapply (ldrop_fwd_length … HLK1) -HLK1 lapply (ldrop_fwd_length … HLK2) -HLK2 normalize // qed-. -lemma lleq_fwd_ldrop_sn: ∀L1,L2,T. L1 ⋕[T] L2 → ∀K1,i. ⇩[0, i] L1 ≡ K1 → +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 #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/ (**) (* full auto fails *) +#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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_lleq.ma index 868eaf7da..e12e5ca9c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_lleq.ma @@ -19,113 +19,423 @@ include "basic_2/relocation/lleq.ma". (* Advanced inversion lemmas ************************************************) -lemma lleq_inv_lref_dx: ∀L1,L2,i. L1 ⋕[#i] L2 → +lemma lleq_inv_lref_dx: ∀L1,L2,d,i. L1 ⋕[d, #i] L2 → ∀I,K2,V. ⇩[0, i] L2 ≡ K2.ⓑ{I}V → - ∃∃K1. ⇩[0, i] L1 ≡ K1.ⓑ{I}V & K1 ⋕[V] K2. -#L1 #L2 #i #H #I #K2 #V #HLK2 elim (lleq_inv_lref … H) -H * + (∃∃K1. ⇩[0, i] L1 ≡ K1.ⓑ{I}V & K1 ⋕[0, V] K2 & d ≤ i) ∨ + ∃∃I1,K1,V1. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V1 & + K1 ⋕[d-i-1, V1] K2 & K1 ⋕[d-i-1, V] K2 & + i < d. +#L1 #L2 #d #i #H #I #K2 #V #HLK2 elim (lleq_inv_lref … H) -H * [ #_ #H elim (lt_refl_false i) - /3 width=5 by ldrop_fwd_length_lt2, lt_to_le_to_lt/ -| #I0 #K1 #K0 #V0 #HLK1 #HLK0 #HK10 lapply (ldrop_mono … HLK0 … HLK2) -L2 + lapply (ldrop_fwd_length_lt2 … HLK2) -HLK2 + /2 width=3 by lt_to_le_to_lt/ (**) (* full auto too slow *) +| #I1 #I2 #K11 #K22 #V1 #V2 #HLK11 #HLK22 #HV1 #HV2 #Hdi lapply (ldrop_mono … HLK22 … HLK2) -L2 + #H destruct /3 width=6 by ex4_3_intro, or_intror/ +| #I0 #K1 #K0 #V0 #HLK1 #HLK0 #HK10 #Hdi lapply (ldrop_mono … HLK0 … HLK2) -L2 + #H destruct /3 width=3 by ex3_intro, or_introl/ +] +qed-. + +lemma lleq_inv_lref_sn: ∀L1,L2,d,i. L1 ⋕[d, #i] L2 → + ∀I,K1,V. ⇩[0, i] L1 ≡ K1.ⓑ{I}V → + (∃∃K2. ⇩[0, i] L2 ≡ K2.ⓑ{I}V & K1 ⋕[0, V] K2 & d ≤ i) ∨ + ∃∃I2,K2,V2. ⇩[0, i] L2 ≡ K2.ⓑ{I2}V2 & + K1 ⋕[d-i-1, V] K2 & K1 ⋕[d-i-1, V2] K2 & + i < d. +#L1 #L2 #d #i #HL12 #I #K1 #V #HLK1 elim (lleq_inv_lref_dx L2 … d … HLK1) -HLK1 +[1,2: * ] /4 width=6 by lleq_sym, ex4_3_intro, ex3_intro, or_introl, or_intror/ +qed-. + +lemma lleq_inv_lref_ge_dx: ∀L1,L2,d,i. L1 ⋕[d, #i] L2 → d ≤ i → + ∀I,K2,V. ⇩[0, i] L2 ≡ K2.ⓑ{I}V → + ∃∃K1. ⇩[0, i] L1 ≡ K1.ⓑ{I}V & K1 ⋕[0, V] K2. +#L1 #L2 #d #i #H #Hdi #I #K2 #V #HLK2 elim (lleq_inv_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 *) +| -HLK2 #I1 #I2 #K11 #K22 #V1 #V2 #_ #_ #_ #_ #H elim (lt_refl_false i) + /2 width=3 by lt_to_le_to_lt/ +| #I0 #K1 #K0 #V0 #HLK1 #HLK0 #HK10 #_ lapply (ldrop_mono … HLK0 … HLK2) -L2 #H destruct /2 width=3 by ex2_intro/ ] qed-. -lemma lleq_inv_lift: ∀L1,L2,U. L1 ⋕[U] L2 → - ∀K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 → - ∀T. ⇧[d, e] T ≡ U → K1 ⋕[T] K2. -#L1 #L2 #U #H elim H -L1 -L2 -U -[ #L1 #L2 #k #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H >(lift_inv_sort2 … H) -X - lapply (ldrop_fwd_length_eq … HLK1 HLK2 HL12) -L1 -L2 -d -e - /2 width=1 by lleq_sort/ (**) (* full auto fails *) -| #I #L1 #L2 #K #K0 #W #i #HLK #HLK0 #HK0 #IHK0 #K1 #K2 #d #e #HLK1 #HLK2 #X #H elim (lift_inv_lref2 … H) -H - * #Hdei #H destruct [ -HK0 | -IHK0 ] - [ elim (ldrop_conf_lt … HLK1 … HLK) // -L1 #L1 #V #HKL1 #KL1 #HV0 - elim (ldrop_conf_lt … HLK2 … HLK0) // -Hdei -L2 #L2 #V2 #HKL2 #K0L2 #HV02 - lapply (lift_inj … HV02 … HV0) -HV02 #H destruct /3 width=11 by lleq_lref/ - | lapply (ldrop_conf_ge … HLK1 … HLK ?) // -L1 - lapply (ldrop_conf_ge … HLK2 … HLK0 ?) // -Hdei -L2 +lemma lleq_inv_lref_ge_sn: ∀L1,L2,d,i. L1 ⋕[d, #i] L2 → d ≤ i → + ∀I,K1,V. ⇩[0, i] L1 ≡ K1.ⓑ{I}V → + ∃∃K2. ⇩[0, i] L2 ≡ K2.ⓑ{I}V & K1 ⋕[0, V] K2. +#L1 #L2 #d #i #HL12 #Hdi #I #K1 #V #HLK1 elim (lleq_inv_lref_ge_dx L2 … Hdi … HLK1) -Hdi -HLK1 +/3 width=3 by lleq_sym, ex2_intro/ +qed-. + +fact lleq_inv_S_aux: ∀L1,L2,T,d0. L1 ⋕[d0, T] L2 → ∀d. d0 = d + 1 → + ∀K1,K2,I,V. ⇩[0, d] L1 ≡ K1.ⓑ{I}V → ⇩[0, d] L2 ≡ K2.ⓑ{I}V → + L1 ⋕[d, T] L2. +#L1 #L2 #T #d0 #H elim H -L1 -L2 -T -d0 +/2 width=1 by lleq_sort, lleq_free, lleq_gref/ +[ #I1 #I2 #L1 #L2 #K11 #K22 #V1 #V2 #d0 #i #Hid0 #HLK11 #HLK22 #HV1 #_ #IHV1 #IHV2 #d #H #K1 #K2 #J #W #HLK1 #HLK2 destruct + elim (le_to_or_lt_eq i d) /2 width=1 by lleq_skip, monotonic_pred/ -Hid0 + [ -HV1 #Hid + lapply (ldrop_fwd_ldrop2 … HLK11) #H1 + lapply (ldrop_fwd_ldrop2 … HLK22) #H2 + lapply (ldrop_conf_ge … H1 … HLK1 ?) // -H1 -HLK1 + lapply (ldrop_conf_ge … H2 … HLK2 ?) // -H2 -HLK2 + (lift_inv_sort2 … H) -X + lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d -e + /2 width=1 by lleq_sort/ +| #I1 #I2 #L1 #L2 #K11 #K22 #W1 #W2 #d0 #i #Hid0 #HLK11 #HLK22 #HW1 #HW2 #IHW1 #IHW2 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref2 … H) -H + * #Hid #H destruct [ -HW1 -HW2 | -IHW1 -IHW2 ] + [ elim (ldrop_conf_lt … HLK1 … HLK11) // -L1 + elim (ldrop_conf_lt … HLK2 … HLK22) // -Hid -L2 + #L2 #V2 #HKL2 #HKL22 #HVW2 #L1 #V1 #HKL1 #HKL11 #HVW1 + @(lleq_skip … HKL1 HKL2) -HKL1 -HKL2 /3 width=6 by monotonic_le_minus_l2/ (**) (* full auto fails *) + | lapply (ldrop_conf_ge … HLK1 … HLK11 ?) // -L1 + lapply (ldrop_conf_ge … HLK2 … HLK22 ?) // -Hid -L2 + #HK22 #HK11 @(lleq_skip … HK11 HK22) -HK11 -HK22 + /2 width=3 by lleq_ge, le_to_lt_to_lt/ (**) (* full auto fails *) + ] +| #I #L1 #L2 #K11 #K22 #W #d0 #i #Hid0 #HLK11 #HLK22 #HW #IHW #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref2 … H) -H + * #Hid #H destruct [ -HW | -IHW ] + [ elim (ldrop_conf_lt … HLK1 … HLK11) // -L1 #L1 #V #HKL1 #KL11 #HVW + elim (ldrop_conf_lt … HLK2 … HLK22) // -Hid -L2 #L2 #V0 #HKL2 #KL22 #HV0 + lapply (lift_inj … HV0 … HVW) -HV0 #H destruct /3 width=12 by lleq_lref/ + | lapply (ldrop_conf_ge … HLK1 … HLK11 ?) // -L1 + lapply (ldrop_conf_ge … HLK2 … HLK22 ?) // -L2 -Hid0 + elim (le_inv_plus_l … Hid) -Hid /3 width=7 by lleq_lref, transitive_le/ + ] +| #L1 #L2 #d0 #i #HL1 #HL2 #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref2 … H) -H + * #_ #H destruct + lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) + [ lapply (ldrop_fwd_length_le4 … HLK1) -HLK1 + lapply (ldrop_fwd_length_le4 … HLK2) -HLK2 + #HKL2 #HKL1 #HK12 @lleq_free // /2 width=3 by transitive_le/ (**) (* full auto too slow *) + | lapply (ldrop_fwd_length … HLK1) -HLK1 #H >H in HL1; -H + lapply (ldrop_fwd_length … HLK2) -HLK2 #H >H in HL2; -H + /3 width=1 by lleq_free, le_plus_to_minus_r/ + ] +| #L1 #L2 #d0 #p #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_gref2 … H) -X + lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d -e + /2 width=1 by lleq_gref/ +| #a #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_bind2 … H) -H + #V #T #HVW #HTU #H destruct /4 width=6 by lleq_bind, ldrop_skip, le_S_S/ +| #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_flat2 … H) -H + #V #T #HVW #HTU #H destruct /3 width=6 by lleq_flat/ +] +qed-. + +lemma lleq_inv_lift_ge: ∀L1,L2,U,d0. L1 ⋕[d0, U] L2 → + ∀K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 → + ∀T. ⇧[d, e] T ≡ U → d+e ≤ d0 → K1 ⋕[d0-e, T] K2. +#L1 #L2 #U #d0 #H elim H -L1 -L2 -U -d0 +[ #L1 #L2 #d0 #k #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_sort2 … H) -X + lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d + /2 width=1 by lleq_sort/ +| #I1 #I2 #L1 #L2 #K11 #K22 #W1 #W2 #d0 #i #Hid0 #HLK11 #HLK22 #HW1 #HW2 #IHW1 #IHW2 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hded0 elim (lift_inv_lref2 … H) -H + * #Hid #H destruct [ -HW1 -HW2 | -IHW1 -IHW2 ] + [ elim (ldrop_conf_lt … HLK1 … HLK11) // -L1 + elim (ldrop_conf_lt … HLK2 … HLK22) // -L2 + elim (le_inv_plus_l … Hded0) #Hdd0e #_ + #L2 #V2 #HKL2 #HKL22 #HVW2 #L1 #V1 #HKL1 #HKL11 #HVW1 + @(lleq_skip … HKL1 HKL2) -HKL1 -HKL2 [ /2 width=3 by lt_to_le_to_lt/ ] (**) (* explicit constructor *) + >minus_minus_comm3 /3 width=6 by arith_k_sn/ (**) (* slow *) + | lapply (ldrop_conf_ge … HLK1 … HLK11 ?) // -L1 + lapply (ldrop_conf_ge … HLK2 … HLK22 ?) // -L2 -Hded0 + elim (le_inv_plus_l … Hid) -Hid #_ #Hei + #HK22 #HK11 @(lleq_skip … HK11 HK22) -HK11 -HK22 (**) (* explicit constructor *) + [ /2 width=1 by monotonic_lt_minus_l/ ] >arith_b1 // + ] +| #I #L1 #L2 #K11 #K22 #W #d0 #i #Hid0 #HLK11 #HLK22 #HW #_ #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hded0 elim (lift_inv_lref2 … H) -H + * #Hid #H destruct + [ -I -L1 -L2 -K11 -K22 -W elim (le_plus_xySz_x_false e 0 d) + /3 width=3 by transitive_le, le_to_lt_to_lt/ + | lapply (ldrop_conf_ge … HLK1 … HLK11 ?) // -L1 + lapply (ldrop_conf_ge … HLK2 … HLK22 ?) // -L2 -Hded0 + /3 width=7 by lleq_lref, monotonic_le_minus_l/ + ] +| #L1 #L2 #d0 #i #HL1 #HL2 #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hded0 elim (lift_inv_lref2 … H) -H * #_ #H destruct - lapply (ldrop_fwd_length_eq … HLK1 HLK2 HL12) - [ /4 width=3 by lleq_free, ldrop_fwd_length_le4, transitive_le/ + lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) + [ lapply (ldrop_fwd_length_le4 … HLK1) -HLK1 + lapply (ldrop_fwd_length_le4 … HLK2) -HLK2 + #HKL2 #HKL1 #HK12 @lleq_free // /2 width=3 by transitive_le/ (**) (* full auto too slow *) | lapply (ldrop_fwd_length … HLK1) -HLK1 #H >H in HL1; -H lapply (ldrop_fwd_length … HLK2) -HLK2 #H >H in HL2; -H /3 width=1 by lleq_free, le_plus_to_minus_r/ ] -| #L1 #L2 #p #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H >(lift_inv_gref2 … H) -X - lapply (ldrop_fwd_length_eq … HLK1 HLK2 HL12) -L1 -L2 -d -e - /2 width=1 by lleq_gref/ (**) (* full auto fails *) -| #a #I #L1 #L2 #W #U #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H elim (lift_inv_bind2 … H) -H - #V #T #HVW #HTU #H destruct /4 width=5 by lleq_bind, ldrop_skip/ -| #I #L1 #L2 #W #U #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H elim (lift_inv_flat2 … H) -H +| #L1 #L2 #d0 #p #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_gref2 … H) -X + lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d + /2 width=1 by lleq_gref/ +| #a #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hded0 elim (lift_inv_bind2 … H) -H + #V #T #HVW #HTU #H destruct + elim (le_inv_plus_l … Hded0) #_ #Hed0 + @lleq_bind [ /2 width=5 by/ ] -IHW (**) (* explicit constructor *) + >plus_minus /3 width=5 by ldrop_skip, le_minus_to_plus/ +| #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hded0 elim (lift_inv_flat2 … H) -H #V #T #HVW #HTU #H destruct /3 width=5 by lleq_flat/ ] qed-. +lemma lleq_inv_lift_be: ∀L1,L2,U,d0. L1 ⋕[d0, U] L2 → + ∀K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 → + ∀T. ⇧[d, e] T ≡ U → d ≤ d0 → d0 ≤ d + e → K1 ⋕[d, T] K2. +#L1 #L2 #U #d0 #H elim H -L1 -L2 -U -d0 +[ #L1 #L2 #d0 #k #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ #_ >(lift_inv_sort2 … H) -X + lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d0 -e + /2 width=1 by lleq_sort/ +| #I1 #I2 #L1 #L2 #K11 #K22 #W1 #W2 #d0 #i #Hid0 #HLK11 #HLK22 #_ #_ #IHW1 #IHW2 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hde elim (lift_inv_lref2 … H) -H + * #Hid #H destruct + [ elim (ldrop_conf_lt … HLK1 … HLK11) // -L1 + elim (ldrop_conf_lt … HLK2 … HLK22) // -L2 -Hid0 + #L2 #V2 #HKL2 #HKL22 #HVW2 #L1 #V1 #HKL1 #HKL11 #HVW1 + @(lleq_skip … HKL1 HKL2) -HKL1 -HKL2 // + /3 width=6 by arith_k_dx, monotonic_le_minus_l2/ (**) (* full auto fails *) + | -I1 -I2 -L1 -L2 -K11 -K22 -W1 -W2 -Hd0 elim (lt_refl_false i) + /3 width=3 by lt_to_le_to_lt, transitive_le/ (**) (* slow *) + ] +| #I #L1 #L2 #K11 #K22 #W #d0 #i #Hid0 #HLK11 #HLK22 #HW #_ #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hde elim (lift_inv_lref2 … H) -H + * #Hid #H destruct + [ -I -L1 -L2 -K11 -K22 -W -Hde elim (lt_refl_false i) + /3 width=3 by lt_to_le_to_lt, transitive_le/ (**) (* slow *) + | lapply (ldrop_conf_ge … HLK1 … HLK11 ?) // -L1 + lapply (ldrop_conf_ge … HLK2 … HLK22 ?) // -L2 -Hid0 -Hd0 -Hde + elim (le_inv_plus_l … Hid) -Hid /2 width=7 by lleq_lref/ + ] +| #L1 #L2 #d0 #i #HL1 #HL2 #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hde elim (lift_inv_lref2 … H) -H + * #_ #H destruct + lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) + [ lapply (ldrop_fwd_length_le4 … HLK1) -HLK1 + lapply (ldrop_fwd_length_le4 … HLK2) -HLK2 + #HKL2 #HKL1 #HK12 @lleq_free // /2 width=3 by transitive_le/ (**) (* full auto too slow *) + | lapply (ldrop_fwd_length … HLK1) -HLK1 #H >H in HL1; -H + lapply (ldrop_fwd_length … HLK2) -HLK2 #H >H in HL2; -H + /3 width=1 by lleq_free, le_plus_to_minus_r/ + ] +| #L1 #L2 #d0 #p #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ #_ >(lift_inv_gref2 … H) -X + lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d0 -e + /2 width=1 by lleq_gref/ +| #a #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hde elim (lift_inv_bind2 … H) -H + #V #T #HVW #HTU #H destruct + @lleq_bind [ /2 width=5 by/ ] -IHW + @(IHU … HTU) -IHU -HTU /2 width=1 by ldrop_skip, le_S_S/ (**) (* full auto too slow *) +| #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hde elim (lift_inv_flat2 … H) -H + #V #T #HVW #HTU #H destruct /3 width=6 by lleq_flat/ +] +qed-. + (* Advanced properties ******************************************************) -lemma lleq_dec: ∀T,L1,L2. Decidable (L1 ⋕[T] L2). +lemma lleq_lift_le: ∀K1,K2,T,d0. K1 ⋕[d0, T] K2 → + ∀L1,L2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 → + ∀U. ⇧[d, e] T ≡ U → d0 ≤ d → L1 ⋕[d0, U] L2. +#K1 #K2 #T #d0 #H elim H -K1 -K2 -T -d0 +[ #K1 #K2 #d0 #k #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_sort1 … H) -X + lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -d + /2 width=1 by lleq_sort/ +| #I1 #I2 #K1 #K2 #K11 #K22 #V1 #V2 #d0 #i #Hid0 #HK11 #HK22 #_ #_ #IHV1 #IHV2 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H + * #Hdi #H destruct + [ elim (ldrop_trans_lt … HLK1 … HK11) // -K1 + elim (ldrop_trans_lt … HLK2 … HK22) // -K2 + #K2 #W2 #HLK2 #HK22 #HVW2 #K1 #W1 #HLK1 #HK11 #HVW1 -Hdi + @(lleq_skip … HLK1 HLK2) // /3 width=6 by monotonic_le_minus_l2/ (**) (* full auto fails *) + | elim (lt_refl_false i) -I1 -I2 -L1 -L2 -K1 -K2 -K11 -K22 -V1 -V2 -e + /3 width=3 by lt_to_le_to_lt, transitive_le/ (**) (* slow *) + ] +| #I #K1 #K2 #K11 #K22 #V #d0 #i #Hid0 #HK11 #HK22 #HV #IHV #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H + * #Hdi #H destruct [ -HV | -IHV ] + [ elim (ldrop_trans_lt … HLK1 … HK11) // -K1 #K1 #W #HLK1 #HK11 #HVW + elim (ldrop_trans_lt … HLK2 … HK22) // -Hdi -K2 #K2 #W2 #HLK2 #HK22 #HVW2 + lapply (lift_mono … HVW2 … HVW) -HVW2 #H destruct /3 width=12 by lleq_lref/ + | lapply (ldrop_trans_ge … HLK1 … HK11 ?) // -K1 + lapply (ldrop_trans_ge … HLK2 … HK22 ?) // -Hdi -K2 + /3 width=7 by lleq_lref, transitive_le/ + ] +| #K1 #K2 #d0 #i #HK1 #HK2 #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H + * #Hid #H destruct + lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -HK12 + [ /3 width=6 by lleq_free, ldrop_fwd_be/ + | lapply (ldrop_fwd_length … HLK1) -HLK1 #HLK1 + lapply (ldrop_fwd_length … HLK2) -HLK2 #HLK2 + @lleq_free [ >HLK1 | >HLK2 ] -Hid -HLK1 -HLK2 /2 width=1 by monotonic_le_plus_r/ (**) (* explicit constructor *) + ] +| #K1 #K2 #d0 #p #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_gref1 … H) -X + lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -d -e + /2 width=1 by lleq_gref/ +| #a #I #K1 #K2 #V #T #d0 #_ #_ #IHV #IHT #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_bind1 … H) -H + #W #U #HVW #HTU #H destruct /4 width=6 by lleq_bind, ldrop_skip, le_S_S/ +| #I #K1 #K2 #V #T #d0 #_ #_ #IHV #IHT #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_flat1 … H) -H + #W #U #HVW #HTU #H destruct /3 width=6 by lleq_flat/ +] +qed-. + +lemma lleq_lift_ge: ∀K1,K2,T,d0. K1 ⋕[d0, T] K2 → + ∀L1,L2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 → + ∀U. ⇧[d, e] T ≡ U → d ≤ d0 → L1 ⋕[d0+e, U] L2. +#K1 #K2 #T #d0 #H elim H -K1 -K2 -T -d0 +[ #K1 #K2 #d0 #k #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_sort1 … H) -X + lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -d + /2 width=1 by lleq_sort/ +| #I1 #I2 #K1 #K2 #K11 #K22 #V1 #V2 #d0 #i #hid0 #HK11 #HK22 #HV1 #HV2 #IHV1 #IHV2 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H + * #Hdi #H destruct [ -HV1 -HV2 | -IHV1 -IHV2 ] + [ elim (ldrop_trans_lt … HLK1 … HK11) // -K1 #K1 #W1 #HLK1 #HK11 #HVW1 + elim (ldrop_trans_lt … HLK2 … HK22) // -K2 #K2 #W2 #HLK2 #HK22 #HVW2 + @(lleq_skip … HLK1 HLK2) -HLK1 -HLK2 (**) (* explicit constructor *) + [ /2 width=3 by lt_to_le_to_lt/ ] + >arith_i /3 width=5 by monotonic_le_minus_l2/ + | lapply (ldrop_trans_ge_comm … HLK1 … HK11 ?) // -K1 + lapply (ldrop_trans_ge_comm … HLK2 … HK22 ?) // -K2 + /4 width=10 by lleq_skip, monotonic_lt_plus_l/ + ] +| #I #K1 #K2 #K11 #K22 #V #d0 #i #Hid0 #HK11 #HK22 #HV #_ #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H + * #Hid #H destruct + [ elim (lt_refl_false i) -I -L1 -L2 -K1 -K2 -K11 -K22 -V -e + /3 width=3 by lt_to_le_to_lt, transitive_le/ (**) (* slow *) + | lapply (ldrop_trans_ge … HLK1 … HK11 ?) // -K1 + lapply (ldrop_trans_ge … HLK2 … HK22 ?) // -Hid -K2 + /3 width=7 by lleq_lref, monotonic_le_plus_l/ + ] +| #K1 #K2 #d0 #i #HK1 #HK2 #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H + * #Hid #H destruct + lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -HK12 + [ /3 width=6 by lleq_free, ldrop_fwd_be/ + | lapply (ldrop_fwd_length … HLK1) -HLK1 #HLK1 + lapply (ldrop_fwd_length … HLK2) -HLK2 #HLK2 + @lleq_free [ >HLK1 | >HLK2 ] -Hid -HLK1 -HLK2 /2 width=1 by monotonic_le_plus_r/ (**) (* explicit constructor *) + ] +| #K1 #K2 #d0 #p #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_gref1 … H) -X + lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -d + /2 width=1 by lleq_gref/ +| #a #I #K1 #K2 #V #T #d0 #_ #_ #IHV #IHT #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_bind1 … H) -H + #W #U #HVW #HTU #H destruct /4 width=5 by lleq_bind, ldrop_skip, le_minus_to_plus/ +| #I #K1 #K2 #V #T #d0 #_ #_ #IHV #IHT #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_flat1 … H) -H + #W #U #HVW #HTU #H destruct /3 width=5 by lleq_flat/ +] +qed-. + +lemma lleq_be: ∀L1,L2,U,d0. L1 ⋕[d0, U] L2 → + ∀K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 → + ∀T. ⇧[d, e] T ≡ U → d ≤ d0 → d0 ≤ d + e → L1 ⋕[d, U] L2. +#L1 #L2 #U #d0 #H elim H -L1 -L2 -U -d0 +/2 width=1 by lleq_sort, lleq_free, lleq_gref/ +[ #I1 #I2 #L1 #L2 #K11 #K22 #W1 #W2 #d0 #i #Hid0 #HLK11 #HLK22 #_ #_ #IHW1 #IHW2 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hd0de elim (lift_inv_lref2 … H) -H + * #Hid #H destruct [ -Hid0 | -Hd0 ] + [ elim (ldrop_conf_lt … HLK1 … HLK11) // -HLK1 + elim (ldrop_conf_lt … HLK2 … HLK22) // -HLK2 + #L2 #V2 #_ #HKL22 #HVW2 #L1 #V1 #_ #HKL21 #HVW1 + @(lleq_skip … HLK11 HLK22) -HLK11 -HLK22 // + /3 width=8 by arith_k_dx, monotonic_le_minus_l2/ (**) (* full auto fails *) + | -I1 -I2 -K11 -K22 -K1 -K2 -W1 -W2 elim (lt_refl_false … i) -L1 -L2 + @(lt_to_le_to_lt … Hid0) -Hid0 /2 width=3 by transitive_le/ (**) (* full auto too slow *) + ] +| #I #L1 #L2 #K11 #K22 #W #d0 #i #Hid0 #HLK11 #HLK22 #HW #_ #K1 #K2 #d #e #_ #_ #X #H #Hd0 #_ elim (lift_inv_lref2 … H) -H + * #Hid #H destruct + [ -I -K1 -K2 -K11 -K22 -W elim (lt_refl_false i) + @(lt_to_le_to_lt … Hid) -Hid /2 width=3 by transitive_le/ (**) (* full auto too slow *) + | -d0 /3 width=7 by lleq_lref, le_plus_b/ + ] +| #a #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hde elim (lift_inv_bind2 … H) -H + #V #T #HVW #HTU #H destruct + @lleq_bind [ /2 width=8 by/ ] -IHW + @(IHU … HTU) -IHU -HTU /2 width=2 by ldrop_skip, le_S_S/ (**) (* full auto too slow *) +| #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hde elim (lift_inv_flat2 … H) -H + #V #T #HVW #HTU #H destruct /3 width=8 by lleq_flat/ +] +qed-. + +axiom- lleq_dec: ∀T,L1,L2,d. Decidable (L1 ⋕[d, T] 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 #H1 #L2 elim (eq_nat_dec (|L1|) (|L2|)) - [ #HL12 elim (lt_or_ge i (|L1|)) + [ #HL12 #d elim (lt_or_ge i d) /3 width=1 by lleq_skip, or_introl/ + #Hdi elim (lt_or_ge i (|L1|)) #HiL1 elim (lt_or_ge i (|L2|)) /3 width=1 by or_introl, lleq_free/ #HiL2 elim (ldrop_O1_lt … HiL2) #I2 #K2 #V2 #HLK2 elim (ldrop_O1_lt … HiL1) #I1 #K1 #V1 #HLK1 elim (eq_bind2_dec I2 I1) [ #H2 elim (eq_term_dec V2 V1) - [ #H3 elim (IH K1 V1 … K2) destruct + [ #H3 elim (IH K1 V1 … K2 0) destruct /3 width=7 by lleq_lref, ldrop_fwd_rfw, or_introl/ ] ] -IH #H3 @or_intror - #H elim (lleq_inv_lref … H) -H * - [1,3,5: /3 width=4 by lt_to_le_to_lt, lt_refl_false/ ] + #H elim (lleq_inv_lref … H) -H [1,3,4,6,7,9: * ] + [1,3,5,7,8,9: /3 width=4 by lt_to_le_to_lt, lt_refl_false/ ] #I0 #X1 #X2 #V0 #HLX1 #HLX2 #HX12 lapply (ldrop_mono … HLX1 … HLK1) -HLX1 -HLK1 lapply (ldrop_mono … HLX2 … HLK2) -HLX2 -HLK2 #H #H0 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 destruct - elim (IH L1 V … L2) /2 width=1 by/ - elim (IH (L1.ⓑ{I}V) T … (L2.ⓑ{I}V)) -IH /3 width=1 by or_introl, lleq_bind/ +| #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 destruct - elim (IH L1 V … L2) /2 width=1 by/ - elim (IH L1 T … L2) -IH /3 width=1 by or_introl, lleq_flat/ +| #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=2 by lleq_fwd_length, or_intror/ +-n /4 width=3 by lleq_fwd_length, or_intror/ qed-. - +*) (* Main properties **********************************************************) -theorem lleq_trans: ∀T. Transitive … (lleq T). -#T #L1 #L #H elim H -T -L1 -L -/4 width=4 by lleq_fwd_length, lleq_gref, lleq_sort, trans_eq/ -[ #I #L1 #L #K1 #K #V #i #HLK1 #HLK #_ #IHK1 #L2 #H elim (lleq_inv_lref … H) -H * - [ -HLK1 -IHK1 #HLi #_ elim (lt_refl_false i) - /3 width=5 by ldrop_fwd_length_lt2, lt_to_le_to_lt/ - | #I0 #K0 #K2 #V0 #HLK0 #HLK2 #HK12 lapply (ldrop_mono … HLK0 … HLK) -L +axiom- lleq_trans: ∀d,T. Transitive … (lleq d T). +(* +#d #T #L1 #L #H elim H -d -T -L1 -L +/4 width=5 by lleq_fwd_length, lleq_gref, lleq_sort, trans_eq/ +[ #L1 #L #d #i #Hid #HL1 #L2 #H lapply (lleq_fwd_length … H) + #HL2 elim (lleq_inv_lref … H) -H /2 width=1 by lleq_skip/ +| #I #L1 #L #K1 #K #V #d #i #Hdi #HLK1 #HLK #_ #IHK1 #L2 #H elim (lleq_inv_lref … H) -H + [ -HLK1 -IHK1 * #HLi #_ elim (lt_refl_false i) + /3 width=5 by ldrop_fwd_length_lt2, lt_to_le_to_lt/ (**) (* slow *) + | -K1 -K #Hid elim (lt_refl_false i) /2 width=3 by lt_to_le_to_lt/ + | * #I0 #K0 #K2 #V0 #HLK0 #HLK2 #HK12 lapply (ldrop_mono … HLK0 … HLK) -L #H destruct /3 width=7 by lleq_lref/ ] -| #L1 #L #i #HL1i #HLi #HL #L2 #H lapply (lleq_fwd_length … H) - #HL2 elim (lleq_inv_lref … H) -H * /2 width=1 by lleq_free/ -| #a #I #L1 #L #V #T #_ #_ #IHV #IHT #L2 #H elim (lleq_inv_bind … H) -H +| #L1 #L #d #i #HL1i #HLi #HL #L2 #H lapply (lleq_fwd_length … H) + #HL2 elim (lleq_inv_lref … H) -H /2 width=1 by lleq_free/ +| #a #I #L1 #L #V #T #d #_ #_ #IHV #IHT #L2 #H elim (lleq_inv_bind … H) -H /3 width=1 by lleq_bind/ -| #I #L1 #L #V #T #_ #_ #IHV #IHT #L2 #H elim (lleq_inv_flat … H) -H +| #I #L1 #L #V #T #d #_ #_ #IHV #IHT #L2 #H elim (lleq_inv_flat … H) -H /3 width=1 by lleq_flat/ ] qed-. - -theorem lleq_canc_sn: ∀L,L1,L2,T. L ⋕[T] L1→ L ⋕[T] L2 → L1 ⋕[T] L2. +*) +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. L1 ⋕[T] L → L2 ⋕[T] L → L1 ⋕[T] L2. +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/notation/functions/predecessor_1.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/predecessor_1.ma index 038a6657e..cf94d0497 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/predecessor_1.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/predecessor_1.ma @@ -14,6 +14,6 @@ (* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) -notation "hvbox( ⫰ term 55 T )" - non associative with precedence 55 +notation "hvbox( ⫰ term 70 T )" + non associative with precedence 70 for @{ 'Predecessor $T }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/successor_1.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/successor_1.ma index 6271880b9..05e2c3146 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/successor_1.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/successor_1.ma @@ -14,6 +14,6 @@ (* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) -notation "hvbox( ⫯ term 55 T )" - non associative with precedence 55 +notation "hvbox( ⫯ term 70 T )" + non associative with precedence 70 for @{ 'Successor $T }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_le.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_le.ma index be13774f5..ccb9563ee 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_le.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_le.ma @@ -81,8 +81,19 @@ lemma yle_inv_succ: ∀m,n. ⫯m ≤ ⫯n → m ≤ n. #x #Hx #H destruct // qed-. +(* Forward lemmas on successor **********************************************) + +lemma yle_fwd_succ1: ∀m,n. ⫯m ≤ n → m ≤ ⫰n. +#m #x #H elim (yle_inv_succ1 … H) -H +#n #Hmn #H destruct // +qed-. + (* Basic properties *********************************************************) +lemma le_O1: ∀n:ynat. 0 ≤ n. +* /2 width=1 by yle_inj/ +qed. + lemma yle_refl: reflexive … yle. * /2 width=1 by le_n, yle_inj/ qed. @@ -98,6 +109,10 @@ lemma yle_refl_pred_sn: ∀x. ⫰x ≤ x. (* Properties on successor **************************************************) +lemma yle_succ: ∀m,n. m ≤ n → ⫯m ≤ ⫯n. +#m #n * -m -n /3 width=1 by yle_inj, le_S_S/ +qed. + lemma yle_succ_dx: ∀m,n. m ≤ n → m ≤ ⫯n. #m #n * -m -n /3 width=1 by le_S, yle_inj/ qed. diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma index 4c63e40a7..b684c0403 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma @@ -51,6 +51,11 @@ qed-. lemma ylt_inv_Y2: ∀x. x < ∞ → ∃m. x = yinj m. /2 width=3 by ylt_inv_Y2_aux/ qed-. +lemma ylt_inv_O1: ∀n. 0 < n → ⫯⫰n = n. +* // #n #H lapply (ylt_inv_inj … H) -H normalize +/3 width=1 by S_pred, eq_f/ +qed-. + (* Inversion lemmas on successor ********************************************) fact ylt_inv_succ1_aux: ∀x,y. x < y → ∀m. x = ⫯m → ∃∃n. m < n & y = ⫯n. @@ -68,7 +73,7 @@ qed-. lemma ylt_inv_succ1: ∀m,y. ⫯m < y → ∃∃n. m < n & y = ⫯n. /2 width=3 by ylt_inv_succ1_aux/ qed-. -lemma yle_inv_succ: ∀m,n. ⫯m < ⫯n → m < n. +lemma ylt_inv_succ: ∀m,n. ⫯m < ⫯n → m < n. #m #n #H elim (ylt_inv_succ1 … H) -H #x #Hx #H destruct // qed-. @@ -81,7 +86,9 @@ fact ylt_inv_succ2_aux: ∀x,y. x < y → ∀n. y = ⫯n → x ≤ n. ] qed-. -lemma ylt_inv_succ2: ∀m,n. m < ⫯n → m ≤ n. +(* Forward lemmas on successor **********************************************) + +lemma ylt_fwd_succ2: ∀m,n. m < ⫯n → m ≤ n. /2 width=3 by ylt_inv_succ2_aux/ qed-. (* inversion and forward lemmas on yle **************************************) @@ -99,6 +106,12 @@ lemma ylt_yle_false: ∀m:ynat. ∀n:ynat. m < n → n ≤ m → ⊥. ] qed-. +(* Properties on successor **************************************************) + +lemma ylt_O_succ: ∀n. 0 < ⫯n. +* /2 width=1 by ylt_inj/ +qed. + (* Properties on yle ********************************************************) lemma yle_to_ylt_or_eq: ∀m:ynat. ∀n:ynat. m ≤ n → m < n ∨ m = n. diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_minus.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_minus.ma new file mode 100644 index 000000000..1110f3e44 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_minus.ma @@ -0,0 +1,61 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground_2/ynat/ynat_lt.ma". + +(* NATURAL NUMBERS WITH INFINITY ********************************************) + +(* subtraction *) +definition yminus: ynat → ynat → ynat ≝ λx,y. match y with +[ yinj n ⇒ ypred^n x +| Y ⇒ yinj 0 +]. + +interpretation "ynat minus" 'minus x y = (yminus x y). + +(* Basic properties *********************************************************) + +lemma yminus_inj: ∀n,m. yinj m - yinj n = yinj (m - n). +#n elim n -n /2 width=3 by trans_eq/ +qed. + +lemma yminus_Y_inj: ∀n. ∞ - yinj n = ∞. +#n elim n -n // normalize +#n #IHn >IHn // +qed. + +(* Properties on successor **************************************************) + +lemma yminus_succ: ∀n,m. ⫯m - ⫯n = m - n. +* // #n * [2: >yminus_Y_inj // ] +#m >yminus_inj // +qed. + +(* Properties on order ******************************************************) + +lemma yle_minus_sn: ∀n,m. m - n ≤ m. +* // #n * /2 width=1 by yle_inj/ +qed. + +lemma yle_to_minus: ∀m:ynat. ∀n:ynat. m ≤ n → m - n = 0. +#m #n * -m -n /3 width=3 by eq_minus_O, eq_f/ +qed-. + +lemma yminus_to_le: ∀n:ynat. ∀m:ynat. m - n = 0 → m ≤ n. +* // #n * +[ #m >yminus_inj #H lapply (yinj_inj … H) -H (**) (* destruct lemma needed *) + /2 width=1 by yle_inj/ +| >yminus_Y_inj #H destruct +] +qed. diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma index 8f348733e..f872f93e2 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma @@ -12,13 +12,13 @@ (* *) (**************************************************************************) -include "ground_2/ynat/ynat_lt.ma". +include "ground_2/ynat/ynat_minus.ma". (* NATURAL NUMBERS WITH INFINITY ********************************************) (* addition *) -definition yplus: ynat → ynat → ynat ≝ λx,y. match x with -[ yinj m ⇒ ysucc^m y +definition yplus: ynat → ynat → ynat ≝ λx,y. match y with +[ yinj n ⇒ ysucc^n x | Y ⇒ Y ]. @@ -26,22 +26,30 @@ interpretation "ynat plus" 'plus x y = (yplus x y). (* Properties on successor **************************************************) -lemma yplus_succ1: ∀m,n. (⫯m) + n = ⫯(m + n). -* // +lemma yplus_succ2: ∀m,n. m + ⫯n = ⫯(m + n). +#m * // +qed. + +lemma yplus_succ1: ∀m,n. ⫯m + n = ⫯(m + n). +#m * normalize // qed. -lemma yplus_SO1: ∀m. 1 + m = ⫯m. +lemma yplus_succ_swap: ∀m,n. m + ⫯n = ⫯m + n. +// qed. + +lemma yplus_SO2: ∀m. m + 1 = ⫯m. * // -qed. +qed. (* Basic properties *********************************************************) -lemma yplus_inj: ∀m,n. yinj m + yinj n = yinj (m + n). -#m elim m -m // -#m #IHm #n >(yplus_succ1 m) >IHm -IHm // +lemma yplus_inj: ∀n,m. yinj m + yinj n = yinj (m + n). +#n elim n -n [ normalize // ] +#n #IHn #m >(yplus_succ2 ? n) >IHn -IHn +ysucc_iter_Y // qed. lemma yplus_assoc: associative … yplus. -* // #x * // -#y #z >yplus_inj whd in ⊢ (??%%); >iter_plus // +#x #y * // #z cases y -y +[ #y >yplus_inj whd in ⊢ (??%%); yplus_Y1 // +] qed. +lemma yplus_O_sn: ∀n:ynat. 0 + n = n. +#n >yplus_comm // qed. + +(* Basic inversion lemmas ***************************************************) + +lemma yplus_inv_inj: ∀z,y,x. x + y = yinj z → + ∃∃m,n. m + n = z & x = yinj m & y = yinj n. +#z * [2: normalize #x #H destruct ] +#y * [2: >yplus_Y1 #H destruct ] +/3 width=5 by yinj_inj, ex3_2_intro/ +qed-. + +(* Properties on order ******************************************************) + +lemma yle_plus_dx2: ∀n,m. n ≤ m + n. +* // +#n elim n -n // +#n #IHn #m >(yplus_succ2 ? n) @(yle_succ n) // (**) (* full auto fails *) +qed. + +lemma yle_plus_dx1: ∀n,m. m ≤ m + n. +// qed. + +(* Forward lemmas on order **************************************************) + +lemma yle_fwd_plus_sn2: ∀x,y,z. x + y ≤ z → y ≤ z. +/2 width=3 by yle_trans/ qed-. + +lemma yle_fwd_plus_sn1: ∀x,y,z. x + y ≤ z → x ≤ z. +/2 width=3 by yle_trans/ qed-. -- 2.39.2