ring

ring は，可換環の等式を示します．ローカルコンテキストの仮定は読まず，環の公理だけを使います．

import Mathlib.Tactic.Ring -- `ring` のために必要

variable (x y z : ℤ)

example : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 := by
  ring

example (hz : z = x + y) : x * z = x ^ 2 + x * y := by
  -- `ring` はローカルコンテキストの仮定を読まないので，これは通らない
  ring
  show x * z = x * y + x ^ 2

  -- `rw` などで，環の公理だけを使って示せる形にすれば OK
  rw [hz]
  ring

ring_nf

ring は等式を示そうとするタクティクですが，ring_nf は式を整理して標準形と呼ばれる形にします．

example {x y z : Rat} (h : z = (x + y) ^ 2) : z = x ^ 2 + 2 * x * y + y ^ 2 := by
  -- `(x + y) ^ 2` を展開する
  ring_nf at h

  -- `h` を代入して `z` を消去する
  rw [h]

  -- 後は可換環の公理から示せる
  ring

環でないものに ring を使ったら

たとえば自然数 ℕ は環ではありません．そのため，自然数の引き算などを含む式は多くの場合 ring では示せません．代わりに ring_nf を使うように促されますが，ring_nf でも示せるとは限りません．

-- Lean では自然数の引き算は
-- `n ≤ m` のとき `n - m = 0` になるように定義されている
example : 7 - 42 = 0 := rfl

-- 整数にすると結果が変わる
example : 7 - (42 : ℤ) = - 35 := rfl

/-- info: Try this: ring_nf -/
#guard_msgs in
example {n : Nat} : n - n + n = n := by
  -- `ring_nf` を提案される
  try ring

  simp

example {n : Nat} : n - n + n = n := by
  -- 提案通りに `ring_nf` を使っても効果なし
  ring_nf
  show n - n + n = n

  simp

ring の中身を見る方法

simp 等と異なり，ring? タクティクは用意されていませんが，show_term で具体的にどんなルールが適用されたのかを知ることができます． ただし，その出力結果は非常に長く読みづらいものであることがしばしばです．

example : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 := by
  try
    /-
      以下のような出力が100行以上続く
      Try this: exact Mathlib.Tactic.Ring.of_eq
      (Mathlib.Tactic.Ring.pow_congr
        ...
    -/
    show_term ring

    fail

  ring