Usage of refine'

Stream: mathlib4

[Josha Dekker]

In a few recent PR's I've been asked to replace my usage of refine' by refine, as the former is more of a legacy usage. As refine' seems to be present in various files, is there an easy way for me to write some code that automatically replaces refine' by refine on various files and make a PR with this? I'm still working through the meta-programming book, so I'm not yet at the point that I can write this up myself, but I'm happy to learn! Otherwise, I'll circle back to this once I've worked through the meta-programming book!

[Damiano Testa]

Automatic replacing might be tricky, mostly due to the formatting of the output text. Automatic flagging would be very easy with a dedicated linter.

[Damiano Testa]

Once you have the flags, you could probably easily write a script to do the replacements.

[Damiano Testa]

However, sometimes you will have to replace _ by ?_ and this could be very tricky.

[Josha Dekker]

Damiano Testa said:

However, sometimes you will have to replace _ by ?_ and this could be very tricky.

Yes, exactly. The quick & dirty way would be to try all possible combinations and continue as soon as the proof compiles, but I’m afraid I don’t know enough meta-programming (yet)

[Josha Dekker]

Damiano Testa said:

Automatic replacing might be tricky, mostly due to the formatting of the output text. Automatic flagging would be very easy with a dedicated linter.

Yes, but there could be very many usages, so I’m not sure what the point is, as long as there is no automatic way to replace them.

[Riccardo Brasca]

Do we still sometimes need to use (_)? This can be very tricky, but maybe refine is smarter now than during the port.

[Damiano Testa]

Josha Dekker said:

Damiano Testa said:

Automatic replacing might be tricky, mostly due to the formatting of the output text. Automatic flagging would be very easy with a dedicated linter.

Yes, but there could be very many usages, so I’m not sure what the point is, as long as there is no automatic way to replace them.

Well, you would get a live warning informing you that refine' should be replaced by refine. You could then collect all these warnings from CI and at least you would know the size of the problem and precise locations of the issues.

[Damiano Testa]

Overall, I think that developing a tool for "generic refactoring" would be very useful. However, doing something ad hoc that would work with refine' and basically nothing else could be a fun learning project, but may not be worth the effort. (This is my very personal opinion.)

[Damiano Testa]

Also, if you decide to do the replacement, then linting against usage of refine' would be a sustainable way of making sure that refine' will not be used, even after you are done with the refactoring.

[Josha Dekker]

Damiano Testa said:

Also, if you decide to do the replacement, then linting against usage of refine' would be a sustainable way of making sure that refine' will not be used, even after you are done with the refactoring.

This is a good point of course. I think it should be possible to have a general refactoring tool, but I’ll have to postpone this until I learn enough meta-programming. Thanks for the suggestions!

[Damiano Testa]

I think that a general refactoring tool is "the next milestone" for development. Right now, if you decide that you want to replace the order of two hypotheses to a function, it can be time-consuming to fix all the breakages. Even having a tool that does this is a principled way would be amazing.

[Josha Dekker]

Damiano Testa said:

Also, if you decide to do the replacement, then linting against usage of refine' would be a sustainable way of making sure that refine' will not be used, even after you are done with the refactoring.

So would a linter only complain for future usage of refine’, or would it also complain for existing usage? In the latter case, I might be able to look into that a bit earlier!

[Damiano Testa]

Btw, there are approximately 11k refine' in mathlib: I strongly suspect that eradicating refine' from mathlib will only be achieved by some very serious automation.

[Damiano Testa]

Josha Dekker said:

Damiano Testa said:

Also, if you decide to do the replacement, then linting against usage of refine' would be a sustainable way of making sure that refine' will not be used, even after you are done with the refactoring.

So would a linter only complain for future usage of refine’, or would it also complain for existing usage? In the latter case, I might be able to look into that a bit earlier!

The linter can complain wherever you want. The easiest is for it to complain everywhere.

[Damiano Testa]

If you give me some time, I can write a very simple-minded linter for that. You would then have to wait for CI (or local build) to know where the usages are.

[Josha Dekker]

Damiano Testa said:

If you give me some time, I can write a very simple-minded linter for that. You would then have to wait for CI (or local build) to know where the usages are.

No hurry, I’ll need to learn more meta-programming first anyway…

[Josha Dekker]

Damiano Testa said:

Btw, there are approximately 11k refine' in mathlib: I strongly suspect that eradicating refine' from mathlib will only be achieved by some very serious automation.

That’s a lot!

[Damiano Testa]

The linter is active at #11884. This is very simple-minded and has no claim of robustness.

