- improved arithmetics for natural numbers with infinity

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / ynat / ynat_plus.ma

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 8f348733e461e1806e7bf111bcfc14109fa65531..f872f93e22224cbe2b1fb82e1b861c2adf5b5d5b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma
@@ -12,13 +12,13 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground_2/ynat/ynat_lt.ma".
+include "ground_2/ynat/ynat_minus.ma".
 
 (* NATURAL NUMBERS WITH INFINITY ********************************************)
 
 (* addition *)
-definition yplus: ynat → ynat → ynat ≝ λx,y. match x with
-[ yinj m ⇒ ysucc^m y
+definition yplus: ynat → ynat → ynat ≝ λx,y. match y with
+[ yinj n ⇒ ysucc^n x
 | Y      ⇒ Y
 ].
 
@@ -26,22 +26,30 @@ interpretation "ynat plus" 'plus x y = (yplus x y).
 
 (* Properties on successor **************************************************)
 
-lemma yplus_succ1: ∀m,n. (⫯m) + n = ⫯(m + n).
-* //
+lemma yplus_succ2: ∀m,n. m + ⫯n = ⫯(m + n).
+#m * //
+qed.
+
+lemma yplus_succ1: ∀m,n. ⫯m + n = ⫯(m + n).
+#m * normalize //
 qed.
 
-lemma yplus_SO1: ∀m. 1 + m = ⫯m.
+lemma yplus_succ_swap: ∀m,n. m + ⫯n = ⫯m + n.
+// qed.
+
+lemma yplus_SO2: ∀m. m + 1 = ⫯m.
 * //
-qed. 
+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 //
+lemma yplus_inj: ∀n,m. yinj m + yinj n = yinj (m + n).
+#n elim n -n [ normalize // ]
+#n #IHn #m >(yplus_succ2 ? n) >IHn -IHn
+<plus_n_Sm //
 qed.
 
-lemma yplus_Y2: ∀m. (m + ∞) = ∞.
+lemma yplus_Y1: ∀m. ∞ + m = ∞.
 * normalize //
 qed.
 
@@ -51,7 +59,39 @@ normalize >ysucc_iter_Y //
 qed.
 
 lemma yplus_assoc: associative … yplus.
-* // #x * //
-#y #z >yplus_inj whd in ⊢ (??%%); >iter_plus //
+#x #y * // #z cases y -y
+[ #y >yplus_inj whd in ⊢ (??%%); <iter_plus //
+| >yplus_Y1 //
+]
 qed.
 
+lemma yplus_O_sn: ∀n:ynat. 0 + n = n.
+#n >yplus_comm // 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-.
+
+(* 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.
+
+(* 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-.