# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1423815203 -32400
# Node ID 4cc65012412f6369eb1ff585a9500cd9970db77d
# Parent  8fc2ac1f901f43fb07210fd63ccd9fa5730314b0
Add proofs of functor-laws on delta

diff -r 8fc2ac1f901f -r 4cc65012412f proof_delta.tex
--- a/proof_delta.tex	Fri Feb 13 11:48:40 2015 +0900
+++ b/proof_delta.tex	Fri Feb 13 17:13:23 2015 +0900
@@ -99,10 +99,68 @@
 
 % }}}
 
+% {{{ 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_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 record を構成する] {src/delta_is_functor.agda.replaced}
+\end{table}
+
+record が正しく構成できたため、Delta は Functor 則を満たす。
+Agda ではこのように法則とデータの関連付けを行なう。
+
+% }}}
 
 \section{Agda における Monad 則}
 \section{Delta が Monad 則を満たす証明}
diff -r 8fc2ac1f901f -r 4cc65012412f replace_agda.rb
--- a/replace_agda.rb	Fri Feb 13 11:48:40 2015 +0900
+++ b/replace_agda.rb	Fri Feb 13 17:13:23 2015 +0900
@@ -2,6 +2,7 @@
 
 replace_table = {
   '∙'  => 'circ',
+  '≡' => 'equiv',
   '×' => 'times',
   '⟨'  => 'langle',
   '⟩'  => 'rangle',
diff -r 8fc2ac1f901f -r 4cc65012412f src/delta_covariant.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/delta_covariant.agda	Fri Feb 13 17:13:23 2015 +0900
@@ -0,0 +1,6 @@
+delta-covariant : {l : Level} {n : Nat} {A B C : Set l} ->
+            (f : B -> C) -> (g : A -> B) -> (d : Delta A (S n)) ->
+            (delta-fmap (f ∙ g)) d ≡ ((delta-fmap f) ∙ (delta-fmap g)) d
+delta-covariant f g (mono x)    = refl
+delta-covariant f g (delta x d) = cong (delta (f (g x)))
+                                       (delta-covariant f g d)
diff -r 8fc2ac1f901f -r 4cc65012412f src/delta_fmap.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/delta_fmap.agda	Fri Feb 13 17:13:23 2015 +0900
@@ -0,0 +1,4 @@
+delta-fmap : {l : Level} {A B : Set l} {n : Nat} ->
+             (A -> B) -> (Delta A (S n)) -> (Delta B (S n))
+delta-fmap f (mono x)    = mono  (f x)
+delta-fmap f (delta x d) = delta (f x) (delta-fmap f d)
diff -r 8fc2ac1f901f -r 4cc65012412f src/delta_is_functor.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/delta_is_functor.agda	Fri Feb 13 17:13:23 2015 +0900
@@ -0,0 +1,6 @@
+delta-is-functor : {l : Level} {n : Nat} ->
+                    Functor {l} (\A -> Delta A (S n))
+delta-is-functor = record { fmap       = delta-fmap
+                          ; preserve-id = delta-preserve-id
+                          ; covariant  = \f g -> delta-covariant g f
+                          ; fmap-equiv = delta-fmap-equiv }
diff -r 8fc2ac1f901f -r 4cc65012412f src/delta_preserve_id.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/delta_preserve_id.agda	Fri Feb 13 17:13:23 2015 +0900
@@ -0,0 +1,4 @@
+delta-preserve-id :  {l : Level} {A : Set l} {n : Nat} -> 
+    (d : Delta A (S n)) -> (delta-fmap id) d ≡ id d
+delta-preserve-id (mono x)    = refl
+delta-preserve-id (delta x d) = cong (delta x) (delta-preserve-id d)