Status of `refine'`

Stream: mathlib4

[Damiano Testa]

Over the last few days, the number of refine' in mathlib decreased from about 11k to approx 600. One of the reasons behind the change is that refine' is considered a "mathlib porting tactic", converted from lean3, rather than "developed natively" in lean 4, like refine.

Regardless, the removals have been almost exclusively obtained by removing the ' and adding some ? in front of the appropriate _. This was an automated process, and there are probably still some of the remaining refine's that could be similarly removed.

If you come across a few of those and feel like you want to PR their replacement with a refine, please feel free to do so! Alternatively/in addition, could you also post here about it, so that I can see whether I can extend the automation to catch these examples as well?

[Michael Rothgang]

Here are 20 more replacements, in Topology: #13383

[Michael Rothgang]

Extremely wild guess: does your script catch proofs in structure fields?
Somehow, many of these still felt "too easy" - I'm not convinced yet the remaining ones all need to stay.)

[Damiano Testa]

Ah, no structures I skipped.

[Michael Rothgang]

Time for another mass-replacement PR :tada:

[Damiano Testa]

Hmmm, some of those are defs, though. I did add defs to the script.

[Michael Rothgang]

Here's another small batch, in Analysis: #13385
Again, about half of them were easy to remove, the other half has to stay for now. Perhaps there's some useful pattern in there.

[Riccardo Brasca]

I've done a couple of them in branch RB/refine. Do you think it is worth do investigate why your script didn't catch those?

[Riccardo Brasca]

(I am merging this in #13385)

[Damiano Testa]

I think that rather than for the specific case of removing refine', I would like to know what I should do to be more thorough in general. I am planning to convert this into a "generic replacement" script, e.g. for deprecations/easy refactors.

[Damiano Testa]

So, the more robust, the better. Catching "all uses of refine' that can be easily replaced by refine" seems like a reasonable robustness bar that I would like to achieve.

[Riccardo Brasca]

I mean, we can do those by hand, it is very quick (the hardest problem is try to do it in the right order to not recompile everything several times).

[Riccardo Brasca]

Maybe we can work folder by folder? I can take for example Mathlib/Algebra

[Damiano Testa]

For the moment, simply gathering data that could trigger the question "if there was a script that scanned for these replacements, why were these not replaced already?" is useful for me.

And these examples are great for that.

[Riccardo Brasca]

What do you think about this commit?

[Riccardo Brasca]

It is an example where something had to be done by hand (replacing rfl by by exact rfl)

[Damiano Testa]

I find this example interesting for the details of how Lean works, but too subtle for the tool. If the tool missed this, I would not think that I should fix the tool!

[Damiano Testa]

However, this replacement should really have been found by the tool

[Riccardo Brasca]

My question was rather if we want to have it in this PR or we prefer to keep this PR for "easy" modification.

[Damiano Testa]

Oh, this is in Archive! I only ran the tool on Mathlib!

[Damiano Testa]

Feel free to keep in that PR: as long as the PR gets merged and does not get side-tracked by questions tangential to the replacement of refine' with refine, I like it! :smile:

[Riccardo Brasca]

I find interesting that refine often does not work with ...closure_induction, for example here refine timeouts, but apply is very fast.

[Damiano Testa]

Getting metavariables right is really hard.

[Michael Rothgang]

Riccardo Brasca said:

I mean, we can do those by hand, it is very quick (the hardest problem is try to do it in the right order to not recompile everything several times).

My personal trick: open n files simultaneously, replace them, wait until they have compiled. Do not save them yet. Then open the next n files and repeat. Choosing n to high will make your computer run hot/bring it to a halt, so you might want to wait sometimes. Works surprisingly well, though.

[Riccardo Brasca]

Ah, nice trick!

[Jeremy Tan]

There are still 268 uses of refine' in 145 files as of my latest commits to the PR

[Ruben Van de Velde]

And probably again that many in open PRs. We'll probably need to do another sweep in a few months anyway

[Andrew Yang]

Maybe we should ban refine' in new PRs?

[Ruben Van de Velde]

I think we already have a linter that disallows certain imports in mathlib. I'd give it some time and then use that

[Mario Carneiro]

refine' is not a mathlibism, it's from core

[Mario Carneiro]

and it is also useful in some circumstances, both when writing proofs and also occasionally in really tricky unification proofs

[Mario Carneiro]

so I don't think it should be banned, a lint which can be overridden is sufficient

[Andrew Yang]

a lint which can be overridden is sufficient

Yeah that's what I was thinking of.
But I'm curious about the "some circumstances" though. Are there any examples that cannot be replaced with refine?

[Yaël Dillies]

I'm sure it happens when metavariable assignment is delicate

[Kevin Buzzard]

Have we got a concrete example of this?

[Kyle Miller]

Mario Carneiro said:

refine' is not a mathlibism, it's from core

That's true, but the history is a bit complicated. Originally Lean 4's refine was like Lean 3's refine, but then the metavariable handling was improved, and the old behavior was renamed to refine! (and later to refine'). I think it's always been meant as a Lean 3 backwards compatibility tactic. https://github.com/leanprover/lean4/commit/2f4340f63cd9bdb0c9e773745edbe201d012b29d

