Checked Bounds for Partial Operations

This module provides checkers and theorems for expressions that may contain inverse-like operations (inv, log, atan, arsinh, atanh) using evalInterval? which handles domain validation.

Main definitions

Boolean Checkers

• checkUpperBoundChecked - Check upper bounds for expressions with inverse support
• checkLowerBoundChecked - Check lower bounds for expressions with inverse support
• checkStrictUpperBoundChecked - Check strict upper bounds
• checkStrictLowerBoundChecked - Check strict lower bounds

Golden Theorems

• verify_upper_bound_checked - Converts boolean check to semantic proof
• verify_lower_bound_checked - Converts boolean check to semantic proof
• verify_strict_upper_bound_checked - Strict upper bound verification
• verify_strict_lower_bound_checked - Strict lower bound verification

Bridge Theorems

• verify_upper_bound_Icc_checked - Bridge to Set.Icc upper bounds
• verify_lower_bound_Icc_checked - Bridge to Set.Icc lower bounds
• verify_strict_upper_bound_Icc_checked - Bridge to Set.Icc strict upper bounds
• verify_strict_lower_bound_Icc_checked - Bridge to Set.Icc strict lower bounds

Boolean Checkers for arbitrary expressions

NOTE: These are noncomputable because evalInterval? uses Real Taylor approximations. They cannot be used with native_decide. Use the verification theorems directly in term proofs or with explicit computation.

def LeanCert.Validity.checkUpperBoundChecked (e : Core.Expr) (I : Core.IntervalRat) (c : ℚ) : Bool

Check upper bound for arbitrary expressions. Returns true iff evalInterval?1 succeeds and the upper bound is ≤ c. NOTE: Noncomputable - cannot be used with native_decide.

Equations

• LeanCert.Validity.checkUpperBoundChecked e I c = match LeanCert.Engine.evalInterval?1 e I with | some J => decide (J.hi ≤ c) | none => false

def LeanCert.Validity.checkLowerBoundChecked (e : Core.Expr) (I : Core.IntervalRat) (c : ℚ) : Bool

Check lower bound for arbitrary expressions. Returns true iff evalInterval?1 succeeds and the lower bound is ≥ c. NOTE: Noncomputable - cannot be used with native_decide.

Equations

• LeanCert.Validity.checkLowerBoundChecked e I c = match LeanCert.Engine.evalInterval?1 e I with | some J => decide (c ≤ J.lo) | none => false

def LeanCert.Validity.checkStrictUpperBoundChecked (e : Core.Expr) (I : Core.IntervalRat) (c : ℚ) : Bool

Check strict upper bound for arbitrary expressions. NOTE: Noncomputable - cannot be used with native_decide.

Equations

• LeanCert.Validity.checkStrictUpperBoundChecked e I c = match LeanCert.Engine.evalInterval?1 e I with | some J => decide (J.hi < c) | none => false

def LeanCert.Validity.checkStrictLowerBoundChecked (e : Core.Expr) (I : Core.IntervalRat) (c : ℚ) : Bool

Check strict lower bound for arbitrary expressions. NOTE: Noncomputable - cannot be used with native_decide.

Equations

• LeanCert.Validity.checkStrictLowerBoundChecked e I c = match LeanCert.Engine.evalInterval?1 e I with | some J => decide (c < J.lo) | none => false

Golden Theorems for arbitrary expressions

theorem LeanCert.Validity.verify_upper_bound_checked (e : Core.Expr) (I : Core.IntervalRat) (c : ℚ) (h_cert : checkUpperBoundChecked e I c = true) (x : ℝ) : x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c

Verification theorem for upper bounds with arbitrary expressions.

theorem LeanCert.Validity.verify_lower_bound_checked (e : Core.Expr) (I : Core.IntervalRat) (c : ℚ) (h_cert : checkLowerBoundChecked e I c = true) (x : ℝ) : x ∈ I → ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Verification theorem for lower bounds with arbitrary expressions.

theorem LeanCert.Validity.verify_strict_upper_bound_checked (e : Core.Expr) (I : Core.IntervalRat) (c : ℚ) (h_cert : checkStrictUpperBoundChecked e I c = true) (x : ℝ) : x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e < ↑c

Verification theorem for strict upper bounds with arbitrary expressions.

theorem LeanCert.Validity.verify_strict_lower_bound_checked (e : Core.Expr) (I : Core.IntervalRat) (c : ℚ) (h_cert : checkStrictLowerBoundChecked e I c = true) (x : ℝ) : x ∈ I → ↑c < Core.Expr.eval (fun (x_1 : ℕ) => x) e

Verification theorem for strict lower bounds with arbitrary expressions.

Set.Icc Bridge Theorems for arbitrary expressions

theorem LeanCert.Validity.verify_upper_bound_Icc_checked (e : Core.Expr) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (h_cert : checkUpperBoundChecked e { lo := lo, hi := hi, le := hle } c = true) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c

Bridge theorem for Set.Icc upper bounds with arbitrary expressions.

theorem LeanCert.Validity.verify_lower_bound_Icc_checked (e : Core.Expr) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (h_cert : checkLowerBoundChecked e { lo := lo, hi := hi, le := hle } c = true) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Bridge theorem for Set.Icc lower bounds with arbitrary expressions.

theorem LeanCert.Validity.verify_strict_upper_bound_Icc_checked (e : Core.Expr) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (h_cert : checkStrictUpperBoundChecked e { lo := lo, hi := hi, le := hle } c = true) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → Core.Expr.eval (fun (x_1 : ℕ) => x) e < ↑c

Bridge theorem for Set.Icc strict upper bounds with arbitrary expressions.

theorem LeanCert.Validity.verify_strict_lower_bound_Icc_checked (e : Core.Expr) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (h_cert : checkStrictLowerBoundChecked e { lo := lo, hi := hi, le := hle } c = true) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → ↑c < Core.Expr.eval (fun (x_1 : ℕ) => x) e

Bridge theorem for Set.Icc strict lower bounds with arbitrary expressions.