Require Import Znumtheory.
Require Import ZArith.
Require Import Setoid.
Require Import Ring.
Require Import Omega.
Require Import FastArith.
Require Import Coqlib.
Local Open Scope Z_scope.
Section Congruence.
Definition congr n x y :
Prop :=
exists q,
y =
x +
q *
n.
Lemma congr_refl :
forall n x,
congr n x x.
Proof.
intros n x; exists 0; auto with zarith. Qed.
Lemma congr_sym :
forall n x y,
congr n x y ->
congr n y x.
Proof.
intros n x y [q Hq]. exists (-q); rewrite Hq.
ring.
Qed.
Lemma congr_trans n :
transitive _ (
congr n).
Proof.
Lemma congr_0_eq :
forall x y,
congr 0
x y ->
x =
y.
Proof.
intros x y [q Hq]; rewrite Hq.
simpl.
auto with zarith.
Qed.
Lemma congr_1 :
forall x y,
congr 1
x y.
Proof.
intros x y; exists (y - x). simpl.
omega.
Qed.
Lemma congr_divide :
forall n m x y,
congr n x y -> (
m |
n) ->
congr m x y.
Proof.
intros n m x y [kn Hn] [km Hm].
exists (kn * km).
rewrite Hn; rewrite Hm.
auto with zarith.
Qed.
Lemma congr_plus_compat_l :
forall n x y m,
congr n x y ->
congr n (
x +
m) (
y +
m).
Proof.
intros n x y m [q Hq].
exists q.
rewrite Hq.
ring.
Qed.
Lemma congr_minus_compat_l :
forall n x y m,
congr n x y ->
congr n (
x -
m) (
y -
m).
Proof.
intros n x y m [q Hq].
exists q.
rewrite Hq.
ring.
Qed.
Lemma congr_minus_compat n x y z t :
congr n x y ->
congr n z t ->
congr n (
x -
z) (
y -
t).
Proof.
intros [a ->] [b ->].
exists (a - b). ring.
Qed.
Lemma congr_neg_compat n x y :
congr n x y ->
congr n (-
x) (-
y).
Proof.
intros [q ->].
exists (-q). ring.
Qed.
Lemma congr_plus_compat :
forall n x y z t,
congr n x y ->
congr n z t ->
congr n (
x +
z) (
y +
t).
Proof.
intros n x y z t [a Ha] [b Hb].
exists (a + b).
rewrite Ha. rewrite Hb.
ring.
Qed.
Lemma congr_diff :
forall a b,
congr (
a -
b)
a b.
Proof.
intros a b.
destruct (
Z_eq_dec a b).
subst;
apply congr_refl.
exists (-1);
auto with zarith.
Qed.
Lemma congr_mod_compat :
forall n x,
n > 0 ->
congr n x (
x mod n).
Proof.
Lemma congr_eqm :
forall n x y,
n > 0 ->
congr n x y ->
eqm n x y.
Proof.
intros n x y POS (
q & ->).
symmetry.
apply Z_mod_plus.
auto.
Qed.
Lemma eqm_congr :
forall n x y,
n > 0 ->
eqm n x y ->
congr n x y.
Proof.
intros n x y POS EQM.
unfold eqm in *.
exists (
y /
n -
x /
n).
replace (
x + (
y /
n -
x /
n) *
n)
with (
y /
n *
n + (
x -
x /
n *
n))
by ring.
assert (
n <> 0)
by intuition.
rewrite <-
Zmod_eq_full;
auto.
rewrite EQM.
rewrite Zmod_eq_full;
auto.
ring.
Qed.
Lemma congr_mult_l_compat :
forall n p x y,
congr n x y ->
congr (
p *
n) (
p *
x) (
p *
y).
Proof.
intros n p x y (q & ->). exists q. ring.
Qed.
Definition divide (
x:
Zfast) (
y:
Nfast) :
bool :=
if Nfasteqb y F0 then Zfasteqb x F0
else Zfasteqb (
Zfastmod x y)
F0.
Lemma divide_ok:
forall x y,
divide x y =
true <-> (
Zfast_of_Nfast y |
x).
Proof.
End Congruence.
Hint Resolve congr_refl congr_trans congr_sym congr_0_eq congr_1 :
congr.
Notation "
x ≡
y [
n ]" := (
congr n x y) (
at level 80).
Section on_gcd.
Variables a b :
Z.
Lemma Zgcd_divides_l : (
Zgcd a b |
a).
Proof.
Lemma Zgcd_divides_r : (
Zgcd a b |
b).
Proof.
End on_gcd.
Require Import Utf8.
Require Psatz.
Remark Ngcd_is_Zgcd (
x y:
N) : (
Z.of_N (
N.gcd x y)) =
Zgcd (
Z.of_N x) (
Z.of_N y).
Proof.
destruct x, y; reflexivity. Qed.
Remark Nlcm_is_Zlcm (
x y:
N) : (
Z.of_N (
N.lcm x y)) =
Z.lcm (
Z.of_N x) (
Z.of_N y).
Proof.
Lemma N_div_eucl_spec a b :
let (
q,
r) :=
N.div_eucl a b in
a = (
b *
q +
r)%
N ∧
(
b ≠ 0 →
r <
b)%
N.
Proof.