to_extending

Stream: general

[Patrick Massot]

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]

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]

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

[Patrick Massot]

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

[Kevin Buzzard]

All the simp tags need transporting over as well.

[Mario Carneiro]

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]

@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]

I think the magic might be limited to structure members

[Patrick Massot]

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

[Patrick Massot]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Scott Morrison]

Ugh, I just ran into this again too.

[Sebastian Ullrich]

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]

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