λx.x K S K ＠ はてな

■[Coq] 8.2 と 8.3 の互換性

久しぶりに Coq を触ったら， 昔書いた Coq のソースプログラムが通らなくなっていました． いろいろ原因を探ってみたところ， Coq 8.2 と Coq 8.3 で， 証明の開始時点での goal の形式が変わったためのようです． たとえば，

Theorem eq_diff_0 (n m: nat) : n = m -> n - m = 0.

という定理を証明しようとすると，8.2 では

============================
   forall n m : nat, n = m -> n - m = 0

で開始されますが，8.3 では

   n : nat
   m : nat
============================
   n = m -> n - m = 0

で開始されてしまいます．

互換性に関する公式の情報によると， -compat 8.2 というオプションを追加すると動作するらしいのですが， 新しいプログラムに混ぜて再利用するときには不都合なので， とりあえず，

Ltac gen_clear := repeat (match goal with [x:_|-_] => generalize x; clear x end).

という tactic を定義して， 動作しなくなった全ての証明の始めのところに gen_clear を追加することで解決できました． こういう仕様変更って，ユーザは困らないのかなぁ…．

Permalink | コメント(0) | トラックバック(0) | 13:11

■[雑記][アンビグラム] あけましておめでとうございます．

今年もアンビグラムというほどのものではありませんが， それに近いものを作成してみました． これまでのもの ( 2008年 / 2009年 / 2010年 ) に比べるとわかりやすすぎますね． 昨年は全く更新しないという体たらくでしたが， 今年はこれで少なくとも一回は更新できました． 今年もよろしくお願い致します．

Permalink | コメント(0) | トラックバック(0) | 18:26

■[雑記] クワインとフェルマーの最終定理

(更新を滞るとずっと侵略されているように見えてしまうので，むりヤリ記事をひねり出すことにしました)

さて，今年も 12 月 25 日が近づいてまいりました．皆さんご存知の「ク」で始まるあの日です． そう，クワイン (W. V. Quine) の命日ですね． ということで，今回はクワインの話です．プログラミングを嗜む人であれば，クワインというと，

を二度書け！ を二度書け！

のような「実行すると自分自身を出力するプログラム」を思い浮かべますが， 今回はそういう話ではありません． 彼が残した短い記事を紹介します． といってもだいぶアレンジしているので，興味のある人は元の文献 *1 を読んでください．

もうすぐお正月．初詣ではおみくじでその年の運勢を占ったりしますが， みくじ棒の入った筒を振って出た数字から大吉やら凶やらが書かれた紙と交換することがあります． みくじ棒を再利用できるように中から出ないようになっているものもありますね． 今回考える問題は，そんな「再利用できるみくじ棒の入った筒」に関するものです． 簡単のため，数字ではなくて大吉や凶が直接書かれたみくじ棒を想像してください．

問題

大吉，吉，凶の 3 種類のみくじ棒が入った筒があります． 3 回以上このおみくじを引くとき， 「大吉と吉が両方 (1回以上) 出る確率」と「凶しか出ない確率」が等しくなるためには， どんな割合で大吉，吉，凶を入れて，何回引けばよいでしょうか？

2 回しか引かないのなら，大吉 1 本，吉 2 本，凶 2 本 入れれば， 大吉と吉が出る確率が 1/5 × 2/5 + 2/5 × 1/5 = 4/25， 凶しか出ない確率が 2/5 × 2/5 = 4/25 なので等しくなります． 3 回以上の場合はどうでしょう？

続きを読む

Permalink | コメント(0) | トラックバック(0) | 23:21