can set_like be inherited?

Stream: new members

[Matt Diamond]

In Lean 3, if I have a structure type Foo and another type Bar that extends Foo, and Foo has a set_like instance, is there an easy way to extend that set_like instance to cover Bar as well?

[Kyle Miller]

I think in mathlib the set_like instances are given from scratch every time. There's not too much boilerplate at least.

[Kyle Miller]

For example, submonoidextends subsemigroup but you have https://github.com/leanprover-community/mathlib/blob/acee671f47b8e7972a1eb6f4eed74b4b3abce829/src/group_theory/submonoid/basic.lean#L129

[Matt Diamond]

I ended up writing something like this:

instance bar_set_like : set_like bar X := {
  coe := λ b, b.carrier,
  coe_injective' := λ p q h, by {
    cases p, cases q,
    cases p__to_foo,
    cases q__to_foo,
    congr',
  }
}

I'm not sure why cases p, cases q, congr' (the proof used by submonoid) wasn't enough.

I have another type that extends bar and the set_like proof for that is even uglier. I feel like I'm missing an easier proof.

[Eric Wieser]

I would recommend that you first prove that Bar.toFoo is injective

[Eric Wieser]

Then the proof will just be toFoo_injective (set_like.coe_injective h)

[Kyle Miller]

You could also be lazy and check if tidy works. (Eric's suggestion seems more principled.)

[Eric Wieser]

Usually you need injectivity of Bar.toFoo later anyway (for instance, to transfer other structure), so it's useful to prove it directly