# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1423794706 -32400
# Node ID 470d997993982f25af66d868d5b0087e35e79b28
# Parent  8a70394e45b43435339392f34429eb916c3bb209
Add description functor record

diff -r 8a70394e45b4 -r 470d99799398 agda.tex
--- a/agda.tex	Thu Feb 12 18:08:01 2015 +0900
+++ b/agda.tex	Fri Feb 13 11:31:46 2015 +0900
@@ -1,4 +1,4 @@
-\chapter{Agda による証明手法}
+\chapter{証明支援系言語 Agda による証明手法}
 \label{chapter:agda}
 第\ref{chapter:category}章においては functor, natural transformation, monad の定義と functional programming における対応について述べた。
 その中で、 Functor 則や Monad 則といった満たすべき性質がいくつか存在した。
diff -r 8a70394e45b4 -r 470d99799398 main.tex
--- a/main.tex	Thu Feb 12 18:08:01 2015 +0900
+++ b/main.tex	Fri Feb 13 11:31:46 2015 +0900
@@ -9,7 +9,7 @@
 \usepackage[utf8]{inputenc}
 
 \setlength{\itemsep}{-1zh}
-\title{圏によるプログラムの変更の形式化}
+\title{プログラムの変更の圏による形式化}
 \icon{
     \includegraphics[width=80mm,bb=0 0 595 642]{fig/ryukyu.pdf}
 }
diff -r 8a70394e45b4 -r 470d99799398 proof_delta.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/proof_delta.tex	Fri Feb 13 11:31:46 2015 +0900
@@ -0,0 +1,71 @@
+\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 における 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 を持つ。
+level とは型のlevelの区別に用いられるものである。
+Agda では型も値として扱えるため、同じ式において型と値が混同することがある。
+厳密に型と値を区別したい場合、level を定義することで区別する。
+levelは任意の level と、関数 suc により定義される。
+関数 suc は level を一つ上昇させる関数である。
+level l を適用した型を用いる時は Set l と記述する。
+
+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 則を満たす証明}
diff -r 8a70394e45b4 -r 470d99799398 src/record_functor.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/record_functor.agda	Fri Feb 13 11:31:46 2015 +0900
@@ -0,0 +1,11 @@
+record Functor {l : Level} (F : Set l -> Set l) : Set (suc l) where
+ field
+  fmap : {A B : Set l} -> (A -> B) -> (F A) -> (F B)
+ field -- laws
+  preserve-id : {A : Set l} (x : F A) → fmap id x ≡ id x
+  covariant   : {A B C : Set l} (f : A -> B) -> (g : B -> C) -> (x : F A)
+                   -> fmap (g ∙ f) x ≡ ((fmap g) ∙ (fmap f)) x
+ field -- proof assistant
+  fmap-equiv : {A B : Set l} {f g : A -> B} ->
+    ((x : A) -> f x ≡ g x) -> (fx : F A) -> fmap f fx ≡ fmap g fx
+