Reification for interval proofs

The interval tactic translates real arithmetic into the common expression language and proves its real interpretation equal to the original expression. Numerical constants carry norm_num certificates. Unrecognized subexpressions become atoms whose bounds are collected by Bounds. One state keeps atom indices, shared syntax, and the certificates needed for equality proofs.

theorem FloatLib.Numerics.Interval.Tactic.eq_rat_of_isRat {x : ℝ} {n : ℤ} {d : ℕ} (h : Mathlib.Meta.NormNum.IsRat x n d) : x = ↑(mkRat n d)

Interpret the rational certificate produced by norm_num as a real equality.

structure FloatLib.Numerics.Interval.Tactic.RationalValue (e : Q(ℝ)) : Type

A rational value, its syntax, and a proof that a real expression has that value.

• value : ℚ

  The normalized rational value, used when comparing candidate bounds.

• rational : Q(ℚ)

  Quoted rational expression for the value.

• equality : Q(«$e» = ↑unknown_1)

  Proof that the original real expression equals this rational.

def FloatLib.Numerics.Interval.Tactic.deriveRationalValue (e : Q(ℝ)) : Lean.MetaM (RationalValue e)

Obtain a rational certificate using the registered norm_num extensions.

def FloatLib.Numerics.Interval.Tactic.rationalValue? (e : Q(ℝ)) : Lean.MetaM (Option (RationalValue e))

Recognize a closed rational expression, exposing numerical coercions when necessary.

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

Share reified subexpressions and retain their rational certificates.

• atoms : Array Q(ℝ)

  Real atoms in variable-index order.

• rationals : Lean.ExprMap Lean.Expr

  Equalities relating real leaves to their reified rational constants.

• expressions : Lean.ExprMap Q(Expr)

  Reified expressions, including atoms and repeated scalar subexpressions.

• extensions : Array Lean.Name

  Registration names, in call-index order.

• calls : Lean.ExprMap (Array Q(ℝ))

  Source arguments of registered calls, retained for their equality proofs.

partial def FloatLib.Numerics.Interval.Tactic.reify (e : Q(ℝ)) : StateRefT' IO.RealWorld ReifyState Lean.MetaM Q(Expr)

Reify real arithmetic, natural powers, and elementary functions.

Registered functions and rational constants are recognized before the structural cases. An unsupported operation is kept as an atom, so the caller must supply an interval for that complete real subexpression.

partial def FloatLib.Numerics.Interval.Tactic.evalEquality (source : Q(ℝ)) (expression : Q(Expr)) (values : Q(ℕ → ℝ)) (cache : ReifyState) (functions : Q(ℕ → List ℝ → ℝ)) : Lean.MetaM Lean.Expr

Prove that a source expression equals the real interpretation of its reified expression.

The source and syntax follow the same arithmetic operations. A variable's source term must agree definitionally with its environment entry; no numerical evaluation of a real atom is used.