conv% and changes to #conv (and friends)

Stream: mathlib4

[Thomas Murrills]

#12353 introduces conv%, along with simp%, push_neg%, and norm_num% as wrappers around conv%.

It makes two syntax choices which are up for discussion:

1. that the syntax should be conv% e => tac, for consistency with conv (as tactics are always called after the arrow)
2. that simp% and norm_num% with arguments can be written using an optional on if the parser is struggling, e.g. simp% only [lem] on e (on isn’t needed in e.g. simp% e, but can help disambiguate e from the arguments)

This breaks with #conv, #simp, and #norm_num. Note that #conv currently is written as #conv tac => e; #simp uses an optional => as a separator, e.g. #simp only [lem] => e; and #norm_num uses an optional : as a separator, e.g. #norm_num [lem] : e. So, this PR also adjusts that syntax to bring it into consistency with the new elaborator syntax (though it could be split into a separate PR if necessary).

Do people think the choices in (1) and (2) are reasonable?

[Thomas Murrills]

(I’m of course open to other ideas for the token on. In any case, I think => and : are a little “wrong”. While this is ok for a temporary #-command, it seems a bit more important to get the syntax right for term elaborators, which might(?) wind up in committed code.)

[Yaël Dillies]

Thomas Murrills said:

#12353 introduces conv%, along with simp%, push_neg%, and norm_num% as wrappers around conv%.

Do you actually mean that? Isn't one of them #conv?

[Damiano Testa]

Judging from the names, I would guess that ...% is the term elaborator, while #... is the command, right? I think that Thomas is introducing conv% and using it to redefine #conv. Maybe...

[Eric Wieser]

Should it be simp only [...] on% e?

[Eric Wieser]

I worry simp% [x] on y is also parseable as simp% ([x] on y)

[Eric Wieser]

(on is syntactically valid there, but without some weird instances does at least fail to elaborate)

[Thomas Murrills]

Eric Wieser said:

Should it be simp only [...] on% e?

I considered this! I was torn on it. Or more precisely, I considered having tac on% e be a macro for conv% e => tac. I do kind of like that!

However, I was also thinking that it should be possible to add arguments to simp% e without moving around the %. (This isn’t necessarily at odds with having on%, though.)

[Thomas Murrills]

One argument for on% is that it makes more sense (and looks nicer) to simply disallow e.g. simp% <args> (<sep>)? e, and have simp%, norm_num% only as shortcuts for the no-argument case. Then, if someone wants arguments, the docstring instructs them to use on%.