Library Float.Zdivides

Require Export Omega.
Require Export Paux.

Definition oZ1 (x : Option positive) :=
  match x with
  | None ⇒ 0%Z
  | Some zZpos z
  end.

Definition Zquotient (n m : Z) :=
  match n, m with
  | Z0, _ ⇒ 0%Z
  | _, Z0 ⇒ 0%Z
  | Zpos x, Zpos ymatch Pdiv x y with
                      | (x, _)oZ1 x
                      end
  | Zneg x, Zneg ymatch Pdiv x y with
                      | (x, _)oZ1 x
                      end
  | Zpos x, Zneg ymatch Pdiv x y with
                      | (x, _) ⇒ (- oZ1 x)%Z
                      end
  | Zneg x, Zpos ymatch Pdiv x y with
                      | (x, _) ⇒ (- oZ1 x)%Z
                      end
  end.

Theorem inj_oZ1 : z, oZ1 z = Z_of_nat (oZ z).
intros z; case z; simpl in |- *;
 try (intros; apply sym_equal; apply inject_nat_convert; auto);
 auto.
Qed.

Theorem Zero_le_oZ : z, 0 oZ z.
intros z; case z; simpl in |- *; auto with arith.
Qed.
Hint Resolve Zero_le_oZ: arith.

Theorem ZquotientProp :
  m n : Z,
 n 0%Z
 ex
   (fun r : Z
    m = (Zquotient m n × n + r)%Z
    (Z.abs (Zquotient m n × n) Z.abs m)%Z (Z.abs r < Z.abs n)%Z).
intros m n; unfold Zquotient in |- *; case n; simpl in |- ×.
intros H; case H; auto.
intros n' Hn'; case m; simpl in |- *; auto.
0%Z; repeat split; simpl in |- *; auto with zarith.
intros m'; generalize (Pdiv_correct m' n'); case (Pdiv m' n'); simpl in |- *;
 auto.
