Interval expressions and endpoint backends

An expression records the numerical operations independently of its endpoint representation. Backend supplies executable enclosures; its real-containment contract is stated in Real. The same expression can therefore run with exact rational endpoints, an integer binary grid, or a format-specific outward rounder.

Evaluation returns none when an input is missing or a backend cannot enclose an operation. In particular, a backend may reject division across zero or an interval outside a function's domain. Success is related to real evaluation by Expr.containsReal_eval?.

structure FloatLib.Numerics.Interval.Backend.Config : Type

Accuracy controls shared by built-in operations and user enclosures.

• precision : ℕ

  Fractional endpoint bits, also used for square-root approximations.

• degree : ℕ

  Approximation degree for elementary functions.

@[instance_reducible]

instance FloatLib.Numerics.Interval.Backend.instDecidableEqConfig : DecidableEq Config

def FloatLib.Numerics.Interval.Backend.instDecidableEqConfig.decEq (x✝ x✝¹ : Config) : Decidable (x✝ = x✝¹)

def FloatLib.Numerics.Interval.Backend.instReprConfig.repr : Config → ℕ → Std.Format

@[instance_reducible]

instance FloatLib.Numerics.Interval.Backend.instReprConfig : Repr Config

@[instance_reducible]

instance FloatLib.Numerics.Interval.Backend.instInhabitedConfig : Inhabited Config

structure FloatLib.Numerics.Interval.Extension : Type

An executable rational enclosure for an operation with a fixed number of real arguments. Constants have arity zero. Extension.Sound supplies its separate containment contract.

• arity : ℕ

  Number of real arguments.

• enclose? : Backend.Config → List (Interval ℚ) → Option (Interval ℚ)

  Enclose the operation, or reject an unsupported input domain.

def FloatLib.Numerics.Interval.Extension.constant (bounds : Backend.Config → Option (Interval ℚ)) : Extension

Adapt a constant enclosure to the common argument-list interface.

def FloatLib.Numerics.Interval.Extension.unary (bounds : Backend.Config → Interval ℚ → Option (Interval ℚ)) : Extension

Adapt a unary enclosure to the common argument-list interface.

def FloatLib.Numerics.Interval.Extension.binary (bounds : Backend.Config → Interval ℚ → Interval ℚ → Option (Interval ℚ)) : Extension

Adapt a binary enclosure to the common argument-list interface.

inductive FloatLib.Numerics.Interval.UnaryOp : Type

Unary operations supported by the common interval expression language.

• neg : UnaryOp
• abs : UnaryOp
• inv : UnaryOp
• pow (exponent : ℕ) : UnaryOp
• exp : UnaryOp
• log : UnaryOp
• sin : UnaryOp
• cos : UnaryOp
• tan : UnaryOp
• asin : UnaryOp
• acos : UnaryOp
• atan : UnaryOp
• sinh : UnaryOp
• cosh : UnaryOp
• tanh : UnaryOp
• sqrt : UnaryOp

@[instance_reducible]

instance FloatLib.Numerics.Interval.instDecidableEqUnaryOp : DecidableEq UnaryOp

def FloatLib.Numerics.Interval.instDecidableEqUnaryOp.decEq (x✝ x✝¹ : UnaryOp) : Decidable (x✝ = x✝¹)

def FloatLib.Numerics.Interval.instReprUnaryOp.repr : UnaryOp → ℕ → Std.Format

@[instance_reducible]

instance FloatLib.Numerics.Interval.instReprUnaryOp : Repr UnaryOp

inductive FloatLib.Numerics.Interval.BinaryOp : Type

Binary operations supported by the common interval expression language.

• add : BinaryOp
• sub : BinaryOp
• mul : BinaryOp
• div : BinaryOp
• min : BinaryOp
• max : BinaryOp

@[instance_reducible]

instance FloatLib.Numerics.Interval.instDecidableEqBinaryOp : DecidableEq BinaryOp

@[instance_reducible]

