RSAPredict Helpers

Low-level expression utilities, MetaBounds interval arithmetic, and enum extraction used across the RSAPredict tactic submodules.

def Tactics.RSAPredict.getOfNat? (e : Lean.Expr) : Option ℕ

Extract a natural number from @OfNat.ofNat T n inst.

Equations

• Tactics.RSAPredict.getOfNat? e = do guard (e.isAppOfArity `OfNat.ofNat 3 = true) e.appFn!.appArg!.rawNatLit?

def Tactics.RSAPredict.getNatCast? (e : Lean.Expr) : Option ℕ

Extract a natural number from @Nat.cast T inst n.

Equations

• Tactics.RSAPredict.getNatCast? e = do guard (e.isAppOfArity `Nat.cast 3 = true) e.getAppArgs[2]!.rawNatLit?

def Tactics.RSAPredict.getNat? (e : Lean.Expr) : Option ℕ

Equations

• Tactics.RSAPredict.getNat? e = (e.rawNatLit? <|> Tactics.RSAPredict.getOfNat? e <|> Tactics.RSAPredict.getNatCast? e)

def Tactics.RSAPredict.isAppOfMin (e : Lean.Expr) (name : Lean.Name) (minArgs : ℕ) : Bool

Equations

• Tactics.RSAPredict.isAppOfMin e name minArgs = (e.getAppFn.isConstOf name && decide (e.getAppNumArgs ≥ minArgs))

def Tactics.RSAPredict.resolveNat? (e : Lean.Expr) : Lean.MetaM (Option ℕ)

Try to extract a natural number, unfolding/reducing as needed.

Equations

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

structure Tactics.RSAPredict.MetaBounds : Type

Meta-level interval bounds for early checks.

• lo : ℚ
• hi : ℚ

def Tactics.RSAPredict.instInhabitedMetaBounds.default : MetaBounds

Equations

• Tactics.RSAPredict.instInhabitedMetaBounds.default = { lo := default, hi := default }

@[implicit_reducible]

instance Tactics.RSAPredict.instInhabitedMetaBounds : Inhabited MetaBounds

Equations

• Tactics.RSAPredict.instInhabitedMetaBounds = { default := Tactics.RSAPredict.instInhabitedMetaBounds.default }

def Tactics.RSAPredict.metaEvalMul (a b : MetaBounds) : MetaBounds

Equations

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

def Tactics.RSAPredict.roundDownBin (q : ℚ) (bits : ℕ) : ℚ

Round a nonneg ℚ down to bits binary digits: floor(q · 2^bits) / 2^bits. The result has a power-of-2 denominator, preventing denominator blowup.

Equations

• Tactics.RSAPredict.roundDownBin q bits = ↑(q.num.toNat * 2 ^ bits / q.den) / ↑(2 ^ bits)

def Tactics.RSAPredict.roundUpBin (q : ℚ) (bits : ℕ) : ℚ

Round a nonneg ℚ up to bits binary digits: ceil(q · 2^bits) / 2^bits.

Equations

• Tactics.RSAPredict.roundUpBin q bits = ↑((q.num.toNat * 2 ^ bits + q.den - 1) / q.den) / ↑(2 ^ bits)

def Tactics.RSAPredict.roundBounds (b : MetaBounds) (bits : ℕ := 48) : MetaBounds

Round MetaBounds outward (lo down, hi up) to bits binary digits. Maintains soundness: the rounded interval contains the original. Assumes both bounds are nonneg (always true for RSA scores).

Equations

• Tactics.RSAPredict.roundBounds b bits = if (b.lo == b.hi) = true then b else { lo := Tactics.RSAPredict.roundDownBin b.lo bits, hi := Tactics.RSAPredict.roundUpBin b.hi bits }

def Tactics.RSAPredict.metaQIAdd (a b : MetaBounds) : MetaBounds

Equations

