--- a/slide.md	Thu May 22 20:30:05 2014 +0900
+++ b/slide.md	Fri May 23 14:13:40 2014 +0900
@@ -48,33 +48,49 @@
 
 # Agda における自然数の定義
 * data 型を使います
-    * data Int : Set where
-    *   Zero : Int
-    *   Succ : Int -> Int
-* Zero は Int, Succ は Int を受けとって Int を返す、と読めます
+
+```
+    data Int : Set where
+      O : Int
+      S : Int -> Int
+```
+* O は Int, S は Int を受けとって Int を返す、と読めます
 * Set は組込みで存在する型です。「成り立つ」といった感じです。
 
 
 # 自然数の例
-* 0 = Zero
-* 1 = Succ Zero
-* 2 = Succ (Succ Zero)
-* 5 = Succ (Succ (Succ (Succ (Succ Zero))))
+* 0 = O
+* 1 = S O
+* 2 = S (S O)
+* 5 = S (S (S (S (S O))))
 
 
 # 自然数に対する演算の定義
-* a と b の加算 : a にかかっている Succ の分だけ Succ を b にかける
-* a と b の加算 : a にかかっている Succ の分だけ b を 0 に加算する
+* x と y の加算 : x にかかっている S の分だけ S を b に適用する
+* x と y の加算 : x にかかっている S の分だけ y を 0 に加算する
 
 * Agda tips : 不明な項を ? と書くこともできます
 * その状態で C-c C-l するとその項の型が分かります
 
 
+# Agda における自然数に対する演算の定義
+```
+    infixl 30 _+_
+    _+_ : Int -> Int -> Int
+    x + O     = x
+    x + (S y) = S (x + y)
+```
+
+* Agda tips : C-c C-n すると式を評価することができます
+* (S O) + (S (S O)) などしてみましょう
+
+
 # Agda における関数定義のSyntax
 * Agda において、関数は
   * 関数名                        : 型
   * 関数名 <スペース区切りで引数> = 関数の定義や値
 * のように定義します
+* 中置関数は _ で挟みます
 
 
 # Agda における引数を持つ関数の型の表記法
@@ -86,32 +102,35 @@
 * 右結合のため、A を受けとって ((A -> B) -> B) を返す、とも読めます
 
 
-# Agda における自然数に対する演算の定義
-TODO: 書いておく
-
-* Agda tips : C-c C-n すると式を評価することができます
-* add (Succ Zero) (Succ (Succ Zero)) などしてみましょう
-
-
 # パターンマッチ
 * Agda においてはデータ型は引数で分解することができます
 * ある型に続している値が、どのコンストラクタにおいて構成されたかをパターンで示せます
   * double : Int -> Int
   * double O     = O
-  * double (S n) = S (S (double n))
+  * double (S x) = S (S (double x))
 * 関数名 (引数のパターン) = 定義
 
 
+# もういちど : 自然数に対する演算の定義
+```
+    infixl 30 _+_
+    _+_ : Int -> Int -> Int
+    x + O     = x
+    x + (S y) = S (x + y)
+```
+* 中置、関数、パターンマッチが使われています
+* infixl は左結合を意味します。数値は結合強度です
+
+
 # これから証明していきたいこと
-* 加法の交換法則 : (a + b) = (b + a)
-* 加法の結合法則 : (a + b) + c = a + (b + c)
+* 加法の交換法則 : (x + y) = (y + x)
+* 加法の結合法則 : (x + y) + z = x + (y + z) <- 目標ライン
+
+* 乗法の交換法則 : (x * y) = (y * x)
+* 乗法の結合法則 : (x * y) * z = x * (y * z)
 
 * 分配法則       : x * (y + z) = (x * y) + (x * z)
 
-* 乗法の交換法則 : (a * b) = (b * a)
-* 乗法の結合法則 : (a * b) * c = a * (b * c)
-
-
 # '等しい' ということ
 * '等しい'という型 _ ≡ _ を定義する
   * refl  : x ≡ x
@@ -119,6 +138,7 @@
   * cong  : (f : A → B) -> x ≡ y → f x ≡ f y
   * trans : x ≡ y -> y ≡ z -> y ≡ z
 * defined : Relation.Binary.PropositionalEquality in Standard Library
+* Agda tips : 記号は \ の後に文字列を入れると出てきます。 '≡' は "\ =="
 
 
 # '同じもの'とは
@@ -132,32 +152,128 @@
 
 # 交換法則を型として定義する
 * ≡を用いて
-  * (n : Int) -> (m : Int) -> n + m ≡ m + n
+  * (x : Int) -> (y : Int) -> x + y ≡ y + x
 * 引数は (名前 : 型) として名前付けできます
 
 
