helm/software/matita/library/nat/sqrt.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/nat/sqrt/".
  16
  17 include "nat/times.ma".
  18 include "nat/compare.ma".
  19 include "nat/log.ma".
  20
  21 definition sqrt \def
  22   \lambda n.max n (\lambda x.leb (x*x) n).
  23
  24 theorem le_sqrt_to_le_times_l : \forall m,n.n \leq sqrt m \to n*n \leq m.
  25 intros;apply (trans_le ? (sqrt m * sqrt m))
  26   [apply le_times;assumption
  27   |apply leb_true_to_le;apply (f_max_true (λx:nat.leb (x*x) m) m);
  28    apply (ex_intro ? ? O);split
  29      [apply le_O_n
  30      |simplify;reflexivity]]
  31 qed.
  32
  33 theorem lt_sqrt_to_le_times_l : \forall m,n.n < sqrt m \to n*n < m.
  34 intros;apply (trans_le ? (sqrt m * sqrt m))
  35   [apply (trans_le ? (S n * S n))
  36      [simplify in \vdash (? ? %);apply le_S_S;apply (trans_le ? (n * S n))
  37         [apply le_times_r;apply le_S;apply le_n
  38         |rewrite > sym_plus;rewrite > plus_n_O in \vdash (? % ?);
  39          apply le_plus_r;apply le_O_n]
  40      |apply le_times;assumption]
  41   |apply le_sqrt_to_le_times_l;apply le_n]
  42 qed.
  43
  44 theorem le_sqrt_to_le_times_r : \forall m,n.sqrt m < n \to m < n*n.
  45 intros;apply not_le_to_lt;intro;
  46 apply ((leb_false_to_not_le ? ?
  47            (lt_max_to_false (\lambda x.leb (x*x) m) m n H ?))
  48          H1);
  49 apply (trans_le ? ? ? ? H1);cases n
  50   [apply le_n
  51   |rewrite > times_n_SO in \vdash (? % ?);rewrite > sym_times;apply le_times
  52      [apply le_S_S;apply le_O_n
  53      |apply le_n]]
  54 qed.
  55
  56 lemma le_sqrt_n_n : \forall n.sqrt n \leq n.
  57 intro.unfold sqrt.apply le_max_n.
  58 qed.
  59
  60 lemma leq_sqrt_n : \forall n. sqrt n * sqrt n \leq n.
  61 intro;unfold sqrt;apply leb_true_to_le;apply f_max_true;apply (ex_intro ? ? O);
  62 split
  63   [apply le_O_n
  64   |simplify;reflexivity]
  65 qed.
  66
  67 alias num (instance 0) = "natural number".
  68 lemma le_sqrt_log_n : \forall n,b. 2 < b \to sqrt n * log b n \leq n.
  69 intros.
  70 apply (trans_le ? ? ? ? (leq_sqrt_n ?));
  71 apply le_times_r;unfold sqrt;
  72 apply f_m_to_le_max
  73   [apply le_log_n_n;apply lt_to_le;assumption
  74   |apply le_to_leb_true;elim (le_to_or_lt_eq ? ? (le_O_n n))
  75      [apply (trans_le ? (exp b (log b n)))
  76         [elim (log b n)
  77            [apply le_O_n
  78            |simplify in \vdash (? ? %);
  79            elim (le_to_or_lt_eq ? ? (le_O_n n1))
  80               [elim (le_to_or_lt_eq ? ? H3)
  81                  [apply (trans_le ? (3*(n1*n1)));
  82                     [simplify in \vdash (? % ?);rewrite > sym_times in \vdash (? % ?);
  83                      simplify in \vdash (? % ?);
  84                      simplify;rewrite > sym_plus;
  85                      rewrite > plus_n_Sm;rewrite > sym_plus in \vdash (? (? % ?) ?);
  86                      rewrite > assoc_plus;apply le_plus_r;
  87                      rewrite < plus_n_Sm;
  88                      rewrite < plus_n_O;
  89                      apply lt_plus;rewrite > times_n_SO in \vdash (? % ?);
  90                      apply lt_times_r1;assumption;
  91                     |apply le_times
  92                        [assumption
  93                        |assumption]]
  94                  |rewrite < H4;apply le_times
  95                     [apply lt_to_le;assumption
  96                     |apply lt_to_le;simplify;rewrite < times_n_SO;assumption]]
  97              |rewrite < H3;simplify;rewrite < times_n_SO;do 2 apply lt_to_le;assumption]]
  98         |simplify;apply le_exp_log;assumption]
  99      |rewrite < H1;simplify;apply le_n]]
 100 qed.