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 include "basics/core_notation/fact_1.ma".
  14
  15 let rec fact n ≝
  16   match n with
  17   [ O ⇒ 1
  18   | S m ⇒ fact m * S m].
  19
  20 interpretation "factorial" 'fact n = (fact n).
  21
  22 lemma factS: ∀n. (S n)! = (S n)*n!.
  23 #n >commutative_times // qed.
  24
  25 theorem le_1_fact : ∀n. 1 ≤ n!.
  26 #n (elim n) normalize /2 by lt_minus_to_plus/
  27 qed.
  28
  29 theorem le_2_fact : ∀n. 1 < n → 2 ≤ n!.
  30 #n (cases n)
  31   [#abs @False_ind /2/
  32   |#m normalize #le2 @(le_times 1 ? 2) //
  33   ]
  34 qed.
  35
  36 theorem le_n_fact_n: ∀n. n ≤ n!.
  37 #n (elim n) normalize //
  38 #n #Hind @(transitive_le ? (1*(S n))) // @le_times //
  39 qed.
  40
  41 theorem lt_n_fact_n: ∀n. 2 < n → n < n!.
  42 #n (cases n)
  43   [#H @False_ind /2/
  44   |#m #lt2 normalize @(lt_to_le_to_lt ? (2*(S m))) //
  45    @le_times // @le_2_fact /2 by lt_plus_to_lt_l/
  46 qed.
  47
  48 (* approximations *)
  49
  50 theorem fact_to_exp1: ∀n.O<n →
  51  (2*n)! ≤ (2^(pred (2*n))) * n! * n!.
  52 #n #posn (cut (∀i.2*(S i) = S(S(2*i)))) [//] #H (elim posn) //
  53 #n #posn #Hind @(transitive_le ? ((2*n)!*(2*(S n))*(2*(S n))))
  54   [>H normalize @le_times //
  55   |cut (pred (2*(S n)) = S(S(pred(2*n))))
  56     [>S_pred // @(le_times 1 ? 1) //] #H1
  57    cut (2^(pred (2*(S n))) = 2^(pred(2*n))*2*2)
  58     [>H1 >H1 //] #H2 >H2
  59    @(transitive_le ? ((2^(pred (2*n))) * n! * n! *(2*(S n))*(2*(S n))))
  60     [@le_times[@le_times //]//
  61     (* we generalize to hide the computational content *)
  62     |normalize in match ((S n)!); generalize in match (S n);
  63      #Sn generalize in match 2; #two //
  64     ]
  65   ]
  66 qed.
  67
  68 theorem fact_to_exp: ∀n.
  69  (2*n)! ≤ (2^(pred (2*n))) * n! * n!.
  70 #n (cases n) [normalize // |#n @fact_to_exp1 //]
  71 qed.
  72
  73 theorem exp_to_fact1: ∀n.O < n →
  74   2^(2*n)*n!*n! < (S(2*n))!.
  75 #n #posn (elim posn) [normalize //]
  76 #n #posn #Hind (cut (∀i.2*(S i) = S(S(2*i)))) [//] #H
  77 cut (2^(2*(S n)) = 2^(2*n)*2*2) [>H //] #H1 >H1
  78 @(le_to_lt_to_lt ? (2^(2*n)*n!*n!*(2*(S n))*(2*(S n))))
  79   [normalize in match ((S n)!); generalize in match (S n); #Sn
  80    generalize in match 2; #two //
  81   |cut ((S(2*(S n)))! = (S(2*n))!*(S(S(2*n)))*(S(S(S(2*n)))))
  82    [>H //] #H2 >H2 @lt_to_le_to_lt_times
  83      [@lt_to_le_to_lt_times //|>H // | //]
  84   ]
  85 qed.
  86
  87 (* a sligtly better result *)
  88 theorem exp_to_fact2: ∀n.O < n →
  89   (exp 2 (2*n))*(exp (fact n) 2) \le 2*n*fact (2*n).
  90 #n #posn elim posn
  91   [@le_n
  92   |#m #le1m #Hind
  93    cut (2*(S m) = S(S (2*m))) [normalize //] #H2 >H2 in ⊢ (?%?);
  94    >factS <times_exp
  95    whd in match (exp 2 (S(S ?))); >(commutative_times ? 2) >associative_times
  96    >associative_times in ⊢ (??%); @monotonic_le_times_r
  97    whd in match (exp 2 (S ?)); >(commutative_times ? 2) >associative_times
  98    @(transitive_le ? (2*((2*m*(2*m)!)*(S m)^2)))
  99     [@le_times [//] >commutative_times in ⊢ (?(??%)?); <associative_times
 100      @le_times [@Hind |@le_n]
 101     |>exp_2 <associative_times <associative_times >commutative_times in ⊢ (??%);
 102      @le_times [2:@le_n] >H2 >factS >commutative_times <associative_times
 103      @le_times //
 104     ]
 105   ]
 106 qed.
 107
 108 theorem le_fact_10: fact (2*5) ≤ (exp 2 ((2*5)-2))*(fact 5)*(fact 5).
 109 >factS in ⊢ (?%?); >factS in ⊢ (?%?); <associative_times in ⊢ (?%?);
 110 >factS in ⊢ (?%?); <associative_times in ⊢ (?%?);
 111 >factS in ⊢ (?%?); <associative_times in ⊢ (?%?);
 112 >factS in ⊢ (?%?); <associative_times in ⊢ (?%?);
 113 @le_times [2:%] @leb_true_to_le %
 114 qed-.
 115
 116 theorem ab_times_cd: ∀a,b,c,d.(a*b)*(c*d)=(a*c)*(b*d).
 117 //
 118 qed.
 119
 120 (* an even better result *)
 121 theorem lt_4_to_fact: ∀n.4<n →
 122   fact (2*n) ≤ (exp 2 ((2*n)-2))*(fact n)*(fact n).
 123 #n #ltn elim ltn
 124   [@le_fact_10
 125   |#m #lem #Hind
 126    cut (2*(S m) = S(S (2*m))) [normalize //] #H2 >H2
 127    whd in match (minus (S(S ?)) 2); <minus_n_O
 128    >factS >factS <associative_times >factS
 129    @(transitive_le ? ((2*(S m))*(2*(S m))*(fact (2*m))))
 130     [@le_times [2:@le_n] >H2 @le_times //
 131     |@(transitive_le ? (2*S m*(2*S m)*(2\sup(2*m-2)*m!*m!)))
 132       [@monotonic_le_times_r //
 133       |>associative_times >ab_times_cd in ⊢ (?(??%)?);
 134        <associative_times @le_times [2:@le_n]
 135        <associative_times in ⊢ (?(??%)?);
 136        >ab_times_cd @le_times [2:@le_n] >commutative_times
 137        >(commutative_times 2) @(le_exp (S(S ((2*m)-2)))) [//]
 138        >eq_minus_S_pred >S_pred
 139         [>eq_minus_S_pred >S_pred [<minus_n_O @le_n |elim lem //]
 140         |elim lem [//] #m0 #le5m0 #Hind
 141          normalize <plus_n_Sm //
 142         ]
 143       ]
 144     ]
 145   ]
 146 qed.