\chapter{証明支援系言語 Agda による証明手法}
\label{chapter:agda}
\ref{chapter:akasha} 章では CbC のモデル検査的検証アプローチとして、akasha を用いた有限の要素数の挿入時の仕様の検証を行なった。
しかし、要素数13個分の挿入を検証しても赤黒木の挿入が必ずバランスするとは断言しづらい。

そこで、 CbC の性質をより厳密に定義し、その上で証明を行なうことを考えた。
CbC のプログラムを証明できる形に変換し、任意の回数の挿入に対しても性質が保証できるよう証明するのである。
証明を行なう機構として注目したのが型システムである。

型システムは Curry-Howard 同型対応により命題と型付きラムダ計算が一対一に対応する。
依存型という型を持つ証明支援系言語 Agda を用いて型システムで証明が行なえることを示す。

% {{{ 型システムとは TODO: もう少し大ざっぱに説明
\section{型システムとは}
型システムとは、計算する値を分類することにでプログラムがある種の振舞いを行なわないことを保証する機構の事である\cite{Pierce:2002:TPL:509043}\cite{pierce2013型システム入門プログラミング言語と型の理論}。
ある種の振舞いとはプログラム中の評価不可能な式や、言語として未定義な式などが当て嵌まる。
例えば、gcc や clang といったコンパイラは関数定義時に指定された引数の型と呼び出し時の値の型が異なる時に警告を出す。
この警告は関数が受けつける範囲以外の値をプログラマが渡してしまった場合などに有効に働く。
加えて、関数を定義する側も受け付ける値の範囲を限定できるため関数内部の処理を記述しやすい。

型システムで行なえることには以下のようなものが存在する。

\begin{itemize}
    \item エラーの検出

        文字列演算を行なう関数に整数を渡してしまったり、複雑な場合分けで境界条件を見落すなど、プログラマの不注意が型の不整合として表れる。

    \item 抽象化

        型は大規模プログラムの抽象化の単位にもなる。
        例えば特定のデータ構造に対する処理をモジュール化し、パッケージングすることができる。

    \item ドキュメント化

        関数やモジュールの型を確認することにより、プログラムの理解の助けになる。
        また、型はコンパイラが実行されるたびに検査されるため、常に最新の正しい情報を提供する。

    \item 言語の安全性

        例えばポインタを直接扱わないようメモリアクセスを抽象化し、データを破壊する可能性をプログラマに提供しないようにできる。

    \item 効率性

        そもそも、科学計算機における最初の型システムは Fortran~\ref{Backus:1978:HFI:960118.808380} などにおける整数と実数の算術式の区別だった。
        型の導入により、ソースからコンパイラがより最適化されたコードを生成できる。

\end{itemize}

型システムには多くの定義が存在する。
型の表現能力には単純型や総称型、部分型などが存在する。
型付けにも動的型付けや静的型付けが存在し、どの型システムを採用するかは言語の設計に依存する。
例えば C言語では数値と文字を二項演算子 \verb/+/ で加算できるが、Haskell では加算することができない。
これは Haskell が C言語よりも厳密な型システムを採用しているからである。
具体的には Haskell は暗黙的な型変換を許さず、 C 言語は言語仕様として暗黙の型変換を持っている。

型システムを定義することはプログラミング言語がどのような特徴を持つかを決めることにも繋がる。

% }}}

