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?
3$\begingroup$ "Occasionally, however, Lean will tell me that something must be marked as noncomputable even though it seems perfectly constructive to me" - can you include the exact message it uses when it tells you this? $\endgroup$– Eric ♦May 16, 2022 at 16:50
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
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
lemma instead of a
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.)
$\begingroup$ Indeed, the problem was just a
lemmathat should have been changed to
defwhen I modified it to return a witness rather than a bare existential statement. $\endgroup$ May 16, 2022 at 17:06
(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.
$\begingroup$ Since it's not documented: it returns the declaration name itself if it's a
theorem, since theorems are inherently noncomputable. $\endgroup$ May 16, 2022 at 16:47
1$\begingroup$ Note this shouldn't be necessary to use explicitly; the error message that says "missing noncomputable" already tells you what the reason is. $\endgroup$– Eric ♦May 16, 2022 at 16:49
$\begingroup$ @Eric good point, maybe the only relevant part of my answer is to be sure to use Lean 3.35 or greater then! $\endgroup$ May 16, 2022 at 22:45
$\begingroup$ I don't think you need such a recent version; that version just happens to be the one where I exposed the C++ API to tactic code. The behavior of showing the reason predates that. Perhaps only the community release has it though... $\endgroup$– Eric ♦May 16, 2022 at 22:56
1$\begingroup$ @Eric That is an old feature, dating to the official release: github.com/leanprover/lean/blob/master/src/frontends/lean/… $\endgroup$ May 17, 2022 at 13:14