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