ring
ring
は、可換環の等式を示します。ローカルコンテキストの仮定は読まず、環の公理だけを使います。
import Mathlib.Tactic.Ring -- `ring` のために必要
example (x y : ℤ) : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 := by
ring
example (x y z : ℤ) (hz : z = x + y) : x * z = x ^ 2 + x * y := by
-- `ring` はローカルコンテキストの仮定を読まないので、証明できない
fail_if_success solve
| ring
-- `rw` などで、環の公理だけを使って示せる形にすれば証明できるようになる
rw [hz]
ring
ring_nf
ring
は等式を示そうとするタクティクですが、ring_nf
は式を整理して標準形と呼ばれる形にします。ring
とは異なり、部分項の変形まで行うことができます。
example {x y : Rat} (F : Rat → Rat) : F (x + y) + F (y + x) = 2 * F (x + y) := by
ring_nf
環でないものに対する振る舞い
たとえば自然数 Nat
はマイナスがないので環ではありません。そのため、自然数の引き算などを含む式は多くの場合 ring
では示せません。代わりに ring_nf
を使うように促されますが、ring_nf
でも示せるとは限りません。
-- Lean では自然数の引き算は
-- `n ≤ m` のとき `n - m = 0` になるように定義されている
example : 7 - 42 = 0 := rfl
-- 整数にすると結果が変わる
example : 7 - (42 : ℤ) = - 35 := rfl
example {n : Nat} : n - n + n = n := by
-- `ring_nf` を提案される
ring says ring_nf
simp
example {n : Nat} : n - n + n = n := by
-- 提案通りに `ring_nf` を使っても証明できない
fail_if_success solve
| ring_nf
-- ゴールが変わっていない
guard_target =ₛ n - n + n = n
simp
自然数 Nat
は半環(環の条件のうちマイナスがあるという条件を満たさないもの)ですが、ring
は可換な半環に対しても使用することができるので自然数の和と積についての式は ring
で示すことができます。
example (n m : Nat) : (n + m) ^ 2 = n ^ 2 + 2 * n * m + m ^ 2 := by
ring
example (n m : Nat) : n * (n + m) = n ^ 2 + n * m := by
ring