Automatic Differentiation - Correctness Theorems

This file proves the correctness of forward-mode automatic differentiation for supported expressions (ExprSupported).

Main theorems

• evalDual_val_correct - Value component is correct
• evalDual_der_correct - Derivative component is correct
• evalFunc1_differentiable - Supported expressions are differentiable
• deriv_mem_dualDer - Key theorem: computed derivative contains true derivative
• evalDual_der_correct_idx - n-variable derivative correctness
• evalWithDeriv1_correct - Single-variable correctness

Design notes

All theorems in this file are FULLY PROVED with no sorry or axioms. The correctness relies on the chain rule for each supported operation.

Correctness

theorem LeanCert.Engine.evalDual_val_correct (e : Core.Expr) (hsupp : ExprSupported e) (ρ_real : ℕ → ℝ) (ρ_dual : DualEnv) (hρ : ∀ (i : ℕ), ρ_real i ∈ (ρ_dual i).val) : Core.Expr.eval ρ_real e ∈ (evalDual e ρ_dual).val

The value component is correct for supported expressions.

This theorem is FULLY PROVED (no sorry, no axioms) for supported expressions. The hsupp hypothesis ensures we only consider expressions in the verified subset.

Single-variable evaluation for derivative proofs

@[reducible, inline]

noncomputable abbrev LeanCert.Engine.evalFunc1 (e : Core.Expr) : ℝ → ℝ

The function t ↦ Expr.eval (fun _ => t) e for single-variable expressions

Equations

• LeanCert.Engine.evalFunc1 e t = LeanCert.Core.Expr.eval (fun (x : ℕ) => t) e

Differentiability of supported expressions

theorem LeanCert.Engine.evalFunc1_differentiable (e : Core.Expr) (hsupp : ExprSupported e) : Differentiable ℝ (evalFunc1 e)

Supported expressions are differentiable as single-variable functions. This theorem shows that for any supported expression, the function evalFunc1 e is differentiable.

FULLY PROVED - no sorry, no axioms.

Core derivative correctness micro-lemmas

theorem LeanCert.Engine.cos_mem_cosInterval_of_any (y : ℝ) (I : Core.IntervalRat) : Real.cos y ∈ cosInterval I

Real.cos y is always in cosInterval I (which is [-1, 1]). This micro-lemma encapsulates the fact that cosInterval uses the global bound.

theorem LeanCert.Engine.sin_mem_sinInterval_of_any (y : ℝ) (I : Core.IntervalRat) : Real.sin y ∈ sinInterval I

Real.sin y is always in sinInterval I (which is [-1, 1]). This micro-lemma encapsulates the fact that sinInterval uses the global bound.

theorem LeanCert.Engine.neg_sin_mem_neg_sinInterval (y : ℝ) (I : Core.IntervalRat) : -Real.sin y ∈ (sinInterval I).neg

-Real.sin y is always in IntervalRat.neg (sinInterval I). This combines the sin global bound with negation for the cos derivative rule.

theorem LeanCert.Engine.updateVar_mem_mkDualEnv_val (ρ_real : ℕ → ℝ) (ρ_int : IntervalEnv) (idx : ℕ) (x : ℝ) (hx : x ∈ ρ_int idx) (hρ : ∀ (i : ℕ), ρ_real i ∈ ρ_int i) (i : ℕ) : (ρ_real[idx ↦ x]) i ∈ (mkDualEnv ρ_int idx i).val

The key lemma for n-variable AD: updateVar ρ_real idx x respects mkDualEnv ρ_int idx. This encapsulates the repeated proof that appears in mul/exp cases.

evalFunc1 unfolding lemmas

theorem LeanCert.Engine.evalFunc1_add (e₁ e₂ : Core.Expr) : evalFunc1 (e₁.add e₂) = fun (t : ℝ) => evalFunc1 e₁ t + evalFunc1 e₂ t

Helper lemma: evalFunc1 for addition unfolds correctly

theorem LeanCert.Engine.evalFunc1_add_pi (e₁ e₂ : Core.Expr) : evalFunc1 (e₁.add e₂) = evalFunc1 e₁ + evalFunc1 e₂

Helper lemma: evalFunc1 for addition in Pi form

theorem LeanCert.Engine.evalFunc1_mul (e₁ e₂ : Core.Expr) : evalFunc1 (e₁.mul e₂) = fun (t : ℝ) => evalFunc1 e₁ t * evalFunc1 e₂ t

Helper lemma: evalFunc1 for multiplication unfolds correctly

theorem LeanCert.Engine.evalFunc1_mul_pi (e₁ e₂ : Core.Expr) : evalFunc1 (e₁.mul e₂) = evalFunc1 e₁ * evalFunc1 e₂

