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