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