λx. x K S K @はてな

このブログ内に記載された文章およびコードの著作権は,すべて Keisuke Nakano に帰属します.

Coq

推移律はいらない? ─比較ソートの正当性に必要な比較関数の性質─

Coq

この記事は Theorem Prover Advent Calendar 2013 最終日 (25日目)*1の記事です. 元々このネタは, 後学期の3年生向けの実験でCoqを教える際に提示した 「挿入ソートの正当性を示す」という最終課題の模範解答を作成する際に気づいたことです. このため,…

8.2 と 8.3 の互換性

Coq

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

(続) Seven trees

[註] この記事には解答はありませんが,Coq の証明が読める人にはヒントになってしまうかもしれません.[追記] 解答の公開が解禁されたそうなので遅ればせながら公開致します.Blassのものと同じ定義なのであまり参考にならないと思います. id:kikx さんが …

APLAS 2006

参加された皆さんお疲れ様でした. さすがに,2泊5日などという頭の悪いスケジュールを組んだのは私だけだったようで. 今回最も印象に残ったのは Tree transducerの業界で著名なSM氏と議論ができたこと 帰りの京成線でのRA氏によるCoqのチュートリアル どっ…