\chapter{定理証明支援系言語 Agda}
\label{c:agda}
Agda \cite{agda} とは定理証明支援器であり、関数型言語である。
Agda は依存型という型システムを持ち、型を第一級オブジェクトとして扱うことが可能である。
また、型システムは Curry-Howard 同型対応により命題と型付きラムダ計算が一対一で対応するため
Agda では記述したプログラムを証明することができる。

本章では Agda で証明をするために必要な要素を示し。
また、Agda での証明について説明する。

\section{関数型言語としての Agda}
Agda \cite{agda} は純粋関数型言語である。
Agda は依存型という型システムを持ち、型を第一級オブジェクトとして扱う。

Agda の記述ではインデントが
意味を持ち、スペースの有無もチェックされる。
コメントは \verb/-- comment/ か \verb/{-- comment --}/ のように記述される。
また、\verb/_/でそこに入りうるすべての値を示すことができ、
\verb/?/でそこに入る値や型を不明瞭なままにしておくことができる。

Agda のプログラムは全てモジュール内部に記述される。
そのため、各ファイルのトップレベルにモジュールを定義する必要がある。
トップレベルのモジュールはファイル名と同一になる。

モジュール内で異なるモジュールをインポートする時は \verb/import/ キーワードを指定する。
インポートを行なう際、モジュール内部の関数を別名に変更するには \verb/as/ キーワードを用いる。
他にも、モジュールから特定の関数のみをインポートする場合は \verb/using/ キーワード、
関数名を、関数の名前を変える時は \verb/renaming/キーワードを、特定の関数のみを隠
す場合は \verb/hiding/ キーワードを用いる。
なお、モジュールに存在する関数をトップレベルで用いる場合は \verb/open import/ キーワードを使うことで展開できる。
モジュールをインポートする例を\coderef{src:agda-import}に示す。

\lstinputlisting[label=src:agda-import, caption=モジュールのインポートとオプション] {src/AgdaImport.agda.replaced}


\section{Agda のデータ}
Agda 型をデータや関数に記述する必要がある。
Agda における型指定は \verb/:/ を用いて \verb/name : type/ のように記述する。
データ型は、代数的なデータ構造で、その定義には \verb/data/ キーワードを用いる。
\verb/data/ キーワードの後に \verb/data/ の名前と、型、 \verb/where/ 句を書きインデントを深くし、
値にコンストラクタとその型を列挙する。

\coderef{src:agda-nat}は自然数の型である $\mathbb{N}$ (Natural Number)を例である。

\lstinputlisting[label=src:agda-nat, caption=自然数を表すデータ型 Nat の定義] {src/nat.agda.replaced}

\verb/Nat/ では \verb/zero/ と \verb/suc/ の2つのコンストラクタを持つデータ型である。
\verb/suc/ は $\mathbb{N}$ を受け取って $\mathbb{N}$ を表す再帰的なデータになっており、
\verb/suc/ を連ねることで自然数全体を表現することができる。

$\mathbb{N}$ 自身の型は \verb/Set/ であり、これは Agda が組み込みで持つ「型集合の型」である。
\verb/Set/ は階層構造を持ち、型集合の集合の型を指定するには \verb/Set1/ と書く。
%% \verb/Level/ を用いることで異なる \verb/Set/ を表現できる。

Agda には C 言語における構造体に相当するレコード型というデータも存在する、
例えば \verb/x/ と \verb/y/ の二つの自然数からなるレコード \verb/Point/ を定義する。\coderef{src:agda-record}のようになる。
\lstinputlisting[label=src:agda-record, caption=Agdaにおけるレコード型の定義] {src/AgdaRecord.agda.replaced}
レコードを構築する際は \verb/record/ キーワード後の \verb/{}/ の内部に \verb/FieldName = value/ の形で値を列挙する。
複数の値を列挙するには \verb/;/ で区切る必要がある。


\section{Agda の関数}
Agda での関数は型の定義と、関数の定義をする必要がある。
関数の型はデータと同様に \verb/:/ を用いて \verb/name : type/ に記述するが、入力を受け取り出力返す型として記述される。$\rightarrow$ 、 または\verb/→/ を用いて \verb/input → output/ のように記述される。
関数の定義は型の定義より下の行に、\verb/=/ を使い \verb/name input = output/ のように記述される。