In the meantime, it's gotten even more complicated, since https://github.com/leanprover/lean4/commit/cf2ea445fe31bb727e9c65afa632def3686089e8 made it so that refine' elaborates its _ as synthetic opaque metavariables and makes synthetic opaque metavariables be assignable. These behave differently from _'s for refine (which elaborate as natural metavariables), both for elaboration under binders (due to creating delayed assignment metavariables) and for the defeq algorithm. Defeq performs ~worse for _'s in refine' than for refine, at least when they appear under binders.

[Jeremy Tan]

Down to 48 in 32

[Jeremy Tan]

You do the rest?

[Riccardo Brasca]

In #13385 there are now 25 refine' (plus two in a comment). None of those is trivial. I think we can bench and then the PR is ready for review.

[Riccardo Brasca]

Do we have a general strategy for things like?

instance : Inhabited (GroupFilterBasis G) := ⟨by
  refine'
    { sets := {{1}}
      nonempty := singleton_nonempty _.. }
  all_goals simp only [exists_prop, mem_singleton_iff]
  · rintro - - rfl rfl
...

[Yaël Dillies]

Sadly no. It's one case where refine' has the edge over refine. I don't apply works either but you might want to try

[Jeremy Tan]

@Riccardo Brasca now 9/8

[Riccardo Brasca]

Thanks!

I think we can stop here for this PR, and deal with the "problematic" cases later

[Riccardo Brasca]

but we really need to bench everything before merging

[Riccardo Brasca]

I've done three more in branch RB/refine_again

[Riccardo Brasca]

Since the benchmark was good I've included those 3 in the PR

[Riccardo Brasca]

I've also done the two about closure. It is enough to give the motive by hand. I am pretty sure the same will work for the two about Clifford algebras.

[Riccardo Brasca]

But I have to stop now.

[Jeremy Tan]

We definitely want to get the last refine' uses out before merging this

[Jeremy Tan]

I had to deal with a new usage of refine' from one of @Joël Riou's commits

[Johan Commelin]

Jeremy Tan said:

We definitely want to get the last refine' uses out before merging this

Why not merge the stuff that builds, and deal with the remainder in a new PR?

[Jeremy Tan]

Better merge it sooner than later, then

[Riccardo Brasca]

I won't be in front of a computer until Monday, but there were quite a lot of comments by @Matthew Ballard

[Damiano Testa]

I'm also away from a computer until Monday, but I'm very happy to see movement in this direction!

[Jeremy Tan]

@Matthew Ballard OK, here's the problem with the instances in Algebra.Field.ULift. When I try to use the same method as I did for replacing refine' as used to build instances:

instance divisionSemiring [DivisionSemiring α] : DivisionSemiring (ULift α) where
  __ := down_injective.divisionSemiring down

I get the error expected structure, which seems like it should not appear

[Jeremy Tan]

When I put this instead

instance divisionSemiring [DivisionSemiring α] : DivisionSemiring (ULift α) where
  left_distrib := sorry
  right_distrib := sorry
  ...

I get stranger error messages like

The rfl tactic failed. Possible reasons:
- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
- The arguments of the relation are not equal.
Try using the reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.
α : Type u
x y : ULift.{v, u} α
inst✝ : DivisionSemiring α
⊢ NatCast.natCast 0 = 0

[Jeremy Tan]

There is only one use of refine' left, in Data.Real.Basic:

