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).

Reify: Convert both sides of the comparison to RExpr AST + meta-level bounds. No congruence proof trees — the kernel handles definitional equality.
Check: native_decide on checkGtOptMemo/checkNotGtOpt (evalValid + separation).
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.

source

def Linglib.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.

Instances For

source

def Linglib.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.

Instances For

source

def Linglib.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.

Instances For

source

opaque Linglib.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.).

source

def Linglib.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_gt_of_score_gt, reducing the goal to a score comparison that skips the shared normalization constant.

Equations