forked from agda/agda-stdlib
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathCoprimality.agda
149 lines (111 loc) · 5.46 KB
/
Coprimality.agda
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
------------------------------------------------------------------------
-- The Agda standard library
--
-- Coprimality
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Nat.Coprimality where
open import Data.Empty
open import Data.Nat.Base
open import Data.Nat.Divisibility
open import Data.Nat.GCD
open import Data.Nat.GCD.Lemmas
open import Data.Nat.Primality
open import Data.Nat.Properties
open import Data.Nat.DivMod
open import Data.Product.Base as Prod
open import Function.Base using (_∘_)
open import Level using (0ℓ)
open import Relation.Binary.PropositionalEquality.Core as P
using (_≡_; _≢_; refl; trans; cong; subst; module ≡-Reasoning)
open import Relation.Nullary as Nullary hiding (recompute)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Definitions using (Symmetric; Decidable)
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 = ∀ {i} → i ∣ m × i ∣ n → i ≡ 1
------------------------------------------------------------------------
-- Relationship between GCD and coprimality
coprime⇒GCD≡1 : ∀ {m n} → Coprime m n → GCD m n 1
coprime⇒GCD≡1 {m} {n} c = GCD.is (1∣ m , 1∣ n) (∣-reflexive ∘ c)
GCD≡1⇒coprime : ∀ {m n} → 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 _ (P.sym eq)
coprime⇒gcd≡1 : ∀ {m n} → Coprime m n → gcd m n ≡ 1
coprime⇒gcd≡1 coprime = GCD.unique (gcd-GCD _ _) (coprime⇒GCD≡1 coprime)
gcd≡1⇒coprime : ∀ {m n} → 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
private
0≢1 : 0 ≢ 1
0≢1 ()
2+≢1 : ∀ {n} → suc (suc n) ≢ 1
2+≢1 ()
coprime? : Decidable Coprime
coprime? i j with mkGCD i j
... | (0 , g) = no (0≢1 ∘ GCD.unique g ∘ coprime⇒GCD≡1)
... | (1 , g) = yes (GCD≡1⇒coprime g)
... | (suc (suc d) , g) = no (2+≢1 ∘ GCD.unique g ∘ coprime⇒GCD≡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 : ∀ {m} → Coprime 0 m → m ≡ 1
0-coprimeTo-m⇒m≡1 {m} c = c (m ∣0 , ∣-refl)
¬0-coprimeTo-2+ : ∀ {n} → ¬ Coprime 0 (2 + n)
¬0-coprimeTo-2+ coprime = contradiction (0-coprimeTo-m⇒m≡1 coprime) λ()
-- If m and n are coprime, then n + m and n are also coprime.
coprime-+ : ∀ {m n} → Coprime m n → Coprime (n + m) n
coprime-+ c (d₁ , d₂) = c (∣m+n∣m⇒∣n d₁ d₂ , d₂)
-- Recomputable
recompute : ∀ {n d} → .(Coprime n d) → Coprime n d
recompute {n} {d} c = Nullary.recompute (coprime? n d) c
------------------------------------------------------------------------
-- 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 : ∀ {i j d} .{{_ : NonZero d}} →
Bézout.Identity d (i * d) (j * d) → Coprime i j
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 : ∀ {i j} → Coprime i j → Bézout.Identity 1 i j
coprime-Bézout = Bézout.identity ∘ coprime⇒GCD≡1
-- If i divides jk and is coprime to j, then it divides k.
coprime-divisor : ∀ {k i j} → Coprime i j → i ∣ j * k → i ∣ k
coprime-divisor {k} c (divides q eq′) with coprime-Bézout c
... | Bézout.+- x y eq = divides (x * k ∸ y * q) (lem₈ x y eq eq′)
... | Bézout.-+ x y eq = divides (y * q ∸ x * k) (lem₉ x y eq eq′)
-- If d is a common divisor of mk and nk, and m and n are coprime,
-- then d divides k.
coprime-factors : ∀ {d m n k} →
Coprime m n → d ∣ m * k × d ∣ n * k → d ∣ k
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 : ∀ m → Prime m →
∀ n → 0 < n → n < m → Coprime m n
prime⇒coprime (suc (suc _)) p _ _ _ {0} (0∣m , _) =
contradiction (0∣⇒≡0 0∣m) λ()
prime⇒coprime (suc (suc _)) _ _ _ _ {1} _ = refl
prime⇒coprime (suc (suc _)) p (suc _) _ n<m {(suc (suc _))} (d∣m , d∣n) =
contradiction d∣m (p 2≤d d<m)
where 2≤d = s≤s (s≤s z≤n); d<m = <-≤-trans (s≤s (∣⇒≤ d∣n)) n<m