# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1385632094 -32400
# Node ID 888cc58ced9da228b4ddc1663be1ebc951d1b8d8
# Parent  aa359e82dab736a836b34288cfa2883b6fc1a493
fix

diff -r aa359e82dab7 -r 888cc58ced9d Agda.mm
--- a/Agda.mm	Thu Nov 28 09:27:34 2013 +0900
+++ b/Agda.mm	Thu Nov 28 18:48:14 2013 +0900
@@ -5,12 +5,19 @@
 <node CREATED="1384158511282" ID="ID_173554271" MODIFIED="1384158517612" TEXT="Programming?">
 <node CREATED="1384158518929" ID="ID_132864750" MODIFIED="1384158520292" TEXT="append"/>
 <node CREATED="1385553167504" ID="ID_655374031" MODIFIED="1385553174525" TEXT="normalzation as eval"/>
+<node CREATED="1385597681199" ID="ID_1206471263" MODIFIED="1385597687519" TEXT="executable like Haskell"/>
 </node>
 <node CREATED="1385553140807" ID="ID_1697810219" MODIFIED="1385553143740" TEXT="Proof">
 <node CREATED="1385553144895" ID="ID_5020353" MODIFIED="1385553161258" TEXT="complain nothing is the goal"/>
+<node CREATED="1385597624397" ID="ID_995313728" MODIFIED="1385597661388" TEXT="how fun non executable program?"/>
+</node>
+<node CREATED="1385597979683" ID="ID_1830603554" MODIFIED="1385597984087" TEXT="How popular?">
+<node CREATED="1385597984088" ID="ID_1047860825" MODIFIED="1385597987107" TEXT="Coq"/>
+<node CREATED="1385597987723" ID="ID_1005518327" MODIFIED="1385598007540" TEXT="Every students use Coq"/>
 </node>
 </node>
 <node CREATED="1384158575905" ID="ID_1857200497" MODIFIED="1384158578202" POSITION="right" TEXT="Proof">
+<node CREATED="1385597911855" ID="ID_226453773" MODIFIED="1385597918132" TEXT="Hayting Algebra"/>
 <node CREATED="1384158578203" ID="ID_1658338767" MODIFIED="1384158586181" TEXT="Curry Howard"/>
 <node CREATED="1384158587810" ID="ID_1975721703" MODIFIED="1384158597800" TEXT="Lambda as proof"/>
 <node CREATED="1385554013320" ID="ID_1356905670" MODIFIED="1385554017783" TEXT="Martin Lof">
@@ -18,19 +25,20 @@
 </node>
 </node>
 <node CREATED="1385552512024" ID="ID_147799666" MODIFIED="1385552516341" POSITION="right" TEXT="Agda Proof System">
+<node CREATED="1385597309971" ID="ID_1759517864" MODIFIED="1385597312786" TEXT="emacs"/>
 <node CREATED="1385552516856" ID="ID_1464159621" MODIFIED="1385552528505" TEXT="expression"/>
 <node CREATED="1385552559432" ID="ID_133092931" MODIFIED="1385552561277" TEXT="binding"/>
 <node CREATED="1385553356789" ID="ID_1762984421" MODIFIED="1385553364891" TEXT="implicit parameters"/>
 <node CREATED="1385552549038" ID="ID_1258388375" MODIFIED="1385552552692" TEXT="lambda expression"/>
 <node CREATED="1385552529036" ID="ID_1881312508" MODIFIED="1385552530633" TEXT="type"/>
-<node CREATED="1385552532612" ID="ID_40469366" MODIFIED="1385552535010" TEXT="equality">
-<node CREATED="1385597173078" ID="ID_503695732" MODIFIED="1385597179382" TEXT="relation"/>
-<node CREATED="1385597180159" ID="ID_366226932" MODIFIED="1385597182662" TEXT="identity"/>
-</node>
 <node CREATED="1385552538773" ID="ID_594724672" MODIFIED="1385552539866" TEXT="data">
 <node CREATED="1385552575615" ID="ID_1970582835" MODIFIED="1385552578092" TEXT="equality"/>
 </node>
 <node CREATED="1385552540357" ID="ID_27933366" MODIFIED="1385552542986" TEXT="record"/>
