]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/nat/binomial.ma
Complete proof of Bertrand for n >= 256.
[helm.git] / helm / software / matita / library / nat / binomial.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 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "nat/iteration2.ma".
16 include "nat/factorial2.ma".
17
18 definition bc \def \lambda n,k. n!/(k!*(n-k)!).
19
20 theorem bc_n_n: \forall n. bc n n = S O.
21 intro.unfold bc.
22 rewrite < minus_n_n.
23 simplify in ⊢ (? ? (? ? (? ? %)) ?).
24 rewrite < times_n_SO.
25 apply div_n_n.
26 apply lt_O_fact.
27 qed.
28
29 theorem bc_n_O: \forall n. bc n O = S O.
30 intro.unfold bc.
31 rewrite < minus_n_O.
32 simplify in ⊢ (? ? (? ? %) ?).
33 rewrite < plus_n_O.
34 apply div_n_n.
35 apply lt_O_fact.
36 qed.
37
38 theorem fact_minus: \forall n,k. k < n \to 
39 (n-k)*(n - S k)! = (n - k)!.
40 intros 2.cases n
41   [intro.apply False_ind.
42    apply (lt_to_not_le ? ? H).
43    apply le_O_n
44   |intros.
45    rewrite > minus_Sn_m.
46    reflexivity.
47    apply le_S_S_to_le.
48    assumption
49   ]
50 qed.
51
52 theorem bc2 : \forall n.
53 \forall k. k \leq n \to divides (k!*(n-k)!) n!.
54 intro;elim n
55   [rewrite < (le_n_O_to_eq ? H);apply reflexive_divides
56   |generalize in match H1;cases k
57      [intro;simplify in ⊢ (? (? ? (? %)) ?);simplify in ⊢ (? (? % ?) ?);
58       rewrite > sym_times;rewrite < times_n_SO;apply reflexive_divides
59      |intro;elim (decidable_eq_nat n2 n1)
60         [rewrite > H3;rewrite < minus_n_n;
61          rewrite > times_n_SO in ⊢ (? ? %);apply reflexive_divides
62         |lapply (H n2)
63            [lapply (H (n1 - (S n2)))
64               [change in ⊢ (? ? %) with ((S n1)*n1!);
65                rewrite > (plus_minus_m_m n1 n2) in ⊢ (? ? (? (? %) ?))
66                  [rewrite > sym_plus;
67                   change in ⊢ (? ? (? % ?)) with ((S n2) + (n1 - n2));
68                   rewrite > sym_times in \vdash (? ? %);
69                   rewrite > distr_times_plus in ⊢ (? ? %);
70                   simplify in ⊢ (? (? ? (? %)) ?);
71                   apply divides_plus
72                     [rewrite > sym_times;
73                      change in ⊢ (? (? ? %) ?) with ((S n2)*n2!);
74                      rewrite > sym_times in ⊢ (? (? ? %) ?);
75                      rewrite < assoc_times;
76                      apply divides_times
77                        [rewrite > sym_times;assumption
78                        |apply reflexive_divides]
79                     |rewrite < fact_minus in ⊢ (? (? ? %) ?)
80                        [rewrite > sym_times in ⊢ (? (? ? %) ?);
81                         rewrite < assoc_times;
82                         apply divides_times
83                           [rewrite < eq_plus_minus_minus_minus in Hletin1;
84                              [rewrite > sym_times;rewrite < minus_n_n in Hletin1;
85                               rewrite < plus_n_O in Hletin1;assumption
86                              |lapply (le_S_S_to_le ? ? H2);
87                               elim (le_to_or_lt_eq ? ? Hletin2);
88                                 [assumption
89                                 |elim (H3 H4)]
90                              |constructor 1]
91                           |apply reflexive_divides]
92                        |lapply (le_S_S_to_le ? ? H2);
93                         elim (le_to_or_lt_eq ? ? Hletin2);
94                           [assumption
95                           |elim (H3 H4)]]]
96                  |apply le_S_S_to_le;assumption]
97               |apply le_minus_m;apply le_S_S_to_le;assumption]
98            |apply le_S_S_to_le;assumption]]]]
99 qed.                      
100     
101 theorem bc1: \forall n.\forall k. k < n \to bc (S n) (S k) = (bc n k) + (bc n (S k)). 
102 intros.unfold bc.
103 rewrite > (lt_to_lt_to_eq_div_div_times_times ? ? (S k)) in ⊢ (? ? ? (? % ?))
104   [rewrite > sym_times in ⊢ (? ? ? (? (? ? %) ?)). 
105    rewrite < assoc_times in ⊢ (? ? ? (? (? ? %) ?)).
106    rewrite > (lt_to_lt_to_eq_div_div_times_times ? ? (n - k)) in ⊢ (? ? ? (? ? %))
107     [rewrite > assoc_times in ⊢ (? ? ? (? ? (? ? %))).
108      rewrite > sym_times in ⊢ (? ? ? (? ? (? ? (? ? %)))).
109      rewrite > fact_minus
110       [rewrite < eq_div_plus
111         [rewrite < distr_times_plus.
112          simplify in ⊢ (? ? ? (? (? ? %) ?)).
113          rewrite > sym_plus in ⊢ (? ? ? (? (? ? (? %)) ?)).
114          rewrite < plus_minus_m_m
115           [rewrite > sym_times in ⊢ (? ? ? (? % ?)).
116            reflexivity
117           |apply lt_to_le.
118            assumption
119           ]
120         |rewrite > (times_n_O O).
121          apply lt_times;apply lt_O_fact
122         |change in ⊢ (? (? % ?) ?) with ((S k)*k!);
123          rewrite < sym_times in ⊢ (? ? %);
124          rewrite > assoc_times;apply divides_times
125            [apply reflexive_divides
126            |apply bc2;apply le_S_S_to_le;constructor 2;assumption]
127         |rewrite < fact_minus
128            [rewrite > sym_times in ⊢ (? (? ? %) ?);rewrite < assoc_times;
129             apply divides_times
130               [apply bc2;assumption
131               |apply reflexive_divides]
132            |assumption]]
133      |assumption]
134   |apply lt_to_lt_O_minus;assumption
135   |rewrite > (times_n_O O).
136    apply lt_times;apply lt_O_fact]
137 |apply lt_O_S
138 |rewrite > (times_n_O O).
139  apply lt_times;apply lt_O_fact]
140 qed.
141
142 theorem lt_O_bc: \forall n,m. m \le n \to O < bc n m.
143 intro.elim n
144   [apply (le_n_O_elim ? H).
145    simplify.apply le_n
146   |elim (le_to_or_lt_eq ? ? H1)
147     [generalize in match H2.cases m;intro
148       [rewrite > bc_n_O.apply le_n
149       |rewrite > bc1
150         [apply (trans_le ? (bc n1 n2))
151           [apply H.apply le_S_S_to_le.apply lt_to_le.assumption
152           |apply le_plus_n_r
153           ]
154         |apply le_S_S_to_le.assumption
155         ]
156       ]
157     |rewrite > H2.
158      rewrite > bc_n_n.
159      apply le_n
160     ]
161   ]
162 qed.
163
164 theorem exp_plus_sigma_p:\forall a,b,n.
165 exp (a+b) n = sigma_p (S n) (\lambda k.true) 
166   (\lambda k.(bc n k)*(exp a (n-k))*(exp b k)).
167 intros.elim n
168   [simplify.reflexivity
169   |simplify in ⊢ (? ? % ?).
170    rewrite > true_to_sigma_p_Sn
171     [rewrite > H;rewrite > sym_times in ⊢ (? ? % ?);
172      rewrite > distr_times_plus in ⊢ (? ? % ?);
173      rewrite < minus_n_n in ⊢ (? ? ? (? (? (? ? (? ? %)) ?) ?));
174      rewrite > sym_times in ⊢ (? ? (? % ?) ?);
175      rewrite > sym_times in ⊢ (? ? (? ? %) ?);
176      rewrite > distributive_times_plus_sigma_p in ⊢ (? ? (? % ?) ?);
177      rewrite > distributive_times_plus_sigma_p in ⊢ (? ? (? ? %) ?);
178      rewrite > true_to_sigma_p_Sn in ⊢ (? ? (? ? %) ?)
179        [rewrite < assoc_plus;rewrite < sym_plus in ⊢ (? ? (? % ?) ?);
180         rewrite > assoc_plus;
181         apply eq_f2
182           [rewrite > sym_times;rewrite > assoc_times;autobatch paramodulation
183           |rewrite > (sigma_p_gi ? ? O);
184             [rewrite < (eq_sigma_p_gh ? S pred n1 (S n1) (λx:nat.true)) in ⊢ (? ? (? (? ? %) ?) ?)
185                [rewrite > (sigma_p_gi ? ? O) in ⊢ (? ? ? %);
186                   [rewrite > assoc_plus;apply eq_f2
187                      [autobatch paramodulation; 
188                      |rewrite < sigma_p_plus_1;
189                       rewrite < (eq_sigma_p_gh ? S pred n1 (S n1) (λx:nat.true)) in \vdash (? ? ? %);
190                         [apply eq_sigma_p
191                            [intros;reflexivity
192                            |intros;rewrite > sym_times;rewrite > assoc_times;
193                             rewrite > sym_times in ⊢ (? ? (? (? ? %) ?) ?);
194                             rewrite > assoc_times;rewrite < assoc_times in ⊢ (? ? (? (? ? %) ?) ?);
195                             rewrite > sym_times in ⊢ (? ? (? (? ? (? % ?)) ?) ?);
196                             change in ⊢ (? ? (? (? ? (? % ?)) ?) ?) with (exp a (S (n1 - S x)));
197                             rewrite < (minus_Sn_m ? ? H1);rewrite > minus_S_S;
198                             rewrite > sym_times in \vdash (? ? (? ? %) ?);
199                             rewrite > assoc_times; 
200                             rewrite > sym_times in ⊢ (? ? (? ? (? ? %)) ?);
201                             change in \vdash (? ? (? ? (? ? %)) ?) with (exp b (S x));
202                             rewrite > assoc_times in \vdash (? ? (? ? %) ?);
203                             rewrite > sym_times in \vdash (? ? (? % ?) ?);
204                             rewrite > sym_times in \vdash (? ? (? ? %) ?);
205                             rewrite > assoc_times in \vdash (? ? ? %);
206                             rewrite > sym_times in \vdash (? ? ? %);
207                             rewrite < distr_times_plus;
208                             rewrite > sym_plus;rewrite < bc1;
209                               [reflexivity|assumption]]
210                         |intros;simplify;reflexivity
211                         |intros;simplify;reflexivity
212                         |intros;apply le_S_S;assumption
213                         |intros;reflexivity
214                         |intros 2;elim j
215                             [simplify in H2;destruct H2
216                             |simplify;reflexivity]
217                         |intro;elim j
218                             [simplify in H2;destruct H2
219                             |simplify;apply le_S_S_to_le;assumption]]]
220                   |apply le_S_S;apply le_O_n
221                   |reflexivity]
222                |intros;simplify;reflexivity
223                |intros;simplify;reflexivity
224                |intros;apply le_S_S;assumption
225                |intros;reflexivity
226                |intros 2;elim j
227                   [simplify in H2;destruct H2
228                   |simplify;reflexivity]
229                |intro;elim j
230                   [simplify in H2;destruct H2
231                   |simplify;apply le_S_S_to_le;assumption]]
232             |apply le_S_S;apply le_O_n
233             |reflexivity]]
234       |reflexivity]
235    |reflexivity]]
236 qed.
237
238 theorem exp_S_sigma_p:\forall a,n.
239 exp (S a) n = sigma_p (S n) (\lambda k.true) (\lambda k.(bc n k)*(exp a (n-k))).
240 intros.
241 rewrite > plus_n_SO.
242 rewrite > exp_plus_sigma_p.
243 apply eq_sigma_p;intros
244   [reflexivity
245   |rewrite < exp_SO_n.
246    rewrite < times_n_SO.
247    reflexivity
248   ]
249 qed.
250
251 theorem exp_Sn_SSO: \forall n. exp (S n) 2 = S((exp n 2) + 2*n).
252 intros.simplify.
253 rewrite < times_n_SO.
254 rewrite < plus_n_O.
255 rewrite < sym_times.simplify.
256 rewrite < assoc_plus.
257 rewrite < sym_plus.
258 reflexivity.
259 qed.
260