X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fminus.ma;h=6ff744dcb5a3aa5e8cc626b20ae2740bda00b49c;hb=33a02e0b639217093eb63f30169aaa6ac8c78907;hp=b4cff5d584ca3c16bf85ce285b3cf6d51f0e1307;hpb=633474751ddf1074947ff0d324fb1aca2293eff8;p=helm.git

diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma
index b4cff5d58..6ff744dcb 100644
--- a/helm/matita/library/nat/minus.ma
+++ b/helm/matita/library/nat/minus.ma
@@ -15,7 +15,7 @@
 
 set "baseuri" "cic:/matita/nat/minus".
 
-include "nat/orders_op.ma".
+include "nat/le_arith.ma".
 include "nat/compare.ma".
 
 let rec minus n m \def 
@@ -26,29 +26,30 @@ let rec minus n m \def
 	[O \Rightarrow (S p)
         | (S q) \Rightarrow minus p q ]].
 
+(*CSC: the URI must disappear: there is a bug now *)
+interpretation "natural minus" 'minus x y = (cic:/matita/nat/minus/minus.con x y).
 
-theorem minus_n_O: \forall n:nat.n=minus n O.
+theorem minus_n_O: \forall n:nat.n=n-O.
 intros.elim n.simplify.reflexivity.
 simplify.reflexivity.
 qed.
 
-theorem minus_n_n: \forall n:nat.O=minus n n.
+theorem minus_n_n: \forall n:nat.O=n-n.
 intros.elim n.simplify.
 reflexivity.
 simplify.apply H.
 qed.
 
-theorem minus_Sn_n: \forall n:nat. S O = minus (S n) n.
+theorem minus_Sn_n: \forall n:nat. S O = (S n)-n.
 intro.elim n.
 simplify.reflexivity.
 elim H.reflexivity.
 qed.
 
-theorem minus_Sn_m: \forall n,m:nat. 
-le m n \to minus (S n) m = S (minus n m).
+theorem minus_Sn_m: \forall n,m:nat. m \leq n \to (S n)-m = S (n-m).
 intros 2.
 apply nat_elim2
-(\lambda n,m.le m n \to minus (S n) m = S (minus n m)).
+(\lambda n,m.m \leq n \to (S n)-m = S (n-m)).
 intros.apply le_n_O_elim n1 H.
 simplify.reflexivity.
 intros.simplify.reflexivity.
@@ -57,10 +58,10 @@ apply le_S_S_to_le. assumption.
 qed.
 
 theorem plus_minus:
-\forall n,m,p:nat. le m n \to plus (minus n m) p = minus (plus n p) m.
+\forall n,m,p:nat. m \leq n \to (n-m)+p = (n+p)-m.
 intros 2.
 apply nat_elim2
-(\lambda n,m.\forall p:nat.le m n \to plus (minus n m) p = minus (plus n p) m).
+(\lambda n,m.\forall p:nat.m \leq n \to (n-m)+p = (n+p)-m).
 intros.apply le_n_O_elim ? H.
 simplify.rewrite < minus_n_O.reflexivity.
 intros.simplify.reflexivity.
@@ -68,9 +69,9 @@ intros.simplify.apply H.apply le_S_S_to_le.assumption.
 qed.
 
 theorem plus_minus_m_m: \forall n,m:nat.
-le m n \to n = plus (minus n m) m.
+m \leq n \to n = (n-m)+m.
 intros 2.
-apply nat_elim2 (\lambda n,m.le m n \to n = plus (minus n m) m).
+apply nat_elim2 (\lambda n,m.m \leq n \to n = (n-m)+m).
 intros.apply le_n_O_elim n1 H.
 reflexivity.
 intros.simplify.rewrite < plus_n_O.reflexivity.
@@ -79,16 +80,16 @@ apply eq_f.rewrite < sym_plus.apply H.
 apply le_S_S_to_le.assumption.
 qed.
 
-theorem minus_to_plus :\forall n,m,p:nat.le m n \to minus n m = p \to 
-n = plus m p.
-intros.apply trans_eq ? ? (plus (minus n m) m) ?.
+theorem minus_to_plus :\forall n,m,p:nat.m \leq n \to n-m = p \to 
+n = m+p.
+intros.apply trans_eq ? ? ((n-m)+m) ?.
 apply plus_minus_m_m.
 apply H.elim H1.
 apply sym_plus.
 qed.
 
-theorem plus_to_minus :\forall n,m,p:nat.le m n \to
-n = plus m p \to minus n m = p.
+theorem plus_to_minus :\forall n,m,p:nat.m \leq n \to
+n = m+p \to n-m = p.
 intros.
 apply inj_plus_r m.
 rewrite < H1.
