more improvements found by tryAtEachStep

[dwrensha]

No description provided.

[augustepoiroux]

That's great, thanks! I am currently trying tryAtEachStep with rfl.
What do you think about using it with grind??

[augustepoiroux]

Here is the result with rfl: #3
@dwrensha would be happy to have your opinion on it

[dwrensha]

I would caution against applying rfl and grind suggestions indiscriminately.

With grind there is significant danger that you will make proofs take longer to execute. Unfortunately, tryAtEachStep does not yet measure performance.

With rfl there is danger that you will add defeq abuse.

[augustepoiroux]

I see, thanks. Indeed, having a way to automatically compare heartbeats before and after would be a really nice feature

[dwrensha]

Mathlib's "tactic analysis framework" has done some work in this direction: https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/TacticAnalysis/Declarations.lean

[augustepoiroux]

@dwrensha More improvements there: #6
I created a tool based on tryAtEachStep automatically trying different tactics and applying the ones decreasing both the number of lines and the number of heartbeats. In the PR above >95% of the golfs are generated by this tool with the following criteria: reducing the number of lines by at least 2, and strictly decreasing the number of heartbeats.