Hypothesis bounds and certified input boxes

Direct and pointwise hypotheses supply rational endpoints for the real atoms discovered by the reifier. The strongest endpoints form the input box, with a proof of each coordinate's membership. Strict hypotheses are conservatively weakened; unresolved indices or guards supply no bounds.

structure FloatLib.Numerics.Interval.Tactic.Bound : Type

A rational lower or upper bound, carrying a proof of the real inequality.

• term : Q(ℝ)

  Real term bounded by this hypothesis.

• value : ℚ

  Rational endpoint, used to select the strongest available bound.

• rational : Q(ℚ)

  Quoted syntax of that endpoint.

• lower : Bool

  Whether the endpoint is a lower bound rather than an upper bound.

• proof : Lean.Expr

  Proof of rational ≤ term when lower is true, and of term ≤ rational otherwise.

partial def FloatLib.Numerics.Interval.Tactic.boundsOfProofFor (atoms : Array Q(ℝ)) (proof : Lean.Expr) : Lean.MetaM (Array Bound)

Extract direct bounds and instantiate universally quantified bounds at the supplied atoms.

For example, ∀ i, x i ∈ Set.Icc lo hi supplies the bounds for each used x i. Unused entries are not enumerated. Concrete guards such as i ∈ Finset.range n are proved before applying a guarded hypothesis; an unresolved index or guard supplies no bounds.

structure FloatLib.Numerics.Interval.Tactic.ReifiedBox : Type

A rational box and the proof that its ordered real coordinates belong to it.

• box : Q(Box)

  Rational intervals in variable-index order.

• reals : Q(List ℝ)

  Real terms in the same order as the box coordinates.

• membership : Q(unknown_1.ContainsReal fun (i : ℕ) => unknown_2[i]?.getD 0)

  Proof that each real term belongs to its corresponding interval.

def FloatLib.Numerics.Interval.Tactic.reifyBox (bounds : Array Bound) : List Q(ℝ) → Lean.MetaM ReifiedBox

Select the strongest endpoints and prove membership, without an intermediate coordinate.