--- a/agda.tex	Tue Feb 10 12:48:02 2015 +0900
+++ b/agda.tex	Tue Feb 10 15:30:01 2015 +0900
@@ -302,6 +302,7 @@
 % {{{ Agda による証明
 
 \section{Agda による証明}
+\label{section:agda}
 \ref{section:curry_howard_isomorphism}節において型を用いて証明を行なう手法を述べた。
 しかし、Haskell における型システムは証明を記述するために用いるものではない。
 よって、依存型を持つ証明支援言語 Agda を用いて証明を記述していく。
@@ -360,7 +361,138 @@
 
 % }}}
 
+\section{Reasoning}
+\label{section:reasoning}
+\ref{section:agda} 節ではAgdaにおける証明の手法について解説した。
+\ref{section:reasoning}節では Agda における証明の例として、自然数の加法の交換法則を証明する。
 
-\section{Reasoning}
+まずは自然数を定義する。
+今回用いる自然数の定義は以下のようなものである。
+
+\begin{itemize}
+    \item 0 は自然数である
+    \item 任意の自然数には後続数が存在する
+    \item 0 はいかなる自然数の後続数でもない
+    \item 異なる自然数どうしの後続数は異なる ($ n \neq m \rightarrow S n \neq S m $)
+    \item 0がある性質を満たし、aがある性質を満たせばその後続数 S(n) も自然数である
+\end{itemize}
+
+この定義は peano arithmetic における自然数の定義である。
+
+Agda で自然数型 Nat を定義するとリスト \ref{src:nat} のようになる。
+
+\begin{table}[html]
+    \lstinputlisting[label=src:nat, caption=Agda における自然数型 Nat の定義] {src/nat.agda}
+\end{table}
+
+自然数型 Nat は2つのコンストラクタを持つ。
+
+\begin{itemize}
+    \item O
+
+        引数を持たないコンストラクタ。これが0に相当する。
+
+    \item S
+
+        Nat を引数に取るコンストラクタ。これが後続数に相当する。
+
+\end{itemize}
+
+よって、数値の 3 は \verb/S (S (S O))/ のように表現される。
+Sの個数が数値に対応する。
+
+次に加算を定義する(リスト\ref{src:nat_add})。
+
+\begin{table}[html]
+    \lstinputlisting[label=src:nat_add, caption=Agdaにおける自然数型に対する加算の定義] {src/nat_add.agda}
+\end{table}
+
+加算は中置関数 \verb/_+_/ として定義する。
+2つの Nat を取り、Natを返す。
+パターンマッチにより処理を変える。
+0に対して m 加算する場合は m であり、 n の後続数に対して m 加算する場合は n に m 加算した数の後続数とする。
+S を左の数から右の数へ1つずつ再帰的に移していくような加算である。
+
+例えば 3 + 1 といった計算は (S (S (S O))) + (S O) のように記述される。
+ここで 3 + 1 が 4と等しいことの証明を行なう。
+
+等式の証明には agda の standard library における Relation.Binary.Core の定義を用いる。
+
+\begin{table}[html]
+    \lstinputlisting[label=src:equiv, caption= Relation.Binary.Core による等式を示す型 $ \equiv $] {src/equiv.agda}
+\end{table}
+等式は等式を示すデータ型 $ \equiv $ により定義される。
+$ \equiv $ は同じ両辺が同じ項に簡約される時にコンストラクタ refl で構築できる。
+
+実際に 3 + 1 = 4 の証明は refl で構成できる(リスト\ref{src:three_plus_one})。
+
+\begin{table}[html]
+    \lstinputlisting[label=src:three_plus_one, caption= Agda における 3 + 1 の結果が 4 と等しい証明] {src/three_plus_one.agda}
+\end{table}
 
-% TODO: nat かなー
+3+1 という1つの関数を定義し、その型として証明すべき式 \verb/(S (S (S O))) + (S O)≡(S (S (S (S O))))/ を記述する。
+そして証明を関数の定義として記述する。
+今回は \verb/_+_/ 関数の定義により \verb/ (S (S (S (S O)))) / に簡約されるためにコンストラクタ refl が証明となる。
+
+$ \equiv $ によって証明する際、必ず同じ式に簡約されるとは限らないため、いくつかの操作が Relation.Binary.PropositionalEquality に定義されている。
+
+\begin{itemize}
+    \item sym  : $ x \equiv y \rightarrow y \equiv x $
+
+        等式が証明できればその等式の左辺と右辺を反転しても等しい。
+
+    \item cong : $ f \rightarrow x \equiv y \rightarrow f x \equiv f y $
+
+        証明した等式に同じ関数を与えても等式は保たれる。
+
+    \item trans : $ x \equiv y \rightarrow y \equiv z \rightarrow x \equiv z $
+
+        2つの等式に表れた同じ項を用いて2つの等式を繋げた等式は等しい。
+\end{itemize}
+
+ではこれから nat の加法の交換法則を証明していく(リスト\ref{src:nat_add_sym})。
+
+\begin{table}[html]
+    \lstinputlisting[label=src:nat_add_sym, caption= Agda における加法の交換法則の証明] {src/nat_add_sym.agda}
+\end{table}
+
+証明する式は $ n + m \equiv m + n $ である。
+n と m は Nat であるため、それぞれがコンストラクタ O か S により構成される。
+そのためにパターンは4通りある。
+
+\begin{itemize}
+    \item n = O, m = O
+
+        + の定義により、 O に簡約されるため refl で証明できる。
+
+    \item n = O, m = S m
+
+        $ O + (S m) \equiv (S m) + O $  を証明することになる。
+        この等式は + の定義により $ O + (S m) \equiv S (m + O) $ と変形できる。
+        $ S (m + O) $ は $ m + O $ に S を加えたものであるため、 cong を用いて再帰的に \verb/add_sym/ を実行することで証明できる。
+
+        この2つの証明はこのような意味を持つ。
+        n が 0 であるとき、 m も 0 なら簡約により等式が成立する。
+        n が 0 であるとき、 m が 0 でないとき、 m は後続数である。
+        よって m が (S x) と書かれる時、 x は m の前の値である。
+        前の値による交換法則を用いてからその結果の後続数も + の定義により等しい。
+        ここで、 \verb/add_sym/ に渡される m は1つ値が減っているため、最終的には n = 0, m = 0 である refl にまで簡約され、等式が得られる。
+
+    \item n = S n, m = O
+
+        $ (S n) + O \equiv O + (S n) $ を証明する。
+        この等式は + の定義により $ S (n + O) \equiv (S n) $ と変形できる。
+        さらに変形すれば $ S (n + O) \equiv S (O + n) $ となる。
+        よって \verb/add_sym/ により O と n を変換した後に cong で S を加えることで証明ができる。
+
+        ここで、 $ O + n  \equiv n $ は + の定義により自明であるが、$ n + O \equiv n $ をそのまま導出できないことに注意して欲しい。
+        + の定義は左側の項から S を右側の項への移すだけであるため、右側の項への演算はしない。
+
+    \item n = S n, m = S m
+
+        3つのパターンは証明したが、このパターンは少々長くなるため別に解説することとする。
+\end{itemize}
+
+3 つのパターンにおいては refl や cong といった単純な項で証明を行なうことができた。
+しかし長い証明になると refl や cong といった式を trans で大量に繋げていく必要性がある。
+長い証明を分かりやすく記述するために $ \equiv $-Reasoning を用いる。