--- a/slide.md	Wed May 21 19:55:16 2014 +0900
+++ b/slide.md	Thu May 22 20:30:05 2014 +0900
@@ -8,16 +8,8 @@
 * 証明支援系の言語である Agda の入門を目的としています
 * 具体的には
   * Agda による証明の方法を知る
-  * 実際に自然数の加算の交換法則の証明を追う
-
-
-# セミナーについて必要する事前知識
-* なお、このセミナーについては
-  * C や Java によるプログラミング言語を書いたことがある
-    * 関数や引数、型といった単語の詳細は省略することがあります
-  * 数学における述語論理
-    * P ならば Q といった論理
-* といったことを前提条件としています
+  * 実際に自然数に対する演算の証明を追う
+* ことをしていきます
 
 
 # Agda とはどういう言語なのか
@@ -25,176 +17,154 @@
   * 他には Coq などがあります
 * Haskell で実装されています
 * dependent type の言語 です
-  * 型から生成さえれた型を扱える
-  * いわゆる「強い静的型付け」などと言われる種類です
+  * 型を第一級オブジェクトとして扱える
+  * X -> X, f x, a == b のような型を扱うことができます
 
 
 # 型と証明との対応 : Curry-Howard Isomorphism
 * Agda における証明は
   * 証明したい命題 == 関数の型
   * 命題の証明     == 関数の定義
-* として定義します。
+* として定義します
 * 関数と命題の対応を Curry-Howard Isomorphism と言います
 
 
-# 'A ならば B' と 'A' が成り立つなら 'B'
-
-* Agda において
-  * apply : A -> (A -> B) -> B
-  * apply a f = f a
-* と記述します
-
-
-# Agda のSyntax
-* apply : A -> (A -> B) -> B
-* apply a f = f a
-
-* 関数名 : 型
-* 関数名 <引数,,,> = 定義
-
-
-# Agda の型のSyntax
-* apply : A -> (A -> B) -> B
-
-* 引数の型 -> 返り値の型
-* 結合は右結合です。なのでこのようになります
-  * A -> ((A -> B) -> B)
-* 右結合のため、A を受けとって ((A -> B) -> B) を返す、とも読めます
-
-
-# Agda の型のSyntax : 複数の引数
-* 複数の引数は
-  * Arg1Type -> Arg2Type -> ReturnType
-* のように書きますが、右結合により
-  * Arg1Type -> (Arg2Type -> ReturnType)
-* となり、引数は1つしかないと考えることができます。
-* これを Curry 化と言い、引数が複数の場合を考えずに良くなります
-
-
-# 関数の定義を C の Syntax 書くと
-* apply : A -> (A -> B) -> B
-
-* B apply(A a, B ( * f )(A))
-* これを満たす定義を関数applyの実装として書けば良い
-* 証明 == 正しい返り値を返す なので
-* つまりコンパイルを通してしまえば良い
-
-
-# Agda で書いてみると
-
-* emacs から使うと良いです
+# Agda をはじめよう
+* emacs に agda-mode があります
 * module < filename > where
 * を先頭に書く必要があります
 * 証明を定義していく
 * C-c C-l で型チェック(証明チェック)ができます
 
 
-# Agda による apply
-* apply : A -> (A -> B) -> B
-* apply a f = f a
-
-* とは
-* A を Int, B を String とすると
-* Int と、 Int から String を返す関数があれば String を作れる
-* と読めます。つまり関数適用です
+# 自然数の定義 : Peano Arithmetic
+* 自然数 0 が存在する
+* 任意の自然数 a にはその後続数 suc(a) が存在する
+* 0 より前の自然数は存在しない
+* 異なる自然数は異なる後続数を持つ
+    * a != b のとき suc(a) != suc(b) となる
+* 0 が性質を満たし、a も性質を満たせばその後続数も性質を満たすとき、すべての自然数はその性質を満たす
 
 
-# 命題に 'ならば' を含む場合
-* 関数を返せば良いです
-* Agda には lambda があるので
-  * id : (A -> A)
-  * id = \a -> a
-* といったように書けます。
-* lambda の syntax は \arg -> body です
+# Agda における自然数の定義
+* data 型を使います
+    * data Int : Set where
+    *   Zero : Int
+    *   Succ : Int -> Int
+* Zero は Int, Succ は Int を受けとって Int を返す、と読めます
+* Set は組込みで存在する型です。「成り立つ」といった感じです。
+
+
+# 自然数の例
+* 0 = Zero
+* 1 = Succ Zero
+* 2 = Succ (Succ Zero)
+* 5 = Succ (Succ (Succ (Succ (Succ Zero))))
 
 
-# 'ならば' を含む証明
-* 三段論法 の証明
+# 自然数に対する演算の定義
+* a と b の加算 : a にかかっている Succ の分だけ Succ を b にかける
+* a と b の加算 : a にかかっている Succ の分だけ b を 0 に加算する
 
