helm/software/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 set "baseuri" "cic:/matita/nat/div_and_mod_diseq".
  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. O < q \to
 187 n < m*q \to n/q < m.
 188 intros.
 189 apply (lt_times_to_lt q ? ? H).
 190 rewrite > sym_times.
 191 rewrite > sym_times in ⊢ (? ? %).
 192 apply (le_plus_to_le (n \mod q)).
 193 rewrite < plus_n_Sm.
 194 rewrite > sym_plus.
 195 rewrite < div_mod
 196   [apply (trans_le ? (m*q))
 197     [assumption
 198     |apply le_plus_n
 199     ]
 200   |assumption
 201   ]
 202 qed.
 203
 204 theorem lt_div: \forall n,m. O < m \to S O < n \to m/n < m.
 205 intros.
 206 apply lt_times_to_lt_div
 207   [apply lt_to_le. assumption
 208   |rewrite > sym_times.
 209    apply lt_m_nm;assumption
 210   ]
 211 qed.
 212
 213 theorem le_div_plus_S: \forall m,n,q. O < q \to
 214 (m+n)/q \le S(m/q + n/q).
 215 intros.
 216 apply le_S_S_to_le.
 217 apply lt_times_to_lt_div
 218   [assumption
 219   |change in ⊢ (? ? %) with (q + (q + (m/q+n/q)*q)).
 220    rewrite > sym_times.
 221    rewrite > distr_times_plus.
 222    rewrite > sym_times.
 223    rewrite < assoc_plus in ⊢ (? ? (? ? %)).
 224    rewrite < assoc_plus.
 225    rewrite > sym_plus in ⊢ (? ? (? % ?)).
 226    rewrite > assoc_plus.
 227    apply lt_plus
 228     [change with (m < S(m/q)*q).
 229      apply lt_div_S.
 230      assumption
 231     |rewrite > sym_times.
 232      change with (n < S(n/q)*q).
 233      apply lt_div_S.
 234      assumption
 235     ]
 236   ]
 237 qed.
 238
 239 theorem le_div_S_S_div: \forall n,m. O < m \to
 240 (S n)/m \le S (n /m).
 241 intros.
 242 apply le_times_to_le_div2
 243   [assumption
 244   |simplify.
 245    rewrite > (div_mod n m H) in ⊢ (? (? %) ?).
 246    rewrite > plus_n_Sm.
 247    rewrite > sym_plus.
 248    apply le_plus_l.
 249    apply lt_mod_m_m.
 250    assumption.
 251   ]
 252 qed.
 253
 254 theorem le_times_div_div_times: \forall a,n,m.O < m \to
 255 a*(n/m) \le a*n/m.
 256 intros.
 257 apply le_times_to_le_div
 258   [assumption
 259   |rewrite > sym_times.
 260    rewrite > assoc_times.
 261    apply le_times_r.
 262    rewrite > (div_mod n m H) in ⊢ (? ? %).
 263    apply le_plus_n_r.
 264   ]
 265 qed.
 266
 267 theorem monotonic_div: \forall n.O < n \to
 268 monotonic nat le (\lambda m.div m n).
 269 unfold monotonic.simplify.intros.
 270 apply le_times_to_le_div
 271   [assumption
 272   |apply (trans_le ? x)
 273     [rewrite > sym_times.
 274      rewrite > (div_mod x n H) in ⊢ (? ? %).
 275      apply le_plus_n_r
 276     |assumption
 277     ]
 278   ]
 279 qed.
 280
 281 theorem le_div_times_m: \forall a,i,m. O < i \to O < m \to
 282 (a * (m / i)) / m \le a / i.
 283 intros.
 284 apply (trans_le ? ((a*m/i)/m))
 285   [apply monotonic_div
 286     [assumption
 287     |apply le_times_div_div_times.
 288      assumption
 289     ]
 290   |rewrite > eq_div_div_div_times
 291     [rewrite > sym_times in ⊢ (? (? ? %) ?).
 292      rewrite < eq_div_div_div_times
 293       [apply monotonic_div
 294         [assumption
 295         |rewrite > lt_O_to_div_times
 296           [apply le_n
 297           |assumption
 298           ]
 299         ]
 300       |assumption
 301       |assumption
 302       ]
 303     |assumption
 304     |assumption
 305     ]
 306   ]
 307 qed.
 308
 309 theorem le_div_times_Sm: \forall a,i,m. O < i \to O < m \to
 310 a / i \le (a * S (m / i))/m.
 311 intros.
 312 apply (trans_le ? ((a * S (m / i))/((S (m/i))*i)))
 313   [rewrite < (eq_div_div_div_times ? i)
 314     [rewrite > lt_O_to_div_times
 315       [apply le_n
 316       |apply lt_O_S
 317       ]
 318     |apply lt_O_S
 319     |assumption
 320     ]
 321   |apply le_times_to_le_div
 322     [assumption
 323     |apply (trans_le ? (m*(a*S (m/i))/(S (m/i)*i)))
 324       [apply le_times_div_div_times.
 325        rewrite > (times_n_O O).
 326        apply lt_times
 327         [apply lt_O_S
 328         |assumption
 329         ]
 330       |rewrite > sym_times.
 331        apply le_times_to_le_div2
 332         [rewrite > (times_n_O O).
 333          apply lt_times
 334           [apply lt_O_S
 335           |assumption
 336           ]
 337         |apply le_times_r.
 338          apply lt_to_le.
 339          apply lt_div_S.
 340          assumption
 341         ]
 342       ]
 343     ]
 344   ]
 345 qed.
 346