+<node CREATED="1385552532612" ID="ID_40469366" MODIFIED="1385597757862" TEXT="equality">
+<node CREATED="1385597173078" ID="ID_503695732" MODIFIED="1385597179382" TEXT="relation"/>
+<node CREATED="1385597180159" ID="ID_366226932" MODIFIED="1385597182662" TEXT="identity"/>
+</node>
 <node CREATED="1385553086985" ID="ID_1287863407" MODIFIED="1385553091444" TEXT="level of Set">
 <node CREATED="1385553107280" ID="ID_1726309329" MODIFIED="1385553114125" TEXT="especialy in set"/>
 </node>
@@ -38,8 +46,14 @@
 <node CREATED="1385554060934" ID="ID_98595305" MODIFIED="1385554062564" TEXT="for all"/>
 <node CREATED="1385554063438" ID="ID_938488241" MODIFIED="1385554066022" TEXT="exisits"/>
 </node>
+<node CREATED="1385597581793" ID="ID_560374" MODIFIED="1385597584096" TEXT="all manual">
+<node CREATED="1385597584881" ID="ID_1563058814" MODIFIED="1385597593100" TEXT="no haskell support"/>
 </node>
-<node CREATED="1385553423068" ID="ID_1167992721" MODIFIED="1385553433515" POSITION="right" TEXT="Comparing Haskell"/>
+</node>
+<node CREATED="1385553423068" ID="ID_1167992721" MODIFIED="1385553433515" POSITION="right" TEXT="Comparing Haskell">
+<node CREATED="1385597515449" ID="ID_148577390" MODIFIED="1385597522642" TEXT="strongness of types"/>
+<node CREATED="1385597771461" ID="ID_1284279754" MODIFIED="1385597775740" TEXT="similar syntax"/>
+</node>
 <node CREATED="1384158640697" ID="ID_1899173298" MODIFIED="1384158643661" POSITION="right" TEXT="Category">
 <node CREATED="1385552494294" ID="ID_1015253891" MODIFIED="1385552505083" TEXT="definition of Category">
 <node CREATED="1385597141136" ID="ID_193939883" MODIFIED="1385597144786" TEXT="Monoid"/>
@@ -49,11 +63,6 @@
 </node>
 <node CREATED="1385552884093" ID="ID_1465613770" MODIFIED="1385552886994" TEXT="What for?"/>
 </node>
-<node CREATED="1385552342991" ID="ID_1939991054" MODIFIED="1385552354178" POSITION="left" TEXT="Proof by human">
-<node CREATED="1385552354669" ID="ID_154501585" MODIFIED="1385552370256" TEXT="wrote at book space"/>
-<node CREATED="1385552371251" ID="ID_836715929" MODIFIED="1385552382002" TEXT="typed text"/>
-<node CREATED="1385552385336" ID="ID_1562417181" MODIFIED="1385552400070" TEXT="Written in Proof System"/>
-</node>
 <node CREATED="1384158653521" ID="ID_666651656" MODIFIED="1384158659565" POSITION="left" TEXT="technique">
 <node CREATED="1384158660337" ID="ID_1951403393" MODIFIED="1384158666022" TEXT="?">
 <node CREATED="1385553875993" ID="ID_1969521083" MODIFIED="1385553887280" TEXT="show type of this place"/>
@@ -80,12 +89,20 @@
 </node>
 <node CREATED="1385553337511" ID="ID_375830623" MODIFIED="1385553340044" TEXT="lemma">
 <node CREATED="1385553340598" ID="ID_1472759359" MODIFIED="1385553342884" TEXT="theorem"/>
