|
159
|
1 module even where
|
|
57
|
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
|
|
149
|
10 open import nat
|
|
151
|
11 open import logic
|
|
57
|
12
|
|
|
13 even : (n : ℕ ) → Set
|
|
141
|
14 even zero = ⊤
|
|
|
15 even (suc zero) = ⊥
|
|
|
16 even (suc (suc n)) = even n
|
|
57
|
17
|
|
|
18 even? : (n : ℕ ) → Dec ( even n )
|
|
141
|
19 even? zero = yes tt
|
|
|
20 even? (suc zero) = no (λ ())
|
|
|
21 even? (suc (suc n)) = even? n
|
|
|
22
|
|
|
23 n+even : {n m : ℕ } → even n → even m → even ( n + m )
|
|
|
24 n+even {zero} {zero} tt tt = tt
|
|
|
25 n+even {zero} {suc m} tt em = em
|
|
|
26 n+even {suc (suc n)} {m} en em = n+even {n} {m} en em
|
|
|
27
|
|
|
28 n*even : {m n : ℕ } → even n → even ( m * n )
|
|
|
29 n*even {zero} {n} en = tt
|
|
|
30 n*even {suc m} {n} en = n+even {n} {m * n} en (n*even {m} {n} en)
|
|
|
31
|
|
|
32 even*n : {n m : ℕ } → even n → even ( n * m )
|
|
|
33 even*n {n} {m} en = subst even (*-comm m n) (n*even {m} {n} en)
|
|
|
34
|
|
|
35
|
|
|
36 record Even (i : ℕ) : Set where
|
|
|
37 field
|
|
|
38 j : ℕ
|
|
|
39 is-twice : i ≡ 2 * j
|
|
|
40
|
|
|
41 e2 : (i : ℕ) → even i → Even i
|
|
|
42 e2 zero en = record { j = 0 ; is-twice = refl }
|
|
|
43 e2 (suc (suc i)) en = record { j = suc (Even.j (e2 i en )) ; is-twice = e21 } where
|
|
|
44 e21 : suc (suc i) ≡ 2 * suc (Even.j (e2 i en))
|
|
|
45 e21 = begin
|
|
|
46 suc (suc i) ≡⟨ cong (λ k → suc (suc k)) (Even.is-twice (e2 i en)) ⟩
|
|
|
47 suc (suc (2 * Even.j (e2 i en))) ≡⟨ sym (*-distribˡ-+ 2 1 _) ⟩
|
|
|
48 2 * suc (Even.j (e2 i en)) ∎ where open ≡-Reasoning
|
|
|
49
|
|
|
50 record Odd (i : ℕ) : Set where
|
|
|
51 field
|
|
|
52 j : ℕ
|
|
|
53 is-twice : i ≡ suc (2 * j )
|
|
57
|
54
|
|
141
|
55 odd2 : (i : ℕ) → ¬ even i → even (suc i)
|
|
|
56 odd2 zero ne = ⊥-elim ( ne tt )
|
|
|
57 odd2 (suc zero) ne = tt
|
|
|
58 odd2 (suc (suc i)) ne = odd2 i ne
|
|
|
59
|
|
|
60 odd3 : (i : ℕ) → ¬ even i → Odd i
|
|
|
61 odd3 zero ne = ⊥-elim ( ne tt )
|
|
|
62 odd3 (suc zero) ne = record { j = 0 ; is-twice = refl }
|
|
|
63 odd3 (suc (suc i)) ne = record { j = Even.j (e2 (suc i) (odd2 i ne)) ; is-twice = odd31 } where
|
|
|
64 odd31 : suc (suc i) ≡ suc (2 * Even.j (e2 (suc i) (odd2 i ne)))
|
|
|
65 odd31 = begin
|
|
|
66 suc (suc i) ≡⟨ cong suc (Even.is-twice (e2 (suc i) (odd2 i ne))) ⟩
|
|
|
67 suc (2 * (Even.j (e2 (suc i) (odd2 i ne)))) ∎ where open ≡-Reasoning
|
|
|
68
|
|
|
69 odd4 : (i : ℕ) → even i → ¬ even ( suc i )
|
|
|
70 odd4 (suc (suc i)) en en1 = odd4 i en en1
|
|
|
71
|
