Advanced Lean

Efficiency: reuse a theorem

Prove the same list length without computing the list.

-- Same proposition as CalculateLength.lean; a different proof.
-- The library already proves this for every length and element.

theorem copies_length :
    (List.replicate 100 7).length = 100 := by
  exact List.length_replicate


-- Lean instantiates a general theorem instead of computing 100 cells.
-- The kernel checks this application; no proof is skipped.
-- No increased recursion or heartbeat limits are needed.

-- Other useful habits:
-- * Use exact when you already have a theorem with the required type.
-- * Use simp? to find the lemmas, then try the suggested simp only.
-- * Name intermediate facts with have instead of repeating proof search.
-- * Measure: a shorter proof script is not automatically a faster proof.

Explanation

`exact List.length_replicate`

Lean infers the length and element from the goal. It checks an application of an existing theorem, avoiding reduction of the list.

`simp? · simp only`

simp? can suggest a sufficient list of simplification lemmas. An explicit list can reduce search and make a proof more predictable, but measure the result.

`Checking versus execution`

This example optimizes proving a statement. Tail recursion and array reuse address a different cost: running a program.

Expected output

Reference only. Run the file to check its actual result.

File checked successfully.

Exercise

Change 100 to 200000 in both places. This theorem application still works without constructing the list. Keep the calculation example small.