よくある罠 — 症状・原因・直し方

①　def … : Prop は decide に載らない

症状

def Pred1 (n : ℕ) : Prop := ∀ m ≤ n, m ∣ n → m = 1
example : Pred1 1 := by decide

error: failed to synthesize
  Decidable (Pred1 1)

原因　decide は Decidable の実例（インスタンス）を探しますが、実例の探索は def の中を開きません。中身が判定できる形（有界の ∀・Bool の等号など）でも、包んだ名前の外からは見えません。

直し方　実例を一行で足します。unfold で中身を開けば、あとは自動で見つかります。

instance : DecidablePred Pred1 := fun n => by unfold Pred1; infer_instance

②　Prop と Bool を使い分ける

症状

def Pb (n : ℕ) : Prop := n = 0
example : Pb 0 = true := rfl

error: Type mismatch
  rfl
has type
  ?m.5 = ?m.5
but is expected to have type
  Pb 0 = (true = true)

原因　Prop は「主張」で、Bool は「計算できる値」です。両者は別の型なので、= で並べられません。上の文面の (true = true) は、Lean が true を Prop に合わせようとして自動で入れた強制変換で、型がずれている場所をそのまま見せています。

直し方　計算する側を Bool で書き、境目に decide（Prop → Bool）と = true（Bool → Prop）を置きます。境目を一箇所に寄せるのが要点です。

/-- 内側は `Prop`、外側は `Bool`。境目は `decide` 一つ。 -/
def Proper (k : ℕ) (f : Fin k → Fin 3) : Bool :=
  decide (∀ i j : Fin k, Adj k i j = true → f i ≠ f j)

定理の側では Proper k f = false という Prop に戻して述べます。判定関数を def … : Prop で書くと①に戻るので、計算をするものは Bool で書くのが経験的に楽です。

③　decide の守備範囲は有限、norm_num の守備範囲は数

症状

example (x : ℝ) : 0 ≤ x ^ 2 := by decide

error: Expected type must not contain free variables
  0 ≤ x ^ 2

Hint: Use the `+revert` option to automatically clean up and revert free variables

原因　decide は閉じた（自由変数の無い）有限の命題だけを扱います。実数の上の不等式や、自由変数の残る目標は範囲外です。

直し方　数の計算と不等式は norm_num・positivity・nlinarith の側です。上の目標は positivity 一手で閉じます。有限の網羅なら decide、数の大小なら norm_num 系と分けて考えます。

④　decide の探索が大きいと再帰の深さで落ちる

症状

theorem noCol6 : ∀ f : Fin 6 → Fin 3, Proper 6 f = false := by decide

error: maximum recursion depth has been reached
use `set_option maxRecDepth <num>` to increase limit
use `set_option diagnostics true` to get diagnostic information

原因　探索空間が既定の再帰の深さを超えました。上の例は 3^6 = 729 通りで、これで既に超えます。

直し方　set_option maxRecDepth 100000 in を宣言の前に置けば通ります。ただし深さを増やして通るのは、量が足りているときだけです。もう一桁大きいと別の限界（次の項）に当たります。費用の実測は 10 Lean では現実的に厳しいものにあります。

⑤　深さを増やすと、次は heartbeat の上限に当たる

症状

error: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.

原因　maxRecDepth を上げたうえで 3^8 = 6561 通りを回すと、今度は heartbeat（決定的な計算量の上限）に当たります。二つの上限は別物です。

直し方　set_option maxHeartbeats 0 で上限を外せますが、外すと止まらなくなります。上限に当たった時点で、量の見積りをやり直すのが正しい手です。上限を外して待つ判断をするなら、先に 1 件あたりの費用を測ります。

⑥　自然数の引き算は切り捨てられる

症状

example (a b : ℕ) : a - b + b = a := by omega

error: omega could not prove the goal:
a possible counterexample may satisfy the constraints
  d ≥ 0
  c ≥ 0
  c - d ≥ 1
where
 c := ↑b
 d := ↑a

原因　ℕ の引き算は、負になるところで 0 に切り捨てられます。3 - 5 = 0 は decide で通ります。したがって a - b + b = a は b ≤ a のときだけ成り立ちます。omega が挙げている反例の条件 c - d ≥ 1 は、まさに b > a のことです。

