花粉症撲滅したい

昨日今日と旅行で箱根に行ってきた.旅行は超楽しかったのだけど,2日目の今日から花粉症の症状がひどくてブチ切れている.

僕の花粉症の症状は目のかゆみ,普段より多い目ヤニ,とどまることを知らない鼻水,くしゃみ,口呼吸をしてしまうことからの唇荒れ,それに心なし頭がぼーっとする等で本当に辛い.毎年大量の鼻セレブを消費してしまう上,花粉症の時期は全然やりたいことができない.鼻水で息が詰まって眠れないこともよくある.鼻水地獄.

確か初めて発症したのが2008年の春だから,もう十年以上苦しんできていることになる.比較的楽な年もあるけど,去年なんかは杉を見ると憎しみを覚える程度にひどかった.

ただ,杉に文句を言っても何にもならないので,今日から僕は花粉症撲滅運動をしていきたい.
具体的に何をしていいかよくわからんが,他に花粉症を撲滅しようとしている人を探して話を聴いたりしたいと思う.

 

身元保証書

4月に会社員になるにあたって、身元保証書に父の署名をもらうため高崎日帰り旅行した。郵送でも良かったんだけど、直接行って色々話ができて良かった。自分が動けるときは動くといいことがある。

ところで身元保証書って必要なんかね?こんなのあっても気休めにしかならないし、ただただ面倒を増やしているだけなのでは?

まあ、何か理由があって書かせているんだろうな

 

書きたいことはあるんだよ

でも,書くためにリサーチしてたら時間経って書きたくなくなるんだよ. あーあ.

今日書きたかったことは,「LEANファイルをEmacsで編集してるときに 簡単に打ち込める記号一覧の見方」. でも,それをしようとしたときにバックスラッシュ'\'キーで円マーク'¥'が 認識されてウワーーーーーッてなったから今日は書かない.

quailとかいうEmacsのinput methodが大事らしい.

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_fugasubstに食わせればなんかいい感じに行けそうな気がする. けど,

  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

のように書けてすごく簡単.