Tactic porting assignments

Stream: mathlib4

[Notification Bot]

This topic was moved here from #ICERM22 after party > List of tactic status descriptions by Mario Carneiro.

[Mario Carneiro]

For those just tuning in, this is a thread we generated at the after-party meeting in Providence this past week, which contains a bunch of useful information about who claimed which tactics to port. I hope to keep this thread going so I've moved it to the public #mathlib4 stream, and if you would like to claim a tactic please post about it on this thread to avoid duplicated work. Also post here if you are learning lean 4 metaprogramming and would like me to assign you a tactic to work on.

[Siddhartha Gadgil]

Just wanted to mention that PR https://github.com/leanprover-community/mathlib4/pull/253 has an "awaiting author" label (I am the author) but I believe I have addressed all comments. For https://github.com/leanprover-community/mathlib4/pull/336 I am waiting for reviewers to weigh in on an issue, otherwise things are done from my side.

[Kevin Buzzard]

In mathlib the author just changes the tags themselves when they're ready (maybe it's the same with mathlib4)

[Siddhartha Gadgil]

So I was told, but I don't seem to find a way to remove the label. It may be that it is only maintainers who can add/remove labels, or I am just missing something.

[Siddhartha Gadgil]

Indeed Github documentation says: "Anyone with triage access to a repository can apply and dismiss labels." I believe I do not have this access.

[Hanting Zhang]

Hello! May I have push access to mathlib4?

[Scott Morrison]

@Siddhartha Gadgil and @Hanting Zhang, I have given you both write access to the mathlib4 repository, so you can open branches and modify labels on PRs.

[Siddhartha Gadgil]

Thanks a lot

[Siddhartha Gadgil]

Don't seem to see the appropriate settings button still. My username is siddhartha-gadgil. @Scott Morrison can you confirm this is the account added?

[Sarah Smith]

@Mario Carneiro @Gabriel Ebner @Leonardo de Moura is this the stream the mathlib mentees should use?

[Moritz Doll]

The videos from the LftCM afterparty are here: https://brown.hosted.panopto.com/Panopto/Pages/Sessions/List.aspx#folderID=%22560ce8fa-8eb7-46e9-9d30-aed70102a92b%22

[Sarah Smith]

@Moritz Doll @Jireh Loreaux @Hanting Zhang @Yevhenii Diomidov @Andrés Goens @Etienne Laurin @Thomas Browning @Nathan Temple @Wrenna Robson here is the Zulip stream we mentioned earlier we can use for mentee/mentor discussions

[Patrick Massot]

Thank you very much to all those people and their mentors! :praise:

[Sarah Smith]

Here is a link to view the recording of our mathlib port mentee session today: https://microsoft-my.sharepoint.com/:v:/p/smithsarah/Ee8R0tMZ86NHlCzbBsZNPIQB5YUUVMOxAxOzYhfYWrKQIQ?e=ZB4j3K

And helpful links that were shared:
https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Mathport/Syntax.lean
https://github.com/arthurpaulino/lean4-metaprogramming-book
https://github.com/leanprover-community/mathlib4#build-instructions
https://leanprover.github.io/lean4/doc/functions.html#syntax-sugar-for-simple-lambda-expressions
https://github.com/leanprover-community/mathlib3port/

And Mario and Gabriel's tips for the next week!

1. install lean4, lake and the whole infrastructure
2. Make sure you can build mathlib 4
3. pick one of the tactics that already exist, read it and try to understand what it does
4. read the metaprogramming book
5. use Zulip stream to communicate and collaborate!
6. we'll do another tactic demo next week!

[Mauricio Collares]

Many thanks for recording these! It's great for those of us who would really like to learn more about it but don't have enough free time to join in just yet.

[Nathan Temple]

Hi All, does anyone have any other directions for building mathlib 4? I'm in VS Code in Windows with Lean 4 installed, but the directions in https://github.com/leanprover-community/mathlib4#build-instructions don't seem to work there.

[Henrik Böving]

What issues are you having

[David Renshaw]

How might I get invited to future such meetings? Do I need to fill out the "mentee sign-up" form?

[Moritz Doll]

yes, this is how we all got invited

[Johan Commelin]

I'm going to simplify wlog in mathlib, so that it will become trivial to port.

[Johan Commelin]

Or at least, I'll make an attempt to do that.

[Gabriel Ebner]

Some of you asked me on Thursday about easy tasks to get started with:

