4
$\begingroup$

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?

$\endgroup$
1
  • 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 at 16:50

2 Answers 2

7
$\begingroup$

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.)

$\endgroup$
1
  • $\begingroup$ Indeed, the problem was just a lemma that should have been changed to def when I modified it to return a witness rather than a bare existential statement. $\endgroup$ May 16 at 17:06
3
$\begingroup$

(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.

$\endgroup$
5
  • $\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 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 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 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 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 at 13:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.