Stream: new members
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):
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
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.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: May 10 2021 at 18:22 UTC