let-lifting for SymM

Sym.liftLets moves let/have declarations toward the root of a term, as far out as their dependencies allow. The result is definitionally equal to the input (lifting is a zeta-permutation), so no proof term is produced.

The implementation avoids the performance pitfalls of the standard Lean.Meta.liftLets:

• No per-binder instantiate/abstract round-trips. The traversal carries an environment xs : PArray Expr mapping de Bruijn indices of the lets being lifted to scratch free variables. Each subterm is processed once; all de Bruijn arithmetic for the result is performed by a single closing pass (mkLets).
• Pointer-keyed memoization. Results are cached per (environment, expression) pointer pair. For subterms without loose bound variables the result does not depend on the environment, so they are cached by expression pointer alone; this also makes the let-block of a shared closed subterm lifted once and shared by all occurrences.
• O(1) merging. In the maximally shared world, syntactically equal types/values are pointer-equal, so deduplicating lets with equal definitions is a pointer-map lookup (cf. the merge := true option of extract_lets). If occurrences disagree on let vs have, the merged declaration is a let, since tactics may zeta-delta reduce lets but not haves.

Scope:

• lets under fun/∀ binders are not lifted, even when they do not depend on the binder. Binder nodes are treated as opaque: their bound occurrences of lifted lets are substituted (they must be, since inserting foreign binders shifts indices), but no let is collected from inside them.
• Both dependent lets and haves (nondependent lets) are lifted, and the nondep flag is preserved.
• lets occurring in the types of lifted lets are lifted as well.

def Lean.Meta.Sym.liftLets (e : Expr) : SymM Expr

Moves the let/have declarations of e toward the root, as far out as their dependencies allow. Nested declarations are flattened, and declarations with pointer-equal types and values are merged. The result is definitionally equal to e.

lets under fun/∀ binders are not lifted; see the module docstring for the precise scope.

Assumptions:

• e is maximally shared and has no loose bound variables.
• Metavariables in e have been instantiated; they are treated as opaque atoms.

If nothing is lifted, the result is pointer-equal to e (check with isSameExpr).

Equations

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