refactor: cleanup simp types and pre and post method semantics

[leodemoura]

Before this commit, Simprocs were defined as Expr -> SimpM (Option Step), where Step is inductively defined as follows:

inductive Step where
  | visit : Result → Step
  | done  : Result → Step

Here, Result is a structure containing the resulting expression and a proof demonstrating its equality to the input. Notably, the proof is optional; in its absence, simp assumes reflexivity.

A simproc can:

• Fail by returning none, indicating its inapplicability. In this case, the next suitable simproc is attempted, along with other simp extensions.
• Succeed and invoke further simplifications using the .visit
  constructor. This action returns control to the beginning of the
  simplification loop.
• Succeed and indicate that the result should not undergo further
  simplifications. However, I find the current approach unsatisfactory, as it does not align with the methodology employed in Transform.lean, where we have the type:

inductive TransformStep where
  /-- Return expression without visiting any subexpressions. -/
  | done (e : Expr)
  /--
  Visit expression (which should be different from current expression) instead.
  The new expression `e` is passed to `pre` again.
  -/
  | visit (e : Expr)
  /--
  Continue transformation with the given expression (defaults to current expression).
  For `pre`, this means visiting the children of the expression.
  For `post`, this is equivalent to returning `done`. -/
  | continue (e? : Option Expr := none)

This type makes it clearer what is going on. The new Simp.Step type is similar but use Result instead of Expr because we need a proof.

Other modifications:

• The pre and post methods have now type Simproc.
• simprocs field at Methods was deleted.
• Added andThen combinator for Simproc.
• Cleanup simpLoop semantics.

Todo: cleanup reduceStep.

Recording adapation PRs here:

• chore: fixes for simp refactor leanprover-community/batteries#571 (working)
• feat: adaptations for leanprover/lean4#3210 leanprover-community/aesop#98 (working but with one test regression)
• chore: adaptations to leanprover/lean4#3210 leanprover-community/mathlib4#10133 (still WIP)

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. (2024-01-23 04:44:15)
• 💥 Mathlib branch lean-pr-testing-3210 build failed against this PR. (2024-01-30 03:12:56) View Log
• 💥 Mathlib branch lean-pr-testing-3210 build failed against this PR. (2024-01-30 03:59:57) View Log
• 💥 Mathlib branch lean-pr-testing-3210 build failed against this PR. (2024-01-30 21:46:39) View Log
• 💥 Mathlib branch lean-pr-testing-3210 build failed against this PR. (2024-01-30 23:45:17) View Log
• 🟡 Mathlib branch lean-pr-testing-3210 build against this PR was cancelled. (2024-01-31 01:37:07) View Log
• 💥 Mathlib branch lean-pr-testing-3210 build failed against this PR. (2024-01-31 01:44:07) View Log
• 🟡 Mathlib branch lean-pr-testing-3210 build this PR didn't complete normally. (2024-01-31 01:55:37) View Log
• 💥 Mathlib branch lean-pr-testing-3210 build failed against this PR. (2024-01-31 02:00:23) View Log
• 🟡 Mathlib branch lean-pr-testing-3210 build this PR didn't complete normally. (2024-01-31 02:29:53) View Log
• 💥 Mathlib branch lean-pr-testing-3210 build failed against this PR. (2024-01-31 02:38:10) View Log
• 💥 Mathlib branch lean-pr-testing-3210 build failed against this PR. (2024-01-31 02:52:30) View Log
• 💥 Mathlib branch lean-pr-testing-3210 build failed against this PR. (2024-01-31 04:19:01) View Log
• 🟡 Mathlib branch lean-pr-testing-3210 build against this PR was cancelled. (2024-01-31 05:32:14) View Log
• 🟡 Mathlib branch lean-pr-testing-3210 build this PR didn't complete normally. (2024-01-31 05:32:29) View Log
• 🟡 Mathlib branch lean-pr-testing-3210 build against this PR was cancelled. (2024-01-31 05:39:08) View Log
• 🟡 Mathlib branch lean-pr-testing-3210 build against this PR was cancelled. (2024-01-31 05:44:23) View Log
• 💥 Mathlib branch lean-pr-testing-3210 build failed against this PR. (2024-01-31 05:54:50) View Log
• 🟡 Mathlib branch lean-pr-testing-3210 build against this PR was cancelled. (2024-02-01 02:15:42) View Log
• 🟡 Mathlib branch lean-pr-testing-3210 build against this PR was cancelled. (2024-02-01 02:35:37) View Log
• ❌ Mathlib branch lean-pr-testing-3210 built against this PR, but linting failed. (2024-02-01 03:47:21) View Log
• 🟡 Mathlib branch lean-pr-testing-3210 build this PR didn't complete normally. (2024-02-01 04:02:51) View Log
• ✅ Mathlib branch lean-pr-testing-3210 has successfully built against this PR. (2024-02-01 05:29:41) View Log

[leodemoura]

The register_simp_attr <id> command now also creates a simproc set.