--- a/agda.tex	Wed Feb 11 12:37:46 2015 +0900
+++ b/agda.tex	Wed Feb 11 13:12:38 2015 +0900
@@ -361,6 +361,8 @@
 
 % }}}
 
+% {{{ Reasoning
+
 \section{Reasoning}
 \label{section:reasoning}
 \ref{section:agda} 節ではAgdaにおける証明の手法について解説した。
@@ -496,3 +498,37 @@
 3 つのパターンにおいては refl や cong といった単純な項で証明を行なうことができた。
 しかし長い証明になると refl や cong といった式を trans で大量に繋げていく必要性がある。
 長い証明を分かりやすく記述するために $ \equiv $-Reasoning を用いる。
+
+$ \equiv $-Reasoning では等式の左辺を begin の後に記述し、等式の変形を $ \equiv \langle expression \rangle $ に記述することで変形していく。
+最終的に等式の左辺を $ \blacksquare $ の項へと変形することで等式の証明が得られる。
+
+自然数の加法の交換法則を $ \equiv $-Reasoning を用いて証明した例がリスト\ref{src:nat_add_sym_reasoning}である。
+特に n と m が1以上である時の証明に注目する。
+
+% TODO: FIXME: unicode char
+\begin{table}[html]
+    \lstinputlisting[label=src:nat_add_sym_reasoning, caption= $ \equiv $ - Reasoning を用いた証明の例] {src/nat_add_sym_reasoning.agda}
+\end{table}
+
+まず \verb/ (S n) + (S m)/ は + の定義により \verb/ S (n + (S m)) / に等しい。
+よって refl で導かれる。
+なお、基本的に定義などで同じ項に簡約される時は refl によって記述することが多い。
+
+次に \verb/S (n + (S m)) / に対して addSym を用いて交換し、 cong によって S を追加することで \verb/ S ((S m) + n) / を得る。
+これは、前3パターンにおいて + の右辺の項が 1以上であっても上手く交換法則が定義できたことを利用して項を変形している。
+このように同じ法則の中でも、違うパターンで証明できた部分を用いて別パターンの証明を行なうこともある。
+
+最後に \verb/S ((S m) + n)/ から \verb/(S m) + (S n)/を得なくてはならない。
+しかし、 + の定義には右辺に対して S を移動する演算が含まれていない。
+よってこのままでは証明することができない。
+そのため、等式 $ S (m + n) \equiv m + (S n) $ を addToRight として定義する。
+addToRight の証明の解説は省略する。
+addToRight を用いることで \verb/S ((S m) + n)/ から \verb/(S m) + (S n)/を得られた。
+これで等式 $ (S m) + (S n) \equiv (S n) + (S m) $  の証明が完了した。
+
+自然数に対する + の演算を考えた時にありえるコンストラクタの組み合せ4パターンのいずれかでも交換法則の等式が成り立つことが分かった。
+また、定義した + の演算のみでは加法の交換法則は証明できず、さらに等式を証明する必要があった。
+
+このように、Agda における等式の証明は、定義や等式を用いて右辺と左辺を同じ項に変形することで行なわれる。
+
+% }}}

--- a/main.tex	Wed Feb 11 12:37:46 2015 +0900
+++ b/main.tex	Wed Feb 11 13:12:38 2015 +0900
@@ -5,6 +5,7 @@
 \usepackage{here}
 \usepackage{listings, jlisting}
 \usepackage{bussproofs}
+\usepackage{amssymb}
 
 \setlength{\itemsep}{-1zh}
 \title{圏によるプログラムの変更の形式化}

--- a/src/nat_add_sym_reasoning.agda	Wed Feb 11 12:37:46 2015 +0900
+++ b/src/nat_add_sym_reasoning.agda	Wed Feb 11 13:12:38 2015 +0900
@@ -14,10 +14,8 @@
 addSym O    (S m)  = cong S (addSym O m)
 addSym (S n)   O   = cong S (addSym n O)
 addSym (S n) (S m) = begin
+  (S n) + (S m)  ≡⟨ refl ⟩
   S (n + S m)    ≡⟨ cong S (addSym n (S m)) ⟩
-  S (S (m + n))  ≡⟨ refl ⟩
   S ((S m) + n)  ≡⟨ addToRight (S m) n ⟩
-  S (m + S n) 
-  ∎
-
-
+  S (m + S n)    ≡⟨ refl ⟩
+  (S m) + (S n)  ∎