From: Ferruccio Guidi Date: Sat, 28 Dec 2013 21:11:26 +0000 (+0000) Subject: some improvements and new lemmas for X-Git-Tag: make_still_working~1009 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4b7a1d1c4258c10822823cb5ee1949bcdf81abcb;p=helm.git some improvements and new lemmas for natural numbers with infinity --- 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 56159d210..b99da4bd6 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 @@ -8,7 +8,7 @@ table { ] class "yellow" [ { "natural numbers with infinity" * } { - [ "ynat ( ∞ )" "ynat_pred ( ⫰? )" "ynat_succ ( ⫯? )" "ynat_le ( ?≤? )" "ynat_lt ( ?<? )" "ynat_minus ( ? - ? )" "ynat_plus ( ? + ? )" * ] + [ "ynat ( ∞ )" "ynat_pred ( ⫰? )" "ynat_succ ( ⫯? )" "ynat_le ( ?≤? )" "ynat_lt ( ?<? )" "ynat_minus ( ? - ? )" "ynat_plus ( ? + ? )" "ynat_max" "ynat_min" * ] } ] class "orange" 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 ccb9563ee..a0fe07331 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_le.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_le.ma @@ -62,30 +62,20 @@ lemma yle_inv_Y1: ∀n. ∞ ≤ n → n = ∞. (* Inversion lemmas on successor ********************************************) -fact yle_inv_succ1_aux: ∀x,y. x ≤ y → ∀m. x = ⫯m → ∃∃n. m ≤ n & y = ⫯n. +fact yle_inv_succ1_aux: ∀x,y. 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 - @(ex2_intro … m) /2 width=1 by yle_inj/ (**) (* explicit constructor *) -| #x #y #H destruct - @(ex2_intro … (∞)) /2 width=1 by yle_Y/ (**) (* explicit constructor *) + #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. ⫯m ≤ y → ∃∃n. m ≤ n & y = ⫯n. +lemma yle_inv_succ1: ∀m,y. ⫯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 -#x #Hx #H destruct // -qed-. - -(* Forward lemmas on successor **********************************************) - -lemma yle_fwd_succ1: ∀m,n. ⫯m ≤ n → m ≤ ⫰n. -#m #x #H elim (yle_inv_succ1 … H) -H -#n #Hmn #H destruct // +#m #n #H elim (yle_inv_succ1 … H) -H // qed-. (* Basic properties *********************************************************) @@ -98,6 +88,12 @@ 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-. + (* Properties on predecessor ************************************************) lemma yle_pred_sn: ∀m,n. m ≤ n → ⫰m ≤ n. @@ -118,7 +114,11 @@ lemma yle_succ_dx: ∀m,n. m ≤ n → m ≤ ⫯n. qed. lemma yle_refl_S_dx: ∀x. x ≤ ⫯x. -/2 width=1 by yle_refl, yle_succ_dx/ qed. +/2 width=1 by yle_succ_dx/ qed. + +lemma yle_refl_SP_dx: ∀x. x ≤ ⫯⫰x. +* // * // +qed. (* Main properties **********************************************************) 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 b684c0403..0167ed27a 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma @@ -58,27 +58,26 @@ qed-. (* Inversion lemmas on successor ********************************************) -fact ylt_inv_succ1_aux: ∀x,y. x < y → ∀m. x = ⫯m → ∃∃n. m < n & y = ⫯n. +fact ylt_inv_succ1_aux: ∀x,y. 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 - @(ex2_intro … m) /2 width=1 by ylt_inj/ (**) (* explicit constructor *) + #m #Hnm #H destruct /3 width=1 by ylt_inj, conj/ | #x #y #H elim (ysucc_inv_inj_sn … H) -H - #m #H #_ destruct - @(ex2_intro … (∞)) /2 width=1 by/ (**) (* explicit constructor *) + #m #H #_ destruct /2 width=1 by ylt_Y, conj/ ] qed-. -lemma ylt_inv_succ1: ∀m,y. ⫯m < y → ∃∃n. m < n & y = ⫯n. +lemma ylt_inv_succ1: ∀m,y. ⫯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 -#x #Hx #H destruct // +#m #n #H elim (ylt_inv_succ1 … H) -H // qed-. -fact ylt_inv_succ2_aux: ∀x,y. x < y → ∀n. y = ⫯n → x ≤ n. +(* 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/ @@ -86,10 +85,8 @@ fact ylt_inv_succ2_aux: ∀x,y. x < y → ∀n. y = ⫯n → x ≤ n. ] qed-. -(* Forward lemmas on successor **********************************************) - lemma ylt_fwd_succ2: ∀m,n. m < ⫯n → m ≤ n. -/2 width=3 by ylt_inv_succ2_aux/ qed-. +/2 width=3 by ylt_fwd_succ2_aux/ qed-. (* inversion and forward lemmas on yle **************************************) @@ -147,4 +144,4 @@ theorem ylt_trans: Transitive … ylt. /3 width=3 by transitive_lt, ylt_inj/ (**) (* full auto too slow *) | #x #z #H elim (ylt_yle_false … H) // ] -qed-. +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 new file mode 100644 index 000000000..acbd31d9d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_max.ma @@ -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/ynat/ynat_min.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_min.ma new file mode 100644 index 000000000..7661dd486 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_min.ma @@ -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/ +| * // #m >yminus_Y_inj // +] +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 index 1110f3e44..ef28be4fe 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_minus.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_minus.ma @@ -35,6 +35,12 @@ lemma yminus_Y_inj: ∀n. ∞ - yinj n = ∞. #n #IHn >IHn // qed. +(* Properties on predecessor ************************************************) + +lemma yminus_SO2: ∀m. m - 1 = ⫰m. +* // +qed. + (* Properties on successor **************************************************) lemma yminus_succ: ∀n,m. ⫯m - ⫯n = m - n.