Can Lean simp arguments be ordered?

Question

I want to simplify the expression 0 * 1 * 1 * 1 * 0 using simp only [mul_zero, zero_mul]. I would like mul_zero to fire first, so that the entire expression is simplified to zero in only one step. If mul_zero fires first, I would expect the simplification process to take 4 steps, due to there being one step to eliminate each 1.

Is there a way I can tell Lean to prioritize which simplification lemma to try first?

Answer 1

Using mathlib's simp_rw, you can order your lemmas:

example (a : nat) : a + 0 * 1 * 1 * 1 * 0 = a := by simp_rw [mul_zero, add_zero]

simp_rw [lemma1, lemma2] does the hand-waved equivalent of simp only [lemma1], simp only [lemma2].

Answer 2

Lean's simp arguments are already ordered:

def a := 0
def b := 0
def c := 0
def f : ℕ → ℕ := default
@[simp] lemma k (x) : f x = b := rfl
@[simp] lemma l : f b = c := rfl

example : f (f a) = c := by simp only [k, l]
example : f (f a) = c := by simp only [l, k] -- failure!