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

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