Zulip Chat Archive

Stream: general

Topic: to_extending


Patrick Massot (Apr 07 2020 at 15:58):

Suppose I have a structure foo, that is not a class and wouldn't make sense as a class. Then I prove lemmas foo.lem1 and foo.lem1 about my structure foo and define a function foo.mk_something. Then I define another structure bar extending foo, which is also not a class. In particular Lean creates bar.to_foo for me. But each time I want to apply my lemmas to x : bar, I need to call x.to_foo.lem1 or x.to_foo.lem1, and the same with x.to_foo.mk_something.

It seems totally within reach of meta-programming to write a command port_lemma foo bar that creates bar.lem1, bar.lem2, bar.mk_something, changing the types of all arguments with type foo and inserting .to_foo everywhere they are used.

Am I talking non-sense? Does this already exist? Could someone do it for me?

Kevin Buzzard (Apr 07 2020 at 16:00):

When bundling algebraic structures I have run into this and I've had some pushback from the CS people because x.lem1 is the same as x.to_foo.lem1 and you are not supposed to duplicate code.

Kevin Buzzard (Apr 07 2020 at 16:01):

If I had it my way we'd have group_hom.map_mul and so on.

Patrick Massot (Apr 07 2020 at 16:01):

Code is not really duplicated if you don't write it.

Kevin Buzzard (Apr 07 2020 at 16:02):

All the simp tags need transporting over as well.

Mario Carneiro (Apr 07 2020 at 21:39):

I think this exact use case already works without any port_lemma command. That is, if you write x.lem1 and x : bar and bar extends foo then the parser will insert a to_foo in there so what the elaborator sees is foo.lem1 (bar.to_foo x)

Patrick Massot (Apr 08 2020 at 12:34):

@Mario Carneiro either you were dreaming or I didn't explain properly:

structure foo :=
(n : )
(n_eq : n = 1)

lemma foo.lem1 (x : foo) : x.n  0 := by rw x.n_eq ; norm_num

structure bar extends foo :=
(m : )

example (x : bar) : x.n  0 := x.to_foo.lem1

example (x : bar) : x.n  0 := x.lem1
/-
invalid field notation, 'lem1' is not a valid "field" because environment does not contain 'bar.lem1'
  x
which has type
  bar
-/

Mario Carneiro (Apr 08 2020 at 12:35):

I think the magic might be limited to structure members

Patrick Massot (Apr 08 2020 at 12:35):

This is the most painful flaw of the Lean 3 elaborator outside type class inference.

Patrick Massot (Apr 08 2020 at 12:35):

Without this issue the manifold files in mathlib would be infinitely easier to read and write.

Mario Carneiro (Apr 08 2020 at 12:35):

which is doubly annoying because there is nothing else that makes structure fields distinguishable from other theorems

Mario Carneiro (Apr 08 2020 at 12:36):

example (x : bar) : x.n = 1 := x.to_foo.n_eq

example (x : bar) : x.n = 1 := x.n_eq

Patrick Massot (Apr 08 2020 at 12:37):

Yes, I knew this works. But it's very far from being sufficient.

Patrick Massot (Apr 08 2020 at 12:38):

Hence my question: should we meta-program away this problem?

Patrick Massot (Apr 08 2020 at 12:38):

Or even better: could someone fix the elaborator in Lean 3.8?

Scott Morrison (Apr 12 2020 at 05:26):

Ugh, I just ran into this again too.

Sebastian Ullrich (Apr 26 2020 at 18:59):

There is at least one issue in that while names of structure fields are unique in a class hierarchy, declaration names in associated namespaces don't need to be, of course. I suppose the sane thing to do would be to raise an error on an ambiguous access, i.e. if the namespaces of two unrelated super structures both define the same name.

Patrick Massot (Apr 26 2020 at 19:46):

Of course there will be ambiguous access, but raising an error sounds fine since we can always give full access information.


Last updated: Dec 20 2023 at 11:08 UTC