diff options
Diffstat (limited to 'theories/ZArith/Zdiv.v')
| -rw-r--r-- | theories/ZArith/Zdiv.v | 423 |
1 files changed, 423 insertions, 0 deletions
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v new file mode 100644 index 00000000..84eb2259 --- /dev/null +++ b/theories/ZArith/Zdiv.v @@ -0,0 +1,423 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Zdiv.v,v 1.21.2.1 2004/07/16 19:31:21 herbelin Exp $ 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. + +*) + +Require Export ZArith_base. +Require Import Zbool. +Require Import Omega. +Require Import ZArithRing. +Require Import Zcomplements. +Open Local Scope Z_scope. + +(** + + 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 + +*) + +Fixpoint Zdiv_eucl_POS (a:positive) (b:Z) {struct a} : + Z * Z := + match a with + | 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 (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) + end. + + +(** + + Euclidean division of integers. + + Total function than returns (0,0) when dividing by 0. + +*) + +(* + + The pseudo-code is: + + if b = 0 : (0,0) + + if b <> 0 and a = 0 : (0,0) + + if b > 0 and a < 0 : let (q,r) = div_eucl_pos (-a) b in + if r = 0 then (-q,0) else (-(q+1),b-r) + + if b < 0 and a < 0 : let (q,r) = div_eucl (-a) (-b) in (q,-r) + + if b < 0 and a > 0 : let (q,r) = div_eucl a (-b) in + if r = 0 then (-q,0) else (-(q+1),b+r) + + In other word, when b is non-zero, q is chosen to be the greatest integer + smaller or equal to a/b. And sgn(r)=sgn(b) and |r| < |b|. + +*) + +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 _ => + 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' => + let (q, r) := Zdiv_eucl_POS a' (Zpos b') in + match r with + | Z0 => (- q, 0) + | _ => (- (q + 1), b + r) + end + end. + + +(** Division and modulo are projections of [Zdiv_eucl] *) + +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. + +(* Tests: + +Eval Compute in `(Zdiv_eucl 7 3)`. + +Eval Compute in `(Zdiv_eucl (-7) 3)`. + +Eval Compute in `(Zdiv_eucl 7 (-3))`. + +Eval Compute in `(Zdiv_eucl (-7) (-3))`. + +*) + + +(** + + 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. +Proof. +simple induction a; unfold Zdiv_eucl_POS in |- *; fold Zdiv_eucl_POS in |- *. + +intro p; case (Zdiv_eucl_POS p b); intros q r [H0 H1]. +generalize (Zgt_cases b (2 * r + 1)). +case (Zgt_bool b (2 * r + 1)); + (rewrite BinInt.Zpos_xI; rewrite H0; split; [ ring | omega ]). + +intros p; case (Zdiv_eucl_POS p b); intros q r [H0 H1]. +generalize (Zgt_cases b (2 * r)). +case (Zgt_bool b (2 * r)); rewrite BinInt.Zpos_xO; + change (Zpos (xO p)) with (2 * Zpos p) in |- *; rewrite H0; + (split; [ ring | omega ]). + +generalize (Zge_cases b 2). +case (Zge_bool b 2); (intros; split; [ 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. +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. +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}. +Proof. +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}. +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 ]. +Qed. + +Implicit Arguments Zdiv_eucl_extended. + +(** 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. +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. +Qed. + +Lemma Z_div_POS_ge0 : + 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. +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. +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. +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]). *) + +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. +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. +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. +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. +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. +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. +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. +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. +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. +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. +Qed. |