matita/matita/lib/arithmetics/factorial.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "arithmetics/exp.ma".
  13
  14 let rec fact n ≝
  15   match n with
  16   [ O ⇒ 1
  17   | S m ⇒ fact m * S m].
  18
  19 interpretation "factorial" 'fact n = (fact n).
  20
  21 theorem le_1_fact : ∀n. 1 ≤ n!.
  22 #n (elim n) normalize /2/
  23 qed.
  24
  25 theorem le_2_fact : ∀n. 1 < n → 2 ≤ n!.
  26 #n (cases n)
  27   [#abs @False_ind /2/
  28   |#m normalize #le2 @(le_times 1 ? 2) //
  29   ]
  30 qed.
  31
  32 theorem le_n_fact_n: ∀n. n ≤ n!.
  33 #n (elim n) normalize //
  34 #n #Hind @(transitive_le ? (1*(S n))) // @le_times //
  35 qed.
  36
  37 theorem lt_n_fact_n: ∀n. 2 < n → n < n!.
  38 #n (cases n)
  39   [#H @False_ind /2/
  40   |#m #lt2 normalize @(lt_to_le_to_lt ? (2*(S m))) //
  41    @le_times // @le_2_fact /2/
  42 qed.
  43
  44 (* approximations *)
  45
  46 theorem fact_to_exp1: ∀n.O<n →
  47  (2*n)! ≤ (2^(pred (2*n))) * n! * n!.
  48 #n #posn (cut (∀i.2*(S i) = S(S(2*i)))) [//] #H (elim posn) //
  49 #n #posn #Hind @(transitive_le ? ((2*n)!*(2*(S n))*(2*(S n))))
  50   [>H normalize @le_times //
  51   |cut (pred (2*(S n)) = S(S(pred(2*n))))
  52     [>S_pred // @(le_times 1 ? 1) //] #H1
  53    cut (2^(pred (2*(S n))) = 2^(pred(2*n))*2*2)
  54     [>H1 >H1 //] #H2 >H2
  55    @(transitive_le ? ((2^(pred (2*n))) * n! * n! *(2*(S n))*(2*(S n))))
  56     [@le_times[@le_times //]//
  57     (* we generalize to hide the computational content *)
  58     |normalize in match ((S n)!) generalize in match (S n)
  59      #Sn generalize in match 2 #two //
  60     ]
  61   ]
  62 qed.
  63
  64 theorem fact_to_exp: ∀n.
  65  (2*n)! ≤ (2^(pred (2*n))) * n! * n!.
  66 #n (cases n) [normalize // |#n @fact_to_exp1 //]
  67 qed.
  68
  69 theorem exp_to_fact1: ∀n.O < n →
  70   2^(2*n)*n!*n! < (S(2*n))!.
  71 #n #posn (elim posn) [normalize //]
  72 #n #posn #Hind (cut (∀i.2*(S i) = S(S(2*i)))) [//] #H
  73 cut (2^(2*(S n)) = 2^(2*n)*2*2) [>H //] #H1 >H1
  74 @(le_to_lt_to_lt ? (2^(2*n)*n!*n!*(2*(S n))*(2*(S n))))
  75   [normalize in match ((S n)!) generalize in match (S n) #Sn
  76    generalize in match 2 #two //
  77   |cut ((S(2*(S n)))! = (S(2*n))!*(S(S(2*n)))*(S(S(S(2*n)))))
  78    [>H //] #H2 >H2 @lt_to_le_to_lt_times
  79      [@lt_to_le_to_lt_times //|>H // | //]
  80   ]
  81 qed.
  82
  83 (* a slightly better result
  84 theorem fact3: \forall n.O < n \to
  85 (exp 2 (2*n))*(exp (fact n) 2) \le 2*n*fact (2*n).
  86 intros.
  87 elim H
  88   [simplify.apply le_n
  89   |rewrite > times_SSO.
  90    rewrite > factS.
  91    rewrite < times_exp.
  92    change in ⊢ (? (? % ?) ?) with ((S(S O))*((S(S O))*(exp (S(S O)) ((S(S O))*n1)))).
  93    rewrite > assoc_times.
  94    rewrite > assoc_times in ⊢ (? (? ? %) ?).
  95    rewrite < assoc_times in ⊢ (? (? ? (? ? %)) ?).
  96    rewrite < sym_times in ⊢ (? (? ? (? ? (? % ?))) ?).
  97    rewrite > assoc_times in ⊢ (? (? ? (? ? %)) ?).
  98    apply (trans_le ? (((S(S O))*((S(S O))*((S n1)\sup((S(S O)))*((S(S O))*n1*((S(S O))*n1)!))))))
  99     [apply le_times_r.
 100      apply le_times_r.
 101      apply le_times_r.
 102      assumption
 103     |rewrite > factS.
 104      rewrite > factS.
 105      rewrite < times_SSO.
 106      rewrite > assoc_times in ⊢ (? ? %).
 107      apply le_times_r.
 108      rewrite < assoc_times.
 109      change in ⊢ (? (? (? ? %) ?) ?) with ((S n1)*((S n1)*(S O))).
 110      rewrite < assoc_times in ⊢ (? (? % ?) ?).
 111      rewrite < times_n_SO.
 112      rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?).
 113      rewrite < assoc_times in ⊢ (? ? %).
 114      rewrite < assoc_times in ⊢ (? ? (? % ?)).
 115      apply le_times_r.
 116      apply le_times_l.
 117      apply le_S.apply le_n
 118     ]
 119   ]
 120 qed.
 121
 122 theorem le_fact_10: fact (2*5) \le (exp 2 ((2*5)-2))*(fact 5)*(fact 5).
 123 simplify in \vdash (? (? %) ?).
 124 rewrite > factS in \vdash (? % ?).
 125 rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash(? % ?).
 126 rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash (? % ?).
 127 rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash (? % ?).
 128 rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash (? % ?).
 129 apply le_times_l.
 130 apply leb_true_to_le.reflexivity.
 131 qed.
 132
 133 theorem ab_times_cd: \forall a,b,c,d.(a*b)*(c*d)=(a*c)*(b*d).
 134 intros.
 135 rewrite > assoc_times.
 136 rewrite > assoc_times.
 137 apply eq_f.
 138 rewrite < assoc_times.
 139 rewrite < assoc_times.
 140 rewrite > sym_times in \vdash (? ? (? % ?) ?).
 141 reflexivity.
 142 qed.
 143
 144 (* an even better result *)
 145 theorem lt_SSSSO_to_fact: \forall n.4<n \to
 146 fact (2*n) \le (exp 2 ((2*n)-2))*(fact n)*(fact n).
 147 intros.elim H
 148   [apply le_fact_10
 149   |rewrite > times_SSO.
 150    change in \vdash (? ? (? (? (? ? %) ?) ?)) with (2*n1 - O);
 151    rewrite < minus_n_O.
 152    rewrite > factS.
 153    rewrite > factS.
 154    rewrite < assoc_times.
 155    rewrite > factS.
 156    apply (trans_le ? ((2*(S n1))*(2*(S n1))*(fact (2*n1))))
 157     [apply le_times_l.
 158      rewrite > times_SSO.
 159      apply le_times_r.
 160      apply le_n_Sn
 161     |apply (trans_le ? (2*S n1*(2*S n1)*(2\sup(2*n1-2)*n1!*n1!)))
 162       [apply le_times_r.assumption
 163       |rewrite > assoc_times.
 164        rewrite > ab_times_cd in \vdash (? (? ? %) ?).
 165        rewrite < assoc_times.
 166        apply le_times_l.
 167        rewrite < assoc_times in \vdash (? (? ? %) ?).
 168        rewrite > ab_times_cd.
 169        apply le_times_l.
 170        rewrite < exp_S.
 171        rewrite < exp_S.
 172        apply le_exp
 173         [apply lt_O_S
 174         |rewrite > eq_minus_S_pred.
 175          rewrite < S_pred
 176           [rewrite > eq_minus_S_pred.
 177            rewrite < S_pred
 178             [rewrite < minus_n_O.
 179              apply le_n
 180             |elim H1;simplify
 181               [apply lt_O_S
 182               |apply lt_O_S
 183               ]
 184             ]
 185           |elim H1;simplify
 186             [apply lt_O_S
 187             |rewrite < plus_n_Sm.
 188              rewrite < minus_n_O.
 189              apply lt_O_S
 190             ]
 191           ]
 192         ]
 193       ]
 194     ]
 195   ]
 196 qed. *)