Common pitfalls — symptom, cause, fix

① A def … : Prop does not go through decide

Symptom

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

error: failed to synthesize
  Decidable (Pred1 1)

Cause decide looks for an instance of Decidable, but instance search does not open up a def. Even when the body is in a decidable form (a bounded ∀, an equality of Bools, and so on), it is invisible from outside the name that wraps it.

Fix Add the instance in one line. Once unfold opens the body, the rest is found automatically.

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

② Keep Prop and Bool apart

Symptom

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)

Cause A Prop is a claim; a Bool is a value that can be computed. They are different types, so you cannot put them on either side of =. The (true = true) in the message above is a coercion Lean inserted on its own while trying to fit true into a Prop, and it shows you exactly where the types went out of step.

Fix Write the computing side in Bool, and put decide (Prop → Bool) and = true (Bool → Prop) at the boundary. The point is to gather the boundary in one place.

/-- Inside is `Prop`, outside is `Bool`. The boundary is a single `decide`. -/
def Proper (k : ℕ) (f : Fin k → Fin 3) : Bool :=
  decide (∀ i j : Fin k, Adj k i j = true → f i ≠ f j)

On the theorem side, go back to the Prop Proper k f = false when you state it. If you write the decision function as def … : Prop, you are back at ①, so whatever computes, write in Bool; in our experience that is the easier way.

③ decide covers finite things; norm_num covers numbers

Symptom

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

Cause decide handles only closed finite propositions (no free variables). Inequalities over the reals, and goals with free variables left in them, are out of its range.

Fix Numerical computation and inequalities belong to norm_num, positivity, and nlinarith. The goal above closes with a single positivity. Keep the division in mind: decide for finite exhaustion, the norm_num family for comparing numbers.

④ A large decide search fails on recursion depth

Symptom

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

Cause The search space went past the default recursion depth. The example above has 3^6 = 729 cases, and that is already enough to exceed it.

Fix Put set_option maxRecDepth 100000 in before the declaration and it goes through. But raising the depth only works when the size is within reach. One more order of magnitude and you hit a different limit (the next entry). Measured costs are in 10 What is realistically too heavy for Lean.

⑤ Raise the depth, and the next wall is the heartbeat limit

Symptom

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

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

Cause With maxRecDepth raised, running through 3^8 = 6561 cases now hits the heartbeat limit (a deterministic cap on the amount of computation). The two limits are different things.

Fix set_option maxHeartbeats 0 removes the cap, but once removed, nothing stops it. The right move, when you hit the cap, is to redo the size estimate. If you do decide to remove the cap and wait, measure the cost of 1 case first.

⑥ Natural-number subtraction truncates

Symptom

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

Cause Subtraction on ℕ is truncated to 0 wherever it would go negative. 3 - 5 = 0 goes through decide. So a - b + b = a holds only when b ≤ a. The counterexample condition omega lists, c - d ≥ 1, is exactly b > a.

Fix Three options: add the hypothesis b ≤ a, rewrite so that no subtraction is used (set a = b + c), or move to ℤ. In counting formulas, it is safest not to leave a subtraction on the left-hand side and to write the form (m+1) * |I| ≤ … instead.

⑦ With period 2, +1 and −1 become the same thing

Symptom

example : (1 : ZMod 2) = -1 := by decide     -- passes
example : (1 : ZMod 3) = -1 := by decide     -- fails

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

Cause In ZMod 2, 1 = -1. If you write a lattice with ZMod L, then at L = 2 "one step forward" and "one step back" land on the same point, and the 4 edges or 6 neighbours that were supposed to be distinct collapse.

Fix Put (2 : ZMod L) ≠ 0 or 3 ≤ L among the hypotheses, and confine its use to a single place. The collapse happens only where you name "the point one step back" as something distinct, so if you change the count to "how many times each edge appears", the condition sometimes becomes unnecessary.

⑧ Without NeZero, ZMod n is not a finite type

Symptom

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

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

Cause ZMod 0 is ℤ. So with n left general, ZMod n is not a finite type.

Fix Add [NeZero n]. It is not needed when n is a concrete number (ZMod.card 5 goes through as is). NeZero is not a "mathematical hypothesis" but a "type-level condition to rule out ZMod 0 = ℤ"; when you list the hypotheses, keep the two kinds apart (09 §06).

