matita/library/nat/factorial2.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 (*       \ /        Matita is distributed under the terms of the          *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "nat/exp.ma".
  16 include "nat/factorial.ma".
  17
  18 theorem factS: \forall n. fact (S n) = (S n)*(fact n).
  19 intro.simplify.reflexivity.
  20 qed.
  21
  22 theorem exp_S: \forall n,m. exp m (S n) = m*exp m n.
  23 intros.reflexivity.
  24 qed.
  25
  26 theorem lt_O_to_fact1: \forall n.O<n \to
  27 fact (2*n) \le (exp 2 (pred (2*n)))*(fact n)*(fact n).
  28 intros.elim H
  29   [apply le_n
  30   |rewrite > times_SSO.
  31    rewrite > factS.
  32    rewrite > factS.
  33    rewrite < assoc_times.
  34    rewrite > factS.
  35    apply (trans_le ? ((2*(S n1))*(2*(S n1))*(fact (2*n1))))
  36     [apply le_times_l.
  37      rewrite > times_SSO.
  38      apply le_times_r.
  39      apply le_n_Sn
  40     |rewrite > assoc_times.
  41      rewrite > assoc_times.
  42      rewrite > assoc_times in ⊢ (? ? %).
  43      change in ⊢ (? ? (? (? ? %) ?)) with (S(2*n1)).
  44      rewrite > exp_S.
  45      rewrite > assoc_times in ⊢ (? ? %).
  46      apply le_times_r.
  47      rewrite < assoc_times.
  48      rewrite < assoc_times.
  49      rewrite < sym_times in ⊢ (? (? (? % ?) ?) ?).
  50      rewrite > assoc_times.
  51      rewrite > assoc_times.
  52      rewrite > S_pred in ⊢ (? ? (? (? ? %) ?))
  53       [rewrite > exp_S.
  54        rewrite > assoc_times in ⊢ (? ? %).
  55        apply le_times_r.
  56        rewrite > sym_times in ⊢ (? ? %).
  57        rewrite > assoc_times in ⊢ (? ? %).
  58        rewrite > assoc_times in ⊢ (? ? %).
  59        apply le_times_r.
  60        rewrite < assoc_times in ⊢ (? ? %).
  61        rewrite < assoc_times in ⊢ (? ? %).
  62        rewrite < sym_times in ⊢ (? ? (? (? % ?) ?)).
  63        rewrite > assoc_times in ⊢ (? ? %).
  64        rewrite > assoc_times in ⊢ (? ? %).
  65        apply le_times_r.
  66        rewrite > sym_times in ⊢ (? ? (? ? %)).
  67        rewrite > sym_times in ⊢ (? ? %).
  68        assumption
  69       |unfold.rewrite > times_n_SO in ⊢ (? % ?).
  70        apply le_times
  71         [apply le_n_Sn
  72         |assumption
  73         ]
  74       ]
  75     ]
  76   ]
  77 qed.
  78
  79 theorem fact1: \forall n.
  80 fact (2*n) \le (exp 2 (pred (2*n)))*(fact n)*(fact n).
  81 intro.cases n
  82   [apply le_n
  83   |apply lt_O_to_fact1.
  84    apply lt_O_S
  85   ]
  86 qed.
  87
  88 theorem lt_O_fact: \forall n. O < fact n.
  89 intro.elim n
  90   [simplify.apply lt_O_S
  91   |rewrite > factS.
  92    rewrite > (times_n_O O).
  93    apply lt_times
  94     [apply lt_O_S
  95     |assumption
  96     ]
  97   ]
  98 qed.
  99
 100 theorem fact2: \forall n.O < n \to
 101 (exp (S(S O)) ((S(S O))*n))*(fact n)*(fact n) < fact (S((S(S O))*n)).
 102 intros.elim H
 103   [simplify.apply le_S.apply le_n
 104   |rewrite > times_SSO.
 105    rewrite > factS.
 106    rewrite > factS.
 107    rewrite < assoc_times.
 108    rewrite > factS.
 109    rewrite < times_SSO in ⊢ (? ? %).
 110    apply (trans_lt ? (((S(S O))*S n1)*((S(S O))*S n1*(S ((S(S O))*n1))!)))
 111     [rewrite > assoc_times in ⊢ (? ? %).
 112      rewrite > exp_S.
 113      rewrite > assoc_times.
 114      rewrite > assoc_times.
 115      rewrite > assoc_times.
 116      apply lt_times_r.
 117      rewrite > exp_S.
 118      rewrite > assoc_times.
 119      rewrite > sym_times in ⊢ (? ? %).
 120      rewrite > assoc_times in ⊢ (? ? %).
 121      rewrite > assoc_times in ⊢ (? ? %).
 122      apply lt_times_r.
 123      rewrite > sym_times.
 124      rewrite > assoc_times.
 125      rewrite > assoc_times.
 126      apply lt_times_r.
 127      rewrite < assoc_times.
 128      rewrite < assoc_times.
 129      rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?).
 130      rewrite > assoc_times.
 131      rewrite > assoc_times.
 132      rewrite > sym_times in ⊢ (? ? %).
 133      apply lt_times_r.
 134      rewrite < assoc_times.
 135      rewrite < sym_times.
 136      rewrite < assoc_times.
 137      assumption
 138     |apply lt_times_l1
 139       [rewrite > (times_n_O O) in ⊢ (? % ?).
 140        apply lt_times
 141         [rewrite > (times_n_O O) in ⊢ (? % ?).
 142          apply lt_times
 143           [apply lt_O_S
 144           |apply lt_O_S
 145           ]
 146         |apply lt_O_fact
 147         ]
 148       |apply le_n
 149       ]
 150     ]
 151   ]
 152 qed.
 153
 154 (* a slightly better result *)
 155 theorem fact3: \forall n.O < n \to
 156 (exp (S(S O)) ((S(S O))*n))*(exp (fact n) (S(S O))) \le (S(S O))*n*fact ((S(S O))*n).
 157 intros.
 158 elim H
 159   [simplify.apply le_n
 160   |rewrite > times_SSO.
 161    rewrite > factS.
 162    rewrite < times_exp.
 163    change in ⊢ (? (? % ?) ?) with ((S(S O))*((S(S O))*(exp (S(S O)) ((S(S O))*n1)))).
 164    rewrite > assoc_times.
 165    rewrite > assoc_times in ⊢ (? (? ? %) ?).
 166    rewrite < assoc_times in ⊢ (? (? ? (? ? %)) ?).
 167    rewrite < sym_times in ⊢ (? (? ? (? ? (? % ?))) ?).
 168    rewrite > assoc_times in ⊢ (? (? ? (? ? %)) ?).
 169    apply (trans_le ? (((S(S O))*((S(S O))*((S n1)\sup((S(S O)))*((S(S O))*n1*((S(S O))*n1)!))))))
 170     [apply le_times_r.
 171      apply le_times_r.
 172      apply le_times_r.
 173      assumption
 174     |rewrite > factS.
 175      rewrite > factS.
 176      rewrite < times_SSO.
 177      rewrite > assoc_times in ⊢ (? ? %).
 178      apply le_times_r.
 179      rewrite < assoc_times.
 180      change in ⊢ (? (? (? ? %) ?) ?) with ((S n1)*((S n1)*(S O))).
 181      rewrite < assoc_times in ⊢ (? (? % ?) ?).
 182      rewrite < times_n_SO.
 183      rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?).
 184      rewrite < assoc_times in ⊢ (? ? %).
 185      rewrite < assoc_times in ⊢ (? ? (? % ?)).
 186      apply le_times_r.
 187      apply le_times_l.
 188      apply le_S.apply le_n
 189     ]
 190   ]
 191 qed.
 192
 193 theorem le_fact_10: fact (2*5) \le (exp 2 ((2*5)-2))*(fact 5)*(fact 5).
 194 simplify in \vdash (? (? %) ?).
 195 rewrite > factS in \vdash (? % ?).
 196 rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash(? % ?).
 197 rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash (? % ?).
 198 rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash (? % ?).
 199 rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash (? % ?).
 200 apply le_times_l.
 201 apply leb_true_to_le.reflexivity.
 202 qed.
 203
 204 theorem ab_times_cd: \forall a,b,c,d.(a*b)*(c*d)=(a*c)*(b*d).
 205 intros.
 206 rewrite > assoc_times.
 207 rewrite > assoc_times.
 208 apply eq_f.
 209 rewrite < assoc_times.
 210 rewrite < assoc_times.
 211 rewrite > sym_times in \vdash (? ? (? % ?) ?).
 212 reflexivity.
 213 qed.
 214
 215 (* an even better result *)
 216 theorem lt_SSSSO_to_fact: \forall n.4<n \to
 217 fact (2*n) \le (exp 2 ((2*n)-2))*(fact n)*(fact n).
 218 intros.elim H
 219   [apply le_fact_10
 220   |rewrite > times_SSO.
 221    change in \vdash (? ? (? (? (? ? %) ?) ?)) with (2*n1 - O);
 222    rewrite < minus_n_O.
 223    rewrite > factS.
 224    rewrite > factS.
 225    rewrite < assoc_times.
 226    rewrite > factS.
 227    apply (trans_le ? ((2*(S n1))*(2*(S n1))*(fact (2*n1))))
 228     [apply le_times_l.
 229      rewrite > times_SSO.
 230      apply le_times_r.
 231      apply le_n_Sn
 232     |apply (trans_le ? (2*S n1*(2*S n1)*(2\sup(2*n1-2)*n1!*n1!)))
 233       [apply le_times_r.assumption
 234       |rewrite > assoc_times.
 235        rewrite > ab_times_cd in \vdash (? (? ? %) ?).
 236        rewrite < assoc_times.
 237        apply le_times_l.
 238        rewrite < assoc_times in \vdash (? (? ? %) ?).
 239        rewrite > ab_times_cd.
 240        apply le_times_l.
 241        rewrite < exp_S.
 242        rewrite < exp_S.
 243        apply le_exp
 244         [apply lt_O_S
 245         |rewrite > eq_minus_S_pred.
 246          rewrite < S_pred
 247           [rewrite > eq_minus_S_pred.
 248            rewrite < S_pred
 249             [rewrite < minus_n_O.
 250              apply le_n
 251             |elim H1;simplify
 252               [apply lt_O_S
 253               |apply lt_O_S
 254               ]
 255             ]
 256           |elim H1;simplify
 257             [apply lt_O_S
 258             |rewrite < plus_n_Sm.
 259              rewrite < minus_n_O.
 260              apply lt_O_S
 261             ]
 262           ]
 263         ]
 264       ]
 265     ]
 266   ]
 267 qed.
 268
 269
 270 (*
 271 theorem stirling: \forall n,k.k \le n \to
 272 log (fact n) < n*log n - n + k*log n.
 273 intro.
 274 apply (nat_elim1 n).
 275 intros.
 276 elim (lt_O_to_or_eq_S m)
 277   [elim H2.clear H2.
 278    elim H4.clear H4.
 279    rewrite > H2.
 280    apply (le_to_lt_to_lt ? (log ((exp (S(S O)) ((S(S O))*a))*(fact a)*(fact a))))
 281     [apply monotonic_log.
 282      apply fact1
 283     |rewrite > assoc_times in ⊢ (? (? %) ?).
 284      rewrite > log_exp.
 285      apply (le_to_lt_to_lt ? ((S(S O))*a+S(log a!+log a!)))
 286       [apply le_plus_r.
 287        apply log_times
 288       |rewrite < plus_n_Sm.
 289        rewrite > plus_n_O in ⊢ (? (? (? ? (? ? %))) ?).
 290        change with
 291         (S((S(S O))*a+((S(S O))*log a!)) < (S(S O))*a*log ((S(S O))*a)-(S(S O))*a+k*log ((S(S O))*a)).
 292        apply (trans_lt ? (S ((S(S O))*a+(S(S O))*(a*log a-a+k*log a))))
 293         [apply le_S_S.
 294          apply lt_plus_r.
 295          apply lt_times_r.
 296          apply H.
 297          assumption
 298         |
 299
 300           [
 301
 302        a*log a-a+k*log a
 303
 304 *)