|
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
|
|
|
11 even : (n : ℕ ) → Set
|
|
141
|
12 even zero = ⊤
|
|
|
13 even (suc zero) = ⊥
|
|
|
14 even (suc (suc n)) = even n
|
|
57
|
15
|
|
|
16 even? : (n : ℕ ) → Dec ( even n )
|
|
141
|
17 even? zero = yes tt
|
|
|
18 even? (suc zero) = no (λ ())
|
|
|
19 even? (suc (suc n)) = even? n
|
|
|
20
|
|
|
21 n+even : {n m : ℕ } → even n → even m → even ( n + m )
|
|
|
22 n+even {zero} {zero} tt tt = tt
|
|
|
23 n+even {zero} {suc m} tt em = em
|
|
|
24 n+even {suc (suc n)} {m} en em = n+even {n} {m} en em
|
|
|
25
|
|
|
26 n*even : {m n : ℕ } → even n → even ( m * n )
|
|
|
27 n*even {zero} {n} en = tt
|
|
|
28 n*even {suc m} {n} en = n+even {n} {m * n} en (n*even {m} {n} en)
|
|
|
29
|
|
|
30 even*n : {n m : ℕ } → even n → even ( n * m )
|
|
|
31 even*n {n} {m} en = subst even (*-comm m n) (n*even {m} {n} en)
|
|
|
32
|
|
|
33 gcd1 : ( i i0 j j0 : ℕ ) → ℕ
|
|
146
|
34 gcd1 zero i0 zero j0 with <-cmp i0 j0
|
|
|
35 ... | tri< a ¬b ¬c = j0
|
|
|
36 ... | tri≈ ¬a refl ¬c = i0
|
|
|
37 ... | tri> ¬a ¬b c = i0
|
|
141
|
38 gcd1 zero i0 (suc zero) j0 = 1
|
|
|
39 gcd1 zero zero (suc (suc j)) j0 = j0
|
|
|
40 gcd1 zero (suc i0) (suc (suc j)) j0 = gcd1 i0 (suc i0) (suc j) (suc (suc j))
|
|
|
41 gcd1 (suc zero) i0 zero j0 = 1
|
|
|
42 gcd1 (suc (suc i)) i0 zero zero = i0
|
|
|
43 gcd1 (suc (suc i)) i0 zero (suc j0) = gcd1 (suc i) (suc (suc i)) j0 (suc j0)
|
|
|
44 gcd1 (suc i) i0 (suc j) j0 = gcd1 i i0 j j0
|
|
|
45
|
|
|
46 gcd : ( i j : ℕ ) → ℕ
|
|
|
47 gcd i j = gcd1 i i j j
|
|
57
|
48
|
|
141
|
49 even→gcd=2 : {n : ℕ} → even n → n > 0 → gcd n 2 ≡ 2
|
|
|
50 even→gcd=2 {suc (suc zero)} en (s≤s z≤n) = refl
|
|
|
51 even→gcd=2 {suc (suc (suc (suc n)))} en (s≤s z≤n) = begin
|
|
|
52 gcd (suc (suc (suc (suc n)))) 2
|
|
|
53 ≡⟨⟩
|
|
|
54 gcd (suc (suc n)) 2
|
|
|
55 ≡⟨ even→gcd=2 {suc (suc n)} en (s≤s z≤n) ⟩
|
|
|
56 2
|
|
|
57 ∎ where open ≡-Reasoning
|
|
57
|
58
|
|
142
|
59 open import nat
|
|
141
|
60
|
|
145
|
61 -- gcd26 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n m ≡ gcd (n - m) m
|
|
|
62 -- gcd25 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n m ≡ gcd m n
|
|
|
63 -- gcd27 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n k ≡ k → k ≤ n
|
|
143
|
64
|
|
146
|
65 gcd22 : ( i i0 o o0 : ℕ ) → gcd1 (suc i) i0 (suc o) o0 ≡ gcd1 i i0 o o0
|
|
|
66 gcd22 zero i0 zero o0 = refl
|
|
|
67 gcd22 zero i0 (suc o) o0 = refl
|
|
|
68 gcd22 (suc i) i0 zero o0 = refl
|
|
|
69 gcd22 (suc i) i0 (suc o) o0 = refl
|
|
|
70
|
|
|
71 gcdsym : { n m : ℕ} → gcd n m ≡ gcd m n
|
|
|
72 gcdsym {n} {m} = gcdsym1 n n m m where
|
|
|
73 gcdsym0 : (i : ℕ) → gcd1 zero i zero i ≡ gcd1 zero i zero i
|
|
|
74 gcdsym0 i = refl
|
|
|
75 gcdsym2 : (i j : ℕ) → gcd1 zero i zero j ≡ gcd1 zero j zero i
|
|
|
76 gcdsym2 i j with <-cmp i j | <-cmp j i
|
|
|
77 ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = ⊥-elim (nat-<> a a₁)
|
|
|
78 ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (nat-≡< (sym b) a)
|
|
|
79 ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = refl
|
|
|
80 ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ⊥-elim (nat-≡< (sym b) a)
|
|
|
81 ... | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = refl
|
|
|
82 ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim (nat-≡< b c)
|
|
|
83 ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = refl
|
|
|
84 ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = ⊥-elim (nat-≡< b c)
|
|
|
85 ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = ⊥-elim (nat-<> c c₁)
|
|
|
86 gcdsym1 : ( i i0 j j0 : ℕ ) → gcd1 i i0 j j0 ≡ gcd1 j j0 i i0
|
|
|
87 gcdsym1 zero zero zero zero = refl
|
|
|
88 gcdsym1 zero zero zero (suc j0) = refl
|
|
|
89 gcdsym1 zero (suc i0) zero zero = refl
|
|
|
90 gcdsym1 zero (suc i0) zero (suc j0) = gcdsym2 (suc i0) (suc j0)
|
|
|
91 gcdsym1 zero zero (suc zero) j0 = refl
|
|
|
92 gcdsym1 zero zero (suc (suc j)) j0 = refl
|
|
|
93 gcdsym1 zero (suc i0) (suc zero) j0 = refl
|
|
|
94 gcdsym1 zero (suc i0) (suc (suc j)) j0 = gcdsym1 i0 (suc i0) (suc j) (suc (suc j))
|
|
|
95 gcdsym1 (suc zero) i0 zero j0 = refl
|
|
|
96 gcdsym1 (suc (suc i)) i0 zero zero = refl
|
|
|
97 gcdsym1 (suc (suc i)) i0 zero (suc j0) = gcdsym1 (suc i) (suc (suc i))j0 (suc j0)
|
|
|
98 gcdsym1 (suc i) i0 (suc j) j0 = subst₂ (λ j k → j ≡ k ) (sym (gcd22 i _ _ _)) (sym (gcd22 j _ _ _)) (gcdsym1 i i0 j j0 )
|
|
|
99
|
|
142
|
100 gcd24 : { n m k : ℕ} → n > 1 → m > 1 → k > 1 → gcd n k ≡ k → gcd m k ≡ k → ¬ ( gcd n m ≡ 1 )
|
|
|
101 gcd24 {n} {m} {k} 1<n 1<m 1<k gn gm gnm = gcd21 n n m m k k 1<n 1<m 1<k gn gm gnm where
|
|
145
|
102 gcd23 : { j j0 : ℕ } → 1 < j → 1 < j0 → ¬ (gcd1 zero zero j j0 ≡ 1)
|
|
146
|
103 gcd23 {zero} {suc j0} 1<j 1<j0 _ = {!!}
|
|
145
|
104 gcd23 {suc zero} {suc j0} 1<j 1<j0 gn = nat-<≡ 1<j
|
|
|
105 gcd23 {suc (suc j)} {suc .0} 1<j 1<j0 refl = nat-<≡ 1<j0
|
|
143
|
106 1<ss : {j : ℕ} → 1 < suc (suc j)
|
|
|
107 1<ss = s≤s (s≤s z≤n)
|
|
142
|
108 gcd21 : ( i i0 j j0 o o0 : ℕ ) → 1 < i0 → 1 < j0 → 1 < o0 → gcd1 i i0 o o0 ≡ k → gcd1 j j0 o o0 ≡ k → gcd1 i i0 j j0 ≡ 1 → ⊥
|
|
146
|
109 gcd21 zero i0 zero j0 o o0 1<i 1<j 1<o refl gm gnm = nat-≡< (sym gnm) {!!}
|
|
145
|
110 --- gcd1 zero i0 o o0 ≡ k o = suc zero → k ≡ 1
|
|
|
111 --- i0 = zero , o = suc (suc o) → o0 = k -> gcd1 zero zero (suc j) j0 ≡ 1
|
|
|
112 -- i0 = suc i0, o = suc (suc o) → gn = gcd1 i0 (suc i0) (suc o) (suc (suc o))
|
|
146
|
113 gcd21 zero i0 (suc j) j0 zero o0 1<i 1<j 1<o refl gm gnm = {!!}
|
|
|
114 gcd21 zero i0 (suc j) j0 (suc zero) o0 1<i 1<j 1<o refl gm gnm = nat-<≡ 1<k
|
|
|
115 gcd21 zero (suc i0) (suc j) j0 (suc (suc o)) o0 1<i 1<j 1<o gn gm gnm =
|
|
|
116 gcd21 i0 {!!} (suc j) j0 (suc o) (suc (suc o)) 1<i 1<j {!!} gn {!!} {!!}
|
|
145
|
117 gcd21 (suc i) i0 zero j0 o o0 1<i 1<j 1<o gn gm gnm = {!!}
|
|
|
118 -- ?
|
|
142
|
119 gcd21 (suc i) i0 (suc j) j0 zero o0 1<i 1<j 1<o gn gm gnm = {!!}
|
|
|
120 gcd21 (suc i) i0 (suc j) j0 (suc o) o0 1<i 1<j 1<o gn gm gnm =
|
|
|
121 gcd21 i i0 j j0 o o0 1<i 1<j 1<o (subst (λ m → m ≡ k) (gcd22 i i0 _ _ ) gn)
|
|
|
122 (subst (λ m → m ≡ k) (gcd22 j j0 _ _ ) gm) (subst (λ k → k ≡ 1) (gcd22 i i0 _ _ ) gnm)
|
|
141
|
123
|
|
|
124 record Even (i : ℕ) : Set where
|
|
|
125 field
|
|
|
126 j : ℕ
|
|
|
127 is-twice : i ≡ 2 * j
|
|
|
128
|
|
|
129 e2 : (i : ℕ) → even i → Even i
|
|
|
130 e2 zero en = record { j = 0 ; is-twice = refl }
|
|
|
131 e2 (suc (suc i)) en = record { j = suc (Even.j (e2 i en )) ; is-twice = e21 } where
|
|
|
132 e21 : suc (suc i) ≡ 2 * suc (Even.j (e2 i en))
|
|
|
133 e21 = begin
|
|
|
134 suc (suc i) ≡⟨ cong (λ k → suc (suc k)) (Even.is-twice (e2 i en)) ⟩
|
|
|
135 suc (suc (2 * Even.j (e2 i en))) ≡⟨ sym (*-distribˡ-+ 2 1 _) ⟩
|
|
|
136 2 * suc (Even.j (e2 i en)) ∎ where open ≡-Reasoning
|
|
|
137
|
|
|
138 record Odd (i : ℕ) : Set where
|
|
|
139 field
|
|
|
140 j : ℕ
|
|
|
141 is-twice : i ≡ suc (2 * j )
|
|
57
|
142
|
|
141
|
143 odd2 : (i : ℕ) → ¬ even i → even (suc i)
|
|
|
144 odd2 zero ne = ⊥-elim ( ne tt )
|
|
|
145 odd2 (suc zero) ne = tt
|
|
|
146 odd2 (suc (suc i)) ne = odd2 i ne
|
|
|
147
|
|
|
148 odd3 : (i : ℕ) → ¬ even i → Odd i
|
|
|
149 odd3 zero ne = ⊥-elim ( ne tt )
|
|
|
150 odd3 (suc zero) ne = record { j = 0 ; is-twice = refl }
|
|
|
151 odd3 (suc (suc i)) ne = record { j = Even.j (e2 (suc i) (odd2 i ne)) ; is-twice = odd31 } where
|
|
|
152 odd31 : suc (suc i) ≡ suc (2 * Even.j (e2 (suc i) (odd2 i ne)))
|
|
|
153 odd31 = begin
|
|
|
154 suc (suc i) ≡⟨ cong suc (Even.is-twice (e2 (suc i) (odd2 i ne))) ⟩
|
|
|
155 suc (2 * (Even.j (e2 (suc i) (odd2 i ne)))) ∎ where open ≡-Reasoning
|
|
|
156
|
|
|
157 odd4 : (i : ℕ) → even i → ¬ even ( suc i )
|
|
|
158 odd4 (suc (suc i)) en en1 = odd4 i en en1
|
|
|
159
|
|
|
160 even^2 : {n : ℕ} → even ( n * n ) → even n
|
|
|
161 even^2 {n} en with even? n
|
|
|
162 ... | yes y = y
|
|
|
163 ... | 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
|
|
|
164 m : ℕ
|
|
|
165 m = Odd.j ( odd3 n ne )
|
|
|
166 ee3 : even (2 * m)
|
|
|
167 ee3 = subst (λ k → even k ) (*-comm m 2) (n*even {m} {2} tt )
|
|
|
168 ee4 : even ((2 * m) * suc (2 * m))
|
|
|
169 ee4 = even*n {(2 * m)} {suc (2 * m)} (even*n {2} {m} tt )
|
|
|
170 ee2 : n * n ≡ suc (2 * m) + ((2 * m) * (suc (2 * m) ))
|
|
|
171 ee2 = begin n * n ≡⟨ cong ( λ k → k * k) (Odd.is-twice (odd3 n ne)) ⟩
|
|
|
172 suc (2 * m) * suc (2 * m) ≡⟨ *-distribʳ-+ (suc (2 * m)) 1 ((2 * m) ) ⟩
|
|
|
173 (1 * suc (2 * m)) + 2 * m * suc (2 * m) ≡⟨ cong (λ k → k + 2 * m * suc (2 * m)) (begin
|
|
|
174 suc m + 1 * m + 0 * (suc m + 1 * m ) ≡⟨ +-comm (suc m + 1 * m) 0 ⟩
|
|
|
175 suc m + 1 * m ≡⟨⟩
|
|
|
176 suc (2 * m)
|
|
|
177 ∎) ⟩ suc (2 * m) + 2 * m * suc (2 * m) ∎ where open ≡-Reasoning
|
|
57
|
178
|
|
141
|
179 open import nat
|
|
|
180
|
|
|
181 e3 : {i j : ℕ } → 2 * i ≡ 2 * j → i ≡ j
|
|
|
182 e3 {zero} {zero} refl = refl
|
|
|
183 e3 {suc x} {suc y} eq with <-cmp x y
|
|
|
184 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< eq (s≤s (<-trans (<-plus a) (<-plus-0 (s≤s (<-plus a ))))))
|
|
|
185 ... | tri≈ ¬a b ¬c = cong suc b
|
|
|
186 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym eq) (s≤s (<-trans (<-plus c) (<-plus-0 (s≤s (<-plus c ))))))
|
|
|
187
|
|
|
188 record Rational : Set where
|
|
|
189 field
|
|
|
190 i j : ℕ
|
|
|
191 coprime : gcd i j ≡ 1
|
|
57
|
192
|
|
142
|
193 root2-irrational : ( n m : ℕ ) → n > 1 → m > 1 → 2 * n * n ≡ m * m → ¬ (gcd n m ≡ 1)
|
|
|
194 root2-irrational n m n>1 m>1 2nm = gcd24 {n} {m} n>1 m>1 (s≤s (s≤s z≤n)) (even→gcd=2 rot7 (rot5 n>1)) (even→gcd=2 ( even^2 {m} ( rot1)) (rot5 m>1))where
|
|
|
195 rot5 : {n : ℕ} → n > 1 → n > 0
|
|
|
196 rot5 {n} lt = <-trans a<sa lt
|
|
141
|
197 rot1 : even ( m * m )
|
|
|
198 rot1 = subst (λ k → even k ) rot4 (n*even {n * n} {2} tt ) where
|
|
|
199 rot4 : (n * n) * 2 ≡ m * m
|
|
|
200 rot4 = begin
|
|
|
201 (n * n) * 2 ≡⟨ *-comm (n * n) 2 ⟩
|
|
|
202 2 * ( n * n ) ≡⟨ sym (*-assoc 2 n n) ⟩
|
|
|
203 2 * n * n ≡⟨ 2nm ⟩
|
|
|
204 m * m ∎ where open ≡-Reasoning
|
|
|
205 E : Even m
|
|
|
206 E = e2 m ( even^2 {m} ( rot1 ))
|
|
|
207 rot2 : 2 * n * n ≡ 2 * Even.j E * m
|
|
|
208 rot2 = subst (λ k → 2 * n * n ≡ k * m ) (Even.is-twice E) 2nm
|
|
|
209 rot3 : n * n ≡ Even.j E * m
|
|
|
210 rot3 = e3 ( begin
|
|
|
211 2 * (n * n) ≡⟨ sym (*-assoc 2 n _) ⟩
|
|
|
212 2 * n * n ≡⟨ rot2 ⟩
|
|
|
213 2 * Even.j E * m ≡⟨ *-assoc 2 (Even.j E) m ⟩
|
|
|
214 2 * (Even.j E * m) ∎ ) where open ≡-Reasoning
|
|
|
215 rot7 : even n
|
|
|
216 rot7 = even^2 {n} (subst (λ k → even k) (sym rot3) ((n*even {Even.j E} {m} ( even^2 {m} ( rot1 )))))
|
|
57
|
217
|
