]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/library_auto/auto/nat/minus.ma
Stuff moved from old Matita.
[helm.git] / matita / matita / contribs / library_auto / auto / 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/library_autobatch/nat/minus".
17
18 include "auto/nat/le_arith.ma".
19 include "auto/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 interpretation "natural minus" 'minus x y = (minus x y).
30
31 theorem minus_n_O: \forall n:nat.n=n-O.
32 intros.
33 elim n;
34 autobatch. (* applico autobatch su entrambi i goal aperti*)
35 (*simplify;reflexivity.*)
36 qed.
37
38 theorem minus_n_n: \forall n:nat.O=n-n.
39 intros.
40 elim n;simplify
41 [ reflexivity
42 | apply H
43 ]
44 qed.
45
46 theorem minus_Sn_n: \forall n:nat. S O = (S n)-n.
47 intro.
48 elim n
49 [ autobatch
50   (*simplify.reflexivity.*)
51 | elim H.
52   reflexivity
53 ]
54 qed.
55
56
57 theorem minus_Sn_m: \forall n,m:nat. m \leq n \to (S n)-m = S (n-m).
58 intros 2.
59 apply (nat_elim2
60 (\lambda n,m.m \leq n \to (S n)-m = S (n-m)));intros
61 [ apply (le_n_O_elim n1 H).
62   autobatch
63   (*simplify.
64   reflexivity.*)
65 | autobatch
66   (*simplify.
67   reflexivity.*)
68 | rewrite < H
69   [ reflexivity
70   | autobatch
71     (*apply le_S_S_to_le. 
72     assumption.*)
73   ]
74 ]
75 qed.
76
77 theorem plus_minus:
78 \forall n,m,p:nat. m \leq n \to (n-m)+p = (n+p)-m.
79 intros 2.
80 apply (nat_elim2
81 (\lambda n,m.\forall p:nat.m \leq n \to (n-m)+p = (n+p)-m));intros
82 [ apply (le_n_O_elim ? H).
83   autobatch
84   (*simplify.
85   rewrite < minus_n_O.
86   reflexivity.*)
87 | autobatch
88   (*simplify.
89   reflexivity.*)
90 | simplify.
91   autobatch
92   (*apply H.
93   apply le_S_S_to_le.
94   assumption.*)
95 ]
96 qed.
97
98 theorem minus_plus_m_m: \forall n,m:nat.n = (n+m)-m.
99 intros 2.
100 generalize in match n.
101 elim m
102 [ rewrite < minus_n_O.
103   apply plus_n_O.
104 | elim n2
105   [ autobatch
106     (*simplify.
107     apply minus_n_n.*)
108   | rewrite < plus_n_Sm.
109     change with (S n3 = (S n3 + n1)-n1).
110     apply H
111   ]
112 ]
113 qed.
114
115 theorem plus_minus_m_m: \forall n,m:nat.
116 m \leq n \to n = (n-m)+m.
117 intros 2.
118 apply (nat_elim2 (\lambda n,m.m \leq n \to n = (n-m)+m));intros
119 [ apply (le_n_O_elim n1 H).
120   reflexivity
121 | autobatch
122   (*simplify.
123   rewrite < plus_n_O.
124   reflexivity.*)
125 | simplify.
126   rewrite < sym_plus.
127   simplify.
128   apply eq_f.
129   rewrite < sym_plus.
130   autobatch
131   (*apply H.
132   apply le_S_S_to_le.
133   assumption.*)
134 ]
135 qed.
136
137 theorem minus_to_plus :\forall n,m,p:nat.m \leq n \to n-m = p \to 
138 n = m+p.
139 intros.apply (trans_eq ? ? ((n-m)+m));autobatch.
140 (*[ apply plus_minus_m_m.
141   apply H.
142 | elim H1.
143   apply sym_plus.
144 ]*)
145 qed.
146
147 theorem plus_to_minus :\forall n,m,p:nat.
148 n = m+p \to n-m = p.
149 intros.
150 apply (inj_plus_r m).
151 rewrite < H.
152 rewrite < sym_plus.
153 symmetry.
154 autobatch.
155 (*apply plus_minus_m_m.
156 rewrite > H.
157 rewrite > sym_plus.
158 apply le_plus_n.*)
159 qed.
160
161 theorem minus_S_S : \forall n,m:nat.
162 eq nat (minus (S n) (S m)) (minus n m).
163 intros.
164 reflexivity.
165 qed.
166
167 theorem minus_pred_pred : \forall n,m:nat. lt O n \to lt O m \to 
168 eq nat (minus (pred n) (pred m)) (minus n m).
169 intros.
170 apply (lt_O_n_elim n H).
171 intro.
172 apply (lt_O_n_elim m H1).
173 intro.
174 autobatch.
175 (*simplify.reflexivity.*)
176 qed.
177
178 theorem eq_minus_n_m_O: \forall n,m:nat.
179 n \leq m \to n-m = O.
180 intros 2.
181 apply (nat_elim2 (\lambda n,m.n \leq m \to n-m = O));intros
182 [ autobatch
183   (*simplify.
184   reflexivity.*)
185 | apply False_ind.
186   autobatch
187   (*apply not_le_Sn_O.
188   goal 15.*) (*prima goal 13*) 
189 (* effettuando un'esecuzione passo-passo, quando si arriva a dover 
190    considerare questa tattica, la finestra di dimostrazione scompare
191    e viene generato il seguente errore:
192    Uncaught exception: File "matitaMathView.ml", line 677, characters
193    6-12: Assertion failed.
194    
195    tuttavia l'esecuzione continua, ed il teorema viene comunque 
196    dimostrato.
197  *)
198   (*apply H.*)
199 | simplify.
200   autobatch
201   (*apply H.
202   apply le_S_S_to_le. 
203   apply H1.*)
204 ]
205 qed.
206
207 theorem le_SO_minus: \forall n,m:nat.S n \leq m \to S O \leq m-n.
208 intros.
209 elim H
210 [ elim (minus_Sn_n n).apply le_n
211 | rewrite > minus_Sn_m;autobatch
212   (*apply le_S.assumption.
213   apply lt_to_le.assumption.*)
214 ]
215 qed.
216
217 theorem minus_le_S_minus_S: \forall n,m:nat. m-n \leq S (m-(S n)).
218 intros.apply (nat_elim2 (\lambda n,m.m-n \leq S (m-(S n))));intros
219 [ elim n1;simplify
220   [ apply le_n_Sn.
221   | rewrite < minus_n_O.
222     apply le_n.
223   ]
224 | autobatch 
225   (*simplify.apply le_n_Sn.*)
226 | simplify.apply H.
227 ]
228 qed.
229
230 theorem lt_minus_S_n_to_le_minus_n : \forall n,m,p:nat. m-(S n) < p \to m-n \leq p. 
231 intros 3.
232 autobatch.
233 (*simplify.
234 intro.
235 apply (trans_le (m-n) (S (m-(S n))) p).
236 apply minus_le_S_minus_S.
237 assumption.*)
238 qed.
239
240 theorem le_minus_m: \forall n,m:nat. n-m \leq n.
241 intros.apply (nat_elim2 (\lambda m,n. n-m \leq n));intros
242 [ autobatch
243   (*rewrite < minus_n_O.
244   apply le_n.*)
245 | autobatch
246   (*simplify.
247   apply le_n.*)
248 | simplify.
249   autobatch
250   (*apply le_S.
251   assumption.*)
252 ]
253 qed.
254
255 theorem lt_minus_m: \forall n,m:nat. O < n \to O < m \to n-m \lt n.
256 intros.
257 apply (lt_O_n_elim n H).
258 intro.
259 apply (lt_O_n_elim m H1).
260 intro.
261 simplify.
262 autobatch.
263 (*unfold lt.
264 apply le_S_S.
265 apply le_minus_m.*)
266 qed.
267
268 theorem minus_le_O_to_le: \forall n,m:nat. n-m \leq O \to n \leq m.
269 intros 2.
270 apply (nat_elim2 (\lambda n,m:nat.n-m \leq O \to n \leq m))
271 [ intros.
272   apply le_O_n
273 | simplify.
274   intros. 
275   assumption
276 | simplify.
277   intros.
278   autobatch
279   (*apply le_S_S.
280   apply H.
281   assumption.*)
282 ]
283 qed.
284
285 (* galois *)
286 theorem monotonic_le_minus_r: 
287 \forall p,q,n:nat. q \leq p \to n-p \le n-q.
288 (*simplify*).
289 intros 2.
290 apply (nat_elim2 
291 (\lambda p,q.\forall a.q \leq p \to a-p \leq a-q));intros
292 [ apply (le_n_O_elim n H).
293   apply le_n.
294 | rewrite < minus_n_O.
295   apply le_minus_m.
296 | elim a
297   [ autobatch
298     (*simplify.
299     apply le_n.*)
300   | simplify.
301     autobatch
302     (*apply H.
303     apply le_S_S_to_le.
304     assumption.*)
305   ]
306 ]
307 qed.
308
309 theorem le_minus_to_plus: \forall n,m,p. (le (n-m) p) \to (le n (p+m)).
310 intros 2.
311 apply (nat_elim2 (\lambda n,m.\forall p.(le (n-m) p) \to (le n (p+m))));intros
312 [ apply le_O_n.
313 | rewrite < plus_n_O.
314   assumption.
315 | rewrite < plus_n_Sm.
316   apply le_S_S.
317   apply H.
318   exact H1.
319 ]
320 qed.
321
322 theorem le_plus_to_minus: \forall n,m,p. (le n (p+m)) \to (le (n-m) p).
323 intros 2.
324 apply (nat_elim2 (\lambda n,m.\forall p.(le n (p+m)) \to (le (n-m) p)))
325 [ intros.
326   autobatch
327   (*simplify.
328   apply le_O_n.*)
329 | intros 2.
330   rewrite < plus_n_O.
331   autobatch
332   (*intro.
333   simplify.
334   assumption.*)
335 | intros.
336   simplify.
337   apply H.
338   apply le_S_S_to_le.
339   rewrite > plus_n_Sm.
340   assumption
341 ]
342 qed.
343
344 (* the converse of le_plus_to_minus does not hold *)
345 theorem le_plus_to_minus_r: \forall n,m,p. (le (n+m) p) \to (le n (p-m)).
346 intros 3.
347 apply (nat_elim2 (\lambda m,p.(le (n+m) p) \to (le n (p-m))));intro
348 [ rewrite < plus_n_O.
349   rewrite < minus_n_O.
350   autobatch
351   (*intro.
352   assumption.*)
353 | intro.
354   cut (n=O)
355   [ autobatch
356     (*rewrite > Hcut.
357     apply le_O_n.*)
358   | apply sym_eq. 
359     apply le_n_O_to_eq.
360     autobatch
361     (*apply (trans_le ? (n+(S n1)))
362     [ rewrite < sym_plus.
363       apply le_plus_n
364     | assumption
365     ]*)
366   ]
367 | intros.
368   simplify.
369   apply H.
370   apply le_S_S_to_le.
371   rewrite > plus_n_Sm.
372   assumption
373 ]
374 qed.
375
376 (* minus and lt - to be completed *)
377 theorem lt_minus_to_plus: \forall n,m,p. (lt n (p-m)) \to (lt (n+m) p).
378 intros 3.
379 apply (nat_elim2 (\lambda m,p.(lt n (p-m)) \to (lt (n+m) p)))
380 [ intro.
381   rewrite < plus_n_O.
382   rewrite < minus_n_O.
383   autobatch
384   (*intro.
385   assumption.*)
386 | simplify.
387   intros.
388   apply False_ind.
389   apply (not_le_Sn_O n H)
390 | (*simplify.*)
391   intros.
392   unfold lt.
393   apply le_S_S.
394   rewrite < plus_n_Sm.
395   autobatch
396   (*apply H.
397   apply H1.*)
398 ]
399 qed.
400
401 theorem distributive_times_minus: distributive nat times minus.
402 unfold distributive.
403 intros.
404 apply ((leb_elim z y));intro
405 [ cut (x*(y-z)+x*z = (x*y-x*z)+x*z)
406     [ autobatch
407       (*apply (inj_plus_l (x*z)).
408       assumption.*)
409     | apply (trans_eq nat ? (x*y))
410       [ rewrite < distr_times_plus.
411         autobatch
412         (*rewrite < (plus_minus_m_m ? ? H).
413         reflexivity.*)
414       | rewrite < plus_minus_m_m;autobatch
415         (*[ reflexivity.
416         | apply le_times_r.
417           assumption.
418         ]*)
419       ]
420     ]
421 | rewrite > eq_minus_n_m_O
422   [ rewrite > (eq_minus_n_m_O (x*y))
423     [ autobatch
424       (*rewrite < sym_times.
425       simplify.
426       reflexivity.*)
427     | apply le_times_r.
428       apply lt_to_le.
429       autobatch
430       (*apply not_le_to_lt.
431       assumption.*)
432     ]
433   | autobatch
434     (*apply lt_to_le.
435     apply not_le_to_lt.
436     assumption.*)
437   ]
438 ]
439 qed.
440
441 theorem distr_times_minus: \forall n,m,p:nat. n*(m-p) = n*m-n*p
442 \def distributive_times_minus.
443
444 theorem eq_minus_plus_plus_minus: \forall n,m,p:nat. p \le m \to (n+m)-p = n+(m-p).
445 intros.
446 apply plus_to_minus.
447 rewrite > sym_plus in \vdash (? ? ? %).
448 rewrite > assoc_plus.
449 autobatch.
450 (*rewrite < plus_minus_m_m.
451 reflexivity.
452 assumption.
453 *)
454 qed.
455
456 theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p).
457 intros.
458 cut (m+p \le n \or m+p \nleq n)
459 [ elim Hcut
460   [ symmetry.
461     apply plus_to_minus.
462     rewrite > assoc_plus.
463     rewrite > (sym_plus p).
464     rewrite < plus_minus_m_m
465     [ rewrite > sym_plus.
466       rewrite < plus_minus_m_m ; autobatch
467       (*[ reflexivity.
468       | apply (trans_le ? (m+p))
469         [ rewrite < sym_plus.
470           apply le_plus_n
471         | assumption
472         ]
473       ]*)
474     | apply le_plus_to_minus_r.
475       rewrite > sym_plus.
476       assumption.  
477     ] 
478   | rewrite > (eq_minus_n_m_O n (m+p))
479     [ rewrite > (eq_minus_n_m_O (n-m) p)
480       [ reflexivity
481       | apply le_plus_to_minus.
482         apply lt_to_le.
483         rewrite < sym_plus.
484         autobatch
485         (*apply not_le_to_lt. 
486         assumption.*)
487       ]
488     | autobatch
489       (*apply lt_to_le.
490       apply not_le_to_lt.
491       assumption.*)          
492     ]
493   ]
494 | apply (decidable_le (m+p) n)
495 ]
496 qed.
497
498 theorem eq_plus_minus_minus_minus: \forall n,m,p:nat. p \le m \to m \le n \to
499 p+(n-m) = n-(m-p).
500 intros.
501 apply sym_eq.
502 apply plus_to_minus.
503 rewrite < assoc_plus.
504 rewrite < plus_minus_m_m;
505 [ rewrite < sym_plus.
506   autobatch
507   (*rewrite < plus_minus_m_m
508   [ reflexivity
509   | assumption
510   ]*)
511 | assumption
512 ]
513 qed.