Fully polymorphic numerical method: bisection

Stream: CSLib

[Oscar Matemb ⚛️]

I’ve implemented a fully polymorphic bisection method here. It finds a root in the interval [a, b], and when executing on floats, it agrees with Python numerical libraries works quite nicely when executing on floats. We made make it fully polymorphic to work with both Floats and ℝ, and prove termination and sub-interval generation thus far. Beyond these, what other properties, theorems or invariants about the code are there that are typically proved in this context?
I redefined mathlib definitions for now to get the code to agree with reals. Any questions, suggestions and critiques on style, refactoring and so on... are welcomed as well.

[Eric Wieser]

You can save yourself a fair amount of boilerplate by writing

class BisectionConfig (α : Type*) extends Zero α, Add α, Sub α, Div α, Mul α where
  [two : OfNat α 2]
  isPositive : α → Bool
  isNegative : α → Bool

[Oscar Matemb ⚛️]

Thank you!

[Oscar Matemb ⚛️]

@Alejandro Radisic this project is a subscript of what you implemented in LeanCert, I wanted to get your opinion on it.

[Alejandro Radisic]

Hey Oscar, nice work getting this running!

So the big difference with what we did in LeanCert is basically point sampling vs interval enclosures. In your version you’re just evaluating f(mid) directly, which is great for Floats and works fast, but it’s hard to prove anything about it, and over ℝ it’s noncomputable anyway

In LeanCert we avoid that by evaluating f on an interval instead, and then checking whether the whole interval is positive, negative, or neither. That way you keep things computable (endpoints are rational) and you also get soundness from the bounds.

The polymorphism issue you ran into with ℝ is pretty much exactly why we went that route, you can’t turn a Prop like f x < 0 into a Bool in a computable way.

If you want to move more in the verification direction, the key idea is switching to a kind of three-state logic. Instead of asking “is f(x) < 0?”, you ask something like “is f([x−ε, x+ε]).hi < 0?”. That’s decidable and actually gives you something you can prove correct

[Oscar Matemb ⚛️]

Thank you very much for your response. I actually didn't think about evaluating f over an interval instead of a fixed point. I don't understand why an interval provides a higher level logic that allows computations to be provable? I understand the simplicity of this approach but not at a high level. If you have some resources to do some reading that's greatly appreciated as well!