• @Jireh Loreaux : can you please finish mathlib4#318? I've added a failing test case. I think Meta.check is the right function to use here.
• @Moritz Doll: can you please check out mapply? (read through https://github.com/arthurpaulino/lean4-metaprogramming-book/blob/master/md/main/metam.md#metavariable-depth)
• @Nathan Temple: can you please give porting econstructor a try?
• @Wrenna Robson: can you please do infer_auto_param? (If you search mathport, you'll see how this tactic used to be called in Lean 3.)

[Wrenna Robson]

I'll give it a go!

[Evgenia Karunus]

Hi folks! Could you please add me to the list of mentees interested in sessions on tactics (lakesare@gmail.com).
I'll be working on user widgets, but I want to understand the internals of tactics/implement some lean3->lean4 transitions before I start.

[Sarah Smith]

Evgenia Karunus said:

Hi folks! Could you please add me to the list of mentees interested in sessions on tactics (lakesare@gmail.com).
I'll be working on user widgets, but I want to understand the internals of tactics/implement some lean3->lean4 transitions before I start.

Just added you to the meeting Evgenia! Could you fill out the mentee application as well so we have it recorded? thank you :) https://docs.google.com/forms/d/e/1FAIpQLSfMfNqRTUCLcNPRvU6l4Y86H-mhPCS0AXoMmcjQEyXqw9Mhdg/viewform?usp=sf_link

[Wrenna Robson]

@Gabriel Ebner was it apply_auto_param before?

[Mario Carneiro]

yes

[David Renshaw]

Is today's meeting right now or in an hour from now?

[Gabriel Ebner]

It's supposed to be now but it can't get into the teams meeting either.

[Gabriel Ebner]

(deleted)

[Gabriel Ebner]

https://github.com/leanprover/vscode-lean4/issues/76#issuecomment-1146324355

[Sarah Smith]

@Alex J. Best @David Renshaw @Floris van Doorn @Justus Springer @Luca Ferranti @Newell Jensen @Sam van G @Hanting Zhang

[Newell Jensen]

Thanks @Sarah Smith

[Jireh Loreaux]

@Gabriel Ebner I think mathlib4#318 is finished now. I plan to start on porting tactic#contrapose unless you have a different suggestion.

[Gabriel Ebner]

Ok, I think we had a misunderstanding about the failure case. But otherwise looks good.

[Gabriel Ebner]

contrapose is a good choice

[Jireh Loreaux]

Oh I see what you mean. My apologies.

[Moritz Doll]

existsi was really easy, essentially removing the try trivial from use. PR is here mathlib4#405 - I don't remember what you said about the workflow, but I could not push to a non-master branch of mathlib4

[Floris van Doorn]

Btw: I continued my work today on the simps attribute porting on a branch: https://github.com/leanprover-community/mathlib4/blob/simpsAttrImpl/Mathlib/Tactic/Simps.lean (it's still a giant mess)

[Justus Springer]

I'm looking at SolveByElim right now, which is missing a lot of features from the original solve_by_elim in lean 3. Would it be okay if I try to work on that? Tagging @Scott Morrison since he ported the minimal version.

[Justus Springer]

I'm not sure how successful I'm going to be though.

[Scott Morrison]

Yes, that would be great! I'm hoping to restart working on mathlib4 tactics
soon, and this is high on my list.

It's fairly important that we try to follow the same behavior as the
mathlib3 version, as various other tactics, e.g. library search and tidy,
call it internally.

[Sarah Smith]

Hi Mathlib Mentees! Here's the recording from yesterday's meeting, where Gabriel showed another tactic demo. Also, these links have a set expiration for 28 days, so you may want to download it if you want to keep it. I also may upload them to GitHub to keep them around longer? TBD https://microsoft-my.sharepoint.com/:v:/p/smithsarah/EWNtVpOCRARBh0vHxCExYwUBGc8avQQMahrcQtsEDY6vOw?e=fYkDOQ

[Evgenia Karunus]

Uploading these to youtube could be good too?

[Moritz Doll]

Hereby, I claim dsimp and guardLHS for conv.

[Alex J. Best]

I was looking at generalize_proofs :wave:

[Etienne Laurin]

Hi! I took a look at abstract, there's a dozen uses of it in mathlib3, but only one with an id and some places it is just used as a fancy dsimp. The others are for performance I think, I'm not sure those are still needed in lean4.

[Johan Commelin]

Does

namespace Lean /- MOVE THIS -/

namespace MVarId

/-- `asserts g l` asserts all the tuples in `l`,
where `l` is a list of tuples of the form `(name, type, val)`.
It returns the resulting goal.

The first element in the list `l` will be asserted first,
and the last element in the list `l` will be asserted last.
In particular, the last element will correspond to the outmost lambda
in the goal that is returned. -/
def asserts (g : MVarId) : List (Name × Expr × Expr) → MetaM MVarId
| [] => pure g
| ((n, ty, val) :: l) => do
  let g₁ ← g.assert n ty val
  asserts g₁ l

end MVarId

end Lean

already exist? If not, where should I put it?

[Mario Carneiro]

You can put it in mathlib for now

[Johan Commelin]

And where in mathlib?

[Arthur Paulino]

Sorry for this ultra late reply. I think this is a suitable place:
https://github.com/leanprover-community/mathlib4/tree/master/Mathlib/Util

[Sarah Smith]

@mathlib mentees this week we're asking mentees to choose a tactic and try out porting it yourself! :computer: message here which one you're working on so there's not duplicate efforts, and next week we'll all share how it's going! :smile:

[Evgenia Karunus]

I'd like to take on the #explode command eventually (in ~2 weeks). Do I understand it right that it's marked as S because it doesn't directly prevent the port, but we would still like it in Mathlib 4?
And would you advise I take a more straightforward/tested tactic marked with E before I start with #explode?

[Mario Carneiro]

The #explode tactic is marked S like all other # commands because they are intended for temporary use only and hence they won't appear in a final product library like mathlib. But that doesn't mean they aren't useful, only that they aren't needed for the port. All the tactics, including the S ones, are on the todo list for mathlib 4

[Mario Carneiro]

I would classify #explode as being on the larger end of Medium size

[Mario Carneiro]

but I think there might be some bikeshedding on the UI design aspects, which could make it more complicated

[Mario Carneiro]

mathlib4 has #explode_widget as well for doing the same thing in the widget view; we probably want something closer to that

[Mario Carneiro]

For an easy tactic, what about the documentation commands copy_doc_string, add_tactic_doc, add_decl_doc? I think the last one has already been implemented in core, so you just have to check that the behavior is sufficient and then PR to remove it from the list

[Evgenia Karunus]

Aha, then I'll start with copy_doc_string, add_tactic_doc, add_decl_doc commands; and look into #explode once I'm done with these.

[Newell Jensen]

I could start looking at one of apply, fapply, eapply, apply_with, mapply, rfl, symm, trans, fsplit if nobody else has picked any of these (didn't see any PRs on mathlib4 gh) also in the next couple weeks. My main problem is I am having too much fun playing with learning Lean 3 that I haven't spent anytime, apart from watching Rob's metaprogramming youtube series, on tactics.

[Moritz Doll]

symm and trans are taken: mathlib4#253

[Mario Carneiro]

the plan with the group of primed tactics is to deal with the problem upstream and make them unnecessary

[Mario Carneiro]

I would like a version of lean 3 refl though (now rfl)

[Newell Jensen]

I really don't have a preference since I am new to this and any low hanging fruit to get the ball rolling is probably the best thing. I don't mind if I am assigned one.

[Newell Jensen]

@Mario Carneiro so feel free to assign me something if you wish ;)

[Mario Carneiro]

well, you said rfl and we don't have that one yet, at least not like the lean 3 one

[Mario Carneiro]

so have at it

[Newell Jensen]

Sounds good, watching the mentor session vids now to get up to speed.

[Newell Jensen]

Mario Carneiro said:

I would like a version of lean 3 refl though (now rfl)

So this new tactic will be called rfl, the same name as what is used in term mode?

[Mario Carneiro]

yes, the tactic already exists but it only does apply rfl instead of applying any reflexivity theorem tagged with @[refl]

[Newell Jensen]

Did we want to call the tactic rfl in lean 4 rather than refl as we have in lean 3 (is what I was alluding to)? refl is a short version of reflexivity and didn't know if we wanted to create the new tactic in lean 4 in a similar manner that lean 3 does it.

[Mario Carneiro]

it's called rfl now

[Wrenna Robson]

I am sorry that I've not had time as I hoped in the last couple weeks. What's the best way to catch up/what ports are open to do?

[Moritz Doll]

@Anatole Dedecker are you still working on filter_upwards?

[Anatole Dedecker]

Sorry, I completely forgot to open a PR at the end of the second week at Providence. It is basically ready but I may need to update it and then open the PR. Btw I think I announced that I would work on zify but it never went further than just thinking about it so if it’s not already done anyone should feel free to work on it

[Sarah Smith]

Wrenna Robson said:

I am sorry that I've not had time as I hoped in the last couple weeks. What's the best way to catch up/what ports are open to do?

Hi Wrenna, no worries :wave: glad to see you back! Watch/re-watch the demo session links up above if you need, and then claim a tactic from the list https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Mathport/Syntax.lean to start attempting your own port. Try to make sure it's not already claimed by someone else, so search if there's already an open PR on the tactic or if someone's staked claim here in this topic stream

[Johan Commelin]

FYI: @Scott Morrison created

tactic porting tracking issue mathlib4#430

[Wrenna Robson]

@Sarah Smith great, I'll try to catch up

[Scott Morrison]

Re: the tracking issue. I'm planning later today to go through this thread and record "claims" in that issue. So far the information contained in that issue only reflects PRs that exist on github, and some private communication.

[Scott Morrison]

Okay, I think I've now gone through this thread and reflected everything in the issue.

[Scott Morrison]

Of course, in many cases someone will have claimed a tactic and either found it's too difficult, they don't have time, have lost interest, etc. Please don't hesitate to take your name off something if appropriate, no explanation required!!

[Scott Morrison]

@Newell Jensen, @Alex J. Best, @Justus Springer, @Evgenia Karunus, @Anatole Dedecker, @Wrenna Robson, @Alena Gusakov, @Siddharth Bhat, when I was creating the tracking issue I discovered that you didn't have write access to the mathlib4 repository, so I've sent you all invitations.

This should make it easier to make PRs (because you can push non-master branches direct to the repository), and it enables you to edit issues and labels on PRs.

[Moritz Doll]

guard_target for conv is in std4 now, so this can be removed from the list - I had issues building mathlib4 after a lake update, therefore I couldn't PR that myself

Edit: oh, this got edited in already - I guess I should open my email account before replying to stuff in zulip..

[Moritz Doll]

but @Scott Morrison can you give me write-access to mathlib4 as well?

[Scott Morrison]

@Moritz Doll, invitation sent.

[Patrick Massot]

Thank you very much for this work Scott, I think it's very useful!

[Sarah Smith]

hey @Scott Morrison the open issue is awesome, I'll try to help keep it accurate as well. for lines like this with multiple similar tactics listed, I assume your thinking is that it makes sense for them to be worked on as a bundle? field / have_field / apply_field

[Mario Carneiro]

yes

[Thomas Browning]

Could I also have write-access to mathlib4? My github username is tb65536. Thanks!

[Moritz Doll]

Anatole Dedecker said:

Sorry, I completely forgot to open a PR at the end of the second week at Providence. It is basically ready but I may need to update it and then open the PR. Btw I think I announced that I would work on zify but it never went further than just thinking about it so if it’s not already done anyone should feel free to work on it

it doesn't look to bad, so I will try to do it

[Mario Carneiro]

I posted a sorted list of tactic occurrences in mathlib on the github issue to help with prioritization

[Newell Jensen]

Is there any reason that polyrith isn't in the list of tactics to be ported? Curious if @Dhruv Bhatia the original author is thinking to port this to Lean 4 or not. If not, I would like to claim this one.

[Mario Carneiro]

polyrith was added after the list was created. New tactics from mathlib are periodically added to the file; this is what the "modifies-tactic-syntax" mathlib tag on PRs is for

[Luca Ferranti]

sorry for missing yesterday meeting. Looking at the available (easy, since I'm no guru yet) tactics, I could start working on ring, I'll start drafting a PR this weekend. Also can I get write access to mathlib4, my handle is lucaferranti

[Luca Ferranti]

what does "conv mode" mean?

[Johan Commelin]

polyrith will definitely be ported at some point in time. But it isn't a tactic that occurs in mathlib proofs, because it is self-replacing. So it isn't prio 1.

[Moritz Doll]

We do need linear_combination, right? that probably does make sense only if we have ported ring

[Newell Jensen]

Johan Commelin said:

polyrith will definitely be ported at some point in time. But it isn't a tactic that occurs in mathlib proofs, because it is self-replacing. So it isn't prio 1.

Yeah, understood but still want to claim it :grinning_face_with_smiling_eyes:

[Johan Commelin]

But ring is already ported!

[Newell Jensen]

Moritz Doll said:

We do need linear_combination, right? that probably does make sense only if we have ported ring

Yeah there is a list of things needed before hand so obviously need to get those done first.

[Newell Jensen]

Newell Jensen said:

Yeah, understood but still want to claim it :grinning_face_with_smiling_eyes:

Saying this in partial jest, I am mostly just intrigued by the fact that it interfaces with Sage and the possibilities that can have for other things.

[Newell Jensen]

Luca Ferranti said:

what does "conv mode" mean?

conv

[Mario Carneiro]

it's totally okay to pick one of the S tactics to work on, especially if it takes lean in a new direction (these are the N tactics). polyrith is definitely an N tactic

[Jireh Loreaux]

ring is only half-ported though right? Doesn't it only handle semi-rings right now?

[Jireh Loreaux]

I mean, semi-ring manipulations, no negatives.

[Mario Carneiro]

it's semi-ring

[Sarah Smith]

hellooo @mathlib mentees :smile: we were thinking this week it would be fun to do some light pair programming at the meeting. Does anyone want to volunteer to share their screen and show what they've been working on? It's totally ok to go if you're stuck or lost on what to do next (or how to start!!), in fact that's even better for everyone to learn, we want to help! Give a :wave: react here if you want to share on Thursday, or message me if you have questions! :dancing: :dancer: :boom:

[Floris van Doorn]

I just encountered a nice little sub-problem that might be nice to do pair programming on, so I'm happy to volunteer.

[Sarah Smith]

@Thomas Murrills this stream is what the mathlib mentees are using to discuss

[Sarah Smith]

big thanks to @Floris van Doorn and @Newell Jensen for sharing their tactics this week and pair programming in the mentee meeting, so many found it useful to watch! @Andrés Goens you mentioned you're willing to share next week, do we have 1 or 2 more volunteers? There's some brand new mentees so even pair programming a fresh tactic from scratch would be helpful :nerd: :grinning_face_with_smiling_eyes:

[Thomas Murrills]

I’ll volunteer! We’ll see what I can figure out by next week 😁

[Moritz Doll]

Sorry for not showing up, I am very much occupied with other obligations. I hope I'll find some time to start working on zify (how is that pronounced btw? 'zee-fee' or 'zett-i-fei' or something completely different?) on the weekend and hopefully have something presentable for the next meeting.

[Mario Carneiro]

how is that pronounced btw?

it's up to your interpretation :)

[Johan Commelin]

My minds voice always says "ziffy". But I guess it should be zettify or zee-ify (depending on where you live/were born).

[Floris van Doorn]

I read it as "zee-ify". I've lived in the US for too long :P

[Thomas Murrills]

To make it just a tiny bit easier to browse tactics to port, I'd like to edit #430 so that each tactic is prefixed by its difficulty (e.g. [E]) and links to its entry in the mathlib docs. (That way you wouldn't have to look back and forth to Syntax.lean to find the difficulty, and could see if it had been claimed at the same time.)

Would it be ok to give me edit access to that issue somehow so I can do that (or would doing so be a whole thing/involve giving me "too many" permissions)? If so, I'm thorimur on github. :)

[Mario Carneiro]

what's your github handle?

[Thomas Murrills]

thorimur

[Mario Carneiro]

invite sent

[Thomas Murrills]

Ok great, thanks :)

