[norm_cast] 属性を紹介する

.lycheeignore

@@ -2,3 +2,4 @@ https://raw.githubusercontent.com/lean-ja/lean-by-example/.*
 https://adam.math.hhu.de/#/g/leanprover-community/NNG4
 https://live.lean-lang.org/
 https://reservoir.lean-lang.org/
+https://dcbadge.limes.pink/api/server/*

Examples/Tactic/NormCast.lean

@@ -27,3 +27,84 @@ example (left : (x : ℝ) < ↑m + ↑n) (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
+  · simp [myInt.ofNat, (· ≈ ·), Setoid.r, IntBase.equiv] at h
+    exact 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
+
+set_option linter.unusedTactic false in --#
+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