Mercurial > hg > Members > atton > agda > systemT
annotate int.agda @ 5:a3cf5cb2b7d3
Auto proof sum-assoc
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 21 May 2014 14:52:44 +0900 |
parents | 6b1230883bfa |
children | db4c6d435f23 |
rev | line source |
---|---|
3 | 1 open import systemT |
2 open import Relation.Binary.PropositionalEquality | |
3 open ≡-Reasoning | |
4 | |
5 module int where | |
6 | |
7 _+_ : Int -> Int -> Int | |
8 n + O = n | |
9 n + (S m) = S (n + m) | |
10 | |
4 | 11 left-increment : (n m : Int) -> (S n) + m ≡ S (n + m) |
12 left-increment n O = refl | |
13 left-increment n (S m) = cong S (left-increment n m) | |
3 | 14 |
15 double : Int -> Int | |
16 double O = O | |
17 double (S n) = S (S (double n)) | |
18 | |
19 sum-sym : (n : Int) (m : Int) -> n + m ≡ m + n | |
20 sum-sym O O = refl | |
21 sum-sym O (S m) = cong S (sum-sym O m) | |
22 sum-sym (S n) O = cong S (sum-sym n O) | |
23 sum-sym (S n) (S m) = begin | |
24 (S n) + (S m) | |
25 ≡⟨ refl ⟩ | |
26 S ((S n) + m) | |
4 | 27 ≡⟨ cong S (left-increment n m)⟩ |
3 | 28 S (S (n + m)) |
29 ≡⟨ cong (\x -> S (S x)) (sum-sym n m) ⟩ | |
30 S (S (m + n)) | |
4 | 31 ≡⟨ sym (cong S (left-increment m n)) ⟩ |
3 | 32 S ((S m) + n) |
33 ≡⟨ refl ⟩ | |
34 (S m) + (S n) | |
35 ∎ | |
5
a3cf5cb2b7d3
Auto proof sum-assoc
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
4
diff
changeset
|
36 |
a3cf5cb2b7d3
Auto proof sum-assoc
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
4
diff
changeset
|
37 sum-assoc : (x y z : Int) -> x + (y + z) ≡ (x + y) + z |
a3cf5cb2b7d3
Auto proof sum-assoc
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
4
diff
changeset
|
38 sum-assoc O O O = refl |
a3cf5cb2b7d3
Auto proof sum-assoc
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
4
diff
changeset
|
39 sum-assoc O O (S z) = cong S (sum-assoc O O z) |
a3cf5cb2b7d3
Auto proof sum-assoc
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
4
diff
changeset
|
40 sum-assoc O (S y) O = refl |
a3cf5cb2b7d3
Auto proof sum-assoc
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
4
diff
changeset
|
41 sum-assoc O (S y) (S z) = cong S (sum-assoc O (S y) z) |
a3cf5cb2b7d3
Auto proof sum-assoc
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
4
diff
changeset
|
42 sum-assoc (S x) O O = refl |
a3cf5cb2b7d3
Auto proof sum-assoc
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
4
diff
changeset
|
43 sum-assoc (S x) O (S z) = cong S (sum-assoc (S x) O z) |
a3cf5cb2b7d3
Auto proof sum-assoc
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
4
diff
changeset
|
44 sum-assoc (S x) (S y) O = refl |
a3cf5cb2b7d3
Auto proof sum-assoc
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
4
diff
changeset
|
45 sum-assoc (S x) (S y) (S z) = cong S (sum-assoc (S x) (S y) z) |