⑨ nlinarith does not close an equation that needs "hypotheses multiplied by variables and added"

Symptom

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

Cause This goal follows from combining the hypotheses as c · hc − d · hd − x · h1. The coefficients are variables. nlinarith only goes as far as products of pairs of hypotheses, so it cannot find this combination.

Fix When the goal is an equation that follows from a "linear combination of the hypotheses with variables as coefficients", use linear_combination. You write the coefficients yourself.

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

What makes this easy to misread is that the failure message says linarith failed. If you read that as "not enough nonlinearity" and go off adding lemmas, you take the long way round. What to read is "which combination of the hypotheses is the difference between the two sides of the goal".

⑩ field_simp normalises the denominator, and your hypothesis no longer matches

Symptom

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

Cause field_simp normalised the denominator 9n/2 − μ to 9n − 2μ. The ≠ 0 hypothesis you have is in the form before normalisation, so it cannot be used for the final step that clears the division.

Fix Rewrite the denominator into its normalised form first, and pass a ≠ 0 in that form via have. In the example above, make have h' : 9 * n - 2 * μ ≠ 0 before calling field_simp.

A note For a large rational expression, do not clear the denominators and then fire ring at the whole thing

Apply field_simp to an identity in a dozen or more variables and the expression with the denominators cleared swells enormously. Fire ring at the swollen expression and you head toward the same kind of limit as ⑪ in §05 and ④⑤ in §02.

Cut the parts with denominators out into small one-variable lemmas, close the rest with a division-free ring, and add them together at the end with linear_combination. Writing it in this form from the start is faster, and the intermediate expressions stay readable. This split is not needed while the expression is small (we confirmed that with 6 variables and 4th powers, field_simp; ring goes through as is). Keep the form in mind for when the number of variables grows.

⑪ A lemma handed to simp forms a loop

Symptom

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

Cause Finset.card_filter rewrites "count → sum", and Finset.sum_boole, which is in the default simp set, rewrites "sum → count" back again. The two form a loop.

Fix Use this lemma with rw. rw [Finset.card_filter] fires once and goes through. For any lemma you hand to simp, check that its direction of rewriting does not collide with the default set. Lean names the culprit for you as Possibly looping simp theorem, so pass that name straight to rw.

⑫ Reindexing does not move under simp

Symptom

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

error: `simp` made no progress

Cause Reindexing a sum by x ↦ x + 1 is an operation that supplies a bijection on the index set. simp does not build such bijections on its own.

Fix Give the bijection explicitly.

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)

If all you need is to swap the order of a double sum, that is Finset.sum_comm; to re-sum over an image, Finset.sum_bij or Finset.sum_nbij. Decide first "what is mapped to what by which bijection", and the lemma is determined.

⑬ A deprecated name goes through with only a warning

Symptom

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.

Cause mathlib is a moving target, so the names of tactics and lemmas get replaced. Deprecation is a warning, not an error. The check passes, and the warning gets buried in long output.

Fix Aim for 0 warnings. If warnings are left lying around, you miss the one you really need to see (declaration uses 'sorry'). Do not guess names; grep through .lake/packages/mathlib/ to confirm them. Additive names generated automatically by @[to_additive] do not show up in grep, so look up the multiplicative name and translate.

⑭ The sorry warning is a single line

Symptom

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

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

Cause sorry leaves the proof blank. The check passes, and all you get is a one-line warning. Every theorem depending on that one inherits sorryAx.

Fix Look with both grep and #print axioms. Either one alone is not enough: grep cannot follow dependencies, and #print axioms only prints when you name the declaration. The procedure is in ② and ③ of 09 How to read a statement.

⑮ lake env lean overwrites LEAN_PATH

Symptom

LEAN_PATH="$SCRATCH/olean:$(lake env printenv LEAN_PATH)" lake env lean X.lean
(the LEAN_PATH you passed has no effect)

Cause lake env rebuilds the environment, so a LEAN_PATH passed in from outside is thrown away. This is where you get stuck when you want to import a file that is not registered at the project root.

Fix Extract the value and pass it to plain lean.

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

One more thing. A module A.B is searched for only in places that have a directory A/. Listing several places in LEAN_PATH does not make a place without that directory a candidate. Copy previously built .olean files into the new workspace with the same directory layout. A reader-side summary is in 02 Getting started.