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

本章では Agda で証明をするために必要な要素について説明を行う。
また、定理証明支援器としての Agda について解説する。

\section{Agda の文法}

Agda はインデントが意味を持ち、スペースの有無もチェックされる。
コメントは \verb/-- comment/ や \verb/{-- comment --}/ のように記述される。

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

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

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


\section{Agda のデータ}
Agda における型指定は : を用いて行う。 変数 x が型 A を持つ、ということを表すには x : A と記述する。
データ型は、代数的なデータ構造で、その定義には data キーワードを用いる。
data キーワードの後に data の名前と、型、 where 句を書きインデントを深くした後、
値にコンストラクタとその型を列挙する。

例えば Bool 型を定義するとリスト~\ref{src:agda-bool}のようになる。
Bool はコンストラクタ \verb/true/ と \verb/false/ を持つデータ型である。
Bool 自身の型は \verb/Set/ であり、これは Agda が組み込みで持つ「型集合の型」である。
Set は階層構造を持ち、型集合の集合の型を指定するには Set1 と書く

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


Agda には C における構造体に相当するレコード型というデータも存在する、
例えば 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}


\section{Agda の関数}

Agda での関数の定義は、関数名と型を記述した後に関数の本体を \verb/=/ の後に記述する。
関数の型には $ \rightarrow $ 、 または\verb/->/ を用いる。

例えば引数が型 \verb/A/ で返り値が型 \verb/B/ の関数は \verb/A -> B/ のように書くことができる。
また、複数の引数を取る関数の型は \verb/A -> A -> B/ のように書ける。この
時の型は \verb/A -> (A -> B)/のように考えられる。
Bool 変数 \verb/x/ を取って true を返す関数 \verb/f/はリスト~\ref{src:agda-function}のようになる。

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

引数は変数名で受けることもでき、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。
これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなもので
例えば Bool 型の値を反転する \verb/not/ 関数を書くとリスト~\ref{src:agda-not}のようになる。

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

パターンマッチでは全てのコンストラクタのパターンを含まなくてはならない。
例えば、Bool 型を受け取る関数で \verb/true/ の時の挙動のみを書くことはできない。
なお、コンストラクタをいくつか指定した後に変数で受けると、変数が持ちうる値は指定した以外のコンストラクタとなる。
例えばリスト~\ref{src:agda-pattern}の not は x には true しか入ることは無い。
なお、マッチした値以外の挙動をまとめて書く際には \verb/_/ を用いることもできる。

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

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}

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}


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

$y = zero$ の時は両辺が zero とできて、左右の項が等しいということを表す refl で証明することができる。
$y = suc y$ の時は x == y の時 fx == fy が成り立つという cong を使って、y の値を 1 減らしたのちに再帰的に $+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$ 項部分で等式を変形する構文が存在している。
 Code \ref{agda-term-pre}、 \ref{agda-term-post} は等式変形の例である。
始めに等式変形を始めたいところで $let open \equiv-Reasoning  in begin$と記述する。
Agda 上では分からないところを ? と置いておくことができるので、残りを ? としておく。
$--$ は Agda 上ではコメントである。

\lstinputlisting[caption=等式変形の例1/2,label=agda-term-pre]{src/term1.agda.replaced}
%% \begin{lstlisting}[caption=等式変形の例1/3,label=agda-term-pre]
%% stmt2Cond : {c10 : ℕ} → Cond
%% stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0)

%% lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c\
%% 10})
%% lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning  in
%%   begin
%%     ?      -- ?0
%%   ≡⟨ ? ⟩  -- ?1
%%     ?      -- ?2
%%   ∎ )

%% -- ?0 : Bool
%% -- ?1 : stmt2Cond (record { varn = varn env ; vari = 0 }) ≡ true
%% -- ?2 : Bool
%% \end{lstlisting}  

この状態で実行すると  ? 部分に入る型を Agda が示してくれる。
始めに変形する等式を ?0 に記述し、?1 の中に $x == y$ のような変形規則を入れることで等式を変形して証明することができる。

ここでは \ref{agda-term-mid} の Bool 値 x を受け取って $x \wedge true$ の時必ず x であるという証明 $\wedge$true と 値と Env を受け取って Bool 値を返す stmt1Cond を使って等式変形を行う。
\lstinputlisting[caption=使っている等式変形規則,label=agda-term-mid]{src/term2.agda.replaced}
%% \begin{lstlisting}[caption=等式変形の例2/3,label=agda-term-mid]
%% ∧true : { x : Bool } →  x  ∧  true  ≡ x
%% ∧true {x} with x
%% ∧true {x} | false = refl
%% ∧true {x} | true = refl

%% stmt1Cond : {c10 : ℕ} → Cond
%% stmt1Cond {c10} env = Equal (varn env) c10
%% \end{lstlisting}

最終的な証明は\ref{agda-term-post} のようになる。
\lstinputlisting[caption=等式変形の例2/2,label=agda-term-post]{src/term3.agda.replaced}
%% \begin{lstlisting}[caption=等式変形の例2/2,label=agda-term-post]
%% lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c\
%% 10})
%% lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning  in
%%   begin
%%     (Equal (varn env) c10 ) ∧ true
%%   ≡⟨ ∧true ⟩
%%     Equal (varn env) c10
%%   ≡⟨ cond ⟩
%%     true
%%   ∎ )
%% \end{lstlisting}