--- a/agda2latex.pl	Fri Dec 06 00:16:37 2013 +0900
+++ b/agda2latex.pl	Thu Jan 09 19:02:04 2014 +0900
@@ -3,7 +3,7 @@
 
 while(<>) {
 
-    next if (/\{\\footnotesize/) ;
+    next if (/\{\\footnotesize\tt/) ;
     if (/\\begin{[Vv]erbatim}/) {
         print "\n{\\tiny\\noindent\n";
         while(<>) {

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/presen/agda-prog.ind	Thu Jan 09 19:02:04 2014 +0900
@@ -0,0 +1,331 @@
+-title:  Agda での Programming 技術
+
+-author: 河野真治
+
+--なんで、今、証明支援系なのか?
+
+証明支援系の歴史は古い ( HOL, Coq, Agda も新しくない )
+
+Monadって何?
+
+Monad を解説しているサイトは多いが、多くは皮相的
+
+元は圏論の概念
+
+→　だったら、Monad を証明支援系を使って理解すれば良いんじゃないの?
+
+--プログラムの検証の二つの方法
+
+    モデル検証
+    証明
+
+-- モデル検証
+
+    可能な実行をすべて試す 
+　　論理の言葉で言えば、充足可能性を調べる
+    バグを探す、検索空間が膨大、比較的大きなものに対処できる
+    扱う問題の規模に探索時間が依存する
+
+--証明
+
+    プログラムがどういう性質を満たすかを論理式で記述する
+    推論規則を使って、公理と仮定から性質を導く
+    非常に難しく、証明の長さも長い
+    扱う問題の規模に証明時間が依存する
+
+--Curry Howard 対応
+
+証明とλ計算式が対応する。対応は、扱う論理に寄って異なる
+
+論理が複雑になる分、λ計算を拡張する必要がある
+
+　　→　ラムダ計算の拡張の指針になる
+
+証明する論理式は型に対応する
+
+証明するべき式の型になるλ式を作れれば証明されたことになる
+
+--Agda とは何か
+
+Haskell実装、Haskellに似た構文
+
+   indent による scope の生成
+
+型と値
+
+   : で型を定義
+   = で値を定義
+
+集合
+    すべての値は集合
+
+集合のレベル
+    集合の集合はレベルが上がる
+
+暗黙の引数
+
+    {} で省略可能な引数を作れる
+
+--λ
+
+    module proposition where
+    postulate A : Set
+    postulate B : Set
+
+集合であるA,Bを命題変数として使う。
+
+    Lemma1 : Set
+    Lemma1 = A -> ( A -> B ) -> B
+
+これが証明すべき命題論理式になる。実際には式に対応する型。
+    lemma1 : Lemma1
+
+として、この型を持つ lambda 式を使えば証明したことになる。
+以下のどれもが証明となり得る。
+
+    -- lemma1 a a-b = a-b a
+    -- lemma1 = \a a-b -> a-b a
+    -- lemma1 = \a b -> b a
+    -- lemma1  a b = b a
+
+
+--data 
+
+Haskell の data と同じ。
+
+    infixr 40 _::_
+    data  List  (A : Set ) : Set  where
+       [] : List A
+       _::_ : A → List A → List A
+
+
+論理式の排他的論理和を表すのにも使える。
+
+    data _∨_  (A B : Set) : Set where
+      or1 : A -> A ∨ B
+      or2 : B -> A ∨ B
+
+or1 と or2 が Constructor である。
+
+    Lemma6  : Set
+    Lemma6 = B -> ( A ∨ B )
+    lemma6 : Lemma6
+    lemma6 = \b -> or2 b
+
+これは、∨ の導入になっている。削除は、
+
+    lemma7: ( A ∨ B ) -> A
+    lemma7 = ?
+
+
+--equality
+
+さらに、data は等式を表すのにも使う。
+
+    data _==_  {A : Set } :  List A → List A → Set  where
+          reflection  : {x : List A} → x == x
+
+直観主義論理には命題自体に真偽はない。なので、返すのは Set になっている。なので、二重否定は自明には成立しない。
+
+--record
+
+record は、論理積を作るのに使う。
+
+    record _∧_ (A B : Set) : Set where
+       field
+          and1 : A
+          and2 : B
+
+∧の導入
+
+    lemma2 : A → B → A ∧ B
+    lemma2 a b =  record { and1 = a ; and2 = b }
+
+∧の削除 ( open _∧_  が必要 )
+
+    lemma3 : A ∧ B → A
+    lemma3 a =  and1 a
+
+record は、ある性質を満たす数学的構造を表すのに使う。
+
+--Append の例
+
+    postulate A : Set
+
+    postulate a : A
+    postulate b : A
+    postulate c : A
+
+
+    infixr 40 _::_
+    data  List  (A : Set ) : Set  where
+       [] : List A
+       _::_ : A → List A → List A
+
+
+    infixl 30 _++_
+    _++_ :   {A : Set } → List A → List A → List A
+    []        ++ ys = ys
+    (x :: xs) ++ ys = x :: (xs ++ ys)
+
+
+-- Append の実行
+
+ 　Agda の実行は正規化
+   Haskell と同じ
+
+    l1 = a :: []
+    l2 = a :: b :: a :: c ::  []
+
+    l3 = l1 ++ l2
+
+
+--Append の結合則の証明
+
+証明するべき式 
+
+    list-assoc : {A : Set } → ( xs ys zs : List A ) →
+         ( ( xs ++ ys ) ++ zs ) == ( xs ++ ( ys ++ zs ) )
+
+
+List の持つ性質を表す式
+
+    data _==_  {A : Set } :  List A → List A → Set  where
+          reflection  : {x : List A} → x == x
+
+    cong1 :  {A : Set  }  { B : Set  } →
+       ( f : List A → List B ) → {x : List A } → {y : List A} → x == y → f x == f y
+
+    eq-cons :   {A : Set } {x y : List A} ( a : A ) → x ==  y → ( a :: x ) == ( a :: y )
+
+--Agda での証明手順
+
+(1) 証明するべき式を型として記述する
+
+(2) 値を = ? と取り敢えず書く
+
+(3) ? をλ式で埋めていく
+
+(4) C-N で正しいかどうかをチェックする
+
+    赤   ... 型エラー
+    黄色 ... 具象化が足りない
+    停止性を満たさなない
+
+(5) data  は patern match で場合分けする
+
+(6) 必要なら式変形を使う
+
+
+--Haskell と Agda の違い
+
+Haskell で結合則を証明できる?
+
+Haskell は型に関数やデータ型の constructor を書けない
+
+Haskell のプログラムは Agda のプログラムになる?
+
+   float とかはない
+   integer は、succesor で書く必要がある
+
+--式変形
+
+λ式では、人間に読める証明にならない
+
+    ++-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
+      ==⟨ reflection ⟩
+         (x :: (xs ++ ys)) ++ zs
+      ==⟨ reflection ⟩
+        x :: ((xs ++ ys) ++ zs)
+      ==⟨ cong1 (_::_ x) (++-assoc A xs ys zs) ⟩
+        x :: (xs ++ (ys ++ zs))
+      ==⟨ reflection ⟩
+        (x :: xs) ++ (ys ++ zs)
+      ∎
+
+
+
+
+--いくつかの技術
+
+等号
+
+?
+
+Unicode の記号
+
+module
+
+暗黙の引数が多すぎる
+
+--Agda で証明できないこと
+
+a ≡ b は証明できない
+
+functional extensionarty
+
+    -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → 
+          (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x )
+
+実際には、
+
+    postulate extensionality : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } 
+       → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
+
+
+部分集合
+
+    異なる集合の要素は異なるので、部分集合を作れない
+    →　　x ∈ P 　を自分で定義する
+
+合同性   x ≡  y ならば f x ≡  f y 。これは、_≡_  に付いてしか言えない。
+Relation などで定義すると、合同性は自分で仮定あるいは証明する必要がある。
+
+
+直観主義論理の限界
+
+   あんまり良くわかりません
+
+--圏論の定理の証明
+
+  Monad の結合性
+  Monad から作る Kleisli 圏
+  Kleisli 圏から作る随伴関手
+  随伴関手での Limit の保存
+  米田のレンマ
+
+--本の証明とAgdaの証明
+
+    本の証明は、山登りの道標しか示さない
+
+    Agdaの証明は、全部繋がっている
+
+    Agda の証明は式なので対称性が目で見える
+
+--定理を理解することと証明を理解すること
+
+定理を理解するということは使い方を理解すること
+
+定理は証明のショートカットでもある
+
+証明を理解しても使いこなせない
+
+--結局、Monad は役に立つのか?
+
+
+--結局、証明 は役に立つのか?
+
+--Agda は面白い
+
+詰将棋みたいなもの
+
+学会でノートPCで内職しているのは Coq 
+
+Agda は Coq よりもマイナー
+
+
+
+
+