intros q r (H1, H2); (oZ1 r); repeat (split; auto with zarith).
rewrite <- (inject_nat_convert (Zpos m') m'); auto.
rewrite H1.
rewrite inj_plus; rewrite inj_mult.
rewrite <- (inject_nat_convert (Zpos n') n'); auto.
repeat rewrite inj_oZ1; auto.
rewrite inj_oZ1; rewrite Z.abs_eq; auto with zarith.
rewrite <- (inject_nat_convert (Zpos m') m'); auto with zarith.
rewrite <- (inject_nat_convert (Zpos n') n'); auto with zarith.
rewrite inj_oZ1; rewrite Z.abs_eq; auto with zarith.
rewrite <- (inject_nat_convert (Zpos n') n'); auto with zarith.
intros m'; generalize (Pdiv_correct m' n'); case (Pdiv m' n'); simpl in |- *;
 auto.
intros q r (H1, H2); (- oZ1 r)%Z; repeat (split; auto with zarith).
replace (Zneg m') with (- Zpos m')%Z; [ idtac | simpl in |- *; auto ].
rewrite <- (inject_nat_convert (Zpos m') m'); auto.
rewrite H1.
rewrite inj_plus; rewrite inj_mult.
rewrite <- (inject_nat_convert (Zpos n') n'); auto.
repeat rewrite inj_oZ1; auto with zarith.
ring.
rewrite <- Zopp_mult_distr_l; rewrite Zabs_Zopp.
rewrite inj_oZ1; rewrite Z.abs_eq; auto with zarith.
rewrite <- (inject_nat_convert (Zpos m') m'); auto with zarith.
rewrite <- (inject_nat_convert (Zpos n') n'); auto with zarith.
rewrite Zabs_Zopp.
rewrite inj_oZ1; rewrite Z.abs_eq; auto with zarith.
rewrite <- (inject_nat_convert (Zpos n') n'); auto with zarith.
intros n' Hn'; case m; simpl in |- *; auto.
0%Z; repeat split; simpl in |- *; auto with zarith.
intros m'; generalize (Pdiv_correct m' n'); case (Pdiv m' n'); simpl in |- *;
 auto.
intros q r (H1, H2); (oZ1 r); repeat (split; auto with zarith).
replace (Zneg n') with (- Zpos n')%Z; [ idtac | simpl in |- *; auto ].
rewrite <- (inject_nat_convert (Zpos m') m'); auto.
rewrite H1.
rewrite inj_plus; rewrite inj_mult.
rewrite <- (inject_nat_convert (Zpos n') n'); auto.
repeat rewrite inj_oZ1; auto with zarith.
ring.
replace (Zneg n') with (- Zpos n')%Z; [ idtac | simpl in |- *; auto ].
rewrite Zmult_opp_opp.
rewrite inj_oZ1; rewrite Z.abs_eq; auto with zarith.
rewrite <- (inject_nat_convert (Zpos n') n'); auto with zarith.
rewrite <- (inject_nat_convert (Zpos m') m'); auto with zarith.
rewrite inj_oZ1; rewrite Z.abs_eq; auto with zarith.
rewrite <- (inject_nat_convert (Zpos n') n'); auto with zarith.
intros m'; generalize (Pdiv_correct m' n'); case (Pdiv m' n'); simpl in |- *;
 auto.
intros q r (H1, H2); (- oZ1 r)%Z; repeat (split; auto with zarith).
replace (Zneg m') with (- Zpos m')%Z; [ idtac | simpl in |- *; auto ].
rewrite <- (inject_nat_convert (Zpos m') m'); auto.
replace (Zneg n') with (- Zpos n')%Z; [ idtac | simpl in |- *; auto ].
rewrite H1.
rewrite inj_plus; rewrite inj_mult.
rewrite <- (inject_nat_convert (Zpos n') n'); auto.
repeat rewrite inj_oZ1; auto with zarith.
ring.
replace (Zneg n') with (- Zpos n')%Z; [ idtac | simpl in |- *; auto ].
rewrite <- Zopp_mult_distr_r; rewrite Zabs_Zopp.
rewrite inj_oZ1; rewrite Z.abs_eq; auto with zarith.
rewrite <- (inject_nat_convert (Zpos m') m'); auto with zarith.
rewrite <- (inject_nat_convert (Zpos n') n'); auto with zarith.
rewrite Zabs_Zopp.
rewrite inj_oZ1; rewrite Z.abs_eq; auto with zarith.
rewrite <- (inject_nat_convert (Zpos n') n'); auto with zarith.
Qed.

Theorem ZquotientPos :
  z1 z2 : Z, (0 z1)%Z (0 z2)%Z (0 Zquotient z1 z2)%Z.
intros z1 z2 H H0; case (Z.eq_dec z2 0); intros Z1.
rewrite Z1; red in |- *; case z1; simpl in |- *; auto; intros; red in |- *;
 intros; discriminate.
case (ZquotientProp z1 z2); auto; intros r (H1, (H2, H3)).
case (Zle_or_lt 0 (Zquotient z1 z2)); auto; intros Z2.
Contradict H3; apply Zle_not_lt.
replace r with (z1 - Zquotient z1 z2 × z2)%Z;
 [ idtac | pattern z1 at 1 in |- *; rewrite H1; ring ].
repeat rewrite Z.abs_eq; auto.
pattern z2 at 1 in |- *; replace z2 with (0 + 1 × z2)%Z; [ idtac | ring ].
unfold Zminus in |- *; apply Z.le_trans with (z1 + 1 × z2)%Z; auto with zarith.
apply Zplus_le_compat_l.
rewrite Zopp_mult_distr_l.
apply Zle_Zmult_comp_r; auto with zarith.
unfold Zminus in |- *; rewrite Zopp_mult_distr_l; auto with zarith.
Qed.

Definition Zdivides (n m : Z) := q : Z, n = (m × q)%Z.

Theorem ZdividesZquotient :
  n m : Z, m 0%Z Zdivides n m n = (Zquotient n m × m)%Z.
intros n m H' H'0.
case H'0; intros z1 Hz1.
case (ZquotientProp n m); auto; intros z2 (Hz2, (Hz3, Hz4)).
cut (z2 = 0%Z);
 [ intros H1; pattern n at 1 in |- *; rewrite Hz2; rewrite H1; ring | idtac ].
cut (z2 = ((z1 - Zquotient n m) × m)%Z); [ intros H2 | idtac ].
case (Z.eq_dec (z1 - Zquotient n m) 0); intros H3.
rewrite H2; rewrite H3; ring.
Contradict Hz4.
replace (Z.abs m) with (1 × Z.abs m)%Z; [ idtac | ring ].
apply Zle_not_lt; rewrite H2.
rewrite Zabs_Zmult; apply Zle_Zmult_comp_r; auto with zarith.
generalize H3; case (z1 - Zquotient n m)%Z;
 try (intros H1; case H1; auto; fail); simpl in |- *;
 intros p; case p; simpl in |- *; auto; intros; red in |- *;
 simpl in |- *; auto; red in |- *; intros; discriminate.
rewrite Zmult_minus_distr_r; rewrite (Zmult_comm z1); rewrite <- Hz1;
 (pattern n at 1 in |- *; rewrite Hz2); ring.
Qed.

Theorem ZdividesZquotientInv :
  n m : Z, n = (Zquotient n m × m)%Z Zdivides n m.
intros n m H'; red in |- ×.
(Zquotient n m); auto.
pattern n at 1 in |- *; rewrite H'; auto with zarith.
Qed.

Theorem ZdividesMult :
  n m p : Z, Zdivides n m Zdivides (p × n) (p × m).
intros n m p H'; red in H'.
elim H'; intros q E.
red in |- ×.
q.
rewrite E.
auto with zarith.
Qed.

Theorem Zeq_mult_simpl :
  a b c : Z, c 0%Z (a × c)%Z = (b × c)%Z a = b.
intros a b c H H0.
case (Zle_or_lt c 0); intros Zl1.
apply Zle_antisym; apply Zmult_le_reg_r with (p := (- c)%Z); try apply Z.lt_gt;
 auto with zarith; repeat rewrite <- Zopp_mult_distr_r;
 rewrite H0; auto with zarith.
apply Zle_antisym; apply Zmult_le_reg_r with (p := c); try apply Z.lt_gt;
 auto with zarith; rewrite H0; auto with zarith.
Qed.

Theorem ZdividesDiv :
  n m p : Z, p 0%Z Zdivides (p × n) (p × m) Zdivides n m.
intros n m p H' H'0.
case H'0; intros q E.
q.
apply Zeq_mult_simpl with (c := p); auto.
rewrite (Zmult_comm n); rewrite E; ring.
Qed.

Definition ZdividesP : n m : Z, {Zdivides n m} + {¬ Zdivides n m}.
intros n m; case m.
case n.
left; red in |- *; 0%Z; auto with zarith.
intros p; right; red in |- *; intros H; case H; simpl in |- *; intros f H1;
 discriminate.
intros p; right; red in |- *; intros H; case H; simpl in |- *; intros f H1;
 discriminate.
intros p; generalize (Z_eq_bool_correct (Zquotient n (Zpos p) × Zpos p) n);
 case (Z_eq_bool (Zquotient n (Zpos p) × Zpos p) n);
 intros H1.
left; apply ZdividesZquotientInv; auto.
right; Contradict H1; apply sym_equal; apply ZdividesZquotient; auto.
red in |- *; intros; discriminate.
intros p; generalize (Z_eq_bool_correct (Zquotient n (Zneg p) × Zneg p) n);
 case (Z_eq_bool (Zquotient n (Zneg p) × Zneg p) n);
 intros H1.
left; apply ZdividesZquotientInv; auto.
right; Contradict H1; apply sym_equal; apply ZdividesZquotient; auto.
red in |- *; intros; discriminate.
Defined.

Theorem Zquotient1 : m : Z, Zquotient m 1 = m.
intros m.
case (ZquotientProp m 1); auto.
red in |- *; intros; discriminate.
intros z (H1, (H2, H3)).
pattern m at 2 in |- *; rewrite H1; replace z with 0%Z; try ring.
generalize H3; case z; simpl in |- *; auto; intros p; case p;
 unfold Z.lt in |- *; simpl in |- *; intros; discriminate.
Qed.

Theorem Zdivides1 : m : Z, Zdivides m 1.
intros m; m; auto with zarith.
Qed.

Theorem Zabs_eq_case :
  z1 z2 : Z, Z.abs z1 = Z.abs z2 z1 = z2 z1 = (- z2)%Z.
intros z1 z2; case z1; case z2; simpl in |- *; auto;
 try (intros; discriminate); intros p1 p2 H1; injection H1;
 (intros H2; rewrite H2); auto.
Qed.

Theorem Zabs_tri : z1 z2 : Z, (Z.abs (z1 + z2) Z.abs z1 + Z.abs z2)%Z.
intros z1 z2; case z1; case z2; try (simpl in |- *; auto with zarith; fail).
intros p1 p2;
 apply
  Zabs_intro with (P := fun x ⇒ (x Z.abs (Zpos p2) + Z.abs (Zneg p1))%Z);
 try rewrite Zopp_plus_distr; auto with zarith.
intros p1 p2;
 apply
  Zabs_intro with (P := fun x ⇒ (x Z.abs (Zpos p2) + Z.abs (Zneg p1))%Z);
 try rewrite Zopp_plus_distr; auto with zarith.
Qed.
Hint Resolve Zabs_tri: zarith.

Theorem ZquotientUnique :
  m n q r : Z,
 n 0%Z
 m = (q × n + r)%Z
 (Z.abs (q × n) Z.abs m)%Z (Z.abs r < Z.abs n)%Z q = Zquotient m n.
intros m n q r H' H'0 H'1 H'2.
case (ZquotientProp m n); auto; intros z (H0, (H1, H2)).
case (Zle_or_lt (Z.abs q) (Z.abs (Zquotient m n))); intros Zl1; auto with arith.
case (Zle_lt_or_eq _ _ Zl1); clear Zl1; intros Zl1; auto with arith.
Contradict H1; apply Zlt_not_le.
pattern m at 1 in |- *; rewrite H'0.
apply Z.le_lt_trans with (Z.abs (q × n) + Z.abs r)%Z; auto with zarith.
apply Z.lt_le_trans with (Z.abs (q × n) + Z.abs n)%Z; auto with zarith.
repeat rewrite Zabs_Zmult.
replace (Z.abs q × Z.abs n + Z.abs n)%Z with (Z.succ (Z.abs q) × Z.abs n)%Z;
 [ auto with zarith | unfold Z.succ in |- *; ring ].
case (Zabs_eq_case _ _ Zl1); auto.
intros H;
 (cut (Zquotient m n = 0%Z);
   [ intros H3; rewrite H; repeat rewrite H3; simpl in |- *; auto | idtac ]).
cut (Z.abs (Zquotient m n) < 1)%Z.
case (Zquotient m n); simpl in |- *; auto; intros p; case p;
 unfold Z.lt in |- *; simpl in |- *; intros; discriminate.
apply Zlt_mult_simpl_l with (c := Z.abs n); auto with zarith.
case (Zle_lt_or_eq 0 (Z.abs n)); auto with zarith.
intros H3; case H'; auto.
generalize H3; case n; simpl in |- *; auto; intros; discriminate.
rewrite <- Zabs_Zmult; rewrite (Zmult_comm n).
replace (Z.abs n × 1)%Z with (Z.abs n); [ idtac | ring ].
apply Z.le_lt_trans with (1 := H1).
apply Zlt_mult_simpl_l with (c := (1 + 1)%Z); auto with zarith.
replace ((1 + 1) × Z.abs m)%Z with (Z.abs (m + m)).
replace ((1 + 1) × Z.abs n)%Z with (Z.abs n + Z.abs n)%Z; [ idtac | ring ].
pattern m at 1 in |- *; rewrite H'0; rewrite H0; rewrite H.
replace (- Zquotient m n × n + r + (Zquotient m n × n + z))%Z with (r + z)%Z;
 [ idtac | ring ].
apply Z.le_lt_trans with (Z.abs r + Z.abs z)%Z; auto with zarith.
rewrite <- (Z.abs_eq (1 + 1)); auto with zarith.
rewrite <- Zabs_Zmult; apply f_equal with (f := Z.abs); auto with zarith.
Contradict H'1; apply Zlt_not_le.
pattern m at 1 in |- *; rewrite H0.
apply Z.le_lt_trans with (Z.abs (Zquotient m n × n) + Z.abs z)%Z;
 auto with zarith.
apply Z.lt_le_trans with (Z.abs (Zquotient m n × n) + Z.abs n)%Z;
 auto with zarith.
repeat rewrite Zabs_Zmult.
replace (Z.abs (Zquotient m n) × Z.abs n + Z.abs n)%Z with
 (Z.succ (Z.abs (Zquotient m n)) × Z.abs n)%Z;
 [ auto with zarith | unfold Z.succ in |- *; ring ].
Qed.

Theorem ZquotientZopp :
  m n : Z, Zquotient (- m) n = (- Zquotient m n)%Z.
intros m n; case (Z.eq_dec n 0); intros Z1.
rewrite Z1; unfold Zquotient in |- *; case n; case m; simpl in |- *; auto.
case (ZquotientProp m n); auto; intros r1 (H'2, (H'3, H'4)); auto with zarith.
apply sym_equal;
 apply ZquotientUnique with (q := (- Zquotient m n)%Z) (r := (- r1)%Z);
 auto.
pattern m at 1 in |- *; rewrite H'2; ring.
rewrite <- Zopp_mult_distr_l; repeat rewrite Zabs_Zopp; auto.
rewrite Zabs_Zopp; auto.
Qed.

Theorem ZquotientMonotone :
  n m q : Z,
 (Z.abs n Z.abs m)%Z (Z.abs (Zquotient n q) Z.abs (Zquotient m q))%Z.
intros n m q H; case (Zle_lt_or_eq _ _ H); intros Z0.
case (Z.eq_dec q 0); intros Z1.
rewrite Z1; unfold Zquotient in |- *; case n; case m; simpl in |- *;
 auto with zarith.
case (Zle_or_lt (Z.abs (Zquotient n q)) (Z.abs (Zquotient m q))); auto;
 intros H'1.
case (ZquotientProp m q); auto; intros r1 (H'2, (H'3, H'4)); auto with zarith.
case (ZquotientProp n q); auto; intros r2 (H'5, (H'6, H'7)); auto with zarith.
Contradict H'6.
apply Zlt_not_le.
apply Z.lt_le_trans with (1 := Z0).
rewrite H'2.
apply Z.le_trans with (Z.abs (Zquotient m q × q) + Z.abs r1)%Z; auto with zarith.
apply Z.le_trans with (Z.abs (Zquotient m q × q) + Z.abs q)%Z; auto with zarith.
repeat rewrite Zabs_Zmult.
replace (Z.abs (Zquotient m q) × Z.abs q + Z.abs q)%Z with
 (Z.succ (Z.abs (Zquotient m q)) × Z.abs q)%Z;
 [ idtac | unfold Z.succ in |- *; ring ].
cut (0 < Z.abs q)%Z; auto with zarith.
case (Zle_lt_or_eq 0 (Z.abs q)); auto with zarith.
intros H'6; case Z1; auto.
generalize H'6; case q; simpl in |- *; auto; intros; discriminate.
case (Zabs_eq_case _ _ Z0); intros Z1; rewrite Z1; auto with zarith.
rewrite ZquotientZopp; rewrite Zabs_Zopp; auto with zarith.
Qed.

Theorem NotDividesDigit :
  r v : Z,
 (1 < r)%Z v 0%Z ¬ Zdivides v (Zpower_nat r (digit r v)).
intros r v H H'; red in |- *; intros H'0; case H'0; intros q E.
absurd (Z.abs v < Zpower_nat r (digit r v))%Z; auto with zarith.
apply Zle_not_lt.
case (Z.eq_dec q 0); intros Z1.
case H'; rewrite E; rewrite Z1; ring.
pattern v at 2 in |- *; rewrite E.
rewrite Zabs_Zmult.
pattern (Zpower_nat r (digit r v)) at 1 in |- *;
 replace (Zpower_nat r (digit r v)) with (Zpower_nat r (digit r v) × 1)%Z;
 [ idtac | ring ].
rewrite (fun x yZ.abs_eq (Zpower_nat x y)); auto with zarith.
apply Zle_Zmult_comp_l; auto with zarith.
generalize Z1; case q; simpl in |- *; try (intros H1; case H1; auto; fail);
 intros p;
 (case p; unfold Z.le in |- *; simpl in |- *; intros; red in |- *; intros;
   discriminate).
Qed.

Theorem ZDividesLe :
  n m : Z, n 0%Z Zdivides n m (Z.abs m Z.abs n)%Z.
intros n m H' H'0; case H'0; intros q E; rewrite E.
rewrite Zabs_Zmult.
pattern (Z.abs m) at 1 in |- *; replace (Z.abs m) with (Z.abs m × 1)%Z;
 [ idtac | ring ].
apply Zle_Zmult_comp_l; auto with zarith.
generalize E H'; case q; simpl in |- *; auto;
 try (intros H1 H2; case H2; rewrite H1; ring; fail);
 intros p; case p; unfold Z.le in |- *; simpl in |- *;
 intros; red in |- *; discriminate.
Qed.

Theorem Zquotient_mult_comp :
  m n p : Z, p 0%Z Zquotient (m × p) (n × p) = Zquotient m n.
intros m n p Z1; case (Z.eq_dec n 0); intros Z2.
rewrite Z2; unfold Zquotient in |- *; case (m × p)%Z; case m; simpl in |- *;
 auto.
case (ZquotientProp m n); auto; intros r (H1, (H2, H3)).
apply sym_equal; apply ZquotientUnique with (r := (r × p)%Z);
 auto with zarith.
pattern m at 1 in |- *; rewrite H1; ring.
rewrite Zmult_assoc.
repeat rewrite (fun xZabs_Zmult x p); auto with zarith.
repeat rewrite Zabs_Zmult; auto with zarith.
apply Zmult_gt_0_lt_compat_r; auto with zarith.
apply Z.lt_gt; generalize Z1; case p; simpl in |- *;
 try (intros H4; case H4; auto; fail); unfold Z.lt in |- *;
 simpl in |- *; auto; intros; red in |- *; intros;
 discriminate.
Qed.

Theorem ZDivides_add :
  n m p : Z, Zdivides n p Zdivides m p Zdivides (n + m) p.
intros n m p H' H'0.
case H'; intros z1 Hz1.
case H'0; intros z2 Hz2.
(z1 + z2)%Z; rewrite Hz1; rewrite Hz2; ring.
Qed.

Theorem NDivides_minus :
  n m p : Z, Zdivides n p Zdivides m p Zdivides (n - m) p.
intros n m p H' H'0.
case H'; intros z1 Hz1.
case H'0; intros z2 Hz2.
(z1 - z2)%Z; rewrite Hz1; rewrite Hz2; ring.
Qed.

Theorem ZDivides_mult :
  n m p q : Z, Zdivides n p Zdivides m q Zdivides (n × m) (p × q).
intros n m p q H' H'0.
case H'; intros z1 Hz1.
case H'0; intros z2 Hz2.
(z1 × z2)%Z; rewrite Hz1; rewrite Hz2; ring.
Qed.

Theorem ZdividesTrans :
  n m p : Z, Zdivides n m Zdivides m p Zdivides n p.
intros n m p H' H'0.
case H'; intros z1 Hz1.
case H'0; intros z2 Hz2.
(z1 × z2)%Z; rewrite Hz1; rewrite Hz2; ring.
Qed.

Theorem ZdividesLessPow :
  (n : Z) (m p : nat),
 m p Zdivides (Zpower_nat n p) (Zpower_nat n m).
intros n m p H'; (Zpower_nat n (p - m)).
rewrite <- Zpower_nat_is_exp.
rewrite <- le_plus_minus; auto.
Qed.