例えば引数が型 \verb/A/ で返り値が型 \verb/B/ の関数は \verb/A → B/ のように書くことができる。
また、複数の引数を取る関数の型は \verb/A → A → B/ のように書ける。
この時の型は \verb/A → (A → B)/のように考えられる。
%% 変数 \verb/x/ を取って true を返す関数 \verb/f/は\tabref{src:agda-function}のようになる。
例として任意の自然数$mathbb{N}$を受け取り、\verb/+1/した値を返す関数は\coderef{src:agda-function}のように定義できる。
\lstinputlisting[label=src:agda-function, caption=Agda における関数定義] {src/agda-func.agda.replaced}


引数は変数名で受けることもでき、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。
これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなものである。
例として自然数$mathbb{N}$の加算を関数で書くと\coderef{agda-plus}のようになる。

\lstinputlisting[label=src:agda-plus, caption=自然数での加算の定義] {src/agda-plus.agda.replaced}
%% \lstinputlisting[label=src:agda-not, caption=Agdaにおける関数 not の定義] {src/AgdaNot.agda.replaced}
\verb/_+_/のように関数名で\verb/_/を使用すると引数がその位置にあることを意味する。

パターンマッチでは全てのコンストラクタのパターンを含む必要がある。
例えば、自然数$mathbb{N}$を受け取る関数では \verb/zero/ と \verb/suc/ の2つのパターンが存在する必要がある。
なお、コンストラクタをいくつか指定した後に変数で受けることもでき、その変数では指定されたもの以外を受けることができる。
例えば\coderef{src:agda-pattern}の減算では初めのパターンで2つ目の引数が\verb/zero/のすべてのパターンが入る。


\lstinputlisting[label=src:agda-pattern, caption=自然数の減算によるパターンマッチの例] {src/agda-pattern.agda.replaced}

Agda には$\lambda$計算が存在している。$\lambda$計算とは関数内で生成できる無名の関数であり、
\verb/\arg1 arg2 → function/ のように書くことができる。
\coderef{agda-function} で例とした \verb/+1/ をラムダ計算で書くと\coderef{src:agda-lambda}の\verb/$\lambda$+1/ように書くことができる。この二つの関数は同一の動作をする。

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

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.replaced}


\section{定理証明支援器としての Agda}
Agda での証明では関数の記述と同様の形で型部分に証明すべき論理式、 $\lambda$ 項部分にそれを満たす証明を書くことで証明を行うことが可能である。
証明の例として Code \coderef{proof} を見る。
ここでの \verb/+zero/ は右から \verb/zero/ を足しても $\equiv$ の両辺は等しいことを証明している。
これは、引数として受けている \verb/y/ が \verb/Nat/ なので、 \verb/zero/ の時と \verb/suc y/ の二つの場合を証明する必要がある。

\verb/y = zero/ の時は両辺が \verb/zero/ とできて、左右の項が等しいということを表す \verb/refl/ で証明することができる。
\verb/y = suc y/ の時は $x \equiv y$ の時 $fx \equiv fy$ が成り立つという \verb/cong/ を使って、y の値を 1 減らしたのちに再帰的に \verb/+zero y/
を用いて証明している。

\lstinputlisting[caption=等式変形の例,label=proof]{src/zero.agda.replaced}
%% \begin{lstlisting}[caption=等式変形の例,label=proof]
%% +zero : { y : ℕ } → y + zero  ≡ y
%% +zero {zero} = refl
%% +zero {suc y} = cong ( λ x → suc x ) ( +zero {y} )
%% \end{lstlisting}

また、他にも $\lambda$ 項部分で等式を変形する構文がいくつか存在している。
ここでは \verb/rewrite/ と $\equiv$\verb/-Reasoning/ の構文を説明するとともに、等式を変形する構文の例として加算の交換則について示す。

\verb/rewrite/ では 関数の \verb/=/ 前に \verb/rewrite 変形規則/ の形で記述し、複数の規則を使う場合は \verb/rewrite/ 変形規則1 \verb/|/ 変形規則2 のように \verb/|/を用いて記述する。
\coderef{agda-rewrite} にある \verb/+-comm/ で \verb/x/ が \verb/zero/ のパターンが良い例である。
ここでは、\verb/+zero/ を利用し、 \verb/zero + y/ を \verb/y/ に変形することで $y \equiv y$となり、左右の項が等しいことを示す \verb/refl/ になっている。

\lstinputlisting[caption=rewrite での等式変形の例,label=agda-rewrite]{src/agda-rewrite.agda.replaced}

\coderef{agda-term-pre}、\coderef{agda-term-mid}、 \coderef{agda-term-post} は$\equiv$\verb/-Reasoning/を用いた等式変形の流れである。
始めに等式変形を始めたいところで \verb/let open/ $\equiv$ \verb/-Reasoning in begin/と記述し、
\verb/変形前/ $\equiv$ $\langle$ \verb/変形規則/ $\rangle$ \verb/変形後/ の形で記述して、
最後に $\blacksquare$ をつけて変形を終える。
この \verb/let open/ から $\blacksquare$ までの流れは1行で記述しても良いし、改行やインデントを含めても良い。
\coderef{agda-term-pre}の例では分からないところを \verb/?/ と置いておき、
\verb/?/ の中で示されている値は下にコメントで示しておく。

