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