old_structure_cmd and mathlib4

Stream: general

[Scott Morrison]

Recall that old_structure_cmd doesn't exist in Lean4.
Instead, Lean4 now has direct support for diamond inheritance.

Thus in Lean4 class Field (α : Type u) extends DivisionRing α, CommRing α produces constructors and projections like:

Field.mk : {α : Type u_1} → [toDivisionRing : DivisionRing α] → (∀ (a b : α), a * b = b * a) → Field α

def Field.toDivisionRing.{u} : {α : Type u} → [self : Field.{u} α] → DivisionRing.{u} α :=
fun (α : Type u) [self : Field.{u} α] => self.1

def Field.toCommRing.{u} : {α : Type u} → [self : Field.{u} α] → CommRing.{u} α :=
fun (α : Type u) [self : Field.{u} α] =>
  @CommRing.mk.{u} α (@DivisionRing.toRing.{u} α (@Field.toDivisionRing.{u} α self)) (@Field.mul_comm.{u} α self)

[Scott Morrison]

Ideally in the long run in Mathlib4 we will be using this implementation. We need to work out how to get there!

[Scott Morrison]

Some alternatives:

1. remove use of old_structure_cmd from mathlib3 before the port
2. during migration, port old_structure_cmd structures by hand to "new" structures, and write automation in mathport to align
3. during migration, implement old_structure_cmd in mathlib4 and automate the port entirely

[Scott Morrison]

If 1. is viable, I'm in favour of it:

• it reduces the work mathport needs to do, saving Daniel's effort for other things
• option 3. seems prematurely pessimistic --- it prolongs the life of the old_structure_cmd hack
• option 2. requires additional work during the port, while option 1. can be done now, while we have lots of refactoring resources available

[Scott Morrison]

That said, even option 1. may require some work in mathport, depending on whether we can remove old_structure_cmd in a way that exactly matches the type signatures that "new structures" generate.

[Scott Morrison]

To this end, yesterday I tried removing some uses of old_structure_cmd from mathlib3. I just worked on the "long-hanging fruit", to get up to speed, and all the cases I tried were either trivial or easy: #9612 #9613 #9614 #9615 #9616 #9617 #9620 #9621 #9622.

[Scott Morrison]

The remaining uses of old_structure_cmd fall mostly into three cases:

• algebraic structures
• algebraic morphisms
• order structures

I suspect that it makes sense to deal with these "all at once" (i.e. 3 seperate refactors), and I'm happy to have a go at these, although if anyone else would like to do some or all please let me know!

[Scott Morrison]

The basic principle of removing old_structure_cmd is:

1. if two parents have overlapping fields, chose a "preferred" one
2. remove the non-preferred parent from the extends clause
3. copy-and-paste the fields of the non-preferred parent into the current structure
4. write to_non_preferred_parent, either as a def or an instance
5. optionally, write a "fully-flattened" constructor that emulates the constructor that old_structure_cmd provided
6. update initialization of simps (see examples in PRs above)
7. patch downstream code as necessary, particularly use of constructors

[Scott Morrison]

(To be clear, the proposal is that after the mathport phase of the mathlib3 -> mathlib4 port, when we are cleaning up files by hand, we will be able to remove these copy-and-paste fields, and restore the non-preferred parent to the extends clause, and Lean4 will then automatically generate to_non_preferred_parent.)

[Scott Morrison]

In the PRs I made so far, it was always obvious which was the "preferred" parent, and it's slightly less so in the remaining cases. I propose the following preferences:

• data over axioms
• additive stuff over multiplicative stuff
• less-algebraic-structure over upgrading-to-equivalences

I'm not sure what other decisions will need to be made.

[Scott Morrison]

So --- in summary:

• If there are reasons I'm missing for not attempting to remove use of old_structure_cmd from mathlib3, please explain them!
• Otherwise, I'll try doing more of this,
• but help is very welcome. :-)

[Mario Carneiro]

When you are doing this, make sure to put an attribute to mark the non-preferred parents as parents

[Eric Wieser]

Won't making this change mean that after telling Leo "hey, we really want direct support for diamonds", that the mathlib port will not end up using them at all?

[Scott Morrison]

Immediately after the automatic port, it won't be using diamonds. Instead, it will be using definitions (manually constructed in mathlib3, automatically ported to mathlib4) which are pretty close to what Leo's solution produces. Then, soon after we're happy with the output of mathport, we will delete these definitions, replacing them with multiple-extends-diamond-inheritance.

[Scott Morrison]

It's just a bridge to get to the point where we are using the direct support for diamonds.

[Scott Morrison]

(But a bridge for which the work can be done "on this side of the gap".)

[Eric Wieser]

