|
148
|
1 {-# OPTIONS --allow-unsolved-metas #-}
|
|
|
2 module gcd where
|
|
57
|
3
|
|
141
|
4 open import Data.Nat
|
|
|
5 open import Data.Nat.Properties
|
|
57
|
6 open import Data.Empty
|
|
141
|
7 open import Data.Unit using (⊤ ; tt)
|
|
57
|
8 open import Relation.Nullary
|
|
|
9 open import Relation.Binary.PropositionalEquality
|
|
141
|
10 open import Relation.Binary.Definitions
|
|
149
|
11 open import nat
|
|
151
|
12 open import logic
|
|
57
|
13
|
|
|
14 even : (n : ℕ ) → Set
|
|
141
|
15 even zero = ⊤
|
|
|
16 even (suc zero) = ⊥
|
|
|
17 even (suc (suc n)) = even n
|
|
57
|
18
|
|
|
19 even? : (n : ℕ ) → Dec ( even n )
|
|
141
|
20 even? zero = yes tt
|
|
|
21 even? (suc zero) = no (λ ())
|
|
|
22 even? (suc (suc n)) = even? n
|
|
|
23
|
|
|
24 n+even : {n m : ℕ } → even n → even m → even ( n + m )
|
|
|
25 n+even {zero} {zero} tt tt = tt
|
|
|
26 n+even {zero} {suc m} tt em = em
|
|
|
27 n+even {suc (suc n)} {m} en em = n+even {n} {m} en em
|
|
|
28
|
|
|
29 n*even : {m n : ℕ } → even n → even ( m * n )
|
|
|
30 n*even {zero} {n} en = tt
|
|
|
31 n*even {suc m} {n} en = n+even {n} {m * n} en (n*even {m} {n} en)
|
|
|
32
|
|
|
33 even*n : {n m : ℕ } → even n → even ( n * m )
|
|
|
34 even*n {n} {m} en = subst even (*-comm m n) (n*even {m} {n} en)
|
|
|
35
|
|
|
36 gcd1 : ( i i0 j j0 : ℕ ) → ℕ
|
|
146
|
37 gcd1 zero i0 zero j0 with <-cmp i0 j0
|
|
|
38 ... | tri< a ¬b ¬c = j0
|
|
|
39 ... | tri≈ ¬a refl ¬c = i0
|
|
|
40 ... | tri> ¬a ¬b c = i0
|
|
141
|
41 gcd1 zero i0 (suc zero) j0 = 1
|
|
|
42 gcd1 zero zero (suc (suc j)) j0 = j0
|
|
|
43 gcd1 zero (suc i0) (suc (suc j)) j0 = gcd1 i0 (suc i0) (suc j) (suc (suc j))
|
|
|
44 gcd1 (suc zero) i0 zero j0 = 1
|
|
|
45 gcd1 (suc (suc i)) i0 zero zero = i0
|
|
|
46 gcd1 (suc (suc i)) i0 zero (suc j0) = gcd1 (suc i) (suc (suc i)) j0 (suc j0)
|
|
|
47 gcd1 (suc i) i0 (suc j) j0 = gcd1 i i0 j j0
|
|
|
48
|
|
|
49 gcd : ( i j : ℕ ) → ℕ
|
|
|
50 gcd i j = gcd1 i i j j
|
|
57
|
51
|
|
141
|
52 even→gcd=2 : {n : ℕ} → even n → n > 0 → gcd n 2 ≡ 2
|
|
|
53 even→gcd=2 {suc (suc zero)} en (s≤s z≤n) = refl
|
|
|
54 even→gcd=2 {suc (suc (suc (suc n)))} en (s≤s z≤n) = begin
|
|
152
|
55 gcd (suc (suc (suc (suc n)))) 2 ≡⟨⟩
|
|
|
56 gcd (suc (suc n)) 2 ≡⟨ even→gcd=2 {suc (suc n)} en (s≤s z≤n) ⟩
|
|
|
57 2 ∎ where open ≡-Reasoning
|
|
57
|
58
|
|
145
|
59 -- gcd26 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n m ≡ gcd (n - m) m
|
|
|
60 -- gcd27 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n k ≡ k → k ≤ n
|
|
143
|
61
|
|
146
|
62 gcd22 : ( i i0 o o0 : ℕ ) → gcd1 (suc i) i0 (suc o) o0 ≡ gcd1 i i0 o o0
|
|
|
63 gcd22 zero i0 zero o0 = refl
|
|
|
64 gcd22 zero i0 (suc o) o0 = refl
|
|
|
65 gcd22 (suc i) i0 zero o0 = refl
|
|
|
66 gcd22 (suc i) i0 (suc o) o0 = refl
|
|
|
67
|
|
152
|
68 gcd20 : (i : ℕ) → gcd i 0 ≡ i
|
|
|
69 gcd20 zero = refl
|
|
|
70 gcd20 (suc i) = gcd201 (suc i) where
|
|
|
71 gcd201 : (i : ℕ ) → gcd1 i i zero zero ≡ i
|
|
|
72 gcd201 zero = refl
|
|
|
73 gcd201 (suc zero) = refl
|
|
|
74 gcd201 (suc (suc i)) = refl
|
|
|
75
|
|
151
|
76 gcdmm : (n m : ℕ) → gcd1 n m n m ≡ m
|
|
|
77 gcdmm zero m with <-cmp m m
|
|
|
78 ... | tri< a ¬b ¬c = refl
|
|
|
79 ... | tri≈ ¬a refl ¬c = refl
|
|
|
80 ... | tri> ¬a ¬b c = refl
|
|
|
81 gcdmm (suc n) m = subst (λ k → k ≡ m) (sym (gcd22 n m n m )) (gcdmm n m )
|
|
|
82
|
|
|
83 record Comp ( m n : ℕ ) : Set where
|
|
|
84 field
|
|
|
85 non-1 : 1 < m
|
|
|
86 comp : ℕ
|
|
|
87 is-comp : n * comp ≡ m
|
|
|
88
|
|
|
89 gcd27 : (n m i : ℕ) → 1 < m → gcd n i ≡ m → Comp m n ∨ Comp m i
|
|
|
90 gcd27 n m i 1<m gn = gcd271 n n i i gn where
|
|
|
91 gcd271 : (n n0 i i0 : ℕ ) → gcd1 n n0 i i0 ≡ m → Comp m n0 ∨ Comp m i0
|
|
|
92 gcd271 zero n0 zero i0 eq with <-cmp n0 i0
|
|
|
93 ... | tri< a ¬b ¬c = case2 (record { non-1 = 1<m ; comp = 1 ; is-comp = subst (λ k → k ≡ m) {!!} eq })
|
|
|
94 ... | tri≈ ¬a refl ¬c = case1 (record { non-1 = 1<m ; comp = 1 ; is-comp = subst (λ k → k ≡ m) {!!} eq })
|
|
|
95 ... | tri> ¬a ¬b c = case1 (record { non-1 = 1<m ; comp = 1 ; is-comp = subst (λ k → k ≡ m) {!!} eq })
|
|
|
96 gcd271 zero n0 (suc zero) i0 eq = ⊥-elim ( nat-≡< eq 1<m )
|
|
|
97 gcd271 zero zero (suc (suc i)) i0 eq = case2 (record { non-1 = 1<m ; comp = 1 ; is-comp = subst (λ k → k ≡ m) {!!} eq })
|
|
|
98 gcd271 zero (suc n0) (suc (suc i)) i0 eq with gcd271 n0 (suc n0) (suc i) (suc (suc i)) eq
|
|
|
99 ... | case1 t = case1 t
|
|
|
100 -- t : Comp m (suc (suc i)), (suc n0) + (suc (suc i)) ≡ i0
|
|
152
|
101 ... | case2 t = case1 (gcd272 t) where
|
|
|
102 gcd272 : Comp m (suc (suc i)) → Comp m (suc n0)
|
|
|
103 gcd272 = {!!}
|
|
151
|
104 gcd271 (suc zero) n0 zero i0 eq = ⊥-elim ( nat-≡< eq 1<m )
|
|
|
105 gcd271 (suc (suc n)) n0 zero zero eq = case2 (record { non-1 = 1<m ; comp = n0 ; is-comp = subst (λ k → k ≡ m) {!!} eq })
|
|
|
106 gcd271 (suc (suc n)) n0 zero (suc i0) eq = {!!}
|
|
152
|
107 gcd271 (suc n) n0 (suc i) i0 eq = gcd271 n n0 i i0 (trans (sym (gcd22 n n0 i i0)) eq )
|
|
148
|
108
|
|
|
109 gcd26 : (n m i : ℕ) → 1 < n → 1 < m → gcd n i ≡ m → ¬ ( gcd n m ≡ 1 )
|
|
|
110 gcd26 n m i 1<n 1<m gi g1 = gcd261 n n m m i i 1<n 1<m gi g1 where
|
|
|
111 gcd261 : (n n0 m m0 i i0 : ℕ) → 1 < n → 1 < m0 → gcd1 n n0 i i0 ≡ m0 → ¬ ( gcd1 n n0 m m0 ≡ 1 )
|
|
|
112 gcd261 zero n0 m m0 i i0 () 1<m gi g1
|
|
149
|
113 -- gi : gcd1 (suc n) n0 zero i0 ≡ m0
|
|
|
114 -- g1 : gcd1 (suc n) n0 m m0 ≡ 1
|
|
151
|
115 gcd261 (suc zero) n0 m m0 zero i0 1<n 1<m gi g1 = ⊥-elim ( nat-≡< gi 1<m )
|
|
|
116 gcd261 (suc (suc n)) n0 zero m0 zero zero 1<n 1<m gi g1 = {!!}
|
|
|
117 gcd261 (suc (suc n)) n0 zero m0 zero (suc i0) 1<n 1<m gi g1 = {!!}
|
|
|
118 gcd261 (suc (suc n)) n0 (suc zero) m0 zero i0 1<n 1<m gi g1 = {!!}
|
|
|
119 gcd261 (suc (suc n)) n0 (suc (suc m)) m0 zero zero 1<n 1<m gi g1 = {!!}
|
|
|
120 gcd261 (suc (suc n)) n0 (suc (suc m)) m0 zero (suc i0) 1<n 1<m gi g1 = {!!}
|
|
149
|
121 -- gi : gcd1 (suc n) n0 (suc i) i0 ≡ m0
|
|
|
122 -- g1 : gcd1 (suc n) n0 zero m0 ≡ 1
|
|
148
|
123 gcd261 (suc n) n0 zero m0 (suc i) i0 1<n 1<m gi g1 = {!!}
|
|
|
124 gcd261 (suc zero) n0 (suc m) m0 (suc i) i0 1<n 1<m gi g1 = ⊥-elim ( nat-<≡ 1<n )
|
|
149
|
125 gcd261 (suc (suc zero)) n0 (suc m) m0 (suc zero) i0 1<n 1<m gi g1 = ⊥-elim ( nat-≡< gi 1<m )
|
|
|
126 -- gi : gcd1 0 n0 i i0 ≡ m0
|
|
151
|
127 gcd261 (suc (suc zero)) n0 (suc zero) m0 (suc (suc i)) i0 1<n 1<m gi refl = {!!}
|
|
149
|
128 -- gi : gcd1 0 n0 i i0 ≡ m0
|
|
|
129 -- g1 : gcd1 0 n0 m m0 ≡ 1
|
|
|
130 gcd261 (suc (suc zero)) n0 (suc (suc m)) m0 (suc (suc i)) i0 1<n 1<m gi g1 = {!!}
|
|
148
|
131 gcd261 (suc (suc (suc n))) n0 (suc m) m0 (suc i) i0 1<n 1<m gi g1 =
|
|
|
132 gcd261 (suc (suc n)) n0 m m0 i i0 (s≤s (s≤s z≤n)) 1<m gi g1
|
|
|
133
|
|
147
|
134 gcdsym2 : (i j : ℕ) → gcd1 zero i zero j ≡ gcd1 zero j zero i
|
|
|
135 gcdsym2 i j with <-cmp i j | <-cmp j i
|
|
|
136 ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = ⊥-elim (nat-<> a a₁)
|
|
|
137 ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (nat-≡< (sym b) a)
|
|
|
138 ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = refl
|
|
|
139 ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ⊥-elim (nat-≡< (sym b) a)
|
|
|
140 ... | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = refl
|
|
|
141 ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim (nat-≡< b c)
|
|
|
142 ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = refl
|
|
|
143 ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = ⊥-elim (nat-≡< b c)
|
|
|
144 ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = ⊥-elim (nat-<> c c₁)
|
|
|
145 gcdsym1 : ( i i0 j j0 : ℕ ) → gcd1 i i0 j j0 ≡ gcd1 j j0 i i0
|
|
|
146 gcdsym1 zero zero zero zero = refl
|
|
|
147 gcdsym1 zero zero zero (suc j0) = refl
|
|
|
148 gcdsym1 zero (suc i0) zero zero = refl
|
|
|
149 gcdsym1 zero (suc i0) zero (suc j0) = gcdsym2 (suc i0) (suc j0)
|
|
|
150 gcdsym1 zero zero (suc zero) j0 = refl
|
|
|
151 gcdsym1 zero zero (suc (suc j)) j0 = refl
|
|
|
152 gcdsym1 zero (suc i0) (suc zero) j0 = refl
|
|
|
153 gcdsym1 zero (suc i0) (suc (suc j)) j0 = gcdsym1 i0 (suc i0) (suc j) (suc (suc j))
|
|
|
154 gcdsym1 (suc zero) i0 zero j0 = refl
|
|
|
155 gcdsym1 (suc (suc i)) i0 zero zero = refl
|
|
|
156 gcdsym1 (suc (suc i)) i0 zero (suc j0) = gcdsym1 (suc i) (suc (suc i))j0 (suc j0)
|
|
|
157 gcdsym1 (suc i) i0 (suc j) j0 = subst₂ (λ j k → j ≡ k ) (sym (gcd22 i _ _ _)) (sym (gcd22 j _ _ _)) (gcdsym1 i i0 j j0 )
|
|
|
158
|
|
146
|
159 gcdsym : { n m : ℕ} → gcd n m ≡ gcd m n
|
|
147
|
160 gcdsym {n} {m} = gcdsym1 n n m m
|
|
146
|
161
|
|
152
|
162 gcd11 : ( i : ℕ ) → gcd i i ≡ i
|
|
|
163 gcd11 i = gcdmm i i
|
|
|
164
|
|
|
165 gcd2 : ( i j : ℕ ) → gcd (i + j) j ≡ gcd i j
|
|
153
|
166 gcd2 i j = gcd200 i i j j where
|
|
|
167 gcd202 : (i j1 : ℕ) → (i + suc j1) ≡ suc (i + j1)
|
|
|
168 gcd202 zero j1 = refl
|
|
|
169 gcd202 (suc i) j1 = cong suc (gcd202 i j1)
|
|
|
170 gcd201 : (i i0 j j0 j1 : ℕ) → gcd1 (i + j1) (i0 + suc j) j1 j0 ≡ gcd1 i (i0 + suc j) zero j0
|
|
|
171 gcd201 i i0 j j0 zero = subst (λ k → gcd1 k (i0 + suc j) zero j0 ≡ gcd1 i (i0 + suc j) zero j0 ) (+-comm zero i) refl
|
|
|
172 gcd201 i i0 j j0 (suc j1) = begin
|
|
|
173 gcd1 (i + suc j1) (i0 + suc j) (suc j1) j0 ≡⟨ cong (λ k → gcd1 k (i0 + suc j) (suc j1) j0 ) (gcd202 i j1) ⟩
|
|
|
174 gcd1 (suc (i + j1)) (i0 + suc j) (suc j1) j0 ≡⟨ gcd22 (i + j1) (i0 + suc j) j1 j0 ⟩
|
|
|
175 gcd1 (i + j1) (i0 + suc j) j1 j0 ≡⟨ gcd201 i i0 j j0 j1 ⟩
|
|
|
176 gcd1 i (i0 + suc j) zero j0 ∎ where open ≡-Reasoning
|
|
|
177 gcd200 : (i i0 j j0 : ℕ) → gcd1 (i + j) (i0 + j) j j0 ≡ gcd1 i i j0 j0
|
|
|
178 -- gcd200 i i0 zero j0 = subst₂ (λ m k → gcd1 m k zero j0 ≡ gcd1 i i0 zero j0 ) (+-comm zero i) (+-comm zero i0) refl
|
|
|
179 gcd200 i i0 zero j0 = {!!}
|
|
|
180 gcd200 (suc (suc i)) i0 (suc j) (suc j0) = gcd201 (suc (suc i)) i0 j (suc j0) (suc j)
|
|
|
181 gcd200 zero zero (suc zero) j0 = {!!}
|
|
|
182 gcd200 zero zero (suc (suc j)) j0 = {!!}
|
|
|
183 gcd200 zero (suc i0) (suc j) j0 = {!!}
|
|
|
184 gcd200 (suc zero) i0 (suc j) j0 = {!!}
|
|
|
185 gcd200 (suc (suc i)) i0 (suc j) zero = ?
|
|
152
|
186
|
|
142
|
187 gcd24 : { n m k : ℕ} → n > 1 → m > 1 → k > 1 → gcd n k ≡ k → gcd m k ≡ k → ¬ ( gcd n m ≡ 1 )
|
|
|
188 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
|
|
147
|
189 gcd23 : {i0 j0 : ℕ } → 1 < i0 → 1 < j0 → 1 < gcd1 zero i0 zero j0
|
|
|
190 gcd23 {i0} {j0} 1<i 1<j with <-cmp i0 j0
|
|
|
191 ... | tri< a ¬b ¬c = 1<j
|
|
|
192 ... | tri≈ ¬a refl ¬c = 1<i
|
|
|
193 ... | tri> ¬a ¬b c = 1<i
|
|
143
|
194 1<ss : {j : ℕ} → 1 < suc (suc j)
|
|
|
195 1<ss = s≤s (s≤s z≤n)
|
|
142
|
196 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 → ⊥
|
|
147
|
197 gcd21 zero i0 zero j0 o o0 1<i 1<j 1<o refl gm gnm = nat-≡< (sym gnm) (gcd23 1<i 1<j)
|
|
|
198 gcd21 zero i0 (suc j) j0 zero o0 1<i 1<j 1<o refl gm gnm = gcd25 i0 o0 j j0 1<o 1<i 1<k gm (subst (λ k → k ≡ 1) (gcdsym1 zero _ (suc j) _) gnm) where
|
|
148
|
199 -- gcd1 (suc j) (suc (suc j)) (suc o0) (suc (suc o0)) ≡ suc (suc i0) , gcd1 (suc j) (suc (suc j)) (suc i0) (suc (suc i0)) ≡ 1
|
|
147
|
200 gcd25 : (i0 o0 j j0 : ℕ) → 1 < o0 → 1 < i0
|
|
|
201 → 1 < gcd1 zero i0 zero o0
|
|
|
202 → ( gm : gcd1 (suc j) j0 zero o0 ≡ gcd1 zero i0 zero o0 ) → (gnm : gcd1 (suc j) j0 zero i0 ≡ 1) → ⊥
|
|
|
203 gcd25 i0 o0 zero j0 1<o 1<i 1<k gm refl with <-cmp i0 o0
|
|
|
204 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< gm 1<o )
|
|
|
205 ... | tri≈ ¬a refl ¬c = ⊥-elim ( nat-≡< gm 1<o )
|
|
|
206 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< gm 1<i )
|
|
|
207 -- gm : gcd1 (suc j) (suc (suc j)) (suc o0) (suc (suc o0)) ≡ (gcd1 zero (suc i0) zero (suc (suc o0))
|
|
|
208 -- gcd1 j (suc (suc j)) o0 (suc (suc o0))
|
|
|
209 -- gnm : gcd1 (suc j) (suc (suc j)) i0 (suc i0) ≡ 1
|
|
148
|
210 gcd25 i0 (suc zero) (suc j) j0 1<o 1<i 1<k gm gnm = {!!} -- ⊥-elim ( nat-≤> (subst (λ k → k ≤ 1 ) gm (gcd27 (suc j) (suc (suc j)))) 1<k )
|
|
147
|
211 gcd25 (suc zero) (suc (suc o0)) (suc j) j0 1<o 1<i 1<k gm gnm = {!!}
|
|
148
|
212 -- (suc (suc i0)) > (suc (suc o0)) → gm = gnm → (suc (suc i0)) ≡ 1
|
|
|
213 -- (suc (suc i0)) < (suc (suc o0)) → ? gcd1 (suc j) (suc (suc j)) (suc o0) (suc (suc o0)) ≡ (suc (suc o0))
|
|
|
214 -- gcd1 (suc j) (suc (suc j)) (suc i0) (suc (suc i0)) ≡ 1
|
|
|
215 gcd25 (suc (suc i0)) (suc (suc o0)) (suc j) j0 1<o 1<i 1<k gm gnm with <-cmp (suc (suc i0)) (suc (suc o0))
|
|
|
216 ... | tri< a ¬b ¬c = {!!}
|
|
|
217 ... | tri≈ ¬a b ¬c = {!!}
|
|
|
218 ... | tri> ¬a ¬b c = gcd26 {!!} {!!} {!!} {!!} {!!} {!!} {!!}
|
|
146
|
219 gcd21 zero i0 (suc j) j0 (suc zero) o0 1<i 1<j 1<o refl gm gnm = nat-<≡ 1<k
|
|
|
220 gcd21 zero (suc i0) (suc j) j0 (suc (suc o)) o0 1<i 1<j 1<o gn gm gnm =
|
|
147
|
221 gcd21 i0 {!!} (suc j) j0 (suc o) (suc (suc o)) 1<i 1<j {!!} gn {!!} {!!}
|
|
145
|
222 gcd21 (suc i) i0 zero j0 o o0 1<i 1<j 1<o gn gm gnm = {!!}
|
|
142
|
223 gcd21 (suc i) i0 (suc j) j0 zero o0 1<i 1<j 1<o gn gm gnm = {!!}
|
|
|
224 gcd21 (suc i) i0 (suc j) j0 (suc o) o0 1<i 1<j 1<o gn gm gnm =
|
|
|
225 gcd21 i i0 j j0 o o0 1<i 1<j 1<o (subst (λ m → m ≡ k) (gcd22 i i0 _ _ ) gn)
|
|
|
226 (subst (λ m → m ≡ k) (gcd22 j j0 _ _ ) gm) (subst (λ k → k ≡ 1) (gcd22 i i0 _ _ ) gnm)
|
|
141
|
227
|
|
|
228 record Even (i : ℕ) : Set where
|
|
|
229 field
|
|
|
230 j : ℕ
|
|
|
231 is-twice : i ≡ 2 * j
|
|
|
232
|
|
|
233 e2 : (i : ℕ) → even i → Even i
|
|
|
234 e2 zero en = record { j = 0 ; is-twice = refl }
|
|
|
235 e2 (suc (suc i)) en = record { j = suc (Even.j (e2 i en )) ; is-twice = e21 } where
|
|
|
236 e21 : suc (suc i) ≡ 2 * suc (Even.j (e2 i en))
|
|
|
237 e21 = begin
|
|
|
238 suc (suc i) ≡⟨ cong (λ k → suc (suc k)) (Even.is-twice (e2 i en)) ⟩
|
|
|
239 suc (suc (2 * Even.j (e2 i en))) ≡⟨ sym (*-distribˡ-+ 2 1 _) ⟩
|
|
|
240 2 * suc (Even.j (e2 i en)) ∎ where open ≡-Reasoning
|
|
|
241
|
|
|
242 record Odd (i : ℕ) : Set where
|
|
|
243 field
|
|
|
244 j : ℕ
|
|
|
245 is-twice : i ≡ suc (2 * j )
|
|
57
|
246
|
|
141
|
247 odd2 : (i : ℕ) → ¬ even i → even (suc i)
|
|
|
248 odd2 zero ne = ⊥-elim ( ne tt )
|
|
|
249 odd2 (suc zero) ne = tt
|
|
|
250 odd2 (suc (suc i)) ne = odd2 i ne
|
|
|
251
|
|
|
252 odd3 : (i : ℕ) → ¬ even i → Odd i
|
|
|
253 odd3 zero ne = ⊥-elim ( ne tt )
|
|
|
254 odd3 (suc zero) ne = record { j = 0 ; is-twice = refl }
|
|
|
255 odd3 (suc (suc i)) ne = record { j = Even.j (e2 (suc i) (odd2 i ne)) ; is-twice = odd31 } where
|
|
|
256 odd31 : suc (suc i) ≡ suc (2 * Even.j (e2 (suc i) (odd2 i ne)))
|
|
|
257 odd31 = begin
|
|
|
258 suc (suc i) ≡⟨ cong suc (Even.is-twice (e2 (suc i) (odd2 i ne))) ⟩
|
|
|
259 suc (2 * (Even.j (e2 (suc i) (odd2 i ne)))) ∎ where open ≡-Reasoning
|
|
|
260
|
|
|
261 odd4 : (i : ℕ) → even i → ¬ even ( suc i )
|
|
|
262 odd4 (suc (suc i)) en en1 = odd4 i en en1
|
|
|
263
|
|
|
264 even^2 : {n : ℕ} → even ( n * n ) → even n
|
|
|
265 even^2 {n} en with even? n
|
|
|
266 ... | yes y = y
|
|
|
267 ... | 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
|
|
|
268 m : ℕ
|
|
|
269 m = Odd.j ( odd3 n ne )
|
|
|
270 ee3 : even (2 * m)
|
|
|
271 ee3 = subst (λ k → even k ) (*-comm m 2) (n*even {m} {2} tt )
|
|
|
272 ee4 : even ((2 * m) * suc (2 * m))
|
|
|
273 ee4 = even*n {(2 * m)} {suc (2 * m)} (even*n {2} {m} tt )
|
|
|
274 ee2 : n * n ≡ suc (2 * m) + ((2 * m) * (suc (2 * m) ))
|
|
|
275 ee2 = begin n * n ≡⟨ cong ( λ k → k * k) (Odd.is-twice (odd3 n ne)) ⟩
|
|
|
276 suc (2 * m) * suc (2 * m) ≡⟨ *-distribʳ-+ (suc (2 * m)) 1 ((2 * m) ) ⟩
|
|
|
277 (1 * suc (2 * m)) + 2 * m * suc (2 * m) ≡⟨ cong (λ k → k + 2 * m * suc (2 * m)) (begin
|
|
|
278 suc m + 1 * m + 0 * (suc m + 1 * m ) ≡⟨ +-comm (suc m + 1 * m) 0 ⟩
|
|
|
279 suc m + 1 * m ≡⟨⟩
|
|
|
280 suc (2 * m)
|
|
|
281 ∎) ⟩ suc (2 * m) + 2 * m * suc (2 * m) ∎ where open ≡-Reasoning
|
|
57
|
282
|
|
141
|
283 open import nat
|
|
|
284
|
|
|
285 e3 : {i j : ℕ } → 2 * i ≡ 2 * j → i ≡ j
|
|
|
286 e3 {zero} {zero} refl = refl
|
|
|
287 e3 {suc x} {suc y} eq with <-cmp x y
|
|
|
288 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< eq (s≤s (<-trans (<-plus a) (<-plus-0 (s≤s (<-plus a ))))))
|
|
|
289 ... | tri≈ ¬a b ¬c = cong suc b
|
|
|
290 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym eq) (s≤s (<-trans (<-plus c) (<-plus-0 (s≤s (<-plus c ))))))
|
|
|
291
|
