]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/nat/factorial2.ma
...
[helm.git] / helm / software / matita / library / nat / factorial2.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/exp.ma".
16 include "nat/factorial.ma".
17
18 theorem factS: \forall n. fact (S n) = (S n)*(fact n).
19 intro.simplify.reflexivity.
20 qed.
21
22 theorem exp_S: \forall n,m. exp m (S n) = m*exp m n.
23 intros.reflexivity.
24 qed.
25
26 theorem lt_O_to_fact1: \forall n.O<n \to
27 fact (2*n) \le (exp 2 (pred (2*n)))*(fact n)*(fact n).
28 intros.elim H
29   [apply le_n
30   |rewrite > times_SSO.
31    rewrite > factS.
32    rewrite > factS.
33    rewrite < assoc_times.
34    rewrite > factS.
35    apply (trans_le ? ((2*(S n1))*(2*(S n1))*(fact (2*n1))))
36     [apply le_times_l.
37      rewrite > times_SSO.
38      apply le_times_r.
39      apply le_n_Sn
40     |rewrite > assoc_times.
41      rewrite > assoc_times.
42      rewrite > assoc_times in ⊢ (? ? %).
43      change in ⊢ (? ? (? (? ? %) ?)) with (S(2*n1)).
44      rewrite > exp_S. 
45      rewrite > assoc_times in ⊢ (? ? %).
46      apply le_times_r.
47      rewrite < assoc_times.
48      rewrite < assoc_times.
49      rewrite < sym_times in ⊢ (? (? (? % ?) ?) ?).
50      rewrite > assoc_times.
51      rewrite > assoc_times.
52      rewrite > S_pred in ⊢ (? ? (? (? ? %) ?))
53       [rewrite > exp_S. 
54        rewrite > assoc_times in ⊢ (? ? %).
55        apply le_times_r.
56        rewrite > sym_times in ⊢ (? ? %).
57        rewrite > assoc_times in ⊢ (? ? %).
58        rewrite > assoc_times in ⊢ (? ? %).
59        apply le_times_r.
60        rewrite < assoc_times in ⊢ (? ? %).
61        rewrite < assoc_times in ⊢ (? ? %).
62        rewrite < sym_times in ⊢ (? ? (? (? % ?) ?)).
63        rewrite > assoc_times in ⊢ (? ? %).
64        rewrite > assoc_times in ⊢ (? ? %).
65        apply le_times_r.
66        rewrite > sym_times in ⊢ (? ? (? ? %)).
67        rewrite > sym_times in ⊢ (? ? %).
68        assumption
69       |unfold.rewrite > times_n_SO in ⊢ (? % ?).
70        apply le_times
71         [apply le_n_Sn
72         |assumption
73         ]
74       ]
75     ]
76   ]
77 qed.
78
79 theorem fact1: \forall n.
80 fact (2*n) \le (exp 2 (pred (2*n)))*(fact n)*(fact n).
81 intro.cases n
82   [apply le_n
83   |apply lt_O_to_fact1.
84    apply lt_O_S
85   ]
86 qed.
87
88 theorem lt_O_fact: \forall n. O < fact n.
89 intro.elim n
90   [simplify.apply lt_O_S
91   |rewrite > factS.
92    rewrite > (times_n_O O).
93    apply lt_times
94     [apply lt_O_S
95     |assumption
96     ]
97   ]
98 qed.
99
100 theorem fact2: \forall n.O < n \to
101 (exp 2 (2*n))*(fact n)*(fact n) < fact (S(2*n)).
102 intros.elim H
103   [simplify.apply le_S.apply le_n
104   |rewrite > times_SSO.
105    rewrite > factS.
106    rewrite > factS.
107    rewrite < assoc_times.
108    rewrite > factS.
109    rewrite < times_SSO in ⊢ (? ? %).
110    apply (trans_lt ? (((S(S O))*S n1)*((S(S O))*S n1*(S ((S(S O))*n1))!)))
111     [rewrite > assoc_times in ⊢ (? ? %).
112      rewrite > exp_S.
113      rewrite > assoc_times.
114      rewrite > assoc_times.
115      rewrite > assoc_times.
116      apply lt_times_r.
117      rewrite > exp_S.
118      rewrite > assoc_times.
119      rewrite > sym_times in ⊢ (? ? %).
120      rewrite > assoc_times in ⊢ (? ? %).
121      rewrite > assoc_times in ⊢ (? ? %).
122      apply lt_times_r.
123      rewrite > sym_times.
124      rewrite > assoc_times.
125      rewrite > assoc_times.
126      apply lt_times_r.
127      rewrite < assoc_times.
128      rewrite < assoc_times.
129      rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?).
130      rewrite > assoc_times.
131      rewrite > assoc_times.
132      rewrite > sym_times in ⊢ (? ? %).
133      apply lt_times_r.
134      rewrite < assoc_times.
135      rewrite < sym_times.
136      rewrite < assoc_times.
137      assumption
138     |apply lt_times_l1
139       [rewrite > (times_n_O O) in ⊢ (? % ?).
140        apply lt_times
141         [rewrite > (times_n_O O) in ⊢ (? % ?).
142          apply lt_times
143           [apply lt_O_S
144           |apply lt_O_S
145           ]
146         |apply lt_O_fact
147         ]
148       |apply le_n
149       ]
150     ]
151   ]
152 qed.
153
154 (* a slightly better result *)
155 theorem fact3: \forall n.O < n \to
156 (exp 2 (2*n))*(exp (fact n) 2) \le 2*n*fact (2*n).
157 intros.
158 elim H
159   [simplify.apply le_n
160   |rewrite > times_SSO.
161    rewrite > factS.
162    rewrite < times_exp.
163    change in ⊢ (? (? % ?) ?) with ((S(S O))*((S(S O))*(exp (S(S O)) ((S(S O))*n1)))).
164    rewrite > assoc_times.
165    rewrite > assoc_times in ⊢ (? (? ? %) ?).
166    rewrite < assoc_times in ⊢ (? (? ? (? ? %)) ?).
167    rewrite < sym_times in ⊢ (? (? ? (? ? (? % ?))) ?).
168    rewrite > assoc_times in ⊢ (? (? ? (? ? %)) ?).
169    apply (trans_le ? (((S(S O))*((S(S O))*((S n1)\sup((S(S O)))*((S(S O))*n1*((S(S O))*n1)!))))))
170     [apply le_times_r.
171      apply le_times_r.
172      apply le_times_r.
173      assumption
174     |rewrite > factS.
175      rewrite > factS.
176      rewrite < times_SSO.
177      rewrite > assoc_times in ⊢ (? ? %). 
178      apply le_times_r.
179      rewrite < assoc_times.
180      change in ⊢ (? (? (? ? %) ?) ?) with ((S n1)*((S n1)*(S O))).
181      rewrite < assoc_times in ⊢ (? (? % ?) ?).
182      rewrite < times_n_SO.
183      rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?).
184      rewrite < assoc_times in ⊢ (? ? %).
185      rewrite < assoc_times in ⊢ (? ? (? % ?)).
186      apply le_times_r.
187      apply le_times_l.
188      apply le_S.apply le_n
189     ]
190   ]
191 qed.
192
193 theorem le_fact_10: fact (2*5) \le (exp 2 ((2*5)-2))*(fact 5)*(fact 5).
194 simplify in \vdash (? (? %) ?).
195 rewrite > factS in \vdash (? % ?).
196 rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash(? % ?).
197 rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash (? % ?).
198 rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash (? % ?).
199 rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash (? % ?).
200 apply le_times_l.
201 apply leb_true_to_le.reflexivity.
202 qed.
203
204 theorem ab_times_cd: \forall a,b,c,d.(a*b)*(c*d)=(a*c)*(b*d).
205 intros.
206 rewrite > assoc_times.
207 rewrite > assoc_times.
208 apply eq_f.
209 rewrite < assoc_times.
210 rewrite < assoc_times.
211 rewrite > sym_times in \vdash (? ? (? % ?) ?).
212 reflexivity.
213 qed.
214
215 (* an even better result *)
216 theorem lt_SSSSO_to_fact: \forall n.4<n \to
217 fact (2*n) \le (exp 2 ((2*n)-2))*(fact n)*(fact n).
218 intros.elim H
219   [apply le_fact_10
220   |rewrite > times_SSO.
221    change in \vdash (? ? (? (? (? ? %) ?) ?)) with (2*n1 - O);
222    rewrite < minus_n_O.
223    rewrite > factS.
224    rewrite > factS.
225    rewrite < assoc_times.
226    rewrite > factS.
227    apply (trans_le ? ((2*(S n1))*(2*(S n1))*(fact (2*n1))))
228     [apply le_times_l.
229      rewrite > times_SSO.
230      apply le_times_r.
231      apply le_n_Sn
232     |apply (trans_le ? (2*S n1*(2*S n1)*(2\sup(2*n1-2)*n1!*n1!)))
233       [apply le_times_r.assumption
234       |rewrite > assoc_times.
235        rewrite > ab_times_cd in \vdash (? (? ? %) ?).
236        rewrite < assoc_times.
237        apply le_times_l.
238        rewrite < assoc_times in \vdash (? (? ? %) ?).
239        rewrite > ab_times_cd.
240        apply le_times_l.
241        rewrite < exp_S.
242        rewrite < exp_S.
243        apply le_exp
244         [apply lt_O_S
245         |rewrite > eq_minus_S_pred.
246          rewrite < S_pred
247           [rewrite > eq_minus_S_pred.
248            rewrite < S_pred
249             [rewrite < minus_n_O.
250              apply le_n
251             |elim H1;simplify
252               [apply lt_O_S
253               |apply lt_O_S
254               ]
255             ]
256           |elim H1;simplify
257             [apply lt_O_S
258             |rewrite < plus_n_Sm.
259              rewrite < minus_n_O.
260              apply lt_O_S
261             ]
262           ]
263         ]
264       ]
265     ]
266   ]
267 qed.
268
269
270 (*
271 theorem stirling: \forall n,k.k \le n \to
272 log (fact n) < n*log n - n + k*log n.
273 intro.
274 apply (nat_elim1 n).
275 intros.
276 elim (lt_O_to_or_eq_S m)
277   [elim H2.clear H2.
278    elim H4.clear H4.
279    rewrite > H2.
280    apply (le_to_lt_to_lt ? (log ((exp (S(S O)) ((S(S O))*a))*(fact a)*(fact a))))
281     [apply monotonic_log.
282      apply fact1
283     |rewrite > assoc_times in ⊢ (? (? %) ?).
284      rewrite > log_exp.
285      apply (le_to_lt_to_lt ? ((S(S O))*a+S(log a!+log a!)))
286       [apply le_plus_r.
287        apply log_times
288       |rewrite < plus_n_Sm.
289        rewrite > plus_n_O in ⊢ (? (? (? ? (? ? %))) ?).
290        change with
291         (S((S(S O))*a+((S(S O))*log a!)) < (S(S O))*a*log ((S(S O))*a)-(S(S O))*a+k*log ((S(S O))*a)).
292        apply (trans_lt ? (S ((S(S O))*a+(S(S O))*(a*log a-a+k*log a))))
293         [apply le_S_S.
294          apply lt_plus_r.
295          apply lt_times_r.
296          apply H.
297          assumption
298         |
299         
300           [
301        
302        a*log a-a+k*log a
303        
304 *)