Error: missing 'noncomputable' modifier

Stream: new members

[learnreal]

Hi,
What does "missing 'noncomputable' modifier, definition 'circle.makenew' depends on 'real.division_ring'Lean" mean?
Here is what I was trying to do:

structure point :=
  (x y: \real)

structure circle :=
  (center: point) (radius: ℝ)

def circle.makenew (d e f: ℝ): circle :=
    circle.mk  (point.mk (-d/2) (-e/2)) (real.sqrt (((d*d)+(e*e))/4)-f)

Thank you.

[Johan Commelin]

Add noncomputable before the def. Or add noncomputable theory to the top of your file.

[Johan Commelin]

Because you can't really do computations with real numbers, and Lean is complaining about that.

[learnreal]

Thank you. This got rid of error. But, how can I make it computable? For example, this is what I was trying:

noncomputable def c2: circle := circle.makenew 10 10 1
#eval c2.radius

I expect that to be 7. Instead it says "code generation failed, VM does not have code for 'c2'"

[Kyle Miller]

And "computation" here specifically means "computing with #eval or its equivalents." There are other sorts of computations you can do with lean, like using simp or norm_num

[Kyle Miller]

You can't #eval real numbers at all since they're defined in a very #eval-incomputable way

[Kyle Miller]

I guess norm_num doesn't know about how to compute square roots of real numbers that have a nicely represented square, but here's an example of how you might evaluate things in another way:

import data.real.basic
import data.real.sqrt
import tactic

noncomputable theory

structure point :=
  (x y: ℝ)

structure circle :=
  (center: point) (radius: ℝ)

def circle.makenew (d e f: ℝ): circle :=
    circle.mk  (point.mk (-d/2) (-e/2)) (real.sqrt (((d*d)+(e*e))/4)-f)

def c2: circle := circle.makenew 10 10 1

#norm_num [c2, circle.makenew] : c2.radius
-- real.sqrt 200 / real.sqrt 4 - 1

[Kyle Miller]

The square brackets after #norm_num are a way to tell it which definitions it should expand in the process of evaluation. It's not the best, but with some more work one can make it so you don't need to do that.

[learnreal]

Great. Thank you :)

This works for me (for now).

[learnreal]

So, QQ - if I really want computations then I should interface with some other language like c/c++?

[Johan Commelin]

Not necessarily. Lean also has Float.

[Johan Commelin]

The question is: do you want to mix proofs and computations?

[learnreal]

Johan Commelin said:

The question is: do you want to mix proofs and computations?

Understood. I really don't want to mix. Just asking what is the way out - if deep into my code I get stuck with some computation.

[Johan Commelin]

If you don't care about proofs, don't use ℝ. It's a type designed for proving things about real numbers.

[learnreal]

Got it. Thanks a lot.

[Mike Shulman]

It's a shame that mathlib is set up that way, because there are computable/constructible notions of real number that one can also prove things about.

[Kevin Buzzard]

We made a decision very early on to be classical pretty much throughout mathlib, because (amongst other things) we were trying to do something new (constructivism is rampant in ITP work and essentially nonexistent in mathematics departments); we were also trying to attract classical mathematicians to the project.

[Mike Shulman]

