Tactic status?

Stream: mathlib4

[Yury G. Kudryashov]

Hi, is there any page where I can see which mathlib tactics were ported to Lean 4? E.g., do we already have rcases/rintro?

[Mac]

You can also go look at https://github.com/leanprover-community/mathlib4/tree/master/Mathlib/Tactic (for the manual port -- which is, as I understand it, were the ported tactics go).

[Yury G. Kudryashov]

It would be nice to have a table with status (not started, NN is working on it, ported).

[Yury G. Kudryashov]

I think about trying to write some Lean 4 meta code, and I don't want to work on something that is being ported by a pro.

[Mario Carneiro]

My guess is that no one is working on rcases at the moment

[Mario Carneiro]

I would suggest copying the syntax from https://github.com/leanprover/mathport/blob/master/Lib/Mathport/Prelude/Syntax.lean when you want to start working on a new tactic

[Yury G. Kudryashov]

Which part of this file?

[Yury G. Kudryashov]

I'm going to finish docs for my Stokes' thm PR, then try to port a tactic. May be, I'll start with choose because it has a simpler syntax.

[Mario Carneiro]

For example, if you want to port rcases, you should look for syntax "rcases" ... : tactic

[Mario Carneiro]

rcases is more complicated than some others since it defines a syntax class for rcases patterns, but the grammar is here

[Mario Carneiro]

So to make this into an actual tactic, you would accompany that syntax with an elab that determines how the tactic behaves

[Mario Carneiro]

For simple tactics or those with a simple desugaring you can instead make it a macro and provide the tactic it expands into

[Yury G. Kudryashov]

I'll come back and ask more questions in a few days.

[Jakob von Raumer]

Yury G. Kudryashov said:

It would be nice to have a table with status (not started, NN is working on it, ported).

In favour of this. I'd also be willing to tackle porting a few tactics, but we need to make sure, we're all choosing the same one

[Mario Carneiro]

I would say, for now just post here if you want to claim a tactic. As long as it's not a huge tactic, there probably won't be a huge gap before the PR shows up and/or lands in mathlib4

[Sebastian Ullrich]

Or (for non-trivial ones) open an issue when starting and close it with the PR when finished?

[Jakob von Raumer]

FWIW I started looking at rcases today :triangular_flag:

[Jakob von Raumer]

Probably best to introduce a new syntax category for the patterns and them parse them into what in Lean 3 is rcases_pat....

[Mario Carneiro]

@Jakob von Raumer Like I said above, I would recommend basing your tactic on the syntax defined in mathport here

[Jakob von Raumer]

Probably some things can be simplified. Flattening the patterns can be done by macros, and I think we don't need to do the thing with get_local_and_type anymore, since cases gives us an FVarSubst

[Arthur Paulino]

Is there a source material on how to write tactics for Mathlib4?

[Mario Carneiro]

not really, but thanks for volunteering to write the docs :P

[Arthur Paulino]

Which docs? The docstrings for the tactics we currently have?

[Arthur Paulino]

Or are you talking about these TODOs? https://leanprover.github.io/lean4/doc/tactics.html

[Mario Carneiro]

I mean the lean 4 metaprogramming tutorial

[Mario Carneiro]

that doesn't exist

[Mario Carneiro]

It's about half syntax/macro stuff and half Elab and MetaM stuff

[Arthur Paulino]