instance commRing : CommRing ℝ := by
  refine' { natCast := fun n => ⟨n⟩
            intCast := fun z => ⟨z⟩
            zero := (0 : ℝ)
            one := (1 : ℝ)
            mul := (· * ·)
            add := (· + ·)
            neg := @Neg.neg ℝ _
            sub := @Sub.sub ℝ _
            npow := @npowRec ℝ ⟨1⟩ ⟨(· * ·)⟩
            nsmul := @nsmulRec ℝ ⟨0⟩ ⟨(· + ·)⟩
            zsmul := @zsmulRec ℝ ⟨0⟩ ⟨(· + ·)⟩ ⟨@Neg.neg ℝ _⟩ (@nsmulRec ℝ ⟨0⟩ ⟨(· + ·)⟩),
            .. }
  all_goals
    intros
    first
    | rfl
    | apply ext_cauchy
      simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul,
        cauchy_natCast, cauchy_intCast]
      first
        | done
        | apply add_assoc
        | apply add_comm
        | apply left_distrib
        | apply right_distrib
        | apply mul_assoc
        | apply mul_comm

[Jeremy Tan]

I've got the last use of refine' out

[Jeremy Tan]

Should we merge this now?

[Andrew Yang]

Riccardo Brasca said:

Do we have a general strategy for things like?

instance : Inhabited (GroupFilterBasis G) := ⟨by
  refine'
    { sets := {{1}}
      nonempty := singleton_nonempty _.. }
  all_goals simp only [exists_prop, mem_singleton_iff]
  · rintro - - rfl rfl
...

I personally think this is a permissible usage of refine'

[Yaël Dillies]

We had refine_struct in Lean 3 for this use case

[Jeremy Tan]

Andrew Yang said:

I personally think this is a permissible usage of refine'

To me that syntax looks awful

[Ruben Van de Velde]

It's a bit silly if you then have to handle each field separately anyway

[Yaël Dillies]

Personally I've never been a big fan of the refine_struct syntax, but this

instance PUnit.instBooleanAlgebra : BooleanAlgebra PUnit := by
  refine'
  { PUnit.instBiheytingAlgebra with
    .. } <;> (intros; trivial)

looks better than

instance PUnit.instBooleanAlgebra : BooleanAlgebra PUnit where
  __ := PUnit.instBiheytingAlgebra
  le_sup_inf := _
  inf_compl_le_bot _ := trivial
  top_le_sup_compl _ := trivial

[Yaël Dillies]

And again it's a bit of a shame having to do

instance instCompleteAtomicBooleanAlgebra : CompleteAtomicBooleanAlgebra PUnit where
  __ := PUnit.instBooleanAlgebra
  sSup _ := unit
  sInf _ := unit
  le_sSup _ _ _ := trivial
  sSup_le _ _ _ := trivial
  sInf_le _ _ _ := trivial
  le_sInf _ _ _ := trivial
  iInf_iSup_eq _ := rfl

to avoid refine'

[Yaël Dillies]

Can you split the changes to former uses of refine_struct out of #13385 ? Then I believe #13385 will only contain non-objectionable changes.

[Jeremy Tan]

When I did the "shameful" thing to the CommRing instance in Data.Real.Basic the instructions decreased by just over a third. Shamefulness can be tolerated if we have performance gains like these – it's the tactic combinators used in some of these instances that are the real shame

[Andrew Yang]

I am personally not against merging the pr as is (after some reviewer take a look). Just that we should have a discussion on this when we write a linter against refine'.

[Jeremy Tan]

Could we have syntax like this?

def subtype : S →⋆ₐ[R] A := by refine { toFun := ((↑) : S → A), ?_ } <;> intros <;> rfl

[Jeremy Tan]

Or even

instance instCompleteAtomicBooleanAlgebra : CompleteAtomicBooleanAlgebra PUnit where
  __ := PUnit.instBooleanAlgebra
  sSup, sInf := by intro; unit
  le_sSup, sSup_le, sInf_le, le_sInf := by intros; trivial
  iInf_iSup_eq _ := rfl

[Yaël Dillies]

I quite like both options

[Eric Wieser]

The first should probably be ?..?

[Eric Wieser]

Then foo ?.. could also mean foo ?_ ?_ etc, to match foo .. meaning foo _ _

[Mario Carneiro]

(FYI, y'all are re-inventing @Thomas Murrills 's proposal for ?.. in structure literals)

[Thomas Murrills]

I did get as far as implementing it for structures, but the core PR died due to lack of interest, stage0 friction (iirc?), and core being more or less frozen at the time. I could revive it, but I’d only want to do so if there’s interest. :)

