No Such Blog or Diary

先週月曜の分の代休？　とりあえず新婚さんの新婚旅行にお邪魔してワイナリー２軒を見学して一緒に昼食という一日．

ワイナリーはオルレアンの中心から１５キロ弱のところ？　とりあえず詳細気にせず白いワンうまかた．おばぁちゃん良い人．ガメだったかのぶどうを食べたのだけどふつうに美味しいぶどうだった．渋い赤ワインにするのがもったいない？

お昼は Le Lift (www.restaurant-le-lift.com) というところで．Google map だと変なところに案内されて迷う事になるが，ウェブサイトの地図を見れば迷わない．トラムのA線が走っている橋から川沿い（中心部側）を東に向かって少し行ったところの左側にある．つか，レストランが屋上にあって駐車場はその建物の地下という構造（駐車場メモ：駐車券とって入場，駐車場に向かう階段を降りてく途中の地下１回の踊り場の精算機に駐車券入れて精算，精算後の駐車券を出口ゲートに突っ込む，というながれ）．そんなに畏まってないので行きやすい雰囲気．前菜・メイン・デザートで３３ユーロ．普段の昼食の４倍程度．

帰りの便を加算するとプレミア資格用のマイル数が 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 が保たれることを示すためにこの型を持つ読めない項が作られるので式の見た目がごちゃごちゃ）．依存型とか使いこなせない気がする．

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

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