From 03d30a78581b24842e1f425b41861e5ae8f912b5 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 13 Mar 2007 10:58:06 +0000
Subject: [PATCH] Few theorems added.`

---
 matita/library/nat/compare.ma     | 60 +++++++++++++++++++++++++------
 matita/library/nat/div_and_mod.ma |  4 +--
 matita/library/nat/le_arith.ma    |  5 +++
 matita/library/nat/minus.ma       | 51 ++++++++++++++++++++++++++
 matita/library/nat/nat.ma         |  2 +-
 matita/library/nat/orders.ma      | 24 +++++++++----
 matita/library/nat/plus.ma        |  5 +++
 7 files changed, 130 insertions(+), 21 deletions(-)

diff --git a/matita/library/nat/compare.ma b/matita/library/nat/compare.ma
index 264731580..c701cd2e7 100644
--- a/matita/library/nat/compare.ma
+++ b/matita/library/nat/compare.ma
@@ -112,23 +112,60 @@ match n with
 	match m with 
         [ O \Rightarrow false
 	| (S q) \Rightarrow leb p q]].
-	
+
+theorem leb_elim: \forall n,m:nat. \forall P:bool \to Prop. 
+(n \leq m \to (P true)) \to (n \nleq m \to (P false)) \to
+P (leb n m).
+apply nat_elim2; intros; simplify
+  [apply H.apply le_O_n
+  |apply H1.apply not_le_Sn_O.
+  |apply H;intros
+    [apply H1.apply le_S_S.assumption.
+    |apply H2.unfold Not.intros.apply H3.apply le_S_S_to_le.assumption
+    ]
+  ]
+qed.
+
+(*
+theorem decidable_le: \forall n,m. n \leq m \lor n \nleq m. 
+intros.
+apply (leb_elim n m)
+  [intro.left.assumption
+  |intro.right.assumption
+  ]
+qed.
+*)
+
+theorem le_to_leb_true: \forall n,m. n \leq m \to leb n m = true.
+intros.apply leb_elim;intros
+  [reflexivity
+  |apply False_ind.apply H1.apply H.
+  ]
+qed.
+
+theorem lt_to_leb_false: \forall n,m. m < n \to leb n m = false.
+intros.apply leb_elim;intros
+  [apply False_ind.apply (le_to_not_lt ? ? H1). assumption
+  |reflexivity
+  ]
+qed.
+
 theorem leb_to_Prop: \forall n,m:nat. 
 match (leb n m) with
 [ true  \Rightarrow n \leq m 
 | false \Rightarrow n \nleq m].
-intros.
-apply (nat_elim2
-(\lambda n,m:nat.match (leb n m) with
-[ true  \Rightarrow n \leq m 
-| false \Rightarrow n \nleq m])).
-simplify.exact le_O_n.
-simplify.exact not_le_Sn_O.
-intros 2.simplify.elim ((leb n1 m1)).
-simplify.apply le_S_S.apply H.
-simplify.unfold Not.intros.apply H.apply le_S_S_to_le.assumption.
+apply nat_elim2;simplify
+  [exact le_O_n
+  |exact not_le_Sn_O
+  |intros 2.simplify.
+   elim ((leb n m));simplify
+    [apply le_S_S.apply H
+    |unfold Not.intros.apply H.apply le_S_S_to_le.assumption
+    ]
+  ]
 qed.
 
+(*
 theorem leb_elim: \forall n,m:nat. \forall P:bool \to Prop. 
 (n \leq m \to (P true)) \to (n \nleq m \to (P false)) \to
 P (leb n m).
@@ -142,6 +179,7 @@ elim (leb n m).
 apply ((H H2)).
 apply ((H1 H2)).
 qed.
+*)
 
 let rec nat_compare n m: compare \def
 match n with
diff --git a/matita/library/nat/div_and_mod.ma b/matita/library/nat/div_and_mod.ma
index 73ff78998..ccddcca3f 100644
--- a/matita/library/nat/div_and_mod.ma
+++ b/matita/library/nat/div_and_mod.ma
@@ -28,7 +28,7 @@ match (leb m n) with
 definition mod : nat \to nat \to nat \def
 \lambda n,m.
 match m with 
-[O \Rightarrow m
+[O \Rightarrow n
 | (S p) \Rightarrow mod_aux n n p]. 
 
 interpretation "natural remainder" 'module x y =
@@ -143,7 +143,7 @@ rewrite > distr_times_minus.
 rewrite > plus_minus.
 rewrite > sym_times.
 rewrite < H5.
-rewrite < sym_times.
+rewrite < sym_times. 
 apply plus_to_minus.
 apply H3.
 apply le_times_r.
diff --git a/matita/library/nat/le_arith.ma b/matita/library/nat/le_arith.ma
index a76183063..ae386d313 100644
--- a/matita/library/nat/le_arith.ma
+++ b/matita/library/nat/le_arith.ma
@@ -51,6 +51,11 @@ intros.change with (O+m \le n+m).
 apply le_plus_l.apply le_O_n.
 qed.
 
+theorem le_plus_n_r :\forall n,m:nat. m \le m + n.
+intros.rewrite > sym_plus.
+apply le_plus_n.
+qed.
+
 theorem eq_plus_to_le: \forall n,m,p:nat.n=m+p \to m \le n.
 intros.rewrite > H.
 rewrite < sym_plus.
diff --git a/matita/library/nat/minus.ma b/matita/library/nat/minus.ma
index 710418d72..71c2cc205 100644
--- a/matita/library/nat/minus.ma
+++ b/matita/library/nat/minus.ma
@@ -57,6 +57,14 @@ intros.rewrite < H.reflexivity.
 apply le_S_S_to_le. assumption.
 qed.
 
+theorem eq_minus_S_pred: \forall n,m. n - (S m) = pred(n -m).
+apply nat_elim2
+  [intro.reflexivity
+  |intro.simplify.auto
+  |intros.simplify.assumption
+  ]
+qed.
+
 theorem plus_minus:
 \forall n,m,p:nat. m \leq n \to (n-m)+p = (n+p)-m.
 intros 2.
@@ -226,6 +234,49 @@ rewrite > plus_n_Sm.assumption.
 qed.
 
 (* minus and lt - to be completed *)
+theorem lt_minus_l: \forall m,l,n:nat. 
+  l < m \to m \le n \to n - m < n - l.
+apply nat_elim2
+  [intros.apply False_ind.apply (not_le_Sn_O ? H)
+  |intros.rewrite < minus_n_O.
+   auto
+  |intros.
+   generalize in match H2.
+   apply (nat_case n1)
+    [intros.apply False_ind.apply (not_le_Sn_O ? H3)
+    |intros.simplify.
+     apply H
+      [
+       apply lt_S_S_to_lt.
+       assumption
+      |apply le_S_S_to_le.assumption
+      ]
+    ]
+  ]
+qed.
+
+theorem lt_minus_r: \forall n,m,l:nat. 
+  n \le l \to l < m \to l -n < m -n.
+intro.elim n
+  [applyS H1
+  |rewrite > eq_minus_S_pred.
+   rewrite > eq_minus_S_pred.
+   apply lt_pred
+    [unfold lt.apply le_plus_to_minus_r.applyS H1
+    |apply H[auto|assumption]
+    ]
+  ]
+qed.
+
+lemma lt_to_lt_O_minus : \forall m,n.
+  n < m \to O < m - n.
+intros.  
+unfold. apply le_plus_to_minus_r. unfold in H. rewrite > sym_plus. 
+rewrite < plus_n_Sm. 
+rewrite < plus_n_O. 
+assumption.
+qed.  
+
 theorem lt_minus_to_plus: \forall n,m,p. (lt n (p-m)) \to (lt (n+m) p).
 intros 3.apply (nat_elim2 (\lambda m,p.(lt n (p-m)) \to (lt (n+m) p))).
 intro.rewrite < plus_n_O.rewrite < minus_n_O.intro.assumption.
diff --git a/matita/library/nat/nat.ma b/matita/library/nat/nat.ma
index b600072c6..b54bc76a9 100644
--- a/matita/library/nat/nat.ma
+++ b/matita/library/nat/nat.ma
@@ -26,7 +26,7 @@ definition pred: nat \to nat \def
  | (S p) \Rightarrow p ].
 
 theorem pred_Sn : \forall n:nat.n=(pred (S n)).
- intros. reflexivity.
+ intros. simplify. reflexivity.
 qed.
 
 theorem injective_S : injective nat nat S.
diff --git a/matita/library/nat/orders.ma b/matita/library/nat/orders.ma
index 807906bd2..8c6ce942e 100644
--- a/matita/library/nat/orders.ma
+++ b/matita/library/nat/orders.ma
@@ -22,9 +22,8 @@ inductive le (n:nat) : nat \to Prop \def
   | le_n : le n n
   | le_S : \forall m:nat. le n m \to le n (S m).
 
-(*CSC: the URI must disappear: there is a bug now *)
 interpretation "natural 'less or equal to'" 'leq x y = (cic:/matita/nat/orders/le.ind#xpointer(1/1) x y).
-(*CSC: the URI must disappear: there is a bug now *)
+
 interpretation "natural 'neither less nor equal to'" 'nleq x y =
   (cic:/matita/logic/connectives/Not.con
     (cic:/matita/nat/orders/le.ind#xpointer(1/1) x y)).
@@ -32,24 +31,21 @@ interpretation "natural 'neither less nor equal to'" 'nleq x y =
 definition lt: nat \to nat \to Prop \def
 \lambda n,m:nat.(S n) \leq m.
 
-(*CSC: the URI must disappear: there is a bug now *)
 interpretation "natural 'less than'" 'lt x y = (cic:/matita/nat/orders/lt.con x y).
-(*CSC: the URI must disappear: there is a bug now *)
+
 interpretation "natural 'not less than'" 'nless x y =
   (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/orders/lt.con x y)).
 
 definition ge: nat \to nat \to Prop \def
 \lambda n,m:nat.m \leq n.
 
-(*CSC: the URI must disappear: there is a bug now *)
 interpretation "natural 'greater or equal to'" 'geq x y = (cic:/matita/nat/orders/ge.con x y).
 
 definition gt: nat \to nat \to Prop \def
 \lambda n,m:nat.m<n.
 
-(*CSC: the URI must disappear: there is a bug now *)
 interpretation "natural 'greater than'" 'gt x y = (cic:/matita/nat/orders/gt.con x y).
-(*CSC: the URI must disappear: there is a bug now *)
+
 interpretation "natural 'not greater than'" 'ngtr x y =
   (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/orders/gt.con x y)).
 
@@ -99,6 +95,11 @@ elim H.apply le_n.apply (trans_le ? (pred n1)).assumption.
 apply le_pred_n.
 qed.
 
+theorem lt_S_S_to_lt: \forall n,m. 
+  S n < S m \to n < m.
+intros. apply le_S_S_to_le. assumption.
+qed.
+
 theorem leS_to_not_zero : \forall n,m:nat. S n \leq m \to not_zero m.
 intros.elim H.exact I.exact I.
 qed.
@@ -114,6 +115,15 @@ apply H.assumption.
 apply le_S_S_to_le.assumption.
 qed.
 
+theorem lt_pred: \forall n,m. 
+  O < n \to n < m \to pred n < pred m. 
+apply nat_elim2
+  [intros.apply False_ind.apply (not_le_Sn_O ? H)
+  |intros.apply False_ind.apply (not_le_Sn_O ? H1)
+  |intros.simplify.unfold.apply le_S_S_to_le.assumption
+  ]
+qed.
+
 (* le to lt or eq *)
 theorem le_to_or_lt_eq : \forall n,m:nat. 
 n \leq m \to n < m \lor n = m.
diff --git a/matita/library/nat/plus.ma b/matita/library/nat/plus.ma
index d595dad19..e8b5f6d29 100644
--- a/matita/library/nat/plus.ma
+++ b/matita/library/nat/plus.ma
@@ -36,6 +36,11 @@ simplify.reflexivity.
 simplify.apply eq_f.assumption.
 qed.
 
+theorem plus_n_SO : \forall n:nat. S n = n+(S O).
+intro.rewrite > plus_n_O.
+apply plus_n_Sm.
+qed.
+
 theorem sym_plus: \forall n,m:nat. n+m = m+n.
 intros.elim n.
 simplify.apply plus_n_O.
-- 
2.39.2