RSAPredict Auto-Detection (Tier 2)

Structural auto-detection of S1 score patterns from raw RSAConfig.

When cfg is NOT built via RSAConfigData.toRSAConfig (Tier 1 fails), this module classifies the s1Score lambda into a known S1ScoreSpec variant by pattern-matching on the normalized AST, then builds an RSAConfigData whose .toRSAConfig is definitionally equal to the user's config.

Pipeline

1. Normalize: Unfold cfg.s1Score, whnf to expose the lambda body.
2. Detect: Pattern-match outermost structure (rpow, ite, exp) to classify.
3. Extract: Evaluate meaning/priors/cost pointwise over finite types → ℚ arrays.
4. Build: Construct an RSAConfigData Expr with ite-chain functions + sorryAx proofs.
5. Bridge: native_decide on checkL1ScoreGt d..., then isDefEq to the goal.

If any step fails, returns false — CProof (Tier 3) handles it.

inductive Linglib.Tactics.RSAPredict.DetectedPattern : Type

Detected S1 score pattern. Each variant corresponds to an S1ScoreSpec constructor. QUD projection is handled orthogonally via RSAConfigData.qudProject.

• beliefBased : DetectedPattern
• beliefAction : DetectedPattern
• weightedBeliefAction : DetectedPattern
• actionBased : DetectedPattern
• beliefWeighted : DetectedPattern
• combinedUtility : DetectedPattern

partial def Linglib.Tactics.RSAPredict.containsConstName (name : Lean.Name) : Lean.Expr → Bool

Walk an expression tree checking if it contains a specific constant name.

def Linglib.Tactics.RSAPredict.detectScorePattern (cfg : Lean.Expr) : Lean.MetaM (Option DetectedPattern)

Detect the S1ScoreSpec variant by inspecting the reduced s1Score expression.

Strategy: reduce cfg.s1Score to whnf and look for signature constants:

• Real.rpow → beliefBased (QUD projection is orthogonal, via qudProject)
• Real.exp + Real.log → beliefAction (filter from QUD is handled separately)
• Real.exp without Real.log → actionBased
• Finset.sum inside Real.exp argument (weighted sum) → beliefWeighted

Equations

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

def Linglib.Tactics.RSAPredict.extractMeaningValues (cfg : Lean.Expr) (allLElems allUElems allWElems : Array Lean.Expr) : Lean.MetaM (Option (Array ℚ))

Extract meaning values: meaning(l, u, w) as ℚ for all (l,u,w) triples. Returns array indexed as [lIdx * nU * nW + uIdx * nW + wIdx].

Equations

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

def Linglib.Tactics.RSAPredict.extractWorldPriorValues (cfg : Lean.Expr) (allWElems : Array Lean.Expr) : Lean.MetaM (Option (Array ℚ))

Extract world prior values as ℚ.

Equations

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

def Linglib.Tactics.RSAPredict.extractLatentPriorValues (cfg : Lean.Expr) (allWElems allLElems : Array Lean.Expr) : Lean.MetaM (Option (Array ℚ))

Extract latent prior values as ℚ. Indexed as [wIdx * nL + lIdx].

Equations

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

def Linglib.Tactics.RSAPredict.peelS1ScoreBody (cfg : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Array Lean.FVarId))

Peel 5 lambdas from a reduced s1Score expression to expose the body. Returns (body, fvars) where fvars = [l0, α, l, w, u].

Equations

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

def Linglib.Tactics.RSAPredict.extractBeliefAndQuality (cfg : Lean.Expr) (allLElems allUElems allWElems : Array Lean.Expr) : Lean.MetaM (Option (Array ℚ × Array Bool))

Extract belief and quality values from a beliefWeighted s1Score. The expected pattern is: if quality(l, u) then exp(α * Σ_s belief(l,s) * log(l0 u s)) else 0 Also handles the KL divergence form where the sum body includes - Σ_s belief(l,s) * log(belief(l,s)) (constant w.r.t. u, so stripped).

Uses withLocalDecl for lambda peeling so fvars are properly registered in the local context (required for whnf/isDefEq to work).

Returns (beliefVals, qualityVals) where:

• beliefVals is indexed as [lIdx * nW + wIdx]
• qualityVals is indexed as [lIdx * nU + uIdx]

Equations

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

partial def Linglib.Tactics.RSAPredict.findCostSubExpr (e : Lean.Expr) (wFvar uFvar : Lean.FVarId) : Option Lean.Expr

Find a sub-expression that looks like a cost term:

• Appears as the RHS of a subtraction (... - cost)
• Does NOT mention wFvar (cost depends on utterance, not world)
• May or may not mention uFvar (constant cost like 0 is valid)

def Linglib.Tactics.RSAPredict.extractCostFromScore (cfg _U _W _L : Lean.Expr) (allUElems _allWElems _allLElems : Array Lean.Expr) (_pattern : DetectedPattern) : Lean.MetaM (Option (Array ℚ))

Extract cost values by structurally finding the cost sub-expression in the s1Score body. For beliefAction: s1Score l0 α l w u = if l0(u,w) = 0 then 0 else exp(α*(log(l0(u,w)) - cost(u))) For actionBased: s1Score l0 α l w u = exp(α*(l0(u,w) - cost(u)))

Uses withLocalDecl for lambda peeling (matching extractBeliefAndQuality) so that fvars have proper types in the local context. This ensures whnf can fully reduce match expressions in the body (e.g., beliefGoalScore/ actionGoalScore pattern matches). Without registered fvars, the match doesn't evaluate and findCostSubExpr fails to find the subtraction.

