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

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