花粉症撲滅したい
昨日今日と旅行で箱根に行ってきた.旅行は超楽しかったのだけど,2日目の今日から花粉症の症状がひどくてブチ切れている.
僕の花粉症の症状は目のかゆみ,普段より多い目ヤニ,とどまることを知らない鼻水,くしゃみ,口呼吸をしてしまうことからの唇荒れ,それに心なし頭がぼーっとする等で本当に辛い.毎年大量の鼻セレブを消費してしまう上,花粉症の時期は全然やりたいことができない.鼻水で息が詰まって眠れないこともよくある.鼻水地獄.
確か初めて発症したのが2008年の春だから,もう十年以上苦しんできていることになる.比較的楽な年もあるけど,去年なんかは杉を見ると憎しみを覚える程度にひどかった.
ただ,杉に文句を言っても何にもならないので,今日から僕は花粉症撲滅運動をしていきたい.
具体的に何をしていいかよくわからんが,他に花粉症を撲滅しようとしている人を探して話を聴いたりしたいと思う.
USキーボード
決めた. バックスラッシュとか辛かったから今度手に入れるPCはUSキーボード配列のものにする. 慣れるまで大変そうだけど,そっちの方がなんかかっこいいし.
LEANで構造体の等価性を証明する
ちょっと空いた時間にLEANで圏論をやってる. 自然変換の等価性を証明するときに困ったけど,友達に聞いて解決したので備忘録. 結論から言うと,
- 構造体を要素に分解するときはcases_onを使う.
- cc tacticは便利.
構造体hogeで説明(?)
次のようにして構造体hogeを定義し, 命題eq_hoge_of_eq_fugaを証明したい.
structure hoge := (fuga : ℕ) (piyo : fuga = fuga) lemma eq_hoge_of_eq_fuga : ∀ (hg₁ hg₂ : hoge), hg₁.fuga = hg₂.fuga → hg₁ = hg₂ := sorry
構造体のデータが等しいことだけ確認したらプロパティは証明の唯一性があるので考慮せずに 構造体が等しいことを示したいという気持ち.
とりあえずタクティックで証明することにして,
begin intros hg₁ hg₂ eq_fuga, end
まで書くと,ゴールが
hg₁ hg₂ : hoge, eq_fuga : hg₁.fuga = hg₂.fuga ⊢ hg₁ = hg₂
となる. このままでは手がつけられないので,ゴールを
hg₁_fuga : ℕ, hg₁_piyo : hg₁_fuga = hg₁_fuga, hg₂_fuga : ℕ, hg₂_piyo : hg₂_fuga = hg₂_fuga, eq_fuga : {fuga := hg₁_fuga, piyo := hg₁_piyo}.fuga = {fuga := hg₂_fuga, piyo := hg₂_piyo}.fuga ⊢ {fuga := hg₁_fuga, piyo := hg₁_piyo} = {fuga := hg₂_fuga, piyo := hg₂_piyo}
のように成分に分解するために,cases_onを使う. タクティックで使うときはcases.
begin intros hg₁ hg₂ eq_fuga, cases hg₁, cases hg₂, end
ここで,eq_fuga
の型は
要するにhg₁_fuga = hg₂_fuga
ということだから,eq_fuga
をsubst
に食わせればなんかいい感じに行けそうな気がする.
けど,
begin intros hg₁ hg₂ eq_fuga, cases hg₁, cases hg₂, subst eq_fuga, end
とすると,
10:5: subst tactic failed, hypothesis 'eq_fuga' is not of the form (x = t) or (t = x)
みたいなエラーが出る.
eq_fuga
の型は等式ではあるけど左辺も右辺も変数ではないから
subst tacticに食わせられんということらしい.
ふざけんな.
で,丁寧に
begin intros hg₁ hg₂ eq_fuga, cases hg₁, cases hg₂, have eq_fuga' : hg₁_fuga = hg₂_fuga := eq_fuga, subst eq_fuga', end
として「eq_fuga
の型は要するに……」の部分をeq_fuga'
として明示してあげると
うまくいってなぜかゴールが全部解消される.
不思議だ.
heq
という面白等価性を使ってあげないと行けなかった話を書こうと思ってたのに
使わなくてもできてしまった.
LEANのコアがどこを自明だと思ってくれるのか,謎であることよ.
まあ,とにかくこんな感じでもできるんだけど, わざわざhave tacticを使って明示するのが面倒臭い人はcc tacticを使うと
begin intros hg₁ hg₂ eq_fuga, cases hg₁, cases hg₂, cc end
のように書けてすごく簡単.
研究
本業の方の研究が進んだと思った一時間後にダメだったことが判明した。今の方針で進んだ先の反例が分かったという意味は進捗があったが、バックトラックすることになりそう。もー
ずっと書いてないな
毎日ブログ書こうと思っていたけど、やりたいことが多くてもう一月近く書けてなかった。よくないなぁ