# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1385976616 -32400
# Node ID c813019c37ffaac4b5cab8592d0d1a28f08d2f5c
# Parent  576a3272522d94eb028888dcc5b8e14f0736a9b8
on going...

diff -r 576a3272522d -r c813019c37ff agda-prog.ind
--- a/agda-prog.ind	Sun Dec 01 17:58:05 2013 +0900
+++ b/agda-prog.ind	Mon Dec 02 18:30:16 2013 +0900
@@ -253,17 +253,17 @@
 % 
 % emacs との連携
 
+ここでは Agda をざっと概観する。例えば、\cite{} の論文がわかりやすい。
 Agda は Haskell と同じような構文を持つλ式の集合である。例えば、Agda の append は以下のようになる。
 
-
     infixr 40 _::_
-    data  List  (A : Set ) : Set  where
+    data  List {a} (A : Set a) : Set a where
        [] : List A
        _::_ : A → List A → List A
 
 
     infixl 30 _++_
-    _++_ :   {A : Set } → List A → List A → List A
+    _++_ : ∀ {a} {A : Set a} → List A → List A → List A
     []        ++ ys = ys
     (x :: xs) ++ ys = x :: (xs ++ ys)
 
@@ -285,17 +285,217 @@
 
 ここでは型には ( 変数名 : 型名 ) による型の要素の定義と、(入力型→出力型)で表される関数の二種類がある。
 
+{a} は、暗黙の引数であり、呼び出す時に省略することができる。ここでは、集合のレベルを暗黙に与えている。
+∀ は飾りであるが任意の a に付いて成り立つことを意味している。
+
+Agda では集合のパラドックスを避けるために集合の集合は一つの上のレベルの集合になる。Set a はレベルaの
+集合になる。Set (suc a) は、Set a の一つ上のレベルの集合を表す。ここでは、任意のレベルの集合に対する
+List を定義している。
+
+infixl, infixr が中置き演算子であり、_  が引数の位置を表す。a ++ b の演算子は _++_ であり、_++_ a b  と同じものを表している。
+
+---data型を使った等号
+
+Agda には、さまざまな等号や関係が定義されるが、同じ物を表すのには data 型が使われる。
+
+    infixr 20  _==_
+
+    data _==_  {A : Set } :  List A → List A → Set  where
+          reflection  : {x : List A} → x == x
+
+同じ物を二つ並べて作られるデータ構造が reflection を提供する。これは等号の反射率 a= a に相当する。
+data の filed の reflection は、等号のコンストラクタだと考えることができる。つまり、a を与えると、
+a == a というデータ構造を返す。これは、a == a の証明に対応するλ式でもあって、Curry Haward 対応に
+相当する。
+
+これは、実際には、Relation.Binary.PropositionalEquality で定義されているので、自分で定義する必要はない。
+
+data 型の他に record 型あり、この append の例題では使わないが、排他的和を表すデータ構造を提供し、圏や関手を定義することができる。
 
 
 --Agda での証明方法
 
-? の使い方
+Agda は Emacs と連携して使用されることが想定されている。Emacs が backend である agda を起動して、Emacs 上で操作を行う。
+
+--- ? の使い方
+
+
+Agda では、まず、ファイルを読み込み C-L (agda2-load)とすると、 全体の型がチェックされ、色で識別される。
+
+<img src="fig/agda-list-1.png">
+ 
+定義した式の一部を ? で置き換えると、そこに必要な型を示してくれる。
+
+--List の append の結合法則の証明
+
+証明には、まず証明するべき式を型として定義する。この型を与えるλ式が証明になるのが Curry Howard 対応である。
+
+    list-assoc : {A : Set } → ( xs ys zs : List A ) →
+         ( ( xs ++ ys ) ++ zs ) == ( xs ++ ( ys ++ zs ) )
+    list-assoc  = ?
+
+list-assoc は、入力として A の list を取る。そして、結合法則を表す等式(を表したデータ構造 _==_ )を返す。_==_ は、同じものからしか作ることはできない。
+
+? は、
+
+    ?0 : {A₁ : Set} (xs ys zs : List A₁) →
+        xs ++ ys ++ zs == xs ++ (ys ++ zs)
+
+だと Agda が教えてくれるが、これは、証明すべき型を返しているだけで証明のヒントにはならない。
+
+List は、二つのfieldを持つデータ構造なので、それを場合分けすることができる。
+
+    list-assoc  [] ys zs = ?
+    list-assoc  (x :: xs)  ys zs = ?
+
+これは、Haskell のパターンマッチと同じ構文である。今度は、
+
+    ?0 : [] ++ ys ++ zs == [] ++ (ys ++ zs)
+    ?1 : x :: xs ++ ys ++ zs == x :: xs ++ (ys ++ zs)
+
+となる。?0 の方は、_++_ の定義( [] ++ ys = ys )から ys ++ zs になる。これは、Emacs の ?0 上にカーソルを合わせて、
+
+    \ys zs -> [] ++ ys ++ zs
+    \ys zs -> [] ++ (ys ++ zs)
+
+を、それぞれ C-n ( normalize ) すると、両方、
 
