RSAPredict Reflection Bridge

Direct RExpr reification for all RSA comparison goals.

Design

The proof-free reifier builds RExpr AST nodes whose denote is definitionally equal to the original expression. The kernel verifies this via iota-reduction of denote (structural recursion, O(1) per node).

1. Reify: Convert both sides of the comparison to RExpr AST + meta-level bounds. No congruence proof trees — the kernel handles definitional equality.
2. Check: native_decide on checkGtOptMemo/checkNotGtOpt (evalValid + separation).
3. Assign: Directly assign gt_of_checkGtOptMemo lhsRExpr rhsRExpr hcheck — the kernel verifies denote(lhsRExpr) ≡ lhsExpr and denote(rhsRExpr) ≡ rhsExpr.

This eliminates the congruence proof tree (O(n) nodes → O(1) proof term) and the equality bridge (gt_of_eq_gt_eq), reducing both reification time and proof term size.

def Tactics.RSAPredict.unfoldToPolicy (e : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr × Lean.Expr))

Try to unfold an expression to RationalAction.policy ra s a.

Equations

• One or more equations did not get rendered due to their size.

def Tactics.RSAPredict.parseL1Policy (e : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr × Lean.Expr))

Extract RSA config and arguments from a policy expression. Returns (cfg, u, w) where the expression is cfg.L1 u w.

Equations

• One or more equations did not get rendered due to their size.

def Tactics.RSAPredict.parseS1Policy (e : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr))

Extract RSA config and arguments from a policy expression. Returns (cfg, l, w, u) where the expression is cfg.S1 l w u.

Equations

• One or more equations did not get rendered due to their size.

opaque Tactics.RSAPredict.persistentReifyCache : IO.Ref (Std.HashMap Lean.Expr (Lean.Expr × MetaBounds))

Module-scope reification cache shared across all rsa_predict invocations within a file. The first theorem pays the full reification cost; subsequent theorems for the same model get cache hits on shared sub-expressions (L0 policies, S1 scores, belief distributions, etc.).

Note on async elaboration. The cache is an IO.Ref, which only persists across theorems when elaboration is synchronous. lake build and the language server set Elab.async = true by default, which runs each theorem in an isolated async branch — the cache is empty at the start of every theorem. RSA-heavy files should add set_option Elab.async false at the file top to re-enable cache sharing (typical 2x speedup; see CHANGELOG 0.230.x). This is the same workaround Lean's own native_decide and #eval use internally (Meta/Native.lean, Meta/Eval.lean). EnvExtension is not a fix — its only consistent-read mode (.sync) blocks on prior async branches, giving equivalent serialization.

def Tactics.RSAPredict.tryDirectRExprCompare (goal : Lean.MVarId) (lhsExpr rhsExpr : Lean.Expr) : Lean.Elab.Tactic.TacticM Bool

Direct RExpr reification for lhs > rhs goals. Runs native_decide on tree-based checkGtOptMemo (sorry-free soundness).

When both sides are policy ra s a₁/a₂ with the same ra and s, applies denominator cancellation first via policy_lt_of_score_lt, reducing the goal to a score comparison that skips the shared normalization constant.

Equations

• One or more equations did not get rendered due to their size.

def Tactics.RSAPredict.tryDirectRExprNotGt (goal : Lean.MVarId) (lhsExpr rhsExpr : Lean.Expr) : Lean.Elab.Tactic.TacticM Bool

Direct RExpr reification for not (lhs > rhs) goals. Assigns proofs directly — the kernel verifies denote ≡ original.

Equations

• One or more equations did not get rendered due to their size.

def Tactics.RSAPredict.tryDirectRExprEq (goal : Lean.MVarId) (lhsExpr rhsExpr : Lean.Expr) : Lean.Elab.Tactic.TacticM Bool

Direct RExpr reification for lhs = rhs goals. Tries structural equality first (same RExpr), then exact ℚ evaluation.

Equations

• One or more equations did not get rendered due to their size.