\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) $ が導けたために証明終了となる。

% }}}

\section{Curry-Howard Isomorphism}
\section{Agda による証明}
\section{Reasoning}