rw_search

rw_search は，ゴールが等式であるときに，ライブラリにある命題を使って rw することを繰り返し，そのゴールを閉じようとするタクティクです．

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

variable (m n : ℕ)

-- `says` のチェックを有効にする
set_option says.verify true

example : (m - n) - n = m - 2 * n := by
  -- `ring` では示せない．自然数は環ではないので当然
  try ring

  -- `aesop` でも示せない
  fail_if_success aesop

  rw_search says
    rw [Nat.sub_sub, Nat.mul_two]

rw では同値関係も扱うことができますが，rw_search が扱うのは等式のみです．

/-- error: Goal is not an equality. -/
#guard_msgs in example (h : n + m = 0) : n = 0 ↔ m = 0 := by
  -- ゴールが等式でないのでエラーになる
  rw_search

-- `=` に書き換えると示せる
example (h : n + m = 0) : n = 0 ↔ m = 0 := by
  suffices (n = 0) = (m = 0) from Eq.to_iff this

  rw_search says
    rw [propext (eq_zero_iff_eq_zero_of_add_eq_zero h)]

rw?

rw? は apply? のように，ゴールを rw できる補題をライブラリから検索します．rw? は等式以外も扱うことができますが，rw_search と同様に同値関係の扱いは苦手です．

example (h : n + m = 0) : n = 0 ↔ m = 0 := by
  try
    -- 複数の候補を出してしまうが，候補は出してくれる
    rw?

    -- いったん失敗させる
    fail

  -- `=` に書き換えると一発で示せる
  suffices (n = 0) = (m = 0) from Eq.to_iff this
  rw? says
    rw [propext (eq_zero_iff_eq_zero_of_add_eq_zero h)]