-* compose : (A -> B) -> (B -> C) -> (A -> C)
-* compose f g = \a -> g (f a)
-
-* 三段論法は関数の合成に相当しています
+* Agda tips : 不明な項を ? と書くこともできます
+* その状態で C-c C-l するとその項の型が分かります
 
 
-# Agda による 証明 の方法のまとめ
-* 型として (仮定) -> (仮定) -> ... -> (命題)
-* として命題を定義
-* それを満たす定義を関数として定義する
+# Agda における関数定義のSyntax
+* Agda において、関数は
+  * 関数名                        : 型
+  * 関数名 <スペース区切りで引数> = 関数の定義や値
+* のように定義します
 
 
-# 自然数の加算の交換法則の証明
-* まずは自然数を定義する
-* ペアノ算術を使います
+# Agda における引数を持つ関数の型の表記法
+* func : A -> (A -> B) -> B
+
+* 引数の型 -> 返り値の型
+* -> の結合は右結合です。なので括弧を付けると以下のようになります
+  * A -> ((A -> B) -> B)
+* 右結合のため、A を受けとって ((A -> B) -> B) を返す、とも読めます
 
 
-# ペアノ算術による自然数の定義
-* ゼロは自然数である
-* 自然数の後続数は自然数である
-* TODO: 詳細は今から
-
+# Agda における自然数に対する演算の定義
+TODO: 書いておく
 
-# ペアノ算術の Agda による定義
-* data type を定義します
-* data Int where
-*   O -> Int
-*   S -> Int -> Int
-* Int は O か、 Int に S をかけたもの、とします
+* Agda tips : C-c C-n すると式を評価することができます
+* add (Succ Zero) (Succ (Succ Zero)) などしてみましょう
 
 
 # パターンマッチ
-* Agda においてはデータ型を引数で分解することができます
+* Agda においてはデータ型は引数で分解することができます
 * ある型に続している値が、どのコンストラクタにおいて構成されたかをパターンで示せます
-* これをパターンマッチと言います
   * double : Int -> Int
   * double O     = O
   * double (S n) = S (S (double n))
 * 関数名 (引数のパターン) = 定義
 
 
-# パターンマッチによる自然数の加算の定義
-* TODO: 今から
-
+# これから証明していきたいこと
+* 加法の交換法則 : (a + b) = (b + a)
+* 加法の結合法則 : (a + b) + c = a + (b + c)
 
-# '等しさ' ということ
-* 交換法則においては '等しい' ということを証明しなければなりません
-* 等しい、ということも定義する必要があります
-* 命題は型で定義するため、'等しい'、という型が必要です
+* 分配法則       : x * (y + z) = (x * y) + (x * z)
+
+* 乗法の交換法則 : (a * b) = (b * a)
+* 乗法の結合法則 : (a * b) * c = a * (b * c)
 
 
-# 等しさをデータ型で定義する
-* == を定義していきます
-* == は型でなくてはならないので
-  * data _==_ : {A : Set} -> A -> A -> Set where
-* となります
-* よって、 hoge と fuga の等しさを証明したい場合は
-* 'hoge == fuga' 、という型を持つ項を関数の定義に書くことが証明になります
+# '等しい' ということ
+* '等しい'という型 _ ≡ _ を定義する
+  * 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
+* defined : Relation.Binary.PropositionalEquality in Standard Library
 
 
-# '等しい'ということの定義3つ
-* TODO: refl, sym, cong を書きます
-* comment
-  * 個人的には Relation.Binary.PropositionalEquality を open import するよりは自前で定義したい
-  * あと R とか reasoning もできれば使いたくない
-  * というか必要でないなら積極的に削っていかないと時間がおそらく足りない
-  * 時間あまった時用に証明をもう1,2 個くらい書いておきたい
+# '同じもの'とは
+* 項なら同じ項
+  * 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 = refl
 
 
-# 交換法則を命題として定義する
-* == を用いて
-  * (n : Int) -> (m : Int) -> n + m == m + n
+# 交換法則を型として定義する
+* ≡を用いて
+  * (n : Int) -> (m : Int) -> n + m ≡ m + n
 * 引数は (名前 : 型) として名前付けできます
 
 
-# 交換法則を証明する
-* 交換法則を関数の定義として書いていきます
-* TODO: 今から
+# 等式変形
+TODO: trans による等式変形
+
+
+# ≡-reasoning による等式変形
+TODO: reasoning による等式変形
+
+
+# 加法の交換法則 : (a + b) = (b + a)
+TODO: 書いとく
+
+# 加法の結合法則 : (a + b) + c = a + (b + c)
+TODO: 書いとく
+
+# 分配法則       : x * (y + z) = (x * y) + (x * z)
+TODO: 書いとく(うしろで良いかな)
+
+# 乗法の交換法則 : (a * b) = (b * a)
+TODO: 書いとく(うしろで良いかな)
+
+# 乗法の結合法則 : (a * b) * c = a * (b * c)
+TODO: 書いとく(うしろで良いかな)
 
 
 # Agda による証明方法のまとめ
 * 関数の型を命題、関数の定義を証明とする
-* 命題を扱う必要があるため、型もデータ型として定義できる
-* データ型はパターンマッチにより分解することができる
+* 等しさを証明するには等しいという型を定義する
+* 等しさを保ったまま式を変形していくことにより等価性を証明できる
+    * trans, reasoning
 * C-c C-l により型のチェックが成功すれば証明終了