Lean 4

Leanの演習問題をChatGPTに作ってもらい，それを解いてみる．
ChatGPTへのプロンプトは以下

#命令書:
あなたは、定理証明支援系のプログラミング言語Lean4のプログラマーです．
以下の制約条件に基づき，Lean4の証明問題を3つ出して下さい．

#制約条件:
・数理論理の問題であること
・証明問題は example を用いること

それでは証明問題を３つ出して下さい．

このプロンプトで出てきた問題を解いてみたのが以下．

-- 論理積（AND）の交換法則を示す定理を証明してください。
example (P Q : Prop) : P ∧ Q ↔ Q ∧ P :=
  Iff.intro
    (fun hPQ : P ∧ Q => And.intro hPQ.right hPQ.left)
    (fun hQP : Q ∧ P => And.intro hQP.right hQP.left)

-- 論理和（OR）の分配法則を示す定理を証明してください。
example (P Q R : Prop) : P ∨ (Q ∧ R) ↔ (P ∨ Q) ∧ (P ∨ R) := by
  constructor
  · intro hPQR -- P ∨ (Q ∧ R) → (P ∨ Q) ∧ (P ∨ R) の証明における仮定
    cases hPQR
    case inl hP => exact And.intro (Or.inl hP) (Or.inl hP)
    case inr hQR => exact And.intro (Or.inr hQR.left) (Or.inr hQR.right)
  · intro hPQPR -- (P ∨ Q) ∧ (P ∨ R) → P ∨ (Q ∧ R) の証明における仮定
    -- 仮定のANDから左右の命題を取り出す
    have hPQ : P ∨ Q := by apply hPQPR.left
    have hPR : P ∨ R := by apply hPQPR.right
    cases hPQ
    case inl hP => exact Or.inl hP -- Pが成り立つ時，P ∨ (Q ∧ R) の Or の左のPが成り立つ
    case inr hQ => -- Qが成り立つ時
      cases hPR -- 一方の P ∨ R の各ケースを考える
      case inl hP => exact Or.inl hP -- Pが成り立つ時，P ∨ (Q ∧ R) の Or の左のPが成り立つ
      case inr hR => exact Or.inr (And.intro hQ hR) -- Rが成り立つ時，P ∨ (Q ∧ R) の Or の右の Q ∧ R が成り立つ
    -- モヤモヤ：cases hPR から始める証明が不要なのは，QとRが対称な関係だからかな

-- 否定（NOT）の二重否定法則を示す定理を証明してください。
example (P : Prop) : ¬¬P ↔ P := by
  have h : P ∨ ¬P := by apply Classical.em
  constructor
  · intro hnnP -- ¬¬P を仮定し P を示す
    cases h -- 排中律 P ∨ ¬P を持ってくる
    case inl => assumption -- Pが成り立つ場合はOK
    case inr => contradiction -- ¬Pを仮定すると矛盾よってPが成り立つ
  · intro hP -- P を仮定し ¬¬P を示す
    intro hnP -- ¬P を仮定すると
    contradiction -- Pと矛盾するので ¬¬P が成り立つ
-- 以下はassumption, contradictionを使わない別解
example (P : Prop) : ¬¬P ↔ P := by
  have h : P ∨ ¬P := by apply Classical.em
  constructor
  · intro hnnP -- ¬¬P を仮定し P を示す
    cases h -- 排中律 P ∨ ¬P を持ってくる
    case inl hP => exact hP -- Pが成り立つ場合はOK
    case inr hnP => apply False.elim (hnnP hnP)-- ¬Pを仮定すると矛盾よってPが成り立つ
  · intro hP -- P を仮定し ¬¬P を示す
    intro hnP -- ¬P を仮定すると
    apply False.elim (hnP hP) -- Pと矛盾するので ¬¬P が成り立つ
    -- False.elimの後にはFalse（矛盾）する命題を入れればよい．

結構勉強になったので，ChatGPTに演習問題を出してもらうのはありかも．