-
Notifications
You must be signed in to change notification settings - Fork 0
/
GCD.agda
183 lines (133 loc) · 6.17 KB
/
GCD.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
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
------------------------------------------------------------------------
-- Greatest common divisor
------------------------------------------------------------------------
module Data.Nat.GCD where
open import Data.Nat
open import Data.Nat.Divisibility as Div
open import Relation.Binary
private module P = Poset Div.poset
open import Data.Product
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
open import Induction
open import Induction.Nat
open import Induction.Lexicographic
open import Function
open import Data.Nat.GCD.Lemmas
------------------------------------------------------------------------
-- Greatest common divisor
module GCD where
-- Specification of the greatest common divisor (gcd) of two natural
-- numbers.
record GCD (m n gcd : ℕ) : Set where
constructor is
field
-- The gcd is a common divisor.
commonDivisor : gcd ∣ m × gcd ∣ n
-- All common divisors divide the gcd, i.e. the gcd is the
-- greatest common divisor according to the partial order _∣_.
greatest : ∀ {d} → d ∣ m × d ∣ n → d ∣ gcd
open GCD public
-- The gcd is unique.
unique : ∀ {d₁ d₂ m n} → GCD m n d₁ → GCD m n d₂ → d₁ ≡ d₂
unique d₁ d₂ = P.antisym (GCD.greatest d₂ (GCD.commonDivisor d₁))
(GCD.greatest d₁ (GCD.commonDivisor d₂))
-- The gcd relation is "symmetric".
sym : ∀ {d m n} → GCD m n d → GCD n m d
sym g = is (swap $ GCD.commonDivisor g) (GCD.greatest g ∘ swap)
-- The gcd relation is "reflexive".
refl : ∀ {n} → GCD n n n
refl = is (P.refl , P.refl) proj₁
-- The GCD of 0 and n is n.
base : ∀ {n} → GCD 0 n n
base {n} = is (n ∣0 , P.refl) proj₂
-- If d is the gcd of n and k, then it is also the gcd of n and
-- n + k.
step : ∀ {n k d} → GCD n k d → GCD n (n + k) d
step g with GCD.commonDivisor g
step {n} {k} {d} g | (d₁ , d₂) = is (d₁ , ∣-+ d₁ d₂) greatest′
where
greatest′ : ∀ {d′} → d′ ∣ n × d′ ∣ n + k → d′ ∣ d
greatest′ (d₁ , d₂) = GCD.greatest g (d₁ , ∣-∸ d₂ d₁)
open GCD public using (GCD)
------------------------------------------------------------------------
-- Calculating the gcd
-- The calculation also proves Bézout's lemma.
module Bézout where
module Identity where
-- If m and n have greatest common divisor d, then one of the
-- following two equations is satisfied, for some numbers x and y.
-- The proof is "lemma" below (Bézout's lemma).
--
-- (If this identity was stated using integers instead of natural
-- numbers, then it would not be necessary to have two equations.)
data Identity (d m n : ℕ) : Set where
+- : (x y : ℕ) (eq : d + y * n ≡ x * m) → Identity d m n
-+ : (x y : ℕ) (eq : d + x * m ≡ y * n) → Identity d m n
-- Various properties about Identity.
sym : ∀ {d} → Symmetric (Identity d)
sym (+- x y eq) = -+ y x eq
sym (-+ x y eq) = +- y x eq
refl : ∀ {d} → Identity d d d
refl = -+ 0 1 PropEq.refl
base : ∀ {d} → Identity d 0 d
base = -+ 0 1 PropEq.refl
private
infixl 7 _⊕_
_⊕_ : ℕ → ℕ → ℕ
m ⊕ n = 1 + m + n
step : ∀ {d n k} → Identity d n k → Identity d n (n + k)
step {d} (+- x y eq) with compare x y
step {d} (+- .x .x eq) | equal x = +- (2 * x) x (lem₂ d x eq)
step {d} (+- .x .(x ⊕ i) eq) | less x i = +- (2 * x ⊕ i) (x ⊕ i) (lem₃ d x eq)
step {d} {n} (+- .(y ⊕ i) .y eq) | greater y i = +- (2 * y ⊕ i) y (lem₄ d y n eq)
step {d} (-+ x y eq) with compare x y
step {d} (-+ .x .x eq) | equal x = -+ (2 * x) x (lem₅ d x eq)
step {d} (-+ .x .(x ⊕ i) eq) | less x i = -+ (2 * x ⊕ i) (x ⊕ i) (lem₆ d x eq)
step {d} {n} (-+ .(y ⊕ i) .y eq) | greater y i = -+ (2 * y ⊕ i) y (lem₇ d y n eq)
open Identity public using (Identity; +-; -+)
module Lemma where
-- This type packs up the gcd, the proof that it is a gcd, and the
-- proof that it satisfies Bézout's identity.
data Lemma (m n : ℕ) : Set where
result : (d : ℕ) (g : GCD m n d) (b : Identity d m n) → Lemma m n
-- Various properties about Lemma.
sym : Symmetric Lemma
sym (result d g b) = result d (GCD.sym g) (Identity.sym b)
base : ∀ d → Lemma 0 d
base d = result d GCD.base Identity.base
refl : ∀ d → Lemma d d
refl d = result d GCD.refl Identity.refl
stepˡ : ∀ {n k} → Lemma n (suc k) → Lemma n (suc (n + k))
stepˡ {n} {k} (result d g b) =
PropEq.subst (Lemma n) (lem₀ n k) $
result d (GCD.step g) (Identity.step b)
stepʳ : ∀ {n k} → Lemma (suc k) n → Lemma (suc (n + k)) n
stepʳ = sym ∘ stepˡ ∘ sym
open Lemma public using (Lemma; result)
-- Bézout's lemma proved using some variant of the extended
-- Euclidean algorithm.
lemma : (m n : ℕ) → Lemma m n
lemma m n = build [ <-rec-builder ⊗ <-rec-builder ] P gcd (m , n)
where
P : ℕ × ℕ → Set
P (m , n) = Lemma m n
gcd : ∀ p → (<-Rec ⊗ <-Rec) P p → P p
gcd (zero , n ) rec = Lemma.base n
gcd (suc m , zero ) rec = Lemma.sym (Lemma.base (suc m))
gcd (suc m , suc n ) rec with compare m n
gcd (suc m , suc .m ) rec | equal .m = Lemma.refl (suc m)
gcd (suc m , suc .(suc (m + k))) rec | less .m k =
-- "gcd (suc m) (suc k)"
Lemma.stepˡ $ proj₁ rec (suc k) (lem₁ k m)
gcd (suc .(suc (n + k)) , suc n) rec | greater .n k =
-- "gcd (suc k) (suc n)"
Lemma.stepʳ $ proj₂ rec (suc k) (lem₁ k n) (suc n)
-- Bézout's identity can be recovered from the GCD.
identity : ∀ {m n d} → GCD m n d → Identity d m n
identity {m} {n} g with lemma m n
identity g | result d g′ b with GCD.unique g g′
identity g | result d g′ b | PropEq.refl = b
-- Calculates the gcd of the arguments.
gcd : (m n : ℕ) → ∃ λ d → GCD m n d
gcd m n with Bézout.lemma m n
gcd m n | Bézout.result d g _ = (d , g)