\chapter{証明支援系言語 Agda による証明手法}
\label{chapter:agda}
第\ref{chapter:category}章においては functor, natural transformation, monad の定義と functional programming における対応について述べた。
その中で、 Functor 則や Monad 則といった満たすべき性質がいくつか存在した。
functional programming において、あるデータ型やそれに対応する計算が Functor 則を満たすことを保証することは言語の実装に依存していい。
例えば、 Haskell において functor は型クラスによって提供されるため、型レベルのチェックに留まっている。
そのため、型チェックは通るが Functor 則を満たさない functor が定義可能となってしまう。

そこで、証明支援系言語 Agda を用いて、 Delta が Functor 則と Monad 則を満たすことを証明することとする。
そのためにまずは Agda における証明手法について述べる。

% {{{ Natural Deduction

\section{Natural Deduction}
\label{section:natural_deduction}
証明には natural deduction(自然演繹)を用いる。
natural deduction は Gentzen によって作られた論理と、その証明システムである。
命題変数と記号を用いた論理式で論理を記述し、推論規則により変形することで求める論理式を導く。

natural deduction において

\begin{eqnarray}
    \vdots \\ \nonumber
    A \\ \nonumber
\end{eqnarray}

と書いた時、最終的に命題Aを証明したことを意味する。
証明は木構造で表わされ、葉の命題は仮定となる。
仮定には dead か alive の2つの状態が存在する。

\begin{eqnarray}
    \label{exp:a_implies_b}
    A \\ \nonumber
    \vdots \\ \nonumber
    B \\ \nonumber
\end{eqnarray}

式\ref{exp:a_implies_b}のように A を仮定して B を導くことができたとする。
この時 A は alive な仮定である。
証明された B は A の仮定に依存していることを意味する。

ここで、推論規則により記号 $ \Rightarrow $ を導入する。

\begin{prooftree}
    \AxiomC{[$ A $]}
    \noLine
    \UnaryInfC{ $ \vdots $}
    \noLine
    \UnaryInfC{ $ B $ }
    \RightLabel{ $ \Rightarrow \mathcal{I} $}
    \UnaryInfC{$ A \Rightarrow B $}
\end{prooftree}

そうすると、仮定 A は dead となり、新たな命題 $ A \Rightarrow B $ を導くことができる。
A という仮定に依存して B を導く証明から、A が存在すれば B が存在するという証明を導いたこととなる。
このように、仮定から始めて最終的に全ての仮定を dead とすることで、仮定に依存しない証明を導くことができる。

alive な仮定を dead にすることができるのは $ \Rightarrow I $ 規則のみである。
それを踏まえ、 natural deduction には以下のような規則が存在する。

\begin{itemize}
    \item Hypothesis

        仮定。葉にある式が仮定となるため、論理式A を仮定する場合に以下のように書く。

        $ A $

    \item Introductions

        導入。証明された論理式に対して記号を導入することで新たな証明を導く。


\begin{prooftree}
    \AxiomC{ $ \vdots $}
    \noLine
    \UnaryInfC{ $ A $ }
    \AxiomC{ $ \vdots $}
    \noLine
    \UnaryInfC{ $ B $ }
    \RightLabel{ $ \land \mathcal{I} $}
    \BinaryInfC{$ A \land B $}
\end{prooftree}

\begin{prooftree}
    \AxiomC{ $ \vdots $}
    \noLine
    \UnaryInfC{ $ A $ }
    \RightLabel{ $ \lor 1 \mathcal{I} $}
    \UnaryInfC{$ A \lor B $}
\end{prooftree}

\begin{prooftree}
    \AxiomC{ $ \vdots $}
    \noLine
    \UnaryInfC{ $ B $ }
    \RightLabel{ $ \lor 2 \mathcal{I} $}
    \UnaryInfC{$ A \lor B $}
\end{prooftree}

\begin{prooftree}
    \AxiomC{[$ A $]}
    \noLine
    \UnaryInfC{ $ \vdots $}
    \noLine
    \UnaryInfC{ $ B $ }
    \RightLabel{ $ \Rightarrow \mathcal{I} $}
    \UnaryInfC{$ A \Rightarrow B $}
\end{prooftree}

\item Eliminations

    除去。ある論理記号で構成された証明から別の証明を導く。

\begin{prooftree}
    \AxiomC{ $ \vdots $}
    \noLine
    \UnaryInfC{ $ A \land B $ }
    \RightLabel{ $ \land 1 \mathcal{E} $}
    \UnaryInfC{$ A $}
\end{prooftree}

\begin{prooftree}
    \AxiomC{ $ \vdots $}
    \noLine
    \UnaryInfC{ $ A \land B $ }
    \RightLabel{ $ \land 2 \mathcal{E} $}
    \UnaryInfC{$ B $}
\end{prooftree}

\begin{prooftree}
    \AxiomC{ $ \vdots $}
    \noLine
    \UnaryInfC{ $ A \lor B $ }

    \AxiomC{[$A$]}
    \noLine
    \UnaryInfC{ $ \vdots $}
    \noLine
    \UnaryInfC{ $ C $ }

    \AxiomC{[$B$]}
    \noLine
    \UnaryInfC{ $ \vdots $}
    \noLine
    \UnaryInfC{ $ C $ }

    \RightLabel{ $ \lor \mathcal{E} $}
    \TrinaryInfC{ $ C $ }
\end{prooftree}

\begin{prooftree}
    \AxiomC{ $ \vdots $}
    \noLine
    \UnaryInfC{ $ A $ }

    \AxiomC{ $ \vdots $}
    \noLine
    \UnaryInfC{ $ A \Rightarrow B $ }

    \RightLabel{ $ \Rightarrow \mathcal{E} $}
    \BinaryInfC{$ B $}
\end{prooftree}

\end{itemize}

記号 $ \lor, \land, \Rightarrow $ の導入の除去規則について述べた。
natural deduction には他にも $ \forall, \exists, \bot $ といった記号が存在するが、ここでは解説を省略する。

それぞれの記号は以下のような意味を持つ
\begin{itemize}
    \item $ \land $
        conjunction。2つの命題が成り立つことを示す。
        $ A \land B $ と記述すると A かつ B と考えることができる。

    \item $ \lor $
        disjunction。2つの命題のうちどちらかが成り立つことを示す。
        $ A \lor B $ と記述すると A または B と考えることができる。

    \item $ \Rightarrow $
        implication。左側の命題が成り立つ時、右側の命題が成り立つことを示す。
        $ A \Rightarrow B $ と記述すると A ならば B と考えることができる。
\end{itemize}

例として、natural deduction で三段論法を証明する。
なお、三段論法とは「A は B であり、 B は C である。よって A は C である」といった文を示すこととする。

\begin{prooftree}
    \AxiomC{ $ [A] $ $_{(1)}$}
    \AxiomC{ [$ (A \Rightarrow B) \land (B \Rightarrow C)$] $_{(2)}$ }
    \RightLabel{ $ \land 1 \mathcal{E} $ }
    \UnaryInfC{ $ (A \Rightarrow B) $ }
    \BinaryInfC{ $ B $ }

    \AxiomC{ [$ (A \Rightarrow B) \land (B \Rightarrow C)$] $_{(2)}$ }
    \RightLabel{ $ \land 2 \mathcal{E} $ }
    \UnaryInfC{ $ (B \Rightarrow C) $ }

    \BinaryInfC{ $ C $ }
    \RightLabel{ $ \Rightarrow \mathcal{I} _{(1)}$}
    \UnaryInfC{ $ A \Rightarrow C $}
    \RightLabel{ $ \Rightarrow \mathcal{I} _{(2)}$}
    \UnaryInfC{ $ ((A \Rightarrow B) \land (B \Rightarrow C)) \Rightarrow (A \Rightarrow C) $}
\end{prooftree}

まず、三段論法を論理式で表す。

「A は B であり、 B は C である。よって A は C である」 が証明するべき命題である。
まず、「A は B であり」から、Aから性質Bが導けることが分かる。これが $ A \Rightarrow B $ となる。
次に、「B は C である」から、Bから性質Cが導けることが分かる。これが $ B \Rightarrow C $ となる。
そしてこの2つは同時に成り立つ。
よって  $ (A \Rightarrow B) \land (B \Rightarrow C)$ が前提となる。
この条件2つが成り立つ時に「Aは Cである」が成りたつ。
条件と同じように「A は C である」は、 $ A \Rightarrow C $ と書けるため、証明するべき論理式は $ ((A \Rightarrow B) \land (B \Rightarrow C)) \Rightarrow (A \Rightarrow C) $ になる。

証明の手順はこうである。
まず条件$ (A \Rightarrow B) \land (B \Rightarrow C)$とAを2つ仮定する。
条件を $ \land 1 \mathcal{E} $ $ \land 2 \mathcal{E} $ により分解する。
A と $ A \Rightarrow B$ から B を、 B から $ B \Rightarrow C $ から C を導く。
ここで $ \Rightarrow \mathcal{I} $ により $ A \Rightarrow C $ を導く。
この際に dead にする仮定は A である。
そのために $_{(1)} $ と対応する \verb/[]/の記号に数値を付けてある。
これで残る仮定は $ (A \Rightarrow B) \land (B \Rightarrow C)$ となり、これから $ A \Rightarrow C $ を導くことができたためにさらに $ \Rightarrow \mathcal{I} $ を適用する。
結果、証明すべき論理式$ ((A \Rightarrow B) \land (B \Rightarrow C)) \Rightarrow (A \Rightarrow C) $ が導けたために証明終了となる。

% }}}

