lean4#2074 (new-style structures)

Stream: mathlib4

[Reid Barton]

Here is an idea that is maybe too dumb to put on github: what if we modify the class command to add some do-nothing class to the start of all extends lists?

[Eric Wieser]

I don't think that works

[Reid Barton]

I guess structure constructor notation would need adjustments too

[Eric Wieser]

The do nothing class has to overlap with all the other classes in order to prevent them getting projections

[Reid Barton]

Oh I just assumed Lean always copied all classes besides the first.

[Reid Barton]

Maybe that's why I had a little trouble trying to reduce the size of the example in 2074

[Eric Wieser]

I think it copies only the ones that don't overlap with anything it's seen so far

[Reid Barton]

Experimentation suggests that you are correct.

[Reid Barton]

But maybe if the do-nothing class just contains a proof of true, then all the classes actually would overlap?

[Reid Barton]

It would be nicer to just have eta work. Maybe we should revisit the example that caused it to be disabled during TC synthesis

[Eric Wieser]

That proof of true approach sounds promising to me, assuming there's no proof irrelevance optimization going on

[Eric Wieser]

That would also unblock porting without rushing people looking for insight on what the right thing to do about TC synthesis is.

[Reid Barton]

Actually in 2074 the classes are all empty already

[Eric Wieser]

I don't think that's relevant

[Eric Wieser]

Or maybe derived extends empty_base is considered not empty

[Reid Barton]

It's not relevant to 2074 but it does mean that Lean is already creating parent class instances with constructors in this situation

[Eric Wieser]

Ah, I think I see what you mean

[Eric Wieser]

So yes, an empty base class for everything algebraic/ordered would likely do the trick

[Yaël Dillies]

That basically amounts to reintroducing old structures, right? (not a bad thing, I like old structures)

[Yury G. Kudryashov]

It seems strange that we move to Lean 4 but we're trying to use new structures as old structures (no, I don't have a better solution).

[Eric Wieser]

It looks like @Gabriel Ebner re-enabled structure eta in typeclass search

[Mario Carneiro]

I think if we want to do this properly, we should add an additional specifier like class Foo extends Bar, @[inline] Baz to say that the fields of Baz should be inlined into Foo even if the fields are all disjoint from previous ones

[Eric Wieser]

I assume attributes are not currently allowed syntactically there?