Automatic Differentiation - Computable Evaluators

This file provides computable dual evaluators using Taylor-based approximations for transcendental functions. This enables native_decide for derivative-based bound checking.

Main definitions

• DualInterval.expCore, sinCore, cosCore - Taylor-based dual functions
• DualInterval.sinhCore, coshCore, tanhCore - Hyperbolic Taylor-based duals
• evalDualCore - Computable dual evaluator for ExprSupportedCore
• derivIntervalCore - Computable single-variable derivative interval

Main theorems

• evalDualCore_val_correct - Value component is correct
• evalDualCore_der_correct - Derivative component is correct
• derivIntervalCore_correct - Derivative interval correctness
• strictMonoOn_of_derivIntervalCore_pos - Monotonicity from positive derivative
• strictAntiOn_of_derivIntervalCore_neg - Antitonicity from negative derivative

Computable Dual Evaluation for ExprSupportedCore

This section provides a fully computable dual evaluator that uses Taylor-based approximations for transcendental functions. This enables native_decide for derivative-based bound checking.

def LeanCert.Engine.DualInterval.expCore (d : DualInterval) (n : ℕ := 10) : DualInterval

Computable dual for exp using Taylor series (chain rule: d(exp f) = exp(f) * f')

Equations

• d.expCore n = { val := d.val.expComputable n, der := (d.val.expComputable n).mul d.der }

def LeanCert.Engine.DualInterval.sinCore (d : DualInterval) (n : ℕ := 10) : DualInterval

Computable dual for sin using Taylor series

Equations

• d.sinCore n = { val := d.val.sinComputable n, der := (d.val.cosComputable n).mul d.der }

def LeanCert.Engine.DualInterval.cosCore (d : DualInterval) (n : ℕ := 10) : DualInterval

Computable dual for cos using Taylor series

Equations

• d.cosCore n = { val := d.val.cosComputable n, der := (d.val.sinComputable n).neg.mul d.der }

def LeanCert.Engine.DualInterval.logCore (d : DualInterval) (n : ℕ := 20) : DualInterval

Computable dual for log using Taylor series via atanh reduction. Chain rule: d(log f) = f' / f

Equations

• d.logCore n = { val := d.val.logComputable n, der := (LeanCert.Engine.invInterval d.val).mul d.der }

def LeanCert.Engine.DualInterval.sinhCore (d : DualInterval) (n : ℕ := 10) : DualInterval

Computable dual for sinh using Taylor series (chain rule: d(sinh f) = cosh(f) * f')

Equations

• d.sinhCore n = { val := d.val.sinhComputable n, der := (d.val.coshComputable n).mul d.der }

def LeanCert.Engine.DualInterval.coshCore (d : DualInterval) (n : ℕ := 10) : DualInterval

Computable dual for cosh using Taylor series (chain rule: d(cosh f) = sinh(f) * f')

Equations

• d.coshCore n = { val := d.val.coshComputable n, der := (d.val.sinhComputable n).mul d.der }

def LeanCert.Engine.DualInterval.tanhCore (d : DualInterval) (_n : ℕ := 10) : DualInterval

Computable dual for tanh (chain rule: d(tanh f) = sech²(f) * f') Since sech²(x) ∈ (0, 1], we use [0, 1] as a conservative bound.

Equations

• d.tanhCore _n = { val := LeanCert.Engine.tanhInterval d.val, der := d.der.mul { lo := 0, hi := 1, le := LeanCert.Engine.DualInterval.tanhCore._proof_1 } }

def LeanCert.Engine.evalDualCore (e : Core.Expr) (ρ : DualEnv) (cfg : EvalConfig := { }) : DualInterval

Computable dual interval evaluator for ExprSupportedCore expressions.

This uses Taylor series approximations for transcendental functions, making it fully computable and usable with native_decide.

For expressions outside ExprSupportedCore (inv, log, atanh), use evalDual? for domain-checked evaluation; correctness is not covered here.

Equations

• LeanCert.Engine.evalDualCore (LeanCert.Core.Expr.const q) ρ cfg = LeanCert.Engine.DualInterval.const q
• LeanCert.Engine.evalDualCore (LeanCert.Core.Expr.var idx) ρ cfg = ρ idx
• LeanCert.Engine.evalDualCore (e₁.add e₂) ρ cfg = (LeanCert.Engine.evalDualCore e₁ ρ cfg).add (LeanCert.Engine.evalDualCore e₂ ρ cfg)
• LeanCert.Engine.evalDualCore (e₁.mul e₂) ρ cfg = (LeanCert.Engine.evalDualCore e₁ ρ cfg).mul (LeanCert.Engine.evalDualCore e₂ ρ cfg)
• LeanCert.Engine.evalDualCore e_2.neg ρ cfg = (LeanCert.Engine.evalDualCore e_2 ρ cfg).neg
• LeanCert.Engine.evalDualCore e_2.inv ρ cfg = (LeanCert.Engine.evalDualCore e_2 ρ cfg).inv
• LeanCert.Engine.evalDualCore e_2.exp ρ cfg = (LeanCert.Engine.evalDualCore e_2 ρ cfg).expCore cfg.taylorDepth
• LeanCert.Engine.evalDualCore e_2.sin ρ cfg = (LeanCert.Engine.evalDualCore e_2 ρ cfg).sinCore cfg.taylorDepth
• LeanCert.Engine.evalDualCore e_2.cos ρ cfg = (LeanCert.Engine.evalDualCore e_2 ρ cfg).cosCore cfg.taylorDepth
• LeanCert.Engine.evalDualCore e_2.log ρ cfg = (LeanCert.Engine.evalDualCore e_2 ρ cfg).logCore cfg.taylorDepth
• LeanCert.Engine.evalDualCore e_2.atan ρ cfg = (LeanCert.Engine.evalDualCore e_2 ρ cfg).atan
• LeanCert.Engine.evalDualCore e_2.arsinh ρ cfg = (LeanCert.Engine.evalDualCore e_2 ρ cfg).arsinh
• LeanCert.Engine.evalDualCore e_2.atanh ρ cfg = default
• LeanCert.Engine.evalDualCore e_2.sinc ρ cfg = (LeanCert.Engine.evalDualCore e_2 ρ cfg).sinc
• LeanCert.Engine.evalDualCore e_2.erf ρ cfg = (LeanCert.Engine.evalDualCore e_2 ρ cfg).erfCore cfg.taylorDepth
• LeanCert.Engine.evalDualCore e_2.sinh ρ cfg = (LeanCert.Engine.evalDualCore e_2 ρ cfg).sinhCore cfg.taylorDepth
• LeanCert.Engine.evalDualCore e_2.cosh ρ cfg = (LeanCert.Engine.evalDualCore e_2 ρ cfg).coshCore cfg.taylorDepth
• LeanCert.Engine.evalDualCore e_2.tanh ρ cfg = (LeanCert.Engine.evalDualCore e_2 ρ cfg).tanhCore cfg.taylorDepth
• LeanCert.Engine.evalDualCore e_2.sqrt ρ cfg = (LeanCert.Engine.evalDualCore e_2 ρ cfg).sqrt
• LeanCert.Engine.evalDualCore LeanCert.Core.Expr.pi ρ cfg = LeanCert.Engine.DualInterval.piConst

def LeanCert.Engine.derivIntervalCore (e : Core.Expr) (I : Core.IntervalRat) (cfg : EvalConfig := { }) : Core.IntervalRat

Computable single-variable derivative interval

Equations

• LeanCert.Engine.derivIntervalCore e I cfg = (LeanCert.Engine.evalDualCore e (fun (x : ℕ) => LeanCert.Engine.DualInterval.varActive I) cfg).der

def LeanCert.Engine.evalDomainValidDual (e : Core.Expr) (ρ : DualEnv) (cfg : EvalConfig := { }) : Prop

Domain validity for dual evaluation. This is defined directly in terms of evalDualCore to ensure compatibility. For log, we require the argument interval to have positive lower bound.

Equations

• LeanCert.Engine.evalDomainValidDual (LeanCert.Core.Expr.const q) ρ cfg = True
• LeanCert.Engine.evalDomainValidDual (LeanCert.Core.Expr.var idx) ρ cfg = True
• LeanCert.Engine.evalDomainValidDual (e₁.add e₂) ρ cfg = (LeanCert.Engine.evalDomainValidDual e₁ ρ cfg ∧ LeanCert.Engine.evalDomainValidDual e₂ ρ cfg)
• LeanCert.Engine.evalDomainValidDual (e₁.mul e₂) ρ cfg = (LeanCert.Engine.evalDomainValidDual e₁ ρ cfg ∧ LeanCert.Engine.evalDomainValidDual e₂ ρ cfg)
• LeanCert.Engine.evalDomainValidDual e_2.neg ρ cfg = LeanCert.Engine.evalDomainValidDual e_2 ρ cfg
• LeanCert.Engine.evalDomainValidDual e_2.inv ρ cfg = LeanCert.Engine.evalDomainValidDual e_2 ρ cfg
• LeanCert.Engine.evalDomainValidDual e_2.exp ρ cfg = LeanCert.Engine.evalDomainValidDual e_2 ρ cfg
• LeanCert.Engine.evalDomainValidDual e_2.sin ρ cfg = LeanCert.Engine.evalDomainValidDual e_2 ρ cfg
• LeanCert.Engine.evalDomainValidDual e_2.cos ρ cfg = LeanCert.Engine.evalDomainValidDual e_2 ρ cfg
• LeanCert.Engine.evalDomainValidDual e_2.log ρ cfg = (LeanCert.Engine.evalDomainValidDual e_2 ρ cfg ∧ (LeanCert.Engine.evalDualCore e_2 ρ cfg).val.lo > 0)
• LeanCert.Engine.evalDomainValidDual e_2.atan ρ cfg = LeanCert.Engine.evalDomainValidDual e_2 ρ cfg
• LeanCert.Engine.evalDomainValidDual e_2.arsinh ρ cfg = LeanCert.Engine.evalDomainValidDual e_2 ρ cfg
• LeanCert.Engine.evalDomainValidDual e_2.atanh ρ cfg = LeanCert.Engine.evalDomainValidDual e_2 ρ cfg
• LeanCert.Engine.evalDomainValidDual e_2.sinc ρ cfg = LeanCert.Engine.evalDomainValidDual e_2 ρ cfg
• LeanCert.Engine.evalDomainValidDual e_2.erf ρ cfg = LeanCert.Engine.evalDomainValidDual e_2 ρ cfg
• LeanCert.Engine.evalDomainValidDual e_2.sinh ρ cfg = LeanCert.Engine.evalDomainValidDual e_2 ρ cfg
• LeanCert.Engine.evalDomainValidDual e_2.cosh ρ cfg = LeanCert.Engine.evalDomainValidDual e_2 ρ cfg
• LeanCert.Engine.evalDomainValidDual e_2.tanh ρ cfg = LeanCert.Engine.evalDomainValidDual e_2 ρ cfg
• LeanCert.Engine.evalDomainValidDual e_2.sqrt ρ cfg = LeanCert.Engine.evalDomainValidDual e_2 ρ cfg
• LeanCert.Engine.evalDomainValidDual LeanCert.Core.Expr.pi ρ cfg = True

theorem LeanCert.Engine.evalDualCore_val_correct (e : Core.Expr) (hsupp : ExprSupportedCore e) (ρ_real : ℕ → ℝ) (ρ_dual : DualEnv) (cfg : EvalConfig) (hρ : ∀ (i : ℕ), ρ_real i ∈ (ρ_dual i).val) (hdom : evalDomainValidDual e ρ_dual cfg) : Core.Expr.eval ρ_real e ∈ (evalDualCore e ρ_dual cfg).val

Correctness theorem for computable dual value component.

Note: Requires domain validity for log (positive argument interval).

theorem LeanCert.Engine.evalDomainValidDual_of_ExprSupported (e : Core.Expr) (hsupp : ExprSupported e) (ρ : DualEnv) (cfg : EvalConfig) : evalDomainValidDual e ρ cfg

For ExprSupported expressions (which exclude log), domain validity is trivially true. This is because ExprSupported has no log constructor.

theorem LeanCert.Engine.evalDualCore_der_correct (e : Core.Expr) (hsupp : ExprSupported e) (I : Core.IntervalRat) (x : ℝ) (hx : x ∈ I) (cfg : EvalConfig) : deriv (evalFunc1 e) x ∈ (evalDualCore e (fun (x : ℕ) => DualInterval.varActive I) cfg).der

Correctness theorem for computable dual derivative component. Uses ExprSupported since derivative correctness requires differentiability.

theorem LeanCert.Engine.derivIntervalCore_correct (e : Core.Expr) (hsupp : ExprSupported e) (I : Core.IntervalRat) (x : ℝ) (hx : x ∈ I) (cfg : EvalConfig) : deriv (evalFunc1 e) x ∈ derivIntervalCore e I cfg

Convenience theorem: derivIntervalCore correctness

theorem LeanCert.Engine.derivIntervalCore_nonzero_implies_deriv_nonzero (e : Core.Expr) (hsupp : ExprSupported e) (I : Core.IntervalRat) (cfg : EvalConfig) (h : ¬(derivIntervalCore e I cfg).containsZero) (x : ℝ) : x ∈ I → deriv (evalFunc1 e) x ≠ 0

If derivIntervalCore doesn't contain zero, the derivative is nonzero everywhere on I. This is a key theorem for Newton contraction analysis.

theorem LeanCert.Engine.derivIntervalCore_pos_implies_deriv_pos (e : Core.Expr) (hsupp : ExprSupported e) (I : Core.IntervalRat) (cfg : EvalConfig) (h : 0 < (derivIntervalCore e I cfg).lo) (x : ℝ) : x ∈ I → 0 < deriv (evalFunc1 e) x

If derivIntervalCore.lo > 0, then the derivative is positive everywhere on I.

theorem LeanCert.Engine.derivIntervalCore_neg_implies_deriv_neg (e : Core.Expr) (hsupp : ExprSupported e) (I : Core.IntervalRat) (cfg : EvalConfig) (h : (derivIntervalCore e I cfg).hi < 0) (x : ℝ) : x ∈ I → deriv (evalFunc1 e) x < 0

If derivIntervalCore.hi < 0, then the derivative is negative everywhere on I.

theorem LeanCert.Engine.strictMonoOn_of_derivIntervalCore_pos (e : Core.Expr) (hsupp : ExprSupported e) (I : Core.IntervalRat) (cfg : EvalConfig) (hpos : 0 < (derivIntervalCore e I cfg).lo) : StrictMonoOn (evalFunc1 e) (Set.Icc ↑I.lo ↑I.hi)

Strictly positive derivative (via Core bounds) implies strict monotonicity

theorem LeanCert.Engine.strictAntiOn_of_derivIntervalCore_neg (e : Core.Expr) (hsupp : ExprSupported e) (I : Core.IntervalRat) (cfg : EvalConfig) (hneg : (derivIntervalCore e I cfg).hi < 0) : StrictAntiOn (evalFunc1 e) (Set.Icc ↑I.lo ↑I.hi)

Strictly negative derivative (via Core bounds) implies strict antitonicity