--- a/slide.md	Tue May 20 16:16:30 2014 +0900
+++ b/slide.md	Tue May 20 17:51:45 2014 +0900
@@ -96,16 +96,14 @@
 * とは
 * A を Int, B を String とすると
 * Int と、 Int から String を返す関数があれば String を作れる
-* と読める。つまり関数適用です
+* と読めます。つまり関数適用です
 
 
 # 命題に 'ならば' を含む場合
 * 関数を返せば良いです
 * Agda には lambda があるので
-
-* id : (A -> A)
-* id = \a -> a
-
+  * id : (A -> A)
+  * id = \a -> a
 * といったように書けます。
 * lambda の syntax は \arg -> body です
 
@@ -126,7 +124,78 @@
 
 
 # 自然数の加算の交換法則の証明
+* まずは自然数を定義する
+* ペアノ算術を使います
 
-* TODO: いまから
+
+# ペアノ算術による自然数の定義
+* ゼロは自然数である
+* 自然数の後続数は自然数である
+* TODO: 詳細は今から
+
+
+# ペアノ算術の Agda による定義
+* data type を定義します
+* data Int where
+*   O -> Int
+*   S -> Int -> Int
+* Int は O か、 Int に S をかけたもの、とします
+
+
+# パターンマッチ
+* Agda においてはデータ型を引数で分解することができます
+* ある型に続している値が、どのコンストラクタにおいて構成されたかをパターンで示せます
+* これをパターンマッチと言います
+  * double : Int -> Int
+  * double O     = O
+  * double (S n) = S (S (double n))
+* 関数名 (引数のパターン) = 定義
+
+
+# パターンマッチによる自然数の加算の定義
+* TODO: 今から
+
+
+# '等しさ' ということ
+* 交換法則においては '等しい' ということを証明しなければなりません
+* 等しい、ということも定義する必要があります
+* 命題は型で定義するため、'等しい'、という型が必要です
+
+
+# 等しさをデータ型で定義する
+* == を定義していきます
+* == は型でなくてはならないので
+  * data _==_ : {A : Set} -> A -> A -> Set where
+* となります
+* よって、 hoge と fuga の等しさを証明したい場合は
+* 'hoge == fuga' 、という型を持つ項を関数の定義に書くことが証明になります
+
+
+# '等しい'ということの定義3つ
+* TODO: refl, sym, cong を書きます
+* comment
+  * 個人的には Relation.Binary.PropositionalEquality を open import するよりは自前で定義したい
+  * あと R とか reasoning もできれば使いたくない
+  * というか必要でないなら積極的に削っていかないと時間がおそらく足りない
+  * 時間あまった時用に証明をもう1,2 個くらい書いておきたい
+
+
+# 交換法則を命題として定義する
+* == を用いて
+  * (n : Int) -> (m : Int) -> n + m == m + n
+* 引数は (名前 : 型) として名前付けできます
+
+
+# 交換法則を証明する
+* 交換法則を関数の定義として書いていきます
+* TODO: 今から
+
+
+# Agda による証明方法のまとめ
+* 関数の型を命題、関数の定義を証明とする
+* 命題を扱う必要があるため、型もデータ型として定義できる
+* データ型はパターンマッチにより分解することができる
+* C-c C-l により型のチェックが成功すれば証明終了
+
 
 <!-- vim: set filetype=markdown.slide: -->