Advanced Lean
Efficiency: calculate the proof
Prove a concrete list length by reducing a decision procedure.
Open CalculateLength.lean in editor-- Compare this file with ReuseLengthTheorem.lean.
-- Both files prove exactly the same proposition.
-- The efficiency lesson compares both files with repeated measurements.
theorem copies_length :
(List.replicate 100 7).length = 100 := by
decide
-- decide constructs a proof by reducing the decision procedure.
-- Here that means building and traversing a 100-element list.
-- The kernel must check the resulting proof as well.
-- A higher heartbeat limit allows more work; it does not make it faster.
Explanation
by decide
Proves this closed proposition through computation. The decision procedure computes the list length; a general lemma avoids that calculation.
Browser limits
This example keeps the list short because browser call stacks are limited. Raising Lean’s maxRecDepth or maxHeartbeats cannot enlarge the browser’s stack.
Elapsed time
Output reports the whole check, including elaboration and kernel checking. Compare repeated runs on the same device; this is not an isolated kernel benchmark.
Expected output
Reference only. Run the file to check its actual result.
File checked successfully.
Exercise
Open the companion example and compare the two checks. Try a smaller list in both files.