Mercurial > hg > Members > atton > agda > systemT
view int.agda @ 6:db4c6d435f23
Fix indent
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 21 May 2014 14:55:52 +0900 |
parents | a3cf5cb2b7d3 |
children | f922e687f3a1 |
line wrap: on
line source
open import systemT open import Relation.Binary.PropositionalEquality open ≡-Reasoning module int where _+_ : Int -> Int -> Int n + O = n n + (S m) = S (n + m) left-increment : (n m : Int) -> (S n) + m ≡ S (n + m) left-increment n O = refl left-increment n (S m) = cong S (left-increment n m) double : Int -> Int double O = O double (S n) = S (S (double n)) sum-sym : (n : Int) (m : Int) -> n + m ≡ m + n sum-sym O O = refl sum-sym O (S m) = cong S (sum-sym O m) sum-sym (S n) O = cong S (sum-sym n O) sum-sym (S n) (S m) = begin (S n) + (S m) ≡⟨ refl ⟩ S ((S n) + m) ≡⟨ cong S (left-increment n m)⟩ S (S (n + m)) ≡⟨ cong (\x -> S (S x)) (sum-sym n m) ⟩ S (S (m + n)) ≡⟨ sym (cong S (left-increment m n)) ⟩ S ((S m) + n) ≡⟨ refl ⟩ (S m) + (S n) ∎ sum-assoc : (x y z : Int) -> x + (y + z) ≡ (x + y) + z sum-assoc O O O = refl sum-assoc O O (S z) = cong S (sum-assoc O O z) sum-assoc O (S y) O = refl sum-assoc O (S y) (S z) = cong S (sum-assoc O (S y) z) sum-assoc (S x) O O = refl sum-assoc (S x) O (S z) = cong S (sum-assoc (S x) O z) sum-assoc (S x) (S y) O = refl sum-assoc (S x) (S y) (S z) = cong S (sum-assoc (S x) (S y) z)