Helper lemma: evalFunc1 for multiplication in Pi form

theorem LeanCert.Engine.evalFunc1_neg (e : Core.Expr) : evalFunc1 e.neg = fun (t : ℝ) => -evalFunc1 e t

Helper lemma: evalFunc1 for negation unfolds correctly

theorem LeanCert.Engine.evalFunc1_neg_pi (e : Core.Expr) : evalFunc1 e.neg = -evalFunc1 e

Helper lemma: evalFunc1 for negation in Pi form

theorem LeanCert.Engine.evalFunc1_sin (e : Core.Expr) : evalFunc1 e.sin = fun (t : ℝ) => Real.sin (evalFunc1 e t)

Helper lemma: evalFunc1 for sin unfolds correctly

theorem LeanCert.Engine.evalFunc1_cos (e : Core.Expr) : evalFunc1 e.cos = fun (t : ℝ) => Real.cos (evalFunc1 e t)

Helper lemma: evalFunc1 for cos unfolds correctly

theorem LeanCert.Engine.evalFunc1_exp (e : Core.Expr) : evalFunc1 e.exp = fun (t : ℝ) => Real.exp (evalFunc1 e t)

Helper lemma: evalFunc1 for exp unfolds correctly

theorem LeanCert.Engine.evalFunc1_log (e : Core.Expr) : evalFunc1 e.log = fun (t : ℝ) => Real.log (evalFunc1 e t)

Helper lemma: evalFunc1 for log unfolds correctly

theorem LeanCert.Engine.evalFunc1_atan (e : Core.Expr) : evalFunc1 e.atan = fun (t : ℝ) => Real.arctan (evalFunc1 e t)

Helper lemma: evalFunc1 for atan unfolds correctly

theorem LeanCert.Engine.evalFunc1_arsinh (e : Core.Expr) : evalFunc1 e.arsinh = fun (t : ℝ) => Real.arsinh (evalFunc1 e t)

Helper lemma: evalFunc1 for arsinh unfolds correctly

theorem LeanCert.Engine.evalFunc1_atanh (e : Core.Expr) : evalFunc1 e.atanh = fun (t : ℝ) => Core.Real.atanh (evalFunc1 e t)

Helper lemma: evalFunc1 for atanh unfolds correctly

theorem LeanCert.Engine.evalFunc1_sinc (e : Core.Expr) : evalFunc1 e.sinc = fun (t : ℝ) => Real.sinc (evalFunc1 e t)

Helper lemma: evalFunc1 for sinc unfolds correctly

theorem LeanCert.Engine.evalFunc1_erf (e : Core.Expr) : evalFunc1 e.erf = fun (t : ℝ) => Core.Real.erf (evalFunc1 e t)

Helper lemma: evalFunc1 for erf unfolds correctly

theorem LeanCert.Engine.evalFunc1_sqrt (e : Core.Expr) : evalFunc1 e.sqrt = fun (t : ℝ) => √(evalFunc1 e t)

Helper lemma: evalFunc1 for sqrt unfolds correctly

@[simp]

theorem LeanCert.Engine.evalFunc1_const (q : ℚ) : evalFunc1 (Core.Expr.const q) = fun (x : ℝ) => ↑q

Helper lemma: evalFunc1 for const

@[simp]

theorem LeanCert.Engine.evalFunc1_var (i : ℕ) : evalFunc1 (Core.Expr.var i) = id

Helper lemma: evalFunc1 for var

@[simp]

theorem LeanCert.Engine.evalFunc1_pi : evalFunc1 Core.Expr.pi = fun (x : ℝ) => Real.pi

Helper lemma: evalFunc1 for pi (constant function)

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

Helper: the dual environment evaluation gives correct derivative. This connects the interval-based AD to actual calculus derivatives.

FULLY PROVED - no sorry, no axioms.

theorem LeanCert.Engine.evalDual_der_correct (e : Core.Expr) (hsupp : ExprSupported e) (I : Core.IntervalRat) (x : ℝ) (hx : x ∈ I) : deriv (fun (t : ℝ) => Core.Expr.eval (fun (x : ℕ) => t) e) x ∈ (evalDual e fun (x : ℕ) => DualInterval.varActive I).der

The derivative component of dual interval evaluation is correct. For a supported expression evaluated at a point x in the interval I, the derivative of the expression (as a function of x) lies in the computed derivative interval.

This is the fundamental correctness theorem for forward-mode AD: the derivative bounds computed by interval arithmetic contain the true derivative at every point in the domain.

FULLY PROVED - no sorry, no axioms.

Generalized n-variable derivative correctness

