No Such Blog or Diary

帰りの便を加算するとプレミア資格用のマイル数が 49000くらいになるらしい．３ヶ月弱に１回の周期でアメリカないしヨーロッパに飛べばそうなるか．

沖縄往復とかやってみてもいいかもしれない．

Android のバックグラウンドデータとか自動同期を止めただけではソフトウェアの更新とかは止まらないのね．そのせいなのか全然通信した記憶が無いのに第一のリミットいっぱいまで使われていたっぽい日が多数……　これまでの旅でも結構無駄が発生していたということか．

普段は音声通話しないのでパケホでトータル６千円なのだけど，今月は少なくとも３万超えでそれの５倍．約半年分と考えると高いかなぁ．

とりあえずデータ通信の大本を切っておけば大丈夫なのだろうか？　

とりあえず，すでにある仮定から導かれる複数の結論を同時に使いたい時にどうすればいいのかとかで小一時間悩む．apply すると元のが消えちゃうし……　とかやってた．面倒になって最終的に assert で必要なものを全部突っ込めばいいやという結論に達した．もしくは replace 使いまくって後回しにするとか．あとは仮定に conjunction が入っているときにその一方だけが使いたいんだよとかいう時には destruct H as [H1 H2] とか叫べばいいと学習．そしてペアの等式から要素の等式を得る方法がわからず，それをやるためだけの証明を別途自前で用意するとかいうアホらしさ．まだまだ色々と経験が足りん．

そして書き換え位置を特定する方法が未だにわからない．

リスト l の n 番目の要素を取ってくる関数 nth n l を定義するのに (n < length l) をつけときゃデフォルト値とか使わずトータルな関数定義できるよね，とかいう勢いで関数本体を書いてみようと思ったのだけどどう書いていいのかわからなかったという．結局，定義の頭に Program ってつけといてよくわからんところに _ （アンダースコア）置いといて，あとで proof obligation を始末する，という方法で定義できることを教えたもらったのでそれで済ませたのだけど……　定義された関数が読めん．そして定義された関数に関する性質の証明も訳わからん項が出てきて混乱する（再帰先で n < length l が保たれることを示すためにこの型を持つ読めない項が作られるので式の見た目がごちゃごちゃ）．依存型とか使いこなせない気がする．

丸一日寝てた．お陰で体調もあと一晩寝れば通常運転くらいに回復．とりあえず予想以上に寝不足と冷えすぎが堪えたっぽい．今日は気温も高くて幸い．

さて，防寒対策を練っておくか．

なんの予定もない週末とか結構久しぶりな気がするなぁ……　とか言いつつ論文の印刷に大学まで出て来たり．つか，でかいディスプレイを使うには必然的に大学に出てこないとならん．

それはよいとして，頭がいたいレベルで風邪引いてるので冬眠しよう．