|
57
|
1 module root2 where
|
|
|
2
|
|
141
|
3 open import Data.Nat
|
|
|
4 open import Data.Nat.Properties
|
|
57
|
5 open import Data.Empty
|
|
141
|
6 open import Data.Unit using (⊤ ; tt)
|
|
57
|
7 open import Relation.Nullary
|
|
|
8 open import Relation.Binary.PropositionalEquality
|
|
141
|
9 open import Relation.Binary.Definitions
|
|
57
|
10
|
|
281
|
11 import gcd as GCD
|
|
159
|
12 open import even
|
|
142
|
13 open import nat
|
|
231
|
14 open import logic
|
|
141
|
15
|
|
|
16 record Rational : Set where
|
|
|
17 field
|
|
|
18 i j : ℕ
|
|
320
|
19 0<j : j > 0
|
|
281
|
20 coprime : GCD.gcd i j ≡ 1
|
|
|
21
|
|
|
22 -- record Dividable (n m : ℕ ) : Set where
|
|
|
23 -- field
|
|
|
24 -- factor : ℕ
|
|
|
25 -- is-factor : factor * n + 0 ≡ m
|
|
|
26
|
|
|
27 gcd : (i j : ℕ) → ℕ
|
|
|
28 gcd = GCD.gcd
|
|
|
29
|
|
|
30 gcd-euclid : ( p a b : ℕ ) → 1 < p → 0 < a → 0 < b → ((i : ℕ ) → i < p → 0 < i → gcd p i ≡ 1)
|
|
|
31 → Dividable p (a * b) → Dividable p a ∨ Dividable p b
|
|
|
32 gcd-euclid = GCD.gcd-euclid
|
|
|
33
|
|
|
34 gcd-div1 : ( i j k : ℕ ) → k > 1 → (if : Dividable k i) (jf : Dividable k j )
|
|
|
35 → Dividable k ( gcd i j )
|
|
|
36 gcd-div1 = GCD.gcd-div
|
|
57
|
37
|
|
231
|
38 open _∧_
|
|
|
39
|
|
|
40 open import prime
|
|
|
41
|
|
233
|
42 divdable^2 : ( n k : ℕ ) → 1 < k → 1 < n → Prime k → Dividable k ( n * n ) → Dividable k n
|
|
|
43 divdable^2 zero zero () 1<n pk dn2
|
|
|
44 divdable^2 (suc n) (suc k) 1<k 1<n pk dn2 with decD {suc k} {suc n} 1<k
|
|
159
|
45 ... | yes y = y
|
|
250
|
46 ... | no non with gcd-euclid (suc k) (suc n) (suc n) 1<k (<-trans a<sa 1<n) (<-trans a<sa 1<n) (Prime.isPrime pk) dn2
|
|
233
|
47 ... | case1 dn = dn
|
|
|
48 ... | case2 dm = dm
|
|
159
|
49
|
|
255
|
50 -- p * n * n ≡ m * m means (m/n)^2 = p
|
|
|
51 -- rational m/n requires m and n is comprime each other which contradicts the condition
|
|
|
52
|
|
254
|
53 root-prime-irrational : ( n m p : ℕ ) → n > 1 → Prime p → m > 1 → p * n * n ≡ m * m → ¬ (gcd n m ≡ 1)
|
|
|
54 root-prime-irrational n m 0 n>1 pn m>1 pnm = ⊥-elim ( nat-≡< refl (<-trans a<sa (Prime.p>1 pn)))
|
|
281
|
55 root-prime-irrational n m (suc p0) n>1 pn m>1 pnm = rot13 ( gcd-div1 n m (suc p0) 1<sp dn dm ) where
|
|
|
56 p = suc p0
|
|
254
|
57 1<sp : 1 < p
|
|
253
|
58 1<sp = Prime.p>1 pn
|
|
281
|
59 rot13 : {m : ℕ } → Dividable (suc p0) m → m ≡ 1 → ⊥
|
|
185
|
60 rot13 d refl with Dividable.factor d | Dividable.is-factor d
|
|
253
|
61 ... | zero | () -- gcd 0 m ≡ 1
|
|
254
|
62 ... | suc n | x = ⊥-elim ( nat-≡< (sym x) rot17 ) where -- x : (suc n * p + 0) ≡ 1
|
|
281
|
63 rot17 : suc n * (suc p0) + 0 > 1
|
|
253
|
64 rot17 = begin
|
|
|
65 2 ≡⟨ refl ⟩
|
|
254
|
66 suc (1 * 1 ) ≤⟨ 1<sp ⟩
|
|
|
67 suc p0 ≡⟨ cong suc (+-comm 0 _) ⟩
|
|
|
68 suc (p0 + 0) ≤⟨ s≤s (+-monoʳ-≤ p0 z≤n) ⟩
|
|
|
69 suc (p0 + n * p ) ≡⟨ +-comm 0 _ ⟩
|
|
|
70 suc n * p + 0 ∎ where open ≤-Reasoning
|
|
|
71 dm : Dividable p m
|
|
|
72 dm = divdable^2 m p 1<sp m>1 pn record { factor = n * n ; is-factor = begin
|
|
|
73 (n * n) * p + 0 ≡⟨ +-comm _ 0 ⟩
|
|
|
74 (n * n) * p ≡⟨ *-comm (n * n) p ⟩
|
|
|
75 p * (n * n) ≡⟨ sym (*-assoc p n n) ⟩
|
|
|
76 (p * n) * n ≡⟨ pnm ⟩
|
|
250
|
77 m * m ∎ } where open ≡-Reasoning
|
|
254
|
78 -- p * n * n = 2m' 2m'
|
|
251
|
79 -- n * n = m' 2m'
|
|
250
|
80 df = Dividable.factor dm
|
|
254
|
81 dn : Dividable p n
|
|
|
82 dn = divdable^2 n p 1<sp n>1 pn record { factor = df * df ; is-factor = begin
|
|
|
83 df * df * p + 0 ≡⟨ *-cancelʳ-≡ _ _ {p0} ( begin
|
|
|
84 (df * df * p + 0) * p ≡⟨ cong (λ k → k * p) (+-comm (df * df * p) 0) ⟩
|
|
281
|
85 ((df * df) * p ) * p ≡⟨ cong (λ k → k * p) (*-assoc df df p ) ⟩
|
|
254
|
86 (df * (df * p)) * p ≡⟨ cong (λ k → (df * k ) * p) (*-comm df p) ⟩
|
|
|
87 (df * (p * df)) * p ≡⟨ sym ( cong (λ k → k * p) (*-assoc df p df ) ) ⟩
|
|
|
88 ((df * p) * df) * p ≡⟨ *-assoc (df * p) df p ⟩
|
|
|
89 (df * p) * (df * p) ≡⟨ cong₂ (λ j k → j * k ) (+-comm 0 (df * p)) (+-comm 0 _) ⟩
|
|
|
90 (df * p + 0) * (df * p + 0) ≡⟨ cong₂ (λ j k → j * k) (Dividable.is-factor dm ) (Dividable.is-factor dm )⟩
|
|
253
|
91 m * m ≡⟨ sym pnm ⟩
|
|
281
|
92 p * n * n ≡⟨ cong (λ k → k * n) (*-comm p n) ⟩
|
|
|
93 n * p * n ≡⟨ *-assoc n p n ⟩
|
|
|
94 n * (p * n) ≡⟨ cong (λ k → n * k) (*-comm p n) ⟩
|
|
|
95 n * (n * p) ≡⟨ sym (*-assoc n n p) ⟩
|
|
254
|
96 n * n * p ∎ ) ⟩
|
|
250
|
97 n * n ∎ } where open ≡-Reasoning
|
|
57
|
98
|
|
320
|
99 mkRational : ( i j : ℕ ) → 0 < j → Rational
|
|
|
100 mkRational zero j 0<j = record { i = 0 ; j = 1 ; coprime = refl ; 0<j = s≤s z≤n }
|
|
321
|
101 mkRational (suc i) (suc j) (s≤s 0<j) = record { i = Dividable.factor id ; j = Dividable.factor jd ; coprime = cop ; 0<j = 0<fj } where
|
|
320
|
102 d : ℕ
|
|
321
|
103 d = gcd (suc i) (suc j)
|
|
|
104 d>0 : gcd (suc i) (suc j) > 0
|
|
|
105 d>0 = GCD.gcd>0 (suc i) (suc j) (s≤s z≤n) (s≤s z≤n )
|
|
|
106 id : Dividable d (suc i)
|
|
|
107 id = proj1 (GCD.gcd-dividable (suc i) (suc j))
|
|
|
108 jd : Dividable d (suc j)
|
|
|
109 jd = proj2 (GCD.gcd-dividable (suc i) (suc j))
|
|
320
|
110 0<fj : Dividable.factor jd > 0
|
|
|
111 0<fj = 0<factor d>0 (s≤s z≤n ) jd
|
|
|
112 cop : gcd (Dividable.factor id) (Dividable.factor jd) ≡ 1
|
|
321
|
113 cop = GCD.gcd-div-1 {suc i} {suc j} (s≤s z≤n) (s≤s z≤n )
|
|
320
|
114
|
|
321
|
115 r1 : {x y : ℕ} → x > 0 → y > 0 → x * y > 0
|
|
|
116 r1 {x} {y} x>0 y>0 = begin
|
|
320
|
117 1 * 1 ≤⟨ *≤ {1} {x} {1} x>0 ⟩
|
|
|
118 x * 1 ≡⟨ *-comm x 1 ⟩
|
|
|
119 1 * x ≤⟨ *≤ {1} {y} {x} y>0 ⟩
|
|
|
120 y * x ≡⟨ *-comm y x ⟩
|
|
|
121 x * y ∎ where open ≤-Reasoning
|
|
185
|
122
|
|
321
|
123 Rational* : (r s : Rational) → Rational
|
|
|
124 Rational* r s = mkRational (Rational.i r * Rational.i s) (Rational.j r * Rational.j s) (r1 (Rational.0<j r) (Rational.0<j s) )
|
|
|
125
|
|
281
|
126 _r=_ : Rational → ℕ → Set
|
|
321
|
127 r r= p = p * Rational.j r ≡ Rational.i r
|
|
|
128
|
|
|
129 r3 : ( p : ℕ ) → p > 0 → ( r : Rational ) → Rational* r r r= p → p * Rational.j r * Rational.j r ≡ Rational.i r * Rational.i r
|
|
|
130 r3 p p>0 r rr = r4 where
|
|
|
131 i : ℕ
|
|
|
132 i = Rational.i r * Rational.i r
|
|
|
133 j : ℕ
|
|
|
134 j = Rational.j r * Rational.j r
|
|
|
135 0<j : 0 < j
|
|
|
136 0<j = r1 (Rational.0<j r) (Rational.0<j r)
|
|
|
137 d1 = Dividable.factor (proj1 (GCD.gcd-dividable i j))
|
|
|
138 d2 = Dividable.factor (proj2 (GCD.gcd-dividable i j))
|
|
|
139 ri=id : ( i j : ℕ) → (0<i : 0 < i ) → (0<j : 0 < j)
|
|
|
140 → Rational.i (mkRational i j 0<j) ≡ Dividable.factor (proj1 (GCD.gcd-dividable i j))
|
|
|
141 ri=id (suc i₁) (suc j₁) 0<i (s≤s 0<j₁) = refl
|
|
|
142 ri=jd : ( i j : ℕ) → (0<i : 0 < i ) → (0<j : 0 < j)
|
|
|
143 → Rational.j (mkRational i j 0<j) ≡ Dividable.factor (proj2 (GCD.gcd-dividable i j))
|
|
|
144 ri=jd (suc i₁) (suc j₁) 0<i (s≤s 0<j₁) = refl
|
|
322
|
145 r0=id : ( i j : ℕ) → (0=i : 0 ≡ i ) → (0<j : 0 < j)
|
|
|
146 → Rational.i (mkRational i j 0<j) ≡ 0
|
|
|
147 r0=id 0 j refl 0<j = refl
|
|
|
148 r0=jd : ( i j : ℕ) → (0=i : 0 ≡ i ) → (0<j : 0 < j)
|
|
|
149 → Rational.j (mkRational i j 0<j) ≡ 1
|
|
|
150 r0=jd 0 j refl 0<j = refl
|
|
321
|
151 d : ℕ
|
|
|
152 d = gcd i j
|
|
|
153 r7 : i > 0 → d > 0
|
|
|
154 r7 0<i = GCD.gcd>0 _ _ 0<i 0<j
|
|
|
155 r6 : i > 0 → d2 > 0
|
|
|
156 r6 0<i = 0<factor (r7 0<i ) 0<j (proj2 (GCD.gcd-dividable i j))
|
|
|
157 r8 : 0 < i → d2 * p ≡ d1
|
|
|
158 r8 0<i = begin
|
|
|
159 d2 * p ≡⟨ *-comm d2 p ⟩
|
|
|
160 p * d2 ≡⟨ cong (λ k → p * k ) (sym (ri=jd i j 0<i 0<j )) ⟩
|
|
|
161 p * Rational.j (mkRational i j _ ) ≡⟨ rr ⟩
|
|
|
162 Rational.i (Rational* r r) ≡⟨ ri=id i j 0<i 0<j ⟩
|
|
|
163 d1 ∎ where open ≡-Reasoning
|
|
|
164 r4 : p * Rational.j r * Rational.j r ≡ Rational.i r * Rational.i r
|
|
|
165 r4 with <-cmp (Rational.i r * Rational.i r) 0
|
|
322
|
166 ... | tri≈ ¬a b ¬c = ⊥-elim (nat-≡< (begin
|
|
|
167 0 ≡⟨ sym (r0=id i j (sym b) 0<j ) ⟩
|
|
|
168 Rational.i (mkRational (Rational.i r * Rational.i r) (Rational.j r * Rational.j r) _ ) ≡⟨ sym rr ⟩
|
|
|
169 p * Rational.j (mkRational (Rational.i r * Rational.i r) (Rational.j r * Rational.j r) _ ) ≡⟨ cong (λ k → p * k ) (r0=jd i j (sym b) 0<j ) ⟩
|
|
|
170 p * 1 ≡⟨ m*1=m ⟩
|
|
|
171 p ∎ ) p>0 ) where open ≡-Reasoning
|
|
321
|
172 ... | tri> ¬a ¬b c = begin
|
|
|
173 p * Rational.j r * Rational.j r ≡⟨ *-cancel-left (r6 c) ( begin
|
|
322
|
174 d2 * ((p * Rational.j r) * Rational.j r) ≡⟨ sym (*-assoc d2 _ _) ⟩
|
|
|
175 (d2 * ( p * Rational.j r )) * Rational.j r ≡⟨ cong (λ k → k * Rational.j r) (sym (*-assoc d2 _ _ )) ⟩
|
|
321
|
176 (d2 * p) * Rational.j r * Rational.j r ≡⟨ cong (λ k → k * Rational.j r * Rational.j r) (r8 c) ⟩
|
|
|
177 d1 * Rational.j r * Rational.j r ≡⟨ *-cancel-left (r7 c) ( begin
|
|
322
|
178 d * ((d1 * Rational.j r) * Rational.j r) ≡⟨ cong (λ k → d * k ) (*-assoc d1 _ _ )⟩
|
|
|
179 d * (d1 * (Rational.j r * Rational.j r)) ≡⟨ sym (*-assoc d _ _) ⟩
|
|
|
180 (d * d1) * (Rational.j r * Rational.j r) ≡⟨ cong (λ k → k * j) (*-comm d _ ) ⟩
|
|
|
181 (d1 * d) * j ≡⟨ cong (λ k → k * j) (+-comm 0 (d1 * d) ) ⟩
|
|
321
|
182 (d1 * d + 0) * j ≡⟨ cong (λ k → k * j ) (Dividable.is-factor (proj1 (GCD.gcd-dividable i j)) ) ⟩
|
|
|
183 i * j ≡⟨ *-comm i j ⟩
|
|
|
184 j * i ≡⟨ cong (λ k → k * i ) (sym (Dividable.is-factor (proj2 (GCD.gcd-dividable i j))) ) ⟩
|
|
322
|
185 (d2 * GCD.gcd i j + 0) * i ≡⟨ cong (λ k → k * i ) (+-comm (d2 * d ) 0) ⟩
|
|
|
186 (d2 * d) * i ≡⟨ cong (λ k → k * i ) (*-comm d2 _ ) ⟩
|
|
|
187 (d * d2) * i ≡⟨ *-assoc d _ _ ⟩
|
|
321
|
188 d * (d2 * (Rational.i r * Rational.i r)) ∎ ) ⟩
|
|
|
189 d2 * (Rational.i r * Rational.i r) ∎ ) ⟩
|
|
|
190 Rational.i r * Rational.i r ∎ where open ≡-Reasoning
|
|
|
191
|
|
|
192
|
|
281
|
193
|
|
320
|
194 root-prime-irrational1 : ( p : ℕ ) → Prime p → ( r : Rational ) → ¬ ( Rational* r r r= p )
|
|
321
|
195 root-prime-irrational1 p pr r div with <-cmp (Rational.j r) 1
|
|
|
196 ... | tri< a ¬b ¬c = ⊥-elim (nat-≤> (Rational.0<j r) a )
|
|
322
|
197 ... | tri≈ ¬a b ¬c = ⊥-elim (nat-≡< r04 (r03 r01)) where
|
|
|
198 i = Rational.i r
|
|
|
199 j = Rational.j r
|
|
|
200 r00 : p * j * j ≡ i * i
|
|
|
201 r00 = r3 p (<-trans a<sa (Prime.p>1 pr )) r div
|
|
|
202 r01 : p ≡ i * i
|
|
323
|
203 r01 = begin
|
|
|
204 p ≡⟨ sym m*1=m ⟩
|
|
|
205 p * 1 ≡⟨ sym m*1=m ⟩
|
|
|
206 p * 1 * 1 ≡⟨ cong (λ k → p * k * k ) (sym b) ⟩
|
|
|
207 p * j * j ≡⟨ r00 ⟩
|
|
|
208 i * i ∎ where open ≡-Reasoning
|
|
322
|
209 r03 : p ≡ i * i → i > 1
|
|
323
|
210 r03 eq with <-cmp i 1
|
|
|
211 ... | tri< a ¬b ¬c = {!!}
|
|
|
212 ... | tri≈ ¬a b ¬c = {!!}
|
|
|
213 ... | tri> ¬a ¬b c = c
|
|
|
214 r02 : p ≡ i * i → gcd p i ≡ i
|
|
|
215 r02 eq = GCD.div→gcd (r03 r01) record { factor = i ; is-factor = trans (+-comm _ 0 ) (sym r01) }
|
|
322
|
216 r04 : 1 ≡ i
|
|
|
217 r04 = begin
|
|
323
|
218 1 ≡⟨ sym (Prime.isPrime pr _ {!!} {!!} ) ⟩
|
|
|
219 gcd p i ≡⟨ r02 r01 ⟩
|
|
322
|
220 i ∎ where open ≡-Reasoning
|
|
321
|
221 ... | tri> ¬a ¬b c with <-cmp (Rational.i r) 1
|
|
322
|
222 ... | tri< a ¬b₁ ¬c = {!!} where
|
|
|
223 i = Rational.i r
|
|
|
224 j = Rational.j r
|
|
|
225 r00 : p * j * j ≡ i * i
|
|
|
226 r00 = r3 p (<-trans a<sa (Prime.p>1 pr )) r div
|
|
|
227 r06 : i ≡ 0
|
|
|
228 r06 = {!!}
|
|
|
229 r05 : p * j * j ≡ i * i -- j > 0 → p * j * j > 0
|
|
|
230 r05 = {!!}
|
|
|
231 ... | tri≈ ¬a₁ b ¬c = {!!} where
|
|
|
232 i = Rational.i r
|
|
|
233 j = Rational.j r
|
|
|
234 r00 : p * j * j ≡ i * i
|
|
|
235 r00 = r3 p (<-trans a<sa (Prime.p>1 pr )) r div
|
|
|
236 r07 : p * j * j ≡ i * i -- j > 0 → p * j * j > 0
|
|
|
237 r07 = {!!}
|
|
321
|
238 ... | tri> ¬a₁ ¬b₁ c₁ = root-prime-irrational (Rational.j r) (Rational.i r) p c pr c₁ (r3 p (<-trans a<sa (Prime.p>1 pr ) ) r div)
|
|
|
239 (trans (GCD.gcdsym {Rational.j r} {_} ) (Rational.coprime r) )
|
