]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/lib/arithmetics/factorial.ma
Matitaweb:
[helm.git] / matitaB / matita / lib / arithmetics / factorial.ma
1 (*
2     ||M||  This file is part of HELM, an Hypertextual, Electronic        
3     ||A||  Library of Mathematics, developed at the Computer Science     
4     ||T||  Department of the University of Bologna, Italy.                     
5     ||I||                                                                 
6     ||T||  
7     ||A||  This file is distributed under the terms of the 
8     \   /  GNU General Public License Version 2        
9      \ /      
10       V_______________________________________________________________ *)
11
12 include "arithmetics/exp.ma".
13
14 let rec fact n ≝
15   match n with 
16   [ O ⇒ 1
17   | S m ⇒ fact m * S m].
18
19 interpretation "factorial" 'fact n = (fact n).
20
21 theorem le_1_fact : ∀n. 1 ≤ n!.
22 #n (elim n) normalize /2/ 
23 qed.
24
25 theorem le_2_fact : ∀n. 1 < n → 2 ≤ n!.
26 #n (cases n)
27   [#abs @False_ind /2/
28   |#m normalize #le2 @(le_times 1 ? 2) //
29   ]
30 qed.
31
32 theorem le_n_fact_n: ∀n. n ≤ n!.
33 #n (elim n) normalize //
34 #n #Hind @(transitive_le ? (1*(S n))) // @le_times //
35 qed.
36
37 theorem lt_n_fact_n: ∀n. 2 < n → n < n!.
38 #n (cases n) 
39   [#H @False_ind /2/ 
40   |#m #lt2 normalize @(lt_to_le_to_lt ? (2*(S m))) //
41    @le_times // @le_2_fact /2/ 
42 qed.
43
44 (* approximations *)
45
46 theorem fact_to_exp1: ∀n.O<n →
47  (2*n)! ≤ (2^(pred (2*n))) * n! * n!.
48 #n #posn (cut (∀i.2*(S i) = S(S(2*i)))) [//] #H (elim posn) //
49 #n #posn #Hind @(transitive_le ? ((2*n)!*(2*(S n))*(2*(S n))))
50   [>H normalize @le_times //
51   |cut (pred (2*(S n)) = S(S(pred(2*n))))
52     [>S_pred // @(le_times 1 ? 1) //] #H1
53    cut (2^(pred (2*(S n))) = 2^(pred(2*n))*2*2) 
54     [>H1 >H1 //] #H2 >H2
55    @(transitive_le ? ((2^(pred (2*n))) * n! * n! *(2*(S n))*(2*(S n))))
56     [@le_times[@le_times //]//
57     (* we generalize to hide the computational content *)
58     |normalize in match ((S n)!) generalize in match (S n)
59      #Sn generalize in match 2 #two //
60     ]
61   ]
62 qed.  
63
64 theorem fact_to_exp: ∀n.
65  (2*n)! ≤ (2^(pred (2*n))) * n! * n!.
66 #n (cases n) [normalize // |#n @fact_to_exp1 //]
67 qed.
68
69 theorem exp_to_fact1: ∀n.O < n →
70   2^(2*n)*n!*n! < (S(2*n))!.
71 #n #posn (elim posn) [normalize //]
72 #n #posn #Hind (cut (∀i.2*(S i) = S(S(2*i)))) [//] #H
73 cut (2^(2*(S n)) = 2^(2*n)*2*2) [>H //] #H1 >H1
74 @(le_to_lt_to_lt ? (2^(2*n)*n!*n!*(2*(S n))*(2*(S n))))
75   [normalize in match ((S n)!) generalize in match (S n) #Sn
76    generalize in match 2 #two //
77   |cut ((S(2*(S n)))! = (S(2*n))!*(S(S(2*n)))*(S(S(S(2*n)))))
78    [>H //] #H2 >H2 @lt_to_le_to_lt_times
79      [@lt_to_le_to_lt_times //|>H // | //]
80   ]
81 qed.
82      
83 (* a slightly better result 
84 theorem fact3: \forall n.O < n \to
85 (exp 2 (2*n))*(exp (fact n) 2) \le 2*n*fact (2*n).
86 intros.
87 elim H
88   [simplify.apply le_n
89   |rewrite > times_SSO.
90    rewrite > factS.
91    rewrite < times_exp.
92    change in ⊢ (? (? % ?) ?) with ((S(S O))*((S(S O))*(exp (S(S O)) ((S(S O))*n1)))).
93    rewrite > assoc_times.
94    rewrite > assoc_times in ⊢ (? (? ? %) ?).
95    rewrite < assoc_times in ⊢ (? (? ? (? ? %)) ?).
96    rewrite < sym_times in ⊢ (? (? ? (? ? (? % ?))) ?).
97    rewrite > assoc_times in ⊢ (? (? ? (? ? %)) ?).
98    apply (trans_le ? (((S(S O))*((S(S O))*((S n1)\sup((S(S O)))*((S(S O))*n1*((S(S O))*n1)!))))))
99     [apply le_times_r.
100      apply le_times_r.
101      apply le_times_r.
102      assumption
103     |rewrite > factS.
104      rewrite > factS.
105      rewrite < times_SSO.
106      rewrite > assoc_times in ⊢ (? ? %). 
107      apply le_times_r.
108      rewrite < assoc_times.
109      change in ⊢ (? (? (? ? %) ?) ?) with ((S n1)*((S n1)*(S O))).
110      rewrite < assoc_times in ⊢ (? (? % ?) ?).
111      rewrite < times_n_SO.
112      rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?).
113      rewrite < assoc_times in ⊢ (? ? %).
114      rewrite < assoc_times in ⊢ (? ? (? % ?)).
115      apply le_times_r.
116      apply le_times_l.
117      apply le_S.apply le_n
118     ]
119   ]
120 qed.
121
122 theorem le_fact_10: fact (2*5) \le (exp 2 ((2*5)-2))*(fact 5)*(fact 5).
123 simplify in \vdash (? (? %) ?).
124 rewrite > factS in \vdash (? % ?).
125 rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash(? % ?).
126 rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash (? % ?).
127 rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash (? % ?).
128 rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash (? % ?).
129 apply le_times_l.
130 apply leb_true_to_le.reflexivity.
131 qed.
132
133 theorem ab_times_cd: \forall a,b,c,d.(a*b)*(c*d)=(a*c)*(b*d).
134 intros.
135 rewrite > assoc_times.
136 rewrite > assoc_times.
137 apply eq_f.
138 rewrite < assoc_times.
139 rewrite < assoc_times.
140 rewrite > sym_times in \vdash (? ? (? % ?) ?).
141 reflexivity.
142 qed.
143
144 (* an even better result *)
145 theorem lt_SSSSO_to_fact: \forall n.4<n \to
146 fact (2*n) \le (exp 2 ((2*n)-2))*(fact n)*(fact n).
147 intros.elim H
148   [apply le_fact_10
149   |rewrite > times_SSO.
150    change in \vdash (? ? (? (? (? ? %) ?) ?)) with (2*n1 - O);
151    rewrite < minus_n_O.
152    rewrite > factS.
153    rewrite > factS.
154    rewrite < assoc_times.
155    rewrite > factS.
156    apply (trans_le ? ((2*(S n1))*(2*(S n1))*(fact (2*n1))))
157     [apply le_times_l.
158      rewrite > times_SSO.
159      apply le_times_r.
160      apply le_n_Sn
161     |apply (trans_le ? (2*S n1*(2*S n1)*(2\sup(2*n1-2)*n1!*n1!)))
162       [apply le_times_r.assumption
163       |rewrite > assoc_times.
164        rewrite > ab_times_cd in \vdash (? (? ? %) ?).
165        rewrite < assoc_times.
166        apply le_times_l.
167        rewrite < assoc_times in \vdash (? (? ? %) ?).
168        rewrite > ab_times_cd.
169        apply le_times_l.
170        rewrite < exp_S.
171        rewrite < exp_S.
172        apply le_exp
173         [apply lt_O_S
174         |rewrite > eq_minus_S_pred.
175          rewrite < S_pred
176           [rewrite > eq_minus_S_pred.
177            rewrite < S_pred
178             [rewrite < minus_n_O.
179              apply le_n
180             |elim H1;simplify
181               [apply lt_O_S
182               |apply lt_O_S
183               ]
184             ]
185           |elim H1;simplify
186             [apply lt_O_S
187             |rewrite < plus_n_Sm.
188              rewrite < minus_n_O.
189              apply lt_O_S
190             ]
191           ]
192         ]
193       ]
194     ]
195   ]
196 qed. *)