Coq'Art読書会 #0 #readcoqart まとめ

ちゅーん @its_out_of_tune

#readcoqart 証明済み C コンパイラ・・・

さかばー @saka_bar

CompCert興味あるけど、コード読んだことない #readcoqart

ちゅーん @its_out_of_tune

#readcoqart ASTから先なのかパーサーからなのかみたいなマサカリが飛んでるｗｗｗ＞証明済Cコンパイラ

さかばー @saka_bar

HaskellerにはおなじみのMonad #readcoqart

さかばー @saka_bar

あれ、returnって予約語だったのか #readcoqart

ちゅーん @its_out_of_tune

ぱっとみ bind (return' a) f = f a ってのが実装っぽく見えるから混乱するっぽい？ #readcoqart

さかばー @saka_bar

anarchyproofにコラッツの問題があるけど、有限の値の話だったな #readcoqart

ざぎん 𒎎𒍝𒆳@C102 2日目東ペ-22a @na4zagin3

Collatz数列を計算する関数は PHPではかけるけれど、 今のところCoqでは書けない #readcoqart

さかばー @saka_bar

仮定が弱すぎるか、結論が強すぎるか #readcoqart

さかばー @saka_bar

CPDT「証明はcrushで自動化するからやらなくていいよ」 #readcoqart

ちゅーん @its_out_of_tune

Certified Programming with Dependent Types, Adam Chlipala (http://t.co/3PsyBKiAul) #readcoqart φ(..)メモメモ

ざぎん 𒎎𒍝𒆳@C102 2日目東ペ-22a @na4zagin3

crushを使うと初心者相当の自動証明をしてくれるww #readcoqart

ちゅーん @its_out_of_tune

「Coqなんて６〜７回ほど講義出れば使えるようになるっしょｗｗｗｗ」 #readcoqart

さかばー @saka_bar

主要なtacticは限られている(2,30程度) #readcoqart

ざぎん 𒎎𒍝𒆳@C102 2日目東ペ-22a @na4zagin3

Coqは解ってる人に聞いた方が早い #readcoqart

ざぎん 𒎎𒍝𒆳@C102 2日目東ペ-22a @na4zagin3

みんな CoqIDE で、ジェネラルたん派は少ないのか #readcoqart

ざぎん 𒎎𒍝𒆳@C102 2日目東ペ-22a @na4zagin3

依存型は難しい #readcoqart

さかばー @saka_bar

依存型に関する説明 引数に依存した型が書ける #readcoqart

さかばー @saka_bar

こんな書き方あったのか #readcoqart

ちゅーん @its_out_of_tune

もう初っ端から知らない記法がバンバン出てきてる。 #readcoqart

さかばー @saka_bar

セミコロンはsubgoalが分かれる時に使うことが多い #readcoqart

ちゅーん @its_out_of_tune

crashは禁断のタクティックらしい #readcoqart

さかばー @saka_bar

Gu Tyoki Paの順番で定義したから #readcoqart

さかばー @saka_bar

Hypothesisとかは見えませんね。#readcoqart

ちゅーん @its_out_of_tune

今目指しているサブゴールにたどり着くために使える定理は基本的にすべて表示されている・・・と思ってたんだけど・・・ #readcoqart