]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/nat/div_and_mod_diseq.ma
fixed some notational collisions
[helm.git] / helm / software / matita / library / nat / div_and_mod_diseq.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 (*       \ /        Matita is distributed under the terms of the          *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "nat/lt_arith.ma".
16
17 (* the proof that 
18      n \mod m < m, 
19    called lt_mod_m_m, is in div_and_mod.
20 Other inequalities are also in lt_arith.ma.  
21 *)
22
23 theorem lt_div_S: \forall n,m. O < m \to 
24 n < S(n / m)*m.
25 intros.
26 change with (n < m +(n/m)*m).
27 rewrite > sym_plus.
28 rewrite > (div_mod n m H) in ⊢ (? % ?).
29 apply lt_plus_r.
30 apply lt_mod_m_m.
31 assumption.
32 qed.
33
34 theorem le_div: \forall n,m. O < n \to m/n \le m.
35 intros.
36 rewrite > (div_mod m n) in \vdash (? ? %)
37   [apply (trans_le ? (m/n*n))
38     [rewrite > times_n_SO in \vdash (? % ?).
39      apply le_times
40       [apply le_n|assumption]
41     |apply le_plus_n_r
42     ]
43   |assumption
44   ]
45 qed.
46
47 theorem le_plus_mod: \forall m,n,q. O < q \to
48 (m+n) \mod q \le m \mod q + n \mod q .
49 intros.
50 elim (decidable_le q (m \mod q + n \mod q))
51   [apply not_lt_to_le.intro.
52    apply (le_to_not_lt q q)
53     [apply le_n
54     |apply (le_to_lt_to_lt ? (m\mod q+n\mod q))
55       [assumption
56       |apply (trans_lt ? ((m+n)\mod q))
57         [assumption
58         |apply lt_mod_m_m.assumption
59         ]
60       ]
61     ]
62   |cut ((m+n)\mod q = m\mod q+n\mod q)
63     [rewrite < Hcut.apply le_n
64     |apply (div_mod_spec_to_eq2 (m+n) q ((m+n)/q) ((m+n) \mod q) (m/q + n/q))
65       [apply div_mod_spec_div_mod.
66        assumption
67       |apply div_mod_spec_intro
68         [apply not_le_to_lt.assumption
69         |rewrite > (div_mod n q H) in ⊢ (? ? (? ? %) ?).
70          rewrite < assoc_plus.
71          rewrite < assoc_plus in ⊢ (? ? ? %).
72          apply eq_f2
73           [rewrite > (div_mod m q) in ⊢ (? ? (? % ?) ?)
74             [rewrite > sym_times in ⊢ (? ? ? (? % ?)).
75              rewrite > distr_times_plus.
76              rewrite > sym_times in ⊢ (? ? ? (? (? % ?) ?)).
77              rewrite > assoc_plus.
78              rewrite > assoc_plus in ⊢ (? ? ? %).
79              apply eq_f.
80              rewrite > sym_plus.
81              rewrite > sym_times.
82              reflexivity
83             |assumption
84             ]
85           |reflexivity
86           ]
87         ]
88       ]
89     ]
90   ]
91 qed.
92
93 theorem le_plus_div: \forall m,n,q. O < q \to
94 m/q + n/q \le (m+n)/q.
95 intros.
96 apply (le_times_to_le q)
97   [assumption
98   |rewrite > distr_times_plus.
99    rewrite > sym_times.
100    rewrite > sym_times in ⊢ (? (? ? %) ?).
101    rewrite > sym_times in ⊢ (? ? %).
102    apply (le_plus_to_le ((m+n) \mod q)).
103    rewrite > sym_plus in ⊢ (? ? %).
104    rewrite < (div_mod ? ? H).
105    rewrite > (div_mod n q H) in ⊢ (? ? (? ? %)).
106    rewrite < assoc_plus.
107    rewrite > sym_plus in ⊢ (? ? (? ? %)).
108    rewrite < assoc_plus in ⊢ (? ? %).
109    apply le_plus_l.
110    rewrite > (div_mod m q H) in ⊢ (? ? (? % ?)).
111    rewrite > assoc_plus.
112    rewrite > sym_plus.
113    apply le_plus_r.
114    apply le_plus_mod.
115    assumption
116   ]
117 qed.
118
119 theorem le_times_to_le_div: \forall a,b,c:nat.
120 O \lt b \to (b*c) \le a \to c \le (a /b).
121 intros.
122 apply lt_S_to_le.
123 apply (lt_times_n_to_lt b)
124   [assumption
125   |rewrite > sym_times.
126    apply (le_to_lt_to_lt ? a)
127     [assumption
128     |simplify.
129      rewrite > sym_plus.
130      rewrite > (div_mod a b) in ⊢ (? % ?)
131       [apply lt_plus_r.
132        apply lt_mod_m_m.
133        assumption
134       |assumption
135       ]
136     ]
137   ]
138 qed.
139
140 theorem le_times_to_le_div2: \forall m,n,q. O < q \to 
141 n \le m*q \to n/q \le m.
142 intros.
143 apply (le_times_to_le q ? ? H).
144 rewrite > sym_times.
145 rewrite > sym_times in ⊢ (? ? %).
146 apply (le_plus_to_le (n \mod q)).
147 rewrite > sym_plus.
148 rewrite < div_mod
149   [apply (trans_le ? (m*q))
150     [assumption
151     |apply le_plus_n
152     ]
153   |assumption
154   ]
155 qed.
156
157 (* da spostare *)
158 theorem lt_m_nm: \forall n,m. O < m \to S O < n \to 
159 m < n*m.
160 intros.
161 elim H1
162   [simplify.rewrite < plus_n_O.
163    rewrite > plus_n_O in ⊢ (? % ?).
164    apply lt_plus_r.assumption
165   |simplify.
166    rewrite > plus_n_O in ⊢ (? % ?).
167    rewrite > sym_plus.
168    apply lt_plus
169     [assumption
170     |assumption
171     ]
172   ]
173 qed.
174
175 theorem lt_times_to_lt: \forall i,n,m. O < i \to
176 i * n < i * m \to n < m.
177 intros.
178 apply not_le_to_lt.intro.
179 apply (lt_to_not_le ? ? H1).
180 apply le_times_r.
181 assumption.
182 qed.
183    
184 theorem lt_times_to_lt_div: \forall m,n,q. n < m*q \to n/q < m.
185 intros.
186 apply (lt_times_to_lt q ? ? (lt_times_to_lt_O ? ? ? H)).
187 rewrite > sym_times.
188 rewrite > sym_times in ⊢ (? ? %).
189 apply (le_plus_to_le (n \mod q)).
190 rewrite < plus_n_Sm. 
191 rewrite > sym_plus.
192 rewrite < div_mod
193   [apply (trans_le ? (m*q))
194     [assumption
195     |apply le_plus_n
196     ]
197   |apply (lt_times_to_lt_O ? ? ? H)
198   ]
199 qed.
200
201 theorem lt_div: \forall n,m. O < m \to S O < n \to m/n < m.
202 intros.
203 apply lt_times_to_lt_div.
204 rewrite < sym_times.
205 apply lt_m_nm;assumption.
206 qed. 
207   
208 theorem le_div_plus_S: \forall m,n,q. O < q \to
209 (m+n)/q \le S(m/q + n/q).
210 intros.
211 apply le_S_S_to_le.
212 apply lt_times_to_lt_div.
213 change in ⊢ (? ? %) with (q + (q + (m/q+n/q)*q)).
214 rewrite > sym_times.
215 rewrite > distr_times_plus.
216 rewrite > sym_times.
217 rewrite < assoc_plus in ⊢ (? ? (? ? %)).
218 rewrite < assoc_plus.
219 rewrite > sym_plus in ⊢ (? ? (? % ?)).
220 rewrite > assoc_plus.
221 apply lt_plus
222   [change with (m < S(m/q)*q).
223    apply lt_div_S.
224    assumption
225   |rewrite > sym_times.
226    change with (n < S(n/q)*q).
227    apply lt_div_S.
228    assumption
229   ]
230 qed.
231
232 theorem le_div_S_S_div: \forall n,m. O < m \to
233 (S n)/m \le S (n /m).
234 intros.
235 apply le_times_to_le_div2
236   [assumption
237   |simplify.
238    rewrite > (div_mod n m H) in ⊢ (? (? %) ?).
239    rewrite > plus_n_Sm.
240    rewrite > sym_plus.
241    apply le_plus_l.
242    apply lt_mod_m_m.
243    assumption.
244   ]
245 qed.
246
247 theorem le_times_div_div_times: \forall a,n,m.O < m \to 
248 a*(n/m) \le a*n/m. 
249 intros.
250 apply le_times_to_le_div
251   [assumption
252   |rewrite > sym_times.
253    rewrite > assoc_times.
254    apply le_times_r.
255    rewrite > (div_mod n m H) in ⊢ (? ? %).
256    apply le_plus_n_r.
257   ]
258 qed.
259
260 theorem monotonic_div: \forall n.O < n \to
261 monotonic nat le (\lambda m.div m n).
262 unfold monotonic.simplify.intros.
263 apply le_times_to_le_div
264   [assumption
265   |apply (trans_le ? x)
266     [rewrite > sym_times.
267      rewrite > (div_mod x n H) in ⊢ (? ? %).
268      apply le_plus_n_r
269     |assumption
270     ]
271   ]
272 qed.
273  
274 theorem le_div_times_m: \forall a,i,m. O < i \to O < m \to
275 (a * (m / i)) / m \le a / i.
276 intros.
277 apply (trans_le ? ((a*m/i)/m))
278   [apply monotonic_div
279     [assumption
280     |apply le_times_div_div_times.
281      assumption
282     ]
283   |rewrite > eq_div_div_div_times
284     [rewrite > sym_times in ⊢ (? (? ? %) ?).
285      rewrite < eq_div_div_div_times
286       [apply monotonic_div
287         [assumption
288         |rewrite > lt_O_to_div_times
289           [apply le_n
290           |assumption
291           ]
292         ]
293       |assumption
294       |assumption
295       ]
296     |assumption
297     |assumption
298     ]
299   ]
300 qed.
301        
302 theorem le_div_times_Sm: \forall a,i,m. O < i \to O < m \to
303 a / i \le (a * S (m / i))/m.
304 intros.
305 apply (trans_le ? ((a * S (m / i))/((S (m/i))*i)))
306   [rewrite < (eq_div_div_div_times ? i)
307     [rewrite > lt_O_to_div_times
308       [apply le_n
309       |apply lt_O_S
310       ]
311     |apply lt_O_S
312     |assumption
313     ]
314   |apply le_times_to_le_div
315     [assumption
316     |apply (trans_le ? (m*(a*S (m/i))/(S (m/i)*i)))
317       [apply le_times_div_div_times.
318        rewrite > (times_n_O O).
319        apply lt_times
320         [apply lt_O_S
321         |assumption
322         ]
323       |rewrite > sym_times.
324        apply le_times_to_le_div2
325         [rewrite > (times_n_O O).
326          apply lt_times
327           [apply lt_O_S
328           |assumption
329           ]
330         |apply le_times_r.
331          apply lt_to_le.
332          apply lt_div_S.
333          assumption
334         ]
335       ]
336     ]
337   ]
338 qed.
339