zify を紹介する

[Seasawher]

型キャスト系のタクティクはすごく重要だと思うが、取りこぼしていたかも

[Seasawher]

push_cast を活用しながら zify を使って自然数の式を整数の問題に帰着させる例

（これはどちらかというと push_cast の例かもしれない）

import Mathlib.Tactic

example (n m : Nat) (h : n ≥ m) : (n + m) * (n - m) = n * n - m * m := by
  -- `(n : Nat) - (m : Nat)` は `(n : Int) - (m : Int)` とは一致しないので、
  -- `zify してから ring` という方法では示すことができない。
  fail_if_success solve
  | zify
    ring

  zify

  have : ↑(n - m)  = (n : Int) - (m : Int) := by omega
  push_cast [this]

  replace : ↑(n * n - m * m) = (n * n : Int) - (m * m : Int) := by
    suffices goal : n * n ≥ m * m from by
      omega
    bound

  push_cast [this]
  ring

[Seasawher]

不要な仮定を除去したバージョン。

import Mathlib.Tactic

example (n m : Nat) : (n + m) * (n - m) = n * n - m * m := by
  -- `(n : Nat) - (m : Nat)` は `(n : Int) - (m : Int)` とは一致しないので、
  -- `zify してから ring` という方法では示すことができない。
  fail_if_success solve
  | zify
    ring

  have h : n ≥ m ∨ n < m := by omega
  rcases h with h | h

  -- `n < m` のとき
  case inr =>
    have : n * n < m * m := by
      qify at h ⊢
      nlinarith
    rw [show n - m = 0 from by omega]
    rw [show n * n - m * m = 0 from by omega]
    simp

  -- `n ≥ m` のとき
  case inl =>
    zify

    have : ↑(n - m)  = (n : Int) - (m : Int) := by omega
    push_cast [this]

    replace : ↑(n * n - m * m) = (n * n : Int) - (m * m : Int) := by
      suffices goal : n * n ≥ m * m from by
        omega
      bound

    push_cast [this]
    ring