-<node CREATED="1385553343847" ID="ID_1243315508" MODIFIED="1385553350226" TEXT="input"/>
+<node CREATED="1385553343847" ID="ID_1243315508" MODIFIED="1385598120000" TEXT="selecting input arguments"/>
+<node CREATED="1385598122577" ID="ID_1512810213" MODIFIED="1385598134539" TEXT="assumption as input arguments"/>
+</node>
+<node CREATED="1385598147877" ID="ID_1767619024" MODIFIED="1385598171099" TEXT="handling not-yet-proved part">
+<node CREATED="1385598184783" ID="ID_1082183331" MODIFIED="1385598190881" TEXT="as inpput arguments"/>
+<node CREATED="1385598192184" ID="ID_14552462" MODIFIED="1385598216243" TEXT="postulate"/>
 </node>
 <node CREATED="1385552588272" ID="ID_102481863" MODIFIED="1385552600054" TEXT="unproofbable theorem">
 <node CREATED="1385552600714" ID="ID_310970637" MODIFIED="1385552682204" TEXT="functional extensionarity "/>
 <node CREATED="1385552710574" ID="ID_1830254576" MODIFIED="1385552716716" TEXT="congulurence"/>
 </node>
+<node CREATED="1385597285233" ID="ID_1903486565" MODIFIED="1385597287428" TEXT="eval">
+<node CREATED="1385597287429" ID="ID_1235285760" MODIFIED="1385597292767" TEXT="environment of eval"/>
+</node>
 <node CREATED="1385552778933" ID="ID_111669053" MODIFIED="1385552786125" TEXT="type inconsistency">
 <node CREATED="1385552786679" ID="ID_463662714" MODIFIED="1385552788556" TEXT="red"/>
 </node>
@@ -103,14 +120,25 @@
 </node>
 </node>
 <node CREATED="1384158677282" ID="ID_174231957" MODIFIED="1385552419537" POSITION="left" TEXT="mathematical thinking">
-<node CREATED="1384158684403" ID="ID_1399570192" MODIFIED="1384158689741" TEXT="understanding"/>
-<node CREATED="1385552451013" ID="ID_831968301" MODIFIED="1385552457147" TEXT="pattern matching"/>
+<node CREATED="1384158684403" ID="ID_1399570192" MODIFIED="1384158689741" TEXT="understanding">
+<node CREATED="1385597890324" ID="ID_1847853272" MODIFIED="1385597941292" TEXT="by types"/>
+<node CREATED="1385597893765" ID="ID_1389031272" MODIFIED="1385597945129" TEXT="by models">
+<node CREATED="1385597950001" ID="ID_151641398" MODIFIED="1385597956505" TEXT="not given by Agda"/>
+</node>
+</node>
+<node CREATED="1385552451013" ID="ID_831968301" MODIFIED="1385552457147" TEXT="pattern matching">
+<node CREATED="1385597962784" ID="ID_87138651" MODIFIED="1385597972049" TEXT="is this understandings?"/>
+</node>
 <node CREATED="1385552461182" ID="ID_220420516" MODIFIED="1385552466866" TEXT="problem solving">
 <node CREATED="1385552466866" ID="ID_781175552" MODIFIED="1385552473172" TEXT="proof finding"/>
 </node>
 <node CREATED="1385552477803" ID="ID_1460716599" MODIFIED="1385552482511" TEXT="problem finding"/>
 </node>
 <node CREATED="1385552909317" ID="ID_1707994061" MODIFIED="1385552914641" POSITION="left" TEXT="usefulness of Agda">
+<node CREATED="1385597697480" ID="ID_895791945" MODIFIED="1385597703669" TEXT="Haskell like syntax">
+<node CREATED="1385597717172" ID="ID_1406282220" MODIFIED="1385597721238" TEXT="strange symbols"/>
+<node CREATED="1385597723709" ID="ID_1501399885" MODIFIED="1385597727477" TEXT="emacs support"/>
+</node>
 <node CREATED="1385552915662" ID="ID_643691875" MODIFIED="1385552927413" TEXT="to complete understandings"/>
 <node CREATED="1385552934325" ID="ID_133712397" MODIFIED="1385552943388" TEXT="see the proof symmetrry"/>
 <node CREATED="1385552951917" ID="ID_1111590064" MODIFIED="1385552962300" TEXT="find proof"/>
@@ -131,5 +159,25 @@
 </node>
 <node CREATED="1385553208022" ID="ID_1238219050" MODIFIED="1385553225357" TEXT="Hoare logic like proof of practical programming"/>
 </node>
