]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/nat/o.ma
...
[helm.git] / helm / software / matita / library / nat / o.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/binomial.ma".
16 include "nat/sqrt.ma".
17
18 theorem le_times_SSO_n_exp_SSO_n: \forall n. 
19 2*n \le exp 2 n.
20 intro.cases n
21   [apply le_O_n
22   |elim n1
23     [apply le_n
24     |rewrite > times_SSO.
25      change in ⊢ (? % ?) with (2 + (2*(S n2))).
26      change in ⊢ (? ? %) with (exp 2 (S n2)+(exp 2 (S n2) + O)).
27      rewrite < plus_n_O.
28      apply le_plus
29       [rewrite > exp_n_SO in ⊢ (? % ?).
30        apply le_exp
31         [apply lt_O_S
32         |apply le_S_S.apply le_O_n
33         ]
34       |assumption
35       ]
36     ]
37   ]
38 qed.
39
40 theorem le_times_n_exp: \forall a,n. exp 2 a \le n \to 
41 exp 2 a*n \le exp 2 n.
42 intros.elim H
43   [rewrite < exp_plus_times.
44    apply le_exp
45     [apply lt_O_S
46     |rewrite > plus_n_O in ⊢ (? (? ? %) ?).
47      change in ⊢ (? % ?) with (2*a).
48      apply le_times_SSO_n_exp_SSO_n
49     ]
50   |rewrite > sym_times.simplify.
51    rewrite < plus_n_O.
52    apply le_plus
53     [apply (trans_le ? n1)
54       [assumption
55       |apply (trans_le ? (2*n1))
56         [apply le_times_n.
57          apply le_n_Sn
58         |apply le_times_SSO_n_exp_SSO_n
59         ]
60       ]
61     |rewrite > sym_times.
62      assumption
63     ]
64   ]
65 qed.     
66
67 theorem lt_times_SSO_n_exp_SSO_n: \forall n. 2 < n \to
68 2*n < exp 2 n.
69 intros.elim H
70   [apply leb_true_to_le.reflexivity.
71   |rewrite > times_SSO.
72    change in ⊢ (? % ?) with (2 + (2*n1)).
73    simplify in ⊢ (? ? %).
74    rewrite < plus_n_O.
75    apply (lt_to_le_to_lt ? (2+(exp 2 n1)))
76     [apply lt_plus_r.assumption
77     |apply le_plus_l.
78      rewrite > exp_n_SO in ⊢ (? % ?).
79      apply le_exp
80       [apply lt_O_S
81       |apply (trans_le ? 3)
82         [apply le_S_S.apply le_O_n
83         |assumption
84         ]
85       ]
86     ]
87   ]
88 qed.
89
90 theorem le_exp_n_SSO_exp_SSO_n:\forall n. 3 < n \to 
91 exp n 2 \le exp 2 n.
92 intros.elim H
93   [simplify.apply le_n
94   |simplify.
95    rewrite < plus_n_O.
96    rewrite < times_n_SO.
97    rewrite < times_n_Sm.
98    rewrite < assoc_plus.
99    rewrite < sym_plus.
100    rewrite > plus_n_Sm.
101    apply le_plus
102     [rewrite < exp_SSO.
103      assumption
104     |rewrite > plus_n_O in ⊢ (? (? (? ? %)) ?).
105      change in ⊢ (? (? %) ?) with (2*n1).
106      apply lt_times_SSO_n_exp_SSO_n.
107      apply lt_to_le.
108      assumption
109     ]
110   ]
111 qed.
112
113 (* a variant *)
114 theorem le_exp_n_SSO_exp_SSO_n1:\forall n. S O < n \to
115 exp (4*n) 2 \le exp 2 (3*n).
116 intros.elim H
117   [apply leb_true_to_le.reflexivity
118   |cut (exp (S n1) 2 \le 3*(exp n1 2))
119     [apply (trans_le ? (3*exp (4*n1) 2))
120       [rewrite < times_exp.
121        rewrite < times_exp.
122        rewrite < assoc_times.
123        rewrite > sym_times in ⊢ (? ? (? % ?)).
124        rewrite > assoc_times.
125        apply le_times_r.
126        assumption
127       |apply (trans_le ? (8*exp 2 (3*n1)))
128         [apply le_times
129           [apply leb_true_to_le.reflexivity
130           |assumption
131           ]
132         |change in ⊢ (? (? % ?) ?) with (exp 2 3).
133          rewrite < exp_plus_times.
134          apply le_exp
135           [apply lt_O_S
136           |simplify.rewrite < plus_n_Sm.
137            rewrite < plus_n_Sm.rewrite < plus_n_Sm.
138            apply le_n
139           ]
140         ]
141       ]
142     |rewrite > exp_Sn_SSO.
143      change in ⊢ (? ? %) with ((exp n1 2) + ((exp n1 2) + ((exp n1 2) + O))).
144      rewrite < plus_n_O.
145      rewrite > plus_n_SO.
146      rewrite > assoc_plus.
147      apply le_plus_r.
148      apply le_plus
149       [rewrite > exp_SSO.
150        apply le_times_l.
151        assumption
152       |apply lt_O_exp.
153        apply lt_to_le.assumption
154       ]
155     ]
156   ]
157 qed.
158
159 (* a strict version *)
160 theorem lt_exp_n_SSO_exp_SSO_n:\forall n. 4 < n \to 
161 exp n 2 < exp 2 n.
162 intros.elim H
163   [apply leb_true_to_le.reflexivity.
164   |simplify.
165    rewrite < plus_n_O.
166    rewrite < times_n_SO.
167    rewrite < times_n_Sm.
168    rewrite < assoc_plus.
169    rewrite < sym_plus.
170    rewrite > plus_n_Sm.
171    apply (lt_to_le_to_lt ? ((exp 2 n1)+S (n1+n1)))
172     [apply lt_plus_l.
173      rewrite < exp_SSO.
174      assumption
175     |apply le_plus_r.
176      rewrite > plus_n_O in ⊢ (? (? (? ? %)) ?).
177      change in ⊢ (? (? %) ?) with (2*n1).
178      apply lt_times_SSO_n_exp_SSO_n.
179      apply lt_to_le.apply lt_to_le.
180      assumption
181     ]
182   ]
183 qed.
184
185 theorem le_times_exp_n_SSO_exp_SSO_n:\forall a,n. 1 < a \to 4*a \le n \to 
186 exp 2 a*exp n 2 \le exp 2 n.
187 intros.elim H1
188   [apply (trans_le ? ((exp 2 a)*(exp 2 (3*a))))
189     [apply le_times_r.
190      apply le_exp_n_SSO_exp_SSO_n1.
191      assumption
192     |rewrite < exp_plus_times.
193      apply le_exp
194       [apply lt_O_S
195       |apply le_n
196       ]
197     ]
198   |apply (trans_le ? ((exp 2 a)*(2*(exp n1 2))))
199     [apply le_times_r.
200      simplify.
201      rewrite < times_n_SO.
202      rewrite < sym_times.simplify.
203      rewrite < plus_n_O.
204      rewrite < assoc_plus.
205      rewrite < sym_plus.
206      rewrite > plus_n_Sm.
207      apply le_plus_r.
208      apply (trans_le ? (3*n1))
209       [simplify.rewrite > plus_n_SO.
210        rewrite > assoc_plus.
211        apply le_plus_r.
212        apply le_plus_r.
213        rewrite < plus_n_O.
214        apply (trans_le ? (4*2))
215         [apply leb_true_to_le.reflexivity
216         |apply (trans_le ? (4*a))
217           [apply le_times_r.assumption
218           |assumption
219           ]
220         ]
221       |apply le_times_l.
222        apply (trans_le ? (4*2))
223         [apply leb_true_to_le.reflexivity
224         |apply (trans_le ? (4*a))
225           [apply le_times_r.assumption
226           |assumption
227           ]
228         ]
229       ]
230     |rewrite < assoc_times.
231      rewrite < sym_times in ⊢ (? (? % ?) ?).
232      rewrite > assoc_times.
233      change in ⊢ (? ? %) with (2*exp 2 n1).
234      apply le_times_r.
235      assumption
236     ]
237   ]
238 qed.
239
240 (* the same for log and sqrt 
241 theorem le_times_log_sqrt:\forall a,n. 1 < a \to exp 2 (8*a) \le n \to 
242 exp 2 a*log 2 n \le sqrt n.
243 intros.unfold sqrt.
244 apply f_m_to_le_max
245   [
246   |apply le_to_leb_true.
247    rewrite < exp_SSO.
248    rewrite < times_exp.
249    rewrite > exp_exp_times.
250    apply (trans_le ? (exp 2 (log 2 n)))
251     [apply le_times_exp_n_SSO_exp_SSO_n.
252 *)
253
254          
255