Zulip Chat Archive

Stream: new members

Topic: Confused by "failed to synthesize type class instance" error

Sara Fish (Jul 17 2020 at 19:04):

To practice writing definitions, I am trying to define what it means for an element $g$ of a group $G$ to generate $G$. I have the definition

def is_generator (G : Type) (g : G) [group G] :=
 h  G,  k  , g^k = h

This gives the error

failed to synthesize type class instance for
G : Type,
g : G,
_inst_1 : group G,
h : G,
H : h  G,
k : ?m_2
 has_mem ?m_2 Type

What does this mean? How can I fix this definition?

Dan Stanescu (Jul 17 2020 at 19:05):

Use k : \N instead of k \in \N in your definition.

Sara Fish (Jul 17 2020 at 19:07):

Ah, thanks. So \in is for sets specifically and : is for when something is just any term of that type?

Carl Friedrich Bolz-Tereick (Jul 17 2020 at 19:10):

exactly (this also confuses me often)

Kyle Miller (Jul 17 2020 at 19:50):

I found it to be helpful to look carefully at the definitions for how set membership works. A term s of set X is nothing more than a function X → Prop, and for sets x ∈ s is defined to be s x. (See set.mem, which is attached to the notation through the has_mem instance on the next line).

So, a "set" in Lean is more like a subset of a given type, and it is given by an indicator function.

You can turn a set into a type using subtype, which is usually done either through an automatic coercion in certain places or by up arrow notation. As an example of an automatic coercion, you can write the binder x : s when s is a set. But then x is a slightly different thing, where x.val is the actual term in X and x.property is the proof that x ∈ s.

Maybe it's also worth knowing that when you write ∀ x ∈ s, ... it's equivalent to ∀ (x : X) (H : x ∈ s), ....

Carl Friedrich Bolz-Tereick (Jul 17 2020 at 19:59):

thanks for this detailed explanation!

Last updated: Dec 20 2023 at 11:08 UTC