feat: non-chronological backtracking for grind (WIP)

[leodemoura]

This PR implements non-chronological backtracking for the grind tactic. This feature ensures that grind does not need to process irrelevant branches after performing a case-split that is not relevant. It is not just about performance, but also the size of the final proof term. The new test demonstrates this feature in practice.

-- In the following test, the first 8 case-splits are irrelevant,
-- and non-choronological backtracking is used to avoid searching
-- (2^8 - 1) irrelevant branches
/--
trace: 
[grind.split] p8 ∨ q8, generation: 0
[grind.split] p7 ∨ q7, generation: 0
[grind.split] p6 ∨ q6, generation: 0
[grind.split] p5 ∨ q5, generation: 0
[grind.split] p4 ∨ q4, generation: 0
[grind.split] p3 ∨ q3, generation: 0
[grind.split] p2 ∨ q2, generation: 0
[grind.split] p1 ∨ q1, generation: 0
[grind.split] ¬p ∨ ¬q, generation: 0
-/
#guard_msgs (trace) in
set_option trace.grind.split true in
theorem ex
    : p ∨ q →
      ¬ p ∨ q →
      p ∨ ¬ q →
      ¬ p ∨ ¬ q →
      p1 ∨ q1 →
      p2 ∨ q2 →
      p3 ∨ q3 →
      p4 ∨ q4 →
      p5 ∨ q5 →
      p6 ∨ q6 →
      p7 ∨ q7 →
      p8 ∨ q8 →
      False := by
  grind (splits := 10)

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 4eccb5b4792c270ad10ac059b9672a8845961079 --onto 47a1355fc43b29421cfb02047445888bbb414441. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-22 03:32:38)
• ✅ Mathlib branch lean-pr-testing-8440 has successfully built against this PR. (2025-05-22 21:32:30) View Log
• ✅ Mathlib branch lean-pr-testing-8440 has successfully built against this PR. (2025-05-23 05:23:32) View Log
• ✅ Mathlib branch lean-pr-testing-8440 has successfully built against this PR. (2025-05-23 20:22:38) View Log