% {{{ Curry-Howard Isomorphism

\section{Curry-Howard Isomorphism}
\label{section:curry_howard_isomorphism}
\ref{section:natural_deduction}節では natural deduction における証明手法について述べた。
natural deduction における証明は Curry-Howard Isomorphism により型付き $ \lambda $ 計算と対応している。

$ \lambda $ 計算とは、計算モデルの1つであり、計算の実行を関数への適用としてモデル化したものである。
関数は $ \lambda $ 式として表され、引数を1つ取りその引数を計算する関数は式\ref{exp:lambda_expression}のように記述される。

\begin{equation}
    \label{exp:lambda_expression}
    \lambda x . x
\end{equation}

値と $ \lambda $ 式には型を付与することができ、その型の計算が natural deduction と対応している。

例えば命題Aが成り立つためには A という型を持つ値が存在すれば良い。
しかしこの命題は A という alive な仮定に依存している。
natural deduction では A の仮定を dead にするために $ \Rightarrow \mathcal{I} $ により $ \Rightarrow $ を導入する。
これが $ \lambda $ による抽象化に対応している。

\begin{eqnarray}
    x : A \\ \nonumber
    \lambda x . x : A \rightarrow A
\end{eqnarray}

プログラムにおいて、変数 x は内部の値により型が決定される。
特に、x の値が未定である場合は未定義の変数としてエラーが発生する。
しかし、 x を取って x を返す関数は定義することはできる。
これは natural deduction の $ \Rightarrow \mathcal{I} $ により仮定を discharge することに相当する。

このように、 natural deduction における証明はそのまま 型付き $ \lambda $ 計算にエンコードすることができる。

それぞれの詳細な対応は省略するが、表\ref{tbl:curry_howard_isomorphism} のような対応が存在する。

\begin{center}
    \begin{table}[htbp]
        \begin{tabular}{|c||c|c|} \hline
                        & natural deduction   & 型付き $ \lambda $ 計算  \\ \hline \hline
            hypothesis  & $ A $               & 型 A を持つ変数 x \\ \hline
            conjunction & $ A \land B $       & 型 A と型 B の直積型 を持つ変数 x \\ \hline
            disjunction & $ A \lor B $        & 型 A と型 B の直和型 を持つ変数 x \\ \hline
            implication & $ A \Rightarrow B $ & 型 A を取り型 B の変数を返す関数 f \\ \hline
        \end{tabular}
        \caption{natural deuction と 型付き $ \lambda $ 計算との対応}
        \label{tbl:curry_howard_isomorphism}
    \end{table}
\end{center}

\ref{section:natural_deduction}節でも行なった三段論法の証明を Haskell により行なうとリスト\ref{src:modus_ponens}

\begin{table}[html]
    \lstinputlisting[label=src:modus_ponens, caption=Haskell における三段論法の証明] {src/modus_ponens.txt}
\end{table}

証明は $ \lambda $ 式の型として表現される。
Haskell における $ \lambda $ 式は \verb| \x -> x| のように表される。
\verb/\/ と \verb/->/ の間が引数であり、 \verb/->/ の後に処理を記述する。
また、$ \land $ に対応する直積型は tuple として提供される。
A と B の直積型は $ (A, B) $ として表現される。
そして、 $ \land 1 \mathcal{E} $ に対応する処理は関数 fst 、 $ \land 2 \mathcal{E} $ に対応する処理は関数 snd として提供される。
fst と snd が $ \land $ の除去に対応しているのは型を見ることで分かる。

そして三段論法の証明の解説を行なう。
三段論法の仮定は、$ (A \Rightarrow B) \land (B \Rightarrow C) $ であった。
この仮定を変数 cond として受けとる。
cond に対して fst を行なうことで $ (A \Rightarrow B) $ を、snd を行なうことで $ (B \Rightarrow C) $ を証明する。
ここでさらに仮定 a を導入し、$ (A \Rightarrow B) $ と$ (B \Rightarrow C) $ に適用することで C を得る。

結果、 \verb/\cond -> (\a -> (snd cond ((fst cond) a)))/のような式が得られ、この型を確認すると正しく三段論法の証明となっている。
なお、型推論の際に A はt2 に、 B は t1 に、 C は t という型名になっている。

% }}}

