From 888840f6b3a71d3d686b53b702d362ab90ab0038 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 15 Feb 2021 23:14:05 +0100 Subject: [PATCH] milestone update in ground, partial commit + propagating the arithmetics library + gathering the arithmetics files + function composition respects extensional equivalence + minor corrections --- .../ground/{lib => arith}/arith_2a.ma | 62 ++- .../ground/{lib => arith}/arith_2b.ma | 28 +- .../ground/arith/{arith.txt => arith_etc.txt} | 3 - .../ground/arith/{nat.txt => nat_etc.txt} | 0 .../lambdadelta/ground/arith/nat_iter.ma | 14 +- .../lambdadelta/ground/arith/nat_le.ma | 10 +- .../lambdadelta/ground/arith/nat_le_minus.ma | 8 +- .../ground/arith/nat_le_minus_plus.ma | 10 +- .../lambdadelta/ground/arith/nat_le_plus.ma | 8 +- .../lambdadelta/ground/arith/nat_lt.ma | 42 +- .../lambdadelta/ground/arith/nat_lt_minus.ma | 20 +- .../ground/arith/nat_lt_minus_plus.ma | 2 +- .../lambdadelta/ground/arith/nat_lt_pred.ma | 7 +- .../lambdadelta/ground/arith/nat_minus.ma | 2 +- .../ground/arith/nat_minus_plus.ma | 2 +- .../lambdadelta/ground/arith/nat_plus.ma | 12 +- .../lambdadelta/ground/arith/nat_pred.ma | 4 +- .../lambdadelta/ground/arith/nat_pred_succ.ma | 2 +- .../lambdadelta/ground/arith/nat_succ.ma | 14 +- .../lambdadelta/ground/arith/nat_succ_iter.ma | 2 +- .../lambdadelta/ground/arith/pnat_iter.ma | 27 +- .../arith/{pnat_dis.ma => pnat_split.ma} | 2 +- .../ground/{wf_ind => arith}/wf1_ind_nlt.ma | 0 .../lambdadelta/ground/arith/wf1_ind_ylt.ma | 31 ++ .../ground/{wf_ind => arith}/wf2_ind_nlt.ma | 0 .../ground/{wf_ind => arith}/wf3_ind_nlt.ma | 0 .../ground/{ynat => arith}/ynat.ma | 38 +- .../lambdadelta/ground/arith/ynat_le.ma | 113 +++++ .../ground/arith/ynat_le_minus1.ma | 57 +++ .../ground/arith/ynat_le_minus1_plus.ma | 117 +++++ .../ground/arith/ynat_le_minus1_succ.ma | 29 ++ .../lambdadelta/ground/arith/ynat_le_plus.ma | 112 +++++ .../lambdadelta/ground/arith/ynat_le_pred.ma | 37 ++ .../ground/arith/ynat_le_pred_succ.ma | 60 +++ .../lambdadelta/ground/arith/ynat_le_succ.ma | 47 ++ .../lambdadelta/ground/arith/ynat_lt.ma | 97 ++++ .../lambdadelta/ground/arith/ynat_lt_le.ma | 112 +++++ .../ground/arith/ynat_lt_le_minus1.ma | 29 ++ .../ground/arith/ynat_lt_le_minus1_plus.ma | 30 ++ .../ground/arith/ynat_lt_le_plus.ma | 64 +++ .../ground/arith/ynat_lt_le_pred.ma | 28 ++ .../ground/arith/ynat_lt_le_pred_succ.ma | 27 ++ .../ground/arith/ynat_lt_le_succ.ma | 50 +++ .../ground/arith/ynat_lt_minus1.ma | 50 +++ .../ground/arith/ynat_lt_minus1_plus.ma | 34 ++ .../lambdadelta/ground/arith/ynat_lt_plus.ma | 123 ++++++ .../ground/arith/ynat_lt_plus_pred.ma | 45 ++ .../lambdadelta/ground/arith/ynat_lt_pred.ma | 28 ++ .../ground/arith/ynat_lt_pred_succ.ma | 55 +++ .../lambdadelta/ground/arith/ynat_lt_succ.ma | 63 +++ .../lambdadelta/ground/arith/ynat_minus1.ma | 76 ++++ .../ground/arith/ynat_minus1_plus.ma | 34 ++ .../ynat_minus1_succ.ma} | 29 +- .../lambdadelta/ground/arith/ynat_nat.ma | 77 ++++ .../lambdadelta/ground/arith/ynat_plus.ma | 201 +++++++++ .../lambdadelta/ground/arith/ynat_pred.ma | 61 +++ .../ground/arith/ynat_pred_succ.ma | 35 ++ .../lambdadelta/ground/arith/ynat_succ.ma | 106 +++++ .../ground/etc/ynat/ynat_minus.etc | 30 ++ .../{insert_eq_0.ma => insert_eq_1.ma} | 3 +- .../contribs/lambdadelta/ground/lib/arith.ma | 417 ------------------ .../contribs/lambdadelta/ground/lib/exteq.ma | 43 +- .../ground/notation/functions/two_0.ma | 19 + .../lambdadelta/ground/web/ground.ldw.xml | 3 + .../lambdadelta/ground/web/ground_src.tbl | 36 +- .../lambdadelta/ground/ynat/ynat_le.ma | 155 ------- .../lambdadelta/ground/ynat/ynat_lt.ma | 271 ------------ .../lambdadelta/ground/ynat/ynat_minus_sn.ma | 221 ---------- .../lambdadelta/ground/ynat/ynat_plus.ma | 313 ------------- .../lambdadelta/ground/ynat/ynat_succ.ma | 97 ---- 70 files changed, 2348 insertions(+), 1636 deletions(-) rename matita/matita/contribs/lambdadelta/ground/{lib => arith}/arith_2a.ma (53%) rename matita/matita/contribs/lambdadelta/ground/{lib => arith}/arith_2b.ma (62%) rename matita/matita/contribs/lambdadelta/ground/arith/{arith.txt => arith_etc.txt} (94%) rename matita/matita/contribs/lambdadelta/ground/arith/{nat.txt => nat_etc.txt} (100%) rename matita/matita/contribs/lambdadelta/ground/arith/{pnat_dis.ma => pnat_split.ma} (95%) rename matita/matita/contribs/lambdadelta/ground/{wf_ind => arith}/wf1_ind_nlt.ma (100%) create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/wf1_ind_ylt.ma rename matita/matita/contribs/lambdadelta/ground/{wf_ind => arith}/wf2_ind_nlt.ma (100%) rename matita/matita/contribs/lambdadelta/ground/{wf_ind => arith}/wf3_ind_nlt.ma (100%) rename matita/matita/contribs/lambdadelta/ground/{ynat => arith}/ynat.ma (63%) create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/ynat_le.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/ynat_le_minus1.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/ynat_le_minus1_plus.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/ynat_le_minus1_succ.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/ynat_le_plus.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/ynat_le_pred.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/ynat_le_pred_succ.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/ynat_le_succ.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/ynat_lt.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_minus1.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_minus1_plus.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_plus.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_pred.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_pred_succ.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_succ.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_minus1.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_minus1_plus.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_plus.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_plus_pred.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_pred.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_pred_succ.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_succ.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/ynat_minus1.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/ynat_minus1_plus.ma rename matita/matita/contribs/lambdadelta/ground/{ynat/ynat_pred.ma => arith/ynat_minus1_succ.ma} (61%) create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/ynat_nat.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/ynat_plus.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/ynat_pred.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/ynat_pred_succ.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/ynat_succ.ma rename matita/matita/contribs/lambdadelta/ground/insert_eq/{insert_eq_0.ma => insert_eq_1.ma} (90%) delete mode 100644 matita/matita/contribs/lambdadelta/ground/lib/arith.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/notation/functions/two_0.ma delete mode 100644 matita/matita/contribs/lambdadelta/ground/ynat/ynat_le.ma delete mode 100644 matita/matita/contribs/lambdadelta/ground/ynat/ynat_lt.ma delete mode 100644 matita/matita/contribs/lambdadelta/ground/ynat/ynat_minus_sn.ma delete mode 100644 matita/matita/contribs/lambdadelta/ground/ynat/ynat_plus.ma delete mode 100644 matita/matita/contribs/lambdadelta/ground/ynat/ynat_succ.ma diff --git a/matita/matita/contribs/lambdadelta/ground/lib/arith_2a.ma b/matita/matita/contribs/lambdadelta/ground/arith/arith_2a.ma similarity index 53% rename from matita/matita/contribs/lambdadelta/ground/lib/arith_2a.ma rename to matita/matita/contribs/lambdadelta/ground/arith/arith_2a.ma index 9b5ccb3f6..b5ff26116 100644 --- a/matita/matita/contribs/lambdadelta/ground/lib/arith_2a.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/arith_2a.ma @@ -12,35 +12,47 @@ (* *) (**************************************************************************) -include "ground/lib/arith.ma". +include "ground/notation/functions/two_0.ma". +include "ground/arith/nat_le_minus_plus.ma". +include "ground/arith/nat_lt.ma". -(* ARITHMETICAL PROPERTIES FOR λδ-2B ****************************************) +(* ARITHMETICAL PROPERTIES FOR λδ-2A ****************************************) + +interpretation + "zero (non-negative integers)" + 'Two = (ninj (psucc punit)). (* Equalities ***************************************************************) -lemma plus_n_2: ∀n. n + 2 = n + 1 + 1. +lemma plus_n_2: ∀n. (n + 𝟐) = n + 𝟏 + 𝟏. // qed. lemma arith_b1: ∀a,b,c1. c1 ≤ b → a - c1 - (b - c1) = a - b. -#a #b #c1 #H >minus_minus_comm >minus_le_minus_minus_comm // +#a #b #c1 #H >nminus_comm minus_plus >minus_plus >minus_plus /2 width=1 by arith_b1/ +#a #b #c1 #c2 #H +>(nminus_plus_assoc ? c1 c2) >(nminus_plus_assoc ? c1 c2) +/2 width=1 by arith_b1/ qed-. lemma arith_c1x: ∀x,a,b,c1. x + c1 + a - (b + c1) = x + a - b. -/3 by monotonic_le_minus_l, le_to_le_to_eq, le_n/ qed. +#x #a #b #c1 +plus_minus /2 width=1 by arith_b2/ +#a1 #a2 #b #c1 #H1 #H2 +>nminus_plus_comm_23 +/2 width=1 by arith_b1/ qed-. -lemma arith_i: ∀x,y,z. y < x → x+z-y-1 = x-y-1+z. -/2 width=1 by plus_minus/ qed-. +lemma arith_i: ∀x,y,z. y < x → x+z-y-(𝟏) = x-y-(𝟏)+z. +/2 width=1 by nminus_plus_comm_23/ qed-. -(* Properties ***************************************************************) +(* Constructions ************************************************************) fact le_repl_sn_conf_aux: ∀x,y,z:nat. x ≤ z → x = y → y ≤ z. // qed-. @@ -48,30 +60,34 @@ fact le_repl_sn_conf_aux: ∀x,y,z:nat. x ≤ z → x = y → y ≤ z. fact le_repl_sn_trans_aux: ∀x,y,z:nat. x ≤ z → y = x → y ≤ z. // qed-. -lemma arith_j: ∀x,y,z. x-y-1 ≤ x-(y-z)-1. -/3 width=1 by monotonic_le_minus_l, monotonic_le_minus_r/ qed. +lemma monotonic_le_minus_l2: ∀x1,x2,y,z. x1 ≤ x2 → x1 - y - z ≤ x2 - y - z. +/3 width=1 by nle_minus_bi_dx/ qed. + +lemma arith_j: ∀x,y,z. x-y-(𝟏) ≤ x-(y-z)-𝟏. +/3 width=1 by nle_minus_bi_dx, nle_minus_bi_sn/ qed. -lemma arith_k_sn: ∀z,x,y,n. z < x → x+n ≤ y → x-z-1+n ≤ y-z-1. +lemma arith_k_sn: ∀z,x,y,n. z < x → x+n ≤ y → x-z-(𝟏)+n ≤ y-z-𝟏. #z #x #y #n #Hzx #Hxny ->plus_minus [2: /2 width=1 by monotonic_le_minus_r/ ] ->plus_minus [2: /2 width=1 by lt_to_le/ ] +>nminus_plus_comm_23 [2: /2 width=1 by nle_minus_bi_sn/ ] +>nminus_plus_comm_23 [2: /2 width=1 by nlt_des_le/ ] /2 width=1 by monotonic_le_minus_l2/ qed. -lemma arith_k_dx: ∀z,x,y,n. z < x → y ≤ x+n → y-z-1 ≤ x-z-1+n. +lemma arith_k_dx: ∀z,x,y,n. z < x → y ≤ x+n → y-z-(𝟏) ≤ x-z-(𝟏)+n. #z #x #y #n #Hzx #Hyxn ->plus_minus [2: /2 width=1 by monotonic_le_minus_r/ ] ->plus_minus [2: /2 width=1 by lt_to_le/ ] +>nminus_plus_comm_23 [2: /2 width=1 by nle_minus_bi_sn/ ] +>nminus_plus_comm_23 [2: /2 width=1 by nlt_des_le/ ] /2 width=1 by monotonic_le_minus_l2/ qed. -(* Inversion & forward lemmas ***********************************************) +(* Inversions ***************************************************************) -lemma lt_plus_SO_to_le: ∀x,y. x < y + 1 → x ≤ y. -/2 width=1 by monotonic_pred/ qed-. +lemma lt_plus_SO_to_le: ∀x,y. x < y + (𝟏) → x ≤ y. +/2 width=1 by nle_inv_succ_bi/ qed-. (* Iterators ****************************************************************) -lemma iter_SO: ∀B:Type[0]. ∀f:B→B. ∀b,l. f^(l+1) b = f (f^l b). -#B #f #b #l >commutative_plus // +lemma iter_SO: ∀B:Type[0]. ∀f:B→B. ∀b,l. f^(l+𝟏) b = f (f^l b). +#B #f #b #l +minus_plus -elim (le_or_ge (m11+m12) m21) #Hm1121 -[ lapply (transitive_le m11 ??? Hm1121) // #Hm121 - lapply (le_plus_to_minus_l … Hm1121) #Hm12211 - (eq_minus_O m11 ?) // >(eq_minus_O m12 ?) // -| >(eq_minus_O m21 ?) // (eq_minus_O m11 ?) // (eq_minus_O m21 ?) // nminus_plus_assoc +elim (nat_split_le_ge (m11+m12) m21) #Hm1121 +[ lapply (nle_trans m11 ??? Hm1121) // #Hm121 + lapply (nle_minus_dx_dx … Hm1121) #Hm12211 + nplus_minus_assoc // >nminus_assoc_comm_23 // + | <(nle_inv_eq_zero_minus m21 ?) // >nminus_assoc_comm_23 // ] ] qed. @@ -35,10 +35,10 @@ qed. lemma arith_l3 (m) (n1) (n2): n1+n2-m = n1-m+(n2-(m-n1)). // qed. -lemma arith_l2 (n1) (n2): ↑n2-n1 = 1-n1+(n2-(n1-1)). +lemma arith_l2 (n1) (n2): ↑n2-n1 = 𝟏-n1+(n2-(n1-𝟏)). #n1 #n2 (eq_inv_nsucc_bi … H) -n // | #o #Ho #H >(eq_inv_nsucc_bi … H) -n @@ -73,7 +73,7 @@ qed-. (*** le_n_O_to_eq *) lemma nle_inv_zero_dx (m): m ≤ 𝟎 → 𝟎 = m. -#m @(insert_eq_0 … (𝟎)) +#m @(insert_eq_1 … (𝟎)) #y * -y [ #H destruct // | #y #_ #H elim (eq_inv_zero_nsucc … H) @@ -124,7 +124,7 @@ qed-. (*** decidable_le le_dec *) lemma nle_dec (m) (n): Decidable … (m ≤ n). -#m #n elim (nle_ge_dis m n) [ /2 width=1 by or_introl/ ] +#m #n elim (nat_split_le_ge m n) [ /2 width=1 by or_introl/ ] #Hnm elim (eq_nat_dec m n) [ #H destruct /2 width=1 by nle_refl, or_introl/ ] /4 width=1 by nle_antisym, or_intror/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_minus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_minus.ma index 507cdd2b6..43e56dac4 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_minus.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_minus.ma @@ -29,19 +29,19 @@ lemma nle_minus_succ_sn (m) (n): ↑n - m ≤ ↑(n - m). // qed. (*** inv_eq_minus_O *) -lemma nle_eq_minus_O (m) (n): 𝟎 = m - n → m ≤ n. +lemma nle_eq_zero_minus (m) (n): 𝟎 = m - n → m ≤ n. #m #n @(nat_ind_2_succ … m n) // /3 width=1 by nle_succ_bi/ qed. (*** monotonic_le_minus_l *) -lemma nle_minus_sn_bi (m) (n) (o): m ≤ n → m-o ≤ n-o. +lemma nle_minus_bi_dx (m) (n) (o): m ≤ n → m-o ≤ n-o. #m #n #o @(nat_ind_succ … o) -o // #o #IH #Hmn /3 width=1 by nle_pred_bi/ qed. (*** monotonic_le_minus_r *) -lemma nle_minus_dx_bi (m) (n) (o): m ≤ n → o-n ≤ o-m. +lemma nle_minus_bi_sn (m) (n) (o): m ≤ n → o-n ≤ o-m. #m #n #o #H elim H -n // #n #_ #IH /2 width=3 by nle_trans/ qed. @@ -53,7 +53,7 @@ lemma nle_minus_sn (o) (m) (n): m ≤ n → m - o ≤ n. (* Inversions with nminus ***************************************************) (*** eq_minus_O *) -lemma nle_inv_eq_minus_O (m) (n): m ≤ n → 𝟎 = m - n. +lemma nle_inv_eq_zero_minus (m) (n): m ≤ n → 𝟎 = m - n. #m #n #H elim H -n // qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_minus_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_minus_plus.ma index 72eff2728..6969fa9f6 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_minus_plus.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_minus_plus.ma @@ -32,22 +32,22 @@ lemma plus_minus_sn_refl_sn_nle (m) (n): n = n - m + m → m ≤ n. (*** le_plus_to_minus *) lemma nle_minus_sn_sn (o) (m) (n): m ≤ n + o → m - o ≤ n. -/2 width=1 by nle_minus_sn_bi/ qed. +/2 width=1 by nle_minus_bi_dx/ qed. (*** le_plus_to_minus_comm *) lemma nle_minus_sn_dx (o) (m) (n): m ≤ o + n → m - o ≤ n. -/2 width=1 by nle_minus_sn_bi/ qed. +/2 width=1 by nle_minus_bi_dx/ qed. (*** le_plus_to_minus_r *) lemma nle_minus_dx_sn (o) (m) (n): m + o ≤ n → m ≤ n - o. #o #m #n #H >(nminus_plus_sn_refl_sn m o) -/2 width=1 by nle_minus_sn_bi/ +/2 width=1 by nle_minus_bi_dx/ qed. (*** le_plus_to_minus_l *) lemma nle_minus_dx_dx (o) (m) (n): o + m ≤ n → m ≤ n - o. #o #m #n #H >(nminus_plus_sn_refl_dx m o) -/2 width=1 by nle_minus_sn_bi/ +/2 width=1 by nle_minus_bi_dx/ qed. (*** le_inv_plus_l *) @@ -113,7 +113,7 @@ theorem nminus_assoc_comm (m1) (m2) (m3): qed-. (*** minus_le_minus_minus_comm *) -theorem minus_assoc_comm_23 (m1) (m2) (m3): +theorem nminus_assoc_comm_23 (m1) (m2) (m3): m3 ≤ m2 → m1 + m3 - m2 = m1 - (m2 - m3). #m1 #m2 #m3 #Hm >(nplus_minus_sn_refl_sn … Hm) in ⊢ (??%?); // diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma index c1dd32661..5e131af37 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma @@ -38,10 +38,6 @@ lemma nle_plus_dx_dx_refl (m) (n): m ≤ m + n. lemma nle_plus_dx_sn_refl (m) (n): m ≤ n + m. /2 width=1 by nle_plus_bi_sn/ qed. -(*** le_plus_b *) -lemma nle_plus_dx_dx (m) (n) (o): n + o ≤ m → n ≤ m. -/2 width=3 by nle_trans/ qed. - (*** le_plus_a *) lemma nle_plus_dx_sn (m) (n) (o): n ≤ m → n ≤ o + m. /2 width=3 by nle_trans/ qed. @@ -55,6 +51,10 @@ theorem nle_plus_bi (m1) (m2) (n1) (n2): (* Inversions with nplus ****************************************************) +(*** le_plus_b *) +lemma nle_inv_plus_sn_dx (m) (n) (o): n + o ≤ m → n ≤ m. +/2 width=3 by nle_trans/ qed. + (*** plus_le_0 *) lemma nle_inv_plus_zero (m) (n): m + n ≤ 𝟎 → ∧∧ 𝟎 = m & 𝟎 = n. /3 width=1 by nle_inv_zero_dx, eq_inv_zero_nplus/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma index cb1021aad..0abb785f7 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma @@ -33,8 +33,11 @@ lemma nlt_i (m) (n): ↑m ≤ n → m < n. lemma nlt_refl_succ (n): n < ↑n. // qed. +lemma nlt_succ_dx (m) (n): m ≤ n → m < ↑n. +/2 width=1 by nle_succ_bi/ qed. + (*** lt_S *) -lemma nlt_succ_dx (m) (n): m < n → m < ↑n. +lemma nlt_succ_dx_trans (m) (n): m < n → m < ↑n. /2 width=1 by nle_succ_dx/ qed. (*** lt_O_S *) @@ -46,51 +49,54 @@ lemma nlt_succ_bi (m) (n): m < n → ↑m < ↑n. /2 width=1 by nle_succ_bi/ qed. (*** le_to_or_lt_eq *) -lemma nle_lt_eq_dis (m) (n): m ≤ n → ∨∨ m < n | m = n. +lemma nle_split_lt_eq (m) (n): m ≤ n → ∨∨ m < n | m = n. #m #n * -n /3 width=1 by nle_succ_bi, or_introl/ qed-. (*** eq_or_gt *) -lemma eq_gt_dis (n): ∨∨ 𝟎 = n | 𝟎 < n. -#n elim (nle_lt_eq_dis (𝟎) n ?) +lemma nat_split_zero_gt (n): ∨∨ 𝟎 = n | 𝟎 < n. +#n elim (nle_split_lt_eq (𝟎) n ?) /2 width=1 by or_introl, or_intror/ qed-. (*** lt_or_ge *) -lemma nlt_ge_dis (m) (n): ∨∨ m < n | n ≤ m. -#m #n elim (nle_ge_dis m n) /2 width=1 by or_intror/ -#H elim (nle_lt_eq_dis … H) -H /2 width=1 by nle_refl, or_introl, or_intror/ +lemma nat_split_lt_ge (m) (n): ∨∨ m < n | n ≤ m. +#m #n elim (nat_split_le_ge m n) /2 width=1 by or_intror/ +#H elim (nle_split_lt_eq … H) -H /2 width=1 by nle_refl, or_introl, or_intror/ qed-. (*** lt_or_eq_or_gt *) -lemma nlt_eq_gt_dis (m) (n): ∨∨ m < n | n = m | n < m. -#m #n elim (nlt_ge_dis m n) /2 width=1 by or3_intro0/ -#H elim (nle_lt_eq_dis … H) -H /2 width=1 by or3_intro1, or3_intro2/ +lemma nat_split_lt_eq_gt (m) (n): ∨∨ m < n | n = m | n < m. +#m #n elim (nat_split_lt_ge m n) /2 width=1 by or3_intro0/ +#H elim (nle_split_lt_eq … H) -H /2 width=1 by or3_intro1, or3_intro2/ qed-. (*** not_le_to_lt *) lemma le_false_nlt (m) (n): (n ≤ m → ⊥) → m < n. -#m #n elim (nlt_ge_dis m n) [ // ] +#m #n elim (nat_split_lt_ge m n) [ // ] #H #Hn elim Hn -Hn // qed. (*** lt_to_le_to_lt *) -lemma nlt_le_trans (o) (m) (n): m < o → o ≤ n → m < n. +lemma nlt_nle_trans (o) (m) (n): m < o → o ≤ n → m < n. /2 width=3 by nle_trans/ qed-. (*** le_to_lt_to_lt *) -lemma le_nlt_trans (o) (m) (n): m ≤ o → o < n → m < n. +lemma nle_nlt_trans (o) (m) (n): m ≤ o → o < n → m < n. /3 width=3 by nle_succ_bi, nle_trans/ qed-. (* Basic inversions *********************************************************) +lemma nlt_inv_succ_dx (m) (n): m < ↑n → m ≤ n. +/2 width=1 by nle_inv_succ_bi/ qed-. + (*** lt_S_S_to_lt *) lemma nlt_inv_succ_bi (m) (n): ↑m < ↑n → m < n. /2 width=1 by nle_inv_succ_bi/ qed-. (*** lt_to_not_le lt_le_false *) lemma nlt_ge_false (m) (n): m < n → n ≤ m → ⊥. -/3 width=4 by nle_inv_succ_sn_refl, nlt_le_trans/ qed-. +/3 width=4 by nle_inv_succ_sn_refl, nlt_nle_trans/ qed-. (*** lt_to_not_eq lt_refl_false *) lemma nlt_inv_refl (m): m < m → ⊥. @@ -107,14 +113,14 @@ lemma nlt_des_le (m) (n): m < n → m ≤ n. /2 width=3 by nle_trans/ qed-. (*** ltn_to_ltO *) -lemma nlt_des_lt_O_sn (m) (n): m < n → 𝟎 < n. -/3 width=3 by le_nlt_trans/ qed-. +lemma nlt_des_lt_zero_sn (m) (n): m < n → 𝟎 < n. +/3 width=3 by nle_nlt_trans/ qed-. (* Main constructions *******************************************************) (*** transitive_lt *) theorem nlt_trans: Transitive … nlt. -/3 width=3 by nlt_des_le, nlt_le_trans/ qed-. +/3 width=3 by nlt_des_le, nlt_nle_trans/ qed-. (* Advanced eliminations ****************************************************) @@ -123,7 +129,7 @@ lemma nat_ind_lt_le (Q:predicate …): #Q #H1 #n @(nat_ind_succ … n) -n [ #m #H <(nle_inv_zero_dx … H) -m @H1 -H1 #o #H elim (nlt_inv_zero_dx … H) -| /5 width=3 by nlt_le_trans, nle_inv_succ_bi/ +| /5 width=3 by nlt_nle_trans, nle_inv_succ_bi/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_minus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_minus.ma index d7654a0bb..5a6c4674b 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_minus.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_minus.ma @@ -20,21 +20,29 @@ include "ground/arith/nat_lt_pred.ma". (* Constructions with nminus ************************************************) (*** monotonic_lt_minus_l *) -lemma nlt_minus_sn_bi (o) (m) (n): o ≤ m → m < n → m - o < n - o. +lemma nlt_minus_bi_dx (o) (m) (n): o ≤ m → m < n → m - o < n - o. #o #m #n #Hom #Hmn -lapply (nle_minus_sn_bi … o Hmn) -Hmn +lapply (nle_minus_bi_dx … o Hmn) -Hmn <(nminus_succ_sn … Hom) // qed. (*** monotonic_lt_minus_r *) -lemma nlt_minus_dx_bi (o) (m) (n): +lemma nlt_minus_bi_sn (o) (m) (n): m < o -> m < n → o-n < o-m. #o #m #n #Ho #H -lapply (nle_minus_dx_bi … o H) -H #H -@(le_nlt_trans … H) -n +lapply (nle_minus_bi_sn … o H) -H #H +@(nle_nlt_trans … H) -n @nlt_i >(nminus_succ_sn … Ho) // qed. +(* Inversions with nminus ***************************************************) + +lemma nlt_inv_minus_bi_dx (o) (m) (n): + m - o < n - o → m < n. +#o @(nat_ind_succ … o) -o +/3 width=1 by nlt_inv_pred_bi/ +qed-. + (* Destructions with nminus *************************************************) (*** minus_pred_pred *) @@ -48,7 +56,7 @@ qed-. lemma nlt_des_minus_dx (o) (m) (n): m < n - o → o < n. #o @(nat_ind_succ … o) -o [ #m #n (nlt_des_gen (𝟎) n) [ /2 width=1 by nlt_succ_bi/ -| /3 width=3 by le_nlt_trans, nlt_le_trans/ +| /3 width=3 by nle_nlt_trans, nlt_nle_trans/ ] qed-. +lemma nlt_inv_pred_bi (m) (n): + ↓m < ↓n → m < n. +/3 width=3 by nlt_inv_pred_dx, nle_nlt_trans/ +qed-. + (* Constructions with npred *************************************************) lemma nlt_zero_sn (n): n = ↑↓n → 𝟎 < n. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma index d975ff3bc..5d3726ca8 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma @@ -22,7 +22,7 @@ definition nminus: nat → nat → nat ≝ λm,n. npred^n m. interpretation - "minus (positive integers)" + "minus (non-negative integers)" 'minus m n = (nminus m n). (* Basic constructions ******************************************************) diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_minus_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus_plus.ma index bb8c911bc..ecda40f03 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_minus_plus.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus_plus.ma @@ -34,7 +34,7 @@ qed. theorem nminus_plus_assoc (o) (m) (n): o-m-n = o-(m+n). #o #m #n @(nat_ind_succ … n) -n // #n #IH yinj_nat_zero #H + /4 width=1 by nle_eq_zero_minus, yle_inj, eq_inv_yinj_nat_bi/ +| #n H12 #H +lapply (yle_inv_plus_bi_sn_inj … H) -H #Hmy2 +generalize in match H12; -H12 (**) (* rewrite in hyp *) +>(yplus_minus1_sn_refl_sn … Hmy2) in ⊢ (%→?); (yplus_minus1_dx_refl_sn … Hnx1) in ⊢ (%→?); -Hnx1 #H +lapply (eq_inv_yplus_bi_sn_inj … H) -H #H12 +/2 width=1 by conj/ +qed-. + +(*** yle_inv_plus_inj2 yle_inv_plus_inj_dx *) +lemma yle_inv_plus_sn_inj_dx (n) (x) (z): + x + yinj_nat n ≤ z → + ∧∧ x ≤ z - n & yinj_nat n ≤ z. +/3 width=3 by yle_plus_sn_dx_minus1_dx, yle_trans, conj/ +qed-. + +(*** yle_inv_plus_inj1 *) +lemma yle_inv_plus_sn_inj_sn (n) (x) (z): + yinj_nat n + x ≤ z → + ∧∧ x ≤ z - n & yinj_nat n ≤ z. +/2 width=1 by yle_inv_plus_sn_inj_dx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_le_minus1_succ.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_le_minus1_succ.ma new file mode 100644 index 000000000..76cfcaf73 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_le_minus1_succ.ma @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||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/arith/ynat_succ.ma". +include "ground/arith/ynat_le_minus1.ma". + +(* ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY ****************************) + +(* Constructions with yminus1 and ysucc *************************************) + +(*** yminus_succ1_inj *) +lemma yminus1_succ_sn (x) (n): + yinj_nat n ≤ x → ↑(x - n) = ↑x - n. +#x @(ynat_split_nat_inf … x) -x // +#m #n #Hnm +ysucc_inj (eq_inv_yinj_nat_bi … H) -n0 + /2 width=3 by ex2_intro/ +| #m0 #H elim (eq_inv_yinj_nat_inf … H) +] +qed-. + +(*** ylt_inv_inj *) +lemma ylt_inv_inj_bi (m) (n): + yinj_nat m < yinj_nat n → m < n. +#m #n #H elim (ylt_inv_inj_dx … H) -H +#x #Hx #H >(eq_inv_yinj_nat_bi … H) -m // +qed-. + +(*** ylt_inv_Y1 *) +lemma ylt_inv_inf_sn (y): ∞ < y → ⊥. +#y #H elim (ylt_des_gen_sn … H) -H +#n #H elim (eq_inv_inf_yinj_nat … H) +qed-. + +lemma ylt_inv_refl (x): x < x → ⊥. +#x @(ynat_split_nat_inf … x) -x +/3 width=2 by ylt_inv_inf_sn, ylt_inv_inj_bi, nlt_inv_refl/ +qed-. + +(* Main constructions *******************************************************) + +(*** ylt_trans *) +theorem ylt_trans: Transitive … ylt. +#x #y * -x -y +[ #m #n #Hxy #z @(ynat_split_nat_inf … z) -z + /4 width=3 by ylt_inv_inj_bi, ylt_inj, nlt_trans/ +| #m #z #H elim (ylt_inv_inf_sn … H) +] +qed-. + +(*** lt_ylt_trans *) +lemma lt_ylt_trans (m) (n) (z): + m < n → yinj_nat n < z → yinj_nat m < z. +/3 width=3 by ylt_trans, ylt_inj/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le.ma new file mode 100644 index 000000000..84edec50f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le.ma @@ -0,0 +1,112 @@ +(**************************************************************************) +(* ___ *) +(* ||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/arith/ynat_le.ma". +include "ground/arith/ynat_lt.ma". + +(* STRICT ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY *********************) + +(* Constructions with yle ***************************************************) + +(*** yle_split_eq *) +lemma yle_split_lt_eq (x) (y): + x ≤ y → ∨∨ x < y | x = y. +#x #y * -x -y +[ #m #n #Hmn elim (nle_split_lt_eq … Hmn) -Hmn + /3 width=1 by or_introl, ylt_inj/ +| #x @(ynat_split_nat_inf … x) -x + /2 width=1 by or_introl, ylt_inf/ +] +qed-. + +(*** ylt_split *) +lemma ynat_split_lt_ge (x) (y): ∨∨ x < y | y ≤ x. +#x #y elim (ynat_split_le_ge x y) /2 width=1 by or_intror/ +#H elim (yle_split_lt_eq … H) -H /2 width=1 by or_introl, or_intror/ +qed-. + +(*** ylt_split_eq *) +lemma ynat_split_lt_eq_gt (x) (y): ∨∨ x < y | y = x | y < x. +#x #y elim (ynat_split_lt_ge x y) /2 width=1 by or3_intro0/ +#H elim (yle_split_lt_eq … H) -H /2 width=1 by or3_intro1, or3_intro2/ +qed-. + +(*** ylt_yle_trans *) +lemma ylt_yle_trans (x) (y) (z): y ≤ z → x < y → x < z. +#x #y #z * -y -z +[ #n #o #Hno #H elim (ylt_inv_inj_dx … H) -H + #m #Hmn #H destruct /3 width=3 by ylt_inj, nlt_nle_trans/ +| #y /2 width=2 by ylt_des_lt_inf_dx/ +] +qed-. + +(*** yle_ylt_trans *) +lemma yle_ylt_trans (x) (y) (z): y < z → x ≤ y → x < z. +#x #y #z * -y -z +[ #n #o #Hno #H elim (yle_inv_inj_dx … H) -H + #m #Hmn #H destruct /3 width=3 by ylt_inj, nle_nlt_trans/ +| #n #H elim (yle_inv_inj_dx … H) -H #m #_ #H destruct // +] +qed-. + +(*** le_ylt_trans *) +lemma nle_ylt_trans (m) (n) (z): + m ≤ n → yinj_nat n < z → yinj_nat m < z. +/3 width=3 by yle_ylt_trans, yle_inj/ qed-. + +(* Inversions with yle ******************************************************) + +(* ylt_yle_false *) +lemma ylt_ge_false (x) (y): x < y → y ≤ x → ⊥. +/3 width=4 by yle_ylt_trans, ylt_inv_refl/ qed-. + +(* Destructions with yle ****************************************************) + +(*** ylt_fwd_le *) +lemma ylt_des_le (x) (y): x < y → x ≤ y. +#x #y * -x -y +/3 width=1 by nlt_des_le, yle_inj/ +qed-. + +(* Eliminations *************************************************************) + +(*** ynat_ind_lt_le_aux *) +lemma ynat_ind_lt_le_inj_dx (Q:predicate …): + (∀y. (∀x. x < y → Q x) → Q y) → + ∀n,x. x ≤ yinj_nat n → Q x. +#Q #IH #n #x #H +elim (yle_inv_inj_dx … H) -H #m #Hmn #H destruct +@(nat_ind_lt_le … Hmn) -Hmn #n0 #IH0 +@IH -IH #x #H +elim (ylt_inv_inj_dx … H) -H #m0 #Hmn0 #H destruct +/2 width=1 by/ +qed-. + +(*** ynat_ind_lt_aux *) +lemma ynat_ind_lt_inj (Q:predicate …): + (∀y. (∀x. x < y → Q x) → Q y) → + ∀n. Q (yinj_nat n). +/4 width=2 by ynat_ind_lt_le_inj_dx/ qed-. + +(*** ynat_ind_lt *) +lemma ynat_ind_lt (Q:predicate …): + (∀y. (∀x. x < y → Q x) → Q y) → + ∀y. Q y. +#Q #IH #y @(ynat_split_nat_inf … y) -y +[ /4 width=1 by ynat_ind_lt_inj/ +| @IH #x #H + elim (ylt_des_gen_sn … H) -H #m #H destruct + /4 width=1 by ynat_ind_lt_inj/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_minus1.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_minus1.ma new file mode 100644 index 000000000..73b5817fb --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_minus1.ma @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||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/arith/nat_lt_minus.ma". +include "ground/arith/ynat_minus1.ma". +include "ground/arith/ynat_le.ma". +include "ground/arith/ynat_lt.ma". + +(* STRICT ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY *********************) + +(* Cobstructions with yle and yminus1 **************************************) + +(*** monotonic_ylt_minus_dx *) +lemma ylt_minus1_bi_dx (o) (x) (y): + x < y → yinj_nat o ≤ x → x - o < y - o. +#o #x #y * -x -y +/4 width=1 by ylt_inj, yle_inv_inj_bi, nlt_minus_bi_dx/ +qed. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_minus1_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_minus1_plus.ma new file mode 100644 index 000000000..bd5ce71bc --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_minus1_plus.ma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||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/arith/ynat_minus1_plus.ma". +include "ground/arith/ynat_lt_le_minus1.ma". + +(* STRICT ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY *********************) + +(* Constructions with yle and yminus1 and yplus ****************************) + +(*** ylt_plus2_to_minus_inj2 *) +lemma ylt_plus_dx_dx_minus1_sn (o) (x) (y): + yinj_nat o ≤ x → x < y + yinj_nat o → x - o < y. +/2 width=1 by ylt_minus1_bi_dx/ qed. + +(*** ylt_plus2_to_minus_inj1 *) +lemma ylt_plus_dx_sn_minus1_sn (o) (x) (y): + yinj_nat o ≤ x → x < yinj_nat o + y → x - o < y. +/2 width=1 by ylt_plus_dx_dx_minus1_sn/ qed. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_plus.ma new file mode 100644 index 000000000..8b6f18b6b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_plus.ma @@ -0,0 +1,64 @@ +(**************************************************************************) +(* ___ *) +(* ||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/arith/ynat_le_plus.ma". +include "ground/arith/ynat_lt_plus.ma". +include "ground/arith/ynat_lt_le.ma". + +(* STRICT ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY *********************) + +(* Constructions with yle and yplus *****************************************) + +(*** monotonic_ylt_plus_inj *) +lemma ylt_yle_plus_bi_inj (x1) (x2) (n1) (y2): + x1 < x2 → yinj_nat n1 ≤ y2 → x1 + yinj_nat n1 < x2 + y2. +/3 width=3 by ylt_plus_bi_dx_inj, yle_plus_bi_sn, ylt_yle_trans/ +qed. + +(*** monotonic_ylt_plus *) +lemma ylt_yle_plus_bi (x1) (x2) (y1) (y2): + x1 < x2 → y1 < ∞ → y1 ≤ y2 → x1 + y1 < x2 + y2. +#x1 #x2 #y1 #y2 #Hx12 #Hy1 #Hy12 +elim (ylt_des_gen_sn … Hy1) -Hy1 #n1 #H destruct +/2 width=1 by ylt_yle_plus_bi_inj/ +qed. + +(* Inversions with yle and yplus ********************************************) + +(*** yle_inv_monotonic_plus_dx *) +lemma yle_inv_plus_bi_dx (z) (x) (y): + z < ∞ → x + z ≤ y + z → x ≤ y. +#z #x #y #Hz #Hxy +elim (ylt_des_gen_sn … Hz) -Hz #o #H destruct +/2 width=2 by yle_inv_plus_bi_sn_inj/ +qed-. + +(*** yle_inv_monotonic_plus_sn *) +lemma yle_inv_plus_bi_sn (z) (x) (y): + z < ∞ → z + x ≤ z + y → x ≤ y. +/2 width=3 by yle_inv_plus_bi_dx/ qed-. + +(* Destructions with yle and yplus ******************************************) + +(*** ylt_fwd_plus_ge *) +lemma ylt_des_plus_bi_sn_ge (x1) (x2) (y1) (y2): + x2 ≤ x1 → x1 + y1 < x2 + y2 → y1 < y2. +#x1 #x2 #y1 #y2 #Hx21 #Hxy +elim (ylt_des_gen_sn … Hxy) #o #H +elim (eq_inv_yplus_inj … H) -H #m1 #n1 #_ #H2 #H3 destruct -o +elim (yle_inv_inj_dx … Hx21) #m2 #_ #H destruct +lapply (ylt_yle_plus_bi_inj … Hxy … Hx21) -Hxy -Hx21 +yinj_nat_zero >(nminus_refl m) +/4 width=1 by ylt_inj, ylt_inv_inj_bi, nlt_minus_bi_dx/ +qed. + +(* Inversions with yminus1 **************************************************) + +(*** yminus_to_lt *) +lemma ylt_inv_zero_minus1 (m) (y): + (𝟎) < y - m → yinj_nat m < y. +#m #y @(ynat_split_nat_inf … y) -y // +#n yinj_nat_zero >(nminus_refl m) #Hmm +/4 width=2 by ylt_inv_inj_bi, ylt_inj, nlt_inv_minus_bi_dx/ +qed-. + +(* Destructions with yminus1 ************************************************) + +(*** yminus_pred *) +lemma yminus1_pred_bi (x:ynat) (n): + (𝟎) < x → 𝟎 < n → x - n = ↓x - ↓n. +#x @(ynat_split_nat_inf … x) -x // +#m #n >yinj_nat_zero +#Hm #Hn ysucc_inj ysucc_inj (ylt_des_gen_dx … Hy) -Hy +(ylt_des_gen_dx … Hx) -Hx +ysucc_inj >ysucc_inj yplus_assoc // +qed. + +lemma yplus_plus_comm_13 (x) (y) (z): + x + z + y = y + z + x. +// qed. + +(*** yplus_comm_24 *) +lemma yplus_plus_comm_24 (x1) (x4) (x2) (x3): + x1 + x4 + x3 + x2 = x1 + x2 + x3 + x4. +#x1 #x4 #x2 #x3 +>yplus_assoc >yplus_assoc >yplus_assoc >yplus_assoc // +qed. + +(*** yplus_assoc_23 *) +lemma yplus_plus_assoc_23 (x1) (x4) (x2) (x3): + x1 + (x2 + x3) + x4 = x1 + x2 + (x3 + x4). +#x1 #x4 #x2 #x3 +>yplus_assoc >yplus_assoc // +qed. + +(* Basic inversions *********************************************************) + +(*** yplus_inv_Y1 *) +lemma eq_inv_inf_plus (x) (y): + ∞ = x + y → ∨∨ ∞ = x | ∞ = y. +#x @(ynat_split_nat_inf … x) -x /2 width=1 by or_introl/ +#m #y @(ynat_split_nat_inf … y) -y /2 width=1 by or_introl/ +#n ysucc_inj yplus_comm /2 width=2 by ex2_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/insert_eq/insert_eq_0.ma b/matita/matita/contribs/lambdadelta/ground/insert_eq/insert_eq_1.ma similarity index 90% rename from matita/matita/contribs/lambdadelta/ground/insert_eq/insert_eq_0.ma rename to matita/matita/contribs/lambdadelta/ground/insert_eq/insert_eq_1.ma index 6a3788e7d..4652c2e86 100644 --- a/matita/matita/contribs/lambdadelta/ground/insert_eq/insert_eq_0.ma +++ b/matita/matita/contribs/lambdadelta/ground/insert_eq/insert_eq_1.ma @@ -16,5 +16,6 @@ include "basics/relations.ma". (* GENERATED LIBRARY ********************************************************) -lemma insert_eq_0: ∀A,a. ∀Q1,Q2:predicate A. (∀a0. Q1 a0 → a = a0 → Q2 a0) → Q1 a → Q2 a. +lemma insert_eq_1 (T1) (a1) (Q1,Q2:predicate T1): + (∀b1. Q1 b1 → a1 = b1 → Q2 b1) → Q1 a1 → Q2 a1. /2 width=1 by/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground/lib/arith.ma deleted file mode 100644 index 6cbf86985..000000000 --- a/matita/matita/contribs/lambdadelta/ground/lib/arith.ma +++ /dev/null @@ -1,417 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 "basics/core_notation/exp_2.ma". -include "arithmetics/nat.ma". -include "ground/xoa/ex_3_1.ma". -include "ground/xoa/or_3.ma". -include "ground/notation/functions/uparrow_1.ma". -include "ground/notation/functions/downarrow_1.ma". -include "ground/pull/pull_2.ma". -include "ground/lib/relations.ma". - -(* ARITHMETICAL PROPERTIES **************************************************) - -interpretation "nat successor" 'UpArrow m = (S m). - -interpretation "nat predecessor" 'DownArrow m = (pred m). - -interpretation "nat min" 'and x y = (min x y). - -interpretation "nat max" 'or x y = (max x y). - -(* Iota equations ***********************************************************) - -lemma pred_O: pred 0 = 0. -normalize // qed. - -lemma pred_S: ∀m. pred (S m) = m. -// qed. - -lemma plus_S1: ∀x,y. ↑(x+y) = (↑x) + y. -// qed. - -lemma max_O1: ∀n. n = (0 ∨ n). -// qed. - -lemma max_O2: ∀n. n = (n ∨ 0). -// qed. - -lemma max_SS: ∀n1,n2. ↑(n1∨n2) = (↑n1 ∨ ↑n2). -#n1 #n2 elim (decidable_le n1 n2) #H normalize -[ >(le_to_leb_true … H) | >(not_le_to_leb_false … H) ] -H // -qed. - -(* Equalities ***************************************************************) - -lemma plus_SO_sn (n): 1 + n = ↑n. -// qed-. - -lemma plus_SO_dx (n): n + 1 = ↑n. -// qed. - -lemma minus_SO_dx (n): n-1 = ↓n. -// qed. - -lemma minus_plus_m_m_commutative: ∀n,m:nat. n = m + n - m. -// qed-. - -lemma plus_minus_m_m_commutative (n) (m): m ≤ n → n = m+(n-m). -/2 width=1 by plus_minus_associative/ qed-. - -lemma plus_to_minus_2: ∀m1,m2,n1,n2. n1 ≤ m1 → n2 ≤ m2 → - m1+n2 = m2+n1 → m1-n1 = m2-n2. -#m1 #m2 #n1 #n2 #H1 #H2 #H -@plus_to_minus >plus_minus_associative // -qed-. - -(* Note: uses minus_minus_comm, minus_plus_m_m, commutative_plus, plus_minus *) -lemma plus_minus_minus_be: ∀x,y,z. y ≤ z → z ≤ x → (x - z) + (z - y) = x - y. -#x #z #y #Hzy #Hyx >plus_minus // >commutative_plus >plus_minus // -qed-. - -lemma lt_succ_pred: ∀m,n. n < m → m = ↑↓m. -#m #n #Hm >S_pred /2 width=2 by ltn_to_ltO/ -qed-. - -fact plus_minus_minus_be_aux: ∀i,x,y,z. y ≤ z → z ≤ x → i = z - y → x - z + i = x - y. -/2 width=1 by plus_minus_minus_be/ qed-. - -lemma le_plus_minus: ∀m,n,p. p ≤ n → m + n - p = m + (n - p). -/2 by plus_minus/ qed-. - -lemma le_plus_minus_comm: ∀n,m,p. p ≤ m → m + n - p = m - p + n. -/2 by plus_minus/ qed-. - -lemma minus_minus_comm3: ∀n,x,y,z. n-x-y-z = n-y-z-x. -// qed. - -lemma idempotent_max: ∀n:nat. n = (n ∨ n). -#n normalize >le_to_leb_true // -qed. - -lemma associative_max: associative … max. -#x #y #z normalize -@(leb_elim x y) normalize #Hxy -@(leb_elim y z) normalize #Hyz // -[1,2: >le_to_leb_true /2 width=3 by transitive_le/ -| >not_le_to_leb_false /4 width=3 by lt_to_not_le, not_le_to_lt, transitive_lt/ - >not_le_to_leb_false // -] -qed. - -(* Properties ***************************************************************) - -lemma eq_nat_dec: ∀n1,n2:nat. Decidable (n1 = n2). -#n1 elim n1 -n1 [| #n1 #IHn1 ] * [2,4: #n2 ] -[1,4: @or_intror #H destruct -| elim (IHn1 n2) -IHn1 /3 width=1 by or_intror, or_introl/ -| /2 width=1 by or_introl/ -] -qed-. - -lemma lt_or_eq_or_gt: ∀m,n. ∨∨ m < n | n = m | n < m. -#m #n elim (lt_or_ge m n) /2 width=1 by or3_intro0/ -#H elim H -m /2 width=1 by or3_intro1/ -#m #Hm * /3 width=1 by not_le_to_lt, le_S_S, or3_intro2/ -qed-. - -lemma monotonic_le_minus_l2: ∀x1,x2,y,z. x1 ≤ x2 → x1 - y - z ≤ x2 - y - z. -/3 width=1 by monotonic_le_minus_l/ qed. - -lemma minus_le_trans_sn: ∀x1,x2. x1 ≤ x2 → ∀x. x1-x ≤ x2. -/2 width=3 by transitive_le/ qed. - -lemma le_plus_to_minus_l: ∀a,b,c. a + b ≤ c → b ≤ c-a. -/2 width=1 by le_plus_to_minus_r/ -qed-. - -lemma le_plus_to_minus_comm: ∀n,m,p. n ≤ p+m → n-p ≤ m. -/2 width=1 by le_plus_to_minus/ qed-. - -lemma le_inv_S1: ∀m,n. ↑m ≤ n → ∃∃p. m ≤ p & ↑p = n. -#m * -[ #H lapply (le_n_O_to_eq … H) -H - #H destruct -| /3 width=3 by monotonic_pred, ex2_intro/ -] -qed-. - -(* Note: this might interfere with nat.ma *) -lemma monotonic_lt_pred: ∀m,n. m < n → 0 < m → pred m < pred n. -#m #n #Hmn #Hm whd >(S_pred … Hm) -@le_S_S_to_le >S_pred /2 width=3 by transitive_lt/ -qed. - -lemma lt_S_S: ∀x,y. x < y → ↑x < ↑y. -/2 width=1 by le_S_S/ qed. - -lemma lt_S: ∀n,m. n < m → n < ↑m. -/2 width=1 by le_S/ qed. - -lemma monotonic_lt_minus_r: -∀p,q,n. q < n -> q < p → n-p < n-q. -#p #q #n #Hn #H -lapply (monotonic_le_minus_r … n H) -H #H -@(le_to_lt_to_lt … H) -H -/2 width=1 by lt_plus_to_minus/ -qed. - -lemma max_S1_le_S: ∀n1,n2,n. (n1 ∨ n2) ≤ n → (↑n1 ∨ n2) ≤ ↑n. -/4 width=2 by to_max, le_maxr, le_S_S, le_S/ qed-. - -lemma max_S2_le_S: ∀n1,n2,n. (n1 ∨ n2) ≤ n → (n1 ∨ ↑n2) ≤ ↑n. -/2 width=1 by max_S1_le_S/ qed-. - -(* Inversion & forward lemmas ***********************************************) - -lemma lt_refl_false: ∀n. n < n → ⊥. -#n #H elim (lt_to_not_eq … H) -H /2 width=1 by/ -qed-. - -lemma lt_zero_false: ∀n. n < 0 → ⊥. -#n #H elim (lt_to_not_le … H) -H /2 width=1 by/ -qed-. - -lemma lt_le_false: ∀x,y. x < y → y ≤ x → ⊥. -/3 width=4 by lt_refl_false, lt_to_le_to_lt/ qed-. - -lemma le_dec (n) (m): Decidable (n≤m). -#n elim n -n [ /2 width=1 by or_introl/ ] -#n #IH * [ /3 width=2 by lt_zero_false, or_intror/ ] -#m elim (IH m) -IH -[ /3 width=1 by or_introl, le_S_S/ -| /4 width=1 by or_intror, le_S_S_to_le/ -] -qed-. - -lemma succ_inv_refl_sn: ∀x. ↑x = x → ⊥. -#x #H @(lt_le_false x (↑x)) // -qed-. - -lemma le_plus_xSy_O_false: ∀x,y. x + S y ≤ 0 → ⊥. -#x #y #H lapply (le_n_O_to_eq … H) -H H -H -/2 width=2 by le_plus_to_le/ -qed-. - -lemma plus2_le_sn_dx: ∀m1,m2,n1,n2. m1 + n1 = n2 + m2 → m1 ≤ m2 → n2 ≤ n1. -/2 width=4 by plus2_le_sn_sn/ qed-. - -lemma plus2_le_dx_sn: ∀m1,m2,n1,n2. n1 + m1 = m2 + n2 → m1 ≤ m2 → n2 ≤ n1. -/2 width=4 by plus2_le_sn_sn/ qed-. - -lemma plus2_le_dx_dx: ∀m1,m2,n1,n2. n1 + m1 = n2 + m2 → m1 ≤ m2 → n2 ≤ n1. -/2 width=4 by plus2_le_sn_sn/ qed-. - -lemma lt_S_S_to_lt: ∀x,y. ↑x < ↑y → x < y. -/2 width=1 by le_S_S_to_le/ qed-. - -(* Note this should go in nat.ma *) -lemma discr_x_minus_xy: ∀x,y. x = x - y → x = 0 ∨ y = 0. -#x @(nat_ind_plus … x) -x /2 width=1 by or_introl/ -#x #_ #y @(nat_ind_plus … y) -y /2 width=1 by or_intror/ -#y #_ >minus_plus_plus_l -#H lapply (discr_plus_xy_minus_xz … H) -H -#H destruct -qed-. - -lemma lt_inv_O1: ∀n. 0 < n → ∃m. ↑m = n. -* /2 width=2 by ex_intro/ -#H cases (lt_le_false … H) -H // -qed-. - -lemma lt_inv_S1: ∀m,n. ↑m < n → ∃∃p. m < p & ↑p = n. -#m * /3 width=3 by lt_S_S_to_lt, ex2_intro/ -#H cases (lt_le_false … H) -H // -qed-. - -lemma lt_inv_gen: ∀y,x. x < y → ∃∃z. x ≤ z & ↑z = y. -* /3 width=3 by le_S_S_to_le, ex2_intro/ -#x #H elim (lt_le_false … H) -H // -qed-. - -lemma plus_inv_O3: ∀x,y. x + y = 0 → x = 0 ∧ y = 0. -/2 width=1 by plus_le_0/ qed-. - -lemma plus_inv_S3_sn: ∀x1,x2,x3. x1+x2 = ↑x3 → - ∨∨ ∧∧ x1 = 0 & x2 = ↑x3 - | ∃∃y1. x1 = ↑y1 & y1 + x2 = x3. -* /3 width=1 by or_introl, conj/ -#x1 #x2 #x3 + + Primitive arithmetics library. + Specification is repackaged for publication. diff --git a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl index 6f52a0d68..e79511f7c 100644 --- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl +++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl @@ -46,18 +46,26 @@ table { } ] class "grass" - [ { "natural numbers with infinity" * } { - [ { "" * } { - [ "ynat ( ∞ )" "ynat_pred ( ↓? )" "ynat_succ ( ↑? )" - "ynat_le ( ? ≤ ? )" "ynat_lt ( ? < ? )" - "ynat_plus ( ? + ? )" "ynat_minus_sn ( ? - ? )" * - ] + [ { "arithmetics" * } { + [ { "extensions" * } { + [ "arith_2a ( 𝟐 )" "arith_2b" * ] + } + ] + [ { "well-founded induction" * } { + [ "wf1_ind_ylt" * ] + [ "wf1_ind_nlt" "wf2_ind_nlt" "wf3_ind_nlt.ma" * ] + } + ] + [ { "non-negative integers with infinity" * } { + [ "ynat_lt ( ?<? )" "ynat_lt_succ" "ynat_lt_pred" "ynat_lt_pred_succ" "ynat_lt_plus" "ynat_lt_plus_pred" "ynat_lt_minus1" "ynat_lt_minus1_plus" "ynat_lt_le" "ynat_lt_le_succ" "ynat_lt_le_pred" "ynat_lt_le_pred_succ" "ynat_lt_le_plus" "ynat_lt_le_minus1" "ynat_lt_le_minus1_plus" * ] + [ "ynat_le ( ?≤? )" "ynat_le_succ" "ynat_le_pred" "ynat_le_pred_succ" "ynat_le_plus" "ynat_le_minus1" "ynat_le_minus1_succ" "ynat_le_minus1_plus" * ] + [ "ynat_minus1 ( ?-? )" "ynat_minus1_succ" "ynat_minus1_plus" * ] + [ "ynat_plus ( ?+? )" * ] + [ "ynat_pred ( ↓? )" "ynat_pred_succ" * ] + [ "ynat_succ ( ↑? )" * ] + [ "ynat ( 𝟎 ) ( ∞ )" "ynat_nat" * ] } ] - } - ] - class "grass" - [ { "arithmetics" * } { [ { "non-negative integers" * } { [ "nat_lt ( ?<? )" "nat_lt_tri" "nat_lt_pred" "nat_lt_plus" "nat_lt_minus" "nat_lt_minus_plus" * ] [ "nat_le ( ?≤? )" "nat_le_pred" "nat_le_plus" "nat_le_minus" "nat_le_minus_plus" "nat_le_max" * ] @@ -71,7 +79,7 @@ table { ] [ { "positive integers" * } { [ "pnat_plus ( ?+? )" * ] - [ "pnat ( 𝟏 ) ( ↑? )" "pnat_dis" "pnat_iter ( ?^{?}? )" *"pnat_tri" ] + [ "pnat ( 𝟏 ) ( ↑? )" "pnat_dis" "pnat_iter ( ?^{?}? )" "pnat_tri" * ] } ] } @@ -81,7 +89,7 @@ table { [ { "" * } { [ "stream ( ? ⨮{?} ? )" "stream_eq ( ? ≗{?} ? )" "stream_hdtl ( ⫰{?}? )" "stream_tls ( ⫰*{?}[?]? )" * ] [ "list ( Ⓔ{?} ) ( ? ⨮{?} ? )" "list_length ( |?| )" * ] - [ "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? ) ( ↑? ) ( ↓? ) ( ? ∨ ? ) ( ? ∧ ? )" "arith_2a" "arith_2b" * ] + [ "bool ( Ⓕ ) ( Ⓣ )" * ] [ "ltc" "ltc_ctc" * ] [ "logic ( ⊥ ) ( ⊤ )" "relations ( ? ⊆ ? )" "functions" "exteq ( ? ≐{?,?} ? )" "star" "lstar_2a" * ] } @@ -90,10 +98,6 @@ table { ] class "orange" [ { "generated library" * } { - [ { "well-founded induction" * } { - [ "wf1_ind_nlt" "wf2_ind_nlt" "wf3_ind_nlt.ma" * ] - } - ] [ { "generalization with equality" * } { [ "insert_eq" * ] } diff --git a/matita/matita/contribs/lambdadelta/ground/ynat/ynat_le.ma b/matita/matita/contribs/lambdadelta/ground/ynat/ynat_le.ma deleted file mode 100644 index 29e11ce3c..000000000 --- a/matita/matita/contribs/lambdadelta/ground/ynat/ynat_le.ma +++ /dev/null @@ -1,155 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/ynat/ynat_succ.ma". - -(* NATURAL NUMBERS WITH INFINITY ********************************************) - -(* order relation *) -inductive yle: relation ynat ≝ -| yle_inj: ∀m,n. m ≤ n → yle m n -| yle_Y : ∀m. yle m (∞) -. - -interpretation "ynat 'less or equal to'" 'leq x y = (yle x y). - -(* Basic inversion lemmas ***************************************************) - -fact yle_inv_inj2_aux: ∀x,y. x ≤ y → ∀n. y = yinj n → - ∃∃m. m ≤ n & x = yinj m. -#x #y * -x -y -[ #x #y #Hxy #n #Hy destruct /2 width=3 by ex2_intro/ -| #x #n #Hy destruct -] -qed-. - -lemma yle_inv_inj2: ∀x,n. x ≤ yinj n → ∃∃m. m ≤ n & x = yinj m. -/2 width=3 by yle_inv_inj2_aux/ qed-. - -lemma yle_inv_inj: ∀m,n. yinj m ≤ yinj n → m ≤ n. -#m #n #H elim (yle_inv_inj2 … H) -H -#x #Hxn #H destruct // -qed-. - -fact yle_inv_O2_aux: ∀m:ynat. ∀x:ynat. m ≤ x → x = 0 → m = 0. -#m #x * -m -x -[ #m #n #Hmn #H destruct /3 width=1 by le_n_O_to_eq, eq_f/ -| #m #H destruct -] -qed-. - -lemma yle_inv_O2: ∀m:ynat. m ≤ 0 → m = 0. -/2 width =3 by yle_inv_O2_aux/ qed-. - -fact yle_inv_Y1_aux: ∀x,n. x ≤ n → x = ∞ → n = ∞. -#x #n * -x -n // -#x #n #_ #H destruct -qed-. - -lemma yle_inv_Y1: ∀n. ∞ ≤ n → n = ∞. -/2 width=3 by yle_inv_Y1_aux/ qed-. - -lemma yle_antisym: ∀y,x. x ≤ y → y ≤ x → x = y. -#x #y #H elim H -x -y -/4 width=1 by yle_inv_Y1, yle_inv_inj, le_to_le_to_eq, eq_f/ -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. - -lemma yle_split: ∀x,y:ynat. x ≤ y ∨ y ≤ x. -* /2 width=1 by or_intror/ -#x * /2 width=1 by or_introl/ -#y elim (le_or_ge x y) /3 width=1 by yle_inj, or_introl, or_intror/ -qed-. - -(* Inversion lemmas on successor ********************************************) - -fact yle_inv_succ1_aux: ∀x,y:ynat. x ≤ y → ∀m. x = ↑m → m ≤ ↓y ∧ ↑↓y = y. -#x #y * -x -y -[ #x #y #Hxy #m #H elim (ysucc_inv_inj_sn … H) -H - #n #H1 #H2 destruct elim (le_inv_S1 … Hxy) -Hxy - #m #Hnm #H destruct /3 width=1 by yle_inj, conj/ -| #x #y #H destruct /2 width=1 by yle_Y, conj/ -] -qed-. - -lemma yle_inv_succ1: ∀m,y:ynat. ↑m ≤ y → m ≤ ↓y ∧ ↑↓y = y. -/2 width=3 by yle_inv_succ1_aux/ qed-. - -lemma yle_inv_succ: ∀m,n. ↑m ≤ ↑n → m ≤ n. -#m #n #H elim (yle_inv_succ1 … H) -H // -qed-. - -lemma yle_inv_succ2: ∀x,y. x ≤ ↑y → ↓x ≤ y. -#x #y #Hxy elim (ynat_cases x) -[ #H destruct // -| * #m #H destruct /2 width=1 by yle_inv_succ/ -] -qed-. - -(* Properties on predecessor ************************************************) - -lemma yle_pred_sn: ∀m,n. m ≤ n → ↓m ≤ n. -#m #n * -m -n /3 width=3 by transitive_le, yle_inj/ -qed. - -lemma yle_refl_pred_sn: ∀x. ↓x ≤ x. -/2 width=1 by yle_refl, yle_pred_sn/ qed. - -lemma yle_pred: ∀m,n. m ≤ n → ↓m ≤ ↓n. -#m #n * -m -n /3 width=1 by yle_inj, monotonic_pred/ -qed. - -(* 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. - -lemma yle_refl_S_dx: ∀x. x ≤ ↑x. -/2 width=1 by yle_succ_dx/ qed. - -lemma yle_refl_SP_dx: ∀x. x ≤ ↑↓x. -* // * // -qed. - -lemma yle_succ2: ∀x,y. ↓x ≤ y → x ≤ ↑y. -#x #y #Hxy elim (ynat_cases x) -[ #H destruct // -| * #m #H destruct /2 width=1 by yle_succ/ -] -qed-. - -(* Main properties **********************************************************) - -theorem yle_trans: Transitive … yle. -#x #y * -x -y -[ #x #y #Hxy * // - #z #H lapply (yle_inv_inj … H) -H - /3 width=3 by transitive_le, yle_inj/ (**) (* full auto too slow *) -| #x #z #H lapply (yle_inv_Y1 … H) // -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/ynat/ynat_lt.ma b/matita/matita/contribs/lambdadelta/ground/ynat/ynat_lt.ma deleted file mode 100644 index 0ab7bee45..000000000 --- a/matita/matita/contribs/lambdadelta/ground/ynat/ynat_lt.ma +++ /dev/null @@ -1,271 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/ynat/ynat_le.ma". - -(* NATURAL NUMBERS WITH INFINITY ********************************************) - -(* strict order relation *) -inductive ylt: relation ynat ≝ -| ylt_inj: ∀m,n. m < n → ylt m n -| ylt_Y : ∀m:nat. ylt m (∞) -. - -interpretation "ynat 'less than'" 'lt x y = (ylt x y). - -(* Basic forward lemmas *****************************************************) - -lemma ylt_fwd_gen: ∀x,y. x < y → ∃m. x = yinj m. -#x #y * -x -y /2 width=2 by ex_intro/ -qed-. - -lemma ylt_fwd_lt_O1: ∀x,y:ynat. x < y → 0 < y. -#x #y #H elim H -x -y /3 width=2 by ylt_inj, ltn_to_ltO/ -qed-. - -(* Basic inversion lemmas ***************************************************) - -fact ylt_inv_inj2_aux: ∀x,y. x < y → ∀n. y = yinj n → - ∃∃m. m < n & x = yinj m. -#x #y * -x -y -[ #x #y #Hxy #n #Hy elim (le_inv_S1 … Hxy) -Hxy - #m #Hm #H destruct /3 width=3 by le_S_S, ex2_intro/ -| #x #n #Hy destruct -] -qed-. - -lemma ylt_inv_inj2: ∀x,n. x < yinj n → - ∃∃m. m < n & x = yinj m. -/2 width=3 by ylt_inv_inj2_aux/ qed-. - -lemma ylt_inv_inj: ∀m,n. yinj m < yinj n → m < n. -#m #n #H elim (ylt_inv_inj2 … H) -H -#x #Hx #H destruct // -qed-. - -lemma ylt_inv_Y1: ∀n. ∞ < n → ⊥. -#n #H elim (ylt_fwd_gen … H) -H -#y #H destruct -qed-. - -lemma ylt_inv_Y2: ∀x:ynat. x < ∞ → ∃n. x = yinj n. -* /2 width=2 by ex_intro/ -#H elim (ylt_inv_Y1 … H) -qed-. - -lemma ylt_inv_O1: ∀n:ynat. 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:ynat. x < y → ∀m. x = ↑m → m < ↓y ∧ ↑↓y = y. -#x #y * -x -y -[ #x #y #Hxy #m #H elim (ysucc_inv_inj_sn … H) -H - #n #H1 #H2 destruct elim (le_inv_S1 … Hxy) -Hxy - #m #Hnm #H destruct /3 width=1 by ylt_inj, conj/ -| #x #y #H elim (ysucc_inv_inj_sn … H) -H - #m #H #_ destruct /2 width=1 by ylt_Y, conj/ -] -qed-. - -lemma ylt_inv_succ1: ∀m,y:ynat. ↑m < y → m < ↓y ∧ ↑↓y = y. -/2 width=3 by ylt_inv_succ1_aux/ qed-. - -lemma ylt_inv_succ: ∀m,n. ↑m < ↑n → m < n. -#m #n #H elim (ylt_inv_succ1 … H) -H // -qed-. - -(* Forward lemmas on successor **********************************************) - -fact ylt_fwd_succ2_aux: ∀x,y. x < y → ∀n. y = ↑n → x ≤ n. -#x #y * -x -y -[ #x #y #Hxy #m #H elim (ysucc_inv_inj_sn … H) -H - #n #H1 #H2 destruct /3 width=1 by yle_inj, le_S_S_to_le/ -| #x #n #H lapply (ysucc_inv_Y_sn … H) -H // -] -qed-. - -lemma ylt_fwd_succ2: ∀m,n. m < ↑n → m ≤ n. -/2 width=3 by ylt_fwd_succ2_aux/ qed-. - -(* inversion and forward lemmas on order ************************************) - -lemma ylt_fwd_le_succ1: ∀m,n. m < n → ↑m ≤ n. -#m #n * -m -n /2 width=1 by yle_inj/ -qed-. - -lemma ylt_fwd_le_pred2: ∀x,y:ynat. x < y → x ≤ ↓y. -#x #y #H elim H -x -y /3 width=1 by yle_inj, monotonic_pred/ -qed-. - -lemma ylt_fwd_le: ∀m:ynat. ∀n:ynat. m < n → m ≤ n. -#m #n * -m -n /3 width=1 by lt_to_le, yle_inj/ -qed-. - -lemma ylt_yle_false: ∀m:ynat. ∀n:ynat. m < n → n ≤ m → ⊥. -#m #n * -m -n -[ #m #n #Hmn #H lapply (yle_inv_inj … H) -H - #H elim (lt_refl_false n) /2 width=3 by le_to_lt_to_lt/ -| #m #H lapply (yle_inv_Y1 … H) -H - #H destruct -] -qed-. - -lemma ylt_inv_le: ∀x,y. x < y → x < ∞ ∧ ↑x ≤ y. -#x #y #H elim H -x -y /3 width=1 by yle_inj, conj/ -qed-. - -(* Basic properties *********************************************************) - -lemma ylt_O1: ∀x:ynat. ↑↓x = x → 0 < x. -* // * /2 width=1 by ylt_inj/ normalize -#H destruct -qed. - -lemma yle_inv_succ_sn_lt (x:ynat) (y:ynat): - ↑x ≤ y → ∧∧ x ≤ ↓y & 0 < y. -#x #y #H elim (yle_inv_succ1 … H) -H /3 width=2 by ylt_O1, conj/ -qed-. - -(* Properties on predecessor ************************************************) - -lemma ylt_pred: ∀m,n:ynat. m < n → 0 < m → ↓m < ↓n. -#m #n * -m -n -/4 width=1 by ylt_inv_inj, ylt_inj, monotonic_lt_pred/ -qed. - -(* Properties on successor **************************************************) - -lemma ylt_O_succ: ∀x:ynat. 0 < ↑x. -* /2 width=1 by ylt_inj/ -qed. - -lemma ylt_succ: ∀m,n. m < n → ↑m < ↑n. -#m #n #H elim H -m -n /3 width=1 by ylt_inj, le_S_S/ -qed. - -lemma ylt_succ_Y: ∀x. x < ∞ → ↑x < ∞. -* /2 width=1 by/ qed. - -lemma yle_succ1_inj: ∀x. ∀y:ynat. ↑yinj x ≤ y → x < y. -#x * /3 width=1 by yle_inv_inj, ylt_inj/ -qed. - -lemma ylt_succ2_refl: ∀x,y:ynat. x < y → x < ↑x. -#x #y #H elim (ylt_fwd_gen … H) -y /2 width=1 by ylt_inj/ -qed. - -(* Properties on order ******************************************************) - -lemma yle_split_eq: ∀m,n:ynat. m ≤ n → m < n ∨ m = n. -#m #n * -m -n -[ #m #n #Hmn elim (le_to_or_lt_eq … Hmn) -Hmn - /3 width=1 by or_introl, ylt_inj/ -| * /2 width=1 by or_introl, ylt_Y/ -] -qed-. - -lemma ylt_split: ∀m,n:ynat. m < n ∨ n ≤ m. -#m #n elim (yle_split m n) /2 width=1 by or_intror/ -#H elim (yle_split_eq … H) -H /2 width=1 by or_introl, or_intror/ -qed-. - -lemma ylt_split_eq: ∀m,n:ynat. ∨∨ m < n | n = m | n < m. -#m #n elim (ylt_split m n) /2 width=1 by or3_intro0/ -#H elim (yle_split_eq … H) -H /2 width=1 by or3_intro1, or3_intro2/ -qed-. - -lemma ylt_yle_trans: ∀x:ynat. ∀y:ynat. ∀z:ynat. y ≤ z → x < y → x < z. -#x #y #z * -y -z -[ #y #z #Hyz #H elim (ylt_inv_inj2 … H) -H - #m #Hm #H destruct /3 width=3 by ylt_inj, lt_to_le_to_lt/ -| #y * // -] -qed-. - -lemma yle_ylt_trans: ∀x:ynat. ∀y:ynat. ∀z:ynat. y < z → x ≤ y → x < z. -#x #y #z * -y -z -[ #y #z #Hyz #H elim (yle_inv_inj2 … H) -H - #m #Hm #H destruct /3 width=3 by ylt_inj, le_to_lt_to_lt/ -| #y #H elim (yle_inv_inj2 … H) -H // -] -qed-. - -lemma le_ylt_trans (x) (y) (z): x ≤ y → yinj y < z → yinj x < z. -/3 width=3 by yle_ylt_trans, yle_inj/ -qed-. - -lemma yle_inv_succ1_lt: ∀x,y:ynat. ↑x ≤ y → 0 < y ∧ x ≤ ↓y. -#x #y #H elim (yle_inv_succ1 … H) -H /3 width=1 by ylt_O1, conj/ -qed-. - -lemma yle_lt: ∀x,y. x < ∞ → ↑x ≤ y → x < y. -#x * // #y #H elim (ylt_inv_Y2 … H) -H #n #H destruct -/3 width=1 by ylt_inj, yle_inv_inj/ -qed-. - -(* Main properties **********************************************************) - -theorem ylt_trans: Transitive … ylt. -#x #y * -x -y -[ #x #y #Hxy * // - #z #H lapply (ylt_inv_inj … H) -H - /3 width=3 by transitive_lt, ylt_inj/ (**) (* full auto too slow *) -| #x #z #H elim (ylt_yle_false … H) // -] -qed-. - -lemma lt_ylt_trans (x) (y) (z): x < y → yinj y < z → yinj x < z. -/3 width=3 by ylt_trans, ylt_inj/ -qed-. - -(* Elimination principles ***************************************************) - -fact ynat_ind_lt_le_aux: ∀R:predicate ynat. - (∀y. (∀x. x < y → R x) → R y) → - ∀y:nat. ∀x. x ≤ y → R x. -#R #IH #y elim y -y -[ #x #H >(yle_inv_O2 … H) -x - @IH -IH #x #H elim (ylt_yle_false … H) -H // -| /5 width=3 by ylt_yle_trans, ylt_fwd_succ2/ -] -qed-. - -fact ynat_ind_lt_aux: ∀R:predicate ynat. - (∀y. (∀x. x < y → R x) → R y) → - ∀y:nat. R y. -/4 width=2 by ynat_ind_lt_le_aux/ qed-. - -lemma ynat_ind_lt: ∀R:predicate ynat. - (∀y. (∀x. x < y → R x) → R y) → - ∀y. R y. -#R #IH * /4 width=1 by ynat_ind_lt_aux/ -@IH #x #H elim (ylt_inv_Y2 … H) -H -#n #H destruct /4 width=1 by ynat_ind_lt_aux/ -qed-. - -fact ynat_f_ind_aux: ∀A. ∀f:A→ynat. ∀R:predicate A. - (∀x. (∀a. f a < x → R a) → ∀a. f a = x → R a) → - ∀x,a. f a = x → R a. -#A #f #R #IH #x @(ynat_ind_lt … x) -x -/3 width=3 by/ -qed-. - -lemma ynat_f_ind: ∀A. ∀f:A→ynat. ∀R:predicate A. - (∀x. (∀a. f a < x → R a) → ∀a. f a = x → R a) → ∀a. R a. -#A #f #R #IH #a -@(ynat_f_ind_aux … IH) -IH [2: // | skip ] -qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/ynat/ynat_minus_sn.ma b/matita/matita/contribs/lambdadelta/ground/ynat/ynat_minus_sn.ma deleted file mode 100644 index 5a9ab855d..000000000 --- a/matita/matita/contribs/lambdadelta/ground/ynat/ynat_minus_sn.ma +++ /dev/null @@ -1,221 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/ynat/ynat_plus.ma". - -(* NATURAL NUMBERS WITH INFINITY ********************************************) - -(* left subtraction *) -definition yminus_sn (x) (y): ynat ≝ ypred^y x. - -interpretation "ynat left minus" 'minus x y = (yminus_sn x y). - -lemma yminus_O2: ∀m:ynat. m - 0 = m. -// qed. - -lemma yminus_S2: ∀m:ynat. ∀n:nat. m - S n = ↓(m - n). -// qed. - -(* Basic properties *********************************************************) - -lemma yminus_inj: ∀m,n. yinj m - n = yinj (m - n). -#m #n elim n -n // -#n #IH >yminus_S2 >IH -IH >eq_minus_S_pred // -qed. - -lemma yminus_Y_inj: ∀n. ∞ - n = ∞. -#n elim n -n // -qed. - -lemma yminus_O1: ∀x:nat. yinj 0 - x = 0. -// qed. - -lemma yminus_refl: ∀x:nat. yinj x - x = 0. -// qed. - -lemma yminus_minus_comm: ∀x:ynat. ∀y,z. x - y - z = x - z - y. -* // qed. - -(* Properties on predecessor ************************************************) - -lemma yminus_SO2: ∀m:ynat. m - 1 = ↓m. -// qed. - -lemma yminus_pred1: ∀x,y. ↓x - y = ↓(x-y). -#x * // #y elim y -y // -qed. - -lemma yminus_pred: ∀m:ynat. ∀n. 0 < m → 0 < n → ↓m - ↓n = m - n. -* // #m #n >yminus_inj >yminus_inj -/4 width=1 by ylt_inv_inj, minus_pred_pred, eq_f/ -qed-. - -(* Properties on successor **************************************************) - -lemma yminus_succ: ∀m:ynat. ∀n. ↑m - ↑n = m - n. -* // qed. - -lemma yminus_succ1_inj: ∀n:nat. ∀m:ynat. n ≤ m → ↑m - n = ↑(m - n). -#n * -[ #m #Hmn >yminus_inj >yminus_inj - /4 width=1 by yle_inv_inj, plus_minus, eq_f/ -| >yminus_Y_inj // -] -qed-. - -lemma yminus_succ2: ∀x:ynat. ∀y. x - ↑y = ↓(x-y). -* // -qed. - -(* Properties on order ******************************************************) - -lemma yle_minus_sn: ∀m:ynat. ∀n. m - n ≤ m. -* // #n /2 width=1 by yle_inj/ -qed. - -lemma yle_to_minus: ∀m:ynat. ∀n:nat. m ≤ n → m - n = 0. -* -[ #m #n #H >yminus_inj /4 width=1 by yle_inv_inj, eq_minus_O, eq_f/ -| #n #H lapply (yle_inv_Y1 … H) -H #H destruct -] -qed-. - -lemma yminus_to_le: ∀m:ynat. ∀n. m - n = 0 → m ≤ n. -* [2: #n >yminus_Y_inj #H destruct ] -#m #n >yminus_inj #H -lapply (yinj_inj … H) -H (**) (* destruct lemma needed *) -/2 width=1 by yle_inj/ -qed. - -lemma monotonic_yle_minus_dx: ∀x,y. x ≤ y → ∀z. x - z ≤ y - z. -#x #y * /3 width=1 by yle_inj, monotonic_le_minus_l2/ -qed. - -(* Properties on strict order ***********************************************) - -lemma ylt_to_minus: ∀y:ynat. ∀x. yinj x < y → 0 < y - x. -* // #y #x #H >yminus_inj -/4 width=1 by ylt_inj, ylt_inv_inj, lt_plus_to_minus_r/ -qed. - -lemma yminus_to_lt: ∀y:ynat. ∀x. 0 < y - x → x < y. -* // #y #x >yminus_inj #H -/4 width=1 by ylt_inv_inj, ylt_inj, lt_minus_to_plus_r/ -qed-. - -lemma monotonic_ylt_minus_dx: ∀x,y:ynat. x < y → ∀z:nat. z ≤ x → x - z < y - z. -#x #y * -x -y -/4 width=1 by ylt_inj, yle_inv_inj, monotonic_lt_minus_l/ -qed. - -(* Properties on minus ******************************************************) - -lemma yplus_minus: ∀m:ynat. ∀n:nat. m + n - n = m. -#m #n elim n -n // -#n #IHn >(yplus_succ2 m n) >(yminus_succ … n) // -qed. - -lemma yminus_plus2: ∀x:ynat. ∀y,z. x - (y + z) = x - y - z. -* // qed. - -(* Forward lemmas on minus **************************************************) - -lemma yle_plus1_to_minus_inj2: ∀x,z:ynat. ∀y:nat. x + y ≤ z → x ≤ z - y. -#x #z #y #H lapply (monotonic_yle_minus_dx … H y) -H // -qed-. - -lemma yle_plus1_to_minus_inj1: ∀x,z:ynat. ∀y:nat. y + x ≤ z → x ≤ z - y. -/2 width=1 by yle_plus1_to_minus_inj2/ qed-. - -lemma yle_plus2_to_minus_inj2: ∀x,y:ynat. ∀z:nat. x ≤ y + z → x - z ≤ y. -/2 width=1 by monotonic_yle_minus_dx/ qed-. - -lemma yle_plus2_to_minus_inj1: ∀x,y:ynat. ∀z:nat. x ≤ z + y → x - z ≤ y. -/2 width=1 by yle_plus2_to_minus_inj2/ qed-. - -lemma yminus_plus (x:ynat) (y:nat): y ≤ x → x = (x-y)+y. -* // #x #y #H >yminus_inj >yplus_inj -/4 width=1 by yle_inv_inj, plus_minus, eq_f/ -qed-. - -lemma yplus_minus_assoc_inj: ∀x:nat. ∀y,z:ynat. x ≤ y → z + (y - x) = z + y - x. -#x * -[ #y * // #z >yminus_inj >yplus_inj >yplus_inj - /4 width=1 by yle_inv_inj, plus_minus, eq_f/ -| >yminus_Y_inj // -] -qed-. - -alias symbol "plus" (instance 5) = "ynat plus". -alias symbol "minus" (instance 4) = "ynat left minus". -alias symbol "minus" (instance 3) = "natural minus". -alias symbol "minus" (instance 2) = "ynat left minus". -alias symbol "leq" (instance 6) = "natural 'less or equal to'". -lemma yplus_minus_assoc_comm_inj: ∀z:ynat. ∀x,y:nat. x ≤ y → z - (y - x) = z + x - y. -* // #z #x #y >yminus_inj >yplus_inj >yminus_inj -/4 width=1 by yle_inv_inj, minus_le_minus_minus_comm, eq_f/ -qed-. - -lemma yplus_minus_comm_inj: ∀y:nat. ∀x,z:ynat. y ≤ x → x + z - y = x - y + z. -#y * // #x * // -#z #Hxy >yplus_inj >yminus_inj yplus_inj #H destruct -qed-. - -lemma yplus_inv_minus: - ∀x1,y2:ynat.∀y1,x2:nat. - y1 ≤ x1 → x1 + x2 = y2 + y1 → ∧∧ x1 - y1 = y2 - x2 & x2 ≤ y2. -* -[ #x1 * [| #y1 #x2 #_ >yplus_inj >yplus_Y1 #H destruct ] - #y2 #y1 #x2 #H1 >yplus_inj >yplus_inj #H2 >yminus_inj >yminus_inj - lapply (yle_inv_inj … H1) -H1 #Hyx1 - lapply (yinj_inj … H2) -H2 #Hxy (**) (* destruct lemma needed *) - /5 width=4 by yle_inj, plus2_le_sn_sn, plus_to_minus_2, conj, eq_f2/ -| #y2 #y1 #x2 #_ >yplus_Y1 #H - elim (yplus_inv_Y1 … H) -H #H destruct /2 width=1 by conj/ -] -qed-. - -(* Inversion lemmas on minus ************************************************) - -lemma yle_inv_plus_inj2: ∀x,z:ynat. ∀y:nat. x + y ≤ z → x ≤ z - y ∧ y ≤ z. -/3 width=3 by yle_plus1_to_minus_inj2, yle_trans, conj/ qed-. - -lemma yle_inv_plus_inj1: ∀x,z:ynat. ∀y:nat. y + x ≤ z → x ≤ z - y ∧ y ≤ z. -/2 width=1 by yle_inv_plus_inj2/ qed-. - -lemma yle_inv_plus_inj_dx: ∀z,x:ynat. ∀y:nat. x + y ≤ z → - ∧∧ x ≤ z - y & y ≤ z. -* [| /2 width=1 by conj/ ] -#z * [| #y >yplus_Y1 #H >(yle_inv_Y1 … H) -z /2 width=1 by conj/ ] -#x #y >yplus_inj #H >yminus_inj -/5 width=2 by yle_inv_inj, yle_inj, le_plus_to_minus_r, le_plus_b, conj/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/ynat/ynat_plus.ma b/matita/matita/contribs/lambdadelta/ground/ynat/ynat_plus.ma deleted file mode 100644 index b33f9300a..000000000 --- a/matita/matita/contribs/lambdadelta/ground/ynat/ynat_plus.ma +++ /dev/null @@ -1,313 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/xoa/ex_3_2.ma". -include "ground/ynat/ynat_lt.ma". - -(* NATURAL NUMBERS WITH INFINITY ********************************************) - -(* addition *) -definition yplus: ynat → ynat → ynat ≝ λx,y. match y with -[ yinj n ⇒ ysucc^n x -| Y ⇒ Y -]. - -interpretation "ynat plus" 'plus x y = (yplus x y). - -lemma yplus_O2: ∀m:ynat. m + 0 = m. -// qed. - -lemma yplus_S2: ∀m:ynat. ∀n. m + S n = ↑(m + n). -// qed. - -lemma yplus_Y2: ∀m:ynat. m + (∞) = ∞. -// qed. - -(* Properties on successor **************************************************) - -lemma yplus_succ2: ∀m,n. m + ↑n = ↑(m + n). -#m * // -qed. - -lemma yplus_succ1: ∀m,n. ↑m + n = ↑(m + n). -#m * // #n elim n -n // -qed. - -lemma yplus_succ_swap: ∀m,n. m + ↑n = ↑m + n. -// qed. - -lemma yplus_SO2: ∀m:ynat. m + 1 = ↑m. -* // -qed. - -(* Basic properties *********************************************************) - -lemma yplus_inj: ∀n,m. yinj m + yinj n = yinj (m + n). -#n elim n -n // -#n #IHn #m >(yplus_succ2 ? n) >IHn -IHn -yplus_inj whd in ⊢ (??%%); yplus_Y1 // -] -qed. - -lemma yplus_O1: ∀n:ynat. 0 + n = n. -#n >yplus_comm // qed. - -lemma yplus_comm_23: ∀x,y,z. x + z + y = x + y + z. -#x #y #z >yplus_assoc // -qed. - -lemma yplus_comm_24: ∀x1,x2,x3,x4. x1 + x4 + x3 + x2 = x1 + x2 + x3 + x4. -#x1 #x2 #x3 #x4 ->yplus_assoc >yplus_assoc >yplus_assoc >yplus_assoc -/2 width=1 by eq_f2/ -qed. - -lemma yplus_assoc_23: ∀x1,x2,x3,x4. x1 + x2 + (x3 + x4) = x1 + (x2 + x3) + x4. -#x1 #x2 #x3 #x4 >yplus_assoc >yplus_assoc -/2 width=1 by eq_f2/ -qed. - -(* Inversion lemmas on successor *********************************************) - -lemma yplus_inv_succ_lt_dx: ∀x,y,z:ynat. 0 < y → x + y = ↑z → x + ↓y = z. -#x #y #z #H <(ylt_inv_O1 y) // >yplus_succ2 -/2 width=1 by ysucc_inv_inj/ -qed-. - -lemma yplus_inv_succ_lt_sn: ∀x,y,z:ynat. 0 < x → x + y = ↑z → ↓x + y = z. -#x #y #z #H <(ylt_inv_O1 x) // >yplus_succ1 -/2 width=1 by ysucc_inv_inj/ - -qed-. - -(* Inversion lemmas on order ************************************************) - -lemma yle_inv_plus_dx: ∀x,y. x ≤ y → ∃z. x + z = y. -#x #y #H elim H -x -y /2 width=2 by ex_intro/ -#m #n #H @(ex_intro … (yinj (n-m))) (**) (* explicit constructor *) -/3 width=1 by plus_minus, eq_f/ -qed-. - -lemma yle_inv_plus_sn: ∀x,y. x ≤ y → ∃z. z + x = y. -#x #y #H elim (yle_inv_plus_dx … H) -H -/2 width=2 by ex_intro/ -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-. - -lemma yplus_inv_O: ∀x,y:ynat. x + y = 0 → x = 0 ∧ y = 0. -#x #y #H elim (yplus_inv_inj … H) -H -#m * /2 width=1 by conj/ #n yplus_Y2 #H destruct ] -#y yplus_succ1 #H -lapply (ysucc_inv_inj … H) -H #H -elim (IHx … H) -IHx -H /2 width=1 by or_introl, or_intror/ -qed-. - -lemma discr_yplus_x_xy: ∀x,y. x = x + y → x = ∞ ∨ y = 0. -/2 width=1 by discr_yplus_xy_x/ qed-. - -lemma yplus_inv_monotonic_dx_inj: ∀z,x,y. x + yinj z = y + yinj z → x = y. -#z @(nat_ind_plus … z) -z /3 width=2 by ysucc_inv_inj/ -qed-. - -lemma yplus_inv_monotonic_dx: ∀z,x,y. z < ∞ → x + z = y + z → x = y. -#z #x #y #H elim (ylt_inv_Y2 … H) -H /2 width=2 by yplus_inv_monotonic_dx_inj/ -qed-. - -lemma yplus_inv_Y2: ∀x,y. x + y = ∞ → x = ∞ ∨ y = ∞. -* /2 width=1 by or_introl/ #x * // #y >yplus_inj #H destruct -qed-. - -lemma yplus_inv_monotonic_23: ∀z,x1,x2,y1,y2. z < ∞ → - x1 + z + y1 = x2 + z + y2 → x1 + y1 = x2 + y2. -#z #x1 #x2 #y1 #y2 #Hz #H @(yplus_inv_monotonic_dx z) // ->yplus_comm_23 >H -H // -qed-. - -(* Inversion lemmas on strict_order *****************************************) - -lemma ylt_inv_plus_Y: ∀x,y. x + y < ∞ → x < ∞ ∧ y < ∞. -#x #y #H elim (ylt_inv_Y2 … H) -H -#z #H elim (yplus_inv_inj … H) -H /2 width=1 by conj/ -qed-. - -lemma ylt_inv_plus_sn: ∀x,y. x < y → ∃∃z. ↑z + x = y & x < ∞. -#x #y #H elim (ylt_inv_le … H) -H -#Hx #H elim (yle_inv_plus_sn … H) -H -/2 width=2 by ex2_intro/ -qed-. - -lemma ylt_inv_plus_dx: ∀x,y. x < y → ∃∃z. x + ↑z = y & x < ∞. -#x #y #H elim (ylt_inv_plus_sn … H) -H -#z >yplus_comm /2 width=2 by ex2_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. - -lemma yle_plus_dx1_trans: ∀x,z. z ≤ x → ∀y. z ≤ x + y. -/2 width=3 by yle_trans/ qed. - -lemma yle_plus_dx2_trans: ∀y,z. z ≤ y → ∀x. z ≤ x + y. -/2 width=3 by yle_trans/ qed. - -lemma monotonic_yle_plus_dx: ∀x,y. x ≤ y → ∀z. x + z ≤ y + z. -#x #y #Hxy * // -#z elim z -z /3 width=1 by yle_succ/ -qed. - -lemma monotonic_yle_plus_sn: ∀x,y. x ≤ y → ∀z. z + x ≤ z + y. -/2 width=1 by monotonic_yle_plus_dx/ qed. - -lemma monotonic_yle_plus: ∀x1,y1. x1 ≤ y1 → ∀x2,y2. x2 ≤ y2 → - x1 + x2 ≤ y1 + y2. -/3 width=3 by monotonic_yle_plus_dx, monotonic_yle_plus_sn, yle_trans/ qed. - -lemma ylt_plus_Y: ∀x,y. x < ∞ → y < ∞ → x + y < ∞. -#x #y #Hx elim (ylt_inv_Y2 … Hx) -Hx -#m #Hm #Hy elim (ylt_inv_Y2 … Hy) -Hy // -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-. - -lemma yle_inv_monotonic_plus_dx_inj: ∀x,y:ynat.∀z:nat. x + z ≤ y + z → x ≤ y. -#x #y #z elim z -z /3 width=1 by yle_inv_succ/ -qed-. - -lemma yle_inv_monotonic_plus_sn_inj: ∀x,y:ynat.∀z:nat. z + x ≤ z + y → x ≤ y. -/2 width=2 by yle_inv_monotonic_plus_dx_inj/ qed-. - -lemma yle_inv_monotonic_plus_dx: ∀x,y,z. z < ∞ → x + z ≤ y + z → x ≤ y. -#x #y #z #Hz elim (ylt_inv_Y2 … Hz) -Hz #m #H destruct -/2 width=2 by yle_inv_monotonic_plus_sn_inj/ -qed-. - -lemma yle_inv_monotonic_plus_sn: ∀x,y,z. z < ∞ → z + x ≤ z + y → x ≤ y. -/2 width=3 by yle_inv_monotonic_plus_dx/ qed-. - -lemma yle_fwd_plus_ge: ∀m1,m2:nat. m2 ≤ m1 → ∀n1,n2:ynat. m1 + n1 ≤ m2 + n2 → n1 ≤ n2. -#m1 #m2 #Hm12 #n1 #n2 #H -lapply (monotonic_yle_plus … Hm12 … H) -Hm12 -H -/2 width=2 by yle_inv_monotonic_plus_sn_inj/ -qed-. - -lemma yle_fwd_plus_ge_inj: ∀m1:nat. ∀m2,n1,n2:ynat. m2 ≤ m1 → m1 + n1 ≤ m2 + n2 → n1 ≤ n2. -#m2 #m1 #n1 #n2 #H elim (yle_inv_inj2 … H) -H -#x #H0 #H destruct /3 width=4 by yle_fwd_plus_ge, yle_inj/ -qed-. - -lemma yle_fwd_plus_yge: ∀n2,m1:ynat. ∀n1,m2:nat. m2 ≤ m1 → m1 + n1 ≤ m2 + n2 → n1 ≤ n2. -* // #n2 * /2 width=4 by yle_fwd_plus_ge_inj/ -qed-. - -(* Properties on strict order ***********************************************) - -lemma ylt_plus_dx1_trans: ∀x,z. z < x → ∀y. z < x + y. -/2 width=3 by ylt_yle_trans/ qed. - -lemma ylt_plus_dx2_trans: ∀y,z. z < y → ∀x. z < x + y. -/2 width=3 by ylt_yle_trans/ qed. - -lemma monotonic_ylt_plus_dx_inj: ∀x,y. x < y → ∀z:nat. x + yinj z < y + yinj z. -#x #y #Hxy #z elim z -z /3 width=1 by ylt_succ/ -qed. - -lemma monotonic_ylt_plus_sn_inj: ∀x,y. x < y → ∀z:nat. yinj z + x < yinj z + y. -/2 width=1 by monotonic_ylt_plus_dx_inj/ qed. - -lemma monotonic_ylt_plus_dx: ∀x,y. x < y → ∀z. z < ∞ → x + z < y + z. -#x #y #Hxy #z #Hz elim (ylt_inv_Y2 … Hz) -Hz -#m #H destruct /2 width=1 by monotonic_ylt_plus_dx_inj/ -qed. - -lemma monotonic_ylt_plus_sn: ∀x,y. x < y → ∀z. z < ∞ → z + x < z + y. -/2 width=1 by monotonic_ylt_plus_dx/ qed. - -lemma monotonic_ylt_plus_inj: ∀m1,m2. m1 < m2 → ∀n1,n2. yinj n1 ≤ n2 → m1 + n1 < m2 + n2. -/3 width=3 by monotonic_ylt_plus_sn_inj, monotonic_yle_plus_sn, ylt_yle_trans/ -qed. - -lemma monotonic_ylt_plus: ∀m1,m2. m1 < m2 → ∀n1. n1 < ∞ → ∀n2. n1 ≤ n2 → m1 + n1 < m2 + n2. -#m1 #m2 #Hm12 #n1 #H elim (ylt_inv_Y2 … H) -H #m #H destruct /2 width=1 by monotonic_ylt_plus_inj/ -qed. - -(* Forward lemmas on strict order *******************************************) - -lemma ylt_inv_monotonic_plus_dx: ∀x,y,z. x + z < y + z → x < y. -* [2: #y #z >yplus_comm #H elim (ylt_inv_Y1 … H) ] -#x * // #y * [2: #H elim (ylt_inv_Y1 … H) ] -/4 width=3 by ylt_inv_inj, ylt_inj, lt_plus_to_lt_l/ -qed-. - -lemma ylt_fwd_plus_ge: ∀m1,m2. m2 ≤ m1 → ∀n1,n2. m1 + n1 < m2 + n2 → n1 < n2. -#m1 #m2 #Hm12 #n1 #n2 #H elim (ylt_fwd_gen … H) -#x #H0 elim (yplus_inv_inj … H0) -H0 -#y #z #_ #H2 #H3 destruct -x -elim (yle_inv_inj2 … Hm12) -#x #_ #H0 destruct -lapply (monotonic_ylt_plus … H … Hm12) -H -Hm12 -/2 width=2 by ylt_inv_monotonic_plus_dx/ -qed-. - -(* Properties on predeccessor ***********************************************) - -lemma yplus_pred1: ∀x,y:ynat. 0 < x → ↓x + y = ↓(x+y). -#x * // #y elim y -y // #y #IH #Hx ->yplus_S2 >yplus_S2 >IH -IH // >ylt_inv_O1 -/2 width=1 by ylt_plus_dx1_trans/ -qed-. - -lemma yplus_pred2: ∀x,y:ynat. 0 < y → x + ↓y = ↓(x+y). -/2 width=1 by yplus_pred1/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/ynat/ynat_succ.ma b/matita/matita/contribs/lambdadelta/ground/ynat/ynat_succ.ma deleted file mode 100644 index f7c8dc521..000000000 --- a/matita/matita/contribs/lambdadelta/ground/ynat/ynat_succ.ma +++ /dev/null @@ -1,97 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/ynat/ynat_pred.ma". - -(* NATURAL NUMBERS WITH INFINITY ********************************************) - -(* the successor function *) -definition ysucc: ynat → ynat ≝ λm. match m with -[ yinj m ⇒ ↑m -| Y ⇒ Y -]. - -interpretation "ynat successor" 'UpArrow m = (ysucc m). - -lemma ysucc_inj: ∀m:nat. ↑(yinj m) = yinj (↑m). -// qed. - -lemma ysucc_Y: ↑(∞) = ∞. -// qed. - -(* Properties ***************************************************************) - -lemma ypred_succ: ∀m. ↓↑m = m. -* // qed. - -lemma ynat_cases: ∀n:ynat. n = 0 ∨ ∃m:ynat. n = ↑m. -* -[ * /2 width=1 by or_introl/ - #n @or_intror @(ex_intro … n) // (**) (* explicit constructor *) -| @or_intror @(ex_intro … (∞)) // (**) (* explicit constructor *) -] -qed-. - -lemma ysucc_iter_Y: ∀m. ysucc^m (∞) = ∞. -#m elim m -m // -#m #IHm whd in ⊢ (??%?); >IHm // -qed. - -(* Inversion lemmas *********************************************************) - -lemma ysucc_inv_inj: ∀m,n. ↑m = ↑n → m = n. -#m #n #H <(ypred_succ m) <(ypred_succ n) // -qed-. - -lemma ysucc_inv_refl: ∀m. ↑m = m → m = ∞. -* // -#m #H lapply (yinj_inj … H) -H (**) (* destruct lemma needed *) -#H elim (lt_refl_false m) // -qed-. - -lemma ysucc_inv_inj_sn: ∀m2,n1. yinj m2 = ↑n1 → - ∃∃m1. n1 = yinj m1 & m2 = S m1. -#m2 * normalize -[ #n1 #H destruct /2 width=3 by ex2_intro/ -| #H destruct -] -qed-. - -lemma ysucc_inv_inj_dx: ∀m2,n1. ↑n1 = yinj m2 → - ∃∃m1. n1 = yinj m1 & m2 = S m1. -/2 width=1 by ysucc_inv_inj_sn/ qed-. - -lemma ysucc_inv_Y_sn: ∀m. ∞ = ↑m → m = ∞. -* // normalize -#m #H destruct -qed-. - -lemma ysucc_inv_Y_dx: ∀m. ↑m = ∞ → m = ∞. -/2 width=1 by ysucc_inv_Y_sn/ qed-. - -lemma ysucc_inv_O_sn: ∀m. yinj 0 = ↑m → ⊥. (**) (* explicit coercion *) -#m #H elim (ysucc_inv_inj_sn … H) -H -#n #_ #H destruct -qed-. - -lemma ysucc_inv_O_dx: ∀m:ynat. ↑m = 0 → ⊥. -/2 width=2 by ysucc_inv_O_sn/ qed-. - -(* Eliminators **************************************************************) - -lemma ynat_ind: ∀R:predicate ynat. - R 0 → (∀n:nat. R n → R (↑n)) → R (∞) → - ∀x. R x. -#R #H1 #H2 #H3 * // #n elim n -n /2 width=1 by/ -qed-. -- 2.39.2