dot notation and inheritance

Stream: general

[Sebastien Gouezel]

I find dot notation extremely useful. However, it has some shortcomings. I would like to know if there are ways to avoid them, or if I will have to live with them. Here is a basic example, with a simple class basic, and another class extended that extends it. If basic has a field n, then a.n works for a : basic, and b.n works for b : extended (I guess by some parser trickery) but it is displayed as b.to_basic.n in a proof state (in tactic mode). Let me now define a function basic.foo doing whatever. Then a.foo works, as well as b.to_basic.foo, but b.foo doesn't (because the parser (?) is looking for a function extended.foo as b has type extended).

[Sebastien Gouezel]

Working example:

structure basic := (n : ℕ)

structure extended extends basic

lemma basic.foo (a : basic) : a.n = a.n :=
begin
  -- goal is a.n = a.n
  refl
end

lemma foo_ext (b : extended) : b.n = b.n :=
begin
  -- goal is (b.to_basic).n = (b.to_basic).n
  -- refl -- works
  exact b.to_basic.foo -- works
  -- exact b.foo -- doesn't work
end

[Sebastien Gouezel]

In python, there is a mechanism by which, if a class doesn't have some attribute, then the system will look for the attribute in classes it inherits from. So, in the above example, it would find b.foo. I have two questions:

• is there a way to make this work in Lean?
• In the proof state, is there a way to display b.n instead of b.to_basic.n?

A positive answer to any of these questions would improve the situation a lot for me, as proofs with nested structures become very messy otherwise. This is all for new style structures, by the way.

[Floris van Doorn]

I don't think there is a good structured way to do this.

A hackish way that might help a bit with (2): you could do something like local postfix ↟:max := extended.to_basic.

[Kevin Buzzard]

A related issue is that group_hom.map_muldoesn't exist even though this is what a mathematician would guess it was called. I just want to make more fields to fix it but I am told by the CS guys that instead I have to write good docs

[Kevin Buzzard]

The docs are supposed to contain a dictionary between what you want to call it and what you have to call it

[Sebastien Gouezel]

Well, what prevents you from defining it (as a lemma, I mean, not as a field)?

[Kevin Buzzard]

Apparently they don't even want the namespace to exist

[Kevin Buzzard]

I don't understand why. You can fix your issues by just defining some stuff, right? Or is it worse than that?

[Kevin Buzzard]

Use the old structure command and just hack things out. That solves your problems right?

[Kevin Buzzard]

I'm sorry I can't check, I'm away from Lean

[Sebastien Gouezel]

You don't need the namespace to exist, you can define the lemma group_hom.map_mul if you like.
My issues are not reallyproblems I can't solve, but things that could be massively improved. Maybe in Lean 4.

The old structure command is not really a solution, as it means you need to restate all your lemmas in the new namespace. What I would like to avoid is code duplication, and clutter in the proofs.

[Kevin Buzzard]

I don't understand what the problem with code duplication is. Who cares?

[Kevin Buzzard]

Mathematicians want group_hom.map_mul because it's what it's called. I couldn't care less if the parser just ate group_hom and replaced it with monoid_hom -- as far as I am concerned these two tokens are syntactically equal but I want to be able to tell lean's pretty printer what I want to see because mathematicians simply do not care about monoids and it makes the software more intimidating

[Kevin Buzzard]

@Sian Carey has taught me a lot of things about how a good mathematician who is a complete beginner in Lean still has to wrestle with group homomorphisms

[Floris van Doorn]

I agree that is_group_hom.map_mul should exist. What is the argument against it? We already have both is_mul_hom.map_mul and is_monoid_hom.map_mul. I understand that generally we don't want to state the same lemma twice, but for the sake of projection notation, it seems useful.

[Sebastien Gouezel]

I don't understand what the problem with code duplication is. Who cares?

Suppose I have developed a theory of local_equivs (partially defined bijections), with 50 lemmas on how the source and target of a local equiv interact with composition, restriction, and so on. And then I want to build local homeomorphisms. With a new style structure, I need to write e.to_local_equiveverywhere. With the old style structure, I need to copy my 50 lemmas to the new setting. And then when I improve local equivs by adding a lemma, or changing the order of parameters, or renaming the lemmas, then I need to update also the local homeomorphisms file, as otherwise things are not coherent any more. In both cases, this is very frustrating.

I started with new style, then I got tired of all this to_local_equiv, so I switched to old style, but this is becoming a maintenance nightmare, so I am considering to move back to new style. Not to mention that I started without coercions, then I realized that coercions are used everywhere with respect to equivs, so I switched to coercions, but this is creating problems down the hill (coercions need the type to be fully elaborated, so I have to add a lot of annotations). So I am considering removing the coercions again... This is really hard to get right. After experimenting with everything, it seems that I will end with new style structure, and no coercion. Unless someone here convinces me to switch again :)

[Andrew Ashworth]

Sounds like we should add something to vscode so that autocomplete will work such that you could type foo.tle (key combination) and have it be expanded out to foo.to_local_equiv

[Sebastien Gouezel]

Sounds like we should add something to the parser so that, if it sees e.foo for eof type local_homeomorph and there is no local_homeomorph.foo, then it goes down the line of inheritance for local_homeomorph (exploring the ancestors either breadth-first or depth first or something more complicated as in Python, I don't mind) looking for somehting named foo in one of these namespaces, and uses the first one it finds.

Except that "we" doesn't mean "me" because this is way above my league, so I don't see this done any time soon: people who could do it have more important things to do!

[Chris Hughes]

How about just map_mul instead of group_hom.map_mul? And the docstribg should mention it doesn't work for semiring_hom, which should be renamed ring_hom

[Andrew Ashworth]

I am optimistic your wish can be fixed in Lean 4. If the parser is as extensible as claimed, we should be able to traverse the scope symbol tables as you describe (maybe, hopefully, disclaimer: haven't looked at lean 4 source).

[Sebastien Gouezel]

I hope so too. Let's wait for Lean 4 then!