TsumuraのProblem402をLeanで形式化した

以下のような内容の数学の問題をLeanで形式化しました。

群 $G$ に対して、以下が成り立つとする。

• 任意の $x, y \in G$ に対して $(x * y)^3 = x^3 * y^3$ が成り立つ。
• 任意の $x \in G$ に対して $x^3 = e → x = e$ が成り立つ。ただし$e$は単位元。

このとき$G$は可換群である。

以下が証明のソースコードです。

import Mathlib.Tactic

-- `G`は群
variable {G : Type} [Group G]

-- `grind`に足りない補題を登録する
attribute [grind _=_] Semigroup.mul_assoc
attribute [grind =] pow_succ' pow_one conj_pow

/-- 交換子の基本的な性質 -/
@[grind =]
theorem commutator_spec (x y : G) :
    x * y * x⁻¹ * y⁻¹ = 1 ↔ x * y = y * x := by
  constructor <;> intro h
  · calc
      _ = x * y := by rfl
      _ = x * y * x⁻¹ * y⁻¹ * (y * x) := by group
      _ = y * x := by simp [h]
  · simp [h]

/-- 2乗する写像が積を保つのであれば、その群は可換 -/
@[grind =]
theorem abelian_of_square (h : ∀ x y : G, (x * y)^2 = x^2 * y^2) :
    ∀ x y : G, x * y = y * x := by
  intro x y
  calc
    _ = x * y := by rfl
    _ = x⁻¹ * (x^2 * y^2) * y⁻¹ := by group
    _ = x⁻¹ * (x * y)^2 * y⁻¹ := by rw [h x y]
    _ = x⁻¹ * (x * y * x * y) * y⁻¹ := by grind
    _ = y * x := by group

/-- `n`乗写像が積を保ち、単射であるとする。
このとき`n`乗して可換ならば、もともと可換 -/
@[grind =>]
theorem reduce_nth_power (n : Nat)
  (hpow : ∀ x y : G, (x * y)^n = x^n * y^n)
  (htor : ∀ x : G, x^n = 1 → x = 1) :
    ∀ x y : G, x * y^n = y^n * x → x * y = y * x := by
  intro x y hcomm
  have : (x * y * x⁻¹ * y⁻¹)^n = 1 := calc
    _ = (x * y * x⁻¹)^n * (y⁻¹)^n := by grind
    _ = (x * y^n * x⁻¹) * (y⁻¹)^n := by grind
    _ = y^n * x * x⁻¹ * (y⁻¹)^n := by grind
    _ = 1 := by simp
  grind

theorem main_theorem
  (hpow : ∀ x y : G, (x * y)^3 = x^3 * y^3)
  (htor : ∀ x : G, x^3 = 1 → x = 1) :
    ∀ x y : G, x * y = y * x := by

  have lem1 : ∀ x y : G, x^3 * y^2 = y^2 * x^3 := by
    intro x y
    calc
      _ = x ^ 3 * y ^ 2 := by rfl
      _ = x ^ 3 * y ^ 3 * y⁻¹ := by group
      _ = (x * y)^3 * y⁻¹ := by grind
      _ = y⁻¹ * y * (x * y)^3 * y⁻¹ := by simp
      _ = y⁻¹ * (y * (x * y) * y⁻¹)^3 := by grind
      _ = y⁻¹ * (y * x)^3 := by group
      _ = y⁻¹ * (y^3 * x^3) := by grind
      _ = y^2 * x^3 := by group

  have lem2 : ∀ x y : G, x * y^2 = y^2 * x := by
    intro x y
    have := reduce_nth_power 3 hpow (by grind) (y^2) x
    grind

  have lem3 : ∀ x y : G, (x * y)^2 = x^2 * y^2 := by
    intro x y
    calc
      _ = (x * y)^2 := by rfl
      _ = (x * y)^3 * (x * y)⁻¹ := by simp [pow_succ']; group
      _ = x^3 * y^3 * (y⁻¹ * x⁻¹) := by rw [hpow x y]; group
      _ = x^3 * y^2 * x⁻¹ := by group
      _ = (y^2 * x^3) * x⁻¹ := by rw [lem1 x y]
      _ = y^2 * x^2 := by group
      _ = x^2 * y^2 := by rw [lem2 _ _]

  grind

感想

group タクティクが意外と弱くてしんどかったですね。grind が全部やってくれると思いきやそうでもないし、Mathlib は Lean 本家の更新に追い付いていないのかもなという気持ちになりました。

参考文献

この問題は Tsumura の Problem 402 に由来します。