Making Reals computable (sometimes) using coercion

Stream: mathlib4

[Cookie Guy]

So I have been reading how Mathlib defines a Real and I found it quite wierd that it was completely uncomputable.. I looked into it and it makes sense, it is a quotient and those cant be computed and all. But I still find it wierd that a calculator cant approximate reals, it feels like a programming language should be able to approximate reals at the least. I figured it should be very handy and very easy in principle to make reals be able to be a function that takes in a precision and gives you are rational which is epsilon precise.

But then i found out that there are things like Specker's sequence.
Here's my solution

When you type let x : ℝ := 1 in lean, it is actually OfNat (1 : ℕ) to cast from natural to real. So my thought was that we remove this cast. We add a new type, called ApproximableReal or something. Every 'normal' number will be of this type. This is because an ApproximableReal is something like

structure ApproximableReal :=
approximator: ℚ → ℚ
convergence_proofs: ommited types

so very similar to our intuition on Cauchy Reals. It doesn't have decidable equality or any of the nice things that we get from normal Mathlib Reals, but it is computable. It is not intended to be used by itself, it automatically casts up to reals.

However, reals constructed in this fashion are nice because of something like Int.OfNat_nonneg, this has the ability to approximate as long as the real comes from an ApproximableReal.

ApproximableReals would have to be constructed differently i guess. Like for example Real.pi couldn't be an approximable real if it was written as IVT on 0 ∈ cos '' Icc (1 : ℝ) 2 like it is in lean right now, but it could if it was written using like infinite sum or integral of circle or whatever (could integrals become approximable too? or could only boxIntegrals).

By doing this, we preserve all of the nice properties present in current reals, but we can add that we can also compute most numbers.

I'd love to hear thoughts on why this is a good or bad idea?

[Aaron Liu]

what kinds of things do you expect to be easier to do with these approximate reals than with the docs#Real already in mathlib?

[Cookie Guy]

i want the ability to approximate reals. This would make, for example, bounding any approximable real, such as pi or e, trivial, but more in general, it allows us to use lean more easily for scientific calculation

[Snir Broshi]

pi is defined as 2 times the unique root of Real.cos in [1, 2], and e is defined as the sum of factorial reciprocals. How would bounding them be trivial? Wouldn't it just shift the problem to defining them as approximable reals?

[Snir Broshi]

btw Mathlib is missing Hurwitz's theorem, so if you're interested in approximating reals it seems fun to work on it

[Cookie Guy]

Snir Broshi said:

pi is defined as 2 times the unique root of Real.cos in [1, 2], and e is defined as the sum of factorial reciprocals. How would bounding them be trivial? Wouldn't it just shift the problem to defining them as approximable reals?

i believe it should be far more natural.

lets say we define

$$\pi = 4 \text{arctan}(1)$$

a proof on the bound should come directly from the approximableReal arctan, which is defined as an infinite sum

alternatively, if we defined it as something more complicated like

$$\displaystyle 2 * lim_{x \to 1^-} arcsin(x)$$

then lean would use the proof that the limit converges as an epsilon delta as the first 'approximant', and i can imagine that this approximant is going to then use the approximant of arcsin internally, so some rather complicated stuff would be happening behind the hood, however it comes out directly from the construction of a ApproximableReal

the way we currently prove that 3.14 < π is through a rather involved proof using a recursive nested sqrt(2 + ...) and random rational numbers provided by mathematica which I honestly don't understand

In my opinion, restricting to approximable reals, while shifting the problem, makes the problem also a lot easier to solve, just a proof of convergence.

[Aaron Liu]

Cookie Guy said:

i want the ability to approximate reals. This would make, for example, bounding any approximable real, such as pi or e, trivial, but more in general, it allows us to use lean more easily for scientific calculation

trivial how? don't you now need to evaluate the approximation and bound its error?

[Aaron Liu]

or are you saying that should be a lot easier

[Snir Broshi]

Cookie Guy said:

