Lean 5

「はじめての数理論理学」山田俊行著，森北出版．2018．に記載されている演習問題を Lean で解いてみた．

-- 「はじめての数理論理学」山田俊行著，森北出版．2018
-- p.55 2-5 演習問題 
import Mathlib.Tactic

-- 演習問題 2.1 奇数と平方
-- 奇数の平方はみな奇数である．
example : ∀ (n : ℤ), Odd (n) → Odd (n * n) := by
  intro n h -- 任意の奇数 n をとってくる．
  have ⟨k, hk⟩ := h -- n = 2 * k + 1 となる k をとってくる．
  use 2 * k^2 + 2 * k
  calc n * n 
  _ = (2 * k + 1) * (2 * k + 1)   := by rw [hk]
  _ = 4 * k^2 + 4 * k + 1         := by ring
  _ = 2 * (2 * k^2 + 2 * k) + 1   := by ring

-- 演習問題 2.2 偶数と平方
-- ５倍すると偶数である整数はみな，平方しても偶数である．
-- 証明の方針：Even (5 * n) → Even (n) → Even (n * n) を示す．
example : ∀ (n : ℤ), Even (5 * n) → Even (n * n) := by
  intro n (hn : Even (5 * n))
  obtain ⟨ k, hk ⟩ := hn -- 5 * n = k + k となる k をとってくる．

  -- Goalを Even (n * n) から Even n に変えるため，Even n → Even (n * n) を示す
  suffices Even n from by
    -- Even n を仮定し，n = m + m となる m をとってくる．
    obtain ⟨ m, hm ⟩ := this -- this は Even n である．hm は n = m + m
    exists 2 * m ^ 2 -- n * n を N としたとき，N = M + M となる M をとってくる．
    rw [hm] -- n * n を n = m + m （仮定）で置き換えると (m + m) * (m + m) となる．
    ring -- (m + m) * (m + m) = 2 * m ^ 2 + 2 * m ^ 2 が成り立つことは明らか．

  -- ここからは Even n が Goal
  -- 5 * n = k + k → 5 * n = 2 * k を示す（仮定hkを置き換える）
  replace hk : 5 * n = 2 * k := by 
    rw [hk] -- 5 * n を仮定どおり k + k に置き換える．
    ring -- k + k = 2 * k が成り立つことは明らか．

  -- n = 2 * (k - 2 * n) を示す．
  have := by
    calc n
      _ = 5 * n - 4 * n := by ring
      _ = 2 * k - 4 * n := by rw [hk]
      _ = 2 * (k - 2 * n) := by ring
  
  exists k - 2 * n -- n = m + m となる m をとってくる．
  -- ここからは Goal が n = k - 2 * n + (k - 2 * n) になる．
  -- ＃hk は replace しているが，Even n の定義は n = m + m のまま．
  nth_rewrite 1 [this] -- 先に示した n = 2 * (k - 2 * n) で，Goal の１番目の n を置き換える
  -- 普通に rw する右項の n も置き換わってしまう．
  ring -- 2 * (k - 2 * n) = k - 2 * n + (k - 2 * n) が成り立つことは明らか．

演習問題 2.2 は自力で解けず，途方にくれていたところ，code for math で助けを求めたら，@Kitamado さんに上記解法を教えていただいた．
suffices, exists, nth_rewrite などの tactic はこれまで使用したことがなかったため，大変勉強になり感謝．
また，Lean の tactic を調べるのに有用なサイト Lean4 タクティク逆引きリスト も教えていただいた．

以下は suffices の使い方に慣れるために解いた問題．

-- suffices の使い方の練習
example (a b c : ℕ) : a = b → b = c → a + a = c + c := by
  intros h1 h2
  -- a + a = c + c を証明するには，a + a = b + b を示せば十分であることを示す．
  -- つまり，a + a = b + b → a + a = c + c を示す．
  suffices a + a = b + b from by
    calc a + a
      _ = b + b := by rw [this]
      _ = c + c := by rw [h2]
    -- calc の代わりに rw [this, h2] だけでもよい．

  -- ここからは Goal が a + a = b + b となる．
  calc a + a
    _ = b + b := by rw [h1]
  -- calc の代わりに rw [h1] だけでもよい．