Why can simp only make progress?

Stream: new members

[VayusElytra]

This is a more general question: many times in the past when I have used aesop, it has suggested to use "simp only" without specifying any theorems or lemmas in brackets - and this does manage to make progress. How can that be the case? I thought simp only used EXCLUSIVELY the theorems in brackets to make progress, so if you give it none it should not be able to do anything...?

My apologies for the lack of MWE, the instance of this behaviour that prompted this question would require hundreds of lines of code to show...

[Yaël Dillies]

VayusElytra said:

I thought simp only used EXCLUSIVELY the theorems in brackets to make progress

This is incorrect. It also uses some reduction rules whose list you can find in docs#Lean.Meta.Simp.Config

[Yaël Dillies]

The configuration of your simp only [] calls can be modified by doing simp only (config := ...) []. If you try something like simp only (config := { zeta := false, eta := false, beta := false, iota := false}) [], it really shouldn't make progress. Try removing things from config := { ... } until it starts making progress again.

[Ruben Van de Velde]

A typical example is (fun x => f x) y getting simplified to f y

[VayusElytra]

Thank you very much, that makes a lot of sense :)

[Damiano Testa]

Also, with no extra config options, "no lemmas" actually means the content of docs#Lean.Elab.Tactic.simpOnlyBuiltins, i.e. [``eq_self, ``iff_self].