Stream: general

Topic: noncomputable theorem

Reid Barton (Oct 19 2018 at 16:38):

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

Simon Hudon (Oct 19 2018 at 16:52):

What happens if you remove noncomputable?

Reid Barton (Oct 19 2018 at 16:57):

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 (Oct 19 2018 at 16:57):

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

Reid Barton (Oct 19 2018 at 16:59):

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 (Oct 19 2018 at 17:01):

Okay yes, that seems to be the case.

Reid Barton (Oct 19 2018 at 17:08):

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 (Oct 19 2018 at 17:11):

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

Reid Barton (Oct 19 2018 at 17:13):

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 (Oct 19 2018 at 17:14):

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

Simon Hudon (Oct 19 2018 at 18:21):

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 (Oct 19 2018 at 18:22):

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

Mario Carneiro (Oct 19 2018 at 22:41):

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 (Oct 19 2018 at 22:45):

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.

@Reid Barton

Floris van Doorn (Oct 01 2019 at 17:23):

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 (Oct 01 2019 at 19:12):

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

Floris van Doorn (Oct 01 2019 at 19:13):

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

Yury G. Kudryashov (Oct 01 2019 at 19:17):

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

Floris van Doorn (Oct 01 2019 at 19:30):

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 (Oct 01 2019 at 19:32):

Does noncomputable infect the declarations that use them?

Yury G. Kudryashov (Oct 01 2019 at 19:34):

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 (Oct 01 2019 at 23:01):

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 (Oct 01 2019 at 23:03):

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.

Last updated: May 16 2021 at 05:21 UTC