Advanced Lean · 8 min

Make proof checking faster

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

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

Both cards state the same theorem: a list containing n copies of 7 has length n. They use the same name and statement, so each is checked in a separate file. Change List size to update both statements together.

decide computes the list’s length while reducing a decision procedure. exact List.length_replicate applies a theorem already proved for every length and element, avoiding that calculation. Lean checks both proofs.

Choose Compare both proofs to measure them on your device. The comparison warms up each proof, then alternates five measured checks of each and displays the median. Times include elaboration and kernel checking, but exclude compiler download and initialization. Small timings can vary between runs.

The exercise below fixes the length at 100. Replace the missing proof with the theorem application. Comparing the cards does not complete the exercise: use Check to validate your own proof.

Exercise

Replace sorry with a theorem application using List.length_replicate, then check the exercise.

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

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

Related example