matita/library/nat/div_and_mod_diseq.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/lt_arith.ma".
  16
  17 (* the proof that
  18      n \mod m < m,
  19    called lt_mod_m_m, is in div_and_mod.
  20 Other inequalities are also in lt_arith.ma.
  21 *)
  22
  23 theorem lt_div_S: \forall n,m. O < m \to
  24 n < S(n / m)*m.
  25 intros.
  26 change with (n < m +(n/m)*m).
  27 rewrite > sym_plus.
  28 rewrite > (div_mod n m H) in ⊢ (? % ?).
  29 apply lt_plus_r.
  30 apply lt_mod_m_m.
  31 assumption.
  32 qed.
  33
  34 theorem le_div: \forall n,m. O < n \to m/n \le m.
  35 intros.
  36 rewrite > (div_mod m n) in \vdash (? ? %)
  37   [apply (trans_le ? (m/n*n))
  38     [rewrite > times_n_SO in \vdash (? % ?).
  39      apply le_times
  40       [apply le_n|assumption]
  41     |apply le_plus_n_r
  42     ]
  43   |assumption
  44   ]
  45 qed.
  46
  47 theorem le_plus_mod: \forall m,n,q. O < q \to
  48 (m+n) \mod q \le m \mod q + n \mod q .
  49 intros.
  50 elim (decidable_le q (m \mod q + n \mod q))
  51   [apply not_lt_to_le.intro.
  52    apply (le_to_not_lt q q)
  53     [apply le_n
  54     |apply (le_to_lt_to_lt ? (m\mod q+n\mod q))
  55       [assumption
  56       |apply (trans_lt ? ((m+n)\mod q))
  57         [assumption
  58         |apply lt_mod_m_m.assumption
  59         ]
  60       ]
  61     ]
  62   |cut ((m+n)\mod q = m\mod q+n\mod q)
  63     [rewrite < Hcut.apply le_n
  64     |apply (div_mod_spec_to_eq2 (m+n) q ((m+n)/q) ((m+n) \mod q) (m/q + n/q))
  65       [apply div_mod_spec_div_mod.
  66        assumption
  67       |apply div_mod_spec_intro
  68         [apply not_le_to_lt.assumption
  69         |rewrite > (div_mod n q H) in ⊢ (? ? (? ? %) ?).
  70          rewrite < assoc_plus.
  71          rewrite < assoc_plus in ⊢ (? ? ? %).
  72          apply eq_f2
  73           [rewrite > (div_mod m q) in ⊢ (? ? (? % ?) ?)
  74             [rewrite > sym_times in ⊢ (? ? ? (? % ?)).
  75              rewrite > distr_times_plus.
  76              rewrite > sym_times in ⊢ (? ? ? (? (? % ?) ?)).
  77              rewrite > assoc_plus.
  78              rewrite > assoc_plus in ⊢ (? ? ? %).
  79              apply eq_f.
  80              rewrite > sym_plus.
  81              rewrite > sym_times.
  82              reflexivity
  83             |assumption
  84             ]
  85           |reflexivity
  86           ]
  87         ]
  88       ]
  89     ]
  90   ]
  91 qed.
  92
  93 theorem le_plus_div: \forall m,n,q. O < q \to
  94 m/q + n/q \le (m+n)/q.
  95 intros.
  96 apply (le_times_to_le q)
  97   [assumption
  98   |rewrite > distr_times_plus.
  99    rewrite > sym_times.
 100    rewrite > sym_times in ⊢ (? (? ? %) ?).
 101    rewrite > sym_times in ⊢ (? ? %).
 102    apply (le_plus_to_le ((m+n) \mod q)).
 103    rewrite > sym_plus in ⊢ (? ? %).
 104    rewrite < (div_mod ? ? H).
 105    rewrite > (div_mod n q H) in ⊢ (? ? (? ? %)).
 106    rewrite < assoc_plus.
 107    rewrite > sym_plus in ⊢ (? ? (? ? %)).
 108    rewrite < assoc_plus in ⊢ (? ? %).
 109    apply le_plus_l.
 110    rewrite > (div_mod m q H) in ⊢ (? ? (? % ?)).
 111    rewrite > assoc_plus.
 112    rewrite > sym_plus.
 113    apply le_plus_r.
 114    apply le_plus_mod.
 115    assumption
 116   ]
 117 qed.
 118
 119 theorem le_times_to_le_div: \forall a,b,c:nat.
 120 O \lt b \to (b*c) \le a \to c \le (a /b).
 121 intros.
 122 apply lt_S_to_le.
 123 apply (lt_times_n_to_lt b)
 124   [assumption
 125   |rewrite > sym_times.
 126    apply (le_to_lt_to_lt ? a)
 127     [assumption
 128     |simplify.
 129      rewrite > sym_plus.
 130      rewrite > (div_mod a b) in ⊢ (? % ?)
 131       [apply lt_plus_r.
 132        apply lt_mod_m_m.
 133        assumption
 134       |assumption
 135       ]
 136     ]
 137   ]
 138 qed.
 139
 140 theorem le_times_to_le_div2: \forall m,n,q. O < q \to
 141 n \le m*q \to n/q \le m.
 142 intros.
 143 apply (le_times_to_le q ? ? H).
 144 rewrite > sym_times.
 145 rewrite > sym_times in ⊢ (? ? %).
 146 apply (le_plus_to_le (n \mod q)).
 147 rewrite > sym_plus.
 148 rewrite < div_mod
 149   [apply (trans_le ? (m*q))
 150     [assumption
 151     |apply le_plus_n
 152     ]
 153   |assumption
 154   ]
 155 qed.
 156
 157 (* da spostare *)
 158 theorem lt_m_nm: \forall n,m. O < m \to S O < n \to
 159 m < n*m.
 160 intros.
 161 elim H1
 162   [simplify.rewrite < plus_n_O.
 163    rewrite > plus_n_O in ⊢ (? % ?).
 164    apply lt_plus_r.assumption
 165   |simplify.
 166    rewrite > plus_n_O in ⊢ (? % ?).
 167    rewrite > sym_plus.
 168    apply lt_plus
 169     [assumption
 170     |assumption
 171     ]
 172   ]
 173 qed.
 174
 175 theorem lt_times_to_lt: \forall i,n,m. O < i \to
 176 i * n < i * m \to n < m.
 177 intros.
 178 apply not_le_to_lt.intro.
 179 apply (lt_to_not_le ? ? H1).
 180 apply le_times_r.
 181 assumption.
 182 qed.
 183
 184 theorem lt_times_to_lt_div: \forall m,n,q. n < m*q \to n/q < m.
 185 intros.
 186 apply (lt_times_to_lt q ? ? (lt_times_to_lt_O ? ? ? H)).
 187 rewrite > sym_times.
 188 rewrite > sym_times in ⊢ (? ? %).
 189 apply (le_plus_to_le (n \mod q)).
 190 rewrite < plus_n_Sm.
 191 rewrite > sym_plus.
 192 rewrite < div_mod
 193   [apply (trans_le ? (m*q))
 194     [assumption
 195     |apply le_plus_n
 196     ]
 197   |apply (lt_times_to_lt_O ? ? ? H)
 198   ]
 199 qed.
 200
 201 theorem lt_div: \forall n,m. O < m \to S O < n \to m/n < m.
 202 intros.
 203 apply lt_times_to_lt_div.
 204 rewrite < sym_times.
 205 apply lt_m_nm;assumption.
 206 qed.
 207
 208 theorem le_div_plus_S: \forall m,n,q. O < q \to
 209 (m+n)/q \le S(m/q + n/q).
 210 intros.
 211 apply le_S_S_to_le.
 212 apply lt_times_to_lt_div.
 213 change in ⊢ (? ? %) with (q + (q + (m/q+n/q)*q)).
 214 rewrite > sym_times.
 215 rewrite > distr_times_plus.
 216 rewrite > sym_times.
 217 rewrite < assoc_plus in ⊢ (? ? (? ? %)).
 218 rewrite < assoc_plus.
 219 rewrite > sym_plus in ⊢ (? ? (? % ?)).
 220 rewrite > assoc_plus.
 221 apply lt_plus
 222   [change with (m < S(m/q)*q).
 223    apply lt_div_S.
 224    assumption
 225   |rewrite > sym_times.
 226    change with (n < S(n/q)*q).
 227    apply lt_div_S.
 228    assumption
 229   ]
 230 qed.
 231
 232 theorem le_div_S_S_div: \forall n,m. O < m \to
 233 (S n)/m \le S (n /m).
 234 intros.
 235 apply le_times_to_le_div2
 236   [assumption
 237   |simplify.
 238    rewrite > (div_mod n m H) in ⊢ (? (? %) ?).
 239    rewrite > plus_n_Sm.
 240    rewrite > sym_plus.
 241    apply le_plus_l.
 242    apply lt_mod_m_m.
 243    assumption.
 244   ]
 245 qed.
 246
 247 theorem le_times_div_div_times: \forall a,n,m.O < m \to
 248 a*(n/m) \le a*n/m.
 249 intros.
 250 apply le_times_to_le_div
 251   [assumption
 252   |rewrite > sym_times.
 253    rewrite > assoc_times.
 254    apply le_times_r.
 255    rewrite > (div_mod n m H) in ⊢ (? ? %).
 256    apply le_plus_n_r.
 257   ]
 258 qed.
 259
 260 theorem monotonic_div: \forall n.O < n \to
 261 monotonic nat le (\lambda m.div m n).
 262 unfold monotonic.simplify.intros.
 263 apply le_times_to_le_div
 264   [assumption
 265   |apply (trans_le ? x)
 266     [rewrite > sym_times.
 267      rewrite > (div_mod x n H) in ⊢ (? ? %).
 268      apply le_plus_n_r
 269     |assumption
 270     ]
 271   ]
 272 qed.
 273
 274 theorem le_div_times_m: \forall a,i,m. O < i \to O < m \to
 275 (a * (m / i)) / m \le a / i.
 276 intros.
 277 apply (trans_le ? ((a*m/i)/m))
 278   [apply monotonic_div
 279     [assumption
 280     |apply le_times_div_div_times.
 281      assumption
 282     ]
 283   |rewrite > eq_div_div_div_times
 284     [rewrite > sym_times in ⊢ (? (? ? %) ?).
 285      rewrite < eq_div_div_div_times
 286       [apply monotonic_div
 287         [assumption
 288         |rewrite > lt_O_to_div_times
 289           [apply le_n
 290           |assumption
 291           ]
 292         ]
 293       |assumption
 294       |assumption
 295       ]
 296     |assumption
 297     |assumption
 298     ]
 299   ]
 300 qed.
 301
 302 theorem le_div_times_Sm: \forall a,i,m. O < i \to O < m \to
 303 a / i \le (a * S (m / i))/m.
 304 intros.
 305 apply (trans_le ? ((a * S (m / i))/((S (m/i))*i)))
 306   [rewrite < (eq_div_div_div_times ? i)
 307     [rewrite > lt_O_to_div_times
 308       [apply le_n
 309       |apply lt_O_S
 310       ]
 311     |apply lt_O_S
 312     |assumption
 313     ]
 314   |apply le_times_to_le_div
 315     [assumption
 316     |apply (trans_le ? (m*(a*S (m/i))/(S (m/i)*i)))
 317       [apply le_times_div_div_times.
 318        rewrite > (times_n_O O).
 319        apply lt_times
 320         [apply lt_O_S
 321         |assumption
 322         ]
 323       |rewrite > sym_times.
 324        apply le_times_to_le_div2
 325         [rewrite > (times_n_O O).
 326          apply lt_times
 327           [apply lt_O_S
 328           |assumption
 329           ]
 330         |apply le_times_r.
 331          apply lt_to_le.
 332          apply lt_div_S.
 333          assumption
 334         ]
 335       ]
 336     ]
 337   ]
 338 qed.
 339