Library Maths.prime


Require Import ZArith.
Require Import ZArithRing.

Require Import divide.
Require Import gcd.

Relative primality

Definition rel_prime (a b : Z) : Prop := gcd a b 1.

Bezout's theorem: a and b are relatively prime if and only if there exist u and v such that ua+vb = 1.

Lemma rel_prime_bezout : ∀ a b : Z, rel_prime a b → Bezout a b 1.
Proof.
intros a b; exact (gcd_bezout a b 1).
Qed.

Lemma bezout_rel_prime : ∀ a b : Z, Bezout a b 1 → rel_prime a b.
Proof.
simple induction 1; constructor; auto.
intros. rewrite <- H0; auto.
Qed.

Gauss's theorem: if a divides bc and if a and b are relatively prime, then a divides c.

Theorem Gauss : ∀ a b c : Z, (a | b × c)%Z → rel_prime a b → (a | c)%Z.
Proof.
intros. elim (rel_prime_bezout a b H0); intros.
replace c with (c × 1)%Z; [ idtac | ring ].
rewrite <- H1.
replace (c × (u × a + v × b))%Z with (c × u × a + v × (b × c))%Z;
 [ eauto | ring ].
Qed.

If a is relatively prime to b and c, then it is to bc

Lemma rel_prime_mult :
 ∀ a b c : Z, rel_prime a b → rel_prime a c → rel_prime a (b × c).
Proof.
intros a b c Hb Hc.
elim (rel_prime_bezout a b Hb); intros.
elim (rel_prime_bezout a c Hc); intros.
apply bezout_rel_prime.
apply
 Bezout_intro
  with (u := (u × u0 × a + v0 × c × u + u0 × v × b)%Z) (v := (v × v0)%Z).
rewrite <- H.
replace (u × a + v × b)%Z with ((u × a + v × b) × 1)%Z; [ idtac | ring ].
rewrite <- H0.
ring.
Qed.

Primality

Inductive prime (p : Z) : Prop :=
    prime_intro :
      (1 < p)%Z → (∀ n : Z, (1 ≤ n < p)%Z → rel_prime n p) → prime p.

The sole divisors of a prime number p are -1, 1, p and -p.

Lemma prime_divisors :
 ∀ p : Z,
 prime p →
 ∀ a : Z, (a | p)%Z → a = (-1)%Z ∨ a = 1%Z ∨ a = p ∨ a = (- p)%Z.
Proof.
simple induction 1; intros.
assert
 (a = (- p)%Z ∨
  (- p < a < -1)%Z ∨
  a = (-1)%Z ∨ a = 0%Z ∨ a = 1%Z ∨ (1 < a < p)%Z ∨ a = p).
assert (Zabs a ≤ Zabs p)%Z. apply divide_bounds; [ assumption | omega ].
generalize H3.
pattern (Zabs a) in |- *; apply Zabs_ind; pattern (Zabs p) in |- *;
 apply Zabs_ind; intros; omega.
intuition.
absurd (rel_prime (- a) p); intuition.
inversion H3.
assert (- a | - a)%Z; auto.
assert (- a | p)%Z; auto.
generalize (H8 (- a)%Z H9 H10); intuition.
generalize (divide_1 (- a) H11); intuition.
inversion H2. subst a; omega.
absurd (rel_prime a p); intuition.
inversion H3.
assert (a | a)%Z; auto.
assert (a | p)%Z; auto.
generalize (H8 a H9 H10); intuition.
generalize (divide_1 a H11); intuition.
Qed.

A prime number is relatively prime with any number it does not divide

Lemma prime_rel_prime :
 ∀ p : Z, prime p → ∀ a : Z, ¬ (p | a)%Z → rel_prime p a.
Proof.
simple induction 1; intros.
constructor; intuition.
elim (prime_divisors p H x H3); intuition; subst; auto.
absurd (p | a)%Z; auto.
absurd (p | a)%Z; intuition.
Qed.

Hint Resolve prime_rel_prime.

divide is decidable

Axiom divide_dec : ∀ a b : Z, {(a | b)%Z} + {¬ (a | b)%Z}.


If a prime p divides ab then it divides either a or b

Lemma prime_mult :
 ∀ p : Z,
 prime p → ∀ a b : Z, (p | a × b)%Z → (p | a)%Z ∨ (p | b)%Z.
Proof.
simple induction 1; intros.
case (divide_dec p a); intuition.
right; apply Gauss with a; auto.
Qed.