Zulip Chat Archive

Stream: general

Topic: Using type classes in definitions


view this post on Zulip Robert Maxton (Oct 31 2020 at 17:06):

So, I have a theorem:

theorem class_equation (G: Type*) [fin_group G]:
  fintype.card G =
    fintype.card (center G)
      + ( x in (conjugacy_classes G), fintype.card x) :=
    sorry

and I have proofs that conjugacy_classes G coerces to a fintype, as are all sets in conjugacy_classes G. How do I tell Lean that those proofs exist, so I can use ∑ and fintype.card x in the statement of the theorem?

view this post on Zulip Johan Commelin (Oct 31 2020 at 17:08):

Do you have instance : fintype (conjugacy_classes G) somewhere?

view this post on Zulip Johan Commelin (Oct 31 2020 at 17:08):

I don't know what you mean by "coerces to a fintype"

view this post on Zulip Johan Commelin (Oct 31 2020 at 17:09):

Note that ∑ x in foo is summing over a finset, whereas ∑ x : foo is summing over a Type (and there must be an instance of fintype foo).

view this post on Zulip Johan Commelin (Oct 31 2020 at 17:11):

Note that there is also finset.card, if you are taking the cardinality of a finset.

view this post on Zulip Robert Maxton (Oct 31 2020 at 17:12):

Well, what I have is a proof that, under certain conditions, there exists an instance of fintype (conjugacy_classes G). I'm not entirely sure how to write a dependent instance like that; do I have to define a structure for it, maybe?

view this post on Zulip Robert Maxton (Oct 31 2020 at 17:20):

and by "coerces to a fintype" I just mean fintype ↥(conjugacy_classes G)

view this post on Zulip Kevin Buzzard (Oct 31 2020 at 17:21):

I don't understand the question. Are you asking how to make a term of that type, or saying you can make a term of that type?

view this post on Zulip Robert Maxton (Oct 31 2020 at 17:22):

I'm saying I can make a term of that type, but not always; so my ability to coherently state my theorem is conditional.

view this post on Zulip Robert Maxton (Oct 31 2020 at 17:22):

Which actually sounds pretty 'just make a dedicated structure'-ish to me, except that I seem to have accidentally gotten it working ...

view this post on Zulip Robert Maxton (Oct 31 2020 at 17:22):

but now I want to know why this works:

theorem class_equation (G: Type*) [fin_group G]:
  fintype.card G =
    fintype.card (center G)
      + ( s: (conjugacy_classes G), fintype.card s) :=
begin
  sorry
end

view this post on Zulip Johan Commelin (Oct 31 2020 at 17:28):

We can't answer that without more context.

view this post on Zulip Johan Commelin (Oct 31 2020 at 17:29):

You'll need to link to a file with more code.

view this post on Zulip Robert Maxton (Oct 31 2020 at 17:31):

that's an mwe lol

view this post on Zulip Robert Maxton (Oct 31 2020 at 17:31):

or almost

view this post on Zulip Robert Maxton (Oct 31 2020 at 17:31):

import group_theory.subgroup
import group_theory.group_action
import data.fintype.basic
import algebra.big_operators

open subgroup
open_locale big_operators
open_locale classical

class fin_group (G: Type*) extends group G, fintype G

def conjugacy_classes (G: Type*) [group G]: set (set G) :=
  { s |  a:G, s = group.conjugates a }

def nontrivial_conjugacy_classes (G: Type*) [group G]: set (set G) :=
  { s  conjugacy_classes G | nontrivial s }

theorem class_equation (G: Type*) [fin_group G]:
  fintype.card G =
    fintype.card (center G)
      + ( s: (nontrivial_conjugacy_classes G), fintype.card s) :=
begin
  sorry
end

view this post on Zulip Robert Maxton (Oct 31 2020 at 17:31):

there, that's an mwe

view this post on Zulip Robert Maxton (Oct 31 2020 at 17:31):

I have no idea why this works and I'm vaguely suspicious it shouldn't

view this post on Zulip Johan Commelin (Oct 31 2020 at 17:33):

Lean knows that s : set X and [fintype X] implies [fintype s]

view this post on Zulip Johan Commelin (Oct 31 2020 at 17:33):

Are you using VS code?

view this post on Zulip Johan Commelin (Oct 31 2020 at 17:33):

If so, you can explore your statement with the widgets in the infoview.

view this post on Zulip Johan Commelin (Oct 31 2020 at 17:33):

Click on the \sum symbol, and then click on finset.univ

view this post on Zulip Johan Commelin (Oct 31 2020 at 17:34):

You'll see subtype.fintype show up in a pop-up window.

view this post on Zulip Kevin Buzzard (Oct 31 2020 at 17:34):

You put open_locale classical so now sanity prevails and everything which is obviously finite classically is known to be finite in lean

view this post on Zulip Johan Commelin (Oct 31 2020 at 17:35):

If you want it to break, add @[irreducible] before one of the defs.

view this post on Zulip Robert Maxton (Oct 31 2020 at 17:35):

@Kevin Buzzard ahh, okay. That would make sense. I had kind of gotten used to having it off

view this post on Zulip Robert Maxton (Oct 31 2020 at 17:36):

and yeah I've been wandering around my file in VS Code but wasn't really getting anywhere

view this post on Zulip Mario Carneiro (Oct 31 2020 at 17:46):

By the way, regarding your earlier question about proving that congugacy_classes is finite, you can express it as finset.image group.conjugates_finset finset.univ provided that G has decidable equality

view this post on Zulip Mario Carneiro (Oct 31 2020 at 17:47):

where group.conjugates_finset a is defined as finset.image (\lam g, g^-1 * a * g) finset.univ


Last updated: May 10 2021 at 00:31 UTC