perf: fuse fvar substitution into instantiateMVars (#12233)

This PR replaces the default `instantiateMVars` implementation with a
two-pass variant that fuses fvar substitution into the traversal,
avoiding separate `replace_fvars` calls for delayed-assigned MVars and
preserving sharing. The old single-pass implementation is removed
entirely.

The previous implementation had quadratic complexity when instantiating
expressions with long chains of nested delayed-assigned MVars. Such
chains arise naturally from repeated `intro`/`apply` tactic sequences,
where each step creates a new delayed assignment wrapping the previous
one. The new two-pass approach resolves the entire chain in a single
traversal with a fused fvar substitution, reducing this to linear
complexity.

### Terminology (used in this PR and in the source)

* **Direct MVar**: an MVar that is not delayed-assigned.
* **Pending MVar**: the direct MVar stored in a
`DelayedMetavarAssignment`.
* **Assigned MVar**: a direct MVar with an assignment, or a
delayed-assigned MVar with an assigned pending MVar.
* **MVar DAG**: the directed acyclic graph of MVars reachable from the
expression.
* **Resolvable MVar**: an MVar where all MVars reachable from it
(including itself) are assigned.
* **Updateable MVar**: an assigned direct MVar, or a delayed-assigned
MVar that is resolvable but not reachable from any other resolvable
delayed-assigned MVar.

In the MVar DAG, the updateable delayed-assigned MVars form a cut (the
**updateable-MVar cut**) with only assigned MVars behind it and no
resolvable delayed-assigned MVars before it.

### Two-pass architecture

**Pass 1** (`instantiate_direct_fn`): Traverses all MVars and
expressions reachable from the initial expression and instantiates all
updateable direct MVars (updating their assignment with the result),
instantiates all level MVars, and determines if there are any updateable
delayed-assigned MVars.

**Pass 2** (`instantiate_delayed_fn`): Only run if pass 1 found
updateable delayed-assigned MVars. Has an **outer** and an **inner**
mode, depending on whether it has crossed the updateable-MVar cut.

In outer mode (empty fvar substitution), all MVars are either unassigned
direct MVars (left alone), non-updateable delayed-assigned MVars
(pending MVar traversed in outer mode and updated with the result), or
updateable delayed-assigned MVars. When a delayed-assigned MVar is
encountered, its MVar DAG is explored (via `is_resolvable_pending`) to
determine if it is resolvable (and thus updateable). Results are cached
across invocations.

If it is updateable, the substitution is initialized from its arguments
and traversal continues with the value of its pending MVar in inner
mode. In inner mode (non-empty substitution), all encountered
delayed-assigned MVars are, by construction, resolvable but not
updateable. The substitution is carried along and extended as we cross
such MVars. Pending MVars of these delayed-assigned MVars are NOT
updated with the result (as the result is valid only for this
substitution, not in general).

Applying the substitution in one go, rather than instantiating each
delayed-assigned MVar on its own from inside out, avoids the quadratic
overhead of that approach when there are long chains of delayed-assigned
MVars.

**Write-back behavior**: Pass 2 writes back the normalized pending MVar
values of delayed-assigned MVars above the updateable-MVar cut (the
non-resolvable ones whose children may have been resolved). This is
exactly the right set: these MVars are visited in outer mode, so their
normalized values are suitable for storing in the mctx. MVars below the
cut are visited in inner mode, so their intermediate values cannot be
written back.

### Pass 2 scope-tracked caching

A `scope_cache` data structure ensures that sharing is preserved even
across different delayed-assigned MVars (and hence with different
substitutions), when possible. Each `visit_delayed` call pushes a new
scope with fresh fvar bindings. The cache correctly handles cross-scope
reuse, fvar shadowing, and late-binding via generation counters and
scope-level tracking.

The `scope_cache` has been formally verified:
`tests/elab/scopeCacheProofs.lean` contains a complete Lean proof that
the lazy generation-based implementation refines the eager
specification, covering all operations (push, pop, lookup, insert)
including the rewind lazy cleanup with scope re-entry and degradation.
The key correctness invariant is inter-entry gen list consistency
(GensConsistent), which, unlike per-entry alignment with `currentGens`,
survives pop+push cycles.

### Behavioral differences from original `instantiateMVars`

The implementation matches the original single-pass `instantiateMVars`
behavior with one cosmetic difference: the new implementation
substitutes fvars inline during traversal rather than constructing
intermediate beta-redexes, producing more beta-reduced terms in some
edge cases. This changes the pretty-printed output for two elab tests
(`1179b`, `depElim1`) but all terms remain definitionally equal.

### Tests

Correctness and performance tests for the new implementation were added
in #12808.

### Files

- `src/library/instantiate_mvars.cpp` — C++ implementation of both
passes (replaces `src/kernel/instantiate_mvars.cpp`)
- `src/library/scope_cache.h` — scope-aware cache data structure
- `src/Lean/MetavarContext.lean` — exported accessors for
`DelayedMetavarAssignment` fields
- `tests/elab/scopeCacheProofs.lean` — formal verification of
`scope_cache` correctness
- `tests/elab/1179b.lean.out.expected`,
`tests/elab/depElim1.lean.out.expected` — updated expected output

Co-authored-by: Claude <noreply@anthropic.com>

---------

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

Author: nomeata

src/Lean/Elab/PreDefinition/Basic.lean

@@ -11,7 +11,6 @@ public import Lean.Util.NumApps
 public import Lean.Meta.Eqns
 public import Lean.Elab.RecAppSyntax
 public import Lean.Elab.DefView
-
 public section
 
 namespace Lean.Elab

src/Lean/MetavarContext.lean

@@ -400,6 +400,12 @@ def MetavarContext.getDelayedMVarAssignmentCore? (mctx : MetavarContext) (mvarId
 def MetavarContext.getDelayedMVarAssignmentExp (mctx : MetavarContext) (mvarId : MVarId) : Option DelayedMetavarAssignment :=
   mctx.dAssignment.find? mvarId
 
+@[export lean_delayed_mvar_assignment_fvars]
+def DelayedMetavarAssignment.fvarsExp (d : DelayedMetavarAssignment) : Array Expr := d.fvars
+
+@[export lean_delayed_mvar_assignment_mvar_id_pending]
+def DelayedMetavarAssignment.mvarIdPendingExp (d : DelayedMetavarAssignment) : MVarId := d.mvarIdPending
+
 def getDelayedMVarAssignment? [Monad m] [MonadMCtx m] (mvarId : MVarId) : m (Option DelayedMetavarAssignment) :=
   return (← getMCtx).getDelayedMVarAssignmentCore? mvarId
 

src/kernel/CMakeLists.txt

@@ -18,5 +18,4 @@ add_library(
   quot.cpp
   inductive.cpp
   trace.cpp
-  instantiate_mvars.cpp
 )