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 56159d210733bc9a8b1eee9a0a5b38e797f05bff..b99da4bd698ca2cfa93d08ba13d4958443834696 100644 (file)
--- 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 ccb9563ee875b23e587956f0b0032602c259e954..a0fe073311dbfb29c4d3c5abe81523af225bad56 100644 (file)
--- 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 b684c0403d4fb146169d0acc84b43b089123debf..0167ed27a9a20e410520916291d66ebbe6b71081 100644 (file)
--- 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 (file)
index 0000000..acbd31d
--- /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 (file)
index 0000000..7661dd4
--- /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 1110f3e44cdd72f41555d45a6c82e80cb99bf234..ef28be4fe5a8a9581ce221715f0acae284136638 100644 (file)
--- 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.