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 eq_sqrt: \forall n. sqrt (n*n) = n.
  25 intros.
  26 unfold sqrt.apply max_spec_to_max.
  27 unfold max_spec.split
  28   [split
  29     [cases n
  30       [apply le_n
  31       |rewrite > times_n_SO in ⊢ (? % ?).
  32        apply le_times_r.
  33        apply le_S_S.apply le_O_n
  34       ]
  35     |apply le_to_leb_true.apply le_n
  36     ]
  37   |intros.
  38    apply lt_to_leb_false.
  39    apply lt_times;assumption
  40   ]
  41 qed.
  42
  43 theorem le_sqrt_to_le_times_l : \forall m,n.n \leq sqrt m \to n*n \leq m.
  44 intros;apply (trans_le ? (sqrt m * sqrt m))
  45   [apply le_times;assumption
  46   |apply leb_true_to_le;apply (f_max_true (λx:nat.leb (x*x) m) m);
  47    apply (ex_intro ? ? O);split
  48      [apply le_O_n
  49      |simplify;reflexivity]]
  50 qed.
  51
  52 theorem lt_sqrt_to_le_times_l : \forall m,n.n < sqrt m \to n*n < m.
  53 intros;apply (trans_le ? (sqrt m * sqrt m))
  54   [apply (trans_le ? (S n * S n))
  55      [simplify in \vdash (? ? %);apply le_S_S;apply (trans_le ? (n * S n))
  56         [apply le_times_r;apply le_S;apply le_n
  57         |rewrite > sym_plus;rewrite > plus_n_O in \vdash (? % ?);
  58          apply le_plus_r;apply le_O_n]
  59      |apply le_times;assumption]
  60   |apply le_sqrt_to_le_times_l;apply le_n]
  61 qed.
  62
  63 theorem le_sqrt_to_le_times_r : \forall m,n.sqrt m < n \to m < n*n.
  64 intros;apply not_le_to_lt;intro;
  65 apply ((leb_false_to_not_le ? ?
  66            (lt_max_to_false (\lambda x.leb (x*x) m) m n H ?))
  67          H1);
  68 apply (trans_le ? ? ? ? H1);cases n
  69   [apply le_n
  70   |rewrite > times_n_SO in \vdash (? % ?);rewrite > sym_times;apply le_times
  71      [apply le_S_S;apply le_O_n
  72      |apply le_n]]
  73 qed.
  74
  75 lemma le_sqrt_n_n : \forall n.sqrt n \leq n.
  76 intro.unfold sqrt.apply le_max_n.
  77 qed.
  78
  79 lemma leq_sqrt_n : \forall n. sqrt n * sqrt n \leq n.
  80 intro;unfold sqrt;apply leb_true_to_le;apply f_max_true;apply (ex_intro ? ? O);
  81 split
  82   [apply le_O_n
  83   |simplify;reflexivity]
  84 qed.
  85
  86 alias num (instance 0) = "natural number".
  87
  88 lemma lt_sqrt_n : \forall n.1 < n \to sqrt n < n.
  89 intros.
  90 elim (le_to_or_lt_eq ? ? (le_sqrt_n_n n))
  91   [assumption
  92   |apply False_ind.
  93    apply (le_to_not_lt ? ? (leq_sqrt_n n)).
  94    rewrite > H1.
  95    rewrite > times_n_SO in ⊢ (? % ?).
  96    apply lt_times_r1
  97     [apply lt_to_le.assumption
  98     |assumption
  99     ]
 100   ]
 101 qed.
 102
 103 lemma lt_sqrt: \forall n.n < (exp (S (sqrt n)) 2).
 104 intro.
 105 cases n
 106   [apply le_n
 107   |cases n1
 108     [simplify.apply lt_to_le.apply lt_to_le.apply le_n
 109     |apply not_le_to_lt.
 110      apply leb_false_to_not_le.
 111      rewrite > exp_SSO.
 112      apply (lt_max_to_false (\lambda x.(leb (x*x) (S(S n2)))) (S(S n2)))
 113       [apply le_n
 114       |apply lt_sqrt_n.
 115        apply le_S_S.apply lt_O_S.
 116       ]
 117     ]
 118   ]
 119 qed.
 120
 121 lemma le_sqrt_n1: \forall n. n - 2*sqrt n \le exp (sqrt n) 2.
 122 intros.
 123 apply le_plus_to_minus.
 124 apply le_S_S_to_le.
 125 cut (S ((sqrt n)\sup 2+2*sqrt n) = (exp (S(sqrt n)) 2))
 126   [rewrite > Hcut.apply lt_sqrt
 127   |rewrite > exp_SSO.rewrite > exp_SSO.
 128    simplify.apply eq_f.
 129    rewrite < times_n_Sm.
 130    rewrite < plus_n_O.
 131    rewrite < assoc_plus in ⊢ (? ? ? %).
 132    rewrite > sym_plus.
 133    reflexivity
 134   ]
 135 qed.
 136
 137 (* falso per n=2, m=7 e n=3, m =15 *)
 138 lemma le_sqrt_nl: \forall n,m. 3 < n \to
 139 m*(pred m)*n \le exp (sqrt ((exp m 2)*n)) 2.
 140 intros.
 141 rewrite > minus_n_O in ⊢ (? (? (? ? (? %)) ?) ?).
 142 rewrite < eq_minus_S_pred.
 143 rewrite > distr_times_minus.
 144 rewrite < times_n_SO.
 145 rewrite > sym_times.
 146 rewrite > distr_times_minus.
 147 rewrite > sym_times.
 148 apply (trans_le ? (m*m*n -2*sqrt(m*m*n)))
 149   [apply monotonic_le_minus_r.
 150    apply (le_exp_to_le1 ? ? 2)
 151     [apply lt_O_S
 152     |rewrite < times_exp.
 153      apply (trans_le ? ((exp 2 2)*(m*m*n)))
 154       [apply le_times_r.
 155        rewrite > exp_SSO.
 156        apply leq_sqrt_n
 157       |rewrite < exp_SSO.
 158        rewrite < times_exp.
 159        rewrite < assoc_times.
 160        rewrite < sym_times in ⊢ (? (? % ?) ?).
 161        rewrite > assoc_times.
 162        rewrite > sym_times.
 163        apply le_times_l.
 164        rewrite > exp_SSO in ⊢ (? ? %).
 165        apply le_times_l.
 166        assumption
 167       ]
 168     ]
 169   |rewrite <exp_SSO.
 170    apply le_sqrt_n1
 171   ]
 172 qed.
 173
 174 lemma le_sqrt_log_n : \forall n,b. 2 < b \to sqrt n * log b n \leq n.
 175 intros.
 176 apply (trans_le ? ? ? ? (leq_sqrt_n ?));
 177 apply le_times_r;unfold sqrt;
 178 apply f_m_to_le_max
 179   [apply le_log_n_n;apply lt_to_le;assumption
 180   |apply le_to_leb_true;elim (le_to_or_lt_eq ? ? (le_O_n n))
 181      [apply (trans_le ? (exp b (log b n)))
 182         [elim (log b n)
 183            [apply le_O_n
 184            |simplify in \vdash (? ? %);
 185            elim (le_to_or_lt_eq ? ? (le_O_n n1))
 186               [elim (le_to_or_lt_eq ? ? H3)
 187                  [apply (trans_le ? (3*(n1*n1)));
 188                     [simplify in \vdash (? % ?);rewrite > sym_times in \vdash (? % ?);
 189                      simplify in \vdash (? % ?);
 190                      simplify;rewrite > sym_plus;
 191                      rewrite > plus_n_Sm;rewrite > sym_plus in \vdash (? (? % ?) ?);
 192                      rewrite > assoc_plus;apply le_plus_r;
 193                      rewrite < plus_n_Sm;
 194                      rewrite < plus_n_O;
 195                      apply lt_plus;rewrite > times_n_SO in \vdash (? % ?);
 196                      apply lt_times_r1;assumption;
 197                     |apply le_times
 198                        [assumption
 199                        |assumption]]
 200                  |rewrite < H4;apply le_times
 201                     [apply lt_to_le;assumption
 202                     |apply lt_to_le;simplify;rewrite < times_n_SO;assumption]]
 203              |rewrite < H3;simplify;rewrite < times_n_SO;do 2 apply lt_to_le;assumption]]
 204         |simplify;apply le_exp_log;assumption]
 205      |rewrite < H1;simplify;apply le_n]]
 206 qed.