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 alias num (instance 0) = "natural number".
  29 lemma times_SSO: \forall n.2*(S n) = S(S(2*n)).
  30 intro.simplify.rewrite < plus_n_Sm.reflexivity.
  31 qed.
  32
  33 theorem lt_O_to_fact1: \forall n.O<n \to
  34 fact (2*n) \le (exp 2 (pred (2*n)))*(fact n)*(fact n).
  35 intros.elim H
  36   [apply le_n
  37   |rewrite > times_SSO.
  38    rewrite > factS.
  39    rewrite > factS.
  40    rewrite < assoc_times.
  41    rewrite > factS.
  42    apply (trans_le ? ((2*(S n1))*(2*(S n1))*(fact (2*n1))))
  43     [apply le_times_l.
  44      rewrite > times_SSO.
  45      apply le_times_r.
  46      apply le_n_Sn
  47     |rewrite > assoc_times.
  48      rewrite > assoc_times.
  49      rewrite > assoc_times in ⊢ (? ? %).
  50      change in ⊢ (? ? (? (? ? %) ?)) with (S(2*n1)).
  51      rewrite > exp_S.
  52      rewrite > assoc_times in ⊢ (? ? %).
  53      apply le_times_r.
  54      rewrite < assoc_times.
  55      rewrite < assoc_times.
  56      rewrite < sym_times in ⊢ (? (? (? % ?) ?) ?).
  57      rewrite > assoc_times.
  58      rewrite > assoc_times.
  59      rewrite > S_pred in ⊢ (? ? (? (? ? %) ?))
  60       [rewrite > exp_S.
  61        rewrite > assoc_times in ⊢ (? ? %).
  62        apply le_times_r.
  63        rewrite > sym_times in ⊢ (? ? %).
  64        rewrite > assoc_times in ⊢ (? ? %).
  65        rewrite > assoc_times in ⊢ (? ? %).
  66        apply le_times_r.
  67        rewrite < assoc_times in ⊢ (? ? %).
  68        rewrite < assoc_times in ⊢ (? ? %).
  69        rewrite < sym_times in ⊢ (? ? (? (? % ?) ?)).
  70        rewrite > assoc_times in ⊢ (? ? %).
  71        rewrite > assoc_times in ⊢ (? ? %).
  72        apply le_times_r.
  73        rewrite > sym_times in ⊢ (? ? (? ? %)).
  74        rewrite > sym_times in ⊢ (? ? %).
  75        assumption
  76       |unfold.rewrite > times_n_SO in ⊢ (? % ?).
  77        apply le_times
  78         [apply le_n_Sn
  79         |assumption
  80         ]
  81       ]
  82     ]
  83   ]
  84 qed.
  85
  86 theorem fact1: \forall n.
  87 fact (2*n) \le (exp 2 (pred (2*n)))*(fact n)*(fact n).
  88 intro.cases n
  89   [apply le_n
  90   |apply lt_O_to_fact1.
  91    apply lt_O_S
  92   ]
  93 qed.
  94
  95 theorem lt_O_fact: \forall n. O < fact n.
  96 intro.elim n
  97   [simplify.apply lt_O_S
  98   |rewrite > factS.
  99    rewrite > (times_n_O O).
 100    apply lt_times
 101     [apply lt_O_S
 102     |assumption
 103     ]
 104   ]
 105 qed.
 106
 107 theorem fact2: \forall n.O < n \to
 108 (exp (S(S O)) ((S(S O))*n))*(fact n)*(fact n) < fact (S((S(S O))*n)).
 109 intros.elim H
 110   [simplify.apply le_S.apply le_n
 111   |rewrite > times_SSO.
 112    rewrite > factS.
 113    rewrite > factS.
 114    rewrite < assoc_times.
 115    rewrite > factS.
 116    rewrite < times_SSO in ⊢ (? ? %).
 117    apply (trans_lt ? (((S(S O))*S n1)*((S(S O))*S n1*(S ((S(S O))*n1))!)))
 118     [rewrite > assoc_times in ⊢ (? ? %).
 119      rewrite > exp_S.
 120      rewrite > assoc_times.
 121      rewrite > assoc_times.
 122      rewrite > assoc_times.
 123      apply lt_times_r.
 124      rewrite > exp_S.
 125      rewrite > assoc_times.
 126      rewrite > sym_times in ⊢ (? ? %).
 127      rewrite > assoc_times in ⊢ (? ? %).
 128      rewrite > assoc_times in ⊢ (? ? %).
 129      apply lt_times_r.
 130      rewrite > sym_times.
 131      rewrite > assoc_times.
 132      rewrite > assoc_times.
 133      apply lt_times_r.
 134      rewrite < assoc_times.
 135      rewrite < assoc_times.
 136      rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?).
 137      rewrite > assoc_times.
 138      rewrite > assoc_times.
 139      rewrite > sym_times in ⊢ (? ? %).
 140      apply lt_times_r.
 141      rewrite < assoc_times.
 142      rewrite < sym_times.
 143      rewrite < assoc_times.
 144      assumption
 145     |apply lt_times_l1
 146       [rewrite > (times_n_O O) in ⊢ (? % ?).
 147        apply lt_times
 148         [rewrite > (times_n_O O) in ⊢ (? % ?).
 149          apply lt_times
 150           [apply lt_O_S
 151           |apply lt_O_S
 152           ]
 153         |apply lt_O_fact
 154         ]
 155       |apply le_n
 156       ]
 157     ]
 158   ]
 159 qed.
 160
 161 (* a slightly better result *)
 162 theorem fact3: \forall n.O < n \to
 163 (exp (S(S O)) ((S(S O))*n))*(exp (fact n) (S(S O))) \le (S(S O))*n*fact ((S(S O))*n).
 164 intros.
 165 elim H
 166   [simplify.apply le_n
 167   |rewrite > times_SSO.
 168    rewrite > factS.
 169    rewrite < times_exp.
 170    change in ⊢ (? (? % ?) ?) with ((S(S O))*((S(S O))*(exp (S(S O)) ((S(S O))*n1)))).
 171    rewrite > assoc_times.
 172    rewrite > assoc_times in ⊢ (? (? ? %) ?).
 173    rewrite < assoc_times in ⊢ (? (? ? (? ? %)) ?).
 174    rewrite < sym_times in ⊢ (? (? ? (? ? (? % ?))) ?).
 175    rewrite > assoc_times in ⊢ (? (? ? (? ? %)) ?).
 176    apply (trans_le ? (((S(S O))*((S(S O))*((S n1)\sup((S(S O)))*((S(S O))*n1*((S(S O))*n1)!))))))
 177     [apply le_times_r.
 178      apply le_times_r.
 179      apply le_times_r.
 180      assumption
 181     |rewrite > factS.
 182      rewrite > factS.
 183      rewrite < times_SSO.
 184      rewrite > assoc_times in ⊢ (? ? %).
 185      apply le_times_r.
 186      rewrite < assoc_times.
 187      change in ⊢ (? (? (? ? %) ?) ?) with ((S n1)*((S n1)*(S O))).
 188      rewrite < assoc_times in ⊢ (? (? % ?) ?).
 189      rewrite < times_n_SO.
 190      rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?).
 191      rewrite < assoc_times in ⊢ (? ? %).
 192      rewrite < assoc_times in ⊢ (? ? (? % ?)).
 193      apply le_times_r.
 194      apply le_times_l.
 195      apply le_S.apply le_n
 196     ]
 197   ]
 198 qed.
 199
 200 (*
 201 theorem stirling: \forall n,k.k \le n \to
 202 log (fact n) < n*log n - n + k*log n.
 203 intro.
 204 apply (nat_elim1 n).
 205 intros.
 206 elim (lt_O_to_or_eq_S m)
 207   [elim H2.clear H2.
 208    elim H4.clear H4.
 209    rewrite > H2.
 210    apply (le_to_lt_to_lt ? (log ((exp (S(S O)) ((S(S O))*a))*(fact a)*(fact a))))
 211     [apply monotonic_log.
 212      apply fact1
 213     |rewrite > assoc_times in ⊢ (? (? %) ?).
 214      rewrite > log_exp.
 215      apply (le_to_lt_to_lt ? ((S(S O))*a+S(log a!+log a!)))
 216       [apply le_plus_r.
 217        apply log_times
 218       |rewrite < plus_n_Sm.
 219        rewrite > plus_n_O in ⊢ (? (? (? ? (? ? %))) ?).
 220        change with
 221         (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)).
 222        apply (trans_lt ? (S ((S(S O))*a+(S(S O))*(a*log a-a+k*log a))))
 223         [apply le_S_S.
 224          apply lt_plus_r.
 225          apply lt_times_r.
 226          apply H.
 227          assumption
 228         |
 229
 230           [
 231
 232        a*log a-a+k*log a
 233
 234 *)