`[norm_cast]` 属性を紹介する

[Seasawher]

norm_cast タクティクは、補題を登録することによりカスタマイズすることが可能である。どういう補題を登録することにより何が可能になるのか解説したい。

[Seasawher]

Mathlib には以下のような例がある：

@[norm_cast, simp 1001]
-- porting note: increase priority to prevent the left-hand side from simplifying
theorem norm_cast_real (r : ℚ) : ‖(r : ℝ)‖ = ‖r‖ :=
  rfl

[Seasawher]

なぜかうまくいかない

import Mathlib.Tactic

def IntBase := Nat × Nat

def IntBase.equiv : IntBase → IntBase → Prop :=
  fun (a₁, b₁) (a₂, b₂) => a₁ + b₂ = b₁ + a₂

instance : 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

def myInt := Quot IntBase.equiv

instance : Coe Nat myInt where
  coe n := ⟦(n, 0)⟧

example (x y : Nat) (h : (x : myInt) = (y : myInt)) : x = y := by
  -- 変化なし
  norm_cast at h
  sorry

theorem myInt_eq {x y : Nat} : (↑x : myInt) = (↑y : myInt) ↔ x = y := by
  constructor <;> intro h
  · simp [(· ≈ ·), Setoid.r, IntBase.equiv] at h
    exact h
  · rw [h]

/--
error: norm_cast: badly shaped lemma, lhs must contain at least one coe
  ⟦(x, 0)⟧ = ⟦(y, 0)⟧
-/
#guard_msgs in
attribute [norm_cast] myInt_eq

/-- 正の自然数を表す型 -/
def Pos := { n : Nat // n > 0 }

/-- `Pos` に対して大小比較を定義する -/
instance : LE Pos where
  le x y := x.val ≤ y.val

/-- `n : Pos` を自然数に自動で変換する -/
instance : Coe Pos Nat where
  coe n := n.val

theorem le_of_pos_le {x y : Pos} (h : (x : Nat) ≤ y) : x ≤ y := by
  exact h

/--
error: norm_cast: lemma must be = or ↔, but is
  (↑x).le ↑y
-/
#guard_msgs in
  attribute [norm_cast] le_of_pos_le

example {x y : Pos} (h : (x : ℕ) ≤ y) : x ≤ y ∨ False := by
  norm_cast at h
  sorry

@[norm_cast]
theorem le_iff_pos_le {x y : Pos} : (x : ℕ) ≤ (y : ℕ) ↔ x ≤ y := by
  constructor <;> intro h
  · apply le_of_pos_le
    exact h
  · exact h

example {x y : Pos} (h : (x : ℕ) ≤ y) : x ≤ y ∨ False := by
  norm_cast at h
  exact Or.inl h

[Seasawher]

Zulip: >
unexpected error on [norm_cast]