helm/software/matita/library/nat/o.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 include "nat/binomial.ma".
  16 include "nat/sqrt.ma".
  17
  18 theorem le_times_SSO_n_exp_SSO_n: \forall n.
  19 2*n \le exp 2 n.
  20 intro.cases n
  21   [apply le_O_n
  22   |elim n1
  23     [apply le_n
  24     |rewrite > times_SSO.
  25      change in ⊢ (? % ?) with (2 + (2*(S n2))).
  26      change in ⊢ (? ? %) with (exp 2 (S n2)+(exp 2 (S n2) + O)).
  27      rewrite < plus_n_O.
  28      apply le_plus
  29       [rewrite > exp_n_SO in ⊢ (? % ?).
  30        apply le_exp
  31         [apply lt_O_S
  32         |apply le_S_S.apply le_O_n
  33         ]
  34       |assumption
  35       ]
  36     ]
  37   ]
  38 qed.
  39
  40 theorem le_times_n_exp: \forall a,n. exp 2 a \le n \to
  41 exp 2 a*n \le exp 2 n.
  42 intros.elim H
  43   [rewrite < exp_plus_times.
  44    apply le_exp
  45     [apply lt_O_S
  46     |rewrite > plus_n_O in ⊢ (? (? ? %) ?).
  47      change in ⊢ (? % ?) with (2*a).
  48      apply le_times_SSO_n_exp_SSO_n
  49     ]
  50   |rewrite > sym_times.simplify.
  51    rewrite < plus_n_O.
  52    apply le_plus
  53     [apply (trans_le ? n1)
  54       [assumption
  55       |apply (trans_le ? (2*n1))
  56         [apply le_times_n.
  57          apply le_n_Sn
  58         |apply le_times_SSO_n_exp_SSO_n
  59         ]
  60       ]
  61     |rewrite > sym_times.
  62      assumption
  63     ]
  64   ]
  65 qed.
  66
  67 theorem lt_times_SSO_n_exp_SSO_n: \forall n. 2 < n \to
  68 2*n < exp 2 n.
  69 intros.elim H
  70   [apply leb_true_to_le.reflexivity.
  71   |rewrite > times_SSO.
  72    change in ⊢ (? % ?) with (2 + (2*n1)).
  73    simplify in ⊢ (? ? %).
  74    rewrite < plus_n_O.
  75    apply (lt_to_le_to_lt ? (2+(exp 2 n1)))
  76     [apply lt_plus_r.assumption
  77     |apply le_plus_l.
  78      rewrite > exp_n_SO in ⊢ (? % ?).
  79      apply le_exp
  80       [apply lt_O_S
  81       |apply (trans_le ? 3)
  82         [apply le_S_S.apply le_O_n
  83         |assumption
  84         ]
  85       ]
  86     ]
  87   ]
  88 qed.
  89
  90 theorem le_exp_n_SSO_exp_SSO_n:\forall n. 3 < n \to
  91 exp n 2 \le exp 2 n.
  92 intros.elim H
  93   [simplify.apply le_n
  94   |simplify.
  95    rewrite < plus_n_O.
  96    rewrite < times_n_SO.
  97    rewrite < times_n_Sm.
  98    rewrite < assoc_plus.
  99    rewrite < sym_plus.
 100    rewrite > plus_n_Sm.
 101    apply le_plus
 102     [rewrite < exp_SSO.
 103      assumption
 104     |rewrite > plus_n_O in ⊢ (? (? (? ? %)) ?).
 105      change in ⊢ (? (? %) ?) with (2*n1).
 106      apply lt_times_SSO_n_exp_SSO_n.
 107      apply lt_to_le.
 108      assumption
 109     ]
 110   ]
 111 qed.
 112
 113 (* a variant *)
 114 theorem le_exp_n_SSO_exp_SSO_n1:\forall n. S O < n \to
 115 exp (4*n) 2 \le exp 2 (3*n).
 116 intros.elim H
 117   [apply leb_true_to_le.reflexivity
 118   |cut (exp (S n1) 2 \le 3*(exp n1 2))
 119     [apply (trans_le ? (3*exp (4*n1) 2))
 120       [rewrite < times_exp.
 121        rewrite < times_exp.
 122        rewrite < assoc_times.
 123        rewrite > sym_times in ⊢ (? ? (? % ?)).
 124        rewrite > assoc_times.
 125        apply le_times_r.
 126        assumption
 127       |apply (trans_le ? (8*exp 2 (3*n1)))
 128         [apply le_times
 129           [apply leb_true_to_le.reflexivity
 130           |assumption
 131           ]
 132         |change in ⊢ (? (? % ?) ?) with (exp 2 3).
 133          rewrite < exp_plus_times.
 134          apply le_exp
 135           [apply lt_O_S
 136           |simplify.rewrite < plus_n_Sm.
 137            rewrite < plus_n_Sm.rewrite < plus_n_Sm.
 138            apply le_n
 139           ]
 140         ]
 141       ]
 142     |rewrite > exp_Sn_SSO.
 143      change in ⊢ (? ? %) with ((exp n1 2) + ((exp n1 2) + ((exp n1 2) + O))).
 144      rewrite < plus_n_O.
 145      rewrite > plus_n_SO.
 146      rewrite > assoc_plus.
 147      apply le_plus_r.
 148      apply le_plus
 149       [rewrite > exp_SSO.
 150        apply le_times_l.
 151        assumption
 152       |apply lt_O_exp.
 153        apply lt_to_le.assumption
 154       ]
 155     ]
 156   ]
 157 qed.
 158
 159 (* a strict version *)
 160 theorem lt_exp_n_SSO_exp_SSO_n:\forall n. 4 < n \to
 161 exp n 2 < exp 2 n.
 162 intros.elim H
 163   [apply leb_true_to_le.reflexivity.
 164   |simplify.
 165    rewrite < plus_n_O.
 166    rewrite < times_n_SO.
 167    rewrite < times_n_Sm.
 168    rewrite < assoc_plus.
 169    rewrite < sym_plus.
 170    rewrite > plus_n_Sm.
 171    apply (lt_to_le_to_lt ? ((exp 2 n1)+S (n1+n1)))
 172     [apply lt_plus_l.
 173      rewrite < exp_SSO.
 174      assumption
 175     |apply le_plus_r.
 176      rewrite > plus_n_O in ⊢ (? (? (? ? %)) ?).
 177      change in ⊢ (? (? %) ?) with (2*n1).
 178      apply lt_times_SSO_n_exp_SSO_n.
 179      apply lt_to_le.apply lt_to_le.
 180      assumption
 181     ]
 182   ]
 183 qed.
 184
 185 theorem le_times_exp_n_SSO_exp_SSO_n:\forall a,n. 1 < a \to 4*a \le n \to
 186 exp 2 a*exp n 2 \le exp 2 n.
 187 intros.elim H1
 188   [apply (trans_le ? ((exp 2 a)*(exp 2 (3*a))))
 189     [apply le_times_r.
 190      apply le_exp_n_SSO_exp_SSO_n1.
 191      assumption
 192     |rewrite < exp_plus_times.
 193      apply le_exp
 194       [apply lt_O_S
 195       |apply le_n
 196       ]
 197     ]
 198   |apply (trans_le ? ((exp 2 a)*(2*(exp n1 2))))
 199     [apply le_times_r.
 200      simplify.
 201      rewrite < times_n_SO.
 202      rewrite < sym_times.simplify.
 203      rewrite < plus_n_O.
 204      rewrite < assoc_plus.
 205      rewrite < sym_plus.
 206      rewrite > plus_n_Sm.
 207      apply le_plus_r.
 208      apply (trans_le ? (3*n1))
 209       [simplify.rewrite > plus_n_SO.
 210        rewrite > assoc_plus.
 211        apply le_plus_r.
 212        apply le_plus_r.
 213        rewrite < plus_n_O.
 214        apply (trans_le ? (4*2))
 215         [apply leb_true_to_le.reflexivity
 216         |apply (trans_le ? (4*a))
 217           [apply le_times_r.assumption
 218           |assumption
 219           ]
 220         ]
 221       |apply le_times_l.
 222        apply (trans_le ? (4*2))
 223         [apply leb_true_to_le.reflexivity
 224         |apply (trans_le ? (4*a))
 225           [apply le_times_r.assumption
 226           |assumption
 227           ]
 228         ]
 229       ]
 230     |rewrite < assoc_times.
 231      rewrite < sym_times in ⊢ (? (? % ?) ?).
 232      rewrite > assoc_times.
 233      change in ⊢ (? ? %) with (2*exp 2 n1).
 234      apply le_times_r.
 235      assumption
 236     ]
 237   ]
 238 qed.
 239
 240 (* the same for log and sqrt
 241 theorem le_times_log_sqrt:\forall a,n. 1 < a \to exp 2 (8*a) \le n \to
 242 exp 2 a*log 2 n \le sqrt n.
 243 intros.unfold sqrt.
 244 apply f_m_to_le_max
 245   [
 246   |apply le_to_leb_true.
 247    rewrite < exp_SSO.
 248    rewrite < times_exp.
 249    rewrite > exp_exp_times.
 250    apply (trans_le ? (exp 2 (log 2 n)))
 251     [apply le_times_exp_n_SSO_exp_SSO_n.
 252 *)
 253
 254
 255