\chapter{Delta Monad が Monad である証明}
\label{chapter:proof_delta}
第\ref{chapter:agda}章では Agda における証明手法について述べた。
第\ref{chapter:proof_delta}章では Agda を用いて Delta Monad が Monad であることを証明していく。
証明のゴールは Delta Monad が Funcor 則と Monad 則を満たすことの証明である。

% {{{ Agda における Delta Monad の表現

\section{Agda における Delta Monad の表現}
\label{section:delta_in_agda}
\ref{section:delta_in_agda}節では Agda において Delta Monad を再定義する。
Agda は Haskell において実装されているため、ほとんど同様に定義できる(リスト\ref{src:delta_in_agda})。

\begin{table}[html]
    \lstinputlisting[label=src:delta_in_agda, caption=Agdaにおける Delta Monad のデータ定義] {src/delta.agda.replaced}
\end{table}

data型 Delta は型A の値と Nat を持つ。

level とは型のlevelの区別に用いられるものである。
Agda では型も値として扱えるため、同じ式において型と値が混同することがある。
厳密に型と値を区別したい場合、level を定義することで区別する。
levelは任意の level と、関数 suc により定義される。
関数 suc は level を一つ上昇させる関数である。
level l を適用した型を用いる時は Set l と記述する。
今回は証明する対象のプログラムは Set l の level とし、それ以外は Set (suc l) の level とする。

Nat は自然数であり、プログラムのバージョンに対応する。
自然数の定義は\ref{section:reasoning} 節にあるリスト \ref{src:nat}にならうものとする。

data 型 Delta は2つのコンストラクタにより構成される。

\begin{itemize}
    \item mono

        プログラムの最初の変更単位を受けとり、バージョン1とする。
        型Aを取り、バージョンが1のDeltaを構成することでその表現とする。

    \item delta

        変更単位と変更単位の列を受けとり、変更単位を追加する。
        これは変更によるバージョンアップに相当する。
        よって任意の1以上のバージョンを持つ Delta に変更単位を加えることでバージョンを1上昇させる。
\end{itemize}

Agda においてもデータ型 Delta が定義できた。
これからこの定義を用いて Functor則と Monad 則を証明していく。

% }}}

% {{{ Agda における Functor 則

\section{Agda における Functor 則}
\label{section:functor_in_agda}
Agda における Functor 則はリスト \ref{src:record_functor} のように記述した。

\begin{table}[html]
    \lstinputlisting[label=src:record_functor, caption=Agdaにおける Functor則の定義] {src/record_functor.agda.replaced}
\end{table}

Agda ではある性質を持つデータは record 構文によって記述する。
record の値は record の定義時に要請した field を全て満たすことで構築される。
よって、あるデータAが持つべき性質は field に定義し、A を用いた証明によって field を満たす。
field を満たすことにより record が構成できることで A がある性質を満たすことを証明する。

record Funcor は implicit な値 level と、型引数を持つ関数 F を持つ。
record Functor が取る F は Set l を取り Set l を取る関数である。
Set l が証明の対象となるプログラムであるため、関数F はプログラムのlevel で表現する。
よって、プログラムの level l を取り、プログラムの level l の Set を返すようにする。
それに対し、 F に対する証明となる record Functor は、証明の対象とするプログラムそのものではない。
よって suc により level を一段上げる。
これは、証明の対象となるプログラムと証明そのものを混同しないためである。

record Functor の field には以下のようなものがある。

\begin{itemize}
    \item fmap

        Functor に要請される、category から category への map 関数である。
        型の定義はほとんど Haskell と同じである。
        fmap は任意の型に対して適用可能でなくてはいけないため、map する対象の型Aと map される対象の型Bは implicit である。

    \item preserve-id

        Functor則の id の保存である。
        型F A  を持つ値x に対するfmap id と id の等価性がなくてはならない。

    \item covariant

        Functor則における関数の合成の保存である。
        関数fとgを合成してから fmap により mapping しても、 f と g を個別に mapping してから合成しても等価性を持たなくてはならない。

    \item fmap-equiv

        ある型A の値x に対して等価である関数f と g を考えた時、 型F A の値 fx の対し、 fmap f としても fmap gとしても等価であることを保証する。
        これは本来はFunctor則には存在しない。
        Agda において Monad の証明に必要であったために追加した。
\end{itemize}

% }}}

\section{Delta が Functor 則を満たす証明}
\label{section:delta_is_functor}
\ref{section:functor_in_agda}節では Agda における Functor則の表現について述べた。
\ref{section:delta_is_functor}節では

\section{Agda における Monad 則}
\section{Delta が Monad 則を満たす証明}