Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/even.agda @ 183:3fa72793620b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 13 Jun 2021 20:45:17 +0900
parents automaton-in-agda/src/agda/even.agda@567754463810
children af8f630b7e60
comparison
equal deleted inserted replaced
182:567754463810 183:3fa72793620b
1 module even where
2
3 open import Data.Nat
4 open import Data.Nat.Properties
5 open import Data.Empty
6 open import Data.Unit using (⊤ ; tt)
7 open import Relation.Nullary
8 open import Relation.Binary.PropositionalEquality
9 open import Relation.Binary.Definitions
10 open import nat
11 open import logic
12
13 even : (n : ℕ ) → Set
14 even zero = ⊤
15 even (suc zero) = ⊥
16 even (suc (suc n)) = even n
17
18 even? : (n : ℕ ) → Dec ( even n )
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 )
54
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