No Such Blog or Diary

とりあえず修学旅行に巻き込まれてチェックインにも時間を食う始末．駅でも５分遅れで電車を逃し２時間足止めとか．

色々とタイミングが悪い．

シンクとかレンジとかの掃除は楽に終わったんだけど，電気コンロ上面のガラスプレートを磨き上げるのに2時間半かかった．汚れの主な原因はフライパン：フライパン本体と縁が別パーツになっていて隙間がある → その隙間に歴代の油汚れが貯まっている → コンロにかけると熱で微妙に溶けて外側に垂れる → コンロのプレートに焼き付く → 根性入れないと落ちない．

この掃除をしておかないとキッチン掃除代15ユーロを取られるのだけど，労力的に掃除しなかったほうがお得だった気がする．まあいいか．

閑話休題．

そして気づけば右腕が筋肉痛．

たかが結合則と分配則ごときを１日かけても証明できないとは……　なるべくプログラムの等式変換で証明しようとしているから面倒なのかね．うまい具合に述語を定義してやれば結構簡単にきそうな気配だけど．

閑話休題．

広いセミナー室に二人ほぼ会話なしで６時間ぶっ続けて証明を書き続けるとかいうことをしても敵は依然として大きいまま．Leibniz equality でなく任意の同値関係を使えるように定式化しようとすると色々な既存の資源が使えなくなるので面倒この上ない．少なくとも Proper のインスタンスを大量に用意せんと身動き取れないし．

閑話休題．

さて，帰り支度をするか．

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

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

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

20時過ぎに作業してたら19:30で建物閉めるんだからさっさと出てけクソがと警備の人たちに追い出された．なんでやねん．カードキー持っとるので幾らでも出入りできるのに……

どうも時間外に作業するには向いていない環境な気がする．

サーチがお馬鹿すぎる．あさっての方向を向いてどんどん突き進んでいく……

どうも引数の構造が「沢山の単純なインスタンス＋それらの関係を示すインスタンス」になっていると単純な方を先にサーチしに行ってどんどんアホになるらしい．まあ，そりゃそうだろうけど．

とりあえず，単純なインスタンスを関係を示すインスタンスの奥底においてやったら頭良くなった．

閑話休題．

どっかにサーチのアルゴリズムを詳細に述べたものとかないんかな？　C++のテンプレートのサーチの方がまだ分かりやすい挙動をしてくれる気が……