\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 による証明}
\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} $ そのものである。

% }}}


\section{Reasoning}

% TODO: nat かなー