If you look at the build mathlib step, you get a report of usages of refine'. I imagine that the output will be too long before CI will give up, but it is a start!

[Damiano Testa]

Just to give you an impression of the challenges that this experiment poses, this is literally the first declaration that the linter flags:

instance : LawfulFunctor (Sum.{v, u} e) := by
  refine' { .. } <;> intros <;> (try casesm Sum _ _) <;> rfl

and replacing refine' with refine breaks the proof.

[Josha Dekker]

Damiano Testa said:

Just to give you an impression of the challenges that this experiment poses, this is literally the first declaration that the linter flags:

instance : LawfulFunctor (Sum.{v, u} e) := by
  refine' { .. } <;> intros <;> (try casesm Sum _ _) <;> rfl

and replacing refine' with refine breaks the proof.

Yeah, dealing with .. will probably be a bit of a challenge...

[Eric Wieser]

Identifying these is probably useful for working out if there are missing features that we need to teach refine first

[Damiano Testa]

Maybe I came across as too negative: I think that this is a very worthwhile project, with the idea of carrying it out in a structured way, with no hacks... and investing a lot of effort!

[Damiano Testa]

There are certainly really useful tools that could be developed in the process of getting rid of refine' that will likely largely outweight the (really hard) goal of removing 11k ' from mathlib.

[Josha Dekker]

Damiano Testa said:

Maybe I came across as too negative: I think that this is a very worthwhile project, with the idea of carrying it out in a structured way, with no hacks... and investing a lot of effort!

No worries, I got that impression as well! I will think on this a bit and return once my meta-programming knowledge is more up to speed!

[Damiano Testa]

Here is something that I would not know right-away how to do and that seems much smaller scope: find places where simply replacing refine' by refine and do nothing else produces a valid proof. Finding these "easy wins" would be good.

[Damiano Testa]

Once you have that, you could for instance find places where refine could be replaced by exact...

[Damiano Testa]

Oh, I forgot to write text for the warning in the linter!

[Josha Dekker]

Damiano Testa said:

Here is something that I would not know right-away how to do and that seems much smaller scope: find places where simply replacing refine' by refine and do nothing else produces a valid proof. Finding these "easy wins" would be good.

I think I’ve always had to replace some _ by ?_ when I replace refine’ by refine, but this is certainly interesting to check!

[Damiano Testa]

With 11k opportunities, everything that has a chance of happening will happen:

-- Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean:520-526
theorem corec_roll {α : TypeVec n} {X Y} {x₀ : X} (f : X → Y) (g : Y → F (α ::: X)) :
    Cofix.corec (g ∘ f) x₀ = Cofix.corec (MvFunctor.map (id ::: f) ∘ g) (f x₀) := by
  mv_bisim x₀ with R a b x Ha Hb
  rw [Ha, Hb, Cofix.dest_corec, Cofix.dest_corec, Function.comp_apply, Function.comp_apply]
  rw [MvFunctor.map_map, ← appendFun_comp_id]
  refine' liftR_map_last _ _ _ _ _
  intro a; refine' ⟨a, rfl, rfl⟩  -- useless `'`

[Damiano Testa]

The first run of the linter is done. This is a tally of the files with at least 30 usages of refine':

30 warnings in Mathlib/LinearAlgebra/LinearIndependent.lean
30 warnings in Mathlib/MeasureTheory/Covering/Differentiation.lean
30 warnings in Mathlib/Topology/ContinuousFunction/Bounded.lean
31 warnings in Mathlib/Analysis/Calculus/ContDiff/Defs.lean
31 warnings in Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean
31 warnings in Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean
31 warnings in Mathlib/MeasureTheory/Constructions/Polish.lean
31 warnings in Mathlib/MeasureTheory/Function/Jacobian.lean
31 warnings in Mathlib/MeasureTheory/Integral/Bochner.lean
31 warnings in Mathlib/RingTheory/Jacobson.lean
32 warnings in Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean
32 warnings in Mathlib/Order/Filter/Basic.lean
32 warnings in Mathlib/Probability/Process/Stopping.lean
32 warnings in Mathlib/Topology/Separation.lean
33 warnings in Mathlib/Analysis/BoxIntegral/Integrability.lean
33 warnings in Mathlib/Analysis/Convex/Between.lean
33 warnings in Mathlib/Data/Seq/WSeq.lean
33 warnings in Mathlib/ModelTheory/Semantics.lean
33 warnings in Mathlib/Probability/Martingale/Basic.lean
33 warnings in Mathlib/RingTheory/UniqueFactorizationDomain.lean
34 warnings in Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean
35 warnings in Mathlib/Analysis/MellinTransform.lean
35 warnings in Mathlib/RingTheory/Ideal/Operations.lean
36 warnings in Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean
36 warnings in Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean
38 warnings in Mathlib/Analysis/Complex/PhragmenLindelof.lean
38 warnings in Mathlib/Data/Complex/ExponentialBounds.lean
39 warnings in Mathlib/Analysis/Distribution/SchwartzSpace.lean
39 warnings in Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean
39 warnings in Mathlib/Probability/Martingale/Upcrossing.lean
40 warnings in Mathlib/CategoryTheory/Generator.lean
41 warnings in Mathlib/Analysis/NormedSpace/lpSpace.lean
42 warnings in Mathlib/NumberTheory/Cyclotomic/Basic.lean
42 warnings in Mathlib/SetTheory/Cardinal/Cofinality.lean
46 warnings in Mathlib/Analysis/Analytic/Basic.lean
46 warnings in Mathlib/Analysis/Convolution.lean
47 warnings in Mathlib/Analysis/Convex/Side.lean
49 warnings in Mathlib/MeasureTheory/Measure/Hausdorff.lean
51 warnings in Mathlib/Computability/TuringMachine.lean
54 warnings in Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
57 warnings in Mathlib/MeasureTheory/Function/LpSpace.lean
61 warnings in Mathlib/MeasureTheory/OuterMeasure/Basic.lean
68 warnings in Mathlib/MeasureTheory/Integral/Lebesgue.lean
74 warnings in Mathlib/MeasureTheory/Integral/SetToL1.lean
78 warnings in Mathlib/MeasureTheory/Function/UniformIntegrable.lean
82 warnings in Mathlib/Computability/TMToPartrec.lean

[Mario Carneiro]

Damiano Testa said:

With 11k opportunities, everything that has a chance of happening will happen:

-- Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean:520-526
theorem corec_roll {α : TypeVec n} {X Y} {x₀ : X} (f : X → Y) (g : Y → F (α ::: X)) :
    Cofix.corec (g ∘ f) x₀ = Cofix.corec (MvFunctor.map (id ::: f) ∘ g) (f x₀) := by
  mv_bisim x₀ with R a b x Ha Hb
  rw [Ha, Hb, Cofix.dest_corec, Cofix.dest_corec, Function.comp_apply, Function.comp_apply]
  rw [MvFunctor.map_map, ← appendFun_comp_id]
  refine' liftR_map_last _ _ _ _ _
  intro a; refine' ⟨a, rfl, rfl⟩  -- useless `'`

That's not just a useless refine' where refine could do, it's a useless refine where exact could do. (This is another lint I've been contemplating)

[Mario Carneiro]

I think it's pretty much an either-or: if this refine' isn't an exact, then it must have some use of _ that needs to be made into ?_

[Damiano Testa]

Yes, I have also been thinking about the "terminal refine" linter. I wonder if it is possible for a refine' to be replaced by a refine without breaking the proof and not being terminal.

[Damiano Testa]

