noncomputable integer

Stream: general

[Kevin Buzzard]

How do I get a noncomputable integer (without using constant)? Sorry for asking. I've spent years completely ignoring computability and it's time I got the hang of it.

[Eric Rodriguez]

Is the Busy Beaver function defined? That'd probably be the easiest way

[Gabriel Ebner]

I'd just if-then-else with the classical locale:

import tactic
open_locale classical
noncomputable def n := if ∀ x, x > 2 then 2 else 42

Bonus points if you use a condition that is actually not computable.

[Kyle Miller]

Another one that uses the axiom of choice, but more directly:

noncomputable def foo : ℕ := classical.choice infer_instance

[Gabriel Ebner]

The fun part about if-then-else is that you can actually prove n = 42, and could e.g. extend norm_num to compute n. But it's still noncomputable because it isn't written the right way.

[Kyle Miller]

Are there any lean/mathlib axioms that trigger noncomputable other than classical.choice?

[Bryan Gin-ge Chen]

Presumably what Lean marks as noncomputable differs from what people interested in computability consider noncomputable, right? (Is it a strict superset?) Does @Mario Carneiro's work in the computability folder have a formalization of computable integers?

[Eric Wieser]

If you define your own constant x : ℤ then presumably anything using it is also noncomputable

[Kyle Miller]

I suppose another way to get noncomptuable integers is docs#polynomial.degree. It only knows that the coefficients have finite support, but it doesn't pretend to know what the support is exactly. This is like @Gabriel Ebner's example in that you can in principle compute the degree if you supply more information.

[Gabriel Ebner]

Bryan Gin-ge Chen said:

Presumably what Lean marks as noncomputable differs from what people interested in computability consider noncomputable, right? (Is it a strict superset?)

Right. For example in computability theory, (classical.choice infer_instance : ℕ) is perfectly computable (although we typically only say "computable" for sets or functions).

[Gabriel Ebner]

Does Mario Carneiro's work in the computability folder have a formalization of computable integers?

Yes and no. Every integer is computable, so there's nothing to formalize. But it does have a formalization of computable functions ℕ → ℤ (actually α → β for any α and β that have a primcodable instance).

[Gabriel Ebner]

Kyle Miller said:

Are there any lean/mathlib axioms that trigger noncomputable other than classical.choice?

No, the other axioms (propext and quot.sound) are computable. (Even sorry is computable.)

[Mario Carneiro]

Gabriel Ebner said:

Does Mario Carneiro's work in the computability folder have a formalization of computable integers?

Yes and no. Every integer is computable, so there's nothing to formalize. But it does have a formalization of computable functions ℕ → ℤ (actually α → β for any α and β that have a primcodable instance).

Indeed, it's pretty easy to prove that const foo = 0 is decidable using the computability theory library, because it is decided by one of the functions const true and const false

[Mario Carneiro]

this is one of the consequences of using a classical metatheory when reasoning about computability

[Mario Carneiro]

oh, gabriel already said this

[Mario Carneiro]

Kyle Miller said:

Are there any lean/mathlib axioms that trigger noncomputable other than classical.choice?

Any axiom will trigger noncomputable, but any noncomputable term nested in a type or proof becomes computable again. So while lean/mathlib has three axioms, two of them are props and so are trivially computable and only classical.choice is properly noncomputable