(Note also that the function application .. syntax is (or at least, when I last checked, was) pretty much unrelated on an implementation level to the structure instance syntax, so I’m guessing these would be two separate PRs. The function application version might even be simpler?)

[Kyle Miller]

Are there applications where foo .. should mean foo _ _ rather than foo ?_ ?_?

[Mario Carneiro]

I think it's a bit dangerous to just use foo ?_ ?_ because ?_ represents arguments that should not be inferred by unification and will give an error if unification forces them to be something in particular

[Mario Carneiro]

refine' has the nice property that it basically "figures out" whether a given hole should be _ or ?_

[Mario Carneiro]

if we were to use ?_ in more hidden locations, I think we would need to use this kind of "figure it out" hole instead of just _ or ?_

[Kyle Miller]

What I mean is, where is foo .. used outside of patterns?

[Mario Carneiro]

I use foo .. all the time in exprs?

[Mario Carneiro]

e.g. have : x + y = y + x := Nat.add_comm ..

[Mario Carneiro]

and this example is correctly using _ holes

[Kyle Miller]

I see, you use it as a cheap by apply Nat.add_comm

[Mario Carneiro]

if you made it use ?_ then it would be a type error

[Kyle Miller]

Yeah, I understand. I only use it for match patterns myself, hence my question.

[Kyle Miller]

I wonder if it would be possible to have a ??_ hole type, which would be somewhere between natural and synthetic opaque. Unlike synthetic opaque it would be assignable, but if there's a unification between a natural metavariable and ??_, the natural metavariable would be the one that gets assigned. I think it ought to behave like synthetic opaques when being abstracted (e.g. in mkLambdaFVars) so that it behaves like ?_ in all respects but assignability.

That way, foo .. could mean foo ??_ ??_, making it usable when some of the arguments can be inferred.

[Thomas Murrills]

I think there’s some UX usefulness in separating “variadic _” from “variadic ?_”—we get to preserve the distinction people have already learned between _ and ?_ without introducing a new concept!

In the other direction, if there are two kinds of holes already, you’d kind of expect there would be two kinds of variadic versions too, right? Visually things would match up nicely and reinforce/reflect the learned distinction: _ ↔︎ .. and ?_ ↔︎ ?..

[Kyle Miller]

My line of questioning here is whether "variadic '_'" and "variadic '?_'" are themselves good UX. They each have some significant problems, and I think before introducing ?.. it would be good to collect the ways we use and want to use .. and to see if we're missing anything here in the design space. While tempting, I don't think 'completing the 2x2 square' is sufficient reason to add ?...

Here's a thought experiment: what if refine f .. was the same as apply f? Neither the current .. nor the proposed ?.. would work to write an apply as a refine. (That said, whatever the choice for .., you wouldn't be able to replace all apply f's with refine f .. since apply f can figure out how to partially apply a function using the expected type. I think it's still worth thinking about in the fully applied case though.)

[Kyle Miller]

I guess a big problem with .. as "variadic ??_" is that if you used it like in Mario's example, with have : x + y = y + x := Nat.add_comm .., and for some reason there were arguments that couldn't be filled in, you'd get new goals, would would likely be an unwelcome surprise.

[Thomas Murrills]

I mean, I’m not tempted by completing the 2x2 square per se, or saying that that’s why we should use ?..; I’m saying that from a usability perspective it’s easily learnable and mentally nearby, in a useful way, to existing design.

The leading ? here functions as a useful visual cue with a consistent meaning, and the visual similarity of _ and .. (with .. looking like multiple _, squished, or at least being a simple mark near the baseline) makes its relationship to _ memorable, meaningful, and simple. (Even if people don’t consciously identify this visual relationship, I think their brain probably does, and it helps keep them related without extra thought.)

I’d say relationships like these help the user more easily keep a reliable understanding of the semantics; I’d be concerned that identifying .. as occupying a new, distinct spot in the design space can translate to “new, distinct behavior the user has to learn”, instead of letting the user extend their understanding of existing behavior in a simple manner.

Likewise, part of me thinks “if you want fancy behavior, use a fancy tactic” like apply.

[Thomas Murrills]

But, to play devil’s advocate with myself a bit…

Sometimes having something which “just does what you want” is better. It remains to be seen if ../?.. are/would be actually close enough to what we typically find useful.