Perhaps this is what Mario was saying above, but it sounds like we should tag every such diamond workaround with a comment (library note?) or attribute, to make them easier to find after the port

[Gabriel Ebner]

Is there any indication that old_str_cmd is an issue for the port? I thought we could just ignore it because the nw structure command is more general.

[Scott Morrison]

I think it limits our flexibility as follows. If we do the port as an automated run through mathport "from scratch", and then patch things up afterwards, then yes, we can probably ignore old_structure_cmd. However we're (probably) not doing the port from scratch: we're going to have a partially "by hand" ported mathlib, just enough to support writing essential tactics, and then we're going to run mathport "relative" to that.

As an example, we already have Ring in mathlib4, to support writing the ring tactic, and when mathport runs at the moment it can't align the ported ring from mathlib3 with the Ring in mathlib4 (because the ring in mathlib3 has flattened fields), so we get a Ring (hand-ported) and a Ringₓ (generated by mathport).

That said:

1. Of course we can put more effort (either by hand or automation) into aligning Ring and Ringₓ.
2. There may not actually be many instances of this problem, because tactics don't actually rely much on the algebraic hierarchy, so we don't need to port much "by hand". (And we could re-engineer things to rely even less on the algebraic hierarchy.)

[Scott Morrison]

There's also just the argument that old_structure_cmd is cruft, and deserves to die. :-) The changes I made so far were surprisingly easy, hence the desire to possibly continue.

[Scott Morrison]

Also re: ignoring it --- the fact that there are some changes that need to be made after removing old_structure_cmd (besides just adding the extra to_parent projections) I'm pretty sure means those changes would be needed during the port. Hopefully by removing old_structure_cmd ahead of time we can make the port have fewer moving pieces.

[Scott Morrison]

Maybe I am being wildly optimistic about getting alignment for ring without further tweaking or further cleverness in mathport.

[Eric Wieser]

Which of the PRs you link above actually involve diamonds?

[Gabriel Ebner]

we're going to have a partially "by hand" ported mathlib, just enough to support writing essential tactics

I wonder how realistic it is to align these classes. There are a lot of changes in core that affect them. For example OfNat vs. has_zero/has_one/has_add. As a result, the mathlib4 instances are significantly different than the Lean 3 ones. The encoding scheme for inheritance seems like the least of our worries here.

[Gabriel Ebner]

so we get a Ring (hand-ported) and a Ringₓ (generated by mathport).

This is not necessarily a huge problem btw. We can add an instance [Ringₓ R] : Ring R where ... and then the tactic should work.

[Eric Wieser]

A consequence of removing old_structure_cmd comes up in #9774; default field values in parent structures no longer work, meaning we need custom mk' constructors and have to replace something readable like { carrier := C, mul_mem' := h_mul, add_mem' := h_add, algebra_map_mem' := h_grade0 } with something less readable like mk' C h_mul h_add h_grade0. Are we convinced that removing old_structure_cmd is actually useful enough to the porting effort to justify losing readability?

[Kevin Buzzard]

It's nothing to do with "we", right? Leo has been arguing since about 2017 that old structures are terrible for internal reasons involving horrible blow-up of term size. It took us 4 years to listen to him, but when we started having slowdowns this was diagnosed as the cause. Old structures aren't in Lean 4 and I am pretty sure that they will not be being added to Lean 4 any time soon.

[Kevin Buzzard]

On the other hand, making cool custom constructors which can do the kind of thing which you're missing is surely well within the scope of Lean 4's fancy macro system

[Eric Wieser]

It took us 4 years to listen to him, but when we started having slowdowns this was diagnosed as the cause.

Do we have any data that shows replacing structures in mathlib with new-style ones actually improves performance?

[Kevin Buzzard]

I think Leo has ample data for him to have made this decision, and indeed he has had it since 2017.

[Eric Wieser]

Old structures aren't in Lean 4 and I am pretty sure that they will not be being added to Lean 4 any time soon.

But that's not really relevant, because the new structures in lean4 come with all the behavior we needed from the old structures in the first place.

[Kevin Buzzard]

I think the fix for your issue is to make a fancy new constructor thing and not to start thinking about old structures again.

[Kevin Buzzard]

https://github.com/leanprover/lean/wiki/Refactoring-structures is Leo's explanation

[Kevin Buzzard]

You have seen the benefits of a super-fine-grained algebra heirarchy, indeed you have contributed to making it even more complex and this idea seems to make maths in Lean better. But Leo says that this + old structures makes complex algebra classes "monstrosities behind the scenes".

[Eric Wieser]

My reading of that page is that eliminating old structures is only half the solution, the other half is redesigning the algebra heirarchy to not carry the data so that it has no diamonds

[Eric Wieser]

And I think the plan to do that half was abandoned long ago

[Scott Morrison]

