RSAPredict Proof Builder

Build compositional QInterval containment proofs (CProof), both generic interval combinators and RSA-specific proof builders for L0, S1, and L1.

structure Linglib.Tactics.RSAPredict.CProof : Type

Result of building a compositional QInterval containment proof. Each CProof carries the interval Expr, its containment proof, and ℚ bounds.

• iExpr : Lean.Expr
• proof : Lean.Expr
• lo : ℚ
• hi : ℚ

def Linglib.Tactics.RSAPredict.instInhabitedCProof.default : CProof

Equations

• Linglib.Tactics.RSAPredict.instInhabitedCProof.default = { iExpr := default, proof := default, lo := default, hi := default }

instance Linglib.Tactics.RSAPredict.instInhabitedCProof : Inhabited CProof

Equations

• Linglib.Tactics.RSAPredict.instInhabitedCProof = { default := Linglib.Tactics.RSAPredict.instInhabitedCProof.default }

instance Linglib.Tactics.RSAPredict.instInhabitedCProof_1 : Inhabited CProof

Equations

• Linglib.Tactics.RSAPredict.instInhabitedCProof_1 = { default := { iExpr := default, proof := default, lo := 0, hi := 0 } }

def Linglib.Tactics.RSAPredict.proveQPropND (type : Lean.Expr) : Lean.Elab.Tactic.TacticM Lean.Expr

Prove a ℚ proposition by native_decide.

Equations

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

def Linglib.Tactics.RSAPredict.buildExact (q : ℚ) : Lean.MetaM CProof

Build CProof for a concrete ℚ value. Uses special lemmas for 0 and 1 to avoid Nat.cast/OfNat mismatch.

Equations

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

def Linglib.Tactics.RSAPredict.buildCAdd (p1 p2 : CProof) : Lean.MetaM CProof

Build CProof for x + y.

Equations

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

def Linglib.Tactics.RSAPredict.buildChainAdd (proofs : Array CProof) : Lean.MetaM CProof

Build right-folded sum matching Finset.sum reduction via List.foldr. For elements [e₁, e₂, e₃], builds f(e₁) + (f(e₂) + (f(e₃) + 0)).

Equations

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

def Linglib.Tactics.RSAPredict.buildLeftAdd (proofs : Array CProof) : Lean.MetaM CProof

Build left-associated sum without trailing zero, matching explicit addition goals. For elements [p₁, p₂, p₃], builds ((p₁ + p₂) + p₃). For a single element, returns it directly (no addition node).

Equations

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

def Linglib.Tactics.RSAPredict.buildCMulNN (p1 p2 : CProof) : Lean.Elab.Tactic.TacticM CProof

Build CProof for x * y (nonneg intervals).

Equations

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

def Linglib.Tactics.RSAPredict.buildCMulGen (p1 p2 : CProof) : Lean.Elab.Tactic.TacticM CProof

Build CProof for x * y (general, handles negative factors via 4-corner method).

Equations

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

def Linglib.Tactics.RSAPredict.buildCMulSafe (p1 p2 : CProof) : Lean.Elab.Tactic.TacticM CProof

Build CProof for x * y, preferring nonneg if possible, falling back to general.

Equations

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

def Linglib.Tactics.RSAPredict.buildCNeg (p : CProof) : Lean.Elab.Tactic.TacticM CProof

Build CProof for -x using neg_containsReal.

Equations

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

def Linglib.Tactics.RSAPredict.buildCDivPos (num denom : CProof) : Lean.Elab.Tactic.TacticM CProof

Build CProof for x / y (nonneg numerator, positive denominator).

Equations

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

def Linglib.Tactics.RSAPredict.buildPolicyProof (scoreProof totalProof : CProof) : Lean.Elab.Tactic.TacticM CProof

Build CProof for policy: if totalScore = 0 then 0 else score / totalScore. Requires totalScore interval to have positive lo.

Equations

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

def Linglib.Tactics.RSAPredict.buildCExp (p : CProof) : Lean.Elab.Tactic.TacticM CProof

Build CProof for Real.exp(x). Uses expInterval_containsReal. Meta-level bounds use expPoint for ℚ approximation.

Equations

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

