aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
Diffstat (limited to 'theories')
-rw-r--r--theories/Numbers/Integer/Abstract/ZAxioms.v6
-rw-r--r--theories/Numbers/Integer/Abstract/ZDivTrunc.v2
-rw-r--r--theories/Numbers/Integer/BigZ/BigZ.v3
-rw-r--r--theories/Numbers/Integer/BigZ/ZMake.v8
-rw-r--r--theories/Numbers/Integer/Binary/ZBinary.v2
-rw-r--r--theories/Numbers/Integer/SpecViaZ/ZSig.v4
-rw-r--r--theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v13
-rw-r--r--theories/ZArith/Zdiv_def.v21
-rw-r--r--theories/ZArith/Zquot.v87
9 files changed, 67 insertions, 79 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index 89fa8e170..f177755fa 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -88,19 +88,19 @@ Module Type ZDiv' (Z:ZAxiomsMiniSig) := NZDiv.NZDiv' Z <+ ZDivSpecific Z.
*)
Module Type QuotRem (Import A : Typ).
- Parameters Inline quot remainder : t -> t -> t.
+ Parameters Inline quot rem : t -> t -> t.
End QuotRem.
Module Type QuotRemNotation (A : Typ)(Import B : QuotRem A).
Infix "÷" := quot (at level 40, left associativity).
- Infix "rem" := remainder (at level 40, no associativity).
+ Infix "rem" := rem (at level 40, no associativity).
End QuotRemNotation.
Module Type QuotRem' (A : Typ) := QuotRem A <+ QuotRemNotation A.
Module Type QuotRemSpec (Import A : ZAxiomsMiniSig')(Import B : QuotRem' A).
Declare Instance quot_wd : Proper (eq==>eq==>eq) quot.
- Declare Instance rem_wd : Proper (eq==>eq==>eq) remainder.
+ Declare Instance rem_wd : Proper (eq==>eq==>eq) B.rem.
Axiom quot_rem : forall a b, b ~= 0 -> a == b*(a÷b) + (a rem b).
Axiom rem_bound_pos : forall a b, 0<=a -> 0<b -> 0 <= a rem b < b.
Axiom rem_opp_l : forall a b, b ~= 0 -> (-a) rem b == - (a rem b).
diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
index 37a0057ed..e33265762 100644
--- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v
+++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
@@ -35,7 +35,7 @@ Module Type ZQuotProp
Module Quot2Div <: NZDiv A.
Definition div := quot.
- Definition modulo := remainder.
+ Definition modulo := A.rem.
Definition div_wd := quot_wd.
Definition mod_wd := rem_wd.
Definition div_mod := quot_rem.
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index 72137eccf..6153ccc75 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -65,7 +65,7 @@ Arguments Scope BigZ.sqrt [bigZ_scope].
Arguments Scope BigZ.div_eucl [bigZ_scope bigZ_scope].
Arguments Scope BigZ.modulo [bigZ_scope bigZ_scope].
Arguments Scope BigZ.quot [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.remainder [bigZ_scope bigZ_scope].
+Arguments Scope BigZ.rem [bigZ_scope bigZ_scope].
Arguments Scope BigZ.gcd [bigZ_scope bigZ_scope].
Arguments Scope BigZ.even [bigZ_scope].
Arguments Scope BigZ.odd [bigZ_scope].
@@ -92,7 +92,6 @@ Notation "x <= y < z" := (x<=y /\ y<z)%bigZ : bigZ_scope.
Notation "x <= y <= z" := (x<=y /\ y<=z)%bigZ : bigZ_scope.
Notation "[ i ]" := (BigZ.to_Z i) : bigZ_scope.
Infix "mod" := BigZ.modulo (at level 40, no associativity) : bigZ_scope.
-Infix "rem" := BigZ.remainder (at level 40, no associativity) : bigZ_scope.
Infix "÷" := BigZ.quot (at level 40, left associativity) : bigZ_scope.
Local Open Scope bigZ_scope.
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index f4baf32bc..4c4eb6c10 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -461,7 +461,7 @@ Module Make (N:NType) <: ZType.
| Neg nx, Neg ny => Pos (N.div nx ny)
end.
- Definition remainder x y :=
+ Definition rem x y :=
if eq_bool y zero then x
else
match x, y with
@@ -478,10 +478,10 @@ Module Make (N:NType) <: ZType.
rewrite Zquot_Zdiv_pos; trivial using N.spec_pos.
Qed.
- Lemma spec_remainder : forall x y,
- to_Z (remainder x y) = (to_Z x) rem (to_Z y).
+ Lemma spec_rem : forall x y,
+ to_Z (rem x y) = Zrem (to_Z x) (to_Z y).
Proof.
- intros x y. unfold remainder. rewrite spec_eq_bool, spec_0.
+ intros x y. unfold rem. rewrite spec_eq_bool, spec_0.
assert (Hy := Zeq_bool_if (to_Z y) 0). destruct Zeq_bool.
now rewrite Hy, Zrem_0_r.
destruct x as [x|x], y as [y|y]; simpl in *; symmetry;
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index f68aa0dbe..5f38d57b8 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -189,7 +189,7 @@ Definition rem_bound_pos := Zrem_bound.
Definition rem_opp_l := fun a b (_:b<>0) => Zrem_opp_l a b.
Definition rem_opp_r := fun a b (_:b<>0) => Zrem_opp_r a b.
Definition quot := Zquot.
-Definition remainder := Zrem.
+Definition rem := Zrem.
(** We define [eq] only here to avoid refering to this [eq] above. *)
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v
index c2a173e22..1c06b0b8e 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSig.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v
@@ -56,7 +56,7 @@ Module Type ZType.
Parameter div : t -> t -> t.
Parameter modulo : t -> t -> t.
Parameter quot : t -> t -> t.
- Parameter remainder : t -> t -> t.
+ Parameter rem : t -> t -> t.
Parameter gcd : t -> t -> t.
Parameter sgn : t -> t.
Parameter abs : t -> t.
@@ -88,7 +88,7 @@ Module Type ZType.
Parameter spec_div: forall x y, [div x y] = [x] / [y].
Parameter spec_modulo: forall x y, [modulo x y] = [x] mod [y].
Parameter spec_quot: forall x y, [quot x y] = [x] ÷ [y].
- Parameter spec_remainder: forall x y, [remainder x y] = [x] rem [y].
+ Parameter spec_rem: forall x y, [rem x y] = Zrem [x] [y].
Parameter spec_gcd: forall a b, [gcd a b] = Zgcd [a] [b].
Parameter spec_sgn : forall x, [sgn x] = Zsgn [x].
Parameter spec_abs : forall x, [abs x] = Zabs [x].
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index 6a823a732..62b79fc3a 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -16,8 +16,7 @@ Hint Rewrite
spec_0 spec_1 spec_2 spec_add spec_sub spec_pred spec_succ
spec_mul spec_opp spec_of_Z spec_div spec_modulo spec_sqrt
spec_compare spec_eq_bool spec_max spec_min spec_abs spec_sgn
- spec_pow spec_log2 spec_even spec_odd spec_gcd spec_quot
- spec_remainder
+ spec_pow spec_log2 spec_even spec_odd spec_gcd spec_quot spec_rem
: zsimpl.
Ltac zsimpl := autorewrite with zsimpl.
@@ -353,25 +352,25 @@ Definition mod_bound_pos :
(** Quot / Rem *)
Program Instance quot_wd : Proper (eq==>eq==>eq) quot.
-Program Instance rem_wd : Proper (eq==>eq==>eq) remainder.
+Program Instance rem_wd : Proper (eq==>eq==>eq) rem.
-Theorem quot_rem : forall a b, ~b==0 -> a == b*(quot a b) + (remainder a b).
+Theorem quot_rem : forall a b, ~b==0 -> a == b*(quot a b) + rem a b.
Proof.
intros a b _. zify. apply Z_quot_rem_eq.
Qed.
Theorem rem_bound_pos :
- forall a b, 0<=a -> 0<b -> 0 <= remainder a b /\ remainder a b < b.
+ forall a b, 0<=a -> 0<b -> 0 <= rem a b /\ rem a b < b.
Proof.
intros a b. zify. intros. now apply Zrem_bound.
Qed.
-Theorem rem_opp_l : forall a b, ~b==0 -> remainder (-a) b == -(remainder a b).
+Theorem rem_opp_l : forall a b, ~b==0 -> rem (-a) b == -(rem a b).
Proof.
intros a b _. zify. apply Zrem_opp_l.
Qed.
-Theorem rem_opp_r : forall a b, ~b==0 -> remainder a (-b) == remainder a b.
+Theorem rem_opp_r : forall a b, ~b==0 -> rem a (-b) == rem a b.
Proof.
intros a b _. zify. apply Zrem_opp_r.
Qed.
diff --git a/theories/ZArith/Zdiv_def.v b/theories/ZArith/Zdiv_def.v
index a48170fd1..0e71bb4c3 100644
--- a/theories/ZArith/Zdiv_def.v
+++ b/theories/ZArith/Zdiv_def.v
@@ -126,18 +126,7 @@ Definition Zquot a b := fst (Zquotrem a b).
Definition Zrem a b := snd (Zquotrem a b).
Infix "÷" := Zquot (at level 40, left associativity) : Z_scope.
-Infix "rem" := Zrem (at level 40, no associativity) : Z_scope.
-
-
-
-(** * Euclid *)
-
-(** In this last convention, the remainder is always non-negative *)
-
-Definition Zeuclid_mod a b := Zmod a (Zabs b).
-Definition Zeuclid_div a b := (Zsgn b) * (Zdiv a (Zabs b)).
-
-
+(** No infix notation for rem, otherwise it becomes a keyword *)
(** * Correctness proofs *)
@@ -280,13 +269,13 @@ Proof.
now rewrite Zopp_plus_distr, Zopp_mult_distr_r.
Qed.
-Lemma Z_quot_rem_eq : forall a b, a = b*(a÷b) + a rem b.
+Lemma Z_quot_rem_eq : forall a b, a = b*(a÷b) + Zrem a b.
Proof.
intros a b. rewrite Zmult_comm. generalize (Zquotrem_eq a b).
unfold Zquot, Zrem. now destruct Zquotrem.
Qed.
-Lemma Zrem_bound : forall a b, 0<=a -> 0<b -> 0 <= a rem b < b.
+Lemma Zrem_bound : forall a b, 0<=a -> 0<b -> 0 <= Zrem a b < b.
Proof.
intros a [|b|b] Ha Hb; discriminate Hb || clear Hb.
destruct a as [|a|a]; (now destruct Ha) || clear Ha.
@@ -297,13 +286,13 @@ Proof.
destruct r; red; simpl; trivial.
Qed.
-Lemma Zrem_opp_l : forall a b, (-a) rem b = - (a rem b).
+Lemma Zrem_opp_l : forall a b, Zrem (-a) b = - (Zrem a b).
Proof.
intros [|a|a] [|b|b]; trivial; unfold Zrem;
simpl; destruct Pdiv_eucl; simpl; try rewrite Zopp_involutive; trivial.
Qed.
-Lemma Zrem_opp_r : forall a b, a rem (-b) = a rem b.
+Lemma Zrem_opp_r : forall a b, Zrem a (-b) = Zrem a b.
Proof.
intros [|a|a] [|b|b]; trivial; unfold Zrem; simpl;
destruct Pdiv_eucl; simpl; try rewrite Zopp_involutive; trivial.
diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v
index 307faccfe..4f1c94e99 100644
--- a/theories/ZArith/Zquot.v
+++ b/theories/ZArith/Zquot.v
@@ -35,7 +35,7 @@ Proof.
Qed.
Lemma Nmod_Zrem : forall a b:N,
- Z_of_N (a mod b) = (Z_of_N a) rem (Z_of_N b).
+ Z_of_N (a mod b) = Zrem (Z_of_N a) (Z_of_N b).
Proof.
intros.
destruct a; destruct b; simpl; auto.
@@ -54,7 +54,7 @@ Notation Z_quot_rem_eq := Z_quot_rem_eq (only parsing).
The remainder is bounded by the divisor, in term of absolute values *)
Theorem Zrem_lt : forall a b:Z, b<>0 ->
- Zabs (a rem b) < Zabs b.
+ Zabs (Zrem a b) < Zabs b.
Proof.
destruct b as [ |b|b]; intro H; try solve [elim H;auto];
destruct a as [ |a|a]; try solve [compute;auto]; unfold Zrem, Zquotrem;
@@ -68,7 +68,7 @@ Qed.
*)
Theorem Zrem_sgn : forall a b:Z,
- 0 <= Zsgn (a rem b) * Zsgn a.
+ 0 <= Zsgn (Zrem a b) * Zsgn a.
Proof.
destruct b as [ |b|b]; destruct a as [ |a|a]; simpl; auto with zarith;
unfold Zrem, Zquotrem; destruct Pdiv_eucl;
@@ -83,7 +83,7 @@ Proof.
Qed.
Theorem Zrem_sgn2 : forall a b:Z,
- 0 <= (a rem b) * a.
+ 0 <= (Zrem a b) * a.
Proof.
intros; rewrite <-Zsgn_pos_iff, Zsgn_Zmult; apply Zrem_sgn.
Qed.
@@ -92,10 +92,10 @@ Qed.
then 4 particular cases. *)
Theorem Zrem_lt_pos : forall a b:Z, 0<=a -> b<>0 ->
- 0 <= a rem b < Zabs b.
+ 0 <= Zrem a b < Zabs b.
Proof.
intros.
- assert (0 <= a rem b).
+ assert (0 <= Zrem a b).
generalize (Zrem_sgn a b).
destruct (Zle_lt_or_eq 0 a H).
rewrite <- Zsgn_pos in H1; rewrite H1; romega with *.
@@ -104,10 +104,10 @@ Proof.
Qed.
Theorem Zrem_lt_neg : forall a b:Z, a<=0 -> b<>0 ->
- -Zabs b < a rem b <= 0.
+ -Zabs b < Zrem a b <= 0.
Proof.
intros.
- assert (a rem b <= 0).
+ assert (Zrem a b <= 0).
generalize (Zrem_sgn a b).
destruct (Zle_lt_or_eq a 0 H).
rewrite <- Zsgn_neg in H1; rewrite H1; romega with *.
@@ -115,22 +115,22 @@ Proof.
generalize (Zrem_lt a b H0); romega with *.
Qed.
-Theorem Zrem_lt_pos_pos : forall a b:Z, 0<=a -> 0<b -> 0 <= a rem b < b.
+Theorem Zrem_lt_pos_pos : forall a b:Z, 0<=a -> 0<b -> 0 <= Zrem a b < b.
Proof.
intros; generalize (Zrem_lt_pos a b); romega with *.
Qed.
-Theorem Zrem_lt_pos_neg : forall a b:Z, 0<=a -> b<0 -> 0 <= a rem b < -b.
+Theorem Zrem_lt_pos_neg : forall a b:Z, 0<=a -> b<0 -> 0 <= Zrem a b < -b.
Proof.
intros; generalize (Zrem_lt_pos a b); romega with *.
Qed.
-Theorem Zrem_lt_neg_pos : forall a b:Z, a<=0 -> 0<b -> -b < a rem b <= 0.
+Theorem Zrem_lt_neg_pos : forall a b:Z, a<=0 -> 0<b -> -b < Zrem a b <= 0.
Proof.
intros; generalize (Zrem_lt_neg a b); romega with *.
Qed.
-Theorem Zrem_lt_neg_neg : forall a b:Z, a<=0 -> b<0 -> b < a rem b <= 0.
+Theorem Zrem_lt_neg_neg : forall a b:Z, a<=0 -> b<0 -> b < Zrem a b <= 0.
Proof.
intros; generalize (Zrem_lt_neg a b); romega with *.
Qed.
@@ -151,13 +151,13 @@ Proof.
unfold Zquot, Zquotrem; destruct Pdiv_eucl; simpl; auto with zarith.
Qed.
-Theorem Zrem_opp_l : forall a b:Z, (-a) rem b = -(a rem b).
+Theorem Zrem_opp_l : forall a b:Z, Zrem (-a) b = -(Zrem a b).
Proof.
destruct a; destruct b; simpl; auto;
unfold Zrem, Zquotrem; destruct Pdiv_eucl; simpl; auto with zarith.
Qed.
-Theorem Zrem_opp_r : forall a b:Z, a rem (-b) = a rem b.
+Theorem Zrem_opp_r : forall a b:Z, Zrem a (-b) = Zrem a b.
Proof.
destruct a; destruct b; simpl; auto;
unfold Zrem, Zquotrem; destruct Pdiv_eucl; simpl; auto with zarith.
@@ -169,7 +169,7 @@ Proof.
unfold Zquot, Zquotrem; destruct Pdiv_eucl; simpl; auto with zarith.
Qed.
-Theorem Zrem_opp_opp : forall a b:Z, (-a) rem (-b) = -(a rem b).
+Theorem Zrem_opp_opp : forall a b:Z, Zrem (-a) (-b) = -(Zrem a b).
Proof.
destruct a; destruct b; simpl; auto;
unfold Zrem, Zquotrem; destruct Pdiv_eucl; simpl; auto with zarith.
@@ -197,7 +197,7 @@ Qed.
Theorem Zquot_mod_unique_full:
forall a b q r, Remainder a b r ->
- a = b*q + r -> q = a÷b /\ r = a rem b.
+ a = b*q + r -> q = a÷b /\ r = Zrem a b.
Proof.
destruct 1 as [(H,H0)|(H,H0)]; intros.
apply Zdiv_mod_unique with b; auto.
@@ -207,7 +207,7 @@ Proof.
rewrite <- (Zopp_involutive a).
rewrite Zquot_opp_l, Zrem_opp_l.
- generalize (Zdiv_mod_unique b (-q) (-a÷b) (-r) (-a rem b)).
+ generalize (Zdiv_mod_unique b (-q) (-a÷b) (-r) (Zrem (-a) b)).
generalize (Zrem_lt_pos (-a) b).
rewrite <-Z_quot_rem_eq, <-Zopp_mult_distr_r, <-Zopp_plus_distr, <-H1.
romega with *.
@@ -227,24 +227,24 @@ Proof. exact Z.quot_unique. Qed.
Theorem Zrem_unique_full:
forall a b q r, Remainder a b r ->
- a = b*q + r -> r = a rem b.
+ a = b*q + r -> r = Zrem a b.
Proof.
intros; destruct (Zquot_mod_unique_full a b q r); auto.
Qed.
Theorem Zrem_unique:
forall a b q r, 0 <= a -> 0 <= r < b ->
- a = b*q + r -> r = a rem b.
+ a = b*q + r -> r = Zrem a b.
Proof. exact Z.rem_unique. Qed.
(** * Basic values of divisions and modulo. *)
-Lemma Zrem_0_l: forall a, 0 rem a = 0.
+Lemma Zrem_0_l: forall a, Zrem 0 a = 0.
Proof.
destruct a; simpl; auto.
Qed.
-Lemma Zrem_0_r: forall a, a rem 0 = a.
+Lemma Zrem_0_r: forall a, Zrem a 0 = a.
Proof.
destruct a; simpl; auto.
Qed.
@@ -259,7 +259,7 @@ Proof.
destruct a; simpl; auto.
Qed.
-Lemma Zrem_1_r: forall a, a rem 1 = 0.
+Lemma Zrem_1_r: forall a, Zrem a 1 = 0.
Proof. exact Z.rem_1_r. Qed.
Lemma Zquot_1_r: forall a, a÷1 = a.
@@ -271,7 +271,7 @@ Hint Resolve Zrem_0_l Zrem_0_r Zquot_0_l Zquot_0_r Zquot_1_r Zrem_1_r
Lemma Zquot_1_l: forall a, 1 < a -> 1÷a = 0.
Proof. exact Z.quot_1_l. Qed.
-Lemma Zrem_1_l: forall a, 1 < a -> 1 rem a = 1.
+Lemma Zrem_1_l: forall a, 1 < a -> Zrem 1 a = 1.
Proof. exact Z.rem_1_l. Qed.
Lemma Z_quot_same : forall a:Z, a<>0 -> a÷a = 1.
@@ -282,10 +282,10 @@ Ltac zero_or_not a :=
[subst; rewrite ?Zrem_0_l, ?Zquot_0_l, ?Zrem_0_r, ?Zquot_0_r;
auto with zarith|].
-Lemma Z_rem_same : forall a, a rem a = 0.
+Lemma Z_rem_same : forall a, Zrem a a = 0.
Proof. intros. zero_or_not a. apply Z.rem_same; auto. Qed.
-Lemma Z_rem_mult : forall a b, (a*b) rem b = 0.
+Lemma Z_rem_mult : forall a b, Zrem (a*b) b = 0.
Proof. intros. zero_or_not b. apply Z.rem_mul; auto. Qed.
Lemma Z_quot_mult : forall a b:Z, b <> 0 -> (a*b)÷b = a.
@@ -311,7 +311,7 @@ Proof. exact Z.quot_small. Qed.
(** Same situation, in term of modulo: *)
-Theorem Zrem_small: forall a n, 0 <= a < n -> a rem n = a.
+Theorem Zrem_small: forall a n, 0 <= a < n -> Zrem a n = a.
Proof. exact Z.rem_small. Qed.
(** [Zge] is compatible with a positive division. *)
@@ -330,12 +330,12 @@ Proof. intros. zero_or_not b. apply Z.mul_quot_ge; auto with zarith. Qed.
(** The previous inequalities between [b*(a÷b)] and [a] are exact
iff the modulo is zero. *)
-Lemma Z_quot_exact_full : forall a b:Z, a = b*(a÷b) <-> a rem b = 0.
+Lemma Z_quot_exact_full : forall a b:Z, a = b*(a÷b) <-> Zrem a b = 0.
Proof. intros. zero_or_not b. intuition. apply Z.quot_exact; auto. Qed.
(** A modulo cannot grow beyond its starting point. *)
-Theorem Zrem_le: forall a b, 0 <= a -> 0 <= b -> a rem b <= a.
+Theorem Zrem_le: forall a b, 0 <= a -> 0 <= b -> Zrem a b <= a.
Proof. intros. zero_or_not b. apply Z.rem_le; auto with zarith. Qed.
(** Some additionnal inequalities about Zdiv. *)
@@ -367,7 +367,7 @@ Qed.
Lemma Z_rem_plus : forall a b c:Z,
0 <= (a+b*c) * a ->
- (a + b * c) rem c = a rem c.
+ Zrem (a + b * c) c = Zrem a c.
Proof. intros. zero_or_not c. apply Z.rem_add; auto with zarith. Qed.
Lemma Z_quot_plus : forall a b c:Z,
@@ -394,14 +394,14 @@ Proof.
Qed.
Lemma Zmult_rem_distr_l: forall a b c,
- (c*a) rem (c*b) = c * (a rem b).
+ Zrem (c*a) (c*b) = c * (Zrem a b).
Proof.
intros. zero_or_not c. rewrite (Zmult_comm c b). zero_or_not b.
rewrite (Zmult_comm b c). apply Z.mul_rem_distr_l; auto.
Qed.
Lemma Zmult_rem_distr_r: forall a b c,
- (a*c) rem (b*c) = (a rem b) * c.
+ Zrem (a*c) (b*c) = (Zrem a b) * c.
Proof.
intros. zero_or_not b. rewrite (Zmult_comm b c). zero_or_not c.
rewrite (Zmult_comm c b). apply Z.mul_rem_distr_r; auto.
@@ -409,11 +409,11 @@ Qed.
(** Operations modulo. *)
-Theorem Zrem_rem: forall a n, (a rem n) rem n = a rem n.
+Theorem Zrem_rem: forall a n, Zrem (Zrem a n) n = Zrem a n.
Proof. intros. zero_or_not n. apply Z.rem_rem; auto. Qed.
Theorem Zmult_rem: forall a b n,
- (a * b) rem n = ((a rem n) * (b rem n)) rem n.
+ Zrem (a * b) n = Zrem (Zrem a n * Zrem b n) n.
Proof. intros. zero_or_not n. apply Z.mul_rem; auto. Qed.
(** addition and modulo
@@ -426,25 +426,26 @@ Proof. intros. zero_or_not n. apply Z.mul_rem; auto. Qed.
Theorem Zplus_rem: forall a b n,
0 <= a * b ->
- (a + b) rem n = (a rem n + b rem n) rem n.
+ Zrem (a + b) n = Zrem (Zrem a n + Zrem b n) n.
Proof. intros. zero_or_not n. apply Z.add_rem; auto. Qed.
Lemma Zplus_rem_idemp_l: forall a b n,
0 <= a * b ->
- (a rem n + b) rem n = (a + b) rem n.
+ Zrem (Zrem a n + b) n = Zrem (a + b) n.
Proof. intros. zero_or_not n. apply Z.add_rem_idemp_l; auto. Qed.
Lemma Zplus_rem_idemp_r: forall a b n,
0 <= a*b ->
- (b + a rem n) rem n = (b + a) rem n.
+ Zrem (b + Zrem a n) n = Zrem (b + a) n.
Proof.
intros. zero_or_not n. apply Z.add_rem_idemp_r; auto.
- rewrite Zmult_comm; auto. Qed.
+ rewrite Zmult_comm; auto.
+Qed.
-Lemma Zmult_rem_idemp_l: forall a b n, (a rem n * b) rem n = (a * b) rem n.
+Lemma Zmult_rem_idemp_l: forall a b n, Zrem (Zrem a n * b) n = Zrem (a * b) n.
Proof. intros. zero_or_not n. apply Z.mul_rem_idemp_l; auto. Qed.
-Lemma Zmult_rem_idemp_r: forall a b n, (b * (a rem n)) rem n = (b * a) rem n.
+Lemma Zmult_rem_idemp_r: forall a b n, Zrem (b * Zrem a n) n = Zrem (b * a) n.
Proof. intros. zero_or_not n. apply Z.mul_rem_idemp_r; auto. Qed.
(** Unlike with Zdiv, the following result is true without restrictions. *)
@@ -464,7 +465,7 @@ Proof. intros. zero_or_not b. apply Z.quot_mul_le; auto with zarith. Qed.
(** Zrem is related to divisibility (see more in Znumtheory) *)
Lemma Zrem_divides : forall a b,
- a rem b = 0 <-> exists c, a = b*c.
+ Zrem a b = 0 <-> exists c, a = b*c.
Proof.
intros. zero_or_not b. firstorder.
rewrite Z.rem_divide; trivial. split; intros (c,Hc); exists c; auto.
@@ -475,7 +476,7 @@ Qed.
(** They agree at least on positive numbers: *)
Theorem Zquotrem_Zdiv_eucl_pos : forall a b:Z, 0 <= a -> 0 < b ->
- a÷b = a/b /\ a rem b = a mod b.
+ a÷b = a/b /\ Zrem a b = a mod b.
Proof.
intros.
apply Zdiv_mod_unique with b.
@@ -495,7 +496,7 @@ Proof.
Qed.
Theorem Zrem_Zmod_pos : forall a b, 0 <= a -> 0 < b ->
- a rem b = a mod b.
+ Zrem a b = a mod b.
Proof.
intros a b Ha Hb; generalize (Zquotrem_Zdiv_eucl_pos a b Ha Hb);
intuition.
@@ -504,7 +505,7 @@ Qed.
(** Modulos are null at the same places *)
Theorem Zrem_Zmod_zero : forall a b, b<>0 ->
- (a rem b = 0 <-> a mod b = 0).
+ (Zrem a b = 0 <-> a mod b = 0).
Proof.
intros.
rewrite Zrem_divides, Zmod_divides; intuition.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 07:35:43 +0000