matita/library/nat/log.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/log".
  16
  17 include "datatypes/constructors.ma".
  18 include "nat/minimization.ma".
  19 include "nat/relevant_equations.ma".
  20 include "nat/primes.ma".
  21
  22 definition log \def \lambda p,n.
  23 max n (\lambda x.leb (exp p x) n).
  24
  25 theorem le_exp_log: \forall p,n. O < n \to
  26 exp p (log p n) \le n.
  27 intros.
  28 apply leb_true_to_le.
  29 unfold log.
  30 apply (f_max_true (\lambda x.leb (exp p x) n)).
  31 apply (ex_intro ? ? O).
  32 split
  33   [apply le_O_n
  34   |apply le_to_leb_true.simplify.assumption
  35   ]
  36 qed.
  37
  38 theorem log_SO: \forall n. S O < n \to log n (S O) = O.
  39 intros.
  40 apply sym_eq.apply le_n_O_to_eq.
  41 apply (le_exp_to_le n)
  42   [assumption
  43   |simplify in ⊢ (? ? %).
  44    apply le_exp_log.
  45    apply le_n
  46   ]
  47 qed.
  48
  49 theorem lt_log_n_n: \forall p, n. S O < p \to O < n \to log p n < n.
  50 intros.
  51 cut (log p n \le n)
  52   [elim (le_to_or_lt_eq ? ? Hcut)
  53     [assumption
  54     |absurd (exp p n \le n)
  55       [rewrite < H2 in ⊢ (? (? ? %) ?).
  56        apply le_exp_log.
  57        assumption
  58       |apply lt_to_not_le.
  59        apply lt_m_exp_nm.
  60        assumption
  61       ]
  62     ]
  63   |unfold log.apply le_max_n
  64   ]
  65 qed.
  66
  67 theorem lt_O_log: \forall p,n. O < n \to p \le n \to O < log p n.
  68 intros.
  69 unfold log.
  70 apply not_lt_to_le.
  71 intro.
  72 apply (leb_false_to_not_le ? ? ? H1).
  73 rewrite > (exp_n_SO p).
  74 apply (lt_max_to_false ? ? ? H2).
  75 assumption.
  76 qed.
  77
  78 theorem le_log_n_n: \forall p,n. S O < p \to log p n \le n.
  79 intros.
  80 cases n
  81   [apply le_n
  82   |apply lt_to_le.
  83    apply lt_log_n_n
  84     [assumption|apply lt_O_S]
  85   ]
  86 qed.
  87
  88 theorem lt_exp_log: \forall p,n. S O < p \to n < exp p (S (log p n)).
  89 intros.cases n
  90   [simplify.rewrite < times_n_SO.apply lt_to_le.assumption
  91   |apply not_le_to_lt.
  92    apply leb_false_to_not_le.
  93    apply (lt_max_to_false ? (S n1) (S (log p (S n1))))
  94     [apply le_S_S.apply le_n
  95     |apply lt_log_n_n
  96       [assumption|apply lt_O_S]
  97     ]
  98   ]
  99 qed.
 100
 101 theorem log_times1: \forall p,n,m. S O < p \to O < n \to O < m \to
 102 log p (n*m) \le S(log p n+log p m).
 103 intros.
 104 unfold in ⊢ (? (% ? ?) ?).
 105 apply f_false_to_le_max
 106   [apply (ex_intro ? ? O).
 107    split
 108     [apply le_O_n
 109     |apply le_to_leb_true.
 110      simplify.
 111      rewrite > times_n_SO.
 112      apply le_times;assumption
 113     ]
 114   |intros.
 115    apply lt_to_leb_false.
 116    apply (lt_to_le_to_lt ? ((exp p (S(log p n)))*(exp p (S(log p m)))))
 117     [apply lt_times;apply lt_exp_log;assumption
 118     |rewrite < exp_plus_times.
 119      apply le_exp
 120       [apply lt_to_le.assumption
 121       |simplify.
 122        rewrite < plus_n_Sm.
 123        assumption
 124       ]
 125     ]
 126   ]
 127 qed.
 128
 129 theorem log_times: \forall p,n,m.S O < p \to log p (n*m) \le S(log p n+log p m).
 130 intros.
 131 cases n
 132   [apply le_O_n
 133   |cases m
 134     [rewrite < times_n_O.
 135      apply le_O_n
 136     |apply log_times1
 137       [assumption
 138       |apply lt_O_S
 139       |apply lt_O_S
 140       ]
 141     ]
 142   ]
 143 qed.
 144
 145 theorem log_exp: \forall p,n,m.S O < p \to O < m \to
 146 log p ((exp p n)*m)=n+log p m.
 147 intros.
 148 unfold log in ⊢ (? ? (% ? ?) ?).
 149 apply max_spec_to_max.
 150 unfold max_spec.
 151 split
 152   [split
 153     [elim n
 154       [simplify.
 155        rewrite < plus_n_O.
 156        apply le_log_n_n.
 157        assumption
 158       |simplify.
 159        rewrite > assoc_times.
 160        apply (trans_le ? ((S(S O))*(p\sup n1*m)))
 161         [apply le_S_times_SSO
 162           [rewrite > (times_n_O O) in ⊢ (? % ?).
 163            apply lt_times
 164             [apply lt_O_exp.
 165              apply lt_to_le.
 166              assumption
 167             |assumption
 168             ]
 169           |assumption
 170           ]
 171         |apply le_times
 172           [assumption
 173           |apply le_n
 174           ]
 175         ]
 176       ]
 177     |simplify.
 178      apply le_to_leb_true.
 179      rewrite > exp_plus_times.
 180      apply le_times_r.
 181      apply le_exp_log.
 182      assumption
 183     ]
 184   |intros.
 185    simplify.
 186    apply lt_to_leb_false.
 187    apply (lt_to_le_to_lt ? ((exp p n)*(exp p (S(log p m)))))
 188     [apply lt_times_r1
 189       [apply lt_O_exp.apply lt_to_le.assumption
 190       |apply lt_exp_log.assumption
 191       ]
 192     |rewrite < exp_plus_times.
 193      apply le_exp
 194       [apply lt_to_le.assumption
 195       |rewrite < plus_n_Sm.
 196        assumption
 197       ]
 198     ]
 199   ]
 200 qed.
 201
 202 theorem le_log: \forall p,n,m. S O < p \to O < n \to n \le m \to
 203 log p n \le log p m.
 204 intros.
 205 apply le_S_S_to_le.
 206 apply (lt_exp_to_lt p)
 207   [assumption
 208   |apply (le_to_lt_to_lt ? n)
 209     [apply le_exp_log.
 210      assumption
 211     |apply (le_to_lt_to_lt ? m)
 212       [assumption
 213       |apply lt_exp_log.
 214        assumption
 215       ]
 216     ]
 217   ]
 218 qed.
 219
 220 theorem log_n_n: \forall n. S O < n \to log n n = S O.
 221 intros.
 222 rewrite > exp_n_SO in ⊢ (? ? (? ? %) ?).
 223 rewrite > times_n_SO in ⊢ (? ? (? ? %) ?).
 224 rewrite > log_exp
 225   [rewrite > log_SO
 226     [reflexivity
 227     |assumption
 228     ]
 229   |assumption
 230   |apply le_n
 231   ]
 232 qed.
 233
 234 theorem log_i_SSOn: \forall n,i. S O < n \to n < i \to i \le ((S(S O))*n) \to
 235 log i ((S(S O))*n) = S O.
 236 intros.
 237 apply antisymmetric_le
 238   [apply not_lt_to_le.intro.
 239    apply (lt_to_not_le ((S(S O)) * n) (exp i (S(S O))))
 240     [rewrite > exp_SSO.
 241      apply lt_times
 242       [apply (le_to_lt_to_lt ? n);assumption
 243       |assumption
 244       ]
 245     |apply (trans_le ? (exp i (log i ((S(S O))*n))))
 246       [apply le_exp
 247         [apply (ltn_to_ltO ? ? H1)
 248         |assumption
 249         ]
 250       |apply le_exp_log.
 251        rewrite > (times_n_O O) in ⊢ (? % ?).
 252        apply lt_times
 253         [apply lt_O_S
 254         |apply lt_to_le.assumption
 255         ]
 256       ]
 257     ]
 258   |apply (trans_le ? (log i i))
 259     [rewrite < (log_n_n i) in ⊢ (? % ?)
 260       [apply le_log
 261         [apply (trans_lt ? n);assumption
 262         |apply (ltn_to_ltO ? ? H1)
 263         |apply le_n
 264         ]
 265       |apply (trans_lt ? n);assumption
 266       ]
 267     |apply le_log
 268       [apply (trans_lt ? n);assumption
 269       |apply (ltn_to_ltO ? ? H1)
 270       |assumption
 271       ]
 272     ]
 273   ]
 274 qed.