-# 等式変形
-TODO: trans による等式変形
+# 交換法則を証明していく
+```
+sum-sym : (x y : Int)  -> x + y ≡ y + x
+sum-sym    O     O  = refl
+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) = ?
+```
+
+# trans による等式変形
+* sum-sym (S x) (S y) の時は1つの関数のみで等しさを証明できない
+* 等しさを保ったまま式を変形していくことが必要になります
+
+* sum-sym (S x) (S y) = trans (a ≡ b) (b ≡ c)
+  * trans (refl) ?
+  * trans (trans refl (cong S (left-add-one x y)) ?
 
 
 # ≡-reasoning による等式変形
-TODO: reasoning による等式変形
+* trans が何段もネストしていくと分かりづらい
+* ≡-reasoning という等式変形の拡張構文が Standard Library にあります
+
+```
+   begin
+     変換前の式
+       ≡⟨ 変換する関数 ⟩
+     変換後の式
+   ∎
+```
+
+
+# ≡-reasoning による最初の定義
+
+```
+sum-sym (S x) (S y) = begin
+    (S x) + (S y)
+  ≡⟨ ? ⟩
+    (S y) + (S x)
+  ∎
+```
+
+
+# 交換法則の証明 : + の定義による変形
+* 上から + の定義により変形
+
+```
+sum-sym (S x) (S y) = begin
+    (S x) + (S y)
+  ≡⟨ refl ⟩
+    S (S x + y)
+  ≡⟨ ? ⟩
+    (S y) + (S x)
+  ∎
+```
+
+
+# cong と sum-sym を使って交換
+* S が1つ取れたのでsum-symで交換できる
+* sum-sym で交換した後に cong で S がかかる
+
+```
+    S ((S x) + y)
+  ≡⟨ cong S (sum-sym (S x) y) ⟩
+    S ((y + (S x)))
+```
 
 
-# 加法の交換法則 : (a + b) = (b + a)
-TODO: 書いとく
+# 交換法則の証明 : 加法の時に左側からSを移動させることができない
+
+* 加法の定義は
+  * x + (S y) = S (x + y)
+* left-operand から S を取る方法が無い
+  * S (y + S x) ≡ S y + S x
+* にあてはまるものを入れてくれ、と出てきている
+
 
-# 加法の結合法則 : (a + b) + c = a + (b + c)
-TODO: 書いとく
+# left-operand からSを操作する証明を定義
+```
+  left-increment : (x y : Int) -> (S x) + y ≡ S (x + y)
+  left-increment x y = ?
+```
+
+* Agda tips : goal の上で C-c C-c で引数のパターン分け
+* Agda tips : goal の上で C-c C-a で証明を探してくれる
+
+
+# left-operand からSを移動させる
+* left-increment は (S x) + y ≡ S (x + y) なので逆にしないと使えない
 
-# 分配法則       : x * (y + z) = (x * y) + (x * z)
-TODO: 書いとく(うしろで良いかな)
+```
+    ...
+    S ((S x) + y)
+      ≡⟨ sym (left-increment x (S y)) ⟩
+    (S y) + (S x)
+  ∎
+```
+
 
-# 乗法の交換法則 : (a * b) = (b * a)
-TODO: 書いとく(うしろで良いかな)
+# 加法の交換法則 : (x + y) = (y + x)
+```
+sum-sym (S x) (S y) = begin
+    (S x) + (S y)
+  ≡⟨ refl ⟩
+    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)
+  ∎
+```
 
-# 乗法の結合法則 : (a * b) * c = a * (b * c)
-TODO: 書いとく(うしろで良いかな)
+
+# 加法の結合法則 : (x + y) + z = x + (y + z)
+* 次に結合法則を証明します
+* 手順は同じです
+  * ≡ で証明したい式を定義
+  * 定義に証明を書く
+  * 必要ならば等式を変形していく
 
 
 # Agda による証明方法のまとめ
@@ -168,4 +284,38 @@
 * C-c C-l により型のチェックが成功すれば証明終了
 
 
+# 乗法の定義
+```
+infixl 40 _*_
+_*_ : Int -> Int -> Int
+n *    O  = O
+n * (S O) = n
+n * (S m) = n + (n * m)
+```
+
+* _+_ よりも結合強度を上げる必要がある
+
+
+# 乗法の交換法則 : (a * b) = (b * a)
+```
+mult-sym : (n m : Int) -> n * m ≡ m * n
+```
+
+途中で
+
+```
+(n m : Int) -> (S n) * m ≡ m + (n * m)
+```
+
+が必要になる
+
+
+# 乗法の結合法則 : (a * b) * c = a * (b * c)
+TODO: まだ。書いとく(うしろで良いかな)
+
+
+# 分配法則  : x * (y + z) = (x * y) + (x * z)
+TODO: まだ。書いとく(うしろで良いかな)
+
+
 <!-- vim: set filetype=markdown.slide: -->