And, even if we don’t want .. to be apply-like, it would definitely be worth exploring what behavior is desired in related cases anyway, including differences between apply behavior and refine behavior; maybe there should be something that fills some gap.

[Richard Osborn]

I would be fine with lean having an option to treat _ or .. as "fill in if you can, create a goal if you can't", as it would make hacking on proofs a bit easier. But for code that needs to be maintained over time, I think explicit holes are much more preferable.

[Kyle Miller]

That's the refine' tactic, unless you mean something else?

[Matthew Ballard]

Jeremy Tan said:

Could we have syntax like this?

def subtype : S →⋆ₐ[R] A := by refine { toFun := ((↑) : S → A), ?_ } <;> intros <;> rfl

I would prefer

def subtype : S →⋆ₐ[R] A := refine% { toFun := ((↑) : S → A), .. } (by intros; rfl)

since the main (mis-)use case here for by refine'/by refine is "I don't want to repetitively fill arguments"

[Kyle Miller]

Maybe we could have a syntax that could be used in where clauses too? Imagine a "default field" that could be used for every field not already specified.

def subtype : S →⋆ₐ[R] A := { toFun := ((↑) : S → A), * := by intros; rfl }

def subtype : S →⋆ₐ[R] A where
  toFun := ((↑) : S → A)
  * := by intros; rfl

The * isn't great. The main point is being able to escape the need to write the structure itself using tactics.

[Richard Osborn]

Well you can place ?_ or _ in non refine tactics. For example, I believe you can write rw [foo], rw [foo _], and rw [foo ?_] which will all potentially create an extra goal.

[Thomas Murrills]

* := is ugly, but honestly quite intuitive…to toss out some other options, we could use _ := by … like a fallback match alt, try to visually clean up/isolate * (e.g. (*) := by …) or use a dedented word token analogous to decreasing_by, such as on_remaining (though I don’t like that particular suggestion).

[Matthew Ballard]

It’s not just structures where you have this though. The Function.Injective instance constructors are another place you see this pattern

[Matthew Ballard]

This could be taken care of with defaults though

[Thomas Murrills]

In that case I wonder if there should be a “term-mode <;>”, so you could write e.g. foo .. <;> by rfl?

[Matthew Ballard]

Yes

[Thomas Murrills]

(I.e. with no refine% necessary)

[Matthew Ballard]

That would be fine with me. I’m not sure about the fine tuning for when you have different proofs. But I think the base case of hit em all comes up enough to warrant existence

[Thomas Murrills]

Another option would be to extend the * notation to function arguments, e.g. foo (* := by rfl), which would fit nicely if we go that route with where

[Thomas Murrills]

Though, I’m not sure this would cover all cases you’re thinking of

[Thomas Murrills]

(If not maybe we’d want both, with a preference for (* := …) (or whatever the actual notation would be))

[Jeremy Tan]

I am leaning towards the second proposal of mine, where fields proved with the same tactics are listed together

[Thomas Murrills]

I like that too; it also seems compatible with the *-like approach. Likewise I wouldn’t be opposed to seeing it in function application as well (e.g. foo (bar, baz := val))

[Kyle Miller]

A syntax issue there is that x, y := v right now means x := x, y := v. I don't think it's possible to use a comma for this new meaning

[Jeremy Tan]

How about using &?

[Kyle Miller]

or maybe [x, y] := v?

[Kyle Miller]

with [*] := v or [_] := v for the wildcard?

[Richard Osborn]

.. := by intros; rflcould work as syntax for where clauses, right?

[Thomas Murrills]

Just to exhaust all options, would x; y := v cause any conflicts? (Though maybe it would be odd having ; indicate a tighter grouping than ,…)

[Jeremy Tan]

I've created #13472 which is #13385 up to GroupTheory and without the refine_struct-related changes

[Jeremy Tan]

Kyle Miller said:

or maybe [x, y] := v?

Yes, that is OK

[Jeremy Tan]

#13474 makes the remaining "uncontroversial" removals of refine'

[Jeremy Tan]

(It has been approved...)

[Eric Wieser]

Thomas Murrills said:

Just to exhaust all options, would x; y := v cause any conflicts? (Though maybe it would be odd having ; indicate a tighter grouping than ,…)

I think this is already valid and means x = x; y = y?

[Eric Wieser]

Kyle Miller said:

or maybe [x, y] := v?

Or {x, y} as I think this already works for destructed assignment?

[Thomas Murrills]

