------------------------------------------------------------------------
-- The Agda standard library
--
-- Coprimality
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Data.Nat.Coprimality where

open import Data.Nat.Base
  using (ℕ; zero; suc; _+_; _*_; _∸_; _<_; NonZero; NonTrivial; nonTrivial⇒≢1)
open import Data.Nat.Divisibility
open import Data.Nat.GCD
open import Data.Nat.GCD.Lemmas using (lem₁₀; lem₁₁; lem₈; lem₉)
open import Data.Nat.Primality using (Prime; prime⇒irreducible)
open import Data.Nat.Properties
open import Data.Nat.DivMod using (_/_; n/1≡n; /-congˡ; /-congʳ; m*n/n≡m)
open import Data.Product.Base as Prod using (proj₁; proj₂; _,_; ∃; _×_; swap)
open import Data.Sum.Base as Sum using (inj₁; inj₂)
open import Function.Base using (_∘_)
open import Level using (0ℓ)
open import Relation.Binary.PropositionalEquality.Core as ≡
  using (_≡_; _≢_; refl; trans; cong; subst)
open import Relation.Nullary as Nullary using (¬_; contradiction; map′)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Definitions using (Symmetric; Decidable)

private
  variable d m n o p : ℕ

open ≤-Reasoning

------------------------------------------------------------------------
-- Definition
--
-- Coprime m n is inhabited iff m and n are coprime (relatively
-- prime), i.e. if their only common divisor is 1.

Coprime : Rel ℕ 0ℓ
Coprime m n = ∀ {d} → d ∣ m × d ∣ n → d ≡ 

------------------------------------------------------------------------
-- Relationship between GCD and coprimality

coprime⇒GCD≡1 : Coprime m n → GCD m n 
coprime⇒GCD≡1 {m} {n} coprime = GCD.is (1∣ m , 1∣ n) (∣-reflexive ∘ coprime)

GCD≡1⇒coprime : GCD m n  → Coprime m n
GCD≡1⇒coprime g cd with divides q eq ← GCD.greatest g cd
  = m*n≡1⇒n≡1 q _ (≡.sym eq)

coprime⇒gcd≡1 : Coprime m n → gcd m n ≡ 
coprime⇒gcd≡1 coprime = GCD.unique (gcd-GCD _ _) (coprime⇒GCD≡1 coprime)

gcd≡1⇒coprime : gcd m n ≡  → Coprime m n
gcd≡1⇒coprime gcd≡1 = GCD≡1⇒coprime (subst (GCD _ _) gcd≡1 (gcd-GCD _ _))

coprime-/gcd : ∀ m n .{{_ : NonZero (gcd m n)}} →
               Coprime (m / gcd m n) (n / gcd m n)
coprime-/gcd m n = GCD≡1⇒coprime (GCD-/gcd m n)

------------------------------------------------------------------------
-- Relational properties of Coprime

sym : Symmetric Coprime
sym c = c ∘ swap

coprime? : Decidable Coprime
coprime? m n = map′ gcd≡1⇒coprime coprime⇒gcd≡1 (gcd m n ≟ )

------------------------------------------------------------------------
-- Other basic properties

-- Everything is coprime to 1.

1-coprimeTo : ∀ m → Coprime  m
1-coprimeTo m = ∣1⇒≡1 ∘ proj₁

-- Nothing except for 1 is coprime to 0.

0-coprimeTo-m⇒m≡1 : Coprime  m → m ≡ 
0-coprimeTo-m⇒m≡1 {m} coprime = coprime (m ∣0 , ∣-refl)

¬0-coprimeTo-2+ : .{{NonTrivial n}} → ¬ Coprime  n
¬0-coprimeTo-2+ {n} coprime = contradiction (0-coprimeTo-m⇒m≡1 coprime) (nonTrivial⇒≢1 {n})

-- If m and n are coprime, then n + m and n are also coprime.

coprime-+ : Coprime m n → Coprime (n + m) n
coprime-+ coprime (d₁ , d₂) = coprime (∣m+n∣m⇒∣n d₁ d₂ , d₂)

-- Recomputable

recompute : .(Coprime n d) → Coprime n d
recompute {n} {d} coprime = Nullary.recompute (coprime? n d) coprime

------------------------------------------------------------------------
-- Relationship with Bezout's lemma

-- If the "gcd" in Bézout's identity is non-zero, then the "other"
-- divisors are coprime.

Bézout-coprime : .{{NonZero d}} →
                 Bézout.Identity d (m * d) (n * d) → Coprime m n
Bézout-coprime {d = suc _} (Bézout.+- x y eq) (divides-refl q₁ , divides-refl q₂) =
  lem₁₀ y q₂ x q₁ eq
Bézout-coprime {d = suc _} (Bézout.-+ x y eq) (divides-refl q₁ , divides-refl q₂) =
  lem₁₀ x q₁ y q₂ eq

-- Coprime numbers satisfy Bézout's identity.

coprime-Bézout : Coprime m n → Bézout.Identity  m n
coprime-Bézout = Bézout.identity ∘ coprime⇒GCD≡1

-- If m divides n*o and is coprime to n, then it divides o.

coprime-divisor : Coprime m n → m ∣ n * o → m ∣ o
coprime-divisor {o = o} c (divides q eq′) with coprime-Bézout c
... | Bézout.+- x y eq = divides (x * o ∸ y * q) (lem₈ x y eq eq′)
... | Bézout.-+ x y eq = divides (y * q ∸ x * o) (lem₉ x y eq eq′)

-- If d is a common divisor of m*o and n*o, and m and n are coprime,
-- then d divides o.

coprime-factors : Coprime m n → d ∣ m * o × d ∣ n * o → d ∣ o
coprime-factors c (divides q₁ eq₁ , divides q₂ eq₂) with coprime-Bézout c
... | Bézout.+- x y eq = divides (x * q₁ ∸ y * q₂) (lem₁₁ x y eq eq₁ eq₂)
... | Bézout.-+ x y eq = divides (y * q₂ ∸ x * q₁) (lem₁₁ y x eq eq₂ eq₁)

------------------------------------------------------------------------
-- Primality implies coprimality.

prime⇒coprime : Prime p → .{{NonZero n}} → n < p → Coprime p n
prime⇒coprime p n<p (d∣p , d∣n) with prime⇒irreducible p d∣p
... | inj₁ d≡1      = d≡1
... | inj₂ d≡p@refl = contradiction n<p (≤⇒≯ (∣⇒≤ d∣n))