Expression Support Predicates

This file defines predicates indicating which expressions are supported by different interval evaluation strategies.

Main definitions

• ExprSupportedCore - Predicate for expressions in the computable subset (const, var, add, mul, neg, sin, cos, exp, log, sqrt, sinh, cosh, tanh, erf, pi)

• ExprSupported - Predicate for the noncomputable AD subset (const, var, add, mul, neg, sin, cos, exp)

• ExprSupportedWithInv - Syntactic support predicate for expressions with inv and log

Design notes

The predicates are ordered by generality:

• ExprSupported ⊆ ExprSupportedCore (via ExprSupported.toCore)
• ExprSupported ⊆ ExprSupportedWithInv (via ExprSupported.toWithInv)

The core subset is kept computable so that tactics can use native_decide for interval bound checking. The extended subset uses Real.exp with floor/ceil bounds, which requires noncomputability.

Core supported expression subset (computable)

inductive LeanCert.Core.ExprSupportedCore : Expr → Prop

Predicate indicating an expression is in the computable core subset. Supports: const, var, add, mul, neg, sin, cos, exp, log, sqrt, sinh, cosh, tanh, erf, pi

Note: log requires positive domain for correctness. The correctness theorem evalIntervalCore_correct has an additional hypothesis evalDomainValid that ensures log arguments evaluate to positive intervals.

• const (q : ℚ) : ExprSupportedCore (Expr.const q)
• var (idx : ℕ) : ExprSupportedCore (Expr.var idx)
• add {e₁ e₂ : Expr} : ExprSupportedCore e₁ → ExprSupportedCore e₂ → ExprSupportedCore (e₁.add e₂)
• mul {e₁ e₂ : Expr} : ExprSupportedCore e₁ → ExprSupportedCore e₂ → ExprSupportedCore (e₁.mul e₂)
• neg {e : Expr} : ExprSupportedCore e → ExprSupportedCore e.neg
• sin {e : Expr} : ExprSupportedCore e → ExprSupportedCore e.sin
• cos {e : Expr} : ExprSupportedCore e → ExprSupportedCore e.cos
• exp {e : Expr} : ExprSupportedCore e → ExprSupportedCore e.exp
• log {e : Expr} : ExprSupportedCore e → ExprSupportedCore e.log
• sqrt {e : Expr} : ExprSupportedCore e → ExprSupportedCore e.sqrt
• sinh {e : Expr} : ExprSupportedCore e → ExprSupportedCore e.sinh
• cosh {e : Expr} : ExprSupportedCore e → ExprSupportedCore e.cosh
• tanh {e : Expr} : ExprSupportedCore e → ExprSupportedCore e.tanh
• erf {e : Expr} : ExprSupportedCore e → ExprSupportedCore e.erf
• pi : ExprSupportedCore Expr.pi

Extended supported expression subset (with exp)

inductive LeanCert.Core.ExprSupported : Expr → Prop

Predicate indicating an expression is in the fully-verified subset for AD. Supports: const, var, add, mul, neg, sin, cos, exp Does NOT support:

• sqrt (not differentiable at 0 - use ExprSupportedCore for interval evaluation only)
• inv (requires nonzero interval checks)
• log (requires positive interval checks)
• atan/arsinh/atanh (derivative proofs incomplete - use ExprSupportedWithInv + evalInterval?)

• const (q : ℚ) : ExprSupported (Expr.const q)
• var (idx : ℕ) : ExprSupported (Expr.var idx)
• add {e₁ e₂ : Expr} : ExprSupported e₁ → ExprSupported e₂ → ExprSupported (e₁.add e₂)
• mul {e₁ e₂ : Expr} : ExprSupported e₁ → ExprSupported e₂ → ExprSupported (e₁.mul e₂)
• neg {e : Expr} : ExprSupported e → ExprSupported e.neg
• sin {e : Expr} : ExprSupported e → ExprSupported e.sin
• cos {e : Expr} : ExprSupported e → ExprSupported e.cos
• exp {e : Expr} : ExprSupported e → ExprSupported e.exp

theorem LeanCert.Core.ExprSupported.toCore {e : Expr} (h : ExprSupported e) : ExprSupportedCore e

ExprSupported expressions are also in ExprSupportedCore

Syntactic support predicate with inv and log

inductive LeanCert.Core.ExprSupportedWithInv : Expr → Prop

Syntactic support predicate for expressions with inv and log (no semantic conditions). This is the most general support predicate, allowing all expression constructors. Semantic correctness is handled by evalInterval? returning None when conditions fail.

• const (q : ℚ) : ExprSupportedWithInv (Expr.const q)
• var (idx : ℕ) : ExprSupportedWithInv (Expr.var idx)
• add {e₁ e₂ : Expr} : ExprSupportedWithInv e₁ → ExprSupportedWithInv e₂ → ExprSupportedWithInv (e₁.add e₂)
• mul {e₁ e₂ : Expr} : ExprSupportedWithInv e₁ → ExprSupportedWithInv e₂ → ExprSupportedWithInv (e₁.mul e₂)
• neg {e : Expr} : ExprSupportedWithInv e → ExprSupportedWithInv e.neg
• inv {e : Expr} : ExprSupportedWithInv e → ExprSupportedWithInv e.inv
• exp {e : Expr} : ExprSupportedWithInv e → ExprSupportedWithInv e.exp
• sin {e : Expr} : ExprSupportedWithInv e → ExprSupportedWithInv e.sin
• cos {e : Expr} : ExprSupportedWithInv e → ExprSupportedWithInv e.cos
• log {e : Expr} : ExprSupportedWithInv e → ExprSupportedWithInv e.log
• atan {e : Expr} : ExprSupportedWithInv e → ExprSupportedWithInv e.atan
• arsinh {e : Expr} : ExprSupportedWithInv e → ExprSupportedWithInv e.arsinh
• atanh {e : Expr} : ExprSupportedWithInv e → ExprSupportedWithInv e.atanh
• sinc {e : Expr} : ExprSupportedWithInv e → ExprSupportedWithInv e.sinc
• erf {e : Expr} : ExprSupportedWithInv e → ExprSupportedWithInv e.erf
• sqrt {e : Expr} : ExprSupportedWithInv e → ExprSupportedWithInv e.sqrt
• pi : ExprSupportedWithInv Expr.pi

theorem LeanCert.Core.ExprSupported.toWithInv {e : Expr} (h : ExprSupported e) : ExprSupportedWithInv e

ExprSupported implies ExprSupportedWithInv