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)

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

Design notes

ADSupported is the differentiable fragment used by automatic differentiation. It is contained in ExprSupportedCore via ADSupported.toCore. Checked evaluators accept arbitrary expressions and encode domain failure in their result type, so they need no syntactic support predicate.

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
• namedConst (c : MathConst) : ExprSupportedCore (Expr.namedConst c)

Extended supported expression subset (with exp)

inductive LeanCert.Core.ADSupported : 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 in the total AD evaluator)

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

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

ADSupported expressions are also in ExprSupportedCore

def LeanCert.Core.Expr.checkADSupported : Expr → Bool

Computable recognition of the differentiable ADSupported subset used by Newton/AD backends.

Equations

• (LeanCert.Core.Expr.const q).checkADSupported = true
• (LeanCert.Core.Expr.var idx).checkADSupported = true
• (e₁.add e₂).checkADSupported = (e₁.checkADSupported && e₂.checkADSupported)
• (e₁.mul e₂).checkADSupported = (e₁.checkADSupported && e₂.checkADSupported)
• e.neg.checkADSupported = e.checkADSupported
• e.exp.checkADSupported = e.checkADSupported
• e.sin.checkADSupported = e.checkADSupported
• e.cos.checkADSupported = e.checkADSupported
• x✝.checkADSupported = false

theorem LeanCert.Core.Expr.checkADSupported_eq_true_iff (e : Expr) : e.checkADSupported = true ↔ ADSupported e

The executable support check recognizes exactly the differentiable ADSupported fragment used by the checked AD/monotonicity backend.

def LeanCert.Core.Expr.checkSupportedCore : Expr → Bool

Computable recognition of ExprSupportedCore.

Equations

• (LeanCert.Core.Expr.const q).checkSupportedCore = true
• (LeanCert.Core.Expr.var idx).checkSupportedCore = true
• (LeanCert.Core.Expr.namedConst c).checkSupportedCore = true
• (e₁.add e₂).checkSupportedCore = (e₁.checkSupportedCore && e₂.checkSupportedCore)
• (e₁.mul e₂).checkSupportedCore = (e₁.checkSupportedCore && e₂.checkSupportedCore)
• e.neg.checkSupportedCore = e.checkSupportedCore
• e.exp.checkSupportedCore = e.checkSupportedCore
• e.sin.checkSupportedCore = e.checkSupportedCore
• e.cos.checkSupportedCore = e.checkSupportedCore
• e.log.checkSupportedCore = e.checkSupportedCore
• e.sqrt.checkSupportedCore = e.checkSupportedCore
• e.sinh.checkSupportedCore = e.checkSupportedCore
• e.cosh.checkSupportedCore = e.checkSupportedCore
• e.tanh.checkSupportedCore = e.checkSupportedCore
• e.erf.checkSupportedCore = e.checkSupportedCore
• x✝.checkSupportedCore = false

theorem LeanCert.Core.Expr.checkSupportedCore_correct {e : Expr} (h : e.checkSupportedCore = true) : ExprSupportedCore e

A successful computable core-support check produces the corresponding proof object required by the tight Rational evaluator theorem.