No Such Blog or Diary

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

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

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

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

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

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

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

予想よりも寒いのでやばそうだなと思っていたら喉と鼻がやられた．とりあえず週末は寝て過ごすか．

閑話休題．

Don't disturb 無視して突っ込んで来ないで欲しいんだけど……　ちょいと移動すっか．

普通に関数型言語として使うのは問題ないけれど依存型で変なことしようかなと思い始めるあたりでごちゃごちゃと……　Prop と bool の違いではまりまくるとか．どこに気をつけるべきなのかがはっきり見えないので修行あるのみ？