Library Stdlib.ZArith.Zdivisibility

From Stdlib Require Import BinInt Wf_Z ZArithRing Zdiv Lia.

Module Z.
Local Open Scope Z_scope.

Lemma mod0_divide : forall a b, (b | a) -> a mod b = 0.

Lemma absle_divide a b : (a | b) -> b <> 0 -> Z.abs a <= Z.abs b.

Lemma BoolSpec_divide_nz a b (H : a <> 0) : BoolSpec (Z.divide a b) (~ Z.divide a b) (b mod a =? 0).

Lemma BoolSpec_divide a b : BoolSpec (Z.divide a b) (~ Z.divide a b) ((b =? 0) || negb (a =? 0) && (b mod a =? 0))%bool.

Lemma divide_m1_l a : ( -1 | a ).

Lemma divide_pow_same_r a n (Hn : 1 <= n) : ( a | a^n ).

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

Lemma BoolSpec_coprime a b : BoolSpec (Z.coprime a b) (~ Z.coprime a b) (Z.gcd a b =? 1).

Lemma Bezout_coprime_iff a b : Z.coprime a b <-> Z.Bezout a b 1.

Definition Bezout_coprime a b := proj1 (Bezout_coprime_iff a b).
Definition coprime_Bezout a b := proj2 (Bezout_coprime_iff a b).

#[global] Instance Symmetric_coprime : RelationClasses.Symmetric coprime.

Lemma coprime_0_l_iff z : coprime 0 z <-> Z.abs z = 1.

Lemma coprime_0_r_iff z : coprime z 0 <-> Z.abs z = 1.

Lemma coprime_1_l z : coprime 1 z.

Lemma coprime_1_r z : coprime z 1.

Lemma coprime_opp_l a b : coprime (- a) b <-> coprime a b.

Lemma coprime_opp_r a b : coprime a (- b) <-> coprime a b.

Lemma coprime_mod_l_iff a b : coprime (a mod b) b <-> coprime a b.

Lemma coprime_mod_r_iff a b : coprime a (b mod a) <-> coprime a b.

Lemma coprime_mul_r a b c : coprime a b -> coprime a c -> coprime a (b * c).

Lemma coprime_mul_l a b c : coprime a c -> coprime b c -> coprime (a * b) c.

Lemma coprime_pow_r a b n : 0 <= n -> coprime a b -> coprime a (b ^ n).

Lemma coprime_pow_l a b n : 0 <= n -> coprime a b -> coprime (a ^ n) b.

Definition prime p := 1 < p /\ forall n, 1 < n < p -> ~ (n|p).
Existing Class prime.

Lemma not_prime_0 : not (prime 0).

Lemma not_prime_1 : not (prime 1).

Lemma prime_2 : prime 2.

Lemma prime_3 : prime 3.

Lemma prime_ge_2 p : prime p -> 2 <= p.

Lemma divide_prime_r a p (Hp : prime p) (Hd : (a | p)) :
  a = -p \/ a = -1 \/ a = 1 \/ a = p.

Lemma divide_prime_r_iff a p (Hp : prime p) :
  (a | p) <-> a = -p \/ a = -1 \/ a = 1 \/ a = p.

Lemma not_prime_square a : ~ prime (a * a).

Lemma coprime_prime_l p a (Hp : prime p) (Ha : ~ (p | a)) : coprime p a.

Lemma coprime_prime_l_iff p a (Hp : prime p) : coprime p a <-> ~ (p | a).

Lemma coprime_prime_small p a (Hp : prime p) (Ha : 1 <= a < p) : coprime p a.

Lemma divide_prime_mul a b p (Hp : prime p) :
  (p | a * b) <-> (p | a) \/ (p | b).

Lemma divide_prime_prime p q (Hp : prime p) (Hq : prime q) :
  ( p | q ) -> p = q.

Lemma divide_prime_prime_iff p q (Hp : prime p) (Hq : prime q) :
  ( p | q ) <-> p = q.

Theorem divide_prime_pp p q n (Hp : prime p) (Hq : prime q) (Hn : 0 <= n) :
  (p | q^n) -> p = q.

Theorem divide_prime_pp_iff p q n (Hp : prime p) (Hq : prime q) (Hn : 1 <= n) :
  (p | q^n) <-> p = q.

Section extended_euclid_algorithm.
Variables a b : Z.

Local Lemma extgcd_rec_helper r1 r2 q :
  Z.gcd r1 r2 = Z.gcd a b -> Z.gcd (r2 - q * r1) r1 = Z.gcd a b.

Let f := S(S(Z.to_nat(Z.log2_up(Z.log2_up(Z.abs(a*b)))))).
Local Definition extgcd_rec : forall r1 u1 v1 r2 u2 v2,
  (True -> 0 <= r1 /\ 0 <= r2 /\ r1 = u1 * a + v1 * b /\ r2 = u2 * a + v2 * b /\
      Z.gcd r1 r2 = Z.gcd a b)
   -> { '(u, v, d) | True -> u * a + v * b = d /\ d = Z.gcd a b}.

Definition extgcd : Z*Z*Z.

Lemma extgcd_correct [u v d] : extgcd = (u, v, d) -> u * a + v * b = d /\ d = Z.gcd a b.
End extended_euclid_algorithm.

End Z.

#[export] Hint Extern 0 (Z.prime 2) => exact Z.prime_2 : typeclass_instances.
#[export] Hint Extern 0 (Z.prime 3) => exact Z.prime_3 : typeclass_instances.