I know. I'm just saying, it's a shame. (-:

[Mike Shulman]

It ought to be possible to develop real numbers constructively insofar as that is easy and then make classical assumptions only when needed.

[Kyle Miller]

A motivated person could develop their own constructive real numbers and then show they're classically isomorphic to mathlib's -- is there any reason for mathlib's real numbers to be constructive?

[Kyle Miller]

Would constructive real numbers mean you could get sensible output for #eval r with r : real? (I think not, but correct me if I'm wrong)

[Mike Shulman]

I don't see why not, as long as your r is built out of constructive operations.

[Mike Shulman]

Then someone like the OP in this thread would get the behavior they're expecting.

[Mike Shulman]

Some operations on real numbers can already be evaled:

def x : ℝ := 2
def y : ℝ := 3
#eval x + y

yields real.of_cauchy (sorry /- 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, ... -/) which is a little weird-looking but does tell you what the answer is.

[Patrick Johnson]

Would constructive real numbers mean you could get sensible output for #eval r with r : real? (I think not, but correct me if I'm wrong)

In theory, #eval can already give a sensible output for r : ℝ, but it would be very inefficient. Each real number can be evaluated to the first n decimal places (for some fixed n), each digit can be determined by running a Lean instance for every possible string checking whether that string represents a Lean proof of the statement "The k-th digit is 0" (resp. 1). Although, for some real numbers (such as Chaitin's constant), the algorithm won't terminate.

[Mario Carneiro]

@Mike Shulman said:

Some operations on real numbers can already be evaled:

def x : ℝ := 2
def y : ℝ := 3
#eval x + y

yields real.of_cauchy (sorry /- 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, ... -/) which is a little weird-looking but does tell you what the answer is.

Ah, but actually the value was 6 all along! It just took a while to converge.

Mathlib reals are not really computable at all. They contain zero bits of extractable information; even the information here can only be obtained by cheating (using unsafe functions that go outside the theory and break the quotient wrapper), at which point we may as well use a tool that looks at the fact that you added 2 and 3 directly and gives a much more sensible answer:

import data.real.basic
def x : ℝ := 2
def y : ℝ := 3
#norm_num [x, y] : x + y -- 5

[Mike Shulman]

It's also true constructively inside the theory that you can't extract any bits from a real number, but for a different reason (continuity). But normalization isn't an operation inside the theory. So if you normalize a real number defined in the empty context, you should get something that's an injection into the quotient of some concrete Cauchy sequence, and you can look (externally) at that Cauchy sequence and get information about the real number. I assumed that the 5, 5, 5, 5, ... in the display was arising from a computation of this sort.

[Mike Shulman]

Constructively one also generally works with Cauchy sequences having a fixed convergence rate, in which case seeing 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, ... would (at least for a sensible choice of convergence rate) at least tell you that the answer isn't 6.

[Mario Carneiro]

yes, I'm talking about the latter issue. You could implement constructive reals in mathlib, but what we have currently isn't that

[Mario Carneiro]

but also, the operation you did wasn't normalization, that's #reduce and it scales atrociously. I very much doubt it terminates on your example in a reasonable time frame

[Mike Shulman]

No, it doesn't, I've tried. But I thought #eval was something like normalization of closed terms using a fast external algorithm.

[Mario Carneiro]

no, it's more like compilation to byte code and then interpretation

[Mario Carneiro]

the consistency of that mapping is actually still an open question, although I suspect it to have reasonable properties and I have no counterexamples

[Mario Carneiro]

the hard part being that it blows right through eq.rec applications, leading to ill typed terms which nevertheless compute reasonably

[Johan Commelin]

@Mike Shulman What do you think of the #norm_num [x, y] : x + y that Mario wrote above?

[Johan Commelin]

Is that close enough to being "computable"?

[Mario Carneiro]

(Note that that's the only method of those discussed so far that would actually be effective in giving you a proof that 2 + 3 = 5 over the reals. Evaluation outside the theory isn't helpful if you can't reflect it back to prove more things.)

[Mike Shulman]

It's hard to know what I think of it since I don't know what it's doing. It looks like it doesn't evaluate square roots? Is it doing more than just applying ring/field axioms?

[Johan Commelin]

It is a system for "numeric normalizations". A user can register extensions, for example for fast primality proofs, or the recently added module for computing Jacobi symbols.

[Johan Commelin]

In a similar manner, someone can extend it with a square-root algorithm for (some?) reals.

[Mario Carneiro]

A reasonable extension for square roots might for example work out expressions in $\mathbb{Q}[\sqrt{p_1},\sqrt{p_2},\dots]$ where the $p_i$ are detected ad-hoc from the expression. So you would get exact answers like $(\sqrt{4 + 2^2} + \sqrt{10})^2=18+8\sqrt{5}$ instead of an approximation (or an infinite sequence of approximations which in theory evaluates to something useful but in practice is left unreduced)

[Mario Carneiro]

In other words, norm_num is a lot closer to a CAS than a calculator

[Eric Wieser]

Does mathlib have a computable type for $\mathbb{Q}[{\sqrt{n} | ∀ n, \operatorname{square\_free} n}] / (∏ n, X_n^2- n)$?

[Johan Commelin]

Do you mean $ℚ$ adjoint the square root of all square free integers?

[Johan Commelin]

You might even go for something like https://en.wikipedia.org/wiki/Quadratically_closed_field#Quadratic_closure

[Eric Wieser]

Oh, I guess I mean the square root of all square-free naturals

[Eric Wieser]

But yes, I think a computable quadratic_closure is what I'm asking for

[Eric Wieser]

No, I think I want something weaker; the quadratic closure contains terms of the form sqrt(1 + sqrt(q)), right?

[Kevin Buzzard]

It contains all square roots of everything; there isn't a sqrt function though because most elements don't have a canonical square root (edit: I guess it's possible to define a "random" one though...)

[Pedro Sánchez Terraf]

Mario Carneiro said:

the hard part being that it blows right through eq.rec applications, leading to ill typed terms which nevertheless compute reasonably

This reminds me of classical realizability (cf. Sect 3.1.2.1 here).

[Bolton Bailey]

Does mathlib have an algebraic numbers type?

[Junyan Xu]

docs#integral_closure ℚ ℂ or docs#algebraic_closure ℚ?

[Eric Wieser]

Yeah, but neither is computable, which seems like the main appeal in the first place

[Eric Wieser]

THere's an obvious implementation with finsupp but... that wouldn't be computable either

[Kevin Buzzard]

The Langlands philosophy is all about representations of the automorphism group of the algebraic numbers and computability is definitely not the main appeal there :-)

[Eric Wieser]

The context of my statement is an unstated claim that If we had a computable representation of these things then it would be easier to teach norm_num to normalize them

[Eric Wieser]

As I understand it, right now most of what norm_num does is construct ℚ representations of the numeric terms, compute with them in the vm to normalize them, and then construct proofs that the normalized version is equivalent

[Kevin Buzzard]

The moment you allow roots of polynomials you face the issue that polynomials have more than one root. For example you don't know sqrt(a^2*b)=a*sqrt(b)etc

[Johan Commelin]

We could add the real closed field of algebraic numbers in $\mathbb{R}$. That's a pretty computable field. Although the decidable equality isn't very fast, I think.

[Mike Shulman]

Mario Carneiro said:

In other words, norm_num is a lot closer to a CAS than a calculator

I see, and I also see the point that when proving things about the real numbers one generally wants something more like a CAS. In principle I think some of this could also be incorporated into definitional equality also, but in any case it is useful to have both.

The description of norm_num sounds a lot like a version of simp specialized to numbers. How are they different?

[Mario Carneiro]

They aren't so different. If simp had "simp-procs" we could potentially do norm_num transparently with it. norm_num also takes simp lemmas and uses simp as the main driver to rewrite inside terms. The main difference is that norm_num recognizes certain kinds of expressions (like prime 37) and uses customized numerical calculation methods on them rather than just blindly applying rewrite rules (of which there wouldn't be any in this case because primality is not a neatly recursive definition over the structure of the term).

[Eric Wieser]

Mario, is my characterization that "having a computable representation of integral closures would make dealing with real.sqrt in norm_num easier" plausible?

[Mario Carneiro]

I think the foremost issue is to find some subset of expressions which have good theoretical properties (e.g. closure under interesting operations) and a normal form

[Mario Carneiro]

TBH I haven't looked into this very much. When you just adjoin one chosen square root, things are easy but when you have multiple it gets a lot harder and I'm not sure you have a compatible set of normal forms

[Johan Commelin]

Maybe roots of unity can help? They form a "canonical basis" that generates a field that contains a lot of interesting algebraic numbers.

[Junyan Xu]

Notice that Mathematica has Root[{f1,f2,…},{k1,k2,…}] that could specify any finite extension of Q via iterated simple extensions; see also https://reference.wolfram.com/language/ref/AlgebraicNumber.html