\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}

% }}}

% {{{ Delta が Functor 則を満たす証明

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

まず、Agdaにおける delta に対する fmap の定義を示す(リスト\ref{src:delta_fmap_in_agda})。

\begin{table}[html]
    \lstinputlisting[label=src:delta_fmap_in_agda, caption= Agda における Delta に対する fmap の定義] {src/delta_fmap.agda}
\end{table}

バージョンが1以上の Delta について fmap を定義する。
関数 f は型 A から B への関数とし、 Delta A から Delta B への関数に mapping する。
コンストラクタ2つのパターンマッチを使って再帰的に f を delta の内部の値への適応することで fmap を行なう。

データ型Delta と関数fmap を定義できたので、これらが Functor 則を満たすか証明していく。
なお、今回 Delta は全ての場合においてバージョンを1以上持つものとする。
その制約は引数の Delta のバージョンに必ず S を付けることで1以下の値を受けつけないようにすることで行なう。


\begin{itemize}
    \item fmap は id を保存する

        リスト\ref{src:delta_preserve_id}に証明を示す。

        \begin{table}[html]
            \lstinputlisting[label=src:delta_preserve_id, caption= Delta における fmap も id を保存する証明] {src/delta_preserve_id.agda.replaced}
        \end{table}


        コンストラクタにようてパターン分けをする
        mono の場合はfmapの定義により同じ項に変形されるために relf で証明できる。
        delta の場合、delta の 第一引数は mono の時のように同じ項に変形できる。
        しかし第二引数は fmap の定義により \verb/delta-fmap d id/ に変形される。
        見掛け上は等式の左辺と変わらないように見えるが、先頭1つめを除いているため、引数で受けたバージョンよりも1値が下がっている。
        よって最終的にバージョン1である mono になるまで再帰的に delta-preserve-id 関数を用いて変形した後に cong によって先頭1つめを適用し続けることで証明ができる。

    \item fmap は関数の合成を保存する

        リスト\ref{src:delta_covariant}に証明を示す。

        \begin{table}[html]
            \lstinputlisting[label=src:delta_covariant, caption= Delta における fmap も関数の合成を保存する証明] {src/delta_covariant.agda.replaced}
        \end{table}

        id の保存のように、コンストラクタによるパターンマッチを行なう。
        バージョンが1の場合は同じものに簡約され、1より大きい場合は再帰的に変形することで証明できる。
\end{itemize}

Delta と fmap と2つの証明を用いて Functor record を構成する(リスト\ref{src:delta_is_functor})。


\begin{table}[html]
    \lstinputlisting[label=src:delta_is_functor, caption= Delta が Functor則を満たすことの証明] {src/delta_is_functor.agda.replaced}
\end{table}

record が正しく構成できたため、Delta は Functor 則を満たす。
Agda ではこのように法則とデータの関連付けを行なう。

% }}}

% {{{ Agda における Monad 則

\section{Agda における Monad 則}
\label{section:monad_laws_in_agda}
\ref{section:functor_in_agda}節と\ref{section:delta_is_functor}節では Delta が Functor 則を満たすことの証明を行なった。
\ref{section:monad_laws_in_agda}節では同じように Monad 則の定義を行ない、\ref{section:delta_is_monad}節で証明を行なう。

まずは Monad則の定義を行なう(リスト\ref{src:monad_laws_in_agda})。

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

Monad 則とは $ triple(T, \eta, \mu) $ に対して課すべき制約であった。
そのためまず要素として $ T $ , $ \eta $, $ \mu $ が存在する。
T は Set l を取り Set l を返す型であり、Functor則を満たす。
$ \eta $ は T を増やす関数であり、 $ \mu $ は T を減らす関数である。
これら Monad の構成要素を定義する field である。

次に、$ \eta $ と $ \mu $ は natural transformation である必要がある。
よって field に制約として $ \eta $ と $ \mu $ の natural transformation を定義する。
なお、 field という予約語は複数書いても2つ目以降は無いものとして振る舞う。

ここで、 \verb/ fmap F / という項に注目して欲しい。
値F は Functor T 型を持ち、fmap や2つの証明を内包する。
fmap や証明へのアクセスは \verb/ field-name record-value / と記述する。
例えば、リスト\ref{src:delta_is_functor}で定義した Functor Delta の型を持つ値 \verb/delta-is-functor/ に対して \verb/ fmap delta-is-functor/ とすると関数 delta-fmap が得られる。
つまり、\verb/fmap F f/ とするのは Functor則が証明された F の fmap に関数fを適用することとなる。

最後に $ triple (T, \eta, \mu) $ に対する Monad 則に相当する等式を記述する。
Monad則は可換図として与えられたTに対する演算の可換性と、Tに対する演算の単位元を強制するものであった。
Tに対する演算の可換性は association-law として、単位元の強制は unity-law として記述できる。
unity-law はTに対する演算が右側からか左側からかの二種類があるため、 right-unity-law と left-unity-law に分割した。

これら全ての field を満たすような証明を記述できれば、 $ triple (T, \eta, \mu) $ は Monad であると言える。

% }}}

\section{Delta が Monad 則を満たす証明}
\label{section:delta_is_monad}