mathlib3 documentation


Linter for simplification lemmas #

This files defines several linters that prevent common mistakes when declaring simp lemmas:

meta def is_simp_eq (a b : expr) :

Checks whether two expressions are equal for the simplifier. That is, they are reducibly-definitional equal, and they have the same head symbol.

meta def simp_nf_linter (timeout : := 200000) (d : declaration) :

Reports declarations that are simp lemmas whose left-hand side is not in simp-normal form.

This note gives you some tips to debug any errors that the simp-normal form linter raises.

The reason that a lemma was considered faulty is because its left-hand side is not in simp-normal form. These lemmas are hence never used by the simplifier.

This linter gives you a list of other simp lemmas: look at them!

Here are some tips depending on the error raised by the linter:

  1. 'the left-hand side reduces to XYZ': you should probably use XYZ as the left-hand side.

  2. 'simp can prove this': This typically means that lemma is a duplicate, or is shadowed by another lemma:

    2a. Always put more general lemmas after specific ones:

    @[simp] lemma zero_add_zero : 0 + 0 = 0 := rfl
    @[simp] lemma add_zero : x + 0 = x := rfl

    And not the other way around! The simplifier always picks the last matching lemma.

    2b. You can also use @[priority] instead of moving simp-lemmas around in the file.

    Tip: the default priority is 1000. Use @[priority 1100] instead of moving a lemma down, and @[priority 900] instead of moving a lemma up.

    2c. Conditional simp lemmas are tried last. If they are shadowed just remove the simp attribute.

    2d. If two lemmas are duplicates, the linter will complain about the first one. Try to fix the second one instead! (You can find it among the other simp lemmas the linter prints out!)

  3. 'try_for tactic failed, timeout': This typically means that there is a loop of simp lemmas. Try to apply squeeze_simp to the right-hand side (removing this lemma from the simp set) to see what lemmas might be causing the loop.

    Another trick is to set_option trace.simplify.rewrite true and then apply try_for 10000 { simp } to the right-hand side. You will see a periodic sequence of lemma applications in the trace message.

meta def linter.simp_nf  :

A linter for simp lemmas whose lhs is not in simp-normal form, and which hence never fire.

A linter for simp lemmas whose lhs has a variable as head symbol, and which hence never fire.

meta def linter.simp_comm  :

A linter for commutativity lemmas that are marked simp.