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