def Linglib.Tactics.RSAPredict.buildCLog (p : CProof) : Lean.Elab.Tactic.TacticM CProof

Build CProof for Real.log(x) where x > 0. Uses logInterval_containsReal.

Equations

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

structure Linglib.Tactics.RSAPredict.L0CacheCtx : Type

Context for lazy L0 policy caching. Contains a builder callback so we avoid forward-reference issues. The cache map is populated on first access.

• build : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Elab.Tactic.TacticM CProof

opaque Linglib.Tactics.RSAPredict.l0CacheCtxRef : IO.Ref (Option L0CacheCtx)

Global lazy L0 cache. When ctx is some, L0 policy expressions are intercepted in buildRealExprProof and built/cached on first encounter.

opaque Linglib.Tactics.RSAPredict.l0CacheMapRef : IO.Ref (Std.HashMap UInt64 CProof)

partial def Linglib.Tactics.RSAPredict.buildRealExprProof (e : Lean.Expr) : Lean.Elab.Tactic.TacticM CProof

Build CProof for an ℝ expression by recursively decomposing arithmetic structure. Handles fractions (like 1/3 : ℝ), exp, log, ite, and other expressions that don't reduce to ↑(q : ℚ) definitionally. Mirrors matchArithOp/extractRat and reifyToRExpr but outputs proof terms instead of ℚ values or RExpr.

At each node, the proof refers to the (possibly unfolded) sub-expressions. The kernel accepts these because unfolded expressions are definitionally equal to the originals.

partial def Linglib.Tactics.RSAPredict.buildRealExprProof.collectNatLits (e : Lean.Expr) : Array ℕ

def Linglib.Tactics.RSAPredict.buildLeaf (_q : ℚ) (realExpr : Lean.Expr) : Lean.Elab.Tactic.TacticM CProof

Build CProof for a concrete ℚ value matching a specific real expression. Pre-reduces the expression via whnf so that structural matching (getNat?, isAppOfMin) catches it immediately, avoiding redundant isDefEq calls on unreduced config field expressions.

Equations

• Linglib.Tactics.RSAPredict.buildLeaf _q realExpr = do let reduced ← liftM (Lean.Meta.whnf realExpr) Linglib.Tactics.RSAPredict.buildRealExprProof reduced

def Linglib.Tactics.RSAPredict.buildL0PolicyCProof (cfg l u : Lean.Expr) (allWElems : Array Lean.Expr) (wIdx : ℕ) : Lean.Elab.Tactic.TacticM CProof

Build CProof for (cfg.L0agent l).policy u w. Uses buildLeaf so each meaning proof mentions the actual cfg.meaning expression, allowing compositions to carry the correct real-valued type.

Equations

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

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

Check whether cfg.s1Score uses rpow (belief-based) or exp (action-based). Inspects the whnf of cfg.s1Score structurally — no kernel reduction needed beyond one config field unfold. Computed once per theorem and cached.

def Linglib.Tactics.RSAPredict.detectBeliefBased (cfg : Lean.Expr) : Lean.Elab.Tactic.TacticM Bool

Equations

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

def Linglib.Tactics.RSAPredict.buildS1ScoreCProof (cfg l w u : Lean.Expr) (allWElems : Array Lean.Expr) (αNat : ℕ) (isBeliefBased : Bool) : Lean.Elab.Tactic.TacticM CProof

Build CProof for (cfg.S1agent l).score w u. Fast path: belief-based scoring with standard s1Score = rpow(L0,α). Fallback: generic decomposition via buildRealExprProof (handles custom s1Score like QUD projection, and action-based exp/log scoring).

Equations

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

def Linglib.Tactics.RSAPredict.buildForallScoreZero (agent s : Lean.Expr) (allElems : Array Lean.Expr) (targetIdx : ℕ) (scoreProofs : Array CProof) : Lean.Elab.Tactic.TacticM Lean.Expr

Build ∀ a', a' ≠ target → agent.score s a' = 0 from individual zero CProofs. Uses the inductive type's casesOn recursor to case-split on a', providing the zero proof for each non-target constructor and absurd rfl h for the target constructor (contradiction).

Equations

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

@[reducible, inline]

