From 2601d0c1a860fdd08c4c1d71473917aa85eeb63a Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 14 Jul 2015 17:38:33 +0000 Subject: [PATCH] - subtraction (and related notions) removed - more lemmas --- .../ground_2/etc/lib/relations.etc | 21 ++ .../ynat_max.ma => etc/ynat/ynat_max.etc} | 0 .../ynat_min.ma => etc/ynat/ynat_min.etc} | 0 .../ynat_minus.ma => etc/ynat/ynat_minus.etc} | 98 ++++++++ .../ground_2/etc/ynat/ynat_plus.etc | 4 + .../lambdadelta/ground_2/web/ground_2_src.tbl | 3 +- .../lambdadelta/ground_2/ynat/ynat.ma | 10 +- .../lambdadelta/ground_2/ynat/ynat_le.ma | 5 + .../lambdadelta/ground_2/ynat/ynat_lt.ma | 65 ++++- .../lambdadelta/ground_2/ynat/ynat_plus.ma | 236 +++++++++++------- .../lambdadelta/ground_2/ynat/ynat_succ.ma | 8 + 11 files changed, 351 insertions(+), 99 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/ground_2/etc/lib/relations.etc rename matita/matita/contribs/lambdadelta/ground_2/{ynat/ynat_max.ma => etc/ynat/ynat_max.etc} (100%) rename matita/matita/contribs/lambdadelta/ground_2/{ynat/ynat_min.ma => etc/ynat/ynat_min.etc} (100%) rename matita/matita/contribs/lambdadelta/ground_2/{ynat/ynat_minus.ma => etc/ynat/ynat_minus.etc} (52%) create mode 100644 matita/matita/contribs/lambdadelta/ground_2/etc/ynat/ynat_plus.etc diff --git a/matita/matita/contribs/lambdadelta/ground_2/etc/lib/relations.etc b/matita/matita/contribs/lambdadelta/ground_2/etc/lib/relations.etc new file mode 100644 index 000000000..6166cf7ee --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/etc/lib/relations.etc @@ -0,0 +1,21 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relations.ma". + +(* ADDITIONAL PROPERTIES OF RELATIONS ***************************************) + +lemma replace2: ∀A,B:Type[0]. ∀R:relation2 A B. ∀x1,y1,x2,y2. + R x1 x2 → y1 = x1 → y2 = x2 → R y1 y2. +// qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_max.ma b/matita/matita/contribs/lambdadelta/ground_2/etc/ynat/ynat_max.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_max.ma rename to matita/matita/contribs/lambdadelta/ground_2/etc/ynat/ynat_max.etc diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_min.ma b/matita/matita/contribs/lambdadelta/ground_2/etc/ynat/ynat_min.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_min.ma rename to matita/matita/contribs/lambdadelta/ground_2/etc/ynat/ynat_min.etc diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_minus.ma b/matita/matita/contribs/lambdadelta/ground_2/etc/ynat/ynat_minus.etc similarity index 52% rename from matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_minus.ma rename to matita/matita/contribs/lambdadelta/ground_2/etc/ynat/ynat_minus.etc index 0c80f8370..a2f15a8e2 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_minus.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/etc/ynat/ynat_minus.etc @@ -127,3 +127,101 @@ lemma monotonic_ylt_minus_dx: ∀x,y:ynat. x < y → ∀z:nat. z ≤ x → x - 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_inj: ∀m:ynat. ∀n:nat. m + n - n = m. +#m #n elim n -n // +#n #IHn >(yplus_succ2 m n) >(yminus_succ … n) // +qed. + +lemma yplus_minus: ∀m,n. m + n - n ≤ m. +#m * // +qed. + +lemma yminus_plus2: ∀z,y,x:ynat. x - (y + z) = x - y - z. +* // #z * [2: >yplus_Y1 >yminus_O1 // ] #y * +[ #x >yplus_inj >yminus_inj >yminus_inj >yminus_inj /2 width=1 by eq_f/ +| >yplus_inj >yminus_Y_inj // +] +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 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-. + +lemma yplus_minus_assoc_comm_inj: ∀x:nat. ∀y,z:ynat. x ≤ y → z - (y - x) = z + x - y. +#x * +[ #y * + [ #z >yminus_inj >yminus_inj >yplus_inj >yminus_inj + /4 width=1 by yle_inv_inj, minus_le_minus_minus_comm, eq_f/ + | >yminus_inj >yminus_Y_inj // + ] +| >yminus_Y_inj // +] +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 in H0; >yplus_inj >yminus_inj >yminus_inj #H0 +@conj // lapply (yinj_inj … H0) -H0 /3 width=1 by arith_b1, eq_f/ +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: ∀x,y:ynat. ∀z:nat. x + y ≤ z → + ∃∃m,n. x = yinj m & y = yinj n & x ≤ z - y & y ≤ z. +#x #y #z #Hz elim (yle_inv_inj2 … Hz) +#z0 #_ #H elim (yplus_inv_inj … H) -H +#m #n #H1 #H2 #H3 destruct +elim (yle_inv_plus_inj2 … Hz) -Hz /2 width=2 by ex4_2_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/etc/ynat/ynat_plus.etc b/matita/matita/contribs/lambdadelta/ground_2/etc/ynat/ynat_plus.etc new file mode 100644 index 000000000..e535b9fe0 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/etc/ynat/ynat_plus.etc @@ -0,0 +1,4 @@ + +lemma pippo: ∀x,y. x + y ≤ x → x = ∞ ∨ y = 0. +/3 width=1 by discr_yplus_xy_x, yle_antisym/ qed-. + diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl index 467d427ff..0ba823065 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl @@ -14,8 +14,7 @@ table { [ { "" * } { [ "ynat ( ∞ )" "ynat_pred ( ⫰? )" "ynat_succ ( ⫯? )" "ynat_le ( ? ≤ ? )" "ynat_lt ( ? < ? )" - "ynat_minus ( ? - ? )" "ynat_plus ( ? + ? )" - "ynat_max" "ynat_min" * + "ynat_plus ( ? + ? )" * ] } ] diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat.ma index 3dbc0c662..7e2c2dc6c 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "arithmetics/nat.ma". +include "ground_2/lib/arith.ma". include "ground_2/notation/constructors/infinity_0.ma". (* NATURAL NUMBERS WITH INFINITY ********************************************) @@ -32,3 +32,11 @@ interpretation "ynat infinity" 'Infinity = Y. lemma yinj_inj: ∀m,n. yinj m = yinj n → m = n. #m #n #H destruct // qed-. + +(* Basic properties *********************************************************) + +lemma eq_ynat_dec: ∀n1,n2:ynat. Decidable (n1 = n2). +* [ #n1 ] * [1,3: #n2 ] /2 width=1 by or_introl/ +[2,3: @or_intror #H destruct ] +elim (eq_nat_dec n1 n2) /4 width=1 by yinj_inj, or_intror, or_introl/ +qed-. 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 b7b57d764..613a9793c 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_le.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_le.ma @@ -60,6 +60,11 @@ 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. 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 3e496e185..2a9fbb515 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma @@ -59,6 +59,11 @@ lemma ylt_inv_Y1: ∀n. ∞ < n → ⊥. #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. 0 < n → ⫯⫰n = n. * // #n #H lapply (ylt_inv_inj … H) -H normalize /3 width=1 by S_pred, eq_f/ @@ -96,7 +101,7 @@ 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 yle **************************************) +(* 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/ @@ -119,10 +124,14 @@ lemma ylt_yle_false: ∀m:ynat. ∀n:ynat. m < n → n ≤ m → ⊥. ] 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_O: ∀x. ⫯⫰(yinj x) = yinj x → 0 < x. -* /2 width=1 by/ normalize +lemma ylt_O1: ∀x. ⫯⫰x = x → 0 < x. +* // * /2 width=1 by ylt_inj/ normalize #H destruct qed. @@ -143,6 +152,9 @@ 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. ⫯yinj x ≤ y → x < y. #x * /3 width=1 by yle_inv_inj, ylt_inj/ qed. @@ -183,6 +195,15 @@ lemma yle_ylt_trans: ∀x:ynat. ∀y:ynat. ∀z:ynat. y < z → x ≤ y → x < ] qed-. +lemma yle_inv_succ1_lt: ∀x,y. ⫯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. @@ -193,3 +214,41 @@ theorem ylt_trans: Transitive … ylt. | #x #z #H elim (ylt_yle_false … H) // ] 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_2/ynat/ynat_plus.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma index f7a15c310..e710032b0 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "ground_2/ynat/ynat_minus.ma". +include "ground_2/ynat/ynat_lt.ma". (* NATURAL NUMBERS WITH INFINITY ********************************************) @@ -80,6 +80,43 @@ 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. 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. 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 → @@ -89,6 +126,59 @@ lemma yplus_inv_inj: ∀z,y,x. x + y = yinj z → /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. @@ -118,6 +208,11 @@ 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. @@ -126,17 +221,25 @@ lemma yle_fwd_plus_sn2: ∀x,y,z. x + y ≤ z → y ≤ z. 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: ∀x,y:ynat.∀z:nat. x + z ≤ y + z → x ≤ y. +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: ∀x,y:ynat.∀z:nat. z + x ≤ z + y → x ≤ y. -/2 width=2 by yle_inv_monotonic_plus_dx/ 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/ +/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. @@ -148,115 +251,62 @@ lemma yle_fwd_plus_yge: ∀n2,m1:ynat. ∀n1,m2:nat. m2 ≤ m1 → m1 + n1 ≤ m * // #n2 * /2 width=4 by yle_fwd_plus_ge_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-. - (* Properties on strict order ***********************************************) -lemma ylt_plus_dx1_trans: ∀x,z. z < x → ∀y. z < x + yinj y. +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 < yinj x + y. +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: ∀x,y. x < y → ∀z:nat. x + yinj z < y + yinj z. +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: ∀x,y. x < y → ∀z:nat. yinj z + x < yinj z + y. -/2 width=1 by monotonic_ylt_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-. +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. -(* Properties on minus ******************************************************) +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 yplus_minus_inj: ∀m:ynat. ∀n:nat. m + n - n = m. -#m #n elim n -n // -#n #IHn >(yplus_succ2 m n) >(yminus_succ … n) // -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 yplus_minus: ∀m,n. m + n - n ≤ m. -#m * // +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 yminus_plus2: ∀z,y,x:ynat. x - (y + z) = x - y - z. -* // #z * [2: >yplus_Y1 >yminus_O1 // ] #y * -[ #x >yplus_inj >yminus_inj >yminus_inj >yminus_inj /2 width=1 by eq_f/ -| >yplus_inj >yminus_Y_inj // -] +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 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-. +(* Forward lemmas on strict order *******************************************) -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 // -] +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 yplus_minus_assoc_comm_inj: ∀x:nat. ∀y,z:ynat. x ≤ y → z - (y - x) = z + x - y. -#x * -[ #y * - [ #z >yminus_inj >yminus_inj >yplus_inj >yminus_inj - /4 width=1 by yle_inv_inj, minus_le_minus_minus_comm, eq_f/ - | >yminus_inj >yminus_Y_inj // - ] -| >yminus_Y_inj // -] +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-. -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_S2 >yplus_S2 >IH -IH // >ylt_inv_O1 +/2 width=1 by ylt_plus_dx1_trans/ qed-. -lemma ylt_plus1_to_minus_inj1: ∀x,z:ynat. ∀y:nat. y + x < z → x < z - y. -/2 width=1 by ylt_plus1_to_minus_inj2/ qed-. - -lemma ylt_plus2_to_minus_inj2: ∀x,y:ynat. ∀z:nat. z ≤ x → x < y + z → x - z < y. -/2 width=1 by monotonic_ylt_minus_dx/ qed-. - -lemma ylt_plus2_to_minus_inj1: ∀x,y:ynat. ∀z:nat. z ≤ x → x < z + y → x - z < y. -/2 width=1 by ylt_plus2_to_minus_inj2/ 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 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_2/ynat/ynat_succ.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma index c95c72d15..c4c989f77 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma @@ -88,3 +88,11 @@ qed-. lemma ysucc_inv_O_dx: ∀m. ⫯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