]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/nat/minus.ma
10d218d440d7194f2d10e127fddcc3f9eadff05e
[helm.git] / helm / software / matita / library / nat / minus.ma
1 (**************************************************************************)
2 (*       ___                                                                *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15
16 include "nat/le_arith.ma".
17 include "nat/compare.ma".
18
19 let rec minus n m \def 
20  match n with 
21  [ O \Rightarrow O
22  | (S p) \Rightarrow 
23         match m with
24         [O \Rightarrow (S p)
25         | (S q) \Rightarrow minus p q ]].
26
27 (*CSC: the URI must disappear: there is a bug now *)
28 interpretation "natural minus" 'minus x y = (cic:/matita/nat/minus/minus.con x y).
29
30 theorem minus_n_O: \forall n:nat.n=n-O.
31 intros.elim n.simplify.reflexivity.
32 simplify.reflexivity.
33 qed.
34
35 theorem minus_n_n: \forall n:nat.O=n-n.
36 intros.elim n.simplify.
37 reflexivity.
38 simplify.apply H.
39 qed.
40
41 theorem minus_Sn_n: \forall n:nat. S O = (S n)-n.
42 intro.elim n.
43 simplify.reflexivity.
44 elim H.reflexivity.
45 qed.
46
47 theorem minus_Sn_m: \forall n,m:nat. m \leq n \to (S n)-m = S (n-m).
48 intros 2.
49 apply (nat_elim2
50 (\lambda n,m.m \leq n \to (S n)-m = S (n-m))).
51 intros.apply (le_n_O_elim n1 H).
52 simplify.reflexivity.
53 intros.simplify.reflexivity.
54 intros.rewrite < H.reflexivity.
55 apply le_S_S_to_le. assumption.
56 qed.
57
58 theorem eq_minus_S_pred: \forall n,m. n - (S m) = pred(n -m).
59 apply nat_elim2
60   [intro.reflexivity
61   |intro.simplify.autobatch
62   |intros.simplify.assumption
63   ]
64 qed.
65
66 theorem plus_minus:
67 \forall n,m,p:nat. m \leq n \to (n-m)+p = (n+p)-m.
68 intros 2.
69 apply (nat_elim2
70 (\lambda n,m.\forall p:nat.m \leq n \to (n-m)+p = (n+p)-m)).
71 intros.apply (le_n_O_elim ? H).
72 simplify.rewrite < minus_n_O.reflexivity.
73 intros.simplify.reflexivity.
74 intros.simplify.apply H.apply le_S_S_to_le.assumption.
75 qed.
76
77 theorem minus_plus_m_m: \forall n,m:nat.n = (n+m)-m.
78 intros 2.
79 elim m in n ⊢ %.
80 rewrite < minus_n_O.apply plus_n_O.
81 elim n1.simplify.
82 apply minus_n_n.
83 rewrite < plus_n_Sm.
84 change with (S n2 = (S n2 + n)-n).
85 apply H.
86 qed.
87
88 theorem plus_minus_m_m: \forall n,m:nat.
89 m \leq n \to n = (n-m)+m.
90 intros 2.
91 apply (nat_elim2 (\lambda n,m.m \leq n \to n = (n-m)+m)).
92 intros.apply (le_n_O_elim n1 H).
93 reflexivity.
94 intros.simplify.rewrite < plus_n_O.reflexivity.
95 intros.simplify.rewrite < sym_plus.simplify.
96 apply eq_f.rewrite < sym_plus.apply H.
97 apply le_S_S_to_le.assumption.
98 qed.
99
100 theorem minus_to_plus :\forall n,m,p:nat.m \leq n \to n-m = p \to 
101 n = m+p.
102 intros.apply (trans_eq ? ? ((n-m)+m)).
103 apply plus_minus_m_m.
104 apply H.elim H1.
105 apply sym_plus.
106 qed.
107
108 theorem plus_to_minus :\forall n,m,p:nat.
109 n = m+p \to n-m = p.
110 intros.
111 apply (inj_plus_r m).
112 rewrite < H.
113 rewrite < sym_plus.
114 symmetry.
115 apply plus_minus_m_m.rewrite > H.
116 rewrite > sym_plus.
117 apply le_plus_n.
118 qed.
119
120 theorem minus_S_S : \forall n,m:nat.
121 eq nat (minus (S n) (S m)) (minus n m).
122 intros.
123 reflexivity.
124 qed.
125
126 theorem minus_pred_pred : \forall n,m:nat. lt O n \to lt O m \to 
127 eq nat (minus (pred n) (pred m)) (minus n m).
128 intros.
129 apply (lt_O_n_elim n H).intro.
130 apply (lt_O_n_elim m H1).intro.
131 simplify.reflexivity.
132 qed.
133
134 theorem eq_minus_n_m_O: \forall n,m:nat.
135 n \leq m \to n-m = O.
136 intros 2.
137 apply (nat_elim2 (\lambda n,m.n \leq m \to n-m = O)).
138 intros.simplify.reflexivity.
139 intros.apply False_ind.
140 apply not_le_Sn_O;
141 [2: apply H | skip].
142 intros.
143 simplify.apply H.apply le_S_S_to_le. apply H1.
144 qed.
145
146 theorem le_SO_minus: \forall n,m:nat.S n \leq m \to S O \leq m-n.
147 intros.elim H.elim (minus_Sn_n n).apply le_n.
148 rewrite > minus_Sn_m.
149 apply le_S.assumption.
150 apply lt_to_le.assumption.
151 qed.
152
153 theorem minus_le_S_minus_S: \forall n,m:nat. m-n \leq S (m-(S n)).
154 intros.apply (nat_elim2 (\lambda n,m.m-n \leq S (m-(S n)))).
155 intro.elim n1.simplify.apply le_n_Sn.
156 simplify.rewrite < minus_n_O.apply le_n.
157 intros.simplify.apply le_n_Sn.
158 intros.simplify.apply H.
159 qed.
160
161 theorem lt_minus_S_n_to_le_minus_n : \forall n,m,p:nat. m-(S n) < p \to m-n \leq p. 
162 intros 3.simplify.intro.
163 apply (trans_le (m-n) (S (m-(S n))) p).
164 apply minus_le_S_minus_S.
165 assumption.
166 qed.
167
168 theorem le_minus_m: \forall n,m:nat. n-m \leq n.
169 intros.apply (nat_elim2 (\lambda m,n. n-m \leq n)).
170 intros.rewrite < minus_n_O.apply le_n.
171 intros.simplify.apply le_n.
172 intros.simplify.apply le_S.assumption.
173 qed.
174
175 theorem lt_minus_m: \forall n,m:nat. O < n \to O < m \to n-m \lt n.
176 intros.apply (lt_O_n_elim n H).intro.
177 apply (lt_O_n_elim m H1).intro.
178 simplify.unfold lt.apply le_S_S.apply le_minus_m.
179 qed.
180
181 theorem minus_le_O_to_le: \forall n,m:nat. n-m \leq O \to n \leq m.
182 intros 2.
183 apply (nat_elim2 (\lambda n,m:nat.n-m \leq O \to n \leq m)).
184 intros.apply le_O_n.
185 simplify.intros. assumption.
186 simplify.intros.apply le_S_S.apply H.assumption.
187 qed.
188
189 (* galois *)
190 theorem monotonic_le_minus_r: 
191 \forall p,q,n:nat. q \leq p \to n-p \le n-q.
192 simplify.intros 2.apply (nat_elim2 
193 (\lambda p,q.\forall a.q \leq p \to a-p \leq a-q)).
194 intros.apply (le_n_O_elim n H).apply le_n.
195 intros.rewrite < minus_n_O.
196 apply le_minus_m.
197 intros.elim a.simplify.apply le_n.
198 simplify.apply H.apply le_S_S_to_le.assumption.
199 qed.
200
201 theorem le_minus_to_plus: \forall n,m,p. (le (n-m) p) \to (le n (p+m)).
202 intros 2.apply (nat_elim2 (\lambda n,m.\forall p.(le (n-m) p) \to (le n (p+m)))).
203 intros.apply le_O_n.
204 simplify.intros.rewrite < plus_n_O.assumption.
205 intros.
206 rewrite < plus_n_Sm.
207 apply le_S_S.apply H.
208 exact H1.
209 qed.
210
211 theorem le_plus_to_minus: \forall n,m,p. (le n (p+m)) \to (le (n-m) p).
212 intros 2.apply (nat_elim2 (\lambda n,m.\forall p.(le n (p+m)) \to (le (n-m) p))).
213 intros.simplify.apply le_O_n.
214 intros 2.rewrite < plus_n_O.intro.simplify.assumption.
215 intros.simplify.apply H.
216 apply le_S_S_to_le.rewrite > plus_n_Sm.assumption.
217 qed.
218
219 (* the converse of le_plus_to_minus does not hold *)
220 theorem le_plus_to_minus_r: \forall n,m,p. (le (n+m) p) \to (le n (p-m)).
221 intros 3.apply (nat_elim2 (\lambda m,p.(le (n+m) p) \to (le n (p-m)))).
222 intro.rewrite < plus_n_O.rewrite < minus_n_O.intro.assumption.
223 intro.intro.cut (n=O).rewrite > Hcut.apply le_O_n.
224 apply sym_eq. apply le_n_O_to_eq.
225 apply (trans_le ? (n+(S n1))).
226 rewrite < sym_plus.
227 apply le_plus_n.assumption.
228 intros.simplify.
229 apply H.apply le_S_S_to_le.
230 rewrite > plus_n_Sm.assumption.
231 qed.
232
233 (* minus and lt - to be completed *)
234 theorem lt_minus_l: \forall m,l,n:nat. 
235   l < m \to m \le n \to n - m < n - l.
236 apply nat_elim2
237   [intros.apply False_ind.apply (not_le_Sn_O ? H)
238   |intros.rewrite < minus_n_O.
239    autobatch
240   |intros.
241    generalize in match H2.
242    apply (nat_case n1)
243     [intros.apply False_ind.apply (not_le_Sn_O ? H3)
244     |intros.simplify.
245      apply H
246       [
247        apply lt_S_S_to_lt.
248        assumption
249       |apply le_S_S_to_le.assumption
250       ]
251     ]
252   ]
253 qed.
254
255 theorem lt_minus_r: \forall n,m,l:nat. 
256   n \le l \to l < m \to l -n < m -n.
257 intro.elim n
258   [applyS H1
259   |rewrite > eq_minus_S_pred.
260    rewrite > eq_minus_S_pred.
261    apply lt_pred
262     [unfold lt.apply le_plus_to_minus_r.applyS H1
263     |apply H[autobatch|assumption]
264     ]
265   ]
266 qed.
267
268 lemma lt_to_lt_O_minus : \forall m,n.
269   n < m \to O < m - n.
270 intros.  
271 unfold. apply le_plus_to_minus_r. unfold in H. rewrite > sym_plus. 
272 rewrite < plus_n_Sm. 
273 rewrite < plus_n_O. 
274 assumption.
275 qed.  
276
277 theorem lt_minus_to_plus: \forall n,m,p. (lt n (p-m)) \to (lt (n+m) p).
278 intros 3.apply (nat_elim2 (\lambda m,p.(lt n (p-m)) \to (lt (n+m) p))).
279 intro.rewrite < plus_n_O.rewrite < minus_n_O.intro.assumption.
280 simplify.intros.apply False_ind.apply (not_le_Sn_O n H).
281 simplify.intros.unfold lt.
282 apply le_S_S.
283 rewrite < plus_n_Sm.
284 apply H.apply H1.
285 qed.
286
287 theorem lt_O_minus_to_lt: \forall a,b:nat.
288 O \lt b-a \to a \lt b.
289 intros.
290 rewrite > (plus_n_O a).
291 rewrite > (sym_plus a O).
292 apply (lt_minus_to_plus O  a b).
293 assumption.
294 qed.
295
296 theorem lt_minus_to_lt_plus:
297 \forall n,m,p. n - m < p \to n < m + p.
298 intros 2.
299 apply (nat_elim2 ? ? ? ? n m)
300   [simplify.intros.autobatch.
301   |intros 2.rewrite < minus_n_O.
302    intro.assumption
303   |intros.
304    simplify.
305    cut (n1 < m1+p)
306     [autobatch
307     |apply H.
308      apply H1
309     ]
310   ]
311 qed.
312
313 theorem lt_plus_to_lt_minus:
314 \forall n,m,p. m \le n \to n < m + p \to n - m < p.
315 intros 2.
316 apply (nat_elim2 ? ? ? ? n m)
317   [simplify.intros 3.
318    apply (le_n_O_elim ? H).
319    simplify.intros.assumption
320   |simplify.intros.assumption.
321   |intros.
322    simplify.
323    apply H
324     [apply le_S_S_to_le.assumption
325     |apply le_S_S_to_le.apply H2
326     ]
327   ]
328 qed. 
329
330 theorem minus_m_minus_mn: \forall n,m. n\le m \to n=m-(m-n).
331 intros.
332 apply sym_eq.
333 apply plus_to_minus.
334 autobatch.
335 qed.
336
337 theorem distributive_times_minus: distributive nat times minus.
338 unfold distributive.
339 intros.
340 apply ((leb_elim z y)).
341   intro.cut (x*(y-z)+x*z = (x*y-x*z)+x*z).
342     apply (inj_plus_l (x*z)).assumption.
343     apply (trans_eq nat ? (x*y)).
344       rewrite < distr_times_plus.rewrite < (plus_minus_m_m ? ? H).reflexivity.
345       rewrite < plus_minus_m_m.
346         reflexivity.
347         apply le_times_r.assumption.
348   intro.rewrite > eq_minus_n_m_O.
349     rewrite > (eq_minus_n_m_O (x*y)).
350       rewrite < sym_times.simplify.reflexivity.
351         apply le_times_r.apply lt_to_le.apply not_le_to_lt.assumption.
352         apply lt_to_le.apply not_le_to_lt.assumption.
353 qed.
354
355 theorem distr_times_minus: \forall n,m,p:nat. n*(m-p) = n*m-n*p
356 \def distributive_times_minus.
357
358 theorem eq_minus_plus_plus_minus: \forall n,m,p:nat. p \le m \to (n+m)-p = n+(m-p).
359 intros.
360 apply plus_to_minus.
361 rewrite > sym_plus in \vdash (? ? ? %).
362 rewrite > assoc_plus.
363 rewrite < plus_minus_m_m.
364 reflexivity.assumption.
365 qed.
366
367 theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p).
368 intros.
369 cut (m+p \le n \or m+p \nleq n).
370   elim Hcut.
371     symmetry.apply plus_to_minus.
372     rewrite > assoc_plus.rewrite > (sym_plus p).rewrite < plus_minus_m_m.
373       rewrite > sym_plus.rewrite < plus_minus_m_m.
374         reflexivity.
375         apply (trans_le ? (m+p)).
376           rewrite < sym_plus.apply le_plus_n.
377           assumption.
378       apply le_plus_to_minus_r.rewrite > sym_plus.assumption.   
379     rewrite > (eq_minus_n_m_O n (m+p)).
380       rewrite > (eq_minus_n_m_O (n-m) p).
381         reflexivity.
382       apply le_plus_to_minus.apply lt_to_le. rewrite < sym_plus.
383        apply not_le_to_lt. assumption.
384     apply lt_to_le.apply not_le_to_lt.assumption.          
385   apply (decidable_le (m+p) n).
386 qed.
387
388 theorem eq_plus_minus_minus_minus: \forall n,m,p:nat. p \le m \to m \le n \to
389 p+(n-m) = n-(m-p).
390 intros.
391 apply sym_eq.
392 apply plus_to_minus.
393 rewrite < assoc_plus.
394 rewrite < plus_minus_m_m.
395 rewrite < sym_plus.
396 rewrite < plus_minus_m_m.reflexivity.
397 assumption.assumption.
398 qed.