Automatic Differentiation - Evaluators

This file provides the evaluation functions for automatic differentiation, mapping expressions to dual intervals.

Main definitions

• DualEnv - Environment mapping variable indices to dual intervals
• LeanCert.Internal.AD.evalUnchecked - Main evaluator for supported expressions (total)
• evalDual? - Partial evaluator supporting domain-checked functions (returns Option)
• evalDual?1 - Single-variable version of evalDual?
• mkDualEnv - Create a dual environment for differentiation w.r.t. a variable
• evalWithDeriv - Evaluate and differentiate w.r.t. a variable index
• derivInterval - Get just the derivative interval
• evalWithDeriv1 - Single-variable evaluation and differentiation

Dual evaluation

@[reducible, inline]

abbrev LeanCert.Engine.DualEnv : Type

Environment for dual evaluation

Equations

• LeanCert.Engine.DualEnv = (ℕ → LeanCert.Engine.DualInterval)

noncomputable def LeanCert.Internal.AD.evalUnchecked (e : Core.Expr) (ρ : Engine.DualEnv) : Engine.DualInterval

Evaluate expression in dual interval mode.

For supported expressions (const, var, add, mul, neg, sin, cos, exp), this computes correct dual interval bounds with a fully-verified proof.

For unsupported expressions (inv, log), returns a default interval. Do not rely on results for expressions containing inv or log. Use evalDual? for partial functions like inv and log.

Equations

• LeanCert.Internal.AD.evalUnchecked (LeanCert.Core.Expr.const q) ρ = LeanCert.Engine.DualInterval.const q
• LeanCert.Internal.AD.evalUnchecked (LeanCert.Core.Expr.var idx) ρ = ρ idx
• LeanCert.Internal.AD.evalUnchecked (e₁.add e₂) ρ = (LeanCert.Internal.AD.evalUnchecked e₁ ρ).add (LeanCert.Internal.AD.evalUnchecked e₂ ρ)
• LeanCert.Internal.AD.evalUnchecked (e₁.mul e₂) ρ = (LeanCert.Internal.AD.evalUnchecked e₁ ρ).mul (LeanCert.Internal.AD.evalUnchecked e₂ ρ)
• LeanCert.Internal.AD.evalUnchecked e_2.neg ρ = (LeanCert.Internal.AD.evalUnchecked e_2 ρ).neg
• LeanCert.Internal.AD.evalUnchecked e_2.inv ρ = default
• LeanCert.Internal.AD.evalUnchecked e_2.exp ρ = (LeanCert.Internal.AD.evalUnchecked e_2 ρ).exp
• LeanCert.Internal.AD.evalUnchecked e_2.sin ρ = (LeanCert.Internal.AD.evalUnchecked e_2 ρ).sin
• LeanCert.Internal.AD.evalUnchecked e_2.cos ρ = (LeanCert.Internal.AD.evalUnchecked e_2 ρ).cos
• LeanCert.Internal.AD.evalUnchecked e_2.log ρ = default
• LeanCert.Internal.AD.evalUnchecked e_2.atan ρ = (LeanCert.Internal.AD.evalUnchecked e_2 ρ).atan
• LeanCert.Internal.AD.evalUnchecked e_2.arsinh ρ = (LeanCert.Internal.AD.evalUnchecked e_2 ρ).arsinh
• LeanCert.Internal.AD.evalUnchecked e_2.atanh ρ = default
• LeanCert.Internal.AD.evalUnchecked e_2.sinc ρ = (LeanCert.Internal.AD.evalUnchecked e_2 ρ).sinc
• LeanCert.Internal.AD.evalUnchecked e_2.erf ρ = (LeanCert.Internal.AD.evalUnchecked e_2 ρ).erf
• LeanCert.Internal.AD.evalUnchecked e_2.sinh ρ = (LeanCert.Internal.AD.evalUnchecked e_2 ρ).sinh
• LeanCert.Internal.AD.evalUnchecked e_2.cosh ρ = (LeanCert.Internal.AD.evalUnchecked e_2 ρ).cosh
• LeanCert.Internal.AD.evalUnchecked e_2.tanh ρ = (LeanCert.Internal.AD.evalUnchecked e_2 ρ).tanh
• LeanCert.Internal.AD.evalUnchecked e_2.sqrt ρ = (LeanCert.Internal.AD.evalUnchecked e_2 ρ).sqrt
• LeanCert.Internal.AD.evalUnchecked (LeanCert.Core.Expr.namedConst c) ρ = LeanCert.Engine.DualInterval.ofMathConst c

Partial dual evaluation

noncomputable def LeanCert.Engine.evalDual? (e : Core.Expr) (ρ : DualEnv) : Option DualInterval

Partial dual evaluator that supports domain-checked functions. Returns none if any domain error would occur:

• inv of an interval containing zero
• log of an interval not strictly positive When it returns some, the result is guaranteed to be correct.

The total and computable dual evaluators support tanh, but this Option-returning evaluator deliberately keeps tanh disabled until the evalDual?-specific value/differentiability/derivative correctness path is wired for that constructor.

Equations

