metaprogramming/refactor challenge: named arguments

Stream: mathlib4

[Johan Commelin]

Mathlib has tonnes of statements like this

theorem inf_right_comm (a b c : α) : a ⊓ b ⊓ c = a ⊓ c ⊓ b :=
  @sup_right_comm αᵒᵈ _ a b c

In Lean 4 we can now write this as

theorem inf_right_comm (a b c : α) : a ⊓ b ⊓ c = a ⊓ c ⊓ b :=
  sup_right_comm (α := αᵒᵈ) a b c

I claim that even in simple cases like this, the resulting proof is more robust.

In cases like

@LinearIndependent.restrict_of_comp_subtype _ _ _ id _ _ _ _ (hs.linearIndependent_extend _)

or

Continuous (@selfAdjointPart R A _ _ _ _ _ _ _ _)

the result will also be shorter and more readable. I think it is one (mild) form in which we can clean up "technical debt".

I think it should be possible to have a Lean meta-program that refactors mathlib to automatically transform to the new syntax. I also think it will be quite a non-trivial program, and it is certainly not within my current skill set.

So I'm posing it as a challenge :grinning:

[Johan Commelin]

One way in which the new style is less robust is:

• if the arguments get renamed. But I hope that in the near future we will have tools to help with that.

Ways in which the new style is more robust:

• if the arguments are reordered, then named arguments don't notice
• if the number of arguments changes (hypothesis turns out to be redundant, or some typeclass is changed to a mixin, etc...) then named arguments don't notice.

[Eric Wieser]

My understanding is that the challenge is that we can't easily go from source -> syntax -> source while preserving formatting in the rest of the file

[Joachim Breitner]

Not my area of expertise, so I’m making things up as we go, but could this be a custom elaborator that somehow runs before the normal function application elaborator, recognizes the unwanted pattern, then elaborates as usual, but produces a code action to update it with the other form?

[Johan Commelin]

But such a code action needs to be executed manually from VScode, or something? Or can that be automated?

[Eric Wieser]

I think the missing piece is a function of signature along the lines of

def transformSource (s : String) (f : Syntax → M (Option Syntax)) : String

which outputs the source verbatim, except for where f requests a modification by returning a some

[Eric Wieser]

It's easy to write this today if you're happy to reformat everything

[Johan Commelin]

I would love to see the output of such a formatter

[Joachim Breitner]

Johan Commelin said:

But such a code action needs to be executed manually from VScode, or something? Or can that be automated?

Not yet, I fear, but using guard_msg in test suites creates a very strong demand for something like that.

[Eric Wieser]

Johan Commelin said:

I would love to see the output of such a formatter

It's the default mathport output style, right?

[Kim Morrison]

Why is it necessary to reformat everything? The Lean frontend makes it pretty easy to take a String representing an entire file, chunk it into substrings corresponding to individual commands, and obtain the Syntax for each command separately.

[Eric Wieser]

That still entails reformatting entire theorems, right?

[Kim Morrison]

Yes.

[Mario Carneiro]

how is that different from reformatting the whole file?

[Mario Carneiro]

an actually targeted edit would only modify the substrings corresponding to applications we actually want to change

[Kim Morrison]

You only reformat the commands in which you want to make a change. Of course it would be nice if we could do even better, but we can do better than reformatting a whole file.

[Moritz Doll]

A rather boring problem with this challenge is that not all arguments are named (in particular instance arguments), so it is not always possible to remove the @ notation.