I mean, I would if I could, but I don't think I'm quite there yet (that's why I asked for some material to get started :rofl:)

[Mario Carneiro]

I can try to answer questions if you have any

[Arthur Paulino]

I have some shallow experience with Elab and MetaM and almost zero experience with syntax/macro. I'm willing to engage with these matters because I want to learn, but it will take quite a while before I'm able to organize the subject in a didactic way focused on tactic writing

[Mario Carneiro]

the syntax/macro part is tactic writing in easy mode

[Mario Carneiro]

for a simple but not completely trivial example of a macro tactic, see iterate

[Mario Carneiro]

for a completely trivial example see rfl

[Mario Carneiro]

(actually that one is slightly more than it seems because there is also a definition of rfl in core, and when you use rfl in a tactic proof it will try both versions)

[Arthur Paulino]

I was looking at that file earlier and I got lost because there seem to exist many ways to define a tactic.
syntax, macro_rules, macro and elab

[Arthur Paulino]

It was a bit overwhelming because they're all unfamiliar to me

[Mario Carneiro]

• syntax declares the syntax of a tactic. If you do this then it will parse in a tactic block but you will get an error saying that it is unimplemented
• macro_rules pattern matches on a syntax object for your tactic application, binding the arguments and doing something with them. This defines a macro tactic, and the idea is that the rhs of the pattern is another tactic or tactic sequence with your arguments interpolated in.
• macro is a shorthand for declaring a syntax and a macro_rules, in the special case that there is only one macro_rules match branch. The syntax looks mostly like syntax on the left side, except you name the arguments, and then the right hand side is a tactic quotation like in macro_rules.
• elab and elab_rules are similar to macro and macro_rules, but they are for defining elaborator tactics. These are used for more heavyweight or primitive tactics that are not simply sugar for another tactic expression. The left hand side is the same as macro and macro_rules respectively but the right hand side is now a TacticM Unit and you can call lean internals to get the goal, call MetaM functions and so on.

[Arthur Paulino]

Wow, thank you very much for the explanations! I am going to study these in the upcoming weeks

[Arthur Paulino]

I have so many questions I don't even know where to start. I'm gonna dig some more and let the information sink deeper.
I do have one comment though:

`iterate n { ... }` runs the tactic block exactly `n` times.
`iterate { ... }` runs the tactic block repeatedly until failure.

The brackets are a bit confusing because one may think they're part of the syntax

[Mario Carneiro]

The brackets are part of the syntax

[Mario Carneiro]

That is, those aren't the same brackets as the ones you normally use to group under a subgoal. For instance iterate 1 { skip } will do nothing but iterate 1 { { skip } } will fail if there are any remaining goals

[Mario Carneiro]

and iterate 1 skip is syntactically incorrect

[Mario Carneiro]

@Arthur Paulino

[Bolton Bailey]

Well I would have expected what Arthur expected, one takeaway for me from my experience with metaprogramming was that curly brackets are more than just for grouping. I guess if nothing else, we know that brackets are a bit confusing because one may not know whether they're part of the syntax or not.

[Mario Carneiro]

the basic rule is that { tacs } on its own is the solve1 function, and foo { tacs } or bar expr + bla => { tacs } are syntaxes for passing a tactic sequence to the tactic combinator foo or bar

[Mario Carneiro]

You can make your own interactive tactic accept a block by using an argument of type itactic

[Mario Carneiro]

The most common tactics accepting braced blocks that you are likely to run across in mathlib are all_goals { ... }, any_goals { ... },try { ... } and case : x y z { ... }, as well as repeat { ... } and iterate n { ... }

[Arthur Paulino]

@Mario Carneiro Hm, I suspect something strange is happening here. It works fine without brackets and when I use brackets it's not digging deep enough

example {a : Nat} : a + a + a + a + a = a + (a + (a + (a + a))) := by
  iterate 1 skip -- works
  iterate rw [Nat.add_assoc] -- goals accomplished

example {a : Nat} : a + a + a + a + a = a + (a + (a + (a + a))) := by
  iterate {rw [Nat.add_assoc]} -- unsolved goals

example {a : Nat} : a + a + a + a + a = a + (a + (a + (a + a))) := by
  iterate 3 rw [Nat.add_assoc] -- goals accomplished

example {a : Nat} : a + a + a + a + a = a + (a + (a + (a + a))) := by
  iterate 3 {rw [Nat.add_assoc]} -- unsolved goals

[Gabriel Ebner]

I think Mario was mixing up Lean 3 and Lean 4. I don't think any tactic in Lean 4 requires braces itself. In Lean 4, braces always mean that the goal must be solved by the enclosed tactic.

[Arthur Paulino]

Ah, that makes sense:

example {a : Nat} : a + a + a + a + a = a + (a + (a + (a + a))) := by
  iterate 1 {skip} -- unsolved goals but I didn't want to solve it here anyways
  iterate rw [Nat.add_assoc] -- goals accomplished

[Gabriel Ebner]

The brackets are part of the syntax

No they're not in Lean 4. If you want to iterate multiple tactics, you can enclose them in parentheses like iterate (rw [a]; simp).

[Mario Carneiro]

Oh, yes that was all lean 3 info. I inferred as much from the docstring; if the lean 4 iterate says that then it needs a rewrite

[Arthur Paulino]

I can open a PR soon

[Arthur Paulino]

https://github.com/leanprover-community/mathlib4/pull/173

[Arthur Paulino]

Following up after reading Yakov's interview (I've been with this question in my head for a few days), do we know the most wanted tactics for Mathlib4? I think an accessible/updated list like this could help outsiders jump in and help effectively

