Policy on replacing manual proofs with automated proofs

Stream: mathlib4

[Jannis Limperg]

At ItaLean, we started a project to add some grind/Aesop annotations to Mathlib. A question that came up during this is Mathlib's stance on replacing manual proofs by automated proofs. For a simple example, this PR proposes to replace some manual List proofs by aesop, without adding any new Aesop annotations.

Advantages of this type of refactoring are (a) less clutter; (b) the new proofs may serve as regression tests, so if either Aesop changes or the Aesop rule set is modified and these proofs break, we know something is probably wrong.

The main disadvantage is that automation is usually much slower than a direct proof, though the slowdown may not be large in absolute term (10ms vs 50ms, say). Additionally, there is a possible maintenance burden since the proofs may be broken by tactic or rule set upgrades, dual to the 'regression test' point above.

Any opinions on this?

[Jannis Limperg]

cc @Farruh Habibullaev @Michael Rothgang

[Violeta Hernández]

The general consensus is that small proofs like these can and probably should stay in term mode. For anything larger than two or three lines, we value the improved maintainability more than we do performance.

[Jannis Limperg]

Okay, thank you! We'll implement that then.

[Farruh Habibullaev]

Another PR for aesop & simp annotation in Mathlib/Data/List/basic.lean: https://github.com/leanprover-community/mathlib4/pull/32698

[Eric Wieser]

@Kim Morrison, was the intent of the new reprove .. by command to allow recording that grind can prove things too?

[Kim Morrison]

In test files, yes. I don't think it belongs in libraries.