### changeset 13:5a81867278afdefaulttip

Imporve proof for sum-sym
author Yasutaka Higa Fri, 23 May 2014 13:53:30 +0900 ce0c3af2c34e int.agda 1 files changed, 10 insertions(+), 14 deletions(-) [+]
line wrap: on
line diff
```--- a/int.agda	Fri May 23 12:10:42 2014 +0900
+++ b/int.agda	Fri May 23 13:53:30 2014 +0900
@@ -26,22 +26,18 @@
left-increment  n    O  = refl
left-increment  n (S m) = cong S (left-increment n m)

-sum-sym : (n : Int) (m : Int) -> n + m ≡ m + n
+sum-sym : (x : Int) (y : Int) -> x + y ≡ y + x
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)
+sum-sym    O  (S y) = cong S (sum-sym O y)
+sum-sym (S x)    O  = cong S (sum-sym x O)
+sum-sym (S x) (S y) = begin
+    (S x) + (S y)
≡⟨ 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)
+    S ((S x) + y)
+  ≡⟨ cong S (sum-sym (S x) y) ⟩
+    S (y + (S x))
+  ≡⟨ (sym (left-increment y (S x))) ⟩
+    (S y) + (S x)
∎

sum-assoc : (x y z : Int) -> x + (y + z) ≡ (x + y) + z```