% {{{ Agda による証明

\section{Agda による証明}
\label{section:agda}
\ref{section:curry_howard_isomorphism}節において型を用いて証明を行なう手法を述べた。
しかし、Haskell における型システムは証明を記述するために用いるものではない。
よって、依存型を持つ証明支援言語 Agda を用いて証明を記述していく。

依存型とは値に依存した型を作ることができる型であり、非常に表現能力が高い。
値に型を使うことができるために証明に基づいた証明を記述することができる。

$ \Rightarrow \mathcal{E} $ に対応する関数適用を Agda で記述するとリスト\ref{src:apply_function_in_agda}のようになる。

\begin{table}[html]
    \lstinputlisting[label=src:apply_function_in_agda, caption=Agda における $ \Rightarrow \mathcal{E} $ ] {src/apply_function.agda}
\end{table}

Agda による型注釈は \verb/ term : type/ と記述する。
postulate とすると alive な証明を記述することができる。
まずは alive な A を仮定している。
なお、Set 型は型の型として組込みで用意されている型である。
そのため詳細は省略するが、 A は型であると考える。

次に関数 f を仮定する。
仮定に用いられている記号 \verb/{}/ の内部の式は implicit な paramter である。
任意の B の対してこの型が成り立つことを記述している。
implicit な parameter は可能であれば Agda が推論する。
そのため、f の見掛け上の型は \verb/A -> B/のようになる。
ここで、 B に明示的に値を代入することで f の型を変更することもできる。
このように Agda では型における引数のようなものが存在し、型の表現能力が高い。

A と f の2つを仮定したところで、証明である \verb/->E/を定義する。
証明するべき式は \verb/->E/ の型として与えられ、証明は \verb/->E/ の式として記述する。
式の型に対する定義を正しく行なうことで証明を与える。

$ \Rightarrow \mathcal{E} $ に対応する \verb/->E/ は関数の適用なので、値a と関数 f を受けとって適用することで B が得られる。
なお、仮定を alive のまま証明を記述するのは依存した仮定を残すことになるため、必要な仮定を引数として受けとったり、implicit な parameter として指定して証明するのが良い。

また、Agda は証明に用いる規則なども Agda 内部で定義することができる。
例えば、直積型の定義はリスト\ref{src:product}のようなものがある。

\begin{table}[html]
    \lstinputlisting[label=src:product, caption=Agdaにおける直積型の例] {src/product.agda}
\end{table}

関数の定義時に \verb/_/ とした部分には項を入れることで関数が適用される。
つまり \verb/_x_/ とすれば中置関数を作成することができる。
データ型 \verb/_x_/ は型 A と B を持つ型である。
データ型 \verb/_x_/ はコンストラクタ \verb/<_,_>/ により構成され、コンストラクタは A と B を取ることで \verb/A x B/ 型を返す。

例えば型A と B から 直積型 $ A \times B $ が作成できる証明は constructProduct である。
任意の型AとBを受けとり、コンストラクタ \verb/<_,_>/を用いて $ A \times B $ に相当する \verb/A x B/を返す。

また、型に対応するコンストラクタはパターンマッチにより分解することができる。
その例が patternMatchProduct である。
受けとる引数の型は \verb/ A x B/ であるため、ありえるコンストラクタは \verb/<_,_>/のみである。
よって引数を取る際に \verb/< a , b >/ のように対応するコンストラクタと変数を用意することで、コンストラクタに基づいて型を分解することができる。
\verb/A x B/ 型から B を取るため、\verb/A x B/ 型の変数を直接束縛せずにコンストラクタで分解し、a と b に束縛することで A と B が得られる。
そのため、 patternMathProduct は $ \land 2 \mathcal{E} $ そのものである。

% }}}

