]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/nat/factorial2.ma
Some progress.
[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 set "baseuri" "cic:/matita/nat/factorial2".
16
17 include "nat/exp.ma".
18 include "nat/factorial.ma".
19
20 theorem factS: \forall n. fact (S n) = (S n)*(fact n).
21 intro.simplify.reflexivity.
22 qed.
23
24 theorem exp_S: \forall n,m. exp m (S n) = m*exp m n.
25 intros.reflexivity.
26 qed.
27
28 lemma times_SSO: \forall n.(S(S O))*(S n) = S(S((S(S O))*n)).
29 intro.simplify.rewrite < plus_n_Sm.reflexivity.
30 qed.
31
32 theorem fact1: \forall n.
33 fact ((S(S O))*n) \le (exp (S(S O)) ((S(S O))*n))*(fact n)*(fact n).
34 intro.elim n
35   [rewrite < times_n_O.apply le_n
36   |rewrite > times_SSO.
37    rewrite > factS.
38    rewrite > factS.
39    rewrite < assoc_times.
40    rewrite > factS.
41    apply (trans_le ? (((S(S O))*(S n1))*((S(S O))*(S n1))*(fact (((S(S O))*n1)))))
42     [apply le_times_l.
43      rewrite > times_SSO.
44      apply le_times_r.
45      apply le_n_Sn
46     |rewrite > assoc_times.
47      rewrite > assoc_times.
48      rewrite > assoc_times in ⊢ (? ? %).
49      rewrite > exp_S. 
50      rewrite > assoc_times in ⊢ (? ? %).
51      apply le_times_r.
52      rewrite < assoc_times.
53      rewrite < assoc_times.
54      rewrite < sym_times in ⊢ (? (? (? % ?) ?) ?).
55      rewrite > assoc_times.
56      rewrite > assoc_times.
57      rewrite > exp_S. 
58      rewrite > assoc_times in ⊢ (? ? %).
59      apply le_times_r.
60      rewrite > sym_times in ⊢ (? ? %).
61      rewrite > assoc_times in ⊢ (? ? %).
62      rewrite > assoc_times in ⊢ (? ? %).
63      apply le_times_r.
64      rewrite < assoc_times in ⊢ (? ? %).
65      rewrite < assoc_times in ⊢ (? ? %).
66      rewrite < sym_times in ⊢ (? ? (? (? % ?) ?)).
67      rewrite > assoc_times in ⊢ (? ? %).
68      rewrite > assoc_times in ⊢ (? ? %).
69      apply le_times_r.
70      rewrite > sym_times in ⊢ (? ? (? ? %)).
71      rewrite > sym_times in ⊢ (? ? %).
72      assumption
73     ]
74   ]
75 qed.
76
77 theorem lt_O_fact: \forall n. O < fact n.
78 intro.elim n
79   [simplify.apply lt_O_S
80   |rewrite > factS.
81    rewrite > (times_n_O O).
82    apply lt_times
83     [apply lt_O_S
84     |assumption
85     ]
86   ]
87 qed.
88
89 theorem fact2: \forall n.O < n \to
90 (exp (S(S O)) ((S(S O))*n))*(fact n)*(fact n) < fact (S((S(S O))*n)).
91 intros.elim H
92   [simplify.apply le_S.apply le_n
93   |rewrite > times_SSO.
94    rewrite > factS.
95    rewrite > factS.
96    rewrite < assoc_times.
97    rewrite > factS.
98    rewrite < times_SSO in ⊢ (? ? %).
99    apply (trans_lt ? (((S(S O))*S n1)*((S(S O))*S n1*(S ((S(S O))*n1))!)))
100     [rewrite > assoc_times in ⊢ (? ? %).
101      rewrite > exp_S.
102      rewrite > assoc_times.
103      rewrite > assoc_times.
104      rewrite > assoc_times.
105      apply lt_times_r.
106      rewrite > exp_S.
107      rewrite > assoc_times.
108      rewrite > sym_times in ⊢ (? ? %).
109      rewrite > assoc_times in ⊢ (? ? %).
110      rewrite > assoc_times in ⊢ (? ? %).
111      apply lt_times_r.
112      rewrite > sym_times.
113      rewrite > assoc_times.
114      rewrite > assoc_times.
115      apply lt_times_r.
116      rewrite < assoc_times.
117      rewrite < assoc_times.
118      rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?).
119      rewrite > assoc_times.
120      rewrite > assoc_times.
121      rewrite > sym_times in ⊢ (? ? %).
122      apply lt_times_r.
123      rewrite < assoc_times.
124      rewrite < sym_times.
125      rewrite < assoc_times.
126      assumption
127     |apply lt_times_l1
128       [rewrite > (times_n_O O) in ⊢ (? % ?).
129        apply lt_times
130         [rewrite > (times_n_O O) in ⊢ (? % ?).
131          apply lt_times
132           [apply lt_O_S
133           |apply lt_O_S
134           ]
135         |apply lt_O_fact
136         ]
137       |apply le_n
138       ]
139     ]
140   ]
141 qed.
142
143 (* a slightly better result *)
144 theorem fact3: \forall n.O < n \to
145 (exp (S(S O)) ((S(S O))*n))*(exp (fact n) (S(S O))) \le (S(S O))*n*fact ((S(S O))*n).
146 intros.
147 elim H
148   [simplify.apply le_n
149   |rewrite > times_SSO.
150    rewrite > factS.
151    rewrite < times_exp.
152    change in ⊢ (? (? % ?) ?) with ((S(S O))*((S(S O))*(exp (S(S O)) ((S(S O))*n1)))).
153    rewrite > assoc_times.
154    rewrite > assoc_times in ⊢ (? (? ? %) ?).
155    rewrite < assoc_times in ⊢ (? (? ? (? ? %)) ?).
156    rewrite < sym_times in ⊢ (? (? ? (? ? (? % ?))) ?).
157    rewrite > assoc_times in ⊢ (? (? ? (? ? %)) ?).
158    apply (trans_le ? (((S(S O))*((S(S O))*((S n1)\sup((S(S O)))*((S(S O))*n1*((S(S O))*n1)!))))))
159     [apply le_times_r.
160      apply le_times_r.
161      apply le_times_r.
162      assumption
163     |rewrite > factS.
164      rewrite > factS.
165      rewrite < times_SSO.
166      rewrite > assoc_times in ⊢ (? ? %). 
167      apply le_times_r.
168      rewrite < assoc_times.
169      change in ⊢ (? (? (? ? %) ?) ?) with ((S n1)*((S n1)*(S O))).
170      rewrite < assoc_times in ⊢ (? (? % ?) ?).
171      rewrite < times_n_SO.
172      rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?).
173      rewrite < assoc_times in ⊢ (? ? %).
174      rewrite < assoc_times in ⊢ (? ? (? % ?)).
175      apply le_times_r.
176      apply le_times_l.
177      apply le_S.apply le_n
178     ]
179   ]
180 qed.
181
182 (*
183 theorem stirling: \forall n,k.k \le n \to
184 log (fact n) < n*log n - n + k*log n.
185 intro.
186 apply (nat_elim1 n).
187 intros.
188 elim (lt_O_to_or_eq_S m)
189   [elim H2.clear H2.
190    elim H4.clear H4.
191    rewrite > H2.
192    apply (le_to_lt_to_lt ? (log ((exp (S(S O)) ((S(S O))*a))*(fact a)*(fact a))))
193     [apply monotonic_log.
194      apply fact1
195     |rewrite > assoc_times in ⊢ (? (? %) ?).
196      rewrite > log_exp.
197      apply (le_to_lt_to_lt ? ((S(S O))*a+S(log a!+log a!)))
198       [apply le_plus_r.
199        apply log_times
200       |rewrite < plus_n_Sm.
201        rewrite > plus_n_O in ⊢ (? (? (? ? (? ? %))) ?).
202        change with
203         (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)).
204        apply (trans_lt ? (S ((S(S O))*a+(S(S O))*(a*log a-a+k*log a))))
205         [apply le_S_S.
206          apply lt_plus_r.
207          apply lt_times_r.
208          apply H.
209          assumption
210         |
211         
212           [
213        
214        a*log a-a+k*log a
215        
216 *)