Execute fully polymorphic defs for floats and real-val funcs

Stream: mathlib4

[Oscar Matemb ⚛️]

We’ve implemented the bisection numerical method here. I posted about it a few months ago as well. 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 want make it fully polymorphic to work with both Float and ℝ, and prove termination, convergence, continuity properties and so on ... for the ℝ. Currently the polymorphic version we came up with looks like this,

-- main loop w/ no float-specific checks
def bisectionCore {α : Type*} [LinearOrder α] [Field α ] [Add α] [Sub α] [Div α] [...]
    (f : α → α) (interval : Interval α) (config : Config α) : Option α :=
  if intervalSmallEnough interval config then
    some (midpoint interval)
  else
    let newInterval := shortenInterval f interval
    bisectionCore f newInterval config


noncomputable def bisectionReal (f : ℝ → ℝ) (a b tol : ℝ)
    (h_cont : ContinuousOn f (Set.Icc a b))
    (h_sign : f a * f b < 0) : ℝ :=
  bisectionCore f ⟨a, b⟩ ⟨tol⟩

-- Continuity theorem
noncomputable def bisectionWithContinuity (f : ℝ → ℝ) (a b tol : ℝ)
    (h_order : a < b)
    (h_tol : 0 < tol)
    (h_cont : ContinuousOn f (Set.Icc a b))
    (h_sign : f a * f b < 0) : ℝ :=
  let interval : bisecInterval ℝ := ⟨a, b, h_order⟩
  let config : BisectionConfig ℝ := ⟨tol, h_tol⟩
  bisectionCore f interval config

-- Convergence theorem
theorem bisection_converges (f : ℝ → ℝ) (a b tol : ℝ)
    (h_cont : ContinuousOn f (Set.Icc a b))
    (h_sign : f a * f b < 0) :
    let result := bisectionReal f a b tol h_cont h_sign
    ∃ root : ℝ, a ≤ root ∧ root ≤ b ∧ f root = 0 ∧
    |result - root| ≤ tol := by
  sorry

I have a few questions :

• What typeclasses or bundled structures could we use ? We've tried [LinearOrder α] [Add α] [Sub α] [Div α] [OfNat α 0] [OfNat α 2] [Field α] [IsOrderedRing α]
• How to handle abs val for reals? Does mathlib have a typeclass to help handle this?
• Should real-valued funcs it return ℝ directly, or Option ℝ, or something else? The Float version returns a sum type with error cases we included , but for Real with proofs, is there need to guarantee success of result?
• I know there is stuff in mathlib for IVT, but it is still ideal to prove convergence and/or continuity seperately?

here's a mwe:

import Mathlib

def bisectionSimple {α : Type*}
    [LinearOrder α] [Add α] [Sub α] [Div α] [OfNat α 2]
    (f : α → α) (a b tolerance : α) (maxIter : Nat) : Option α :=
  if a >= b then none
  else
    let rec loop (left right : α) (iter : Nat) : Option α :=
      if iter >= maxIter || right - left < tolerance then
        some ((left + right) / 2)
      else
        let mid := (left + right) / 2
        let fleft := f left
        let fmid := f mid
        if (fleft > 0 && fmid < 0) || (fleft < 0 && fmid > 0) then
          loop left mid (iter + 1)
        else
          loop mid right (iter + 1)
    loop a b 0


def testFloat : Option Float :=
  bisectionSimple (fun x => x * x - 2.0) 1.0 2.0 1e-6 100

#eval testFloat  -- approx 1.4142135...

noncomputable def testReal : Option ℝ :=
  bisectionSimple (fun x => x^2 - 2) 1 2 (1/1000000) 100

[Eric Wieser]

When you write

[Add α] [Sub α] [Div α] [OfNat α 0] [OfNat α 2] [Field α]

this means "let α have two unrelated +s, -s, 0s, and 2s". You should either drop Field or drop the other five.

[Eric Wieser]

(note that Field Float is false, which should make clear that it is Field you need to drop)