I can't have Lean infer a type class instance

Stream: Berkeley Lean Seminar

[Kentarô YAMAMOTO]

I have been playing around the following snippet I wrote in which I attempted to show that every Boolean algebra is an ortholattice:

import order.bounded_lattice
import order.boolean_algebra

universe u

structure ortholattice (α : Type u) extends bounded_lattice α, has_neg α :=
  mk :: (neg_is_compl : ∀x : α, is_compl (-x) x)

namespace boolean_algebra

instance to_ortholattice {α : Type u} :
  has_coe (boolean_algebra α) (ortholattice α) :=
begin
  constructor,
  intro b,
  constructor,
    show has_neg α,
    have neg := (λ (x : α), -x),
    sorry,
end
end boolean_algebra

Ortholattices have negations, and so do Boolean algebras. I want to construct a term of type has_neg α and I want to just use that coming from α being a boolean algebra, but I get:

18:29: failed to synthesize type class instance for
α : Type u,
b : boolean_algebra α,
x : α
⊢ has_neg α

What is going on?

[Kyle Miller]

I think it's because you're not asserting there is an instance boolean_algebra α. If you change the beginning of the instance definition to the following, it seems OK:

instance to_ortholattice {α : Type u} [boolean_algebra α] :
  has_coe (boolean_algebra α) (ortholattice α) :=
...

[Kyle Miller]

I think you might want to be defining your ortholattice as a class, and then provide an instance of ortholattice given boolean_algebra (assuming the ortholattice structure is unique)

[Kyle Miller]

Like this:

import order.bounded_lattice
import order.boolean_algebra

universe u

class ortholattice (α : Type u) extends bounded_lattice α, has_neg α :=
(neg_is_compl : ∀x : α, is_compl (-x) x)

namespace boolean_algebra

instance to_ortholattice {α : Type u} [boolean_algebra α] :
  ortholattice α :=
begin
  ...
end
end boolean_algebra

[Kyle Miller]

(as I understand it, class/instance gives a way to define structures and specific instances of those constructors in such a way that Lean will automatically supply you with one of those instances when you request it with the [...] argument notation. It's a bit more free-form than Haskell's typeclasses, if you're familiar with those.)

[Kentarô YAMAMOTO]

Thank you (also thank you for spotting my error in typing structure instead of class...)