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 (*
 144 theorem stirling: \forall n,k.k \le n \to
 145 log (fact n) < n*log n - n + k*log n.
 146 intro.
 147 apply (nat_elim1 n).
 148 intros.
 149 elim (lt_O_to_or_eq_S m)
 150   [elim H2.clear H2.
 151    elim H4.clear H4.
 152    rewrite > H2.
 153    apply (le_to_lt_to_lt ? (log ((exp (S(S O)) ((S(S O))*a))*(fact a)*(fact a))))
 154     [apply monotonic_log.
 155      apply fact1
 156     |rewrite > assoc_times in ⊢ (? (? %) ?).
 157      rewrite > log_exp.
 158      apply (le_to_lt_to_lt ? ((S(S O))*a+S(log a!+log a!)))
 159       [apply le_plus_r.
 160        apply log_times
 161       |rewrite < plus_n_Sm.
 162        rewrite > plus_n_O in ⊢ (? (? (? ? (? ? %))) ?).
 163        change with
 164         (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)).
 165        apply (trans_lt ? (S ((S(S O))*a+(S(S O))*(a*log a-a+k*log a))))
 166         [apply le_S_S.
 167          apply lt_plus_r.
 168          apply lt_times_r.
 169          apply H.
 170          assumption
 171         |
 172
 173           [
 174
 175        a*log a-a+k*log a
 176
 177 *)