Equations

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

def Linglib.Tactics.RSAPredict.buildUnaryQFn (T : Lean.Expr) (elems : Array Lean.Expr) (values : Array ℚ) : Lean.MetaM Lean.Expr

Build fun (x : T) => if x = e₁ then v₁ else if x = e₂ then v₂ else... else vₙ

Equations

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

def Linglib.Tactics.RSAPredict.buildBinaryQFn (T₁ T₂ : Lean.Expr) (elems₁ elems₂ : Array Lean.Expr) (values : Array ℚ) : Lean.MetaM Lean.Expr

Build fun (x₁ : T₁) (x₂ : T₂) => <ite chain>. values indexed as [i * n₂ + j].

Equations

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

def Linglib.Tactics.RSAPredict.buildBinaryBoolFn (T₁ T₂ : Lean.Expr) (elems₁ elems₂ : Array Lean.Expr) (values : Array Bool) : Lean.MetaM Lean.Expr

Build fun (x₁ : T₁) (x₂ : T₂) => <ite chain> returning Bool. values indexed as [i * n₂ + j].

Equations

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

def Linglib.Tactics.RSAPredict.buildTernaryQFn (L U W : Lean.Expr) (lElems uElems wElems : Array Lean.Expr) (values : Array ℚ) : Lean.MetaM Lean.Expr

Build fun (l : L) (u : U) (w : W) => <ite chain>. values indexed as [li * nU * nW + ui * nW + wi].

Equations

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

def Linglib.Tactics.RSAPredict.mkSorryProof (ty : Lean.Expr) : Lean.Expr

Build a sorryAx proof of type ty : Prop.

Equations

• Linglib.Tactics.RSAPredict.mkSorryProof ty = Lean.mkApp2 (Lean.mkConst `sorryAx [Lean.Level.zero]) ty (Lean.mkConst `Bool.true)

def Linglib.Tactics.RSAPredict.mkMeaningNonnegProof (L U W meaningFn : Lean.Expr) : Lean.MetaM Lean.Expr

Build ∀ (l : L) (u : U) (w : W), 0 ≤ meaningFn l u w and its sorry proof.

Equations

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

def Linglib.Tactics.RSAPredict.mkAlphaPosProof (αLit : Lean.Expr) : Lean.MetaM Lean.Expr

Build 0 < α and its sorry proof (α : ℚ).

Equations

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

def Linglib.Tactics.RSAPredict.mkWpNonnegProof (W wpFn : Lean.Expr) : Lean.MetaM Lean.Expr

Build ∀ (w : W), 0 ≤ wpFn w and its sorry proof.

Equations

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

def Linglib.Tactics.RSAPredict.mkLpNonnegProof (W L lpFn : Lean.Expr) : Lean.MetaM Lean.Expr

Build ∀ (w : W) (l : L), 0 ≤ lpFn w l and its sorry proof.

Equations

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

def Linglib.Tactics.RSAPredict.buildConfigData (U W L : Lean.Expr) (allUElems allWElems allLElems : Array Lean.Expr) (meaningVals wpVals lpVals : Array ℚ) (αNat : ℕ) (pattern : DetectedPattern) (costVals beliefVals : Option (Array ℚ) := none) (qualityVals : Option (Array Bool) := none) (infWeightVal : Option ℚ := none) (bonusVals : Option (Array ℚ) := none) : Lean.MetaM (Option Lean.Expr)

Build an RSAConfigData Expr from detected pattern and extracted ℚ values.

The result d has the property that d.toRSAConfig is definitionally equal to the user's cfg (verified by isDefEq at the bridge step). Proof obligations are closed with sorryAx (erased at runtime, so native_decide works).

Equations

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

def Linglib.Tactics.RSAPredict.tryAutoDetectL1Compare (goal : Lean.MVarId) (cfg u w₁ w₂ : Lean.Expr) : Lean.Elab.Tactic.TacticM Bool

Full Tier 2 pipeline for L1 comparison: detect → extract → build → native_decide → bridge.

Returns true if successful, false to fall back to CProof (Tier 3).

Equations

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

def Linglib.Tactics.RSAPredict.tryAutoDetectL1NotGt (goal : Lean.MVarId) (cfg u w₁ w₂ : Lean.Expr) : Lean.Elab.Tactic.TacticM Bool

Tier 2 pipeline for ¬(L1 gt).

Equations

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

def Linglib.Tactics.RSAPredict.tryAutoDetectS1Compare (goal : Lean.MVarId) (cfg l w u₁ u₂ : Lean.Expr) : Lean.Elab.Tactic.TacticM Bool

Tier 2 pipeline for S1 comparison.

Equations

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

def Linglib.Tactics.RSAPredict.tryAutoDetectS1NotGt (goal : Lean.MVarId) (cfg l w u₁ u₂ : Lean.Expr) : Lean.Elab.Tactic.TacticM Bool

Tier 2 pipeline for ¬(S1 gt).

Equations

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

def Linglib.Tactics.RSAPredict.tryAutoDetectL1ScoreGt (goal : Lean.MVarId) (cfg u₁ w₁ u₂ w₂ : Lean.Expr) : Lean.Elab.Tactic.TacticM Bool

Tier 2 pipeline for L1 score gt (cross-utterance).

Equations

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