Insert for Finset α

Stream: new members

[Mark Fischer]

As I understand it, the following creates a singleton set, then inserts the second Nat

def a : Finset Nat := {1, 2}

The same doesn't work in the following:

inductive E where | e1 | e2
def b : Finset E := {e1, e2}

I imagine that there's some Typeclass instance missing for E, which Nat has. Specifically, I would guess I need DecidableEq for E. That's just a gut feeling though. I'm not seeing how to discover this from the documentation.

[Eric Rodriguez]

that is indeed the case, you should be able to see it from the signature of docs#Finset.insert but it is unintuitive. Note that where | e1 | e2 deriving DecidableEq fixes this, although this is just a band aid for not great error messages.

[Mark Fischer]

Right, yeah. deriving DecidableEq does the trick.

[Mark Fischer]

I get a 404 not found for Finset insert

[Eric Rodriguez]

sorry, docs#Finset.instInsertFinset (hard to find)!

[Mark Fischer]

Yup! there it is. Okay, good. I was expecting to find that. It's good that DeciableEq α is in the sig

[Mark Fischer]

Thanks :)

[Kyle Miller]

Here's a searching hint:

import Mathlib.Tactic

variable (α : Type*)
#instances Insert α (Finset α)
/-
1 instance:

Finset.instInsertFinset.{u_1} {α : Type u_1} [inst✝ : DecidableEq α] : Insert α (Finset α)
-/

[Mark Fischer]

I haven't used #instances before.
Oh. That's helpful to know.

[Mark Fischer]

Is it possible to look into an already defined FInset? For example:

def full : Finset Elem := {e1, e2}
example: e1 ∈ full := sorry

[Kevin Buzzard]

by simp [full] and then decide if that didn't do it? Maybe?

[Kevin Buzzard]

Lean won't see through definitions if they're not marked @[reducible] or abbrev

[Mauricio Collares]

import Mathlib.Data.Finset.Basic

inductive E where | e1 | e2 deriving DecidableEq
open E

def full : Finset E := {e1, e2}
example : e1 ∈ full := by decide

works indeed

[Eric Wieser]

It would be really great if Lean could run #instances for you in the error message when elaboration fails to find an instance

[Kevin Buzzard]

Especially as sometimes it's not at all clear to the user that the failure is a missing instance