[Thomas Murrills]

Is there a quick automatic way to get the full name of a tactic, either within lean or otherwise? e.g. to produce tactic.interactive.assoc_rw from assoc_rw?

[Mario Carneiro]

yes, prepend tactic.interactive.

[Mario Carneiro]

if you mean lean 3

[Mario Carneiro]

all lean 3 tactics are required to be in that namespace

[Thomas Murrills]

Some of them seem not to be, such as op_induction

[Thomas Murrills]

(among others)

[Thomas Murrills]

Should simp_intro be simp_intros? I can't seem to find simp_intro in mathlib3

[Mario Carneiro]

Ah. Those tactics are special... In lean 3 you are allowed to write elements of the tactic unit monad directly in a by block, and this is sometimes used to call "non-interactive" tactics that can be in any namespace

[Mario Carneiro]

simp_intro is lean 3 simp_intros indeed. I'm taking the opportunity to normalize some of the names

[Mario Carneiro]

Mathport handles the tactic renames / syntactic changes

[Thomas Murrills]

ah okay! so are the snake case strings in Syntax.lean "new" names for lean 4, and not the old lean 3 names?

[Mario Carneiro]

yes

[Thomas Murrills]

cool! is there a list of other normalizations? could be useful in general, I imagine

[Mario Carneiro]

https://github.com/leanprover-community/mathport/blob/master/Mathport/Syntax/Translate/Tactic/Lean3.lean#L424-L431

Here is where you can see the renaming happen: notice that it is spelled simp_intros in the attribute at the top (that's the lean 3 name) and simp_intro in the syntax quotation (that's the lean 4 name)

[Mario Carneiro]

that also handles stuff like: in lean 3 the config argument comes at the end, in lean 4 it comes at the beginning in a (config := ...) wrapper

[Mario Carneiro]

So because we have this syntax transformation tool we have significant latitude to make the lean 4 tactic equivalent more lean-4-ish syntactically

[Thomas Murrills]

Gotcha, neat! I do feel like having a mapping somewhere of lean 3 things to their lean 4 equivalents will be useful outside of mathport as well...e.g. I'm guessing the mathlib3 docs will eventually be updated to point to the corresponding thing in the mathlib4 docs (and vice versa)

[Mario Carneiro]

I don't think we want that to live in the official docs, but an on-the-side cheat sheet would be useful in the mid to late stage of porting

[Thomas Murrills]

Won't people still want to know what the lean 4 correspondent is if they're used to using lean 3? I'm imagining a user who's used to calling something one name in lean 3 and doesn't know what to call it in lean 4

[Thomas Murrills]

While I'm at it, I could also sort this list of tactics by the priorities/occurrences given in the most recent comment, and also split them up by unclaimed, claimed, and finished...does this sound like a good idea?

[Thomas Murrills]

Also, there are three attributes marked as "stub" difficulty but included in the main list—I'm guessing these should be in the stub section instead, right? (intro, interactive, protect_proj)

[Mario Carneiro]

Best not to re-sort them for now. They are in the same order as the Syntax.lean file

[Mario Carneiro]

interactive should actually be removed entirely, we're not planning to port it. protect_proj shouldn't be marked S, we need to handle it but we're not going to do so by implementing it in mathlib4 as the comment indicates

[Mario Carneiro]

intro is an S for now, we may not want to port it at all

[Thomas Murrills]

Gotcha, I'll omit interactive, turn protect_proj into ?-difficulty for now, and move intro to the stub section (unless something different is desired)

[Thomas Murrills]

Just wondering, why is it important that they stay in the same order as the Syntax.lean file? The two things I can imagine are 1) the ability to match up the difficulty (but I'll be including the difficulty next to each entry in the issue, so this won't be necessary) 2) there might be some effect on the Syntax.lean file depending on what happens in the issue. (I notice the stubs are out of order though?)

I wish markdown had sortable tables...then we wouldn't have to choose an order :)

I'll post the edit tomorrow!

[Thomas Murrills]

Ok, posted! In the future, if we do choose to make it a prioritized list, feel free to ping me—it should be pretty easy to sort it with the code I've written to generate the formatting and links.

Also let me know if there are any opinions on the icons/emojis/formatting used for the status and for the difficulty; currently, I just use the letters in Syntax.lean for difficulty, but it would be likewise very easy to change everything systematically, e.g. to some visually distinct emojis.

[Thomas Murrills]

ok, I’m going to try ring1 / ring1! :)

[Mario Carneiro]

This is just a checkup for people who are currently marked as claiming a tactic: Are you still working on the tactic / interested in retaining the claim? If it turned out to be harder than you expected / out of your depth, or you don't have time to work on it, I would recommend not holding on the claim, since it means others won't work on it either which might delay matters. If you have already have some partial progress or are preparing a PR then of course you should keep the claim though. No explanation is required either way, this is just making sure our information is up to date.

