noncomputable theorem

Stream: general

[Reid Barton]

Is there any sense in writing noncomputable theorem, as in mathlib logic.basic lines 516-519?

[Simon Hudon]

What happens if you remove noncomputable?

[Reid Barton]

Probably I wait a long time for mathlib to rebuild and then nothing interesting happens--I've written lots of theorems that use noncomputable things before.

[Reid Barton]

I wonder whether they should be noncomputable def, or just theorem, or maybe none of this matters

[Reid Barton]

Actually I could be wrong--these theorems are special because their result types are not Props (that's why I'm looking at them), and maybe that is what triggers the noncomputable check

[Reid Barton]

Okay yes, that seems to be the case.

[Reid Barton]

I never thought about exactly what is going on with def and theorem. I guess the difference is like let vs have, that is, something defined with def can be replaced by its definition by one of the reduction rules, while something defined with theorem can't be replaced by, well, its proof?

[Reid Barton]

The VM can't reduce a theorem either, right? So why bother with the noncomputable check for theorems?

[Reid Barton]

In the case of classical.dec I guess someone decided that it was useless to allow it to be unfolded because it's essentially just an application of an axiom, and it's uniquely determined up to propositional equality, anyways?

[Reid Barton]

This all seems to make sense, I'm just not sure my mental picture is actually correct.

[Simon Hudon]

I'm wondering if it's about generating byte code for the VM. If the theorem's type is in Prop, then, it doesn't matter.

[Simon Hudon]

But otherwise, you may have to say explicitly "Don't generate code" with noncomputable

[Mario Carneiro]

If you mark something as either noncomputable or theorem, then the VM does not generate code for the definition. This is why sometimes you get those errors about bytecode generation failed when you accidentally mark something as a theorem

[Mario Carneiro]

noncomputable theorem is almost always not needed, but it is used in a few specialized instances. One other consequence of defining something as a theorem is that it is "definition irrelevant", that is, lean will not generate or use the definitional equation for this definition. This is almost never appropriate for a Type valued expression, since it provides relations between definiendum and definiens that we can't otherwise recover. So the place where it makes sense is when the definition is already ambiguous, as in classical.some - unfolding it will not tell us any more about its value - and it is also using the axiom of choice so it should not have any code generation.

[Mario Carneiro]

@Reid Barton

[Floris van Doorn]

As part of sanity_check cleanup, I tried making these theorems dec, dec_eq, dec_rel and dec_pred definitions, but it does cause an error later on:

D:\projects\mathlib2\src\ring_theory\unique_factorization_domain.lean:146:18: warning: failed to generate bytecode for 'of_unique_irreducible_factorization'

Interestingly, when I mark that definition as noncomputable, I get two conflicting(?) errors:

D:\projects\mathlib2\src\ring_theory\unique_factorization_domain.lean:146:18: warning: definition 'of_unique_irreducible_factorization' was incorrectly marked as noncomputable
D:\projects\mathlib2\src\ring_theory\unique_factorization_domain.lean:146:18: warning: failed to generate bytecode for 'of_unique_irreducible_factorization'

For now, I just added the sanity_skip attribute to these decidability declarations.

[Yury G. Kudryashov]

Hi, where are the definitions that you're trying to change from theorem to def? I mean, file/line.

[Floris van Doorn]

https://github.com/leanprover-community/mathlib/blob/master/src/logic/basic.lean#L593-L597

[Yury G. Kudryashov]

BTW, is there any difference between theorem and noncomputable theorem? I mean, theorems do not generate bytecode anyway.

[Floris van Doorn]

Lean will try to generate bytecode for them, because their type is non a proposition. You get an error when you remove noncomputable.

[Simon Hudon]

Does noncomputable infect the declarations that use them?

[Yury G. Kudryashov]

I had a similar error when one of the dependencies of a def was marked as theorem instead of def. It was something like induction_on with output in Sort.

[Yury G. Kudryashov]

The reason is that letI hides the definition behind let ... in ..., and Lean can't understand that classical.choice is used only in the proofs.

[Yury G. Kudryashov]

A few ways to fix the problem: (a) use haveI; (b) move letI to the proof of prime_factors; (c) write refine_struct { .. o } before letI.

[Eric Wieser]

It seems that the reason for using noncomputable theorem here no longer applies, as replacing it with noncomputable def as in #10292 seems to work just fine.