\lstinputlisting[caption=等式変形の例1/3,label=agda-term-pre]{src/agda-term1.agda.replaced}
%% \begin{lstlisting}[caption=等式変形の例1/3,label=agda-term-pre]
%% +-suc : {x y : ℕ} → x + suc y ≡ suc (x + y)
%% +-suc {zero} {y} = refl
%% +-suc {suc x} {y} = cong suc (+-suc {x} {y})

%% +-comm : (x y : ℕ) → x + y ≡ y + x
%% +-comm zero y rewrite (+zero {y}) = refl
%% +-comm (suc x) y = let open ≡-Reasoning in
%%   begin
%%   ?0 ≡⟨ ?1 ⟩
%%   ?2 ∎

%% -- ?0 : (suc x) + y
%% -- ?1 : suc x + y ≡ y + suc x
%% -- ?2 : y + (suc x)
%% \end{lstlisting}  

この状態で実行すると \verb/?/ 部分に入る型を Agda が示してくれる。
始めに変形する等式を ?0 に記述し、?1 の中に変形規則を使用することで等式を変形できる。
ここでの方針は \verb/(suc x) + y/ を \verb/suc (x + y)/ 変形してやり、
\verb/y + (suc x)/ も同様に \verb/ suc (x + y)/ の形に変形することで等しさを証明する。
Agda の加算では左側に \verb/suc/ がついていた場合外に \verb/suc/ を出して再帰的に中身と足し算を行うため、
何もせずに \verb/(suc x) + y/ は \verb/suc (x + y)/ に変換できる。
\coderef{agda-term-mid} では \verb/suc (x + y)/ に対して \verb/cong/ で \verb/suc/ を外に出し　\verb/+comm/ を再帰的に利用することで \verb/suc (y + x)/ へ変換している。

\lstinputlisting[caption=等式変形の例2/3,label=agda-term-mid]{src/agda-term2.agda.replaced}
%% \begin{lstlisting}[caption=等式変形の例2/3,label=agda-term-mid]
%% +-comm : (x y : ℕ) → x + y ≡ y + x
%% +-comm zero y rewrite (+zero {y}) = refl
%% +-comm (suc x) y = let open ≡-Reasoning in
%%   begin
%%   (suc x) + y ≡⟨⟩
%%   suc (x + y) ≡⟨ cong suc (+-comm x y) ⟩
%%   suc (y + x) ≡⟨ ?0 ⟩
%%   ?1 ∎

%% -- ?0 : suc (y + x) ≡ y + suc x
%% -- ?1 : y + suc x

%% \end{lstlisting}



\coderef{agda-term-post} では \verb/suc (y + x)/ $equiv$ \verb/y + (suc x)/ という等式に対して $equiv$ の対称律 \verb/sym/ を使って左右の項を反転させ\verb/y + (suc x)/ $equiv$ \verb/suc (y + x)/の形にし、\verb/y + (suc x)/が\verb/suc (y + x)/ に変形できることを \verb/+-suc/ を用いて示した。
これにより等式の左右の項が等しくなったため \verb/+-comm/ が示せた。
\lstinputlisting[caption=等式変形の例3/3,label=agda-term-post]{src/agda-term3.agda.replaced}
%% \begin{lstlisting}[caption=等式変形の例2/2,label=agda-term-post]
%% +-comm : (x y : ℕ) → x + y ≡ y + x
%% +-comm zero y rewrite (+zero {y}) = refl
%% +-comm (suc x) y = let open ≡-Reasoning in
%%   begin
%%   suc (x + y) ≡⟨⟩
%%   suc (x + y) ≡⟨ cong suc (+-comm x y) ⟩
%%   suc (y + x) ≡⟨ sym (+-suc {y} {x}) ⟩
%%   y + suc x ∎

%% -- +-suc : {x y : ℕ} → x + suc y ≡ suc (x + y)
%% -- +-suc {zero} {y} = refl
%% -- +-suc {suc x} {y} = cong suc (+-suc {x} {y})
%% \end{lstlisting}
Agda ではこのような形で等式を変形しながら証明を行う事ができる。

%% 例として先程の \verb/+-comm/ を rewrite で証明した \verb/rewrite-+-comm/ を \coderef{agda-rewrite} を載せる。