直し方　仮定に b ≤ a を足すか、引き算を使わない形に書き換える（a = b + c と置く）か、ℤ に移すかの三つです。数え上げの式では、引き算を左辺に残さず (m+1) * |I| ≤ … の形に書くのが安全です。

⑦　周期 2 では +1 と −1 が同じものになる

症状

example : (1 : ZMod 2) = -1 := by decide     -- 通る
example : (1 : ZMod 3) = -1 := by decide     -- 通らない

error: Tactic `decide` proved that the proposition
  1 = -1
is false

原因　ZMod 2 では 1 = -1 です。格子を ZMod L で書いていると、L = 2 のとき「一つ進む」と「一つ戻る」が同じ点になり、相異なるはずの 4 辺や 6 個の近傍が潰れます。

直し方　(2 : ZMod L) ≠ 0 か 3 ≤ L を仮定に置き、それを使う箇所を一箇所に絞ります。潰れが起きるのは「一つ戻った点」を名指しで区別する所だけなので、数え方を「辺ごとに何回現れるか」に変えると条件が要らなくなることがあります。

⑧　NeZero が無いと ZMod n は有限型にならない

症状

example (n : ℕ) : Fintype.card (ZMod n) = n := ZMod.card n

error(lean.synthInstanceFailed): failed to synthesize instance of type class
  Fintype (ZMod n)

原因　ZMod 0 は ℤ です。だから n が一般のままでは ZMod n は有限型ではありません。

直し方　[NeZero n] を付けます。n が具体的な数なら要りません（ZMod.card 5 はそのまま通ります）。NeZero は「数学の仮定」ではなく「ZMod 0 = ℤ を避けるための型の条件」です——仮定の一覧を作るときは、この二種類を分けます（09 §06）。

⑨　nlinarith は「仮説に変数を掛けて足す」等式を閉じない

症状

example (x y c d : ℝ) (hc : x * c + y * d = 1 / 2) (hd : y * c - x * d = 1)
    (h1 : c * c + d * d = 1) : x = c * (1 / 2) - d * 1 := by
  nlinarith

error: linarith failed to find a contradiction
case h1
x y c d : ℝ
hc : x * c + y * d = 1 / 2
hd : y * c - x * d = 1
h1 : c * c + d * d = 1
a✝ : x < c * (1 / 2) - d * 1
⊢ False
failed

原因　この目標は、仮説を c · hc − d · hd − x · h1 と組めば出ます。係数が変数です。nlinarith は仮説どうしの積までしか作らないので、この組み合わせを見つけられません。

直し方　目標が等式で、仮説の「変数を係数とする線形結合」で出るなら linear_combination を使います。係数は自分で書きます。

  linear_combination c * hc - d * hd - x * h1

読み間違えやすいのは、失敗の文面が linarith failed であることです。「非線形が足りない」と読んで補題を足しにいくと遠回りになります。読むべきは「目標の両辺の差が、仮説のどんな組み合わせなのか」です。

⑩　field_simp が分母を正規化して、仮定が当たらなくなる

症状

example (n μ : ℝ) (h : 9 * n / 2 - μ ≠ 0) :
    (1 : ℝ) / (9 * n / 2 - μ) * (9 * n / 2 - μ) = 1 := by
  field_simp

error: unsolved goals
n μ : ℝ
h : 9 * n / 2 - μ ≠ 0
⊢ (9 * n - 2 * μ) / (9 * n - 2 * μ) = 1

原因　field_simp は分母 9n/2 − μ を 9n − 2μ に正規化しました。手元にある ≠ 0 の仮定は正規化前の形なので、割り算を消す最後の一歩に使えません。

直し方　分母を先に正規化後の形に書き換え、その形の ≠ 0 を have で渡します。上の例なら have h' : 9 * n - 2 * μ ≠ 0 を作ってから field_simp を呼びます。

覚え書き　大きな有理式は、分母を払ってから一気に ring を打たない

変数が十数個ある恒等式に field_simp を掛けると、分母を払った式が大きく膨らみます。膨らんだ式に ring を打つと、§05 の⑪ や §02 の④⑤ と同じ型の上限に向かいます。

