2012年11月08日

正しく証明できた定理の上部で後から必要になったライブラリのモジュールをインポートしたら証明が破綻した．原因はライブラリ内で Obligation Tactic が上書きされててそれがグローバルに影響をもたらしてくれてるからで……　副作用ありまくりだなぁ．デフォルトが何なのかわからんが Show Obligation tactic で見る限り "Obligation Tactic := unfold complement, equiv; program_simpl." あたりっぽい？

モジュールを読み込んで泣く別のパターンとしては型クラスのインスタンスの優先度が変わってしまって implicit な引数に思ったものがハマってくれなくなるという現象が起きる．使って欲しいインスタンスを Existing Instance でトップに持ってきておけばなんとか大丈夫っぽいけれど．

色々と副作用がありまくりなので透明なライブラリとか頑健なライブラリとか気をつけないと書くことができないと理解した．