matita/matita/lib/arithmetics/div_and_mod.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "arithmetics/nat.ma".
  13
  14 let rec mod_aux p m n: nat ≝
  15 match p with
  16   [ O ⇒ m
  17   | S q ⇒ match (leb m n) with
  18     [ true ⇒ m
  19     | false ⇒ mod_aux q (m-(S n)) n]].
  20
  21 definition mod : nat → nat → nat ≝
  22 λn,m. match m with
  23   [ O ⇒ n
  24   | S p ⇒ mod_aux n n p].
  25
  26 interpretation "natural remainder" 'module x y = (mod x y).
  27
  28 let rec div_aux p m n : nat ≝
  29 match p with
  30   [ O ⇒ O
  31   | S q ⇒ match (leb m n) with
  32     [ true ⇒ O
  33     | false ⇒ S (div_aux q (m-(S n)) n)]].
  34
  35 definition div : nat → nat → nat ≝
  36 λn,m.match m with
  37   [ O ⇒ S n
  38   | S p ⇒ div_aux n n p].
  39
  40 interpretation "natural divide" 'divide x y = (div x y).
  41
  42 theorem le_mod_aux_m_m:
  43 ∀p,n,m. n ≤ p → mod_aux p n m ≤ m.
  44 #p (elim p)
  45 [ normalize #n #m #lenO @(le_n_O_elim …lenO) //
  46 | #q #Hind #n #m #len normalize
  47     @(leb_elim n m) normalize //
  48     #notlenm @Hind @le_plus_to_minus
  49     @(transitive_le … len) /2/
  50 qed.
  51
  52 theorem lt_mod_m_m: ∀n,m. O < m → n \mod m  < m.
  53 #n #m (cases m)
  54   [#abs @False_ind /2/
  55   |#p #_ normalize @le_S_S /2/
  56   ]
  57 qed.
  58
  59 theorem div_aux_mod_aux: ∀p,n,m:nat.
  60 n=(div_aux p n m)*(S m) + (mod_aux p n m).
  61 #p (elim p)
  62   [#n #m normalize //
  63   |#q #Hind #n #m normalize
  64      @(leb_elim n m) #lenm normalize //
  65      >associative_plus <(Hind (n-(S m)) m)
  66      applyS plus_minus_m_m (* bello *) /2/
  67 qed.
  68
  69 theorem div_mod: ∀n,m:nat. n=(n / m)*m+(n \mod m).
  70 #n #m (cases m) normalize //
  71 qed.
  72
  73 theorem eq_times_div_minus_mod:
  74 ∀a,b:nat. (a / b) * b = a - (a \mod b).
  75 #a #b (applyS minus_plus_m_m) qed.
  76
  77 inductive div_mod_spec (n,m,q,r:nat) : Prop ≝
  78 div_mod_spec_intro: r < m → n=q*m+r → div_mod_spec n m q r.
  79
  80 theorem div_mod_spec_to_not_eq_O:
  81   ∀n,m,q,r.div_mod_spec n m q r → m ≠ O.
  82 #n #m #q #r * /2/
  83 qed.
  84
  85 theorem div_mod_spec_div_mod:
  86   ∀n,m. O < m → div_mod_spec n m (n / m) (n \mod m).
  87 #n #m #posm % /2/ qed.
  88
  89 theorem div_mod_spec_to_eq :∀ a,b,q,r,q1,r1.
  90 div_mod_spec a b q r → div_mod_spec a b q1 r1 → q = q1.
  91 #a #b #q #r #q1 #r1 * #ltrb #spec *  #ltr1b #spec1
  92 @(leb_elim q q1) #leqq1
  93   [(elim (le_to_or_lt_eq … leqq1)) //
  94      #ltqq1 @False_ind @(absurd ?? (not_le_Sn_n a))
  95      @(lt_to_le_to_lt ? ((S q)*b) ?)
  96       [>spec (applyS (monotonic_lt_plus_r … ltrb))
  97       |@(transitive_le ? (q1*b)) /2/
  98       ]
  99   (* this case is symmetric *)
 100   |@False_ind @(absurd ?? (not_le_Sn_n a))
 101      @(lt_to_le_to_lt ? ((S q1)*b) ?)
 102       [>spec1 (applyS (monotonic_lt_plus_r … ltr1b))
 103       |cut (q1 < q) [/2/] #ltq1q @(transitive_le ? (q*b)) /2/
 104       ]
 105   ]
 106 qed.
 107
 108 theorem div_mod_spec_to_eq2: ∀a,b,q,r,q1,r1.
 109   div_mod_spec a b q r → div_mod_spec a b q1 r1 → r = r1.
 110 #a #b #q #r #q1 #r1 #spec #spec1
 111 cut (q=q1) [@(div_mod_spec_to_eq … spec spec1)]
 112 #eqq (elim spec) #_ #eqa (elim spec1) #_ #eqa1
 113 @(injective_plus_r (q*b)) //
 114 qed.
 115
 116 (* boh
 117 theorem div_mod_spec_times : ∀ n,m:nat.div_mod_spec ((S n)*m) (S n) m O.
 118 intros.constructor 1.
 119 unfold lt.apply le_S_S.apply le_O_n. demodulate. reflexivity.
 120 (*rewrite < plus_n_O.rewrite < sym_times.reflexivity.*)
 121 qed. *)
 122
 123 lemma div_plus_times: ∀m,q,r:nat. r < m → (q*m+r)/ m = q.
 124 #m #q #r #ltrm
 125 @(div_mod_spec_to_eq … (div_mod_spec_div_mod ???)) /2/
 126 qed.
 127
 128 lemma mod_plus_times: ∀m,q,r:nat. r < m → (q*m+r) \mod m = r.
 129 #m #q #r #ltrm
 130 @(div_mod_spec_to_eq2 … (div_mod_spec_div_mod ???)) /2/
 131 qed.
 132
 133 (* some properties of div and mod *)
 134 theorem div_times: ∀a,b:nat. O < b → a*b/b = a.
 135 #a #b #posb
 136 @(div_mod_spec_to_eq (a*b) b … O (div_mod_spec_div_mod …))
 137 // @div_mod_spec_intro // qed.
 138
 139 (*
 140 theorem div_n_n: ∀n:nat. O < n → n / n = 1.
 141 /2/ qed.
 142
 143 theorem eq_div_O: ∀n,m. n < m → n / m = O.
 144 #n #m #ltnm
 145 @(div_mod_spec_to_eq n m (n/m) … n (div_mod_spec_div_mod …))
 146 /2/ qed.
 147
 148 theorem mod_n_n: ∀n:nat. O < n → n \mod n = O.
 149 #n #posn
 150 @(div_mod_spec_to_eq2 n n … 1 0 (div_mod_spec_div_mod …))
 151 /2/ qed. *)
 152
 153 theorem mod_S: ∀n,m:nat. O < m → S (n \mod m) < m →
 154 ((S n) \mod m) = S (n \mod m).
 155 #n #m #posm #H
 156 @(div_mod_spec_to_eq2 (S n) m … (n / m) ? (div_mod_spec_div_mod …))
 157 // @div_mod_spec_intro// (applyS eq_f) //
 158 qed.
 159
 160 theorem mod_O_n: ∀n:nat.O \mod n = O.
 161 /2/ qed.
 162
 163 theorem lt_to_eq_mod: ∀n,m:nat. n < m → n \mod m = n.
 164 #n #m #ltnm
 165 @(div_mod_spec_to_eq2 n m (n/m) … O n (div_mod_spec_div_mod …))
 166 /2/ qed.
 167
 168 (*
 169 theorem mod_1: ∀n:nat. mod n 1 = O.
 170 #n @sym_eq @le_n_O_to_eq
 171 @le_S_S_to_le /2/ qed.
 172
 173 theorem div_1: ∀n:nat. div n 1 = n.
 174 #n @sym_eq napplyS (div_mod n 1) qed. *)
 175
 176 theorem or_div_mod: ∀n,q. O < q →
 177   ((S (n \mod q)=q) ∧ S n = (S (div n q)) * q ∨
 178   ((S (n \mod q)<q) ∧ S n = (div n q) * q + S (n\mod q))).
 179 #n #q #posq
 180 (elim (le_to_or_lt_eq ?? (lt_mod_m_m n q posq))) #H
 181   [%2 % // (applyS eq_f) //
 182   |%1 % // /demod/ <H in ⊢(? ? ? (? % ?)) @eq_f//
 183   ]
 184 qed.
 185
 186 (* injectivity *)
 187 theorem injective_times_r:
 188   ∀n:nat. O < n → injective nat nat (λm:nat.n*m).
 189 #n #posn #a #b #eqn
 190 <(div_times a n posn) <(div_times b n posn) //
 191 qed.
 192
 193 theorem injective_times_l:
 194     ∀n:nat. O < n → injective nat nat (λm:nat.m*n).
 195 /2/ qed.
 196
 197 (* n_divides computes the pair (div,mod)
 198 (* p is just an upper bound, acc is an accumulator *)
 199 let rec n_divides_aux p n m acc \def
 200   match n \mod m with
 201   [ O \Rightarrow
 202     match p with
 203       [ O \Rightarrow pair nat nat acc n
 204       | (S p) \Rightarrow n_divides_aux p (n / m) m (S acc)]
 205   | (S a) \Rightarrow pair nat nat acc n].
 206
 207 (* n_divides n m = <q,r> if m divides n q times, with remainder r *)
 208 definition n_divides \def \lambda n,m:nat.n_divides_aux n n m O. *)
 209
 210 (* inequalities *)
 211
 212 theorem lt_div_S: ∀n,m. O < m → n < S(n / m)*m.
 213 #n #m #posm (change with (n < m +(n/m)*m))
 214 >(div_mod n m) in ⊢ (? % ?) >commutative_plus
 215 @monotonic_lt_plus_l @lt_mod_m_m //
 216 qed.
 217
 218 theorem le_div: ∀n,m. O < n → m/n ≤ m.
 219 #n #m #posn
 220 >(div_mod m n) in ⊢ (? ? %) @(transitive_le ? (m/n*n)) /2/
 221 qed.
 222
 223 theorem le_plus_mod: ∀m,n,q. O < q →
 224 (m+n) \mod q ≤ m \mod q + n \mod q .
 225 #m #n #q #posq
 226 (elim (decidable_le q (m \mod q + n \mod q))) #Hle
 227   [@(transitive_le … Hle) @le_S_S_to_le @le_S /2/
 228   |cut ((m+n)\mod q = m\mod q+n\mod q) //
 229      @(div_mod_spec_to_eq2 … (m/q + n/q) ? (div_mod_spec_div_mod … posq)).
 230      @div_mod_spec_intro
 231       [@not_le_to_lt //
 232       |>(div_mod n q) in ⊢ (? ? (? ? %) ?)
 233        (applyS (eq_f … (λx.plus x (n \mod q))))
 234        >(div_mod m q) in ⊢ (? ? (? % ?) ?)
 235        (applyS (eq_f … (λx.plus x (m \mod q)))) //
 236       ]
 237   ]
 238 qed.
 239
 240 theorem le_plus_div: ∀m,n,q. O < q →
 241   m/q + n/q \le (m+n)/q.
 242 #m #n #q #posq @(le_times_to_le … posq)
 243 @(le_plus_to_le_r ((m+n) \mod q))
 244 (* bruttino *)
 245 >commutative_times in ⊢ (? ? %) <div_mod
 246 >(div_mod m q) in ⊢ (? ? (? % ?)) >(div_mod n q) in ⊢ (? ? (? ? %))
 247 >commutative_plus in ⊢ (? ? (? % ?)) >associative_plus in ⊢ (? ? %)
 248 <associative_plus in ⊢ (? ? (? ? %)) (applyS monotonic_le_plus_l) /2/
 249 qed.
 250
 251 theorem le_times_to_le_div: ∀a,b,c:nat.
 252   O < b → b*c ≤ a → c ≤ a/b.
 253 #a #b #c #posb #Hle
 254 @le_S_S_to_le @(lt_times_n_to_lt_l b) @(le_to_lt_to_lt ? a)/2/
 255 qed.
 256
 257 theorem le_times_to_le_div2: ∀m,n,q. O < q →
 258   n ≤ m*q → n/q ≤ m.
 259 #m #n #q #posq #Hle
 260 @(le_times_to_le q ? ? posq) @(le_plus_to_le (n \mod q)) /2/
 261 qed.
 262
 263 (* da spostare
 264 theorem lt_m_nm: ∀n,m. O < m → 1 < n → m < n*m.
 265 /2/ qed. *)
 266
 267 theorem lt_times_to_lt_div: ∀m,n,q. n < m*q → n/q < m.
 268 #m #n #q #Hlt
 269 @(lt_times_n_to_lt_l q …) @(lt_plus_to_lt_l (n \mod q)) /2/
 270 qed.
 271
 272 (*
 273 theorem lt_div: ∀n,m. O < m → 1 < n → m/n < m.
 274 #n #m #posm #lt1n
 275 @lt_times_to_lt_div (applyS lt_m_nm) //.
 276 qed.
 277
 278 theorem le_div_plus_S: ∀m,n,q. O < q →
 279 (m+n)/q \le S(m/q + n/q).
 280 #m #n #q #posq
 281 @le_S_S_to_le @lt_times_to_lt_div
 282 @(lt_to_le_to_lt … (lt_plus … (lt_div_S m … posq) (lt_div_S n … posq)))
 283 //
 284 qed. *)
 285
 286 theorem le_div_S_S_div: ∀n,m. O < m → (S n)/m ≤ S (n /m).
 287 #n #m #posm @le_times_to_le_div2 /2/
 288 qed.
 289
 290 theorem le_times_div_div_times: ∀a,n,m.O < m →
 291 a*(n/m) ≤ a*n/m.
 292 #a #n #m #posm @le_times_to_le_div /2/
 293 qed.
 294
 295 theorem monotonic_div: ∀n.O < n →
 296   monotonic nat le (λm.div m n).
 297 #n #posn #a #b #leab @le_times_to_le_div/2/
 298 qed.
 299
 300 theorem pos_div: ∀n,m:nat. O < m → O < n → n \mod m = O →
 301   O < n / m.
 302 #n #m #posm #posn #mod0
 303 @(lt_times_n_to_lt_l m)// (* MITICO *)
 304 qed.
 305
 306 (*
 307 theorem lt_div_n_m_n: ∀n,m:nat. 1 < m → O < n → n / m < n.
 308 #n #m #ltm #posn
 309 @(leb_elim 1 (n / m))/2/ (* MITICO *)
 310 qed. *)
 311
 312 theorem eq_div_div_div_times: ∀n,m,q. O < n → O < m →
 313  q/n/m = q/(n*m).
 314 #n #m #q #posn #posm
 315 @(div_mod_spec_to_eq … (q\mod n+n*(q/n\mod m)) … (div_mod_spec_div_mod …)) /2/
 316 @div_mod_spec_intro // @(lt_to_le_to_lt ? (n*(S (q/n\mod m))))
 317   [(applyS monotonic_lt_plus_l) /2/
 318   |@monotonic_le_times_r/2/
 319   ]
 320 qed.
 321
 322 theorem eq_div_div_div_div: ∀n,m,q. O < n → O < m →
 323 q/n/m = q/m/n.
 324 #n #m #q #posn #posm
 325 @(trans_eq ? ? (q/(n*m)))
 326   [/2/
 327   |@sym_eq (applyS eq_div_div_div_times) //
 328   ]
 329 qed.
 330
 331 (*
 332 theorem SSO_mod: \forall n,m. O < m \to (S(S O))*n/m = (n/m)*(S(S O)) + mod ((S(S O))*n/m) (S(S O)).
 333 intros.
 334 rewrite < (lt_O_to_div_times n (S(S O))) in ⊢ (? ? ? (? (? (? % ?) ?) ?))
 335   [rewrite > eq_div_div_div_div
 336     [rewrite > sym_times in ⊢ (? ? ? (? (? (? (? % ?) ?) ?) ?)).
 337      apply div_mod.
 338      apply lt_O_S
 339     |apply lt_O_S
 340     |assumption
 341     ]
 342   |apply lt_O_S
 343   ]
 344 qed. *)
 345 (* Forall a,b : N. 0 < b \to b * (a/b) <= a < b * (a/b +1) *)
 346 (* The theorem is shown in two different parts: *)
 347 (*
 348 theorem lt_to_div_to_and_le_times_lt_S: \forall a,b,c:nat.
 349 O \lt b \to a/b = c \to (b*c \le a \land a \lt b*(S c)).
 350 intros.
 351 split
 352 [ rewrite < H1.
 353   rewrite > sym_times.
 354   rewrite > eq_times_div_minus_mod
 355   [ apply (le_minus_m a (a \mod b))
 356   | assumption
 357   ]
 358 | rewrite < (times_n_Sm b c).
 359   rewrite < H1.
 360   rewrite > sym_times.
 361   rewrite > (div_mod a b) in \vdash (? % ?)
 362   [ rewrite > (sym_plus b ((a/b)*b)).
 363     apply lt_plus_r.
 364     apply lt_mod_m_m.
 365     assumption
 366   | assumption
 367   ]
 368 ]
 369 qed. *)
 370
 371 theorem le_plus_to_minus_r: ∀a,b,c. a + b ≤ c → a ≤ c -b.
 372 #a #b #c #H @(le_plus_to_le_r … b) /2/
 373 qed.
 374
 375 theorem le_minus_to_plus_r: ∀a,b,c. c ≤ b → a ≤ b - c → a + c ≤ b.
 376 #a #b #c #Hlecb #H >(plus_minus_m_m … Hlecb) /2/
 377 qed.
 378
 379 theorem lt_minus_to_plus: ∀a,b,c. a - b < c → a < c + b.
 380 #a #b #c #H @not_le_to_lt
 381 @(not_to_not … (lt_to_not_le …H)) /2/
 382 qed.
 383
 384 theorem lt_minus_to_plus_r: ∀a,b,c. c ≤ a →
 385   a < b + c → a - c < b.
 386 #a #b #c #lea #H @not_le_to_lt
 387 @(not_to_not … (lt_to_not_le …H)) /2/
 388 qed.
 389
 390 theorem lt_to_le_times_to_lt_S_to_div: ∀a,c,b:nat.
 391 O < b → (b*c) ≤ a → a < (b*(S c)) → a/b = c.
 392 #a #c #b #posb#lea #lta
 393 @(div_mod_spec_to_eq … (a-b*c) (div_mod_spec_div_mod … posb …))
 394 @div_mod_spec_intro [@lt_minus_to_plus_r // |/2/]
 395 qed.
 396
 397 theorem div_times_times: ∀a,b,c:nat. O < c → O < b →
 398   (a/b) = (a*c)/(b*c).
 399 #a #b #c #posc #posb
 400 >(commutative_times b) <eq_div_div_div_times //
 401 >div_times //
 402 qed.
 403
 404 theorem times_mod: ∀a,b,c:nat.
 405 O < c → O < b → (a*c) \mod (b*c) = c*(a\mod b).
 406 #a #b #c #posc #posb
 407 @(div_mod_spec_to_eq2 (a*c) (b*c) (a/b) ((a*c) \mod (b*c)) (a/b) (c*(a \mod b)))
 408   [>(div_times_times … posc) // @div_mod_spec_div_mod /2/
 409   |@div_mod_spec_intro
 410     [(applyS monotonic_lt_times_l) /2/
 411     |(applyS (eq_f …(λx.x*c))) //
 412     ]
 413   ]
 414 qed.
 415
 416 theorem le_div_times_m: ∀a,i,m. O < i → O < m →
 417  (a * (m / i)) / m ≤ a / i.
 418 #a #i #m #posi #posm
 419 @(transitive_le ? ((a*m/i)/m))
 420   [@monotonic_div /2/
 421   |>eq_div_div_div_div // >div_times //
 422   ]
 423 qed.
 424
 425 (* serve ?
 426 theorem le_div_times_Sm: ∀a,i,m. O < i → O < m →
 427 a / i ≤ (a * S (m / i))/m.
 428 intros.
 429 apply (trans_le ? ((a * S (m/i))/((S (m/i))*i)))
 430   [rewrite < (eq_div_div_div_times ? i)
 431     [rewrite > lt_O_to_div_times
 432       [apply le_n
 433       |apply lt_O_S
 434       ]
 435     |apply lt_O_S
 436     |assumption
 437     ]
 438   |apply le_times_to_le_div
 439     [assumption
 440     |apply (trans_le ? (m*(a*S (m/i))/(S (m/i)*i)))
 441       [apply le_times_div_div_times.
 442        rewrite > (times_n_O O).
 443        apply lt_times
 444         [apply lt_O_S
 445         |assumption
 446         ]
 447       |rewrite > sym_times.
 448        apply le_times_to_le_div2
 449         [rewrite > (times_n_O O).
 450          apply lt_times
 451           [apply lt_O_S
 452           |assumption
 453           ]
 454         |apply le_times_r.
 455          apply lt_to_le.
 456          apply lt_div_S.
 457          assumption
 458         ]
 459       ]
 460     ]
 461   ]
 462 qed. *)