abbrev Linglib.Tactics.RSAPredict.S1Cache : Type

S1 score CProof cache indexed by (lIdx, wIdx, uIdx).

Equations

• Linglib.Tactics.RSAPredict.S1Cache = Array (Array (Array Linglib.Tactics.RSAPredict.CProof))

def Linglib.Tactics.RSAPredict.buildAllS1ScoreCProofs (cfg : Lean.Expr) (allUElems allWElems allLElems : Array Lean.Expr) (αNat : ℕ) (isBeliefBased : Bool) (s1Bounds : Option (Array MetaBounds) := none) : Lean.Elab.Tactic.TacticM S1Cache

Build all S1 score CProofs once. Returns cache indexed [l][w][u]. When s1Bounds is provided (from the reify pass), entries known to be zero are given a trivial zero CProof if the kernel can verify score ≡ 0 definitionally. Otherwise (e.g., QUD-projection models where the reduction chain is too deep), full CProofs are built.

Equations

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

def Linglib.Tactics.RSAPredict.buildS1PolicyCProof (cfg l w : Lean.Expr) (allWElems allUElems allLElems : Array Lean.Expr) (uIdx αNat : ℕ) (isBeliefBased : Bool) (s1Cache : Option S1Cache := none) : Lean.Elab.Tactic.TacticM CProof

Build CProof for cfg.S1 l w u = (cfg.S1agent l).policy w u. Uses pre-built S1 score CProofs from cache if provided. Checks zero-score and self-cancellation BEFORE building the total sum, since both paths don't need it. Only builds the expensive buildChainAdd when the general division path is needed.

Equations

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

structure Linglib.Tactics.RSAPredict.LeafCache : Type

Pre-built leaf CProofs for worldPrior and latentPrior. Avoids redundant whnf + buildRealExprProof across phases.

• wpProofs : Array CProof
• lpProofs : Array CProof

def Linglib.Tactics.RSAPredict.buildLeafCache (cfg : Lean.Expr) (allWElems allLElems : Array Lean.Expr) (wpValues lpValues : Array ℚ) : Lean.Elab.Tactic.TacticM LeafCache

Build leaf CProofs for all worldPrior and latentPrior values.

Equations

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

def Linglib.Tactics.RSAPredict.buildL1ScoreCProof (cfg u w : Lean.Expr) (allUElems allWElems allLElems : Array Lean.Expr) (wpValues lpValues : Array ℚ) (αNat : ℕ) (isBeliefBased : Bool) (s1Cache : Option S1Cache := none) (leafCache : Option LeafCache := none) : Lean.Elab.Tactic.TacticM CProof

Build CProof for cfg.L1agent.score u w = worldPrior(w) * ∑ l, latentPrior(w,l) * S1(l,w,u).

Equations

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

def Linglib.Tactics.RSAPredict.buildAllL1ScoreCProofs (cfg u : Lean.Expr) (allUElems allWElems allLElems : Array Lean.Expr) (wpValues lpValues : Array ℚ) (αNat : ℕ) (isBeliefBased : Bool) (s1Cache : Option S1Cache := none) (leafCache : Option LeafCache := none) : Lean.Elab.Tactic.TacticM (Array CProof × CProof)

Build all L1 score CProofs for a given utterance u (one per world). Returns the array of CProofs and the totalScore CProof.

Equations

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

def Linglib.Tactics.RSAPredict.buildL1PolicyFromScores (cfg u w : Lean.Expr) (allWElems : Array Lean.Expr) (allScoreProofs : Array CProof) (totalProof : CProof) : Lean.Elab.Tactic.TacticM CProof

Build L1 policy CProof from pre-computed L1 score CProofs.

Equations

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

def Linglib.Tactics.RSAPredict.buildL1LatentScoreCProof (cfg u l : Lean.Expr) (allUElems allWElems allLElems : Array Lean.Expr) (wpValues lpValues : Array ℚ) (αNat : ℕ) (isBeliefBased : Bool) (s1Cache : Option S1Cache := none) : Lean.Elab.Tactic.TacticM CProof

Build CProof for (cfg.L1_latent_agent u).score l = Σ_w worldPrior(w) · latentPrior(w,l) · S1(l,w,u).

Equations

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