Eric Wieser said:

I think this is already valid and means x = x; y = y?

Huh, really? I can’t get that to work; can you give an example?

[Thomas Murrills]

Just to put it out there, another option is to prefix (or suffix) with some symbol, e.g. *(x, y) or *[x, y] or *{x, y}—whatever symbol might be used for wildcard case, to tie the two together. (Though it’s starting to look a little busy…)

[Richard Osborn]

Do we have a case where we need to list the names? I'm slightly worried we are over-engineering a solution.

[Kyle Miller]

I think it's usually a good idea to explore the design space to make sure you're not designing yourself into a corner, for future extensibility, even if it won't be used. It's like a fiction author who comes up with all the characters' backstories and the region's full history.

[Thomas Murrills]

Also, was the original example one such case, or was that for demonstration purposes?

[Kyle Miller]

Listing names came up because of Jeremy pointing out that different collections of fields might need different proofs: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Status.20of.20.60refine'.60/near/442033686

[Kyle Miller]

There's another option of having structure instances have a remaining_fields clause with one goal per missing field

[Thomas Murrills]

I think it would be great for this notation to be compatible with function application somehow, given the earlier-stated need for non-structure cases

[Thomas Murrills]

(Also ideally I think we shouldn’t “force the user into tactic mode” unnecessarily, so to speak)

[Kyle Miller]

Are there use cases for specifying a single value for the remaining fields? It seems to me that value fields tend to be rather heterogenous, vs proof fields that plausibly could use the same tactic script with different meanings.

I suppose using default as a value isn't absurd.

[Thomas Murrills]

Or e.g. fun _ => rfl, where all arguments (here, to rfl) and types are implicit

[Thomas Murrills]

That is, sometimes proof fields are terms with implicit arguments, though rfl is the only one I can think of that would be widespread.

[Kyle Miller]

Oh, a technical argument against the remaining_fields clause is that it would not support the use case of replacing refine_struct. You can't do remaining_fields exact ?_ since this metavariable has to be solved for within the tactic block.

[Thomas Murrills]

(Only tangentially related: .. has some “expectable” usages which aren’t allowed yet, e.g. fun .. => as a term-mode intros (and likewise in match alts) and nonterminal .. in function application. These seem “nice” and “obvious” to me, but I’m not sure if everyone would agree or think they’re worth the time/energy to implement. There also might be technical challenges, of course…)

[Jeremy Tan]

#13490 removes those remaining refine's where doing so at least keeps the line count unchanged

[Damiano Testa]

