NII Shonan Summer School on Coq

やったー I solved terminates_bigstep in lesson-8 . #CoqSchool

2014-08-26 10:03:10

k @mathink

私も terminates_bigstep やっと終わったー．補題しっかり作ればあっさりなのですなー(補題の証明がちょっと雑だけど) #CoqSchool

2014-08-26 11:13:00

#CoqSchool glyphwiki.org/wiki/u21a6 この記号ってどうやって入力するのだろう？ \u21a6 と入力すれば CoqIDE は通るのだが、unicode 以外で代替入力ないのかしらん？

2014-08-26 17:57:47

#CoqSchool 皆様に色々教えて頂いて、terminates_bigstep が証明出来た。帰納的に定義された命題は induction の対象になる、というテクニックを @yoshihiro503 さんに教わった。あと、inversion したら subst するの大事。

2014-08-26 18:00:37

#CoqSchool CPDTのcrushも賢いが、今回の教材の go も強力な tactic で、ユーザが理解出来てなくても色々証明出来てしまう。最初から Coq に同梱してくれればいいのに。。。

2014-08-26 18:03:15

#CoqSchool Iyves 先生から additional exercises are introduced. pic.twitter.com/KPu0TgeOTx

2014-08-26 18:12:34

拡大

S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください) @esumii

#CoqSchool に行った学生さんは生きているだろうか（

2014-08-26 18:20:09

やったねたえちゃん！サブゴールが増えるよ！ #CoqSchool

2014-08-26 19:39:43

#CoqSchool まだ2日目という気がしない。密度が濃いので既に何日も過ごした感じがする。

2014-08-26 21:10:50

K. Sakaguchi @pi8027

Coq サマースクールで難しい問題解きたそうな人に算術級数定理を推奨する人になってる。

2014-08-26 22:45:47

#CoqSchool なぜかフランス人とケンシイムラのサカバトウの話をしていた。 #緋村抜刀斎 #Hは発音しない

2014-08-27 08:46:11

#CoqSchool nowタクティカルを学んだ ssreflectのbyみたいで便利！

2014-08-27 08:58:56

#CoqSchool coqではいろんな演算子を定義できるけど、その記号の定義を調べるためにはLocateコマンドが便利。

2014-08-27 09:10:45

@yoshihiro503 例えば Locate "::". で::演算子の正体がリストのconsであることが分かる。 #CoqSchool

2014-08-27 09:12:24

K. Sakaguchi @pi8027

@yoshihiro503 Locate は notation だけでなく定義がどのモジュールに含まれているかも調べられる。

2014-08-27 09:14:15

サブゴールがどんどん増えていったときの顔 pic.twitter.com/SfpivqqO6a / zoi.herokuapp.com #CoqSchool

2014-08-27 11:04:45

拡大

coqの式をGallinaと呼ぶのはラテン語のメン鳥。フランス語のそれはあまりよい意味を持たないらしい。 #CoqSchool

2014-08-27 18:28:02

数式の羅列にしか見えない #CoqSchool pic.twitter.com/pXieiKJsPZ

2014-08-27 20:33:51

拡大

T.T. @t_teruya

今日習ったtactic: unfold, generalize, replace． replaceは等式をassertで突っ込むようなものらしい． #CoqSchool

2014-08-27 22:12:10

合宿4日目朝の俺 pic.twitter.com/eKX6p5uak8 / zoi.herokuapp.com #CoqSchool

2014-08-28 08:34:06

拡大

#CoqSchool あー、変数による帰納法では項が減らないから命題に関する帰納法使わないと駄目な例がこれか。。。 step_while_true は while e i が seq i (while e i) と小さくならない。

2014-08-28 09:38:06

疲れからか黒塗りの車への衝突不可避 #CoqSchool #おうちに帰るまでがCoqSchoolです

2014-08-28 10:25:21

k @mathink

描いてしまった #CoqSchool

2014-08-28 13:33:33