instance FloatLib.Numerics.Interval.instReprBinaryOp : Repr BinaryOp

def FloatLib.Numerics.Interval.instReprBinaryOp.repr : BinaryOp → ℕ → Std.Format

inductive FloatLib.Numerics.Interval.TernaryOp : Type

Three-input operations supported by the common interval expression language.

• fma : TernaryOp

@[instance_reducible]

instance FloatLib.Numerics.Interval.instDecidableEqTernaryOp : DecidableEq TernaryOp

def FloatLib.Numerics.Interval.instReprTernaryOp.repr : TernaryOp → ℕ → Std.Format

@[instance_reducible]

instance FloatLib.Numerics.Interval.instReprTernaryOp : Repr TernaryOp

inductive FloatLib.Numerics.Interval.Expr : Type

A real expression with rational constants, numbered variables, and registered calls.

• const (value : ℚ) : Expr
• var (index : ℕ) : Expr
• unary (op : UnaryOp) (arg : Expr) : Expr
• binary (op : BinaryOp) (left right : Expr) : Expr
• ternary (op : TernaryOp) (first second third : Expr) : Expr
• call (index : ℕ) (args : List Expr) : Expr

partial def FloatLib.Numerics.Interval.instReprExpr.repr : Expr → ℕ → Std.Format

@[instance_reducible]

instance FloatLib.Numerics.Interval.instReprExpr : Repr Expr

def FloatLib.Numerics.Interval.Expr.beq : Expr → Expr → Bool

Structural Boolean comparison, including registered argument lists.

def FloatLib.Numerics.Interval.Expr.beqArgs : List Expr → List Expr → Bool

Structural comparison of the argument lists of registered calls.

theorem FloatLib.Numerics.Interval.Expr.beq_eq_true_iff (a b : Expr) : a.beq b = true ↔ a = b

Boolean expression comparison is exact.

@[instance_reducible]

instance FloatLib.Numerics.Interval.instDecidableEqExpr : DecidableEq Expr

@[instance_reducible]

instance FloatLib.Numerics.Interval.instAddExpr : Add Expr

Build an addition expression; evaluation uses the selected backend.

@[instance_reducible]

instance FloatLib.Numerics.Interval.instMulExpr : Mul Expr

Build a multiplication expression; evaluation uses the selected backend.

structure FloatLib.Numerics.Interval.Backend (α : Type u_1) : Type u_1

Executable interval operations for an endpoint representation.

The decoder identifies the exact rational value of each usable endpoint. Operations may work directly on the representation without decoding intermediate results. Backend.Sound is the separate proof contract required to use an evaluation in a theorem.

• decode : α → Option ℚ

  Exact rational interpretation of a finite endpoint.

• const? : ℚ → Option (Interval α)

  Enclose a rational constant.

• unary? : UnaryOp → Interval α → Option (Interval α)

  Enclose a unary operation, or reject its domain or unavailable output range.

• binary? : BinaryOp → Interval α → Interval α → Option (Interval α)

  Enclose a binary operation, or reject its domain or unavailable output range.

• ternary? : TernaryOp → Interval α → Interval α → Interval α → Option (Interval α)

  Enclose a three-input operation, or reject an unavailable output range.

• call? : ℕ → List (Interval α) → Option (Interval α)

  Enclose a registered operation; unavailable indices must fail.

def FloatLib.Numerics.Interval.Expr.eval? {α : Type u_1} (e : Expr) (B : Backend α) (env : ℕ → Option (Interval α)) : Option (Interval α)

Evaluate an expression with the selected backend and variable intervals.

The environment may be partial. Missing variables and failed operations propagate as none; no default numerical value is substituted.

def FloatLib.Numerics.Interval.Expr.evalArgs? {α : Type u_1} (args : List Expr) (B : Backend α) (env : ℕ → Option (Interval α)) : Option (List (Interval α))

Evaluate all arguments of a registered call, preserving failure and argument order.