Eric Wieser said:

But that's not really relevant, because the new structures in lean4 come with all the behaviour we needed from the old structures in the first place.

No, this part is just not the case. The way I am removing old_structure_cmd at the moment is by replacing it with a rough approximation of what Lean4's new structure command will produce. It will be nicer in Lean4 --- we won't have to write out the "non-preferred parent fields" by hand, and we won't have to write the to_other_parent declarations ourselves, but they will be produced under the hood.

Thus, to a first approximation all the changes that need to be made downstream (i.e. after doing those two things) are changes that will need to be made to the library for mathlib4 in any case. Given the choice of doing it now, or doing it mid-port, when many other things are going on as well, and many things are broken, I would far prefer to get it done now.

It's true that the thing Eric is annoyed about here (having to write a separate constructor when you use multiple inheritance and fill in some of the preferred-parent fields using default values) will be better in Lean4 than we can currently achieve (I think?). But we can readily change this back after mathlib4 is the official version (i.e. change a few subalgebra.mk' back to structure literals), at very little expense compared to the peace of mind of knowing that mathlib is possible without old_structure_cmd.

[Mario Carneiro]

I don't see how what you say contradicts what Eric said. We used old_structure_cmd for years because "new structures" banned diamonds, and this was not an acceptable solution. Lean 4's "newer" structure command is a hybrid that allows diamonds but is otherwise new-structure-like.

[Mario Carneiro]

It is not clear to me that performing a mathlib refactor to remove old_structure_cmd is necessarily all that helpful for the port. It is good to know if the refactor will hit any major roadblocks, so doing the exploration now is fine, but actually applying the refactor might be counterproductive for synport, since it would prefer to see actual structure instance syntax rather than foo.mk', and similarly for extends in structures.

[Scott Morrison]

Okay -- but these refactors (unlike the earlier ones) are resulting in lots of changes downstream being required. We really don't want to have to be making those changes "mid-port".

[Scott Morrison]

Further, the experiments only work step by step. I can only remove old_structure_cmd from something once its has been removed from all descendants. I can't really keep going unless we actually apply the earlier stages.

[Scott Morrison]

Could we think about how to remove uses of old_structure_cmd, but to leave some indication (just the @[ancestor] attribute?) so that synport can automatically write new structure commands?

This had seemed to me like unnecessary extra work in synport: my thought had just been to do the translation from "by hand newer structures" to "actual newer structures" as a late step in the port, by hand. But we could also automate it.

[Scott Morrison]

But really my main point is just the above: changing from old structures to newer ones is not completely trivial, and already we're going to have a million things broken in the output of synport, and I think if we can make changes ahead of time we should.

[Gabriel Ebner]

I agree with Mario. For synport it would be better to have "idiomatic Lean 3", because that is most likely to map to idiomatic Lean 4. If you don't look under the hood, the Lean 3 old_structure_cmd and Lean 4's structure command behave very similarly. (The only real difference I can think of is how the cases tactic behaves, but maybe we should change that in Lean 4 instead.)

[Scott Morrison]

Okay! We'll give it a go that way, I guess. :-) I remain pretty worried about how much stuff is going to be broken even with the most optimistic view of what synport can achieve, but we'll get there somehow.

[Scott Morrison]

I have some PRs #9719 #9739 #9748 that remove one or two old_structure_cmd, but only incidentally (really they are about making domain and integral_domain mixins, and in fact combining them into a single is_domain). They'll stay on the queue, but #9774 can be abandoned.

[Sebastien Gouezel]

There is still a big difference that, in Lean 4, we will need to choose a preferred parent for the data fields, right? And this choice should be made with conscious design decisions, because this will have an impact performancewise. Currently, there is no way synport will have this kind of information available.

[Gabriel Ebner]

But it does? Synport can just write the extends clause in the same order.

[Sebastian Ullrich]

And hopefully the performance impact isn't any worse than old structures to begin with, so this could be optimized after porting

[Sebastien Gouezel]

What if you have foo with fields A, B, C and bar with fields A, B, D, and you want a class extending foo and bar to pick A, C from foo and B, D from bar? (This is the kind of stuff that you see all the time in the algebraic hierarchy).

[Mario Carneiro]

With the lean 4 structure command, you get foo as preferred parent and D as a mixin from bar; I don't know what it would mean to pick A, C from foo and B, D from bar

[Mario Carneiro]

in lean 3 old structures you always merge all common fields, so there is no half and half thing

[Mario Carneiro]

i.e. you get one class with A, B, C, D and the forgetful functors to foo and bar do the obvious thing

[Mario Carneiro]

There is no constructor that takes a complete foo and a complete bar and mixes and matches fields; this would almost certainly lead to type errors due to the existence of non-defeq foo.A and bar.A in the context