Autograd proofs

autograd combines registered derivative rules and lifts scalar derivatives to elementwise tensor nodes. It constructs the existing NodeFDerivCorrect certificates; it does not introduce a second graph representation or certify an arbitrary runtime program by inspecting its name.

Use @[autograd] to register a proved rule for a new operation. Use autograd? to inspect the proof script. Nonsmooth operations still require their pointwise domain hypotheses. @[autograd simp] registers proved identities for rewriting inside expressions without changing the ordinary simp set. These rewrites retain their hypotheses and can be scoped locally.

For nested evaluation, the tactic combines higher-order Dual.jet rules and mathlib smoothness proofs, then lifts them through tensor coordinates and recorded graph nodes. These rules cover arbitrary finite order, tensor shape, and fixed coordinate reindexing. The tactic also assembles jet laws for ordered sums and products, matrix multiplication, and reverse accumulation. The smooth nonlinear rules include tanh and the mutually differentiating sinh/cosh pair. Local rules cover division, logarithms, and square roots away from zero, including compositions with the smooth activation rules. They require smoothness near the evaluation point, not everywhere. Tensor outputs, reductions, and matrix products use the same local rules. Congruence carries tensor identities through surrounding functions and retains membership hypotheses inside ordered folds. Interchange rules identify derivatives of a pullback with pullbacks of higher derivatives when the direction tuple and cotangent are fixed and the required smoothness is proved. The first-order adjoint certificate remains independent; general model lowering and checked IO require their own correctness connections.

def tacticAutograd : Lean.ParserDescr

Prove a scalar derivative or a registered autograd certificate, including its side conditions. Fails unless the whole goal is solved. Extend goal-directed rules with @[autograd], or register rewrites inside expressions with @[autograd simp].

def tacticAutograd? : Lean.ParserDescr

Prove a scalar derivative or a registered autograd certificate, including its side conditions. Fails unless the whole goal is solved. Extend goal-directed rules with @[autograd], or register rewrites inside expressions with @[autograd simp].