`decide` タクティクはなぜ irreducible だと動作しなくなるのか

一言で言うと、通常の decide は #eval 的な実行ではなく、Decidable p の項を“透明性設定つきの簡約”で isTrue h まで落とそうとするからです。@[irreducible] はその簡約を止めます。

Lean のリファレンスでも、decide は目標 p に対して Decidable p を合成し、それを簡約して isTrue h になれば、その h : p で目標を閉じる、と説明されています。さらに decide +kernel はカーネル簡約を使うため透明性を無視して展開でき、decide +native / native_decide は #eval を使う別モードだとされています。([Lean Language]1)

たとえば概念的には、目標が

f a = b

なら、decide はだいたい次のようなものを作ろうとします。

inferInstance : Decidable (f a = b)

これが簡約によって

Decidable.isTrue h

まで落ちれば、h : f a = b が得られます。

しかし f が @[irreducible] だと、通常のメタレベル簡約では f a を展開しません。Lean の定義は δ 簡約で本体へ置き換わり得ますが、エラボレータ側ではこの展開が reducibility によって制御されます。([Lean Language]2) そのため、たとえば Nat の等号判定が内部で

decEq (f a) b

のような形になっていても、f a が 0 や Nat.succ ... まで見えないので、判定計算がそこで止まります。結果として isTrue h まで簡約できず、decide は失敗します。

ここで混同しやすいのは、「評価」には少なくとも二種類あるという点です。

#eval f a

はコンパイラ／実行系によるプログラム実行です。これは @[irreducible] な定義でも、実装本体を持っていれば実行できます。

一方、通常の

by decide

は「実行して true だったから信じる」という処理ではありません。Lean が信頼できる証明項を構成するために、Decidable p の項を論理側の簡約で isTrue h まで落とそうとしています。この簡約は通常、透明性設定を尊重します。だから irreducible に邪魔されます。

対応策は状況ごとに違います。

@[irreducible] def f : Nat := 3

example : f = 3 := by
  -- decide        -- 通常は失敗し得る
  decide +kernel

decide +kernel は透明性を無視してカーネルで簡約するので、単に @[irreducible] が原因なら通ることがあります。リファレンスでも +kernel は透明性を無視して展開すると説明されています。([Lean Language]1)

また、

example : f = 3 := by
  native_decide

のように native_decide を使う手もあります。これは decide +native の別名で、#eval によって Decidable インスタンスを評価します。ただし、これは Lean コンパイラや @[implemented_by] 付き実装の正しさを信頼基盤に加える、というトレードオフがあります。([Lean Language]1)

要するに、

#eval で計算できる
≠
通常の decide が証明項として受理できる形まで簡約できる

です。

decide が必要としているのは単なる Bool の計算結果ではなく、最終的には

h : f a = b

という証明です。通常モードでは、その証明を Decidable.isTrue h の形で簡約から取り出す必要がある。その簡約が @[irreducible] によって止まる、というのが本質です。

The issue names no repository file, test, or documentation entry point. First clarify where this explanation of decide, decide +kernel, and native_decide should be added, then review the linked Tactic Reference and Definitions pages. Done should mean the intended documentation includes the distinction between proof reduction and evaluation, with the shown examples and trade-offs.