### view int.agda @ 5:a3cf5cb2b7d3

Auto proof sum-assoc
author Yasutaka Higa Wed, 21 May 2014 14:52:44 +0900 6b1230883bfa db4c6d435f23
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)
```