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