RL Proof Tactics

This file defines a small set of proof-focused tactics/macros used across NN/Proofs/RL.

Design goals:

• Lightweight: no heavyweight automation, just convenience wrappers.
• Stable: avoid tactics that are fragile under small definitional changes.
• Local: the API is intentionally small; add new helpers only when repeated boilerplate has shown up in multiple RL proof files.

References:

• Lean 4 documentation (macros, tactics, simp): https://lean-lang.org/lean4/doc/

def Proofs.RL.simp_rl : Lean.ParserDescr

simp_rl is a simp-wrapper used across NN/Proofs/RL.

It unfolds the core one-step formulas by default:

• Spec.RL.discountedBackup
• Spec.RL.tdTarget
• Spec.RL.tdResidual

continueMask is intentionally not unfolded by default, since many proofs keep it symbolic and only unfold it at the point they need case-splits on done.

Usage:

simp_rl
simp_rl [myLemma, myOtherLemma]

def Proofs.RL.except_cases : Lean.ParserDescr

except_cases peels a successful Except do-chain by case-splitting an intermediate step.

This is useful in trust-boundary proofs (where checkers return Except String _):

• In the .ok branch, it gives you an equality h : e = .ok v and continues with payload v.
• In the .error branch, it closes the goal by contradiction using the hypothesis that the whole chain succeeded.

Example:

have hOk : (do _ ← f; g) = .ok x := ...
except_cases hf : f using hOk with v =>
  -- `v` is the `.ok` payload from `f`.
  ...