|
57
|
1 module root2 where
|
|
|
2
|
|
|
3 open import Data.Nat
|
|
|
4 open import Data.Empty
|
|
|
5 open import Relation.Nullary
|
|
|
6 open import Relation.Binary.PropositionalEquality
|
|
|
7 open import Data.Nat.DivMod
|
|
|
8
|
|
|
9 even : (n : ℕ ) → Set
|
|
|
10 even n = n % 2 ≡ 0
|
|
|
11
|
|
|
12 even? : (n : ℕ ) → Dec ( even n )
|
|
|
13 even? n with n % 2
|
|
|
14 even? n | zero = yes refl
|
|
|
15 even? n | suc k = no ( λ () )
|
|
|
16
|
|
|
17 nn-even : {n : ℕ } → even n → even ( n * n )
|
|
|
18 nn-even {n} eq = {!!}
|
|
|
19
|
|
|
20 2-even : {n : ℕ } → even ( 2 * n )
|
|
|
21 2-even {n} = {!!}
|
|
|
22
|
|
|
23 even-2 : (n : ℕ ) → (n + 2) % 2 ≡ 0 → n % 2 ≡ 0
|
|
|
24 even-2 0 refl = refl
|
|
|
25 even-2 1 ()
|
|
|
26 even-2 (suc (suc n)) eq = {!!} -- trans ([a+n]%n≡a%n (suc (suc n)) _ ) eq -- [a+n]%n≡a%n : ∀ a n → (a + suc n) % suc n ≡ a % suc n
|
|
|
27
|
|
|
28 even-half : (n : ℕ ) → even n → ℕ
|
|
|
29 even-half zero _ = zero
|
|
|
30 even-half (suc (suc n)) ev = {!!} -- 1 + even-half n (subst (λ k → k ≡ 0 ) {!!} {!!} )
|
|
|
31
|
|
|
32 root2-irrational : ( n m : ℕ ) → ¬ ( 2 * n * n ≡ m * m )
|
|
|
33 root2-irrational n m eq = {!!}
|
|
|
34
|
