perf: optimize kernel type-checking for have-telescope simplification in Sym.simp

[leodemoura]

This PR implements a new strategy for simplifying have-telescopes in Sym.simp that achieves linear kernel type-checking time instead of quadratic.

Problem

When simplifying deep have-telescopes, the previous approach using have_congr' produced proofs that type-checked in quadratic time. The simplifier itself was fast, but the kernel became the bottleneck for large telescopes.

For example, at n=100:

• Before: simp = 2.4ms, kernel = 225ms
• After: simp = 3.5ms, kernel = 10ms

The quadratic behavior occurred because the kernel creates fresh free variables for each binder when type-checking, destroying sharing and producing O(n²) intermediate terms.

Solution

We transform sequential have-telescopes into a parallel beta-application form:

have x₁ := v₁; have x₂ := v₂[x₁]; b[x₁, x₂]
  ↓ (definitionally equal)
(fun x₁ x₂' => b[x₁, x₂' x₁]) v₁ (fun x₁ => v₂[x₁])

This parallel form leverages the efficient simplifier for lambdas in Sym.simp. This form enables:

1. Independent simplification of each argument
2. Proof construction using standard congruence lemmas
3. Linear kernel type-checking time

The algorithm has three phases:

1. toBetaApp: Transform telescope → parallel beta-application
2. simpBetaApp: Simplify using congr/congrArg/congrFun' and simpLambda
3. toHave: Convert back to have form

Benchmark Results

Benchmark 1: Chain with all variables used in body

n	Before (simp)	Before (kernel)	After (simp)	After (kernel)
50	1.2ms	32ms	1.6ms	4.4ms
100	2.4ms	225ms	3.5ms	10ms
200	4.5ms	—	8.4ms	27ms
500	11.7ms	—	33.6ms	128ms

Benchmark 3: Parallel declarations (simplified values)

n	Before (simp)	Before (kernel)	After (simp)	After (kernel)
50	0.5ms	24ms	0.8ms	1.8ms
100	1.2ms	169ms	1.8ms	5.3ms
200	2.2ms	—	3.9ms	17ms
500	5.9ms	—	12.3ms	93ms

Benchmark 5: Chain with single dependency

n	Before (simp)	Before (kernel)	After (simp)	After (kernel)
100	1.6ms	6.2ms	1.8ms	6.2ms
200	2.8ms	21.6ms	4.4ms	16.5ms
500	7.3ms	125ms	12.8ms	72ms

Key observations:

• Kernel time is now linear in telescope depth (previously quadratic)
• Simp time increases slightly due to the transformation overhead
• Total time (simp + kernel) is dramatically reduced for large telescopes
• The improvement is most pronounced when the body depends on many variables

Trade-offs

• Proof sizes are larger (more congruence lemma applications)
• Simp time has ~1.5x overhead from the transformation
• For very small telescopes (n < 10), the overhead may not pay off

The optimization targets the critical path: kernel type-checking was the bottleneck preventing scaling to realistic symbolic simulation workloads.