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 theorem le_fact_10: fact (2*5) \le (exp 2 ((2*5)-2))*(fact 5)*(fact 5).
 201 simplify in \vdash (? (? %) ?).
 202 rewrite > factS in \vdash (? % ?).
 203 rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash(? % ?).
 204 rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash (? % ?).
 205 rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash (? % ?).
 206 rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash (? % ?).
 207 apply le_times_l.
 208 apply leb_true_to_le.reflexivity.
 209 qed.
 210
 211 theorem ab_times_cd: \forall a,b,c,d.(a*b)*(c*d)=(a*c)*(b*d).
 212 intros.
 213 rewrite > assoc_times.
 214 rewrite > assoc_times.
 215 apply eq_f.
 216 rewrite < assoc_times.
 217 rewrite < assoc_times.
 218 rewrite > sym_times in \vdash (? ? (? % ?) ?).
 219 reflexivity.
 220 qed.
 221
 222 (* an even better result *)
 223 theorem lt_SSSSO_to_fact: \forall n.4<n \to
 224 fact (2*n) \le (exp 2 ((2*n)-2))*(fact n)*(fact n).
 225 intros.elim H
 226   [apply le_fact_10
 227   |rewrite > times_SSO.
 228    change in \vdash (? ? (? (? (? ? %) ?) ?)) with (2*n1 - O);
 229    rewrite < minus_n_O.
 230    rewrite > factS.
 231    rewrite > factS.
 232    rewrite < assoc_times.
 233    rewrite > factS.
 234    apply (trans_le ? ((2*(S n1))*(2*(S n1))*(fact (2*n1))))
 235     [apply le_times_l.
 236      rewrite > times_SSO.
 237      apply le_times_r.
 238      apply le_n_Sn
 239     |apply (trans_le ? (2*S n1*(2*S n1)*(2\sup(2*n1-2)*n1!*n1!)))
 240       [apply le_times_r.assumption
 241       |rewrite > assoc_times.
 242        rewrite > ab_times_cd in \vdash (? (? ? %) ?).
 243        rewrite < assoc_times.
 244        apply le_times_l.
 245        rewrite < assoc_times in \vdash (? (? ? %) ?).
 246        rewrite > ab_times_cd.
 247        apply le_times_l.
 248        rewrite < exp_S.
 249        rewrite < exp_S.
 250        apply le_exp
 251         [apply lt_O_S
 252         |rewrite > eq_minus_S_pred.
 253          rewrite < S_pred
 254           [rewrite > eq_minus_S_pred.
 255            rewrite < S_pred
 256             [rewrite < minus_n_O.
 257              apply le_n
 258             |elim H1;simplify
 259               [apply lt_O_S
 260               |apply lt_O_S
 261               ]
 262             ]
 263           |elim H1;simplify
 264             [apply lt_O_S
 265             |rewrite < plus_n_Sm.
 266              rewrite < minus_n_O.
 267              apply lt_O_S
 268             ]
 269           ]
 270         ]
 271       ]
 272     ]
 273   ]
 274 qed.
 275
 276
 277 (*
 278 theorem stirling: \forall n,k.k \le n \to
 279 log (fact n) < n*log n - n + k*log n.
 280 intro.
 281 apply (nat_elim1 n).
 282 intros.
 283 elim (lt_O_to_or_eq_S m)
 284   [elim H2.clear H2.
 285    elim H4.clear H4.
 286    rewrite > H2.
 287    apply (le_to_lt_to_lt ? (log ((exp (S(S O)) ((S(S O))*a))*(fact a)*(fact a))))
 288     [apply monotonic_log.
 289      apply fact1
 290     |rewrite > assoc_times in ⊢ (? (? %) ?).
 291      rewrite > log_exp.
 292      apply (le_to_lt_to_lt ? ((S(S O))*a+S(log a!+log a!)))
 293       [apply le_plus_r.
 294        apply log_times
 295       |rewrite < plus_n_Sm.
 296        rewrite > plus_n_O in ⊢ (? (? (? ? (? ? %))) ?).
 297        change with
 298         (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)).
 299        apply (trans_lt ? (S ((S(S O))*a+(S(S O))*(a*log a-a+k*log a))))
 300         [apply le_S_S.
 301          apply lt_plus_r.
 302          apply lt_times_r.
 303          apply H.
 304          assumption
 305         |
 306
 307           [
 308
 309        a*log a-a+k*log a
 310
 311 *)