Lean unif_hint 使用例調査メモ
結論：Lean 4 のコマンド名は基本的に unif_hint です。local unif_hint / scoped unif_hint の形でも使えます。構文は概ね次です。≟ と =?= は同じ用途の記法として使われています。Lean 本体の Init.NotationExtra に構文定義があります。 oai_citation:0‡GitHub
unif_hint 名前? (束縛変数...) where
前提制約1
前提制約2
⊢ 結論制約
例：
unif_hint (p : Prop) where
⊢ Not p =?= p → False
これは Lean 本体 Init/Hints.lean にある例で、Not p と p → False を定義展開が弱い場面でも同一視しやすくするためのヒントです。 
1. Magma の例
Zulip で出ている最小例です。S =?= Nat.Magma が分かったとき、S.α =?= Nat を解かせるヒントです。 
structure Magma where
α : Type
mul : α → α → α
instance : CoeSort Magma Type where
coe M := M.α
infixl:70 (priority := high) "**" => Magma.mul _
def Nat.Magma : Magma where
α := Nat
mul a b := Nat.mul a b
unif_hint (S : Magma) where
S =?= Nat.Magma
|-
S.α =?= Nat
#check (3 : Nat) ** (3 : Nat)
ポイント：
unif_hint は「結論を直接証明する」のではなく、この形の単一化問題が来たとき、前提制約を追加して解かせるためのものです。
2. Quiver の積で射の型を推測させる例
Zulip の長い実験例では、積 quiver の射
(a, b) ⟶ (a', b')
が
(a ⟶ a') × (b ⟶ b')
と定義的に等しいにもかかわらず、Lean がメタ変数をうまく埋められない場面で unif_hint を使っています。 
universe u v
class Hom (α : Type u) : Sort (max u v + 1) where
hom : α → α → Sort v
infixr:10 " ⟶ " => Hom.hom
structure Quiver : Type (max u v + 1) where
α : Type u
hom : α → α → Sort v
instance : CoeSort Quiver (Type u) where
coe Q := Q.α
instance (Q : Quiver.{u,v}) : Hom.{u,v} Q where
hom := Q.hom
structure Prefunctor (Q R : Quiver.{u,v}) : Type (max u v) where
obj : Q → R
map {x y : Q} : (x ⟶ y) → (obj x ⟶ obj y)
infixr:26 "⥤" => Prefunctor
def product_quiver (Q R : Quiver) : Quiver where
α := Q × R
hom a b := (a.1 ⟶ b.1) × (a.2 ⟶ b.2)
infixr:70 "⊗" => product_quiver
def symm (Q R : Quiver) : Q ⊗ R ⥤ R ⊗ Q where
obj := fun (a, b) => (b, a)
map := fun (f, g) => (g, f)
local unif_hint (C D : Quiver) (c : C) (d d' : D) (x : C ⊗ D) where
x =?= (c, d)
⊢ d' =?= x.2
local unif_hint (C D : Quiver) (c c' : C) (d : D) (x : C ⊗ D) where
x =?= (c, d)
⊢ c' =?= x.1
theorem symm_map₁ {A B : Quiver}
{a a' : A} {b b' : B}
(f : a ⟶ a') (g : b ⟶ b') :
(symm A B).map (f, g) = (g, f) := rfl
ここで重要なのは、右辺の d' や c' を 新しい変数として置いている点です。
3. 悪い例：循環して最大再帰深度に達する
同じ Zulip 投稿では、次のようなヒントは危険だと報告されています。 
local unif_hint (C D : Quiver) (c : C) (d : D) (x : C ⊗ D) where
x =?= (c, d)
⊢ d =?= x.2
local unif_hint (C D : Quiver) (c : C) (d : D) (x : C ⊗ D) where
x =?= (c, d)
⊢ c =?= x.1
この形だと、Lean が x =?= (c, d) を確認する過程でまた同じヒントを呼び、循環して
maximum recursion depth has been reached
になり得ます。
修正版は次です。
local unif_hint (C D : Quiver) (c : C) (d d' : D) (x : C ⊗ D) where
x =?= (c, d)
⊢ d' =?= x.2
local unif_hint (C D : Quiver) (c c' : C) (d : D) (x : C ⊗ D) where
x =?= (c, d)
⊢ c' =?= x.1
4. Finset → Set coercion 周辺の例
Zulip では、Finset α を Set α に coercion したときの単一化補助として次のような案が出ています。 
import Mathlib.Data.Finset.Basic
unif_hint guess {α : Type*} (s : Finset α) (t : Set α) (x : α) where
(s : Set α) =?= t ⊢ (x ∈ s) =?= (x ∈ t)
これは「s と t が coercion 後に一致するなら、membership の型も一致させる」という方向のヒントです。
注意点
* unif_hint は強力だが、かなり低レベル。
* 誤ったヒントを書くと、Lean の単一化器に「本当は残すべき制約」を忘れさせることがある。
* Zulip の投稿でも「ill-formed unification hint により Lean が制約を整合的だと信じてしまう」危険が指摘されています。 
* 2025年の Lean issue でも、unsound な unif_hint がクラッシュを引き起こす例が報告されています。 
実用上の目安
unif_hint は通常の simp, coercion, typeclass, instance, notation 設計で解決できないときの最終手段です。
使うなら、次の用途に限定するのが安全です。
1. 構造体・coercion・射記法などの展開後に明らかな単一化を補助する。
2. 結論制約の両辺が弱頭正規形でマッチしやすい形にする。
3. 既存変数を無理に再利用せず、新しいメタ変数を導入して循環を避ける。
4. set_option trace.Meta.isDefEq true と set_option trace.Meta.isDefEq.hint true で挙動を確認する。
Lean
unif_hint使用例調査メモ結論：Lean 4 のコマンド名は基本的に
unif_hintです。local unif_hint/scoped unif_hintの形でも使えます。構文は概ね次です。≟と=?=は同じ用途の記法として使われています。Lean 本体のInit.NotationExtraに構文定義があります。 oai_citation:0‡GitHub