Trivial calculations with Reals?

Stream: new members

[Adomas Baliuka]

Today I started learning Lean for fun. Here's a thing I tried to do:

noncomputable def log₂ (x:ℝ) := Real.logb 2 x

-- Shannon binary entropy
noncomputable def h₂ (x : ℝ) : ℝ :=
    -x * log₂ x - (1 - x) * log₂ (1 - x)

First thing I tried was #eval h₂ 0.5, which should give 1, but I guess Lean doesn't work that way. So I "proved" it...

theorem log2_div_log2_is1 : -log 2 / log 2 = -1 := by
    have h : log 2 ≠ 0 := by
        refine Iff.mpr log_ne_zero ?_  -- no idea what this is, found by `apply?`
        simp
        linarith
    rw [neg_div]
    rw [div_self h]

example : h₂ (1/2) = 1 := by
    rw [h₂]
    have h: log₂ (2⁻¹) = -1 := by
        rw [log₂]
        rw [logb]
        simp
        refine log2_div_log2_is1
    repeat simp [*, h]
    have asdf: 1 - (2:ℝ)⁻¹ = (2:ℝ)⁻¹ := by ring
    rw [asdf]
    simp [*, h]
    ring

This works, but is incredibly ugly. I'm sure the proofs can be simplified. But even then, isn't there some tactic that can "just compute this"? Is there some way I can say "compute h₂ 0.1234 to at least 10 digits"? I also had trouble proving that 0.5 = 1/2, which also seems somehow too trivial to have to think about...

[Ruben Van de Velde]

"to at least 10 digits" is somewhat hard, but for exact computations, the tactic is called norm_num

[Ruben Van de Velde]

But to use it, you'll first need to unfold your own definitions; I don't think it can see through those. And then your guess is as good as mine as to whether it already supports Real.logb

[Adomas Baliuka]

Thanks a lot for the help! Is there a way to "automatically unfold my definitions"? Otherwise, it seems like I should minimize my own definitions at any cost...
So there isn't a way to, say "compute with 64bit floats and get a rigorous (maybe very loose) bound on accuracy"? I would think that's a nice use-case for a theorem prover. Is there a way to "plug in 64 bit floats where there used to be reals in the code"?

[Niels Voss]

You can do unfold h₂, or unfold h₂ at h (if h₂ occurs somewhere other than the goal) to unwrap your definition. (Note that sometimes, unfolding is not necessary because of definition equalities, but it is usually necessary if you are using rw). It is still often useful to keep your definitions short and concise, for other reasons.

[Niels Voss]

I don't think there is a way to use computation on Floats to get bounds for real numbers. There are after all a finite number of Floats and an uncountable number of Reals, and Reals are always exact rather than an approximation. Like mentioned above, norm_num is sort of like a mini-CAS which can be used to simplify expressions.
That isn't to say that it wouldn't be useful or possible to get bounds using Floats, but no one has managed to accomplish that yet, and proving properties about the precision of floats is very, very hard.

[Niels Voss]

There was a project which might be of interest to you, called Sci Lean. I haven't used it, but I think it might be able to do approximations of Reals using Floats, but not prove that they are correct.

[Adomas Baliuka]

Niels Voss said:

proving properties about the precision of floats is very, very hard.

