--- a/slide.md	Fri May 23 17:56:49 2014 +0900
+++ b/slide.md	Fri May 23 20:05:05 2014 +0900
@@ -16,9 +16,9 @@
 * 証明支援系と呼ばれる分野の言語です
   * 他には Coq などがあります
 * Haskell で実装されています
-* dependent type の言語 です
-  * 型を第一級オブジェクトとして扱える
-  * X -> X, f x, a == b のような型を扱うことができます
+* 型が非常に強力で表現力が高いです
+  * 命題や仕様を表す論理式を型として定義することができます
+  * 例えば 1 + 1 = 2 とか
 
 
 # 型と証明との対応 : Curry-Howard Isomorphism
@@ -28,6 +28,15 @@
 * として定義します
 * 関数と命題の対応を Curry-Howard Isomorphism と言います
 
+# 命題と定義, 仕様と実装
+* どうしてプログラムで証明できるかというと
+* (命題 と 定義) は (仕様 と 実装) のように対応します
+  * int chars_to_int(char * chars)
+  * つまり char * から int は作れる、という命題に対応している
+  * 実装は { itoa(chars) }
+* char * から int は作れる、という仕様(型, 命題)は
+* atoi という実装(定義)により証明された
+
 
 # Agda をはじめよう
 * emacs に agda-mode があります
@@ -39,10 +48,10 @@
 
 # 自然数の定義 : Peano Arithmetic
 * 自然数 0 が存在する
-* 任意の自然数 a にはその後続数 suc(a) が存在する
+* 任意の自然数 x にはその後続数 S (x) が存在する
 * 0 より前の自然数は存在しない
 * 異なる自然数は異なる後続数を持つ
-    * a != b のとき suc(a) != suc(b) となる
+    * x != y のとき S(x) != S(y) となる
 * 0 が性質を満たし、a も性質を満たせばその後続数も性質を満たすとき、すべての自然数はその性質を満たす
 
 
@@ -54,8 +63,8 @@
     O : Int
     S : Int -> Int
 ```
-* Int は O か、 Int に S がかかったもののみ
-* Set は組込みで存在する型です。「成り立つ」と考えてもらえれば良いです。
+* Int は O か、 Int に S がかかったもののみで構成される
+* Set は組込みで存在する型で、"成り立つ"と考えてもらうと良いです。
 
 
 # 自然数の例
@@ -66,7 +75,7 @@
 
 
 # 自然数に対する演算の定義
-* x と y の加算 : x にかかっている S の分だけ S を b に適用する
+* x と y の加算 : x にかかっている S の分だけ S を y に適用する
 * x と y の乗算 : x にかかっている S の分だけ y を 0 に加算する
 
 * Agda tips : 不明な項を ? と書くこともできます。 goal と呼びます
@@ -87,13 +96,15 @@
 
 # Agda における関数定義のSyntax
 * Agda において、関数は
+  * _ + _ : Int -> Int -> Int
   * 関数名                      : 型
   * 関数名 引数はスペース区切り = 関数の定義や値
 * のように定義します
-* 中置関数は _ で挟みます
+* 中置関数は、引数があるべきところに _ を書くことでできます
 
 
 # Agda で複数の引数がある関数の型
+* _ + _ : Int -> Int -> Int
 * func : A -> (A -> B) -> B
 
 * 引数の型 -> 返り値の型
@@ -106,9 +117,8 @@
 * Agda においてはデータ型は引数で分解することができます
 * ある型に続している値が、どのコンストラクタにおいて構成されたかをパターンで示せます
 * Int は O か Int に S が付いたもの、でした
-  * double : Int -> Int
-  * double O     = O
-  * double (S x) = S (S (double x))
+  * x + O     = x
+  * x + (S y) = S (x + y)
 * 関数名 (引数のパターン) = 定義
 
 
@@ -128,13 +138,15 @@
 * 加法の結合法則 : (x + y) + z = x + (y + z) <- 目標ライン
 
 * 乗法の交換法則 : (x * y) = (y * x)
+* 乗法の結合法則 : (x * y) * z = x * (y * z)
+
 
 # '等しい' ということ
-* '等しい'という型 _ ≡ _ を定義する
+* '等しい'という型 _ ≡ _ を data で定義します。コンストラクタは以下。
   * refl  : x ≡ x
   * sym   : x ≡ y -> y ≡ x
   * cong  : (f : A -> B) -> x ≡ y -> f x ≡ f y
-  * trans : x ≡ y -> y ≡ z -> y ≡ z
+  * trans : x ≡ y -> y ≡ z -> x ≡ z
 * defined : Relation.Binary.PropositionalEquality in Standard Library
 * Agda tips : 記号は \ の後に文字列を入れると出てきます。 '≡' は "\ =="
 
@@ -144,7 +156,7 @@
   * term : (A : Set) -> (a : Set) -> a ≡ a
   * term A a = refl
 * 関数なら normal form が同じなら同じ
-  * lambda-term : (A : Set)  -> (\(x : A) -> x) ≡ (\(y : A) -> y)
+  * lambda-term : (A : Set)  -> (\ (x : A) -> x) ≡ (\ (y : A) -> y)
   * lambda-term A = refl
 * 関数による式変形は等しいものとして扱います
 
@@ -164,18 +176,39 @@
   sum-sym (S x) (S y) = ?
 ```
 