[Johan Commelin]

@Mario Carneiro had a list somewhere, I think

[Mario Carneiro]

The list is https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Mathport/Syntax.lean : every syntax in that file is a TODO

[Mario Carneiro]

We talked about having a more organized list, say ordered by difficulty or priority (usefulness for the port), but now I'm second guessing how to provide that information. Should it be a tactic_wishlist.md file separate from Syntax.lean? Or perhaps I could put comments like -- expected difficulty: easy on each of the syntax lines?

[Arthur Paulino]

I think a separate markdown file linked from the main repo README allows more visibility. Then there's also the benefit of tweaking it without needing to change Lean source code

[Arthur Paulino]

https://github.com/leanprover-community/mathlib4/pull/175 getting used to it

[Johan Commelin]

Mario Carneiro said:

The list is https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Mathport/Syntax.lean : every syntax in that file is a TODO

Is a link to this file already posted as an issue somewhere?

[Johan Commelin]

Should there be a github project tracking these?

[Mario Carneiro]

Like I said, I don't really know how to structure the issue. If you want to take a stab at it please post an issue on mathport or add a page on the leanprover community web site, and I will chip in to make the information as accurate as possible

[Mario Carneiro]

Actually I guess I didn't say, I must not have sent that message. It's hard to know what to say about all this stuff

[Kevin Buzzard]

I know nothing about tactic writing so shouldn't really be wading in here but I thought Yakov's suggestion in the community blog post "choose a random file and get it working" was an interesting one. It might be another way of deciding what to work on. I don't know how far we are from getting any file working at this point though. Does logic.basic get autotranslated yet?

[Mario Carneiro]

I've already done "choose a random file and get it working" for maybe 8 mathlib files or so

[Mario Carneiro]

working from the bottom, of course, so no fancy tactics were in use

[Mario Carneiro]

Everything gets autotranslated, it's just a question of how many red squiggles you have to battle. I would guess that logic.basic isn't too bad, except for the fact that it is used for some initial mathlib tactic setup because it is "that one file that literally everything imports"

[Mario Carneiro]

and those tactics might not all be translated

[Mario Carneiro]

like library_note

[Yakov Pechersky]

Your "get a random file working" efforts are exactly what inspired me

[Mario Carneiro]

There is a tension between making the theorems typecheck and preserving the original proofs though. When the file translation is goal directed (as I was), you might be tempted to just get the proofs working by a workaround for the issue of the day, which will later have to be cleaned up

[Yakov Pechersky]

Not to derail the tactic topic -- but if we get a tiny rooted subbranch of some files working in mathlib4, we can suggest future mathlib3 PRs on the corresponding files to also port their PRs on this subbranch in mathlib4. It's not required, but could be a good way of helping surface new issues

[Mario Carneiro]

I think we should strive for preserving the proofs, on the premise that those proofs are the way we want to be able to write proofs, so if lean 4 can't do it then that's a deficiency that we will feel even at t=infinity of the port

[Yakov Pechersky]

People rarely touch logic.basicand the like, and when they do, the changes are tiny -- so maybe they can try to also get them into mathlib4?

[Mario Carneiro]

I don't know about asking a non-self-selected group of contributors to suddenly get involved in lean 4 porting

[Gabriel Ebner]

Also the current version of Logic.Basic in mathlib4 is not very close to mathlib both content and style-wise.

[Gabriel Ebner]

I think we should strive for preserving the proofs, on the premise that those proofs are the way we want to be able to write proofs

I disagree on the premise. Mathlib proofs are 50% writing what you mean, and 50% making Lean happy. Preserving obtain/have/etc. is certainly high priority, but spending effort on preserving dsimp; simp is imho wasted.

[Johan Commelin]

Mario Carneiro said:

The list is https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Mathport/Syntax.lean : every syntax in that file is a TODO

