|
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
|
|
148
|
11 open import gcd
|
|
159
|
12 open import even
|
|
142
|
13 open import nat
|
|
141
|
14
|
|
|
15 record Rational : Set where
|
|
|
16 field
|
|
|
17 i j : ℕ
|
|
|
18 coprime : gcd i j ≡ 1
|
|
57
|
19
|
|
159
|
20 even→gcd=2 : {n : ℕ} → even n → n > 0 → gcd n 2 ≡ 2
|
|
|
21 even→gcd=2 {suc (suc zero)} en (s≤s z≤n) = refl
|
|
|
22 even→gcd=2 {suc (suc (suc (suc n)))} en (s≤s z≤n) = begin
|
|
|
23 gcd (suc (suc (suc (suc n)))) 2 ≡⟨⟩
|
|
|
24 gcd (suc (suc n)) 2 ≡⟨ even→gcd=2 {suc (suc n)} en (s≤s z≤n) ⟩
|
|
|
25 2 ∎ where open ≡-Reasoning
|
|
|
26
|
|
186
|
27 even→gcd : (n m : ℕ) → even n → even m → even (gcd n m)
|
|
|
28 even→gcd zero zero en em = tt
|
|
|
29 even→gcd zero (suc (suc m)) en em = em
|
|
|
30 even→gcd (suc (suc n)) zero en em = en
|
|
|
31 even→gcd (suc (suc n)) (suc (suc m)) en em = ee2 n n (suc (suc m)) (suc (suc m)) refl refl
|
|
|
32 (subst (λ k → even k) (gcdsym {suc (suc m)} {n}) (ee2 m m n n refl refl (subst (λ k → even k) (gcdsym {n} {m}) ee1))) where
|
|
|
33 ee1 : even (gcd n m)
|
|
|
34 ee1 = even→gcd n m en em
|
|
|
35 ee2 : (i i0 j j0 : ℕ) → i ≡ i0 → j ≡ j0 → even (gcd1 i i j0 j0) → even (gcd1 (suc (suc i)) (suc (suc i)) j0 j0)
|
|
|
36 ee2 i i0 j j0 i=i0 j=j0 e = {!!}
|
|
|
37
|
|
159
|
38 even^2 : {n : ℕ} → even ( n * n ) → even n
|
|
|
39 even^2 {n} en with even? n
|
|
|
40 ... | yes y = y
|
|
|
41 ... | no ne = ⊥-elim ( odd4 ((2 * m) + 2 * m * suc (2 * m)) (n+even {2 * m} {2 * m * suc (2 * m)} ee3 ee4) (subst (λ k → even k) ee2 en )) where
|
|
|
42 m : ℕ
|
|
|
43 m = Odd.j ( odd3 n ne )
|
|
|
44 ee3 : even (2 * m)
|
|
|
45 ee3 = subst (λ k → even k ) (*-comm m 2) (n*even {m} {2} tt )
|
|
|
46 ee4 : even ((2 * m) * suc (2 * m))
|
|
|
47 ee4 = even*n {(2 * m)} {suc (2 * m)} (even*n {2} {m} tt )
|
|
|
48 ee2 : n * n ≡ suc (2 * m) + ((2 * m) * (suc (2 * m) ))
|
|
|
49 ee2 = begin n * n ≡⟨ cong ( λ k → k * k) (Odd.is-twice (odd3 n ne)) ⟩
|
|
|
50 suc (2 * m) * suc (2 * m) ≡⟨ *-distribʳ-+ (suc (2 * m)) 1 ((2 * m) ) ⟩
|
|
|
51 (1 * suc (2 * m)) + 2 * m * suc (2 * m) ≡⟨ cong (λ k → k + 2 * m * suc (2 * m)) (begin
|
|
|
52 suc m + 1 * m + 0 * (suc m + 1 * m ) ≡⟨ +-comm (suc m + 1 * m) 0 ⟩
|
|
|
53 suc m + 1 * m ≡⟨⟩
|
|
|
54 suc (2 * m)
|
|
|
55 ∎) ⟩ suc (2 * m) + 2 * m * suc (2 * m) ∎ where open ≡-Reasoning
|
|
|
56
|
|
|
57 e3 : {i j : ℕ } → 2 * i ≡ 2 * j → i ≡ j
|
|
|
58 e3 {zero} {zero} refl = refl
|
|
|
59 e3 {suc x} {suc y} eq with <-cmp x y
|
|
|
60 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< eq (s≤s (<-trans (<-plus a) (<-plus-0 (s≤s (<-plus a ))))))
|
|
|
61 ... | tri≈ ¬a b ¬c = cong suc b
|
|
|
62 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym eq) (s≤s (<-trans (<-plus c) (<-plus-0 (s≤s (<-plus c ))))))
|
|
|
63
|
|
165
|
64 open Factor
|
|
164
|
65
|
|
186
|
66 -- gcd-div : ( i j k : ℕ ) → (if : Factor k i) (jf : Factor k j )
|
|
|
67 -- → remain if ≡ 0 → remain jf ≡ 0
|
|
|
68 -- → Dividable k ( gcd i j )
|
|
|
69
|
|
142
|
70 root2-irrational : ( n m : ℕ ) → n > 1 → m > 1 → 2 * n * n ≡ m * m → ¬ (gcd n m ≡ 1)
|
|
186
|
71 root2-irrational n m n>1 m>1 2nm = rot13 ( gcd-div n m 2 f2 fm (f3 n rot7) refl ) where
|
|
165
|
72 rot13 : {m : ℕ } → Dividable 2 m → m ≡ 1 → ⊥
|
|
185
|
73 rot13 d refl with Dividable.factor d | Dividable.is-factor d
|
|
|
74 ... | zero | ()
|
|
|
75 ... | suc n | ()
|
|
165
|
76 rot11 : {m : ℕ } → even m → Factor 2 m
|
|
|
77 rot11 {zero} em = record { factor = 0 ; remain = 0 ; is-factor = refl }
|
|
|
78 rot11 {suc zero} ()
|
|
|
79 rot11 {suc (suc m) } em = record { factor = suc (factor fc ) ; remain = remain fc ; is-factor = isfc } where
|
|
|
80 fc : Factor 2 m
|
|
|
81 fc = rot11 {m} em
|
|
|
82 isfc : suc (factor fc) * 2 + remain fc ≡ suc (suc m)
|
|
|
83 isfc = begin
|
|
|
84 suc (factor fc) * 2 + remain fc ≡⟨ cong (λ k → k + remain fc) (*-distribʳ-+ 2 1 (factor fc)) ⟩
|
|
|
85 ((1 * 2) + (factor fc)* 2 ) + remain fc ≡⟨⟩
|
|
|
86 ((1 + 1) + (factor fc)* 2 ) + remain fc ≡⟨ cong (λ k → k + remain fc) (+-assoc 1 1 _ ) ⟩
|
|
|
87 (1 + (1 + (factor fc)* 2 )) + remain fc ≡⟨⟩
|
|
|
88 suc (suc ((factor fc * 2) + remain fc )) ≡⟨ cong (λ x → suc (suc x)) (is-factor fc) ⟩
|
|
|
89 suc (suc m) ∎ where open ≡-Reasoning
|
|
142
|
90 rot5 : {n : ℕ} → n > 1 → n > 0
|
|
|
91 rot5 {n} lt = <-trans a<sa lt
|
|
141
|
92 rot1 : even ( m * m )
|
|
|
93 rot1 = subst (λ k → even k ) rot4 (n*even {n * n} {2} tt ) where
|
|
|
94 rot4 : (n * n) * 2 ≡ m * m
|
|
|
95 rot4 = begin
|
|
|
96 (n * n) * 2 ≡⟨ *-comm (n * n) 2 ⟩
|
|
|
97 2 * ( n * n ) ≡⟨ sym (*-assoc 2 n n) ⟩
|
|
|
98 2 * n * n ≡⟨ 2nm ⟩
|
|
|
99 m * m ∎ where open ≡-Reasoning
|
|
|
100 E : Even m
|
|
|
101 E = e2 m ( even^2 {m} ( rot1 ))
|
|
|
102 rot2 : 2 * n * n ≡ 2 * Even.j E * m
|
|
|
103 rot2 = subst (λ k → 2 * n * n ≡ k * m ) (Even.is-twice E) 2nm
|
|
|
104 rot3 : n * n ≡ Even.j E * m
|
|
|
105 rot3 = e3 ( begin
|
|
|
106 2 * (n * n) ≡⟨ sym (*-assoc 2 n _) ⟩
|
|
|
107 2 * n * n ≡⟨ rot2 ⟩
|
|
|
108 2 * Even.j E * m ≡⟨ *-assoc 2 (Even.j E) m ⟩
|
|
|
109 2 * (Even.j E * m) ∎ ) where open ≡-Reasoning
|
|
|
110 rot7 : even n
|
|
|
111 rot7 = even^2 {n} (subst (λ k → even k) (sym rot3) ((n*even {Even.j E} {m} ( even^2 {m} ( rot1 )))))
|
|
165
|
112 f2 : Factor 2 n
|
|
|
113 f2 = rot11 rot7
|
|
185
|
114 f3 : ( n : ℕ) → (e : even n ) → remain (rot11 {n} e) ≡ 0
|
|
|
115 f3 zero e = refl
|
|
|
116 f3 (suc (suc n)) e = f3 n e
|
|
165
|
117 fm : Factor 2 m
|
|
185
|
118 fm = record { factor = Even.j E ; remain = 0 ; is-factor = fm1 } where
|
|
|
119 fm1 : Even.j E * 2 + 0 ≡ m
|
|
|
120 fm1 = begin
|
|
|
121 Even.j E * 2 + 0 ≡⟨ +-comm _ 0 ⟩
|
|
|
122 Even.j E * 2 ≡⟨ *-comm (Even.j E) 2 ⟩
|
|
|
123 2 * Even.j E ≡⟨ sym ( Even.is-twice E ) ⟩
|
|
|
124 m ∎ where open ≡-Reasoning
|
|
57
|
125
|
|
185
|
126
|
