feat: Upstream MPL.SPred.* from mpl
#8745
Conversation
src/Std/Tactic.lean
Outdated
|
|
||
| Note that this does not contain meta programs that implement tactics themselves because these would | ||
| rely on importing things from `Lean` which cannot done in `Std`. |
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
Ah, probably you shoud just move the tactic stuff from Std.Tactic to Lean.Elab.Tactic.
There was a problem hiding this comment.
So the permitted dependency ordering is Lean -> Std -> Init (and no other edges). Makes sense.
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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 ofInit, 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.
There was a problem hiding this comment.
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.
9b48813 to
43875af
Compare
6aa1fb7 to
4dd37ba
Compare
|
Mathlib CI status (docs):
|
7e9cb89 to
80b9764
Compare
80b9764 to
17b13fd
Compare
This reverts commit 61ee83f.
Reverts #8745 until I take a closer look on its breakage in Mathlib on Monday
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`. Co-authored-by: Sebastian Graf <sg@lean-fro.org>
) Reverts leanprover#8745 until I take a closer look on its breakage in Mathlib on Monday
This PR adds a logic of stateful predicates
SPredtoStd.Doin order to support reasoning about monadic programs. It comes with a dedicated proof mode the tactics of which are accessible by importingStd.Tactic.Do.