i believe it should be far more natural.
...
a proof on the bound should come directly from the approximableReal arctan, which is defined as an infinite sum
...
then lean would use the proof that the limit converges as an epsilon delta as the first 'approximant', and i can imagine that this approximant is going to then use the approximant of arcsin internally, so some rather complicated stuff would be happening behind the hood, however it comes out directly from the construction of a ApproximableReal
...
In my opinion, restricting to approximable reals, while shifting the problem, makes the problem also a lot easier to solve, just a proof of convergence.

You're making bold claims without supplying any form of evidence (i.e. code) to support them. I don't see how that's any easier, but perhaps a code example would demonstrate it. Note that such an example needs to avoid importing the existing definition of pi, otherwise it might be using theorems which rely on the current definition of pi and so can't be used to change its definition.

Also, it seems like you're advocating for changing the definition of pi using inverse trig functions, which is a separate problem.

[Cookie Guy]

Aaron Liu said:

Cookie Guy said:

i want the ability to approximate reals. This would make, for example, bounding any approximable real, such as pi or e, trivial, but more in general, it allows us to use lean more easily for scientific calculation

trivial how? don't you now need to evaluate the approximation and bound its error?

I am imagining that ApproximableReal.approximant is a function that takes in a rational number epsilon and gives you a rational number which is closer than epsilon to the 'true value'. In my mind what will make it easier is that composition of functions comes automatically

now if i defined addition between two apporximableReal,
let a b: approximableReal, let ε be given

let a1 := a.approximant ε/2
let b1 := b.approximant ε/2

a + b

now by design, we will know that approximableReal has the property of being epsilon precise through some argument with ε = ε / 2 + ε / 2.

Using this , if we had appropriately defined pi and e, then lean would automatically know bounds on π + e

This idea could be extended to much more than just addition, such as sin : approximableReal → approximableReal would allow us to automatically argue about sin pi.

[Snir Broshi]