Is this file maintained manually, or generated/updated by some of the porting tools?

[Mario Carneiro]

maintained manually

[Gabriel Ebner]

So when you see new tactics being added to mathlib, feel free to PR the syntax to mathlib4 (we also need to adapt mathport after that).

[Mario Carneiro]

Hopefully we can use judgment to determine what part of mathlib proofs are not preservation-worthy. But I want to avoid this becoming a sour grapes argument where we get rid of stuff that is genuinely useful because we don't want to support it

[Arthur Paulino]

@Gabriel Ebner said:

I believe this function is called List.splitAt and is already in mathlib4.

Indeed it's under Data/List/Defs.lean, but when I import it a lot of things tick red, so I'm not sure how to make use of it

[Gabriel Ebner]

That's because the extra import created a cyclic dependency. I would split up the Tactic/Basic.lean file, it's too large anyhow.

[Arthur Paulino]

Mario Carneiro said:

I don't know about asking a non-self-selected group of contributors to suddenly get involved in lean 4 porting

Do you think something like a Google forms might help on getting a read on the community about this? Maybe there people interested in helping out but don't know how and don't want to bother with questions (just an exemplary hypothesis)

[František Silváši]

There are absolutely people like that. I've only checked the stream due to Kevin's comment in a 'Lean4' topic. I rarely use mathlib due to the nature of the stuff I do with Lean (so it hasn't really occurred to me to check what's being done wrt. mathlib port), but 'porting the community over to Lean4' faster is valuable :).

[Arthur Paulino]

Question: in Lean 3 we could have an argument like this: (l : parse pexpr_list_or_texpr) which would allow the user to enter an expression or a list of expressions and in the tactic definition we'd access it as a list. Is it still possible with Lean 4? I noticed that rw and simp, for instance, seem to always require a list of expressions like rw [myTheorem] and rw myTheorem doesn't work anymore

[Mario Carneiro]

Yes, it's possible, that change was deliberate to make the syntax more regular

[Mario Carneiro]

note that lean 3 simp also does not accept a single lemma without brackets, only rw

[Arthur Paulino]

Mario Carneiro said:

Yes, it's possible, that change was deliberate to make the syntax more regular

Is this the new Mathlib4 standard?

[Mario Carneiro]

It was a lean 4 core decision

[Mario Carneiro]

these tactics are defined in core

[Arthur Paulino]

But I mean, is this style encouraged in Mathlib4 tactics as well?

[Mario Carneiro]

I tried to keep a syntax consistent with lean 4 core tactics when possible, because users shouldn't have to worry about whether the tactic was defined in mathlib or core to guess the syntax

[Mario Carneiro]

The reason that lean 3 simp couldn't take an unbracketed expression was because it did not work with the config argument, which has the syntax simp [th1, th2] cfg

[Mario Carneiro]

I think if you let it parse an expression at the position of the brackets it will try interpreting [th1, th2] cfg as an expression (applying a list of terms to another term)

[Mario Carneiro]

this isn't an issue for rw because it doesn't have a cfg argument

[Arthur Paulino]

Got it. While I like a more regular syntax, I also miss writing rw e

[Mario Carneiro]

In lean 4, the cfg argument has moved to the start and has a different syntax, simp (config := cfg) [th1, th2] so this isn't a concern anymore

[Mario Carneiro]

I wouldn't be opposed to changing it but you should take it up with leo

[Mario Carneiro]

mathlib will follow whatever lean 4 core does here

[Arthur Paulino]

i'm a very green Lean user so I'd rather see what more senior users think first

[Arthur Paulino]

I'm gonna try writing simp_rw for Mathlib4 as my first 100% authorial tactic port

[Mario Carneiro]

You shouldn't have to worry about syntax decisions for tactic porting since the work is already done in https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Mathport/Syntax.lean:

syntax (name := simpRw) "simp_rw " rwRuleSeq (ppSpace location)? : tactic

[Johan Commelin]

Mario Carneiro said:

this isn't an issue for rw because it doesn't have a cfg argument

But you can provide some sort of cfg, right? What with the { occs := ... }?

[Mario Carneiro]

Oh that's a good point. I just tested and by rw [th] {} parses as you would expect while by rw th {} tries to apply {} to th, which seems reasonable. Now I'm curious what would happen if we just tried the same thing for simp

