RSAPredict Reifier

Convert Expr : ℝ to MetaBounds via memoized recursive reification, and extract ℚ values from ℝ expressions.

def Linglib.Tactics.RSAPredict.evalLogPoint (q : ℚ) : ℚ × ℚ

Equations

• Linglib.Tactics.RSAPredict.evalLogPoint q = if h : 0 < q then have I := Linglib.Interval.logPoint q h; (I.lo, I.hi) else (0, 0)

def Linglib.Tactics.RSAPredict.fastLogBounds (q : ℚ) : ℚ × ℚ

Fast meta-level log bounds using bit-length. O(1), no recursion. For q > 0, returns (lo, hi) with lo ≤ ln(q) ≤ hi. Uses ln(2) ∈ [693/1000, 694/1000] and Nat.log 2 for floor-log₂. Much less precise than evalLogPoint but avoids the deep recursion in logBisectCore that overflows the interpreter stack on large models.

Equations

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

def Linglib.Tactics.RSAPredict.safeLogBounds (q : ℚ) : ℚ × ℚ

Overflow-safe log bounds. Uses precise evalLogPoint for small rationals (≤ 200 bits). For large rationals, coarsens to 64-bit precision first, preserving soundness: truncDown(q) ≤ q → log(truncDown) ≤ log(q), and truncUp(q) ≥ q → log(truncUp) ≥ log(q).

Equations

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

partial def Linglib.Tactics.RSAPredict.findEmbeddedNat (e : Lean.Expr) (depth : ℕ := 15) : Option ℕ

Scan an expression for an embedded raw natural number literal. After whnf reduces n : ℝ to its Cauchy sequence form, the natural number is typically buried inside @Nat.cast ℚ _ n or similar. This scans the expression tree (limited depth) for the first raw nat literal.

def Linglib.Tactics.RSAPredict.extractIntExpr (e : Lean.Expr) : Lean.MetaM (Option ℤ)

Extract a ℤ from an expression in constructor form (Int.ofNat n or Int.negSucc n).

Equations

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

partial def Linglib.Tactics.RSAPredict.extractRatQ (e : Lean.Expr) : Lean.MetaM (Option ℚ)

Try to extract ℚ from a Rat-typed expression that may involve opaque arithmetic operations (Rat.mul, Rat.inv, etc.). These are @[extern] in Lean 4 and don't reduce under whnf/reduce, so we recursively decompose arithmetic operators and evaluate at the meta level.

Handles: Rat.mul, Rat.inv, Rat.add, Rat.sub, Rat.neg, Rat.div, Rat.ofScientific, OfNat.ofNat, Rat.mk' constructor, and Rat.num/Rat.den projections.

def Linglib.Tactics.RSAPredict.extractRatFromCauchy (e : Lean.Expr) : Lean.MetaM (Option (ℚ × Lean.Expr))

Extract ℚ from a Real.ofCauchy expression by evaluating the Cauchy sequence at index 0 and reading the resulting ℚ literal.

Returns `(ℚ value, original ℚ Expr)`. The ℚ value is used for bounds; the
original Expr is used in `RExpr.ratCast` so that `denote` produces an expression
definitionally equal to the goal. This is critical because `Rat.mul`/`Rat.inv`
are `@[extern]` and opaque to the kernel — using `mkRatExpr` would produce a
normalized form (e.g., `19/20`) that the kernel can't equate with the original
(`Rat.mul 95 (Rat.inv 100)`).

CauSeq ℚ abs is a Subtype { val : ℕ → ℚ // IsCauSeq abs val }, so we project

.val (field 0 of Subtype), apply to 0, and whnf-reduce to get a concrete Rat constructor (Rat.mk num den proof₁ proof₂). Then project.num and.den to extract the ℚ value.

This handles fractions (2/3, 1/3, etc.) that findEmbeddedNat cannot,
since findEmbeddedNat only scans for the first raw nat literal. 

Equations

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

def Linglib.Tactics.RSAPredict.maxDepth : ℕ

Equations

• Linglib.Tactics.RSAPredict.maxDepth = 500

@[reducible, inline]

abbrev Linglib.Tactics.RSAPredict.ReifyCache : Type

Memoization cache for reifyToRExpr, keyed on Expr (structural equality). Stores (rexprExpr, bounds).

Using Expr as key (not UInt64 hash) ensures collision safety: two expressions with the same hash but different structure are correctly distinguished by HashMap's BEq Expr check. Without this, the preseed path could populate cache entries that collide with organically-reached sub-expressions, causing denote(rexpr) ≢ e kernel failures.

Equations

• Linglib.Tactics.RSAPredict.ReifyCache = IO.Ref (Std.HashMap Lean.Expr (Lean.Expr × Linglib.Tactics.RSAPredict.MetaBounds))

opaque Linglib.Tactics.RSAPredict.persistentFilterCache : IO.Ref (Std.HashMap UInt64 (Array Lean.Expr))

Module-scope filter result cache for Finset.filter evaluations. For predicates of the form fun x => f(x) = c (constant-RHS equality), caches which elements pass the filter, keyed by (hash f, hash reduced_c). This deduplicates filter evaluations for qudProject equivalence classes: worlds with project(w₁, q) = project(w₂, q) share the same filter result, avoiding redundant reduce calls (20 per filter × ~300 duplicate filters).

partial def Linglib.Tactics.RSAPredict.reifyToRExpr (cache : ReifyCache) (e : Lean.Expr) (depth : ℕ) : Lean.MetaM (Lean.Expr × MetaBounds)

Proof-free RExpr reifier for rsa_predict. Produces (rexprExpr, bounds). The kernel verifies denote(rexprExpr) ≡ e by iota-reducing denote, eliminating the need for congruence proof trees.

Transparent steps (unfoldDefinition?, whnf, headBeta, let-substitution) produce definitionally equal forms — the reified RExpr from the recursive call works unchanged because denote(rexpr) ≡ e' ≡ e.

Structural steps (pattern-matching on HAdd, Real.exp, ite, etc.) build RExpr nodes whose denote is definitionally equal to the original expression.

Uses a hash-keyed cache to avoid redundant reification of shared subexpressions.

partial def Linglib.Tactics.RSAPredict.extractRat (e : Lean.Expr) : Lean.MetaM ℚ

Try to extract a ℚ literal from an ℝ expression. Uses incremental unfolding to avoid whnf over-reducing operators.

def Linglib.Tactics.RSAPredict.reifyS1Scores (cfg : Lean.Expr) : Lean.MetaM (Lean.Expr × Lean.Expr × Lean.Expr × Array Lean.Expr × Array Lean.Expr × Array Lean.Expr × Array MetaBounds × Array ℚ × Array ℚ)

Shared infrastructure: extract config info, reify all S1 scores. Returns (U, W, L types, element arrays, s1Bounds, wpValues, lpValues).

Equations

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