extending instances

Stream: general

[Kevin Buzzard]

What's the sensible way to get the bounded lattice instance when type class inference knows all the ingredients? by apply_instance doesn't work for me.

import order.conditionally_complete_lattice

open lattice

variables {α : Type*} [conditionally_complete_lattice α]

example : lattice (with_bot (with_top α)) := by apply_instance -- with_bot.lattice
example : order_bot (with_bot (with_top α)) := by apply_instance -- with_bot.order_bot
example : order_top (with_bot (with_top α)) := by apply_instance -- with_bot.order_top

-- class bounded_lattice (α : Type u) extends lattice α, order_top α, order_bot α

example : bounded_lattice (with_bot (with_top α)) := by sorry

[Mario Carneiro]

I think {} works

[Mario Carneiro]

If not, {..instance1, ..instance2} should

[Kevin Buzzard]

I had trouble with both of these approaches. Hang on.

[Mario Carneiro]

Note that this is expected behavior. There is no instance deriving a subclass from its parents, even if there are no fields. You have to explicitly instantiate the substructure

[Kevin Buzzard]

{} gives 17 errors of the form

invalid structure value { ... }, field 'inf' was not provided

[Mario Carneiro]

this works for me:

example : bounded_lattice (with_bot (with_top α)) :=
{..with_bot.lattice, ..with_bot.order_bot, ..with_bot.order_top}

[Mario Carneiro]

Oh I see, it's because bounded_lattice is an old style structure

[Kevin Buzzard]

Yup, works for me too. Thanks.

[Kevin Buzzard]

While I'm here, what's the idiomatic way for getting set X from set (with_top X)?

[Mario Carneiro]

When you use a new style structure, these parents are inferred by type class inference, but with an old style structure the fields are splayed and reconstructed, so you need {.. foo} to construct the instance

[Kevin Buzzard]

i.e the intersection.

[Mario Carneiro]

I guess that would be coe '' X

[Mario Carneiro]

or rather coe ⁻¹' X

[Kevin Buzzard]

right. Thanks.