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