Allow function inlining in quantifiers

[thanhnguyen-aws]

Problem

LExpr.eval does not reduce under .abs or .quant binders — these are treated as canonical values with no congruence rule. Consequently, calls to inline factory functions inside quantifier or lambda bodies are never expanded.

Solution

Introduce LExpr.expandInlineCalls, a fuel-bounded structural pre-pass that:

1. Walks the entire expression tree, including under binders.
2. At each fully-applied call to an inline factory function with a body, substitutes arguments into the body (using substFvarsLifting for correct de Bruijn lifting).
3. Recurses into the substituted result to handle nested inline calls.

This pre-pass is called in CmdEval.eval before the main evaluator, so inline expansion under binders happens transparently.

Changes

File	Change
Strata/DL/Lambda/LExprEval.lean	Add expandInlineCalls
Strata/Languages/Core/CmdEval.lean	Wire expandInlineCalls as a pre-pass before LExpr.eval
StrataTest/DL/Lambda/InlineInQuantifierTests.lean (new)	Tests confirming the bug and the fix

Testing

New test file verifies:

• Top-level inline call expands correctly (baseline sanity check).
• Inline call under a ∀ binder is not expanded by eval alone (confirms the bug).
• expandInlineCalls correctly expands the call under the binder.
• Composing the pre-pass with eval produces the fully reduced result.

[thanhnguyen-aws]

@keyboardDrummer-bot Please rewrite the PR description.

[keyboardDrummer-bot]

Done — I've rewritten the PR description with a clearer structure (problem/solution/changes table/testing).

[tautschnig]

Suggested theorems to lock the behaviour down:

• theorem expandInlineCalls_zero (e : LExpr TBase.mono) : expandInlineCalls F 0 e = e — trivial but worth marking @[simp].
• theorem expandInlineCalls_no_inline (e : LExpr TBase.mono) (h : ∀ sub, sub ∈ subterms e → ¬ isInlineCall F sub) : ∀ fuel, expandInlineCalls F fuel e = e — pre-pass is identity when there's nothing to do (justifies running it unconditionally).
• theorem expandInlineCalls_idempotent (h : sufficientFuel) : expandInlineCalls F fuel (expandInlineCalls F fuel e) = expandInlineCalls F fuel e — protects against double-application surprises (relevant if anyone wires it elsewhere).
• theorem expandInlineCalls_eval_eq : LExpr.eval n σ (expandInlineCalls F m e) = LExpr.eval n σ e for e that contains no inline calls under binders — proves the pre-pass is conservative on terms eval already handles.
• The right long-term fix is to extend Step with congruence rules step_under_abs / step_under_quant (currently absent — confirmed by grep) and prove Step* F rf e (expandInlineCalls F fuel e). That ties the pre-pass back into the semantics machinery and would let it eventually be folded into eval.

[tautschnig]

Two issues with this expansion arm:

1. Stricter trigger than eval. eval (line ~223) inlines on attr.contains .inline || constrArgAt findInlineIfConstr || (hasInlineIfAllCanonical && args.all isCanonicalValue). This pre-pass only checks .inline. So an inlineIfConstr factory whose argument inside a binder would be a constructor at runtime will silently not get expanded by the pre-pass while it would outside the binder. If this asymmetry is intentional (because we can't determine canonicality of bvars), please add a one-line comment saying so; otherwise mirror eval's logic.
2. Duplicated logic. The body / computeTypeSubst / applySubst / substFvarsLifting chain is now a verbatim copy of eval's inline branch. Please factor a private helper tryInlineExpand : Factory T → LExpr T.mono → Option (LExpr T.mono) (returning none when the call doesn't apply) and route both call sites through it. That also makes the proof obligations in the top-level review stateable in one place.

Minor: Bool.and_eq_true_iff.mp h |>.1 is more readable than the current (Bool.and_eq_true_iff.mp h).1 once the helper exists, and matches the idiom used in Semantics.lean:2539.

[tautschnig]

Wiring only here means the bug persists for every other caller of LExpr.eval — at least Lambda.typeCheckAndPartialEval (Strata/DL/Lambda/Lambda.lean:55) and the Lambda evaluator tests. Better to do one of:

• Apply the pre-pass inside LExpr.eval itself (with a guard that fuel > 0, and proof obligation expandInlineCalls_no_inline → eval is unchanged), so all consumers benefit.
• Or expose a single LExpr.evalWithInlineExpansion and switch every existing direct caller of LExpr.eval.

As written, two callers will silently diverge in behaviour for the same input — confusing for anyone debugging.

[tautschnig]

Coverage is thin for the change's blast radius. Please add #guard_msgs cases for:

1. Inline call under a λ binder (the description explicitly mentions lambdas; only forall is exercised).
2. Nested quantifiers with the inline call at the inner level — confirms recursion really does descend, not just stop at the outermost binder.
3. inlineIfConstr / inlineIfAllCanonical factory functions under a binder — locks in the trigger-set asymmetry called out on LExprEval.lean (whichever direction you choose).
4. Fuel-exhaustion: call with fuel := 1 against a 3-deep nested binder containing an inline call; assert the pre-pass returns something sensible (probably the original) rather than partially expanded garbage.
5. A negative test: a term with no inline calls under binders is unchanged by the pre-pass (expandInlineCalls F n e == e). This is the practical witness for the expandInlineCalls_no_inline theorem suggested in the top-level review.