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