[Arthur Paulino]

https://github.com/leanprover-community/mathlib4/pull/178

[Arthur Paulino]

I couldn't figure out how to deal with rwRuleSeq when trying to port simp_rw so I ported other tactics instead.
Guidance on how to mimic this behavior is appreciated :+1:

[Mario Carneiro]

do you have a WIP that I can play with?

[Arthur Paulino]

Nope... I didn't go much further than defining an elab and getting stuck in the first line of code :sweat_smile:

[Mario Carneiro]

The hard part seems to be getting the positional goal state display right. Otherwise it looks like this can be implemented as a macro tactic

macro (name := simpRw) "simp_rw " rws:rwRuleSeq loc:(ppSpace location)? : tactic => do
  let loc := loc.getOptional?
  let stx ← rws[1].getSepArgs.mapM fun
    | `(rwRule| $e:term) => `(tactic| simp%$e only [$e:term] $(loc)?)
    | `(rwRule| ←%$tk $e:term) => `(tactic| simp%$tk only [← $e:term] $(loc)?)
    | _ => Macro.throwUnsupported
  `(tactic| ($[$stx]*))

[Arthur Paulino]

(deleted)

[Arthur Paulino]

@Mario Carneiro let me know if you really think we should enhance swap and rotate with that idea of yours at this point

[Mario Carneiro]

I don't see any reason not to, I can help you with the implementation if you like

[Arthur Paulino]

My only point of doubt is making the optional <- argument

[Mario Carneiro]

Quick poll: should the syntax for moving the nth-to-last goal to the front be called swap <- n or swap -n? Ditto for rotate <- n vs rotate -n for rotating left instead of the default right

[Jeremy Avigad]

-n seems more natural to me.

[Arthur Paulino]

actually -n is faster so i'm changing my mind

[Arthur Paulino]

(but I still would like to know how to make the optional <- parameter for the syntax)

[Mario Carneiro]

To parse this, you would do syntax "rotate" "-"? num : tactic

[Arthur Paulino]

wait, so rotate -1 and rotate - 1 would have the same behavior?

[Mario Carneiro]

with possible ppSpace in there to make things print nicely

[Mario Carneiro]

yes

[Mario Carneiro]

num doesn't accept negatives IIRC

[Mario Carneiro]

if that's what you're worried about

[Arthur Paulino]

I was hoping it would accept negatives

[Mario Carneiro]

that is, I don't think "negative literals" are a thing

[Mario Carneiro]

num is basically the [0-9]+ regex

[Arthur Paulino]

i'll do the adjustments tomorrow :+1:

[Mario Carneiro]

(not really, there are other base inputs but you get the idea)

[Arthur Paulino]

what about the left arrow? how to get that in the syntax?

[Arthur Paulino]

(just so I can learn)

[Mac]

Mario Carneiro said:

num is basically the [0-9]+ regex

Fyi, its not just decimal numbers, it also includes hex, octal, and binary.

[Mario Carneiro]

that was the parenthetical

[Mario Carneiro]

Arthur Paulino said:

what about the left arrow? how to get that in the syntax?

just replace "-" with "←"

[Mario Carneiro]

or ("←" <|> "<-") for the ascii artists

[Mario Carneiro]

or ("-" <|> "←" <|> "<-") if you want to be indecisive

[Arthur Paulino]

This one is in Syntax.lean but seems to be already implemented:
syntax (name := ext) "ext" (ppSpace ident)? : attr

[Mario Carneiro]

Ah, that's true, ext in lean 4 core is most similar to lean 3 funext, so you will have to rename the mathlib ext tactic to ext'

[Mario Carneiro]

actually scratch that, the syntax you wrote isn't the syntax for ext

[Mario Carneiro]

I think what happened is that someone implemented a basic form of ext but the syntax doesn't match the full mathlib ext grammar so the original syntax was kept in the Syntax.lean file for mathport to use

[Arthur Paulino]

Ah, okay

[Mario Carneiro]

I think the first thing to do is to make mathlib4 ext use the Syntax.lean grammar without implementing the extra bells and whistles just yet

[Mario Carneiro]

just fail if the input isn't an ident

[Mario Carneiro]

although that's also going to involve rcases since mathlib ext uses rcases patterns

[Arthur Paulino]

I'm trying to pick the ones with a good trade-off between learning and difficulty

[Mario Carneiro]

I will look into rcases myself, it's one of the more complicated ones. You shouldn't have to interact with it beyond the syntax, which I guess is already extracted into a file in mathlib4

[Arthur Paulino]

I'm going to try set next

[Arthur Paulino]

Forgot to say that simp_rw is ready for review: https://github.com/leanprover-community/mathlib4/pull/180

[Arthur Paulino]

Mario Carneiro said:

Yes, it's possible, that change was deliberate to make the syntax more regular

So, I'm implementing use and I'm sitting in front of this question again. In mathlib one can do use e or use [e1, e2, ...]. Are we going to restrict the syntax to use [...]?

[Arthur Paulino]

(BTW I'm not asking Mario specifically so everyone's input is welcome)

[Reid Barton]

Probably unrelated to the argument syntax, but on the topic of use, I hope the error handling can be improved over the Lean 3 version

[Ruben Van de Velde]

Hmm, based on a quick grep, use e seems to be used maybe 5 times as often as use [..] (very rough count, because "use" occurs a lot on comments as well). While talking about the syntax, often when I use use [..], I end up rewriting it as refine ⟨..⟩ and the difference in braces is a minor annoyance. Maybe use could use ⟨..⟩as well?

[Eric Rodriguez]

yeah, I really don't know why we have use when compared to refine. we could make use \<a,b,c\> be a shortcut for refine \<a,b,c,_,_...\>, which I'd be in favour of

[Damiano Testa]

I'm not sure, but I think that use does some form of refl, besides what is achieved by refine ..., but, honestly, this something that I only observed rarely.

[Gabriel Ebner]

I think a lot of the unpredictability of use (and bad error messages) is because it is not equivalent to that refine. The following two examples both work:

import tactic
example : ∃ x : string × string, x.1 = x.2 := by use ["a", "a"]
example : ∃ x : string × string, x.1 = x.2 := by use [("a", "a")]

[Gabriel Ebner]

(Originally I wanted to use ℕ instead of string, but that shows a different behavior since 0 coerces to ℕ × ℕ)

[Reid Barton]

I have the impression that the poor error handling of use is related to this flexibility, but I don't have a good understanding of the situation because I found it was easier to just use refine all the time

[Reid Barton]

Oh wow I never realized that use would try to recurse into the "left" side like that. That does make more sense now.

[Kevin Buzzard]

use was written after me and possibly others complained that mathematician users wanted a simple tactic to make progress on \exists goals which was better than existsi, which would for example barf on existsi 0 if the goal was \exists (r : real), .... It's a great beginner tactic for people who aren't ready to start partially solving goals with refine and who have no concept of constructors for inductive types

[Gabriel Ebner]

That seems reasonable enough, but I don't know where the "∃ (x : α × β), ... should take either one or two arguments depending on what works" behavior came from.

[Arthur Paulino]

To me, if I'm trying to prove ∃ (x : α × β), ..., I'd expect use to accept something like (a, b). use [a, b] seems a bit odd to me

[Rob Lewis]

This feature of use was requested by Mario way back in #486 and added in #497

[Rob Lewis]

(Remember when tactic docs lived in tactics.md?)

[Mario Carneiro]

what, I can't believe I suggested that

[Rob Lewis]

"Requested" might be a strong word, to be fair

[Arthur Paulino]

So that makes it two questions:

• Do we want to restrict the syntax to use [...]?
• Do we want use to keep that "Prod-destructing" behavior?

[Arthur Paulino]

While we don't have those answers, here goes use in its simplest form:
https://github.com/leanprover-community/mathlib4/pull/184

[Arthur Paulino]

An update on my tactics porting effort: I've looked through the remaining tactics and I noticed that they are no longer easy enough for me. And while I'm on a trip visiting my family, I am also waiting for some content from @Jannis Limperg's metaprogramming guide, which I'm sure will be helpful to get more tactics ported to Mathlib4.

Jannis, the scope for the guide ended up pretty big so here's an idea: I wouldn't hesitate to start off a mdbook skeleton and then invite the community to help. I know how big scopes can be daunting to face alone!