% {{{ Natural Deduction
\section{Natural Deduction}
\label{section:natural_deduction}
まず始めに証明を行なうためにNatural Deduction(自然演繹)を示す。

Natural Deduction は Gentzen によって作られた論理と、その証明システムである~\cite{Girard:1989:PT:64805}。
命題変数と記号を用いた論理式で論理を記述し、推論規則により変形することで求める論理式を導く。

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}

$ \Rightarrow \mathcal{I} $ を適用することで仮定 A は dead となり、新たな命題 $ A \Rightarrow B $ を導くことができる。
A という仮定に依存して B を導く証明から、「A が存在すれば B が存在する」という証明を導いたこととなる。
このように、仮定から始めて最終的に全ての仮定を dead とすることで、仮定に依存しない証明を導ける。
なお、dead な仮定は \verb/[A]/ のように \verb/[]/ で囲んで書く。

alive な仮定を dead にすることができるのは $ \Rightarrow \mathcal{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)$ が仮定となる。
この仮定が成り立つ時に「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 である。
数回仮定を dead にする際は $_{(1)} $ のように対応する \verb/[]/の記号に数値を付ける。
これで残る alive な仮定は $ (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 TODO: もっと増やす(Agda でラムダ計算を説明する)
\section{Curry-Howard Isomorphism}
\label{section:curry_howard_isomorphism}
\ref{section:natural_deduction}節では natural deduction における証明手法について述べた。
natural deduction における証明はほとんど型付き $ \lambda $ 計算のような形をしている。
実際、Curry-Howard Isomorphism により Natural Deduction と型付き $ \lambda $ 計算は対応している。% ref TaPL 104
Curry-Howard Isomorphism の概要を~\ref{section:curry_howard_isomorphism} 節に述べる。

関数型 $ \rightarrow $ のみに注目した時

\begin{enumerate}
    \item 導入規則(T-ABS) は、その型の要素がどのように作られるかを記述する
    \item 除去規則(T-APP) は、その型の要素がどのように作られるかを記述する
\end{enumerate}


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

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

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

また、仮定Aが成り立つ時に結論Bを得ることは、関数適用(T-APP)に相当している。

\begin{prooftree}
    \AxiomC{$A$}
    \AxiomC{$A \rightarrow B $}
    \RightLabel{T-APP}
    \BinaryInfC{$B$}
\end{prooftree}

このように、 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 $ 計算との対応(Curry-Howard Isomorphism)}
        \label{tbl:curry_howard_isomorphism}
    \end{table}
\end{center}
% }}}

