Zulip Chat Archive

Stream: new members

Topic: extending from the same type class in 2 different ways


view this post on Zulip Charlie Conneen (May 14 2020 at 04:49):

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.

view this post on Zulip Charlie Conneen (May 14 2020 at 04:50):

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

view this post on Zulip Yury G. Kudryashov (May 14 2020 at 04:52):

Try using set_option old_structure_cmd true before all your classes.

view this post on Zulip Yury G. Kudryashov (May 14 2020 at 04:53):

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.

view this post on Zulip Johan Commelin (May 14 2020 at 04:54):

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

view this post on Zulip Charlie Conneen (May 14 2020 at 04:56):

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.

view this post on Zulip Johan Commelin (May 14 2020 at 04:58):

#mwe

view this post on Zulip Johan Commelin (May 14 2020 at 04:58):

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

view this post on Zulip Charlie Conneen (May 14 2020 at 05:06):

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.

view this post on Zulip Johan Commelin (May 14 2020 at 05:17):

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

view this post on Zulip Johan Commelin (May 14 2020 at 05:18):

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

view this post on Zulip Johan Commelin (May 14 2020 at 05:18):

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

view this post on Zulip Yury G. Kudryashov (May 14 2020 at 05:56):

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

view this post on Zulip Charlie Conneen (May 14 2020 at 06:38):

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

view this post on Zulip Johan Commelin (May 14 2020 at 06:38):

That's great! :thumbs_up:

view this post on Zulip Kevin Buzzard (May 14 2020 at 06:40):

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.


Last updated: May 10 2021 at 00:31 UTC