Zulip Chat Archive

Stream: general

Topic: simp lemmas priority

Yury G. Kudryashov (Nov 12 2019 at 02:43):

Hi, how does Lean decide which simp lemma to apply? I'm trying to add

@[simp] theorem ball_image_iff {f : α  β} {s : set α} {p : β  Prop} :
  ( y  f '' s, p y)  ( x  s, p (f x)) :=
  (assume h a ha, h _ $ mem_image_of_mem f ha)

but Lean always applies mem_image before it, and for ∀ y ∈ f '' s, p y it leads to worse results. I tried adding @[simp, priority=20] to mem_image, with no effect.

Floris van Doorn (Nov 12 2019 at 17:58):

I think simp simplifies starting at the leaves (atomic expressions) and then building up. So it will always simplify subexpressions of t before simplifying t. You probably get the desired behavior if you put the LHS of the above theorem in simp-normal form.

Last updated: Aug 03 2023 at 10:10 UTC