--- a/.hgignore	Tue Feb 10 11:38:36 2015 +0900
+++ b/.hgignore	Tue Feb 10 12:48:02 2015 +0900
@@ -3,6 +3,7 @@
 .DS_Store
 
 *.swp
+*.*~
 
 *.lof
 *.lol
@@ -13,4 +14,7 @@
 *.toc
 *.cpt
 
+*.agdai
+*.agda~
+
 main.pdf

--- a/agda.tex	Tue Feb 10 11:38:36 2015 +0900
+++ b/agda.tex	Tue Feb 10 12:48:02 2015 +0900
@@ -299,6 +299,68 @@
 
 % }}}
 
+% {{{ Agda による証明
+
 \section{Agda による証明}
+\ref{section:curry_howard_isomorphism}節において型を用いて証明を行なう手法を述べた。
+しかし、Haskell における型システムは証明を記述するために用いるものではない。
+よって、依存型を持つ証明支援言語 Agda を用いて証明を記述していく。
+
+依存型とは値に依存した型を作ることができる型であり、非常に表現能力が高い。
+値に型を使うことができるために証明に基づいた証明を記述することができる。
+
+$ \Rightarrow \mathcal{E} $ に対応する関数適用を Agda で記述するとリスト\ref{src:apply_function_in_agda}のようになる。
+
+\begin{table}[html]
+    \lstinputlisting[label=src:apply_function_in_agda, caption=Agda における $ \Rightarrow \mathcal{E} $ ] {src/apply_function.agda}
+\end{table}
+
+Agda による型注釈は \verb/ term : type/ と記述する。
+postulate とすると alive な証明を記述することができる。
+まずは alive な A を仮定している。
+なお、Set 型は型の型として組込みで用意されている型である。
+そのため詳細は省略するが、 A は型であると考える。
+
+次に関数 f を仮定する。
+仮定に用いられている記号 \verb/{}/ の内部の式は implicit な paramter である。
+任意の B の対してこの型が成り立つことを記述している。
+implicit な parameter は可能であれば Agda が推論する。
+そのため、f の見掛け上の型は \verb/A -> B/のようになる。
+ここで、 B に明示的に値を代入することで f の型を変更することもできる。
+このように Agda では型における引数のようなものが存在し、型の表現能力が高い。
+
+A と f の2つを仮定したところで、証明である \verb/->E/を定義する。
+証明するべき式は \verb/->E/ の型として与えられ、証明は \verb/->E/ の式として記述する。
+式の型に対する定義を正しく行なうことで証明を与える。
+
+$ \Rightarrow \mathcal{E} $ に対応する \verb/->E/ は関数の適用なので、値a と関数 f を受けとって適用することで B が得られる。
+なお、仮定を alive のまま証明を記述するのは依存した仮定を残すことになるため、必要な仮定を引数として受けとったり、implicit な parameter として指定して証明するのが良い。
+
+また、Agda は証明に用いる規則なども Agda 内部で定義することができる。
+例えば、直積型の定義はリスト\ref{src:product}のようなものがある。
+
+\begin{table}[html]
+    \lstinputlisting[label=src:product, caption=Agdaにおける直積型の例] {src/product.agda}
+\end{table}
+
+関数の定義時に \verb/_/ とした部分には項を入れることで関数が適用される。
+つまり \verb/_x_/ とすれば中置関数を作成することができる。
+データ型 \verb/_x_/ は型 A と B を持つ型である。
+データ型 \verb/_x_/ はコンストラクタ \verb/<_,_>/ により構成され、コンストラクタは A と B を取ることで \verb/A x B/ 型を返す。
+
+例えば型A と B から 直積型 $ A \times B $ が作成できる証明は constructProduct である。
+任意の型AとBを受けとり、コンストラクタ \verb/<_,_>/を用いて $ A \times B $ に相当する \verb/A x B/を返す。
+
+また、型に対応するコンストラクタはパターンマッチにより分解することができる。
+その例が patternMatchProduct である。
+受けとる引数の型は \verb/ A x B/ であるため、ありえるコンストラクタは \verb/<_,_>/のみである。
+よって引数を取る際に \verb/< a , b >/ のように対応するコンストラクタと変数を用意することで、コンストラクタに基づいて型を分解することができる。
+\verb/A x B/ 型から B を取るため、\verb/A x B/ 型の変数を直接束縛せずにコンストラクタで分解し、a と b に束縛することで A と B が得られる。
+そのため、 patternMathProduct は $ \land 2 \mathcal{E} $ そのものである。
+
+% }}}
+
+
 \section{Reasoning}
 
+% TODO: nat かなー

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/apply_function.agda	Tue Feb 10 12:48:02 2015 +0900
@@ -0,0 +1,7 @@
+module apply_function where
+
+postulate A : Set 
+postulate f : {B : Set} -> A -> B
+
+->E : {B : Set} -> A -> (A -> B) -> B
+->E a f = f a
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/product.agda	Tue Feb 10 12:48:02 2015 +0900
@@ -0,0 +1,10 @@
+module product where
+
+data _x_ (A B : Set) : Set where
+  <_,_> : A -> B -> A x B
+
+constructProduct : {A B : Set} -> A -> B -> A x B
+constructProduct a b = < a , b >
+
+patternMatchProduct : {A B : Set} -> A x B -> B
+patternMatchProduct (< a , b >) = b
\ No newline at end of file