rfl tactic

Stream: mathlib4

[Scott Morrison]

@Newell Jensen, I agree relationAppM? belongs higher up. #253 hasn't seen much progress recently; perhaps one solution is to make a mini-PR with just relationAppM? in some "central" location. You can then use it for your work, and #253 can be refactored to use it.

[Newell Jensen]

@Scott Morrison from the current directory structure my suggestion would be to make a directory Relation in the Tactic folder and then within it that we could have Symm.lean, Trans.lean, Rfl.lean and Main.lean (this actually follows the directory structure in Lean4).

[Scott Morrison]

That sounds fine. Where in would you put something like relationAppM?? That feels like it should go somewhere even more central, e.g. Mathlib/Lean/Expr.lean.

[Newell Jensen]

I was thinking in the Main.lean but if others think it should be somewhere else and have better reasons than that is probably the better solution. I was just modeling my suggestion after the directory structure within Lean4s tactics.

[Newell Jensen]

From the other code in Mathlb/Lean/Expr folder seems better to keep tactic code in the Tactic directory IMHO.

[Newell Jensen]

@Scott Morrison here is #425. Thanks for the input.

[Johan Commelin]

@Newell Jensen Note that you can write mathlib4#425 and zulip will turn this into mathlib4#425. This works with every repo in the leanprover-community organization on github.

[Newell Jensen]

Thanks @Johan Commelin

[Newell Jensen]

@Mario Carneiro just put up mathlib4#436 and let me know if you can think of any further corner cases to check for the attribute parsing. I based this branch off of mathlib4#425 but for some reason github is showing the additional file from mathlib4#425 (will most likely go away if that branch lands first).

[Newell Jensen]

From what I read online having two PRs from dependent branches would be handled appropriately. Seeing the commit history of the parent branch in the child PR is making me queasy... :laughing:

[Mario Carneiro]

yeah that's normal

[Newell Jensen]

@Mario Carneiro updated the branch to use elab_rules and pushed. However, something I noticed, and this may not be a big deal, is that the docstring that pops up from the tool tip seems to be affected by the priority. For example, in the tests, if you however over by rfl in the example that uses the refl attribute, it will show the docstring from Lean 4 and not the docstring for the tactic I wrote. Is there a way to also set the priority of the docstring?

[Mario Carneiro]

Yes, that's intentional. It's not priority based, it's just the docs on the syntax declaration that are being shown, which should incorporate elements of all the elab_rules associated to that syntax

[Mario Carneiro]

which makes things a bit awkward for something like a mathlib extension of a core tactic

[Mario Carneiro]

it might be possible to overwrite the doc string on the original syntax?

[Mario Carneiro]

Nope, it panics if you call addDocString on a declaration from another module

[Newell Jensen]

I mean, its not a big deal, at least IMHO, since the docstring from Lean 4 is valid as well so.... just wanted to bring your attention to it in case you felt like it should be changed somehow.

[Mario Carneiro]

yeah, the easiest way to address the problem is to make the docstring of the core tactic vague enough to apply to your version as well

[Newell Jensen]

Its just the docstring for macro "rfl" : tactic => `(eq_refl) that shows up, so unless you think we should change that, won't pay it anymore mind. The only suggestion that I would have is that we could change that dosctring so it doesn't mention the extensibility, i.e. the second sentence, and extract that to sit in a non-docstring comment.

[Mario Carneiro]

The docstring there is the main docstring for rfl

[Mario Carneiro]

it's probably a bit misleading that it's written using the macro command since it's supposed to be only the first of multiple implementations

[Mario Carneiro]

why wouldn't we mention the extensibility? That's an important piece of information for readers, especially if they are looking at a definition that says only macro "rfl" : tactic => `(eq_refl)

[Newell Jensen]

I don't know where all the docstrings show up within the ecosystem so that suggestion could definitely be misplaced. I was only viewing it from a tooltip perspective. Where are all the places that the docstrings show up?

[Mario Carneiro]

The tooltip shows the documentation on the syntax "rfl" declaration

[Mario Carneiro]

so if you have

/-- doc 1 -/
syntax "foo" : term
/-- doc 2 -/
macro_rules | `(foo) => ...
/-- doc 3 -/
elab_rules | `(foo) => ...

then you will see only doc 1 in the tooltip

[Mario Carneiro]

doc 2 and doc 3 are more code-reading focused documentation

[Mario Carneiro]

doc 1 should summarize all the macro_rules and elab_rules that will be declared for it because it's the user-facing documentation

[Newell Jensen]

Mario Carneiro said:

doc 1 should summarize all the macro_rules and elab_rules that will be declared for it because it's the user-facing documentation

If I am following you correctly then this would imply that I would need to create a branch in Lean 4 to update this doc 1, correct?

[Mario Carneiro]

yes

[Mario Carneiro]

but lean 4 welcomes documentation improvements so I don't think this would be a major problem

[Newell Jensen]

@Mario Carneiro I see that you are trying to merge the rfl branch before the one that was stubbed out with some code from Siddhartha. It might be too late and not a big deal since the one has the code from the other.

[Mario Carneiro]

I removed that part

[Newell Jensen]

Yeah just saw that

[Newell Jensen]

Cool, will start looking at next tactic I should take on...thanks for the help.

[Mario Carneiro]

The original implementation wasn't great, and I don't think it's needed here anyway since you are already checking that the two sides are defeq

[Mario Carneiro]

@Newell Jensen A procedural note: you should make PRs originating in the mathlib4 repo itself, from a branch you create to master, or else the CI won't run on it

[Newell Jensen]

What did I do (just to be clear where my error was)?

[Mario Carneiro]

You PR'd from your fork of mathlib4

[Mario Carneiro]

the mathlib4 CI doesn't run on forks

[Newell Jensen]

Ah okay, so used to doing it from forks didn't realize that I needed to just do it directly to the repo. mathlib4 seems unique in this regard (compared to lean 4 etc)

[Mario Carneiro]

it's the same procedure used in mathlib repo, but yes it is a bit unique compared to most github projects

[Newell Jensen]

We don't need mathlib4#425 then now correct?