extending from the same type class in 2 different ways

Stream: new members

[Charlie Conneen]

I've run into the issue

"invalid 'structure' header, field 'class W' from 'class Y' has already been declared."

This is because I want a class Z that extends from both class Y and class X. The issue is, class X and class Y are both extensions of class W. I would like to keep classes X and Y as they are, but I don't know how to handle construction of class Z if I'm not allowed to inherit from class W twice. In other words, the following diagram cannot be constructed:

class W -----> class X
  |                 |
  v                 v
class Y   -----> class Z

where arrows are extending to a class. Is there a nice way to clean this up? I would rather not have to list out all the hypotheses from either X or Y in the construction of Z, if that is avoidable. Obviously I could do that, but I would much rather keep the structure of Z inheriting from both X and Y, if possible.

[Charlie Conneen]

sorry, it ate my whitespace, so the formatting is all gross. But I think it should be clear what I meant

[Yury G. Kudryashov]

Try using set_option old_structure_cmd true before all your classes.

[Yury G. Kudryashov]

By default Lean creates to_W field in X and Y. With old_structure_cmd it will duplicate all fields from W in X and Y and define a function to_W.

[Johan Commelin]

Charlie Conneen said:

sorry, it ate my whitespace, so the formatting is all gross. But I think it should be clear what I meant

#backticks

[Charlie Conneen]

set_option old_structure_cmd true seems to have broken some of my proofs. Specifically, when proving a field is a vector space over itself, it now doesn't understand that multiplying two scalars and scaling a vector use the same operation.

[Johan Commelin]

#mwe

[Johan Commelin]

This has already been done in mathlib. Have you checked how it's solved there?

[Charlie Conneen]

Yes. Because a field is a ring, and a ring is a module, the proof is immediate when a vector space is defined as a module over a field (since then a field over a field is also a module over a field). As an exercise, I was defining a vector space directly from its axioms, and proving statements about it.

[Johan Commelin]

I don't think using rings and modules makes the problem any easier or harder.

[Johan Commelin]

Why is a ring a module over itself, in mathlib?

[Johan Commelin]

For exactly the same reason, a field can be a vector space over itself in your own code.

[Yury G. Kudryashov]

It's hard to tell why your code doesn't work without looking at the actual code.

[Charlie Conneen]

I resolved the issue and gained clarity from what's already been said. Thank you for the help!

[Johan Commelin]

That's great! :thumbs_up:

[Kevin Buzzard]

This old_structure_cmd stuff is just one of several things which is obscure to discover and breaks stuff which "should be obvious". The easiest way to resolve things like this is just literally to post a #mwe and ask "why doesn't this code run?". Experts can fix issues quickly here making it easier for mathematicians to proceed. I know things could be better. We're working on it.