Can you please provide a concrete example of what you mean, using code? (#mwe)

[Cookie Guy]

yup, gimme a minute

[Stepan Nesterov]

It would certainly be convenient to have something like this work:
example : 23 < exp pi := by decide
but I assume that the reason it's not done with things like Approximable Reals is that it's probably very very hard and very slow

[Aaron Liu]

it's also not actually decidable

[Stepan Nesterov]

It's not decidable, but it is recursively enumerable

[Stepan Nesterov]

Like you can compute both sides to a certain precision and prove it

[Cookie Guy]

ok heres my rough draft of a mwe

https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAWQIYwBYBtgCMB0ARFJHAJQFMl0cAhJAZ2AGMAoUSWRFDbHAFSQZiMmTWjCgBXAeKik4AQTBgoEAB6gkWdKTIU4Ad1SkZTABRJFylXABccQKiEcQEmEcQFiEASlMMkk1AE8bcIAARHAgcAB2ADRwGrRwZhaqIXAAtNEJVmEB7nCAJkRxJgBMWW5wAHpxIMCZoWFuboDeBACdHkwQYKSZCkqq6pra5OjCACakAGZwo8ogAHIocZm2diW2XZa9WjroNgC8TADead1WAPo74RFMcHBePv5IcFhnWP704EwAvsJVokhhDLJ7MLvAIAeVGs3gqx6IA0GwG4X0hmMVwg4Lm1m2EymEPCwzGcBgEE2cSsK3S636FGWcEAuIRPXyXOC0aBQBlMEbjJBDIYkuD+MlHCmbalQtQwvrEjH7Q6WM6AbuAEdsAHxwFQ4cxHeYAagAjCUtXz1eltXqLlcbgw/NEHvTGeaKMwrk64AAfNUa2VmOAGvXew0exJen0lVImd3GkyPYN+3xGzWRv16twuu1wU45VPOq6FMohKrWrANRo7TNO55MlkMz4sMI/P6yFbc+Tk8Vw3QYuCAC/IuUNAJfkwnEtaQo1k3xgv3+ATISmbgtblK2BiMpEZMiUAAUZAxVXAwDs11BN6Rt2G47KACwABhKYGEAGJSAA3CgAQjiOoCoqFA31cB1TAfZ90DfEwTA/AU1nnYVEzcM9EgAZmEJhklSOhrW6VE4EwhgIHrMAYCiLQYFiDkqlkIpMUwUIc1SApSmSWpoliTJnEAPCJkNSHhDDgIxlCgOBgFiOYQAgUQ/wAejosI8XGGA9AgORaAAZSMYBSFiCDoVhBcSwOAMMjOIpQxzWxsnKWomjNa5vEtfwaltZ09HQCAAHM4FQAJQjyTI9GANA4AACVTAB23dxFoVBjjCUg3LmVBSygPQ4AAbRiY5aHELBjhwkAQCiCEcEqMJsogXKAF1S1IFR+HgAKEWorRjlRY50HgVAPGdRKUoKorjlIABHFqxjairnRQuAAHEIAoWwXSMiS6NCUN5p1STSlqF1cgW0oQFTcalNYTBRjU2JCVm1apJSbaQE2vILp2vbUgO+skm8qI9FkVAkEfWR7syO61ryitXT+q77puuBMXBsG1uk50vp+9yClCWwTEvYo4AAHjgIpyhRzFy0gehBEfPyGXh77PoKBY4nR0ySmx3GEQ7QnRL84BSZgcmnS65KIogJKTNcEM4iZkAiyumjRdzCzmkh6XzIl5bc3FpoHn8KAqhc0aeaS1KsFodLMpK3KojS5qwlw6LtZCuBSwRhtaYxvIc0VtWWf8In2c57nnUwMIkE1tBbftyn3JAGmhbM16cZlhysyuKqat3AWhuOSA9GOTWXNQGBAACCOJy0tqAQCi8QUffZ2cZKeKE4dgSwkfIaAlAop6ZliWXajko8Ylj3SyuXmqibgamui44hg5qJh76wbcNICeOZ1hOk4ELDx8npvGvnxem+arQkdCVAI9Lf3A78+Lq3Gj7wgF6zMhgUh0C2XwIHEaIoCwPzA8Du4WxQYAuFYi4VjpRUA0taL0UYmhFicB2IASfK+Ak8lFIqU1upOCVgdSXmENfWQXhMgUGZIcdA/hRiDgEIA2sBIIAEkMLQWQYRy5YCMMA/iOUv7RToaQUIvweRaF+NEcQhIYSCC8M/fwABrS2ehYioDvoSO241xEMHEOgFAsg0CMNIElLAb8whDFoAgoCIE5IKWUqpdSMFMF/hwUAA

it demonstrates how we could have reals with computable data that approximate

[Aaron Liu]

this is great for #eval! but

[Aaron Liu]

what about writing proofs with them

[Aaron Liu]

can you demonstrate how you can use these approximations to prove a bound

[Junyan Xu]

You might define

class Real.Approximation (r : ℝ) where
  approx : ℕ → ℚ
  is_approx : ∀ m, abs (approx m - r) ≤ (2 ^ m)⁻¹

and constructing instances of this class for specific real numbers, and on the other hand prove lemmas or write computable functions taking instances of this class as arguments, similarly to what I do for polynomials.

[Jakub Nowak]

Maybe we could change the definition of IsCauSeq from IsCauSeq abv f = ∀ ε > 0, ∃ (i : ℕ), ∀ j ≥ i, abv (f j - f i) < ε to something like

inductive IsCauSeq [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] (abv : β → α) (f : ℕ → β) where
| existential (_ : ∀ ε > 0, ∃ (i : ℕ), ∀ j ≥ i, abv (f j - f i) < ε)
| computable (_ : ∀ ε > 0, { i : ℕ // ∀ j ≥ i, abv (f j - f i) < ε })

And then make Ring operations on CauSeq.Completion.Cauchy "try its best" to preserve computable when possible?

[Jakub Nowak]

I think instead of having this be part of the definition, having computable approximation as separate class as @Junyan Xu suggested would be cleaner. But that would require adding class instances for all definitions that output Real I think?

[Jakub Nowak]

Yet another idea is to have Real become a class, and have two different implementations of reals, one noncomputable and one computable.

[Junyan Xu]

As long as IsCauSeq is Prop it cannot carry any data for computability
It looks like your computable can carry data while existential cannot; why do you want both?

[Jakub Nowak]

Junyan Xu said:

As long as IsCauSeq is Prop it cannot carry any data for computability

Ah yes, you're right, we would have to make a change in the definition of CauSeq instead of IsCauSeq.

Junyan Xu said:

It looks like your computable can carry data while existential cannot; why do you want both?

computable one lets you extract approximations. But not all reals can be defined using computable so you still need to be able to create reals with existential constructor.

[Jakub Nowak]

In fact, maybe we could change definition of CauSeq to { f : ℕ → β // ∀ ε > 0, { i : ℕ // ∀ j ≥ i, abv (f j - f i) < ε } } and mark definitions of reals that require existential statement as noncomputable?

[David Loeffler]

Jakub Nowak said:

In fact, maybe we could change definition of CauSeq to { f : ℕ → β // ∀ ε > 0, { i : ℕ // ∀ j ≥ i, abv (f j - f i) < ε } } and mark definitions of reals that require existential statement as noncomputable?

What does { f : ℕ → β // ∀ ε > 0, { i : ℕ // ∀ j ≥ i, abv (f j - f i) < ε } } mean here? I am familiar with the syntax { x : X // P x } if P : X → Prop, but I believe it isn't well-defined if P is Type-valued, as here.

Are you aiming at something like this, maybe?

structure CauSeqWithWitness where
  f : ℕ → β
  bound : ∀ ε > 0, ℕ
  h_bound : ∀ ε > 0, ∀ i j ≥ bound ε, abs (f j - f i) < ε

And a CauchySeqWithWitness would count as being "computable" if both f and bound are computable functions?

[Cookie Guy]

Ok so i was doing some thinking today about this, and I realized there is a far better solution

[Cookie Guy]

Rather than changing the underlying type on reals, its far less intrusive to make a typeclass instance on the values, similar to how the measurability tactic does it

[Cookie Guy]

we can make a tag called calculability which shows how to calculate something, even if the underlying type was defined in an incalculable way

[Cookie Guy]

since it is now a typeclass over reals, it also allows us to make a much nicer definition of approximability

class Calculable (r : ℝ) where
  /-- Given ε > 0, returns a rational approximation to r -/
  approx : (ε : ℚ) → ε > 0 → ℚ
  /-- The approximation is within ε of r -/
  modulus : ∀ ε (ε_pos : ε > 0), |approx ε ε_pos - r| < ε

[Cookie Guy]

i have a working draft of it, though it does require two files to be created to allow aesop to work properly.

https://live.lean-lang.org/#codez=LTAECcFMAcBsEMDGlQBkCiBBActg9gC6QDOoA7gJYEAWoAnngK7ih5kB2o04eAVpIgKh28ALaQAUBVHQ84IRhz4ixAHQBheLESMEAI1iRVASXZUpMuUICy8GrAp7VAETvxVAJUhbVAIXjEFIgWsvKgtvaOqgAqSARBEhJ40JCcXlqJAPTAAISgAMT5oJgEBOCOjESg8OwAJqCxgkGgzpAAZhRm8XjspMCZWSDFpeV6lSgEeKAE8ADmoIhaOvoUDgR0oJ3EM+zIpG1y09QoAAbw0Nx4AB7SdhQ9J9Nxzf0Sokg8oABEi9q68HpVlQ6F9QAAuaojUAAXgAfBJQKATgAKOxlAA+8BIyVAxHgbRQ5zgG2R4F0kAA+sRIARSGDoaAANoAEmRqG87FUogA1sZaqkhCdNH99IYAJRgij89gEAC6YrFgzAjXiiGmU0QPW2ZMESOFywBhkeWx2e2qlTw71VWlgG0YgXY8yxxBxr3eiE+XyJPBuVvu7FBEJmTTVcIRSORwdV6Oq2OgoGRmvYHXm9NAAG9ppBwKJOlpwQyyoxIAAaUCpQ2QADK0njabaWmpoAAvorEYjSeSqTS6QyWWyOVzedLBfr/gZIBKpQL5YqJNk8oVQGPRSh1AhiKRWh0uv7QK950NMOQqOwSKQaHYkeBjaRfgaJxDLgA3aekGrVC4+27dThtRi7L+J40OW4A8CwehMHUaj7gMiAbqQK6VgmLAQoAuIRiuQxxQOG2RgAA4hQz6pKAgCtwKAsKgAADGWUAEMwvTVBAdw9Pm3rXD+e6TBAsHhuxVzggm5EQoAWISYYASYRkRR1GgJJIm4UM0THJ+ly+ixnAUKQlA0J0Ul4G0PGvIioh4LUuj2oJgAARFJyKkRSsh0lJlFUWKZaYl+1xSXZDn7hAMYADxkYkh5gJg7AbOA6n5uwjCiHo2abHeSzjoYCa8PaQh0Qxmy0pAsBtJhrwAAKMve45AusspSL0pooGVq4UpFQjIgAjoJYmCUhE4Jm16GYWQ2GSIi/GgBSo0FqALXhiZZmwBZ5HUMJDJ6BsgQyAA3OWVxxBSM0Uos2ygItSqgNgdjMNFsXxeA75QAsyWrrxJX1QCFV0FVJo1Mg90ipWFIiM1nAQoAqISYRCXWpciQOgBhWHZkNKk+uNY1puw02meZpALUtoArbitabZA22CLtpn7QEQjHSFoCmEQszZrddUPchxWlczgJrO91XbF9TO/ROFKdM1ABegmACSEYPLuzkOi31cM4cNHkCWNKMMsL6OzfNR043ja3QITxMEKTtTk4dVN4adsXZs0azZo21R3S93WvvAoAAPJtGdQis07b0fTVvM/Q+hgUvpXsJtDoNMh74docIsqddLKDIjHdiqGHV7Q7DA3w3xSvIxNaPGRjc1Y9rE0reGiLUPAxGCUVHhpwdQhx2NUPtZhDKpwQ6ee5nFerXI4B0FX+MyEyOnEGWi1VcFz3s373O1UHKWUvAtT1Omrt6IJaHNkyNeJ/zqXwAnjLUDv4NJ7jCdX8fyeuwA1Lj/WDXnqlSYtBajzXqgjbZoBMigAAEyYWRDXfK9k8CkEWphZ+F8/75wAUA0BCYIFtCgTA0ibZQAzUxhNf8nBsYwkopXdsQdR6InRIARMJwHuBGirUA8CnAMNGoVBMT8X7okoeNBk6I6GII/m3dBmDtaSw6swwRSNhFaAwT5WBvlURMK4QPYQchRCmwIDwsafDkQCNYXQyB8jsHsPgHAhMtCEEGJEcYhUvk9BihjGmPG5RHT/TaNo0AgATIlAPw3+1jZGiNgaYmMz8aHgJYfnGRRjoFiPYXoJxDIATEApOvE2qUVaeMCrQ8iKDzE5MASAsGy0R7kPIbMJMswWAAEYeGIiJnEI67g8Gl3GoYuRsTYF1K2o0hBLSLLRI6VgnB5CdFSWcatWsrB2C2iZI3HuzcKS1CImWeZqhFkZwIGWNJFIIHEWILPee/NF6fV2HzYOlIzzzC3rvfe59XZ3wudUW+Ut74JmAGY+WCMRrELTMAfx+dsYa3wb8kpo89bTNmYyNZiyrlliuVSRgeh/qQFmFVch4AyBMmSYi5FmpRCiHRe2Bpupf79LLlTI5D4TkBzOSvBqxAkUZm3rcg+DzXlPNPgfS+HLV43yPk8pRYAHFfPfkjUFP96FINyUUtBgTbG+SsdKwpqD2lBOwcC1p9YAKf3InCXGpT2z3h4eEgFQjxpgCVeaik7ChVcM8bos10i5UxOGR3RVkTzVqoVWAO1DjEkGrUTmTRDrfF6KdZ5QZ6q7FgE+b6yxnrnXes6SY+xjjVGuNmO4zxPi/FSq9TYlNMbqihN8QmqRkaXVDLifYgNOLGU70yWU8a2TkGyufgUvJA9ukVJ6FU0AtTm31MNk0rkJcBlVujd0kllMnDkraYW4ZoadaTPHj0KFMKKZLJWaATd2xQ59y2dUDeuytD7NnguAoRRogkFpLxCQilb0Qiav6fMttIqwAkA0mQqVHl8r0dU91csJmIw4n6HoiRH3bAhGkqge59LMV/I2L920f0oD/Y9PRyJqmZGAUBmG5iAOZAAMz4YwsUwN/FOIQcg2AdgbBQCGCEBZW4sxOiElwXIFAbRDDEGOPUJgQhiI3XgwZGgKAHB6EisPL55AUA1zriZO6py9hlgcNyFAPBCBTyOCRMgTNODwAtH6X4szIIAXqDpR0pB1MoGIC1MIwDEj8gMvZ+QwDyZvIw8hZEbmhCoJzndMVnkJXkKGJPRKrA2iamYE2D8nRNRgQEEIWshhxAynUmWdKh0DgsH5CZGqL6ehcGYA5Ego8KAGXIj4wDQDqlUQa7pzgPDqkABY2uFPq410eeUmyVakjVzrjXxPNebR1urVFQA9dgH1qr3iB1Daa1NsbqhWvLeJTNlAPCnPF01hSlduIh4jwkPkSAz4tB5D8x5p2hgK0CWw5kLrLkEx43o8GmKog5zia46IXEDmCAedgEbWoeGIR+ZAaAQK2HVvVIAKxAbBYiIYPQ6pMFgPUVj7GjhXl0uJ0A/56JQDLBFmL6PcYoFqCj80kwTM2g2HjPHVHwOcCjEEMsA0gi0DIGj+okEQIem8FUPHN2UAqcJHUJb9pRdCG4uZiX4O8O60tJp8k75zOUwY9xKX9LkLcR3PUWAbAEpy9qMQcMCmUDnbmuhv77nPMXLuwmHDT2wGvfUf9WKncB0w7WyB0eAMiKUn5Igac5va7oYZFd+3q8x17ad49hrz3kRu/e578MmKmRW+LNsvQKSgcJyvJPdPMAEDfTTJPVQg6FiGHgCwLPCMM+MgRUD3Fgs2gYJb2kgA5AXmX1BNLhgcCIcoNBaNHE0riagbAYEMap6T+o2vGdK2oyz54apuIvhQCb0gxWoAIHiMRWZ+K4BBDsJAeoRNuDnn9MQIAA

[Cookie Guy]

to make aesop work, we need to create a new file Called insert project.Calculable.Init in
with

import Aesop
import Mathlib.Init
/-!
# Calculable Rule Set

This module defines the `Calculable` Aesop rule set which is used by the
`approximation` tactic. Aesop rule sets only become visible once the file in which
they're declared is imported, so we must put this declaration into its own file.
-/

declare_aesop_rule_sets [Calculable]

[Robin Arnez]

There are actually already several projects for making real numbers more computable and automating proofs for interval arithmetic on real numbers, the most recent one being #general > LeanBound - interval arithmetic for Lean 4

[Robin Arnez]

Another one is #announce > Computable Reals for native_decide for example which works directly with native_decide (not quite decide but close)