Lean: dubious noncomputability

Question

In Lean, some definitions must be marked as noncomputable, for example if they depend on the law of the excluded middle or other nonconstructive choice principles. Usually, the reason for noncomputability is obvious. Occasionally, however, Lean will tell me that something must be marked as noncomputable even though it seems perfectly constructive to me. The example that I am facing at the moment involves long and complicated definitions spread over a number of files, so I cannot give a self-contained explanation here. Are there good general methods for diagnosing this kind of issue?

Answer 1

The purpose of the noncomputability checker is to (try to) determine whether or not the VM compiler will succeed in making executable bytecode, which can be evaluated more efficiently (by #eval for instance). One thing to keep in mind is that "computability" is not a property that's verified by the Lean kernel, so if you're not planning on evaluating your definitions, the easiest thing to do is to just put noncomputable theory at the top of your modules :-). Lean will still compile definitions that pass the noncomputability checker when in this mode -- it just won't complain at you if you neglect to annotate noncomputable definitions with noncomputable.

That said, there are a few tricks to get things to be computable. Overall, what the noncomputability checker is trying to do is determine whether there is a noncomputable function being used within the computationally relevant part of the definition. The following are computationally irrelevant: anything that is Prop-valued (that includes set), anything that is Type-valued, proofs, and the parameters/indices that are the first arguments to a recursor or a constructor. (Note that a definition can depend on the law of the excluded middle and still be computable -- the way it usually would be noncomputable is if you're depending on the classical decidable instance for em in the computationally relevant part of the definition.)

Sometimes there are functions that use noncomputable arguments in a computationally irrelevant way. You can try using the @[inline] attribute for this since the noncomputability checker will inline definitions with this attribute while checking.

Sometimes it's that you're accidentally using a theorem/lemma instead of a def. Only def's are compiled, so technically theorems are noncomputable (in the next release of Lean 3 there will be a more user-friendly error message for this).

Sometimes it's that you're using a noncomputable instance somewhere. If you can figure out what it is, you can write a computable instance for the given types. The @[inline] trick can also be useful here if those instances aren't used in a computationally relevant way. (This shows up in mathlib for some constructors for homomorphisms, though while these constructors are computable, they're not really usefully computable.)

Answer 2

(assuming Lean 3): There is a command called environment.decl_noncomputable_reason in Lean 3.35c or later that may help you diagnose the reason for noncomputability, or at least the declaration in question, it can be used as follows

open tactic
noncomputable!
def aa := 1
noncomputable theory
def bb := aa
run_cmd do
  e ← get_env,
  trace $ e.decl_noncomputable_reason ``bb -- (some aa)

Using this hopefully you can find the location of the mismatch, and update the question with more info if needed.