From: Ferruccio Guidi Date: Fri, 29 Nov 2013 16:33:57 +0000 (+0000) Subject: addition for natural numbers with infinity X-Git-Tag: make_still_working~1040 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b3f8b89278d193ed0aa0f39e7f8d74cf1de81d8d;p=helm.git addition for natural numbers with infinity --- diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma index 732c1b64c..0cbcff85e 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma @@ -134,6 +134,10 @@ lemma iter_n_Sm: ∀B:Type[0]. ∀f:B→B. ∀b,l. f^l (f b) = f (f^l b). #B #f #b #l elim l -l normalize // qed. +lemma iter_plus: ∀B:Type[0]. ∀f:B→B. ∀b,l1,l2. f^(l1+l2) b = f^l1 (f^l2 b). +#B #f #b #l1 elim l1 -l1 normalize // +qed. + (* Trichotomy operator ******************************************************) (* Note: this is "if eqb n1 n2 then a2 else if leb n1 n2 then a1 else a3" *) 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 8bc1e8538..827a8fcf8 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 ( ∞ )" "ynat_pred ( ⫰? )" "ynat_succ ( ⫯? )" "ynat_le ( ?≤? )" "ynat_lt ( ?<? )" "ynat_plus ( ? + ? )" * ] } ] class "orange" diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma new file mode 100644 index 000000000..8f348733e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma @@ -0,0 +1,57 @@ +(**************************************************************************) +(* ___ *) +(* ||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 ********************************************) + +(* addition *) +definition yplus: ynat → ynat → ynat ≝ λx,y. match x with +[ yinj m ⇒ ysucc^m y +| Y ⇒ Y +]. + +interpretation "ynat plus" 'plus x y = (yplus x y). + +(* Properties on successor **************************************************) + +lemma yplus_succ1: ∀m,n. (⫯m) + n = ⫯(m + n). +* // +qed. + +lemma yplus_SO1: ∀m. 1 + m = ⫯m. +* // +qed. + +(* Basic properties *********************************************************) + +lemma yplus_inj: ∀m,n. yinj m + yinj n = yinj (m + n). +#m elim m -m // +#m #IHm #n >(yplus_succ1 m) >IHm -IHm // +qed. + +lemma yplus_Y2: ∀m. (m + ∞) = ∞. +* normalize // +qed. + +lemma yplus_comm: commutative … yplus. +* [ #m ] * [1,3: #n ] // +normalize >ysucc_iter_Y // +qed. + +lemma yplus_assoc: associative … yplus. +* // #x * // +#y #z >yplus_inj whd in ⊢ (??%%); >iter_plus // +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 c244b9cae..a8d1946be 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma @@ -38,6 +38,11 @@ lemma ynat_cases: ∀n:ynat. n = 0 ∨ ∃m. n = ⫯m. ] qed-. +lemma ysucc_iter_Y: ∀m. ysucc^m (∞) = ∞. +#m elim m -m // +#m #IHm whd in ⊢ (??%?); >IHm // +qed. + (* Inversion lemmas *********************************************************) lemma ysucc_inj: ∀m,n. ⫯m = ⫯n → m = n.