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