helm/software/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 include "nat/iteration2.ma".
  22 include "nat/div_and_mod_diseq.ma".
  23
  24 definition log \def \lambda p,n.
  25 max n (\lambda x.leb (exp p x) n).
  26
  27 theorem le_exp_log: \forall p,n. O < n \to
  28 exp p (log p n) \le n.
  29 intros.
  30 apply leb_true_to_le.
  31 unfold log.
  32 apply (f_max_true (\lambda x.leb (exp p x) n)).
  33 apply (ex_intro ? ? O).
  34 split
  35   [apply le_O_n
  36   |apply le_to_leb_true.simplify.assumption
  37   ]
  38 qed.
  39
  40 theorem log_SO: \forall n. S O < n \to log n (S O) = O.
  41 intros.
  42 apply sym_eq.apply le_n_O_to_eq.
  43 apply (le_exp_to_le n)
  44   [assumption
  45   |simplify in ⊢ (? ? %).
  46    apply le_exp_log.
  47    apply le_n
  48   ]
  49 qed.
  50
  51 theorem lt_to_log_O: \forall n,m. O < m \to m < n \to log n m = O.
  52 intros.
  53 apply sym_eq.apply le_n_O_to_eq.
  54 apply le_S_S_to_le.
  55 apply (lt_exp_to_lt n)
  56   [apply (le_to_lt_to_lt ? m);assumption
  57   |simplify in ⊢ (? ? %).
  58    rewrite < times_n_SO.
  59    apply (le_to_lt_to_lt ? m)
  60     [apply le_exp_log.assumption
  61     |assumption
  62     ]
  63   ]
  64 qed.
  65
  66 theorem lt_log_n_n: \forall p, n. S O < p \to O < n \to log p n < n.
  67 intros.
  68 cut (log p n \le n)
  69   [elim (le_to_or_lt_eq ? ? Hcut)
  70     [assumption
  71     |absurd (exp p n \le n)
  72       [rewrite < H2 in ⊢ (? (? ? %) ?).
  73        apply le_exp_log.
  74        assumption
  75       |apply lt_to_not_le.
  76        apply lt_m_exp_nm.
  77        assumption
  78       ]
  79     ]
  80   |unfold log.apply le_max_n
  81   ]
  82 qed.
  83
  84 theorem lt_O_log: \forall p,n. O < n \to p \le n \to O < log p n.
  85 intros.
  86 unfold log.
  87 apply not_lt_to_le.
  88 intro.
  89 apply (leb_false_to_not_le ? ? ? H1).
  90 rewrite > (exp_n_SO p).
  91 apply (lt_max_to_false ? ? ? H2).
  92 assumption.
  93 qed.
  94
  95 theorem le_log_n_n: \forall p,n. S O < p \to log p n \le n.
  96 intros.
  97 cases n
  98   [apply le_n
  99   |apply lt_to_le.
 100    apply lt_log_n_n
 101     [assumption|apply lt_O_S]
 102   ]
 103 qed.
 104
 105 theorem lt_exp_log: \forall p,n. S O < p \to n < exp p (S (log p n)).
 106 intros.cases n
 107   [simplify.rewrite < times_n_SO.apply lt_to_le.assumption
 108   |apply not_le_to_lt.
 109    apply leb_false_to_not_le.
 110    apply (lt_max_to_false ? (S n1) (S (log p (S n1))))
 111     [apply le_S_S.apply le_n
 112     |apply lt_log_n_n
 113       [assumption|apply lt_O_S]
 114     ]
 115   ]
 116 qed.
 117
 118 theorem log_times1: \forall p,n,m. S O < p \to O < n \to O < m \to
 119 log p (n*m) \le S(log p n+log p m).
 120 intros.
 121 unfold in ⊢ (? (% ? ?) ?).
 122 apply f_false_to_le_max
 123   [apply (ex_intro ? ? O).
 124    split
 125     [apply le_O_n
 126     |apply le_to_leb_true.
 127      simplify.
 128      rewrite > times_n_SO.
 129      apply le_times;assumption
 130     ]
 131   |intros.
 132    apply lt_to_leb_false.
 133    apply (lt_to_le_to_lt ? ((exp p (S(log p n)))*(exp p (S(log p m)))))
 134     [apply lt_times;apply lt_exp_log;assumption
 135     |rewrite < exp_plus_times.
 136      apply le_exp
 137       [apply lt_to_le.assumption
 138       |simplify.
 139        rewrite < plus_n_Sm.
 140        assumption
 141       ]
 142     ]
 143   ]
 144 qed.
 145
 146 theorem log_times: \forall p,n,m.S O < p \to log p (n*m) \le S(log p n+log p m).
 147 intros.
 148 cases n
 149   [apply le_O_n
 150   |cases m
 151     [rewrite < times_n_O.
 152      apply le_O_n
 153     |apply log_times1
 154       [assumption
 155       |apply lt_O_S
 156       |apply lt_O_S
 157       ]
 158     ]
 159   ]
 160 qed.
 161
 162 theorem log_times_l: \forall p,n,m.O < n \to O < m \to S O < p \to
 163 log p n+log p m \le log p (n*m) .
 164 intros.
 165 unfold log in ⊢ (? ? (% ? ?)).
 166 apply f_m_to_le_max
 167   [elim H
 168     [rewrite > log_SO
 169       [simplify.
 170        rewrite < plus_n_O.
 171        apply le_log_n_n.
 172        assumption
 173       |assumption
 174       ]
 175     |elim H1
 176       [rewrite > log_SO
 177         [rewrite < plus_n_O.
 178          rewrite < times_n_SO.
 179          apply le_log_n_n.
 180          assumption
 181         |assumption
 182         ]
 183       |apply (trans_le ? (S n1 + S n2))
 184         [apply le_plus;apply le_log_n_n;assumption
 185         |simplify.
 186          apply le_S_S.
 187          rewrite < plus_n_Sm.
 188          change in ⊢ (? % ?) with ((S n1)+n2).
 189          rewrite > sym_plus.
 190          apply le_plus_r.
 191          change with (n1 < n1*S n2).
 192          rewrite > times_n_SO in ⊢ (? % ?).
 193          apply lt_times_r1
 194           [assumption
 195           |apply le_S_S.assumption
 196           ]
 197         ]
 198       ]
 199     ]
 200   |apply le_to_leb_true.
 201    rewrite > exp_plus_times.
 202    apply le_times;apply le_exp_log;assumption
 203   ]
 204 qed.
 205
 206 theorem log_exp: \forall p,n,m.S O < p \to O < m \to
 207 log p ((exp p n)*m)=n+log p m.
 208 intros.
 209 unfold log in ⊢ (? ? (% ? ?) ?).
 210 apply max_spec_to_max.
 211 unfold max_spec.
 212 split
 213   [split
 214     [elim n
 215       [simplify.
 216        rewrite < plus_n_O.
 217        apply le_log_n_n.
 218        assumption
 219       |simplify.
 220        rewrite > assoc_times.
 221        apply (trans_le ? ((S(S O))*(p\sup n1*m)))
 222         [apply le_S_times_SSO
 223           [rewrite > (times_n_O O) in ⊢ (? % ?).
 224            apply lt_times
 225             [apply lt_O_exp.
 226              apply lt_to_le.
 227              assumption
 228             |assumption
 229             ]
 230           |assumption
 231           ]
 232         |apply le_times
 233           [assumption
 234           |apply le_n
 235           ]
 236         ]
 237       ]
 238     |simplify.
 239      apply le_to_leb_true.
 240      rewrite > exp_plus_times.
 241      apply le_times_r.
 242      apply le_exp_log.
 243      assumption
 244     ]
 245   |intros.
 246    simplify.
 247    apply lt_to_leb_false.
 248    apply (lt_to_le_to_lt ? ((exp p n)*(exp p (S(log p m)))))
 249     [apply lt_times_r1
 250       [apply lt_O_exp.apply lt_to_le.assumption
 251       |apply lt_exp_log.assumption
 252       ]
 253     |rewrite < exp_plus_times.
 254      apply le_exp
 255       [apply lt_to_le.assumption
 256       |rewrite < plus_n_Sm.
 257        assumption
 258       ]
 259     ]
 260   ]
 261 qed.
 262
 263 theorem eq_log_exp: \forall p,n.S O < p \to
 264 log p (exp p n)=n.
 265 intros.
 266 rewrite > times_n_SO in ⊢ (? ? (? ? %) ?).
 267 rewrite > log_exp
 268   [rewrite > log_SO
 269     [rewrite < plus_n_O.reflexivity
 270     |assumption
 271     ]
 272   |assumption
 273   |apply le_n
 274   ]
 275 qed.
 276
 277 theorem log_exp1: \forall p,n,m.S O < p \to
 278 log p (exp n m) \le m*S(log p n).
 279 intros.elim m
 280   [simplify in ⊢ (? (? ? %) ?).
 281    rewrite > log_SO
 282     [apply le_O_n
 283     |assumption
 284     ]
 285   |simplify.
 286    apply (trans_le ? (S (log p n+log p (n\sup n1))))
 287     [apply log_times.assumption
 288     |apply le_S_S.
 289      apply le_plus_r.
 290      assumption
 291     ]
 292   ]
 293 qed.
 294
 295 theorem log_exp2: \forall p,n,m.S O < p \to O < n \to
 296 m*(log p n) \le log p (exp n m).
 297 intros.
 298 apply le_S_S_to_le.
 299 apply (lt_exp_to_lt p)
 300   [assumption
 301   |rewrite > sym_times.
 302    rewrite < exp_exp_times.
 303    apply (le_to_lt_to_lt ? (exp n m))
 304     [elim m
 305       [simplify.apply le_n
 306       |simplify.apply le_times
 307         [apply le_exp_log.
 308          assumption
 309         |assumption
 310         ]
 311       ]
 312     |apply lt_exp_log.
 313      assumption
 314     ]
 315   ]
 316 qed.
 317
 318 lemma le_log_plus: \forall p,n.S O < p \to log p n \leq log p (S n).
 319 intros;apply (bool_elim ? (leb (p*(exp p n)) (S n)))
 320   [simplify;intro;rewrite > H1;simplify;apply (trans_le ? n)
 321     [apply le_log_n_n;assumption
 322     |apply le_n_Sn]
 323   |intro;unfold log;simplify;rewrite > H1;simplify;apply le_max_f_max_g;
 324    intros;apply le_to_leb_true;constructor 2;apply leb_true_to_le;assumption]
 325 qed.
 326
 327 theorem le_log: \forall p,n,m. S O < p \to n \le m \to
 328 log p n \le log p m.
 329 intros.elim H1
 330   [constructor 1
 331   |apply (trans_le ? ? ? H3);apply le_log_plus;assumption]
 332 qed.
 333
 334 theorem log_div: \forall p,n,m. S O < p \to O < m \to m \le n \to
 335 log p (n/m) \le log p n -log p m.
 336 intros.
 337 apply le_plus_to_minus_r.
 338 apply (trans_le ? (log p ((n/m)*m)))
 339   [apply log_times_l
 340     [apply le_times_to_le_div
 341       [assumption
 342       |rewrite < times_n_SO.
 343        assumption
 344       ]
 345     |assumption
 346     |assumption
 347     ]
 348   |apply le_log
 349     [assumption
 350     |rewrite > (div_mod n m) in ⊢ (? ? %)
 351       [apply le_plus_n_r
 352       |assumption
 353       ]
 354     ]
 355   ]
 356 qed.
 357
 358 theorem log_n_n: \forall n. S O < n \to log n n = S O.
 359 intros.
 360 rewrite > exp_n_SO in ⊢ (? ? (? ? %) ?).
 361 rewrite > times_n_SO in ⊢ (? ? (? ? %) ?).
 362 rewrite > log_exp
 363   [rewrite > log_SO
 364     [reflexivity
 365     |assumption
 366     ]
 367   |assumption
 368   |apply le_n
 369   ]
 370 qed.
 371
 372 theorem log_i_SSOn: \forall n,i. S O < n \to n < i \to i \le ((S(S O))*n) \to
 373 log i ((S(S O))*n) = S O.
 374 intros.
 375 apply antisymmetric_le
 376   [apply not_lt_to_le.intro.
 377    apply (lt_to_not_le ((S(S O)) * n) (exp i (S(S O))))
 378     [rewrite > exp_SSO.
 379      apply lt_times
 380       [apply (le_to_lt_to_lt ? n);assumption
 381       |assumption
 382       ]
 383     |apply (trans_le ? (exp i (log i ((S(S O))*n))))
 384       [apply le_exp
 385         [apply (ltn_to_ltO ? ? H1)
 386         |assumption
 387         ]
 388       |apply le_exp_log.
 389        rewrite > (times_n_O O) in ⊢ (? % ?).
 390        apply lt_times
 391         [apply lt_O_S
 392         |apply lt_to_le.assumption
 393         ]
 394       ]
 395     ]
 396   |apply (trans_le ? (log i i))
 397     [rewrite < (log_n_n i) in ⊢ (? % ?)
 398       [apply le_log
 399         [apply (trans_lt ? n);assumption
 400         |apply le_n
 401         ]
 402       |apply (trans_lt ? n);assumption
 403       ]
 404     |apply le_log
 405       [apply (trans_lt ? n);assumption
 406       |assumption
 407       ]
 408     ]
 409   ]
 410 qed.
 411
 412 theorem exp_n_O: \forall n. O < n \to exp O n = O.
 413 intros.apply (lt_O_n_elim ? H).intros.
 414 simplify.reflexivity.
 415 qed.
 416
 417 (*
 418 theorem tech1: \forall n,i.O < n \to
 419 (exp (S n) (S(S i)))/(exp n (S i)) \le ((exp n i) + (exp (S n) (S i)))/(exp n i).
 420 intros.
 421 simplify in ⊢ (? (? ? %) ?).
 422 rewrite < eq_div_div_div_times
 423   [apply monotonic_div
 424     [apply lt_O_exp.assumption
 425     |apply le_S_S_to_le.
 426      apply lt_times_to_lt_div.
 427      change in ⊢ (? % ?) with ((exp (S n) (S i)) + n*(exp (S n) (S i))).
 428
 429
 430   |apply (trans_le ? ((n)\sup(i)*(S n)\sup(S i)/(n)\sup(S i)))
 431     [apply le_times_div_div_times.
 432      apply lt_O_exp.assumption
 433     |apply le_times_to_le_div2
 434       [apply lt_O_exp.assumption
 435       |simplify.
 436
 437 theorem tech1: \forall a,b,n,m.O < m \to
 438 n/m \le b \to (a*n)/m \le a*b.
 439 intros.
 440 apply le_times_to_le_div2
 441   [assumption
 442   |
 443
 444 theorem tech2: \forall n,m. O < n \to
 445 (exp (S n) m) / (exp n m) \le (n + m)/n.
 446 intros.
 447 elim m
 448   [rewrite < plus_n_O.simplify.
 449    rewrite > div_n_n.apply le_n
 450   |apply le_times_to_le_div
 451     [assumption
 452     |apply (trans_le ? (n*(S n)\sup(S n1)/(n)\sup(S n1)))
 453       [apply le_times_div_div_times.
 454        apply lt_O_exp
 455       |simplify in ⊢ (? (? ? %) ?).
 456        rewrite > sym_times in ⊢ (? (? ? %) ?).
 457        rewrite < eq_div_div_div_times
 458         [apply le_times_to_le_div2
 459           [assumption
 460           |
 461
 462
 463 theorem le_log_sigma_p:\forall n,m,p. O < m \to S O < p \to
 464 log p (exp n m) \le sigma_p n (\lambda i.true) (\lambda i. (m / i)).
 465 intros.
 466 elim n
 467   [rewrite > exp_n_O
 468     [simplify.apply le_n
 469     |assumption
 470     ]
 471   |rewrite > true_to_sigma_p_Sn
 472     [apply (trans_le ? (m/n1+(log p (exp n1 m))))
 473       [
 474 *)