diff options
Diffstat (limited to 'theories/ZArith/Zdiv.v')
| -rw-r--r-- | theories/ZArith/Zdiv.v | 476 |
1 files changed, 232 insertions, 244 deletions
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index e391d087..31f68207 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -6,17 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zdiv.v 6295 2004-11-12 16:40:39Z gregoire $ i*) +(*i $Id: Zdiv.v 9245 2006-10-17 12:53:34Z notin $ i*) (* Contribution by Claude Marché and Xavier Urbain *) -(** - -Euclidean Division - -Defines first of function that allows Coq to normalize. -Then only after proves the main required property. +(** Euclidean Division + Defines first of function that allows Coq to normalize. + Then only after proves the main required property. *) Require Export ZArith_base. @@ -26,40 +23,37 @@ Require Import ZArithRing. Require Import Zcomplements. Open Local Scope Z_scope. -(** +(** * Definitions of Euclidian operations *) - Euclidean division of a positive by a integer - (that is supposed to be positive). +(** Euclidean division of a positive by a integer + (that is supposed to be positive). - total function than returns an arbitrary value when - divisor is not positive + Total function than returns an arbitrary value when + divisor is not positive *) Unboxed Fixpoint Zdiv_eucl_POS (a:positive) (b:Z) {struct a} : - Z * Z := + Z * Z := match a with - | xH => if Zge_bool b 2 then (0, 1) else (1, 0) - | xO a' => + | xH => if Zge_bool b 2 then (0, 1) else (1, 0) + | xO a' => let (q, r) := Zdiv_eucl_POS a' b in - let r' := 2 * r in - if Zgt_bool b r' then (2 * q, r') else (2 * q + 1, r' - b) - | xI a' => + let r' := 2 * r in + if Zgt_bool b r' then (2 * q, r') else (2 * q + 1, r' - b) + | xI a' => let (q, r) := Zdiv_eucl_POS a' b in - let r' := 2 * r + 1 in - if Zgt_bool b r' then (2 * q, r') else (2 * q + 1, r' - b) + let r' := 2 * r + 1 in + if Zgt_bool b r' then (2 * q, r') else (2 * q + 1, r' - b) end. -(** - - Euclidean division of integers. +(** Euclidean division of integers. - Total function than returns (0,0) when dividing by 0. - + Total function than returns (0,0) when dividing by 0. *) -(* +(** The pseudo-code is: @@ -82,22 +76,22 @@ Unboxed Fixpoint Zdiv_eucl_POS (a:positive) (b:Z) {struct a} : Definition Zdiv_eucl (a b:Z) : Z * Z := match a, b with - | Z0, _ => (0, 0) - | _, Z0 => (0, 0) - | Zpos a', Zpos _ => Zdiv_eucl_POS a' b - | Zneg a', Zpos _ => + | Z0, _ => (0, 0) + | _, Z0 => (0, 0) + | Zpos a', Zpos _ => Zdiv_eucl_POS a' b + | Zneg a', Zpos _ => let (q, r) := Zdiv_eucl_POS a' b in - match r with - | Z0 => (- q, 0) - | _ => (- (q + 1), b - r) - end - | Zneg a', Zneg b' => let (q, r) := Zdiv_eucl_POS a' (Zpos b') in (q, - r) - | Zpos a', Zneg b' => + match r with + | Z0 => (- q, 0) + | _ => (- (q + 1), b - r) + end + | Zneg a', Zneg b' => let (q, r) := Zdiv_eucl_POS a' (Zpos b') in (q, - r) + | Zpos a', Zneg b' => let (q, r) := Zdiv_eucl_POS a' (Zpos b') in - match r with - | Z0 => (- q, 0) - | _ => (- (q + 1), b + r) - end + match r with + | Z0 => (- q, 0) + | _ => (- (q + 1), b + r) + end end. @@ -107,6 +101,11 @@ Definition Zdiv (a b:Z) : Z := let (q, _) := Zdiv_eucl a b in q. Definition Zmod (a b:Z) : Z := let (_, r) := Zdiv_eucl a b in r. +(** Syntax *) + +Infix "/" := Zdiv : Z_scope. +Infix "mod" := Zmod (at level 40, no associativity) : Z_scope. + (* Tests: Eval Compute in `(Zdiv_eucl 7 3)`. @@ -120,19 +119,15 @@ Eval Compute in `(Zdiv_eucl (-7) (-3))`. *) -(** - - Main division theorem. - - First a lemma for positive +(** * Main division theorem *) -*) +(** First a lemma for positive *) Lemma Z_div_mod_POS : - forall b:Z, - b > 0 -> - forall a:positive, - let (q, r) := Zdiv_eucl_POS a b in Zpos a = b * q + r /\ 0 <= r < b. + forall b:Z, + b > 0 -> + forall a:positive, + let (q, r) := Zdiv_eucl_POS a b in Zpos a = b * q + r /\ 0 <= r < b. Proof. simple induction a; unfold Zdiv_eucl_POS in |- *; fold Zdiv_eucl_POS in |- *. @@ -148,276 +143,269 @@ case (Zgt_bool b (2 * r)); rewrite BinInt.Zpos_xO; (split; [ ring | omega ]). generalize (Zge_cases b 2). -case (Zge_bool b 2); (intros; split; [ ring | omega ]). +case (Zge_bool b 2); (intros; split; [ try ring | omega ]). omega. Qed. Theorem Z_div_mod : - forall a b:Z, - b > 0 -> let (q, r) := Zdiv_eucl a b in a = b * q + r /\ 0 <= r < b. + forall a b:Z, + b > 0 -> let (q, r) := Zdiv_eucl a b in a = b * q + r /\ 0 <= r < b. Proof. -intros a b; case a; case b; try (simpl in |- *; intros; omega). -unfold Zdiv_eucl in |- *; intros; apply Z_div_mod_POS; trivial. - -intros; discriminate. - -intros. -generalize (Z_div_mod_POS (Zpos p) H p0). -unfold Zdiv_eucl in |- *. -case (Zdiv_eucl_POS p0 (Zpos p)). -intros z z0. -case z0. - -intros [H1 H2]. -split; trivial. -replace (Zneg p0) with (- Zpos p0); [ rewrite H1; ring | trivial ]. - -intros p1 [H1 H2]. -split; trivial. -replace (Zneg p0) with (- Zpos p0); [ rewrite H1; ring | trivial ]. -generalize (Zorder.Zgt_pos_0 p1); omega. - -intros p1 [H1 H2]. -split; trivial. -replace (Zneg p0) with (- Zpos p0); [ rewrite H1; ring | trivial ]. -generalize (Zorder.Zlt_neg_0 p1); omega. - -intros; discriminate. + intros a b; case a; case b; try (simpl in |- *; intros; omega). + unfold Zdiv_eucl in |- *; intros; apply Z_div_mod_POS; trivial. + + intros; discriminate. + + intros. + generalize (Z_div_mod_POS (Zpos p) H p0). + unfold Zdiv_eucl in |- *. + case (Zdiv_eucl_POS p0 (Zpos p)). + intros z z0. + case z0. + + intros [H1 H2]. + split; trivial. + replace (Zneg p0) with (- Zpos p0); [ rewrite H1; ring | trivial ]. + + intros p1 [H1 H2]. + split; trivial. + replace (Zneg p0) with (- Zpos p0); [ rewrite H1; ring | trivial ]. + generalize (Zorder.Zgt_pos_0 p1); omega. + + intros p1 [H1 H2]. + split; trivial. + replace (Zneg p0) with (- Zpos p0); [ rewrite H1; ring | trivial ]. + generalize (Zorder.Zlt_neg_0 p1); omega. + + intros; discriminate. Qed. (** Existence theorems *) Theorem Zdiv_eucl_exist : - forall b:Z, - b > 0 -> - forall a:Z, {qr : Z * Z | let (q, r) := qr in a = b * q + r /\ 0 <= r < b}. + forall b:Z, + b > 0 -> + forall a:Z, {qr : Z * Z | let (q, r) := qr in a = b * q + r /\ 0 <= r < b}. Proof. -intros b Hb a. -exists (Zdiv_eucl a b). -exact (Z_div_mod a b Hb). + intros b Hb a. + exists (Zdiv_eucl a b). + exact (Z_div_mod a b Hb). Qed. Implicit Arguments Zdiv_eucl_exist. Theorem Zdiv_eucl_extended : - forall b:Z, - b <> 0 -> - forall a:Z, - {qr : Z * Z | let (q, r) := qr in a = b * q + r /\ 0 <= r < Zabs b}. + forall b:Z, + b <> 0 -> + forall a:Z, + {qr : Z * Z | let (q, r) := qr in a = b * q + r /\ 0 <= r < Zabs b}. Proof. -intros b Hb a. -elim (Z_le_gt_dec 0 b); intro Hb'. -cut (b > 0); [ intro Hb'' | omega ]. -rewrite Zabs_eq; [ apply Zdiv_eucl_exist; assumption | assumption ]. -cut (- b > 0); [ intro Hb'' | omega ]. -elim (Zdiv_eucl_exist Hb'' a); intros qr. -elim qr; intros q r Hqr. -exists (- q, r). -elim Hqr; intros. -split. -rewrite <- Zmult_opp_comm; assumption. -rewrite Zabs_non_eq; [ assumption | omega ]. + intros b Hb a. + elim (Z_le_gt_dec 0 b); intro Hb'. + cut (b > 0); [ intro Hb'' | omega ]. + rewrite Zabs_eq; [ apply Zdiv_eucl_exist; assumption | assumption ]. + cut (- b > 0); [ intro Hb'' | omega ]. + elim (Zdiv_eucl_exist Hb'' a); intros qr. + elim qr; intros q r Hqr. + exists (- q, r). + elim Hqr; intros. + split. + rewrite <- Zmult_opp_comm; assumption. + rewrite Zabs_non_eq; [ assumption | omega ]. Qed. Implicit Arguments Zdiv_eucl_extended. -(** Auxiliary lemmas about [Zdiv] and [Zmod] *) +(** * Auxiliary lemmas about [Zdiv] and [Zmod] *) Lemma Z_div_mod_eq : forall a b:Z, b > 0 -> a = b * Zdiv a b + Zmod a b. Proof. -unfold Zdiv, Zmod in |- *. -intros a b Hb. -generalize (Z_div_mod a b Hb). -case Zdiv_eucl; tauto. + unfold Zdiv, Zmod in |- *. + intros a b Hb. + generalize (Z_div_mod a b Hb). + case Zdiv_eucl; tauto. Qed. Lemma Z_mod_lt : forall a b:Z, b > 0 -> 0 <= Zmod a b < b. Proof. -unfold Zmod in |- *. -intros a b Hb. -generalize (Z_div_mod a b Hb). -case (Zdiv_eucl a b); tauto. + unfold Zmod in |- *. + intros a b Hb. + generalize (Z_div_mod a b Hb). + case (Zdiv_eucl a b); tauto. Qed. Lemma Z_div_POS_ge0 : - forall (b:Z) (a:positive), let (q, _) := Zdiv_eucl_POS a b in q >= 0. + forall (b:Z) (a:positive), let (q, _) := Zdiv_eucl_POS a b in q >= 0. Proof. -simple induction a; unfold Zdiv_eucl_POS in |- *; fold Zdiv_eucl_POS in |- *. -intro p; case (Zdiv_eucl_POS p b). -intros; case (Zgt_bool b (2 * z0 + 1)); intros; omega. -intro p; case (Zdiv_eucl_POS p b). -intros; case (Zgt_bool b (2 * z0)); intros; omega. -case (Zge_bool b 2); simpl in |- *; omega. + simple induction a; unfold Zdiv_eucl_POS in |- *; fold Zdiv_eucl_POS in |- *. + intro p; case (Zdiv_eucl_POS p b). + intros; case (Zgt_bool b (2 * z0 + 1)); intros; omega. + intro p; case (Zdiv_eucl_POS p b). + intros; case (Zgt_bool b (2 * z0)); intros; omega. + case (Zge_bool b 2); simpl in |- *; omega. Qed. Lemma Z_div_ge0 : forall a b:Z, b > 0 -> a >= 0 -> Zdiv a b >= 0. Proof. -intros a b Hb; unfold Zdiv, Zdiv_eucl in |- *; case a; simpl in |- *; intros. -case b; simpl in |- *; trivial. -generalize Hb; case b; try trivial. -auto with zarith. -intros p0 Hp0; generalize (Z_div_POS_ge0 (Zpos p0) p). -case (Zdiv_eucl_POS p (Zpos p0)); simpl in |- *; tauto. -intros; discriminate. -elim H; trivial. + intros a b Hb; unfold Zdiv, Zdiv_eucl in |- *; case a; simpl in |- *; intros. + case b; simpl in |- *; trivial. + generalize Hb; case b; try trivial. + auto with zarith. + intros p0 Hp0; generalize (Z_div_POS_ge0 (Zpos p0) p). + case (Zdiv_eucl_POS p (Zpos p0)); simpl in |- *; tauto. + intros; discriminate. + elim H; trivial. Qed. Lemma Z_div_lt : forall a b:Z, b >= 2 -> a > 0 -> Zdiv a b < a. Proof. -intros. cut (b > 0); [ intro Hb | omega ]. -generalize (Z_div_mod a b Hb). -cut (a >= 0); [ intro Ha | omega ]. -generalize (Z_div_ge0 a b Hb Ha). -unfold Zdiv in |- *; case (Zdiv_eucl a b); intros q r H1 [H2 H3]. -cut (a >= 2 * q -> q < a); [ intro h; apply h; clear h | intros; omega ]. -apply Zge_trans with (b * q). -omega. -auto with zarith. + intros. cut (b > 0); [ intro Hb | omega ]. + generalize (Z_div_mod a b Hb). + cut (a >= 0); [ intro Ha | omega ]. + generalize (Z_div_ge0 a b Hb Ha). + unfold Zdiv in |- *; case (Zdiv_eucl a b); intros q r H1 [H2 H3]. + cut (a >= 2 * q -> q < a); [ intro h; apply h; clear h | intros; omega ]. + apply Zge_trans with (b * q). + omega. + auto with zarith. Qed. -(** Syntax *) - - - -Infix "/" := Zdiv : Z_scope. -Infix "mod" := Zmod (at level 40, no associativity) : Z_scope. - -(** Other lemmas (now using the syntax for [Zdiv] and [Zmod]). *) +(** * Other lemmas (now using the syntax for [Zdiv] and [Zmod]). *) Lemma Z_div_ge : forall a b c:Z, c > 0 -> a >= b -> a / c >= b / c. Proof. -intros a b c cPos aGeb. -generalize (Z_div_mod_eq a c cPos). -generalize (Z_mod_lt a c cPos). -generalize (Z_div_mod_eq b c cPos). -generalize (Z_mod_lt b c cPos). -intros. -elim (Z_ge_lt_dec (a / c) (b / c)); trivial. -intro. -absurd (b - a >= 1). -omega. -rewrite H0. -rewrite H2. -assert - (c * (b / c) + b mod c - (c * (a / c) + a mod c) = - c * (b / c - a / c) + b mod c - a mod c). -ring. -rewrite H3. -assert (c * (b / c - a / c) >= c * 1). -apply Zmult_ge_compat_l. -omega. -omega. -assert (c * 1 = c). -ring. -omega. + intros a b c cPos aGeb. + generalize (Z_div_mod_eq a c cPos). + generalize (Z_mod_lt a c cPos). + generalize (Z_div_mod_eq b c cPos). + generalize (Z_mod_lt b c cPos). + intros. + elim (Z_ge_lt_dec (a / c) (b / c)); trivial. + intro. + absurd (b - a >= 1). + omega. + rewrite H0. + rewrite H2. + assert + (c * (b / c) + b mod c - (c * (a / c) + a mod c) = + c * (b / c - a / c) + b mod c - a mod c). + ring. + rewrite H3. + assert (c * (b / c - a / c) >= c * 1). + apply Zmult_ge_compat_l. + omega. + omega. + assert (c * 1 = c). + ring. + omega. Qed. Lemma Z_mod_plus : forall a b c:Z, c > 0 -> (a + b * c) mod c = a mod c. Proof. -intros a b c cPos. -generalize (Z_div_mod_eq a c cPos). -generalize (Z_mod_lt a c cPos). -generalize (Z_div_mod_eq (a + b * c) c cPos). -generalize (Z_mod_lt (a + b * c) c cPos). -intros. - -assert ((a + b * c) mod c - a mod c = c * (b + a / c - (a + b * c) / c)). -replace ((a + b * c) mod c) with (a + b * c - c * ((a + b * c) / c)). -replace (a mod c) with (a - c * (a / c)). -ring. -omega. -omega. -set (q := b + a / c - (a + b * c) / c) in *. -apply (Zcase_sign q); intros. -assert (c * q = 0). -rewrite H4; ring. -rewrite H5 in H3. -omega. - -assert (c * q >= c). -pattern c at 2 in |- *; replace c with (c * 1). -apply Zmult_ge_compat_l; omega. -ring. -omega. - -assert (c * q <= - c). -replace (- c) with (c * -1). -apply Zmult_le_compat_l; omega. -ring. -omega. + intros a b c cPos. + generalize (Z_div_mod_eq a c cPos). + generalize (Z_mod_lt a c cPos). + generalize (Z_div_mod_eq (a + b * c) c cPos). + generalize (Z_mod_lt (a + b * c) c cPos). + intros. + + assert ((a + b * c) mod c - a mod c = c * (b + a / c - (a + b * c) / c)). + replace ((a + b * c) mod c) with (a + b * c - c * ((a + b * c) / c)). + replace (a mod c) with (a - c * (a / c)). + ring. + omega. + omega. + set (q := b + a / c - (a + b * c) / c) in *. + apply (Zcase_sign q); intros. + assert (c * q = 0). + rewrite H4; ring. + rewrite H5 in H3. + omega. + + assert (c * q >= c). + pattern c at 2 in |- *; replace c with (c * 1). + apply Zmult_ge_compat_l; omega. + ring. + omega. + + assert (c * q <= - c). + replace (- c) with (c * -1). + apply Zmult_le_compat_l; omega. + ring. + omega. Qed. Lemma Z_div_plus : forall a b c:Z, c > 0 -> (a + b * c) / c = a / c + b. Proof. -intros a b c cPos. -generalize (Z_div_mod_eq a c cPos). -generalize (Z_mod_lt a c cPos). -generalize (Z_div_mod_eq (a + b * c) c cPos). -generalize (Z_mod_lt (a + b * c) c cPos). -intros. -apply Zmult_reg_l with c. omega. -replace (c * ((a + b * c) / c)) with (a + b * c - (a + b * c) mod c). -rewrite (Z_mod_plus a b c cPos). -pattern a at 1 in |- *; rewrite H2. -ring. -pattern (a + b * c) at 1 in |- *; rewrite H0. -ring. + intros a b c cPos. + generalize (Z_div_mod_eq a c cPos). + generalize (Z_mod_lt a c cPos). + generalize (Z_div_mod_eq (a + b * c) c cPos). + generalize (Z_mod_lt (a + b * c) c cPos). + intros. + apply Zmult_reg_l with c. omega. + replace (c * ((a + b * c) / c)) with (a + b * c - (a + b * c) mod c). + rewrite (Z_mod_plus a b c cPos). + pattern a at 1 in |- *; rewrite H2. + ring. + pattern (a + b * c) at 1 in |- *; rewrite H0. + ring. Qed. Lemma Z_div_mult : forall a b:Z, b > 0 -> a * b / b = a. -intros; replace (a * b) with (0 + a * b); auto. -rewrite Z_div_plus; auto. + intros; replace (a * b) with (0 + a * b); auto. + rewrite Z_div_plus; auto. Qed. Lemma Z_mult_div_ge : forall a b:Z, b > 0 -> b * (a / b) <= a. Proof. -intros a b bPos. -generalize (Z_div_mod_eq a _ bPos); intros. -generalize (Z_mod_lt a _ bPos); intros. -pattern a at 2 in |- *; rewrite H. -omega. + intros a b bPos. + generalize (Z_div_mod_eq a _ bPos); intros. + generalize (Z_mod_lt a _ bPos); intros. + pattern a at 2 in |- *; rewrite H. + omega. Qed. Lemma Z_mod_same : forall a:Z, a > 0 -> a mod a = 0. Proof. -intros a aPos. -generalize (Z_mod_plus 0 1 a aPos). -replace (0 + 1 * a) with a. -intros. -rewrite H. -compute in |- *. -trivial. -ring. + intros a aPos. + generalize (Z_mod_plus 0 1 a aPos). + replace (0 + 1 * a) with a. + intros. + rewrite H. + compute in |- *. + trivial. + ring. Qed. Lemma Z_div_same : forall a:Z, a > 0 -> a / a = 1. Proof. -intros a aPos. -generalize (Z_div_plus 0 1 a aPos). -replace (0 + 1 * a) with a. -intros. -rewrite H. -compute in |- *. -trivial. -ring. + intros a aPos. + generalize (Z_div_plus 0 1 a aPos). + replace (0 + 1 * a) with a. + intros. + rewrite H. + compute in |- *. + trivial. + ring. Qed. Lemma Z_div_exact_1 : forall a b:Z, b > 0 -> a = b * (a / b) -> a mod b = 0. -intros a b Hb; generalize (Z_div_mod a b Hb); unfold Zmod, Zdiv in |- *. -case (Zdiv_eucl a b); intros q r; omega. + intros a b Hb; generalize (Z_div_mod a b Hb); unfold Zmod, Zdiv in |- *. + case (Zdiv_eucl a b); intros q r; omega. Qed. Lemma Z_div_exact_2 : forall a b:Z, b > 0 -> a mod b = 0 -> a = b * (a / b). -intros a b Hb; generalize (Z_div_mod a b Hb); unfold Zmod, Zdiv in |- *. -case (Zdiv_eucl a b); intros q r; omega. + intros a b Hb; generalize (Z_div_mod a b Hb); unfold Zmod, Zdiv in |- *. + case (Zdiv_eucl a b); intros q r; omega. Qed. Lemma Z_mod_zero_opp : forall a b:Z, b > 0 -> a mod b = 0 -> - a mod b = 0. -intros a b Hb. -intros. -rewrite Z_div_exact_2 with a b; auto. -replace (- (b * (a / b))) with (0 + - (a / b) * b). -rewrite Z_mod_plus; auto. -ring. + intros a b Hb. + intros. + rewrite Z_div_exact_2 with a b; auto. + replace (- (b * (a / b))) with (0 + - (a / b) * b). + rewrite Z_mod_plus; auto. + ring. Qed. |