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