Bracketing a Real Value

A location records whether an input is the lower endpoint of a half-open interval or, for an interior point, whether it lies below, at, or above the midpoint. The refinement rules transfer this information from a subdivision cell to its enclosing interval. These are the Lean counterparts of Flocq's Calc.Bracket location semantics.

inductive FloatLib.Floats.Formats.Flocq.Location : Type

Position of a real value relative to the lower endpoint and midpoint of a bracket.

• exact : Location
• inexact (midpointOrder : Ordering) : Location

@[instance_reducible]

instance FloatLib.Floats.Formats.Flocq.instDecidableEqLocation : DecidableEq Location

def FloatLib.Floats.Formats.Flocq.instDecidableEqLocation.decEq (x✝ x✝¹ : Location) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Floats.Formats.Flocq.instReprLocation : Repr Location

def FloatLib.Floats.Formats.Flocq.instReprLocation.repr : Location → ℕ → Std.Format

noncomputable def FloatLib.Floats.Formats.Flocq.inbetweenLocation (d u x : ℝ) : Location

Compute the location of x in a bracket whose lower endpoint is d.

inductive FloatLib.Floats.Formats.Flocq.Inbetween (d u x : ℝ) : Location → Prop

Semantic meaning of a bracket location.

• exact {d u x : ℝ} (hx : x = d) : Inbetween d u x Location.exact
• inexact {d u x : ℝ} (l : Ordering) (hx : d < x ∧ x < u) (hmid : cmp x ((d + u) / 2) = l) : Inbetween d u x (Location.inexact l)

theorem FloatLib.Floats.Formats.Flocq.inbetweenLocation_spec {d u x : ℝ} (_hdu : d < u) (hx : d ≤ x ∧ x < u) : Inbetween d u x (inbetweenLocation d u x)

The computed location satisfies the bracket semantics.

