search

leanprover-community / aesop

White-box automation for Lean 4
Apache License 2.0
183 stars 26 forks source link

RFC: do not unfold semireducible definitions by default #146

Open fpvandoorn opened 2 months ago

fpvandoorn commented 2 months ago

I think aesop (and all other automation) should apply lemmas up to instances transparency by default. Otherwise, I don't think it is possible to make performant automation. It is unreasonable to expect automation to be quick if it can unfold almost any definitions, and experimentally, sometimes apply ... takes seconds to fail (even if the lemma "obviously" doesn't apply). Sure, in those cases we could do better in Mathlib, marking more things irreducible, but we cannot only fix in on Mathlib's side.

My experience is that aesop is often very slow, and there have been multiple PRs to Mathlib moving away from aesop because of performance reasons: 1 2 3 4.

This will lead to a regression in capabilities of aesop and we will need to mark more things as unfoldable by aesop. Maybe specialized tactics like aesop_cat can work up to semireducible transparency.

I think I already talked to @JLimperg about this in person, but I'm surprised that I never wrote up the suggestion on Zulip/Github.

JLimperg commented 2 months ago

Thanks for bringing this up! Link to Zulip discussion for reference: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/should.20aesop.20unfold.20semireducible.20definitions.3F