% {{{ 依存型を持つ証明支援系言語 Agda

\section{依存型を持つ証明支援系言語 Agda}
型システムを用いて証明を行なうことができる言語に Agda~\cite{agda} が存在する。
Agda は依存型という強力な型システムを持っている。
依存型とは型も第一級オブジェクトとする型であり、型を引数に取る関数や値を取って型を返す関数、型の型などが記述できる。
この節では Agda の文法的な紹介を行なう~\cite{Norell:2009:DTP:1481861.1481862}~\cite{agda-documentation}。

まず Agda のプログラムは全てモジュールの内部に記述されるため、まずはトップレベルにモジュールを定義する必要がある。
トップレベルのモジュールはファイル名と同一となる。
例えば \verb/AgdaBasics.agda/ のモジュール名定義はリスト~\ref{src:agda-module}のようになる。

\lstinputlisting[label=src:agda-module, caption=Agdaのモジュールの定義する] {src/AgdaBasics.agda}

また、Agda はインデントに意味を持つ言語であるため、インデントはきちんと揃える必要がある。

まず Agda におけるデータ型について触れていく。
Agda における型指定は $:$ を用いて行なう。
例えば、変数xが型Aを持つ、ということを表すには \verb/x : A/ と記述する。

データ型は Haskell や ML に似て代数的なデータ構造のパターンマッチを扱うことができる
データ型の定義は \verb/data/ キーワードを用いる。
\verb/data/キーワードの後に \verb/where/ 句を書きインデントを深くした後、値にコンストラクタとその型を列挙する。
例えば Bool 型を定義するとリスト~\ref{src:agda-bool}のようになる。

\lstinputlisting[label=src:agda-bool, caption=Agdaにおけるデータ型 Bool の定義] {src/AgdaBool.agda}

Bool はコンストラクタ \verb/true/ か \verb/false/ を持つデータ型である。
Bool 自身の型は \verb/Set/ であり、これは Agda が組み込みで持つ「型の型」である。
Set は階層構造を持ち、型の型の型を指定するには Set1 と書く。

関数の定義は Haskell に近い。
関数名と型を記述した後に関数の本体を \verb/=/ の後に指定する。
関数の型は単純型付き $ \lambda$ 計算と同様に $ \rightarrow $ を用いる。
なお、$\rightarrow$に対しては糖衣構文 \verb/->/ も用意されている。
引数は変数名で受けることもできるが、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。
これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなものである。
例えば Bool 型の値を反転する \verb/not/ 関数を書くとリスト~\ref{src:agda-not}のようになる。

\lstinputlisting[label=src:agda-not, caption=Agdaにおける関数 not の定義] {src/AgdaNot.agda}

関数にはリテラルが存在し、関数名を定義せずともその場で生成することができる。
これをラムダ式と呼び、\verb/\arg1 arg2 -> function body/ のように書く。
例えば Bool 型の引数 \verb/b/ を取って not を適用する \verb/not-apply/ をラムダ式で書くとリスト~\ref{src:agda-lambda}のようになる。
関数 \verb/not-apply/ をラムダ式を使わずに定義すると \verb/not-apply-2/ になるが、この二つの関数は同一の動作をする。

\lstinputlisting[label=src:agda-lambda, caption=Agda におけるラムダ式] {src/AgdaLambda.agda}

コンストラクタによって処理を分岐する場合はパターンマッチを利用する。
関数の変数部分にコンストラクタを指定し、それぞれに対する処理を \verb/=/ で繋いで記述する。
パターンマッチは全てのコンストラクタのパターンを含まなくてはならない。
なお、コンストラクタをいくつか指定した後に変数で受けると、変数が持ちうる値は指定した以外のコンストラクタとなる。
例えばリスト~\ref{src:agda-pattern}の not は x には true しか入ることは無い。
なお、マッチした値を変数として利用しない場合は \verb/_/ を用いて捨てることもできる。

\lstinputlisting[label=src:agda-pattern, caption=Agdaにおけるパターンマッチ] {src/AgdaPattern.agda}

Agda では特定の関数内のみで利用する関数を \verb/where/ 句で記述できる。
これは関数内部の冗長な記述を省略するのに活用できる。
スコープは \verb/where/句が存在する関数内部のみであるため、名前空間が汚染させることも無い。
例えば自然数3つを取ってそれぞれ3倍して加算する関数 \verb/f/ を定義するとき、 \verb/where/ を使うとリスト~\ref{src:agda-where} のように書ける。
これは \verb/f'/ と同様の動作をする。
\verb/where/ 句は利用したい関数の末尾にインデント付きで \verb/where/ キーワードを記述し、改行の後インデントをして関数内部で利用する関数を定義する。

\lstinputlisting[label=src:agda-where, caption=Agda における where 句] {src/AgdaWhere.agda}


データ型のコンストラクタには自分自身の型を引数に取ることもできる(リスト~\ref{src:agda-nat})。
自然数のコンストラクタは2つあり、片方は自然数ゼロ、片方は自然数を取って後続数を返すものである。
例えば0 は \verb/zero/ であり、1 は \verb/suc zero/に、3は \verb/suc (suc (suc zero))/ に対応する。

\lstinputlisting[label=src:agda-nat, caption=Agdaにおける自然数の定義] {src/AgdaNat.agda}

自然数に対する演算は再帰関数として定義できる。
例えば自然数どうしの加算は二項演算子\verb/+/としてリスト~\ref{src:agda-plus}のように書ける。

この二項演算子は正確には中置関数である。
前置や後置で定義できる部分を関数名に \verb/_/ として埋め込んでおくことで、関数を呼ぶ時にあたかも前置や後置演算子のように振る舞う。
例えば \verb/!_/ 関数を定義すると \verb/! true/ のように利用でき、\verb/_~/ 関数を定義すると \verb/false ~/ のように利用できる。

また、Agda は再帰関数が停止するかを判定できる。
この加算の二項演算子は左側がゼロに対しては明らかに停止する。
左側が1以上の時の再帰時には \verb/suc n/ から \verb/n/へと減っているため、再帰で繰り返し減らすことでいつかは停止する。
もし \verb/suc n/ のまま自分自身へと再帰した場合、Agda は警告を出す。

\lstinputlisting[label=src:agda-plus, caption=Agda における自然数の加算の定義] {src/AgdaPlus.agda}

次に依存型について見ていく。
依存型で最も基本的なものは関数型である。
依存型を利用した関数は引数の型に依存して返す型を決定できる。

Agda で \verb/(x : A) -> B/ と書くと関数は型 A を持つx を受け取り、Bを返す。
ここで B の中で x を扱っても良い。
例えば任意の型に対する恒等関数はリスト~\ref{src:agda-id}のように書ける。

\lstinputlisting[label=src:agda-id, caption=依存型を持つ関数の定義] {src/AgdaId.agda}

この恒等関数 \verb/identitiy/ は任意の型に適用可能である。
実際に関数 \verb/identitiy/ を Nat へ適用した例が \verb/identitiy-zero/ である。

多相の恒等関数では型を明示的に指定せずとも \verb/zero/ に適用した場合の型は自明に \verb/Nat -> Nat/である。
Agda はこのような推論をサポートしており、推論可能な引数は省略できる。
推論によって解決される引数を暗黙的な引数(implicit arguments) と言い、記号 \verb/{}/ でくくる。

例えば、\verb/identitiy/ の対象とする型\verb/A/を暗黙的な引数として省略するとリスト~\ref{src:agda-implicit-id}のようになる。
この恒等関数を利用する際は特定の型に属する値を渡すだけでその型が自動的に推論される。
よって関数を利用する際は \verb/id-zero/ のように型を省略して良い。
なお、関数の本体で暗黙的な引数を利用したい場合は \verb/{variableName}/ で束縛することもできる(\verb/id'/ 関数)。
適用する場合も \verb/{}/でくくり、\verb/id-true/のように使用する。

\lstinputlisting[label=src:agda-implicit-id, caption=Agdaにおける暗黙的な引数を持つ関数] {src/AgdaImplicitId.agda}

Agda には C における構造体に相当するレコード型も存在する。
定義を行なう際は \verb/record/キーワードの後にレコード名、型、\verb/where/ の後に \verb/field/ キーワードを入れた後、フィールド名と型名を列挙する。
例えば x と y の二つの自然数からなるレコード \verb/Point/ を定義するとリスト~\ref{src:agda-record}のようになる。
レコードを構築する際は \verb/record/ キーワードの後の \verb/{}/ の内部に \verb/fieldName = value/ の形で値を列挙していく。
複数の値を列挙する際は \verb/;/ で区切る。

\lstinputlisting[label=src:agda-record, caption=Agdaにおけるレコード型の定義] {src/AgdaRecord.agda}

構築されたレコードから値を取得する際には \verb/RecordName.fieldName/ という名前の関数を適用する(リスト~\ref{src:agda-record-proj} 内2行目) 。
なお、レコードにもパターンマッチが利用できる(リスト~\ref{src:agda-record-proj} 内5行目)。
また、値を更新する際は \verb/record oldRecord {field = value ; ... }/ という構文を利用する。
Point の中の x の値を5増やす関数 \verb/xPlus5/ はリスト~\ref{src:agda-record-proj}の 7,8行目のように書ける。

\lstinputlisting[label=src:agda-record-proj, caption=Agda におけるレコードの射影、パターンマッチ、値の更新] {src/AgdaRecordProj.agda}

Agda における部分型のように振る舞う機能として Instance Arguments が存在する。
これはとあるデータ型が、ある型と名前を持つ関数を持つことを保証する機能であり、Haskell における型クラスや Java におけるインターフェースに相当する。
Agda における部分型の制約は、必要な関数を定義した record に相当し、その制約を保証するにはその record を instance として登録することになる。
例えば、同じ型と比較することができる、という性質を表すとリスト~\ref{src:agda-type-class}のようになる。
具体的にはとある型 A における中置関数 \verb/_==_/ を定義することに相当する。

\lstinputlisting[label=src:agda-type-class, caption=Agdaにおける部分型制約] {src/AgdaTypeClass.agda}

ある型 T がこの部分型制約を満たすことを示すには、型 T でこのレコードを作成できることを示し、それを instance 構文で登録する。
型Nat が Eq の上位型であることを記述するとリスト~\ref{src:agda-instance}のようになる。

\lstinputlisting[label=src:agda-instance, caption=Agdaにおける部分型関係の構築] {src/AgdaInstance.agda}

これで \verb/Eq/ が要求される関数に対して Nat が適用できるようになる。
例えば型 A の要素を持つ List A から要素を探してくる elem を定義する。
部分型のインスタンスは \verb/{{}}/ 内部に名前と型名で記述する。
なお、名前部分は必須である。
仮に変数として受けても利用しない場合は \verb/_/ で捨てると良い。
部分型として登録した record は関数本体において \verb/{{variableName}}/ という構文で変数に束縛できる。

\lstinputlisting[label=src:agda-use-instance, caption=Agdaにおける部分型を使う関数の定義] {src/AgdaElem.agda.replaced}

この \verb/elem/ 関数はリスト~\ref{src:agda-elem-apply} のように利用できる。
Nat型の要素を持つリストの内部に4が含まれるか確認している。
この \verb/listHas4/ は \verb/true/ に評価される。
なお、 \verb/--/ の後はコメントである。

\lstinputlisting[label=src:agda-elem-apply, caption=部分型を持つ関数の適用] {src/AgdaElemApply.agda.replaced}

最後にモジュールについて述べる。
モジュールはほとんど名前空間として作用する。
なお、依存型の解決はモジュールのインポート時に行なわれる。
モジュールをインポートする時は \verb/import/ キーワードを指定する。
また、インポートを行なう際に名前を別名に変更することもでき、その際は \verb/as/ キーワードを用いる。
モジュールから特定の関数のみをインポートする場合は \verb/using/ キーワードを、関数の名前を変える時は \verb/renaming/キーワードを、特定の関数のみを隠す場合は \verb/hiding/ キーワードを用いる。
なお、モジュールに存在する関数をトップレベルで用いる場合は \verb/open/ キーワードを使うことで展開できる。
モジュールをインポートする例をリスト~\ref{src:agda-import}に示す。

\lstinputlisting[label=src:agda-import, caption=Agdaにおけるモジュールのインポート] {src/AgdaImport.agda}

また、モジュールには値を渡すことができる。
そのようなモジュールは Parameterized Module と呼ばれ、渡された値はそのモジュール内部で一貫して扱える。
例えば要素の型と比較する二項演算子を使って並べ替えをするモジュール\verb/Sort/ を考える。
そのモジュールは引数に型Aと二項演算子 \verb/</を取り、ソートする関数を提供する。
\verb/Sort/モジュールを \verb/Nat/ と \verb/Bool/ で利用した例がリスト~\ref{src:agda-parameterized-module}である。

\lstinputlisting[label=src:agda-parameterized-module, caption=Agda における Parameterized Module] {src/AgdaParameterizedModule.agda}

% }}}

% {{{ Reasoning

\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:agda-nat-2} のようになる。

\lstinputlisting[label=src:agda-nat-2, caption=Agda における自然数型 Nat の定義] {src/Nat.agda}

自然数型 Nat は2つのコンストラクタを持つ。

\begin{itemize}
    \item O

        引数を持たないコンストラクタ。これが0に相当する。

    \item S

        Nat を引数に取るコンストラクタ。これが後続数に相当する。

\end{itemize}

よって、数値の 3 は \verb/S (S (S O))/ のように表現される。
Sの個数が数値に対応する。

次に加算を定義する(リスト\ref{src:agda-nat-add})。

\lstinputlisting[label=src:agda-nat-add, caption=Agdaにおける自然数型に対する加算の定義] {src/NatAdd.agda}

加算は中置関数 \verb/_+_/ として定義する。
2つの Nat を取り、Natを返す。
関数 \verb/_+_/ はパターンマッチにより処理を変える。
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 の定義を用いる。

\lstinputlisting[label=src:agda-equiv, caption= Relation.Binary.Core による等式を示す型 $ \equiv $] {src/Equiv.agda.replaced}
Agda において等式は、等式を示すデータ型 $ \equiv $ により定義される。
$ \equiv $ は同じ両辺が同じ項に簡約される時にコンストラクタ refl で構築できる。

実際に 3 + 1 = 4 の証明は refl で構成できる(リスト\ref{src:agda-three-plus-one})。

\lstinputlisting[label=src:agda-three-plus-one, caption= Agda における 3 + 1 の結果が 4 と等しい証明] {src/ThreePlusOne.agda}

3+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:agda-nat-add-sym})。

\lstinputlisting[label=src:agda-nat-add-sym, caption= Agda における加法の交換法則の証明] {src/NatAddSym.agda}

証明する式は $ n + m \equiv m + n $ である。
n と m は Nat であるため、それぞれがコンストラクタ O か S により構成される。
そのためにパターンは4通りある。

\begin{itemize}
    \item n = O, m = O

        \verb/_+_/ の定義により、 O に簡約されるため refl で証明できる。

    \item n = O, m = S m

        $ O + (S m) \equiv (S m) + O $  を証明することになる。
        この等式は \verb/_+_/ の定義により $ 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/_+_/ の定義により等しい。

        ここで、 \verb/addSym/ に渡される m は1つ値が減っているため、最終的には n = 0, m = 0 である refl にまで簡約され、等式が得られる。

    \item n = S n, m = O

        $ (S n) + O \equiv O + (S n) $ を証明する。
        この等式は \verb/_+_/ の定義により $ S (n + O) \equiv (S n) $ と変形できる。
        さらに変形すれば $ S (n + O) \equiv S (O + n) $ となる。
        よって \verb/addSym/ により O と n を変換した後に cong で S を加えることで証明ができる。

        ここで、 $ O + n  \equiv n $ は \verb/_+_/ の定義により自明であるが、$ n + O \equiv n $ をそのまま導出できないことに注意して欲しい。
        \verb/_+_/ の定義は左側の項から 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:agda-reasoning}である。
特に n と m が1以上である時の証明に注目する。

\lstinputlisting[label=src:agda-reasoning, caption= $ \equiv $ - Reasoning を用いた証明の例] {src/Reasoning.agda.replaced}

まず \verb/ (S n) + (S m)/ は \verb/_+_/ の定義により \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)/を得なくてはならない。
しかし、 \verb/_+_/ の定義には右辺に対して S を移動する演算が含まれていない。
よってこのままでは証明することができない。
そのため、等式 $ S (m + n) \equiv m + (S n) $ を addToRight として定義する。
addToRight はコンストラクタによる分岐を用いて証明できる。
値が0であれば自明に成り立ち、1以上であれば再帰的に addToRight を適用することで任意の数に対して成り立つ。
addToRight を用いることで \verb/S ((S m) + n)/ から \verb/(S m) + (S n)/を得られた。
これで等式 $ (S m) + (S n) \equiv (S n) + (S m) $  の証明が完了した。

自然数に対する + の演算を考えた時にありえるコンストラクタの組み合せ4パターンのいずれかでも交換法則の等式が成り立つことが分かった。
このように、Agda における等式の証明は、定義や等式を用いて右辺と左辺を同じ項に変形することで行なわれる。

% }}}