Unexpected behavior of simp with pre lemma

Stream: lean4

[Tomas Skrivan]

Pre and post simp theorems are applied only until first match. By that I mean if simp rewrites an expression E to E' at pre/post step, simp does not try to apply pre/post theorems to E' but instead jumps into sub-expressions.

This lead to this surprising behavior:

def foo (f : Nat → Nat) := λ a b : Nat => f b

theorem foo_simp (f : Nat → Nat) (a b : Nat) : foo f a b = f b := by simp[foo]

-- works
example (f : Nat → Nat) : foo f a (foo f b c) = f (f c) := by simp (config := {singlePass := true}) only [↓foo_simp]

-- does not work
example : foo (λ x => x) a (foo (λ x => x) b c) = c := by simp (config := {singlePass := true}) only [↓foo_simp]

My application: I know my simp lemmas can eliminate foo in a single pass. I really want to achieve that as I'm working with rather large expressions and case like this tripped me over.

I have modified tracing a bit to show pre and post stages and the trace for:

example : foo (λ x => x) a (foo (λ x => x) b c) = c := by simp (config := {singlePass := true}) only [↓foo_simp]

is:

...
[Meta.Tactic.simp] Running pre on foo (fun x => x) a (foo (fun x => x) b c)
[Meta.Tactic.simp.rewrite] foo_simp:1000, foo (fun x => x) a (foo (fun x => x) b c) ==> foo (fun x => x) b c
[Meta.Tactic.simp] Running pre on foo
[Meta.Tactic.simp] Running post on foo
[Meta.Tactic.simp] Running pre on fun x => x
[Meta.Tactic.simp] Running pre on x
[Meta.Tactic.simp] Running post on x
...

In constrast, in the working example the trace is:

...
[Meta.Tactic.simp] Running pre on foo f a (foo f b c)
[Meta.Tactic.simp.rewrite] foo_simp:1000, foo f a (foo f b c) ==> f (foo f b c)
[Meta.Tactic.simp] Running pre on f
[Meta.Tactic.simp] Running post on f
[Meta.Tactic.simp] Running pre on foo f b c
[Meta.Tactic.simp.rewrite] foo_simp:1000, foo f b c ==> f c
[Meta.Tactic.simp] Running pre on c
[Meta.Tactic.simp] Running post on c
...

---

I can fix this by writing my own variant of Lean.Meta.Tactic.Simp.rewritePre and passing it as a custom pre method. Is the current behavior desirable?

[Jeremy Salwen]

Not sure if this is helpful coming so late, but to me the difference between the two cases is that the non-working example requires you to rewrite the same node in the expression tree multiple times, while the working example only rewrites the root once, then a child expression once. I am curious about the logging code you used to debug simp though :)

[Tomas Skrivan]

Have a look at how norm_num is implemented in mathlib. It calls the simplifier with custom pre/post methods, look at this line