Mercurial > hg > Members > atton > delta_monad
comparison agda/nat.agda @ 77:4b16b485a4b2
Split nat definition
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 01 Dec 2014 11:58:35 +0900 |
parents | |
children | a271f3ff1922 |
comparison
equal
deleted
inserted
replaced
76:c7076f9bbaed | 77:4b16b485a4b2 |
---|---|
1 open import Relation.Binary.PropositionalEquality | |
2 open ≡-Reasoning | |
3 | |
4 module nat where | |
5 | |
6 data Nat : Set where | |
7 O : Nat | |
8 S : Nat -> Nat | |
9 | |
10 _+_ : Nat -> Nat -> Nat | |
11 O + n = n | |
12 (S m) + n = S (m + n) | |
13 | |
14 nat-add-right-zero : (n : Nat) -> n ≡ n + O | |
15 nat-add-right-zero O = refl | |
16 nat-add-right-zero (S n) = begin | |
17 S n ≡⟨ cong (\n -> S n) (nat-add-right-zero n) ⟩ | |
18 S (n + O) ≡⟨ refl ⟩ | |
19 S n + O | |
20 ∎ | |
21 | |
22 nat-right-increment : (n m : Nat) -> n + S m ≡ S (n + m) | |
23 nat-right-increment O m = refl | |
24 nat-right-increment (S n) m = cong S (nat-right-increment n m) | |
25 | |
26 nat-add-sym : (n m : Nat) -> n + m ≡ m + n | |
27 nat-add-sym O O = refl | |
28 nat-add-sym O (S m) = cong S (nat-add-sym O m) | |
29 nat-add-sym (S n) O = cong S (nat-add-sym n O) | |
30 nat-add-sym (S n) (S m) = begin | |
31 S n + S m ≡⟨ refl ⟩ | |
32 S (n + S m) ≡⟨ cong S (nat-add-sym n (S m)) ⟩ | |
33 S ((S m) + n) ≡⟨ sym (nat-right-increment (S m) n) ⟩ | |
34 S m + S n ∎ |