Coercing list to set?

Stream: new members

[Siddharth Bhat]

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))

1. How do I get a set out of a list to compute the closure, and
2. What's the usual way one works with finite/computable objects in the context of mathlib?

[Kevin Buzzard]

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]

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]

You can also easily coerce from a finset to a set

[Kevin Buzzard]

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]

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]

Note that your group instance already exists, it's docs#equiv.perm.perm_group

[Eric Wieser]

If you mark S @[reducible] then lean will find it for you

[Siddharth Bhat]

Thanks! What's the precise difference between @[simp] and @[reducible]?

[Siddharth Bhat]

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]

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]

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]

The kernel does not care about reducibility.

[Anne Baanen]

(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.)