theorem FloatLib.Floats.Formats.Flocq.inbetween_unique {d u x : ℝ} {l l' : Location} (hl : Inbetween d u x l) (hl' : Inbetween d u x l') : l = l'

A value has at most one semantic location in a fixed bracket.

theorem FloatLib.Floats.Formats.Flocq.inbetween_bounds {d u x : ℝ} {l : Location} (hdu : d < u) (hl : Inbetween d u x l) : d ≤ x ∧ x < u

Every semantic location places the input in the half-open bracket [d, u).

theorem FloatLib.Floats.Formats.Flocq.inbetween_strict_bounds {d u x : ℝ} {order : Ordering} (hl : Inbetween d u x (Location.inexact order)) : d < x ∧ x < u

An inexact location places the input strictly between the bracket endpoints.

theorem FloatLib.Floats.Formats.Flocq.inbetween_distance {d u x : ℝ} {order : Ordering} (hl : Inbetween d u x (Location.inexact order)) : cmp (x - d) (u - x) = order

Midpoint comparison is equivalent to comparing distances from the two endpoints.

theorem FloatLib.Floats.Formats.Flocq.inbetween_abs_distance {d u x : ℝ} {order : Ordering} (hl : Inbetween d u x (Location.inexact order)) : cmp |d - x| |u - x| = order

The midpoint order also compares the absolute distances to the endpoints.

theorem FloatLib.Floats.Formats.Flocq.inbetween_exists {d u : ℝ} (hdu : d < u) (location : Location) : ∃ (x : ℝ), Inbetween d u x location

Every location is realized by a point in every nondegenerate bracket.

theorem FloatLib.Floats.Formats.Flocq.orderedSteps {start step : ℝ} (hstep : 0 < step) (k : ℤ) : start + ↑k * step < start + ↑(k + 1) * step

Consecutive points in a positive-step arithmetic progression are strictly ordered.

theorem FloatLib.Floats.Formats.Flocq.stepMidpoint (start step : ℝ) (steps : ℤ) : (start + (start + ↑steps * step)) / 2 = start + ↑steps / 2 * step

Midpoint of an arithmetic progression interval.

theorem FloatLib.Floats.Formats.Flocq.inbetween_step_interior {start step x : ℝ} {steps k : ℤ} {localLocation : Location} {globalOrder : Ordering} (hstep : 0 < step) (_hsteps : 1 < steps) (hk : 0 < k ∧ k < steps) (hl : Inbetween (start + ↑k * step) (start + ↑(k + 1) * step) x localLocation) (hmid : cmp x (start + ↑steps / 2 * step) = globalOrder) : Inbetween start (start + ↑steps * step) x (Location.inexact globalOrder)

A location in an interior arithmetic-progression cell determines a location in the full interval, given the comparison with the full midpoint.

theorem FloatLib.Floats.Formats.Flocq.inbetween_step_low {start step x : ℝ} {steps k : ℤ} {localLocation : Location} (hstep : 0 < step) (hsteps : 1 < steps) (hk : 0 < k) (hcell : 2 * k + 1 < steps) (hl : Inbetween (start + ↑k * step) (start + ↑(k + 1) * step) x localLocation) : Inbetween start (start + ↑steps * step) x (Location.inexact Ordering.lt)

A subinterval strictly below the global midpoint has global location .lt.

theorem FloatLib.Floats.Formats.Flocq.inbetween_step_high {start step x : ℝ} {steps k : ℤ} {localLocation : Location} (hstep : 0 < step) (hsteps : 1 < steps) (hcell : steps < 2 * k) (hk : k < steps) (hl : Inbetween (start + ↑k * step) (start + ↑(k + 1) * step) x localLocation) : Inbetween start (start + ↑steps * step) x (Location.inexact Ordering.gt)

A subinterval strictly above the global midpoint has global location .gt.

theorem FloatLib.Floats.Formats.Flocq.inbetween_step_zero_exact {start step x : ℝ} {steps : ℤ} (hl : Inbetween start (start + step) x Location.exact) : Inbetween start (start + ↑steps * step) x Location.exact

Exactness at the first cell's lower endpoint remains exact in the full interval.

theorem FloatLib.Floats.Formats.Flocq.inbetween_step_zero_inexact {start step x : ℝ} {steps : ℤ} {order : Ordering} (hstep : 0 < step) (hsteps : 1 < steps) (hl : Inbetween start (start + step) x (Location.inexact order)) : Inbetween start (start + ↑steps * step) x (Location.inexact Ordering.lt)

An inexact point in the first cell lies below the full midpoint when there are several cells.

theorem FloatLib.Floats.Formats.Flocq.inbetween_step_middle_even_exact {start step x : ℝ} {steps k : ℤ} (hstep : 0 < step) (hsteps : 1 < steps) (hmiddle : 2 * k = steps) (hl : Inbetween (start + ↑k * step) (start + ↑(k + 1) * step) x Location.exact) : Inbetween start (start + ↑steps * step) x (Location.inexact Ordering.eq)

At the central lower endpoint of an even subdivision, the global location is midpoint exact.

theorem FloatLib.Floats.Formats.Flocq.inbetween_step_middle_even_inexact {start step x : ℝ} {steps k : ℤ} {order : Ordering} (hstep : 0 < step) (hsteps : 1 < steps) (hmiddle : 2 * k = steps) (hl : Inbetween (start + ↑k * step) (start + ↑(k + 1) * step) x (Location.inexact order)) : Inbetween start (start + ↑steps * step) x (Location.inexact Ordering.gt)

An inexact point in the central cell of an even subdivision is above the global midpoint.

theorem FloatLib.Floats.Formats.Flocq.inbetween_step_middle_odd_exact {start step x : ℝ} {steps k : ℤ} (hstep : 0 < step) (hsteps : 1 < steps) (hmiddle : 2 * k + 1 = steps) (hl : Inbetween (start + ↑k * step) (start + ↑(k + 1) * step) x Location.exact) : Inbetween start (start + ↑steps * step) x (Location.inexact Ordering.lt)

At the lower endpoint of the central cell of an odd subdivision, the global location is low.

theorem FloatLib.Floats.Formats.Flocq.inbetween_step_middle_odd_inexact {start step x : ℝ} {steps k : ℤ} {order : Ordering} (hstep : 0 < step) (hsteps : 1 < steps) (hmiddle : 2 * k + 1 = steps) (hl : Inbetween (start + ↑k * step) (start + ↑(k + 1) * step) x (Location.inexact order)) : Inbetween start (start + ↑steps * step) x (Location.inexact order)

In the central cell of an odd subdivision, local and global midpoint locations agree.

def FloatLib.Floats.Formats.Flocq.refineLocationEven (steps k : ℤ) (location : Location) : Location

Refine a local location when the enclosing subdivision count is even.

def FloatLib.Floats.Formats.Flocq.refineLocationOdd (steps k : ℤ) (location : Location) : Location

Refine a local location when the enclosing subdivision count is odd.

theorem FloatLib.Floats.Formats.Flocq.refineLocationEven_correct {start step x : ℝ} {steps k : ℤ} {location : Location} (hstep : 0 < step) (hsteps : 1 < steps) (heven : Even steps) (hk : 0 ≤ k ∧ k < steps) (hl : Inbetween (start + ↑k * step) (start + ↑(k + 1) * step) x location) : Inbetween start (start + ↑steps * step) x (refineLocationEven steps k location)

Correctness of location refinement for an even number of cells.

theorem FloatLib.Floats.Formats.Flocq.refineLocationOdd_correct {start step x : ℝ} {steps k : ℤ} {location : Location} (hstep : 0 < step) (hsteps : 1 < steps) (hodd : Odd steps) (hk : 0 ≤ k ∧ k < steps) (hl : Inbetween (start + ↑k * step) (start + ↑(k + 1) * step) x location) : Inbetween start (start + ↑steps * step) x (refineLocationOdd steps k location)

Correctness of location refinement for an odd number of cells.

def FloatLib.Floats.Formats.Flocq.refineLocation (steps k : ℤ) (location : Location) : Location

Refine a local location, selecting the even or odd subdivision rule automatically.

The parity test is the decidable steps % 2 = 0, so this definition and the truncation layer built on it are executable.

theorem FloatLib.Floats.Formats.Flocq.refineLocation_correct {start step x : ℝ} {steps k : ℤ} {location : Location} (hstep : 0 < step) (hsteps : 1 < steps) (hk : 0 ≤ k ∧ k < steps) (hl : Inbetween (start + ↑k * step) (start + ↑(k + 1) * step) x location) : Inbetween start (start + ↑steps * step) x (refineLocation steps k location)

Correctness of automatic local-to-global location refinement.