aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
Diffstat (limited to 'theories')
-rw-r--r--theories/Numbers/Integer/BigZ/ZMake.v4
-rw-r--r--theories/Numbers/Integer/Binary/ZBinary.v4
-rw-r--r--theories/Numbers/Integer/SpecViaZ/ZSig.v2
-rw-r--r--theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v2
-rw-r--r--theories/Numbers/Natural/BigN/NMake.v4
-rw-r--r--theories/Numbers/Natural/SpecViaZ/NSig.v2
-rw-r--r--theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v2
-rw-r--r--theories/ZArith/Zdigits.v2
-rw-r--r--theories/ZArith/Zdigits_def.v20
-rw-r--r--theories/ZArith/Zdiv.v2
-rw-r--r--theories/ZArith/Zeven.v199
-rw-r--r--theories/ZArith/Zquot.v20
12 files changed, 120 insertions, 143 deletions
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index 1327c1923..7534628fa 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -719,9 +719,9 @@ Module Make (N:NType) <: ZType.
now rewrite <- Z.lxor_lnot_lnot, !Zlnot_alt2.
Qed.
- Lemma spec_div2: forall x, to_Z (div2 x) = Zdiv2' (to_Z x).
+ Lemma spec_div2: forall x, to_Z (div2 x) = Zdiv2 (to_Z x).
Proof.
- intros x. unfold div2. now rewrite spec_shiftr, Zdiv2'_spec, spec_1.
+ intros x. unfold div2. now rewrite spec_shiftr, Zdiv2_spec, spec_1.
Qed.
End Make.
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index eab33051d..8ed42ed8d 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -202,7 +202,7 @@ Definition land_spec := Zand_spec.
Definition lor_spec := Zor_spec.
Definition ldiff_spec := Zdiff_spec.
Definition lxor_spec := Zxor_spec.
-Definition div2_spec := Zdiv2'_spec.
+Definition div2_spec := Zdiv2_spec.
Definition testbit := Ztestbit.
Definition shiftl := Zshiftl.
@@ -211,7 +211,7 @@ Definition land := Zand.
Definition lor := Zor.
Definition ldiff := Zdiff.
Definition lxor := Zxor.
-Definition div2 := Zdiv2'.
+Definition div2 := Zdiv2.
(** 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 c33915449..788ca8e56 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSig.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v
@@ -109,7 +109,7 @@ Module Type ZType.
Parameter spec_lor: forall x y, [lor x y] = Zor [x] [y].
Parameter spec_ldiff: forall x y, [ldiff x y] = Zdiff [x] [y].
Parameter spec_lxor: forall x y, [lxor x y] = Zxor [x] [y].
- Parameter spec_div2: forall x, [div2 x] = Zdiv2' [x].
+ Parameter spec_div2: forall x, [div2 x] = Zdiv2 [x].
End ZType.
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index f8fa84283..8c1e7b4fa 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -471,7 +471,7 @@ Qed.
Lemma div2_spec : forall a, div2 a == shiftr a 1.
Proof.
- intros a. zify. now apply Zdiv2'_spec.
+ intros a. zify. now apply Zdiv2_spec.
Qed.
End ZTypeIsZAxioms.
diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v
index a55fb5900..105cf0620 100644
--- a/theories/Numbers/Natural/BigN/NMake.v
+++ b/theories/Numbers/Natural/BigN/NMake.v
@@ -1593,10 +1593,10 @@ Module Make (W0:CyclicType) <: NType.
Definition div2 x := shiftr x one.
- Lemma spec_div2: forall x, [div2 x] = Zdiv2' [x].
+ Lemma spec_div2: forall x, [div2 x] = Zdiv2 [x].
Proof.
intros. unfold div2. symmetry.
- rewrite spec_shiftr, spec_1. apply Zdiv2'_spec.
+ rewrite spec_shiftr, spec_1. apply Zdiv2_spec.
Qed.
(** TODO : provide efficient versions instead of just converting
diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v
index 021ac29ee..f186c55b4 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSig.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSig.v
@@ -99,7 +99,7 @@ Module Type NType.
Parameter spec_lor: forall x y, [lor x y] = Zor [x] [y].
Parameter spec_ldiff: forall x y, [ldiff x y] = Zdiff [x] [y].
Parameter spec_lxor: forall x y, [lxor x y] = Zxor [x] [y].
- Parameter spec_div2: forall x, [div2 x] = Zdiv2' [x].
+ Parameter spec_div2: forall x, [div2 x] = Zdiv2 [x].
End NType.
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index a169c009d..175b1ad2c 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -408,7 +408,7 @@ Qed.
Lemma div2_spec : forall a, div2 a == shiftr a 1.
Proof.
- intros a. zify. now apply Zdiv2'_spec.
+ intros a. zify. now apply Zdiv2_spec.
Qed.
(** Recursion *)
diff --git a/theories/ZArith/Zdigits.v b/theories/ZArith/Zdigits.v
index 1bea2bbbe..6d8a237e5 100644
--- a/theories/ZArith/Zdigits.v
+++ b/theories/ZArith/Zdigits.v
@@ -219,7 +219,7 @@ Section Z_BRIC_A_BRAC.
destruct (Zeven.Zeven_odd_dec z); intros.
rewrite <- Zeven.Zeven_div2; auto.
- generalize (Zeven.Zodd_div2 z H z0); omega.
+ generalize (Zeven.Zodd_div2 z z0); omega.
Qed.
Lemma Z_to_two_compl_Sn_z :
diff --git a/theories/ZArith/Zdigits_def.v b/theories/ZArith/Zdigits_def.v
index a31ef8c98..71b647063 100644
--- a/theories/ZArith/Zdigits_def.v
+++ b/theories/ZArith/Zdigits_def.v
@@ -41,15 +41,15 @@ Definition Ztestbit a n :=
For fulfilling the two's complement convention, shifting to
the right a negative number should correspond to a division
- by 2 with rounding toward bottom, hence the use of [Zdiv2']
- instead of [Zdiv2].
+ by 2 with rounding toward bottom, hence the use of [Zdiv2]
+ instead of [Zquot2].
*)
Definition Zshiftl a n :=
match n with
| 0 => a
| Zpos p => iter_pos p _ (Zmult 2) a
- | Zneg p => iter_pos p _ Zdiv2' a
+ | Zneg p => iter_pos p _ Zdiv2 a
end.
Definition Zshiftr a n := Zshiftl a (-n).
@@ -98,7 +98,7 @@ Definition Zxor a b :=
(** Proofs of specifications *)
-Lemma Zdiv2'_spec : forall a, Zdiv2' a = Zshiftr a 1.
+Lemma Zdiv2_spec : forall a, Zdiv2 a = Zshiftr a 1.
Proof.
reflexivity.
Qed.
@@ -115,8 +115,8 @@ Proof.
intros a [ |n|n] Hn; (now destruct Hn) || clear Hn.
(* n = 0 *)
simpl Ztestbit.
- exists 0. exists (Zdiv2' a). repeat split. easy.
- now rewrite Zplus_0_l, Zmult_1_r, Zplus_comm, <- Zdiv2'_odd.
+ exists 0. exists (Zdiv2 a). repeat split. easy.
+ now rewrite Zplus_0_l, Zmult_1_r, Zplus_comm, <- Zdiv2_odd_eqn.
(* n > 0 *)
destruct a.
(* ... a = 0 *)
@@ -211,12 +211,12 @@ Proof.
destruct p; simpl; trivial.
Qed.
-Lemma Z_of_N_div2' : forall n, Z_of_N (Ndiv2 n) = Zdiv2' (Z_of_N n).
+Lemma Z_of_N_div2 : forall n, Z_of_N (Ndiv2 n) = Zdiv2 (Z_of_N n).
Proof.
intros [|p]; trivial. now destruct p.
Qed.
-Lemma Z_of_N_div2 : forall n, Z_of_N (Ndiv2 n) = Zdiv2 (Z_of_N n).
+Lemma Z_of_N_quot2 : forall n, Z_of_N (Ndiv2 n) = Zquot2 (Z_of_N n).
Proof.
intros [|p]; trivial. now destruct p.
Qed.
@@ -263,12 +263,12 @@ Proof.
now rewrite Zplus_0_r.
destruct a as [ |a|a].
(* a = 0 *)
- replace (iter_pos n _ Zdiv2' 0) with 0
+ replace (iter_pos n _ Zdiv2 0) with 0
by (apply iter_pos_invariant; intros; subst; trivial).
now rewrite 2 Ztestbit_0_l.
(* a > 0 *)
rewrite <- (Z_of_N_pos a) at 1.
- rewrite <- (iter_pos_swap_gen _ _ _ Ndiv2) by exact Z_of_N_div2'.
+ rewrite <- (iter_pos_swap_gen _ _ _ Ndiv2) by exact Z_of_N_div2.
rewrite Ztestbit_Zpos, Ztestbit_of_N'; trivial.
rewrite Zabs_N_plus; try easy. simpl Zabs_N.
exact (Nshiftr_spec (Npos a) (Npos n) (Zabs_N m)).
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index c9397db8b..563f8080d 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -523,7 +523,7 @@ Qed.
(** Particular case : dividing by 2 is related with parity *)
-Lemma Zdiv2'_div : forall a, Zdiv2' a = a/2.
+Lemma Zdiv2_div : forall a, Zdiv2 a = a/2.
Proof.
apply Z.div2_div.
Qed.
diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v
index 70ab4dacc..9bff641b7 100644
--- a/theories/ZArith/Zeven.v
+++ b/theories/ZArith/Zeven.v
@@ -170,17 +170,26 @@ Proof.
Qed.
(******************************************************************)
-(** * Definition of [Zdiv2] and properties wrt [Zeven] and [Zodd] *)
+(** * Definition of [Zquot2], [Zdiv2] and properties wrt [Zeven]
+ and [Zodd] *)
-(** [Zdiv2] is defined on all [Z], but notice that for odd negative
- integers we have [n = 2*(Zdiv2 n)-1], hence it does not
- correspond to the usual Coq division [Zdiv], for which we would
- have here [n = 2*(n/2)+1]. Since [Zdiv2] performs rounding
- toward zero, it is rather a particular case of the alternative
- division [Zquot].
-*)
+(** [Zdiv2] performs rounding toward bottom, it is hence a particular
+ case of [Zdiv], and for all relative number [n] we have:
+ [n = 2 * Zdiv2 n + if Zodd_bool n then 1 else 0]. *)
-Definition Zdiv2 (z:Z) :=
+Definition Zdiv2 z :=
+ match z with
+ | 0 => 0
+ | Zpos 1 => 0
+ | Zpos p => Zpos (Pdiv2 p)
+ | Zneg p => Zneg (Pdiv2_up p)
+ end.
+
+(** [Zquot2] performs rounding toward zero, it is hence a particular
+ case of [Zquot], and for all relative number [n] we have:
+ [n = 2 * Zdiv2 n + if Zodd_bool n then Zsgn n else 0]. *)
+
+Definition Zquot2 (z:Z) :=
match z with
| 0 => 0
| Zpos 1 => 0
@@ -189,19 +198,12 @@ Definition Zdiv2 (z:Z) :=
| Zneg p => Zneg (Pdiv2 p)
end.
-(** We also provide an alternative [Zdiv2'] performing round toward
- bottom, and hence corresponding to [Zdiv]. *)
+(** NB: [Zquot2] used to be named [Zdiv2] in Coq <= 8.3 *)
-Definition Zdiv2' a :=
- match a with
- | 0 => 0
- | Zpos 1 => 0
- | Zpos p => Zpos (Pdiv2 p)
- | Zneg p => Zneg (Pdiv2_up p)
- end.
+(** Properties of [Zdiv2] *)
-Lemma Zdiv2'_odd : forall a,
- a = 2*(Zdiv2' a) + if Zodd_bool a then 1 else 0.
+Lemma Zdiv2_odd_eqn : forall n,
+ n = 2*(Zdiv2 n) + if Zodd_bool n then 1 else 0.
Proof.
intros [ |[p|p| ]|[p|p| ]]; simpl; trivial.
f_equal. now rewrite xO_succ_permute, <-Ppred_minus, Ppred_succ.
@@ -209,50 +211,56 @@ Qed.
Lemma Zeven_div2 : forall n:Z, Zeven n -> n = 2 * Zdiv2 n.
Proof.
- intro x; destruct x.
- auto with arith.
- destruct p; auto with arith.
- intros. absurd (Zeven (Zpos (xI p))); red; auto with arith.
- intros. absurd (Zeven 1); red; auto with arith.
- destruct p; auto with arith.
- intros. absurd (Zeven (Zneg (xI p))); red; auto with arith.
- intros. absurd (Zeven (-1)); red; auto with arith.
+ intros n Hn. apply Zeven_bool_iff in Hn.
+ pattern n at 1.
+ now rewrite (Zdiv2_odd_eqn n), Zodd_even_bool, Hn, Zplus_0_r.
Qed.
-Lemma Zodd_div2 : forall n:Z, n >= 0 -> Zodd n -> n = 2 * Zdiv2 n + 1.
+Lemma Zodd_div2 : forall n:Z, Zodd n -> n = 2 * Zdiv2 n + 1.
Proof.
- intro x; destruct x.
- intros. absurd (Zodd 0); red; auto with arith.
- destruct p; auto with arith.
- intros. absurd (Zodd (Zpos (xO p))); red; auto with arith.
- intros. absurd (Zneg p >= 0); red; auto with arith.
+ intros n Hn. apply Zodd_bool_iff in Hn.
+ pattern n at 1. now rewrite (Zdiv2_odd_eqn n), Hn.
Qed.
-Lemma Zodd_div2_neg :
- forall n:Z, n <= 0 -> Zodd n -> n = 2 * Zdiv2 n - 1.
+(** Properties of [Zquot2] *)
+
+Lemma Zquot2_odd_eqn : forall n,
+ n = 2*(Zquot2 n) + if Zodd_bool n then Zsgn n else 0.
Proof.
- intro x; destruct x.
- intros. absurd (Zodd 0); red; auto with arith.
- intros. absurd (Zneg p >= 0); red; auto with arith.
- destruct p; auto with arith.
- intros. absurd (Zodd (Zneg (xO p))); red; auto with arith.
+ intros [ |[p|p| ]|[p|p| ]]; simpl; trivial.
+Qed.
+
+Lemma Zeven_quot2 : forall n:Z, Zeven n -> n = 2 * Zquot2 n.
+Proof.
+ intros n Hn. apply Zeven_bool_iff in Hn.
+ pattern n at 1.
+ now rewrite (Zquot2_odd_eqn n), Zodd_even_bool, Hn, Zplus_0_r.
+Qed.
+
+Lemma Zodd_quot2 : forall n:Z, n >= 0 -> Zodd n -> n = 2 * Zquot2 n + 1.
+Proof.
+ intros n Hn Hn'. apply Zodd_bool_iff in Hn'.
+ pattern n at 1. rewrite (Zquot2_odd_eqn n), Hn'. f_equal.
+ destruct n; (now destruct Hn) || easy.
+Qed.
+
+Lemma Zodd_quot2_neg :
+ forall n:Z, n <= 0 -> Zodd n -> n = 2 * Zquot2 n - 1.
+Proof.
+ intros n Hn Hn'. apply Zodd_bool_iff in Hn'.
+ pattern n at 1. rewrite (Zquot2_odd_eqn n), Hn'. unfold Zminus. f_equal.
+ destruct n; (now destruct Hn) || easy.
Qed.
+(** More properties of parity *)
+
Lemma Z_modulo_2 :
forall n:Z, {y : Z | n = 2 * y} + {y : Z | n = 2 * y + 1}.
Proof.
- intros x.
- elim (Zeven_odd_dec x); intro.
- left. split with (Zdiv2 x). exact (Zeven_div2 x a).
- right. generalize b; clear b; case x.
- intro b; inversion b.
- intro p; split with (Zdiv2 (Zpos p)). apply (Zodd_div2 (Zpos p)); trivial.
- unfold Zge, Zcompare; simpl; discriminate.
- intro p; split with (Zdiv2 (Zpred (Zneg p))).
- pattern (Zneg p) at 1; rewrite (Zsucc_pred (Zneg p)).
- pattern (Zpred (Zneg p)) at 1; rewrite (Zeven_div2 (Zpred (Zneg p))).
- reflexivity.
- apply Zeven_pred; assumption.
+ intros n.
+ destruct (Zeven_odd_dec n) as [Hn|Hn].
+ left. exists (Zdiv2 n). exact (Zeven_div2 n Hn).
+ right. exists (Zdiv2 n). exact (Zodd_div2 n Hn).
Qed.
Lemma Zsplit2 :
@@ -260,18 +268,13 @@ Lemma Zsplit2 :
{p : Z * Z |
let (x1, x2) := p in n = x1 + x2 /\ (x1 = x2 \/ x2 = x1 + 1)}.
Proof.
- intros x.
- elim (Z_modulo_2 x); intros [y Hy]; rewrite Zmult_comm in Hy;
- rewrite <- Zplus_diag_eq_mult_2 in Hy.
- exists (y, y); split.
- assumption.
- left; reflexivity.
- exists (y, (y + 1)%Z); split.
- rewrite Zplus_assoc; assumption.
- right; reflexivity.
+ intros n.
+ destruct (Z_modulo_2 n) as [(y,Hy)|(y,Hy)];
+ rewrite Zmult_comm, <- Zplus_diag_eq_mult_2 in Hy.
+ exists (y, y). split. assumption. now left.
+ exists (y, y + 1). split. now rewrite Zplus_assoc. now right.
Qed.
-
Theorem Zeven_ex: forall n, Zeven n -> exists m, n = 2 * m.
Proof.
intro n; exists (Zdiv2 n); apply Zeven_div2; auto.
@@ -279,16 +282,7 @@ Qed.
Theorem Zodd_ex: forall n, Zodd n -> exists m, n = 2 * m + 1.
Proof.
- destruct n; intros.
- inversion H.
- exists (Zdiv2 (Zpos p)).
- apply Zodd_div2; simpl; auto; compute; inversion 1.
- exists (Zdiv2 (Zneg p) - 1).
- unfold Zminus.
- rewrite Zmult_plus_distr_r.
- rewrite <- Zplus_assoc.
- assert (Zneg p <= 0) by (compute; inversion 1).
- exact (Zodd_div2_neg _ H0 H).
+ intro n; exists (Zdiv2 n); apply Zodd_div2; auto.
Qed.
Theorem Zeven_2p: forall p, Zeven (2 * p).
@@ -315,58 +309,50 @@ Qed.
Theorem Zeven_plus_Zodd: forall a b,
Zeven a -> Zodd b -> Zodd (a + b).
Proof.
- intros a b H1 H2; case Zeven_ex with (1 := H1); intros x H3; try rewrite H3; auto.
- case Zodd_ex with (1 := H2); intros y H4; try rewrite H4; auto.
- replace (2 * x + (2 * y + 1)) with (2 * (x + y) + 1); try apply Zodd_2p_plus_1; auto with zarith.
- rewrite Zmult_plus_distr_r, Zplus_assoc; auto.
+ intros a b Ha Hb.
+ destruct (Zeven_ex a) as (x,->), (Zodd_ex b) as (y,->); trivial.
+ rewrite Zplus_assoc, <- Zmult_plus_distr_r.
+ apply Zodd_2p_plus_1.
Qed.
Theorem Zeven_plus_Zeven: forall a b,
Zeven a -> Zeven b -> Zeven (a + b).
Proof.
- intros a b H1 H2; case Zeven_ex with (1 := H1); intros x H3; try rewrite H3; auto.
- case Zeven_ex with (1 := H2); intros y H4; try rewrite H4; auto.
- replace (2 * x + 2 * y) with (2 * (x + y)); try apply Zeven_2p; auto with zarith.
- apply Zmult_plus_distr_r; auto.
+ intros a b Ha Hb.
+ destruct (Zeven_ex a) as (x,->), (Zeven_ex b) as (y,->); trivial.
+ rewrite <- Zmult_plus_distr_r.
+ apply Zeven_2p.
Qed.
Theorem Zodd_plus_Zeven: forall a b,
Zodd a -> Zeven b -> Zodd (a + b).
Proof.
- intros a b H1 H2; rewrite Zplus_comm; apply Zeven_plus_Zodd; auto.
+ intros a b Ha Hb; rewrite Zplus_comm; apply Zeven_plus_Zodd; auto.
Qed.
Theorem Zodd_plus_Zodd: forall a b,
Zodd a -> Zodd b -> Zeven (a + b).
Proof.
- intros a b H1 H2; case Zodd_ex with (1 := H1); intros x H3; try rewrite H3; auto.
- case Zodd_ex with (1 := H2); intros y H4; try rewrite H4; auto.
- replace ((2 * x + 1) + (2 * y + 1)) with (2 * (x + y + 1)); try apply Zeven_2p; auto.
- (* ring part *)
- do 2 rewrite Zmult_plus_distr_r; auto.
- repeat rewrite <- Zplus_assoc; f_equal.
- rewrite (Zplus_comm 1).
- repeat rewrite <- Zplus_assoc; auto.
+ intros a b Ha Hb.
+ destruct (Zodd_ex a) as (x,->), (Zodd_ex b) as (y,->); trivial.
+ rewrite <- Zplus_assoc, (Zplus_comm 1), <- Zplus_assoc.
+ change (1+1) with (2*1). rewrite <- 2 Zmult_plus_distr_r.
+ apply Zeven_2p.
Qed.
Theorem Zeven_mult_Zeven_l: forall a b,
Zeven a -> Zeven (a * b).
Proof.
- intros a b H1; case Zeven_ex with (1 := H1); intros x H3; try rewrite H3; auto.
- replace (2 * x * b) with (2 * (x * b)); try apply Zeven_2p; auto with zarith.
- (* ring part *)
- apply Zmult_assoc.
+ intros a b Ha.
+ destruct (Zeven_ex a) as (x,->); trivial.
+ rewrite <- Zmult_assoc.
+ apply Zeven_2p.
Qed.
Theorem Zeven_mult_Zeven_r: forall a b,
Zeven b -> Zeven (a * b).
Proof.
- intros a b H1; case Zeven_ex with (1 := H1); intros x H3; try rewrite H3; auto.
- replace (a * (2 * x)) with (2 * (x * a)); try apply Zeven_2p; auto.
- (* ring part *)
- rewrite (Zmult_comm x a).
- do 2 rewrite Zmult_assoc.
- rewrite (Zmult_comm 2 a); auto.
+ intros a b Hb. rewrite Zmult_comm. now apply Zeven_mult_Zeven_l.
Qed.
Hint Rewrite Zmult_plus_distr_r Zmult_plus_distr_l
@@ -375,14 +361,11 @@ Hint Rewrite Zmult_plus_distr_r Zmult_plus_distr_l
Theorem Zodd_mult_Zodd: forall a b,
Zodd a -> Zodd b -> Zodd (a * b).
Proof.
- intros a b H1 H2; case Zodd_ex with (1 := H1); intros x H3; try rewrite H3; auto.
- case Zodd_ex with (1 := H2); intros y H4; try rewrite H4; auto.
- replace ((2 * x + 1) * (2 * y + 1)) with (2 * (2 * x * y + x + y) + 1); try apply Zodd_2p_plus_1; auto.
- (* ring part *)
- autorewrite with Zexpand; f_equal.
- repeat rewrite <- Zplus_assoc; f_equal.
- repeat rewrite <- Zmult_assoc; f_equal.
- repeat rewrite Zmult_assoc; f_equal; apply Zmult_comm.
+ intros a b Ha Hb.
+ destruct (Zodd_ex a) as (x,->), (Zodd_ex b) as (y,->); trivial.
+ rewrite Zmult_plus_distr_l, Zmult_1_l.
+ rewrite <- Zmult_assoc, Zplus_assoc, <- Zmult_plus_distr_r.
+ apply Zodd_2p_plus_1.
Qed.
(* for compatibility *)
diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v
index 5fe105aa5..7f0885128 100644
--- a/theories/ZArith/Zquot.v
+++ b/theories/ZArith/Zquot.v
@@ -473,13 +473,7 @@ Qed.
(** Particular case : dividing by 2 is related with parity *)
-Lemma Zdiv2_odd_eq : forall a,
- a = 2 * Zdiv2 a + if Zodd_bool a then Zsgn a else 0.
-Proof.
- destruct a as [ |p|p]; try destruct p; trivial.
-Qed.
-
-Lemma Zdiv2_odd_remainder : forall a,
+Lemma Zquot2_odd_remainder : forall a,
Remainder a 2 (if Zodd_bool a then Zsgn a else 0).
Proof.
intros [ |p|p]. simpl.
@@ -488,20 +482,20 @@ Proof.
right. destruct p; simpl; split; now auto with zarith.
Qed.
-Lemma Zdiv2_quot : forall a, Zdiv2 a = a÷2.
+Lemma Zquot2_quot : forall a, Zquot2 a = a÷2.
Proof.
intros.
apply Zquot_unique_full with (if Zodd_bool a then Zsgn a else 0).
- apply Zdiv2_odd_remainder.
- apply Zdiv2_odd_eq.
+ apply Zquot2_odd_remainder.
+ apply Zquot2_odd_eqn.
Qed.
Lemma Zrem_odd : forall a, Zrem a 2 = if Zodd_bool a then Zsgn a else 0.
Proof.
intros. symmetry.
- apply Zrem_unique_full with (Zdiv2 a).
- apply Zdiv2_odd_remainder.
- apply Zdiv2_odd_eq.
+ apply Zrem_unique_full with (Zquot2 a).
+ apply Zquot2_odd_remainder.
+ apply Zquot2_odd_eqn.
Qed.
Lemma Zrem_even : forall a, Zrem a 2 = if Zeven_bool a then 0 else Zsgn a.
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-11 08:55:36 +0000