# Zulip Chat Archive

## Stream: new members

### Topic: Coercing list to set?

#### Siddharth Bhat (Feb 16 2022 at 09:30):

I'm slowly implementing some computational math (the Schreier Sims algorithm), and I have to coerce a `list`

to a `set`

, because I have a list of generators, which I want to state generate a subgroup. I tried:

```
import group_theory.subgroup.basic
import group_theory.perm.basic
import group_theory.perm.fin
import algebra.group.defs
open list fin function subgroup
@[simp]
def S (n: nat) := (equiv.perm (fin n))
instance (n: nat) : group (S n) :=
{ mul := λ f g, equiv.trans g f,
one := equiv.refl _,
inv := equiv.symm,
mul_assoc := λ f g h, (equiv.trans_assoc _ _ _).symm,
one_mul := equiv.trans_refl,
mul_one := equiv.refl_trans,
mul_left_inv := equiv.self_trans_symm }
def generators (N: nat) (gs: list (S N)) (H: subgroup (S N)) : Prop :=
closure (coe gs) = H
```

but no `coe`

instance was found:

```
failed to synthesize type class instance for
N : ℕ,
gs : list (S N),
H : subgroup (S N)
⊢ has_lift_t (list (S N)) (set (S N))
```

- How do I get a
`set`

out of a`list`

to compute the closure, and - What's the usual way one works with finite/computable objects in the context of
`mathlib`

?

#### Kevin Buzzard (Feb 16 2022 at 09:32):

Are you sure you don't want a `finset`

instead? It's easy to make one of those from a list, and finsets are computable. Sets can be infinite and membership is in general undecidable.

#### Siddharth Bhat (Feb 16 2022 at 09:33):

I'd like to use `finset`

, but it seems to me that most of the definitions in `group_theory.basic`

(eg. that of `closure`

) are written using `set`

. I'm unsure how to interface between the two.

#### Kevin Buzzard (Feb 16 2022 at 09:33):

You can also easily coerce from a finset to a set

#### Kevin Buzzard (Feb 16 2022 at 09:34):

I'm not at lean right now but finset to set is an inbuilt coercion and list to finset is probably docs#list.to_finset

#### Siddharth Bhat (Feb 16 2022 at 09:34):

Yes, changing the declaration to

```
def generators (N: nat) (gs: finset (S N)) (H: subgroup (S N)) : Prop :=
closure (coe gs) = H
```

works. Thanks!

#### Eric Wieser (Feb 16 2022 at 09:37):

Note that your `group`

instance already exists, it's docs#equiv.perm.perm_group

#### Eric Wieser (Feb 16 2022 at 09:38):

If you mark `S`

`@[reducible]`

then lean will find it for you

#### Siddharth Bhat (Feb 16 2022 at 09:42):

Thanks! What's the precise difference between `@[simp]`

and `@[reducible]`

?

#### Siddharth Bhat (Feb 16 2022 at 09:47):

Ah, is it that `@[simp]`

is a hint to the _simplifier_ which must be explicitly invoked with `simp`

, while `@[reducible]`

is a hint to the elaborator which is always applied during elaboration into core?

#### Anne Baanen (Feb 16 2022 at 09:48):

Essentially yes: `@[simp]`

on a definition tells the `simp`

tactic to unfold the definition, while `@[reducible]`

tells the elaborator it is allowed to unfold the definition in more cases. (The elaborator does not always unfold definitions.)

#### Anne Baanen (Feb 16 2022 at 09:51):

By default definitions are semireducible and instances are "instance reducible". You can also mark them as `@[reducible]`

or `@[irreducible]`

. Type checking is allowed to unfold reducible, "instance reducible" and semireducible. Instance search is allowed to unfold reducible and "instance reducible". Most rewriting tactics like `simp`

and `rw`

are allowed to unfold only reducible.

#### Anne Baanen (Feb 16 2022 at 09:51):

The kernel does not care about reducibility.

#### Anne Baanen (Feb 16 2022 at 09:54):

(I put "instance reducible" in quotes because I understand the C++ code has only three transparency levels, `reducible`

, `semireducible`

and `irreducible`

, and "instance reducible" is the combination of `@[instance, semireducible]`

attributes. Or something along those lines.)

Last updated: Dec 20 2023 at 11:08 UTC