fintype issues

Stream: maths

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

do you have a representative example aka MWE?

[Kevin Buzzard]

On a WIP branch of mathlib :-/

[Mario Carneiro]

a non-compiling example then?

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

In the quotient_group_refactor branch of mathlib, in group_theory.sylow

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

yes

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

fincard seems like a reasonable fix here

[Mario Carneiro]

another fix would be an is_card s n predicate

[Kenny Lau]

I support fincard

[Kevin Buzzard]

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]

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]

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

[Johan Commelin]

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

[Carl Friedrich Bolz-Tereick]

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

[Carl Friedrich Bolz-Tereick]

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