+<node CREATED="1385552342991" ID="ID_1939991054" MODIFIED="1385552354178" POSITION="right" TEXT="Proof by human">
+<node CREATED="1385552354669" ID="ID_154501585" MODIFIED="1385552370256" TEXT="wrote at book space">
+<node CREATED="1385597411306" ID="ID_41605107" MODIFIED="1385597416033" TEXT="3 lines of proof">
+<node CREATED="1385597422045" ID="ID_1465170514" MODIFIED="1385597433982" TEXT="many missing parts"/>
+<node CREATED="1385597436540" ID="ID_1855719075" MODIFIED="1385597452864" TEXT="exercise"/>
+</node>
+<node CREATED="1385597804760" ID="ID_552514819" MODIFIED="1385597842300" TEXT="write necessary keywords to recall only"/>
+</node>
+<node CREATED="1385552371251" ID="ID_836715929" MODIFIED="1385552382002" TEXT="typed text">
+<node CREATED="1385597464732" ID="ID_664600436" MODIFIED="1385597469501" TEXT="missing parts"/>
+<node CREATED="1385597848856" ID="ID_1150238160" MODIFIED="1385597852328" TEXT="formatting problem">
+<node CREATED="1385597852600" ID="ID_1735973674" MODIFIED="1385597854304" TEXT="TeX"/>
+<node CREATED="1385597854832" ID="ID_526772293" MODIFIED="1385597862164" TEXT="Commutive diagram"/>
+</node>
+</node>
+<node CREATED="1385552385336" ID="ID_1562417181" MODIFIED="1385552400070" TEXT="Written in Proof System">
+<node CREATED="1385597474149" ID="ID_1437200348" MODIFIED="1385597476509" TEXT="checked"/>
+<node CREATED="1385597477565" ID="ID_1553409639" MODIFIED="1385597481238" TEXT="have to be complete"/>
+</node>
+</node>
 </node>
 </map>
diff -r aa359e82dab7 -r 888cc58ced9d agda-prog.ind
--- a/agda-prog.ind	Thu Nov 28 09:27:34 2013 +0900
+++ b/agda-prog.ind	Thu Nov 28 18:48:14 2013 +0900
@@ -32,4 +32,135 @@
 また、Agda の特徴である式変形を明示する推論に対するいくつかの手法に
 関しても考察する。
 
+--証明支援系
 
+Monad とか Kan extension とかを知らないと関数型プログラミングできない
+
+Monad の結合性を示すだけでも煩雑な計算が必要
+
+高階述語論理
+
+ハイティング代数
+
+Curry Howard 対応
+
+Coq
+
+例題としての圏論
+
+--人による証明
+
+数学の本に書いてある証明
+
+省略された部分
+
+問題を解いてわかる部分
+
+手書きの証明
+
+清書された証明
+
+Proof System 上の証明
+
+理解するとはどういうこと?
+
+モデルを理解する
+
+証明を理解する
+
+パターンを理解する
+
+--Agda
+
+式
+
+Lambda 式
+
+変数の定義
+
+変数の型
+
+データ型
+
+レコード型
+
+等号
+
+   データ型を使った等号
+   関係を表す集合としての等号
+
+集合のレベル
+
+暗黙の引数
+
+emacs との連携
+
+--Agda での証明方法
+
+? の使い方
+
+数式変形
+
+数式変形の記述
+
+数式変形用に ? を使う
+
+record の使い方
+
+数学的構造の存在を示す
+
+record での変数の位置の選択
+
+これから証明する部分の扱い
+
+eval の使い方
+
+Agda では証明できないもの
+
+外延性
+
+合同性
+
+a=b は証明できない。
+
+赤を解決する(型の矛盾)
+
+黄を解決する(十分限定されていない変数)
+
+暗黙の変数を明示する
+
+再利用性
+
+module parameter と、lemma の入力
+
+Mono morphism から来る問題
+
+--Agda の有効性
+
+Haskell の構文との親和性
+
+証明の完成度がわかる
+
+証明の対称性を視認できる
+
+Unification により証明を見つけることができる
+
+すべて人手
+
+式変形を明示できる
+
+証明は極めて個人的
+
+勝手な記号
+
+勝手なrecord
+
+勝手な module parameter
+
+理論の理解に使う Monad とか Kan extension とか
+
+--今後の展開
+
+プログラミングと証明を同時に行う
+
+