feat: Upstream MPL.SPred.* from mpl

[sgraf812]

This PR adds a logic of stateful predicates SPred to Std.Do in order to support reasoning about monadic programs. It comes with a dedicated proof mode the tactics of which are accessible by importing Std.Tactic.Do.

[sgraf812]

Given this comment block, Std.Tactic might be a strange to put the proof mode.
I also don't understand the comment. Can you implement a tactic without depending on Lean?
Besides, the definitions I added depend on Lean without introducing any cycles (apparently).
Is this comment perhaps out of date?

Indepdently, I don't like Std.Tactic.Do.ProofMode.Tactic.Refine much. Quite long and the initial Tactic is redundant.

[TwoFX]

Ah, probably you shoud just move the tactic stuff from Std.Tactic to Lean.Elab.Tactic.

[sgraf812]

So the permitted dependency ordering is Lean -> Std -> Init (and no other edges). Makes sense.

[sgraf812]

Lean.Elab.Tactic.Do.ProofMode.Tactic.Refine isn't exactly an improvement, but I take solice in the fact there also is Lean.Meta.Tactic.Simp.Arith.Nat.Simp.

[sgraf812]

Alright, spent quite some time refactoring elaborators in terms of @[builtin_tactic] and moving modules around. Would appreciate if you could give the directory outline a quick glance and nod.

[TwoFX]

I'm afraid it's not quite right yet.

If you are using @[builtin_tactic] (which is the right thing to do in this case), then one of the following must still be true:

• the corresponding syntax must be a builtin_parser, and all lemmas that are referenced by the terms generated by your tactic are part of Init, or
• the user must import the module where the syntax is declared and the contains all auxiliary lemmas.

Now, I'm pretty sure we don't want to ask users to import something from Lean to get access to your tactics, as Lean.* is reserved for metaprogramming and implementation details. Instead, we will want to follow the bv_decide route, where you import Std.Tactic.BVDecide. So I suggest moving the syntax of your tactics to Std.Tactic.Do and make sure that Std.Do gets transitively imported from there.

In addition, bv_decide defines a macro in Init directing users to the correct import. I think this is a good idea that you should copy.

[sgraf812]

Thanks. I think now I've got it.

the corresponding syntax must be a builtin_parser, and all lemmas that are referenced by the terms generated by your tactic are part of Init, or

(Not relevant to this PR, but FYI intro is a counterexample (Lean.Elab.Tactic.evalIntro), because it combines regular, non-builtin syntax with a @[builtin_tactic]. I think that's OK because intro syntax is not expected to change. But maybe your rule does not apply to syntax defined in Init.)

In addition, bv_decide defines a macro in Init directing users to the correct import. I think this is a good idea that you should copy.

Done. I added the erroring stub macros including docstrings to src/Init/Tactics.lean and the actual syntax definitions to src/Std/Tactic/Do/Syntax.lean. My test file seems to be happy.

If there isn't anything else, I'll merge today. There will be follow-up MRs next week to do touch ups.

[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 c2876a1a6a42e6df458ffb37abbc3868632beb58 --onto faffe863343211d03d07d4ef19d90a2aa9d6fc8c. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-13 16:07:38)
• ❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-06-12 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-13 16:42:09)