@@ -97,10 +98,24 @@ symmetry.
 apply plus_minus_m_m.assumption.
 qed.
 
+theorem minus_S_S : \forall n,m:nat.
+eq nat (minus (S n) (S m)) (minus n m).
+intros.
+reflexivity.
+qed.
+
+theorem minus_pred_pred : \forall n,m:nat. lt O n \to lt O m \to 
+eq nat (minus (pred n) (pred m)) (minus n m).
+intros.
+apply lt_O_n_elim n H.intro.
+apply lt_O_n_elim m H1.intro.
+simplify.reflexivity.
+qed.
+
 theorem eq_minus_n_m_O: \forall n,m:nat.
-le n m \to minus n m = O.
+n \leq m \to n-m = O.
 intros 2.
-apply nat_elim2 (\lambda n,m.le n m \to minus n m = O).
+apply nat_elim2 (\lambda n,m.n \leq m \to n-m = O).
 intros.simplify.reflexivity.
 intros.apply False_ind.
 (* ancora problemi con il not *)
@@ -109,40 +124,110 @@ intros.
 simplify.apply H.apply le_S_S_to_le. apply H1.
 qed.
 
-theorem le_SO_minus: \forall n,m:nat.le (S n) m \to le (S O) (minus m n).
+theorem le_SO_minus: \forall n,m:nat.S n \leq m \to S O \leq m-n.
 intros.elim H.elim minus_Sn_n n.apply le_n.
 rewrite > minus_Sn_m.
 apply le_S.assumption.
 apply lt_to_le.assumption.
 qed.
 
-(*
-theorem le_plus_minus: \forall n,m,p. (le (plus n m) p) \to (le n (minus p m)).
-intros 3.
-elim p.simplify.apply trans_le ? (plus n m) ?.
-elim sym_plus ? ?.
-apply plus_le.assumption.
-apply le_n_Sm_elim ? ? H1.
+theorem minus_le_S_minus_S: \forall n,m:nat. m-n \leq S (m-(S n)).
+intros.apply nat_elim2 (\lambda n,m.m-n \leq S (m-(S n))).
+intro.elim n1.simplify.apply le_n_Sn.
+simplify.rewrite < minus_n_O.apply le_n.
+intros.simplify.apply le_n_Sn.
+intros.simplify.apply H.
+qed.
+
+theorem lt_minus_S_n_to_le_minus_n : \forall n,m,p:nat. m-(S n) < p \to m-n \leq p. 
+intros 3.simplify.intro.
+apply trans_le (m-n) (S (m-(S n))) p.
+apply minus_le_S_minus_S.
+assumption.
+qed.
+
+theorem le_minus_m: \forall n,m:nat. n-m \leq n.
+intros.apply nat_elim2 (\lambda m,n. n-m \leq n).
+intros.rewrite < minus_n_O.apply le_n.
+intros.simplify.apply le_n.
+intros.simplify.apply le_S.assumption.
+qed.
+
+theorem lt_minus_m: \forall n,m:nat. O < n \to O < m \to n-m \lt n.
+intros.apply lt_O_n_elim n H.intro.
+apply lt_O_n_elim m H1.intro.
+simplify.apply le_S_S.apply le_minus_m.
+qed.
+
+theorem minus_le_O_to_le: \forall n,m:nat. n-m \leq O \to n \leq m.
+intros 2.
+apply nat_elim2 (\lambda n,m:nat.n-m \leq O \to n \leq m).
+intros.apply le_O_n.
+simplify.intros. assumption.
+simplify.intros.apply le_S_S.apply H.assumption.
+qed.
+
+(* galois *)
+theorem monotonic_le_minus_r: 
+\forall p,q,n:nat. q \leq p \to n-p \le n-q.
+simplify.intros 2.apply nat_elim2 
+(\lambda p,q.\forall a.q \leq p \to a-p \leq a-q).
+intros.apply le_n_O_elim n H.apply le_n.
+intros.rewrite < minus_n_O.
+apply le_minus_m.
+intros.elim a.simplify.apply le_n.
+simplify.apply H.apply le_S_S_to_le.assumption.
+qed.
+
+theorem le_minus_to_plus: \forall n,m,p. (le (n-m) p) \to (le n (p+m)).
+intros 2.apply nat_elim2 (\lambda n,m.\forall p.(le (n-m) p) \to (le n (p+m))).
+intros.apply le_O_n.
+simplify.intros.rewrite < plus_n_O.assumption.
 intros.
-*)
+rewrite < plus_n_Sm.
+apply le_S_S.apply H.
+exact H1.
+qed.
+
+theorem le_plus_to_minus: \forall n,m,p. (le n (p+m)) \to (le (n-m) p).
+intros 2.apply nat_elim2 (\lambda n,m.\forall p.(le n (p+m)) \to (le (n-m) p)).
+intros.simplify.apply le_O_n.
+intros 2.rewrite < plus_n_O.intro.simplify.assumption.
+intros.simplify.apply H.
+apply le_S_S_to_le.rewrite > plus_n_Sm.assumption.
+qed.
+
+(* the converse of le_plus_to_minus does not hold *)
+theorem le_plus_to_minus_r: \forall n,m,p. (le (n+m) p) \to (le n (p-m)).
+intros 3.apply nat_elim2 (\lambda m,p.(le (n+m) p) \to (le n (p-m))).
+intro.rewrite < plus_n_O.rewrite < minus_n_O.intro.assumption.
+intro.intro.cut n=O.rewrite > Hcut.apply le_O_n.
+apply sym_eq. apply le_n_O_to_eq.
+apply trans_le ? (n+(S n1)).
+rewrite < sym_plus.
+apply le_plus_n.assumption.
+intros.simplify.
+apply H.apply le_S_S_to_le.
+rewrite > plus_n_Sm.assumption.
+qed.
+
 
 theorem distributive_times_minus: distributive nat times minus.
 simplify.
 intros.
 apply (leb_elim z y).intro.