I am not sure if there are more PRs removing uses of refine', but the PR with the linter deprecating refine' (#11884) fixes the remaining 17 uses of refine' that the linter catches.

[Damiano Testa]

I can extract the refine' --> refine to a separate PR, if the linter is not something that is wanted, though.

[Johan Commelin]

@Damiano Testa Can you please update the PR description? (This is just a test, etc...)

[Damiano Testa]

I updated the PR description.

[Damiano Testa]

In fact, following what Michael usually says, I will add the reasons why the linter is ther to the docs themselves!

[Michael Rothgang]

My impression is that this thread has converged to some consensus. Is the following an accurate summary? Please let me know if something is amiss or missing.

• replace refine' by refine in easy cases is good and desirable
• some fixes (such as avoiding refine' to construct data) were clearly good and different
• there was a relatively small number of more interesting cases. There are various proposals aimed to improve this slice of refine'; it is not apparent to me whether anybody has actually worked on any of these. The existing replacements in #13385 were acceptable to everybody. (There may be a spectrum of opinions here, but I didn't hear anybody specifically object to these.)
• some prefer to not simply ban all refine', but check if any further cases come up.

Two months ago, there were no uses of refine' in mathlib; they are slowly creeping in. #11884 adds a linter which warns on uses of refine', but is worded in a soft way. The implementation there looks good to me, perhaps module some word-smithing of the linter message. Are there concerns with merging it (perhaps, after fixing the remaining occurrences)?

[Riccardo Brasca]

Wow, like 80 refine' in two months!

[Riccardo Brasca]

We really want the linter I think

[Riccardo Brasca]

@Damiano Testa can you have a look at how many of those can be removed automatically?

[Michael Rothgang]

#14902 has cherry-picked Damiano's fixes from June, plus almost all the new ones. (Two files are missing, I'm waiting for the cache to be available.)

[Riccardo Brasca]

Thanks!

[Michael Rothgang]

Riccardo Brasca said:

Wow, like 80 refine' in two months!

To be fair, 50 of these are in porting notes or commented code - but still, 30 is also a lot!

[Damiano Testa]

I just "restarted" the PR with the refine' linter: I'll take care of the comments, clean up what needs to be cleaned up and then I'll ping again to see if it is ready to merge!

[Michael Rothgang]

#14902 needs one more tweak. I need to run now, but will return to this in the afternoon.

[Damiano Testa]

Michael, I also updated the linter PR and I got it to build. I am not sure what is better going forwards: merge the replacements refine' --> refine separately and then the linter, or merge the linter with the replacements.

I do not particularly mind either way, but since it seems that the linter is going to be merged, maybe it is not necessary to have two more PRs about this.

[Damiano Testa]

Anyway, once the #align removal PR will get merged, everyone is likely to have merge conflicts.

[Johan Commelin]

Except for my PR changing a CI workflow :rofl:

[Riccardo Brasca]

Damiano Testa said:

Anyway, once the #align removal PR will get merged, everyone is likely to have merge conflicts.

Yep, we should write an announce or something

[Michael Rothgang]

I've just bors-ed #14902; we can compare if the linter found anything different :-)

[Michael Rothgang]

If there turn out to be conflict, we can happily roll it all into #11884.

[Damiano Testa]

Michael's PR with the removal of the remaining refine' made it into master and I merged the new master into the linter PR with no conflicts.

CI is working on #11884: assuming that it becomes green, I think that it is ready to go! Are there any more comments on the linter?

[Johan Commelin]

[Damiano Testa]

The refine' linter has been merged! Now, everyone using mathlib will have to think twice about using refine'! :smile:

[Kim Morrison]

Can we just get rid of it? I feel like if we're in the situation that we don't want anyone using it in Mathlib (which I agree with!) then we may as well just remove the distracting variation in ways to say the same thing. Redundant syntaxes come at a cost to learning the language, and this has to weigh against corner cases or narrow use by experts.

[Mario Carneiro]

I'd prefer we didn't, it's useful for live coding

[Mario Carneiro]

also IIRC we still don't have an alternative to refine' for refine_struct

[Richard Osborn]

Could we eventually turn refine' into a replacement tactic that suggests the refine replacement? Maybe rename it to refine? in alignment with other replacement tactics.

[Kyle Miller]

One idea from earlier is to allow syntax like refine { a := x, b := y, .. := ?_ } for refine_struct, with the understanding that ?_ would be elaborated per additional field.

[Kim Morrison]

Hmmmm, I'd argue that Mario wanting to use it for live coding might be included in what I had in mind for "narrow use by experts". :-) It still needs to be weighed against increasing the surface area of the language.

[Kim Morrison]

I do like refine?.

[Mario Carneiro]

I mean, you can say the same things about refine' as have', and sorry for that matter

[Mario Carneiro]

they are useful when you aren't done with the proof yet

[Mario Carneiro]

keep in mind that mathlib is a collection of finished proofs, proofs in progress have a very different style

[Mario Carneiro]

you shouldn't take nonexistence in mathlib, or linted-against-ness in mathlib as evidence that a tactic is not useful

[Mario Carneiro]

honestly for most beginners refine' and have' are strictly easier to use than the unprimed variants

[Mario Carneiro]

refine makes you attend to a detail that is only relevant if you are trying to write high quality maintainable code

[Mario Carneiro]

so I very much disagree about it being an expert-only feature, it's closer to a beginner-only feature

[Kim Morrison]

But refine?, with the behaviour of refine' plus a suggestion would be even better?

[Mario Carneiro]

that seems fine, assuming that we can write it

[Kevin Buzzard]

(Note also that cases' is much easier than cases for mathematician beginners and it's not really possible to use cases within a lean4game game)

[Eric Wieser]

(I think the argument goes we should teach obtain there instead of cases'? So obtain _ | n := n instead of cases' n with n etc)

[Kevin Buzzard]

Ok I'll switch to obtain :-) Nice idea!

[David Ang]

Or rcases…

[Floris van Doorn]

refine is really annoying if you have to specify that goals should be created for implicit arguments, e.g. refine my_lemma (β := ?_) (f := ?_) ?_ ?_ or something (e.g. when my_lemma is a transitivity)

[Matthew Ballard]

To me, the main problem with refine' is implementation and the lesser problem is readability.