-数式変形
+    λ ys₁ zs₁ → ys₁ ++ zs₁
+
+となる。つまり両辺は同じものなので、_==_ のコンストラクタ reflection を使って生成できる。
+
+    list-assoc  [] ys zs = reflection
+
+つまり、 list-assoc  [] ys zs の型を生成するのが reflection であり、list-assoc  [] ys zs は ys ++ zs == ys ++ zs でもある。
+
+    ?1 : x :: xs ++ ys ++ zs == x :: xs ++ (ys ++ zs)
+
+の方は、_++_ のもう一つのパターンを使う必要がある。こちらの両辺は、C-n を使っても
+
+    λ x₁ xs₁ ys₁ zs₁ → x₁ :: (xs₁ ++ ys₁ ++ zs₁)
+    λ x₁ xs₁ ys₁ zs₁ → x₁ :: (xs₁ ++ (ys₁ ++ zs₁))
+
+となり、そのままでは同じにはならない。しかし、:: の後ろの部分が証明するべき式と同じであることはわかる。
+List は一つ短くなっているので、これを既に証明されている式とみなして良い。[] の場合の証明は終わっているので、
+帰納法の基点は証明されている。つまり、後ろの部分、
+
+    (xs₁ ++ ys₁ ++ zs₁) == (xs₁ ++ (ys₁ ++ zs₁))
+
+は list-assoc xs₁ ys₁ zs₁ そのものになる。あとは、同じものに xs₁ を append しても同じであることが証明できれば良い。つまり、
+
+    eq-cons :  ∀{n} {A : Set n} {x y : List A} ( a : A ) → x ==  y → ( a :: x ) == ( a :: y )
+
+を証明できれば良い。
+
+そのためには、congluence を使う。これは、同じ入力に同じ関数を作用させても同じになるという定理になる。これは、以下のように証明される。
+
+    cong1 : ∀{a} {A : Set a } {b} { B : Set b } →
+       ( f : List A → List B ) → {x : List A } → {y : List A} → x == y → f x == f y
+    cong1 f reflection = reflection
+
+ここで、cong1 の最初の引数は作用させる関数f で、二つ目の引数は x == y という式である。x == y は _==_ のデータ構造で、
+reflection という field を持っている。
+
+    cong1 f reflection 
+
+は、
+
+    list-assco [] ys zs
+
+と同じパターンマッチングになる。reflection の型は x == x なので、x == y とマッチした時に、x と y は単一化されて同じものになる。
+同じものなので、
 
