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