Please reply to this message with a :+1: if you are still working on the tactic and :-1: if you would like others to work on it instead (you can follow up with a message if you would like to have something else assigned to you). Reply with :thinking: if you would like to work on someone else's tactic (e.g. you know how you could implement it) and are holding off because of the claim.

[Mario Carneiro]

@Yury G. Kudryashov and @Wrenna Robson , are you still working on infer_auto_param?

[Mario Carneiro]

@Siddharth Bhat, are you still working on try_for?

[Mario Carneiro]

@Alena Gusakov , are you still working on convert / convert_to?

[Mario Carneiro]

@Johan Commelin , are you still working on lift?

[Mario Carneiro]

@Siddharth Bhat , are you still working on tfae_have / tfae_finish?

[Mario Carneiro]

@Scott Morrison , are you still working on apply_fun?

[Mario Carneiro]

@Thomas Browning , are you still working on group?

[Mario Carneiro]

@Anatole Dedecker and @Moritz Doll , are you still working on zify?

[Mario Carneiro]

@Hanting Zhang , are you still working on nth_rw?

[Mario Carneiro]

@Anatole Dedecker , are you still working on filter_upwards?

[Mario Carneiro]

@Siddharth Bhat , are you still working on norm_num / norm_num1 conv mode?

[Mario Carneiro]

@Evgenia Karunus , are you still working on copy_doc_string / add_decl_doc / add_tactic_doc?

[Mario Carneiro]

@Justus Springer , are you still working on solve_by_elim?

[Mario Carneiro]

@Rob Lewis , are you still working on extract_goal?

[Mario Carneiro]

@Alena Gusakov , are you still working on guard_tags?

[Mario Carneiro]

@Evgenia Karunus , are you still working on #explode?

[Wrenna Robson]

No, I'm afraid I've been ill with Covid and then had other commitments. I don't think I'm going to successfully juggle this around my new internship.

[Johan Commelin]

I will release my hold on lift for now. I might return to it in the near future.
The refactor of lift in mathlib3 has been merged. This should make it quite a bit easier to port to mathlib4.

[Mario Carneiro]

Remember, these aren't commitments, it's totally fine to work on other stuff. The purpose of keeping track here is only to avoid duplicated work since a bunch of people are working on a bunch of little tasks.

[Evgenia Karunus]

Mario Carneiro said:

For an easy tactic, what about the documentation commands copy_doc_string, add_tactic_doc, add_decl_doc? I think the last one has already been implemented in core, so you just have to check that the behavior is sufficient and then PR to remove it from the list

What do you mean by the core here, Lean 4 itself? (This commit? https://github.com/leanprover/lean4/commit/2c0de29dfda46e1cf2995cedd3934fe548cd9901#diff-3ce51f25fd5254dcc48457b22dfec73e612f5973c1811f7b60df29b95e2810efL36)
Do some of these tactics belong to Lean 4?

[Mario Carneiro]

yes

[Mario Carneiro]

"lean core" means the lean4 repo

[Mario Carneiro]

It is simpler not to try to work out what should go in core at this point. Most tactics you write here should go in mathlib4, and if they become useful in lean core then they can be migrated to std4 or core later

[Siddharth Bhat]

@Mario Carneiro No, I've abandoned norm_num / norm_mul, tfae_have / tfae_finish, try_for.

[Moritz Doll]

Mario Carneiro said:

Anatole Dedecker and Moritz Doll , are you still working on zify?

I am very sorry, I have been busy with moving. I'll try to find time to make some progress that is presentable (I actually have some questions that I wanted to ask yesterday, but I couldn't make it. I'll ask them in the evening). In case zify and qify are blocking something, someone else should do them, but it seems to me that we will not switch to Lean4 next week.

[Hanting Zhang]

Mario Carneiro said:

Hanting Zhang , are you still working on nth_rw?

I think you said Leo wanted to implement it in core so I dropped it

[Mario Carneiro]

That work is done now: it can be implemented in terms of the pattern (occs := n) conv

[Mario Carneiro]

there is still some work to be done to match the interface of nth_rw so would you like to pick it up again @Hanting Zhang ?

[Hanting Zhang]

No it's ok, someone else can pick it up :smiley:

[Alena Gusakov]

Mario Carneiro said:

Alena Gusakov , are you still working on guard_tags?

So I guess this got lost in the stream but I linked someone else's PR, it looks like they had already done guard_tags so I haven't worked on it since

[Alena Gusakov]

Alena Gusakov said:

Heather Macbeth said:

guard_tags: goal tagging has changed in Lean 4, now more common to see "tagged goals". For example, after an induction. Used for case. So maybe the syntax needs to be one ident rather than a list of idents. Alena Gusakov

I should've checked the PRs sooner. It looks like someone already took care of this: https://github.com/leanprover-community/mathlib4/pull/258

[Scott Morrison]

I've noted that guard_tags is in the PR https://github.com/leanprover-community/mathlib4/pull/258.

[Thomas Murrills]

I'll officially try tauto! Even though it's Big and I'm still just getting started, I feel like I know what it should do abstractly, which makes it a lot more tackleable. However, if anyone else would like to work on it in tandem, let me know—I'm more than open to collaborating! :)

[Jireh Loreaux]

@Mario Carneiro I was looking to start tactic#generalize, but I wanted to ask if you think there will be any particular obstructions to watch for. it's defined here: https://github.com/leanprover-community/lean/blob/283f6ed8083ab4dd7c36300f31816c5cb793f2f7/library/init/meta/interactive.lean#L503 and doesn't look terribly complicated.

[Alex J. Best]

There is already https://github.com/leanprover/lean4/blob/e44fd19074259018b9ddcbdb00209492416bc8ac/src/Lean/Meta/Tactic/Generalize.lean in core btw. But I don't know if it is feature complete with the lean 3 one right now

[Jireh Loreaux]

