--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/agda/even.agda	Mon Jan 04 09:24:11 2021 +0900
@@ -0,0 +1,71 @@
+module even where
+
+open import Data.Nat 
+open import Data.Nat.Properties
+open import Data.Empty
+open import Data.Unit using (⊤ ; tt)
+open import Relation.Nullary
+open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.Definitions
+open import nat
+open import logic
+
+even : (n : ℕ ) → Set
+even zero = ⊤
+even (suc zero) = ⊥
+even (suc (suc n)) = even n
+
+even? : (n : ℕ ) → Dec ( even n )
+even? zero = yes tt
+even? (suc zero) = no (λ ())
+even? (suc (suc n)) = even? n
+
+n+even : {n m : ℕ } → even n → even m  → even ( n + m )
+n+even {zero} {zero} tt tt = tt
+n+even {zero} {suc m} tt em = em
+n+even {suc (suc n)} {m} en em = n+even {n} {m} en em
+
+n*even : {m n : ℕ } → even n → even ( m * n )
+n*even {zero} {n} en = tt
+n*even {suc m} {n} en = n+even {n} {m * n} en (n*even {m} {n} en) 
+
+even*n : {n m : ℕ } → even n → even ( n * m )
+even*n {n} {m} en = subst even (*-comm m n) (n*even {m} {n} en)
+
+
+record Even (i : ℕ) : Set where
+  field
+     j : ℕ
+     is-twice : i ≡ 2 * j
+
+e2 : (i : ℕ) → even i → Even i
+e2 zero en = record { j = 0 ; is-twice = refl }
+e2 (suc (suc i)) en = record { j = suc (Even.j (e2 i en )) ; is-twice = e21 } where
+   e21 : suc (suc i) ≡ 2 * suc (Even.j (e2 i en))
+   e21 = begin
+    suc (suc i)  ≡⟨ cong (λ k → suc (suc k)) (Even.is-twice (e2 i en))  ⟩
+    suc (suc (2 * Even.j (e2 i en)))  ≡⟨ sym (*-distribˡ-+ 2 1 _) ⟩
+    2 * suc (Even.j (e2 i en))      ∎ where open ≡-Reasoning
+
+record Odd (i : ℕ) : Set where
+  field
+     j : ℕ
+     is-twice : i ≡ suc (2 * j )
+
+odd2 : (i : ℕ) → ¬ even i → even (suc i) 
+odd2 zero ne = ⊥-elim ( ne tt )
+odd2 (suc zero) ne = tt
+odd2 (suc (suc i)) ne = odd2 i ne 
+
+odd3 : (i : ℕ) → ¬ even i →  Odd i
+odd3 zero ne = ⊥-elim ( ne tt )
+odd3 (suc zero) ne = record { j = 0 ; is-twice = refl }
+odd3 (suc (suc i))  ne = record { j = Even.j (e2 (suc i) (odd2 i ne)) ; is-twice = odd31 } where
+  odd31 : suc (suc i) ≡ suc (2 * Even.j (e2 (suc i) (odd2 i ne)))
+  odd31 = begin
+    suc (suc i) ≡⟨  cong suc (Even.is-twice (e2 (suc i) (odd2 i ne)))  ⟩
+    suc (2 * (Even.j (e2 (suc i) (odd2 i ne))))      ∎ where open ≡-Reasoning
+
+odd4 : (i : ℕ) → even i → ¬ even ( suc i )
+odd4 (suc (suc i)) en en1 = odd4 i en en1 
+