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