# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1423966679 -32400
# Node ID 1b688e70f2a8dacaabb66bc0228e26f8a6790600
# Parent  12c5e455fe55335d9d74c6a26a2caedbc80d3075
Move proofs to appendix

diff -r 12c5e455fe55 -r 1b688e70f2a8 appendix.tex
--- a/appendix.tex	Sun Feb 15 10:33:47 2015 +0900
+++ b/appendix.tex	Sun Feb 15 11:17:59 2015 +0900
@@ -1,2 +1,6 @@
+\appendix
+
+\input{proof_delta}
+% \input{proof_deltaM}
 % TODO: 実験環境
 % TODO: Delta と DeltaM の本体
diff -r 12c5e455fe55 -r 1b688e70f2a8 delta_with_monad.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/delta_with_monad.tex	Sun Feb 15 11:17:59 2015 +0900
@@ -0,0 +1,4 @@
+\chapter{任意の Monad と Delta の組み合せ}
+\section{Monad と組み合せた Delta である DeltaM の定義}
+\section{DeltaM を用いたプログラムの例}
+
diff -r 12c5e455fe55 -r 1b688e70f2a8 main.tex
--- a/main.tex	Sun Feb 15 10:33:47 2015 +0900
+++ b/main.tex	Sun Feb 15 11:17:59 2015 +0900
@@ -70,18 +70,15 @@
 \listoftables       % 表目次
 \lstlistoflistings  % ソースコード目次
 
-
+% 本文
 \input{introduction}
 \pagenumbering{arabic}
 \input{delta}
 \input{category}
 \input{functional_programming}
 \input{agda}
-\input{proof_delta}
+\input{delta_with_monad.tex}
 
-\chapter{任意の Monad と Delta の組み合せ}
-\section{Monad と組み合せた Delta である DeltaM の定義}
-\section{DeltaM が Monad 則を満たす証明}
 
 % 今後の課題
 \input{future.tex}
diff -r 12c5e455fe55 -r 1b688e70f2a8 proof_delta.tex
--- a/proof_delta.tex	Sun Feb 15 10:33:47 2015 +0900
+++ b/proof_delta.tex	Sun Feb 15 11:17:59 2015 +0900
@@ -232,6 +232,7 @@
 
 Delta Monad に対応する $ triple (T, \eta, \mu ) $ が定義できた。
 これから Monad 則を満たすことを証明していく。
+% TODO: layout
 
 \begin{enumerate}
     \item  $ \eta $ が natural transformation であること
@@ -268,6 +269,11 @@
 
     \item T に対する演算の単位元が存在する
 
+        図\ref{fig:monad_laws}で示した右側の可換図に相当する。
+        単位元に相当する演算は右側と左側の2つが存在するため、証明も2つに分割する。
+
+        右側単位元の証明をリスト\ref{src:delta_right_unity_law}に示す。
+
 \begin{table}[html]
     \lstinputlisting[basicstyle={\scriptsize},
                      numberstyle={\tiny},
@@ -276,6 +282,11 @@
                      {src/delta_right_unity_law.agda.replaced}
 \end{table}
 
+        バージョンが1である時は同じ項となるため refl となる。
+        バージョンが1以上である時は再帰的に定義することになるが、途中で $ \eta $ が natural transformation である性質を利用している。
+
+        次に左側単位元の証明をリスト\ref{src:delta_left_unity_law}に示す。
+
 \begin{table}[html]
     \lstinputlisting[basicstyle={\scriptsize},
                      numberstyle={\tiny},
@@ -284,8 +295,13 @@
                      {src/delta_left_unity_law.agda.replaced}
 \end{table}
 
+        これまでの証明と同様にバージョンが1である場合は定義から同じ項となる。
+        バージョンが1以上の場合、Functor則の関数の合成の保存を利用して証明を再帰的に行なう。
+
     \item T に対する演算の可換性が存在する
 
+        図\ref{fig:monad_laws}で示した左側の可換図に相当する。
+
 \begin{table}[html]
     \lstinputlisting[basicstyle={\scriptsize},
                      numberstyle={\tiny},
@@ -296,5 +312,3 @@
 
 \end{enumerate}
 
-
-
diff -r 12c5e455fe55 -r 1b688e70f2a8 proof_deltaM.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/proof_deltaM.tex	Sun Feb 15 11:17:59 2015 +0900
@@ -0,0 +1,2 @@
+\section{DeltaM が Monad 則を満たす証明}
+
diff -r 12c5e455fe55 -r 1b688e70f2a8 src/delta_association_law.agda
--- a/src/delta_association_law.agda	Sun Feb 15 10:33:47 2015 +0900
+++ b/src/delta_association_law.agda	Sun Feb 15 11:17:59 2015 +0900
@@ -26,7 +26,7 @@
 
 delta-association-law : {l : Level} {A : Set l} {n : Nat} (d : Delta (Delta (Delta A (S n)) (S n)) (S n)) ->
               ((delta-mu ∙ (delta-fmap delta-mu)) d) ≡ ((delta-mu ∙ delta-mu) d)
-delta-association-law {n =       O} (mono d)                          = refl
+delta-association-law {n =   O} (mono d)                          = refl
 delta-association-law {n = S n} (delta (delta (delta x d) dd) ds) = begin
   delta x (delta-mu (delta-fmap tailDelta (delta-fmap delta-mu ds)))
   ≡⟨ cong (\de -> delta x (delta-mu de)) (delta-fmap-mu-to-tail n n ds) ⟩