Lean4 学習2 - ushumpei’s blog

Quantifiers and Equality の The Existential Quantifier セクションにある問題を解いた。

変数名を気にして書いてみたけど一向に読みやすくならない、たとえばこんなやつ (シンタックスハイライトないのでさらに読みにくい)

example : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) := Iff.intro
  (fun h_not_all_p : ¬ ∀ x, p x =>
    (em (∃ x, ¬ p x )).elim
      (id)
      (fun h_not_exists_not_p : ¬ ∃ x, ¬ p x =>
        have h_all_p : ∀ x, p x :=
          fun w => (em (p w)).elim
            (id)
            (fun hw : ¬ p w =>
              have h_exists_not_p : ∃ x, ¬ p x := Exists.intro w hw
              absurd h_exists_not_p h_not_exists_not_p)
        absurd h_all_p h_not_all_p))
  (fun h_exists_not_p : ∃ x, ¬ p x =>
    fun h_all_p : ∀ x, p x =>
    h_exists_not_p.elim fun (w : α) (h_not_p : ¬ p w) =>
      absurd (h_all_p w) h_not_p)

byContradiction は (em h).elim (id) (fun hn =>) を書き換えられるようだが、宣言以降 False を示すことを覚えておかなければいけないのがちょっと嫌な感じがする。結局 absurd するし。

だが absurd に関しても曖昧な部分が多い、関数が implicit な変数をどうやって見つけているか理解できていないので、無関係な h, not h を渡したら示したかった命題が証明された、という感じがする

byContradiction ... show False from h hn の方が見やすいのだろうか？証明として読みやすいことと、プログラムとして読みやすいことはどうバランスを取ればいいのだろうか？というか現時点だとどちらとしても読みやすくない書き方になっている。コメントをちゃんとつけるのがいいのだろうか？

変えてみた

example : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) := Iff.intro (
    -- Not「任意の x に対し p x が真」と仮定する
    fun h_not_all_p : ¬ ∀ x, p x =>
    -- Not「ある x が存在し p x が偽」と仮定して、背理法を用いて証明する
    byContradiction (fun h_not_exists_not_p : ¬ ∃ x, ¬ p x =>
      -- 補題「任意の x に対し p x が真」が成り立つ
      have h_all_p : ∀ x, p x := fun x =>
        -- 「p x が偽」 を仮定して、背理法を用いて証明する
        byContradiction (fun hx : ¬ p x =>
          -- 背理法の仮定より、補題「ある x が存在し p x が偽」が成り立つ
          have h_exists_not_p : ∃ x, ¬ p x := Exists.intro x hx
          -- 一つ目の背理法の仮定と補題より矛盾が示された
          show False from h_not_exists_not_p h_exists_not_p)
      -- 仮定と補題より矛盾が示された
      show False from h_not_all_p h_all_p)
  ) (
    -- 「ある x が存在し p x が偽」を仮定する
    fun h_exists_not_p : ∃ x, ¬ p x =>
    -- 仮定より「p x が偽」な x が得られる
    h_exists_not_p.elim fun (x : α) (h_not_p : ¬ p x) =>
    -- 「任意の x に対し p x が真」を仮定する
    fun h_all_p : ∀ x, p x =>
    -- x は「p x が偽」であるが、上記の仮定より「p x が真」になるため、Not「任意の x に対し p x が真」が示された
    show False from h_not_p (h_all_p x)
  )

コードとコメントを一対一で書くのは無駄なことしている感がある、ただ数学の証明として意味のあるものを１行に収めることはわかりやすくなるかもしれない。

コメントの方は若干日本語が怪しい (Not とか。~ が偽、というのが偽、を表現するのが難しい)、だいぶブランクがあるか、元々そんなもんだったかわからないが。

感想

１行を意味のある単位で改行するのはアリかもしれない
変数名をどうするべきかはあまり考えられていない、数学のノリだと lem1 とか数字振っちゃうでもいいけど、もっと読みやすくできないだろうか？しかし文字だけで表現するのは限界があるし、定義元へジャンプできるのだからいいのかもしれない。h_∃x¬px とそのまんま記号入りで変数名考えたけど普通にダメ
インデントも悩む
とはいえ証明っぽくなってきてなかなか楽しい
byContradiction は脳に悪いということを誰かが言っていたのを思い出した
調べたら普通にスタイルガイドあるっぽい？: https://leanprover-community.github.io/contribute/style.html