Coq

Coq の Reference Manual が一新されてた

連休の飛び石部分1日目.連休といっても論文書かなきゃいけないので実質休みなし.まあ,どうでもいいことで時間取られるよりよっぽど有意義なので問題ない. 閑話休題.今日まで気づかなかったが, Coq の Reference manual のデザインが一新されている.お…

かっこの対応チェッカーの検証

うちの研究室の,新 B4 向けの春休みの宿題?で,「かっこの対応をチェックするプログラムを作成せよ」というのがある.もとは隣の研究室のネタだったらしいが,引き続き使わせていただいているらしい. ちなみに去年は私も提出する側で,Haskell の練習がて…

いらいら

杜撰な計画のせいで,非常に貴重な機会を逃すことになりいらいら.何も考えてないくせに「とりあえず戻ってこい」とか抜かすんじゃねえ.何を考えているのだ(何も考えていない). これについて書いていると,精神衛生上非常によくないので別の話をば.その…

SSReflect はじめました

卒論で多少言及したいので, Coq の拡張の一つである SSReflect を色々試してみる.素 Coq に慣れているとちょっと戸惑うが,素 Coq とのタクティックの対応表みたいなのがあるので,割とスムーズに移行できそう.けんども,新しい言語を使い始める時特有の…

写真

某所の人からTwitterで呼び出されたので,「あれ俺の荷物なんか置いたまんまだっけ」と思って焦って某所に行くと,「集合写真をとってほしい」といわれる.まあミーティング中だったが別に自分のターンじゃないからいいかと思って,とりあえず了承.感想:な…

気軽に引き算するな

昼から晩までずっと,研究で開発したライブラリとその使用例を整理していた.まあ,結構綺麗な使用例ができたでしょう. ところで,Ackermann関数が原始再帰的でないことを証明するときに使う Lemma ack_inc : forall c1 c2 : nat , exists c3 : nat , foral…

家探し part 2

午前中は昨日に引き続き家探しその2.当たり前だけど,家賃高い家ほどまあ綺麗だわな.それにしても,あそこの立地は良いな.CoCo壱が近くにあるのは強い. 午後からは平常運転.といいつつ,特に何も仕事せずダラダラ過ごしてしまった感じもあるが,諸々疲…

Bool型を使った古典命題論理の埋め込み?

昼ごろ起床.昼夜逆転を半回転させるのに成功した. んで,本題.Coq というか Gallina の if-then-else を使った証明が扱いにくくて悩ましいが,if の後の bool 値は,中身の構造に立ち入らなくても, true だった場合と false だった場合に場合分けしてし…