noncomputable theory

Stream: new members

[Bryan Gin-ge Chen]

I think I'm confused as to what noncomputable theory does. I thought that having noncomputable theory at the top of a file means that you don't have to add noncomputable explicitly anymore.

However, this commit implements a suggestion I made to remove noncomputable from a def in a file that starts with noncomputable theory and Lean complains.

[Pietro Lavino]

what is the goal of letting certain functions be non computable? for example log? is it telling lean to not compute that value?

[Chris Bailey]

There's useful stuff that can be reasoned about in Lean's theory, but can't actually be computed. The big one is choice. The noncomputable keyword is a viral marker that allows for a relatively clean separation of the computable and noncomputable parts, to prevent users from finding out at runtime that they accidentally relied on something that can't be computed.

[Luigi Massacci]

If I’m not mistaken, it also saves the code generator the trouble of trying unsuccessfully to compile your definition to code for the VM, so it should speed things up a little too, and make your .olean slightly smaller. As for why log is non-computable, that is because classically defined real numbers are violently uncomputable, even testing for equality is undecidable. Coq has a neat little library for computable real analysis if you want to take a look at how one might go about it