分母のある部分を一変数の小補題に切り出し、残りを割り算の無い ring で閉じ、最後に linear_combination で足します。最初からこの形で書くほうが速く、途中の式も読めます。この書き分けは、式が小さいうちは必要ありません（変数 6 つ・4 乗だと field_simp; ring がそのまま通るのを確かめました）。変数の数が増えたときにこの形を思い出せるようにしておきます。

⑪　simp に渡した補題が環になる

症状

example (s : Finset ℕ) (p : ℕ → Prop) [DecidablePred p] :
    (s.filter p).card = ∑ x ∈ s, if p x then 1 else 0 := by
  simp [Finset.card_filter]

warning: Possibly looping simp theorem: `Finset.card_filter`

Note: Possibly caused by: `Finset.sum_boole`

error: Tactic `simp` failed with a nested error:
maximum recursion depth has been reached

原因　Finset.card_filter は「個数 → 和」に書き換え、既定の simp 集合に入っている Finset.sum_boole は「和 → 個数」に戻します。二つで環になります。

直し方　この補題は rw で使います。rw [Finset.card_filter] なら一回だけ当たって通ります。simp に渡す補題は、書き換えの向きが既定の集合と衝突しないかを見ます。Lean が Possibly looping simp theorem と名指ししてくれるので、その名前をそのまま rw に回します。

⑫　添字の付け替えは simp では動かない

症状

example (f : ZMod 5 → ℕ) : ∑ x : ZMod 5, f (x + 1) = ∑ x : ZMod 5, f x := by
  simp

error: `simp` made no progress

原因　和の添字を x ↦ x + 1 で付け替えるのは、添字の集合の上の全単射を与える操作です。simp はそういう全単射を自分では作りません。

直し方　全単射を明示して渡します。

example (f : ZMod 5 → ℕ) : ∑ x : ZMod 5, f (x + 1) = ∑ x : ZMod 5, f x :=
  Fintype.sum_equiv (Equiv.addRight (1 : ZMod 5)) _ _ (fun _ => rfl)

二重の和の順序を入れ替えるだけなら Finset.sum_comm、像で足し直すなら Finset.sum_bij・Finset.sum_nbij です。「何を何に写す全単射か」を先に決めると、補題は一つに決まります。

⑬　非推奨になった名前は、警告だけ出して通る

症状

example (p : ℕ → Prop) (h : ¬ ∀ n, p n) : ∃ n, ¬ p n := by
  push_neg at h
  exact h

warning: `push_neg` has been deprecated. Prefer using `push Not` instead.

原因　mathlib は動いているので、戦術や補題の名前は入れ替わります。非推奨は警告で、エラーではありません。だから検査は通り、長い出力の中に埋もれます。

直し方　警告 0 を目標にします。警告が残っていると、本当に見たい警告（declaration uses 'sorry'）を見落とします。名前は当てずっぽうで書かず、.lake/packages/mathlib/ を grep して確かめます。@[to_additive] で自動生成された加法版の名前は grep に掛からないので、乗法版の名前で引いて読み替えます。

⑭　sorry の警告は一行だけ

症状

theorem gap : 1 + 1 = 2 := by sorry

warning: declaration uses `sorry`
'gap' depends on axioms: [sorryAx]

原因　sorry は証明を空欄にします。検査は通り、出るのは一行の警告だけです。その定理に依存する定理は全部 sorryAx を引き継ぎます。

直し方　grep と #print axioms の両方で見ます。片方だけでは足りません——grep は依存先まで追えず、#print axioms は宣言を名指ししないと出ないからです。手順は 09 言明を読む手順の②③にあります。

⑮　lake env lean は LEAN_PATH を上書きする

症状

LEAN_PATH="$SCRATCH/olean:$(lake env printenv LEAN_PATH)" lake env lean X.lean
（自分で渡した LEAN_PATH が効かない）

原因　lake env は環境を作り直すので、外から渡した LEAN_PATH は捨てられます。ルートに登録していないファイルを import したいときに、ここで詰まります。

直し方　値を取り出して、素の lean に渡します。

LP="$(lake env printenv LEAN_PATH)"
LEAN_PATH="$SCRATCH/olean:$LP" lean Proofs/X.lean

もう一つ。モジュール A.B は「A/ という階層を持つ場所」だけで探されます。LEAN_PATH に複数並べても、階層の無い場所は候補になりません。前に作った .olean は、新しい作業場に同じ階層で写します。読む側としてまとめたものが 02 使い方の入口にあります。