% {{{ Reasoning

\section{Reasoning}
\label{section:reasoning}
\ref{section:agda} 節ではAgdaにおける証明の手法について解説した。
\ref{section:reasoning}節では Agda における証明の例として、自然数の加法の交換法則を証明する。

まずは自然数を定義する。
今回用いる自然数の定義は以下のようなものである。

\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}

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/addSym/ を実行することで証明できる。

        この2つの証明はこのような意味を持つ。
        n が 0 であるとき、 m も 0 なら簡約により等式が成立する。
        n が 0 であるとき、 m が 0 でないとき、 m は後続数である。
        よって m が (S x) と書かれる時、 x は m の前の値である。
        前の値による交換法則を用いてからその結果の後続数も + の定義により等しい。
        ここで、 \verb/addSym/ に渡される 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/addSym/ により 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 を用いる。

$ \equiv $-Reasoning では等式の左辺を begin の後に記述し、等式の変形を $ \equiv \langle expression \rangle $ に記述することで変形していく。
最終的に等式の左辺を $ \blacksquare $ の項へと変形することで等式の証明が得られる。

自然数の加法の交換法則を $ \equiv $-Reasoning を用いて証明した例がリスト\ref{src:nat_add_sym_reasoning}である。
特に n と m が1以上である時の証明に注目する。

\begin{table}[html]
    \lstinputlisting[label=src:nat_add_sym_reasoning, caption= $ \equiv $ - Reasoning を用いた証明の例] {src/nat_add_sym_reasoning.agda.replaced}
\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 における等式の証明は、定義や等式を用いて右辺と左辺を同じ項に変形することで行なわれる。

% }}}