-数式変形の記述
+   f x == f x 
+
+という型を reflection によって作ることができる。これで cong1 の証明ができたことになる。
+
+f に λ x → ( a :: x ) を使うと eq-cons を証明できる。
+
+    eq-cons :  ∀{n} {A : Set n} {x y : List A} ( a : A ) → x ==  y → ( a :: x ) == ( a :: y )
+    eq-cons a z = cong1 ( λ x → ( a :: x) ) z
+
+最終的な証明は、
+
+    list-assoc : {A : Set } → ( xs ys zs : List A ) →
+         ( ( xs ++ ys ) ++ zs ) == ( xs ++ ( ys ++ zs ) )
+    list-assoc  [] ys zs = reflection
+    list-assoc  (x :: xs)  ys zs = eq-cons x ( list-assoc xs ys zs )
+
+という形になる。残念ながら、これは人に読みやすいとは言えないが、Agda では推論規則による数式変形という形で読みやすい形にすることが可能になっている。
+
+--数式変形
+
+数式変形を使うと、この証明は以下のようになる。
+
+    ++-assoc : ∀{n} (L : Set n) ( xs ys zs : List L ) → (xs ++ ys) ++ zs  == xs ++ (ys ++ zs)
+    ++-assoc A [] ys zs = let open ==-Reasoning A in
+      begin -- to prove ([] ++ ys) ++ zs  == [] ++ (ys ++ zs)                                                                                     
+       ( [] ++ ys ) ++ zs
+      ==⟨ reflection ⟩
+        ys ++ zs
+      ==⟨⟩
+        [] ++ ( ys ++ zs )
+      ∎
+
+    ++-assoc A (x :: xs) ys zs = let open  ==-Reasoning A in
+      begin -- to prove ((x :: xs) ++ ys) ++ zs == (x :: xs) ++ (ys ++ zs)                                                                        
+        ((x :: xs) ++ ys) ++ zs
+      ==⟨⟩
+         (x :: (xs ++ ys)) ++ zs
+      ==⟨⟩
+        x :: ((xs ++ ys) ++ zs)
+      ==⟨ cong1 (_::_ x) (++-assoc A xs ys zs) ⟩
+        x :: (xs ++ (ys ++ zs))
+      ==⟨⟩
+        (x :: xs) ++ (ys ++ zs)
+      ∎
 
-数式変形用に ? を使う
+数式が ==⟨ cong1 (_::_ x) (++-assoc A xs ys zs) ⟩ などで変形されている。 ==⟨ reflection ⟩ は、何の変形もしてないが、両方が異なる見かけの同じ正規型
+である時に見かけを変形している。 ==⟨⟩ と書くこともできる。
+
+---数式変形の記述
+
+この数式変形自体も Agda で記述されている。
+
+    module ==-Reasoning {n} (A : Set n ) where
+
+      infixr  2 _∎
+      infixr 2 _==⟨_⟩_ _==⟨⟩_
+      infix  1 begin_
+
+
+      data _IsRelatedTo_ (x y : List A) :
+                         Set n where
+        relTo : (x≈y : x  == y  ) → x IsRelatedTo y
+
+      begin_ : {x : List A } {y : List A} →
+               x IsRelatedTo y →  x ==  y
+      begin relTo x≈y = x≈y
+
+      _==⟨_⟩_ : (x : List A ) {y z : List A} →
+                x == y  → y IsRelatedTo z → x IsRelatedTo z
+      _ ==⟨ x≈y ⟩ relTo y≈z = relTo (trans-list x≈y y≈z)
+
+      _==⟨⟩_ : (x : List A ) {y : List A}
+                → x IsRelatedTo y → x IsRelatedTo y
+      _ ==⟨⟩ x≈y = x≈y
+
+      _∎ : (x : List A ) → x IsRelatedTo x
+      _∎ _ = relTo reflection
+
+これは List 専用の式変形を定義している。trans-list は、List での等式の三段論法になっている。これは、単一化で証明される。
+
+    trans-list :  ∀{n} {A : Set n} {x y z : List A}  → x ==  y → y == z → x == z
+    trans-list reflection reflection = reflection
+
+relTo が、等しくなるべき等式を持っていて、証明の最後を示す _∎ _ が、三段論法で繋がったすべての等式が等しいことを要求する。
+最後に　begin_ が _IsRelatedTo_ を _==_ に変換する。
+
+数式変形は任意の等式に使えるが、自分用にカスタマイズして使う方が良い。良く使用する推論や定理も一緒に記述する方が良い。
+
+Agda の module には引数があり、暗黙の引数も使うことができる。
+
+---数式変形用に ? を使う
 
 証明の例 (Append の結合)