old_structure_cmd

Stream: mathlib4

[Winston Yin]

I understand that old_structure_cmd has been removed from Lean4. Does this mean that we have to manually restore the long chains of dots, e.g. LinearEquiv.AddEquiv.AddHom.toFun instead of LinearEquiv.toFun? How are the field diamonds handled then, e.g. LinearEquiv.AddEquiv.AddHom.toFun vs LinearEquiv.AddEquiv.Equiv.toFun?

[Jireh Loreaux]

I think the way it works is that when you write extends, if there are overlapping fields, then only the first thing you are extending is the "true" ancestor and the extra fields from the second structure get inlined. That means that the fields that have overlapping names are really taken only from the first structure.

Someone please correct me if I'm wrong.

[Jireh Loreaux]

I'm not sure if the chains of dots are necessary or if there is a better way.

[Mario Carneiro]

the chain of dots should not be necessary (neither in lean 3 or lean 4)

[Winston Yin]

Consider the Lean3 code:

set_option old_structure_cmd true

structure monoid_hom (M : Type*) (N : Type*) [mul_one_class M] [mul_one_class N]
  extends one_hom M N, M →ₙ* N

#check monoid_hom.to_fun -- ... (M →* N) → M → N

In Lean4 without the old structure, a function like monoid_hom.to_fun would have to be rewritten as fun f : MonoidHom M N => f.toFun.

[Eric Wieser]

then only the first thing you are extending is the "true" ancestor and the extra fields from the second structure get inlined

Does this mean we can emulate the old behavior by adding

structure old_structure_base.

and always using this as the first ancestor?

[Mario Carneiro]

no, because as long as the fields are disjoint you can still have multiple "preferred parents"

[Mario Carneiro]

you would need old_structure_base to have a copy of every field, and this would cause problems of its own

[Eric Wieser]

If A extends B and C, C extends D, B and D have disjoint fields but B shares a field with C, is D a "preferred parent" of A?

[Mario Carneiro]

I believe so

[Mario Carneiro]

that is to say, it is a field of A

[Mario Carneiro]

because C is splatted into A which pulls all the fields in, including toD

[Winston Yin]

Here's a strange behaviour. Given that MonoidHom extends OneHom, and the latter has a toFun field, #check MonoidHom.toFun gives the error unknown constant. As above, one has to do fun f : MonoidHom M N => f.toFun for the intended effect. However, def MonoidHom.toFun ... fails as well, with the error structure 'MonoidHom' has field 'toFun'.

So basically I'm neither able to use MonoidHom.toFun, nor allowed to define it?