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 bc1: \forall n.
  55 (\forall i. i < n \to divides (i!*(n-i)!) n!) \to
  56 \forall k. k < n \to
  57 bc (S n) (S k) = (bc n k) + (bc n (S k)).
  58 intros.unfold bc.
  59 rewrite > (lt_to_lt_to_eq_div_div_times_times ? ? (S k)) in ⊢ (? ? ? (? % ?))
  60   [rewrite > sym_times in ⊢ (? ? ? (? (? ? %) ?)).
  61    rewrite < assoc_times in ⊢ (? ? ? (? (? ? %) ?)).
  62    rewrite > (lt_to_lt_to_eq_div_div_times_times ? ? (n - k)) in ⊢ (? ? ? (? ? %))
  63     [rewrite > assoc_times in ⊢ (? ? ? (? ? (? ? %))).
  64      rewrite > sym_times in ⊢ (? ? ? (? ? (? ? (? ? %)))).
  65      rewrite > fact_minus
  66       [rewrite < eq_div_plus
  67         [rewrite < distr_times_plus.
  68          simplify in ⊢ (? ? ? (? (? ? %) ?)).
  69          rewrite > sym_plus in ⊢ (? ? ? (? (? ? (? %)) ?)).
  70          rewrite < plus_minus_m_m
  71           [rewrite > sym_times in ⊢ (? ? ? (? % ?)).
  72            reflexivity
  73           |apply lt_to_le.
  74            assumption
  75           ]
  76         |rewrite > (times_n_O O).
  77          apply lt_times;apply lt_O_fact
  78         |apply H.
  79
  80
  81 theorem exp_plus_sigma_p:\forall a,b,n.
  82 exp (a+b) n = sigma_p (S n) (\lambda k.true)
  83   (\lambda k.(bc n k)*(exp a (n-k))*(exp b k)).
  84 intros.elim n
  85   [simplify.reflexivity
  86   |simplify in ⊢ (? ? % ?).
  87    rewrite > true_to_sigma_p_Sn
  88     [rewrite <