1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
16 set "baseuri" "cic:/matita/nat/minus".
18 include "nat/le_arith.ma".
19 include "nat/compare.ma".
21 let rec minus n m \def
27 | (S q) \Rightarrow minus p q ]].
29 (*CSC: the URI must disappear: there is a bug now *)
30 interpretation "natural minus" 'minus x y = (cic:/matita/nat/minus/minus.con x y).
32 theorem minus_n_O: \forall n:nat.n=n-O.
33 intros.elim n.simplify.reflexivity.
37 theorem minus_n_n: \forall n:nat.O=n-n.
38 intros.elim n.simplify.
43 theorem minus_Sn_n: \forall n:nat. S O = (S n)-n.
49 theorem minus_Sn_m: \forall n,m:nat. m \leq n \to (S n)-m = S (n-m).
52 (\lambda n,m.m \leq n \to (S n)-m = S (n-m)).
53 intros.apply le_n_O_elim n1 H.
55 intros.simplify.reflexivity.
56 intros.rewrite < H.reflexivity.
57 apply le_S_S_to_le. assumption.
61 \forall n,m,p:nat. m \leq n \to (n-m)+p = (n+p)-m.
64 (\lambda n,m.\forall p:nat.m \leq n \to (n-m)+p = (n+p)-m).
65 intros.apply le_n_O_elim ? H.
66 simplify.rewrite < minus_n_O.reflexivity.
67 intros.simplify.reflexivity.
68 intros.simplify.apply H.apply le_S_S_to_le.assumption.
71 theorem minus_plus_m_m: \forall n,m:nat.n = (n+m)-m.
73 generalize in match n.
75 rewrite < minus_n_O.apply plus_n_O.
79 change with S n3 = (S n3 + n1)-n1.
83 theorem plus_minus_m_m: \forall n,m:nat.
84 m \leq n \to n = (n-m)+m.
86 apply nat_elim2 (\lambda n,m.m \leq n \to n = (n-m)+m).
87 intros.apply le_n_O_elim n1 H.
89 intros.simplify.rewrite < plus_n_O.reflexivity.
90 intros.simplify.rewrite < sym_plus.simplify.
91 apply eq_f.rewrite < sym_plus.apply H.
92 apply le_S_S_to_le.assumption.
95 theorem minus_to_plus :\forall n,m,p:nat.m \leq n \to n-m = p \to
97 intros.apply trans_eq ? ? ((n-m)+m).
103 theorem plus_to_minus :\forall n,m,p:nat.
110 apply plus_minus_m_m.rewrite > H.
115 theorem minus_S_S : \forall n,m:nat.
116 eq nat (minus (S n) (S m)) (minus n m).
121 theorem minus_pred_pred : \forall n,m:nat. lt O n \to lt O m \to
122 eq nat (minus (pred n) (pred m)) (minus n m).
124 apply lt_O_n_elim n H.intro.
125 apply lt_O_n_elim m H1.intro.
126 simplify.reflexivity.
129 theorem eq_minus_n_m_O: \forall n,m:nat.
130 n \leq m \to n-m = O.
132 apply nat_elim2 (\lambda n,m.n \leq m \to n-m = O).
133 intros.simplify.reflexivity.
134 intros.apply False_ind.
138 simplify.apply H.apply le_S_S_to_le. apply H1.
141 theorem le_SO_minus: \forall n,m:nat.S n \leq m \to S O \leq m-n.
142 intros.elim H.elim minus_Sn_n n.apply le_n.
143 rewrite > minus_Sn_m.
144 apply le_S.assumption.
145 apply lt_to_le.assumption.
148 theorem minus_le_S_minus_S: \forall n,m:nat. m-n \leq S (m-(S n)).
149 intros.apply nat_elim2 (\lambda n,m.m-n \leq S (m-(S n))).
150 intro.elim n1.simplify.apply le_n_Sn.
151 simplify.rewrite < minus_n_O.apply le_n.
152 intros.simplify.apply le_n_Sn.
153 intros.simplify.apply H.
156 theorem lt_minus_S_n_to_le_minus_n : \forall n,m,p:nat. m-(S n) < p \to m-n \leq p.
157 intros 3.simplify.intro.
158 apply trans_le (m-n) (S (m-(S n))) p.
159 apply minus_le_S_minus_S.
163 theorem le_minus_m: \forall n,m:nat. n-m \leq n.
164 intros.apply nat_elim2 (\lambda m,n. n-m \leq n).
165 intros.rewrite < minus_n_O.apply le_n.
166 intros.simplify.apply le_n.
167 intros.simplify.apply le_S.assumption.
170 theorem lt_minus_m: \forall n,m:nat. O < n \to O < m \to n-m \lt n.
171 intros.apply lt_O_n_elim n H.intro.
172 apply lt_O_n_elim m H1.intro.
173 simplify.apply le_S_S.apply le_minus_m.
176 theorem minus_le_O_to_le: \forall n,m:nat. n-m \leq O \to n \leq m.
178 apply nat_elim2 (\lambda n,m:nat.n-m \leq O \to n \leq m).
180 simplify.intros. assumption.
181 simplify.intros.apply le_S_S.apply H.assumption.
185 theorem monotonic_le_minus_r:
186 \forall p,q,n:nat. q \leq p \to n-p \le n-q.
187 simplify.intros 2.apply nat_elim2
188 (\lambda p,q.\forall a.q \leq p \to a-p \leq a-q).
189 intros.apply le_n_O_elim n H.apply le_n.
190 intros.rewrite < minus_n_O.
192 intros.elim a.simplify.apply le_n.
193 simplify.apply H.apply le_S_S_to_le.assumption.
196 theorem le_minus_to_plus: \forall n,m,p. (le (n-m) p) \to (le n (p+m)).
197 intros 2.apply nat_elim2 (\lambda n,m.\forall p.(le (n-m) p) \to (le n (p+m))).
199 simplify.intros.rewrite < plus_n_O.assumption.
202 apply le_S_S.apply H.
206 theorem le_plus_to_minus: \forall n,m,p. (le n (p+m)) \to (le (n-m) p).
207 intros 2.apply nat_elim2 (\lambda n,m.\forall p.(le n (p+m)) \to (le (n-m) p)).
208 intros.simplify.apply le_O_n.
209 intros 2.rewrite < plus_n_O.intro.simplify.assumption.
210 intros.simplify.apply H.
211 apply le_S_S_to_le.rewrite > plus_n_Sm.assumption.
214 (* the converse of le_plus_to_minus does not hold *)
215 theorem le_plus_to_minus_r: \forall n,m,p. (le (n+m) p) \to (le n (p-m)).
216 intros 3.apply nat_elim2 (\lambda m,p.(le (n+m) p) \to (le n (p-m))).
217 intro.rewrite < plus_n_O.rewrite < minus_n_O.intro.assumption.
218 intro.intro.cut n=O.rewrite > Hcut.apply le_O_n.
219 apply sym_eq. apply le_n_O_to_eq.
220 apply trans_le ? (n+(S n1)).
222 apply le_plus_n.assumption.
224 apply H.apply le_S_S_to_le.
225 rewrite > plus_n_Sm.assumption.
229 theorem distributive_times_minus: distributive nat times minus.
232 apply (leb_elim z y).
233 intro.cut x*(y-z)+x*z = (x*y-x*z)+x*z.
234 apply inj_plus_l (x*z).assumption.
235 apply trans_eq nat ? (x*y).
236 rewrite < distr_times_plus.rewrite < plus_minus_m_m ? ? H.reflexivity.
237 rewrite < plus_minus_m_m.
239 apply le_times_r.assumption.
240 intro.rewrite > eq_minus_n_m_O.
241 rewrite > eq_minus_n_m_O (x*y).
242 rewrite < sym_times.simplify.reflexivity.
243 apply le_times_r.apply lt_to_le.apply not_le_to_lt.assumption.
244 apply lt_to_le.apply not_le_to_lt.assumption.
247 theorem distr_times_minus: \forall n,m,p:nat. n*(m-p) = n*m-n*p
248 \def distributive_times_minus.
250 theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p).
252 cut m+p \le n \or m+p \nleq n.
254 symmetry.apply plus_to_minus.
255 rewrite > assoc_plus.rewrite > sym_plus p.rewrite < plus_minus_m_m.
256 rewrite > sym_plus.rewrite < plus_minus_m_m.
258 apply trans_le ? (m+p).
259 rewrite < sym_plus.apply le_plus_n.
261 apply le_plus_to_minus_r.rewrite > sym_plus.assumption.
262 rewrite > eq_minus_n_m_O n (m+p).
263 rewrite > eq_minus_n_m_O (n-m) p.
265 apply le_plus_to_minus.apply lt_to_le. rewrite < sym_plus.
266 apply not_le_to_lt. assumption.
267 apply lt_to_le.apply not_le_to_lt.assumption.
268 apply decidable_le (m+p) n.
271 theorem eq_plus_minus_minus_minus: \forall n,m,p:nat. p \le m \to m \le n \to
276 rewrite < assoc_plus.
277 rewrite < plus_minus_m_m.
279 rewrite < plus_minus_m_m.reflexivity.
280 assumption.assumption.