• Tactics.RSAPredict.metaQIAdd a b = { lo := a.lo + b.lo, hi := a.hi + b.hi }

def Tactics.RSAPredict.metaQISumMap (scores : Array MetaBounds) : MetaBounds

Equations

• Tactics.RSAPredict.metaQISumMap scores = Array.foldl Tactics.RSAPredict.metaQIAdd { lo := 0, hi := 0 } scores

def Tactics.RSAPredict.metaQIDivPosSafe (num denom : MetaBounds) : MetaBounds

Equations

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

def Tactics.RSAPredict.metaQINormalize (scores : Array MetaBounds) (targetIdx : ℕ) : MetaBounds

Equations

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

def Tactics.RSAPredict.metaL1Score (nL nW nU : ℕ) (s1Bounds : Array MetaBounds) (wpValues lpValues : Array ℚ) (uIdx wIdx : ℕ) : MetaBounds

Compute L1 unnormalized score at meta level using MetaBounds. L1(u,w) = worldPrior(w) · Σ_l latentPrior(w,l) · S1_policy(l,w,u) where S1_policy(l,w,u) = S1(l,w,u) / Σ_{u'} S1(l,w,u'). lpValues is indexed as lpValues[wIdx * nL + lIdx].

Equations

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

def Tactics.RSAPredict.metaL1LatentScore (nL nW nU : ℕ) (s1Bounds : Array MetaBounds) (wpValues lpValues : Array ℚ) (uIdx lIdx : ℕ) : MetaBounds

Compute latent inference score at meta level: latent_score(l) = Σ_w worldPrior(w) · latentPrior(w,l) · S1_policy(l,w,u) where S1_policy(l,w,u) = S1(l,w,u) / Σ_{u'} S1(l,w,u'). lpValues is indexed as lpValues[wIdx * nL + lIdx].

Equations

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

def Tactics.RSAPredict.metaL1Policy (nL nW nU : ℕ) (s1Bounds : Array MetaBounds) (wpValues lpValues : Array ℚ) (uIdx : ℕ) (allWIndices : Array ℕ) (targetWIdx : ℕ) : MetaBounds

Compute L1 policy bounds at meta level (score / total). Used for cross-utterance comparisons where denominators differ.

Equations

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

def Tactics.RSAPredict.metaS2Score (nL nW nU : ℕ) (s1Bounds : Array MetaBounds) (wpValues lpValues : Array ℚ) (allUIndices : Array ℕ) (targetUIdx wIdx : ℕ) : MetaBounds

Compute S2 policy bounds at meta level (cross-world comparison). S2(u|w) = L1(u,w) / Σ_{u'} L1(u',w), where L1 is the normalized posterior. S2agent.score(w,u) = cfg.L1(u,w) = L1agent.policy(u,w).

Equations

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

def Tactics.RSAPredict.findElemIdx (elems : Array Lean.Expr) (target : Lean.Expr) : Lean.MetaM ℕ

Find the index of target in elems by definitional equality.

Equations

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

def Tactics.RSAPredict.extractList (e : Lean.Expr) : Lean.MetaM (Array Lean.Expr)

Extract a concrete List from a Lean Expr, extracting cons cells.

Equations

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

partial def Tactics.RSAPredict.getFiniteElems (T : Lean.Expr) : Lean.MetaM (Lean.Expr × Array Lean.Expr)

Get all elements of a finite type as a List, represented as Lean Exprs. Returns (listExpr, elemExprs) where listExpr : Expr of type List T and elemExprs are the individual elements.

def Tactics.RSAPredict.mkRatExpr (q : ℚ) : Lean.MetaM Lean.Expr

Build a Lean Expr for a ℚ literal.

Equations

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

@[implemented_by _private.Linglib.Tactics.RSAPredict.Helpers.0.Tactics.RSAPredict.tryEvalBoolUnsafe]

opaque Tactics.RSAPredict.tryEvalBool (e : Lean.Expr) : Lean.MetaM (Option Bool)