------------------------------------------------------------------------
-- 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 ≡ 1
------------------------------------------------------------------------
-- Relationship between GCD and coprimality
coprime⇒GCD≡1 : Coprime m n → GCD m n 1
coprime⇒GCD≡1 {m} {n} coprime = GCD.is (1∣ m , 1∣ n) (∣-reflexive ∘ coprime)
GCD≡1⇒coprime : GCD m n 1 → 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 ≡ 1
coprime⇒gcd≡1 coprime = GCD.unique (gcd-GCD _ _) (coprime⇒GCD≡1 coprime)
gcd≡1⇒coprime : gcd m n ≡ 1 → 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 ≟ 1)
------------------------------------------------------------------------
-- Other basic properties
-- Everything is coprime to 1.
1-coprimeTo : ∀ m → Coprime 1 m
1-coprimeTo m = ∣1⇒≡1 ∘ proj₁
-- Nothing except for 1 is coprime to 0.
0-coprimeTo-m⇒m≡1 : Coprime 0 m → m ≡ 1
0-coprimeTo-m⇒m≡1 {m} coprime = coprime (m ∣0 , ∣-refl)
¬0-coprimeTo-2+ : .{{NonTrivial n}} → ¬ Coprime 0 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 1 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))
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4