From: Ferruccio Guidi Date: Tue, 14 Jul 2015 17:38:33 +0000 (+0000) Subject: - subtraction (and related notions) removed X-Git-Tag: make_still_working~705 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=2601d0c1a860fdd08c4c1d71473917aa85eeb63a - subtraction (and related notions) removed - more lemmas --- 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/etc/ynat/ynat_max.etc b/matita/matita/contribs/lambdadelta/ground_2/etc/ynat/ynat_max.etc new file mode 100644 index 000000000..acbd31d9d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/etc/ynat/ynat_max.etc @@ -0,0 +1,58 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground_2/ynat/ynat_plus.ma". + +(* NATURAL NUMBERS WITH INFINITY ********************************************) + +lemma ymax_pre_dx: ∀x,y. x ≤ y → x - y + y = y. +#x #y * -x -y // +#x #y #Hxy >yminus_inj >(eq_minus_O … Hxy) -Hxy // +qed-. + +lemma ymax_pre_sn: ∀x,y. y ≤ x → x - y + y = x. +#x #y * -x -y +[ #x #y #Hxy >yminus_inj /3 width=3 by plus_minus, eq_f/ +| * // +] +qed-. + +lemma ymax_pre_i_dx: ∀y,x. y ≤ x - y + y. +// qed. + +lemma ymax_pre_i_sn: ∀y,x. x ≤ x - y + y. +* // #y * /2 width=1 by yle_inj/ +qed. + +lemma ymax_pre_e: ∀x,z. x ≤ z → ∀y. y ≤ z → x - y + y ≤ z. +#x #z #Hxz #y #Hyz elim (yle_split x y) +[ #Hxy >(ymax_pre_dx … Hxy) -x // +| #Hyx >(ymax_pre_sn … Hyx) -y // +] +qed. + +lemma ymax_pre_dx_comm: ∀x,y. x ≤ y → y + (x - y) = y. +/2 width=1 by ymax_pre_dx/ qed-. + +lemma ymax_pre_sn_comm: ∀x,y. y ≤ x → y + (x - y) = x. +/2 width=1 by ymax_pre_sn/ qed-. + +lemma ymax_pre_i_dx_comm: ∀y,x. y ≤ y + (x - y). +// qed. + +lemma ymax_pre_i_sn_comm: ∀y,x. x ≤ y + (x - y). +/2 width=1 by ymax_pre_i_sn/ qed. + +lemma ymax_pre_e_comm: ∀x,z. x ≤ z → ∀y. y ≤ z → y + (x - y) ≤ z. +/2 width=1 by ymax_pre_e/ qed. diff --git a/matita/matita/contribs/lambdadelta/ground_2/etc/ynat/ynat_min.etc b/matita/matita/contribs/lambdadelta/ground_2/etc/ynat/ynat_min.etc new file mode 100644 index 000000000..96b8f2a21 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/etc/ynat/ynat_min.etc @@ -0,0 +1,52 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground_2/ynat/ynat_plus.ma". + +(* NATURAL NUMBERS WITH INFINITY ********************************************) + +fact ymin_pre_dx_aux: ∀x,y. y ≤ x → x - (x - y) ≤ y. +#x #y * -x -y +[ #x #y #Hxy >yminus_inj + /3 width=4 by yle_inj, monotonic_le_minus_l/ +| * // +] +qed-. + +lemma ymin_pre_sn: ∀x,y. x ≤ y → x - (x - y) = x. +#x #y * -x -y // +#x #y #Hxy >yminus_inj >(eq_minus_O … Hxy) -Hxy // +qed-. + +lemma ymin_pre_i_dx: ∀x,y. x - (x - y) ≤ y. +#x #y elim (yle_split x y) /2 width=1 by ymin_pre_dx_aux/ +#Hxy >(ymin_pre_sn … Hxy) // +qed. + +lemma ymin_pre_i_sn: ∀x,y. x - (x - y) ≤ x. +// qed. + +lemma ymin_pre_dx: ∀x,y. y ≤ yinj x → yinj x - (yinj x - y) = y. +#x #y #H elim (yle_inv_inj2 … H) -H +#z #Hzx #H destruct >yminus_inj +/3 width=4 by minus_le_minus_minus_comm, eq_f/ +qed-. + +lemma ymin_pre_e: ∀z,x. z ≤ yinj x → ∀y. z ≤ y → + z ≤ yinj x - (yinj x - y). +#z #x #Hzx #y #Hzy elim (yle_split x y) +[ #H >(ymin_pre_sn … H) -y // +| #H >(ymin_pre_dx … H) -x // +] +qed. diff --git a/matita/matita/contribs/lambdadelta/ground_2/etc/ynat/ynat_minus.etc b/matita/matita/contribs/lambdadelta/ground_2/etc/ynat/ynat_minus.etc new file mode 100644 index 000000000..a2f15a8e2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/etc/ynat/ynat_minus.etc @@ -0,0 +1,227 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground_2/ynat/ynat_lt.ma". + +(* NATURAL NUMBERS WITH INFINITY ********************************************) + +(* subtraction *) +definition yminus: ynat → ynat → ynat ≝ λx,y. match y with +[ yinj n ⇒ ypred^n x +| Y ⇒ yinj 0 +]. + +interpretation "ynat minus" 'minus x y = (yminus x y). + +lemma yminus_O2: ∀m:ynat. m - 0 = m. +// qed. + +lemma yminus_S2: ∀m:ynat. ∀n:nat. m - S n = ⫰(m - n). +// qed. + +lemma yminus_Y2: ∀m. m - (∞) = 0. +// qed. + +(* Basic properties *********************************************************) + +lemma yminus_inj: ∀m,n. yinj m - yinj 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. ∞ - yinj n = ∞. +#n elim n -n // +qed. + +lemma yminus_O1: ∀x:ynat. 0 - x = 0. +* // qed. + +lemma yminus_refl: ∀x:ynat. x - x = 0. +* // qed. + +lemma yminus_minus_comm: ∀y,z,x. x - y - z = x - z - y. +* #y [ * #z [ * // ] ] >yminus_O1 // +qed. + +(* Properties on predecessor ************************************************) + +lemma yminus_SO2: ∀m. m - 1 = ⫰m. +* // +qed. + +lemma yminus_pred1: ∀x,y. ⫰x - y = ⫰(x-y). +#x * // #y elim y -y // +qed. + +lemma yminus_pred: ∀n,m. 0 < m → 0 < n → ⫰m - ⫰n = m - n. +* // #n * +[ #m #Hm #Hn >yminus_inj >yminus_inj + /4 width=1 by ylt_inv_inj, minus_pred_pred, eq_f/ +| >yminus_Y_inj // +] +qed-. + +(* Properties on successor **************************************************) + +lemma yminus_succ: ∀n,m. ⫯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: ∀y,x. x - ⫯y = ⫰(x-y). +* // +qed. + +(* Properties on order ******************************************************) + +lemma yle_minus_sn: ∀n,m. m - n ≤ m. +* // #n * /2 width=1 by yle_inj/ +qed. + +lemma yle_to_minus: ∀m:ynat. ∀n:ynat. m ≤ n → m - n = 0. +#m #n * -m -n /3 width=3 by eq_minus_O, eq_f/ +qed-. + +lemma yminus_to_le: ∀n:ynat. ∀m:ynat. m - n = 0 → m ≤ n. +* // #n * +[ #m >yminus_inj #H lapply (yinj_inj … H) -H (**) (* destruct lemma needed *) + /2 width=1 by yle_inj/ +| >yminus_Y_inj #H destruct +] +qed. + +lemma monotonic_yle_minus_dx: ∀x,y. x ≤ y → ∀z. x - z ≤ y - z. +#x #y #Hxy * // +#z elim z -z /3 width=1 by yle_pred/ +qed. + +(* Properties on strict order ***********************************************) + +lemma ylt_to_minus: ∀x,y:ynat. x < y → 0 < y - x. +#x #y #H elim H -x -y /3 width=1 by ylt_inj, lt_plus_to_minus_r/ +qed. + +lemma yminus_to_lt: ∀x,y:ynat. 0 < y - x → x < y. +* [2: #y #H elim (ylt_yle_false … H) // ] +#m * /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_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_max.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_max.ma deleted file mode 100644 index acbd31d9d..000000000 --- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_max.ma +++ /dev/null @@ -1,58 +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_2/ynat/ynat_plus.ma". - -(* NATURAL NUMBERS WITH INFINITY ********************************************) - -lemma ymax_pre_dx: ∀x,y. x ≤ y → x - y + y = y. -#x #y * -x -y // -#x #y #Hxy >yminus_inj >(eq_minus_O … Hxy) -Hxy // -qed-. - -lemma ymax_pre_sn: ∀x,y. y ≤ x → x - y + y = x. -#x #y * -x -y -[ #x #y #Hxy >yminus_inj /3 width=3 by plus_minus, eq_f/ -| * // -] -qed-. - -lemma ymax_pre_i_dx: ∀y,x. y ≤ x - y + y. -// qed. - -lemma ymax_pre_i_sn: ∀y,x. x ≤ x - y + y. -* // #y * /2 width=1 by yle_inj/ -qed. - -lemma ymax_pre_e: ∀x,z. x ≤ z → ∀y. y ≤ z → x - y + y ≤ z. -#x #z #Hxz #y #Hyz elim (yle_split x y) -[ #Hxy >(ymax_pre_dx … Hxy) -x // -| #Hyx >(ymax_pre_sn … Hyx) -y // -] -qed. - -lemma ymax_pre_dx_comm: ∀x,y. x ≤ y → y + (x - y) = y. -/2 width=1 by ymax_pre_dx/ qed-. - -lemma ymax_pre_sn_comm: ∀x,y. y ≤ x → y + (x - y) = x. -/2 width=1 by ymax_pre_sn/ qed-. - -lemma ymax_pre_i_dx_comm: ∀y,x. y ≤ y + (x - y). -// qed. - -lemma ymax_pre_i_sn_comm: ∀y,x. x ≤ y + (x - y). -/2 width=1 by ymax_pre_i_sn/ qed. - -lemma ymax_pre_e_comm: ∀x,z. x ≤ z → ∀y. y ≤ z → y + (x - y) ≤ z. -/2 width=1 by ymax_pre_e/ qed. diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_min.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_min.ma deleted file mode 100644 index 96b8f2a21..000000000 --- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_min.ma +++ /dev/null @@ -1,52 +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_2/ynat/ynat_plus.ma". - -(* NATURAL NUMBERS WITH INFINITY ********************************************) - -fact ymin_pre_dx_aux: ∀x,y. y ≤ x → x - (x - y) ≤ y. -#x #y * -x -y -[ #x #y #Hxy >yminus_inj - /3 width=4 by yle_inj, monotonic_le_minus_l/ -| * // -] -qed-. - -lemma ymin_pre_sn: ∀x,y. x ≤ y → x - (x - y) = x. -#x #y * -x -y // -#x #y #Hxy >yminus_inj >(eq_minus_O … Hxy) -Hxy // -qed-. - -lemma ymin_pre_i_dx: ∀x,y. x - (x - y) ≤ y. -#x #y elim (yle_split x y) /2 width=1 by ymin_pre_dx_aux/ -#Hxy >(ymin_pre_sn … Hxy) // -qed. - -lemma ymin_pre_i_sn: ∀x,y. x - (x - y) ≤ x. -// qed. - -lemma ymin_pre_dx: ∀x,y. y ≤ yinj x → yinj x - (yinj x - y) = y. -#x #y #H elim (yle_inv_inj2 … H) -H -#z #Hzx #H destruct >yminus_inj -/3 width=4 by minus_le_minus_minus_comm, eq_f/ -qed-. - -lemma ymin_pre_e: ∀z,x. z ≤ yinj x → ∀y. z ≤ y → - z ≤ yinj x - (yinj x - y). -#z #x #Hzx #y #Hzy elim (yle_split x y) -[ #H >(ymin_pre_sn … H) -y // -| #H >(ymin_pre_dx … H) -x // -] -qed. diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_minus.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_minus.ma deleted file mode 100644 index 0c80f8370..000000000 --- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_minus.ma +++ /dev/null @@ -1,129 +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_2/ynat/ynat_lt.ma". - -(* NATURAL NUMBERS WITH INFINITY ********************************************) - -(* subtraction *) -definition yminus: ynat → ynat → ynat ≝ λx,y. match y with -[ yinj n ⇒ ypred^n x -| Y ⇒ yinj 0 -]. - -interpretation "ynat minus" 'minus x y = (yminus x y). - -lemma yminus_O2: ∀m:ynat. m - 0 = m. -// qed. - -lemma yminus_S2: ∀m:ynat. ∀n:nat. m - S n = ⫰(m - n). -// qed. - -lemma yminus_Y2: ∀m. m - (∞) = 0. -// qed. - -(* Basic properties *********************************************************) - -lemma yminus_inj: ∀m,n. yinj m - yinj 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. ∞ - yinj n = ∞. -#n elim n -n // -qed. - -lemma yminus_O1: ∀x:ynat. 0 - x = 0. -* // qed. - -lemma yminus_refl: ∀x:ynat. x - x = 0. -* // qed. - -lemma yminus_minus_comm: ∀y,z,x. x - y - z = x - z - y. -* #y [ * #z [ * // ] ] >yminus_O1 // -qed. - -(* Properties on predecessor ************************************************) - -lemma yminus_SO2: ∀m. m - 1 = ⫰m. -* // -qed. - -lemma yminus_pred1: ∀x,y. ⫰x - y = ⫰(x-y). -#x * // #y elim y -y // -qed. - -lemma yminus_pred: ∀n,m. 0 < m → 0 < n → ⫰m - ⫰n = m - n. -* // #n * -[ #m #Hm #Hn >yminus_inj >yminus_inj - /4 width=1 by ylt_inv_inj, minus_pred_pred, eq_f/ -| >yminus_Y_inj // -] -qed-. - -(* Properties on successor **************************************************) - -lemma yminus_succ: ∀n,m. ⫯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: ∀y,x. x - ⫯y = ⫰(x-y). -* // -qed. - -(* Properties on order ******************************************************) - -lemma yle_minus_sn: ∀n,m. m - n ≤ m. -* // #n * /2 width=1 by yle_inj/ -qed. - -lemma yle_to_minus: ∀m:ynat. ∀n:ynat. m ≤ n → m - n = 0. -#m #n * -m -n /3 width=3 by eq_minus_O, eq_f/ -qed-. - -lemma yminus_to_le: ∀n:ynat. ∀m:ynat. m - n = 0 → m ≤ n. -* // #n * -[ #m >yminus_inj #H lapply (yinj_inj … H) -H (**) (* destruct lemma needed *) - /2 width=1 by yle_inj/ -| >yminus_Y_inj #H destruct -] -qed. - -lemma monotonic_yle_minus_dx: ∀x,y. x ≤ y → ∀z. x - z ≤ y - z. -#x #y #Hxy * // -#z elim z -z /3 width=1 by yle_pred/ -qed. - -(* Properties on strict order ***********************************************) - -lemma ylt_to_minus: ∀x,y:ynat. x < y → 0 < y - x. -#x #y #H elim H -x -y /3 width=1 by ylt_inj, lt_plus_to_minus_r/ -qed. - -lemma yminus_to_lt: ∀x,y:ynat. 0 < y - x → x < y. -* [2: #y #H elim (ylt_yle_false … H) // ] -#m * /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. 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-.