finset <-> boolean algebra, universes

Stream: new members

[Eric Meinhardt]

I'd like to associate every finite set (over a finite type with decidable equality) with its boolean algebra, i.e. make use of https://github.com/leanprover-community/mathlib/blob/40b6b45c052e188122ec9a25e8aedf00232e4633/src/data/fintype/basic.lean#L125

My reading of the typeclass instance there is that for every α s.t. fintype α and decidable_eq α, every s : finset α has a boolean algebra instance associated with it. How do I actually make use of this to associate any particular s : finset α with its boolean algebra instance?

-- typechecks
def foo {α : Type _} [fintype α] [decidable_eq α] : boolean_algebra (finset α) :=
  finset.boolean_algebra

-- tweak of foo whose explicit type is what I think I want
def bar {α : Type _} [fintype α] [decidable_eq α] (h : finset α) : boolean_algebra h :=
  finset.boolean_algebra

results in the following error on the body of bar:

type mismatch, term
  finset.boolean_algebra
has type
  boolean_algebra (finset ?m_1) : Type ?
but is expected to have type
  boolean_algebra ↥h : Type ?

My current guess as to the meaning of the error is something related to universes?

[Henrik Böving]

I'd say that the precise thing you are asking for here is not possible, you want to return an instance of a typeclass on a specific term of a type but that is not possible, the boolean_algebra typeclass can only be implemented by types themselves. That is, the mathlib boolean algebras are (to my understanding of the types, I don't actually have a clue of the mathematics involved here) not defined over a concrete carrier set of values but rather over an entire type.

[Eric Wieser]

When you say boolean_algebra h lean is translating it to boolean_algebra (coe_sort h), which is what that funny arrow means

[Eric Wieser]

docs#finset.has_coe_to_sort implements that arrow as "the type of elements contained in h"

[Alex J. Best]

I don't think your reading of the instance is correct. docs#finset.boolean algebra says that given a finite type \alpha the type of all possible finite subsets has the structure of a boolean algebra, that is there is an algebra structure where the sup of two finite subsets is their union, etc. Each s : finset \alpha doesn't have its own boolean algebra structure, there is just a way to sup finsets.

[Alex J. Best]

If you say a bit more about what you want to use this for then we can try and see how to phrase this in Lean