1
------------------------------------------------------------------------
3
------------------------------------------------------------------------
5
module Data.Nat.Coprimality where
8
import Data.Nat.Properties as NatProp
9
open import Data.Nat.Divisibility as Div
10
open import Data.Nat.GCD
11
open import Data.Nat.GCD.Lemmas
12
open import Data.Product as Prod
13
open import Data.Function
14
open import Relation.Binary.PropositionalEquality as PropEq
15
using (_≡_; _≢_; refl)
16
open import Relation.Nullary
17
open import Relation.Binary
20
module P = Poset Div.poset
21
module CS = CommutativeSemiring NatProp.commutativeSemiring
23
-- Coprime m n is inhabited iff m and n are coprime (relatively
24
-- prime), i.e. if their only common divisor is 1.
26
Coprime : (m n : ℕ) → Set
27
Coprime m n = ∀ {i} → i ∣ m × i ∣ n → i ≡ 1
29
-- Coprime numbers have 1 as their gcd.
31
coprime-gcd : ∀ {m n} → Coprime m n → GCD m n 1
32
coprime-gcd {m} {n} c = GCD.is (1∣ m , 1∣ n) greatest
34
greatest : ∀ {d} → d ∣ m × d ∣ n → d ∣ 1
36
greatest .{1} cd | refl = 1∣ 1
38
-- If two numbers have 1 as their gcd, then they are coprime.
40
gcd-coprime : ∀ {m n} → GCD m n 1 → Coprime m n
41
gcd-coprime g cd with GCD.greatest g cd
42
gcd-coprime g cd | divides q eq =
43
NatProp.i*j≡1⇒j≡1 q _ (PropEq.sym eq)
45
-- Coprime is decidable.
51
2+≢1 : ∀ {n} → suc (suc n) ≢ 1
54
coprime? : Decidable Coprime
55
coprime? i j with gcd i j
56
... | (0 , g) = no (0≢1 ∘ GCD.unique g ∘ coprime-gcd)
57
... | (1 , g) = yes (λ {i} → gcd-coprime g {i})
58
... | (suc (suc d) , g) = no (2+≢1 ∘ GCD.unique g ∘ coprime-gcd)
60
-- The coprimality relation is symmetric.
62
sym : ∀ {m n} → Coprime m n → Coprime n m
65
-- Everything is coprime to 1.
67
1-coprimeTo : ∀ m → Coprime 1 m
68
1-coprimeTo m = 1∣1 ∘ proj₁
70
-- Nothing except for 1 is coprime to 0.
72
0-coprimeTo-1 : ∀ {m} → Coprime 0 m → m ≡ 1
73
0-coprimeTo-1 {m} c = c (m ∣0 , P.refl)
75
-- If m and n are coprime, then n + m and n are also coprime.
77
coprime-+ : ∀ {m n} → Coprime m n → Coprime (n + m) n
78
coprime-+ c (d₁ , d₂) = c (∣-∸ d₁ d₂ , d₂)
80
-- If the "gcd" in Bézout's identity is non-zero, then the "other"
81
-- divisors are coprime.
83
Bézout-coprime : ∀ {i j d} →
84
Bézout.Identity (suc d) (i * suc d) (j * suc d) →
86
Bézout-coprime (Bézout.+- x y eq) (divides q₁ refl , divides q₂ refl) =
88
Bézout-coprime (Bézout.-+ x y eq) (divides q₁ refl , divides q₂ refl) =
91
-- Coprime numbers satisfy Bézout's identity.
93
coprime-Bézout : ∀ {i j} → Coprime i j → Bézout.Identity 1 i j
94
coprime-Bézout = Bézout.identity ∘ coprime-gcd
96
-- If i divides jk and is coprime to j, then it divides k.
98
coprime-divisor : ∀ {k i j} → Coprime i j → i ∣ j * k → i ∣ k
99
coprime-divisor {k} c (divides q eq′) with coprime-Bézout c
100
... | Bézout.+- x y eq = divides (x * k ∸ y * q) (lem₈ x y eq eq′)
101
... | Bézout.-+ x y eq = divides (y * q ∸ x * k) (lem₉ x y eq eq′)
103
-- If d is a common divisor of mk and nk, and m and n are coprime,
106
coprime-factors : ∀ {d m n k} →
107
Coprime m n → d ∣ m * k × d ∣ n * k → d ∣ k
108
coprime-factors c (divides q₁ eq₁ , divides q₂ eq₂) with coprime-Bézout c
109
... | Bézout.+- x y eq = divides (x * q₁ ∸ y * q₂) (lem₁₁ x y eq eq₁ eq₂)
110
... | Bézout.-+ x y eq = divides (y * q₂ ∸ x * q₁) (lem₁₁ y x eq eq₂ eq₁)
114
data GCD′ : ℕ → ℕ → ℕ → Set where
115
gcd-* : ∀ {d} q₁ q₂ (c : Coprime q₁ q₂) →
116
GCD′ (q₁ * d) (q₂ * d) d
118
-- The two definitions are equivalent.
120
gcd-gcd′ : ∀ {d m n} → GCD m n d → GCD′ m n d
121
gcd-gcd′ g with GCD.commonDivisor g
122
gcd-gcd′ {zero} g | (divides q₁ refl , divides q₂ refl)
123
with q₁ * 0 | CS.*-comm 0 q₁
124
| q₂ * 0 | CS.*-comm 0 q₂
125
... | .0 | refl | .0 | refl = gcd-* 1 1 (1-coprimeTo 1)
126
gcd-gcd′ {suc d} g | (divides q₁ refl , divides q₂ refl) =
127
gcd-* q₁ q₂ (Bézout-coprime (Bézout.identity g))
129
gcd′-gcd : ∀ {m n d} → GCD′ m n d → GCD m n d
130
gcd′-gcd (gcd-* q₁ q₂ c) = GCD.is (∣-* q₁ , ∣-* q₂) (coprime-factors c)
132
-- Calculates (the alternative representation of) the gcd of the
135
gcd′ : ∀ m n → ∃ λ d → GCD′ m n d
136
gcd′ m n = Prod.map id gcd-gcd′ (gcd m n)
added
removed
src/Data/Nat/Coprimality.agda