• LeanCert.Engine.evalDual? (LeanCert.Core.Expr.const q) ρ = some (LeanCert.Engine.DualInterval.const q)
• LeanCert.Engine.evalDual? (LeanCert.Core.Expr.var idx) ρ = some (ρ idx)
• LeanCert.Engine.evalDual? (e₁.add e₂) ρ = match LeanCert.Engine.evalDual? e₁ ρ, LeanCert.Engine.evalDual? e₂ ρ with | some d₁, some d₂ => some (d₁.add d₂) | x, x_1 => none
• LeanCert.Engine.evalDual? (e₁.mul e₂) ρ = match LeanCert.Engine.evalDual? e₁ ρ, LeanCert.Engine.evalDual? e₂ ρ with | some d₁, some d₂ => some (d₁.mul d₂) | x, x_1 => none
• LeanCert.Engine.evalDual? e_2.neg ρ = match LeanCert.Engine.evalDual? e_2 ρ with | some d => some d.neg | none => none
• LeanCert.Engine.evalDual? e_2.inv ρ = match LeanCert.Engine.evalDual? e_2 ρ with | none => none | some d => d.inv?
• LeanCert.Engine.evalDual? e_2.exp ρ = match LeanCert.Engine.evalDual? e_2 ρ with | some d => some d.exp | none => none
• LeanCert.Engine.evalDual? e_2.sin ρ = match LeanCert.Engine.evalDual? e_2 ρ with | some d => some d.sin | none => none
• LeanCert.Engine.evalDual? e_2.cos ρ = match LeanCert.Engine.evalDual? e_2 ρ with | some d => some d.cos | none => none
• LeanCert.Engine.evalDual? e_2.log ρ = match LeanCert.Engine.evalDual? e_2 ρ with | none => none | some d => d.log?
• LeanCert.Engine.evalDual? e_2.atan ρ = match LeanCert.Engine.evalDual? e_2 ρ with | some d => some d.atan | none => none
• LeanCert.Engine.evalDual? e_2.arsinh ρ = match LeanCert.Engine.evalDual? e_2 ρ with | some d => some d.arsinh | none => none
• LeanCert.Engine.evalDual? e_2.atanh ρ = none
• LeanCert.Engine.evalDual? e_2.sinc ρ = match LeanCert.Engine.evalDual? e_2 ρ with | some d => some d.sinc | none => none
• LeanCert.Engine.evalDual? e_2.erf ρ = match LeanCert.Engine.evalDual? e_2 ρ with | some d => some d.erf | none => none
• LeanCert.Engine.evalDual? e_2.sinh ρ = match LeanCert.Engine.evalDual? e_2 ρ with | some d => some d.sinh | none => none
• LeanCert.Engine.evalDual? e_2.cosh ρ = match LeanCert.Engine.evalDual? e_2 ρ with | some d => some d.cosh | none => none
• LeanCert.Engine.evalDual? e_2.tanh ρ = none
• LeanCert.Engine.evalDual? e_2.sqrt ρ = match LeanCert.Engine.evalDual? e_2 ρ with | some d => d.sqrt? | none => none
• LeanCert.Engine.evalDual? (LeanCert.Core.Expr.namedConst c) ρ = some (LeanCert.Engine.DualInterval.ofMathConst c)

noncomputable def LeanCert.Engine.evalDual?1 (e : Core.Expr) (I : Core.IntervalRat) : Option DualInterval

Single-variable version of evalDual?

Equations

• LeanCert.Engine.evalDual?1 e I = LeanCert.Engine.evalDual? e fun (x : ℕ) => LeanCert.Engine.DualInterval.varActive I

Single variable differentiation

def LeanCert.Engine.mkDualEnv (ρ : IntervalEnv) (idx : ℕ) : DualEnv

Create dual environment for differentiating with respect to variable idx

Equations

• LeanCert.Engine.mkDualEnv ρ idx i = if i = idx then LeanCert.Engine.DualInterval.varActive (ρ i) else LeanCert.Engine.DualInterval.varPassive (ρ i)

noncomputable def LeanCert.Engine.evalWithDeriv (e : Core.Expr) (ρ : IntervalEnv) (idx : ℕ) : DualInterval

Evaluate and differentiate with respect to variable idx

Equations

• LeanCert.Engine.evalWithDeriv e ρ idx = LeanCert.Internal.AD.evalUnchecked e (LeanCert.Engine.mkDualEnv ρ idx)

noncomputable def LeanCert.Engine.derivInterval (e : Core.Expr) (ρ : IntervalEnv) (idx : ℕ) : Core.IntervalRat

Get just the derivative interval

Equations

• LeanCert.Engine.derivInterval e ρ idx = (LeanCert.Engine.evalWithDeriv e ρ idx).der

noncomputable def LeanCert.Engine.evalWithDeriv1 (e : Core.Expr) (I : Core.IntervalRat) : DualInterval

Evaluate and differentiate a single-variable expression

Equations

• LeanCert.Engine.evalWithDeriv1 e I = LeanCert.Internal.AD.evalUnchecked e fun (x : ℕ) => LeanCert.Engine.DualInterval.varActive I