yes, I just noticed that (and it's not actually on mathport list). I was originally looking at generalizes, but that is used only 2 places.

[Jireh Loreaux]

What about just avoiding porting things (at least for now) that are rarely used by removing occurrences of them in mathlib? For example, if I could get rid of those two generalizes uses, would it be fine to just mark it with an S?

[Alex J. Best]

I've been working under the assumption that that's a productive way to go for some tactics (e.g. #16839).
With generalizes though it seems like it might not be too annoying to understand and implement (as a macro using generalize even?), and I think there are probably a bunch more places in mathlib where it could be used but isn't (grepping for generalize .*\n *generalize finds 5 or so) so probably either would be an ok solution?

[Alex J. Best]

Saying that, I can't even find the two uses you mention, where are they?

[Alex J. Best]

Ok a macro seems too simplistic, so I'm certainly leaning towards the "mark it with S" approach assuming the two uses can be replaced

[Jannis Limperg]

Core generalize now seems to correctly handle multiple generalisations with dependencies between the generalised terms:

example (P : ∀ n, Fin n → Prop) (n : Nat) (f : Fin n) : P n.succ f.succ := by
  generalize hm : n.succ = m, hg : f.succ = g
  /-
    P : (n : Nat) → Fin n → Prop
    n : Nat
    f : Fin n
    m : Nat
    g : Fin m
    hm : Nat.succ n = m
    hg : HEq (Fin.succ f) g
    ⊢ P m g
  -/
  sorry

Support for this sort of thing is why I wrote generalizes back then, so if that's not a concern any more, it shouldn't need porting.

[Jireh Loreaux]

I actually am having trouble finding the two places as well. My count came from Mario's breakdown at the bottom of the tactic portion issue.

[Mario Carneiro]

Jannis Limperg said:

Core generalize now seems to correctly handle multiple generalisations with dependencies between the generalised terms:
Support for this sort of thing is why I wrote generalizes back then, so if that's not a concern any more, it shouldn't need porting.

Well it still "needs porting", but the result of a finding like this is generally that mathport needs to be updated to translate generalizes into generalize , and then the generalizes line can be removed from the syntax file. That's one way to "finish" a tactic

[Mario Carneiro]

(Although with only two uses a backport removal is also an option)

[Mario Carneiro]

The two uses are both false positives: one for a variable named generalizes inside the induction' tactic and one for generalizes' inside the implementation of generalizes (I guess regex end-of-word matching allows quotes, so there are probably many other false positives of the same kind with primed tactics.)

[Jannis Limperg]

(induction' internally uses generalizes, but induction' is also unused in mathlib afair. We use it for the Hitchhiker's Guide and are therefore porting it, but that doesn't need to concern mathport.)

[Evgenia Karunus]

Sarah Smith said:

Here is a link to view the recording of our mathlib port mentee session today: https://microsoft-my.sharepoint.com/:v:/p/smithsarah/Ee8R0tMZ86NHlCzbBsZNPIQB5YUUVMOxAxOzYhfYWrKQIQ?e=ZB4j3K

Uh the link has expired, could someone please share the video with me? (Also - did @Sarah Smith end up uploading them to github?)

[Newell Jensen]

@Evgenia Karunus Uploaded the two I have to my Google Drive. Hope that helps. vids

[Scott Morrison]

We could host these videos on the mathlib youtube channel, presumably as private (i.e. URL required to view) videos.

[Thomas Murrills]

(Sorry I couldn't make it to the current meeting; unfortunately I haven't been feeling too well. Hopefully I'll be there next week :) )

[Newell Jensen]

Claiming apply_normed. I updated the tactic sheet.

[Newell Jensen]

@Mario Carneiro apply_normed is actually in tactic/norm_num.lean within mathlib, so probably should check with you first that you are also not covering this in your current work on norm_num.

[Mario Carneiro]

no that's fine

[Newell Jensen]

@Mario Carneiro any issues with having separate files for this then?

[Mario Carneiro]

you probably want to put it in the same file as well, if there are any conflicts I can clean it up

[Evgenia Karunus]

Do I understand it right that doc_string is defined in C++ in Lean 3, and it's not yet defined in Lean 4?
What's a good approach here, should I copypaste C++ doc_string code from Lean 3 to Lean 4?

[Mario Carneiro]

no, that is a function that returns the doc string on the definition

[Mario Carneiro]

your search isn't finding anything because stuff is camel cased in lean 4

[Mario Carneiro]

and also because github search sucks

[Mario Carneiro]

relevant hits include src4#Lean.addDocString and src4#Lean.findDocString?

[Evgenia Karunus]

Ah! Very nice, thanks.

[Alex J. Best]

Is the mentor session happening today? I can't connect to the meeting it seems, I've been in the waiting room for a few minutes

[David Renshaw]

I hereby claim split_ifs. I hope to put up a PR for it before too long.

[Evgenia Karunus]

@Mario Carneiro, could you please take a look at this PR https://github.com/leanprover-community/mathlib4/pull/494/files:

1. Is there a way to write the elab insides better than I did?
2. What's the appropriate test for this kind of code, I imagine executing copy_doc_string hi → one two, and then checking whether findDocString? env one returns the appropriate docstring? Inside what kind of method would I assert this so that Lean tests validate this automatically?

[Mario Carneiro]

The implementation of the command looks good. To test, you could indeed use findDocString?. Just do something like

#eval show MetaM _ from do
  guard <| findDocString? (<- getEnv) ``one == some "my amazing docstring"
  guard <| findDocString? (<- getEnv) ``two == some "my amazing docstring"

[Mario Carneiro]

On second thought though I think we might not want this command at all, since lean 4 now has the inherit_doc attribute which is used to express this kind of docstring copying. Mathport could translate copy_doc_string hi → one two to attribute [inherit_doc hi] one two

[Mario Carneiro]

although there may be restrictions on whether you can put docstrings on a foreign definition this way

[Evgenia Karunus]

@Mario Carneiro, do I understand it right that the main purpose of add_tactic_doc is setting the tactic_doc attribute to some methods, so that doc-gen can call get_tactic_doc_entries (https://github.com/leanprover-community/doc-gen/blob/master/src/export_json.lean#L453) and generate html docs from those?
So if I port add_tactic_doc to mathlib 4, I'd want to port all accompanying methods used in doc-gen (get_tactic_doc_entries, to_json, to_string)?

[Mario Carneiro]

Yes that would be nice, although hopefully it is not too much work (to_json is just a deriving Json on the struct in all likelihood). You should implement it as an environment extension: look for register*Extension in mathlib4 for examples

[Thomas Murrills]

I'm willing to take a (hopefully short) break from tauto (which so far has been a lot of reading to try to figure out how best to proceed—I want an algorithm I'm sure works!) to try refine_struct and/or pi_instance if no one else would like to try them at this time!

Where did we land on refine_struct? (I seem to remember last week it was mentioned that refine_struct wasn't used, but I can find quite a few occurrences of it in mathlib.)

[Mario Carneiro]

What I said at the last meeting is that refine_struct is not used in isolation, it is always followed by pi_instance_derive_field

[Thomas Murrills]

oops, that is in fact what I meant to say I could find :upside_down: while most are indeed followed by pi_instance_derive_field, a fair number aren’t. though I’m not sure whether the ones that aren’t just as well could be.

[Moritz Doll]

If nobody objects, I would do convert_to and ac_change.

[Scott Morrison]

Hopefully convert_to is quite straightforward: convert is already in. I'd love to have ac_refl, as already we've encountered missing it in porting files.

[Moritz Doll]

For some reason I thought you also did ac_refl..

[Alex J. Best]

There is an ac_rfl in core due to @Daniel Fabian, see https://github.com/leanprover/lean4/blob/c672046767611565b84729db06a7c416625591b4/src/Lean/Meta/Tactic/AC/Main.lean

[Mario Carneiro]

Unfortunately the relationship between that ac_rfl tactic and the mathlib tactic is not clear. We might be able to just check it off the list but we should create test cases and make sure it has the right functionality first.

[Alex J. Best]

Yes it seems there are some problems, or at least a disconnect between docs4#IsAssociative and docs4#Lean.IsAssociative

[Alex J. Best]

Likewise with IsCommutative and IsIdempotent

[Mario Carneiro]

The fix for that is to add an instance [IsAssociative f] : Lean.IsAssociative f

[Alex J. Best]

Sure, my point is that its rather strange that we have two classes doing exactly the same thing

[Alex J. Best]

The instances

instance [h : IsAssociative R op] : Lean.IsAssociative op := {h with}
instance [h : IsCommutative R op] : Lean.IsCommutative op := {h with}
instance [h : IsIdempotent R op] : Lean.IsIdempotent op := {h with}
@[to_additive]
instance [Semigroup R] : IsAssociative R (. * .) := {assoc := mul_assoc}
@[to_additive]
instance [CommSemigroup R] : IsCommutative R (. * .) := {comm := mul_comm}

give me a ac_rfl that works ok with goals in mathlib Rings

[Scott Morrison]

I've put up a PR at mathlib4#526 for the port of linarith.

There are still some remaining issues, but the core functionality, and many tests, are working. Tomorrow I'll write up a TODO list of things that should happen before and/or after merging this PR.

[Daniel Fabian]

the ac_rfl is meant to be part of a much more complex rewriting modulo ac. The way you'd go about it is using an ac normalization, matching in that transformed world and then use ac_rfl to justify your matching. That said, it's quite a lot of work and fairly complex. So far, I didn't get to the matching and rewriting parts, yet. Not least due a change in my personal circumstances that make it hard for me to contribute much code these days. However, ac_rfl is useful in its own right. All you need is to provide a combination of Lean.IsAssociative, Lean.IsCommutative, Lean.IsNeutral and Lean.IsIdempotent and it'll use them to synthesize a proof. The nice thing is that your proof is short, using kernel computation instead of huge proof terms.

If anyone wants a bit of info how it works, just reach out.

(Also I had to add the Lean.IsAssociative, Lean.IsCommutative, Lean.IsNeutral and Lean.IsIdempotent because they are used for ac_rfl and we don't have a mathlib dependecy)

[Alex J. Best]

@Daniel Fabian I'd definitely be interested in having some implementation rewriting modulo AC and would be willing to work on it a bit. Do you have a roadmap or reference you were looking at for that? I found some relevant prior work in Coq, that I think is now https://github.com/coq-community/aac-tactics. Was that the sort of approach you were thinking of or did you have a different design in mind?

[Daniel Fabian]

no, the idea was quite along the quoted paper. In fact we took plenty of inspiration from there. They explain the general idea that you need a matching algorithm, rewriting and then you use ac_rfl to justify your steps.

One thing we do differently from the paper if memory serves, is that we don't deal with multiple operators at once in the kernel, but rather in the meta program. This allows us to have a somewhat simpler theorem (only dealing with one operator at a time) and it allows us to also use ac_rflin types, inside binders, etc.

The next step would then be something that implements ac matching, i.e. find a substitution such that after substituting the terms are identical modulo ac.

And finally, we'll want to do rewriting in the various subexpressions that constituted the match which in turn will have to be justified by a few ac_rfl calls.

[Daniel Fabian]

one design goal here is to never normalize, but rather leave the user term as intact as possible. So we'd only replace the specific subterms that were rewritten, but wouldn't change brackets, orders of things, etc.

[Floris van Doorn]

FYI: I won't be able to make it to the tactic porting session because I'm attending the FLAIM conference ( https://indico.math.cnrs.fr/event/8087/ )

[Scott Morrison]

@Moritz Doll, thanks for doing zify in #517. However for linarith I need the "plumbing" part as well as the "porcelain". Could I tempt you into providing zify_proof from mathlib3 as well?

[Scott Morrison]

(This isn't holding up linarith, but we'll need it to implement the natToInt preprocessor which is essential for linarith working over ℕ.)

[Moritz Doll]

it doesn't look that bad, but I will not have time for that in the next few days.

[Thomas Murrills]

I'm almost finished implementing refine_struct functionality, but just realized I never officially claimed it! I'll also claim pi_instance while I'm at it. :)

[David Renshaw]

I'm looking at solve_by_elim now. I updated the github issue.

[Evgenia Karunus]

add_tactic_doc question: these 3 lines add a declaration (e.g. tactic_doc.hole_command.hi) and add the docstring we derived to that declaration. Is there still a reason you can think of to do this in the Mathlib 4 version if we could use SimplePersistentEnvExtension and just store the declaration & the accompanying docstring in the environment?

[Mario Carneiro]

yes, we should just use an environment extension here.

[Riccardo Brasca]

Can someone who knows how to write tactics have a look at mathlib4#627? I've ported Algebra.Order.Hom.Basic, but at the end there an extension for the positivity tactic, and I don't know anything about metaprogramming. Thanks!

[Yaël Dillies]

Oh I can try having a look.

[Yaël Dillies]

What's the plan for tests? test.positivity can't be ported because it requires a bunch more files, but of course we should have the test before all extensions are ported.

[Jireh Loreaux]

My suggestion: do a partial port of test.positivity with the tests we can do already and leave the rest in a comment saying that they need X theory files ported in order to work.

[Mario Carneiro]

comment out any tactic code for now. Those are handled with a separate PR

[Mario Carneiro]

we port tactics as they become necessary / according to how important they are, not based on when they show up in the import hierarchy

[Mario Carneiro]

also, we already have test.positivity, and half of the tests are indeed commented out. Those serve as indication that we aren't done yet, and PRs that add more extensions uncomment the tests

[Ruben Van de Velde]

Thomas Murrills said:

I'm almost finished implementing refine_struct functionality, but just realized I never officially claimed it! I'll also claim pi_instance while I'm at it. :)

Any news on those? It looks like I'll need them for mathlib4#642

[Thomas Murrills]

Yep! I’m writing docstrings so that the refine_struct functionality can pass linting on the branch thorimur/refine_struct-via-StructInst of mathlib4; it currently works, but there are a couple of syntax/design choices we might want to tweak, then it’ll be done.

I’ll see if I can get the pi_instance functionality done in the next few days!

[Moritz Doll]

Hi, since I finished all my metaprogramming assignments, I want to port another tactic. Is there anything that is nontrivial, but not too big? I was looking at mono and nth_rewrite, but they still seem at bit scary

[Kevin Buzzard]

Presumably cc also looks scary? I only mention it because I just wrote about 15 lines of lean 4 code when porting a file when in lean 3 it just said cc

[Moritz Doll]

cc looks even worse

[Alex J. Best]

I bet you could do nth_rewrite by now!

[Jireh Loreaux]

How about apply_assumption? It came up in a file and I was just going to circumvent it for now.

[David Renshaw]

oh, you could get this testcase of solve_by_elim working: https://github.com/leanprover-community/mathlib4/blob/f017f329a16e78f031a193107cb7fbdb866d0d22/test/SolveByElim.lean#L57-L59

[David Renshaw]

the missing piece is trying symm on assumptions

[David Renshaw]

this is related to apply_assumption

[Moritz Doll]

thanks for the suggestions, I can look into the solve_by_elim issue (and I claim nth_rewrite for now)

[Scott Morrison]

[deleted]

[Moritz Doll]

Jireh Loreaux said:

How about apply_assumption? It came up in a file and I was just going to circumvent it for now.

mathlib4#708 for the trivial version.

[Moritz Doll]

Jireh, if you need any of the additional features right away, please let me know

[Jireh Loreaux]

Thanks! It won't be until tomorrow that I will check it.

[Moritz Doll]

no need to hurry - I have enough metaprogramming projects for now

[Yury G. Kudryashov]

Hi, I ported the non-tactic part of tactic#lift, see mathlib4#723. What should I read about porting tactic code? I forgot (almost) everything we were taught in summer.

[Scott Morrison]

The best places to start are probably reading other tactics in `mathlib4, the Metaprogramming in Lean 4 book (which doesn't actually explain much about tactic-rewriting per-se, it is more about the internals), and there are a handful of videos on the youtube channel.

[Yury G. Kudryashov]

I've noticed that inhabit in Mathlib4 does the Prop/Type cases incorrectly:

theorem tmp (α : Type _) [Nonempty α] (p : Prop) (h : Inhabited α → p) : p := by
  inhabit α
  apply h
  assumption

#print axioms tmp
-- 'tmp' depends on axioms: [Classical.choice]

[Yury G. Kudryashov]

(deleted)

[Yury G. Kudryashov]

(deleted)

[Scott Morrison]

linarith has finally arrived in mathlib4! :-)

[Johan Commelin]

That's a milestone! Great job!

[Patrick Massot]

This is fantastic news!

[Patrick Massot]

Did you find a way to compile it so that we can figure out whether it's faster than in Lean 3?

[Scott Morrison]

No, I don't know how to do this. (I haven't tried.)

[Alex J. Best]

We should also be sure that the implementation doesn't have any subtle performance issues first before comparing, e.g mathlib4#694 or analogous issues may affect linarith still

[Thomas Murrills]

@Ruben Van de Velde Apologies for the delay—I didn't have the time over the past holiday week that I thought I would! I've started working on pi_instance again, and hope to have it done within a few days from now, which should hopefully be a more reliable estimate now that things are back to normal.

[Ruben Van de Velde]

Thanks for letting me know. I'm not blocked on this anymore, though

[Yury G. Kudryashov]

Note that there were some bugs in the Lean3 version of pi_instance.

[Yury G. Kudryashov]

I remember that we had to explicitly provide all data fields to avoid extra ids or something like that in the generated fields.

[Thomas Murrills]

Thanks, I’ll keep an eye out for that! iirc (from what I’ve read of the code/tests) that might actually have come from refine_struct, which is used in pi_instance. so hopefully that issue will be automatically solved since we’re porting refine_struct’s functionality in a different way!

[Yury G. Kudryashov]

AFAIR, in one of the versions the tactic in fact failed to generate data fields, and was recovering them by unification. I don't remember if this was fixed.

[Scott Morrison]

nlinarith has arrived as well now, if anyone would like to abuse it and report failures. :-)

[Sarah Smith]

We have a few high priority tactics :fire: still in need of porting before the end of the year. Is anyone available to jump in and help us out on these remaining items? We would really appreciate it! :star_struck:

1. polyrith, interval cases, slim_check (front end)
2. adding these options to apply_rules:
   a) at the step where newly-created goals are checked against the list of hypotheses, check against a specified list of hypotheses rather than all hypotheses, see
   https://github.com/leanprover-community/mathlib/blob/d032ed1dcb4e8b3fcc07c8fc92e0a7423b732b87/src/tactic/core.lean#L1029
   b) where hypotheses have a natural symmetry (e.g. equality hypotheses), check against the symms of the hypotheses as well as the hypotheses themselves

[Jireh Loreaux]

I could be mistaken, but I don't think polyrith is high priority because it's a self-replacing tactic.

[Heather Macbeth]

"High-priority" here is for a certain definition of priority :) It includes requests that people planning to teach next semester with Lean 4 (including @Rob Lewis and myself) have made.

[Jireh Loreaux]

Aha, gotcha.

[Scott Morrison]

To clarify on the request for apply_rules (2a), the request is to have support for apply_rules only [X, Y, Z], which will not use other local hypotheses. Possibly also support for apply_rules [-X, -Y, Z]to omit particular local hypotheses.

[Kevin Buzzard]

You guys are very brave! I'm teaching next semester with Lean 3 and I'm telling everyone that this will be the last time I'm doing it.

[Scott Morrison]

Re: apply_rules, I am doing a big refactor of solve_by_elim during my interminable plane flights and layovers. I suspect that I can reimplement apply_rules as a thin layer around solve_by_elim with appropriate options, and then we should get the asked-for goodies for free.

[Moritz Doll]

I had the symm feature for solve_by_elim on my list, is that included in your refactor?

[Scott Morrison]

I haven't done it yet.

[Scott Morrison]

But I have another long flight to go. :-)

[Scott Morrison]

However a simultaneous refactor will definitely not work, as I've rewritten most lines by now.

[Scott Morrison]

I'll PR whatever state it is in tomorrow.

[Moritz Doll]

if you want to do it, feel free. if not I will wait until your refactors are done

[Moritz Doll]

I've just stumbled upon @[mono] and I wonder whether we have to port the tactic or aesop can replace it.

[Jannis Limperg]

After a quick look at mono, it seems like Aesop could probably replace terminal mono* calls, but not non-terminal mono calls. ac_mono* would be tricky but maybe doable.

[Frédéric Dupuis]

Is anyone working on porting lift? If not, I could have a go at it.

[Kevin Buzzard]

@Yury G. Kudryashov ?

[Jireh Loreaux]

mathlib4#723 : seems like it's mostly done in case you want to get it to build again.

[Sarah Smith]

(double posting to look for help) positivity and norm_num can now be finished with data.rat.order ported! Is anyone interested in picking these two tactics up? :smile: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/port.20progress/near/317273090

[Heather Macbeth]

Does ring also need some updates, now that data.rat.order is in?

import Mathlib.Data.Rat.Order
import Mathlib.Tactic.Ring

example {u : ℚ} : u / 2 + u / 2 = u := by ring
/-
unsolved goals
u: ℚ
⊢ u / 2 * 2 = u
-/

This worked in mathlib3. cc @Mario Carneiro

[Mario Carneiro]

yes

[Heather Macbeth]

I see that ring imports norm_num. Will the rat functionality for norm_num (i.e. mathlib4#1102) be enough, or is there more work required beyond that?

[Mario Carneiro]

a bit more work is required, because ring has to recognize that u / 2 means 1/2 * u

[Heather Macbeth]

Opened mathlib4#1189 to record this.

[Yury G. Kudryashov]

Jireh Loreaux said:

mathlib4#723 : seems like it's mostly done in case you want to get it to build again.

@Frédéric Dupuis Feel free to adopt the lift tactic.

[Thomas Murrills]

@Sarah Smith reached out to me about porting the remaining norm_num Rat-dependent functionality, and now that I'm a bit more familiar with norm_num, I'm interested in taking it on (mathlib4#1102).

But: is the specific functionality we still need to port outlined anywhere? Are we following mathlib at all? The implementation looks...a bit different. If anyone already knows what specific extensions we need, that would be a great help.

(Or, if part of the task is to figure out new ones for mathlib4 such that all the examples work, I'm happy to try that!)

[Jireh Loreaux]

@Mario Carneiro

[Mario Carneiro]

The main changes are:

• norm_num should be using Rat instead of Int for representing constants
• we need an evaluator for division and inverse

[Yury G. Kudryashov]

I'm trying to port the noncomm_ring tactic. What should I use instead of bit0_mul etc?

[Yury G. Kudryashov]

Also, what's the right syntax for chaining tactics in a macro? I tried

macro (name := noncommRing) "noncomm_ring" : tactic => do
  `(tactic|simp only [-- Expand everything out.
     add_mul, mul_add, sub_eq_add_neg,
     -- Right associate all products.
     mul_assoc,
     -- Expand powers to numerals.
     pow_succ, pow_zero,
     -- Replace multiplication by numerals with `zsmul`.
     bit0_mul, mul_bit0, bit1_mul, mul_bit1, one_mul, mul_one, zero_mul, mul_zero,
     -- Pull `zsmul n` out the front so `abel` can see them.
     mul_smul_comm, smul_mul_assoc,
     -- Pull out negations.
     neg_mul, mul_neg]; abel)

and got

(many lines)
has type
  Lean.TSyntax `tactic.seq : Type
but is expected to have type
  Lean.TSyntax `tactic : Type

[Moritz Doll]

I had this lying around, so your issue seems to be the ;:

macro "noncomm_ring" : tactic =>
  `(tactic|
    simp only [-- Expand everything out.
              add_mul, mul_add, sub_eq_add_neg,
              -- Right associate all products.
              mul_assoc,
              -- Expand powers to numerals.
              --pow_bit0, pow_bit1,
              pow_one,
              -- Replace multiplication by numerals with `zsmul`.
              --bit0_mul, mul_bit0, bit1_mul, mul_bit1,
              one_mul, mul_one, zero_mul, mul_zero,
              -- Pull `zsmul n` out the front so `abel` can see them.
              --mul_smul_comm,
              --smul_mul_assoc,
              -- Pull out negations.
              neg_mul, mul_neg] <;>
              abel )

[Yury G. Kudryashov]

So, now I need to find replacements to bin0_mul etc.

[Yury G. Kudryashov]

Probably, it should match on nat literals.

[Mario Carneiro]

What is the lemma set doing?

[Yury G. Kudryashov]

I meant docs#bit0_mul

[Yury G. Kudryashov]

Basically, for n : Int, we want to replace Int.cast n * x and x * Int.cast n with n • x, and similarly with numerical literals

[Mario Carneiro]

For that we can do it in one go now, by having that exact lemma, plus a version with OfNat.ofNat n * x and OfNat.ofNat n • x

[Johan Commelin]

@porters Is anyone working of the tfae tactic? Because that seems to become urgent now.

[Yury G. Kudryashov]

For now, I use apply_rules [tfae_of_cycle, Chain.cons, Chain.nil] <;> dsimp only [ilast'], then prove implications in the cycle.

[Arien Malec]

added to wiki

[Arien Malec]

What's the general fix for change ... with ...?

I've seen dsimp work...

[Jireh Loreaux]

You might be able to use placeholders, but I haven't checked. For instance, if your goal is ⊢ a = b and c is defeq to a, then in place of change a with c, I think you should be able to do change c = _.

[Yury G. Kudryashov]

About TFAE: I have 2 separate requests (both can be postponed or rejected):

• add support for labels (e.g., by using docs4#AList)
• add support for any partial order, not only Prop.

[Johan Commelin]

Ha, the second one is interesting. Do you have a use case in mind?

[Yury G. Kudryashov]

I don't remember any specific example but I remember that several times I wanted to turn something like a ≤ b ≤ c ≤ a into a = b ∧ b = c.

[Jireh Loreaux]

I've wanted that too. It would be so cool if you could get that out of a calc block, but I imagine it's not possible.

[Reid Barton]

tfae block (the following are equal)?

[Jireh Loreaux]

Yes, I was thinking it could just be a new tfae_calc tactic.

[Thomas Murrills]

I'll be taking a look at tfae_have and tfae_finish :)

[Johan Commelin]

wlog is now ready for porting. the mathlib3 refactor just got merged

[Jireh Loreaux]

Is anyone working on the continuity tactic?

[Jireh Loreaux]

If not, I can try to start working on it, but suggestions on the best way to proceed are welcome.

[Yury G. Kudryashov]

@Heather Macbeth had some ideas in "porting progress".

[Yury G. Kudryashov]

It seems that simp_rw doesn't fail if it doesn't simplify anything on one of the steps.

[Kevin Buzzard]

Same is true of simp. Is there is issue for this?

[Yury G. Kudryashov]

When porting, sometimes a proof breaks because one of the lemmas in a simp_rw sequence doesn't work. It would be nice to see an error where it happens.

[Yury G. Kudryashov]

For me, simp_rw is like rw that can do rewrite under binders etc. In particular, every step must change the goal.

[Heather Macbeth]

Yury G. Kudryashov said:

It seems that simp_rw doesn't fail if it doesn't simplify anything on one of the steps.

This was the case in mathlib3, too!

[Floris van Doorn]

Heather Macbeth said:

Yury G. Kudryashov said:

It seems that simp_rw doesn't fail if it doesn't simplify anything on one of the steps.

This was the case in mathlib3, too!

It wasn't... If one step doesn't simplify, then you'll get the error "simplify tactic failed to simplify".

import data.real.basic

example (x y : ℝ) : x + x = y := by simp_rw [mul_assoc] -- simplify tactic failed to simplify

It unfortunately doesn't specify which of the steps doesn't simplify.
There was one unfortunate behavior it had though, namely that if dsimp only would make progress, then simp_rw [foo] would make progress as well (even if foo was never applied), and then simp_rw wouldn't fail:

import data.real.basic

example (x y : ℝ) : (λ x, x) x + x = y := by simp_rw [mul_assoc] -- succeeds, because it could beta-reduce

[Heather Macbeth]

Thanks for the correction. Indeed, that must have been what I was thinking of.

[Thomas Murrills]

It seems slice(_lhs/_rhs) is blocking some files. Just to double-check, is anyone working on it? If not I’d like to try porting it :)

[Matej Penciak]

I've taken a few stabs at it the last few weeks, but I'm hopelessly confused about how conv-mode tactics work so feel free to take it over (though, if you make any progress or want to talk about it let me know. I'd be happy to help!)

[Thomas Murrills]

Ok, sounds good! :) I'll take a shot at it and I might take you up on that—it'd be nice to talk about it/work together on it if you're down! :)

[Thomas Murrills]

Oh wait, it seems like @Matthew Ballard may have implemented it already? There's a branch but no pull request

[Moritz Doll]

Hereby I claim rsuffices (should be done in a min or so)

[Matthew Ballard]

I hewed fairly closely to the Lean 3 version. I haven't done much testing and I was thinking about ways to make it rely only on an instance of a heterogeneous associativity class but, if people are eager to help push it out the door, let me PR it.

[Matthew Ballard]

!4#2109

[Matthew Ballard]

I have to prep for teaching now so @Thomas Murrills @Matej Penciak please feel free to do as you please.

[Thomas Murrills]

Are there any tactics people are blocked on right now (or expect to be blocked on in a few days)? Or tactics which are consistently missing and would make life easier?

Going by number of uses I was thinking maybe I’d try lift next (alongside enhancements to existing tactics), but I’m not sure what the situation on the ground is, so to speak.

[Matthew Ballard]

I ran into issues with refl (and trans and probably symm) tags. https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Algebra.2EOrder.2EHom.2ERing.20.231482/near/326670322

[Eric Wieser]

rsuffices came up in a PR I looked at recently

[Thomas Murrills]

I think @Moritz Doll has rsuffices! :)

[Thomas Murrills]

Matthew Ballard said:

I ran into issues with refl (and trans and probably symm) tags.

I’ll take a look and see if I can help! But consider me still open for tactic porting requests, since that might be more of a bug fix.

[Moritz Doll]

docs4#rsuffices is already there

[Moritz Doll]

we will need mono sometime soon. If you want to do it that would be great, otherwise I will have a look soonish.

[Thomas Murrills]

Sounds good, I’ll take a look! :)

[Thomas Murrills]

Also, if people have other tactics which will be needed soon, feel free to continue mentioning them—it’ll be useful info to have when the time comes for one of us to port another tactic!

[Jireh Loreaux]

I think @Yury G. Kudryashov already has a PR for lift, but IIRC he was looking for someone to adopt it.

[Kevin Buzzard]

Apparently we have lift now

[Jireh Loreaux]

oh nice!

[Thomas Murrills]

that’s great! I suppose the tactic porting tracking issue is a little out of date—but that shouldn’t be a surprise to me, since I still need to update it with my changes! 😅

[Thomas Murrills]

if I get the chance I’ll try to go through and bring it all up to date. EDIT: done, as far as I could tell! :)

[Thomas Murrills]

I'm finally looking at mono, but I notice there's a basic version already at !4#1740 thanks to @Heather Macbeth! Nice! Heather, do you mind if I polish up that PR by adding appropriate throwUnsupportedSyntaxs? (I think that's all that's holding it up.) Then I'll base the "full" version off of that PR.

[Heather Macbeth]

Thank you, please do!

[Heather Macbeth]

Thomas Murrills said:

Are there any tactics people are blocked on right now (or expect to be blocked on in a few days)? Or tactics which are consistently missing and would make life easier?

I'm a few weeks behind the times, but

• is field_simp still blocked by the issues @David Renshaw was encountering? Or is it done now?
• the fraction functionality of linarith is something people seem consistently surprised to find missing
• for me personally in teaching, I would love to have fixes for any of these three bugs in zify

[David Renshaw]

field_simp has landed and it has worked well for all of the real examples I've tried it on

[David Renshaw]

e.g. https://github.com/dwrensha/math-puzzles-in-lean4/blob/cd83692feb4f6f605ff889a8d0acc9cbcfc17e1f/MathPuzzles/Imo2013Q5.lean#L54
plus also some minif2f stuff

[David Renshaw]

The example in test/FieldSimp.lean is still slow, but less slow than it used to be. https://github.com/leanprover-community/mathlib4/blob/7872193d1e0dcb1ce7393da890d987abbbba5a09/test/FieldSimp.lean#L36

[Thomas Murrills]

Heather Macbeth said:

• the fraction functionality of linarith is something people seem consistently surprised to find missing
• for me personally in teaching, I would love to have fixes for any of these three bugs in zify

I’ll add these to my list and maybe work on a little of each thing in parallel! :)

[Thomas Murrills]

Aforementioned partial port of mono is cleaned up and has a green check: !4#1740

[Thomas Murrills]

It seems like (certain) rational linarith functionality depends on cancel_denoms functionality. (@Mario Carneiro, is that preprocessor section about the whole of it, or is there more?) So, I’ll start on cancel_denoms.

[Moritz Doll]

If nobody is working at it already, I would like to claim congrm. It looks simple enough for a first 'real' tactic.

[Joël Riou]

Anyone interested in porting tactic.elementwise? Basically, lemmas asserting equality of maps f = g in concrete categories like abelian groups are translated into f x = g x for all elements x. (It is needed for category_theory.elementwise, and it shall be necessary for porting many other category theory files).

[Matthew Ballard]

It looks like one can copy the Lean 4 implementation of reassoc excepting the missing reassoc_of.

[Adam Topaz]

IIRC elementwise also converts things like (f \gg g) x to g (f x).

[Matthew Ballard]

I have copy-pasta of Scott's reassoc that does some elementwise things. I've been distracted with the little time I had over the weekend.

[Jeremy Tan]

Joël Riou said:

Anyone interested in porting tactic.elementwise?

If you can guide me at that, yes

[Kyle Miller]

Do you mind if I start porting it right now @Jeremy Tan? I remember there was a universe variable bug in the mathlib3 version of elementwise that would be nice to try to fix.

[Jeremy Tan]

Kyle Miller said:

Do you mind if I start porting it right now Jeremy Tan?

I don't mind, you go

[Matthew Ballard]

I pushed my wip branch for this but it looks like I somehow deleted all the work, :sad:

[Matthew Ballard]

Not much help am I

[Kyle Miller]

mathlib4#2882 has the @[elementwise] attribute and the elementwise_of% h term elaborator

[Kyle Miller]

@Floris van Doorn This is using the attribute application machinery from to_additive -- is using ToAdditive.applyAttributes supported in the case where you want to add the attribute in another module if you originally put simp on it?

I'm asking because this doesn't seem to work to turn off the linter:

set_option linter.existingAttributeWarning false in
attribute [elementwise] Iso.hom_inv_id Iso.inv_hom_id IsIso.hom_inv_id IsIso.inv_hom_id

The Linter.logLint function used in ToAdditive.warnExt doesn't seem to look at the linter option value.

[Floris van Doorn]

ToAdditive.applyAttributes is doing a bunch of things that only makes sense for to_additive, because it's changing its behavior on some attributes. @[reassoc] also uses ToAdditive.applyAttributes, but it's on my to do-list to fix that.
Note also that the semantics of ToAdditive.applyAttributes is to apply the attribute to both src and tgt, which is problematic in your case!?
For the linter issue: I was convinced that Linter.logLint doesn't print anything if the option was turned set to false, but apparently that is not the case. That is good to know, and something I can fix...

[Scott Morrison]

I've updated mathlib4#2882 to factor out the common code from elementwise and reassoc, so they don't accidentally diverge later.

[Thomas Murrills]

mono now has a green check! !4#2323 I’m not putting it out for review just yet, though—there are some documentation strings to write, implementation choices that could still be changed, and, most importantly, tests to perform. A green check doesn’t mean it works correctly just yet! Consider it in beta.

But, if you’re porting a file that uses mono, please merge the mono branch and ping me if something goes awry or simply isn’t as nice as you’d expect! There are several different points at which things could be tweaked, and I expect to be intervening at some of them.