unif_hint コマンドを紹介する

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 で挙動を確認する。