|
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 : ℕ
|
|
281
|
19 coprime : GCD.gcd i j ≡ 1
|
|
|
20
|
|
|
21 -- record Dividable (n m : ℕ ) : Set where
|
|
|
22 -- field
|
|
|
23 -- factor : ℕ
|
|
|
24 -- is-factor : factor * n + 0 ≡ m
|
|
|
25
|
|
|
26 gcd : (i j : ℕ) → ℕ
|
|
|
27 gcd = GCD.gcd
|
|
|
28
|
|
|
29 gcd-euclid : ( p a b : ℕ ) → 1 < p → 0 < a → 0 < b → ((i : ℕ ) → i < p → 0 < i → gcd p i ≡ 1)
|
|
|
30 → Dividable p (a * b) → Dividable p a ∨ Dividable p b
|
|
|
31 gcd-euclid = GCD.gcd-euclid
|
|
|
32
|
|
|
33 gcd-div1 : ( i j k : ℕ ) → k > 1 → (if : Dividable k i) (jf : Dividable k j )
|
|
|
34 → Dividable k ( gcd i j )
|
|
|
35 gcd-div1 = GCD.gcd-div
|
|
57
|
36
|
|
231
|
37 open _∧_
|
|
|
38
|
|
|
39 open import prime
|
|
|
40
|
|
233
|
41 divdable^2 : ( n k : ℕ ) → 1 < k → 1 < n → Prime k → Dividable k ( n * n ) → Dividable k n
|
|
|
42 divdable^2 zero zero () 1<n pk dn2
|
|
|
43 divdable^2 (suc n) (suc k) 1<k 1<n pk dn2 with decD {suc k} {suc n} 1<k
|
|
159
|
44 ... | yes y = y
|
|
250
|
45 ... | 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
|
46 ... | case1 dn = dn
|
|
|
47 ... | case2 dm = dm
|
|
159
|
48
|
|
255
|
49 -- p * n * n ≡ m * m means (m/n)^2 = p
|
|
|
50 -- rational m/n requires m and n is comprime each other which contradicts the condition
|
|
|
51
|
|
254
|
52 root-prime-irrational : ( n m p : ℕ ) → n > 1 → Prime p → m > 1 → p * n * n ≡ m * m → ¬ (gcd n m ≡ 1)
|
|
|
53 root-prime-irrational n m 0 n>1 pn m>1 pnm = ⊥-elim ( nat-≡< refl (<-trans a<sa (Prime.p>1 pn)))
|
|
281
|
54 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
|
|
|
55 p = suc p0
|
|
254
|
56 1<sp : 1 < p
|
|
253
|
57 1<sp = Prime.p>1 pn
|
|
281
|
58 rot13 : {m : ℕ } → Dividable (suc p0) m → m ≡ 1 → ⊥
|
|
185
|
59 rot13 d refl with Dividable.factor d | Dividable.is-factor d
|
|
253
|
60 ... | zero | () -- gcd 0 m ≡ 1
|
|
254
|
61 ... | suc n | x = ⊥-elim ( nat-≡< (sym x) rot17 ) where -- x : (suc n * p + 0) ≡ 1
|
|
281
|
62 rot17 : suc n * (suc p0) + 0 > 1
|
|
253
|
63 rot17 = begin
|
|
|
64 2 ≡⟨ refl ⟩
|
|
254
|
65 suc (1 * 1 ) ≤⟨ 1<sp ⟩
|
|
|
66 suc p0 ≡⟨ cong suc (+-comm 0 _) ⟩
|
|
|
67 suc (p0 + 0) ≤⟨ s≤s (+-monoʳ-≤ p0 z≤n) ⟩
|
|
|
68 suc (p0 + n * p ) ≡⟨ +-comm 0 _ ⟩
|
|
|
69 suc n * p + 0 ∎ where open ≤-Reasoning
|
|
|
70 dm : Dividable p m
|
|
|
71 dm = divdable^2 m p 1<sp m>1 pn record { factor = n * n ; is-factor = begin
|
|
|
72 (n * n) * p + 0 ≡⟨ +-comm _ 0 ⟩
|
|
|
73 (n * n) * p ≡⟨ *-comm (n * n) p ⟩
|
|
|
74 p * (n * n) ≡⟨ sym (*-assoc p n n) ⟩
|
|
|
75 (p * n) * n ≡⟨ pnm ⟩
|
|
250
|
76 m * m ∎ } where open ≡-Reasoning
|
|
254
|
77 -- p * n * n = 2m' 2m'
|
|
251
|
78 -- n * n = m' 2m'
|
|
250
|
79 df = Dividable.factor dm
|
|
254
|
80 dn : Dividable p n
|
|
|
81 dn = divdable^2 n p 1<sp n>1 pn record { factor = df * df ; is-factor = begin
|
|
|
82 df * df * p + 0 ≡⟨ *-cancelʳ-≡ _ _ {p0} ( begin
|
|
|
83 (df * df * p + 0) * p ≡⟨ cong (λ k → k * p) (+-comm (df * df * p) 0) ⟩
|
|
281
|
84 ((df * df) * p ) * p ≡⟨ cong (λ k → k * p) (*-assoc df df p ) ⟩
|
|
254
|
85 (df * (df * p)) * p ≡⟨ cong (λ k → (df * k ) * p) (*-comm df p) ⟩
|
|
|
86 (df * (p * df)) * p ≡⟨ sym ( cong (λ k → k * p) (*-assoc df p df ) ) ⟩
|
|
|
87 ((df * p) * df) * p ≡⟨ *-assoc (df * p) df p ⟩
|
|
|
88 (df * p) * (df * p) ≡⟨ cong₂ (λ j k → j * k ) (+-comm 0 (df * p)) (+-comm 0 _) ⟩
|
|
|
89 (df * p + 0) * (df * p + 0) ≡⟨ cong₂ (λ j k → j * k) (Dividable.is-factor dm ) (Dividable.is-factor dm )⟩
|
|
253
|
90 m * m ≡⟨ sym pnm ⟩
|
|
281
|
91 p * n * n ≡⟨ cong (λ k → k * n) (*-comm p n) ⟩
|
|
|
92 n * p * n ≡⟨ *-assoc n p n ⟩
|
|
|
93 n * (p * n) ≡⟨ cong (λ k → n * k) (*-comm p n) ⟩
|
|
|
94 n * (n * p) ≡⟨ sym (*-assoc n n p) ⟩
|
|
254
|
95 n * n * p ∎ ) ⟩
|
|
250
|
96 n * n ∎ } where open ≡-Reasoning
|
|
57
|
97
|
|
281
|
98 Rational* : (r s : Rational) → Rational
|
|
|
99 Rational* r s = record { i = {!!} ; j = {!!} ; coprime = {!!} }
|
|
185
|
100
|
|
281
|
101 _r=_ : Rational → ℕ → Set
|
|
|
102 r r= n = (Rational.i r ≡ n) ∧ (Rational.j r ≡ 1)
|
|
|
103
|
|
|
104 root-prime-irrational1 : ( p : ℕ ) → Prime p → ¬ ( ( r : Rational ) → Rational* r r r= p )
|
|
|
105 root-prime-irrational1 = {!!}
|
