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