1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
10
Require Import BinPos BinNat Nnat ZArith_base ROmega ZArithRing.
11
Require Export ZOdiv_def.
16
(** This file provides results about the Round-Toward-Zero Euclidean
17
division [ZOdiv_eucl], whose projections are [ZOdiv] and [ZOmod].
18
Definition of this division can be found in file [ZOdiv_def].
20
This division and the one defined in Zdiv agree only on positive
21
numbers. Otherwise, Zdiv performs Round-Toward-Bottom.
23
The current approach is compatible with the division of usual
24
programming languages such as Ocaml. In addition, it has nicer
25
properties with respect to opposite and other usual operations.
28
(** Since ZOdiv and Zdiv are not meant to be used concurrently,
29
we reuse the same notation. *)
31
Infix "/" := ZOdiv : Z_scope.
32
Infix "mod" := ZOmod (at level 40, no associativity) : Z_scope.
34
Infix "/" := Ndiv : N_scope.
35
Infix "mod" := Nmod (at level 40, no associativity) : N_scope.
37
(** Auxiliary results on the ad-hoc comparison [NPgeb]. *)
39
Lemma NPgeb_Zge : forall (n:N)(p:positive),
40
NPgeb n p = true -> Z_of_N n >= Zpos p.
42
destruct n as [|n]; simpl; intros.
44
red; simpl; destruct Pcompare; now auto.
47
Lemma NPgeb_Zlt : forall (n:N)(p:positive),
48
NPgeb n p = false -> Z_of_N n < Zpos p.
50
destruct n as [|n]; simpl; intros.
52
red; simpl; destruct Pcompare; now auto.
55
(** * Relation between division on N and on Z. *)
57
Lemma Ndiv_Z0div : forall a b:N,
58
Z_of_N (a/b) = (Z_of_N a / Z_of_N b).
61
destruct a; destruct b; simpl; auto.
62
unfold Ndiv, ZOdiv; simpl; destruct Pdiv_eucl; auto.
65
Lemma Nmod_Z0mod : forall a b:N,
66
Z_of_N (a mod b) = (Z_of_N a) mod (Z_of_N b).
69
destruct a; destruct b; simpl; auto.
70
unfold Nmod, ZOmod; simpl; destruct Pdiv_eucl; auto.
73
(** * Characterization of this euclidean division. *)
75
(** First, the usual equation [a=q*b+r]. Notice that [a mod 0]
76
has been chosen to be [a], so this equation holds even for [b=0].
79
Theorem N_div_mod_eq : forall a b,
80
a = (b * (Ndiv a b) + (Nmod a b))%N.
82
intros; generalize (Ndiv_eucl_correct a b).
83
unfold Ndiv, Nmod; destruct Ndiv_eucl; simpl.
84
intro H; rewrite H; rewrite Nmult_comm; auto.
87
Theorem ZO_div_mod_eq : forall a b,
88
a = b * (ZOdiv a b) + (ZOmod a b).
90
intros; generalize (ZOdiv_eucl_correct a b).
91
unfold ZOdiv, ZOmod; destruct ZOdiv_eucl; simpl.
92
intro H; rewrite H; rewrite Zmult_comm; auto.
95
(** Then, the inequalities constraining the remainder. *)
97
Theorem Pdiv_eucl_remainder : forall a b:positive,
98
Z_of_N (snd (Pdiv_eucl a b)) < Zpos b.
100
induction a; cbv beta iota delta [Pdiv_eucl]; fold Pdiv_eucl; cbv zeta.
101
intros b; generalize (IHa b); case Pdiv_eucl.
102
intros q1 r1 Hr1; simpl in Hr1.
103
case_eq (NPgeb (2*r1+1) b); intros; unfold snd.
105
apply NPgeb_Zlt; auto.
106
intros b; generalize (IHa b); case Pdiv_eucl.
107
intros q1 r1 Hr1; simpl in Hr1.
108
case_eq (NPgeb (2*r1) b); intros; unfold snd.
110
apply NPgeb_Zlt; auto.
111
destruct b; simpl; romega with *.
114
Theorem Nmod_lt : forall (a b:N), b<>0%N ->
117
destruct b as [ |b]; intro H; try solve [elim H;auto].
118
destruct a as [ |a]; try solve [compute;auto]; unfold Nmod, Ndiv_eucl.
119
generalize (Pdiv_eucl_remainder a b); destruct Pdiv_eucl; simpl.
123
(** The remainder is bounded by the divisor, in term of absolute values *)
125
Theorem ZOmod_lt : forall a b:Z, b<>0 ->
126
Zabs (a mod b) < Zabs b.
128
destruct b as [ |b|b]; intro H; try solve [elim H;auto];
129
destruct a as [ |a|a]; try solve [compute;auto]; unfold ZOmod, ZOdiv_eucl;
130
generalize (Pdiv_eucl_remainder a b); destruct Pdiv_eucl; simpl;
131
try rewrite Zabs_Zopp; rewrite Zabs_eq; auto; apply Z_of_N_le_0.
134
(** The sign of the remainder is the one of [a]. Due to the possible
135
nullity of [a], a general result is to be stated in the following form:
138
Theorem ZOmod_sgn : forall a b:Z,
139
0 <= Zsgn (a mod b) * Zsgn a.
141
destruct b as [ |b|b]; destruct a as [ |a|a]; simpl; auto with zarith;
142
unfold ZOmod, ZOdiv_eucl; destruct Pdiv_eucl;
143
simpl; destruct n0; simpl; auto with zarith.
146
(** This can also be said in a simplier way: *)
148
Theorem Zsgn_pos_iff : forall z, 0 <= Zsgn z <-> 0 <= z.
150
destruct z; simpl; intuition auto with zarith.
153
Theorem ZOmod_sgn2 : forall a b:Z,
156
intros; rewrite <-Zsgn_pos_iff, Zsgn_Zmult; apply ZOmod_sgn.
159
(** Reformulation of [ZOdiv_lt] and [ZOmod_sgn] in 2
160
then 4 particular cases. *)
162
Theorem ZOmod_lt_pos : forall a b:Z, 0<=a -> b<>0 ->
163
0 <= a mod b < Zabs b.
166
assert (0 <= a mod b).
167
generalize (ZOmod_sgn a b).
168
destruct (Zle_lt_or_eq 0 a H).
169
rewrite <- Zsgn_pos in H1; rewrite H1; romega with *.
170
subst a; simpl; auto.
171
generalize (ZOmod_lt a b H0); romega with *.
174
Theorem ZOmod_lt_neg : forall a b:Z, a<=0 -> b<>0 ->
175
-Zabs b < a mod b <= 0.
178
assert (a mod b <= 0).
179
generalize (ZOmod_sgn a b).
180
destruct (Zle_lt_or_eq a 0 H).
181
rewrite <- Zsgn_neg in H1; rewrite H1; romega with *.
182
subst a; simpl; auto.
183
generalize (ZOmod_lt a b H0); romega with *.
186
Theorem ZOmod_lt_pos_pos : forall a b:Z, 0<=a -> 0<b -> 0 <= a mod b < b.
188
intros; generalize (ZOmod_lt_pos a b); romega with *.
191
Theorem ZOmod_lt_pos_neg : forall a b:Z, 0<=a -> b<0 -> 0 <= a mod b < -b.
193
intros; generalize (ZOmod_lt_pos a b); romega with *.
196
Theorem ZOmod_lt_neg_pos : forall a b:Z, a<=0 -> 0<b -> -b < a mod b <= 0.
198
intros; generalize (ZOmod_lt_neg a b); romega with *.
201
Theorem ZOmod_lt_neg_neg : forall a b:Z, a<=0 -> b<0 -> b < a mod b <= 0.
203
intros; generalize (ZOmod_lt_neg a b); romega with *.
206
(** * Division and Opposite *)
208
(* The precise equalities that are invalid with "historic" Zdiv. *)
210
Theorem ZOdiv_opp_l : forall a b:Z, (-a)/b = -(a/b).
212
destruct a; destruct b; simpl; auto;
213
unfold ZOdiv, ZOdiv_eucl; destruct Pdiv_eucl; simpl; auto with zarith.
216
Theorem ZOdiv_opp_r : forall a b:Z, a/(-b) = -(a/b).
218
destruct a; destruct b; simpl; auto;
219
unfold ZOdiv, ZOdiv_eucl; destruct Pdiv_eucl; simpl; auto with zarith.
222
Theorem ZOmod_opp_l : forall a b:Z, (-a) mod b = -(a mod b).
224
destruct a; destruct b; simpl; auto;
225
unfold ZOmod, ZOdiv_eucl; destruct Pdiv_eucl; simpl; auto with zarith.
228
Theorem ZOmod_opp_r : forall a b:Z, a mod (-b) = a mod b.
230
destruct a; destruct b; simpl; auto;
231
unfold ZOmod, ZOdiv_eucl; destruct Pdiv_eucl; simpl; auto with zarith.
234
Theorem ZOdiv_opp_opp : forall a b:Z, (-a)/(-b) = a/b.
236
destruct a; destruct b; simpl; auto;
237
unfold ZOdiv, ZOdiv_eucl; destruct Pdiv_eucl; simpl; auto with zarith.
240
Theorem ZOmod_opp_opp : forall a b:Z, (-a) mod (-b) = -(a mod b).
242
destruct a; destruct b; simpl; auto;
243
unfold ZOmod, ZOdiv_eucl; destruct Pdiv_eucl; simpl; auto with zarith.
246
(** * Unicity results *)
248
Definition Remainder a b r :=
249
(0 <= a /\ 0 <= r < Zabs b) \/ (a <= 0 /\ -Zabs b < r <= 0).
251
Definition Remainder_alt a b r :=
252
Zabs r < Zabs b /\ 0 <= r * a.
254
Lemma Remainder_equiv : forall a b r,
255
Remainder a b r <-> Remainder_alt a b r.
257
unfold Remainder, Remainder_alt; intuition.
260
rewrite <-(Zmult_opp_opp).
261
apply Zmult_le_0_compat; romega.
262
assert (0 <= Zsgn r * Zsgn a) by (rewrite <-Zsgn_Zmult, Zsgn_pos_iff; auto).
263
destruct r; simpl Zsgn in *; romega with *.
266
Theorem ZOdiv_mod_unique_full:
267
forall a b q r, Remainder a b r ->
268
a = b*q + r -> q = a/b /\ r = a mod b.
270
destruct 1 as [(H,H0)|(H,H0)]; intros.
271
apply Zdiv.Zdiv_mod_unique with b; auto.
272
apply ZOmod_lt_pos; auto.
274
rewrite <- H1; apply ZO_div_mod_eq.
276
rewrite <- (Zopp_involutive a).
277
rewrite ZOdiv_opp_l, ZOmod_opp_l.
278
generalize (Zdiv.Zdiv_mod_unique b (-q) (-a/b) (-r) (-a mod b)).
279
generalize (ZOmod_lt_pos (-a) b).
280
rewrite <-ZO_div_mod_eq, <-Zopp_mult_distr_r, <-Zopp_plus_distr, <-H1.
284
Theorem ZOdiv_unique_full:
285
forall a b q r, Remainder a b r ->
286
a = b*q + r -> q = a/b.
288
intros; destruct (ZOdiv_mod_unique_full a b q r); auto.
291
Theorem ZOdiv_unique:
292
forall a b q r, 0 <= a -> 0 <= r < b ->
293
a = b*q + r -> q = a/b.
295
intros; eapply ZOdiv_unique_full; eauto.
299
Theorem ZOmod_unique_full:
300
forall a b q r, Remainder a b r ->
301
a = b*q + r -> r = a mod b.
303
intros; destruct (ZOdiv_mod_unique_full a b q r); auto.
306
Theorem ZOmod_unique:
307
forall a b q r, 0 <= a -> 0 <= r < b ->
308
a = b*q + r -> r = a mod b.
310
intros; eapply ZOmod_unique_full; eauto.
314
(** * Basic values of divisions and modulo. *)
316
Lemma ZOmod_0_l: forall a, 0 mod a = 0.
318
destruct a; simpl; auto.
321
Lemma ZOmod_0_r: forall a, a mod 0 = a.
323
destruct a; simpl; auto.
326
Lemma ZOdiv_0_l: forall a, 0/a = 0.
328
destruct a; simpl; auto.
331
Lemma ZOdiv_0_r: forall a, a/0 = 0.
333
destruct a; simpl; auto.
336
Lemma ZOmod_1_r: forall a, a mod 1 = 0.
338
intros; symmetry; apply ZOmod_unique_full with a; auto with zarith.
339
rewrite Remainder_equiv; red; simpl; auto with zarith.
342
Lemma ZOdiv_1_r: forall a, a/1 = a.
344
intros; symmetry; apply ZOdiv_unique_full with 0; auto with zarith.
345
rewrite Remainder_equiv; red; simpl; auto with zarith.
348
Hint Resolve ZOmod_0_l ZOmod_0_r ZOdiv_0_l ZOdiv_0_r ZOdiv_1_r ZOmod_1_r
351
Lemma ZOdiv_1_l: forall a, 1 < a -> 1/a = 0.
353
intros; symmetry; apply ZOdiv_unique with 1; auto with zarith.
356
Lemma ZOmod_1_l: forall a, 1 < a -> 1 mod a = 1.
358
intros; symmetry; apply ZOmod_unique with 0; auto with zarith.
361
Lemma ZO_div_same : forall a:Z, a<>0 -> a/a = 1.
363
intros; symmetry; apply ZOdiv_unique_full with 0; auto with *.
364
rewrite Remainder_equiv; red; simpl; romega with *.
367
Lemma ZO_mod_same : forall a, a mod a = 0.
369
destruct a; intros; symmetry.
371
apply ZOmod_unique with 1; auto with *; romega with *.
372
apply ZOmod_unique_full with 1; auto with *; red; romega with *.
375
Lemma ZO_mod_mult : forall a b, (a*b) mod b = 0.
377
intros a b; destruct (Z_eq_dec b 0) as [Hb|Hb].
378
subst; simpl; rewrite ZOmod_0_r; auto with zarith.
379
symmetry; apply ZOmod_unique_full with a; [ red; romega with * | ring ].
382
Lemma ZO_div_mult : forall a b:Z, b <> 0 -> (a*b)/b = a.
384
intros; symmetry; apply ZOdiv_unique_full with 0; auto with zarith;
385
[ red; romega with * | ring].
388
(** * Order results about ZOmod and ZOdiv *)
390
(* Division of positive numbers is positive. *)
392
Lemma ZO_div_pos: forall a b, 0 <= a -> 0 <= b -> 0 <= a/b.
395
destruct (Zle_lt_or_eq 0 b H0).
396
assert (H2:=ZOmod_lt_pos_pos a b H H1).
397
rewrite (ZO_div_mod_eq a b) in H.
398
destruct (Z_lt_le_dec (a/b) 0); auto.
399
assert (b*(a/b) <= -b).
400
replace (-b) with (b*-1); [ | ring].
401
apply Zmult_le_compat_l; auto with zarith.
403
subst b; rewrite ZOdiv_0_r; auto.
406
(** As soon as the divisor is greater or equal than 2,
407
the division is strictly decreasing. *)
409
Lemma ZO_div_lt : forall a b:Z, 0 < a -> 2 <= b -> a/b < a.
412
assert (Hb : 0 < b) by romega.
413
assert (H1 : 0 <= a/b) by (apply ZO_div_pos; auto with zarith).
414
assert (H2 : 0 <= a mod b < b) by (apply ZOmod_lt_pos_pos; auto with zarith).
415
destruct (Zle_lt_or_eq 0 (a/b) H1) as [H3|H3]; [ | rewrite <- H3; auto].
416
pattern a at 2; rewrite (ZO_div_mod_eq a b).
417
apply Zlt_le_trans with (2*(a/b)).
419
apply Zle_trans with (b*(a/b)).
420
apply Zmult_le_compat_r; auto.
424
(** A division of a small number by a bigger one yields zero. *)
426
Theorem ZOdiv_small: forall a b, 0 <= a < b -> a/b = 0.
428
intros a b H; apply sym_equal; apply ZOdiv_unique with a; auto with zarith.
431
(** Same situation, in term of modulo: *)
433
Theorem ZOmod_small: forall a n, 0 <= a < n -> a mod n = a.
435
intros a b H; apply sym_equal; apply ZOmod_unique with 0; auto with zarith.
438
(** [Zge] is compatible with a positive division. *)
440
Lemma ZO_div_monotone_pos : forall a b c:Z, 0<=c -> 0<=a<=b -> a/c <= b/c.
444
destruct (Zle_lt_or_eq 0 c H);
445
[ clear H | subst c; do 2 rewrite ZOdiv_0_r; auto].
446
generalize (ZO_div_mod_eq a c).
447
generalize (ZOmod_lt_pos_pos a c H0 H2).
448
generalize (ZO_div_mod_eq b c).
449
generalize (ZOmod_lt_pos_pos b c (Zle_trans _ _ _ H0 H1) H2).
451
elim (Z_le_gt_dec (a / c) (b / c)); auto with zarith.
455
replace (a-b) with (c * (a/c-b/c) + a mod c - b mod c) by
456
(symmetry; pattern a at 1; rewrite H5; pattern b at 1; rewrite H3; ring).
457
assert (c * (a / c - b / c) >= c * 1).
458
apply Zmult_ge_compat_l.
466
Lemma ZO_div_monotone : forall a b c, 0<=c -> a<=b -> a/c <= b/c.
469
destruct (Z_le_gt_dec 0 a).
470
apply ZO_div_monotone_pos; auto with zarith.
471
destruct (Z_le_gt_dec 0 b).
472
apply Zle_trans with 0.
475
rewrite <- ZOdiv_opp_l.
476
apply ZO_div_pos; auto with zarith.
477
apply ZO_div_pos; auto with zarith.
478
rewrite <-(Zopp_involutive a), (ZOdiv_opp_l (-a)).
479
rewrite <-(Zopp_involutive b), (ZOdiv_opp_l (-b)).
480
generalize (ZO_div_monotone_pos (-b) (-a) c H).
484
(** With our choice of division, rounding of (a/b) is always done toward zero: *)
486
Lemma ZO_mult_div_le : forall a b:Z, 0 <= a -> 0 <= b*(a/b) <= a.
489
destruct b as [ |b|b].
490
simpl; auto with zarith.
492
apply Zmult_le_0_compat; auto with zarith.
493
apply ZO_div_pos; auto with zarith.
494
generalize (ZO_div_mod_eq a (Zpos b)) (ZOmod_lt_pos_pos a (Zpos b) Ha); romega with *.
495
change (Zneg b) with (-Zpos b); rewrite ZOdiv_opp_r, Zmult_opp_opp.
497
apply Zmult_le_0_compat; auto with zarith.
498
apply ZO_div_pos; auto with zarith.
499
generalize (ZO_div_mod_eq a (Zpos b)) (ZOmod_lt_pos_pos a (Zpos b) Ha); romega with *.
502
Lemma ZO_mult_div_ge : forall a b:Z, a <= 0 -> a <= b*(a/b) <= 0.
505
destruct b as [ |b|b].
506
simpl; auto with zarith.
508
generalize (ZO_div_mod_eq a (Zpos b)) (ZOmod_lt_neg_pos a (Zpos b) Ha); romega with *.
509
apply Zle_left_rev; unfold Zplus.
510
rewrite Zopp_mult_distr_r, <-ZOdiv_opp_l.
511
apply Zmult_le_0_compat; auto with zarith.
512
apply ZO_div_pos; auto with zarith.
513
change (Zneg b) with (-Zpos b); rewrite ZOdiv_opp_r, Zmult_opp_opp.
515
generalize (ZO_div_mod_eq a (Zpos b)) (ZOmod_lt_neg_pos a (Zpos b) Ha); romega with *.
516
apply Zle_left_rev; unfold Zplus.
517
rewrite Zopp_mult_distr_r, <-ZOdiv_opp_l.
518
apply Zmult_le_0_compat; auto with zarith.
519
apply ZO_div_pos; auto with zarith.
522
(** The previous inequalities between [b*(a/b)] and [a] are exact
523
iff the modulo is zero. *)
525
Lemma ZO_div_exact_full_1 : forall a b:Z, a = b*(a/b) -> a mod b = 0.
527
intros; generalize (ZO_div_mod_eq a b); romega.
530
Lemma ZO_div_exact_full_2 : forall a b:Z, a mod b = 0 -> a = b*(a/b).
532
intros; generalize (ZO_div_mod_eq a b); romega.
535
(** A modulo cannot grow beyond its starting point. *)
537
Theorem ZOmod_le: forall a b, 0 <= a -> 0 <= b -> a mod b <= a.
540
destruct (Zle_lt_or_eq _ _ H2).
541
case (Zle_or_lt b a); intros H3.
542
case (ZOmod_lt_pos_pos a b); auto with zarith.
543
rewrite ZOmod_small; auto with zarith.
544
subst; rewrite ZOmod_0_r; auto with zarith.
547
(** Some additionnal inequalities about Zdiv. *)
549
Theorem ZOdiv_le_upper_bound:
550
forall a b q, 0 <= a -> 0 < b -> a <= q*b -> a/b <= q.
552
intros a b q H1 H2 H3.
553
apply Zmult_le_reg_r with b; auto with zarith.
554
apply Zle_trans with (2 := H3).
555
pattern a at 2; rewrite (ZO_div_mod_eq a b); auto with zarith.
556
rewrite (Zmult_comm b); case (ZOmod_lt_pos_pos a b); auto with zarith.
559
Theorem ZOdiv_lt_upper_bound:
560
forall a b q, 0 <= a -> 0 < b -> a < q*b -> a/b < q.
562
intros a b q H1 H2 H3.
563
apply Zmult_lt_reg_r with b; auto with zarith.
564
apply Zle_lt_trans with (2 := H3).
565
pattern a at 2; rewrite (ZO_div_mod_eq a b); auto with zarith.
566
rewrite (Zmult_comm b); case (ZOmod_lt_pos_pos a b); auto with zarith.
569
Theorem ZOdiv_le_lower_bound:
570
forall a b q, 0 <= a -> 0 < b -> q*b <= a -> q <= a/b.
572
intros a b q H1 H2 H3.
573
assert (q < a / b + 1); auto with zarith.
574
apply Zmult_lt_reg_r with b; auto with zarith.
575
apply Zle_lt_trans with (1 := H3).
576
pattern a at 1; rewrite (ZO_div_mod_eq a b); auto with zarith.
577
rewrite Zmult_plus_distr_l; rewrite (Zmult_comm b); case (ZOmod_lt_pos_pos a b);
581
Theorem ZOdiv_sgn: forall a b,
582
0 <= Zsgn (a/b) * Zsgn a * Zsgn b.
584
destruct a as [ |a|a]; destruct b as [ |b|b]; simpl; auto with zarith;
585
unfold ZOdiv; simpl; destruct Pdiv_eucl; simpl; destruct n; simpl; auto with zarith.
588
(** * Relations between usual operations and Zmod and Zdiv *)
590
(** First, a result that used to be always valid with Zdiv,
591
but must be restricted here.
592
For instance, now (9+(-5)*2) mod 2 = -1 <> 1 = 9 mod 2 *)
594
Lemma ZO_mod_plus : forall a b c:Z,
596
(a + b * c) mod c = a mod c.
598
intros; destruct (Z_eq_dec a 0) as [Ha|Ha].
599
subst; simpl; rewrite ZOmod_0_l; apply ZO_mod_mult.
600
intros; destruct (Z_eq_dec c 0) as [Hc|Hc].
601
subst; do 2 rewrite ZOmod_0_r; romega.
602
symmetry; apply ZOmod_unique_full with (a/c+b); auto with zarith.
603
rewrite Remainder_equiv; split.
604
apply ZOmod_lt; auto.
605
apply Zmult_le_0_reg_r with (a*a); eauto.
606
destruct a; simpl; auto with zarith.
607
replace ((a mod c)*(a+b*c)*(a*a)) with (((a mod c)*a)*((a+b*c)*a)) by ring.
608
apply Zmult_le_0_compat; auto.
610
rewrite Zmult_plus_distr_r, Zmult_comm.
611
generalize (ZO_div_mod_eq a c); romega.
614
Lemma ZO_div_plus : forall a b c:Z,
615
0 <= (a+b*c) * a -> c<>0 ->
616
(a + b * c) / c = a / c + b.
618
intros; destruct (Z_eq_dec a 0) as [Ha|Ha].
619
subst; simpl; apply ZO_div_mult; auto.
621
apply ZOdiv_unique_full with (a mod c); auto with zarith.
622
rewrite Remainder_equiv; split.
623
apply ZOmod_lt; auto.
624
apply Zmult_le_0_reg_r with (a*a); eauto.
625
destruct a; simpl; auto with zarith.
626
replace ((a mod c)*(a+b*c)*(a*a)) with (((a mod c)*a)*((a+b*c)*a)) by ring.
627
apply Zmult_le_0_compat; auto.
629
rewrite Zmult_plus_distr_r, Zmult_comm.
630
generalize (ZO_div_mod_eq a c); romega.
633
Theorem ZO_div_plus_l: forall a b c : Z,
634
0 <= (a*b+c)*c -> b<>0 ->
635
b<>0 -> (a * b + c) / b = a + c / b.
637
intros a b c; rewrite Zplus_comm; intros; rewrite ZO_div_plus;
638
try apply Zplus_comm; auto with zarith.
641
(** Cancellations. *)
643
Lemma ZOdiv_mult_cancel_r : forall a b c:Z,
644
c<>0 -> (a*c)/(b*c) = a/b.
647
destruct (Z_eq_dec b 0).
648
subst; simpl; do 2 rewrite ZOdiv_0_r; auto.
650
apply ZOdiv_unique_full with ((a mod b)*c); auto with zarith.
651
rewrite Remainder_equiv.
653
do 2 rewrite Zabs_Zmult.
654
apply Zmult_lt_compat_r.
656
apply ZOmod_lt; auto.
657
replace ((a mod b)*c*(a*c)) with (((a mod b)*a)*(c*c)) by ring.
658
apply Zmult_le_0_compat.
660
destruct c; simpl; auto with zarith.
661
pattern a at 1; rewrite (ZO_div_mod_eq a b); ring.
664
Lemma ZOdiv_mult_cancel_l : forall a b c:Z,
665
c<>0 -> (c*a)/(c*b) = a/b.
668
rewrite (Zmult_comm c a); rewrite (Zmult_comm c b).
669
apply ZOdiv_mult_cancel_r; auto.
672
Lemma ZOmult_mod_distr_l: forall a b c,
673
(c*a) mod (c*b) = c * (a mod b).
675
intros; destruct (Z_eq_dec c 0) as [Hc|Hc].
676
subst; simpl; rewrite ZOmod_0_r; auto.
677
destruct (Z_eq_dec b 0) as [Hb|Hb].
678
subst; repeat rewrite Zmult_0_r || rewrite ZOmod_0_r; auto.
680
contradict Hc; eapply Zmult_integral_l; eauto.
681
rewrite (Zplus_minus_eq _ _ _ (ZO_div_mod_eq (c*a) (c*b))).
682
rewrite (Zplus_minus_eq _ _ _ (ZO_div_mod_eq a b)).
683
rewrite ZOdiv_mult_cancel_l; auto with zarith.
687
Lemma ZOmult_mod_distr_r: forall a b c,
688
(a*c) mod (b*c) = (a mod b) * c.
690
intros; repeat rewrite (fun x => (Zmult_comm x c)).
691
apply ZOmult_mod_distr_l; auto.
694
(** Operations modulo. *)
696
Theorem ZOmod_mod: forall a n, (a mod n) mod n = a mod n.
699
generalize (ZOmod_sgn2 a n).
700
pattern a at 2 4; rewrite (ZO_div_mod_eq a n); auto with zarith.
701
rewrite Zplus_comm; rewrite (Zmult_comm n).
703
apply sym_equal; apply ZO_mod_plus; auto with zarith.
704
rewrite Zmult_comm; auto.
707
Theorem ZOmult_mod: forall a b n,
708
(a * b) mod n = ((a mod n) * (b mod n)) mod n.
711
generalize (Zmult_le_0_compat _ _ (ZOmod_sgn2 a n) (ZOmod_sgn2 b n)).
712
pattern a at 2 3; rewrite (ZO_div_mod_eq a n); auto with zarith.
713
pattern b at 2 3; rewrite (ZO_div_mod_eq b n); auto with zarith.
714
set (A:=a mod n); set (B:=b mod n); set (A':=a/n); set (B':=b/n).
715
replace (A*(n*A'+A)*(B*(n*B'+B))) with (((n*A' + A) * (n*B' + B))*(A*B))
717
replace ((n*A' + A) * (n*B' + B))
718
with (A*B + (A'*B+B'*A+n*A'*B')*n) by ring.
720
apply ZO_mod_plus; auto with zarith.
723
(** addition and modulo
725
Generally speaking, unlike with Zdiv, we don't have
726
(a+b) mod n = (a mod n + b mod n) mod n
728
For instance, take (8 + (-10)) mod 3 = -2 whereas
729
(8 mod 3 + (-10 mod 3)) mod 3 = 1. *)
731
Theorem ZOplus_mod: forall a b n,
733
(a + b) mod n = (a mod n + b mod n) mod n.
735
assert (forall a b n, 0<a -> 0<b ->
736
(a + b) mod n = (a mod n + b mod n) mod n).
738
assert (H : 0<=a+b) by (romega with * ); revert H.
739
pattern a at 1 2; rewrite (ZO_div_mod_eq a n); auto with zarith.
740
pattern b at 1 2; rewrite (ZO_div_mod_eq b n); auto with zarith.
741
replace ((n * (a / n) + a mod n) + (n * (b / n) + b mod n))
742
with ((a mod n + b mod n) + (a / n + b / n) * n) by ring.
744
apply ZO_mod_plus; auto with zarith.
745
apply Zmult_le_0_compat; auto with zarith.
746
apply Zplus_le_0_compat.
747
apply Zmult_le_reg_r with a; auto with zarith.
748
simpl; apply ZOmod_sgn2; auto.
749
apply Zmult_le_reg_r with b; auto with zarith.
750
simpl; apply ZOmod_sgn2; auto.
751
(* general situation *)
753
destruct (Z_eq_dec a 0).
754
subst; simpl; symmetry; apply ZOmod_mod.
755
destruct (Z_eq_dec b 0).
756
subst; simpl; do 2 rewrite Zplus_0_r; symmetry; apply ZOmod_mod.
757
assert (0<a /\ 0<b \/ a<0 /\ b<0).
758
destruct a; destruct b; simpl in *; intuition; romega with *.
761
rewrite <-(Zopp_involutive a), <-(Zopp_involutive b).
762
rewrite <- Zopp_plus_distr; rewrite ZOmod_opp_l.
763
rewrite (ZOmod_opp_l (-a)),(ZOmod_opp_l (-b)).
764
match goal with |- _ = (-?x+-?y) mod n =>
765
rewrite <-(Zopp_plus_distr x y), ZOmod_opp_l end.
766
f_equal; apply H; auto with zarith.
769
Lemma ZOplus_mod_idemp_l: forall a b n,
771
(a mod n + b) mod n = (a + b) mod n.
777
apply ZOplus_mod; auto.
778
destruct (Z_eq_dec a 0).
779
subst; rewrite ZOmod_0_l; auto.
780
destruct (Z_eq_dec b 0).
781
subst; rewrite Zmult_0_r; auto with zarith.
782
apply Zmult_le_reg_r with (a*b).
785
rewrite (Zmult_integral_l _ _ n1 Hab) in n0; auto with zarith.
788
replace (a mod n * b * (a*b)) with ((a mod n * a)*(b*b)) by ring.
789
apply Zmult_le_0_compat.
791
destruct b; simpl; auto with zarith.
794
Lemma ZOplus_mod_idemp_r: forall a b n,
796
(b + a mod n) mod n = (b + a) mod n.
799
rewrite Zplus_comm, (Zplus_comm b a).
800
apply ZOplus_mod_idemp_l; auto.
803
Lemma ZOmult_mod_idemp_l: forall a b n, (a mod n * b) mod n = (a * b) mod n.
805
intros; rewrite ZOmult_mod, ZOmod_mod, <- ZOmult_mod; auto.
808
Lemma ZOmult_mod_idemp_r: forall a b n, (b * (a mod n)) mod n = (b * a) mod n.
810
intros; rewrite ZOmult_mod, ZOmod_mod, <- ZOmult_mod; auto.
813
(** Unlike with Zdiv, the following result is true without restrictions. *)
815
Lemma ZOdiv_ZOdiv : forall a b c, (a/b)/c = a/(b*c).
817
(* particular case: a, b, c positive *)
818
assert (forall a b c, a>0 -> b>0 -> c>0 -> (a/b)/c = a/(b*c)).
819
intros a b c H H0 H1.
820
pattern a at 2;rewrite (ZO_div_mod_eq a b).
821
pattern (a/b) at 2;rewrite (ZO_div_mod_eq (a/b) c).
822
replace (b * (c * (a / b / c) + (a / b) mod c) + a mod b) with
823
((a / b / c)*(b * c) + (b * ((a / b) mod c) + a mod b)) by ring.
826
assert (H3: c <> 0) by auto with zarith;
827
rewrite (Zmult_integral_l _ _ H3 H2) in H0; auto with zarith.
828
assert (0<=a/b) by (apply (ZO_div_pos a b); auto with zarith).
829
assert (0<=a mod b < b) by (apply ZOmod_lt_pos_pos; auto with zarith).
830
assert (0<=(a/b) mod c < c) by
831
(apply ZOmod_lt_pos_pos; auto with zarith).
832
rewrite ZO_div_plus_l; auto with zarith.
833
rewrite (ZOdiv_small (b * ((a / b) mod c) + a mod b)).
836
apply Zplus_le_0_compat;auto with zarith.
837
apply Zle_lt_trans with (b * ((a / b) mod c) + (b-1)).
838
apply Zplus_le_compat;auto with zarith.
839
apply Zle_lt_trans with (b * (c-1) + (b - 1)).
840
apply Zplus_le_compat;auto with zarith.
841
replace (b * (c - 1) + (b - 1)) with (b*c-1);try ring;auto with zarith.
842
repeat (apply Zmult_le_0_compat || apply Zplus_le_0_compat); auto with zarith.
843
apply (ZO_div_pos (a/b) c); auto with zarith.
844
(* b c positive, a general *)
845
assert (forall a b c, b>0 -> c>0 -> (a/b)/c = a/(b*c)).
846
intros; destruct a as [ |a|a]; try reflexivity.
847
apply H; auto with zarith.
848
change (Zneg a) with (-Zpos a); repeat rewrite ZOdiv_opp_l.
849
f_equal; apply H; auto with zarith.
850
(* c positive, a b general *)
851
assert (forall a b c, c>0 -> (a/b)/c = a/(b*c)).
852
intros; destruct b as [ |b|b].
853
repeat rewrite ZOdiv_0_r; reflexivity.
854
apply H0; auto with zarith.
855
change (Zneg b) with (-Zpos b);
856
repeat (rewrite ZOdiv_opp_r || rewrite ZOdiv_opp_l || rewrite <- Zopp_mult_distr_l).
857
f_equal; apply H0; auto with zarith.
859
intros; destruct c as [ |c|c].
860
rewrite Zmult_0_r; repeat rewrite ZOdiv_0_r; reflexivity.
861
apply H1; auto with zarith.
862
change (Zneg c) with (-Zpos c);
863
rewrite <- Zopp_mult_distr_r; do 2 rewrite ZOdiv_opp_r.
864
f_equal; apply H1; auto with zarith.
867
(** A last inequality: *)
869
Theorem ZOdiv_mult_le:
870
forall a b c, 0<=a -> 0<=b -> 0<=c -> c*(a/b) <= (c*a)/b.
872
intros a b c Ha Hb Hc.
873
destruct (Zle_lt_or_eq _ _ Ha);
874
[ | subst; rewrite ZOdiv_0_l, Zmult_0_r, ZOdiv_0_l; auto].
875
destruct (Zle_lt_or_eq _ _ Hb);
876
[ | subst; rewrite ZOdiv_0_r, ZOdiv_0_r, Zmult_0_r; auto].
877
destruct (Zle_lt_or_eq _ _ Hc);
878
[ | subst; rewrite ZOdiv_0_l; auto].
879
case (ZOmod_lt_pos_pos a b); auto with zarith; intros Hu1 Hu2.
880
case (ZOmod_lt_pos_pos c b); auto with zarith; intros Hv1 Hv2.
881
apply Zmult_le_reg_r with b; auto with zarith.
882
rewrite <- Zmult_assoc.
883
replace (a / b * b) with (a - a mod b).
884
replace (c * a / b * b) with (c * a - (c * a) mod b).
885
rewrite Zmult_minus_distr_l.
886
unfold Zminus; apply Zplus_le_compat_l.
887
match goal with |- - ?X <= -?Y => assert (Y <= X); auto with zarith end.
888
apply Zle_trans with ((c mod b) * (a mod b)); auto with zarith.
889
rewrite ZOmult_mod; auto with zarith.
890
apply (ZOmod_le ((c mod b) * (a mod b)) b); auto with zarith.
891
apply Zmult_le_compat_r; auto with zarith.
892
apply (ZOmod_le c b); auto.
893
pattern (c * a) at 1; rewrite (ZO_div_mod_eq (c * a) b); try ring;
895
pattern a at 1; rewrite (ZO_div_mod_eq a b); try ring; auto with zarith.
898
(** ZOmod is related to divisibility (see more in Znumtheory) *)
900
Lemma ZOmod_divides : forall a b,
901
a mod b = 0 <-> exists c, a = b*c.
905
pattern a at 1; rewrite (ZO_div_mod_eq a b).
906
rewrite H; auto with zarith.
907
destruct H as [c Hc].
908
destruct (Z_eq_dec b 0).
909
subst b; simpl in *; subst a; auto.
911
apply ZOmod_unique_full with c; auto with zarith.
915
(** * Interaction with "historic" Zdiv *)
917
(** They agree at least on positive numbers: *)
919
Theorem ZOdiv_eucl_Zdiv_eucl_pos : forall a b:Z, 0 <= a -> 0 < b ->
920
a/b = Zdiv.Zdiv a b /\ a mod b = Zdiv.Zmod a b.
923
apply Zdiv.Zdiv_mod_unique with b.
924
apply ZOmod_lt_pos; auto with zarith.
925
rewrite Zabs_eq; auto with *; apply Zdiv.Z_mod_lt; auto with *.
926
rewrite <- Zdiv.Z_div_mod_eq; auto with *.
927
symmetry; apply ZO_div_mod_eq; auto with *.
930
Theorem ZOdiv_Zdiv_pos : forall a b, 0 <= a -> 0 <= b ->
934
destruct (Zle_lt_or_eq _ _ Hb).
935
generalize (ZOdiv_eucl_Zdiv_eucl_pos a b Ha H); intuition.
936
subst; rewrite ZOdiv_0_r, Zdiv.Zdiv_0_r; reflexivity.
939
Theorem ZOmod_Zmod_pos : forall a b, 0 <= a -> 0 < b ->
940
a mod b = Zdiv.Zmod a b.
942
intros a b Ha Hb; generalize (ZOdiv_eucl_Zdiv_eucl_pos a b Ha Hb);
946
(** Modulos are null at the same places *)
948
Theorem ZOmod_Zmod_zero : forall a b, b<>0 ->
949
(a mod b = 0 <-> Zdiv.Zmod a b = 0).
952
rewrite ZOmod_divides, Zdiv.Zmod_divides; intuition.
added
removed
theories/ZArith/ZOdiv.v
