Zulip Chat Archive

Stream: maths

Topic: fintype issues


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 27 2020 at 21:20):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jul 27 2020 at 21:21):

do you have a representative example aka MWE?

view this post on Zulip Kevin Buzzard (Jul 27 2020 at 21:21):

On a WIP branch of mathlib :-/

view this post on Zulip Mario Carneiro (Jul 27 2020 at 21:22):

a non-compiling example then?

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jul 27 2020 at 21:22):

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

view this post on Zulip Kevin Buzzard (Jul 27 2020 at 21:23):

In the quotient_group_refactor branch of mathlib, in group_theory.sylow

view this post on Zulip Kevin Buzzard (Jul 27 2020 at 21:23):

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

view this post on Zulip Kevin Buzzard (Jul 27 2020 at 21:24):

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

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Jul 27 2020 at 21:25):

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

view this post on Zulip Kevin Buzzard (Jul 27 2020 at 21:25):

yes

view this post on Zulip 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!

view this post on Zulip Kevin Buzzard (Jul 27 2020 at 21:26):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jul 27 2020 at 21:29):

fincard seems like a reasonable fix here

view this post on Zulip Mario Carneiro (Jul 27 2020 at 21:30):

another fix would be an is_card s n predicate

view this post on Zulip Kenny Lau (Jul 27 2020 at 21:30):

I support fincard

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Carl Friedrich Bolz-Tereick (Jul 28 2020 at 09:27):

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

view this post on Zulip Johan Commelin (Jul 28 2020 at 09:28):

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

view this post on Zulip Carl Friedrich Bolz-Tereick (Jul 28 2020 at 09:29):

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

view this post on Zulip 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