Coq tutorial
話す内容は倍くらいあったんだけど、時間が足りなかったなぁ。
- 次回は=を含む証明、帰納法の証明、Listの証明。
- inversion使えると、初心者卒業かな。
- 機能的定義
- いろんな定義の仕方があるけど、Coqでは機能的な定義をするのが望ましい。
- 証明が簡単になる。
- 決定可能な述語
- 必ず結果がどちらかに決まるのであれば、証明するのが望ましい。
- 清楚帰納法の話はCoq Tutorialではできなかった。
- 依存型の話もCoq Tutorialでは難しいかも。
- 引数として証明を渡せる。
- 関数と証明の統合。
- Programコマンドを使うと、証明付き関数を作れる。
- Notation, Type Class
- 話さなかったことも、データは公開します。
- Monadの定義
- Record,Moduleでもできるよ。
- Type Classだと型推論などもしてくれる。
次回あるなら、回数を増やしてやってくれないかな。
- どっちかというと、Coq Tutorialで興味を持ってくれた人が、FM_Forumに来てくれないかな、と思ってます。
上級編、というと、人によって興味が分かれちゃうんですよね。
- ツールの使い方なら菊地さんにssrefrectの話してもらうとか。
- 8.4が出たら機能紹介してもいいかな。Language Updateのネタで話す機会がでるかも。
実際の問題を解きたい、というのがゴールにあるかも。
- 結局、手続き型の言語の証明をしたい、ということになると、Separation Logicというのがある。
- ポインタ
- 領域の確保
- 手続き型
- CoqライブラリにはSEPLOGがある。
- もうちょっとヌルいところで、MLのプログラム(ただし、破壊的代入有)なら、
- CFML <- OCaml => Coq の証明課題生成ツール
- Why3 これならVSTTEのcompetitionにでてくるのもできそう。
- 依存型の理論を勉強するとか?
- 値:Set (自己言及的な記述を許さない)
- 命題:Prop
- TAPLが好きなら、単純型付ラムダ計算をCoqで実装とか。
- Coq以外のツールとか
- IsabelleはどうもCoqより強力?
- OCL -> Isabelleとか
- IsabelleからScala生成できる
- Isabelleは集合ライブラリがある
1,2年目は Alloy,Coqを勉強した
Why3
- Why3のintは無限。
- 使いこなすには、適当な課題を見つけてきて課題を解く。
- ライブラリを作るとか。
- 実際のコードでは、ループ不変式を上手く決定するのが難しい。
- Bもループ不変式をやるのが難しい。
Krakatoa
- Why3より(生成されたコードが)すごいことになってる。
今年の目標
- Why3は、VSTTEの問題を解くところから挑戦
- 次回VSTTEを解こう!
- TPP参加?
- 今年は千葉大のはず。
Coqその他
- Implicit Argumentsで指定する[A]とAの違いは?
Alloy Analyzer
assert ReformulateNonEmptinessOK {
all r: univ->univ |
some r iff (some x, y: univ | x->y in r)
}
check ReformulateNonEmptinessOK
assert ReformulateTransitiveOK {
all r: univ -> univ |
(r.r in r) iff (all x,y,z :univ | x -> y in r and y -> z in r implies x -> z in r)
//(all x,z :univ | some y :univ | x -> z in r implies x -> y in r and y -> z in r) //駄目な例
}
check ReformulateTransitiveOK
assert ReformulateIrreflexiveOK {
all r: univ -> univ |
(no iden & r) iff (all x: univ | x -> x not in r)
}
check ReformulateIrreflexiveOK
assert ReformulateSymmetricOK {
all r: univ -> univ |
(~r in r) iff (all x, y: univ | x -> y in r implies y -> x in r)
}
check ReformulateSymmetricOK
assert ReformulateFunctionalOK {
all r: univ -> univ |
(~r.r in iden) iff
// (all x,y :univ | y -> x in r implies x -> y in r)
(all x,y1,y2:univ | x -> y1 in r and x -> y2 in r implies y1 = y2)
}
check ReformulateFunctionalOK
assert ReformulateInjectiveOK {
all r: univ -> univ |
(r.~r in iden) iff
(all x1,x2,y :univ | x1 -> y in r and x2 -> y in r implies x1 = x2)
}
check ReformulateInjectiveOK
assert ReformulateTotalOK {
all r: univ -> univ |
(univ in r.univ) iff
(all x :univ | some y :univ | x -> y in r)
}
check ReformulateTotalOK
assert ReformulateSurjectiveOK {
all r: univ -> univ |
(univ in univ.r) iff
(all y :univ | some x :univ | x -> y in r)
}
check ReformulateSurjectiveOK
A.1.3 (a) sibling
- 同じ親を持つ子供をunivとする
- この間の関係を兄弟関係rとする
- 兄弟関係難しいよ。法律的？生物学的？数学的？
- そもそもここでいう集合{r:univ->univ}は「すべての人の関係」？「ある兄弟関係」？
- -> ｒが何を指しているかを言わないと答えられない？
- 日本的に「自分は自分の兄弟」を認めないと・・・対称律と推移律をみたさないので反例がでる。
- どう定義するか、という問題。Alloyなら反例が出て終わり、だけど、Coqだと矛盾が出たら大変なことになるね。
- 多義性のある言葉をどう扱うか。
A.1.3 (b) links
A.1.3 (c) contains
A.1.3 (d) group
- これってcontainsと何が違うの?
- 要素 -> Groupか?これを決めないと関数的、単射的が判断できない。
- ルートが無くてもいいということか。
- ここではグループの階層は認めていないようだ。
- グループは図的要素なの?グループっていうのがピンとこないなぁ。
- グループ=図的要素の部分集合。
