## Stream: maths

### Topic: fintype issues

#### Kevin Buzzard (Jul 27 2020 at 21:06):

Looks like I'm going to have to engage with fintypes for the first time. They're already driving me nuts. I have managed to construct two proofs that the identity subgroup of a group is a fintype (one uses fintype_set and LEM, the other uses the fact that it's the trivial subgroup). I know I can somehow dig my way out of things with convert or what have you -- but I wouldn't be in this mess if there were a Prop-valued fintype. I remember @Chris Hughes complaining about this when doing Sylow's theorems (we still don't have Sylow 2 or 3 in mathlib, even though he formalised them for his 1st year project two years ago). I'm refactoring subgroup and am having to engage with this proof of Sylow. These problems are completely superficial as far as I can see, and I think they would be solved with an is_fintype typeclass. Does such a typeclass not exist? Is there a call for such a typeclass? Is it nonempty (fintype X)?

Related: I made a little API for fincard:

/-
fincard -- ℕ-valued cardinality of a type (zero for infinite types)
-/
import tactic data.fintype.card

open_locale classical
noncomputable theory

def fincard (X : Type*) :  :=
if h : nonempty (fintype X) then @fintype.card X (classical.choice h) else 0

I proved fincard (X × Y) = fincard X * fincard Y (no finiteness assumptions necessary).

I have students thinking about finite groups and it's so much messier than I want it to be. I'm wondering if there are any tricks which people know about, which haven't been implemented yet.

#### Mario Carneiro (Jul 27 2020 at 21:17):

My suggested proof:

instance subgroup.bot.fintype {G} [group G] : fintype ( : subgroup G) :=
@fintype.of_finset _ ((:subgroup G):set G) {1} \$ by simp

#### Mario Carneiro (Jul 27 2020 at 21:20):

example {G} [group G] : fintype.card ( : subgroup G) = 1 := rfl

#### Kevin Buzzard (Jul 27 2020 at 21:21):

Yeah but the issue is that I'm in the middle of the proof of Sylow's first theorem and rw card_trivial is failing for reasons which I'm finding hard to control.

#### Mario Carneiro (Jul 27 2020 at 21:21):

do you have a representative example aka MWE?

#### Kevin Buzzard (Jul 27 2020 at 21:21):

On a WIP branch of mathlib :-/

#### Mario Carneiro (Jul 27 2020 at 21:22):

a non-compiling example then?

#### Kevin Buzzard (Jul 27 2020 at 21:22):

The question is not "can you fix this proof" -- I can fix it with a convert -- the question is why I'm having to even think about this issue, because my mental model of "this set is finite" is a Prop and I'm hurting because this isn't Lean's example.

#### Mario Carneiro (Jul 27 2020 at 21:22):

I want to see the proof so I can fix it without convert

#### Kevin Buzzard (Jul 27 2020 at 21:23):

In the quotient_group_refactor branch of mathlib, in group_theory.sylow

#### Kevin Buzzard (Jul 27 2020 at 21:23):

wait a second, let me see what state it's in on GH

#### Kevin Buzzard (Jul 27 2020 at 21:24):

https://github.com/leanprover-community/mathlib/blob/86a4929c05bd5807981ced1f469fd0507d998315/src/group_theory/sylow.lean#L201

#### Kevin Buzzard (Jul 27 2020 at 21:25):

I don't know whether that proof works, but sometimes it doesn't. There's a random local attribute [instance] set_fintype before it, and if you remove it then you can observe that it still has the instance attribute anyway.

#### Kenny Lau (Jul 27 2020 at 21:25):

the issue is that rw sees the mismatch between the two different proofs of fintype?

yes

#### Kevin Buzzard (Jul 27 2020 at 21:26):

but there's a bigger issue, which is that people are randomly adding local attribute [instance] set_fintype in an attempt to make things work (I think this just changes the priority of the instance). People are doing some sort of juggling game to try and make the instances fire in the right order. It shouldn't be like this, surely!

