Bisection algorithm

Stream: lean4

[Oscar Matemb ⚛️]

I’ve recently implemented the numerical bisection algorithm in Lean and I’m considering what kinds of properties can be formally established about it. Beyond termination, are there other theorems or invariants that are typically proved in this context?
I’m also interested in perspectives on the design itself: would a refactoring be advisable in order to highlight particular structural features maybe? Also, what would a 'real-valued' formulation of this algorithm look like, and is such a formulation meaningful or useful in practice? I’d appreciate any question, feedback or suggestions!

import Lake.Main
import Lake.Load.Resolve

-- result format (sum type)
inductive BisectionResult where
  | success (root : Float) (iterations : Nat)
  | invalidBounds (reason : String)
  | maxIterationsReached (bestApprox : Float) (iterations : Nat)
  | numericalError (reason : String)

-- values for safe checks
structure BisectionConfig where
  tolerance : Float := 1e-10
  maxIterations : Nat := 1000
  minInterval : Float := 1e-15

-- check if floats have opposite signs
def oppositeSigns (x y : Float) : Bool :=
  (x > 0.0 && y < 0.0) || (x < 0.0 && y > 0.0)

-- check for infinity
def isFinite (x : Float) : Bool :=
  ¬(x.isNaN || x.isInf)

-- f (find roots), a b (left right bounds)
def bisection (f : Float → Float) (a b : Float) (config : BisectionConfig := {} ) : BisectionResult :=
  if ¬(isFinite a && isFinite b) then
    BisectionResult.invalidBounds "bounds must be finite numbers"
  else if a >= b then
    BisectionResult.invalidBounds "left bound must be less than right bound"
  else
    let fa := f a
    let fb := f b

    if ¬(isFinite fa && isFinite fb) then
      BisectionResult.numericalError "Function values at bounds are not finite"
    else if fa.abs < config.tolerance then
      BisectionResult.success a 0
    else if fb.abs < config.tolerance then
      BisectionResult.success b 0
    else if ¬(oppositeSigns fa fb) then
      BisectionResult.invalidBounds "Function must have opposite signs at bounds"
    else
      -- left right -> dataset split, iter (iterations done to finding root, not useful?)
      let rec bisectionLoop (left right : Float) (iter : Nat) : BisectionResult :=
        if iter >= config.maxIterations then
          BisectionResult.maxIterationsReached ((left + right) / 2.0) iter
        else if right - left < config.minInterval then
          BisectionResult.numericalError "interval too small for float precision" /-central limit theorem (for larger data)-/
        else
          let mid := (left + right) / 2.0

          if ¬(isFinite mid) then
            BisectionResult.numericalError "midpoint exceeded acceptable limit"
          else
            let fmid := f mid

            if ¬(isFinite fmid) then
              BisectionResult.numericalError s!"Function value at {mid} is not finite"
            else if fmid.abs < config.tolerance then -- count iterations after all infinity checks
              BisectionResult.success mid (iter + 1)
            else if right - left < config.tolerance then
              BisectionResult.success mid (iter + 1)
            else
              let fleft := f left
              if oppositeSigns fleft fmid then
                bisectionLoop left mid (iter + 1)
              else
                bisectionLoop mid right (iter + 1)

      bisectionLoop a b 0


def findRoot (f : Float → Float) (a b : Float) : BisectionResult :=
  bisection f a b

/- 'prettier' display of result -/
def BisectionResult.toString : BisectionResult → String
  | success root iter => s!"Root found: {root} (after {iter} iterations)"
  | invalidBounds reason => s!"Invalid bounds: {reason}"
  | maxIterationsReached approx iter => s!"Max iterations reached: best approximation {approx} (after {iter} iterations)"
  | numericalError reason => s!"Numerical error: {reason}"

/-
instance : ToString BisectionResult where
  toString := BisectionResult.toString -/

[Ruben Van de Velde]

Unfortunately, what you can prove about floats is pretty much nothing

[Oscar Matemb ⚛️]

Got it. What critics can you give about the code's structure? Any aspect of it could be refactored in some way maybe?