Mercurial > hg > Members > atton > delta_monad

annotate agda/nat.agda @ 87:6789c65a75bc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Split functor-proofs into delta.functor
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 19 Jan 2015 11:00:34 +0900
parents 4b16b485a4b2
children a271f3ff1922
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
77
4b16b485a4b2 Split nat definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import Relation.Binary.PropositionalEquality
4b16b485a4b2 Split nat definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 open ≡-Reasoning
4b16b485a4b2 Split nat definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3
4b16b485a4b2 Split nat definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 module nat where
4b16b485a4b2 Split nat definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
4b16b485a4b2 Split nat definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 data Nat : Set where
4b16b485a4b2 Split nat definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 O : Nat
4b16b485a4b2 Split nat definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 S : Nat -> Nat
4b16b485a4b2 Split nat definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9
4b16b485a4b2 Split nat definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 _+_ : Nat -> Nat -> Nat
4b16b485a4b2 Split nat definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 O + n = n
4b16b485a4b2 Split nat definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 (S m) + n = S (m + n)
4b16b485a4b2 Split nat definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
4b16b485a4b2 Split nat definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 nat-add-right-zero : (n : Nat) -> n ≡ n + O
4b16b485a4b2 Split nat definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 nat-add-right-zero O = refl
4b16b485a4b2 Split nat definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 nat-add-right-zero (S n) = begin
4b16b485a4b2 Split nat definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 S n ≡⟨ cong (\n -> S n) (nat-add-right-zero n) ⟩
4b16b485a4b2 Split nat definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 S (n + O) ≡⟨ refl ⟩
4b16b485a4b2 Split nat definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 S n + O
4b16b485a4b2 Split nat definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 ∎
4b16b485a4b2 Split nat definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21
4b16b485a4b2 Split nat definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 nat-right-increment : (n m : Nat) -> n + S m ≡ S (n + m)
4b16b485a4b2 Split nat definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 nat-right-increment O m = refl
4b16b485a4b2 Split nat definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 nat-right-increment (S n) m = cong S (nat-right-increment n m)
4b16b485a4b2 Split nat definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25
4b16b485a4b2 Split nat definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 nat-add-sym : (n m : Nat) -> n + m ≡ m + n
4b16b485a4b2 Split nat definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 nat-add-sym O O = refl
4b16b485a4b2 Split nat definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 nat-add-sym O (S m) = cong S (nat-add-sym O m)
4b16b485a4b2 Split nat definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 nat-add-sym (S n) O = cong S (nat-add-sym n O)
4b16b485a4b2 Split nat definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 nat-add-sym (S n) (S m) = begin
4b16b485a4b2 Split nat definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 S n + S m ≡⟨ refl ⟩
4b16b485a4b2 Split nat definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 S (n + S m) ≡⟨ cong S (nat-add-sym n (S m)) ⟩
4b16b485a4b2 Split nat definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 S ((S m) + n) ≡⟨ sym (nat-right-increment (S m) n) ⟩
4b16b485a4b2 Split nat definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 S m + S n ∎