|
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. |
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.
|
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.