+
+# O, O の場合
+* sum-sym    O     O  = refl
+* 両方ともO の時、証明したい命題は O + O ≡ O + O
+* _ + _ の定義の x + O  = x より
+* O ≡ O を構成したい
+* refl によって構成する
+* refl O と考えてもらえると良い
+
+
+# 片方が O, 片方に S が付いている場合
+* sum-sym    O  (S y) = cong S (sum-sym O y)
+* 式的には O + (S y) ≡ (S y) + O
+* _ + _ の定義 x + (S y) = S (x + y) より
+* O + (S y) ≡ S (O + y)
+* 交換して O + (S y) ≡ S (y + O)
+* つまり y と O を交換して S をかけると良い
+* 交換して S をかける -> cong S (sum-sym O y)
+
+
 # trans による等式変形
 * sum-sym (S x) (S y) の時は1つの関数のみで等しさを証明できない
 * 等しさを保ったまま式を変形していくことが必要になります
 
-* sum-sym (S x) (S y) = trans (a ≡ b) (b ≡ c)
+* sum-sym (S x) (S y) = trans (f : a ≡ b) (g : b ≡ c)
   * trans (refl) ?
-  * trans (trans refl (cong S (left-add-one x y)) ?
+  * trans (trans refl (cong S (sum-sym (S x) y)) ?
 
 
 # ≡-reasoning による等式変形
 * trans が何段もネストしていくと分かりづらい
-* ≡-reasoning という等式変形の拡張構文が Standard Library にあります
+* ≡-reasoning という等式変形の構文が Standard Library にあります
+* Agda では見掛け上構文のような関数をAgdaでは定義できます
 
 ```
   begin
@@ -198,7 +231,7 @@
 
 
 # 交換法則の証明 : + の定義による変形
-* 上から + の定義により変形
+* + の定義である x + (S y) = S (x + y) により変形
 
 ```
   sum-sym (S x) (S y) = begin
@@ -227,7 +260,7 @@
 * 加法の定義は
   * x + (S y) = S (x + y)
 * left-operand にかかっている S を移動させる方法が無い
-* たしかに
+* たしかに ? のについて
   * S (y + S x) ≡ S y + S x
 * にあてはまるものを入れてくれ、と出てきている
 
@@ -322,4 +355,14 @@
   * lambda-term の等価性によってリファクタリングなど
 
 
+# 良くあるエラー
+* parse error
+  * スペースある無しで意味が変わります
+  * A: Set <- NG
+  * A : Set <- OK
+  * A: という term がありえるから
+* 型が合わない   -> 赤で警告されます
+* 情報が足りない -> 黄色で警告されます
+
+
 <!-- vim: set filetype=markdown.slide: -->