norm_cast

norm_cast は、型キャスト（ある型からある型への変換）と型強制を簡約するタクティクです。

詳細については論文 「Simplifying Casts and Coercions」 などを参照してください。

import Mathlib.Tactic

-- `x, m, n` は自然数とする
variable (x m n : ℕ)

example (left : (x : ℝ) < ↑m + ↑n) (right : ↑m + ↑n < (x : ℝ) + 1) : False := by
  -- `linarith` では示すことができない
  fail_if_success linarith

  -- `omega` でも示すことができない
  fail_if_success omega

  -- 仮定の `left` と `right` は実数上の不等式だが、
  -- 自然数上の不等式と解釈できるはずである。
  -- `norm_cast` はそれを実行してくれる。
  norm_cast at left right

  -- 仮定が自然数における不等式に変わった！
  guard_hyp left : x < m + n
  guard_hyp right : m + n < x + 1

  -- 後は `omega` で示せる
  omega

[norm_cast] 属性によるカスタマイズ

命題に [norm_cast] 属性を付与することにより、norm_cast タクティクでできることを増やすことができます。

/-- 自然数のペア -/
def IntBase := ℕ × ℕ

/-- 自然数のペアが「整数として等しい」という同値関係 -/
def IntBase.equiv : IntBase → IntBase → Prop :=
  fun (a₁, b₁) (a₂, b₂) => a₁ + b₂ = b₁ + a₂

/-- `IntBase` と同値関係 `IntBase.equiv` をペアにする -/
instance IntBase.setoid : Setoid IntBase where
  r := IntBase.equiv
  iseqv := by
    constructor
    case refl =>
      intro ⟨x, y⟩
      dsimp [IntBase.equiv]
      ac_rfl
    case symm =>
      intro ⟨x, y⟩ ⟨x', y'⟩ h
      dsimp [IntBase.equiv] at *
      omega
    case trans =>
      intro ⟨x, y⟩ ⟨x', y'⟩ ⟨x'', y''⟩ hxy hyz
      dsimp [IntBase.equiv] at *
      omega

/-- 自前で定義した整数 -/
abbrev myInt := Quotient IntBase.setoid

/-- 自然数を `myInt` と解釈する関数 -/
def myInt.ofNat (n : ℕ) : myInt := ⟦(n, 0)⟧

/-- 型強制を定義 -/
instance : Coe Nat myInt where
  coe := myInt.ofNat

/-- 型キャストの簡約を行う補題。`ℕ` の項が `myInt` として等しいなら、元から等しい。 -/
theorem myInt_eq {x y : ℕ} : (x : myInt) = (y : myInt) ↔ x = y := by
  constructor <;> intro h
  · simpa [myInt.ofNat, (· ≈ ·), Setoid.r, IntBase.equiv] using h
  · rw [h]

-- `[norm_cast]` 属性の制約として、
-- 登録する補題の中には型強制が含まれていなくてはいけない
-- たとえば `↑` など
/--
error: norm_cast: badly shaped lemma, lhs must contain at least one coe
  myInt.ofNat x = myInt.ofNat y
-/
#guard_msgs in
  attribute [norm_cast] myInt_eq

-- `[coe]` 属性を付与し、`myInt.ofNat` を型キャストを行う関数として認識させる
attribute [coe] myInt.ofNat

example {x y z : ℕ} (h : (x : myInt) = (y : myInt)) : x + z = y + z := by
  norm_cast at h

  -- `norm_cast` の効果が出ていない
  guard_hyp h : (x : myInt) = (y : myInt)

  simp [myInt_eq] at h
  omega

-- `norm_cast` に使ってもらえるように登録する
attribute [norm_cast] myInt_eq

example {x y z : Nat} (h : (x : myInt) = (y : myInt)) : x + z = y + z := by
  norm_cast at h

  -- `norm_cast` で簡約できるようになった！
  guard_hyp h : x = y

  omega