(In fact, I found the example by looking for terminal refine's.)

[Mario Carneiro]

refine without any use of ?_ will not produce any subgoals

[Damiano Testa]

Ok, I was simply wondering if they have different heuristics internally, but if you are sure, then this is what it is!

[Mario Carneiro]

I suppose if the refine' could be using ?_, then it would match your criteria

[Mario Carneiro]

Damiano Testa said:

Ok, I was simply wondering if they have different heuristics internally, but if you are sure, then this is what it is!

what heuristics?

[Mario Carneiro]

I am sure that refine will not produce subgoals if there are no ?_, but I am less sure that this syntax isn't produced by some complicated elabs

[Damiano Testa]

I do not know if refine with or without ' use some heuristics to close the goals that are implied by their syntax. If there are differences, it could be that one of the two deals with some goals that the other would have left.

[Mario Carneiro]

no, they have no such thing, they exclusively do unification

[Mario Carneiro]

(one of the reasons it's my favorite tactic)

[Damiano Testa]

E.g., refine will do something with _ to try to close them, and that something could have been different to what refine' does and then there is some scope for what I said [reading your comments, I understand that this is not the case].

[Damiano Testa]

I also like refine a lot. And honestly, Lean 4 apply climbed up in my list of favorite tactics from the place that it had in Lean 3.

[Damiano Testa]

Anyway, I view every added comment as further confirmation that more automation is needed! :smile:

[Mario Carneiro]

Maybe the first thing we can do with refine' conversion is to have a code action for it. I think it will be insufficient for mathlib because we have 10000 occurrences to replace, but at least for the PR author case it seems helpful

[Mario Carneiro]

it's not that hard to find the right locations to replace _ with ?_ (given the info tree), you just need to replace _ syntaxes that elaborated to mvars that are in the goalsAfter for the tactic

[Damiano Testa]

With these automatic replacements, I always worry about getting the proposed syntax to match the input one. E.g. in this case, I would expect that (except for the 100 character limit) the code action would simply erase a ' and add some ?. However, most of the time, the printing does more than just that.

[Damiano Testa]

(The linter found 11340 refine' in mathlib.)

[Yaël Dillies]

Damiano Testa said:

Here is something that I would not know right-away how to do and that seems much smaller scope: find places where simply replacing refine' by refine and do nothing else produces a valid proof. Finding these "easy wins" would be good.

That pretty much never happens, right?

[Damiano Testa]

I had a hunch that it could only happen for terminal refine's and Mario confirmed this.

[Mario Carneiro]

Damiano Testa said:

With these automatic replacements, I always worry about getting the proposed syntax to match the input one. E.g. in this case, I would expect that (except for the 100 character limit) the code action would simply erase a ' and add some ?. However, most of the time, the printing does more than just that.

That's okay, the code action doesn't have to reprint the whole syntax, it can literally say "insert ? here, remove ' there"

[Mario Carneiro]

which could of course go over the line length, but probably rarely enough that it can be handled manually

[Damiano Testa]

Ah, good to know! I am curious to learn about automatic replacements: after linting, I will explore that!

[Damiano Testa]

Btw, when producing the refine linter PR, I reached for lake exe mkAll and of course it failed me! I already depend on it! :smile:
cc @Yaël Dillies

[Yaël Dillies]

Ahah, that's a very good sign :smiley:

[Yaël Dillies]

Damiano Testa said:

I had a hunch that it could only happen for terminal refine's and Mario confirmed this.

Yes sorry I didn't scroll enough

[Josha Dekker]

can we [@deprecated] tactics (like refine')? Or is this not possible?

[Mario Carneiro]

it's not directly possible, but you can write a linter that pretends to be the deprecation linter and puts warnings on uses of refine'

[Damiano Testa]

In fact, this is exactly what the PR does! :smile:

[Damiano Testa]

In case anyone is interested, I also wrote a quick "terminal refine" linter: #11890.

I may have made the "terminal" part too strict, but even so it is catching some good stuff.

[Damiano Testa]

It turns out that there are over 170 terminal uses of refine/refine' in mathlib.

Assuming that I fixed all the complaints of the linter, all of them can be replaced by exact with a unique exception:

--  Mathlib/RingTheory/Jacobson.lean:477-519
  ...
  suffices (⊥ : Ideal (Localization M)).IsMaximal by
    rw [← IsLocalization.comap_map_of_isPrime_disjoint M (Localization M) ⊥ bot_prime
      (disjoint_iff_inf_le.mpr fun x hx => hM (hx.2 ▸ hx.1))]
    -- a terminal `refine'` that cannot be replaced by either a `refine` nor an `exact!
    refine' ((isMaximal_iff_isMaximal_disjoint (Localization M) _ _).mp (by rwa [map_bot])).1
  ...

This is the commit that unlints this usage.

Source: #11890

[Kyle Miller]

I was going to mention that there's a very subtle difference between refine and refine' in the way _'s are elaborated, so you might run into some oddities!

[Kyle Miller]

It turns out we can fix this one easily by replacing the first _ with a:

exact ((isMaximal_iff_isMaximal_disjoint (Localization M) a _).mp (by rwa [map_bot])).1

[Damiano Testa]

I feel that mathlib is so big that any quirk in any tactic is exploited somewhere.

[Damiano Testa]

I'll remove the no-linting and use your proof in the next round of CI: I am now curious to check that there are no further warnings.

[Damiano Testa]

I was a little skeptical about this linter, but !bench gives a (small) speed-up. I put it up for review, but feel free to say that this is undesirable!

[Damiano Testa]

The file with the speed-up had 3 refine' that became exact.

[Matthew Ballard]

Not that the overall change in instructions is nearing +1T which is an increase of about 0.75% and fairly large for a single PR so your skepticism is supported I would say.

I would recommend breaking off performant changes into a separate PR.

[Damiano Testa]

Oh, I see! I only looked at the summary, thinking that it was representative (and since I usually have very little understanding of the figures in the !bench output)!

[Matthew Ballard]

I think the highlights should always include the change in total instructions

[Damiano Testa]

I really have a hard time understanding these benchmarks: where are the total instructions?

[Damiano Testa]

(And roughly "total instructions" is a good measure of "total time for a single run"?)

[Matthew Ballard]

Time can be affected by spurious things like other processes CPU and RAM usage. This is more deterministic and a proxy for "how hard the computer has to work to build Mathlib"

[Matthew Ballard]

Perhaps is it far to say they are "atoms of CPU work" as a metaphor

[Damiano Testa]

Ok, that's good enough. Probably similar to the difference between "time" and "heartbeats"?

[Matthew Ballard]

If I knew more about the implementation of heartbeats, I would probably safely say yes. I say it unsafely still

[Damiano Testa]

Ok, thanks!

[Damiano Testa]

How can I extract the information of which files were positively affected?

[Damiano Testa]

I assume that the suggestion would be "perform the refine --> exact change in those files and nowhere else"?

[Kyle Miller]

It's still not perfect though -- you can change the memory access patterns while keeping the number of instructions the same, and it's possible for one instruction to take 200 cycles waiting on main memory during a cache miss.

A program could get faster while using more instructions, if those calculations allow the program to avoid reading from main memory.

[Matthew Ballard]

Damiano Testa said:

How can I extract the information of which files were positively affected?

I use the web interface and sort by change

[Damiano Testa]

For the level of understanding that I have "It's complicated, but it is roughly the number of elementary steps that the computer does" is a good approximation!

[Matthew Ballard]

The current terminal refine''s in RingHomProperties existed because refine' could resolve differences in typeclass instances better than exact. It was a hack

[Damiano Testa]

Matthew Ballard said:

Damiano Testa said:

How can I extract the information of which files were positively affected?

I use the web interface and sort by change

Ok, I see that a "feature" of the sort is that it sorts by absolute value of change of instructions! This had confused me earlier.

[Damiano Testa]

Just to be completely clear: the "good" changes are the ones that have a - right?

[Damiano Testa]

Thanks and sorry for the silly questions!

[Matthew Ballard]

Not silly whatsoever. Very happy to see things benchmarked before merging instead of after

[Damiano Testa]

#11896 and !benched!

[Damiano Testa]

I still wonder whether having the linter as "dormant" might be desirable. It can easily be changed to inspect other finishing tactics (e.g. finding terminal applys and may be useful for other purposes).

I will leave the PR open (and it is independent anyway of the one with the alleged speedup).

[Damiano Testa]

The benchmark on #11896 is in: this is good, right?

[Thomas Murrills]

Josha Dekker said:

can we [@deprecated] tactics (like refine')? Or is this not possible?

This is exactly what motivated #mathlib4 > linting_rules (and foo_rules) (#11520) which allows linting syntax by providing match alts (and can deprecate it) :) (I’m also interested in making a code action.)

[Thomas Murrills]

By the way, #8364 (refine?, which tells you which _’s need to become ?_’s) might also be relevant to this thread. (It’s stalled since its dependencies (#8503) need to be split up, and I haven’t had the motivation/time to do so yet.)

[Damiano Testa]

I went back to the speed ups using Scott's count heartbeats and on the file that most improved, there was exactly one refine' that was really slow. These are the timings

--  Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
--  affineLocally_of_isOpenImmersion
    · exact
        @IsLocalization.away_of_isUnit_of_bijective _ _ _ _ (_) _ isUnit_one Function.bijective_id
/-
heartbeats using `exact`   in 10 runs: Min: 747 Max: 865
heartbeats using `refine`  in 10 runs: Min: 747 Max: 865
heartbeats using `refine'` in 10 runs: Min: 72431 Max: 72549
-/

[Damiano Testa]

I am thinking of automating these tests: whenever there are two tactic sequences that achieve the same result, there should be an easy way to get the timings and use the quickest.

[Damiano Testa]

For instance, hint could use this information to print the fastest solution, when it finds one.

[Kim Morrison]

I think hint is not really the best avenue for this. It really should be suggesting the most stylistically canonical solution, regardless of speed.

[Damiano Testa]

Ok, fair enough!

[Damiano Testa]

Btw, this experiment made me wonder whether replacing some exacts by refines could result in speedups somewhere. :upside_down:

[Markus Himmel]

We're considering moving the refine' linter up to core, with an eye towards dropping support for refine' (and have' and let') entirely at some point in the future. @Damiano Testa, would you be happy with your linter moving to core?

[Damiano Testa]

Yes, of course!