#### Kevin Buzzard (Jul 27 2020 at 21:26):

Earlier we have local attribute [instance, priority 10] subtype.fintype set_fintype

#### Kevin Buzzard (Jul 27 2020 at 21:28):

People (perhaps Chris) are having to juggle with instance priorities to make stuff as basic as Sylow's 1st theorem work. There must be a better way. I'm happy to spend some time writing the API for it but I don't know what it is.

#### Mario Carneiro (Jul 27 2020 at 21:29):

fincard seems like a reasonable fix here

#### Mario Carneiro (Jul 27 2020 at 21:30):

another fix would be an is_card s n predicate

#### Kenny Lau (Jul 27 2020 at 21:30):

I support fincard

#### Kevin Buzzard (Jul 27 2020 at 21:30):

In my current unpushed work, the proof that the trivial group is finite is

@fintype.card.{?l_1}
(@coe_sort.{?l_1+1 (max 1 (?l_1+1))+1} (@subgroup.{?l_1} ?m_2 ?m_3) (@subgroup.has_coe_to_sort.{?l_1} ?m_2 ?m_3)
(@has_bot.bot.{?l_1} (@subgroup.{?l_1} ?m_2 ?m_3) (@subgroup.has_bot.{?l_1} ?m_2 ?m_3)))
(@fintype_bot.{?l_1} ?m_2 ?m_3)

and Lean wants it to be

(@fintype.card.{u}
(@coe_sort.{u+1 (max 1 (u+1))+1} (@subgroup.{u} G _inst_1) (@subgroup.has_coe_to_sort.{u} G _inst_1)
(@has_bot.bot.{u} (@subgroup.{u} G _inst_1) (@subgroup.has_bot.{u} G _inst_1)))
(@set_fintype.{u} G _inst_2
(@has_coe_t_aux.coe.{u+1 (max (u+1) 1)} (@subgroup.{u} G _inst_1) (set.{u} G)
(@coe_base_aux.{u+1 (max (u+1) 1)} (@subgroup.{u} G _inst_1) (set.{u} G) (@subgroup.has_coe.{u} G _inst_1))
(@has_bot.bot.{u} (@subgroup.{u} G _inst_1) (@subgroup.has_bot.{u} G _inst_1)))
(λ (a : G),
classical.prop_decidable
(@has_coe_t_aux.coe.{u+1 (max (u+1) 1)} (@subgroup.{u} G _inst_1) (set.{u} G)
(@coe_base_aux.{u+1 (max (u+1) 1)} (@subgroup.{u} G _inst_1) (set.{u} G)
(@subgroup.has_coe.{u} G _inst_1))
(@has_bot.bot.{u} (@subgroup.{u} G _inst_1) (@subgroup.has_bot.{u} G _inst_1))
a))))

Note that the latter has some classical.prop_decidable in. I traced it back to def set_fintype {α} [fintype α] (s : set α) [decidable_pred s] : fintype s :=, whereas the simpler proof comes from fintype_bot.

#### Kevin Buzzard (Jul 27 2020 at 21:31):

fintype_bot explicitly enumerates the trivial group as {1}, whereas set_fintype says that any decidable subset of a fintype is a fintype.

#### Carl Friedrich Bolz-Tereick (Jul 28 2020 at 09:27):

fwiw, I am constantly fighting issues like that, and find it indeed very frustrating

#### Johan Commelin (Jul 28 2020 at 09:28):

@Carl Friedrich Bolz-Tereick Also with fintype? Or with other instances?

#### Carl Friedrich Bolz-Tereick (Jul 28 2020 at 09:29):

no, specifically fintype (I am doing things with finite groups)

#### Carl Friedrich Bolz-Tereick (Jul 28 2020 at 09:37):

@Johan Commelin I'll try to post a concrete example soon (still busy with post-semester admin)

Last updated: May 19 2021 at 00:40 UTC