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