theorem LeanCert.Engine.evalAlong_differentiable (e : Core.Expr) (hsupp : ExprSupported e) (ρ : ℕ → ℝ) (idx : ℕ) : Differentiable ℝ (e.evalAlong ρ idx)

Helper: evalAlong is differentiable for supported expressions

theorem LeanCert.Engine.evalDual_der_correct_idx (e : Core.Expr) (hsupp : ExprSupported e) (ρ_real : ℕ → ℝ) (ρ_int : IntervalEnv) (idx : ℕ) (hρ : ∀ (i : ℕ), ρ_real i ∈ ρ_int i) (x : ℝ) (hx : x ∈ ρ_int idx) : deriv (e.evalAlong ρ_real idx) x ∈ (evalDual e (mkDualEnv ρ_int idx)).der

The derivative of evalAlong with respect to coordinate idx lies in the computed derivative interval from mkDualEnv.

This is the fundamental n-variable derivative correctness theorem. It shows that for any expression, if we differentiate along coordinate idx while holding all other coordinates fixed according to ρ, the derivative at any point x in the interval ρ_int idx lies in the computed interval.

FULLY PROVED - no sorry, no axioms.

theorem LeanCert.Engine.derivInterval_correct_idx (e : Core.Expr) (hsupp : ExprSupported e) (ρ_real : ℕ → ℝ) (ρ_int : IntervalEnv) (idx : ℕ) (hρ : ∀ (i : ℕ), ρ_real i ∈ ρ_int i) (x : ℝ) (hx : x ∈ ρ_int idx) : deriv (e.evalAlong ρ_real idx) x ∈ derivInterval e ρ_int idx

Convenience theorem: derivInterval correctness for n-variable expressions. The derivative of evalAlong e ρ idx at any point x in the interval lies in derivInterval e ρ_int idx.

Single-variable expressions

inductive LeanCert.Engine.UsesOnlyVar0 : Core.Expr → Prop

Predicate: expression only uses variable index 0. This is useful for proving that different environments give the same result when they agree at index 0.

• const (q : ℚ) : UsesOnlyVar0 (Core.Expr.const q)
• var0 : UsesOnlyVar0 (Core.Expr.var 0)
• add (e₁ e₂ : Core.Expr) (h₁ : UsesOnlyVar0 e₁) (h₂ : UsesOnlyVar0 e₂) : UsesOnlyVar0 (e₁.add e₂)
• mul (e₁ e₂ : Core.Expr) (h₁ : UsesOnlyVar0 e₁) (h₂ : UsesOnlyVar0 e₂) : UsesOnlyVar0 (e₁.mul e₂)
• neg (e : Core.Expr) (h : UsesOnlyVar0 e) : UsesOnlyVar0 e.neg
• sin (e : Core.Expr) (h : UsesOnlyVar0 e) : UsesOnlyVar0 e.sin
• cos (e : Core.Expr) (h : UsesOnlyVar0 e) : UsesOnlyVar0 e.cos
• exp (e : Core.Expr) (h : UsesOnlyVar0 e) : UsesOnlyVar0 e.exp
• atan (e : Core.Expr) (h : UsesOnlyVar0 e) : UsesOnlyVar0 e.atan
• arsinh (e : Core.Expr) (h : UsesOnlyVar0 e) : UsesOnlyVar0 e.arsinh

theorem LeanCert.Engine.evalDual_congr_at_0 (e : Core.Expr) (h : UsesOnlyVar0 e) (ρ₁ ρ₂ : DualEnv) (heq : ρ₁ 0 = ρ₂ 0) : evalDual e ρ₁ = evalDual e ρ₂

For expressions using only var 0, evalDual agrees for environments that match at 0

theorem LeanCert.Engine.mkDualEnv_at_0 (I : Core.IntervalRat) : mkDualEnv (fun (x : ℕ) => I) 0 0 = DualInterval.varActive I

mkDualEnv at index 0 equals varActive at 0

theorem LeanCert.Engine.derivInterval_eq_evalWithDeriv1_of_UsesOnlyVar0 (e : Core.Expr) (h : UsesOnlyVar0 e) (I : Core.IntervalRat) : derivInterval e (fun (x : ℕ) => I) 0 = (evalWithDeriv1 e I).der

For expressions using only var 0, derivInterval equals evalWithDeriv1

theorem LeanCert.Engine.evalWithDeriv1_correct (e : Core.Expr) (hsupp : ExprSupported e) (I : Core.IntervalRat) (x : ℝ) (hx : x ∈ I) : Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ (evalWithDeriv1 e I).val ∧ deriv (fun (t : ℝ) => Core.Expr.eval (fun (x : ℕ) => t) e) x ∈ (evalWithDeriv1 e I).der

Correctness of single-variable derivative bounds