I would think this is only hard "in general" and if you want tight bounds. If I'm happy with propagating some worst-case errors, that shouldn't be so bad? Guess I haven't studied enough numerics.
Anyway, this means that actually calculating with real numbers isn't (currently) possible in Lean? Is there at least a Float64 type? The docs aren't very informative on the matter (empty page at https://leanprover.github.io/lean4/doc/float.html) and I can't find it...

[Ruben Van de Velde]

(Also, you rely on the assumption that your computer's implementation of floats is correct)

[Niels Voss]

Floats have somewhat redimentarty support, and it is very hard to prove theorems about them. I think Float is what most languages call double, and there are no 32-bit floats.

[Adomas Baliuka]

Thanks. Is there any docs about the Float support? I'm somewhat aghast at the docs page I linked above being empty...

[Kevin Buzzard]

Lean is a theorem prover not a computer algebra system, and it's extremely difficult to prove theorems about floats because things like x+y=y+x aren't true.

[Kevin Buzzard]

People will get to floats in the end, but the biggest lean project right now is its mathematics library which has no use at all for floats, it uses infinite precision reals instead because they're much better for theorems (and much worse for computations)

[Adomas Baliuka]

Ok, so let's forget proving things. Is there a way to compute h₂ 0.1234 in Lean such that I can have reasonable confidence (as I would get from Float64) that it's correct up to 5 digits? Does the C code generation support using native C-Floats?

[Niels Voss]

Here are some of the functions on floats, https://leanprover-community.github.io/mathlib4_docs/Init/Data/Float.html#floatSpec

[Niels Voss]

But if you read it closely, you will notice that Float is essentially defined as a extra axiom

[Niels Voss]

So I think it is not currently possible to reason about floats in any meaningful manner. (Except for something called native_decide)

[Adomas Baliuka]

I guess noone does things like this then, but is there an easy way to prove something like exp 14515/1234156 > 1? Or is that a hard problem?

[Anatole Dedecker]

(deleted)

[Kevin Buzzard]

Assuming now you're talking about reals, we will have a lemma saying x > 0 -> exp x > 1 so that reduces the problem to showing that your rational is positive, which the norm_num tactic will do. So it's a process of both applying theorems and using algorithms.

[Niels Voss]

If you mean for floats, you can try native_decide but note that native decide adds an additional axiom whose soundness is questionable

[Niels Voss]

Anyway, this means that actually calculating with real numbers isn't (currently) possible in Lean?

There are essentially two different reasons why Reals are uncomputable. They are defined as Cauchy sequences of rational numbers. In general, there's no way to know whether one Cauchy sequence will coverage to a greater number than the other, so < is undecidable on Reals, among other things.

Another reason is that the axiom of choice is used extensively in defining functions and values. For example, we can prove via IVT that there is a real number c in [1,2] such that cos c = 0. Then pi is defined as 2 * c. This obviously doesn't give any way to compute pi

[Adomas Baliuka]

Yes, I get that. However, if people cared about it (and I'm not saying they should) it would be possible to have #eval cos Real.pi work. So I'm just finding out which things work and which don't. Thanks for the help!

[Niels Voss]

You can maybe try #norm_num cos Real.pi, though I'm not sure if that's been ported to Lean 4 yet

[Adomas Baliuka]

Any idea why #norm_num log (exp 4) works but #norm_num exp (log 4) doesn't? (Let me know if I'm starting to spam/bother people here...)

[Tyler Josephson ⚛️]

My group is prioritizing real-to-float conversions right now, for scientific computing applications. @John Velkey ⚛️ is currently working on this, building off the code by @Alexander Bentkamp here: https://github.com/verified-optimization/CvxLean/blob/main/CvxLean/Tactic/Solver/Float/RealToFloat.lean

Read some more in this thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Real.20to.20float.20translation

[Tyler Josephson ⚛️]

In our case, we intend to entirely ignore errors in floating point precision (other people can work on that). We just want to prove that functions over real numbers have certain properties, and then use such functions on floats for computations and IO.

[Jz Pan]

Kevin Buzzard said:

Assuming now you're talking about reals, we will have a lemma saying x > 0 -> exp x > 1 so that reduces the problem to showing that your rational is positive, which the norm_num tactic will do. So it's a process of both applying theorems and using algorithms.

But can Lean4 prove 333/106 < Pi < 355/113 ?

[Jz Pan]

I think maybe we can add a typeclass called "computable real", which means that there is a computable function which accepts a positive rational number epsilon and outputs two rational numbers a and b such that a<=x<=b and |x-a|<epsilon and |x-b|<epsilon.

[Jz Pan]

I mean a computable function, and a proof that this function returns the correct value.

[Jz Pan]

Niels Voss said:

Another reason is that the axiom of choice is used extensively in defining functions and values. For example, we can prove via IVT that there is a real number c in [1,2] such that cos c = 0. Then pi is defined as 2 * c. This obviously doesn't give any way to compute pi

But you can use Newton's method or bisection method, no?

[Damiano Testa]

Jz Pan said:

But can Lean4 prove 333/106 < Pi < 355/113 ?

There is docs#Real.pi_lt_3141593.

[Damiano Testa]

The file where this lemma is proven will never cease to grow.

[Jz Pan]

Cool. This file essentially proves that pi is a computable real.

[Mario Carneiro]

ab said:

I guess noone does things like this then, but is there an easy way to prove something like exp 14515/1234156 > 1? Or is that a hard problem?

Yes, I believe we do have high precision exp calculations in mathlib, although not via any general tactic

[Mario Carneiro]

so you would have to copy the approach used there, most likely to work out the first few terms (until it exceeds 1)

[Mario Carneiro]

the denominators grow pretty quickly with this method though so it would be better to have something more approximate

[Mario Carneiro]

More generally, the tactic that does "calculate the first 10 digits of this real expression" via interval arithmetic is approx, which I wrote in lean 3 and never finished to push to mathlib; I translated it to lean 4 in the Leiden Workshop 3 weeks ago but it turned out to be a bit of an ambitious project for an "intro to metaprogramming" project so we did clean instead

[Adomas Baliuka]

This approx sounds great. Do you think it might be ported e.g. this year? I would also be interested in seeing how powerful it is/will be. (I guess I would also love to help porting it but that's probably too ambitious for my current stage of learning)

[Adomas Baliuka]

@Mario Carneiro Hi, sorry to bother you again. I'm really interested in getting this approx tactic to work. Any clue where I should start? Do I have to port over some lean 3-tactic to lean 4? You mentioned that you already translated it to lean 4? I'm still only a beginner, so meta-programing a tactic might be a bit ambitious, but I would like to try.

[Mario Carneiro]

I wrote it in lean 3, and hastily mathported it to lean4 a few months ago: https://gist.github.com/digama0/fd3be96cd82e92535dbb420e86a8b1be

[Adomas Baliuka]

Thanks for responding @Mario Carneiro !
This was never in Mathlib3, right? Was it ever seriously used somewhere or was it always a prototype? Is there any example on how this is intended to be used (using concrete numbers)?

Finishing the porting (especially without knowing the intended way to use it) is currently beyond my capabilities but I could probably learn a lot by trying.