issue !4#5025: `simp` does not try applying `@[refl]` lem...

Stream: triage

[Random Issue Bot]

Today I chose issue #5025 for discussion!

simp does not try applying @[refl] lemmas to close the goal
Created by @Kim Morrison (@kim-em) on 2023-06-14
Labels: lean4-change-in-behaviour

Is this issue still relevant? Any recent updates? Anyone making progress?

[Ruben Van de Velde]

Still relevant as far as I'm aware

[Kyle Miller]

What's the issue here? Is it that simp doesn't use the rfl tactic to close goals? Or that we should tag @[refl] lemmas as @[simp] too?

[Ruben Van de Velde]

My understanding is that lean 3 simp used something like rfl at the end, yeah. I guess we could just tag all the refl lemmas with simp as well, but that seems annoying

[Kyle Miller]

It's stronger having every @[refl] lemma be a @[simp] lemma, since the proposition could appear somewhere within the goal.

[Ruben Van de Velde]

That's true

[Bhavik Mehta]

That's stronger, but wouldn't it be a pretty bad performance hit, since the discrimination key could be super general?

[Kyle Miller]

@Bhavik Mehta docs#eq_self and docs#iff_self are simp lemmas (and they're ones that always appear in every simp set via docs#Lean.Elab.Tactic.simpOnlyBuiltins, even if you use simp only). The performance impact would be similar; the key for a relation R would be R * * and would apply wherever R appears.

[Bhavik Mehta]

Hmm, okay. I suppose I shouldn't really complain about potential performance hits without seeing benchmarks anyway :)