ring_nf のページを独立させる

[Seasawher]

タクティクとして別物として扱いたい気持ちがある。

（このリファレンスは辞書として使われることも想定しているので、基本的には見出し語に載せておきたい。）

[Seasawher]

/- ## 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