-cut plus (times x (minus y z)) (times x z) =
-    plus (minus (times x y) (times x z)) (times x z).
-apply inj_plus_l (times x z).
+cut x*(y-z)+x*z = (x*y-x*z)+x*z.
+apply inj_plus_l (x*z).
 assumption.
-apply trans_eq nat ? (times x y).
-rewrite < times_plus_distr. 
+apply trans_eq nat ? (x*y).
+rewrite < distr_times_plus. 
 rewrite < plus_minus_m_m ? ? H.reflexivity.
 rewrite < plus_minus_m_m ? ? ?.reflexivity.
 apply le_times_r.
 assumption.
 intro.
 rewrite > eq_minus_n_m_O.
-rewrite > eq_minus_n_m_O (times x y).
+rewrite > eq_minus_n_m_O (x*y).
 rewrite < sym_times.simplify.reflexivity.
 apply lt_to_le.
 apply not_le_to_lt.assumption.
@@ -150,12 +235,44 @@ apply le_times_r.apply lt_to_le.
 apply not_le_to_lt.assumption.
 qed.
 
-theorem distr_times_minus: \forall n,m,p:nat.
-times n (minus m p) = minus (times n m) (times n p)
+theorem distr_times_minus: \forall n,m,p:nat. n*(m-p) = n*m-n*p
 \def distributive_times_minus.
 
-theorem le_minus_m: \forall n,m:nat. le (minus n m) n.
-intro.elim n.simplify.apply le_n.
-elim m.simplify.apply le_n.
-simplify.apply le_S.apply H.
+theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p).
+intros.
+cut m+p \le n \or \not m+p \le n.
+elim Hcut.
+apply sym_eq.
+apply plus_to_minus.assumption.
+rewrite > assoc_plus.
+rewrite > sym_plus p.
+rewrite < plus_minus_m_m.
+rewrite > sym_plus.
+rewrite < plus_minus_m_m.reflexivity.
+rewrite > eq_minus_n_m_O n (m+p).
+rewrite > eq_minus_n_m_O (n-m) p.reflexivity.
+apply decidable_le (m+p) n.
+apply le_plus_to_minus_r.
+rewrite > sym_plus.assumption.
+apply trans_le ? (m+p).
+rewrite < sym_plus.
+apply le_plus_n.assumption.
+apply lt_to_le.apply not_le_to_lt.assumption.
+apply le_plus_to_minus.
+apply lt_to_le.apply not_le_to_lt.
+rewrite < sym_plus.assumption.
+qed.
+
+theorem eq_plus_minus_minus_minus: \forall n,m,p:nat. p \le m \to m \le n \to
+p+(n-m) = n-(m-p).
+intros.
+apply sym_eq.
+apply plus_to_minus.
+apply le_plus_to_minus.
+apply trans_le ? n.assumption.rewrite < sym_plus.apply le_plus_n.
+rewrite < assoc_plus.
+rewrite < plus_minus_m_m.
+rewrite < sym_plus.
+rewrite < plus_minus_m_m.reflexivity.
+assumption.assumption.
 qed.